sqrt2irr - Intuitionistic Logic Explorer

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

Theorem sqrt2irr 11686

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 11703 for the proof that the square root of two is irrational.

The proof's core is proven in sqrt2irrlem 11685, 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 8642	. . . . . 6
2		breq2 3899	. . . . . . . . 9
3	2	imbi1d 230	. . . . . . . 8
4	3	ralbidv 2411	. . . . . . 7
5		breq2 3899	. . . . . . . . 9
6	5	imbi1d 230	. . . . . . . 8
7	6	ralbidv 2411	. . . . . . 7
8		breq2 3899	. . . . . . . . 9
9	8	imbi1d 230	. . . . . . . 8
10	9	ralbidv 2411	. . . . . . 7
11		nnnlt1 8656	. . . . . . . . 9
12	11	pm2.21d 591	. . . . . . . 8
13	12	rgen 2459	. . . . . . 7
14		nnrp 9352	. . . . . . . . . . . . . 14
15		rphalflt 9372	. . . . . . . . . . . . . 14
16	14, 15	syl 14	. . . . . . . . . . . . 13
17		breq1 3898	. . . . . . . . . . . . . . . 16
18		oveq2 5736	. . . . . . . . . . . . . . . . . 18
19	18	neeq2d 2301	. . . . . . . . . . . . . . . . 17
20	19	ralbidv 2411	. . . . . . . . . . . . . . . 16
21	17, 20	imbi12d 233	. . . . . . . . . . . . . . 15
22	21	rspcv 2756	. . . . . . . . . . . . . 14
23	22	com13 80	. . . . . . . . . . . . 13
24	16, 23	syl 14	. . . . . . . . . . . 12
25		simpr 109	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
26		zcn 8963	. . . . . . . . . . . . . . . . . . 19
27	26	ad2antlr 478	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
28		nncn 8638	. . . . . . . . . . . . . . . . . . 19
29	28	ad2antrr 477	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
30		2cnd 8703	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
31		nnap0 8659	. . . . . . . . . . . . . . . . . . 19 #
32	31	ad2antrr 477	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ #
33		2ap0 8723	. . . . . . . . . . . . . . . . . . 19 #
34	33	a1i 9	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ #
35	27, 29, 30, 32, 34	divcanap7d 8492	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
36	25, 35	eqtr4d 2150	. . . . . . . . . . . . . . . 16 $/\$ $/\$
37		simplr 502	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
38		simpll 501	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
39	37, 38, 25	sqrt2irrlem 11685	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
40	39	simprd 113	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
41	39	simpld 111	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
42		oveq1 5735	. . . . . . . . . . . . . . . . . . . . 21
43	42	neeq2d 2301	. . . . . . . . . . . . . . . . . . . 20
44	43	rspcv 2756	. . . . . . . . . . . . . . . . . . 19
45	41, 44	syl 14	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
46	40, 45	embantd 56	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
47	46	necon2bd 2340	. . . . . . . . . . . . . . . 16 $/\$ $/\$
48	36, 47	mpd 13	. . . . . . . . . . . . . . 15 $/\$ $/\$
49	48	ex 114	. . . . . . . . . . . . . 14 $/\$
50	49	necon2ad 2339	. . . . . . . . . . . . 13 $/\$
51	50	ralrimdva 2486	. . . . . . . . . . . 12
52	24, 51	syld 45	. . . . . . . . . . 11
53		oveq1 5735	. . . . . . . . . . . . 13
54	53	neeq2d 2301	. . . . . . . . . . . 12
55	54	cbvralv 2628	. . . . . . . . . . 11
56	52, 55	syl6ibr 161	. . . . . . . . . 10
57		oveq2 5736	. . . . . . . . . . . . 13
58	57	neeq2d 2301	. . . . . . . . . . . 12
59	58	ralbidv 2411	. . . . . . . . . . 11
60	59	ceqsralv 2688	. . . . . . . . . 10
61	56, 60	sylibrd 168	. . . . . . . . 9
62	61	ancld 321	. . . . . . . 8 $/\$
63		nnleltp1 9017	. . . . . . . . . . . . . 14 $/\$
64		nnz 8977	. . . . . . . . . . . . . . 15
65		nnz 8977	. . . . . . . . . . . . . . 15
66		zleloe 9005	. . . . . . . . . . . . . . 15 $/\$ $\/$
67	64, 65, 66	syl2an 285	. . . . . . . . . . . . . 14 $/\$ $\/$
68	63, 67	bitr3d 189	. . . . . . . . . . . . 13 $/\$ $\/$
69	68	ancoms 266	. . . . . . . . . . . 12 $/\$ $\/$
70	69	imbi1d 230	. . . . . . . . . . 11 $/\$ $\/$
71		jaob 682	. . . . . . . . . . 11 $\/$ $/\$
72	70, 71	syl6bb 195	. . . . . . . . . 10 $/\$ $/\$
73	72	ralbidva 2407	. . . . . . . . 9 $/\$
74		r19.26 2532	. . . . . . . . 9 $/\$ $/\$
75	73, 74	syl6bb 195	. . . . . . . 8 $/\$
76	62, 75	sylibrd 168	. . . . . . 7
77	4, 7, 10, 10, 13, 76	nnind 8646	. . . . . 6
78	1, 77	syl 14	. . . . 5
79		nnre 8637	. . . . . 6
80	79	ltp1d 8598	. . . . 5
81		breq1 3898	. . . . . . 7
82		df-ne 2283	. . . . . . . . . 10
83	58, 82	syl6bb 195	. . . . . . . . 9
84	83	ralbidv 2411	. . . . . . . 8
85		ralnex 2400	. . . . . . . 8
86	84, 85	syl6bb 195	. . . . . . 7
87	81, 86	imbi12d 233	. . . . . 6
88	87	rspcv 2756	. . . . 5
89	78, 80, 88	mp2d 47	. . . 4
90	89	nrex 2498	. . 3
91		elq 9316	. . . 4
92		rexcom 2569	. . . 4
93	91, 92	bitri 183	. . 3
94	90, 93	mtbir 643	. 2
95	94	nelir 2380	1

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 103

