This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sqrt2irr0

Description: The square root of 2 is an irrational number. (Contributed by AV, 23-Dec-2022)

		Ref	Expression
	Assertion	sqrt2irr0	$⊢ \sqrt{2} \in (ℝ ∖ ℚ)$

Step	Hyp	Ref	Expression
1		sqrt2irr	$⊢ \sqrt{2} \notin ℚ$
2		sqrt2re	$⊢ \sqrt{2} \in ℝ$
3	2	a1i	$⊢ \sqrt{2} \notin ℚ \to \sqrt{2} \in ℝ$
4		df-nel	$⊢ \sqrt{2} \notin ℚ \leftrightarrow \neg \sqrt{2} \in ℚ$
5	4	biimpi	$⊢ \sqrt{2} \notin ℚ \to \neg \sqrt{2} \in ℚ$
6	3 5	eldifd	$⊢ \sqrt{2} \notin ℚ \to \sqrt{2} \in (ℝ ∖ ℚ)$
7	1 6	ax-mp	$⊢ \sqrt{2} \in (ℝ ∖ ℚ)$