Step | Hyp | Ref
| Expression |
1 | | oveq2 5822 |
. . . . . . 7
⊢ (𝑤 = 1 → (𝐴↑𝑤) = (𝐴↑1)) |
2 | | oveq2 5822 |
. . . . . . 7
⊢ (𝑤 = 1 → (𝐵↑𝑤) = (𝐵↑1)) |
3 | 1, 2 | breq12d 3974 |
. . . . . 6
⊢ (𝑤 = 1 → ((𝐴↑𝑤) # (𝐵↑𝑤) ↔ (𝐴↑1) # (𝐵↑1))) |
4 | 3 | imbi1d 230 |
. . . . 5
⊢ (𝑤 = 1 → (((𝐴↑𝑤) # (𝐵↑𝑤) → 𝐴 # 𝐵) ↔ ((𝐴↑1) # (𝐵↑1) → 𝐴 # 𝐵))) |
5 | 4 | imbi2d 229 |
. . . 4
⊢ (𝑤 = 1 → (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑𝑤) # (𝐵↑𝑤) → 𝐴 # 𝐵)) ↔ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑1) # (𝐵↑1) → 𝐴 # 𝐵)))) |
6 | | oveq2 5822 |
. . . . . . 7
⊢ (𝑤 = 𝑘 → (𝐴↑𝑤) = (𝐴↑𝑘)) |
7 | | oveq2 5822 |
. . . . . . 7
⊢ (𝑤 = 𝑘 → (𝐵↑𝑤) = (𝐵↑𝑘)) |
8 | 6, 7 | breq12d 3974 |
. . . . . 6
⊢ (𝑤 = 𝑘 → ((𝐴↑𝑤) # (𝐵↑𝑤) ↔ (𝐴↑𝑘) # (𝐵↑𝑘))) |
9 | 8 | imbi1d 230 |
. . . . 5
⊢ (𝑤 = 𝑘 → (((𝐴↑𝑤) # (𝐵↑𝑤) → 𝐴 # 𝐵) ↔ ((𝐴↑𝑘) # (𝐵↑𝑘) → 𝐴 # 𝐵))) |
10 | 9 | imbi2d 229 |
. . . 4
⊢ (𝑤 = 𝑘 → (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑𝑤) # (𝐵↑𝑤) → 𝐴 # 𝐵)) ↔ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑𝑘) # (𝐵↑𝑘) → 𝐴 # 𝐵)))) |
11 | | oveq2 5822 |
. . . . . . 7
⊢ (𝑤 = (𝑘 + 1) → (𝐴↑𝑤) = (𝐴↑(𝑘 + 1))) |
12 | | oveq2 5822 |
. . . . . . 7
⊢ (𝑤 = (𝑘 + 1) → (𝐵↑𝑤) = (𝐵↑(𝑘 + 1))) |
13 | 11, 12 | breq12d 3974 |
. . . . . 6
⊢ (𝑤 = (𝑘 + 1) → ((𝐴↑𝑤) # (𝐵↑𝑤) ↔ (𝐴↑(𝑘 + 1)) # (𝐵↑(𝑘 + 1)))) |
14 | 13 | imbi1d 230 |
. . . . 5
⊢ (𝑤 = (𝑘 + 1) → (((𝐴↑𝑤) # (𝐵↑𝑤) → 𝐴 # 𝐵) ↔ ((𝐴↑(𝑘 + 1)) # (𝐵↑(𝑘 + 1)) → 𝐴 # 𝐵))) |
15 | 14 | imbi2d 229 |
. . . 4
⊢ (𝑤 = (𝑘 + 1) → (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑𝑤) # (𝐵↑𝑤) → 𝐴 # 𝐵)) ↔ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑(𝑘 + 1)) # (𝐵↑(𝑘 + 1)) → 𝐴 # 𝐵)))) |
16 | | oveq2 5822 |
. . . . . . 7
⊢ (𝑤 = 𝑁 → (𝐴↑𝑤) = (𝐴↑𝑁)) |
17 | | oveq2 5822 |
. . . . . . 7
⊢ (𝑤 = 𝑁 → (𝐵↑𝑤) = (𝐵↑𝑁)) |
18 | 16, 17 | breq12d 3974 |
. . . . . 6
⊢ (𝑤 = 𝑁 → ((𝐴↑𝑤) # (𝐵↑𝑤) ↔ (𝐴↑𝑁) # (𝐵↑𝑁))) |
19 | 18 | imbi1d 230 |
. . . . 5
⊢ (𝑤 = 𝑁 → (((𝐴↑𝑤) # (𝐵↑𝑤) → 𝐴 # 𝐵) ↔ ((𝐴↑𝑁) # (𝐵↑𝑁) → 𝐴 # 𝐵))) |
20 | 19 | imbi2d 229 |
. . . 4
⊢ (𝑤 = 𝑁 → (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑𝑤) # (𝐵↑𝑤) → 𝐴 # 𝐵)) ↔ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑𝑁) # (𝐵↑𝑁) → 𝐴 # 𝐵)))) |
21 | | simpl 108 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐴 ∈
ℂ) |
22 | 21 | exp1d 10523 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴↑1) = 𝐴) |
23 | | simpr 109 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐵 ∈
ℂ) |
24 | 23 | exp1d 10523 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵↑1) = 𝐵) |
25 | 22, 24 | breq12d 3974 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑1) # (𝐵↑1) ↔ 𝐴 # 𝐵)) |
26 | 25 | biimpd 143 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑1) # (𝐵↑1) → 𝐴 # 𝐵)) |
27 | | simpr 109 |
. . . . . . . 8
⊢
(((((𝑘 ∈
ℕ ∧ (𝐴 ∈
ℂ ∧ 𝐵 ∈
ℂ)) ∧ ((𝐴↑𝑘) # (𝐵↑𝑘) → 𝐴 # 𝐵)) ∧ (𝐴↑(𝑘 + 1)) # (𝐵↑(𝑘 + 1))) ∧ (𝐴↑𝑘) # (𝐵↑𝑘)) → (𝐴↑𝑘) # (𝐵↑𝑘)) |
28 | | simpllr 524 |
. . . . . . . 8
⊢
(((((𝑘 ∈
ℕ ∧ (𝐴 ∈
ℂ ∧ 𝐵 ∈
ℂ)) ∧ ((𝐴↑𝑘) # (𝐵↑𝑘) → 𝐴 # 𝐵)) ∧ (𝐴↑(𝑘 + 1)) # (𝐵↑(𝑘 + 1))) ∧ (𝐴↑𝑘) # (𝐵↑𝑘)) → ((𝐴↑𝑘) # (𝐵↑𝑘) → 𝐴 # 𝐵)) |
29 | 27, 28 | mpd 13 |
. . . . . . 7
⊢
(((((𝑘 ∈
ℕ ∧ (𝐴 ∈
ℂ ∧ 𝐵 ∈
ℂ)) ∧ ((𝐴↑𝑘) # (𝐵↑𝑘) → 𝐴 # 𝐵)) ∧ (𝐴↑(𝑘 + 1)) # (𝐵↑(𝑘 + 1))) ∧ (𝐴↑𝑘) # (𝐵↑𝑘)) → 𝐴 # 𝐵) |
30 | | simpr 109 |
. . . . . . 7
⊢
(((((𝑘 ∈
ℕ ∧ (𝐴 ∈
ℂ ∧ 𝐵 ∈
ℂ)) ∧ ((𝐴↑𝑘) # (𝐵↑𝑘) → 𝐴 # 𝐵)) ∧ (𝐴↑(𝑘 + 1)) # (𝐵↑(𝑘 + 1))) ∧ 𝐴 # 𝐵) → 𝐴 # 𝐵) |
31 | | simpr 109 |
. . . . . . . . 9
⊢ ((((𝑘 ∈ ℕ ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ)) ∧ ((𝐴↑𝑘) # (𝐵↑𝑘) → 𝐴 # 𝐵)) ∧ (𝐴↑(𝑘 + 1)) # (𝐵↑(𝑘 + 1))) → (𝐴↑(𝑘 + 1)) # (𝐵↑(𝑘 + 1))) |
32 | 21 | ad3antlr 485 |
. . . . . . . . . 10
⊢ ((((𝑘 ∈ ℕ ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ)) ∧ ((𝐴↑𝑘) # (𝐵↑𝑘) → 𝐴 # 𝐵)) ∧ (𝐴↑(𝑘 + 1)) # (𝐵↑(𝑘 + 1))) → 𝐴 ∈ ℂ) |
33 | | nnnn0 9076 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℕ0) |
34 | 33 | ad3antrrr 484 |
. . . . . . . . . 10
⊢ ((((𝑘 ∈ ℕ ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ)) ∧ ((𝐴↑𝑘) # (𝐵↑𝑘) → 𝐴 # 𝐵)) ∧ (𝐴↑(𝑘 + 1)) # (𝐵↑(𝑘 + 1))) → 𝑘 ∈ ℕ0) |
35 | 32, 34 | expp1d 10529 |
. . . . . . . . 9
⊢ ((((𝑘 ∈ ℕ ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ)) ∧ ((𝐴↑𝑘) # (𝐵↑𝑘) → 𝐴 # 𝐵)) ∧ (𝐴↑(𝑘 + 1)) # (𝐵↑(𝑘 + 1))) → (𝐴↑(𝑘 + 1)) = ((𝐴↑𝑘) · 𝐴)) |
36 | 23 | ad3antlr 485 |
. . . . . . . . . 10
⊢ ((((𝑘 ∈ ℕ ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ)) ∧ ((𝐴↑𝑘) # (𝐵↑𝑘) → 𝐴 # 𝐵)) ∧ (𝐴↑(𝑘 + 1)) # (𝐵↑(𝑘 + 1))) → 𝐵 ∈ ℂ) |
37 | 36, 34 | expp1d 10529 |
. . . . . . . . 9
⊢ ((((𝑘 ∈ ℕ ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ)) ∧ ((𝐴↑𝑘) # (𝐵↑𝑘) → 𝐴 # 𝐵)) ∧ (𝐴↑(𝑘 + 1)) # (𝐵↑(𝑘 + 1))) → (𝐵↑(𝑘 + 1)) = ((𝐵↑𝑘) · 𝐵)) |
38 | 31, 35, 37 | 3brtr3d 3991 |
. . . . . . . 8
⊢ ((((𝑘 ∈ ℕ ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ)) ∧ ((𝐴↑𝑘) # (𝐵↑𝑘) → 𝐴 # 𝐵)) ∧ (𝐴↑(𝑘 + 1)) # (𝐵↑(𝑘 + 1))) → ((𝐴↑𝑘) · 𝐴) # ((𝐵↑𝑘) · 𝐵)) |
39 | 32, 34 | expcld 10528 |
. . . . . . . . 9
⊢ ((((𝑘 ∈ ℕ ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ)) ∧ ((𝐴↑𝑘) # (𝐵↑𝑘) → 𝐴 # 𝐵)) ∧ (𝐴↑(𝑘 + 1)) # (𝐵↑(𝑘 + 1))) → (𝐴↑𝑘) ∈ ℂ) |
40 | 36, 34 | expcld 10528 |
. . . . . . . . 9
⊢ ((((𝑘 ∈ ℕ ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ)) ∧ ((𝐴↑𝑘) # (𝐵↑𝑘) → 𝐴 # 𝐵)) ∧ (𝐴↑(𝑘 + 1)) # (𝐵↑(𝑘 + 1))) → (𝐵↑𝑘) ∈ ℂ) |
41 | | mulext 8468 |
. . . . . . . . 9
⊢ ((((𝐴↑𝑘) ∈ ℂ ∧ 𝐴 ∈ ℂ) ∧ ((𝐵↑𝑘) ∈ ℂ ∧ 𝐵 ∈ ℂ)) → (((𝐴↑𝑘) · 𝐴) # ((𝐵↑𝑘) · 𝐵) → ((𝐴↑𝑘) # (𝐵↑𝑘) ∨ 𝐴 # 𝐵))) |
42 | 39, 32, 40, 36, 41 | syl22anc 1218 |
. . . . . . . 8
⊢ ((((𝑘 ∈ ℕ ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ)) ∧ ((𝐴↑𝑘) # (𝐵↑𝑘) → 𝐴 # 𝐵)) ∧ (𝐴↑(𝑘 + 1)) # (𝐵↑(𝑘 + 1))) → (((𝐴↑𝑘) · 𝐴) # ((𝐵↑𝑘) · 𝐵) → ((𝐴↑𝑘) # (𝐵↑𝑘) ∨ 𝐴 # 𝐵))) |
43 | 38, 42 | mpd 13 |
. . . . . . 7
⊢ ((((𝑘 ∈ ℕ ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ)) ∧ ((𝐴↑𝑘) # (𝐵↑𝑘) → 𝐴 # 𝐵)) ∧ (𝐴↑(𝑘 + 1)) # (𝐵↑(𝑘 + 1))) → ((𝐴↑𝑘) # (𝐵↑𝑘) ∨ 𝐴 # 𝐵)) |
44 | 29, 30, 43 | mpjaodan 788 |
. . . . . 6
⊢ ((((𝑘 ∈ ℕ ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ)) ∧ ((𝐴↑𝑘) # (𝐵↑𝑘) → 𝐴 # 𝐵)) ∧ (𝐴↑(𝑘 + 1)) # (𝐵↑(𝑘 + 1))) → 𝐴 # 𝐵) |
45 | 44 | exp41 368 |
. . . . 5
⊢ (𝑘 ∈ ℕ → ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴↑𝑘) # (𝐵↑𝑘) → 𝐴 # 𝐵) → ((𝐴↑(𝑘 + 1)) # (𝐵↑(𝑘 + 1)) → 𝐴 # 𝐵)))) |
46 | 45 | a2d 26 |
. . . 4
⊢ (𝑘 ∈ ℕ → (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑𝑘) # (𝐵↑𝑘) → 𝐴 # 𝐵)) → ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑(𝑘 + 1)) # (𝐵↑(𝑘 + 1)) → 𝐴 # 𝐵)))) |
47 | 5, 10, 15, 20, 26, 46 | nnind 8828 |
. . 3
⊢ (𝑁 ∈ ℕ → ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑𝑁) # (𝐵↑𝑁) → 𝐴 # 𝐵))) |
48 | 47 | impcom 124 |
. 2
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑁 ∈ ℕ) → ((𝐴↑𝑁) # (𝐵↑𝑁) → 𝐴 # 𝐵)) |
49 | 48 | 3impa 1177 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ) → ((𝐴↑𝑁) # (𝐵↑𝑁) → 𝐴 # 𝐵)) |