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

Theorem receu 9293
 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
StepHypRef Expression
1 recex 9280 . . . 4
3 simprl 735 . . . . . . . 8
4 simpll 733 . . . . . . . 8
53, 4mulcld 8735 . . . . . . 7
6 oveq1 5717 . . . . . . . . 9
76ad2antll 712 . . . . . . . 8
8 simplr 734 . . . . . . . . 9
98, 3, 4mulassd 8738 . . . . . . . 8
104mulid2d 8733 . . . . . . . 8
117, 9, 103eqtr3d 2293 . . . . . . 7
12 oveq2 5718 . . . . . . . . 9
1312eqeq1d 2261 . . . . . . . 8
1413rcla4ev 2821 . . . . . . 7
155, 11, 14syl2anc 645 . . . . . 6
1615exp32 591 . . . . 5
1716rexlimdv 2628 . . . 4
192, 18mpd 16 . 2
20 eqtr3 2272 . . . . . . 7
21 mulcan 9285 . . . . . . 7
2220, 21syl5ib 212 . . . . . 6
23223expa 1156 . . . . 5
2423expcom 426 . . . 4