Theorem sqr2irrlem3 6607

Description: Main theorem for irrationality of square root of 2. There are no natural numbers such that the square of one is twice the square of the other. Uses strong induction.

Assertion

Ref	Expression
sqr2irrlem3	|- -. E.x e. NN E.y e. NN (x^2) = (2 x. (y^2))

Distinct variable group:   x,y

Proof of Theorem sqr2irrlem3

Step	Hyp	Ref	Expression
1		opreq1 3907	. . . . . . . 8 |- (x = z -> (x^2) = (z^2))
2	1	eqeq1d 1459	. . . . . . 7 |- (x = z -> ((x^2) = (2 x. (y^2)) <-> (z^2) = (2 x. (y^2))))
3	2	negbid 609	. . . . . 6 |- (x = z -> (-. (x^2) = (2 x. (y^2)) <-> -. (z^2) = (2 x. (y^2))))
4	3	ralbidv 1639	. . . . 5 |- (x = z -> (A.y e. NN -. (x^2) = (2 x. (y^2)) <-> A.y e. NN -. (z^2) = (2 x. (y^2))))
5		opreq1 3907	. . . . . . . . 9 |- (y = w -> (y^2) = (w^2))
6	5	opreq2d 3915	. . . . . . . 8 |- (y = w -> (2 x. (y^2)) = (2 x. (w^2)))
7	6	eqeq2d 1462	. . . . . . 7 |- (y = w -> ((z^2) = (2 x. (y^2)) <-> (z^2) = (2 x. (w^2))))
8	7	negbid 609	. . . . . 6 |- (y = w -> (-. (z^2) = (2 x. (y^2)) <-> -. (z^2) = (2 x. (w^2))))
9	8	cbvralv 1775	. . . . 5 |- (A.y e. NN -. (z^2) = (2 x. (y^2)) <-> A.w e. NN -. (z^2) = (2 x. (w^2)))
10	4, 9	syl6bb 534	. . . 4 |- (x = z -> (A.y e. NN -. (x^2) = (2 x. (y^2)) <-> A.w e. NN -. (z^2) = (2 x. (w^2))))
11		breq1 2590	. . . . . . . . . . . . 13 |- (z = y -> (z < x <-> y < x))
12		opreq1 3907	. . . . . . . . . . . . . . . 16 |- (z = y -> (z^2) = (y^2))
13	12	eqeq1d 1459	. . . . . . . . . . . . . . 15 |- (z = y -> ((z^2) = (2 x. (w^2)) <-> (y^2) = (2 x. (w^2))))
14	13	negbid 609	. . . . . . . . . . . . . 14 |- (z = y -> (-. (z^2) = (2 x. (w^2)) <-> -. (y^2) = (2 x. (w^2))))
15	14	ralbidv 1639	. . . . . . . . . . . . 13 |- (z = y -> (A.w e. NN -. (z^2) = (2 x. (w^2)) <-> A.w e. NN -. (y^2) = (2 x. (w^2))))
16	11, 15	imbi12d 624	. . . . . . . . . . . 12 |- (z = y -> ((z < x -> A.w e. NN -. (z^2) = (2 x. (w^2))) <-> (y < x -> A.w e. NN -. (y^2) = (2 x. (w^2)))))
17	16	rcla4cva 1849	. . . . . . . . . . 11 |- ((A.z e. NN (z < x -> A.w e. NN -. (z^2) = (2 x. (w^2))) /\ y e. NN) -> (y < x -> A.w e. NN -. (y^2) = (2 x. (w^2))))
18		opreq1 3907	. . . . . . . . . . . . . . 15 |- (w = (x / 2) -> (w^2) = ((x / 2)^2))
19	18	opreq2d 3915	. . . . . . . . . . . . . 14 |- (w = (x / 2) -> (2 x. (w^2)) = (2 x. ((x / 2)^2)))
20	19	eqeq2d 1462	. . . . . . . . . . . . 13 |- (w = (x / 2) -> ((y^2) = (2 x. (w^2)) <-> (y^2) = (2 x. ((x / 2)^2))))
21	20	negbid 609	. . . . . . . . . . . 12 |- (w = (x / 2) -> (-. (y^2) = (2 x. (w^2)) <-> -. (y^2) = (2 x. ((x / 2)^2))))
22	21	rcla4cv 1847	. . . . . . . . . . 11 |- (A.w e. NN -. (y^2) = (2 x. (w^2)) -> ((x / 2) e. NN -> -. (y^2) = (2 x. ((x / 2)^2))))
23	17, 22	syl6 22	. . . . . . . . . 10 |- ((A.z e. NN (z < x -> A.w e. NN -. (z^2) = (2 x. (w^2))) /\ y e. NN) -> (y < x -> ((x / 2) e. NN -> -. (y^2) = (2 x. ((x / 2)^2)))))
24	23	imp3a 361	. . . . . . . . 9 |- ((A.z e. NN (z < x -> A.w e. NN -. (z^2) = (2 x. (w^2))) /\ y e. NN) -> ((y < x /\ (x / 2) e. NN) -> -. (y^2) = (2 x. ((x / 2)^2))))
25		imnan 242	. . . . . . . . 9 |- (((y < x /\ (x / 2) e. NN) -> -. (y^2) = (2 x. ((x / 2)^2))) <-> -. ((y < x /\ (x / 2) e. NN) /\ (y^2) = (2 x. ((x / 2)^2))))
26	24, 25	sylib 198	. . . . . . . 8 |- ((A.z e. NN (z < x -> A.w e. NN -. (z^2) = (2 x. (w^2))) /\ y e. NN) -> -. ((y < x /\ (x / 2) e. NN) /\ (y^2) = (2 x. ((x / 2)^2))))
27	26	adantll 392	. . . . . . 7 |- (((x e. NN /\ A.z e. NN (z < x -> A.w e. NN -. (z^2) = (2 x. (w^2)))) /\ y e. NN) -> -. ((y < x /\ (x / 2) e. NN) /\ (y^2) = (2 x. ((x / 2)^2))))
28		sqr2irrlem2 6606	. . . . . . . 8 |- ((x e. NN /\ y e. NN) -> ((x^2) = (2 x. (y^2)) -> ((y < x /\ (x / 2) e. NN) /\ (y^2) = (2 x. ((x / 2)^2)))))
29	28	adantlr 393	. . . . . . 7 |- (((x e. NN /\ A.z e. NN (z < x -> A.w e. NN -. (z^2) = (2 x. (w^2)))) /\ y e. NN) -> ((x^2) = (2 x. (y^2)) -> ((y < x /\ (x / 2) e. NN) /\ (y^2) = (2 x. ((x / 2)^2)))))
30	27, 29	mtod 108	. . . . . 6 |- (((x e. NN /\ A.z e. NN (z < x -> A.w e. NN -. (z^2) = (2 x. (w^2)))) /\ y e. NN) -> -. (x^2) = (2 x. (y^2)))
31	30	exp31 376	. . . . 5 |- (x e. NN -> (A.z e. NN (z < x -> A.w e. NN -. (z^2) = (2 x. (w^2))) -> (y e. NN -> -. (x^2) = (2 x. (y^2)))))
32	31	r19.21adv 1694	. . . 4 |- (x e. NN -> (A.z e. NN (z < x -> A.w e. NN -. (z^2) = (2 x. (w^2))) -> A.y e. NN -. (x^2) = (2 x. (y^2))))
33	10, 32	indstr 6344	. . 3 |- (x e. NN -> A.y e. NN -. (x^2) = (2 x. (y^2)))
34		ralnex 1629	. . 3 |- (A.y e. NN -. (x^2) = (2 x. (y^2)) <-> -. E.y e. NN (x^2) = (2 x. (y^2)))
35	33, 34	sylib 198	. 2 |- (x e. NN -> -. E.y e. NN (x^2) = (2 x. (y^2)))
36	35	nrex 1705	1 |- -. E.x e. NN E.y e. NN (x^2) = (2 x. (y^2))

