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 PP0QQ01P+1Q=1P1Q1=1

Proof

Step Hyp Ref Expression
1 simpll PP0QQ0P
2 simprl PP0QQ0Q
3 reccl PP01P
4 3 adantr PP0QQ01P
5 1 2 4 mul32d PP0QQ0PQ1P=P1PQ
6 recid PP0P1P=1
7 6 oveq1d PP0P1PQ=1Q
8 7 adantr PP0QQ0P1PQ=1Q
9 mulid2 Q1Q=Q
10 9 ad2antrl PP0QQ01Q=Q
11 5 8 10 3eqtrd PP0QQ0PQ1P=Q
12 reccl QQ01Q
13 12 adantl PP0QQ01Q
14 1 2 13 mulassd PP0QQ0PQ1Q=PQ1Q
15 recid QQ0Q1Q=1
16 15 oveq2d QQ0PQ1Q=P1
17 16 adantl PP0QQ0PQ1Q=P1
18 mulid1 PP1=P
19 18 ad2antrr PP0QQ0P1=P
20 14 17 19 3eqtrd PP0QQ0PQ1Q=P
21 11 20 oveq12d PP0QQ0PQ1P+PQ1Q=Q+P
22 mulcl PQPQ
23 22 ad2ant2r PP0QQ0PQ
24 23 4 13 adddid PP0QQ0PQ1P+1Q=PQ1P+PQ1Q
25 addcom PQP+Q=Q+P
26 25 ad2ant2r PP0QQ0P+Q=Q+P
27 21 24 26 3eqtr4d PP0QQ0PQ1P+1Q=P+Q
28 22 mulid1d PQPQ1=PQ
29 28 ad2ant2r PP0QQ0PQ1=PQ
30 27 29 eqeq12d PP0QQ0PQ1P+1Q=PQ1P+Q=PQ
31 addcl 1P1Q1P+1Q
32 3 12 31 syl2an PP0QQ01P+1Q
33 mulne0 PP0QQ0PQ0
34 ax-1cn 1
35 mulcan 1P+1Q1PQPQ0PQ1P+1Q=PQ11P+1Q=1
36 34 35 mp3an2 1P+1QPQPQ0PQ1P+1Q=PQ11P+1Q=1
37 32 23 33 36 syl12anc PP0QQ0PQ1P+1Q=PQ11P+1Q=1
38 eqcom P+Q=PQPQ=P+Q
39 muleqadd PQPQ=P+QP1Q1=1
40 38 39 syl5bb PQP+Q=PQP1Q1=1
41 40 ad2ant2r PP0QQ0P+Q=PQP1Q1=1
42 30 37 41 3bitr3d PP0QQ01P+1Q=1P1Q1=1