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 ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ต โ‰  0 ) โ†’ โˆƒ! ๐‘ฅ โˆˆ โ„‚ ( ๐ต ยท ๐‘ฅ ) = ๐ด )

Proof

Step Hyp Ref Expression
1 recex โŠข ( ( ๐ต โˆˆ โ„‚ โˆง ๐ต โ‰  0 ) โ†’ โˆƒ ๐‘ฆ โˆˆ โ„‚ ( ๐ต ยท ๐‘ฆ ) = 1 )
2 1 3adant1 โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ต โ‰  0 ) โ†’ โˆƒ ๐‘ฆ โˆˆ โ„‚ ( ๐ต ยท ๐‘ฆ ) = 1 )
3 simprl โŠข ( ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ ) โˆง ( ๐‘ฆ โˆˆ โ„‚ โˆง ( ๐ต ยท ๐‘ฆ ) = 1 ) ) โ†’ ๐‘ฆ โˆˆ โ„‚ )
4 simpll โŠข ( ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ ) โˆง ( ๐‘ฆ โˆˆ โ„‚ โˆง ( ๐ต ยท ๐‘ฆ ) = 1 ) ) โ†’ ๐ด โˆˆ โ„‚ )
5 3 4 mulcld โŠข ( ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ ) โˆง ( ๐‘ฆ โˆˆ โ„‚ โˆง ( ๐ต ยท ๐‘ฆ ) = 1 ) ) โ†’ ( ๐‘ฆ ยท ๐ด ) โˆˆ โ„‚ )
6 oveq1 โŠข ( ( ๐ต ยท ๐‘ฆ ) = 1 โ†’ ( ( ๐ต ยท ๐‘ฆ ) ยท ๐ด ) = ( 1 ยท ๐ด ) )
7 6 ad2antll โŠข ( ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ ) โˆง ( ๐‘ฆ โˆˆ โ„‚ โˆง ( ๐ต ยท ๐‘ฆ ) = 1 ) ) โ†’ ( ( ๐ต ยท ๐‘ฆ ) ยท ๐ด ) = ( 1 ยท ๐ด ) )
8 simplr โŠข ( ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ ) โˆง ( ๐‘ฆ โˆˆ โ„‚ โˆง ( ๐ต ยท ๐‘ฆ ) = 1 ) ) โ†’ ๐ต โˆˆ โ„‚ )
9 8 3 4 mulassd โŠข ( ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ ) โˆง ( ๐‘ฆ โˆˆ โ„‚ โˆง ( ๐ต ยท ๐‘ฆ ) = 1 ) ) โ†’ ( ( ๐ต ยท ๐‘ฆ ) ยท ๐ด ) = ( ๐ต ยท ( ๐‘ฆ ยท ๐ด ) ) )
10 4 mulid2d โŠข ( ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ ) โˆง ( ๐‘ฆ โˆˆ โ„‚ โˆง ( ๐ต ยท ๐‘ฆ ) = 1 ) ) โ†’ ( 1 ยท ๐ด ) = ๐ด )
11 7 9 10 3eqtr3d โŠข ( ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ ) โˆง ( ๐‘ฆ โˆˆ โ„‚ โˆง ( ๐ต ยท ๐‘ฆ ) = 1 ) ) โ†’ ( ๐ต ยท ( ๐‘ฆ ยท ๐ด ) ) = ๐ด )
12 oveq2 โŠข ( ๐‘ฅ = ( ๐‘ฆ ยท ๐ด ) โ†’ ( ๐ต ยท ๐‘ฅ ) = ( ๐ต ยท ( ๐‘ฆ ยท ๐ด ) ) )
13 12 eqeq1d โŠข ( ๐‘ฅ = ( ๐‘ฆ ยท ๐ด ) โ†’ ( ( ๐ต ยท ๐‘ฅ ) = ๐ด โ†” ( ๐ต ยท ( ๐‘ฆ ยท ๐ด ) ) = ๐ด ) )
14 13 rspcev โŠข ( ( ( ๐‘ฆ ยท ๐ด ) โˆˆ โ„‚ โˆง ( ๐ต ยท ( ๐‘ฆ ยท ๐ด ) ) = ๐ด ) โ†’ โˆƒ ๐‘ฅ โˆˆ โ„‚ ( ๐ต ยท ๐‘ฅ ) = ๐ด )
15 5 11 14 syl2anc โŠข ( ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ ) โˆง ( ๐‘ฆ โˆˆ โ„‚ โˆง ( ๐ต ยท ๐‘ฆ ) = 1 ) ) โ†’ โˆƒ ๐‘ฅ โˆˆ โ„‚ ( ๐ต ยท ๐‘ฅ ) = ๐ด )
16 15 rexlimdvaa โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ ) โ†’ ( โˆƒ ๐‘ฆ โˆˆ โ„‚ ( ๐ต ยท ๐‘ฆ ) = 1 โ†’ โˆƒ ๐‘ฅ โˆˆ โ„‚ ( ๐ต ยท ๐‘ฅ ) = ๐ด ) )
17 16 3adant3 โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ต โ‰  0 ) โ†’ ( โˆƒ ๐‘ฆ โˆˆ โ„‚ ( ๐ต ยท ๐‘ฆ ) = 1 โ†’ โˆƒ ๐‘ฅ โˆˆ โ„‚ ( ๐ต ยท ๐‘ฅ ) = ๐ด ) )
18 2 17 mpd โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ต โ‰  0 ) โ†’ โˆƒ ๐‘ฅ โˆˆ โ„‚ ( ๐ต ยท ๐‘ฅ ) = ๐ด )
19 eqtr3 โŠข ( ( ( ๐ต ยท ๐‘ฅ ) = ๐ด โˆง ( ๐ต ยท ๐‘ฆ ) = ๐ด ) โ†’ ( ๐ต ยท ๐‘ฅ ) = ( ๐ต ยท ๐‘ฆ ) )
20 mulcan โŠข ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚ โˆง ( ๐ต โˆˆ โ„‚ โˆง ๐ต โ‰  0 ) ) โ†’ ( ( ๐ต ยท ๐‘ฅ ) = ( ๐ต ยท ๐‘ฆ ) โ†” ๐‘ฅ = ๐‘ฆ ) )
21 19 20 syl5ib โŠข ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚ โˆง ( ๐ต โˆˆ โ„‚ โˆง ๐ต โ‰  0 ) ) โ†’ ( ( ( ๐ต ยท ๐‘ฅ ) = ๐ด โˆง ( ๐ต ยท ๐‘ฆ ) = ๐ด ) โ†’ ๐‘ฅ = ๐‘ฆ ) )
22 21 3expa โŠข ( ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚ ) โˆง ( ๐ต โˆˆ โ„‚ โˆง ๐ต โ‰  0 ) ) โ†’ ( ( ( ๐ต ยท ๐‘ฅ ) = ๐ด โˆง ( ๐ต ยท ๐‘ฆ ) = ๐ด ) โ†’ ๐‘ฅ = ๐‘ฆ ) )
23 22 expcom โŠข ( ( ๐ต โˆˆ โ„‚ โˆง ๐ต โ‰  0 ) โ†’ ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚ ) โ†’ ( ( ( ๐ต ยท ๐‘ฅ ) = ๐ด โˆง ( ๐ต ยท ๐‘ฆ ) = ๐ด ) โ†’ ๐‘ฅ = ๐‘ฆ ) ) )
24 23 3adant1 โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ต โ‰  0 ) โ†’ ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚ ) โ†’ ( ( ( ๐ต ยท ๐‘ฅ ) = ๐ด โˆง ( ๐ต ยท ๐‘ฆ ) = ๐ด ) โ†’ ๐‘ฅ = ๐‘ฆ ) ) )
25 24 ralrimivv โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ต โ‰  0 ) โ†’ โˆ€ ๐‘ฅ โˆˆ โ„‚ โˆ€ ๐‘ฆ โˆˆ โ„‚ ( ( ( ๐ต ยท ๐‘ฅ ) = ๐ด โˆง ( ๐ต ยท ๐‘ฆ ) = ๐ด ) โ†’ ๐‘ฅ = ๐‘ฆ ) )
26 oveq2 โŠข ( ๐‘ฅ = ๐‘ฆ โ†’ ( ๐ต ยท ๐‘ฅ ) = ( ๐ต ยท ๐‘ฆ ) )
27 26 eqeq1d โŠข ( ๐‘ฅ = ๐‘ฆ โ†’ ( ( ๐ต ยท ๐‘ฅ ) = ๐ด โ†” ( ๐ต ยท ๐‘ฆ ) = ๐ด ) )
28 27 reu4 โŠข ( โˆƒ! ๐‘ฅ โˆˆ โ„‚ ( ๐ต ยท ๐‘ฅ ) = ๐ด โ†” ( โˆƒ ๐‘ฅ โˆˆ โ„‚ ( ๐ต ยท ๐‘ฅ ) = ๐ด โˆง โˆ€ ๐‘ฅ โˆˆ โ„‚ โˆ€ ๐‘ฆ โˆˆ โ„‚ ( ( ( ๐ต ยท ๐‘ฅ ) = ๐ด โˆง ( ๐ต ยท ๐‘ฆ ) = ๐ด ) โ†’ ๐‘ฅ = ๐‘ฆ ) ) )
29 18 25 28 sylanbrc โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ต โ‰  0 ) โ†’ โˆƒ! ๐‘ฅ โˆˆ โ„‚ ( ๐ต ยท ๐‘ฅ ) = ๐ด )