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

Theorem lgsquadlem2 25968
Description: Lemma for lgsquad 25970. Count the members of 𝑆 with even coordinates, and combine with lgsquadlem1 25967 to get the total count of lattice points in 𝑆 (up to parity). (Contributed by Mario Carneiro, 18-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
lgsquadlem2 (𝜑 → (𝑄 /L 𝑃) = (-1↑(♯‘𝑆)))
Distinct variable groups:   𝑥,𝑦,𝑃   𝜑,𝑥,𝑦   𝑦,𝑀   𝑥,𝑁,𝑦   𝑥,𝑄,𝑦   𝑥,𝑆   𝑥,𝑀   𝑦,𝑆

Proof of Theorem lgsquadlem2
Dummy variables 𝑢 𝑣 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 lgseisen.1 . . 3 (𝜑𝑃 ∈ (ℙ ∖ {2}))
2 lgseisen.2 . . 3 (𝜑𝑄 ∈ (ℙ ∖ {2}))
3 lgseisen.3 . . 3 (𝜑𝑃𝑄)
41, 2, 3lgseisen 25966 . 2 (𝜑 → (𝑄 /L 𝑃) = (-1↑Σ𝑢 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
5 lgsquad.4 . . . . . 6 𝑀 = ((𝑃 − 1) / 2)
65oveq2i 7160 . . . . 5 (1...𝑀) = (1...((𝑃 − 1) / 2))
76sumeq1i 15055 . . . 4 Σ𝑢 ∈ (1...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = Σ𝑢 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))
81, 5gausslemma2dlem0b 25944 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℕ)
98nnred 11649 . . . . . . . . . 10 (𝜑𝑀 ∈ ℝ)
109rehalfcld 11881 . . . . . . . . 9 (𝜑 → (𝑀 / 2) ∈ ℝ)
1110flcld 13172 . . . . . . . 8 (𝜑 → (⌊‘(𝑀 / 2)) ∈ ℤ)
1211zred 12084 . . . . . . 7 (𝜑 → (⌊‘(𝑀 / 2)) ∈ ℝ)
1312ltp1d 11568 . . . . . 6 (𝜑 → (⌊‘(𝑀 / 2)) < ((⌊‘(𝑀 / 2)) + 1))
14 fzdisj 12938 . . . . . 6 ((⌊‘(𝑀 / 2)) < ((⌊‘(𝑀 / 2)) + 1) → ((1...(⌊‘(𝑀 / 2))) ∩ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) = ∅)
1513, 14syl 17 . . . . 5 (𝜑 → ((1...(⌊‘(𝑀 / 2))) ∩ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) = ∅)
168nnrpd 12426 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℝ+)
1716rphalfcld 12440 . . . . . . . . . 10 (𝜑 → (𝑀 / 2) ∈ ℝ+)
1817rpge0d 12432 . . . . . . . . 9 (𝜑 → 0 ≤ (𝑀 / 2))
19 flge0nn0 13194 . . . . . . . . 9 (((𝑀 / 2) ∈ ℝ ∧ 0 ≤ (𝑀 / 2)) → (⌊‘(𝑀 / 2)) ∈ ℕ0)
2010, 18, 19syl2anc 587 . . . . . . . 8 (𝜑 → (⌊‘(𝑀 / 2)) ∈ ℕ0)
218nnnn0d 11952 . . . . . . . 8 (𝜑𝑀 ∈ ℕ0)
22 rphalflt 12415 . . . . . . . . . . 11 (𝑀 ∈ ℝ+ → (𝑀 / 2) < 𝑀)
2316, 22syl 17 . . . . . . . . . 10 (𝜑 → (𝑀 / 2) < 𝑀)
248nnzd 12083 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℤ)
25 fllt 13180 . . . . . . . . . . 11 (((𝑀 / 2) ∈ ℝ ∧ 𝑀 ∈ ℤ) → ((𝑀 / 2) < 𝑀 ↔ (⌊‘(𝑀 / 2)) < 𝑀))
2610, 24, 25syl2anc 587 . . . . . . . . . 10 (𝜑 → ((𝑀 / 2) < 𝑀 ↔ (⌊‘(𝑀 / 2)) < 𝑀))
2723, 26mpbid 235 . . . . . . . . 9 (𝜑 → (⌊‘(𝑀 / 2)) < 𝑀)
2812, 9, 27ltled 10786 . . . . . . . 8 (𝜑 → (⌊‘(𝑀 / 2)) ≤ 𝑀)
29 elfz2nn0 13002 . . . . . . . 8 ((⌊‘(𝑀 / 2)) ∈ (0...𝑀) ↔ ((⌊‘(𝑀 / 2)) ∈ ℕ0𝑀 ∈ ℕ0 ∧ (⌊‘(𝑀 / 2)) ≤ 𝑀))
3020, 21, 28, 29syl3anbrc 1340 . . . . . . 7 (𝜑 → (⌊‘(𝑀 / 2)) ∈ (0...𝑀))
31 nn0uz 12277 . . . . . . . . 9 0 = (ℤ‘0)
3221, 31eleqtrdi 2926 . . . . . . . 8 (𝜑𝑀 ∈ (ℤ‘0))
33 elfzp12 12990 . . . . . . . 8 (𝑀 ∈ (ℤ‘0) → ((⌊‘(𝑀 / 2)) ∈ (0...𝑀) ↔ ((⌊‘(𝑀 / 2)) = 0 ∨ (⌊‘(𝑀 / 2)) ∈ ((0 + 1)...𝑀))))
3432, 33syl 17 . . . . . . 7 (𝜑 → ((⌊‘(𝑀 / 2)) ∈ (0...𝑀) ↔ ((⌊‘(𝑀 / 2)) = 0 ∨ (⌊‘(𝑀 / 2)) ∈ ((0 + 1)...𝑀))))
3530, 34mpbid 235 . . . . . 6 (𝜑 → ((⌊‘(𝑀 / 2)) = 0 ∨ (⌊‘(𝑀 / 2)) ∈ ((0 + 1)...𝑀)))
36 oveq2 7157 . . . . . . . . . 10 ((⌊‘(𝑀 / 2)) = 0 → (1...(⌊‘(𝑀 / 2))) = (1...0))
37 fz10 12932 . . . . . . . . . 10 (1...0) = ∅
3836, 37syl6eq 2875 . . . . . . . . 9 ((⌊‘(𝑀 / 2)) = 0 → (1...(⌊‘(𝑀 / 2))) = ∅)
39 oveq1 7156 . . . . . . . . . . 11 ((⌊‘(𝑀 / 2)) = 0 → ((⌊‘(𝑀 / 2)) + 1) = (0 + 1))
40 0p1e1 11756 . . . . . . . . . . 11 (0 + 1) = 1
4139, 40syl6eq 2875 . . . . . . . . . 10 ((⌊‘(𝑀 / 2)) = 0 → ((⌊‘(𝑀 / 2)) + 1) = 1)
4241oveq1d 7164 . . . . . . . . 9 ((⌊‘(𝑀 / 2)) = 0 → (((⌊‘(𝑀 / 2)) + 1)...𝑀) = (1...𝑀))
4338, 42uneq12d 4126 . . . . . . . 8 ((⌊‘(𝑀 / 2)) = 0 → ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) = (∅ ∪ (1...𝑀)))
44 un0 4327 . . . . . . . . 9 ((1...𝑀) ∪ ∅) = (1...𝑀)
45 uncom 4115 . . . . . . . . 9 ((1...𝑀) ∪ ∅) = (∅ ∪ (1...𝑀))
4644, 45eqtr3i 2849 . . . . . . . 8 (1...𝑀) = (∅ ∪ (1...𝑀))
4743, 46syl6reqr 2878 . . . . . . 7 ((⌊‘(𝑀 / 2)) = 0 → (1...𝑀) = ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀)))
48 fzsplit 12937 . . . . . . . 8 ((⌊‘(𝑀 / 2)) ∈ (1...𝑀) → (1...𝑀) = ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀)))
4940oveq1i 7159 . . . . . . . 8 ((0 + 1)...𝑀) = (1...𝑀)
5048, 49eleq2s 2934 . . . . . . 7 ((⌊‘(𝑀 / 2)) ∈ ((0 + 1)...𝑀) → (1...𝑀) = ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀)))
5147, 50jaoi 854 . . . . . 6 (((⌊‘(𝑀 / 2)) = 0 ∨ (⌊‘(𝑀 / 2)) ∈ ((0 + 1)...𝑀)) → (1...𝑀) = ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀)))
5235, 51syl 17 . . . . 5 (𝜑 → (1...𝑀) = ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀)))
53 fzfid 13345 . . . . 5 (𝜑 → (1...𝑀) ∈ Fin)
542gausslemma2dlem0a 25943 . . . . . . . . . . 11 (𝜑𝑄 ∈ ℕ)
5554nnred 11649 . . . . . . . . . 10 (𝜑𝑄 ∈ ℝ)
561gausslemma2dlem0a 25943 . . . . . . . . . 10 (𝜑𝑃 ∈ ℕ)
5755, 56nndivred 11688 . . . . . . . . 9 (𝜑 → (𝑄 / 𝑃) ∈ ℝ)
5857adantr 484 . . . . . . . 8 ((𝜑𝑢 ∈ (1...𝑀)) → (𝑄 / 𝑃) ∈ ℝ)
59 2nn 11707 . . . . . . . . . 10 2 ∈ ℕ
60 elfznn 12940 . . . . . . . . . . 11 (𝑢 ∈ (1...𝑀) → 𝑢 ∈ ℕ)
6160adantl 485 . . . . . . . . . 10 ((𝜑𝑢 ∈ (1...𝑀)) → 𝑢 ∈ ℕ)
62 nnmulcl 11658 . . . . . . . . . 10 ((2 ∈ ℕ ∧ 𝑢 ∈ ℕ) → (2 · 𝑢) ∈ ℕ)
6359, 61, 62sylancr 590 . . . . . . . . 9 ((𝜑𝑢 ∈ (1...𝑀)) → (2 · 𝑢) ∈ ℕ)
6463nnred 11649 . . . . . . . 8 ((𝜑𝑢 ∈ (1...𝑀)) → (2 · 𝑢) ∈ ℝ)
6558, 64remulcld 10669 . . . . . . 7 ((𝜑𝑢 ∈ (1...𝑀)) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ)
6654nnrpd 12426 . . . . . . . . . . 11 (𝜑𝑄 ∈ ℝ+)
6756nnrpd 12426 . . . . . . . . . . 11 (𝜑𝑃 ∈ ℝ+)
6866, 67rpdivcld 12445 . . . . . . . . . 10 (𝜑 → (𝑄 / 𝑃) ∈ ℝ+)
6968adantr 484 . . . . . . . . 9 ((𝜑𝑢 ∈ (1...𝑀)) → (𝑄 / 𝑃) ∈ ℝ+)
7063nnrpd 12426 . . . . . . . . 9 ((𝜑𝑢 ∈ (1...𝑀)) → (2 · 𝑢) ∈ ℝ+)
7169, 70rpmulcld 12444 . . . . . . . 8 ((𝜑𝑢 ∈ (1...𝑀)) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ+)
7271rpge0d 12432 . . . . . . 7 ((𝜑𝑢 ∈ (1...𝑀)) → 0 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)))
73 flge0nn0 13194 . . . . . . 7 ((((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ ∧ 0 ≤ ((𝑄 / 𝑃) · (2 · 𝑢))) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℕ0)
7465, 72, 73syl2anc 587 . . . . . 6 ((𝜑𝑢 ∈ (1...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℕ0)
7574nn0cnd 11954 . . . . 5 ((𝜑𝑢 ∈ (1...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℂ)
7615, 52, 53, 75fsumsplit 15097 . . . 4 (𝜑 → Σ𝑢 ∈ (1...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = (Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
777, 76syl5eqr 2873 . . 3 (𝜑 → Σ𝑢 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = (Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
7877oveq2d 7165 . 2 (𝜑 → (-1↑Σ𝑢 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (-1↑(Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
79 neg1cn 11748 . . . . 5 -1 ∈ ℂ
8079a1i 11 . . . 4 (𝜑 → -1 ∈ ℂ)
81 fzfid 13345 . . . . 5 (𝜑 → (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∈ Fin)
82 ssun2 4135 . . . . . . . 8 (((⌊‘(𝑀 / 2)) + 1)...𝑀) ⊆ ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀))
8382, 52sseqtrrid 4006 . . . . . . 7 (𝜑 → (((⌊‘(𝑀 / 2)) + 1)...𝑀) ⊆ (1...𝑀))
8483sselda 3953 . . . . . 6 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ∈ (1...𝑀))
8584, 74syldan 594 . . . . 5 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℕ0)
8681, 85fsumnn0cl 15093 . . . 4 (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℕ0)
87 fzfid 13345 . . . . 5 (𝜑 → (1...(⌊‘(𝑀 / 2))) ∈ Fin)
88 ssun1 4134 . . . . . . . 8 (1...(⌊‘(𝑀 / 2))) ⊆ ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀))
8988, 52sseqtrrid 4006 . . . . . . 7 (𝜑 → (1...(⌊‘(𝑀 / 2))) ⊆ (1...𝑀))
9089sselda 3953 . . . . . 6 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ∈ (1...𝑀))
9190, 74syldan 594 . . . . 5 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℕ0)
9287, 91fsumnn0cl 15093 . . . 4 (𝜑 → Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℕ0)
9380, 86, 92expaddd 13517 . . 3 (𝜑 → (-1↑(Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = ((-1↑Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) · (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
94 fzfid 13345 . . . . . . . . 9 (𝜑 → (1...𝑁) ∈ Fin)
95 xpfi 8786 . . . . . . . . 9 (((1...𝑀) ∈ Fin ∧ (1...𝑁) ∈ Fin) → ((1...𝑀) × (1...𝑁)) ∈ Fin)
9653, 94, 95syl2anc 587 . . . . . . . 8 (𝜑 → ((1...𝑀) × (1...𝑁)) ∈ Fin)
97 lgsquad.6 . . . . . . . . 9 𝑆 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))}
98 opabssxp 5630 . . . . . . . . 9 {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} ⊆ ((1...𝑀) × (1...𝑁))
9997, 98eqsstri 3987 . . . . . . . 8 𝑆 ⊆ ((1...𝑀) × (1...𝑁))
100 ssfi 8735 . . . . . . . 8 ((((1...𝑀) × (1...𝑁)) ∈ Fin ∧ 𝑆 ⊆ ((1...𝑀) × (1...𝑁))) → 𝑆 ∈ Fin)
10196, 99, 100sylancl 589 . . . . . . 7 (𝜑𝑆 ∈ Fin)
102 ssrab2 4042 . . . . . . 7 {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)} ⊆ 𝑆
103 ssfi 8735 . . . . . . 7 ((𝑆 ∈ Fin ∧ {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)} ⊆ 𝑆) → {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)} ∈ Fin)
104101, 102, 103sylancl 589 . . . . . 6 (𝜑 → {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)} ∈ Fin)
105 hashcl 13722 . . . . . 6 ({𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)} ∈ Fin → (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) ∈ ℕ0)
106104, 105syl 17 . . . . 5 (𝜑 → (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) ∈ ℕ0)
107 ssrab2 4042 . . . . . . 7 {𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ⊆ 𝑆
108 ssfi 8735 . . . . . . 7 ((𝑆 ∈ Fin ∧ {𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ⊆ 𝑆) → {𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∈ Fin)
109101, 107, 108sylancl 589 . . . . . 6 (𝜑 → {𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∈ Fin)
110 hashcl 13722 . . . . . 6 ({𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∈ Fin → (♯‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)}) ∈ ℕ0)
111109, 110syl 17 . . . . 5 (𝜑 → (♯‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)}) ∈ ℕ0)
11280, 106, 111expaddd 13517 . . . 4 (𝜑 → (-1↑((♯‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)}) + (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))) = ((-1↑(♯‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)})) · (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))))
11390, 63syldan 594 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (2 · 𝑢) ∈ ℕ)
114 fzfid 13345 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ Fin)
115 xpsnen2g 8606 . . . . . . . . . . 11 (((2 · 𝑢) ∈ ℕ ∧ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ Fin) → ({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ≈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
116113, 114, 115syl2anc 587 . . . . . . . . . 10 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ≈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
117 hasheni 13713 . . . . . . . . . 10 (({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ≈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) → (♯‘({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) = (♯‘(1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
118116, 117syl 17 . . . . . . . . 9 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (♯‘({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) = (♯‘(1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
119 ssrab2 4042 . . . . . . . . . . . . 13 {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} ⊆ 𝑆
12097relopabi 5681 . . . . . . . . . . . . 13 Rel 𝑆
121 relss 5643 . . . . . . . . . . . . 13 ({𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} ⊆ 𝑆 → (Rel 𝑆 → Rel {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)}))
122119, 120, 121mp2 9 . . . . . . . . . . . 12 Rel {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)}
123 relxp 5560 . . . . . . . . . . . 12 Rel ({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
12497eleq2i 2907 . . . . . . . . . . . . . . . 16 (⟨𝑥, 𝑦⟩ ∈ 𝑆 ↔ ⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))})
125 opabidw 5399 . . . . . . . . . . . . . . . 16 (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} ↔ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))
126124, 125bitri 278 . . . . . . . . . . . . . . 15 (⟨𝑥, 𝑦⟩ ∈ 𝑆 ↔ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))
127 anass 472 . . . . . . . . . . . . . . . . . 18 (((𝑦 ∈ ℕ ∧ 𝑦𝑁) ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢))) ↔ (𝑦 ∈ ℕ ∧ (𝑦𝑁 ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)))))
128113adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2 · 𝑢) ∈ ℕ)
129128nnred 11649 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2 · 𝑢) ∈ ℝ)
13056ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℕ)
131130nnred 11649 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℝ)
132131rehalfcld 11881 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 / 2) ∈ ℝ)
1339adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑀 ∈ ℝ)
134133adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑀 ∈ ℝ)
135 elfzle2 12915 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) → 𝑢 ≤ (⌊‘(𝑀 / 2)))
136135adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ≤ (⌊‘(𝑀 / 2)))
137133rehalfcld 11881 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (𝑀 / 2) ∈ ℝ)
138 elfzelz 12911 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) → 𝑢 ∈ ℤ)
139138adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ∈ ℤ)
140 flge 13179 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑀 / 2) ∈ ℝ ∧ 𝑢 ∈ ℤ) → (𝑢 ≤ (𝑀 / 2) ↔ 𝑢 ≤ (⌊‘(𝑀 / 2))))
141137, 139, 140syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (𝑢 ≤ (𝑀 / 2) ↔ 𝑢 ≤ (⌊‘(𝑀 / 2))))
142136, 141mpbird 260 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ≤ (𝑀 / 2))
143 elfznn 12940 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) → 𝑢 ∈ ℕ)
144143adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ∈ ℕ)
145144nnred 11649 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ∈ ℝ)
146 2re 11708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 2 ∈ ℝ
147146a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 2 ∈ ℝ)
148 2pos 11737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 0 < 2
149148a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 0 < 2)
150 lemuldiv2 11519 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑢 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 𝑢) ≤ 𝑀𝑢 ≤ (𝑀 / 2)))
151145, 133, 147, 149, 150syl112anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((2 · 𝑢) ≤ 𝑀𝑢 ≤ (𝑀 / 2)))
152142, 151mpbird 260 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (2 · 𝑢) ≤ 𝑀)
153152adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2 · 𝑢) ≤ 𝑀)
154131ltm1d 11570 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 − 1) < 𝑃)
155 peano2rem 10951 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑃 ∈ ℝ → (𝑃 − 1) ∈ ℝ)
156131, 155syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 − 1) ∈ ℝ)
157146a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 2 ∈ ℝ)
158148a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 0 < 2)
159 ltdiv1 11502 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑃 − 1) ∈ ℝ ∧ 𝑃 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((𝑃 − 1) < 𝑃 ↔ ((𝑃 − 1) / 2) < (𝑃 / 2)))
160156, 131, 157, 158, 159syl112anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑃 − 1) < 𝑃 ↔ ((𝑃 − 1) / 2) < (𝑃 / 2)))
161154, 160mpbid 235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑃 − 1) / 2) < (𝑃 / 2))
1625, 161eqbrtrid 5087 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑀 < (𝑃 / 2))
163129, 134, 132, 153, 162lelttrd 10796 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2 · 𝑢) < (𝑃 / 2))
164130nnrpd 12426 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℝ+)
165 rphalflt 12415 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑃 ∈ ℝ+ → (𝑃 / 2) < 𝑃)
166164, 165syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 / 2) < 𝑃)
167129, 132, 131, 163, 166lttrd 10799 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2 · 𝑢) < 𝑃)
168129, 131ltnled 10785 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((2 · 𝑢) < 𝑃 ↔ ¬ 𝑃 ≤ (2 · 𝑢)))
169167, 168mpbid 235 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ¬ 𝑃 ≤ (2 · 𝑢))
1701eldifad 3931 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝑃 ∈ ℙ)
171170ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℙ)
172 prmz 16017 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
173171, 172syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℤ)
174 dvdsle 15660 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑃 ∈ ℤ ∧ (2 · 𝑢) ∈ ℕ) → (𝑃 ∥ (2 · 𝑢) → 𝑃 ≤ (2 · 𝑢)))
175173, 128, 174syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 ∥ (2 · 𝑢) → 𝑃 ≤ (2 · 𝑢)))
176169, 175mtod 201 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ¬ 𝑃 ∥ (2 · 𝑢))
1772eldifad 3931 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝑄 ∈ ℙ)
178 prmrp 16054 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ) → ((𝑃 gcd 𝑄) = 1 ↔ 𝑃𝑄))
179170, 177, 178syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ((𝑃 gcd 𝑄) = 1 ↔ 𝑃𝑄))
1803, 179mpbird 260 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝑃 gcd 𝑄) = 1)
181180ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 gcd 𝑄) = 1)
182177ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈ ℙ)
183 prmz 16017 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑄 ∈ ℙ → 𝑄 ∈ ℤ)
184182, 183syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈ ℤ)
185128nnzd 12083 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2 · 𝑢) ∈ ℤ)
186 coprmdvds 15995 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑃 ∈ ℤ ∧ 𝑄 ∈ ℤ ∧ (2 · 𝑢) ∈ ℤ) → ((𝑃 ∥ (𝑄 · (2 · 𝑢)) ∧ (𝑃 gcd 𝑄) = 1) → 𝑃 ∥ (2 · 𝑢)))
187173, 184, 185, 186syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑃 ∥ (𝑄 · (2 · 𝑢)) ∧ (𝑃 gcd 𝑄) = 1) → 𝑃 ∥ (2 · 𝑢)))
188181, 187mpan2d 693 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 ∥ (𝑄 · (2 · 𝑢)) → 𝑃 ∥ (2 · 𝑢)))
189176, 188mtod 201 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ¬ 𝑃 ∥ (𝑄 · (2 · 𝑢)))
190 nnz 12001 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 ∈ ℕ → 𝑦 ∈ ℤ)
191190adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ ℤ)
192 dvdsmul2 15632 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑦 ∈ ℤ ∧ 𝑃 ∈ ℤ) → 𝑃 ∥ (𝑦 · 𝑃))
193191, 173, 192syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∥ (𝑦 · 𝑃))
194 breq2 5056 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑄 · (2 · 𝑢)) = (𝑦 · 𝑃) → (𝑃 ∥ (𝑄 · (2 · 𝑢)) ↔ 𝑃 ∥ (𝑦 · 𝑃)))
195193, 194syl5ibrcom 250 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 · (2 · 𝑢)) = (𝑦 · 𝑃) → 𝑃 ∥ (𝑄 · (2 · 𝑢))))
196195necon3bd 3028 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (¬ 𝑃 ∥ (𝑄 · (2 · 𝑢)) → (𝑄 · (2 · 𝑢)) ≠ (𝑦 · 𝑃)))
197189, 196mpd 15 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (2 · 𝑢)) ≠ (𝑦 · 𝑃))
198 simpr 488 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ ℕ)
199198, 130nnmulcld 11687 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 · 𝑃) ∈ ℕ)
200199nnred 11649 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 · 𝑃) ∈ ℝ)
20154adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑄 ∈ ℕ)
202201, 113nnmulcld 11687 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (𝑄 · (2 · 𝑢)) ∈ ℕ)
203202adantr 484 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (2 · 𝑢)) ∈ ℕ)
204203nnred 11649 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (2 · 𝑢)) ∈ ℝ)
205200, 204ltlend 10783 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ↔ ((𝑦 · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ∧ (𝑄 · (2 · 𝑢)) ≠ (𝑦 · 𝑃))))
206197, 205mpbiran2d 707 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ↔ (𝑦 · 𝑃) ≤ (𝑄 · (2 · 𝑢))))
207 nnre 11641 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
208207adantl 485 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ ℝ)
209130nngt0d 11683 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 0 < 𝑃)
210 lemuldiv 11518 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 ∈ ℝ ∧ (𝑄 · (2 · 𝑢)) ∈ ℝ ∧ (𝑃 ∈ ℝ ∧ 0 < 𝑃)) → ((𝑦 · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ↔ 𝑦 ≤ ((𝑄 · (2 · 𝑢)) / 𝑃)))
211208, 204, 131, 209, 210syl112anc 1371 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ↔ 𝑦 ≤ ((𝑄 · (2 · 𝑢)) / 𝑃)))
212201adantr 484 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈ ℕ)
213212nncnd 11650 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈ ℂ)
214128nncnd 11650 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2 · 𝑢) ∈ ℂ)
215130nncnd 11650 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℂ)
216130nnne0d 11684 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ≠ 0)
217213, 214, 215, 216div23d 11451 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 · (2 · 𝑢)) / 𝑃) = ((𝑄 / 𝑃) · (2 · 𝑢)))
218217breq2d 5064 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 ≤ ((𝑄 · (2 · 𝑢)) / 𝑃) ↔ 𝑦 ≤ ((𝑄 / 𝑃) · (2 · 𝑢))))
219206, 211, 2183bitrd 308 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ↔ 𝑦 ≤ ((𝑄 / 𝑃) · (2 · 𝑢))))
220212nnred 11649 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈ ℝ)
221212nngt0d 11683 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 0 < 𝑄)
222 ltmul2 11489 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((2 · 𝑢) ∈ ℝ ∧ (𝑃 / 2) ∈ ℝ ∧ (𝑄 ∈ ℝ ∧ 0 < 𝑄)) → ((2 · 𝑢) < (𝑃 / 2) ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · (𝑃 / 2))))
223129, 132, 220, 221, 222syl112anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((2 · 𝑢) < (𝑃 / 2) ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · (𝑃 / 2))))
224163, 223mpbid 235 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (2 · 𝑢)) < (𝑄 · (𝑃 / 2)))
225 2cnd 11712 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 2 ∈ ℂ)
226 2ne0 11738 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 2 ≠ 0
227226a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 2 ≠ 0)
228 divass 11314 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑄 ∈ ℂ ∧ 𝑃 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((𝑄 · 𝑃) / 2) = (𝑄 · (𝑃 / 2)))
229 div23 11315 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑄 ∈ ℂ ∧ 𝑃 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((𝑄 · 𝑃) / 2) = ((𝑄 / 2) · 𝑃))
230228, 229eqtr3d 2861 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑄 ∈ ℂ ∧ 𝑃 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (𝑄 · (𝑃 / 2)) = ((𝑄 / 2) · 𝑃))
231213, 215, 225, 227, 230syl112anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (𝑃 / 2)) = ((𝑄 / 2) · 𝑃))
232224, 231breqtrd 5078 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (2 · 𝑢)) < ((𝑄 / 2) · 𝑃))
233220rehalfcld 11881 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 / 2) ∈ ℝ)
234233, 131remulcld 10669 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 / 2) · 𝑃) ∈ ℝ)
235 lttr 10715 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑦 · 𝑃) ∈ ℝ ∧ (𝑄 · (2 · 𝑢)) ∈ ℝ ∧ ((𝑄 / 2) · 𝑃) ∈ ℝ) → (((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ∧ (𝑄 · (2 · 𝑢)) < ((𝑄 / 2) · 𝑃)) → (𝑦 · 𝑃) < ((𝑄 / 2) · 𝑃)))
236200, 204, 234, 235syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ∧ (𝑄 · (2 · 𝑢)) < ((𝑄 / 2) · 𝑃)) → (𝑦 · 𝑃) < ((𝑄 / 2) · 𝑃)))
237232, 236mpan2d 693 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) → (𝑦 · 𝑃) < ((𝑄 / 2) · 𝑃)))
238 ltmul1 11488 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑦 ∈ ℝ ∧ (𝑄 / 2) ∈ ℝ ∧ (𝑃 ∈ ℝ ∧ 0 < 𝑃)) → (𝑦 < (𝑄 / 2) ↔ (𝑦 · 𝑃) < ((𝑄 / 2) · 𝑃)))
239208, 233, 131, 209, 238syl112anc 1371 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 < (𝑄 / 2) ↔ (𝑦 · 𝑃) < ((𝑄 / 2) · 𝑃)))
240237, 239sylibrd 262 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) → 𝑦 < (𝑄 / 2)))
241 peano2rem 10951 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑄 ∈ ℝ → (𝑄 − 1) ∈ ℝ)
242220, 241syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 − 1) ∈ ℝ)
243242recnd 10667 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 − 1) ∈ ℂ)
244213, 243, 225, 227divsubdird 11453 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 − (𝑄 − 1)) / 2) = ((𝑄 / 2) − ((𝑄 − 1) / 2)))
245 lgsquad.5 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑁 = ((𝑄 − 1) / 2)
246245oveq2i 7160 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑄 / 2) − 𝑁) = ((𝑄 / 2) − ((𝑄 − 1) / 2))
247244, 246syl6eqr 2877 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 − (𝑄 − 1)) / 2) = ((𝑄 / 2) − 𝑁))
248 ax-1cn 10593 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 1 ∈ ℂ
249 nncan 10913 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑄 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑄 − (𝑄 − 1)) = 1)
250213, 248, 249sylancl 589 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 − (𝑄 − 1)) = 1)
251250oveq1d 7164 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 − (𝑄 − 1)) / 2) = (1 / 2))
252 halflt1 11852 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (1 / 2) < 1
253251, 252eqbrtrdi 5091 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 − (𝑄 − 1)) / 2) < 1)
254247, 253eqbrtrrd 5076 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 / 2) − 𝑁) < 1)
2552, 245gausslemma2dlem0b 25944 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝑁 ∈ ℕ)
256255ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑁 ∈ ℕ)
257256nnred 11649 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑁 ∈ ℝ)
258 1red 10640 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 1 ∈ ℝ)
259233, 257, 258ltsubadd2d 11236 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (((𝑄 / 2) − 𝑁) < 1 ↔ (𝑄 / 2) < (𝑁 + 1)))
260254, 259mpbid 235 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 / 2) < (𝑁 + 1))
261 peano2re 10811 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑁 ∈ ℝ → (𝑁 + 1) ∈ ℝ)
262257, 261syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑁 + 1) ∈ ℝ)
263 lttr 10715 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑦 ∈ ℝ ∧ (𝑄 / 2) ∈ ℝ ∧ (𝑁 + 1) ∈ ℝ) → ((𝑦 < (𝑄 / 2) ∧ (𝑄 / 2) < (𝑁 + 1)) → 𝑦 < (𝑁 + 1)))
264208, 233, 262, 263syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 < (𝑄 / 2) ∧ (𝑄 / 2) < (𝑁 + 1)) → 𝑦 < (𝑁 + 1)))
265260, 264mpan2d 693 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 < (𝑄 / 2) → 𝑦 < (𝑁 + 1)))
266240, 265syld 47 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) → 𝑦 < (𝑁 + 1)))
267 nnleltp1 12034 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑦𝑁𝑦 < (𝑁 + 1)))
268198, 256, 267syl2anc 587 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦𝑁𝑦 < (𝑁 + 1)))
269266, 268sylibrd 262 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) → 𝑦𝑁))
270269pm4.71rd 566 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ↔ (𝑦𝑁 ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)))))
27190, 65syldan 594 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ)
272 flge 13179 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ ∧ 𝑦 ∈ ℤ) → (𝑦 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)) ↔ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
273271, 190, 272syl2an 598 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)) ↔ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
274219, 270, 2733bitr3d 312 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦𝑁 ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢))) ↔ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
275274pm5.32da 582 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((𝑦 ∈ ℕ ∧ (𝑦𝑁 ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
276127, 275syl5bb 286 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (((𝑦 ∈ ℕ ∧ 𝑦𝑁) ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
277276adantr 484 . . . . . . . . . . . . . . . 16 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (((𝑦 ∈ ℕ ∧ 𝑦𝑁) ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
278 simpr 488 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → 𝑥 = (2 · 𝑢))
279 nnuz 12278 . . . . . . . . . . . . . . . . . . . . . . . 24 ℕ = (ℤ‘1)
280113, 279eleqtrdi 2926 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (2 · 𝑢) ∈ (ℤ‘1))
28124adantr 484 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑀 ∈ ℤ)
282 elfz5 12903 . . . . . . . . . . . . . . . . . . . . . . 23 (((2 · 𝑢) ∈ (ℤ‘1) ∧ 𝑀 ∈ ℤ) → ((2 · 𝑢) ∈ (1...𝑀) ↔ (2 · 𝑢) ≤ 𝑀))
283280, 281, 282syl2anc 587 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((2 · 𝑢) ∈ (1...𝑀) ↔ (2 · 𝑢) ≤ 𝑀))
284152, 283mpbird 260 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (2 · 𝑢) ∈ (1...𝑀))
285284adantr 484 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (2 · 𝑢) ∈ (1...𝑀))
286278, 285eqeltrd 2916 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → 𝑥 ∈ (1...𝑀))
287286biantrurd 536 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (𝑦 ∈ (1...𝑁) ↔ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))))
288255nnzd 12083 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑁 ∈ ℤ)
289288ad2antrr 725 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → 𝑁 ∈ ℤ)
290 fznn 12979 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ ℤ → (𝑦 ∈ (1...𝑁) ↔ (𝑦 ∈ ℕ ∧ 𝑦𝑁)))
291289, 290syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (𝑦 ∈ (1...𝑁) ↔ (𝑦 ∈ ℕ ∧ 𝑦𝑁)))
292287, 291bitr3d 284 . . . . . . . . . . . . . . . . 17 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ↔ (𝑦 ∈ ℕ ∧ 𝑦𝑁)))
293 oveq1 7156 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (2 · 𝑢) → (𝑥 · 𝑄) = ((2 · 𝑢) · 𝑄))
294113nncnd 11650 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (2 · 𝑢) ∈ ℂ)
295201nncnd 11650 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑄 ∈ ℂ)
296294, 295mulcomd 10660 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((2 · 𝑢) · 𝑄) = (𝑄 · (2 · 𝑢)))
297293, 296sylan9eqr 2881 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (𝑥 · 𝑄) = (𝑄 · (2 · 𝑢)))
298297breq2d 5064 . . . . . . . . . . . . . . . . 17 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → ((𝑦 · 𝑃) < (𝑥 · 𝑄) ↔ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢))))
299292, 298anbi12d 633 . . . . . . . . . . . . . . . 16 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)) ↔ ((𝑦 ∈ ℕ ∧ 𝑦𝑁) ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)))))
300271flcld 13172 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ)
301 fznn 12979 . . . . . . . . . . . . . . . . . 18 ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ → (𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
302300, 301syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
303302adantr 484 . . . . . . . . . . . . . . . 16 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
304277, 299, 3033bitr4d 314 . . . . . . . . . . . . . . 15 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)) ↔ 𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
305126, 304syl5bb 286 . . . . . . . . . . . . . 14 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (⟨𝑥, 𝑦⟩ ∈ 𝑆𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
306305pm5.32da 582 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((𝑥 = (2 · 𝑢) ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑆) ↔ (𝑥 = (2 · 𝑢) ∧ 𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
307 vex 3483 . . . . . . . . . . . . . . . . . 18 𝑥 ∈ V
308 vex 3483 . . . . . . . . . . . . . . . . . 18 𝑦 ∈ V
309307, 308op1std 7694 . . . . . . . . . . . . . . . . 17 (𝑧 = ⟨𝑥, 𝑦⟩ → (1st𝑧) = 𝑥)
310309eqeq2d 2835 . . . . . . . . . . . . . . . 16 (𝑧 = ⟨𝑥, 𝑦⟩ → ((2 · 𝑢) = (1st𝑧) ↔ (2 · 𝑢) = 𝑥))
311 eqcom 2831 . . . . . . . . . . . . . . . 16 ((2 · 𝑢) = 𝑥𝑥 = (2 · 𝑢))
312310, 311syl6bb 290 . . . . . . . . . . . . . . 15 (𝑧 = ⟨𝑥, 𝑦⟩ → ((2 · 𝑢) = (1st𝑧) ↔ 𝑥 = (2 · 𝑢)))
313312elrab 3666 . . . . . . . . . . . . . 14 (⟨𝑥, 𝑦⟩ ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} ↔ (⟨𝑥, 𝑦⟩ ∈ 𝑆𝑥 = (2 · 𝑢)))
314313biancomi 466 . . . . . . . . . . . . 13 (⟨𝑥, 𝑦⟩ ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} ↔ (𝑥 = (2 · 𝑢) ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑆))
315 opelxp 5578 . . . . . . . . . . . . . 14 (⟨𝑥, 𝑦⟩ ∈ ({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ↔ (𝑥 ∈ {(2 · 𝑢)} ∧ 𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
316 velsn 4566 . . . . . . . . . . . . . . 15 (𝑥 ∈ {(2 · 𝑢)} ↔ 𝑥 = (2 · 𝑢))
317316anbi1i 626 . . . . . . . . . . . . . 14 ((𝑥 ∈ {(2 · 𝑢)} ∧ 𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ↔ (𝑥 = (2 · 𝑢) ∧ 𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
318315, 317bitri 278 . . . . . . . . . . . . 13 (⟨𝑥, 𝑦⟩ ∈ ({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ↔ (𝑥 = (2 · 𝑢) ∧ 𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
319306, 314, 3183bitr4g 317 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (⟨𝑥, 𝑦⟩ ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} ↔ ⟨𝑥, 𝑦⟩ ∈ ({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
320122, 123, 319eqrelrdv 5652 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} = ({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
321320eqcomd 2830 . . . . . . . . . 10 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)})
322321fveq2d 6665 . . . . . . . . 9 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (♯‘({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) = (♯‘{𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)}))
323 hashfz1 13711 . . . . . . . . . 10 ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℕ0 → (♯‘(1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))
32491, 323syl 17 . . . . . . . . 9 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (♯‘(1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))
325118, 322, 3243eqtr3rd 2868 . . . . . . . 8 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = (♯‘{𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)}))
326325sumeq2dv 15060 . . . . . . 7 (𝜑 → Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(♯‘{𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)}))
327101adantr 484 . . . . . . . . 9 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑆 ∈ Fin)
328 ssfi 8735 . . . . . . . . 9 ((𝑆 ∈ Fin ∧ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} ⊆ 𝑆) → {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} ∈ Fin)
329327, 119, 328sylancl 589 . . . . . . . 8 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} ∈ Fin)
330 fveq2 6661 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑣 → (1st𝑧) = (1st𝑣))
331330eqeq2d 2835 . . . . . . . . . . . . . . 15 (𝑧 = 𝑣 → ((2 · 𝑢) = (1st𝑧) ↔ (2 · 𝑢) = (1st𝑣)))
332331elrab 3666 . . . . . . . . . . . . . 14 (𝑣 ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} ↔ (𝑣𝑆 ∧ (2 · 𝑢) = (1st𝑣)))
333332simprbi 500 . . . . . . . . . . . . 13 (𝑣 ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} → (2 · 𝑢) = (1st𝑣))
334333ad2antll 728 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)})) → (2 · 𝑢) = (1st𝑣))
335334oveq1d 7164 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)})) → ((2 · 𝑢) / 2) = ((1st𝑣) / 2))
336144nncnd 11650 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ∈ ℂ)
337336adantrr 716 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)})) → 𝑢 ∈ ℂ)
338 2cnd 11712 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)})) → 2 ∈ ℂ)
339226a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)})) → 2 ≠ 0)
340337, 338, 339divcan3d 11419 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)})) → ((2 · 𝑢) / 2) = 𝑢)
341335, 340eqtr3d 2861 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)})) → ((1st𝑣) / 2) = 𝑢)
342341ralrimivva 3186 . . . . . . . . 9 (𝜑 → ∀𝑢 ∈ (1...(⌊‘(𝑀 / 2)))∀𝑣 ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} ((1st𝑣) / 2) = 𝑢)
343 invdisj 5036 . . . . . . . . 9 (∀𝑢 ∈ (1...(⌊‘(𝑀 / 2)))∀𝑣 ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} ((1st𝑣) / 2) = 𝑢Disj 𝑢 ∈ (1...(⌊‘(𝑀 / 2))){𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)})
344342, 343syl 17 . . . . . . . 8 (𝜑Disj 𝑢 ∈ (1...(⌊‘(𝑀 / 2))){𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)})
34587, 329, 344hashiun 15177 . . . . . . 7 (𝜑 → (♯‘ 𝑢 ∈ (1...(⌊‘(𝑀 / 2))){𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)}) = Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(♯‘{𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)}))
346 iunrab 4962 . . . . . . . . 9 𝑢 ∈ (1...(⌊‘(𝑀 / 2))){𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} = {𝑧𝑆 ∣ ∃𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(2 · 𝑢) = (1st𝑧)}
347 2cn 11709 . . . . . . . . . . . . . 14 2 ∈ ℂ
348 zcn 11983 . . . . . . . . . . . . . . 15 (𝑢 ∈ ℤ → 𝑢 ∈ ℂ)
349348adantl 485 . . . . . . . . . . . . . 14 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ ℤ) → 𝑢 ∈ ℂ)
350 mulcom 10621 . . . . . . . . . . . . . 14 ((2 ∈ ℂ ∧ 𝑢 ∈ ℂ) → (2 · 𝑢) = (𝑢 · 2))
351347, 349, 350sylancr 590 . . . . . . . . . . . . 13 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ ℤ) → (2 · 𝑢) = (𝑢 · 2))
352351eqeq1d 2826 . . . . . . . . . . . 12 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ ℤ) → ((2 · 𝑢) = (1st𝑧) ↔ (𝑢 · 2) = (1st𝑧)))
353352rexbidva 3288 . . . . . . . . . . 11 ((𝜑𝑧𝑆) → (∃𝑢 ∈ ℤ (2 · 𝑢) = (1st𝑧) ↔ ∃𝑢 ∈ ℤ (𝑢 · 2) = (1st𝑧)))
354138anim1i 617 . . . . . . . . . . . . 13 ((𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ (2 · 𝑢) = (1st𝑧)) → (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧)))
355354reximi2 3238 . . . . . . . . . . . 12 (∃𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(2 · 𝑢) = (1st𝑧) → ∃𝑢 ∈ ℤ (2 · 𝑢) = (1st𝑧))
356 simprr 772 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (2 · 𝑢) = (1st𝑧))
357 simpr 488 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑧𝑆) → 𝑧𝑆)
35899, 357sseldi 3951 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑧𝑆) → 𝑧 ∈ ((1...𝑀) × (1...𝑁)))
359 xp1st 7716 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ ((1...𝑀) × (1...𝑁)) → (1st𝑧) ∈ (1...𝑀))
360358, 359syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑧𝑆) → (1st𝑧) ∈ (1...𝑀))
361360adantr 484 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (1st𝑧) ∈ (1...𝑀))
362 elfzle2 12915 . . . . . . . . . . . . . . . . . . . 20 ((1st𝑧) ∈ (1...𝑀) → (1st𝑧) ≤ 𝑀)
363361, 362syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (1st𝑧) ≤ 𝑀)
364356, 363eqbrtrd 5074 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (2 · 𝑢) ≤ 𝑀)
365 zre 11982 . . . . . . . . . . . . . . . . . . . 20 (𝑢 ∈ ℤ → 𝑢 ∈ ℝ)
366365ad2antrl 727 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 𝑢 ∈ ℝ)
3679ad2antrr 725 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 𝑀 ∈ ℝ)
368146a1i 11 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 2 ∈ ℝ)
369148a1i 11 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 0 < 2)
370366, 367, 368, 369, 150syl112anc 1371 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → ((2 · 𝑢) ≤ 𝑀𝑢 ≤ (𝑀 / 2)))
371364, 370mpbid 235 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 𝑢 ≤ (𝑀 / 2))
37210ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (𝑀 / 2) ∈ ℝ)
373 simprl 770 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 𝑢 ∈ ℤ)
374372, 373, 140syl2anc 587 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (𝑢 ≤ (𝑀 / 2) ↔ 𝑢 ≤ (⌊‘(𝑀 / 2))))
375371, 374mpbid 235 . . . . . . . . . . . . . . . 16 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 𝑢 ≤ (⌊‘(𝑀 / 2)))
376 2t0e0 11803 . . . . . . . . . . . . . . . . . . . . 21 (2 · 0) = 0
377 elfznn 12940 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1st𝑧) ∈ (1...𝑀) → (1st𝑧) ∈ ℕ)
378361, 377syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (1st𝑧) ∈ ℕ)
379356, 378eqeltrd 2916 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (2 · 𝑢) ∈ ℕ)
380379nngt0d 11683 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 0 < (2 · 𝑢))
381376, 380eqbrtrid 5087 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (2 · 0) < (2 · 𝑢))
382 0red 10642 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 0 ∈ ℝ)
383 ltmul2 11489 . . . . . . . . . . . . . . . . . . . . 21 ((0 ∈ ℝ ∧ 𝑢 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (0 < 𝑢 ↔ (2 · 0) < (2 · 𝑢)))
384382, 366, 368, 369, 383syl112anc 1371 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (0 < 𝑢 ↔ (2 · 0) < (2 · 𝑢)))
385381, 384mpbird 260 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 0 < 𝑢)
386 elnnz 11988 . . . . . . . . . . . . . . . . . . 19 (𝑢 ∈ ℕ ↔ (𝑢 ∈ ℤ ∧ 0 < 𝑢))
387373, 385, 386sylanbrc 586 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 𝑢 ∈ ℕ)
388387, 279eleqtrdi 2926 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 𝑢 ∈ (ℤ‘1))
38911ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (⌊‘(𝑀 / 2)) ∈ ℤ)
390 elfz5 12903 . . . . . . . . . . . . . . . . 17 ((𝑢 ∈ (ℤ‘1) ∧ (⌊‘(𝑀 / 2)) ∈ ℤ) → (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ↔ 𝑢 ≤ (⌊‘(𝑀 / 2))))
391388, 389, 390syl2anc 587 . . . . . . . . . . . . . . . 16 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ↔ 𝑢 ≤ (⌊‘(𝑀 / 2))))
392375, 391mpbird 260 . . . . . . . . . . . . . . 15 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 𝑢 ∈ (1...(⌊‘(𝑀 / 2))))
393392, 356jca 515 . . . . . . . . . . . . . 14 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ (2 · 𝑢) = (1st𝑧)))
394393ex 416 . . . . . . . . . . . . 13 ((𝜑𝑧𝑆) → ((𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧)) → (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ (2 · 𝑢) = (1st𝑧))))
395394reximdv2 3263 . . . . . . . . . . . 12 ((𝜑𝑧𝑆) → (∃𝑢 ∈ ℤ (2 · 𝑢) = (1st𝑧) → ∃𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(2 · 𝑢) = (1st𝑧)))
396355, 395impbid2 229 . . . . . . . . . . 11 ((𝜑𝑧𝑆) → (∃𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(2 · 𝑢) = (1st𝑧) ↔ ∃𝑢 ∈ ℤ (2 · 𝑢) = (1st𝑧)))
397 2z 12011 . . . . . . . . . . . 12 2 ∈ ℤ
398 elfzelz 12911 . . . . . . . . . . . . 13 ((1st𝑧) ∈ (1...𝑀) → (1st𝑧) ∈ ℤ)
399360, 398syl 17 . . . . . . . . . . . 12 ((𝜑𝑧𝑆) → (1st𝑧) ∈ ℤ)
400 divides 15609 . . . . . . . . . . . 12 ((2 ∈ ℤ ∧ (1st𝑧) ∈ ℤ) → (2 ∥ (1st𝑧) ↔ ∃𝑢 ∈ ℤ (𝑢 · 2) = (1st𝑧)))
401397, 399, 400sylancr 590 . . . . . . . . . . 11 ((𝜑𝑧𝑆) → (2 ∥ (1st𝑧) ↔ ∃𝑢 ∈ ℤ (𝑢 · 2) = (1st𝑧)))
402353, 396, 4013bitr4d 314 . . . . . . . . . 10 ((𝜑𝑧𝑆) → (∃𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(2 · 𝑢) = (1st𝑧) ↔ 2 ∥ (1st𝑧)))
403402rabbidva 3463 . . . . . . . . 9 (𝜑 → {𝑧𝑆 ∣ ∃𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(2 · 𝑢) = (1st𝑧)} = {𝑧𝑆 ∣ 2 ∥ (1st𝑧)})
404346, 403syl5eq 2871 . . . . . . . 8 (𝜑 𝑢 ∈ (1...(⌊‘(𝑀 / 2))){𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} = {𝑧𝑆 ∣ 2 ∥ (1st𝑧)})
405404fveq2d 6665 . . . . . . 7 (𝜑 → (♯‘ 𝑢 ∈ (1...(⌊‘(𝑀 / 2))){𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)}) = (♯‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)}))
406326, 345, 4053eqtr2d 2865 . . . . . 6 (𝜑 → Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = (♯‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)}))
407406oveq2d 7165 . . . . 5 (𝜑 → (-1↑Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (-1↑(♯‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)})))
4081, 2, 3, 5, 245, 97lgsquadlem1 25967 . . . . 5 (𝜑 → (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})))
409407, 408oveq12d 7167 . . . 4 (𝜑 → ((-1↑Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) · (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = ((-1↑(♯‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)})) · (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))))
410112, 409eqtr4d 2862 . . 3 (𝜑 → (-1↑((♯‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)}) + (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))) = ((-1↑Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) · (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
411 unrab 4259 . . . . . . 7 ({𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∪ {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) = {𝑧𝑆 ∣ (2 ∥ (1st𝑧) ∨ ¬ 2 ∥ (1st𝑧))}
412 exmid 892 . . . . . . . . 9 (2 ∥ (1st𝑧) ∨ ¬ 2 ∥ (1st𝑧))
413412rgenw 3145 . . . . . . . 8 𝑧𝑆 (2 ∥ (1st𝑧) ∨ ¬ 2 ∥ (1st𝑧))
414 rabid2 3372 . . . . . . . 8 (𝑆 = {𝑧𝑆 ∣ (2 ∥ (1st𝑧) ∨ ¬ 2 ∥ (1st𝑧))} ↔ ∀𝑧𝑆 (2 ∥ (1st𝑧) ∨ ¬ 2 ∥ (1st𝑧)))
415413, 414mpbir 234 . . . . . . 7 𝑆 = {𝑧𝑆 ∣ (2 ∥ (1st𝑧) ∨ ¬ 2 ∥ (1st𝑧))}
416411, 415eqtr4i 2850 . . . . . 6 ({𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∪ {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) = 𝑆
417416fveq2i 6664 . . . . 5 (♯‘({𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∪ {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) = (♯‘𝑆)
418 inrab 4260 . . . . . . 7 ({𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∩ {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) = {𝑧𝑆 ∣ (2 ∥ (1st𝑧) ∧ ¬ 2 ∥ (1st𝑧))}
419 pm3.24 406 . . . . . . . . . 10 ¬ (2 ∥ (1st𝑧) ∧ ¬ 2 ∥ (1st𝑧))
420419a1i 11 . . . . . . . . 9 (𝜑 → ¬ (2 ∥ (1st𝑧) ∧ ¬ 2 ∥ (1st𝑧)))
421420ralrimivw 3178 . . . . . . . 8 (𝜑 → ∀𝑧𝑆 ¬ (2 ∥ (1st𝑧) ∧ ¬ 2 ∥ (1st𝑧)))
422 rabeq0 4321 . . . . . . . 8 ({𝑧𝑆 ∣ (2 ∥ (1st𝑧) ∧ ¬ 2 ∥ (1st𝑧))} = ∅ ↔ ∀𝑧𝑆 ¬ (2 ∥ (1st𝑧) ∧ ¬ 2 ∥ (1st𝑧)))
423421, 422sylibr 237 . . . . . . 7 (𝜑 → {𝑧𝑆 ∣ (2 ∥ (1st𝑧) ∧ ¬ 2 ∥ (1st𝑧))} = ∅)
424418, 423syl5eq 2871 . . . . . 6 (𝜑 → ({𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∩ {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) = ∅)
425 hashun 13748 . . . . . 6 (({𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∈ Fin ∧ {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)} ∈ Fin ∧ ({𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∩ {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) = ∅) → (♯‘({𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∪ {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) = ((♯‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)}) + (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})))
426109, 104, 424, 425syl3anc 1368 . . . . 5 (𝜑 → (♯‘({𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∪ {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) = ((♯‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)}) + (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})))
427417, 426syl5reqr 2874 . . . 4 (𝜑 → ((♯‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)}) + (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) = (♯‘𝑆))
428427oveq2d 7165 . . 3 (𝜑 → (-1↑((♯‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)}) + (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))) = (-1↑(♯‘𝑆)))
42993, 410, 4283eqtr2d 2865 . 2 (𝜑 → (-1↑(Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = (-1↑(♯‘𝑆)))
4304, 78, 4293eqtrd 2863 1 (𝜑 → (𝑄 /L 𝑃) = (-1↑(♯‘𝑆)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wo 844  w3a 1084   = wceq 1538  wcel 2115  wne 3014  wral 3133  wrex 3134  {crab 3137  cdif 3916  cun 3917  cin 3918  wss 3919  c0 4276  {csn 4550  cop 4556   ciun 4905  Disj wdisj 5017   class class class wbr 5052  {copab 5114   × cxp 5540  Rel wrel 5547  cfv 6343  (class class class)co 7149  1st c1st 7682  cen 8502  Fincfn 8505  cc 10533  cr 10534  0cc0 10535  1c1 10536   + caddc 10538   · cmul 10540   < clt 10673  cle 10674  cmin 10868  -cneg 10869   / cdiv 11295  cn 11634  2c2 11689  0cn0 11894  cz 11978  cuz 12240  +crp 12386  ...cfz 12894  cfl 13164  cexp 13434  chash 13695  Σcsu 15042  cdvds 15607   gcd cgcd 15841  cprime 16013   /L clgs 25881
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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5176  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317  ax-un 7455  ax-inf2 9101  ax-cnex 10591  ax-resscn 10592  ax-1cn 10593  ax-icn 10594  ax-addcl 10595  ax-addrcl 10596  ax-mulcl 10597  ax-mulrcl 10598  ax-mulcom 10599  ax-addass 10600  ax-mulass 10601  ax-distr 10602  ax-i2m1 10603  ax-1ne0 10604  ax-1rid 10605  ax-rnegex 10606  ax-rrecex 10607  ax-cnre 10608  ax-pre-lttri 10609  ax-pre-lttrn 10610  ax-pre-ltadd 10611  ax-pre-mulgt0 10612  ax-pre-sup 10613  ax-addf 10614  ax-mulf 10615
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-nel 3119  df-ral 3138  df-rex 3139  df-reu 3140  df-rmo 3141  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-pss 3938  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-tp 4555  df-op 4557  df-uni 4825  df-int 4863  df-iun 4907  df-disj 5018  df-br 5053  df-opab 5115  df-mpt 5133  df-tr 5159  df-id 5447  df-eprel 5452  df-po 5461  df-so 5462  df-fr 5501  df-se 5502  df-we 5503  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-pred 6135  df-ord 6181  df-on 6182  df-lim 6183  df-suc 6184  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-f1 6348  df-fo 6349  df-f1o 6350  df-fv 6351  df-isom 6352  df-riota 7107  df-ov 7152  df-oprab 7153  df-mpo 7154  df-of 7403  df-om 7575  df-1st 7684  df-2nd 7685  df-supp 7827  df-tpos 7888  df-wrecs 7943  df-recs 8004  df-rdg 8042  df-1o 8098  df-2o 8099  df-oadd 8102  df-er 8285  df-ec 8287  df-qs 8291  df-map 8404  df-en 8506  df-dom 8507  df-sdom 8508  df-fin 8509  df-fsupp 8831  df-sup 8903  df-inf 8904  df-oi 8971  df-dju 9327  df-card 9365  df-pnf 10675  df-mnf 10676  df-xr 10677  df-ltxr 10678  df-le 10679  df-sub 10870  df-neg 10871  df-div 11296  df-nn 11635  df-2 11697  df-3 11698  df-4 11699  df-5 11700  df-6 11701  df-7 11702  df-8 11703  df-9 11704  df-n0 11895  df-xnn0 11965  df-z 11979  df-dec 12096  df-uz 12241  df-q 12346  df-rp 12387  df-fz 12895  df-fzo 13038  df-fl 13166  df-mod 13242  df-seq 13374  df-exp 13435  df-hash 13696  df-cj 14458  df-re 14459  df-im 14460  df-sqrt 14594  df-abs 14595  df-clim 14845  df-sum 15043  df-dvds 15608  df-gcd 15842  df-prm 16014  df-phi 16101  df-pc 16172  df-struct 16485  df-ndx 16486  df-slot 16487  df-base 16489  df-sets 16490  df-ress 16491  df-plusg 16578  df-mulr 16579  df-starv 16580  df-sca 16581  df-vsca 16582  df-ip 16583  df-tset 16584  df-ple 16585  df-ds 16587  df-unif 16588  df-0g 16715  df-gsum 16716  df-imas 16781  df-qus 16782  df-mgm 17852  df-sgrp 17901  df-mnd 17912  df-mhm 17956  df-submnd 17957  df-grp 18106  df-minusg 18107  df-sbg 18108  df-mulg 18225  df-subg 18276  df-nsg 18277  df-eqg 18278  df-ghm 18356  df-cntz 18447  df-cmn 18908  df-abl 18909  df-mgp 19240  df-ur 19252  df-ring 19299  df-cring 19300  df-oppr 19376  df-dvdsr 19394  df-unit 19395  df-invr 19425  df-dvr 19436  df-rnghom 19470  df-drng 19504  df-field 19505  df-subrg 19533  df-lmod 19636  df-lss 19704  df-lsp 19744  df-sra 19944  df-rgmod 19945  df-lidl 19946  df-rsp 19947  df-2idl 20005  df-nzr 20031  df-rlreg 20056  df-domn 20057  df-idom 20058  df-cnfld 20546  df-zring 20618  df-zrh 20651  df-zn 20654  df-lgs 25882
This theorem is referenced by:  lgsquadlem3  25969
  Copyright terms: Public domain W3C validator