Theorem sqrt2irr0

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

	Ref	Expression
Assertion	sqrt2irr0	⊢ ( √ ‘ 2 ) ∈ ( ℝ ∖ ℚ )

Proof

Step	Hyp	Ref	Expression
1		sqrt2irr	⊢ ( √ ‘ 2 ) ∉ ℚ
2		sqrt2re	⊢ ( √ ‘ 2 ) ∈ ℝ
3	2	a1i	⊢ ( ( √ ‘ 2 ) ∉ ℚ → ( √ ‘ 2 ) ∈ ℝ )
4		df-nel	⊢ ( ( √ ‘ 2 ) ∉ ℚ ↔ ¬ ( √ ‘ 2 ) ∈ ℚ )
5	4	biimpi	⊢ ( ( √ ‘ 2 ) ∉ ℚ → ¬ ( √ ‘ 2 ) ∈ ℚ )
6	3 5	eldifd	⊢ ( ( √ ‘ 2 ) ∉ ℚ → ( √ ‘ 2 ) ∈ ( ℝ ∖ ℚ ) )
7	1 6	ax-mp	⊢ ( √ ‘ 2 ) ∈ ( ℝ ∖ ℚ )