Metamath Proof Explorer

Theorem remulcan2d

Description: mulcan2d for real numbers using fewer axioms. (Contributed by Steven Nguyen, 15-Apr-2023)

Ref Expression
Hypotheses remulcan2d.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
remulcan2d.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
remulcan2d.3 ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
remulcan2d.4 ⊢ ( 𝜑 → 𝐶 ≠ 0 )
Assertion remulcan2d ( 𝜑 → ( ( 𝐴 · 𝐶 ) = ( 𝐵 · 𝐶 ) ↔ 𝐴 = 𝐵 ) )

Proof

Step Hyp Ref Expression
1 remulcan2d.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 remulcan2d.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 remulcan2d.3 ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
4 remulcan2d.4 ⊢ ( 𝜑 → 𝐶 ≠ 0 )
5 ax-rrecex ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐶 ≠ 0 ) → ∃ 𝑥 ∈ ℝ ( 𝐶 · 𝑥 ) = 1 )
6 3 4 5 syl2anc ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ( 𝐶 · 𝑥 ) = 1 )
7 oveq1 ⊢ ( ( 𝐴 · 𝐶 ) = ( 𝐵 · 𝐶 ) → ( ( 𝐴 · 𝐶 ) · 𝑥 ) = ( ( 𝐵 · 𝐶 ) · 𝑥 ) )
8 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐶 · 𝑥 ) = 1 ) ) → 𝐴 ∈ ℝ )
9 8 recnd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐶 · 𝑥 ) = 1 ) ) → 𝐴 ∈ ℂ )
10 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐶 · 𝑥 ) = 1 ) ) → 𝐶 ∈ ℝ )
11 10 recnd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐶 · 𝑥 ) = 1 ) ) → 𝐶 ∈ ℂ )
12 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐶 · 𝑥 ) = 1 ) ) → 𝑥 ∈ ℝ )
13 12 recnd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐶 · 𝑥 ) = 1 ) ) → 𝑥 ∈ ℂ )
14 9 11 13 mulassd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐶 · 𝑥 ) = 1 ) ) → ( ( 𝐴 · 𝐶 ) · 𝑥 ) = ( 𝐴 · ( 𝐶 · 𝑥 ) ) )
15 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐶 · 𝑥 ) = 1 ) ) → ( 𝐶 · 𝑥 ) = 1 )
16 15 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐶 · 𝑥 ) = 1 ) ) → ( 𝐴 · ( 𝐶 · 𝑥 ) ) = ( 𝐴 · 1 ) )
17 ax-1rid ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 · 1 ) = 𝐴 )
18 8 17 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐶 · 𝑥 ) = 1 ) ) → ( 𝐴 · 1 ) = 𝐴 )
19 14 16 18 3eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐶 · 𝑥 ) = 1 ) ) → ( ( 𝐴 · 𝐶 ) · 𝑥 ) = 𝐴 )
20 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐶 · 𝑥 ) = 1 ) ) → 𝐵 ∈ ℝ )
21 20 recnd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐶 · 𝑥 ) = 1 ) ) → 𝐵 ∈ ℂ )
22 21 11 13 mulassd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐶 · 𝑥 ) = 1 ) ) → ( ( 𝐵 · 𝐶 ) · 𝑥 ) = ( 𝐵 · ( 𝐶 · 𝑥 ) ) )
23 15 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐶 · 𝑥 ) = 1 ) ) → ( 𝐵 · ( 𝐶 · 𝑥 ) ) = ( 𝐵 · 1 ) )
24 ax-1rid ⊢ ( 𝐵 ∈ ℝ → ( 𝐵 · 1 ) = 𝐵 )
25 20 24 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐶 · 𝑥 ) = 1 ) ) → ( 𝐵 · 1 ) = 𝐵 )
26 22 23 25 3eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐶 · 𝑥 ) = 1 ) ) → ( ( 𝐵 · 𝐶 ) · 𝑥 ) = 𝐵 )
27 19 26 eqeq12d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐶 · 𝑥 ) = 1 ) ) → ( ( ( 𝐴 · 𝐶 ) · 𝑥 ) = ( ( 𝐵 · 𝐶 ) · 𝑥 ) ↔ 𝐴 = 𝐵 ) )
28 7 27 imbitrid ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐶 · 𝑥 ) = 1 ) ) → ( ( 𝐴 · 𝐶 ) = ( 𝐵 · 𝐶 ) → 𝐴 = 𝐵 ) )
29 6 28 rexlimddv ⊢ ( 𝜑 → ( ( 𝐴 · 𝐶 ) = ( 𝐵 · 𝐶 ) → 𝐴 = 𝐵 ) )
30 oveq1 ⊢ ( 𝐴 = 𝐵 → ( 𝐴 · 𝐶 ) = ( 𝐵 · 𝐶 ) )
31 29 30 impbid1 ⊢ ( 𝜑 → ( ( 𝐴 · 𝐶 ) = ( 𝐵 · 𝐶 ) ↔ 𝐴 = 𝐵 ) )