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

Theorem lgsquadlem1 25326
Description: Lemma for lgsquad 25329. 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:   𝑥,𝑢,𝑦,𝑧,𝑃   𝜑,𝑢,𝑥,𝑦,𝑧   𝑢,𝑀,𝑦,𝑧   𝑢,𝑁,𝑥,𝑦,𝑧   𝑢,𝑄,𝑥,𝑦,𝑧   𝑢,𝑆,𝑥,𝑧   𝑥,𝑀   𝑦,𝑆

Proof of Theorem lgsquadlem1
Dummy variables 𝑛 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 neg1cn 11326 . . . 4 -1 ∈ ℂ
21a1i 11 . . 3 (𝜑 → -1 ∈ ℂ)
3 neg1ne0 11328 . . . 4 -1 ≠ 0
43a1i 11 . . 3 (𝜑 → -1 ≠ 0)
5 fzfid 12980 . . . 4 (𝜑 → (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∈ Fin)
6 lgseisen.2 . . . . . . . . . 10 (𝜑𝑄 ∈ (ℙ ∖ {2}))
7 eldifi 3883 . . . . . . . . . 10 (𝑄 ∈ (ℙ ∖ {2}) → 𝑄 ∈ ℙ)
8 prmnn 15595 . . . . . . . . . 10 (𝑄 ∈ ℙ → 𝑄 ∈ ℕ)
96, 7, 83syl 18 . . . . . . . . 9 (𝜑𝑄 ∈ ℕ)
109nnred 11237 . . . . . . . 8 (𝜑𝑄 ∈ ℝ)
11 lgseisen.1 . . . . . . . . 9 (𝜑𝑃 ∈ (ℙ ∖ {2}))
12 eldifi 3883 . . . . . . . . 9 (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℙ)
13 prmnn 15595 . . . . . . . . 9 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
1411, 12, 133syl 18 . . . . . . . 8 (𝜑𝑃 ∈ ℕ)
1510, 14nndivred 11271 . . . . . . 7 (𝜑 → (𝑄 / 𝑃) ∈ ℝ)
1615adantr 466 . . . . . 6 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 / 𝑃) ∈ ℝ)
17 2z 11611 . . . . . . . 8 2 ∈ ℤ
18 elfzelz 12549 . . . . . . . . 9 (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) → 𝑢 ∈ ℤ)
1918adantl 467 . . . . . . . 8 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ∈ ℤ)
20 zmulcl 11628 . . . . . . . 8 ((2 ∈ ℤ ∧ 𝑢 ∈ ℤ) → (2 · 𝑢) ∈ ℤ)
2117, 19, 20sylancr 575 . . . . . . 7 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ∈ ℤ)
2221zred 11684 . . . . . 6 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ∈ ℝ)
2316, 22remulcld 10272 . . . . 5 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ)
2423flcld 12807 . . . 4 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ)
255, 24fsumzcl 14674 . . 3 (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ)
262, 4, 25expclzd 13220 . 2 (𝜑 → (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℂ)
27 fzfid 12980 . . . . . . 7 (𝜑 → (1...𝑀) ∈ Fin)
28 fzfid 12980 . . . . . . 7 (𝜑 → (1...𝑁) ∈ Fin)
29 xpfi 8387 . . . . . . 7 (((1...𝑀) ∈ Fin ∧ (1...𝑁) ∈ Fin) → ((1...𝑀) × (1...𝑁)) ∈ Fin)
3027, 28, 29syl2anc 573 . . . . . 6 (𝜑 → ((1...𝑀) × (1...𝑁)) ∈ Fin)
31 lgsquad.6 . . . . . . 7 𝑆 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))}
32 opabssxp 5333 . . . . . . 7 {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} ⊆ ((1...𝑀) × (1...𝑁))
3331, 32eqsstri 3784 . . . . . 6 𝑆 ⊆ ((1...𝑀) × (1...𝑁))
34 ssfi 8336 . . . . . 6 ((((1...𝑀) × (1...𝑁)) ∈ Fin ∧ 𝑆 ⊆ ((1...𝑀) × (1...𝑁))) → 𝑆 ∈ Fin)
3530, 33, 34sylancl 574 . . . . 5 (𝜑𝑆 ∈ Fin)
36 ssrab2 3836 . . . . 5 {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)} ⊆ 𝑆
37 ssfi 8336 . . . . 5 ((𝑆 ∈ Fin ∧ {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)} ⊆ 𝑆) → {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)} ∈ Fin)
3835, 36, 37sylancl 574 . . . 4 (𝜑 → {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)} ∈ Fin)
39 hashcl 13349 . . . 4 ({𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)} ∈ Fin → (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) ∈ ℕ0)
4038, 39syl 17 . . 3 (𝜑 → (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) ∈ ℕ0)
41 expcl 13085 . . 3 ((-1 ∈ ℂ ∧ (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) ∈ ℕ0) → (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) ∈ ℂ)
421, 40, 41sylancr 575 . 2 (𝜑 → (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) ∈ ℂ)
4340nn0zd 11682 . . 3 (𝜑 → (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) ∈ ℤ)
442, 4, 43expne0d 13221 . 2 (𝜑 → (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) ≠ 0)
4542, 44recidd 10998 . . . 4 (𝜑 → ((-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) · (1 / (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})))) = 1)
46 1div1e1 10919 . . . . . . . . 9 (1 / 1) = 1
4746negeqi 10476 . . . . . . . 8 -(1 / 1) = -1
48 ax-1cn 10196 . . . . . . . . 9 1 ∈ ℂ
49 ax-1ne0 10207 . . . . . . . . 9 1 ≠ 0
50 divneg2 10951 . . . . . . . . 9 ((1 ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ≠ 0) → -(1 / 1) = (1 / -1))
5148, 48, 49, 50mp3an 1572 . . . . . . . 8 -(1 / 1) = (1 / -1)
5247, 51eqtr3i 2795 . . . . . . 7 -1 = (1 / -1)
5352oveq1i 6803 . . . . . 6 (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) = ((1 / -1)↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))
542, 4, 43exprecd 13223 . . . . . 6 (𝜑 → ((1 / -1)↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) = (1 / (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))))
5553, 54syl5eq 2817 . . . . 5 (𝜑 → (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) = (1 / (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))))
5655oveq2d 6809 . . . 4 (𝜑 → ((-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) · (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))) = ((-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) · (1 / (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})))))
5735adantr 466 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑆 ∈ Fin)
58 ssrab2 3836 . . . . . . . . . . . 12 {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} ⊆ 𝑆
59 ssfi 8336 . . . . . . . . . . . 12 ((𝑆 ∈ Fin ∧ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} ⊆ 𝑆) → {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} ∈ Fin)
6057, 58, 59sylancl 574 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} ∈ Fin)
61 fveq2 6332 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = 𝑣 → (1st𝑧) = (1st𝑣))
6261eqeq1d 2773 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑣 → ((1st𝑧) = (𝑃 − (2 · 𝑢)) ↔ (1st𝑣) = (𝑃 − (2 · 𝑢))))
6362elrab 3515 . . . . . . . . . . . . . . . . . . 19 (𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} ↔ (𝑣𝑆 ∧ (1st𝑣) = (𝑃 − (2 · 𝑢))))
6463simprbi 484 . . . . . . . . . . . . . . . . . 18 (𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} → (1st𝑣) = (𝑃 − (2 · 𝑢)))
6564ad2antll 708 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → (1st𝑣) = (𝑃 − (2 · 𝑢)))
6665oveq2d 6809 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → (𝑃 − (1st𝑣)) = (𝑃 − (𝑃 − (2 · 𝑢))))
6714adantr 466 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℕ)
6867nncnd 11238 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℂ)
6968adantrr 696 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → 𝑃 ∈ ℂ)
7021zcnd 11685 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ∈ ℂ)
7170adantrr 696 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → (2 · 𝑢) ∈ ℂ)
7269, 71nncand 10599 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → (𝑃 − (𝑃 − (2 · 𝑢))) = (2 · 𝑢))
7366, 72eqtrd 2805 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → (𝑃 − (1st𝑣)) = (2 · 𝑢))
7473oveq1d 6808 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → ((𝑃 − (1st𝑣)) / 2) = ((2 · 𝑢) / 2))
7519zcnd 11685 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ∈ ℂ)
7675adantrr 696 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → 𝑢 ∈ ℂ)
77 2cnd 11295 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → 2 ∈ ℂ)
78 2ne0 11315 . . . . . . . . . . . . . . . 16 2 ≠ 0
7978a1i 11 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → 2 ≠ 0)
8076, 77, 79divcan3d 11008 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → ((2 · 𝑢) / 2) = 𝑢)
8174, 80eqtrd 2805 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → ((𝑃 − (1st𝑣)) / 2) = 𝑢)
8281ralrimivva 3120 . . . . . . . . . . . 12 (𝜑 → ∀𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)∀𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} ((𝑃 − (1st𝑣)) / 2) = 𝑢)
83 invdisj 4772 . . . . . . . . . . . 12 (∀𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)∀𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} ((𝑃 − (1st𝑣)) / 2) = 𝑢Disj 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})
8482, 83syl 17 . . . . . . . . . . 11 (𝜑Disj 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})
855, 60, 84hashiun 14761 . . . . . . . . . 10 (𝜑 → (♯‘ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))}) = Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(♯‘{𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))}))
86 iunrab 4701 . . . . . . . . . . . 12 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} = {𝑧𝑆 ∣ ∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1st𝑧) = (𝑃 − (2 · 𝑢))}
87 eldifsni 4457 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ≠ 2)
8811, 87syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑃 ≠ 2)
8988necomd 2998 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 2 ≠ 𝑃)
9089neneqd 2948 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ¬ 2 = 𝑃)
9190ad2antrr 705 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ¬ 2 = 𝑃)
92 uzid 11903 . . . . . . . . . . . . . . . . . . . . 21 (2 ∈ ℤ → 2 ∈ (ℤ‘2))
9317, 92ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 2 ∈ (ℤ‘2)
9411, 12syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑃 ∈ ℙ)
9594ad2antrr 705 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℙ)
96 dvdsprm 15622 . . . . . . . . . . . . . . . . . . . 20 ((2 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) → (2 ∥ 𝑃 ↔ 2 = 𝑃))
9793, 95, 96sylancr 575 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 ∥ 𝑃 ↔ 2 = 𝑃))
9891, 97mtbird 314 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ¬ 2 ∥ 𝑃)
9914ad2antrr 705 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℕ)
10099nncnd 11238 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℂ)
10121adantlr 694 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ∈ ℤ)
102101zcnd 11685 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ∈ ℂ)
103100, 102npcand 10598 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) + (2 · 𝑢)) = 𝑃)
104103breq2d 4798 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 ∥ ((𝑃 − (2 · 𝑢)) + (2 · 𝑢)) ↔ 2 ∥ 𝑃))
10598, 104mtbird 314 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ¬ 2 ∥ ((𝑃 − (2 · 𝑢)) + (2 · 𝑢)))
10618adantl 467 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ∈ ℤ)
107 dvdsmul1 15212 . . . . . . . . . . . . . . . . . . 19 ((2 ∈ ℤ ∧ 𝑢 ∈ ℤ) → 2 ∥ (2 · 𝑢))
10817, 106, 107sylancr 575 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 2 ∥ (2 · 𝑢))
10917a1i 11 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 2 ∈ ℤ)
11099nnzd 11683 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℤ)
111110, 101zsubcld 11689 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − (2 · 𝑢)) ∈ ℤ)
112 dvds2add 15224 . . . . . . . . . . . . . . . . . . 19 ((2 ∈ ℤ ∧ (𝑃 − (2 · 𝑢)) ∈ ℤ ∧ (2 · 𝑢) ∈ ℤ) → ((2 ∥ (𝑃 − (2 · 𝑢)) ∧ 2 ∥ (2 · 𝑢)) → 2 ∥ ((𝑃 − (2 · 𝑢)) + (2 · 𝑢))))
113109, 111, 101, 112syl3anc 1476 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 ∥ (𝑃 − (2 · 𝑢)) ∧ 2 ∥ (2 · 𝑢)) → 2 ∥ ((𝑃 − (2 · 𝑢)) + (2 · 𝑢))))
114108, 113mpan2d 674 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 ∥ (𝑃 − (2 · 𝑢)) → 2 ∥ ((𝑃 − (2 · 𝑢)) + (2 · 𝑢))))
115105, 114mtod 189 . . . . . . . . . . . . . . . 16 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ¬ 2 ∥ (𝑃 − (2 · 𝑢)))
116 breq2 4790 . . . . . . . . . . . . . . . . 17 ((1st𝑧) = (𝑃 − (2 · 𝑢)) → (2 ∥ (1st𝑧) ↔ 2 ∥ (𝑃 − (2 · 𝑢))))
117116notbid 307 . . . . . . . . . . . . . . . 16 ((1st𝑧) = (𝑃 − (2 · 𝑢)) → (¬ 2 ∥ (1st𝑧) ↔ ¬ 2 ∥ (𝑃 − (2 · 𝑢))))
118115, 117syl5ibrcom 237 . . . . . . . . . . . . . . 15 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((1st𝑧) = (𝑃 − (2 · 𝑢)) → ¬ 2 ∥ (1st𝑧)))
119118rexlimdva 3179 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑆) → (∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1st𝑧) = (𝑃 − (2 · 𝑢)) → ¬ 2 ∥ (1st𝑧)))
120 simpr 471 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧𝑆) → 𝑧𝑆)
12133, 120sseldi 3750 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧𝑆) → 𝑧 ∈ ((1...𝑀) × (1...𝑁)))
122 xp1st 7347 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ ((1...𝑀) × (1...𝑁)) → (1st𝑧) ∈ (1...𝑀))
123121, 122syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑧𝑆) → (1st𝑧) ∈ (1...𝑀))
124 elfzelz 12549 . . . . . . . . . . . . . . . 16 ((1st𝑧) ∈ (1...𝑀) → (1st𝑧) ∈ ℤ)
125 odd2np1 15273 . . . . . . . . . . . . . . . 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 15722 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑃 ∈ (ℙ ∖ {2}) → ((𝑃 − 1) / 2) ∈ ℕ)
12911, 128syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝑃 − 1) / 2) ∈ ℕ)
130127, 129syl5eqel 2854 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑀 ∈ ℕ)
131130nnred 11237 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑀 ∈ ℝ)
132131ad2antrr 705 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑀 ∈ ℝ)
133132rehalfcld 11481 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑀 / 2) ∈ ℝ)
134 reflcl 12805 . . . . . . . . . . . . . . . . . . . . 21 ((𝑀 / 2) ∈ ℝ → (⌊‘(𝑀 / 2)) ∈ ℝ)
135133, 134syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (⌊‘(𝑀 / 2)) ∈ ℝ)
136130ad2antrr 705 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑀 ∈ ℕ)
137136nnzd 11683 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑀 ∈ ℤ)
138 simprl 754 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑛 ∈ ℤ)
139137, 138zsubcld 11689 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑀𝑛) ∈ ℤ)
140139zred 11684 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑀𝑛) ∈ ℝ)
141 flle 12808 . . . . . . . . . . . . . . . . . . . . 21 ((𝑀 / 2) ∈ ℝ → (⌊‘(𝑀 / 2)) ≤ (𝑀 / 2))
142133, 141syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (⌊‘(𝑀 / 2)) ≤ (𝑀 / 2))
143 zre 11583 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ ℤ → 𝑛 ∈ ℝ)
144143ad2antrl 707 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑛 ∈ ℝ)
145 simprr 756 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((2 · 𝑛) + 1) = (1st𝑧))
146123adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (1st𝑧) ∈ (1...𝑀))
147145, 146eqeltrd 2850 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((2 · 𝑛) + 1) ∈ (1...𝑀))
148 elfzle2 12552 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((2 · 𝑛) + 1) ∈ (1...𝑀) → ((2 · 𝑛) + 1) ≤ 𝑀)
149147, 148syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((2 · 𝑛) + 1) ≤ 𝑀)
150 zmulcl 11628 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((2 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (2 · 𝑛) ∈ ℤ)
15117, 138, 150sylancr 575 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (2 · 𝑛) ∈ ℤ)
152 zltp1le 11629 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((2 · 𝑛) ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((2 · 𝑛) < 𝑀 ↔ ((2 · 𝑛) + 1) ≤ 𝑀))
153151, 137, 152syl2anc 573 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((2 · 𝑛) < 𝑀 ↔ ((2 · 𝑛) + 1) ≤ 𝑀))
154149, 153mpbird 247 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (2 · 𝑛) < 𝑀)
155 2re 11292 . . . . . . . . . . . . . . . . . . . . . . . . 25 2 ∈ ℝ
156155a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 2 ∈ ℝ)
157 2pos 11314 . . . . . . . . . . . . . . . . . . . . . . . . 25 0 < 2
158157a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 0 < 2)
159 ltmuldiv2 11099 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 𝑛) < 𝑀𝑛 < (𝑀 / 2)))
160144, 132, 156, 158, 159syl112anc 1480 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((2 · 𝑛) < 𝑀𝑛 < (𝑀 / 2)))
161154, 160mpbid 222 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑛 < (𝑀 / 2))
162133recnd 10270 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑀 / 2) ∈ ℂ)
163162, 162pncan2d 10596 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (((𝑀 / 2) + (𝑀 / 2)) − (𝑀 / 2)) = (𝑀 / 2))
164130nncnd 11238 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝑀 ∈ ℂ)
165164ad2antrr 705 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑀 ∈ ℂ)
1661652halvesd 11480 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((𝑀 / 2) + (𝑀 / 2)) = 𝑀)
167166oveq1d 6808 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (((𝑀 / 2) + (𝑀 / 2)) − (𝑀 / 2)) = (𝑀 − (𝑀 / 2)))
168163, 167eqtr3d 2807 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑀 / 2) = (𝑀 − (𝑀 / 2)))
169161, 168breqtrd 4812 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑛 < (𝑀 − (𝑀 / 2)))
170144, 132, 133, 169ltsub13d 10835 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑀 / 2) < (𝑀𝑛))
171135, 133, 140, 142, 170lelttrd 10397 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (⌊‘(𝑀 / 2)) < (𝑀𝑛))
172133flcld 12807 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (⌊‘(𝑀 / 2)) ∈ ℤ)
173 zltp1le 11629 . . . . . . . . . . . . . . . . . . . 20 (((⌊‘(𝑀 / 2)) ∈ ℤ ∧ (𝑀𝑛) ∈ ℤ) → ((⌊‘(𝑀 / 2)) < (𝑀𝑛) ↔ ((⌊‘(𝑀 / 2)) + 1) ≤ (𝑀𝑛)))
174172, 139, 173syl2anc 573 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((⌊‘(𝑀 / 2)) < (𝑀𝑛) ↔ ((⌊‘(𝑀 / 2)) + 1) ≤ (𝑀𝑛)))
175171, 174mpbid 222 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((⌊‘(𝑀 / 2)) + 1) ≤ (𝑀𝑛))
176 2t0e0 11385 . . . . . . . . . . . . . . . . . . . . 21 (2 · 0) = 0
177 2cn 11293 . . . . . . . . . . . . . . . . . . . . . . . . 25 2 ∈ ℂ
178 zcn 11584 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 ∈ ℤ → 𝑛 ∈ ℂ)
179178ad2antrl 707 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑛 ∈ ℂ)
180 mulcl 10222 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((2 ∈ ℂ ∧ 𝑛 ∈ ℂ) → (2 · 𝑛) ∈ ℂ)
181177, 179, 180sylancr 575 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (2 · 𝑛) ∈ ℂ)
182 pncan 10489 . . . . . . . . . . . . . . . . . . . . . . . 24 (((2 · 𝑛) ∈ ℂ ∧ 1 ∈ ℂ) → (((2 · 𝑛) + 1) − 1) = (2 · 𝑛))
183181, 48, 182sylancl 574 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (((2 · 𝑛) + 1) − 1) = (2 · 𝑛))
184 elfznn 12577 . . . . . . . . . . . . . . . . . . . . . . . 24 (((2 · 𝑛) + 1) ∈ (1...𝑀) → ((2 · 𝑛) + 1) ∈ ℕ)
185 nnm1nn0 11536 . . . . . . . . . . . . . . . . . . . . . . . 24 (((2 · 𝑛) + 1) ∈ ℕ → (((2 · 𝑛) + 1) − 1) ∈ ℕ0)
186147, 184, 1853syl 18 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (((2 · 𝑛) + 1) − 1) ∈ ℕ0)
187183, 186eqeltrrd 2851 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (2 · 𝑛) ∈ ℕ0)
188187nn0ge0d 11556 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 0 ≤ (2 · 𝑛))
189176, 188syl5eqbr 4821 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (2 · 0) ≤ (2 · 𝑛))
190 0red 10243 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 0 ∈ ℝ)
191 lemul2 11078 . . . . . . . . . . . . . . . . . . . . 21 ((0 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (0 ≤ 𝑛 ↔ (2 · 0) ≤ (2 · 𝑛)))
192190, 144, 156, 158, 191syl112anc 1480 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (0 ≤ 𝑛 ↔ (2 · 0) ≤ (2 · 𝑛)))
193189, 192mpbird 247 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 0 ≤ 𝑛)
194132, 144subge02d 10821 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (0 ≤ 𝑛 ↔ (𝑀𝑛) ≤ 𝑀))
195193, 194mpbid 222 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑀𝑛) ≤ 𝑀)
196172peano2zd 11687 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((⌊‘(𝑀 / 2)) + 1) ∈ ℤ)
197 elfz 12539 . . . . . . . . . . . . . . . . . . 19 (((𝑀𝑛) ∈ ℤ ∧ ((⌊‘(𝑀 / 2)) + 1) ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑀𝑛) ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ↔ (((⌊‘(𝑀 / 2)) + 1) ≤ (𝑀𝑛) ∧ (𝑀𝑛) ≤ 𝑀)))
198139, 196, 137, 197syl3anc 1476 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((𝑀𝑛) ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ↔ (((⌊‘(𝑀 / 2)) + 1) ≤ (𝑀𝑛) ∧ (𝑀𝑛) ≤ 𝑀)))
199175, 195, 198mpbir2and 692 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑀𝑛) ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀))
20094ad2antrr 705 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑃 ∈ ℙ)
201200, 13syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑃 ∈ ℕ)
202201nncnd 11238 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑃 ∈ ℂ)
203 peano2cn 10410 . . . . . . . . . . . . . . . . . . . 20 ((2 · 𝑛) ∈ ℂ → ((2 · 𝑛) + 1) ∈ ℂ)
204181, 203syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((2 · 𝑛) + 1) ∈ ℂ)
205202, 204nncand 10599 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑃 − (𝑃 − ((2 · 𝑛) + 1))) = ((2 · 𝑛) + 1))
206 1cnd 10258 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 1 ∈ ℂ)
207202, 181, 206sub32d 10626 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((𝑃 − (2 · 𝑛)) − 1) = ((𝑃 − 1) − (2 · 𝑛)))
208202, 181, 206subsub4d 10625 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((𝑃 − (2 · 𝑛)) − 1) = (𝑃 − ((2 · 𝑛) + 1)))
209 2cnd 11295 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 2 ∈ ℂ)
210209, 165, 179subdid 10688 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (2 · (𝑀𝑛)) = ((2 · 𝑀) − (2 · 𝑛)))
211127oveq2i 6804 . . . . . . . . . . . . . . . . . . . . . . 23 (2 · 𝑀) = (2 · ((𝑃 − 1) / 2))
21214nnzd 11683 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝑃 ∈ ℤ)
213212ad2antrr 705 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑃 ∈ ℤ)
214 peano2zm 11622 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑃 ∈ ℤ → (𝑃 − 1) ∈ ℤ)
215213, 214syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑃 − 1) ∈ ℤ)
216215zcnd 11685 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑃 − 1) ∈ ℂ)
21778a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 2 ≠ 0)
218216, 209, 217divcan2d 11005 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (2 · ((𝑃 − 1) / 2)) = (𝑃 − 1))
219211, 218syl5eq 2817 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (2 · 𝑀) = (𝑃 − 1))
220219oveq1d 6808 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((2 · 𝑀) − (2 · 𝑛)) = ((𝑃 − 1) − (2 · 𝑛)))
221210, 220eqtr2d 2806 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((𝑃 − 1) − (2 · 𝑛)) = (2 · (𝑀𝑛)))
222207, 208, 2213eqtr3d 2813 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑃 − ((2 · 𝑛) + 1)) = (2 · (𝑀𝑛)))
223222oveq2d 6809 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑃 − (𝑃 − ((2 · 𝑛) + 1))) = (𝑃 − (2 · (𝑀𝑛))))
224205, 223, 1453eqtr3rd 2814 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (1st𝑧) = (𝑃 − (2 · (𝑀𝑛))))
225 oveq2 6801 . . . . . . . . . . . . . . . . . . . 20 (𝑢 = (𝑀𝑛) → (2 · 𝑢) = (2 · (𝑀𝑛)))
226225oveq2d 6809 . . . . . . . . . . . . . . . . . . 19 (𝑢 = (𝑀𝑛) → (𝑃 − (2 · 𝑢)) = (𝑃 − (2 · (𝑀𝑛))))
227226eqeq2d 2781 . . . . . . . . . . . . . . . . . 18 (𝑢 = (𝑀𝑛) → ((1st𝑧) = (𝑃 − (2 · 𝑢)) ↔ (1st𝑧) = (𝑃 − (2 · (𝑀𝑛)))))
228227rspcev 3460 . . . . . . . . . . . . . . . . 17 (((𝑀𝑛) ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ (1st𝑧) = (𝑃 − (2 · (𝑀𝑛)))) → ∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1st𝑧) = (𝑃 − (2 · 𝑢)))
229199, 224, 228syl2anc 573 . . . . . . . . . . . . . . . 16 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1st𝑧) = (𝑃 − (2 · 𝑢)))
230229rexlimdvaa 3180 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑆) → (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = (1st𝑧) → ∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1st𝑧) = (𝑃 − (2 · 𝑢))))
231126, 230sylbid 230 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑆) → (¬ 2 ∥ (1st𝑧) → ∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1st𝑧) = (𝑃 − (2 · 𝑢))))
232119, 231impbid 202 . . . . . . . . . . . . 13 ((𝜑𝑧𝑆) → (∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1st𝑧) = (𝑃 − (2 · 𝑢)) ↔ ¬ 2 ∥ (1st𝑧)))
233232rabbidva 3338 . . . . . . . . . . . 12 (𝜑 → {𝑧𝑆 ∣ ∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1st𝑧) = (𝑃 − (2 · 𝑢))} = {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})
23486, 233syl5eq 2817 . . . . . . . . . . 11 (𝜑 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} = {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})
235234fveq2d 6336 . . . . . . . . . 10 (𝜑 → (♯‘ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))}) = (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))
23631relopabi 5384 . . . . . . . . . . . . . . 15 Rel 𝑆
237 relss 5346 . . . . . . . . . . . . . . 15 ({𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} ⊆ 𝑆 → (Rel 𝑆 → Rel {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))}))
23858, 236, 237mp2 9 . . . . . . . . . . . . . 14 Rel {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))}
239 relxp 5266 . . . . . . . . . . . . . 14 Rel ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
24031eleq2i 2842 . . . . . . . . . . . . . . . . . 18 (⟨𝑥, 𝑦⟩ ∈ 𝑆 ↔ ⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))})
241 opabid 5115 . . . . . . . . . . . . . . . . . 18 (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} ↔ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))
242240, 241bitri 264 . . . . . . . . . . . . . . . . 17 (⟨𝑥, 𝑦⟩ ∈ 𝑆 ↔ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))
243 anass 459 . . . . . . . . . . . . . . . . . . 19 (((𝑦 ∈ ℕ ∧ 𝑦𝑁) ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄)) ↔ (𝑦 ∈ ℕ ∧ (𝑦𝑁 ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄))))
24424peano2zd 11687 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ∈ ℤ)
245244zred 11684 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ∈ ℝ)
246245adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ∈ ℝ)
24710ad2antrr 705 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈ ℝ)
248 nnre 11229 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
249248adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ ℝ)
250 lesub 10709 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ∈ ℝ ∧ 𝑄 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ≤ (𝑄𝑦) ↔ 𝑦 ≤ (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1))))
251246, 247, 249, 250syl3anc 1476 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ≤ (𝑄𝑦) ↔ 𝑦 ≤ (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1))))
25210adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑄 ∈ ℝ)
253252recnd 10270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑄 ∈ ℂ)
25468, 253mulcomd 10263 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 · 𝑄) = (𝑄 · 𝑃))
25570, 253mulcomd 10263 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑢) · 𝑄) = (𝑄 · (2 · 𝑢)))
25667nnne0d 11267 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ≠ 0)
257253, 68, 256divcan1d 11004 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 𝑃) · 𝑃) = 𝑄)
258257oveq1d 6808 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑄 / 𝑃) · 𝑃) · (2 · 𝑢)) = (𝑄 · (2 · 𝑢)))
25916recnd 10270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 / 𝑃) ∈ ℂ)
260259, 68, 70mul32d 10448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑄 / 𝑃) · 𝑃) · (2 · 𝑢)) = (((𝑄 / 𝑃) · (2 · 𝑢)) · 𝑃))
261255, 258, 2603eqtr2d 2811 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑢) · 𝑄) = (((𝑄 / 𝑃) · (2 · 𝑢)) · 𝑃))
262254, 261oveq12d 6811 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 · 𝑄) − ((2 · 𝑢) · 𝑄)) = ((𝑄 · 𝑃) − (((𝑄 / 𝑃) · (2 · 𝑢)) · 𝑃)))
26368, 70, 253subdird 10689 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) · 𝑄) = ((𝑃 · 𝑄) − ((2 · 𝑢) · 𝑄)))
26423recnd 10270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℂ)
265253, 264, 68subdird 10689 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃) = ((𝑄 · 𝑃) − (((𝑄 / 𝑃) · (2 · 𝑢)) · 𝑃)))
266262, 263, 2653eqtr4d 2815 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) · 𝑄) = ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃))
267266adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑃 − (2 · 𝑢)) · 𝑄) = ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃))
268267breq2d 4798 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄) ↔ (𝑦 · 𝑃) < ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃)))
26923adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ)
270247, 269resubcld 10660 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℝ)
27167adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℕ)
272271nnred 11237 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℝ)
273271nngt0d 11266 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 0 < 𝑃)
274 ltmul1 11075 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦 ∈ ℝ ∧ (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℝ ∧ (𝑃 ∈ ℝ ∧ 0 < 𝑃)) → (𝑦 < (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ↔ (𝑦 · 𝑃) < ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃)))
275249, 270, 272, 273, 274syl112anc 1480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑦 < (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ↔ (𝑦 · 𝑃) < ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃)))
276 ltsub13 10711 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦 ∈ ℝ ∧ 𝑄 ∈ ℝ ∧ ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ) → (𝑦 < (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ↔ ((𝑄 / 𝑃) · (2 · 𝑢)) < (𝑄𝑦)))
277249, 247, 269, 276syl3anc 1476 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑦 < (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ↔ ((𝑄 / 𝑃) · (2 · 𝑢)) < (𝑄𝑦)))
278268, 275, 2773bitr2d 296 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄) ↔ ((𝑄 / 𝑃) · (2 · 𝑢)) < (𝑄𝑦)))
2799adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑄 ∈ ℕ)
280279nnzd 11683 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑄 ∈ ℤ)
281 nnz 11601 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 ∈ ℕ → 𝑦 ∈ ℤ)
282 zsubcl 11621 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑄 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑄𝑦) ∈ ℤ)
283280, 281, 282syl2an 583 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑄𝑦) ∈ ℤ)
284 fllt 12815 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ ∧ (𝑄𝑦) ∈ ℤ) → (((𝑄 / 𝑃) · (2 · 𝑢)) < (𝑄𝑦) ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < (𝑄𝑦)))
285269, 283, 284syl2anc 573 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (((𝑄 / 𝑃) · (2 · 𝑢)) < (𝑄𝑦) ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < (𝑄𝑦)))
28624adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ)
287 zltp1le 11629 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ ∧ (𝑄𝑦) ∈ ℤ) → ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < (𝑄𝑦) ↔ ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ≤ (𝑄𝑦)))
288286, 283, 287syl2anc 573 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < (𝑄𝑦) ↔ ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ≤ (𝑄𝑦)))
289278, 285, 2883bitrd 294 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄) ↔ ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ≤ (𝑄𝑦)))
290 lgsquad.5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 𝑁 = ((𝑄 − 1) / 2)
291290oveq2i 6804 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (2 · 𝑁) = (2 · ((𝑄 − 1) / 2))
292 peano2rem 10550 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑄 ∈ ℝ → (𝑄 − 1) ∈ ℝ)
293252, 292syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 − 1) ∈ ℝ)
294293recnd 10270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 − 1) ∈ ℂ)
295 2cnd 11295 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 2 ∈ ℂ)
29678a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 2 ≠ 0)
297294, 295, 296divcan2d 11005 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · ((𝑄 − 1) / 2)) = (𝑄 − 1))
298291, 297syl5eq 2817 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) = (𝑄 − 1))
299298oveq1d 6808 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = ((𝑄 − 1) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
300 1cnd 10258 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 1 ∈ ℂ)
30124zcnd 11685 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℂ)
302253, 300, 301sub32d 10626 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 − 1) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = ((𝑄 − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) − 1))
303253, 301, 300subsub4d 10625 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) − 1) = (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1)))
304299, 302, 3033eqtrd 2809 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1)))
305304adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1)))
306305breq2d 4798 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ↔ 𝑦 ≤ (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1))))
307251, 289, 3063bitr4d 300 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄) ↔ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
308307anbi2d 614 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦𝑁 ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄)) ↔ (𝑦𝑁𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
309 2nn 11387 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 2 ∈ ℕ
310 oddprm 15722 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑄 ∈ (ℙ ∖ {2}) → ((𝑄 − 1) / 2) ∈ ℕ)
3116, 310syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → ((𝑄 − 1) / 2) ∈ ℕ)
312290, 311syl5eqel 2854 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝑁 ∈ ℕ)
313 nnmulcl 11245 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((2 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (2 · 𝑁) ∈ ℕ)
314309, 312, 313sylancr 575 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (2 · 𝑁) ∈ ℕ)
315314adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) ∈ ℕ)
316315nnred 11237 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) ∈ ℝ)
317312adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ∈ ℕ)
318317nnred 11237 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ∈ ℝ)
31924zred 11684 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℝ)
320312nncnd 11238 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑𝑁 ∈ ℂ)
321320adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ∈ ℂ)
3223212timesd 11477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) = (𝑁 + 𝑁))
323322oveq1d 6808 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − 𝑁) = ((𝑁 + 𝑁) − 𝑁))
324321, 321pncan2d 10596 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑁 + 𝑁) − 𝑁) = 𝑁)
325323, 324eqtrd 2805 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − 𝑁) = 𝑁)
326252rehalfcld 11481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 / 2) ∈ ℝ)
327252ltm1d 11158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 − 1) < 𝑄)
328155a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 2 ∈ ℝ)
329157a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 0 < 2)
330 ltdiv1 11089 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑄 − 1) ∈ ℝ ∧ 𝑄 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((𝑄 − 1) < 𝑄 ↔ ((𝑄 − 1) / 2) < (𝑄 / 2)))
331293, 252, 328, 329, 330syl112anc 1480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 − 1) < 𝑄 ↔ ((𝑄 − 1) / 2) < (𝑄 / 2)))
332327, 331mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 − 1) / 2) < (𝑄 / 2))
333290, 332syl5eqbr 4821 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 < (𝑄 / 2))
334318, 326, 333ltled 10387 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ≤ (𝑄 / 2))
335253, 295, 68, 296div32d 11026 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 2) · 𝑃) = (𝑄 · (𝑃 / 2)))
336131adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑀 ∈ ℝ)
337336rehalfcld 11481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑀 / 2) ∈ ℝ)
338 peano2re 10411 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((⌊‘(𝑀 / 2)) ∈ ℝ → ((⌊‘(𝑀 / 2)) + 1) ∈ ℝ)
339337, 134, 3383syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((⌊‘(𝑀 / 2)) + 1) ∈ ℝ)
34019zred 11684 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ∈ ℝ)
341 flltp1 12809 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑀 / 2) ∈ ℝ → (𝑀 / 2) < ((⌊‘(𝑀 / 2)) + 1))
342337, 341syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑀 / 2) < ((⌊‘(𝑀 / 2)) + 1))
343 elfzle1 12551 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) → ((⌊‘(𝑀 / 2)) + 1) ≤ 𝑢)
344343adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((⌊‘(𝑀 / 2)) + 1) ≤ 𝑢)
345337, 339, 340, 342, 344ltletrd 10399 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑀 / 2) < 𝑢)
346 ltdivmul 11100 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑀 ∈ ℝ ∧ 𝑢 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((𝑀 / 2) < 𝑢𝑀 < (2 · 𝑢)))
347336, 340, 328, 329, 346syl112anc 1480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑀 / 2) < 𝑢𝑀 < (2 · 𝑢)))
348345, 347mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑀 < (2 · 𝑢))
349127, 348syl5eqbrr 4822 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − 1) / 2) < (2 · 𝑢))
35067nnred 11237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℝ)
351 peano2rem 10550 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑃 ∈ ℝ → (𝑃 − 1) ∈ ℝ)
352350, 351syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − 1) ∈ ℝ)
353 ltdivmul 11100 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((𝑃 − 1) ∈ ℝ ∧ (2 · 𝑢) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (((𝑃 − 1) / 2) < (2 · 𝑢) ↔ (𝑃 − 1) < (2 · (2 · 𝑢))))
354352, 22, 328, 329, 353syl112anc 1480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑃 − 1) / 2) < (2 · 𝑢) ↔ (𝑃 − 1) < (2 · (2 · 𝑢))))
355349, 354mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − 1) < (2 · (2 · 𝑢)))
356212adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℤ)
357 zmulcl 11628 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((2 ∈ ℤ ∧ (2 · 𝑢) ∈ ℤ) → (2 · (2 · 𝑢)) ∈ ℤ)
35817, 21, 357sylancr 575 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · (2 · 𝑢)) ∈ ℤ)
359 zlem1lt 11631 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑃 ∈ ℤ ∧ (2 · (2 · 𝑢)) ∈ ℤ) → (𝑃 ≤ (2 · (2 · 𝑢)) ↔ (𝑃 − 1) < (2 · (2 · 𝑢))))
360356, 358, 359syl2anc 573 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 ≤ (2 · (2 · 𝑢)) ↔ (𝑃 − 1) < (2 · (2 · 𝑢))))
361355, 360mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ≤ (2 · (2 · 𝑢)))
362 ledivmul 11101 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑃 ∈ ℝ ∧ (2 · 𝑢) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((𝑃 / 2) ≤ (2 · 𝑢) ↔ 𝑃 ≤ (2 · (2 · 𝑢))))
363350, 22, 328, 329, 362syl112anc 1480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 / 2) ≤ (2 · 𝑢) ↔ 𝑃 ≤ (2 · (2 · 𝑢))))
364361, 363mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 / 2) ≤ (2 · 𝑢))
365350rehalfcld 11481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 / 2) ∈ ℝ)
366279nngt0d 11266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 0 < 𝑄)
367 lemul2 11078 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑃 / 2) ∈ ℝ ∧ (2 · 𝑢) ∈ ℝ ∧ (𝑄 ∈ ℝ ∧ 0 < 𝑄)) → ((𝑃 / 2) ≤ (2 · 𝑢) ↔ (𝑄 · (𝑃 / 2)) ≤ (𝑄 · (2 · 𝑢))))
368365, 22, 252, 366, 367syl112anc 1480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 / 2) ≤ (2 · 𝑢) ↔ (𝑄 · (𝑃 / 2)) ≤ (𝑄 · (2 · 𝑢))))
369364, 368mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 · (𝑃 / 2)) ≤ (𝑄 · (2 · 𝑢)))
370335, 369eqbrtrd 4808 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 2) · 𝑃) ≤ (𝑄 · (2 · 𝑢)))
371252, 22remulcld 10272 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 · (2 · 𝑢)) ∈ ℝ)
37267nngt0d 11266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 0 < 𝑃)
373 lemuldiv 11105 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑄 / 2) ∈ ℝ ∧ (𝑄 · (2 · 𝑢)) ∈ ℝ ∧ (𝑃 ∈ ℝ ∧ 0 < 𝑃)) → (((𝑄 / 2) · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ↔ (𝑄 / 2) ≤ ((𝑄 · (2 · 𝑢)) / 𝑃)))
374326, 371, 350, 372, 373syl112anc 1480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑄 / 2) · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ↔ (𝑄 / 2) ≤ ((𝑄 · (2 · 𝑢)) / 𝑃)))
375370, 374mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 / 2) ≤ ((𝑄 · (2 · 𝑢)) / 𝑃))
376253, 70, 68, 256div23d 11040 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 · (2 · 𝑢)) / 𝑃) = ((𝑄 / 𝑃) · (2 · 𝑢)))
377375, 376breqtrd 4812 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 / 2) ≤ ((𝑄 / 𝑃) · (2 · 𝑢)))
378318, 326, 23, 334, 377letrd 10396 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)))
379312nnzd 11683 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑𝑁 ∈ ℤ)
380379adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ∈ ℤ)
381 flge 12814 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ ∧ 𝑁 ∈ ℤ) → (𝑁 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)) ↔ 𝑁 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
38223, 380, 381syl2anc 573 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑁 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)) ↔ 𝑁 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
383378, 382mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))
384325, 383eqbrtrd 4808 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − 𝑁) ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))
385316, 318, 319, 384subled 10832 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ≤ 𝑁)
386385adantr 466 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ≤ 𝑁)
387315nnzd 11683 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) ∈ ℤ)
388387, 24zsubcld 11689 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℤ)
389388adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℤ)
390389zred 11684 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℝ)
391312ad2antrr 705 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑁 ∈ ℕ)
392391nnred 11237 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑁 ∈ ℝ)
393 letr 10333 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑦 ∈ ℝ ∧ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∧ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ≤ 𝑁) → 𝑦𝑁))
394249, 390, 392, 393syl3anc 1476 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∧ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ≤ 𝑁) → 𝑦𝑁))
395386, 394mpan2d 674 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) → 𝑦𝑁))
396395pm4.71rd 552 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ↔ (𝑦𝑁𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
397308, 396bitr4d 271 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦𝑁 ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄)) ↔ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
398397pm5.32da 568 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑦 ∈ ℕ ∧ (𝑦𝑁 ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
399398adantr 466 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → ((𝑦 ∈ ℕ ∧ (𝑦𝑁 ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
400243, 399syl5bb 272 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (((𝑦 ∈ ℕ ∧ 𝑦𝑁) ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄)) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
401 simpr 471 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → 𝑥 = (𝑃 − (2 · 𝑢)))
402356, 21zsubcld 11689 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − (2 · 𝑢)) ∈ ℤ)
403 elfzle2 12552 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) → 𝑢𝑀)
404403adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢𝑀)
405404, 127syl6breq 4827 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ≤ ((𝑃 − 1) / 2))
406 lemuldiv2 11106 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑢 ∈ ℝ ∧ (𝑃 − 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 𝑢) ≤ (𝑃 − 1) ↔ 𝑢 ≤ ((𝑃 − 1) / 2)))
407340, 352, 328, 329, 406syl112anc 1480 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑢) ≤ (𝑃 − 1) ↔ 𝑢 ≤ ((𝑃 − 1) / 2)))
408405, 407mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ≤ (𝑃 − 1))
409350ltm1d 11158 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − 1) < 𝑃)
41022, 352, 350, 408, 409lelttrd 10397 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) < 𝑃)
41122, 350posdifd 10816 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑢) < 𝑃 ↔ 0 < (𝑃 − (2 · 𝑢))))
412410, 411mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 0 < (𝑃 − (2 · 𝑢)))
413 elnnz 11589 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑃 − (2 · 𝑢)) ∈ ℕ ↔ ((𝑃 − (2 · 𝑢)) ∈ ℤ ∧ 0 < (𝑃 − (2 · 𝑢))))
414402, 412, 413sylanbrc 572 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − (2 · 𝑢)) ∈ ℕ)
41568, 70, 300sub32d 10626 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) − 1) = ((𝑃 − 1) − (2 · 𝑢)))
416127, 127oveq12i 6805 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑀 + 𝑀) = (((𝑃 − 1) / 2) + ((𝑃 − 1) / 2))
41767nnzd 11683 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℤ)
418417, 214syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − 1) ∈ ℤ)
419418zcnd 11685 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − 1) ∈ ℂ)
4204192halvesd 11480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑃 − 1) / 2) + ((𝑃 − 1) / 2)) = (𝑃 − 1))
421416, 420syl5eq 2817 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑀 + 𝑀) = (𝑃 − 1))
422421oveq1d 6808 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑀 + 𝑀) − 𝑀) = ((𝑃 − 1) − 𝑀))
423164adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑀 ∈ ℂ)
424423, 423pncan2d 10596 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑀 + 𝑀) − 𝑀) = 𝑀)
425422, 424eqtr3d 2807 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − 1) − 𝑀) = 𝑀)
426425, 348eqbrtrd 4808 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − 1) − 𝑀) < (2 · 𝑢))
427352, 336, 22, 426ltsub23d 10834 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − 1) − (2 · 𝑢)) < 𝑀)
428415, 427eqbrtrd 4808 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) − 1) < 𝑀)
429130adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑀 ∈ ℕ)
430429nnzd 11683 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑀 ∈ ℤ)
431 zlem1lt 11631 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑃 − (2 · 𝑢)) ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑃 − (2 · 𝑢)) ≤ 𝑀 ↔ ((𝑃 − (2 · 𝑢)) − 1) < 𝑀))
432402, 430, 431syl2anc 573 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) ≤ 𝑀 ↔ ((𝑃 − (2 · 𝑢)) − 1) < 𝑀))
433428, 432mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − (2 · 𝑢)) ≤ 𝑀)
434 fznn 12615 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑀 ∈ ℤ → ((𝑃 − (2 · 𝑢)) ∈ (1...𝑀) ↔ ((𝑃 − (2 · 𝑢)) ∈ ℕ ∧ (𝑃 − (2 · 𝑢)) ≤ 𝑀)))
435430, 434syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) ∈ (1...𝑀) ↔ ((𝑃 − (2 · 𝑢)) ∈ ℕ ∧ (𝑃 − (2 · 𝑢)) ≤ 𝑀)))
436414, 433, 435mpbir2and 692 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − (2 · 𝑢)) ∈ (1...𝑀))
437436adantr 466 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (𝑃 − (2 · 𝑢)) ∈ (1...𝑀))
438401, 437eqeltrd 2850 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → 𝑥 ∈ (1...𝑀))
439438biantrurd 522 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (𝑦 ∈ (1...𝑁) ↔ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))))
440379ad2antrr 705 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → 𝑁 ∈ ℤ)
441 fznn 12615 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ ℤ → (𝑦 ∈ (1...𝑁) ↔ (𝑦 ∈ ℕ ∧ 𝑦𝑁)))
442440, 441syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (𝑦 ∈ (1...𝑁) ↔ (𝑦 ∈ ℕ ∧ 𝑦𝑁)))
443439, 442bitr3d 270 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ↔ (𝑦 ∈ ℕ ∧ 𝑦𝑁)))
444401oveq1d 6808 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (𝑥 · 𝑄) = ((𝑃 − (2 · 𝑢)) · 𝑄))
445444breq2d 4798 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → ((𝑦 · 𝑃) < (𝑥 · 𝑄) ↔ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄)))
446443, 445anbi12d 616 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)) ↔ ((𝑦 ∈ ℕ ∧ 𝑦𝑁) ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄))))
447388adantr 466 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℤ)
448 fznn 12615 . . . . . . . . . . . . . . . . . . 19 (((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℤ → (𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
449447, 448syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
450400, 446, 4493bitr4d 300 . . . . . . . . . . . . . . . . 17 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)) ↔ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
451242, 450syl5bb 272 . . . . . . . . . . . . . . . 16 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (⟨𝑥, 𝑦⟩ ∈ 𝑆𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
452451pm5.32da 568 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑥 = (𝑃 − (2 · 𝑢)) ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑆) ↔ (𝑥 = (𝑃 − (2 · 𝑢)) ∧ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))))
453 vex 3354 . . . . . . . . . . . . . . . . . . 19 𝑥 ∈ V
454 vex 3354 . . . . . . . . . . . . . . . . . . 19 𝑦 ∈ V
455453, 454op1std 7325 . . . . . . . . . . . . . . . . . 18 (𝑧 = ⟨𝑥, 𝑦⟩ → (1st𝑧) = 𝑥)
456455eqeq1d 2773 . . . . . . . . . . . . . . . . 17 (𝑧 = ⟨𝑥, 𝑦⟩ → ((1st𝑧) = (𝑃 − (2 · 𝑢)) ↔ 𝑥 = (𝑃 − (2 · 𝑢))))
457456elrab 3515 . . . . . . . . . . . . . . . 16 (⟨𝑥, 𝑦⟩ ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} ↔ (⟨𝑥, 𝑦⟩ ∈ 𝑆𝑥 = (𝑃 − (2 · 𝑢))))
458 ancom 452 . . . . . . . . . . . . . . . 16 ((⟨𝑥, 𝑦⟩ ∈ 𝑆𝑥 = (𝑃 − (2 · 𝑢))) ↔ (𝑥 = (𝑃 − (2 · 𝑢)) ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑆))
459457, 458bitri 264 . . . . . . . . . . . . . . 15 (⟨𝑥, 𝑦⟩ ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} ↔ (𝑥 = (𝑃 − (2 · 𝑢)) ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑆))
460 opelxp 5286 . . . . . . . . . . . . . . . 16 (⟨𝑥, 𝑦⟩ ∈ ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ↔ (𝑥 ∈ {(𝑃 − (2 · 𝑢))} ∧ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
461 velsn 4332 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ {(𝑃 − (2 · 𝑢))} ↔ 𝑥 = (𝑃 − (2 · 𝑢)))
462461anbi1i 610 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ {(𝑃 − (2 · 𝑢))} ∧ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ↔ (𝑥 = (𝑃 − (2 · 𝑢)) ∧ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
463460, 462bitri 264 . . . . . . . . . . . . . . 15 (⟨𝑥, 𝑦⟩ ∈ ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ↔ (𝑥 = (𝑃 − (2 · 𝑢)) ∧ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
464452, 459, 4633bitr4g 303 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⟨𝑥, 𝑦⟩ ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} ↔ ⟨𝑥, 𝑦⟩ ∈ ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))))
465238, 239, 464eqrelrdv 5356 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} = ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
466465fveq2d 6336 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (♯‘{𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))}) = (♯‘({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))))
467 fzfid 12980 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ∈ Fin)
468 xpsnen2g 8209 . . . . . . . . . . . . . 14 (((𝑃 − (2 · 𝑢)) ∈ ℤ ∧ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ∈ Fin) → ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ≈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
469402, 467, 468syl2anc 573 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ≈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
470 hasheni 13340 . . . . . . . . . . . . 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 11076 . . . . . . . . . . . . . . . . . . . . 21 (((2 · 𝑢) ∈ ℝ ∧ 𝑃 ∈ ℝ ∧ (𝑄 ∈ ℝ ∧ 0 < 𝑄)) → ((2 · 𝑢) < 𝑃 ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · 𝑃)))
47322, 350, 252, 366, 472syl112anc 1480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑢) < 𝑃 ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · 𝑃)))
474410, 473mpbid 222 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 · (2 · 𝑢)) < (𝑄 · 𝑃))
475 ltdivmul2 11102 . . . . . . . . . . . . . . . . . . . 20 (((𝑄 · (2 · 𝑢)) ∈ ℝ ∧ 𝑄 ∈ ℝ ∧ (𝑃 ∈ ℝ ∧ 0 < 𝑃)) → (((𝑄 · (2 · 𝑢)) / 𝑃) < 𝑄 ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · 𝑃)))
476371, 252, 350, 372, 475syl112anc 1480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑄 · (2 · 𝑢)) / 𝑃) < 𝑄 ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · 𝑃)))
477474, 476mpbird 247 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 · (2 · 𝑢)) / 𝑃) < 𝑄)
478376, 477eqbrtrrd 4810 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 𝑃) · (2 · 𝑢)) < 𝑄)
479 fllt 12815 . . . . . . . . . . . . . . . . . 18 ((((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ ∧ 𝑄 ∈ ℤ) → (((𝑄 / 𝑃) · (2 · 𝑢)) < 𝑄 ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < 𝑄))
48023, 280, 479syl2anc 573 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑄 / 𝑃) · (2 · 𝑢)) < 𝑄 ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < 𝑄))
481478, 480mpbid 222 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < 𝑄)
482 zltlem1 11632 . . . . . . . . . . . . . . . . 17 (((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ ∧ 𝑄 ∈ ℤ) → ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < 𝑄 ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ≤ (𝑄 − 1)))
48324, 280, 482syl2anc 573 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < 𝑄 ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ≤ (𝑄 − 1)))
484481, 483mpbid 222 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ≤ (𝑄 − 1))
485484, 298breqtrrd 4814 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ≤ (2 · 𝑁))
486 eluz2 11894 . . . . . . . . . . . . . 14 ((2 · 𝑁) ∈ (ℤ‘(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ↔ ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ ∧ (2 · 𝑁) ∈ ℤ ∧ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ≤ (2 · 𝑁)))
48724, 387, 485, 486syl3anbrc 1428 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) ∈ (ℤ‘(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
488 uznn0sub 11921 . . . . . . . . . . . . 13 ((2 · 𝑁) ∈ (ℤ‘(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℕ0)
489 hashfz1 13338 . . . . . . . . . . . . 13 (((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℕ0 → (♯‘(1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) = ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
490487, 488, 4893syl 18 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (♯‘(1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) = ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
491466, 471, 4903eqtrd 2809 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (♯‘{𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))}) = ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
492491sumeq2dv 14641 . . . . . . . . . 10 (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(♯‘{𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))}) = Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
49385, 235, 4923eqtr3rd 2814 . . . . . . . . 9 (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))
494314nncnd 11238 . . . . . . . . . . 11 (𝜑 → (2 · 𝑁) ∈ ℂ)
495494adantr 466 . . . . . . . . . 10 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) ∈ ℂ)
4965, 495, 301fsumsub 14727 . . . . . . . . 9 (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) − Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
497493, 496eqtr3d 2807 . . . . . . . 8 (𝜑 → (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) = (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) − Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
498497oveq2d 6809 . . . . . . 7 (𝜑 → (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) = (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) − Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
49925zcnd 11685 . . . . . . . 8 (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℂ)
5005, 387fsumzcl 14674 . . . . . . . . 9 (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) ∈ ℤ)
501500zcnd 11685 . . . . . . . 8 (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) ∈ ℂ)
502499, 501pncan3d 10597 . . . . . . 7 (𝜑 → (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) − Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁))
503 fsumconst 14729 . . . . . . . . 9 (((((⌊‘(𝑀 / 2)) + 1)...𝑀) ∈ Fin ∧ (2 · 𝑁) ∈ ℂ) → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) = ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · (2 · 𝑁)))
5045, 494, 503syl2anc 573 . . . . . . . 8 (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) = ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · (2 · 𝑁)))
505 hashcl 13349 . . . . . . . . . . 11 ((((⌊‘(𝑀 / 2)) + 1)...𝑀) ∈ Fin → (♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∈ ℕ0)
5065, 505syl 17 . . . . . . . . . 10 (𝜑 → (♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∈ ℕ0)
507506nn0cnd 11555 . . . . . . . . 9 (𝜑 → (♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∈ ℂ)
508 2cnd 11295 . . . . . . . . 9 (𝜑 → 2 ∈ ℂ)
509507, 508, 320mul12d 10447 . . . . . . . 8 (𝜑 → ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · (2 · 𝑁)) = (2 · ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)))
510504, 509eqtrd 2805 . . . . . . 7 (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) = (2 · ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)))
511498, 502, 5103eqtrd 2809 . . . . . 6 (𝜑 → (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) = (2 · ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)))
512511oveq2d 6809 . . . . 5 (𝜑 → (-1↑(Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))) = (-1↑(2 · ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁))))
51317a1i 11 . . . . . 6 (𝜑 → 2 ∈ ℤ)
514506nn0zd 11682 . . . . . . 7 (𝜑 → (♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∈ ℤ)
515514, 379zmulcld 11690 . . . . . 6 (𝜑 → ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁) ∈ ℤ)
516 expmulz 13113 . . . . . 6 (((-1 ∈ ℂ ∧ -1 ≠ 0) ∧ (2 ∈ ℤ ∧ ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁) ∈ ℤ)) → (-1↑(2 · ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁))) = ((-1↑2)↑((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)))
5172, 4, 513, 515, 516syl22anc 1477 . . . . 5 (𝜑 → (-1↑(2 · ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁))) = ((-1↑2)↑((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)))
518 neg1sqe1 13166 . . . . . . 7 (-1↑2) = 1
519518oveq1i 6803 . . . . . 6 ((-1↑2)↑((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)) = (1↑((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁))
520 1exp 13096 . . . . . . 7 (((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁) ∈ ℤ → (1↑((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)) = 1)
521515, 520syl 17 . . . . . 6 (𝜑 → (1↑((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)) = 1)
522519, 521syl5eq 2817 . . . . 5 (𝜑 → ((-1↑2)↑((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)) = 1)
523512, 517, 5223eqtrd 2809 . . . 4 (𝜑 → (-1↑(Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))) = 1)
52445, 56, 5233eqtr4d 2815 . . 3 (𝜑 → ((-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) · (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))) = (-1↑(Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))))
525 expaddz 13111 . . . 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 1477 . . 3 (𝜑 → (-1↑(Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))) = ((-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) · (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))))
527524, 526eqtr2d 2806 . 2 (𝜑 → ((-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) · (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))) = ((-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) · (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))))
52826, 42, 42, 44, 527mulcan2ad 10865 1 (𝜑 → (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 382   = wceq 1631  wcel 2145  wne 2943  wral 3061  wrex 3062  {crab 3065  cdif 3720  wss 3723  {csn 4316  cop 4322   ciun 4654  Disj wdisj 4754   class class class wbr 4786  {copab 4846   × cxp 5247  Rel wrel 5254  cfv 6031  (class class class)co 6793  1st c1st 7313  cen 8106  Fincfn 8109  cc 10136  cr 10137  0cc0 10138  1c1 10139   + caddc 10141   · cmul 10143   < clt 10276  cle 10277  cmin 10468  -cneg 10469   / cdiv 10886  cn 11222  2c2 11272  0cn0 11494  cz 11579  cuz 11888  ...cfz 12533  cfl 12799  cexp 13067  chash 13321  Σcsu 14624  cdvds 15189  cprime 15592
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-inf2 8702  ax-cnex 10194  ax-resscn 10195  ax-1cn 10196  ax-icn 10197  ax-addcl 10198  ax-addrcl 10199  ax-mulcl 10200  ax-mulrcl 10201  ax-mulcom 10202  ax-addass 10203  ax-mulass 10204  ax-distr 10205  ax-i2m1 10206  ax-1ne0 10207  ax-1rid 10208  ax-rnegex 10209  ax-rrecex 10210  ax-cnre 10211  ax-pre-lttri 10212  ax-pre-lttrn 10213  ax-pre-ltadd 10214  ax-pre-mulgt0 10215  ax-pre-sup 10216
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-fal 1637  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-int 4612  df-iun 4656  df-disj 4755  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-se 5209  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-isom 6040  df-riota 6754  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-om 7213  df-1st 7315  df-2nd 7316  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-1o 7713  df-2o 7714  df-oadd 7717  df-er 7896  df-en 8110  df-dom 8111  df-sdom 8112  df-fin 8113  df-sup 8504  df-inf 8505  df-oi 8571  df-card 8965  df-pnf 10278  df-mnf 10279  df-xr 10280  df-ltxr 10281  df-le 10282  df-sub 10470  df-neg 10471  df-div 10887  df-nn 11223  df-2 11281  df-3 11282  df-n0 11495  df-z 11580  df-uz 11889  df-rp 12036  df-fz 12534  df-fzo 12674  df-fl 12801  df-seq 13009  df-exp 13068  df-hash 13322  df-cj 14047  df-re 14048  df-im 14049  df-sqrt 14183  df-abs 14184  df-clim 14427  df-sum 14625  df-dvds 15190  df-prm 15593
This theorem is referenced by:  lgsquadlem2  25327
  Copyright terms: Public domain W3C validator