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	mulridi	⊢ ( 1 · 1 ) = 1
6	5	oveq2i	⊢ ( ( 𝐴 · 𝐵 ) + ( 1 · 1 ) ) = ( ( 𝐴 · 𝐵 ) + 1 )
7	6	a1i	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 · 𝐵 ) + ( 1 · 1 ) ) = ( ( 𝐴 · 𝐵 ) + 1 ) )
8		mulrid	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 · 1 ) = 𝐴 )
9		mulrid	⊢ ( 𝐵 ∈ ℂ → ( 𝐵 · 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	addlidi	⊢ ( 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 ) )