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