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

Metamath Proof Explorer

Theorem lgsquadlem1

Proof