Theorem nna4b4nsq

Description: Strengthening of Fermat's last theorem for exponent 4, where the sum is only assumed to be a square. (Contributed by SN, 23-Aug-2024)

	Ref	Expression
Hypotheses	nna4b4nsq.a	|- ( ph -> A e. NN )
	nna4b4nsq.b	|- ( ph -> B e. NN )
	nna4b4nsq.c	|- ( ph -> C e. NN )
Assertion	nna4b4nsq	|- ( ph -> ( ( A ^ 4 ) + ( B ^ 4 ) ) =/= ( C ^ 2 ) )

Proof

Step	Hyp	Ref	Expression
1		nna4b4nsq.a	|- ( ph -> A e. NN )
2		nna4b4nsq.b	|- ( ph -> B e. NN )
3		nna4b4nsq.c	|- ( ph -> C e. NN )
4		oveq1	|- ( a = A -> ( a ^ 4 ) = ( A ^ 4 ) )
5	4	oveq1d	|- ( a = A -> ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( ( A ^ 4 ) + ( b ^ 4 ) ) )
6	5	eqeq1d	|- ( a = A -> ( ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) <-> ( ( A ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) )
7		oveq1	|- ( b = B -> ( b ^ 4 ) = ( B ^ 4 ) )
8	7	oveq2d	|- ( b = B -> ( ( A ^ 4 ) + ( b ^ 4 ) ) = ( ( A ^ 4 ) + ( B ^ 4 ) ) )
9	8	eqeq1d	|- ( b = B -> ( ( ( A ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) <-> ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( c ^ 2 ) ) )
10	1	ad2antrr	|- ( ( ( ph /\ c e. NN ) /\ ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( c ^ 2 ) ) -> A e. NN )
11	2	ad2antrr	|- ( ( ( ph /\ c e. NN ) /\ ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( c ^ 2 ) ) -> B e. NN )
12		simpr	|- ( ( ( ph /\ c e. NN ) /\ ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( c ^ 2 ) ) -> ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( c ^ 2 ) )
13	6 9 10 11 12	2rspcedvdw	|- ( ( ( ph /\ c e. NN ) /\ ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( c ^ 2 ) ) -> E. a e. NN E. b e. NN ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) )
14	13	ex	|- ( ( ph /\ c e. NN ) -> ( ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( c ^ 2 ) -> E. a e. NN E. b e. NN ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) )
15	14	ss2rabdv	|- ( ph -> { c e. NN | ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( c ^ 2 ) } C_ { c e. NN | E. a e. NN E. b e. NN ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) } )
16		oveq1	|- ( f = i -> ( f ^ 2 ) = ( i ^ 2 ) )
17	16	eqeq2d	|- ( f = i -> ( ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) <-> ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( i ^ 2 ) ) )
18	17	anbi2d	|- ( f = i -> ( ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) <-> ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( i ^ 2 ) ) ) )
19	18	anbi2d	|- ( f = i -> ( ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) ) <-> ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( i ^ 2 ) ) ) ) )
20	19	2rexbidv	|- ( f = i -> ( E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) ) <-> E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( i ^ 2 ) ) ) ) )
21		oveq1	|- ( f = l -> ( f ^ 2 ) = ( l ^ 2 ) )
22	21	eqeq2d	|- ( f = l -> ( ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) <-> ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( l ^ 2 ) ) )
23	22	anbi2d	|- ( f = l -> ( ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) <-> ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( l ^ 2 ) ) ) )
24	23	anbi2d	|- ( f = l -> ( ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) ) <-> ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( l ^ 2 ) ) ) ) )
25	24	2rexbidv	|- ( f = l -> ( E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) ) <-> E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( l ^ 2 ) ) ) ) )
26		nnuz	|- NN = ( ZZ>= ` 1 )
27	26	eqimssi	|- NN C_ ( ZZ>= ` 1 )
28	27	a1i	|- ( ph -> NN C_ ( ZZ>= ` 1 ) )
29		breq2	|- ( g = j -> ( 2 || g <-> 2 || j ) )
30	29	notbid	|- ( g = j -> ( -. 2 || g <-> -. 2 || j ) )
31		oveq1	|- ( g = j -> ( g gcd h ) = ( j gcd h ) )
32	31	eqeq1d	|- ( g = j -> ( ( g gcd h ) = 1 <-> ( j gcd h ) = 1 ) )
33		oveq1	|- ( g = j -> ( g ^ 4 ) = ( j ^ 4 ) )
34	33	oveq1d	|- ( g = j -> ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( ( j ^ 4 ) + ( h ^ 4 ) ) )
35	34	eqeq1d	|- ( g = j -> ( ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( i ^ 2 ) <-> ( ( j ^ 4 ) + ( h ^ 4 ) ) = ( i ^ 2 ) ) )
36	32 35	anbi12d	|- ( g = j -> ( ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( i ^ 2 ) ) <-> ( ( j gcd h ) = 1 /\ ( ( j ^ 4 ) + ( h ^ 4 ) ) = ( i ^ 2 ) ) ) )
37	30 36	anbi12d	|- ( g = j -> ( ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( i ^ 2 ) ) ) <-> ( -. 2 || j /\ ( ( j gcd h ) = 1 /\ ( ( j ^ 4 ) + ( h ^ 4 ) ) = ( i ^ 2 ) ) ) ) )
38		oveq2	|- ( h = k -> ( j gcd h ) = ( j gcd k ) )
39	38	eqeq1d	|- ( h = k -> ( ( j gcd h ) = 1 <-> ( j gcd k ) = 1 ) )
40		oveq1	|- ( h = k -> ( h ^ 4 ) = ( k ^ 4 ) )
41	40	oveq2d	|- ( h = k -> ( ( j ^ 4 ) + ( h ^ 4 ) ) = ( ( j ^ 4 ) + ( k ^ 4 ) ) )
42	41	eqeq1d	|- ( h = k -> ( ( ( j ^ 4 ) + ( h ^ 4 ) ) = ( i ^ 2 ) <-> ( ( j ^ 4 ) + ( k ^ 4 ) ) = ( i ^ 2 ) ) )
43	39 42	anbi12d	|- ( h = k -> ( ( ( j gcd h ) = 1 /\ ( ( j ^ 4 ) + ( h ^ 4 ) ) = ( i ^ 2 ) ) <-> ( ( j gcd k ) = 1 /\ ( ( j ^ 4 ) + ( k ^ 4 ) ) = ( i ^ 2 ) ) ) )
44	43	anbi2d	|- ( h = k -> ( ( -. 2 || j /\ ( ( j gcd h ) = 1 /\ ( ( j ^ 4 ) + ( h ^ 4 ) ) = ( i ^ 2 ) ) ) <-> ( -. 2 || j /\ ( ( j gcd k ) = 1 /\ ( ( j ^ 4 ) + ( k ^ 4 ) ) = ( i ^ 2 ) ) ) ) )
45	37 44	cbvrex2vw	|- ( E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( i ^ 2 ) ) ) <-> E. j e. NN E. k e. NN ( -. 2 || j /\ ( ( j gcd k ) = 1 /\ ( ( j ^ 4 ) + ( k ^ 4 ) ) = ( i ^ 2 ) ) ) )
46		simplrl	|- ( ( ( ( ph /\ i e. NN ) /\ ( j e. NN /\ k e. NN ) ) /\ ( -. 2 || j /\ ( ( j gcd k ) = 1 /\ ( ( j ^ 4 ) + ( k ^ 4 ) ) = ( i ^ 2 ) ) ) ) -> j e. NN )
47		simplrr	|- ( ( ( ( ph /\ i e. NN ) /\ ( j e. NN /\ k e. NN ) ) /\ ( -. 2 || j /\ ( ( j gcd k ) = 1 /\ ( ( j ^ 4 ) + ( k ^ 4 ) ) = ( i ^ 2 ) ) ) ) -> k e. NN )
48		simpllr	|- ( ( ( ( ph /\ i e. NN ) /\ ( j e. NN /\ k e. NN ) ) /\ ( -. 2 || j /\ ( ( j gcd k ) = 1 /\ ( ( j ^ 4 ) + ( k ^ 4 ) ) = ( i ^ 2 ) ) ) ) -> i e. NN )
49		simprl	|- ( ( ( ( ph /\ i e. NN ) /\ ( j e. NN /\ k e. NN ) ) /\ ( -. 2 || j /\ ( ( j gcd k ) = 1 /\ ( ( j ^ 4 ) + ( k ^ 4 ) ) = ( i ^ 2 ) ) ) ) -> -. 2 || j )
50		simprrl	|- ( ( ( ( ph /\ i e. NN ) /\ ( j e. NN /\ k e. NN ) ) /\ ( -. 2 || j /\ ( ( j gcd k ) = 1 /\ ( ( j ^ 4 ) + ( k ^ 4 ) ) = ( i ^ 2 ) ) ) ) -> ( j gcd k ) = 1 )
51		simprrr	|- ( ( ( ( ph /\ i e. NN ) /\ ( j e. NN /\ k e. NN ) ) /\ ( -. 2 || j /\ ( ( j gcd k ) = 1 /\ ( ( j ^ 4 ) + ( k ^ 4 ) ) = ( i ^ 2 ) ) ) ) -> ( ( j ^ 4 ) + ( k ^ 4 ) ) = ( i ^ 2 ) )
52	46 47 48 49 50 51	flt4lem7	|- ( ( ( ( ph /\ i e. NN ) /\ ( j e. NN /\ k e. NN ) ) /\ ( -. 2 || j /\ ( ( j gcd k ) = 1 /\ ( ( j ^ 4 ) + ( k ^ 4 ) ) = ( i ^ 2 ) ) ) ) -> E. l e. NN ( E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( l ^ 2 ) ) ) /\ l < i ) )
53	52	ex	|- ( ( ( ph /\ i e. NN ) /\ ( j e. NN /\ k e. NN ) ) -> ( ( -. 2 || j /\ ( ( j gcd k ) = 1 /\ ( ( j ^ 4 ) + ( k ^ 4 ) ) = ( i ^ 2 ) ) ) -> E. l e. NN ( E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( l ^ 2 ) ) ) /\ l < i ) ) )
54	53	rexlimdvva	|- ( ( ph /\ i e. NN ) -> ( E. j e. NN E. k e. NN ( -. 2 || j /\ ( ( j gcd k ) = 1 /\ ( ( j ^ 4 ) + ( k ^ 4 ) ) = ( i ^ 2 ) ) ) -> E. l e. NN ( E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( l ^ 2 ) ) ) /\ l < i ) ) )
55	45 54	biimtrid	|- ( ( ph /\ i e. NN ) -> ( E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( i ^ 2 ) ) ) -> E. l e. NN ( E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( l ^ 2 ) ) ) /\ l < i ) ) )
56	55	impr	|- ( ( ph /\ ( i e. NN /\ E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( i ^ 2 ) ) ) ) ) -> E. l e. NN ( E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( l ^ 2 ) ) ) /\ l < i ) )
57	20 25 28 56	infdesc	|- ( ph -> { f e. NN | E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) ) } = (/) )
58		breq2	|- ( g = d -> ( 2 || g <-> 2 || d ) )
59	58	notbid	|- ( g = d -> ( -. 2 || g <-> -. 2 || d ) )
60		oveq1	|- ( g = d -> ( g gcd h ) = ( d gcd h ) )
61	60	eqeq1d	|- ( g = d -> ( ( g gcd h ) = 1 <-> ( d gcd h ) = 1 ) )
62		oveq1	|- ( g = d -> ( g ^ 4 ) = ( d ^ 4 ) )
63	62	oveq1d	|- ( g = d -> ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( ( d ^ 4 ) + ( h ^ 4 ) ) )
64	63	eqeq1d	|- ( g = d -> ( ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) <-> ( ( d ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) )
65	61 64	anbi12d	|- ( g = d -> ( ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) <-> ( ( d gcd h ) = 1 /\ ( ( d ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) ) )
66	59 65	anbi12d	|- ( g = d -> ( ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) ) <-> ( -. 2 || d /\ ( ( d gcd h ) = 1 /\ ( ( d ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) ) ) )
67		oveq2	|- ( h = e -> ( d gcd h ) = ( d gcd e ) )
68	67	eqeq1d	|- ( h = e -> ( ( d gcd h ) = 1 <-> ( d gcd e ) = 1 ) )
69		oveq1	|- ( h = e -> ( h ^ 4 ) = ( e ^ 4 ) )
70	69	oveq2d	|- ( h = e -> ( ( d ^ 4 ) + ( h ^ 4 ) ) = ( ( d ^ 4 ) + ( e ^ 4 ) ) )
71	70	eqeq1d	|- ( h = e -> ( ( ( d ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) <-> ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) )
72	68 71	anbi12d	|- ( h = e -> ( ( ( d gcd h ) = 1 /\ ( ( d ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) <-> ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) )
73	72	anbi2d	|- ( h = e -> ( ( -. 2 || d /\ ( ( d gcd h ) = 1 /\ ( ( d ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) ) <-> ( -. 2 || d /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) ) )
74		simprl	|- ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) -> d e. NN )
75	74	ad2antrr	|- ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ -. 2 || d ) -> d e. NN )
76		simprr	|- ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) -> e e. NN )
77	76	ad2antrr	|- ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ -. 2 || d ) -> e e. NN )
78		simpr	|- ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ -. 2 || d ) -> -. 2 || d )
79		simplr	|- ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ -. 2 || d ) -> ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) )
80	78 79	jca	|- ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ -. 2 || d ) -> ( -. 2 || d /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) )
81	66 73 75 77 80	2rspcedvdw	|- ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ -. 2 || d ) -> E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) ) )
82		breq2	|- ( g = e -> ( 2 || g <-> 2 || e ) )
83	82	notbid	|- ( g = e -> ( -. 2 || g <-> -. 2 || e ) )
84		oveq1	|- ( g = e -> ( g gcd h ) = ( e gcd h ) )
85	84	eqeq1d	|- ( g = e -> ( ( g gcd h ) = 1 <-> ( e gcd h ) = 1 ) )
86		oveq1	|- ( g = e -> ( g ^ 4 ) = ( e ^ 4 ) )
87	86	oveq1d	|- ( g = e -> ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( ( e ^ 4 ) + ( h ^ 4 ) ) )
88	87	eqeq1d	|- ( g = e -> ( ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) <-> ( ( e ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) )
89	85 88	anbi12d	|- ( g = e -> ( ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) <-> ( ( e gcd h ) = 1 /\ ( ( e ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) ) )
90	83 89	anbi12d	|- ( g = e -> ( ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) ) <-> ( -. 2 || e /\ ( ( e gcd h ) = 1 /\ ( ( e ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) ) ) )
91		oveq2	|- ( h = d -> ( e gcd h ) = ( e gcd d ) )
92	91	eqeq1d	|- ( h = d -> ( ( e gcd h ) = 1 <-> ( e gcd d ) = 1 ) )
93		oveq1	|- ( h = d -> ( h ^ 4 ) = ( d ^ 4 ) )
94	93	oveq2d	|- ( h = d -> ( ( e ^ 4 ) + ( h ^ 4 ) ) = ( ( e ^ 4 ) + ( d ^ 4 ) ) )
95	94	eqeq1d	|- ( h = d -> ( ( ( e ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) <-> ( ( e ^ 4 ) + ( d ^ 4 ) ) = ( f ^ 2 ) ) )
96	92 95	anbi12d	|- ( h = d -> ( ( ( e gcd h ) = 1 /\ ( ( e ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) <-> ( ( e gcd d ) = 1 /\ ( ( e ^ 4 ) + ( d ^ 4 ) ) = ( f ^ 2 ) ) ) )
97	96	anbi2d	|- ( h = d -> ( ( -. 2 || e /\ ( ( e gcd h ) = 1 /\ ( ( e ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) ) <-> ( -. 2 || e /\ ( ( e gcd d ) = 1 /\ ( ( e ^ 4 ) + ( d ^ 4 ) ) = ( f ^ 2 ) ) ) ) )
98	76	ad2antrr	|- ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ -. 2 || e ) -> e e. NN )
99	74	ad2antrr	|- ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ -. 2 || e ) -> d e. NN )
100		simpr	|- ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ -. 2 || e ) -> -. 2 || e )
101	98	nnzd	|- ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ -. 2 || e ) -> e e. ZZ )
102	99	nnzd	|- ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ -. 2 || e ) -> d e. ZZ )
103	101 102	gcdcomd	|- ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ -. 2 || e ) -> ( e gcd d ) = ( d gcd e ) )
104		simplrl	|- ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ -. 2 || e ) -> ( d gcd e ) = 1 )
105	103 104	eqtrd	|- ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ -. 2 || e ) -> ( e gcd d ) = 1 )
106		4nn0	|- 4 e. NN0
107	106	a1i	|- ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ -. 2 || e ) -> 4 e. NN0 )
108	98 107	nnexpcld	|- ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ -. 2 || e ) -> ( e ^ 4 ) e. NN )
109	108	nncnd	|- ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ -. 2 || e ) -> ( e ^ 4 ) e. CC )
110	99 107	nnexpcld	|- ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ -. 2 || e ) -> ( d ^ 4 ) e. NN )
111	110	nncnd	|- ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ -. 2 || e ) -> ( d ^ 4 ) e. CC )
112	109 111	addcomd	|- ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ -. 2 || e ) -> ( ( e ^ 4 ) + ( d ^ 4 ) ) = ( ( d ^ 4 ) + ( e ^ 4 ) ) )
113		simplrr	|- ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ -. 2 || e ) -> ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) )
114	112 113	eqtrd	|- ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ -. 2 || e ) -> ( ( e ^ 4 ) + ( d ^ 4 ) ) = ( f ^ 2 ) )
115	100 105 114	jca32	|- ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ -. 2 || e ) -> ( -. 2 || e /\ ( ( e gcd d ) = 1 /\ ( ( e ^ 4 ) + ( d ^ 4 ) ) = ( f ^ 2 ) ) ) )
116	90 97 98 99 115	2rspcedvdw	|- ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ -. 2 || e ) -> E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) ) )
117	74	ad2antrr	|- ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ 2 || d ) -> d e. NN )
118	117	nnsqcld	|- ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ 2 || d ) -> ( d ^ 2 ) e. NN )
119	76	ad2antrr	|- ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ 2 || d ) -> e e. NN )
120	119	nnsqcld	|- ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ 2 || d ) -> ( e ^ 2 ) e. NN )
121		simp-4r	|- ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ 2 || d ) -> f e. NN )
122		2z	|- 2 e. ZZ
123		simplrl	|- ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) -> d e. NN )
124	123	nnzd	|- ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) -> d e. ZZ )
125		2nn	|- 2 e. NN
126	125	a1i	|- ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) -> 2 e. NN )
127		dvdsexp2im	|- ( ( 2 e. ZZ /\ d e. ZZ /\ 2 e. NN ) -> ( 2 || d -> 2 || ( d ^ 2 ) ) )
128	122 124 126 127	mp3an2i	|- ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) -> ( 2 || d -> 2 || ( d ^ 2 ) ) )
129	128	imp	|- ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ 2 || d ) -> 2 || ( d ^ 2 ) )
130		2nn0	|- 2 e. NN0
131	130	a1i	|- ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ 2 || d ) -> 2 e. NN0 )
132	117	nncnd	|- ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ 2 || d ) -> d e. CC )
133	132	flt4lem	|- ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ 2 || d ) -> ( d ^ 4 ) = ( ( d ^ 2 ) ^ 2 ) )
134	119	nncnd	|- ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ 2 || d ) -> e e. CC )
135	134	flt4lem	|- ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ 2 || d ) -> ( e ^ 4 ) = ( ( e ^ 2 ) ^ 2 ) )
136	133 135	oveq12d	|- ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ 2 || d ) -> ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( ( ( d ^ 2 ) ^ 2 ) + ( ( e ^ 2 ) ^ 2 ) ) )
137		simplrr	|- ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ 2 || d ) -> ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) )
138	136 137	eqtr3d	|- ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ 2 || d ) -> ( ( ( d ^ 2 ) ^ 2 ) + ( ( e ^ 2 ) ^ 2 ) ) = ( f ^ 2 ) )
139		simplrl	|- ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ 2 || d ) -> ( d gcd e ) = 1 )
140	125	a1i	|- ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ 2 || d ) -> 2 e. NN )
141		rppwr	|- ( ( d e. NN /\ e e. NN /\ 2 e. NN ) -> ( ( d gcd e ) = 1 -> ( ( d ^ 2 ) gcd ( e ^ 2 ) ) = 1 ) )
142	117 119 140 141	syl3anc	|- ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ 2 || d ) -> ( ( d gcd e ) = 1 -> ( ( d ^ 2 ) gcd ( e ^ 2 ) ) = 1 ) )
143	139 142	mpd	|- ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ 2 || d ) -> ( ( d ^ 2 ) gcd ( e ^ 2 ) ) = 1 )
144	118 120 121 131 138 143	fltaccoprm	|- ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ 2 || d ) -> ( ( d ^ 2 ) gcd f ) = 1 )
145	118 120 121 129 144 138	flt4lem2	|- ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ 2 || d ) -> -. 2 || ( e ^ 2 ) )
146	119	nnzd	|- ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ 2 || d ) -> e e. ZZ )
147		dvdsexp2im	|- ( ( 2 e. ZZ /\ e e. ZZ /\ 2 e. NN ) -> ( 2 || e -> 2 || ( e ^ 2 ) ) )
148	122 146 140 147	mp3an2i	|- ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ 2 || d ) -> ( 2 || e -> 2 || ( e ^ 2 ) ) )
149	145 148	mtod	|- ( ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) /\ 2 || d ) -> -. 2 || e )
150	149	ex	|- ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) -> ( 2 || d -> -. 2 || e ) )
151		imor	|- ( ( 2 || d -> -. 2 || e ) <-> ( -. 2 || d \/ -. 2 || e ) )
152	150 151	sylib	|- ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) -> ( -. 2 || d \/ -. 2 || e ) )
153	81 116 152	mpjaodan	|- ( ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) /\ ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) -> E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) ) )
154	153	ex	|- ( ( ( ph /\ f e. NN ) /\ ( d e. NN /\ e e. NN ) ) -> ( ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) -> E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) ) ) )
155	154	rexlimdvva	|- ( ( ph /\ f e. NN ) -> ( E. d e. NN E. e e. NN ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) -> E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) ) ) )
156	155	reximdva	|- ( ph -> ( E. f e. NN E. d e. NN E. e e. NN ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) -> E. f e. NN E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) ) ) )
157	156	con3d	|- ( ph -> ( -. E. f e. NN E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) ) -> -. E. f e. NN E. d e. NN E. e e. NN ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) )
158		ralnex	|- ( A. f e. NN -. E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) ) <-> -. E. f e. NN E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) ) )
159		ralnex	|- ( A. f e. NN -. E. d e. NN E. e e. NN ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) <-> -. E. f e. NN E. d e. NN E. e e. NN ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) )
160	157 158 159	3imtr4g	|- ( ph -> ( A. f e. NN -. E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) ) -> A. f e. NN -. E. d e. NN E. e e. NN ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) )
161		rabeq0	|- ( { f e. NN | E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) ) } = (/) <-> A. f e. NN -. E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) ) )
162		rabeq0	|- ( { f e. NN | E. d e. NN E. e e. NN ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) } = (/) <-> A. f e. NN -. E. d e. NN E. e e. NN ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) )
163	160 161 162	3imtr4g	|- ( ph -> ( { f e. NN | E. g e. NN E. h e. NN ( -. 2 || g /\ ( ( g gcd h ) = 1 /\ ( ( g ^ 4 ) + ( h ^ 4 ) ) = ( f ^ 2 ) ) ) } = (/) -> { f e. NN | E. d e. NN E. e e. NN ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) } = (/) ) )
164	57 163	mpd	|- ( ph -> { f e. NN | E. d e. NN E. e e. NN ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) } = (/) )
165		oveq1	|- ( f = ( c / ( ( a gcd b ) ^ 2 ) ) -> ( f ^ 2 ) = ( ( c / ( ( a gcd b ) ^ 2 ) ) ^ 2 ) )
166	165	eqeq2d	|- ( f = ( c / ( ( a gcd b ) ^ 2 ) ) -> ( ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) <-> ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( ( c / ( ( a gcd b ) ^ 2 ) ) ^ 2 ) ) )
167	166	anbi2d	|- ( f = ( c / ( ( a gcd b ) ^ 2 ) ) -> ( ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) <-> ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( ( c / ( ( a gcd b ) ^ 2 ) ) ^ 2 ) ) ) )
168		oveq1	|- ( d = ( a / ( a gcd b ) ) -> ( d gcd e ) = ( ( a / ( a gcd b ) ) gcd e ) )
169	168	eqeq1d	|- ( d = ( a / ( a gcd b ) ) -> ( ( d gcd e ) = 1 <-> ( ( a / ( a gcd b ) ) gcd e ) = 1 ) )
170		oveq1	|- ( d = ( a / ( a gcd b ) ) -> ( d ^ 4 ) = ( ( a / ( a gcd b ) ) ^ 4 ) )
171	170	oveq1d	|- ( d = ( a / ( a gcd b ) ) -> ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( ( ( a / ( a gcd b ) ) ^ 4 ) + ( e ^ 4 ) ) )
172	171	eqeq1d	|- ( d = ( a / ( a gcd b ) ) -> ( ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( ( c / ( ( a gcd b ) ^ 2 ) ) ^ 2 ) <-> ( ( ( a / ( a gcd b ) ) ^ 4 ) + ( e ^ 4 ) ) = ( ( c / ( ( a gcd b ) ^ 2 ) ) ^ 2 ) ) )
173	169 172	anbi12d	|- ( d = ( a / ( a gcd b ) ) -> ( ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( ( c / ( ( a gcd b ) ^ 2 ) ) ^ 2 ) ) <-> ( ( ( a / ( a gcd b ) ) gcd e ) = 1 /\ ( ( ( a / ( a gcd b ) ) ^ 4 ) + ( e ^ 4 ) ) = ( ( c / ( ( a gcd b ) ^ 2 ) ) ^ 2 ) ) ) )
174		oveq2	|- ( e = ( b / ( a gcd b ) ) -> ( ( a / ( a gcd b ) ) gcd e ) = ( ( a / ( a gcd b ) ) gcd ( b / ( a gcd b ) ) ) )
175	174	eqeq1d	|- ( e = ( b / ( a gcd b ) ) -> ( ( ( a / ( a gcd b ) ) gcd e ) = 1 <-> ( ( a / ( a gcd b ) ) gcd ( b / ( a gcd b ) ) ) = 1 ) )
176		oveq1	|- ( e = ( b / ( a gcd b ) ) -> ( e ^ 4 ) = ( ( b / ( a gcd b ) ) ^ 4 ) )
177	176	oveq2d	|- ( e = ( b / ( a gcd b ) ) -> ( ( ( a / ( a gcd b ) ) ^ 4 ) + ( e ^ 4 ) ) = ( ( ( a / ( a gcd b ) ) ^ 4 ) + ( ( b / ( a gcd b ) ) ^ 4 ) ) )
178	177	eqeq1d	|- ( e = ( b / ( a gcd b ) ) -> ( ( ( ( a / ( a gcd b ) ) ^ 4 ) + ( e ^ 4 ) ) = ( ( c / ( ( a gcd b ) ^ 2 ) ) ^ 2 ) <-> ( ( ( a / ( a gcd b ) ) ^ 4 ) + ( ( b / ( a gcd b ) ) ^ 4 ) ) = ( ( c / ( ( a gcd b ) ^ 2 ) ) ^ 2 ) ) )
179	175 178	anbi12d	|- ( e = ( b / ( a gcd b ) ) -> ( ( ( ( a / ( a gcd b ) ) gcd e ) = 1 /\ ( ( ( a / ( a gcd b ) ) ^ 4 ) + ( e ^ 4 ) ) = ( ( c / ( ( a gcd b ) ^ 2 ) ) ^ 2 ) ) <-> ( ( ( a / ( a gcd b ) ) gcd ( b / ( a gcd b ) ) ) = 1 /\ ( ( ( a / ( a gcd b ) ) ^ 4 ) + ( ( b / ( a gcd b ) ) ^ 4 ) ) = ( ( c / ( ( a gcd b ) ^ 2 ) ) ^ 2 ) ) ) )
180		simplrr	|- ( ( ( ph /\ ( c e. NN /\ a e. NN ) ) /\ ( b e. NN /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) -> a e. NN )
181		simprl	|- ( ( ( ph /\ ( c e. NN /\ a e. NN ) ) /\ ( b e. NN /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) -> b e. NN )
182		simplrl	|- ( ( ( ph /\ ( c e. NN /\ a e. NN ) ) /\ ( b e. NN /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) -> c e. NN )
183		simprr	|- ( ( ( ph /\ ( c e. NN /\ a e. NN ) ) /\ ( b e. NN /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) -> ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) )
184	180 181 182 183	flt4lem6	|- ( ( ( ph /\ ( c e. NN /\ a e. NN ) ) /\ ( b e. NN /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) -> ( ( ( a / ( a gcd b ) ) e. NN /\ ( b / ( a gcd b ) ) e. NN /\ ( c / ( ( a gcd b ) ^ 2 ) ) e. NN ) /\ ( ( ( a / ( a gcd b ) ) ^ 4 ) + ( ( b / ( a gcd b ) ) ^ 4 ) ) = ( ( c / ( ( a gcd b ) ^ 2 ) ) ^ 2 ) ) )
185	184	simpld	|- ( ( ( ph /\ ( c e. NN /\ a e. NN ) ) /\ ( b e. NN /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) -> ( ( a / ( a gcd b ) ) e. NN /\ ( b / ( a gcd b ) ) e. NN /\ ( c / ( ( a gcd b ) ^ 2 ) ) e. NN ) )
186	185	simp3d	|- ( ( ( ph /\ ( c e. NN /\ a e. NN ) ) /\ ( b e. NN /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) -> ( c / ( ( a gcd b ) ^ 2 ) ) e. NN )
187	185	simp1d	|- ( ( ( ph /\ ( c e. NN /\ a e. NN ) ) /\ ( b e. NN /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) -> ( a / ( a gcd b ) ) e. NN )
188	185	simp2d	|- ( ( ( ph /\ ( c e. NN /\ a e. NN ) ) /\ ( b e. NN /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) -> ( b / ( a gcd b ) ) e. NN )
189	180	nnzd	|- ( ( ( ph /\ ( c e. NN /\ a e. NN ) ) /\ ( b e. NN /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) -> a e. ZZ )
190	181	nnzd	|- ( ( ( ph /\ ( c e. NN /\ a e. NN ) ) /\ ( b e. NN /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) -> b e. ZZ )
191	181	nnne0d	|- ( ( ( ph /\ ( c e. NN /\ a e. NN ) ) /\ ( b e. NN /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) -> b =/= 0 )
192		divgcdcoprm0	|- ( ( a e. ZZ /\ b e. ZZ /\ b =/= 0 ) -> ( ( a / ( a gcd b ) ) gcd ( b / ( a gcd b ) ) ) = 1 )
193	189 190 191 192	syl3anc	|- ( ( ( ph /\ ( c e. NN /\ a e. NN ) ) /\ ( b e. NN /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) -> ( ( a / ( a gcd b ) ) gcd ( b / ( a gcd b ) ) ) = 1 )
194	184	simprd	|- ( ( ( ph /\ ( c e. NN /\ a e. NN ) ) /\ ( b e. NN /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) -> ( ( ( a / ( a gcd b ) ) ^ 4 ) + ( ( b / ( a gcd b ) ) ^ 4 ) ) = ( ( c / ( ( a gcd b ) ^ 2 ) ) ^ 2 ) )
195	193 194	jca	|- ( ( ( ph /\ ( c e. NN /\ a e. NN ) ) /\ ( b e. NN /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) -> ( ( ( a / ( a gcd b ) ) gcd ( b / ( a gcd b ) ) ) = 1 /\ ( ( ( a / ( a gcd b ) ) ^ 4 ) + ( ( b / ( a gcd b ) ) ^ 4 ) ) = ( ( c / ( ( a gcd b ) ^ 2 ) ) ^ 2 ) ) )
196	167 173 179 186 187 188 195	3rspcedvdw	|- ( ( ( ph /\ ( c e. NN /\ a e. NN ) ) /\ ( b e. NN /\ ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) ) -> E. f e. NN E. d e. NN E. e e. NN ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) )
197	196	rexlimdvaa	|- ( ( ph /\ ( c e. NN /\ a e. NN ) ) -> ( E. b e. NN ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) -> E. f e. NN E. d e. NN E. e e. NN ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) )
198	197	rexlimdvva	|- ( ph -> ( E. c e. NN E. a e. NN E. b e. NN ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) -> E. f e. NN E. d e. NN E. e e. NN ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) ) )
199	198	con3d	|- ( ph -> ( -. E. f e. NN E. d e. NN E. e e. NN ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) -> -. E. c e. NN E. a e. NN E. b e. NN ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) )
200		ralnex	|- ( A. c e. NN -. E. a e. NN E. b e. NN ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) <-> -. E. c e. NN E. a e. NN E. b e. NN ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) )
201	199 159 200	3imtr4g	|- ( ph -> ( A. f e. NN -. E. d e. NN E. e e. NN ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) -> A. c e. NN -. E. a e. NN E. b e. NN ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) ) )
202		rabeq0	|- ( { c e. NN | E. a e. NN E. b e. NN ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) } = (/) <-> A. c e. NN -. E. a e. NN E. b e. NN ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) )
203	201 162 202	3imtr4g	|- ( ph -> ( { f e. NN | E. d e. NN E. e e. NN ( ( d gcd e ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 4 ) ) = ( f ^ 2 ) ) } = (/) -> { c e. NN | E. a e. NN E. b e. NN ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) } = (/) ) )
204	164 203	mpd	|- ( ph -> { c e. NN | E. a e. NN E. b e. NN ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) } = (/) )
205		sseq0	|- ( ( { c e. NN | ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( c ^ 2 ) } C_ { c e. NN | E. a e. NN E. b e. NN ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) } /\ { c e. NN | E. a e. NN E. b e. NN ( ( a ^ 4 ) + ( b ^ 4 ) ) = ( c ^ 2 ) } = (/) ) -> { c e. NN | ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( c ^ 2 ) } = (/) )
206	15 204 205	syl2anc	|- ( ph -> { c e. NN | ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( c ^ 2 ) } = (/) )
207		rabeq0	|- ( { c e. NN | ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( c ^ 2 ) } = (/) <-> A. c e. NN -. ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( c ^ 2 ) )
208	206 207	sylib	|- ( ph -> A. c e. NN -. ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( c ^ 2 ) )
209		oveq1	|- ( c = C -> ( c ^ 2 ) = ( C ^ 2 ) )
210	209	eqeq2d	|- ( c = C -> ( ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( c ^ 2 ) <-> ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( C ^ 2 ) ) )
211	210	necon3bbid	|- ( c = C -> ( -. ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( c ^ 2 ) <-> ( ( A ^ 4 ) + ( B ^ 4 ) ) =/= ( C ^ 2 ) ) )
212	211	rspcv	|- ( C e. NN -> ( A. c e. NN -. ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( c ^ 2 ) -> ( ( A ^ 4 ) + ( B ^ 4 ) ) =/= ( C ^ 2 ) ) )
213	3 208 212	sylc	|- ( ph -> ( ( A ^ 4 ) + ( B ^ 4 ) ) =/= ( C ^ 2 ) )