Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  expival GIF version

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.
StepHypRef Expression
1 iftrue 3381 . . . . 5 (𝑁 = 0 → if(𝑁 = 0, 1, if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁)))) = 1)
2 ax-1cn 7359 . . . . 5 1 ∈ ℂ
31, 2syl6eqel 2175 . . . 4 (𝑁 = 0 → if(𝑁 = 0, 1, if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁)))) ∈ ℂ)
43a1i 9 . . 3 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) → (𝑁 = 0 → if(𝑁 = 0, 1, if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁)))) ∈ ℂ))
5 elnnz 8670 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℤ ∧ 0 < 𝑁))
6 elnnuz 8964 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ ↔ 𝑁 ∈ (ℤ‘1))
75, 6sylbb1 135 . . . . . . . . . . . 12 ((𝑁 ∈ ℤ ∧ 0 < 𝑁) → 𝑁 ∈ (ℤ‘1))
87adantll 460 . . . . . . . . . . 11 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ) ∧ 0 < 𝑁) → 𝑁 ∈ (ℤ‘1))
9 simpl 107 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℂ ∧ 𝑧 ∈ (ℤ‘1)) → 𝐴 ∈ ℂ)
10 elnnuz 8964 . . . . . . . . . . . . . . . 16 (𝑧 ∈ ℕ ↔ 𝑧 ∈ (ℤ‘1))
11 fvconst2g 5454 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℂ ∧ 𝑧 ∈ ℕ) → ((ℕ × {𝐴})‘𝑧) = 𝐴)
1210, 11sylan2br 282 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℂ ∧ 𝑧 ∈ (ℤ‘1)) → ((ℕ × {𝐴})‘𝑧) = 𝐴)
1312eleq1d 2153 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℂ ∧ 𝑧 ∈ (ℤ‘1)) → (((ℕ × {𝐴})‘𝑧) ∈ ℂ ↔ 𝐴 ∈ ℂ))
149, 13mpbird 165 . . . . . . . . . . . . 13 ((𝐴 ∈ ℂ ∧ 𝑧 ∈ (ℤ‘1)) → ((ℕ × {𝐴})‘𝑧) ∈ ℂ)
1514adantlr 461 . . . . . . . . . . . 12 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ) ∧ 𝑧 ∈ (ℤ‘1)) → ((ℕ × {𝐴})‘𝑧) ∈ ℂ)
1615adantlr 461 . . . . . . . . . . 11 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ) ∧ 0 < 𝑁) ∧ 𝑧 ∈ (ℤ‘1)) → ((ℕ × {𝐴})‘𝑧) ∈ ℂ)
17 mulcl 7390 . . . . . . . . . . . 12 ((𝑧 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (𝑧 · 𝑤) ∈ ℂ)
1817adantl 271 . . . . . . . . . . 11 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ) ∧ 0 < 𝑁) ∧ (𝑧 ∈ ℂ ∧ 𝑤 ∈ ℂ)) → (𝑧 · 𝑤) ∈ ℂ)
198, 16, 18iseqcl 9770 . . . . . . . . . 10 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ) ∧ 0 < 𝑁) → (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁) ∈ ℂ)
20 iftrue 3381 . . . . . . . . . . . 12 (0 < 𝑁 → if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁))) = (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁))
2120eleq1d 2153 . . . . . . . . . . 11 (0 < 𝑁 → (if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁))) ∈ ℂ ↔ (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁) ∈ ℂ))
2221adantl 271 . . . . . . . . . 10 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ) ∧ 0 < 𝑁) → (if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁))) ∈ ℂ ↔ (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁) ∈ ℂ))
2319, 22mpbird 165 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ) ∧ 0 < 𝑁) → if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁))) ∈ ℂ)
2423ex 113 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ) → (0 < 𝑁 → if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁))) ∈ ℂ))
2524adantr 270 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → (0 < 𝑁 → if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁))) ∈ ℂ))
26253adantl3 1099 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) → (0 < 𝑁 → if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁))) ∈ ℂ))
27 simpll2 981 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → 𝑁 ∈ ℤ)
2827znegcld 8780 . . . . . . . . . . . 12 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → -𝑁 ∈ ℤ)
2927zred 8778 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → 𝑁 ∈ ℝ)
30 0red 7410 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → 0 ∈ ℝ)
31 simpr 108 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → ¬ 0 < 𝑁)
3229, 30, 31nltled 7525 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → 𝑁 ≤ 0)
33 simplr 497 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → ¬ 𝑁 = 0)
3433neneqad 2330 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → 𝑁 ≠ 0)
3534necomd 2337 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → 0 ≠ 𝑁)
36 0z 8671 . . . . . . . . . . . . . . . . 17 0 ∈ ℤ
37 zltlen 8735 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ ℤ ∧ 0 ∈ ℤ) → (𝑁 < 0 ↔ (𝑁 ≤ 0 ∧ 0 ≠ 𝑁)))
3836, 37mpan2 416 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℤ → (𝑁 < 0 ↔ (𝑁 ≤ 0 ∧ 0 ≠ 𝑁)))
39383ad2ant2 963 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) → (𝑁 < 0 ↔ (𝑁 ≤ 0 ∧ 0 ≠ 𝑁)))
4039ad2antrr 472 . . . . . . . . . . . . . 14 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → (𝑁 < 0 ↔ (𝑁 ≤ 0 ∧ 0 ≠ 𝑁)))
4132, 35, 40mpbir2and 888 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → 𝑁 < 0)
4229lt0neg1d 7911 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → (𝑁 < 0 ↔ 0 < -𝑁))
4341, 42mpbid 145 . . . . . . . . . . . 12 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → 0 < -𝑁)
44 elnnz 8670 . . . . . . . . . . . 12 (-𝑁 ∈ ℕ ↔ (-𝑁 ∈ ℤ ∧ 0 < -𝑁))
4528, 43, 44sylanbrc 408 . . . . . . . . . . 11 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → -𝑁 ∈ ℕ)
46 elnnuz 8964 . . . . . . . . . . 11 (-𝑁 ∈ ℕ ↔ -𝑁 ∈ (ℤ‘1))
4745, 46sylib 120 . . . . . . . . . 10 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → -𝑁 ∈ (ℤ‘1))
48143ad2antl1 1103 . . . . . . . . . . . 12 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ 𝑧 ∈ (ℤ‘1)) → ((ℕ × {𝐴})‘𝑧) ∈ ℂ)
4948adantlr 461 . . . . . . . . . . 11 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ 𝑧 ∈ (ℤ‘1)) → ((ℕ × {𝐴})‘𝑧) ∈ ℂ)
5049adantlr 461 . . . . . . . . . 10 (((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) ∧ 𝑧 ∈ (ℤ‘1)) → ((ℕ × {𝐴})‘𝑧) ∈ ℂ)
5117adantl 271 . . . . . . . . . 10 (((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) ∧ (𝑧 ∈ ℂ ∧ 𝑤 ∈ ℂ)) → (𝑧 · 𝑤) ∈ ℂ)
5247, 50, 51iseqcl 9770 . . . . . . . . 9 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁) ∈ ℂ)
53 simpll1 980 . . . . . . . . . . 11 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → 𝐴 ∈ ℂ)
54 expivallem 9807 . . . . . . . . . . . . 13 ((𝐴 ∈ ℂ ∧ 𝐴 # 0 ∧ -𝑁 ∈ ℕ) → (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁) # 0)
55543com23 1147 . . . . . . . . . . . 12 ((𝐴 ∈ ℂ ∧ -𝑁 ∈ ℕ ∧ 𝐴 # 0) → (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁) # 0)
56553expia 1143 . . . . . . . . . . 11 ((𝐴 ∈ ℂ ∧ -𝑁 ∈ ℕ) → (𝐴 # 0 → (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁) # 0))
5753, 45, 56syl2anc 403 . . . . . . . . . 10 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → (𝐴 # 0 → (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁) # 0))
5835neneqd 2272 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → ¬ 0 = 𝑁)
59 ioran 702 . . . . . . . . . . . . 13 (¬ (0 < 𝑁 ∨ 0 = 𝑁) ↔ (¬ 0 < 𝑁 ∧ ¬ 0 = 𝑁))
6031, 58, 59sylanbrc 408 . . . . . . . . . . . 12 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → ¬ (0 < 𝑁 ∨ 0 = 𝑁))
61 zleloe 8707 . . . . . . . . . . . . . . 15 ((0 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (0 ≤ 𝑁 ↔ (0 < 𝑁 ∨ 0 = 𝑁)))
6236, 61mpan 415 . . . . . . . . . . . . . 14 (𝑁 ∈ ℤ → (0 ≤ 𝑁 ↔ (0 < 𝑁 ∨ 0 = 𝑁)))
63623ad2ant2 963 . . . . . . . . . . . . 13 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) → (0 ≤ 𝑁 ↔ (0 < 𝑁 ∨ 0 = 𝑁)))
6463ad2antrr 472 . . . . . . . . . . . 12 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → (0 ≤ 𝑁 ↔ (0 < 𝑁 ∨ 0 = 𝑁)))
6560, 64mtbird 631 . . . . . . . . . . 11 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → ¬ 0 ≤ 𝑁)
6665pm2.21d 582 . . . . . . . . . 10 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → (0 ≤ 𝑁 → (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁) # 0))
67 simpll3 982 . . . . . . . . . 10 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → (𝐴 # 0 ∨ 0 ≤ 𝑁))
6857, 66, 67mpjaod 671 . . . . . . . . 9 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁) # 0)
6952, 68recclapd 8164 . . . . . . . 8 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁)) ∈ ℂ)
70 iffalse 3384 . . . . . . . . . 10 (¬ 0 < 𝑁 → if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁))) = (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁)))
7170eleq1d 2153 . . . . . . . . 9 (¬ 0 < 𝑁 → (if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁))) ∈ ℂ ↔ (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁)) ∈ ℂ))
7271adantl 271 . . . . . . . 8 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → (if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁))) ∈ ℂ ↔ (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁)) ∈ ℂ))
7369, 72mpbird 165 . . . . . . 7 ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁))) ∈ ℂ)
7473ex 113 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) → (¬ 0 < 𝑁 → if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁))) ∈ ℂ))
75 zdclt 8734 . . . . . . . . . . 11 ((0 ∈ ℤ ∧ 𝑁 ∈ ℤ) → DECID 0 < 𝑁)
7636, 75mpan 415 . . . . . . . . . 10 (𝑁 ∈ ℤ → DECID 0 < 𝑁)
77 df-dc 779 . . . . . . . . . 10 (DECID 0 < 𝑁 ↔ (0 < 𝑁 ∨ ¬ 0 < 𝑁))
7876, 77sylib 120 . . . . . . . . 9 (𝑁 ∈ ℤ → (0 < 𝑁 ∨ ¬ 0 < 𝑁))
7978adantl 271 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ) → (0 < 𝑁 ∨ ¬ 0 < 𝑁))
8079adantr 270 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ) ∧ ¬ 𝑁 = 0) → (0 < 𝑁 ∨ ¬ 0 < 𝑁))
81803adantl3 1099 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) → (0 < 𝑁 ∨ ¬ 0 < 𝑁))
8226, 74, 81mpjaod 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( · , (ℕ × {𝐴}), ℂ)‘-𝑁))))
8483eleq1d 2153 . . . . . 6 𝑁 = 0 → (if(𝑁 = 0, 1, if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁)))) ∈ ℂ ↔ if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁))) ∈ ℂ))
8584adantl 271 . . . . 5 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) → (if(𝑁 = 0, 1, if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁)))) ∈ ℂ ↔ if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁))) ∈ ℂ))
8682, 85mpbird 165 . . . 4 (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) → if(𝑁 = 0, 1, if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁)))) ∈ ℂ)
8786ex 113 . . 3 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) → (¬ 𝑁 = 0 → if(𝑁 = 0, 1, if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁)))) ∈ ℂ))
88 zdceq 8732 . . . . . 6 ((𝑁 ∈ ℤ ∧ 0 ∈ ℤ) → DECID 𝑁 = 0)
8936, 88mpan2 416 . . . . 5 (𝑁 ∈ ℤ → DECID 𝑁 = 0)
90 df-dc 779 . . . . 5 (DECID 𝑁 = 0 ↔ (𝑁 = 0 ∨ ¬ 𝑁 = 0))
9189, 90sylib 120 . . . 4 (𝑁 ∈ ℤ → (𝑁 = 0 ∨ ¬ 𝑁 = 0))
92913ad2ant2 963 . . 3 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) → (𝑁 = 0 ∨ ¬ 𝑁 = 0))
934, 87, 92mpjaod 671 . 2 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) → if(𝑁 = 0, 1, if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁)))) ∈ ℂ)
94 sneq 3436 . . . . . . . 8 (𝑥 = 𝐴 → {𝑥} = {𝐴})
9594xpeq2d 4428 . . . . . . 7 (𝑥 = 𝐴 → (ℕ × {𝑥}) = (ℕ × {𝐴}))
96 iseqeq3 9759 . . . . . . 7 ((ℕ × {𝑥}) = (ℕ × {𝐴}) → seq1( · , (ℕ × {𝑥}), ℂ) = seq1( · , (ℕ × {𝐴}), ℂ))
9795, 96syl 14 . . . . . 6 (𝑥 = 𝐴 → seq1( · , (ℕ × {𝑥}), ℂ) = seq1( · , (ℕ × {𝐴}), ℂ))
9897fveq1d 5258 . . . . 5 (𝑥 = 𝐴 → (seq1( · , (ℕ × {𝑥}), ℂ)‘𝑦) = (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑦))
9997fveq1d 5258 . . . . . 6 (𝑥 = 𝐴 → (seq1( · , (ℕ × {𝑥}), ℂ)‘-𝑦) = (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑦))
10099oveq2d 5610 . . . . 5 (𝑥 = 𝐴 → (1 / (seq1( · , (ℕ × {𝑥}), ℂ)‘-𝑦)) = (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑦)))
10198, 100ifeq12d 3393 . . . 4 (𝑥 = 𝐴 → if(0 < 𝑦, (seq1( · , (ℕ × {𝑥}), ℂ)‘𝑦), (1 / (seq1( · , (ℕ × {𝑥}), ℂ)‘-𝑦))) = if(0 < 𝑦, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑦), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑦))))
102101ifeq2d 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 (𝑦 = 𝑁 → -𝑦 = -𝑁)
107106fveq2d 5260 . . . . . 6 (𝑦 = 𝑁 → (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑦) = (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁))
108107oveq2d 5610 . . . . 5 (𝑦 = 𝑁 → (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑦)) = (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁)))
109104, 105, 108ifbieq12d 3400 . . . 4 (𝑦 = 𝑁 → if(0 < 𝑦, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑦), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑦))) = if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁))))
110103, 109ifbieq2d 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( · , (ℕ × {𝑥}), ℂ)‘-𝑦)))))
112102, 110, 111ovmpt2g 5717 . 2 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ if(𝑁 = 0, 1, if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁)))) ∈ ℂ) → (𝐴𝑁) = if(𝑁 = 0, 1, if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁)))))
11393, 112syld3an3 1217 1 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) → (𝐴𝑁) = if(𝑁 = 0, 1, if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}), ℂ)‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}), ℂ)‘-𝑁)))))
 Colors of variables: wff set class 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
 Copyright terms: Public domain W3C validator