Metamath Proof Explorer

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 ↑ ( ♯ ‘ 𝑆 ) ) )