pythagtrip - Metamath Proof Explorer

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

Theorem pythagtrip 14777

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 14646	. . . . . . 7 $/\$ $\/$
2	1	3adant3 1026	. . . . . 6 $/\$ $/\$ $\/$
3	2	adantr 467	. . . . 5 $/\$ $/\$ $/\$ $\/$
4		pythagtriplem19 14776	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
5	4	3expia 1208	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
6		simp12 1037	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
7		simp11 1036	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
8		simp13 1038	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
9		nnsqcl 12345	. . . . . . . . . . . . . 14
10	9	nncnd 10627	. . . . . . . . . . . . 13
11	10	3ad2ant1 1027	. . . . . . . . . . . 12 $/\$ $/\$
12		nnsqcl 12345	. . . . . . . . . . . . . 14
13	12	nncnd 10627	. . . . . . . . . . . . 13
14	13	3ad2ant2 1028	. . . . . . . . . . . 12 $/\$ $/\$
15	11, 14	addcomd 9837	. . . . . . . . . . 11 $/\$ $/\$
16	15	eqeq1d 2425	. . . . . . . . . 10 $/\$ $/\$
17	16	biimpa 487	. . . . . . . . 9 $/\$ $/\$ $/\$
18	17	3adant3 1026	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
19		nnz 10961	. . . . . . . . . . . . . . 15
20	19	3ad2ant1 1027	. . . . . . . . . . . . . 14 $/\$ $/\$
21	20	adantr 467	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
22		nnz 10961	. . . . . . . . . . . . . . 15
23	22	3ad2ant2 1028	. . . . . . . . . . . . . 14 $/\$ $/\$
24	23	adantr 467	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
25		gcdcom 14477	. . . . . . . . . . . . 13 $/\$
26	21, 24, 25	syl2anc 666	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
27	26	oveq2d 6319	. . . . . . . . . . 11 $/\$ $/\$ $/\$
28	27	breq2d 4433	. . . . . . . . . 10 $/\$ $/\$ $/\$
29	28	notbid 296	. . . . . . . . 9 $/\$ $/\$ $/\$
30	29	biimp3a 1365	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
31		pythagtriplem19 14776	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
32	6, 7, 8, 18, 30, 31	syl311anc 1279	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
33	32	3expia 1208	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
34	5, 33	orim12d 847	. . . . 5 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $/\$
35	3, 34	mpd 15	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
36		ovex 6331	. . . . . . . . . . 11
37		ovex 6331	. . . . . . . . . . 11
38		preq12bg 4177	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$
39	36, 37, 38	mpanr12 690	. . . . . . . . . 10 $/\$ $/\$ $\/$ $/\$
40	39	anbi1d 710	. . . . . . . . 9 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
41	40	rexbidv 2940	. . . . . . . 8 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
42	41	2rexbidv 2947	. . . . . . 7 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
43		andir 877	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
44		df-3an 985	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
45		df-3an 985	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
46	44, 45	orbi12i 524	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
47		3ancoma 990	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
48	47	orbi2i 522	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
49	43, 46, 48	3bitr2i 277	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
50	49	rexbii 2928	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
51	50	2rexbii 2929	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
52		r19.43 2985	. . . . . . . . . 10 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
53	52	2rexbii 2929	. . . . . . . . 9 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
54		r19.43 2985	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
55	54	rexbii 2928	. . . . . . . . . 10 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
56		r19.43 2985	. . . . . . . . . 10 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
57	55, 56	bitri 253	. . . . . . . . 9 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
58	53, 57	bitri 253	. . . . . . . 8 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
59	51, 58	bitri 253	. . . . . . 7 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
60	42, 59	syl6bb 265	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
61	60	3adant3 1026	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
62	61	adantr 467	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
63	35, 62	mpbird 236	. . 3 $/\$ $/\$ $/\$ $/\$
64	63	ex 436	. 2 $/\$ $/\$ $/\$
65		pythagtriplem2 14760	. . 3 $/\$ $/\$
66	65	3adant3 1026	. 2 $/\$ $/\$ $/\$
67	64, 66	impbid 194	1 $/\$ $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 188 $\/$ wo 370 $/\$ wa 371 $/\$ w3a 983

