pythagtrip - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > pythagtrip		Structured version Unicode version

Theorem pythagtrip 14012

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 13916	. . . . . . 7 $/\$ $\/$
2	1	3adant3 1008	. . . . . 6 $/\$ $/\$ $\/$
3	2	adantr 465	. . . . 5 $/\$ $/\$ $/\$ $\/$
4		pythagtriplem19 14011	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
5	4	3expia 1190	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
6		simp12 1019	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
7		simp11 1018	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
8		simp13 1020	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
9		nnsqcl 12045	. . . . . . . . . . . . . 14
10	9	nncnd 10442	. . . . . . . . . . . . 13
11	10	3ad2ant1 1009	. . . . . . . . . . . 12 $/\$ $/\$
12		nnsqcl 12045	. . . . . . . . . . . . . 14
13	12	nncnd 10442	. . . . . . . . . . . . 13
14	13	3ad2ant2 1010	. . . . . . . . . . . 12 $/\$ $/\$
15	11, 14	addcomd 9675	. . . . . . . . . . 11 $/\$ $/\$
16	15	eqeq1d 2453	. . . . . . . . . 10 $/\$ $/\$
17	16	biimpa 484	. . . . . . . . 9 $/\$ $/\$ $/\$
18	17	3adant3 1008	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
19		nnz 10772	. . . . . . . . . . . . . . 15
20	19	3ad2ant1 1009	. . . . . . . . . . . . . 14 $/\$ $/\$
21	20	adantr 465	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
22		nnz 10772	. . . . . . . . . . . . . . 15
23	22	3ad2ant2 1010	. . . . . . . . . . . . . 14 $/\$ $/\$
24	23	adantr 465	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
25		gcdcom 13815	. . . . . . . . . . . . 13 $/\$
26	21, 24, 25	syl2anc 661	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
27	26	oveq2d 6209	. . . . . . . . . . 11 $/\$ $/\$ $/\$
28	27	breq2d 4405	. . . . . . . . . 10 $/\$ $/\$ $/\$
29	28	notbid 294	. . . . . . . . 9 $/\$ $/\$ $/\$
30	29	biimp3a 1319	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
31		pythagtriplem19 14011	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
32	6, 7, 8, 18, 30, 31	syl311anc 1233	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
33	32	3expia 1190	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
34	5, 33	orim12d 834	. . . . 5 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $/\$
35	3, 34	mpd 15	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
36		ovex 6218	. . . . . . . . . . 11
37		ovex 6218	. . . . . . . . . . 11
38		preq12bg 4152	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$
39	36, 37, 38	mpanr12 685	. . . . . . . . . 10 $/\$ $/\$ $\/$ $/\$
40	39	anbi1d 704	. . . . . . . . 9 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
41	40	rexbidv 2855	. . . . . . . 8 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
42	41	2rexbidv 2872	. . . . . . 7 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
43		andir 863	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
44		df-3an 967	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
45		df-3an 967	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
46	44, 45	orbi12i 521	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
47		3ancoma 972	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
48	47	orbi2i 519	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
49	43, 46, 48	3bitr2i 273	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
50	49	rexbii 2859	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
51	50	2rexbii 2861	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
52		r19.43 2975	. . . . . . . . . 10 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
53	52	2rexbii 2861	. . . . . . . . 9 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
54		r19.43 2975	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
55	54	rexbii 2859	. . . . . . . . . 10 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
56		r19.43 2975	. . . . . . . . . 10 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
57	55, 56	bitri 249	. . . . . . . . 9 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
58	53, 57	bitri 249	. . . . . . . 8 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
59	51, 58	bitri 249	. . . . . . 7 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
60	42, 59	syl6bb 261	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
61	60	3adant3 1008	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
62	61	adantr 465	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
63	35, 62	mpbird 232	. . 3 $/\$ $/\$ $/\$ $/\$
64	63	ex 434	. 2 $/\$ $/\$ $/\$
65		pythagtriplem2 13995	. . 3 $/\$ $/\$
66	65	3adant3 1008	. 2 $/\$ $/\$ $/\$
67	64, 66	impbid 191	1 $/\$ $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $\/$ wo 368 $/\$ wa 369 $/\$ w3a 965

wceq 1370

wcel 1758

wrex 2796

cvv 3071

cpr 3980 class class class wbr 4393 (class class class)co 6193

cc 9384

caddc 9389

cmul 9391

cmin 9699

cdiv 10097

cn 10426

c2 10475

cz 10750

cexp 11975

cdivides 13646

cgcd 13801

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1952 ax-ext 2430 ax-sep 4514 ax-nul 4522 ax-pow 4571 ax-pr 4632 ax-un 6475 ax-cnex 9442 ax-resscn 9443 ax-1cn 9444 ax-icn 9445 ax-addcl 9446 ax-addrcl 9447 ax-mulcl 9448 ax-mulrcl 9449 ax-mulcom 9450 ax-addass 9451 ax-mulass 9452 ax-distr 9453 ax-i2m1 9454 ax-1ne0 9455 ax-1rid 9456 ax-rnegex 9457 ax-rrecex 9458 ax-cnre 9459 ax-pre-lttri 9460 ax-pre-lttrn 9461 ax-pre-ltadd 9462 ax-pre-mulgt0 9463 ax-pre-sup 9464

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2264 df-mo 2265 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2601 df-ne 2646 df-nel 2647 df-ral 2800 df-rex 2801 df-reu 2802 df-rmo 2803 df-rab 2804 df-v 3073 df-sbc 3288 df-csb 3390 df-dif 3432 df-un 3434 df-in 3436 df-ss 3443 df-pss 3445 df-nul 3739 df-if 3893 df-pw 3963 df-sn 3979 df-pr 3981 df-tp 3983 df-op 3985 df-uni 4193 df-int 4230 df-iun 4274 df-br 4394 df-opab 4452 df-mpt 4453 df-tr 4487 df-eprel 4733 df-id 4737 df-po 4742 df-so 4743 df-fr 4780 df-we 4782 df-ord 4823 df-on 4824 df-lim 4825 df-suc 4826 df-xp 4947 df-rel 4948 df-cnv 4949 df-co 4950 df-dm 4951 df-rn 4952 df-res 4953 df-ima 4954 df-iota 5482 df-fun 5521 df-fn 5522 df-f 5523 df-f1 5524 df-fo 5525 df-f1o 5526 df-fv 5527 df-riota 6154 df-ov 6196 df-oprab 6197 df-mpt2 6198 df-om 6580 df-1st 6680 df-2nd 6681 df-recs 6935 df-rdg 6969 df-1o 7023 df-2o 7024 df-oadd 7027 df-er 7204 df-en 7414 df-dom 7415 df-sdom 7416 df-fin 7417 df-sup 7795 df-pnf 9524 df-mnf 9525 df-xr 9526 df-ltxr 9527 df-le 9528 df-sub 9701 df-neg 9702 df-div 10098 df-nn 10427 df-2 10484 df-3 10485 df-4 10486 df-n0 10684 df-z 10751 df-uz 10966 df-rp 11096 df-fz 11548 df-fl 11752 df-mod 11819 df-seq 11917 df-exp 11976 df-cj 12699 df-re 12700 df-im 12701 df-sqr 12835 df-abs 12836 df-dvds 13647 df-gcd 13802 df-prm 13875

This theorem is referenced by: (None)

W3C validator