pythagtriplem14 - Intuitionistic Logic Explorer

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

Theorem pythagtriplem14 12786

Description: Lemma for pythagtrip 12792. Calculate the square of

. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)

**Hypothesis**
Ref	Expression
pythagtriplem13.1

**Assertion**
Ref	Expression
pythagtriplem14	$/\$ $/\$ $/\$ $/\$ $/\$

**Proof of Theorem pythagtriplem14**
Step	Hyp	Ref	Expression
1		pythagtriplem13.1	. . 3
2	1	oveq1i 6004	. 2
3		simp13 1053	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
4		simp12 1052	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
5	3, 4	nnaddcld 9146	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
6	5	nnrpd 9878	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
7	6	rpsqrtcld 11655	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
8	7	rpcnd 9882	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
9	3	nnred 9111	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
10	4	nnred 9111	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
11	9, 10	resubcld 8515	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
12		pythagtriplem10 12778	. . . . . . . . 9 $/\$ $/\$ $/\$
13	12	3adant3 1041	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
14	11, 13	elrpd 9877	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
15	14	rpsqrtcld 11655	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
16	15	rpcnd 9882	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
17	8, 16	subcld 8445	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
18		2cn 9169	. . . . 5
19	18	a1i 9	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
20		2ap0 9191	. . . . 5 #
21	20	a1i 9	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ #
22	17, 19, 21	sqdivapd 10895	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
23	18	sqvali 10828	. . . . 5
24	23	oveq2i 6005	. . . 4
25	17	sqcld 10880	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
26	25, 19, 19, 21, 21	divdivap1d 8957	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
27		binom2sub 10862	. . . . . . . . . 10 $/\$
28	8, 16, 27	syl2anc 411	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
29		nnre 9105	. . . . . . . . . . . . . . 15
30		nnre 9105	. . . . . . . . . . . . . . 15
31		readdcl 8113	. . . . . . . . . . . . . . 15 $/\$
32	29, 30, 31	syl2anr 290	. . . . . . . . . . . . . 14 $/\$
33	32	3adant1 1039	. . . . . . . . . . . . 13 $/\$ $/\$
34	33	3ad2ant1 1042	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
35	34	recnd 8163	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
36		resubcl 8398	. . . . . . . . . . . . . . 15 $/\$
37	29, 30, 36	syl2anr 290	. . . . . . . . . . . . . 14 $/\$
38	37	3adant1 1039	. . . . . . . . . . . . 13 $/\$ $/\$
39	38	3ad2ant1 1042	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
40	39	recnd 8163	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
41	8, 16	mulcld 8155	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
42		mulcl 8114	. . . . . . . . . . . 12 $/\$
43	18, 41, 42	sylancr 414	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
44	35, 40, 43	addsubd 8466	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
45	3	nncnd 9112	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
46		simp11 1051	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
47	46	nncnd 9112	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
48		subdi 8519	. . . . . . . . . . . 12 $/\$ $/\$
49	18, 45, 47, 48	mp3an2i 1376	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
50		nncn 9106	. . . . . . . . . . . . . . 15
51		nncn 9106	. . . . . . . . . . . . . . 15
52		ppncan 8376	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
53	52	3anidm13 1330	. . . . . . . . . . . . . . . 16 $/\$
54		2times 9226	. . . . . . . . . . . . . . . . 17
55	54	adantr 276	. . . . . . . . . . . . . . . 16 $/\$
56	53, 55	eqtr4d 2265	. . . . . . . . . . . . . . 15 $/\$
57	50, 51, 56	syl2anr 290	. . . . . . . . . . . . . 14 $/\$
58	57	3adant1 1039	. . . . . . . . . . . . 13 $/\$ $/\$
59	58	3ad2ant1 1042	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
60	4	nncnd 9112	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
61		subsq 10855	. . . . . . . . . . . . . . . . 17 $/\$
62	45, 60, 61	syl2anc 411	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
63		oveq1 6001	. . . . . . . . . . . . . . . . . 18
64	63	3ad2ant2 1043	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
65		nncn 9106	. . . . . . . . . . . . . . . . . . . . 21
66	65	sqcld 10880	. . . . . . . . . . . . . . . . . . . 20
67	66	3ad2ant1 1042	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
68	51	sqcld 10880	. . . . . . . . . . . . . . . . . . . 20
69	68	3ad2ant2 1043	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
70	67, 69	pncand 8446	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
71	70	3ad2ant1 1042	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
72	64, 71	eqtr3d 2264	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
73	62, 72	eqtr3d 2264	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
74	73	fveq2d 5627	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
75	29	adantl 277	. . . . . . . . . . . . . . . . . . 19 $/\$
76	30	adantr 276	. . . . . . . . . . . . . . . . . . 19 $/\$
77		nngt0 9123	. . . . . . . . . . . . . . . . . . . 20
78	77	adantl 277	. . . . . . . . . . . . . . . . . . 19 $/\$
79		nngt0 9123	. . . . . . . . . . . . . . . . . . . 20
80	79	adantr 276	. . . . . . . . . . . . . . . . . . 19 $/\$
81	75, 76, 78, 80	addgt0d 8656	. . . . . . . . . . . . . . . . . 18 $/\$
82		0re 8134	. . . . . . . . . . . . . . . . . . 19
83		ltle 8222	. . . . . . . . . . . . . . . . . . 19 $/\$
84	82, 83	mpan 424	. . . . . . . . . . . . . . . . . 18
85	32, 81, 84	sylc 62	. . . . . . . . . . . . . . . . 17 $/\$
86	85	3adant1 1039	. . . . . . . . . . . . . . . 16 $/\$ $/\$
87	86	3ad2ant1 1042	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
88		ltle 8222	. . . . . . . . . . . . . . . . 17 $/\$
89	82, 88	mpan 424	. . . . . . . . . . . . . . . 16
90	39, 13, 89	sylc 62	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
91	34, 87, 39, 90	sqrtmuld 11666	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
92		nnre 9105	. . . . . . . . . . . . . . . . 17
93	92	3ad2ant1 1042	. . . . . . . . . . . . . . . 16 $/\$ $/\$
94	93	3ad2ant1 1042	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
95		nnnn0 9364	. . . . . . . . . . . . . . . . . 18
96	95	nn0ge0d 9413	. . . . . . . . . . . . . . . . 17
97	96	3ad2ant1 1042	. . . . . . . . . . . . . . . 16 $/\$ $/\$
98	97	3ad2ant1 1042	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
99	94, 98	sqrtsqd 11662	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
100	74, 91, 99	3eqtr3d 2270	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
101	100	oveq2d 6010	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
102	59, 101	oveq12d 6012	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
103	49, 102	eqtr4d 2265	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
104		resqrtth 11528	. . . . . . . . . . . . 13 $/\$
105	34, 87, 104	syl2anc 411	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
106	105	oveq1d 6009	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
107		resqrtth 11528	. . . . . . . . . . . 12 $/\$
108	39, 90, 107	syl2anc 411	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
109	106, 108	oveq12d 6012	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
110	44, 103, 109	3eqtr4rd 2273	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
111	28, 110	eqtrd 2262	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
112	111	oveq1d 6009	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
113		subcl 8333	. . . . . . . . . . 11 $/\$
114	50, 65, 113	syl2anr 290	. . . . . . . . . 10 $/\$
115	114	3adant2 1040	. . . . . . . . 9 $/\$ $/\$
116	115	3ad2ant1 1042	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
117	116, 19, 21	divcanap3d 8930	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
118	112, 117	eqtrd 2262	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
119	118	oveq1d 6009	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
120	26, 119	eqtr3d 2264	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
121	24, 120	eqtrid 2274	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
122	22, 121	eqtrd 2262	. 2 $/\$ $/\$ $/\$ $/\$ $/\$
123	2, 122	eqtrid 2274	1 $/\$ $/\$ $/\$ $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 104 $/\$ w3a 1002

wceq 1395

wcel 2200 class class class wbr 4082

cfv 5314 (class class class)co 5994

cc 7985

cr 7986

cc0 7987

c1 7988

caddc 7990

cmul 7992

clt 8169

cle 8170

cmin 8305 # cap 8716

cdiv 8807

cn 9098

c2 9149

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-dc 840 df-3or 1003 df-3an 1004 df-tru 1398 df-fal 1401 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-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-rp 9838 df-seqfrec 10657 df-exp 10748 df-rsqrt 11495

This theorem is referenced by: pythagtriplem15 12787 pythagtriplem17 12789

W3C validator