Metamath Proof Explorer

Theorem resubdrg

Description: The real numbers form a division subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014) (Revised by Thierry Arnoux, 30-Jun-2019)

Ref Expression
Assertion resubdrg ⊢ ℝ ∈ SubRing ⁡ ℂ fld ∧ ℝ fld ∈ DivRing

Proof

Step Hyp Ref Expression
1 recn ⊢ x ∈ ℝ → x ∈ ℂ
2 readdcl ⊢ x ∈ ℝ ∧ y ∈ ℝ → x + y ∈ ℝ
3 renegcl ⊢ x ∈ ℝ → − x ∈ ℝ
4 1re ⊢ 1 ∈ ℝ
5 remulcl ⊢ x ∈ ℝ ∧ y ∈ ℝ → x ⁢ y ∈ ℝ
6 rereccl ⊢ x ∈ ℝ ∧ x ≠ 0 → 1 x ∈ ℝ
7 1 2 3 4 5 6 cnsubdrglem ⊢ ℝ ∈ SubRing ⁡ ℂ fld ∧ ℂ fld ↾ 𝑠 ℝ ∈ DivRing
8 df-refld ⊢ ℝ fld = ℂ fld ↾ 𝑠 ℝ
9 8 eleq1i ⊢ ℝ fld ∈ DivRing ↔ ℂ fld ↾ 𝑠 ℝ ∈ DivRing
10 9 anbi2i ⊢ ℝ ∈ SubRing ⁡ ℂ fld ∧ ℝ fld ∈ DivRing ↔ ℝ ∈ SubRing ⁡ ℂ fld ∧ ℂ fld ↾ 𝑠 ℝ ∈ DivRing
11 7 10 mpbir ⊢ ℝ ∈ SubRing ⁡ ℂ fld ∧ ℝ fld ∈ DivRing