Step | Hyp | Ref
| Expression |
1 | | 1cnd 7964 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ 𝑁 = 0) → 1 ∈
ℂ) |
2 | | simp1 997 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) → 𝐴 ∈ ℂ) |
3 | | nnuz 9552 |
. . . . . . . 8
⊢ ℕ =
(ℤ≥‘1) |
4 | | 1zzd 9269 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → 1 ∈
ℤ) |
5 | | fvconst2g 5726 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℕ) →
((ℕ × {𝐴})‘𝑥) = 𝐴) |
6 | | simpl 109 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℕ) → 𝐴 ∈
ℂ) |
7 | 5, 6 | eqeltrd 2254 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℕ) →
((ℕ × {𝐴})‘𝑥) ∈ ℂ) |
8 | | mulcl 7929 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) ∈ ℂ) |
9 | 8 | adantl 277 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) ∈ ℂ) |
10 | 3, 4, 7, 9 | seqf 10447 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → seq1(
· , (ℕ × {𝐴})):ℕ⟶ℂ) |
11 | 2, 10 | syl 14 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) → seq1( · ,
(ℕ × {𝐴})):ℕ⟶ℂ) |
12 | 11 | ad2antrr 488 |
. . . . 5
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ 0 < 𝑁) → seq1( · , (ℕ ×
{𝐴})):ℕ⟶ℂ) |
13 | | simp2 998 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) → 𝑁 ∈ ℤ) |
14 | 13 | ad2antrr 488 |
. . . . . 6
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ 0 < 𝑁) → 𝑁 ∈ ℤ) |
15 | | simpr 110 |
. . . . . 6
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ 0 < 𝑁) → 0 < 𝑁) |
16 | | elnnz 9252 |
. . . . . 6
⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℤ ∧ 0 <
𝑁)) |
17 | 14, 15, 16 | sylanbrc 417 |
. . . . 5
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ 0 < 𝑁) → 𝑁 ∈ ℕ) |
18 | 12, 17 | ffvelcdmd 5648 |
. . . 4
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ 0 < 𝑁) → (seq1( · , (ℕ ×
{𝐴}))‘𝑁) ∈
ℂ) |
19 | 11 | ad2antrr 488 |
. . . . . 6
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → seq1( · , (ℕ ×
{𝐴})):ℕ⟶ℂ) |
20 | 13 | ad2antrr 488 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → 𝑁 ∈ ℤ) |
21 | 20 | znegcld 9366 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → -𝑁 ∈ ℤ) |
22 | | simpr 110 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → ¬ 0 < 𝑁) |
23 | | simplr 528 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → ¬ 𝑁 = 0) |
24 | | eqcom 2179 |
. . . . . . . . . . . 12
⊢ (𝑁 = 0 ↔ 0 = 𝑁) |
25 | 23, 24 | sylnib 676 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → ¬ 0 = 𝑁) |
26 | | ioran 752 |
. . . . . . . . . . 11
⊢ (¬ (0
< 𝑁 ∨ 0 = 𝑁) ↔ (¬ 0 < 𝑁 ∧ ¬ 0 = 𝑁)) |
27 | 22, 25, 26 | sylanbrc 417 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → ¬ (0 < 𝑁 ∨ 0 = 𝑁)) |
28 | | 0zd 9254 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → 0 ∈ ℤ) |
29 | | zleloe 9289 |
. . . . . . . . . . 11
⊢ ((0
∈ ℤ ∧ 𝑁
∈ ℤ) → (0 ≤ 𝑁 ↔ (0 < 𝑁 ∨ 0 = 𝑁))) |
30 | 28, 20, 29 | syl2anc 411 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → (0 ≤ 𝑁 ↔ (0 < 𝑁 ∨ 0 = 𝑁))) |
31 | 27, 30 | mtbird 673 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → ¬ 0 ≤ 𝑁) |
32 | | zltnle 9288 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ 0 ∈
ℤ) → (𝑁 < 0
↔ ¬ 0 ≤ 𝑁)) |
33 | 20, 28, 32 | syl2anc 411 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → (𝑁 < 0 ↔ ¬ 0 ≤ 𝑁)) |
34 | 31, 33 | mpbird 167 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → 𝑁 < 0) |
35 | 20 | zred 9364 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → 𝑁 ∈ ℝ) |
36 | 35 | lt0neg1d 8462 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → (𝑁 < 0 ↔ 0 < -𝑁)) |
37 | 34, 36 | mpbid 147 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → 0 < -𝑁) |
38 | | elnnz 9252 |
. . . . . . 7
⊢ (-𝑁 ∈ ℕ ↔ (-𝑁 ∈ ℤ ∧ 0 <
-𝑁)) |
39 | 21, 37, 38 | sylanbrc 417 |
. . . . . 6
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → -𝑁 ∈ ℕ) |
40 | 19, 39 | ffvelcdmd 5648 |
. . . . 5
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → (seq1( · , (ℕ ×
{𝐴}))‘-𝑁) ∈
ℂ) |
41 | 2 | ad2antrr 488 |
. . . . . 6
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → 𝐴 ∈ ℂ) |
42 | | simpll3 1038 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → (𝐴 # 0 ∨ 0 ≤ 𝑁)) |
43 | 31, 42 | ecased 1349 |
. . . . . 6
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → 𝐴 # 0) |
44 | 41, 43, 39 | exp3vallem 10507 |
. . . . 5
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → (seq1( · , (ℕ ×
{𝐴}))‘-𝑁) # 0) |
45 | 40, 44 | recclapd 8727 |
. . . 4
⊢ ((((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) ∧ ¬ 0 < 𝑁) → (1 / (seq1( · , (ℕ
× {𝐴}))‘-𝑁)) ∈
ℂ) |
46 | | 0zd 9254 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) → 0 ∈
ℤ) |
47 | | simpl2 1001 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) → 𝑁 ∈ ℤ) |
48 | | zdclt 9319 |
. . . . 5
⊢ ((0
∈ ℤ ∧ 𝑁
∈ ℤ) → DECID 0 < 𝑁) |
49 | 46, 47, 48 | syl2anc 411 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) → DECID 0 <
𝑁) |
50 | 18, 45, 49 | ifcldadc 3563 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) ∧ ¬ 𝑁 = 0) → if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}))‘𝑁), (1 / (seq1( · , (ℕ ×
{𝐴}))‘-𝑁))) ∈
ℂ) |
51 | | 0zd 9254 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) → 0 ∈
ℤ) |
52 | | zdceq 9317 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ 0 ∈
ℤ) → DECID 𝑁 = 0) |
53 | 13, 51, 52 | syl2anc 411 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) → DECID
𝑁 = 0) |
54 | 1, 50, 53 | ifcldadc 3563 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) → if(𝑁 = 0, 1, if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}))‘𝑁), (1 / (seq1( · , (ℕ ×
{𝐴}))‘-𝑁)))) ∈
ℂ) |
55 | | sneq 3602 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → {𝑥} = {𝐴}) |
56 | 55 | xpeq2d 4647 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (ℕ × {𝑥}) = (ℕ × {𝐴})) |
57 | 56 | seqeq3d 10439 |
. . . . . 6
⊢ (𝑥 = 𝐴 → seq1( · , (ℕ ×
{𝑥})) = seq1( · ,
(ℕ × {𝐴}))) |
58 | 57 | fveq1d 5513 |
. . . . 5
⊢ (𝑥 = 𝐴 → (seq1( · , (ℕ ×
{𝑥}))‘𝑦) = (seq1( · , (ℕ
× {𝐴}))‘𝑦)) |
59 | 57 | fveq1d 5513 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (seq1( · , (ℕ ×
{𝑥}))‘-𝑦) = (seq1( · , (ℕ
× {𝐴}))‘-𝑦)) |
60 | 59 | oveq2d 5885 |
. . . . 5
⊢ (𝑥 = 𝐴 → (1 / (seq1( · , (ℕ
× {𝑥}))‘-𝑦)) = (1 / (seq1( · ,
(ℕ × {𝐴}))‘-𝑦))) |
61 | 58, 60 | ifeq12d 3553 |
. . . 4
⊢ (𝑥 = 𝐴 → if(0 < 𝑦, (seq1( · , (ℕ × {𝑥}))‘𝑦), (1 / (seq1( · , (ℕ ×
{𝑥}))‘-𝑦))) = if(0 < 𝑦, (seq1( · , (ℕ
× {𝐴}))‘𝑦), (1 / (seq1( · ,
(ℕ × {𝐴}))‘-𝑦)))) |
62 | 61 | ifeq2d 3552 |
. . 3
⊢ (𝑥 = 𝐴 → if(𝑦 = 0, 1, if(0 < 𝑦, (seq1( · , (ℕ × {𝑥}))‘𝑦), (1 / (seq1( · , (ℕ ×
{𝑥}))‘-𝑦)))) = if(𝑦 = 0, 1, if(0 < 𝑦, (seq1( · , (ℕ × {𝐴}))‘𝑦), (1 / (seq1( · , (ℕ ×
{𝐴}))‘-𝑦))))) |
63 | | eqeq1 2184 |
. . . 4
⊢ (𝑦 = 𝑁 → (𝑦 = 0 ↔ 𝑁 = 0)) |
64 | | breq2 4004 |
. . . . 5
⊢ (𝑦 = 𝑁 → (0 < 𝑦 ↔ 0 < 𝑁)) |
65 | | fveq2 5511 |
. . . . 5
⊢ (𝑦 = 𝑁 → (seq1( · , (ℕ ×
{𝐴}))‘𝑦) = (seq1( · , (ℕ
× {𝐴}))‘𝑁)) |
66 | | negeq 8140 |
. . . . . . 7
⊢ (𝑦 = 𝑁 → -𝑦 = -𝑁) |
67 | 66 | fveq2d 5515 |
. . . . . 6
⊢ (𝑦 = 𝑁 → (seq1( · , (ℕ ×
{𝐴}))‘-𝑦) = (seq1( · , (ℕ
× {𝐴}))‘-𝑁)) |
68 | 67 | oveq2d 5885 |
. . . . 5
⊢ (𝑦 = 𝑁 → (1 / (seq1( · , (ℕ
× {𝐴}))‘-𝑦)) = (1 / (seq1( · ,
(ℕ × {𝐴}))‘-𝑁))) |
69 | 64, 65, 68 | ifbieq12d 3560 |
. . . 4
⊢ (𝑦 = 𝑁 → if(0 < 𝑦, (seq1( · , (ℕ × {𝐴}))‘𝑦), (1 / (seq1( · , (ℕ ×
{𝐴}))‘-𝑦))) = if(0 < 𝑁, (seq1( · , (ℕ
× {𝐴}))‘𝑁), (1 / (seq1( · ,
(ℕ × {𝐴}))‘-𝑁)))) |
70 | 63, 69 | ifbieq2d 3558 |
. . 3
⊢ (𝑦 = 𝑁 → if(𝑦 = 0, 1, if(0 < 𝑦, (seq1( · , (ℕ × {𝐴}))‘𝑦), (1 / (seq1( · , (ℕ ×
{𝐴}))‘-𝑦)))) = if(𝑁 = 0, 1, if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}))‘𝑁), (1 / (seq1( · , (ℕ ×
{𝐴}))‘-𝑁))))) |
71 | | df-exp 10506 |
. . 3
⊢ ↑ =
(𝑥 ∈ ℂ, 𝑦 ∈ ℤ ↦ if(𝑦 = 0, 1, if(0 < 𝑦, (seq1( · , (ℕ
× {𝑥}))‘𝑦), (1 / (seq1( · ,
(ℕ × {𝑥}))‘-𝑦))))) |
72 | 62, 70, 71 | ovmpog 6003 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ if(𝑁 = 0, 1, if(0 < 𝑁, (seq1( · , (ℕ
× {𝐴}))‘𝑁), (1 / (seq1( · ,
(ℕ × {𝐴}))‘-𝑁)))) ∈ ℂ) → (𝐴↑𝑁) = if(𝑁 = 0, 1, if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}))‘𝑁), (1 / (seq1( · , (ℕ ×
{𝐴}))‘-𝑁))))) |
73 | 54, 72 | syld3an3 1283 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ∧ (𝐴 # 0 ∨ 0 ≤ 𝑁)) → (𝐴↑𝑁) = if(𝑁 = 0, 1, if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}))‘𝑁), (1 / (seq1( · , (ℕ ×
{𝐴}))‘-𝑁))))) |