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 ) )