MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2sqlem8 Structured version   Visualization version   GIF version

Theorem 2sqlem8 25929
Description: Lemma for 2sq 25933. (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 12310 . . . 4 (𝑀 ∈ (ℤ‘2) ↔ (𝑀 ∈ ℕ ∧ 𝑀 ≠ 1))
42, 3sylib 219 . . 3 (𝜑 → (𝑀 ∈ ℕ ∧ 𝑀 ≠ 1))
54simpld 495 . 2 (𝜑𝑀 ∈ ℕ)
6 2sqlem9.7 . . . . . . 7 (𝜑𝑀𝑁)
7 eluzelz 12241 . . . . . . . . 9 (𝑀 ∈ (ℤ‘2) → 𝑀 ∈ ℤ)
82, 7syl 17 . . . . . . . 8 (𝜑𝑀 ∈ ℤ)
9 2sqlem8.n . . . . . . . . 9 (𝜑𝑁 ∈ ℕ)
109nnzd 12074 . . . . . . . 8 (𝜑𝑁 ∈ ℤ)
11 2sqlem8.1 . . . . . . . . . . . 12 (𝜑𝐴 ∈ ℤ)
12 2sqlem8.c . . . . . . . . . . . 12 𝐶 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))
1311, 5, 124sqlem5 16266 . . . . . . . . . . 11 (𝜑 → (𝐶 ∈ ℤ ∧ ((𝐴𝐶) / 𝑀) ∈ ℤ))
1413simpld 495 . . . . . . . . . 10 (𝜑𝐶 ∈ ℤ)
15 zsqcl 13482 . . . . . . . . . 10 (𝐶 ∈ ℤ → (𝐶↑2) ∈ ℤ)
1614, 15syl 17 . . . . . . . . 9 (𝜑 → (𝐶↑2) ∈ ℤ)
17 2sqlem8.2 . . . . . . . . . . . 12 (𝜑𝐵 ∈ ℤ)
18 2sqlem8.d . . . . . . . . . . . 12 𝐷 = (((𝐵 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))
1917, 5, 184sqlem5 16266 . . . . . . . . . . 11 (𝜑 → (𝐷 ∈ ℤ ∧ ((𝐵𝐷) / 𝑀) ∈ ℤ))
2019simpld 495 . . . . . . . . . 10 (𝜑𝐷 ∈ ℤ)
21 zsqcl 13482 . . . . . . . . . 10 (𝐷 ∈ ℤ → (𝐷↑2) ∈ ℤ)
2220, 21syl 17 . . . . . . . . 9 (𝜑 → (𝐷↑2) ∈ ℤ)
2316, 22zaddcld 12079 . . . . . . . 8 (𝜑 → ((𝐶↑2) + (𝐷↑2)) ∈ ℤ)
2411, 5, 124sqlem8 16269 . . . . . . . . . 10 (𝜑𝑀 ∥ ((𝐴↑2) − (𝐶↑2)))
2517, 5, 184sqlem8 16269 . . . . . . . . . 10 (𝜑𝑀 ∥ ((𝐵↑2) − (𝐷↑2)))
26 zsqcl 13482 . . . . . . . . . . . . 13 (𝐴 ∈ ℤ → (𝐴↑2) ∈ ℤ)
2711, 26syl 17 . . . . . . . . . . . 12 (𝜑 → (𝐴↑2) ∈ ℤ)
2827, 16zsubcld 12080 . . . . . . . . . . 11 (𝜑 → ((𝐴↑2) − (𝐶↑2)) ∈ ℤ)
29 zsqcl 13482 . . . . . . . . . . . . 13 (𝐵 ∈ ℤ → (𝐵↑2) ∈ ℤ)
3017, 29syl 17 . . . . . . . . . . . 12 (𝜑 → (𝐵↑2) ∈ ℤ)
3130, 22zsubcld 12080 . . . . . . . . . . 11 (𝜑 → ((𝐵↑2) − (𝐷↑2)) ∈ ℤ)
32 dvds2add 15631 . . . . . . . . . . 11 ((𝑀 ∈ ℤ ∧ ((𝐴↑2) − (𝐶↑2)) ∈ ℤ ∧ ((𝐵↑2) − (𝐷↑2)) ∈ ℤ) → ((𝑀 ∥ ((𝐴↑2) − (𝐶↑2)) ∧ 𝑀 ∥ ((𝐵↑2) − (𝐷↑2))) → 𝑀 ∥ (((𝐴↑2) − (𝐶↑2)) + ((𝐵↑2) − (𝐷↑2)))))
338, 28, 31, 32syl3anc 1363 . . . . . . . . . 10 (𝜑 → ((𝑀 ∥ ((𝐴↑2) − (𝐶↑2)) ∧ 𝑀 ∥ ((𝐵↑2) − (𝐷↑2))) → 𝑀 ∥ (((𝐴↑2) − (𝐶↑2)) + ((𝐵↑2) − (𝐷↑2)))))
3424, 25, 33mp2and 695 . . . . . . . . 9 (𝜑𝑀 ∥ (((𝐴↑2) − (𝐶↑2)) + ((𝐵↑2) − (𝐷↑2))))
35 2sqlem8.4 . . . . . . . . . . 11 (𝜑𝑁 = ((𝐴↑2) + (𝐵↑2)))
3635oveq1d 7160 . . . . . . . . . 10 (𝜑 → (𝑁 − ((𝐶↑2) + (𝐷↑2))) = (((𝐴↑2) + (𝐵↑2)) − ((𝐶↑2) + (𝐷↑2))))
3727zcnd 12076 . . . . . . . . . . 11 (𝜑 → (𝐴↑2) ∈ ℂ)
3830zcnd 12076 . . . . . . . . . . 11 (𝜑 → (𝐵↑2) ∈ ℂ)
3916zcnd 12076 . . . . . . . . . . 11 (𝜑 → (𝐶↑2) ∈ ℂ)
4022zcnd 12076 . . . . . . . . . . 11 (𝜑 → (𝐷↑2) ∈ ℂ)
4137, 38, 39, 40addsub4d 11032 . . . . . . . . . 10 (𝜑 → (((𝐴↑2) + (𝐵↑2)) − ((𝐶↑2) + (𝐷↑2))) = (((𝐴↑2) − (𝐶↑2)) + ((𝐵↑2) − (𝐷↑2))))
4236, 41eqtrd 2853 . . . . . . . . 9 (𝜑 → (𝑁 − ((𝐶↑2) + (𝐷↑2))) = (((𝐴↑2) − (𝐶↑2)) + ((𝐵↑2) − (𝐷↑2))))
4334, 42breqtrrd 5085 . . . . . . . 8 (𝜑𝑀 ∥ (𝑁 − ((𝐶↑2) + (𝐷↑2))))
44 dvdssub2 15639 . . . . . . . 8 (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ((𝐶↑2) + (𝐷↑2)) ∈ ℤ) ∧ 𝑀 ∥ (𝑁 − ((𝐶↑2) + (𝐷↑2)))) → (𝑀𝑁𝑀 ∥ ((𝐶↑2) + (𝐷↑2))))
458, 10, 23, 43, 44syl31anc 1365 . . . . . . 7 (𝜑 → (𝑀𝑁𝑀 ∥ ((𝐶↑2) + (𝐷↑2))))
466, 45mpbid 233 . . . . . 6 (𝜑𝑀 ∥ ((𝐶↑2) + (𝐷↑2)))
47 2sqlem7.2 . . . . . . . . . . . 12 𝑌 = {𝑧 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2)))}
48 2sqlem9.5 . . . . . . . . . . . 12 (𝜑 → ∀𝑏 ∈ (1...(𝑀 − 1))∀𝑎𝑌 (𝑏𝑎𝑏𝑆))
49 2sqlem8.3 . . . . . . . . . . . 12 (𝜑 → (𝐴 gcd 𝐵) = 1)
501, 47, 48, 6, 9, 2, 11, 17, 49, 35, 12, 182sqlem8a 25928 . . . . . . . . . . 11 (𝜑 → (𝐶 gcd 𝐷) ∈ ℕ)
5150nnzd 12074 . . . . . . . . . 10 (𝜑 → (𝐶 gcd 𝐷) ∈ ℤ)
52 zsqcl2 13490 . . . . . . . . . 10 ((𝐶 gcd 𝐷) ∈ ℤ → ((𝐶 gcd 𝐷)↑2) ∈ ℕ0)
5351, 52syl 17 . . . . . . . . 9 (𝜑 → ((𝐶 gcd 𝐷)↑2) ∈ ℕ0)
5453nn0cnd 11945 . . . . . . . 8 (𝜑 → ((𝐶 gcd 𝐷)↑2) ∈ ℂ)
55 2sqlem8.e . . . . . . . . . . 11 𝐸 = (𝐶 / (𝐶 gcd 𝐷))
56 gcddvds 15840 . . . . . . . . . . . . . 14 ((𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ) → ((𝐶 gcd 𝐷) ∥ 𝐶 ∧ (𝐶 gcd 𝐷) ∥ 𝐷))
5714, 20, 56syl2anc 584 . . . . . . . . . . . . 13 (𝜑 → ((𝐶 gcd 𝐷) ∥ 𝐶 ∧ (𝐶 gcd 𝐷) ∥ 𝐷))
5857simpld 495 . . . . . . . . . . . 12 (𝜑 → (𝐶 gcd 𝐷) ∥ 𝐶)
5950nnne0d 11675 . . . . . . . . . . . . 13 (𝜑 → (𝐶 gcd 𝐷) ≠ 0)
60 dvdsval2 15598 . . . . . . . . . . . . 13 (((𝐶 gcd 𝐷) ∈ ℤ ∧ (𝐶 gcd 𝐷) ≠ 0 ∧ 𝐶 ∈ ℤ) → ((𝐶 gcd 𝐷) ∥ 𝐶 ↔ (𝐶 / (𝐶 gcd 𝐷)) ∈ ℤ))
6151, 59, 14, 60syl3anc 1363 . . . . . . . . . . . 12 (𝜑 → ((𝐶 gcd 𝐷) ∥ 𝐶 ↔ (𝐶 / (𝐶 gcd 𝐷)) ∈ ℤ))
6258, 61mpbid 233 . . . . . . . . . . 11 (𝜑 → (𝐶 / (𝐶 gcd 𝐷)) ∈ ℤ)
6355, 62eqeltrid 2914 . . . . . . . . . 10 (𝜑𝐸 ∈ ℤ)
64 zsqcl2 13490 . . . . . . . . . 10 (𝐸 ∈ ℤ → (𝐸↑2) ∈ ℕ0)
6563, 64syl 17 . . . . . . . . 9 (𝜑 → (𝐸↑2) ∈ ℕ0)
6665nn0cnd 11945 . . . . . . . 8 (𝜑 → (𝐸↑2) ∈ ℂ)
67 2sqlem8.f . . . . . . . . . . 11 𝐹 = (𝐷 / (𝐶 gcd 𝐷))
6857simprd 496 . . . . . . . . . . . 12 (𝜑 → (𝐶 gcd 𝐷) ∥ 𝐷)
69 dvdsval2 15598 . . . . . . . . . . . . 13 (((𝐶 gcd 𝐷) ∈ ℤ ∧ (𝐶 gcd 𝐷) ≠ 0 ∧ 𝐷 ∈ ℤ) → ((𝐶 gcd 𝐷) ∥ 𝐷 ↔ (𝐷 / (𝐶 gcd 𝐷)) ∈ ℤ))
7051, 59, 20, 69syl3anc 1363 . . . . . . . . . . . 12 (𝜑 → ((𝐶 gcd 𝐷) ∥ 𝐷 ↔ (𝐷 / (𝐶 gcd 𝐷)) ∈ ℤ))
7168, 70mpbid 233 . . . . . . . . . . 11 (𝜑 → (𝐷 / (𝐶 gcd 𝐷)) ∈ ℤ)
7267, 71eqeltrid 2914 . . . . . . . . . 10 (𝜑𝐹 ∈ ℤ)
73 zsqcl2 13490 . . . . . . . . . 10 (𝐹 ∈ ℤ → (𝐹↑2) ∈ ℕ0)
7472, 73syl 17 . . . . . . . . 9 (𝜑 → (𝐹↑2) ∈ ℕ0)
7574nn0cnd 11945 . . . . . . . 8 (𝜑 → (𝐹↑2) ∈ ℂ)
7654, 66, 75adddid 10653 . . . . . . 7 (𝜑 → (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2))) = ((((𝐶 gcd 𝐷)↑2) · (𝐸↑2)) + (((𝐶 gcd 𝐷)↑2) · (𝐹↑2))))
7751zcnd 12076 . . . . . . . . . 10 (𝜑 → (𝐶 gcd 𝐷) ∈ ℂ)
7863zcnd 12076 . . . . . . . . . 10 (𝜑𝐸 ∈ ℂ)
7977, 78sqmuld 13510 . . . . . . . . 9 (𝜑 → (((𝐶 gcd 𝐷) · 𝐸)↑2) = (((𝐶 gcd 𝐷)↑2) · (𝐸↑2)))
8055oveq2i 7156 . . . . . . . . . . 11 ((𝐶 gcd 𝐷) · 𝐸) = ((𝐶 gcd 𝐷) · (𝐶 / (𝐶 gcd 𝐷)))
8114zcnd 12076 . . . . . . . . . . . 12 (𝜑𝐶 ∈ ℂ)
8281, 77, 59divcan2d 11406 . . . . . . . . . . 11 (𝜑 → ((𝐶 gcd 𝐷) · (𝐶 / (𝐶 gcd 𝐷))) = 𝐶)
8380, 82syl5eq 2865 . . . . . . . . . 10 (𝜑 → ((𝐶 gcd 𝐷) · 𝐸) = 𝐶)
8483oveq1d 7160 . . . . . . . . 9 (𝜑 → (((𝐶 gcd 𝐷) · 𝐸)↑2) = (𝐶↑2))
8579, 84eqtr3d 2855 . . . . . . . 8 (𝜑 → (((𝐶 gcd 𝐷)↑2) · (𝐸↑2)) = (𝐶↑2))
8672zcnd 12076 . . . . . . . . . 10 (𝜑𝐹 ∈ ℂ)
8777, 86sqmuld 13510 . . . . . . . . 9 (𝜑 → (((𝐶 gcd 𝐷) · 𝐹)↑2) = (((𝐶 gcd 𝐷)↑2) · (𝐹↑2)))
8867oveq2i 7156 . . . . . . . . . . 11 ((𝐶 gcd 𝐷) · 𝐹) = ((𝐶 gcd 𝐷) · (𝐷 / (𝐶 gcd 𝐷)))
8920zcnd 12076 . . . . . . . . . . . 12 (𝜑𝐷 ∈ ℂ)
9089, 77, 59divcan2d 11406 . . . . . . . . . . 11 (𝜑 → ((𝐶 gcd 𝐷) · (𝐷 / (𝐶 gcd 𝐷))) = 𝐷)
9188, 90syl5eq 2865 . . . . . . . . . 10 (𝜑 → ((𝐶 gcd 𝐷) · 𝐹) = 𝐷)
9291oveq1d 7160 . . . . . . . . 9 (𝜑 → (((𝐶 gcd 𝐷) · 𝐹)↑2) = (𝐷↑2))
9387, 92eqtr3d 2855 . . . . . . . 8 (𝜑 → (((𝐶 gcd 𝐷)↑2) · (𝐹↑2)) = (𝐷↑2))
9485, 93oveq12d 7163 . . . . . . 7 (𝜑 → ((((𝐶 gcd 𝐷)↑2) · (𝐸↑2)) + (((𝐶 gcd 𝐷)↑2) · (𝐹↑2))) = ((𝐶↑2) + (𝐷↑2)))
9576, 94eqtrd 2853 . . . . . 6 (𝜑 → (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2))) = ((𝐶↑2) + (𝐷↑2)))
9646, 95breqtrrd 5085 . . . . 5 (𝜑𝑀 ∥ (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2))))
97 zsqcl 13482 . . . . . . . 8 ((𝐶 gcd 𝐷) ∈ ℤ → ((𝐶 gcd 𝐷)↑2) ∈ ℤ)
9851, 97syl 17 . . . . . . 7 (𝜑 → ((𝐶 gcd 𝐷)↑2) ∈ ℤ)
99 gcdcom 15850 . . . . . . 7 ((𝑀 ∈ ℤ ∧ ((𝐶 gcd 𝐷)↑2) ∈ ℤ) → (𝑀 gcd ((𝐶 gcd 𝐷)↑2)) = (((𝐶 gcd 𝐷)↑2) gcd 𝑀))
1008, 98, 99syl2anc 584 . . . . . 6 (𝜑 → (𝑀 gcd ((𝐶 gcd 𝐷)↑2)) = (((𝐶 gcd 𝐷)↑2) gcd 𝑀))
101 gcddvds 15840 . . . . . . . . . . . . . 14 (((𝐶 gcd 𝐷) ∈ ℤ ∧ 𝑀 ∈ ℤ) → (((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐶 gcd 𝐷) ∧ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝑀))
10251, 8, 101syl2anc 584 . . . . . . . . . . . . 13 (𝜑 → (((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐶 gcd 𝐷) ∧ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝑀))
103102simpld 495 . . . . . . . . . . . 12 (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐶 gcd 𝐷))
10451, 8gcdcld 15845 . . . . . . . . . . . . . 14 (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℕ0)
105104nn0zd 12073 . . . . . . . . . . . . 13 (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℤ)
106 dvdstr 15634 . . . . . . . . . . . . 13 ((((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℤ ∧ (𝐶 gcd 𝐷) ∈ ℤ ∧ 𝐶 ∈ ℤ) → ((((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐶 gcd 𝐷) ∧ (𝐶 gcd 𝐷) ∥ 𝐶) → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐶))
107105, 51, 14, 106syl3anc 1363 . . . . . . . . . . . 12 (𝜑 → ((((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐶 gcd 𝐷) ∧ (𝐶 gcd 𝐷) ∥ 𝐶) → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐶))
108103, 58, 107mp2and 695 . . . . . . . . . . 11 (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐶)
109102simprd 496 . . . . . . . . . . . . 13 (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝑀)
11013simprd 496 . . . . . . . . . . . . . 14 (𝜑 → ((𝐴𝐶) / 𝑀) ∈ ℤ)
1115nnne0d 11675 . . . . . . . . . . . . . . 15 (𝜑𝑀 ≠ 0)
11211, 14zsubcld 12080 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴𝐶) ∈ ℤ)
113 dvdsval2 15598 . . . . . . . . . . . . . . 15 ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ (𝐴𝐶) ∈ ℤ) → (𝑀 ∥ (𝐴𝐶) ↔ ((𝐴𝐶) / 𝑀) ∈ ℤ))
1148, 111, 112, 113syl3anc 1363 . . . . . . . . . . . . . 14 (𝜑 → (𝑀 ∥ (𝐴𝐶) ↔ ((𝐴𝐶) / 𝑀) ∈ ℤ))
115110, 114mpbird 258 . . . . . . . . . . . . 13 (𝜑𝑀 ∥ (𝐴𝐶))
116 dvdstr 15634 . . . . . . . . . . . . . 14 ((((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (𝐴𝐶) ∈ ℤ) → ((((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝑀𝑀 ∥ (𝐴𝐶)) → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐴𝐶)))
117105, 8, 112, 116syl3anc 1363 . . . . . . . . . . . . 13 (𝜑 → ((((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝑀𝑀 ∥ (𝐴𝐶)) → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐴𝐶)))
118109, 115, 117mp2and 695 . . . . . . . . . . . 12 (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐴𝐶))
119 dvdssub2 15639 . . . . . . . . . . . 12 (((((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐴𝐶)) → (((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐴 ↔ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐶))
120105, 11, 14, 118, 119syl31anc 1365 . . . . . . . . . . 11 (𝜑 → (((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐴 ↔ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐶))
121108, 120mpbird 258 . . . . . . . . . 10 (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐴)
122 dvdstr 15634 . . . . . . . . . . . . 13 ((((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℤ ∧ (𝐶 gcd 𝐷) ∈ ℤ ∧ 𝐷 ∈ ℤ) → ((((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐶 gcd 𝐷) ∧ (𝐶 gcd 𝐷) ∥ 𝐷) → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐷))
123105, 51, 20, 122syl3anc 1363 . . . . . . . . . . . 12 (𝜑 → ((((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐶 gcd 𝐷) ∧ (𝐶 gcd 𝐷) ∥ 𝐷) → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐷))
124103, 68, 123mp2and 695 . . . . . . . . . . 11 (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐷)
12519simprd 496 . . . . . . . . . . . . . 14 (𝜑 → ((𝐵𝐷) / 𝑀) ∈ ℤ)
12617, 20zsubcld 12080 . . . . . . . . . . . . . . 15 (𝜑 → (𝐵𝐷) ∈ ℤ)
127 dvdsval2 15598 . . . . . . . . . . . . . . 15 ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ (𝐵𝐷) ∈ ℤ) → (𝑀 ∥ (𝐵𝐷) ↔ ((𝐵𝐷) / 𝑀) ∈ ℤ))
1288, 111, 126, 127syl3anc 1363 . . . . . . . . . . . . . 14 (𝜑 → (𝑀 ∥ (𝐵𝐷) ↔ ((𝐵𝐷) / 𝑀) ∈ ℤ))
129125, 128mpbird 258 . . . . . . . . . . . . 13 (𝜑𝑀 ∥ (𝐵𝐷))
130 dvdstr 15634 . . . . . . . . . . . . . 14 ((((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (𝐵𝐷) ∈ ℤ) → ((((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝑀𝑀 ∥ (𝐵𝐷)) → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐵𝐷)))
131105, 8, 126, 130syl3anc 1363 . . . . . . . . . . . . 13 (𝜑 → ((((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝑀𝑀 ∥ (𝐵𝐷)) → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐵𝐷)))
132109, 129, 131mp2and 695 . . . . . . . . . . . 12 (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐵𝐷))
133 dvdssub2 15639 . . . . . . . . . . . 12 (((((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐵𝐷)) → (((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐵 ↔ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐷))
134105, 17, 20, 132, 133syl31anc 1365 . . . . . . . . . . 11 (𝜑 → (((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐵 ↔ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐷))
135124, 134mpbird 258 . . . . . . . . . 10 (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐵)
136 ax-1ne0 10594 . . . . . . . . . . . . . . 15 1 ≠ 0
137136a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 1 ≠ 0)
13849, 137eqnetrd 3080 . . . . . . . . . . . . 13 (𝜑 → (𝐴 gcd 𝐵) ≠ 0)
139138neneqd 3018 . . . . . . . . . . . 12 (𝜑 → ¬ (𝐴 gcd 𝐵) = 0)
140 gcdeq0 15853 . . . . . . . . . . . . 13 ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) = 0 ↔ (𝐴 = 0 ∧ 𝐵 = 0)))
14111, 17, 140syl2anc 584 . . . . . . . . . . . 12 (𝜑 → ((𝐴 gcd 𝐵) = 0 ↔ (𝐴 = 0 ∧ 𝐵 = 0)))
142139, 141mtbid 325 . . . . . . . . . . 11 (𝜑 → ¬ (𝐴 = 0 ∧ 𝐵 = 0))
143 dvdslegcd 15841 . . . . . . . . . . 11 (((((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → ((((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐴 ∧ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐵) → ((𝐶 gcd 𝐷) gcd 𝑀) ≤ (𝐴 gcd 𝐵)))
144105, 11, 17, 142, 143syl31anc 1365 . . . . . . . . . 10 (𝜑 → ((((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐴 ∧ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐵) → ((𝐶 gcd 𝐷) gcd 𝑀) ≤ (𝐴 gcd 𝐵)))
145121, 135, 144mp2and 695 . . . . . . . . 9 (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ≤ (𝐴 gcd 𝐵))
146145, 49breqtrd 5083 . . . . . . . 8 (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ≤ 1)
147 simpr 485 . . . . . . . . . . . 12 (((𝐶 gcd 𝐷) = 0 ∧ 𝑀 = 0) → 𝑀 = 0)
148147necon3ai 3038 . . . . . . . . . . 11 (𝑀 ≠ 0 → ¬ ((𝐶 gcd 𝐷) = 0 ∧ 𝑀 = 0))
149111, 148syl 17 . . . . . . . . . 10 (𝜑 → ¬ ((𝐶 gcd 𝐷) = 0 ∧ 𝑀 = 0))
150 gcdn0cl 15839 . . . . . . . . . 10 ((((𝐶 gcd 𝐷) ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ ¬ ((𝐶 gcd 𝐷) = 0 ∧ 𝑀 = 0)) → ((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℕ)
15151, 8, 149, 150syl21anc 833 . . . . . . . . 9 (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℕ)
152 nnle1eq1 11655 . . . . . . . . 9 (((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℕ → (((𝐶 gcd 𝐷) gcd 𝑀) ≤ 1 ↔ ((𝐶 gcd 𝐷) gcd 𝑀) = 1))
153151, 152syl 17 . . . . . . . 8 (𝜑 → (((𝐶 gcd 𝐷) gcd 𝑀) ≤ 1 ↔ ((𝐶 gcd 𝐷) gcd 𝑀) = 1))
154146, 153mpbid 233 . . . . . . 7 (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) = 1)
155 2nn 11698 . . . . . . . . 9 2 ∈ ℕ
156155a1i 11 . . . . . . . 8 (𝜑 → 2 ∈ ℕ)
157 rplpwr 15895 . . . . . . . 8 (((𝐶 gcd 𝐷) ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 2 ∈ ℕ) → (((𝐶 gcd 𝐷) gcd 𝑀) = 1 → (((𝐶 gcd 𝐷)↑2) gcd 𝑀) = 1))
15850, 5, 156, 157syl3anc 1363 . . . . . . 7 (𝜑 → (((𝐶 gcd 𝐷) gcd 𝑀) = 1 → (((𝐶 gcd 𝐷)↑2) gcd 𝑀) = 1))
159154, 158mpd 15 . . . . . 6 (𝜑 → (((𝐶 gcd 𝐷)↑2) gcd 𝑀) = 1)
160100, 159eqtrd 2853 . . . . 5 (𝜑 → (𝑀 gcd ((𝐶 gcd 𝐷)↑2)) = 1)
16165, 74nn0addcld 11947 . . . . . . 7 (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℕ0)
162161nn0zd 12073 . . . . . 6 (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℤ)
163 coprmdvds 15985 . . . . . 6 ((𝑀 ∈ ℤ ∧ ((𝐶 gcd 𝐷)↑2) ∈ ℤ ∧ ((𝐸↑2) + (𝐹↑2)) ∈ ℤ) → ((𝑀 ∥ (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2))) ∧ (𝑀 gcd ((𝐶 gcd 𝐷)↑2)) = 1) → 𝑀 ∥ ((𝐸↑2) + (𝐹↑2))))
1648, 98, 162, 163syl3anc 1363 . . . . 5 (𝜑 → ((𝑀 ∥ (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2))) ∧ (𝑀 gcd ((𝐶 gcd 𝐷)↑2)) = 1) → 𝑀 ∥ ((𝐸↑2) + (𝐹↑2))))
16596, 160, 164mp2and 695 . . . 4 (𝜑𝑀 ∥ ((𝐸↑2) + (𝐹↑2)))
166 dvdsval2 15598 . . . . 5 ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ ((𝐸↑2) + (𝐹↑2)) ∈ ℤ) → (𝑀 ∥ ((𝐸↑2) + (𝐹↑2)) ↔ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ))
1678, 111, 162, 166syl3anc 1363 . . . 4 (𝜑 → (𝑀 ∥ ((𝐸↑2) + (𝐹↑2)) ↔ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ))
168165, 167mpbid 233 . . 3 (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ)
16965nn0red 11944 . . . . 5 (𝜑 → (𝐸↑2) ∈ ℝ)
17074nn0red 11944 . . . . 5 (𝜑 → (𝐹↑2) ∈ ℝ)
171169, 170readdcld 10658 . . . 4 (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℝ)
1725nnred 11641 . . . 4 (𝜑𝑀 ∈ ℝ)
1731, 472sqlem7 25927 . . . . . . 7 𝑌 ⊆ (𝑆 ∩ ℕ)
174 inss2 4203 . . . . . . 7 (𝑆 ∩ ℕ) ⊆ ℕ
175173, 174sstri 3973 . . . . . 6 𝑌 ⊆ ℕ
17663, 72gcdcld 15845 . . . . . . . . . 10 (𝜑 → (𝐸 gcd 𝐹) ∈ ℕ0)
177176nn0cnd 11945 . . . . . . . . 9 (𝜑 → (𝐸 gcd 𝐹) ∈ ℂ)
178 1cnd 10624 . . . . . . . . 9 (𝜑 → 1 ∈ ℂ)
17977mulid1d 10646 . . . . . . . . . 10 (𝜑 → ((𝐶 gcd 𝐷) · 1) = (𝐶 gcd 𝐷))
18083, 91oveq12d 7163 . . . . . . . . . 10 (𝜑 → (((𝐶 gcd 𝐷) · 𝐸) gcd ((𝐶 gcd 𝐷) · 𝐹)) = (𝐶 gcd 𝐷))
18114, 20gcdcld 15845 . . . . . . . . . . 11 (𝜑 → (𝐶 gcd 𝐷) ∈ ℕ0)
182 mulgcd 15884 . . . . . . . . . . 11 (((𝐶 gcd 𝐷) ∈ ℕ0𝐸 ∈ ℤ ∧ 𝐹 ∈ ℤ) → (((𝐶 gcd 𝐷) · 𝐸) gcd ((𝐶 gcd 𝐷) · 𝐹)) = ((𝐶 gcd 𝐷) · (𝐸 gcd 𝐹)))
183181, 63, 72, 182syl3anc 1363 . . . . . . . . . 10 (𝜑 → (((𝐶 gcd 𝐷) · 𝐸) gcd ((𝐶 gcd 𝐷) · 𝐹)) = ((𝐶 gcd 𝐷) · (𝐸 gcd 𝐹)))
184179, 180, 1833eqtr2rd 2860 . . . . . . . . 9 (𝜑 → ((𝐶 gcd 𝐷) · (𝐸 gcd 𝐹)) = ((𝐶 gcd 𝐷) · 1))
185177, 178, 77, 59, 184mulcanad 11263 . . . . . . . 8 (𝜑 → (𝐸 gcd 𝐹) = 1)
186 eqidd 2819 . . . . . . . 8 (𝜑 → ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝐹↑2)))
187 oveq1 7152 . . . . . . . . . . 11 (𝑥 = 𝐸 → (𝑥 gcd 𝑦) = (𝐸 gcd 𝑦))
188187eqeq1d 2820 . . . . . . . . . 10 (𝑥 = 𝐸 → ((𝑥 gcd 𝑦) = 1 ↔ (𝐸 gcd 𝑦) = 1))
189 oveq1 7152 . . . . . . . . . . . 12 (𝑥 = 𝐸 → (𝑥↑2) = (𝐸↑2))
190189oveq1d 7160 . . . . . . . . . . 11 (𝑥 = 𝐸 → ((𝑥↑2) + (𝑦↑2)) = ((𝐸↑2) + (𝑦↑2)))
191190eqeq2d 2829 . . . . . . . . . 10 (𝑥 = 𝐸 → (((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2)) ↔ ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝑦↑2))))
192188, 191anbi12d 630 . . . . . . . . 9 (𝑥 = 𝐸 → (((𝑥 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2))) ↔ ((𝐸 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝑦↑2)))))
193 oveq2 7153 . . . . . . . . . . 11 (𝑦 = 𝐹 → (𝐸 gcd 𝑦) = (𝐸 gcd 𝐹))
194193eqeq1d 2820 . . . . . . . . . 10 (𝑦 = 𝐹 → ((𝐸 gcd 𝑦) = 1 ↔ (𝐸 gcd 𝐹) = 1))
195 oveq1 7152 . . . . . . . . . . . 12 (𝑦 = 𝐹 → (𝑦↑2) = (𝐹↑2))
196195oveq2d 7161 . . . . . . . . . . 11 (𝑦 = 𝐹 → ((𝐸↑2) + (𝑦↑2)) = ((𝐸↑2) + (𝐹↑2)))
197196eqeq2d 2829 . . . . . . . . . 10 (𝑦 = 𝐹 → (((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝑦↑2)) ↔ ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝐹↑2))))
198194, 197anbi12d 630 . . . . . . . . 9 (𝑦 = 𝐹 → (((𝐸 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝑦↑2))) ↔ ((𝐸 gcd 𝐹) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝐹↑2)))))
199192, 198rspc2ev 3632 . . . . . . . 8 ((𝐸 ∈ ℤ ∧ 𝐹 ∈ ℤ ∧ ((𝐸 gcd 𝐹) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝐹↑2)))) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2))))
20063, 72, 185, 186, 199syl112anc 1366 . . . . . . 7 (𝜑 → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2))))
201 ovex 7178 . . . . . . . 8 ((𝐸↑2) + (𝐹↑2)) ∈ V
202 eqeq1 2822 . . . . . . . . . 10 (𝑧 = ((𝐸↑2) + (𝐹↑2)) → (𝑧 = ((𝑥↑2) + (𝑦↑2)) ↔ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2))))
203202anbi2d 628 . . . . . . . . 9 (𝑧 = ((𝐸↑2) + (𝐹↑2)) → (((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2))) ↔ ((𝑥 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2)))))
2042032rexbidv 3297 . . . . . . . 8 (𝑧 = ((𝐸↑2) + (𝐹↑2)) → (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2))) ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2)))))
205201, 204, 47elab2 3667 . . . . . . 7 (((𝐸↑2) + (𝐹↑2)) ∈ 𝑌 ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2))))
206200, 205sylibr 235 . . . . . 6 (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ 𝑌)
207175, 206sseldi 3962 . . . . 5 (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℕ)
208207nngt0d 11674 . . . 4 (𝜑 → 0 < ((𝐸↑2) + (𝐹↑2)))
2095nngt0d 11674 . . . 4 (𝜑 → 0 < 𝑀)
210171, 172, 208, 209divgt0d 11563 . . 3 (𝜑 → 0 < (((𝐸↑2) + (𝐹↑2)) / 𝑀))
211 elnnz 11979 . . 3 ((((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℕ ↔ ((((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ ∧ 0 < (((𝐸↑2) + (𝐹↑2)) / 𝑀)))
212168, 210, 211sylanbrc 583 . 2 (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℕ)
213 prmnn 16006 . . . . . . . 8 (𝑝 ∈ ℙ → 𝑝 ∈ ℕ)
214213ad2antrl 724 . . . . . . 7 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∈ ℕ)
215214nnred 11641 . . . . . . . 8 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∈ ℝ)
216168adantr 481 . . . . . . . . 9 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ)
217216zred 12075 . . . . . . . 8 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℝ)
218 peano2zm 12013 . . . . . . . . . . 11 (𝑀 ∈ ℤ → (𝑀 − 1) ∈ ℤ)
2198, 218syl 17 . . . . . . . . . 10 (𝜑 → (𝑀 − 1) ∈ ℤ)
220219zred 12075 . . . . . . . . 9 (𝜑 → (𝑀 − 1) ∈ ℝ)
221220adantr 481 . . . . . . . 8 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (𝑀 − 1) ∈ ℝ)
222 simprr 769 . . . . . . . . 9 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))
223 prmz 16007 . . . . . . . . . . 11 (𝑝 ∈ ℙ → 𝑝 ∈ ℤ)
224223ad2antrl 724 . . . . . . . . . 10 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∈ ℤ)
225212adantr 481 . . . . . . . . . 10 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℕ)
226 dvdsle 15648 . . . . . . . . . 10 ((𝑝 ∈ ℤ ∧ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℕ) → (𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀) → 𝑝 ≤ (((𝐸↑2) + (𝐹↑2)) / 𝑀)))
227224, 225, 226syl2anc 584 . . . . . . . . 9 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀) → 𝑝 ≤ (((𝐸↑2) + (𝐹↑2)) / 𝑀)))
228222, 227mpd 15 . . . . . . . 8 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ≤ (((𝐸↑2) + (𝐹↑2)) / 𝑀))
229 zsqcl 13482 . . . . . . . . . . . . . . . 16 (𝑀 ∈ ℤ → (𝑀↑2) ∈ ℤ)
2308, 229syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝑀↑2) ∈ ℤ)
231230zred 12075 . . . . . . . . . . . . . 14 (𝜑 → (𝑀↑2) ∈ ℝ)
232231rehalfcld 11872 . . . . . . . . . . . . 13 (𝜑 → ((𝑀↑2) / 2) ∈ ℝ)
23316zred 12075 . . . . . . . . . . . . . . 15 (𝜑 → (𝐶↑2) ∈ ℝ)
23422zred 12075 . . . . . . . . . . . . . . 15 (𝜑 → (𝐷↑2) ∈ ℝ)
235233, 234readdcld 10658 . . . . . . . . . . . . . 14 (𝜑 → ((𝐶↑2) + (𝐷↑2)) ∈ ℝ)
236 1red 10630 . . . . . . . . . . . . . . . 16 (𝜑 → 1 ∈ ℝ)
23750nnsqcld 13593 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐶 gcd 𝐷)↑2) ∈ ℕ)
238237nnred 11641 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐶 gcd 𝐷)↑2) ∈ ℝ)
239161nn0ge0d 11946 . . . . . . . . . . . . . . . 16 (𝜑 → 0 ≤ ((𝐸↑2) + (𝐹↑2)))
240237nnge1d 11673 . . . . . . . . . . . . . . . 16 (𝜑 → 1 ≤ ((𝐶 gcd 𝐷)↑2))
241236, 238, 171, 239, 240lemul1ad 11567 . . . . . . . . . . . . . . 15 (𝜑 → (1 · ((𝐸↑2) + (𝐹↑2))) ≤ (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2))))
242161nn0cnd 11945 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℂ)
243242mulid2d 10647 . . . . . . . . . . . . . . 15 (𝜑 → (1 · ((𝐸↑2) + (𝐹↑2))) = ((𝐸↑2) + (𝐹↑2)))
244241, 243, 953brtr3d 5088 . . . . . . . . . . . . . 14 (𝜑 → ((𝐸↑2) + (𝐹↑2)) ≤ ((𝐶↑2) + (𝐷↑2)))
245232rehalfcld 11872 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝑀↑2) / 2) / 2) ∈ ℝ)
24611, 5, 124sqlem7 16268 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐶↑2) ≤ (((𝑀↑2) / 2) / 2))
24717, 5, 184sqlem7 16268 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐷↑2) ≤ (((𝑀↑2) / 2) / 2))
248233, 234, 245, 245, 246, 247le2addd 11247 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐶↑2) + (𝐷↑2)) ≤ ((((𝑀↑2) / 2) / 2) + (((𝑀↑2) / 2) / 2)))
249232recnd 10657 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑀↑2) / 2) ∈ ℂ)
2502492halvesd 11871 . . . . . . . . . . . . . . 15 (𝜑 → ((((𝑀↑2) / 2) / 2) + (((𝑀↑2) / 2) / 2)) = ((𝑀↑2) / 2))
251248, 250breqtrd 5083 . . . . . . . . . . . . . 14 (𝜑 → ((𝐶↑2) + (𝐷↑2)) ≤ ((𝑀↑2) / 2))
252171, 235, 232, 244, 251letrd 10785 . . . . . . . . . . . . 13 (𝜑 → ((𝐸↑2) + (𝐹↑2)) ≤ ((𝑀↑2) / 2))
2535nnsqcld 13593 . . . . . . . . . . . . . . 15 (𝜑 → (𝑀↑2) ∈ ℕ)
254253nnrpd 12417 . . . . . . . . . . . . . 14 (𝜑 → (𝑀↑2) ∈ ℝ+)
255 rphalflt 12406 . . . . . . . . . . . . . 14 ((𝑀↑2) ∈ ℝ+ → ((𝑀↑2) / 2) < (𝑀↑2))
256254, 255syl 17 . . . . . . . . . . . . 13 (𝜑 → ((𝑀↑2) / 2) < (𝑀↑2))
257171, 232, 231, 252, 256lelttrd 10786 . . . . . . . . . . . 12 (𝜑 → ((𝐸↑2) + (𝐹↑2)) < (𝑀↑2))
2588zcnd 12076 . . . . . . . . . . . . 13 (𝜑𝑀 ∈ ℂ)
259258sqvald 13495 . . . . . . . . . . . 12 (𝜑 → (𝑀↑2) = (𝑀 · 𝑀))
260257, 259breqtrd 5083 . . . . . . . . . . 11 (𝜑 → ((𝐸↑2) + (𝐹↑2)) < (𝑀 · 𝑀))
261 ltdivmul 11503 . . . . . . . . . . . 12 ((((𝐸↑2) + (𝐹↑2)) ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (𝑀 ∈ ℝ ∧ 0 < 𝑀)) → ((((𝐸↑2) + (𝐹↑2)) / 𝑀) < 𝑀 ↔ ((𝐸↑2) + (𝐹↑2)) < (𝑀 · 𝑀)))
262171, 172, 172, 209, 261syl112anc 1366 . . . . . . . . . . 11 (𝜑 → ((((𝐸↑2) + (𝐹↑2)) / 𝑀) < 𝑀 ↔ ((𝐸↑2) + (𝐹↑2)) < (𝑀 · 𝑀)))
263260, 262mpbird 258 . . . . . . . . . 10 (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) < 𝑀)
264 zltlem1 12023 . . . . . . . . . . 11 (((((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((((𝐸↑2) + (𝐹↑2)) / 𝑀) < 𝑀 ↔ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ≤ (𝑀 − 1)))
265168, 8, 264syl2anc 584 . . . . . . . . . 10 (𝜑 → ((((𝐸↑2) + (𝐹↑2)) / 𝑀) < 𝑀 ↔ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ≤ (𝑀 − 1)))
266263, 265mpbid 233 . . . . . . . . 9 (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ≤ (𝑀 − 1))
267266adantr 481 . . . . . . . 8 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ≤ (𝑀 − 1))
268215, 217, 221, 228, 267letrd 10785 . . . . . . 7 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ≤ (𝑀 − 1))
269219adantr 481 . . . . . . . 8 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (𝑀 − 1) ∈ ℤ)
270 fznn 12963 . . . . . . . 8 ((𝑀 − 1) ∈ ℤ → (𝑝 ∈ (1...(𝑀 − 1)) ↔ (𝑝 ∈ ℕ ∧ 𝑝 ≤ (𝑀 − 1))))
271269, 270syl 17 . . . . . . 7 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (𝑝 ∈ (1...(𝑀 − 1)) ↔ (𝑝 ∈ ℕ ∧ 𝑝 ≤ (𝑀 − 1))))
272214, 268, 271mpbir2and 709 . . . . . 6 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∈ (1...(𝑀 − 1)))
273206adantr 481 . . . . . 6 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → ((𝐸↑2) + (𝐹↑2)) ∈ 𝑌)
274272, 273jca 512 . . . . 5 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (𝑝 ∈ (1...(𝑀 − 1)) ∧ ((𝐸↑2) + (𝐹↑2)) ∈ 𝑌))
27548adantr 481 . . . . 5 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → ∀𝑏 ∈ (1...(𝑀 − 1))∀𝑎𝑌 (𝑏𝑎𝑏𝑆))
276 dvdsmul2 15620 . . . . . . . . 9 ((𝑀 ∈ ℤ ∧ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∥ (𝑀 · (((𝐸↑2) + (𝐹↑2)) / 𝑀)))
2778, 168, 276syl2anc 584 . . . . . . . 8 (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∥ (𝑀 · (((𝐸↑2) + (𝐹↑2)) / 𝑀)))
278242, 258, 111divcan2d 11406 . . . . . . . 8 (𝜑 → (𝑀 · (((𝐸↑2) + (𝐹↑2)) / 𝑀)) = ((𝐸↑2) + (𝐹↑2)))
279277, 278breqtrd 5083 . . . . . . 7 (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∥ ((𝐸↑2) + (𝐹↑2)))
280279adantr 481 . . . . . 6 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∥ ((𝐸↑2) + (𝐹↑2)))
281162adantr 481 . . . . . . 7 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → ((𝐸↑2) + (𝐹↑2)) ∈ ℤ)
282 dvdstr 15634 . . . . . . 7 ((𝑝 ∈ ℤ ∧ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ ∧ ((𝐸↑2) + (𝐹↑2)) ∈ ℤ) → ((𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∧ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∥ ((𝐸↑2) + (𝐹↑2))) → 𝑝 ∥ ((𝐸↑2) + (𝐹↑2))))
283224, 216, 281, 282syl3anc 1363 . . . . . 6 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → ((𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∧ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∥ ((𝐸↑2) + (𝐹↑2))) → 𝑝 ∥ ((𝐸↑2) + (𝐹↑2))))
284222, 280, 283mp2and 695 . . . . 5 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∥ ((𝐸↑2) + (𝐹↑2)))
285 breq1 5060 . . . . . . 7 (𝑏 = 𝑝 → (𝑏𝑎𝑝𝑎))
286 eleq1w 2892 . . . . . . 7 (𝑏 = 𝑝 → (𝑏𝑆𝑝𝑆))
287285, 286imbi12d 346 . . . . . 6 (𝑏 = 𝑝 → ((𝑏𝑎𝑏𝑆) ↔ (𝑝𝑎𝑝𝑆)))
288 breq2 5061 . . . . . . 7 (𝑎 = ((𝐸↑2) + (𝐹↑2)) → (𝑝𝑎𝑝 ∥ ((𝐸↑2) + (𝐹↑2))))
289288imbi1d 343 . . . . . 6 (𝑎 = ((𝐸↑2) + (𝐹↑2)) → ((𝑝𝑎𝑝𝑆) ↔ (𝑝 ∥ ((𝐸↑2) + (𝐹↑2)) → 𝑝𝑆)))
290287, 289rspc2v 3630 . . . . 5 ((𝑝 ∈ (1...(𝑀 − 1)) ∧ ((𝐸↑2) + (𝐹↑2)) ∈ 𝑌) → (∀𝑏 ∈ (1...(𝑀 − 1))∀𝑎𝑌 (𝑏𝑎𝑏𝑆) → (𝑝 ∥ ((𝐸↑2) + (𝐹↑2)) → 𝑝𝑆)))
291274, 275, 284, 290syl3c 66 . . . 4 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝𝑆)
292291expr 457 . . 3 ((𝜑𝑝 ∈ ℙ) → (𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀) → 𝑝𝑆))
293292ralrimiva 3179 . 2 (𝜑 → ∀𝑝 ∈ ℙ (𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀) → 𝑝𝑆))
294 inss1 4202 . . . . 5 (𝑆 ∩ ℕ) ⊆ 𝑆
295173, 294sstri 3973 . . . 4 𝑌𝑆
296295, 206sseldi 3962 . . 3 (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ 𝑆)
297278, 296eqeltrd 2910 . 2 (𝜑 → (𝑀 · (((𝐸↑2) + (𝐹↑2)) / 𝑀)) ∈ 𝑆)
2981, 5, 212, 293, 2972sqlem6 25926 1 (𝜑𝑀𝑆)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396   = wceq 1528  wcel 2105  {cab 2796  wne 3013  wral 3135  wrex 3136  cin 3932   class class class wbr 5057  cmpt 5137  ran crn 5549  cfv 6348  (class class class)co 7145  cr 10524  0cc0 10525  1c1 10526   + caddc 10528   · cmul 10530   < clt 10663  cle 10664  cmin 10858   / cdiv 11285  cn 11626  2c2 11680  0cn0 11885  cz 11969  cuz 12231  +crp 12377  ...cfz 12880   mod cmo 13225  cexp 13417  abscabs 14581  cdvds 15595   gcd cgcd 15831  cprime 16003  ℤ[i]cgz 16253
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-cnex 10581  ax-resscn 10582  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-addrcl 10586  ax-mulcl 10587  ax-mulrcl 10588  ax-mulcom 10589  ax-addass 10590  ax-mulass 10591  ax-distr 10592  ax-i2m1 10593  ax-1ne0 10594  ax-1rid 10595  ax-rnegex 10596  ax-rrecex 10597  ax-cnre 10598  ax-pre-lttri 10599  ax-pre-lttrn 10600  ax-pre-ltadd 10601  ax-pre-mulgt0 10602  ax-pre-sup 10603
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-nel 3121  df-ral 3140  df-rex 3141  df-reu 3142  df-rmo 3143  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7570  df-1st 7678  df-2nd 7679  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-1o 8091  df-2o 8092  df-er 8278  df-en 8498  df-dom 8499  df-sdom 8500  df-fin 8501  df-sup 8894  df-inf 8895  df-pnf 10665  df-mnf 10666  df-xr 10667  df-ltxr 10668  df-le 10669  df-sub 10860  df-neg 10861  df-div 11286  df-nn 11627  df-2 11688  df-3 11689  df-n0 11886  df-z 11970  df-uz 12232  df-rp 12378  df-fz 12881  df-fl 13150  df-mod 13226  df-seq 13358  df-exp 13418  df-cj 14446  df-re 14447  df-im 14448  df-sqrt 14582  df-abs 14583  df-dvds 15596  df-gcd 15832  df-prm 16004  df-gz 16254
This theorem is referenced by:  2sqlem9  25930
  Copyright terms: Public domain W3C validator