wceq 1438

wcel 1869

wrex 2777

cvv 3082

cpr 3999 class class class wbr 4421 (class class class)co 6303

cc 9539

caddc 9544

cmul 9546

cmin 9862

cdiv 10271

cn 10611

c2 10661

cz 10939

cexp 12273

cdvds 14298

cgcd 14461

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1666 ax-4 1679 ax-5 1749 ax-6 1795 ax-7 1840 ax-8 1871 ax-9 1873 ax-10 1888 ax-11 1893 ax-12 1906 ax-13 2054 ax-ext 2401 ax-sep 4544 ax-nul 4553 ax-pow 4600 ax-pr 4658 ax-un 6595 ax-cnex 9597 ax-resscn 9598 ax-1cn 9599 ax-icn 9600 ax-addcl 9601 ax-addrcl 9602 ax-mulcl 9603 ax-mulrcl 9604 ax-mulcom 9605 ax-addass 9606 ax-mulass 9607 ax-distr 9608 ax-i2m1 9609 ax-1ne0 9610 ax-1rid 9611 ax-rnegex 9612 ax-rrecex 9613 ax-cnre 9614 ax-pre-lttri 9615 ax-pre-lttrn 9616 ax-pre-ltadd 9617 ax-pre-mulgt0 9618 ax-pre-sup 9619

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 984 df-3an 985 df-tru 1441 df-ex 1661 df-nf 1665 df-sb 1788 df-eu 2270 df-mo 2271 df-clab 2409 df-cleq 2415 df-clel 2418 df-nfc 2573 df-ne 2621 df-nel 2622 df-ral 2781 df-rex 2782 df-reu 2783 df-rmo 2784 df-rab 2785 df-v 3084 df-sbc 3301 df-csb 3397 df-dif 3440 df-un 3442 df-in 3444 df-ss 3451 df-pss 3453 df-nul 3763 df-if 3911 df-pw 3982 df-sn 3998 df-pr 4000 df-tp 4002 df-op 4004 df-uni 4218 df-int 4254 df-iun 4299 df-br 4422 df-opab 4481 df-mpt 4482 df-tr 4517 df-eprel 4762 df-id 4766 df-po 4772 df-so 4773 df-fr 4810 df-we 4812 df-xp 4857 df-rel 4858 df-cnv 4859 df-co 4860 df-dm 4861 df-rn 4862 df-res 4863 df-ima 4864 df-pred 5397 df-ord 5443 df-on 5444 df-lim 5445 df-suc 5446 df-iota 5563 df-fun 5601 df-fn 5602 df-f 5603 df-f1 5604 df-fo 5605 df-f1o 5606 df-fv 5607 df-riota 6265 df-ov 6306 df-oprab 6307 df-mpt2 6308 df-om 6705 df-1st 6805 df-2nd 6806 df-wrecs 7034 df-recs 7096 df-rdg 7134 df-1o 7188 df-2o 7189 df-oadd 7192 df-er 7369 df-en 7576 df-dom 7577 df-sdom 7578 df-fin 7579 df-sup 7960 df-inf 7961 df-pnf 9679 df-mnf 9680 df-xr 9681 df-ltxr 9682 df-le 9683 df-sub 9864 df-neg 9865 df-div 10272 df-nn 10612 df-2 10670 df-3 10671 df-4 10672 df-n0 10872 df-z 10940 df-uz 11162 df-rp 11305 df-fz 11787 df-fl 12029 df-mod 12098 df-seq 12215 df-exp 12274 df-cj 13156 df-re 13157 df-im 13158 df-sqrt 13292 df-abs 13293 df-dvds 14299 df-gcd 14462 df-prm 14616

This theorem is referenced by: (None)

W3C validator