pythagtriplem16 - Intuitionistic Logic Explorer

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

Theorem pythagtriplem16 12768

Description: Lemma for pythagtrip 12772. Show the relationship between

, and

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

**Hypotheses**
Ref	Expression
pythagtriplem15.1
pythagtriplem15.2

**Assertion**
Ref	Expression
pythagtriplem16	$/\$ $/\$ $/\$ $/\$ $/\$

**Proof of Theorem pythagtriplem16**
Step	Hyp	Ref	Expression
1		pythagtriplem15.1	. . . . 5
2		pythagtriplem15.2	. . . . 5
3	1, 2	oveq12i 5986	. . . 4
4		simp13 1034	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
5		simp12 1033	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
6	4, 5	nnaddcld 9126	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
7	6	nnrpd 9858	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
8	7	rpsqrtcld 11635	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
9	8	rpcnd 9862	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
10	4	nnzd 9536	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
11	5	nnzd 9536	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
12	10, 11	zsubcld 9542	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
13	12	zred 9537	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
14		pythagtriplem10 12758	. . . . . . . . . . 11 $/\$ $/\$ $/\$
15	14	3adant3 1022	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
16	13, 15	elrpd 9857	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
17	16	rpsqrtcld 11635	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
18	17	rpcnd 9862	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
19	9, 18	addcld 8134	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
20		2cnd 9151	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
21	9, 18	subcld 8425	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
22		2ap0 9171	. . . . . . 7 #
23	22	a1i 9	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ #
24	19, 20, 21, 20, 23, 23	divmuldivapd 8947	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
25	19, 21	mulcld 8135	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
26	25, 20, 20, 23, 23	divdivap1d 8937	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
27		nnre 9085	. . . . . . . . . . . . 13
28		nnre 9085	. . . . . . . . . . . . 13
29		readdcl 8093	. . . . . . . . . . . . 13 $/\$
30	27, 28, 29	syl2anr 290	. . . . . . . . . . . 12 $/\$
31	30	3adant1 1020	. . . . . . . . . . 11 $/\$ $/\$
32	31	3ad2ant1 1023	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
33	27	adantl 277	. . . . . . . . . . . . . 14 $/\$
34	28	adantr 276	. . . . . . . . . . . . . 14 $/\$
35		nngt0 9103	. . . . . . . . . . . . . . 15
36	35	adantl 277	. . . . . . . . . . . . . 14 $/\$
37		nngt0 9103	. . . . . . . . . . . . . . 15
38	37	adantr 276	. . . . . . . . . . . . . 14 $/\$
39	33, 34, 36, 38	addgt0d 8636	. . . . . . . . . . . . 13 $/\$
40		0re 8114	. . . . . . . . . . . . . 14
41		ltle 8202	. . . . . . . . . . . . . 14 $/\$
42	40, 41	mpan 424	. . . . . . . . . . . . 13
43	30, 39, 42	sylc 62	. . . . . . . . . . . 12 $/\$
44	43	3adant1 1020	. . . . . . . . . . 11 $/\$ $/\$
45	44	3ad2ant1 1023	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
46		resqrtth 11508	. . . . . . . . . 10 $/\$
47	32, 45, 46	syl2anc 411	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
48		resubcl 8378	. . . . . . . . . . . . 13 $/\$
49	27, 28, 48	syl2anr 290	. . . . . . . . . . . 12 $/\$
50	49	3adant1 1020	. . . . . . . . . . 11 $/\$ $/\$
51	50	3ad2ant1 1023	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
52		ltle 8202	. . . . . . . . . . . 12 $/\$
53	40, 52	mpan 424	. . . . . . . . . . 11
54	51, 15, 53	sylc 62	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
55		resqrtth 11508	. . . . . . . . . 10 $/\$
56	51, 54, 55	syl2anc 411	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
57	47, 56	oveq12d 5992	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
58	57	oveq1d 5989	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
59		subsq 10835	. . . . . . . . 9 $/\$
60	9, 18, 59	syl2anc 411	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
61	60	oveq1d 5989	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
62		nncn 9086	. . . . . . . . . . . 12
63		nncn 9086	. . . . . . . . . . . 12
64		pnncan 8355	. . . . . . . . . . . . . 14 $/\$ $/\$
65	64	3anidm23 1312	. . . . . . . . . . . . 13 $/\$
66		2times 9206	. . . . . . . . . . . . . 14
67	66	adantl 277	. . . . . . . . . . . . 13 $/\$
68	65, 67	eqtr4d 2245	. . . . . . . . . . . 12 $/\$
69	62, 63, 68	syl2anr 290	. . . . . . . . . . 11 $/\$
70	69	3adant1 1020	. . . . . . . . . 10 $/\$ $/\$
71	70	3ad2ant1 1023	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
72	71	oveq1d 5989	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
73	5	nncnd 9092	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
74	73, 20, 23	divcanap3d 8910	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
75	72, 74	eqtrd 2242	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
76	58, 61, 75	3eqtr3d 2250	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
77	76	oveq1d 5989	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
78	24, 26, 77	3eqtr2d 2248	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
79	3, 78	eqtrid 2254	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
80	79	oveq2d 5990	. 2 $/\$ $/\$ $/\$ $/\$ $/\$
81	73, 20, 23	divcanap2d 8907	. 2 $/\$ $/\$ $/\$ $/\$ $/\$
82	80, 81	eqtr2d 2243	1 $/\$ $/\$ $/\$ $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

