pythagtriplem14 - Intuitionistic Logic Explorer

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

Theorem pythagtriplem14 12650

Description: Lemma for pythagtrip 12656. 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 5964	. 2
3		simp13 1032	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
4		simp12 1031	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
5	3, 4	nnaddcld 9097	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
6	5	nnrpd 9829	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
7	6	rpsqrtcld 11519	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
8	7	rpcnd 9833	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
9	3	nnred 9062	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
10	4	nnred 9062	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
11	9, 10	resubcld 8466	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
12		pythagtriplem10 12642	. . . . . . . . 9 $/\$ $/\$ $/\$
13	12	3adant3 1020	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
14	11, 13	elrpd 9828	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
15	14	rpsqrtcld 11519	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
16	15	rpcnd 9833	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
17	8, 16	subcld 8396	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
18		2cn 9120	. . . . 5
19	18	a1i 9	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
20		2ap0 9142	. . . . 5 #
21	20	a1i 9	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ #
22	17, 19, 21	sqdivapd 10844	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
23	18	sqvali 10777	. . . . 5
24	23	oveq2i 5965	. . . 4
25	17	sqcld 10829	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
26	25, 19, 19, 21, 21	divdivap1d 8908	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
27		binom2sub 10811	. . . . . . . . . 10 $/\$
28	8, 16, 27	syl2anc 411	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
29		nnre 9056	. . . . . . . . . . . . . . 15
30		nnre 9056	. . . . . . . . . . . . . . 15
31		readdcl 8064	. . . . . . . . . . . . . . 15 $/\$
32	29, 30, 31	syl2anr 290	. . . . . . . . . . . . . 14 $/\$
33	32	3adant1 1018	. . . . . . . . . . . . 13 $/\$ $/\$
34	33	3ad2ant1 1021	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
35	34	recnd 8114	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
36		resubcl 8349	. . . . . . . . . . . . . . 15 $/\$
37	29, 30, 36	syl2anr 290	. . . . . . . . . . . . . 14 $/\$
38	37	3adant1 1018	. . . . . . . . . . . . 13 $/\$ $/\$
39	38	3ad2ant1 1021	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
40	39	recnd 8114	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
41	8, 16	mulcld 8106	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
42		mulcl 8065	. . . . . . . . . . . 12 $/\$
43	18, 41, 42	sylancr 414	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
44	35, 40, 43	addsubd 8417	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
45	3	nncnd 9063	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
46		simp11 1030	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
47	46	nncnd 9063	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
48		subdi 8470	. . . . . . . . . . . 12 $/\$ $/\$
49	18, 45, 47, 48	mp3an2i 1355	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
50		nncn 9057	. . . . . . . . . . . . . . 15
51		nncn 9057	. . . . . . . . . . . . . . 15
52		ppncan 8327	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
53	52	3anidm13 1309	. . . . . . . . . . . . . . . 16 $/\$
54		2times 9177	. . . . . . . . . . . . . . . . 17
55	54	adantr 276	. . . . . . . . . . . . . . . 16 $/\$
56	53, 55	eqtr4d 2242	. . . . . . . . . . . . . . 15 $/\$
57	50, 51, 56	syl2anr 290	. . . . . . . . . . . . . 14 $/\$
58	57	3adant1 1018	. . . . . . . . . . . . 13 $/\$ $/\$
59	58	3ad2ant1 1021	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
60	4	nncnd 9063	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
61		subsq 10804	. . . . . . . . . . . . . . . . 17 $/\$
62	45, 60, 61	syl2anc 411	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
63		oveq1 5961	. . . . . . . . . . . . . . . . . 18
64	63	3ad2ant2 1022	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
65		nncn 9057	. . . . . . . . . . . . . . . . . . . . 21
66	65	sqcld 10829	. . . . . . . . . . . . . . . . . . . 20
67	66	3ad2ant1 1021	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
68	51	sqcld 10829	. . . . . . . . . . . . . . . . . . . 20
69	68	3ad2ant2 1022	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
70	67, 69	pncand 8397	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
71	70	3ad2ant1 1021	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
72	64, 71	eqtr3d 2241	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
73	62, 72	eqtr3d 2241	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
74	73	fveq2d 5590	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
75	29	adantl 277	. . . . . . . . . . . . . . . . . . 19 $/\$
76	30	adantr 276	. . . . . . . . . . . . . . . . . . 19 $/\$
77		nngt0 9074	. . . . . . . . . . . . . . . . . . . 20
78	77	adantl 277	. . . . . . . . . . . . . . . . . . 19 $/\$
79		nngt0 9074	. . . . . . . . . . . . . . . . . . . 20
80	79	adantr 276	. . . . . . . . . . . . . . . . . . 19 $/\$
81	75, 76, 78, 80	addgt0d 8607	. . . . . . . . . . . . . . . . . 18 $/\$
82		0re 8085	. . . . . . . . . . . . . . . . . . 19
83		ltle 8173	. . . . . . . . . . . . . . . . . . 19 $/\$
84	82, 83	mpan 424	. . . . . . . . . . . . . . . . . 18
85	32, 81, 84	sylc 62	. . . . . . . . . . . . . . . . 17 $/\$
86	85	3adant1 1018	. . . . . . . . . . . . . . . 16 $/\$ $/\$
87	86	3ad2ant1 1021	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
88		ltle 8173	. . . . . . . . . . . . . . . . 17 $/\$
89	82, 88	mpan 424	. . . . . . . . . . . . . . . 16
90	39, 13, 89	sylc 62	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
91	34, 87, 39, 90	sqrtmuld 11530	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
92		nnre 9056	. . . . . . . . . . . . . . . . 17
93	92	3ad2ant1 1021	. . . . . . . . . . . . . . . 16 $/\$ $/\$
94	93	3ad2ant1 1021	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
95		nnnn0 9315	. . . . . . . . . . . . . . . . . 18
96	95	nn0ge0d 9364	. . . . . . . . . . . . . . . . 17
97	96	3ad2ant1 1021	. . . . . . . . . . . . . . . 16 $/\$ $/\$
98	97	3ad2ant1 1021	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
99	94, 98	sqrtsqd 11526	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
100	74, 91, 99	3eqtr3d 2247	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
101	100	oveq2d 5970	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
102	59, 101	oveq12d 5972	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
103	49, 102	eqtr4d 2242	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
104		resqrtth 11392	. . . . . . . . . . . . 13 $/\$
105	34, 87, 104	syl2anc 411	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
106	105	oveq1d 5969	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
107		resqrtth 11392	. . . . . . . . . . . 12 $/\$
108	39, 90, 107	syl2anc 411	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
109	106, 108	oveq12d 5972	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
110	44, 103, 109	3eqtr4rd 2250	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
111	28, 110	eqtrd 2239	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
112	111	oveq1d 5969	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
113		subcl 8284	. . . . . . . . . . 11 $/\$
114	50, 65, 113	syl2anr 290	. . . . . . . . . 10 $/\$
115	114	3adant2 1019	. . . . . . . . 9 $/\$ $/\$
116	115	3ad2ant1 1021	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
117	116, 19, 21	divcanap3d 8881	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
118	112, 117	eqtrd 2239	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
119	118	oveq1d 5969	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
120	26, 119	eqtr3d 2241	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
121	24, 120	eqtrid 2251	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
122	22, 121	eqtrd 2239	. 2 $/\$ $/\$ $/\$ $/\$ $/\$
123	2, 122	eqtrid 2251	1 $/\$ $/\$ $/\$ $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

