sqrt2irr - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > sqrt2irr		Unicode version

Theorem sqrt2irr 12965

Description: The square root of 2 is not rational. That is, for any rational number,

does not equal it. However, if we were to say "the square root of 2 is irrational" that would mean something stronger: "for any rational number,

is apart from it" (the two statements are equivalent given excluded middle). See sqrt2irrap 12984 for the proof that the square root of two is irrational.

The proof's core is proven in sqrt2irrlem 12964, which shows that if , then and are even, so and are smaller representatives, which is absurd. (Contributed by NM, 8-Jan-2002.) (Proof shortened by Mario Carneiro, 12-Sep-2015.)

**Assertion**
Ref	Expression
sqrt2irr

Proof of Theorem sqrt2irr Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		peano2nn 9325	. . . . . 6
2		breq2 4135	. . . . . . . . 9
3	2	imbi1d 231	. . . . . . . 8
4	3	ralbidv 2550	. . . . . . 7
5		breq2 4135	. . . . . . . . 9
6	5	imbi1d 231	. . . . . . . 8
7	6	ralbidv 2550	. . . . . . 7
8		breq2 4135	. . . . . . . . 9
9	8	imbi1d 231	. . . . . . . 8
10	9	ralbidv 2550	. . . . . . 7
11		nnnlt1 9339	. . . . . . . . 9
12	11	pm2.21d 628	. . . . . . . 8
13	12	rgen 2603	. . . . . . 7
14		nnrp 10080	. . . . . . . . . . . . . 14
15		rphalflt 10100	. . . . . . . . . . . . . 14
16	14, 15	syl 14	. . . . . . . . . . . . 13
17		breq1 4134	. . . . . . . . . . . . . . . 16
18		oveq2 6096	. . . . . . . . . . . . . . . . . 18
19	18	neeq2d 2439	. . . . . . . . . . . . . . . . 17
20	19	ralbidv 2550	. . . . . . . . . . . . . . . 16
21	17, 20	imbi12d 234	. . . . . . . . . . . . . . 15
22	21	rspcv 2925	. . . . . . . . . . . . . 14
23	22	com13 80	. . . . . . . . . . . . 13
24	16, 23	syl 14	. . . . . . . . . . . 12
25		simpr 110	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
26		zcn 9658	. . . . . . . . . . . . . . . . . . 19
27	26	ad2antlr 493	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
28		nncn 9321	. . . . . . . . . . . . . . . . . . 19
29	28	ad2antrr 492	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
30		2cnd 9386	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
31		nnap0 9342	. . . . . . . . . . . . . . . . . . 19 #
32	31	ad2antrr 492	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ #
33		2ap0 9406	. . . . . . . . . . . . . . . . . . 19 #
34	33	a1i 9	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ #
35	27, 29, 30, 32, 34	divcanap7d 9157	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
36	25, 35	eqtr4d 2274	. . . . . . . . . . . . . . . 16 $/\$ $/\$
37		simplr 533	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
38		simpll 531	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
39	37, 38, 25	sqrt2irrlem 12964	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
40	39	simprd 114	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
41	39	simpld 112	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
42		oveq1 6095	. . . . . . . . . . . . . . . . . . . . 21
43	42	neeq2d 2439	. . . . . . . . . . . . . . . . . . . 20
44	43	rspcv 2925	. . . . . . . . . . . . . . . . . . 19
45	41, 44	syl 14	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
46	40, 45	embantd 56	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
47	46	necon2bd 2478	. . . . . . . . . . . . . . . 16 $/\$ $/\$
48	36, 47	mpd 13	. . . . . . . . . . . . . . 15 $/\$ $/\$
49	48	ex 115	. . . . . . . . . . . . . 14 $/\$
50	49	necon2ad 2477	. . . . . . . . . . . . 13 $/\$
51	50	ralrimdva 2630	. . . . . . . . . . . 12
52	24, 51	syld 45	. . . . . . . . . . 11
53		oveq1 6095	. . . . . . . . . . . . 13
54	53	neeq2d 2439	. . . . . . . . . . . 12
55	54	cbvralv 2786	. . . . . . . . . . 11
56	52, 55	imbitrrdi 162	. . . . . . . . . 10
57		oveq2 6096	. . . . . . . . . . . . 13
58	57	neeq2d 2439	. . . . . . . . . . . 12
59	58	ralbidv 2550	. . . . . . . . . . 11
60	59	ceqsralv 2853	. . . . . . . . . 10
61	56, 60	sylibrd 169	. . . . . . . . 9
62	61	ancld 325	. . . . . . . 8 $/\$
63		nnleltp1 9713	. . . . . . . . . . . . . 14 $/\$
64		nnz 9672	. . . . . . . . . . . . . . 15
65		nnz 9672	. . . . . . . . . . . . . . 15
66		zleloe 9700	. . . . . . . . . . . . . . 15 $/\$ $\/$
67	64, 65, 66	syl2an 289	. . . . . . . . . . . . . 14 $/\$ $\/$
68	63, 67	bitr3d 190	. . . . . . . . . . . . 13 $/\$ $\/$
69	68	ancoms 268	. . . . . . . . . . . 12 $/\$ $\/$
70	69	imbi1d 231	. . . . . . . . . . 11 $/\$ $\/$
71		jaob 722	. . . . . . . . . . 11 $\/$ $/\$
72	70, 71	bitrdi 196	. . . . . . . . . 10 $/\$ $/\$
73	72	ralbidva 2546	. . . . . . . . 9 $/\$
74		r19.26 2677	. . . . . . . . 9 $/\$ $/\$
75	73, 74	bitrdi 196	. . . . . . . 8 $/\$
76	62, 75	sylibrd 169	. . . . . . 7
77	4, 7, 10, 10, 13, 76	nnind 9329	. . . . . 6
78	1, 77	syl 14	. . . . 5
79		nnre 9320	. . . . . 6
80	79	ltp1d 9268	. . . . 5
81		breq1 4134	. . . . . . 7
82		df-ne 2421	. . . . . . . . . 10
83	58, 82	bitrdi 196	. . . . . . . . 9
84	83	ralbidv 2550	. . . . . . . 8
85		ralnex 2538	. . . . . . . 8
86	84, 85	bitrdi 196	. . . . . . 7
87	81, 86	imbi12d 234	. . . . . 6
88	87	rspcv 2925	. . . . 5
89	78, 80, 88	mp2d 47	. . . 4
90	89	nrex 2642	. . 3
91		elq 10037	. . . 4
92		rexcom 2715	. . . 4
93	91, 92	bitri 184	. . 3
94	90, 93	mtbir 682	. 2
95	94	nelir 2518	1

