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

Theorem receu 9413
 Description: Existential uniqueness of reciprocals. Theorem I.8 of [Apostol] p. 18. (Contributed by NM, 29-Jan-1995.) (Revised by Mario Carneiro, 17-Feb-2014.)
Assertion
Ref Expression
receu
Distinct variable groups:   ,   ,

Proof of Theorem receu
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 recex 9400 . . . 4
3 simprl 732 . . . . . . . 8
4 simpll 730 . . . . . . . 8
53, 4mulcld 8855 . . . . . . 7
6 oveq1 5865 . . . . . . . . 9
76ad2antll 709 . . . . . . . 8
8 simplr 731 . . . . . . . . 9
98, 3, 4mulassd 8858 . . . . . . . 8
104mulid2d 8853 . . . . . . . 8
117, 9, 103eqtr3d 2323 . . . . . . 7
12 oveq2 5866 . . . . . . . . 9
1312eqeq1d 2291 . . . . . . . 8
1413rspcev 2884 . . . . . . 7
155, 11, 14syl2anc 642 . . . . . 6
1615exp32 588 . . . . 5
1716rexlimdv 2666 . . . 4
192, 18mpd 14 . 2
20 eqtr3 2302 . . . . . . 7
21 mulcan 9405 . . . . . . 7
2220, 21syl5ib 210 . . . . . 6
23223expa 1151 . . . . 5
2423expcom 424 . . . 4