Theorem 2sqlem8

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

	Ref	Expression
Hypotheses	2sq.1	⊢ 𝑆 = ran ( 𝑤 ∈ ℤ[i] ↦ ( ( abs ‘ 𝑤 ) ↑ 2 ) )
	2sqlem7.2	⊢ 𝑌 = { 𝑧 ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( ( 𝑥 gcd 𝑦 ) = 1 ∧ 𝑧 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) }
	2sqlem9.5	⊢ ( 𝜑 → ∀ 𝑏 ∈ ( 1 ... ( 𝑀 − 1 ) ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) )
	2sqlem9.7	⊢ ( 𝜑 → 𝑀 ∥ 𝑁 )
	2sqlem8.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	2sqlem8.m	⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 2 ) )
	2sqlem8.1	⊢ ( 𝜑 → 𝐴 ∈ ℤ )
	2sqlem8.2	⊢ ( 𝜑 → 𝐵 ∈ ℤ )
	2sqlem8.3	⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) = 1 )
	2sqlem8.4	⊢ ( 𝜑 → 𝑁 = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) )
	2sqlem8.c	⊢ 𝐶 = ( ( ( 𝐴 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) )
	2sqlem8.d	⊢ 𝐷 = ( ( ( 𝐵 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) )
	2sqlem8.e	⊢ 𝐸 = ( 𝐶 / ( 𝐶 gcd 𝐷 ) )
	2sqlem8.f	⊢ 𝐹 = ( 𝐷 / ( 𝐶 gcd 𝐷 ) )
Assertion	2sqlem8	⊢ ( 𝜑 → 𝑀 ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		2sq.1	⊢ 𝑆 = ran ( 𝑤 ∈ ℤ[i] ↦ ( ( abs ‘ 𝑤 ) ↑ 2 ) )
2		2sqlem7.2	⊢ 𝑌 = { 𝑧 ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( ( 𝑥 gcd 𝑦 ) = 1 ∧ 𝑧 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) }
3		2sqlem9.5	⊢ ( 𝜑 → ∀ 𝑏 ∈ ( 1 ... ( 𝑀 − 1 ) ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) )
4		2sqlem9.7	⊢ ( 𝜑 → 𝑀 ∥ 𝑁 )
5		2sqlem8.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
6		2sqlem8.m	⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 2 ) )
7		2sqlem8.1	⊢ ( 𝜑 → 𝐴 ∈ ℤ )
8		2sqlem8.2	⊢ ( 𝜑 → 𝐵 ∈ ℤ )
9		2sqlem8.3	⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) = 1 )
10		2sqlem8.4	⊢ ( 𝜑 → 𝑁 = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) )
11		2sqlem8.c	⊢ 𝐶 = ( ( ( 𝐴 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) )
12		2sqlem8.d	⊢ 𝐷 = ( ( ( 𝐵 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) )
13		2sqlem8.e	⊢ 𝐸 = ( 𝐶 / ( 𝐶 gcd 𝐷 ) )
14		2sqlem8.f	⊢ 𝐹 = ( 𝐷 / ( 𝐶 gcd 𝐷 ) )
15		eluz2b3	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑀 ∈ ℕ ∧ 𝑀 ≠ 1 ) )
16	6 15	sylib	⊢ ( 𝜑 → ( 𝑀 ∈ ℕ ∧ 𝑀 ≠ 1 ) )
17	16	simpld	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
18		eluzelz	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 2 ) → 𝑀 ∈ ℤ )
19	6 18	syl	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
20	5	nnzd	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
21	7 17 11	4sqlem5	⊢ ( 𝜑 → ( 𝐶 ∈ ℤ ∧ ( ( 𝐴 − 𝐶 ) / 𝑀 ) ∈ ℤ ) )
22	21	simpld	⊢ ( 𝜑 → 𝐶 ∈ ℤ )
23		zsqcl	⊢ ( 𝐶 ∈ ℤ → ( 𝐶 ↑ 2 ) ∈ ℤ )
24	22 23	syl	⊢ ( 𝜑 → ( 𝐶 ↑ 2 ) ∈ ℤ )
25	8 17 12	4sqlem5	⊢ ( 𝜑 → ( 𝐷 ∈ ℤ ∧ ( ( 𝐵 − 𝐷 ) / 𝑀 ) ∈ ℤ ) )
26	25	simpld	⊢ ( 𝜑 → 𝐷 ∈ ℤ )
27		zsqcl	⊢ ( 𝐷 ∈ ℤ → ( 𝐷 ↑ 2 ) ∈ ℤ )
28	26 27	syl	⊢ ( 𝜑 → ( 𝐷 ↑ 2 ) ∈ ℤ )
29	24 28	zaddcld	⊢ ( 𝜑 → ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ∈ ℤ )
30		zsqcl	⊢ ( 𝐴 ∈ ℤ → ( 𝐴 ↑ 2 ) ∈ ℤ )
31	7 30	syl	⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) ∈ ℤ )
32	31 24	zsubcld	⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) − ( 𝐶 ↑ 2 ) ) ∈ ℤ )
33		zsqcl	⊢ ( 𝐵 ∈ ℤ → ( 𝐵 ↑ 2 ) ∈ ℤ )
34	8 33	syl	⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) ∈ ℤ )
35	34 28	zsubcld	⊢ ( 𝜑 → ( ( 𝐵 ↑ 2 ) − ( 𝐷 ↑ 2 ) ) ∈ ℤ )
36	7 17 11	4sqlem8	⊢ ( 𝜑 → 𝑀 ∥ ( ( 𝐴 ↑ 2 ) − ( 𝐶 ↑ 2 ) ) )
37	8 17 12	4sqlem8	⊢ ( 𝜑 → 𝑀 ∥ ( ( 𝐵 ↑ 2 ) − ( 𝐷 ↑ 2 ) ) )
38	19 32 35 36 37	dvds2addd	⊢ ( 𝜑 → 𝑀 ∥ ( ( ( 𝐴 ↑ 2 ) − ( 𝐶 ↑ 2 ) ) + ( ( 𝐵 ↑ 2 ) − ( 𝐷 ↑ 2 ) ) ) )
39	10	oveq1d	⊢ ( 𝜑 → ( 𝑁 − ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) = ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) − ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) )
40	31	zcnd	⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) ∈ ℂ )
41	34	zcnd	⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) ∈ ℂ )
42	24	zcnd	⊢ ( 𝜑 → ( 𝐶 ↑ 2 ) ∈ ℂ )
43	28	zcnd	⊢ ( 𝜑 → ( 𝐷 ↑ 2 ) ∈ ℂ )
44	40 41 42 43	addsub4d	⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) − ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) = ( ( ( 𝐴 ↑ 2 ) − ( 𝐶 ↑ 2 ) ) + ( ( 𝐵 ↑ 2 ) − ( 𝐷 ↑ 2 ) ) ) )
45	39 44	eqtrd	⊢ ( 𝜑 → ( 𝑁 − ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) = ( ( ( 𝐴 ↑ 2 ) − ( 𝐶 ↑ 2 ) ) + ( ( 𝐵 ↑ 2 ) − ( 𝐷 ↑ 2 ) ) ) )
46	38 45	breqtrrd	⊢ ( 𝜑 → 𝑀 ∥ ( 𝑁 − ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) )
47		dvdssub2	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ∈ ℤ ) ∧ 𝑀 ∥ ( 𝑁 − ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) ) → ( 𝑀 ∥ 𝑁 ↔ 𝑀 ∥ ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) )
48	19 20 29 46 47	syl31anc	⊢ ( 𝜑 → ( 𝑀 ∥ 𝑁 ↔ 𝑀 ∥ ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) )
49	4 48	mpbid	⊢ ( 𝜑 → 𝑀 ∥ ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) )
50	1 2 3 4 5 6 7 8 9 10 11 12	2sqlem8a	⊢ ( 𝜑 → ( 𝐶 gcd 𝐷 ) ∈ ℕ )
51	50	nnzd	⊢ ( 𝜑 → ( 𝐶 gcd 𝐷 ) ∈ ℤ )
52		zsqcl2	⊢ ( ( 𝐶 gcd 𝐷 ) ∈ ℤ → ( ( 𝐶 gcd 𝐷 ) ↑ 2 ) ∈ ℕ0 )
53	51 52	syl	⊢ ( 𝜑 → ( ( 𝐶 gcd 𝐷 ) ↑ 2 ) ∈ ℕ0 )
54	53	nn0cnd	⊢ ( 𝜑 → ( ( 𝐶 gcd 𝐷 ) ↑ 2 ) ∈ ℂ )
55		gcddvds	⊢ ( ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) → ( ( 𝐶 gcd 𝐷 ) ∥ 𝐶 ∧ ( 𝐶 gcd 𝐷 ) ∥ 𝐷 ) )
56	22 26 55	syl2anc	⊢ ( 𝜑 → ( ( 𝐶 gcd 𝐷 ) ∥ 𝐶 ∧ ( 𝐶 gcd 𝐷 ) ∥ 𝐷 ) )
57	56	simpld	⊢ ( 𝜑 → ( 𝐶 gcd 𝐷 ) ∥ 𝐶 )
58	50	nnne0d	⊢ ( 𝜑 → ( 𝐶 gcd 𝐷 ) ≠ 0 )
59		dvdsval2	⊢ ( ( ( 𝐶 gcd 𝐷 ) ∈ ℤ ∧ ( 𝐶 gcd 𝐷 ) ≠ 0 ∧ 𝐶 ∈ ℤ ) → ( ( 𝐶 gcd 𝐷 ) ∥ 𝐶 ↔ ( 𝐶 / ( 𝐶 gcd 𝐷 ) ) ∈ ℤ ) )
60	51 58 22 59	syl3anc	⊢ ( 𝜑 → ( ( 𝐶 gcd 𝐷 ) ∥ 𝐶 ↔ ( 𝐶 / ( 𝐶 gcd 𝐷 ) ) ∈ ℤ ) )
61	57 60	mpbid	⊢ ( 𝜑 → ( 𝐶 / ( 𝐶 gcd 𝐷 ) ) ∈ ℤ )
62	13 61	eqeltrid	⊢ ( 𝜑 → 𝐸 ∈ ℤ )
63		zsqcl2	⊢ ( 𝐸 ∈ ℤ → ( 𝐸 ↑ 2 ) ∈ ℕ0 )
64	62 63	syl	⊢ ( 𝜑 → ( 𝐸 ↑ 2 ) ∈ ℕ0 )
65	64	nn0cnd	⊢ ( 𝜑 → ( 𝐸 ↑ 2 ) ∈ ℂ )
66	56	simprd	⊢ ( 𝜑 → ( 𝐶 gcd 𝐷 ) ∥ 𝐷 )
67		dvdsval2	⊢ ( ( ( 𝐶 gcd 𝐷 ) ∈ ℤ ∧ ( 𝐶 gcd 𝐷 ) ≠ 0 ∧ 𝐷 ∈ ℤ ) → ( ( 𝐶 gcd 𝐷 ) ∥ 𝐷 ↔ ( 𝐷 / ( 𝐶 gcd 𝐷 ) ) ∈ ℤ ) )
68	51 58 26 67	syl3anc	⊢ ( 𝜑 → ( ( 𝐶 gcd 𝐷 ) ∥ 𝐷 ↔ ( 𝐷 / ( 𝐶 gcd 𝐷 ) ) ∈ ℤ ) )
69	66 68	mpbid	⊢ ( 𝜑 → ( 𝐷 / ( 𝐶 gcd 𝐷 ) ) ∈ ℤ )
70	14 69	eqeltrid	⊢ ( 𝜑 → 𝐹 ∈ ℤ )
71		zsqcl2	⊢ ( 𝐹 ∈ ℤ → ( 𝐹 ↑ 2 ) ∈ ℕ0 )
72	70 71	syl	⊢ ( 𝜑 → ( 𝐹 ↑ 2 ) ∈ ℕ0 )
73	72	nn0cnd	⊢ ( 𝜑 → ( 𝐹 ↑ 2 ) ∈ ℂ )
74	54 65 73	adddid	⊢ ( 𝜑 → ( ( ( 𝐶 gcd 𝐷 ) ↑ 2 ) · ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ) = ( ( ( ( 𝐶 gcd 𝐷 ) ↑ 2 ) · ( 𝐸 ↑ 2 ) ) + ( ( ( 𝐶 gcd 𝐷 ) ↑ 2 ) · ( 𝐹 ↑ 2 ) ) ) )
75	51	zcnd	⊢ ( 𝜑 → ( 𝐶 gcd 𝐷 ) ∈ ℂ )
76	62	zcnd	⊢ ( 𝜑 → 𝐸 ∈ ℂ )
77	75 76	sqmuld	⊢ ( 𝜑 → ( ( ( 𝐶 gcd 𝐷 ) · 𝐸 ) ↑ 2 ) = ( ( ( 𝐶 gcd 𝐷 ) ↑ 2 ) · ( 𝐸 ↑ 2 ) ) )
78	13	oveq2i	⊢ ( ( 𝐶 gcd 𝐷 ) · 𝐸 ) = ( ( 𝐶 gcd 𝐷 ) · ( 𝐶 / ( 𝐶 gcd 𝐷 ) ) )
79	22	zcnd	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
80	79 75 58	divcan2d	⊢ ( 𝜑 → ( ( 𝐶 gcd 𝐷 ) · ( 𝐶 / ( 𝐶 gcd 𝐷 ) ) ) = 𝐶 )
81	78 80	eqtrid	⊢ ( 𝜑 → ( ( 𝐶 gcd 𝐷 ) · 𝐸 ) = 𝐶 )
82	81	oveq1d	⊢ ( 𝜑 → ( ( ( 𝐶 gcd 𝐷 ) · 𝐸 ) ↑ 2 ) = ( 𝐶 ↑ 2 ) )
83	77 82	eqtr3d	⊢ ( 𝜑 → ( ( ( 𝐶 gcd 𝐷 ) ↑ 2 ) · ( 𝐸 ↑ 2 ) ) = ( 𝐶 ↑ 2 ) )
84	70	zcnd	⊢ ( 𝜑 → 𝐹 ∈ ℂ )
85	75 84	sqmuld	⊢ ( 𝜑 → ( ( ( 𝐶 gcd 𝐷 ) · 𝐹 ) ↑ 2 ) = ( ( ( 𝐶 gcd 𝐷 ) ↑ 2 ) · ( 𝐹 ↑ 2 ) ) )
86	14	oveq2i	⊢ ( ( 𝐶 gcd 𝐷 ) · 𝐹 ) = ( ( 𝐶 gcd 𝐷 ) · ( 𝐷 / ( 𝐶 gcd 𝐷 ) ) )
87	26	zcnd	⊢ ( 𝜑 → 𝐷 ∈ ℂ )
88	87 75 58	divcan2d	⊢ ( 𝜑 → ( ( 𝐶 gcd 𝐷 ) · ( 𝐷 / ( 𝐶 gcd 𝐷 ) ) ) = 𝐷 )
89	86 88	eqtrid	⊢ ( 𝜑 → ( ( 𝐶 gcd 𝐷 ) · 𝐹 ) = 𝐷 )
90	89	oveq1d	⊢ ( 𝜑 → ( ( ( 𝐶 gcd 𝐷 ) · 𝐹 ) ↑ 2 ) = ( 𝐷 ↑ 2 ) )
91	85 90	eqtr3d	⊢ ( 𝜑 → ( ( ( 𝐶 gcd 𝐷 ) ↑ 2 ) · ( 𝐹 ↑ 2 ) ) = ( 𝐷 ↑ 2 ) )
92	83 91	oveq12d	⊢ ( 𝜑 → ( ( ( ( 𝐶 gcd 𝐷 ) ↑ 2 ) · ( 𝐸 ↑ 2 ) ) + ( ( ( 𝐶 gcd 𝐷 ) ↑ 2 ) · ( 𝐹 ↑ 2 ) ) ) = ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) )
93	74 92	eqtrd	⊢ ( 𝜑 → ( ( ( 𝐶 gcd 𝐷 ) ↑ 2 ) · ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ) = ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) )
94	49 93	breqtrrd	⊢ ( 𝜑 → 𝑀 ∥ ( ( ( 𝐶 gcd 𝐷 ) ↑ 2 ) · ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ) )
95		zsqcl	⊢ ( ( 𝐶 gcd 𝐷 ) ∈ ℤ → ( ( 𝐶 gcd 𝐷 ) ↑ 2 ) ∈ ℤ )
96	51 95	syl	⊢ ( 𝜑 → ( ( 𝐶 gcd 𝐷 ) ↑ 2 ) ∈ ℤ )
97	19 96	gcdcomd	⊢ ( 𝜑 → ( 𝑀 gcd ( ( 𝐶 gcd 𝐷 ) ↑ 2 ) ) = ( ( ( 𝐶 gcd 𝐷 ) ↑ 2 ) gcd 𝑀 ) )
98	51 19	gcdcld	⊢ ( 𝜑 → ( ( 𝐶 gcd 𝐷 ) gcd 𝑀 ) ∈ ℕ0 )
99	98	nn0zd	⊢ ( 𝜑 → ( ( 𝐶 gcd 𝐷 ) gcd 𝑀 ) ∈ ℤ )
100		gcddvds	⊢ ( ( ( 𝐶 gcd 𝐷 ) ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( ( 𝐶 gcd 𝐷 ) gcd 𝑀 ) ∥ ( 𝐶 gcd 𝐷 ) ∧ ( ( 𝐶 gcd 𝐷 ) gcd 𝑀 ) ∥ 𝑀 ) )
101	51 19 100	syl2anc	⊢ ( 𝜑 → ( ( ( 𝐶 gcd 𝐷 ) gcd 𝑀 ) ∥ ( 𝐶 gcd 𝐷 ) ∧ ( ( 𝐶 gcd 𝐷 ) gcd 𝑀 ) ∥ 𝑀 ) )
102	101	simpld	⊢ ( 𝜑 → ( ( 𝐶 gcd 𝐷 ) gcd 𝑀 ) ∥ ( 𝐶 gcd 𝐷 ) )
103	99 51 22 102 57	dvdstrd	⊢ ( 𝜑 → ( ( 𝐶 gcd 𝐷 ) gcd 𝑀 ) ∥ 𝐶 )
104	7 22	zsubcld	⊢ ( 𝜑 → ( 𝐴 − 𝐶 ) ∈ ℤ )
105	101	simprd	⊢ ( 𝜑 → ( ( 𝐶 gcd 𝐷 ) gcd 𝑀 ) ∥ 𝑀 )
106	21	simprd	⊢ ( 𝜑 → ( ( 𝐴 − 𝐶 ) / 𝑀 ) ∈ ℤ )
107	17	nnne0d	⊢ ( 𝜑 → 𝑀 ≠ 0 )
108		dvdsval2	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ ( 𝐴 − 𝐶 ) ∈ ℤ ) → ( 𝑀 ∥ ( 𝐴 − 𝐶 ) ↔ ( ( 𝐴 − 𝐶 ) / 𝑀 ) ∈ ℤ ) )
109	19 107 104 108	syl3anc	⊢ ( 𝜑 → ( 𝑀 ∥ ( 𝐴 − 𝐶 ) ↔ ( ( 𝐴 − 𝐶 ) / 𝑀 ) ∈ ℤ ) )
110	106 109	mpbird	⊢ ( 𝜑 → 𝑀 ∥ ( 𝐴 − 𝐶 ) )
111	99 19 104 105 110	dvdstrd	⊢ ( 𝜑 → ( ( 𝐶 gcd 𝐷 ) gcd 𝑀 ) ∥ ( 𝐴 − 𝐶 ) )
112		dvdssub2	⊢ ( ( ( ( ( 𝐶 gcd 𝐷 ) gcd 𝑀 ) ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( ( 𝐶 gcd 𝐷 ) gcd 𝑀 ) ∥ ( 𝐴 − 𝐶 ) ) → ( ( ( 𝐶 gcd 𝐷 ) gcd 𝑀 ) ∥ 𝐴 ↔ ( ( 𝐶 gcd 𝐷 ) gcd 𝑀 ) ∥ 𝐶 ) )
113	99 7 22 111 112	syl31anc	⊢ ( 𝜑 → ( ( ( 𝐶 gcd 𝐷 ) gcd 𝑀 ) ∥ 𝐴 ↔ ( ( 𝐶 gcd 𝐷 ) gcd 𝑀 ) ∥ 𝐶 ) )
114	103 113	mpbird	⊢ ( 𝜑 → ( ( 𝐶 gcd 𝐷 ) gcd 𝑀 ) ∥ 𝐴 )
115	99 51 26 102 66	dvdstrd	⊢ ( 𝜑 → ( ( 𝐶 gcd 𝐷 ) gcd 𝑀 ) ∥ 𝐷 )
116	8 26	zsubcld	⊢ ( 𝜑 → ( 𝐵 − 𝐷 ) ∈ ℤ )
117	25	simprd	⊢ ( 𝜑 → ( ( 𝐵 − 𝐷 ) / 𝑀 ) ∈ ℤ )
118		dvdsval2	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ ( 𝐵 − 𝐷 ) ∈ ℤ ) → ( 𝑀 ∥ ( 𝐵 − 𝐷 ) ↔ ( ( 𝐵 − 𝐷 ) / 𝑀 ) ∈ ℤ ) )
119	19 107 116 118	syl3anc	⊢ ( 𝜑 → ( 𝑀 ∥ ( 𝐵 − 𝐷 ) ↔ ( ( 𝐵 − 𝐷 ) / 𝑀 ) ∈ ℤ ) )
120	117 119	mpbird	⊢ ( 𝜑 → 𝑀 ∥ ( 𝐵 − 𝐷 ) )
121	99 19 116 105 120	dvdstrd	⊢ ( 𝜑 → ( ( 𝐶 gcd 𝐷 ) gcd 𝑀 ) ∥ ( 𝐵 − 𝐷 ) )
122		dvdssub2	⊢ ( ( ( ( ( 𝐶 gcd 𝐷 ) gcd 𝑀 ) ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ∧ ( ( 𝐶 gcd 𝐷 ) gcd 𝑀 ) ∥ ( 𝐵 − 𝐷 ) ) → ( ( ( 𝐶 gcd 𝐷 ) gcd 𝑀 ) ∥ 𝐵 ↔ ( ( 𝐶 gcd 𝐷 ) gcd 𝑀 ) ∥ 𝐷 ) )
123	99 8 26 121 122	syl31anc	⊢ ( 𝜑 → ( ( ( 𝐶 gcd 𝐷 ) gcd 𝑀 ) ∥ 𝐵 ↔ ( ( 𝐶 gcd 𝐷 ) gcd 𝑀 ) ∥ 𝐷 ) )
124	115 123	mpbird	⊢ ( 𝜑 → ( ( 𝐶 gcd 𝐷 ) gcd 𝑀 ) ∥ 𝐵 )
125		ax-1ne0	⊢ 1 ≠ 0
126	125	a1i	⊢ ( 𝜑 → 1 ≠ 0 )
127	9 126	eqnetrd	⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) ≠ 0 )
128	127	neneqd	⊢ ( 𝜑 → ¬ ( 𝐴 gcd 𝐵 ) = 0 )
129		gcdeq0	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 gcd 𝐵 ) = 0 ↔ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) )
130	7 8 129	syl2anc	⊢ ( 𝜑 → ( ( 𝐴 gcd 𝐵 ) = 0 ↔ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) )
131	128 130	mtbid	⊢ ( 𝜑 → ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) )
132		dvdslegcd	⊢ ( ( ( ( ( 𝐶 gcd 𝐷 ) gcd 𝑀 ) ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) → ( ( ( ( 𝐶 gcd 𝐷 ) gcd 𝑀 ) ∥ 𝐴 ∧ ( ( 𝐶 gcd 𝐷 ) gcd 𝑀 ) ∥ 𝐵 ) → ( ( 𝐶 gcd 𝐷 ) gcd 𝑀 ) ≤ ( 𝐴 gcd 𝐵 ) ) )
133	99 7 8 131 132	syl31anc	⊢ ( 𝜑 → ( ( ( ( 𝐶 gcd 𝐷 ) gcd 𝑀 ) ∥ 𝐴 ∧ ( ( 𝐶 gcd 𝐷 ) gcd 𝑀 ) ∥ 𝐵 ) → ( ( 𝐶 gcd 𝐷 ) gcd 𝑀 ) ≤ ( 𝐴 gcd 𝐵 ) ) )
134	114 124 133	mp2and	⊢ ( 𝜑 → ( ( 𝐶 gcd 𝐷 ) gcd 𝑀 ) ≤ ( 𝐴 gcd 𝐵 ) )
135	134 9	breqtrd	⊢ ( 𝜑 → ( ( 𝐶 gcd 𝐷 ) gcd 𝑀 ) ≤ 1 )
136		simpr	⊢ ( ( ( 𝐶 gcd 𝐷 ) = 0 ∧ 𝑀 = 0 ) → 𝑀 = 0 )
137	136	necon3ai	⊢ ( 𝑀 ≠ 0 → ¬ ( ( 𝐶 gcd 𝐷 ) = 0 ∧ 𝑀 = 0 ) )
138	107 137	syl	⊢ ( 𝜑 → ¬ ( ( 𝐶 gcd 𝐷 ) = 0 ∧ 𝑀 = 0 ) )
139		gcdn0cl	⊢ ( ( ( ( 𝐶 gcd 𝐷 ) ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ ¬ ( ( 𝐶 gcd 𝐷 ) = 0 ∧ 𝑀 = 0 ) ) → ( ( 𝐶 gcd 𝐷 ) gcd 𝑀 ) ∈ ℕ )
140	51 19 138 139	syl21anc	⊢ ( 𝜑 → ( ( 𝐶 gcd 𝐷 ) gcd 𝑀 ) ∈ ℕ )
141		nnle1eq1	⊢ ( ( ( 𝐶 gcd 𝐷 ) gcd 𝑀 ) ∈ ℕ → ( ( ( 𝐶 gcd 𝐷 ) gcd 𝑀 ) ≤ 1 ↔ ( ( 𝐶 gcd 𝐷 ) gcd 𝑀 ) = 1 ) )
142	140 141	syl	⊢ ( 𝜑 → ( ( ( 𝐶 gcd 𝐷 ) gcd 𝑀 ) ≤ 1 ↔ ( ( 𝐶 gcd 𝐷 ) gcd 𝑀 ) = 1 ) )
143	135 142	mpbid	⊢ ( 𝜑 → ( ( 𝐶 gcd 𝐷 ) gcd 𝑀 ) = 1 )
144		2nn	⊢ 2 ∈ ℕ
145	144	a1i	⊢ ( 𝜑 → 2 ∈ ℕ )
146		rplpwr	⊢ ( ( ( 𝐶 gcd 𝐷 ) ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 2 ∈ ℕ ) → ( ( ( 𝐶 gcd 𝐷 ) gcd 𝑀 ) = 1 → ( ( ( 𝐶 gcd 𝐷 ) ↑ 2 ) gcd 𝑀 ) = 1 ) )
147	50 17 145 146	syl3anc	⊢ ( 𝜑 → ( ( ( 𝐶 gcd 𝐷 ) gcd 𝑀 ) = 1 → ( ( ( 𝐶 gcd 𝐷 ) ↑ 2 ) gcd 𝑀 ) = 1 ) )
148	143 147	mpd	⊢ ( 𝜑 → ( ( ( 𝐶 gcd 𝐷 ) ↑ 2 ) gcd 𝑀 ) = 1 )
149	97 148	eqtrd	⊢ ( 𝜑 → ( 𝑀 gcd ( ( 𝐶 gcd 𝐷 ) ↑ 2 ) ) = 1 )
150	64 72	nn0addcld	⊢ ( 𝜑 → ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ∈ ℕ0 )
151	150	nn0zd	⊢ ( 𝜑 → ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ∈ ℤ )
152		coprmdvds	⊢ ( ( 𝑀 ∈ ℤ ∧ ( ( 𝐶 gcd 𝐷 ) ↑ 2 ) ∈ ℤ ∧ ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ∈ ℤ ) → ( ( 𝑀 ∥ ( ( ( 𝐶 gcd 𝐷 ) ↑ 2 ) · ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ) ∧ ( 𝑀 gcd ( ( 𝐶 gcd 𝐷 ) ↑ 2 ) ) = 1 ) → 𝑀 ∥ ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ) )
153	19 96 151 152	syl3anc	⊢ ( 𝜑 → ( ( 𝑀 ∥ ( ( ( 𝐶 gcd 𝐷 ) ↑ 2 ) · ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ) ∧ ( 𝑀 gcd ( ( 𝐶 gcd 𝐷 ) ↑ 2 ) ) = 1 ) → 𝑀 ∥ ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ) )
154	94 149 153	mp2and	⊢ ( 𝜑 → 𝑀 ∥ ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) )
155		dvdsval2	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ∈ ℤ ) → ( 𝑀 ∥ ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ↔ ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) ∈ ℤ ) )
156	19 107 151 155	syl3anc	⊢ ( 𝜑 → ( 𝑀 ∥ ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ↔ ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) ∈ ℤ ) )
157	154 156	mpbid	⊢ ( 𝜑 → ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) ∈ ℤ )
158	64	nn0red	⊢ ( 𝜑 → ( 𝐸 ↑ 2 ) ∈ ℝ )
159	72	nn0red	⊢ ( 𝜑 → ( 𝐹 ↑ 2 ) ∈ ℝ )
160	158 159	readdcld	⊢ ( 𝜑 → ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ∈ ℝ )
161	17	nnred	⊢ ( 𝜑 → 𝑀 ∈ ℝ )
162	1 2	2sqlem7	⊢ 𝑌 ⊆ ( 𝑆 ∩ ℕ )
163		inss2	⊢ ( 𝑆 ∩ ℕ ) ⊆ ℕ
164	162 163	sstri	⊢ 𝑌 ⊆ ℕ
165	62 70	gcdcld	⊢ ( 𝜑 → ( 𝐸 gcd 𝐹 ) ∈ ℕ0 )
166	165	nn0cnd	⊢ ( 𝜑 → ( 𝐸 gcd 𝐹 ) ∈ ℂ )
167		1cnd	⊢ ( 𝜑 → 1 ∈ ℂ )
168	75	mulridd	⊢ ( 𝜑 → ( ( 𝐶 gcd 𝐷 ) · 1 ) = ( 𝐶 gcd 𝐷 ) )
169	81 89	oveq12d	⊢ ( 𝜑 → ( ( ( 𝐶 gcd 𝐷 ) · 𝐸 ) gcd ( ( 𝐶 gcd 𝐷 ) · 𝐹 ) ) = ( 𝐶 gcd 𝐷 ) )
170	22 26	gcdcld	⊢ ( 𝜑 → ( 𝐶 gcd 𝐷 ) ∈ ℕ0 )
171		mulgcd	⊢ ( ( ( 𝐶 gcd 𝐷 ) ∈ ℕ0 ∧ 𝐸 ∈ ℤ ∧ 𝐹 ∈ ℤ ) → ( ( ( 𝐶 gcd 𝐷 ) · 𝐸 ) gcd ( ( 𝐶 gcd 𝐷 ) · 𝐹 ) ) = ( ( 𝐶 gcd 𝐷 ) · ( 𝐸 gcd 𝐹 ) ) )
172	170 62 70 171	syl3anc	⊢ ( 𝜑 → ( ( ( 𝐶 gcd 𝐷 ) · 𝐸 ) gcd ( ( 𝐶 gcd 𝐷 ) · 𝐹 ) ) = ( ( 𝐶 gcd 𝐷 ) · ( 𝐸 gcd 𝐹 ) ) )
173	168 169 172	3eqtr2rd	⊢ ( 𝜑 → ( ( 𝐶 gcd 𝐷 ) · ( 𝐸 gcd 𝐹 ) ) = ( ( 𝐶 gcd 𝐷 ) · 1 ) )
174	166 167 75 58 173	mulcanad	⊢ ( 𝜑 → ( 𝐸 gcd 𝐹 ) = 1 )
175		eqidd	⊢ ( 𝜑 → ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) = ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) )
176		oveq1	⊢ ( 𝑥 = 𝐸 → ( 𝑥 gcd 𝑦 ) = ( 𝐸 gcd 𝑦 ) )
177	176	eqeq1d	⊢ ( 𝑥 = 𝐸 → ( ( 𝑥 gcd 𝑦 ) = 1 ↔ ( 𝐸 gcd 𝑦 ) = 1 ) )
178		oveq1	⊢ ( 𝑥 = 𝐸 → ( 𝑥 ↑ 2 ) = ( 𝐸 ↑ 2 ) )
179	178	oveq1d	⊢ ( 𝑥 = 𝐸 → ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( ( 𝐸 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) )
180	179	eqeq2d	⊢ ( 𝑥 = 𝐸 → ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ↔ ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) = ( ( 𝐸 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) )
181	177 180	anbi12d	⊢ ( 𝑥 = 𝐸 → ( ( ( 𝑥 gcd 𝑦 ) = 1 ∧ ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ↔ ( ( 𝐸 gcd 𝑦 ) = 1 ∧ ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) = ( ( 𝐸 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ) )
182		oveq2	⊢ ( 𝑦 = 𝐹 → ( 𝐸 gcd 𝑦 ) = ( 𝐸 gcd 𝐹 ) )
183	182	eqeq1d	⊢ ( 𝑦 = 𝐹 → ( ( 𝐸 gcd 𝑦 ) = 1 ↔ ( 𝐸 gcd 𝐹 ) = 1 ) )
184		oveq1	⊢ ( 𝑦 = 𝐹 → ( 𝑦 ↑ 2 ) = ( 𝐹 ↑ 2 ) )
185	184	oveq2d	⊢ ( 𝑦 = 𝐹 → ( ( 𝐸 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) )
186	185	eqeq2d	⊢ ( 𝑦 = 𝐹 → ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) = ( ( 𝐸 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ↔ ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) = ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ) )
187	183 186	anbi12d	⊢ ( 𝑦 = 𝐹 → ( ( ( 𝐸 gcd 𝑦 ) = 1 ∧ ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) = ( ( 𝐸 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ↔ ( ( 𝐸 gcd 𝐹 ) = 1 ∧ ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) = ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ) ) )
188	181 187	rspc2ev	⊢ ( ( 𝐸 ∈ ℤ ∧ 𝐹 ∈ ℤ ∧ ( ( 𝐸 gcd 𝐹 ) = 1 ∧ ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) = ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ) ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( ( 𝑥 gcd 𝑦 ) = 1 ∧ ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) )
189	62 70 174 175 188	syl112anc	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( ( 𝑥 gcd 𝑦 ) = 1 ∧ ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) )
190		ovex	⊢ ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ∈ V
191		eqeq1	⊢ ( 𝑧 = ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) → ( 𝑧 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ↔ ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) )
192	191	anbi2d	⊢ ( 𝑧 = ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) → ( ( ( 𝑥 gcd 𝑦 ) = 1 ∧ 𝑧 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ↔ ( ( 𝑥 gcd 𝑦 ) = 1 ∧ ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ) )
193	192	2rexbidv	⊢ ( 𝑧 = ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) → ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( ( 𝑥 gcd 𝑦 ) = 1 ∧ 𝑧 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( ( 𝑥 gcd 𝑦 ) = 1 ∧ ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ) )
194	190 193 2	elab2	⊢ ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ∈ 𝑌 ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( ( 𝑥 gcd 𝑦 ) = 1 ∧ ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) )
195	189 194	sylibr	⊢ ( 𝜑 → ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ∈ 𝑌 )
196	164 195	sselid	⊢ ( 𝜑 → ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ∈ ℕ )
197	196	nngt0d	⊢ ( 𝜑 → 0 < ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) )
198	17	nngt0d	⊢ ( 𝜑 → 0 < 𝑀 )
199	160 161 197 198	divgt0d	⊢ ( 𝜑 → 0 < ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) )
200		elnnz	⊢ ( ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) ∈ ℕ ↔ ( ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) ∈ ℤ ∧ 0 < ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) ) )
201	157 199 200	sylanbrc	⊢ ( 𝜑 → ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) ∈ ℕ )
202		prmnn	⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℕ )
203	202	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) ) ) → 𝑝 ∈ ℕ )
204	203	nnred	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) ) ) → 𝑝 ∈ ℝ )
205	157	adantr	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) ) ) → ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) ∈ ℤ )
206	205	zred	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) ) ) → ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) ∈ ℝ )
207		peano2zm	⊢ ( 𝑀 ∈ ℤ → ( 𝑀 − 1 ) ∈ ℤ )
208	19 207	syl	⊢ ( 𝜑 → ( 𝑀 − 1 ) ∈ ℤ )
209	208	zred	⊢ ( 𝜑 → ( 𝑀 − 1 ) ∈ ℝ )
210	209	adantr	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) ) ) → ( 𝑀 − 1 ) ∈ ℝ )
211		simprr	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) ) ) → 𝑝 ∥ ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) )
212		prmz	⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℤ )
213	212	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) ) ) → 𝑝 ∈ ℤ )
214	201	adantr	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) ) ) → ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) ∈ ℕ )
215		dvdsle	⊢ ( ( 𝑝 ∈ ℤ ∧ ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) ∈ ℕ ) → ( 𝑝 ∥ ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) → 𝑝 ≤ ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) ) )
216	213 214 215	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) ) ) → ( 𝑝 ∥ ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) → 𝑝 ≤ ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) ) )
217	211 216	mpd	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) ) ) → 𝑝 ≤ ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) )
218		zsqcl	⊢ ( 𝑀 ∈ ℤ → ( 𝑀 ↑ 2 ) ∈ ℤ )
219	19 218	syl	⊢ ( 𝜑 → ( 𝑀 ↑ 2 ) ∈ ℤ )
220	219	zred	⊢ ( 𝜑 → ( 𝑀 ↑ 2 ) ∈ ℝ )
221	220	rehalfcld	⊢ ( 𝜑 → ( ( 𝑀 ↑ 2 ) / 2 ) ∈ ℝ )
222	24	zred	⊢ ( 𝜑 → ( 𝐶 ↑ 2 ) ∈ ℝ )
223	28	zred	⊢ ( 𝜑 → ( 𝐷 ↑ 2 ) ∈ ℝ )
224	222 223	readdcld	⊢ ( 𝜑 → ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ∈ ℝ )
225		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
226	50	nnsqcld	⊢ ( 𝜑 → ( ( 𝐶 gcd 𝐷 ) ↑ 2 ) ∈ ℕ )
227	226	nnred	⊢ ( 𝜑 → ( ( 𝐶 gcd 𝐷 ) ↑ 2 ) ∈ ℝ )
228	150	nn0ge0d	⊢ ( 𝜑 → 0 ≤ ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) )
229	226	nnge1d	⊢ ( 𝜑 → 1 ≤ ( ( 𝐶 gcd 𝐷 ) ↑ 2 ) )
230	225 227 160 228 229	lemul1ad	⊢ ( 𝜑 → ( 1 · ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ) ≤ ( ( ( 𝐶 gcd 𝐷 ) ↑ 2 ) · ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ) )
231	150	nn0cnd	⊢ ( 𝜑 → ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ∈ ℂ )
232	231	mullidd	⊢ ( 𝜑 → ( 1 · ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ) = ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) )
233	230 232 93	3brtr3d	⊢ ( 𝜑 → ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ≤ ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) )
234	221	rehalfcld	⊢ ( 𝜑 → ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ∈ ℝ )
235	7 17 11	4sqlem7	⊢ ( 𝜑 → ( 𝐶 ↑ 2 ) ≤ ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) )
236	8 17 12	4sqlem7	⊢ ( 𝜑 → ( 𝐷 ↑ 2 ) ≤ ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) )
237	222 223 234 234 235 236	le2addd	⊢ ( 𝜑 → ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ≤ ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) + ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) )
238	221	recnd	⊢ ( 𝜑 → ( ( 𝑀 ↑ 2 ) / 2 ) ∈ ℂ )
239	238	2halvesd	⊢ ( 𝜑 → ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) + ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) = ( ( 𝑀 ↑ 2 ) / 2 ) )
240	237 239	breqtrd	⊢ ( 𝜑 → ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ≤ ( ( 𝑀 ↑ 2 ) / 2 ) )
241	160 224 221 233 240	letrd	⊢ ( 𝜑 → ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ≤ ( ( 𝑀 ↑ 2 ) / 2 ) )
242	17	nnsqcld	⊢ ( 𝜑 → ( 𝑀 ↑ 2 ) ∈ ℕ )
243	242	nnrpd	⊢ ( 𝜑 → ( 𝑀 ↑ 2 ) ∈ ℝ+ )
244		rphalflt	⊢ ( ( 𝑀 ↑ 2 ) ∈ ℝ+ → ( ( 𝑀 ↑ 2 ) / 2 ) < ( 𝑀 ↑ 2 ) )
245	243 244	syl	⊢ ( 𝜑 → ( ( 𝑀 ↑ 2 ) / 2 ) < ( 𝑀 ↑ 2 ) )
246	160 221 220 241 245	lelttrd	⊢ ( 𝜑 → ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) < ( 𝑀 ↑ 2 ) )
247	19	zcnd	⊢ ( 𝜑 → 𝑀 ∈ ℂ )
248	247	sqvald	⊢ ( 𝜑 → ( 𝑀 ↑ 2 ) = ( 𝑀 · 𝑀 ) )
249	246 248	breqtrd	⊢ ( 𝜑 → ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) < ( 𝑀 · 𝑀 ) )
250		ltdivmul	⊢ ( ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ ( 𝑀 ∈ ℝ ∧ 0 < 𝑀 ) ) → ( ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) < 𝑀 ↔ ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) < ( 𝑀 · 𝑀 ) ) )
251	160 161 161 198 250	syl112anc	⊢ ( 𝜑 → ( ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) < 𝑀 ↔ ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) < ( 𝑀 · 𝑀 ) ) )
252	249 251	mpbird	⊢ ( 𝜑 → ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) < 𝑀 )
253		zltlem1	⊢ ( ( ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) < 𝑀 ↔ ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) ≤ ( 𝑀 − 1 ) ) )
254	157 19 253	syl2anc	⊢ ( 𝜑 → ( ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) < 𝑀 ↔ ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) ≤ ( 𝑀 − 1 ) ) )
255	252 254	mpbid	⊢ ( 𝜑 → ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) ≤ ( 𝑀 − 1 ) )
256	255	adantr	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) ) ) → ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) ≤ ( 𝑀 − 1 ) )
257	204 206 210 217 256	letrd	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) ) ) → 𝑝 ≤ ( 𝑀 − 1 ) )
258	208	adantr	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) ) ) → ( 𝑀 − 1 ) ∈ ℤ )
259		fznn	⊢ ( ( 𝑀 − 1 ) ∈ ℤ → ( 𝑝 ∈ ( 1 ... ( 𝑀 − 1 ) ) ↔ ( 𝑝 ∈ ℕ ∧ 𝑝 ≤ ( 𝑀 − 1 ) ) ) )
260	258 259	syl	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) ) ) → ( 𝑝 ∈ ( 1 ... ( 𝑀 − 1 ) ) ↔ ( 𝑝 ∈ ℕ ∧ 𝑝 ≤ ( 𝑀 − 1 ) ) ) )
261	203 257 260	mpbir2and	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) ) ) → 𝑝 ∈ ( 1 ... ( 𝑀 − 1 ) ) )
262	195	adantr	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) ) ) → ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ∈ 𝑌 )
263	261 262	jca	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) ) ) → ( 𝑝 ∈ ( 1 ... ( 𝑀 − 1 ) ) ∧ ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ∈ 𝑌 ) )
264	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) ) ) → ∀ 𝑏 ∈ ( 1 ... ( 𝑀 − 1 ) ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) )
265	151	adantr	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) ) ) → ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ∈ ℤ )
266		dvdsmul2	⊢ ( ( 𝑀 ∈ ℤ ∧ ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) ∈ ℤ ) → ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) ∥ ( 𝑀 · ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) ) )
267	19 157 266	syl2anc	⊢ ( 𝜑 → ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) ∥ ( 𝑀 · ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) ) )
268	231 247 107	divcan2d	⊢ ( 𝜑 → ( 𝑀 · ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) ) = ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) )
269	267 268	breqtrd	⊢ ( 𝜑 → ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) ∥ ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) )
270	269	adantr	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) ) ) → ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) ∥ ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) )
271	213 205 265 211 270	dvdstrd	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) ) ) → 𝑝 ∥ ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) )
272		breq1	⊢ ( 𝑏 = 𝑝 → ( 𝑏 ∥ 𝑎 ↔ 𝑝 ∥ 𝑎 ) )
273		eleq1w	⊢ ( 𝑏 = 𝑝 → ( 𝑏 ∈ 𝑆 ↔ 𝑝 ∈ 𝑆 ) )
274	272 273	imbi12d	⊢ ( 𝑏 = 𝑝 → ( ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) ↔ ( 𝑝 ∥ 𝑎 → 𝑝 ∈ 𝑆 ) ) )
275		breq2	⊢ ( 𝑎 = ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) → ( 𝑝 ∥ 𝑎 ↔ 𝑝 ∥ ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ) )
276	275	imbi1d	⊢ ( 𝑎 = ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) → ( ( 𝑝 ∥ 𝑎 → 𝑝 ∈ 𝑆 ) ↔ ( 𝑝 ∥ ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) → 𝑝 ∈ 𝑆 ) ) )
277	274 276	rspc2v	⊢ ( ( 𝑝 ∈ ( 1 ... ( 𝑀 − 1 ) ) ∧ ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ∈ 𝑌 ) → ( ∀ 𝑏 ∈ ( 1 ... ( 𝑀 − 1 ) ) ∀ 𝑎 ∈ 𝑌 ( 𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆 ) → ( 𝑝 ∥ ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) → 𝑝 ∈ 𝑆 ) ) )
278	263 264 271 277	syl3c	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) ) ) → 𝑝 ∈ 𝑆 )
279	278	expr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ∥ ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) → 𝑝 ∈ 𝑆 ) )
280	279	ralrimiva	⊢ ( 𝜑 → ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) → 𝑝 ∈ 𝑆 ) )
281		inss1	⊢ ( 𝑆 ∩ ℕ ) ⊆ 𝑆
282	162 281	sstri	⊢ 𝑌 ⊆ 𝑆
283	282 195	sselid	⊢ ( 𝜑 → ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ∈ 𝑆 )
284	268 283	eqeltrd	⊢ ( 𝜑 → ( 𝑀 · ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) / 𝑀 ) ) ∈ 𝑆 )
285	1 17 201 280 284	2sqlem6	⊢ ( 𝜑 → 𝑀 ∈ 𝑆 )