Metamath Proof Explorer


Theorem receu

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)

Ref Expression
Assertion receu ABB0∃!xBx=A

Proof

Step Hyp Ref Expression
1 recex BB0yBy=1
2 1 3adant1 ABB0yBy=1
3 simprl AByBy=1y
4 simpll AByBy=1A
5 3 4 mulcld AByBy=1yA
6 oveq1 By=1ByA=1A
7 6 ad2antll AByBy=1ByA=1A
8 simplr AByBy=1B
9 8 3 4 mulassd AByBy=1ByA=ByA
10 4 mulid2d AByBy=11A=A
11 7 9 10 3eqtr3d AByBy=1ByA=A
12 oveq2 x=yABx=ByA
13 12 eqeq1d x=yABx=AByA=A
14 13 rspcev yAByA=AxBx=A
15 5 11 14 syl2anc AByBy=1xBx=A
16 15 rexlimdvaa AByBy=1xBx=A
17 16 3adant3 ABB0yBy=1xBx=A
18 2 17 mpd ABB0xBx=A
19 eqtr3 Bx=ABy=ABx=By
20 mulcan xyBB0Bx=Byx=y
21 19 20 syl5ib xyBB0Bx=ABy=Ax=y
22 21 3expa xyBB0Bx=ABy=Ax=y
23 22 expcom BB0xyBx=ABy=Ax=y
24 23 3adant1 ABB0xyBx=ABy=Ax=y
25 24 ralrimivv ABB0xyBx=ABy=Ax=y
26 oveq2 x=yBx=By
27 26 eqeq1d x=yBx=ABy=A
28 27 reu4 ∃!xBx=AxBx=AxyBx=ABy=Ax=y
29 18 25 28 sylanbrc ABB0∃!xBx=A