pythagtrip - Metamath Proof Explorer

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

Theorem pythagtrip 14370

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 14272	. . . . . . 7 $/\$ $\/$
2	1	3adant3 1016	. . . . . 6 $/\$ $/\$ $\/$
3	2	adantr 465	. . . . 5 $/\$ $/\$ $/\$ $\/$
4		pythagtriplem19 14369	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
5	4	3expia 1198	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
6		simp12 1027	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
7		simp11 1026	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
8		simp13 1028	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
9		nnsqcl 12240	. . . . . . . . . . . . . 14
10	9	nncnd 10572	. . . . . . . . . . . . 13
11	10	3ad2ant1 1017	. . . . . . . . . . . 12 $/\$ $/\$
12		nnsqcl 12240	. . . . . . . . . . . . . 14
13	12	nncnd 10572	. . . . . . . . . . . . 13
14	13	3ad2ant2 1018	. . . . . . . . . . . 12 $/\$ $/\$
15	11, 14	addcomd 9799	. . . . . . . . . . 11 $/\$ $/\$
16	15	eqeq1d 2459	. . . . . . . . . 10 $/\$ $/\$
17	16	biimpa 484	. . . . . . . . 9 $/\$ $/\$ $/\$
18	17	3adant3 1016	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
19		nnz 10907	. . . . . . . . . . . . . . 15
20	19	3ad2ant1 1017	. . . . . . . . . . . . . 14 $/\$ $/\$
21	20	adantr 465	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
22		nnz 10907	. . . . . . . . . . . . . . 15
23	22	3ad2ant2 1018	. . . . . . . . . . . . . 14 $/\$ $/\$
24	23	adantr 465	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
25		gcdcom 14170	. . . . . . . . . . . . 13 $/\$
26	21, 24, 25	syl2anc 661	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
27	26	oveq2d 6312	. . . . . . . . . . 11 $/\$ $/\$ $/\$
28	27	breq2d 4468	. . . . . . . . . 10 $/\$ $/\$ $/\$
29	28	notbid 294	. . . . . . . . 9 $/\$ $/\$ $/\$
30	29	biimp3a 1328	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
31		pythagtriplem19 14369	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
32	6, 7, 8, 18, 30, 31	syl311anc 1242	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
33	32	3expia 1198	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
34	5, 33	orim12d 838	. . . . 5 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $/\$
35	3, 34	mpd 15	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
36		ovex 6324	. . . . . . . . . . 11
37		ovex 6324	. . . . . . . . . . 11
38		preq12bg 4211	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$
39	36, 37, 38	mpanr12 685	. . . . . . . . . 10 $/\$ $/\$ $\/$ $/\$
40	39	anbi1d 704	. . . . . . . . 9 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
41	40	rexbidv 2968	. . . . . . . 8 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
42	41	2rexbidv 2975	. . . . . . 7 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
43		andir 868	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
44		df-3an 975	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
45		df-3an 975	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
46	44, 45	orbi12i 521	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
47		3ancoma 980	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
48	47	orbi2i 519	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
49	43, 46, 48	3bitr2i 273	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
50	49	rexbii 2959	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
51	50	2rexbii 2960	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
52		r19.43 3013	. . . . . . . . . 10 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
53	52	2rexbii 2960	. . . . . . . . 9 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
54		r19.43 3013	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
55	54	rexbii 2959	. . . . . . . . . 10 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
56		r19.43 3013	. . . . . . . . . 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 1016	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
62	61	adantr 465	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
63	35, 62	mpbird 232	. . 3 $/\$ $/\$ $/\$ $/\$
64	63	ex 434	. 2 $/\$ $/\$ $/\$
65		pythagtriplem2 14353	. . 3 $/\$ $/\$
66	65	3adant3 1016	. 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 973

wceq 1395

wcel 1819

wrex 2808

cvv 3109

cpr 4034 class class class wbr 4456 (class class class)co 6296

cc 9507

caddc 9512

cmul 9514

cmin 9824

cdiv 10227

cn 10556

c2 10606

cz 10885

cexp 12169

cdvds 13998

cgcd 14156

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1619 ax-4 1632 ax-5 1705 ax-6 1748 ax-7 1791 ax-8 1821 ax-9 1823 ax-10 1838 ax-11 1843 ax-12 1855 ax-13 2000 ax-ext 2435 ax-sep 4578 ax-nul 4586 ax-pow 4634 ax-pr 4695 ax-un 6591 ax-cnex 9565 ax-resscn 9566 ax-1cn 9567 ax-icn 9568 ax-addcl 9569 ax-addrcl 9570 ax-mulcl 9571 ax-mulrcl 9572 ax-mulcom 9573 ax-addass 9574 ax-mulass 9575 ax-distr 9576 ax-i2m1 9577 ax-1ne0 9578 ax-1rid 9579 ax-rnegex 9580 ax-rrecex 9581 ax-cnre 9582 ax-pre-lttri 9583 ax-pre-lttrn 9584 ax-pre-ltadd 9585 ax-pre-mulgt0 9586 ax-pre-sup 9587

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1398 df-ex 1614 df-nf 1618 df-sb 1741 df-eu 2287 df-mo 2288 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ne 2654 df-nel 2655 df-ral 2812 df-rex 2813 df-reu 2814 df-rmo 2815 df-rab 2816 df-v 3111 df-sbc 3328 df-csb 3431 df-dif 3474 df-un 3476 df-in 3478 df-ss 3485 df-pss 3487 df-nul 3794 df-if 3945 df-pw 4017 df-sn 4033 df-pr 4035 df-tp 4037 df-op 4039 df-uni 4252 df-int 4289 df-iun 4334 df-br 4457 df-opab 4516 df-mpt 4517 df-tr 4551 df-eprel 4800 df-id 4804 df-po 4809 df-so 4810 df-fr 4847 df-we 4849 df-ord 4890 df-on 4891 df-lim 4892 df-suc 4893 df-xp 5014 df-rel 5015 df-cnv 5016 df-co 5017 df-dm 5018 df-rn 5019 df-res 5020 df-ima 5021 df-iota 5557 df-fun 5596 df-fn 5597 df-f 5598 df-f1 5599 df-fo 5600 df-f1o 5601 df-fv 5602 df-riota 6258 df-ov 6299 df-oprab 6300 df-mpt2 6301 df-om 6700 df-1st 6799 df-2nd 6800 df-recs 7060 df-rdg 7094 df-1o 7148 df-2o 7149 df-oadd 7152 df-er 7329 df-en 7536 df-dom 7537 df-sdom 7538 df-fin 7539 df-sup 7919 df-pnf 9647 df-mnf 9648 df-xr 9649 df-ltxr 9650 df-le 9651 df-sub 9826 df-neg 9827 df-div 10228 df-nn 10557 df-2 10615 df-3 10616 df-4 10617 df-n0 10817 df-z 10886 df-uz 11107 df-rp 11246 df-fz 11698 df-fl 11932 df-mod 12000 df-seq 12111 df-exp 12170 df-cj 12944 df-re 12945 df-im 12946 df-sqrt 13080 df-abs 13081 df-dvds 13999 df-gcd 14157 df-prm 14230

This theorem is referenced by: (None)

W3C validator