pythagtrip - Intuitionistic Logic Explorer

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

Theorem pythagtrip 12792

Description: Parameterize the Pythagorean triples. If

, and

are naturals, then they obey the Pythagorean triple formula iff they are parameterized by three naturals. This proof follows the Isabelle proof at http://afp.sourceforge.net/entries/Fermat3_4.shtml. This is Metamath 100 proof #23. (Contributed by Scott Fenton, 19-Apr-2014.)

**Assertion**
Ref	Expression
pythagtrip	$/\$ $/\$ $/\$

Distinct variable groups:

**Proof of Theorem pythagtrip**
Step	Hyp	Ref	Expression
1		divgcdodd 12651	. . . . . . 7 $/\$ $\/$
2	1	3adant3 1041	. . . . . 6 $/\$ $/\$ $\/$
3	2	adantr 276	. . . . 5 $/\$ $/\$ $/\$ $\/$
4		pythagtriplem19 12791	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
5	4	3expia 1229	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
6		simp12 1052	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
7		simp11 1051	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
8		simp13 1053	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
9		nnsqcl 10818	. . . . . . . . . . . . . 14
10	9	nncnd 9112	. . . . . . . . . . . . 13
11	10	3ad2ant1 1042	. . . . . . . . . . . 12 $/\$ $/\$
12		nnsqcl 10818	. . . . . . . . . . . . . 14
13	12	nncnd 9112	. . . . . . . . . . . . 13
14	13	3ad2ant2 1043	. . . . . . . . . . . 12 $/\$ $/\$
15	11, 14	addcomd 8285	. . . . . . . . . . 11 $/\$ $/\$
16	15	eqeq1d 2238	. . . . . . . . . 10 $/\$ $/\$
17	16	biimpa 296	. . . . . . . . 9 $/\$ $/\$ $/\$
18	17	3adant3 1041	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
19		nnz 9453	. . . . . . . . . . . . . 14
20	19	3ad2ant1 1042	. . . . . . . . . . . . 13 $/\$ $/\$
21		nnz 9453	. . . . . . . . . . . . . . 15
22	21	3ad2ant2 1043	. . . . . . . . . . . . . 14 $/\$ $/\$
23	22	adantr 276	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
24		gcdcom 12480	. . . . . . . . . . . . 13 $/\$
25	20, 23, 24	syl2an2r 597	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
26	25	oveq2d 6010	. . . . . . . . . . 11 $/\$ $/\$ $/\$
27	26	breq2d 4094	. . . . . . . . . 10 $/\$ $/\$ $/\$
28	27	notbid 671	. . . . . . . . 9 $/\$ $/\$ $/\$
29	28	biimp3a 1379	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
30		pythagtriplem19 12791	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
31	6, 7, 8, 18, 29, 30	syl311anc 1285	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
32	31	3expia 1229	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
33	5, 32	orim12d 791	. . . . 5 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $/\$
34	3, 33	mpd 13	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
35		simplll 533	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
36		simpllr 534	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
37		nnz 9453	. . . . . . . . . . . . 13
38	37	adantl 277	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
39		simplrr 536	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
40	39	nnzd 9556	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
41		zsqcl 10819	. . . . . . . . . . . . . 14
42	40, 41	syl 14	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
43		simplrl 535	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
44	43	nnzd 9556	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
45		zsqcl 10819	. . . . . . . . . . . . . 14
46	44, 45	syl 14	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
47	42, 46	zsubcld 9562	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
48	38, 47	zmulcld 9563	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
49		2z 9462	. . . . . . . . . . . . . 14
50	49	a1i 9	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
51	40, 44	zmulcld 9563	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
52	50, 51	zmulcld 9563	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
53	38, 52	zmulcld 9563	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
54		preq12bg 3850	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$
55	35, 36, 48, 53, 54	syl22anc 1272	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$
56	55	anbi1d 465	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
57	56	rexbidva 2527	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
58	57	2rexbidva 2553	. . . . . . 7 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
59		andir 824	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
60		df-3an 1004	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
61		df-3an 1004	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
62	60, 61	orbi12i 769	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
63		3ancoma 1009	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
64	63	orbi2i 767	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
65	59, 62, 64	3bitr2i 208	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
66	65	rexbii 2537	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
67	66	2rexbii 2539	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
68		r19.43 2689	. . . . . . . . . 10 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
69	68	2rexbii 2539	. . . . . . . . 9 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
70		r19.43 2689	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
71	70	rexbii 2537	. . . . . . . . . 10 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
72		r19.43 2689	. . . . . . . . . 10 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
73	71, 72	bitri 184	. . . . . . . . 9 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
74	69, 73	bitri 184	. . . . . . . 8 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
75	67, 74	bitri 184	. . . . . . 7 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
76	58, 75	bitrdi 196	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
77	76	3adant3 1041	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
78	77	adantr 276	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
79	34, 78	mpbird 167	. . 3 $/\$ $/\$ $/\$ $/\$
80	79	ex 115	. 2 $/\$ $/\$ $/\$
81		pythagtriplem2 12775	. . 3 $/\$ $/\$
82	81	3adant3 1041	. 2 $/\$ $/\$ $/\$
83	80, 82	impbid 129	1 $/\$ $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 104

wb 105 $\/$ wo 713 $/\$ w3a 1002

wceq 1395

wcel 2200

wrex 2509

cpr 3667 class class class wbr 4082 (class class class)co 5994

cc 7985

caddc 7990

cmul 7992

cmin 8305

cdiv 8807

cn 9098

c2 9149

cz 9434

cexp 10747

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: (None)

W3C validator