Proof of Theorem muleqadd
Step | Hyp | Ref
| Expression |
1 | | ax-1cn 6776 |
. . . . 5
⊢ 1 ∈ ℂ |
2 | | mulsub 7194 |
. . . . . 6
⊢
(((A ∈ ℂ ∧ 1
∈ ℂ) ∧
(B ∈
ℂ ∧ 1 ∈ ℂ)) → ((A − 1) · (B − 1)) = (((A · B) +
(1 · 1)) − ((A · 1) +
(B · 1)))) |
3 | 1, 2 | mpanr2 414 |
. . . . 5
⊢
(((A ∈ ℂ ∧ 1
∈ ℂ) ∧
B ∈
ℂ) → ((A − 1) ·
(B − 1)) = (((A · B) +
(1 · 1)) − ((A · 1) +
(B · 1)))) |
4 | 1, 3 | mpanl2 411 |
. . . 4
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → ((A − 1) ·
(B − 1)) = (((A · B) +
(1 · 1)) − ((A · 1) +
(B · 1)))) |
5 | 1 | mulid1i 6827 |
. . . . . . 7
⊢ (1
· 1) = 1 |
6 | 5 | oveq2i 5466 |
. . . . . 6
⊢
((A · B) + (1 · 1)) = ((A · B) +
1) |
7 | 6 | a1i 9 |
. . . . 5
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → ((A · B) + (1 · 1)) = ((A · B) +
1)) |
8 | | mulid1 6822 |
. . . . . 6
⊢ (A ∈ ℂ →
(A · 1) = A) |
9 | | mulid1 6822 |
. . . . . 6
⊢ (B ∈ ℂ →
(B · 1) = B) |
10 | 8, 9 | oveqan12d 5474 |
. . . . 5
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → ((A · 1) + (B · 1)) = (A + B)) |
11 | 7, 10 | oveq12d 5473 |
. . . 4
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → (((A · B) + (1 · 1)) − ((A · 1) + (B · 1))) = (((A · B) +
1) − (A + B))) |
12 | | mulcl 6806 |
. . . . 5
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → (A · B) ∈
ℂ) |
13 | | addcl 6804 |
. . . . 5
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → (A + B) ∈
ℂ) |
14 | | addsub 7019 |
. . . . . 6
⊢
(((A · B) ∈ ℂ ∧ 1 ∈ ℂ
∧ (A +
B) ∈
ℂ) → (((A · B) + 1) − (A + B)) =
(((A · B) − (A +
B)) + 1)) |
15 | 1, 14 | mp3an2 1219 |
. . . . 5
⊢
(((A · B) ∈ ℂ ∧ (A + B) ∈ ℂ)
→ (((A · B) + 1) − (A + B)) =
(((A · B) − (A +
B)) + 1)) |
16 | 12, 13, 15 | syl2anc 391 |
. . . 4
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → (((A · B) + 1) − (A + B)) =
(((A · B) − (A +
B)) + 1)) |
17 | 4, 11, 16 | 3eqtrd 2073 |
. . 3
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → ((A − 1) ·
(B − 1)) = (((A · B)
− (A + B)) + 1)) |
18 | 17 | eqeq1d 2045 |
. 2
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → (((A − 1) ·
(B − 1)) = 1 ↔ (((A · B)
− (A + B)) + 1) = 1)) |
19 | 1 | addid2i 6953 |
. . . 4
⊢ (0 + 1) =
1 |
20 | 19 | eqeq2i 2047 |
. . 3
⊢
((((A · B) − (A +
B)) + 1) = (0 + 1) ↔ (((A · B)
− (A + B)) + 1) = 1) |
21 | 12, 13 | subcld 7118 |
. . . 4
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → ((A · B) − (A +
B)) ∈
ℂ) |
22 | | 0cn 6817 |
. . . . 5
⊢ 0 ∈ ℂ |
23 | | addcan2 6989 |
. . . . 5
⊢
((((A · B) − (A +
B)) ∈
ℂ ∧ 0 ∈ ℂ ∧ 1
∈ ℂ) → ((((A · B)
− (A + B)) + 1) = (0 + 1) ↔ ((A · B)
− (A + B)) = 0)) |
24 | 22, 1, 23 | mp3an23 1223 |
. . . 4
⊢
(((A · B) − (A +
B)) ∈
ℂ → ((((A · B) − (A +
B)) + 1) = (0 + 1) ↔ ((A · B)
− (A + B)) = 0)) |
25 | 21, 24 | syl 14 |
. . 3
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → ((((A · B) − (A +
B)) + 1) = (0 + 1) ↔ ((A · B)
− (A + B)) = 0)) |
26 | 20, 25 | syl5rbbr 184 |
. 2
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → (((A · B) − (A +
B)) = 0 ↔ (((A · B)
− (A + B)) + 1) = 1)) |
27 | 12, 13 | subeq0ad 7128 |
. 2
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → (((A · B) − (A +
B)) = 0 ↔ (A · B) =
(A + B))) |
28 | 18, 26, 27 | 3bitr2rd 206 |
1
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → ((A · B) = (A +
B) ↔ ((A − 1) · (B − 1)) = 1)) |