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 \left(ℝ\setminus \mathbb{Q}\right)$$

Proof

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