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 xmullid ⊢ ( 𝐴 ∈ ℝ* → ( 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 imbitrid ⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 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 𝑥 ) = 𝐴 )