Theorem lgsquadlem2 15625

Description: Lemma for lgsquad 15627. Count the members of 𝑆 with even coordinates, and combine with lgsquadlem1 15624 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.

Step	Hyp	Ref	Expression
1		lgseisen.1	. . 3 ⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))
2		lgseisen.2	. . 3 ⊢ (𝜑 → 𝑄 ∈ (ℙ ∖ {2}))
3		lgseisen.3	. . 3 ⊢ (𝜑 → 𝑃 ≠ 𝑄)
4	1, 2, 3	lgseisen 15621	. 2 ⊢ (𝜑 → (𝑄 /L 𝑃) = (-1↑Σ𝑢 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
5		lgsquad.4	. . . . . 6 ⊢ 𝑀 = ((𝑃 − 1) / 2)
6	5	oveq2i 5967	. . . . 5 ⊢ (1...𝑀) = (1...((𝑃 − 1) / 2))
7	6	sumeq1i 11744	. . . 4 ⊢ Σ𝑢 ∈ (1...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = Σ𝑢 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))
8	1, 5	gausslemma2dlem0b 15597	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℕ)
9	8	nnzd 9509	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ ℤ)
10		2nn 9213	. . . . . . . . . 10 ⊢ 2 ∈ ℕ
11		znq 9760	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℤ ∧ 2 ∈ ℕ) → (𝑀 / 2) ∈ ℚ)
12	9, 10, 11	sylancl 413	. . . . . . . . 9 ⊢ (𝜑 → (𝑀 / 2) ∈ ℚ)
13	12	flqcld 10437	. . . . . . . 8 ⊢ (𝜑 → (⌊‘(𝑀 / 2)) ∈ ℤ)
14	13	zred 9510	. . . . . . 7 ⊢ (𝜑 → (⌊‘(𝑀 / 2)) ∈ ℝ)
15	14	ltp1d 9018	. . . . . 6 ⊢ (𝜑 → (⌊‘(𝑀 / 2)) < ((⌊‘(𝑀 / 2)) + 1))
16		fzdisj 10189	. . . . . 6 ⊢ ((⌊‘(𝑀 / 2)) < ((⌊‘(𝑀 / 2)) + 1) → ((1...(⌊‘(𝑀 / 2))) ∩ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) = ∅)
17	15, 16	syl 14	. . . . 5 ⊢ (𝜑 → ((1...(⌊‘(𝑀 / 2))) ∩ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) = ∅)
18	8	nnrpd 9831	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℝ+)
19	18	rphalfcld 9846	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀 / 2) ∈ ℝ+)
20	19	rpge0d 9837	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ (𝑀 / 2))
21		flqge0nn0 10453	. . . . . . . . 9 ⊢ (((𝑀 / 2) ∈ ℚ ∧ 0 ≤ (𝑀 / 2)) → (⌊‘(𝑀 / 2)) ∈ ℕ0)
22	12, 20, 21	syl2anc 411	. . . . . . . 8 ⊢ (𝜑 → (⌊‘(𝑀 / 2)) ∈ ℕ0)
23	8	nnnn0d 9363	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℕ0)
24	8	nnred 9064	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ ℝ)
25		rphalflt 9820	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℝ+ → (𝑀 / 2) < 𝑀)
26	18, 25	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀 / 2) < 𝑀)
27		flqlt 10443	. . . . . . . . . . 11 ⊢ (((𝑀 / 2) ∈ ℚ ∧ 𝑀 ∈ ℤ) → ((𝑀 / 2) < 𝑀 ↔ (⌊‘(𝑀 / 2)) < 𝑀))
28	12, 9, 27	syl2anc 411	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑀 / 2) < 𝑀 ↔ (⌊‘(𝑀 / 2)) < 𝑀))
29	26, 28	mpbid 147	. . . . . . . . 9 ⊢ (𝜑 → (⌊‘(𝑀 / 2)) < 𝑀)
30	14, 24, 29	ltled 8206	. . . . . . . 8 ⊢ (𝜑 → (⌊‘(𝑀 / 2)) ≤ 𝑀)
31		elfz2nn0 10249	. . . . . . . 8 ⊢ ((⌊‘(𝑀 / 2)) ∈ (0...𝑀) ↔ ((⌊‘(𝑀 / 2)) ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ (⌊‘(𝑀 / 2)) ≤ 𝑀))
32	22, 23, 30, 31	syl3anbrc 1184	. . . . . . 7 ⊢ (𝜑 → (⌊‘(𝑀 / 2)) ∈ (0...𝑀))
33		nn0uz 9698	. . . . . . . . 9 ⊢ ℕ0 = (ℤ≥‘0)
34	23, 33	eleqtrdi 2299	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘0))
35		elfzp12 10236	. . . . . . . 8 ⊢ (𝑀 ∈ (ℤ≥‘0) → ((⌊‘(𝑀 / 2)) ∈ (0...𝑀) ↔ ((⌊‘(𝑀 / 2)) = 0 ∨ (⌊‘(𝑀 / 2)) ∈ ((0 + 1)...𝑀))))
36	34, 35	syl 14	. . . . . . 7 ⊢ (𝜑 → ((⌊‘(𝑀 / 2)) ∈ (0...𝑀) ↔ ((⌊‘(𝑀 / 2)) = 0 ∨ (⌊‘(𝑀 / 2)) ∈ ((0 + 1)...𝑀))))
37	32, 36	mpbid 147	. . . . . 6 ⊢ (𝜑 → ((⌊‘(𝑀 / 2)) = 0 ∨ (⌊‘(𝑀 / 2)) ∈ ((0 + 1)...𝑀)))
38		un0 3498	. . . . . . . . 9 ⊢ ((1...𝑀) ∪ ∅) = (1...𝑀)
39		uncom 3321	. . . . . . . . 9 ⊢ ((1...𝑀) ∪ ∅) = (∅ ∪ (1...𝑀))
40	38, 39	eqtr3i 2229	. . . . . . . 8 ⊢ (1...𝑀) = (∅ ∪ (1...𝑀))
41		oveq2 5964	. . . . . . . . . 10 ⊢ ((⌊‘(𝑀 / 2)) = 0 → (1...(⌊‘(𝑀 / 2))) = (1...0))
42		fz10 10183	. . . . . . . . . 10 ⊢ (1...0) = ∅
43	41, 42	eqtrdi 2255	. . . . . . . . 9 ⊢ ((⌊‘(𝑀 / 2)) = 0 → (1...(⌊‘(𝑀 / 2))) = ∅)
44		oveq1 5963	. . . . . . . . . . 11 ⊢ ((⌊‘(𝑀 / 2)) = 0 → ((⌊‘(𝑀 / 2)) + 1) = (0 + 1))
45		0p1e1 9165	. . . . . . . . . . 11 ⊢ (0 + 1) = 1
46	44, 45	eqtrdi 2255	. . . . . . . . . 10 ⊢ ((⌊‘(𝑀 / 2)) = 0 → ((⌊‘(𝑀 / 2)) + 1) = 1)
47	46	oveq1d 5971	. . . . . . . . 9 ⊢ ((⌊‘(𝑀 / 2)) = 0 → (((⌊‘(𝑀 / 2)) + 1)...𝑀) = (1...𝑀))
48	43, 47	uneq12d 3332	. . . . . . . 8 ⊢ ((⌊‘(𝑀 / 2)) = 0 → ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) = (∅ ∪ (1...𝑀)))
49	40, 48	eqtr4id 2258	. . . . . . 7 ⊢ ((⌊‘(𝑀 / 2)) = 0 → (1...𝑀) = ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀)))
50		fzsplit 10188	. . . . . . . 8 ⊢ ((⌊‘(𝑀 / 2)) ∈ (1...𝑀) → (1...𝑀) = ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀)))
51	45	oveq1i 5966	. . . . . . . 8 ⊢ ((0 + 1)...𝑀) = (1...𝑀)
52	50, 51	eleq2s 2301	. . . . . . 7 ⊢ ((⌊‘(𝑀 / 2)) ∈ ((0 + 1)...𝑀) → (1...𝑀) = ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀)))
53	49, 52	jaoi 718	. . . . . 6 ⊢ (((⌊‘(𝑀 / 2)) = 0 ∨ (⌊‘(𝑀 / 2)) ∈ ((0 + 1)...𝑀)) → (1...𝑀) = ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀)))
54	37, 53	syl 14	. . . . 5 ⊢ (𝜑 → (1...𝑀) = ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀)))
55		1zzd 9414	. . . . . 6 ⊢ (𝜑 → 1 ∈ ℤ)
56	55, 9	fzfigd 10593	. . . . 5 ⊢ (𝜑 → (1...𝑀) ∈ Fin)
57	2	gausslemma2dlem0a 15596	. . . . . . . . . 10 ⊢ (𝜑 → 𝑄 ∈ ℕ)
58	57	nnzd 9509	. . . . . . . . 9 ⊢ (𝜑 → 𝑄 ∈ ℤ)
59	1	gausslemma2dlem0a 15596	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃 ∈ ℕ)
60	59	adantr 276	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → 𝑃 ∈ ℕ)
61		znq 9760	. . . . . . . . 9 ⊢ ((𝑄 ∈ ℤ ∧ 𝑃 ∈ ℕ) → (𝑄 / 𝑃) ∈ ℚ)
62	58, 60, 61	syl2an2r 595	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → (𝑄 / 𝑃) ∈ ℚ)
63		elfznn 10191	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ (1...𝑀) → 𝑢 ∈ ℕ)
64	63	adantl 277	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → 𝑢 ∈ ℕ)
65		nnmulcl 9072	. . . . . . . . . . 11 ⊢ ((2 ∈ ℕ ∧ 𝑢 ∈ ℕ) → (2 · 𝑢) ∈ ℕ)
66	10, 64, 65	sylancr 414	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → (2 · 𝑢) ∈ ℕ)
67	66	nnzd 9509	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → (2 · 𝑢) ∈ ℤ)
68		zq 9762	. . . . . . . . 9 ⊢ ((2 · 𝑢) ∈ ℤ → (2 · 𝑢) ∈ ℚ)
69	67, 68	syl 14	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → (2 · 𝑢) ∈ ℚ)
70		qmulcl 9773	. . . . . . . 8 ⊢ (((𝑄 / 𝑃) ∈ ℚ ∧ (2 · 𝑢) ∈ ℚ) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℚ)
71	62, 69, 70	syl2anc 411	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℚ)
72	57	nnrpd 9831	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑄 ∈ ℝ+)
73	59	nnrpd 9831	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑃 ∈ ℝ+)
74	72, 73	rpdivcld 9851	. . . . . . . . . 10 ⊢ (𝜑 → (𝑄 / 𝑃) ∈ ℝ+)
75	74	adantr 276	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → (𝑄 / 𝑃) ∈ ℝ+)
76	66	nnrpd 9831	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → (2 · 𝑢) ∈ ℝ+)
77	75, 76	rpmulcld 9850	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ+)
78	77	rpge0d 9837	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → 0 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)))
79		flqge0nn0 10453	. . . . . . 7 ⊢ ((((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℚ ∧ 0 ≤ ((𝑄 / 𝑃) · (2 · 𝑢))) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℕ0)
80	71, 78, 79	syl2anc 411	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℕ0)
81	80	nn0cnd 9365	. . . . 5 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℂ)
82	17, 54, 56, 81	fsumsplit 11788	. . . 4 ⊢ (𝜑 → Σ𝑢 ∈ (1...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = (Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
83	7, 82	eqtr3id 2253	. . 3 ⊢ (𝜑 → Σ𝑢 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = (Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
84	83	oveq2d 5972	. 2 ⊢ (𝜑 → (-1↑Σ𝑢 ∈ (1...((𝑃 − 1) / 2))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (-1↑(Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
85		neg1cn 9156	. . . . 5 ⊢ -1 ∈ ℂ
86	85	a1i 9	. . . 4 ⊢ (𝜑 → -1 ∈ ℂ)
87	13	peano2zd 9513	. . . . . 6 ⊢ (𝜑 → ((⌊‘(𝑀 / 2)) + 1) ∈ ℤ)
88	87, 9	fzfigd 10593	. . . . 5 ⊢ (𝜑 → (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∈ Fin)
89		ssun2 3341	. . . . . . . 8 ⊢ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ⊆ ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀))
90	89, 54	sseqtrrid 3248	. . . . . . 7 ⊢ (𝜑 → (((⌊‘(𝑀 / 2)) + 1)...𝑀) ⊆ (1...𝑀))
91	90	sselda 3197	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ∈ (1...𝑀))
92	91, 80	syldan 282	. . . . 5 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℕ0)
93	88, 92	fsumnn0cl 11784	. . . 4 ⊢ (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℕ0)
94	55, 13	fzfigd 10593	. . . . 5 ⊢ (𝜑 → (1...(⌊‘(𝑀 / 2))) ∈ Fin)
95		ssun1 3340	. . . . . . . 8 ⊢ (1...(⌊‘(𝑀 / 2))) ⊆ ((1...(⌊‘(𝑀 / 2))) ∪ (((⌊‘(𝑀 / 2)) + 1)...𝑀))
96	95, 54	sseqtrrid 3248	. . . . . . 7 ⊢ (𝜑 → (1...(⌊‘(𝑀 / 2))) ⊆ (1...𝑀))
97	96	sselda 3197	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ∈ (1...𝑀))
98	97, 80	syldan 282	. . . . 5 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℕ0)
99	94, 98	fsumnn0cl 11784	. . . 4 ⊢ (𝜑 → Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℕ0)
100	86, 93, 99	expaddd 10837	. . 3 ⊢ (𝜑 → (-1↑(Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = ((-1↑Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) · (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
101		lgsquad.5	. . . . . . 7 ⊢ 𝑁 = ((𝑄 − 1) / 2)
102		lgsquad.6	. . . . . . 7 ⊢ 𝑆 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))}
103	1, 2, 3, 5, 101, 102	lgsquadlemofi 15623	. . . . . 6 ⊢ (𝜑 → {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st ‘𝑧)} ∈ Fin)
104		hashcl 10943	. . . . . 6 ⊢ ({𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st ‘𝑧)} ∈ Fin → (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st ‘𝑧)}) ∈ ℕ0)
105	103, 104	syl 14	. . . . 5 ⊢ (𝜑 → (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st ‘𝑧)}) ∈ ℕ0)
106	1, 2, 3, 5, 101, 102	lgsquadlemsfi 15622	. . . . . . 7 ⊢ (𝜑 → 𝑆 ∈ Fin)
107		opabssxp 4756	. . . . . . . . . . . . . 14 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} ⊆ ((1...𝑀) × (1...𝑁))
108	102, 107	eqsstri 3229	. . . . . . . . . . . . 13 ⊢ 𝑆 ⊆ ((1...𝑀) × (1...𝑁))
109	108	sseli 3193	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ 𝑆 → 𝑧 ∈ ((1...𝑀) × (1...𝑁)))
110		xp1st 6263	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ((1...𝑀) × (1...𝑁)) → (1st ‘𝑧) ∈ (1...𝑀))
111	109, 110	syl 14	. . . . . . . . . . 11 ⊢ (𝑧 ∈ 𝑆 → (1st ‘𝑧) ∈ (1...𝑀))
112	111	elfzelzd 10163	. . . . . . . . . 10 ⊢ (𝑧 ∈ 𝑆 → (1st ‘𝑧) ∈ ℤ)
113	112	adantl 277	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (1st ‘𝑧) ∈ ℤ)
114		dvdsdc 12179	. . . . . . . . 9 ⊢ ((2 ∈ ℕ ∧ (1st ‘𝑧) ∈ ℤ) → DECID 2 ∥ (1st ‘𝑧))
115	10, 113, 114	sylancr 414	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → DECID 2 ∥ (1st ‘𝑧))
116	115	ralrimiva 2580	. . . . . . 7 ⊢ (𝜑 → ∀𝑧 ∈ 𝑆 DECID 2 ∥ (1st ‘𝑧))
117	106, 116	ssfirab 7047	. . . . . 6 ⊢ (𝜑 → {𝑧 ∈ 𝑆 ∣ 2 ∥ (1st ‘𝑧)} ∈ Fin)
118		hashcl 10943	. . . . . 6 ⊢ ({𝑧 ∈ 𝑆 ∣ 2 ∥ (1st ‘𝑧)} ∈ Fin → (♯‘{𝑧 ∈ 𝑆 ∣ 2 ∥ (1st ‘𝑧)}) ∈ ℕ0)
119	117, 118	syl 14	. . . . 5 ⊢ (𝜑 → (♯‘{𝑧 ∈ 𝑆 ∣ 2 ∥ (1st ‘𝑧)}) ∈ ℕ0)
120	86, 105, 119	expaddd 10837	. . . 4 ⊢ (𝜑 → (-1↑((♯‘{𝑧 ∈ 𝑆 ∣ 2 ∥ (1st ‘𝑧)}) + (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st ‘𝑧)}))) = ((-1↑(♯‘{𝑧 ∈ 𝑆 ∣ 2 ∥ (1st ‘𝑧)})) · (-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st ‘𝑧)}))))
121	97, 66	syldan 282	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (2 · 𝑢) ∈ ℕ)
122		1zzd 9414	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 1 ∈ ℤ)
123	98	nn0zd 9508	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ)
124	122, 123	fzfigd 10593	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ Fin)
125		xpsnen2g 6938	. . . . . . . . . . 11 ⊢ (((2 · 𝑢) ∈ ℕ ∧ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ Fin) → ({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ≈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
126	121, 124, 125	syl2anc 411	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ≈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
127		snfig 6919	. . . . . . . . . . . . 13 ⊢ ((2 · 𝑢) ∈ ℕ → {(2 · 𝑢)} ∈ Fin)
128	121, 127	syl 14	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → {(2 · 𝑢)} ∈ Fin)
129		xpfi 7043	. . . . . . . . . . . 12 ⊢ (({(2 · 𝑢)} ∈ Fin ∧ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ Fin) → ({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ∈ Fin)
130	128, 124, 129	syl2anc 411	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ∈ Fin)
131		hashen 10946	. . . . . . . . . . 11 ⊢ ((({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ∈ Fin ∧ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ Fin) → ((♯‘({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) = (♯‘(1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ↔ ({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ≈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
132	130, 124, 131	syl2anc 411	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((♯‘({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) = (♯‘(1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ↔ ({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ≈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
133	126, 132	mpbird 167	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (♯‘({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) = (♯‘(1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
134		ssrab2 3282	. . . . . . . . . . . . 13 ⊢ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} ⊆ 𝑆
135	102	relopabiv 4808	. . . . . . . . . . . . 13 ⊢ Rel 𝑆
136		relss 4769	. . . . . . . . . . . . 13 ⊢ ({𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} ⊆ 𝑆 → (Rel 𝑆 → Rel {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)}))
137	134, 135, 136	mp2 16	. . . . . . . . . . . 12 ⊢ Rel {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)}
138		relxp 4791	. . . . . . . . . . . 12 ⊢ Rel ({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
139	102	eleq2i 2273	. . . . . . . . . . . . . . . 16 ⊢ (⟨𝑥, 𝑦⟩ ∈ 𝑆 ↔ ⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))})
140		opabidw 4310	. . . . . . . . . . . . . . . 16 ⊢ (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} ↔ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))
141	139, 140	bitri 184	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑥, 𝑦⟩ ∈ 𝑆 ↔ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))
142		anass 401	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁) ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢))) ↔ (𝑦 ∈ ℕ ∧ (𝑦 ≤ 𝑁 ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)))))
143	121	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2 · 𝑢) ∈ ℕ)
144	143	nnred 9064	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2 · 𝑢) ∈ ℝ)
145	59	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℕ)
146	145	nnred 9064	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℝ)
147	146	rehalfcld 9299	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 / 2) ∈ ℝ)
148	24	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑀 ∈ ℝ)
149	148	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑀 ∈ ℝ)
150		elfzle2 10165	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) → 𝑢 ≤ (⌊‘(𝑀 / 2)))
151	150	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ≤ (⌊‘(𝑀 / 2)))
152		elfzelz 10162	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) → 𝑢 ∈ ℤ)
153		flqge 10442	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑀 / 2) ∈ ℚ ∧ 𝑢 ∈ ℤ) → (𝑢 ≤ (𝑀 / 2) ↔ 𝑢 ≤ (⌊‘(𝑀 / 2))))
154	12, 152, 153	syl2an 289	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (𝑢 ≤ (𝑀 / 2) ↔ 𝑢 ≤ (⌊‘(𝑀 / 2))))
155	151, 154	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ≤ (𝑀 / 2))
156		elfznn 10191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) → 𝑢 ∈ ℕ)
157	156	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ∈ ℕ)
158	157	nnred 9064	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ∈ ℝ)
159		2re 9121	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 2 ∈ ℝ
160	159	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 2 ∈ ℝ)
161		2pos 9142	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 0 < 2
162	161	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 0 < 2)
163		lemuldiv2 8970	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑢 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 𝑢) ≤ 𝑀 ↔ 𝑢 ≤ (𝑀 / 2)))
164	158, 148, 160, 162, 163	syl112anc 1254	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((2 · 𝑢) ≤ 𝑀 ↔ 𝑢 ≤ (𝑀 / 2)))
165	155, 164	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (2 · 𝑢) ≤ 𝑀)
166	165	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2 · 𝑢) ≤ 𝑀)
167	146	ltm1d 9020	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 − 1) < 𝑃)
168		peano2rem 8354	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑃 ∈ ℝ → (𝑃 − 1) ∈ ℝ)
169	146, 168	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 − 1) ∈ ℝ)
170	159	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 2 ∈ ℝ)
171	161	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 0 < 2)
172		ltdiv1 8956	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑃 − 1) ∈ ℝ ∧ 𝑃 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((𝑃 − 1) < 𝑃 ↔ ((𝑃 − 1) / 2) < (𝑃 / 2)))
173	169, 146, 170, 171, 172	syl112anc 1254	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑃 − 1) < 𝑃 ↔ ((𝑃 − 1) / 2) < (𝑃 / 2)))
174	167, 173	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑃 − 1) / 2) < (𝑃 / 2))
175	5, 174	eqbrtrid 4085	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑀 < (𝑃 / 2))
176	144, 149, 147, 166, 175	lelttrd 8212	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2 · 𝑢) < (𝑃 / 2))
177	145	nnrpd 9831	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℝ+)
178		rphalflt 9820	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑃 ∈ ℝ+ → (𝑃 / 2) < 𝑃)
179	177, 178	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 / 2) < 𝑃)
180	144, 147, 146, 176, 179	lttrd 8213	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2 · 𝑢) < 𝑃)
181	143	nnzd 9509	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2 · 𝑢) ∈ ℤ)
182	145	nnzd 9509	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℤ)
183		zltnle 9433	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((2 · 𝑢) ∈ ℤ ∧ 𝑃 ∈ ℤ) → ((2 · 𝑢) < 𝑃 ↔ ¬ 𝑃 ≤ (2 · 𝑢)))
184	181, 182, 183	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((2 · 𝑢) < 𝑃 ↔ ¬ 𝑃 ≤ (2 · 𝑢)))
185	180, 184	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ¬ 𝑃 ≤ (2 · 𝑢))
186	1	eldifad 3181	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝑃 ∈ ℙ)
187	186	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℙ)
188		prmz 12503	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
189	187, 188	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℤ)
190		dvdsle 12225	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑃 ∈ ℤ ∧ (2 · 𝑢) ∈ ℕ) → (𝑃 ∥ (2 · 𝑢) → 𝑃 ≤ (2 · 𝑢)))
191	189, 143, 190	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 ∥ (2 · 𝑢) → 𝑃 ≤ (2 · 𝑢)))
192	185, 191	mtod 665	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ¬ 𝑃 ∥ (2 · 𝑢))
193	2	eldifad 3181	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝑄 ∈ ℙ)
194		prmrp 12537	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ) → ((𝑃 gcd 𝑄) = 1 ↔ 𝑃 ≠ 𝑄))
195	186, 193, 194	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((𝑃 gcd 𝑄) = 1 ↔ 𝑃 ≠ 𝑄))
196	3, 195	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝑃 gcd 𝑄) = 1)
197	196	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 gcd 𝑄) = 1)
198	193	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈ ℙ)
199		prmz 12503	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑄 ∈ ℙ → 𝑄 ∈ ℤ)
200	198, 199	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈ ℤ)
201		coprmdvds 12484	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑃 ∈ ℤ ∧ 𝑄 ∈ ℤ ∧ (2 · 𝑢) ∈ ℤ) → ((𝑃 ∥ (𝑄 · (2 · 𝑢)) ∧ (𝑃 gcd 𝑄) = 1) → 𝑃 ∥ (2 · 𝑢)))
202	189, 200, 181, 201	syl3anc 1250	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑃 ∥ (𝑄 · (2 · 𝑢)) ∧ (𝑃 gcd 𝑄) = 1) → 𝑃 ∥ (2 · 𝑢)))
203	197, 202	mpan2d 428	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑃 ∥ (𝑄 · (2 · 𝑢)) → 𝑃 ∥ (2 · 𝑢)))
204	192, 203	mtod 665	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ¬ 𝑃 ∥ (𝑄 · (2 · 𝑢)))
205		nnz 9406	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℤ)
206	205	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ ℤ)
207		dvdsmul2 12195	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑦 ∈ ℤ ∧ 𝑃 ∈ ℤ) → 𝑃 ∥ (𝑦 · 𝑃))
208	206, 189, 207	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∥ (𝑦 · 𝑃))
209		breq2 4054	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑄 · (2 · 𝑢)) = (𝑦 · 𝑃) → (𝑃 ∥ (𝑄 · (2 · 𝑢)) ↔ 𝑃 ∥ (𝑦 · 𝑃)))
210	208, 209	syl5ibrcom 157	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 · (2 · 𝑢)) = (𝑦 · 𝑃) → 𝑃 ∥ (𝑄 · (2 · 𝑢))))
211	210	necon3bd 2420	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (¬ 𝑃 ∥ (𝑄 · (2 · 𝑢)) → (𝑄 · (2 · 𝑢)) ≠ (𝑦 · 𝑃)))
212	204, 211	mpd 13	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (2 · 𝑢)) ≠ (𝑦 · 𝑃))
213		simpr 110	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ ℕ)
214	213, 145	nnmulcld 9100	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 · 𝑃) ∈ ℕ)
215	214	nnzd 9509	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 · 𝑃) ∈ ℤ)
216	57	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑄 ∈ ℕ)
217	216, 121	nnmulcld 9100	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (𝑄 · (2 · 𝑢)) ∈ ℕ)
218	217	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (2 · 𝑢)) ∈ ℕ)
219	218	nnzd 9509	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (2 · 𝑢)) ∈ ℤ)
220		zltlen 9466	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑦 · 𝑃) ∈ ℤ ∧ (𝑄 · (2 · 𝑢)) ∈ ℤ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ↔ ((𝑦 · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ∧ (𝑄 · (2 · 𝑢)) ≠ (𝑦 · 𝑃))))
221	215, 219, 220	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ↔ ((𝑦 · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ∧ (𝑄 · (2 · 𝑢)) ≠ (𝑦 · 𝑃))))
222	212, 221	mpbiran2d 442	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ↔ (𝑦 · 𝑃) ≤ (𝑄 · (2 · 𝑢))))
223		nnre 9058	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
224	223	adantl 277	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ ℝ)
225	218	nnred 9064	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (2 · 𝑢)) ∈ ℝ)
226	145	nngt0d 9095	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 0 < 𝑃)
227		lemuldiv 8969	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑦 ∈ ℝ ∧ (𝑄 · (2 · 𝑢)) ∈ ℝ ∧ (𝑃 ∈ ℝ ∧ 0 < 𝑃)) → ((𝑦 · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ↔ 𝑦 ≤ ((𝑄 · (2 · 𝑢)) / 𝑃)))
228	224, 225, 146, 226, 227	syl112anc 1254	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ↔ 𝑦 ≤ ((𝑄 · (2 · 𝑢)) / 𝑃)))
229	216	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈ ℕ)
230	229	nncnd 9065	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈ ℂ)
231	143	nncnd 9065	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (2 · 𝑢) ∈ ℂ)
232	145	nncnd 9065	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℂ)
233	146, 226	gt0ap0d 8717	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑃 # 0)
234	230, 231, 232, 233	div23apd 8916	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 · (2 · 𝑢)) / 𝑃) = ((𝑄 / 𝑃) · (2 · 𝑢)))
235	234	breq2d 4062	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 ≤ ((𝑄 · (2 · 𝑢)) / 𝑃) ↔ 𝑦 ≤ ((𝑄 / 𝑃) · (2 · 𝑢))))
236	222, 228, 235	3bitrd 214	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ↔ 𝑦 ≤ ((𝑄 / 𝑃) · (2 · 𝑢))))
237	229	nnred 9064	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈ ℝ)
238	229	nngt0d 9095	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 0 < 𝑄)
239		ltmul2 8944	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((2 · 𝑢) ∈ ℝ ∧ (𝑃 / 2) ∈ ℝ ∧ (𝑄 ∈ ℝ ∧ 0 < 𝑄)) → ((2 · 𝑢) < (𝑃 / 2) ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · (𝑃 / 2))))
240	144, 147, 237, 238, 239	syl112anc 1254	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((2 · 𝑢) < (𝑃 / 2) ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · (𝑃 / 2))))
241	176, 240	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (2 · 𝑢)) < (𝑄 · (𝑃 / 2)))
242		2cnd 9124	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 2 ∈ ℂ)
243	170, 171	gt0ap0d 8717	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 2 # 0)
244		divassap 8778	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑄 ∈ ℂ ∧ 𝑃 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 # 0)) → ((𝑄 · 𝑃) / 2) = (𝑄 · (𝑃 / 2)))
245		div23ap 8779	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑄 ∈ ℂ ∧ 𝑃 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 # 0)) → ((𝑄 · 𝑃) / 2) = ((𝑄 / 2) · 𝑃))
246	244, 245	eqtr3d 2241	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑄 ∈ ℂ ∧ 𝑃 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 # 0)) → (𝑄 · (𝑃 / 2)) = ((𝑄 / 2) · 𝑃))
247	230, 232, 242, 243, 246	syl112anc 1254	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (𝑃 / 2)) = ((𝑄 / 2) · 𝑃))
248	241, 247	breqtrd 4076	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 · (2 · 𝑢)) < ((𝑄 / 2) · 𝑃))
249	214	nnred 9064	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 · 𝑃) ∈ ℝ)
250	237	rehalfcld 9299	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 / 2) ∈ ℝ)
251	250, 146	remulcld 8118	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 / 2) · 𝑃) ∈ ℝ)
252		lttr 8161	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑦 · 𝑃) ∈ ℝ ∧ (𝑄 · (2 · 𝑢)) ∈ ℝ ∧ ((𝑄 / 2) · 𝑃) ∈ ℝ) → (((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ∧ (𝑄 · (2 · 𝑢)) < ((𝑄 / 2) · 𝑃)) → (𝑦 · 𝑃) < ((𝑄 / 2) · 𝑃)))
253	249, 225, 251, 252	syl3anc 1250	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ∧ (𝑄 · (2 · 𝑢)) < ((𝑄 / 2) · 𝑃)) → (𝑦 · 𝑃) < ((𝑄 / 2) · 𝑃)))
254	248, 253	mpan2d 428	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) → (𝑦 · 𝑃) < ((𝑄 / 2) · 𝑃)))
255		ltmul1 8680	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑦 ∈ ℝ ∧ (𝑄 / 2) ∈ ℝ ∧ (𝑃 ∈ ℝ ∧ 0 < 𝑃)) → (𝑦 < (𝑄 / 2) ↔ (𝑦 · 𝑃) < ((𝑄 / 2) · 𝑃)))
256	224, 250, 146, 226, 255	syl112anc 1254	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 < (𝑄 / 2) ↔ (𝑦 · 𝑃) < ((𝑄 / 2) · 𝑃)))
257	254, 256	sylibrd 169	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) → 𝑦 < (𝑄 / 2)))
258		peano2rem 8354	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑄 ∈ ℝ → (𝑄 − 1) ∈ ℝ)
259	237, 258	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 − 1) ∈ ℝ)
260	259	recnd 8116	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 − 1) ∈ ℂ)
261	230, 260, 242, 243	divsubdirapd 8918	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 − (𝑄 − 1)) / 2) = ((𝑄 / 2) − ((𝑄 − 1) / 2)))
262	101	oveq2i 5967	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑄 / 2) − 𝑁) = ((𝑄 / 2) − ((𝑄 − 1) / 2))
263	261, 262	eqtr4di 2257	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 − (𝑄 − 1)) / 2) = ((𝑄 / 2) − 𝑁))
264		ax-1cn 8033	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 1 ∈ ℂ
265		nncan 8316	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑄 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑄 − (𝑄 − 1)) = 1)
266	230, 264, 265	sylancl 413	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 − (𝑄 − 1)) = 1)
267	266	oveq1d 5971	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 − (𝑄 − 1)) / 2) = (1 / 2))
268		halflt1 9269	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (1 / 2) < 1
269	267, 268	eqbrtrdi 4089	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 − (𝑄 − 1)) / 2) < 1)
270	263, 269	eqbrtrrd 4074	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑄 / 2) − 𝑁) < 1)
271	2, 101	gausslemma2dlem0b 15597	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝑁 ∈ ℕ)
272	271	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑁 ∈ ℕ)
273	272	nnred 9064	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 𝑁 ∈ ℝ)
274		1red 8102	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → 1 ∈ ℝ)
275	250, 273, 274	ltsubadd2d 8631	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (((𝑄 / 2) − 𝑁) < 1 ↔ (𝑄 / 2) < (𝑁 + 1)))
276	270, 275	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑄 / 2) < (𝑁 + 1))
277		peano2re 8223	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑁 ∈ ℝ → (𝑁 + 1) ∈ ℝ)
278	273, 277	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑁 + 1) ∈ ℝ)
279		lttr 8161	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑦 ∈ ℝ ∧ (𝑄 / 2) ∈ ℝ ∧ (𝑁 + 1) ∈ ℝ) → ((𝑦 < (𝑄 / 2) ∧ (𝑄 / 2) < (𝑁 + 1)) → 𝑦 < (𝑁 + 1)))
280	224, 250, 278, 279	syl3anc 1250	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 < (𝑄 / 2) ∧ (𝑄 / 2) < (𝑁 + 1)) → 𝑦 < (𝑁 + 1)))
281	276, 280	mpan2d 428	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 < (𝑄 / 2) → 𝑦 < (𝑁 + 1)))
282	257, 281	syld 45	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) → 𝑦 < (𝑁 + 1)))
283		nnleltp1 9447	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑦 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑦 ≤ 𝑁 ↔ 𝑦 < (𝑁 + 1)))
284	213, 272, 283	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 ≤ 𝑁 ↔ 𝑦 < (𝑁 + 1)))
285	282, 284	sylibrd 169	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) → 𝑦 ≤ 𝑁))
286	285	pm4.71rd 394	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)) ↔ (𝑦 ≤ 𝑁 ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)))))
287	97, 71	syldan 282	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℚ)
288		flqge 10442	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℚ ∧ 𝑦 ∈ ℤ) → (𝑦 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)) ↔ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
289	287, 205, 288	syl2an 289	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → (𝑦 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)) ↔ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
290	236, 286, 289	3bitr3d 218	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑦 ∈ ℕ) → ((𝑦 ≤ 𝑁 ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢))) ↔ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
291	290	pm5.32da 452	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((𝑦 ∈ ℕ ∧ (𝑦 ≤ 𝑁 ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
292	142, 291	bitrid 192	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (((𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁) ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
293	292	adantr 276	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (((𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁) ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
294		simpr 110	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → 𝑥 = (2 · 𝑢))
295		nnuz 9699	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ℕ = (ℤ≥‘1)
296	121, 295	eleqtrdi 2299	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (2 · 𝑢) ∈ (ℤ≥‘1))
297	9	adantr 276	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑀 ∈ ℤ)
298		elfz5 10154	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((2 · 𝑢) ∈ (ℤ≥‘1) ∧ 𝑀 ∈ ℤ) → ((2 · 𝑢) ∈ (1...𝑀) ↔ (2 · 𝑢) ≤ 𝑀))
299	296, 297, 298	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((2 · 𝑢) ∈ (1...𝑀) ↔ (2 · 𝑢) ≤ 𝑀))
300	165, 299	mpbird 167	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (2 · 𝑢) ∈ (1...𝑀))
301	300	adantr 276	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (2 · 𝑢) ∈ (1...𝑀))
302	294, 301	eqeltrd 2283	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → 𝑥 ∈ (1...𝑀))
303	302	biantrurd 305	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (𝑦 ∈ (1...𝑁) ↔ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))))
304	271	nnzd 9509	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑁 ∈ ℤ)
305	304	ad2antrr 488	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → 𝑁 ∈ ℤ)
306		fznn 10226	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ ℤ → (𝑦 ∈ (1...𝑁) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁)))
307	305, 306	syl 14	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (𝑦 ∈ (1...𝑁) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁)))
308	303, 307	bitr3d 190	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁)))
309		oveq1 5963	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (2 · 𝑢) → (𝑥 · 𝑄) = ((2 · 𝑢) · 𝑄))
310	121	nncnd 9065	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (2 · 𝑢) ∈ ℂ)
311	216	nncnd 9065	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑄 ∈ ℂ)
312	310, 311	mulcomd 8109	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((2 · 𝑢) · 𝑄) = (𝑄 · (2 · 𝑢)))
313	309, 312	sylan9eqr 2261	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (𝑥 · 𝑄) = (𝑄 · (2 · 𝑢)))
314	313	breq2d 4062	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → ((𝑦 · 𝑃) < (𝑥 · 𝑄) ↔ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢))))
315	308, 314	anbi12d 473	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)) ↔ ((𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁) ∧ (𝑦 · 𝑃) < (𝑄 · (2 · 𝑢)))))
316	287	flqcld 10437	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ)
317		fznn 10226	. . . . . . . . . . . . . . . . . 18 ⊢ ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ → (𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
318	316, 317	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
319	318	adantr 276	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
320	293, 315, 319	3bitr4d 220	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)) ↔ 𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
321	141, 320	bitrid 192	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑥 = (2 · 𝑢)) → (⟨𝑥, 𝑦⟩ ∈ 𝑆 ↔ 𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
322	321	pm5.32da 452	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ((𝑥 = (2 · 𝑢) ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑆) ↔ (𝑥 = (2 · 𝑢) ∧ 𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
323		vex 2776	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑥 ∈ V
324		vex 2776	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑦 ∈ V
325	323, 324	op1std 6246	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (1st ‘𝑧) = 𝑥)
326	325	eqeq2d 2218	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → ((2 · 𝑢) = (1st ‘𝑧) ↔ (2 · 𝑢) = 𝑥))
327		eqcom 2208	. . . . . . . . . . . . . . . 16 ⊢ ((2 · 𝑢) = 𝑥 ↔ 𝑥 = (2 · 𝑢))
328	326, 327	bitrdi 196	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → ((2 · 𝑢) = (1st ‘𝑧) ↔ 𝑥 = (2 · 𝑢)))
329	328	elrab 2933	. . . . . . . . . . . . . 14 ⊢ (⟨𝑥, 𝑦⟩ ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} ↔ (⟨𝑥, 𝑦⟩ ∈ 𝑆 ∧ 𝑥 = (2 · 𝑢)))
330	329	biancomi 270	. . . . . . . . . . . . 13 ⊢ (⟨𝑥, 𝑦⟩ ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} ↔ (𝑥 = (2 · 𝑢) ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑆))
331		opelxp 4712	. . . . . . . . . . . . . 14 ⊢ (⟨𝑥, 𝑦⟩ ∈ ({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ↔ (𝑥 ∈ {(2 · 𝑢)} ∧ 𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
332		velsn 3654	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ {(2 · 𝑢)} ↔ 𝑥 = (2 · 𝑢))
333	332	anbi1i 458	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ {(2 · 𝑢)} ∧ 𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ↔ (𝑥 = (2 · 𝑢) ∧ 𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
334	331, 333	bitri 184	. . . . . . . . . . . . 13 ⊢ (⟨𝑥, 𝑦⟩ ∈ ({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ↔ (𝑥 = (2 · 𝑢) ∧ 𝑦 ∈ (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
335	322, 330, 334	3bitr4g 223	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (⟨𝑥, 𝑦⟩ ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} ↔ ⟨𝑥, 𝑦⟩ ∈ ({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
336	137, 138, 335	eqrelrdv 4778	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} = ({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
337	336	eqcomd 2212	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})
338	337	fveq2d 5592	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (♯‘({(2 · 𝑢)} × (1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) = (♯‘{𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)}))
339		hashfz1 10945	. . . . . . . . . 10 ⊢ ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℕ0 → (♯‘(1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))
340	98, 339	syl 14	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (♯‘(1...(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))
341	133, 338, 340	3eqtr3rd 2248	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = (♯‘{𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)}))
342	341	sumeq2dv 11749	. . . . . . 7 ⊢ (𝜑 → Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(♯‘{𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)}))
343	106	adantr 276	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑆 ∈ Fin)
344	97, 67	syldan 282	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → (2 · 𝑢) ∈ ℤ)
345		zdceq 9463	. . . . . . . . . . 11 ⊢ (((2 · 𝑢) ∈ ℤ ∧ (1st ‘𝑧) ∈ ℤ) → DECID (2 · 𝑢) = (1st ‘𝑧))
346	344, 112, 345	syl2an 289	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) ∧ 𝑧 ∈ 𝑆) → DECID (2 · 𝑢) = (1st ‘𝑧))
347	346	ralrimiva 2580	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → ∀𝑧 ∈ 𝑆 DECID (2 · 𝑢) = (1st ‘𝑧))
348	343, 347	ssfirab 7047	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} ∈ Fin)
349		fveq2 5588	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑣 → (1st ‘𝑧) = (1st ‘𝑣))
350	349	eqeq2d 2218	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑣 → ((2 · 𝑢) = (1st ‘𝑧) ↔ (2 · 𝑢) = (1st ‘𝑣)))
351	350	elrab 2933	. . . . . . . . . . . . . 14 ⊢ (𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} ↔ (𝑣 ∈ 𝑆 ∧ (2 · 𝑢) = (1st ‘𝑣)))
352	351	simprbi 275	. . . . . . . . . . . . 13 ⊢ (𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} → (2 · 𝑢) = (1st ‘𝑣))
353	352	ad2antll 491	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})) → (2 · 𝑢) = (1st ‘𝑣))
354	353	oveq1d 5971	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})) → ((2 · 𝑢) / 2) = ((1st ‘𝑣) / 2))
355	157	nncnd 9065	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...(⌊‘(𝑀 / 2)))) → 𝑢 ∈ ℂ)
356	355	adantrr 479	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})) → 𝑢 ∈ ℂ)
357		2cnd 9124	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})) → 2 ∈ ℂ)
358		2ap0 9144	. . . . . . . . . . . . 13 ⊢ 2 # 0
359	358	a1i 9	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})) → 2 # 0)
360	356, 357, 359	divcanap3d 8883	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})) → ((2 · 𝑢) / 2) = 𝑢)
361	354, 360	eqtr3d 2241	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})) → ((1st ‘𝑣) / 2) = 𝑢)
362	361	ralrimivva 2589	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑢 ∈ (1...(⌊‘(𝑀 / 2)))∀𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} ((1st ‘𝑣) / 2) = 𝑢)
363		invdisj 4043	. . . . . . . . 9 ⊢ (∀𝑢 ∈ (1...(⌊‘(𝑀 / 2)))∀𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} ((1st ‘𝑣) / 2) = 𝑢 → Disj 𝑢 ∈ (1...(⌊‘(𝑀 / 2))){𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})
364	362, 363	syl 14	. . . . . . . 8 ⊢ (𝜑 → Disj 𝑢 ∈ (1...(⌊‘(𝑀 / 2))){𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)})
365	94, 348, 364	hashiun 11859	. . . . . . 7 ⊢ (𝜑 → (♯‘∪ 𝑢 ∈ (1...(⌊‘(𝑀 / 2))){𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)}) = Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(♯‘{𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)}))
366		iunrab 3980	. . . . . . . . 9 ⊢ ∪ 𝑢 ∈ (1...(⌊‘(𝑀 / 2))){𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} = {𝑧 ∈ 𝑆 ∣ ∃𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(2 · 𝑢) = (1st ‘𝑧)}
367		2cn 9122	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℂ
368		zcn 9392	. . . . . . . . . . . . . . 15 ⊢ (𝑢 ∈ ℤ → 𝑢 ∈ ℂ)
369	368	adantl 277	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ ℤ) → 𝑢 ∈ ℂ)
370		mulcom 8069	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℂ ∧ 𝑢 ∈ ℂ) → (2 · 𝑢) = (𝑢 · 2))
371	367, 369, 370	sylancr 414	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ ℤ) → (2 · 𝑢) = (𝑢 · 2))
372	371	eqeq1d 2215	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ ℤ) → ((2 · 𝑢) = (1st ‘𝑧) ↔ (𝑢 · 2) = (1st ‘𝑧)))
373	372	rexbidva 2504	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (∃𝑢 ∈ ℤ (2 · 𝑢) = (1st ‘𝑧) ↔ ∃𝑢 ∈ ℤ (𝑢 · 2) = (1st ‘𝑧)))
374	152	anim1i 340	. . . . . . . . . . . . 13 ⊢ ((𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ (2 · 𝑢) = (1st ‘𝑧)) → (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧)))
375	374	reximi2 2603	. . . . . . . . . . . 12 ⊢ (∃𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(2 · 𝑢) = (1st ‘𝑧) → ∃𝑢 ∈ ℤ (2 · 𝑢) = (1st ‘𝑧))
376		simprr 531	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (2 · 𝑢) = (1st ‘𝑧))
377		simpr 110	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → 𝑧 ∈ 𝑆)
378	108, 377	sselid 3195	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → 𝑧 ∈ ((1...𝑀) × (1...𝑁)))
379	378, 110	syl 14	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (1st ‘𝑧) ∈ (1...𝑀))
380	379	adantr 276	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (1st ‘𝑧) ∈ (1...𝑀))
381		elfzle2 10165	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1st ‘𝑧) ∈ (1...𝑀) → (1st ‘𝑧) ≤ 𝑀)
382	380, 381	syl 14	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (1st ‘𝑧) ≤ 𝑀)
383	376, 382	eqbrtrd 4072	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (2 · 𝑢) ≤ 𝑀)
384		zre 9391	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 ∈ ℤ → 𝑢 ∈ ℝ)
385	384	ad2antrl 490	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 𝑢 ∈ ℝ)
386	24	ad2antrr 488	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 𝑀 ∈ ℝ)
387	159	a1i 9	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 2 ∈ ℝ)
388	161	a1i 9	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 0 < 2)
389	385, 386, 387, 388, 163	syl112anc 1254	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → ((2 · 𝑢) ≤ 𝑀 ↔ 𝑢 ≤ (𝑀 / 2)))
390	383, 389	mpbid 147	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 𝑢 ≤ (𝑀 / 2))
391	12	ad2antrr 488	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (𝑀 / 2) ∈ ℚ)
392		simprl 529	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 𝑢 ∈ ℤ)
393	391, 392, 153	syl2anc 411	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (𝑢 ≤ (𝑀 / 2) ↔ 𝑢 ≤ (⌊‘(𝑀 / 2))))
394	390, 393	mpbid 147	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 𝑢 ≤ (⌊‘(𝑀 / 2)))
395		2t0e0 9211	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (2 · 0) = 0
396		elfznn 10191	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((1st ‘𝑧) ∈ (1...𝑀) → (1st ‘𝑧) ∈ ℕ)
397	380, 396	syl 14	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (1st ‘𝑧) ∈ ℕ)
398	376, 397	eqeltrd 2283	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (2 · 𝑢) ∈ ℕ)
399	398	nngt0d 9095	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 0 < (2 · 𝑢))
400	395, 399	eqbrtrid 4085	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (2 · 0) < (2 · 𝑢))
401		0red 8088	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 0 ∈ ℝ)
402		ltmul2 8944	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((0 ∈ ℝ ∧ 𝑢 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (0 < 𝑢 ↔ (2 · 0) < (2 · 𝑢)))
403	401, 385, 387, 388, 402	syl112anc 1254	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (0 < 𝑢 ↔ (2 · 0) < (2 · 𝑢)))
404	400, 403	mpbird 167	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 0 < 𝑢)
405		elnnz 9397	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 ∈ ℕ ↔ (𝑢 ∈ ℤ ∧ 0 < 𝑢))
406	392, 404, 405	sylanbrc 417	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 𝑢 ∈ ℕ)
407	406, 295	eleqtrdi 2299	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 𝑢 ∈ (ℤ≥‘1))
408	13	ad2antrr 488	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (⌊‘(𝑀 / 2)) ∈ ℤ)
409		elfz5 10154	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ (ℤ≥‘1) ∧ (⌊‘(𝑀 / 2)) ∈ ℤ) → (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ↔ 𝑢 ≤ (⌊‘(𝑀 / 2))))
410	407, 408, 409	syl2anc 411	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ↔ 𝑢 ≤ (⌊‘(𝑀 / 2))))
411	394, 410	mpbird 167	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → 𝑢 ∈ (1...(⌊‘(𝑀 / 2))))
412	411, 376	jca 306	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧))) → (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ (2 · 𝑢) = (1st ‘𝑧)))
413	412	ex 115	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → ((𝑢 ∈ ℤ ∧ (2 · 𝑢) = (1st ‘𝑧)) → (𝑢 ∈ (1...(⌊‘(𝑀 / 2))) ∧ (2 · 𝑢) = (1st ‘𝑧))))
414	413	reximdv2 2606	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (∃𝑢 ∈ ℤ (2 · 𝑢) = (1st ‘𝑧) → ∃𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(2 · 𝑢) = (1st ‘𝑧)))
415	375, 414	impbid2 143	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (∃𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(2 · 𝑢) = (1st ‘𝑧) ↔ ∃𝑢 ∈ ℤ (2 · 𝑢) = (1st ‘𝑧)))
416		2z 9415	. . . . . . . . . . . 12 ⊢ 2 ∈ ℤ
417	379	elfzelzd 10163	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (1st ‘𝑧) ∈ ℤ)
418		divides 12170	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℤ ∧ (1st ‘𝑧) ∈ ℤ) → (2 ∥ (1st ‘𝑧) ↔ ∃𝑢 ∈ ℤ (𝑢 · 2) = (1st ‘𝑧)))
419	416, 417, 418	sylancr 414	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (2 ∥ (1st ‘𝑧) ↔ ∃𝑢 ∈ ℤ (𝑢 · 2) = (1st ‘𝑧)))
420	373, 415, 419	3bitr4d 220	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (∃𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(2 · 𝑢) = (1st ‘𝑧) ↔ 2 ∥ (1st ‘𝑧)))
421	420	rabbidva 2761	. . . . . . . . 9 ⊢ (𝜑 → {𝑧 ∈ 𝑆 ∣ ∃𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(2 · 𝑢) = (1st ‘𝑧)} = {𝑧 ∈ 𝑆 ∣ 2 ∥ (1st ‘𝑧)})
422	366, 421	eqtrid 2251	. . . . . . . 8 ⊢ (𝜑 → ∪ 𝑢 ∈ (1...(⌊‘(𝑀 / 2))){𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)} = {𝑧 ∈ 𝑆 ∣ 2 ∥ (1st ‘𝑧)})
423	422	fveq2d 5592	. . . . . . 7 ⊢ (𝜑 → (♯‘∪ 𝑢 ∈ (1...(⌊‘(𝑀 / 2))){𝑧 ∈ 𝑆 ∣ (2 · 𝑢) = (1st ‘𝑧)}) = (♯‘{𝑧 ∈ 𝑆 ∣ 2 ∥ (1st ‘𝑧)}))
424	342, 365, 423	3eqtr2d 2245	. . . . . 6 ⊢ (𝜑 → Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) = (♯‘{𝑧 ∈ 𝑆 ∣ 2 ∥ (1st ‘𝑧)}))
425	424	oveq2d 5972	. . . . 5 ⊢ (𝜑 → (-1↑Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (-1↑(♯‘{𝑧 ∈ 𝑆 ∣ 2 ∥ (1st ‘𝑧)})))
426	1, 2, 3, 5, 101, 102	lgsquadlem1 15624	. . . . 5 ⊢ (𝜑 → (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st ‘𝑧)})))
427	425, 426	oveq12d 5974	. . . 4 ⊢ (𝜑 → ((-1↑Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) · (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = ((-1↑(♯‘{𝑧 ∈ 𝑆 ∣ 2 ∥ (1st ‘𝑧)})) · (-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st ‘𝑧)}))))
428	120, 427	eqtr4d 2242	. . 3 ⊢ (𝜑 → (-1↑((♯‘{𝑧 ∈ 𝑆 ∣ 2 ∥ (1st ‘𝑧)}) + (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st ‘𝑧)}))) = ((-1↑Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) · (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
429		inrab 3449	. . . . . . 7 ⊢ ({𝑧 ∈ 𝑆 ∣ 2 ∥ (1st ‘𝑧)} ∩ {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st ‘𝑧)}) = {𝑧 ∈ 𝑆 ∣ (2 ∥ (1st ‘𝑧) ∧ ¬ 2 ∥ (1st ‘𝑧))}
430		pm3.24 695	. . . . . . . . . 10 ⊢ ¬ (2 ∥ (1st ‘𝑧) ∧ ¬ 2 ∥ (1st ‘𝑧))
431	430	a1i 9	. . . . . . . . 9 ⊢ (𝜑 → ¬ (2 ∥ (1st ‘𝑧) ∧ ¬ 2 ∥ (1st ‘𝑧)))
432	431	ralrimivw 2581	. . . . . . . 8 ⊢ (𝜑 → ∀𝑧 ∈ 𝑆 ¬ (2 ∥ (1st ‘𝑧) ∧ ¬ 2 ∥ (1st ‘𝑧)))
433		rabeq0 3494	. . . . . . . 8 ⊢ ({𝑧 ∈ 𝑆 ∣ (2 ∥ (1st ‘𝑧) ∧ ¬ 2 ∥ (1st ‘𝑧))} = ∅ ↔ ∀𝑧 ∈ 𝑆 ¬ (2 ∥ (1st ‘𝑧) ∧ ¬ 2 ∥ (1st ‘𝑧)))
434	432, 433	sylibr 134	. . . . . . 7 ⊢ (𝜑 → {𝑧 ∈ 𝑆 ∣ (2 ∥ (1st ‘𝑧) ∧ ¬ 2 ∥ (1st ‘𝑧))} = ∅)
435	429, 434	eqtrid 2251	. . . . . 6 ⊢ (𝜑 → ({𝑧 ∈ 𝑆 ∣ 2 ∥ (1st ‘𝑧)} ∩ {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st ‘𝑧)}) = ∅)
436		hashun 10967	. . . . . 6 ⊢ (({𝑧 ∈ 𝑆 ∣ 2 ∥ (1st ‘𝑧)} ∈ Fin ∧ {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st ‘𝑧)} ∈ Fin ∧ ({𝑧 ∈ 𝑆 ∣ 2 ∥ (1st ‘𝑧)} ∩ {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st ‘𝑧)}) = ∅) → (♯‘({𝑧 ∈ 𝑆 ∣ 2 ∥ (1st ‘𝑧)} ∪ {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st ‘𝑧)})) = ((♯‘{𝑧 ∈ 𝑆 ∣ 2 ∥ (1st ‘𝑧)}) + (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st ‘𝑧)})))
437	117, 103, 435, 436	syl3anc 1250	. . . . 5 ⊢ (𝜑 → (♯‘({𝑧 ∈ 𝑆 ∣ 2 ∥ (1st ‘𝑧)} ∪ {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st ‘𝑧)})) = ((♯‘{𝑧 ∈ 𝑆 ∣ 2 ∥ (1st ‘𝑧)}) + (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st ‘𝑧)})))
438		unrab 3448	. . . . . . 7 ⊢ ({𝑧 ∈ 𝑆 ∣ 2 ∥ (1st ‘𝑧)} ∪ {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st ‘𝑧)}) = {𝑧 ∈ 𝑆 ∣ (2 ∥ (1st ‘𝑧) ∨ ¬ 2 ∥ (1st ‘𝑧))}
439		rabid2 2684	. . . . . . . 8 ⊢ (𝑆 = {𝑧 ∈ 𝑆 ∣ (2 ∥ (1st ‘𝑧) ∨ ¬ 2 ∥ (1st ‘𝑧))} ↔ ∀𝑧 ∈ 𝑆 (2 ∥ (1st ‘𝑧) ∨ ¬ 2 ∥ (1st ‘𝑧)))
440	10, 112, 114	sylancr 414	. . . . . . . . 9 ⊢ (𝑧 ∈ 𝑆 → DECID 2 ∥ (1st ‘𝑧))
441		exmiddc 838	. . . . . . . . 9 ⊢ (DECID 2 ∥ (1st ‘𝑧) → (2 ∥ (1st ‘𝑧) ∨ ¬ 2 ∥ (1st ‘𝑧)))
442	440, 441	syl 14	. . . . . . . 8 ⊢ (𝑧 ∈ 𝑆 → (2 ∥ (1st ‘𝑧) ∨ ¬ 2 ∥ (1st ‘𝑧)))
443	439, 442	mprgbir 2565	. . . . . . 7 ⊢ 𝑆 = {𝑧 ∈ 𝑆 ∣ (2 ∥ (1st ‘𝑧) ∨ ¬ 2 ∥ (1st ‘𝑧))}
444	438, 443	eqtr4i 2230	. . . . . 6 ⊢ ({𝑧 ∈ 𝑆 ∣ 2 ∥ (1st ‘𝑧)} ∪ {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st ‘𝑧)}) = 𝑆
445	444	fveq2i 5591	. . . . 5 ⊢ (♯‘({𝑧 ∈ 𝑆 ∣ 2 ∥ (1st ‘𝑧)} ∪ {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st ‘𝑧)})) = (♯‘𝑆)
446	437, 445	eqtr3di 2254	. . . 4 ⊢ (𝜑 → ((♯‘{𝑧 ∈ 𝑆 ∣ 2 ∥ (1st ‘𝑧)}) + (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st ‘𝑧)})) = (♯‘𝑆))
447	446	oveq2d 5972	. . 3 ⊢ (𝜑 → (-1↑((♯‘{𝑧 ∈ 𝑆 ∣ 2 ∥ (1st ‘𝑧)}) + (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st ‘𝑧)}))) = (-1↑(♯‘𝑆)))
448	100, 428, 447	3eqtr2d 2245	. 2 ⊢ (𝜑 → (-1↑(Σ𝑢 ∈ (1...(⌊‘(𝑀 / 2)))(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = (-1↑(♯‘𝑆)))
449	4, 84, 448	3eqtrd 2243	1 ⊢ (𝜑 → (𝑄 /L 𝑃) = (-1↑(♯‘𝑆)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ↔ wb 105   ∨ wo 710  DECID wdc 836   ∧ w3a 981   = wceq 1373   ∈ wcel 2177   ≠ wne 2377  ∀wral 2485  ∃wrex 2486  {crab 2489   ∖ cdif 3167   ∪ cun 3168   ∩ cin 3169   ⊆ wss 3170  ∅c0 3464  {csn 3637  ⟨cop 3640  ∪ ciun 3932  Disj wdisj 4026   class class class wbr 4050  {copab 4111   × cxp 4680  Rel wrel 4687  ‘cfv 5279  (class class class)co 5956  1^st c1st 6236   ≈ cen 6837  Fincfn 6839  ℂcc 7938  ℝcr 7939  0cc0 7940  1c1 7941   + caddc 7943   · cmul 7945   < clt 8122   ≤ cle 8123   − cmin 8258  -cneg 8259   # cap 8669   / cdiv 8760  ℕcn 9051  2c2 9102  ℕ₀cn0 9310  ℤcz 9387  ℤ_≥cuz 9663  ℚcq 9755  ℝ⁺crp 9790  ...cfz 10145  ⌊cfl 10428  ↑cexp 10700  ♯chash 10937  Σcsu 11734   ∥ cdvds 12168   gcd cgcd 12344  ℙcprime 12499   /_L clgs 15544

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-13 2179  ax-14 2180  ax-ext 2188  ax-coll 4166  ax-sep 4169  ax-nul 4177  ax-pow 4225  ax-pr 4260  ax-un 4487  ax-setind 4592  ax-iinf 4643  ax-cnex 8031  ax-resscn 8032  ax-1cn 8033  ax-1re 8034  ax-icn 8035  ax-addcl 8036  ax-addrcl 8037  ax-mulcl 8038  ax-mulrcl 8039  ax-addcom 8040  ax-mulcom 8041  ax-addass 8042  ax-mulass 8043  ax-distr 8044  ax-i2m1 8045  ax-0lt1 8046  ax-1rid 8047  ax-0id 8048  ax-rnegex 8049  ax-precex 8050  ax-cnre 8051  ax-pre-ltirr 8052  ax-pre-ltwlin 8053  ax-pre-lttrn 8054  ax-pre-apti 8055  ax-pre-ltadd 8056  ax-pre-mulgt0 8057  ax-pre-mulext 8058  ax-arch 8059  ax-caucvg 8060  ax-addf 8062  ax-mulf 8063

This theorem depends on definitions:  df-bi 117  df-stab 833  df-dc 837  df-3or 982  df-3an 983  df-tru 1376  df-fal 1379  df-xor 1396  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ne 2378  df-nel 2473  df-ral 2490  df-rex 2491  df-reu 2492  df-rmo 2493  df-rab 2494  df-v 2775  df-sbc 3003  df-csb 3098  df-dif 3172  df-un 3174  df-in 3176  df-ss 3183  df-nul 3465  df-if 3576  df-pw 3622  df-sn 3643  df-pr 3644  df-tp 3645  df-op 3646  df-uni 3856  df-int 3891  df-iun 3934  df-disj 4027  df-br 4051  df-opab 4113  df-mpt 4114  df-tr 4150  df-id 4347  df-po 4350  df-iso 4351  df-iord 4420  df-on 4422  df-ilim 4423  df-suc 4425  df-iom 4646  df-xp 4688  df-rel 4689  df-cnv 4690  df-co 4691  df-dm 4692  df-rn 4693  df-res 4694  df-ima 4695  df-iota 5240  df-fun 5281  df-fn 5282  df-f 5283  df-f1 5284  df-fo 5285  df-f1o 5286  df-fv 5287  df-isom 5288  df-riota 5911  df-ov 5959  df-oprab 5960  df-mpo 5961  df-of 6170  df-1st 6238  df-2nd 6239  df-tpos 6343  df-recs 6403  df-irdg 6468  df-frec 6489  df-1o 6514  df-2o 6515  df-oadd 6518  df-er 6632  df-ec 6634  df-qs 6638  df-map 6749  df-en 6840  df-dom 6841  df-fin 6842  df-sup 7100  df-inf 7101  df-pnf 8124  df-mnf 8125  df-xr 8126  df-ltxr 8127  df-le 8128  df-sub 8260  df-neg 8261  df-reap 8663  df-ap 8670  df-div 8761  df-inn 9052  df-2 9110  df-3 9111  df-4 9112  df-5 9113  df-6 9114  df-7 9115  df-8 9116  df-9 9117  df-n0 9311  df-z 9388  df-dec 9520  df-uz 9664  df-q 9756  df-rp 9791  df-fz 10146  df-fzo 10280  df-fl 10430  df-mod 10485  df-seqfrec 10610  df-exp 10701  df-ihash 10938  df-cj 11223  df-re 11224  df-im 11225  df-rsqrt 11379  df-abs 11380  df-clim 11660  df-sumdc 11735  df-proddc 11932  df-dvds 12169  df-gcd 12345  df-prm 12500  df-phi 12603  df-pc 12678  df-struct 12904  df-ndx 12905  df-slot 12906  df-base 12908  df-sets 12909  df-iress 12910  df-plusg 12992  df-mulr 12993  df-starv 12994  df-sca 12995  df-vsca 12996  df-ip 12997  df-tset 12998  df-ple 12999  df-ds 13001  df-unif 13002  df-0g 13160  df-igsum 13161  df-topgen 13162  df-iimas 13204  df-qus 13205  df-mgm 13258  df-sgrp 13304  df-mnd 13319  df-mhm 13361  df-submnd 13362  df-grp 13405  df-minusg 13406  df-sbg 13407  df-mulg 13526  df-subg 13576  df-nsg 13577  df-eqg 13578  df-ghm 13647  df-cmn 13692  df-abl 13693  df-mgp 13753  df-rng 13765  df-ur 13792  df-srg 13796  df-ring 13830  df-cring 13831  df-oppr 13900  df-dvdsr 13921  df-unit 13922  df-invr 13953  df-dvr 13964  df-rhm 13984  df-nzr 14012  df-subrg 14051  df-domn 14091  df-idom 14092  df-lmod 14121  df-lssm 14185  df-lsp 14219  df-sra 14267  df-rgmod 14268  df-lidl 14301  df-rsp 14302  df-2idl 14332  df-bl 14378  df-mopn 14379  df-fg 14381  df-metu 14382  df-cnfld 14389  df-zring 14423  df-zrh 14446  df-zn 14448  df-lgs 15545

This theorem is referenced by:  lgsquadlem3  15626