wb 104 $\/$ wo 680

wceq 1314

wcel 1463

wne 2282

wnel 2377

wral 2390

wrex 2391 class class class wbr 3895

cfv 5081 (class class class)co 5728

cc 7545

cc0 7547

c1 7548

caddc 7550

clt 7724

cle 7725 # cap 8261

cdiv 8345

cn 8630

c2 8681

cz 8958

cq 9313

crp 9343

csqrt 10660

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 586 ax-in2 587 ax-io 681 ax-5 1406 ax-7 1407 ax-gen 1408 ax-ie1 1452 ax-ie2 1453 ax-8 1465 ax-10 1466 ax-11 1467 ax-i12 1468 ax-bndl 1469 ax-4 1470 ax-13 1474 ax-14 1475 ax-17 1489 ax-i9 1493 ax-ial 1497 ax-i5r 1498 ax-ext 2097 ax-coll 4003 ax-sep 4006 ax-nul 4014 ax-pow 4058 ax-pr 4091 ax-un 4315 ax-setind 4412 ax-iinf 4462 ax-cnex 7636 ax-resscn 7637 ax-1cn 7638 ax-1re 7639 ax-icn 7640 ax-addcl 7641 ax-addrcl 7642 ax-mulcl 7643 ax-mulrcl 7644 ax-addcom 7645 ax-mulcom 7646 ax-addass 7647 ax-mulass 7648 ax-distr 7649 ax-i2m1 7650 ax-0lt1 7651 ax-1rid 7652 ax-0id 7653 ax-rnegex 7654 ax-precex 7655 ax-cnre 7656 ax-pre-ltirr 7657 ax-pre-ltwlin 7658 ax-pre-lttrn 7659 ax-pre-apti 7660 ax-pre-ltadd 7661 ax-pre-mulgt0 7662 ax-pre-mulext 7663 ax-arch 7664 ax-caucvg 7665

This theorem depends on definitions: df-bi 116 df-dc 803 df-3or 946 df-3an 947 df-tru 1317 df-fal 1320 df-nf 1420 df-sb 1719 df-eu 1978 df-mo 1979 df-clab 2102 df-cleq 2108 df-clel 2111 df-nfc 2244 df-ne 2283 df-nel 2378 df-ral 2395 df-rex 2396 df-reu 2397 df-rmo 2398 df-rab 2399 df-v 2659 df-sbc 2879 df-csb 2972 df-dif 3039 df-un 3041 df-in 3043 df-ss 3050 df-nul 3330 df-if 3441 df-pw 3478 df-sn 3499 df-pr 3500 df-op 3502 df-uni 3703 df-int 3738 df-iun 3781 df-br 3896 df-opab 3950 df-mpt 3951 df-tr 3987 df-id 4175 df-po 4178 df-iso 4179 df-iord 4248 df-on 4250 df-ilim 4251 df-suc 4253 df-iom 4465 df-xp 4505 df-rel 4506 df-cnv 4507 df-co 4508 df-dm 4509 df-rn 4510 df-res 4511 df-ima 4512 df-iota 5046 df-fun 5083 df-fn 5084 df-f 5085 df-f1 5086 df-fo 5087 df-f1o 5088 df-fv 5089 df-riota 5684 df-ov 5731 df-oprab 5732 df-mpo 5733 df-1st 5992 df-2nd 5993 df-recs 6156 df-frec 6242 df-pnf 7726 df-mnf 7727 df-xr 7728 df-ltxr 7729 df-le 7730 df-sub 7858 df-neg 7859 df-reap 8255 df-ap 8262 df-div 8346 df-inn 8631 df-2 8689 df-3 8690 df-4 8691 df-n0 8882 df-z 8959 df-uz 9229 df-q 9314 df-rp 9344 df-seqfrec 10112 df-exp 10186 df-rsqrt 10662

This theorem is referenced by: (None)

W3C validator