Metamath Proof Explorer


Theorem xreceu

Description: Existential uniqueness of reciprocals. Theorem I.8 of Apostol p. 18. (Contributed by Thierry Arnoux, 17-Dec-2016)

Ref Expression
Assertion xreceu ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → ∃! 𝑥 ∈ ℝ* ( 𝐵 ·e 𝑥 ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 ressxr ℝ ⊆ ℝ*
2 xrecex ( ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → ∃ 𝑦 ∈ ℝ ( 𝐵 ·e 𝑦 ) = 1 )
3 2 3adant1 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → ∃ 𝑦 ∈ ℝ ( 𝐵 ·e 𝑦 ) = 1 )
4 ssrexv ( ℝ ⊆ ℝ* → ( ∃ 𝑦 ∈ ℝ ( 𝐵 ·e 𝑦 ) = 1 → ∃ 𝑦 ∈ ℝ* ( 𝐵 ·e 𝑦 ) = 1 ) )
5 1 3 4 mpsyl ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → ∃ 𝑦 ∈ ℝ* ( 𝐵 ·e 𝑦 ) = 1 )
6 simprl ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℝ* ∧ ( 𝐵 ·e 𝑦 ) = 1 ) ) → 𝑦 ∈ ℝ* )
7 simpll ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℝ* ∧ ( 𝐵 ·e 𝑦 ) = 1 ) ) → 𝐴 ∈ ℝ* )
8 6 7 xmulcld ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℝ* ∧ ( 𝐵 ·e 𝑦 ) = 1 ) ) → ( 𝑦 ·e 𝐴 ) ∈ ℝ* )
9 oveq1 ( ( 𝐵 ·e 𝑦 ) = 1 → ( ( 𝐵 ·e 𝑦 ) ·e 𝐴 ) = ( 1 ·e 𝐴 ) )
10 9 ad2antll ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℝ* ∧ ( 𝐵 ·e 𝑦 ) = 1 ) ) → ( ( 𝐵 ·e 𝑦 ) ·e 𝐴 ) = ( 1 ·e 𝐴 ) )
11 simplr ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℝ* ∧ ( 𝐵 ·e 𝑦 ) = 1 ) ) → 𝐵 ∈ ℝ )
12 11 rexrd ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℝ* ∧ ( 𝐵 ·e 𝑦 ) = 1 ) ) → 𝐵 ∈ ℝ* )
13 xmulass ( ( 𝐵 ∈ ℝ*𝑦 ∈ ℝ*𝐴 ∈ ℝ* ) → ( ( 𝐵 ·e 𝑦 ) ·e 𝐴 ) = ( 𝐵 ·e ( 𝑦 ·e 𝐴 ) ) )
14 12 6 7 13 syl3anc ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℝ* ∧ ( 𝐵 ·e 𝑦 ) = 1 ) ) → ( ( 𝐵 ·e 𝑦 ) ·e 𝐴 ) = ( 𝐵 ·e ( 𝑦 ·e 𝐴 ) ) )
15 xmulid2 ( 𝐴 ∈ ℝ* → ( 1 ·e 𝐴 ) = 𝐴 )
16 7 15 syl ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℝ* ∧ ( 𝐵 ·e 𝑦 ) = 1 ) ) → ( 1 ·e 𝐴 ) = 𝐴 )
17 10 14 16 3eqtr3d ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℝ* ∧ ( 𝐵 ·e 𝑦 ) = 1 ) ) → ( 𝐵 ·e ( 𝑦 ·e 𝐴 ) ) = 𝐴 )
18 oveq2 ( 𝑥 = ( 𝑦 ·e 𝐴 ) → ( 𝐵 ·e 𝑥 ) = ( 𝐵 ·e ( 𝑦 ·e 𝐴 ) ) )
19 18 eqeq1d ( 𝑥 = ( 𝑦 ·e 𝐴 ) → ( ( 𝐵 ·e 𝑥 ) = 𝐴 ↔ ( 𝐵 ·e ( 𝑦 ·e 𝐴 ) ) = 𝐴 ) )
20 19 rspcev ( ( ( 𝑦 ·e 𝐴 ) ∈ ℝ* ∧ ( 𝐵 ·e ( 𝑦 ·e 𝐴 ) ) = 𝐴 ) → ∃ 𝑥 ∈ ℝ* ( 𝐵 ·e 𝑥 ) = 𝐴 )
21 8 17 20 syl2anc ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℝ* ∧ ( 𝐵 ·e 𝑦 ) = 1 ) ) → ∃ 𝑥 ∈ ℝ* ( 𝐵 ·e 𝑥 ) = 𝐴 )
22 21 rexlimdvaa ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ ) → ( ∃ 𝑦 ∈ ℝ* ( 𝐵 ·e 𝑦 ) = 1 → ∃ 𝑥 ∈ ℝ* ( 𝐵 ·e 𝑥 ) = 𝐴 ) )
23 22 3adant3 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → ( ∃ 𝑦 ∈ ℝ* ( 𝐵 ·e 𝑦 ) = 1 → ∃ 𝑥 ∈ ℝ* ( 𝐵 ·e 𝑥 ) = 𝐴 ) )
24 5 23 mpd ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → ∃ 𝑥 ∈ ℝ* ( 𝐵 ·e 𝑥 ) = 𝐴 )
25 eqtr3 ( ( ( 𝐵 ·e 𝑥 ) = 𝐴 ∧ ( 𝐵 ·e 𝑦 ) = 𝐴 ) → ( 𝐵 ·e 𝑥 ) = ( 𝐵 ·e 𝑦 ) )
26 simp1 ( ( 𝑥 ∈ ℝ*𝑦 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ) → 𝑥 ∈ ℝ* )
27 simp2 ( ( 𝑥 ∈ ℝ*𝑦 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ) → 𝑦 ∈ ℝ* )
28 simp3l ( ( 𝑥 ∈ ℝ*𝑦 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ) → 𝐵 ∈ ℝ )
29 simp3r ( ( 𝑥 ∈ ℝ*𝑦 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ) → 𝐵 ≠ 0 )
30 26 27 28 29 xmulcand ( ( 𝑥 ∈ ℝ*𝑦 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ) → ( ( 𝐵 ·e 𝑥 ) = ( 𝐵 ·e 𝑦 ) ↔ 𝑥 = 𝑦 ) )
31 25 30 syl5ib ( ( 𝑥 ∈ ℝ*𝑦 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ) → ( ( ( 𝐵 ·e 𝑥 ) = 𝐴 ∧ ( 𝐵 ·e 𝑦 ) = 𝐴 ) → 𝑥 = 𝑦 ) )
32 31 3expa ( ( ( 𝑥 ∈ ℝ*𝑦 ∈ ℝ* ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ) → ( ( ( 𝐵 ·e 𝑥 ) = 𝐴 ∧ ( 𝐵 ·e 𝑦 ) = 𝐴 ) → 𝑥 = 𝑦 ) )
33 32 expcom ( ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → ( ( 𝑥 ∈ ℝ*𝑦 ∈ ℝ* ) → ( ( ( 𝐵 ·e 𝑥 ) = 𝐴 ∧ ( 𝐵 ·e 𝑦 ) = 𝐴 ) → 𝑥 = 𝑦 ) ) )
34 33 3adant1 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → ( ( 𝑥 ∈ ℝ*𝑦 ∈ ℝ* ) → ( ( ( 𝐵 ·e 𝑥 ) = 𝐴 ∧ ( 𝐵 ·e 𝑦 ) = 𝐴 ) → 𝑥 = 𝑦 ) ) )
35 34 ralrimivv ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → ∀ 𝑥 ∈ ℝ*𝑦 ∈ ℝ* ( ( ( 𝐵 ·e 𝑥 ) = 𝐴 ∧ ( 𝐵 ·e 𝑦 ) = 𝐴 ) → 𝑥 = 𝑦 ) )
36 oveq2 ( 𝑥 = 𝑦 → ( 𝐵 ·e 𝑥 ) = ( 𝐵 ·e 𝑦 ) )
37 36 eqeq1d ( 𝑥 = 𝑦 → ( ( 𝐵 ·e 𝑥 ) = 𝐴 ↔ ( 𝐵 ·e 𝑦 ) = 𝐴 ) )
38 37 reu4 ( ∃! 𝑥 ∈ ℝ* ( 𝐵 ·e 𝑥 ) = 𝐴 ↔ ( ∃ 𝑥 ∈ ℝ* ( 𝐵 ·e 𝑥 ) = 𝐴 ∧ ∀ 𝑥 ∈ ℝ*𝑦 ∈ ℝ* ( ( ( 𝐵 ·e 𝑥 ) = 𝐴 ∧ ( 𝐵 ·e 𝑦 ) = 𝐴 ) → 𝑥 = 𝑦 ) ) )
39 24 35 38 sylanbrc ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → ∃! 𝑥 ∈ ℝ* ( 𝐵 ·e 𝑥 ) = 𝐴 )