Metamath Proof Explorer

Theorem conjmul

Description: Two numbers whose reciprocals sum to 1 are called "conjugates" and satisfy this relationship. Equation 5 of Kreyszig p. 12. (Contributed by NM, 12-Nov-2006)

Ref Expression
Assertion conjmul 
|- ( ( ( P e. CC /\ P =/= 0 ) /\ ( Q e. CC /\ Q =/= 0 ) ) -> ( ( ( 1 / P ) + ( 1 / Q ) ) = 1 <-> ( ( P - 1 ) x. ( Q - 1 ) ) = 1 ) )

Proof

Step Hyp Ref Expression
1 simpll 
 |-  ( ( ( P e. CC /\ P =/= 0 ) /\ ( Q e. CC /\ Q =/= 0 ) ) -> P e. CC )
2 simprl 
 |-  ( ( ( P e. CC /\ P =/= 0 ) /\ ( Q e. CC /\ Q =/= 0 ) ) -> Q e. CC )
3 reccl 
 |-  ( ( P e. CC /\ P =/= 0 ) -> ( 1 / P ) e. CC )
4 3 adantr 
 |-  ( ( ( P e. CC /\ P =/= 0 ) /\ ( Q e. CC /\ Q =/= 0 ) ) -> ( 1 / P ) e. CC )
5 1 2 4 mul32d 
 |-  ( ( ( P e. CC /\ P =/= 0 ) /\ ( Q e. CC /\ Q =/= 0 ) ) -> ( ( P x. Q ) x. ( 1 / P ) ) = ( ( P x. ( 1 / P ) ) x. Q ) )
6 recid 
 |-  ( ( P e. CC /\ P =/= 0 ) -> ( P x. ( 1 / P ) ) = 1 )
7 6 oveq1d 
 |-  ( ( P e. CC /\ P =/= 0 ) -> ( ( P x. ( 1 / P ) ) x. Q ) = ( 1 x. Q ) )
8 7 adantr 
 |-  ( ( ( P e. CC /\ P =/= 0 ) /\ ( Q e. CC /\ Q =/= 0 ) ) -> ( ( P x. ( 1 / P ) ) x. Q ) = ( 1 x. Q ) )
9 mulid2 
 |-  ( Q e. CC -> ( 1 x. Q ) = Q )
10 9 ad2antrl 
 |-  ( ( ( P e. CC /\ P =/= 0 ) /\ ( Q e. CC /\ Q =/= 0 ) ) -> ( 1 x. Q ) = Q )
11 5 8 10 3eqtrd 
 |-  ( ( ( P e. CC /\ P =/= 0 ) /\ ( Q e. CC /\ Q =/= 0 ) ) -> ( ( P x. Q ) x. ( 1 / P ) ) = Q )
12 reccl 
 |-  ( ( Q e. CC /\ Q =/= 0 ) -> ( 1 / Q ) e. CC )
13 12 adantl 
 |-  ( ( ( P e. CC /\ P =/= 0 ) /\ ( Q e. CC /\ Q =/= 0 ) ) -> ( 1 / Q ) e. CC )
14 1 2 13 mulassd 
 |-  ( ( ( P e. CC /\ P =/= 0 ) /\ ( Q e. CC /\ Q =/= 0 ) ) -> ( ( P x. Q ) x. ( 1 / Q ) ) = ( P x. ( Q x. ( 1 / Q ) ) ) )
15 recid 
 |-  ( ( Q e. CC /\ Q =/= 0 ) -> ( Q x. ( 1 / Q ) ) = 1 )
16 15 oveq2d 
 |-  ( ( Q e. CC /\ Q =/= 0 ) -> ( P x. ( Q x. ( 1 / Q ) ) ) = ( P x. 1 ) )
17 16 adantl 
 |-  ( ( ( P e. CC /\ P =/= 0 ) /\ ( Q e. CC /\ Q =/= 0 ) ) -> ( P x. ( Q x. ( 1 / Q ) ) ) = ( P x. 1 ) )
18 mulid1 
 |-  ( P e. CC -> ( P x. 1 ) = P )
19 18 ad2antrr 
 |-  ( ( ( P e. CC /\ P =/= 0 ) /\ ( Q e. CC /\ Q =/= 0 ) ) -> ( P x. 1 ) = P )
20 14 17 19 3eqtrd 
 |-  ( ( ( P e. CC /\ P =/= 0 ) /\ ( Q e. CC /\ Q =/= 0 ) ) -> ( ( P x. Q ) x. ( 1 / Q ) ) = P )
21 11 20 oveq12d 
 |-  ( ( ( P e. CC /\ P =/= 0 ) /\ ( Q e. CC /\ Q =/= 0 ) ) -> ( ( ( P x. Q ) x. ( 1 / P ) ) + ( ( P x. Q ) x. ( 1 / Q ) ) ) = ( Q + P ) )
22 mulcl 
 |-  ( ( P e. CC /\ Q e. CC ) -> ( P x. Q ) e. CC )
23 22 ad2ant2r 
 |-  ( ( ( P e. CC /\ P =/= 0 ) /\ ( Q e. CC /\ Q =/= 0 ) ) -> ( P x. Q ) e. CC )
