Database
REAL AND COMPLEX NUMBERS
Derive the basic properties from the field axioms
Some deductions from the field axioms for complex numbers
0red
Next ⟩
mulid1i
Metamath Proof Explorer
Ascii
Structured
Theorem
0red
Description:
The number 0 is real, deduction form.
(Contributed by
David A. Wheeler
, 6-Dec-2018)
Ref
Expression
Assertion
0red
⊢
(
𝜑
→ 0 ∈ ℝ )
Proof
Step
Hyp
Ref
Expression
1
0re
⊢
0 ∈ ℝ
2
1
a1i
⊢
(
𝜑
→ 0 ∈ ℝ )