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

Theorem lgsquadlem1 26528
Description: Lemma for lgsquad 26531. 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 12087 . . . 4 -1 ∈ ℂ
21a1i 11 . . 3 (𝜑 → -1 ∈ ℂ)
3 neg1ne0 12089 . . . 4 -1 ≠ 0
43a1i 11 . . 3 (𝜑 → -1 ≠ 0)
5 fzfid 13693 . . . 4 (𝜑 → (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∈ Fin)
6 lgseisen.2 . . . . . . . . . 10 (𝜑𝑄 ∈ (ℙ ∖ {2}))
76gausslemma2dlem0a 26504 . . . . . . . . 9 (𝜑𝑄 ∈ ℕ)
87nnred 11988 . . . . . . . 8 (𝜑𝑄 ∈ ℝ)
9 lgseisen.1 . . . . . . . . 9 (𝜑𝑃 ∈ (ℙ ∖ {2}))
109gausslemma2dlem0a 26504 . . . . . . . 8 (𝜑𝑃 ∈ ℕ)
118, 10nndivred 12027 . . . . . . 7 (𝜑 → (𝑄 / 𝑃) ∈ ℝ)
1211adantr 481 . . . . . 6 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 / 𝑃) ∈ ℝ)
13 2z 12352 . . . . . . . 8 2 ∈ ℤ
14 elfzelz 13256 . . . . . . . . 9 (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) → 𝑢 ∈ ℤ)
1514adantl 482 . . . . . . . 8 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ∈ ℤ)
16 zmulcl 12369 . . . . . . . 8 ((2 ∈ ℤ ∧ 𝑢 ∈ ℤ) → (2 · 𝑢) ∈ ℤ)
1713, 15, 16sylancr 587 . . . . . . 7 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ∈ ℤ)
1817zred 12426 . . . . . 6 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ∈ ℝ)
1912, 18remulcld 11005 . . . . 5 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ)
2019flcld 13518 . . . 4 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ)
215, 20fsumzcl 15447 . . 3 (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ)
222, 4, 21expclzd 13869 . 2 (𝜑 → (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℂ)
23 fzfid 13693 . . . . . . 7 (𝜑 → (1...𝑀) ∈ Fin)
24 fzfid 13693 . . . . . . 7 (𝜑 → (1...𝑁) ∈ Fin)
25 xpfi 9085 . . . . . . 7 (((1...𝑀) ∈ Fin ∧ (1...𝑁) ∈ Fin) → ((1...𝑀) × (1...𝑁)) ∈ Fin)
2623, 24, 25syl2anc 584 . . . . . 6 (𝜑 → ((1...𝑀) × (1...𝑁)) ∈ Fin)
27 lgsquad.6 . . . . . . 7 𝑆 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))}
28 opabssxp 5679 . . . . . . 7 {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} ⊆ ((1...𝑀) × (1...𝑁))
2927, 28eqsstri 3955 . . . . . 6 𝑆 ⊆ ((1...𝑀) × (1...𝑁))
30 ssfi 8956 . . . . . 6 ((((1...𝑀) × (1...𝑁)) ∈ Fin ∧ 𝑆 ⊆ ((1...𝑀) × (1...𝑁))) → 𝑆 ∈ Fin)
3126, 29, 30sylancl 586 . . . . 5 (𝜑𝑆 ∈ Fin)
32 ssrab2 4013 . . . . 5 {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)} ⊆ 𝑆
33 ssfi 8956 . . . . 5 ((𝑆 ∈ Fin ∧ {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)} ⊆ 𝑆) → {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)} ∈ Fin)
3431, 32, 33sylancl 586 . . . 4 (𝜑 → {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)} ∈ Fin)
35 hashcl 14071 . . . 4 ({𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)} ∈ Fin → (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) ∈ ℕ0)
3634, 35syl 17 . . 3 (𝜑 → (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) ∈ ℕ0)
37 expcl 13800 . . 3 ((-1 ∈ ℂ ∧ (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) ∈ ℕ0) → (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) ∈ ℂ)
381, 36, 37sylancr 587 . 2 (𝜑 → (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) ∈ ℂ)
3936nn0zd 12424 . . 3 (𝜑 → (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) ∈ ℤ)
402, 4, 39expne0d 13870 . 2 (𝜑 → (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) ≠ 0)
4138, 40recidd 11746 . . . 4 (𝜑 → ((-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) · (1 / (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})))) = 1)
42 1div1e1 11665 . . . . . . . . 9 (1 / 1) = 1
4342negeqi 11214 . . . . . . . 8 -(1 / 1) = -1
44 ax-1cn 10929 . . . . . . . . 9 1 ∈ ℂ
45 ax-1ne0 10940 . . . . . . . . 9 1 ≠ 0
46 divneg2 11699 . . . . . . . . 9 ((1 ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ≠ 0) → -(1 / 1) = (1 / -1))
4744, 44, 45, 46mp3an 1460 . . . . . . . 8 -(1 / 1) = (1 / -1)
4843, 47eqtr3i 2768 . . . . . . 7 -1 = (1 / -1)
4948oveq1i 7285 . . . . . 6 (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) = ((1 / -1)↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))
502, 4, 39exprecd 13872 . . . . . 6 (𝜑 → ((1 / -1)↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) = (1 / (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))))
5149, 50eqtrid 2790 . . . . 5 (𝜑 → (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) = (1 / (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))))
5251oveq2d 7291 . . . 4 (𝜑 → ((-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) · (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))) = ((-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) · (1 / (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})))))
5331adantr 481 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑆 ∈ Fin)
54 ssrab2 4013 . . . . . . . . . . . 12 {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} ⊆ 𝑆
55 ssfi 8956 . . . . . . . . . . . 12 ((𝑆 ∈ Fin ∧ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} ⊆ 𝑆) → {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} ∈ Fin)
5653, 54, 55sylancl 586 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} ∈ Fin)
57 fveqeq2 6783 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑣 → ((1st𝑧) = (𝑃 − (2 · 𝑢)) ↔ (1st𝑣) = (𝑃 − (2 · 𝑢))))
5857elrab 3624 . . . . . . . . . . . . . . . . . . 19 (𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} ↔ (𝑣𝑆 ∧ (1st𝑣) = (𝑃 − (2 · 𝑢))))
5958simprbi 497 . . . . . . . . . . . . . . . . . 18 (𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} → (1st𝑣) = (𝑃 − (2 · 𝑢)))
6059ad2antll 726 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → (1st𝑣) = (𝑃 − (2 · 𝑢)))
6160oveq2d 7291 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → (𝑃 − (1st𝑣)) = (𝑃 − (𝑃 − (2 · 𝑢))))
6210adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℕ)
6362nncnd 11989 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℂ)
6463adantrr 714 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → 𝑃 ∈ ℂ)
6517zcnd 12427 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ∈ ℂ)
6665adantrr 714 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → (2 · 𝑢) ∈ ℂ)
6764, 66nncand 11337 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → (𝑃 − (𝑃 − (2 · 𝑢))) = (2 · 𝑢))
6861, 67eqtrd 2778 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → (𝑃 − (1st𝑣)) = (2 · 𝑢))
6968oveq1d 7290 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → ((𝑃 − (1st𝑣)) / 2) = ((2 · 𝑢) / 2))
7015zcnd 12427 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ∈ ℂ)
7170adantrr 714 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → 𝑢 ∈ ℂ)
72 2cnd 12051 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → 2 ∈ ℂ)
73 2ne0 12077 . . . . . . . . . . . . . . . 16 2 ≠ 0
7473a1i 11 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → 2 ≠ 0)
7571, 72, 74divcan3d 11756 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → ((2 · 𝑢) / 2) = 𝑢)
7669, 75eqtrd 2778 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})) → ((𝑃 − (1st𝑣)) / 2) = 𝑢)
7776ralrimivva 3123 . . . . . . . . . . . 12 (𝜑 → ∀𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)∀𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} ((𝑃 − (1st𝑣)) / 2) = 𝑢)
78 invdisj 5058 . . . . . . . . . . . 12 (∀𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)∀𝑣 ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} ((𝑃 − (1st𝑣)) / 2) = 𝑢Disj 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})
7977, 78syl 17 . . . . . . . . . . 11 (𝜑Disj 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))})
805, 56, 79hashiun 15534 . . . . . . . . . 10 (𝜑 → (♯‘ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))}) = Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(♯‘{𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))}))
81 iunrab 4982 . . . . . . . . . . . 12 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} = {𝑧𝑆 ∣ ∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1st𝑧) = (𝑃 − (2 · 𝑢))}
82 eldifsni 4723 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ≠ 2)
839, 82syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑃 ≠ 2)
8483necomd 2999 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 2 ≠ 𝑃)
8584neneqd 2948 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ¬ 2 = 𝑃)
8685ad2antrr 723 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ¬ 2 = 𝑃)
87 uzid 12597 . . . . . . . . . . . . . . . . . . . . 21 (2 ∈ ℤ → 2 ∈ (ℤ‘2))
8813, 87ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 2 ∈ (ℤ‘2)
899eldifad 3899 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑃 ∈ ℙ)
9089ad2antrr 723 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℙ)
91 dvdsprm 16408 . . . . . . . . . . . . . . . . . . . 20 ((2 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) → (2 ∥ 𝑃 ↔ 2 = 𝑃))
9288, 90, 91sylancr 587 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 ∥ 𝑃 ↔ 2 = 𝑃))
9386, 92mtbird 325 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ¬ 2 ∥ 𝑃)
9410ad2antrr 723 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℕ)
9594nncnd 11989 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℂ)
9617adantlr 712 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ∈ ℤ)
9796zcnd 12427 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ∈ ℂ)
9895, 97npcand 11336 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) + (2 · 𝑢)) = 𝑃)
9998breq2d 5086 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 ∥ ((𝑃 − (2 · 𝑢)) + (2 · 𝑢)) ↔ 2 ∥ 𝑃))
10093, 99mtbird 325 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ¬ 2 ∥ ((𝑃 − (2 · 𝑢)) + (2 · 𝑢)))
10114adantl 482 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ∈ ℤ)
102 dvdsmul1 15987 . . . . . . . . . . . . . . . . . . 19 ((2 ∈ ℤ ∧ 𝑢 ∈ ℤ) → 2 ∥ (2 · 𝑢))
10313, 101, 102sylancr 587 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 2 ∥ (2 · 𝑢))
10413a1i 11 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 2 ∈ ℤ)
10594nnzd 12425 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℤ)
106105, 96zsubcld 12431 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − (2 · 𝑢)) ∈ ℤ)
107 dvds2add 15999 . . . . . . . . . . . . . . . . . . 19 ((2 ∈ ℤ ∧ (𝑃 − (2 · 𝑢)) ∈ ℤ ∧ (2 · 𝑢) ∈ ℤ) → ((2 ∥ (𝑃 − (2 · 𝑢)) ∧ 2 ∥ (2 · 𝑢)) → 2 ∥ ((𝑃 − (2 · 𝑢)) + (2 · 𝑢))))
108104, 106, 96, 107syl3anc 1370 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 ∥ (𝑃 − (2 · 𝑢)) ∧ 2 ∥ (2 · 𝑢)) → 2 ∥ ((𝑃 − (2 · 𝑢)) + (2 · 𝑢))))
109103, 108mpan2d 691 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 ∥ (𝑃 − (2 · 𝑢)) → 2 ∥ ((𝑃 − (2 · 𝑢)) + (2 · 𝑢))))
110100, 109mtod 197 . . . . . . . . . . . . . . . 16 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ¬ 2 ∥ (𝑃 − (2 · 𝑢)))
111 breq2 5078 . . . . . . . . . . . . . . . . 17 ((1st𝑧) = (𝑃 − (2 · 𝑢)) → (2 ∥ (1st𝑧) ↔ 2 ∥ (𝑃 − (2 · 𝑢))))
112111notbid 318 . . . . . . . . . . . . . . . 16 ((1st𝑧) = (𝑃 − (2 · 𝑢)) → (¬ 2 ∥ (1st𝑧) ↔ ¬ 2 ∥ (𝑃 − (2 · 𝑢))))
113110, 112syl5ibrcom 246 . . . . . . . . . . . . . . 15 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((1st𝑧) = (𝑃 − (2 · 𝑢)) → ¬ 2 ∥ (1st𝑧)))
114113rexlimdva 3213 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑆) → (∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1st𝑧) = (𝑃 − (2 · 𝑢)) → ¬ 2 ∥ (1st𝑧)))
115 simpr 485 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧𝑆) → 𝑧𝑆)
11629, 115sselid 3919 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧𝑆) → 𝑧 ∈ ((1...𝑀) × (1...𝑁)))
117 xp1st 7863 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ ((1...𝑀) × (1...𝑁)) → (1st𝑧) ∈ (1...𝑀))
118116, 117syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑧𝑆) → (1st𝑧) ∈ (1...𝑀))
119 elfzelz 13256 . . . . . . . . . . . . . . . 16 ((1st𝑧) ∈ (1...𝑀) → (1st𝑧) ∈ ℤ)
120 odd2np1 16050 . . . . . . . . . . . . . . . 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 26505 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑀 ∈ ℕ)
124123nnred 11988 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑀 ∈ ℝ)
125124ad2antrr 723 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑀 ∈ ℝ)
126125rehalfcld 12220 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑀 / 2) ∈ ℝ)
127126flcld 13518 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (⌊‘(𝑀 / 2)) ∈ ℤ)
128127peano2zd 12429 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((⌊‘(𝑀 / 2)) + 1) ∈ ℤ)
129123ad2antrr 723 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑀 ∈ ℕ)
130129nnzd 12425 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑀 ∈ ℤ)
131 simprl 768 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑛 ∈ ℤ)
132130, 131zsubcld 12431 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑀𝑛) ∈ ℤ)
133 reflcl 13516 . . . . . . . . . . . . . . . . . . . . 21 ((𝑀 / 2) ∈ ℝ → (⌊‘(𝑀 / 2)) ∈ ℝ)
134126, 133syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (⌊‘(𝑀 / 2)) ∈ ℝ)
135132zred 12426 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑀𝑛) ∈ ℝ)
136 flle 13519 . . . . . . . . . . . . . . . . . . . . 21 ((𝑀 / 2) ∈ ℝ → (⌊‘(𝑀 / 2)) ≤ (𝑀 / 2))
137126, 136syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (⌊‘(𝑀 / 2)) ≤ (𝑀 / 2))
138 zre 12323 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ ℤ → 𝑛 ∈ ℝ)
139138ad2antrl 725 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑛 ∈ ℝ)
140 simprr 770 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((2 · 𝑛) + 1) = (1st𝑧))
141118adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (1st𝑧) ∈ (1...𝑀))
142140, 141eqeltrd 2839 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((2 · 𝑛) + 1) ∈ (1...𝑀))
143 elfzle2 13260 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((2 · 𝑛) + 1) ∈ (1...𝑀) → ((2 · 𝑛) + 1) ≤ 𝑀)
144142, 143syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((2 · 𝑛) + 1) ≤ 𝑀)
145 zmulcl 12369 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((2 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (2 · 𝑛) ∈ ℤ)
14613, 131, 145sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (2 · 𝑛) ∈ ℤ)
147 zltp1le 12370 . . . . . . . . . . . . . . . . . . . . . . . . 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 12047 . . . . . . . . . . . . . . . . . . . . . . . . 25 2 ∈ ℝ
151150a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 2 ∈ ℝ)
152 2pos 12076 . . . . . . . . . . . . . . . . . . . . . . . . 25 0 < 2
153152a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 0 < 2)
154 ltmuldiv2 11849 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 𝑛) < 𝑀𝑛 < (𝑀 / 2)))
155139, 125, 151, 153, 154syl112anc 1373 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((2 · 𝑛) < 𝑀𝑛 < (𝑀 / 2)))
156149, 155mpbid 231 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑛 < (𝑀 / 2))
157126recnd 11003 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑀 / 2) ∈ ℂ)
158123nncnd 11989 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝑀 ∈ ℂ)
159158ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑀 ∈ ℂ)
1601592halvesd 12219 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((𝑀 / 2) + (𝑀 / 2)) = 𝑀)
161157, 157, 160mvlraddd 11385 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑀 / 2) = (𝑀 − (𝑀 / 2)))
162156, 161breqtrd 5100 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑛 < (𝑀 − (𝑀 / 2)))
163139, 125, 126, 162ltsub13d 11581 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑀 / 2) < (𝑀𝑛))
164134, 126, 135, 137, 163lelttrd 11133 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (⌊‘(𝑀 / 2)) < (𝑀𝑛))
165 zltp1le 12370 . . . . . . . . . . . . . . . . . . . 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 12142 . . . . . . . . . . . . . . . . . . . . 21 (2 · 0) = 0
169 2cn 12048 . . . . . . . . . . . . . . . . . . . . . . . . 25 2 ∈ ℂ
170 zcn 12324 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 ∈ ℤ → 𝑛 ∈ ℂ)
171170ad2antrl 725 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑛 ∈ ℂ)
172 mulcl 10955 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((2 ∈ ℂ ∧ 𝑛 ∈ ℂ) → (2 · 𝑛) ∈ ℂ)
173169, 171, 172sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (2 · 𝑛) ∈ ℂ)
174 pncan 11227 . . . . . . . . . . . . . . . . . . . . . . . 24 (((2 · 𝑛) ∈ ℂ ∧ 1 ∈ ℂ) → (((2 · 𝑛) + 1) − 1) = (2 · 𝑛))
175173, 44, 174sylancl 586 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (((2 · 𝑛) + 1) − 1) = (2 · 𝑛))
176 elfznn 13285 . . . . . . . . . . . . . . . . . . . . . . . 24 (((2 · 𝑛) + 1) ∈ (1...𝑀) → ((2 · 𝑛) + 1) ∈ ℕ)
177 nnm1nn0 12274 . . . . . . . . . . . . . . . . . . . . . . . 24 (((2 · 𝑛) + 1) ∈ ℕ → (((2 · 𝑛) + 1) − 1) ∈ ℕ0)
178142, 176, 1773syl 18 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (((2 · 𝑛) + 1) − 1) ∈ ℕ0)
179175, 178eqeltrrd 2840 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (2 · 𝑛) ∈ ℕ0)
180179nn0ge0d 12296 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 0 ≤ (2 · 𝑛))
181168, 180eqbrtrid 5109 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (2 · 0) ≤ (2 · 𝑛))
182 0red 10978 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 0 ∈ ℝ)
183 lemul2 11828 . . . . . . . . . . . . . . . . . . . . 21 ((0 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (0 ≤ 𝑛 ↔ (2 · 0) ≤ (2 · 𝑛)))
184182, 139, 151, 153, 183syl112anc 1373 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (0 ≤ 𝑛 ↔ (2 · 0) ≤ (2 · 𝑛)))
185181, 184mpbird 256 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 0 ≤ 𝑛)
186125, 139subge02d 11567 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (0 ≤ 𝑛 ↔ (𝑀𝑛) ≤ 𝑀))
187185, 186mpbid 231 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑀𝑛) ≤ 𝑀)
188128, 130, 132, 167, 187elfzd 13247 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑀𝑛) ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀))
18989ad2antrr 723 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑃 ∈ ℙ)
190 prmnn 16379 . . . . . . . . . . . . . . . . . . . . 21 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
191189, 190syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑃 ∈ ℕ)
192191nncnd 11989 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑃 ∈ ℂ)
193 peano2cn 11147 . . . . . . . . . . . . . . . . . . . 20 ((2 · 𝑛) ∈ ℂ → ((2 · 𝑛) + 1) ∈ ℂ)
194173, 193syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((2 · 𝑛) + 1) ∈ ℂ)
195192, 194nncand 11337 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑃 − (𝑃 − ((2 · 𝑛) + 1))) = ((2 · 𝑛) + 1))
196 1cnd 10970 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 1 ∈ ℂ)
197192, 173, 196sub32d 11364 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((𝑃 − (2 · 𝑛)) − 1) = ((𝑃 − 1) − (2 · 𝑛)))
198192, 173, 196subsub4d 11363 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((𝑃 − (2 · 𝑛)) − 1) = (𝑃 − ((2 · 𝑛) + 1)))
199 2cnd 12051 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 2 ∈ ℂ)
200199, 159, 171subdid 11431 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (2 · (𝑀𝑛)) = ((2 · 𝑀) − (2 · 𝑛)))
201122oveq2i 7286 . . . . . . . . . . . . . . . . . . . . . . 23 (2 · 𝑀) = (2 · ((𝑃 − 1) / 2))
20210nnzd 12425 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝑃 ∈ ℤ)
203202ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 𝑃 ∈ ℤ)
204 peano2zm 12363 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑃 ∈ ℤ → (𝑃 − 1) ∈ ℤ)
205203, 204syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑃 − 1) ∈ ℤ)
206205zcnd 12427 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑃 − 1) ∈ ℂ)
20773a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → 2 ≠ 0)
208206, 199, 207divcan2d 11753 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (2 · ((𝑃 − 1) / 2)) = (𝑃 − 1))
209201, 208eqtrid 2790 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (2 · 𝑀) = (𝑃 − 1))
210209oveq1d 7290 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((2 · 𝑀) − (2 · 𝑛)) = ((𝑃 − 1) − (2 · 𝑛)))
211200, 210eqtr2d 2779 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ((𝑃 − 1) − (2 · 𝑛)) = (2 · (𝑀𝑛)))
212197, 198, 2113eqtr3d 2786 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑃 − ((2 · 𝑛) + 1)) = (2 · (𝑀𝑛)))
213212oveq2d 7291 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (𝑃 − (𝑃 − ((2 · 𝑛) + 1))) = (𝑃 − (2 · (𝑀𝑛))))
214195, 213, 1403eqtr3rd 2787 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → (1st𝑧) = (𝑃 − (2 · (𝑀𝑛))))
215 oveq2 7283 . . . . . . . . . . . . . . . . . . 19 (𝑢 = (𝑀𝑛) → (2 · 𝑢) = (2 · (𝑀𝑛)))
216215oveq2d 7291 . . . . . . . . . . . . . . . . . 18 (𝑢 = (𝑀𝑛) → (𝑃 − (2 · 𝑢)) = (𝑃 − (2 · (𝑀𝑛))))
217216rspceeqv 3575 . . . . . . . . . . . . . . . . 17 (((𝑀𝑛) ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ (1st𝑧) = (𝑃 − (2 · (𝑀𝑛)))) → ∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1st𝑧) = (𝑃 − (2 · 𝑢)))
218188, 214, 217syl2anc 584 . . . . . . . . . . . . . . . 16 (((𝜑𝑧𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1st𝑧))) → ∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1st𝑧) = (𝑃 − (2 · 𝑢)))
219218rexlimdvaa 3214 . . . . . . . . . . . . . . 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 3413 . . . . . . . . . . . 12 (𝜑 → {𝑧𝑆 ∣ ∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1st𝑧) = (𝑃 − (2 · 𝑢))} = {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})
22381, 222eqtrid 2790 . . . . . . . . . . 11 (𝜑 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} = {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})
224223fveq2d 6778 . . . . . . . . . 10 (𝜑 → (♯‘ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))}) = (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))
22527relopabiv 5730 . . . . . . . . . . . . . . 15 Rel 𝑆
226 relss 5692 . . . . . . . . . . . . . . 15 ({𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} ⊆ 𝑆 → (Rel 𝑆 → Rel {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))}))
22754, 225, 226mp2 9 . . . . . . . . . . . . . 14 Rel {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))}
228 relxp 5607 . . . . . . . . . . . . . 14 Rel ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
22927eleq2i 2830 . . . . . . . . . . . . . . . . . 18 (⟨𝑥, 𝑦⟩ ∈ 𝑆 ↔ ⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))})
230 opabidw 5437 . . . . . . . . . . . . . . . . . 18 (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} ↔ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))
231229, 230bitri 274 . . . . . . . . . . . . . . . . 17 (⟨𝑥, 𝑦⟩ ∈ 𝑆 ↔ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))
232 anass 469 . . . . . . . . . . . . . . . . . . 19 (((𝑦 ∈ ℕ ∧ 𝑦𝑁) ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄)) ↔ (𝑦 ∈ ℕ ∧ (𝑦𝑁 ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄))))
23320peano2zd 12429 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ∈ ℤ)
234233zred 12426 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ∈ ℝ)
235234adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ∈ ℝ)
2368ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈ ℝ)
237 nnre 11980 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
238237adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ ℝ)
239 lesub 11454 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ∈ ℝ ∧ 𝑄 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ≤ (𝑄𝑦) ↔ 𝑦 ≤ (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1))))
240235, 236, 238, 239syl3anc 1370 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ≤ (𝑄𝑦) ↔ 𝑦 ≤ (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1))))
2418adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑄 ∈ ℝ)
242241recnd 11003 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑄 ∈ ℂ)
24363, 242mulcomd 10996 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 · 𝑄) = (𝑄 · 𝑃))
24465, 242mulcomd 10996 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑢) · 𝑄) = (𝑄 · (2 · 𝑢)))
24562nnne0d 12023 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ≠ 0)
246242, 63, 245divcan1d 11752 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 𝑃) · 𝑃) = 𝑄)
247246oveq1d 7290 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑄 / 𝑃) · 𝑃) · (2 · 𝑢)) = (𝑄 · (2 · 𝑢)))
24812recnd 11003 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 / 𝑃) ∈ ℂ)
249248, 63, 65mul32d 11185 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑄 / 𝑃) · 𝑃) · (2 · 𝑢)) = (((𝑄 / 𝑃) · (2 · 𝑢)) · 𝑃))
250244, 247, 2493eqtr2d 2784 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑢) · 𝑄) = (((𝑄 / 𝑃) · (2 · 𝑢)) · 𝑃))
251243, 250oveq12d 7293 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 · 𝑄) − ((2 · 𝑢) · 𝑄)) = ((𝑄 · 𝑃) − (((𝑄 / 𝑃) · (2 · 𝑢)) · 𝑃)))
25263, 65, 242subdird 11432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) · 𝑄) = ((𝑃 · 𝑄) − ((2 · 𝑢) · 𝑄)))
25319recnd 11003 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℂ)
254242, 253, 63subdird 11432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃) = ((𝑄 · 𝑃) − (((𝑄 / 𝑃) · (2 · 𝑢)) · 𝑃)))
255251, 252, 2543eqtr4d 2788 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) · 𝑄) = ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃))
256255adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑃 − (2 · 𝑢)) · 𝑄) = ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃))
257256breq2d 5086 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄) ↔ (𝑦 · 𝑃) < ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃)))
25819adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ)
259236, 258resubcld 11403 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℝ)
26062adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℕ)
261260nnred 11988 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℝ)
262260nngt0d 12022 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 0 < 𝑃)
263 ltmul1 11825 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦 ∈ ℝ ∧ (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℝ ∧ (𝑃 ∈ ℝ ∧ 0 < 𝑃)) → (𝑦 < (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ↔ (𝑦 · 𝑃) < ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃)))
264238, 259, 261, 262, 263syl112anc 1373 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑦 < (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ↔ (𝑦 · 𝑃) < ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃)))
265 ltsub13 11456 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦 ∈ ℝ ∧ 𝑄 ∈ ℝ ∧ ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ) → (𝑦 < (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ↔ ((𝑄 / 𝑃) · (2 · 𝑢)) < (𝑄𝑦)))
266238, 236, 258, 265syl3anc 1370 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑦 < (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ↔ ((𝑄 / 𝑃) · (2 · 𝑢)) < (𝑄𝑦)))
267257, 264, 2663bitr2d 307 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄) ↔ ((𝑄 / 𝑃) · (2 · 𝑢)) < (𝑄𝑦)))
2687adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑄 ∈ ℕ)
269268nnzd 12425 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑄 ∈ ℤ)
270 nnz 12342 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 ∈ ℕ → 𝑦 ∈ ℤ)
271 zsubcl 12362 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑄 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑄𝑦) ∈ ℤ)
272269, 270, 271syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑄𝑦) ∈ ℤ)
273 fllt 13526 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ ∧ (𝑄𝑦) ∈ ℤ) → (((𝑄 / 𝑃) · (2 · 𝑢)) < (𝑄𝑦) ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < (𝑄𝑦)))
274258, 272, 273syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (((𝑄 / 𝑃) · (2 · 𝑢)) < (𝑄𝑦) ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < (𝑄𝑦)))
27520adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ)
276 zltp1le 12370 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ ∧ (𝑄𝑦) ∈ ℤ) → ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < (𝑄𝑦) ↔ ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ≤ (𝑄𝑦)))
277275, 272, 276syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < (𝑄𝑦) ↔ ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ≤ (𝑄𝑦)))
278267, 274, 2773bitrd 305 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄) ↔ ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ≤ (𝑄𝑦)))
279 lgsquad.5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 𝑁 = ((𝑄 − 1) / 2)
280279oveq2i 7286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (2 · 𝑁) = (2 · ((𝑄 − 1) / 2))
281 peano2rem 11288 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑄 ∈ ℝ → (𝑄 − 1) ∈ ℝ)
282241, 281syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 − 1) ∈ ℝ)
283282recnd 11003 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 − 1) ∈ ℂ)
284 2cnd 12051 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 2 ∈ ℂ)
28573a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 2 ≠ 0)
286283, 284, 285divcan2d 11753 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · ((𝑄 − 1) / 2)) = (𝑄 − 1))
287280, 286eqtrid 2790 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) = (𝑄 − 1))
288287oveq1d 7290 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = ((𝑄 − 1) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
289 1cnd 10970 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 1 ∈ ℂ)
29020zcnd 12427 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℂ)
291242, 289, 290sub32d 11364 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 − 1) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = ((𝑄 − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) − 1))
292242, 290, 289subsub4d 11363 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) − 1) = (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1)))
293288, 291, 2923eqtrd 2782 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1)))
294293adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1)))
295294breq2d 5086 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ↔ 𝑦 ≤ (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1))))
296240, 278, 2953bitr4d 311 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄) ↔ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
297296anbi2d 629 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦𝑁 ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄)) ↔ (𝑦𝑁𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
298 2nn 12046 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 2 ∈ ℕ
2996, 279gausslemma2dlem0b 26505 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝑁 ∈ ℕ)
300 nnmulcl 11997 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((2 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (2 · 𝑁) ∈ ℕ)
301298, 299, 300sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (2 · 𝑁) ∈ ℕ)
302301adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) ∈ ℕ)
303302nnred 11988 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) ∈ ℝ)
304299adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ∈ ℕ)
305304nnred 11988 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ∈ ℝ)
30620zred 12426 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℝ)
307299nncnd 11989 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝑁 ∈ ℂ)
308307adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ∈ ℂ)
3093082timesd 12216 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) = (𝑁 + 𝑁))
310308, 308, 309mvrladdd 11388 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − 𝑁) = 𝑁)
311241rehalfcld 12220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 / 2) ∈ ℝ)
312241ltm1d 11907 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 − 1) < 𝑄)
313150a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 2 ∈ ℝ)
314152a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 0 < 2)
315 ltdiv1 11839 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑄 − 1) ∈ ℝ ∧ 𝑄 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((𝑄 − 1) < 𝑄 ↔ ((𝑄 − 1) / 2) < (𝑄 / 2)))
316282, 241, 313, 314, 315syl112anc 1373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 − 1) < 𝑄 ↔ ((𝑄 − 1) / 2) < (𝑄 / 2)))
317312, 316mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 − 1) / 2) < (𝑄 / 2))
318279, 317eqbrtrid 5109 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 < (𝑄 / 2))
319305, 311, 318ltled 11123 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ≤ (𝑄 / 2))
320242, 284, 63, 285div32d 11774 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 2) · 𝑃) = (𝑄 · (𝑃 / 2)))
321124adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑀 ∈ ℝ)
322321rehalfcld 12220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑀 / 2) ∈ ℝ)
323 peano2re 11148 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((⌊‘(𝑀 / 2)) ∈ ℝ → ((⌊‘(𝑀 / 2)) + 1) ∈ ℝ)
324322, 133, 3233syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((⌊‘(𝑀 / 2)) + 1) ∈ ℝ)
32515zred 12426 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ∈ ℝ)
326 flltp1 13520 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑀 / 2) ∈ ℝ → (𝑀 / 2) < ((⌊‘(𝑀 / 2)) + 1))
327322, 326syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑀 / 2) < ((⌊‘(𝑀 / 2)) + 1))
328 elfzle1 13259 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) → ((⌊‘(𝑀 / 2)) + 1) ≤ 𝑢)
329328adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((⌊‘(𝑀 / 2)) + 1) ≤ 𝑢)
330322, 324, 325, 327, 329ltletrd 11135 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑀 / 2) < 𝑢)
331 ltdivmul 11850 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑀 ∈ ℝ ∧ 𝑢 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((𝑀 / 2) < 𝑢𝑀 < (2 · 𝑢)))
332321, 325, 313, 314, 331syl112anc 1373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑀 / 2) < 𝑢𝑀 < (2 · 𝑢)))
333330, 332mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑀 < (2 · 𝑢))
334122, 333eqbrtrrid 5110 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − 1) / 2) < (2 · 𝑢))
33562nnred 11988 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℝ)
336 peano2rem 11288 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑃 ∈ ℝ → (𝑃 − 1) ∈ ℝ)
337335, 336syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − 1) ∈ ℝ)
338 ltdivmul 11850 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((𝑃 − 1) ∈ ℝ ∧ (2 · 𝑢) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (((𝑃 − 1) / 2) < (2 · 𝑢) ↔ (𝑃 − 1) < (2 · (2 · 𝑢))))
339337, 18, 313, 314, 338syl112anc 1373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 12369 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((2 ∈ ℤ ∧ (2 · 𝑢) ∈ ℤ) → (2 · (2 · 𝑢)) ∈ ℤ)
34313, 17, 342sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · (2 · 𝑢)) ∈ ℤ)
344 zlem1lt 12372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11851 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑃 ∈ ℝ ∧ (2 · 𝑢) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((𝑃 / 2) ≤ (2 · 𝑢) ↔ 𝑃 ≤ (2 · (2 · 𝑢))))
348335, 18, 313, 314, 347syl112anc 1373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 / 2) ≤ (2 · 𝑢) ↔ 𝑃 ≤ (2 · (2 · 𝑢))))
349346, 348mpbird 256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 / 2) ≤ (2 · 𝑢))
350335rehalfcld 12220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 / 2) ∈ ℝ)
351268nngt0d 12022 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 0 < 𝑄)
352 lemul2 11828 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑃 / 2) ∈ ℝ ∧ (2 · 𝑢) ∈ ℝ ∧ (𝑄 ∈ ℝ ∧ 0 < 𝑄)) → ((𝑃 / 2) ≤ (2 · 𝑢) ↔ (𝑄 · (𝑃 / 2)) ≤ (𝑄 · (2 · 𝑢))))
353350, 18, 241, 351, 352syl112anc 1373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 / 2) ≤ (2 · 𝑢) ↔ (𝑄 · (𝑃 / 2)) ≤ (𝑄 · (2 · 𝑢))))
354349, 353mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 · (𝑃 / 2)) ≤ (𝑄 · (2 · 𝑢)))
355320, 354eqbrtrd 5096 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 2) · 𝑃) ≤ (𝑄 · (2 · 𝑢)))
356241, 18remulcld 11005 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 · (2 · 𝑢)) ∈ ℝ)
35762nngt0d 12022 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 0 < 𝑃)
358 lemuldiv 11855 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑄 / 2) ∈ ℝ ∧ (𝑄 · (2 · 𝑢)) ∈ ℝ ∧ (𝑃 ∈ ℝ ∧ 0 < 𝑃)) → (((𝑄 / 2) · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ↔ (𝑄 / 2) ≤ ((𝑄 · (2 · 𝑢)) / 𝑃)))
359311, 356, 335, 357, 358syl112anc 1373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑄 / 2) · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ↔ (𝑄 / 2) ≤ ((𝑄 · (2 · 𝑢)) / 𝑃)))
360355, 359mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 / 2) ≤ ((𝑄 · (2 · 𝑢)) / 𝑃))
361242, 65, 63, 245div23d 11788 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 · (2 · 𝑢)) / 𝑃) = ((𝑄 / 𝑃) · (2 · 𝑢)))
362360, 361breqtrd 5100 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 / 2) ≤ ((𝑄 / 𝑃) · (2 · 𝑢)))
363305, 311, 19, 319, 362letrd 11132 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)))
364299nnzd 12425 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑𝑁 ∈ ℤ)
365364adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ∈ ℤ)
366 flge 13525 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ ∧ 𝑁 ∈ ℤ) → (𝑁 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)) ↔ 𝑁 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
36719, 365, 366syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑁 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)) ↔ 𝑁 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
368363, 367mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))
369310, 368eqbrtrd 5096 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − 𝑁) ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))
370303, 305, 306, 369subled 11578 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ≤ 𝑁)
371370adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ≤ 𝑁)
372302nnzd 12425 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) ∈ ℤ)
373372, 20zsubcld 12431 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℤ)
374373adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℤ)
375374zred 12426 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℝ)
376299ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑁 ∈ ℕ)
377376nnred 11988 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑁 ∈ ℝ)
378 letr 11069 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑦 ∈ ℝ ∧ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∧ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ≤ 𝑁) → 𝑦𝑁))
379238, 375, 377, 378syl3anc 1370 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∧ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ≤ 𝑁) → 𝑦𝑁))
380371, 379mpan2d 691 . . . . . . . . . . . . . . . . . . . . . . 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 12431 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − (2 · 𝑢)) ∈ ℤ)
388 elfzle2 13260 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) → 𝑢𝑀)
389388adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢𝑀)
390389, 122breqtrdi 5115 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ≤ ((𝑃 − 1) / 2))
391 lemuldiv2 11856 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑢 ∈ ℝ ∧ (𝑃 − 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 𝑢) ≤ (𝑃 − 1) ↔ 𝑢 ≤ ((𝑃 − 1) / 2)))
392325, 337, 313, 314, 391syl112anc 1373 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑢) ≤ (𝑃 − 1) ↔ 𝑢 ≤ ((𝑃 − 1) / 2)))
393390, 392mpbird 256 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ≤ (𝑃 − 1))
394335ltm1d 11907 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − 1) < 𝑃)
39518, 337, 335, 393, 394lelttrd 11133 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) < 𝑃)
39618, 335posdifd 11562 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑢) < 𝑃 ↔ 0 < (𝑃 − (2 · 𝑢))))
397395, 396mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 0 < (𝑃 − (2 · 𝑢)))
398 elnnz 12329 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑃 − (2 · 𝑢)) ∈ ℕ ↔ ((𝑃 − (2 · 𝑢)) ∈ ℤ ∧ 0 < (𝑃 − (2 · 𝑢))))
399387, 397, 398sylanbrc 583 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − (2 · 𝑢)) ∈ ℕ)
40063, 65, 289sub32d 11364 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) − 1) = ((𝑃 − 1) − (2 · 𝑢)))
401122, 122oveq12i 7287 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑀 + 𝑀) = (((𝑃 − 1) / 2) + ((𝑃 − 1) / 2))
40262nnzd 12425 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℤ)
403402, 204syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − 1) ∈ ℤ)
404403zcnd 12427 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − 1) ∈ ℂ)
4054042halvesd 12219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑃 − 1) / 2) + ((𝑃 − 1) / 2)) = (𝑃 − 1))
406401, 405eqtrid 2790 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑀 + 𝑀) = (𝑃 − 1))
407406oveq1d 7290 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑀 + 𝑀) − 𝑀) = ((𝑃 − 1) − 𝑀))
408158adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑀 ∈ ℂ)
409408, 408pncan2d 11334 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑀 + 𝑀) − 𝑀) = 𝑀)
410407, 409eqtr3d 2780 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − 1) − 𝑀) = 𝑀)
411410, 333eqbrtrd 5096 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − 1) − 𝑀) < (2 · 𝑢))
412337, 321, 18, 411ltsub23d 11580 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − 1) − (2 · 𝑢)) < 𝑀)
413400, 412eqbrtrd 5096 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) − 1) < 𝑀)
414123adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑀 ∈ ℕ)
415414nnzd 12425 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑀 ∈ ℤ)
416 zlem1lt 12372 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑃 − (2 · 𝑢)) ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑃 − (2 · 𝑢)) ≤ 𝑀 ↔ ((𝑃 − (2 · 𝑢)) − 1) < 𝑀))
417387, 415, 416syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) ≤ 𝑀 ↔ ((𝑃 − (2 · 𝑢)) − 1) < 𝑀))
418413, 417mpbird 256 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − (2 · 𝑢)) ≤ 𝑀)
419 fznn 13324 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑀 ∈ ℤ → ((𝑃 − (2 · 𝑢)) ∈ (1...𝑀) ↔ ((𝑃 − (2 · 𝑢)) ∈ ℕ ∧ (𝑃 − (2 · 𝑢)) ≤ 𝑀)))
420415, 419syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) ∈ (1...𝑀) ↔ ((𝑃 − (2 · 𝑢)) ∈ ℕ ∧ (𝑃 − (2 · 𝑢)) ≤ 𝑀)))
421399, 418, 420mpbir2and 710 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − (2 · 𝑢)) ∈ (1...𝑀))
422421adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (𝑃 − (2 · 𝑢)) ∈ (1...𝑀))
423386, 422eqeltrd 2839 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → 𝑥 ∈ (1...𝑀))
424423biantrurd 533 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (𝑦 ∈ (1...𝑁) ↔ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))))
425364ad2antrr 723 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → 𝑁 ∈ ℤ)
426 fznn 13324 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ ℤ → (𝑦 ∈ (1...𝑁) ↔ (𝑦 ∈ ℕ ∧ 𝑦𝑁)))
427425, 426syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (𝑦 ∈ (1...𝑁) ↔ (𝑦 ∈ ℕ ∧ 𝑦𝑁)))
428424, 427bitr3d 280 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ↔ (𝑦 ∈ ℕ ∧ 𝑦𝑁)))
429386oveq1d 7290 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (𝑥 · 𝑄) = ((𝑃 − (2 · 𝑢)) · 𝑄))
430429breq2d 5086 . . . . . . . . . . . . . . . . . . 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 13324 . . . . . . . . . . . . . . . . . . 19 (((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℤ → (𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
434432, 433syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
435385, 431, 4343bitr4d 311 . . . . . . . . . . . . . . . . 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 3436 . . . . . . . . . . . . . . . . . . 19 𝑥 ∈ V
439 vex 3436 . . . . . . . . . . . . . . . . . . 19 𝑦 ∈ V
440438, 439op1std 7841 . . . . . . . . . . . . . . . . . 18 (𝑧 = ⟨𝑥, 𝑦⟩ → (1st𝑧) = 𝑥)
441440eqeq1d 2740 . . . . . . . . . . . . . . . . 17 (𝑧 = ⟨𝑥, 𝑦⟩ → ((1st𝑧) = (𝑃 − (2 · 𝑢)) ↔ 𝑥 = (𝑃 − (2 · 𝑢))))
442441elrab 3624 . . . . . . . . . . . . . . . 16 (⟨𝑥, 𝑦⟩ ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} ↔ (⟨𝑥, 𝑦⟩ ∈ 𝑆𝑥 = (𝑃 − (2 · 𝑢))))
443442biancomi 463 . . . . . . . . . . . . . . 15 (⟨𝑥, 𝑦⟩ ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} ↔ (𝑥 = (𝑃 − (2 · 𝑢)) ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑆))
444 opelxp 5625 . . . . . . . . . . . . . . . 16 (⟨𝑥, 𝑦⟩ ∈ ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ↔ (𝑥 ∈ {(𝑃 − (2 · 𝑢))} ∧ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
445 velsn 4577 . . . . . . . . . . . . . . . . 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 314 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⟨𝑥, 𝑦⟩ ∈ {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} ↔ ⟨𝑥, 𝑦⟩ ∈ ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))))
449227, 228, 448eqrelrdv 5702 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → {𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))} = ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
450449fveq2d 6778 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (♯‘{𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))}) = (♯‘({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))))
451 fzfid 13693 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ∈ Fin)
452 xpsnen2g 8852 . . . . . . . . . . . . . 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 14062 . . . . . . . . . . . . 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 11826 . . . . . . . . . . . . . . . . . . . . 21 (((2 · 𝑢) ∈ ℝ ∧ 𝑃 ∈ ℝ ∧ (𝑄 ∈ ℝ ∧ 0 < 𝑄)) → ((2 · 𝑢) < 𝑃 ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · 𝑃)))
45718, 335, 241, 351, 456syl112anc 1373 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑢) < 𝑃 ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · 𝑃)))
458395, 457mpbid 231 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 · (2 · 𝑢)) < (𝑄 · 𝑃))
459 ltdivmul2 11852 . . . . . . . . . . . . . . . . . . . 20 (((𝑄 · (2 · 𝑢)) ∈ ℝ ∧ 𝑄 ∈ ℝ ∧ (𝑃 ∈ ℝ ∧ 0 < 𝑃)) → (((𝑄 · (2 · 𝑢)) / 𝑃) < 𝑄 ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · 𝑃)))
460356, 241, 335, 357, 459syl112anc 1373 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑄 · (2 · 𝑢)) / 𝑃) < 𝑄 ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · 𝑃)))
461458, 460mpbird 256 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 · (2 · 𝑢)) / 𝑃) < 𝑄)
462361, 461eqbrtrrd 5098 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 𝑃) · (2 · 𝑢)) < 𝑄)
463 fllt 13526 . . . . . . . . . . . . . . . . . 18 ((((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ ∧ 𝑄 ∈ ℤ) → (((𝑄 / 𝑃) · (2 · 𝑢)) < 𝑄 ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < 𝑄))
46419, 269, 463syl2anc 584 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑄 / 𝑃) · (2 · 𝑢)) < 𝑄 ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < 𝑄))
465462, 464mpbid 231 . . . . . . . . . . . . . . . 16 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < 𝑄)
466 zltlem1 12373 . . . . . . . . . . . . . . . . 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 5102 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ≤ (2 · 𝑁))
470 eluz2 12588 . . . . . . . . . . . . . 14 ((2 · 𝑁) ∈ (ℤ‘(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ↔ ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ ∧ (2 · 𝑁) ∈ ℤ ∧ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ≤ (2 · 𝑁)))
47120, 372, 469, 470syl3anbrc 1342 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) ∈ (ℤ‘(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
472 uznn0sub 12617 . . . . . . . . . . . . 13 ((2 · 𝑁) ∈ (ℤ‘(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℕ0)
473 hashfz1 14060 . . . . . . . . . . . . 13 (((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℕ0 → (♯‘(1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) = ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
474471, 472, 4733syl 18 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (♯‘(1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) = ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
475450, 455, 4743eqtrd 2782 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (♯‘{𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))}) = ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
476475sumeq2dv 15415 . . . . . . . . . 10 (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(♯‘{𝑧𝑆 ∣ (1st𝑧) = (𝑃 − (2 · 𝑢))}) = Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
47780, 224, 4763eqtr3rd 2787 . . . . . . . . 9 (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))
478301nncnd 11989 . . . . . . . . . . 11 (𝜑 → (2 · 𝑁) ∈ ℂ)
479478adantr 481 . . . . . . . . . 10 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) ∈ ℂ)
4805, 479, 290fsumsub 15500 . . . . . . . . 9 (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) − Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
481477, 480eqtr3d 2780 . . . . . . . 8 (𝜑 → (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) = (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) − Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
482481oveq2d 7291 . . . . . . 7 (𝜑 → (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) = (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) − Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
48321zcnd 12427 . . . . . . . 8 (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℂ)
4845, 372fsumzcl 15447 . . . . . . . . 9 (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) ∈ ℤ)
485484zcnd 12427 . . . . . . . 8 (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) ∈ ℂ)
486483, 485pncan3d 11335 . . . . . . 7 (𝜑 → (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) − Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁))
487 fsumconst 15502 . . . . . . . . 9 (((((⌊‘(𝑀 / 2)) + 1)...𝑀) ∈ Fin ∧ (2 · 𝑁) ∈ ℂ) → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) = ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · (2 · 𝑁)))
4885, 478, 487syl2anc 584 . . . . . . . 8 (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) = ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · (2 · 𝑁)))
489 hashcl 14071 . . . . . . . . . . 11 ((((⌊‘(𝑀 / 2)) + 1)...𝑀) ∈ Fin → (♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∈ ℕ0)
4905, 489syl 17 . . . . . . . . . 10 (𝜑 → (♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∈ ℕ0)
491490nn0cnd 12295 . . . . . . . . 9 (𝜑 → (♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∈ ℂ)
492 2cnd 12051 . . . . . . . . 9 (𝜑 → 2 ∈ ℂ)
493491, 492, 307mul12d 11184 . . . . . . . 8 (𝜑 → ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · (2 · 𝑁)) = (2 · ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)))
494488, 493eqtrd 2778 . . . . . . 7 (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) = (2 · ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)))
495482, 486, 4943eqtrd 2782 . . . . . 6 (𝜑 → (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) = (2 · ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)))
496495oveq2d 7291 . . . . 5 (𝜑 → (-1↑(Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))) = (-1↑(2 · ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁))))
49713a1i 11 . . . . . 6 (𝜑 → 2 ∈ ℤ)
498490nn0zd 12424 . . . . . . 7 (𝜑 → (♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∈ ℤ)
499498, 364zmulcld 12432 . . . . . 6 (𝜑 → ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁) ∈ ℤ)
500 expmulz 13829 . . . . . 6 (((-1 ∈ ℂ ∧ -1 ≠ 0) ∧ (2 ∈ ℤ ∧ ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁) ∈ ℤ)) → (-1↑(2 · ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁))) = ((-1↑2)↑((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)))
5012, 4, 497, 499, 500syl22anc 836 . . . . 5 (𝜑 → (-1↑(2 · ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁))) = ((-1↑2)↑((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)))
502 neg1sqe1 13913 . . . . . . 7 (-1↑2) = 1
503502oveq1i 7285 . . . . . 6 ((-1↑2)↑((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)) = (1↑((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁))
504 1exp 13812 . . . . . . 7 (((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁) ∈ ℤ → (1↑((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)) = 1)
505499, 504syl 17 . . . . . 6 (𝜑 → (1↑((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)) = 1)
506503, 505eqtrid 2790 . . . . 5 (𝜑 → ((-1↑2)↑((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)) = 1)
507496, 501, 5063eqtrd 2782 . . . 4 (𝜑 → (-1↑(Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))) = 1)
50841, 52, 5073eqtr4d 2788 . . 3 (𝜑 → ((-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) · (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))) = (-1↑(Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))))
509 expaddz 13827 . . . 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 836 . . 3 (𝜑 → (-1↑(Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))) = ((-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) · (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))))
511508, 510eqtr2d 2779 . 2 (𝜑 → ((-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) · (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))) = ((-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) · (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))))
51222, 38, 38, 40, 511mulcan2ad 11611 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 1539  wcel 2106  wne 2943  wral 3064  wrex 3065  {crab 3068  cdif 3884  wss 3887  {csn 4561  cop 4567   ciun 4924  Disj wdisj 5039   class class class wbr 5074  {copab 5136   × cxp 5587  Rel wrel 5594  cfv 6433  (class class class)co 7275  1st c1st 7829  cen 8730  Fincfn 8733  cc 10869  cr 10870  0cc0 10871  1c1 10872   + caddc 10874   · cmul 10876   < clt 11009  cle 11010  cmin 11205  -cneg 11206   / cdiv 11632  cn 11973  2c2 12028  0cn0 12233  cz 12319  cuz 12582  ...cfz 13239  cfl 13510  cexp 13782  chash 14044  Σcsu 15397  cdvds 15963  cprime 16376
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  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 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-inf2 9399  ax-cnex 10927  ax-resscn 10928  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-addrcl 10932  ax-mulcl 10933  ax-mulrcl 10934  ax-mulcom 10935  ax-addass 10936  ax-mulass 10937  ax-distr 10938  ax-i2m1 10939  ax-1ne0 10940  ax-1rid 10941  ax-rnegex 10942  ax-rrecex 10943  ax-cnre 10944  ax-pre-lttri 10945  ax-pre-lttrn 10946  ax-pre-ltadd 10947  ax-pre-mulgt0 10948  ax-pre-sup 10949
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-rmo 3071  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-int 4880  df-iun 4926  df-disj 5040  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-se 5545  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-isom 6442  df-riota 7232  df-ov 7278  df-oprab 7279  df-mpo 7280  df-om 7713  df-1st 7831  df-2nd 7832  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-rdg 8241  df-1o 8297  df-2o 8298  df-er 8498  df-en 8734  df-dom 8735  df-sdom 8736  df-fin 8737  df-sup 9201  df-inf 9202  df-oi 9269  df-card 9697  df-pnf 11011  df-mnf 11012  df-xr 11013  df-ltxr 11014  df-le 11015  df-sub 11207  df-neg 11208  df-div 11633  df-nn 11974  df-2 12036  df-3 12037  df-4 12038  df-n0 12234  df-z 12320  df-uz 12583  df-rp 12731  df-fz 13240  df-fzo 13383  df-fl 13512  df-seq 13722  df-exp 13783  df-hash 14045  df-cj 14810  df-re 14811  df-im 14812  df-sqrt 14946  df-abs 14947  df-clim 15197  df-sum 15398  df-dvds 15964  df-prm 16377
This theorem is referenced by:  lgsquadlem2  26529
  Copyright terms: Public domain W3C validator