Step | Hyp | Ref
| Expression |
1 | | oveq2 5832 |
. . . . . 6
⊢ (𝑗 = 1 → (𝐴↑𝑗) = (𝐴↑1)) |
2 | 1 | breq1d 3975 |
. . . . 5
⊢ (𝑗 = 1 → ((𝐴↑𝑗) # 0 ↔ (𝐴↑1) # 0)) |
3 | 2 | bibi1d 232 |
. . . 4
⊢ (𝑗 = 1 → (((𝐴↑𝑗) # 0 ↔ 𝐴 # 0) ↔ ((𝐴↑1) # 0 ↔ 𝐴 # 0))) |
4 | 3 | imbi2d 229 |
. . 3
⊢ (𝑗 = 1 → ((𝐴 ∈ ℂ → ((𝐴↑𝑗) # 0 ↔ 𝐴 # 0)) ↔ (𝐴 ∈ ℂ → ((𝐴↑1) # 0 ↔ 𝐴 # 0)))) |
5 | | oveq2 5832 |
. . . . . 6
⊢ (𝑗 = 𝑘 → (𝐴↑𝑗) = (𝐴↑𝑘)) |
6 | 5 | breq1d 3975 |
. . . . 5
⊢ (𝑗 = 𝑘 → ((𝐴↑𝑗) # 0 ↔ (𝐴↑𝑘) # 0)) |
7 | 6 | bibi1d 232 |
. . . 4
⊢ (𝑗 = 𝑘 → (((𝐴↑𝑗) # 0 ↔ 𝐴 # 0) ↔ ((𝐴↑𝑘) # 0 ↔ 𝐴 # 0))) |
8 | 7 | imbi2d 229 |
. . 3
⊢ (𝑗 = 𝑘 → ((𝐴 ∈ ℂ → ((𝐴↑𝑗) # 0 ↔ 𝐴 # 0)) ↔ (𝐴 ∈ ℂ → ((𝐴↑𝑘) # 0 ↔ 𝐴 # 0)))) |
9 | | oveq2 5832 |
. . . . . 6
⊢ (𝑗 = (𝑘 + 1) → (𝐴↑𝑗) = (𝐴↑(𝑘 + 1))) |
10 | 9 | breq1d 3975 |
. . . . 5
⊢ (𝑗 = (𝑘 + 1) → ((𝐴↑𝑗) # 0 ↔ (𝐴↑(𝑘 + 1)) # 0)) |
11 | 10 | bibi1d 232 |
. . . 4
⊢ (𝑗 = (𝑘 + 1) → (((𝐴↑𝑗) # 0 ↔ 𝐴 # 0) ↔ ((𝐴↑(𝑘 + 1)) # 0 ↔ 𝐴 # 0))) |
12 | 11 | imbi2d 229 |
. . 3
⊢ (𝑗 = (𝑘 + 1) → ((𝐴 ∈ ℂ → ((𝐴↑𝑗) # 0 ↔ 𝐴 # 0)) ↔ (𝐴 ∈ ℂ → ((𝐴↑(𝑘 + 1)) # 0 ↔ 𝐴 # 0)))) |
13 | | oveq2 5832 |
. . . . . 6
⊢ (𝑗 = 𝑁 → (𝐴↑𝑗) = (𝐴↑𝑁)) |
14 | 13 | breq1d 3975 |
. . . . 5
⊢ (𝑗 = 𝑁 → ((𝐴↑𝑗) # 0 ↔ (𝐴↑𝑁) # 0)) |
15 | 14 | bibi1d 232 |
. . . 4
⊢ (𝑗 = 𝑁 → (((𝐴↑𝑗) # 0 ↔ 𝐴 # 0) ↔ ((𝐴↑𝑁) # 0 ↔ 𝐴 # 0))) |
16 | 15 | imbi2d 229 |
. . 3
⊢ (𝑗 = 𝑁 → ((𝐴 ∈ ℂ → ((𝐴↑𝑗) # 0 ↔ 𝐴 # 0)) ↔ (𝐴 ∈ ℂ → ((𝐴↑𝑁) # 0 ↔ 𝐴 # 0)))) |
17 | | exp1 10425 |
. . . 4
⊢ (𝐴 ∈ ℂ → (𝐴↑1) = 𝐴) |
18 | 17 | breq1d 3975 |
. . 3
⊢ (𝐴 ∈ ℂ → ((𝐴↑1) # 0 ↔ 𝐴 # 0)) |
19 | | nnnn0 9097 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℕ0) |
20 | | expp1 10426 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝐴↑(𝑘 + 1)) = ((𝐴↑𝑘) · 𝐴)) |
21 | 20 | breq1d 3975 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ ((𝐴↑(𝑘 + 1)) # 0 ↔ ((𝐴↑𝑘) · 𝐴) # 0)) |
22 | 21 | ancoms 266 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℕ0
∧ 𝐴 ∈ ℂ)
→ ((𝐴↑(𝑘 + 1)) # 0 ↔ ((𝐴↑𝑘) · 𝐴) # 0)) |
23 | 19, 22 | sylan 281 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℕ ∧ 𝐴 ∈ ℂ) → ((𝐴↑(𝑘 + 1)) # 0 ↔ ((𝐴↑𝑘) · 𝐴) # 0)) |
24 | 23 | adantr 274 |
. . . . . . 7
⊢ (((𝑘 ∈ ℕ ∧ 𝐴 ∈ ℂ) ∧ ((𝐴↑𝑘) # 0 ↔ 𝐴 # 0)) → ((𝐴↑(𝑘 + 1)) # 0 ↔ ((𝐴↑𝑘) · 𝐴) # 0)) |
25 | | simplr 520 |
. . . . . . . . 9
⊢ (((𝑘 ∈ ℕ ∧ 𝐴 ∈ ℂ) ∧ ((𝐴↑𝑘) # 0 ↔ 𝐴 # 0)) → 𝐴 ∈ ℂ) |
26 | 19 | ad2antrr 480 |
. . . . . . . . 9
⊢ (((𝑘 ∈ ℕ ∧ 𝐴 ∈ ℂ) ∧ ((𝐴↑𝑘) # 0 ↔ 𝐴 # 0)) → 𝑘 ∈ ℕ0) |
27 | | expcl 10437 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝐴↑𝑘) ∈
ℂ) |
28 | 25, 26, 27 | syl2anc 409 |
. . . . . . . 8
⊢ (((𝑘 ∈ ℕ ∧ 𝐴 ∈ ℂ) ∧ ((𝐴↑𝑘) # 0 ↔ 𝐴 # 0)) → (𝐴↑𝑘) ∈ ℂ) |
29 | 28, 25 | mulap0bd 8531 |
. . . . . . 7
⊢ (((𝑘 ∈ ℕ ∧ 𝐴 ∈ ℂ) ∧ ((𝐴↑𝑘) # 0 ↔ 𝐴 # 0)) → (((𝐴↑𝑘) # 0 ∧ 𝐴 # 0) ↔ ((𝐴↑𝑘) · 𝐴) # 0)) |
30 | | anbi1 462 |
. . . . . . . 8
⊢ (((𝐴↑𝑘) # 0 ↔ 𝐴 # 0) → (((𝐴↑𝑘) # 0 ∧ 𝐴 # 0) ↔ (𝐴 # 0 ∧ 𝐴 # 0))) |
31 | 30 | adantl 275 |
. . . . . . 7
⊢ (((𝑘 ∈ ℕ ∧ 𝐴 ∈ ℂ) ∧ ((𝐴↑𝑘) # 0 ↔ 𝐴 # 0)) → (((𝐴↑𝑘) # 0 ∧ 𝐴 # 0) ↔ (𝐴 # 0 ∧ 𝐴 # 0))) |
32 | 24, 29, 31 | 3bitr2d 215 |
. . . . . 6
⊢ (((𝑘 ∈ ℕ ∧ 𝐴 ∈ ℂ) ∧ ((𝐴↑𝑘) # 0 ↔ 𝐴 # 0)) → ((𝐴↑(𝑘 + 1)) # 0 ↔ (𝐴 # 0 ∧ 𝐴 # 0))) |
33 | | anidm 394 |
. . . . . 6
⊢ ((𝐴 # 0 ∧ 𝐴 # 0) ↔ 𝐴 # 0) |
34 | 32, 33 | bitrdi 195 |
. . . . 5
⊢ (((𝑘 ∈ ℕ ∧ 𝐴 ∈ ℂ) ∧ ((𝐴↑𝑘) # 0 ↔ 𝐴 # 0)) → ((𝐴↑(𝑘 + 1)) # 0 ↔ 𝐴 # 0)) |
35 | 34 | exp31 362 |
. . . 4
⊢ (𝑘 ∈ ℕ → (𝐴 ∈ ℂ → (((𝐴↑𝑘) # 0 ↔ 𝐴 # 0) → ((𝐴↑(𝑘 + 1)) # 0 ↔ 𝐴 # 0)))) |
36 | 35 | a2d 26 |
. . 3
⊢ (𝑘 ∈ ℕ → ((𝐴 ∈ ℂ → ((𝐴↑𝑘) # 0 ↔ 𝐴 # 0)) → (𝐴 ∈ ℂ → ((𝐴↑(𝑘 + 1)) # 0 ↔ 𝐴 # 0)))) |
37 | 4, 8, 12, 16, 18, 36 | nnind 8849 |
. 2
⊢ (𝑁 ∈ ℕ → (𝐴 ∈ ℂ → ((𝐴↑𝑁) # 0 ↔ 𝐴 # 0))) |
38 | 37 | impcom 124 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → ((𝐴↑𝑁) # 0 ↔ 𝐴 # 0)) |