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 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 · 𝐵 ) = ( 𝐴 + 𝐵 ) ↔ ( ( 𝐴 − 1 ) · ( 𝐵 − 1 ) ) = 1 ) )

Proof

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