Metamath Proof Explorer

Theorem rediveud

Description: Existential uniqueness of real quotients. (Contributed by SN, 25-Nov-2025)

Ref Expression
Hypotheses redivvald.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
redivvald.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
redivvald.z ⊢ ( 𝜑 → 𝐵 ≠ 0 )
Assertion rediveud ( 𝜑 → ∃! 𝑥 ∈ ℝ ( 𝐵 · 𝑥 ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 redivvald.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 redivvald.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 redivvald.z ⊢ ( 𝜑 → 𝐵 ≠ 0 )
4 ax-rrecex ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → ∃ 𝑦 ∈ ℝ ( 𝐵 · 𝑦 ) = 1 )
5 2 3 4 syl2anc ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ( 𝐵 · 𝑦 ) = 1 )
6 oveq2 ⊢ ( 𝑥 = ( 𝑦 · 𝐴 ) → ( 𝐵 · 𝑥 ) = ( 𝐵 · ( 𝑦 · 𝐴 ) ) )
7 6 eqeq1d ⊢ ( 𝑥 = ( 𝑦 · 𝐴 ) → ( ( 𝐵 · 𝑥 ) = 𝐴 ↔ ( 𝐵 · ( 𝑦 · 𝐴 ) ) = 𝐴 ) )
8 simprl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝐵 · 𝑦 ) = 1 ) ) → 𝑦 ∈ ℝ )
9 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝐵 · 𝑦 ) = 1 ) ) → 𝐴 ∈ ℝ )
10 8 9 remulcld ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝐵 · 𝑦 ) = 1 ) ) → ( 𝑦 · 𝐴 ) ∈ ℝ )
11 simprr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝐵 · 𝑦 ) = 1 ) ) → ( 𝐵 · 𝑦 ) = 1 )
12 11 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝐵 · 𝑦 ) = 1 ) ) → ( ( 𝐵 · 𝑦 ) · 𝐴 ) = ( 1 · 𝐴 ) )
13 2 recnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
14 13 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝐵 · 𝑦 ) = 1 ) ) → 𝐵 ∈ ℂ )
15 8 recnd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝐵 · 𝑦 ) = 1 ) ) → 𝑦 ∈ ℂ )
16 1 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
17 16 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝐵 · 𝑦 ) = 1 ) ) → 𝐴 ∈ ℂ )
18 14 15 17 mulassd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝐵 · 𝑦 ) = 1 ) ) → ( ( 𝐵 · 𝑦 ) · 𝐴 ) = ( 𝐵 · ( 𝑦 · 𝐴 ) ) )
19 remullid ⊢ ( 𝐴 ∈ ℝ → ( 1 · 𝐴 ) = 𝐴 )
20 1 19 syl ⊢ ( 𝜑 → ( 1 · 𝐴 ) = 𝐴 )
21 20 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝐵 · 𝑦 ) = 1 ) ) → ( 1 · 𝐴 ) = 𝐴 )
22 12 18 21 3eqtr3d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝐵 · 𝑦 ) = 1 ) ) → ( 𝐵 · ( 𝑦 · 𝐴 ) ) = 𝐴 )
23 7 10 22 rspcedvdw ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝐵 · 𝑦 ) = 1 ) ) → ∃ 𝑥 ∈ ℝ ( 𝐵 · 𝑥 ) = 𝐴 )
24 5 23 rexlimddv ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ( 𝐵 · 𝑥 ) = 𝐴 )
25 eqtr3 ⊢ ( ( ( 𝐵 · 𝑥 ) = 𝐴 ∧ ( 𝐵 · 𝑦 ) = 𝐴 ) → ( 𝐵 · 𝑥 ) = ( 𝐵 · 𝑦 ) )
26 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) → 𝑥 ∈ ℝ )
27 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) → 𝑦 ∈ ℝ )
28 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) → 𝐵 ∈ ℝ )
29 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) → 𝐵 ≠ 0 )
30 26 27 28 29 remulcand ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) → ( ( 𝐵 · 𝑥 ) = ( 𝐵 · 𝑦 ) ↔ 𝑥 = 𝑦 ) )
31 25 30 imbitrid ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) → ( ( ( 𝐵 · 𝑥 ) = 𝐴 ∧ ( 𝐵 · 𝑦 ) = 𝐴 ) → 𝑥 = 𝑦 ) )
32 31 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℝ ( ( ( 𝐵 · 𝑥 ) = 𝐴 ∧ ( 𝐵 · 𝑦 ) = 𝐴 ) → 𝑥 = 𝑦 ) )
33 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐵 · 𝑥 ) = ( 𝐵 · 𝑦 ) )
34 33 eqeq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐵 · 𝑥 ) = 𝐴 ↔ ( 𝐵 · 𝑦 ) = 𝐴 ) )
35 34 reu4 ⊢ ( ∃! 𝑥 ∈ ℝ ( 𝐵 · 𝑥 ) = 𝐴 ↔ ( ∃ 𝑥 ∈ ℝ ( 𝐵 · 𝑥 ) = 𝐴 ∧ ∀ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℝ ( ( ( 𝐵 · 𝑥 ) = 𝐴 ∧ ( 𝐵 · 𝑦 ) = 𝐴 ) → 𝑥 = 𝑦 ) ) )
36 24 32 35 sylanbrc ⊢ ( 𝜑 → ∃! 𝑥 ∈ ℝ ( 𝐵 · 𝑥 ) = 𝐴 )