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 𝑥 ) = 𝐴 )