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