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 e. CC /\ B e. CC ) -> ( ( A x. B ) = ( A + B ) <-> ( ( A - 1 ) x. ( B - 1 ) ) = 1 ) )

Proof

Step Hyp Ref Expression
1 ax-1cn 
 |-  1 e. CC
2 mulsub 
 |-  ( ( ( A e. CC /\ 1 e. CC ) /\ ( B e. CC /\ 1 e. CC ) ) -> ( ( A - 1 ) x. ( B - 1 ) ) = ( ( ( A x. B ) + ( 1 x. 1 ) ) - ( ( A x. 1 ) + ( B x. 1 ) ) ) )
3 1 2 mpanr2 
 |-  ( ( ( A e. CC /\ 1 e. CC ) /\ B e. CC ) -> ( ( A - 1 ) x. ( B - 1 ) ) = ( ( ( A x. B ) + ( 1 x. 1 ) ) - ( ( A x. 1 ) + ( B x. 1 ) ) ) )
4 1 3 mpanl2 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A - 1 ) x. ( B - 1 ) ) = ( ( ( A x. B ) + ( 1 x. 1 ) ) - ( ( A x. 1 ) + ( B x. 1 ) ) ) )
5 1 mulid1i 
 |-  ( 1 x. 1 ) = 1
6 5 oveq2i 
 |-  ( ( A x. B ) + ( 1 x. 1 ) ) = ( ( A x. B ) + 1 )
7 6 a1i 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A x. B ) + ( 1 x. 1 ) ) = ( ( A x. B ) + 1 ) )
8 mulid1 
 |-  ( A e. CC -> ( A x. 1 ) = A )
9 mulid1 
 |-  ( B e. CC -> ( B x. 1 ) = B )
10 8 9 oveqan12d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A x. 1 ) + ( B x. 1 ) ) = ( A + B ) )
11 7 10 oveq12d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( A x. B ) + ( 1 x. 1 ) ) - ( ( A x. 1 ) + ( B x. 1 ) ) ) = ( ( ( A x. B ) + 1 ) - ( A + B ) ) )
12 mulcl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )
13 addcl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
14 addsub 
 |-  ( ( ( A x. B ) e. CC /\ 1 e. CC /\ ( A + B ) e. CC ) -> ( ( ( A x. B ) + 1 ) - ( A + B ) ) = ( ( ( A x. B ) - ( A + B ) ) + 1 ) )
15 1 14 mp3an2 
 |-  ( ( ( A x. B ) e. CC /\ ( A + B ) e. CC ) -> ( ( ( A x. B ) + 1 ) - ( A + B ) ) = ( ( ( A x. B ) - ( A + B ) ) + 1 ) )
16 12 13 15 syl2anc 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( A x. B ) + 1 ) - ( A + B ) ) = ( ( ( A x. B ) - ( A + B ) ) + 1 ) )
17 4 11 16 3eqtrd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A - 1 ) x. ( B - 1 ) ) = ( ( ( A x. B ) - ( A + B ) ) + 1 ) )
18 17 eqeq1d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( A - 1 ) x. ( B - 1 ) ) = 1 <-> ( ( ( A x. B ) - ( A + B ) ) + 1 ) = 1 ) )
19 12 13 subcld 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A x. B ) - ( A + B ) ) e. CC )
20 0cn 
 |-  0 e. CC
21 addcan2 
 |-  ( ( ( ( A x. B ) - ( A + B ) ) e. CC /\ 0 e. CC /\ 1 e. CC ) -> ( ( ( ( A x. B ) - ( A + B ) ) + 1 ) = ( 0 + 1 ) <-> ( ( A x. B ) - ( A + B ) ) = 0 ) )
22 20 1 21 mp3an23 
 |-  ( ( ( A x. B ) - ( A + B ) ) e. CC -> ( ( ( ( A x. B ) - ( A + B ) ) + 1 ) = ( 0 + 1 ) <-> ( ( A x. B ) - ( A + B ) ) = 0 ) )
23 19 22 syl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( ( A x. B ) - ( A + B ) ) + 1 ) = ( 0 + 1 ) <-> ( ( A x. B ) - ( A + B ) ) = 0 ) )
24 1 addid2i 
 |-  ( 0 + 1 ) = 1
25 24 eqeq2i 
 |-  ( ( ( ( A x. B ) - ( A + B ) ) + 1 ) = ( 0 + 1 ) <-> ( ( ( A x. B ) - ( A + B ) ) + 1 ) = 1 )
26 23 25 bitr3di 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( A x. B ) - ( A + B ) ) = 0 <-> ( ( ( A x. B ) - ( A + B ) ) + 1 ) = 1 ) )
27 12 13 subeq0ad 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( A x. B ) - ( A + B ) ) = 0 <-> ( A x. B ) = ( A + B ) ) )
28 18 26 27 3bitr2rd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A x. B ) = ( A + B ) <-> ( ( A - 1 ) x. ( B - 1 ) ) = 1 ) )