Proof of Theorem muleqadd
| Step | Hyp | Ref
| Expression |
| 1 | | ax-1cn 11213 |
. . . . 5
⊢ 1 ∈
ℂ |
| 2 | | mulsub 11706 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 1 ∈
ℂ) ∧ (𝐵 ∈
ℂ ∧ 1 ∈ ℂ)) → ((𝐴 − 1) · (𝐵 − 1)) = (((𝐴 · 𝐵) + (1 · 1)) − ((𝐴 · 1) + (𝐵 · 1)))) |
| 3 | 1, 2 | mpanr2 704 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 1 ∈
ℂ) ∧ 𝐵 ∈
ℂ) → ((𝐴 −
1) · (𝐵 − 1))
= (((𝐴 · 𝐵) + (1 · 1)) −
((𝐴 · 1) + (𝐵 · 1)))) |
| 4 | 1, 3 | mpanl2 701 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 1) · (𝐵 − 1)) = (((𝐴 · 𝐵) + (1 · 1)) − ((𝐴 · 1) + (𝐵 · 1)))) |
| 5 | 1 | mulridi 11265 |
. . . . . . 7
⊢ (1
· 1) = 1 |
| 6 | 5 | oveq2i 7442 |
. . . . . 6
⊢ ((𝐴 · 𝐵) + (1 · 1)) = ((𝐴 · 𝐵) + 1) |
| 7 | 6 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 · 𝐵) + (1 · 1)) = ((𝐴 · 𝐵) + 1)) |
| 8 | | mulrid 11259 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴) |
| 9 | | mulrid 11259 |
. . . . . 6
⊢ (𝐵 ∈ ℂ → (𝐵 · 1) = 𝐵) |
| 10 | 8, 9 | oveqan12d 7450 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 · 1) + (𝐵 · 1)) = (𝐴 + 𝐵)) |
| 11 | 7, 10 | oveq12d 7449 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 · 𝐵) + (1 · 1)) − ((𝐴 · 1) + (𝐵 · 1))) = (((𝐴 · 𝐵) + 1) − (𝐴 + 𝐵))) |
| 12 | | mulcl 11239 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ) |
| 13 | | addcl 11237 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) |
| 14 | | addsub 11519 |
. . . . . 6
⊢ (((𝐴 · 𝐵) ∈ ℂ ∧ 1 ∈ ℂ
∧ (𝐴 + 𝐵) ∈ ℂ) →
(((𝐴 · 𝐵) + 1) − (𝐴 + 𝐵)) = (((𝐴 · 𝐵) − (𝐴 + 𝐵)) + 1)) |
| 15 | 1, 14 | mp3an2 1451 |
. . . . 5
⊢ (((𝐴 · 𝐵) ∈ ℂ ∧ (𝐴 + 𝐵) ∈ ℂ) → (((𝐴 · 𝐵) + 1) − (𝐴 + 𝐵)) = (((𝐴 · 𝐵) − (𝐴 + 𝐵)) + 1)) |
| 16 | 12, 13, 15 | syl2anc 584 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 · 𝐵) + 1) − (𝐴 + 𝐵)) = (((𝐴 · 𝐵) − (𝐴 + 𝐵)) + 1)) |
| 17 | 4, 11, 16 | 3eqtrd 2781 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 1) · (𝐵 − 1)) = (((𝐴 · 𝐵) − (𝐴 + 𝐵)) + 1)) |
| 18 | 17 | eqeq1d 2739 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 − 1) · (𝐵 − 1)) = 1 ↔ (((𝐴 · 𝐵) − (𝐴 + 𝐵)) + 1) = 1)) |
| 19 | 12, 13 | subcld 11620 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 · 𝐵) − (𝐴 + 𝐵)) ∈ ℂ) |
| 20 | | 0cn 11253 |
. . . . 5
⊢ 0 ∈
ℂ |
| 21 | | addcan2 11446 |
. . . . 5
⊢ ((((𝐴 · 𝐵) − (𝐴 + 𝐵)) ∈ ℂ ∧ 0 ∈ ℂ
∧ 1 ∈ ℂ) → ((((𝐴 · 𝐵) − (𝐴 + 𝐵)) + 1) = (0 + 1) ↔ ((𝐴 · 𝐵) − (𝐴 + 𝐵)) = 0)) |
| 22 | 20, 1, 21 | mp3an23 1455 |
. . . 4
⊢ (((𝐴 · 𝐵) − (𝐴 + 𝐵)) ∈ ℂ → ((((𝐴 · 𝐵) − (𝐴 + 𝐵)) + 1) = (0 + 1) ↔ ((𝐴 · 𝐵) − (𝐴 + 𝐵)) = 0)) |
| 23 | 19, 22 | syl 17 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((((𝐴 · 𝐵) − (𝐴 + 𝐵)) + 1) = (0 + 1) ↔ ((𝐴 · 𝐵) − (𝐴 + 𝐵)) = 0)) |
| 24 | 1 | addlidi 11449 |
. . . 4
⊢ (0 + 1) =
1 |
| 25 | 24 | eqeq2i 2750 |
. . 3
⊢ ((((𝐴 · 𝐵) − (𝐴 + 𝐵)) + 1) = (0 + 1) ↔ (((𝐴 · 𝐵) − (𝐴 + 𝐵)) + 1) = 1) |
| 26 | 23, 25 | bitr3di 286 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 · 𝐵) − (𝐴 + 𝐵)) = 0 ↔ (((𝐴 · 𝐵) − (𝐴 + 𝐵)) + 1) = 1)) |
| 27 | 12, 13 | subeq0ad 11630 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 · 𝐵) − (𝐴 + 𝐵)) = 0 ↔ (𝐴 · 𝐵) = (𝐴 + 𝐵))) |
| 28 | 18, 26, 27 | 3bitr2rd 308 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 · 𝐵) = (𝐴 + 𝐵) ↔ ((𝐴 − 1) · (𝐵 − 1)) = 1)) |