Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  conjmul Structured version   Unicode version

Theorem conjmul 10302
 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.)
Assertion
Ref Expression
conjmul

Proof of Theorem conjmul
StepHypRef Expression
1 simpll 752 . . . . . . 7
2 simprl 756 . . . . . . 7
3 reccl 10255 . . . . . . . 8
43adantr 463 . . . . . . 7
51, 2, 4mul32d 9824 . . . . . 6
6 recid 10262 . . . . . . . 8
76oveq1d 6293 . . . . . . 7
87adantr 463 . . . . . 6
9 mulid2 9624 . . . . . . 7
109ad2antrl 726 . . . . . 6
115, 8, 103eqtrd 2447 . . . . 5
12 reccl 10255 . . . . . . . 8
1312adantl 464 . . . . . . 7
141, 2, 13mulassd 9649 . . . . . 6
15 recid 10262 . . . . . . . 8
1615oveq2d 6294 . . . . . . 7
1716adantl 464 . . . . . 6
18 mulid1 9623 . . . . . . 7
1918ad2antrr 724 . . . . . 6
2014, 17, 193eqtrd 2447 . . . . 5
2111, 20oveq12d 6296 . . . 4
22 mulcl 9606 . . . . . 6
2322ad2ant2r 745 . . . . 5
2423, 4, 13adddid 9650 . . . 4
25 addcom 9800 . . . . 5
2625ad2ant2r 745 . . . 4
2721, 24, 263eqtr4d 2453 . . 3
2822mulid1d 9643 . . . 4
3027, 29eqeq12d 2424 . 2
31 addcl 9604 . . . 4
323, 12, 31syl2an 475 . . 3
33 mulne0 10232 . . 3
34 ax-1cn 9580 . . . 4
35 mulcan 10227 . . . 4
3634, 35mp3an2 1314 . . 3
3732, 23, 33, 36syl12anc 1228 . 2
38 eqcom 2411 . . . 4
39 muleqadd 10234 . . . 4
4038, 39syl5bb 257 . . 3