Theorem 2sqlem8 25151

Description: Lemma for 2sq 25155. (Contributed by Mario Carneiro, 20-Jun-2015.)

Hypotheses

Ref	Expression
2sq.1	|- S = ran ( w e. ZZ[_i] |-> ( ( abs ` w ) ^ 2 ) )
2sqlem7.2	|- Y = { z | E. x e. ZZ E. y e. ZZ ( ( x gcd y ) = 1 /\ z = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) }
2sqlem9.5	|- ( ph -> A. b e. ( 1 ... ( M - 1 ) ) A. a e. Y ( b || a -> b e. S ) )
2sqlem9.7	|- ( ph -> M || N )
2sqlem8.n	|- ( ph -> N e. NN )
2sqlem8.m	|- ( ph -> M e. ( ZZ>= ` 2 ) )
2sqlem8.1	|- ( ph -> A e. ZZ )
2sqlem8.2	|- ( ph -> B e. ZZ )
2sqlem8.3	|- ( ph -> ( A gcd B ) = 1 )
2sqlem8.4	|- ( ph -> N = ( ( A ^ 2 ) + ( B ^ 2 ) ) )
2sqlem8.c	|- C = ( ( ( A + ( M / 2 ) ) mod M ) - ( M / 2 ) )
2sqlem8.d	|- D = ( ( ( B + ( M / 2 ) ) mod M ) - ( M / 2 ) )
2sqlem8.e	|- E = ( C / ( C gcd D ) )
2sqlem8.f	|- F = ( D / ( C gcd D ) )

Assertion

Ref	Expression
2sqlem8	|- ( ph -> M e. S )

Distinct variable groups:   a, b, w, x, y, z   A, a, x, y, z   x, C   ph, x, y   B, a, b, x, y   M, a, b, x, y, z   S, a, b, x, y, z   x, D   E, a, x, y, z   x, N, y, z   Y, a, b, x, y   F, a, x, y, z

Allowed substitution hints:   ph( z, w, a, b)   A( w, b)   B( z, w)   C( y, z, w, a, b)   D( y, z, w, a, b)   S( w)   E( w, b)   F( w, b)   M( w)   N( w, a, b)   Y( z, w)

Proof of Theorem 2sqlem8

Dummy variable p is distinct from all other variables.

Step	Hyp	Ref	Expression
1		2sq.1	. 2 |- S = ran ( w e. ZZ[_i] |-> ( ( abs ` w ) ^ 2 ) )
2		2sqlem8.m	. . . 4 |- ( ph -> M e. ( ZZ>= ` 2 ) )
3		eluz2b3 11762	. . . 4 |- ( M e. ( ZZ>= ` 2 ) <-> ( M e. NN /\ M =/= 1 ) )
4	2, 3	sylib 208	. . 3 |- ( ph -> ( M e. NN /\ M =/= 1 ) )
5	4	simpld 475	. 2 |- ( ph -> M e. NN )
6		2sqlem9.7	. . . . . . 7 |- ( ph -> M || N )
7		eluzelz 11697	. . . . . . . . 9 |- ( M e. ( ZZ>= ` 2 ) -> M e. ZZ )
8	2, 7	syl 17	. . . . . . . 8 |- ( ph -> M e. ZZ )
9		2sqlem8.n	. . . . . . . . 9 |- ( ph -> N e. NN )
10	9	nnzd 11481	. . . . . . . 8 |- ( ph -> N e. ZZ )
11		2sqlem8.1	. . . . . . . . . . . 12 |- ( ph -> A e. ZZ )
12		2sqlem8.c	. . . . . . . . . . . 12 |- C = ( ( ( A + ( M / 2 ) ) mod M ) - ( M / 2 ) )
13	11, 5, 12	4sqlem5 15646	. . . . . . . . . . 11 |- ( ph -> ( C e. ZZ /\ ( ( A - C ) / M ) e. ZZ ) )
14	13	simpld 475	. . . . . . . . . 10 |- ( ph -> C e. ZZ )
15		zsqcl 12934	. . . . . . . . . 10 |- ( C e. ZZ -> ( C ^ 2 ) e. ZZ )
16	14, 15	syl 17	. . . . . . . . 9 |- ( ph -> ( C ^ 2 ) e. ZZ )
17		2sqlem8.2	. . . . . . . . . . . 12 |- ( ph -> B e. ZZ )
18		2sqlem8.d	. . . . . . . . . . . 12 |- D = ( ( ( B + ( M / 2 ) ) mod M ) - ( M / 2 ) )
19	17, 5, 18	4sqlem5 15646	. . . . . . . . . . 11 |- ( ph -> ( D e. ZZ /\ ( ( B - D ) / M ) e. ZZ ) )
20	19	simpld 475	. . . . . . . . . 10 |- ( ph -> D e. ZZ )
21		zsqcl 12934	. . . . . . . . . 10 |- ( D e. ZZ -> ( D ^ 2 ) e. ZZ )
22	20, 21	syl 17	. . . . . . . . 9 |- ( ph -> ( D ^ 2 ) e. ZZ )
23	16, 22	zaddcld 11486	. . . . . . . 8 |- ( ph -> ( ( C ^ 2 ) + ( D ^ 2 ) ) e. ZZ )
24	11, 5, 12	4sqlem8 15649	. . . . . . . . . 10 |- ( ph -> M || ( ( A ^ 2 ) - ( C ^ 2 ) ) )
25	17, 5, 18	4sqlem8 15649	. . . . . . . . . 10 |- ( ph -> M || ( ( B ^ 2 ) - ( D ^ 2 ) ) )
26		zsqcl 12934	. . . . . . . . . . . . 13 |- ( A e. ZZ -> ( A ^ 2 ) e. ZZ )
27	11, 26	syl 17	. . . . . . . . . . . 12 |- ( ph -> ( A ^ 2 ) e. ZZ )
28	27, 16	zsubcld 11487	. . . . . . . . . . 11 |- ( ph -> ( ( A ^ 2 ) - ( C ^ 2 ) ) e. ZZ )
29		zsqcl 12934	. . . . . . . . . . . . 13 |- ( B e. ZZ -> ( B ^ 2 ) e. ZZ )
30	17, 29	syl 17	. . . . . . . . . . . 12 |- ( ph -> ( B ^ 2 ) e. ZZ )
31	30, 22	zsubcld 11487	. . . . . . . . . . 11 |- ( ph -> ( ( B ^ 2 ) - ( D ^ 2 ) ) e. ZZ )
32		dvds2add 15015	. . . . . . . . . . 11 |- ( ( M e. ZZ /\ ( ( A ^ 2 ) - ( C ^ 2 ) ) e. ZZ /\ ( ( B ^ 2 ) - ( D ^ 2 ) ) e. ZZ ) -> ( ( M || ( ( A ^ 2 ) - ( C ^ 2 ) ) /\ M || ( ( B ^ 2 ) - ( D ^ 2 ) ) ) -> M || ( ( ( A ^ 2 ) - ( C ^ 2 ) ) + ( ( B ^ 2 ) - ( D ^ 2 ) ) ) ) )
33	8, 28, 31, 32	syl3anc 1326	. . . . . . . . . 10 |- ( ph -> ( ( M || ( ( A ^ 2 ) - ( C ^ 2 ) ) /\ M || ( ( B ^ 2 ) - ( D ^ 2 ) ) ) -> M || ( ( ( A ^ 2 ) - ( C ^ 2 ) ) + ( ( B ^ 2 ) - ( D ^ 2 ) ) ) ) )
34	24, 25, 33	mp2and 715	. . . . . . . . 9 |- ( ph -> M || ( ( ( A ^ 2 ) - ( C ^ 2 ) ) + ( ( B ^ 2 ) - ( D ^ 2 ) ) ) )
35		2sqlem8.4	. . . . . . . . . . 11 |- ( ph -> N = ( ( A ^ 2 ) + ( B ^ 2 ) ) )
36	35	oveq1d 6665	. . . . . . . . . 10 |- ( ph -> ( N - ( ( C ^ 2 ) + ( D ^ 2 ) ) ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) - ( ( C ^ 2 ) + ( D ^ 2 ) ) ) )
37	27	zcnd 11483	. . . . . . . . . . 11 |- ( ph -> ( A ^ 2 ) e. CC )
38	30	zcnd 11483	. . . . . . . . . . 11 |- ( ph -> ( B ^ 2 ) e. CC )
39	16	zcnd 11483	. . . . . . . . . . 11 |- ( ph -> ( C ^ 2 ) e. CC )
40	22	zcnd 11483	. . . . . . . . . . 11 |- ( ph -> ( D ^ 2 ) e. CC )
41	37, 38, 39, 40	addsub4d 10439	. . . . . . . . . 10 |- ( ph -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) - ( ( C ^ 2 ) + ( D ^ 2 ) ) ) = ( ( ( A ^ 2 ) - ( C ^ 2 ) ) + ( ( B ^ 2 ) - ( D ^ 2 ) ) ) )
42	36, 41	eqtrd 2656	. . . . . . . . 9 |- ( ph -> ( N - ( ( C ^ 2 ) + ( D ^ 2 ) ) ) = ( ( ( A ^ 2 ) - ( C ^ 2 ) ) + ( ( B ^ 2 ) - ( D ^ 2 ) ) ) )
43	34, 42	breqtrrd 4681	. . . . . . . 8 |- ( ph -> M || ( N - ( ( C ^ 2 ) + ( D ^ 2 ) ) ) )
44		dvdssub2 15023	. . . . . . . 8 |- ( ( ( M e. ZZ /\ N e. ZZ /\ ( ( C ^ 2 ) + ( D ^ 2 ) ) e. ZZ ) /\ M || ( N - ( ( C ^ 2 ) + ( D ^ 2 ) ) ) ) -> ( M || N <-> M || ( ( C ^ 2 ) + ( D ^ 2 ) ) ) )
45	8, 10, 23, 43, 44	syl31anc 1329	. . . . . . 7 |- ( ph -> ( M || N <-> M || ( ( C ^ 2 ) + ( D ^ 2 ) ) ) )
46	6, 45	mpbid 222	. . . . . 6 |- ( ph -> M || ( ( C ^ 2 ) + ( D ^ 2 ) ) )
47		2sqlem7.2	. . . . . . . . . . . 12 |- Y = { z | E. x e. ZZ E. y e. ZZ ( ( x gcd y ) = 1 /\ z = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) }
48		2sqlem9.5	. . . . . . . . . . . 12 |- ( ph -> A. b e. ( 1 ... ( M - 1 ) ) A. a e. Y ( b || a -> b e. S ) )
49		2sqlem8.3	. . . . . . . . . . . 12 |- ( ph -> ( A gcd B ) = 1 )
50	1, 47, 48, 6, 9, 2, 11, 17, 49, 35, 12, 18	2sqlem8a 25150	. . . . . . . . . . 11 |- ( ph -> ( C gcd D ) e. NN )
51	50	nnzd 11481	. . . . . . . . . 10 |- ( ph -> ( C gcd D ) e. ZZ )
52		zsqcl2 12941	. . . . . . . . . 10 |- ( ( C gcd D ) e. ZZ -> ( ( C gcd D ) ^ 2 ) e. NN0 )
53	51, 52	syl 17	. . . . . . . . 9 |- ( ph -> ( ( C gcd D ) ^ 2 ) e. NN0 )
54	53	nn0cnd 11353	. . . . . . . 8 |- ( ph -> ( ( C gcd D ) ^ 2 ) e. CC )
55		2sqlem8.e	. . . . . . . . . . 11 |- E = ( C / ( C gcd D ) )
56		gcddvds 15225	. . . . . . . . . . . . . 14 |- ( ( C e. ZZ /\ D e. ZZ ) -> ( ( C gcd D ) || C /\ ( C gcd D ) || D ) )
57	14, 20, 56	syl2anc 693	. . . . . . . . . . . . 13 |- ( ph -> ( ( C gcd D ) || C /\ ( C gcd D ) || D ) )
58	57	simpld 475	. . . . . . . . . . . 12 |- ( ph -> ( C gcd D ) || C )
59	50	nnne0d 11065	. . . . . . . . . . . . 13 |- ( ph -> ( C gcd D ) =/= 0 )
60		dvdsval2 14986	. . . . . . . . . . . . 13 |- ( ( ( C gcd D ) e. ZZ /\ ( C gcd D ) =/= 0 /\ C e. ZZ ) -> ( ( C gcd D ) || C <-> ( C / ( C gcd D ) ) e. ZZ ) )
61	51, 59, 14, 60	syl3anc 1326	. . . . . . . . . . . 12 |- ( ph -> ( ( C gcd D ) || C <-> ( C / ( C gcd D ) ) e. ZZ ) )
62	58, 61	mpbid 222	. . . . . . . . . . 11 |- ( ph -> ( C / ( C gcd D ) ) e. ZZ )
63	55, 62	syl5eqel 2705	. . . . . . . . . 10 |- ( ph -> E e. ZZ )
64		zsqcl2 12941	. . . . . . . . . 10 |- ( E e. ZZ -> ( E ^ 2 ) e. NN0 )
65	63, 64	syl 17	. . . . . . . . 9 |- ( ph -> ( E ^ 2 ) e. NN0 )
66	65	nn0cnd 11353	. . . . . . . 8 |- ( ph -> ( E ^ 2 ) e. CC )
67		2sqlem8.f	. . . . . . . . . . 11 |- F = ( D / ( C gcd D ) )
68	57	simprd 479	. . . . . . . . . . . 12 |- ( ph -> ( C gcd D ) || D )
69		dvdsval2 14986	. . . . . . . . . . . . 13 |- ( ( ( C gcd D ) e. ZZ /\ ( C gcd D ) =/= 0 /\ D e. ZZ ) -> ( ( C gcd D ) || D <-> ( D / ( C gcd D ) ) e. ZZ ) )
70	51, 59, 20, 69	syl3anc 1326	. . . . . . . . . . . 12 |- ( ph -> ( ( C gcd D ) || D <-> ( D / ( C gcd D ) ) e. ZZ ) )
71	68, 70	mpbid 222	. . . . . . . . . . 11 |- ( ph -> ( D / ( C gcd D ) ) e. ZZ )
72	67, 71	syl5eqel 2705	. . . . . . . . . 10 |- ( ph -> F e. ZZ )
73		zsqcl2 12941	. . . . . . . . . 10 |- ( F e. ZZ -> ( F ^ 2 ) e. NN0 )
74	72, 73	syl 17	. . . . . . . . 9 |- ( ph -> ( F ^ 2 ) e. NN0 )
75	74	nn0cnd 11353	. . . . . . . 8 |- ( ph -> ( F ^ 2 ) e. CC )
76	54, 66, 75	adddid 10064	. . . . . . 7 |- ( ph -> ( ( ( C gcd D ) ^ 2 ) x. ( ( E ^ 2 ) + ( F ^ 2 ) ) ) = ( ( ( ( C gcd D ) ^ 2 ) x. ( E ^ 2 ) ) + ( ( ( C gcd D ) ^ 2 ) x. ( F ^ 2 ) ) ) )
77	51	zcnd 11483	. . . . . . . . . 10 |- ( ph -> ( C gcd D ) e. CC )
78	63	zcnd 11483	. . . . . . . . . 10 |- ( ph -> E e. CC )
79	77, 78	sqmuld 13020	. . . . . . . . 9 |- ( ph -> ( ( ( C gcd D ) x. E ) ^ 2 ) = ( ( ( C gcd D ) ^ 2 ) x. ( E ^ 2 ) ) )
80	55	oveq2i 6661	. . . . . . . . . . 11 |- ( ( C gcd D ) x. E ) = ( ( C gcd D ) x. ( C / ( C gcd D ) ) )
81	14	zcnd 11483	. . . . . . . . . . . 12 |- ( ph -> C e. CC )
82	81, 77, 59	divcan2d 10803	. . . . . . . . . . 11 |- ( ph -> ( ( C gcd D ) x. ( C / ( C gcd D ) ) ) = C )
83	80, 82	syl5eq 2668	. . . . . . . . . 10 |- ( ph -> ( ( C gcd D ) x. E ) = C )
84	83	oveq1d 6665	. . . . . . . . 9 |- ( ph -> ( ( ( C gcd D ) x. E ) ^ 2 ) = ( C ^ 2 ) )
85	79, 84	eqtr3d 2658	. . . . . . . 8 |- ( ph -> ( ( ( C gcd D ) ^ 2 ) x. ( E ^ 2 ) ) = ( C ^ 2 ) )
86	72	zcnd 11483	. . . . . . . . . 10 |- ( ph -> F e. CC )
87	77, 86	sqmuld 13020	. . . . . . . . 9 |- ( ph -> ( ( ( C gcd D ) x. F ) ^ 2 ) = ( ( ( C gcd D ) ^ 2 ) x. ( F ^ 2 ) ) )
88	67	oveq2i 6661	. . . . . . . . . . 11 |- ( ( C gcd D ) x. F ) = ( ( C gcd D ) x. ( D / ( C gcd D ) ) )
89	20	zcnd 11483	. . . . . . . . . . . 12 |- ( ph -> D e. CC )
90	89, 77, 59	divcan2d 10803	. . . . . . . . . . 11 |- ( ph -> ( ( C gcd D ) x. ( D / ( C gcd D ) ) ) = D )
91	88, 90	syl5eq 2668	. . . . . . . . . 10 |- ( ph -> ( ( C gcd D ) x. F ) = D )
92	91	oveq1d 6665	. . . . . . . . 9 |- ( ph -> ( ( ( C gcd D ) x. F ) ^ 2 ) = ( D ^ 2 ) )
93	87, 92	eqtr3d 2658	. . . . . . . 8 |- ( ph -> ( ( ( C gcd D ) ^ 2 ) x. ( F ^ 2 ) ) = ( D ^ 2 ) )
94	85, 93	oveq12d 6668	. . . . . . 7 |- ( ph -> ( ( ( ( C gcd D ) ^ 2 ) x. ( E ^ 2 ) ) + ( ( ( C gcd D ) ^ 2 ) x. ( F ^ 2 ) ) ) = ( ( C ^ 2 ) + ( D ^ 2 ) ) )
95	76, 94	eqtrd 2656	. . . . . 6 |- ( ph -> ( ( ( C gcd D ) ^ 2 ) x. ( ( E ^ 2 ) + ( F ^ 2 ) ) ) = ( ( C ^ 2 ) + ( D ^ 2 ) ) )
96	46, 95	breqtrrd 4681	. . . . 5 |- ( ph -> M || ( ( ( C gcd D ) ^ 2 ) x. ( ( E ^ 2 ) + ( F ^ 2 ) ) ) )
97		zsqcl 12934	. . . . . . . 8 |- ( ( C gcd D ) e. ZZ -> ( ( C gcd D ) ^ 2 ) e. ZZ )
98	51, 97	syl 17	. . . . . . 7 |- ( ph -> ( ( C gcd D ) ^ 2 ) e. ZZ )
99		gcdcom 15235	. . . . . . 7 |- ( ( M e. ZZ /\ ( ( C gcd D ) ^ 2 ) e. ZZ ) -> ( M gcd ( ( C gcd D ) ^ 2 ) ) = ( ( ( C gcd D ) ^ 2 ) gcd M ) )
100	8, 98, 99	syl2anc 693	. . . . . 6 |- ( ph -> ( M gcd ( ( C gcd D ) ^ 2 ) ) = ( ( ( C gcd D ) ^ 2 ) gcd M ) )
101		gcddvds 15225	. . . . . . . . . . . . . 14 |- ( ( ( C gcd D ) e. ZZ /\ M e. ZZ ) -> ( ( ( C gcd D ) gcd M ) || ( C gcd D ) /\ ( ( C gcd D ) gcd M ) || M ) )
102	51, 8, 101	syl2anc 693	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( C gcd D ) gcd M ) || ( C gcd D ) /\ ( ( C gcd D ) gcd M ) || M ) )
103	102	simpld 475	. . . . . . . . . . . 12 |- ( ph -> ( ( C gcd D ) gcd M ) || ( C gcd D ) )
104	51, 8	gcdcld 15230	. . . . . . . . . . . . . 14 |- ( ph -> ( ( C gcd D ) gcd M ) e. NN0 )
105	104	nn0zd 11480	. . . . . . . . . . . . 13 |- ( ph -> ( ( C gcd D ) gcd M ) e. ZZ )
106		dvdstr 15018	. . . . . . . . . . . . 13 |- ( ( ( ( C gcd D ) gcd M ) e. ZZ /\ ( C gcd D ) e. ZZ /\ C e. ZZ ) -> ( ( ( ( C gcd D ) gcd M ) || ( C gcd D ) /\ ( C gcd D ) || C ) -> ( ( C gcd D ) gcd M ) || C ) )
107	105, 51, 14, 106	syl3anc 1326	. . . . . . . . . . . 12 |- ( ph -> ( ( ( ( C gcd D ) gcd M ) || ( C gcd D ) /\ ( C gcd D ) || C ) -> ( ( C gcd D ) gcd M ) || C ) )
108	103, 58, 107	mp2and 715	. . . . . . . . . . 11 |- ( ph -> ( ( C gcd D ) gcd M ) || C )
109	102	simprd 479	. . . . . . . . . . . . 13 |- ( ph -> ( ( C gcd D ) gcd M ) || M )
110	13	simprd 479	. . . . . . . . . . . . . 14 |- ( ph -> ( ( A - C ) / M ) e. ZZ )
111	5	nnne0d 11065	. . . . . . . . . . . . . . 15 |- ( ph -> M =/= 0 )
112	11, 14	zsubcld 11487	. . . . . . . . . . . . . . 15 |- ( ph -> ( A - C ) e. ZZ )
113		dvdsval2 14986	. . . . . . . . . . . . . . 15 |- ( ( M e. ZZ /\ M =/= 0 /\ ( A - C ) e. ZZ ) -> ( M || ( A - C ) <-> ( ( A - C ) / M ) e. ZZ ) )
114	8, 111, 112, 113	syl3anc 1326	. . . . . . . . . . . . . 14 |- ( ph -> ( M || ( A - C ) <-> ( ( A - C ) / M ) e. ZZ ) )
115	110, 114	mpbird 247	. . . . . . . . . . . . 13 |- ( ph -> M || ( A - C ) )
116		dvdstr 15018	. . . . . . . . . . . . . 14 |- ( ( ( ( C gcd D ) gcd M ) e. ZZ /\ M e. ZZ /\ ( A - C ) e. ZZ ) -> ( ( ( ( C gcd D ) gcd M ) || M /\ M || ( A - C ) ) -> ( ( C gcd D ) gcd M ) || ( A - C ) ) )
117	105, 8, 112, 116	syl3anc 1326	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( ( C gcd D ) gcd M ) || M /\ M || ( A - C ) ) -> ( ( C gcd D ) gcd M ) || ( A - C ) ) )
118	109, 115, 117	mp2and 715	. . . . . . . . . . . 12 |- ( ph -> ( ( C gcd D ) gcd M ) || ( A - C ) )
119		dvdssub2 15023	. . . . . . . . . . . 12 |- ( ( ( ( ( C gcd D ) gcd M ) e. ZZ /\ A e. ZZ /\ C e. ZZ ) /\ ( ( C gcd D ) gcd M ) || ( A - C ) ) -> ( ( ( C gcd D ) gcd M ) || A <-> ( ( C gcd D ) gcd M ) || C ) )
120	105, 11, 14, 118, 119	syl31anc 1329	. . . . . . . . . . 11 |- ( ph -> ( ( ( C gcd D ) gcd M ) || A <-> ( ( C gcd D ) gcd M ) || C ) )
121	108, 120	mpbird 247	. . . . . . . . . 10 |- ( ph -> ( ( C gcd D ) gcd M ) || A )
122		dvdstr 15018	. . . . . . . . . . . . 13 |- ( ( ( ( C gcd D ) gcd M ) e. ZZ /\ ( C gcd D ) e. ZZ /\ D e. ZZ ) -> ( ( ( ( C gcd D ) gcd M ) || ( C gcd D ) /\ ( C gcd D ) || D ) -> ( ( C gcd D ) gcd M ) || D ) )
123	105, 51, 20, 122	syl3anc 1326	. . . . . . . . . . . 12 |- ( ph -> ( ( ( ( C gcd D ) gcd M ) || ( C gcd D ) /\ ( C gcd D ) || D ) -> ( ( C gcd D ) gcd M ) || D ) )
124	103, 68, 123	mp2and 715	. . . . . . . . . . 11 |- ( ph -> ( ( C gcd D ) gcd M ) || D )
125	19	simprd 479	. . . . . . . . . . . . . 14 |- ( ph -> ( ( B - D ) / M ) e. ZZ )
126	17, 20	zsubcld 11487	. . . . . . . . . . . . . . 15 |- ( ph -> ( B - D ) e. ZZ )
127		dvdsval2 14986	. . . . . . . . . . . . . . 15 |- ( ( M e. ZZ /\ M =/= 0 /\ ( B - D ) e. ZZ ) -> ( M || ( B - D ) <-> ( ( B - D ) / M ) e. ZZ ) )
128	8, 111, 126, 127	syl3anc 1326	. . . . . . . . . . . . . 14 |- ( ph -> ( M || ( B - D ) <-> ( ( B - D ) / M ) e. ZZ ) )
129	125, 128	mpbird 247	. . . . . . . . . . . . 13 |- ( ph -> M || ( B - D ) )
130		dvdstr 15018	. . . . . . . . . . . . . 14 |- ( ( ( ( C gcd D ) gcd M ) e. ZZ /\ M e. ZZ /\ ( B - D ) e. ZZ ) -> ( ( ( ( C gcd D ) gcd M ) || M /\ M || ( B - D ) ) -> ( ( C gcd D ) gcd M ) || ( B - D ) ) )
131	105, 8, 126, 130	syl3anc 1326	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( ( C gcd D ) gcd M ) || M /\ M || ( B - D ) ) -> ( ( C gcd D ) gcd M ) || ( B - D ) ) )
132	109, 129, 131	mp2and 715	. . . . . . . . . . . 12 |- ( ph -> ( ( C gcd D ) gcd M ) || ( B - D ) )
133		dvdssub2 15023	. . . . . . . . . . . 12 |- ( ( ( ( ( C gcd D ) gcd M ) e. ZZ /\ B e. ZZ /\ D e. ZZ ) /\ ( ( C gcd D ) gcd M ) || ( B - D ) ) -> ( ( ( C gcd D ) gcd M ) || B <-> ( ( C gcd D ) gcd M ) || D ) )
134	105, 17, 20, 132, 133	syl31anc 1329	. . . . . . . . . . 11 |- ( ph -> ( ( ( C gcd D ) gcd M ) || B <-> ( ( C gcd D ) gcd M ) || D ) )
135	124, 134	mpbird 247	. . . . . . . . . 10 |- ( ph -> ( ( C gcd D ) gcd M ) || B )
136		ax-1ne0 10005	. . . . . . . . . . . . . . 15 |- 1 =/= 0
137	136	a1i 11	. . . . . . . . . . . . . 14 |- ( ph -> 1 =/= 0 )
138	49, 137	eqnetrd 2861	. . . . . . . . . . . . 13 |- ( ph -> ( A gcd B ) =/= 0 )
139	138	neneqd 2799	. . . . . . . . . . . 12 |- ( ph -> -. ( A gcd B ) = 0 )
140		gcdeq0 15238	. . . . . . . . . . . . 13 |- ( ( A e. ZZ /\ B e. ZZ ) -> ( ( A gcd B ) = 0 <-> ( A = 0 /\ B = 0 ) ) )
141	11, 17, 140	syl2anc 693	. . . . . . . . . . . 12 |- ( ph -> ( ( A gcd B ) = 0 <-> ( A = 0 /\ B = 0 ) ) )
142	139, 141	mtbid 314	. . . . . . . . . . 11 |- ( ph -> -. ( A = 0 /\ B = 0 ) )
143		dvdslegcd 15226	. . . . . . . . . . 11 |- ( ( ( ( ( C gcd D ) gcd M ) e. ZZ /\ A e. ZZ /\ B e. ZZ ) /\ -. ( A = 0 /\ B = 0 ) ) -> ( ( ( ( C gcd D ) gcd M ) || A /\ ( ( C gcd D ) gcd M ) || B ) -> ( ( C gcd D ) gcd M ) <_ ( A gcd B ) ) )
144	105, 11, 17, 142, 143	syl31anc 1329	. . . . . . . . . 10 |- ( ph -> ( ( ( ( C gcd D ) gcd M ) || A /\ ( ( C gcd D ) gcd M ) || B ) -> ( ( C gcd D ) gcd M ) <_ ( A gcd B ) ) )
145	121, 135, 144	mp2and 715	. . . . . . . . 9 |- ( ph -> ( ( C gcd D ) gcd M ) <_ ( A gcd B ) )
146	145, 49	breqtrd 4679	. . . . . . . 8 |- ( ph -> ( ( C gcd D ) gcd M ) <_ 1 )
147		simpr 477	. . . . . . . . . . . 12 |- ( ( ( C gcd D ) = 0 /\ M = 0 ) -> M = 0 )
148	147	necon3ai 2819	. . . . . . . . . . 11 |- ( M =/= 0 -> -. ( ( C gcd D ) = 0 /\ M = 0 ) )
149	111, 148	syl 17	. . . . . . . . . 10 |- ( ph -> -. ( ( C gcd D ) = 0 /\ M = 0 ) )
150		gcdn0cl 15224	. . . . . . . . . 10 |- ( ( ( ( C gcd D ) e. ZZ /\ M e. ZZ ) /\ -. ( ( C gcd D ) = 0 /\ M = 0 ) ) -> ( ( C gcd D ) gcd M ) e. NN )
151	51, 8, 149, 150	syl21anc 1325	. . . . . . . . 9 |- ( ph -> ( ( C gcd D ) gcd M ) e. NN )
152		nnle1eq1 11048	. . . . . . . . 9 |- ( ( ( C gcd D ) gcd M ) e. NN -> ( ( ( C gcd D ) gcd M ) <_ 1 <-> ( ( C gcd D ) gcd M ) = 1 ) )
153	151, 152	syl 17	. . . . . . . 8 |- ( ph -> ( ( ( C gcd D ) gcd M ) <_ 1 <-> ( ( C gcd D ) gcd M ) = 1 ) )
154	146, 153	mpbid 222	. . . . . . 7 |- ( ph -> ( ( C gcd D ) gcd M ) = 1 )
155		2nn 11185	. . . . . . . . 9 |- 2 e. NN
156	155	a1i 11	. . . . . . . 8 |- ( ph -> 2 e. NN )
157		rplpwr 15276	. . . . . . . 8 |- ( ( ( C gcd D ) e. NN /\ M e. NN /\ 2 e. NN ) -> ( ( ( C gcd D ) gcd M ) = 1 -> ( ( ( C gcd D ) ^ 2 ) gcd M ) = 1 ) )
158	50, 5, 156, 157	syl3anc 1326	. . . . . . 7 |- ( ph -> ( ( ( C gcd D ) gcd M ) = 1 -> ( ( ( C gcd D ) ^ 2 ) gcd M ) = 1 ) )
159	154, 158	mpd 15	. . . . . 6 |- ( ph -> ( ( ( C gcd D ) ^ 2 ) gcd M ) = 1 )
160	100, 159	eqtrd 2656	. . . . 5 |- ( ph -> ( M gcd ( ( C gcd D ) ^ 2 ) ) = 1 )
161	65, 74	nn0addcld 11355	. . . . . . 7 |- ( ph -> ( ( E ^ 2 ) + ( F ^ 2 ) ) e. NN0 )
162	161	nn0zd 11480	. . . . . 6 |- ( ph -> ( ( E ^ 2 ) + ( F ^ 2 ) ) e. ZZ )
163		coprmdvds 15366	. . . . . 6 |- ( ( M e. ZZ /\ ( ( C gcd D ) ^ 2 ) e. ZZ /\ ( ( E ^ 2 ) + ( F ^ 2 ) ) e. ZZ ) -> ( ( M || ( ( ( C gcd D ) ^ 2 ) x. ( ( E ^ 2 ) + ( F ^ 2 ) ) ) /\ ( M gcd ( ( C gcd D ) ^ 2 ) ) = 1 ) -> M || ( ( E ^ 2 ) + ( F ^ 2 ) ) ) )
164	8, 98, 162, 163	syl3anc 1326	. . . . 5 |- ( ph -> ( ( M || ( ( ( C gcd D ) ^ 2 ) x. ( ( E ^ 2 ) + ( F ^ 2 ) ) ) /\ ( M gcd ( ( C gcd D ) ^ 2 ) ) = 1 ) -> M || ( ( E ^ 2 ) + ( F ^ 2 ) ) ) )
165	96, 160, 164	mp2and 715	. . . 4 |- ( ph -> M || ( ( E ^ 2 ) + ( F ^ 2 ) ) )
166		dvdsval2 14986	. . . . 5 |- ( ( M e. ZZ /\ M =/= 0 /\ ( ( E ^ 2 ) + ( F ^ 2 ) ) e. ZZ ) -> ( M || ( ( E ^ 2 ) + ( F ^ 2 ) ) <-> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) e. ZZ ) )
167	8, 111, 162, 166	syl3anc 1326	. . . 4 |- ( ph -> ( M || ( ( E ^ 2 ) + ( F ^ 2 ) ) <-> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) e. ZZ ) )
168	165, 167	mpbid 222	. . 3 |- ( ph -> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) e. ZZ )
169	65	nn0red 11352	. . . . 5 |- ( ph -> ( E ^ 2 ) e. RR )
170	74	nn0red 11352	. . . . 5 |- ( ph -> ( F ^ 2 ) e. RR )
171	169, 170	readdcld 10069	. . . 4 |- ( ph -> ( ( E ^ 2 ) + ( F ^ 2 ) ) e. RR )
172	5	nnred 11035	. . . 4 |- ( ph -> M e. RR )
173	1, 47	2sqlem7 25149	. . . . . . 7 |- Y C_ ( S i^i NN )
174		inss2 3834	. . . . . . 7 |- ( S i^i NN ) C_ NN
175	173, 174	sstri 3612	. . . . . 6 |- Y C_ NN
176	63, 72	gcdcld 15230	. . . . . . . . . 10 |- ( ph -> ( E gcd F ) e. NN0 )
177	176	nn0cnd 11353	. . . . . . . . 9 |- ( ph -> ( E gcd F ) e. CC )
178		1cnd 10056	. . . . . . . . 9 |- ( ph -> 1 e. CC )
179	77	mulid1d 10057	. . . . . . . . . 10 |- ( ph -> ( ( C gcd D ) x. 1 ) = ( C gcd D ) )
180	83, 91	oveq12d 6668	. . . . . . . . . 10 |- ( ph -> ( ( ( C gcd D ) x. E ) gcd ( ( C gcd D ) x. F ) ) = ( C gcd D ) )
181	14, 20	gcdcld 15230	. . . . . . . . . . 11 |- ( ph -> ( C gcd D ) e. NN0 )
182		mulgcd 15265	. . . . . . . . . . 11 |- ( ( ( C gcd D ) e. NN0 /\ E e. ZZ /\ F e. ZZ ) -> ( ( ( C gcd D ) x. E ) gcd ( ( C gcd D ) x. F ) ) = ( ( C gcd D ) x. ( E gcd F ) ) )
183	181, 63, 72, 182	syl3anc 1326	. . . . . . . . . 10 |- ( ph -> ( ( ( C gcd D ) x. E ) gcd ( ( C gcd D ) x. F ) ) = ( ( C gcd D ) x. ( E gcd F ) ) )
184	179, 180, 183	3eqtr2rd 2663	. . . . . . . . 9 |- ( ph -> ( ( C gcd D ) x. ( E gcd F ) ) = ( ( C gcd D ) x. 1 ) )
185	177, 178, 77, 59, 184	mulcanad 10662	. . . . . . . 8 |- ( ph -> ( E gcd F ) = 1 )
186		eqidd 2623	. . . . . . . 8 |- ( ph -> ( ( E ^ 2 ) + ( F ^ 2 ) ) = ( ( E ^ 2 ) + ( F ^ 2 ) ) )
187		oveq1 6657	. . . . . . . . . . 11 |- ( x = E -> ( x gcd y ) = ( E gcd y ) )
188	187	eqeq1d 2624	. . . . . . . . . 10 |- ( x = E -> ( ( x gcd y ) = 1 <-> ( E gcd y ) = 1 ) )
189		oveq1 6657	. . . . . . . . . . . 12 |- ( x = E -> ( x ^ 2 ) = ( E ^ 2 ) )
190	189	oveq1d 6665	. . . . . . . . . . 11 |- ( x = E -> ( ( x ^ 2 ) + ( y ^ 2 ) ) = ( ( E ^ 2 ) + ( y ^ 2 ) ) )
191	190	eqeq2d 2632	. . . . . . . . . 10 |- ( x = E -> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) <-> ( ( E ^ 2 ) + ( F ^ 2 ) ) = ( ( E ^ 2 ) + ( y ^ 2 ) ) ) )
192	188, 191	anbi12d 747	. . . . . . . . 9 |- ( x = E -> ( ( ( x gcd y ) = 1 /\ ( ( E ^ 2 ) + ( F ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) <-> ( ( E gcd y ) = 1 /\ ( ( E ^ 2 ) + ( F ^ 2 ) ) = ( ( E ^ 2 ) + ( y ^ 2 ) ) ) ) )
193		oveq2 6658	. . . . . . . . . . 11 |- ( y = F -> ( E gcd y ) = ( E gcd F ) )
194	193	eqeq1d 2624	. . . . . . . . . 10 |- ( y = F -> ( ( E gcd y ) = 1 <-> ( E gcd F ) = 1 ) )
195		oveq1 6657	. . . . . . . . . . . 12 |- ( y = F -> ( y ^ 2 ) = ( F ^ 2 ) )
196	195	oveq2d 6666	. . . . . . . . . . 11 |- ( y = F -> ( ( E ^ 2 ) + ( y ^ 2 ) ) = ( ( E ^ 2 ) + ( F ^ 2 ) ) )
197	196	eqeq2d 2632	. . . . . . . . . 10 |- ( y = F -> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) = ( ( E ^ 2 ) + ( y ^ 2 ) ) <-> ( ( E ^ 2 ) + ( F ^ 2 ) ) = ( ( E ^ 2 ) + ( F ^ 2 ) ) ) )
198	194, 197	anbi12d 747	. . . . . . . . 9 |- ( y = F -> ( ( ( E gcd y ) = 1 /\ ( ( E ^ 2 ) + ( F ^ 2 ) ) = ( ( E ^ 2 ) + ( y ^ 2 ) ) ) <-> ( ( E gcd F ) = 1 /\ ( ( E ^ 2 ) + ( F ^ 2 ) ) = ( ( E ^ 2 ) + ( F ^ 2 ) ) ) ) )
199	192, 198	rspc2ev 3324	. . . . . . . 8 |- ( ( E e. ZZ /\ F e. ZZ /\ ( ( E gcd F ) = 1 /\ ( ( E ^ 2 ) + ( F ^ 2 ) ) = ( ( E ^ 2 ) + ( F ^ 2 ) ) ) ) -> E. x e. ZZ E. y e. ZZ ( ( x gcd y ) = 1 /\ ( ( E ^ 2 ) + ( F ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) )
200	63, 72, 185, 186, 199	syl112anc 1330	. . . . . . 7 |- ( ph -> E. x e. ZZ E. y e. ZZ ( ( x gcd y ) = 1 /\ ( ( E ^ 2 ) + ( F ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) )
201		ovex 6678	. . . . . . . 8 |- ( ( E ^ 2 ) + ( F ^ 2 ) ) e. _V
202		eqeq1 2626	. . . . . . . . . 10 |- ( z = ( ( E ^ 2 ) + ( F ^ 2 ) ) -> ( z = ( ( x ^ 2 ) + ( y ^ 2 ) ) <-> ( ( E ^ 2 ) + ( F ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) )
203	202	anbi2d 740	. . . . . . . . 9 |- ( z = ( ( E ^ 2 ) + ( F ^ 2 ) ) -> ( ( ( x gcd y ) = 1 /\ z = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) <-> ( ( x gcd y ) = 1 /\ ( ( E ^ 2 ) + ( F ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) )
204	203	2rexbidv 3057	. . . . . . . 8 |- ( z = ( ( E ^ 2 ) + ( F ^ 2 ) ) -> ( E. x e. ZZ E. y e. ZZ ( ( x gcd y ) = 1 /\ z = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) <-> E. x e. ZZ E. y e. ZZ ( ( x gcd y ) = 1 /\ ( ( E ^ 2 ) + ( F ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) )
205	201, 204, 47	elab2 3354	. . . . . . 7 |- ( ( ( E ^ 2 ) + ( F ^ 2 ) ) e. Y <-> E. x e. ZZ E. y e. ZZ ( ( x gcd y ) = 1 /\ ( ( E ^ 2 ) + ( F ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) )
206	200, 205	sylibr 224	. . . . . 6 |- ( ph -> ( ( E ^ 2 ) + ( F ^ 2 ) ) e. Y )
207	175, 206	sseldi 3601	. . . . 5 |- ( ph -> ( ( E ^ 2 ) + ( F ^ 2 ) ) e. NN )
208	207	nngt0d 11064	. . . 4 |- ( ph -> 0 < ( ( E ^ 2 ) + ( F ^ 2 ) ) )
209	5	nngt0d 11064	. . . 4 |- ( ph -> 0 < M )
210	171, 172, 208, 209	divgt0d 10959	. . 3 |- ( ph -> 0 < ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) )
211		elnnz 11387	. . 3 |- ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) e. NN <-> ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) e. ZZ /\ 0 < ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) )
212	168, 210, 211	sylanbrc 698	. 2 |- ( ph -> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) e. NN )
213		prmnn 15388	. . . . . . . 8 |- ( p e. Prime -> p e. NN )
214	213	ad2antrl 764	. . . . . . 7 |- ( ( ph /\ ( p e. Prime /\ p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) ) -> p e. NN )
215	214	nnred 11035	. . . . . . . 8 |- ( ( ph /\ ( p e. Prime /\ p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) ) -> p e. RR )
216	168	adantr 481	. . . . . . . . 9 |- ( ( ph /\ ( p e. Prime /\ p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) ) -> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) e. ZZ )
217	216	zred 11482	. . . . . . . 8 |- ( ( ph /\ ( p e. Prime /\ p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) ) -> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) e. RR )
218		peano2zm 11420	. . . . . . . . . . 11 |- ( M e. ZZ -> ( M - 1 ) e. ZZ )
219	8, 218	syl 17	. . . . . . . . . 10 |- ( ph -> ( M - 1 ) e. ZZ )
220	219	zred 11482	. . . . . . . . 9 |- ( ph -> ( M - 1 ) e. RR )
221	220	adantr 481	. . . . . . . 8 |- ( ( ph /\ ( p e. Prime /\ p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) ) -> ( M - 1 ) e. RR )
222		simprr 796	. . . . . . . . 9 |- ( ( ph /\ ( p e. Prime /\ p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) ) -> p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) )
223		prmz 15389	. . . . . . . . . . 11 |- ( p e. Prime -> p e. ZZ )
224	223	ad2antrl 764	. . . . . . . . . 10 |- ( ( ph /\ ( p e. Prime /\ p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) ) -> p e. ZZ )
225	212	adantr 481	. . . . . . . . . 10 |- ( ( ph /\ ( p e. Prime /\ p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) ) -> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) e. NN )
226		dvdsle 15032	. . . . . . . . . 10 |- ( ( p e. ZZ /\ ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) e. NN ) -> ( p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) -> p <_ ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) )
227	224, 225, 226	syl2anc 693	. . . . . . . . 9 |- ( ( ph /\ ( p e. Prime /\ p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) ) -> ( p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) -> p <_ ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) )
228	222, 227	mpd 15	. . . . . . . 8 |- ( ( ph /\ ( p e. Prime /\ p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) ) -> p <_ ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) )
229		zsqcl 12934	. . . . . . . . . . . . . . . 16 |- ( M e. ZZ -> ( M ^ 2 ) e. ZZ )
230	8, 229	syl 17	. . . . . . . . . . . . . . 15 |- ( ph -> ( M ^ 2 ) e. ZZ )
231	230	zred 11482	. . . . . . . . . . . . . 14 |- ( ph -> ( M ^ 2 ) e. RR )
232	231	rehalfcld 11279	. . . . . . . . . . . . 13 |- ( ph -> ( ( M ^ 2 ) / 2 ) e. RR )
233	16	zred 11482	. . . . . . . . . . . . . . 15 |- ( ph -> ( C ^ 2 ) e. RR )
234	22	zred 11482	. . . . . . . . . . . . . . 15 |- ( ph -> ( D ^ 2 ) e. RR )
235	233, 234	readdcld 10069	. . . . . . . . . . . . . 14 |- ( ph -> ( ( C ^ 2 ) + ( D ^ 2 ) ) e. RR )
236		1red 10055	. . . . . . . . . . . . . . . 16 |- ( ph -> 1 e. RR )
237	50	nnsqcld 13029	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( C gcd D ) ^ 2 ) e. NN )
238	237	nnred 11035	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( C gcd D ) ^ 2 ) e. RR )
239	161	nn0ge0d 11354	. . . . . . . . . . . . . . . 16 |- ( ph -> 0 <_ ( ( E ^ 2 ) + ( F ^ 2 ) ) )
240	237	nnge1d 11063	. . . . . . . . . . . . . . . 16 |- ( ph -> 1 <_ ( ( C gcd D ) ^ 2 ) )
241	236, 238, 171, 239, 240	lemul1ad 10963	. . . . . . . . . . . . . . 15 |- ( ph -> ( 1 x. ( ( E ^ 2 ) + ( F ^ 2 ) ) ) <_ ( ( ( C gcd D ) ^ 2 ) x. ( ( E ^ 2 ) + ( F ^ 2 ) ) ) )
242	161	nn0cnd 11353	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( E ^ 2 ) + ( F ^ 2 ) ) e. CC )
243	242	mulid2d 10058	. . . . . . . . . . . . . . 15 |- ( ph -> ( 1 x. ( ( E ^ 2 ) + ( F ^ 2 ) ) ) = ( ( E ^ 2 ) + ( F ^ 2 ) ) )
244	241, 243, 95	3brtr3d 4684	. . . . . . . . . . . . . 14 |- ( ph -> ( ( E ^ 2 ) + ( F ^ 2 ) ) <_ ( ( C ^ 2 ) + ( D ^ 2 ) ) )
245	232	rehalfcld 11279	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( ( M ^ 2 ) / 2 ) / 2 ) e. RR )
246	11, 5, 12	4sqlem7 15648	. . . . . . . . . . . . . . . 16 |- ( ph -> ( C ^ 2 ) <_ ( ( ( M ^ 2 ) / 2 ) / 2 ) )
247	17, 5, 18	4sqlem7 15648	. . . . . . . . . . . . . . . 16 |- ( ph -> ( D ^ 2 ) <_ ( ( ( M ^ 2 ) / 2 ) / 2 ) )
248	233, 234, 245, 245, 246, 247	le2addd 10646	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( C ^ 2 ) + ( D ^ 2 ) ) <_ ( ( ( ( M ^ 2 ) / 2 ) / 2 ) + ( ( ( M ^ 2 ) / 2 ) / 2 ) ) )
249	232	recnd 10068	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( M ^ 2 ) / 2 ) e. CC )
250	249	2halvesd 11278	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( ( ( M ^ 2 ) / 2 ) / 2 ) + ( ( ( M ^ 2 ) / 2 ) / 2 ) ) = ( ( M ^ 2 ) / 2 ) )
251	248, 250	breqtrd 4679	. . . . . . . . . . . . . 14 |- ( ph -> ( ( C ^ 2 ) + ( D ^ 2 ) ) <_ ( ( M ^ 2 ) / 2 ) )
252	171, 235, 232, 244, 251	letrd 10194	. . . . . . . . . . . . 13 |- ( ph -> ( ( E ^ 2 ) + ( F ^ 2 ) ) <_ ( ( M ^ 2 ) / 2 ) )
253	5	nnsqcld 13029	. . . . . . . . . . . . . . 15 |- ( ph -> ( M ^ 2 ) e. NN )
254	253	nnrpd 11870	. . . . . . . . . . . . . 14 |- ( ph -> ( M ^ 2 ) e. RR+ )
255		rphalflt 11860	. . . . . . . . . . . . . 14 |- ( ( M ^ 2 ) e. RR+ -> ( ( M ^ 2 ) / 2 ) < ( M ^ 2 ) )
256	254, 255	syl 17	. . . . . . . . . . . . 13 |- ( ph -> ( ( M ^ 2 ) / 2 ) < ( M ^ 2 ) )
257	171, 232, 231, 252, 256	lelttrd 10195	. . . . . . . . . . . 12 |- ( ph -> ( ( E ^ 2 ) + ( F ^ 2 ) ) < ( M ^ 2 ) )
258	8	zcnd 11483	. . . . . . . . . . . . 13 |- ( ph -> M e. CC )
259	258	sqvald 13005	. . . . . . . . . . . 12 |- ( ph -> ( M ^ 2 ) = ( M x. M ) )
260	257, 259	breqtrd 4679	. . . . . . . . . . 11 |- ( ph -> ( ( E ^ 2 ) + ( F ^ 2 ) ) < ( M x. M ) )
261		ltdivmul 10898	. . . . . . . . . . . 12 |- ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) e. RR /\ M e. RR /\ ( M e. RR /\ 0 < M ) ) -> ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) < M <-> ( ( E ^ 2 ) + ( F ^ 2 ) ) < ( M x. M ) ) )
262	171, 172, 172, 209, 261	syl112anc 1330	. . . . . . . . . . 11 |- ( ph -> ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) < M <-> ( ( E ^ 2 ) + ( F ^ 2 ) ) < ( M x. M ) ) )
263	260, 262	mpbird 247	. . . . . . . . . 10 |- ( ph -> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) < M )
264		zltlem1 11430	. . . . . . . . . . 11 |- ( ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) e. ZZ /\ M e. ZZ ) -> ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) < M <-> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) <_ ( M - 1 ) ) )
265	168, 8, 264	syl2anc 693	. . . . . . . . . 10 |- ( ph -> ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) < M <-> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) <_ ( M - 1 ) ) )
266	263, 265	mpbid 222	. . . . . . . . 9 |- ( ph -> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) <_ ( M - 1 ) )
267	266	adantr 481	. . . . . . . 8 |- ( ( ph /\ ( p e. Prime /\ p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) ) -> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) <_ ( M - 1 ) )
268	215, 217, 221, 228, 267	letrd 10194	. . . . . . 7 |- ( ( ph /\ ( p e. Prime /\ p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) ) -> p <_ ( M - 1 ) )
269	219	adantr 481	. . . . . . . 8 |- ( ( ph /\ ( p e. Prime /\ p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) ) -> ( M - 1 ) e. ZZ )
270		fznn 12408	. . . . . . . 8 |- ( ( M - 1 ) e. ZZ -> ( p e. ( 1 ... ( M - 1 ) ) <-> ( p e. NN /\ p <_ ( M - 1 ) ) ) )
271	269, 270	syl 17	. . . . . . 7 |- ( ( ph /\ ( p e. Prime /\ p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) ) -> ( p e. ( 1 ... ( M - 1 ) ) <-> ( p e. NN /\ p <_ ( M - 1 ) ) ) )
272	214, 268, 271	mpbir2and 957	. . . . . 6 |- ( ( ph /\ ( p e. Prime /\ p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) ) -> p e. ( 1 ... ( M - 1 ) ) )
273	206	adantr 481	. . . . . 6 |- ( ( ph /\ ( p e. Prime /\ p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) ) -> ( ( E ^ 2 ) + ( F ^ 2 ) ) e. Y )
274	272, 273	jca 554	. . . . 5 |- ( ( ph /\ ( p e. Prime /\ p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) ) -> ( p e. ( 1 ... ( M - 1 ) ) /\ ( ( E ^ 2 ) + ( F ^ 2 ) ) e. Y ) )
275	48	adantr 481	. . . . 5 |- ( ( ph /\ ( p e. Prime /\ p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) ) -> A. b e. ( 1 ... ( M - 1 ) ) A. a e. Y ( b || a -> b e. S ) )
276		dvdsmul2 15004	. . . . . . . . 9 |- ( ( M e. ZZ /\ ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) e. ZZ ) -> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) || ( M x. ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) )
277	8, 168, 276	syl2anc 693	. . . . . . . 8 |- ( ph -> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) || ( M x. ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) )
278	242, 258, 111	divcan2d 10803	. . . . . . . 8 |- ( ph -> ( M x. ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) = ( ( E ^ 2 ) + ( F ^ 2 ) ) )
279	277, 278	breqtrd 4679	. . . . . . 7 |- ( ph -> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) || ( ( E ^ 2 ) + ( F ^ 2 ) ) )
280	279	adantr 481	. . . . . 6 |- ( ( ph /\ ( p e. Prime /\ p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) ) -> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) || ( ( E ^ 2 ) + ( F ^ 2 ) ) )
281	162	adantr 481	. . . . . . 7 |- ( ( ph /\ ( p e. Prime /\ p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) ) -> ( ( E ^ 2 ) + ( F ^ 2 ) ) e. ZZ )
282		dvdstr 15018	. . . . . . 7 |- ( ( p e. ZZ /\ ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) e. ZZ /\ ( ( E ^ 2 ) + ( F ^ 2 ) ) e. ZZ ) -> ( ( p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) /\ ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) || ( ( E ^ 2 ) + ( F ^ 2 ) ) ) -> p || ( ( E ^ 2 ) + ( F ^ 2 ) ) ) )
283	224, 216, 281, 282	syl3anc 1326	. . . . . 6 |- ( ( ph /\ ( p e. Prime /\ p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) ) -> ( ( p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) /\ ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) || ( ( E ^ 2 ) + ( F ^ 2 ) ) ) -> p || ( ( E ^ 2 ) + ( F ^ 2 ) ) ) )
284	222, 280, 283	mp2and 715	. . . . 5 |- ( ( ph /\ ( p e. Prime /\ p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) ) -> p || ( ( E ^ 2 ) + ( F ^ 2 ) ) )
285		breq1 4656	. . . . . . 7 |- ( b = p -> ( b || a <-> p || a ) )
286		eleq1 2689	. . . . . . 7 |- ( b = p -> ( b e. S <-> p e. S ) )
287	285, 286	imbi12d 334	. . . . . 6 |- ( b = p -> ( ( b || a -> b e. S ) <-> ( p || a -> p e. S ) ) )
288		breq2 4657	. . . . . . 7 |- ( a = ( ( E ^ 2 ) + ( F ^ 2 ) ) -> ( p || a <-> p || ( ( E ^ 2 ) + ( F ^ 2 ) ) ) )
289	288	imbi1d 331	. . . . . 6 |- ( a = ( ( E ^ 2 ) + ( F ^ 2 ) ) -> ( ( p || a -> p e. S ) <-> ( p || ( ( E ^ 2 ) + ( F ^ 2 ) ) -> p e. S ) ) )
290	287, 289	rspc2v 3322	. . . . 5 |- ( ( p e. ( 1 ... ( M - 1 ) ) /\ ( ( E ^ 2 ) + ( F ^ 2 ) ) e. Y ) -> ( A. b e. ( 1 ... ( M - 1 ) ) A. a e. Y ( b || a -> b e. S ) -> ( p || ( ( E ^ 2 ) + ( F ^ 2 ) ) -> p e. S ) ) )
291	274, 275, 284, 290	syl3c 66	. . . 4 |- ( ( ph /\ ( p e. Prime /\ p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) ) -> p e. S )
292	291	expr 643	. . 3 |- ( ( ph /\ p e. Prime ) -> ( p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) -> p e. S ) )
293	292	ralrimiva 2966	. 2 |- ( ph -> A. p e. Prime ( p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) -> p e. S ) )
294		inss1 3833	. . . . 5 |- ( S i^i NN ) C_ S
295	173, 294	sstri 3612	. . . 4 |- Y C_ S
296	295, 206	sseldi 3601	. . 3 |- ( ph -> ( ( E ^ 2 ) + ( F ^ 2 ) ) e. S )
297	278, 296	eqeltrd 2701	. 2 |- ( ph -> ( M x. ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) e. S )
298	1, 5, 212, 293, 297	2sqlem6 25148	1 |- ( ph -> M e. S )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   e. wcel 1990   {cab 2608   =/= wne 2794   A.wral 2912   E.wrex 2913   i^i cin 3573   class class class wbr 4653   |-> cmpt 4729   ran crn 5115   ` cfv 5888  (class class class)co 6650   RRcr 9935   0cc0 9936   1c1 9937   + caddc 9939   x. cmul 9941   < clt 10074   <_ cle 10075   - cmin 10266   / cdiv 10684   NNcn 11020   2c2 11070   NN0cn0 11292   ZZcz 11377   ZZ>=cuz 11687   RR+crp 11832   ...cfz 12326   mod cmo 12668   ^cexp 12860   abscabs 13974   || cdvds 14983   gcd cgcd 15216   Primecprime 15385   ZZ[_i]cgz 15633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-2o 7561  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-sup 8348  df-inf 8349  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-n0 11293  df-z 11378  df-uz 11688  df-rp 11833  df-fz 12327  df-fl 12593  df-mod 12669  df-seq 12802  df-exp 12861  df-cj 13839  df-re 13840  df-im 13841  df-sqrt 13975  df-abs 13976  df-dvds 14984  df-gcd 15217  df-prm 15386  df-gz 15634

This theorem is referenced by:  2sqlem9  25152