pythagtriplem2 - Intuitionistic Logic Explorer

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

Theorem pythagtriplem2 12639

Description: Lemma for pythagtrip 12656. Prove the full version of one direction of the theorem. (Contributed by Scott Fenton, 28-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)

**Assertion**
Ref	Expression
pythagtriplem2	$/\$ $/\$

Distinct variable groups:

**Proof of Theorem pythagtriplem2**
Step	Hyp	Ref	Expression
1		simplll 533	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
2		simpllr 534	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
3		nnz 9404	. . . . . . . . . 10
4	3	adantl 277	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
5		simplrr 536	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
6	5	nnzd 9507	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
7		zsqcl 10768	. . . . . . . . . . 11
8	6, 7	syl 14	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
9		simplrl 535	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
10	9	nnzd 9507	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
11		zsqcl 10768	. . . . . . . . . . 11
12	10, 11	syl 14	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
13	8, 12	zsubcld 9513	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
14	4, 13	zmulcld 9514	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
15		2z 9413	. . . . . . . . . . 11
16	15	a1i 9	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
17	6, 10	zmulcld 9514	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
18	16, 17	zmulcld 9514	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
19	4, 18	zmulcld 9514	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
20		preq12bg 3817	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$
21	1, 2, 14, 19, 20	syl22anc 1251	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$
22	21	anbi1d 465	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
23		andir 821	. . . . . . 7 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
24		df-3an 983	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
25		df-3an 983	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
26	24, 25	orbi12i 766	. . . . . . 7 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
27	23, 26	bitr4i 187	. . . . . 6 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
28	22, 27	bitrdi 196	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
29	28	rexbidva 2504	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
30	29	2rexbidva 2530	. . 3 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
31		r19.43 2665	. . . . 5 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
32	31	2rexbii 2516	. . . 4 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
33		r19.43 2665	. . . . 5 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
34	33	rexbii 2514	. . . 4 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
35		r19.43 2665	. . . 4 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
36	32, 34, 35	3bitri 206	. . 3 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
37	30, 36	bitrdi 196	. 2 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
38		pythagtriplem1 12638	. . . 4 $/\$ $/\$
39	38	a1i 9	. . 3 $/\$ $/\$ $/\$
40		3ancoma 988	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
41	40	rexbii 2514	. . . . . 6 $/\$ $/\$ $/\$ $/\$
42	41	2rexbii 2516	. . . . 5 $/\$ $/\$ $/\$ $/\$
43		pythagtriplem1 12638	. . . . 5 $/\$ $/\$
44	42, 43	sylbi 121	. . . 4 $/\$ $/\$
45		nncn 9057	. . . . . . 7
46	45	sqcld 10829	. . . . . 6
47		nncn 9057	. . . . . . 7
48	47	sqcld 10829	. . . . . 6
49		addcom 8222	. . . . . 6 $/\$
50	46, 48, 49	syl2an 289	. . . . 5 $/\$
51	50	eqeq1d 2215	. . . 4 $/\$
52	44, 51	imbitrrid 156	. . 3 $/\$ $/\$ $/\$
53	39, 52	jaod 719	. 2 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
54	37, 53	sylbid 150	1 $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 104

wb 105 $\/$ wo 710 $/\$ w3a 981

wceq 1373

wcel 2177

wrex 2486

cpr 3636 (class class class)co 5954

cc 7936

caddc 7941

cmul 7943

cmin 8256

cn 9049

c2 9100

cz 9385

cexp 10696

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

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-seqfrec 10606 df-exp 10697

This theorem is referenced by: pythagtrip 12656

W3C validator