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 ⊢ A ∈ ℝ * ∧ B ∈ ℝ ∧ B ≠ 0 → ∃! x ∈ ℝ * B ⋅ 𝑒 x = A

Proof

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