Metamath Proof Explorer

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 ⊢ ( 𝜑 → 𝑀 ∈ 𝑆 )