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

Theorem 2sqlem8 26918
Description: Lemma for 2sq 26922. (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 12902 . . . 4 (𝑀 ∈ (ℤ‘2) ↔ (𝑀 ∈ ℕ ∧ 𝑀 ≠ 1))
42, 3sylib 217 . . 3 (𝜑 → (𝑀 ∈ ℕ ∧ 𝑀 ≠ 1))
54simpld 495 . 2 (𝜑𝑀 ∈ ℕ)
6 2sqlem9.7 . . . . . . 7 (𝜑𝑀𝑁)
7 eluzelz 12828 . . . . . . . . 9 (𝑀 ∈ (ℤ‘2) → 𝑀 ∈ ℤ)
82, 7syl 17 . . . . . . . 8 (𝜑𝑀 ∈ ℤ)
9 2sqlem8.n . . . . . . . . 9 (𝜑𝑁 ∈ ℕ)
109nnzd 12581 . . . . . . . 8 (𝜑𝑁 ∈ ℤ)
11 2sqlem8.1 . . . . . . . . . . . 12 (𝜑𝐴 ∈ ℤ)
12 2sqlem8.c . . . . . . . . . . . 12 𝐶 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))
1311, 5, 124sqlem5 16871 . . . . . . . . . . 11 (𝜑 → (𝐶 ∈ ℤ ∧ ((𝐴𝐶) / 𝑀) ∈ ℤ))
1413simpld 495 . . . . . . . . . 10 (𝜑𝐶 ∈ ℤ)
15 zsqcl 14090 . . . . . . . . . 10 (𝐶 ∈ ℤ → (𝐶↑2) ∈ ℤ)
1614, 15syl 17 . . . . . . . . 9 (𝜑 → (𝐶↑2) ∈ ℤ)
17 2sqlem8.2 . . . . . . . . . . . 12 (𝜑𝐵 ∈ ℤ)
18 2sqlem8.d . . . . . . . . . . . 12 𝐷 = (((𝐵 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))
1917, 5, 184sqlem5 16871 . . . . . . . . . . 11 (𝜑 → (𝐷 ∈ ℤ ∧ ((𝐵𝐷) / 𝑀) ∈ ℤ))
2019simpld 495 . . . . . . . . . 10 (𝜑𝐷 ∈ ℤ)
21 zsqcl 14090 . . . . . . . . . 10 (𝐷 ∈ ℤ → (𝐷↑2) ∈ ℤ)
2220, 21syl 17 . . . . . . . . 9 (𝜑 → (𝐷↑2) ∈ ℤ)
2316, 22zaddcld 12666 . . . . . . . 8 (𝜑 → ((𝐶↑2) + (𝐷↑2)) ∈ ℤ)
24 zsqcl 14090 . . . . . . . . . . . 12 (𝐴 ∈ ℤ → (𝐴↑2) ∈ ℤ)
2511, 24syl 17 . . . . . . . . . . 11 (𝜑 → (𝐴↑2) ∈ ℤ)
2625, 16zsubcld 12667 . . . . . . . . . 10 (𝜑 → ((𝐴↑2) − (𝐶↑2)) ∈ ℤ)
27 zsqcl 14090 . . . . . . . . . . . 12 (𝐵 ∈ ℤ → (𝐵↑2) ∈ ℤ)
2817, 27syl 17 . . . . . . . . . . 11 (𝜑 → (𝐵↑2) ∈ ℤ)
2928, 22zsubcld 12667 . . . . . . . . . 10 (𝜑 → ((𝐵↑2) − (𝐷↑2)) ∈ ℤ)
3011, 5, 124sqlem8 16874 . . . . . . . . . 10 (𝜑𝑀 ∥ ((𝐴↑2) − (𝐶↑2)))
3117, 5, 184sqlem8 16874 . . . . . . . . . 10 (𝜑𝑀 ∥ ((𝐵↑2) − (𝐷↑2)))
328, 26, 29, 30, 31dvds2addd 16231 . . . . . . . . 9 (𝜑𝑀 ∥ (((𝐴↑2) − (𝐶↑2)) + ((𝐵↑2) − (𝐷↑2))))
33 2sqlem8.4 . . . . . . . . . . 11 (𝜑𝑁 = ((𝐴↑2) + (𝐵↑2)))
3433oveq1d 7420 . . . . . . . . . 10 (𝜑 → (𝑁 − ((𝐶↑2) + (𝐷↑2))) = (((𝐴↑2) + (𝐵↑2)) − ((𝐶↑2) + (𝐷↑2))))
3525zcnd 12663 . . . . . . . . . . 11 (𝜑 → (𝐴↑2) ∈ ℂ)
3628zcnd 12663 . . . . . . . . . . 11 (𝜑 → (𝐵↑2) ∈ ℂ)
3716zcnd 12663 . . . . . . . . . . 11 (𝜑 → (𝐶↑2) ∈ ℂ)
3822zcnd 12663 . . . . . . . . . . 11 (𝜑 → (𝐷↑2) ∈ ℂ)
3935, 36, 37, 38addsub4d 11614 . . . . . . . . . 10 (𝜑 → (((𝐴↑2) + (𝐵↑2)) − ((𝐶↑2) + (𝐷↑2))) = (((𝐴↑2) − (𝐶↑2)) + ((𝐵↑2) − (𝐷↑2))))
4034, 39eqtrd 2772 . . . . . . . . 9 (𝜑 → (𝑁 − ((𝐶↑2) + (𝐷↑2))) = (((𝐴↑2) − (𝐶↑2)) + ((𝐵↑2) − (𝐷↑2))))
4132, 40breqtrrd 5175 . . . . . . . 8 (𝜑𝑀 ∥ (𝑁 − ((𝐶↑2) + (𝐷↑2))))
42 dvdssub2 16240 . . . . . . . 8 (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ((𝐶↑2) + (𝐷↑2)) ∈ ℤ) ∧ 𝑀 ∥ (𝑁 − ((𝐶↑2) + (𝐷↑2)))) → (𝑀𝑁𝑀 ∥ ((𝐶↑2) + (𝐷↑2))))
438, 10, 23, 41, 42syl31anc 1373 . . . . . . 7 (𝜑 → (𝑀𝑁𝑀 ∥ ((𝐶↑2) + (𝐷↑2))))
446, 43mpbid 231 . . . . . 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 26917 . . . . . . . . . . 11 (𝜑 → (𝐶 gcd 𝐷) ∈ ℕ)
4948nnzd 12581 . . . . . . . . . 10 (𝜑 → (𝐶 gcd 𝐷) ∈ ℤ)
50 zsqcl2 14099 . . . . . . . . . 10 ((𝐶 gcd 𝐷) ∈ ℤ → ((𝐶 gcd 𝐷)↑2) ∈ ℕ0)
5149, 50syl 17 . . . . . . . . 9 (𝜑 → ((𝐶 gcd 𝐷)↑2) ∈ ℕ0)
5251nn0cnd 12530 . . . . . . . 8 (𝜑 → ((𝐶 gcd 𝐷)↑2) ∈ ℂ)
53 2sqlem8.e . . . . . . . . . . 11 𝐸 = (𝐶 / (𝐶 gcd 𝐷))
54 gcddvds 16440 . . . . . . . . . . . . . 14 ((𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ) → ((𝐶 gcd 𝐷) ∥ 𝐶 ∧ (𝐶 gcd 𝐷) ∥ 𝐷))
5514, 20, 54syl2anc 584 . . . . . . . . . . . . 13 (𝜑 → ((𝐶 gcd 𝐷) ∥ 𝐶 ∧ (𝐶 gcd 𝐷) ∥ 𝐷))
5655simpld 495 . . . . . . . . . . . 12 (𝜑 → (𝐶 gcd 𝐷) ∥ 𝐶)
5748nnne0d 12258 . . . . . . . . . . . . 13 (𝜑 → (𝐶 gcd 𝐷) ≠ 0)
58 dvdsval2 16196 . . . . . . . . . . . . 13 (((𝐶 gcd 𝐷) ∈ ℤ ∧ (𝐶 gcd 𝐷) ≠ 0 ∧ 𝐶 ∈ ℤ) → ((𝐶 gcd 𝐷) ∥ 𝐶 ↔ (𝐶 / (𝐶 gcd 𝐷)) ∈ ℤ))
5949, 57, 14, 58syl3anc 1371 . . . . . . . . . . . 12 (𝜑 → ((𝐶 gcd 𝐷) ∥ 𝐶 ↔ (𝐶 / (𝐶 gcd 𝐷)) ∈ ℤ))
6056, 59mpbid 231 . . . . . . . . . . 11 (𝜑 → (𝐶 / (𝐶 gcd 𝐷)) ∈ ℤ)
6153, 60eqeltrid 2837 . . . . . . . . . 10 (𝜑𝐸 ∈ ℤ)
62 zsqcl2 14099 . . . . . . . . . 10 (𝐸 ∈ ℤ → (𝐸↑2) ∈ ℕ0)
6361, 62syl 17 . . . . . . . . 9 (𝜑 → (𝐸↑2) ∈ ℕ0)
6463nn0cnd 12530 . . . . . . . 8 (𝜑 → (𝐸↑2) ∈ ℂ)
65 2sqlem8.f . . . . . . . . . . 11 𝐹 = (𝐷 / (𝐶 gcd 𝐷))
6655simprd 496 . . . . . . . . . . . 12 (𝜑 → (𝐶 gcd 𝐷) ∥ 𝐷)
67 dvdsval2 16196 . . . . . . . . . . . . 13 (((𝐶 gcd 𝐷) ∈ ℤ ∧ (𝐶 gcd 𝐷) ≠ 0 ∧ 𝐷 ∈ ℤ) → ((𝐶 gcd 𝐷) ∥ 𝐷 ↔ (𝐷 / (𝐶 gcd 𝐷)) ∈ ℤ))
6849, 57, 20, 67syl3anc 1371 . . . . . . . . . . . 12 (𝜑 → ((𝐶 gcd 𝐷) ∥ 𝐷 ↔ (𝐷 / (𝐶 gcd 𝐷)) ∈ ℤ))
6966, 68mpbid 231 . . . . . . . . . . 11 (𝜑 → (𝐷 / (𝐶 gcd 𝐷)) ∈ ℤ)
7065, 69eqeltrid 2837 . . . . . . . . . 10 (𝜑𝐹 ∈ ℤ)
71 zsqcl2 14099 . . . . . . . . . 10 (𝐹 ∈ ℤ → (𝐹↑2) ∈ ℕ0)
7270, 71syl 17 . . . . . . . . 9 (𝜑 → (𝐹↑2) ∈ ℕ0)
7372nn0cnd 12530 . . . . . . . 8 (𝜑 → (𝐹↑2) ∈ ℂ)
7452, 64, 73adddid 11234 . . . . . . 7 (𝜑 → (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2))) = ((((𝐶 gcd 𝐷)↑2) · (𝐸↑2)) + (((𝐶 gcd 𝐷)↑2) · (𝐹↑2))))
7549zcnd 12663 . . . . . . . . . 10 (𝜑 → (𝐶 gcd 𝐷) ∈ ℂ)
7661zcnd 12663 . . . . . . . . . 10 (𝜑𝐸 ∈ ℂ)
7775, 76sqmuld 14119 . . . . . . . . 9 (𝜑 → (((𝐶 gcd 𝐷) · 𝐸)↑2) = (((𝐶 gcd 𝐷)↑2) · (𝐸↑2)))
7853oveq2i 7416 . . . . . . . . . . 11 ((𝐶 gcd 𝐷) · 𝐸) = ((𝐶 gcd 𝐷) · (𝐶 / (𝐶 gcd 𝐷)))
7914zcnd 12663 . . . . . . . . . . . 12 (𝜑𝐶 ∈ ℂ)
8079, 75, 57divcan2d 11988 . . . . . . . . . . 11 (𝜑 → ((𝐶 gcd 𝐷) · (𝐶 / (𝐶 gcd 𝐷))) = 𝐶)
8178, 80eqtrid 2784 . . . . . . . . . 10 (𝜑 → ((𝐶 gcd 𝐷) · 𝐸) = 𝐶)
8281oveq1d 7420 . . . . . . . . 9 (𝜑 → (((𝐶 gcd 𝐷) · 𝐸)↑2) = (𝐶↑2))
8377, 82eqtr3d 2774 . . . . . . . 8 (𝜑 → (((𝐶 gcd 𝐷)↑2) · (𝐸↑2)) = (𝐶↑2))
8470zcnd 12663 . . . . . . . . . 10 (𝜑𝐹 ∈ ℂ)
8575, 84sqmuld 14119 . . . . . . . . 9 (𝜑 → (((𝐶 gcd 𝐷) · 𝐹)↑2) = (((𝐶 gcd 𝐷)↑2) · (𝐹↑2)))
8665oveq2i 7416 . . . . . . . . . . 11 ((𝐶 gcd 𝐷) · 𝐹) = ((𝐶 gcd 𝐷) · (𝐷 / (𝐶 gcd 𝐷)))
8720zcnd 12663 . . . . . . . . . . . 12 (𝜑𝐷 ∈ ℂ)
8887, 75, 57divcan2d 11988 . . . . . . . . . . 11 (𝜑 → ((𝐶 gcd 𝐷) · (𝐷 / (𝐶 gcd 𝐷))) = 𝐷)
8986, 88eqtrid 2784 . . . . . . . . . 10 (𝜑 → ((𝐶 gcd 𝐷) · 𝐹) = 𝐷)
9089oveq1d 7420 . . . . . . . . 9 (𝜑 → (((𝐶 gcd 𝐷) · 𝐹)↑2) = (𝐷↑2))
9185, 90eqtr3d 2774 . . . . . . . 8 (𝜑 → (((𝐶 gcd 𝐷)↑2) · (𝐹↑2)) = (𝐷↑2))
9283, 91oveq12d 7423 . . . . . . 7 (𝜑 → ((((𝐶 gcd 𝐷)↑2) · (𝐸↑2)) + (((𝐶 gcd 𝐷)↑2) · (𝐹↑2))) = ((𝐶↑2) + (𝐷↑2)))
9374, 92eqtrd 2772 . . . . . 6 (𝜑 → (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2))) = ((𝐶↑2) + (𝐷↑2)))
9444, 93breqtrrd 5175 . . . . 5 (𝜑𝑀 ∥ (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2))))
95 zsqcl 14090 . . . . . . . 8 ((𝐶 gcd 𝐷) ∈ ℤ → ((𝐶 gcd 𝐷)↑2) ∈ ℤ)
9649, 95syl 17 . . . . . . 7 (𝜑 → ((𝐶 gcd 𝐷)↑2) ∈ ℤ)
978, 96gcdcomd 16451 . . . . . 6 (𝜑 → (𝑀 gcd ((𝐶 gcd 𝐷)↑2)) = (((𝐶 gcd 𝐷)↑2) gcd 𝑀))
9849, 8gcdcld 16445 . . . . . . . . . . . . 13 (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℕ0)
9998nn0zd 12580 . . . . . . . . . . . 12 (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℤ)
100 gcddvds 16440 . . . . . . . . . . . . . 14 (((𝐶 gcd 𝐷) ∈ ℤ ∧ 𝑀 ∈ ℤ) → (((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐶 gcd 𝐷) ∧ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝑀))
10149, 8, 100syl2anc 584 . . . . . . . . . . . . 13 (𝜑 → (((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐶 gcd 𝐷) ∧ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝑀))
102101simpld 495 . . . . . . . . . . . 12 (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐶 gcd 𝐷))
10399, 49, 14, 102, 56dvdstrd 16234 . . . . . . . . . . 11 (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐶)
10411, 14zsubcld 12667 . . . . . . . . . . . . 13 (𝜑 → (𝐴𝐶) ∈ ℤ)
105101simprd 496 . . . . . . . . . . . . 13 (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝑀)
10613simprd 496 . . . . . . . . . . . . . 14 (𝜑 → ((𝐴𝐶) / 𝑀) ∈ ℤ)
1075nnne0d 12258 . . . . . . . . . . . . . . 15 (𝜑𝑀 ≠ 0)
108 dvdsval2 16196 . . . . . . . . . . . . . . 15 ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ (𝐴𝐶) ∈ ℤ) → (𝑀 ∥ (𝐴𝐶) ↔ ((𝐴𝐶) / 𝑀) ∈ ℤ))
1098, 107, 104, 108syl3anc 1371 . . . . . . . . . . . . . 14 (𝜑 → (𝑀 ∥ (𝐴𝐶) ↔ ((𝐴𝐶) / 𝑀) ∈ ℤ))
110106, 109mpbird 256 . . . . . . . . . . . . 13 (𝜑𝑀 ∥ (𝐴𝐶))
11199, 8, 104, 105, 110dvdstrd 16234 . . . . . . . . . . . 12 (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐴𝐶))
112 dvdssub2 16240 . . . . . . . . . . . 12 (((((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐴𝐶)) → (((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐴 ↔ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐶))
11399, 11, 14, 111, 112syl31anc 1373 . . . . . . . . . . 11 (𝜑 → (((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐴 ↔ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐶))
114103, 113mpbird 256 . . . . . . . . . 10 (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐴)
11599, 49, 20, 102, 66dvdstrd 16234 . . . . . . . . . . 11 (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐷)
11617, 20zsubcld 12667 . . . . . . . . . . . . 13 (𝜑 → (𝐵𝐷) ∈ ℤ)
11719simprd 496 . . . . . . . . . . . . . 14 (𝜑 → ((𝐵𝐷) / 𝑀) ∈ ℤ)
118 dvdsval2 16196 . . . . . . . . . . . . . . 15 ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ (𝐵𝐷) ∈ ℤ) → (𝑀 ∥ (𝐵𝐷) ↔ ((𝐵𝐷) / 𝑀) ∈ ℤ))
1198, 107, 116, 118syl3anc 1371 . . . . . . . . . . . . . 14 (𝜑 → (𝑀 ∥ (𝐵𝐷) ↔ ((𝐵𝐷) / 𝑀) ∈ ℤ))
120117, 119mpbird 256 . . . . . . . . . . . . 13 (𝜑𝑀 ∥ (𝐵𝐷))
12199, 8, 116, 105, 120dvdstrd 16234 . . . . . . . . . . . 12 (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐵𝐷))
122 dvdssub2 16240 . . . . . . . . . . . 12 (((((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐵𝐷)) → (((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐵 ↔ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐷))
12399, 17, 20, 121, 122syl31anc 1373 . . . . . . . . . . 11 (𝜑 → (((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐵 ↔ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐷))
124115, 123mpbird 256 . . . . . . . . . 10 (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐵)
125 ax-1ne0 11175 . . . . . . . . . . . . . . 15 1 ≠ 0
126125a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 1 ≠ 0)
12747, 126eqnetrd 3008 . . . . . . . . . . . . 13 (𝜑 → (𝐴 gcd 𝐵) ≠ 0)
128127neneqd 2945 . . . . . . . . . . . 12 (𝜑 → ¬ (𝐴 gcd 𝐵) = 0)
129 gcdeq0 16454 . . . . . . . . . . . . 13 ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) = 0 ↔ (𝐴 = 0 ∧ 𝐵 = 0)))
13011, 17, 129syl2anc 584 . . . . . . . . . . . 12 (𝜑 → ((𝐴 gcd 𝐵) = 0 ↔ (𝐴 = 0 ∧ 𝐵 = 0)))
131128, 130mtbid 323 . . . . . . . . . . 11 (𝜑 → ¬ (𝐴 = 0 ∧ 𝐵 = 0))
132 dvdslegcd 16441 . . . . . . . . . . 11 (((((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → ((((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐴 ∧ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐵) → ((𝐶 gcd 𝐷) gcd 𝑀) ≤ (𝐴 gcd 𝐵)))
13399, 11, 17, 131, 132syl31anc 1373 . . . . . . . . . 10 (𝜑 → ((((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐴 ∧ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐵) → ((𝐶 gcd 𝐷) gcd 𝑀) ≤ (𝐴 gcd 𝐵)))
134114, 124, 133mp2and 697 . . . . . . . . 9 (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ≤ (𝐴 gcd 𝐵))
135134, 47breqtrd 5173 . . . . . . . 8 (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ≤ 1)
136 simpr 485 . . . . . . . . . . . 12 (((𝐶 gcd 𝐷) = 0 ∧ 𝑀 = 0) → 𝑀 = 0)
137136necon3ai 2965 . . . . . . . . . . 11 (𝑀 ≠ 0 → ¬ ((𝐶 gcd 𝐷) = 0 ∧ 𝑀 = 0))
138107, 137syl 17 . . . . . . . . . 10 (𝜑 → ¬ ((𝐶 gcd 𝐷) = 0 ∧ 𝑀 = 0))
139 gcdn0cl 16439 . . . . . . . . . 10 ((((𝐶 gcd 𝐷) ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ ¬ ((𝐶 gcd 𝐷) = 0 ∧ 𝑀 = 0)) → ((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℕ)
14049, 8, 138, 139syl21anc 836 . . . . . . . . 9 (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℕ)
141 nnle1eq1 12238 . . . . . . . . 9 (((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℕ → (((𝐶 gcd 𝐷) gcd 𝑀) ≤ 1 ↔ ((𝐶 gcd 𝐷) gcd 𝑀) = 1))
142140, 141syl 17 . . . . . . . 8 (𝜑 → (((𝐶 gcd 𝐷) gcd 𝑀) ≤ 1 ↔ ((𝐶 gcd 𝐷) gcd 𝑀) = 1))
143135, 142mpbid 231 . . . . . . 7 (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) = 1)
144 2nn 12281 . . . . . . . . 9 2 ∈ ℕ
145144a1i 11 . . . . . . . 8 (𝜑 → 2 ∈ ℕ)
146 rplpwr 16495 . . . . . . . 8 (((𝐶 gcd 𝐷) ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 2 ∈ ℕ) → (((𝐶 gcd 𝐷) gcd 𝑀) = 1 → (((𝐶 gcd 𝐷)↑2) gcd 𝑀) = 1))
14748, 5, 145, 146syl3anc 1371 . . . . . . 7 (𝜑 → (((𝐶 gcd 𝐷) gcd 𝑀) = 1 → (((𝐶 gcd 𝐷)↑2) gcd 𝑀) = 1))
148143, 147mpd 15 . . . . . 6 (𝜑 → (((𝐶 gcd 𝐷)↑2) gcd 𝑀) = 1)
14997, 148eqtrd 2772 . . . . 5 (𝜑 → (𝑀 gcd ((𝐶 gcd 𝐷)↑2)) = 1)
15063, 72nn0addcld 12532 . . . . . . 7 (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℕ0)
151150nn0zd 12580 . . . . . 6 (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℤ)
152 coprmdvds 16586 . . . . . 6 ((𝑀 ∈ ℤ ∧ ((𝐶 gcd 𝐷)↑2) ∈ ℤ ∧ ((𝐸↑2) + (𝐹↑2)) ∈ ℤ) → ((𝑀 ∥ (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2))) ∧ (𝑀 gcd ((𝐶 gcd 𝐷)↑2)) = 1) → 𝑀 ∥ ((𝐸↑2) + (𝐹↑2))))
1538, 96, 151, 152syl3anc 1371 . . . . 5 (𝜑 → ((𝑀 ∥ (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2))) ∧ (𝑀 gcd ((𝐶 gcd 𝐷)↑2)) = 1) → 𝑀 ∥ ((𝐸↑2) + (𝐹↑2))))
15494, 149, 153mp2and 697 . . . 4 (𝜑𝑀 ∥ ((𝐸↑2) + (𝐹↑2)))
155 dvdsval2 16196 . . . . 5 ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ ((𝐸↑2) + (𝐹↑2)) ∈ ℤ) → (𝑀 ∥ ((𝐸↑2) + (𝐹↑2)) ↔ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ))
1568, 107, 151, 155syl3anc 1371 . . . 4 (𝜑 → (𝑀 ∥ ((𝐸↑2) + (𝐹↑2)) ↔ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ))
157154, 156mpbid 231 . . 3 (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ)
15863nn0red 12529 . . . . 5 (𝜑 → (𝐸↑2) ∈ ℝ)
15972nn0red 12529 . . . . 5 (𝜑 → (𝐹↑2) ∈ ℝ)
160158, 159readdcld 11239 . . . 4 (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℝ)
1615nnred 12223 . . . 4 (𝜑𝑀 ∈ ℝ)
1621, 452sqlem7 26916 . . . . . . 7 𝑌 ⊆ (𝑆 ∩ ℕ)
163 inss2 4228 . . . . . . 7 (𝑆 ∩ ℕ) ⊆ ℕ
164162, 163sstri 3990 . . . . . 6 𝑌 ⊆ ℕ
16561, 70gcdcld 16445 . . . . . . . . . 10 (𝜑 → (𝐸 gcd 𝐹) ∈ ℕ0)
166165nn0cnd 12530 . . . . . . . . 9 (𝜑 → (𝐸 gcd 𝐹) ∈ ℂ)
167 1cnd 11205 . . . . . . . . 9 (𝜑 → 1 ∈ ℂ)
16875mulridd 11227 . . . . . . . . . 10 (𝜑 → ((𝐶 gcd 𝐷) · 1) = (𝐶 gcd 𝐷))
16981, 89oveq12d 7423 . . . . . . . . . 10 (𝜑 → (((𝐶 gcd 𝐷) · 𝐸) gcd ((𝐶 gcd 𝐷) · 𝐹)) = (𝐶 gcd 𝐷))
17014, 20gcdcld 16445 . . . . . . . . . . 11 (𝜑 → (𝐶 gcd 𝐷) ∈ ℕ0)
171 mulgcd 16486 . . . . . . . . . . 11 (((𝐶 gcd 𝐷) ∈ ℕ0𝐸 ∈ ℤ ∧ 𝐹 ∈ ℤ) → (((𝐶 gcd 𝐷) · 𝐸) gcd ((𝐶 gcd 𝐷) · 𝐹)) = ((𝐶 gcd 𝐷) · (𝐸 gcd 𝐹)))
172170, 61, 70, 171syl3anc 1371 . . . . . . . . . 10 (𝜑 → (((𝐶 gcd 𝐷) · 𝐸) gcd ((𝐶 gcd 𝐷) · 𝐹)) = ((𝐶 gcd 𝐷) · (𝐸 gcd 𝐹)))
173168, 169, 1723eqtr2rd 2779 . . . . . . . . 9 (𝜑 → ((𝐶 gcd 𝐷) · (𝐸 gcd 𝐹)) = ((𝐶 gcd 𝐷) · 1))
174166, 167, 75, 57, 173mulcanad 11845 . . . . . . . 8 (𝜑 → (𝐸 gcd 𝐹) = 1)
175 eqidd 2733 . . . . . . . 8 (𝜑 → ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝐹↑2)))
176 oveq1 7412 . . . . . . . . . . 11 (𝑥 = 𝐸 → (𝑥 gcd 𝑦) = (𝐸 gcd 𝑦))
177176eqeq1d 2734 . . . . . . . . . 10 (𝑥 = 𝐸 → ((𝑥 gcd 𝑦) = 1 ↔ (𝐸 gcd 𝑦) = 1))
178 oveq1 7412 . . . . . . . . . . . 12 (𝑥 = 𝐸 → (𝑥↑2) = (𝐸↑2))
179178oveq1d 7420 . . . . . . . . . . 11 (𝑥 = 𝐸 → ((𝑥↑2) + (𝑦↑2)) = ((𝐸↑2) + (𝑦↑2)))
180179eqeq2d 2743 . . . . . . . . . 10 (𝑥 = 𝐸 → (((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2)) ↔ ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝑦↑2))))
181177, 180anbi12d 631 . . . . . . . . 9 (𝑥 = 𝐸 → (((𝑥 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2))) ↔ ((𝐸 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝑦↑2)))))
182 oveq2 7413 . . . . . . . . . . 11 (𝑦 = 𝐹 → (𝐸 gcd 𝑦) = (𝐸 gcd 𝐹))
183182eqeq1d 2734 . . . . . . . . . 10 (𝑦 = 𝐹 → ((𝐸 gcd 𝑦) = 1 ↔ (𝐸 gcd 𝐹) = 1))
184 oveq1 7412 . . . . . . . . . . . 12 (𝑦 = 𝐹 → (𝑦↑2) = (𝐹↑2))
185184oveq2d 7421 . . . . . . . . . . 11 (𝑦 = 𝐹 → ((𝐸↑2) + (𝑦↑2)) = ((𝐸↑2) + (𝐹↑2)))
186185eqeq2d 2743 . . . . . . . . . 10 (𝑦 = 𝐹 → (((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝑦↑2)) ↔ ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝐹↑2))))
187183, 186anbi12d 631 . . . . . . . . 9 (𝑦 = 𝐹 → (((𝐸 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝑦↑2))) ↔ ((𝐸 gcd 𝐹) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝐹↑2)))))
188181, 187rspc2ev 3623 . . . . . . . 8 ((𝐸 ∈ ℤ ∧ 𝐹 ∈ ℤ ∧ ((𝐸 gcd 𝐹) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝐹↑2)))) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2))))
18961, 70, 174, 175, 188syl112anc 1374 . . . . . . 7 (𝜑 → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2))))
190 ovex 7438 . . . . . . . 8 ((𝐸↑2) + (𝐹↑2)) ∈ V
191 eqeq1 2736 . . . . . . . . . 10 (𝑧 = ((𝐸↑2) + (𝐹↑2)) → (𝑧 = ((𝑥↑2) + (𝑦↑2)) ↔ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2))))
192191anbi2d 629 . . . . . . . . 9 (𝑧 = ((𝐸↑2) + (𝐹↑2)) → (((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2))) ↔ ((𝑥 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2)))))
1931922rexbidv 3219 . . . . . . . 8 (𝑧 = ((𝐸↑2) + (𝐹↑2)) → (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2))) ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2)))))
194190, 193, 45elab2 3671 . . . . . . 7 (((𝐸↑2) + (𝐹↑2)) ∈ 𝑌 ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2))))
195189, 194sylibr 233 . . . . . 6 (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ 𝑌)
196164, 195sselid 3979 . . . . 5 (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℕ)
197196nngt0d 12257 . . . 4 (𝜑 → 0 < ((𝐸↑2) + (𝐹↑2)))
1985nngt0d 12257 . . . 4 (𝜑 → 0 < 𝑀)
199160, 161, 197, 198divgt0d 12145 . . 3 (𝜑 → 0 < (((𝐸↑2) + (𝐹↑2)) / 𝑀))
200 elnnz 12564 . . 3 ((((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℕ ↔ ((((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ ∧ 0 < (((𝐸↑2) + (𝐹↑2)) / 𝑀)))
201157, 199, 200sylanbrc 583 . 2 (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℕ)
202 prmnn 16607 . . . . . . . 8 (𝑝 ∈ ℙ → 𝑝 ∈ ℕ)
203202ad2antrl 726 . . . . . . 7 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∈ ℕ)
204203nnred 12223 . . . . . . . 8 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∈ ℝ)
205157adantr 481 . . . . . . . . 9 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ)
206205zred 12662 . . . . . . . 8 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℝ)
207 peano2zm 12601 . . . . . . . . . . 11 (𝑀 ∈ ℤ → (𝑀 − 1) ∈ ℤ)
2088, 207syl 17 . . . . . . . . . 10 (𝜑 → (𝑀 − 1) ∈ ℤ)
209208zred 12662 . . . . . . . . 9 (𝜑 → (𝑀 − 1) ∈ ℝ)
210209adantr 481 . . . . . . . 8 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (𝑀 − 1) ∈ ℝ)
211 simprr 771 . . . . . . . . 9 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))
212 prmz 16608 . . . . . . . . . . 11 (𝑝 ∈ ℙ → 𝑝 ∈ ℤ)
213212ad2antrl 726 . . . . . . . . . 10 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∈ ℤ)
214201adantr 481 . . . . . . . . . 10 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℕ)
215 dvdsle 16249 . . . . . . . . . 10 ((𝑝 ∈ ℤ ∧ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℕ) → (𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀) → 𝑝 ≤ (((𝐸↑2) + (𝐹↑2)) / 𝑀)))
216213, 214, 215syl2anc 584 . . . . . . . . 9 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀) → 𝑝 ≤ (((𝐸↑2) + (𝐹↑2)) / 𝑀)))
217211, 216mpd 15 . . . . . . . 8 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ≤ (((𝐸↑2) + (𝐹↑2)) / 𝑀))
218 zsqcl 14090 . . . . . . . . . . . . . . . 16 (𝑀 ∈ ℤ → (𝑀↑2) ∈ ℤ)
2198, 218syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝑀↑2) ∈ ℤ)
220219zred 12662 . . . . . . . . . . . . . 14 (𝜑 → (𝑀↑2) ∈ ℝ)
221220rehalfcld 12455 . . . . . . . . . . . . 13 (𝜑 → ((𝑀↑2) / 2) ∈ ℝ)
22216zred 12662 . . . . . . . . . . . . . . 15 (𝜑 → (𝐶↑2) ∈ ℝ)
22322zred 12662 . . . . . . . . . . . . . . 15 (𝜑 → (𝐷↑2) ∈ ℝ)
224222, 223readdcld 11239 . . . . . . . . . . . . . 14 (𝜑 → ((𝐶↑2) + (𝐷↑2)) ∈ ℝ)
225 1red 11211 . . . . . . . . . . . . . . . 16 (𝜑 → 1 ∈ ℝ)
22648nnsqcld 14203 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐶 gcd 𝐷)↑2) ∈ ℕ)
227226nnred 12223 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐶 gcd 𝐷)↑2) ∈ ℝ)
228150nn0ge0d 12531 . . . . . . . . . . . . . . . 16 (𝜑 → 0 ≤ ((𝐸↑2) + (𝐹↑2)))
229226nnge1d 12256 . . . . . . . . . . . . . . . 16 (𝜑 → 1 ≤ ((𝐶 gcd 𝐷)↑2))
230225, 227, 160, 228, 229lemul1ad 12149 . . . . . . . . . . . . . . 15 (𝜑 → (1 · ((𝐸↑2) + (𝐹↑2))) ≤ (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2))))
231150nn0cnd 12530 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℂ)
232231mullidd 11228 . . . . . . . . . . . . . . 15 (𝜑 → (1 · ((𝐸↑2) + (𝐹↑2))) = ((𝐸↑2) + (𝐹↑2)))
233230, 232, 933brtr3d 5178 . . . . . . . . . . . . . 14 (𝜑 → ((𝐸↑2) + (𝐹↑2)) ≤ ((𝐶↑2) + (𝐷↑2)))
234221rehalfcld 12455 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝑀↑2) / 2) / 2) ∈ ℝ)
23511, 5, 124sqlem7 16873 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐶↑2) ≤ (((𝑀↑2) / 2) / 2))
23617, 5, 184sqlem7 16873 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐷↑2) ≤ (((𝑀↑2) / 2) / 2))
237222, 223, 234, 234, 235, 236le2addd 11829 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐶↑2) + (𝐷↑2)) ≤ ((((𝑀↑2) / 2) / 2) + (((𝑀↑2) / 2) / 2)))
238221recnd 11238 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑀↑2) / 2) ∈ ℂ)
2392382halvesd 12454 . . . . . . . . . . . . . . 15 (𝜑 → ((((𝑀↑2) / 2) / 2) + (((𝑀↑2) / 2) / 2)) = ((𝑀↑2) / 2))
240237, 239breqtrd 5173 . . . . . . . . . . . . . 14 (𝜑 → ((𝐶↑2) + (𝐷↑2)) ≤ ((𝑀↑2) / 2))
241160, 224, 221, 233, 240letrd 11367 . . . . . . . . . . . . 13 (𝜑 → ((𝐸↑2) + (𝐹↑2)) ≤ ((𝑀↑2) / 2))
2425nnsqcld 14203 . . . . . . . . . . . . . . 15 (𝜑 → (𝑀↑2) ∈ ℕ)
243242nnrpd 13010 . . . . . . . . . . . . . 14 (𝜑 → (𝑀↑2) ∈ ℝ+)
244 rphalflt 12999 . . . . . . . . . . . . . 14 ((𝑀↑2) ∈ ℝ+ → ((𝑀↑2) / 2) < (𝑀↑2))
245243, 244syl 17 . . . . . . . . . . . . 13 (𝜑 → ((𝑀↑2) / 2) < (𝑀↑2))
246160, 221, 220, 241, 245lelttrd 11368 . . . . . . . . . . . 12 (𝜑 → ((𝐸↑2) + (𝐹↑2)) < (𝑀↑2))
2478zcnd 12663 . . . . . . . . . . . . 13 (𝜑𝑀 ∈ ℂ)
248247sqvald 14104 . . . . . . . . . . . 12 (𝜑 → (𝑀↑2) = (𝑀 · 𝑀))
249246, 248breqtrd 5173 . . . . . . . . . . 11 (𝜑 → ((𝐸↑2) + (𝐹↑2)) < (𝑀 · 𝑀))
250 ltdivmul 12085 . . . . . . . . . . . 12 ((((𝐸↑2) + (𝐹↑2)) ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (𝑀 ∈ ℝ ∧ 0 < 𝑀)) → ((((𝐸↑2) + (𝐹↑2)) / 𝑀) < 𝑀 ↔ ((𝐸↑2) + (𝐹↑2)) < (𝑀 · 𝑀)))
251160, 161, 161, 198, 250syl112anc 1374 . . . . . . . . . . 11 (𝜑 → ((((𝐸↑2) + (𝐹↑2)) / 𝑀) < 𝑀 ↔ ((𝐸↑2) + (𝐹↑2)) < (𝑀 · 𝑀)))
252249, 251mpbird 256 . . . . . . . . . 10 (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) < 𝑀)
253 zltlem1 12611 . . . . . . . . . . 11 (((((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((((𝐸↑2) + (𝐹↑2)) / 𝑀) < 𝑀 ↔ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ≤ (𝑀 − 1)))
254157, 8, 253syl2anc 584 . . . . . . . . . 10 (𝜑 → ((((𝐸↑2) + (𝐹↑2)) / 𝑀) < 𝑀 ↔ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ≤ (𝑀 − 1)))
255252, 254mpbid 231 . . . . . . . . 9 (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ≤ (𝑀 − 1))
256255adantr 481 . . . . . . . 8 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ≤ (𝑀 − 1))
257204, 206, 210, 217, 256letrd 11367 . . . . . . 7 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ≤ (𝑀 − 1))
258208adantr 481 . . . . . . . 8 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (𝑀 − 1) ∈ ℤ)
259 fznn 13565 . . . . . . . 8 ((𝑀 − 1) ∈ ℤ → (𝑝 ∈ (1...(𝑀 − 1)) ↔ (𝑝 ∈ ℕ ∧ 𝑝 ≤ (𝑀 − 1))))
260258, 259syl 17 . . . . . . 7 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (𝑝 ∈ (1...(𝑀 − 1)) ↔ (𝑝 ∈ ℕ ∧ 𝑝 ≤ (𝑀 − 1))))
261203, 257, 260mpbir2and 711 . . . . . 6 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∈ (1...(𝑀 − 1)))
262195adantr 481 . . . . . 6 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → ((𝐸↑2) + (𝐹↑2)) ∈ 𝑌)
263261, 262jca 512 . . . . 5 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (𝑝 ∈ (1...(𝑀 − 1)) ∧ ((𝐸↑2) + (𝐹↑2)) ∈ 𝑌))
26446adantr 481 . . . . 5 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → ∀𝑏 ∈ (1...(𝑀 − 1))∀𝑎𝑌 (𝑏𝑎𝑏𝑆))
265151adantr 481 . . . . . 6 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → ((𝐸↑2) + (𝐹↑2)) ∈ ℤ)
266 dvdsmul2 16218 . . . . . . . . 9 ((𝑀 ∈ ℤ ∧ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∥ (𝑀 · (((𝐸↑2) + (𝐹↑2)) / 𝑀)))
2678, 157, 266syl2anc 584 . . . . . . . 8 (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∥ (𝑀 · (((𝐸↑2) + (𝐹↑2)) / 𝑀)))
268231, 247, 107divcan2d 11988 . . . . . . . 8 (𝜑 → (𝑀 · (((𝐸↑2) + (𝐹↑2)) / 𝑀)) = ((𝐸↑2) + (𝐹↑2)))
269267, 268breqtrd 5173 . . . . . . 7 (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∥ ((𝐸↑2) + (𝐹↑2)))
270269adantr 481 . . . . . 6 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∥ ((𝐸↑2) + (𝐹↑2)))
271213, 205, 265, 211, 270dvdstrd 16234 . . . . 5 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∥ ((𝐸↑2) + (𝐹↑2)))
272 breq1 5150 . . . . . . 7 (𝑏 = 𝑝 → (𝑏𝑎𝑝𝑎))
273 eleq1w 2816 . . . . . . 7 (𝑏 = 𝑝 → (𝑏𝑆𝑝𝑆))
274272, 273imbi12d 344 . . . . . 6 (𝑏 = 𝑝 → ((𝑏𝑎𝑏𝑆) ↔ (𝑝𝑎𝑝𝑆)))
275 breq2 5151 . . . . . . 7 (𝑎 = ((𝐸↑2) + (𝐹↑2)) → (𝑝𝑎𝑝 ∥ ((𝐸↑2) + (𝐹↑2))))
276275imbi1d 341 . . . . . 6 (𝑎 = ((𝐸↑2) + (𝐹↑2)) → ((𝑝𝑎𝑝𝑆) ↔ (𝑝 ∥ ((𝐸↑2) + (𝐹↑2)) → 𝑝𝑆)))
277274, 276rspc2v 3621 . . . . 5 ((𝑝 ∈ (1...(𝑀 − 1)) ∧ ((𝐸↑2) + (𝐹↑2)) ∈ 𝑌) → (∀𝑏 ∈ (1...(𝑀 − 1))∀𝑎𝑌 (𝑏𝑎𝑏𝑆) → (𝑝 ∥ ((𝐸↑2) + (𝐹↑2)) → 𝑝𝑆)))
278263, 264, 271, 277syl3c 66 . . . 4 ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝𝑆)
279278expr 457 . . 3 ((𝜑𝑝 ∈ ℙ) → (𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀) → 𝑝𝑆))
280279ralrimiva 3146 . 2 (𝜑 → ∀𝑝 ∈ ℙ (𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀) → 𝑝𝑆))
281 inss1 4227 . . . . 5 (𝑆 ∩ ℕ) ⊆ 𝑆
282162, 281sstri 3990 . . . 4 𝑌𝑆
283282, 195sselid 3979 . . 3 (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ 𝑆)
284268, 283eqeltrd 2833 . 2 (𝜑 → (𝑀 · (((𝐸↑2) + (𝐹↑2)) / 𝑀)) ∈ 𝑆)
2851, 5, 201, 280, 2842sqlem6 26915 1 (𝜑𝑀𝑆)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396   = wceq 1541  wcel 2106  {cab 2709  wne 2940  wral 3061  wrex 3070  cin 3946   class class class wbr 5147  cmpt 5230  ran crn 5676  cfv 6540  (class class class)co 7405  cr 11105  0cc0 11106  1c1 11107   + caddc 11109   · cmul 11111   < clt 11244  cle 11245  cmin 11440   / cdiv 11867  cn 12208  2c2 12263  0cn0 12468  cz 12554  cuz 12818  +crp 12970  ...cfz 13480   mod cmo 13830  cexp 14023  abscabs 15177  cdvds 16193   gcd cgcd 16431  cprime 16604  ℤ[i]cgz 16858
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7852  df-1st 7971  df-2nd 7972  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-1o 8462  df-2o 8463  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-sup 9433  df-inf 9434  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-div 11868  df-nn 12209  df-2 12271  df-3 12272  df-n0 12469  df-z 12555  df-uz 12819  df-rp 12971  df-fz 13481  df-fl 13753  df-mod 13831  df-seq 13963  df-exp 14024  df-cj 15042  df-re 15043  df-im 15044  df-sqrt 15178  df-abs 15179  df-dvds 16194  df-gcd 16432  df-prm 16605  df-gz 16859
This theorem is referenced by:  2sqlem9  26919
  Copyright terms: Public domain W3C validator