sqrt2irr

Description: The square root of 2 is irrational. See zsqrtelqelz for a generalization to all non-square integers. The proof's core is proven in sqrt2irrlem , which shows that if A / B = sqrt ( 2 ) , then A and B are even, so A / 2 and B / 2 are smaller representatives, which is absurd. An older version of this proof was included inThe Seventeen Provers of the World compiled by Freek Wiedijk. It is also the first of the "top 100" mathematical theorems whose formalization is tracked by Freek Wiedijk on hisFormalizing 100 Theorems page at http://www.cs.ru.nl/~freek/100/ . (Contributed by NM, 8-Jan-2002) (Proof shortened by Mario Carneiro, 12-Sep-2015)

		Ref	Expression
	Assertion	sqrt2irr	$⊢ \sqrt{2} \notin ℚ$

Proof

Step	Hyp	Ref	Expression
1		peano2nn	$⊢ y \in ℕ \to y + 1 \in ℕ$
2		breq2	$⊢ n = 1 \to (z < n \leftrightarrow z < 1)$
3	2	imbi1d	$⊢ n = 1 \to ((z < n \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{z}) \leftrightarrow (z < 1 \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{z}))$
4	3	ralbidv	$⊢ n = 1 \to (\forall z \in ℕ (z < n \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{z}) \leftrightarrow \forall z \in ℕ (z < 1 \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{z}))$
5		breq2	$⊢ n = y \to (z < n \leftrightarrow z < y)$
6	5	imbi1d	$⊢ n = y \to ((z < n \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{z}) \leftrightarrow (z < y \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{z}))$
7	6	ralbidv	$⊢ n = y \to (\forall z \in ℕ (z < n \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{z}) \leftrightarrow \forall z \in ℕ (z < y \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{z}))$
8		breq2	$⊢ n = y + 1 \to (z < n \leftrightarrow z < y + 1)$
9	8	imbi1d	$⊢ n = y + 1 \to ((z < n \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{z}) \leftrightarrow (z < y + 1 \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{z}))$
10	9	ralbidv	$⊢ n = y + 1 \to (\forall z \in ℕ (z < n \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{z}) \leftrightarrow \forall z \in ℕ (z < y + 1 \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{z}))$
11		nnnlt1	$⊢ z \in ℕ \to \neg z < 1$
12	11	pm2.21d	$⊢ z \in ℕ \to (z < 1 \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{z})$
13	12	rgen	$⊢ \forall z \in ℕ (z < 1 \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{z})$
14		nnrp	$⊢ y \in ℕ \to y \in ℝ^{+}$
15		rphalflt	$⊢ y \in ℝ^{+} \to \frac{y}{2} < y$
16	14 15	syl	$⊢ y \in ℕ \to \frac{y}{2} < y$
17		breq1	$⊢ z = \frac{y}{2} \to (z < y \leftrightarrow \frac{y}{2} < y)$
18		oveq2	$⊢ z = \frac{y}{2} \to \frac{x}{z} = \frac{x}{\frac{y}{2}}$
19	18	neeq2d	$⊢ z = \frac{y}{2} \to (\sqrt{2} \neq \frac{x}{z} \leftrightarrow \sqrt{2} \neq \frac{x}{\frac{y}{2}})$
20	19	ralbidv	$⊢ z = \frac{y}{2} \to (\forall x \in ℤ \sqrt{2} \neq \frac{x}{z} \leftrightarrow \forall x \in ℤ \sqrt{2} \neq \frac{x}{\frac{y}{2}})$
21	17 20	imbi12d	$⊢ z = \frac{y}{2} \to ((z < y \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{z}) \leftrightarrow (\frac{y}{2} < y \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{\frac{y}{2}}))$
22	21	rspcv	$⊢ \frac{y}{2} \in ℕ \to (\forall z \in ℕ (z < y \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{z}) \to (\frac{y}{2} < y \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{\frac{y}{2}}))$
23	22	com13	$⊢ \frac{y}{2} < y \to (\forall z \in ℕ (z < y \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{z}) \to (\frac{y}{2} \in ℕ \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{\frac{y}{2}}))$
24	16 23	syl	$⊢ y \in ℕ \to (\forall z \in ℕ (z < y \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{z}) \to (\frac{y}{2} \in ℕ \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{\frac{y}{2}}))$
25		simpr	$⊢ ((y \in ℕ \land z \in ℤ) \land \sqrt{2} = \frac{z}{y}) \to \sqrt{2} = \frac{z}{y}$
26		zcn	$⊢ z \in ℤ \to z \in ℂ$
27	26	ad2antlr	$⊢ ((y \in ℕ \land z \in ℤ) \land \sqrt{2} = \frac{z}{y}) \to z \in ℂ$
28		nncn	$⊢ y \in ℕ \to y \in ℂ$
29	28	ad2antrr	$⊢ ((y \in ℕ \land z \in ℤ) \land \sqrt{2} = \frac{z}{y}) \to y \in ℂ$
30		2cnd	$⊢ ((y \in ℕ \land z \in ℤ) \land \sqrt{2} = \frac{z}{y}) \to 2 \in ℂ$
31		nnne0	$⊢ y \in ℕ \to y \neq 0$
32	31	ad2antrr	$⊢ ((y \in ℕ \land z \in ℤ) \land \sqrt{2} = \frac{z}{y}) \to y \neq 0$
33		2ne0	$⊢ 2 \neq 0$
34	33	a1i	$⊢ ((y \in ℕ \land z \in ℤ) \land \sqrt{2} = \frac{z}{y}) \to 2 \neq 0$
35	27 29 30 32 34	divcan7d	$⊢ ((y \in ℕ \land z \in ℤ) \land \sqrt{2} = \frac{z}{y}) \to \frac{\frac{z}{2}}{\frac{y}{2}} = \frac{z}{y}$
36	25 35	eqtr4d	$⊢ ((y \in ℕ \land z \in ℤ) \land \sqrt{2} = \frac{z}{y}) \to \sqrt{2} = \frac{\frac{z}{2}}{\frac{y}{2}}$
37		simplr	$⊢ ((y \in ℕ \land z \in ℤ) \land \sqrt{2} = \frac{z}{y}) \to z \in ℤ$
38		simpll	$⊢ ((y \in ℕ \land z \in ℤ) \land \sqrt{2} = \frac{z}{y}) \to y \in ℕ$
39	37 38 25	sqrt2irrlem	$⊢ ((y \in ℕ \land z \in ℤ) \land \sqrt{2} = \frac{z}{y}) \to (\frac{z}{2} \in ℤ \land \frac{y}{2} \in ℕ)$
40	39	simprd	$⊢ ((y \in ℕ \land z \in ℤ) \land \sqrt{2} = \frac{z}{y}) \to \frac{y}{2} \in ℕ$
41	39	simpld	$⊢ ((y \in ℕ \land z \in ℤ) \land \sqrt{2} = \frac{z}{y}) \to \frac{z}{2} \in ℤ$
42		oveq1	$⊢ x = \frac{z}{2} \to \frac{x}{\frac{y}{2}} = \frac{\frac{z}{2}}{\frac{y}{2}}$
43	42	neeq2d	$⊢ x = \frac{z}{2} \to (\sqrt{2} \neq \frac{x}{\frac{y}{2}} \leftrightarrow \sqrt{2} \neq \frac{\frac{z}{2}}{\frac{y}{2}})$
44	43	rspcv	$⊢ \frac{z}{2} \in ℤ \to (\forall x \in ℤ \sqrt{2} \neq \frac{x}{\frac{y}{2}} \to \sqrt{2} \neq \frac{\frac{z}{2}}{\frac{y}{2}})$
45	41 44	syl	$⊢ ((y \in ℕ \land z \in ℤ) \land \sqrt{2} = \frac{z}{y}) \to (\forall x \in ℤ \sqrt{2} \neq \frac{x}{\frac{y}{2}} \to \sqrt{2} \neq \frac{\frac{z}{2}}{\frac{y}{2}})$
46	40 45	embantd	$⊢ ((y \in ℕ \land z \in ℤ) \land \sqrt{2} = \frac{z}{y}) \to ((\frac{y}{2} \in ℕ \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{\frac{y}{2}}) \to \sqrt{2} \neq \frac{\frac{z}{2}}{\frac{y}{2}})$
47	46	necon2bd	$⊢ ((y \in ℕ \land z \in ℤ) \land \sqrt{2} = \frac{z}{y}) \to (\sqrt{2} = \frac{\frac{z}{2}}{\frac{y}{2}} \to \neg (\frac{y}{2} \in ℕ \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{\frac{y}{2}}))$
48	36 47	mpd	$⊢ ((y \in ℕ \land z \in ℤ) \land \sqrt{2} = \frac{z}{y}) \to \neg (\frac{y}{2} \in ℕ \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{\frac{y}{2}})$
49	48	ex	$⊢ (y \in ℕ \land z \in ℤ) \to (\sqrt{2} = \frac{z}{y} \to \neg (\frac{y}{2} \in ℕ \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{\frac{y}{2}}))$
50	49	necon2ad	$⊢ (y \in ℕ \land z \in ℤ) \to ((\frac{y}{2} \in ℕ \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{\frac{y}{2}}) \to \sqrt{2} \neq \frac{z}{y})$
51	50	ralrimdva	$⊢ y \in ℕ \to ((\frac{y}{2} \in ℕ \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{\frac{y}{2}}) \to \forall z \in ℤ \sqrt{2} \neq \frac{z}{y})$
52	24 51	syld	$⊢ y \in ℕ \to (\forall z \in ℕ (z < y \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{z}) \to \forall z \in ℤ \sqrt{2} \neq \frac{z}{y})$
53		oveq1	$⊢ x = z \to \frac{x}{y} = \frac{z}{y}$
54	53	neeq2d	$⊢ x = z \to (\sqrt{2} \neq \frac{x}{y} \leftrightarrow \sqrt{2} \neq \frac{z}{y})$
55	54	cbvralvw	$⊢ \forall x \in ℤ \sqrt{2} \neq \frac{x}{y} \leftrightarrow \forall z \in ℤ \sqrt{2} \neq \frac{z}{y}$
56	52 55	imbitrrdi	$⊢ y \in ℕ \to (\forall z \in ℕ (z < y \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{z}) \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{y})$
57		oveq2	$⊢ z = y \to \frac{x}{z} = \frac{x}{y}$
58	57	neeq2d	$⊢ z = y \to (\sqrt{2} \neq \frac{x}{z} \leftrightarrow \sqrt{2} \neq \frac{x}{y})$
59	58	ralbidv	$⊢ z = y \to (\forall x \in ℤ \sqrt{2} \neq \frac{x}{z} \leftrightarrow \forall x \in ℤ \sqrt{2} \neq \frac{x}{y})$
60	59	ceqsralv	$⊢ y \in ℕ \to (\forall z \in ℕ (z = y \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{z}) \leftrightarrow \forall x \in ℤ \sqrt{2} \neq \frac{x}{y})$
61	56 60	sylibrd	$⊢ y \in ℕ \to (\forall z \in ℕ (z < y \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{z}) \to \forall z \in ℕ (z = y \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{z}))$
62	61	ancld	$⊢ y \in ℕ \to (\forall z \in ℕ (z < y \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{z}) \to (\forall z \in ℕ (z < y \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{z}) \land \forall z \in ℕ (z = y \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{z})))$
63		nnleltp1	$⊢ (z \in ℕ \land y \in ℕ) \to (z \leq y \leftrightarrow z < y + 1)$
64		nnre	$⊢ z \in ℕ \to z \in ℝ$
65		nnre	$⊢ y \in ℕ \to y \in ℝ$
66		leloe	$⊢ (z \in ℝ \land y \in ℝ) \to (z \leq y \leftrightarrow (z < y \lor z = y))$
67	64 65 66	syl2an	$⊢ (z \in ℕ \land y \in ℕ) \to (z \leq y \leftrightarrow (z < y \lor z = y))$
68	63 67	bitr3d	$⊢ (z \in ℕ \land y \in ℕ) \to (z < y + 1 \leftrightarrow (z < y \lor z = y))$
69	68	ancoms	$⊢ (y \in ℕ \land z \in ℕ) \to (z < y + 1 \leftrightarrow (z < y \lor z = y))$
70	69	imbi1d	$⊢ (y \in ℕ \land z \in ℕ) \to ((z < y + 1 \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{z}) \leftrightarrow ((z < y \lor z = y) \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{z}))$
71		jaob	$⊢ ((z < y \lor z = y) \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{z}) \leftrightarrow ((z < y \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{z}) \land (z = y \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{z}))$
72	70 71	bitrdi	$⊢ (y \in ℕ \land z \in ℕ) \to ((z < y + 1 \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{z}) \leftrightarrow ((z < y \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{z}) \land (z = y \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{z})))$
73	72	ralbidva	$⊢ y \in ℕ \to (\forall z \in ℕ (z < y + 1 \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{z}) \leftrightarrow \forall z \in ℕ ((z < y \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{z}) \land (z = y \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{z})))$
74		r19.26	$⊢ \forall z \in ℕ ((z < y \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{z}) \land (z = y \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{z})) \leftrightarrow (\forall z \in ℕ (z < y \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{z}) \land \forall z \in ℕ (z = y \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{z}))$
75	73 74	bitrdi	$⊢ y \in ℕ \to (\forall z \in ℕ (z < y + 1 \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{z}) \leftrightarrow (\forall z \in ℕ (z < y \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{z}) \land \forall z \in ℕ (z = y \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{z})))$
76	62 75	sylibrd	$⊢ y \in ℕ \to (\forall z \in ℕ (z < y \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{z}) \to \forall z \in ℕ (z < y + 1 \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{z}))$
77	4 7 10 10 13 76	nnind	$⊢ y + 1 \in ℕ \to \forall z \in ℕ (z < y + 1 \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{z})$
78	1 77	syl	$⊢ y \in ℕ \to \forall z \in ℕ (z < y + 1 \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{z})$
79	65	ltp1d	$⊢ y \in ℕ \to y < y + 1$
80		breq1	$⊢ z = y \to (z < y + 1 \leftrightarrow y < y + 1)$
81		df-ne	$⊢ \sqrt{2} \neq \frac{x}{y} \leftrightarrow \neg \sqrt{2} = \frac{x}{y}$
82	58 81	bitrdi	$⊢ z = y \to (\sqrt{2} \neq \frac{x}{z} \leftrightarrow \neg \sqrt{2} = \frac{x}{y})$
83	82	ralbidv	$⊢ z = y \to (\forall x \in ℤ \sqrt{2} \neq \frac{x}{z} \leftrightarrow \forall x \in ℤ \neg \sqrt{2} = \frac{x}{y})$
84		ralnex	$⊢ \forall x \in ℤ \neg \sqrt{2} = \frac{x}{y} \leftrightarrow \neg \exists x \in ℤ \sqrt{2} = \frac{x}{y}$
85	83 84	bitrdi	$⊢ z = y \to (\forall x \in ℤ \sqrt{2} \neq \frac{x}{z} \leftrightarrow \neg \exists x \in ℤ \sqrt{2} = \frac{x}{y})$
86	80 85	imbi12d	$⊢ z = y \to ((z < y + 1 \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{z}) \leftrightarrow (y < y + 1 \to \neg \exists x \in ℤ \sqrt{2} = \frac{x}{y}))$
87	86	rspcv	$⊢ y \in ℕ \to (\forall z \in ℕ (z < y + 1 \to \forall x \in ℤ \sqrt{2} \neq \frac{x}{z}) \to (y < y + 1 \to \neg \exists x \in ℤ \sqrt{2} = \frac{x}{y}))$
88	78 79 87	mp2d	$⊢ y \in ℕ \to \neg \exists x \in ℤ \sqrt{2} = \frac{x}{y}$
89	88	nrex	$⊢ \neg \exists y \in ℕ \exists x \in ℤ \sqrt{2} = \frac{x}{y}$
90		elq	$⊢ \sqrt{2} \in ℚ \leftrightarrow \exists x \in ℤ \exists y \in ℕ \sqrt{2} = \frac{x}{y}$
91		rexcom	$⊢ \exists x \in ℤ \exists y \in ℕ \sqrt{2} = \frac{x}{y} \leftrightarrow \exists y \in ℕ \exists x \in ℤ \sqrt{2} = \frac{x}{y}$
92	90 91	bitri	$⊢ \sqrt{2} \in ℚ \leftrightarrow \exists y \in ℕ \exists x \in ℤ \sqrt{2} = \frac{x}{y}$
93	89 92	mtbir	$⊢ \neg \sqrt{2} \in ℚ$
94	93	nelir	$⊢ \sqrt{2} \notin ℚ$

Metamath Proof Explorer

Theorem sqrt2irr

Proof