lgsquadlem1 - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > lgsquadlem1		GIF version

Theorem lgsquadlem1 15234

Description: Lemma for lgsquad 15237. Count the members of 𝑆 with odd coordinates. (Contributed by Mario Carneiro, 19-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
lgsquadlem1	⊢ (𝜑 → (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)})))

Distinct variable groups: 𝑥,𝑢,𝑦,𝑧,𝑃 𝜑,𝑢,𝑥,𝑦,𝑧 𝑢,𝑀,𝑦,𝑧 𝑢,𝑁,𝑥,𝑦,𝑧 𝑢,𝑄,𝑥,𝑦,𝑧 𝑢,𝑆,𝑥,𝑧 𝑥,𝑀 𝑦,𝑆

Proof of Theorem lgsquadlem1 Dummy variables 𝑛 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		neg1cn 9089	. . . 4 ⊢ -1 ∈ ℂ
2	1	a1i 9	. . 3 ⊢ (𝜑 → -1 ∈ ℂ)
3		neg1ap0 9093	. . . 4 ⊢ -1 # 0
4	3	a1i 9	. . 3 ⊢ (𝜑 → -1 # 0)
5		lgseisen.1	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))
6		lgsquad.4	. . . . . . . . . 10 ⊢ 𝑀 = ((𝑃 − 1) / 2)
7	5, 6	gausslemma2dlem0b 15207	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ ℕ)
8	7	nnzd 9441	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℤ)
9		2nn 9146	. . . . . . . 8 ⊢ 2 ∈ ℕ
10		znq 9692	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ 2 ∈ ℕ) → (𝑀 / 2) ∈ ℚ)
11	8, 9, 10	sylancl 413	. . . . . . 7 ⊢ (𝜑 → (𝑀 / 2) ∈ ℚ)
12	11	flqcld 10349	. . . . . 6 ⊢ (𝜑 → (⌊‘(𝑀 / 2)) ∈ ℤ)
13	12	peano2zd 9445	. . . . 5 ⊢ (𝜑 → ((⌊‘(𝑀 / 2)) + 1) ∈ ℤ)
14	13, 8	fzfigd 10505	. . . 4 ⊢ (𝜑 → (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∈ Fin)
15		lgseisen.2	. . . . . . . . 9 ⊢ (𝜑 → 𝑄 ∈ (ℙ ∖ {2}))
16	15	gausslemma2dlem0a 15206	. . . . . . . 8 ⊢ (𝜑 → 𝑄 ∈ ℕ)
17	16	nnzd 9441	. . . . . . 7 ⊢ (𝜑 → 𝑄 ∈ ℤ)
18	5	gausslemma2dlem0a 15206	. . . . . . . 8 ⊢ (𝜑 → 𝑃 ∈ ℕ)
19	18	adantr 276	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℕ)
20		znq 9692	. . . . . . 7 ⊢ ((𝑄 ∈ ℤ ∧ 𝑃 ∈ ℕ) → (𝑄 / 𝑃) ∈ ℚ)
21	17, 19, 20	syl2an2r 595	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 / 𝑃) ∈ ℚ)
22		2z 9348	. . . . . . . 8 ⊢ 2 ∈ ℤ
23		elfzelz 10094	. . . . . . . . 9 ⊢ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) → 𝑢 ∈ ℤ)
24	23	adantl 277	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ∈ ℤ)
25		zmulcl 9373	. . . . . . . 8 ⊢ ((2 ∈ ℤ ∧ 𝑢 ∈ ℤ) → (2 · 𝑢) ∈ ℤ)
26	22, 24, 25	sylancr 414	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ∈ ℤ)
27		zq 9694	. . . . . . 7 ⊢ ((2 · 𝑢) ∈ ℤ → (2 · 𝑢) ∈ ℚ)
28	26, 27	syl 14	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ∈ ℚ)
29		qmulcl 9705	. . . . . 6 ⊢ (((𝑄 / 𝑃) ∈ ℚ ∧ (2 · 𝑢) ∈ ℚ) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℚ)
30	21, 28, 29	syl2anc 411	. . . . 5 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℚ)
31	30	flqcld 10349	. . . 4 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ)
32	14, 31	fsumzcl 11548	. . 3 ⊢ (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ)
33	2, 4, 32	expclzapd 10752	. 2 ⊢ (𝜑 → (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℂ)
34		lgseisen.3	. . . . 5 ⊢ (𝜑 → 𝑃 ≠ 𝑄)
35		lgsquad.5	. . . . 5 ⊢ 𝑁 = ((𝑄 − 1) / 2)
36		lgsquad.6	. . . . 5 ⊢ 𝑆 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))}
37	5, 15, 34, 6, 35, 36	lgsquadlemofi 15233	. . . 4 ⊢ (𝜑 → {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)} ∈ Fin)
38		hashcl 10855	. . . 4 ⊢ ({𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)} ∈ Fin → (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)}) ∈ ℕ₀)
39	37, 38	syl 14	. . 3 ⊢ (𝜑 → (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)}) ∈ ℕ₀)
40		expcl 10631	. . 3 ⊢ ((-1 ∈ ℂ ∧ (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)}) ∈ ℕ₀) → (-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)})) ∈ ℂ)
41	1, 39, 40	sylancr 414	. 2 ⊢ (𝜑 → (-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)})) ∈ ℂ)
42	39	nn0zd 9440	. . 3 ⊢ (𝜑 → (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)}) ∈ ℤ)
43	2, 4, 42	expap0d 10753	. 2 ⊢ (𝜑 → (-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)})) # 0)
44	41, 43	recidapd 8804	. . . 4 ⊢ (𝜑 → ((-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)})) · (1 / (-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)})))) = 1)
45		1div1e1 8725	. . . . . . . . 9 ⊢ (1 / 1) = 1
46	45	negeqi 8215	. . . . . . . 8 ⊢ -(1 / 1) = -1
47		ax-1cn 7967	. . . . . . . . 9 ⊢ 1 ∈ ℂ
48		1ap0 8611	. . . . . . . . 9 ⊢ 1 # 0
49		divneg2ap 8757	. . . . . . . . 9 ⊢ ((1 ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 # 0) → -(1 / 1) = (1 / -1))
50	47, 47, 48, 49	mp3an 1348	. . . . . . . 8 ⊢ -(1 / 1) = (1 / -1)
51	46, 50	eqtr3i 2216	. . . . . . 7 ⊢ -1 = (1 / -1)
52	51	oveq1i 5929	. . . . . 6 ⊢ (-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)})) = ((1 / -1)↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)}))
53	2, 4, 42	exprecapd 10755	. . . . . 6 ⊢ (𝜑 → ((1 / -1)↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)})) = (1 / (-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)}))))
54	52, 53	eqtrid 2238	. . . . 5 ⊢ (𝜑 → (-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)})) = (1 / (-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)}))))
55	54	oveq2d 5935	. . . 4 ⊢ (𝜑 → ((-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)})) · (-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)}))) = ((-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)})) · (1 / (-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)})))))
56	5, 15, 34, 6, 35, 36	lgsquadlemsfi 15232	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑆 ∈ Fin)
57	56	adantr 276	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑆 ∈ Fin)
58		opabssxp 4734	. . . . . . . . . . . . . . . . . 18 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} ⊆ ((1...𝑀) × (1...𝑁))
59	36, 58	eqsstri 3212	. . . . . . . . . . . . . . . . 17 ⊢ 𝑆 ⊆ ((1...𝑀) × (1...𝑁))
60	59	sseli 3176	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ 𝑆 → 𝑧 ∈ ((1...𝑀) × (1...𝑁)))
61		xp1st 6220	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ ((1...𝑀) × (1...𝑁)) → (1^st ‘𝑧) ∈ (1...𝑀))
62	60, 61	syl 14	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ 𝑆 → (1^st ‘𝑧) ∈ (1...𝑀))
63	62	elfzelzd 10095	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ 𝑆 → (1^st ‘𝑧) ∈ ℤ)
64	19	nnzd 9441	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℤ)
65	64, 26	zsubcld 9447	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − (2 · 𝑢)) ∈ ℤ)
66		zdceq 9395	. . . . . . . . . . . . . 14 ⊢ (((1^st ‘𝑧) ∈ ℤ ∧ (𝑃 − (2 · 𝑢)) ∈ ℤ) → DECID (1^st ‘𝑧) = (𝑃 − (2 · 𝑢)))
67	63, 65, 66	syl2anr 290	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑧 ∈ 𝑆) → DECID (1^st ‘𝑧) = (𝑃 − (2 · 𝑢)))
68	67	ralrimiva 2567	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ∀𝑧 ∈ 𝑆 DECID (1^st ‘𝑧) = (𝑃 − (2 · 𝑢)))
69	57, 68	ssfirab 6992	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → {𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))} ∈ Fin)
70		fveqeq2 5564	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = 𝑣 → ((1^st ‘𝑧) = (𝑃 − (2 · 𝑢)) ↔ (1^st ‘𝑣) = (𝑃 − (2 · 𝑢))))
71	70	elrab 2917	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))} ↔ (𝑣 ∈ 𝑆 ∧ (1^st ‘𝑣) = (𝑃 − (2 · 𝑢))))
72	71	simprbi 275	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))} → (1^st ‘𝑣) = (𝑃 − (2 · 𝑢)))
73	72	ad2antll 491	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → (1^st ‘𝑣) = (𝑃 − (2 · 𝑢)))
74	73	oveq2d 5935	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → (𝑃 − (1^st ‘𝑣)) = (𝑃 − (𝑃 − (2 · 𝑢))))
75	19	nncnd 8998	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℂ)
76	75	adantrr 479	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → 𝑃 ∈ ℂ)
77	26	zcnd 9443	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ∈ ℂ)
78	77	adantrr 479	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → (2 · 𝑢) ∈ ℂ)
79	76, 78	nncand 8337	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → (𝑃 − (𝑃 − (2 · 𝑢))) = (2 · 𝑢))
80	74, 79	eqtrd 2226	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → (𝑃 − (1^st ‘𝑣)) = (2 · 𝑢))
81	80	oveq1d 5934	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → ((𝑃 − (1^st ‘𝑣)) / 2) = ((2 · 𝑢) / 2))
82	24	zcnd 9443	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ∈ ℂ)
83	82	adantrr 479	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → 𝑢 ∈ ℂ)
84		2cnd 9057	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → 2 ∈ ℂ)
85		2ap0 9077	. . . . . . . . . . . . . . . 16 ⊢ 2 # 0
86	85	a1i 9	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → 2 # 0)
87	83, 84, 86	divcanap3d 8816	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → ((2 · 𝑢) / 2) = 𝑢)
88	81, 87	eqtrd 2226	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → ((𝑃 − (1^st ‘𝑣)) / 2) = 𝑢)
89	88	ralrimivva 2576	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)∀𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))} ((𝑃 − (1^st ‘𝑣)) / 2) = 𝑢)
90		invdisj 4024	. . . . . . . . . . . 12 ⊢ (∀𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)∀𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))} ((𝑃 − (1^st ‘𝑣)) / 2) = 𝑢 → Disj 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))})
91	89, 90	syl 14	. . . . . . . . . . 11 ⊢ (𝜑 → Disj 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))})
92	14, 69, 91	hashiun 11624	. . . . . . . . . 10 ⊢ (𝜑 → (♯‘∪ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))}) = Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(♯‘{𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))}))
93		iunrab 3961	. . . . . . . . . . . 12 ⊢ ∪ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))} = {𝑧 ∈ 𝑆 ∣ ∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1^st ‘𝑧) = (𝑃 − (2 · 𝑢))}
94		eldifsni 3748	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ≠ 2)
95	5, 94	syl 14	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑃 ≠ 2)
96	95	necomd 2450	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 2 ≠ 𝑃)
97	96	neneqd 2385	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ¬ 2 = 𝑃)
98	97	ad2antrr 488	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ¬ 2 = 𝑃)
99		uzid 9609	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (2 ∈ ℤ → 2 ∈ (ℤ_≥‘2))
100	22, 99	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 ∈ (ℤ_≥‘2)
101	5	eldifad 3165	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑃 ∈ ℙ)
102	101	ad2antrr 488	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℙ)
103		dvdsprm 12278	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2 ∈ (ℤ_≥‘2) ∧ 𝑃 ∈ ℙ) → (2 ∥ 𝑃 ↔ 2 = 𝑃))
104	100, 102, 103	sylancr 414	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 ∥ 𝑃 ↔ 2 = 𝑃))
105	98, 104	mtbird 674	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ¬ 2 ∥ 𝑃)
106	18	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℕ)
107	106	nncnd 8998	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℂ)
108	26	adantlr 477	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ∈ ℤ)
109	108	zcnd 9443	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ∈ ℂ)
110	107, 109	npcand 8336	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) + (2 · 𝑢)) = 𝑃)
111	110	breq2d 4042	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 ∥ ((𝑃 − (2 · 𝑢)) + (2 · 𝑢)) ↔ 2 ∥ 𝑃))
112	105, 111	mtbird 674	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ¬ 2 ∥ ((𝑃 − (2 · 𝑢)) + (2 · 𝑢)))
113	23	adantl 277	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ∈ ℤ)
114		dvdsmul1 11959	. . . . . . . . . . . . . . . . . . 19 ⊢ ((2 ∈ ℤ ∧ 𝑢 ∈ ℤ) → 2 ∥ (2 · 𝑢))
115	22, 113, 114	sylancr 414	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 2 ∥ (2 · 𝑢))
116	22	a1i 9	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 2 ∈ ℤ)
117	106	nnzd 9441	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℤ)
118	117, 108	zsubcld 9447	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − (2 · 𝑢)) ∈ ℤ)
119		dvds2add 11971	. . . . . . . . . . . . . . . . . . 19 ⊢ ((2 ∈ ℤ ∧ (𝑃 − (2 · 𝑢)) ∈ ℤ ∧ (2 · 𝑢) ∈ ℤ) → ((2 ∥ (𝑃 − (2 · 𝑢)) ∧ 2 ∥ (2 · 𝑢)) → 2 ∥ ((𝑃 − (2 · 𝑢)) + (2 · 𝑢))))
120	116, 118, 108, 119	syl3anc 1249	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 ∥ (𝑃 − (2 · 𝑢)) ∧ 2 ∥ (2 · 𝑢)) → 2 ∥ ((𝑃 − (2 · 𝑢)) + (2 · 𝑢))))
121	115, 120	mpan2d 428	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 ∥ (𝑃 − (2 · 𝑢)) → 2 ∥ ((𝑃 − (2 · 𝑢)) + (2 · 𝑢))))
122	112, 121	mtod 664	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ¬ 2 ∥ (𝑃 − (2 · 𝑢)))
123		breq2 4034	. . . . . . . . . . . . . . . . 17 ⊢ ((1^st ‘𝑧) = (𝑃 − (2 · 𝑢)) → (2 ∥ (1^st ‘𝑧) ↔ 2 ∥ (𝑃 − (2 · 𝑢))))
124	123	notbid 668	. . . . . . . . . . . . . . . 16 ⊢ ((1^st ‘𝑧) = (𝑃 − (2 · 𝑢)) → (¬ 2 ∥ (1^st ‘𝑧) ↔ ¬ 2 ∥ (𝑃 − (2 · 𝑢))))
125	122, 124	syl5ibrcom 157	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((1^st ‘𝑧) = (𝑃 − (2 · 𝑢)) → ¬ 2 ∥ (1^st ‘𝑧)))
126	125	rexlimdva 2611	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1^st ‘𝑧) = (𝑃 − (2 · 𝑢)) → ¬ 2 ∥ (1^st ‘𝑧)))
127		simpr 110	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → 𝑧 ∈ 𝑆)
128	59, 127	sselid 3178	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → 𝑧 ∈ ((1...𝑀) × (1...𝑁)))
129	128, 61	syl 14	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (1^st ‘𝑧) ∈ (1...𝑀))
130		elfzelz 10094	. . . . . . . . . . . . . . . 16 ⊢ ((1^st ‘𝑧) ∈ (1...𝑀) → (1^st ‘𝑧) ∈ ℤ)
131		odd2np1 12017	. . . . . . . . . . . . . . . 16 ⊢ ((1^st ‘𝑧) ∈ ℤ → (¬ 2 ∥ (1^st ‘𝑧) ↔ ∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = (1^st ‘𝑧)))
132	129, 130, 131	3syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (¬ 2 ∥ (1^st ‘𝑧) ↔ ∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = (1^st ‘𝑧)))
133	11	ad2antrr 488	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (𝑀 / 2) ∈ ℚ)
134	133	flqcld 10349	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (⌊‘(𝑀 / 2)) ∈ ℤ)
135	134	peano2zd 9445	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → ((⌊‘(𝑀 / 2)) + 1) ∈ ℤ)
136	7	ad2antrr 488	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → 𝑀 ∈ ℕ)
137	136	nnzd 9441	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → 𝑀 ∈ ℤ)
138		simprl 529	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → 𝑛 ∈ ℤ)
139	137, 138	zsubcld 9447	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (𝑀 − 𝑛) ∈ ℤ)
140	134	zred 9442	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (⌊‘(𝑀 / 2)) ∈ ℝ)
141	7	nnred 8997	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑀 ∈ ℝ)
142	141	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → 𝑀 ∈ ℝ)
143	142	rehalfcld 9232	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (𝑀 / 2) ∈ ℝ)
144	139	zred 9442	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (𝑀 − 𝑛) ∈ ℝ)
145		flqle 10350	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑀 / 2) ∈ ℚ → (⌊‘(𝑀 / 2)) ≤ (𝑀 / 2))
146	133, 145	syl 14	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (⌊‘(𝑀 / 2)) ≤ (𝑀 / 2))
147		zre 9324	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ ℤ → 𝑛 ∈ ℝ)
148	147	ad2antrl 490	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → 𝑛 ∈ ℝ)
149		simprr 531	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → ((2 · 𝑛) + 1) = (1^st ‘𝑧))
150	129	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (1^st ‘𝑧) ∈ (1...𝑀))
151	149, 150	eqeltrd 2270	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → ((2 · 𝑛) + 1) ∈ (1...𝑀))
152		elfzle2 10097	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((2 · 𝑛) + 1) ∈ (1...𝑀) → ((2 · 𝑛) + 1) ≤ 𝑀)
153	151, 152	syl 14	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → ((2 · 𝑛) + 1) ≤ 𝑀)
154		zmulcl 9373	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((2 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (2 · 𝑛) ∈ ℤ)
155	22, 138, 154	sylancr 414	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (2 · 𝑛) ∈ ℤ)
156		zltp1le 9374	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((2 · 𝑛) ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((2 · 𝑛) < 𝑀 ↔ ((2 · 𝑛) + 1) ≤ 𝑀))
157	155, 137, 156	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → ((2 · 𝑛) < 𝑀 ↔ ((2 · 𝑛) + 1) ≤ 𝑀))
158	153, 157	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (2 · 𝑛) < 𝑀)
159		2re 9054	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 2 ∈ ℝ
160	159	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → 2 ∈ ℝ)
161		2pos 9075	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 0 < 2
162	161	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → 0 < 2)
163		ltmuldiv2 8896	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑛 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 𝑛) < 𝑀 ↔ 𝑛 < (𝑀 / 2)))
164	148, 142, 160, 162, 163	syl112anc 1253	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → ((2 · 𝑛) < 𝑀 ↔ 𝑛 < (𝑀 / 2)))
165	158, 164	mpbid 147	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → 𝑛 < (𝑀 / 2))
166	143	recnd 8050	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (𝑀 / 2) ∈ ℂ)
167	7	nncnd 8998	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑀 ∈ ℂ)
168	167	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → 𝑀 ∈ ℂ)
169	168	2halvesd 9231	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → ((𝑀 / 2) + (𝑀 / 2)) = 𝑀)
170	166, 166, 169	mvlraddd 8385	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (𝑀 / 2) = (𝑀 − (𝑀 / 2)))
171	165, 170	breqtrd 4056	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → 𝑛 < (𝑀 − (𝑀 / 2)))
172	148, 142, 143, 171	ltsub13d 8572	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (𝑀 / 2) < (𝑀 − 𝑛))
173	140, 143, 144, 146, 172	lelttrd 8146	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (⌊‘(𝑀 / 2)) < (𝑀 − 𝑛))
174		zltp1le 9374	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((⌊‘(𝑀 / 2)) ∈ ℤ ∧ (𝑀 − 𝑛) ∈ ℤ) → ((⌊‘(𝑀 / 2)) < (𝑀 − 𝑛) ↔ ((⌊‘(𝑀 / 2)) + 1) ≤ (𝑀 − 𝑛)))
175	134, 139, 174	syl2anc 411	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → ((⌊‘(𝑀 / 2)) < (𝑀 − 𝑛) ↔ ((⌊‘(𝑀 / 2)) + 1) ≤ (𝑀 − 𝑛)))
176	173, 175	mpbid 147	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → ((⌊‘(𝑀 / 2)) + 1) ≤ (𝑀 − 𝑛))
177		2t0e0 9144	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (2 · 0) = 0
178		2cn 9055	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 2 ∈ ℂ
179		zcn 9325	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑛 ∈ ℤ → 𝑛 ∈ ℂ)
180	179	ad2antrl 490	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → 𝑛 ∈ ℂ)
181		mulcl 8001	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((2 ∈ ℂ ∧ 𝑛 ∈ ℂ) → (2 · 𝑛) ∈ ℂ)
182	178, 180, 181	sylancr 414	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (2 · 𝑛) ∈ ℂ)
183		pncan 8227	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((2 · 𝑛) ∈ ℂ ∧ 1 ∈ ℂ) → (((2 · 𝑛) + 1) − 1) = (2 · 𝑛))
184	182, 47, 183	sylancl 413	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (((2 · 𝑛) + 1) − 1) = (2 · 𝑛))
185		elfznn 10123	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((2 · 𝑛) + 1) ∈ (1...𝑀) → ((2 · 𝑛) + 1) ∈ ℕ)
186		nnm1nn0 9284	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((2 · 𝑛) + 1) ∈ ℕ → (((2 · 𝑛) + 1) − 1) ∈ ℕ₀)
187	151, 185, 186	3syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (((2 · 𝑛) + 1) − 1) ∈ ℕ₀)
188	184, 187	eqeltrrd 2271	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (2 · 𝑛) ∈ ℕ₀)
189	188	nn0ge0d 9299	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → 0 ≤ (2 · 𝑛))
190	177, 189	eqbrtrid 4065	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (2 · 0) ≤ (2 · 𝑛))
191		0red 8022	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → 0 ∈ ℝ)
192		lemul2 8878	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((0 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (0 ≤ 𝑛 ↔ (2 · 0) ≤ (2 · 𝑛)))
193	191, 148, 160, 162, 192	syl112anc 1253	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (0 ≤ 𝑛 ↔ (2 · 0) ≤ (2 · 𝑛)))
194	190, 193	mpbird 167	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → 0 ≤ 𝑛)
195	142, 148	subge02d 8558	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (0 ≤ 𝑛 ↔ (𝑀 − 𝑛) ≤ 𝑀))
196	194, 195	mpbid 147	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (𝑀 − 𝑛) ≤ 𝑀)
197	135, 137, 139, 176, 196	elfzd 10085	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (𝑀 − 𝑛) ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀))
198	101	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → 𝑃 ∈ ℙ)
199		prmnn 12251	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
200	198, 199	syl 14	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → 𝑃 ∈ ℕ)
201	200	nncnd 8998	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → 𝑃 ∈ ℂ)
202		peano2cn 8156	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2 · 𝑛) ∈ ℂ → ((2 · 𝑛) + 1) ∈ ℂ)
203	182, 202	syl 14	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → ((2 · 𝑛) + 1) ∈ ℂ)
204	201, 203	nncand 8337	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (𝑃 − (𝑃 − ((2 · 𝑛) + 1))) = ((2 · 𝑛) + 1))
205		1cnd 8037	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → 1 ∈ ℂ)
206	201, 182, 205	sub32d 8364	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → ((𝑃 − (2 · 𝑛)) − 1) = ((𝑃 − 1) − (2 · 𝑛)))
207	201, 182, 205	subsub4d 8363	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → ((𝑃 − (2 · 𝑛)) − 1) = (𝑃 − ((2 · 𝑛) + 1)))
208		2cnd 9057	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → 2 ∈ ℂ)
209	208, 168, 180	subdid 8435	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (2 · (𝑀 − 𝑛)) = ((2 · 𝑀) − (2 · 𝑛)))
210	6	oveq2i 5930	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (2 · 𝑀) = (2 · ((𝑃 − 1) / 2))
211	18	nnzd 9441	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑃 ∈ ℤ)
212	211	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → 𝑃 ∈ ℤ)
213		peano2zm 9358	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑃 ∈ ℤ → (𝑃 − 1) ∈ ℤ)
214	212, 213	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (𝑃 − 1) ∈ ℤ)
215	214	zcnd 9443	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (𝑃 − 1) ∈ ℂ)
216	160, 162	gt0ap0d 8650	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → 2 # 0)
217	215, 208, 216	divcanap2d 8813	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (2 · ((𝑃 − 1) / 2)) = (𝑃 − 1))
218	210, 217	eqtrid 2238	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (2 · 𝑀) = (𝑃 − 1))
219	218	oveq1d 5934	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → ((2 · 𝑀) − (2 · 𝑛)) = ((𝑃 − 1) − (2 · 𝑛)))
220	209, 219	eqtr2d 2227	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → ((𝑃 − 1) − (2 · 𝑛)) = (2 · (𝑀 − 𝑛)))
221	206, 207, 220	3eqtr3d 2234	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (𝑃 − ((2 · 𝑛) + 1)) = (2 · (𝑀 − 𝑛)))
222	221	oveq2d 5935	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (𝑃 − (𝑃 − ((2 · 𝑛) + 1))) = (𝑃 − (2 · (𝑀 − 𝑛))))
223	204, 222, 149	3eqtr3rd 2235	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (1^st ‘𝑧) = (𝑃 − (2 · (𝑀 − 𝑛))))
224		oveq2 5927	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 = (𝑀 − 𝑛) → (2 · 𝑢) = (2 · (𝑀 − 𝑛)))
225	224	oveq2d 5935	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 = (𝑀 − 𝑛) → (𝑃 − (2 · 𝑢)) = (𝑃 − (2 · (𝑀 − 𝑛))))
226	225	rspceeqv 2883	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 − 𝑛) ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ (1^st ‘𝑧) = (𝑃 − (2 · (𝑀 − 𝑛)))) → ∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1^st ‘𝑧) = (𝑃 − (2 · 𝑢)))
227	197, 223, 226	syl2anc 411	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → ∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1^st ‘𝑧) = (𝑃 − (2 · 𝑢)))
228	227	rexlimdvaa 2612	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = (1^st ‘𝑧) → ∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1^st ‘𝑧) = (𝑃 − (2 · 𝑢))))
229	132, 228	sylbid 150	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (¬ 2 ∥ (1^st ‘𝑧) → ∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1^st ‘𝑧) = (𝑃 − (2 · 𝑢))))
230	126, 229	impbid 129	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1^st ‘𝑧) = (𝑃 − (2 · 𝑢)) ↔ ¬ 2 ∥ (1^st ‘𝑧)))
231	230	rabbidva 2748	. . . . . . . . . . . 12 ⊢ (𝜑 → {𝑧 ∈ 𝑆 ∣ ∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1^st ‘𝑧) = (𝑃 − (2 · 𝑢))} = {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)})
232	93, 231	eqtrid 2238	. . . . . . . . . . 11 ⊢ (𝜑 → ∪ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))} = {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)})
233	232	fveq2d 5559	. . . . . . . . . 10 ⊢ (𝜑 → (♯‘∪ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))}) = (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)}))
234		ssrab2 3265	. . . . . . . . . . . . . . 15 ⊢ {𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))} ⊆ 𝑆
235	36	relopabiv 4786	. . . . . . . . . . . . . . 15 ⊢ Rel 𝑆
236		relss 4747	. . . . . . . . . . . . . . 15 ⊢ ({𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))} ⊆ 𝑆 → (Rel 𝑆 → Rel {𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))}))
237	234, 235, 236	mp2 16	. . . . . . . . . . . . . 14 ⊢ Rel {𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))}
238		relxp 4769	. . . . . . . . . . . . . 14 ⊢ Rel ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
239	36	eleq2i 2260	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑥, 𝑦⟩ ∈ 𝑆 ↔ ⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))})
240		opabidw 4288	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} ↔ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))
241	239, 240	bitri 184	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝑥, 𝑦⟩ ∈ 𝑆 ↔ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))
242		anass 401	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁) ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄)) ↔ (𝑦 ∈ ℕ ∧ (𝑦 ≤ 𝑁 ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄))))
243	31	peano2zd 9445	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ∈ ℤ)
244	243	zred 9442	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ∈ ℝ)
245	244	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ∈ ℝ)
246	16	nnred 8997	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑄 ∈ ℝ)
247	246	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈ ℝ)
248		nnre 8991	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
249	248	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ ℝ)
250		lesub 8462	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ∈ ℝ ∧ 𝑄 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ≤ (𝑄 − 𝑦) ↔ 𝑦 ≤ (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1))))
251	245, 247, 249, 250	syl3anc 1249	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ≤ (𝑄 − 𝑦) ↔ 𝑦 ≤ (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1))))
252	246	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑄 ∈ ℝ)
253	252	recnd 8050	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑄 ∈ ℂ)
254	75, 253	mulcomd 8043	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 · 𝑄) = (𝑄 · 𝑃))
255	77, 253	mulcomd 8043	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑢) · 𝑄) = (𝑄 · (2 · 𝑢)))
256	19	nnap0d 9030	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 # 0)
257	253, 75, 256	divcanap1d 8812	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 𝑃) · 𝑃) = 𝑄)
258	257	oveq1d 5934	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑄 / 𝑃) · 𝑃) · (2 · 𝑢)) = (𝑄 · (2 · 𝑢)))
259	246, 18	nndivred 9034	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → (𝑄 / 𝑃) ∈ ℝ)
260	259	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 / 𝑃) ∈ ℝ)
261	260	recnd 8050	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 / 𝑃) ∈ ℂ)
262	261, 75, 77	mul32d 8174	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑄 / 𝑃) · 𝑃) · (2 · 𝑢)) = (((𝑄 / 𝑃) · (2 · 𝑢)) · 𝑃))
263	255, 258, 262	3eqtr2d 2232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑢) · 𝑄) = (((𝑄 / 𝑃) · (2 · 𝑢)) · 𝑃))
264	254, 263	oveq12d 5937	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 · 𝑄) − ((2 · 𝑢) · 𝑄)) = ((𝑄 · 𝑃) − (((𝑄 / 𝑃) · (2 · 𝑢)) · 𝑃)))
265	75, 77, 253	subdird 8436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) · 𝑄) = ((𝑃 · 𝑄) − ((2 · 𝑢) · 𝑄)))
266	26	zred 9442	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ∈ ℝ)
267	260, 266	remulcld 8052	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ)
268	267	recnd 8050	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℂ)
269	253, 268, 75	subdird 8436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃) = ((𝑄 · 𝑃) − (((𝑄 / 𝑃) · (2 · 𝑢)) · 𝑃)))
270	264, 265, 269	3eqtr4d 2236	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) · 𝑄) = ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃))
271	270	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑃 − (2 · 𝑢)) · 𝑄) = ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃))
272	271	breq2d 4042	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄) ↔ (𝑦 · 𝑃) < ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃)))
273	267	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ)
274	247, 273	resubcld 8402	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℝ)
275	19	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℕ)
276	275	nnred 8997	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℝ)
277	275	nngt0d 9028	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 0 < 𝑃)
278		ltmul1 8613	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑦 ∈ ℝ ∧ (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℝ ∧ (𝑃 ∈ ℝ ∧ 0 < 𝑃)) → (𝑦 < (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ↔ (𝑦 · 𝑃) < ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃)))
279	249, 274, 276, 277, 278	syl112anc 1253	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑦 < (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ↔ (𝑦 · 𝑃) < ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃)))
280		ltsub13 8464	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑦 ∈ ℝ ∧ 𝑄 ∈ ℝ ∧ ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ) → (𝑦 < (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ↔ ((𝑄 / 𝑃) · (2 · 𝑢)) < (𝑄 − 𝑦)))
281	249, 247, 273, 280	syl3anc 1249	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑦 < (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ↔ ((𝑄 / 𝑃) · (2 · 𝑢)) < (𝑄 − 𝑦)))
282	272, 279, 281	3bitr2d 216	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄) ↔ ((𝑄 / 𝑃) · (2 · 𝑢)) < (𝑄 − 𝑦)))
283	16	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑄 ∈ ℕ)
284	283	nnzd 9441	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑄 ∈ ℤ)
285		nnz 9339	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℤ)
286		zsubcl 9361	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑄 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑄 − 𝑦) ∈ ℤ)
287	284, 285, 286	syl2an 289	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑄 − 𝑦) ∈ ℤ)
288		flqlt 10355	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℚ ∧ (𝑄 − 𝑦) ∈ ℤ) → (((𝑄 / 𝑃) · (2 · 𝑢)) < (𝑄 − 𝑦) ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < (𝑄 − 𝑦)))
289	30, 287, 288	syl2an2r 595	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (((𝑄 / 𝑃) · (2 · 𝑢)) < (𝑄 − 𝑦) ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < (𝑄 − 𝑦)))
290		zltp1le 9374	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ ∧ (𝑄 − 𝑦) ∈ ℤ) → ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < (𝑄 − 𝑦) ↔ ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ≤ (𝑄 − 𝑦)))
291	31, 287, 290	syl2an2r 595	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < (𝑄 − 𝑦) ↔ ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ≤ (𝑄 − 𝑦)))
292	282, 289, 291	3bitrd 214	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄) ↔ ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ≤ (𝑄 − 𝑦)))
293	35	oveq2i 5930	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (2 · 𝑁) = (2 · ((𝑄 − 1) / 2))
294		peano2rem 8288	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑄 ∈ ℝ → (𝑄 − 1) ∈ ℝ)
295	252, 294	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 − 1) ∈ ℝ)
296	295	recnd 8050	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 − 1) ∈ ℂ)
297		2cnd 9057	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 2 ∈ ℂ)
298	85	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 2 # 0)
299	296, 297, 298	divcanap2d 8813	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · ((𝑄 − 1) / 2)) = (𝑄 − 1))
300	293, 299	eqtrid 2238	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) = (𝑄 − 1))
301	300	oveq1d 5934	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = ((𝑄 − 1) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
302		1cnd 8037	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 1 ∈ ℂ)
303	31	zcnd 9443	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℂ)
304	253, 302, 303	sub32d 8364	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 − 1) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = ((𝑄 − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) − 1))
305	253, 303, 302	subsub4d 8363	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) − 1) = (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1)))
306	301, 304, 305	3eqtrd 2230	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1)))
307	306	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1)))
308	307	breq2d 4042	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ↔ 𝑦 ≤ (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1))))
309	251, 292, 308	3bitr4d 220	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄) ↔ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
310	309	anbi2d 464	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 ≤ 𝑁 ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄)) ↔ (𝑦 ≤ 𝑁 ∧ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
311	15, 35	gausslemma2dlem0b 15207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 𝑁 ∈ ℕ)
312		nnmulcl 9005	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((2 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (2 · 𝑁) ∈ ℕ)
313	9, 311, 312	sylancr 414	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (2 · 𝑁) ∈ ℕ)
314	313	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) ∈ ℕ)
315	314	nnred 8997	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) ∈ ℝ)
316	311	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ∈ ℕ)
317	316	nnred 8997	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ∈ ℝ)
318	31	zred 9442	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℝ)
319	311	nncnd 8998	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 𝑁 ∈ ℂ)
320	319	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ∈ ℂ)
321	320	2timesd 9228	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) = (𝑁 + 𝑁))
322	320, 320, 321	mvrladdd 8388	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − 𝑁) = 𝑁)
323	252	rehalfcld 9232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 / 2) ∈ ℝ)
324	252	ltm1d 8953	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 − 1) < 𝑄)
325	159	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 2 ∈ ℝ)
326	161	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 0 < 2)
327		ltdiv1 8889	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑄 − 1) ∈ ℝ ∧ 𝑄 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((𝑄 − 1) < 𝑄 ↔ ((𝑄 − 1) / 2) < (𝑄 / 2)))
328	295, 252, 325, 326, 327	syl112anc 1253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 − 1) < 𝑄 ↔ ((𝑄 − 1) / 2) < (𝑄 / 2)))
329	324, 328	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 − 1) / 2) < (𝑄 / 2))
330	35, 329	eqbrtrid 4065	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 < (𝑄 / 2))
331	317, 323, 330	ltled 8140	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ≤ (𝑄 / 2))
332	253, 297, 75, 298	div32apd 8835	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 2) · 𝑃) = (𝑄 · (𝑃 / 2)))
333	141	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑀 ∈ ℝ)
334	333	rehalfcld 9232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑀 / 2) ∈ ℝ)
335	13	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((⌊‘(𝑀 / 2)) + 1) ∈ ℤ)
336	335	zred 9442	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((⌊‘(𝑀 / 2)) + 1) ∈ ℝ)
337	24	zred 9442	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ∈ ℝ)
338	11	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑀 / 2) ∈ ℚ)
339		flqltp1 10351	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝑀 / 2) ∈ ℚ → (𝑀 / 2) < ((⌊‘(𝑀 / 2)) + 1))
340	338, 339	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑀 / 2) < ((⌊‘(𝑀 / 2)) + 1))
341		elfzle1 10096	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) → ((⌊‘(𝑀 / 2)) + 1) ≤ 𝑢)
342	341	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((⌊‘(𝑀 / 2)) + 1) ≤ 𝑢)
343	334, 336, 337, 340, 342	ltletrd 8444	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑀 / 2) < 𝑢)
344		ltdivmul 8897	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝑀 ∈ ℝ ∧ 𝑢 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((𝑀 / 2) < 𝑢 ↔ 𝑀 < (2 · 𝑢)))
345	333, 337, 325, 326, 344	syl112anc 1253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑀 / 2) < 𝑢 ↔ 𝑀 < (2 · 𝑢)))
346	343, 345	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑀 < (2 · 𝑢))
347	6, 346	eqbrtrrid 4066	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − 1) / 2) < (2 · 𝑢))
348	19	nnred 8997	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℝ)
349		peano2rem 8288	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑃 ∈ ℝ → (𝑃 − 1) ∈ ℝ)
350	348, 349	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − 1) ∈ ℝ)
351		ltdivmul 8897	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((𝑃 − 1) ∈ ℝ ∧ (2 · 𝑢) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (((𝑃 − 1) / 2) < (2 · 𝑢) ↔ (𝑃 − 1) < (2 · (2 · 𝑢))))
352	350, 266, 325, 326, 351	syl112anc 1253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑃 − 1) / 2) < (2 · 𝑢) ↔ (𝑃 − 1) < (2 · (2 · 𝑢))))
353	347, 352	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − 1) < (2 · (2 · 𝑢)))
354		zmulcl 9373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((2 ∈ ℤ ∧ (2 · 𝑢) ∈ ℤ) → (2 · (2 · 𝑢)) ∈ ℤ)
355	22, 26, 354	sylancr 414	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · (2 · 𝑢)) ∈ ℤ)
356		zlem1lt 9376	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑃 ∈ ℤ ∧ (2 · (2 · 𝑢)) ∈ ℤ) → (𝑃 ≤ (2 · (2 · 𝑢)) ↔ (𝑃 − 1) < (2 · (2 · 𝑢))))
357	211, 355, 356	syl2an2r 595	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 ≤ (2 · (2 · 𝑢)) ↔ (𝑃 − 1) < (2 · (2 · 𝑢))))
358	353, 357	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ≤ (2 · (2 · 𝑢)))
359		ledivmul 8898	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑃 ∈ ℝ ∧ (2 · 𝑢) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((𝑃 / 2) ≤ (2 · 𝑢) ↔ 𝑃 ≤ (2 · (2 · 𝑢))))
360	348, 266, 325, 326, 359	syl112anc 1253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 / 2) ≤ (2 · 𝑢) ↔ 𝑃 ≤ (2 · (2 · 𝑢))))
361	358, 360	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 / 2) ≤ (2 · 𝑢))
362	348	rehalfcld 9232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 / 2) ∈ ℝ)
363	283	nngt0d 9028	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 0 < 𝑄)
364		lemul2 8878	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝑃 / 2) ∈ ℝ ∧ (2 · 𝑢) ∈ ℝ ∧ (𝑄 ∈ ℝ ∧ 0 < 𝑄)) → ((𝑃 / 2) ≤ (2 · 𝑢) ↔ (𝑄 · (𝑃 / 2)) ≤ (𝑄 · (2 · 𝑢))))
365	362, 266, 252, 363, 364	syl112anc 1253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 / 2) ≤ (2 · 𝑢) ↔ (𝑄 · (𝑃 / 2)) ≤ (𝑄 · (2 · 𝑢))))
366	361, 365	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 · (𝑃 / 2)) ≤ (𝑄 · (2 · 𝑢)))
367	332, 366	eqbrtrd 4052	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 2) · 𝑃) ≤ (𝑄 · (2 · 𝑢)))
368	252, 266	remulcld 8052	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 · (2 · 𝑢)) ∈ ℝ)
369	19	nngt0d 9028	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 0 < 𝑃)
370		lemuldiv 8902	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑄 / 2) ∈ ℝ ∧ (𝑄 · (2 · 𝑢)) ∈ ℝ ∧ (𝑃 ∈ ℝ ∧ 0 < 𝑃)) → (((𝑄 / 2) · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ↔ (𝑄 / 2) ≤ ((𝑄 · (2 · 𝑢)) / 𝑃)))
371	323, 368, 348, 369, 370	syl112anc 1253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑄 / 2) · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ↔ (𝑄 / 2) ≤ ((𝑄 · (2 · 𝑢)) / 𝑃)))
372	367, 371	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 / 2) ≤ ((𝑄 · (2 · 𝑢)) / 𝑃))
373	253, 77, 75, 256	div23apd 8849	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 · (2 · 𝑢)) / 𝑃) = ((𝑄 / 𝑃) · (2 · 𝑢)))
374	372, 373	breqtrd 4056	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 / 2) ≤ ((𝑄 / 𝑃) · (2 · 𝑢)))
375	317, 323, 267, 331, 374	letrd 8145	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)))
376	311	nnzd 9441	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → 𝑁 ∈ ℤ)
377	376	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ∈ ℤ)
378		flqge 10354	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℚ ∧ 𝑁 ∈ ℤ) → (𝑁 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)) ↔ 𝑁 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
379	30, 377, 378	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑁 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)) ↔ 𝑁 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
380	375, 379	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))
381	322, 380	eqbrtrd 4052	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − 𝑁) ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))
382	315, 317, 318, 381	subled 8569	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ≤ 𝑁)
383	382	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ≤ 𝑁)
384	314	nnzd 9441	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) ∈ ℤ)
385	384, 31	zsubcld 9447	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℤ)
386	385	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℤ)
387	386	zred 9442	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℝ)
388	311	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑁 ∈ ℕ)
389	388	nnred 8997	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑁 ∈ ℝ)
390		letr 8104	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑦 ∈ ℝ ∧ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∧ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ≤ 𝑁) → 𝑦 ≤ 𝑁))
391	249, 387, 389, 390	syl3anc 1249	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∧ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ≤ 𝑁) → 𝑦 ≤ 𝑁))
392	383, 391	mpan2d 428	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) → 𝑦 ≤ 𝑁))
393	392	pm4.71rd 394	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ↔ (𝑦 ≤ 𝑁 ∧ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
394	310, 393	bitr4d 191	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 ≤ 𝑁 ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄)) ↔ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
395	394	pm5.32da 452	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑦 ∈ ℕ ∧ (𝑦 ≤ 𝑁 ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
396	395	adantr 276	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → ((𝑦 ∈ ℕ ∧ (𝑦 ≤ 𝑁 ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
397	242, 396	bitrid 192	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (((𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁) ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄)) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
398		simpr 110	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → 𝑥 = (𝑃 − (2 · 𝑢)))
399	211	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℤ)
400	399, 26	zsubcld 9447	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − (2 · 𝑢)) ∈ ℤ)
401		elfzle2 10097	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) → 𝑢 ≤ 𝑀)
402	401	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ≤ 𝑀)
403	402, 6	breqtrdi 4071	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ≤ ((𝑃 − 1) / 2))
404		lemuldiv2 8903	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑢 ∈ ℝ ∧ (𝑃 − 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 𝑢) ≤ (𝑃 − 1) ↔ 𝑢 ≤ ((𝑃 − 1) / 2)))
405	337, 350, 325, 326, 404	syl112anc 1253	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑢) ≤ (𝑃 − 1) ↔ 𝑢 ≤ ((𝑃 − 1) / 2)))
406	403, 405	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ≤ (𝑃 − 1))
407	348	ltm1d 8953	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − 1) < 𝑃)
408	266, 350, 348, 406, 407	lelttrd 8146	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) < 𝑃)
409	266, 348	posdifd 8553	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑢) < 𝑃 ↔ 0 < (𝑃 − (2 · 𝑢))))
410	408, 409	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 0 < (𝑃 − (2 · 𝑢)))
411		elnnz 9330	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑃 − (2 · 𝑢)) ∈ ℕ ↔ ((𝑃 − (2 · 𝑢)) ∈ ℤ ∧ 0 < (𝑃 − (2 · 𝑢))))
412	400, 410, 411	sylanbrc 417	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − (2 · 𝑢)) ∈ ℕ)
413	75, 77, 302	sub32d 8364	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) − 1) = ((𝑃 − 1) − (2 · 𝑢)))
414	6, 6	oveq12i 5931	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑀 + 𝑀) = (((𝑃 − 1) / 2) + ((𝑃 − 1) / 2))
415	64, 213	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − 1) ∈ ℤ)
416	415	zcnd 9443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − 1) ∈ ℂ)
417	416	2halvesd 9231	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑃 − 1) / 2) + ((𝑃 − 1) / 2)) = (𝑃 − 1))
418	414, 417	eqtrid 2238	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑀 + 𝑀) = (𝑃 − 1))
419	418	oveq1d 5934	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑀 + 𝑀) − 𝑀) = ((𝑃 − 1) − 𝑀))
420	167	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑀 ∈ ℂ)
421	420, 420	pncan2d 8334	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑀 + 𝑀) − 𝑀) = 𝑀)
422	419, 421	eqtr3d 2228	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − 1) − 𝑀) = 𝑀)
423	422, 346	eqbrtrd 4052	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − 1) − 𝑀) < (2 · 𝑢))
424	350, 333, 266, 423	ltsub23d 8571	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − 1) − (2 · 𝑢)) < 𝑀)
425	413, 424	eqbrtrd 4052	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) − 1) < 𝑀)
426	7	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑀 ∈ ℕ)
427	426	nnzd 9441	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑀 ∈ ℤ)
428		zlem1lt 9376	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑃 − (2 · 𝑢)) ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑃 − (2 · 𝑢)) ≤ 𝑀 ↔ ((𝑃 − (2 · 𝑢)) − 1) < 𝑀))
429	400, 427, 428	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) ≤ 𝑀 ↔ ((𝑃 − (2 · 𝑢)) − 1) < 𝑀))
430	425, 429	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − (2 · 𝑢)) ≤ 𝑀)
431		fznn 10158	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑀 ∈ ℤ → ((𝑃 − (2 · 𝑢)) ∈ (1...𝑀) ↔ ((𝑃 − (2 · 𝑢)) ∈ ℕ ∧ (𝑃 − (2 · 𝑢)) ≤ 𝑀)))
432	427, 431	syl 14	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) ∈ (1...𝑀) ↔ ((𝑃 − (2 · 𝑢)) ∈ ℕ ∧ (𝑃 − (2 · 𝑢)) ≤ 𝑀)))
433	412, 430, 432	mpbir2and 946	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − (2 · 𝑢)) ∈ (1...𝑀))
434	433	adantr 276	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (𝑃 − (2 · 𝑢)) ∈ (1...𝑀))
435	398, 434	eqeltrd 2270	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → 𝑥 ∈ (1...𝑀))
436	435	biantrurd 305	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (𝑦 ∈ (1...𝑁) ↔ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))))
437	376	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → 𝑁 ∈ ℤ)
438		fznn 10158	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℤ → (𝑦 ∈ (1...𝑁) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁)))
439	437, 438	syl 14	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (𝑦 ∈ (1...𝑁) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁)))
440	436, 439	bitr3d 190	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁)))
441	398	oveq1d 5934	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (𝑥 · 𝑄) = ((𝑃 − (2 · 𝑢)) · 𝑄))
442	441	breq2d 4042	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → ((𝑦 · 𝑃) < (𝑥 · 𝑄) ↔ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄)))
443	440, 442	anbi12d 473	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)) ↔ ((𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁) ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄))))
444	385	adantr 276	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℤ)
445		fznn 10158	. . . . . . . . . . . . . . . . . . 19 ⊢ (((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℤ → (𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
446	444, 445	syl 14	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
447	397, 443, 446	3bitr4d 220	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)) ↔ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
448	241, 447	bitrid 192	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (⟨𝑥, 𝑦⟩ ∈ 𝑆 ↔ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
449	448	pm5.32da 452	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑥 = (𝑃 − (2 · 𝑢)) ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑆) ↔ (𝑥 = (𝑃 − (2 · 𝑢)) ∧ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))))
450		vex 2763	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑥 ∈ V
451		vex 2763	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑦 ∈ V
452	450, 451	op1std 6203	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (1^st ‘𝑧) = 𝑥)
453	452	eqeq1d 2202	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → ((1^st ‘𝑧) = (𝑃 − (2 · 𝑢)) ↔ 𝑥 = (𝑃 − (2 · 𝑢))))
454	453	elrab 2917	. . . . . . . . . . . . . . . 16 ⊢ (⟨𝑥, 𝑦⟩ ∈ {𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))} ↔ (⟨𝑥, 𝑦⟩ ∈ 𝑆 ∧ 𝑥 = (𝑃 − (2 · 𝑢))))
455	454	biancomi 270	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑥, 𝑦⟩ ∈ {𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))} ↔ (𝑥 = (𝑃 − (2 · 𝑢)) ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑆))
456		opelxp 4690	. . . . . . . . . . . . . . . 16 ⊢ (⟨𝑥, 𝑦⟩ ∈ ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ↔ (𝑥 ∈ {(𝑃 − (2 · 𝑢))} ∧ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
457		velsn 3636	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ {(𝑃 − (2 · 𝑢))} ↔ 𝑥 = (𝑃 − (2 · 𝑢)))
458	457	anbi1i 458	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ {(𝑃 − (2 · 𝑢))} ∧ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ↔ (𝑥 = (𝑃 − (2 · 𝑢)) ∧ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
459	456, 458	bitri 184	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑥, 𝑦⟩ ∈ ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ↔ (𝑥 = (𝑃 − (2 · 𝑢)) ∧ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
460	449, 455, 459	3bitr4g 223	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⟨𝑥, 𝑦⟩ ∈ {𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))} ↔ ⟨𝑥, 𝑦⟩ ∈ ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))))
461	237, 238, 460	eqrelrdv 4756	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → {𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))} = ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
462	461	fveq2d 5559	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (♯‘{𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))}) = (♯‘({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))))
463		1zzd 9347	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 1 ∈ ℤ)
464	463, 385	fzfigd 10505	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ∈ Fin)
465		xpsnen2g 6885	. . . . . . . . . . . . . 14 ⊢ (((𝑃 − (2 · 𝑢)) ∈ ℤ ∧ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ∈ Fin) → ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ≈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
466	400, 464, 465	syl2anc 411	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ≈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
467	461, 69	eqeltrrd 2271	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ∈ Fin)
468		hashen 10858	. . . . . . . . . . . . . 14 ⊢ ((({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ∈ Fin ∧ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ∈ Fin) → ((♯‘({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) = (♯‘(1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ↔ ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ≈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
469	467, 464, 468	syl2anc 411	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((♯‘({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) = (♯‘(1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ↔ ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ≈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
470	466, 469	mpbird 167	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (♯‘({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) = (♯‘(1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
471		ltmul2 8877	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((2 · 𝑢) ∈ ℝ ∧ 𝑃 ∈ ℝ ∧ (𝑄 ∈ ℝ ∧ 0 < 𝑄)) → ((2 · 𝑢) < 𝑃 ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · 𝑃)))
472	266, 348, 252, 363, 471	syl112anc 1253	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑢) < 𝑃 ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · 𝑃)))
473	408, 472	mpbid 147	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 · (2 · 𝑢)) < (𝑄 · 𝑃))
474		ltdivmul2 8899	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑄 · (2 · 𝑢)) ∈ ℝ ∧ 𝑄 ∈ ℝ ∧ (𝑃 ∈ ℝ ∧ 0 < 𝑃)) → (((𝑄 · (2 · 𝑢)) / 𝑃) < 𝑄 ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · 𝑃)))
475	368, 252, 348, 369, 474	syl112anc 1253	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑄 · (2 · 𝑢)) / 𝑃) < 𝑄 ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · 𝑃)))
476	473, 475	mpbird 167	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 · (2 · 𝑢)) / 𝑃) < 𝑄)
477	373, 476	eqbrtrrd 4054	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 𝑃) · (2 · 𝑢)) < 𝑄)
478		flqlt 10355	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℚ ∧ 𝑄 ∈ ℤ) → (((𝑄 / 𝑃) · (2 · 𝑢)) < 𝑄 ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < 𝑄))
479	30, 284, 478	syl2anc 411	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑄 / 𝑃) · (2 · 𝑢)) < 𝑄 ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < 𝑄))
480	477, 479	mpbid 147	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < 𝑄)
481		zltlem1 9377	. . . . . . . . . . . . . . . . 17 ⊢ (((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ ∧ 𝑄 ∈ ℤ) → ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < 𝑄 ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ≤ (𝑄 − 1)))
482	31, 284, 481	syl2anc 411	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < 𝑄 ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ≤ (𝑄 − 1)))
483	480, 482	mpbid 147	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ≤ (𝑄 − 1))
484	483, 300	breqtrrd 4058	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ≤ (2 · 𝑁))
485		eluz2 9601	. . . . . . . . . . . . . 14 ⊢ ((2 · 𝑁) ∈ (ℤ_≥‘(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ↔ ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ ∧ (2 · 𝑁) ∈ ℤ ∧ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ≤ (2 · 𝑁)))
486	31, 384, 484, 485	syl3anbrc 1183	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) ∈ (ℤ_≥‘(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
487		uznn0sub 9627	. . . . . . . . . . . . 13 ⊢ ((2 · 𝑁) ∈ (ℤ_≥‘(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℕ₀)
488		hashfz1 10857	. . . . . . . . . . . . 13 ⊢ (((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℕ₀ → (♯‘(1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) = ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
489	486, 487, 488	3syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (♯‘(1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) = ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
490	462, 470, 489	3eqtrd 2230	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (♯‘{𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))}) = ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
491	490	sumeq2dv 11514	. . . . . . . . . 10 ⊢ (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(♯‘{𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))}) = Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
492	92, 233, 491	3eqtr3rd 2235	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)}))
493	313	nncnd 8998	. . . . . . . . . . 11 ⊢ (𝜑 → (2 · 𝑁) ∈ ℂ)
494	493	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) ∈ ℂ)
495	14, 494, 303	fsumsub 11598	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) − Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
496	492, 495	eqtr3d 2228	. . . . . . . 8 ⊢ (𝜑 → (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)}) = (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) − Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
497	496	oveq2d 5935	. . . . . . 7 ⊢ (𝜑 → (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)})) = (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) − Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
498	32	zcnd 9443	. . . . . . . 8 ⊢ (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℂ)
499	14, 384	fsumzcl 11548	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) ∈ ℤ)
500	499	zcnd 9443	. . . . . . . 8 ⊢ (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) ∈ ℂ)
501	498, 500	pncan3d 8335	. . . . . . 7 ⊢ (𝜑 → (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) − Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁))
502		fsumconst 11600	. . . . . . . . 9 ⊢ (((((⌊‘(𝑀 / 2)) + 1)...𝑀) ∈ Fin ∧ (2 · 𝑁) ∈ ℂ) → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) = ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · (2 · 𝑁)))
503	14, 493, 502	syl2anc 411	. . . . . . . 8 ⊢ (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) = ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · (2 · 𝑁)))
504		hashcl 10855	. . . . . . . . . . 11 ⊢ ((((⌊‘(𝑀 / 2)) + 1)...𝑀) ∈ Fin → (♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∈ ℕ₀)
505	14, 504	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → (♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∈ ℕ₀)
506	505	nn0cnd 9298	. . . . . . . . 9 ⊢ (𝜑 → (♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∈ ℂ)
507		2cnd 9057	. . . . . . . . 9 ⊢ (𝜑 → 2 ∈ ℂ)
508	506, 507, 319	mul12d 8173	. . . . . . . 8 ⊢ (𝜑 → ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · (2 · 𝑁)) = (2 · ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)))
509	503, 508	eqtrd 2226	. . . . . . 7 ⊢ (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) = (2 · ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)))
510	497, 501, 509	3eqtrd 2230	. . . . . 6 ⊢ (𝜑 → (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)})) = (2 · ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)))
511	510	oveq2d 5935	. . . . 5 ⊢ (𝜑 → (-1↑(Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)}))) = (-1↑(2 · ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁))))
512	22	a1i 9	. . . . . 6 ⊢ (𝜑 → 2 ∈ ℤ)
513	505	nn0zd 9440	. . . . . . 7 ⊢ (𝜑 → (♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∈ ℤ)
514	513, 376	zmulcld 9448	. . . . . 6 ⊢ (𝜑 → ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁) ∈ ℤ)
515		expmulzap 10659	. . . . . 6 ⊢ (((-1 ∈ ℂ ∧ -1 # 0) ∧ (2 ∈ ℤ ∧ ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁) ∈ ℤ)) → (-1↑(2 · ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁))) = ((-1↑2)↑((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)))
516	2, 4, 512, 514, 515	syl22anc 1250	. . . . 5 ⊢ (𝜑 → (-1↑(2 · ((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁))) = ((-1↑2)↑((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)))
517		neg1sqe1 10708	. . . . . . 7 ⊢ (-1↑2) = 1
518	517	oveq1i 5929	. . . . . 6 ⊢ ((-1↑2)↑((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)) = (1↑((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁))
519		1exp 10642	. . . . . . 7 ⊢ (((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁) ∈ ℤ → (1↑((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)) = 1)
520	514, 519	syl 14	. . . . . 6 ⊢ (𝜑 → (1↑((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)) = 1)
521	518, 520	eqtrid 2238	. . . . 5 ⊢ (𝜑 → ((-1↑2)↑((♯‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)) = 1)
522	511, 516, 521	3eqtrd 2230	. . . 4 ⊢ (𝜑 → (-1↑(Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)}))) = 1)
523	44, 55, 522	3eqtr4d 2236	. . 3 ⊢ (𝜑 → ((-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)})) · (-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)}))) = (-1↑(Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)}))))
524		expaddzap 10657	. . . 4 ⊢ (((-1 ∈ ℂ ∧ -1 # 0) ∧ (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ ∧ (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)}) ∈ ℤ)) → (-1↑(Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)}))) = ((-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) · (-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)}))))
525	2, 4, 32, 42, 524	syl22anc 1250	. . 3 ⊢ (𝜑 → (-1↑(Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)}))) = ((-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) · (-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)}))))
526	523, 525	eqtr2d 2227	. 2 ⊢ (𝜑 → ((-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) · (-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)}))) = ((-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)})) · (-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)}))))
527	33, 41, 41, 43, 526	mulcanap2ad 8685	1 ⊢ (𝜑 → (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (-1↑(♯‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)})))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 DECID wdc 835 = wceq 1364 ∈ wcel 2164 ≠ wne 2364 ∀wral 2472 ∃wrex 2473 {crab 2476 ∖ cdif 3151 ⊆ wss 3154 {csn 3619 ⟨cop 3622 ∪ ciun 3913 Disj wdisj 4007 class class class wbr 4030 {copab 4090 × cxp 4658 Rel wrel 4665 ‘cfv 5255 (class class class)co 5919 1^st c1st 6193 ≈ cen 6794 Fincfn 6796 ℂcc 7872 ℝcr 7873 0cc0 7874 1c1 7875 + caddc 7877 · cmul 7879 < clt 8056 ≤ cle 8057 − cmin 8192 -cneg 8193 # cap 8602 / cdiv 8693 ℕcn 8984 2c2 9035 ℕ₀cn0 9243 ℤcz 9320 ℤ_≥cuz 9595 ℚcq 9687 ...cfz 10077 ⌊cfl 10340 ↑cexp 10612 ♯chash 10849 Σcsu 11499 ∥ cdvds 11933 ℙcprime 12248

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 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-13 2166 ax-14 2167 ax-ext 2175 ax-coll 4145 ax-sep 4148 ax-nul 4156 ax-pow 4204 ax-pr 4239 ax-un 4465 ax-setind 4570 ax-iinf 4621 ax-cnex 7965 ax-resscn 7966 ax-1cn 7967 ax-1re 7968 ax-icn 7969 ax-addcl 7970 ax-addrcl 7971 ax-mulcl 7972 ax-mulrcl 7973 ax-addcom 7974 ax-mulcom 7975 ax-addass 7976 ax-mulass 7977 ax-distr 7978 ax-i2m1 7979 ax-0lt1 7980 ax-1rid 7981 ax-0id 7982 ax-rnegex 7983 ax-precex 7984 ax-cnre 7985 ax-pre-ltirr 7986 ax-pre-ltwlin 7987 ax-pre-lttrn 7988 ax-pre-apti 7989 ax-pre-ltadd 7990 ax-pre-mulgt0 7991 ax-pre-mulext 7992 ax-arch 7993 ax-caucvg 7994

This theorem depends on definitions: df-bi 117 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-xor 1387 df-nf 1472 df-sb 1774 df-eu 2045 df-mo 2046 df-clab 2180 df-cleq 2186 df-clel 2189 df-nfc 2325 df-ne 2365 df-nel 2460 df-ral 2477 df-rex 2478 df-reu 2479 df-rmo 2480 df-rab 2481 df-v 2762 df-sbc 2987 df-csb 3082 df-dif 3156 df-un 3158 df-in 3160 df-ss 3167 df-nul 3448 df-if 3559 df-pw 3604 df-sn 3625 df-pr 3626 df-op 3628 df-uni 3837 df-int 3872 df-iun 3915 df-disj 4008 df-br 4031 df-opab 4092 df-mpt 4093 df-tr 4129 df-id 4325 df-po 4328 df-iso 4329 df-iord 4398 df-on 4400 df-ilim 4401 df-suc 4403 df-iom 4624 df-xp 4666 df-rel 4667 df-cnv 4668 df-co 4669 df-dm 4670 df-rn 4671 df-res 4672 df-ima 4673 df-iota 5216 df-fun 5257 df-fn 5258 df-f 5259 df-f1 5260 df-fo 5261 df-f1o 5262 df-fv 5263 df-isom 5264 df-riota 5874 df-ov 5922 df-oprab 5923 df-mpo 5924 df-1st 6195 df-2nd 6196 df-recs 6360 df-irdg 6425 df-frec 6446 df-1o 6471 df-2o 6472 df-oadd 6475 df-er 6589 df-en 6797 df-dom 6798 df-fin 6799 df-pnf 8058 df-mnf 8059 df-xr 8060 df-ltxr 8061 df-le 8062 df-sub 8194 df-neg 8195 df-reap 8596 df-ap 8603 df-div 8694 df-inn 8985 df-2 9043 df-3 9044 df-4 9045 df-n0 9244 df-z 9321 df-uz 9596 df-q 9688 df-rp 9723 df-fz 10078 df-fzo 10212 df-fl 10342 df-mod 10397 df-seqfrec 10522 df-exp 10613 df-ihash 10850 df-cj 10989 df-re 10990 df-im 10991 df-rsqrt 11145 df-abs 11146 df-clim 11425 df-sumdc 11500 df-dvds 11934 df-prm 12249

This theorem is referenced by: lgsquadlem2 15235

W3C validator