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 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → ( 𝐴 ( /r ‘ ℝfld ) 𝐵 ) = ( 𝐴 / 𝐵 ) )

Proof

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