wn 3

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

wceq 1373

wcel 2177 class class class wbr 4048

cfv 5277 (class class class)co 5954

cc 7936

cr 7937

cc0 7938

c1 7939

caddc 7941

cmul 7943

clt 8120

cle 8121

cmin 8256 # cap 8667

cdiv 8758

cn 9049

c2 9100

cexp 10696

csqrt 11357

cdvds 12148

cgcd 12324

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 615 ax-in2 616 ax-io 711 ax-5 1471 ax-7 1472 ax-gen 1473 ax-ie1 1517 ax-ie2 1518 ax-8 1528 ax-10 1529 ax-11 1530 ax-i12 1531 ax-bndl 1533 ax-4 1534 ax-17 1550 ax-i9 1554 ax-ial 1558 ax-i5r 1559 ax-13 2179 ax-14 2180 ax-ext 2188 ax-coll 4164 ax-sep 4167 ax-nul 4175 ax-pow 4223 ax-pr 4258 ax-un 4485 ax-setind 4590 ax-iinf 4641 ax-cnex 8029 ax-resscn 8030 ax-1cn 8031 ax-1re 8032 ax-icn 8033 ax-addcl 8034 ax-addrcl 8035 ax-mulcl 8036 ax-mulrcl 8037 ax-addcom 8038 ax-mulcom 8039 ax-addass 8040 ax-mulass 8041 ax-distr 8042 ax-i2m1 8043 ax-0lt1 8044 ax-1rid 8045 ax-0id 8046 ax-rnegex 8047 ax-precex 8048 ax-cnre 8049 ax-pre-ltirr 8050 ax-pre-ltwlin 8051 ax-pre-lttrn 8052 ax-pre-apti 8053 ax-pre-ltadd 8054 ax-pre-mulgt0 8055 ax-pre-mulext 8056 ax-arch 8057 ax-caucvg 8058

This theorem depends on definitions: df-bi 117 df-dc 837 df-3or 982 df-3an 983 df-tru 1376 df-fal 1379 df-nf 1485 df-sb 1787 df-eu 2058 df-mo 2059 df-clab 2193 df-cleq 2199 df-clel 2202 df-nfc 2338 df-ne 2378 df-nel 2473 df-ral 2490 df-rex 2491 df-reu 2492 df-rmo 2493 df-rab 2494 df-v 2775 df-sbc 3001 df-csb 3096 df-dif 3170 df-un 3172 df-in 3174 df-ss 3181 df-nul 3463 df-if 3574 df-pw 3620 df-sn 3641 df-pr 3642 df-op 3644 df-uni 3854 df-int 3889 df-iun 3932 df-br 4049 df-opab 4111 df-mpt 4112 df-tr 4148 df-id 4345 df-po 4348 df-iso 4349 df-iord 4418 df-on 4420 df-ilim 4421 df-suc 4423 df-iom 4644 df-xp 4686 df-rel 4687 df-cnv 4688 df-co 4689 df-dm 4690 df-rn 4691 df-res 4692 df-ima 4693 df-iota 5238 df-fun 5279 df-fn 5280 df-f 5281 df-f1 5282 df-fo 5283 df-f1o 5284 df-fv 5285 df-riota 5909 df-ov 5957 df-oprab 5958 df-mpo 5959 df-1st 6236 df-2nd 6237 df-recs 6401 df-frec 6487 df-pnf 8122 df-mnf 8123 df-xr 8124 df-ltxr 8125 df-le 8126 df-sub 8258 df-neg 8259 df-reap 8661 df-ap 8668 df-div 8759 df-inn 9050 df-2 9108 df-3 9109 df-4 9110 df-n0 9309 df-z 9386 df-uz 9662 df-rp 9789 df-seqfrec 10606 df-exp 10697 df-rsqrt 11359

This theorem is referenced by: pythagtriplem15 12651 pythagtriplem17 12653

W3C validator