wn 3

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

wceq 1375

wcel 2180 class class class wbr 4062

cfv 5294 (class class class)co 5974

cc 7965

cr 7966

cc0 7967

c1 7968

caddc 7970

cmul 7972

clt 8149

cle 8150

cmin 8285 # cap 8696

cdiv 8787

cn 9078

c2 9129

cexp 10727

csqrt 11473

cdvds 12264

cgcd 12440

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 713 ax-5 1473 ax-7 1474 ax-gen 1475 ax-ie1 1519 ax-ie2 1520 ax-8 1530 ax-10 1531 ax-11 1532 ax-i12 1533 ax-bndl 1535 ax-4 1536 ax-17 1552 ax-i9 1556 ax-ial 1560 ax-i5r 1561 ax-13 2182 ax-14 2183 ax-ext 2191 ax-coll 4178 ax-sep 4181 ax-nul 4189 ax-pow 4237 ax-pr 4272 ax-un 4501 ax-setind 4606 ax-iinf 4657 ax-cnex 8058 ax-resscn 8059 ax-1cn 8060 ax-1re 8061 ax-icn 8062 ax-addcl 8063 ax-addrcl 8064 ax-mulcl 8065 ax-mulrcl 8066 ax-addcom 8067 ax-mulcom 8068 ax-addass 8069 ax-mulass 8070 ax-distr 8071 ax-i2m1 8072 ax-0lt1 8073 ax-1rid 8074 ax-0id 8075 ax-rnegex 8076 ax-precex 8077 ax-cnre 8078 ax-pre-ltirr 8079 ax-pre-ltwlin 8080 ax-pre-lttrn 8081 ax-pre-apti 8082 ax-pre-ltadd 8083 ax-pre-mulgt0 8084 ax-pre-mulext 8085 ax-arch 8086 ax-caucvg 8087

This theorem depends on definitions: df-bi 117 df-dc 839 df-3or 984 df-3an 985 df-tru 1378 df-fal 1381 df-nf 1487 df-sb 1789 df-eu 2060 df-mo 2061 df-clab 2196 df-cleq 2202 df-clel 2205 df-nfc 2341 df-ne 2381 df-nel 2476 df-ral 2493 df-rex 2494 df-reu 2495 df-rmo 2496 df-rab 2497 df-v 2781 df-sbc 3009 df-csb 3105 df-dif 3179 df-un 3181 df-in 3183 df-ss 3190 df-nul 3472 df-if 3583 df-pw 3631 df-sn 3652 df-pr 3653 df-op 3655 df-uni 3868 df-int 3903 df-iun 3946 df-br 4063 df-opab 4125 df-mpt 4126 df-tr 4162 df-id 4361 df-po 4364 df-iso 4365 df-iord 4434 df-on 4436 df-ilim 4437 df-suc 4439 df-iom 4660 df-xp 4702 df-rel 4703 df-cnv 4704 df-co 4705 df-dm 4706 df-rn 4707 df-res 4708 df-ima 4709 df-iota 5254 df-fun 5296 df-fn 5297 df-f 5298 df-f1 5299 df-fo 5300 df-f1o 5301 df-fv 5302 df-riota 5927 df-ov 5977 df-oprab 5978 df-mpo 5979 df-1st 6256 df-2nd 6257 df-recs 6421 df-frec 6507 df-pnf 8151 df-mnf 8152 df-xr 8153 df-ltxr 8154 df-le 8155 df-sub 8287 df-neg 8288 df-reap 8690 df-ap 8697 df-div 8788 df-inn 9079 df-2 9137 df-3 9138 df-4 9139 df-n0 9338 df-z 9415 df-uz 9691 df-rp 9818 df-seqfrec 10637 df-exp 10728 df-rsqrt 11475

This theorem is referenced by: pythagtriplem18 12770

W3C validator