lgsquadlem1

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

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		neg1cn	⊢ - 1 ∈ ℂ
8	7	a1i	⊢ ( 𝜑 → - 1 ∈ ℂ )
9		neg1ne0	⊢ - 1 ≠ 0
10	9	a1i	⊢ ( 𝜑 → - 1 ≠ 0 )
11		fzfid	⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ∈ Fin )
12	2	gausslemma2dlem0a	⊢ ( 𝜑 → 𝑄 ∈ ℕ )
13	12	nnred	⊢ ( 𝜑 → 𝑄 ∈ ℝ )
14	1	gausslemma2dlem0a	⊢ ( 𝜑 → 𝑃 ∈ ℕ )
15	13 14	nndivred	⊢ ( 𝜑 → ( 𝑄 / 𝑃 ) ∈ ℝ )
16	15	adantr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( 𝑄 / 𝑃 ) ∈ ℝ )
17		2z	⊢ 2 ∈ ℤ
18		elfzelz	⊢ ( 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) → 𝑢 ∈ ℤ )
19	18	adantl	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → 𝑢 ∈ ℤ )
20		zmulcl	⊢ ( ( 2 ∈ ℤ ∧ 𝑢 ∈ ℤ ) → ( 2 · 𝑢 ) ∈ ℤ )
21	17 19 20	sylancr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( 2 · 𝑢 ) ∈ ℤ )
22	21	zred	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( 2 · 𝑢 ) ∈ ℝ )
23	16 22	remulcld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ∈ ℝ )
24	23	flcld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ∈ ℤ )
25	11 24	fsumzcl	⊢ ( 𝜑 → Σ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ∈ ℤ )
26	8 10 25	expclzd	⊢ ( 𝜑 → ( - 1 ↑ Σ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ∈ ℂ )
27		fzfid	⊢ ( 𝜑 → ( 1 ... 𝑀 ) ∈ Fin )
28		fzfid	⊢ ( 𝜑 → ( 1 ... 𝑁 ) ∈ Fin )
29		xpfi	⊢ ( ( ( 1 ... 𝑀 ) ∈ Fin ∧ ( 1 ... 𝑁 ) ∈ Fin ) → ( ( 1 ... 𝑀 ) × ( 1 ... 𝑁 ) ) ∈ Fin )
30	27 28 29	syl2anc	⊢ ( 𝜑 → ( ( 1 ... 𝑀 ) × ( 1 ... 𝑁 ) ) ∈ Fin )
31		opabssxp	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 1 ... 𝑀 ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑦 · 𝑃 ) < ( 𝑥 · 𝑄 ) ) } ⊆ ( ( 1 ... 𝑀 ) × ( 1 ... 𝑁 ) )
32	6 31	eqsstri	⊢ 𝑆 ⊆ ( ( 1 ... 𝑀 ) × ( 1 ... 𝑁 ) )
33		ssfi	⊢ ( ( ( ( 1 ... 𝑀 ) × ( 1 ... 𝑁 ) ) ∈ Fin ∧ 𝑆 ⊆ ( ( 1 ... 𝑀 ) × ( 1 ... 𝑁 ) ) ) → 𝑆 ∈ Fin )
34	30 32 33	sylancl	⊢ ( 𝜑 → 𝑆 ∈ Fin )
35		ssrab2	⊢ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1^st ‘ 𝑧 ) } ⊆ 𝑆
36		ssfi	⊢ ( ( 𝑆 ∈ Fin ∧ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1^st ‘ 𝑧 ) } ⊆ 𝑆 ) → { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1^st ‘ 𝑧 ) } ∈ Fin )
37	34 35 36	sylancl	⊢ ( 𝜑 → { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1^st ‘ 𝑧 ) } ∈ Fin )
38		hashcl	⊢ ( { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1^st ‘ 𝑧 ) } ∈ Fin → ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1^st ‘ 𝑧 ) } ) ∈ ℕ₀ )
39	37 38	syl	⊢ ( 𝜑 → ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1^st ‘ 𝑧 ) } ) ∈ ℕ₀ )
40		expcl	⊢ ( ( - 1 ∈ ℂ ∧ ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1^st ‘ 𝑧 ) } ) ∈ ℕ₀ ) → ( - 1 ↑ ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1^st ‘ 𝑧 ) } ) ) ∈ ℂ )
41	7 39 40	sylancr	⊢ ( 𝜑 → ( - 1 ↑ ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1^st ‘ 𝑧 ) } ) ) ∈ ℂ )
42	39	nn0zd	⊢ ( 𝜑 → ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1^st ‘ 𝑧 ) } ) ∈ ℤ )
43	8 10 42	expne0d	⊢ ( 𝜑 → ( - 1 ↑ ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1^st ‘ 𝑧 ) } ) ) ≠ 0 )
44	41 43	recidd	⊢ ( 𝜑 → ( ( - 1 ↑ ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1^st ‘ 𝑧 ) } ) ) · ( 1 / ( - 1 ↑ ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1^st ‘ 𝑧 ) } ) ) ) ) = 1 )
45		1div1e1	⊢ ( 1 / 1 ) = 1
46	45	negeqi	⊢ - ( 1 / 1 ) = - 1
47		ax-1cn	⊢ 1 ∈ ℂ
48		ax-1ne0	⊢ 1 ≠ 0
49		divneg2	⊢ ( ( 1 ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ≠ 0 ) → - ( 1 / 1 ) = ( 1 / - 1 ) )
50	47 47 48 49	mp3an	⊢ - ( 1 / 1 ) = ( 1 / - 1 )
51	46 50	eqtr3i	⊢ - 1 = ( 1 / - 1 )
52	51	oveq1i	⊢ ( - 1 ↑ ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1^st ‘ 𝑧 ) } ) ) = ( ( 1 / - 1 ) ↑ ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1^st ‘ 𝑧 ) } ) )
53	8 10 42	exprecd	⊢ ( 𝜑 → ( ( 1 / - 1 ) ↑ ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1^st ‘ 𝑧 ) } ) ) = ( 1 / ( - 1 ↑ ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1^st ‘ 𝑧 ) } ) ) ) )
54	52 53	eqtrid	⊢ ( 𝜑 → ( - 1 ↑ ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1^st ‘ 𝑧 ) } ) ) = ( 1 / ( - 1 ↑ ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1^st ‘ 𝑧 ) } ) ) ) )
55	54	oveq2d	⊢ ( 𝜑 → ( ( - 1 ↑ ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1^st ‘ 𝑧 ) } ) ) · ( - 1 ↑ ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1^st ‘ 𝑧 ) } ) ) ) = ( ( - 1 ↑ ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1^st ‘ 𝑧 ) } ) ) · ( 1 / ( - 1 ↑ ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1^st ‘ 𝑧 ) } ) ) ) ) )
56	34	adantr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → 𝑆 ∈ Fin )
57		ssrab2	⊢ { 𝑧 ∈ 𝑆 ∣ ( 1^st ‘ 𝑧 ) = ( 𝑃 − ( 2 · 𝑢 ) ) } ⊆ 𝑆
58		ssfi	⊢ ( ( 𝑆 ∈ Fin ∧ { 𝑧 ∈ 𝑆 ∣ ( 1^st ‘ 𝑧 ) = ( 𝑃 − ( 2 · 𝑢 ) ) } ⊆ 𝑆 ) → { 𝑧 ∈ 𝑆 ∣ ( 1^st ‘ 𝑧 ) = ( 𝑃 − ( 2 · 𝑢 ) ) } ∈ Fin )
59	56 57 58	sylancl	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → { 𝑧 ∈ 𝑆 ∣ ( 1^st ‘ 𝑧 ) = ( 𝑃 − ( 2 · 𝑢 ) ) } ∈ Fin )
60		fveqeq2	⊢ ( 𝑧 = 𝑣 → ( ( 1^st ‘ 𝑧 ) = ( 𝑃 − ( 2 · 𝑢 ) ) ↔ ( 1^st ‘ 𝑣 ) = ( 𝑃 − ( 2 · 𝑢 ) ) ) )
61	60	elrab	⊢ ( 𝑣 ∈ { 𝑧 ∈ 𝑆 ∣ ( 1^st ‘ 𝑧 ) = ( 𝑃 − ( 2 · 𝑢 ) ) } ↔ ( 𝑣 ∈ 𝑆 ∧ ( 1^st ‘ 𝑣 ) = ( 𝑃 − ( 2 · 𝑢 ) ) ) )
62	61	simprbi	⊢ ( 𝑣 ∈ { 𝑧 ∈ 𝑆 ∣ ( 1^st ‘ 𝑧 ) = ( 𝑃 − ( 2 · 𝑢 ) ) } → ( 1^st ‘ 𝑣 ) = ( 𝑃 − ( 2 · 𝑢 ) ) )
63	62	ad2antll	⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ∧ 𝑣 ∈ { 𝑧 ∈ 𝑆 ∣ ( 1^st ‘ 𝑧 ) = ( 𝑃 − ( 2 · 𝑢 ) ) } ) ) → ( 1^st ‘ 𝑣 ) = ( 𝑃 − ( 2 · 𝑢 ) ) )
64	63	oveq2d	⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ∧ 𝑣 ∈ { 𝑧 ∈ 𝑆 ∣ ( 1^st ‘ 𝑧 ) = ( 𝑃 − ( 2 · 𝑢 ) ) } ) ) → ( 𝑃 − ( 1^st ‘ 𝑣 ) ) = ( 𝑃 − ( 𝑃 − ( 2 · 𝑢 ) ) ) )
65	14	adantr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → 𝑃 ∈ ℕ )
66	65	nncnd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → 𝑃 ∈ ℂ )
67	66	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ∧ 𝑣 ∈ { 𝑧 ∈ 𝑆 ∣ ( 1^st ‘ 𝑧 ) = ( 𝑃 − ( 2 · 𝑢 ) ) } ) ) → 𝑃 ∈ ℂ )
68	21	zcnd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( 2 · 𝑢 ) ∈ ℂ )
69	68	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ∧ 𝑣 ∈ { 𝑧 ∈ 𝑆 ∣ ( 1^st ‘ 𝑧 ) = ( 𝑃 − ( 2 · 𝑢 ) ) } ) ) → ( 2 · 𝑢 ) ∈ ℂ )
70	67 69	nncand	⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ∧ 𝑣 ∈ { 𝑧 ∈ 𝑆 ∣ ( 1^st ‘ 𝑧 ) = ( 𝑃 − ( 2 · 𝑢 ) ) } ) ) → ( 𝑃 − ( 𝑃 − ( 2 · 𝑢 ) ) ) = ( 2 · 𝑢 ) )
71	64 70	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ∧ 𝑣 ∈ { 𝑧 ∈ 𝑆 ∣ ( 1^st ‘ 𝑧 ) = ( 𝑃 − ( 2 · 𝑢 ) ) } ) ) → ( 𝑃 − ( 1^st ‘ 𝑣 ) ) = ( 2 · 𝑢 ) )
72	71	oveq1d	⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ∧ 𝑣 ∈ { 𝑧 ∈ 𝑆 ∣ ( 1^st ‘ 𝑧 ) = ( 𝑃 − ( 2 · 𝑢 ) ) } ) ) → ( ( 𝑃 − ( 1^st ‘ 𝑣 ) ) / 2 ) = ( ( 2 · 𝑢 ) / 2 ) )
73	19	zcnd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → 𝑢 ∈ ℂ )
74	73	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ∧ 𝑣 ∈ { 𝑧 ∈ 𝑆 ∣ ( 1^st ‘ 𝑧 ) = ( 𝑃 − ( 2 · 𝑢 ) ) } ) ) → 𝑢 ∈ ℂ )
75		2cnd	⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ∧ 𝑣 ∈ { 𝑧 ∈ 𝑆 ∣ ( 1^st ‘ 𝑧 ) = ( 𝑃 − ( 2 · 𝑢 ) ) } ) ) → 2 ∈ ℂ )
76		2ne0	⊢ 2 ≠ 0
77	76	a1i	⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ∧ 𝑣 ∈ { 𝑧 ∈ 𝑆 ∣ ( 1^st ‘ 𝑧 ) = ( 𝑃 − ( 2 · 𝑢 ) ) } ) ) → 2 ≠ 0 )
78	74 75 77	divcan3d	⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ∧ 𝑣 ∈ { 𝑧 ∈ 𝑆 ∣ ( 1^st ‘ 𝑧 ) = ( 𝑃 − ( 2 · 𝑢 ) ) } ) ) → ( ( 2 · 𝑢 ) / 2 ) = 𝑢 )
79	72 78	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ∧ 𝑣 ∈ { 𝑧 ∈ 𝑆 ∣ ( 1^st ‘ 𝑧 ) = ( 𝑃 − ( 2 · 𝑢 ) ) } ) ) → ( ( 𝑃 − ( 1^st ‘ 𝑣 ) ) / 2 ) = 𝑢 )
80	79	ralrimivva	⊢ ( 𝜑 → ∀ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ∀ 𝑣 ∈ { 𝑧 ∈ 𝑆 ∣ ( 1^st ‘ 𝑧 ) = ( 𝑃 − ( 2 · 𝑢 ) ) } ( ( 𝑃 − ( 1^st ‘ 𝑣 ) ) / 2 ) = 𝑢 )
81		invdisj	⊢ ( ∀ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ∀ 𝑣 ∈ { 𝑧 ∈ 𝑆 ∣ ( 1^st ‘ 𝑧 ) = ( 𝑃 − ( 2 · 𝑢 ) ) } ( ( 𝑃 − ( 1^st ‘ 𝑣 ) ) / 2 ) = 𝑢 → Disj 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) { 𝑧 ∈ 𝑆 ∣ ( 1^st ‘ 𝑧 ) = ( 𝑃 − ( 2 · 𝑢 ) ) } )
82	80 81	syl	⊢ ( 𝜑 → Disj 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) { 𝑧 ∈ 𝑆 ∣ ( 1^st ‘ 𝑧 ) = ( 𝑃 − ( 2 · 𝑢 ) ) } )
83	11 59 82	hashiun	⊢ ( 𝜑 → ( ♯ ‘ ∪ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) { 𝑧 ∈ 𝑆 ∣ ( 1^st ‘ 𝑧 ) = ( 𝑃 − ( 2 · 𝑢 ) ) } ) = Σ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ( 1^st ‘ 𝑧 ) = ( 𝑃 − ( 2 · 𝑢 ) ) } ) )
84		iunrab	⊢ ∪ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) { 𝑧 ∈ 𝑆 ∣ ( 1^st ‘ 𝑧 ) = ( 𝑃 − ( 2 · 𝑢 ) ) } = { 𝑧 ∈ 𝑆 ∣ ∃ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ( 1^st ‘ 𝑧 ) = ( 𝑃 − ( 2 · 𝑢 ) ) }
85		eldifsni	⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 𝑃 ≠ 2 )
86	1 85	syl	⊢ ( 𝜑 → 𝑃 ≠ 2 )
87	86	necomd	⊢ ( 𝜑 → 2 ≠ 𝑃 )
88	87	neneqd	⊢ ( 𝜑 → ¬ 2 = 𝑃 )
89	88	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ¬ 2 = 𝑃 )
90		uzid	⊢ ( 2 ∈ ℤ → 2 ∈ ( ℤ_≥ ‘ 2 ) )
91	17 90	ax-mp	⊢ 2 ∈ ( ℤ_≥ ‘ 2 )
92	1	eldifad	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
93	92	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → 𝑃 ∈ ℙ )
94		dvdsprm	⊢ ( ( 2 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ) → ( 2 ∥ 𝑃 ↔ 2 = 𝑃 ) )
95	91 93 94	sylancr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( 2 ∥ 𝑃 ↔ 2 = 𝑃 ) )
96	89 95	mtbird	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ¬ 2 ∥ 𝑃 )
97	14	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → 𝑃 ∈ ℕ )
98	97	nncnd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → 𝑃 ∈ ℂ )
99	21	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( 2 · 𝑢 ) ∈ ℤ )
100	99	zcnd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( 2 · 𝑢 ) ∈ ℂ )
101	98 100	npcand	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( 𝑃 − ( 2 · 𝑢 ) ) + ( 2 · 𝑢 ) ) = 𝑃 )
102	101	breq2d	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( 2 ∥ ( ( 𝑃 − ( 2 · 𝑢 ) ) + ( 2 · 𝑢 ) ) ↔ 2 ∥ 𝑃 ) )
103	96 102	mtbird	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ¬ 2 ∥ ( ( 𝑃 − ( 2 · 𝑢 ) ) + ( 2 · 𝑢 ) ) )
104	18	adantl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → 𝑢 ∈ ℤ )
105		dvdsmul1	⊢ ( ( 2 ∈ ℤ ∧ 𝑢 ∈ ℤ ) → 2 ∥ ( 2 · 𝑢 ) )
106	17 104 105	sylancr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → 2 ∥ ( 2 · 𝑢 ) )
107	17	a1i	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → 2 ∈ ℤ )
108	97	nnzd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → 𝑃 ∈ ℤ )
109	108 99	zsubcld	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( 𝑃 − ( 2 · 𝑢 ) ) ∈ ℤ )
110		dvds2add	⊢ ( ( 2 ∈ ℤ ∧ ( 𝑃 − ( 2 · 𝑢 ) ) ∈ ℤ ∧ ( 2 · 𝑢 ) ∈ ℤ ) → ( ( 2 ∥ ( 𝑃 − ( 2 · 𝑢 ) ) ∧ 2 ∥ ( 2 · 𝑢 ) ) → 2 ∥ ( ( 𝑃 − ( 2 · 𝑢 ) ) + ( 2 · 𝑢 ) ) ) )
111	107 109 99 110	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( 2 ∥ ( 𝑃 − ( 2 · 𝑢 ) ) ∧ 2 ∥ ( 2 · 𝑢 ) ) → 2 ∥ ( ( 𝑃 − ( 2 · 𝑢 ) ) + ( 2 · 𝑢 ) ) ) )
112	106 111	mpan2d	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( 2 ∥ ( 𝑃 − ( 2 · 𝑢 ) ) → 2 ∥ ( ( 𝑃 − ( 2 · 𝑢 ) ) + ( 2 · 𝑢 ) ) ) )
113	103 112	mtod	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ¬ 2 ∥ ( 𝑃 − ( 2 · 𝑢 ) ) )
114		breq2	⊢ ( ( 1^st ‘ 𝑧 ) = ( 𝑃 − ( 2 · 𝑢 ) ) → ( 2 ∥ ( 1^st ‘ 𝑧 ) ↔ 2 ∥ ( 𝑃 − ( 2 · 𝑢 ) ) ) )
115	114	notbid	⊢ ( ( 1^st ‘ 𝑧 ) = ( 𝑃 − ( 2 · 𝑢 ) ) → ( ¬ 2 ∥ ( 1^st ‘ 𝑧 ) ↔ ¬ 2 ∥ ( 𝑃 − ( 2 · 𝑢 ) ) ) )
116	113 115	syl5ibrcom	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( 1^st ‘ 𝑧 ) = ( 𝑃 − ( 2 · 𝑢 ) ) → ¬ 2 ∥ ( 1^st ‘ 𝑧 ) ) )
117	116	rexlimdva	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → ( ∃ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ( 1^st ‘ 𝑧 ) = ( 𝑃 − ( 2 · 𝑢 ) ) → ¬ 2 ∥ ( 1^st ‘ 𝑧 ) ) )
118		simpr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → 𝑧 ∈ 𝑆 )
119	32 118	sselid	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → 𝑧 ∈ ( ( 1 ... 𝑀 ) × ( 1 ... 𝑁 ) ) )
120		xp1st	⊢ ( 𝑧 ∈ ( ( 1 ... 𝑀 ) × ( 1 ... 𝑁 ) ) → ( 1^st ‘ 𝑧 ) ∈ ( 1 ... 𝑀 ) )
121	119 120	syl	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → ( 1^st ‘ 𝑧 ) ∈ ( 1 ... 𝑀 ) )
122		elfzelz	⊢ ( ( 1^st ‘ 𝑧 ) ∈ ( 1 ... 𝑀 ) → ( 1^st ‘ 𝑧 ) ∈ ℤ )
123		odd2np1	⊢ ( ( 1^st ‘ 𝑧 ) ∈ ℤ → ( ¬ 2 ∥ ( 1^st ‘ 𝑧 ) ↔ ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) )
124	121 122 123	3syl	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → ( ¬ 2 ∥ ( 1^st ‘ 𝑧 ) ↔ ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) )
125	1 4	gausslemma2dlem0b	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
126	125	nnred	⊢ ( 𝜑 → 𝑀 ∈ ℝ )
127	126	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → 𝑀 ∈ ℝ )
128	127	rehalfcld	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → ( 𝑀 / 2 ) ∈ ℝ )
129	128	flcld	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → ( ⌊ ‘ ( 𝑀 / 2 ) ) ∈ ℤ )
130	129	peano2zd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ∈ ℤ )
131	125	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → 𝑀 ∈ ℕ )
132	131	nnzd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → 𝑀 ∈ ℤ )
133		simprl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → 𝑛 ∈ ℤ )
134	132 133	zsubcld	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → ( 𝑀 − 𝑛 ) ∈ ℤ )
135		reflcl	⊢ ( ( 𝑀 / 2 ) ∈ ℝ → ( ⌊ ‘ ( 𝑀 / 2 ) ) ∈ ℝ )
136	128 135	syl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → ( ⌊ ‘ ( 𝑀 / 2 ) ) ∈ ℝ )
137	134	zred	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → ( 𝑀 − 𝑛 ) ∈ ℝ )
138		flle	⊢ ( ( 𝑀 / 2 ) ∈ ℝ → ( ⌊ ‘ ( 𝑀 / 2 ) ) ≤ ( 𝑀 / 2 ) )
139	128 138	syl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → ( ⌊ ‘ ( 𝑀 / 2 ) ) ≤ ( 𝑀 / 2 ) )
140		zre	⊢ ( 𝑛 ∈ ℤ → 𝑛 ∈ ℝ )
141	140	ad2antrl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → 𝑛 ∈ ℝ )
142		simprr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) )
143	121	adantr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → ( 1^st ‘ 𝑧 ) ∈ ( 1 ... 𝑀 ) )
144	142 143	eqeltrd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → ( ( 2 · 𝑛 ) + 1 ) ∈ ( 1 ... 𝑀 ) )
145		elfzle2	⊢ ( ( ( 2 · 𝑛 ) + 1 ) ∈ ( 1 ... 𝑀 ) → ( ( 2 · 𝑛 ) + 1 ) ≤ 𝑀 )
146	144 145	syl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → ( ( 2 · 𝑛 ) + 1 ) ≤ 𝑀 )
147		zmulcl	⊢ ( ( 2 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( 2 · 𝑛 ) ∈ ℤ )
148	17 133 147	sylancr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → ( 2 · 𝑛 ) ∈ ℤ )
149		zltp1le	⊢ ( ( ( 2 · 𝑛 ) ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( 2 · 𝑛 ) < 𝑀 ↔ ( ( 2 · 𝑛 ) + 1 ) ≤ 𝑀 ) )
150	148 132 149	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → ( ( 2 · 𝑛 ) < 𝑀 ↔ ( ( 2 · 𝑛 ) + 1 ) ≤ 𝑀 ) )
151	146 150	mpbird	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → ( 2 · 𝑛 ) < 𝑀 )
152		2re	⊢ 2 ∈ ℝ
153	152	a1i	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → 2 ∈ ℝ )
154		2pos	⊢ 0 < 2
155	154	a1i	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → 0 < 2 )
156		ltmuldiv2	⊢ ( ( 𝑛 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( 2 · 𝑛 ) < 𝑀 ↔ 𝑛 < ( 𝑀 / 2 ) ) )
157	141 127 153 155 156	syl112anc	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → ( ( 2 · 𝑛 ) < 𝑀 ↔ 𝑛 < ( 𝑀 / 2 ) ) )
158	151 157	mpbid	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → 𝑛 < ( 𝑀 / 2 ) )
159	128	recnd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → ( 𝑀 / 2 ) ∈ ℂ )
160	125	nncnd	⊢ ( 𝜑 → 𝑀 ∈ ℂ )
161	160	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → 𝑀 ∈ ℂ )
162	161	2halvesd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → ( ( 𝑀 / 2 ) + ( 𝑀 / 2 ) ) = 𝑀 )
163	159 159 162	mvlraddd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → ( 𝑀 / 2 ) = ( 𝑀 − ( 𝑀 / 2 ) ) )
164	158 163	breqtrd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → 𝑛 < ( 𝑀 − ( 𝑀 / 2 ) ) )
165	141 127 128 164	ltsub13d	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → ( 𝑀 / 2 ) < ( 𝑀 − 𝑛 ) )
166	136 128 137 139 165	lelttrd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → ( ⌊ ‘ ( 𝑀 / 2 ) ) < ( 𝑀 − 𝑛 ) )
167		zltp1le	⊢ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) ∈ ℤ ∧ ( 𝑀 − 𝑛 ) ∈ ℤ ) → ( ( ⌊ ‘ ( 𝑀 / 2 ) ) < ( 𝑀 − 𝑛 ) ↔ ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ≤ ( 𝑀 − 𝑛 ) ) )
168	129 134 167	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → ( ( ⌊ ‘ ( 𝑀 / 2 ) ) < ( 𝑀 − 𝑛 ) ↔ ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ≤ ( 𝑀 − 𝑛 ) ) )
169	166 168	mpbid	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ≤ ( 𝑀 − 𝑛 ) )
170		2t0e0	⊢ ( 2 · 0 ) = 0
171		2cn	⊢ 2 ∈ ℂ
172		zcn	⊢ ( 𝑛 ∈ ℤ → 𝑛 ∈ ℂ )
173	172	ad2antrl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → 𝑛 ∈ ℂ )
174		mulcl	⊢ ( ( 2 ∈ ℂ ∧ 𝑛 ∈ ℂ ) → ( 2 · 𝑛 ) ∈ ℂ )
175	171 173 174	sylancr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → ( 2 · 𝑛 ) ∈ ℂ )
176		pncan	⊢ ( ( ( 2 · 𝑛 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( 2 · 𝑛 ) + 1 ) − 1 ) = ( 2 · 𝑛 ) )
177	175 47 176	sylancl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → ( ( ( 2 · 𝑛 ) + 1 ) − 1 ) = ( 2 · 𝑛 ) )
178		elfznn	⊢ ( ( ( 2 · 𝑛 ) + 1 ) ∈ ( 1 ... 𝑀 ) → ( ( 2 · 𝑛 ) + 1 ) ∈ ℕ )
179		nnm1nn0	⊢ ( ( ( 2 · 𝑛 ) + 1 ) ∈ ℕ → ( ( ( 2 · 𝑛 ) + 1 ) − 1 ) ∈ ℕ₀ )
180	144 178 179	3syl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → ( ( ( 2 · 𝑛 ) + 1 ) − 1 ) ∈ ℕ₀ )
181	177 180	eqeltrrd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → ( 2 · 𝑛 ) ∈ ℕ₀ )
182	181	nn0ge0d	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → 0 ≤ ( 2 · 𝑛 ) )
183	170 182	eqbrtrid	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → ( 2 · 0 ) ≤ ( 2 · 𝑛 ) )
184		0red	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → 0 ∈ ℝ )
185		lemul2	⊢ ( ( 0 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( 0 ≤ 𝑛 ↔ ( 2 · 0 ) ≤ ( 2 · 𝑛 ) ) )
186	184 141 153 155 185	syl112anc	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → ( 0 ≤ 𝑛 ↔ ( 2 · 0 ) ≤ ( 2 · 𝑛 ) ) )
187	183 186	mpbird	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → 0 ≤ 𝑛 )
188	127 141	subge02d	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → ( 0 ≤ 𝑛 ↔ ( 𝑀 − 𝑛 ) ≤ 𝑀 ) )
189	187 188	mpbid	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → ( 𝑀 − 𝑛 ) ≤ 𝑀 )
190	130 132 134 169 189	elfzd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → ( 𝑀 − 𝑛 ) ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) )
191	92	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → 𝑃 ∈ ℙ )
192		prmnn	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
193	191 192	syl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → 𝑃 ∈ ℕ )
194	193	nncnd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → 𝑃 ∈ ℂ )
195		peano2cn	⊢ ( ( 2 · 𝑛 ) ∈ ℂ → ( ( 2 · 𝑛 ) + 1 ) ∈ ℂ )
196	175 195	syl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → ( ( 2 · 𝑛 ) + 1 ) ∈ ℂ )
197	194 196	nncand	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → ( 𝑃 − ( 𝑃 − ( ( 2 · 𝑛 ) + 1 ) ) ) = ( ( 2 · 𝑛 ) + 1 ) )
198		1cnd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → 1 ∈ ℂ )
199	194 175 198	sub32d	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → ( ( 𝑃 − ( 2 · 𝑛 ) ) − 1 ) = ( ( 𝑃 − 1 ) − ( 2 · 𝑛 ) ) )
200	194 175 198	subsub4d	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → ( ( 𝑃 − ( 2 · 𝑛 ) ) − 1 ) = ( 𝑃 − ( ( 2 · 𝑛 ) + 1 ) ) )
201		2cnd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → 2 ∈ ℂ )
202	201 161 173	subdid	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → ( 2 · ( 𝑀 − 𝑛 ) ) = ( ( 2 · 𝑀 ) − ( 2 · 𝑛 ) ) )
203	4	oveq2i	⊢ ( 2 · 𝑀 ) = ( 2 · ( ( 𝑃 − 1 ) / 2 ) )
204	14	nnzd	⊢ ( 𝜑 → 𝑃 ∈ ℤ )
205	204	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → 𝑃 ∈ ℤ )
206		peano2zm	⊢ ( 𝑃 ∈ ℤ → ( 𝑃 − 1 ) ∈ ℤ )
207	205 206	syl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → ( 𝑃 − 1 ) ∈ ℤ )
208	207	zcnd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → ( 𝑃 − 1 ) ∈ ℂ )
209	76	a1i	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → 2 ≠ 0 )
210	208 201 209	divcan2d	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → ( 2 · ( ( 𝑃 − 1 ) / 2 ) ) = ( 𝑃 − 1 ) )
211	203 210	eqtrid	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → ( 2 · 𝑀 ) = ( 𝑃 − 1 ) )
212	211	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → ( ( 2 · 𝑀 ) − ( 2 · 𝑛 ) ) = ( ( 𝑃 − 1 ) − ( 2 · 𝑛 ) ) )
213	202 212	eqtr2d	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → ( ( 𝑃 − 1 ) − ( 2 · 𝑛 ) ) = ( 2 · ( 𝑀 − 𝑛 ) ) )
214	199 200 213	3eqtr3d	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → ( 𝑃 − ( ( 2 · 𝑛 ) + 1 ) ) = ( 2 · ( 𝑀 − 𝑛 ) ) )
215	214	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → ( 𝑃 − ( 𝑃 − ( ( 2 · 𝑛 ) + 1 ) ) ) = ( 𝑃 − ( 2 · ( 𝑀 − 𝑛 ) ) ) )
216	197 215 142	3eqtr3rd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → ( 1^st ‘ 𝑧 ) = ( 𝑃 − ( 2 · ( 𝑀 − 𝑛 ) ) ) )
217		oveq2	⊢ ( 𝑢 = ( 𝑀 − 𝑛 ) → ( 2 · 𝑢 ) = ( 2 · ( 𝑀 − 𝑛 ) ) )
218	217	oveq2d	⊢ ( 𝑢 = ( 𝑀 − 𝑛 ) → ( 𝑃 − ( 2 · 𝑢 ) ) = ( 𝑃 − ( 2 · ( 𝑀 − 𝑛 ) ) ) )
219	218	rspceeqv	⊢ ( ( ( 𝑀 − 𝑛 ) ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ∧ ( 1^st ‘ 𝑧 ) = ( 𝑃 − ( 2 · ( 𝑀 − 𝑛 ) ) ) ) → ∃ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ( 1^st ‘ 𝑧 ) = ( 𝑃 − ( 2 · 𝑢 ) ) )
220	190 216 219	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) ) ) → ∃ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ( 1^st ‘ 𝑧 ) = ( 𝑃 − ( 2 · 𝑢 ) ) )
221	220	rexlimdvaa	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → ( ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = ( 1^st ‘ 𝑧 ) → ∃ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ( 1^st ‘ 𝑧 ) = ( 𝑃 − ( 2 · 𝑢 ) ) ) )
222	124 221	sylbid	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → ( ¬ 2 ∥ ( 1^st ‘ 𝑧 ) → ∃ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ( 1^st ‘ 𝑧 ) = ( 𝑃 − ( 2 · 𝑢 ) ) ) )
223	117 222	impbid	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → ( ∃ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ( 1^st ‘ 𝑧 ) = ( 𝑃 − ( 2 · 𝑢 ) ) ↔ ¬ 2 ∥ ( 1^st ‘ 𝑧 ) ) )
224	223	rabbidva	⊢ ( 𝜑 → { 𝑧 ∈ 𝑆 ∣ ∃ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ( 1^st ‘ 𝑧 ) = ( 𝑃 − ( 2 · 𝑢 ) ) } = { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1^st ‘ 𝑧 ) } )
225	84 224	eqtrid	⊢ ( 𝜑 → ∪ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) { 𝑧 ∈ 𝑆 ∣ ( 1^st ‘ 𝑧 ) = ( 𝑃 − ( 2 · 𝑢 ) ) } = { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1^st ‘ 𝑧 ) } )
226	225	fveq2d	⊢ ( 𝜑 → ( ♯ ‘ ∪ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) { 𝑧 ∈ 𝑆 ∣ ( 1^st ‘ 𝑧 ) = ( 𝑃 − ( 2 · 𝑢 ) ) } ) = ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1^st ‘ 𝑧 ) } ) )
227	6	relopabiv	⊢ Rel 𝑆
228		relss	⊢ ( { 𝑧 ∈ 𝑆 ∣ ( 1^st ‘ 𝑧 ) = ( 𝑃 − ( 2 · 𝑢 ) ) } ⊆ 𝑆 → ( Rel 𝑆 → Rel { 𝑧 ∈ 𝑆 ∣ ( 1^st ‘ 𝑧 ) = ( 𝑃 − ( 2 · 𝑢 ) ) } ) )
229	57 227 228	mp2	⊢ Rel { 𝑧 ∈ 𝑆 ∣ ( 1^st ‘ 𝑧 ) = ( 𝑃 − ( 2 · 𝑢 ) ) }
230		relxp	⊢ Rel ( { ( 𝑃 − ( 2 · 𝑢 ) ) } × ( 1 ... ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) )
231	6	eleq2i	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑆 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 1 ... 𝑀 ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑦 · 𝑃 ) < ( 𝑥 · 𝑄 ) ) } )
232		opabidw	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 1 ... 𝑀 ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑦 · 𝑃 ) < ( 𝑥 · 𝑄 ) ) } ↔ ( ( 𝑥 ∈ ( 1 ... 𝑀 ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑦 · 𝑃 ) < ( 𝑥 · 𝑄 ) ) )
233	231 232	bitri	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑆 ↔ ( ( 𝑥 ∈ ( 1 ... 𝑀 ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑦 · 𝑃 ) < ( 𝑥 · 𝑄 ) ) )
234		anass	⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁 ) ∧ ( 𝑦 · 𝑃 ) < ( ( 𝑃 − ( 2 · 𝑢 ) ) · 𝑄 ) ) ↔ ( 𝑦 ∈ ℕ ∧ ( 𝑦 ≤ 𝑁 ∧ ( 𝑦 · 𝑃 ) < ( ( 𝑃 − ( 2 · 𝑢 ) ) · 𝑄 ) ) ) )
235	24	peano2zd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) + 1 ) ∈ ℤ )
236	235	zred	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) + 1 ) ∈ ℝ )
237	236	adantr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) ∧ 𝑦 ∈ ℕ ) → ( ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) + 1 ) ∈ ℝ )
238	13	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) ∧ 𝑦 ∈ ℕ ) → 𝑄 ∈ ℝ )
239		nnre	⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℝ )
240	239	adantl	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) ∧ 𝑦 ∈ ℕ ) → 𝑦 ∈ ℝ )
241		lesub	⊢ ( ( ( ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) + 1 ) ∈ ℝ ∧ 𝑄 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) + 1 ) ≤ ( 𝑄 − 𝑦 ) ↔ 𝑦 ≤ ( 𝑄 − ( ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) + 1 ) ) ) )
242	237 238 240 241	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) ∧ 𝑦 ∈ ℕ ) → ( ( ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) + 1 ) ≤ ( 𝑄 − 𝑦 ) ↔ 𝑦 ≤ ( 𝑄 − ( ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) + 1 ) ) ) )
243	13	adantr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → 𝑄 ∈ ℝ )
244	243	recnd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → 𝑄 ∈ ℂ )
245	66 244	mulcomd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( 𝑃 · 𝑄 ) = ( 𝑄 · 𝑃 ) )
246	68 244	mulcomd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( 2 · 𝑢 ) · 𝑄 ) = ( 𝑄 · ( 2 · 𝑢 ) ) )
247	65	nnne0d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → 𝑃 ≠ 0 )
248	244 66 247	divcan1d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( 𝑄 / 𝑃 ) · 𝑃 ) = 𝑄 )
249	248	oveq1d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( ( 𝑄 / 𝑃 ) · 𝑃 ) · ( 2 · 𝑢 ) ) = ( 𝑄 · ( 2 · 𝑢 ) ) )
250	16	recnd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( 𝑄 / 𝑃 ) ∈ ℂ )
251	250 66 68	mul32d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( ( 𝑄 / 𝑃 ) · 𝑃 ) · ( 2 · 𝑢 ) ) = ( ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) · 𝑃 ) )
252	246 249 251	3eqtr2d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( 2 · 𝑢 ) · 𝑄 ) = ( ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) · 𝑃 ) )
253	245 252	oveq12d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( 𝑃 · 𝑄 ) − ( ( 2 · 𝑢 ) · 𝑄 ) ) = ( ( 𝑄 · 𝑃 ) − ( ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) · 𝑃 ) ) )
254	66 68 244	subdird	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( 𝑃 − ( 2 · 𝑢 ) ) · 𝑄 ) = ( ( 𝑃 · 𝑄 ) − ( ( 2 · 𝑢 ) · 𝑄 ) ) )
255	23	recnd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ∈ ℂ )
256	244 255 66	subdird	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( 𝑄 − ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) · 𝑃 ) = ( ( 𝑄 · 𝑃 ) − ( ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) · 𝑃 ) ) )
257	253 254 256	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( 𝑃 − ( 2 · 𝑢 ) ) · 𝑄 ) = ( ( 𝑄 − ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) · 𝑃 ) )
258	257	adantr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) ∧ 𝑦 ∈ ℕ ) → ( ( 𝑃 − ( 2 · 𝑢 ) ) · 𝑄 ) = ( ( 𝑄 − ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) · 𝑃 ) )
259	258	breq2d	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) ∧ 𝑦 ∈ ℕ ) → ( ( 𝑦 · 𝑃 ) < ( ( 𝑃 − ( 2 · 𝑢 ) ) · 𝑄 ) ↔ ( 𝑦 · 𝑃 ) < ( ( 𝑄 − ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) · 𝑃 ) ) )
260	23	adantr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) ∧ 𝑦 ∈ ℕ ) → ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ∈ ℝ )
261	238 260	resubcld	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) ∧ 𝑦 ∈ ℕ ) → ( 𝑄 − ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ∈ ℝ )
262	65	adantr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) ∧ 𝑦 ∈ ℕ ) → 𝑃 ∈ ℕ )
263	262	nnred	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) ∧ 𝑦 ∈ ℕ ) → 𝑃 ∈ ℝ )
264	262	nngt0d	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) ∧ 𝑦 ∈ ℕ ) → 0 < 𝑃 )
265		ltmul1	⊢ ( ( 𝑦 ∈ ℝ ∧ ( 𝑄 − ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ∈ ℝ ∧ ( 𝑃 ∈ ℝ ∧ 0 < 𝑃 ) ) → ( 𝑦 < ( 𝑄 − ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ↔ ( 𝑦 · 𝑃 ) < ( ( 𝑄 − ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) · 𝑃 ) ) )
266	240 261 263 264 265	syl112anc	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) ∧ 𝑦 ∈ ℕ ) → ( 𝑦 < ( 𝑄 − ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ↔ ( 𝑦 · 𝑃 ) < ( ( 𝑄 − ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) · 𝑃 ) ) )
267		ltsub13	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑄 ∈ ℝ ∧ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ∈ ℝ ) → ( 𝑦 < ( 𝑄 − ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ↔ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) < ( 𝑄 − 𝑦 ) ) )
268	240 238 260 267	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) ∧ 𝑦 ∈ ℕ ) → ( 𝑦 < ( 𝑄 − ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ↔ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) < ( 𝑄 − 𝑦 ) ) )
269	259 266 268	3bitr2d	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) ∧ 𝑦 ∈ ℕ ) → ( ( 𝑦 · 𝑃 ) < ( ( 𝑃 − ( 2 · 𝑢 ) ) · 𝑄 ) ↔ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) < ( 𝑄 − 𝑦 ) ) )
270	12	adantr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → 𝑄 ∈ ℕ )
271	270	nnzd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → 𝑄 ∈ ℤ )
272		nnz	⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℤ )
273		zsubcl	⊢ ( ( 𝑄 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( 𝑄 − 𝑦 ) ∈ ℤ )
274	271 272 273	syl2an	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) ∧ 𝑦 ∈ ℕ ) → ( 𝑄 − 𝑦 ) ∈ ℤ )
275		fllt	⊢ ( ( ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ∈ ℝ ∧ ( 𝑄 − 𝑦 ) ∈ ℤ ) → ( ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) < ( 𝑄 − 𝑦 ) ↔ ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) < ( 𝑄 − 𝑦 ) ) )
276	260 274 275	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) ∧ 𝑦 ∈ ℕ ) → ( ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) < ( 𝑄 − 𝑦 ) ↔ ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) < ( 𝑄 − 𝑦 ) ) )
277	24	adantr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) ∧ 𝑦 ∈ ℕ ) → ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ∈ ℤ )
278		zltp1le	⊢ ( ( ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ∈ ℤ ∧ ( 𝑄 − 𝑦 ) ∈ ℤ ) → ( ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) < ( 𝑄 − 𝑦 ) ↔ ( ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) + 1 ) ≤ ( 𝑄 − 𝑦 ) ) )
279	277 274 278	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) ∧ 𝑦 ∈ ℕ ) → ( ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) < ( 𝑄 − 𝑦 ) ↔ ( ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) + 1 ) ≤ ( 𝑄 − 𝑦 ) ) )
280	269 276 279	3bitrd	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) ∧ 𝑦 ∈ ℕ ) → ( ( 𝑦 · 𝑃 ) < ( ( 𝑃 − ( 2 · 𝑢 ) ) · 𝑄 ) ↔ ( ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) + 1 ) ≤ ( 𝑄 − 𝑦 ) ) )
281	5	oveq2i	⊢ ( 2 · 𝑁 ) = ( 2 · ( ( 𝑄 − 1 ) / 2 ) )
282		peano2rem	⊢ ( 𝑄 ∈ ℝ → ( 𝑄 − 1 ) ∈ ℝ )
283	243 282	syl	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( 𝑄 − 1 ) ∈ ℝ )
284	283	recnd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( 𝑄 − 1 ) ∈ ℂ )
285		2cnd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → 2 ∈ ℂ )
286	76	a1i	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → 2 ≠ 0 )
287	284 285 286	divcan2d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( 2 · ( ( 𝑄 − 1 ) / 2 ) ) = ( 𝑄 − 1 ) )
288	281 287	eqtrid	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( 2 · 𝑁 ) = ( 𝑄 − 1 ) )
289	288	oveq1d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) = ( ( 𝑄 − 1 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) )
290		1cnd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → 1 ∈ ℂ )
291	24	zcnd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ∈ ℂ )
292	244 290 291	sub32d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( 𝑄 − 1 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) = ( ( 𝑄 − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) − 1 ) )
293	244 291 290	subsub4d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( 𝑄 − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) − 1 ) = ( 𝑄 − ( ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) + 1 ) ) )
294	289 292 293	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) = ( 𝑄 − ( ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) + 1 ) ) )
295	294	adantr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) ∧ 𝑦 ∈ ℕ ) → ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) = ( 𝑄 − ( ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) + 1 ) ) )
296	295	breq2d	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) ∧ 𝑦 ∈ ℕ ) → ( 𝑦 ≤ ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ↔ 𝑦 ≤ ( 𝑄 − ( ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) + 1 ) ) ) )
297	242 280 296	3bitr4d	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) ∧ 𝑦 ∈ ℕ ) → ( ( 𝑦 · 𝑃 ) < ( ( 𝑃 − ( 2 · 𝑢 ) ) · 𝑄 ) ↔ 𝑦 ≤ ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) )
298	297	anbi2d	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) ∧ 𝑦 ∈ ℕ ) → ( ( 𝑦 ≤ 𝑁 ∧ ( 𝑦 · 𝑃 ) < ( ( 𝑃 − ( 2 · 𝑢 ) ) · 𝑄 ) ) ↔ ( 𝑦 ≤ 𝑁 ∧ 𝑦 ≤ ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) ) )
299		2nn	⊢ 2 ∈ ℕ
300	2 5	gausslemma2dlem0b	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
301		nnmulcl	⊢ ( ( 2 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 2 · 𝑁 ) ∈ ℕ )
302	299 300 301	sylancr	⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℕ )
303	302	adantr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( 2 · 𝑁 ) ∈ ℕ )
304	303	nnred	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( 2 · 𝑁 ) ∈ ℝ )
305	300	adantr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → 𝑁 ∈ ℕ )
306	305	nnred	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → 𝑁 ∈ ℝ )
307	24	zred	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ∈ ℝ )
308	300	nncnd	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
309	308	adantr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → 𝑁 ∈ ℂ )
310	309	2timesd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( 2 · 𝑁 ) = ( 𝑁 + 𝑁 ) )
311	309 309 310	mvrladdd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( 2 · 𝑁 ) − 𝑁 ) = 𝑁 )
312	243	rehalfcld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( 𝑄 / 2 ) ∈ ℝ )
313	243	ltm1d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( 𝑄 − 1 ) < 𝑄 )
314	152	a1i	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → 2 ∈ ℝ )
315	154	a1i	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → 0 < 2 )
316		ltdiv1	⊢ ( ( ( 𝑄 − 1 ) ∈ ℝ ∧ 𝑄 ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( 𝑄 − 1 ) < 𝑄 ↔ ( ( 𝑄 − 1 ) / 2 ) < ( 𝑄 / 2 ) ) )
317	283 243 314 315 316	syl112anc	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( 𝑄 − 1 ) < 𝑄 ↔ ( ( 𝑄 − 1 ) / 2 ) < ( 𝑄 / 2 ) ) )
318	313 317	mpbid	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( 𝑄 − 1 ) / 2 ) < ( 𝑄 / 2 ) )
319	5 318	eqbrtrid	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → 𝑁 < ( 𝑄 / 2 ) )
320	306 312 319	ltled	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → 𝑁 ≤ ( 𝑄 / 2 ) )
321	244 285 66 286	div32d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( 𝑄 / 2 ) · 𝑃 ) = ( 𝑄 · ( 𝑃 / 2 ) ) )
322	126	adantr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → 𝑀 ∈ ℝ )
323	322	rehalfcld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( 𝑀 / 2 ) ∈ ℝ )
324		peano2re	⊢ ( ( ⌊ ‘ ( 𝑀 / 2 ) ) ∈ ℝ → ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ∈ ℝ )
325	323 135 324	3syl	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ∈ ℝ )
326	19	zred	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → 𝑢 ∈ ℝ )
327		flltp1	⊢ ( ( 𝑀 / 2 ) ∈ ℝ → ( 𝑀 / 2 ) < ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) )
328	323 327	syl	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( 𝑀 / 2 ) < ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) )
329		elfzle1	⊢ ( 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) → ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ≤ 𝑢 )
330	329	adantl	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ≤ 𝑢 )
331	323 325 326 328 330	ltletrd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( 𝑀 / 2 ) < 𝑢 )
332		ltdivmul	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑢 ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( 𝑀 / 2 ) < 𝑢 ↔ 𝑀 < ( 2 · 𝑢 ) ) )
333	322 326 314 315 332	syl112anc	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( 𝑀 / 2 ) < 𝑢 ↔ 𝑀 < ( 2 · 𝑢 ) ) )
334	331 333	mpbid	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → 𝑀 < ( 2 · 𝑢 ) )
335	4 334	eqbrtrrid	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( 𝑃 − 1 ) / 2 ) < ( 2 · 𝑢 ) )
336	65	nnred	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → 𝑃 ∈ ℝ )
337		peano2rem	⊢ ( 𝑃 ∈ ℝ → ( 𝑃 − 1 ) ∈ ℝ )
338	336 337	syl	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( 𝑃 − 1 ) ∈ ℝ )
339		ltdivmul	⊢ ( ( ( 𝑃 − 1 ) ∈ ℝ ∧ ( 2 · 𝑢 ) ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( ( 𝑃 − 1 ) / 2 ) < ( 2 · 𝑢 ) ↔ ( 𝑃 − 1 ) < ( 2 · ( 2 · 𝑢 ) ) ) )
340	338 22 314 315 339	syl112anc	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( ( 𝑃 − 1 ) / 2 ) < ( 2 · 𝑢 ) ↔ ( 𝑃 − 1 ) < ( 2 · ( 2 · 𝑢 ) ) ) )
341	335 340	mpbid	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( 𝑃 − 1 ) < ( 2 · ( 2 · 𝑢 ) ) )
342	204	adantr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → 𝑃 ∈ ℤ )
343		zmulcl	⊢ ( ( 2 ∈ ℤ ∧ ( 2 · 𝑢 ) ∈ ℤ ) → ( 2 · ( 2 · 𝑢 ) ) ∈ ℤ )
344	17 21 343	sylancr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( 2 · ( 2 · 𝑢 ) ) ∈ ℤ )
345		zlem1lt	⊢ ( ( 𝑃 ∈ ℤ ∧ ( 2 · ( 2 · 𝑢 ) ) ∈ ℤ ) → ( 𝑃 ≤ ( 2 · ( 2 · 𝑢 ) ) ↔ ( 𝑃 − 1 ) < ( 2 · ( 2 · 𝑢 ) ) ) )
346	342 344 345	syl2anc	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( 𝑃 ≤ ( 2 · ( 2 · 𝑢 ) ) ↔ ( 𝑃 − 1 ) < ( 2 · ( 2 · 𝑢 ) ) ) )
347	341 346	mpbird	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → 𝑃 ≤ ( 2 · ( 2 · 𝑢 ) ) )
348		ledivmul	⊢ ( ( 𝑃 ∈ ℝ ∧ ( 2 · 𝑢 ) ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( 𝑃 / 2 ) ≤ ( 2 · 𝑢 ) ↔ 𝑃 ≤ ( 2 · ( 2 · 𝑢 ) ) ) )
349	336 22 314 315 348	syl112anc	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( 𝑃 / 2 ) ≤ ( 2 · 𝑢 ) ↔ 𝑃 ≤ ( 2 · ( 2 · 𝑢 ) ) ) )
350	347 349	mpbird	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( 𝑃 / 2 ) ≤ ( 2 · 𝑢 ) )
351	336	rehalfcld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( 𝑃 / 2 ) ∈ ℝ )
352	270	nngt0d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → 0 < 𝑄 )
353		lemul2	⊢ ( ( ( 𝑃 / 2 ) ∈ ℝ ∧ ( 2 · 𝑢 ) ∈ ℝ ∧ ( 𝑄 ∈ ℝ ∧ 0 < 𝑄 ) ) → ( ( 𝑃 / 2 ) ≤ ( 2 · 𝑢 ) ↔ ( 𝑄 · ( 𝑃 / 2 ) ) ≤ ( 𝑄 · ( 2 · 𝑢 ) ) ) )
354	351 22 243 352 353	syl112anc	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( 𝑃 / 2 ) ≤ ( 2 · 𝑢 ) ↔ ( 𝑄 · ( 𝑃 / 2 ) ) ≤ ( 𝑄 · ( 2 · 𝑢 ) ) ) )
355	350 354	mpbid	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( 𝑄 · ( 𝑃 / 2 ) ) ≤ ( 𝑄 · ( 2 · 𝑢 ) ) )
356	321 355	eqbrtrd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( 𝑄 / 2 ) · 𝑃 ) ≤ ( 𝑄 · ( 2 · 𝑢 ) ) )
357	243 22	remulcld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( 𝑄 · ( 2 · 𝑢 ) ) ∈ ℝ )
358	65	nngt0d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → 0 < 𝑃 )
359		lemuldiv	⊢ ( ( ( 𝑄 / 2 ) ∈ ℝ ∧ ( 𝑄 · ( 2 · 𝑢 ) ) ∈ ℝ ∧ ( 𝑃 ∈ ℝ ∧ 0 < 𝑃 ) ) → ( ( ( 𝑄 / 2 ) · 𝑃 ) ≤ ( 𝑄 · ( 2 · 𝑢 ) ) ↔ ( 𝑄 / 2 ) ≤ ( ( 𝑄 · ( 2 · 𝑢 ) ) / 𝑃 ) ) )
360	312 357 336 358 359	syl112anc	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( ( 𝑄 / 2 ) · 𝑃 ) ≤ ( 𝑄 · ( 2 · 𝑢 ) ) ↔ ( 𝑄 / 2 ) ≤ ( ( 𝑄 · ( 2 · 𝑢 ) ) / 𝑃 ) ) )
361	356 360	mpbid	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( 𝑄 / 2 ) ≤ ( ( 𝑄 · ( 2 · 𝑢 ) ) / 𝑃 ) )
362	244 68 66 247	div23d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( 𝑄 · ( 2 · 𝑢 ) ) / 𝑃 ) = ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) )
363	361 362	breqtrd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( 𝑄 / 2 ) ≤ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) )
364	306 312 23 320 363	letrd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → 𝑁 ≤ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) )
365	300	nnzd	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
366	365	adantr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → 𝑁 ∈ ℤ )
367		flge	⊢ ( ( ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ∈ ℝ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 ≤ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ↔ 𝑁 ≤ ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) )
368	23 366 367	syl2anc	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( 𝑁 ≤ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ↔ 𝑁 ≤ ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) )
369	364 368	mpbid	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → 𝑁 ≤ ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) )
370	311 369	eqbrtrd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( 2 · 𝑁 ) − 𝑁 ) ≤ ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) )
371	304 306 307 370	subled	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ≤ 𝑁 )
372	371	adantr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) ∧ 𝑦 ∈ ℕ ) → ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ≤ 𝑁 )
373	303	nnzd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( 2 · 𝑁 ) ∈ ℤ )
374	373 24	zsubcld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ∈ ℤ )
375	374	adantr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) ∧ 𝑦 ∈ ℕ ) → ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ∈ ℤ )
376	375	zred	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) ∧ 𝑦 ∈ ℕ ) → ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ∈ ℝ )
377	300	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) ∧ 𝑦 ∈ ℕ ) → 𝑁 ∈ ℕ )
378	377	nnred	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) ∧ 𝑦 ∈ ℕ ) → 𝑁 ∈ ℝ )
379		letr	⊢ ( ( 𝑦 ∈ ℝ ∧ ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 𝑦 ≤ ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ∧ ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ≤ 𝑁 ) → 𝑦 ≤ 𝑁 ) )
380	240 376 378 379	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) ∧ 𝑦 ∈ ℕ ) → ( ( 𝑦 ≤ ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ∧ ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ≤ 𝑁 ) → 𝑦 ≤ 𝑁 ) )
381	372 380	mpan2d	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) ∧ 𝑦 ∈ ℕ ) → ( 𝑦 ≤ ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) → 𝑦 ≤ 𝑁 ) )
382	381	pm4.71rd	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) ∧ 𝑦 ∈ ℕ ) → ( 𝑦 ≤ ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ↔ ( 𝑦 ≤ 𝑁 ∧ 𝑦 ≤ ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) ) )
383	298 382	bitr4d	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) ∧ 𝑦 ∈ ℕ ) → ( ( 𝑦 ≤ 𝑁 ∧ ( 𝑦 · 𝑃 ) < ( ( 𝑃 − ( 2 · 𝑢 ) ) · 𝑄 ) ) ↔ 𝑦 ≤ ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) )
384	383	pm5.32da	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( 𝑦 ∈ ℕ ∧ ( 𝑦 ≤ 𝑁 ∧ ( 𝑦 · 𝑃 ) < ( ( 𝑃 − ( 2 · 𝑢 ) ) · 𝑄 ) ) ) ↔ ( 𝑦 ∈ ℕ ∧ 𝑦 ≤ ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) ) )
385	384	adantr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) ∧ 𝑥 = ( 𝑃 − ( 2 · 𝑢 ) ) ) → ( ( 𝑦 ∈ ℕ ∧ ( 𝑦 ≤ 𝑁 ∧ ( 𝑦 · 𝑃 ) < ( ( 𝑃 − ( 2 · 𝑢 ) ) · 𝑄 ) ) ) ↔ ( 𝑦 ∈ ℕ ∧ 𝑦 ≤ ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) ) )
386	234 385	bitrid	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) ∧ 𝑥 = ( 𝑃 − ( 2 · 𝑢 ) ) ) → ( ( ( 𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁 ) ∧ ( 𝑦 · 𝑃 ) < ( ( 𝑃 − ( 2 · 𝑢 ) ) · 𝑄 ) ) ↔ ( 𝑦 ∈ ℕ ∧ 𝑦 ≤ ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) ) )
387		simpr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) ∧ 𝑥 = ( 𝑃 − ( 2 · 𝑢 ) ) ) → 𝑥 = ( 𝑃 − ( 2 · 𝑢 ) ) )
388	342 21	zsubcld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( 𝑃 − ( 2 · 𝑢 ) ) ∈ ℤ )
389		elfzle2	⊢ ( 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) → 𝑢 ≤ 𝑀 )
390	389	adantl	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → 𝑢 ≤ 𝑀 )
391	390 4	breqtrdi	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → 𝑢 ≤ ( ( 𝑃 − 1 ) / 2 ) )
392		lemuldiv2	⊢ ( ( 𝑢 ∈ ℝ ∧ ( 𝑃 − 1 ) ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( 2 · 𝑢 ) ≤ ( 𝑃 − 1 ) ↔ 𝑢 ≤ ( ( 𝑃 − 1 ) / 2 ) ) )
393	326 338 314 315 392	syl112anc	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( 2 · 𝑢 ) ≤ ( 𝑃 − 1 ) ↔ 𝑢 ≤ ( ( 𝑃 − 1 ) / 2 ) ) )
394	391 393	mpbird	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( 2 · 𝑢 ) ≤ ( 𝑃 − 1 ) )
395	336	ltm1d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( 𝑃 − 1 ) < 𝑃 )
396	22 338 336 394 395	lelttrd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( 2 · 𝑢 ) < 𝑃 )
397	22 336	posdifd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( 2 · 𝑢 ) < 𝑃 ↔ 0 < ( 𝑃 − ( 2 · 𝑢 ) ) ) )
398	396 397	mpbid	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → 0 < ( 𝑃 − ( 2 · 𝑢 ) ) )
399		elnnz	⊢ ( ( 𝑃 − ( 2 · 𝑢 ) ) ∈ ℕ ↔ ( ( 𝑃 − ( 2 · 𝑢 ) ) ∈ ℤ ∧ 0 < ( 𝑃 − ( 2 · 𝑢 ) ) ) )
400	388 398 399	sylanbrc	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( 𝑃 − ( 2 · 𝑢 ) ) ∈ ℕ )
401	66 68 290	sub32d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( 𝑃 − ( 2 · 𝑢 ) ) − 1 ) = ( ( 𝑃 − 1 ) − ( 2 · 𝑢 ) ) )
402	4 4	oveq12i	⊢ ( 𝑀 + 𝑀 ) = ( ( ( 𝑃 − 1 ) / 2 ) + ( ( 𝑃 − 1 ) / 2 ) )
403	65	nnzd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → 𝑃 ∈ ℤ )
404	403 206	syl	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( 𝑃 − 1 ) ∈ ℤ )
405	404	zcnd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( 𝑃 − 1 ) ∈ ℂ )
406	405	2halvesd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( ( 𝑃 − 1 ) / 2 ) + ( ( 𝑃 − 1 ) / 2 ) ) = ( 𝑃 − 1 ) )
407	402 406	eqtrid	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( 𝑀 + 𝑀 ) = ( 𝑃 − 1 ) )
408	407	oveq1d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( 𝑀 + 𝑀 ) − 𝑀 ) = ( ( 𝑃 − 1 ) − 𝑀 ) )
409	160	adantr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → 𝑀 ∈ ℂ )
410	409 409	pncan2d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( 𝑀 + 𝑀 ) − 𝑀 ) = 𝑀 )
411	408 410	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( 𝑃 − 1 ) − 𝑀 ) = 𝑀 )
412	411 334	eqbrtrd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( 𝑃 − 1 ) − 𝑀 ) < ( 2 · 𝑢 ) )
413	338 322 22 412	ltsub23d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( 𝑃 − 1 ) − ( 2 · 𝑢 ) ) < 𝑀 )
414	401 413	eqbrtrd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( 𝑃 − ( 2 · 𝑢 ) ) − 1 ) < 𝑀 )
415	125	adantr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → 𝑀 ∈ ℕ )
416	415	nnzd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → 𝑀 ∈ ℤ )
417		zlem1lt	⊢ ( ( ( 𝑃 − ( 2 · 𝑢 ) ) ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( 𝑃 − ( 2 · 𝑢 ) ) ≤ 𝑀 ↔ ( ( 𝑃 − ( 2 · 𝑢 ) ) − 1 ) < 𝑀 ) )
418	388 416 417	syl2anc	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( 𝑃 − ( 2 · 𝑢 ) ) ≤ 𝑀 ↔ ( ( 𝑃 − ( 2 · 𝑢 ) ) − 1 ) < 𝑀 ) )
419	414 418	mpbird	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( 𝑃 − ( 2 · 𝑢 ) ) ≤ 𝑀 )
420		fznn	⊢ ( 𝑀 ∈ ℤ → ( ( 𝑃 − ( 2 · 𝑢 ) ) ∈ ( 1 ... 𝑀 ) ↔ ( ( 𝑃 − ( 2 · 𝑢 ) ) ∈ ℕ ∧ ( 𝑃 − ( 2 · 𝑢 ) ) ≤ 𝑀 ) ) )
421	416 420	syl	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( 𝑃 − ( 2 · 𝑢 ) ) ∈ ( 1 ... 𝑀 ) ↔ ( ( 𝑃 − ( 2 · 𝑢 ) ) ∈ ℕ ∧ ( 𝑃 − ( 2 · 𝑢 ) ) ≤ 𝑀 ) ) )
422	400 419 421	mpbir2and	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( 𝑃 − ( 2 · 𝑢 ) ) ∈ ( 1 ... 𝑀 ) )
423	422	adantr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) ∧ 𝑥 = ( 𝑃 − ( 2 · 𝑢 ) ) ) → ( 𝑃 − ( 2 · 𝑢 ) ) ∈ ( 1 ... 𝑀 ) )
424	387 423	eqeltrd	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) ∧ 𝑥 = ( 𝑃 − ( 2 · 𝑢 ) ) ) → 𝑥 ∈ ( 1 ... 𝑀 ) )
425	424	biantrurd	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) ∧ 𝑥 = ( 𝑃 − ( 2 · 𝑢 ) ) ) → ( 𝑦 ∈ ( 1 ... 𝑁 ) ↔ ( 𝑥 ∈ ( 1 ... 𝑀 ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) ) )
426	365	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) ∧ 𝑥 = ( 𝑃 − ( 2 · 𝑢 ) ) ) → 𝑁 ∈ ℤ )
427		fznn	⊢ ( 𝑁 ∈ ℤ → ( 𝑦 ∈ ( 1 ... 𝑁 ) ↔ ( 𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁 ) ) )
428	426 427	syl	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) ∧ 𝑥 = ( 𝑃 − ( 2 · 𝑢 ) ) ) → ( 𝑦 ∈ ( 1 ... 𝑁 ) ↔ ( 𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁 ) ) )
429	425 428	bitr3d	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) ∧ 𝑥 = ( 𝑃 − ( 2 · 𝑢 ) ) ) → ( ( 𝑥 ∈ ( 1 ... 𝑀 ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) ↔ ( 𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁 ) ) )
430	387	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) ∧ 𝑥 = ( 𝑃 − ( 2 · 𝑢 ) ) ) → ( 𝑥 · 𝑄 ) = ( ( 𝑃 − ( 2 · 𝑢 ) ) · 𝑄 ) )
431	430	breq2d	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) ∧ 𝑥 = ( 𝑃 − ( 2 · 𝑢 ) ) ) → ( ( 𝑦 · 𝑃 ) < ( 𝑥 · 𝑄 ) ↔ ( 𝑦 · 𝑃 ) < ( ( 𝑃 − ( 2 · 𝑢 ) ) · 𝑄 ) ) )
432	429 431	anbi12d	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) ∧ 𝑥 = ( 𝑃 − ( 2 · 𝑢 ) ) ) → ( ( ( 𝑥 ∈ ( 1 ... 𝑀 ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑦 · 𝑃 ) < ( 𝑥 · 𝑄 ) ) ↔ ( ( 𝑦 ∈ ℕ ∧ 𝑦 ≤ 𝑁 ) ∧ ( 𝑦 · 𝑃 ) < ( ( 𝑃 − ( 2 · 𝑢 ) ) · 𝑄 ) ) ) )
433	374	adantr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) ∧ 𝑥 = ( 𝑃 − ( 2 · 𝑢 ) ) ) → ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ∈ ℤ )
434		fznn	⊢ ( ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ∈ ℤ → ( 𝑦 ∈ ( 1 ... ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) ↔ ( 𝑦 ∈ ℕ ∧ 𝑦 ≤ ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) ) )
435	433 434	syl	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) ∧ 𝑥 = ( 𝑃 − ( 2 · 𝑢 ) ) ) → ( 𝑦 ∈ ( 1 ... ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) ↔ ( 𝑦 ∈ ℕ ∧ 𝑦 ≤ ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) ) )
436	386 432 435	3bitr4d	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) ∧ 𝑥 = ( 𝑃 − ( 2 · 𝑢 ) ) ) → ( ( ( 𝑥 ∈ ( 1 ... 𝑀 ) ∧ 𝑦 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑦 · 𝑃 ) < ( 𝑥 · 𝑄 ) ) ↔ 𝑦 ∈ ( 1 ... ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) ) )
437	233 436	bitrid	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) ∧ 𝑥 = ( 𝑃 − ( 2 · 𝑢 ) ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑆 ↔ 𝑦 ∈ ( 1 ... ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) ) )
438	437	pm5.32da	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( 𝑥 = ( 𝑃 − ( 2 · 𝑢 ) ) ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑆 ) ↔ ( 𝑥 = ( 𝑃 − ( 2 · 𝑢 ) ) ∧ 𝑦 ∈ ( 1 ... ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) ) ) )
439		vex	⊢ 𝑥 ∈ V
440		vex	⊢ 𝑦 ∈ V
441	439 440	op1std	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 1^st ‘ 𝑧 ) = 𝑥 )
442	441	eqeq1d	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 1^st ‘ 𝑧 ) = ( 𝑃 − ( 2 · 𝑢 ) ) ↔ 𝑥 = ( 𝑃 − ( 2 · 𝑢 ) ) ) )
443	442	elrab	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { 𝑧 ∈ 𝑆 ∣ ( 1^st ‘ 𝑧 ) = ( 𝑃 − ( 2 · 𝑢 ) ) } ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑆 ∧ 𝑥 = ( 𝑃 − ( 2 · 𝑢 ) ) ) )
444	443	biancomi	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { 𝑧 ∈ 𝑆 ∣ ( 1^st ‘ 𝑧 ) = ( 𝑃 − ( 2 · 𝑢 ) ) } ↔ ( 𝑥 = ( 𝑃 − ( 2 · 𝑢 ) ) ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑆 ) )
445		opelxp	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( { ( 𝑃 − ( 2 · 𝑢 ) ) } × ( 1 ... ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) ) ↔ ( 𝑥 ∈ { ( 𝑃 − ( 2 · 𝑢 ) ) } ∧ 𝑦 ∈ ( 1 ... ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) ) )
446		velsn	⊢ ( 𝑥 ∈ { ( 𝑃 − ( 2 · 𝑢 ) ) } ↔ 𝑥 = ( 𝑃 − ( 2 · 𝑢 ) ) )
447	446	anbi1i	⊢ ( ( 𝑥 ∈ { ( 𝑃 − ( 2 · 𝑢 ) ) } ∧ 𝑦 ∈ ( 1 ... ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) ) ↔ ( 𝑥 = ( 𝑃 − ( 2 · 𝑢 ) ) ∧ 𝑦 ∈ ( 1 ... ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) ) )
448	445 447	bitri	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( { ( 𝑃 − ( 2 · 𝑢 ) ) } × ( 1 ... ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) ) ↔ ( 𝑥 = ( 𝑃 − ( 2 · 𝑢 ) ) ∧ 𝑦 ∈ ( 1 ... ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) ) )
449	438 444 448	3bitr4g	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { 𝑧 ∈ 𝑆 ∣ ( 1^st ‘ 𝑧 ) = ( 𝑃 − ( 2 · 𝑢 ) ) } ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( { ( 𝑃 − ( 2 · 𝑢 ) ) } × ( 1 ... ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) ) ) )
450	229 230 449	eqrelrdv	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → { 𝑧 ∈ 𝑆 ∣ ( 1^st ‘ 𝑧 ) = ( 𝑃 − ( 2 · 𝑢 ) ) } = ( { ( 𝑃 − ( 2 · 𝑢 ) ) } × ( 1 ... ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) ) )
451	450	fveq2d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ( 1^st ‘ 𝑧 ) = ( 𝑃 − ( 2 · 𝑢 ) ) } ) = ( ♯ ‘ ( { ( 𝑃 − ( 2 · 𝑢 ) ) } × ( 1 ... ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) ) ) )
452		fzfid	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( 1 ... ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) ∈ Fin )
453		xpsnen2g	⊢ ( ( ( 𝑃 − ( 2 · 𝑢 ) ) ∈ ℤ ∧ ( 1 ... ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) ∈ Fin ) → ( { ( 𝑃 − ( 2 · 𝑢 ) ) } × ( 1 ... ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) ) ≈ ( 1 ... ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) )
454	388 452 453	syl2anc	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( { ( 𝑃 − ( 2 · 𝑢 ) ) } × ( 1 ... ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) ) ≈ ( 1 ... ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) )
455		hasheni	⊢ ( ( { ( 𝑃 − ( 2 · 𝑢 ) ) } × ( 1 ... ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) ) ≈ ( 1 ... ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) → ( ♯ ‘ ( { ( 𝑃 − ( 2 · 𝑢 ) ) } × ( 1 ... ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) ) ) = ( ♯ ‘ ( 1 ... ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) ) )
456	454 455	syl	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ♯ ‘ ( { ( 𝑃 − ( 2 · 𝑢 ) ) } × ( 1 ... ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) ) ) = ( ♯ ‘ ( 1 ... ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) ) )
457		ltmul2	⊢ ( ( ( 2 · 𝑢 ) ∈ ℝ ∧ 𝑃 ∈ ℝ ∧ ( 𝑄 ∈ ℝ ∧ 0 < 𝑄 ) ) → ( ( 2 · 𝑢 ) < 𝑃 ↔ ( 𝑄 · ( 2 · 𝑢 ) ) < ( 𝑄 · 𝑃 ) ) )
458	22 336 243 352 457	syl112anc	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( 2 · 𝑢 ) < 𝑃 ↔ ( 𝑄 · ( 2 · 𝑢 ) ) < ( 𝑄 · 𝑃 ) ) )
459	396 458	mpbid	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( 𝑄 · ( 2 · 𝑢 ) ) < ( 𝑄 · 𝑃 ) )
460		ltdivmul2	⊢ ( ( ( 𝑄 · ( 2 · 𝑢 ) ) ∈ ℝ ∧ 𝑄 ∈ ℝ ∧ ( 𝑃 ∈ ℝ ∧ 0 < 𝑃 ) ) → ( ( ( 𝑄 · ( 2 · 𝑢 ) ) / 𝑃 ) < 𝑄 ↔ ( 𝑄 · ( 2 · 𝑢 ) ) < ( 𝑄 · 𝑃 ) ) )
461	357 243 336 358 460	syl112anc	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( ( 𝑄 · ( 2 · 𝑢 ) ) / 𝑃 ) < 𝑄 ↔ ( 𝑄 · ( 2 · 𝑢 ) ) < ( 𝑄 · 𝑃 ) ) )
462	459 461	mpbird	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( 𝑄 · ( 2 · 𝑢 ) ) / 𝑃 ) < 𝑄 )
463	362 462	eqbrtrrd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) < 𝑄 )
464		fllt	⊢ ( ( ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ∈ ℝ ∧ 𝑄 ∈ ℤ ) → ( ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) < 𝑄 ↔ ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) < 𝑄 ) )
465	23 271 464	syl2anc	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) < 𝑄 ↔ ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) < 𝑄 ) )
466	463 465	mpbid	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) < 𝑄 )
467		zltlem1	⊢ ( ( ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ∈ ℤ ∧ 𝑄 ∈ ℤ ) → ( ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) < 𝑄 ↔ ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ≤ ( 𝑄 − 1 ) ) )
468	24 271 467	syl2anc	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) < 𝑄 ↔ ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ≤ ( 𝑄 − 1 ) ) )
469	466 468	mpbid	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ≤ ( 𝑄 − 1 ) )
470	469 288	breqtrrd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ≤ ( 2 · 𝑁 ) )
471		eluz2	⊢ ( ( 2 · 𝑁 ) ∈ ( ℤ_≥ ‘ ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ↔ ( ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ∈ ℤ ∧ ( 2 · 𝑁 ) ∈ ℤ ∧ ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ≤ ( 2 · 𝑁 ) ) )
472	24 373 470 471	syl3anbrc	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( 2 · 𝑁 ) ∈ ( ℤ_≥ ‘ ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) )
473		uznn0sub	⊢ ( ( 2 · 𝑁 ) ∈ ( ℤ_≥ ‘ ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) → ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ∈ ℕ₀ )
474		hashfz1	⊢ ( ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ∈ ℕ₀ → ( ♯ ‘ ( 1 ... ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) ) = ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) )
475	472 473 474	3syl	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ♯ ‘ ( 1 ... ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) ) = ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) )
476	451 456 475	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ( 1^st ‘ 𝑧 ) = ( 𝑃 − ( 2 · 𝑢 ) ) } ) = ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) )
477	476	sumeq2dv	⊢ ( 𝜑 → Σ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ( 1^st ‘ 𝑧 ) = ( 𝑃 − ( 2 · 𝑢 ) ) } ) = Σ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) )
478	83 226 477	3eqtr3rd	⊢ ( 𝜑 → Σ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) = ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1^st ‘ 𝑧 ) } ) )
479	302	nncnd	⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℂ )
480	479	adantr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) → ( 2 · 𝑁 ) ∈ ℂ )
481	11 480 291	fsumsub	⊢ ( 𝜑 → Σ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ( ( 2 · 𝑁 ) − ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) = ( Σ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ( 2 · 𝑁 ) − Σ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) )
482	478 481	eqtr3d	⊢ ( 𝜑 → ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1^st ‘ 𝑧 ) } ) = ( Σ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ( 2 · 𝑁 ) − Σ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) )
483	482	oveq2d	⊢ ( 𝜑 → ( Σ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) + ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1^st ‘ 𝑧 ) } ) ) = ( Σ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) + ( Σ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ( 2 · 𝑁 ) − Σ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) )
484	25	zcnd	⊢ ( 𝜑 → Σ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ∈ ℂ )
485	11 373	fsumzcl	⊢ ( 𝜑 → Σ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ( 2 · 𝑁 ) ∈ ℤ )
486	485	zcnd	⊢ ( 𝜑 → Σ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ( 2 · 𝑁 ) ∈ ℂ )
487	484 486	pncan3d	⊢ ( 𝜑 → ( Σ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) + ( Σ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ( 2 · 𝑁 ) − Σ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) ) = Σ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ( 2 · 𝑁 ) )
488		fsumconst	⊢ ( ( ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ∈ Fin ∧ ( 2 · 𝑁 ) ∈ ℂ ) → Σ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ( 2 · 𝑁 ) = ( ( ♯ ‘ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) · ( 2 · 𝑁 ) ) )
489	11 479 488	syl2anc	⊢ ( 𝜑 → Σ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ( 2 · 𝑁 ) = ( ( ♯ ‘ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) · ( 2 · 𝑁 ) ) )
490		hashcl	⊢ ( ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ∈ Fin → ( ♯ ‘ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) ∈ ℕ₀ )
491	11 490	syl	⊢ ( 𝜑 → ( ♯ ‘ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) ∈ ℕ₀ )
492	491	nn0cnd	⊢ ( 𝜑 → ( ♯ ‘ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) ∈ ℂ )
493		2cnd	⊢ ( 𝜑 → 2 ∈ ℂ )
494	492 493 308	mul12d	⊢ ( 𝜑 → ( ( ♯ ‘ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) · ( 2 · 𝑁 ) ) = ( 2 · ( ( ♯ ‘ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) · 𝑁 ) ) )
495	489 494	eqtrd	⊢ ( 𝜑 → Σ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ( 2 · 𝑁 ) = ( 2 · ( ( ♯ ‘ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) · 𝑁 ) ) )
496	483 487 495	3eqtrd	⊢ ( 𝜑 → ( Σ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) + ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1^st ‘ 𝑧 ) } ) ) = ( 2 · ( ( ♯ ‘ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) · 𝑁 ) ) )
497	496	oveq2d	⊢ ( 𝜑 → ( - 1 ↑ ( Σ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) + ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1^st ‘ 𝑧 ) } ) ) ) = ( - 1 ↑ ( 2 · ( ( ♯ ‘ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) · 𝑁 ) ) ) )
498	17	a1i	⊢ ( 𝜑 → 2 ∈ ℤ )
499	491	nn0zd	⊢ ( 𝜑 → ( ♯ ‘ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) ∈ ℤ )
500	499 365	zmulcld	⊢ ( 𝜑 → ( ( ♯ ‘ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) · 𝑁 ) ∈ ℤ )
501		expmulz	⊢ ( ( ( - 1 ∈ ℂ ∧ - 1 ≠ 0 ) ∧ ( 2 ∈ ℤ ∧ ( ( ♯ ‘ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) · 𝑁 ) ∈ ℤ ) ) → ( - 1 ↑ ( 2 · ( ( ♯ ‘ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) · 𝑁 ) ) ) = ( ( - 1 ↑ 2 ) ↑ ( ( ♯ ‘ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) · 𝑁 ) ) )
502	8 10 498 500 501	syl22anc	⊢ ( 𝜑 → ( - 1 ↑ ( 2 · ( ( ♯ ‘ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) · 𝑁 ) ) ) = ( ( - 1 ↑ 2 ) ↑ ( ( ♯ ‘ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) · 𝑁 ) ) )
503		neg1sqe1	⊢ ( - 1 ↑ 2 ) = 1
504	503	oveq1i	⊢ ( ( - 1 ↑ 2 ) ↑ ( ( ♯ ‘ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) · 𝑁 ) ) = ( 1 ↑ ( ( ♯ ‘ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) · 𝑁 ) )
505		1exp	⊢ ( ( ( ♯ ‘ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) · 𝑁 ) ∈ ℤ → ( 1 ↑ ( ( ♯ ‘ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) · 𝑁 ) ) = 1 )
506	500 505	syl	⊢ ( 𝜑 → ( 1 ↑ ( ( ♯ ‘ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) · 𝑁 ) ) = 1 )
507	504 506	eqtrid	⊢ ( 𝜑 → ( ( - 1 ↑ 2 ) ↑ ( ( ♯ ‘ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ) · 𝑁 ) ) = 1 )
508	497 502 507	3eqtrd	⊢ ( 𝜑 → ( - 1 ↑ ( Σ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) + ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1^st ‘ 𝑧 ) } ) ) ) = 1 )
509	44 55 508	3eqtr4d	⊢ ( 𝜑 → ( ( - 1 ↑ ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1^st ‘ 𝑧 ) } ) ) · ( - 1 ↑ ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1^st ‘ 𝑧 ) } ) ) ) = ( - 1 ↑ ( Σ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) + ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1^st ‘ 𝑧 ) } ) ) ) )
510		expaddz	⊢ ( ( ( - 1 ∈ ℂ ∧ - 1 ≠ 0 ) ∧ ( Σ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ∈ ℤ ∧ ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1^st ‘ 𝑧 ) } ) ∈ ℤ ) ) → ( - 1 ↑ ( Σ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) + ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1^st ‘ 𝑧 ) } ) ) ) = ( ( - 1 ↑ Σ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) · ( - 1 ↑ ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1^st ‘ 𝑧 ) } ) ) ) )
511	8 10 25 42 510	syl22anc	⊢ ( 𝜑 → ( - 1 ↑ ( Σ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) + ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1^st ‘ 𝑧 ) } ) ) ) = ( ( - 1 ↑ Σ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) · ( - 1 ↑ ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1^st ‘ 𝑧 ) } ) ) ) )
512	509 511	eqtr2d	⊢ ( 𝜑 → ( ( - 1 ↑ Σ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) · ( - 1 ↑ ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1^st ‘ 𝑧 ) } ) ) ) = ( ( - 1 ↑ ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1^st ‘ 𝑧 ) } ) ) · ( - 1 ↑ ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1^st ‘ 𝑧 ) } ) ) ) )
513	26 41 41 43 512	mulcan2ad	⊢ ( 𝜑 → ( - 1 ↑ Σ 𝑢 ∈ ( ( ( ⌊ ‘ ( 𝑀 / 2 ) ) + 1 ) ... 𝑀 ) ( ⌊ ‘ ( ( 𝑄 / 𝑃 ) · ( 2 · 𝑢 ) ) ) ) = ( - 1 ↑ ( ♯ ‘ { 𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ ( 1^st ‘ 𝑧 ) } ) ) )

Metamath Proof Explorer

Theorem lgsquadlem1

Proof