Metamath Proof Explorer

Theorem muleqadd

Description: Property of numbers whose product equals their sum. Equation 5 of Kreyszig p. 12. (Contributed by NM, 13-Nov-2006)

Ref Expression
Assertion muleqadd ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ B = A + B ↔ A − 1 ⁢ B − 1 = 1

Proof

Step Hyp Ref Expression
1 ax-1cn ⊢ 1 ∈ ℂ
2 mulsub ⊢ A ∈ ℂ ∧ 1 ∈ ℂ ∧ B ∈ ℂ ∧ 1 ∈ ℂ → A − 1 ⁢ B − 1 = A ⁢ B + 1 ⋅ 1 - A ⋅ 1 + B ⋅ 1
3 1 2 mpanr2 ⊢ A ∈ ℂ ∧ 1 ∈ ℂ ∧ B ∈ ℂ → A − 1 ⁢ B − 1 = A ⁢ B + 1 ⋅ 1 - A ⋅ 1 + B ⋅ 1
4 1 3 mpanl2 ⊢ A ∈ ℂ ∧ B ∈ ℂ → A − 1 ⁢ B − 1 = A ⁢ B + 1 ⋅ 1 - A ⋅ 1 + B ⋅ 1
5 1 mulridi ⊢ 1 ⋅ 1 = 1
6 5 oveq2i ⊢ A ⁢ B + 1 ⋅ 1 = A ⁢ B + 1
7 6 a1i ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ B + 1 ⋅ 1 = A ⁢ B + 1
8 mulrid ⊢ A ∈ ℂ → A ⋅ 1 = A
9 mulrid ⊢ B ∈ ℂ → B ⋅ 1 = B
10 8 9 oveqan12d ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⋅ 1 + B ⋅ 1 = A + B
11 7 10 oveq12d ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ B + 1 ⋅ 1 - A ⋅ 1 + B ⋅ 1 = A ⁢ B + 1 - A + B
12 mulcl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ B ∈ ℂ
13 addcl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B ∈ ℂ
14 addsub ⊢ A ⁢ B ∈ ℂ ∧ 1 ∈ ℂ ∧ A + B ∈ ℂ → A ⁢ B + 1 - A + B = A ⁢ B - A + B + 1
15 1 14 mp3an2 ⊢ A ⁢ B ∈ ℂ ∧ A + B ∈ ℂ → A ⁢ B + 1 - A + B = A ⁢ B - A + B + 1
16 12 13 15 syl2anc ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ B + 1 - A + B = A ⁢ B - A + B + 1
17 4 11 16 3eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ → A − 1 ⁢ B − 1 = A ⁢ B - A + B + 1
18 17 eqeq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ → A − 1 ⁢ B − 1 = 1 ↔ A ⁢ B - A + B + 1 = 1
19 12 13 subcld ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ B − A + B ∈ ℂ
20 0cn ⊢ 0 ∈ ℂ
21 addcan2 ⊢ A ⁢ B − A + B ∈ ℂ ∧ 0 ∈ ℂ ∧ 1 ∈ ℂ → A ⁢ B - A + B + 1 = 0 + 1 ↔ A ⁢ B − A + B = 0
22 20 1 21 mp3an23 ⊢ A ⁢ B − A + B ∈ ℂ → A ⁢ B - A + B + 1 = 0 + 1 ↔ A ⁢ B − A + B = 0
23 19 22 syl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ B - A + B + 1 = 0 + 1 ↔ A ⁢ B − A + B = 0
24 1 addlidi ⊢ 0 + 1 = 1
25 24 eqeq2i ⊢ A ⁢ B - A + B + 1 = 0 + 1 ↔ A ⁢ B - A + B + 1 = 1
26 23 25 bitr3di ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ B − A + B = 0 ↔ A ⁢ B - A + B + 1 = 1
27 12 13 subeq0ad ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ B − A + B = 0 ↔ A ⁢ B = A + B
28 18 26 27 3bitr2rd ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ B = A + B ↔ A − 1 ⁢ B − 1 = 1