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

Theorem lgsquadlem2 26729
Description: Lemma for lgsquad 26731. Count the members of 𝑆 with even coordinates, and combine with lgsquadlem1 26728 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 26727 . 2 (𝜑 → (𝑄 /L 𝑃) = (-1↑Σ𝑢 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
5 lgsquad.4 . . . . . 6 𝑀 = ((𝑃 − 1) / 2)
65oveq2i 7368 . . . . 5 (1...𝑀) = (1...((𝑃 − 1) / 2))
76sumeq1i 15583 . . . 4 Σ𝑢 ∈ (1...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = Σ𝑢 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))
81, 5gausslemma2dlem0b 26705 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℕ)
98nnred 12168 . . . . . . . . . 10 (𝜑𝑀 ∈ ℝ)
109rehalfcld 12400 . . . . . . . . 9 (𝜑 → (𝑀 / 2) ∈ ℝ)
1110flcld 13703 . . . . . . . 8 (𝜑 → (⌊‘(𝑀 / 2)) ∈ ℤ)
1211zred 12607 . . . . . . 7 (𝜑 → (⌊‘(𝑀 / 2)) ∈ ℝ)
1312ltp1d 12085 . . . . . 6 (𝜑 → (⌊‘(𝑀 / 2)) < ((⌊‘(𝑀 / 2)) + 1))
14 fzdisj 13468 . . . . . 6 ((⌊‘(𝑀 / 2)) < ((⌊‘(𝑀 / 2)) + 1) → ((1...(⌊‘(𝑀 / 2))) ∩ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) = ∅)
1513, 14syl 17 . . . . 5 (𝜑 → ((1...(⌊‘(𝑀 / 2))) ∩ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) = ∅)
168nnrpd 12955 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℝ+)
1716rphalfcld 12969 . . . . . . . . . 10 (𝜑 → (𝑀 / 2) ∈ ℝ+)
1817rpge0d 12961 . . . . . . . . 9 (𝜑 → 0 ≤ (𝑀 / 2))
19 flge0nn0 13725 . . . . . . . . 9 (((𝑀 / 2) ∈ ℝ ∧ 0 ≤ (𝑀 / 2)) → (⌊‘(𝑀 / 2)) ∈ ℕ0)
2010, 18, 19syl2anc 584 . . . . . . . 8 (𝜑 → (⌊‘(𝑀 / 2)) ∈ ℕ0)
218nnnn0d 12473 . . . . . . . 8 (𝜑𝑀 ∈ ℕ0)
22 rphalflt 12944 . . . . . . . . . . 11 (𝑀 ∈ ℝ+ → (𝑀 / 2) < 𝑀)
2316, 22syl 17 . . . . . . . . . 10 (𝜑 → (𝑀 / 2) < 𝑀)
248nnzd 12526 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℤ)
25 fllt 13711 . . . . . . . . . . 11 (((𝑀 / 2) ∈ ℝ ∧ 𝑀 ∈ ℤ) → ((𝑀 / 2) < 𝑀 ↔ (⌊‘(𝑀 / 2)) < 𝑀))
2610, 24, 25syl2anc 584 . . . . . . . . . 10 (𝜑 → ((𝑀 / 2) < 𝑀 ↔ (⌊‘(𝑀 / 2)) < 𝑀))
2723, 26mpbid 231 . . . . . . . . 9 (𝜑 → (⌊‘(𝑀 / 2)) < 𝑀)
2812, 9, 27ltled 11303 . . . . . . . 8 (𝜑 → (⌊‘(𝑀 / 2)) ≤ 𝑀)
29 elfz2nn0 13532 . . . . . . . 8 ((⌊‘(𝑀 / 2)) ∈ (0...𝑀) ↔ ((⌊‘(𝑀 / 2)) ∈ ℕ0𝑀 ∈ ℕ0 ∧ (⌊‘(𝑀 / 2)) ≤ 𝑀))
3020, 21, 28, 29syl3anbrc 1343 . . . . . . 7 (𝜑 → (⌊‘(𝑀 / 2)) ∈ (0...𝑀))
31 nn0uz 12805 . . . . . . . . 9 0 = (ℤ‘0)
3221, 31eleqtrdi 2848 . . . . . . . 8 (𝜑𝑀 ∈ (ℤ‘0))
33 elfzp12 13520 . . . . . . . 8 (𝑀 ∈ (ℤ‘0) → ((⌊‘(𝑀 / 2)) ∈ (0...𝑀) ↔ ((⌊‘(𝑀 / 2)) = 0 ∨ (⌊‘(𝑀 / 2)) ∈ ((0 + 1)...𝑀))))
3432, 33syl 17 . . . . . . 7 (𝜑 → ((⌊‘(𝑀 / 2)) ∈ (0...𝑀) ↔ ((⌊‘(𝑀 / 2)) = 0 ∨ (⌊‘(𝑀 / 2)) ∈ ((0 + 1)...𝑀))))
3530, 34mpbid 231 . . . . . 6 (𝜑 → ((⌊‘(𝑀 / 2)) = 0 ∨ (⌊‘(𝑀 / 2)) ∈ ((0 + 1)...𝑀)))
36 un0 4350 . . . . . . . . 9 ((1...𝑀) ∪ ∅) = (1...𝑀)
37 uncom 4113 . . . . . . . . 9 ((1...𝑀) ∪ ∅) = (∅ ∪ (1...𝑀))
3836, 37eqtr3i 2766 . . . . . . . 8 (1...𝑀) = (∅ ∪ (1...𝑀))
39 oveq2 7365 . . . . . . . . . 10 ((⌊‘(𝑀 / 2)) = 0 → (1...(⌊‘(𝑀 / 2))) = (1...0))
40 fz10 13462 . . . . . . . . . 10 (1...0) = ∅
4139, 40eqtrdi 2792 . . . . . . . . 9 ((⌊‘(𝑀 / 2)) = 0 → (1...(⌊‘(𝑀 / 2))) = ∅)
42 oveq1 7364 . . . . . . . . . . 11 ((⌊‘(𝑀 / 2)) = 0 → ((⌊‘(𝑀 / 2)) + 1) = (0 + 1))
43 0p1e1 12275 . . . . . . . . . . 11 (0 + 1) = 1
4442, 43eqtrdi 2792 . . . . . . . . . 10 ((⌊‘(𝑀 / 2)) = 0 → ((⌊‘(𝑀 / 2)) + 1) = 1)
4544oveq1d 7372 . . . . . . . . 9 ((⌊‘(𝑀 / 2)) = 0 → (((⌊‘(𝑀 / 2)) + 1)...𝑀) = (1...𝑀))
4641, 45uneq12d 4124 . . . . . . . 8 ((⌊‘(𝑀 / 2)) = 0 → ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) = (∅ ∪ (1...𝑀)))
4738, 46eqtr4id 2795 . . . . . . 7 ((⌊‘(𝑀 / 2)) = 0 → (1...𝑀) = ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀)))
48 fzsplit 13467 . . . . . . . 8 ((⌊‘(𝑀 / 2)) ∈ (1...𝑀) → (1...𝑀) = ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀)))
4943oveq1i 7367 . . . . . . . 8 ((0 + 1)...𝑀) = (1...𝑀)
5048, 49eleq2s 2856 . . . . . . 7 ((⌊‘(𝑀 / 2)) ∈ ((0 + 1)...𝑀) → (1...𝑀) = ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀)))
5147, 50jaoi 855 . . . . . 6 (((⌊‘(𝑀 / 2)) = 0 ∨ (⌊‘(𝑀 / 2)) ∈ ((0 + 1)...𝑀)) → (1...𝑀) = ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀)))
5235, 51syl 17 . . . . 5 (𝜑 → (1...𝑀) = ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀)))
53 fzfid 13878 . . . . 5 (𝜑 → (1...𝑀) ∈ Fin)
542gausslemma2dlem0a 26704 . . . . . . . . . . 11 (𝜑𝑄 ∈ ℕ)
5554nnred 12168 . . . . . . . . . 10 (𝜑𝑄 ∈ ℝ)
561gausslemma2dlem0a 26704 . . . . . . . . . 10 (𝜑𝑃 ∈ ℕ)
5755, 56nndivred 12207 . . . . . . . . 9 (𝜑 → (𝑄 / 𝑃) ∈ ℝ)
5857adantr 481 . . . . . . . 8 ((𝜑𝑢 ∈ (1...𝑀)) → (𝑄 / 𝑃) ∈ ℝ)
59 2nn 12226 . . . . . . . . . 10 2 ∈ ℕ
60 elfznn 13470 . . . . . . . . . . 11 (𝑢 ∈ (1...𝑀) → 𝑢 ∈ ℕ)
6160adantl 482 . . . . . . . . . 10 ((𝜑𝑢 ∈ (1...𝑀)) → 𝑢 ∈ ℕ)
62 nnmulcl 12177 . . . . . . . . . 10 ((2 ∈ ℕ ∧ 𝑢 ∈ ℕ) → (2 · 𝑢) ∈ ℕ)
6359, 61, 62sylancr 587 . . . . . . . . 9 ((𝜑𝑢 ∈ (1...𝑀)) → (2 · 𝑢) ∈ ℕ)
6463nnred 12168 . . . . . . . 8 ((𝜑𝑢 ∈ (1...𝑀)) → (2 · 𝑢) ∈ ℝ)
6558, 64remulcld 11185 . . . . . . 7 ((𝜑𝑢 ∈ (1...𝑀)) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ)
6654nnrpd 12955 . . . . . . . . . . 11 (𝜑𝑄 ∈ ℝ+)
6756nnrpd 12955 . . . . . . . . . . 11 (𝜑𝑃 ∈ ℝ+)
6866, 67rpdivcld 12974 . . . . . . . . . 10 (𝜑 → (𝑄 / 𝑃) ∈ ℝ+)
6968adantr 481 . . . . . . . . 9 ((𝜑𝑢 ∈ (1...𝑀)) → (𝑄 / 𝑃) ∈ ℝ+)
7063nnrpd 12955 . . . . . . . . 9 ((𝜑𝑢 ∈ (1...𝑀)) → (2 · 𝑢) ∈ ℝ+)
7169, 70rpmulcld 12973 . . . . . . . 8 ((𝜑𝑢 ∈ (1...𝑀)) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ+)
7271rpge0d 12961 . . . . . . 7 ((𝜑𝑢 ∈ (1...𝑀)) → 0 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)))
73 flge0nn0 13725 . . . . . . 7 ((((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ ∧ 0 ≤ ((𝑄 / 𝑃) · (2 · 𝑢))) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℕ0)
7465, 72, 73syl2anc 584 . . . . . 6 ((𝜑𝑢 ∈ (1...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℕ0)
7574nn0cnd 12475 . . . . 5 ((𝜑𝑢 ∈ (1...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℂ)
7615, 52, 53, 75fsumsplit 15626 . . . 4 (𝜑 → Σ𝑢 ∈ (1...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = (Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
777, 76eqtr3id 2790 . . 3 (𝜑 → Σ𝑢 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = (Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
7877oveq2d 7373 . 2 (𝜑 → (-1↑Σ𝑢 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (-1↑(Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
79 neg1cn 12267 . . . . 5 -1 ∈ ℂ
8079a1i 11 . . . 4 (𝜑 → -1 ∈ ℂ)
81 fzfid 13878 . . . . 5 (𝜑 → (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∈ Fin)
82 ssun2 4133 . . . . . . . 8 (((⌊‘(𝑀 / 2)) + 1)...𝑀) ⊆ ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀))
8382, 52sseqtrrid 3997 . . . . . . 7 (𝜑 → (((⌊‘(𝑀 / 2)) + 1)...𝑀) ⊆ (1...𝑀))
8483sselda 3944 . . . . . 6 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ∈ (1...𝑀))
8584, 74syldan 591 . . . . 5 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℕ0)
8681, 85fsumnn0cl 15621 . . . 4 (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℕ0)
87 fzfid 13878 . . . . 5 (𝜑 → (1...(⌊‘(𝑀 / 2))) ∈ Fin)
88 ssun1 4132 . . . . . . . 8 (1...(⌊‘(𝑀 / 2))) ⊆ ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀))
8988, 52sseqtrrid 3997 . . . . . . 7 (𝜑 → (1...(⌊‘(𝑀 / 2))) ⊆ (1...𝑀))
9089sselda 3944 . . . . . 6 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ∈ (1...𝑀))
9190, 74syldan 591 . . . . 5 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℕ0)
9287, 91fsumnn0cl 15621 . . . 4 (𝜑 → Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℕ0)
9380, 86, 92expaddd 14053 . . 3 (𝜑 → (-1↑(Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = ((-1↑Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) · (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
94 fzfid 13878 . . . . . . . . 9 (𝜑 → (1...𝑁) ∈ Fin)
95 xpfi 9261 . . . . . . . . 9 (((1...𝑀) ∈ Fin ∧ (1...𝑁) ∈ Fin) → ((1...𝑀) × (1...𝑁)) ∈ Fin)
9653, 94, 95syl2anc 584 . . . . . . . 8 (𝜑 → ((1...𝑀) × (1...𝑁)) ∈ Fin)
97 lgsquad.6 . . . . . . . . 9 𝑆 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))}
98 opabssxp 5724 . . . . . . . . 9 {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} ⊆ ((1...𝑀) × (1...𝑁))
9997, 98eqsstri 3978 . . . . . . . 8 𝑆 ⊆ ((1...𝑀) × (1...𝑁))
100 ssfi 9117 . . . . . . . 8 ((((1...𝑀) × (1...𝑁)) ∈ Fin ∧ 𝑆 ⊆ ((1...𝑀) × (1...𝑁))) → 𝑆 ∈ Fin)
10196, 99, 100sylancl 586 . . . . . . 7 (𝜑𝑆 ∈ Fin)
102 ssrab2 4037 . . . . . . 7 {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)} ⊆ 𝑆
103 ssfi 9117 . . . . . . 7 ((𝑆 ∈ Fin ∧ {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)} ⊆ 𝑆) → {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)} ∈ Fin)
104101, 102, 103sylancl 586 . . . . . 6 (𝜑 → {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)} ∈ Fin)
105 hashcl 14256 . . . . . 6 ({𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)} ∈ Fin → (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) ∈ ℕ0)
106104, 105syl 17 . . . . 5 (𝜑 → (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) ∈ ℕ0)
107 ssrab2 4037 . . . . . . 7 {𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ⊆ 𝑆
108 ssfi 9117 . . . . . . 7 ((𝑆 ∈ Fin ∧ {𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ⊆ 𝑆) → {𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∈ Fin)
109101, 107, 108sylancl 586 . . . . . 6 (𝜑 → {𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∈ Fin)
110 hashcl 14256 . . . . . 6 ({𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∈ Fin → (♯‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)}) ∈ ℕ0)
111109, 110syl 17 . . . . 5 (𝜑 → (♯‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)}) ∈ ℕ0)
11280, 106, 111expaddd 14053 . . . 4 (𝜑 → (-1↑((♯‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)}) + (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))) = ((-1↑(♯‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)})) · (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))))
11390, 63syldan 591 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (2 · 𝑢) ∈ ℕ)
114 fzfid 13878 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ Fin)
115 xpsnen2g 9009 . . . . . . . . . . 11 (((2 · 𝑢) ∈ ℕ ∧ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ Fin) → ({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ≈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
116113, 114, 115syl2anc 584 . . . . . . . . . 10 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ≈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
117 hasheni 14248 . . . . . . . . . 10 (({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ≈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) → (♯‘({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) = (♯‘(1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
118116, 117syl 17 . . . . . . . . 9 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (♯‘({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) = (♯‘(1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
119 ssrab2 4037 . . . . . . . . . . . . 13 {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} ⊆ 𝑆
12097relopabiv 5776 . . . . . . . . . . . . 13 Rel 𝑆
121 relss 5737 . . . . . . . . . . . . 13 ({𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} ⊆ 𝑆 → (Rel 𝑆 → Rel {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)}))
122119, 120, 121mp2 9 . . . . . . . . . . . 12 Rel {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)}
123 relxp 5651 . . . . . . . . . . . 12 Rel ({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
12497eleq2i 2829 . . . . . . . . . . . . . . . 16 (⟨𝑥, 𝑦⟩ ∈ 𝑆 ↔ ⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))})
125 opabidw 5481 . . . . . . . . . . . . . . . 16 (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} ↔ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))
126124, 125bitri 274 . . . . . . . . . . . . . . 15 (⟨𝑥, 𝑦⟩ ∈ 𝑆 ↔ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))
127 anass 469 . . . . . . . . . . . . . . . . . 18 (((𝑦 ∈ ℕ ∧ 𝑦𝑁) ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢))) ↔ (𝑦 ∈ ℕ ∧ (𝑦𝑁 ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)))))
128113adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2 · 𝑢) ∈ ℕ)
129128nnred 12168 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2 · 𝑢) ∈ ℝ)
13056ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℕ)
131130nnred 12168 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℝ)
132131rehalfcld 12400 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 / 2) ∈ ℝ)
1339adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑀 ∈ ℝ)
134133adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑀 ∈ ℝ)
135 elfzle2 13445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) → 𝑢 ≤ (⌊‘(𝑀 / 2)))
136135adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ≤ (⌊‘(𝑀 / 2)))
137133rehalfcld 12400 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (𝑀 / 2) ∈ ℝ)
138 elfzelz 13441 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) → 𝑢 ∈ ℤ)
139138adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ∈ ℤ)
140 flge 13710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑀 / 2) ∈ ℝ ∧ 𝑢 ∈ ℤ) → (𝑢 ≤ (𝑀 / 2) ↔ 𝑢 ≤ (⌊‘(𝑀 / 2))))
141137, 139, 140syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (𝑢 ≤ (𝑀 / 2) ↔ 𝑢 ≤ (⌊‘(𝑀 / 2))))
142136, 141mpbird 256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ≤ (𝑀 / 2))
143 elfznn 13470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) → 𝑢 ∈ ℕ)
144143adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ∈ ℕ)
145144nnred 12168 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ∈ ℝ)
146 2re 12227 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 2 ∈ ℝ
147146a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 2 ∈ ℝ)
148 2pos 12256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 0 < 2
149148a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 0 < 2)
150 lemuldiv2 12036 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑢 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 𝑢) ≤ 𝑀𝑢 ≤ (𝑀 / 2)))
151145, 133, 147, 149, 150syl112anc 1374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((2 · 𝑢) ≤ 𝑀𝑢 ≤ (𝑀 / 2)))
152142, 151mpbird 256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (2 · 𝑢) ≤ 𝑀)
153152adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2 · 𝑢) ≤ 𝑀)
154131ltm1d 12087 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 − 1) < 𝑃)
155 peano2rem 11468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑃 ∈ ℝ → (𝑃 − 1) ∈ ℝ)
156131, 155syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 − 1) ∈ ℝ)
157146a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 2 ∈ ℝ)
158148a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 0 < 2)
159 ltdiv1 12019 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑃 − 1) ∈ ℝ ∧ 𝑃 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((𝑃 − 1) < 𝑃 ↔ ((𝑃 − 1) / 2) < (𝑃 / 2)))
160156, 131, 157, 158, 159syl112anc 1374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑃 − 1) < 𝑃 ↔ ((𝑃 − 1) / 2) < (𝑃 / 2)))
161154, 160mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑃 − 1) / 2) < (𝑃 / 2))
1625, 161eqbrtrid 5140 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑀 < (𝑃 / 2))
163129, 134, 132, 153, 162lelttrd 11313 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2 · 𝑢) < (𝑃 / 2))
164130nnrpd 12955 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℝ+)
165 rphalflt 12944 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑃 ∈ ℝ+ → (𝑃 / 2) < 𝑃)
166164, 165syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 / 2) < 𝑃)
167129, 132, 131, 163, 166lttrd 11316 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2 · 𝑢) < 𝑃)
168129, 131ltnled 11302 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((2 · 𝑢) < 𝑃 ↔ ¬ 𝑃 ≤ (2 · 𝑢)))
169167, 168mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ¬ 𝑃 ≤ (2 · 𝑢))
1701eldifad 3922 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝑃 ∈ ℙ)
171170ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℙ)
172 prmz 16551 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
173171, 172syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℤ)
174 dvdsle 16192 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑃 ∈ ℤ ∧ (2 · 𝑢) ∈ ℕ) → (𝑃 ∥ (2 · 𝑢) → 𝑃 ≤ (2 · 𝑢)))
175173, 128, 174syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 ∥ (2 · 𝑢) → 𝑃 ≤ (2 · 𝑢)))
176169, 175mtod 197 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ¬ 𝑃 ∥ (2 · 𝑢))
1772eldifad 3922 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝑄 ∈ ℙ)
178 prmrp 16588 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ) → ((𝑃 gcd 𝑄) = 1 ↔ 𝑃𝑄))
179170, 177, 178syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ((𝑃 gcd 𝑄) = 1 ↔ 𝑃𝑄))
1803, 179mpbird 256 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝑃 gcd 𝑄) = 1)
181180ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 gcd 𝑄) = 1)
182177ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈ ℙ)
183 prmz 16551 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑄 ∈ ℙ → 𝑄 ∈ ℤ)
184182, 183syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈ ℤ)
185128nnzd 12526 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2 · 𝑢) ∈ ℤ)
186 coprmdvds 16529 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑃 ∈ ℤ ∧ 𝑄 ∈ ℤ ∧ (2 · 𝑢) ∈ ℤ) → ((𝑃 ∥ (𝑄 · (2 · 𝑢)) ∧ (𝑃 gcd 𝑄) = 1) → 𝑃 ∥ (2 · 𝑢)))
187173, 184, 185, 186syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑃 ∥ (𝑄 · (2 · 𝑢)) ∧ (𝑃 gcd 𝑄) = 1) → 𝑃 ∥ (2 · 𝑢)))
188181, 187mpan2d 692 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 ∥ (𝑄 · (2 · 𝑢)) → 𝑃 ∥ (2 · 𝑢)))
189176, 188mtod 197 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ¬ 𝑃 ∥ (𝑄 · (2 · 𝑢)))
190 nnz 12520 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 ∈ ℕ → 𝑦 ∈ ℤ)
191190adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ ℤ)
192 dvdsmul2 16161 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑦 ∈ ℤ ∧ 𝑃 ∈ ℤ) → 𝑃 ∥ (𝑦 · 𝑃))
193191, 173, 192syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∥ (𝑦 · 𝑃))
194 breq2 5109 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑄 · (2 · 𝑢)) = (𝑦 · 𝑃) → (𝑃 ∥ (𝑄 · (2 · 𝑢)) ↔ 𝑃 ∥ (𝑦 · 𝑃)))
195193, 194syl5ibrcom 246 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 · (2 · 𝑢)) = (𝑦 · 𝑃) → 𝑃 ∥ (𝑄 · (2 · 𝑢))))
196195necon3bd 2957 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (¬ 𝑃 ∥ (𝑄 · (2 · 𝑢)) → (𝑄 · (2 · 𝑢)) ≠ (𝑦 · 𝑃)))
197189, 196mpd 15 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (2 · 𝑢)) ≠ (𝑦 · 𝑃))
198 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ ℕ)
199198, 130nnmulcld 12206 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 · 𝑃) ∈ ℕ)
200199nnred 12168 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 · 𝑃) ∈ ℝ)
20154adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑄 ∈ ℕ)
202201, 113nnmulcld 12206 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (𝑄 · (2 · 𝑢)) ∈ ℕ)
203202adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (2 · 𝑢)) ∈ ℕ)
204203nnred 12168 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (2 · 𝑢)) ∈ ℝ)
205200, 204ltlend 11300 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ↔ ((𝑦 · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ∧ (𝑄 · (2 · 𝑢)) ≠ (𝑦 · 𝑃))))
206197, 205mpbiran2d 706 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ↔ (𝑦 · 𝑃) ≤ (𝑄 · (2 · 𝑢))))
207 nnre 12160 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
208207adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ ℝ)
209130nngt0d 12202 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 0 < 𝑃)
210 lemuldiv 12035 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 ∈ ℝ ∧ (𝑄 · (2 · 𝑢)) ∈ ℝ ∧ (𝑃 ∈ ℝ ∧ 0 < 𝑃)) → ((𝑦 · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ↔ 𝑦 ≤ ((𝑄 · (2 · 𝑢)) / 𝑃)))
211208, 204, 131, 209, 210syl112anc 1374 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ↔ 𝑦 ≤ ((𝑄 · (2 · 𝑢)) / 𝑃)))
212201adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈ ℕ)
213212nncnd 12169 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈ ℂ)
214128nncnd 12169 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2 · 𝑢) ∈ ℂ)
215130nncnd 12169 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℂ)
216130nnne0d 12203 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ≠ 0)
217213, 214, 215, 216div23d 11968 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 · (2 · 𝑢)) / 𝑃) = ((𝑄 / 𝑃) · (2 · 𝑢)))
218217breq2d 5117 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 ≤ ((𝑄 · (2 · 𝑢)) / 𝑃) ↔ 𝑦 ≤ ((𝑄 / 𝑃) · (2 · 𝑢))))
219206, 211, 2183bitrd 304 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ↔ 𝑦 ≤ ((𝑄 / 𝑃) · (2 · 𝑢))))
220212nnred 12168 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈ ℝ)
221212nngt0d 12202 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 0 < 𝑄)
222 ltmul2 12006 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((2 · 𝑢) ∈ ℝ ∧ (𝑃 / 2) ∈ ℝ ∧ (𝑄 ∈ ℝ ∧ 0 < 𝑄)) → ((2 · 𝑢) < (𝑃 / 2) ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · (𝑃 / 2))))
223129, 132, 220, 221, 222syl112anc 1374 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((2 · 𝑢) < (𝑃 / 2) ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · (𝑃 / 2))))
224163, 223mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (2 · 𝑢)) < (𝑄 · (𝑃 / 2)))
225 2cnd 12231 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 2 ∈ ℂ)
226 2ne0 12257 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 2 ≠ 0
227226a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 2 ≠ 0)
228 divass 11831 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑄 ∈ ℂ ∧ 𝑃 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((𝑄 · 𝑃) / 2) = (𝑄 · (𝑃 / 2)))
229 div23 11832 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑄 ∈ ℂ ∧ 𝑃 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((𝑄 · 𝑃) / 2) = ((𝑄 / 2) · 𝑃))
230228, 229eqtr3d 2778 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑄 ∈ ℂ ∧ 𝑃 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (𝑄 · (𝑃 / 2)) = ((𝑄 / 2) · 𝑃))
231213, 215, 225, 227, 230syl112anc 1374 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (𝑃 / 2)) = ((𝑄 / 2) · 𝑃))
232224, 231breqtrd 5131 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (2 · 𝑢)) < ((𝑄 / 2) · 𝑃))
233220rehalfcld 12400 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 / 2) ∈ ℝ)
234233, 131remulcld 11185 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 / 2) · 𝑃) ∈ ℝ)
235 lttr 11231 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑦 · 𝑃) ∈ ℝ ∧ (𝑄 · (2 · 𝑢)) ∈ ℝ ∧ ((𝑄 / 2) · 𝑃) ∈ ℝ) → (((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ∧ (𝑄 · (2 · 𝑢)) < ((𝑄 / 2) · 𝑃)) → (𝑦 · 𝑃) < ((𝑄 / 2) · 𝑃)))
236200, 204, 234, 235syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ∧ (𝑄 · (2 · 𝑢)) < ((𝑄 / 2) · 𝑃)) → (𝑦 · 𝑃) < ((𝑄 / 2) · 𝑃)))
237232, 236mpan2d 692 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) → (𝑦 · 𝑃) < ((𝑄 / 2) · 𝑃)))
238 ltmul1 12005 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑦 ∈ ℝ ∧ (𝑄 / 2) ∈ ℝ ∧ (𝑃 ∈ ℝ ∧ 0 < 𝑃)) → (𝑦 < (𝑄 / 2) ↔ (𝑦 · 𝑃) < ((𝑄 / 2) · 𝑃)))
239208, 233, 131, 209, 238syl112anc 1374 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 < (𝑄 / 2) ↔ (𝑦 · 𝑃) < ((𝑄 / 2) · 𝑃)))
240237, 239sylibrd 258 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) → 𝑦 < (𝑄 / 2)))
241 peano2rem 11468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑄 ∈ ℝ → (𝑄 − 1) ∈ ℝ)
242220, 241syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 − 1) ∈ ℝ)
243242recnd 11183 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 − 1) ∈ ℂ)
244213, 243, 225, 227divsubdird 11970 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 − (𝑄 − 1)) / 2) = ((𝑄 / 2) − ((𝑄 − 1) / 2)))
245 lgsquad.5 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑁 = ((𝑄 − 1) / 2)
246245oveq2i 7368 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑄 / 2) − 𝑁) = ((𝑄 / 2) − ((𝑄 − 1) / 2))
247244, 246eqtr4di 2794 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 − (𝑄 − 1)) / 2) = ((𝑄 / 2) − 𝑁))
248 ax-1cn 11109 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 1 ∈ ℂ
249 nncan 11430 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑄 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑄 − (𝑄 − 1)) = 1)
250213, 248, 249sylancl 586 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 − (𝑄 − 1)) = 1)
251250oveq1d 7372 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 − (𝑄 − 1)) / 2) = (1 / 2))
252 halflt1 12371 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (1 / 2) < 1
253251, 252eqbrtrdi 5144 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 − (𝑄 − 1)) / 2) < 1)
254247, 253eqbrtrrd 5129 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 / 2) − 𝑁) < 1)
2552, 245gausslemma2dlem0b 26705 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝑁 ∈ ℕ)
256255ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑁 ∈ ℕ)
257256nnred 12168 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑁 ∈ ℝ)
258 1red 11156 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 1 ∈ ℝ)
259233, 257, 258ltsubadd2d 11753 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (((𝑄 / 2) − 𝑁) < 1 ↔ (𝑄 / 2) < (𝑁 + 1)))
260254, 259mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 / 2) < (𝑁 + 1))
261 peano2re 11328 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑁 ∈ ℝ → (𝑁 + 1) ∈ ℝ)
262257, 261syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑁 + 1) ∈ ℝ)
263 lttr 11231 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑦 ∈ ℝ ∧ (𝑄 / 2) ∈ ℝ ∧ (𝑁 + 1) ∈ ℝ) → ((𝑦 < (𝑄 / 2) ∧ (𝑄 / 2) < (𝑁 + 1)) → 𝑦 < (𝑁 + 1)))
264208, 233, 262, 263syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 < (𝑄 / 2) ∧ (𝑄 / 2) < (𝑁 + 1)) → 𝑦 < (𝑁 + 1)))
265260, 264mpan2d 692 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 < (𝑄 / 2) → 𝑦 < (𝑁 + 1)))
266240, 265syld 47 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) → 𝑦 < (𝑁 + 1)))
267 nnleltp1 12558 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑦𝑁𝑦 < (𝑁 + 1)))
268198, 256, 267syl2anc 584 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦𝑁𝑦 < (𝑁 + 1)))
269266, 268sylibrd 258 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) → 𝑦𝑁))
270269pm4.71rd 563 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ↔ (𝑦𝑁 ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)))))
27190, 65syldan 591 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ)
272 flge 13710 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ ∧ 𝑦 ∈ ℤ) → (𝑦 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)) ↔ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
273271, 190, 272syl2an 596 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)) ↔ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
274219, 270, 2733bitr3d 308 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦𝑁 ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢))) ↔ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
275274pm5.32da 579 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((𝑦 ∈ ℕ ∧ (𝑦𝑁 ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
276127, 275bitrid 282 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (((𝑦 ∈ ℕ ∧ 𝑦𝑁) ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
277276adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (((𝑦 ∈ ℕ ∧ 𝑦𝑁) ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
278 simpr 485 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → 𝑥 = (2 · 𝑢))
279 nnuz 12806 . . . . . . . . . . . . . . . . . . . . . . . 24 ℕ = (ℤ‘1)
280113, 279eleqtrdi 2848 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (2 · 𝑢) ∈ (ℤ‘1))
28124adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑀 ∈ ℤ)
282 elfz5 13433 . . . . . . . . . . . . . . . . . . . . . . 23 (((2 · 𝑢) ∈ (ℤ‘1) ∧ 𝑀 ∈ ℤ) → ((2 · 𝑢) ∈ (1...𝑀) ↔ (2 · 𝑢) ≤ 𝑀))
283280, 281, 282syl2anc 584 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((2 · 𝑢) ∈ (1...𝑀) ↔ (2 · 𝑢) ≤ 𝑀))
284152, 283mpbird 256 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (2 · 𝑢) ∈ (1...𝑀))
285284adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (2 · 𝑢) ∈ (1...𝑀))
286278, 285eqeltrd 2838 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → 𝑥 ∈ (1...𝑀))
287286biantrurd 533 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (𝑦 ∈ (1...𝑁) ↔ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))))
288255nnzd 12526 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑁 ∈ ℤ)
289288ad2antrr 724 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → 𝑁 ∈ ℤ)
290 fznn 13509 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ ℤ → (𝑦 ∈ (1...𝑁) ↔ (𝑦 ∈ ℕ ∧ 𝑦𝑁)))
291289, 290syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (𝑦 ∈ (1...𝑁) ↔ (𝑦 ∈ ℕ ∧ 𝑦𝑁)))
292287, 291bitr3d 280 . . . . . . . . . . . . . . . . 17 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ↔ (𝑦 ∈ ℕ ∧ 𝑦𝑁)))
293 oveq1 7364 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (2 · 𝑢) → (𝑥 · 𝑄) = ((2 · 𝑢) · 𝑄))
294113nncnd 12169 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (2 · 𝑢) ∈ ℂ)
295201nncnd 12169 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑄 ∈ ℂ)
296294, 295mulcomd 11176 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((2 · 𝑢) · 𝑄) = (𝑄 · (2 · 𝑢)))
297293, 296sylan9eqr 2798 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (𝑥 · 𝑄) = (𝑄 · (2 · 𝑢)))
298297breq2d 5117 . . . . . . . . . . . . . . . . 17 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → ((𝑦 · 𝑃) < (𝑥 · 𝑄) ↔ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢))))
299292, 298anbi12d 631 . . . . . . . . . . . . . . . 16 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)) ↔ ((𝑦 ∈ ℕ ∧ 𝑦𝑁) ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)))))
300271flcld 13703 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ)
301 fznn 13509 . . . . . . . . . . . . . . . . . 18 ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ → (𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
302300, 301syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
303302adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
304277, 299, 3033bitr4d 310 . . . . . . . . . . . . . . 15 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)) ↔ 𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
305126, 304bitrid 282 . . . . . . . . . . . . . 14 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (⟨𝑥, 𝑦⟩ ∈ 𝑆𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
306305pm5.32da 579 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((𝑥 = (2 · 𝑢) ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑆) ↔ (𝑥 = (2 · 𝑢) ∧ 𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
307 vex 3449 . . . . . . . . . . . . . . . . . 18 𝑥 ∈ V
308 vex 3449 . . . . . . . . . . . . . . . . . 18 𝑦 ∈ V
309307, 308op1std 7931 . . . . . . . . . . . . . . . . 17 (𝑧 = ⟨𝑥, 𝑦⟩ → (1st𝑧) = 𝑥)
310309eqeq2d 2747 . . . . . . . . . . . . . . . 16 (𝑧 = ⟨𝑥, 𝑦⟩ → ((2 · 𝑢) = (1st𝑧) ↔ (2 · 𝑢) = 𝑥))
311 eqcom 2743 . . . . . . . . . . . . . . . 16 ((2 · 𝑢) = 𝑥𝑥 = (2 · 𝑢))
312310, 311bitrdi 286 . . . . . . . . . . . . . . 15 (𝑧 = ⟨𝑥, 𝑦⟩ → ((2 · 𝑢) = (1st𝑧) ↔ 𝑥 = (2 · 𝑢)))
313312elrab 3645 . . . . . . . . . . . . . 14 (⟨𝑥, 𝑦⟩ ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} ↔ (⟨𝑥, 𝑦⟩ ∈ 𝑆𝑥 = (2 · 𝑢)))
314313biancomi 463 . . . . . . . . . . . . 13 (⟨𝑥, 𝑦⟩ ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} ↔ (𝑥 = (2 · 𝑢) ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑆))
315 opelxp 5669 . . . . . . . . . . . . . 14 (⟨𝑥, 𝑦⟩ ∈ ({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ↔ (𝑥 ∈ {(2 · 𝑢)} ∧ 𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
316 velsn 4602 . . . . . . . . . . . . . . 15 (𝑥 ∈ {(2 · 𝑢)} ↔ 𝑥 = (2 · 𝑢))
317316anbi1i 624 . . . . . . . . . . . . . 14 ((𝑥 ∈ {(2 · 𝑢)} ∧ 𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ↔ (𝑥 = (2 · 𝑢) ∧ 𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
318315, 317bitri 274 . . . . . . . . . . . . 13 (⟨𝑥, 𝑦⟩ ∈ ({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ↔ (𝑥 = (2 · 𝑢) ∧ 𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
319306, 314, 3183bitr4g 313 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (⟨𝑥, 𝑦⟩ ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} ↔ ⟨𝑥, 𝑦⟩ ∈ ({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
320122, 123, 319eqrelrdv 5748 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} = ({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
321320eqcomd 2742 . . . . . . . . . 10 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)})
322321fveq2d 6846 . . . . . . . . 9 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (♯‘({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) = (♯‘{𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)}))
323 hashfz1 14246 . . . . . . . . . 10 ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℕ0 → (♯‘(1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))
32491, 323syl 17 . . . . . . . . 9 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (♯‘(1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))
325118, 322, 3243eqtr3rd 2785 . . . . . . . 8 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = (♯‘{𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)}))
326325sumeq2dv 15588 . . . . . . 7 (𝜑 → Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(♯‘{𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)}))
327101adantr 481 . . . . . . . . 9 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑆 ∈ Fin)
328 ssfi 9117 . . . . . . . . 9 ((𝑆 ∈ Fin ∧ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} ⊆ 𝑆) → {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} ∈ Fin)
329327, 119, 328sylancl 586 . . . . . . . 8 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} ∈ Fin)
330 fveq2 6842 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑣 → (1st𝑧) = (1st𝑣))
331330eqeq2d 2747 . . . . . . . . . . . . . . 15 (𝑧 = 𝑣 → ((2 · 𝑢) = (1st𝑧) ↔ (2 · 𝑢) = (1st𝑣)))
332331elrab 3645 . . . . . . . . . . . . . 14 (𝑣 ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} ↔ (𝑣𝑆 ∧ (2 · 𝑢) = (1st𝑣)))
333332simprbi 497 . . . . . . . . . . . . 13 (𝑣 ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} → (2 · 𝑢) = (1st𝑣))
334333ad2antll 727 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)})) → (2 · 𝑢) = (1st𝑣))
335334oveq1d 7372 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)})) → ((2 · 𝑢) / 2) = ((1st𝑣) / 2))
336144nncnd 12169 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ∈ ℂ)
337336adantrr 715 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)})) → 𝑢 ∈ ℂ)
338 2cnd 12231 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)})) → 2 ∈ ℂ)
339226a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)})) → 2 ≠ 0)
340337, 338, 339divcan3d 11936 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)})) → ((2 · 𝑢) / 2) = 𝑢)
341335, 340eqtr3d 2778 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)})) → ((1st𝑣) / 2) = 𝑢)
342341ralrimivva 3197 . . . . . . . . 9 (𝜑 → ∀𝑢 ∈ (1...(⌊‘(𝑀 / 2)))∀𝑣 ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} ((1st𝑣) / 2) = 𝑢)
343 invdisj 5089 . . . . . . . . 9 (∀𝑢 ∈ (1...(⌊‘(𝑀 / 2)))∀𝑣 ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} ((1st𝑣) / 2) = 𝑢Disj 𝑢 ∈ (1...(⌊‘(𝑀 / 2))){𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)})
344342, 343syl 17 . . . . . . . 8 (𝜑Disj 𝑢 ∈ (1...(⌊‘(𝑀 / 2))){𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)})
34587, 329, 344hashiun 15707 . . . . . . 7 (𝜑 → (♯‘ 𝑢 ∈ (1...(⌊‘(𝑀 / 2))){𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)}) = Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(♯‘{𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)}))
346 iunrab 5012 . . . . . . . . 9 𝑢 ∈ (1...(⌊‘(𝑀 / 2))){𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} = {𝑧𝑆 ∣ ∃𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(2 · 𝑢) = (1st𝑧)}
347 2cn 12228 . . . . . . . . . . . . . 14 2 ∈ ℂ
348 zcn 12504 . . . . . . . . . . . . . . 15 (𝑢 ∈ ℤ → 𝑢 ∈ ℂ)
349348adantl 482 . . . . . . . . . . . . . 14 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ ℤ) → 𝑢 ∈ ℂ)
350 mulcom 11137 . . . . . . . . . . . . . 14 ((2 ∈ ℂ ∧ 𝑢 ∈ ℂ) → (2 · 𝑢) = (𝑢 · 2))
351347, 349, 350sylancr 587 . . . . . . . . . . . . 13 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ ℤ) → (2 · 𝑢) = (𝑢 · 2))
352351eqeq1d 2738 . . . . . . . . . . . 12 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ ℤ) → ((2 · 𝑢) = (1st𝑧) ↔ (𝑢 · 2) = (1st𝑧)))
353352rexbidva 3173 . . . . . . . . . . 11 ((𝜑𝑧𝑆) → (∃𝑢 ∈ ℤ (2 · 𝑢) = (1st𝑧) ↔ ∃𝑢 ∈ ℤ (𝑢 · 2) = (1st𝑧)))
354138anim1i 615 . . . . . . . . . . . . 13 ((𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ (2 · 𝑢) = (1st𝑧)) → (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧)))
355354reximi2 3082 . . . . . . . . . . . 12 (∃𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(2 · 𝑢) = (1st𝑧) → ∃𝑢 ∈ ℤ (2 · 𝑢) = (1st𝑧))
356 simprr 771 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (2 · 𝑢) = (1st𝑧))
357 simpr 485 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑧𝑆) → 𝑧𝑆)
35899, 357sselid 3942 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑧𝑆) → 𝑧 ∈ ((1...𝑀) × (1...𝑁)))
359 xp1st 7953 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ ((1...𝑀) × (1...𝑁)) → (1st𝑧) ∈ (1...𝑀))
360358, 359syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑧𝑆) → (1st𝑧) ∈ (1...𝑀))
361360adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (1st𝑧) ∈ (1...𝑀))
362 elfzle2 13445 . . . . . . . . . . . . . . . . . . . 20 ((1st𝑧) ∈ (1...𝑀) → (1st𝑧) ≤ 𝑀)
363361, 362syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (1st𝑧) ≤ 𝑀)
364356, 363eqbrtrd 5127 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (2 · 𝑢) ≤ 𝑀)
365 zre 12503 . . . . . . . . . . . . . . . . . . . 20 (𝑢 ∈ ℤ → 𝑢 ∈ ℝ)
366365ad2antrl 726 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 𝑢 ∈ ℝ)
3679ad2antrr 724 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 𝑀 ∈ ℝ)
368146a1i 11 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 2 ∈ ℝ)
369148a1i 11 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 0 < 2)
370366, 367, 368, 369, 150syl112anc 1374 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → ((2 · 𝑢) ≤ 𝑀𝑢 ≤ (𝑀 / 2)))
371364, 370mpbid 231 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 𝑢 ≤ (𝑀 / 2))
37210ad2antrr 724 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (𝑀 / 2) ∈ ℝ)
373 simprl 769 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 𝑢 ∈ ℤ)
374372, 373, 140syl2anc 584 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (𝑢 ≤ (𝑀 / 2) ↔ 𝑢 ≤ (⌊‘(𝑀 / 2))))
375371, 374mpbid 231 . . . . . . . . . . . . . . . 16 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 𝑢 ≤ (⌊‘(𝑀 / 2)))
376 2t0e0 12322 . . . . . . . . . . . . . . . . . . . . 21 (2 · 0) = 0
377 elfznn 13470 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1st𝑧) ∈ (1...𝑀) → (1st𝑧) ∈ ℕ)
378361, 377syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (1st𝑧) ∈ ℕ)
379356, 378eqeltrd 2838 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (2 · 𝑢) ∈ ℕ)
380379nngt0d 12202 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 0 < (2 · 𝑢))
381376, 380eqbrtrid 5140 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (2 · 0) < (2 · 𝑢))
382 0red 11158 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 0 ∈ ℝ)
383 ltmul2 12006 . . . . . . . . . . . . . . . . . . . . 21 ((0 ∈ ℝ ∧ 𝑢 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (0 < 𝑢 ↔ (2 · 0) < (2 · 𝑢)))
384382, 366, 368, 369, 383syl112anc 1374 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (0 < 𝑢 ↔ (2 · 0) < (2 · 𝑢)))
385381, 384mpbird 256 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 0 < 𝑢)
386 elnnz 12509 . . . . . . . . . . . . . . . . . . 19 (𝑢 ∈ ℕ ↔ (𝑢 ∈ ℤ ∧ 0 < 𝑢))
387373, 385, 386sylanbrc 583 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 𝑢 ∈ ℕ)
388387, 279eleqtrdi 2848 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 𝑢 ∈ (ℤ‘1))
38911ad2antrr 724 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (⌊‘(𝑀 / 2)) ∈ ℤ)
390 elfz5 13433 . . . . . . . . . . . . . . . . 17 ((𝑢 ∈ (ℤ‘1) ∧ (⌊‘(𝑀 / 2)) ∈ ℤ) → (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ↔ 𝑢 ≤ (⌊‘(𝑀 / 2))))
391388, 389, 390syl2anc 584 . . . . . . . . . . . . . . . 16 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ↔ 𝑢 ≤ (⌊‘(𝑀 / 2))))
392375, 391mpbird 256 . . . . . . . . . . . . . . 15 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 𝑢 ∈ (1...(⌊‘(𝑀 / 2))))
393392, 356jca 512 . . . . . . . . . . . . . 14 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ (2 · 𝑢) = (1st𝑧)))
394393ex 413 . . . . . . . . . . . . 13 ((𝜑𝑧𝑆) → ((𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧)) → (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ (2 · 𝑢) = (1st𝑧))))
395394reximdv2 3161 . . . . . . . . . . . 12 ((𝜑𝑧𝑆) → (∃𝑢 ∈ ℤ (2 · 𝑢) = (1st𝑧) → ∃𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(2 · 𝑢) = (1st𝑧)))
396355, 395impbid2 225 . . . . . . . . . . 11 ((𝜑𝑧𝑆) → (∃𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(2 · 𝑢) = (1st𝑧) ↔ ∃𝑢 ∈ ℤ (2 · 𝑢) = (1st𝑧)))
397 2z 12535 . . . . . . . . . . . 12 2 ∈ ℤ
398360elfzelzd 13442 . . . . . . . . . . . 12 ((𝜑𝑧𝑆) → (1st𝑧) ∈ ℤ)
399 divides 16138 . . . . . . . . . . . 12 ((2 ∈ ℤ ∧ (1st𝑧) ∈ ℤ) → (2 ∥ (1st𝑧) ↔ ∃𝑢 ∈ ℤ (𝑢 · 2) = (1st𝑧)))
400397, 398, 399sylancr 587 . . . . . . . . . . 11 ((𝜑𝑧𝑆) → (2 ∥ (1st𝑧) ↔ ∃𝑢 ∈ ℤ (𝑢 · 2) = (1st𝑧)))
401353, 396, 4003bitr4d 310 . . . . . . . . . 10 ((𝜑𝑧𝑆) → (∃𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(2 · 𝑢) = (1st𝑧) ↔ 2 ∥ (1st𝑧)))
402401rabbidva 3414 . . . . . . . . 9 (𝜑 → {𝑧𝑆 ∣ ∃𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(2 · 𝑢) = (1st𝑧)} = {𝑧𝑆 ∣ 2 ∥ (1st𝑧)})
403346, 402eqtrid 2788 . . . . . . . 8 (𝜑 𝑢 ∈ (1...(⌊‘(𝑀 / 2))){𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} = {𝑧𝑆 ∣ 2 ∥ (1st𝑧)})
404403fveq2d 6846 . . . . . . 7 (𝜑 → (♯‘ 𝑢 ∈ (1...(⌊‘(𝑀 / 2))){𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)}) = (♯‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)}))
405326, 345, 4043eqtr2d 2782 . . . . . 6 (𝜑 → Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = (♯‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)}))
406405oveq2d 7373 . . . . 5 (𝜑 → (-1↑Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (-1↑(♯‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)})))
4071, 2, 3, 5, 245, 97lgsquadlem1 26728 . . . . 5 (𝜑 → (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})))
408406, 407oveq12d 7375 . . . 4 (𝜑 → ((-1↑Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) · (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = ((-1↑(♯‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)})) · (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))))
409112, 408eqtr4d 2779 . . 3 (𝜑 → (-1↑((♯‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)}) + (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))) = ((-1↑Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) · (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
410 inrab 4266 . . . . . . 7 ({𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∩ {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) = {𝑧𝑆 ∣ (2 ∥ (1st𝑧) ∧ ¬ 2 ∥ (1st𝑧))}
411 pm3.24 403 . . . . . . . . . 10 ¬ (2 ∥ (1st𝑧) ∧ ¬ 2 ∥ (1st𝑧))
412411a1i 11 . . . . . . . . 9 (𝜑 → ¬ (2 ∥ (1st𝑧) ∧ ¬ 2 ∥ (1st𝑧)))
413412ralrimivw 3147 . . . . . . . 8 (𝜑 → ∀𝑧𝑆 ¬ (2 ∥ (1st𝑧) ∧ ¬ 2 ∥ (1st𝑧)))
414 rabeq0 4344 . . . . . . . 8 ({𝑧𝑆 ∣ (2 ∥ (1st𝑧) ∧ ¬ 2 ∥ (1st𝑧))} = ∅ ↔ ∀𝑧𝑆 ¬ (2 ∥ (1st𝑧) ∧ ¬ 2 ∥ (1st𝑧)))
415413, 414sylibr 233 . . . . . . 7 (𝜑 → {𝑧𝑆 ∣ (2 ∥ (1st𝑧) ∧ ¬ 2 ∥ (1st𝑧))} = ∅)
416410, 415eqtrid 2788 . . . . . 6 (𝜑 → ({𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∩ {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) = ∅)
417 hashun 14282 . . . . . 6 (({𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∈ Fin ∧ {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)} ∈ Fin ∧ ({𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∩ {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) = ∅) → (♯‘({𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∪ {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) = ((♯‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)}) + (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})))
418109, 104, 416, 417syl3anc 1371 . . . . 5 (𝜑 → (♯‘({𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∪ {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) = ((♯‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)}) + (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})))
419 unrab 4265 . . . . . . 7 ({𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∪ {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) = {𝑧𝑆 ∣ (2 ∥ (1st𝑧) ∨ ¬ 2 ∥ (1st𝑧))}
420 exmid 893 . . . . . . . . 9 (2 ∥ (1st𝑧) ∨ ¬ 2 ∥ (1st𝑧))
421420rgenw 3068 . . . . . . . 8 𝑧𝑆 (2 ∥ (1st𝑧) ∨ ¬ 2 ∥ (1st𝑧))
422 rabid2 3436 . . . . . . . 8 (𝑆 = {𝑧𝑆 ∣ (2 ∥ (1st𝑧) ∨ ¬ 2 ∥ (1st𝑧))} ↔ ∀𝑧𝑆 (2 ∥ (1st𝑧) ∨ ¬ 2 ∥ (1st𝑧)))
423421, 422mpbir 230 . . . . . . 7 𝑆 = {𝑧𝑆 ∣ (2 ∥ (1st𝑧) ∨ ¬ 2 ∥ (1st𝑧))}
424419, 423eqtr4i 2767 . . . . . 6 ({𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∪ {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) = 𝑆
425424fveq2i 6845 . . . . 5 (♯‘({𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∪ {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) = (♯‘𝑆)
426418, 425eqtr3di 2791 . . . 4 (𝜑 → ((♯‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)}) + (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) = (♯‘𝑆))
427426oveq2d 7373 . . 3 (𝜑 → (-1↑((♯‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)}) + (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))) = (-1↑(♯‘𝑆)))
42893, 409, 4273eqtr2d 2782 . 2 (𝜑 → (-1↑(Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = (-1↑(♯‘𝑆)))
4294, 78, 4283eqtrd 2780 1 (𝜑 → (𝑄 /L 𝑃) = (-1↑(♯‘𝑆)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 845  w3a 1087   = wceq 1541  wcel 2106  wne 2943  wral 3064  wrex 3073  {crab 3407  cdif 3907  cun 3908  cin 3909  wss 3910  c0 4282  {csn 4586  cop 4592   ciun 4954  Disj wdisj 5070   class class class wbr 5105  {copab 5167   × cxp 5631  Rel wrel 5638  cfv 6496  (class class class)co 7357  1st c1st 7919  cen 8880  Fincfn 8883  cc 11049  cr 11050  0cc0 11051  1c1 11052   + caddc 11054   · cmul 11056   < clt 11189  cle 11190  cmin 11385  -cneg 11386   / cdiv 11812  cn 12153  2c2 12208  0cn0 12413  cz 12499  cuz 12763  +crp 12915  ...cfz 13424  cfl 13695  cexp 13967  chash 14230  Σcsu 15570  cdvds 16136   gcd cgcd 16374  cprime 16547   /L clgs 26642
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-inf2 9577  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129  ax-addf 11130  ax-mulf 11131
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-disj 5071  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-of 7617  df-om 7803  df-1st 7921  df-2nd 7922  df-supp 8093  df-tpos 8157  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-2o 8413  df-oadd 8416  df-er 8648  df-ec 8650  df-qs 8654  df-map 8767  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fsupp 9306  df-sup 9378  df-inf 9379  df-oi 9446  df-dju 9837  df-card 9875  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-4 12218  df-5 12219  df-6 12220  df-7 12221  df-8 12222  df-9 12223  df-n0 12414  df-xnn0 12486  df-z 12500  df-dec 12619  df-uz 12764  df-q 12874  df-rp 12916  df-fz 13425  df-fzo 13568  df-fl 13697  df-mod 13775  df-seq 13907  df-exp 13968  df-hash 14231  df-cj 14984  df-re 14985  df-im 14986  df-sqrt 15120  df-abs 15121  df-clim 15370  df-sum 15571  df-dvds 16137  df-gcd 16375  df-prm 16548  df-phi 16638  df-pc 16709  df-struct 17019  df-sets 17036  df-slot 17054  df-ndx 17066  df-base 17084  df-ress 17113  df-plusg 17146  df-mulr 17147  df-starv 17148  df-sca 17149  df-vsca 17150  df-ip 17151  df-tset 17152  df-ple 17153  df-ds 17155  df-unif 17156  df-0g 17323  df-gsum 17324  df-imas 17390  df-qus 17391  df-mgm 18497  df-sgrp 18546  df-mnd 18557  df-mhm 18601  df-submnd 18602  df-grp 18751  df-minusg 18752  df-sbg 18753  df-mulg 18873  df-subg 18925  df-nsg 18926  df-eqg 18927  df-ghm 19006  df-cntz 19097  df-cmn 19564  df-abl 19565  df-mgp 19897  df-ur 19914  df-ring 19966  df-cring 19967  df-oppr 20049  df-dvdsr 20070  df-unit 20071  df-invr 20101  df-dvr 20112  df-rnghom 20146  df-drng 20187  df-field 20188  df-subrg 20220  df-lmod 20324  df-lss 20393  df-lsp 20433  df-sra 20633  df-rgmod 20634  df-lidl 20635  df-rsp 20636  df-2idl 20702  df-nzr 20728  df-rlreg 20753  df-domn 20754  df-idom 20755  df-cnfld 20797  df-zring 20870  df-zrh 20904  df-zn 20907  df-lgs 26643
This theorem is referenced by:  lgsquadlem3  26730
  Copyright terms: Public domain W3C validator