Theorem sqrt2irr0

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

	Ref	Expression
Assertion	sqrt2irr0	|- ( sqrt ` 2 ) e. ( RR \ QQ )

Proof

Step	Hyp	Ref	Expression
1		sqrt2irr	|- ( sqrt ` 2 ) e/ QQ
2		sqrt2re	|- ( sqrt ` 2 ) e. RR
3	2	a1i	|- ( ( sqrt ` 2 ) e/ QQ -> ( sqrt ` 2 ) e. RR )
4		df-nel	|- ( ( sqrt ` 2 ) e/ QQ <-> -. ( sqrt ` 2 ) e. QQ )
5	4	biimpi	|- ( ( sqrt ` 2 ) e/ QQ -> -. ( sqrt ` 2 ) e. QQ )
6	3 5	eldifd	|- ( ( sqrt ` 2 ) e/ QQ -> ( sqrt ` 2 ) e. ( RR \ QQ ) )
7	1 6	ax-mp	|- ( sqrt ` 2 ) e. ( RR \ QQ )