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

Theorem lgsquadlem2 25320
Description: Lemma for lgsquad 25322. Count the members of 𝑆 with even coordinates, and combine with lgsquadlem1 25319 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 25318 . 2 (𝜑 → (𝑄 /L 𝑃) = (-1↑Σ𝑢 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
5 lgsquad.4 . . . . . 6 𝑀 = ((𝑃 − 1) / 2)
65oveq2i 6885 . . . . 5 (1...𝑀) = (1...((𝑃 − 1) / 2))
76sumeq1i 14651 . . . 4 Σ𝑢 ∈ (1...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = Σ𝑢 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))
8 oddprm 15732 . . . . . . . . . . . . 13 (𝑃 ∈ (ℙ ∖ {2}) → ((𝑃 − 1) / 2) ∈ ℕ)
91, 8syl 17 . . . . . . . . . . . 12 (𝜑 → ((𝑃 − 1) / 2) ∈ ℕ)
105, 9syl5eqel 2889 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℕ)
1110nnred 11320 . . . . . . . . . 10 (𝜑𝑀 ∈ ℝ)
1211rehalfcld 11546 . . . . . . . . 9 (𝜑 → (𝑀 / 2) ∈ ℝ)
1312flcld 12823 . . . . . . . 8 (𝜑 → (⌊‘(𝑀 / 2)) ∈ ℤ)
1413zred 11748 . . . . . . 7 (𝜑 → (⌊‘(𝑀 / 2)) ∈ ℝ)
1514ltp1d 11239 . . . . . 6 (𝜑 → (⌊‘(𝑀 / 2)) < ((⌊‘(𝑀 / 2)) + 1))
16 fzdisj 12591 . . . . . 6 ((⌊‘(𝑀 / 2)) < ((⌊‘(𝑀 / 2)) + 1) → ((1...(⌊‘(𝑀 / 2))) ∩ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) = ∅)
1715, 16syl 17 . . . . 5 (𝜑 → ((1...(⌊‘(𝑀 / 2))) ∩ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) = ∅)
1810nnrpd 12084 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℝ+)
1918rphalfcld 12098 . . . . . . . . . 10 (𝜑 → (𝑀 / 2) ∈ ℝ+)
2019rpge0d 12090 . . . . . . . . 9 (𝜑 → 0 ≤ (𝑀 / 2))
21 flge0nn0 12845 . . . . . . . . 9 (((𝑀 / 2) ∈ ℝ ∧ 0 ≤ (𝑀 / 2)) → (⌊‘(𝑀 / 2)) ∈ ℕ0)
2212, 20, 21syl2anc 575 . . . . . . . 8 (𝜑 → (⌊‘(𝑀 / 2)) ∈ ℕ0)
2310nnnn0d 11617 . . . . . . . 8 (𝜑𝑀 ∈ ℕ0)
24 rphalflt 12074 . . . . . . . . . . 11 (𝑀 ∈ ℝ+ → (𝑀 / 2) < 𝑀)
2518, 24syl 17 . . . . . . . . . 10 (𝜑 → (𝑀 / 2) < 𝑀)
2610nnzd 11747 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℤ)
27 fllt 12831 . . . . . . . . . . 11 (((𝑀 / 2) ∈ ℝ ∧ 𝑀 ∈ ℤ) → ((𝑀 / 2) < 𝑀 ↔ (⌊‘(𝑀 / 2)) < 𝑀))
2812, 26, 27syl2anc 575 . . . . . . . . . 10 (𝜑 → ((𝑀 / 2) < 𝑀 ↔ (⌊‘(𝑀 / 2)) < 𝑀))
2925, 28mpbid 223 . . . . . . . . 9 (𝜑 → (⌊‘(𝑀 / 2)) < 𝑀)
3014, 11, 29ltled 10470 . . . . . . . 8 (𝜑 → (⌊‘(𝑀 / 2)) ≤ 𝑀)
31 elfz2nn0 12654 . . . . . . . 8 ((⌊‘(𝑀 / 2)) ∈ (0...𝑀) ↔ ((⌊‘(𝑀 / 2)) ∈ ℕ0𝑀 ∈ ℕ0 ∧ (⌊‘(𝑀 / 2)) ≤ 𝑀))
3222, 23, 30, 31syl3anbrc 1436 . . . . . . 7 (𝜑 → (⌊‘(𝑀 / 2)) ∈ (0...𝑀))
33 nn0uz 11940 . . . . . . . . 9 0 = (ℤ‘0)
3423, 33syl6eleq 2895 . . . . . . . 8 (𝜑𝑀 ∈ (ℤ‘0))
35 elfzp12 12642 . . . . . . . 8 (𝑀 ∈ (ℤ‘0) → ((⌊‘(𝑀 / 2)) ∈ (0...𝑀) ↔ ((⌊‘(𝑀 / 2)) = 0 ∨ (⌊‘(𝑀 / 2)) ∈ ((0 + 1)...𝑀))))
3634, 35syl 17 . . . . . . 7 (𝜑 → ((⌊‘(𝑀 / 2)) ∈ (0...𝑀) ↔ ((⌊‘(𝑀 / 2)) = 0 ∨ (⌊‘(𝑀 / 2)) ∈ ((0 + 1)...𝑀))))
3732, 36mpbid 223 . . . . . 6 (𝜑 → ((⌊‘(𝑀 / 2)) = 0 ∨ (⌊‘(𝑀 / 2)) ∈ ((0 + 1)...𝑀)))
38 oveq2 6882 . . . . . . . . . 10 ((⌊‘(𝑀 / 2)) = 0 → (1...(⌊‘(𝑀 / 2))) = (1...0))
39 fz10 12585 . . . . . . . . . 10 (1...0) = ∅
4038, 39syl6eq 2856 . . . . . . . . 9 ((⌊‘(𝑀 / 2)) = 0 → (1...(⌊‘(𝑀 / 2))) = ∅)
41 oveq1 6881 . . . . . . . . . . 11 ((⌊‘(𝑀 / 2)) = 0 → ((⌊‘(𝑀 / 2)) + 1) = (0 + 1))
42 0p1e1 11414 . . . . . . . . . . 11 (0 + 1) = 1
4341, 42syl6eq 2856 . . . . . . . . . 10 ((⌊‘(𝑀 / 2)) = 0 → ((⌊‘(𝑀 / 2)) + 1) = 1)
4443oveq1d 6889 . . . . . . . . 9 ((⌊‘(𝑀 / 2)) = 0 → (((⌊‘(𝑀 / 2)) + 1)...𝑀) = (1...𝑀))
4540, 44uneq12d 3967 . . . . . . . 8 ((⌊‘(𝑀 / 2)) = 0 → ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) = (∅ ∪ (1...𝑀)))
46 un0 4165 . . . . . . . . 9 ((1...𝑀) ∪ ∅) = (1...𝑀)
47 uncom 3956 . . . . . . . . 9 ((1...𝑀) ∪ ∅) = (∅ ∪ (1...𝑀))
4846, 47eqtr3i 2830 . . . . . . . 8 (1...𝑀) = (∅ ∪ (1...𝑀))
4945, 48syl6reqr 2859 . . . . . . 7 ((⌊‘(𝑀 / 2)) = 0 → (1...𝑀) = ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀)))
50 fzsplit 12590 . . . . . . . 8 ((⌊‘(𝑀 / 2)) ∈ (1...𝑀) → (1...𝑀) = ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀)))
5142oveq1i 6884 . . . . . . . 8 ((0 + 1)...𝑀) = (1...𝑀)
5250, 51eleq2s 2903 . . . . . . 7 ((⌊‘(𝑀 / 2)) ∈ ((0 + 1)...𝑀) → (1...𝑀) = ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀)))
5349, 52jaoi 875 . . . . . 6 (((⌊‘(𝑀 / 2)) = 0 ∨ (⌊‘(𝑀 / 2)) ∈ ((0 + 1)...𝑀)) → (1...𝑀) = ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀)))
5437, 53syl 17 . . . . 5 (𝜑 → (1...𝑀) = ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀)))
55 fzfid 12996 . . . . 5 (𝜑 → (1...𝑀) ∈ Fin)
562eldifad 3781 . . . . . . . . . . . 12 (𝜑𝑄 ∈ ℙ)
57 prmnn 15606 . . . . . . . . . . . 12 (𝑄 ∈ ℙ → 𝑄 ∈ ℕ)
5856, 57syl 17 . . . . . . . . . . 11 (𝜑𝑄 ∈ ℕ)
5958nnred 11320 . . . . . . . . . 10 (𝜑𝑄 ∈ ℝ)
601eldifad 3781 . . . . . . . . . . 11 (𝜑𝑃 ∈ ℙ)
61 prmnn 15606 . . . . . . . . . . 11 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
6260, 61syl 17 . . . . . . . . . 10 (𝜑𝑃 ∈ ℕ)
6359, 62nndivred 11355 . . . . . . . . 9 (𝜑 → (𝑄 / 𝑃) ∈ ℝ)
6463adantr 468 . . . . . . . 8 ((𝜑𝑢 ∈ (1...𝑀)) → (𝑄 / 𝑃) ∈ ℝ)
65 2nn 11462 . . . . . . . . . 10 2 ∈ ℕ
66 elfznn 12593 . . . . . . . . . . 11 (𝑢 ∈ (1...𝑀) → 𝑢 ∈ ℕ)
6766adantl 469 . . . . . . . . . 10 ((𝜑𝑢 ∈ (1...𝑀)) → 𝑢 ∈ ℕ)
68 nnmulcl 11328 . . . . . . . . . 10 ((2 ∈ ℕ ∧ 𝑢 ∈ ℕ) → (2 · 𝑢) ∈ ℕ)
6965, 67, 68sylancr 577 . . . . . . . . 9 ((𝜑𝑢 ∈ (1...𝑀)) → (2 · 𝑢) ∈ ℕ)
7069nnred 11320 . . . . . . . 8 ((𝜑𝑢 ∈ (1...𝑀)) → (2 · 𝑢) ∈ ℝ)
7164, 70remulcld 10355 . . . . . . 7 ((𝜑𝑢 ∈ (1...𝑀)) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ)
7258nnrpd 12084 . . . . . . . . . . 11 (𝜑𝑄 ∈ ℝ+)
7362nnrpd 12084 . . . . . . . . . . 11 (𝜑𝑃 ∈ ℝ+)
7472, 73rpdivcld 12103 . . . . . . . . . 10 (𝜑 → (𝑄 / 𝑃) ∈ ℝ+)
7574adantr 468 . . . . . . . . 9 ((𝜑𝑢 ∈ (1...𝑀)) → (𝑄 / 𝑃) ∈ ℝ+)
7669nnrpd 12084 . . . . . . . . 9 ((𝜑𝑢 ∈ (1...𝑀)) → (2 · 𝑢) ∈ ℝ+)
7775, 76rpmulcld 12102 . . . . . . . 8 ((𝜑𝑢 ∈ (1...𝑀)) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ+)
7877rpge0d 12090 . . . . . . 7 ((𝜑𝑢 ∈ (1...𝑀)) → 0 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)))
79 flge0nn0 12845 . . . . . . 7 ((((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ ∧ 0 ≤ ((𝑄 / 𝑃) · (2 · 𝑢))) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℕ0)
8071, 78, 79syl2anc 575 . . . . . 6 ((𝜑𝑢 ∈ (1...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℕ0)
8180nn0cnd 11619 . . . . 5 ((𝜑𝑢 ∈ (1...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℂ)
8217, 54, 55, 81fsumsplit 14694 . . . 4 (𝜑 → Σ𝑢 ∈ (1...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = (Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
837, 82syl5eqr 2854 . . 3 (𝜑 → Σ𝑢 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = (Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
8483oveq2d 6890 . 2 (𝜑 → (-1↑Σ𝑢 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (-1↑(Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
85 neg1cn 11406 . . . . 5 -1 ∈ ℂ
8685a1i 11 . . . 4 (𝜑 → -1 ∈ ℂ)
87 fzfid 12996 . . . . 5 (𝜑 → (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∈ Fin)
88 ssun2 3976 . . . . . . . 8 (((⌊‘(𝑀 / 2)) + 1)...𝑀) ⊆ ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀))
8988, 54syl5sseqr 3851 . . . . . . 7 (𝜑 → (((⌊‘(𝑀 / 2)) + 1)...𝑀) ⊆ (1...𝑀))
9089sselda 3798 . . . . . 6 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ∈ (1...𝑀))
9190, 80syldan 581 . . . . 5 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℕ0)
9287, 91fsumnn0cl 14690 . . . 4 (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℕ0)
93 fzfid 12996 . . . . 5 (𝜑 → (1...(⌊‘(𝑀 / 2))) ∈ Fin)
94 ssun1 3975 . . . . . . . 8 (1...(⌊‘(𝑀 / 2))) ⊆ ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀))
9594, 54syl5sseqr 3851 . . . . . . 7 (𝜑 → (1...(⌊‘(𝑀 / 2))) ⊆ (1...𝑀))
9695sselda 3798 . . . . . 6 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ∈ (1...𝑀))
9796, 80syldan 581 . . . . 5 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℕ0)
9893, 97fsumnn0cl 14690 . . . 4 (𝜑 → Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℕ0)
9986, 92, 98expaddd 13233 . . 3 (𝜑 → (-1↑(Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = ((-1↑Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) · (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
100 fzfid 12996 . . . . . . . . 9 (𝜑 → (1...𝑁) ∈ Fin)
101 xpfi 8470 . . . . . . . . 9 (((1...𝑀) ∈ Fin ∧ (1...𝑁) ∈ Fin) → ((1...𝑀) × (1...𝑁)) ∈ Fin)
10255, 100, 101syl2anc 575 . . . . . . . 8 (𝜑 → ((1...𝑀) × (1...𝑁)) ∈ Fin)
103 lgsquad.6 . . . . . . . . 9 𝑆 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))}
104 opabssxp 5395 . . . . . . . . 9 {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} ⊆ ((1...𝑀) × (1...𝑁))
105103, 104eqsstri 3832 . . . . . . . 8 𝑆 ⊆ ((1...𝑀) × (1...𝑁))
106 ssfi 8419 . . . . . . . 8 ((((1...𝑀) × (1...𝑁)) ∈ Fin ∧ 𝑆 ⊆ ((1...𝑀) × (1...𝑁))) → 𝑆 ∈ Fin)
107102, 105, 106sylancl 576 . . . . . . 7 (𝜑𝑆 ∈ Fin)
108 ssrab2 3884 . . . . . . 7 {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)} ⊆ 𝑆
109 ssfi 8419 . . . . . . 7 ((𝑆 ∈ Fin ∧ {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)} ⊆ 𝑆) → {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)} ∈ Fin)
110107, 108, 109sylancl 576 . . . . . 6 (𝜑 → {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)} ∈ Fin)
111 hashcl 13365 . . . . . 6 ({𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)} ∈ Fin → (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) ∈ ℕ0)
112110, 111syl 17 . . . . 5 (𝜑 → (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) ∈ ℕ0)
113 ssrab2 3884 . . . . . . 7 {𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ⊆ 𝑆
114 ssfi 8419 . . . . . . 7 ((𝑆 ∈ Fin ∧ {𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ⊆ 𝑆) → {𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∈ Fin)
115107, 113, 114sylancl 576 . . . . . 6 (𝜑 → {𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∈ Fin)
116 hashcl 13365 . . . . . 6 ({𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∈ Fin → (♯‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)}) ∈ ℕ0)
117115, 116syl 17 . . . . 5 (𝜑 → (♯‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)}) ∈ ℕ0)
11886, 112, 117expaddd 13233 . . . 4 (𝜑 → (-1↑((♯‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)}) + (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))) = ((-1↑(♯‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)})) · (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))))
11996, 69syldan 581 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (2 · 𝑢) ∈ ℕ)
120 fzfid 12996 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ Fin)
121 xpsnen2g 8292 . . . . . . . . . . 11 (((2 · 𝑢) ∈ ℕ ∧ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ Fin) → ({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ≈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
122119, 120, 121syl2anc 575 . . . . . . . . . 10 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ≈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
123 hasheni 13356 . . . . . . . . . 10 (({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ≈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) → (♯‘({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) = (♯‘(1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
124122, 123syl 17 . . . . . . . . 9 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (♯‘({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) = (♯‘(1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
125 ssrab2 3884 . . . . . . . . . . . . 13 {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} ⊆ 𝑆
126103relopabi 5447 . . . . . . . . . . . . 13 Rel 𝑆
127 relss 5408 . . . . . . . . . . . . 13 ({𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} ⊆ 𝑆 → (Rel 𝑆 → Rel {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)}))
128125, 126, 127mp2 9 . . . . . . . . . . . 12 Rel {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)}
129 relxp 5328 . . . . . . . . . . . 12 Rel ({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
130103eleq2i 2877 . . . . . . . . . . . . . . . 16 (⟨𝑥, 𝑦⟩ ∈ 𝑆 ↔ ⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))})
131 opabid 5177 . . . . . . . . . . . . . . . 16 (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} ↔ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))
132130, 131bitri 266 . . . . . . . . . . . . . . 15 (⟨𝑥, 𝑦⟩ ∈ 𝑆 ↔ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))
133 anass 456 . . . . . . . . . . . . . . . . . 18 (((𝑦 ∈ ℕ ∧ 𝑦𝑁) ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢))) ↔ (𝑦 ∈ ℕ ∧ (𝑦𝑁 ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)))))
134 simpr 473 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ ℕ)
13562ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℕ)
136134, 135nnmulcld 11354 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 · 𝑃) ∈ ℕ)
137136nnred 11320 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 · 𝑃) ∈ ℝ)
13858adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑄 ∈ ℕ)
139138, 119nnmulcld 11354 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (𝑄 · (2 · 𝑢)) ∈ ℕ)
140139adantr 468 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (2 · 𝑢)) ∈ ℕ)
141140nnred 11320 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (2 · 𝑢)) ∈ ℝ)
142137, 141ltlend 10467 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ↔ ((𝑦 · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ∧ (𝑄 · (2 · 𝑢)) ≠ (𝑦 · 𝑃))))
143119adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2 · 𝑢) ∈ ℕ)
144143nnred 11320 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2 · 𝑢) ∈ ℝ)
145135nnred 11320 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℝ)
146145rehalfcld 11546 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 / 2) ∈ ℝ)
14711adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑀 ∈ ℝ)
148147adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑀 ∈ ℝ)
149 elfzle2 12568 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) → 𝑢 ≤ (⌊‘(𝑀 / 2)))
150149adantl 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ≤ (⌊‘(𝑀 / 2)))
151147rehalfcld 11546 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (𝑀 / 2) ∈ ℝ)
152 elfzelz 12565 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) → 𝑢 ∈ ℤ)
153152adantl 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ∈ ℤ)
154 flge 12830 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑀 / 2) ∈ ℝ ∧ 𝑢 ∈ ℤ) → (𝑢 ≤ (𝑀 / 2) ↔ 𝑢 ≤ (⌊‘(𝑀 / 2))))
155151, 153, 154syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (𝑢 ≤ (𝑀 / 2) ↔ 𝑢 ≤ (⌊‘(𝑀 / 2))))
156150, 155mpbird 248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ≤ (𝑀 / 2))
157 elfznn 12593 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) → 𝑢 ∈ ℕ)
158157adantl 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ∈ ℕ)
159158nnred 11320 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ∈ ℝ)
160 2re 11374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 2 ∈ ℝ
161160a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 2 ∈ ℝ)
162 2pos 11395 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 0 < 2
163162a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 0 < 2)
164 lemuldiv2 11189 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑢 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 𝑢) ≤ 𝑀𝑢 ≤ (𝑀 / 2)))
165159, 147, 161, 163, 164syl112anc 1486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((2 · 𝑢) ≤ 𝑀𝑢 ≤ (𝑀 / 2)))
166156, 165mpbird 248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (2 · 𝑢) ≤ 𝑀)
167166adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2 · 𝑢) ≤ 𝑀)
168145ltm1d 11241 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 − 1) < 𝑃)
169 peano2rem 10633 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑃 ∈ ℝ → (𝑃 − 1) ∈ ℝ)
170145, 169syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 − 1) ∈ ℝ)
171160a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 2 ∈ ℝ)
172162a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 0 < 2)
173 ltdiv1 11172 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑃 − 1) ∈ ℝ ∧ 𝑃 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((𝑃 − 1) < 𝑃 ↔ ((𝑃 − 1) / 2) < (𝑃 / 2)))
174170, 145, 171, 172, 173syl112anc 1486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑃 − 1) < 𝑃 ↔ ((𝑃 − 1) / 2) < (𝑃 / 2)))
175168, 174mpbid 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑃 − 1) / 2) < (𝑃 / 2))
1765, 175syl5eqbr 4879 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑀 < (𝑃 / 2))
177144, 148, 146, 167, 176lelttrd 10480 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2 · 𝑢) < (𝑃 / 2))
178135nnrpd 12084 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℝ+)
179 rphalflt 12074 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑃 ∈ ℝ+ → (𝑃 / 2) < 𝑃)
180178, 179syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 / 2) < 𝑃)
181144, 146, 145, 177, 180lttrd 10483 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2 · 𝑢) < 𝑃)
182144, 145ltnled 10469 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((2 · 𝑢) < 𝑃 ↔ ¬ 𝑃 ≤ (2 · 𝑢)))
183181, 182mpbid 223 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ¬ 𝑃 ≤ (2 · 𝑢))
18460ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℙ)
185 prmz 15607 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
186184, 185syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℤ)
187 dvdsle 15255 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑃 ∈ ℤ ∧ (2 · 𝑢) ∈ ℕ) → (𝑃 ∥ (2 · 𝑢) → 𝑃 ≤ (2 · 𝑢)))
188186, 143, 187syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 ∥ (2 · 𝑢) → 𝑃 ≤ (2 · 𝑢)))
189183, 188mtod 189 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ¬ 𝑃 ∥ (2 · 𝑢))
190 prmrp 15641 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ) → ((𝑃 gcd 𝑄) = 1 ↔ 𝑃𝑄))
19160, 56, 190syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → ((𝑃 gcd 𝑄) = 1 ↔ 𝑃𝑄))
1923, 191mpbird 248 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝑃 gcd 𝑄) = 1)
193192ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 gcd 𝑄) = 1)
19456ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈ ℙ)
195 prmz 15607 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑄 ∈ ℙ → 𝑄 ∈ ℤ)
196194, 195syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈ ℤ)
197143nnzd 11747 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2 · 𝑢) ∈ ℤ)
198 coprmdvds 15585 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑃 ∈ ℤ ∧ 𝑄 ∈ ℤ ∧ (2 · 𝑢) ∈ ℤ) → ((𝑃 ∥ (𝑄 · (2 · 𝑢)) ∧ (𝑃 gcd 𝑄) = 1) → 𝑃 ∥ (2 · 𝑢)))
199186, 196, 197, 198syl3anc 1483 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑃 ∥ (𝑄 · (2 · 𝑢)) ∧ (𝑃 gcd 𝑄) = 1) → 𝑃 ∥ (2 · 𝑢)))
200193, 199mpan2d 677 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 ∥ (𝑄 · (2 · 𝑢)) → 𝑃 ∥ (2 · 𝑢)))
201189, 200mtod 189 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ¬ 𝑃 ∥ (𝑄 · (2 · 𝑢)))
202 nnz 11665 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 ∈ ℕ → 𝑦 ∈ ℤ)
203202adantl 469 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ ℤ)
204 dvdsmul2 15227 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦 ∈ ℤ ∧ 𝑃 ∈ ℤ) → 𝑃 ∥ (𝑦 · 𝑃))
205203, 186, 204syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∥ (𝑦 · 𝑃))
206 breq2 4848 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑄 · (2 · 𝑢)) = (𝑦 · 𝑃) → (𝑃 ∥ (𝑄 · (2 · 𝑢)) ↔ 𝑃 ∥ (𝑦 · 𝑃)))
207205, 206syl5ibrcom 238 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 · (2 · 𝑢)) = (𝑦 · 𝑃) → 𝑃 ∥ (𝑄 · (2 · 𝑢))))
208207necon3bd 2992 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (¬ 𝑃 ∥ (𝑄 · (2 · 𝑢)) → (𝑄 · (2 · 𝑢)) ≠ (𝑦 · 𝑃)))
209201, 208mpd 15 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (2 · 𝑢)) ≠ (𝑦 · 𝑃))
210209biantrud 523 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ↔ ((𝑦 · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ∧ (𝑄 · (2 · 𝑢)) ≠ (𝑦 · 𝑃))))
211142, 210bitr4d 273 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ↔ (𝑦 · 𝑃) ≤ (𝑄 · (2 · 𝑢))))
212 nnre 11312 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
213212adantl 469 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ ℝ)
214135nngt0d 11350 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 0 < 𝑃)
215 lemuldiv 11188 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 ∈ ℝ ∧ (𝑄 · (2 · 𝑢)) ∈ ℝ ∧ (𝑃 ∈ ℝ ∧ 0 < 𝑃)) → ((𝑦 · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ↔ 𝑦 ≤ ((𝑄 · (2 · 𝑢)) / 𝑃)))
216213, 141, 145, 214, 215syl112anc 1486 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ↔ 𝑦 ≤ ((𝑄 · (2 · 𝑢)) / 𝑃)))
217138adantr 468 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈ ℕ)
218217nncnd 11321 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈ ℂ)
219143nncnd 11321 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2 · 𝑢) ∈ ℂ)
220135nncnd 11321 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℂ)
221135nnne0d 11351 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ≠ 0)
222218, 219, 220, 221div23d 11123 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 · (2 · 𝑢)) / 𝑃) = ((𝑄 / 𝑃) · (2 · 𝑢)))
223222breq2d 4856 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 ≤ ((𝑄 · (2 · 𝑢)) / 𝑃) ↔ 𝑦 ≤ ((𝑄 / 𝑃) · (2 · 𝑢))))
224211, 216, 2233bitrd 296 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ↔ 𝑦 ≤ ((𝑄 / 𝑃) · (2 · 𝑢))))
225217nnred 11320 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈ ℝ)
226217nngt0d 11350 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 0 < 𝑄)
227 ltmul2 11159 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((2 · 𝑢) ∈ ℝ ∧ (𝑃 / 2) ∈ ℝ ∧ (𝑄 ∈ ℝ ∧ 0 < 𝑄)) → ((2 · 𝑢) < (𝑃 / 2) ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · (𝑃 / 2))))
228144, 146, 225, 226, 227syl112anc 1486 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((2 · 𝑢) < (𝑃 / 2) ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · (𝑃 / 2))))
229177, 228mpbid 223 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (2 · 𝑢)) < (𝑄 · (𝑃 / 2)))
230 2cnd 11377 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 2 ∈ ℂ)
231 2ne0 11396 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 2 ≠ 0
232231a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 2 ≠ 0)
233 divass 10988 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑄 ∈ ℂ ∧ 𝑃 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((𝑄 · 𝑃) / 2) = (𝑄 · (𝑃 / 2)))
234 div23 10989 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑄 ∈ ℂ ∧ 𝑃 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((𝑄 · 𝑃) / 2) = ((𝑄 / 2) · 𝑃))
235233, 234eqtr3d 2842 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑄 ∈ ℂ ∧ 𝑃 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (𝑄 · (𝑃 / 2)) = ((𝑄 / 2) · 𝑃))
236218, 220, 230, 232, 235syl112anc 1486 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (𝑃 / 2)) = ((𝑄 / 2) · 𝑃))
237229, 236breqtrd 4870 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (2 · 𝑢)) < ((𝑄 / 2) · 𝑃))
238225rehalfcld 11546 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 / 2) ∈ ℝ)
239238, 145remulcld 10355 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 / 2) · 𝑃) ∈ ℝ)
240 lttr 10399 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑦 · 𝑃) ∈ ℝ ∧ (𝑄 · (2 · 𝑢)) ∈ ℝ ∧ ((𝑄 / 2) · 𝑃) ∈ ℝ) → (((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ∧ (𝑄 · (2 · 𝑢)) < ((𝑄 / 2) · 𝑃)) → (𝑦 · 𝑃) < ((𝑄 / 2) · 𝑃)))
241137, 141, 239, 240syl3anc 1483 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ∧ (𝑄 · (2 · 𝑢)) < ((𝑄 / 2) · 𝑃)) → (𝑦 · 𝑃) < ((𝑄 / 2) · 𝑃)))
242237, 241mpan2d 677 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) → (𝑦 · 𝑃) < ((𝑄 / 2) · 𝑃)))
243 ltmul1 11158 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑦 ∈ ℝ ∧ (𝑄 / 2) ∈ ℝ ∧ (𝑃 ∈ ℝ ∧ 0 < 𝑃)) → (𝑦 < (𝑄 / 2) ↔ (𝑦 · 𝑃) < ((𝑄 / 2) · 𝑃)))
244213, 238, 145, 214, 243syl112anc 1486 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 < (𝑄 / 2) ↔ (𝑦 · 𝑃) < ((𝑄 / 2) · 𝑃)))
245242, 244sylibrd 250 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) → 𝑦 < (𝑄 / 2)))
246 peano2rem 10633 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑄 ∈ ℝ → (𝑄 − 1) ∈ ℝ)
247225, 246syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 − 1) ∈ ℝ)
248247recnd 10353 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 − 1) ∈ ℂ)
249218, 248, 230, 232divsubdird 11125 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 − (𝑄 − 1)) / 2) = ((𝑄 / 2) − ((𝑄 − 1) / 2)))
250 lgsquad.5 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑁 = ((𝑄 − 1) / 2)
251250oveq2i 6885 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑄 / 2) − 𝑁) = ((𝑄 / 2) − ((𝑄 − 1) / 2))
252249, 251syl6eqr 2858 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 − (𝑄 − 1)) / 2) = ((𝑄 / 2) − 𝑁))
253 ax-1cn 10279 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 1 ∈ ℂ
254 nncan 10595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑄 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑄 − (𝑄 − 1)) = 1)
255218, 253, 254sylancl 576 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 − (𝑄 − 1)) = 1)
256255oveq1d 6889 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 − (𝑄 − 1)) / 2) = (1 / 2))
257 halflt1 11517 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (1 / 2) < 1
258256, 257syl6eqbr 4883 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 − (𝑄 − 1)) / 2) < 1)
259252, 258eqbrtrrd 4868 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 / 2) − 𝑁) < 1)
260 oddprm 15732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑄 ∈ (ℙ ∖ {2}) → ((𝑄 − 1) / 2) ∈ ℕ)
2612, 260syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → ((𝑄 − 1) / 2) ∈ ℕ)
262250, 261syl5eqel 2889 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝑁 ∈ ℕ)
263262ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑁 ∈ ℕ)
264263nnred 11320 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑁 ∈ ℝ)
265 1red 10326 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 1 ∈ ℝ)
266238, 264, 265ltsubadd2d 10910 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (((𝑄 / 2) − 𝑁) < 1 ↔ (𝑄 / 2) < (𝑁 + 1)))
267259, 266mpbid 223 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 / 2) < (𝑁 + 1))
268 peano2re 10494 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑁 ∈ ℝ → (𝑁 + 1) ∈ ℝ)
269264, 268syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑁 + 1) ∈ ℝ)
270 lttr 10399 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑦 ∈ ℝ ∧ (𝑄 / 2) ∈ ℝ ∧ (𝑁 + 1) ∈ ℝ) → ((𝑦 < (𝑄 / 2) ∧ (𝑄 / 2) < (𝑁 + 1)) → 𝑦 < (𝑁 + 1)))
271213, 238, 269, 270syl3anc 1483 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 < (𝑄 / 2) ∧ (𝑄 / 2) < (𝑁 + 1)) → 𝑦 < (𝑁 + 1)))
272267, 271mpan2d 677 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 < (𝑄 / 2) → 𝑦 < (𝑁 + 1)))
273245, 272syld 47 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) → 𝑦 < (𝑁 + 1)))
274 nnleltp1 11698 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑦𝑁𝑦 < (𝑁 + 1)))
275134, 263, 274syl2anc 575 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦𝑁𝑦 < (𝑁 + 1)))
276273, 275sylibrd 250 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) → 𝑦𝑁))
277276pm4.71rd 554 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ↔ (𝑦𝑁 ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)))))
27896, 71syldan 581 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ)
279 flge 12830 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ ∧ 𝑦 ∈ ℤ) → (𝑦 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)) ↔ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
280278, 202, 279syl2an 585 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)) ↔ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
281224, 277, 2803bitr3d 300 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦𝑁 ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢))) ↔ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
282281pm5.32da 570 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((𝑦 ∈ ℕ ∧ (𝑦𝑁 ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
283133, 282syl5bb 274 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (((𝑦 ∈ ℕ ∧ 𝑦𝑁) ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
284283adantr 468 . . . . . . . . . . . . . . . 16 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (((𝑦 ∈ ℕ ∧ 𝑦𝑁) ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
285 simpr 473 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → 𝑥 = (2 · 𝑢))
286 nnuz 11941 . . . . . . . . . . . . . . . . . . . . . . . 24 ℕ = (ℤ‘1)
287119, 286syl6eleq 2895 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (2 · 𝑢) ∈ (ℤ‘1))
28826adantr 468 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑀 ∈ ℤ)
289 elfz5 12557 . . . . . . . . . . . . . . . . . . . . . . 23 (((2 · 𝑢) ∈ (ℤ‘1) ∧ 𝑀 ∈ ℤ) → ((2 · 𝑢) ∈ (1...𝑀) ↔ (2 · 𝑢) ≤ 𝑀))
290287, 288, 289syl2anc 575 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((2 · 𝑢) ∈ (1...𝑀) ↔ (2 · 𝑢) ≤ 𝑀))
291166, 290mpbird 248 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (2 · 𝑢) ∈ (1...𝑀))
292291adantr 468 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (2 · 𝑢) ∈ (1...𝑀))
293285, 292eqeltrd 2885 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → 𝑥 ∈ (1...𝑀))
294293biantrurd 524 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (𝑦 ∈ (1...𝑁) ↔ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))))
295262nnzd 11747 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑁 ∈ ℤ)
296295ad2antrr 708 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → 𝑁 ∈ ℤ)
297 fznn 12631 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ ℤ → (𝑦 ∈ (1...𝑁) ↔ (𝑦 ∈ ℕ ∧ 𝑦𝑁)))
298296, 297syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (𝑦 ∈ (1...𝑁) ↔ (𝑦 ∈ ℕ ∧ 𝑦𝑁)))
299294, 298bitr3d 272 . . . . . . . . . . . . . . . . 17 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ↔ (𝑦 ∈ ℕ ∧ 𝑦𝑁)))
300 oveq1 6881 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (2 · 𝑢) → (𝑥 · 𝑄) = ((2 · 𝑢) · 𝑄))
301119nncnd 11321 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (2 · 𝑢) ∈ ℂ)
302138nncnd 11321 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑄 ∈ ℂ)
303301, 302mulcomd 10346 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((2 · 𝑢) · 𝑄) = (𝑄 · (2 · 𝑢)))
304300, 303sylan9eqr 2862 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (𝑥 · 𝑄) = (𝑄 · (2 · 𝑢)))
305304breq2d 4856 . . . . . . . . . . . . . . . . 17 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → ((𝑦 · 𝑃) < (𝑥 · 𝑄) ↔ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢))))
306299, 305anbi12d 618 . . . . . . . . . . . . . . . 16 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)) ↔ ((𝑦 ∈ ℕ ∧ 𝑦𝑁) ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)))))
307278flcld 12823 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ)
308 fznn 12631 . . . . . . . . . . . . . . . . . 18 ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ → (𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
309307, 308syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
310309adantr 468 . . . . . . . . . . . . . . . 16 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
311284, 306, 3103bitr4d 302 . . . . . . . . . . . . . . 15 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)) ↔ 𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
312132, 311syl5bb 274 . . . . . . . . . . . . . 14 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (⟨𝑥, 𝑦⟩ ∈ 𝑆𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
313312pm5.32da 570 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((𝑥 = (2 · 𝑢) ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑆) ↔ (𝑥 = (2 · 𝑢) ∧ 𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
314 vex 3394 . . . . . . . . . . . . . . . . . 18 𝑥 ∈ V
315 vex 3394 . . . . . . . . . . . . . . . . . 18 𝑦 ∈ V
316314, 315op1std 7408 . . . . . . . . . . . . . . . . 17 (𝑧 = ⟨𝑥, 𝑦⟩ → (1st𝑧) = 𝑥)
317316eqeq2d 2816 . . . . . . . . . . . . . . . 16 (𝑧 = ⟨𝑥, 𝑦⟩ → ((2 · 𝑢) = (1st𝑧) ↔ (2 · 𝑢) = 𝑥))
318 eqcom 2813 . . . . . . . . . . . . . . . 16 ((2 · 𝑢) = 𝑥𝑥 = (2 · 𝑢))
319317, 318syl6bb 278 . . . . . . . . . . . . . . 15 (𝑧 = ⟨𝑥, 𝑦⟩ → ((2 · 𝑢) = (1st𝑧) ↔ 𝑥 = (2 · 𝑢)))
320319elrab 3559 . . . . . . . . . . . . . 14 (⟨𝑥, 𝑦⟩ ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} ↔ (⟨𝑥, 𝑦⟩ ∈ 𝑆𝑥 = (2 · 𝑢)))
321 ancom 450 . . . . . . . . . . . . . 14 ((⟨𝑥, 𝑦⟩ ∈ 𝑆𝑥 = (2 · 𝑢)) ↔ (𝑥 = (2 · 𝑢) ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑆))
322320, 321bitri 266 . . . . . . . . . . . . 13 (⟨𝑥, 𝑦⟩ ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} ↔ (𝑥 = (2 · 𝑢) ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑆))
323 opelxp 5346 . . . . . . . . . . . . . 14 (⟨𝑥, 𝑦⟩ ∈ ({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ↔ (𝑥 ∈ {(2 · 𝑢)} ∧ 𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
324 velsn 4386 . . . . . . . . . . . . . . 15 (𝑥 ∈ {(2 · 𝑢)} ↔ 𝑥 = (2 · 𝑢))
325324anbi1i 612 . . . . . . . . . . . . . 14 ((𝑥 ∈ {(2 · 𝑢)} ∧ 𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ↔ (𝑥 = (2 · 𝑢) ∧ 𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
326323, 325bitri 266 . . . . . . . . . . . . 13 (⟨𝑥, 𝑦⟩ ∈ ({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ↔ (𝑥 = (2 · 𝑢) ∧ 𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
327313, 322, 3263bitr4g 305 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (⟨𝑥, 𝑦⟩ ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} ↔ ⟨𝑥, 𝑦⟩ ∈ ({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
328128, 129, 327eqrelrdv 5418 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} = ({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
329328eqcomd 2812 . . . . . . . . . 10 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)})
330329fveq2d 6412 . . . . . . . . 9 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (♯‘({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) = (♯‘{𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)}))
331 hashfz1 13354 . . . . . . . . . 10 ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℕ0 → (♯‘(1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))
33297, 331syl 17 . . . . . . . . 9 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (♯‘(1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))
333124, 330, 3323eqtr3rd 2849 . . . . . . . 8 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = (♯‘{𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)}))
334333sumeq2dv 14656 . . . . . . 7 (𝜑 → Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(♯‘{𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)}))
335107adantr 468 . . . . . . . . 9 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑆 ∈ Fin)
336 ssfi 8419 . . . . . . . . 9 ((𝑆 ∈ Fin ∧ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} ⊆ 𝑆) → {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} ∈ Fin)
337335, 125, 336sylancl 576 . . . . . . . 8 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} ∈ Fin)
338 fveq2 6408 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑣 → (1st𝑧) = (1st𝑣))
339338eqeq2d 2816 . . . . . . . . . . . . . . 15 (𝑧 = 𝑣 → ((2 · 𝑢) = (1st𝑧) ↔ (2 · 𝑢) = (1st𝑣)))
340339elrab 3559 . . . . . . . . . . . . . 14 (𝑣 ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} ↔ (𝑣𝑆 ∧ (2 · 𝑢) = (1st𝑣)))
341340simprbi 486 . . . . . . . . . . . . 13 (𝑣 ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} → (2 · 𝑢) = (1st𝑣))
342341ad2antll 711 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)})) → (2 · 𝑢) = (1st𝑣))
343342oveq1d 6889 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)})) → ((2 · 𝑢) / 2) = ((1st𝑣) / 2))
344158nncnd 11321 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ∈ ℂ)
345344adantrr 699 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)})) → 𝑢 ∈ ℂ)
346 2cnd 11377 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)})) → 2 ∈ ℂ)
347231a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)})) → 2 ≠ 0)
348345, 346, 347divcan3d 11091 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)})) → ((2 · 𝑢) / 2) = 𝑢)
349343, 348eqtr3d 2842 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)})) → ((1st𝑣) / 2) = 𝑢)
350349ralrimivva 3159 . . . . . . . . 9 (𝜑 → ∀𝑢 ∈ (1...(⌊‘(𝑀 / 2)))∀𝑣 ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} ((1st𝑣) / 2) = 𝑢)
351 invdisj 4830 . . . . . . . . 9 (∀𝑢 ∈ (1...(⌊‘(𝑀 / 2)))∀𝑣 ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} ((1st𝑣) / 2) = 𝑢Disj 𝑢 ∈ (1...(⌊‘(𝑀 / 2))){𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)})
352350, 351syl 17 . . . . . . . 8 (𝜑Disj 𝑢 ∈ (1...(⌊‘(𝑀 / 2))){𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)})
35393, 337, 352hashiun 14776 . . . . . . 7 (𝜑 → (♯‘ 𝑢 ∈ (1...(⌊‘(𝑀 / 2))){𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)}) = Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(♯‘{𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)}))
354 iunrab 4759 . . . . . . . . 9 𝑢 ∈ (1...(⌊‘(𝑀 / 2))){𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} = {𝑧𝑆 ∣ ∃𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(2 · 𝑢) = (1st𝑧)}
355 2cn 11375 . . . . . . . . . . . . . 14 2 ∈ ℂ
356 zcn 11648 . . . . . . . . . . . . . . 15 (𝑢 ∈ ℤ → 𝑢 ∈ ℂ)
357356adantl 469 . . . . . . . . . . . . . 14 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ ℤ) → 𝑢 ∈ ℂ)
358 mulcom 10307 . . . . . . . . . . . . . 14 ((2 ∈ ℂ ∧ 𝑢 ∈ ℂ) → (2 · 𝑢) = (𝑢 · 2))
359355, 357, 358sylancr 577 . . . . . . . . . . . . 13 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ ℤ) → (2 · 𝑢) = (𝑢 · 2))
360359eqeq1d 2808 . . . . . . . . . . . 12 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ ℤ) → ((2 · 𝑢) = (1st𝑧) ↔ (𝑢 · 2) = (1st𝑧)))
361360rexbidva 3237 . . . . . . . . . . 11 ((𝜑𝑧𝑆) → (∃𝑢 ∈ ℤ (2 · 𝑢) = (1st𝑧) ↔ ∃𝑢 ∈ ℤ (𝑢 · 2) = (1st𝑧)))
362152anim1i 604 . . . . . . . . . . . . 13 ((𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ (2 · 𝑢) = (1st𝑧)) → (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧)))
363362reximi2 3197 . . . . . . . . . . . 12 (∃𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(2 · 𝑢) = (1st𝑧) → ∃𝑢 ∈ ℤ (2 · 𝑢) = (1st𝑧))
364 simprr 780 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (2 · 𝑢) = (1st𝑧))
365 simpr 473 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑧𝑆) → 𝑧𝑆)
366105, 365sseldi 3796 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑧𝑆) → 𝑧 ∈ ((1...𝑀) × (1...𝑁)))
367 xp1st 7430 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ ((1...𝑀) × (1...𝑁)) → (1st𝑧) ∈ (1...𝑀))
368366, 367syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑧𝑆) → (1st𝑧) ∈ (1...𝑀))
369368adantr 468 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (1st𝑧) ∈ (1...𝑀))
370 elfzle2 12568 . . . . . . . . . . . . . . . . . . . 20 ((1st𝑧) ∈ (1...𝑀) → (1st𝑧) ≤ 𝑀)
371369, 370syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (1st𝑧) ≤ 𝑀)
372364, 371eqbrtrd 4866 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (2 · 𝑢) ≤ 𝑀)
373 zre 11647 . . . . . . . . . . . . . . . . . . . 20 (𝑢 ∈ ℤ → 𝑢 ∈ ℝ)
374373ad2antrl 710 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 𝑢 ∈ ℝ)
37511ad2antrr 708 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 𝑀 ∈ ℝ)
376160a1i 11 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 2 ∈ ℝ)
377162a1i 11 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 0 < 2)
378374, 375, 376, 377, 164syl112anc 1486 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → ((2 · 𝑢) ≤ 𝑀𝑢 ≤ (𝑀 / 2)))
379372, 378mpbid 223 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 𝑢 ≤ (𝑀 / 2))
38012ad2antrr 708 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (𝑀 / 2) ∈ ℝ)
381 simprl 778 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 𝑢 ∈ ℤ)
382380, 381, 154syl2anc 575 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (𝑢 ≤ (𝑀 / 2) ↔ 𝑢 ≤ (⌊‘(𝑀 / 2))))
383379, 382mpbid 223 . . . . . . . . . . . . . . . 16 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 𝑢 ≤ (⌊‘(𝑀 / 2)))
384 2t0e0 11460 . . . . . . . . . . . . . . . . . . . . 21 (2 · 0) = 0
385 elfznn 12593 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1st𝑧) ∈ (1...𝑀) → (1st𝑧) ∈ ℕ)
386369, 385syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (1st𝑧) ∈ ℕ)
387364, 386eqeltrd 2885 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (2 · 𝑢) ∈ ℕ)
388387nngt0d 11350 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 0 < (2 · 𝑢))
389384, 388syl5eqbr 4879 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (2 · 0) < (2 · 𝑢))
390 0red 10328 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 0 ∈ ℝ)
391 ltmul2 11159 . . . . . . . . . . . . . . . . . . . . 21 ((0 ∈ ℝ ∧ 𝑢 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (0 < 𝑢 ↔ (2 · 0) < (2 · 𝑢)))
392390, 374, 376, 377, 391syl112anc 1486 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (0 < 𝑢 ↔ (2 · 0) < (2 · 𝑢)))
393389, 392mpbird 248 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 0 < 𝑢)
394 elnnz 11653 . . . . . . . . . . . . . . . . . . 19 (𝑢 ∈ ℕ ↔ (𝑢 ∈ ℤ ∧ 0 < 𝑢))
395381, 393, 394sylanbrc 574 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 𝑢 ∈ ℕ)
396395, 286syl6eleq 2895 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 𝑢 ∈ (ℤ‘1))
39713ad2antrr 708 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (⌊‘(𝑀 / 2)) ∈ ℤ)
398 elfz5 12557 . . . . . . . . . . . . . . . . 17 ((𝑢 ∈ (ℤ‘1) ∧ (⌊‘(𝑀 / 2)) ∈ ℤ) → (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ↔ 𝑢 ≤ (⌊‘(𝑀 / 2))))
399396, 397, 398syl2anc 575 . . . . . . . . . . . . . . . 16 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ↔ 𝑢 ≤ (⌊‘(𝑀 / 2))))
400383, 399mpbird 248 . . . . . . . . . . . . . . 15 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 𝑢 ∈ (1...(⌊‘(𝑀 / 2))))
401400, 364jca 503 . . . . . . . . . . . . . 14 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ (2 · 𝑢) = (1st𝑧)))
402401ex 399 . . . . . . . . . . . . 13 ((𝜑𝑧𝑆) → ((𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧)) → (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ (2 · 𝑢) = (1st𝑧))))
403402reximdv2 3201 . . . . . . . . . . . 12 ((𝜑𝑧𝑆) → (∃𝑢 ∈ ℤ (2 · 𝑢) = (1st𝑧) → ∃𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(2 · 𝑢) = (1st𝑧)))
404363, 403impbid2 217 . . . . . . . . . . 11 ((𝜑𝑧𝑆) → (∃𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(2 · 𝑢) = (1st𝑧) ↔ ∃𝑢 ∈ ℤ (2 · 𝑢) = (1st𝑧)))
405 2z 11675 . . . . . . . . . . . 12 2 ∈ ℤ
406 elfzelz 12565 . . . . . . . . . . . . 13 ((1st𝑧) ∈ (1...𝑀) → (1st𝑧) ∈ ℤ)
407368, 406syl 17 . . . . . . . . . . . 12 ((𝜑𝑧𝑆) → (1st𝑧) ∈ ℤ)
408 divides 15205 . . . . . . . . . . . 12 ((2 ∈ ℤ ∧ (1st𝑧) ∈ ℤ) → (2 ∥ (1st𝑧) ↔ ∃𝑢 ∈ ℤ (𝑢 · 2) = (1st𝑧)))
409405, 407, 408sylancr 577 . . . . . . . . . . 11 ((𝜑𝑧𝑆) → (2 ∥ (1st𝑧) ↔ ∃𝑢 ∈ ℤ (𝑢 · 2) = (1st𝑧)))
410361, 404, 4093bitr4d 302 . . . . . . . . . 10 ((𝜑𝑧𝑆) → (∃𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(2 · 𝑢) = (1st𝑧) ↔ 2 ∥ (1st𝑧)))
411410rabbidva 3378 . . . . . . . . 9 (𝜑 → {𝑧𝑆 ∣ ∃𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(2 · 𝑢) = (1st𝑧)} = {𝑧𝑆 ∣ 2 ∥ (1st𝑧)})
412354, 411syl5eq 2852 . . . . . . . 8 (𝜑 𝑢 ∈ (1...(⌊‘(𝑀 / 2))){𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} = {𝑧𝑆 ∣ 2 ∥ (1st𝑧)})
413412fveq2d 6412 . . . . . . 7 (𝜑 → (♯‘ 𝑢 ∈ (1...(⌊‘(𝑀 / 2))){𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)}) = (♯‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)}))
414334, 353, 4133eqtr2d 2846 . . . . . 6 (𝜑 → Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = (♯‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)}))
415414oveq2d 6890 . . . . 5 (𝜑 → (-1↑Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (-1↑(♯‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)})))
4161, 2, 3, 5, 250, 103lgsquadlem1 25319 . . . . 5 (𝜑 → (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})))
417415, 416oveq12d 6892 . . . 4 (𝜑 → ((-1↑Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) · (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = ((-1↑(♯‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)})) · (-1↑(♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))))
418118, 417eqtr4d 2843 . . 3 (𝜑 → (-1↑((♯‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)}) + (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))) = ((-1↑Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) · (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
419 unrab 4099 . . . . . . 7 ({𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∪ {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) = {𝑧𝑆 ∣ (2 ∥ (1st𝑧) ∨ ¬ 2 ∥ (1st𝑧))}
420 exmid 909 . . . . . . . . 9 (2 ∥ (1st𝑧) ∨ ¬ 2 ∥ (1st𝑧))
421420rgenw 3112 . . . . . . . 8 𝑧𝑆 (2 ∥ (1st𝑧) ∨ ¬ 2 ∥ (1st𝑧))
422 rabid2 3307 . . . . . . . 8 (𝑆 = {𝑧𝑆 ∣ (2 ∥ (1st𝑧) ∨ ¬ 2 ∥ (1st𝑧))} ↔ ∀𝑧𝑆 (2 ∥ (1st𝑧) ∨ ¬ 2 ∥ (1st𝑧)))
423421, 422mpbir 222 . . . . . . 7 𝑆 = {𝑧𝑆 ∣ (2 ∥ (1st𝑧) ∨ ¬ 2 ∥ (1st𝑧))}
424419, 423eqtr4i 2831 . . . . . 6 ({𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∪ {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) = 𝑆
425424fveq2i 6411 . . . . 5 (♯‘({𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∪ {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) = (♯‘𝑆)
426 inrab 4100 . . . . . . 7 ({𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∩ {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) = {𝑧𝑆 ∣ (2 ∥ (1st𝑧) ∧ ¬ 2 ∥ (1st𝑧))}
427 pm3.24 391 . . . . . . . . . 10 ¬ (2 ∥ (1st𝑧) ∧ ¬ 2 ∥ (1st𝑧))
428427a1i 11 . . . . . . . . 9 (𝜑 → ¬ (2 ∥ (1st𝑧) ∧ ¬ 2 ∥ (1st𝑧)))
429428ralrimivw 3155 . . . . . . . 8 (𝜑 → ∀𝑧𝑆 ¬ (2 ∥ (1st𝑧) ∧ ¬ 2 ∥ (1st𝑧)))
430 rabeq0 4157 . . . . . . . 8 ({𝑧𝑆 ∣ (2 ∥ (1st𝑧) ∧ ¬ 2 ∥ (1st𝑧))} = ∅ ↔ ∀𝑧𝑆 ¬ (2 ∥ (1st𝑧) ∧ ¬ 2 ∥ (1st𝑧)))
431429, 430sylibr 225 . . . . . . 7 (𝜑 → {𝑧𝑆 ∣ (2 ∥ (1st𝑧) ∧ ¬ 2 ∥ (1st𝑧))} = ∅)
432426, 431syl5eq 2852 . . . . . 6 (𝜑 → ({𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∩ {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) = ∅)
433 hashun 13389 . . . . . 6 (({𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∈ Fin ∧ {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)} ∈ Fin ∧ ({𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∩ {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) = ∅) → (♯‘({𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∪ {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) = ((♯‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)}) + (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})))
434115, 110, 432, 433syl3anc 1483 . . . . 5 (𝜑 → (♯‘({𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∪ {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) = ((♯‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)}) + (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})))
435425, 434syl5reqr 2855 . . . 4 (𝜑 → ((♯‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)}) + (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) = (♯‘𝑆))
436435oveq2d 6890 . . 3 (𝜑 → (-1↑((♯‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)}) + (♯‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))) = (-1↑(♯‘𝑆)))
43799, 418, 4363eqtr2d 2846 . 2 (𝜑 → (-1↑(Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = (-1↑(♯‘𝑆)))
4384, 84, 4373eqtrd 2844 1 (𝜑 → (𝑄 /L 𝑃) = (-1↑(♯‘𝑆)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 865  w3a 1100   = wceq 1637  wcel 2156  wne 2978  wral 3096  wrex 3097  {crab 3100  cdif 3766  cun 3767  cin 3768  wss 3769  c0 4116  {csn 4370  cop 4376   ciun 4712  Disj wdisj 4812   class class class wbr 4844  {copab 4906   × cxp 5309  Rel wrel 5316  cfv 6101  (class class class)co 6874  1st c1st 7396  cen 8189  Fincfn 8192  cc 10219  cr 10220  0cc0 10221  1c1 10222   + caddc 10224   · cmul 10226   < clt 10359  cle 10360  cmin 10551  -cneg 10552   / cdiv 10969  cn 11305  2c2 11356  0cn0 11559  cz 11643  cuz 11904  +crp 12046  ...cfz 12549  cfl 12815  cexp 13083  chash 13337  Σcsu 14639  cdvds 15203   gcd cgcd 15435  cprime 15603   /L clgs 25233
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-rep 4964  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7179  ax-inf2 8785  ax-cnex 10277  ax-resscn 10278  ax-1cn 10279  ax-icn 10280  ax-addcl 10281  ax-addrcl 10282  ax-mulcl 10283  ax-mulrcl 10284  ax-mulcom 10285  ax-addass 10286  ax-mulass 10287  ax-distr 10288  ax-i2m1 10289  ax-1ne0 10290  ax-1rid 10291  ax-rnegex 10292  ax-rrecex 10293  ax-cnre 10294  ax-pre-lttri 10295  ax-pre-lttrn 10296  ax-pre-ltadd 10297  ax-pre-mulgt0 10298  ax-pre-sup 10299  ax-addf 10300  ax-mulf 10301
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-fal 1651  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-nel 3082  df-ral 3101  df-rex 3102  df-reu 3103  df-rmo 3104  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-int 4670  df-iun 4714  df-disj 4813  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-se 5271  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6064  df-fun 6103  df-fn 6104  df-f 6105  df-f1 6106  df-fo 6107  df-f1o 6108  df-fv 6109  df-isom 6110  df-riota 6835  df-ov 6877  df-oprab 6878  df-mpt2 6879  df-of 7127  df-om 7296  df-1st 7398  df-2nd 7399  df-supp 7530  df-tpos 7587  df-wrecs 7642  df-recs 7704  df-rdg 7742  df-1o 7796  df-2o 7797  df-oadd 7800  df-er 7979  df-ec 7981  df-qs 7985  df-map 8094  df-en 8193  df-dom 8194  df-sdom 8195  df-fin 8196  df-fsupp 8515  df-sup 8587  df-inf 8588  df-oi 8654  df-card 9048  df-cda 9275  df-pnf 10361  df-mnf 10362  df-xr 10363  df-ltxr 10364  df-le 10365  df-sub 10553  df-neg 10554  df-div 10970  df-nn 11306  df-2 11364  df-3 11365  df-4 11366  df-5 11367  df-6 11368  df-7 11369  df-8 11370  df-9 11371  df-n0 11560  df-xnn0 11630  df-z 11644  df-dec 11760  df-uz 11905  df-q 12008  df-rp 12047  df-fz 12550  df-fzo 12690  df-fl 12817  df-mod 12893  df-seq 13025  df-exp 13084  df-hash 13338  df-cj 14062  df-re 14063  df-im 14064  df-sqrt 14198  df-abs 14199  df-clim 14442  df-sum 14640  df-dvds 15204  df-gcd 15436  df-prm 15604  df-phi 15688  df-pc 15759  df-struct 16070  df-ndx 16071  df-slot 16072  df-base 16074  df-sets 16075  df-ress 16076  df-plusg 16166  df-mulr 16167  df-starv 16168  df-sca 16169  df-vsca 16170  df-ip 16171  df-tset 16172  df-ple 16173  df-ds 16175  df-unif 16176  df-0g 16307  df-gsum 16308  df-imas 16373  df-qus 16374  df-mgm 17447  df-sgrp 17489  df-mnd 17500  df-mhm 17540  df-submnd 17541  df-grp 17630  df-minusg 17631  df-sbg 17632  df-mulg 17746  df-subg 17793  df-nsg 17794  df-eqg 17795  df-ghm 17860  df-cntz 17951  df-cmn 18396  df-abl 18397  df-mgp 18692  df-ur 18704  df-ring 18751  df-cring 18752  df-oppr 18825  df-dvdsr 18843  df-unit 18844  df-invr 18874  df-dvr 18885  df-rnghom 18919  df-drng 18953  df-field 18954  df-subrg 18982  df-lmod 19069  df-lss 19137  df-lsp 19179  df-sra 19381  df-rgmod 19382  df-lidl 19383  df-rsp 19384  df-2idl 19441  df-nzr 19467  df-rlreg 19492  df-domn 19493  df-idom 19494  df-cnfld 19955  df-zring 20027  df-zrh 20060  df-zn 20063  df-lgs 25234
This theorem is referenced by:  lgsquadlem3  25321
  Copyright terms: Public domain W3C validator