24 23 4 13 adddid 
 |-  ( ( ( P e. CC /\ P =/= 0 ) /\ ( Q e. CC /\ Q =/= 0 ) ) -> ( ( P x. Q ) x. ( ( 1 / P ) + ( 1 / Q ) ) ) = ( ( ( P x. Q ) x. ( 1 / P ) ) + ( ( P x. Q ) x. ( 1 / Q ) ) ) )
25 addcom 
 |-  ( ( P e. CC /\ Q e. CC ) -> ( P + Q ) = ( Q + P ) )
26 25 ad2ant2r 
 |-  ( ( ( P e. CC /\ P =/= 0 ) /\ ( Q e. CC /\ Q =/= 0 ) ) -> ( P + Q ) = ( Q + P ) )
27 21 24 26 3eqtr4d 
 |-  ( ( ( P e. CC /\ P =/= 0 ) /\ ( Q e. CC /\ Q =/= 0 ) ) -> ( ( P x. Q ) x. ( ( 1 / P ) + ( 1 / Q ) ) ) = ( P + Q ) )
28 22 mulid1d 
 |-  ( ( P e. CC /\ Q e. CC ) -> ( ( P x. Q ) x. 1 ) = ( P x. Q ) )
29 28 ad2ant2r 
 |-  ( ( ( P e. CC /\ P =/= 0 ) /\ ( Q e. CC /\ Q =/= 0 ) ) -> ( ( P x. Q ) x. 1 ) = ( P x. Q ) )
30 27 29 eqeq12d 
 |-  ( ( ( P e. CC /\ P =/= 0 ) /\ ( Q e. CC /\ Q =/= 0 ) ) -> ( ( ( P x. Q ) x. ( ( 1 / P ) + ( 1 / Q ) ) ) = ( ( P x. Q ) x. 1 ) <-> ( P + Q ) = ( P x. Q ) ) )
31 addcl 
 |-  ( ( ( 1 / P ) e. CC /\ ( 1 / Q ) e. CC ) -> ( ( 1 / P ) + ( 1 / Q ) ) e. CC )
32 3 12 31 syl2an 
 |-  ( ( ( P e. CC /\ P =/= 0 ) /\ ( Q e. CC /\ Q =/= 0 ) ) -> ( ( 1 / P ) + ( 1 / Q ) ) e. CC )
33 mulne0 
 |-  ( ( ( P e. CC /\ P =/= 0 ) /\ ( Q e. CC /\ Q =/= 0 ) ) -> ( P x. Q ) =/= 0 )
34 ax-1cn 
 |-  1 e. CC
35 mulcan 
 |-  ( ( ( ( 1 / P ) + ( 1 / Q ) ) e. CC /\ 1 e. CC /\ ( ( P x. Q ) e. CC /\ ( P x. Q ) =/= 0 ) ) -> ( ( ( P x. Q ) x. ( ( 1 / P ) + ( 1 / Q ) ) ) = ( ( P x. Q ) x. 1 ) <-> ( ( 1 / P ) + ( 1 / Q ) ) = 1 ) )
36 34 35 mp3an2 
 |-  ( ( ( ( 1 / P ) + ( 1 / Q ) ) e. CC /\ ( ( P x. Q ) e. CC /\ ( P x. Q ) =/= 0 ) ) -> ( ( ( P x. Q ) x. ( ( 1 / P ) + ( 1 / Q ) ) ) = ( ( P x. Q ) x. 1 ) <-> ( ( 1 / P ) + ( 1 / Q ) ) = 1 ) )
37 32 23 33 36 syl12anc 
 |-  ( ( ( P e. CC /\ P =/= 0 ) /\ ( Q e. CC /\ Q =/= 0 ) ) -> ( ( ( P x. Q ) x. ( ( 1 / P ) + ( 1 / Q ) ) ) = ( ( P x. Q ) x. 1 ) <-> ( ( 1 / P ) + ( 1 / Q ) ) = 1 ) )
38 eqcom 
 |-  ( ( P + Q ) = ( P x. Q ) <-> ( P x. Q ) = ( P + Q ) )
39 muleqadd 
 |-  ( ( P e. CC /\ Q e. CC ) -> ( ( P x. Q ) = ( P + Q ) <-> ( ( P - 1 ) x. ( Q - 1 ) ) = 1 ) )
40 38 39 syl5bb 
 |-  ( ( P e. CC /\ Q e. CC ) -> ( ( P + Q ) = ( P x. Q ) <-> ( ( P - 1 ) x. ( Q - 1 ) ) = 1 ) )
41 40 ad2ant2r 
 |-  ( ( ( P e. CC /\ P =/= 0 ) /\ ( Q e. CC /\ Q =/= 0 ) ) -> ( ( P + Q ) = ( P x. Q ) <-> ( ( P - 1 ) x. ( Q - 1 ) ) = 1 ) )
42 30 37 41 3bitr3d 
 |-  ( ( ( P e. CC /\ P =/= 0 ) /\ ( Q e. CC /\ Q =/= 0 ) ) -> ( ( ( 1 / P ) + ( 1 / Q ) ) = 1 <-> ( ( P - 1 ) x. ( Q - 1 ) ) = 1 ) )