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

Theorem lgsquadlem2 26529
Description: Lemma for lgsquad 26531. Count the members of 𝑆 with even coordinates, and combine with lgsquadlem1 26528 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 26527 . 2 (𝜑 → (𝑄 /L 𝑃) = (-1↑Σ𝑢 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
5 lgsquad.4 . . . . . 6 𝑀 = ((𝑃 − 1) / 2)
65oveq2i 7286 . . . . 5 (1...𝑀) = (1...((𝑃 − 1) / 2))
76sumeq1i 15410 . . . 4 Σ𝑢 ∈ (1...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = Σ𝑢 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))
81, 5gausslemma2dlem0b 26505 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℕ)
98nnred 11988 . . . . . . . . . 10 (𝜑𝑀 ∈ ℝ)
109rehalfcld 12220 . . . . . . . . 9 (𝜑 → (𝑀 / 2) ∈ ℝ)
1110flcld 13518 . . . . . . . 8 (𝜑 → (⌊‘(𝑀 / 2)) ∈ ℤ)
1211zred 12426 . . . . . . 7 (𝜑 → (⌊‘(𝑀 / 2)) ∈ ℝ)
1312ltp1d 11905 . . . . . 6 (𝜑 → (⌊‘(𝑀 / 2)) < ((⌊‘(𝑀 / 2)) + 1))
14 fzdisj 13283 . . . . . 6 ((⌊‘(𝑀 / 2)) < ((⌊‘(𝑀 / 2)) + 1) → ((1...(⌊‘(𝑀 / 2))) ∩ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) = ∅)
1513, 14syl 17 . . . . 5 (𝜑 → ((1...(⌊‘(𝑀 / 2))) ∩ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) = ∅)
168nnrpd 12770 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℝ+)
1716rphalfcld 12784 . . . . . . . . . 10 (𝜑 → (𝑀 / 2) ∈ ℝ+)
1817rpge0d 12776 . . . . . . . . 9 (𝜑 → 0 ≤ (𝑀 / 2))
19 flge0nn0 13540 . . . . . . . . 9 (((𝑀 / 2) ∈ ℝ ∧ 0 ≤ (𝑀 / 2)) → (⌊‘(𝑀 / 2)) ∈ ℕ0)
2010, 18, 19syl2anc 584 . . . . . . . 8 (𝜑 → (⌊‘(𝑀 / 2)) ∈ ℕ0)
218nnnn0d 12293 . . . . . . . 8 (𝜑𝑀 ∈ ℕ0)
22 rphalflt 12759 . . . . . . . . . . 11 (𝑀 ∈ ℝ+ → (𝑀 / 2) < 𝑀)
2316, 22syl 17 . . . . . . . . . 10 (𝜑 → (𝑀 / 2) < 𝑀)
248nnzd 12425 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℤ)
25 fllt 13526 . . . . . . . . . . 11 (((𝑀 / 2) ∈ ℝ ∧ 𝑀 ∈ ℤ) → ((𝑀 / 2) < 𝑀 ↔ (⌊‘(𝑀 / 2)) < 𝑀))
2610, 24, 25syl2anc 584 . . . . . . . . . 10 (𝜑 → ((𝑀 / 2) < 𝑀 ↔ (⌊‘(𝑀 / 2)) < 𝑀))
2723, 26mpbid 231 . . . . . . . . 9 (𝜑 → (⌊‘(𝑀 / 2)) < 𝑀)
2812, 9, 27ltled 11123 . . . . . . . 8 (𝜑 → (⌊‘(𝑀 / 2)) ≤ 𝑀)
29 elfz2nn0 13347 . . . . . . . 8 ((⌊‘(𝑀 / 2)) ∈ (0...𝑀) ↔ ((⌊‘(𝑀 / 2)) ∈ ℕ0𝑀 ∈ ℕ0 ∧ (⌊‘(𝑀 / 2)) ≤ 𝑀))
3020, 21, 28, 29syl3anbrc 1342 . . . . . . 7 (𝜑 → (⌊‘(𝑀 / 2)) ∈ (0...𝑀))
31 nn0uz 12620 . . . . . . . . 9 0 = (ℤ‘0)
3221, 31eleqtrdi 2849 . . . . . . . 8 (𝜑𝑀 ∈ (ℤ‘0))
33 elfzp12 13335 . . . . . . . 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 4324 . . . . . . . . 9 ((1...𝑀) ∪ ∅) = (1...𝑀)
37 uncom 4087 . . . . . . . . 9 ((1...𝑀) ∪ ∅) = (∅ ∪ (1...𝑀))
3836, 37eqtr3i 2768 . . . . . . . 8 (1...𝑀) = (∅ ∪ (1...𝑀))
39 oveq2 7283 . . . . . . . . . 10 ((⌊‘(𝑀 / 2)) = 0 → (1...(⌊‘(𝑀 / 2))) = (1...0))
40 fz10 13277 . . . . . . . . . 10 (1...0) = ∅
4139, 40eqtrdi 2794 . . . . . . . . 9 ((⌊‘(𝑀 / 2)) = 0 → (1...(⌊‘(𝑀 / 2))) = ∅)
42 oveq1 7282 . . . . . . . . . . 11 ((⌊‘(𝑀 / 2)) = 0 → ((⌊‘(𝑀 / 2)) + 1) = (0 + 1))
43 0p1e1 12095 . . . . . . . . . . 11 (0 + 1) = 1
4442, 43eqtrdi 2794 . . . . . . . . . 10 ((⌊‘(𝑀 / 2)) = 0 → ((⌊‘(𝑀 / 2)) + 1) = 1)
4544oveq1d 7290 . . . . . . . . 9 ((⌊‘(𝑀 / 2)) = 0 → (((⌊‘(𝑀 / 2)) + 1)...𝑀) = (1...𝑀))
4641, 45uneq12d 4098 . . . . . . . 8 ((⌊‘(𝑀 / 2)) = 0 → ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) = (∅ ∪ (1...𝑀)))
4738, 46eqtr4id 2797 . . . . . . 7 ((⌊‘(𝑀 / 2)) = 0 → (1...𝑀) = ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀)))
48 fzsplit 13282 . . . . . . . 8 ((⌊‘(𝑀 / 2)) ∈ (1...𝑀) → (1...𝑀) = ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀)))
4943oveq1i 7285 . . . . . . . 8 ((0 + 1)...𝑀) = (1...𝑀)
5048, 49eleq2s 2857 . . . . . . 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 13693 . . . . 5 (𝜑 → (1...𝑀) ∈ Fin)
542gausslemma2dlem0a 26504 . . . . . . . . . . 11 (𝜑𝑄 ∈ ℕ)
5554nnred 11988 . . . . . . . . . 10 (𝜑𝑄 ∈ ℝ)
561gausslemma2dlem0a 26504 . . . . . . . . . 10 (𝜑𝑃 ∈ ℕ)
5755, 56nndivred 12027 . . . . . . . . 9 (𝜑 → (𝑄 / 𝑃) ∈ ℝ)
5857adantr 481 . . . . . . . 8 ((𝜑𝑢 ∈ (1...𝑀)) → (𝑄 / 𝑃) ∈ ℝ)
59 2nn 12046 . . . . . . . . . 10 2 ∈ ℕ
60 elfznn 13285 . . . . . . . . . . 11 (𝑢 ∈ (1...𝑀) → 𝑢 ∈ ℕ)
6160adantl 482 . . . . . . . . . 10 ((𝜑𝑢 ∈ (1...𝑀)) → 𝑢 ∈ ℕ)
62 nnmulcl 11997 . . . . . . . . . 10 ((2 ∈ ℕ ∧ 𝑢 ∈ ℕ) → (2 · 𝑢) ∈ ℕ)
6359, 61, 62sylancr 587 . . . . . . . . 9 ((𝜑𝑢 ∈ (1...𝑀)) → (2 · 𝑢) ∈ ℕ)
6463nnred 11988 . . . . . . . 8 ((𝜑𝑢 ∈ (1...𝑀)) → (2 · 𝑢) ∈ ℝ)
6558, 64remulcld 11005 . . . . . . 7 ((𝜑𝑢 ∈ (1...𝑀)) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ)
6654nnrpd 12770 . . . . . . . . . . 11 (𝜑𝑄 ∈ ℝ+)
6756nnrpd 12770 . . . . . . . . . . 11 (𝜑𝑃 ∈ ℝ+)
6866, 67rpdivcld 12789 . . . . . . . . . 10 (𝜑 → (𝑄 / 𝑃) ∈ ℝ+)
6968adantr 481 . . . . . . . . 9 ((𝜑𝑢 ∈ (1...𝑀)) → (𝑄 / 𝑃) ∈ ℝ+)
7063nnrpd 12770 . . . . . . . . 9 ((𝜑𝑢 ∈ (1...𝑀)) → (2 · 𝑢) ∈ ℝ+)
7169, 70rpmulcld 12788 . . . . . . . 8 ((𝜑𝑢 ∈ (1...𝑀)) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ+)
7271rpge0d 12776 . . . . . . 7 ((𝜑𝑢 ∈ (1...𝑀)) → 0 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)))
73 flge0nn0 13540 . . . . . . 7 ((((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ ∧ 0 ≤ ((𝑄 / 𝑃) · (2 · 𝑢))) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℕ0)
7465, 72, 73syl2anc 584 . . . . . 6 ((𝜑𝑢 ∈ (1...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℕ0)
7574nn0cnd 12295 . . . . 5 ((𝜑𝑢 ∈ (1...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℂ)
7615, 52, 53, 75fsumsplit 15453 . . . 4 (𝜑 → Σ𝑢 ∈ (1...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = (Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
777, 76eqtr3id 2792 . . 3 (𝜑 → Σ𝑢 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = (Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
7877oveq2d 7291 . 2 (𝜑 → (-1↑Σ𝑢 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (-1↑(Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
79 neg1cn 12087 . . . . 5 -1 ∈ ℂ
8079a1i 11 . . . 4 (𝜑 → -1 ∈ ℂ)
81 fzfid 13693 . . . . 5 (𝜑 → (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∈ Fin)
82 ssun2 4107 . . . . . . . 8 (((⌊‘(𝑀 / 2)) + 1)...𝑀) ⊆ ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀))
8382, 52sseqtrrid 3974 . . . . . . 7 (𝜑 → (((⌊‘(𝑀 / 2)) + 1)...𝑀) ⊆ (1...𝑀))
8483sselda 3921 . . . . . 6 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ∈ (1...𝑀))
8584, 74syldan 591 . . . . 5 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℕ0)
8681, 85fsumnn0cl 15448 . . . 4 (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℕ0)
87 fzfid 13693 . . . . 5 (𝜑 → (1...(⌊‘(𝑀 / 2))) ∈ Fin)
88 ssun1 4106 . . . . . . . 8 (1...(⌊‘(𝑀 / 2))) ⊆ ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀))
8988, 52sseqtrrid 3974 . . . . . . 7 (𝜑 → (1...(⌊‘(𝑀 / 2))) ⊆ (1...𝑀))
9089sselda 3921 . . . . . 6 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ∈ (1...𝑀))
9190, 74syldan 591 . . . . 5 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℕ0)
9287, 91fsumnn0cl 15448 . . . 4 (𝜑 → Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℕ0)
9380, 86, 92expaddd 13866 . . 3 (𝜑 → (-1↑(Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = ((-1↑Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) · (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
94 fzfid 13693 . . . . . . . . 9 (𝜑 → (1...𝑁) ∈ Fin)
95 xpfi 9085 . . . . . . . . 9 (((1...𝑀) ∈ Fin ∧ (1...𝑁) ∈ Fin) → ((1...𝑀) × (1...𝑁)) ∈ Fin)
9653, 94, 95syl2anc 584 . . . . . . . 8 (𝜑 → ((1...𝑀) × (1...𝑁)) ∈ Fin)
97 lgsquad.6 . . . . . . . . 9 𝑆 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))}
98 opabssxp 5679 . . . . . . . . 9 {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} ⊆ ((1...𝑀) × (1...𝑁))
9997, 98eqsstri 3955 . . . . . . . 8 𝑆 ⊆ ((1...𝑀) × (1...𝑁))
100 ssfi 8956 . . . . . . . 8 ((((1...𝑀) × (1...𝑁)) ∈ Fin ∧ 𝑆 ⊆ ((1...𝑀) × (1...𝑁))) → 𝑆 ∈ Fin)
10196, 99, 100sylancl 586 . . . . . . 7 (𝜑𝑆 ∈ Fin)
102 ssrab2 4013 . . . . . . 7 {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)} ⊆ 𝑆
103 ssfi 8956 . . . . . . 7 ((𝑆 ∈ Fin ∧ {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)} ⊆ 𝑆) → {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)} ∈ Fin)
104101, 102, 103sylancl 586 . . . . . 6 (𝜑 → {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)} ∈ Fin)
105 hashcl 14071 . . . . . 6 ({𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)} ∈ Fin → (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) ∈ ℕ0)
106104, 105syl 17 . . . . 5 (𝜑 → (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) ∈ ℕ0)
107 ssrab2 4013 . . . . . . 7 {𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ⊆ 𝑆
108 ssfi 8956 . . . . . . 7 ((𝑆 ∈ Fin ∧ {𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ⊆ 𝑆) → {𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∈ Fin)
109101, 107, 108sylancl 586 . . . . . 6 (𝜑 → {𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∈ Fin)
110 hashcl 14071 . . . . . 6 ({𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∈ Fin → (♯‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)}) ∈ ℕ0)
111109, 110syl 17 . . . . 5 (𝜑 → (♯‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)}) ∈ ℕ0)
11280, 106, 111expaddd 13866 . . . 4 (𝜑 → (-1↑((♯‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)}) + (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))) = ((-1↑(♯‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)})) · (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))))
11390, 63syldan 591 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (2 · 𝑢) ∈ ℕ)
114 fzfid 13693 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ Fin)
115 xpsnen2g 8852 . . . . . . . . . . 11 (((2 · 𝑢) ∈ ℕ ∧ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ Fin) → ({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ≈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
116113, 114, 115syl2anc 584 . . . . . . . . . 10 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ≈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
117 hasheni 14062 . . . . . . . . . 10 (({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ≈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) → (♯‘({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) = (♯‘(1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
118116, 117syl 17 . . . . . . . . 9 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (♯‘({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) = (♯‘(1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
119 ssrab2 4013 . . . . . . . . . . . . 13 {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} ⊆ 𝑆
12097relopabiv 5730 . . . . . . . . . . . . 13 Rel 𝑆
121 relss 5692 . . . . . . . . . . . . 13 ({𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} ⊆ 𝑆 → (Rel 𝑆 → Rel {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)}))
122119, 120, 121mp2 9 . . . . . . . . . . . 12 Rel {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)}
123 relxp 5607 . . . . . . . . . . . 12 Rel ({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
12497eleq2i 2830 . . . . . . . . . . . . . . . 16 (⟨𝑥, 𝑦⟩ ∈ 𝑆 ↔ ⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))})
125 opabidw 5437 . . . . . . . . . . . . . . . 16 (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} ↔ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))
126124, 125bitri 274 . . . . . . . . . . . . . . 15 (⟨𝑥, 𝑦⟩ ∈ 𝑆 ↔ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))
127 anass 469 . . . . . . . . . . . . . . . . . 18 (((𝑦 ∈ ℕ ∧ 𝑦𝑁) ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢))) ↔ (𝑦 ∈ ℕ ∧ (𝑦𝑁 ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)))))
128113adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2 · 𝑢) ∈ ℕ)
129128nnred 11988 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2 · 𝑢) ∈ ℝ)
13056ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℕ)
131130nnred 11988 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℝ)
132131rehalfcld 12220 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 / 2) ∈ ℝ)
1339adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑀 ∈ ℝ)
134133adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑀 ∈ ℝ)
135 elfzle2 13260 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) → 𝑢 ≤ (⌊‘(𝑀 / 2)))
136135adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ≤ (⌊‘(𝑀 / 2)))
137133rehalfcld 12220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (𝑀 / 2) ∈ ℝ)
138 elfzelz 13256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) → 𝑢 ∈ ℤ)
139138adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ∈ ℤ)
140 flge 13525 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑀 / 2) ∈ ℝ ∧ 𝑢 ∈ ℤ) → (𝑢 ≤ (𝑀 / 2) ↔ 𝑢 ≤ (⌊‘(𝑀 / 2))))
141137, 139, 140syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (𝑢 ≤ (𝑀 / 2) ↔ 𝑢 ≤ (⌊‘(𝑀 / 2))))
142136, 141mpbird 256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ≤ (𝑀 / 2))
143 elfznn 13285 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) → 𝑢 ∈ ℕ)
144143adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ∈ ℕ)
145144nnred 11988 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ∈ ℝ)
146 2re 12047 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 2 ∈ ℝ
147146a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 2 ∈ ℝ)
148 2pos 12076 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 0 < 2
149148a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 0 < 2)
150 lemuldiv2 11856 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑢 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 𝑢) ≤ 𝑀𝑢 ≤ (𝑀 / 2)))
151145, 133, 147, 149, 150syl112anc 1373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((2 · 𝑢) ≤ 𝑀𝑢 ≤ (𝑀 / 2)))
152142, 151mpbird 256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (2 · 𝑢) ≤ 𝑀)
153152adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2 · 𝑢) ≤ 𝑀)
154131ltm1d 11907 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 − 1) < 𝑃)
155 peano2rem 11288 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑃 ∈ ℝ → (𝑃 − 1) ∈ ℝ)
156131, 155syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 − 1) ∈ ℝ)
157146a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 2 ∈ ℝ)
158148a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 0 < 2)
159 ltdiv1 11839 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑃 − 1) ∈ ℝ ∧ 𝑃 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((𝑃 − 1) < 𝑃 ↔ ((𝑃 − 1) / 2) < (𝑃 / 2)))
160156, 131, 157, 158, 159syl112anc 1373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑃 − 1) < 𝑃 ↔ ((𝑃 − 1) / 2) < (𝑃 / 2)))
161154, 160mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑃 − 1) / 2) < (𝑃 / 2))
1625, 161eqbrtrid 5109 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑀 < (𝑃 / 2))
163129, 134, 132, 153, 162lelttrd 11133 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2 · 𝑢) < (𝑃 / 2))
164130nnrpd 12770 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℝ+)
165 rphalflt 12759 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑃 ∈ ℝ+ → (𝑃 / 2) < 𝑃)
166164, 165syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 / 2) < 𝑃)
167129, 132, 131, 163, 166lttrd 11136 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2 · 𝑢) < 𝑃)
168129, 131ltnled 11122 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((2 · 𝑢) < 𝑃 ↔ ¬ 𝑃 ≤ (2 · 𝑢)))
169167, 168mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ¬ 𝑃 ≤ (2 · 𝑢))
1701eldifad 3899 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝑃 ∈ ℙ)
171170ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℙ)
172 prmz 16380 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
173171, 172syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℤ)
174 dvdsle 16019 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑃 ∈ ℤ ∧ (2 · 𝑢) ∈ ℕ) → (𝑃 ∥ (2 · 𝑢) → 𝑃 ≤ (2 · 𝑢)))
175173, 128, 174syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 ∥ (2 · 𝑢) → 𝑃 ≤ (2 · 𝑢)))
176169, 175mtod 197 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ¬ 𝑃 ∥ (2 · 𝑢))
1772eldifad 3899 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝑄 ∈ ℙ)
178 prmrp 16417 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ) → ((𝑃 gcd 𝑄) = 1 ↔ 𝑃𝑄))
179170, 177, 178syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ((𝑃 gcd 𝑄) = 1 ↔ 𝑃𝑄))
1803, 179mpbird 256 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝑃 gcd 𝑄) = 1)
181180ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 gcd 𝑄) = 1)
182177ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈ ℙ)
183 prmz 16380 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑄 ∈ ℙ → 𝑄 ∈ ℤ)
184182, 183syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈ ℤ)
185128nnzd 12425 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2 · 𝑢) ∈ ℤ)
186 coprmdvds 16358 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑃 ∈ ℤ ∧ 𝑄 ∈ ℤ ∧ (2 · 𝑢) ∈ ℤ) → ((𝑃 ∥ (𝑄 · (2 · 𝑢)) ∧ (𝑃 gcd 𝑄) = 1) → 𝑃 ∥ (2 · 𝑢)))
187173, 184, 185, 186syl3anc 1370 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑃 ∥ (𝑄 · (2 · 𝑢)) ∧ (𝑃 gcd 𝑄) = 1) → 𝑃 ∥ (2 · 𝑢)))
188181, 187mpan2d 691 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 ∥ (𝑄 · (2 · 𝑢)) → 𝑃 ∥ (2 · 𝑢)))
189176, 188mtod 197 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ¬ 𝑃 ∥ (𝑄 · (2 · 𝑢)))
190 nnz 12342 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 ∈ ℕ → 𝑦 ∈ ℤ)
191190adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ ℤ)
192 dvdsmul2 15988 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑦 ∈ ℤ ∧ 𝑃 ∈ ℤ) → 𝑃 ∥ (𝑦 · 𝑃))
193191, 173, 192syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∥ (𝑦 · 𝑃))
194 breq2 5078 . . . . . . . . . . . . . . . . . . . . . . . . 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 12026 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 · 𝑃) ∈ ℕ)
200199nnred 11988 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 · 𝑃) ∈ ℝ)
20154adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑄 ∈ ℕ)
202201, 113nnmulcld 12026 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (𝑄 · (2 · 𝑢)) ∈ ℕ)
203202adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (2 · 𝑢)) ∈ ℕ)
204203nnred 11988 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (2 · 𝑢)) ∈ ℝ)
205200, 204ltlend 11120 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ↔ ((𝑦 · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ∧ (𝑄 · (2 · 𝑢)) ≠ (𝑦 · 𝑃))))
206197, 205mpbiran2d 705 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ↔ (𝑦 · 𝑃) ≤ (𝑄 · (2 · 𝑢))))
207 nnre 11980 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
208207adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ ℝ)
209130nngt0d 12022 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 0 < 𝑃)
210 lemuldiv 11855 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 ∈ ℝ ∧ (𝑄 · (2 · 𝑢)) ∈ ℝ ∧ (𝑃 ∈ ℝ ∧ 0 < 𝑃)) → ((𝑦 · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ↔ 𝑦 ≤ ((𝑄 · (2 · 𝑢)) / 𝑃)))
211208, 204, 131, 209, 210syl112anc 1373 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ↔ 𝑦 ≤ ((𝑄 · (2 · 𝑢)) / 𝑃)))
212201adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈ ℕ)
213212nncnd 11989 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈ ℂ)
214128nncnd 11989 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2 · 𝑢) ∈ ℂ)
215130nncnd 11989 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℂ)
216130nnne0d 12023 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ≠ 0)
217213, 214, 215, 216div23d 11788 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 · (2 · 𝑢)) / 𝑃) = ((𝑄 / 𝑃) · (2 · 𝑢)))
218217breq2d 5086 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 ≤ ((𝑄 · (2 · 𝑢)) / 𝑃) ↔ 𝑦 ≤ ((𝑄 / 𝑃) · (2 · 𝑢))))
219206, 211, 2183bitrd 305 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ↔ 𝑦 ≤ ((𝑄 / 𝑃) · (2 · 𝑢))))
220212nnred 11988 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈ ℝ)
221212nngt0d 12022 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 0 < 𝑄)
222 ltmul2 11826 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((2 · 𝑢) ∈ ℝ ∧ (𝑃 / 2) ∈ ℝ ∧ (𝑄 ∈ ℝ ∧ 0 < 𝑄)) → ((2 · 𝑢) < (𝑃 / 2) ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · (𝑃 / 2))))
223129, 132, 220, 221, 222syl112anc 1373 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((2 · 𝑢) < (𝑃 / 2) ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · (𝑃 / 2))))
224163, 223mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (2 · 𝑢)) < (𝑄 · (𝑃 / 2)))
225 2cnd 12051 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 2 ∈ ℂ)
226 2ne0 12077 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 2 ≠ 0
227226a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 2 ≠ 0)
228 divass 11651 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑄 ∈ ℂ ∧ 𝑃 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((𝑄 · 𝑃) / 2) = (𝑄 · (𝑃 / 2)))
229 div23 11652 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑄 ∈ ℂ ∧ 𝑃 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((𝑄 · 𝑃) / 2) = ((𝑄 / 2) · 𝑃))
230228, 229eqtr3d 2780 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑄 ∈ ℂ ∧ 𝑃 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (𝑄 · (𝑃 / 2)) = ((𝑄 / 2) · 𝑃))
231213, 215, 225, 227, 230syl112anc 1373 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (𝑃 / 2)) = ((𝑄 / 2) · 𝑃))
232224, 231breqtrd 5100 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (2 · 𝑢)) < ((𝑄 / 2) · 𝑃))
233220rehalfcld 12220 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 / 2) ∈ ℝ)
234233, 131remulcld 11005 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 / 2) · 𝑃) ∈ ℝ)
235 lttr 11051 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑦 · 𝑃) ∈ ℝ ∧ (𝑄 · (2 · 𝑢)) ∈ ℝ ∧ ((𝑄 / 2) · 𝑃) ∈ ℝ) → (((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ∧ (𝑄 · (2 · 𝑢)) < ((𝑄 / 2) · 𝑃)) → (𝑦 · 𝑃) < ((𝑄 / 2) · 𝑃)))
236200, 204, 234, 235syl3anc 1370 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ∧ (𝑄 · (2 · 𝑢)) < ((𝑄 / 2) · 𝑃)) → (𝑦 · 𝑃) < ((𝑄 / 2) · 𝑃)))
237232, 236mpan2d 691 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) → (𝑦 · 𝑃) < ((𝑄 / 2) · 𝑃)))
238 ltmul1 11825 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑦 ∈ ℝ ∧ (𝑄 / 2) ∈ ℝ ∧ (𝑃 ∈ ℝ ∧ 0 < 𝑃)) → (𝑦 < (𝑄 / 2) ↔ (𝑦 · 𝑃) < ((𝑄 / 2) · 𝑃)))
239208, 233, 131, 209, 238syl112anc 1373 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 < (𝑄 / 2) ↔ (𝑦 · 𝑃) < ((𝑄 / 2) · 𝑃)))
240237, 239sylibrd 258 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) → 𝑦 < (𝑄 / 2)))
241 peano2rem 11288 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑄 ∈ ℝ → (𝑄 − 1) ∈ ℝ)
242220, 241syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 − 1) ∈ ℝ)
243242recnd 11003 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 − 1) ∈ ℂ)
244213, 243, 225, 227divsubdird 11790 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 − (𝑄 − 1)) / 2) = ((𝑄 / 2) − ((𝑄 − 1) / 2)))
245 lgsquad.5 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑁 = ((𝑄 − 1) / 2)
246245oveq2i 7286 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑄 / 2) − 𝑁) = ((𝑄 / 2) − ((𝑄 − 1) / 2))
247244, 246eqtr4di 2796 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 − (𝑄 − 1)) / 2) = ((𝑄 / 2) − 𝑁))
248 ax-1cn 10929 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 1 ∈ ℂ
249 nncan 11250 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑄 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑄 − (𝑄 − 1)) = 1)
250213, 248, 249sylancl 586 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 − (𝑄 − 1)) = 1)
251250oveq1d 7290 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 − (𝑄 − 1)) / 2) = (1 / 2))
252 halflt1 12191 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (1 / 2) < 1
253251, 252eqbrtrdi 5113 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 − (𝑄 − 1)) / 2) < 1)
254247, 253eqbrtrrd 5098 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 / 2) − 𝑁) < 1)
2552, 245gausslemma2dlem0b 26505 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝑁 ∈ ℕ)
256255ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑁 ∈ ℕ)
257256nnred 11988 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑁 ∈ ℝ)
258 1red 10976 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 1 ∈ ℝ)
259233, 257, 258ltsubadd2d 11573 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (((𝑄 / 2) − 𝑁) < 1 ↔ (𝑄 / 2) < (𝑁 + 1)))
260254, 259mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 / 2) < (𝑁 + 1))
261 peano2re 11148 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑁 ∈ ℝ → (𝑁 + 1) ∈ ℝ)
262257, 261syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑁 + 1) ∈ ℝ)
263 lttr 11051 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑦 ∈ ℝ ∧ (𝑄 / 2) ∈ ℝ ∧ (𝑁 + 1) ∈ ℝ) → ((𝑦 < (𝑄 / 2) ∧ (𝑄 / 2) < (𝑁 + 1)) → 𝑦 < (𝑁 + 1)))
264208, 233, 262, 263syl3anc 1370 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 < (𝑄 / 2) ∧ (𝑄 / 2) < (𝑁 + 1)) → 𝑦 < (𝑁 + 1)))
265260, 264mpan2d 691 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 < (𝑄 / 2) → 𝑦 < (𝑁 + 1)))
266240, 265syld 47 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) → 𝑦 < (𝑁 + 1)))
267 nnleltp1 12375 . . . . . . . . . . . . . . . . . . . . . . 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 13525 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ ∧ 𝑦 ∈ ℤ) → (𝑦 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)) ↔ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
273271, 190, 272syl2an 596 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)) ↔ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
274219, 270, 2733bitr3d 309 . . . . . . . . . . . . . . . . . . 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 12621 . . . . . . . . . . . . . . . . . . . . . . . 24 ℕ = (ℤ‘1)
280113, 279eleqtrdi 2849 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (2 · 𝑢) ∈ (ℤ‘1))
28124adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑀 ∈ ℤ)
282 elfz5 13248 . . . . . . . . . . . . . . . . . . . . . . 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 2839 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → 𝑥 ∈ (1...𝑀))
287286biantrurd 533 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (𝑦 ∈ (1...𝑁) ↔ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))))
288255nnzd 12425 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑁 ∈ ℤ)
289288ad2antrr 723 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → 𝑁 ∈ ℤ)
290 fznn 13324 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ ℤ → (𝑦 ∈ (1...𝑁) ↔ (𝑦 ∈ ℕ ∧ 𝑦𝑁)))
291289, 290syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (𝑦 ∈ (1...𝑁) ↔ (𝑦 ∈ ℕ ∧ 𝑦𝑁)))
292287, 291bitr3d 280 . . . . . . . . . . . . . . . . 17 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ↔ (𝑦 ∈ ℕ ∧ 𝑦𝑁)))
293 oveq1 7282 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (2 · 𝑢) → (𝑥 · 𝑄) = ((2 · 𝑢) · 𝑄))
294113nncnd 11989 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (2 · 𝑢) ∈ ℂ)
295201nncnd 11989 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑄 ∈ ℂ)
296294, 295mulcomd 10996 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((2 · 𝑢) · 𝑄) = (𝑄 · (2 · 𝑢)))
297293, 296sylan9eqr 2800 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (𝑥 · 𝑄) = (𝑄 · (2 · 𝑢)))
298297breq2d 5086 . . . . . . . . . . . . . . . . 17 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → ((𝑦 · 𝑃) < (𝑥 · 𝑄) ↔ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢))))
299292, 298anbi12d 631 . . . . . . . . . . . . . . . 16 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)) ↔ ((𝑦 ∈ ℕ ∧ 𝑦𝑁) ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)))))
300271flcld 13518 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ)
301 fznn 13324 . . . . . . . . . . . . . . . . . 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 311 . . . . . . . . . . . . . . 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 3436 . . . . . . . . . . . . . . . . . 18 𝑥 ∈ V
308 vex 3436 . . . . . . . . . . . . . . . . . 18 𝑦 ∈ V
309307, 308op1std 7841 . . . . . . . . . . . . . . . . 17 (𝑧 = ⟨𝑥, 𝑦⟩ → (1st𝑧) = 𝑥)
310309eqeq2d 2749 . . . . . . . . . . . . . . . 16 (𝑧 = ⟨𝑥, 𝑦⟩ → ((2 · 𝑢) = (1st𝑧) ↔ (2 · 𝑢) = 𝑥))
311 eqcom 2745 . . . . . . . . . . . . . . . 16 ((2 · 𝑢) = 𝑥𝑥 = (2 · 𝑢))
312310, 311bitrdi 287 . . . . . . . . . . . . . . 15 (𝑧 = ⟨𝑥, 𝑦⟩ → ((2 · 𝑢) = (1st𝑧) ↔ 𝑥 = (2 · 𝑢)))
313312elrab 3624 . . . . . . . . . . . . . 14 (⟨𝑥, 𝑦⟩ ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} ↔ (⟨𝑥, 𝑦⟩ ∈ 𝑆𝑥 = (2 · 𝑢)))
314313biancomi 463 . . . . . . . . . . . . 13 (⟨𝑥, 𝑦⟩ ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} ↔ (𝑥 = (2 · 𝑢) ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑆))
315 opelxp 5625 . . . . . . . . . . . . . 14 (⟨𝑥, 𝑦⟩ ∈ ({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ↔ (𝑥 ∈ {(2 · 𝑢)} ∧ 𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
316 velsn 4577 . . . . . . . . . . . . . . 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 314 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (⟨𝑥, 𝑦⟩ ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} ↔ ⟨𝑥, 𝑦⟩ ∈ ({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
320122, 123, 319eqrelrdv 5702 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} = ({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
321320eqcomd 2744 . . . . . . . . . 10 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)})
322321fveq2d 6778 . . . . . . . . 9 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (♯‘({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) = (♯‘{𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)}))
323 hashfz1 14060 . . . . . . . . . 10 ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℕ0 → (♯‘(1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))
32491, 323syl 17 . . . . . . . . 9 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (♯‘(1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))
325118, 322, 3243eqtr3rd 2787 . . . . . . . 8 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = (♯‘{𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)}))
326325sumeq2dv 15415 . . . . . . 7 (𝜑 → Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(♯‘{𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)}))
327101adantr 481 . . . . . . . . 9 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑆 ∈ Fin)
328 ssfi 8956 . . . . . . . . 9 ((𝑆 ∈ Fin ∧ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} ⊆ 𝑆) → {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} ∈ Fin)
329327, 119, 328sylancl 586 . . . . . . . 8 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} ∈ Fin)
330 fveq2 6774 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑣 → (1st𝑧) = (1st𝑣))
331330eqeq2d 2749 . . . . . . . . . . . . . . 15 (𝑧 = 𝑣 → ((2 · 𝑢) = (1st𝑧) ↔ (2 · 𝑢) = (1st𝑣)))
332331elrab 3624 . . . . . . . . . . . . . 14 (𝑣 ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} ↔ (𝑣𝑆 ∧ (2 · 𝑢) = (1st𝑣)))
333332simprbi 497 . . . . . . . . . . . . 13 (𝑣 ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} → (2 · 𝑢) = (1st𝑣))
334333ad2antll 726 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)})) → (2 · 𝑢) = (1st𝑣))
335334oveq1d 7290 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)})) → ((2 · 𝑢) / 2) = ((1st𝑣) / 2))
336144nncnd 11989 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ∈ ℂ)
337336adantrr 714 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)})) → 𝑢 ∈ ℂ)
338 2cnd 12051 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)})) → 2 ∈ ℂ)
339226a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)})) → 2 ≠ 0)
340337, 338, 339divcan3d 11756 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)})) → ((2 · 𝑢) / 2) = 𝑢)
341335, 340eqtr3d 2780 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)})) → ((1st𝑣) / 2) = 𝑢)
342341ralrimivva 3123 . . . . . . . . 9 (𝜑 → ∀𝑢 ∈ (1...(⌊‘(𝑀 / 2)))∀𝑣 ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} ((1st𝑣) / 2) = 𝑢)
343 invdisj 5058 . . . . . . . . 9 (∀𝑢 ∈ (1...(⌊‘(𝑀 / 2)))∀𝑣 ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} ((1st𝑣) / 2) = 𝑢Disj 𝑢 ∈ (1...(⌊‘(𝑀 / 2))){𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)})
344342, 343syl 17 . . . . . . . 8 (𝜑Disj 𝑢 ∈ (1...(⌊‘(𝑀 / 2))){𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)})
34587, 329, 344hashiun 15534 . . . . . . 7 (𝜑 → (♯‘ 𝑢 ∈ (1...(⌊‘(𝑀 / 2))){𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)}) = Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(♯‘{𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)}))
346 iunrab 4982 . . . . . . . . 9 𝑢 ∈ (1...(⌊‘(𝑀 / 2))){𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} = {𝑧𝑆 ∣ ∃𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(2 · 𝑢) = (1st𝑧)}
347 2cn 12048 . . . . . . . . . . . . . 14 2 ∈ ℂ
348 zcn 12324 . . . . . . . . . . . . . . 15 (𝑢 ∈ ℤ → 𝑢 ∈ ℂ)
349348adantl 482 . . . . . . . . . . . . . 14 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ ℤ) → 𝑢 ∈ ℂ)
350 mulcom 10957 . . . . . . . . . . . . . 14 ((2 ∈ ℂ ∧ 𝑢 ∈ ℂ) → (2 · 𝑢) = (𝑢 · 2))
351347, 349, 350sylancr 587 . . . . . . . . . . . . 13 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ ℤ) → (2 · 𝑢) = (𝑢 · 2))
352351eqeq1d 2740 . . . . . . . . . . . 12 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ ℤ) → ((2 · 𝑢) = (1st𝑧) ↔ (𝑢 · 2) = (1st𝑧)))
353352rexbidva 3225 . . . . . . . . . . 11 ((𝜑𝑧𝑆) → (∃𝑢 ∈ ℤ (2 · 𝑢) = (1st𝑧) ↔ ∃𝑢 ∈ ℤ (𝑢 · 2) = (1st𝑧)))
354138anim1i 615 . . . . . . . . . . . . 13 ((𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ (2 · 𝑢) = (1st𝑧)) → (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧)))
355354reximi2 3175 . . . . . . . . . . . 12 (∃𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(2 · 𝑢) = (1st𝑧) → ∃𝑢 ∈ ℤ (2 · 𝑢) = (1st𝑧))
356 simprr 770 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (2 · 𝑢) = (1st𝑧))
357 simpr 485 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑧𝑆) → 𝑧𝑆)
35899, 357sselid 3919 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑧𝑆) → 𝑧 ∈ ((1...𝑀) × (1...𝑁)))
359 xp1st 7863 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ ((1...𝑀) × (1...𝑁)) → (1st𝑧) ∈ (1...𝑀))
360358, 359syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑧𝑆) → (1st𝑧) ∈ (1...𝑀))
361360adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (1st𝑧) ∈ (1...𝑀))
362 elfzle2 13260 . . . . . . . . . . . . . . . . . . . 20 ((1st𝑧) ∈ (1...𝑀) → (1st𝑧) ≤ 𝑀)
363361, 362syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (1st𝑧) ≤ 𝑀)
364356, 363eqbrtrd 5096 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (2 · 𝑢) ≤ 𝑀)
365 zre 12323 . . . . . . . . . . . . . . . . . . . 20 (𝑢 ∈ ℤ → 𝑢 ∈ ℝ)
366365ad2antrl 725 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 𝑢 ∈ ℝ)
3679ad2antrr 723 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 𝑀 ∈ ℝ)
368146a1i 11 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 2 ∈ ℝ)
369148a1i 11 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 0 < 2)
370366, 367, 368, 369, 150syl112anc 1373 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → ((2 · 𝑢) ≤ 𝑀𝑢 ≤ (𝑀 / 2)))
371364, 370mpbid 231 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 𝑢 ≤ (𝑀 / 2))
37210ad2antrr 723 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (𝑀 / 2) ∈ ℝ)
373 simprl 768 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 𝑢 ∈ ℤ)
374372, 373, 140syl2anc 584 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (𝑢 ≤ (𝑀 / 2) ↔ 𝑢 ≤ (⌊‘(𝑀 / 2))))
375371, 374mpbid 231 . . . . . . . . . . . . . . . 16 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 𝑢 ≤ (⌊‘(𝑀 / 2)))
376 2t0e0 12142 . . . . . . . . . . . . . . . . . . . . 21 (2 · 0) = 0
377 elfznn 13285 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1st𝑧) ∈ (1...𝑀) → (1st𝑧) ∈ ℕ)
378361, 377syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (1st𝑧) ∈ ℕ)
379356, 378eqeltrd 2839 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (2 · 𝑢) ∈ ℕ)
380379nngt0d 12022 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 0 < (2 · 𝑢))
381376, 380eqbrtrid 5109 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (2 · 0) < (2 · 𝑢))
382 0red 10978 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 0 ∈ ℝ)
383 ltmul2 11826 . . . . . . . . . . . . . . . . . . . . 21 ((0 ∈ ℝ ∧ 𝑢 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (0 < 𝑢 ↔ (2 · 0) < (2 · 𝑢)))
384382, 366, 368, 369, 383syl112anc 1373 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (0 < 𝑢 ↔ (2 · 0) < (2 · 𝑢)))
385381, 384mpbird 256 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 0 < 𝑢)
386 elnnz 12329 . . . . . . . . . . . . . . . . . . 19 (𝑢 ∈ ℕ ↔ (𝑢 ∈ ℤ ∧ 0 < 𝑢))
387373, 385, 386sylanbrc 583 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 𝑢 ∈ ℕ)
388387, 279eleqtrdi 2849 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 𝑢 ∈ (ℤ‘1))
38911ad2antrr 723 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (⌊‘(𝑀 / 2)) ∈ ℤ)
390 elfz5 13248 . . . . . . . . . . . . . . . . 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 3199 . . . . . . . . . . . 12 ((𝜑𝑧𝑆) → (∃𝑢 ∈ ℤ (2 · 𝑢) = (1st𝑧) → ∃𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(2 · 𝑢) = (1st𝑧)))
396355, 395impbid2 225 . . . . . . . . . . 11 ((𝜑𝑧𝑆) → (∃𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(2 · 𝑢) = (1st𝑧) ↔ ∃𝑢 ∈ ℤ (2 · 𝑢) = (1st𝑧)))
397 2z 12352 . . . . . . . . . . . 12 2 ∈ ℤ
398360elfzelzd 13257 . . . . . . . . . . . 12 ((𝜑𝑧𝑆) → (1st𝑧) ∈ ℤ)
399 divides 15965 . . . . . . . . . . . 12 ((2 ∈ ℤ ∧ (1st𝑧) ∈ ℤ) → (2 ∥ (1st𝑧) ↔ ∃𝑢 ∈ ℤ (𝑢 · 2) = (1st𝑧)))
400397, 398, 399sylancr 587 . . . . . . . . . . 11 ((𝜑𝑧𝑆) → (2 ∥ (1st𝑧) ↔ ∃𝑢 ∈ ℤ (𝑢 · 2) = (1st𝑧)))
401353, 396, 4003bitr4d 311 . . . . . . . . . 10 ((𝜑𝑧𝑆) → (∃𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(2 · 𝑢) = (1st𝑧) ↔ 2 ∥ (1st𝑧)))
402401rabbidva 3413 . . . . . . . . 9 (𝜑 → {𝑧𝑆 ∣ ∃𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(2 · 𝑢) = (1st𝑧)} = {𝑧𝑆 ∣ 2 ∥ (1st𝑧)})
403346, 402eqtrid 2790 . . . . . . . 8 (𝜑 𝑢 ∈ (1...(⌊‘(𝑀 / 2))){𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} = {𝑧𝑆 ∣ 2 ∥ (1st𝑧)})
404403fveq2d 6778 . . . . . . 7 (𝜑 → (♯‘ 𝑢 ∈ (1...(⌊‘(𝑀 / 2))){𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)}) = (♯‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)}))
405326, 345, 4043eqtr2d 2784 . . . . . 6 (𝜑 → Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = (♯‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)}))
406405oveq2d 7291 . . . . 5 (𝜑 → (-1↑Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (-1↑(♯‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)})))
4071, 2, 3, 5, 245, 97lgsquadlem1 26528 . . . . 5 (𝜑 → (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})))
408406, 407oveq12d 7293 . . . 4 (𝜑 → ((-1↑Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) · (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = ((-1↑(♯‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)})) · (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))))
409112, 408eqtr4d 2781 . . 3 (𝜑 → (-1↑((♯‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)}) + (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))) = ((-1↑Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) · (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
410 inrab 4240 . . . . . . 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 3104 . . . . . . . 8 (𝜑 → ∀𝑧𝑆 ¬ (2 ∥ (1st𝑧) ∧ ¬ 2 ∥ (1st𝑧)))
414 rabeq0 4318 . . . . . . . 8 ({𝑧𝑆 ∣ (2 ∥ (1st𝑧) ∧ ¬ 2 ∥ (1st𝑧))} = ∅ ↔ ∀𝑧𝑆 ¬ (2 ∥ (1st𝑧) ∧ ¬ 2 ∥ (1st𝑧)))
415413, 414sylibr 233 . . . . . . 7 (𝜑 → {𝑧𝑆 ∣ (2 ∥ (1st𝑧) ∧ ¬ 2 ∥ (1st𝑧))} = ∅)
416410, 415eqtrid 2790 . . . . . 6 (𝜑 → ({𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∩ {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) = ∅)
417 hashun 14097 . . . . . 6 (({𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∈ Fin ∧ {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)} ∈ Fin ∧ ({𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∩ {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) = ∅) → (♯‘({𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∪ {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) = ((♯‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)}) + (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})))
418109, 104, 416, 417syl3anc 1370 . . . . 5 (𝜑 → (♯‘({𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∪ {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) = ((♯‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)}) + (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})))
419 unrab 4239 . . . . . . 7 ({𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∪ {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) = {𝑧𝑆 ∣ (2 ∥ (1st𝑧) ∨ ¬ 2 ∥ (1st𝑧))}
420 exmid 892 . . . . . . . . 9 (2 ∥ (1st𝑧) ∨ ¬ 2 ∥ (1st𝑧))
421420rgenw 3076 . . . . . . . 8 𝑧𝑆 (2 ∥ (1st𝑧) ∨ ¬ 2 ∥ (1st𝑧))
422 rabid2 3314 . . . . . . . 8 (𝑆 = {𝑧𝑆 ∣ (2 ∥ (1st𝑧) ∨ ¬ 2 ∥ (1st𝑧))} ↔ ∀𝑧𝑆 (2 ∥ (1st𝑧) ∨ ¬ 2 ∥ (1st𝑧)))
423421, 422mpbir 230 . . . . . . 7 𝑆 = {𝑧𝑆 ∣ (2 ∥ (1st𝑧) ∨ ¬ 2 ∥ (1st𝑧))}
424419, 423eqtr4i 2769 . . . . . 6 ({𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∪ {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) = 𝑆
425424fveq2i 6777 . . . . 5 (♯‘({𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∪ {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) = (♯‘𝑆)
426418, 425eqtr3di 2793 . . . 4 (𝜑 → ((♯‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)}) + (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) = (♯‘𝑆))
427426oveq2d 7291 . . 3 (𝜑 → (-1↑((♯‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)}) + (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))) = (-1↑(♯‘𝑆)))
42893, 409, 4273eqtr2d 2784 . 2 (𝜑 → (-1↑(Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = (-1↑(♯‘𝑆)))
4294, 78, 4283eqtrd 2782 1 (𝜑 → (𝑄 /L 𝑃) = (-1↑(♯‘𝑆)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 844  w3a 1086   = wceq 1539  wcel 2106  wne 2943  wral 3064  wrex 3065  {crab 3068  cdif 3884  cun 3885  cin 3886  wss 3887  c0 4256  {csn 4561  cop 4567   ciun 4924  Disj wdisj 5039   class class class wbr 5074  {copab 5136   × cxp 5587  Rel wrel 5594  cfv 6433  (class class class)co 7275  1st c1st 7829  cen 8730  Fincfn 8733  cc 10869  cr 10870  0cc0 10871  1c1 10872   + caddc 10874   · cmul 10876   < clt 11009  cle 11010  cmin 11205  -cneg 11206   / cdiv 11632  cn 11973  2c2 12028  0cn0 12233  cz 12319  cuz 12582  +crp 12730  ...cfz 13239  cfl 13510  cexp 13782  chash 14044  Σcsu 15397  cdvds 15963   gcd cgcd 16201  cprime 16376   /L clgs 26442
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-inf2 9399  ax-cnex 10927  ax-resscn 10928  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-addrcl 10932  ax-mulcl 10933  ax-mulrcl 10934  ax-mulcom 10935  ax-addass 10936  ax-mulass 10937  ax-distr 10938  ax-i2m1 10939  ax-1ne0 10940  ax-1rid 10941  ax-rnegex 10942  ax-rrecex 10943  ax-cnre 10944  ax-pre-lttri 10945  ax-pre-lttrn 10946  ax-pre-ltadd 10947  ax-pre-mulgt0 10948  ax-pre-sup 10949  ax-addf 10950  ax-mulf 10951
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-rmo 3071  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-tp 4566  df-op 4568  df-uni 4840  df-int 4880  df-iun 4926  df-disj 5040  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-se 5545  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-isom 6442  df-riota 7232  df-ov 7278  df-oprab 7279  df-mpo 7280  df-of 7533  df-om 7713  df-1st 7831  df-2nd 7832  df-supp 7978  df-tpos 8042  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-rdg 8241  df-1o 8297  df-2o 8298  df-oadd 8301  df-er 8498  df-ec 8500  df-qs 8504  df-map 8617  df-en 8734  df-dom 8735  df-sdom 8736  df-fin 8737  df-fsupp 9129  df-sup 9201  df-inf 9202  df-oi 9269  df-dju 9659  df-card 9697  df-pnf 11011  df-mnf 11012  df-xr 11013  df-ltxr 11014  df-le 11015  df-sub 11207  df-neg 11208  df-div 11633  df-nn 11974  df-2 12036  df-3 12037  df-4 12038  df-5 12039  df-6 12040  df-7 12041  df-8 12042  df-9 12043  df-n0 12234  df-xnn0 12306  df-z 12320  df-dec 12438  df-uz 12583  df-q 12689  df-rp 12731  df-fz 13240  df-fzo 13383  df-fl 13512  df-mod 13590  df-seq 13722  df-exp 13783  df-hash 14045  df-cj 14810  df-re 14811  df-im 14812  df-sqrt 14946  df-abs 14947  df-clim 15197  df-sum 15398  df-dvds 15964  df-gcd 16202  df-prm 16377  df-phi 16467  df-pc 16538  df-struct 16848  df-sets 16865  df-slot 16883  df-ndx 16895  df-base 16913  df-ress 16942  df-plusg 16975  df-mulr 16976  df-starv 16977  df-sca 16978  df-vsca 16979  df-ip 16980  df-tset 16981  df-ple 16982  df-ds 16984  df-unif 16985  df-0g 17152  df-gsum 17153  df-imas 17219  df-qus 17220  df-mgm 18326  df-sgrp 18375  df-mnd 18386  df-mhm 18430  df-submnd 18431  df-grp 18580  df-minusg 18581  df-sbg 18582  df-mulg 18701  df-subg 18752  df-nsg 18753  df-eqg 18754  df-ghm 18832  df-cntz 18923  df-cmn 19388  df-abl 19389  df-mgp 19721  df-ur 19738  df-ring 19785  df-cring 19786  df-oppr 19862  df-dvdsr 19883  df-unit 19884  df-invr 19914  df-dvr 19925  df-rnghom 19959  df-drng 19993  df-field 19994  df-subrg 20022  df-lmod 20125  df-lss 20194  df-lsp 20234  df-sra 20434  df-rgmod 20435  df-lidl 20436  df-rsp 20437  df-2idl 20503  df-nzr 20529  df-rlreg 20554  df-domn 20555  df-idom 20556  df-cnfld 20598  df-zring 20671  df-zrh 20705  df-zn 20708  df-lgs 26443
This theorem is referenced by:  lgsquadlem3  26530
  Copyright terms: Public domain W3C validator