| Step | Hyp | Ref
| Expression |
| 1 | | oveq1 7438 |
. . . . 5
⊢ (𝑥 = 1 → (𝑥 · 𝐵) = (1 · 𝐵)) |
| 2 | | oveq2 7439 |
. . . . 5
⊢ (𝑥 = 1 → (𝐵 · 𝑥) = (𝐵 · 1)) |
| 3 | 1, 2 | eqeq12d 2753 |
. . . 4
⊢ (𝑥 = 1 → ((𝑥 · 𝐵) = (𝐵 · 𝑥) ↔ (1 · 𝐵) = (𝐵 · 1))) |
| 4 | 3 | imbi2d 340 |
. . 3
⊢ (𝑥 = 1 → ((𝐵 ∈ ℕ → (𝑥 · 𝐵) = (𝐵 · 𝑥)) ↔ (𝐵 ∈ ℕ → (1 · 𝐵) = (𝐵 · 1)))) |
| 5 | | oveq1 7438 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝑥 · 𝐵) = (𝑦 · 𝐵)) |
| 6 | | oveq2 7439 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝐵 · 𝑥) = (𝐵 · 𝑦)) |
| 7 | 5, 6 | eqeq12d 2753 |
. . . 4
⊢ (𝑥 = 𝑦 → ((𝑥 · 𝐵) = (𝐵 · 𝑥) ↔ (𝑦 · 𝐵) = (𝐵 · 𝑦))) |
| 8 | 7 | imbi2d 340 |
. . 3
⊢ (𝑥 = 𝑦 → ((𝐵 ∈ ℕ → (𝑥 · 𝐵) = (𝐵 · 𝑥)) ↔ (𝐵 ∈ ℕ → (𝑦 · 𝐵) = (𝐵 · 𝑦)))) |
| 9 | | oveq1 7438 |
. . . . 5
⊢ (𝑥 = (𝑦 + 1) → (𝑥 · 𝐵) = ((𝑦 + 1) · 𝐵)) |
| 10 | | oveq2 7439 |
. . . . 5
⊢ (𝑥 = (𝑦 + 1) → (𝐵 · 𝑥) = (𝐵 · (𝑦 + 1))) |
| 11 | 9, 10 | eqeq12d 2753 |
. . . 4
⊢ (𝑥 = (𝑦 + 1) → ((𝑥 · 𝐵) = (𝐵 · 𝑥) ↔ ((𝑦 + 1) · 𝐵) = (𝐵 · (𝑦 + 1)))) |
| 12 | 11 | imbi2d 340 |
. . 3
⊢ (𝑥 = (𝑦 + 1) → ((𝐵 ∈ ℕ → (𝑥 · 𝐵) = (𝐵 · 𝑥)) ↔ (𝐵 ∈ ℕ → ((𝑦 + 1) · 𝐵) = (𝐵 · (𝑦 + 1))))) |
| 13 | | oveq1 7438 |
. . . . 5
⊢ (𝑥 = 𝐴 → (𝑥 · 𝐵) = (𝐴 · 𝐵)) |
| 14 | | oveq2 7439 |
. . . . 5
⊢ (𝑥 = 𝐴 → (𝐵 · 𝑥) = (𝐵 · 𝐴)) |
| 15 | 13, 14 | eqeq12d 2753 |
. . . 4
⊢ (𝑥 = 𝐴 → ((𝑥 · 𝐵) = (𝐵 · 𝑥) ↔ (𝐴 · 𝐵) = (𝐵 · 𝐴))) |
| 16 | 15 | imbi2d 340 |
. . 3
⊢ (𝑥 = 𝐴 → ((𝐵 ∈ ℕ → (𝑥 · 𝐵) = (𝐵 · 𝑥)) ↔ (𝐵 ∈ ℕ → (𝐴 · 𝐵) = (𝐵 · 𝐴)))) |
| 17 | | nnmul1com 42306 |
. . 3
⊢ (𝐵 ∈ ℕ → (1
· 𝐵) = (𝐵 · 1)) |
| 18 | | simp3 1139 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝑦 · 𝐵) = (𝐵 · 𝑦)) → (𝑦 · 𝐵) = (𝐵 · 𝑦)) |
| 19 | 17 | 3ad2ant2 1135 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝑦 · 𝐵) = (𝐵 · 𝑦)) → (1 · 𝐵) = (𝐵 · 1)) |
| 20 | 18, 19 | oveq12d 7449 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝑦 · 𝐵) = (𝐵 · 𝑦)) → ((𝑦 · 𝐵) + (1 · 𝐵)) = ((𝐵 · 𝑦) + (𝐵 · 1))) |
| 21 | | simp1 1137 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝑦 · 𝐵) = (𝐵 · 𝑦)) → 𝑦 ∈ ℕ) |
| 22 | | 1nn 12277 |
. . . . . . . 8
⊢ 1 ∈
ℕ |
| 23 | 22 | a1i 11 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝑦 · 𝐵) = (𝐵 · 𝑦)) → 1 ∈ ℕ) |
| 24 | | simp2 1138 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝑦 · 𝐵) = (𝐵 · 𝑦)) → 𝐵 ∈ ℕ) |
| 25 | | nnadddir 42305 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ ∧ 1 ∈
ℕ ∧ 𝐵 ∈
ℕ) → ((𝑦 + 1)
· 𝐵) = ((𝑦 · 𝐵) + (1 · 𝐵))) |
| 26 | 21, 23, 24, 25 | syl3anc 1373 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝑦 · 𝐵) = (𝐵 · 𝑦)) → ((𝑦 + 1) · 𝐵) = ((𝑦 · 𝐵) + (1 · 𝐵))) |
| 27 | 24 | nncnd 12282 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝑦 · 𝐵) = (𝐵 · 𝑦)) → 𝐵 ∈ ℂ) |
| 28 | 21 | nncnd 12282 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝑦 · 𝐵) = (𝐵 · 𝑦)) → 𝑦 ∈ ℂ) |
| 29 | | 1cnd 11256 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝑦 · 𝐵) = (𝐵 · 𝑦)) → 1 ∈ ℂ) |
| 30 | 27, 28, 29 | adddid 11285 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝑦 · 𝐵) = (𝐵 · 𝑦)) → (𝐵 · (𝑦 + 1)) = ((𝐵 · 𝑦) + (𝐵 · 1))) |
| 31 | 20, 26, 30 | 3eqtr4d 2787 |
. . . . 5
⊢ ((𝑦 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝑦 · 𝐵) = (𝐵 · 𝑦)) → ((𝑦 + 1) · 𝐵) = (𝐵 · (𝑦 + 1))) |
| 32 | 31 | 3exp 1120 |
. . . 4
⊢ (𝑦 ∈ ℕ → (𝐵 ∈ ℕ → ((𝑦 · 𝐵) = (𝐵 · 𝑦) → ((𝑦 + 1) · 𝐵) = (𝐵 · (𝑦 + 1))))) |
| 33 | 32 | a2d 29 |
. . 3
⊢ (𝑦 ∈ ℕ → ((𝐵 ∈ ℕ → (𝑦 · 𝐵) = (𝐵 · 𝑦)) → (𝐵 ∈ ℕ → ((𝑦 + 1) · 𝐵) = (𝐵 · (𝑦 + 1))))) |
| 34 | 4, 8, 12, 16, 17, 33 | nnind 12284 |
. 2
⊢ (𝐴 ∈ ℕ → (𝐵 ∈ ℕ → (𝐴 · 𝐵) = (𝐵 · 𝐴))) |
| 35 | 34 | imp 406 |
1
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) |