pythagtriplem13 - Intuitionistic Logic Explorer

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

Theorem pythagtriplem13 12785

Description: Lemma for pythagtrip 12792. Show that

(which will eventually be closely related to the

in the final statement) is a natural. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)

**Hypothesis**
Ref	Expression
pythagtriplem13.1

**Assertion**
Ref	Expression
pythagtriplem13	$/\$ $/\$ $/\$ $/\$ $/\$

**Proof of Theorem pythagtriplem13**
Step	Hyp	Ref	Expression
1		pythagtriplem13.1	. 2
2		pythagtriplem9 12782	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
3	2	nnzd 9556	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
4		simp3r 1050	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
5		2z 9462	. . . . . . . . . 10
6		simp3 1023	. . . . . . . . . . . . 13 $/\$ $/\$
7		simp2 1022	. . . . . . . . . . . . 13 $/\$ $/\$
8	6, 7	nnaddcld 9146	. . . . . . . . . . . 12 $/\$ $/\$
9	8	nnzd 9556	. . . . . . . . . . 11 $/\$ $/\$
10	9	3ad2ant1 1042	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
11		nnz 9453	. . . . . . . . . . . 12
12	11	3ad2ant1 1042	. . . . . . . . . . 11 $/\$ $/\$
13	12	3ad2ant1 1042	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
14		dvdsgcdb 12520	. . . . . . . . . 10 $/\$ $/\$ $/\$
15	5, 10, 13, 14	mp3an2i 1376	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
16	15	biimpar 297	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
17	16	simprd 114	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
18	4, 17	mtand 669	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
19		pythagtriplem7 12780	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
20	19	breq2d 4094	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
21	18, 20	mtbird 677	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
22		pythagtriplem8 12781	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
23	22	nnzd 9556	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
24		nnz 9453	. . . . . . . . . . . . 13
25	24	3ad2ant3 1044	. . . . . . . . . . . 12 $/\$ $/\$
26		nnz 9453	. . . . . . . . . . . . 13
27	26	3ad2ant2 1043	. . . . . . . . . . . 12 $/\$ $/\$
28	25, 27	zsubcld 9562	. . . . . . . . . . 11 $/\$ $/\$
29	28	3ad2ant1 1042	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
30		dvdsgcdb 12520	. . . . . . . . . 10 $/\$ $/\$ $/\$
31	5, 29, 13, 30	mp3an2i 1376	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
32	31	biimpar 297	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
33	32	simprd 114	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
34	4, 33	mtand 669	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
35		pythagtriplem6 12779	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
36	35	breq2d 4094	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
37	34, 36	mtbird 677	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
38		omoe 12393	. . . . 5 $/\$ $/\$ $/\$
39	3, 21, 23, 37, 38	syl22anc 1272	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
40	28	zred 9557	. . . . . . . . . 10 $/\$ $/\$
41	40	3ad2ant1 1042	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
42		simp13 1053	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
43	42	nnred 9111	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
44	8	nnred 9111	. . . . . . . . . 10 $/\$ $/\$
45	44	3ad2ant1 1042	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
46		nnrp 9847	. . . . . . . . . . . 12
47	46	3ad2ant2 1043	. . . . . . . . . . 11 $/\$ $/\$
48	47	3ad2ant1 1042	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
49	43, 48	ltsubrpd 9913	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
50		nngt0 9123	. . . . . . . . . . . 12
51	50	3ad2ant2 1043	. . . . . . . . . . 11 $/\$ $/\$
52	51	3ad2ant1 1042	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
53		simp12 1052	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
54	53	nnred 9111	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
55	54, 43	ltaddposd 8664	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
56	52, 55	mpbid 147	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
57	41, 43, 45, 49, 56	lttrd 8260	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
58		pythagtriplem10 12778	. . . . . . . . . . 11 $/\$ $/\$ $/\$
59	58	3adant3 1041	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
60		0re 8134	. . . . . . . . . . 11
61		ltle 8222	. . . . . . . . . . 11 $/\$
62	60, 61	mpan 424	. . . . . . . . . 10
63	41, 59, 62	sylc 62	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
64		nngt0 9123	. . . . . . . . . . . . 13
65	64	3ad2ant3 1044	. . . . . . . . . . . 12 $/\$ $/\$
66	65	3ad2ant1 1042	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
67	43, 54, 66, 52	addgt0d 8656	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
68		ltle 8222	. . . . . . . . . . 11 $/\$
69	60, 68	mpan 424	. . . . . . . . . 10
70	45, 67, 69	sylc 62	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
71	41, 63, 45, 70	sqrtltd 11669	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
72	57, 71	mpbid 147	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
73		nnsub 9137	. . . . . . . 8 $/\$
74	22, 2, 73	syl2anc 411	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
75	72, 74	mpbid 147	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
76	75	nnzd 9556	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
77		evend2 12386	. . . . 5
78	76, 77	syl 14	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
79	39, 78	mpbid 147	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
80	75	nngt0d 9142	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
81	75	nnred 9111	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
82		halfpos2 9329	. . . . 5
83	81, 82	syl 14	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
84	80, 83	mpbid 147	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
85		elnnz 9444	. . 3 $/\$
86	79, 84, 85	sylanbrc 417	. 2 $/\$ $/\$ $/\$ $/\$ $/\$
87	1, 86	eqeltrid 2316	1 $/\$ $/\$ $/\$ $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 104

