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

Theorem receu 9656
 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 9643 . . . 4
3 simprl 733 . . . . . . 7
4 simpll 731 . . . . . . 7
53, 4mulcld 9097 . . . . . 6
6 oveq1 6079 . . . . . . . 8
76ad2antll 710 . . . . . . 7
8 simplr 732 . . . . . . . 8
98, 3, 4mulassd 9100 . . . . . . 7
104mulid2d 9095 . . . . . . 7
117, 9, 103eqtr3d 2475 . . . . . 6
12 oveq2 6080 . . . . . . . 8
1312eqeq1d 2443 . . . . . . 7
1413rspcev 3044 . . . . . 6
155, 11, 14syl2anc 643 . . . . 5
1615rexlimdvaa 2823 . . . 4
182, 17mpd 15 . 2
19 eqtr3 2454 . . . . . . 7
20 mulcan 9648 . . . . . . 7
2119, 20syl5ib 211 . . . . . 6
22213expa 1153 . . . . 5
2322expcom 425 . . . 4