lgsquadlem1 - Metamath Proof Explorer

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

Theorem lgsquadlem1 24905

Description: Lemma for lgsquad 24908. 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 11001	. . . 4 ⊢ -1 ∈ ℂ
2	1	a1i 11	. . 3 ⊢ (𝜑 → -1 ∈ ℂ)
3		neg1ne0 11003	. . . 4 ⊢ -1 ≠ 0
4	3	a1i 11	. . 3 ⊢ (𝜑 → -1 ≠ 0)
5		fzfid 12634	. . . 4 ⊢ (𝜑 → (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∈ Fin)
6		lgseisen.2	. . . . . . . . . 10 ⊢ (𝜑 → 𝑄 ∈ (ℙ ∖ {2}))
7		eldifi 3694	. . . . . . . . . 10 ⊢ (𝑄 ∈ (ℙ ∖ {2}) → 𝑄 ∈ ℙ)
8		prmnn 15226	. . . . . . . . . 10 ⊢ (𝑄 ∈ ℙ → 𝑄 ∈ ℕ)
9	6, 7, 8	3syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝑄 ∈ ℕ)
10	9	nnred 10912	. . . . . . . 8 ⊢ (𝜑 → 𝑄 ∈ ℝ)
11		lgseisen.1	. . . . . . . . 9 ⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))
12		eldifi 3694	. . . . . . . . 9 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℙ)
13		prmnn 15226	. . . . . . . . 9 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
14	11, 12, 13	3syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝑃 ∈ ℕ)
15	10, 14	nndivred 10946	. . . . . . 7 ⊢ (𝜑 → (𝑄 / 𝑃) ∈ ℝ)
16	15	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 / 𝑃) ∈ ℝ)
17		2z 11286	. . . . . . . 8 ⊢ 2 ∈ ℤ
18		elfzelz 12213	. . . . . . . . 9 ⊢ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) → 𝑢 ∈ ℤ)
19	18	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ∈ ℤ)
20		zmulcl 11303	. . . . . . . 8 ⊢ ((2 ∈ ℤ ∧ 𝑢 ∈ ℤ) → (2 · 𝑢) ∈ ℤ)
21	17, 19, 20	sylancr 694	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ∈ ℤ)
22	21	zred 11358	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ∈ ℝ)
23	16, 22	remulcld 9949	. . . . 5 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ)
24	23	flcld 12461	. . . 4 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ)
25	5, 24	fsumzcl 14313	. . 3 ⊢ (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ)
26	2, 4, 25	expclzd 12875	. 2 ⊢ (𝜑 → (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℂ)
27		fzfid 12634	. . . . . . 7 ⊢ (𝜑 → (1...𝑀) ∈ Fin)
28		fzfid 12634	. . . . . . 7 ⊢ (𝜑 → (1...𝑁) ∈ Fin)
29		xpfi 8116	. . . . . . 7 ⊢ (((1...𝑀) ∈ Fin ∧ (1...𝑁) ∈ Fin) → ((1...𝑀) × (1...𝑁)) ∈ Fin)
30	27, 28, 29	syl2anc 691	. . . . . 6 ⊢ (𝜑 → ((1...𝑀) × (1...𝑁)) ∈ Fin)
31		lgsquad.6	. . . . . . 7 ⊢ 𝑆 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))}
32		opabssxp 5116	. . . . . . 7 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} ⊆ ((1...𝑀) × (1...𝑁))
33	31, 32	eqsstri 3598	. . . . . 6 ⊢ 𝑆 ⊆ ((1...𝑀) × (1...𝑁))
34		ssfi 8065	. . . . . 6 ⊢ ((((1...𝑀) × (1...𝑁)) ∈ Fin ∧ 𝑆 ⊆ ((1...𝑀) × (1...𝑁))) → 𝑆 ∈ Fin)
35	30, 33, 34	sylancl 693	. . . . 5 ⊢ (𝜑 → 𝑆 ∈ Fin)
36		ssrab2 3650	. . . . 5 ⊢ {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)} ⊆ 𝑆
37		ssfi 8065	. . . . 5 ⊢ ((𝑆 ∈ Fin ∧ {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)} ⊆ 𝑆) → {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)} ∈ Fin)
38	35, 36, 37	sylancl 693	. . . 4 ⊢ (𝜑 → {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)} ∈ Fin)
39		hashcl 13009	. . . 4 ⊢ ({𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)} ∈ Fin → (#‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)}) ∈ ℕ₀)
40	38, 39	syl 17	. . 3 ⊢ (𝜑 → (#‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)}) ∈ ℕ₀)
41		expcl 12740	. . 3 ⊢ ((-1 ∈ ℂ ∧ (#‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)}) ∈ ℕ₀) → (-1↑(#‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)})) ∈ ℂ)
42	1, 40, 41	sylancr 694	. 2 ⊢ (𝜑 → (-1↑(#‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)})) ∈ ℂ)
43	40	nn0zd 11356	. . 3 ⊢ (𝜑 → (#‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)}) ∈ ℤ)
44	2, 4, 43	expne0d 12876	. 2 ⊢ (𝜑 → (-1↑(#‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)})) ≠ 0)
45	42, 44	recidd 10675	. . . 4 ⊢ (𝜑 → ((-1↑(#‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)})) · (1 / (-1↑(#‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)})))) = 1)
46		1div1e1 10596	. . . . . . . . 9 ⊢ (1 / 1) = 1
47	46	negeqi 10153	. . . . . . . 8 ⊢ -(1 / 1) = -1
48		ax-1cn 9873	. . . . . . . . 9 ⊢ 1 ∈ ℂ
49		ax-1ne0 9884	. . . . . . . . 9 ⊢ 1 ≠ 0
50		divneg2 10628	. . . . . . . . 9 ⊢ ((1 ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ≠ 0) → -(1 / 1) = (1 / -1))
51	48, 48, 49, 50	mp3an 1416	. . . . . . . 8 ⊢ -(1 / 1) = (1 / -1)
52	47, 51	eqtr3i 2634	. . . . . . 7 ⊢ -1 = (1 / -1)
53	52	oveq1i 6559	. . . . . 6 ⊢ (-1↑(#‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)})) = ((1 / -1)↑(#‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)}))
54	2, 4, 43	exprecd 12878	. . . . . 6 ⊢ (𝜑 → ((1 / -1)↑(#‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)})) = (1 / (-1↑(#‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)}))))
55	53, 54	syl5eq 2656	. . . . 5 ⊢ (𝜑 → (-1↑(#‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)})) = (1 / (-1↑(#‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)}))))
56	55	oveq2d 6565	. . . 4 ⊢ (𝜑 → ((-1↑(#‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)})) · (-1↑(#‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)}))) = ((-1↑(#‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)})) · (1 / (-1↑(#‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)})))))
57	35	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑆 ∈ Fin)
58		ssrab2 3650	. . . . . . . . . . . 12 ⊢ {𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))} ⊆ 𝑆
59		ssfi 8065	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ Fin ∧ {𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))} ⊆ 𝑆) → {𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))} ∈ Fin)
60	57, 58, 59	sylancl 693	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → {𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))} ∈ Fin)
61		fveq2 6103	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = 𝑣 → (1^st ‘𝑧) = (1^st ‘𝑣))
62	61	eqeq1d 2612	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = 𝑣 → ((1^st ‘𝑧) = (𝑃 − (2 · 𝑢)) ↔ (1^st ‘𝑣) = (𝑃 − (2 · 𝑢))))
63	62	elrab 3331	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))} ↔ (𝑣 ∈ 𝑆 ∧ (1^st ‘𝑣) = (𝑃 − (2 · 𝑢))))
64	63	simprbi 479	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))} → (1^st ‘𝑣) = (𝑃 − (2 · 𝑢)))
65	64	ad2antll 761	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → (1^st ‘𝑣) = (𝑃 − (2 · 𝑢)))
66	65	oveq2d 6565	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → (𝑃 − (1^st ‘𝑣)) = (𝑃 − (𝑃 − (2 · 𝑢))))
67	14	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℕ)
68	67	nncnd 10913	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℂ)
69	68	adantrr 749	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → 𝑃 ∈ ℂ)
70	21	zcnd 11359	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ∈ ℂ)
71	70	adantrr 749	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → (2 · 𝑢) ∈ ℂ)
72	69, 71	nncand 10276	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → (𝑃 − (𝑃 − (2 · 𝑢))) = (2 · 𝑢))
73	66, 72	eqtrd 2644	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → (𝑃 − (1^st ‘𝑣)) = (2 · 𝑢))
74	73	oveq1d 6564	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → ((𝑃 − (1^st ‘𝑣)) / 2) = ((2 · 𝑢) / 2))
75	19	zcnd 11359	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ∈ ℂ)
76	75	adantrr 749	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → 𝑢 ∈ ℂ)
77		2cnd 10970	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → 2 ∈ ℂ)
78		2ne0 10990	. . . . . . . . . . . . . . . 16 ⊢ 2 ≠ 0
79	78	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → 2 ≠ 0)
80	76, 77, 79	divcan3d 10685	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → ((2 · 𝑢) / 2) = 𝑢)
81	74, 80	eqtrd 2644	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ 𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))})) → ((𝑃 − (1^st ‘𝑣)) / 2) = 𝑢)
82	81	ralrimivva 2954	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)∀𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))} ((𝑃 − (1^st ‘𝑣)) / 2) = 𝑢)
83		invdisj 4571	. . . . . . . . . . . 12 ⊢ (∀𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)∀𝑣 ∈ {𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))} ((𝑃 − (1^st ‘𝑣)) / 2) = 𝑢 → Disj 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))})
84	82, 83	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → Disj 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))})
85	5, 60, 84	hashiun 14395	. . . . . . . . . 10 ⊢ (𝜑 → (#‘∪ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))}) = Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(#‘{𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))}))
86		iunrab 4503	. . . . . . . . . . . 12 ⊢ ∪ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))} = {𝑧 ∈ 𝑆 ∣ ∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1^st ‘𝑧) = (𝑃 − (2 · 𝑢))}
87		eldifsni 4261	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ≠ 2)
88	11, 87	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑃 ≠ 2)
89	88	necomd 2837	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 2 ≠ 𝑃)
90	89	neneqd 2787	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ¬ 2 = 𝑃)
91	90	ad2antrr 758	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ¬ 2 = 𝑃)
92		uzid 11578	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (2 ∈ ℤ → 2 ∈ (ℤ_≥‘2))
93	17, 92	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 ∈ (ℤ_≥‘2)
94	11, 12	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑃 ∈ ℙ)
95	94	ad2antrr 758	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℙ)
96		dvdsprm 15253	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2 ∈ (ℤ_≥‘2) ∧ 𝑃 ∈ ℙ) → (2 ∥ 𝑃 ↔ 2 = 𝑃))
97	93, 95, 96	sylancr 694	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 ∥ 𝑃 ↔ 2 = 𝑃))
98	91, 97	mtbird 314	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ¬ 2 ∥ 𝑃)
99	14	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℕ)
100	99	nncnd 10913	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℂ)
101	21	adantlr 747	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ∈ ℤ)
102	101	zcnd 11359	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ∈ ℂ)
103	100, 102	npcand 10275	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) + (2 · 𝑢)) = 𝑃)
104	103	breq2d 4595	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 ∥ ((𝑃 − (2 · 𝑢)) + (2 · 𝑢)) ↔ 2 ∥ 𝑃))
105	98, 104	mtbird 314	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ¬ 2 ∥ ((𝑃 − (2 · 𝑢)) + (2 · 𝑢)))
106	18	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ∈ ℤ)
107		dvdsmul1 14841	. . . . . . . . . . . . . . . . . . 19 ⊢ ((2 ∈ ℤ ∧ 𝑢 ∈ ℤ) → 2 ∥ (2 · 𝑢))
108	17, 106, 107	sylancr 694	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 2 ∥ (2 · 𝑢))
109	17	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 2 ∈ ℤ)
110	99	nnzd 11357	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℤ)
111	110, 101	zsubcld 11363	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − (2 · 𝑢)) ∈ ℤ)
112		dvds2add 14853	. . . . . . . . . . . . . . . . . . 19 ⊢ ((2 ∈ ℤ ∧ (𝑃 − (2 · 𝑢)) ∈ ℤ ∧ (2 · 𝑢) ∈ ℤ) → ((2 ∥ (𝑃 − (2 · 𝑢)) ∧ 2 ∥ (2 · 𝑢)) → 2 ∥ ((𝑃 − (2 · 𝑢)) + (2 · 𝑢))))
113	109, 111, 101, 112	syl3anc 1318	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 ∥ (𝑃 − (2 · 𝑢)) ∧ 2 ∥ (2 · 𝑢)) → 2 ∥ ((𝑃 − (2 · 𝑢)) + (2 · 𝑢))))
114	108, 113	mpan2d 706	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 ∥ (𝑃 − (2 · 𝑢)) → 2 ∥ ((𝑃 − (2 · 𝑢)) + (2 · 𝑢))))
115	105, 114	mtod 188	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ¬ 2 ∥ (𝑃 − (2 · 𝑢)))
116		breq2 4587	. . . . . . . . . . . . . . . . 17 ⊢ ((1^st ‘𝑧) = (𝑃 − (2 · 𝑢)) → (2 ∥ (1^st ‘𝑧) ↔ 2 ∥ (𝑃 − (2 · 𝑢))))
117	116	notbid 307	. . . . . . . . . . . . . . . 16 ⊢ ((1^st ‘𝑧) = (𝑃 − (2 · 𝑢)) → (¬ 2 ∥ (1^st ‘𝑧) ↔ ¬ 2 ∥ (𝑃 − (2 · 𝑢))))
118	115, 117	syl5ibrcom 236	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((1^st ‘𝑧) = (𝑃 − (2 · 𝑢)) → ¬ 2 ∥ (1^st ‘𝑧)))
119	118	rexlimdva 3013	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1^st ‘𝑧) = (𝑃 − (2 · 𝑢)) → ¬ 2 ∥ (1^st ‘𝑧)))
120		simpr 476	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → 𝑧 ∈ 𝑆)
121	33, 120	sseldi 3566	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → 𝑧 ∈ ((1...𝑀) × (1...𝑁)))
122		xp1st 7089	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ ((1...𝑀) × (1...𝑁)) → (1^st ‘𝑧) ∈ (1...𝑀))
123	121, 122	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (1^st ‘𝑧) ∈ (1...𝑀))
124		elfzelz 12213	. . . . . . . . . . . . . . . 16 ⊢ ((1^st ‘𝑧) ∈ (1...𝑀) → (1^st ‘𝑧) ∈ ℤ)
125		odd2np1 14903	. . . . . . . . . . . . . . . 16 ⊢ ((1^st ‘𝑧) ∈ ℤ → (¬ 2 ∥ (1^st ‘𝑧) ↔ ∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = (1^st ‘𝑧)))
126	123, 124, 125	3syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (¬ 2 ∥ (1^st ‘𝑧) ↔ ∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = (1^st ‘𝑧)))
127		lgsquad.4	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑀 = ((𝑃 − 1) / 2)
128		oddprm 15353	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((𝑃 − 1) / 2) ∈ ℕ)
129	11, 128	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((𝑃 − 1) / 2) ∈ ℕ)
130	127, 129	syl5eqel 2692	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑀 ∈ ℕ)
131	130	nnred 10912	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑀 ∈ ℝ)
132	131	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → 𝑀 ∈ ℝ)
133	132	rehalfcld 11156	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (𝑀 / 2) ∈ ℝ)
134		reflcl 12459	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑀 / 2) ∈ ℝ → (⌊‘(𝑀 / 2)) ∈ ℝ)
135	133, 134	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (⌊‘(𝑀 / 2)) ∈ ℝ)
136	130	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → 𝑀 ∈ ℕ)
137	136	nnzd 11357	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → 𝑀 ∈ ℤ)
138		simprl 790	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → 𝑛 ∈ ℤ)
139	137, 138	zsubcld 11363	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (𝑀 − 𝑛) ∈ ℤ)
140	139	zred 11358	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (𝑀 − 𝑛) ∈ ℝ)
141		flle 12462	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑀 / 2) ∈ ℝ → (⌊‘(𝑀 / 2)) ≤ (𝑀 / 2))
142	133, 141	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (⌊‘(𝑀 / 2)) ≤ (𝑀 / 2))
143		zre 11258	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ ℤ → 𝑛 ∈ ℝ)
144	143	ad2antrl 760	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → 𝑛 ∈ ℝ)
145		simprr 792	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → ((2 · 𝑛) + 1) = (1^st ‘𝑧))
146	123	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (1^st ‘𝑧) ∈ (1...𝑀))
147	145, 146	eqeltrd 2688	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → ((2 · 𝑛) + 1) ∈ (1...𝑀))
148		elfzle2 12216	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((2 · 𝑛) + 1) ∈ (1...𝑀) → ((2 · 𝑛) + 1) ≤ 𝑀)
149	147, 148	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → ((2 · 𝑛) + 1) ≤ 𝑀)
150		zmulcl 11303	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((2 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (2 · 𝑛) ∈ ℤ)
151	17, 138, 150	sylancr 694	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (2 · 𝑛) ∈ ℤ)
152		zltp1le 11304	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((2 · 𝑛) ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((2 · 𝑛) < 𝑀 ↔ ((2 · 𝑛) + 1) ≤ 𝑀))
153	151, 137, 152	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → ((2 · 𝑛) < 𝑀 ↔ ((2 · 𝑛) + 1) ≤ 𝑀))
154	149, 153	mpbird 246	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (2 · 𝑛) < 𝑀)
155		2re 10967	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 2 ∈ ℝ
156	155	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → 2 ∈ ℝ)
157		2pos 10989	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 0 < 2
158	157	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → 0 < 2)
159		ltmuldiv2 10776	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑛 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 𝑛) < 𝑀 ↔ 𝑛 < (𝑀 / 2)))
160	144, 132, 156, 158, 159	syl112anc 1322	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → ((2 · 𝑛) < 𝑀 ↔ 𝑛 < (𝑀 / 2)))
161	154, 160	mpbid 221	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → 𝑛 < (𝑀 / 2))
162	133	recnd 9947	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (𝑀 / 2) ∈ ℂ)
163	162, 162	pncan2d 10273	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (((𝑀 / 2) + (𝑀 / 2)) − (𝑀 / 2)) = (𝑀 / 2))
164	130	nncnd 10913	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑀 ∈ ℂ)
165	164	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → 𝑀 ∈ ℂ)
166	165	2halvesd 11155	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → ((𝑀 / 2) + (𝑀 / 2)) = 𝑀)
167	166	oveq1d 6564	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (((𝑀 / 2) + (𝑀 / 2)) − (𝑀 / 2)) = (𝑀 − (𝑀 / 2)))
168	163, 167	eqtr3d 2646	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (𝑀 / 2) = (𝑀 − (𝑀 / 2)))
169	161, 168	breqtrd 4609	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → 𝑛 < (𝑀 − (𝑀 / 2)))
170	144, 132, 133, 169	ltsub13d 10512	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (𝑀 / 2) < (𝑀 − 𝑛))
171	135, 133, 140, 142, 170	lelttrd 10074	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (⌊‘(𝑀 / 2)) < (𝑀 − 𝑛))
172	133	flcld 12461	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (⌊‘(𝑀 / 2)) ∈ ℤ)
173		zltp1le 11304	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((⌊‘(𝑀 / 2)) ∈ ℤ ∧ (𝑀 − 𝑛) ∈ ℤ) → ((⌊‘(𝑀 / 2)) < (𝑀 − 𝑛) ↔ ((⌊‘(𝑀 / 2)) + 1) ≤ (𝑀 − 𝑛)))
174	172, 139, 173	syl2anc 691	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → ((⌊‘(𝑀 / 2)) < (𝑀 − 𝑛) ↔ ((⌊‘(𝑀 / 2)) + 1) ≤ (𝑀 − 𝑛)))
175	171, 174	mpbid 221	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → ((⌊‘(𝑀 / 2)) + 1) ≤ (𝑀 − 𝑛))
176		2t0e0 11060	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (2 · 0) = 0
177		2cn 10968	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 2 ∈ ℂ
178		zcn 11259	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑛 ∈ ℤ → 𝑛 ∈ ℂ)
179	178	ad2antrl 760	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → 𝑛 ∈ ℂ)
180		mulcl 9899	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((2 ∈ ℂ ∧ 𝑛 ∈ ℂ) → (2 · 𝑛) ∈ ℂ)
181	177, 179, 180	sylancr 694	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (2 · 𝑛) ∈ ℂ)
182		pncan 10166	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((2 · 𝑛) ∈ ℂ ∧ 1 ∈ ℂ) → (((2 · 𝑛) + 1) − 1) = (2 · 𝑛))
183	181, 48, 182	sylancl 693	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (((2 · 𝑛) + 1) − 1) = (2 · 𝑛))
184		elfznn 12241	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((2 · 𝑛) + 1) ∈ (1...𝑀) → ((2 · 𝑛) + 1) ∈ ℕ)
185		nnm1nn0 11211	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((2 · 𝑛) + 1) ∈ ℕ → (((2 · 𝑛) + 1) − 1) ∈ ℕ₀)
186	147, 184, 185	3syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (((2 · 𝑛) + 1) − 1) ∈ ℕ₀)
187	183, 186	eqeltrrd 2689	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (2 · 𝑛) ∈ ℕ₀)
188	187	nn0ge0d 11231	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → 0 ≤ (2 · 𝑛))
189	176, 188	syl5eqbr 4618	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (2 · 0) ≤ (2 · 𝑛))
190		0red 9920	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → 0 ∈ ℝ)
191		lemul2 10755	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((0 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (0 ≤ 𝑛 ↔ (2 · 0) ≤ (2 · 𝑛)))
192	190, 144, 156, 158, 191	syl112anc 1322	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (0 ≤ 𝑛 ↔ (2 · 0) ≤ (2 · 𝑛)))
193	189, 192	mpbird 246	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → 0 ≤ 𝑛)
194	132, 144	subge02d 10498	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (0 ≤ 𝑛 ↔ (𝑀 − 𝑛) ≤ 𝑀))
195	193, 194	mpbid 221	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (𝑀 − 𝑛) ≤ 𝑀)
196	172	peano2zd 11361	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → ((⌊‘(𝑀 / 2)) + 1) ∈ ℤ)
197		elfz 12203	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 − 𝑛) ∈ ℤ ∧ ((⌊‘(𝑀 / 2)) + 1) ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑀 − 𝑛) ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ↔ (((⌊‘(𝑀 / 2)) + 1) ≤ (𝑀 − 𝑛) ∧ (𝑀 − 𝑛) ≤ 𝑀)))
198	139, 196, 137, 197	syl3anc 1318	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → ((𝑀 − 𝑛) ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ↔ (((⌊‘(𝑀 / 2)) + 1) ≤ (𝑀 − 𝑛) ∧ (𝑀 − 𝑛) ≤ 𝑀)))
199	175, 195, 198	mpbir2and 959	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (𝑀 − 𝑛) ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀))
200	94	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → 𝑃 ∈ ℙ)
201	200, 13	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → 𝑃 ∈ ℕ)
202	201	nncnd 10913	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → 𝑃 ∈ ℂ)
203		peano2cn 10087	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2 · 𝑛) ∈ ℂ → ((2 · 𝑛) + 1) ∈ ℂ)
204	181, 203	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → ((2 · 𝑛) + 1) ∈ ℂ)
205	202, 204	nncand 10276	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (𝑃 − (𝑃 − ((2 · 𝑛) + 1))) = ((2 · 𝑛) + 1))
206		1cnd 9935	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → 1 ∈ ℂ)
207	202, 181, 206	sub32d 10303	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → ((𝑃 − (2 · 𝑛)) − 1) = ((𝑃 − 1) − (2 · 𝑛)))
208	202, 181, 206	subsub4d 10302	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → ((𝑃 − (2 · 𝑛)) − 1) = (𝑃 − ((2 · 𝑛) + 1)))
209		2cnd 10970	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → 2 ∈ ℂ)
210	209, 165, 179	subdid 10365	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (2 · (𝑀 − 𝑛)) = ((2 · 𝑀) − (2 · 𝑛)))
211	127	oveq2i 6560	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (2 · 𝑀) = (2 · ((𝑃 − 1) / 2))
212	14	nnzd 11357	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑃 ∈ ℤ)
213	212	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → 𝑃 ∈ ℤ)
214		peano2zm 11297	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑃 ∈ ℤ → (𝑃 − 1) ∈ ℤ)
215	213, 214	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (𝑃 − 1) ∈ ℤ)
216	215	zcnd 11359	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (𝑃 − 1) ∈ ℂ)
217	78	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → 2 ≠ 0)
218	216, 209, 217	divcan2d 10682	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (2 · ((𝑃 − 1) / 2)) = (𝑃 − 1))
219	211, 218	syl5eq 2656	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (2 · 𝑀) = (𝑃 − 1))
220	219	oveq1d 6564	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → ((2 · 𝑀) − (2 · 𝑛)) = ((𝑃 − 1) − (2 · 𝑛)))
221	210, 220	eqtr2d 2645	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → ((𝑃 − 1) − (2 · 𝑛)) = (2 · (𝑀 − 𝑛)))
222	207, 208, 221	3eqtr3d 2652	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (𝑃 − ((2 · 𝑛) + 1)) = (2 · (𝑀 − 𝑛)))
223	222	oveq2d 6565	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (𝑃 − (𝑃 − ((2 · 𝑛) + 1))) = (𝑃 − (2 · (𝑀 − 𝑛))))
224	205, 223, 145	3eqtr3rd 2653	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → (1^st ‘𝑧) = (𝑃 − (2 · (𝑀 − 𝑛))))
225		oveq2 6557	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 = (𝑀 − 𝑛) → (2 · 𝑢) = (2 · (𝑀 − 𝑛)))
226	225	oveq2d 6565	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 = (𝑀 − 𝑛) → (𝑃 − (2 · 𝑢)) = (𝑃 − (2 · (𝑀 − 𝑛))))
227	226	eqeq2d 2620	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 = (𝑀 − 𝑛) → ((1^st ‘𝑧) = (𝑃 − (2 · 𝑢)) ↔ (1^st ‘𝑧) = (𝑃 − (2 · (𝑀 − 𝑛)))))
228	227	rspcev 3282	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 − 𝑛) ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) ∧ (1^st ‘𝑧) = (𝑃 − (2 · (𝑀 − 𝑛)))) → ∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1^st ‘𝑧) = (𝑃 − (2 · 𝑢)))
229	199, 224, 228	syl2anc 691	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ (𝑛 ∈ ℤ ∧ ((2 · 𝑛) + 1) = (1^st ‘𝑧))) → ∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1^st ‘𝑧) = (𝑃 − (2 · 𝑢)))
230	229	rexlimdvaa 3014	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = (1^st ‘𝑧) → ∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1^st ‘𝑧) = (𝑃 − (2 · 𝑢))))
231	126, 230	sylbid 229	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (¬ 2 ∥ (1^st ‘𝑧) → ∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1^st ‘𝑧) = (𝑃 − (2 · 𝑢))))
232	119, 231	impbid 201	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1^st ‘𝑧) = (𝑃 − (2 · 𝑢)) ↔ ¬ 2 ∥ (1^st ‘𝑧)))
233	232	rabbidva 3163	. . . . . . . . . . . 12 ⊢ (𝜑 → {𝑧 ∈ 𝑆 ∣ ∃𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(1^st ‘𝑧) = (𝑃 − (2 · 𝑢))} = {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)})
234	86, 233	syl5eq 2656	. . . . . . . . . . 11 ⊢ (𝜑 → ∪ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))} = {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)})
235	234	fveq2d 6107	. . . . . . . . . 10 ⊢ (𝜑 → (#‘∪ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀){𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))}) = (#‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)}))
236	31	relopabi 5167	. . . . . . . . . . . . . . 15 ⊢ Rel 𝑆
237		relss 5129	. . . . . . . . . . . . . . 15 ⊢ ({𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))} ⊆ 𝑆 → (Rel 𝑆 → Rel {𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))}))
238	58, 236, 237	mp2 9	. . . . . . . . . . . . . 14 ⊢ Rel {𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))}
239		relxp 5150	. . . . . . . . . . . . . 14 ⊢ Rel ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
240	31	eleq2i 2680	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑥, 𝑦⟩ ∈ 𝑆 ↔ ⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))})
241		opabid 4907	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} ↔ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))
242	240, 241	bitri 263	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝑥, 𝑦⟩ ∈ 𝑆 ↔ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)))
243		anass 679	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁) ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄)) ↔ (𝑦 ∈ ℕ ∧ (𝑦 ≤ 𝑁 ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄))))
244	24	peano2zd 11361	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ∈ ℤ)
245	244	zred 11358	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ∈ ℝ)
246	245	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ∈ ℝ)
247	10	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑄 ∈ ℝ)
248		nnre 10904	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
249	248	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ ℝ)
250		lesub 10386	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ∈ ℝ ∧ 𝑄 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ≤ (𝑄 − 𝑦) ↔ 𝑦 ≤ (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1))))
251	246, 247, 249, 250	syl3anc 1318	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ≤ (𝑄 − 𝑦) ↔ 𝑦 ≤ (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1))))
252	10	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑄 ∈ ℝ)
253	252	recnd 9947	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑄 ∈ ℂ)
254	68, 253	mulcomd 9940	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 · 𝑄) = (𝑄 · 𝑃))
255	70, 253	mulcomd 9940	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑢) · 𝑄) = (𝑄 · (2 · 𝑢)))
256	67	nnne0d 10942	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ≠ 0)
257	253, 68, 256	divcan1d 10681	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 𝑃) · 𝑃) = 𝑄)
258	257	oveq1d 6564	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑄 / 𝑃) · 𝑃) · (2 · 𝑢)) = (𝑄 · (2 · 𝑢)))
259	16	recnd 9947	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 / 𝑃) ∈ ℂ)
260	259, 68, 70	mul32d 10125	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑄 / 𝑃) · 𝑃) · (2 · 𝑢)) = (((𝑄 / 𝑃) · (2 · 𝑢)) · 𝑃))
261	255, 258, 260	3eqtr2d 2650	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑢) · 𝑄) = (((𝑄 / 𝑃) · (2 · 𝑢)) · 𝑃))
262	254, 261	oveq12d 6567	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 · 𝑄) − ((2 · 𝑢) · 𝑄)) = ((𝑄 · 𝑃) − (((𝑄 / 𝑃) · (2 · 𝑢)) · 𝑃)))
263	68, 70, 253	subdird 10366	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) · 𝑄) = ((𝑃 · 𝑄) − ((2 · 𝑢) · 𝑄)))
264	23	recnd 9947	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℂ)
265	253, 264, 68	subdird 10366	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃) = ((𝑄 · 𝑃) − (((𝑄 / 𝑃) · (2 · 𝑢)) · 𝑃)))
266	262, 263, 265	3eqtr4d 2654	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) · 𝑄) = ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃))
267	266	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑃 − (2 · 𝑢)) · 𝑄) = ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃))
268	267	breq2d 4595	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄) ↔ (𝑦 · 𝑃) < ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃)))
269	23	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ)
270	247, 269	resubcld 10337	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℝ)
271	67	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℕ)
272	271	nnred 10912	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑃 ∈ ℝ)
273	271	nngt0d 10941	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 0 < 𝑃)
274		ltmul1 10752	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑦 ∈ ℝ ∧ (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℝ ∧ (𝑃 ∈ ℝ ∧ 0 < 𝑃)) → (𝑦 < (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ↔ (𝑦 · 𝑃) < ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃)))
275	249, 270, 272, 273, 274	syl112anc 1322	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑦 < (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ↔ (𝑦 · 𝑃) < ((𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) · 𝑃)))
276		ltsub13 10388	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑦 ∈ ℝ ∧ 𝑄 ∈ ℝ ∧ ((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ) → (𝑦 < (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ↔ ((𝑄 / 𝑃) · (2 · 𝑢)) < (𝑄 − 𝑦)))
277	249, 247, 269, 276	syl3anc 1318	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑦 < (𝑄 − ((𝑄 / 𝑃) · (2 · 𝑢))) ↔ ((𝑄 / 𝑃) · (2 · 𝑢)) < (𝑄 − 𝑦)))
278	268, 275, 277	3bitr2d 295	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄) ↔ ((𝑄 / 𝑃) · (2 · 𝑢)) < (𝑄 − 𝑦)))
279	9	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑄 ∈ ℕ)
280	279	nnzd 11357	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑄 ∈ ℤ)
281		nnz 11276	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℤ)
282		zsubcl 11296	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑄 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑄 − 𝑦) ∈ ℤ)
283	280, 281, 282	syl2an 493	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑄 − 𝑦) ∈ ℤ)
284		fllt 12469	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ ∧ (𝑄 − 𝑦) ∈ ℤ) → (((𝑄 / 𝑃) · (2 · 𝑢)) < (𝑄 − 𝑦) ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < (𝑄 − 𝑦)))
285	269, 283, 284	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (((𝑄 / 𝑃) · (2 · 𝑢)) < (𝑄 − 𝑦) ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < (𝑄 − 𝑦)))
286	24	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ)
287		zltp1le 11304	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ ∧ (𝑄 − 𝑦) ∈ ℤ) → ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < (𝑄 − 𝑦) ↔ ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ≤ (𝑄 − 𝑦)))
288	286, 283, 287	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < (𝑄 − 𝑦) ↔ ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ≤ (𝑄 − 𝑦)))
289	278, 285, 288	3bitrd 293	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄) ↔ ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1) ≤ (𝑄 − 𝑦)))
290		lgsquad.5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 𝑁 = ((𝑄 − 1) / 2)
291	290	oveq2i 6560	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (2 · 𝑁) = (2 · ((𝑄 − 1) / 2))
292		peano2rem 10227	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑄 ∈ ℝ → (𝑄 − 1) ∈ ℝ)
293	252, 292	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 − 1) ∈ ℝ)
294	293	recnd 9947	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 − 1) ∈ ℂ)
295		2cnd 10970	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 2 ∈ ℂ)
296	78	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 2 ≠ 0)
297	294, 295, 296	divcan2d 10682	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · ((𝑄 − 1) / 2)) = (𝑄 − 1))
298	291, 297	syl5eq 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) = (𝑄 − 1))
299	298	oveq1d 6564	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = ((𝑄 − 1) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
300		1cnd 9935	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 1 ∈ ℂ)
301	24	zcnd 11359	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℂ)
302	253, 300, 301	sub32d 10303	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 − 1) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = ((𝑄 − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) − 1))
303	253, 301, 300	subsub4d 10302	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) − 1) = (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1)))
304	299, 302, 303	3eqtrd 2648	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1)))
305	304	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1)))
306	305	breq2d 4595	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ↔ 𝑦 ≤ (𝑄 − ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + 1))))
307	251, 289, 306	3bitr4d 299	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄) ↔ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
308	307	anbi2d 736	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 ≤ 𝑁 ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄)) ↔ (𝑦 ≤ 𝑁 ∧ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
309		2nn 11062	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 2 ∈ ℕ
310		oddprm 15353	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑄 ∈ (ℙ ∖ {2}) → ((𝑄 − 1) / 2) ∈ ℕ)
311	6, 310	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → ((𝑄 − 1) / 2) ∈ ℕ)
312	290, 311	syl5eqel 2692	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 𝑁 ∈ ℕ)
313		nnmulcl 10920	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((2 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (2 · 𝑁) ∈ ℕ)
314	309, 312, 313	sylancr 694	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (2 · 𝑁) ∈ ℕ)
315	314	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) ∈ ℕ)
316	315	nnred 10912	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) ∈ ℝ)
317	312	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ∈ ℕ)
318	317	nnred 10912	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ∈ ℝ)
319	24	zred 11358	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℝ)
320	312	nncnd 10913	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → 𝑁 ∈ ℂ)
321	320	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ∈ ℂ)
322	321	2timesd 11152	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) = (𝑁 + 𝑁))
323	322	oveq1d 6564	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − 𝑁) = ((𝑁 + 𝑁) − 𝑁))
324	321, 321	pncan2d 10273	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑁 + 𝑁) − 𝑁) = 𝑁)
325	323, 324	eqtrd 2644	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − 𝑁) = 𝑁)
326	252	rehalfcld 11156	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 / 2) ∈ ℝ)
327	252	ltm1d 10835	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 − 1) < 𝑄)
328	155	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 2 ∈ ℝ)
329	157	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 0 < 2)
330		ltdiv1 10766	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑄 − 1) ∈ ℝ ∧ 𝑄 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((𝑄 − 1) < 𝑄 ↔ ((𝑄 − 1) / 2) < (𝑄 / 2)))
331	293, 252, 328, 329, 330	syl112anc 1322	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 − 1) < 𝑄 ↔ ((𝑄 − 1) / 2) < (𝑄 / 2)))
332	327, 331	mpbid 221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 − 1) / 2) < (𝑄 / 2))
333	290, 332	syl5eqbr 4618	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 < (𝑄 / 2))
334	318, 326, 333	ltled 10064	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ≤ (𝑄 / 2))
335	253, 295, 68, 296	div32d 10703	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 2) · 𝑃) = (𝑄 · (𝑃 / 2)))
336	131	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑀 ∈ ℝ)
337	336	rehalfcld 11156	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑀 / 2) ∈ ℝ)
338		peano2re 10088	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((⌊‘(𝑀 / 2)) ∈ ℝ → ((⌊‘(𝑀 / 2)) + 1) ∈ ℝ)
339	337, 134, 338	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((⌊‘(𝑀 / 2)) + 1) ∈ ℝ)
340	19	zred 11358	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ∈ ℝ)
341		flltp1 12463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝑀 / 2) ∈ ℝ → (𝑀 / 2) < ((⌊‘(𝑀 / 2)) + 1))
342	337, 341	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑀 / 2) < ((⌊‘(𝑀 / 2)) + 1))
343		elfzle1 12215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) → ((⌊‘(𝑀 / 2)) + 1) ≤ 𝑢)
344	343	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((⌊‘(𝑀 / 2)) + 1) ≤ 𝑢)
345	337, 339, 340, 342, 344	ltletrd 10076	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑀 / 2) < 𝑢)
346		ltdivmul 10777	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝑀 ∈ ℝ ∧ 𝑢 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((𝑀 / 2) < 𝑢 ↔ 𝑀 < (2 · 𝑢)))
347	336, 340, 328, 329, 346	syl112anc 1322	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑀 / 2) < 𝑢 ↔ 𝑀 < (2 · 𝑢)))
348	345, 347	mpbid 221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑀 < (2 · 𝑢))
349	127, 348	syl5eqbrr 4619	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − 1) / 2) < (2 · 𝑢))
350	67	nnred 10912	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℝ)
351		peano2rem 10227	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑃 ∈ ℝ → (𝑃 − 1) ∈ ℝ)
352	350, 351	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − 1) ∈ ℝ)
353		ltdivmul 10777	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((𝑃 − 1) ∈ ℝ ∧ (2 · 𝑢) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (((𝑃 − 1) / 2) < (2 · 𝑢) ↔ (𝑃 − 1) < (2 · (2 · 𝑢))))
354	352, 22, 328, 329, 353	syl112anc 1322	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑃 − 1) / 2) < (2 · 𝑢) ↔ (𝑃 − 1) < (2 · (2 · 𝑢))))
355	349, 354	mpbid 221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − 1) < (2 · (2 · 𝑢)))
356	212	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℤ)
357		zmulcl 11303	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((2 ∈ ℤ ∧ (2 · 𝑢) ∈ ℤ) → (2 · (2 · 𝑢)) ∈ ℤ)
358	17, 21, 357	sylancr 694	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · (2 · 𝑢)) ∈ ℤ)
359		zlem1lt 11306	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑃 ∈ ℤ ∧ (2 · (2 · 𝑢)) ∈ ℤ) → (𝑃 ≤ (2 · (2 · 𝑢)) ↔ (𝑃 − 1) < (2 · (2 · 𝑢))))
360	356, 358, 359	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 ≤ (2 · (2 · 𝑢)) ↔ (𝑃 − 1) < (2 · (2 · 𝑢))))
361	355, 360	mpbird 246	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ≤ (2 · (2 · 𝑢)))
362		ledivmul 10778	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑃 ∈ ℝ ∧ (2 · 𝑢) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((𝑃 / 2) ≤ (2 · 𝑢) ↔ 𝑃 ≤ (2 · (2 · 𝑢))))
363	350, 22, 328, 329, 362	syl112anc 1322	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 / 2) ≤ (2 · 𝑢) ↔ 𝑃 ≤ (2 · (2 · 𝑢))))
364	361, 363	mpbird 246	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 / 2) ≤ (2 · 𝑢))
365	350	rehalfcld 11156	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 / 2) ∈ ℝ)
366	279	nngt0d 10941	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 0 < 𝑄)
367		lemul2 10755	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝑃 / 2) ∈ ℝ ∧ (2 · 𝑢) ∈ ℝ ∧ (𝑄 ∈ ℝ ∧ 0 < 𝑄)) → ((𝑃 / 2) ≤ (2 · 𝑢) ↔ (𝑄 · (𝑃 / 2)) ≤ (𝑄 · (2 · 𝑢))))
368	365, 22, 252, 366, 367	syl112anc 1322	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 / 2) ≤ (2 · 𝑢) ↔ (𝑄 · (𝑃 / 2)) ≤ (𝑄 · (2 · 𝑢))))
369	364, 368	mpbid 221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 · (𝑃 / 2)) ≤ (𝑄 · (2 · 𝑢)))
370	335, 369	eqbrtrd 4605	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 2) · 𝑃) ≤ (𝑄 · (2 · 𝑢)))
371	252, 22	remulcld 9949	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 · (2 · 𝑢)) ∈ ℝ)
372	67	nngt0d 10941	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 0 < 𝑃)
373		lemuldiv 10782	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑄 / 2) ∈ ℝ ∧ (𝑄 · (2 · 𝑢)) ∈ ℝ ∧ (𝑃 ∈ ℝ ∧ 0 < 𝑃)) → (((𝑄 / 2) · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ↔ (𝑄 / 2) ≤ ((𝑄 · (2 · 𝑢)) / 𝑃)))
374	326, 371, 350, 372, 373	syl112anc 1322	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑄 / 2) · 𝑃) ≤ (𝑄 · (2 · 𝑢)) ↔ (𝑄 / 2) ≤ ((𝑄 · (2 · 𝑢)) / 𝑃)))
375	370, 374	mpbid 221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 / 2) ≤ ((𝑄 · (2 · 𝑢)) / 𝑃))
376	253, 70, 68, 256	div23d 10717	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 · (2 · 𝑢)) / 𝑃) = ((𝑄 / 𝑃) · (2 · 𝑢)))
377	375, 376	breqtrd 4609	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 / 2) ≤ ((𝑄 / 𝑃) · (2 · 𝑢)))
378	318, 326, 23, 334, 377	letrd 10073	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)))
379	312	nnzd 11357	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → 𝑁 ∈ ℤ)
380	379	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ∈ ℤ)
381		flge 12468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ ∧ 𝑁 ∈ ℤ) → (𝑁 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)) ↔ 𝑁 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
382	23, 380, 381	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑁 ≤ ((𝑄 / 𝑃) · (2 · 𝑢)) ↔ 𝑁 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
383	378, 382	mpbid 221	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑁 ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))
384	325, 383	eqbrtrd 4605	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − 𝑁) ≤ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))
385	316, 318, 319, 384	subled 10509	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ≤ 𝑁)
386	385	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ≤ 𝑁)
387	315	nnzd 11357	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) ∈ ℤ)
388	387, 24	zsubcld 11363	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℤ)
389	388	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℤ)
390	389	zred 11358	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℝ)
391	312	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑁 ∈ ℕ)
392	391	nnred 10912	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → 𝑁 ∈ ℝ)
393		letr 10010	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑦 ∈ ℝ ∧ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∧ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ≤ 𝑁) → 𝑦 ≤ 𝑁))
394	249, 390, 392, 393	syl3anc 1318	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∧ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ≤ 𝑁) → 𝑦 ≤ 𝑁))
395	386, 394	mpan2d 706	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) → 𝑦 ≤ 𝑁))
396	395	pm4.71rd 665	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → (𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ↔ (𝑦 ≤ 𝑁 ∧ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
397	308, 396	bitr4d 270	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑦 ∈ ℕ) → ((𝑦 ≤ 𝑁 ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄)) ↔ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
398	397	pm5.32da 671	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑦 ∈ ℕ ∧ (𝑦 ≤ 𝑁 ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
399	398	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → ((𝑦 ∈ ℕ ∧ (𝑦 ≤ 𝑁 ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
400	243, 399	syl5bb 271	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (((𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁) ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄)) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
401		simpr 476	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → 𝑥 = (𝑃 − (2 · 𝑢)))
402	356, 21	zsubcld 11363	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − (2 · 𝑢)) ∈ ℤ)
403		elfzle2 12216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀) → 𝑢 ≤ 𝑀)
404	403	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ≤ 𝑀)
405	404, 127	syl6breq 4624	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑢 ≤ ((𝑃 − 1) / 2))
406		lemuldiv2 10783	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑢 ∈ ℝ ∧ (𝑃 − 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 𝑢) ≤ (𝑃 − 1) ↔ 𝑢 ≤ ((𝑃 − 1) / 2)))
407	340, 352, 328, 329, 406	syl112anc 1322	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑢) ≤ (𝑃 − 1) ↔ 𝑢 ≤ ((𝑃 − 1) / 2)))
408	405, 407	mpbird 246	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) ≤ (𝑃 − 1))
409	350	ltm1d 10835	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − 1) < 𝑃)
410	22, 352, 350, 408, 409	lelttrd 10074	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑢) < 𝑃)
411	22, 350	posdifd 10493	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑢) < 𝑃 ↔ 0 < (𝑃 − (2 · 𝑢))))
412	410, 411	mpbid 221	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 0 < (𝑃 − (2 · 𝑢)))
413		elnnz 11264	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑃 − (2 · 𝑢)) ∈ ℕ ↔ ((𝑃 − (2 · 𝑢)) ∈ ℤ ∧ 0 < (𝑃 − (2 · 𝑢))))
414	402, 412, 413	sylanbrc 695	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − (2 · 𝑢)) ∈ ℕ)
415	68, 70, 300	sub32d 10303	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) − 1) = ((𝑃 − 1) − (2 · 𝑢)))
416	127, 127	oveq12i 6561	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑀 + 𝑀) = (((𝑃 − 1) / 2) + ((𝑃 − 1) / 2))
417	67	nnzd 11357	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑃 ∈ ℤ)
418	417, 214	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − 1) ∈ ℤ)
419	418	zcnd 11359	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − 1) ∈ ℂ)
420	419	2halvesd 11155	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑃 − 1) / 2) + ((𝑃 − 1) / 2)) = (𝑃 − 1))
421	416, 420	syl5eq 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑀 + 𝑀) = (𝑃 − 1))
422	421	oveq1d 6564	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑀 + 𝑀) − 𝑀) = ((𝑃 − 1) − 𝑀))
423	164	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑀 ∈ ℂ)
424	423, 423	pncan2d 10273	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑀 + 𝑀) − 𝑀) = 𝑀)
425	422, 424	eqtr3d 2646	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − 1) − 𝑀) = 𝑀)
426	425, 348	eqbrtrd 4605	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − 1) − 𝑀) < (2 · 𝑢))
427	352, 336, 22, 426	ltsub23d 10511	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − 1) − (2 · 𝑢)) < 𝑀)
428	415, 427	eqbrtrd 4605	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) − 1) < 𝑀)
429	130	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑀 ∈ ℕ)
430	429	nnzd 11357	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → 𝑀 ∈ ℤ)
431		zlem1lt 11306	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑃 − (2 · 𝑢)) ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑃 − (2 · 𝑢)) ≤ 𝑀 ↔ ((𝑃 − (2 · 𝑢)) − 1) < 𝑀))
432	402, 430, 431	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) ≤ 𝑀 ↔ ((𝑃 − (2 · 𝑢)) − 1) < 𝑀))
433	428, 432	mpbird 246	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − (2 · 𝑢)) ≤ 𝑀)
434		fznn 12278	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑀 ∈ ℤ → ((𝑃 − (2 · 𝑢)) ∈ (1...𝑀) ↔ ((𝑃 − (2 · 𝑢)) ∈ ℕ ∧ (𝑃 − (2 · 𝑢)) ≤ 𝑀)))
435	430, 434	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑃 − (2 · 𝑢)) ∈ (1...𝑀) ↔ ((𝑃 − (2 · 𝑢)) ∈ ℕ ∧ (𝑃 − (2 · 𝑢)) ≤ 𝑀)))
436	414, 433, 435	mpbir2and 959	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑃 − (2 · 𝑢)) ∈ (1...𝑀))
437	436	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (𝑃 − (2 · 𝑢)) ∈ (1...𝑀))
438	401, 437	eqeltrd 2688	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → 𝑥 ∈ (1...𝑀))
439	438	biantrurd 528	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (𝑦 ∈ (1...𝑁) ↔ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁))))
440	379	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → 𝑁 ∈ ℤ)
441		fznn 12278	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℤ → (𝑦 ∈ (1...𝑁) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁)))
442	440, 441	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (𝑦 ∈ (1...𝑁) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁)))
443	439, 442	bitr3d 269	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁)))
444	401	oveq1d 6564	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (𝑥 · 𝑄) = ((𝑃 − (2 · 𝑢)) · 𝑄))
445	444	breq2d 4595	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → ((𝑦 · 𝑃) < (𝑥 · 𝑄) ↔ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄)))
446	443, 445	anbi12d 743	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)) ↔ ((𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁) ∧ (𝑦 · 𝑃) < ((𝑃 − (2 · 𝑢)) · 𝑄))))
447	388	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℤ)
448		fznn 12278	. . . . . . . . . . . . . . . . . . 19 ⊢ (((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℤ → (𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
449	447, 448	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ↔ (𝑦 ∈ ℕ ∧ 𝑦 ≤ ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
450	400, 446, 449	3bitr4d 299	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄)) ↔ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
451	242, 450	syl5bb 271	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∧ 𝑥 = (𝑃 − (2 · 𝑢))) → (⟨𝑥, 𝑦⟩ ∈ 𝑆 ↔ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
452	451	pm5.32da 671	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑥 = (𝑃 − (2 · 𝑢)) ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑆) ↔ (𝑥 = (𝑃 − (2 · 𝑢)) ∧ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))))
453		vex 3176	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑥 ∈ V
454		vex 3176	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑦 ∈ V
455	453, 454	op1std 7069	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (1^st ‘𝑧) = 𝑥)
456	455	eqeq1d 2612	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → ((1^st ‘𝑧) = (𝑃 − (2 · 𝑢)) ↔ 𝑥 = (𝑃 − (2 · 𝑢))))
457	456	elrab 3331	. . . . . . . . . . . . . . . 16 ⊢ (⟨𝑥, 𝑦⟩ ∈ {𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))} ↔ (⟨𝑥, 𝑦⟩ ∈ 𝑆 ∧ 𝑥 = (𝑃 − (2 · 𝑢))))
458		ancom 465	. . . . . . . . . . . . . . . 16 ⊢ ((⟨𝑥, 𝑦⟩ ∈ 𝑆 ∧ 𝑥 = (𝑃 − (2 · 𝑢))) ↔ (𝑥 = (𝑃 − (2 · 𝑢)) ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑆))
459	457, 458	bitri 263	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑥, 𝑦⟩ ∈ {𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))} ↔ (𝑥 = (𝑃 − (2 · 𝑢)) ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑆))
460		opelxp 5070	. . . . . . . . . . . . . . . 16 ⊢ (⟨𝑥, 𝑦⟩ ∈ ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ↔ (𝑥 ∈ {(𝑃 − (2 · 𝑢))} ∧ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
461		velsn 4141	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ {(𝑃 − (2 · 𝑢))} ↔ 𝑥 = (𝑃 − (2 · 𝑢)))
462	461	anbi1i 727	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ {(𝑃 − (2 · 𝑢))} ∧ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ↔ (𝑥 = (𝑃 − (2 · 𝑢)) ∧ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
463	460, 462	bitri 263	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑥, 𝑦⟩ ∈ ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ↔ (𝑥 = (𝑃 − (2 · 𝑢)) ∧ 𝑦 ∈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
464	452, 459, 463	3bitr4g 302	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⟨𝑥, 𝑦⟩ ∈ {𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))} ↔ ⟨𝑥, 𝑦⟩ ∈ ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))))
465	238, 239, 464	eqrelrdv 5139	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → {𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))} = ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
466	465	fveq2d 6107	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (#‘{𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))}) = (#‘({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))))
467		fzfid 12634	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ∈ Fin)
468		xpsnen2g 7938	. . . . . . . . . . . . . 14 ⊢ (((𝑃 − (2 · 𝑢)) ∈ ℤ ∧ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) ∈ Fin) → ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ≈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
469	402, 467, 468	syl2anc 691	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ≈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
470		hasheni 12998	. . . . . . . . . . . . 13 ⊢ (({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) ≈ (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) → (#‘({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) = (#‘(1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
471	469, 470	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (#‘({(𝑃 − (2 · 𝑢))} × (1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))) = (#‘(1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))))
472		ltmul2 10753	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((2 · 𝑢) ∈ ℝ ∧ 𝑃 ∈ ℝ ∧ (𝑄 ∈ ℝ ∧ 0 < 𝑄)) → ((2 · 𝑢) < 𝑃 ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · 𝑃)))
473	22, 350, 252, 366, 472	syl112anc 1322	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((2 · 𝑢) < 𝑃 ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · 𝑃)))
474	410, 473	mpbid 221	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (𝑄 · (2 · 𝑢)) < (𝑄 · 𝑃))
475		ltdivmul2 10779	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑄 · (2 · 𝑢)) ∈ ℝ ∧ 𝑄 ∈ ℝ ∧ (𝑃 ∈ ℝ ∧ 0 < 𝑃)) → (((𝑄 · (2 · 𝑢)) / 𝑃) < 𝑄 ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · 𝑃)))
476	371, 252, 350, 372, 475	syl112anc 1322	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑄 · (2 · 𝑢)) / 𝑃) < 𝑄 ↔ (𝑄 · (2 · 𝑢)) < (𝑄 · 𝑃)))
477	474, 476	mpbird 246	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 · (2 · 𝑢)) / 𝑃) < 𝑄)
478	376, 477	eqbrtrrd 4607	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((𝑄 / 𝑃) · (2 · 𝑢)) < 𝑄)
479		fllt 12469	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑄 / 𝑃) · (2 · 𝑢)) ∈ ℝ ∧ 𝑄 ∈ ℤ) → (((𝑄 / 𝑃) · (2 · 𝑢)) < 𝑄 ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < 𝑄))
480	23, 280, 479	syl2anc 691	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (((𝑄 / 𝑃) · (2 · 𝑢)) < 𝑄 ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < 𝑄))
481	478, 480	mpbid 221	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < 𝑄)
482		zltlem1 11307	. . . . . . . . . . . . . . . . 17 ⊢ (((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ ∧ 𝑄 ∈ ℤ) → ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < 𝑄 ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ≤ (𝑄 − 1)))
483	24, 280, 482	syl2anc 691	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) < 𝑄 ↔ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ≤ (𝑄 − 1)))
484	481, 483	mpbid 221	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ≤ (𝑄 − 1))
485	484, 298	breqtrrd 4611	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ≤ (2 · 𝑁))
486		eluz2 11569	. . . . . . . . . . . . . 14 ⊢ ((2 · 𝑁) ∈ (ℤ_≥‘(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ↔ ((⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℤ ∧ (2 · 𝑁) ∈ ℤ ∧ (⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ≤ (2 · 𝑁)))
487	24, 387, 485, 486	syl3anbrc 1239	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) ∈ (ℤ_≥‘(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
488		uznn0sub 11595	. . . . . . . . . . . . 13 ⊢ ((2 · 𝑁) ∈ (ℤ_≥‘(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) → ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℕ₀)
489		hashfz1 12996	. . . . . . . . . . . . 13 ⊢ (((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) ∈ ℕ₀ → (#‘(1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) = ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
490	487, 488, 489	3syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (#‘(1...((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))) = ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
491	466, 471, 490	3eqtrd 2648	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (#‘{𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))}) = ((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
492	491	sumeq2dv 14281	. . . . . . . . . 10 ⊢ (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(#‘{𝑧 ∈ 𝑆 ∣ (1^st ‘𝑧) = (𝑃 − (2 · 𝑢))}) = Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
493	85, 235, 492	3eqtr3rd 2653	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (#‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)}))
494	314	nncnd 10913	. . . . . . . . . . 11 ⊢ (𝜑 → (2 · 𝑁) ∈ ℂ)
495	494	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)) → (2 · 𝑁) ∈ ℂ)
496	5, 495, 301	fsumsub 14362	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)((2 · 𝑁) − (⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) − Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
497	493, 496	eqtr3d 2646	. . . . . . . 8 ⊢ (𝜑 → (#‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)}) = (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) − Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))))
498	497	oveq2d 6565	. . . . . . 7 ⊢ (𝜑 → (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (#‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)})) = (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) − Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))))
499	25	zcnd 11359	. . . . . . . 8 ⊢ (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) ∈ ℂ)
500	5, 387	fsumzcl 14313	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) ∈ ℤ)
501	500	zcnd 11359	. . . . . . . 8 ⊢ (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) ∈ ℂ)
502	499, 501	pncan3d 10274	. . . . . . 7 ⊢ (𝜑 → (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) − Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))))) = Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁))
503		fsumconst 14364	. . . . . . . . 9 ⊢ (((((⌊‘(𝑀 / 2)) + 1)...𝑀) ∈ Fin ∧ (2 · 𝑁) ∈ ℂ) → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) = ((#‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · (2 · 𝑁)))
504	5, 494, 503	syl2anc 691	. . . . . . . 8 ⊢ (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) = ((#‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · (2 · 𝑁)))
505		hashcl 13009	. . . . . . . . . . 11 ⊢ ((((⌊‘(𝑀 / 2)) + 1)...𝑀) ∈ Fin → (#‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∈ ℕ₀)
506	5, 505	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (#‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∈ ℕ₀)
507	506	nn0cnd 11230	. . . . . . . . 9 ⊢ (𝜑 → (#‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∈ ℂ)
508		2cnd 10970	. . . . . . . . 9 ⊢ (𝜑 → 2 ∈ ℂ)
509	507, 508, 320	mul12d 10124	. . . . . . . 8 ⊢ (𝜑 → ((#‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · (2 · 𝑁)) = (2 · ((#‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)))
510	504, 509	eqtrd 2644	. . . . . . 7 ⊢ (𝜑 → Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(2 · 𝑁) = (2 · ((#‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)))
511	498, 502, 510	3eqtrd 2648	. . . . . 6 ⊢ (𝜑 → (Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (#‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)})) = (2 · ((#‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)))
512	511	oveq2d 6565	. . . . 5 ⊢ (𝜑 → (-1↑(Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (#‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)}))) = (-1↑(2 · ((#‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁))))
513	17	a1i 11	. . . . . 6 ⊢ (𝜑 → 2 ∈ ℤ)
514	506	nn0zd 11356	. . . . . . 7 ⊢ (𝜑 → (#‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) ∈ ℤ)
515	514, 379	zmulcld 11364	. . . . . 6 ⊢ (𝜑 → ((#‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁) ∈ ℤ)
516		expmulz 12768	. . . . . 6 ⊢ (((-1 ∈ ℂ ∧ -1 ≠ 0) ∧ (2 ∈ ℤ ∧ ((#‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁) ∈ ℤ)) → (-1↑(2 · ((#‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁))) = ((-1↑2)↑((#‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)))
517	2, 4, 513, 515, 516	syl22anc 1319	. . . . 5 ⊢ (𝜑 → (-1↑(2 · ((#‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁))) = ((-1↑2)↑((#‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)))
518		neg1sqe1 12821	. . . . . . 7 ⊢ (-1↑2) = 1
519	518	oveq1i 6559	. . . . . 6 ⊢ ((-1↑2)↑((#‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)) = (1↑((#‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁))
520		1exp 12751	. . . . . . 7 ⊢ (((#‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁) ∈ ℤ → (1↑((#‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)) = 1)
521	515, 520	syl 17	. . . . . 6 ⊢ (𝜑 → (1↑((#‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)) = 1)
522	519, 521	syl5eq 2656	. . . . 5 ⊢ (𝜑 → ((-1↑2)↑((#‘(((⌊‘(𝑀 / 2)) + 1)...𝑀)) · 𝑁)) = 1)
523	512, 517, 522	3eqtrd 2648	. . . 4 ⊢ (𝜑 → (-1↑(Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (#‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)}))) = 1)
524	45, 56, 523	3eqtr4d 2654	. . 3 ⊢ (𝜑 → ((-1↑(#‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)})) · (-1↑(#‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)}))) = (-1↑(Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (#‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)}))))
525		expaddz 12766	. . . 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 ‘𝑧)}))))
526	2, 4, 25, 43, 525	syl22anc 1319	. . 3 ⊢ (𝜑 → (-1↑(Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢))) + (#‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)}))) = ((-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) · (-1↑(#‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)}))))
527	524, 526	eqtr2d 2645	. 2 ⊢ (𝜑 → ((-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) · (-1↑(#‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)}))) = ((-1↑(#‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)})) · (-1↑(#‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)}))))
528	26, 42, 42, 44, 527	mulcan2ad 10542	1 ⊢ (𝜑 → (-1↑Σ𝑢 ∈ (((⌊‘(𝑀 / 2)) + 1)...𝑀)(⌊‘((𝑄 / 𝑃) · (2 · 𝑢)))) = (-1↑(#‘{𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1^st ‘𝑧)})))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 195 ∧ wa 383 = wceq 1475 ∈ wcel 1977 ≠ wne 2780 ∀wral 2896 ∃wrex 2897 {crab 2900 ∖ cdif 3537 ⊆ wss 3540 {csn 4125 ⟨cop 4131 ∪ ciun 4455 Disj wdisj 4553 class class class wbr 4583 {copab 4642 × cxp 5036 Rel wrel 5043 ‘cfv 5804 (class class class)co 6549 1^st c1st 7057 ≈ cen 7838 Fincfn 7841 ℂcc 9813 ℝcr 9814 0cc0 9815 1c1 9816 + caddc 9818 · cmul 9820 < clt 9953 ≤ cle 9954 − cmin 10145 -cneg 10146 / cdiv 10563 ℕcn 10897 2c2 10947 ℕ₀cn0 11169 ℤcz 11254 ℤ_≥cuz 11563 ...cfz 12197 ⌊cfl 12453 ↑cexp 12722 #chash 12979 Σcsu 14264 ∥ cdvds 14821 ℙcprime 15223

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-inf2 8421 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892 ax-pre-sup 9893

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-fal 1481 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rmo 2904 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-int 4411 df-iun 4457 df-disj 4554 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-se 4998 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-isom 5813 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-om 6958 df-1st 7059 df-2nd 7060 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-1o 7447 df-2o 7448 df-oadd 7451 df-er 7629 df-en 7842 df-dom 7843 df-sdom 7844 df-fin 7845 df-sup 8231 df-inf 8232 df-oi 8298 df-card 8648 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-div 10564 df-nn 10898 df-2 10956 df-3 10957 df-n0 11170 df-z 11255 df-uz 11564 df-rp 11709 df-fz 12198 df-fzo 12335 df-fl 12455 df-seq 12664 df-exp 12723 df-hash 12980 df-cj 13687 df-re 13688 df-im 13689 df-sqrt 13823 df-abs 13824 df-clim 14067 df-sum 14265 df-dvds 14822 df-prm 15224

This theorem is referenced by: lgsquadlem2 24906

W3C validator