Theorem bposlem5

Description: Lemma for bpos . Bound the product of all small primes in the binomial coefficient. (Contributed by Mario Carneiro, 15-Mar-2014) (Proof shortened by AV, 15-Sep-2021)

	Ref	Expression
Hypotheses	bpos.1	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 5 ) )
	bpos.2	⊢ ( 𝜑 → ¬ ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ ( 2 · 𝑁 ) ) )
	bpos.3	⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ ( 𝑛 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) , 1 ) )
	bpos.4	⊢ 𝐾 = ( ⌊ ‘ ( ( 2 · 𝑁 ) / 3 ) )
	bpos.5	⊢ 𝑀 = ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) )
Assertion	bposlem5	⊢ ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ≤ ( ( 2 · 𝑁 ) ↑𝑐 ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) ) )

Proof

Step	Hyp	Ref	Expression
1		bpos.1	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 5 ) )
2		bpos.2	⊢ ( 𝜑 → ¬ ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ ( 2 · 𝑁 ) ) )
3		bpos.3	⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ ( 𝑛 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) , 1 ) )
4		bpos.4	⊢ 𝐾 = ( ⌊ ‘ ( ( 2 · 𝑁 ) / 3 ) )
5		bpos.5	⊢ 𝑀 = ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) )
6		id	⊢ ( 𝑛 ∈ ℙ → 𝑛 ∈ ℙ )
7		5nn	⊢ 5 ∈ ℕ
8		eluznn	⊢ ( ( 5 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 5 ) ) → 𝑁 ∈ ℕ )
9	7 1 8	sylancr	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
10	9	nnnn0d	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
11		fzctr	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ( 0 ... ( 2 · 𝑁 ) ) )
12		bccl2	⊢ ( 𝑁 ∈ ( 0 ... ( 2 · 𝑁 ) ) → ( ( 2 · 𝑁 ) C 𝑁 ) ∈ ℕ )
13	10 11 12	3syl	⊢ ( 𝜑 → ( ( 2 · 𝑁 ) C 𝑁 ) ∈ ℕ )
14		pccl	⊢ ( ( 𝑛 ∈ ℙ ∧ ( ( 2 · 𝑁 ) C 𝑁 ) ∈ ℕ ) → ( 𝑛 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℕ0 )
15	6 13 14	syl2anr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℙ ) → ( 𝑛 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℕ0 )
16	15	ralrimiva	⊢ ( 𝜑 → ∀ 𝑛 ∈ ℙ ( 𝑛 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℕ0 )
17	3 16	pcmptcl	⊢ ( 𝜑 → ( 𝐹 : ℕ ⟶ ℕ ∧ seq 1 ( · , 𝐹 ) : ℕ ⟶ ℕ ) )
18	17	simprd	⊢ ( 𝜑 → seq 1 ( · , 𝐹 ) : ℕ ⟶ ℕ )
19		3nn	⊢ 3 ∈ ℕ
20		2z	⊢ 2 ∈ ℤ
21	9	nnzd	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
22		zmulcl	⊢ ( ( 2 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 2 · 𝑁 ) ∈ ℤ )
23	20 21 22	sylancr	⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℤ )
24	23	zred	⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℝ )
25		2nn	⊢ 2 ∈ ℕ
26		nnmulcl	⊢ ( ( 2 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 2 · 𝑁 ) ∈ ℕ )
27	25 9 26	sylancr	⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℕ )
28	27	nnrpd	⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℝ+ )
29	28	rpge0d	⊢ ( 𝜑 → 0 ≤ ( 2 · 𝑁 ) )
30	24 29	resqrtcld	⊢ ( 𝜑 → ( √ ‘ ( 2 · 𝑁 ) ) ∈ ℝ )
31	30	flcld	⊢ ( 𝜑 → ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) ) ∈ ℤ )
32		sqrt9	⊢ ( √ ‘ 9 ) = 3
33		9re	⊢ 9 ∈ ℝ
34	33	a1i	⊢ ( 𝜑 → 9 ∈ ℝ )
35		10re	⊢ ; 1 0 ∈ ℝ
36	35	a1i	⊢ ( 𝜑 → ; 1 0 ∈ ℝ )
37		lep1	⊢ ( 9 ∈ ℝ → 9 ≤ ( 9 + 1 ) )
38	33 37	ax-mp	⊢ 9 ≤ ( 9 + 1 )
39		9p1e10	⊢ ( 9 + 1 ) = ; 1 0
40	38 39	breqtri	⊢ 9 ≤ ; 1 0
41	40	a1i	⊢ ( 𝜑 → 9 ≤ ; 1 0 )
42		5cn	⊢ 5 ∈ ℂ
43		2cn	⊢ 2 ∈ ℂ
44		5t2e10	⊢ ( 5 · 2 ) = ; 1 0
45	42 43 44	mulcomli	⊢ ( 2 · 5 ) = ; 1 0
46		eluzle	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) → 5 ≤ 𝑁 )
47	1 46	syl	⊢ ( 𝜑 → 5 ≤ 𝑁 )
48	9	nnred	⊢ ( 𝜑 → 𝑁 ∈ ℝ )
49		5re	⊢ 5 ∈ ℝ
50		2re	⊢ 2 ∈ ℝ
51		2pos	⊢ 0 < 2
52	50 51	pm3.2i	⊢ ( 2 ∈ ℝ ∧ 0 < 2 )
53		lemul2	⊢ ( ( 5 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( 5 ≤ 𝑁 ↔ ( 2 · 5 ) ≤ ( 2 · 𝑁 ) ) )
54	49 52 53	mp3an13	⊢ ( 𝑁 ∈ ℝ → ( 5 ≤ 𝑁 ↔ ( 2 · 5 ) ≤ ( 2 · 𝑁 ) ) )
55	48 54	syl	⊢ ( 𝜑 → ( 5 ≤ 𝑁 ↔ ( 2 · 5 ) ≤ ( 2 · 𝑁 ) ) )
56	47 55	mpbid	⊢ ( 𝜑 → ( 2 · 5 ) ≤ ( 2 · 𝑁 ) )
57	45 56	eqbrtrrid	⊢ ( 𝜑 → ; 1 0 ≤ ( 2 · 𝑁 ) )
58	34 36 24 41 57	letrd	⊢ ( 𝜑 → 9 ≤ ( 2 · 𝑁 ) )
59		0re	⊢ 0 ∈ ℝ
60		9pos	⊢ 0 < 9
61	59 33 60	ltleii	⊢ 0 ≤ 9
62	33 61	pm3.2i	⊢ ( 9 ∈ ℝ ∧ 0 ≤ 9 )
63	24 29	jca	⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ∈ ℝ ∧ 0 ≤ ( 2 · 𝑁 ) ) )
64		sqrtle	⊢ ( ( ( 9 ∈ ℝ ∧ 0 ≤ 9 ) ∧ ( ( 2 · 𝑁 ) ∈ ℝ ∧ 0 ≤ ( 2 · 𝑁 ) ) ) → ( 9 ≤ ( 2 · 𝑁 ) ↔ ( √ ‘ 9 ) ≤ ( √ ‘ ( 2 · 𝑁 ) ) ) )
65	62 63 64	sylancr	⊢ ( 𝜑 → ( 9 ≤ ( 2 · 𝑁 ) ↔ ( √ ‘ 9 ) ≤ ( √ ‘ ( 2 · 𝑁 ) ) ) )
66	58 65	mpbid	⊢ ( 𝜑 → ( √ ‘ 9 ) ≤ ( √ ‘ ( 2 · 𝑁 ) ) )
67	32 66	eqbrtrrid	⊢ ( 𝜑 → 3 ≤ ( √ ‘ ( 2 · 𝑁 ) ) )
68		3z	⊢ 3 ∈ ℤ
69		flge	⊢ ( ( ( √ ‘ ( 2 · 𝑁 ) ) ∈ ℝ ∧ 3 ∈ ℤ ) → ( 3 ≤ ( √ ‘ ( 2 · 𝑁 ) ) ↔ 3 ≤ ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) ) ) )
70	30 68 69	sylancl	⊢ ( 𝜑 → ( 3 ≤ ( √ ‘ ( 2 · 𝑁 ) ) ↔ 3 ≤ ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) ) ) )
71	67 70	mpbid	⊢ ( 𝜑 → 3 ≤ ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) ) )
72	68	eluz1i	⊢ ( ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) ) ∈ ( ℤ≥ ‘ 3 ) ↔ ( ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) ) ∈ ℤ ∧ 3 ≤ ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) ) ) )
73	31 71 72	sylanbrc	⊢ ( 𝜑 → ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) ) ∈ ( ℤ≥ ‘ 3 ) )
74	5 73	eqeltrid	⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 3 ) )
75		eluznn	⊢ ( ( 3 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 3 ) ) → 𝑀 ∈ ℕ )
76	19 74 75	sylancr	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
77	18 76	ffvelcdmd	⊢ ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ∈ ℕ )
78	77	nnred	⊢ ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ∈ ℝ )
79	76	nnred	⊢ ( 𝜑 → 𝑀 ∈ ℝ )
80		ppicl	⊢ ( 𝑀 ∈ ℝ → ( π ‘ 𝑀 ) ∈ ℕ0 )
81	79 80	syl	⊢ ( 𝜑 → ( π ‘ 𝑀 ) ∈ ℕ0 )
82	27 81	nnexpcld	⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑀 ) ) ∈ ℕ )
83	82	nnred	⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑀 ) ) ∈ ℝ )
84		nndivre	⊢ ( ( ( √ ‘ ( 2 · 𝑁 ) ) ∈ ℝ ∧ 3 ∈ ℕ ) → ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) ∈ ℝ )
85	30 19 84	sylancl	⊢ ( 𝜑 → ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) ∈ ℝ )
86		readdcl	⊢ ( ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) ∈ ℝ ∧ 2 ∈ ℝ ) → ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) ∈ ℝ )
87	85 50 86	sylancl	⊢ ( 𝜑 → ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) ∈ ℝ )
88	24 29 87	recxpcld	⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ↑𝑐 ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) ) ∈ ℝ )
89		fveq2	⊢ ( 𝑥 = 1 → ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) = ( seq 1 ( · , 𝐹 ) ‘ 1 ) )
90		fveq2	⊢ ( 𝑥 = 1 → ( π ‘ 𝑥 ) = ( π ‘ 1 ) )
91		ppi1	⊢ ( π ‘ 1 ) = 0
92	90 91	eqtrdi	⊢ ( 𝑥 = 1 → ( π ‘ 𝑥 ) = 0 )
93	92	oveq2d	⊢ ( 𝑥 = 1 → ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑥 ) ) = ( ( 2 · 𝑁 ) ↑ 0 ) )
94	89 93	breq12d	⊢ ( 𝑥 = 1 → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑥 ) ) ↔ ( seq 1 ( · , 𝐹 ) ‘ 1 ) ≤ ( ( 2 · 𝑁 ) ↑ 0 ) ) )
95	94	imbi2d	⊢ ( 𝑥 = 1 → ( ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑥 ) ) ) ↔ ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 1 ) ≤ ( ( 2 · 𝑁 ) ↑ 0 ) ) ) )
96		fveq2	⊢ ( 𝑥 = 𝑘 → ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) = ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) )
97		fveq2	⊢ ( 𝑥 = 𝑘 → ( π ‘ 𝑥 ) = ( π ‘ 𝑘 ) )
98	97	oveq2d	⊢ ( 𝑥 = 𝑘 → ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑥 ) ) = ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑘 ) ) )
99	96 98	breq12d	⊢ ( 𝑥 = 𝑘 → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑥 ) ) ↔ ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑘 ) ) ) )
100	99	imbi2d	⊢ ( 𝑥 = 𝑘 → ( ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑥 ) ) ) ↔ ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑘 ) ) ) ) )
101		fveq2	⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) = ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) )
102		fveq2	⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( π ‘ 𝑥 ) = ( π ‘ ( 𝑘 + 1 ) ) )
103	102	oveq2d	⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑥 ) ) = ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) )
104	101 103	breq12d	⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑥 ) ) ↔ ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ) )
105	104	imbi2d	⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑥 ) ) ) ↔ ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ) ) )
106		fveq2	⊢ ( 𝑥 = 𝑀 → ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) = ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) )
107		fveq2	⊢ ( 𝑥 = 𝑀 → ( π ‘ 𝑥 ) = ( π ‘ 𝑀 ) )
108	107	oveq2d	⊢ ( 𝑥 = 𝑀 → ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑥 ) ) = ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑀 ) ) )
109	106 108	breq12d	⊢ ( 𝑥 = 𝑀 → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑥 ) ) ↔ ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑀 ) ) ) )
110	109	imbi2d	⊢ ( 𝑥 = 𝑀 → ( ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑥 ) ) ) ↔ ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑀 ) ) ) ) )
111		1z	⊢ 1 ∈ ℤ
112		seq1	⊢ ( 1 ∈ ℤ → ( seq 1 ( · , 𝐹 ) ‘ 1 ) = ( 𝐹 ‘ 1 ) )
113	111 112	ax-mp	⊢ ( seq 1 ( · , 𝐹 ) ‘ 1 ) = ( 𝐹 ‘ 1 )
114		1nn	⊢ 1 ∈ ℕ
115		1nprm	⊢ ¬ 1 ∈ ℙ
116		eleq1	⊢ ( 𝑛 = 1 → ( 𝑛 ∈ ℙ ↔ 1 ∈ ℙ ) )
117	115 116	mtbiri	⊢ ( 𝑛 = 1 → ¬ 𝑛 ∈ ℙ )
118	117	iffalsed	⊢ ( 𝑛 = 1 → if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ ( 𝑛 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) , 1 ) = 1 )
119		1ex	⊢ 1 ∈ V
120	118 3 119	fvmpt	⊢ ( 1 ∈ ℕ → ( 𝐹 ‘ 1 ) = 1 )
121	114 120	ax-mp	⊢ ( 𝐹 ‘ 1 ) = 1
122	113 121	eqtri	⊢ ( seq 1 ( · , 𝐹 ) ‘ 1 ) = 1
123		1le1	⊢ 1 ≤ 1
124	122 123	eqbrtri	⊢ ( seq 1 ( · , 𝐹 ) ‘ 1 ) ≤ 1
125	23	zcnd	⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℂ )
126	125	exp0d	⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ↑ 0 ) = 1 )
127	124 126	breqtrrid	⊢ ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 1 ) ≤ ( ( 2 · 𝑁 ) ↑ 0 ) )
128	18	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ∈ ℕ )
129	128	nnred	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ∈ ℝ )
130	129	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ∈ ℝ )
131	27	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( 2 · 𝑁 ) ∈ ℕ )
132		nnre	⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℝ )
133	132	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → 𝑘 ∈ ℝ )
134		ppicl	⊢ ( 𝑘 ∈ ℝ → ( π ‘ 𝑘 ) ∈ ℕ0 )
135	133 134	syl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( π ‘ 𝑘 ) ∈ ℕ0 )
136	131 135	nnexpcld	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑘 ) ) ∈ ℕ )
137	136	nnred	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑘 ) ) ∈ ℝ )
138		nnre	⊢ ( ( 2 · 𝑁 ) ∈ ℕ → ( 2 · 𝑁 ) ∈ ℝ )
139		nngt0	⊢ ( ( 2 · 𝑁 ) ∈ ℕ → 0 < ( 2 · 𝑁 ) )
140	138 139	jca	⊢ ( ( 2 · 𝑁 ) ∈ ℕ → ( ( 2 · 𝑁 ) ∈ ℝ ∧ 0 < ( 2 · 𝑁 ) ) )
141	27 140	syl	⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ∈ ℝ ∧ 0 < ( 2 · 𝑁 ) ) )
142	141	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( 2 · 𝑁 ) ∈ ℝ ∧ 0 < ( 2 · 𝑁 ) ) )
143		lemul1	⊢ ( ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ∈ ℝ ∧ ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑘 ) ) ∈ ℝ ∧ ( ( 2 · 𝑁 ) ∈ ℝ ∧ 0 < ( 2 · 𝑁 ) ) ) → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑘 ) ) ↔ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) ≤ ( ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑘 ) ) · ( 2 · 𝑁 ) ) ) )
144	130 137 142 143	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑘 ) ) ↔ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) ≤ ( ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑘 ) ) · ( 2 · 𝑁 ) ) ) )
145		nnz	⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℤ )
146	145	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℤ )
147		ppiprm	⊢ ( ( 𝑘 ∈ ℤ ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( π ‘ ( 𝑘 + 1 ) ) = ( ( π ‘ 𝑘 ) + 1 ) )
148	146 147	sylan	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( π ‘ ( 𝑘 + 1 ) ) = ( ( π ‘ 𝑘 ) + 1 ) )
149	148	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) = ( ( 2 · 𝑁 ) ↑ ( ( π ‘ 𝑘 ) + 1 ) ) )
150	125	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( 2 · 𝑁 ) ∈ ℂ )
151	150 135	expp1d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( 2 · 𝑁 ) ↑ ( ( π ‘ 𝑘 ) + 1 ) ) = ( ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑘 ) ) · ( 2 · 𝑁 ) ) )
152	149 151	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) = ( ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑘 ) ) · ( 2 · 𝑁 ) ) )
153	152	breq2d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ↔ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) ≤ ( ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑘 ) ) · ( 2 · 𝑁 ) ) ) )
154	144 153	bitr4d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑘 ) ) ↔ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ) )
155		simpr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℕ )
156		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
157	155 156	eleqtrdi	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ( ℤ≥ ‘ 1 ) )
158		seqp1	⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 1 ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) = ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
159	157 158	syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) = ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
160	159	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) = ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
161		peano2nn	⊢ ( 𝑘 ∈ ℕ → ( 𝑘 + 1 ) ∈ ℕ )
162	161	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑘 + 1 ) ∈ ℕ )
163		eleq1	⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( 𝑛 ∈ ℙ ↔ ( 𝑘 + 1 ) ∈ ℙ ) )
164		id	⊢ ( 𝑛 = ( 𝑘 + 1 ) → 𝑛 = ( 𝑘 + 1 ) )
165		oveq1	⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( 𝑛 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) = ( ( 𝑘 + 1 ) pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) )
166	164 165	oveq12d	⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( 𝑛 ↑ ( 𝑛 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) = ( ( 𝑘 + 1 ) ↑ ( ( 𝑘 + 1 ) pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) )
167	163 166	ifbieq1d	⊢ ( 𝑛 = ( 𝑘 + 1 ) → if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ ( 𝑛 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) , 1 ) = if ( ( 𝑘 + 1 ) ∈ ℙ , ( ( 𝑘 + 1 ) ↑ ( ( 𝑘 + 1 ) pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) , 1 ) )
168		ovex	⊢ ( ( 𝑘 + 1 ) ↑ ( ( 𝑘 + 1 ) pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) ∈ V
169	168 119	ifex	⊢ if ( ( 𝑘 + 1 ) ∈ ℙ , ( ( 𝑘 + 1 ) ↑ ( ( 𝑘 + 1 ) pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) , 1 ) ∈ V
170	167 3 169	fvmpt	⊢ ( ( 𝑘 + 1 ) ∈ ℕ → ( 𝐹 ‘ ( 𝑘 + 1 ) ) = if ( ( 𝑘 + 1 ) ∈ ℙ , ( ( 𝑘 + 1 ) ↑ ( ( 𝑘 + 1 ) pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) , 1 ) )
171	162 170	syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) = if ( ( 𝑘 + 1 ) ∈ ℙ , ( ( 𝑘 + 1 ) ↑ ( ( 𝑘 + 1 ) pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) , 1 ) )
172		iftrue	⊢ ( ( 𝑘 + 1 ) ∈ ℙ → if ( ( 𝑘 + 1 ) ∈ ℙ , ( ( 𝑘 + 1 ) ↑ ( ( 𝑘 + 1 ) pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) , 1 ) = ( ( 𝑘 + 1 ) ↑ ( ( 𝑘 + 1 ) pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) )
173	171 172	sylan9eq	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) = ( ( 𝑘 + 1 ) ↑ ( ( 𝑘 + 1 ) pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) )
174	9	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑁 ∈ ℕ )
175		bposlem1	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( 𝑘 + 1 ) ↑ ( ( 𝑘 + 1 ) pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) ≤ ( 2 · 𝑁 ) )
176	174 175	sylan	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( 𝑘 + 1 ) ↑ ( ( 𝑘 + 1 ) pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) ≤ ( 2 · 𝑁 ) )
177	173 176	eqbrtrd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤ ( 2 · 𝑁 ) )
178	17	simpld	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ℕ )
179		ffvelcdm	⊢ ( ( 𝐹 : ℕ ⟶ ℕ ∧ ( 𝑘 + 1 ) ∈ ℕ ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ ℕ )
180	178 161 179	syl2an	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ ℕ )
181	180	nnred	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ ℝ )
182	181	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ ℝ )
183	24	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( 2 · 𝑁 ) ∈ ℝ )
184		nnre	⊢ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ∈ ℕ → ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ∈ ℝ )
185		nngt0	⊢ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ∈ ℕ → 0 < ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) )
186	184 185	jca	⊢ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ∈ ℕ → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ∈ ℝ ∧ 0 < ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ) )
187	128 186	syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ∈ ℝ ∧ 0 < ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ) )
188	187	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ∈ ℝ ∧ 0 < ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ) )
189		lemul2	⊢ ( ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ ℝ ∧ ( 2 · 𝑁 ) ∈ ℝ ∧ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ∈ ℝ ∧ 0 < ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ) ) → ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤ ( 2 · 𝑁 ) ↔ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ≤ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) ) )
190	182 183 188 189	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤ ( 2 · 𝑁 ) ↔ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ≤ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) ) )
191	177 190	mpbid	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ≤ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) )
192	160 191	eqbrtrd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ≤ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) )
193		ffvelcdm	⊢ ( ( seq 1 ( · , 𝐹 ) : ℕ ⟶ ℕ ∧ ( 𝑘 + 1 ) ∈ ℕ ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ∈ ℕ )
194	18 161 193	syl2an	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ∈ ℕ )
195	194	nnred	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ∈ ℝ )
196	27	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 2 · 𝑁 ) ∈ ℕ )
197	128 196	nnmulcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) ∈ ℕ )
198	197	nnred	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) ∈ ℝ )
199	162	nnred	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑘 + 1 ) ∈ ℝ )
200		ppicl	⊢ ( ( 𝑘 + 1 ) ∈ ℝ → ( π ‘ ( 𝑘 + 1 ) ) ∈ ℕ0 )
201	199 200	syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( π ‘ ( 𝑘 + 1 ) ) ∈ ℕ0 )
202	196 201	nnexpcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ∈ ℕ )
203	202	nnred	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ∈ ℝ )
204		letr	⊢ ( ( ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ∈ ℝ ∧ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) ∈ ℝ ∧ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ∈ ℝ ) → ( ( ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ≤ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) ∧ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ) )
205	195 198 203 204	syl3anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ≤ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) ∧ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ) )
206	205	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ≤ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) ∧ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ) )
207	192 206	mpand	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ) )
208	154 207	sylbid	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑘 ) ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ) )
209	159	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ¬ ( 𝑘 + 1 ) ∈ ℙ ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) = ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
210		iffalse	⊢ ( ¬ ( 𝑘 + 1 ) ∈ ℙ → if ( ( 𝑘 + 1 ) ∈ ℙ , ( ( 𝑘 + 1 ) ↑ ( ( 𝑘 + 1 ) pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) , 1 ) = 1 )
211	171 210	sylan9eq	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ¬ ( 𝑘 + 1 ) ∈ ℙ ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) = 1 )
212	211	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ¬ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) = ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · 1 ) )
213	128	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ¬ ( 𝑘 + 1 ) ∈ ℙ ) → ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ∈ ℕ )
214	213	nncnd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ¬ ( 𝑘 + 1 ) ∈ ℙ ) → ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ∈ ℂ )
215	214	mulridd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ¬ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · 1 ) = ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) )
216	209 212 215	3eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ¬ ( 𝑘 + 1 ) ∈ ℙ ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) = ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) )
217		ppinprm	⊢ ( ( 𝑘 ∈ ℤ ∧ ¬ ( 𝑘 + 1 ) ∈ ℙ ) → ( π ‘ ( 𝑘 + 1 ) ) = ( π ‘ 𝑘 ) )
218	146 217	sylan	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ¬ ( 𝑘 + 1 ) ∈ ℙ ) → ( π ‘ ( 𝑘 + 1 ) ) = ( π ‘ 𝑘 ) )
219	218	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ¬ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) = ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑘 ) ) )
220	216 219	breq12d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ¬ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ↔ ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑘 ) ) ) )
221	220	biimprd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ¬ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑘 ) ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ) )
222	208 221	pm2.61dan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑘 ) ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ) )
223	222	expcom	⊢ ( 𝑘 ∈ ℕ → ( 𝜑 → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑘 ) ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ) ) )
224	223	a2d	⊢ ( 𝑘 ∈ ℕ → ( ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑘 ) ) ) → ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ) ) )
225	95 100 105 110 127 224	nnind	⊢ ( 𝑀 ∈ ℕ → ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑀 ) ) ) )
226	76 225	mpcom	⊢ ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑀 ) ) )
227		cxpexp	⊢ ( ( ( 2 · 𝑁 ) ∈ ℂ ∧ ( π ‘ 𝑀 ) ∈ ℕ0 ) → ( ( 2 · 𝑁 ) ↑𝑐 ( π ‘ 𝑀 ) ) = ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑀 ) ) )
228	125 81 227	syl2anc	⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ↑𝑐 ( π ‘ 𝑀 ) ) = ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑀 ) ) )
229	81	nn0red	⊢ ( 𝜑 → ( π ‘ 𝑀 ) ∈ ℝ )
230		nndivre	⊢ ( ( 𝑀 ∈ ℝ ∧ 3 ∈ ℕ ) → ( 𝑀 / 3 ) ∈ ℝ )
231	79 19 230	sylancl	⊢ ( 𝜑 → ( 𝑀 / 3 ) ∈ ℝ )
232		readdcl	⊢ ( ( ( 𝑀 / 3 ) ∈ ℝ ∧ 2 ∈ ℝ ) → ( ( 𝑀 / 3 ) + 2 ) ∈ ℝ )
233	231 50 232	sylancl	⊢ ( 𝜑 → ( ( 𝑀 / 3 ) + 2 ) ∈ ℝ )
234	76	nnnn0d	⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
235	234	nn0ge0d	⊢ ( 𝜑 → 0 ≤ 𝑀 )
236		ppiub	⊢ ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) → ( π ‘ 𝑀 ) ≤ ( ( 𝑀 / 3 ) + 2 ) )
237	79 235 236	syl2anc	⊢ ( 𝜑 → ( π ‘ 𝑀 ) ≤ ( ( 𝑀 / 3 ) + 2 ) )
238	50	a1i	⊢ ( 𝜑 → 2 ∈ ℝ )
239		flle	⊢ ( ( √ ‘ ( 2 · 𝑁 ) ) ∈ ℝ → ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) ) ≤ ( √ ‘ ( 2 · 𝑁 ) ) )
240	30 239	syl	⊢ ( 𝜑 → ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) ) ≤ ( √ ‘ ( 2 · 𝑁 ) ) )
241	5 240	eqbrtrid	⊢ ( 𝜑 → 𝑀 ≤ ( √ ‘ ( 2 · 𝑁 ) ) )
242		3re	⊢ 3 ∈ ℝ
243		3pos	⊢ 0 < 3
244	242 243	pm3.2i	⊢ ( 3 ∈ ℝ ∧ 0 < 3 )
245	244	a1i	⊢ ( 𝜑 → ( 3 ∈ ℝ ∧ 0 < 3 ) )
246		lediv1	⊢ ( ( 𝑀 ∈ ℝ ∧ ( √ ‘ ( 2 · 𝑁 ) ) ∈ ℝ ∧ ( 3 ∈ ℝ ∧ 0 < 3 ) ) → ( 𝑀 ≤ ( √ ‘ ( 2 · 𝑁 ) ) ↔ ( 𝑀 / 3 ) ≤ ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) ) )
247	79 30 245 246	syl3anc	⊢ ( 𝜑 → ( 𝑀 ≤ ( √ ‘ ( 2 · 𝑁 ) ) ↔ ( 𝑀 / 3 ) ≤ ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) ) )
248	241 247	mpbid	⊢ ( 𝜑 → ( 𝑀 / 3 ) ≤ ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) )
249	231 85 238 248	leadd1dd	⊢ ( 𝜑 → ( ( 𝑀 / 3 ) + 2 ) ≤ ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) )
250	229 233 87 237 249	letrd	⊢ ( 𝜑 → ( π ‘ 𝑀 ) ≤ ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) )
251		2t1e2	⊢ ( 2 · 1 ) = 2
252	9	nnge1d	⊢ ( 𝜑 → 1 ≤ 𝑁 )
253		1re	⊢ 1 ∈ ℝ
254		lemul2	⊢ ( ( 1 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( 1 ≤ 𝑁 ↔ ( 2 · 1 ) ≤ ( 2 · 𝑁 ) ) )
255	253 52 254	mp3an13	⊢ ( 𝑁 ∈ ℝ → ( 1 ≤ 𝑁 ↔ ( 2 · 1 ) ≤ ( 2 · 𝑁 ) ) )
256	48 255	syl	⊢ ( 𝜑 → ( 1 ≤ 𝑁 ↔ ( 2 · 1 ) ≤ ( 2 · 𝑁 ) ) )
257	252 256	mpbid	⊢ ( 𝜑 → ( 2 · 1 ) ≤ ( 2 · 𝑁 ) )
258	251 257	eqbrtrrid	⊢ ( 𝜑 → 2 ≤ ( 2 · 𝑁 ) )
259	20	eluz1i	⊢ ( ( 2 · 𝑁 ) ∈ ( ℤ≥ ‘ 2 ) ↔ ( ( 2 · 𝑁 ) ∈ ℤ ∧ 2 ≤ ( 2 · 𝑁 ) ) )
260	23 258 259	sylanbrc	⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ( ℤ≥ ‘ 2 ) )
261		eluz2gt1	⊢ ( ( 2 · 𝑁 ) ∈ ( ℤ≥ ‘ 2 ) → 1 < ( 2 · 𝑁 ) )
262	260 261	syl	⊢ ( 𝜑 → 1 < ( 2 · 𝑁 ) )
263	24 262 229 87	cxpled	⊢ ( 𝜑 → ( ( π ‘ 𝑀 ) ≤ ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) ↔ ( ( 2 · 𝑁 ) ↑𝑐 ( π ‘ 𝑀 ) ) ≤ ( ( 2 · 𝑁 ) ↑𝑐 ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) ) ) )
264	250 263	mpbid	⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ↑𝑐 ( π ‘ 𝑀 ) ) ≤ ( ( 2 · 𝑁 ) ↑𝑐 ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) ) )
265	228 264	eqbrtrrd	⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑀 ) ) ≤ ( ( 2 · 𝑁 ) ↑𝑐 ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) ) )
266	78 83 88 226 265	letrd	⊢ ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ≤ ( ( 2 · 𝑁 ) ↑𝑐 ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) ) )