Step | Hyp | Ref
| Expression |
1 | | oveq2 5540 |
. . . . . 6
⊢ (𝑗 = 1 → (𝐴↑𝑗) = (𝐴↑1)) |
2 | 1 | breq1d 3795 |
. . . . 5
⊢ (𝑗 = 1 → ((𝐴↑𝑗) # 0 ↔ (𝐴↑1) # 0)) |
3 | 2 | bibi1d 231 |
. . . 4
⊢ (𝑗 = 1 → (((𝐴↑𝑗) # 0 ↔ 𝐴 # 0) ↔ ((𝐴↑1) # 0 ↔ 𝐴 # 0))) |
4 | 3 | imbi2d 228 |
. . 3
⊢ (𝑗 = 1 → ((𝐴 ∈ ℂ → ((𝐴↑𝑗) # 0 ↔ 𝐴 # 0)) ↔ (𝐴 ∈ ℂ → ((𝐴↑1) # 0 ↔ 𝐴 # 0)))) |
5 | | oveq2 5540 |
. . . . . 6
⊢ (𝑗 = 𝑘 → (𝐴↑𝑗) = (𝐴↑𝑘)) |
6 | 5 | breq1d 3795 |
. . . . 5
⊢ (𝑗 = 𝑘 → ((𝐴↑𝑗) # 0 ↔ (𝐴↑𝑘) # 0)) |
7 | 6 | bibi1d 231 |
. . . 4
⊢ (𝑗 = 𝑘 → (((𝐴↑𝑗) # 0 ↔ 𝐴 # 0) ↔ ((𝐴↑𝑘) # 0 ↔ 𝐴 # 0))) |
8 | 7 | imbi2d 228 |
. . 3
⊢ (𝑗 = 𝑘 → ((𝐴 ∈ ℂ → ((𝐴↑𝑗) # 0 ↔ 𝐴 # 0)) ↔ (𝐴 ∈ ℂ → ((𝐴↑𝑘) # 0 ↔ 𝐴 # 0)))) |
9 | | oveq2 5540 |
. . . . . 6
⊢ (𝑗 = (𝑘 + 1) → (𝐴↑𝑗) = (𝐴↑(𝑘 + 1))) |
10 | 9 | breq1d 3795 |
. . . . 5
⊢ (𝑗 = (𝑘 + 1) → ((𝐴↑𝑗) # 0 ↔ (𝐴↑(𝑘 + 1)) # 0)) |
11 | 10 | bibi1d 231 |
. . . 4
⊢ (𝑗 = (𝑘 + 1) → (((𝐴↑𝑗) # 0 ↔ 𝐴 # 0) ↔ ((𝐴↑(𝑘 + 1)) # 0 ↔ 𝐴 # 0))) |
12 | 11 | imbi2d 228 |
. . 3
⊢ (𝑗 = (𝑘 + 1) → ((𝐴 ∈ ℂ → ((𝐴↑𝑗) # 0 ↔ 𝐴 # 0)) ↔ (𝐴 ∈ ℂ → ((𝐴↑(𝑘 + 1)) # 0 ↔ 𝐴 # 0)))) |
13 | | oveq2 5540 |
. . . . . 6
⊢ (𝑗 = 𝑁 → (𝐴↑𝑗) = (𝐴↑𝑁)) |
14 | 13 | breq1d 3795 |
. . . . 5
⊢ (𝑗 = 𝑁 → ((𝐴↑𝑗) # 0 ↔ (𝐴↑𝑁) # 0)) |
15 | 14 | bibi1d 231 |
. . . 4
⊢ (𝑗 = 𝑁 → (((𝐴↑𝑗) # 0 ↔ 𝐴 # 0) ↔ ((𝐴↑𝑁) # 0 ↔ 𝐴 # 0))) |
16 | 15 | imbi2d 228 |
. . 3
⊢ (𝑗 = 𝑁 → ((𝐴 ∈ ℂ → ((𝐴↑𝑗) # 0 ↔ 𝐴 # 0)) ↔ (𝐴 ∈ ℂ → ((𝐴↑𝑁) # 0 ↔ 𝐴 # 0)))) |
17 | | exp1 9482 |
. . . 4
⊢ (𝐴 ∈ ℂ → (𝐴↑1) = 𝐴) |
18 | 17 | breq1d 3795 |
. . 3
⊢ (𝐴 ∈ ℂ → ((𝐴↑1) # 0 ↔ 𝐴 # 0)) |
19 | | nnnn0 8295 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℕ0) |
20 | | expp1 9483 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝐴↑(𝑘 + 1)) = ((𝐴↑𝑘) · 𝐴)) |
21 | 20 | breq1d 3795 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ ((𝐴↑(𝑘 + 1)) # 0 ↔ ((𝐴↑𝑘) · 𝐴) # 0)) |
22 | 21 | ancoms 264 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℕ0
∧ 𝐴 ∈ ℂ)
→ ((𝐴↑(𝑘 + 1)) # 0 ↔ ((𝐴↑𝑘) · 𝐴) # 0)) |
23 | 19, 22 | sylan 277 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℕ ∧ 𝐴 ∈ ℂ) → ((𝐴↑(𝑘 + 1)) # 0 ↔ ((𝐴↑𝑘) · 𝐴) # 0)) |
24 | 23 | adantr 270 |
. . . . . . 7
⊢ (((𝑘 ∈ ℕ ∧ 𝐴 ∈ ℂ) ∧ ((𝐴↑𝑘) # 0 ↔ 𝐴 # 0)) → ((𝐴↑(𝑘 + 1)) # 0 ↔ ((𝐴↑𝑘) · 𝐴) # 0)) |
25 | | simplr 496 |
. . . . . . . . 9
⊢ (((𝑘 ∈ ℕ ∧ 𝐴 ∈ ℂ) ∧ ((𝐴↑𝑘) # 0 ↔ 𝐴 # 0)) → 𝐴 ∈ ℂ) |
26 | 19 | ad2antrr 471 |
. . . . . . . . 9
⊢ (((𝑘 ∈ ℕ ∧ 𝐴 ∈ ℂ) ∧ ((𝐴↑𝑘) # 0 ↔ 𝐴 # 0)) → 𝑘 ∈ ℕ0) |
27 | | expcl 9494 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝐴↑𝑘) ∈
ℂ) |
28 | 25, 26, 27 | syl2anc 403 |
. . . . . . . 8
⊢ (((𝑘 ∈ ℕ ∧ 𝐴 ∈ ℂ) ∧ ((𝐴↑𝑘) # 0 ↔ 𝐴 # 0)) → (𝐴↑𝑘) ∈ ℂ) |
29 | 28, 25 | mulap0bd 7747 |
. . . . . . 7
⊢ (((𝑘 ∈ ℕ ∧ 𝐴 ∈ ℂ) ∧ ((𝐴↑𝑘) # 0 ↔ 𝐴 # 0)) → (((𝐴↑𝑘) # 0 ∧ 𝐴 # 0) ↔ ((𝐴↑𝑘) · 𝐴) # 0)) |
30 | | anbi1 453 |
. . . . . . . 8
⊢ (((𝐴↑𝑘) # 0 ↔ 𝐴 # 0) → (((𝐴↑𝑘) # 0 ∧ 𝐴 # 0) ↔ (𝐴 # 0 ∧ 𝐴 # 0))) |
31 | 30 | adantl 271 |
. . . . . . 7
⊢ (((𝑘 ∈ ℕ ∧ 𝐴 ∈ ℂ) ∧ ((𝐴↑𝑘) # 0 ↔ 𝐴 # 0)) → (((𝐴↑𝑘) # 0 ∧ 𝐴 # 0) ↔ (𝐴 # 0 ∧ 𝐴 # 0))) |
32 | 24, 29, 31 | 3bitr2d 214 |
. . . . . 6
⊢ (((𝑘 ∈ ℕ ∧ 𝐴 ∈ ℂ) ∧ ((𝐴↑𝑘) # 0 ↔ 𝐴 # 0)) → ((𝐴↑(𝑘 + 1)) # 0 ↔ (𝐴 # 0 ∧ 𝐴 # 0))) |
33 | | anidm 388 |
. . . . . 6
⊢ ((𝐴 # 0 ∧ 𝐴 # 0) ↔ 𝐴 # 0) |
34 | 32, 33 | syl6bb 194 |
. . . . 5
⊢ (((𝑘 ∈ ℕ ∧ 𝐴 ∈ ℂ) ∧ ((𝐴↑𝑘) # 0 ↔ 𝐴 # 0)) → ((𝐴↑(𝑘 + 1)) # 0 ↔ 𝐴 # 0)) |
35 | 34 | exp31 356 |
. . . 4
⊢ (𝑘 ∈ ℕ → (𝐴 ∈ ℂ → (((𝐴↑𝑘) # 0 ↔ 𝐴 # 0) → ((𝐴↑(𝑘 + 1)) # 0 ↔ 𝐴 # 0)))) |
36 | 35 | a2d 26 |
. . 3
⊢ (𝑘 ∈ ℕ → ((𝐴 ∈ ℂ → ((𝐴↑𝑘) # 0 ↔ 𝐴 # 0)) → (𝐴 ∈ ℂ → ((𝐴↑(𝑘 + 1)) # 0 ↔ 𝐴 # 0)))) |
37 | 4, 8, 12, 16, 18, 36 | nnind 8055 |
. 2
⊢ (𝑁 ∈ ℕ → (𝐴 ∈ ℂ → ((𝐴↑𝑁) # 0 ↔ 𝐴 # 0))) |
38 | 37 | impcom 123 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → ((𝐴↑𝑁) # 0 ↔ 𝐴 # 0)) |