Syntax hints:  -. wn 2   -> wi 3   /\ wa 223   = wceq 1099   e. wcel 1105  A.wral 1621  E.wrex 1622   class class class wbr 2587  (class class class)co 3902   x. cmul 5162   / cdiv 5217  NNcn 5219   < clt 5409  2c2 5859  ^cexp 6451

This theorem is referenced by:  sqr2irr 6610

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-13 1107  ax-14 1108  ax-11 1180  ax-17 1190  ax-16 1194  ax-11o 1202  ax-ext 1436  ax-rep 2661  ax-sep 2671  ax-nul 2678  ax-pow 2710  ax-pr 2747  ax-un 2830  ax-inf2 4549

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 773  df-3an 774  df-ex 957  df-sb 1155  df-eu 1359  df-mo 1360  df-clab 1441  df-cleq 1446  df-clel 1449  df-ne 1563  df-nel 1564  df-ral 1625  df-rex 1626  df-reu 1627  df-rab 1628  df-v 1787  df-sbc 1913  df-csb 1973  df-dif 2020  df-un 2021  df-in 2022  df-ss 2024  df-pss 2026  df-nul 2252  df-if 2333  df-pw 2373  df-sn 2383  df-pr 2384  df-tp 2386  df-op 2387  df-uni 2472  df-int 2502  df-iun 2536  df-br 2588  df-opab 2635  df-tr 2649  df-eprel 2794  df-id 2797  df-po 2804  df-so 2814  df-fr 2880  df-we 2897  df-ord 2914  df-on 2915  df-lim 2916  df-suc 2917  df-om 3095  df-xp 3147  df-rel 3148  df-cnv 3149  df-co 3150  df-dm 3151  df-rn 3152  df-res 3153  df-ima 3154  df-fun 3155  df-fn 3156  df-f 3157  df-f1 3158  df-fo 3159  df-f1o 3160  df-fv 3161  df-rdg 3871  df-opr 3904  df-oprab 3905  df-1st 4017  df-2nd 4018  df-1o 4071  df-oadd 4073  df-omul 4074  df-er 4199  df-ec 4201  df-qs 4204  df-en 4305  df-dom 4306  df-sdom 4307  df-ni 4923  df-pli 4924  df-mi 4925  df-lti 4926  df-plpq 4958  df-mpq 4959  df-enq 4960  df-nq 4961  df-plq 4962  df-mq 4963  df-rq 4964  df-ltq 4965  df-1q 4966  df-np 5009  df-1p 5010  df-plp 5011  df-mp 5012  df-ltp 5013  df-plpr 5087  df-mpr 5088  df-enr 5089  df-nr 5090  df-plr 5091  df-mr 5092  df-ltr 5093  df-0r 5094  df-1r 5095  df-m1r 5096  df-c 5163  df-0 5164  df-1 5165  df-i 5166  df-r 5167  df-plus 5168  df-mul 5169  df-lt 5170  df-sub 5279  df-neg 5281  df-pnf 5410  df-mnf 5411  df-xr 5412  df-ltxr 5413  df-le 5414  df-div 5623  df-n 5824  df-2 5868  df-n0 5998  df-z 6034  df-seq1 6196  df-uz 6301  df-exp 6452

Copyright terms: Public domain