chebbnd1lem1

Description: Lemma for chebbnd1 : show a lower bound on ppi ( x ) at even integers using similar techniques to those used to prove bpos . (Note that the expression K is actually equal to 2 x. N , but proving that is not necessary for the proof, and it's too much work.) The key to the proof is bposlem1 , which shows that each term in the expansion ( ( 2 x. N )C N ) = prod p e. Prime ( p ^ ( p pCnt ( ( 2 x. N )C N ) ) ) is at most 2 x. N , so that the sum really only has nonzero elements up to 2 x. N , and since each term is at most 2 x. N , after taking logs we get the inequality ppi ( 2 x. N ) x. log ( 2 x. N ) < log ( ( 2 x. N ) _C N ) , and bclbnd finishes the proof. (Contributed by Mario Carneiro, 22-Sep-2014) (Revised by Mario Carneiro, 15-Apr-2016)

		Ref	Expression
	Hypothesis	chebbnd1lem1.1	$⊢ K = if (2 \cdot N \leq (\binom{2 \cdot N}{N}), 2 \cdot N, (\binom{2 \cdot N}{N}))$
	Assertion	chebbnd1lem1	$⊢ N \in ℤ_{\geq 4} \to \log (\frac{4^{N}}{N}) < \underline{π} (2 \cdot N) \log 2 \cdot N$

Proof

Step	Hyp	Ref	Expression
1		chebbnd1lem1.1	$⊢ K = if (2 \cdot N \leq (\binom{2 \cdot N}{N}), 2 \cdot N, (\binom{2 \cdot N}{N}))$
2		4nn	$⊢ 4 \in ℕ$
3		eluznn	$⊢ (4 \in ℕ \land N \in ℤ_{\geq 4}) \to N \in ℕ$
4	2 3	mpan	$⊢ N \in ℤ_{\geq 4} \to N \in ℕ$
5	4	nnnn0d	$⊢ N \in ℤ_{\geq 4} \to N \in ℕ_{0}$
6		nnexpcl	$⊢ (4 \in ℕ \land N \in ℕ_{0}) \to 4^{N} \in ℕ$
7	2 5 6	sylancr	$⊢ N \in ℤ_{\geq 4} \to 4^{N} \in ℕ$
8	7	nnrpd	$⊢ N \in ℤ_{\geq 4} \to 4^{N} \in ℝ^{+}$
9	4	nnrpd	$⊢ N \in ℤ_{\geq 4} \to N \in ℝ^{+}$
10	8 9	rpdivcld	$⊢ N \in ℤ_{\geq 4} \to \frac{4^{N}}{N} \in ℝ^{+}$
11	10	relogcld	$⊢ N \in ℤ_{\geq 4} \to \log (\frac{4^{N}}{N}) \in ℝ$
12		fzctr	$⊢ N \in ℕ_{0} \to N \in (0 \dots 2 \cdot N)$
13	5 12	syl	$⊢ N \in ℤ_{\geq 4} \to N \in (0 \dots 2 \cdot N)$
14		bccl2	$⊢ N \in (0 \dots 2 \cdot N) \to (\binom{2 \cdot N}{N}) \in ℕ$
15	13 14	syl	$⊢ N \in ℤ_{\geq 4} \to (\binom{2 \cdot N}{N}) \in ℕ$
16	15	nnrpd	$⊢ N \in ℤ_{\geq 4} \to (\binom{2 \cdot N}{N}) \in ℝ^{+}$
17	16	relogcld	$⊢ N \in ℤ_{\geq 4} \to \log (\binom{2 \cdot N}{N}) \in ℝ$
18		2z	$⊢ 2 \in ℤ$
19		eluzelz	$⊢ N \in ℤ_{\geq 4} \to N \in ℤ$
20		zmulcl	$⊢ (2 \in ℤ \land N \in ℤ) \to 2 \cdot N \in ℤ$
21	18 19 20	sylancr	$⊢ N \in ℤ_{\geq 4} \to 2 \cdot N \in ℤ$
22	21	zred	$⊢ N \in ℤ_{\geq 4} \to 2 \cdot N \in ℝ$
23		ppicl	$⊢ 2 \cdot N \in ℝ \to \underline{π} (2 \cdot N) \in ℕ_{0}$
24	22 23	syl	$⊢ N \in ℤ_{\geq 4} \to \underline{π} (2 \cdot N) \in ℕ_{0}$
25	24	nn0red	$⊢ N \in ℤ_{\geq 4} \to \underline{π} (2 \cdot N) \in ℝ$
26		2nn	$⊢ 2 \in ℕ$
27		nnmulcl	$⊢ (2 \in ℕ \land N \in ℕ) \to 2 \cdot N \in ℕ$
28	26 4 27	sylancr	$⊢ N \in ℤ_{\geq 4} \to 2 \cdot N \in ℕ$
29	28	nnrpd	$⊢ N \in ℤ_{\geq 4} \to 2 \cdot N \in ℝ^{+}$
30	29	relogcld	$⊢ N \in ℤ_{\geq 4} \to \log 2 \cdot N \in ℝ$
31	25 30	remulcld	$⊢ N \in ℤ_{\geq 4} \to \underline{π} (2 \cdot N) \log 2 \cdot N \in ℝ$
32		bclbnd	$⊢ N \in ℤ_{\geq 4} \to \frac{4^{N}}{N} < (\binom{2 \cdot N}{N})$
33		logltb	$⊢ (\frac{4^{N}}{N} \in ℝ^{+} \land (\binom{2 \cdot N}{N}) \in ℝ^{+}) \to (\frac{4^{N}}{N} < (\binom{2 \cdot N}{N}) \leftrightarrow \log (\frac{4^{N}}{N}) < \log (\binom{2 \cdot N}{N}))$
34	10 16 33	syl2anc	$⊢ N \in ℤ_{\geq 4} \to (\frac{4^{N}}{N} < (\binom{2 \cdot N}{N}) \leftrightarrow \log (\frac{4^{N}}{N}) < \log (\binom{2 \cdot N}{N}))$
35	32 34	mpbid	$⊢ N \in ℤ_{\geq 4} \to \log (\frac{4^{N}}{N}) < \log (\binom{2 \cdot N}{N})$
36	28 15	ifcld	$⊢ N \in ℤ_{\geq 4} \to if (2 \cdot N \leq (\binom{2 \cdot N}{N}), 2 \cdot N, (\binom{2 \cdot N}{N})) \in ℕ$
37	1 36	eqeltrid	$⊢ N \in ℤ_{\geq 4} \to K \in ℕ$
38	37	nnred	$⊢ N \in ℤ_{\geq 4} \to K \in ℝ$
39		ppicl	$⊢ K \in ℝ \to \underline{π} (K) \in ℕ_{0}$
40	38 39	syl	$⊢ N \in ℤ_{\geq 4} \to \underline{π} (K) \in ℕ_{0}$
41	40	nn0red	$⊢ N \in ℤ_{\geq 4} \to \underline{π} (K) \in ℝ$
42	41 30	remulcld	$⊢ N \in ℤ_{\geq 4} \to \underline{π} (K) \log 2 \cdot N \in ℝ$
43		fzfid	$⊢ N \in ℤ_{\geq 4} \to (1 \dots K) \in Fin$
44		inss1	$⊢ (1 \dots K) \cap ℙ \subseteq (1 \dots K)$
45		ssfi	$⊢ ((1 \dots K) \in Fin \land (1 \dots K) \cap ℙ \subseteq (1 \dots K)) \to (1 \dots K) \cap ℙ \in Fin$
46	43 44 45	sylancl	$⊢ N \in ℤ_{\geq 4} \to (1 \dots K) \cap ℙ \in Fin$
47	37	nnzd	$⊢ N \in ℤ_{\geq 4} \to K \in ℤ$
48	15	nnzd	$⊢ N \in ℤ_{\geq 4} \to (\binom{2 \cdot N}{N}) \in ℤ$
49	15	nnred	$⊢ N \in ℤ_{\geq 4} \to (\binom{2 \cdot N}{N}) \in ℝ$
50		min2	$⊢ (2 \cdot N \in ℝ \land (\binom{2 \cdot N}{N}) \in ℝ) \to if (2 \cdot N \leq (\binom{2 \cdot N}{N}), 2 \cdot N, (\binom{2 \cdot N}{N})) \leq (\binom{2 \cdot N}{N})$
51	22 49 50	syl2anc	$⊢ N \in ℤ_{\geq 4} \to if (2 \cdot N \leq (\binom{2 \cdot N}{N}), 2 \cdot N, (\binom{2 \cdot N}{N})) \leq (\binom{2 \cdot N}{N})$
52	1 51	eqbrtrid	$⊢ N \in ℤ_{\geq 4} \to K \leq (\binom{2 \cdot N}{N})$
53		eluz2	$⊢ (\binom{2 \cdot N}{N}) \in ℤ_{\geq K} \leftrightarrow (K \in ℤ \land (\binom{2 \cdot N}{N}) \in ℤ \land K \leq (\binom{2 \cdot N}{N}))$
54	47 48 52 53	syl3anbrc	$⊢ N \in ℤ_{\geq 4} \to (\binom{2 \cdot N}{N}) \in ℤ_{\geq K}$
55		fzss2	$⊢ (\binom{2 \cdot N}{N}) \in ℤ_{\geq K} \to (1 \dots K) \subseteq (1 \dots (\binom{2 \cdot N}{N}))$
56	54 55	syl	$⊢ N \in ℤ_{\geq 4} \to (1 \dots K) \subseteq (1 \dots (\binom{2 \cdot N}{N}))$
57	56	ssrind	$⊢ N \in ℤ_{\geq 4} \to (1 \dots K) \cap ℙ \subseteq (1 \dots (\binom{2 \cdot N}{N})) \cap ℙ$
58	57	sselda	$⊢ (N \in ℤ_{\geq 4} \land k \in ((1 \dots K) \cap ℙ)) \to k \in ((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ)$
59		simpr	$⊢ (N \in ℤ_{\geq 4} \land k \in ((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ)) \to k \in ((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ)$
60	59	elin1d	$⊢ (N \in ℤ_{\geq 4} \land k \in ((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ)) \to k \in (1 \dots (\binom{2 \cdot N}{N}))$
61		elfznn	$⊢ k \in (1 \dots (\binom{2 \cdot N}{N})) \to k \in ℕ$
62	60 61	syl	$⊢ (N \in ℤ_{\geq 4} \land k \in ((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ)) \to k \in ℕ$
63	59	elin2d	$⊢ (N \in ℤ_{\geq 4} \land k \in ((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ)) \to k \in ℙ$
64	15	adantr	$⊢ (N \in ℤ_{\geq 4} \land k \in ((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ)) \to (\binom{2 \cdot N}{N}) \in ℕ$
65	63 64	pccld	$⊢ (N \in ℤ_{\geq 4} \land k \in ((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ)) \to k pCnt (\binom{2 \cdot N}{N}) \in ℕ_{0}$
66	62 65	nnexpcld	$⊢ (N \in ℤ_{\geq 4} \land k \in ((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ)) \to k^{k pCnt (\binom{2 \cdot N}{N})} \in ℕ$
67	66	nnrpd	$⊢ (N \in ℤ_{\geq 4} \land k \in ((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ)) \to k^{k pCnt (\binom{2 \cdot N}{N})} \in ℝ^{+}$
68	67	relogcld	$⊢ (N \in ℤ_{\geq 4} \land k \in ((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ)) \to \log k^{k pCnt (\binom{2 \cdot N}{N})} \in ℝ$
69	58 68	syldan	$⊢ (N \in ℤ_{\geq 4} \land k \in ((1 \dots K) \cap ℙ)) \to \log k^{k pCnt (\binom{2 \cdot N}{N})} \in ℝ$
70	30	adantr	$⊢ (N \in ℤ_{\geq 4} \land k \in ((1 \dots K) \cap ℙ)) \to \log 2 \cdot N \in ℝ$
71		elinel2	$⊢ k \in ((1 \dots K) \cap ℙ) \to k \in ℙ$
72		bposlem1	$⊢ (N \in ℕ \land k \in ℙ) \to k^{k pCnt (\binom{2 \cdot N}{N})} \leq 2 \cdot N$
73	4 71 72	syl2an	$⊢ (N \in ℤ_{\geq 4} \land k \in ((1 \dots K) \cap ℙ)) \to k^{k pCnt (\binom{2 \cdot N}{N})} \leq 2 \cdot N$
74	58 67	syldan	$⊢ (N \in ℤ_{\geq 4} \land k \in ((1 \dots K) \cap ℙ)) \to k^{k pCnt (\binom{2 \cdot N}{N})} \in ℝ^{+}$
75	74	reeflogd	$⊢ (N \in ℤ_{\geq 4} \land k \in ((1 \dots K) \cap ℙ)) \to e^{\log k^{k pCnt (\binom{2 \cdot N}{N})}} = k^{k pCnt (\binom{2 \cdot N}{N})}$
76	29	adantr	$⊢ (N \in ℤ_{\geq 4} \land k \in ((1 \dots K) \cap ℙ)) \to 2 \cdot N \in ℝ^{+}$
77	76	reeflogd	$⊢ (N \in ℤ_{\geq 4} \land k \in ((1 \dots K) \cap ℙ)) \to e^{\log 2 \cdot N} = 2 \cdot N$
78	73 75 77	3brtr4d	$⊢ (N \in ℤ_{\geq 4} \land k \in ((1 \dots K) \cap ℙ)) \to e^{\log k^{k pCnt (\binom{2 \cdot N}{N})}} \leq e^{\log 2 \cdot N}$
79		efle	$⊢ (\log k^{k pCnt (\binom{2 \cdot N}{N})} \in ℝ \land \log 2 \cdot N \in ℝ) \to (\log k^{k pCnt (\binom{2 \cdot N}{N})} \leq \log 2 \cdot N \leftrightarrow e^{\log k^{k pCnt (\binom{2 \cdot N}{N})}} \leq e^{\log 2 \cdot N})$
80	69 70 79	syl2anc	$⊢ (N \in ℤ_{\geq 4} \land k \in ((1 \dots K) \cap ℙ)) \to (\log k^{k pCnt (\binom{2 \cdot N}{N})} \leq \log 2 \cdot N \leftrightarrow e^{\log k^{k pCnt (\binom{2 \cdot N}{N})}} \leq e^{\log 2 \cdot N})$
81	78 80	mpbird	$⊢ (N \in ℤ_{\geq 4} \land k \in ((1 \dots K) \cap ℙ)) \to \log k^{k pCnt (\binom{2 \cdot N}{N})} \leq \log 2 \cdot N$
82	46 69 70 81	fsumle	$⊢ N \in ℤ_{\geq 4} \to \sum_{k \in (1 \dots K) \cap ℙ} \log k^{k pCnt (\binom{2 \cdot N}{N})} \leq \sum_{k \in (1 \dots K) \cap ℙ} \log 2 \cdot N$
83	68	recnd	$⊢ (N \in ℤ_{\geq 4} \land k \in ((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ)) \to \log k^{k pCnt (\binom{2 \cdot N}{N})} \in ℂ$
84	58 83	syldan	$⊢ (N \in ℤ_{\geq 4} \land k \in ((1 \dots K) \cap ℙ)) \to \log k^{k pCnt (\binom{2 \cdot N}{N})} \in ℂ$
85		eldifn	$⊢ k \in (((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ) ∖ ((1 \dots K) \cap ℙ)) \to \neg k \in ((1 \dots K) \cap ℙ)$
86	85	adantl	$⊢ (N \in ℤ_{\geq 4} \land k \in (((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ) ∖ ((1 \dots K) \cap ℙ))) \to \neg k \in ((1 \dots K) \cap ℙ)$
87		simpr	$⊢ (N \in ℤ_{\geq 4} \land k \in (((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ) ∖ ((1 \dots K) \cap ℙ))) \to k \in (((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ) ∖ ((1 \dots K) \cap ℙ))$
88	87	eldifad	$⊢ (N \in ℤ_{\geq 4} \land k \in (((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ) ∖ ((1 \dots K) \cap ℙ))) \to k \in ((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ)$
89	88	elin1d	$⊢ (N \in ℤ_{\geq 4} \land k \in (((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ) ∖ ((1 \dots K) \cap ℙ))) \to k \in (1 \dots (\binom{2 \cdot N}{N}))$
90	89 61	syl	$⊢ (N \in ℤ_{\geq 4} \land k \in (((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ) ∖ ((1 \dots K) \cap ℙ))) \to k \in ℕ$
91	90	adantrr	$⊢ (N \in ℤ_{\geq 4} \land (k \in (((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ) ∖ ((1 \dots K) \cap ℙ)) \land k pCnt (\binom{2 \cdot N}{N}) \in ℕ)) \to k \in ℕ$
92	91	nnred	$⊢ (N \in ℤ_{\geq 4} \land (k \in (((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ) ∖ ((1 \dots K) \cap ℙ)) \land k pCnt (\binom{2 \cdot N}{N}) \in ℕ)) \to k \in ℝ$
93	88 66	syldan	$⊢ (N \in ℤ_{\geq 4} \land k \in (((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ) ∖ ((1 \dots K) \cap ℙ))) \to k^{k pCnt (\binom{2 \cdot N}{N})} \in ℕ$
94	93	nnred	$⊢ (N \in ℤ_{\geq 4} \land k \in (((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ) ∖ ((1 \dots K) \cap ℙ))) \to k^{k pCnt (\binom{2 \cdot N}{N})} \in ℝ$
95	94	adantrr	$⊢ (N \in ℤ_{\geq 4} \land (k \in (((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ) ∖ ((1 \dots K) \cap ℙ)) \land k pCnt (\binom{2 \cdot N}{N}) \in ℕ)) \to k^{k pCnt (\binom{2 \cdot N}{N})} \in ℝ$
96	22	adantr	$⊢ (N \in ℤ_{\geq 4} \land (k \in (((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ) ∖ ((1 \dots K) \cap ℙ)) \land k pCnt (\binom{2 \cdot N}{N}) \in ℕ)) \to 2 \cdot N \in ℝ$
97	91	nncnd	$⊢ (N \in ℤ_{\geq 4} \land (k \in (((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ) ∖ ((1 \dots K) \cap ℙ)) \land k pCnt (\binom{2 \cdot N}{N}) \in ℕ)) \to k \in ℂ$
98	97	exp1d	$⊢ (N \in ℤ_{\geq 4} \land (k \in (((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ) ∖ ((1 \dots K) \cap ℙ)) \land k pCnt (\binom{2 \cdot N}{N}) \in ℕ)) \to k^{1} = k$
99	91	nnge1d	$⊢ (N \in ℤ_{\geq 4} \land (k \in (((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ) ∖ ((1 \dots K) \cap ℙ)) \land k pCnt (\binom{2 \cdot N}{N}) \in ℕ)) \to 1 \leq k$
100		simprr	$⊢ (N \in ℤ_{\geq 4} \land (k \in (((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ) ∖ ((1 \dots K) \cap ℙ)) \land k pCnt (\binom{2 \cdot N}{N}) \in ℕ)) \to k pCnt (\binom{2 \cdot N}{N}) \in ℕ$
101		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
102	100 101	eleqtrdi	$⊢ (N \in ℤ_{\geq 4} \land (k \in (((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ) ∖ ((1 \dots K) \cap ℙ)) \land k pCnt (\binom{2 \cdot N}{N}) \in ℕ)) \to k pCnt (\binom{2 \cdot N}{N}) \in ℤ_{\geq 1}$
103	92 99 102	leexp2ad	$⊢ (N \in ℤ_{\geq 4} \land (k \in (((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ) ∖ ((1 \dots K) \cap ℙ)) \land k pCnt (\binom{2 \cdot N}{N}) \in ℕ)) \to k^{1} \leq k^{k pCnt (\binom{2 \cdot N}{N})}$
104	98 103	eqbrtrrd	$⊢ (N \in ℤ_{\geq 4} \land (k \in (((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ) ∖ ((1 \dots K) \cap ℙ)) \land k pCnt (\binom{2 \cdot N}{N}) \in ℕ)) \to k \leq k^{k pCnt (\binom{2 \cdot N}{N})}$
105	4	adantr	$⊢ (N \in ℤ_{\geq 4} \land (k \in (((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ) ∖ ((1 \dots K) \cap ℙ)) \land k pCnt (\binom{2 \cdot N}{N}) \in ℕ)) \to N \in ℕ$
106	88	elin2d	$⊢ (N \in ℤ_{\geq 4} \land k \in (((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ) ∖ ((1 \dots K) \cap ℙ))) \to k \in ℙ$
107	106	adantrr	$⊢ (N \in ℤ_{\geq 4} \land (k \in (((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ) ∖ ((1 \dots K) \cap ℙ)) \land k pCnt (\binom{2 \cdot N}{N}) \in ℕ)) \to k \in ℙ$
108	105 107 72	syl2anc	$⊢ (N \in ℤ_{\geq 4} \land (k \in (((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ) ∖ ((1 \dots K) \cap ℙ)) \land k pCnt (\binom{2 \cdot N}{N}) \in ℕ)) \to k^{k pCnt (\binom{2 \cdot N}{N})} \leq 2 \cdot N$
109	92 95 96 104 108	letrd	$⊢ (N \in ℤ_{\geq 4} \land (k \in (((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ) ∖ ((1 \dots K) \cap ℙ)) \land k pCnt (\binom{2 \cdot N}{N}) \in ℕ)) \to k \leq 2 \cdot N$
110		elfzle2	$⊢ k \in (1 \dots (\binom{2 \cdot N}{N})) \to k \leq (\binom{2 \cdot N}{N})$
111	89 110	syl	$⊢ (N \in ℤ_{\geq 4} \land k \in (((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ) ∖ ((1 \dots K) \cap ℙ))) \to k \leq (\binom{2 \cdot N}{N})$
112	111	adantrr	$⊢ (N \in ℤ_{\geq 4} \land (k \in (((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ) ∖ ((1 \dots K) \cap ℙ)) \land k pCnt (\binom{2 \cdot N}{N}) \in ℕ)) \to k \leq (\binom{2 \cdot N}{N})$
113	49	adantr	$⊢ (N \in ℤ_{\geq 4} \land (k \in (((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ) ∖ ((1 \dots K) \cap ℙ)) \land k pCnt (\binom{2 \cdot N}{N}) \in ℕ)) \to (\binom{2 \cdot N}{N}) \in ℝ$
114		lemin	$⊢ (k \in ℝ \land 2 \cdot N \in ℝ \land (\binom{2 \cdot N}{N}) \in ℝ) \to (k \leq if (2 \cdot N \leq (\binom{2 \cdot N}{N}), 2 \cdot N, (\binom{2 \cdot N}{N})) \leftrightarrow (k \leq 2 \cdot N \land k \leq (\binom{2 \cdot N}{N})))$
115	92 96 113 114	syl3anc	$⊢ (N \in ℤ_{\geq 4} \land (k \in (((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ) ∖ ((1 \dots K) \cap ℙ)) \land k pCnt (\binom{2 \cdot N}{N}) \in ℕ)) \to (k \leq if (2 \cdot N \leq (\binom{2 \cdot N}{N}), 2 \cdot N, (\binom{2 \cdot N}{N})) \leftrightarrow (k \leq 2 \cdot N \land k \leq (\binom{2 \cdot N}{N})))$
116	109 112 115	mpbir2and	$⊢ (N \in ℤ_{\geq 4} \land (k \in (((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ) ∖ ((1 \dots K) \cap ℙ)) \land k pCnt (\binom{2 \cdot N}{N}) \in ℕ)) \to k \leq if (2 \cdot N \leq (\binom{2 \cdot N}{N}), 2 \cdot N, (\binom{2 \cdot N}{N}))$
117	116 1	breqtrrdi	$⊢ (N \in ℤ_{\geq 4} \land (k \in (((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ) ∖ ((1 \dots K) \cap ℙ)) \land k pCnt (\binom{2 \cdot N}{N}) \in ℕ)) \to k \leq K$
118	37	adantr	$⊢ (N \in ℤ_{\geq 4} \land (k \in (((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ) ∖ ((1 \dots K) \cap ℙ)) \land k pCnt (\binom{2 \cdot N}{N}) \in ℕ)) \to K \in ℕ$
119	118	nnzd	$⊢ (N \in ℤ_{\geq 4} \land (k \in (((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ) ∖ ((1 \dots K) \cap ℙ)) \land k pCnt (\binom{2 \cdot N}{N}) \in ℕ)) \to K \in ℤ$
120		fznn	$⊢ K \in ℤ \to (k \in (1 \dots K) \leftrightarrow (k \in ℕ \land k \leq K))$
121	119 120	syl	$⊢ (N \in ℤ_{\geq 4} \land (k \in (((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ) ∖ ((1 \dots K) \cap ℙ)) \land k pCnt (\binom{2 \cdot N}{N}) \in ℕ)) \to (k \in (1 \dots K) \leftrightarrow (k \in ℕ \land k \leq K))$
122	91 117 121	mpbir2and	$⊢ (N \in ℤ_{\geq 4} \land (k \in (((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ) ∖ ((1 \dots K) \cap ℙ)) \land k pCnt (\binom{2 \cdot N}{N}) \in ℕ)) \to k \in (1 \dots K)$
123	122 107	elind	$⊢ (N \in ℤ_{\geq 4} \land (k \in (((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ) ∖ ((1 \dots K) \cap ℙ)) \land k pCnt (\binom{2 \cdot N}{N}) \in ℕ)) \to k \in ((1 \dots K) \cap ℙ)$
124	123	expr	$⊢ (N \in ℤ_{\geq 4} \land k \in (((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ) ∖ ((1 \dots K) \cap ℙ))) \to (k pCnt (\binom{2 \cdot N}{N}) \in ℕ \to k \in ((1 \dots K) \cap ℙ))$
125	86 124	mtod	$⊢ (N \in ℤ_{\geq 4} \land k \in (((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ) ∖ ((1 \dots K) \cap ℙ))) \to \neg k pCnt (\binom{2 \cdot N}{N}) \in ℕ$
126	88 65	syldan	$⊢ (N \in ℤ_{\geq 4} \land k \in (((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ) ∖ ((1 \dots K) \cap ℙ))) \to k pCnt (\binom{2 \cdot N}{N}) \in ℕ_{0}$
127		elnn0	$⊢ k pCnt (\binom{2 \cdot N}{N}) \in ℕ_{0} \leftrightarrow (k pCnt (\binom{2 \cdot N}{N}) \in ℕ \lor k pCnt (\binom{2 \cdot N}{N}) = 0)$
128	126 127	sylib	$⊢ (N \in ℤ_{\geq 4} \land k \in (((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ) ∖ ((1 \dots K) \cap ℙ))) \to (k pCnt (\binom{2 \cdot N}{N}) \in ℕ \lor k pCnt (\binom{2 \cdot N}{N}) = 0)$
129	128	ord	$⊢ (N \in ℤ_{\geq 4} \land k \in (((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ) ∖ ((1 \dots K) \cap ℙ))) \to (\neg k pCnt (\binom{2 \cdot N}{N}) \in ℕ \to k pCnt (\binom{2 \cdot N}{N}) = 0)$
130	125 129	mpd	$⊢ (N \in ℤ_{\geq 4} \land k \in (((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ) ∖ ((1 \dots K) \cap ℙ))) \to k pCnt (\binom{2 \cdot N}{N}) = 0$
131	130	oveq2d	$⊢ (N \in ℤ_{\geq 4} \land k \in (((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ) ∖ ((1 \dots K) \cap ℙ))) \to k^{k pCnt (\binom{2 \cdot N}{N})} = k^{0}$
132	90	nncnd	$⊢ (N \in ℤ_{\geq 4} \land k \in (((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ) ∖ ((1 \dots K) \cap ℙ))) \to k \in ℂ$
133	132	exp0d	$⊢ (N \in ℤ_{\geq 4} \land k \in (((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ) ∖ ((1 \dots K) \cap ℙ))) \to k^{0} = 1$
134	131 133	eqtrd	$⊢ (N \in ℤ_{\geq 4} \land k \in (((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ) ∖ ((1 \dots K) \cap ℙ))) \to k^{k pCnt (\binom{2 \cdot N}{N})} = 1$
135	134	fveq2d	$⊢ (N \in ℤ_{\geq 4} \land k \in (((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ) ∖ ((1 \dots K) \cap ℙ))) \to \log k^{k pCnt (\binom{2 \cdot N}{N})} = \log 1$
136		log1	$⊢ \log 1 = 0$
137	135 136	eqtrdi	$⊢ (N \in ℤ_{\geq 4} \land k \in (((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ) ∖ ((1 \dots K) \cap ℙ))) \to \log k^{k pCnt (\binom{2 \cdot N}{N})} = 0$
138		fzfid	$⊢ N \in ℤ_{\geq 4} \to (1 \dots (\binom{2 \cdot N}{N})) \in Fin$
139		inss1	$⊢ (1 \dots (\binom{2 \cdot N}{N})) \cap ℙ \subseteq (1 \dots (\binom{2 \cdot N}{N}))$
140		ssfi	$⊢ ((1 \dots (\binom{2 \cdot N}{N})) \in Fin \land (1 \dots (\binom{2 \cdot N}{N})) \cap ℙ \subseteq (1 \dots (\binom{2 \cdot N}{N}))) \to (1 \dots (\binom{2 \cdot N}{N})) \cap ℙ \in Fin$
141	138 139 140	sylancl	$⊢ N \in ℤ_{\geq 4} \to (1 \dots (\binom{2 \cdot N}{N})) \cap ℙ \in Fin$
142	57 84 137 141	fsumss	$⊢ N \in ℤ_{\geq 4} \to \sum_{k \in (1 \dots K) \cap ℙ} \log k^{k pCnt (\binom{2 \cdot N}{N})} = \sum_{k \in (1 \dots (\binom{2 \cdot N}{N})) \cap ℙ} \log k^{k pCnt (\binom{2 \cdot N}{N})}$
143	62	nnrpd	$⊢ (N \in ℤ_{\geq 4} \land k \in ((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ)) \to k \in ℝ^{+}$
144	65	nn0zd	$⊢ (N \in ℤ_{\geq 4} \land k \in ((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ)) \to k pCnt (\binom{2 \cdot N}{N}) \in ℤ$
145		relogexp	$⊢ (k \in ℝ^{+} \land k pCnt (\binom{2 \cdot N}{N}) \in ℤ) \to \log k^{k pCnt (\binom{2 \cdot N}{N})} = (k pCnt (\binom{2 \cdot N}{N})) \log k$
146	143 144 145	syl2anc	$⊢ (N \in ℤ_{\geq 4} \land k \in ((1 \dots (\binom{2 \cdot N}{N})) \cap ℙ)) \to \log k^{k pCnt (\binom{2 \cdot N}{N})} = (k pCnt (\binom{2 \cdot N}{N})) \log k$
147	146	sumeq2dv	$⊢ N \in ℤ_{\geq 4} \to \sum_{k \in (1 \dots (\binom{2 \cdot N}{N})) \cap ℙ} \log k^{k pCnt (\binom{2 \cdot N}{N})} = \sum_{k \in (1 \dots (\binom{2 \cdot N}{N})) \cap ℙ} (k pCnt (\binom{2 \cdot N}{N})) \log k$
148		pclogsum	$⊢ (\binom{2 \cdot N}{N}) \in ℕ \to \sum_{k \in (1 \dots (\binom{2 \cdot N}{N})) \cap ℙ} (k pCnt (\binom{2 \cdot N}{N})) \log k = \log (\binom{2 \cdot N}{N})$
149	15 148	syl	$⊢ N \in ℤ_{\geq 4} \to \sum_{k \in (1 \dots (\binom{2 \cdot N}{N})) \cap ℙ} (k pCnt (\binom{2 \cdot N}{N})) \log k = \log (\binom{2 \cdot N}{N})$
150	142 147 149	3eqtrd	$⊢ N \in ℤ_{\geq 4} \to \sum_{k \in (1 \dots K) \cap ℙ} \log k^{k pCnt (\binom{2 \cdot N}{N})} = \log (\binom{2 \cdot N}{N})$
151	30	recnd	$⊢ N \in ℤ_{\geq 4} \to \log 2 \cdot N \in ℂ$
152		fsumconst	$⊢ ((1 \dots K) \cap ℙ \in Fin \land \log 2 \cdot N \in ℂ) \to \sum_{k \in (1 \dots K) \cap ℙ} \log 2 \cdot N = \|(1 \dots K) \cap ℙ\| \log 2 \cdot N$
153	46 151 152	syl2anc	$⊢ N \in ℤ_{\geq 4} \to \sum_{k \in (1 \dots K) \cap ℙ} \log 2 \cdot N = \|(1 \dots K) \cap ℙ\| \log 2 \cdot N$
154		2eluzge1	$⊢ 2 \in ℤ_{\geq 1}$
155		ppival2g	$⊢ (K \in ℤ \land 2 \in ℤ_{\geq 1}) \to \underline{π} (K) = \|(1 \dots K) \cap ℙ\|$
156	47 154 155	sylancl	$⊢ N \in ℤ_{\geq 4} \to \underline{π} (K) = \|(1 \dots K) \cap ℙ\|$
157	156	oveq1d	$⊢ N \in ℤ_{\geq 4} \to \underline{π} (K) \log 2 \cdot N = \|(1 \dots K) \cap ℙ\| \log 2 \cdot N$
158	153 157	eqtr4d	$⊢ N \in ℤ_{\geq 4} \to \sum_{k \in (1 \dots K) \cap ℙ} \log 2 \cdot N = \underline{π} (K) \log 2 \cdot N$
159	82 150 158	3brtr3d	$⊢ N \in ℤ_{\geq 4} \to \log (\binom{2 \cdot N}{N}) \leq \underline{π} (K) \log 2 \cdot N$
160		min1	$⊢ (2 \cdot N \in ℝ \land (\binom{2 \cdot N}{N}) \in ℝ) \to if (2 \cdot N \leq (\binom{2 \cdot N}{N}), 2 \cdot N, (\binom{2 \cdot N}{N})) \leq 2 \cdot N$
161	22 49 160	syl2anc	$⊢ N \in ℤ_{\geq 4} \to if (2 \cdot N \leq (\binom{2 \cdot N}{N}), 2 \cdot N, (\binom{2 \cdot N}{N})) \leq 2 \cdot N$
162	1 161	eqbrtrid	$⊢ N \in ℤ_{\geq 4} \to K \leq 2 \cdot N$
163		ppiwordi	$⊢ (K \in ℝ \land 2 \cdot N \in ℝ \land K \leq 2 \cdot N) \to \underline{π} (K) \leq \underline{π} (2 \cdot N)$
164	38 22 162 163	syl3anc	$⊢ N \in ℤ_{\geq 4} \to \underline{π} (K) \leq \underline{π} (2 \cdot N)$
165		1red	$⊢ N \in ℤ_{\geq 4} \to 1 \in ℝ$
166		2re	$⊢ 2 \in ℝ$
167	166	a1i	$⊢ N \in ℤ_{\geq 4} \to 2 \in ℝ$
168		1lt2	$⊢ 1 < 2$
169	168	a1i	$⊢ N \in ℤ_{\geq 4} \to 1 < 2$
170		2t1e2	$⊢ 2 \cdot 1 = 2$
171	4	nnge1d	$⊢ N \in ℤ_{\geq 4} \to 1 \leq N$
172		eluzelre	$⊢ N \in ℤ_{\geq 4} \to N \in ℝ$
173		2pos	$⊢ 0 < 2$
174	166 173	pm3.2i	$⊢ (2 \in ℝ \land 0 < 2)$
175	174	a1i	$⊢ N \in ℤ_{\geq 4} \to (2 \in ℝ \land 0 < 2)$
176		lemul2	$⊢ (1 \in ℝ \land N \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (1 \leq N \leftrightarrow 2 \cdot 1 \leq 2 \cdot N)$
177	165 172 175 176	syl3anc	$⊢ N \in ℤ_{\geq 4} \to (1 \leq N \leftrightarrow 2 \cdot 1 \leq 2 \cdot N)$
178	171 177	mpbid	$⊢ N \in ℤ_{\geq 4} \to 2 \cdot 1 \leq 2 \cdot N$
179	170 178	eqbrtrrid	$⊢ N \in ℤ_{\geq 4} \to 2 \leq 2 \cdot N$
180	165 167 22 169 179	ltletrd	$⊢ N \in ℤ_{\geq 4} \to 1 < 2 \cdot N$
181	22 180	rplogcld	$⊢ N \in ℤ_{\geq 4} \to \log 2 \cdot N \in ℝ^{+}$
182	41 25 181	lemul1d	$⊢ N \in ℤ_{\geq 4} \to (\underline{π} (K) \leq \underline{π} (2 \cdot N) \leftrightarrow \underline{π} (K) \log 2 \cdot N \leq \underline{π} (2 \cdot N) \log 2 \cdot N)$
183	164 182	mpbid	$⊢ N \in ℤ_{\geq 4} \to \underline{π} (K) \log 2 \cdot N \leq \underline{π} (2 \cdot N) \log 2 \cdot N$
184	17 42 31 159 183	letrd	$⊢ N \in ℤ_{\geq 4} \to \log (\binom{2 \cdot N}{N}) \leq \underline{π} (2 \cdot N) \log 2 \cdot N$
185	11 17 31 35 184	ltletrd	$⊢ N \in ℤ_{\geq 4} \to \log (\frac{4^{N}}{N}) < \underline{π} (2 \cdot N) \log 2 \cdot N$

Metamath Proof Explorer

Theorem chebbnd1lem1

Proof