Metamath Proof Explorer

Theorem redvr

Description: The division operation of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017)

Ref Expression
Assertion redvr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ B ≠ 0 → A / r ⁡ ℝ fld B = A B

Proof

Step Hyp Ref Expression
1 resubdrg ⊢ ℝ ∈ SubRing ⁡ ℂ fld ∧ ℝ fld ∈ DivRing
2 1 simpli ⊢ ℝ ∈ SubRing ⁡ ℂ fld
3 simp1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ B ≠ 0 → A ∈ ℝ
4 3simpc ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ B ≠ 0 → B ∈ ℝ ∧ B ≠ 0
5 1 simpri ⊢ ℝ fld ∈ DivRing
6 rebase ⊢ ℝ = Base ℝ fld
7 eqid ⊢ Unit ⁡ ℝ fld = Unit ⁡ ℝ fld
8 re0g ⊢ 0 = 0 ℝ fld
9 6 7 8 drngunit ⊢ ℝ fld ∈ DivRing → B ∈ Unit ⁡ ℝ fld ↔ B ∈ ℝ ∧ B ≠ 0
10 5 9 ax-mp ⊢ B ∈ Unit ⁡ ℝ fld ↔ B ∈ ℝ ∧ B ≠ 0
11 4 10 sylibr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ B ≠ 0 → B ∈ Unit ⁡ ℝ fld
12 df-refld ⊢ ℝ fld = ℂ fld ↾ 𝑠 ℝ
13 cnflddiv ⊢ ÷ = / r ⁡ ℂ fld
14 eqid ⊢ / r ⁡ ℝ fld = / r ⁡ ℝ fld
15 12 13 7 14 subrgdv ⊢ ℝ ∈ SubRing ⁡ ℂ fld ∧ A ∈ ℝ ∧ B ∈ Unit ⁡ ℝ fld → A B = A / r ⁡ ℝ fld B
16 2 3 11 15 mp3an2i ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ B ≠ 0 → A B = A / r ⁡ ℝ fld B
17 16 eqcomd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ B ≠ 0 → A / r ⁡ ℝ fld B = A B