Theorem expival 9808

Description: Value of exponentiation to integer powers. (Contributed by Jim Kingdon, 7-Jun-2020.)

Assertion

Ref	Expression
expival	⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) → (𝐴↑𝑁) = if(𝑁 = 0, 1, if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁)))))

Proof of Theorem expival

Dummy variables 𝑥 𝑦 𝑧 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		iftrue 3381	. . . . 5 ⊢ (𝑁 = 0 → if(𝑁 = 0, 1, if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁)))) = 1)
2		ax-1cn 7359	. . . . 5 ⊢ 1 ∈ ℂ
3	1, 2	syl6eqel 2175	. . . 4 ⊢ (𝑁 = 0 → if(𝑁 = 0, 1, if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁)))) ∈ ℂ)
4	3	a1i 9	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) → (𝑁 = 0 → if(𝑁 = 0, 1, if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁)))) ∈ ℂ))
5		elnnz 8670	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℤ ∧ 0 < 𝑁))
6		elnnuz 8964	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈ (ℤ≥‘1))
7	5, 6	sylbb1 135	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℤ ∧ 0 < 𝑁) → 𝑁 ∈ (ℤ≥‘1))
8	7	adantll 460	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ) ∧ 0 < 𝑁) → 𝑁 ∈ (ℤ≥‘1))
9		simpl 107	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ 𝑧 ∈ (ℤ≥‘1)) → 𝐴 ∈ ℂ)
10		elnnuz 8964	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ ℕ ↔ 𝑧 ∈ (ℤ≥‘1))
11		fvconst2g 5454	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℂ ∧ 𝑧 ∈ ℕ) → ((ℕ × {𝐴})‘𝑧) = 𝐴)
12	10, 11	sylan2br 282	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℂ ∧ 𝑧 ∈ (ℤ≥‘1)) → ((ℕ × {𝐴})‘𝑧) = 𝐴)
13	12	eleq1d 2153	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ 𝑧 ∈ (ℤ≥‘1)) → (((ℕ × {𝐴})‘𝑧) ∈ ℂ ↔ 𝐴 ∈ ℂ))
14	9, 13	mpbird 165	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ 𝑧 ∈ (ℤ≥‘1)) → ((ℕ × {𝐴})‘𝑧) ∈ ℂ)
15	14	adantlr 461	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ) ∧ 𝑧 ∈ (ℤ≥‘1)) → ((ℕ × {𝐴})‘𝑧) ∈ ℂ)
16	15	adantlr 461	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ) ∧ 0 < 𝑁) ∧ 𝑧 ∈ (ℤ≥‘1)) → ((ℕ × {𝐴})‘𝑧) ∈ ℂ)
17		mulcl 7390	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (𝑧 · 𝑤) ∈ ℂ)
18	17	adantl 271	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ) ∧ 0 < 𝑁) ∧ (𝑧 ∈ ℂ ∧ 𝑤 ∈ ℂ)) → (𝑧 · 𝑤) ∈ ℂ)
19	8, 16, 18	iseqcl 9770	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ) ∧ 0 < 𝑁) → (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁) ∈ ℂ)
20		iftrue 3381	. . . . . . . . . . . 12 ⊢ (0 < 𝑁 → if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁))) = (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁))
21	20	eleq1d 2153	. . . . . . . . . . 11 ⊢ (0 < 𝑁 → (if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁))) ∈ ℂ ↔ (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁) ∈ ℂ))
22	21	adantl 271	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ) ∧ 0 < 𝑁) → (if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁))) ∈ ℂ ↔ (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁) ∈ ℂ))
23	19, 22	mpbird 165	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ) ∧ 0 < 𝑁) → if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁))) ∈ ℂ)
24	23	ex 113	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ) → (0 < 𝑁 → if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁))) ∈ ℂ))
25	24	adantr 270	. . . . . . 7 ⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → (0 < 𝑁 → if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁))) ∈ ℂ))
26	25	3adantl3 1099	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) → (0 < 𝑁 → if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁))) ∈ ℂ))
27		simpll2 981	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → 𝑁 ∈ ℤ)
28	27	znegcld 8780	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → -𝑁 ∈ ℤ)
29	27	zred 8778	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → 𝑁 ∈ ℝ)
30		0red 7410	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → 0 ∈ ℝ)
31		simpr 108	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → ¬ 0 < 𝑁)
32	29, 30, 31	nltled 7525	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → 𝑁 ≤ 0)
33		simplr 497	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → ¬ 𝑁 = 0)
34	33	neneqad 2330	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → 𝑁 ≠ 0)
35	34	necomd 2337	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → 0 ≠ 𝑁)
36		0z 8671	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ ℤ
37		zltlen 8735	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℤ ∧ 0 ∈ ℤ) → (𝑁 < 0 ↔ (𝑁 ≤ 0 ∧ 0 ≠ 𝑁)))
38	36, 37	mpan2 416	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℤ → (𝑁 < 0 ↔ (𝑁 ≤ 0 ∧ 0 ≠ 𝑁)))
39	38	3ad2ant2 963	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) → (𝑁 < 0 ↔ (𝑁 ≤ 0 ∧ 0 ≠ 𝑁)))
40	39	ad2antrr 472	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → (𝑁 < 0 ↔ (𝑁 ≤ 0 ∧ 0 ≠ 𝑁)))
41	32, 35, 40	mpbir2and 888	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → 𝑁 < 0)
42	29	lt0neg1d 7911	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → (𝑁 < 0 ↔ 0 < -𝑁))
43	41, 42	mpbid 145	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → 0 < -𝑁)
44		elnnz 8670	. . . . . . . . . . . 12 ⊢ (-𝑁 ∈ ℕ ↔ (-𝑁 ∈ ℤ ∧ 0 < -𝑁))
45	28, 43, 44	sylanbrc 408	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → -𝑁 ∈ ℕ)
46		elnnuz 8964	. . . . . . . . . . 11 ⊢ (-𝑁 ∈ ℕ ↔ -𝑁 ∈ (ℤ≥‘1))
47	45, 46	sylib 120	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → -𝑁 ∈ (ℤ≥‘1))
48	14	3ad2antl1 1103	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ 𝑧 ∈ (ℤ≥‘1)) → ((ℕ × {𝐴})‘𝑧) ∈ ℂ)
49	48	adantlr 461	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ 𝑧 ∈ (ℤ≥‘1)) → ((ℕ × {𝐴})‘𝑧) ∈ ℂ)
50	49	adantlr 461	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) ∧ 𝑧 ∈ (ℤ≥‘1)) → ((ℕ × {𝐴})‘𝑧) ∈ ℂ)
51	17	adantl 271	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) ∧ (𝑧 ∈ ℂ ∧ 𝑤 ∈ ℂ)) → (𝑧 · 𝑤) ∈ ℂ)
52	47, 50, 51	iseqcl 9770	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁) ∈ ℂ)
53		simpll1 980	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → 𝐴 ∈ ℂ)
54		expivallem 9807	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0 ∧ -𝑁 ∈ ℕ) → (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁) # 0)
55	54	3com23 1147	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ -𝑁 ∈ ℕ ∧ 𝐴 # 0) → (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁) # 0)
56	55	3expia 1143	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ -𝑁 ∈ ℕ) → (𝐴 # 0 → (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁) # 0))
57	53, 45, 56	syl2anc 403	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → (𝐴 # 0 → (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁) # 0))
58	35	neneqd 2272	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → ¬ 0 = 𝑁)
59		ioran 702	. . . . . . . . . . . . 13 ⊢ (¬ (0 < 𝑁 ∨ 0 = 𝑁) ↔ (¬ 0 < 𝑁 ∧ ¬ 0 = 𝑁))
60	31, 58, 59	sylanbrc 408	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → ¬ (0 < 𝑁 ∨ 0 = 𝑁))
61		zleloe 8707	. . . . . . . . . . . . . . 15 ⊢ ((0 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (0 ≤ 𝑁 ↔ (0 < 𝑁 ∨ 0 = 𝑁)))
62	36, 61	mpan 415	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℤ → (0 ≤ 𝑁 ↔ (0 < 𝑁 ∨ 0 = 𝑁)))
63	62	3ad2ant2 963	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) → (0 ≤ 𝑁 ↔ (0 < 𝑁 ∨ 0 = 𝑁)))
64	63	ad2antrr 472	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → (0 ≤ 𝑁 ↔ (0 < 𝑁 ∨ 0 = 𝑁)))
65	60, 64	mtbird 631	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → ¬ 0 ≤ 𝑁)
66	65	pm2.21d 582	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → (0 ≤ 𝑁 → (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁) # 0))
67		simpll3 982	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → (𝐴 # 0 ∨ 0 ≤ 𝑁))
68	57, 66, 67	mpjaod 671	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁) # 0)
69	52, 68	recclapd 8164	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁)) ∈ ℂ)
70		iffalse 3384	. . . . . . . . . 10 ⊢ (¬ 0 < 𝑁 → if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁))) = (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁)))
71	70	eleq1d 2153	. . . . . . . . 9 ⊢ (¬ 0 < 𝑁 → (if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁))) ∈ ℂ ↔ (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁)) ∈ ℂ))
72	71	adantl 271	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → (if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁))) ∈ ℂ ↔ (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁)) ∈ ℂ))
73	69, 72	mpbird 165	. . . . . . 7 ⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁))) ∈ ℂ)
74	73	ex 113	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) → (¬ 0 < 𝑁 → if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁))) ∈ ℂ))
75		zdclt 8734	. . . . . . . . . . 11 ⊢ ((0 ∈ ℤ ∧ 𝑁 ∈ ℤ) → DECID 0 < 𝑁)
76	36, 75	mpan 415	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℤ → DECID 0 < 𝑁)
77		df-dc 779	. . . . . . . . . 10 ⊢ (DECID 0 < 𝑁 ↔ (0 < 𝑁 ∨ ¬ 0 < 𝑁))
78	76, 77	sylib 120	. . . . . . . . 9 ⊢ (𝑁 ∈ ℤ → (0 < 𝑁 ∨ ¬ 0 < 𝑁))
79	78	adantl 271	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ) → (0 < 𝑁 ∨ ¬ 0 < 𝑁))
80	79	adantr 270	. . . . . . 7 ⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → (0 < 𝑁 ∨ ¬ 0 < 𝑁))
81	80	3adantl3 1099	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) → (0 < 𝑁 ∨ ¬ 0 < 𝑁))
82	26, 74, 81	mpjaod 671	. . . . 5 ⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) → if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁))) ∈ ℂ)
83		iffalse 3384	. . . . . . 7 ⊢ (¬ 𝑁 = 0 → if(𝑁 = 0, 1, if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁)))) = if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁))))
84	83	eleq1d 2153	. . . . . 6 ⊢ (¬ 𝑁 = 0 → (if(𝑁 = 0, 1, if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁)))) ∈ ℂ ↔ if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁))) ∈ ℂ))
85	84	adantl 271	. . . . 5 ⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) → (if(𝑁 = 0, 1, if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁)))) ∈ ℂ ↔ if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁))) ∈ ℂ))
86	82, 85	mpbird 165	. . . 4 ⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) → if(𝑁 = 0, 1, if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁)))) ∈ ℂ)
87	86	ex 113	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) → (¬ 𝑁 = 0 → if(𝑁 = 0, 1, if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁)))) ∈ ℂ))
88		zdceq 8732	. . . . . 6 ⊢ ((𝑁 ∈ ℤ ∧ 0 ∈ ℤ) → DECID 𝑁 = 0)
89	36, 88	mpan2 416	. . . . 5 ⊢ (𝑁 ∈ ℤ → DECID 𝑁 = 0)
90		df-dc 779	. . . . 5 ⊢ (DECID 𝑁 = 0 ↔ (𝑁 = 0 ∨ ¬ 𝑁 = 0))
91	89, 90	sylib 120	. . . 4 ⊢ (𝑁 ∈ ℤ → (𝑁 = 0 ∨ ¬ 𝑁 = 0))
92	91	3ad2ant2 963	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) → (𝑁 = 0 ∨ ¬ 𝑁 = 0))
93	4, 87, 92	mpjaod 671	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) → if(𝑁 = 0, 1, if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁)))) ∈ ℂ)
94		sneq 3436	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → {𝑥} = {𝐴})
95	94	xpeq2d 4428	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (ℕ × {𝑥}) = (ℕ × {𝐴}))
96		iseqeq3 9759	. . . . . . 7 ⊢ ((ℕ × {𝑥}) = (ℕ × {𝐴}) → seq1( · , (ℕ × {𝑥}), ℂ) = seq1( · , (ℕ × {𝐴}), ℂ))
97	95, 96	syl 14	. . . . . 6 ⊢ (𝑥 = 𝐴 → seq1( · , (ℕ × {𝑥}), ℂ) = seq1( · , (ℕ × {𝐴}), ℂ))
98	97	fveq1d 5258	. . . . 5 ⊢ (𝑥 = 𝐴 → (seq1( · , (ℕ × {𝑥}), ℂ)‘𝑦) = (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑦))
99	97	fveq1d 5258	. . . . . 6 ⊢ (𝑥 = 𝐴 → (seq1( · , (ℕ × {𝑥}), ℂ)‘-𝑦) = (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑦))
100	99	oveq2d 5610	. . . . 5 ⊢ (𝑥 = 𝐴 → (1 / (seq1( · , (ℕ × {𝑥}), ℂ)‘-𝑦)) = (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑦)))
101	98, 100	ifeq12d 3393	. . . 4 ⊢ (𝑥 = 𝐴 → if(0 < 𝑦, (seq1( · , (ℕ × {𝑥}), ℂ)‘𝑦), (1 / (seq1( · , (ℕ × {𝑥}), ℂ)‘-𝑦))) = if(0 < 𝑦, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑦), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑦))))
102	101	ifeq2d 3392	. . 3 ⊢ (𝑥 = 𝐴 → if(𝑦 = 0, 1, if(0 < 𝑦, (seq1( · , (ℕ × {𝑥}), ℂ)‘𝑦), (1 / (seq1( · , (ℕ × {𝑥}), ℂ)‘-𝑦)))) = if(𝑦 = 0, 1, if(0 < 𝑦, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑦), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑦)))))
103		eqeq1 2091	. . . 4 ⊢ (𝑦 = 𝑁 → (𝑦 = 0 ↔ 𝑁 = 0))
104		breq2 3818	. . . . 5 ⊢ (𝑦 = 𝑁 → (0 < 𝑦 ↔ 0 < 𝑁))
105		fveq2 5256	. . . . 5 ⊢ (𝑦 = 𝑁 → (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑦) = (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁))
106		negeq 7596	. . . . . . 7 ⊢ (𝑦 = 𝑁 → -𝑦 = -𝑁)
107	106	fveq2d 5260	. . . . . 6 ⊢ (𝑦 = 𝑁 → (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑦) = (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁))
108	107	oveq2d 5610	. . . . 5 ⊢ (𝑦 = 𝑁 → (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑦)) = (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁)))
109	104, 105, 108	ifbieq12d 3400	. . . 4 ⊢ (𝑦 = 𝑁 → if(0 < 𝑦, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑦), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑦))) = if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁))))
110	103, 109	ifbieq2d 3398	. . 3 ⊢ (𝑦 = 𝑁 → if(𝑦 = 0, 1, if(0 < 𝑦, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑦), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑦)))) = if(𝑁 = 0, 1, if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁)))))
111		df-iexp 9806	. . 3 ⊢ ↑ = (𝑥 ∈ ℂ, 𝑦 ∈ ℤ ↦ if(𝑦 = 0, 1, if(0 < 𝑦, (seq1( · , (ℕ × {𝑥}), ℂ)‘𝑦), (1 / (seq1( · , (ℕ × {𝑥}), ℂ)‘-𝑦)))))
112	102, 110, 111	ovmpt2g 5717	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ if(𝑁 = 0, 1, if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁)))) ∈ ℂ) → (𝐴↑𝑁) = if(𝑁 = 0, 1, if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁)))))
113	93, 112	syld3an3 1217	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) → (𝐴↑𝑁) = if(𝑁 = 0, 1, if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁)))))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 102   ↔ wb 103   ∨ wo 662  DECID wdc 778   ∧ w3a 922   = wceq 1287   ∈ wcel 1436   ≠ wne 2251  ifcif 3376  {csn 3425   class class class wbr 3814   × cxp 4402  ‘cfv 4972  (class class class)co 5594  ℂcc 7269  0cc0 7271  1c1 7272   · cmul 7276   < clt 7443   ≤ cle 7444  -cneg 7575   # cap 7976   / cdiv 8055  ℕcn 8334  ℤcz 8660  ℤ_≥cuz 8928  seqcseq 9754  ↑cexp 9805

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-13 1447  ax-14 1448  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-coll 3922  ax-sep 3925  ax-nul 3933  ax-pow 3977  ax-pr 4003  ax-un 4227  ax-setind 4319  ax-iinf 4369  ax-cnex 7357  ax-resscn 7358  ax-1cn 7359  ax-1re 7360  ax-icn 7361  ax-addcl 7362  ax-addrcl 7363  ax-mulcl 7364  ax-mulrcl 7365  ax-addcom 7366  ax-mulcom 7367  ax-addass 7368  ax-mulass 7369  ax-distr 7370  ax-i2m1 7371  ax-0lt1 7372  ax-1rid 7373  ax-0id 7374  ax-rnegex 7375  ax-precex 7376  ax-cnre 7377  ax-pre-ltirr 7378  ax-pre-ltwlin 7379  ax-pre-lttrn 7380  ax-pre-apti 7381  ax-pre-ltadd 7382  ax-pre-mulgt0 7383  ax-pre-mulext 7384

This theorem depends on definitions:  df-bi 115  df-dc 779  df-3or 923  df-3an 924  df-tru 1290  df-fal 1293  df-nf 1393  df-sb 1690  df-eu 1948  df-mo 1949  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ne 2252  df-nel 2347  df-ral 2360  df-rex 2361  df-reu 2362  df-rmo 2363  df-rab 2364  df-v 2616  df-sbc 2829  df-csb 2922  df-dif 2988  df-un 2990  df-in 2992  df-ss 2999  df-nul 3273  df-if 3377  df-pw 3411  df-sn 3431  df-pr 3432  df-op 3434  df-uni 3631  df-int 3666  df-iun 3709  df-br 3815  df-opab 3869  df-mpt 3870  df-tr 3905  df-id 4087  df-po 4090  df-iso 4091  df-iord 4160  df-on 4162  df-ilim 4163  df-suc 4165  df-iom 4372  df-xp 4410  df-rel 4411  df-cnv 4412  df-co 4413  df-dm 4414  df-rn 4415  df-res 4416  df-ima 4417  df-iota 4937  df-fun 4974  df-fn 4975  df-f 4976  df-f1 4977  df-fo 4978  df-f1o 4979  df-fv 4980  df-riota 5550  df-ov 5597  df-oprab 5598  df-mpt2 5599  df-1st 5849  df-2nd 5850  df-recs 6005  df-frec 6091  df-pnf 7445  df-mnf 7446  df-xr 7447  df-ltxr 7448  df-le 7449  df-sub 7576  df-neg 7577  df-reap 7970  df-ap 7977  df-div 8056  df-inn 8335  df-n0 8584  df-z 8661  df-uz 8929  df-iseq 9755  df-iexp 9806

This theorem is referenced by:  expinnval  9809  exp0  9810  expnegap0  9814