bposlem6

Description: Lemma for bpos . By using the various bounds at our disposal, arrive at an inequality that is false for N large enough. (Contributed by Mario Carneiro, 14-Mar-2014) (Revised by Wolf Lammen, 12-Sep-2020)

	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	bposlem6	$⊢ φ \to \frac{4^{N}}{N} < {2 \cdot N}^{(\frac{\sqrt{2 \cdot N}}{3}) + 2} 2^{(\frac{4 \cdot N}{3}) - 5}$

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		4nn	$⊢ 4 \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		nnexpcl	$⊢ (4 \in ℕ \land N \in ℕ_{0}) \to 4^{N} \in ℕ$
12	6 10 11	sylancr	$⊢ φ \to 4^{N} \in ℕ$
13	12	nnred	$⊢ φ \to 4^{N} \in ℝ$
14	13 9	nndivred	$⊢ φ \to \frac{4^{N}}{N} \in ℝ$
15		fzctr	$⊢ N \in ℕ_{0} \to N \in (0 \dots 2 \cdot N)$
16	10 15	syl	$⊢ φ \to N \in (0 \dots 2 \cdot N)$
17		bccl2	$⊢ N \in (0 \dots 2 \cdot N) \to (\binom{2 \cdot N}{N}) \in ℕ$
18	16 17	syl	$⊢ φ \to (\binom{2 \cdot N}{N}) \in ℕ$
19	18	nnred	$⊢ φ \to (\binom{2 \cdot N}{N}) \in ℝ$
20		2nn	$⊢ 2 \in ℕ$
21		nnmulcl	$⊢ (2 \in ℕ \land N \in ℕ) \to 2 \cdot N \in ℕ$
22	20 9 21	sylancr	$⊢ φ \to 2 \cdot N \in ℕ$
23	22	nnrpd	$⊢ φ \to 2 \cdot N \in ℝ^{+}$
24	22	nnred	$⊢ φ \to 2 \cdot N \in ℝ$
25	23	rpge0d	$⊢ φ \to 0 \leq 2 \cdot N$
26	24 25	resqrtcld	$⊢ φ \to \sqrt{2 \cdot N} \in ℝ$
27		3nn	$⊢ 3 \in ℕ$
28		nndivre	$⊢ (\sqrt{2 \cdot N} \in ℝ \land 3 \in ℕ) \to \frac{\sqrt{2 \cdot N}}{3} \in ℝ$
29	26 27 28	sylancl	$⊢ φ \to \frac{\sqrt{2 \cdot N}}{3} \in ℝ$
30		2re	$⊢ 2 \in ℝ$
31		readdcl	$⊢ (\frac{\sqrt{2 \cdot N}}{3} \in ℝ \land 2 \in ℝ) \to (\frac{\sqrt{2 \cdot N}}{3}) + 2 \in ℝ$
32	29 30 31	sylancl	$⊢ φ \to (\frac{\sqrt{2 \cdot N}}{3}) + 2 \in ℝ$
33	23 32	rpcxpcld	$⊢ φ \to {2 \cdot N}^{(\frac{\sqrt{2 \cdot N}}{3}) + 2} \in ℝ^{+}$
34	33	rpred	$⊢ φ \to {2 \cdot N}^{(\frac{\sqrt{2 \cdot N}}{3}) + 2} \in ℝ$
35		2rp	$⊢ 2 \in ℝ^{+}$
36		nnmulcl	$⊢ (4 \in ℕ \land N \in ℕ) \to 4 \cdot N \in ℕ$
37	6 9 36	sylancr	$⊢ φ \to 4 \cdot N \in ℕ$
38	37	nnred	$⊢ φ \to 4 \cdot N \in ℝ$
39		nndivre	$⊢ (4 \cdot N \in ℝ \land 3 \in ℕ) \to \frac{4 \cdot N}{3} \in ℝ$
40	38 27 39	sylancl	$⊢ φ \to \frac{4 \cdot N}{3} \in ℝ$
41		5re	$⊢ 5 \in ℝ$
42		resubcl	$⊢ (\frac{4 \cdot N}{3} \in ℝ \land 5 \in ℝ) \to (\frac{4 \cdot N}{3}) - 5 \in ℝ$
43	40 41 42	sylancl	$⊢ φ \to (\frac{4 \cdot N}{3}) - 5 \in ℝ$
44		rpcxpcl	$⊢ (2 \in ℝ^{+} \land (\frac{4 \cdot N}{3}) - 5 \in ℝ) \to 2^{(\frac{4 \cdot N}{3}) - 5} \in ℝ^{+}$
45	35 43 44	sylancr	$⊢ φ \to 2^{(\frac{4 \cdot N}{3}) - 5} \in ℝ^{+}$
46	45	rpred	$⊢ φ \to 2^{(\frac{4 \cdot N}{3}) - 5} \in ℝ$
47	34 46	remulcld	$⊢ φ \to {2 \cdot N}^{(\frac{\sqrt{2 \cdot N}}{3}) + 2} 2^{(\frac{4 \cdot N}{3}) - 5} \in ℝ$
48		df-5	$⊢ 5 = 4 + 1$
49		4z	$⊢ 4 \in ℤ$
50		uzid	$⊢ 4 \in ℤ \to 4 \in ℤ_{\geq 4}$
51		peano2uz	$⊢ 4 \in ℤ_{\geq 4} \to 4 + 1 \in ℤ_{\geq 4}$
52	49 50 51	mp2b	$⊢ 4 + 1 \in ℤ_{\geq 4}$
53	48 52	eqeltri	$⊢ 5 \in ℤ_{\geq 4}$
54		eqid	$⊢ ℤ_{\geq 4} = ℤ_{\geq 4}$
55	54	uztrn2	$⊢ (5 \in ℤ_{\geq 4} \land N \in ℤ_{\geq 5}) \to N \in ℤ_{\geq 4}$
56	53 1 55	sylancr	$⊢ φ \to N \in ℤ_{\geq 4}$
57		bclbnd	$⊢ N \in ℤ_{\geq 4} \to \frac{4^{N}}{N} < (\binom{2 \cdot N}{N})$
58	56 57	syl	$⊢ φ \to \frac{4^{N}}{N} < (\binom{2 \cdot N}{N})$
59		id	$⊢ n \in ℙ \to n \in ℙ$
60		pccl	$⊢ (n \in ℙ \land (\binom{2 \cdot N}{N}) \in ℕ) \to n pCnt (\binom{2 \cdot N}{N}) \in ℕ_{0}$
61	59 18 60	syl2anr	$⊢ (φ \land n \in ℙ) \to n pCnt (\binom{2 \cdot N}{N}) \in ℕ_{0}$
62	61	ralrimiva	$⊢ φ \to \forall n \in ℙ n pCnt (\binom{2 \cdot N}{N}) \in ℕ_{0}$
63	3 62	pcmptcl	$⊢ φ \to (F : ℕ ⟶ ℕ \land seq 1 (\times F) : ℕ ⟶ ℕ)$
64	63	simprd	$⊢ φ \to seq 1 (\times F) : ℕ ⟶ ℕ$
65	1 2 3 4 5	bposlem4	$⊢ φ \to M \in (3 \dots K)$
66		elfzuz	$⊢ M \in (3 \dots K) \to M \in ℤ_{\geq 3}$
67	65 66	syl	$⊢ φ \to M \in ℤ_{\geq 3}$
68		eluznn	$⊢ (3 \in ℕ \land M \in ℤ_{\geq 3}) \to M \in ℕ$
69	27 67 68	sylancr	$⊢ φ \to M \in ℕ$
70	64 69	ffvelcdmd	$⊢ φ \to seq 1 (\times F) (M) \in ℕ$
71	70	nnred	$⊢ φ \to seq 1 (\times F) (M) \in ℝ$
72		2z	$⊢ 2 \in ℤ$
73		nndivre	$⊢ (2 \cdot N \in ℝ \land 3 \in ℕ) \to \frac{2 \cdot N}{3} \in ℝ$
74	24 27 73	sylancl	$⊢ φ \to \frac{2 \cdot N}{3} \in ℝ$
75	74	flcld	$⊢ φ \to ⌊\frac{2 \cdot N}{3}⌋ \in ℤ$
76	4 75	eqeltrid	$⊢ φ \to K \in ℤ$
77		zmulcl	$⊢ (2 \in ℤ \land K \in ℤ) \to 2 K \in ℤ$
78	72 76 77	sylancr	$⊢ φ \to 2 K \in ℤ$
79	7	nnzi	$⊢ 5 \in ℤ$
80		zsubcl	$⊢ (2 K \in ℤ \land 5 \in ℤ) \to 2 K - 5 \in ℤ$
81	78 79 80	sylancl	$⊢ φ \to 2 K - 5 \in ℤ$
82	81	zred	$⊢ φ \to 2 K - 5 \in ℝ$
83		rpcxpcl	$⊢ (2 \in ℝ^{+} \land 2 K - 5 \in ℝ) \to 2^{2 K - 5} \in ℝ^{+}$
84	35 82 83	sylancr	$⊢ φ \to 2^{2 K - 5} \in ℝ^{+}$
85	84	rpred	$⊢ φ \to 2^{2 K - 5} \in ℝ$
86	71 85	remulcld	$⊢ φ \to seq 1 (\times F) (M) 2^{2 K - 5} \in ℝ$
87	1 2 3 4	bposlem3	$⊢ φ \to seq 1 (\times F) (K) = (\binom{2 \cdot N}{N})$
88		elfzuz3	$⊢ M \in (3 \dots K) \to K \in ℤ_{\geq M}$
89	65 88	syl	$⊢ φ \to K \in ℤ_{\geq M}$
90	3 62 69 89	pcmptdvds	$⊢ φ \to seq 1 (\times F) (M) ∥ seq 1 (\times F) (K)$
91	70	nnzd	$⊢ φ \to seq 1 (\times F) (M) \in ℤ$
92	70	nnne0d	$⊢ φ \to seq 1 (\times F) (M) \neq 0$
93		uztrn	$⊢ (K \in ℤ_{\geq M} \land M \in ℤ_{\geq 3}) \to K \in ℤ_{\geq 3}$
94	89 67 93	syl2anc	$⊢ φ \to K \in ℤ_{\geq 3}$
95		eluznn	$⊢ (3 \in ℕ \land K \in ℤ_{\geq 3}) \to K \in ℕ$
96	27 94 95	sylancr	$⊢ φ \to K \in ℕ$
97	64 96	ffvelcdmd	$⊢ φ \to seq 1 (\times F) (K) \in ℕ$
98	97	nnzd	$⊢ φ \to seq 1 (\times F) (K) \in ℤ$
99		dvdsval2	$⊢ (seq 1 (\times F) (M) \in ℤ \land seq 1 (\times F) (M) \neq 0 \land seq 1 (\times F) (K) \in ℤ) \to (seq 1 (\times F) (M) ∥ seq 1 (\times F) (K) \leftrightarrow \frac{seq 1 (\times F) (K)}{seq 1 (\times F) (M)} \in ℤ)$
100	91 92 98 99	syl3anc	$⊢ φ \to (seq 1 (\times F) (M) ∥ seq 1 (\times F) (K) \leftrightarrow \frac{seq 1 (\times F) (K)}{seq 1 (\times F) (M)} \in ℤ)$
101	90 100	mpbid	$⊢ φ \to \frac{seq 1 (\times F) (K)}{seq 1 (\times F) (M)} \in ℤ$
102	101	zred	$⊢ φ \to \frac{seq 1 (\times F) (K)}{seq 1 (\times F) (M)} \in ℝ$
103	69	nnred	$⊢ φ \to M \in ℝ$
104	76	zred	$⊢ φ \to K \in ℝ$
105		eluzle	$⊢ K \in ℤ_{\geq M} \to M \leq K$
106	89 105	syl	$⊢ φ \to M \leq K$
107		efchtdvds	$⊢ (M \in ℝ \land K \in ℝ \land M \leq K) \to e^{θ (M)} ∥ e^{θ (K)}$
108	103 104 106 107	syl3anc	$⊢ φ \to e^{θ (M)} ∥ e^{θ (K)}$
109		efchtcl	$⊢ M \in ℝ \to e^{θ (M)} \in ℕ$
110	103 109	syl	$⊢ φ \to e^{θ (M)} \in ℕ$
111	110	nnzd	$⊢ φ \to e^{θ (M)} \in ℤ$
112	110	nnne0d	$⊢ φ \to e^{θ (M)} \neq 0$
113		efchtcl	$⊢ K \in ℝ \to e^{θ (K)} \in ℕ$
114	104 113	syl	$⊢ φ \to e^{θ (K)} \in ℕ$
115	114	nnzd	$⊢ φ \to e^{θ (K)} \in ℤ$
116		dvdsval2	$⊢ (e^{θ (M)} \in ℤ \land e^{θ (M)} \neq 0 \land e^{θ (K)} \in ℤ) \to (e^{θ (M)} ∥ e^{θ (K)} \leftrightarrow \frac{e^{θ (K)}}{e^{θ (M)}} \in ℤ)$
117	111 112 115 116	syl3anc	$⊢ φ \to (e^{θ (M)} ∥ e^{θ (K)} \leftrightarrow \frac{e^{θ (K)}}{e^{θ (M)}} \in ℤ)$
118	108 117	mpbid	$⊢ φ \to \frac{e^{θ (K)}}{e^{θ (M)}} \in ℤ$
119	118	zred	$⊢ φ \to \frac{e^{θ (K)}}{e^{θ (M)}} \in ℝ$
120		prmz	$⊢ p \in ℙ \to p \in ℤ$
121		fllt	$⊢ (\sqrt{2 \cdot N} \in ℝ \land p \in ℤ) \to (\sqrt{2 \cdot N} < p \leftrightarrow ⌊\sqrt{2 \cdot N}⌋ < p)$
122	26 120 121	syl2an	$⊢ (φ \land p \in ℙ) \to (\sqrt{2 \cdot N} < p \leftrightarrow ⌊\sqrt{2 \cdot N}⌋ < p)$
123	5	breq1i	$⊢ M < p \leftrightarrow ⌊\sqrt{2 \cdot N}⌋ < p$
124	122 123	bitr4di	$⊢ (φ \land p \in ℙ) \to (\sqrt{2 \cdot N} < p \leftrightarrow M < p)$
125	120	zred	$⊢ p \in ℙ \to p \in ℝ$
126		ltnle	$⊢ (M \in ℝ \land p \in ℝ) \to (M < p \leftrightarrow \neg p \leq M)$
127	103 125 126	syl2an	$⊢ (φ \land p \in ℙ) \to (M < p \leftrightarrow \neg p \leq M)$
128	124 127	bitrd	$⊢ (φ \land p \in ℙ) \to (\sqrt{2 \cdot N} < p \leftrightarrow \neg p \leq M)$
129		bposlem1	$⊢ (N \in ℕ \land p \in ℙ) \to p^{p pCnt (\binom{2 \cdot N}{N})} \leq 2 \cdot N$
130	9 129	sylan	$⊢ (φ \land p \in ℙ) \to p^{p pCnt (\binom{2 \cdot N}{N})} \leq 2 \cdot N$
131	125	adantl	$⊢ (φ \land p \in ℙ) \to p \in ℝ$
132		id	$⊢ p \in ℙ \to p \in ℙ$
133		pccl	$⊢ (p \in ℙ \land (\binom{2 \cdot N}{N}) \in ℕ) \to p pCnt (\binom{2 \cdot N}{N}) \in ℕ_{0}$
134	132 18 133	syl2anr	$⊢ (φ \land p \in ℙ) \to p pCnt (\binom{2 \cdot N}{N}) \in ℕ_{0}$
135	131 134	reexpcld	$⊢ (φ \land p \in ℙ) \to p^{p pCnt (\binom{2 \cdot N}{N})} \in ℝ$
136	24	adantr	$⊢ (φ \land p \in ℙ) \to 2 \cdot N \in ℝ$
137	131	resqcld	$⊢ (φ \land p \in ℙ) \to p^{2} \in ℝ$
138		lelttr	$⊢ (p^{p pCnt (\binom{2 \cdot N}{N})} \in ℝ \land 2 \cdot N \in ℝ \land p^{2} \in ℝ) \to ((p^{p pCnt (\binom{2 \cdot N}{N})} \leq 2 \cdot N \land 2 \cdot N < p^{2}) \to p^{p pCnt (\binom{2 \cdot N}{N})} < p^{2})$
139	135 136 137 138	syl3anc	$⊢ (φ \land p \in ℙ) \to ((p^{p pCnt (\binom{2 \cdot N}{N})} \leq 2 \cdot N \land 2 \cdot N < p^{2}) \to p^{p pCnt (\binom{2 \cdot N}{N})} < p^{2})$
140	130 139	mpand	$⊢ (φ \land p \in ℙ) \to (2 \cdot N < p^{2} \to p^{p pCnt (\binom{2 \cdot N}{N})} < p^{2})$
141		resqrtth	$⊢ (2 \cdot N \in ℝ \land 0 \leq 2 \cdot N) \to {\sqrt{2 \cdot N}}^{2} = 2 \cdot N$
142	24 25 141	syl2anc	$⊢ φ \to {\sqrt{2 \cdot N}}^{2} = 2 \cdot N$
143	142	breq1d	$⊢ φ \to ({\sqrt{2 \cdot N}}^{2} < p^{2} \leftrightarrow 2 \cdot N < p^{2})$
144	143	adantr	$⊢ (φ \land p \in ℙ) \to ({\sqrt{2 \cdot N}}^{2} < p^{2} \leftrightarrow 2 \cdot N < p^{2})$
145	134	nn0zd	$⊢ (φ \land p \in ℙ) \to p pCnt (\binom{2 \cdot N}{N}) \in ℤ$
146	72	a1i	$⊢ (φ \land p \in ℙ) \to 2 \in ℤ$
147		prmgt1	$⊢ p \in ℙ \to 1 < p$
148	147	adantl	$⊢ (φ \land p \in ℙ) \to 1 < p$
149	131 145 146 148	ltexp2d	$⊢ (φ \land p \in ℙ) \to (p pCnt (\binom{2 \cdot N}{N}) < 2 \leftrightarrow p^{p pCnt (\binom{2 \cdot N}{N})} < p^{2})$
150	140 144 149	3imtr4d	$⊢ (φ \land p \in ℙ) \to ({\sqrt{2 \cdot N}}^{2} < p^{2} \to p pCnt (\binom{2 \cdot N}{N}) < 2)$
151		df-2	$⊢ 2 = 1 + 1$
152	151	breq2i	$⊢ p pCnt (\binom{2 \cdot N}{N}) < 2 \leftrightarrow p pCnt (\binom{2 \cdot N}{N}) < 1 + 1$
153	150 152	imbitrdi	$⊢ (φ \land p \in ℙ) \to ({\sqrt{2 \cdot N}}^{2} < p^{2} \to p pCnt (\binom{2 \cdot N}{N}) < 1 + 1)$
154	26	adantr	$⊢ (φ \land p \in ℙ) \to \sqrt{2 \cdot N} \in ℝ$
155	24 25	sqrtge0d	$⊢ φ \to 0 \leq \sqrt{2 \cdot N}$
156	155	adantr	$⊢ (φ \land p \in ℙ) \to 0 \leq \sqrt{2 \cdot N}$
157		prmnn	$⊢ p \in ℙ \to p \in ℕ$
158	157	nnrpd	$⊢ p \in ℙ \to p \in ℝ^{+}$
159	158	rpge0d	$⊢ p \in ℙ \to 0 \leq p$
160	159	adantl	$⊢ (φ \land p \in ℙ) \to 0 \leq p$
161	154 131 156 160	lt2sqd	$⊢ (φ \land p \in ℙ) \to (\sqrt{2 \cdot N} < p \leftrightarrow {\sqrt{2 \cdot N}}^{2} < p^{2})$
162		1z	$⊢ 1 \in ℤ$
163		zleltp1	$⊢ (p pCnt (\binom{2 \cdot N}{N}) \in ℤ \land 1 \in ℤ) \to (p pCnt (\binom{2 \cdot N}{N}) \leq 1 \leftrightarrow p pCnt (\binom{2 \cdot N}{N}) < 1 + 1)$
164	145 162 163	sylancl	$⊢ (φ \land p \in ℙ) \to (p pCnt (\binom{2 \cdot N}{N}) \leq 1 \leftrightarrow p pCnt (\binom{2 \cdot N}{N}) < 1 + 1)$
165	153 161 164	3imtr4d	$⊢ (φ \land p \in ℙ) \to (\sqrt{2 \cdot N} < p \to p pCnt (\binom{2 \cdot N}{N}) \leq 1)$
166	128 165	sylbird	$⊢ (φ \land p \in ℙ) \to (\neg p \leq M \to p pCnt (\binom{2 \cdot N}{N}) \leq 1)$
167	166	imp	$⊢ ((φ \land p \in ℙ) \land \neg p \leq M) \to p pCnt (\binom{2 \cdot N}{N}) \leq 1$
168	167	adantrl	$⊢ ((φ \land p \in ℙ) \land (p \leq K \land \neg p \leq M)) \to p pCnt (\binom{2 \cdot N}{N}) \leq 1$
169		iftrue	$⊢ (p \leq K \land \neg p \leq M) \to if ((p \leq K \land \neg p \leq M), p pCnt (\binom{2 \cdot N}{N}), 0) = p pCnt (\binom{2 \cdot N}{N})$
170	169	adantl	$⊢ ((φ \land p \in ℙ) \land (p \leq K \land \neg p \leq M)) \to if ((p \leq K \land \neg p \leq M), p pCnt (\binom{2 \cdot N}{N}), 0) = p pCnt (\binom{2 \cdot N}{N})$
171		iftrue	$⊢ (p \leq K \land \neg p \leq M) \to if ((p \leq K \land \neg p \leq M), 1, 0) = 1$
172	171	adantl	$⊢ ((φ \land p \in ℙ) \land (p \leq K \land \neg p \leq M)) \to if ((p \leq K \land \neg p \leq M), 1, 0) = 1$
173	168 170 172	3brtr4d	$⊢ ((φ \land p \in ℙ) \land (p \leq K \land \neg p \leq M)) \to if ((p \leq K \land \neg p \leq M), p pCnt (\binom{2 \cdot N}{N}), 0) \leq if ((p \leq K \land \neg p \leq M), 1, 0)$
174		0le0	$⊢ 0 \leq 0$
175		iffalse	$⊢ \neg (p \leq K \land \neg p \leq M) \to if ((p \leq K \land \neg p \leq M), p pCnt (\binom{2 \cdot N}{N}), 0) = 0$
176		iffalse	$⊢ \neg (p \leq K \land \neg p \leq M) \to if ((p \leq K \land \neg p \leq M), 1, 0) = 0$
177	175 176	breq12d	$⊢ \neg (p \leq K \land \neg p \leq M) \to (if ((p \leq K \land \neg p \leq M), p pCnt (\binom{2 \cdot N}{N}), 0) \leq if ((p \leq K \land \neg p \leq M), 1, 0) \leftrightarrow 0 \leq 0)$
178	174 177	mpbiri	$⊢ \neg (p \leq K \land \neg p \leq M) \to if ((p \leq K \land \neg p \leq M), p pCnt (\binom{2 \cdot N}{N}), 0) \leq if ((p \leq K \land \neg p \leq M), 1, 0)$
179	178	adantl	$⊢ ((φ \land p \in ℙ) \land \neg (p \leq K \land \neg p \leq M)) \to if ((p \leq K \land \neg p \leq M), p pCnt (\binom{2 \cdot N}{N}), 0) \leq if ((p \leq K \land \neg p \leq M), 1, 0)$
180	173 179	pm2.61dan	$⊢ (φ \land p \in ℙ) \to if ((p \leq K \land \neg p \leq M), p pCnt (\binom{2 \cdot N}{N}), 0) \leq if ((p \leq K \land \neg p \leq M), 1, 0)$
181	62	adantr	$⊢ (φ \land p \in ℙ) \to \forall n \in ℙ n pCnt (\binom{2 \cdot N}{N}) \in ℕ_{0}$
182	69	adantr	$⊢ (φ \land p \in ℙ) \to M \in ℕ$
183		simpr	$⊢ (φ \land p \in ℙ) \to p \in ℙ$
184		oveq1	$⊢ n = p \to n pCnt (\binom{2 \cdot N}{N}) = p pCnt (\binom{2 \cdot N}{N})$
185	89	adantr	$⊢ (φ \land p \in ℙ) \to K \in ℤ_{\geq M}$
186	3 181 182 183 184 185	pcmpt2	$⊢ (φ \land p \in ℙ) \to p pCnt (\frac{seq 1 (\times F) (K)}{seq 1 (\times F) (M)}) = if ((p \leq K \land \neg p \leq M), p pCnt (\binom{2 \cdot N}{N}), 0)$
187		eqid	$⊢ (n \in ℕ ⟼ if (n \in ℙ, n, 1)) = (n \in ℕ ⟼ if (n \in ℙ, n, 1))$
188	187	prmorcht	$⊢ K \in ℕ \to e^{θ (K)} = seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, n, 1))) (K)$
189	96 188	syl	$⊢ φ \to e^{θ (K)} = seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, n, 1))) (K)$
190	187	prmorcht	$⊢ M \in ℕ \to e^{θ (M)} = seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, n, 1))) (M)$
191	69 190	syl	$⊢ φ \to e^{θ (M)} = seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, n, 1))) (M)$
192	189 191	oveq12d	$⊢ φ \to \frac{e^{θ (K)}}{e^{θ (M)}} = \frac{seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, n, 1))) (K)}{seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, n, 1))) (M)}$
193	192	adantr	$⊢ (φ \land p \in ℙ) \to \frac{e^{θ (K)}}{e^{θ (M)}} = \frac{seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, n, 1))) (K)}{seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, n, 1))) (M)}$
194	193	oveq2d	$⊢ (φ \land p \in ℙ) \to p pCnt (\frac{e^{θ (K)}}{e^{θ (M)}}) = p pCnt (\frac{seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, n, 1))) (K)}{seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, n, 1))) (M)})$
195		nncn	$⊢ n \in ℕ \to n \in ℂ$
196	195	exp1d	$⊢ n \in ℕ \to n^{1} = n$
197	196	ifeq1d	$⊢ n \in ℕ \to if (n \in ℙ, n^{1}, 1) = if (n \in ℙ, n, 1)$
198	197	mpteq2ia	$⊢ (n \in ℕ ⟼ if (n \in ℙ, n^{1}, 1)) = (n \in ℕ ⟼ if (n \in ℙ, n, 1))$
199	198	eqcomi	$⊢ (n \in ℕ ⟼ if (n \in ℙ, n, 1)) = (n \in ℕ ⟼ if (n \in ℙ, n^{1}, 1))$
200		1nn0	$⊢ 1 \in ℕ_{0}$
201	200	a1i	$⊢ (φ \land n \in ℙ) \to 1 \in ℕ_{0}$
202	201	ralrimiva	$⊢ φ \to \forall n \in ℙ 1 \in ℕ_{0}$
203	202	adantr	$⊢ (φ \land p \in ℙ) \to \forall n \in ℙ 1 \in ℕ_{0}$
204		eqidd	$⊢ n = p \to 1 = 1$
205	199 203 182 183 204 185	pcmpt2	$⊢ (φ \land p \in ℙ) \to p pCnt (\frac{seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, n, 1))) (K)}{seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, n, 1))) (M)}) = if ((p \leq K \land \neg p \leq M), 1, 0)$
206	194 205	eqtrd	$⊢ (φ \land p \in ℙ) \to p pCnt (\frac{e^{θ (K)}}{e^{θ (M)}}) = if ((p \leq K \land \neg p \leq M), 1, 0)$
207	180 186 206	3brtr4d	$⊢ (φ \land p \in ℙ) \to p pCnt (\frac{seq 1 (\times F) (K)}{seq 1 (\times F) (M)}) \leq p pCnt (\frac{e^{θ (K)}}{e^{θ (M)}})$
208	207	ralrimiva	$⊢ φ \to \forall p \in ℙ p pCnt (\frac{seq 1 (\times F) (K)}{seq 1 (\times F) (M)}) \leq p pCnt (\frac{e^{θ (K)}}{e^{θ (M)}})$
209		pc2dvds	$⊢ (\frac{seq 1 (\times F) (K)}{seq 1 (\times F) (M)} \in ℤ \land \frac{e^{θ (K)}}{e^{θ (M)}} \in ℤ) \to ((\frac{seq 1 (\times F) (K)}{seq 1 (\times F) (M)}) ∥ (\frac{e^{θ (K)}}{e^{θ (M)}}) \leftrightarrow \forall p \in ℙ p pCnt (\frac{seq 1 (\times F) (K)}{seq 1 (\times F) (M)}) \leq p pCnt (\frac{e^{θ (K)}}{e^{θ (M)}}))$
210	101 118 209	syl2anc	$⊢ φ \to ((\frac{seq 1 (\times F) (K)}{seq 1 (\times F) (M)}) ∥ (\frac{e^{θ (K)}}{e^{θ (M)}}) \leftrightarrow \forall p \in ℙ p pCnt (\frac{seq 1 (\times F) (K)}{seq 1 (\times F) (M)}) \leq p pCnt (\frac{e^{θ (K)}}{e^{θ (M)}}))$
211	208 210	mpbird	$⊢ φ \to (\frac{seq 1 (\times F) (K)}{seq 1 (\times F) (M)}) ∥ (\frac{e^{θ (K)}}{e^{θ (M)}})$
212	114	nnred	$⊢ φ \to e^{θ (K)} \in ℝ$
213	110	nnred	$⊢ φ \to e^{θ (M)} \in ℝ$
214	114	nngt0d	$⊢ φ \to 0 < e^{θ (K)}$
215	110	nngt0d	$⊢ φ \to 0 < e^{θ (M)}$
216	212 213 214 215	divgt0d	$⊢ φ \to 0 < \frac{e^{θ (K)}}{e^{θ (M)}}$
217		elnnz	$⊢ \frac{e^{θ (K)}}{e^{θ (M)}} \in ℕ \leftrightarrow (\frac{e^{θ (K)}}{e^{θ (M)}} \in ℤ \land 0 < \frac{e^{θ (K)}}{e^{θ (M)}})$
218	118 216 217	sylanbrc	$⊢ φ \to \frac{e^{θ (K)}}{e^{θ (M)}} \in ℕ$
219		dvdsle	$⊢ (\frac{seq 1 (\times F) (K)}{seq 1 (\times F) (M)} \in ℤ \land \frac{e^{θ (K)}}{e^{θ (M)}} \in ℕ) \to ((\frac{seq 1 (\times F) (K)}{seq 1 (\times F) (M)}) ∥ (\frac{e^{θ (K)}}{e^{θ (M)}}) \to \frac{seq 1 (\times F) (K)}{seq 1 (\times F) (M)} \leq \frac{e^{θ (K)}}{e^{θ (M)}})$
220	101 218 219	syl2anc	$⊢ φ \to ((\frac{seq 1 (\times F) (K)}{seq 1 (\times F) (M)}) ∥ (\frac{e^{θ (K)}}{e^{θ (M)}}) \to \frac{seq 1 (\times F) (K)}{seq 1 (\times F) (M)} \leq \frac{e^{θ (K)}}{e^{θ (M)}})$
221	211 220	mpd	$⊢ φ \to \frac{seq 1 (\times F) (K)}{seq 1 (\times F) (M)} \leq \frac{e^{θ (K)}}{e^{θ (M)}}$
222		nndivre	$⊢ (e^{θ (K)} \in ℝ \land 4 \in ℕ) \to \frac{e^{θ (K)}}{4} \in ℝ$
223	212 6 222	sylancl	$⊢ φ \to \frac{e^{θ (K)}}{4} \in ℝ$
224		4re	$⊢ 4 \in ℝ$
225	224	a1i	$⊢ φ \to 4 \in ℝ$
226		6re	$⊢ 6 \in ℝ$
227	226	a1i	$⊢ φ \to 6 \in ℝ$
228		4lt6	$⊢ 4 < 6$
229	228	a1i	$⊢ φ \to 4 < 6$
230		cht3	$⊢ θ (3) = \log 6$
231	230	fveq2i	$⊢ e^{θ (3)} = e^{\log 6}$
232		6pos	$⊢ 0 < 6$
233	226 232	elrpii	$⊢ 6 \in ℝ^{+}$
234		reeflog	$⊢ 6 \in ℝ^{+} \to e^{\log 6} = 6$
235	233 234	ax-mp	$⊢ e^{\log 6} = 6$
236	231 235	eqtri	$⊢ e^{θ (3)} = 6$
237		3re	$⊢ 3 \in ℝ$
238	237	a1i	$⊢ φ \to 3 \in ℝ$
239		eluzle	$⊢ M \in ℤ_{\geq 3} \to 3 \leq M$
240	67 239	syl	$⊢ φ \to 3 \leq M$
241		chtwordi	$⊢ (3 \in ℝ \land M \in ℝ \land 3 \leq M) \to θ (3) \leq θ (M)$
242	238 103 240 241	syl3anc	$⊢ φ \to θ (3) \leq θ (M)$
243		chtcl	$⊢ 3 \in ℝ \to θ (3) \in ℝ$
244	237 243	ax-mp	$⊢ θ (3) \in ℝ$
245		chtcl	$⊢ M \in ℝ \to θ (M) \in ℝ$
246	103 245	syl	$⊢ φ \to θ (M) \in ℝ$
247		efle	$⊢ (θ (3) \in ℝ \land θ (M) \in ℝ) \to (θ (3) \leq θ (M) \leftrightarrow e^{θ (3)} \leq e^{θ (M)})$
248	244 246 247	sylancr	$⊢ φ \to (θ (3) \leq θ (M) \leftrightarrow e^{θ (3)} \leq e^{θ (M)})$
249	242 248	mpbid	$⊢ φ \to e^{θ (3)} \leq e^{θ (M)}$
250	236 249	eqbrtrrid	$⊢ φ \to 6 \leq e^{θ (M)}$
251	225 227 213 229 250	ltletrd	$⊢ φ \to 4 < e^{θ (M)}$
252		4pos	$⊢ 0 < 4$
253	252	a1i	$⊢ φ \to 0 < 4$
254		ltdiv2	$⊢ ((4 \in ℝ \land 0 < 4) \land (e^{θ (M)} \in ℝ \land 0 < e^{θ (M)}) \land (e^{θ (K)} \in ℝ \land 0 < e^{θ (K)})) \to (4 < e^{θ (M)} \leftrightarrow \frac{e^{θ (K)}}{e^{θ (M)}} < \frac{e^{θ (K)}}{4})$
255	225 253 213 215 212 214 254	syl222anc	$⊢ φ \to (4 < e^{θ (M)} \leftrightarrow \frac{e^{θ (K)}}{e^{θ (M)}} < \frac{e^{θ (K)}}{4})$
256	251 255	mpbid	$⊢ φ \to \frac{e^{θ (K)}}{e^{θ (M)}} < \frac{e^{θ (K)}}{4}$
257	30	a1i	$⊢ φ \to 2 \in ℝ$
258		2lt3	$⊢ 2 < 3$
259	258	a1i	$⊢ φ \to 2 < 3$
260	238 103 104 240 106	letrd	$⊢ φ \to 3 \leq K$
261	257 238 104 259 260	ltletrd	$⊢ φ \to 2 < K$
262		chtub	$⊢ (K \in ℝ \land 2 < K) \to θ (K) < \log 2 (2 K - 3)$
263	104 261 262	syl2anc	$⊢ φ \to θ (K) < \log 2 (2 K - 3)$
264		chtcl	$⊢ K \in ℝ \to θ (K) \in ℝ$
265	104 264	syl	$⊢ φ \to θ (K) \in ℝ$
266		relogcl	$⊢ 2 \in ℝ^{+} \to \log 2 \in ℝ$
267	35 266	ax-mp	$⊢ \log 2 \in ℝ$
268		3z	$⊢ 3 \in ℤ$
269		zsubcl	$⊢ (2 K \in ℤ \land 3 \in ℤ) \to 2 K - 3 \in ℤ$
270	78 268 269	sylancl	$⊢ φ \to 2 K - 3 \in ℤ$
271	270	zred	$⊢ φ \to 2 K - 3 \in ℝ$
272		remulcl	$⊢ (\log 2 \in ℝ \land 2 K - 3 \in ℝ) \to \log 2 (2 K - 3) \in ℝ$
273	267 271 272	sylancr	$⊢ φ \to \log 2 (2 K - 3) \in ℝ$
274		eflt	$⊢ (θ (K) \in ℝ \land \log 2 (2 K - 3) \in ℝ) \to (θ (K) < \log 2 (2 K - 3) \leftrightarrow e^{θ (K)} < e^{\log 2 (2 K - 3)})$
275	265 273 274	syl2anc	$⊢ φ \to (θ (K) < \log 2 (2 K - 3) \leftrightarrow e^{θ (K)} < e^{\log 2 (2 K - 3)})$
276	263 275	mpbid	$⊢ φ \to e^{θ (K)} < e^{\log 2 (2 K - 3)}$
277		reexplog	$⊢ (2 \in ℝ^{+} \land 2 K - 3 \in ℤ) \to 2^{2 K - 3} = e^{(2 K - 3) \log 2}$
278	35 270 277	sylancr	$⊢ φ \to 2^{2 K - 3} = e^{(2 K - 3) \log 2}$
279	270	zcnd	$⊢ φ \to 2 K - 3 \in ℂ$
280	267	recni	$⊢ \log 2 \in ℂ$
281		mulcom	$⊢ (2 K - 3 \in ℂ \land \log 2 \in ℂ) \to (2 K - 3) \log 2 = \log 2 (2 K - 3)$
282	279 280 281	sylancl	$⊢ φ \to (2 K - 3) \log 2 = \log 2 (2 K - 3)$
283	282	fveq2d	$⊢ φ \to e^{(2 K - 3) \log 2} = e^{\log 2 (2 K - 3)}$
284	278 283	eqtrd	$⊢ φ \to 2^{2 K - 3} = e^{\log 2 (2 K - 3)}$
285	276 284	breqtrrd	$⊢ φ \to e^{θ (K)} < 2^{2 K - 3}$
286		3p2e5	$⊢ 3 + 2 = 5$
287	286	oveq1i	$⊢ 3 + 2 - 2 = 5 - 2$
288		3cn	$⊢ 3 \in ℂ$
289		2cn	$⊢ 2 \in ℂ$
290	288 289	pncan3oi	$⊢ 3 + 2 - 2 = 3$
291	287 290	eqtr3i	$⊢ 5 - 2 = 3$
292	291	oveq2i	$⊢ 2 K - (5 - 2) = 2 K - 3$
293	78	zcnd	$⊢ φ \to 2 K \in ℂ$
294		5cn	$⊢ 5 \in ℂ$
295		subsub	$⊢ (2 K \in ℂ \land 5 \in ℂ \land 2 \in ℂ) \to 2 K - (5 - 2) = 2 K - 5 + 2$
296	294 289 295	mp3an23	$⊢ 2 K \in ℂ \to 2 K - (5 - 2) = 2 K - 5 + 2$
297	293 296	syl	$⊢ φ \to 2 K - (5 - 2) = 2 K - 5 + 2$
298	292 297	eqtr3id	$⊢ φ \to 2 K - 3 = 2 K - 5 + 2$
299	298	oveq2d	$⊢ φ \to 2^{2 K - 3} = 2^{2 K - 5 + 2}$
300		2ne0	$⊢ 2 \neq 0$
301		cxpexpz	$⊢ (2 \in ℂ \land 2 \neq 0 \land 2 K - 3 \in ℤ) \to 2^{2 K - 3} = 2^{2 K - 3}$
302	289 300 270 301	mp3an12i	$⊢ φ \to 2^{2 K - 3} = 2^{2 K - 3}$
303	81	zcnd	$⊢ φ \to 2 K - 5 \in ℂ$
304		2cnne0	$⊢ (2 \in ℂ \land 2 \neq 0)$
305		cxpadd	$⊢ ((2 \in ℂ \land 2 \neq 0) \land 2 K - 5 \in ℂ \land 2 \in ℂ) \to 2^{2 K - 5 + 2} = 2^{2 K - 5} 2^{2}$
306	304 289 305	mp3an13	$⊢ 2 K - 5 \in ℂ \to 2^{2 K - 5 + 2} = 2^{2 K - 5} 2^{2}$
307	303 306	syl	$⊢ φ \to 2^{2 K - 5 + 2} = 2^{2 K - 5} 2^{2}$
308	299 302 307	3eqtr3d	$⊢ φ \to 2^{2 K - 3} = 2^{2 K - 5} 2^{2}$
309		2nn0	$⊢ 2 \in ℕ_{0}$
310		cxpexp	$⊢ (2 \in ℂ \land 2 \in ℕ_{0}) \to 2^{2} = 2^{2}$
311	289 309 310	mp2an	$⊢ 2^{2} = 2^{2}$
312		sq2	$⊢ 2^{2} = 4$
313	311 312	eqtri	$⊢ 2^{2} = 4$
314	313	oveq2i	$⊢ 2^{2 K - 5} 2^{2} = 2^{2 K - 5} \cdot 4$
315	308 314	eqtrdi	$⊢ φ \to 2^{2 K - 3} = 2^{2 K - 5} \cdot 4$
316	285 315	breqtrd	$⊢ φ \to e^{θ (K)} < 2^{2 K - 5} \cdot 4$
317	224 252	pm3.2i	$⊢ (4 \in ℝ \land 0 < 4)$
318	317	a1i	$⊢ φ \to (4 \in ℝ \land 0 < 4)$
319		ltdivmul2	$⊢ (e^{θ (K)} \in ℝ \land 2^{2 K - 5} \in ℝ \land (4 \in ℝ \land 0 < 4)) \to (\frac{e^{θ (K)}}{4} < 2^{2 K - 5} \leftrightarrow e^{θ (K)} < 2^{2 K - 5} \cdot 4)$
320	212 85 318 319	syl3anc	$⊢ φ \to (\frac{e^{θ (K)}}{4} < 2^{2 K - 5} \leftrightarrow e^{θ (K)} < 2^{2 K - 5} \cdot 4)$
321	316 320	mpbird	$⊢ φ \to \frac{e^{θ (K)}}{4} < 2^{2 K - 5}$
322	119 223 85 256 321	lttrd	$⊢ φ \to \frac{e^{θ (K)}}{e^{θ (M)}} < 2^{2 K - 5}$
323	102 119 85 221 322	lelttrd	$⊢ φ \to \frac{seq 1 (\times F) (K)}{seq 1 (\times F) (M)} < 2^{2 K - 5}$
324	97	nnred	$⊢ φ \to seq 1 (\times F) (K) \in ℝ$
325		nnre	$⊢ seq 1 (\times F) (M) \in ℕ \to seq 1 (\times F) (M) \in ℝ$
326		nngt0	$⊢ seq 1 (\times F) (M) \in ℕ \to 0 < seq 1 (\times F) (M)$
327	325 326	jca	$⊢ seq 1 (\times F) (M) \in ℕ \to (seq 1 (\times F) (M) \in ℝ \land 0 < seq 1 (\times F) (M))$
328	70 327	syl	$⊢ φ \to (seq 1 (\times F) (M) \in ℝ \land 0 < seq 1 (\times F) (M))$
329		ltdivmul	$⊢ (seq 1 (\times F) (K) \in ℝ \land 2^{2 K - 5} \in ℝ \land (seq 1 (\times F) (M) \in ℝ \land 0 < seq 1 (\times F) (M))) \to (\frac{seq 1 (\times F) (K)}{seq 1 (\times F) (M)} < 2^{2 K - 5} \leftrightarrow seq 1 (\times F) (K) < seq 1 (\times F) (M) 2^{2 K - 5})$
330	324 85 328 329	syl3anc	$⊢ φ \to (\frac{seq 1 (\times F) (K)}{seq 1 (\times F) (M)} < 2^{2 K - 5} \leftrightarrow seq 1 (\times F) (K) < seq 1 (\times F) (M) 2^{2 K - 5})$
331	323 330	mpbid	$⊢ φ \to seq 1 (\times F) (K) < seq 1 (\times F) (M) 2^{2 K - 5}$
332	87 331	eqbrtrrd	$⊢ φ \to (\binom{2 \cdot N}{N}) < seq 1 (\times F) (M) 2^{2 K - 5}$
333	34 85	remulcld	$⊢ φ \to {2 \cdot N}^{(\frac{\sqrt{2 \cdot N}}{3}) + 2} 2^{2 K - 5} \in ℝ$
334	1 2 3 4 5	bposlem5	$⊢ φ \to seq 1 (\times F) (M) \leq {2 \cdot N}^{(\frac{\sqrt{2 \cdot N}}{3}) + 2}$
335	71 34 84	lemul1d	$⊢ φ \to (seq 1 (\times F) (M) \leq {2 \cdot N}^{(\frac{\sqrt{2 \cdot N}}{3}) + 2} \leftrightarrow seq 1 (\times F) (M) 2^{2 K - 5} \leq {2 \cdot N}^{(\frac{\sqrt{2 \cdot N}}{3}) + 2} 2^{2 K - 5})$
336	334 335	mpbid	$⊢ φ \to seq 1 (\times F) (M) 2^{2 K - 5} \leq {2 \cdot N}^{(\frac{\sqrt{2 \cdot N}}{3}) + 2} 2^{2 K - 5}$
337	78	zred	$⊢ φ \to 2 K \in ℝ$
338	41	a1i	$⊢ φ \to 5 \in ℝ$
339		flle	$⊢ \frac{2 \cdot N}{3} \in ℝ \to ⌊\frac{2 \cdot N}{3}⌋ \leq \frac{2 \cdot N}{3}$
340	74 339	syl	$⊢ φ \to ⌊\frac{2 \cdot N}{3}⌋ \leq \frac{2 \cdot N}{3}$
341	4 340	eqbrtrid	$⊢ φ \to K \leq \frac{2 \cdot N}{3}$
342		2pos	$⊢ 0 < 2$
343	30 342	pm3.2i	$⊢ (2 \in ℝ \land 0 < 2)$
344	343	a1i	$⊢ φ \to (2 \in ℝ \land 0 < 2)$
345		lemul2	$⊢ (K \in ℝ \land \frac{2 \cdot N}{3} \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (K \leq \frac{2 \cdot N}{3} \leftrightarrow 2 K \leq 2 (\frac{2 \cdot N}{3}))$
346	104 74 344 345	syl3anc	$⊢ φ \to (K \leq \frac{2 \cdot N}{3} \leftrightarrow 2 K \leq 2 (\frac{2 \cdot N}{3}))$
347	341 346	mpbid	$⊢ φ \to 2 K \leq 2 (\frac{2 \cdot N}{3})$
348	22	nncnd	$⊢ φ \to 2 \cdot N \in ℂ$
349		3ne0	$⊢ 3 \neq 0$
350	288 349	pm3.2i	$⊢ (3 \in ℂ \land 3 \neq 0)$
351		divass	$⊢ (2 \in ℂ \land 2 \cdot N \in ℂ \land (3 \in ℂ \land 3 \neq 0)) \to \frac{2 2 \cdot N}{3} = 2 (\frac{2 \cdot N}{3})$
352	289 350 351	mp3an13	$⊢ 2 \cdot N \in ℂ \to \frac{2 2 \cdot N}{3} = 2 (\frac{2 \cdot N}{3})$
353	348 352	syl	$⊢ φ \to \frac{2 2 \cdot N}{3} = 2 (\frac{2 \cdot N}{3})$
354	9	nncnd	$⊢ φ \to N \in ℂ$
355		mulass	$⊢ (2 \in ℂ \land 2 \in ℂ \land N \in ℂ) \to 2 \cdot 2 \cdot N = 2 2 \cdot N$
356	289 289 354 355	mp3an12i	$⊢ φ \to 2 \cdot 2 \cdot N = 2 2 \cdot N$
357		2t2e4	$⊢ 2 \cdot 2 = 4$
358	357	oveq1i	$⊢ 2 \cdot 2 \cdot N = 4 \cdot N$
359	356 358	eqtr3di	$⊢ φ \to 2 2 \cdot N = 4 \cdot N$
360	359	oveq1d	$⊢ φ \to \frac{2 2 \cdot N}{3} = \frac{4 \cdot N}{3}$
361	353 360	eqtr3d	$⊢ φ \to 2 (\frac{2 \cdot N}{3}) = \frac{4 \cdot N}{3}$
362	347 361	breqtrd	$⊢ φ \to 2 K \leq \frac{4 \cdot N}{3}$
363	337 40 338 362	lesub1dd	$⊢ φ \to 2 K - 5 \leq (\frac{4 \cdot N}{3}) - 5$
364		1lt2	$⊢ 1 < 2$
365	364	a1i	$⊢ φ \to 1 < 2$
366	257 365 82 43	cxpled	$⊢ φ \to (2 K - 5 \leq (\frac{4 \cdot N}{3}) - 5 \leftrightarrow 2^{2 K - 5} \leq 2^{(\frac{4 \cdot N}{3}) - 5})$
367	363 366	mpbid	$⊢ φ \to 2^{2 K - 5} \leq 2^{(\frac{4 \cdot N}{3}) - 5}$
368	85 46 33	lemul2d	$⊢ φ \to (2^{2 K - 5} \leq 2^{(\frac{4 \cdot N}{3}) - 5} \leftrightarrow {2 \cdot N}^{(\frac{\sqrt{2 \cdot N}}{3}) + 2} 2^{2 K - 5} \leq {2 \cdot N}^{(\frac{\sqrt{2 \cdot N}}{3}) + 2} 2^{(\frac{4 \cdot N}{3}) - 5})$
369	367 368	mpbid	$⊢ φ \to {2 \cdot N}^{(\frac{\sqrt{2 \cdot N}}{3}) + 2} 2^{2 K - 5} \leq {2 \cdot N}^{(\frac{\sqrt{2 \cdot N}}{3}) + 2} 2^{(\frac{4 \cdot N}{3}) - 5}$
370	86 333 47 336 369	letrd	$⊢ φ \to seq 1 (\times F) (M) 2^{2 K - 5} \leq {2 \cdot N}^{(\frac{\sqrt{2 \cdot N}}{3}) + 2} 2^{(\frac{4 \cdot N}{3}) - 5}$
371	19 86 47 332 370	ltletrd	$⊢ φ \to (\binom{2 \cdot N}{N}) < {2 \cdot N}^{(\frac{\sqrt{2 \cdot N}}{3}) + 2} 2^{(\frac{4 \cdot N}{3}) - 5}$
372	14 19 47 58 371	lttrd	$⊢ φ \to \frac{4^{N}}{N} < {2 \cdot N}^{(\frac{\sqrt{2 \cdot N}}{3}) + 2} 2^{(\frac{4 \cdot N}{3}) - 5}$

Metamath Proof Explorer

Theorem bposlem6

Proof