Theorem pythagtrip 14832

Description: Parameterize the Pythagorean triples. If A, B, and C 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	|- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) <-> E. n e. NN E. m e. NN E. k e. NN ( { A , B } = { ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) , ( k x. ( 2 x. ( m x. n ) ) ) } /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )

Distinct variable groups:   A, k, m, n   B, k, m, n   C, k, m, n

Proof of Theorem pythagtrip

Step	Hyp	Ref	Expression
1		divgcdodd 14701	. . . . . . 7 |- ( ( A e. NN /\ B e. NN ) -> ( -. 2 || ( A / ( A gcd B ) ) \/ -. 2 || ( B / ( A gcd B ) ) ) )
2	1	3adant3 1034	. . . . . 6 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( -. 2 || ( A / ( A gcd B ) ) \/ -. 2 || ( B / ( A gcd B ) ) ) )
3	2	adantr 471	. . . . 5 |- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> ( -. 2 || ( A / ( A gcd B ) ) \/ -. 2 || ( B / ( A gcd B ) ) ) )
4		pythagtriplem19 14831	. . . . . . 7 |- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ -. 2 || ( A / ( A gcd B ) ) ) -> E. n e. NN E. m e. NN E. k e. NN ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) )
5	4	3expia 1217	. . . . . 6 |- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> ( -. 2 || ( A / ( A gcd B ) ) -> E. n e. NN E. m e. NN E. k e. NN ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
6		simp12 1045	. . . . . . . 8 |- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ -. 2 || ( B / ( A gcd B ) ) ) -> B e. NN )
7		simp11 1044	. . . . . . . 8 |- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ -. 2 || ( B / ( A gcd B ) ) ) -> A e. NN )
8		simp13 1046	. . . . . . . 8 |- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ -. 2 || ( B / ( A gcd B ) ) ) -> C e. NN )
9		nnsqcl 12375	. . . . . . . . . . . . . 14 |- ( A e. NN -> ( A ^ 2 ) e. NN )
10	9	nncnd 10652	. . . . . . . . . . . . 13 |- ( A e. NN -> ( A ^ 2 ) e. CC )
11	10	3ad2ant1 1035	. . . . . . . . . . . 12 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( A ^ 2 ) e. CC )
12		nnsqcl 12375	. . . . . . . . . . . . . 14 |- ( B e. NN -> ( B ^ 2 ) e. NN )
13	12	nncnd 10652	. . . . . . . . . . . . 13 |- ( B e. NN -> ( B ^ 2 ) e. CC )
14	13	3ad2ant2 1036	. . . . . . . . . . . 12 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( B ^ 2 ) e. CC )
15	11, 14	addcomd 9860	. . . . . . . . . . 11 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( ( B ^ 2 ) + ( A ^ 2 ) ) )
16	15	eqeq1d 2463	. . . . . . . . . 10 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) <-> ( ( B ^ 2 ) + ( A ^ 2 ) ) = ( C ^ 2 ) ) )
17	16	biimpa 491	. . . . . . . . 9 |- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> ( ( B ^ 2 ) + ( A ^ 2 ) ) = ( C ^ 2 ) )
18	17	3adant3 1034	. . . . . . . 8 |- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ -. 2 || ( B / ( A gcd B ) ) ) -> ( ( B ^ 2 ) + ( A ^ 2 ) ) = ( C ^ 2 ) )
19		nnz 10987	. . . . . . . . . . . . . . 15 |- ( A e. NN -> A e. ZZ )
20	19	3ad2ant1 1035	. . . . . . . . . . . . . 14 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> A e. ZZ )
21	20	adantr 471	. . . . . . . . . . . . 13 |- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> A e. ZZ )
22		nnz 10987	. . . . . . . . . . . . . . 15 |- ( B e. NN -> B e. ZZ )
23	22	3ad2ant2 1036	. . . . . . . . . . . . . 14 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> B e. ZZ )
24	23	adantr 471	. . . . . . . . . . . . 13 |- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> B e. ZZ )
25		gcdcom 14532	. . . . . . . . . . . . 13 |- ( ( A e. ZZ /\ B e. ZZ ) -> ( A gcd B ) = ( B gcd A ) )
26	21, 24, 25	syl2anc 671	. . . . . . . . . . . 12 |- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> ( A gcd B ) = ( B gcd A ) )
27	26	oveq2d 6330	. . . . . . . . . . 11 |- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> ( B / ( A gcd B ) ) = ( B / ( B gcd A ) ) )
28	27	breq2d 4427	. . . . . . . . . 10 |- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> ( 2 || ( B / ( A gcd B ) ) <-> 2 || ( B / ( B gcd A ) ) ) )
29	28	notbid 300	. . . . . . . . 9 |- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> ( -. 2 || ( B / ( A gcd B ) ) <-> -. 2 || ( B / ( B gcd A ) ) ) )
30	29	biimp3a 1379	. . . . . . . 8 |- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ -. 2 || ( B / ( A gcd B ) ) ) -> -. 2 || ( B / ( B gcd A ) ) )
31		pythagtriplem19 14831	. . . . . . . 8 |- ( ( ( B e. NN /\ A e. NN /\ C e. NN ) /\ ( ( B ^ 2 ) + ( A ^ 2 ) ) = ( C ^ 2 ) /\ -. 2 || ( B / ( B gcd A ) ) ) -> E. n e. NN E. m e. NN E. k e. NN ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) )
32	6, 7, 8, 18, 30, 31	syl311anc 1290	. . . . . . 7 |- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ -. 2 || ( B / ( A gcd B ) ) ) -> E. n e. NN E. m e. NN E. k e. NN ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) )
33	32	3expia 1217	. . . . . 6 |- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> ( -. 2 || ( B / ( A gcd B ) ) -> E. n e. NN E. m e. NN E. k e. NN ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
34	5, 33	orim12d 854	. . . . 5 |- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> ( ( -. 2 || ( A / ( A gcd B ) ) \/ -. 2 || ( B / ( A gcd B ) ) ) -> ( E. n e. NN E. m e. NN E. k e. NN ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) \/ E. n e. NN E. m e. NN E. k e. NN ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) ) )
35	3, 34	mpd 15	. . . 4 |- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> ( E. n e. NN E. m e. NN E. k e. NN ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) \/ E. n e. NN E. m e. NN E. k e. NN ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
36		ovex 6342	. . . . . . . . . . 11 |- ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) e. _V
37		ovex 6342	. . . . . . . . . . 11 |- ( k x. ( 2 x. ( m x. n ) ) ) e. _V
38		preq12bg 4167	. . . . . . . . . . 11 |- ( ( ( A e. NN /\ B e. NN ) /\ ( ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) e. _V /\ ( k x. ( 2 x. ( m x. n ) ) ) e. _V ) ) -> ( { A , B } = { ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) , ( k x. ( 2 x. ( m x. n ) ) ) } <-> ( ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) ) \/ ( A = ( k x. ( 2 x. ( m x. n ) ) ) /\ B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) ) ) ) )
39	36, 37, 38	mpanr12 696	. . . . . . . . . 10 |- ( ( A e. NN /\ B e. NN ) -> ( { A , B } = { ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) , ( k x. ( 2 x. ( m x. n ) ) ) } <-> ( ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) ) \/ ( A = ( k x. ( 2 x. ( m x. n ) ) ) /\ B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) ) ) ) )
40	39	anbi1d 716	. . . . . . . . 9 |- ( ( A e. NN /\ B e. NN ) -> ( ( { A , B } = { ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) , ( k x. ( 2 x. ( m x. n ) ) ) } /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) <-> ( ( ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) ) \/ ( A = ( k x. ( 2 x. ( m x. n ) ) ) /\ B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
41	40	rexbidv 2912	. . . . . . . 8 |- ( ( A e. NN /\ B e. NN ) -> ( E. k e. NN ( { A , B } = { ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) , ( k x. ( 2 x. ( m x. n ) ) ) } /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) <-> E. k e. NN ( ( ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) ) \/ ( A = ( k x. ( 2 x. ( m x. n ) ) ) /\ B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
42	41	2rexbidv 2919	. . . . . . 7 |- ( ( A e. NN /\ B e. NN ) -> ( E. n e. NN E. m e. NN E. k e. NN ( { A , B } = { ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) , ( k x. ( 2 x. ( m x. n ) ) ) } /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) <-> E. n e. NN E. m e. NN E. k e. NN ( ( ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) ) \/ ( A = ( k x. ( 2 x. ( m x. n ) ) ) /\ B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
43		andir 884	. . . . . . . . . . 11 |- ( ( ( ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) ) \/ ( A = ( k x. ( 2 x. ( m x. n ) ) ) /\ B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) <-> ( ( ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) \/ ( ( A = ( k x. ( 2 x. ( m x. n ) ) ) /\ B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
44		df-3an 993	. . . . . . . . . . . 12 |- ( ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) <-> ( ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) )
45		df-3an 993	. . . . . . . . . . . 12 |- ( ( A = ( k x. ( 2 x. ( m x. n ) ) ) /\ B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) <-> ( ( A = ( k x. ( 2 x. ( m x. n ) ) ) /\ B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) )
46	44, 45	orbi12i 528	. . . . . . . . . . 11 |- ( ( ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) \/ ( A = ( k x. ( 2 x. ( m x. n ) ) ) /\ B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) <-> ( ( ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) \/ ( ( A = ( k x. ( 2 x. ( m x. n ) ) ) /\ B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
47		3ancoma 998	. . . . . . . . . . . 12 |- ( ( A = ( k x. ( 2 x. ( m x. n ) ) ) /\ B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) <-> ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) )
48	47	orbi2i 526	. . . . . . . . . . 11 |- ( ( ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) \/ ( A = ( k x. ( 2 x. ( m x. n ) ) ) /\ B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) <-> ( ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) \/ ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
49	43, 46, 48	3bitr2i 281	. . . . . . . . . 10 |- ( ( ( ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) ) \/ ( A = ( k x. ( 2 x. ( m x. n ) ) ) /\ B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) <-> ( ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) \/ ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
50	49	rexbii 2900	. . . . . . . . 9 |- ( E. k e. NN ( ( ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) ) \/ ( A = ( k x. ( 2 x. ( m x. n ) ) ) /\ B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) <-> E. k e. NN ( ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) \/ ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
51	50	2rexbii 2901	. . . . . . . 8 |- ( E. n e. NN E. m e. NN E. k e. NN ( ( ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) ) \/ ( A = ( k x. ( 2 x. ( m x. n ) ) ) /\ B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) <-> E. n e. NN E. m e. NN E. k e. NN ( ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) \/ ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
52		r19.43 2957	. . . . . . . . . 10 |- ( E. k e. NN ( ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) \/ ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) <-> ( E. k e. NN ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) \/ E. k e. NN ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
53	52	2rexbii 2901	. . . . . . . . 9 |- ( E. n e. NN E. m e. NN E. k e. NN ( ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) \/ ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) <-> E. n e. NN E. m e. NN ( E. k e. NN ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) \/ E. k e. NN ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
54		r19.43 2957	. . . . . . . . . . 11 |- ( E. m e. NN ( E. k e. NN ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) \/ E. k e. NN ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) <-> ( E. m e. NN E. k e. NN ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) \/ E. m e. NN E. k e. NN ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
55	54	rexbii 2900	. . . . . . . . . 10 |- ( E. n e. NN E. m e. NN ( E. k e. NN ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) \/ E. k e. NN ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) <-> E. n e. NN ( E. m e. NN E. k e. NN ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) \/ E. m e. NN E. k e. NN ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
56		r19.43 2957	. . . . . . . . . 10 |- ( E. n e. NN ( E. m e. NN E. k e. NN ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) \/ E. m e. NN E. k e. NN ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) <-> ( E. n e. NN E. m e. NN E. k e. NN ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) \/ E. n e. NN E. m e. NN E. k e. NN ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
57	55, 56	bitri 257	. . . . . . . . 9 |- ( E. n e. NN E. m e. NN ( E. k e. NN ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) \/ E. k e. NN ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) <-> ( E. n e. NN E. m e. NN E. k e. NN ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) \/ E. n e. NN E. m e. NN E. k e. NN ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
58	53, 57	bitri 257	. . . . . . . 8 |- ( E. n e. NN E. m e. NN E. k e. NN ( ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) \/ ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) <-> ( E. n e. NN E. m e. NN E. k e. NN ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) \/ E. n e. NN E. m e. NN E. k e. NN ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
59	51, 58	bitri 257	. . . . . . 7 |- ( E. n e. NN E. m e. NN E. k e. NN ( ( ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) ) \/ ( A = ( k x. ( 2 x. ( m x. n ) ) ) /\ B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) <-> ( E. n e. NN E. m e. NN E. k e. NN ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) \/ E. n e. NN E. m e. NN E. k e. NN ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
60	42, 59	syl6bb 269	. . . . . 6 |- ( ( A e. NN /\ B e. NN ) -> ( E. n e. NN E. m e. NN E. k e. NN ( { A , B } = { ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) , ( k x. ( 2 x. ( m x. n ) ) ) } /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) <-> ( E. n e. NN E. m e. NN E. k e. NN ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) \/ E. n e. NN E. m e. NN E. k e. NN ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) ) )
61	60	3adant3 1034	. . . . 5 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( E. n e. NN E. m e. NN E. k e. NN ( { A , B } = { ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) , ( k x. ( 2 x. ( m x. n ) ) ) } /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) <-> ( E. n e. NN E. m e. NN E. k e. NN ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) \/ E. n e. NN E. m e. NN E. k e. NN ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) ) )
62	61	adantr 471	. . . 4 |- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> ( E. n e. NN E. m e. NN E. k e. NN ( { A , B } = { ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) , ( k x. ( 2 x. ( m x. n ) ) ) } /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) <-> ( E. n e. NN E. m e. NN E. k e. NN ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) \/ E. n e. NN E. m e. NN E. k e. NN ( B = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ A = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) ) )
63	35, 62	mpbird 240	. . 3 |- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> E. n e. NN E. m e. NN E. k e. NN ( { A , B } = { ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) , ( k x. ( 2 x. ( m x. n ) ) ) } /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) )
64	63	ex 440	. 2 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) -> E. n e. NN E. m e. NN E. k e. NN ( { A , B } = { ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) , ( k x. ( 2 x. ( m x. n ) ) ) } /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
65		pythagtriplem2 14815	. . 3 |- ( ( A e. NN /\ B e. NN ) -> ( E. n e. NN E. m e. NN E. k e. NN ( { A , B } = { ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) , ( k x. ( 2 x. ( m x. n ) ) ) } /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) )
66	65	3adant3 1034	. 2 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( E. n e. NN E. m e. NN E. k e. NN ( { A , B } = { ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) , ( k x. ( 2 x. ( m x. n ) ) ) } /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) )
67	64, 66	impbid 195	1 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) <-> E. n e. NN E. m e. NN E. k e. NN ( { A , B } = { ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) , ( k x. ( 2 x. ( m x. n ) ) ) } /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 189   \/ wo 374   /\ wa 375   /\ w3a 991   = wceq 1454   e. wcel 1897   E.wrex 2749   _Vcvv 3056   {cpr 3981   class class class wbr 4415  (class class class)co 6314   CCcc 9562   + caddc 9567   x. cmul 9569   - cmin 9885   / cdiv 10296   NNcn 10636   2c2 10686   ZZcz 10965   ^cexp 12303   || cdvds 14353   gcd cgcd 14516

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-8 1899  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-sep 4538  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6609  ax-cnex 9620  ax-resscn 9621  ax-1cn 9622  ax-icn 9623  ax-addcl 9624  ax-addrcl 9625  ax-mulcl 9626  ax-mulrcl 9627  ax-mulcom 9628  ax-addass 9629  ax-mulass 9630  ax-distr 9631  ax-i2m1 9632  ax-1ne0 9633  ax-1rid 9634  ax-rnegex 9635  ax-rrecex 9636  ax-cnre 9637  ax-pre-lttri 9638  ax-pre-lttrn 9639  ax-pre-ltadd 9640  ax-pre-mulgt0 9641  ax-pre-sup 9642

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-eu 2313  df-mo 2314  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-nel 2635  df-ral 2753  df-rex 2754  df-reu 2755  df-rmo 2756  df-rab 2757  df-v 3058  df-sbc 3279  df-csb 3375  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-pss 3431  df-nul 3743  df-if 3893  df-pw 3964  df-sn 3980  df-pr 3982  df-tp 3984  df-op 3986  df-uni 4212  df-int 4248  df-iun 4293  df-br 4416  df-opab 4475  df-mpt 4476  df-tr 4511  df-eprel 4763  df-id 4767  df-po 4773  df-so 4774  df-fr 4811  df-we 4813  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-pred 5398  df-ord 5444  df-on 5445  df-lim 5446  df-suc 5447  df-iota 5564  df-fun 5602  df-fn 5603  df-f 5604  df-f1 5605  df-fo 5606  df-f1o 5607  df-fv 5608  df-riota 6276  df-ov 6317  df-oprab 6318  df-mpt2 6319  df-om 6719  df-1st 6819  df-2nd 6820  df-wrecs 7053  df-recs 7115  df-rdg 7153  df-1o 7207  df-2o 7208  df-oadd 7211  df-er 7388  df-en 7595  df-dom 7596  df-sdom 7597  df-fin 7598  df-sup 7981  df-inf 7982  df-pnf 9702  df-mnf 9703  df-xr 9704  df-ltxr 9705  df-le 9706  df-sub 9887  df-neg 9888  df-div 10297  df-nn 10637  df-2 10695  df-3 10696  df-4 10697  df-n0 10898  df-z 10966  df-uz 11188  df-rp 11331  df-fz 11813  df-fl 12059  df-mod 12128  df-seq 12245  df-exp 12304  df-cj 13210  df-re 13211  df-im 13212  df-sqrt 13346  df-abs 13347  df-dvds 14354  df-gcd 14517  df-prm 14671

This theorem is referenced by: (None)