Theorem 0re

Description: The number 0 is real. Remark: the first step could also be ax-icn . See also 0reALT . (Contributed by Eric Schmidt, 21-May-2007) (Revised by Scott Fenton, 3-Jan-2013) Reduce dependencies on axioms. (Revised by Steven Nguyen, 11-Oct-2022)

	Ref	Expression
Assertion	0re	⊢ 0 ∈ ℝ

Proof

Step	Hyp	Ref	Expression
1		ax-1cn	⊢ 1 ∈ ℂ
2		cnre	⊢ ( 1 ∈ ℂ → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 1 = ( 𝑥 + ( i · 𝑦 ) ) )
3		ax-rnegex	⊢ ( 𝑥 ∈ ℝ → ∃ 𝑧 ∈ ℝ ( 𝑥 + 𝑧 ) = 0 )
4		readdcl	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( 𝑥 + 𝑧 ) ∈ ℝ )
5		eleq1	⊢ ( ( 𝑥 + 𝑧 ) = 0 → ( ( 𝑥 + 𝑧 ) ∈ ℝ ↔ 0 ∈ ℝ ) )
6	4 5	syl5ibcom	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( ( 𝑥 + 𝑧 ) = 0 → 0 ∈ ℝ ) )
7	6	rexlimdva	⊢ ( 𝑥 ∈ ℝ → ( ∃ 𝑧 ∈ ℝ ( 𝑥 + 𝑧 ) = 0 → 0 ∈ ℝ ) )
8	3 7	mpd	⊢ ( 𝑥 ∈ ℝ → 0 ∈ ℝ )
9	8	adantr	⊢ ( ( 𝑥 ∈ ℝ ∧ ∃ 𝑦 ∈ ℝ 1 = ( 𝑥 + ( i · 𝑦 ) ) ) → 0 ∈ ℝ )
10	9	rexlimiva	⊢ ( ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 1 = ( 𝑥 + ( i · 𝑦 ) ) → 0 ∈ ℝ )
11	1 2 10	mp2b	⊢ 0 ∈ ℝ