ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  2sqlem8 GIF version

Theorem 2sqlem8 14030
Description: Lemma for 2sq . (Contributed by Mario Carneiro, 20-Jun-2015.)
Hypotheses
Ref Expression
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
Ref Expression
2sqlem8 (𝜑𝑀𝑆)
Distinct variable groups:   𝑎,𝑏,𝑤,𝑥,𝑦,𝑧   𝐴,𝑎,𝑥,𝑦,𝑧   𝑥,𝐶   𝜑,𝑥,𝑦   𝐵,𝑎,𝑏,𝑥,𝑦   𝑀,𝑎,𝑏,𝑥,𝑦,𝑧   𝑆,𝑎,𝑏,𝑥,𝑦,𝑧   𝑥,𝐷   𝐸,𝑎,𝑥,𝑦,𝑧   𝑥,𝑁,𝑦,𝑧   𝑌,𝑎,𝑏,𝑥,𝑦   𝐹,𝑎,𝑥,𝑦,𝑧
Allowed substitution hints:   𝜑(𝑧,𝑤,𝑎,𝑏)   𝐴(𝑤,𝑏)   𝐵(𝑧,𝑤)   𝐶(𝑦,𝑧,𝑤,𝑎,𝑏)   𝐷(𝑦,𝑧,𝑤,𝑎,𝑏)   𝑆(𝑤)   𝐸(𝑤,𝑏)   𝐹(𝑤,𝑏)   𝑀(𝑤)   𝑁(𝑤,𝑎,𝑏)   𝑌(𝑧,𝑤)

