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

Theorem lgsquadlem1 25396
Description: Lemma for lgsquad 25399. 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 11393 . . . 4 -1 ∈ ℂ
21a1i 11 . . 3 (𝜑 → -1 ∈ ℂ)
3 neg1ne0 11395 . . . 4 -1 ≠ 0
43a1i 11 . . 3 (𝜑 → -1 ≠ 0)
5 fzfid 12980 . . . 4 (𝜑 → (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∈ Fin)
6 lgseisen.2 . . . . . . . . . 10 (𝜑𝑄 ∈ (ℙ ∖ {2}))
7 eldifi 3894 . . . . . . . . . 10 (𝑄 ∈ (ℙ ∖ {2}) → 𝑄 ∈ ℙ)
8 prmnn 15668 . . . . . . . . . 10 (𝑄 ∈ ℙ → 𝑄 ∈ ℕ)
96, 7, 83syl 18 . . . . . . . . 9 (𝜑𝑄 ∈ ℕ)
109nnred 11291 . . . . . . . 8 (𝜑𝑄 ∈ ℝ)
11 lgseisen.1 . . . . . . . . 9 (𝜑𝑃 ∈ (ℙ ∖ {2}))
12 eldifi 3894 . . . . . . . . 9 (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℙ)
13 prmnn 15668 . . . . . . . . 9 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
1411, 12, 133syl 18 . . . . . . . 8 (𝜑𝑃 ∈ ℕ)
1510, 14nndivred 11326 . . . . . . 7 (𝜑 → (𝑄 / 𝑃) ∈ ℝ)
1615adantr 472 . . . . . 6 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 / 𝑃) ∈ ℝ)
17 2z 11656 . . . . . . . 8 2 ∈ ℤ
18 elfzelz 12549 . . . . . . . . 9 (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) → 𝑢 ∈ ℤ)
1918adantl 473 . . . . . . . 8 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ∈ ℤ)
20 zmulcl 11673 . . . . . . . 8 ((2 ∈ ℤ ∧ 𝑢 ∈ ℤ) → (2 · 𝑢) ∈ ℤ)
2117, 19, 20sylancr 581 . . . . . . 7 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ∈ ℤ)
2221zred 11729 . . . . . 6 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ∈ ℝ)
2316, 22remulcld 10324 . . . . 5 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ)
2423flcld 12807 . . . 4 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ)
255, 24fsumzcl 14751 . . 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 8438 . . . . . . 7 (((1...𝑀) ∈ Fin ∧ (1...𝑁) ∈ Fin) → ((1...𝑀) × (1...𝑁)) ∈ Fin)
3027, 28, 29syl2anc 579 . . . . . 6 (𝜑 → ((1...𝑀) × (1...𝑁)) ∈ Fin)
31 lgsquad.6 . . . . . . 7 𝑆 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))}
32 opabssxp 5363 . . . . . . 7 {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} ⊆ ((1...𝑀) × (1...𝑁))
3331, 32eqsstri 3795 . . . . . 6 𝑆 ⊆ ((1...𝑀) × (1...𝑁))
34 ssfi 8387 . . . . . 6 ((((1...𝑀) × (1...𝑁)) ∈ Fin ∧ 𝑆 ⊆ ((1...𝑀) × (1...𝑁))) → 𝑆 ∈ Fin)
3530, 33, 34sylancl 580 . . . . 5 (𝜑𝑆 ∈ Fin)
36 ssrab2 3847 . . . . 5 {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)} ⊆ 𝑆
37 ssfi 8387 . . . . 5 ((𝑆 ∈ Fin ∧ {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)} ⊆ 𝑆) → {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)} ∈ Fin)
3835, 36, 37sylancl 580 . . . 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 581 . 2 (𝜑 → (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) ∈ ℂ)
4340nn0zd 11727 . . 3 (𝜑 → (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) ∈ ℤ)
442, 4, 43expne0d 13221 . 2 (𝜑 → (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) ≠ 0)
4542, 44recidd 11050 . . . 4 (𝜑 → ((-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) · (1 / (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})))) = 1)
46 1div1e1 10971 . . . . . . . . 9 (1 / 1) = 1
4746negeqi 10528 . . . . . . . 8 -(1 / 1) = -1
48 ax-1cn 10247 . . . . . . . . 9 1 ∈ ℂ
49 ax-1ne0 10258 . . . . . . . . 9 1 ≠ 0
50 divneg2 11003 . . . . . . . . 9 ((1 ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ≠ 0) → -(1 / 1) = (1 / -1))
5148, 48, 49, 50mp3an 1585 . . . . . . . 8 -(1 / 1) = (1 / -1)
5247, 51eqtr3i 2789 . . . . . . 7 -1 = (1 / -1)
5352oveq1i 6852 . . . . . 6 (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) = ((1 / -1)↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))
542, 4, 43exprecd 13223 . . . . . 6 (𝜑 → ((1 / -1)↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) = (1 / (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))))
5553, 54syl5eq 2811 . . . . 5 (𝜑 → (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) = (1 / (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))))
5655oveq2d 6858 . . . 4 (𝜑 → ((-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) · (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))) = ((-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) · (1 / (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})))))
5735adantr 472 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑆 ∈ Fin)
58 ssrab2 3847 . . . . . . . . . . . 12 {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} ⊆ 𝑆
59 ssfi 8387 . . . . . . . . . . . 12 ((𝑆 ∈ Fin ∧ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} ⊆ 𝑆) → {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} ∈ Fin)
6057, 58, 59sylancl 580 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} ∈ Fin)
61 fveqeq2 6384 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑣 → ((1st𝑧) = (𝑃 − (2 · 𝑢)) ↔ (1st𝑣) = (𝑃 − (2 · 𝑢))))
6261elrab 3519 . . . . . . . . . . . . . . . . . . 19 (𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} ↔ (𝑣𝑆 ∧ (1st𝑣) = (𝑃 − (2 · 𝑢))))
6362simprbi 490 . . . . . . . . . . . . . . . . . 18 (𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} → (1st𝑣) = (𝑃 − (2 · 𝑢)))
6463ad2antll 720 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → (1st𝑣) = (𝑃 − (2 · 𝑢)))
6564oveq2d 6858 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → (𝑃 − (1st𝑣)) = (𝑃 − (𝑃 − (2 · 𝑢))))
6614adantr 472 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℕ)
6766nncnd 11292 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℂ)
6867adantrr 708 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → 𝑃 ∈ ℂ)
6921zcnd 11730 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ∈ ℂ)
7069adantrr 708 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → (2 · 𝑢) ∈ ℂ)
7168, 70nncand 10651 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → (𝑃 − (𝑃 − (2 · 𝑢))) = (2 · 𝑢))
7265, 71eqtrd 2799 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → (𝑃 − (1st𝑣)) = (2 · 𝑢))
7372oveq1d 6857 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → ((𝑃 − (1st𝑣)) / 2) = ((2 · 𝑢) / 2))
7419zcnd 11730 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ∈ ℂ)
7574adantrr 708 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → 𝑢 ∈ ℂ)
76 2cnd 11350 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → 2 ∈ ℂ)
77 2ne0 11383 . . . . . . . . . . . . . . . 16 2 ≠ 0
7877a1i 11 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → 2 ≠ 0)
7975, 76, 78divcan3d 11060 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → ((2 · 𝑢) / 2) = 𝑢)
8073, 79eqtrd 2799 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → ((𝑃 − (1st𝑣)) / 2) = 𝑢)
8180ralrimivva 3118 . . . . . . . . . . . 12 (𝜑 → ∀𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)∀𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} ((𝑃 − (1st𝑣)) / 2) = 𝑢)
82 invdisj 4795 . . . . . . . . . . . 12 (∀𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)∀𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} ((𝑃 − (1st𝑣)) / 2) = 𝑢Disj 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})
8381, 82syl 17 . . . . . . . . . . 11 (𝜑Disj 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})
845, 60, 83hashiun 14838 . . . . . . . . . 10 (𝜑 → (♯‘ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))}) = Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(♯‘{𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))}))
85 iunrab 4723 . . . . . . . . . . . 12 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} = {𝑧𝑆 ∣ ∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1st𝑧) = (𝑃 − (2 · 𝑢))}
86 eldifsni 4476 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ≠ 2)
8711, 86syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑃 ≠ 2)
8887necomd 2992 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 2 ≠ 𝑃)
8988neneqd 2942 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ¬ 2 = 𝑃)
9089ad2antrr 717 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ¬ 2 = 𝑃)
91 uzid 11901 . . . . . . . . . . . . . . . . . . . . 21 (2 ∈ ℤ → 2 ∈ (ℤ‘2))
9217, 91ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 2 ∈ (ℤ‘2)
9311, 12syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑃 ∈ ℙ)
9493ad2antrr 717 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℙ)
95 dvdsprm 15694 . . . . . . . . . . . . . . . . . . . 20 ((2 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) → (2 ∥ 𝑃 ↔ 2 = 𝑃))
9692, 94, 95sylancr 581 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 ∥ 𝑃 ↔ 2 = 𝑃))
9790, 96mtbird 316 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ¬ 2 ∥ 𝑃)
9814ad2antrr 717 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℕ)
9998nncnd 11292 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℂ)
10021adantlr 706 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ∈ ℤ)
101100zcnd 11730 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ∈ ℂ)
10299, 101npcand 10650 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) + (2 · 𝑢)) = 𝑃)
103102breq2d 4821 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 ∥ ((𝑃 − (2 · 𝑢)) + (2 · 𝑢)) ↔ 2 ∥ 𝑃))
10497, 103mtbird 316 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ¬ 2 ∥ ((𝑃 − (2 · 𝑢)) + (2 · 𝑢)))
10518adantl 473 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ∈ ℤ)
106 dvdsmul1 15288 . . . . . . . . . . . . . . . . . . 19 ((2 ∈ ℤ ∧ 𝑢 ∈ ℤ) → 2 ∥ (2 · 𝑢))
10717, 105, 106sylancr 581 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 2 ∥ (2 · 𝑢))
10817a1i 11 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 2 ∈ ℤ)
10998nnzd 11728 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℤ)
110109, 100zsubcld 11734 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − (2 · 𝑢)) ∈ ℤ)
111 dvds2add 15300 . . . . . . . . . . . . . . . . . . 19 ((2 ∈ ℤ ∧ (𝑃 − (2 · 𝑢)) ∈ ℤ ∧ (2 · 𝑢) ∈ ℤ) → ((2 ∥ (𝑃 − (2 · 𝑢)) ∧ 2 ∥ (2 · 𝑢)) → 2 ∥ ((𝑃 − (2 · 𝑢)) + (2 · 𝑢))))
112108, 110, 100, 111syl3anc 1490 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 ∥ (𝑃 − (2 · 𝑢)) ∧ 2 ∥ (2 · 𝑢)) → 2 ∥ ((𝑃 − (2 · 𝑢)) + (2 · 𝑢))))
113107, 112mpan2d 685 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 ∥ (𝑃 − (2 · 𝑢)) → 2 ∥ ((𝑃 − (2 · 𝑢)) + (2 · 𝑢))))
114104, 113mtod 189 . . . . . . . . . . . . . . . 16 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ¬ 2 ∥ (𝑃 − (2 · 𝑢)))
115 breq2 4813 . . . . . . . . . . . . . . . . 17 ((1st𝑧) = (𝑃 − (2 · 𝑢)) → (2 ∥ (1st𝑧) ↔ 2 ∥ (𝑃 − (2 · 𝑢))))
116115notbid 309 . . . . . . . . . . . . . . . 16 ((1st𝑧) = (𝑃 − (2 · 𝑢)) → (¬ 2 ∥ (1st𝑧) ↔ ¬ 2 ∥ (𝑃 − (2 · 𝑢))))
117114, 116syl5ibrcom 238 . . . . . . . . . . . . . . 15 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((1st𝑧) = (𝑃 − (2 · 𝑢)) → ¬ 2 ∥ (1st𝑧)))
118117rexlimdva 3178 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑆) → (∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1st𝑧) = (𝑃 − (2 · 𝑢)) → ¬ 2 ∥ (1st𝑧)))
119 simpr 477 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧𝑆) → 𝑧𝑆)
12033, 119sseldi 3759 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧𝑆) → 𝑧 ∈ ((1...𝑀) × (1...𝑁)))
121 xp1st 7398 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ ((1...𝑀) × (1...𝑁)) → (1st𝑧) ∈ (1...𝑀))
122120, 121syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑧𝑆) → (1st𝑧) ∈ (1...𝑀))
123 elfzelz 12549 . . . . . . . . . . . . . . . 16 ((1st𝑧) ∈ (1...𝑀) → (1st𝑧) ∈ ℤ)
124 odd2np1 15347 . . . . . . . . . . . . . . . 16 ((1st𝑧) ∈ ℤ → (¬ 2 ∥ (1st𝑧) ↔ ∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = (1st𝑧)))
125122, 123, 1243syl 18 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑆) → (¬ 2 ∥ (1st𝑧) ↔ ∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = (1st𝑧)))
126 lgsquad.4 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑀 = ((𝑃 − 1) / 2)
127 oddprm 15794 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑃 ∈ (ℙ ∖ {2}) → ((𝑃 − 1) / 2) ∈ ℕ)
12811, 127syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝑃 − 1) / 2) ∈ ℕ)
129126, 128syl5eqel 2848 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑀 ∈ ℕ)
130129nnred 11291 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑀 ∈ ℝ)
131130ad2antrr 717 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑀 ∈ ℝ)
132131rehalfcld 11525 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑀 / 2) ∈ ℝ)
133 reflcl 12805 . . . . . . . . . . . . . . . . . . . . 21 ((𝑀 / 2) ∈ ℝ → (⌊‘(𝑀 / 2)) ∈ ℝ)
134132, 133syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (⌊‘(𝑀 / 2)) ∈ ℝ)
135129ad2antrr 717 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑀 ∈ ℕ)
136135nnzd 11728 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑀 ∈ ℤ)
137 simprl 787 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑛 ∈ ℤ)
138136, 137zsubcld 11734 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑀𝑛) ∈ ℤ)
139138zred 11729 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑀𝑛) ∈ ℝ)
140 flle 12808 . . . . . . . . . . . . . . . . . . . . 21 ((𝑀 / 2) ∈ ℝ → (⌊‘(𝑀 / 2)) ≤ (𝑀 / 2))
141132, 140syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (⌊‘(𝑀 / 2)) ≤ (𝑀 / 2))
142 zre 11628 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ ℤ → 𝑛 ∈ ℝ)
143142ad2antrl 719 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑛 ∈ ℝ)
144 simprr 789 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((2 · 𝑛) + 1) = (1st𝑧))
145122adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (1st𝑧) ∈ (1...𝑀))
146144, 145eqeltrd 2844 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((2 · 𝑛) + 1) ∈ (1...𝑀))
147 elfzle2 12552 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((2 · 𝑛) + 1) ∈ (1...𝑀) → ((2 · 𝑛) + 1) ≤ 𝑀)
148146, 147syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((2 · 𝑛) + 1) ≤ 𝑀)
149 zmulcl 11673 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((2 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (2 · 𝑛) ∈ ℤ)
15017, 137, 149sylancr 581 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (2 · 𝑛) ∈ ℤ)
151 zltp1le 11674 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((2 · 𝑛) ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((2 · 𝑛) < 𝑀 ↔ ((2 · 𝑛) + 1) ≤ 𝑀))
152150, 136, 151syl2anc 579 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((2 · 𝑛) < 𝑀 ↔ ((2 · 𝑛) + 1) ≤ 𝑀))
153148, 152mpbird 248 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (2 · 𝑛) < 𝑀)
154 2re 11346 . . . . . . . . . . . . . . . . . . . . . . . . 25 2 ∈ ℝ
155154a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 2 ∈ ℝ)
156 2pos 11382 . . . . . . . . . . . . . . . . . . . . . . . . 25 0 < 2
157156a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 0 < 2)
158 ltmuldiv2 11151 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 𝑛) < 𝑀𝑛 < (𝑀 / 2)))
159143, 131, 155, 157, 158syl112anc 1493 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((2 · 𝑛) < 𝑀𝑛 < (𝑀 / 2)))
160153, 159mpbid 223 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑛 < (𝑀 / 2))
161132recnd 10322 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑀 / 2) ∈ ℂ)
162161, 161pncan2d 10648 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (((𝑀 / 2) + (𝑀 / 2)) − (𝑀 / 2)) = (𝑀 / 2))
163129nncnd 11292 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝑀 ∈ ℂ)
164163ad2antrr 717 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑀 ∈ ℂ)
1651642halvesd 11524 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((𝑀 / 2) + (𝑀 / 2)) = 𝑀)
166165oveq1d 6857 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (((𝑀 / 2) + (𝑀 / 2)) − (𝑀 / 2)) = (𝑀 − (𝑀 / 2)))
167162, 166eqtr3d 2801 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑀 / 2) = (𝑀 − (𝑀 / 2)))
168160, 167breqtrd 4835 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑛 < (𝑀 − (𝑀 / 2)))
169143, 131, 132, 168ltsub13d 10887 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑀 / 2) < (𝑀𝑛))
170134, 132, 139, 141, 169lelttrd 10449 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (⌊‘(𝑀 / 2)) < (𝑀𝑛))
171132flcld 12807 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (⌊‘(𝑀 / 2)) ∈ ℤ)
172 zltp1le 11674 . . . . . . . . . . . . . . . . . . . 20 (((⌊‘(𝑀 / 2)) ∈ ℤ ∧ (𝑀𝑛) ∈ ℤ) → ((⌊‘(𝑀 / 2)) < (𝑀𝑛) ↔ ((⌊‘(𝑀 / 2)) + 1) ≤ (𝑀𝑛)))
173171, 138, 172syl2anc 579 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((⌊‘(𝑀 / 2)) < (𝑀𝑛) ↔ ((⌊‘(𝑀 / 2)) + 1) ≤ (𝑀𝑛)))
174170, 173mpbid 223 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((⌊‘(𝑀 / 2)) + 1) ≤ (𝑀𝑛))
175 2t0e0 11447 . . . . . . . . . . . . . . . . . . . . 21 (2 · 0) = 0
176 2cn 11347 . . . . . . . . . . . . . . . . . . . . . . . . 25 2 ∈ ℂ
177 zcn 11629 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 ∈ ℤ → 𝑛 ∈ ℂ)
178177ad2antrl 719 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑛 ∈ ℂ)
179 mulcl 10273 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((2 ∈ ℂ ∧ 𝑛 ∈ ℂ) → (2 · 𝑛) ∈ ℂ)
180176, 178, 179sylancr 581 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (2 · 𝑛) ∈ ℂ)
181 pncan 10541 . . . . . . . . . . . . . . . . . . . . . . . 24 (((2 · 𝑛) ∈ ℂ ∧ 1 ∈ ℂ) → (((2 · 𝑛) + 1) − 1) = (2 · 𝑛))
182180, 48, 181sylancl 580 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (((2 · 𝑛) + 1) − 1) = (2 · 𝑛))
183 elfznn 12577 . . . . . . . . . . . . . . . . . . . . . . . 24 (((2 · 𝑛) + 1) ∈ (1...𝑀) → ((2 · 𝑛) + 1) ∈ ℕ)
184 nnm1nn0 11581 . . . . . . . . . . . . . . . . . . . . . . . 24 (((2 · 𝑛) + 1) ∈ ℕ → (((2 · 𝑛) + 1) − 1) ∈ ℕ0)
185146, 183, 1843syl 18 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (((2 · 𝑛) + 1) − 1) ∈ ℕ0)
186182, 185eqeltrrd 2845 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (2 · 𝑛) ∈ ℕ0)
187186nn0ge0d 11601 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 0 ≤ (2 · 𝑛))
188175, 187syl5eqbr 4844 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (2 · 0) ≤ (2 · 𝑛))
189 0red 10297 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 0 ∈ ℝ)
190 lemul2 11130 . . . . . . . . . . . . . . . . . . . . 21 ((0 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (0 ≤ 𝑛 ↔ (2 · 0) ≤ (2 · 𝑛)))
191189, 143, 155, 157, 190syl112anc 1493 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (0 ≤ 𝑛 ↔ (2 · 0) ≤ (2 · 𝑛)))
192188, 191mpbird 248 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 0 ≤ 𝑛)
193131, 143subge02d 10873 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (0 ≤ 𝑛 ↔ (𝑀𝑛) ≤ 𝑀))
194192, 193mpbid 223 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑀𝑛) ≤ 𝑀)
195171peano2zd 11732 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((⌊‘(𝑀 / 2)) + 1) ∈ ℤ)
196 elfz 12539 . . . . . . . . . . . . . . . . . . 19 (((𝑀𝑛) ∈ ℤ ∧ ((⌊‘(𝑀 / 2)) + 1) ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑀𝑛) ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ↔ (((⌊‘(𝑀 / 2)) + 1) ≤ (𝑀𝑛) ∧ (𝑀𝑛) ≤ 𝑀)))
197138, 195, 136, 196syl3anc 1490 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((𝑀𝑛) ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ↔ (((⌊‘(𝑀 / 2)) + 1) ≤ (𝑀𝑛) ∧ (𝑀𝑛) ≤ 𝑀)))
198174, 194, 197mpbir2and 704 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑀𝑛) ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀))
19993ad2antrr 717 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑃 ∈ ℙ)
200199, 13syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑃 ∈ ℕ)
201200nncnd 11292 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑃 ∈ ℂ)
202 peano2cn 10462 . . . . . . . . . . . . . . . . . . . 20 ((2 · 𝑛) ∈ ℂ → ((2 · 𝑛) + 1) ∈ ℂ)
203180, 202syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((2 · 𝑛) + 1) ∈ ℂ)
204201, 203nncand 10651 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑃 − (𝑃 − ((2 · 𝑛) + 1))) = ((2 · 𝑛) + 1))
205 1cnd 10288 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 1 ∈ ℂ)
206201, 180, 205sub32d 10678 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((𝑃 − (2 · 𝑛)) − 1) = ((𝑃 − 1) − (2 · 𝑛)))
207201, 180, 205subsub4d 10677 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((𝑃 − (2 · 𝑛)) − 1) = (𝑃 − ((2 · 𝑛) + 1)))
208 2cnd 11350 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 2 ∈ ℂ)
209208, 164, 178subdid 10740 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (2 · (𝑀𝑛)) = ((2 · 𝑀) − (2 · 𝑛)))
210126oveq2i 6853 . . . . . . . . . . . . . . . . . . . . . . 23 (2 · 𝑀) = (2 · ((𝑃 − 1) / 2))
21114nnzd 11728 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝑃 ∈ ℤ)
212211ad2antrr 717 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑃 ∈ ℤ)
213 peano2zm 11667 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑃 ∈ ℤ → (𝑃 − 1) ∈ ℤ)
214212, 213syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑃 − 1) ∈ ℤ)
215214zcnd 11730 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑃 − 1) ∈ ℂ)
21677a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 2 ≠ 0)
217215, 208, 216divcan2d 11057 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (2 · ((𝑃 − 1) / 2)) = (𝑃 − 1))
218210, 217syl5eq 2811 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (2 · 𝑀) = (𝑃 − 1))
219218oveq1d 6857 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((2 · 𝑀) − (2 · 𝑛)) = ((𝑃 − 1) − (2 · 𝑛)))
220209, 219eqtr2d 2800 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((𝑃 − 1) − (2 · 𝑛)) = (2 · (𝑀𝑛)))
221206, 207, 2203eqtr3d 2807 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑃 − ((2 · 𝑛) + 1)) = (2 · (𝑀𝑛)))
222221oveq2d 6858 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑃 − (𝑃 − ((2 · 𝑛) + 1))) = (𝑃 − (2 · (𝑀𝑛))))
223204, 222, 1443eqtr3rd 2808 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (1st𝑧) = (𝑃 − (2 · (𝑀𝑛))))
224 oveq2 6850 . . . . . . . . . . . . . . . . . . 19 (𝑢 = (𝑀𝑛) → (2 · 𝑢) = (2 · (𝑀𝑛)))
225224oveq2d 6858 . . . . . . . . . . . . . . . . . 18 (𝑢 = (𝑀𝑛) → (𝑃 − (2 · 𝑢)) = (𝑃 − (2 · (𝑀𝑛))))
226225rspceeqv 3479 . . . . . . . . . . . . . . . . 17 (((𝑀𝑛) ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ (1st𝑧) = (𝑃 − (2 · (𝑀𝑛)))) → ∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1st𝑧) = (𝑃 − (2 · 𝑢)))
227198, 223, 226syl2anc 579 . . . . . . . . . . . . . . . 16 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1st𝑧) = (𝑃 − (2 · 𝑢)))
228227rexlimdvaa 3179 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑆) → (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = (1st𝑧) → ∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1st𝑧) = (𝑃 − (2 · 𝑢))))
229125, 228sylbid 231 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑆) → (¬ 2 ∥ (1st𝑧) → ∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1st𝑧) = (𝑃 − (2 · 𝑢))))
230118, 229impbid 203 . . . . . . . . . . . . 13 ((𝜑𝑧𝑆) → (∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1st𝑧) = (𝑃 − (2 · 𝑢)) ↔ ¬ 2 ∥ (1st𝑧)))
231230rabbidva 3337 . . . . . . . . . . . 12 (𝜑 → {𝑧𝑆 ∣ ∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1st𝑧) = (𝑃 − (2 · 𝑢))} = {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})
23285, 231syl5eq 2811 . . . . . . . . . . 11 (𝜑 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} = {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})
233232fveq2d 6379 . . . . . . . . . 10 (𝜑 → (♯‘ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))}) = (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))
23431relopabi 5414 . . . . . . . . . . . . . . 15 Rel 𝑆
235 relss 5376 . . . . . . . . . . . . . . 15 ({𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} ⊆ 𝑆 → (Rel 𝑆 → Rel {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))}))
23658, 234, 235mp2 9 . . . . . . . . . . . . . 14 Rel {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))}
237 relxp 5295 . . . . . . . . . . . . . 14 Rel ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
23831eleq2i 2836 . . . . . . . . . . . . . . . . . 18 (⟨𝑥, 𝑦⟩ ∈ 𝑆 ↔ ⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))})
239 opabid 5143 . . . . . . . . . . . . . . . . . 18 (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} ↔ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))
240238, 239bitri 266 . . . . . . . . . . . . . . . . 17 (⟨𝑥, 𝑦⟩ ∈ 𝑆 ↔ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))
241 anass 460 . . . . . . . . . . . . . . . . . . 19 (((𝑦 ∈ ℕ ∧ 𝑦𝑁) ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄)) ↔ (𝑦 ∈ ℕ ∧ (𝑦𝑁 ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄))))
24224peano2zd 11732 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ∈ ℤ)
243242zred 11729 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ∈ ℝ)
244243adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ∈ ℝ)
24510ad2antrr 717 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈ ℝ)
246 nnre 11282 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
247246adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ ℝ)
248 lesub 10761 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ∈ ℝ ∧ 𝑄 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ≤ (𝑄𝑦) ↔ 𝑦 ≤ (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1))))
249244, 245, 247, 248syl3anc 1490 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ≤ (𝑄𝑦) ↔ 𝑦 ≤ (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1))))
25010adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑄 ∈ ℝ)
251250recnd 10322 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑄 ∈ ℂ)
25267, 251mulcomd 10315 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 · 𝑄) = (𝑄 · 𝑃))
25369, 251mulcomd 10315 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑢) · 𝑄) = (𝑄 · (2 · 𝑢)))
25466nnne0d 11322 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ≠ 0)
255251, 67, 254divcan1d 11056 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 𝑃) · 𝑃) = 𝑄)
256255oveq1d 6857 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑄 / 𝑃) · 𝑃) · (2 · 𝑢)) = (𝑄 · (2 · 𝑢)))
25716recnd 10322 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 / 𝑃) ∈ ℂ)
258257, 67, 69mul32d 10500 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑄 / 𝑃) · 𝑃) · (2 · 𝑢)) = (((𝑄 / 𝑃) · (2 · 𝑢)) · 𝑃))
259253, 256, 2583eqtr2d 2805 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑢) · 𝑄) = (((𝑄 / 𝑃) · (2 · 𝑢)) · 𝑃))
260252, 259oveq12d 6860 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 · 𝑄) − ((2 · 𝑢) · 𝑄)) = ((𝑄 · 𝑃) − (((𝑄 / 𝑃) · (2 · 𝑢)) · 𝑃)))
26167, 69, 251subdird 10741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) · 𝑄) = ((𝑃 · 𝑄) − ((2 · 𝑢) · 𝑄)))
26223recnd 10322 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℂ)
263251, 262, 67subdird 10741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃) = ((𝑄 · 𝑃) − (((𝑄 / 𝑃) · (2 · 𝑢)) · 𝑃)))
264260, 261, 2633eqtr4d 2809 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) · 𝑄) = ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃))
265264adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑃 − (2 · 𝑢)) · 𝑄) = ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃))
266265breq2d 4821 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄) ↔ (𝑦 · 𝑃) < ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃)))
26723adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ)
268245, 267resubcld 10712 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℝ)
26966adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℕ)
270269nnred 11291 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℝ)
271269nngt0d 11321 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 0 < 𝑃)
272 ltmul1 11127 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦 ∈ ℝ ∧ (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℝ ∧ (𝑃 ∈ ℝ ∧ 0 < 𝑃)) → (𝑦 < (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ↔ (𝑦 · 𝑃) < ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃)))
273247, 268, 270, 271, 272syl112anc 1493 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑦 < (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ↔ (𝑦 · 𝑃) < ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃)))
274 ltsub13 10763 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦 ∈ ℝ ∧ 𝑄 ∈ ℝ ∧ ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ) → (𝑦 < (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ↔ ((𝑄 / 𝑃) · (2 · 𝑢)) < (𝑄𝑦)))
275247, 245, 267, 274syl3anc 1490 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑦 < (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ↔ ((𝑄 / 𝑃) · (2 · 𝑢)) < (𝑄𝑦)))
276266, 273, 2753bitr2d 298 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄) ↔ ((𝑄 / 𝑃) · (2 · 𝑢)) < (𝑄𝑦)))
2779adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑄 ∈ ℕ)
278277nnzd 11728 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑄 ∈ ℤ)
279 nnz 11646 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 ∈ ℕ → 𝑦 ∈ ℤ)
280 zsubcl 11666 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑄 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑄𝑦) ∈ ℤ)
281278, 279, 280syl2an 589 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑄𝑦) ∈ ℤ)
282 fllt 12815 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ ∧ (𝑄𝑦) ∈ ℤ) → (((𝑄 / 𝑃) · (2 · 𝑢)) < (𝑄𝑦) ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < (𝑄𝑦)))
283267, 281, 282syl2anc 579 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (((𝑄 / 𝑃) · (2 · 𝑢)) < (𝑄𝑦) ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < (𝑄𝑦)))
28424adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ)
285 zltp1le 11674 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ ∧ (𝑄𝑦) ∈ ℤ) → ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < (𝑄𝑦) ↔ ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ≤ (𝑄𝑦)))
286284, 281, 285syl2anc 579 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < (𝑄𝑦) ↔ ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ≤ (𝑄𝑦)))
287276, 283, 2863bitrd 296 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄) ↔ ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ≤ (𝑄𝑦)))
288 lgsquad.5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 𝑁 = ((𝑄 − 1) / 2)
289288oveq2i 6853 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (2 · 𝑁) = (2 · ((𝑄 − 1) / 2))
290 peano2rem 10602 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑄 ∈ ℝ → (𝑄 − 1) ∈ ℝ)
291250, 290syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 − 1) ∈ ℝ)
292291recnd 10322 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 − 1) ∈ ℂ)
293 2cnd 11350 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 2 ∈ ℂ)
29477a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 2 ≠ 0)
295292, 293, 294divcan2d 11057 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · ((𝑄 − 1) / 2)) = (𝑄 − 1))
296289, 295syl5eq 2811 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) = (𝑄 − 1))
297296oveq1d 6857 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = ((𝑄 − 1) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
298 1cnd 10288 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 1 ∈ ℂ)
29924zcnd 11730 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℂ)
300251, 298, 299sub32d 10678 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 − 1) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = ((𝑄 − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) − 1))
301251, 299, 298subsub4d 10677 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) − 1) = (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1)))
302297, 300, 3013eqtrd 2803 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1)))
303302adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1)))
304303breq2d 4821 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ↔ 𝑦 ≤ (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1))))
305249, 287, 3043bitr4d 302 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄) ↔ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
306305anbi2d 622 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦𝑁 ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄)) ↔ (𝑦𝑁𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
307 2nn 11345 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 2 ∈ ℕ
308 oddprm 15794 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑄 ∈ (ℙ ∖ {2}) → ((𝑄 − 1) / 2) ∈ ℕ)
3096, 308syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → ((𝑄 − 1) / 2) ∈ ℕ)
310288, 309syl5eqel 2848 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝑁 ∈ ℕ)
311 nnmulcl 11299 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((2 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (2 · 𝑁) ∈ ℕ)
312307, 310, 311sylancr 581 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (2 · 𝑁) ∈ ℕ)
313312adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) ∈ ℕ)
314313nnred 11291 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) ∈ ℝ)
315310adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ∈ ℕ)
316315nnred 11291 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ∈ ℝ)
31724zred 11729 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℝ)
318310nncnd 11292 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑𝑁 ∈ ℂ)
319318adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ∈ ℂ)
3203192timesd 11521 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) = (𝑁 + 𝑁))
321320oveq1d 6857 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − 𝑁) = ((𝑁 + 𝑁) − 𝑁))
322319, 319pncan2d 10648 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑁 + 𝑁) − 𝑁) = 𝑁)
323321, 322eqtrd 2799 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − 𝑁) = 𝑁)
324250rehalfcld 11525 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 / 2) ∈ ℝ)
325250ltm1d 11210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 − 1) < 𝑄)
326154a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 2 ∈ ℝ)
327156a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 0 < 2)
328 ltdiv1 11141 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑄 − 1) ∈ ℝ ∧ 𝑄 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((𝑄 − 1) < 𝑄 ↔ ((𝑄 − 1) / 2) < (𝑄 / 2)))
329291, 250, 326, 327, 328syl112anc 1493 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 − 1) < 𝑄 ↔ ((𝑄 − 1) / 2) < (𝑄 / 2)))
330325, 329mpbid 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 − 1) / 2) < (𝑄 / 2))
331288, 330syl5eqbr 4844 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 < (𝑄 / 2))
332316, 324, 331ltled 10439 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ≤ (𝑄 / 2))
333251, 293, 67, 294div32d 11078 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 2) · 𝑃) = (𝑄 · (𝑃 / 2)))
334130adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑀 ∈ ℝ)
335334rehalfcld 11525 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑀 / 2) ∈ ℝ)
336 peano2re 10463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((⌊‘(𝑀 / 2)) ∈ ℝ → ((⌊‘(𝑀 / 2)) + 1) ∈ ℝ)
337335, 133, 3363syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((⌊‘(𝑀 / 2)) + 1) ∈ ℝ)
33819zred 11729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ∈ ℝ)
339 flltp1 12809 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑀 / 2) ∈ ℝ → (𝑀 / 2) < ((⌊‘(𝑀 / 2)) + 1))
340335, 339syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑀 / 2) < ((⌊‘(𝑀 / 2)) + 1))
341 elfzle1 12551 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) → ((⌊‘(𝑀 / 2)) + 1) ≤ 𝑢)
342341adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((⌊‘(𝑀 / 2)) + 1) ≤ 𝑢)
343335, 337, 338, 340, 342ltletrd 10451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑀 / 2) < 𝑢)
344 ltdivmul 11152 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑀 ∈ ℝ ∧ 𝑢 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((𝑀 / 2) < 𝑢𝑀 < (2 · 𝑢)))
345334, 338, 326, 327, 344syl112anc 1493 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑀 / 2) < 𝑢𝑀 < (2 · 𝑢)))
346343, 345mpbid 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑀 < (2 · 𝑢))
347126, 346syl5eqbrr 4845 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − 1) / 2) < (2 · 𝑢))
34866nnred 11291 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℝ)
349 peano2rem 10602 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑃 ∈ ℝ → (𝑃 − 1) ∈ ℝ)
350348, 349syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − 1) ∈ ℝ)
351 ltdivmul 11152 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((𝑃 − 1) ∈ ℝ ∧ (2 · 𝑢) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (((𝑃 − 1) / 2) < (2 · 𝑢) ↔ (𝑃 − 1) < (2 · (2 · 𝑢))))
352350, 22, 326, 327, 351syl112anc 1493 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑃 − 1) / 2) < (2 · 𝑢) ↔ (𝑃 − 1) < (2 · (2 · 𝑢))))
353347, 352mpbid 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − 1) < (2 · (2 · 𝑢)))
354211adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℤ)
355 zmulcl 11673 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((2 ∈ ℤ ∧ (2 · 𝑢) ∈ ℤ) → (2 · (2 · 𝑢)) ∈ ℤ)
35617, 21, 355sylancr 581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · (2 · 𝑢)) ∈ ℤ)
357 zlem1lt 11676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑃 ∈ ℤ ∧ (2 · (2 · 𝑢)) ∈ ℤ) → (𝑃 ≤ (2 · (2 · 𝑢)) ↔ (𝑃 − 1) < (2 · (2 · 𝑢))))
358354, 356, 357syl2anc 579 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 ≤ (2 · (2 · 𝑢)) ↔ (𝑃 − 1) < (2 · (2 · 𝑢))))
359353, 358mpbird 248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ≤ (2 · (2 · 𝑢)))
360 ledivmul 11153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑃 ∈ ℝ ∧ (2 · 𝑢) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((𝑃 / 2) ≤ (2 · 𝑢) ↔ 𝑃 ≤ (2 · (2 · 𝑢))))
361348, 22, 326, 327, 360syl112anc 1493 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 / 2) ≤ (2 · 𝑢) ↔ 𝑃 ≤ (2 · (2 · 𝑢))))
362359, 361mpbird 248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 / 2) ≤ (2 · 𝑢))
363348rehalfcld 11525 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 / 2) ∈ ℝ)
364277nngt0d 11321 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 0 < 𝑄)
365 lemul2 11130 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑃 / 2) ∈ ℝ ∧ (2 · 𝑢) ∈ ℝ ∧ (𝑄 ∈ ℝ ∧ 0 < 𝑄)) → ((𝑃 / 2) ≤ (2 · 𝑢) ↔ (𝑄 · (𝑃 / 2)) ≤ (𝑄 · (2 · 𝑢))))
366363, 22, 250, 364, 365syl112anc 1493 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 / 2) ≤ (2 · 𝑢) ↔ (𝑄 · (𝑃 / 2)) ≤ (𝑄 · (2 · 𝑢))))
367362, 366mpbid 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 · (𝑃 / 2)) ≤ (𝑄 · (2 · 𝑢)))
368333, 367eqbrtrd 4831 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 2) · 𝑃) ≤ (𝑄 · (2 · 𝑢)))
369250, 22remulcld 10324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 · (2 · 𝑢)) ∈ ℝ)
37066nngt0d 11321 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 0 < 𝑃)
371 lemuldiv 11157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑄 / 2) ∈ ℝ ∧ (𝑄 · (2 · 𝑢)) ∈ ℝ ∧ (𝑃 ∈ ℝ ∧ 0 < 𝑃)) → (((𝑄 / 2) · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ↔ (𝑄 / 2) ≤ ((𝑄 · (2 · 𝑢)) / 𝑃)))
372324, 369, 348, 370, 371syl112anc 1493 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑄 / 2) · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ↔ (𝑄 / 2) ≤ ((𝑄 · (2 · 𝑢)) / 𝑃)))
373368, 372mpbid 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 / 2) ≤ ((𝑄 · (2 · 𝑢)) / 𝑃))
374251, 69, 67, 254div23d 11092 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 · (2 · 𝑢)) / 𝑃) = ((𝑄 / 𝑃) · (2 · 𝑢)))
375373, 374breqtrd 4835 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 / 2) ≤ ((𝑄 / 𝑃) · (2 · 𝑢)))
376316, 324, 23, 332, 375letrd 10448 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)))
377310nnzd 11728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑𝑁 ∈ ℤ)
378377adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ∈ ℤ)
379 flge 12814 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ ∧ 𝑁 ∈ ℤ) → (𝑁 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)) ↔ 𝑁 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
38023, 378, 379syl2anc 579 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑁 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)) ↔ 𝑁 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
381376, 380mpbid 223 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))
382323, 381eqbrtrd 4831 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − 𝑁) ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))
383314, 316, 317, 382subled 10884 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ≤ 𝑁)
384383adantr 472 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ≤ 𝑁)
385313nnzd 11728 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) ∈ ℤ)
386385, 24zsubcld 11734 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℤ)
387386adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℤ)
388387zred 11729 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℝ)
389310ad2antrr 717 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑁 ∈ ℕ)
390389nnred 11291 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑁 ∈ ℝ)
391 letr 10385 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑦 ∈ ℝ ∧ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∧ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ≤ 𝑁) → 𝑦𝑁))
392247, 388, 390, 391syl3anc 1490 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∧ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ≤ 𝑁) → 𝑦𝑁))
393384, 392mpan2d 685 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) → 𝑦𝑁))
394393pm4.71rd 558 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ↔ (𝑦𝑁𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
395306, 394bitr4d 273 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦𝑁 ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄)) ↔ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
396395pm5.32da 574 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑦 ∈ ℕ ∧ (𝑦𝑁 ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
397396adantr 472 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → ((𝑦 ∈ ℕ ∧ (𝑦𝑁 ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
398241, 397syl5bb 274 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (((𝑦 ∈ ℕ ∧ 𝑦𝑁) ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄)) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
399 simpr 477 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → 𝑥 = (𝑃 − (2 · 𝑢)))
400354, 21zsubcld 11734 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − (2 · 𝑢)) ∈ ℤ)
401 elfzle2 12552 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) → 𝑢𝑀)
402401adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢𝑀)
403402, 126syl6breq 4850 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ≤ ((𝑃 − 1) / 2))
404 lemuldiv2 11158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑢 ∈ ℝ ∧ (𝑃 − 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 𝑢) ≤ (𝑃 − 1) ↔ 𝑢 ≤ ((𝑃 − 1) / 2)))
405338, 350, 326, 327, 404syl112anc 1493 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑢) ≤ (𝑃 − 1) ↔ 𝑢 ≤ ((𝑃 − 1) / 2)))
406403, 405mpbird 248 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ≤ (𝑃 − 1))
407348ltm1d 11210 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − 1) < 𝑃)
40822, 350, 348, 406, 407lelttrd 10449 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) < 𝑃)
40922, 348posdifd 10868 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑢) < 𝑃 ↔ 0 < (𝑃 − (2 · 𝑢))))
410408, 409mpbid 223 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 0 < (𝑃 − (2 · 𝑢)))
411 elnnz 11634 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑃 − (2 · 𝑢)) ∈ ℕ ↔ ((𝑃 − (2 · 𝑢)) ∈ ℤ ∧ 0 < (𝑃 − (2 · 𝑢))))
412400, 410, 411sylanbrc 578 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − (2 · 𝑢)) ∈ ℕ)
41367, 69, 298sub32d 10678 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) − 1) = ((𝑃 − 1) − (2 · 𝑢)))
414126, 126oveq12i 6854 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑀 + 𝑀) = (((𝑃 − 1) / 2) + ((𝑃 − 1) / 2))
41566nnzd 11728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℤ)
416415, 213syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − 1) ∈ ℤ)
417416zcnd 11730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − 1) ∈ ℂ)
4184172halvesd 11524 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑃 − 1) / 2) + ((𝑃 − 1) / 2)) = (𝑃 − 1))
419414, 418syl5eq 2811 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑀 + 𝑀) = (𝑃 − 1))
420419oveq1d 6857 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑀 + 𝑀) − 𝑀) = ((𝑃 − 1) − 𝑀))
421163adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑀 ∈ ℂ)
422421, 421pncan2d 10648 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑀 + 𝑀) − 𝑀) = 𝑀)
423420, 422eqtr3d 2801 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − 1) − 𝑀) = 𝑀)
424423, 346eqbrtrd 4831 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − 1) − 𝑀) < (2 · 𝑢))
425350, 334, 22, 424ltsub23d 10886 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − 1) − (2 · 𝑢)) < 𝑀)
426413, 425eqbrtrd 4831 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) − 1) < 𝑀)
427129adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑀 ∈ ℕ)
428427nnzd 11728 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑀 ∈ ℤ)
429 zlem1lt 11676 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑃 − (2 · 𝑢)) ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑃 − (2 · 𝑢)) ≤ 𝑀 ↔ ((𝑃 − (2 · 𝑢)) − 1) < 𝑀))
430400, 428, 429syl2anc 579 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) ≤ 𝑀 ↔ ((𝑃 − (2 · 𝑢)) − 1) < 𝑀))
431426, 430mpbird 248 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − (2 · 𝑢)) ≤ 𝑀)
432 fznn 12615 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑀 ∈ ℤ → ((𝑃 − (2 · 𝑢)) ∈ (1...𝑀) ↔ ((𝑃 − (2 · 𝑢)) ∈ ℕ ∧ (𝑃 − (2 · 𝑢)) ≤ 𝑀)))
433428, 432syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) ∈ (1...𝑀) ↔ ((𝑃 − (2 · 𝑢)) ∈ ℕ ∧ (𝑃 − (2 · 𝑢)) ≤ 𝑀)))
434412, 431, 433mpbir2and 704 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − (2 · 𝑢)) ∈ (1...𝑀))
435434adantr 472 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (𝑃 − (2 · 𝑢)) ∈ (1...𝑀))
436399, 435eqeltrd 2844 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → 𝑥 ∈ (1...𝑀))
437436biantrurd 528 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (𝑦 ∈ (1...𝑁) ↔ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))))
438377ad2antrr 717 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → 𝑁 ∈ ℤ)
439 fznn 12615 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ ℤ → (𝑦 ∈ (1...𝑁) ↔ (𝑦 ∈ ℕ ∧ 𝑦𝑁)))
440438, 439syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (𝑦 ∈ (1...𝑁) ↔ (𝑦 ∈ ℕ ∧ 𝑦𝑁)))
441437, 440bitr3d 272 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ↔ (𝑦 ∈ ℕ ∧ 𝑦𝑁)))
442399oveq1d 6857 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (𝑥 · 𝑄) = ((𝑃 − (2 · 𝑢)) · 𝑄))
443442breq2d 4821 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → ((𝑦 · 𝑃) < (𝑥 · 𝑄) ↔ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄)))
444441, 443anbi12d 624 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)) ↔ ((𝑦 ∈ ℕ ∧ 𝑦𝑁) ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄))))
445386adantr 472 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℤ)
446 fznn 12615 . . . . . . . . . . . . . . . . . . 19 (((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℤ → (𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
447445, 446syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
448398, 444, 4473bitr4d 302 . . . . . . . . . . . . . . . . 17 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)) ↔ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
449240, 448syl5bb 274 . . . . . . . . . . . . . . . 16 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (⟨𝑥, 𝑦⟩ ∈ 𝑆𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
450449pm5.32da 574 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑥 = (𝑃 − (2 · 𝑢)) ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑆) ↔ (𝑥 = (𝑃 − (2 · 𝑢)) ∧ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))))
451 vex 3353 . . . . . . . . . . . . . . . . . . 19 𝑥 ∈ V
452 vex 3353 . . . . . . . . . . . . . . . . . . 19 𝑦 ∈ V
453451, 452op1std 7376 . . . . . . . . . . . . . . . . . 18 (𝑧 = ⟨𝑥, 𝑦⟩ → (1st𝑧) = 𝑥)
454453eqeq1d 2767 . . . . . . . . . . . . . . . . 17 (𝑧 = ⟨𝑥, 𝑦⟩ → ((1st𝑧) = (𝑃 − (2 · 𝑢)) ↔ 𝑥 = (𝑃 − (2 · 𝑢))))
455454elrab 3519 . . . . . . . . . . . . . . . 16 (⟨𝑥, 𝑦⟩ ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} ↔ (⟨𝑥, 𝑦⟩ ∈ 𝑆𝑥 = (𝑃 − (2 · 𝑢))))
456 ancom 452 . . . . . . . . . . . . . . . 16 ((⟨𝑥, 𝑦⟩ ∈ 𝑆𝑥 = (𝑃 − (2 · 𝑢))) ↔ (𝑥 = (𝑃 − (2 · 𝑢)) ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑆))
457455, 456bitri 266 . . . . . . . . . . . . . . 15 (⟨𝑥, 𝑦⟩ ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} ↔ (𝑥 = (𝑃 − (2 · 𝑢)) ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑆))
458 opelxp 5313 . . . . . . . . . . . . . . . 16 (⟨𝑥, 𝑦⟩ ∈ ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ↔ (𝑥 ∈ {(𝑃 − (2 · 𝑢))} ∧ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
459 velsn 4350 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ {(𝑃 − (2 · 𝑢))} ↔ 𝑥 = (𝑃 − (2 · 𝑢)))
460459anbi1i 617 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ {(𝑃 − (2 · 𝑢))} ∧ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ↔ (𝑥 = (𝑃 − (2 · 𝑢)) ∧ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
461458, 460bitri 266 . . . . . . . . . . . . . . 15 (⟨𝑥, 𝑦⟩ ∈ ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ↔ (𝑥 = (𝑃 − (2 · 𝑢)) ∧ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
462450, 457, 4613bitr4g 305 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⟨𝑥, 𝑦⟩ ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} ↔ ⟨𝑥, 𝑦⟩ ∈ ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))))
463236, 237, 462eqrelrdv 5385 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} = ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
464463fveq2d 6379 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (♯‘{𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))}) = (♯‘({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))))
465 fzfid 12980 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ∈ Fin)
466 xpsnen2g 8260 . . . . . . . . . . . . . 14 (((𝑃 − (2 · 𝑢)) ∈ ℤ ∧ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ∈ Fin) → ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ≈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
467400, 465, 466syl2anc 579 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ≈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
468 hasheni 13340 . . . . . . . . . . . . 13 (({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ≈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) → (♯‘({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) = (♯‘(1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
469467, 468syl 17 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (♯‘({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) = (♯‘(1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
470 ltmul2 11128 . . . . . . . . . . . . . . . . . . . . 21 (((2 · 𝑢) ∈ ℝ ∧ 𝑃 ∈ ℝ ∧ (𝑄 ∈ ℝ ∧ 0 < 𝑄)) → ((2 · 𝑢) < 𝑃 ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · 𝑃)))
47122, 348, 250, 364, 470syl112anc 1493 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑢) < 𝑃 ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · 𝑃)))
472408, 471mpbid 223 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 · (2 · 𝑢)) < (𝑄 · 𝑃))
473 ltdivmul2 11154 . . . . . . . . . . . . . . . . . . . 20 (((𝑄 · (2 · 𝑢)) ∈ ℝ ∧ 𝑄 ∈ ℝ ∧ (𝑃 ∈ ℝ ∧ 0 < 𝑃)) → (((𝑄 · (2 · 𝑢)) / 𝑃) < 𝑄 ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · 𝑃)))
474369, 250, 348, 370, 473syl112anc 1493 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑄 · (2 · 𝑢)) / 𝑃) < 𝑄 ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · 𝑃)))
475472, 474mpbird 248 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 · (2 · 𝑢)) / 𝑃) < 𝑄)
476374, 475eqbrtrrd 4833 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 𝑃) · (2 · 𝑢)) < 𝑄)
477 fllt 12815 . . . . . . . . . . . . . . . . . 18 ((((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ ∧ 𝑄 ∈ ℤ) → (((𝑄 / 𝑃) · (2 · 𝑢)) < 𝑄 ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < 𝑄))
47823, 278, 477syl2anc 579 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑄 / 𝑃) · (2 · 𝑢)) < 𝑄 ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < 𝑄))
479476, 478mpbid 223 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < 𝑄)
480 zltlem1 11677 . . . . . . . . . . . . . . . . 17 (((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ ∧ 𝑄 ∈ ℤ) → ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < 𝑄 ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ≤ (𝑄 − 1)))
48124, 278, 480syl2anc 579 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < 𝑄 ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ≤ (𝑄 − 1)))
482479, 481mpbid 223 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ≤ (𝑄 − 1))
483482, 296breqtrrd 4837 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ≤ (2 · 𝑁))
484 eluz2 11892 . . . . . . . . . . . . . 14 ((2 · 𝑁) ∈ (ℤ‘(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ↔ ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ ∧ (2 · 𝑁) ∈ ℤ ∧ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ≤ (2 · 𝑁)))
48524, 385, 483, 484syl3anbrc 1443 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) ∈ (ℤ‘(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
486 uznn0sub 11919 . . . . . . . . . . . . 13 ((2 · 𝑁) ∈ (ℤ‘(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℕ0)
487 hashfz1 13338 . . . . . . . . . . . . 13 (((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℕ0 → (♯‘(1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) = ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
488485, 486, 4873syl 18 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (♯‘(1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) = ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
489464, 469, 4883eqtrd 2803 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (♯‘{𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))}) = ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
490489sumeq2dv 14718 . . . . . . . . . 10 (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(♯‘{𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))}) = Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
49184, 233, 4903eqtr3rd 2808 . . . . . . . . 9 (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))
492312nncnd 11292 . . . . . . . . . . 11 (𝜑 → (2 · 𝑁) ∈ ℂ)
493492adantr 472 . . . . . . . . . 10 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) ∈ ℂ)
4945, 493, 299fsumsub 14804 . . . . . . . . 9 (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) − Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
495491, 494eqtr3d 2801 . . . . . . . 8 (𝜑 → (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) = (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) − Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
496495oveq2d 6858 . . . . . . 7 (𝜑 → (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) = (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) − Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
49725zcnd 11730 . . . . . . . 8 (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℂ)
4985, 385fsumzcl 14751 . . . . . . . . 9 (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) ∈ ℤ)
499498zcnd 11730 . . . . . . . 8 (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) ∈ ℂ)
500497, 499pncan3d 10649 . . . . . . 7 (𝜑 → (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) − Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁))
501 fsumconst 14806 . . . . . . . . 9 (((((⌊‘(𝑀 / 2)) + 1)...𝑀) ∈ Fin ∧ (2 · 𝑁) ∈ ℂ) → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) = ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · (2 · 𝑁)))
5025, 492, 501syl2anc 579 . . . . . . . 8 (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) = ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · (2 · 𝑁)))
503 hashcl 13349 . . . . . . . . . . 11 ((((⌊‘(𝑀 / 2)) + 1)...𝑀) ∈ Fin → (♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∈ ℕ0)
5045, 503syl 17 . . . . . . . . . 10 (𝜑 → (♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∈ ℕ0)
505504nn0cnd 11600 . . . . . . . . 9 (𝜑 → (♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∈ ℂ)
506 2cnd 11350 . . . . . . . . 9 (𝜑 → 2 ∈ ℂ)
507505, 506, 318mul12d 10499 . . . . . . . 8 (𝜑 → ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · (2 · 𝑁)) = (2 · ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)))
508502, 507eqtrd 2799 . . . . . . 7 (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) = (2 · ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)))
509496, 500, 5083eqtrd 2803 . . . . . 6 (𝜑 → (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) = (2 · ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)))
510509oveq2d 6858 . . . . 5 (𝜑 → (-1↑(Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))) = (-1↑(2 · ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁))))
51117a1i 11 . . . . . 6 (𝜑 → 2 ∈ ℤ)
512504nn0zd 11727 . . . . . . 7 (𝜑 → (♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∈ ℤ)
513512, 377zmulcld 11735 . . . . . 6 (𝜑 → ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁) ∈ ℤ)
514 expmulz 13113 . . . . . 6 (((-1 ∈ ℂ ∧ -1 ≠ 0) ∧ (2 ∈ ℤ ∧ ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁) ∈ ℤ)) → (-1↑(2 · ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁))) = ((-1↑2)↑((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)))
5152, 4, 511, 513, 514syl22anc 867 . . . . 5 (𝜑 → (-1↑(2 · ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁))) = ((-1↑2)↑((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)))
516 neg1sqe1 13166 . . . . . . 7 (-1↑2) = 1
517516oveq1i 6852 . . . . . 6 ((-1↑2)↑((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)) = (1↑((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁))
518 1exp 13096 . . . . . . 7 (((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁) ∈ ℤ → (1↑((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)) = 1)
519513, 518syl 17 . . . . . 6 (𝜑 → (1↑((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)) = 1)
520517, 519syl5eq 2811 . . . . 5 (𝜑 → ((-1↑2)↑((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)) = 1)
521510, 515, 5203eqtrd 2803 . . . 4 (𝜑 → (-1↑(Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))) = 1)
52245, 56, 5213eqtr4d 2809 . . 3 (𝜑 → ((-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) · (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))) = (-1↑(Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))))
523 expaddz 13111 . . . 4 (((-1 ∈ ℂ ∧ -1 ≠ 0) ∧ (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ ∧ (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) ∈ ℤ)) → (-1↑(Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))) = ((-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) · (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))))
5242, 4, 25, 43, 523syl22anc 867 . . 3 (𝜑 → (-1↑(Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))) = ((-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) · (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))))
525522, 524eqtr2d 2800 . 2 (𝜑 → ((-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) · (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))) = ((-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) · (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))))
52626, 42, 42, 44, 525mulcan2ad 10917 1 (𝜑 → (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384   = wceq 1652  wcel 2155  wne 2937  wral 3055  wrex 3056  {crab 3059  cdif 3729  wss 3732  {csn 4334  cop 4340   ciun 4676  Disj wdisj 4777   class class class wbr 4809  {copab 4871   × cxp 5275  Rel wrel 5282  cfv 6068  (class class class)co 6842  1st c1st 7364  cen 8157  Fincfn 8160  cc 10187  cr 10188  0cc0 10189  1c1 10190   + caddc 10192   · cmul 10194   < clt 10328  cle 10329  cmin 10520  -cneg 10521   / cdiv 10938  cn 11274  2c2 11327  0cn0 11538  cz 11624  cuz 11886  ...cfz 12533  cfl 12799  cexp 13067  chash 13321  Σcsu 14701  cdvds 15265  cprime 15665
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-inf2 8753  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266  ax-pre-sup 10267
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-fal 1666  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-int 4634  df-iun 4678  df-disj 4778  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-se 5237  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-isom 6077  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-om 7264  df-1st 7366  df-2nd 7367  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-1o 7764  df-2o 7765  df-oadd 7768  df-er 7947  df-en 8161  df-dom 8162  df-sdom 8163  df-fin 8164  df-sup 8555  df-inf 8556  df-oi 8622  df-card 9016  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-div 10939  df-nn 11275  df-2 11335  df-3 11336  df-n0 11539  df-z 11625  df-uz 11887  df-rp 12029  df-fz 12534  df-fzo 12674  df-fl 12801  df-seq 13009  df-exp 13068  df-hash 13322  df-cj 14124  df-re 14125  df-im 14126  df-sqrt 14260  df-abs 14261  df-clim 14504  df-sum 14702  df-dvds 15266  df-prm 15666
This theorem is referenced by:  lgsquadlem2  25397
  Copyright terms: Public domain W3C validator