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

 Description: Lemma for lgsquad 24908. Count the members of 𝑆 with odd coordinates. (Contributed by Mario Carneiro, 19-Jun-2015.)
Hypotheses
Ref Expression
lgseisen.1 (𝜑𝑃 ∈ (ℙ ∖ {2}))
lgseisen.2 (𝜑𝑄 ∈ (ℙ ∖ {2}))
lgseisen.3 (𝜑𝑃𝑄)
lgsquad.4 𝑀 = ((𝑃 − 1) / 2)
lgsquad.5 𝑁 = ((𝑄 − 1) / 2)
lgsquad.6 𝑆 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))}
Assertion
Ref Expression
lgsquadlem1 (𝜑 → (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (-1↑(#‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})))
Distinct variable groups:   𝑥,𝑢,𝑦,𝑧,𝑃   𝜑,𝑢,𝑥,𝑦,𝑧   𝑢,𝑀,𝑦,𝑧   𝑢,𝑁,𝑥,𝑦,𝑧   𝑢,𝑄,𝑥,𝑦,𝑧   𝑢,𝑆,𝑥,𝑧   𝑥,𝑀   𝑦,𝑆

Dummy variables 𝑛 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 neg1cn 11001 . . . 4 -1 ∈ ℂ
21a1i 11 . . 3 (𝜑 → -1 ∈ ℂ)
3 neg1ne0 11003 . . . 4 -1 ≠ 0
43a1i 11 . . 3 (𝜑 → -1 ≠ 0)
5 fzfid 12634 . . . 4 (𝜑 → (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∈ Fin)
6 lgseisen.2 . . . . . . . . . 10 (𝜑𝑄 ∈ (ℙ ∖ {2}))
7 eldifi 3694 . . . . . . . . . 10 (𝑄 ∈ (ℙ ∖ {2}) → 𝑄 ∈ ℙ)
8 prmnn 15226 . . . . . . . . . 10 (𝑄 ∈ ℙ → 𝑄 ∈ ℕ)
96, 7, 83syl 18 . . . . . . . . 9 (𝜑𝑄 ∈ ℕ)
109nnred 10912 . . . . . . . 8 (𝜑𝑄 ∈ ℝ)
11 lgseisen.1 . . . . . . . . 9 (𝜑𝑃 ∈ (ℙ ∖ {2}))
12 eldifi 3694 . . . . . . . . 9 (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℙ)
13 prmnn 15226 . . . . . . . . 9 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
1411, 12, 133syl 18 . . . . . . . 8 (𝜑𝑃 ∈ ℕ)
1510, 14nndivred 10946 . . . . . . 7 (𝜑 → (𝑄 / 𝑃) ∈ ℝ)
1615adantr 480 . . . . . 6 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 / 𝑃) ∈ ℝ)
17 2z 11286 . . . . . . . 8 2 ∈ ℤ
18 elfzelz 12213 . . . . . . . . 9 (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) → 𝑢 ∈ ℤ)
1918adantl 481 . . . . . . . 8 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ∈ ℤ)
20 zmulcl 11303 . . . . . . . 8 ((2 ∈ ℤ ∧ 𝑢 ∈ ℤ) → (2 · 𝑢) ∈ ℤ)
2117, 19, 20sylancr 694 . . . . . . 7 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ∈ ℤ)
2221zred 11358 . . . . . 6 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ∈ ℝ)
2316, 22remulcld 9949 . . . . 5 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ)
2423flcld 12461 . . . 4 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ)
255, 24fsumzcl 14313 . . 3 (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ)
262, 4, 25expclzd 12875 . 2 (𝜑 → (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℂ)
27 fzfid 12634 . . . . . . 7 (𝜑 → (1...𝑀) ∈ Fin)
28 fzfid 12634 . . . . . . 7 (𝜑 → (1...𝑁) ∈ Fin)
29 xpfi 8116 . . . . . . 7 (((1...𝑀) ∈ Fin ∧ (1...𝑁) ∈ Fin) → ((1...𝑀) × (1...𝑁)) ∈ Fin)
3027, 28, 29syl2anc 691 . . . . . 6 (𝜑 → ((1...𝑀) × (1...𝑁)) ∈ Fin)
31 lgsquad.6 . . . . . . 7 𝑆 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))}
32 opabssxp 5116 . . . . . . 7 {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} ⊆ ((1...𝑀) × (1...𝑁))
3331, 32eqsstri 3598 . . . . . 6 𝑆 ⊆ ((1...𝑀) × (1...𝑁))
34 ssfi 8065 . . . . . 6 ((((1...𝑀) × (1...𝑁)) ∈ Fin ∧ 𝑆 ⊆ ((1...𝑀) × (1...𝑁))) → 𝑆 ∈ Fin)
3530, 33, 34sylancl 693 . . . . 5 (𝜑𝑆 ∈ Fin)
36 ssrab2 3650 . . . . 5 {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)} ⊆ 𝑆
37 ssfi 8065 . . . . 5 ((𝑆 ∈ Fin ∧ {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)} ⊆ 𝑆) → {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)} ∈ Fin)
3835, 36, 37sylancl 693 . . . 4 (𝜑 → {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)} ∈ Fin)
39 hashcl 13009 . . . 4 ({𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)} ∈ Fin → (#‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) ∈ ℕ0)
4038, 39syl 17 . . 3 (𝜑 → (#‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) ∈ ℕ0)
41 expcl 12740 . . 3 ((-1 ∈ ℂ ∧ (#‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) ∈ ℕ0) → (-1↑(#‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) ∈ ℂ)
421, 40, 41sylancr 694 . 2 (𝜑 → (-1↑(#‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) ∈ ℂ)
4340nn0zd 11356 . . 3 (𝜑 → (#‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) ∈ ℤ)
442, 4, 43expne0d 12876 . 2 (𝜑 → (-1↑(#‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) ≠ 0)
4542, 44recidd 10675 . . . 4 (𝜑 → ((-1↑(#‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) · (1 / (-1↑(#‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})))) = 1)
46 1div1e1 10596 . . . . . . . . 9 (1 / 1) = 1
4746negeqi 10153 . . . . . . . 8 -(1 / 1) = -1
48 ax-1cn 9873 . . . . . . . . 9 1 ∈ ℂ
49 ax-1ne0 9884 . . . . . . . . 9 1 ≠ 0
50 divneg2 10628 . . . . . . . . 9 ((1 ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ≠ 0) → -(1 / 1) = (1 / -1))
5148, 48, 49, 50mp3an 1416 . . . . . . . 8 -(1 / 1) = (1 / -1)
5247, 51eqtr3i 2634 . . . . . . 7 -1 = (1 / -1)
5352oveq1i 6559 . . . . . 6 (-1↑(#‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) = ((1 / -1)↑(#‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))
542, 4, 43exprecd 12878 . . . . . 6 (𝜑 → ((1 / -1)↑(#‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) = (1 / (-1↑(#‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))))
5553, 54syl5eq 2656 . . . . 5 (𝜑 → (-1↑(#‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) = (1 / (-1↑(#‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))))
5655oveq2d 6565 . . . 4 (𝜑 → ((-1↑(#‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) · (-1↑(#‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))) = ((-1↑(#‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) · (1 / (-1↑(#‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})))))
5735adantr 480 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑆 ∈ Fin)
58 ssrab2 3650 . . . . . . . . . . . 12 {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} ⊆ 𝑆
59 ssfi 8065 . . . . . . . . . . . 12 ((𝑆 ∈ Fin ∧ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} ⊆ 𝑆) → {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} ∈ Fin)
6057, 58, 59sylancl 693 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} ∈ Fin)
61 fveq2 6103 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = 𝑣 → (1st𝑧) = (1st𝑣))
6261eqeq1d 2612 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑣 → ((1st𝑧) = (𝑃 − (2 · 𝑢)) ↔ (1st𝑣) = (𝑃 − (2 · 𝑢))))
6362elrab 3331 . . . . . . . . . . . . . . . . . . 19 (𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} ↔ (𝑣𝑆 ∧ (1st𝑣) = (𝑃 − (2 · 𝑢))))
6463simprbi 479 . . . . . . . . . . . . . . . . . 18 (𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} → (1st𝑣) = (𝑃 − (2 · 𝑢)))
6564ad2antll 761 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → (1st𝑣) = (𝑃 − (2 · 𝑢)))
6665oveq2d 6565 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → (𝑃 − (1st𝑣)) = (𝑃 − (𝑃 − (2 · 𝑢))))
6714adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℕ)
6867nncnd 10913 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℂ)
6968adantrr 749 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → 𝑃 ∈ ℂ)
7021zcnd 11359 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ∈ ℂ)
7170adantrr 749 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → (2 · 𝑢) ∈ ℂ)
7269, 71nncand 10276 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → (𝑃 − (𝑃 − (2 · 𝑢))) = (2 · 𝑢))
7366, 72eqtrd 2644 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → (𝑃 − (1st𝑣)) = (2 · 𝑢))
7473oveq1d 6564 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → ((𝑃 − (1st𝑣)) / 2) = ((2 · 𝑢) / 2))
7519zcnd 11359 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ∈ ℂ)
7675adantrr 749 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → 𝑢 ∈ ℂ)
77 2cnd 10970 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → 2 ∈ ℂ)
78 2ne0 10990 . . . . . . . . . . . . . . . 16 2 ≠ 0
7978a1i 11 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → 2 ≠ 0)
8076, 77, 79divcan3d 10685 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → ((2 · 𝑢) / 2) = 𝑢)
8174, 80eqtrd 2644 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → ((𝑃 − (1st𝑣)) / 2) = 𝑢)
8281ralrimivva 2954 . . . . . . . . . . . 12 (𝜑 → ∀𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)∀𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} ((𝑃 − (1st𝑣)) / 2) = 𝑢)
83 invdisj 4571 . . . . . . . . . . . 12 (∀𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)∀𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} ((𝑃 − (1st𝑣)) / 2) = 𝑢Disj 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})
8482, 83syl 17 . . . . . . . . . . 11 (𝜑Disj 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})
855, 60, 84hashiun 14395 . . . . . . . . . 10 (𝜑 → (#‘ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))}) = Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(#‘{𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))}))
86 iunrab 4503 . . . . . . . . . . . 12 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} = {𝑧𝑆 ∣ ∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1st𝑧) = (𝑃 − (2 · 𝑢))}
87 eldifsni 4261 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ≠ 2)
8811, 87syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑃 ≠ 2)
8988necomd 2837 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 2 ≠ 𝑃)
9089neneqd 2787 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ¬ 2 = 𝑃)
9190ad2antrr 758 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ¬ 2 = 𝑃)
92 uzid 11578 . . . . . . . . . . . . . . . . . . . . 21 (2 ∈ ℤ → 2 ∈ (ℤ‘2))
9317, 92ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 2 ∈ (ℤ‘2)
9411, 12syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑃 ∈ ℙ)
9594ad2antrr 758 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℙ)
96 dvdsprm 15253 . . . . . . . . . . . . . . . . . . . 20 ((2 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) → (2 ∥ 𝑃 ↔ 2 = 𝑃))
9793, 95, 96sylancr 694 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 ∥ 𝑃 ↔ 2 = 𝑃))
9891, 97mtbird 314 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ¬ 2 ∥ 𝑃)
9914ad2antrr 758 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℕ)
10099nncnd 10913 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℂ)
10121adantlr 747 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ∈ ℤ)
102101zcnd 11359 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ∈ ℂ)
103100, 102npcand 10275 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) + (2 · 𝑢)) = 𝑃)
104103breq2d 4595 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 ∥ ((𝑃 − (2 · 𝑢)) + (2 · 𝑢)) ↔ 2 ∥ 𝑃))
10598, 104mtbird 314 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ¬ 2 ∥ ((𝑃 − (2 · 𝑢)) + (2 · 𝑢)))
10618adantl 481 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ∈ ℤ)
107 dvdsmul1 14841 . . . . . . . . . . . . . . . . . . 19 ((2 ∈ ℤ ∧ 𝑢 ∈ ℤ) → 2 ∥ (2 · 𝑢))
10817, 106, 107sylancr 694 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 2 ∥ (2 · 𝑢))
10917a1i 11 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 2 ∈ ℤ)
11099nnzd 11357 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℤ)
111110, 101zsubcld 11363 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − (2 · 𝑢)) ∈ ℤ)
112 dvds2add 14853 . . . . . . . . . . . . . . . . . . 19 ((2 ∈ ℤ ∧ (𝑃 − (2 · 𝑢)) ∈ ℤ ∧ (2 · 𝑢) ∈ ℤ) → ((2 ∥ (𝑃 − (2 · 𝑢)) ∧ 2 ∥ (2 · 𝑢)) → 2 ∥ ((𝑃 − (2 · 𝑢)) + (2 · 𝑢))))
113109, 111, 101, 112syl3anc 1318 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 ∥ (𝑃 − (2 · 𝑢)) ∧ 2 ∥ (2 · 𝑢)) → 2 ∥ ((𝑃 − (2 · 𝑢)) + (2 · 𝑢))))
114108, 113mpan2d 706 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 ∥ (𝑃 − (2 · 𝑢)) → 2 ∥ ((𝑃 − (2 · 𝑢)) + (2 · 𝑢))))
115105, 114mtod 188 . . . . . . . . . . . . . . . 16 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ¬ 2 ∥ (𝑃 − (2 · 𝑢)))
116 breq2 4587 . . . . . . . . . . . . . . . . 17 ((1st𝑧) = (𝑃 − (2 · 𝑢)) → (2 ∥ (1st𝑧) ↔ 2 ∥ (𝑃 − (2 · 𝑢))))
117116notbid 307 . . . . . . . . . . . . . . . 16 ((1st𝑧) = (𝑃 − (2 · 𝑢)) → (¬ 2 ∥ (1st𝑧) ↔ ¬ 2 ∥ (𝑃 − (2 · 𝑢))))
118115, 117syl5ibrcom 236 . . . . . . . . . . . . . . 15 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((1st𝑧) = (𝑃 − (2 · 𝑢)) → ¬ 2 ∥ (1st𝑧)))
119118rexlimdva 3013 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑆) → (∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1st𝑧) = (𝑃 − (2 · 𝑢)) → ¬ 2 ∥ (1st𝑧)))
120 simpr 476 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧𝑆) → 𝑧𝑆)
12133, 120sseldi 3566 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧𝑆) → 𝑧 ∈ ((1...𝑀) × (1...𝑁)))
122 xp1st 7089 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ ((1...𝑀) × (1...𝑁)) → (1st𝑧) ∈ (1...𝑀))
123121, 122syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑧𝑆) → (1st𝑧) ∈ (1...𝑀))
124 elfzelz 12213 . . . . . . . . . . . . . . . 16 ((1st𝑧) ∈ (1...𝑀) → (1st𝑧) ∈ ℤ)
125 odd2np1 14903 . . . . . . . . . . . . . . . 16 ((1st𝑧) ∈ ℤ → (¬ 2 ∥ (1st𝑧) ↔ ∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = (1st𝑧)))
126123, 124, 1253syl 18 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑆) → (¬ 2 ∥ (1st𝑧) ↔ ∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = (1st𝑧)))
127 lgsquad.4 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑀 = ((𝑃 − 1) / 2)
128 oddprm 15353 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑃 ∈ (ℙ ∖ {2}) → ((𝑃 − 1) / 2) ∈ ℕ)
12911, 128syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝑃 − 1) / 2) ∈ ℕ)
130127, 129syl5eqel 2692 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑀 ∈ ℕ)
131130nnred 10912 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑀 ∈ ℝ)
132131ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑀 ∈ ℝ)
133132rehalfcld 11156 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑀 / 2) ∈ ℝ)
134 reflcl 12459 . . . . . . . . . . . . . . . . . . . . 21 ((𝑀 / 2) ∈ ℝ → (⌊‘(𝑀 / 2)) ∈ ℝ)
135133, 134syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (⌊‘(𝑀 / 2)) ∈ ℝ)
136130ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑀 ∈ ℕ)
137136nnzd 11357 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑀 ∈ ℤ)
138 simprl 790 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑛 ∈ ℤ)
139137, 138zsubcld 11363 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑀𝑛) ∈ ℤ)
140139zred 11358 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑀𝑛) ∈ ℝ)
141 flle 12462 . . . . . . . . . . . . . . . . . . . . 21 ((𝑀 / 2) ∈ ℝ → (⌊‘(𝑀 / 2)) ≤ (𝑀 / 2))
142133, 141syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (⌊‘(𝑀 / 2)) ≤ (𝑀 / 2))
143 zre 11258 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ ℤ → 𝑛 ∈ ℝ)
144143ad2antrl 760 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑛 ∈ ℝ)
145 simprr 792 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((2 · 𝑛) + 1) = (1st𝑧))
146123adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (1st𝑧) ∈ (1...𝑀))
147145, 146eqeltrd 2688 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((2 · 𝑛) + 1) ∈ (1...𝑀))
148 elfzle2 12216 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((2 · 𝑛) + 1) ∈ (1...𝑀) → ((2 · 𝑛) + 1) ≤ 𝑀)
149147, 148syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((2 · 𝑛) + 1) ≤ 𝑀)
150 zmulcl 11303 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((2 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (2 · 𝑛) ∈ ℤ)
15117, 138, 150sylancr 694 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (2 · 𝑛) ∈ ℤ)
152 zltp1le 11304 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((2 · 𝑛) ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((2 · 𝑛) < 𝑀 ↔ ((2 · 𝑛) + 1) ≤ 𝑀))
153151, 137, 152syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((2 · 𝑛) < 𝑀 ↔ ((2 · 𝑛) + 1) ≤ 𝑀))
154149, 153mpbird 246 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (2 · 𝑛) < 𝑀)
155 2re 10967 . . . . . . . . . . . . . . . . . . . . . . . . 25 2 ∈ ℝ
156155a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 2 ∈ ℝ)
157 2pos 10989 . . . . . . . . . . . . . . . . . . . . . . . . 25 0 < 2
158157a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 0 < 2)
159 ltmuldiv2 10776 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 𝑛) < 𝑀𝑛 < (𝑀 / 2)))
160144, 132, 156, 158, 159syl112anc 1322 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((2 · 𝑛) < 𝑀𝑛 < (𝑀 / 2)))
161154, 160mpbid 221 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑛 < (𝑀 / 2))
162133recnd 9947 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑀 / 2) ∈ ℂ)
163162, 162pncan2d 10273 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (((𝑀 / 2) + (𝑀 / 2)) − (𝑀 / 2)) = (𝑀 / 2))
164130nncnd 10913 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝑀 ∈ ℂ)
165164ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑀 ∈ ℂ)
1661652halvesd 11155 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((𝑀 / 2) + (𝑀 / 2)) = 𝑀)
167166oveq1d 6564 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (((𝑀 / 2) + (𝑀 / 2)) − (𝑀 / 2)) = (𝑀 − (𝑀 / 2)))
168163, 167eqtr3d 2646 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑀 / 2) = (𝑀 − (𝑀 / 2)))
169161, 168breqtrd 4609 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑛 < (𝑀 − (𝑀 / 2)))
170144, 132, 133, 169ltsub13d 10512 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑀 / 2) < (𝑀𝑛))
171135, 133, 140, 142, 170lelttrd 10074 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (⌊‘(𝑀 / 2)) < (𝑀𝑛))
172133flcld 12461 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (⌊‘(𝑀 / 2)) ∈ ℤ)
173 zltp1le 11304 . . . . . . . . . . . . . . . . . . . 20 (((⌊‘(𝑀 / 2)) ∈ ℤ ∧ (𝑀𝑛) ∈ ℤ) → ((⌊‘(𝑀 / 2)) < (𝑀𝑛) ↔ ((⌊‘(𝑀 / 2)) + 1) ≤ (𝑀𝑛)))
174172, 139, 173syl2anc 691 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((⌊‘(𝑀 / 2)) < (𝑀𝑛) ↔ ((⌊‘(𝑀 / 2)) + 1) ≤ (𝑀𝑛)))
175171, 174mpbid 221 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((⌊‘(𝑀 / 2)) + 1) ≤ (𝑀𝑛))
176 2t0e0 11060 . . . . . . . . . . . . . . . . . . . . 21 (2 · 0) = 0
177 2cn 10968 . . . . . . . . . . . . . . . . . . . . . . . . 25 2 ∈ ℂ
178 zcn 11259 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 ∈ ℤ → 𝑛 ∈ ℂ)
179178ad2antrl 760 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑛 ∈ ℂ)
180 mulcl 9899 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((2 ∈ ℂ ∧ 𝑛 ∈ ℂ) → (2 · 𝑛) ∈ ℂ)
181177, 179, 180sylancr 694 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (2 · 𝑛) ∈ ℂ)
182 pncan 10166 . . . . . . . . . . . . . . . . . . . . . . . 24 (((2 · 𝑛) ∈ ℂ ∧ 1 ∈ ℂ) → (((2 · 𝑛) + 1) − 1) = (2 · 𝑛))
183181, 48, 182sylancl 693 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (((2 · 𝑛) + 1) − 1) = (2 · 𝑛))
184 elfznn 12241 . . . . . . . . . . . . . . . . . . . . . . . 24 (((2 · 𝑛) + 1) ∈ (1...𝑀) → ((2 · 𝑛) + 1) ∈ ℕ)
185 nnm1nn0 11211 . . . . . . . . . . . . . . . . . . . . . . . 24 (((2 · 𝑛) + 1) ∈ ℕ → (((2 · 𝑛) + 1) − 1) ∈ ℕ0)
186147, 184, 1853syl 18 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (((2 · 𝑛) + 1) − 1) ∈ ℕ0)
187183, 186eqeltrrd 2689 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (2 · 𝑛) ∈ ℕ0)
188187nn0ge0d 11231 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 0 ≤ (2 · 𝑛))
189176, 188syl5eqbr 4618 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (2 · 0) ≤ (2 · 𝑛))
190 0red 9920 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 0 ∈ ℝ)
191 lemul2 10755 . . . . . . . . . . . . . . . . . . . . 21 ((0 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (0 ≤ 𝑛 ↔ (2 · 0) ≤ (2 · 𝑛)))
192190, 144, 156, 158, 191syl112anc 1322 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (0 ≤ 𝑛 ↔ (2 · 0) ≤ (2 · 𝑛)))
193189, 192mpbird 246 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 0 ≤ 𝑛)
194132, 144subge02d 10498 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (0 ≤ 𝑛 ↔ (𝑀𝑛) ≤ 𝑀))
195193, 194mpbid 221 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑀𝑛) ≤ 𝑀)
196172peano2zd 11361 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((⌊‘(𝑀 / 2)) + 1) ∈ ℤ)
197 elfz 12203 . . . . . . . . . . . . . . . . . . 19 (((𝑀𝑛) ∈ ℤ ∧ ((⌊‘(𝑀 / 2)) + 1) ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑀𝑛) ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ↔ (((⌊‘(𝑀 / 2)) + 1) ≤ (𝑀𝑛) ∧ (𝑀𝑛) ≤ 𝑀)))
198139, 196, 137, 197syl3anc 1318 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((𝑀𝑛) ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ↔ (((⌊‘(𝑀 / 2)) + 1) ≤ (𝑀𝑛) ∧ (𝑀𝑛) ≤ 𝑀)))
199175, 195, 198mpbir2and 959 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑀𝑛) ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀))
20094ad2antrr 758 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑃 ∈ ℙ)
201200, 13syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑃 ∈ ℕ)
202201nncnd 10913 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑃 ∈ ℂ)
203 peano2cn 10087 . . . . . . . . . . . . . . . . . . . 20 ((2 · 𝑛) ∈ ℂ → ((2 · 𝑛) + 1) ∈ ℂ)
204181, 203syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((2 · 𝑛) + 1) ∈ ℂ)
205202, 204nncand 10276 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑃 − (𝑃 − ((2 · 𝑛) + 1))) = ((2 · 𝑛) + 1))
206 1cnd 9935 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 1 ∈ ℂ)
207202, 181, 206sub32d 10303 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((𝑃 − (2 · 𝑛)) − 1) = ((𝑃 − 1) − (2 · 𝑛)))
208202, 181, 206subsub4d 10302 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((𝑃 − (2 · 𝑛)) − 1) = (𝑃 − ((2 · 𝑛) + 1)))
209 2cnd 10970 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 2 ∈ ℂ)
210209, 165, 179subdid 10365 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (2 · (𝑀𝑛)) = ((2 · 𝑀) − (2 · 𝑛)))
211127oveq2i 6560 . . . . . . . . . . . . . . . . . . . . . . 23 (2 · 𝑀) = (2 · ((𝑃 − 1) / 2))
21214nnzd 11357 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝑃 ∈ ℤ)
213212ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑃 ∈ ℤ)
214 peano2zm 11297 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑃 ∈ ℤ → (𝑃 − 1) ∈ ℤ)
215213, 214syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑃 − 1) ∈ ℤ)
216215zcnd 11359 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑃 − 1) ∈ ℂ)
21778a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 2 ≠ 0)
218216, 209, 217divcan2d 10682 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (2 · ((𝑃 − 1) / 2)) = (𝑃 − 1))
219211, 218syl5eq 2656 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (2 · 𝑀) = (𝑃 − 1))
220219oveq1d 6564 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((2 · 𝑀) − (2 · 𝑛)) = ((𝑃 − 1) − (2 · 𝑛)))
221210, 220eqtr2d 2645 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((𝑃 − 1) − (2 · 𝑛)) = (2 · (𝑀𝑛)))
222207, 208, 2213eqtr3d 2652 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑃 − ((2 · 𝑛) + 1)) = (2 · (𝑀𝑛)))
223222oveq2d 6565 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑃 − (𝑃 − ((2 · 𝑛) + 1))) = (𝑃 − (2 · (𝑀𝑛))))
224205, 223, 1453eqtr3rd 2653 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (1st𝑧) = (𝑃 − (2 · (𝑀𝑛))))
225 oveq2 6557 . . . . . . . . . . . . . . . . . . . 20 (𝑢 = (𝑀𝑛) → (2 · 𝑢) = (2 · (𝑀𝑛)))
226225oveq2d 6565 . . . . . . . . . . . . . . . . . . 19 (𝑢 = (𝑀𝑛) → (𝑃 − (2 · 𝑢)) = (𝑃 − (2 · (𝑀𝑛))))
227226eqeq2d 2620 . . . . . . . . . . . . . . . . . 18 (𝑢 = (𝑀𝑛) → ((1st𝑧) = (𝑃 − (2 · 𝑢)) ↔ (1st𝑧) = (𝑃 − (2 · (𝑀𝑛)))))
228227rspcev 3282 . . . . . . . . . . . . . . . . 17 (((𝑀𝑛) ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ (1st𝑧) = (𝑃 − (2 · (𝑀𝑛)))) → ∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1st𝑧) = (𝑃 − (2 · 𝑢)))
229199, 224, 228syl2anc 691 . . . . . . . . . . . . . . . 16 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1st𝑧) = (𝑃 − (2 · 𝑢)))
230229rexlimdvaa 3014 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑆) → (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = (1st𝑧) → ∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1st𝑧) = (𝑃 − (2 · 𝑢))))
231126, 230sylbid 229 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑆) → (¬ 2 ∥ (1st𝑧) → ∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1st𝑧) = (𝑃 − (2 · 𝑢))))
232119, 231impbid 201 . . . . . . . . . . . . 13 ((𝜑𝑧𝑆) → (∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1st𝑧) = (𝑃 − (2 · 𝑢)) ↔ ¬ 2 ∥ (1st𝑧)))
233232rabbidva 3163 . . . . . . . . . . . 12 (𝜑 → {𝑧𝑆 ∣ ∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1st𝑧) = (𝑃 − (2 · 𝑢))} = {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})
23486, 233syl5eq 2656 . . . . . . . . . . 11 (𝜑 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} = {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})
235234fveq2d 6107 . . . . . . . . . 10 (𝜑 → (#‘ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))}) = (#‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))
23631relopabi 5167 . . . . . . . . . . . . . . 15 Rel 𝑆
237 relss 5129 . . . . . . . . . . . . . . 15 ({𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} ⊆ 𝑆 → (Rel 𝑆 → Rel {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))}))
23858, 236, 237mp2 9 . . . . . . . . . . . . . 14 Rel {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))}
239 relxp 5150 . . . . . . . . . . . . . 14 Rel ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
24031eleq2i 2680 . . . . . . . . . . . . . . . . . 18 (⟨𝑥, 𝑦⟩ ∈ 𝑆 ↔ ⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))})
241 opabid 4907 . . . . . . . . . . . . . . . . . 18 (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} ↔ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))
242240, 241bitri 263 . . . . . . . . . . . . . . . . 17 (⟨𝑥, 𝑦⟩ ∈ 𝑆 ↔ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))
243 anass 679 . . . . . . . . . . . . . . . . . . 19 (((𝑦 ∈ ℕ ∧ 𝑦𝑁) ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄)) ↔ (𝑦 ∈ ℕ ∧ (𝑦𝑁 ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄))))
24424peano2zd 11361 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ∈ ℤ)
245244zred 11358 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ∈ ℝ)
246245adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ∈ ℝ)
24710ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈ ℝ)
248 nnre 10904 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
249248adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ ℝ)
250 lesub 10386 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ∈ ℝ ∧ 𝑄 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ≤ (𝑄𝑦) ↔ 𝑦 ≤ (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1))))
251246, 247, 249, 250syl3anc 1318 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ≤ (𝑄𝑦) ↔ 𝑦 ≤ (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1))))
25210adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑄 ∈ ℝ)
253252recnd 9947 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑄 ∈ ℂ)
25468, 253mulcomd 9940 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 · 𝑄) = (𝑄 · 𝑃))
25570, 253mulcomd 9940 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑢) · 𝑄) = (𝑄 · (2 · 𝑢)))
25667nnne0d 10942 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ≠ 0)
257253, 68, 256divcan1d 10681 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 𝑃) · 𝑃) = 𝑄)
258257oveq1d 6564 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑄 / 𝑃) · 𝑃) · (2 · 𝑢)) = (𝑄 · (2 · 𝑢)))
25916recnd 9947 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 / 𝑃) ∈ ℂ)
260259, 68, 70mul32d 10125 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑄 / 𝑃) · 𝑃) · (2 · 𝑢)) = (((𝑄 / 𝑃) · (2 · 𝑢)) · 𝑃))
261255, 258, 2603eqtr2d 2650 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑢) · 𝑄) = (((𝑄 / 𝑃) · (2 · 𝑢)) · 𝑃))
262254, 261oveq12d 6567 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 · 𝑄) − ((2 · 𝑢) · 𝑄)) = ((𝑄 · 𝑃) − (((𝑄 / 𝑃) · (2 · 𝑢)) · 𝑃)))
26368, 70, 253subdird 10366 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) · 𝑄) = ((𝑃 · 𝑄) − ((2 · 𝑢) · 𝑄)))
26423recnd 9947 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℂ)
265253, 264, 68subdird 10366 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃) = ((𝑄 · 𝑃) − (((𝑄 / 𝑃) · (2 · 𝑢)) · 𝑃)))
266262, 263, 2653eqtr4d 2654 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) · 𝑄) = ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃))
267266adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑃 − (2 · 𝑢)) · 𝑄) = ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃))
268267breq2d 4595 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄) ↔ (𝑦 · 𝑃) < ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃)))
26923adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ)
270247, 269resubcld 10337 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℝ)
27167adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℕ)
272271nnred 10912 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℝ)
273271nngt0d 10941 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 0 < 𝑃)
274 ltmul1 10752 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦 ∈ ℝ ∧ (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℝ ∧ (𝑃 ∈ ℝ ∧ 0 < 𝑃)) → (𝑦 < (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ↔ (𝑦 · 𝑃) < ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃)))
275249, 270, 272, 273, 274syl112anc 1322 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑦 < (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ↔ (𝑦 · 𝑃) < ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃)))
276 ltsub13 10388 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦 ∈ ℝ ∧ 𝑄 ∈ ℝ ∧ ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ) → (𝑦 < (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ↔ ((𝑄 / 𝑃) · (2 · 𝑢)) < (𝑄𝑦)))
277249, 247, 269, 276syl3anc 1318 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑦 < (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ↔ ((𝑄 / 𝑃) · (2 · 𝑢)) < (𝑄𝑦)))
278268, 275, 2773bitr2d 295 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄) ↔ ((𝑄 / 𝑃) · (2 · 𝑢)) < (𝑄𝑦)))
2799adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑄 ∈ ℕ)
280279nnzd 11357 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑄 ∈ ℤ)
281 nnz 11276 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 ∈ ℕ → 𝑦 ∈ ℤ)
282 zsubcl 11296 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑄 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑄𝑦) ∈ ℤ)
283280, 281, 282syl2an 493 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑄𝑦) ∈ ℤ)
284 fllt 12469 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ ∧ (𝑄𝑦) ∈ ℤ) → (((𝑄 / 𝑃) · (2 · 𝑢)) < (𝑄𝑦) ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < (𝑄𝑦)))
285269, 283, 284syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (((𝑄 / 𝑃) · (2 · 𝑢)) < (𝑄𝑦) ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < (𝑄𝑦)))
28624adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ)
287 zltp1le 11304 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ ∧ (𝑄𝑦) ∈ ℤ) → ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < (𝑄𝑦) ↔ ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ≤ (𝑄𝑦)))
288286, 283, 287syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < (𝑄𝑦) ↔ ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ≤ (𝑄𝑦)))
289278, 285, 2883bitrd 293 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄) ↔ ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ≤ (𝑄𝑦)))
290 lgsquad.5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 𝑁 = ((𝑄 − 1) / 2)
291290oveq2i 6560 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (2 · 𝑁) = (2 · ((𝑄 − 1) / 2))
292 peano2rem 10227 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑄 ∈ ℝ → (𝑄 − 1) ∈ ℝ)
293252, 292syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 − 1) ∈ ℝ)
294293recnd 9947 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 − 1) ∈ ℂ)
295 2cnd 10970 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 2 ∈ ℂ)
29678a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 2 ≠ 0)
297294, 295, 296divcan2d 10682 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · ((𝑄 − 1) / 2)) = (𝑄 − 1))
298291, 297syl5eq 2656 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) = (𝑄 − 1))
299298oveq1d 6564 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = ((𝑄 − 1) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
300 1cnd 9935 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 1 ∈ ℂ)
30124zcnd 11359 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℂ)
302253, 300, 301sub32d 10303 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 − 1) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = ((𝑄 − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) − 1))
303253, 301, 300subsub4d 10302 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) − 1) = (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1)))
304299, 302, 3033eqtrd 2648 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1)))
305304adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1)))
306305breq2d 4595 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ↔ 𝑦 ≤ (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1))))
307251, 289, 3063bitr4d 299 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄) ↔ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
308307anbi2d 736 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦𝑁 ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄)) ↔ (𝑦𝑁𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
309 2nn 11062 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 2 ∈ ℕ
310 oddprm 15353 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑄 ∈ (ℙ ∖ {2}) → ((𝑄 − 1) / 2) ∈ ℕ)
3116, 310syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → ((𝑄 − 1) / 2) ∈ ℕ)
312290, 311syl5eqel 2692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝑁 ∈ ℕ)
313 nnmulcl 10920 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((2 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (2 · 𝑁) ∈ ℕ)
314309, 312, 313sylancr 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (2 · 𝑁) ∈ ℕ)
315314adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) ∈ ℕ)
316315nnred 10912 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) ∈ ℝ)
317312adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ∈ ℕ)
318317nnred 10912 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ∈ ℝ)
31924zred 11358 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℝ)
320312nncnd 10913 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑𝑁 ∈ ℂ)
321320adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ∈ ℂ)
3223212timesd 11152 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) = (𝑁 + 𝑁))
323322oveq1d 6564 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − 𝑁) = ((𝑁 + 𝑁) − 𝑁))
324321, 321pncan2d 10273 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑁 + 𝑁) − 𝑁) = 𝑁)
325323, 324eqtrd 2644 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − 𝑁) = 𝑁)
326252rehalfcld 11156 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 / 2) ∈ ℝ)
327252ltm1d 10835 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 − 1) < 𝑄)
328155a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 2 ∈ ℝ)
329157a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 0 < 2)
330 ltdiv1 10766 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑄 − 1) ∈ ℝ ∧ 𝑄 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((𝑄 − 1) < 𝑄 ↔ ((𝑄 − 1) / 2) < (𝑄 / 2)))
331293, 252, 328, 329, 330syl112anc 1322 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 − 1) < 𝑄 ↔ ((𝑄 − 1) / 2) < (𝑄 / 2)))
332327, 331mpbid 221 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 − 1) / 2) < (𝑄 / 2))
333290, 332syl5eqbr 4618 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 < (𝑄 / 2))
334318, 326, 333ltled 10064 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ≤ (𝑄 / 2))
335253, 295, 68, 296div32d 10703 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 2) · 𝑃) = (𝑄 · (𝑃 / 2)))
336131adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑀 ∈ ℝ)
337336rehalfcld 11156 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑀 / 2) ∈ ℝ)
338 peano2re 10088 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((⌊‘(𝑀 / 2)) ∈ ℝ → ((⌊‘(𝑀 / 2)) + 1) ∈ ℝ)
339337, 134, 3383syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((⌊‘(𝑀 / 2)) + 1) ∈ ℝ)
34019zred 11358 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ∈ ℝ)
341 flltp1 12463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑀 / 2) ∈ ℝ → (𝑀 / 2) < ((⌊‘(𝑀 / 2)) + 1))
342337, 341syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑀 / 2) < ((⌊‘(𝑀 / 2)) + 1))
343 elfzle1 12215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) → ((⌊‘(𝑀 / 2)) + 1) ≤ 𝑢)
344343adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((⌊‘(𝑀 / 2)) + 1) ≤ 𝑢)
345337, 339, 340, 342, 344ltletrd 10076 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑀 / 2) < 𝑢)
346 ltdivmul 10777 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑀 ∈ ℝ ∧ 𝑢 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((𝑀 / 2) < 𝑢𝑀 < (2 · 𝑢)))
347336, 340, 328, 329, 346syl112anc 1322 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑀 / 2) < 𝑢𝑀 < (2 · 𝑢)))
348345, 347mpbid 221 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑀 < (2 · 𝑢))
349127, 348syl5eqbrr 4619 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − 1) / 2) < (2 · 𝑢))
35067nnred 10912 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℝ)
351 peano2rem 10227 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑃 ∈ ℝ → (𝑃 − 1) ∈ ℝ)
352350, 351syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − 1) ∈ ℝ)
353 ltdivmul 10777 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((𝑃 − 1) ∈ ℝ ∧ (2 · 𝑢) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (((𝑃 − 1) / 2) < (2 · 𝑢) ↔ (𝑃 − 1) < (2 · (2 · 𝑢))))
354352, 22, 328, 329, 353syl112anc 1322 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑃 − 1) / 2) < (2 · 𝑢) ↔ (𝑃 − 1) < (2 · (2 · 𝑢))))
355349, 354mpbid 221 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − 1) < (2 · (2 · 𝑢)))
356212adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℤ)
357 zmulcl 11303 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((2 ∈ ℤ ∧ (2 · 𝑢) ∈ ℤ) → (2 · (2 · 𝑢)) ∈ ℤ)
35817, 21, 357sylancr 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · (2 · 𝑢)) ∈ ℤ)
359 zlem1lt 11306 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑃 ∈ ℤ ∧ (2 · (2 · 𝑢)) ∈ ℤ) → (𝑃 ≤ (2 · (2 · 𝑢)) ↔ (𝑃 − 1) < (2 · (2 · 𝑢))))
360356, 358, 359syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 ≤ (2 · (2 · 𝑢)) ↔ (𝑃 − 1) < (2 · (2 · 𝑢))))
361355, 360mpbird 246 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ≤ (2 · (2 · 𝑢)))
362 ledivmul 10778 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑃 ∈ ℝ ∧ (2 · 𝑢) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((𝑃 / 2) ≤ (2 · 𝑢) ↔ 𝑃 ≤ (2 · (2 · 𝑢))))
363350, 22, 328, 329, 362syl112anc 1322 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 / 2) ≤ (2 · 𝑢) ↔ 𝑃 ≤ (2 · (2 · 𝑢))))
364361, 363mpbird 246 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 / 2) ≤ (2 · 𝑢))
365350rehalfcld 11156 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 / 2) ∈ ℝ)
366279nngt0d 10941 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 0 < 𝑄)
367 lemul2 10755 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑃 / 2) ∈ ℝ ∧ (2 · 𝑢) ∈ ℝ ∧ (𝑄 ∈ ℝ ∧ 0 < 𝑄)) → ((𝑃 / 2) ≤ (2 · 𝑢) ↔ (𝑄 · (𝑃 / 2)) ≤ (𝑄 · (2 · 𝑢))))
368365, 22, 252, 366, 367syl112anc 1322 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 / 2) ≤ (2 · 𝑢) ↔ (𝑄 · (𝑃 / 2)) ≤ (𝑄 · (2 · 𝑢))))
369364, 368mpbid 221 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 · (𝑃 / 2)) ≤ (𝑄 · (2 · 𝑢)))
370335, 369eqbrtrd 4605 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 2) · 𝑃) ≤ (𝑄 · (2 · 𝑢)))
371252, 22remulcld 9949 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 · (2 · 𝑢)) ∈ ℝ)
37267nngt0d 10941 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 0 < 𝑃)
373 lemuldiv 10782 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑄 / 2) ∈ ℝ ∧ (𝑄 · (2 · 𝑢)) ∈ ℝ ∧ (𝑃 ∈ ℝ ∧ 0 < 𝑃)) → (((𝑄 / 2) · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ↔ (𝑄 / 2) ≤ ((𝑄 · (2 · 𝑢)) / 𝑃)))
374326, 371, 350, 372, 373syl112anc 1322 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑄 / 2) · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ↔ (𝑄 / 2) ≤ ((𝑄 · (2 · 𝑢)) / 𝑃)))
375370, 374mpbid 221 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 / 2) ≤ ((𝑄 · (2 · 𝑢)) / 𝑃))
376253, 70, 68, 256div23d 10717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 · (2 · 𝑢)) / 𝑃) = ((𝑄 / 𝑃) · (2 · 𝑢)))
377375, 376breqtrd 4609 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 / 2) ≤ ((𝑄 / 𝑃) · (2 · 𝑢)))
378318, 326, 23, 334, 377letrd 10073 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)))
379312nnzd 11357 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑𝑁 ∈ ℤ)
380379adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ∈ ℤ)
381 flge 12468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ ∧ 𝑁 ∈ ℤ) → (𝑁 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)) ↔ 𝑁 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
38223, 380, 381syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑁 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)) ↔ 𝑁 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
383378, 382mpbid 221 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))
384325, 383eqbrtrd 4605 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − 𝑁) ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))
385316, 318, 319, 384subled 10509 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ≤ 𝑁)
386385adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ≤ 𝑁)
387315nnzd 11357 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) ∈ ℤ)
388387, 24zsubcld 11363 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℤ)
389388adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℤ)
390389zred 11358 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℝ)
391312ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑁 ∈ ℕ)
392391nnred 10912 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑁 ∈ ℝ)
393 letr 10010 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑦 ∈ ℝ ∧ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∧ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ≤ 𝑁) → 𝑦𝑁))
394249, 390, 392, 393syl3anc 1318 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∧ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ≤ 𝑁) → 𝑦𝑁))
395386, 394mpan2d 706 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) → 𝑦𝑁))
396395pm4.71rd 665 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ↔ (𝑦𝑁𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
397308, 396bitr4d 270 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦𝑁 ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄)) ↔ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
398397pm5.32da 671 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑦 ∈ ℕ ∧ (𝑦𝑁 ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
399398adantr 480 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → ((𝑦 ∈ ℕ ∧ (𝑦𝑁 ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
400243, 399syl5bb 271 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (((𝑦 ∈ ℕ ∧ 𝑦𝑁) ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄)) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
401 simpr 476 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → 𝑥 = (𝑃 − (2 · 𝑢)))
402356, 21zsubcld 11363 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − (2 · 𝑢)) ∈ ℤ)
403 elfzle2 12216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) → 𝑢𝑀)
404403adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢𝑀)
405404, 127syl6breq 4624 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ≤ ((𝑃 − 1) / 2))
406 lemuldiv2 10783 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑢 ∈ ℝ ∧ (𝑃 − 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 𝑢) ≤ (𝑃 − 1) ↔ 𝑢 ≤ ((𝑃 − 1) / 2)))
407340, 352, 328, 329, 406syl112anc 1322 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑢) ≤ (𝑃 − 1) ↔ 𝑢 ≤ ((𝑃 − 1) / 2)))
408405, 407mpbird 246 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ≤ (𝑃 − 1))
409350ltm1d 10835 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − 1) < 𝑃)
41022, 352, 350, 408, 409lelttrd 10074 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) < 𝑃)
41122, 350posdifd 10493 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑢) < 𝑃 ↔ 0 < (𝑃 − (2 · 𝑢))))
412410, 411mpbid 221 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 0 < (𝑃 − (2 · 𝑢)))
413 elnnz 11264 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑃 − (2 · 𝑢)) ∈ ℕ ↔ ((𝑃 − (2 · 𝑢)) ∈ ℤ ∧ 0 < (𝑃 − (2 · 𝑢))))
414402, 412, 413sylanbrc 695 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − (2 · 𝑢)) ∈ ℕ)
41568, 70, 300sub32d 10303 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) − 1) = ((𝑃 − 1) − (2 · 𝑢)))
416127, 127oveq12i 6561 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑀 + 𝑀) = (((𝑃 − 1) / 2) + ((𝑃 − 1) / 2))
41767nnzd 11357 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℤ)
418417, 214syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − 1) ∈ ℤ)
419418zcnd 11359 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − 1) ∈ ℂ)
4204192halvesd 11155 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑃 − 1) / 2) + ((𝑃 − 1) / 2)) = (𝑃 − 1))
421416, 420syl5eq 2656 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑀 + 𝑀) = (𝑃 − 1))
422421oveq1d 6564 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑀 + 𝑀) − 𝑀) = ((𝑃 − 1) − 𝑀))
423164adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑀 ∈ ℂ)
424423, 423pncan2d 10273 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑀 + 𝑀) − 𝑀) = 𝑀)
425422, 424eqtr3d 2646 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − 1) − 𝑀) = 𝑀)
426425, 348eqbrtrd 4605 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − 1) − 𝑀) < (2 · 𝑢))
427352, 336, 22, 426ltsub23d 10511 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − 1) − (2 · 𝑢)) < 𝑀)
428415, 427eqbrtrd 4605 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) − 1) < 𝑀)
429130adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑀 ∈ ℕ)
430429nnzd 11357 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑀 ∈ ℤ)
431 zlem1lt 11306 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑃 − (2 · 𝑢)) ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑃 − (2 · 𝑢)) ≤ 𝑀 ↔ ((𝑃 − (2 · 𝑢)) − 1) < 𝑀))
432402, 430, 431syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) ≤ 𝑀 ↔ ((𝑃 − (2 · 𝑢)) − 1) < 𝑀))
433428, 432mpbird 246 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − (2 · 𝑢)) ≤ 𝑀)
434 fznn 12278 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑀 ∈ ℤ → ((𝑃 − (2 · 𝑢)) ∈ (1...𝑀) ↔ ((𝑃 − (2 · 𝑢)) ∈ ℕ ∧ (𝑃 − (2 · 𝑢)) ≤ 𝑀)))
435430, 434syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) ∈ (1...𝑀) ↔ ((𝑃 − (2 · 𝑢)) ∈ ℕ ∧ (𝑃 − (2 · 𝑢)) ≤ 𝑀)))
436414, 433, 435mpbir2and 959 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − (2 · 𝑢)) ∈ (1...𝑀))
437436adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (𝑃 − (2 · 𝑢)) ∈ (1...𝑀))
438401, 437eqeltrd 2688 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → 𝑥 ∈ (1...𝑀))
439438biantrurd 528 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (𝑦 ∈ (1...𝑁) ↔ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))))
440379ad2antrr 758 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → 𝑁 ∈ ℤ)
441 fznn 12278 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ ℤ → (𝑦 ∈ (1...𝑁) ↔ (𝑦 ∈ ℕ ∧ 𝑦𝑁)))
442440, 441syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (𝑦 ∈ (1...𝑁) ↔ (𝑦 ∈ ℕ ∧ 𝑦𝑁)))
443439, 442bitr3d 269 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ↔ (𝑦 ∈ ℕ ∧ 𝑦𝑁)))
444401oveq1d 6564 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (𝑥 · 𝑄) = ((𝑃 − (2 · 𝑢)) · 𝑄))
445444breq2d 4595 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → ((𝑦 · 𝑃) < (𝑥 · 𝑄) ↔ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄)))
446443, 445anbi12d 743 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)) ↔ ((𝑦 ∈ ℕ ∧ 𝑦𝑁) ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄))))
447388adantr 480 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℤ)
448 fznn 12278 . . . . . . . . . . . . . . . . . . 19 (((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℤ → (𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
449447, 448syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
450400, 446, 4493bitr4d 299 . . . . . . . . . . . . . . . . 17 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)) ↔ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
451242, 450syl5bb 271 . . . . . . . . . . . . . . . 16 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (⟨𝑥, 𝑦⟩ ∈ 𝑆𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
452451pm5.32da 671 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑥 = (𝑃 − (2 · 𝑢)) ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑆) ↔ (𝑥 = (𝑃 − (2 · 𝑢)) ∧ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))))
453 vex 3176 . . . . . . . . . . . . . . . . . . 19 𝑥 ∈ V
454 vex 3176 . . . . . . . . . . . . . . . . . . 19 𝑦 ∈ V
455453, 454op1std 7069 . . . . . . . . . . . . . . . . . 18 (𝑧 = ⟨𝑥, 𝑦⟩ → (1st𝑧) = 𝑥)
456455eqeq1d 2612 . . . . . . . . . . . . . . . . 17 (𝑧 = ⟨𝑥, 𝑦⟩ → ((1st𝑧) = (𝑃 − (2 · 𝑢)) ↔ 𝑥 = (𝑃 − (2 · 𝑢))))
457456elrab 3331 . . . . . . . . . . . . . . . 16 (⟨𝑥, 𝑦⟩ ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} ↔ (⟨𝑥, 𝑦⟩ ∈ 𝑆𝑥 = (𝑃 − (2 · 𝑢))))
458 ancom 465 . . . . . . . . . . . . . . . 16 ((⟨𝑥, 𝑦⟩ ∈ 𝑆𝑥 = (𝑃 − (2 · 𝑢))) ↔ (𝑥 = (𝑃 − (2 · 𝑢)) ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑆))
459457, 458bitri 263 . . . . . . . . . . . . . . 15 (⟨𝑥, 𝑦⟩ ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} ↔ (𝑥 = (𝑃 − (2 · 𝑢)) ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑆))
460 opelxp 5070 . . . . . . . . . . . . . . . 16 (⟨𝑥, 𝑦⟩ ∈ ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ↔ (𝑥 ∈ {(𝑃 − (2 · 𝑢))} ∧ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
461 velsn 4141 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ {(𝑃 − (2 · 𝑢))} ↔ 𝑥 = (𝑃 − (2 · 𝑢)))
462461anbi1i 727 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ {(𝑃 − (2 · 𝑢))} ∧ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ↔ (𝑥 = (𝑃 − (2 · 𝑢)) ∧ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
463460, 462bitri 263 . . . . . . . . . . . . . . 15 (⟨𝑥, 𝑦⟩ ∈ ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ↔ (𝑥 = (𝑃 − (2 · 𝑢)) ∧ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
464452, 459, 4633bitr4g 302 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⟨𝑥, 𝑦⟩ ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} ↔ ⟨𝑥, 𝑦⟩ ∈ ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))))
465238, 239, 464eqrelrdv 5139 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} = ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
466465fveq2d 6107 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (#‘{𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))}) = (#‘({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))))
467 fzfid 12634 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ∈ Fin)
468 xpsnen2g 7938 . . . . . . . . . . . . . 14 (((𝑃 − (2 · 𝑢)) ∈ ℤ ∧ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ∈ Fin) → ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ≈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
469402, 467, 468syl2anc 691 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ≈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
470 hasheni 12998 . . . . . . . . . . . . 13 (({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ≈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) → (#‘({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) = (#‘(1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
471469, 470syl 17 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (#‘({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) = (#‘(1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
472 ltmul2 10753 . . . . . . . . . . . . . . . . . . . . 21 (((2 · 𝑢) ∈ ℝ ∧ 𝑃 ∈ ℝ ∧ (𝑄 ∈ ℝ ∧ 0 < 𝑄)) → ((2 · 𝑢) < 𝑃 ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · 𝑃)))
47322, 350, 252, 366, 472syl112anc 1322 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑢) < 𝑃 ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · 𝑃)))
474410, 473mpbid 221 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 · (2 · 𝑢)) < (𝑄 · 𝑃))
475 ltdivmul2 10779 . . . . . . . . . . . . . . . . . . . 20 (((𝑄 · (2 · 𝑢)) ∈ ℝ ∧ 𝑄 ∈ ℝ ∧ (𝑃 ∈ ℝ ∧ 0 < 𝑃)) → (((𝑄 · (2 · 𝑢)) / 𝑃) < 𝑄 ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · 𝑃)))
476371, 252, 350, 372, 475syl112anc 1322 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑄 · (2 · 𝑢)) / 𝑃) < 𝑄 ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · 𝑃)))
477474, 476mpbird 246 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 · (2 · 𝑢)) / 𝑃) < 𝑄)
478376, 477eqbrtrrd 4607 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 𝑃) · (2 · 𝑢)) < 𝑄)
479 fllt 12469 . . . . . . . . . . . . . . . . . 18 ((((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ ∧ 𝑄 ∈ ℤ) → (((𝑄 / 𝑃) · (2 · 𝑢)) < 𝑄 ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < 𝑄))
48023, 280, 479syl2anc 691 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑄 / 𝑃) · (2 · 𝑢)) < 𝑄 ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < 𝑄))
481478, 480mpbid 221 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < 𝑄)
482 zltlem1 11307 . . . . . . . . . . . . . . . . 17 (((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ ∧ 𝑄 ∈ ℤ) → ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < 𝑄 ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ≤ (𝑄 − 1)))
48324, 280, 482syl2anc 691 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < 𝑄 ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ≤ (𝑄 − 1)))
484481, 483mpbid 221 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ≤ (𝑄 − 1))
485484, 298breqtrrd 4611 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ≤ (2 · 𝑁))
486 eluz2 11569 . . . . . . . . . . . . . 14 ((2 · 𝑁) ∈ (ℤ‘(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ↔ ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ ∧ (2 · 𝑁) ∈ ℤ ∧ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ≤ (2 · 𝑁)))
48724, 387, 485, 486syl3anbrc 1239 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) ∈ (ℤ‘(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
488 uznn0sub 11595 . . . . . . . . . . . . 13 ((2 · 𝑁) ∈ (ℤ‘(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℕ0)
489 hashfz1 12996 . . . . . . . . . . . . 13 (((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℕ0 → (#‘(1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) = ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
490487, 488, 4893syl 18 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (#‘(1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) = ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
491466, 471, 4903eqtrd 2648 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (#‘{𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))}) = ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
492491sumeq2dv 14281 . . . . . . . . . 10 (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(#‘{𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))}) = Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
49385, 235, 4923eqtr3rd 2653 . . . . . . . . 9 (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (#‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))
494314nncnd 10913 . . . . . . . . . . 11 (𝜑 → (2 · 𝑁) ∈ ℂ)
495494adantr 480 . . . . . . . . . 10 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) ∈ ℂ)
4965, 495, 301fsumsub 14362 . . . . . . . . 9 (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) − Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
497493, 496eqtr3d 2646 . . . . . . . 8 (𝜑 → (#‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) = (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) − Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
498497oveq2d 6565 . . . . . . 7 (𝜑 → (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (#‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) = (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) − Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
49925zcnd 11359 . . . . . . . 8 (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℂ)
5005, 387fsumzcl 14313 . . . . . . . . 9 (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) ∈ ℤ)
501500zcnd 11359 . . . . . . . 8 (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) ∈ ℂ)
502499, 501pncan3d 10274 . . . . . . 7 (𝜑 → (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) − Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁))
503 fsumconst 14364 . . . . . . . . 9 (((((⌊‘(𝑀 / 2)) + 1)...𝑀) ∈ Fin ∧ (2 · 𝑁) ∈ ℂ) → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) = ((#‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · (2 · 𝑁)))
5045, 494, 503syl2anc 691 . . . . . . . 8 (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) = ((#‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · (2 · 𝑁)))
505 hashcl 13009 . . . . . . . . . . 11 ((((⌊‘(𝑀 / 2)) + 1)...𝑀) ∈ Fin → (#‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∈ ℕ0)
5065, 505syl 17 . . . . . . . . . 10 (𝜑 → (#‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∈ ℕ0)
507506nn0cnd 11230 . . . . . . . . 9 (𝜑 → (#‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∈ ℂ)
508 2cnd 10970 . . . . . . . . 9 (𝜑 → 2 ∈ ℂ)
509507, 508, 320mul12d 10124 . . . . . . . 8 (𝜑 → ((#‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · (2 · 𝑁)) = (2 · ((#‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)))
510504, 509eqtrd 2644 . . . . . . 7 (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) = (2 · ((#‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)))
511498, 502, 5103eqtrd 2648 . . . . . 6 (𝜑 → (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (#‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) = (2 · ((#‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)))
512511oveq2d 6565 . . . . 5 (𝜑 → (-1↑(Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (#‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))) = (-1↑(2 · ((#‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁))))
51317a1i 11 . . . . . 6 (𝜑 → 2 ∈ ℤ)
514506nn0zd 11356 . . . . . . 7 (𝜑 → (#‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∈ ℤ)
515514, 379zmulcld 11364 . . . . . 6 (𝜑 → ((#‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁) ∈ ℤ)
516 expmulz 12768 . . . . . 6 (((-1 ∈ ℂ ∧ -1 ≠ 0) ∧ (2 ∈ ℤ ∧ ((#‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁) ∈ ℤ)) → (-1↑(2 · ((#‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁))) = ((-1↑2)↑((#‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)))
5172, 4, 513, 515, 516syl22anc 1319 . . . . 5 (𝜑 → (-1↑(2 · ((#‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁))) = ((-1↑2)↑((#‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)))
518 neg1sqe1 12821 . . . . . . 7 (-1↑2) = 1
519518oveq1i 6559 . . . . . 6 ((-1↑2)↑((#‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)) = (1↑((#‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁))
520 1exp 12751 . . . . . . 7 (((#‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁) ∈ ℤ → (1↑((#‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)) = 1)
521515, 520syl 17 . . . . . 6 (𝜑 → (1↑((#‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)) = 1)
522519, 521syl5eq 2656 . . . . 5 (𝜑 → ((-1↑2)↑((#‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)) = 1)
523512, 517, 5223eqtrd 2648 . . . 4 (𝜑 → (-1↑(Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (#‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))) = 1)
52445, 56, 5233eqtr4d 2654 . . 3 (𝜑 → ((-1↑(#‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) · (-1↑(#‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))) = (-1↑(Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (#‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))))
525 expaddz 12766 . . . 4 (((-1 ∈ ℂ ∧ -1 ≠ 0) ∧ (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ ∧ (#‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) ∈ ℤ)) → (-1↑(Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (#‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))) = ((-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) · (-1↑(#‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))))
5262, 4, 25, 43, 525syl22anc 1319 . . 3 (𝜑 → (-1↑(Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (#‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))) = ((-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) · (-1↑(#‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))))
527524, 526eqtr2d 2645 . 2 (𝜑 → ((-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) · (-1↑(#‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))) = ((-1↑(#‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) · (-1↑(#‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))))
52826, 42, 42, 44, 527mulcan2ad 10542 1 (𝜑 → (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (-1↑(#‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  {crab 2900   ∖ cdif 3537   ⊆ wss 3540  {csn 4125  ⟨cop 4131  ∪ ciun 4455  Disj wdisj 4553   class class class wbr 4583  {copab 4642   × cxp 5036  Rel wrel 5043  ‘cfv 5804  (class class class)co 6549  1st c1st 7057   ≈ cen 7838  Fincfn 7841  ℂcc 9813  ℝcr 9814  0cc0 9815  1c1 9816   + caddc 9818   · cmul 9820   < clt 9953   ≤ cle 9954   − cmin 10145  -cneg 10146   / cdiv 10563  ℕcn 10897  2c2 10947  ℕ0cn0 11169  ℤcz 11254  ℤ≥cuz 11563  ...cfz 12197  ⌊cfl 12453  ↑cexp 12722  #chash 12979  Σcsu 14264   ∥ cdvds 14821  ℙcprime 15223 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-disj 4554  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-sup 8231  df-inf 8232  df-oi 8298  df-card 8648  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-n0 11170  df-z 11255  df-uz 11564  df-rp 11709  df-fz 12198  df-fzo 12335  df-fl 12455  df-seq 12664  df-exp 12723  df-hash 12980  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-clim 14067  df-sum 14265  df-dvds 14822  df-prm 15224 This theorem is referenced by:  lgsquadlem2  24906
 Copyright terms: Public domain W3C validator