wb 105 $/\$ w3a 1002

wceq 1395

wcel 2200 class class class wbr 4082

cfv 5314 (class class class)co 5994

cr 7986

cc0 7987

c1 7988

caddc 7990

clt 8169

cle 8170

cmin 8305

cdiv 8807

cn 9098

c2 9149

cz 9434

crp 9837

cexp 10747

csqrt 11493

cdvds 12284

cgcd 12460

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 617 ax-in2 618 ax-io 714 ax-5 1493 ax-7 1494 ax-gen 1495 ax-ie1 1539 ax-ie2 1540 ax-8 1550 ax-10 1551 ax-11 1552 ax-i12 1553 ax-bndl 1555 ax-4 1556 ax-17 1572 ax-i9 1576 ax-ial 1580 ax-i5r 1581 ax-13 2202 ax-14 2203 ax-ext 2211 ax-coll 4198 ax-sep 4201 ax-nul 4209 ax-pow 4257 ax-pr 4292 ax-un 4521 ax-setind 4626 ax-iinf 4677 ax-cnex 8078 ax-resscn 8079 ax-1cn 8080 ax-1re 8081 ax-icn 8082 ax-addcl 8083 ax-addrcl 8084 ax-mulcl 8085 ax-mulrcl 8086 ax-addcom 8087 ax-mulcom 8088 ax-addass 8089 ax-mulass 8090 ax-distr 8091 ax-i2m1 8092 ax-0lt1 8093 ax-1rid 8094 ax-0id 8095 ax-rnegex 8096 ax-precex 8097 ax-cnre 8098 ax-pre-ltirr 8099 ax-pre-ltwlin 8100 ax-pre-lttrn 8101 ax-pre-apti 8102 ax-pre-ltadd 8103 ax-pre-mulgt0 8104 ax-pre-mulext 8105 ax-arch 8106 ax-caucvg 8107

This theorem depends on definitions: df-bi 117 df-stab 836 df-dc 840 df-3or 1003 df-3an 1004 df-tru 1398 df-fal 1401 df-xor 1418 df-nf 1507 df-sb 1809 df-eu 2080 df-mo 2081 df-clab 2216 df-cleq 2222 df-clel 2225 df-nfc 2361 df-ne 2401 df-nel 2496 df-ral 2513 df-rex 2514 df-reu 2515 df-rmo 2516 df-rab 2517 df-v 2801 df-sbc 3029 df-csb 3125 df-dif 3199 df-un 3201 df-in 3203 df-ss 3210 df-nul 3492 df-if 3603 df-pw 3651 df-sn 3672 df-pr 3673 df-op 3675 df-uni 3888 df-int 3923 df-iun 3966 df-br 4083 df-opab 4145 df-mpt 4146 df-tr 4182 df-id 4381 df-po 4384 df-iso 4385 df-iord 4454 df-on 4456 df-ilim 4457 df-suc 4459 df-iom 4680 df-xp 4722 df-rel 4723 df-cnv 4724 df-co 4725 df-dm 4726 df-rn 4727 df-res 4728 df-ima 4729 df-iota 5274 df-fun 5316 df-fn 5317 df-f 5318 df-f1 5319 df-fo 5320 df-f1o 5321 df-fv 5322 df-riota 5947 df-ov 5997 df-oprab 5998 df-mpo 5999 df-1st 6276 df-2nd 6277 df-recs 6441 df-frec 6527 df-1o 6552 df-2o 6553 df-er 6670 df-en 6878 df-sup 7139 df-pnf 8171 df-mnf 8172 df-xr 8173 df-ltxr 8174 df-le 8175 df-sub 8307 df-neg 8308 df-reap 8710 df-ap 8717 df-div 8808 df-inn 9099 df-2 9157 df-3 9158 df-4 9159 df-n0 9358 df-z 9435 df-uz 9711 df-q 9803 df-rp 9838 df-fz 10193 df-fzo 10327 df-fl 10477 df-mod 10532 df-seqfrec 10657 df-exp 10748 df-cj 11339 df-re 11340 df-im 11341 df-rsqrt 11495 df-abs 11496 df-dvds 12285 df-gcd 12461 df-prm 12616

This theorem is referenced by: pythagtriplem18 12790

W3C validator