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	$⊢ φ \to N \in ℤ_{\geq 5}$
	bpos.2	$⊢ φ \to \neg \exists p \in ℙ (N < p \land p \leq 2 \cdot N)$
	bpos.3	$⊢ F = (n \in ℕ ⟼ if (n \in ℙ, n^{n pCnt (\binom{2 \cdot N}{N})}, 1))$
	bpos.4	$⊢ K = ⌊\frac{2 \cdot N}{3}⌋$
	bpos.5	$⊢ M = ⌊\sqrt{2 \cdot N}⌋$
Assertion	bposlem5	$⊢ φ \to seq 1 (\times F) (M) \leq {2 \cdot N}^{(\frac{\sqrt{2 \cdot N}}{3}) + 2}$

Proof

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

Metamath Proof Explorer

Theorem bposlem5

Proof