Colors of variables: wff set class

This proof depends on syntax axioms:

wn 3

wi 4 $/\$ wa 104

wb 105 $\/$ wo 720

wceq 1402

wcel 2209

wne 2420

wnel 2515

wral 2528

wrex 2529 class class class wbr 4131

cfv 5380 (class class class)co 6088

cc 8183

cc0 8185

c1 8186

caddc 8188

clt 8366

cle 8367 # cap 8917

cdiv 9010

cn 9313

c2 9364

cz 9653

cq 10034

crp 10070

csqrt 11783

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 623 ax-in2 624 ax-io 721 ax-5 1500 ax-7 1501 ax-gen 1502 ax-ie1 1546 ax-ie2 1547 ax-8 1557 ax-10 1558 ax-11 1559 ax-i12 1560 ax-bndl 1562 ax-4 1563 ax-17 1579 ax-i9 1583 ax-ial 1587 ax-i5r 1588 ax-14 2212 ax-ext 2220 ax-coll 4248 ax-sep 4251 ax-nul 4261 ax-pow 4313 ax-pr 4348 ax-un 4580 ax-setind 4686 ax-iinf 4737 ax-cnex 8276 ax-resscn 8277 ax-1cn 8278 ax-1re 8279 ax-icn 8280 ax-addcl 8281 ax-addrcl 8282 ax-mulcl 8283 ax-mulrcl 8284 ax-addcom 8285 ax-mulcom 8286 ax-addass 8287 ax-mulass 8288 ax-distr 8289 ax-i2m1 8290 ax-0lt1 8291 ax-1rid 8292 ax-0id 8293 ax-rnegex 8294 ax-precex 8295 ax-cnre 8296 ax-pre-ltirr 8297 ax-pre-ltwlin 8298 ax-pre-lttrn 8299 ax-pre-apti 8300 ax-pre-ltadd 8301 ax-pre-mulgt0 8302 ax-pre-mulext 8303 ax-arch 8304 ax-caucvg 8305

This proof depends on definitions: df-bi 117 df-dc 847 df-3or 1010 df-3an 1011 df-tru 1405 df-fal 1408 df-nf 1514 df-sb 1816 df-eu 2089 df-mo 2090 df-clab 2225 df-cleq 2231 df-clel 2234 df-nfc 2381 df-ne 2421 df-nel 2516 df-ral 2533 df-rex 2534 df-reu 2535 df-rmo 2536 df-rab 2537 df-v 2823 df-sbc 3052 df-csb 3148 df-dif 3222 df-un 3224 df-in 3226 df-ss 3233 df-nul 3521 df-if 3639 df-pw 3690 df-sn 3715 df-pr 3716 df-op 3718 df-uni 3936 df-int 3971 df-iun 4014 df-br 4132 df-opab 4194 df-mpt 4195 df-tr 4232 df-id 4440 df-po 4443 df-iso 4444 df-iord 4513 df-on 4515 df-ilim 4516 df-suc 4518 df-iom 4740 df-xp 4782 df-rel 4783 df-cnv 4784 df-co 4785 df-dm 4786 df-rn 4787 df-res 4788 df-ima 4789 df-iota 5340 df-fun 5382 df-fn 5383 df-f 5384 df-f1 5385 df-fo 5386 df-f1o 5387 df-fv 5388 df-riota 6041 df-ov 6091 df-oprab 6092 df-mpo 6093 df-1st 6378 df-2nd 6379 df-recs 6581 df-frec 6667 df-pnf 8368 df-mnf 8369 df-xr 8370 df-ltxr 8371 df-le 8372 df-sub 8506 df-neg 8507 df-reap 8911 df-ap 8918 df-div 9011 df-inn 9314 df-2 9372 df-3 9373 df-4 9374 df-n0 9575 df-z 9654 df-uz 9937 df-q 10035 df-rp 10071 df-seqfrec 10905 df-exp 10996 df-rsqrt 11785

This theorem is used by: sqrt2irr0 12967

W3C validator