Theorem pythagtriplem19 12296

Description: Lemma for pythagtrip 12297. Introduce k and remove the relative primality requirement. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)

Assertion

Ref	Expression
pythagtriplem19	|- ( ( ( 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 ) ) ) ) )

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

Proof of Theorem pythagtriplem19

Step	Hyp	Ref	Expression
1		gcdnncl 11982	. . . . 5 |- ( ( A e. NN /\ B e. NN ) -> ( A gcd B ) e. NN )
2	1	3adant3 1018	. . . 4 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( A gcd B ) e. NN )
3	2	3ad2ant1 1019	. . 3 |- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ -. 2 || ( A / ( A gcd B ) ) ) -> ( A gcd B ) e. NN )
4		nnz 9286	. . . . . . . . . . 11 |- ( A e. NN -> A e. ZZ )
5		nnz 9286	. . . . . . . . . . 11 |- ( B e. NN -> B e. ZZ )
6		gcddvds 11978	. . . . . . . . . . 11 |- ( ( A e. ZZ /\ B e. ZZ ) -> ( ( A gcd B ) || A /\ ( A gcd B ) || B ) )
7	4, 5, 6	syl2an 289	. . . . . . . . . 10 |- ( ( A e. NN /\ B e. NN ) -> ( ( A gcd B ) || A /\ ( A gcd B ) || B ) )
8	7	3adant3 1018	. . . . . . . . 9 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( A gcd B ) || A /\ ( A gcd B ) || B ) )
9	8	simpld 112	. . . . . . . 8 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( A gcd B ) || A )
10	2	nnzd 9388	. . . . . . . . 9 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( A gcd B ) e. ZZ )
11	2	nnne0d 8978	. . . . . . . . 9 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( A gcd B ) =/= 0 )
12	4	3ad2ant1 1019	. . . . . . . . 9 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> A e. ZZ )
13		dvdsval2 11811	. . . . . . . . 9 |- ( ( ( A gcd B ) e. ZZ /\ ( A gcd B ) =/= 0 /\ A e. ZZ ) -> ( ( A gcd B ) || A <-> ( A / ( A gcd B ) ) e. ZZ ) )
14	10, 11, 12, 13	syl3anc 1248	. . . . . . . 8 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( A gcd B ) || A <-> ( A / ( A gcd B ) ) e. ZZ ) )
15	9, 14	mpbid 147	. . . . . . 7 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( A / ( A gcd B ) ) e. ZZ )
16		nnre 8940	. . . . . . . . 9 |- ( A e. NN -> A e. RR )
17	16	3ad2ant1 1019	. . . . . . . 8 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> A e. RR )
18	2	nnred 8946	. . . . . . . 8 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( A gcd B ) e. RR )
19		nngt0 8958	. . . . . . . . 9 |- ( A e. NN -> 0 < A )
20	19	3ad2ant1 1019	. . . . . . . 8 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> 0 < A )
21	2	nngt0d 8977	. . . . . . . 8 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> 0 < ( A gcd B ) )
22	17, 18, 20, 21	divgt0d 8906	. . . . . . 7 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> 0 < ( A / ( A gcd B ) ) )
23		elnnz 9277	. . . . . . 7 |- ( ( A / ( A gcd B ) ) e. NN <-> ( ( A / ( A gcd B ) ) e. ZZ /\ 0 < ( A / ( A gcd B ) ) ) )
24	15, 22, 23	sylanbrc 417	. . . . . 6 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( A / ( A gcd B ) ) e. NN )
25	24	3ad2ant1 1019	. . . . 5 |- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ -. 2 || ( A / ( A gcd B ) ) ) -> ( A / ( A gcd B ) ) e. NN )
26	8	simprd 114	. . . . . . . 8 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( A gcd B ) || B )
27	5	3ad2ant2 1020	. . . . . . . . 9 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> B e. ZZ )
28		dvdsval2 11811	. . . . . . . . 9 |- ( ( ( A gcd B ) e. ZZ /\ ( A gcd B ) =/= 0 /\ B e. ZZ ) -> ( ( A gcd B ) || B <-> ( B / ( A gcd B ) ) e. ZZ ) )
29	10, 11, 27, 28	syl3anc 1248	. . . . . . . 8 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( A gcd B ) || B <-> ( B / ( A gcd B ) ) e. ZZ ) )
30	26, 29	mpbid 147	. . . . . . 7 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( B / ( A gcd B ) ) e. ZZ )
31		nnre 8940	. . . . . . . . 9 |- ( B e. NN -> B e. RR )
32	31	3ad2ant2 1020	. . . . . . . 8 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> B e. RR )
33		nngt0 8958	. . . . . . . . 9 |- ( B e. NN -> 0 < B )
34	33	3ad2ant2 1020	. . . . . . . 8 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> 0 < B )
35	32, 18, 34, 21	divgt0d 8906	. . . . . . 7 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> 0 < ( B / ( A gcd B ) ) )
36		elnnz 9277	. . . . . . 7 |- ( ( B / ( A gcd B ) ) e. NN <-> ( ( B / ( A gcd B ) ) e. ZZ /\ 0 < ( B / ( A gcd B ) ) ) )
37	30, 35, 36	sylanbrc 417	. . . . . 6 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( B / ( A gcd B ) ) e. NN )
38	37	3ad2ant1 1019	. . . . 5 |- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ -. 2 || ( A / ( A gcd B ) ) ) -> ( B / ( A gcd B ) ) e. NN )
39		dvdssq 12046	. . . . . . . . . . . . . . 15 |- ( ( ( A gcd B ) e. ZZ /\ A e. ZZ ) -> ( ( A gcd B ) || A <-> ( ( A gcd B ) ^ 2 ) || ( A ^ 2 ) ) )
40	10, 12, 39	syl2anc 411	. . . . . . . . . . . . . 14 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( A gcd B ) || A <-> ( ( A gcd B ) ^ 2 ) || ( A ^ 2 ) ) )
41		dvdssq 12046	. . . . . . . . . . . . . . 15 |- ( ( ( A gcd B ) e. ZZ /\ B e. ZZ ) -> ( ( A gcd B ) || B <-> ( ( A gcd B ) ^ 2 ) || ( B ^ 2 ) ) )
42	10, 27, 41	syl2anc 411	. . . . . . . . . . . . . 14 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( A gcd B ) || B <-> ( ( A gcd B ) ^ 2 ) || ( B ^ 2 ) ) )
43	40, 42	anbi12d 473	. . . . . . . . . . . . 13 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( ( A gcd B ) || A /\ ( A gcd B ) || B ) <-> ( ( ( A gcd B ) ^ 2 ) || ( A ^ 2 ) /\ ( ( A gcd B ) ^ 2 ) || ( B ^ 2 ) ) ) )
44	8, 43	mpbid 147	. . . . . . . . . . . 12 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( ( A gcd B ) ^ 2 ) || ( A ^ 2 ) /\ ( ( A gcd B ) ^ 2 ) || ( B ^ 2 ) ) )
45	2	nnsqcld 10689	. . . . . . . . . . . . . 14 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( A gcd B ) ^ 2 ) e. NN )
46	45	nnzd 9388	. . . . . . . . . . . . 13 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( A gcd B ) ^ 2 ) e. ZZ )
47		nnsqcl 10604	. . . . . . . . . . . . . . 15 |- ( A e. NN -> ( A ^ 2 ) e. NN )
48	47	3ad2ant1 1019	. . . . . . . . . . . . . 14 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( A ^ 2 ) e. NN )
49	48	nnzd 9388	. . . . . . . . . . . . 13 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( A ^ 2 ) e. ZZ )
50		nnsqcl 10604	. . . . . . . . . . . . . . 15 |- ( B e. NN -> ( B ^ 2 ) e. NN )
51	50	3ad2ant2 1020	. . . . . . . . . . . . . 14 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( B ^ 2 ) e. NN )
52	51	nnzd 9388	. . . . . . . . . . . . 13 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( B ^ 2 ) e. ZZ )
53		dvds2add 11846	. . . . . . . . . . . . 13 |- ( ( ( ( A gcd B ) ^ 2 ) e. ZZ /\ ( A ^ 2 ) e. ZZ /\ ( B ^ 2 ) e. ZZ ) -> ( ( ( ( A gcd B ) ^ 2 ) || ( A ^ 2 ) /\ ( ( A gcd B ) ^ 2 ) || ( B ^ 2 ) ) -> ( ( A gcd B ) ^ 2 ) || ( ( A ^ 2 ) + ( B ^ 2 ) ) ) )
54	46, 49, 52, 53	syl3anc 1248	. . . . . . . . . . . 12 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( ( ( A gcd B ) ^ 2 ) || ( A ^ 2 ) /\ ( ( A gcd B ) ^ 2 ) || ( B ^ 2 ) ) -> ( ( A gcd B ) ^ 2 ) || ( ( A ^ 2 ) + ( B ^ 2 ) ) ) )
55	44, 54	mpd 13	. . . . . . . . . . 11 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( A gcd B ) ^ 2 ) || ( ( A ^ 2 ) + ( B ^ 2 ) ) )
56	55	adantr 276	. . . . . . . . . 10 |- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> ( ( A gcd B ) ^ 2 ) || ( ( A ^ 2 ) + ( B ^ 2 ) ) )
57		simpr 110	. . . . . . . . . 10 |- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) )
58	56, 57	breqtrd 4041	. . . . . . . . 9 |- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> ( ( A gcd B ) ^ 2 ) || ( C ^ 2 ) )
59		nnz 9286	. . . . . . . . . . . 12 |- ( C e. NN -> C e. ZZ )
60	59	3ad2ant3 1021	. . . . . . . . . . 11 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> C e. ZZ )
61		dvdssq 12046	. . . . . . . . . . 11 |- ( ( ( A gcd B ) e. ZZ /\ C e. ZZ ) -> ( ( A gcd B ) || C <-> ( ( A gcd B ) ^ 2 ) || ( C ^ 2 ) ) )
62	10, 60, 61	syl2anc 411	. . . . . . . . . 10 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( A gcd B ) || C <-> ( ( A gcd B ) ^ 2 ) || ( C ^ 2 ) ) )
63	62	adantr 276	. . . . . . . . 9 |- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> ( ( A gcd B ) || C <-> ( ( A gcd B ) ^ 2 ) || ( C ^ 2 ) ) )
64	58, 63	mpbird 167	. . . . . . . 8 |- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> ( A gcd B ) || C )
65		dvdsval2 11811	. . . . . . . . . 10 |- ( ( ( A gcd B ) e. ZZ /\ ( A gcd B ) =/= 0 /\ C e. ZZ ) -> ( ( A gcd B ) || C <-> ( C / ( A gcd B ) ) e. ZZ ) )
66	10, 11, 60, 65	syl3anc 1248	. . . . . . . . 9 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( A gcd B ) || C <-> ( C / ( A gcd B ) ) e. ZZ ) )
67	66	adantr 276	. . . . . . . 8 |- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> ( ( A gcd B ) || C <-> ( C / ( A gcd B ) ) e. ZZ ) )
68	64, 67	mpbid 147	. . . . . . 7 |- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> ( C / ( A gcd B ) ) e. ZZ )
69		nnre 8940	. . . . . . . . . 10 |- ( C e. NN -> C e. RR )
70	69	3ad2ant3 1021	. . . . . . . . 9 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> C e. RR )
71		nngt0 8958	. . . . . . . . . 10 |- ( C e. NN -> 0 < C )
72	71	3ad2ant3 1021	. . . . . . . . 9 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> 0 < C )
73	70, 18, 72, 21	divgt0d 8906	. . . . . . . 8 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> 0 < ( C / ( A gcd B ) ) )
74	73	adantr 276	. . . . . . 7 |- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> 0 < ( C / ( A gcd B ) ) )
75		elnnz 9277	. . . . . . 7 |- ( ( C / ( A gcd B ) ) e. NN <-> ( ( C / ( A gcd B ) ) e. ZZ /\ 0 < ( C / ( A gcd B ) ) ) )
76	68, 74, 75	sylanbrc 417	. . . . . 6 |- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) -> ( C / ( A gcd B ) ) e. NN )
77	76	3adant3 1018	. . . . 5 |- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ -. 2 || ( A / ( A gcd B ) ) ) -> ( C / ( A gcd B ) ) e. NN )
78	48	nncnd 8947	. . . . . . . 8 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( A ^ 2 ) e. CC )
79	51	nncnd 8947	. . . . . . . 8 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( B ^ 2 ) e. CC )
80	45	nncnd 8947	. . . . . . . 8 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( A gcd B ) ^ 2 ) e. CC )
81	45	nnap0d 8979	. . . . . . . 8 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( A gcd B ) ^ 2 ) # 0 )
82	78, 79, 80, 81	divdirapd 8800	. . . . . . 7 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) / ( ( A gcd B ) ^ 2 ) ) = ( ( ( A ^ 2 ) / ( ( A gcd B ) ^ 2 ) ) + ( ( B ^ 2 ) / ( ( A gcd B ) ^ 2 ) ) ) )
83	82	3ad2ant1 1019	. . . . . 6 |- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ -. 2 || ( A / ( A gcd B ) ) ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) / ( ( A gcd B ) ^ 2 ) ) = ( ( ( A ^ 2 ) / ( ( A gcd B ) ^ 2 ) ) + ( ( B ^ 2 ) / ( ( A gcd B ) ^ 2 ) ) ) )
84		nncn 8941	. . . . . . . . . 10 |- ( C e. NN -> C e. CC )
85	84	3ad2ant3 1021	. . . . . . . . 9 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> C e. CC )
86	2	nncnd 8947	. . . . . . . . 9 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( A gcd B ) e. CC )
87	2	nnap0d 8979	. . . . . . . . 9 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( A gcd B ) # 0 )
88	85, 86, 87	sqdivapd 10681	. . . . . . . 8 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( C / ( A gcd B ) ) ^ 2 ) = ( ( C ^ 2 ) / ( ( A gcd B ) ^ 2 ) ) )
89	88	3ad2ant1 1019	. . . . . . 7 |- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ -. 2 || ( A / ( A gcd B ) ) ) -> ( ( C / ( A gcd B ) ) ^ 2 ) = ( ( C ^ 2 ) / ( ( A gcd B ) ^ 2 ) ) )
90		oveq1 5895	. . . . . . . 8 |- ( ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) / ( ( A gcd B ) ^ 2 ) ) = ( ( C ^ 2 ) / ( ( A gcd B ) ^ 2 ) ) )
91	90	3ad2ant2 1020	. . . . . . 7 |- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ -. 2 || ( A / ( A gcd B ) ) ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) / ( ( A gcd B ) ^ 2 ) ) = ( ( C ^ 2 ) / ( ( A gcd B ) ^ 2 ) ) )
92	89, 91	eqtr4d 2223	. . . . . 6 |- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ -. 2 || ( A / ( A gcd B ) ) ) -> ( ( C / ( A gcd B ) ) ^ 2 ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) / ( ( A gcd B ) ^ 2 ) ) )
93		nncn 8941	. . . . . . . . . 10 |- ( A e. NN -> A e. CC )
94	93	3ad2ant1 1019	. . . . . . . . 9 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> A e. CC )
95	94, 86, 87	sqdivapd 10681	. . . . . . . 8 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( A / ( A gcd B ) ) ^ 2 ) = ( ( A ^ 2 ) / ( ( A gcd B ) ^ 2 ) ) )
96		nncn 8941	. . . . . . . . . 10 |- ( B e. NN -> B e. CC )
97	96	3ad2ant2 1020	. . . . . . . . 9 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> B e. CC )
98	97, 86, 87	sqdivapd 10681	. . . . . . . 8 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( B / ( A gcd B ) ) ^ 2 ) = ( ( B ^ 2 ) / ( ( A gcd B ) ^ 2 ) ) )
99	95, 98	oveq12d 5906	. . . . . . 7 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( ( A / ( A gcd B ) ) ^ 2 ) + ( ( B / ( A gcd B ) ) ^ 2 ) ) = ( ( ( A ^ 2 ) / ( ( A gcd B ) ^ 2 ) ) + ( ( B ^ 2 ) / ( ( A gcd B ) ^ 2 ) ) ) )
100	99	3ad2ant1 1019	. . . . . 6 |- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ -. 2 || ( A / ( A gcd B ) ) ) -> ( ( ( A / ( A gcd B ) ) ^ 2 ) + ( ( B / ( A gcd B ) ) ^ 2 ) ) = ( ( ( A ^ 2 ) / ( ( A gcd B ) ^ 2 ) ) + ( ( B ^ 2 ) / ( ( A gcd B ) ^ 2 ) ) ) )
101	83, 92, 100	3eqtr4rd 2231	. . . . 5 |- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ -. 2 || ( A / ( A gcd B ) ) ) -> ( ( ( A / ( A gcd B ) ) ^ 2 ) + ( ( B / ( A gcd B ) ) ^ 2 ) ) = ( ( C / ( A gcd B ) ) ^ 2 ) )
102		gcddiv 12034	. . . . . . . 8 |- ( ( ( A e. ZZ /\ B e. ZZ /\ ( A gcd B ) e. NN ) /\ ( ( A gcd B ) || A /\ ( A gcd B ) || B ) ) -> ( ( A gcd B ) / ( A gcd B ) ) = ( ( A / ( A gcd B ) ) gcd ( B / ( A gcd B ) ) ) )
103	12, 27, 2, 8, 102	syl31anc 1251	. . . . . . 7 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( A gcd B ) / ( A gcd B ) ) = ( ( A / ( A gcd B ) ) gcd ( B / ( A gcd B ) ) ) )
104	86, 87	dividapd 8757	. . . . . . 7 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( A gcd B ) / ( A gcd B ) ) = 1 )
105	103, 104	eqtr3d 2222	. . . . . 6 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( A / ( A gcd B ) ) gcd ( B / ( A gcd B ) ) ) = 1 )
106	105	3ad2ant1 1019	. . . . 5 |- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ -. 2 || ( A / ( A gcd B ) ) ) -> ( ( A / ( A gcd B ) ) gcd ( B / ( A gcd B ) ) ) = 1 )
107		simp3 1000	. . . . 5 |- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ -. 2 || ( A / ( A gcd B ) ) ) -> -. 2 || ( A / ( A gcd B ) ) )
108		pythagtriplem18 12295	. . . . 5 |- ( ( ( ( A / ( A gcd B ) ) e. NN /\ ( B / ( A gcd B ) ) e. NN /\ ( C / ( A gcd B ) ) e. NN ) /\ ( ( ( A / ( A gcd B ) ) ^ 2 ) + ( ( B / ( A gcd B ) ) ^ 2 ) ) = ( ( C / ( A gcd B ) ) ^ 2 ) /\ ( ( ( A / ( A gcd B ) ) gcd ( B / ( A gcd B ) ) ) = 1 /\ -. 2 || ( A / ( A gcd B ) ) ) ) -> E. n e. NN E. m e. NN ( ( A / ( A gcd B ) ) = ( ( m ^ 2 ) - ( n ^ 2 ) ) /\ ( B / ( A gcd B ) ) = ( 2 x. ( m x. n ) ) /\ ( C / ( A gcd B ) ) = ( ( m ^ 2 ) + ( n ^ 2 ) ) ) )
109	25, 38, 77, 101, 106, 107, 108	syl312anc 1269	. . . 4 |- ( ( ( 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 ( ( A / ( A gcd B ) ) = ( ( m ^ 2 ) - ( n ^ 2 ) ) /\ ( B / ( A gcd B ) ) = ( 2 x. ( m x. n ) ) /\ ( C / ( A gcd B ) ) = ( ( m ^ 2 ) + ( n ^ 2 ) ) ) )
110	94, 86, 87	divcanap2d 8763	. . . . . . . . . 10 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( A gcd B ) x. ( A / ( A gcd B ) ) ) = A )
111	110	eqcomd 2193	. . . . . . . . 9 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> A = ( ( A gcd B ) x. ( A / ( A gcd B ) ) ) )
112	97, 86, 87	divcanap2d 8763	. . . . . . . . . 10 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( A gcd B ) x. ( B / ( A gcd B ) ) ) = B )
113	112	eqcomd 2193	. . . . . . . . 9 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> B = ( ( A gcd B ) x. ( B / ( A gcd B ) ) ) )
114	85, 86, 87	divcanap2d 8763	. . . . . . . . . 10 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( A gcd B ) x. ( C / ( A gcd B ) ) ) = C )
115	114	eqcomd 2193	. . . . . . . . 9 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> C = ( ( A gcd B ) x. ( C / ( A gcd B ) ) ) )
116	111, 113, 115	3jca 1178	. . . . . . . 8 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( A = ( ( A gcd B ) x. ( A / ( A gcd B ) ) ) /\ B = ( ( A gcd B ) x. ( B / ( A gcd B ) ) ) /\ C = ( ( A gcd B ) x. ( C / ( A gcd B ) ) ) ) )
117	116	3ad2ant1 1019	. . . . . . 7 |- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ -. 2 || ( A / ( A gcd B ) ) ) -> ( A = ( ( A gcd B ) x. ( A / ( A gcd B ) ) ) /\ B = ( ( A gcd B ) x. ( B / ( A gcd B ) ) ) /\ C = ( ( A gcd B ) x. ( C / ( A gcd B ) ) ) ) )
118		oveq2 5896	. . . . . . . . . 10 |- ( ( A / ( A gcd B ) ) = ( ( m ^ 2 ) - ( n ^ 2 ) ) -> ( ( A gcd B ) x. ( A / ( A gcd B ) ) ) = ( ( A gcd B ) x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) )
119	118	eqeq2d 2199	. . . . . . . . 9 |- ( ( A / ( A gcd B ) ) = ( ( m ^ 2 ) - ( n ^ 2 ) ) -> ( A = ( ( A gcd B ) x. ( A / ( A gcd B ) ) ) <-> A = ( ( A gcd B ) x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) ) )
120	119	3ad2ant1 1019	. . . . . . . 8 |- ( ( ( A / ( A gcd B ) ) = ( ( m ^ 2 ) - ( n ^ 2 ) ) /\ ( B / ( A gcd B ) ) = ( 2 x. ( m x. n ) ) /\ ( C / ( A gcd B ) ) = ( ( m ^ 2 ) + ( n ^ 2 ) ) ) -> ( A = ( ( A gcd B ) x. ( A / ( A gcd B ) ) ) <-> A = ( ( A gcd B ) x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) ) )
121		oveq2 5896	. . . . . . . . . 10 |- ( ( B / ( A gcd B ) ) = ( 2 x. ( m x. n ) ) -> ( ( A gcd B ) x. ( B / ( A gcd B ) ) ) = ( ( A gcd B ) x. ( 2 x. ( m x. n ) ) ) )
122	121	eqeq2d 2199	. . . . . . . . 9 |- ( ( B / ( A gcd B ) ) = ( 2 x. ( m x. n ) ) -> ( B = ( ( A gcd B ) x. ( B / ( A gcd B ) ) ) <-> B = ( ( A gcd B ) x. ( 2 x. ( m x. n ) ) ) ) )
123	122	3ad2ant2 1020	. . . . . . . 8 |- ( ( ( A / ( A gcd B ) ) = ( ( m ^ 2 ) - ( n ^ 2 ) ) /\ ( B / ( A gcd B ) ) = ( 2 x. ( m x. n ) ) /\ ( C / ( A gcd B ) ) = ( ( m ^ 2 ) + ( n ^ 2 ) ) ) -> ( B = ( ( A gcd B ) x. ( B / ( A gcd B ) ) ) <-> B = ( ( A gcd B ) x. ( 2 x. ( m x. n ) ) ) ) )
124		oveq2 5896	. . . . . . . . . 10 |- ( ( C / ( A gcd B ) ) = ( ( m ^ 2 ) + ( n ^ 2 ) ) -> ( ( A gcd B ) x. ( C / ( A gcd B ) ) ) = ( ( A gcd B ) x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) )
125	124	eqeq2d 2199	. . . . . . . . 9 |- ( ( C / ( A gcd B ) ) = ( ( m ^ 2 ) + ( n ^ 2 ) ) -> ( C = ( ( A gcd B ) x. ( C / ( A gcd B ) ) ) <-> C = ( ( A gcd B ) x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) )
126	125	3ad2ant3 1021	. . . . . . . 8 |- ( ( ( A / ( A gcd B ) ) = ( ( m ^ 2 ) - ( n ^ 2 ) ) /\ ( B / ( A gcd B ) ) = ( 2 x. ( m x. n ) ) /\ ( C / ( A gcd B ) ) = ( ( m ^ 2 ) + ( n ^ 2 ) ) ) -> ( C = ( ( A gcd B ) x. ( C / ( A gcd B ) ) ) <-> C = ( ( A gcd B ) x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) )
127	120, 123, 126	3anbi123d 1322	. . . . . . 7 |- ( ( ( A / ( A gcd B ) ) = ( ( m ^ 2 ) - ( n ^ 2 ) ) /\ ( B / ( A gcd B ) ) = ( 2 x. ( m x. n ) ) /\ ( C / ( A gcd B ) ) = ( ( m ^ 2 ) + ( n ^ 2 ) ) ) -> ( ( A = ( ( A gcd B ) x. ( A / ( A gcd B ) ) ) /\ B = ( ( A gcd B ) x. ( B / ( A gcd B ) ) ) /\ C = ( ( A gcd B ) x. ( C / ( A gcd B ) ) ) ) <-> ( A = ( ( A gcd B ) x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( ( A gcd B ) x. ( 2 x. ( m x. n ) ) ) /\ C = ( ( A gcd B ) x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
128	117, 127	syl5ibcom 155	. . . . . 6 |- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ -. 2 || ( A / ( A gcd B ) ) ) -> ( ( ( A / ( A gcd B ) ) = ( ( m ^ 2 ) - ( n ^ 2 ) ) /\ ( B / ( A gcd B ) ) = ( 2 x. ( m x. n ) ) /\ ( C / ( A gcd B ) ) = ( ( m ^ 2 ) + ( n ^ 2 ) ) ) -> ( A = ( ( A gcd B ) x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( ( A gcd B ) x. ( 2 x. ( m x. n ) ) ) /\ C = ( ( A gcd B ) x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
129	128	reximdv 2588	. . . . 5 |- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ -. 2 || ( A / ( A gcd B ) ) ) -> ( E. m e. NN ( ( A / ( A gcd B ) ) = ( ( m ^ 2 ) - ( n ^ 2 ) ) /\ ( B / ( A gcd B ) ) = ( 2 x. ( m x. n ) ) /\ ( C / ( A gcd B ) ) = ( ( m ^ 2 ) + ( n ^ 2 ) ) ) -> E. m e. NN ( A = ( ( A gcd B ) x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( ( A gcd B ) x. ( 2 x. ( m x. n ) ) ) /\ C = ( ( A gcd B ) x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
130	129	reximdv 2588	. . . 4 |- ( ( ( 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 ( ( A / ( A gcd B ) ) = ( ( m ^ 2 ) - ( n ^ 2 ) ) /\ ( B / ( A gcd B ) ) = ( 2 x. ( m x. n ) ) /\ ( C / ( A gcd B ) ) = ( ( m ^ 2 ) + ( n ^ 2 ) ) ) -> E. n e. NN E. m e. NN ( A = ( ( A gcd B ) x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( ( A gcd B ) x. ( 2 x. ( m x. n ) ) ) /\ C = ( ( A gcd B ) x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
131	109, 130	mpd 13	. . 3 |- ( ( ( 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 ( A = ( ( A gcd B ) x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( ( A gcd B ) x. ( 2 x. ( m x. n ) ) ) /\ C = ( ( A gcd B ) x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) )
132		oveq1 5895	. . . . . . 7 |- ( k = ( A gcd B ) -> ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) = ( ( A gcd B ) x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) )
133	132	eqeq2d 2199	. . . . . 6 |- ( k = ( A gcd B ) -> ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) <-> A = ( ( A gcd B ) x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) ) )
134		oveq1 5895	. . . . . . 7 |- ( k = ( A gcd B ) -> ( k x. ( 2 x. ( m x. n ) ) ) = ( ( A gcd B ) x. ( 2 x. ( m x. n ) ) ) )
135	134	eqeq2d 2199	. . . . . 6 |- ( k = ( A gcd B ) -> ( B = ( k x. ( 2 x. ( m x. n ) ) ) <-> B = ( ( A gcd B ) x. ( 2 x. ( m x. n ) ) ) ) )
136		oveq1 5895	. . . . . . 7 |- ( k = ( A gcd B ) -> ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) = ( ( A gcd B ) x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) )
137	136	eqeq2d 2199	. . . . . 6 |- ( k = ( A gcd B ) -> ( C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) <-> C = ( ( A gcd B ) x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) )
138	133, 135, 137	3anbi123d 1322	. . . . 5 |- ( k = ( A gcd B ) -> ( ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) <-> ( A = ( ( A gcd B ) x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( ( A gcd B ) x. ( 2 x. ( m x. n ) ) ) /\ C = ( ( A gcd B ) x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
139	138	2rexbidv 2512	. . . 4 |- ( k = ( A gcd B ) -> ( E. n e. NN E. m 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 ( A = ( ( A gcd B ) x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( ( A gcd B ) x. ( 2 x. ( m x. n ) ) ) /\ C = ( ( A gcd B ) x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) )
140	139	rspcev 2853	. . 3 |- ( ( ( A gcd B ) e. NN /\ E. n e. NN E. m e. NN ( A = ( ( A gcd B ) x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( ( A gcd B ) x. ( 2 x. ( m x. n ) ) ) /\ C = ( ( A gcd B ) x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) -> E. k e. NN E. n e. NN E. m e. NN ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) )
141	3, 131, 140	syl2anc 411	. 2 |- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ -. 2 || ( A / ( A gcd B ) ) ) -> E. k e. NN E. n e. NN E. m e. NN ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) )
142		rexcom 2651	. . 3 |- ( E. k e. NN E. n e. NN E. m 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. k e. NN E. m e. NN ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) )
143		rexcom 2651	. . . 4 |- ( E. k e. NN E. m 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 ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) )
144	143	rexbii 2494	. . 3 |- ( E. n e. NN E. k e. NN E. m 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 ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) )
145	142, 144	bitri 184	. 2 |- ( E. k e. NN E. n e. NN E. m 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 ( A = ( k x. ( ( m ^ 2 ) - ( n ^ 2 ) ) ) /\ B = ( k x. ( 2 x. ( m x. n ) ) ) /\ C = ( k x. ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) )
146	141, 145	sylib 122	1 |- ( ( ( 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 ) ) ) ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   <-> wb 105   /\ w3a 979   = wceq 1363   e. wcel 2158   =/= wne 2357   E.wrex 2466   class class class wbr 4015  (class class class)co 5888   CCcc 7823   RRcr 7824   0cc0 7825   1c1 7826   + caddc 7828   x. cmul 7830   < clt 8006   - cmin 8142   / cdiv 8643   NNcn 8933   2c2 8984   ZZcz 9267   ^cexp 10533   || cdvds 11808   gcd cgcd 11957

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-13 2160  ax-14 2161  ax-ext 2169  ax-coll 4130  ax-sep 4133  ax-nul 4141  ax-pow 4186  ax-pr 4221  ax-un 4445  ax-setind 4548  ax-iinf 4599  ax-cnex 7916  ax-resscn 7917  ax-1cn 7918  ax-1re 7919  ax-icn 7920  ax-addcl 7921  ax-addrcl 7922  ax-mulcl 7923  ax-mulrcl 7924  ax-addcom 7925  ax-mulcom 7926  ax-addass 7927  ax-mulass 7928  ax-distr 7929  ax-i2m1 7930  ax-0lt1 7931  ax-1rid 7932  ax-0id 7933  ax-rnegex 7934  ax-precex 7935  ax-cnre 7936  ax-pre-ltirr 7937  ax-pre-ltwlin 7938  ax-pre-lttrn 7939  ax-pre-apti 7940  ax-pre-ltadd 7941  ax-pre-mulgt0 7942  ax-pre-mulext 7943  ax-arch 7944  ax-caucvg 7945

This theorem depends on definitions:  df-bi 117  df-stab 832  df-dc 836  df-3or 980  df-3an 981  df-tru 1366  df-fal 1369  df-xor 1386  df-nf 1471  df-sb 1773  df-eu 2039  df-mo 2040  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-ne 2358  df-nel 2453  df-ral 2470  df-rex 2471  df-reu 2472  df-rmo 2473  df-rab 2474  df-v 2751  df-sbc 2975  df-csb 3070  df-dif 3143  df-un 3145  df-in 3147  df-ss 3154  df-nul 3435  df-if 3547  df-pw 3589  df-sn 3610  df-pr 3611  df-op 3613  df-uni 3822  df-int 3857  df-iun 3900  df-br 4016  df-opab 4077  df-mpt 4078  df-tr 4114  df-id 4305  df-po 4308  df-iso 4309  df-iord 4378  df-on 4380  df-ilim 4381  df-suc 4383  df-iom 4602  df-xp 4644  df-rel 4645  df-cnv 4646  df-co 4647  df-dm 4648  df-rn 4649  df-res 4650  df-ima 4651  df-iota 5190  df-fun 5230  df-fn 5231  df-f 5232  df-f1 5233  df-fo 5234  df-f1o 5235  df-fv 5236  df-riota 5844  df-ov 5891  df-oprab 5892  df-mpo 5893  df-1st 6155  df-2nd 6156  df-recs 6320  df-frec 6406  df-1o 6431  df-2o 6432  df-er 6549  df-en 6755  df-sup 6997  df-pnf 8008  df-mnf 8009  df-xr 8010  df-ltxr 8011  df-le 8012  df-sub 8144  df-neg 8145  df-reap 8546  df-ap 8553  df-div 8644  df-inn 8934  df-2 8992  df-3 8993  df-4 8994  df-n0 9191  df-z 9268  df-uz 9543  df-q 9634  df-rp 9668  df-fz 10023  df-fzo 10157  df-fl 10284  df-mod 10337  df-seqfrec 10460  df-exp 10534  df-cj 10865  df-re 10866  df-im 10867  df-rsqrt 11021  df-abs 11022  df-dvds 11809  df-gcd 11958  df-prm 12122

This theorem is referenced by:  pythagtrip  12297