Proof of Theorem zmulcomlem
| Step | Hyp | Ref
| Expression |
| 1 | | elnn0 12528 |
. 2
⊢ (𝐵 ∈ ℕ0
↔ (𝐵 ∈ ℕ
∨ 𝐵 =
0)) |
| 2 | | renegneg 42441 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → (0
−ℝ (0 −ℝ 𝐴)) = 𝐴) |
| 3 | 2 | oveq1d 7446 |
. . . . 5
⊢ (𝐴 ∈ ℝ → ((0
−ℝ (0 −ℝ 𝐴)) · 𝐵) = (𝐴 · 𝐵)) |
| 4 | 3 | ad2antrr 726 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ 𝐵 ∈ ℕ) → ((0
−ℝ (0 −ℝ 𝐴)) · 𝐵) = (𝐴 · 𝐵)) |
| 5 | | rernegcl 42401 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → (0
−ℝ 𝐴) ∈ ℝ) |
| 6 | 5 | ad2antrr 726 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ 𝐵 ∈ ℕ) → (0
−ℝ 𝐴) ∈ ℝ) |
| 7 | | simpr 484 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ 𝐵 ∈ ℕ) → 𝐵 ∈ ℕ) |
| 8 | 6, 7 | renegmulnnass 42483 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ 𝐵 ∈ ℕ) → ((0
−ℝ (0 −ℝ 𝐴)) · 𝐵) = (0 −ℝ ((0
−ℝ 𝐴) · 𝐵))) |
| 9 | | nnmulcom 42307 |
. . . . . . . 8
⊢ (((0
−ℝ 𝐴) ∈ ℕ ∧ 𝐵 ∈ ℕ) → ((0
−ℝ 𝐴) · 𝐵) = (𝐵 · (0 −ℝ 𝐴))) |
| 10 | 9 | adantll 714 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ 𝐵 ∈ ℕ) → ((0
−ℝ 𝐴) · 𝐵) = (𝐵 · (0 −ℝ 𝐴))) |
| 11 | 10 | oveq2d 7447 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ 𝐵 ∈ ℕ) → (0
−ℝ ((0 −ℝ 𝐴) · 𝐵)) = (0 −ℝ (𝐵 · (0
−ℝ 𝐴)))) |
| 12 | | nnre 12273 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℝ) |
| 13 | 12 | adantl 481 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ 𝐵 ∈ ℕ) → 𝐵 ∈ ℝ) |
| 14 | | 0red 11264 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ 𝐵 ∈ ℕ) → 0 ∈
ℝ) |
| 15 | | resubdi 42426 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℝ ∧ 0 ∈
ℝ ∧ (0 −ℝ 𝐴) ∈ ℝ) → (𝐵 · (0 −ℝ (0
−ℝ 𝐴))) = ((𝐵 · 0) −ℝ
(𝐵 · (0
−ℝ 𝐴)))) |
| 16 | 13, 14, 6, 15 | syl3anc 1373 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ 𝐵 ∈ ℕ) → (𝐵 · (0 −ℝ (0
−ℝ 𝐴))) = ((𝐵 · 0) −ℝ
(𝐵 · (0
−ℝ 𝐴)))) |
| 17 | | remul01 42437 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ℝ → (𝐵 · 0) =
0) |
| 18 | 12, 17 | syl 17 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℕ → (𝐵 · 0) =
0) |
| 19 | 18 | adantl 481 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ 𝐵 ∈ ℕ) → (𝐵 · 0) = 0) |
| 20 | 19 | oveq1d 7446 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ 𝐵 ∈ ℕ) → ((𝐵 · 0) −ℝ
(𝐵 · (0
−ℝ 𝐴))) = (0 −ℝ (𝐵 · (0
−ℝ 𝐴)))) |
| 21 | 16, 20 | eqtrd 2777 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ 𝐵 ∈ ℕ) → (𝐵 · (0 −ℝ (0
−ℝ 𝐴))) = (0 −ℝ (𝐵 · (0
−ℝ 𝐴)))) |
| 22 | 2 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ 𝐵 ∈ ℕ) → (0
−ℝ (0 −ℝ 𝐴)) = 𝐴) |
| 23 | 22 | oveq2d 7447 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ 𝐵 ∈ ℕ) → (𝐵 · (0 −ℝ (0
−ℝ 𝐴))) = (𝐵 · 𝐴)) |
| 24 | 11, 21, 23 | 3eqtr2d 2783 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ 𝐵 ∈ ℕ) → (0
−ℝ ((0 −ℝ 𝐴) · 𝐵)) = (𝐵 · 𝐴)) |
| 25 | 8, 4, 24 | 3eqtr3d 2785 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ 𝐵 ∈ ℕ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) |
| 26 | 4, 4, 25 | 3eqtr3d 2785 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ 𝐵 ∈ ℕ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) |
| 27 | | remul01 42437 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → (𝐴 · 0) =
0) |
| 28 | | remul02 42435 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → (0
· 𝐴) =
0) |
| 29 | 27, 28 | eqtr4d 2780 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → (𝐴 · 0) = (0 · 𝐴)) |
| 30 | 29 | adantr 480 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) → (𝐴 · 0) = (0 · 𝐴)) |
| 31 | | oveq2 7439 |
. . . . . 6
⊢ (𝐵 = 0 → (𝐴 · 𝐵) = (𝐴 · 0)) |
| 32 | | oveq1 7438 |
. . . . . 6
⊢ (𝐵 = 0 → (𝐵 · 𝐴) = (0 · 𝐴)) |
| 33 | 31, 32 | eqeq12d 2753 |
. . . . 5
⊢ (𝐵 = 0 → ((𝐴 · 𝐵) = (𝐵 · 𝐴) ↔ (𝐴 · 0) = (0 · 𝐴))) |
| 34 | 30, 33 | syl5ibrcom 247 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) → (𝐵 = 0 → (𝐴 · 𝐵) = (𝐵 · 𝐴))) |
| 35 | 34 | imp 406 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ 𝐵 = 0) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) |
| 36 | 26, 35 | jaodan 960 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ (𝐵 ∈ ℕ ∨ 𝐵 = 0)) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) |
| 37 | 1, 36 | sylan2b 594 |
1
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ 𝐵 ∈ ℕ0) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) |