Theorem lgsquadlem2

Description: Lemma for lgsquad . Count the members of S with even coordinates, and combine with lgsquadlem1 to get the total count of lattice points in S (up to parity). (Contributed by Mario Carneiro, 18-Jun-2015)

	Ref	Expression
Hypotheses	lgseisen.1	⊢ ( 𝜑 → 𝑃 ∈ ( ℙ ∖ { 2 } ) )
	lgseisen.2	⊢ ( 𝜑 → 𝑄 ∈ ( ℙ ∖ { 2 } ) )
	lgseisen.3	⊢ ( 𝜑 → 𝑃 ≠ 𝑄 )
	lgsquad.4	⊢ 𝑀 = ( ( 𝑃 − 1 ) / 2 )
	lgsquad.5	⊢ 𝑁 = ( ( 𝑄 − 1 ) / 2 )
	lgsquad.6	⊢ 𝑆 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 1 ... 𝑀 ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑦 · 𝑃 ) < ( 𝑥 · 𝑄 ) ) }
Assertion	lgsquadlem2	⊢ ( 𝜑 → ( 𝑄 /L 𝑃 ) = ( - 1 ↑ ( ♯ ‘ 𝑆 ) ) )

Proof

Step	Hyp	Ref	Expression
1		lgseisen.1	⊢ ( 𝜑 → 𝑃 ∈ ( ℙ ∖ { 2 } ) )
2		lgseisen.2	⊢ ( 𝜑 → 𝑄 ∈ ( ℙ ∖ { 2 } ) )
3		lgseisen.3	⊢ ( 𝜑 → 𝑃 ≠ 𝑄 )
4		lgsquad.4	⊢ 𝑀 = ( ( 𝑃 − 1 ) / 2 )
5		lgsquad.5	⊢ 𝑁 = ( ( 𝑄 − 1 ) / 2 )
6		lgsquad.6	⊢ 𝑆 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 1 ... 𝑀 ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑦 · 𝑃 ) < ( 𝑥 · 𝑄 ) ) }
7	1 2 3	lgseisen	⊢ ( 𝜑 → ( 𝑄 /L 𝑃 ) = ( - 1 ↑ Σ 𝑢 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) )
8	4	oveq2i	⊢ ( 1 ... 𝑀 ) = ( 1 ... ( ( 𝑃 − 1 ) / 2 ) )
9	8	sumeq1i	⊢ Σ 𝑢 ∈ ( 1 ... 𝑀 ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) = Σ 𝑢 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) )
10	1 4	gausslemma2dlem0b	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
11	10	nnred	⊢ ( 𝜑 → 𝑀 ∈ ℝ )
12	11	rehalfcld	⊢ ( 𝜑 → ( 𝑀 / 2 ) ∈ ℝ )
13	12	flcld	⊢ ( 𝜑 → ( ⌊ ‘ ( 𝑀 / 2 ) ) ∈ ℤ )
14	13	zred	⊢ ( 𝜑 → ( ⌊ ‘ ( 𝑀 / 2 ) ) ∈ ℝ )
15	14	ltp1d	⊢ ( 𝜑 → ( ⌊ ‘ ( 𝑀 / 2 ) ) < ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) )
16		fzdisj	⊢ ( ( ⌊ ‘ ( 𝑀 / 2 ) ) < ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) → ( ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ∩ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) = ∅ )
17	15 16	syl	⊢ ( 𝜑 → ( ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ∩ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) = ∅ )
18	10	nnrpd	⊢ ( 𝜑 → 𝑀 ∈ ℝ+ )
19	18	rphalfcld	⊢ ( 𝜑 → ( 𝑀 / 2 ) ∈ ℝ+ )
20	19	rpge0d	⊢ ( 𝜑 → 0 ≤ ( 𝑀 / 2 ) )
21		flge0nn0	⊢ ( ( ( 𝑀 / 2 ) ∈ ℝ ∧ 0 ≤ ( 𝑀 / 2 ) ) → ( ⌊ ‘ ( 𝑀 / 2 ) ) ∈ ℕ0 )
22	12 20 21	syl2anc	⊢ ( 𝜑 → ( ⌊ ‘ ( 𝑀 / 2 ) ) ∈ ℕ0 )
23	10	nnnn0d	⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
24		rphalflt	⊢ ( 𝑀 ∈ ℝ+ → ( 𝑀 / 2 ) < 𝑀 )
25	18 24	syl	⊢ ( 𝜑 → ( 𝑀 / 2 ) < 𝑀 )
26	10	nnzd	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
27		fllt	⊢ ( ( ( 𝑀 / 2 ) ∈ ℝ ∧ 𝑀 ∈ ℤ ) → ( ( 𝑀 / 2 ) < 𝑀 ↔ ( ⌊ ‘ ( 𝑀 / 2 ) ) < 𝑀 ) )
28	12 26 27	syl2anc	⊢ ( 𝜑 → ( ( 𝑀 / 2 ) < 𝑀 ↔ ( ⌊ ‘ ( 𝑀 / 2 ) ) < 𝑀 ) )
29	25 28	mpbid	⊢ ( 𝜑 → ( ⌊ ‘ ( 𝑀 / 2 ) ) < 𝑀 )
30	14 11 29	ltled	⊢ ( 𝜑 → ( ⌊ ‘ ( 𝑀 / 2 ) ) ≤ 𝑀 )
31		elfz2nn0	⊢ ( ( ⌊ ‘ ( 𝑀 / 2 ) ) ∈ ( 0 ... 𝑀 ) ↔ ( ( ⌊ ‘ ( 𝑀 / 2 ) ) ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ ( ⌊ ‘ ( 𝑀 / 2 ) ) ≤ 𝑀 ) )
32	22 23 30 31	syl3anbrc	⊢ ( 𝜑 → ( ⌊ ‘ ( 𝑀 / 2 ) ) ∈ ( 0 ... 𝑀 ) )
33		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
34	23 33	eleqtrdi	⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 0 ) )
35		elfzp12	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 0 ) → ( ( ⌊ ‘ ( 𝑀 / 2 ) ) ∈ ( 0 ... 𝑀 ) ↔ ( ( ⌊ ‘ ( 𝑀 / 2 ) ) = 0 ∨ ( ⌊ ‘ ( 𝑀 / 2 ) ) ∈ ( ( 0 + 1 ) ... 𝑀 ) ) ) )
36	34 35	syl	⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝑀 / 2 ) ) ∈ ( 0 ... 𝑀 ) ↔ ( ( ⌊ ‘ ( 𝑀 / 2 ) ) = 0 ∨ ( ⌊ ‘ ( 𝑀 / 2 ) ) ∈ ( ( 0 + 1 ) ... 𝑀 ) ) ) )
37	32 36	mpbid	⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝑀 / 2 ) ) = 0 ∨ ( ⌊ ‘ ( 𝑀 / 2 ) ) ∈ ( ( 0 + 1 ) ... 𝑀 ) ) )
38		un0	⊢ ( ( 1 ... 𝑀 ) ∪ ∅ ) = ( 1 ... 𝑀 )
39		uncom	⊢ ( ( 1 ... 𝑀 ) ∪ ∅ ) = ( ∅ ∪ ( 1 ... 𝑀 ) )
40	38 39	eqtr3i	⊢ ( 1 ... 𝑀 ) = ( ∅ ∪ ( 1 ... 𝑀 ) )
41		oveq2	⊢ ( ( ⌊ ‘ ( 𝑀 / 2 ) ) = 0 → ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) = ( 1 ... 0 ) )
42		fz10	⊢ ( 1 ... 0 ) = ∅
43	41 42	eqtrdi	⊢ ( ( ⌊ ‘ ( 𝑀 / 2 ) ) = 0 → ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) = ∅ )
44		oveq1	⊢ ( ( ⌊ ‘ ( 𝑀 / 2 ) ) = 0 → ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) = ( 0 + 1 ) )
45		0p1e1	⊢ ( 0 + 1 ) = 1
46	44 45	eqtrdi	⊢ ( ( ⌊ ‘ ( 𝑀 / 2 ) ) = 0 → ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) = 1 )
47	46	oveq1d	⊢ ( ( ⌊ ‘ ( 𝑀 / 2 ) ) = 0 → ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) = ( 1 ... 𝑀 ) )
48	43 47	uneq12d	⊢ ( ( ⌊ ‘ ( 𝑀 / 2 ) ) = 0 → ( ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ∪ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) = ( ∅ ∪ ( 1 ... 𝑀 ) ) )
49	40 48	eqtr4id	⊢ ( ( ⌊ ‘ ( 𝑀 / 2 ) ) = 0 → ( 1 ... 𝑀 ) = ( ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ∪ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) )
50		fzsplit	⊢ ( ( ⌊ ‘ ( 𝑀 / 2 ) ) ∈ ( 1 ... 𝑀 ) → ( 1 ... 𝑀 ) = ( ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ∪ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) )
51	45	oveq1i	⊢ ( ( 0 + 1 ) ... 𝑀 ) = ( 1 ... 𝑀 )
52	50 51	eleq2s	⊢ ( ( ⌊ ‘ ( 𝑀 / 2 ) ) ∈ ( ( 0 + 1 ) ... 𝑀 ) → ( 1 ... 𝑀 ) = ( ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ∪ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) )
53	49 52	jaoi	⊢ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) = 0 ∨ ( ⌊ ‘ ( 𝑀 / 2 ) ) ∈ ( ( 0 + 1 ) ... 𝑀 ) ) → ( 1 ... 𝑀 ) = ( ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ∪ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) )
54	37 53	syl	⊢ ( 𝜑 → ( 1 ... 𝑀 ) = ( ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ∪ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) )
55		fzfid	⊢ ( 𝜑 → ( 1 ... 𝑀 ) ∈ Fin )
56	2	gausslemma2dlem0a	⊢ ( 𝜑 → 𝑄 ∈ ℕ )
57	56	nnred	⊢ ( 𝜑 → 𝑄 ∈ ℝ )
58	1	gausslemma2dlem0a	⊢ ( 𝜑 → 𝑃 ∈ ℕ )
59	57 58	nndivred	⊢ ( 𝜑 → ( 𝑄 / 𝑃 ) ∈ ℝ )
60	59	adantr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... 𝑀 ) ) → ( 𝑄 / 𝑃 ) ∈ ℝ )
61		2nn	⊢ 2 ∈ ℕ
62		elfznn	⊢ ( 𝑢 ∈ ( 1 ... 𝑀 ) → 𝑢 ∈ ℕ )
63	62	adantl	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... 𝑀 ) ) → 𝑢 ∈ ℕ )
64		nnmulcl	⊢ ( ( 2 ∈ ℕ ∧ 𝑢 ∈ ℕ ) → ( 2 · 𝑢 ) ∈ ℕ )
65	61 63 64	sylancr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... 𝑀 ) ) → ( 2 · 𝑢 ) ∈ ℕ )
66	65	nnred	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... 𝑀 ) ) → ( 2 · 𝑢 ) ∈ ℝ )
67	60 66	remulcld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ∈ ℝ )
68	56	nnrpd	⊢ ( 𝜑 → 𝑄 ∈ ℝ+ )
69	58	nnrpd	⊢ ( 𝜑 → 𝑃 ∈ ℝ+ )
70	68 69	rpdivcld	⊢ ( 𝜑 → ( 𝑄 / 𝑃 ) ∈ ℝ+ )
71	70	adantr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... 𝑀 ) ) → ( 𝑄 / 𝑃 ) ∈ ℝ+ )
72	65	nnrpd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... 𝑀 ) ) → ( 2 · 𝑢 ) ∈ ℝ+ )
73	71 72	rpmulcld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ∈ ℝ+ )
74	73	rpge0d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... 𝑀 ) ) → 0 ≤ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) )
75		flge0nn0	⊢ ( ( ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ∈ ℝ ∧ 0 ≤ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) → ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ∈ ℕ0 )
76	67 74 75	syl2anc	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... 𝑀 ) ) → ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ∈ ℕ0 )
77	76	nn0cnd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... 𝑀 ) ) → ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ∈ ℂ )
78	17 54 55 77	fsumsplit	⊢ ( 𝜑 → Σ 𝑢 ∈ ( 1 ... 𝑀 ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) = ( Σ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) + Σ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) )
79	9 78	eqtr3id	⊢ ( 𝜑 → Σ 𝑢 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) = ( Σ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) + Σ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) )
80	79	oveq2d	⊢ ( 𝜑 → ( - 1 ↑ Σ 𝑢 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) = ( - 1 ↑ ( Σ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) + Σ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) )
81		neg1cn	⊢ - 1 ∈ ℂ
82	81	a1i	⊢ ( 𝜑 → - 1 ∈ ℂ )
83		fzfid	⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ∈ Fin )
84		ssun2	⊢ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ⊆ ( ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ∪ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) )
85	84 54	sseqtrrid	⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ⊆ ( 1 ... 𝑀 ) )
86	85	sselda	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → 𝑢 ∈ ( 1 ... 𝑀 ) )
87	86 76	syldan	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ∈ ℕ0 )
88	83 87	fsumnn0cl	⊢ ( 𝜑 → Σ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ∈ ℕ0 )
89		fzfid	⊢ ( 𝜑 → ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ∈ Fin )
90		ssun1	⊢ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ⊆ ( ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ∪ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) )
91	90 54	sseqtrrid	⊢ ( 𝜑 → ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ⊆ ( 1 ... 𝑀 ) )
92	91	sselda	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) → 𝑢 ∈ ( 1 ... 𝑀 ) )
93	92 76	syldan	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) → ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ∈ ℕ0 )
94	89 93	fsumnn0cl	⊢ ( 𝜑 → Σ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ∈ ℕ0 )
95	82 88 94	expaddd	⊢ ( 𝜑 → ( - 1 ↑ ( Σ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) + Σ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) = ( ( - 1 ↑ Σ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) · ( - 1 ↑ Σ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) )
96		fzfid	⊢ ( 𝜑 → ( 1 ... 𝑁 ) ∈ Fin )
97		xpfi	⊢ ( ( ( 1 ... 𝑀 ) ∈ Fin ∧ ( 1 ... 𝑁 ) ∈ Fin ) → ( ( 1 ... 𝑀 ) × ( 1 ... 𝑁 ) ) ∈ Fin )
98	55 96 97	syl2anc	⊢ ( 𝜑 → ( ( 1 ... 𝑀 ) × ( 1 ... 𝑁 ) ) ∈ Fin )
99		opabssxp	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 1 ... 𝑀 ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑦 · 𝑃 ) < ( 𝑥 · 𝑄 ) ) } ⊆ ( ( 1 ... 𝑀 ) × ( 1 ... 𝑁 ) )
100	6 99	eqsstri	⊢ 𝑆 ⊆ ( ( 1 ... 𝑀 ) × ( 1 ... 𝑁 ) )
101		ssfi	⊢ ( ( ( ( 1 ... 𝑀 ) × ( 1 ... 𝑁 ) ) ∈ Fin ∧ 𝑆 ⊆ ( ( 1 ... 𝑀 ) × ( 1 ... 𝑁 ) ) ) → 𝑆 ∈ Fin )
102	98 100 101	sylancl	⊢ ( 𝜑 → 𝑆 ∈ Fin )
103		ssrab2	⊢ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1st ‘ 𝑧 ) } ⊆ 𝑆
104		ssfi	⊢ ( ( 𝑆 ∈ Fin ∧ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1st ‘ 𝑧 ) } ⊆ 𝑆 ) → { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1st ‘ 𝑧 ) } ∈ Fin )
105	102 103 104	sylancl	⊢ ( 𝜑 → { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1st ‘ 𝑧 ) } ∈ Fin )
106		hashcl	⊢ ( { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1st ‘ 𝑧 ) } ∈ Fin → ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1st ‘ 𝑧 ) } ) ∈ ℕ0 )
107	105 106	syl	⊢ ( 𝜑 → ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1st ‘ 𝑧 ) } ) ∈ ℕ0 )
108		ssrab2	⊢ { 𝑧 ∈ 𝑆 ∣ 2 ∥ ( 1st ‘ 𝑧 ) } ⊆ 𝑆
109		ssfi	⊢ ( ( 𝑆 ∈ Fin ∧ { 𝑧 ∈ 𝑆 ∣ 2 ∥ ( 1st ‘ 𝑧 ) } ⊆ 𝑆 ) → { 𝑧 ∈ 𝑆 ∣ 2 ∥ ( 1st ‘ 𝑧 ) } ∈ Fin )
110	102 108 109	sylancl	⊢ ( 𝜑 → { 𝑧 ∈ 𝑆 ∣ 2 ∥ ( 1st ‘ 𝑧 ) } ∈ Fin )
111		hashcl	⊢ ( { 𝑧 ∈ 𝑆 ∣ 2 ∥ ( 1st ‘ 𝑧 ) } ∈ Fin → ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ 2 ∥ ( 1st ‘ 𝑧 ) } ) ∈ ℕ0 )
112	110 111	syl	⊢ ( 𝜑 → ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ 2 ∥ ( 1st ‘ 𝑧 ) } ) ∈ ℕ0 )
113	82 107 112	expaddd	⊢ ( 𝜑 → ( - 1 ↑ ( ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ 2 ∥ ( 1st ‘ 𝑧 ) } ) + ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1st ‘ 𝑧 ) } ) ) ) = ( ( - 1 ↑ ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ 2 ∥ ( 1st ‘ 𝑧 ) } ) ) · ( - 1 ↑ ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1st ‘ 𝑧 ) } ) ) ) )
114	92 65	syldan	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) → ( 2 · 𝑢 ) ∈ ℕ )
115		fzfid	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) → ( 1 ... ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ∈ Fin )
116		xpsnen2g	⊢ ( ( ( 2 · 𝑢 ) ∈ ℕ ∧ ( 1 ... ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ∈ Fin ) → ( { ( 2 · 𝑢 ) } × ( 1 ... ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) ≈ ( 1 ... ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) )
117	114 115 116	syl2anc	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) → ( { ( 2 · 𝑢 ) } × ( 1 ... ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) ≈ ( 1 ... ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) )
118		hasheni	⊢ ( ( { ( 2 · 𝑢 ) } × ( 1 ... ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) ≈ ( 1 ... ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) → ( ♯ ‘ ( { ( 2 · 𝑢 ) } × ( 1 ... ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) ) = ( ♯ ‘ ( 1 ... ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) )
119	117 118	syl	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) → ( ♯ ‘ ( { ( 2 · 𝑢 ) } × ( 1 ... ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) ) = ( ♯ ‘ ( 1 ... ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) )
120		ssrab2	⊢ { 𝑧 ∈ 𝑆 ∣ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) } ⊆ 𝑆
121	6	relopabiv	⊢ Rel 𝑆
122		relss	⊢ ( { 𝑧 ∈ 𝑆 ∣ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) } ⊆ 𝑆 → ( Rel 𝑆 → Rel { 𝑧 ∈ 𝑆 ∣ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) } ) )
123	120 121 122	mp2	⊢ Rel { 𝑧 ∈ 𝑆 ∣ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) }
124		relxp	⊢ Rel ( { ( 2 · 𝑢 ) } × ( 1 ... ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) )
125	6	eleq2i	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑆 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 1 ... 𝑀 ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑦 · 𝑃 ) < ( 𝑥 · 𝑄 ) ) } )
126		opabidw	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 1 ... 𝑀 ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑦 · 𝑃 ) < ( 𝑥 · 𝑄 ) ) } ↔ ( ( 𝑥 ∈ ( 1 ... 𝑀 ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑦 · 𝑃 ) < ( 𝑥 · 𝑄 ) ) )
127	125 126	bitri	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑆 ↔ ( ( 𝑥 ∈ ( 1 ... 𝑀 ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑦 · 𝑃 ) < ( 𝑥 · 𝑄 ) ) )
128		anass	⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁 ) ∧ ( 𝑦 · 𝑃 ) < ( 𝑄 · ( 2 · 𝑢 ) ) ) ↔ ( 𝑦 ∈ ℕ ∧ ( 𝑦 ≤ 𝑁 ∧ ( 𝑦 · 𝑃 ) < ( 𝑄 · ( 2 · 𝑢 ) ) ) ) )
129	114	adantr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( 2 · 𝑢 ) ∈ ℕ )
130	129	nnred	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( 2 · 𝑢 ) ∈ ℝ )
131	58	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → 𝑃 ∈ ℕ )
132	131	nnred	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → 𝑃 ∈ ℝ )
133	132	rehalfcld	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( 𝑃 / 2 ) ∈ ℝ )
134	11	adantr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) → 𝑀 ∈ ℝ )
135	134	adantr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → 𝑀 ∈ ℝ )
136		elfzle2	⊢ ( 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) → 𝑢 ≤ ( ⌊ ‘ ( 𝑀 / 2 ) ) )
137	136	adantl	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) → 𝑢 ≤ ( ⌊ ‘ ( 𝑀 / 2 ) ) )
138	134	rehalfcld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) → ( 𝑀 / 2 ) ∈ ℝ )
139		elfzelz	⊢ ( 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) → 𝑢 ∈ ℤ )
140	139	adantl	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) → 𝑢 ∈ ℤ )
141		flge	⊢ ( ( ( 𝑀 / 2 ) ∈ ℝ ∧ 𝑢 ∈ ℤ ) → ( 𝑢 ≤ ( 𝑀 / 2 ) ↔ 𝑢 ≤ ( ⌊ ‘ ( 𝑀 / 2 ) ) ) )
142	138 140 141	syl2anc	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) → ( 𝑢 ≤ ( 𝑀 / 2 ) ↔ 𝑢 ≤ ( ⌊ ‘ ( 𝑀 / 2 ) ) ) )
143	137 142	mpbird	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) → 𝑢 ≤ ( 𝑀 / 2 ) )
144		elfznn	⊢ ( 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) → 𝑢 ∈ ℕ )
145	144	adantl	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) → 𝑢 ∈ ℕ )
146	145	nnred	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) → 𝑢 ∈ ℝ )
147		2re	⊢ 2 ∈ ℝ
148	147	a1i	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) → 2 ∈ ℝ )
149		2pos	⊢ 0 < 2
150	149	a1i	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) → 0 < 2 )
151		lemuldiv2	⊢ ( ( 𝑢 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( 2 · 𝑢 ) ≤ 𝑀 ↔ 𝑢 ≤ ( 𝑀 / 2 ) ) )
152	146 134 148 150 151	syl112anc	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) → ( ( 2 · 𝑢 ) ≤ 𝑀 ↔ 𝑢 ≤ ( 𝑀 / 2 ) ) )
153	143 152	mpbird	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) → ( 2 · 𝑢 ) ≤ 𝑀 )
154	153	adantr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( 2 · 𝑢 ) ≤ 𝑀 )
155	132	ltm1d	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( 𝑃 − 1 ) < 𝑃 )
156		peano2rem	⊢ ( 𝑃 ∈ ℝ → ( 𝑃 − 1 ) ∈ ℝ )
157	132 156	syl	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( 𝑃 − 1 ) ∈ ℝ )
158	147	a1i	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → 2 ∈ ℝ )
159	149	a1i	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → 0 < 2 )
160		ltdiv1	⊢ ( ( ( 𝑃 − 1 ) ∈ ℝ ∧ 𝑃 ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( 𝑃 − 1 ) < 𝑃 ↔ ( ( 𝑃 − 1 ) / 2 ) < ( 𝑃 / 2 ) ) )
161	157 132 158 159 160	syl112anc	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( ( 𝑃 − 1 ) < 𝑃 ↔ ( ( 𝑃 − 1 ) / 2 ) < ( 𝑃 / 2 ) ) )
162	155 161	mpbid	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( ( 𝑃 − 1 ) / 2 ) < ( 𝑃 / 2 ) )
163	4 162	eqbrtrid	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → 𝑀 < ( 𝑃 / 2 ) )
164	130 135 133 154 163	lelttrd	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( 2 · 𝑢 ) < ( 𝑃 / 2 ) )
165	131	nnrpd	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → 𝑃 ∈ ℝ+ )
166		rphalflt	⊢ ( 𝑃 ∈ ℝ+ → ( 𝑃 / 2 ) < 𝑃 )
167	165 166	syl	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( 𝑃 / 2 ) < 𝑃 )
168	130 133 132 164 167	lttrd	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( 2 · 𝑢 ) < 𝑃 )
169	130 132	ltnled	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( ( 2 · 𝑢 ) < 𝑃 ↔ ¬ 𝑃 ≤ ( 2 · 𝑢 ) ) )
170	168 169	mpbid	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ¬ 𝑃 ≤ ( 2 · 𝑢 ) )
171	1	eldifad	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
172	171	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → 𝑃 ∈ ℙ )
173		prmz	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
174	172 173	syl	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → 𝑃 ∈ ℤ )
175		dvdsle	⊢ ( ( 𝑃 ∈ ℤ ∧ ( 2 · 𝑢 ) ∈ ℕ ) → ( 𝑃 ∥ ( 2 · 𝑢 ) → 𝑃 ≤ ( 2 · 𝑢 ) ) )
176	174 129 175	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( 𝑃 ∥ ( 2 · 𝑢 ) → 𝑃 ≤ ( 2 · 𝑢 ) ) )
177	170 176	mtod	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ¬ 𝑃 ∥ ( 2 · 𝑢 ) )
178	2	eldifad	⊢ ( 𝜑 → 𝑄 ∈ ℙ )
179		prmrp	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ) → ( ( 𝑃 gcd 𝑄 ) = 1 ↔ 𝑃 ≠ 𝑄 ) )
180	171 178 179	syl2anc	⊢ ( 𝜑 → ( ( 𝑃 gcd 𝑄 ) = 1 ↔ 𝑃 ≠ 𝑄 ) )
181	3 180	mpbird	⊢ ( 𝜑 → ( 𝑃 gcd 𝑄 ) = 1 )
182	181	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( 𝑃 gcd 𝑄 ) = 1 )
183	178	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → 𝑄 ∈ ℙ )
184		prmz	⊢ ( 𝑄 ∈ ℙ → 𝑄 ∈ ℤ )
185	183 184	syl	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → 𝑄 ∈ ℤ )
186	129	nnzd	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( 2 · 𝑢 ) ∈ ℤ )
187		coprmdvds	⊢ ( ( 𝑃 ∈ ℤ ∧ 𝑄 ∈ ℤ ∧ ( 2 · 𝑢 ) ∈ ℤ ) → ( ( 𝑃 ∥ ( 𝑄 · ( 2 · 𝑢 ) ) ∧ ( 𝑃 gcd 𝑄 ) = 1 ) → 𝑃 ∥ ( 2 · 𝑢 ) ) )
188	174 185 186 187	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( ( 𝑃 ∥ ( 𝑄 · ( 2 · 𝑢 ) ) ∧ ( 𝑃 gcd 𝑄 ) = 1 ) → 𝑃 ∥ ( 2 · 𝑢 ) ) )
189	182 188	mpan2d	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( 𝑃 ∥ ( 𝑄 · ( 2 · 𝑢 ) ) → 𝑃 ∥ ( 2 · 𝑢 ) ) )
190	177 189	mtod	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ¬ 𝑃 ∥ ( 𝑄 · ( 2 · 𝑢 ) ) )
191		nnz	⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℤ )
192	191	adantl	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → 𝑦 ∈ ℤ )
193		dvdsmul2	⊢ ( ( 𝑦 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → 𝑃 ∥ ( 𝑦 · 𝑃 ) )
194	192 174 193	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → 𝑃 ∥ ( 𝑦 · 𝑃 ) )
195		breq2	⊢ ( ( 𝑄 · ( 2 · 𝑢 ) ) = ( 𝑦 · 𝑃 ) → ( 𝑃 ∥ ( 𝑄 · ( 2 · 𝑢 ) ) ↔ 𝑃 ∥ ( 𝑦 · 𝑃 ) ) )
196	194 195	syl5ibrcom	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( ( 𝑄 · ( 2 · 𝑢 ) ) = ( 𝑦 · 𝑃 ) → 𝑃 ∥ ( 𝑄 · ( 2 · 𝑢 ) ) ) )
197	196	necon3bd	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( ¬ 𝑃 ∥ ( 𝑄 · ( 2 · 𝑢 ) ) → ( 𝑄 · ( 2 · 𝑢 ) ) ≠ ( 𝑦 · 𝑃 ) ) )
198	190 197	mpd	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( 𝑄 · ( 2 · 𝑢 ) ) ≠ ( 𝑦 · 𝑃 ) )
199		simpr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → 𝑦 ∈ ℕ )
200	199 131	nnmulcld	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( 𝑦 · 𝑃 ) ∈ ℕ )
201	200	nnred	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( 𝑦 · 𝑃 ) ∈ ℝ )
202	56	adantr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) → 𝑄 ∈ ℕ )
203	202 114	nnmulcld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) → ( 𝑄 · ( 2 · 𝑢 ) ) ∈ ℕ )
204	203	adantr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( 𝑄 · ( 2 · 𝑢 ) ) ∈ ℕ )
205	204	nnred	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( 𝑄 · ( 2 · 𝑢 ) ) ∈ ℝ )
206	201 205	ltlend	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( ( 𝑦 · 𝑃 ) < ( 𝑄 · ( 2 · 𝑢 ) ) ↔ ( ( 𝑦 · 𝑃 ) ≤ ( 𝑄 · ( 2 · 𝑢 ) ) ∧ ( 𝑄 · ( 2 · 𝑢 ) ) ≠ ( 𝑦 · 𝑃 ) ) ) )
207	198 206	mpbiran2d	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( ( 𝑦 · 𝑃 ) < ( 𝑄 · ( 2 · 𝑢 ) ) ↔ ( 𝑦 · 𝑃 ) ≤ ( 𝑄 · ( 2 · 𝑢 ) ) ) )
208		nnre	⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℝ )
209	208	adantl	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → 𝑦 ∈ ℝ )
210	131	nngt0d	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → 0 < 𝑃 )
211		lemuldiv	⊢ ( ( 𝑦 ∈ ℝ ∧ ( 𝑄 · ( 2 · 𝑢 ) ) ∈ ℝ ∧ ( 𝑃 ∈ ℝ ∧ 0 < 𝑃 ) ) → ( ( 𝑦 · 𝑃 ) ≤ ( 𝑄 · ( 2 · 𝑢 ) ) ↔ 𝑦 ≤ ( ( 𝑄 · ( 2 · 𝑢 ) ) / 𝑃 ) ) )
212	209 205 132 210 211	syl112anc	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( ( 𝑦 · 𝑃 ) ≤ ( 𝑄 · ( 2 · 𝑢 ) ) ↔ 𝑦 ≤ ( ( 𝑄 · ( 2 · 𝑢 ) ) / 𝑃 ) ) )
213	202	adantr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → 𝑄 ∈ ℕ )
214	213	nncnd	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → 𝑄 ∈ ℂ )
215	129	nncnd	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( 2 · 𝑢 ) ∈ ℂ )
216	131	nncnd	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → 𝑃 ∈ ℂ )
217	131	nnne0d	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → 𝑃 ≠ 0 )
218	214 215 216 217	div23d	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( ( 𝑄 · ( 2 · 𝑢 ) ) / 𝑃 ) = ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) )
219	218	breq2d	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( 𝑦 ≤ ( ( 𝑄 · ( 2 · 𝑢 ) ) / 𝑃 ) ↔ 𝑦 ≤ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) )
220	207 212 219	3bitrd	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( ( 𝑦 · 𝑃 ) < ( 𝑄 · ( 2 · 𝑢 ) ) ↔ 𝑦 ≤ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) )
221	213	nnred	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → 𝑄 ∈ ℝ )
222	213	nngt0d	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → 0 < 𝑄 )
223		ltmul2	⊢ ( ( ( 2 · 𝑢 ) ∈ ℝ ∧ ( 𝑃 / 2 ) ∈ ℝ ∧ ( 𝑄 ∈ ℝ ∧ 0 < 𝑄 ) ) → ( ( 2 · 𝑢 ) < ( 𝑃 / 2 ) ↔ ( 𝑄 · ( 2 · 𝑢 ) ) < ( 𝑄 · ( 𝑃 / 2 ) ) ) )
224	130 133 221 222 223	syl112anc	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( ( 2 · 𝑢 ) < ( 𝑃 / 2 ) ↔ ( 𝑄 · ( 2 · 𝑢 ) ) < ( 𝑄 · ( 𝑃 / 2 ) ) ) )
225	164 224	mpbid	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( 𝑄 · ( 2 · 𝑢 ) ) < ( 𝑄 · ( 𝑃 / 2 ) ) )
226		2cnd	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → 2 ∈ ℂ )
227		2ne0	⊢ 2 ≠ 0
228	227	a1i	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → 2 ≠ 0 )
229		divass	⊢ ( ( 𝑄 ∈ ℂ ∧ 𝑃 ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( 𝑄 · 𝑃 ) / 2 ) = ( 𝑄 · ( 𝑃 / 2 ) ) )
230		div23	⊢ ( ( 𝑄 ∈ ℂ ∧ 𝑃 ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( 𝑄 · 𝑃 ) / 2 ) = ( ( 𝑄 / 2 ) · 𝑃 ) )
231	229 230	eqtr3d	⊢ ( ( 𝑄 ∈ ℂ ∧ 𝑃 ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( 𝑄 · ( 𝑃 / 2 ) ) = ( ( 𝑄 / 2 ) · 𝑃 ) )
232	214 216 226 228 231	syl112anc	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( 𝑄 · ( 𝑃 / 2 ) ) = ( ( 𝑄 / 2 ) · 𝑃 ) )
233	225 232	breqtrd	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( 𝑄 · ( 2 · 𝑢 ) ) < ( ( 𝑄 / 2 ) · 𝑃 ) )
234	221	rehalfcld	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( 𝑄 / 2 ) ∈ ℝ )
235	234 132	remulcld	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( ( 𝑄 / 2 ) · 𝑃 ) ∈ ℝ )
236		lttr	⊢ ( ( ( 𝑦 · 𝑃 ) ∈ ℝ ∧ ( 𝑄 · ( 2 · 𝑢 ) ) ∈ ℝ ∧ ( ( 𝑄 / 2 ) · 𝑃 ) ∈ ℝ ) → ( ( ( 𝑦 · 𝑃 ) < ( 𝑄 · ( 2 · 𝑢 ) ) ∧ ( 𝑄 · ( 2 · 𝑢 ) ) < ( ( 𝑄 / 2 ) · 𝑃 ) ) → ( 𝑦 · 𝑃 ) < ( ( 𝑄 / 2 ) · 𝑃 ) ) )
237	201 205 235 236	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( ( ( 𝑦 · 𝑃 ) < ( 𝑄 · ( 2 · 𝑢 ) ) ∧ ( 𝑄 · ( 2 · 𝑢 ) ) < ( ( 𝑄 / 2 ) · 𝑃 ) ) → ( 𝑦 · 𝑃 ) < ( ( 𝑄 / 2 ) · 𝑃 ) ) )
238	233 237	mpan2d	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( ( 𝑦 · 𝑃 ) < ( 𝑄 · ( 2 · 𝑢 ) ) → ( 𝑦 · 𝑃 ) < ( ( 𝑄 / 2 ) · 𝑃 ) ) )
239		ltmul1	⊢ ( ( 𝑦 ∈ ℝ ∧ ( 𝑄 / 2 ) ∈ ℝ ∧ ( 𝑃 ∈ ℝ ∧ 0 < 𝑃 ) ) → ( 𝑦 < ( 𝑄 / 2 ) ↔ ( 𝑦 · 𝑃 ) < ( ( 𝑄 / 2 ) · 𝑃 ) ) )
240	209 234 132 210 239	syl112anc	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( 𝑦 < ( 𝑄 / 2 ) ↔ ( 𝑦 · 𝑃 ) < ( ( 𝑄 / 2 ) · 𝑃 ) ) )
241	238 240	sylibrd	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( ( 𝑦 · 𝑃 ) < ( 𝑄 · ( 2 · 𝑢 ) ) → 𝑦 < ( 𝑄 / 2 ) ) )
242		peano2rem	⊢ ( 𝑄 ∈ ℝ → ( 𝑄 − 1 ) ∈ ℝ )
243	221 242	syl	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( 𝑄 − 1 ) ∈ ℝ )
244	243	recnd	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( 𝑄 − 1 ) ∈ ℂ )
245	214 244 226 228	divsubdird	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( ( 𝑄 − ( 𝑄 − 1 ) ) / 2 ) = ( ( 𝑄 / 2 ) − ( ( 𝑄 − 1 ) / 2 ) ) )
246	5	oveq2i	⊢ ( ( 𝑄 / 2 ) − 𝑁 ) = ( ( 𝑄 / 2 ) − ( ( 𝑄 − 1 ) / 2 ) )
247	245 246	eqtr4di	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( ( 𝑄 − ( 𝑄 − 1 ) ) / 2 ) = ( ( 𝑄 / 2 ) − 𝑁 ) )
248		ax-1cn	⊢ 1 ∈ ℂ
249		nncan	⊢ ( ( 𝑄 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝑄 − ( 𝑄 − 1 ) ) = 1 )
250	214 248 249	sylancl	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( 𝑄 − ( 𝑄 − 1 ) ) = 1 )
251	250	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( ( 𝑄 − ( 𝑄 − 1 ) ) / 2 ) = ( 1 / 2 ) )
252		halflt1	⊢ ( 1 / 2 ) < 1
253	251 252	eqbrtrdi	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( ( 𝑄 − ( 𝑄 − 1 ) ) / 2 ) < 1 )
254	247 253	eqbrtrrd	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( ( 𝑄 / 2 ) − 𝑁 ) < 1 )
255	2 5	gausslemma2dlem0b	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
256	255	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → 𝑁 ∈ ℕ )
257	256	nnred	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → 𝑁 ∈ ℝ )
258		1red	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → 1 ∈ ℝ )
259	234 257 258	ltsubadd2d	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( ( ( 𝑄 / 2 ) − 𝑁 ) < 1 ↔ ( 𝑄 / 2 ) < ( 𝑁 + 1 ) ) )
260	254 259	mpbid	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( 𝑄 / 2 ) < ( 𝑁 + 1 ) )
261		peano2re	⊢ ( 𝑁 ∈ ℝ → ( 𝑁 + 1 ) ∈ ℝ )
262	257 261	syl	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( 𝑁 + 1 ) ∈ ℝ )
263		lttr	⊢ ( ( 𝑦 ∈ ℝ ∧ ( 𝑄 / 2 ) ∈ ℝ ∧ ( 𝑁 + 1 ) ∈ ℝ ) → ( ( 𝑦 < ( 𝑄 / 2 ) ∧ ( 𝑄 / 2 ) < ( 𝑁 + 1 ) ) → 𝑦 < ( 𝑁 + 1 ) ) )
264	209 234 262 263	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( ( 𝑦 < ( 𝑄 / 2 ) ∧ ( 𝑄 / 2 ) < ( 𝑁 + 1 ) ) → 𝑦 < ( 𝑁 + 1 ) ) )
265	260 264	mpan2d	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( 𝑦 < ( 𝑄 / 2 ) → 𝑦 < ( 𝑁 + 1 ) ) )
266	241 265	syld	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( ( 𝑦 · 𝑃 ) < ( 𝑄 · ( 2 · 𝑢 ) ) → 𝑦 < ( 𝑁 + 1 ) ) )
267		nnleltp1	⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑦 ≤ 𝑁 ↔ 𝑦 < ( 𝑁 + 1 ) ) )
268	199 256 267	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( 𝑦 ≤ 𝑁 ↔ 𝑦 < ( 𝑁 + 1 ) ) )
269	266 268	sylibrd	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( ( 𝑦 · 𝑃 ) < ( 𝑄 · ( 2 · 𝑢 ) ) → 𝑦 ≤ 𝑁 ) )
270	269	pm4.71rd	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( ( 𝑦 · 𝑃 ) < ( 𝑄 · ( 2 · 𝑢 ) ) ↔ ( 𝑦 ≤ 𝑁 ∧ ( 𝑦 · 𝑃 ) < ( 𝑄 · ( 2 · 𝑢 ) ) ) ) )
271	92 67	syldan	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) → ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ∈ ℝ )
272		flge	⊢ ( ( ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ∈ ℝ ∧ 𝑦 ∈ ℤ ) → ( 𝑦 ≤ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ↔ 𝑦 ≤ ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) )
273	271 191 272	syl2an	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( 𝑦 ≤ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ↔ 𝑦 ≤ ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) )
274	220 270 273	3bitr3d	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑦 ∈ ℕ ) → ( ( 𝑦 ≤ 𝑁 ∧ ( 𝑦 · 𝑃 ) < ( 𝑄 · ( 2 · 𝑢 ) ) ) ↔ 𝑦 ≤ ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) )
275	274	pm5.32da	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) → ( ( 𝑦 ∈ ℕ ∧ ( 𝑦 ≤ 𝑁 ∧ ( 𝑦 · 𝑃 ) < ( 𝑄 · ( 2 · 𝑢 ) ) ) ) ↔ ( 𝑦 ∈ ℕ ∧ 𝑦 ≤ ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) )
276	128 275	bitrid	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) → ( ( ( 𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁 ) ∧ ( 𝑦 · 𝑃 ) < ( 𝑄 · ( 2 · 𝑢 ) ) ) ↔ ( 𝑦 ∈ ℕ ∧ 𝑦 ≤ ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) )
277	276	adantr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑥 = ( 2 · 𝑢 ) ) → ( ( ( 𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁 ) ∧ ( 𝑦 · 𝑃 ) < ( 𝑄 · ( 2 · 𝑢 ) ) ) ↔ ( 𝑦 ∈ ℕ ∧ 𝑦 ≤ ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) )
278		simpr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑥 = ( 2 · 𝑢 ) ) → 𝑥 = ( 2 · 𝑢 ) )
279		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
280	114 279	eleqtrdi	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) → ( 2 · 𝑢 ) ∈ ( ℤ≥ ‘ 1 ) )
281	26	adantr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) → 𝑀 ∈ ℤ )
282		elfz5	⊢ ( ( ( 2 · 𝑢 ) ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑀 ∈ ℤ ) → ( ( 2 · 𝑢 ) ∈ ( 1 ... 𝑀 ) ↔ ( 2 · 𝑢 ) ≤ 𝑀 ) )
283	280 281 282	syl2anc	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) → ( ( 2 · 𝑢 ) ∈ ( 1 ... 𝑀 ) ↔ ( 2 · 𝑢 ) ≤ 𝑀 ) )
284	153 283	mpbird	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) → ( 2 · 𝑢 ) ∈ ( 1 ... 𝑀 ) )
285	284	adantr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑥 = ( 2 · 𝑢 ) ) → ( 2 · 𝑢 ) ∈ ( 1 ... 𝑀 ) )
286	278 285	eqeltrd	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑥 = ( 2 · 𝑢 ) ) → 𝑥 ∈ ( 1 ... 𝑀 ) )
287	286	biantrurd	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑥 = ( 2 · 𝑢 ) ) → ( 𝑦 ∈ ( 1 ... 𝑁 ) ↔ ( 𝑥 ∈ ( 1 ... 𝑀 ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) ) )
288	255	nnzd	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
289	288	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑥 = ( 2 · 𝑢 ) ) → 𝑁 ∈ ℤ )
290		fznn	⊢ ( 𝑁 ∈ ℤ → ( 𝑦 ∈ ( 1 ... 𝑁 ) ↔ ( 𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁 ) ) )
291	289 290	syl	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑥 = ( 2 · 𝑢 ) ) → ( 𝑦 ∈ ( 1 ... 𝑁 ) ↔ ( 𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁 ) ) )
292	287 291	bitr3d	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑥 = ( 2 · 𝑢 ) ) → ( ( 𝑥 ∈ ( 1 ... 𝑀 ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) ↔ ( 𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁 ) ) )
293		oveq1	⊢ ( 𝑥 = ( 2 · 𝑢 ) → ( 𝑥 · 𝑄 ) = ( ( 2 · 𝑢 ) · 𝑄 ) )
294	114	nncnd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) → ( 2 · 𝑢 ) ∈ ℂ )
295	202	nncnd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) → 𝑄 ∈ ℂ )
296	294 295	mulcomd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) → ( ( 2 · 𝑢 ) · 𝑄 ) = ( 𝑄 · ( 2 · 𝑢 ) ) )
297	293 296	sylan9eqr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑥 = ( 2 · 𝑢 ) ) → ( 𝑥 · 𝑄 ) = ( 𝑄 · ( 2 · 𝑢 ) ) )
298	297	breq2d	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑥 = ( 2 · 𝑢 ) ) → ( ( 𝑦 · 𝑃 ) < ( 𝑥 · 𝑄 ) ↔ ( 𝑦 · 𝑃 ) < ( 𝑄 · ( 2 · 𝑢 ) ) ) )
299	292 298	anbi12d	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑥 = ( 2 · 𝑢 ) ) → ( ( ( 𝑥 ∈ ( 1 ... 𝑀 ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑦 · 𝑃 ) < ( 𝑥 · 𝑄 ) ) ↔ ( ( 𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁 ) ∧ ( 𝑦 · 𝑃 ) < ( 𝑄 · ( 2 · 𝑢 ) ) ) ) )
300	271	flcld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) → ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ∈ ℤ )
301		fznn	⊢ ( ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ∈ ℤ → ( 𝑦 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ↔ ( 𝑦 ∈ ℕ ∧ 𝑦 ≤ ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) )
302	300 301	syl	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) → ( 𝑦 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ↔ ( 𝑦 ∈ ℕ ∧ 𝑦 ≤ ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) )
303	302	adantr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑥 = ( 2 · 𝑢 ) ) → ( 𝑦 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ↔ ( 𝑦 ∈ ℕ ∧ 𝑦 ≤ ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) )
304	277 299 303	3bitr4d	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑥 = ( 2 · 𝑢 ) ) → ( ( ( 𝑥 ∈ ( 1 ... 𝑀 ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑦 · 𝑃 ) < ( 𝑥 · 𝑄 ) ) ↔ 𝑦 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) )
305	127 304	bitrid	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) ∧ 𝑥 = ( 2 · 𝑢 ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑆 ↔ 𝑦 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) )
306	305	pm5.32da	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) → ( ( 𝑥 = ( 2 · 𝑢 ) ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑆 ) ↔ ( 𝑥 = ( 2 · 𝑢 ) ∧ 𝑦 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) ) )
307		vex	⊢ 𝑥 ∈ V
308		vex	⊢ 𝑦 ∈ V
309	307 308	op1std	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 1st ‘ 𝑧 ) = 𝑥 )
310	309	eqeq2d	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) ↔ ( 2 · 𝑢 ) = 𝑥 ) )
311		eqcom	⊢ ( ( 2 · 𝑢 ) = 𝑥 ↔ 𝑥 = ( 2 · 𝑢 ) )
312	310 311	bitrdi	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) ↔ 𝑥 = ( 2 · 𝑢 ) ) )
313	312	elrab	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { 𝑧 ∈ 𝑆 ∣ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) } ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑆 ∧ 𝑥 = ( 2 · 𝑢 ) ) )
314	313	biancomi	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { 𝑧 ∈ 𝑆 ∣ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) } ↔ ( 𝑥 = ( 2 · 𝑢 ) ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑆 ) )
315		opelxp	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( { ( 2 · 𝑢 ) } × ( 1 ... ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) ↔ ( 𝑥 ∈ { ( 2 · 𝑢 ) } ∧ 𝑦 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) )
316		velsn	⊢ ( 𝑥 ∈ { ( 2 · 𝑢 ) } ↔ 𝑥 = ( 2 · 𝑢 ) )
317	316	anbi1i	⊢ ( ( 𝑥 ∈ { ( 2 · 𝑢 ) } ∧ 𝑦 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) ↔ ( 𝑥 = ( 2 · 𝑢 ) ∧ 𝑦 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) )
318	315 317	bitri	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( { ( 2 · 𝑢 ) } × ( 1 ... ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) ↔ ( 𝑥 = ( 2 · 𝑢 ) ∧ 𝑦 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) )
319	306 314 318	3bitr4g	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { 𝑧 ∈ 𝑆 ∣ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) } ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( { ( 2 · 𝑢 ) } × ( 1 ... ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) ) )
320	123 124 319	eqrelrdv	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) → { 𝑧 ∈ 𝑆 ∣ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) } = ( { ( 2 · 𝑢 ) } × ( 1 ... ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) )
321	320	eqcomd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) → ( { ( 2 · 𝑢 ) } × ( 1 ... ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) = { 𝑧 ∈ 𝑆 ∣ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) } )
322	321	fveq2d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) → ( ♯ ‘ ( { ( 2 · 𝑢 ) } × ( 1 ... ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) ) = ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) } ) )
323		hashfz1	⊢ ( ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ∈ ℕ0 → ( ♯ ‘ ( 1 ... ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) = ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) )
324	93 323	syl	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) → ( ♯ ‘ ( 1 ... ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) = ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) )
325	119 322 324	3eqtr3rd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) → ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) = ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) } ) )
326	325	sumeq2dv	⊢ ( 𝜑 → Σ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) = Σ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) } ) )
327	102	adantr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) → 𝑆 ∈ Fin )
328		ssfi	⊢ ( ( 𝑆 ∈ Fin ∧ { 𝑧 ∈ 𝑆 ∣ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) } ⊆ 𝑆 ) → { 𝑧 ∈ 𝑆 ∣ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) } ∈ Fin )
329	327 120 328	sylancl	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) → { 𝑧 ∈ 𝑆 ∣ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) } ∈ Fin )
330		fveq2	⊢ ( 𝑧 = 𝑣 → ( 1st ‘ 𝑧 ) = ( 1st ‘ 𝑣 ) )
331	330	eqeq2d	⊢ ( 𝑧 = 𝑣 → ( ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) ↔ ( 2 · 𝑢 ) = ( 1st ‘ 𝑣 ) ) )
332	331	elrab	⊢ ( 𝑣 ∈ { 𝑧 ∈ 𝑆 ∣ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) } ↔ ( 𝑣 ∈ 𝑆 ∧ ( 2 · 𝑢 ) = ( 1st ‘ 𝑣 ) ) )
333	332	simprbi	⊢ ( 𝑣 ∈ { 𝑧 ∈ 𝑆 ∣ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) } → ( 2 · 𝑢 ) = ( 1st ‘ 𝑣 ) )
334	333	ad2antll	⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ∧ 𝑣 ∈ { 𝑧 ∈ 𝑆 ∣ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) } ) ) → ( 2 · 𝑢 ) = ( 1st ‘ 𝑣 ) )
335	334	oveq1d	⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ∧ 𝑣 ∈ { 𝑧 ∈ 𝑆 ∣ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) } ) ) → ( ( 2 · 𝑢 ) / 2 ) = ( ( 1st ‘ 𝑣 ) / 2 ) )
336	145	nncnd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ) → 𝑢 ∈ ℂ )
337	336	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ∧ 𝑣 ∈ { 𝑧 ∈ 𝑆 ∣ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) } ) ) → 𝑢 ∈ ℂ )
338		2cnd	⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ∧ 𝑣 ∈ { 𝑧 ∈ 𝑆 ∣ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) } ) ) → 2 ∈ ℂ )
339	227	a1i	⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ∧ 𝑣 ∈ { 𝑧 ∈ 𝑆 ∣ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) } ) ) → 2 ≠ 0 )
340	337 338 339	divcan3d	⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ∧ 𝑣 ∈ { 𝑧 ∈ 𝑆 ∣ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) } ) ) → ( ( 2 · 𝑢 ) / 2 ) = 𝑢 )
341	335 340	eqtr3d	⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ∧ 𝑣 ∈ { 𝑧 ∈ 𝑆 ∣ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) } ) ) → ( ( 1st ‘ 𝑣 ) / 2 ) = 𝑢 )
342	341	ralrimivva	⊢ ( 𝜑 → ∀ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ∀ 𝑣 ∈ { 𝑧 ∈ 𝑆 ∣ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) } ( ( 1st ‘ 𝑣 ) / 2 ) = 𝑢 )
343		invdisj	⊢ ( ∀ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ∀ 𝑣 ∈ { 𝑧 ∈ 𝑆 ∣ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) } ( ( 1st ‘ 𝑣 ) / 2 ) = 𝑢 → Disj 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) { 𝑧 ∈ 𝑆 ∣ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) } )
344	342 343	syl	⊢ ( 𝜑 → Disj 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) { 𝑧 ∈ 𝑆 ∣ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) } )
345	89 329 344	hashiun	⊢ ( 𝜑 → ( ♯ ‘ ∪ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) { 𝑧 ∈ 𝑆 ∣ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) } ) = Σ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) } ) )
346		iunrab	⊢ ∪ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) { 𝑧 ∈ 𝑆 ∣ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) } = { 𝑧 ∈ 𝑆 ∣ ∃ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) }
347		2cn	⊢ 2 ∈ ℂ
348		zcn	⊢ ( 𝑢 ∈ ℤ → 𝑢 ∈ ℂ )
349	348	adantl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑢 ∈ ℤ ) → 𝑢 ∈ ℂ )
350		mulcom	⊢ ( ( 2 ∈ ℂ ∧ 𝑢 ∈ ℂ ) → ( 2 · 𝑢 ) = ( 𝑢 · 2 ) )
351	347 349 350	sylancr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑢 ∈ ℤ ) → ( 2 · 𝑢 ) = ( 𝑢 · 2 ) )
352	351	eqeq1d	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑢 ∈ ℤ ) → ( ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) ↔ ( 𝑢 · 2 ) = ( 1st ‘ 𝑧 ) ) )
353	352	rexbidva	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → ( ∃ 𝑢 ∈ ℤ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) ↔ ∃ 𝑢 ∈ ℤ ( 𝑢 · 2 ) = ( 1st ‘ 𝑧 ) ) )
354	139	anim1i	⊢ ( ( 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ∧ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) ) → ( 𝑢 ∈ ℤ ∧ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) ) )
355	354	reximi2	⊢ ( ∃ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) → ∃ 𝑢 ∈ ℤ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) )
356		simprr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑢 ∈ ℤ ∧ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) ) ) → ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) )
357		simpr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → 𝑧 ∈ 𝑆 )
358	100 357	sselid	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → 𝑧 ∈ ( ( 1 ... 𝑀 ) × ( 1 ... 𝑁 ) ) )
359		xp1st	⊢ ( 𝑧 ∈ ( ( 1 ... 𝑀 ) × ( 1 ... 𝑁 ) ) → ( 1st ‘ 𝑧 ) ∈ ( 1 ... 𝑀 ) )
360	358 359	syl	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → ( 1st ‘ 𝑧 ) ∈ ( 1 ... 𝑀 ) )
361	360	adantr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑢 ∈ ℤ ∧ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) ) ) → ( 1st ‘ 𝑧 ) ∈ ( 1 ... 𝑀 ) )
362		elfzle2	⊢ ( ( 1st ‘ 𝑧 ) ∈ ( 1 ... 𝑀 ) → ( 1st ‘ 𝑧 ) ≤ 𝑀 )
363	361 362	syl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑢 ∈ ℤ ∧ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) ) ) → ( 1st ‘ 𝑧 ) ≤ 𝑀 )
364	356 363	eqbrtrd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑢 ∈ ℤ ∧ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) ) ) → ( 2 · 𝑢 ) ≤ 𝑀 )
365		zre	⊢ ( 𝑢 ∈ ℤ → 𝑢 ∈ ℝ )
366	365	ad2antrl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑢 ∈ ℤ ∧ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) ) ) → 𝑢 ∈ ℝ )
367	11	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑢 ∈ ℤ ∧ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) ) ) → 𝑀 ∈ ℝ )
368	147	a1i	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑢 ∈ ℤ ∧ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) ) ) → 2 ∈ ℝ )
369	149	a1i	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑢 ∈ ℤ ∧ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) ) ) → 0 < 2 )
370	366 367 368 369 151	syl112anc	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑢 ∈ ℤ ∧ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) ) ) → ( ( 2 · 𝑢 ) ≤ 𝑀 ↔ 𝑢 ≤ ( 𝑀 / 2 ) ) )
371	364 370	mpbid	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑢 ∈ ℤ ∧ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) ) ) → 𝑢 ≤ ( 𝑀 / 2 ) )
372	12	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑢 ∈ ℤ ∧ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) ) ) → ( 𝑀 / 2 ) ∈ ℝ )
373		simprl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑢 ∈ ℤ ∧ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) ) ) → 𝑢 ∈ ℤ )
374	372 373 141	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑢 ∈ ℤ ∧ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) ) ) → ( 𝑢 ≤ ( 𝑀 / 2 ) ↔ 𝑢 ≤ ( ⌊ ‘ ( 𝑀 / 2 ) ) ) )
375	371 374	mpbid	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑢 ∈ ℤ ∧ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) ) ) → 𝑢 ≤ ( ⌊ ‘ ( 𝑀 / 2 ) ) )
376		2t0e0	⊢ ( 2 · 0 ) = 0
377		elfznn	⊢ ( ( 1st ‘ 𝑧 ) ∈ ( 1 ... 𝑀 ) → ( 1st ‘ 𝑧 ) ∈ ℕ )
378	361 377	syl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑢 ∈ ℤ ∧ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) ) ) → ( 1st ‘ 𝑧 ) ∈ ℕ )
379	356 378	eqeltrd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑢 ∈ ℤ ∧ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) ) ) → ( 2 · 𝑢 ) ∈ ℕ )
380	379	nngt0d	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑢 ∈ ℤ ∧ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) ) ) → 0 < ( 2 · 𝑢 ) )
381	376 380	eqbrtrid	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑢 ∈ ℤ ∧ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) ) ) → ( 2 · 0 ) < ( 2 · 𝑢 ) )
382		0red	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑢 ∈ ℤ ∧ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) ) ) → 0 ∈ ℝ )
383		ltmul2	⊢ ( ( 0 ∈ ℝ ∧ 𝑢 ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( 0 < 𝑢 ↔ ( 2 · 0 ) < ( 2 · 𝑢 ) ) )
384	382 366 368 369 383	syl112anc	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑢 ∈ ℤ ∧ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) ) ) → ( 0 < 𝑢 ↔ ( 2 · 0 ) < ( 2 · 𝑢 ) ) )
385	381 384	mpbird	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑢 ∈ ℤ ∧ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) ) ) → 0 < 𝑢 )
386		elnnz	⊢ ( 𝑢 ∈ ℕ ↔ ( 𝑢 ∈ ℤ ∧ 0 < 𝑢 ) )
387	373 385 386	sylanbrc	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑢 ∈ ℤ ∧ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) ) ) → 𝑢 ∈ ℕ )
388	387 279	eleqtrdi	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑢 ∈ ℤ ∧ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) ) ) → 𝑢 ∈ ( ℤ≥ ‘ 1 ) )
389	13	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑢 ∈ ℤ ∧ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) ) ) → ( ⌊ ‘ ( 𝑀 / 2 ) ) ∈ ℤ )
390		elfz5	⊢ ( ( 𝑢 ∈ ( ℤ≥ ‘ 1 ) ∧ ( ⌊ ‘ ( 𝑀 / 2 ) ) ∈ ℤ ) → ( 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ↔ 𝑢 ≤ ( ⌊ ‘ ( 𝑀 / 2 ) ) ) )
391	388 389 390	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑢 ∈ ℤ ∧ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) ) ) → ( 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ↔ 𝑢 ≤ ( ⌊ ‘ ( 𝑀 / 2 ) ) ) )
392	375 391	mpbird	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑢 ∈ ℤ ∧ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) ) ) → 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) )
393	392 356	jca	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑢 ∈ ℤ ∧ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) ) ) → ( 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ∧ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) ) )
394	393	ex	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → ( ( 𝑢 ∈ ℤ ∧ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) ) → ( 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ∧ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) ) ) )
395	394	reximdv2	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → ( ∃ 𝑢 ∈ ℤ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) → ∃ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) ) )
396	355 395	impbid2	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → ( ∃ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) ↔ ∃ 𝑢 ∈ ℤ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) ) )
397		2z	⊢ 2 ∈ ℤ
398	360	elfzelzd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → ( 1st ‘ 𝑧 ) ∈ ℤ )
399		divides	⊢ ( ( 2 ∈ ℤ ∧ ( 1st ‘ 𝑧 ) ∈ ℤ ) → ( 2 ∥ ( 1st ‘ 𝑧 ) ↔ ∃ 𝑢 ∈ ℤ ( 𝑢 · 2 ) = ( 1st ‘ 𝑧 ) ) )
400	397 398 399	sylancr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → ( 2 ∥ ( 1st ‘ 𝑧 ) ↔ ∃ 𝑢 ∈ ℤ ( 𝑢 · 2 ) = ( 1st ‘ 𝑧 ) ) )
401	353 396 400	3bitr4d	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → ( ∃ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) ↔ 2 ∥ ( 1st ‘ 𝑧 ) ) )
402	401	rabbidva	⊢ ( 𝜑 → { 𝑧 ∈ 𝑆 ∣ ∃ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) } = { 𝑧 ∈ 𝑆 ∣ 2 ∥ ( 1st ‘ 𝑧 ) } )
403	346 402	eqtrid	⊢ ( 𝜑 → ∪ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) { 𝑧 ∈ 𝑆 ∣ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) } = { 𝑧 ∈ 𝑆 ∣ 2 ∥ ( 1st ‘ 𝑧 ) } )
404	403	fveq2d	⊢ ( 𝜑 → ( ♯ ‘ ∪ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) { 𝑧 ∈ 𝑆 ∣ ( 2 · 𝑢 ) = ( 1st ‘ 𝑧 ) } ) = ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ 2 ∥ ( 1st ‘ 𝑧 ) } ) )
405	326 345 404	3eqtr2d	⊢ ( 𝜑 → Σ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) = ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ 2 ∥ ( 1st ‘ 𝑧 ) } ) )
406	405	oveq2d	⊢ ( 𝜑 → ( - 1 ↑ Σ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) = ( - 1 ↑ ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ 2 ∥ ( 1st ‘ 𝑧 ) } ) ) )
407	1 2 3 4 5 6	lgsquadlem1	⊢ ( 𝜑 → ( - 1 ↑ Σ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) = ( - 1 ↑ ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1st ‘ 𝑧 ) } ) ) )
408	406 407	oveq12d	⊢ ( 𝜑 → ( ( - 1 ↑ Σ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) · ( - 1 ↑ Σ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) = ( ( - 1 ↑ ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ 2 ∥ ( 1st ‘ 𝑧 ) } ) ) · ( - 1 ↑ ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1st ‘ 𝑧 ) } ) ) ) )
409	113 408	eqtr4d	⊢ ( 𝜑 → ( - 1 ↑ ( ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ 2 ∥ ( 1st ‘ 𝑧 ) } ) + ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1st ‘ 𝑧 ) } ) ) ) = ( ( - 1 ↑ Σ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) · ( - 1 ↑ Σ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) )
410		inrab	⊢ ( { 𝑧 ∈ 𝑆 ∣ 2 ∥ ( 1st ‘ 𝑧 ) } ∩ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1st ‘ 𝑧 ) } ) = { 𝑧 ∈ 𝑆 ∣ ( 2 ∥ ( 1st ‘ 𝑧 ) ∧ ¬ 2 ∥ ( 1st ‘ 𝑧 ) ) }
411		pm3.24	⊢ ¬ ( 2 ∥ ( 1st ‘ 𝑧 ) ∧ ¬ 2 ∥ ( 1st ‘ 𝑧 ) )
412	411	a1i	⊢ ( 𝜑 → ¬ ( 2 ∥ ( 1st ‘ 𝑧 ) ∧ ¬ 2 ∥ ( 1st ‘ 𝑧 ) ) )
413	412	ralrimivw	⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑆 ¬ ( 2 ∥ ( 1st ‘ 𝑧 ) ∧ ¬ 2 ∥ ( 1st ‘ 𝑧 ) ) )
414		rabeq0	⊢ ( { 𝑧 ∈ 𝑆 ∣ ( 2 ∥ ( 1st ‘ 𝑧 ) ∧ ¬ 2 ∥ ( 1st ‘ 𝑧 ) ) } = ∅ ↔ ∀ 𝑧 ∈ 𝑆 ¬ ( 2 ∥ ( 1st ‘ 𝑧 ) ∧ ¬ 2 ∥ ( 1st ‘ 𝑧 ) ) )
415	413 414	sylibr	⊢ ( 𝜑 → { 𝑧 ∈ 𝑆 ∣ ( 2 ∥ ( 1st ‘ 𝑧 ) ∧ ¬ 2 ∥ ( 1st ‘ 𝑧 ) ) } = ∅ )
416	410 415	eqtrid	⊢ ( 𝜑 → ( { 𝑧 ∈ 𝑆 ∣ 2 ∥ ( 1st ‘ 𝑧 ) } ∩ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1st ‘ 𝑧 ) } ) = ∅ )
417		hashun	⊢ ( ( { 𝑧 ∈ 𝑆 ∣ 2 ∥ ( 1st ‘ 𝑧 ) } ∈ Fin ∧ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1st ‘ 𝑧 ) } ∈ Fin ∧ ( { 𝑧 ∈ 𝑆 ∣ 2 ∥ ( 1st ‘ 𝑧 ) } ∩ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1st ‘ 𝑧 ) } ) = ∅ ) → ( ♯ ‘ ( { 𝑧 ∈ 𝑆 ∣ 2 ∥ ( 1st ‘ 𝑧 ) } ∪ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1st ‘ 𝑧 ) } ) ) = ( ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ 2 ∥ ( 1st ‘ 𝑧 ) } ) + ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1st ‘ 𝑧 ) } ) ) )
418	110 105 416 417	syl3anc	⊢ ( 𝜑 → ( ♯ ‘ ( { 𝑧 ∈ 𝑆 ∣ 2 ∥ ( 1st ‘ 𝑧 ) } ∪ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1st ‘ 𝑧 ) } ) ) = ( ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ 2 ∥ ( 1st ‘ 𝑧 ) } ) + ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1st ‘ 𝑧 ) } ) ) )
419		unrab	⊢ ( { 𝑧 ∈ 𝑆 ∣ 2 ∥ ( 1st ‘ 𝑧 ) } ∪ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1st ‘ 𝑧 ) } ) = { 𝑧 ∈ 𝑆 ∣ ( 2 ∥ ( 1st ‘ 𝑧 ) ∨ ¬ 2 ∥ ( 1st ‘ 𝑧 ) ) }
420		exmid	⊢ ( 2 ∥ ( 1st ‘ 𝑧 ) ∨ ¬ 2 ∥ ( 1st ‘ 𝑧 ) )
421	420	rgenw	⊢ ∀ 𝑧 ∈ 𝑆 ( 2 ∥ ( 1st ‘ 𝑧 ) ∨ ¬ 2 ∥ ( 1st ‘ 𝑧 ) )
422		rabid2	⊢ ( 𝑆 = { 𝑧 ∈ 𝑆 ∣ ( 2 ∥ ( 1st ‘ 𝑧 ) ∨ ¬ 2 ∥ ( 1st ‘ 𝑧 ) ) } ↔ ∀ 𝑧 ∈ 𝑆 ( 2 ∥ ( 1st ‘ 𝑧 ) ∨ ¬ 2 ∥ ( 1st ‘ 𝑧 ) ) )
423	421 422	mpbir	⊢ 𝑆 = { 𝑧 ∈ 𝑆 ∣ ( 2 ∥ ( 1st ‘ 𝑧 ) ∨ ¬ 2 ∥ ( 1st ‘ 𝑧 ) ) }
424	419 423	eqtr4i	⊢ ( { 𝑧 ∈ 𝑆 ∣ 2 ∥ ( 1st ‘ 𝑧 ) } ∪ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1st ‘ 𝑧 ) } ) = 𝑆
425	424	fveq2i	⊢ ( ♯ ‘ ( { 𝑧 ∈ 𝑆 ∣ 2 ∥ ( 1st ‘ 𝑧 ) } ∪ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1st ‘ 𝑧 ) } ) ) = ( ♯ ‘ 𝑆 )
426	418 425	eqtr3di	⊢ ( 𝜑 → ( ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ 2 ∥ ( 1st ‘ 𝑧 ) } ) + ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1st ‘ 𝑧 ) } ) ) = ( ♯ ‘ 𝑆 ) )
427	426	oveq2d	⊢ ( 𝜑 → ( - 1 ↑ ( ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ 2 ∥ ( 1st ‘ 𝑧 ) } ) + ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1st ‘ 𝑧 ) } ) ) ) = ( - 1 ↑ ( ♯ ‘ 𝑆 ) ) )
428	95 409 427	3eqtr2d	⊢ ( 𝜑 → ( - 1 ↑ ( Σ 𝑢 ∈ ( 1 ... ( ⌊ ‘ ( 𝑀 / 2 ) ) ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) + Σ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) = ( - 1 ↑ ( ♯ ‘ 𝑆 ) ) )
429	7 80 428	3eqtrd	⊢ ( 𝜑 → ( 𝑄 /L 𝑃 ) = ( - 1 ↑ ( ♯ ‘ 𝑆 ) ) )