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

Theorem lgsquadlem2 24851
Description: Lemma for lgsquad 24853. Count the members of 𝑆 with even coordinates, and combine with lgsquadlem1 24850 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 24849 . 2 (𝜑 → (𝑄 /L 𝑃) = (-1↑Σ𝑢 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
5 lgsquad.4 . . . . . 6 𝑀 = ((𝑃 − 1) / 2)
65oveq2i 6538 . . . . 5 (1...𝑀) = (1...((𝑃 − 1) / 2))
76sumeq1i 14225 . . . 4 Σ𝑢 ∈ (1...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = Σ𝑢 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))
8 oddprm 15302 . . . . . . . . . . . . 13 (𝑃 ∈ (ℙ ∖ {2}) → ((𝑃 − 1) / 2) ∈ ℕ)
91, 8syl 17 . . . . . . . . . . . 12 (𝜑 → ((𝑃 − 1) / 2) ∈ ℕ)
105, 9syl5eqel 2691 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℕ)
1110nnred 10885 . . . . . . . . . 10 (𝜑𝑀 ∈ ℝ)
1211rehalfcld 11129 . . . . . . . . 9 (𝜑 → (𝑀 / 2) ∈ ℝ)
1312flcld 12419 . . . . . . . 8 (𝜑 → (⌊‘(𝑀 / 2)) ∈ ℤ)
1413zred 11317 . . . . . . 7 (𝜑 → (⌊‘(𝑀 / 2)) ∈ ℝ)
1514ltp1d 10806 . . . . . 6 (𝜑 → (⌊‘(𝑀 / 2)) < ((⌊‘(𝑀 / 2)) + 1))
16 fzdisj 12197 . . . . . 6 ((⌊‘(𝑀 / 2)) < ((⌊‘(𝑀 / 2)) + 1) → ((1...(⌊‘(𝑀 / 2))) ∩ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) = ∅)
1715, 16syl 17 . . . . 5 (𝜑 → ((1...(⌊‘(𝑀 / 2))) ∩ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) = ∅)
1810nnrpd 11705 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℝ+)
1918rphalfcld 11719 . . . . . . . . . 10 (𝜑 → (𝑀 / 2) ∈ ℝ+)
2019rpge0d 11711 . . . . . . . . 9 (𝜑 → 0 ≤ (𝑀 / 2))
21 flge0nn0 12441 . . . . . . . . 9 (((𝑀 / 2) ∈ ℝ ∧ 0 ≤ (𝑀 / 2)) → (⌊‘(𝑀 / 2)) ∈ ℕ0)
2212, 20, 21syl2anc 690 . . . . . . . 8 (𝜑 → (⌊‘(𝑀 / 2)) ∈ ℕ0)
2310nnnn0d 11201 . . . . . . . 8 (𝜑𝑀 ∈ ℕ0)
24 rphalflt 11695 . . . . . . . . . . 11 (𝑀 ∈ ℝ+ → (𝑀 / 2) < 𝑀)
2518, 24syl 17 . . . . . . . . . 10 (𝜑 → (𝑀 / 2) < 𝑀)
2610nnzd 11316 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℤ)
27 fllt 12427 . . . . . . . . . . 11 (((𝑀 / 2) ∈ ℝ ∧ 𝑀 ∈ ℤ) → ((𝑀 / 2) < 𝑀 ↔ (⌊‘(𝑀 / 2)) < 𝑀))
2812, 26, 27syl2anc 690 . . . . . . . . . 10 (𝜑 → ((𝑀 / 2) < 𝑀 ↔ (⌊‘(𝑀 / 2)) < 𝑀))
2925, 28mpbid 220 . . . . . . . . 9 (𝜑 → (⌊‘(𝑀 / 2)) < 𝑀)
3014, 11, 29ltled 10037 . . . . . . . 8 (𝜑 → (⌊‘(𝑀 / 2)) ≤ 𝑀)
31 elfz2nn0 12258 . . . . . . . 8 ((⌊‘(𝑀 / 2)) ∈ (0...𝑀) ↔ ((⌊‘(𝑀 / 2)) ∈ ℕ0𝑀 ∈ ℕ0 ∧ (⌊‘(𝑀 / 2)) ≤ 𝑀))
3222, 23, 30, 31syl3anbrc 1238 . . . . . . 7 (𝜑 → (⌊‘(𝑀 / 2)) ∈ (0...𝑀))
33 nn0uz 11557 . . . . . . . . 9 0 = (ℤ‘0)
3423, 33syl6eleq 2697 . . . . . . . 8 (𝜑𝑀 ∈ (ℤ‘0))
35 elfzp12 12246 . . . . . . . 8 (𝑀 ∈ (ℤ‘0) → ((⌊‘(𝑀 / 2)) ∈ (0...𝑀) ↔ ((⌊‘(𝑀 / 2)) = 0 ∨ (⌊‘(𝑀 / 2)) ∈ ((0 + 1)...𝑀))))
3634, 35syl 17 . . . . . . 7 (𝜑 → ((⌊‘(𝑀 / 2)) ∈ (0...𝑀) ↔ ((⌊‘(𝑀 / 2)) = 0 ∨ (⌊‘(𝑀 / 2)) ∈ ((0 + 1)...𝑀))))
3732, 36mpbid 220 . . . . . 6 (𝜑 → ((⌊‘(𝑀 / 2)) = 0 ∨ (⌊‘(𝑀 / 2)) ∈ ((0 + 1)...𝑀)))
38 oveq2 6535 . . . . . . . . . 10 ((⌊‘(𝑀 / 2)) = 0 → (1...(⌊‘(𝑀 / 2))) = (1...0))
39 fz10 12191 . . . . . . . . . 10 (1...0) = ∅
4038, 39syl6eq 2659 . . . . . . . . 9 ((⌊‘(𝑀 / 2)) = 0 → (1...(⌊‘(𝑀 / 2))) = ∅)
41 oveq1 6534 . . . . . . . . . . 11 ((⌊‘(𝑀 / 2)) = 0 → ((⌊‘(𝑀 / 2)) + 1) = (0 + 1))
42 0p1e1 10982 . . . . . . . . . . 11 (0 + 1) = 1
4341, 42syl6eq 2659 . . . . . . . . . 10 ((⌊‘(𝑀 / 2)) = 0 → ((⌊‘(𝑀 / 2)) + 1) = 1)
4443oveq1d 6542 . . . . . . . . 9 ((⌊‘(𝑀 / 2)) = 0 → (((⌊‘(𝑀 / 2)) + 1)...𝑀) = (1...𝑀))
4540, 44uneq12d 3729 . . . . . . . 8 ((⌊‘(𝑀 / 2)) = 0 → ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) = (∅ ∪ (1...𝑀)))
46 un0 3918 . . . . . . . . 9 ((1...𝑀) ∪ ∅) = (1...𝑀)
47 uncom 3718 . . . . . . . . 9 ((1...𝑀) ∪ ∅) = (∅ ∪ (1...𝑀))
4846, 47eqtr3i 2633 . . . . . . . 8 (1...𝑀) = (∅ ∪ (1...𝑀))
4945, 48syl6reqr 2662 . . . . . . 7 ((⌊‘(𝑀 / 2)) = 0 → (1...𝑀) = ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀)))
50 fzsplit 12196 . . . . . . . 8 ((⌊‘(𝑀 / 2)) ∈ (1...𝑀) → (1...𝑀) = ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀)))
5142oveq1i 6537 . . . . . . . 8 ((0 + 1)...𝑀) = (1...𝑀)
5250, 51eleq2s 2705 . . . . . . 7 ((⌊‘(𝑀 / 2)) ∈ ((0 + 1)...𝑀) → (1...𝑀) = ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀)))
5349, 52jaoi 392 . . . . . 6 (((⌊‘(𝑀 / 2)) = 0 ∨ (⌊‘(𝑀 / 2)) ∈ ((0 + 1)...𝑀)) → (1...𝑀) = ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀)))
5437, 53syl 17 . . . . 5 (𝜑 → (1...𝑀) = ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀)))
55 fzfid 12592 . . . . 5 (𝜑 → (1...𝑀) ∈ Fin)
562eldifad 3551 . . . . . . . . . . . 12 (𝜑𝑄 ∈ ℙ)
57 prmnn 15175 . . . . . . . . . . . 12 (𝑄 ∈ ℙ → 𝑄 ∈ ℕ)
5856, 57syl 17 . . . . . . . . . . 11 (𝜑𝑄 ∈ ℕ)
5958nnred 10885 . . . . . . . . . 10 (𝜑𝑄 ∈ ℝ)
601eldifad 3551 . . . . . . . . . . 11 (𝜑𝑃 ∈ ℙ)
61 prmnn 15175 . . . . . . . . . . 11 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
6260, 61syl 17 . . . . . . . . . 10 (𝜑𝑃 ∈ ℕ)
6359, 62nndivred 10919 . . . . . . . . 9 (𝜑 → (𝑄 / 𝑃) ∈ ℝ)
6463adantr 479 . . . . . . . 8 ((𝜑𝑢 ∈ (1...𝑀)) → (𝑄 / 𝑃) ∈ ℝ)
65 2nn 11035 . . . . . . . . . 10 2 ∈ ℕ
66 elfznn 12199 . . . . . . . . . . 11 (𝑢 ∈ (1...𝑀) → 𝑢 ∈ ℕ)
6766adantl 480 . . . . . . . . . 10 ((𝜑𝑢 ∈ (1...𝑀)) → 𝑢 ∈ ℕ)
68 nnmulcl 10893 . . . . . . . . . 10 ((2 ∈ ℕ ∧ 𝑢 ∈ ℕ) → (2 · 𝑢) ∈ ℕ)
6965, 67, 68sylancr 693 . . . . . . . . 9 ((𝜑𝑢 ∈ (1...𝑀)) → (2 · 𝑢) ∈ ℕ)
7069nnred 10885 . . . . . . . 8 ((𝜑𝑢 ∈ (1...𝑀)) → (2 · 𝑢) ∈ ℝ)
7164, 70remulcld 9927 . . . . . . 7 ((𝜑𝑢 ∈ (1...𝑀)) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ)
7258nnrpd 11705 . . . . . . . . . . 11 (𝜑𝑄 ∈ ℝ+)
7362nnrpd 11705 . . . . . . . . . . 11 (𝜑𝑃 ∈ ℝ+)
7472, 73rpdivcld 11724 . . . . . . . . . 10 (𝜑 → (𝑄 / 𝑃) ∈ ℝ+)
7574adantr 479 . . . . . . . . 9 ((𝜑𝑢 ∈ (1...𝑀)) → (𝑄 / 𝑃) ∈ ℝ+)
7669nnrpd 11705 . . . . . . . . 9 ((𝜑𝑢 ∈ (1...𝑀)) → (2 · 𝑢) ∈ ℝ+)
7775, 76rpmulcld 11723 . . . . . . . 8 ((𝜑𝑢 ∈ (1...𝑀)) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ+)
7877rpge0d 11711 . . . . . . 7 ((𝜑𝑢 ∈ (1...𝑀)) → 0 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)))
79 flge0nn0 12441 . . . . . . 7 ((((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ ∧ 0 ≤ ((𝑄 / 𝑃) · (2 · 𝑢))) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℕ0)
8071, 78, 79syl2anc 690 . . . . . 6 ((𝜑𝑢 ∈ (1...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℕ0)
8180nn0cnd 11203 . . . . 5 ((𝜑𝑢 ∈ (1...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℂ)
8217, 54, 55, 81fsumsplit 14267 . . . 4 (𝜑 → Σ𝑢 ∈ (1...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = (Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
837, 82syl5eqr 2657 . . 3 (𝜑 → Σ𝑢 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = (Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
8483oveq2d 6543 . 2 (𝜑 → (-1↑Σ𝑢 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (-1↑(Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
85 neg1cn 10974 . . . . 5 -1 ∈ ℂ
8685a1i 11 . . . 4 (𝜑 → -1 ∈ ℂ)
87 fzfid 12592 . . . . 5 (𝜑 → (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∈ Fin)
88 ssun2 3738 . . . . . . . 8 (((⌊‘(𝑀 / 2)) + 1)...𝑀) ⊆ ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀))
8988, 54syl5sseqr 3616 . . . . . . 7 (𝜑 → (((⌊‘(𝑀 / 2)) + 1)...𝑀) ⊆ (1...𝑀))
9089sselda 3567 . . . . . 6 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ∈ (1...𝑀))
9190, 80syldan 485 . . . . 5 ((𝜑𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℕ0)
9287, 91fsumnn0cl 14263 . . . 4 (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℕ0)
93 fzfid 12592 . . . . 5 (𝜑 → (1...(⌊‘(𝑀 / 2))) ∈ Fin)
94 ssun1 3737 . . . . . . . 8 (1...(⌊‘(𝑀 / 2))) ⊆ ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀))
9594, 54syl5sseqr 3616 . . . . . . 7 (𝜑 → (1...(⌊‘(𝑀 / 2))) ⊆ (1...𝑀))
9695sselda 3567 . . . . . 6 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ∈ (1...𝑀))
9796, 80syldan 485 . . . . 5 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℕ0)
9893, 97fsumnn0cl 14263 . . . 4 (𝜑 → Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℕ0)
9986, 92, 98expaddd 12830 . . 3 (𝜑 → (-1↑(Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = ((-1↑Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) · (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
100 fzfid 12592 . . . . . . . . 9 (𝜑 → (1...𝑁) ∈ Fin)
101 xpfi 8094 . . . . . . . . 9 (((1...𝑀) ∈ Fin ∧ (1...𝑁) ∈ Fin) → ((1...𝑀) × (1...𝑁)) ∈ Fin)
10255, 100, 101syl2anc 690 . . . . . . . 8 (𝜑 → ((1...𝑀) × (1...𝑁)) ∈ Fin)
103 lgsquad.6 . . . . . . . . 9 𝑆 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))}
104 opabssxp 5106 . . . . . . . . 9 {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} ⊆ ((1...𝑀) × (1...𝑁))
105103, 104eqsstri 3597 . . . . . . . 8 𝑆 ⊆ ((1...𝑀) × (1...𝑁))
106 ssfi 8043 . . . . . . . 8 ((((1...𝑀) × (1...𝑁)) ∈ Fin ∧ 𝑆 ⊆ ((1...𝑀) × (1...𝑁))) → 𝑆 ∈ Fin)
107102, 105, 106sylancl 692 . . . . . . 7 (𝜑𝑆 ∈ Fin)
108 ssrab2 3649 . . . . . . 7 {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)} ⊆ 𝑆
109 ssfi 8043 . . . . . . 7 ((𝑆 ∈ Fin ∧ {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)} ⊆ 𝑆) → {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)} ∈ Fin)
110107, 108, 109sylancl 692 . . . . . 6 (𝜑 → {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)} ∈ Fin)
111 hashcl 12964 . . . . . 6 ({𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)} ∈ Fin → (#‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) ∈ ℕ0)
112110, 111syl 17 . . . . 5 (𝜑 → (#‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) ∈ ℕ0)
113 ssrab2 3649 . . . . . . 7 {𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ⊆ 𝑆
114 ssfi 8043 . . . . . . 7 ((𝑆 ∈ Fin ∧ {𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ⊆ 𝑆) → {𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∈ Fin)
115107, 113, 114sylancl 692 . . . . . 6 (𝜑 → {𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∈ Fin)
116 hashcl 12964 . . . . . 6 ({𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∈ Fin → (#‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)}) ∈ ℕ0)
117115, 116syl 17 . . . . 5 (𝜑 → (#‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)}) ∈ ℕ0)
11886, 112, 117expaddd 12830 . . . 4 (𝜑 → (-1↑((#‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)}) + (#‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))) = ((-1↑(#‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)})) · (-1↑(#‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))))
11996, 69syldan 485 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (2 · 𝑢) ∈ ℕ)
120 fzfid 12592 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ Fin)
121 xpsnen2g 7916 . . . . . . . . . . 11 (((2 · 𝑢) ∈ ℕ ∧ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ Fin) → ({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ≈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
122119, 120, 121syl2anc 690 . . . . . . . . . 10 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ≈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
123 hasheni 12953 . . . . . . . . . 10 (({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ≈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) → (#‘({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) = (#‘(1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
124122, 123syl 17 . . . . . . . . 9 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (#‘({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) = (#‘(1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
125 ssrab2 3649 . . . . . . . . . . . . 13 {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} ⊆ 𝑆
126103relopabi 5156 . . . . . . . . . . . . 13 Rel 𝑆
127 relss 5119 . . . . . . . . . . . . 13 ({𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} ⊆ 𝑆 → (Rel 𝑆 → Rel {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)}))
128125, 126, 127mp2 9 . . . . . . . . . . . 12 Rel {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)}
129 relxp 5139 . . . . . . . . . . . 12 Rel ({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
130103eleq2i 2679 . . . . . . . . . . . . . . . 16 (⟨𝑥, 𝑦⟩ ∈ 𝑆 ↔ ⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))})
131 opabid 4897 . . . . . . . . . . . . . . . 16 (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} ↔ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))
132130, 131bitri 262 . . . . . . . . . . . . . . 15 (⟨𝑥, 𝑦⟩ ∈ 𝑆 ↔ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))
133 anass 678 . . . . . . . . . . . . . . . . . 18 (((𝑦 ∈ ℕ ∧ 𝑦𝑁) ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢))) ↔ (𝑦 ∈ ℕ ∧ (𝑦𝑁 ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)))))
134 simpr 475 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ ℕ)
13562ad2antrr 757 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℕ)
136134, 135nnmulcld 10918 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 · 𝑃) ∈ ℕ)
137136nnred 10885 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 · 𝑃) ∈ ℝ)
13858adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑄 ∈ ℕ)
139138, 119nnmulcld 10918 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (𝑄 · (2 · 𝑢)) ∈ ℕ)
140139adantr 479 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (2 · 𝑢)) ∈ ℕ)
141140nnred 10885 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (2 · 𝑢)) ∈ ℝ)
142137, 141ltlend 10034 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ↔ ((𝑦 · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ∧ (𝑄 · (2 · 𝑢)) ≠ (𝑦 · 𝑃))))
143119adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2 · 𝑢) ∈ ℕ)
144143nnred 10885 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2 · 𝑢) ∈ ℝ)
145135nnred 10885 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℝ)
146145rehalfcld 11129 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 / 2) ∈ ℝ)
14711adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑀 ∈ ℝ)
148147adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑀 ∈ ℝ)
149 elfzle2 12174 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) → 𝑢 ≤ (⌊‘(𝑀 / 2)))
150149adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ≤ (⌊‘(𝑀 / 2)))
151147rehalfcld 11129 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (𝑀 / 2) ∈ ℝ)
152 elfzelz 12171 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) → 𝑢 ∈ ℤ)
153152adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ∈ ℤ)
154 flge 12426 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑀 / 2) ∈ ℝ ∧ 𝑢 ∈ ℤ) → (𝑢 ≤ (𝑀 / 2) ↔ 𝑢 ≤ (⌊‘(𝑀 / 2))))
155151, 153, 154syl2anc 690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (𝑢 ≤ (𝑀 / 2) ↔ 𝑢 ≤ (⌊‘(𝑀 / 2))))
156150, 155mpbird 245 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ≤ (𝑀 / 2))
157 elfznn 12199 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) → 𝑢 ∈ ℕ)
158157adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ∈ ℕ)
159158nnred 10885 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ∈ ℝ)
160 2re 10940 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 2 ∈ ℝ
161160a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 2 ∈ ℝ)
162 2pos 10962 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 0 < 2
163162a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 0 < 2)
164 lemuldiv2 10756 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑢 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 𝑢) ≤ 𝑀𝑢 ≤ (𝑀 / 2)))
165159, 147, 161, 163, 164syl112anc 1321 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((2 · 𝑢) ≤ 𝑀𝑢 ≤ (𝑀 / 2)))
166156, 165mpbird 245 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (2 · 𝑢) ≤ 𝑀)
167166adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2 · 𝑢) ≤ 𝑀)
168145ltm1d 10808 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 − 1) < 𝑃)
169 peano2rem 10200 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑃 ∈ ℝ → (𝑃 − 1) ∈ ℝ)
170145, 169syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 − 1) ∈ ℝ)
171160a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 2 ∈ ℝ)
172162a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 0 < 2)
173 ltdiv1 10739 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑃 − 1) ∈ ℝ ∧ 𝑃 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((𝑃 − 1) < 𝑃 ↔ ((𝑃 − 1) / 2) < (𝑃 / 2)))
174170, 145, 171, 172, 173syl112anc 1321 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑃 − 1) < 𝑃 ↔ ((𝑃 − 1) / 2) < (𝑃 / 2)))
175168, 174mpbid 220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑃 − 1) / 2) < (𝑃 / 2))
1765, 175syl5eqbr 4612 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑀 < (𝑃 / 2))
177144, 148, 146, 167, 176lelttrd 10047 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2 · 𝑢) < (𝑃 / 2))
178135nnrpd 11705 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℝ+)
179 rphalflt 11695 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑃 ∈ ℝ+ → (𝑃 / 2) < 𝑃)
180178, 179syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 / 2) < 𝑃)
181144, 146, 145, 177, 180lttrd 10050 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2 · 𝑢) < 𝑃)
182144, 145ltnled 10036 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((2 · 𝑢) < 𝑃 ↔ ¬ 𝑃 ≤ (2 · 𝑢)))
183181, 182mpbid 220 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ¬ 𝑃 ≤ (2 · 𝑢))
18460ad2antrr 757 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℙ)
185 prmz 15176 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
186184, 185syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℤ)
187 dvdsle 14819 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑃 ∈ ℤ ∧ (2 · 𝑢) ∈ ℕ) → (𝑃 ∥ (2 · 𝑢) → 𝑃 ≤ (2 · 𝑢)))
188186, 143, 187syl2anc 690 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 ∥ (2 · 𝑢) → 𝑃 ≤ (2 · 𝑢)))
189183, 188mtod 187 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ¬ 𝑃 ∥ (2 · 𝑢))
190 prmrp 15211 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ) → ((𝑃 gcd 𝑄) = 1 ↔ 𝑃𝑄))
19160, 56, 190syl2anc 690 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → ((𝑃 gcd 𝑄) = 1 ↔ 𝑃𝑄))
1923, 191mpbird 245 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝑃 gcd 𝑄) = 1)
193192ad2antrr 757 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 gcd 𝑄) = 1)
19456ad2antrr 757 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈ ℙ)
195 prmz 15176 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑄 ∈ ℙ → 𝑄 ∈ ℤ)
196194, 195syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈ ℤ)
197143nnzd 11316 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2 · 𝑢) ∈ ℤ)
198 coprmdvds 15153 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑃 ∈ ℤ ∧ 𝑄 ∈ ℤ ∧ (2 · 𝑢) ∈ ℤ) → ((𝑃 ∥ (𝑄 · (2 · 𝑢)) ∧ (𝑃 gcd 𝑄) = 1) → 𝑃 ∥ (2 · 𝑢)))
199186, 196, 197, 198syl3anc 1317 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑃 ∥ (𝑄 · (2 · 𝑢)) ∧ (𝑃 gcd 𝑄) = 1) → 𝑃 ∥ (2 · 𝑢)))
200193, 199mpan2d 705 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 ∥ (𝑄 · (2 · 𝑢)) → 𝑃 ∥ (2 · 𝑢)))
201189, 200mtod 187 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ¬ 𝑃 ∥ (𝑄 · (2 · 𝑢)))
202 nnz 11235 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 ∈ ℕ → 𝑦 ∈ ℤ)
203202adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ ℤ)
204 dvdsmul2 14791 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦 ∈ ℤ ∧ 𝑃 ∈ ℤ) → 𝑃 ∥ (𝑦 · 𝑃))
205203, 186, 204syl2anc 690 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∥ (𝑦 · 𝑃))
206 breq2 4581 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑄 · (2 · 𝑢)) = (𝑦 · 𝑃) → (𝑃 ∥ (𝑄 · (2 · 𝑢)) ↔ 𝑃 ∥ (𝑦 · 𝑃)))
207205, 206syl5ibrcom 235 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 · (2 · 𝑢)) = (𝑦 · 𝑃) → 𝑃 ∥ (𝑄 · (2 · 𝑢))))
208207necon3bd 2795 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (¬ 𝑃 ∥ (𝑄 · (2 · 𝑢)) → (𝑄 · (2 · 𝑢)) ≠ (𝑦 · 𝑃)))
209201, 208mpd 15 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (2 · 𝑢)) ≠ (𝑦 · 𝑃))
210209biantrud 526 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ↔ ((𝑦 · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ∧ (𝑄 · (2 · 𝑢)) ≠ (𝑦 · 𝑃))))
211142, 210bitr4d 269 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ↔ (𝑦 · 𝑃) ≤ (𝑄 · (2 · 𝑢))))
212 nnre 10877 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
213212adantl 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ ℝ)
214135nngt0d 10914 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 0 < 𝑃)
215 lemuldiv 10755 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 ∈ ℝ ∧ (𝑄 · (2 · 𝑢)) ∈ ℝ ∧ (𝑃 ∈ ℝ ∧ 0 < 𝑃)) → ((𝑦 · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ↔ 𝑦 ≤ ((𝑄 · (2 · 𝑢)) / 𝑃)))
216213, 141, 145, 214, 215syl112anc 1321 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ↔ 𝑦 ≤ ((𝑄 · (2 · 𝑢)) / 𝑃)))
217138adantr 479 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈ ℕ)
218217nncnd 10886 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈ ℂ)
219143nncnd 10886 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2 · 𝑢) ∈ ℂ)
220135nncnd 10886 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℂ)
221135nnne0d 10915 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ≠ 0)
222218, 219, 220, 221div23d 10690 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 · (2 · 𝑢)) / 𝑃) = ((𝑄 / 𝑃) · (2 · 𝑢)))
223222breq2d 4589 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 ≤ ((𝑄 · (2 · 𝑢)) / 𝑃) ↔ 𝑦 ≤ ((𝑄 / 𝑃) · (2 · 𝑢))))
224211, 216, 2233bitrd 292 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ↔ 𝑦 ≤ ((𝑄 / 𝑃) · (2 · 𝑢))))
225217nnred 10885 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈ ℝ)
226217nngt0d 10914 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 0 < 𝑄)
227 ltmul2 10726 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((2 · 𝑢) ∈ ℝ ∧ (𝑃 / 2) ∈ ℝ ∧ (𝑄 ∈ ℝ ∧ 0 < 𝑄)) → ((2 · 𝑢) < (𝑃 / 2) ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · (𝑃 / 2))))
228144, 146, 225, 226, 227syl112anc 1321 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((2 · 𝑢) < (𝑃 / 2) ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · (𝑃 / 2))))
229177, 228mpbid 220 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (2 · 𝑢)) < (𝑄 · (𝑃 / 2)))
230 2cnd 10943 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 2 ∈ ℂ)
231 2ne0 10963 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 2 ≠ 0
232231a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 2 ≠ 0)
233 divass 10555 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑄 ∈ ℂ ∧ 𝑃 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((𝑄 · 𝑃) / 2) = (𝑄 · (𝑃 / 2)))
234 div23 10556 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑄 ∈ ℂ ∧ 𝑃 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((𝑄 · 𝑃) / 2) = ((𝑄 / 2) · 𝑃))
235233, 234eqtr3d 2645 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑄 ∈ ℂ ∧ 𝑃 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (𝑄 · (𝑃 / 2)) = ((𝑄 / 2) · 𝑃))
236218, 220, 230, 232, 235syl112anc 1321 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (𝑃 / 2)) = ((𝑄 / 2) · 𝑃))
237229, 236breqtrd 4603 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (2 · 𝑢)) < ((𝑄 / 2) · 𝑃))
238225rehalfcld 11129 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 / 2) ∈ ℝ)
239238, 145remulcld 9927 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 / 2) · 𝑃) ∈ ℝ)
240 lttr 9966 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑦 · 𝑃) ∈ ℝ ∧ (𝑄 · (2 · 𝑢)) ∈ ℝ ∧ ((𝑄 / 2) · 𝑃) ∈ ℝ) → (((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ∧ (𝑄 · (2 · 𝑢)) < ((𝑄 / 2) · 𝑃)) → (𝑦 · 𝑃) < ((𝑄 / 2) · 𝑃)))
241137, 141, 239, 240syl3anc 1317 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ∧ (𝑄 · (2 · 𝑢)) < ((𝑄 / 2) · 𝑃)) → (𝑦 · 𝑃) < ((𝑄 / 2) · 𝑃)))
242237, 241mpan2d 705 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) → (𝑦 · 𝑃) < ((𝑄 / 2) · 𝑃)))
243 ltmul1 10725 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑦 ∈ ℝ ∧ (𝑄 / 2) ∈ ℝ ∧ (𝑃 ∈ ℝ ∧ 0 < 𝑃)) → (𝑦 < (𝑄 / 2) ↔ (𝑦 · 𝑃) < ((𝑄 / 2) · 𝑃)))
244213, 238, 145, 214, 243syl112anc 1321 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 < (𝑄 / 2) ↔ (𝑦 · 𝑃) < ((𝑄 / 2) · 𝑃)))
245242, 244sylibrd 247 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) → 𝑦 < (𝑄 / 2)))
246 peano2rem 10200 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑄 ∈ ℝ → (𝑄 − 1) ∈ ℝ)
247225, 246syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 − 1) ∈ ℝ)
248247recnd 9925 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 − 1) ∈ ℂ)
249218, 248, 230, 232divsubdird 10692 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 − (𝑄 − 1)) / 2) = ((𝑄 / 2) − ((𝑄 − 1) / 2)))
250 lgsquad.5 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑁 = ((𝑄 − 1) / 2)
251250oveq2i 6538 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑄 / 2) − 𝑁) = ((𝑄 / 2) − ((𝑄 − 1) / 2))
252249, 251syl6eqr 2661 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 − (𝑄 − 1)) / 2) = ((𝑄 / 2) − 𝑁))
253 ax-1cn 9851 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 1 ∈ ℂ
254 nncan 10162 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑄 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑄 − (𝑄 − 1)) = 1)
255218, 253, 254sylancl 692 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 − (𝑄 − 1)) = 1)
256255oveq1d 6542 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 − (𝑄 − 1)) / 2) = (1 / 2))
257 halflt1 11100 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (1 / 2) < 1
258256, 257syl6eqbr 4616 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 − (𝑄 − 1)) / 2) < 1)
259252, 258eqbrtrrd 4601 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 / 2) − 𝑁) < 1)
260 oddprm 15302 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑄 ∈ (ℙ ∖ {2}) → ((𝑄 − 1) / 2) ∈ ℕ)
2612, 260syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → ((𝑄 − 1) / 2) ∈ ℕ)
262250, 261syl5eqel 2691 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝑁 ∈ ℕ)
263262ad2antrr 757 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑁 ∈ ℕ)
264263nnred 10885 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑁 ∈ ℝ)
265 1red 9912 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 1 ∈ ℝ)
266238, 264, 265ltsubadd2d 10477 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (((𝑄 / 2) − 𝑁) < 1 ↔ (𝑄 / 2) < (𝑁 + 1)))
267259, 266mpbid 220 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 / 2) < (𝑁 + 1))
268 peano2re 10061 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑁 ∈ ℝ → (𝑁 + 1) ∈ ℝ)
269264, 268syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑁 + 1) ∈ ℝ)
270 lttr 9966 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑦 ∈ ℝ ∧ (𝑄 / 2) ∈ ℝ ∧ (𝑁 + 1) ∈ ℝ) → ((𝑦 < (𝑄 / 2) ∧ (𝑄 / 2) < (𝑁 + 1)) → 𝑦 < (𝑁 + 1)))
271213, 238, 269, 270syl3anc 1317 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 < (𝑄 / 2) ∧ (𝑄 / 2) < (𝑁 + 1)) → 𝑦 < (𝑁 + 1)))
272267, 271mpan2d 705 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 < (𝑄 / 2) → 𝑦 < (𝑁 + 1)))
273245, 272syld 45 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) → 𝑦 < (𝑁 + 1)))
274 nnleltp1 11268 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑦𝑁𝑦 < (𝑁 + 1)))
275134, 263, 274syl2anc 690 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦𝑁𝑦 < (𝑁 + 1)))
276273, 275sylibrd 247 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) → 𝑦𝑁))
277276pm4.71rd 664 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ↔ (𝑦𝑁 ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)))))
27896, 71syldan 485 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ)
279 flge 12426 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ ∧ 𝑦 ∈ ℤ) → (𝑦 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)) ↔ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
280278, 202, 279syl2an 492 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)) ↔ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
281224, 277, 2803bitr3d 296 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦𝑁 ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢))) ↔ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
282281pm5.32da 670 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((𝑦 ∈ ℕ ∧ (𝑦𝑁 ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
283133, 282syl5bb 270 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (((𝑦 ∈ ℕ ∧ 𝑦𝑁) ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
284283adantr 479 . . . . . . . . . . . . . . . 16 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (((𝑦 ∈ ℕ ∧ 𝑦𝑁) ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
285 simpr 475 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → 𝑥 = (2 · 𝑢))
286 nnuz 11558 . . . . . . . . . . . . . . . . . . . . . . . 24 ℕ = (ℤ‘1)
287119, 286syl6eleq 2697 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (2 · 𝑢) ∈ (ℤ‘1))
28826adantr 479 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑀 ∈ ℤ)
289 elfz5 12163 . . . . . . . . . . . . . . . . . . . . . . 23 (((2 · 𝑢) ∈ (ℤ‘1) ∧ 𝑀 ∈ ℤ) → ((2 · 𝑢) ∈ (1...𝑀) ↔ (2 · 𝑢) ≤ 𝑀))
290287, 288, 289syl2anc 690 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((2 · 𝑢) ∈ (1...𝑀) ↔ (2 · 𝑢) ≤ 𝑀))
291166, 290mpbird 245 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (2 · 𝑢) ∈ (1...𝑀))
292291adantr 479 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (2 · 𝑢) ∈ (1...𝑀))
293285, 292eqeltrd 2687 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → 𝑥 ∈ (1...𝑀))
294293biantrurd 527 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (𝑦 ∈ (1...𝑁) ↔ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))))
295262nnzd 11316 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑁 ∈ ℤ)
296295ad2antrr 757 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → 𝑁 ∈ ℤ)
297 fznn 12236 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ ℤ → (𝑦 ∈ (1...𝑁) ↔ (𝑦 ∈ ℕ ∧ 𝑦𝑁)))
298296, 297syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (𝑦 ∈ (1...𝑁) ↔ (𝑦 ∈ ℕ ∧ 𝑦𝑁)))
299294, 298bitr3d 268 . . . . . . . . . . . . . . . . 17 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ↔ (𝑦 ∈ ℕ ∧ 𝑦𝑁)))
300 oveq1 6534 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (2 · 𝑢) → (𝑥 · 𝑄) = ((2 · 𝑢) · 𝑄))
301119nncnd 10886 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (2 · 𝑢) ∈ ℂ)
302138nncnd 10886 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑄 ∈ ℂ)
303301, 302mulcomd 9918 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((2 · 𝑢) · 𝑄) = (𝑄 · (2 · 𝑢)))
304300, 303sylan9eqr 2665 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (𝑥 · 𝑄) = (𝑄 · (2 · 𝑢)))
305304breq2d 4589 . . . . . . . . . . . . . . . . 17 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → ((𝑦 · 𝑃) < (𝑥 · 𝑄) ↔ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢))))
306299, 305anbi12d 742 . . . . . . . . . . . . . . . 16 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)) ↔ ((𝑦 ∈ ℕ ∧ 𝑦𝑁) ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)))))
307278flcld 12419 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ)
308 fznn 12236 . . . . . . . . . . . . . . . . . 18 ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ → (𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
309307, 308syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
310309adantr 479 . . . . . . . . . . . . . . . 16 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
311284, 306, 3103bitr4d 298 . . . . . . . . . . . . . . 15 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)) ↔ 𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
312132, 311syl5bb 270 . . . . . . . . . . . . . 14 (((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (⟨𝑥, 𝑦⟩ ∈ 𝑆𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
313312pm5.32da 670 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((𝑥 = (2 · 𝑢) ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑆) ↔ (𝑥 = (2 · 𝑢) ∧ 𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
314 vex 3175 . . . . . . . . . . . . . . . . . 18 𝑥 ∈ V
315 vex 3175 . . . . . . . . . . . . . . . . . 18 𝑦 ∈ V
316314, 315op1std 7047 . . . . . . . . . . . . . . . . 17 (𝑧 = ⟨𝑥, 𝑦⟩ → (1st𝑧) = 𝑥)
317316eqeq2d 2619 . . . . . . . . . . . . . . . 16 (𝑧 = ⟨𝑥, 𝑦⟩ → ((2 · 𝑢) = (1st𝑧) ↔ (2 · 𝑢) = 𝑥))
318 eqcom 2616 . . . . . . . . . . . . . . . 16 ((2 · 𝑢) = 𝑥𝑥 = (2 · 𝑢))
319317, 318syl6bb 274 . . . . . . . . . . . . . . 15 (𝑧 = ⟨𝑥, 𝑦⟩ → ((2 · 𝑢) = (1st𝑧) ↔ 𝑥 = (2 · 𝑢)))
320319elrab 3330 . . . . . . . . . . . . . 14 (⟨𝑥, 𝑦⟩ ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} ↔ (⟨𝑥, 𝑦⟩ ∈ 𝑆𝑥 = (2 · 𝑢)))
321 ancom 464 . . . . . . . . . . . . . 14 ((⟨𝑥, 𝑦⟩ ∈ 𝑆𝑥 = (2 · 𝑢)) ↔ (𝑥 = (2 · 𝑢) ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑆))
322320, 321bitri 262 . . . . . . . . . . . . 13 (⟨𝑥, 𝑦⟩ ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} ↔ (𝑥 = (2 · 𝑢) ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑆))
323 opelxp 5060 . . . . . . . . . . . . . 14 (⟨𝑥, 𝑦⟩ ∈ ({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ↔ (𝑥 ∈ {(2 · 𝑢)} ∧ 𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
324 velsn 4140 . . . . . . . . . . . . . . 15 (𝑥 ∈ {(2 · 𝑢)} ↔ 𝑥 = (2 · 𝑢))
325324anbi1i 726 . . . . . . . . . . . . . 14 ((𝑥 ∈ {(2 · 𝑢)} ∧ 𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ↔ (𝑥 = (2 · 𝑢) ∧ 𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
326323, 325bitri 262 . . . . . . . . . . . . 13 (⟨𝑥, 𝑦⟩ ∈ ({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ↔ (𝑥 = (2 · 𝑢) ∧ 𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
327313, 322, 3263bitr4g 301 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (⟨𝑥, 𝑦⟩ ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} ↔ ⟨𝑥, 𝑦⟩ ∈ ({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
328128, 129, 327eqrelrdv 5128 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} = ({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
329328eqcomd 2615 . . . . . . . . . 10 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)})
330329fveq2d 6092 . . . . . . . . 9 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (#‘({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) = (#‘{𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)}))
331 hashfz1 12951 . . . . . . . . . 10 ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℕ0 → (#‘(1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))
33297, 331syl 17 . . . . . . . . 9 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (#‘(1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))
333124, 330, 3323eqtr3rd 2652 . . . . . . . 8 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = (#‘{𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)}))
334333sumeq2dv 14230 . . . . . . 7 (𝜑 → Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(#‘{𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)}))
335107adantr 479 . . . . . . . . 9 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑆 ∈ Fin)
336 ssfi 8043 . . . . . . . . 9 ((𝑆 ∈ Fin ∧ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} ⊆ 𝑆) → {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} ∈ Fin)
337335, 125, 336sylancl 692 . . . . . . . 8 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} ∈ Fin)
338 fveq2 6088 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑣 → (1st𝑧) = (1st𝑣))
339338eqeq2d 2619 . . . . . . . . . . . . . . 15 (𝑧 = 𝑣 → ((2 · 𝑢) = (1st𝑧) ↔ (2 · 𝑢) = (1st𝑣)))
340339elrab 3330 . . . . . . . . . . . . . 14 (𝑣 ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} ↔ (𝑣𝑆 ∧ (2 · 𝑢) = (1st𝑣)))
341340simprbi 478 . . . . . . . . . . . . 13 (𝑣 ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} → (2 · 𝑢) = (1st𝑣))
342341ad2antll 760 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)})) → (2 · 𝑢) = (1st𝑣))
343342oveq1d 6542 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)})) → ((2 · 𝑢) / 2) = ((1st𝑣) / 2))
344158nncnd 10886 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ∈ ℂ)
345344adantrr 748 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)})) → 𝑢 ∈ ℂ)
346 2cnd 10943 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)})) → 2 ∈ ℂ)
347231a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)})) → 2 ≠ 0)
348345, 346, 347divcan3d 10658 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)})) → ((2 · 𝑢) / 2) = 𝑢)
349343, 348eqtr3d 2645 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)})) → ((1st𝑣) / 2) = 𝑢)
350349ralrimivva 2953 . . . . . . . . 9 (𝜑 → ∀𝑢 ∈ (1...(⌊‘(𝑀 / 2)))∀𝑣 ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} ((1st𝑣) / 2) = 𝑢)
351 invdisj 4565 . . . . . . . . 9 (∀𝑢 ∈ (1...(⌊‘(𝑀 / 2)))∀𝑣 ∈ {𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} ((1st𝑣) / 2) = 𝑢Disj 𝑢 ∈ (1...(⌊‘(𝑀 / 2))){𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)})
352350, 351syl 17 . . . . . . . 8 (𝜑Disj 𝑢 ∈ (1...(⌊‘(𝑀 / 2))){𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)})
35393, 337, 352hashiun 14344 . . . . . . 7 (𝜑 → (#‘ 𝑢 ∈ (1...(⌊‘(𝑀 / 2))){𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)}) = Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(#‘{𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)}))
354 iunrab 4497 . . . . . . . . 9 𝑢 ∈ (1...(⌊‘(𝑀 / 2))){𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} = {𝑧𝑆 ∣ ∃𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(2 · 𝑢) = (1st𝑧)}
355 2cn 10941 . . . . . . . . . . . . . 14 2 ∈ ℂ
356 zcn 11218 . . . . . . . . . . . . . . 15 (𝑢 ∈ ℤ → 𝑢 ∈ ℂ)
357356adantl 480 . . . . . . . . . . . . . 14 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ ℤ) → 𝑢 ∈ ℂ)
358 mulcom 9879 . . . . . . . . . . . . . 14 ((2 ∈ ℂ ∧ 𝑢 ∈ ℂ) → (2 · 𝑢) = (𝑢 · 2))
359355, 357, 358sylancr 693 . . . . . . . . . . . . 13 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ ℤ) → (2 · 𝑢) = (𝑢 · 2))
360359eqeq1d 2611 . . . . . . . . . . . 12 (((𝜑𝑧𝑆) ∧ 𝑢 ∈ ℤ) → ((2 · 𝑢) = (1st𝑧) ↔ (𝑢 · 2) = (1st𝑧)))
361360rexbidva 3030 . . . . . . . . . . 11 ((𝜑𝑧𝑆) → (∃𝑢 ∈ ℤ (2 · 𝑢) = (1st𝑧) ↔ ∃𝑢 ∈ ℤ (𝑢 · 2) = (1st𝑧)))
362152anim1i 589 . . . . . . . . . . . . 13 ((𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ (2 · 𝑢) = (1st𝑧)) → (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧)))
363362reximi2 2992 . . . . . . . . . . . 12 (∃𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(2 · 𝑢) = (1st𝑧) → ∃𝑢 ∈ ℤ (2 · 𝑢) = (1st𝑧))
364 simprr 791 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (2 · 𝑢) = (1st𝑧))
365 simpr 475 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑧𝑆) → 𝑧𝑆)
366105, 365sseldi 3565 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑧𝑆) → 𝑧 ∈ ((1...𝑀) × (1...𝑁)))
367 xp1st 7067 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ ((1...𝑀) × (1...𝑁)) → (1st𝑧) ∈ (1...𝑀))
368366, 367syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑧𝑆) → (1st𝑧) ∈ (1...𝑀))
369368adantr 479 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (1st𝑧) ∈ (1...𝑀))
370 elfzle2 12174 . . . . . . . . . . . . . . . . . . . 20 ((1st𝑧) ∈ (1...𝑀) → (1st𝑧) ≤ 𝑀)
371369, 370syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (1st𝑧) ≤ 𝑀)
372364, 371eqbrtrd 4599 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (2 · 𝑢) ≤ 𝑀)
373 zre 11217 . . . . . . . . . . . . . . . . . . . 20 (𝑢 ∈ ℤ → 𝑢 ∈ ℝ)
374373ad2antrl 759 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 𝑢 ∈ ℝ)
37511ad2antrr 757 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 𝑀 ∈ ℝ)
376160a1i 11 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 2 ∈ ℝ)
377162a1i 11 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 0 < 2)
378374, 375, 376, 377, 164syl112anc 1321 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → ((2 · 𝑢) ≤ 𝑀𝑢 ≤ (𝑀 / 2)))
379372, 378mpbid 220 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 𝑢 ≤ (𝑀 / 2))
38012ad2antrr 757 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (𝑀 / 2) ∈ ℝ)
381 simprl 789 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 𝑢 ∈ ℤ)
382380, 381, 154syl2anc 690 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (𝑢 ≤ (𝑀 / 2) ↔ 𝑢 ≤ (⌊‘(𝑀 / 2))))
383379, 382mpbid 220 . . . . . . . . . . . . . . . 16 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 𝑢 ≤ (⌊‘(𝑀 / 2)))
384 2t0e0 11033 . . . . . . . . . . . . . . . . . . . . 21 (2 · 0) = 0
385 elfznn 12199 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1st𝑧) ∈ (1...𝑀) → (1st𝑧) ∈ ℕ)
386369, 385syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (1st𝑧) ∈ ℕ)
387364, 386eqeltrd 2687 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (2 · 𝑢) ∈ ℕ)
388387nngt0d 10914 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 0 < (2 · 𝑢))
389384, 388syl5eqbr 4612 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (2 · 0) < (2 · 𝑢))
390 0red 9898 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 0 ∈ ℝ)
391 ltmul2 10726 . . . . . . . . . . . . . . . . . . . . 21 ((0 ∈ ℝ ∧ 𝑢 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (0 < 𝑢 ↔ (2 · 0) < (2 · 𝑢)))
392390, 374, 376, 377, 391syl112anc 1321 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (0 < 𝑢 ↔ (2 · 0) < (2 · 𝑢)))
393389, 392mpbird 245 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 0 < 𝑢)
394 elnnz 11223 . . . . . . . . . . . . . . . . . . 19 (𝑢 ∈ ℕ ↔ (𝑢 ∈ ℤ ∧ 0 < 𝑢))
395381, 393, 394sylanbrc 694 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 𝑢 ∈ ℕ)
396395, 286syl6eleq 2697 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 𝑢 ∈ (ℤ‘1))
39713ad2antrr 757 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (⌊‘(𝑀 / 2)) ∈ ℤ)
398 elfz5 12163 . . . . . . . . . . . . . . . . 17 ((𝑢 ∈ (ℤ‘1) ∧ (⌊‘(𝑀 / 2)) ∈ ℤ) → (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ↔ 𝑢 ≤ (⌊‘(𝑀 / 2))))
399396, 397, 398syl2anc 690 . . . . . . . . . . . . . . . 16 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ↔ 𝑢 ≤ (⌊‘(𝑀 / 2))))
400383, 399mpbird 245 . . . . . . . . . . . . . . 15 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → 𝑢 ∈ (1...(⌊‘(𝑀 / 2))))
401400, 364jca 552 . . . . . . . . . . . . . 14 (((𝜑𝑧𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧))) → (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ (2 · 𝑢) = (1st𝑧)))
402401ex 448 . . . . . . . . . . . . 13 ((𝜑𝑧𝑆) → ((𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st𝑧)) → (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ (2 · 𝑢) = (1st𝑧))))
403402reximdv2 2996 . . . . . . . . . . . 12 ((𝜑𝑧𝑆) → (∃𝑢 ∈ ℤ (2 · 𝑢) = (1st𝑧) → ∃𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(2 · 𝑢) = (1st𝑧)))
404363, 403impbid2 214 . . . . . . . . . . 11 ((𝜑𝑧𝑆) → (∃𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(2 · 𝑢) = (1st𝑧) ↔ ∃𝑢 ∈ ℤ (2 · 𝑢) = (1st𝑧)))
405 2z 11245 . . . . . . . . . . . 12 2 ∈ ℤ
406 elfzelz 12171 . . . . . . . . . . . . 13 ((1st𝑧) ∈ (1...𝑀) → (1st𝑧) ∈ ℤ)
407368, 406syl 17 . . . . . . . . . . . 12 ((𝜑𝑧𝑆) → (1st𝑧) ∈ ℤ)
408 divides 14772 . . . . . . . . . . . 12 ((2 ∈ ℤ ∧ (1st𝑧) ∈ ℤ) → (2 ∥ (1st𝑧) ↔ ∃𝑢 ∈ ℤ (𝑢 · 2) = (1st𝑧)))
409405, 407, 408sylancr 693 . . . . . . . . . . 11 ((𝜑𝑧𝑆) → (2 ∥ (1st𝑧) ↔ ∃𝑢 ∈ ℤ (𝑢 · 2) = (1st𝑧)))
410361, 404, 4093bitr4d 298 . . . . . . . . . 10 ((𝜑𝑧𝑆) → (∃𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(2 · 𝑢) = (1st𝑧) ↔ 2 ∥ (1st𝑧)))
411410rabbidva 3162 . . . . . . . . 9 (𝜑 → {𝑧𝑆 ∣ ∃𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(2 · 𝑢) = (1st𝑧)} = {𝑧𝑆 ∣ 2 ∥ (1st𝑧)})
412354, 411syl5eq 2655 . . . . . . . 8 (𝜑 𝑢 ∈ (1...(⌊‘(𝑀 / 2))){𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)} = {𝑧𝑆 ∣ 2 ∥ (1st𝑧)})
413412fveq2d 6092 . . . . . . 7 (𝜑 → (#‘ 𝑢 ∈ (1...(⌊‘(𝑀 / 2))){𝑧𝑆 ∣ (2 · 𝑢) = (1st𝑧)}) = (#‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)}))
414334, 353, 4133eqtr2d 2649 . . . . . 6 (𝜑 → Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = (#‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)}))
415414oveq2d 6543 . . . . 5 (𝜑 → (-1↑Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (-1↑(#‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)})))
4161, 2, 3, 5, 250, 103lgsquadlem1 24850 . . . . 5 (𝜑 → (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (-1↑(#‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})))
417415, 416oveq12d 6545 . . . 4 (𝜑 → ((-1↑Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) · (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = ((-1↑(#‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)})) · (-1↑(#‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))))
418118, 417eqtr4d 2646 . . 3 (𝜑 → (-1↑((#‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)}) + (#‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))) = ((-1↑Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) · (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
419 unrab 3856 . . . . . . 7 ({𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∪ {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) = {𝑧𝑆 ∣ (2 ∥ (1st𝑧) ∨ ¬ 2 ∥ (1st𝑧))}
420 exmid 429 . . . . . . . . 9 (2 ∥ (1st𝑧) ∨ ¬ 2 ∥ (1st𝑧))
421420rgenw 2907 . . . . . . . 8 𝑧𝑆 (2 ∥ (1st𝑧) ∨ ¬ 2 ∥ (1st𝑧))
422 rabid2 3095 . . . . . . . 8 (𝑆 = {𝑧𝑆 ∣ (2 ∥ (1st𝑧) ∨ ¬ 2 ∥ (1st𝑧))} ↔ ∀𝑧𝑆 (2 ∥ (1st𝑧) ∨ ¬ 2 ∥ (1st𝑧)))
423421, 422mpbir 219 . . . . . . 7 𝑆 = {𝑧𝑆 ∣ (2 ∥ (1st𝑧) ∨ ¬ 2 ∥ (1st𝑧))}
424419, 423eqtr4i 2634 . . . . . 6 ({𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∪ {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) = 𝑆
425424fveq2i 6091 . . . . 5 (#‘({𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∪ {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) = (#‘𝑆)
426 inrab 3857 . . . . . . 7 ({𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∩ {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) = {𝑧𝑆 ∣ (2 ∥ (1st𝑧) ∧ ¬ 2 ∥ (1st𝑧))}
427 pm3.24 921 . . . . . . . . . 10 ¬ (2 ∥ (1st𝑧) ∧ ¬ 2 ∥ (1st𝑧))
428427a1i 11 . . . . . . . . 9 (𝜑 → ¬ (2 ∥ (1st𝑧) ∧ ¬ 2 ∥ (1st𝑧)))
429428ralrimivw 2949 . . . . . . . 8 (𝜑 → ∀𝑧𝑆 ¬ (2 ∥ (1st𝑧) ∧ ¬ 2 ∥ (1st𝑧)))
430 rabeq0 3910 . . . . . . . 8 ({𝑧𝑆 ∣ (2 ∥ (1st𝑧) ∧ ¬ 2 ∥ (1st𝑧))} = ∅ ↔ ∀𝑧𝑆 ¬ (2 ∥ (1st𝑧) ∧ ¬ 2 ∥ (1st𝑧)))
431429, 430sylibr 222 . . . . . . 7 (𝜑 → {𝑧𝑆 ∣ (2 ∥ (1st𝑧) ∧ ¬ 2 ∥ (1st𝑧))} = ∅)
432426, 431syl5eq 2655 . . . . . 6 (𝜑 → ({𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∩ {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) = ∅)
433 hashun 12987 . . . . . 6 (({𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∈ Fin ∧ {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)} ∈ Fin ∧ ({𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∩ {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}) = ∅) → (#‘({𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∪ {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) = ((#‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)}) + (#‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})))
434115, 110, 432, 433syl3anc 1317 . . . . 5 (𝜑 → (#‘({𝑧𝑆 ∣ 2 ∥ (1st𝑧)} ∪ {𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) = ((#‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)}) + (#‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})))
435425, 434syl5reqr 2658 . . . 4 (𝜑 → ((#‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)}) + (#‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)})) = (#‘𝑆))
436435oveq2d 6543 . . 3 (𝜑 → (-1↑((#‘{𝑧𝑆 ∣ 2 ∥ (1st𝑧)}) + (#‘{𝑧𝑆 ∣ ¬ 2 ∥ (1st𝑧)}))) = (-1↑(#‘𝑆)))
43799, 418, 4363eqtr2d 2649 . 2 (𝜑 → (-1↑(Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = (-1↑(#‘𝑆)))
4384, 84, 4373eqtrd 2647 1 (𝜑 → (𝑄 /L 𝑃) = (-1↑(#‘𝑆)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wo 381  wa 382  w3a 1030   = wceq 1474  wcel 1976  wne 2779  wral 2895  wrex 2896  {crab 2899  cdif 3536  cun 3537  cin 3538  wss 3539  c0 3873  {csn 4124  cop 4130   ciun 4449  Disj wdisj 4547   class class class wbr 4577  {copab 4636   × cxp 5026  Rel wrel 5033  cfv 5790  (class class class)co 6527  1st c1st 7035  cen 7816  Fincfn 7819  cc 9791  cr 9792  0cc0 9793  1c1 9794   + caddc 9796   · cmul 9798   < clt 9931  cle 9932  cmin 10118  -cneg 10119   / cdiv 10536  cn 10870  2c2 10920  0cn0 11142  cz 11213  cuz 11522  +crp 11667  ...cfz 12155  cfl 12411  cexp 12680  #chash 12937  Σcsu 14213  cdvds 14770   gcd cgcd 15003  cprime 15172   /L clgs 24764
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6825  ax-inf2 8399  ax-cnex 9849  ax-resscn 9850  ax-1cn 9851  ax-icn 9852  ax-addcl 9853  ax-addrcl 9854  ax-mulcl 9855  ax-mulrcl 9856  ax-mulcom 9857  ax-addass 9858  ax-mulass 9859  ax-distr 9860  ax-i2m1 9861  ax-1ne0 9862  ax-1rid 9863  ax-rnegex 9864  ax-rrecex 9865  ax-cnre 9866  ax-pre-lttri 9867  ax-pre-lttrn 9868  ax-pre-ltadd 9869  ax-pre-mulgt0 9870  ax-pre-sup 9871  ax-addf 9872  ax-mulf 9873
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-int 4405  df-iun 4451  df-disj 4548  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-se 4988  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-isom 5799  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-of 6773  df-om 6936  df-1st 7037  df-2nd 7038  df-supp 7161  df-tpos 7217  df-wrecs 7272  df-recs 7333  df-rdg 7371  df-1o 7425  df-2o 7426  df-oadd 7429  df-er 7607  df-ec 7609  df-qs 7613  df-map 7724  df-en 7820  df-dom 7821  df-sdom 7822  df-fin 7823  df-fsupp 8137  df-sup 8209  df-inf 8210  df-oi 8276  df-card 8626  df-cda 8851  df-pnf 9933  df-mnf 9934  df-xr 9935  df-ltxr 9936  df-le 9937  df-sub 10120  df-neg 10121  df-div 10537  df-nn 10871  df-2 10929  df-3 10930  df-4 10931  df-5 10932  df-6 10933  df-7 10934  df-8 10935  df-9 10936  df-n0 11143  df-z 11214  df-dec 11329  df-uz 11523  df-q 11624  df-rp 11668  df-fz 12156  df-fzo 12293  df-fl 12413  df-mod 12489  df-seq 12622  df-exp 12681  df-hash 12938  df-cj 13636  df-re 13637  df-im 13638  df-sqrt 13772  df-abs 13773  df-clim 14016  df-sum 14214  df-dvds 14771  df-gcd 15004  df-prm 15173  df-phi 15258  df-pc 15329  df-struct 15646  df-ndx 15647  df-slot 15648  df-base 15649  df-sets 15650  df-ress 15651  df-plusg 15730  df-mulr 15731  df-starv 15732  df-sca 15733  df-vsca 15734  df-ip 15735  df-tset 15736  df-ple 15737  df-ds 15740  df-unif 15741  df-0g 15874  df-gsum 15875  df-imas 15940  df-qus 15941  df-mgm 17014  df-sgrp 17056  df-mnd 17067  df-mhm 17107  df-submnd 17108  df-grp 17197  df-minusg 17198  df-sbg 17199  df-mulg 17313  df-subg 17363  df-nsg 17364  df-eqg 17365  df-ghm 17430  df-cntz 17522  df-cmn 17967  df-abl 17968  df-mgp 18262  df-ur 18274  df-ring 18321  df-cring 18322  df-oppr 18395  df-dvdsr 18413  df-unit 18414  df-invr 18444  df-dvr 18455  df-rnghom 18487  df-drng 18521  df-field 18522  df-subrg 18550  df-lmod 18637  df-lss 18703  df-lsp 18742  df-sra 18942  df-rgmod 18943  df-lidl 18944  df-rsp 18945  df-2idl 19002  df-nzr 19028  df-rlreg 19053  df-domn 19054  df-idom 19055  df-cnfld 19517  df-zring 19587  df-zrh 19619  df-zn 19622  df-lgs 24765
This theorem is referenced by:  lgsquadlem3  24852
  Copyright terms: Public domain W3C validator