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

Theorem lgsquadlem1 26728
Description: Lemma for lgsquad 26731. 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 12267 . . . 4 -1 ∈ ℂ
21a1i 11 . . 3 (𝜑 → -1 ∈ ℂ)
3 neg1ne0 12269 . . . 4 -1 ≠ 0
43a1i 11 . . 3 (𝜑 → -1 ≠ 0)
5 fzfid 13878 . . . 4 (𝜑 → (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∈ Fin)
6 lgseisen.2 . . . . . . . . . 10 (𝜑𝑄 ∈ (ℙ ∖ {2}))
76gausslemma2dlem0a 26704 . . . . . . . . 9 (𝜑𝑄 ∈ ℕ)
87nnred 12168 . . . . . . . 8 (𝜑𝑄 ∈ ℝ)
9 lgseisen.1 . . . . . . . . 9 (𝜑𝑃 ∈ (ℙ ∖ {2}))
109gausslemma2dlem0a 26704 . . . . . . . 8 (𝜑𝑃 ∈ ℕ)
118, 10nndivred 12207 . . . . . . 7 (𝜑 → (𝑄 / 𝑃) ∈ ℝ)
1211adantr 481 . . . . . 6 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 / 𝑃) ∈ ℝ)
13 2z 12535 . . . . . . . 8 2 ∈ ℤ
14 elfzelz 13441 . . . . . . . . 9 (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) → 𝑢 ∈ ℤ)
1514adantl 482 . . . . . . . 8 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ∈ ℤ)
16 zmulcl 12552 . . . . . . . 8 ((2 ∈ ℤ ∧ 𝑢 ∈ ℤ) → (2 · 𝑢) ∈ ℤ)
1713, 15, 16sylancr 587 . . . . . . 7 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ∈ ℤ)
1817zred 12607 . . . . . 6 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ∈ ℝ)
1912, 18remulcld 11185 . . . . 5 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ)
2019flcld 13703 . . . 4 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ)
215, 20fsumzcl 15620 . . 3 (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ)
222, 4, 21expclzd 14056 . 2 (𝜑 → (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℂ)
23 fzfid 13878 . . . . . . 7 (𝜑 → (1...𝑀) ∈ Fin)
24 fzfid 13878 . . . . . . 7 (𝜑 → (1...𝑁) ∈ Fin)
25 xpfi 9261 . . . . . . 7 (((1...𝑀) ∈ Fin ∧ (1...𝑁) ∈ Fin) → ((1...𝑀) × (1...𝑁)) ∈ Fin)
2623, 24, 25syl2anc 584 . . . . . 6 (𝜑 → ((1...𝑀) × (1...𝑁)) ∈ Fin)
27 lgsquad.6 . . . . . . 7 𝑆 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))}
28 opabssxp 5724 . . . . . . 7 {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} ⊆ ((1...𝑀) × (1...𝑁))
2927, 28eqsstri 3978 . . . . . 6 𝑆 ⊆ ((1...𝑀) × (1...𝑁))
30 ssfi 9117 . . . . . 6 ((((1...𝑀) × (1...𝑁)) ∈ Fin ∧ 𝑆 ⊆ ((1...𝑀) × (1...𝑁))) → 𝑆 ∈ Fin)
3126, 29, 30sylancl 586 . . . . 5 (𝜑𝑆 ∈ Fin)
32 ssrab2 4037 . . . . 5 {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)} ⊆ 𝑆
33 ssfi 9117 . . . . 5 ((𝑆 ∈ Fin ∧ {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)} ⊆ 𝑆) → {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)} ∈ Fin)
3431, 32, 33sylancl 586 . . . 4 (𝜑 → {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)} ∈ Fin)
35 hashcl 14256 . . . 4 ({𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)} ∈ Fin → (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) ∈ ℕ0)
3634, 35syl 17 . . 3 (𝜑 → (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) ∈ ℕ0)
37 expcl 13985 . . 3 ((-1 ∈ ℂ ∧ (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) ∈ ℕ0) → (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) ∈ ℂ)
381, 36, 37sylancr 587 . 2 (𝜑 → (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) ∈ ℂ)
3936nn0zd 12525 . . 3 (𝜑 → (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) ∈ ℤ)
402, 4, 39expne0d 14057 . 2 (𝜑 → (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) ≠ 0)
4138, 40recidd 11926 . . . 4 (𝜑 → ((-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) · (1 / (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})))) = 1)
42 1div1e1 11845 . . . . . . . . 9 (1 / 1) = 1
4342negeqi 11394 . . . . . . . 8 -(1 / 1) = -1
44 ax-1cn 11109 . . . . . . . . 9 1 ∈ ℂ
45 ax-1ne0 11120 . . . . . . . . 9 1 ≠ 0
46 divneg2 11879 . . . . . . . . 9 ((1 ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ≠ 0) → -(1 / 1) = (1 / -1))
4744, 44, 45, 46mp3an 1461 . . . . . . . 8 -(1 / 1) = (1 / -1)
4843, 47eqtr3i 2766 . . . . . . 7 -1 = (1 / -1)
4948oveq1i 7367 . . . . . 6 (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) = ((1 / -1)↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))
502, 4, 39exprecd 14059 . . . . . 6 (𝜑 → ((1 / -1)↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) = (1 / (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))))
5149, 50eqtrid 2788 . . . . 5 (𝜑 → (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) = (1 / (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))))
5251oveq2d 7373 . . . 4 (𝜑 → ((-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) · (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))) = ((-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) · (1 / (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})))))
5331adantr 481 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑆 ∈ Fin)
54 ssrab2 4037 . . . . . . . . . . . 12 {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} ⊆ 𝑆
55 ssfi 9117 . . . . . . . . . . . 12 ((𝑆 ∈ Fin ∧ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} ⊆ 𝑆) → {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} ∈ Fin)
5653, 54, 55sylancl 586 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} ∈ Fin)
57 fveqeq2 6851 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑣 → ((1st𝑧) = (𝑃 − (2 · 𝑢)) ↔ (1st𝑣) = (𝑃 − (2 · 𝑢))))
5857elrab 3645 . . . . . . . . . . . . . . . . . . 19 (𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} ↔ (𝑣𝑆 ∧ (1st𝑣) = (𝑃 − (2 · 𝑢))))
5958simprbi 497 . . . . . . . . . . . . . . . . . 18 (𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} → (1st𝑣) = (𝑃 − (2 · 𝑢)))
6059ad2antll 727 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → (1st𝑣) = (𝑃 − (2 · 𝑢)))
6160oveq2d 7373 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → (𝑃 − (1st𝑣)) = (𝑃 − (𝑃 − (2 · 𝑢))))
6210adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℕ)
6362nncnd 12169 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℂ)
6463adantrr 715 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → 𝑃 ∈ ℂ)
6517zcnd 12608 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ∈ ℂ)
6665adantrr 715 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → (2 · 𝑢) ∈ ℂ)
6764, 66nncand 11517 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → (𝑃 − (𝑃 − (2 · 𝑢))) = (2 · 𝑢))
6861, 67eqtrd 2776 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → (𝑃 − (1st𝑣)) = (2 · 𝑢))
6968oveq1d 7372 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → ((𝑃 − (1st𝑣)) / 2) = ((2 · 𝑢) / 2))
7015zcnd 12608 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ∈ ℂ)
7170adantrr 715 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → 𝑢 ∈ ℂ)
72 2cnd 12231 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → 2 ∈ ℂ)
73 2ne0 12257 . . . . . . . . . . . . . . . 16 2 ≠ 0
7473a1i 11 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → 2 ≠ 0)
7571, 72, 74divcan3d 11936 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → ((2 · 𝑢) / 2) = 𝑢)
7669, 75eqtrd 2776 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → ((𝑃 − (1st𝑣)) / 2) = 𝑢)
7776ralrimivva 3197 . . . . . . . . . . . 12 (𝜑 → ∀𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)∀𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} ((𝑃 − (1st𝑣)) / 2) = 𝑢)
78 invdisj 5089 . . . . . . . . . . . 12 (∀𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)∀𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} ((𝑃 − (1st𝑣)) / 2) = 𝑢Disj 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})
7977, 78syl 17 . . . . . . . . . . 11 (𝜑Disj 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})
805, 56, 79hashiun 15707 . . . . . . . . . 10 (𝜑 → (♯‘ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))}) = Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(♯‘{𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))}))
81 iunrab 5012 . . . . . . . . . . . 12 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} = {𝑧𝑆 ∣ ∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1st𝑧) = (𝑃 − (2 · 𝑢))}
82 eldifsni 4750 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ≠ 2)
839, 82syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑃 ≠ 2)
8483necomd 2999 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 2 ≠ 𝑃)
8584neneqd 2948 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ¬ 2 = 𝑃)
8685ad2antrr 724 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ¬ 2 = 𝑃)
87 uzid 12778 . . . . . . . . . . . . . . . . . . . . 21 (2 ∈ ℤ → 2 ∈ (ℤ‘2))
8813, 87ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 2 ∈ (ℤ‘2)
899eldifad 3922 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑃 ∈ ℙ)
9089ad2antrr 724 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℙ)
91 dvdsprm 16579 . . . . . . . . . . . . . . . . . . . 20 ((2 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) → (2 ∥ 𝑃 ↔ 2 = 𝑃))
9288, 90, 91sylancr 587 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 ∥ 𝑃 ↔ 2 = 𝑃))
9386, 92mtbird 324 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ¬ 2 ∥ 𝑃)
9410ad2antrr 724 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℕ)
9594nncnd 12169 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℂ)
9617adantlr 713 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ∈ ℤ)
9796zcnd 12608 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ∈ ℂ)
9895, 97npcand 11516 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) + (2 · 𝑢)) = 𝑃)
9998breq2d 5117 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 ∥ ((𝑃 − (2 · 𝑢)) + (2 · 𝑢)) ↔ 2 ∥ 𝑃))
10093, 99mtbird 324 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ¬ 2 ∥ ((𝑃 − (2 · 𝑢)) + (2 · 𝑢)))
10114adantl 482 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ∈ ℤ)
102 dvdsmul1 16160 . . . . . . . . . . . . . . . . . . 19 ((2 ∈ ℤ ∧ 𝑢 ∈ ℤ) → 2 ∥ (2 · 𝑢))
10313, 101, 102sylancr 587 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 2 ∥ (2 · 𝑢))
10413a1i 11 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 2 ∈ ℤ)
10594nnzd 12526 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℤ)
106105, 96zsubcld 12612 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − (2 · 𝑢)) ∈ ℤ)
107 dvds2add 16172 . . . . . . . . . . . . . . . . . . 19 ((2 ∈ ℤ ∧ (𝑃 − (2 · 𝑢)) ∈ ℤ ∧ (2 · 𝑢) ∈ ℤ) → ((2 ∥ (𝑃 − (2 · 𝑢)) ∧ 2 ∥ (2 · 𝑢)) → 2 ∥ ((𝑃 − (2 · 𝑢)) + (2 · 𝑢))))
108104, 106, 96, 107syl3anc 1371 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 ∥ (𝑃 − (2 · 𝑢)) ∧ 2 ∥ (2 · 𝑢)) → 2 ∥ ((𝑃 − (2 · 𝑢)) + (2 · 𝑢))))
109103, 108mpan2d 692 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 ∥ (𝑃 − (2 · 𝑢)) → 2 ∥ ((𝑃 − (2 · 𝑢)) + (2 · 𝑢))))
110100, 109mtod 197 . . . . . . . . . . . . . . . 16 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ¬ 2 ∥ (𝑃 − (2 · 𝑢)))
111 breq2 5109 . . . . . . . . . . . . . . . . 17 ((1st𝑧) = (𝑃 − (2 · 𝑢)) → (2 ∥ (1st𝑧) ↔ 2 ∥ (𝑃 − (2 · 𝑢))))
112111notbid 317 . . . . . . . . . . . . . . . 16 ((1st𝑧) = (𝑃 − (2 · 𝑢)) → (¬ 2 ∥ (1st𝑧) ↔ ¬ 2 ∥ (𝑃 − (2 · 𝑢))))
113110, 112syl5ibrcom 246 . . . . . . . . . . . . . . 15 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((1st𝑧) = (𝑃 − (2 · 𝑢)) → ¬ 2 ∥ (1st𝑧)))
114113rexlimdva 3152 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑆) → (∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1st𝑧) = (𝑃 − (2 · 𝑢)) → ¬ 2 ∥ (1st𝑧)))
115 simpr 485 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧𝑆) → 𝑧𝑆)
11629, 115sselid 3942 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧𝑆) → 𝑧 ∈ ((1...𝑀) × (1...𝑁)))
117 xp1st 7953 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ ((1...𝑀) × (1...𝑁)) → (1st𝑧) ∈ (1...𝑀))
118116, 117syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑧𝑆) → (1st𝑧) ∈ (1...𝑀))
119 elfzelz 13441 . . . . . . . . . . . . . . . 16 ((1st𝑧) ∈ (1...𝑀) → (1st𝑧) ∈ ℤ)
120 odd2np1 16223 . . . . . . . . . . . . . . . 16 ((1st𝑧) ∈ ℤ → (¬ 2 ∥ (1st𝑧) ↔ ∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = (1st𝑧)))
121118, 119, 1203syl 18 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑆) → (¬ 2 ∥ (1st𝑧) ↔ ∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = (1st𝑧)))
122 lgsquad.4 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑀 = ((𝑃 − 1) / 2)
1239, 122gausslemma2dlem0b 26705 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑀 ∈ ℕ)
124123nnred 12168 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑀 ∈ ℝ)
125124ad2antrr 724 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑀 ∈ ℝ)
126125rehalfcld 12400 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑀 / 2) ∈ ℝ)
127126flcld 13703 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (⌊‘(𝑀 / 2)) ∈ ℤ)
128127peano2zd 12610 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((⌊‘(𝑀 / 2)) + 1) ∈ ℤ)
129123ad2antrr 724 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑀 ∈ ℕ)
130129nnzd 12526 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑀 ∈ ℤ)
131 simprl 769 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑛 ∈ ℤ)
132130, 131zsubcld 12612 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑀𝑛) ∈ ℤ)
133 reflcl 13701 . . . . . . . . . . . . . . . . . . . . 21 ((𝑀 / 2) ∈ ℝ → (⌊‘(𝑀 / 2)) ∈ ℝ)
134126, 133syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (⌊‘(𝑀 / 2)) ∈ ℝ)
135132zred 12607 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑀𝑛) ∈ ℝ)
136 flle 13704 . . . . . . . . . . . . . . . . . . . . 21 ((𝑀 / 2) ∈ ℝ → (⌊‘(𝑀 / 2)) ≤ (𝑀 / 2))
137126, 136syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (⌊‘(𝑀 / 2)) ≤ (𝑀 / 2))
138 zre 12503 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ ℤ → 𝑛 ∈ ℝ)
139138ad2antrl 726 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑛 ∈ ℝ)
140 simprr 771 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((2 · 𝑛) + 1) = (1st𝑧))
141118adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (1st𝑧) ∈ (1...𝑀))
142140, 141eqeltrd 2838 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((2 · 𝑛) + 1) ∈ (1...𝑀))
143 elfzle2 13445 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((2 · 𝑛) + 1) ∈ (1...𝑀) → ((2 · 𝑛) + 1) ≤ 𝑀)
144142, 143syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((2 · 𝑛) + 1) ≤ 𝑀)
145 zmulcl 12552 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((2 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (2 · 𝑛) ∈ ℤ)
14613, 131, 145sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (2 · 𝑛) ∈ ℤ)
147 zltp1le 12553 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((2 · 𝑛) ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((2 · 𝑛) < 𝑀 ↔ ((2 · 𝑛) + 1) ≤ 𝑀))
148146, 130, 147syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((2 · 𝑛) < 𝑀 ↔ ((2 · 𝑛) + 1) ≤ 𝑀))
149144, 148mpbird 256 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (2 · 𝑛) < 𝑀)
150 2re 12227 . . . . . . . . . . . . . . . . . . . . . . . . 25 2 ∈ ℝ
151150a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 2 ∈ ℝ)
152 2pos 12256 . . . . . . . . . . . . . . . . . . . . . . . . 25 0 < 2
153152a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 0 < 2)
154 ltmuldiv2 12029 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 𝑛) < 𝑀𝑛 < (𝑀 / 2)))
155139, 125, 151, 153, 154syl112anc 1374 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((2 · 𝑛) < 𝑀𝑛 < (𝑀 / 2)))
156149, 155mpbid 231 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑛 < (𝑀 / 2))
157126recnd 11183 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑀 / 2) ∈ ℂ)
158123nncnd 12169 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝑀 ∈ ℂ)
159158ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑀 ∈ ℂ)
1601592halvesd 12399 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((𝑀 / 2) + (𝑀 / 2)) = 𝑀)
161157, 157, 160mvlraddd 11565 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑀 / 2) = (𝑀 − (𝑀 / 2)))
162156, 161breqtrd 5131 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑛 < (𝑀 − (𝑀 / 2)))
163139, 125, 126, 162ltsub13d 11761 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑀 / 2) < (𝑀𝑛))
164134, 126, 135, 137, 163lelttrd 11313 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (⌊‘(𝑀 / 2)) < (𝑀𝑛))
165 zltp1le 12553 . . . . . . . . . . . . . . . . . . . 20 (((⌊‘(𝑀 / 2)) ∈ ℤ ∧ (𝑀𝑛) ∈ ℤ) → ((⌊‘(𝑀 / 2)) < (𝑀𝑛) ↔ ((⌊‘(𝑀 / 2)) + 1) ≤ (𝑀𝑛)))
166127, 132, 165syl2anc 584 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((⌊‘(𝑀 / 2)) < (𝑀𝑛) ↔ ((⌊‘(𝑀 / 2)) + 1) ≤ (𝑀𝑛)))
167164, 166mpbid 231 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((⌊‘(𝑀 / 2)) + 1) ≤ (𝑀𝑛))
168 2t0e0 12322 . . . . . . . . . . . . . . . . . . . . 21 (2 · 0) = 0
169 2cn 12228 . . . . . . . . . . . . . . . . . . . . . . . . 25 2 ∈ ℂ
170 zcn 12504 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 ∈ ℤ → 𝑛 ∈ ℂ)
171170ad2antrl 726 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑛 ∈ ℂ)
172 mulcl 11135 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((2 ∈ ℂ ∧ 𝑛 ∈ ℂ) → (2 · 𝑛) ∈ ℂ)
173169, 171, 172sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (2 · 𝑛) ∈ ℂ)
174 pncan 11407 . . . . . . . . . . . . . . . . . . . . . . . 24 (((2 · 𝑛) ∈ ℂ ∧ 1 ∈ ℂ) → (((2 · 𝑛) + 1) − 1) = (2 · 𝑛))
175173, 44, 174sylancl 586 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (((2 · 𝑛) + 1) − 1) = (2 · 𝑛))
176 elfznn 13470 . . . . . . . . . . . . . . . . . . . . . . . 24 (((2 · 𝑛) + 1) ∈ (1...𝑀) → ((2 · 𝑛) + 1) ∈ ℕ)
177 nnm1nn0 12454 . . . . . . . . . . . . . . . . . . . . . . . 24 (((2 · 𝑛) + 1) ∈ ℕ → (((2 · 𝑛) + 1) − 1) ∈ ℕ0)
178142, 176, 1773syl 18 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (((2 · 𝑛) + 1) − 1) ∈ ℕ0)
179175, 178eqeltrrd 2839 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (2 · 𝑛) ∈ ℕ0)
180179nn0ge0d 12476 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 0 ≤ (2 · 𝑛))
181168, 180eqbrtrid 5140 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (2 · 0) ≤ (2 · 𝑛))
182 0red 11158 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 0 ∈ ℝ)
183 lemul2 12008 . . . . . . . . . . . . . . . . . . . . 21 ((0 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (0 ≤ 𝑛 ↔ (2 · 0) ≤ (2 · 𝑛)))
184182, 139, 151, 153, 183syl112anc 1374 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (0 ≤ 𝑛 ↔ (2 · 0) ≤ (2 · 𝑛)))
185181, 184mpbird 256 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 0 ≤ 𝑛)
186125, 139subge02d 11747 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (0 ≤ 𝑛 ↔ (𝑀𝑛) ≤ 𝑀))
187185, 186mpbid 231 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑀𝑛) ≤ 𝑀)
188128, 130, 132, 167, 187elfzd 13432 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑀𝑛) ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀))
18989ad2antrr 724 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑃 ∈ ℙ)
190 prmnn 16550 . . . . . . . . . . . . . . . . . . . . 21 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
191189, 190syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑃 ∈ ℕ)
192191nncnd 12169 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑃 ∈ ℂ)
193 peano2cn 11327 . . . . . . . . . . . . . . . . . . . 20 ((2 · 𝑛) ∈ ℂ → ((2 · 𝑛) + 1) ∈ ℂ)
194173, 193syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((2 · 𝑛) + 1) ∈ ℂ)
195192, 194nncand 11517 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑃 − (𝑃 − ((2 · 𝑛) + 1))) = ((2 · 𝑛) + 1))
196 1cnd 11150 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 1 ∈ ℂ)
197192, 173, 196sub32d 11544 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((𝑃 − (2 · 𝑛)) − 1) = ((𝑃 − 1) − (2 · 𝑛)))
198192, 173, 196subsub4d 11543 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((𝑃 − (2 · 𝑛)) − 1) = (𝑃 − ((2 · 𝑛) + 1)))
199 2cnd 12231 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 2 ∈ ℂ)
200199, 159, 171subdid 11611 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (2 · (𝑀𝑛)) = ((2 · 𝑀) − (2 · 𝑛)))
201122oveq2i 7368 . . . . . . . . . . . . . . . . . . . . . . 23 (2 · 𝑀) = (2 · ((𝑃 − 1) / 2))
20210nnzd 12526 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝑃 ∈ ℤ)
203202ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑃 ∈ ℤ)
204 peano2zm 12546 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑃 ∈ ℤ → (𝑃 − 1) ∈ ℤ)
205203, 204syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑃 − 1) ∈ ℤ)
206205zcnd 12608 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑃 − 1) ∈ ℂ)
20773a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 2 ≠ 0)
208206, 199, 207divcan2d 11933 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (2 · ((𝑃 − 1) / 2)) = (𝑃 − 1))
209201, 208eqtrid 2788 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (2 · 𝑀) = (𝑃 − 1))
210209oveq1d 7372 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((2 · 𝑀) − (2 · 𝑛)) = ((𝑃 − 1) − (2 · 𝑛)))
211200, 210eqtr2d 2777 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((𝑃 − 1) − (2 · 𝑛)) = (2 · (𝑀𝑛)))
212197, 198, 2113eqtr3d 2784 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑃 − ((2 · 𝑛) + 1)) = (2 · (𝑀𝑛)))
213212oveq2d 7373 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑃 − (𝑃 − ((2 · 𝑛) + 1))) = (𝑃 − (2 · (𝑀𝑛))))
214195, 213, 1403eqtr3rd 2785 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (1st𝑧) = (𝑃 − (2 · (𝑀𝑛))))
215 oveq2 7365 . . . . . . . . . . . . . . . . . . 19 (𝑢 = (𝑀𝑛) → (2 · 𝑢) = (2 · (𝑀𝑛)))
216215oveq2d 7373 . . . . . . . . . . . . . . . . . 18 (𝑢 = (𝑀𝑛) → (𝑃 − (2 · 𝑢)) = (𝑃 − (2 · (𝑀𝑛))))
217216rspceeqv 3595 . . . . . . . . . . . . . . . . 17 (((𝑀𝑛) ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ (1st𝑧) = (𝑃 − (2 · (𝑀𝑛)))) → ∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1st𝑧) = (𝑃 − (2 · 𝑢)))
218188, 214, 217syl2anc 584 . . . . . . . . . . . . . . . 16 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1st𝑧) = (𝑃 − (2 · 𝑢)))
219218rexlimdvaa 3153 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑆) → (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = (1st𝑧) → ∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1st𝑧) = (𝑃 − (2 · 𝑢))))
220121, 219sylbid 239 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑆) → (¬ 2 ∥ (1st𝑧) → ∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1st𝑧) = (𝑃 − (2 · 𝑢))))
221114, 220impbid 211 . . . . . . . . . . . . 13 ((𝜑𝑧𝑆) → (∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1st𝑧) = (𝑃 − (2 · 𝑢)) ↔ ¬ 2 ∥ (1st𝑧)))
222221rabbidva 3414 . . . . . . . . . . . 12 (𝜑 → {𝑧𝑆 ∣ ∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1st𝑧) = (𝑃 − (2 · 𝑢))} = {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})
22381, 222eqtrid 2788 . . . . . . . . . . 11 (𝜑 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} = {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})
224223fveq2d 6846 . . . . . . . . . 10 (𝜑 → (♯‘ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))}) = (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))
22527relopabiv 5776 . . . . . . . . . . . . . . 15 Rel 𝑆
226 relss 5737 . . . . . . . . . . . . . . 15 ({𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} ⊆ 𝑆 → (Rel 𝑆 → Rel {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))}))
22754, 225, 226mp2 9 . . . . . . . . . . . . . 14 Rel {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))}
228 relxp 5651 . . . . . . . . . . . . . 14 Rel ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
22927eleq2i 2829 . . . . . . . . . . . . . . . . . 18 (⟨𝑥, 𝑦⟩ ∈ 𝑆 ↔ ⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))})
230 opabidw 5481 . . . . . . . . . . . . . . . . . 18 (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} ↔ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))
231229, 230bitri 274 . . . . . . . . . . . . . . . . 17 (⟨𝑥, 𝑦⟩ ∈ 𝑆 ↔ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))
232 anass 469 . . . . . . . . . . . . . . . . . . 19 (((𝑦 ∈ ℕ ∧ 𝑦𝑁) ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄)) ↔ (𝑦 ∈ ℕ ∧ (𝑦𝑁 ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄))))
23320peano2zd 12610 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ∈ ℤ)
234233zred 12607 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ∈ ℝ)
235234adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ∈ ℝ)
2368ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈ ℝ)
237 nnre 12160 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
238237adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ ℝ)
239 lesub 11634 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ∈ ℝ ∧ 𝑄 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ≤ (𝑄𝑦) ↔ 𝑦 ≤ (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1))))
240235, 236, 238, 239syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ≤ (𝑄𝑦) ↔ 𝑦 ≤ (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1))))
2418adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑄 ∈ ℝ)
242241recnd 11183 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑄 ∈ ℂ)
24363, 242mulcomd 11176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 · 𝑄) = (𝑄 · 𝑃))
24465, 242mulcomd 11176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑢) · 𝑄) = (𝑄 · (2 · 𝑢)))
24562nnne0d 12203 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ≠ 0)
246242, 63, 245divcan1d 11932 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 𝑃) · 𝑃) = 𝑄)
247246oveq1d 7372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑄 / 𝑃) · 𝑃) · (2 · 𝑢)) = (𝑄 · (2 · 𝑢)))
24812recnd 11183 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 / 𝑃) ∈ ℂ)
249248, 63, 65mul32d 11365 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑄 / 𝑃) · 𝑃) · (2 · 𝑢)) = (((𝑄 / 𝑃) · (2 · 𝑢)) · 𝑃))
250244, 247, 2493eqtr2d 2782 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑢) · 𝑄) = (((𝑄 / 𝑃) · (2 · 𝑢)) · 𝑃))
251243, 250oveq12d 7375 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 · 𝑄) − ((2 · 𝑢) · 𝑄)) = ((𝑄 · 𝑃) − (((𝑄 / 𝑃) · (2 · 𝑢)) · 𝑃)))
25263, 65, 242subdird 11612 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) · 𝑄) = ((𝑃 · 𝑄) − ((2 · 𝑢) · 𝑄)))
25319recnd 11183 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℂ)
254242, 253, 63subdird 11612 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃) = ((𝑄 · 𝑃) − (((𝑄 / 𝑃) · (2 · 𝑢)) · 𝑃)))
255251, 252, 2543eqtr4d 2786 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) · 𝑄) = ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃))
256255adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑃 − (2 · 𝑢)) · 𝑄) = ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃))
257256breq2d 5117 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄) ↔ (𝑦 · 𝑃) < ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃)))
25819adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ)
259236, 258resubcld 11583 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℝ)
26062adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℕ)
261260nnred 12168 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℝ)
262260nngt0d 12202 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 0 < 𝑃)
263 ltmul1 12005 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦 ∈ ℝ ∧ (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℝ ∧ (𝑃 ∈ ℝ ∧ 0 < 𝑃)) → (𝑦 < (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ↔ (𝑦 · 𝑃) < ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃)))
264238, 259, 261, 262, 263syl112anc 1374 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑦 < (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ↔ (𝑦 · 𝑃) < ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃)))
265 ltsub13 11636 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦 ∈ ℝ ∧ 𝑄 ∈ ℝ ∧ ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ) → (𝑦 < (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ↔ ((𝑄 / 𝑃) · (2 · 𝑢)) < (𝑄𝑦)))
266238, 236, 258, 265syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑦 < (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ↔ ((𝑄 / 𝑃) · (2 · 𝑢)) < (𝑄𝑦)))
267257, 264, 2663bitr2d 306 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄) ↔ ((𝑄 / 𝑃) · (2 · 𝑢)) < (𝑄𝑦)))
2687adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑄 ∈ ℕ)
269268nnzd 12526 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑄 ∈ ℤ)
270 nnz 12520 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 ∈ ℕ → 𝑦 ∈ ℤ)
271 zsubcl 12545 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑄 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑄𝑦) ∈ ℤ)
272269, 270, 271syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑄𝑦) ∈ ℤ)
273 fllt 13711 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ ∧ (𝑄𝑦) ∈ ℤ) → (((𝑄 / 𝑃) · (2 · 𝑢)) < (𝑄𝑦) ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < (𝑄𝑦)))
274258, 272, 273syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (((𝑄 / 𝑃) · (2 · 𝑢)) < (𝑄𝑦) ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < (𝑄𝑦)))
27520adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ)
276 zltp1le 12553 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ ∧ (𝑄𝑦) ∈ ℤ) → ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < (𝑄𝑦) ↔ ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ≤ (𝑄𝑦)))
277275, 272, 276syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < (𝑄𝑦) ↔ ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ≤ (𝑄𝑦)))
278267, 274, 2773bitrd 304 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄) ↔ ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ≤ (𝑄𝑦)))
279 lgsquad.5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 𝑁 = ((𝑄 − 1) / 2)
280279oveq2i 7368 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (2 · 𝑁) = (2 · ((𝑄 − 1) / 2))
281 peano2rem 11468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑄 ∈ ℝ → (𝑄 − 1) ∈ ℝ)
282241, 281syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 − 1) ∈ ℝ)
283282recnd 11183 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 − 1) ∈ ℂ)
284 2cnd 12231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 2 ∈ ℂ)
28573a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 2 ≠ 0)
286283, 284, 285divcan2d 11933 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · ((𝑄 − 1) / 2)) = (𝑄 − 1))
287280, 286eqtrid 2788 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) = (𝑄 − 1))
288287oveq1d 7372 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = ((𝑄 − 1) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
289 1cnd 11150 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 1 ∈ ℂ)
29020zcnd 12608 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℂ)
291242, 289, 290sub32d 11544 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 − 1) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = ((𝑄 − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) − 1))
292242, 290, 289subsub4d 11543 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) − 1) = (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1)))
293288, 291, 2923eqtrd 2780 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1)))
294293adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1)))
295294breq2d 5117 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ↔ 𝑦 ≤ (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1))))
296240, 278, 2953bitr4d 310 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄) ↔ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
297296anbi2d 629 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦𝑁 ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄)) ↔ (𝑦𝑁𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
298 2nn 12226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 2 ∈ ℕ
2996, 279gausslemma2dlem0b 26705 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝑁 ∈ ℕ)
300 nnmulcl 12177 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((2 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (2 · 𝑁) ∈ ℕ)
301298, 299, 300sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (2 · 𝑁) ∈ ℕ)
302301adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) ∈ ℕ)
303302nnred 12168 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) ∈ ℝ)
304299adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ∈ ℕ)
305304nnred 12168 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ∈ ℝ)
30620zred 12607 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℝ)
307299nncnd 12169 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝑁 ∈ ℂ)
308307adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ∈ ℂ)
3093082timesd 12396 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) = (𝑁 + 𝑁))
310308, 308, 309mvrladdd 11568 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − 𝑁) = 𝑁)
311241rehalfcld 12400 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 / 2) ∈ ℝ)
312241ltm1d 12087 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 − 1) < 𝑄)
313150a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 2 ∈ ℝ)
314152a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 0 < 2)
315 ltdiv1 12019 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑄 − 1) ∈ ℝ ∧ 𝑄 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((𝑄 − 1) < 𝑄 ↔ ((𝑄 − 1) / 2) < (𝑄 / 2)))
316282, 241, 313, 314, 315syl112anc 1374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 − 1) < 𝑄 ↔ ((𝑄 − 1) / 2) < (𝑄 / 2)))
317312, 316mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 − 1) / 2) < (𝑄 / 2))
318279, 317eqbrtrid 5140 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 < (𝑄 / 2))
319305, 311, 318ltled 11303 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ≤ (𝑄 / 2))
320242, 284, 63, 285div32d 11954 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 2) · 𝑃) = (𝑄 · (𝑃 / 2)))
321124adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑀 ∈ ℝ)
322321rehalfcld 12400 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑀 / 2) ∈ ℝ)
323 peano2re 11328 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((⌊‘(𝑀 / 2)) ∈ ℝ → ((⌊‘(𝑀 / 2)) + 1) ∈ ℝ)
324322, 133, 3233syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((⌊‘(𝑀 / 2)) + 1) ∈ ℝ)
32515zred 12607 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ∈ ℝ)
326 flltp1 13705 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑀 / 2) ∈ ℝ → (𝑀 / 2) < ((⌊‘(𝑀 / 2)) + 1))
327322, 326syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑀 / 2) < ((⌊‘(𝑀 / 2)) + 1))
328 elfzle1 13444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) → ((⌊‘(𝑀 / 2)) + 1) ≤ 𝑢)
329328adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((⌊‘(𝑀 / 2)) + 1) ≤ 𝑢)
330322, 324, 325, 327, 329ltletrd 11315 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑀 / 2) < 𝑢)
331 ltdivmul 12030 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑀 ∈ ℝ ∧ 𝑢 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((𝑀 / 2) < 𝑢𝑀 < (2 · 𝑢)))
332321, 325, 313, 314, 331syl112anc 1374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑀 / 2) < 𝑢𝑀 < (2 · 𝑢)))
333330, 332mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑀 < (2 · 𝑢))
334122, 333eqbrtrrid 5141 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − 1) / 2) < (2 · 𝑢))
33562nnred 12168 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℝ)
336 peano2rem 11468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑃 ∈ ℝ → (𝑃 − 1) ∈ ℝ)
337335, 336syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − 1) ∈ ℝ)
338 ltdivmul 12030 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((𝑃 − 1) ∈ ℝ ∧ (2 · 𝑢) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (((𝑃 − 1) / 2) < (2 · 𝑢) ↔ (𝑃 − 1) < (2 · (2 · 𝑢))))
339337, 18, 313, 314, 338syl112anc 1374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑃 − 1) / 2) < (2 · 𝑢) ↔ (𝑃 − 1) < (2 · (2 · 𝑢))))
340334, 339mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − 1) < (2 · (2 · 𝑢)))
341202adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℤ)
342 zmulcl 12552 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((2 ∈ ℤ ∧ (2 · 𝑢) ∈ ℤ) → (2 · (2 · 𝑢)) ∈ ℤ)
34313, 17, 342sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · (2 · 𝑢)) ∈ ℤ)
344 zlem1lt 12555 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑃 ∈ ℤ ∧ (2 · (2 · 𝑢)) ∈ ℤ) → (𝑃 ≤ (2 · (2 · 𝑢)) ↔ (𝑃 − 1) < (2 · (2 · 𝑢))))
345341, 343, 344syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 ≤ (2 · (2 · 𝑢)) ↔ (𝑃 − 1) < (2 · (2 · 𝑢))))
346340, 345mpbird 256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ≤ (2 · (2 · 𝑢)))
347 ledivmul 12031 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑃 ∈ ℝ ∧ (2 · 𝑢) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((𝑃 / 2) ≤ (2 · 𝑢) ↔ 𝑃 ≤ (2 · (2 · 𝑢))))
348335, 18, 313, 314, 347syl112anc 1374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 / 2) ≤ (2 · 𝑢) ↔ 𝑃 ≤ (2 · (2 · 𝑢))))
349346, 348mpbird 256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 / 2) ≤ (2 · 𝑢))
350335rehalfcld 12400 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 / 2) ∈ ℝ)
351268nngt0d 12202 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 0 < 𝑄)
352 lemul2 12008 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑃 / 2) ∈ ℝ ∧ (2 · 𝑢) ∈ ℝ ∧ (𝑄 ∈ ℝ ∧ 0 < 𝑄)) → ((𝑃 / 2) ≤ (2 · 𝑢) ↔ (𝑄 · (𝑃 / 2)) ≤ (𝑄 · (2 · 𝑢))))
353350, 18, 241, 351, 352syl112anc 1374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 / 2) ≤ (2 · 𝑢) ↔ (𝑄 · (𝑃 / 2)) ≤ (𝑄 · (2 · 𝑢))))
354349, 353mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 · (𝑃 / 2)) ≤ (𝑄 · (2 · 𝑢)))
355320, 354eqbrtrd 5127 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 2) · 𝑃) ≤ (𝑄 · (2 · 𝑢)))
356241, 18remulcld 11185 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 · (2 · 𝑢)) ∈ ℝ)
35762nngt0d 12202 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 0 < 𝑃)
358 lemuldiv 12035 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑄 / 2) ∈ ℝ ∧ (𝑄 · (2 · 𝑢)) ∈ ℝ ∧ (𝑃 ∈ ℝ ∧ 0 < 𝑃)) → (((𝑄 / 2) · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ↔ (𝑄 / 2) ≤ ((𝑄 · (2 · 𝑢)) / 𝑃)))
359311, 356, 335, 357, 358syl112anc 1374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑄 / 2) · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ↔ (𝑄 / 2) ≤ ((𝑄 · (2 · 𝑢)) / 𝑃)))
360355, 359mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 / 2) ≤ ((𝑄 · (2 · 𝑢)) / 𝑃))
361242, 65, 63, 245div23d 11968 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 · (2 · 𝑢)) / 𝑃) = ((𝑄 / 𝑃) · (2 · 𝑢)))
362360, 361breqtrd 5131 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 / 2) ≤ ((𝑄 / 𝑃) · (2 · 𝑢)))
363305, 311, 19, 319, 362letrd 11312 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)))
364299nnzd 12526 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑𝑁 ∈ ℤ)
365364adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ∈ ℤ)
366 flge 13710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ ∧ 𝑁 ∈ ℤ) → (𝑁 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)) ↔ 𝑁 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
36719, 365, 366syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑁 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)) ↔ 𝑁 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
368363, 367mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))
369310, 368eqbrtrd 5127 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − 𝑁) ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))
370303, 305, 306, 369subled 11758 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ≤ 𝑁)
371370adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ≤ 𝑁)
372302nnzd 12526 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) ∈ ℤ)
373372, 20zsubcld 12612 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℤ)
374373adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℤ)
375374zred 12607 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℝ)
376299ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑁 ∈ ℕ)
377376nnred 12168 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑁 ∈ ℝ)
378 letr 11249 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑦 ∈ ℝ ∧ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∧ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ≤ 𝑁) → 𝑦𝑁))
379238, 375, 377, 378syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∧ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ≤ 𝑁) → 𝑦𝑁))
380371, 379mpan2d 692 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) → 𝑦𝑁))
381380pm4.71rd 563 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ↔ (𝑦𝑁𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
382297, 381bitr4d 281 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦𝑁 ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄)) ↔ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
383382pm5.32da 579 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑦 ∈ ℕ ∧ (𝑦𝑁 ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
384383adantr 481 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → ((𝑦 ∈ ℕ ∧ (𝑦𝑁 ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
385232, 384bitrid 282 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (((𝑦 ∈ ℕ ∧ 𝑦𝑁) ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄)) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
386 simpr 485 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → 𝑥 = (𝑃 − (2 · 𝑢)))
387341, 17zsubcld 12612 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − (2 · 𝑢)) ∈ ℤ)
388 elfzle2 13445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) → 𝑢𝑀)
389388adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢𝑀)
390389, 122breqtrdi 5146 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ≤ ((𝑃 − 1) / 2))
391 lemuldiv2 12036 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑢 ∈ ℝ ∧ (𝑃 − 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 𝑢) ≤ (𝑃 − 1) ↔ 𝑢 ≤ ((𝑃 − 1) / 2)))
392325, 337, 313, 314, 391syl112anc 1374 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑢) ≤ (𝑃 − 1) ↔ 𝑢 ≤ ((𝑃 − 1) / 2)))
393390, 392mpbird 256 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ≤ (𝑃 − 1))
394335ltm1d 12087 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − 1) < 𝑃)
39518, 337, 335, 393, 394lelttrd 11313 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) < 𝑃)
39618, 335posdifd 11742 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑢) < 𝑃 ↔ 0 < (𝑃 − (2 · 𝑢))))
397395, 396mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 0 < (𝑃 − (2 · 𝑢)))
398 elnnz 12509 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑃 − (2 · 𝑢)) ∈ ℕ ↔ ((𝑃 − (2 · 𝑢)) ∈ ℤ ∧ 0 < (𝑃 − (2 · 𝑢))))
399387, 397, 398sylanbrc 583 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − (2 · 𝑢)) ∈ ℕ)
40063, 65, 289sub32d 11544 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) − 1) = ((𝑃 − 1) − (2 · 𝑢)))
401122, 122oveq12i 7369 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑀 + 𝑀) = (((𝑃 − 1) / 2) + ((𝑃 − 1) / 2))
40262nnzd 12526 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℤ)
403402, 204syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − 1) ∈ ℤ)
404403zcnd 12608 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − 1) ∈ ℂ)
4054042halvesd 12399 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑃 − 1) / 2) + ((𝑃 − 1) / 2)) = (𝑃 − 1))
406401, 405eqtrid 2788 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑀 + 𝑀) = (𝑃 − 1))
407406oveq1d 7372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑀 + 𝑀) − 𝑀) = ((𝑃 − 1) − 𝑀))
408158adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑀 ∈ ℂ)
409408, 408pncan2d 11514 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑀 + 𝑀) − 𝑀) = 𝑀)
410407, 409eqtr3d 2778 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − 1) − 𝑀) = 𝑀)
411410, 333eqbrtrd 5127 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − 1) − 𝑀) < (2 · 𝑢))
412337, 321, 18, 411ltsub23d 11760 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − 1) − (2 · 𝑢)) < 𝑀)
413400, 412eqbrtrd 5127 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) − 1) < 𝑀)
414123adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑀 ∈ ℕ)
415414nnzd 12526 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑀 ∈ ℤ)
416 zlem1lt 12555 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑃 − (2 · 𝑢)) ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑃 − (2 · 𝑢)) ≤ 𝑀 ↔ ((𝑃 − (2 · 𝑢)) − 1) < 𝑀))
417387, 415, 416syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) ≤ 𝑀 ↔ ((𝑃 − (2 · 𝑢)) − 1) < 𝑀))
418413, 417mpbird 256 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − (2 · 𝑢)) ≤ 𝑀)
419 fznn 13509 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑀 ∈ ℤ → ((𝑃 − (2 · 𝑢)) ∈ (1...𝑀) ↔ ((𝑃 − (2 · 𝑢)) ∈ ℕ ∧ (𝑃 − (2 · 𝑢)) ≤ 𝑀)))
420415, 419syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) ∈ (1...𝑀) ↔ ((𝑃 − (2 · 𝑢)) ∈ ℕ ∧ (𝑃 − (2 · 𝑢)) ≤ 𝑀)))
421399, 418, 420mpbir2and 711 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − (2 · 𝑢)) ∈ (1...𝑀))
422421adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (𝑃 − (2 · 𝑢)) ∈ (1...𝑀))
423386, 422eqeltrd 2838 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → 𝑥 ∈ (1...𝑀))
424423biantrurd 533 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (𝑦 ∈ (1...𝑁) ↔ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))))
425364ad2antrr 724 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → 𝑁 ∈ ℤ)
426 fznn 13509 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ ℤ → (𝑦 ∈ (1...𝑁) ↔ (𝑦 ∈ ℕ ∧ 𝑦𝑁)))
427425, 426syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (𝑦 ∈ (1...𝑁) ↔ (𝑦 ∈ ℕ ∧ 𝑦𝑁)))
428424, 427bitr3d 280 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ↔ (𝑦 ∈ ℕ ∧ 𝑦𝑁)))
429386oveq1d 7372 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (𝑥 · 𝑄) = ((𝑃 − (2 · 𝑢)) · 𝑄))
430429breq2d 5117 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → ((𝑦 · 𝑃) < (𝑥 · 𝑄) ↔ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄)))
431428, 430anbi12d 631 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)) ↔ ((𝑦 ∈ ℕ ∧ 𝑦𝑁) ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄))))
432373adantr 481 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℤ)
433 fznn 13509 . . . . . . . . . . . . . . . . . . 19 (((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℤ → (𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
434432, 433syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
435385, 431, 4343bitr4d 310 . . . . . . . . . . . . . . . . 17 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)) ↔ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
436231, 435bitrid 282 . . . . . . . . . . . . . . . 16 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (⟨𝑥, 𝑦⟩ ∈ 𝑆𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
437436pm5.32da 579 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑥 = (𝑃 − (2 · 𝑢)) ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑆) ↔ (𝑥 = (𝑃 − (2 · 𝑢)) ∧ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))))
438 vex 3449 . . . . . . . . . . . . . . . . . . 19 𝑥 ∈ V
439 vex 3449 . . . . . . . . . . . . . . . . . . 19 𝑦 ∈ V
440438, 439op1std 7931 . . . . . . . . . . . . . . . . . 18 (𝑧 = ⟨𝑥, 𝑦⟩ → (1st𝑧) = 𝑥)
441440eqeq1d 2738 . . . . . . . . . . . . . . . . 17 (𝑧 = ⟨𝑥, 𝑦⟩ → ((1st𝑧) = (𝑃 − (2 · 𝑢)) ↔ 𝑥 = (𝑃 − (2 · 𝑢))))
442441elrab 3645 . . . . . . . . . . . . . . . 16 (⟨𝑥, 𝑦⟩ ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} ↔ (⟨𝑥, 𝑦⟩ ∈ 𝑆𝑥 = (𝑃 − (2 · 𝑢))))
443442biancomi 463 . . . . . . . . . . . . . . 15 (⟨𝑥, 𝑦⟩ ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} ↔ (𝑥 = (𝑃 − (2 · 𝑢)) ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑆))
444 opelxp 5669 . . . . . . . . . . . . . . . 16 (⟨𝑥, 𝑦⟩ ∈ ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ↔ (𝑥 ∈ {(𝑃 − (2 · 𝑢))} ∧ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
445 velsn 4602 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ {(𝑃 − (2 · 𝑢))} ↔ 𝑥 = (𝑃 − (2 · 𝑢)))
446445anbi1i 624 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ {(𝑃 − (2 · 𝑢))} ∧ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ↔ (𝑥 = (𝑃 − (2 · 𝑢)) ∧ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
447444, 446bitri 274 . . . . . . . . . . . . . . 15 (⟨𝑥, 𝑦⟩ ∈ ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ↔ (𝑥 = (𝑃 − (2 · 𝑢)) ∧ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
448437, 443, 4473bitr4g 313 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⟨𝑥, 𝑦⟩ ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} ↔ ⟨𝑥, 𝑦⟩ ∈ ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))))
449227, 228, 448eqrelrdv 5748 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} = ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
450449fveq2d 6846 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (♯‘{𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))}) = (♯‘({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))))
451 fzfid 13878 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ∈ Fin)
452 xpsnen2g 9009 . . . . . . . . . . . . . 14 (((𝑃 − (2 · 𝑢)) ∈ ℤ ∧ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ∈ Fin) → ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ≈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
453387, 451, 452syl2anc 584 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ≈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
454 hasheni 14248 . . . . . . . . . . . . 13 (({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ≈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) → (♯‘({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) = (♯‘(1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
455453, 454syl 17 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (♯‘({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) = (♯‘(1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
456 ltmul2 12006 . . . . . . . . . . . . . . . . . . . . 21 (((2 · 𝑢) ∈ ℝ ∧ 𝑃 ∈ ℝ ∧ (𝑄 ∈ ℝ ∧ 0 < 𝑄)) → ((2 · 𝑢) < 𝑃 ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · 𝑃)))
45718, 335, 241, 351, 456syl112anc 1374 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑢) < 𝑃 ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · 𝑃)))
458395, 457mpbid 231 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 · (2 · 𝑢)) < (𝑄 · 𝑃))
459 ltdivmul2 12032 . . . . . . . . . . . . . . . . . . . 20 (((𝑄 · (2 · 𝑢)) ∈ ℝ ∧ 𝑄 ∈ ℝ ∧ (𝑃 ∈ ℝ ∧ 0 < 𝑃)) → (((𝑄 · (2 · 𝑢)) / 𝑃) < 𝑄 ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · 𝑃)))
460356, 241, 335, 357, 459syl112anc 1374 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑄 · (2 · 𝑢)) / 𝑃) < 𝑄 ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · 𝑃)))
461458, 460mpbird 256 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 · (2 · 𝑢)) / 𝑃) < 𝑄)
462361, 461eqbrtrrd 5129 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 𝑃) · (2 · 𝑢)) < 𝑄)
463 fllt 13711 . . . . . . . . . . . . . . . . . 18 ((((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ ∧ 𝑄 ∈ ℤ) → (((𝑄 / 𝑃) · (2 · 𝑢)) < 𝑄 ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < 𝑄))
46419, 269, 463syl2anc 584 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑄 / 𝑃) · (2 · 𝑢)) < 𝑄 ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < 𝑄))
465462, 464mpbid 231 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < 𝑄)
466 zltlem1 12556 . . . . . . . . . . . . . . . . 17 (((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ ∧ 𝑄 ∈ ℤ) → ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < 𝑄 ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ≤ (𝑄 − 1)))
46720, 269, 466syl2anc 584 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < 𝑄 ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ≤ (𝑄 − 1)))
468465, 467mpbid 231 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ≤ (𝑄 − 1))
469468, 287breqtrrd 5133 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ≤ (2 · 𝑁))
470 eluz2 12769 . . . . . . . . . . . . . 14 ((2 · 𝑁) ∈ (ℤ‘(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ↔ ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ ∧ (2 · 𝑁) ∈ ℤ ∧ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ≤ (2 · 𝑁)))
47120, 372, 469, 470syl3anbrc 1343 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) ∈ (ℤ‘(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
472 uznn0sub 12802 . . . . . . . . . . . . 13 ((2 · 𝑁) ∈ (ℤ‘(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℕ0)
473 hashfz1 14246 . . . . . . . . . . . . 13 (((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℕ0 → (♯‘(1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) = ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
474471, 472, 4733syl 18 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (♯‘(1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) = ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
475450, 455, 4743eqtrd 2780 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (♯‘{𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))}) = ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
476475sumeq2dv 15588 . . . . . . . . . 10 (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(♯‘{𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))}) = Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
47780, 224, 4763eqtr3rd 2785 . . . . . . . . 9 (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))
478301nncnd 12169 . . . . . . . . . . 11 (𝜑 → (2 · 𝑁) ∈ ℂ)
479478adantr 481 . . . . . . . . . 10 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) ∈ ℂ)
4805, 479, 290fsumsub 15673 . . . . . . . . 9 (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) − Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
481477, 480eqtr3d 2778 . . . . . . . 8 (𝜑 → (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) = (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) − Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
482481oveq2d 7373 . . . . . . 7 (𝜑 → (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) = (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) − Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
48321zcnd 12608 . . . . . . . 8 (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℂ)
4845, 372fsumzcl 15620 . . . . . . . . 9 (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) ∈ ℤ)
485484zcnd 12608 . . . . . . . 8 (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) ∈ ℂ)
486483, 485pncan3d 11515 . . . . . . 7 (𝜑 → (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) − Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁))
487 fsumconst 15675 . . . . . . . . 9 (((((⌊‘(𝑀 / 2)) + 1)...𝑀) ∈ Fin ∧ (2 · 𝑁) ∈ ℂ) → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) = ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · (2 · 𝑁)))
4885, 478, 487syl2anc 584 . . . . . . . 8 (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) = ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · (2 · 𝑁)))
489 hashcl 14256 . . . . . . . . . . 11 ((((⌊‘(𝑀 / 2)) + 1)...𝑀) ∈ Fin → (♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∈ ℕ0)
4905, 489syl 17 . . . . . . . . . 10 (𝜑 → (♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∈ ℕ0)
491490nn0cnd 12475 . . . . . . . . 9 (𝜑 → (♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∈ ℂ)
492 2cnd 12231 . . . . . . . . 9 (𝜑 → 2 ∈ ℂ)
493491, 492, 307mul12d 11364 . . . . . . . 8 (𝜑 → ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · (2 · 𝑁)) = (2 · ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)))
494488, 493eqtrd 2776 . . . . . . 7 (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) = (2 · ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)))
495482, 486, 4943eqtrd 2780 . . . . . 6 (𝜑 → (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) = (2 · ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)))
496495oveq2d 7373 . . . . 5 (𝜑 → (-1↑(Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))) = (-1↑(2 · ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁))))
49713a1i 11 . . . . . 6 (𝜑 → 2 ∈ ℤ)
498490nn0zd 12525 . . . . . . 7 (𝜑 → (♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∈ ℤ)
499498, 364zmulcld 12613 . . . . . 6 (𝜑 → ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁) ∈ ℤ)
500 expmulz 14014 . . . . . 6 (((-1 ∈ ℂ ∧ -1 ≠ 0) ∧ (2 ∈ ℤ ∧ ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁) ∈ ℤ)) → (-1↑(2 · ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁))) = ((-1↑2)↑((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)))
5012, 4, 497, 499, 500syl22anc 837 . . . . 5 (𝜑 → (-1↑(2 · ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁))) = ((-1↑2)↑((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)))
502 neg1sqe1 14100 . . . . . . 7 (-1↑2) = 1
503502oveq1i 7367 . . . . . 6 ((-1↑2)↑((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)) = (1↑((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁))
504 1exp 13997 . . . . . . 7 (((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁) ∈ ℤ → (1↑((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)) = 1)
505499, 504syl 17 . . . . . 6 (𝜑 → (1↑((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)) = 1)
506503, 505eqtrid 2788 . . . . 5 (𝜑 → ((-1↑2)↑((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)) = 1)
507496, 501, 5063eqtrd 2780 . . . 4 (𝜑 → (-1↑(Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))) = 1)
50841, 52, 5073eqtr4d 2786 . . 3 (𝜑 → ((-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) · (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))) = (-1↑(Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))))
509 expaddz 14012 . . . 4 (((-1 ∈ ℂ ∧ -1 ≠ 0) ∧ (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ ∧ (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) ∈ ℤ)) → (-1↑(Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))) = ((-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) · (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))))
5102, 4, 21, 39, 509syl22anc 837 . . 3 (𝜑 → (-1↑(Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))) = ((-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) · (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))))
511508, 510eqtr2d 2777 . 2 (𝜑 → ((-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) · (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))) = ((-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) · (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))))
51222, 38, 38, 40, 511mulcan2ad 11791 1 (𝜑 → (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396   = wceq 1541  wcel 2106  wne 2943  wral 3064  wrex 3073  {crab 3407  cdif 3907  wss 3910  {csn 4586  cop 4592   ciun 4954  Disj wdisj 5070   class class class wbr 5105  {copab 5167   × cxp 5631  Rel wrel 5638  cfv 6496  (class class class)co 7357  1st c1st 7919  cen 8880  Fincfn 8883  cc 11049  cr 11050  0cc0 11051  1c1 11052   + caddc 11054   · cmul 11056   < clt 11189  cle 11190  cmin 11385  -cneg 11386   / cdiv 11812  cn 12153  2c2 12208  0cn0 12413  cz 12499  cuz 12763  ...cfz 13424  cfl 13695  cexp 13967  chash 14230  Σcsu 15570  cdvds 16136  cprime 16547
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-inf2 9577  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-disj 5071  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-2o 8413  df-er 8648  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-sup 9378  df-inf 9379  df-oi 9446  df-card 9875  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-4 12218  df-n0 12414  df-z 12500  df-uz 12764  df-rp 12916  df-fz 13425  df-fzo 13568  df-fl 13697  df-seq 13907  df-exp 13968  df-hash 14231  df-cj 14984  df-re 14985  df-im 14986  df-sqrt 15120  df-abs 15121  df-clim 15370  df-sum 15571  df-dvds 16137  df-prm 16548
This theorem is referenced by:  lgsquadlem2  26729
  Copyright terms: Public domain W3C validator