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 \in ℝ$

Proof

Step	Hyp	Ref	Expression
1		ax-1cn	$⊢ 1 \in ℂ$
2		cnre	$⊢ 1 \in ℂ \to \exists x \in ℝ \exists y \in ℝ 1 = x + i y$
3		ax-rnegex	$⊢ x \in ℝ \to \exists z \in ℝ x + z = 0$
4		readdcl	$⊢ (x \in ℝ \land z \in ℝ) \to x + z \in ℝ$
5		eleq1	$⊢ x + z = 0 \to (x + z \in ℝ \leftrightarrow 0 \in ℝ)$
6	4 5	syl5ibcom	$⊢ (x \in ℝ \land z \in ℝ) \to (x + z = 0 \to 0 \in ℝ)$
7	6	rexlimdva	$⊢ x \in ℝ \to (\exists z \in ℝ x + z = 0 \to 0 \in ℝ)$
8	3 7	mpd	$⊢ x \in ℝ \to 0 \in ℝ$
9	8	adantr	$⊢ (x \in ℝ \land \exists y \in ℝ 1 = x + i y) \to 0 \in ℝ$
10	9	rexlimiva	$⊢ \exists x \in ℝ \exists y \in ℝ 1 = x + i y \to 0 \in ℝ$
11	1 2 10	mp2b	$⊢ 0 \in ℝ$

Metamath Proof Explorer

Theorem 0re

Proof