pythagtrip - Metamath Proof Explorer

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

Theorem pythagtrip 14206

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 14108	. . . . . . 7 $/\$ $\/$
2	1	3adant3 1011	. . . . . 6 $/\$ $/\$ $\/$
3	2	adantr 465	. . . . 5 $/\$ $/\$ $/\$ $\/$
4		pythagtriplem19 14205	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
5	4	3expia 1193	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
6		simp12 1022	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
7		simp11 1021	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
8		simp13 1023	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
9		nnsqcl 12192	. . . . . . . . . . . . . 14
10	9	nncnd 10541	. . . . . . . . . . . . 13
11	10	3ad2ant1 1012	. . . . . . . . . . . 12 $/\$ $/\$
12		nnsqcl 12192	. . . . . . . . . . . . . 14
13	12	nncnd 10541	. . . . . . . . . . . . 13
14	13	3ad2ant2 1013	. . . . . . . . . . . 12 $/\$ $/\$
15	11, 14	addcomd 9770	. . . . . . . . . . 11 $/\$ $/\$
16	15	eqeq1d 2462	. . . . . . . . . 10 $/\$ $/\$
17	16	biimpa 484	. . . . . . . . 9 $/\$ $/\$ $/\$
18	17	3adant3 1011	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
19		nnz 10875	. . . . . . . . . . . . . . 15
20	19	3ad2ant1 1012	. . . . . . . . . . . . . 14 $/\$ $/\$
21	20	adantr 465	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
22		nnz 10875	. . . . . . . . . . . . . . 15
23	22	3ad2ant2 1013	. . . . . . . . . . . . . 14 $/\$ $/\$
24	23	adantr 465	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
25		gcdcom 14006	. . . . . . . . . . . . 13 $/\$
26	21, 24, 25	syl2anc 661	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
27	26	oveq2d 6291	. . . . . . . . . . 11 $/\$ $/\$ $/\$
28	27	breq2d 4452	. . . . . . . . . 10 $/\$ $/\$ $/\$
29	28	notbid 294	. . . . . . . . 9 $/\$ $/\$ $/\$
30	29	biimp3a 1323	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
31		pythagtriplem19 14205	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
32	6, 7, 8, 18, 30, 31	syl311anc 1237	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
33	32	3expia 1193	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
34	5, 33	orim12d 835	. . . . 5 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $/\$
35	3, 34	mpd 15	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
36		ovex 6300	. . . . . . . . . . 11
37		ovex 6300	. . . . . . . . . . 11
38		preq12bg 4198	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$
39	36, 37, 38	mpanr12 685	. . . . . . . . . 10 $/\$ $/\$ $\/$ $/\$
40	39	anbi1d 704	. . . . . . . . 9 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
41	40	rexbidv 2966	. . . . . . . 8 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
42	41	2rexbidv 2973	. . . . . . 7 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
43		andir 864	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
44		df-3an 970	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
45		df-3an 970	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
46	44, 45	orbi12i 521	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
47		3ancoma 975	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
48	47	orbi2i 519	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
49	43, 46, 48	3bitr2i 273	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
50	49	rexbii 2958	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
51	50	2rexbii 2959	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
52		r19.43 3010	. . . . . . . . . 10 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
53	52	2rexbii 2959	. . . . . . . . 9 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
54		r19.43 3010	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
55	54	rexbii 2958	. . . . . . . . . 10 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
56		r19.43 3010	. . . . . . . . . 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 1011	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
62	61	adantr 465	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
63	35, 62	mpbird 232	. . 3 $/\$ $/\$ $/\$ $/\$
64	63	ex 434	. 2 $/\$ $/\$ $/\$
65		pythagtriplem2 14189	. . 3 $/\$ $/\$
66	65	3adant3 1011	. 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 968

wceq 1374

wcel 1762

wrex 2808

cvv 3106

cpr 4022 class class class wbr 4440 (class class class)co 6275

cc 9479

caddc 9484

cmul 9486

cmin 9794

cdiv 10195

cn 10525

c2 10574

cz 10853

cexp 12122

cdivides 13836

cgcd 13992

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1596 ax-4 1607 ax-5 1675 ax-6 1714 ax-7 1734 ax-8 1764 ax-9 1766 ax-10 1781 ax-11 1786 ax-12 1798 ax-13 1961 ax-ext 2438 ax-sep 4561 ax-nul 4569 ax-pow 4618 ax-pr 4679 ax-un 6567 ax-cnex 9537 ax-resscn 9538 ax-1cn 9539 ax-icn 9540 ax-addcl 9541 ax-addrcl 9542 ax-mulcl 9543 ax-mulrcl 9544 ax-mulcom 9545 ax-addass 9546 ax-mulass 9547 ax-distr 9548 ax-i2m1 9549 ax-1ne0 9550 ax-1rid 9551 ax-rnegex 9552 ax-rrecex 9553 ax-cnre 9554 ax-pre-lttri 9555 ax-pre-lttrn 9556 ax-pre-ltadd 9557 ax-pre-mulgt0 9558 ax-pre-sup 9559

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 969 df-3an 970 df-tru 1377 df-ex 1592 df-nf 1595 df-sb 1707 df-eu 2272 df-mo 2273 df-clab 2446 df-cleq 2452 df-clel 2455 df-nfc 2610 df-ne 2657 df-nel 2658 df-ral 2812 df-rex 2813 df-reu 2814 df-rmo 2815 df-rab 2816 df-v 3108 df-sbc 3325 df-csb 3429 df-dif 3472 df-un 3474 df-in 3476 df-ss 3483 df-pss 3485 df-nul 3779 df-if 3933 df-pw 4005 df-sn 4021 df-pr 4023 df-tp 4025 df-op 4027 df-uni 4239 df-int 4276 df-iun 4320 df-br 4441 df-opab 4499 df-mpt 4500 df-tr 4534 df-eprel 4784 df-id 4788 df-po 4793 df-so 4794 df-fr 4831 df-we 4833 df-ord 4874 df-on 4875 df-lim 4876 df-suc 4877 df-xp 4998 df-rel 4999 df-cnv 5000 df-co 5001 df-dm 5002 df-rn 5003 df-res 5004 df-ima 5005 df-iota 5542 df-fun 5581 df-fn 5582 df-f 5583 df-f1 5584 df-fo 5585 df-f1o 5586 df-fv 5587 df-riota 6236 df-ov 6278 df-oprab 6279 df-mpt2 6280 df-om 6672 df-1st 6774 df-2nd 6775 df-recs 7032 df-rdg 7066 df-1o 7120 df-2o 7121 df-oadd 7124 df-er 7301 df-en 7507 df-dom 7508 df-sdom 7509 df-fin 7510 df-sup 7890 df-pnf 9619 df-mnf 9620 df-xr 9621 df-ltxr 9622 df-le 9623 df-sub 9796 df-neg 9797 df-div 10196 df-nn 10526 df-2 10583 df-3 10584 df-4 10585 df-n0 10785 df-z 10854 df-uz 11072 df-rp 11210 df-fz 11662 df-fl 11886 df-mod 11953 df-seq 12064 df-exp 12123 df-cj 12882 df-re 12883 df-im 12884 df-sqr 13018 df-abs 13019 df-dvds 13837 df-gcd 13993 df-prm 14066

This theorem is referenced by: (None)

W3C validator