Proof of Theorem 2sqlem8
Dummy variable 𝑝 is distinct from all other variables.
StepHypRef Expression
1 2sq.1 . 2 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2))
2 2sqlem8.m . . . 4 (𝜑𝑀 ∈ (ℤ‘2))
3 eluz2b3 9577 . . . 4 (𝑀 ∈ (ℤ‘2) ↔ (𝑀 ∈ ℕ ∧ 𝑀 ≠ 1))
42, 3sylib 122 . . 3 (𝜑 → (𝑀 ∈ ℕ ∧ 𝑀 ≠ 1))
54simpld 112 . 2 (𝜑𝑀 ∈ ℕ)
6 2sqlem9.7 . . . . . . 7 (𝜑𝑀𝑁)
7 eluzelz 9510 . . . . . . . . 9 (𝑀 ∈ (ℤ‘2) → 𝑀 ∈ ℤ)
82, 7syl 14 . . . . . . . 8 (𝜑𝑀 ∈ ℤ)
9 2sqlem8.n . . . . . . . . 9 (𝜑𝑁 ∈ ℕ)
109nnzd 9347 . . . . . . . 8 (𝜑𝑁 ∈ ℤ)
11 2sqlem8.1 . . . . . . . . . . . 12 (𝜑𝐴 ∈ ℤ)
12 2sqlem8.c . . . . . . . . . . . 12 𝐶 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))
1311, 5, 124sqlem5 12347 . . . . . . . . . . 11 (𝜑 → (𝐶 ∈ ℤ ∧ ((𝐴𝐶) / 𝑀) ∈ ℤ))
1413simpld 112 . . . . . . . . . 10 (𝜑𝐶 ∈ ℤ)
15 zsqcl 10560 . . . . . . . . . 10 (𝐶 ∈ ℤ → (𝐶↑2) ∈ ℤ)
1614, 15syl 14 . . . . . . . . 9 (𝜑 → (𝐶↑2) ∈ ℤ)
17 2sqlem8.2 . . . . . . . . . . . 12 (𝜑𝐵 ∈ ℤ)
18 2sqlem8.d . . . . . . . . . . . 12 𝐷 = (((𝐵 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))
1917, 5, 184sqlem5 12347 . . . . . . . . . . 11 (𝜑 → (𝐷 ∈ ℤ ∧ ((𝐵𝐷) / 𝑀) ∈ ℤ))
2019simpld 112 . . . . . . . . . 10 (𝜑𝐷 ∈ ℤ)
21 zsqcl 10560 . . . . . . . . . 10 (𝐷 ∈ ℤ → (𝐷↑2) ∈ ℤ)
2220, 21syl 14 . . . . . . . . 9 (𝜑 → (𝐷↑2) ∈ ℤ)
2316, 22zaddcld 9352 . . . . . . . 8 (𝜑 → ((𝐶↑2) + (𝐷↑2)) ∈ ℤ)
24 zsqcl 10560 . . . . . . . . . . . 12 (𝐴 ∈ ℤ → (𝐴↑2) ∈ ℤ)
2511, 24syl 14 . . . . . . . . . . 11 (𝜑 → (𝐴↑2) ∈ ℤ)
2625, 16zsubcld 9353 . . . . . . . . . 10 (𝜑 → ((𝐴↑2) − (𝐶↑2)) ∈ ℤ)
27 zsqcl 10560 . . . . . . . . . . . 12 (𝐵 ∈ ℤ → (𝐵↑2) ∈ ℤ)
2817, 27syl 14 . . . . . . . . . . 11 (𝜑 → (𝐵↑2) ∈ ℤ)
2928, 22zsubcld 9353 . . . . . . . . . 10 (𝜑 → ((𝐵↑2) − (𝐷↑2)) ∈ ℤ)
3011, 5, 124sqlem8 12350 . . . . . . . . . 10 (𝜑𝑀 ∥ ((𝐴↑2) − (𝐶↑2)))
3117, 5, 184sqlem8 12350 . . . . . . . . . 10 (𝜑𝑀 ∥ ((𝐵↑2) − (𝐷↑2)))
328, 26, 29, 30, 31dvds2addd 11804 . . . . . . . . 9 (𝜑𝑀 ∥ (((𝐴↑2) − (𝐶↑2)) + ((𝐵↑2) − (𝐷↑2))))
33 2sqlem8.4 . . . . . . . . . . 11 (𝜑𝑁 = ((𝐴↑2) + (𝐵↑2)))
3433oveq1d 5880 . . . . . . . . . 10 (𝜑 → (𝑁 − ((𝐶↑2) + (𝐷↑2))) = (((𝐴↑2) + (𝐵↑2)) − ((𝐶↑2) + (𝐷↑2))))
3525zcnd 9349 . . . . . . . . . . 11 (𝜑 → (𝐴↑2) ∈ ℂ)
3628zcnd 9349 . . . . . . . . . . 11 (𝜑 → (𝐵↑2) ∈ ℂ)
3716zcnd 9349 . . . . . . . . . . 11 (𝜑 → (𝐶↑2) ∈ ℂ)
3822zcnd 9349 . . . . . . . . . . 11 (𝜑 → (𝐷↑2) ∈ ℂ)
3935, 36, 37, 38addsub4d 8289 . . . . . . . . . 10 (𝜑 → (((𝐴↑2) + (𝐵↑2)) − ((𝐶↑2) + (𝐷↑2))) = (((𝐴↑2) − (𝐶↑2)) + ((𝐵↑2) − (𝐷↑2))))
4034, 39eqtrd 2208 . . . . . . . . 9 (𝜑 → (𝑁 − ((𝐶↑2) + (𝐷↑2))) = (((𝐴↑2) − (𝐶↑2)) + ((𝐵↑2) − (𝐷↑2))))
4132, 40breqtrrd 4026 . . . . . . . 8 (𝜑𝑀 ∥ (𝑁 − ((𝐶↑2) + (𝐷↑2))))
42 dvdssub2 11810 . . . . . . . 8 (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ((𝐶↑2) + (𝐷↑2)) ∈ ℤ) ∧ 𝑀 ∥ (𝑁 − ((𝐶↑2) + (𝐷↑2)))) → (𝑀𝑁𝑀 ∥ ((𝐶↑2) + (𝐷↑2))))
438, 10, 23, 41, 42syl31anc 1241 . . . . . . 7 (𝜑 → (𝑀𝑁𝑀 ∥ ((𝐶↑2) + (𝐷↑2))))
446, 43mpbid 147 . . . . . 6 (𝜑𝑀 ∥ ((𝐶↑2) + (𝐷↑2)))
45 2sqlem7.2 . . . . . . . . . . . 12 𝑌 = {𝑧 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2)))}
46 2sqlem9.5 . . . . . . . . . . . 12 (𝜑 → ∀𝑏 ∈ (1...(𝑀 − 1))∀𝑎𝑌 (𝑏𝑎𝑏𝑆))
47 2sqlem8.3 . . . . . . . . . . . 12 (𝜑 → (𝐴 gcd 𝐵) = 1)
481, 45, 46, 6, 9, 2, 11, 17, 47, 33, 12, 182sqlem8a 14029 . . . . . . . . . . 11 (𝜑 → (𝐶 gcd 𝐷) ∈ ℕ)
4948nnzd 9347 . . . . . . . . . 10 (𝜑 → (𝐶 gcd 𝐷) ∈ ℤ)
50 zsqcl2 10567 . . . . . . . . . 10 ((𝐶 gcd 𝐷) ∈ ℤ → ((𝐶 gcd 𝐷)↑2) ∈ ℕ0)
5149, 50syl 14 . . . . . . . . 9 (𝜑 → ((𝐶 gcd 𝐷)↑2) ∈ ℕ0)
5251nn0cnd 9204 . . . . . . . 8 (𝜑 → ((𝐶 gcd 𝐷)↑2) ∈ ℂ)
53 2sqlem8.e . . . . . . . . . . 11 𝐸 = (𝐶 / (𝐶 gcd 𝐷))
54 gcddvds 11931 . . . . . . . . . . . . . 14 ((𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ) → ((𝐶 gcd 𝐷) ∥ 𝐶 ∧ (𝐶 gcd 𝐷) ∥ 𝐷))
5514, 20, 54syl2anc 411 . . . . . . . . . . . . 13 (𝜑 → ((𝐶 gcd 𝐷) ∥ 𝐶 ∧ (𝐶 gcd 𝐷) ∥ 𝐷))
5655simpld 112 . . . . . . . . . . . 12 (𝜑 → (𝐶 gcd 𝐷) ∥ 𝐶)
5748nnne0d 8937 . . . . . . . . . . . . 13 (𝜑 → (𝐶 gcd 𝐷) ≠ 0)
58 dvdsval2 11765 . . . . . . . . . . . . 13 (((𝐶 gcd 𝐷) ∈ ℤ ∧ (𝐶 gcd 𝐷) ≠ 0 ∧ 𝐶 ∈ ℤ) → ((𝐶 gcd 𝐷) ∥ 𝐶 ↔ (𝐶 / (𝐶 gcd 𝐷)) ∈ ℤ))
5949, 57, 14, 58syl3anc 1238 . . . . . . . . . . . 12 (𝜑 → ((𝐶 gcd 𝐷) ∥ 𝐶 ↔ (𝐶 / (𝐶 gcd 𝐷)) ∈ ℤ))
6056, 59mpbid 147 . . . . . . . . . . 11 (𝜑 → (𝐶 / (𝐶 gcd 𝐷)) ∈ ℤ)
6153, 60eqeltrid 2262 . . . . . . . . . 10 (𝜑𝐸 ∈ ℤ)
62 zsqcl2 10567 . . . . . . . . . 10 (𝐸 ∈ ℤ → (𝐸↑2) ∈ ℕ0)
6361, 62syl 14 . . . . . . . . 9 (𝜑 → (𝐸↑2) ∈ ℕ0)
6463nn0cnd 9204 . . . . . . . 8 (𝜑 → (𝐸↑2) ∈ ℂ)
65 2sqlem8.f . . . . . . . . . . 11 𝐹 = (𝐷 / (𝐶 gcd 𝐷))
6655simprd 114 . . . . . . . . . . . 12 (𝜑 → (𝐶 gcd 𝐷) ∥ 𝐷)
67 dvdsval2 11765 . . . . . . . . . . . . 13 (((𝐶 gcd 𝐷) ∈ ℤ ∧ (𝐶 gcd 𝐷) ≠ 0 ∧ 𝐷 ∈ ℤ) → ((𝐶 gcd 𝐷) ∥ 𝐷 ↔ (𝐷 / (𝐶 gcd 𝐷)) ∈ ℤ))
6849, 57, 20, 67syl3anc 1238 . . . . . . . . . . . 12 (𝜑 → ((𝐶 gcd 𝐷) ∥ 𝐷 ↔ (𝐷 / (𝐶 gcd 𝐷)) ∈ ℤ))
6966, 68mpbid 147 . . . . . . . . . . 11 (𝜑 → (𝐷 / (𝐶 gcd 𝐷)) ∈ ℤ)
7065, 69eqeltrid 2262 . . . . . . . . . 10 (𝜑𝐹 ∈ ℤ)
71 zsqcl2 10567 . . . . . . . . . 10 (𝐹 ∈ ℤ → (𝐹↑2) ∈ ℕ0)
7270, 71syl 14 . . . . . . . . 9 (𝜑 → (𝐹↑2) ∈ ℕ0)
7372nn0cnd 9204 . . . . . . . 8 (𝜑 → (𝐹↑2) ∈ ℂ)
7452, 64, 73adddid 7956 . . . . . . 7 (𝜑 → (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2))) = ((((𝐶 gcd 𝐷)↑2) · (𝐸↑2)) + (((𝐶 gcd 𝐷)↑2) · (𝐹↑2))))
7549zcnd 9349 . . . . . . . . . 10 (𝜑 → (𝐶 gcd 𝐷) ∈ ℂ)
7661zcnd 9349 . . . . . . . . . 10 (𝜑𝐸 ∈ ℂ)
7775, 76sqmuld 10635 . . . . . . . . 9 (𝜑 → (((𝐶 gcd 𝐷) · 𝐸)↑2) = (((𝐶 gcd 𝐷)↑2) · (𝐸↑2)))
7853oveq2i 5876 . . . . . . . . . . 11 ((𝐶 gcd 𝐷) · 𝐸) = ((𝐶 gcd 𝐷) · (𝐶 / (𝐶 gcd 𝐷)))
7914zcnd 9349 . . . . . . . . . . . 12 (𝜑𝐶 ∈ ℂ)
8048nnap0d 8938 . . . . . . . . . . . 12 (𝜑 → (𝐶 gcd 𝐷) # 0)
8179, 75, 80divcanap2d 8722 . . . . . . . . . . 11 (𝜑 → ((𝐶 gcd 𝐷) · (𝐶 / (𝐶 gcd 𝐷))) = 𝐶)
8278, 81eqtrid 2220 . . . . . . . . . 10 (𝜑 → ((𝐶 gcd 𝐷) · 𝐸) = 𝐶)
8382oveq1d 5880 . . . . . . . . 9 (𝜑 → (((𝐶 gcd 𝐷) · 𝐸)↑2) = (𝐶↑2))
8477, 83eqtr3d 2210 . . . . . . . 8 (𝜑 → (((𝐶 gcd 𝐷)↑2) · (𝐸↑2)) = (𝐶↑2))
8570zcnd 9349 . . . . . . . . . 10 (𝜑𝐹 ∈ ℂ)
8675, 85sqmuld 10635 . . . . . . . . 9 (𝜑 → (((𝐶 gcd 𝐷) · 𝐹)↑2) = (((𝐶 gcd 𝐷)↑2) · (𝐹↑2)))
8765oveq2i 5876 . . . . . . . . . . 11 ((𝐶 gcd 𝐷) · 𝐹) = ((𝐶 gcd 𝐷) · (𝐷 / (𝐶 gcd 𝐷)))
8820zcnd 9349 . . . . . . . . . . . 12 (𝜑𝐷 ∈ ℂ)
8988, 75, 80divcanap2d 8722 . . . . . . . . . . 11 (𝜑 → ((𝐶 gcd 𝐷) · (𝐷 / (𝐶 gcd 𝐷))) = 𝐷)
9087, 89eqtrid 2220 . . . . . . . . . 10 (𝜑 → ((𝐶 gcd 𝐷) · 𝐹) = 𝐷)
9190oveq1d 5880 . . . . . . . . 9 (𝜑 → (((𝐶 gcd 𝐷) · 𝐹)↑2) = (𝐷↑2))
9286, 91eqtr3d 2210 . . . . . . . 8 (𝜑 → (((𝐶 gcd 𝐷)↑2) · (𝐹↑2)) = (𝐷↑2))
9384, 92oveq12d 5883 . . . . . . 7 (𝜑 → ((((𝐶 gcd 𝐷)↑2) · (𝐸↑2)) + (((𝐶 gcd 𝐷)↑2) · (𝐹↑2))) = ((𝐶↑2) + (𝐷↑2)))
9474, 93eqtrd 2208 . . . . . 6 (𝜑 → (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2))) = ((𝐶↑2) + (𝐷↑2)))
9544, 94breqtrrd 4026 . . . . 5 (𝜑𝑀 ∥ (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2))))
96 zsqcl 10560 . . . . . . . 8 ((𝐶 gcd 𝐷) ∈ ℤ → ((𝐶 gcd 𝐷)↑2) ∈ ℤ)
9749, 96syl 14 . . . . . . 7 (𝜑 → ((𝐶 gcd 𝐷)↑2) ∈ ℤ)
988, 97gcdcomd 11942 . . . . . 6 (𝜑 → (𝑀 gcd ((𝐶 gcd 𝐷)↑2)) = (((𝐶 gcd 𝐷)↑2) gcd 𝑀))
9949, 8gcdcld 11936 . . . . . . . . . . . . 13 (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℕ0)
10099nn0zd 9346 . . . . . . . . . . . 12 (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℤ)
101 gcddvds 11931 . . . . . . . . . . . . . 14 (((𝐶 gcd 𝐷) ∈ ℤ ∧ 𝑀 ∈ ℤ) → (((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐶 gcd 𝐷) ∧ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝑀))
10249, 8, 101syl2anc 411 . . . . . . . . . . . . 13 (𝜑 → (((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐶 gcd 𝐷) ∧ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝑀))
103102simpld 112 . . . . . . . . . . . 12 (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐶 gcd 𝐷))
104100, 49, 14, 103, 56dvdstrd 11805 . . . . . . . . . . 11 (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐶)
10511, 14zsubcld 9353 . . . . . . . . . . . . 13 (𝜑 → (𝐴𝐶) ∈ ℤ)
106102simprd 114 . . . . . . . . . . . . 13 (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝑀)
10713simprd 114 . . . . . . . . . . . . . 14 (𝜑 → ((𝐴𝐶) / 𝑀) ∈ ℤ)
1085nnne0d 8937 . . . . . . . . . . . . . . 15 (𝜑𝑀 ≠ 0)
109 dvdsval2 11765 . . . . . . . . . . . . . . 15 ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ (𝐴𝐶) ∈ ℤ) → (𝑀 ∥ (𝐴𝐶) ↔ ((𝐴𝐶) / 𝑀) ∈ ℤ))
1108, 108, 105, 109syl3anc 1238 . . . . . . . . . . . . . 14 (𝜑 → (𝑀 ∥ (𝐴𝐶) ↔ ((𝐴𝐶) / 𝑀) ∈ ℤ))
111107, 110mpbird 167 . . . . . . . . . . . . 13 (𝜑𝑀 ∥ (𝐴𝐶))
112100, 8, 105, 106, 111dvdstrd 11805 . . . . . . . . . . . 12 (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐴𝐶))
113 dvdssub2 11810 . . . . . . . . . . . 12 (((((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐴𝐶)) → (((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐴 ↔ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐶))
114100, 11, 14, 112, 113syl31anc 1241 . . . . . . . . . . 11 (𝜑 → (((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐴 ↔ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐶))
115104, 114mpbird 167 . . . . . . . . . 10 (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐴)
116100, 49, 20, 103, 66dvdstrd 11805 . . . . . . . . . . 11 (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐷)
11717, 20zsubcld 9353 . . . . . . . . . . . . 13 (𝜑 → (𝐵𝐷) ∈ ℤ)
11819simprd 114 . . . . . . . . . . . . . 14 (𝜑 → ((𝐵𝐷) / 𝑀) ∈ ℤ)
119 dvdsval2 11765 . . . . . . . . . . . . . . 15 ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ (𝐵𝐷) ∈ ℤ) → (𝑀 ∥ (𝐵𝐷) ↔ ((𝐵𝐷) / 𝑀) ∈ ℤ))
1208, 108, 117, 119syl3anc 1238 . . . . . . . . . . . . . 14 (𝜑 → (𝑀 ∥ (𝐵𝐷) ↔ ((𝐵𝐷) / 𝑀) ∈ ℤ))
121118, 120mpbird 167 . . . . . . . . . . . . 13 (𝜑𝑀 ∥ (𝐵𝐷))
122100, 8, 117, 106, 121dvdstrd 11805 . . . . . . . . . . . 12 (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐵𝐷))
123 dvdssub2 11810 . . . . . . . . . . . 12 (((((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐵𝐷)) → (((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐵 ↔ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐷))
124100, 17, 20, 122, 123syl31anc 1241 . . . . . . . . . . 11 (𝜑 → (((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐵 ↔ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐷))
125116, 124mpbird 167 . . . . . . . . . 10 (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐵)
126 1ne0 8960 . . . . . . . . . . . . . . 15 1 ≠ 0
127126a1i 9 . . . . . . . . . . . . . 14 (𝜑 → 1 ≠ 0)
12847, 127eqnetrd 2369 . . . . . . . . . . . . 13 (𝜑 → (𝐴 gcd 𝐵) ≠ 0)
129128neneqd 2366 . . . . . . . . . . . 12 (𝜑 → ¬ (𝐴 gcd 𝐵) = 0)
130 gcdeq0 11945 . . . . . . . . . . . . 13 ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) = 0 ↔ (𝐴 = 0 ∧ 𝐵 = 0)))
13111, 17, 130syl2anc 411 . . . . . . . . . . . 12 (𝜑 → ((𝐴 gcd 𝐵) = 0 ↔ (𝐴 = 0 ∧ 𝐵 = 0)))
132129, 131mtbid 672 . . . . . . . . . . 11 (𝜑 → ¬ (𝐴 = 0 ∧ 𝐵 = 0))
133 dvdslegcd 11932 . . . . . . . . . . 11 (((((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → ((((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐴 ∧ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐵) → ((𝐶 gcd 𝐷) gcd 𝑀) ≤ (𝐴 gcd 𝐵)))
134100, 11, 17, 132, 133syl31anc 1241 . . . . . . . . . 10 (𝜑 → ((((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐴 ∧ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐵) → ((𝐶 gcd 𝐷) gcd 𝑀) ≤ (𝐴 gcd 𝐵)))
135115, 125, 134mp2and 433 . . . . . . . . 9 (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ≤ (𝐴 gcd 𝐵))
136135, 47breqtrd 4024 . . . . . . . 8 (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ≤ 1)
137 simpr 110 . . . . . . . . . . . 12 (((𝐶 gcd 𝐷) = 0 ∧ 𝑀 = 0) → 𝑀 = 0)
138137necon3ai 2394 . . . . . . . . . . 11 (𝑀 ≠ 0 → ¬ ((𝐶 gcd 𝐷) = 0 ∧ 𝑀 = 0))
139108, 138syl 14 . . . . . . . . . 10 (𝜑 → ¬ ((𝐶 gcd 𝐷) = 0 ∧ 𝑀 = 0))
140 gcdn0cl 11930 . . . . . . . . . 10 ((((𝐶 gcd 𝐷) ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ ¬ ((𝐶 gcd 𝐷) = 0 ∧ 𝑀 = 0)) → ((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℕ)
14149, 8, 139, 140syl21anc 1237 . . . . . . . . 9 (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℕ)
142 nnle1eq1 8916 . . . . . . . . 9 (((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℕ → (((𝐶 gcd 𝐷) gcd 𝑀) ≤ 1 ↔ ((𝐶 gcd 𝐷) gcd 𝑀) = 1))
143141, 142syl 14 . . . . . . . 8 (𝜑 → (((𝐶 gcd 𝐷) gcd 𝑀) ≤ 1 ↔ ((𝐶 gcd 𝐷) gcd 𝑀) = 1))
144136, 143mpbid 147 . . . . . . 7 (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) = 1)
145 2nn 9053 . . . . . . . . 9 2 ∈ ℕ
146145a1i 9 . . . . . . . 8 (𝜑 → 2 ∈ ℕ)
147 rplpwr 11995 . . . . . . . 8 (((𝐶 gcd 𝐷) ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 2 ∈ ℕ) → (((𝐶 gcd 𝐷) gcd 𝑀) = 1 → (((𝐶 gcd 𝐷)↑2) gcd 𝑀) = 1))
14848, 5, 146, 147syl3anc 1238 . . . . . . 7 (𝜑 → (((𝐶 gcd 𝐷) gcd 𝑀) = 1 → (((𝐶 gcd 𝐷)↑2) gcd 𝑀) = 1))
149144, 148mpd 13 . . . . . 6 (𝜑 → (((𝐶 gcd 𝐷)↑2) gcd 𝑀) = 1)
15098, 149eqtrd 2208 . . . . 5 (𝜑 → (𝑀 gcd ((𝐶 gcd 𝐷)↑2)) = 1)
15163, 72nn0addcld 9206 . . . . . . 7 (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℕ0)
152151nn0zd 9346 . . . . . 6 (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℤ)
153 coprmdvds 12059 . . . . . 6 ((𝑀 ∈ ℤ ∧ ((𝐶 gcd 𝐷)↑2) ∈ ℤ ∧ ((𝐸↑2) + (𝐹↑2)) ∈ ℤ) → ((𝑀 ∥ (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2))) ∧ (𝑀 gcd ((𝐶 gcd 𝐷)↑2)) = 1) → 𝑀 ∥ ((𝐸↑2) + (𝐹↑2))))
1548, 97, 152, 153syl3anc 1238 . . . . 5 (𝜑 → ((𝑀 ∥ (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2))) ∧ (𝑀 gcd ((𝐶 gcd 𝐷)↑2)) = 1) → 𝑀 ∥ ((𝐸↑2) + (𝐹↑2))))
15595, 150, 154mp2and 433 . . . 4 (𝜑𝑀 ∥ ((𝐸↑2) + (𝐹↑2)))
156 dvdsval2 11765 . . . . 5 ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ ((𝐸↑2) + (𝐹↑2)) ∈ ℤ) → (𝑀 ∥ ((𝐸↑2) + (𝐹↑2)) ↔ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ))
1578, 108, 152, 156syl3anc 1238 . . . 4 (𝜑 → (𝑀 ∥ ((𝐸↑2) + (𝐹↑2)) ↔ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ))
158155, 157mpbid 147 . . 3 (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ)
15963nn0red 9203 . . . . 5 (𝜑 → (𝐸↑2) ∈ ℝ)
16072nn0red 9203 . . . . 5 (𝜑 → (𝐹↑2) ∈ ℝ)
161159, 160readdcld 7961 . . . 4 (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℝ)
1625nnred 8905 . . . 4 (𝜑𝑀 ∈ ℝ)
1631, 452sqlem7 14028 . . . . . . 7 𝑌 ⊆ (𝑆 ∩ ℕ)
164 inss2 3354 . . . . . . 7 (𝑆 ∩ ℕ) ⊆ ℕ
165163, 164sstri 3162 . . . . . 6 𝑌 ⊆ ℕ
16661, 70gcdcld 11936 . . . . . . . . . 10 (𝜑 → (𝐸 gcd 𝐹) ∈ ℕ0)
167166nn0cnd 9204 . . . . . . . . 9 (𝜑 → (𝐸 gcd 𝐹) ∈ ℂ)
168 1cnd 7948 . . . . . . . . 9 (𝜑 → 1 ∈ ℂ)
16975mulid1d 7949 . . . . . . . . . 10 (𝜑 → ((𝐶 gcd 𝐷) · 1) = (𝐶 gcd 𝐷))
17082, 90oveq12d 5883 . . . . . . . . . 10 (𝜑 → (((𝐶 gcd 𝐷) · 𝐸) gcd ((𝐶 gcd 𝐷) · 𝐹)) = (𝐶 gcd 𝐷))
17114, 20gcdcld 11936 . . . . . . . . . . 11 (𝜑 → (𝐶 gcd 𝐷) ∈ ℕ0)
172 mulgcd 11984 . . . . . . . . . . 11 (((𝐶 gcd 𝐷) ∈ ℕ0𝐸 ∈ ℤ ∧ 𝐹 ∈ ℤ) → (((𝐶 gcd 𝐷) · 𝐸) gcd ((𝐶 gcd 𝐷) · 𝐹)) = ((𝐶 gcd 𝐷) · (𝐸 gcd 𝐹)))
173171, 61, 70, 172syl3anc 1238 . . . . . . . . . 10 (𝜑 → (((𝐶 gcd 𝐷) · 𝐸) gcd ((𝐶 gcd 𝐷) · 𝐹)) = ((𝐶 gcd 𝐷) · (𝐸 gcd 𝐹)))
174169, 170, 1733eqtr2rd 2215 . . . . . . . . 9 (𝜑 → ((𝐶 gcd 𝐷) · (𝐸 gcd 𝐹)) = ((𝐶 gcd 𝐷) · 1))
175167, 168, 75, 80, 174mulcanapad 8593 . . . . . . . 8 (𝜑 → (𝐸 gcd 𝐹) = 1)
176 eqidd 2176 . . . . . . . 8 (𝜑 → ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝐹↑2)))
177 oveq1 5872 . . . . . . . . . . 11 (𝑥 = 𝐸 → (𝑥 gcd 𝑦) = (𝐸 gcd 𝑦))
178177eqeq1d 2184 . . . . . . . . . 10 (𝑥 = 𝐸 → ((𝑥 gcd 𝑦) = 1 ↔ (𝐸 gcd 𝑦) = 1))
179 oveq1 5872 . . . . . . . . . . . 12 (𝑥 = 𝐸 → (𝑥↑2) = (𝐸↑2))
180179oveq1d 5880 . . . . . . . . . . 11 (𝑥 = 𝐸 → ((𝑥↑2) + (𝑦↑2)) = ((𝐸↑2) + (𝑦↑2)))
181180eqeq2d 2187 . . . . . . . . . 10 (𝑥 = 𝐸 → (((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2)) ↔ ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝑦↑2))))
182178, 181anbi12d 473 . . . . . . . . 9 (𝑥 = 𝐸 → (((𝑥 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2))) ↔ ((𝐸 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝑦↑2)))))
183 oveq2 5873 . . . . . . . . . . 11 (𝑦 = 𝐹 → (𝐸 gcd 𝑦) = (𝐸 gcd 𝐹))
184183eqeq1d 2184 . . . . . . . . . 10 (𝑦 = 𝐹 → ((𝐸 gcd 𝑦) = 1 ↔ (𝐸 gcd 𝐹) = 1))
185 oveq1 5872 . . . . . . . . . . . 12 (𝑦 = 𝐹 → (𝑦↑2) = (𝐹↑2))
186185oveq2d 5881 . . . . . . . . . . 11 (𝑦 = 𝐹 → ((𝐸↑2) + (𝑦↑2)) = ((𝐸↑2) + (𝐹↑2)))
187186eqeq2d 2187 . . . . . . . . . 10 (𝑦 = 𝐹 → (((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝑦↑2)) ↔ ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝐹↑2))))
188184, 187anbi12d 473 . . . . . . . . 9 (𝑦 = 𝐹 → (((𝐸 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝑦↑2))) ↔ ((𝐸 gcd 𝐹) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝐹↑2)))))
189182, 188rspc2ev 2854 . . . . . . . 8 ((𝐸 ∈ ℤ ∧ 𝐹 ∈ ℤ ∧ ((𝐸 gcd 𝐹) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝐹↑2)))) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2))))
19061, 70, 175, 176, 189syl112anc 1242 . . . . . . 7 (𝜑 → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2))))
191 eqeq1 2182 . . . . . . . . . . 11 (𝑧 = ((𝐸↑2) + (𝐹↑2)) → (𝑧 = ((𝑥↑2) + (𝑦↑2)) ↔ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2))))
192191anbi2d 464 . . . . . . . . . 10 (𝑧 = ((𝐸↑2) + (𝐹↑2)) → (((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2))) ↔ ((𝑥 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2)))))
1931922rexbidv 2500 . . . . . . . . 9 (𝑧 = ((𝐸↑2) + (𝐹↑2)) → (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2))) ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2)))))
194193, 45elab2g 2882 . . . . . . . 8 (((𝐸↑2) + (𝐹↑2)) ∈ ℕ0 → (((𝐸↑2) + (𝐹↑2)) ∈ 𝑌 ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2)))))
195151, 194syl 14 . . . . . . 7 (𝜑 → (((𝐸↑2) + (𝐹↑2)) ∈ 𝑌 ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2)))))
196190, 195mpbird 167 . . . . . 6 (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ 𝑌)
197165, 196sselid 3151 . . . . 5 (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℕ)
198197nngt0d 8936 . . . 4 (𝜑 → 0 < ((𝐸↑2) + (𝐹↑2)))
1995nngt0d 8936 . . . 4 (𝜑 → 0 < 𝑀)
200161, 162, 198, 199divgt0d 8865 . . 3 (𝜑 → 0 < (((𝐸↑2) + (𝐹↑2)) / 𝑀))
201 elnnz 9236 . . 3 ((((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℕ ↔ ((((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ ∧ 0 < (((𝐸↑2) + (𝐹↑2)) / 𝑀)))
202158, 200, 201sylanbrc 417 . 2 (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℕ)
203 prmnn 12077 . . . . . . . 8 (𝑝 ∈ ℙ → 𝑝 ∈ ℕ)
204203ad2antrl 490 . . . . . . 7 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∈ ℕ)
205204nnred 8905 . . . . . . . 8 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∈ ℝ)
206158adantr 276 . . . . . . . . 9 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ)
207206zred 9348 . . . . . . . 8 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℝ)
208 peano2zm 9264 . . . . . . . . . . 11 (𝑀 ∈ ℤ → (𝑀 − 1) ∈ ℤ)
2098, 208syl 14 . . . . . . . . . 10 (𝜑 → (𝑀 − 1) ∈ ℤ)
210209zred 9348 . . . . . . . . 9 (𝜑 → (𝑀 − 1) ∈ ℝ)
211210adantr 276 . . . . . . . 8 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (𝑀 − 1) ∈ ℝ)
212 simprr 531 . . . . . . . . 9 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))
213 prmz 12078 . . . . . . . . . . 11 (𝑝 ∈ ℙ → 𝑝 ∈ ℤ)
214213ad2antrl 490 . . . . . . . . . 10 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∈ ℤ)
215202adantr 276 . . . . . . . . . 10 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℕ)
216 dvdsle 11817 . . . . . . . . . 10 ((𝑝 ∈ ℤ ∧ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℕ) → (𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀) → 𝑝 ≤ (((𝐸↑2) + (𝐹↑2)) / 𝑀)))
217214, 215, 216syl2anc 411 . . . . . . . . 9 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀) → 𝑝 ≤ (((𝐸↑2) + (𝐹↑2)) / 𝑀)))
218212, 217mpd 13 . . . . . . . 8 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ≤ (((𝐸↑2) + (𝐹↑2)) / 𝑀))
219 zsqcl 10560 . . . . . . . . . . . . . . . 16 (𝑀 ∈ ℤ → (𝑀↑2) ∈ ℤ)
2208, 219syl 14 . . . . . . . . . . . . . . 15 (𝜑 → (𝑀↑2) ∈ ℤ)
221220zred 9348 . . . . . . . . . . . . . 14 (𝜑 → (𝑀↑2) ∈ ℝ)
222221rehalfcld 9138 . . . . . . . . . . . . 13 (𝜑 → ((𝑀↑2) / 2) ∈ ℝ)
22316zred 9348 . . . . . . . . . . . . . . 15 (𝜑 → (𝐶↑2) ∈ ℝ)
22422zred 9348 . . . . . . . . . . . . . . 15 (𝜑 → (𝐷↑2) ∈ ℝ)
225223, 224readdcld 7961 . . . . . . . . . . . . . 14 (𝜑 → ((𝐶↑2) + (𝐷↑2)) ∈ ℝ)
226 1red 7947 . . . . . . . . . . . . . . . 16 (𝜑 → 1 ∈ ℝ)
22748nnsqcld 10644 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐶 gcd 𝐷)↑2) ∈ ℕ)
228227nnred 8905 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐶 gcd 𝐷)↑2) ∈ ℝ)
229151nn0ge0d 9205 . . . . . . . . . . . . . . . 16 (𝜑 → 0 ≤ ((𝐸↑2) + (𝐹↑2)))
230227nnge1d 8935 . . . . . . . . . . . . . . . 16 (𝜑 → 1 ≤ ((𝐶 gcd 𝐷)↑2))
231226, 228, 161, 229, 230lemul1ad 8869 . . . . . . . . . . . . . . 15 (𝜑 → (1 · ((𝐸↑2) + (𝐹↑2))) ≤ (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2))))
232151nn0cnd 9204 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℂ)
233232mulid2d 7950 . . . . . . . . . . . . . . 15 (𝜑 → (1 · ((𝐸↑2) + (𝐹↑2))) = ((𝐸↑2) + (𝐹↑2)))
234231, 233, 943brtr3d 4029 . . . . . . . . . . . . . 14 (𝜑 → ((𝐸↑2) + (𝐹↑2)) ≤ ((𝐶↑2) + (𝐷↑2)))
235222rehalfcld 9138 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝑀↑2) / 2) / 2) ∈ ℝ)
23611, 5, 124sqlem7 12349 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐶↑2) ≤ (((𝑀↑2) / 2) / 2))
23717, 5, 184sqlem7 12349 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐷↑2) ≤ (((𝑀↑2) / 2) / 2))
238223, 224, 235, 235, 236, 237le2addd 8494 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐶↑2) + (𝐷↑2)) ≤ ((((𝑀↑2) / 2) / 2) + (((𝑀↑2) / 2) / 2)))
239222recnd 7960 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑀↑2) / 2) ∈ ℂ)
2402392halvesd 9137 . . . . . . . . . . . . . . 15 (𝜑 → ((((𝑀↑2) / 2) / 2) + (((𝑀↑2) / 2) / 2)) = ((𝑀↑2) / 2))
241238, 240breqtrd 4024 . . . . . . . . . . . . . 14 (𝜑 → ((𝐶↑2) + (𝐷↑2)) ≤ ((𝑀↑2) / 2))
242161, 225, 222, 234, 241letrd 8055 . . . . . . . . . . . . 13 (𝜑 → ((𝐸↑2) + (𝐹↑2)) ≤ ((𝑀↑2) / 2))
2435nnsqcld 10644 . . . . . . . . . . . . . . 15 (𝜑 → (𝑀↑2) ∈ ℕ)
244243nnrpd 9665 . . . . . . . . . . . . . 14 (𝜑 → (𝑀↑2) ∈ ℝ+)
245 rphalflt 9654 . . . . . . . . . . . . . 14 ((𝑀↑2) ∈ ℝ+ → ((𝑀↑2) / 2) < (𝑀↑2))
246244, 245syl 14 . . . . . . . . . . . . 13 (𝜑 → ((𝑀↑2) / 2) < (𝑀↑2))
247161, 222, 221, 242, 246lelttrd 8056 . . . . . . . . . . . 12 (𝜑 → ((𝐸↑2) + (𝐹↑2)) < (𝑀↑2))
2488zcnd 9349 . . . . . . . . . . . . 13 (𝜑𝑀 ∈ ℂ)
249248sqvald 10620 . . . . . . . . . . . 12 (𝜑 → (𝑀↑2) = (𝑀 · 𝑀))
250247, 249breqtrd 4024 . . . . . . . . . . 11 (𝜑 → ((𝐸↑2) + (𝐹↑2)) < (𝑀 · 𝑀))
251 ltdivmul 8806 . . . . . . . . . . . 12 ((((𝐸↑2) + (𝐹↑2)) ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (𝑀 ∈ ℝ ∧ 0 < 𝑀)) → ((((𝐸↑2) + (𝐹↑2)) / 𝑀) < 𝑀 ↔ ((𝐸↑2) + (𝐹↑2)) < (𝑀 · 𝑀)))
252161, 162, 162, 199, 251syl112anc 1242 . . . . . . . . . . 11 (𝜑 → ((((𝐸↑2) + (𝐹↑2)) / 𝑀) < 𝑀 ↔ ((𝐸↑2) + (𝐹↑2)) < (𝑀 · 𝑀)))
253250, 252mpbird 167 . . . . . . . . . 10 (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) < 𝑀)
254 zltlem1 9283 . . . . . . . . . . 11 (((((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((((𝐸↑2) + (𝐹↑2)) / 𝑀) < 𝑀 ↔ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ≤ (𝑀 − 1)))
255158, 8, 254syl2anc 411 . . . . . . . . . 10 (𝜑 → ((((𝐸↑2) + (𝐹↑2)) / 𝑀) < 𝑀 ↔ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ≤ (𝑀 − 1)))
256253, 255mpbid 147 . . . . . . . . 9 (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ≤ (𝑀 − 1))
257256adantr 276 . . . . . . . 8 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ≤ (𝑀 − 1))
258205, 207, 211, 218, 257letrd 8055 . . . . . . 7 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ≤ (𝑀 − 1))
259209adantr 276 . . . . . . . 8 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (𝑀 − 1) ∈ ℤ)
260 fznn 10059 . . . . . . . 8 ((𝑀 − 1) ∈ ℤ → (𝑝 ∈ (1...(𝑀 − 1)) ↔ (𝑝 ∈ ℕ ∧ 𝑝 ≤ (𝑀 − 1))))
261259, 260syl 14 . . . . . . 7 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (𝑝 ∈ (1...(𝑀 − 1)) ↔ (𝑝 ∈ ℕ ∧ 𝑝 ≤ (𝑀 − 1))))
262204, 258, 261mpbir2and 944 . . . . . 6 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∈ (1...(𝑀 − 1)))
263196adantr 276 . . . . . 6 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → ((𝐸↑2) + (𝐹↑2)) ∈ 𝑌)
264262, 263jca 306 . . . . 5 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (𝑝 ∈ (1...(𝑀 − 1)) ∧ ((𝐸↑2) + (𝐹↑2)) ∈ 𝑌))
26546adantr 276 . . . . 5 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → ∀𝑏 ∈ (1...(𝑀 − 1))∀𝑎𝑌 (𝑏𝑎𝑏𝑆))
266152adantr 276 . . . . . 6 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → ((𝐸↑2) + (𝐹↑2)) ∈ ℤ)
267 dvdsmul2 11789 . . . . . . . . 9 ((𝑀 ∈ ℤ ∧ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∥ (𝑀 · (((𝐸↑2) + (𝐹↑2)) / 𝑀)))
2688, 158, 267syl2anc 411 . . . . . . . 8 (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∥ (𝑀 · (((𝐸↑2) + (𝐹↑2)) / 𝑀)))
2695nnap0d 8938 . . . . . . . . 9 (𝜑𝑀 # 0)
270232, 248, 269divcanap2d 8722 . . . . . . . 8 (𝜑 → (𝑀 · (((𝐸↑2) + (𝐹↑2)) / 𝑀)) = ((𝐸↑2) + (𝐹↑2)))
271268, 270breqtrd 4024 . . . . . . 7 (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∥ ((𝐸↑2) + (𝐹↑2)))
272271adantr 276 . . . . . 6 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∥ ((𝐸↑2) + (𝐹↑2)))
273214, 206, 266, 212, 272dvdstrd 11805 . . . . 5 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∥ ((𝐸↑2) + (𝐹↑2)))
274 breq1 4001 . . . . . . 7 (𝑏 = 𝑝 → (𝑏𝑎𝑝𝑎))
275 eleq1w 2236 . . . . . . 7 (𝑏 = 𝑝 → (𝑏𝑆𝑝𝑆))
276274, 275imbi12d 234 . . . . . 6 (𝑏 = 𝑝 → ((𝑏𝑎𝑏𝑆) ↔ (𝑝𝑎𝑝𝑆)))
277 breq2 4002 . . . . . . 7 (𝑎 = ((𝐸↑2) + (𝐹↑2)) → (𝑝𝑎𝑝 ∥ ((𝐸↑2) + (𝐹↑2))))
278277imbi1d 231 . . . . . 6 (𝑎 = ((𝐸↑2) + (𝐹↑2)) → ((𝑝𝑎𝑝𝑆) ↔ (𝑝 ∥ ((𝐸↑2) + (𝐹↑2)) → 𝑝𝑆)))
279276, 278rspc2v 2852 . . . . 5 ((𝑝 ∈ (1...(𝑀 − 1)) ∧ ((𝐸↑2) + (𝐹↑2)) ∈ 𝑌) → (∀𝑏 ∈ (1...(𝑀 − 1))∀𝑎𝑌 (𝑏𝑎𝑏𝑆) → (𝑝 ∥ ((𝐸↑2) + (𝐹↑2)) → 𝑝𝑆)))
280264, 265, 273, 279syl3c 63 . . . 4 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝𝑆)
281280expr 375 . . 3 ((𝜑𝑝 ∈ ℙ) → (𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀) → 𝑝𝑆))
282281ralrimiva 2548 . 2 (𝜑 → ∀𝑝 ∈ ℙ (𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀) → 𝑝𝑆))
283 inss1 3353 . . . . 5 (𝑆 ∩ ℕ) ⊆ 𝑆
284163, 283sstri 3162 . . . 4 𝑌𝑆
285284, 196sselid 3151 . . 3 (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ 𝑆)
286270, 285eqeltrd 2252 . 2 (𝜑 → (𝑀 · (((𝐸↑2) + (𝐹↑2)) / 𝑀)) ∈ 𝑆)
2871, 5, 202, 282, 2862sqlem6 14027 1 (𝜑𝑀𝑆)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wb 105   = wceq 1353  wcel 2146  {cab 2161  wne 2345  wral 2453  wrex 2454  cin 3126   class class class wbr 3998  cmpt 4059  ran crn 4621  cfv 5208  (class class class)co 5865  cr 7785  0cc0 7786  1c1 7787   + caddc 7789   · cmul 7791   < clt 7966  cle 7967  cmin 8102   / cdiv 8602  cn 8892  2c2 8943  0cn0 9149  cz 9226  cuz 9501  +crp 9624  ...cfz 9979   mod cmo 10292  cexp 10489  abscabs 10974  cdvds 11762   gcd cgcd 11910  cprime 12074  ℤ[i]cgz 12334
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-13 2148  ax-14 2149  ax-ext 2157  ax-coll 4113  ax-sep 4116  ax-nul 4124  ax-pow 4169  ax-pr 4203  ax-un 4427  ax-setind 4530  ax-iinf 4581  ax-cnex 7877  ax-resscn 7878  ax-1cn 7879  ax-1re 7880  ax-icn 7881  ax-addcl 7882  ax-addrcl 7883  ax-mulcl 7884  ax-mulrcl 7885  ax-addcom 7886  ax-mulcom 7887  ax-addass 7888  ax-mulass 7889  ax-distr 7890  ax-i2m1 7891  ax-0lt1 7892  ax-1rid 7893  ax-0id 7894  ax-rnegex 7895  ax-precex 7896  ax-cnre 7897  ax-pre-ltirr 7898  ax-pre-ltwlin 7899  ax-pre-lttrn 7900  ax-pre-apti 7901  ax-pre-ltadd 7902  ax-pre-mulgt0 7903  ax-pre-mulext 7904  ax-arch 7905  ax-caucvg 7906
This theorem depends on definitions:  df-bi 117  df-stab 831  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1459  df-sb 1761  df-eu 2027  df-mo 2028  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-ne 2346  df-nel 2441  df-ral 2458  df-rex 2459  df-reu 2460  df-rmo 2461  df-rab 2462  df-v 2737  df-sbc 2961  df-csb 3056  df-dif 3129  df-un 3131  df-in 3133  df-ss 3140  df-nul 3421  df-if 3533  df-pw 3574  df-sn 3595  df-pr 3596  df-op 3598  df-uni 3806  df-int 3841  df-iun 3884  df-br 3999  df-opab 4060  df-mpt 4061  df-tr 4097  df-id 4287  df-po 4290  df-iso 4291  df-iord 4360  df-on 4362  df-ilim 4363  df-suc 4365  df-iom 4584  df-xp 4626  df-rel 4627  df-cnv 4628  df-co 4629  df-dm 4630  df-rn 4631  df-res 4632  df-ima 4633  df-iota 5170  df-fun 5210  df-fn 5211  df-f 5212  df-f1 5213  df-fo 5214  df-f1o 5215  df-fv 5216  df-riota 5821  df-ov 5868  df-oprab 5869  df-mpo 5870  df-1st 6131  df-2nd 6132  df-recs 6296  df-frec 6382  df-1o 6407  df-2o 6408  df-er 6525  df-en 6731  df-sup 6973  df-pnf 7968  df-mnf 7969  df-xr 7970  df-ltxr 7971  df-le 7972  df-sub 8104  df-neg 8105  df-reap 8506  df-ap 8513  df-div 8603  df-inn 8893  df-2 8951  df-3 8952  df-4 8953  df-n0 9150  df-z 9227  df-uz 9502  df-q 9593  df-rp 9625  df-fz 9980  df-fzo 10113  df-fl 10240  df-mod 10293  df-seqfrec 10416  df-exp 10490  df-cj 10819  df-re 10820  df-im 10821  df-rsqrt 10975  df-abs 10976  df-dvds 11763  df-gcd 11911  df-prm 12075  df-gz 12335
This theorem is referenced by:  2sqlem9  14031
  Copyright terms: Public domain W3C validator