chtublem

		Ref	Expression
	Assertion	chtublem	$⊢ N \in ℕ \to θ (2 \cdot N - 1) \leq θ (N) + \log 4 (N - 1)$

Proof

Step	Hyp	Ref	Expression
1		2nn	$⊢ 2 \in ℕ$
2		nnmulcl	$⊢ (2 \in ℕ \land N \in ℕ) \to 2 \cdot N \in ℕ$
3	1 2	mpan	$⊢ N \in ℕ \to 2 \cdot N \in ℕ$
4	3	nnred	$⊢ N \in ℕ \to 2 \cdot N \in ℝ$
5		peano2rem	$⊢ 2 \cdot N \in ℝ \to 2 \cdot N - 1 \in ℝ$
6	4 5	syl	$⊢ N \in ℕ \to 2 \cdot N - 1 \in ℝ$
7		chtcl	$⊢ 2 \cdot N - 1 \in ℝ \to θ (2 \cdot N - 1) \in ℝ$
8	6 7	syl	$⊢ N \in ℕ \to θ (2 \cdot N - 1) \in ℝ$
9		nnre	$⊢ N \in ℕ \to N \in ℝ$
10		chtcl	$⊢ N \in ℝ \to θ (N) \in ℝ$
11	9 10	syl	$⊢ N \in ℕ \to θ (N) \in ℝ$
12		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
13		2m1e1	$⊢ 2 - 1 = 1$
14	13	oveq2i	$⊢ 2 \cdot N - (2 - 1) = 2 \cdot N - 1$
15	3	nncnd	$⊢ N \in ℕ \to 2 \cdot N \in ℂ$
16		2cn	$⊢ 2 \in ℂ$
17		ax-1cn	$⊢ 1 \in ℂ$
18		subsub	$⊢ (2 \cdot N \in ℂ \land 2 \in ℂ \land 1 \in ℂ) \to 2 \cdot N - (2 - 1) = 2 \cdot N - 2 + 1$
19	16 17 18	mp3an23	$⊢ 2 \cdot N \in ℂ \to 2 \cdot N - (2 - 1) = 2 \cdot N - 2 + 1$
20	15 19	syl	$⊢ N \in ℕ \to 2 \cdot N - (2 - 1) = 2 \cdot N - 2 + 1$
21		nncn	$⊢ N \in ℕ \to N \in ℂ$
22		subdi	$⊢ (2 \in ℂ \land N \in ℂ \land 1 \in ℂ) \to 2 (N - 1) = 2 \cdot N - 2 \cdot 1$
23	16 17 22	mp3an13	$⊢ N \in ℂ \to 2 (N - 1) = 2 \cdot N - 2 \cdot 1$
24	21 23	syl	$⊢ N \in ℕ \to 2 (N - 1) = 2 \cdot N - 2 \cdot 1$
25		2t1e2	$⊢ 2 \cdot 1 = 2$
26	25	oveq2i	$⊢ 2 \cdot N - 2 \cdot 1 = 2 \cdot N - 2$
27	24 26	eqtrdi	$⊢ N \in ℕ \to 2 (N - 1) = 2 \cdot N - 2$
28	27	oveq1d	$⊢ N \in ℕ \to 2 (N - 1) + 1 = 2 \cdot N - 2 + 1$
29	20 28	eqtr4d	$⊢ N \in ℕ \to 2 \cdot N - (2 - 1) = 2 (N - 1) + 1$
30	14 29	eqtr3id	$⊢ N \in ℕ \to 2 \cdot N - 1 = 2 (N - 1) + 1$
31		2nn0	$⊢ 2 \in ℕ_{0}$
32		nnm1nn0	$⊢ N \in ℕ \to N - 1 \in ℕ_{0}$
33		nn0mulcl	$⊢ (2 \in ℕ_{0} \land N - 1 \in ℕ_{0}) \to 2 (N - 1) \in ℕ_{0}$
34	31 32 33	sylancr	$⊢ N \in ℕ \to 2 (N - 1) \in ℕ_{0}$
35		nn0p1nn	$⊢ 2 (N - 1) \in ℕ_{0} \to 2 (N - 1) + 1 \in ℕ$
36	34 35	syl	$⊢ N \in ℕ \to 2 (N - 1) + 1 \in ℕ$
37	30 36	eqeltrd	$⊢ N \in ℕ \to 2 \cdot N - 1 \in ℕ$
38		nnnn0	$⊢ 2 \cdot N - 1 \in ℕ \to 2 \cdot N - 1 \in ℕ_{0}$
39	37 38	syl	$⊢ N \in ℕ \to 2 \cdot N - 1 \in ℕ_{0}$
40		1re	$⊢ 1 \in ℝ$
41	40	a1i	$⊢ N \in ℕ \to 1 \in ℝ$
42		nnge1	$⊢ N \in ℕ \to 1 \leq N$
43	41 9 9 42	leadd2dd	$⊢ N \in ℕ \to N + 1 \leq N + N$
44	21	2timesd	$⊢ N \in ℕ \to 2 \cdot N = N + N$
45	43 44	breqtrrd	$⊢ N \in ℕ \to N + 1 \leq 2 \cdot N$
46		leaddsub	$⊢ (N \in ℝ \land 1 \in ℝ \land 2 \cdot N \in ℝ) \to (N + 1 \leq 2 \cdot N \leftrightarrow N \leq 2 \cdot N - 1)$
47	9 41 4 46	syl3anc	$⊢ N \in ℕ \to (N + 1 \leq 2 \cdot N \leftrightarrow N \leq 2 \cdot N - 1)$
48	45 47	mpbid	$⊢ N \in ℕ \to N \leq 2 \cdot N - 1$
49		elfz2nn0	$⊢ N \in (0 \dots 2 \cdot N - 1) \leftrightarrow (N \in ℕ_{0} \land 2 \cdot N - 1 \in ℕ_{0} \land N \leq 2 \cdot N - 1)$
50	12 39 48 49	syl3anbrc	$⊢ N \in ℕ \to N \in (0 \dots 2 \cdot N - 1)$
51		bccl2	$⊢ N \in (0 \dots 2 \cdot N - 1) \to (\binom{2 \cdot N - 1}{N}) \in ℕ$
52	50 51	syl	$⊢ N \in ℕ \to (\binom{2 \cdot N - 1}{N}) \in ℕ$
53	52	nnrpd	$⊢ N \in ℕ \to (\binom{2 \cdot N - 1}{N}) \in ℝ^{+}$
54	53	relogcld	$⊢ N \in ℕ \to \log (\binom{2 \cdot N - 1}{N}) \in ℝ$
55	11 54	readdcld	$⊢ N \in ℕ \to θ (N) + \log (\binom{2 \cdot N - 1}{N}) \in ℝ$
56		4re	$⊢ 4 \in ℝ$
57		4pos	$⊢ 0 < 4$
58	56 57	elrpii	$⊢ 4 \in ℝ^{+}$
59		relogcl	$⊢ 4 \in ℝ^{+} \to \log 4 \in ℝ$
60	58 59	ax-mp	$⊢ \log 4 \in ℝ$
61	32	nn0red	$⊢ N \in ℕ \to N - 1 \in ℝ$
62		remulcl	$⊢ (\log 4 \in ℝ \land N - 1 \in ℝ) \to \log 4 (N - 1) \in ℝ$
63	60 61 62	sylancr	$⊢ N \in ℕ \to \log 4 (N - 1) \in ℝ$
64	11 63	readdcld	$⊢ N \in ℕ \to θ (N) + \log 4 (N - 1) \in ℝ$
65		iftrue	$⊢ p \leq 2 \cdot N - 1 \to if (p \leq 2 \cdot N - 1, 1, 0) = 1$
66	65	adantl	$⊢ ((N \in ℕ \land p \in ℙ) \land p \leq 2 \cdot N - 1) \to if (p \leq 2 \cdot N - 1, 1, 0) = 1$
67		simpr	$⊢ (N \in ℕ \land p \in ℙ) \to p \in ℙ$
68	52	adantr	$⊢ (N \in ℕ \land p \in ℙ) \to (\binom{2 \cdot N - 1}{N}) \in ℕ$
69	67 68	pccld	$⊢ (N \in ℕ \land p \in ℙ) \to p pCnt (\binom{2 \cdot N - 1}{N}) \in ℕ_{0}$
70		nn0addge1	$⊢ (1 \in ℝ \land p pCnt (\binom{2 \cdot N - 1}{N}) \in ℕ_{0}) \to 1 \leq 1 + (p pCnt (\binom{2 \cdot N - 1}{N}))$
71	40 69 70	sylancr	$⊢ (N \in ℕ \land p \in ℙ) \to 1 \leq 1 + (p pCnt (\binom{2 \cdot N - 1}{N}))$
72		iftrue	$⊢ p \leq N \to if (p \leq N, 1, 0) = 1$
73	72	oveq1d	$⊢ p \leq N \to if (p \leq N, 1, 0) + (p pCnt (\binom{2 \cdot N - 1}{N})) = 1 + (p pCnt (\binom{2 \cdot N - 1}{N}))$
74	73	breq2d	$⊢ p \leq N \to (1 \leq if (p \leq N, 1, 0) + (p pCnt (\binom{2 \cdot N - 1}{N})) \leftrightarrow 1 \leq 1 + (p pCnt (\binom{2 \cdot N - 1}{N})))$
75	71 74	syl5ibrcom	$⊢ (N \in ℕ \land p \in ℙ) \to (p \leq N \to 1 \leq if (p \leq N, 1, 0) + (p pCnt (\binom{2 \cdot N - 1}{N})))$
76	75	adantr	$⊢ ((N \in ℕ \land p \in ℙ) \land p \leq 2 \cdot N - 1) \to (p \leq N \to 1 \leq if (p \leq N, 1, 0) + (p pCnt (\binom{2 \cdot N - 1}{N})))$
77		prmnn	$⊢ p \in ℙ \to p \in ℕ$
78	77	ad2antlr	$⊢ ((N \in ℕ \land p \in ℙ) \land (p \leq 2 \cdot N - 1 \land \neg p \leq N)) \to p \in ℕ$
79		simprl	$⊢ ((N \in ℕ \land p \in ℙ) \land (p \leq 2 \cdot N - 1 \land \neg p \leq N)) \to p \leq 2 \cdot N - 1$
80		prmz	$⊢ p \in ℙ \to p \in ℤ$
81	37	nnzd	$⊢ N \in ℕ \to 2 \cdot N - 1 \in ℤ$
82		eluz	$⊢ (p \in ℤ \land 2 \cdot N - 1 \in ℤ) \to (2 \cdot N - 1 \in ℤ_{\geq p} \leftrightarrow p \leq 2 \cdot N - 1)$
83	80 81 82	syl2anr	$⊢ (N \in ℕ \land p \in ℙ) \to (2 \cdot N - 1 \in ℤ_{\geq p} \leftrightarrow p \leq 2 \cdot N - 1)$
84	83	adantr	$⊢ ((N \in ℕ \land p \in ℙ) \land (p \leq 2 \cdot N - 1 \land \neg p \leq N)) \to (2 \cdot N - 1 \in ℤ_{\geq p} \leftrightarrow p \leq 2 \cdot N - 1)$
85	79 84	mpbird	$⊢ ((N \in ℕ \land p \in ℙ) \land (p \leq 2 \cdot N - 1 \land \neg p \leq N)) \to 2 \cdot N - 1 \in ℤ_{\geq p}$
86		dvdsfac	$⊢ (p \in ℕ \land 2 \cdot N - 1 \in ℤ_{\geq p}) \to p ∥ (2 \cdot N - 1)!$
87	78 85 86	syl2anc	$⊢ ((N \in ℕ \land p \in ℙ) \land (p \leq 2 \cdot N - 1 \land \neg p \leq N)) \to p ∥ (2 \cdot N - 1)!$
88		id	$⊢ p \in ℙ \to p \in ℙ$
89	39	faccld	$⊢ N \in ℕ \to (2 \cdot N - 1)! \in ℕ$
90		pcelnn	$⊢ (p \in ℙ \land (2 \cdot N - 1)! \in ℕ) \to (p pCnt (2 \cdot N - 1)! \in ℕ \leftrightarrow p ∥ (2 \cdot N - 1)!)$
91	88 89 90	syl2anr	$⊢ (N \in ℕ \land p \in ℙ) \to (p pCnt (2 \cdot N - 1)! \in ℕ \leftrightarrow p ∥ (2 \cdot N - 1)!)$
92	91	adantr	$⊢ ((N \in ℕ \land p \in ℙ) \land (p \leq 2 \cdot N - 1 \land \neg p \leq N)) \to (p pCnt (2 \cdot N - 1)! \in ℕ \leftrightarrow p ∥ (2 \cdot N - 1)!)$
93	87 92	mpbird	$⊢ ((N \in ℕ \land p \in ℙ) \land (p \leq 2 \cdot N - 1 \land \neg p \leq N)) \to p pCnt (2 \cdot N - 1)! \in ℕ$
94	93	nnge1d	$⊢ ((N \in ℕ \land p \in ℙ) \land (p \leq 2 \cdot N - 1 \land \neg p \leq N)) \to 1 \leq p pCnt (2 \cdot N - 1)!$
95		iffalse	$⊢ \neg p \leq N \to if (p \leq N, 1, 0) = 0$
96	95	oveq1d	$⊢ \neg p \leq N \to if (p \leq N, 1, 0) + (p pCnt (\binom{2 \cdot N - 1}{N})) = 0 + (p pCnt (\binom{2 \cdot N - 1}{N}))$
97	96	ad2antll	$⊢ ((N \in ℕ \land p \in ℙ) \land (p \leq 2 \cdot N - 1 \land \neg p \leq N)) \to if (p \leq N, 1, 0) + (p pCnt (\binom{2 \cdot N - 1}{N})) = 0 + (p pCnt (\binom{2 \cdot N - 1}{N}))$
98	69	nn0cnd	$⊢ (N \in ℕ \land p \in ℙ) \to p pCnt (\binom{2 \cdot N - 1}{N}) \in ℂ$
99	98	addid2d	$⊢ (N \in ℕ \land p \in ℙ) \to 0 + (p pCnt (\binom{2 \cdot N - 1}{N})) = p pCnt (\binom{2 \cdot N - 1}{N})$
100	99	adantr	$⊢ ((N \in ℕ \land p \in ℙ) \land (p \leq 2 \cdot N - 1 \land \neg p \leq N)) \to 0 + (p pCnt (\binom{2 \cdot N - 1}{N})) = p pCnt (\binom{2 \cdot N - 1}{N})$
101		bcval2	$⊢ N \in (0 \dots 2 \cdot N - 1) \to (\binom{2 \cdot N - 1}{N}) = \frac{(2 \cdot N - 1)!}{(2 \cdot N - 1 - N)! N!}$
102	50 101	syl	$⊢ N \in ℕ \to (\binom{2 \cdot N - 1}{N}) = \frac{(2 \cdot N - 1)!}{(2 \cdot N - 1 - N)! N!}$
103	32	nn0cnd	$⊢ N \in ℕ \to N - 1 \in ℂ$
104	17	a1i	$⊢ N \in ℕ \to 1 \in ℂ$
105	44	oveq1d	$⊢ N \in ℕ \to 2 \cdot N - 1 = N + N - 1$
106	21 21 104 105	assraddsubd	$⊢ N \in ℕ \to 2 \cdot N - 1 = N + N - 1$
107	21 103 106	mvrladdd	$⊢ N \in ℕ \to 2 \cdot N - 1 - N = N - 1$
108	107	fveq2d	$⊢ N \in ℕ \to (2 \cdot N - 1 - N)! = (N - 1)!$
109	108	oveq1d	$⊢ N \in ℕ \to (2 \cdot N - 1 - N)! N! = (N - 1)! N!$
110	109	oveq2d	$⊢ N \in ℕ \to \frac{(2 \cdot N - 1)!}{(2 \cdot N - 1 - N)! N!} = \frac{(2 \cdot N - 1)!}{(N - 1)! N!}$
111	102 110	eqtrd	$⊢ N \in ℕ \to (\binom{2 \cdot N - 1}{N}) = \frac{(2 \cdot N - 1)!}{(N - 1)! N!}$
112	111	adantr	$⊢ (N \in ℕ \land p \in ℙ) \to (\binom{2 \cdot N - 1}{N}) = \frac{(2 \cdot N - 1)!}{(N - 1)! N!}$
113	112	oveq2d	$⊢ (N \in ℕ \land p \in ℙ) \to p pCnt (\binom{2 \cdot N - 1}{N}) = p pCnt (\frac{(2 \cdot N - 1)!}{(N - 1)! N!})$
114		nnz	$⊢ (2 \cdot N - 1)! \in ℕ \to (2 \cdot N - 1)! \in ℤ$
115		nnne0	$⊢ (2 \cdot N - 1)! \in ℕ \to (2 \cdot N - 1)! \neq 0$
116	114 115	jca	$⊢ (2 \cdot N - 1)! \in ℕ \to ((2 \cdot N - 1)! \in ℤ \land (2 \cdot N - 1)! \neq 0)$
117	89 116	syl	$⊢ N \in ℕ \to ((2 \cdot N - 1)! \in ℤ \land (2 \cdot N - 1)! \neq 0)$
118	117	adantr	$⊢ (N \in ℕ \land p \in ℙ) \to ((2 \cdot N - 1)! \in ℤ \land (2 \cdot N - 1)! \neq 0)$
119	32	faccld	$⊢ N \in ℕ \to (N - 1)! \in ℕ$
120	12	faccld	$⊢ N \in ℕ \to N! \in ℕ$
121	119 120	nnmulcld	$⊢ N \in ℕ \to (N - 1)! N! \in ℕ$
122	121	adantr	$⊢ (N \in ℕ \land p \in ℙ) \to (N - 1)! N! \in ℕ$
123		pcdiv	$⊢ (p \in ℙ \land ((2 \cdot N - 1)! \in ℤ \land (2 \cdot N - 1)! \neq 0) \land (N - 1)! N! \in ℕ) \to p pCnt (\frac{(2 \cdot N - 1)!}{(N - 1)! N!}) = (p pCnt (2 \cdot N - 1)!) - (p pCnt (N - 1)! N!)$
124	67 118 122 123	syl3anc	$⊢ (N \in ℕ \land p \in ℙ) \to p pCnt (\frac{(2 \cdot N - 1)!}{(N - 1)! N!}) = (p pCnt (2 \cdot N - 1)!) - (p pCnt (N - 1)! N!)$
125		nnz	$⊢ (N - 1)! \in ℕ \to (N - 1)! \in ℤ$
126		nnne0	$⊢ (N - 1)! \in ℕ \to (N - 1)! \neq 0$
127	125 126	jca	$⊢ (N - 1)! \in ℕ \to ((N - 1)! \in ℤ \land (N - 1)! \neq 0)$
128	119 127	syl	$⊢ N \in ℕ \to ((N - 1)! \in ℤ \land (N - 1)! \neq 0)$
129	128	adantr	$⊢ (N \in ℕ \land p \in ℙ) \to ((N - 1)! \in ℤ \land (N - 1)! \neq 0)$
130		nnz	$⊢ N! \in ℕ \to N! \in ℤ$
131		nnne0	$⊢ N! \in ℕ \to N! \neq 0$
132	130 131	jca	$⊢ N! \in ℕ \to (N! \in ℤ \land N! \neq 0)$
133	120 132	syl	$⊢ N \in ℕ \to (N! \in ℤ \land N! \neq 0)$
134	133	adantr	$⊢ (N \in ℕ \land p \in ℙ) \to (N! \in ℤ \land N! \neq 0)$
135		pcmul	$⊢ (p \in ℙ \land ((N - 1)! \in ℤ \land (N - 1)! \neq 0) \land (N! \in ℤ \land N! \neq 0)) \to p pCnt (N - 1)! N! = (p pCnt (N - 1)!) + (p pCnt N!)$
136	67 129 134 135	syl3anc	$⊢ (N \in ℕ \land p \in ℙ) \to p pCnt (N - 1)! N! = (p pCnt (N - 1)!) + (p pCnt N!)$
137	136	oveq2d	$⊢ (N \in ℕ \land p \in ℙ) \to (p pCnt (2 \cdot N - 1)!) - (p pCnt (N - 1)! N!) = (p pCnt (2 \cdot N - 1)!) - ((p pCnt (N - 1)!) + (p pCnt N!))$
138	113 124 137	3eqtrd	$⊢ (N \in ℕ \land p \in ℙ) \to p pCnt (\binom{2 \cdot N - 1}{N}) = (p pCnt (2 \cdot N - 1)!) - ((p pCnt (N - 1)!) + (p pCnt N!))$
139	138	adantr	$⊢ ((N \in ℕ \land p \in ℙ) \land (p \leq 2 \cdot N - 1 \land \neg p \leq N)) \to p pCnt (\binom{2 \cdot N - 1}{N}) = (p pCnt (2 \cdot N - 1)!) - ((p pCnt (N - 1)!) + (p pCnt N!))$
140		simprr	$⊢ ((N \in ℕ \land p \in ℙ) \land (p \leq 2 \cdot N - 1 \land \neg p \leq N)) \to \neg p \leq N$
141		prmfac1	$⊢ (N \in ℕ_{0} \land p \in ℙ \land p ∥ N!) \to p \leq N$
142	141	3expia	$⊢ (N \in ℕ_{0} \land p \in ℙ) \to (p ∥ N! \to p \leq N)$
143	12 142	sylan	$⊢ (N \in ℕ \land p \in ℙ) \to (p ∥ N! \to p \leq N)$
144	143	adantr	$⊢ ((N \in ℕ \land p \in ℙ) \land (p \leq 2 \cdot N - 1 \land \neg p \leq N)) \to (p ∥ N! \to p \leq N)$
145	140 144	mtod	$⊢ ((N \in ℕ \land p \in ℙ) \land (p \leq 2 \cdot N - 1 \land \neg p \leq N)) \to \neg p ∥ N!$
146	80	adantl	$⊢ (N \in ℕ \land p \in ℙ) \to p \in ℤ$
147	129	simpld	$⊢ (N \in ℕ \land p \in ℙ) \to (N - 1)! \in ℤ$
148		nnz	$⊢ N \in ℕ \to N \in ℤ$
149	148	adantr	$⊢ (N \in ℕ \land p \in ℙ) \to N \in ℤ$
150		dvdsmultr1	$⊢ (p \in ℤ \land (N - 1)! \in ℤ \land N \in ℤ) \to (p ∥ (N - 1)! \to p ∥ (N - 1)! \cdot N)$
151	146 147 149 150	syl3anc	$⊢ (N \in ℕ \land p \in ℙ) \to (p ∥ (N - 1)! \to p ∥ (N - 1)! \cdot N)$
152		facnn2	$⊢ N \in ℕ \to N! = (N - 1)! \cdot N$
153	152	adantr	$⊢ (N \in ℕ \land p \in ℙ) \to N! = (N - 1)! \cdot N$
154	153	breq2d	$⊢ (N \in ℕ \land p \in ℙ) \to (p ∥ N! \leftrightarrow p ∥ (N - 1)! \cdot N)$
155	151 154	sylibrd	$⊢ (N \in ℕ \land p \in ℙ) \to (p ∥ (N - 1)! \to p ∥ N!)$
156	155	adantr	$⊢ ((N \in ℕ \land p \in ℙ) \land (p \leq 2 \cdot N - 1 \land \neg p \leq N)) \to (p ∥ (N - 1)! \to p ∥ N!)$
157	145 156	mtod	$⊢ ((N \in ℕ \land p \in ℙ) \land (p \leq 2 \cdot N - 1 \land \neg p \leq N)) \to \neg p ∥ (N - 1)!$
158		pceq0	$⊢ (p \in ℙ \land (N - 1)! \in ℕ) \to (p pCnt (N - 1)! = 0 \leftrightarrow \neg p ∥ (N - 1)!)$
159	88 119 158	syl2anr	$⊢ (N \in ℕ \land p \in ℙ) \to (p pCnt (N - 1)! = 0 \leftrightarrow \neg p ∥ (N - 1)!)$
160	159	adantr	$⊢ ((N \in ℕ \land p \in ℙ) \land (p \leq 2 \cdot N - 1 \land \neg p \leq N)) \to (p pCnt (N - 1)! = 0 \leftrightarrow \neg p ∥ (N - 1)!)$
161	157 160	mpbird	$⊢ ((N \in ℕ \land p \in ℙ) \land (p \leq 2 \cdot N - 1 \land \neg p \leq N)) \to p pCnt (N - 1)! = 0$
162		pceq0	$⊢ (p \in ℙ \land N! \in ℕ) \to (p pCnt N! = 0 \leftrightarrow \neg p ∥ N!)$
163	88 120 162	syl2anr	$⊢ (N \in ℕ \land p \in ℙ) \to (p pCnt N! = 0 \leftrightarrow \neg p ∥ N!)$
164	163	adantr	$⊢ ((N \in ℕ \land p \in ℙ) \land (p \leq 2 \cdot N - 1 \land \neg p \leq N)) \to (p pCnt N! = 0 \leftrightarrow \neg p ∥ N!)$
165	145 164	mpbird	$⊢ ((N \in ℕ \land p \in ℙ) \land (p \leq 2 \cdot N - 1 \land \neg p \leq N)) \to p pCnt N! = 0$
166	161 165	oveq12d	$⊢ ((N \in ℕ \land p \in ℙ) \land (p \leq 2 \cdot N - 1 \land \neg p \leq N)) \to (p pCnt (N - 1)!) + (p pCnt N!) = 0 + 0$
167		00id	$⊢ 0 + 0 = 0$
168	166 167	eqtrdi	$⊢ ((N \in ℕ \land p \in ℙ) \land (p \leq 2 \cdot N - 1 \land \neg p \leq N)) \to (p pCnt (N - 1)!) + (p pCnt N!) = 0$
169	168	oveq2d	$⊢ ((N \in ℕ \land p \in ℙ) \land (p \leq 2 \cdot N - 1 \land \neg p \leq N)) \to (p pCnt (2 \cdot N - 1)!) - ((p pCnt (N - 1)!) + (p pCnt N!)) = (p pCnt (2 \cdot N - 1)!) - 0$
170		pccl	$⊢ (p \in ℙ \land (2 \cdot N - 1)! \in ℕ) \to p pCnt (2 \cdot N - 1)! \in ℕ_{0}$
171	88 89 170	syl2anr	$⊢ (N \in ℕ \land p \in ℙ) \to p pCnt (2 \cdot N - 1)! \in ℕ_{0}$
172	171	nn0cnd	$⊢ (N \in ℕ \land p \in ℙ) \to p pCnt (2 \cdot N - 1)! \in ℂ$
173	172	subid1d	$⊢ (N \in ℕ \land p \in ℙ) \to (p pCnt (2 \cdot N - 1)!) - 0 = p pCnt (2 \cdot N - 1)!$
174	173	adantr	$⊢ ((N \in ℕ \land p \in ℙ) \land (p \leq 2 \cdot N - 1 \land \neg p \leq N)) \to (p pCnt (2 \cdot N - 1)!) - 0 = p pCnt (2 \cdot N - 1)!$
175	139 169 174	3eqtrd	$⊢ ((N \in ℕ \land p \in ℙ) \land (p \leq 2 \cdot N - 1 \land \neg p \leq N)) \to p pCnt (\binom{2 \cdot N - 1}{N}) = p pCnt (2 \cdot N - 1)!$
176	97 100 175	3eqtrd	$⊢ ((N \in ℕ \land p \in ℙ) \land (p \leq 2 \cdot N - 1 \land \neg p \leq N)) \to if (p \leq N, 1, 0) + (p pCnt (\binom{2 \cdot N - 1}{N})) = p pCnt (2 \cdot N - 1)!$
177	94 176	breqtrrd	$⊢ ((N \in ℕ \land p \in ℙ) \land (p \leq 2 \cdot N - 1 \land \neg p \leq N)) \to 1 \leq if (p \leq N, 1, 0) + (p pCnt (\binom{2 \cdot N - 1}{N}))$
178	177	expr	$⊢ ((N \in ℕ \land p \in ℙ) \land p \leq 2 \cdot N - 1) \to (\neg p \leq N \to 1 \leq if (p \leq N, 1, 0) + (p pCnt (\binom{2 \cdot N - 1}{N})))$
179	76 178	pm2.61d	$⊢ ((N \in ℕ \land p \in ℙ) \land p \leq 2 \cdot N - 1) \to 1 \leq if (p \leq N, 1, 0) + (p pCnt (\binom{2 \cdot N - 1}{N}))$
180	66 179	eqbrtrd	$⊢ ((N \in ℕ \land p \in ℙ) \land p \leq 2 \cdot N - 1) \to if (p \leq 2 \cdot N - 1, 1, 0) \leq if (p \leq N, 1, 0) + (p pCnt (\binom{2 \cdot N - 1}{N}))$
181	180	ex	$⊢ (N \in ℕ \land p \in ℙ) \to (p \leq 2 \cdot N - 1 \to if (p \leq 2 \cdot N - 1, 1, 0) \leq if (p \leq N, 1, 0) + (p pCnt (\binom{2 \cdot N - 1}{N})))$
182		1nn0	$⊢ 1 \in ℕ_{0}$
183		0nn0	$⊢ 0 \in ℕ_{0}$
184	182 183	ifcli	$⊢ if (p \leq N, 1, 0) \in ℕ_{0}$
185		nn0addcl	$⊢ (if (p \leq N, 1, 0) \in ℕ_{0} \land p pCnt (\binom{2 \cdot N - 1}{N}) \in ℕ_{0}) \to if (p \leq N, 1, 0) + (p pCnt (\binom{2 \cdot N - 1}{N})) \in ℕ_{0}$
186	184 69 185	sylancr	$⊢ (N \in ℕ \land p \in ℙ) \to if (p \leq N, 1, 0) + (p pCnt (\binom{2 \cdot N - 1}{N})) \in ℕ_{0}$
187	186	nn0ge0d	$⊢ (N \in ℕ \land p \in ℙ) \to 0 \leq if (p \leq N, 1, 0) + (p pCnt (\binom{2 \cdot N - 1}{N}))$
188		iffalse	$⊢ \neg p \leq 2 \cdot N - 1 \to if (p \leq 2 \cdot N - 1, 1, 0) = 0$
189	188	breq1d	$⊢ \neg p \leq 2 \cdot N - 1 \to (if (p \leq 2 \cdot N - 1, 1, 0) \leq if (p \leq N, 1, 0) + (p pCnt (\binom{2 \cdot N - 1}{N})) \leftrightarrow 0 \leq if (p \leq N, 1, 0) + (p pCnt (\binom{2 \cdot N - 1}{N})))$
190	187 189	syl5ibrcom	$⊢ (N \in ℕ \land p \in ℙ) \to (\neg p \leq 2 \cdot N - 1 \to if (p \leq 2 \cdot N - 1, 1, 0) \leq if (p \leq N, 1, 0) + (p pCnt (\binom{2 \cdot N - 1}{N})))$
191	181 190	pm2.61d	$⊢ (N \in ℕ \land p \in ℙ) \to if (p \leq 2 \cdot N - 1, 1, 0) \leq if (p \leq N, 1, 0) + (p pCnt (\binom{2 \cdot N - 1}{N}))$
192		eqid	$⊢ (n \in ℕ ⟼ if (n \in ℙ, n, 1)) = (n \in ℕ ⟼ if (n \in ℙ, n, 1))$
193	192	prmorcht	$⊢ 2 \cdot N - 1 \in ℕ \to e^{θ (2 \cdot N - 1)} = seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, n, 1))) (2 \cdot N - 1)$
194	37 193	syl	$⊢ N \in ℕ \to e^{θ (2 \cdot N - 1)} = seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, n, 1))) (2 \cdot N - 1)$
195	194	oveq2d	$⊢ N \in ℕ \to p pCnt e^{θ (2 \cdot N - 1)} = p pCnt seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, n, 1))) (2 \cdot N - 1)$
196	195	adantr	$⊢ (N \in ℕ \land p \in ℙ) \to p pCnt e^{θ (2 \cdot N - 1)} = p pCnt seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, n, 1))) (2 \cdot N - 1)$
197		nncn	$⊢ n \in ℕ \to n \in ℂ$
198	197	exp1d	$⊢ n \in ℕ \to n^{1} = n$
199	198	ifeq1d	$⊢ n \in ℕ \to if (n \in ℙ, n^{1}, 1) = if (n \in ℙ, n, 1)$
200	199	mpteq2ia	$⊢ (n \in ℕ ⟼ if (n \in ℙ, n^{1}, 1)) = (n \in ℕ ⟼ if (n \in ℙ, n, 1))$
201	200	eqcomi	$⊢ (n \in ℕ ⟼ if (n \in ℙ, n, 1)) = (n \in ℕ ⟼ if (n \in ℙ, n^{1}, 1))$
202	182	a1i	$⊢ ((N \in ℕ \land p \in ℙ) \land n \in ℙ) \to 1 \in ℕ_{0}$
203	202	ralrimiva	$⊢ (N \in ℕ \land p \in ℙ) \to \forall n \in ℙ 1 \in ℕ_{0}$
204	37	adantr	$⊢ (N \in ℕ \land p \in ℙ) \to 2 \cdot N - 1 \in ℕ$
205		eqidd	$⊢ n = p \to 1 = 1$
206	201 203 204 67 205	pcmpt	$⊢ (N \in ℕ \land p \in ℙ) \to p pCnt seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, n, 1))) (2 \cdot N - 1) = if (p \leq 2 \cdot N - 1, 1, 0)$
207	196 206	eqtrd	$⊢ (N \in ℕ \land p \in ℙ) \to p pCnt e^{θ (2 \cdot N - 1)} = if (p \leq 2 \cdot N - 1, 1, 0)$
208		efchtcl	$⊢ N \in ℝ \to e^{θ (N)} \in ℕ$
209	9 208	syl	$⊢ N \in ℕ \to e^{θ (N)} \in ℕ$
210	209	adantr	$⊢ (N \in ℕ \land p \in ℙ) \to e^{θ (N)} \in ℕ$
211		nnz	$⊢ e^{θ (N)} \in ℕ \to e^{θ (N)} \in ℤ$
212		nnne0	$⊢ e^{θ (N)} \in ℕ \to e^{θ (N)} \neq 0$
213	211 212	jca	$⊢ e^{θ (N)} \in ℕ \to (e^{θ (N)} \in ℤ \land e^{θ (N)} \neq 0)$
214	210 213	syl	$⊢ (N \in ℕ \land p \in ℙ) \to (e^{θ (N)} \in ℤ \land e^{θ (N)} \neq 0)$
215		nnz	$⊢ (\binom{2 \cdot N - 1}{N}) \in ℕ \to (\binom{2 \cdot N - 1}{N}) \in ℤ$
216		nnne0	$⊢ (\binom{2 \cdot N - 1}{N}) \in ℕ \to (\binom{2 \cdot N - 1}{N}) \neq 0$
217	215 216	jca	$⊢ (\binom{2 \cdot N - 1}{N}) \in ℕ \to ((\binom{2 \cdot N - 1}{N}) \in ℤ \land (\binom{2 \cdot N - 1}{N}) \neq 0)$
218	68 217	syl	$⊢ (N \in ℕ \land p \in ℙ) \to ((\binom{2 \cdot N - 1}{N}) \in ℤ \land (\binom{2 \cdot N - 1}{N}) \neq 0)$
219		pcmul	$⊢ (p \in ℙ \land (e^{θ (N)} \in ℤ \land e^{θ (N)} \neq 0) \land ((\binom{2 \cdot N - 1}{N}) \in ℤ \land (\binom{2 \cdot N - 1}{N}) \neq 0)) \to p pCnt e^{θ (N)} (\binom{2 \cdot N - 1}{N}) = (p pCnt e^{θ (N)}) + (p pCnt (\binom{2 \cdot N - 1}{N}))$
220	67 214 218 219	syl3anc	$⊢ (N \in ℕ \land p \in ℙ) \to p pCnt e^{θ (N)} (\binom{2 \cdot N - 1}{N}) = (p pCnt e^{θ (N)}) + (p pCnt (\binom{2 \cdot N - 1}{N}))$
221	192	prmorcht	$⊢ N \in ℕ \to e^{θ (N)} = seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, n, 1))) (N)$
222	221	oveq2d	$⊢ N \in ℕ \to p pCnt e^{θ (N)} = p pCnt seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, n, 1))) (N)$
223	222	adantr	$⊢ (N \in ℕ \land p \in ℙ) \to p pCnt e^{θ (N)} = p pCnt seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, n, 1))) (N)$
224		simpl	$⊢ (N \in ℕ \land p \in ℙ) \to N \in ℕ$
225	201 203 224 67 205	pcmpt	$⊢ (N \in ℕ \land p \in ℙ) \to p pCnt seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, n, 1))) (N) = if (p \leq N, 1, 0)$
226	223 225	eqtrd	$⊢ (N \in ℕ \land p \in ℙ) \to p pCnt e^{θ (N)} = if (p \leq N, 1, 0)$
227	226	oveq1d	$⊢ (N \in ℕ \land p \in ℙ) \to (p pCnt e^{θ (N)}) + (p pCnt (\binom{2 \cdot N - 1}{N})) = if (p \leq N, 1, 0) + (p pCnt (\binom{2 \cdot N - 1}{N}))$
228	220 227	eqtrd	$⊢ (N \in ℕ \land p \in ℙ) \to p pCnt e^{θ (N)} (\binom{2 \cdot N - 1}{N}) = if (p \leq N, 1, 0) + (p pCnt (\binom{2 \cdot N - 1}{N}))$
229	191 207 228	3brtr4d	$⊢ (N \in ℕ \land p \in ℙ) \to p pCnt e^{θ (2 \cdot N - 1)} \leq p pCnt e^{θ (N)} (\binom{2 \cdot N - 1}{N})$
230	229	ralrimiva	$⊢ N \in ℕ \to \forall p \in ℙ p pCnt e^{θ (2 \cdot N - 1)} \leq p pCnt e^{θ (N)} (\binom{2 \cdot N - 1}{N})$
231		efchtcl	$⊢ 2 \cdot N - 1 \in ℝ \to e^{θ (2 \cdot N - 1)} \in ℕ$
232	6 231	syl	$⊢ N \in ℕ \to e^{θ (2 \cdot N - 1)} \in ℕ$
233	232	nnzd	$⊢ N \in ℕ \to e^{θ (2 \cdot N - 1)} \in ℤ$
234	209 52	nnmulcld	$⊢ N \in ℕ \to e^{θ (N)} (\binom{2 \cdot N - 1}{N}) \in ℕ$
235	234	nnzd	$⊢ N \in ℕ \to e^{θ (N)} (\binom{2 \cdot N - 1}{N}) \in ℤ$
236		pc2dvds	$⊢ (e^{θ (2 \cdot N - 1)} \in ℤ \land e^{θ (N)} (\binom{2 \cdot N - 1}{N}) \in ℤ) \to (e^{θ (2 \cdot N - 1)} ∥ e^{θ (N)} (\binom{2 \cdot N - 1}{N}) \leftrightarrow \forall p \in ℙ p pCnt e^{θ (2 \cdot N - 1)} \leq p pCnt e^{θ (N)} (\binom{2 \cdot N - 1}{N}))$
237	233 235 236	syl2anc	$⊢ N \in ℕ \to (e^{θ (2 \cdot N - 1)} ∥ e^{θ (N)} (\binom{2 \cdot N - 1}{N}) \leftrightarrow \forall p \in ℙ p pCnt e^{θ (2 \cdot N - 1)} \leq p pCnt e^{θ (N)} (\binom{2 \cdot N - 1}{N}))$
238	230 237	mpbird	$⊢ N \in ℕ \to e^{θ (2 \cdot N - 1)} ∥ e^{θ (N)} (\binom{2 \cdot N - 1}{N})$
239		dvdsle	$⊢ (e^{θ (2 \cdot N - 1)} \in ℤ \land e^{θ (N)} (\binom{2 \cdot N - 1}{N}) \in ℕ) \to (e^{θ (2 \cdot N - 1)} ∥ e^{θ (N)} (\binom{2 \cdot N - 1}{N}) \to e^{θ (2 \cdot N - 1)} \leq e^{θ (N)} (\binom{2 \cdot N - 1}{N}))$
240	233 234 239	syl2anc	$⊢ N \in ℕ \to (e^{θ (2 \cdot N - 1)} ∥ e^{θ (N)} (\binom{2 \cdot N - 1}{N}) \to e^{θ (2 \cdot N - 1)} \leq e^{θ (N)} (\binom{2 \cdot N - 1}{N}))$
241	238 240	mpd	$⊢ N \in ℕ \to e^{θ (2 \cdot N - 1)} \leq e^{θ (N)} (\binom{2 \cdot N - 1}{N})$
242	11	recnd	$⊢ N \in ℕ \to θ (N) \in ℂ$
243	54	recnd	$⊢ N \in ℕ \to \log (\binom{2 \cdot N - 1}{N}) \in ℂ$
244		efadd	$⊢ (θ (N) \in ℂ \land \log (\binom{2 \cdot N - 1}{N}) \in ℂ) \to e^{θ (N) + \log (\binom{2 \cdot N - 1}{N})} = e^{θ (N)} e^{\log (\binom{2 \cdot N - 1}{N})}$
245	242 243 244	syl2anc	$⊢ N \in ℕ \to e^{θ (N) + \log (\binom{2 \cdot N - 1}{N})} = e^{θ (N)} e^{\log (\binom{2 \cdot N - 1}{N})}$
246	53	reeflogd	$⊢ N \in ℕ \to e^{\log (\binom{2 \cdot N - 1}{N})} = (\binom{2 \cdot N - 1}{N})$
247	246	oveq2d	$⊢ N \in ℕ \to e^{θ (N)} e^{\log (\binom{2 \cdot N - 1}{N})} = e^{θ (N)} (\binom{2 \cdot N - 1}{N})$
248	245 247	eqtrd	$⊢ N \in ℕ \to e^{θ (N) + \log (\binom{2 \cdot N - 1}{N})} = e^{θ (N)} (\binom{2 \cdot N - 1}{N})$
249	241 248	breqtrrd	$⊢ N \in ℕ \to e^{θ (2 \cdot N - 1)} \leq e^{θ (N) + \log (\binom{2 \cdot N - 1}{N})}$
250		efle	$⊢ (θ (2 \cdot N - 1) \in ℝ \land θ (N) + \log (\binom{2 \cdot N - 1}{N}) \in ℝ) \to (θ (2 \cdot N - 1) \leq θ (N) + \log (\binom{2 \cdot N - 1}{N}) \leftrightarrow e^{θ (2 \cdot N - 1)} \leq e^{θ (N) + \log (\binom{2 \cdot N - 1}{N})})$
251	8 55 250	syl2anc	$⊢ N \in ℕ \to (θ (2 \cdot N - 1) \leq θ (N) + \log (\binom{2 \cdot N - 1}{N}) \leftrightarrow e^{θ (2 \cdot N - 1)} \leq e^{θ (N) + \log (\binom{2 \cdot N - 1}{N})})$
252	249 251	mpbird	$⊢ N \in ℕ \to θ (2 \cdot N - 1) \leq θ (N) + \log (\binom{2 \cdot N - 1}{N})$
253		fzfid	$⊢ N \in ℕ \to (0 \dots 2 \cdot N - 1) \in Fin$
254		elfzelz	$⊢ k \in (0 \dots 2 \cdot N - 1) \to k \in ℤ$
255		bccl	$⊢ (2 \cdot N - 1 \in ℕ_{0} \land k \in ℤ) \to (\binom{2 \cdot N - 1}{k}) \in ℕ_{0}$
256	39 254 255	syl2an	$⊢ (N \in ℕ \land k \in (0 \dots 2 \cdot N - 1)) \to (\binom{2 \cdot N - 1}{k}) \in ℕ_{0}$
257	256	nn0red	$⊢ (N \in ℕ \land k \in (0 \dots 2 \cdot N - 1)) \to (\binom{2 \cdot N - 1}{k}) \in ℝ$
258	256	nn0ge0d	$⊢ (N \in ℕ \land k \in (0 \dots 2 \cdot N - 1)) \to 0 \leq (\binom{2 \cdot N - 1}{k})$
259		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
260	32 259	eleqtrdi	$⊢ N \in ℕ \to N - 1 \in ℤ_{\geq 0}$
261		fzss1	$⊢ N - 1 \in ℤ_{\geq 0} \to (N - 1 \dots N) \subseteq (0 \dots N)$
262	260 261	syl	$⊢ N \in ℕ \to (N - 1 \dots N) \subseteq (0 \dots N)$
263		eluz	$⊢ (N \in ℤ \land 2 \cdot N - 1 \in ℤ) \to (2 \cdot N - 1 \in ℤ_{\geq N} \leftrightarrow N \leq 2 \cdot N - 1)$
264	148 81 263	syl2anc	$⊢ N \in ℕ \to (2 \cdot N - 1 \in ℤ_{\geq N} \leftrightarrow N \leq 2 \cdot N - 1)$
265	48 264	mpbird	$⊢ N \in ℕ \to 2 \cdot N - 1 \in ℤ_{\geq N}$
266		fzss2	$⊢ 2 \cdot N - 1 \in ℤ_{\geq N} \to (0 \dots N) \subseteq (0 \dots 2 \cdot N - 1)$
267	265 266	syl	$⊢ N \in ℕ \to (0 \dots N) \subseteq (0 \dots 2 \cdot N - 1)$
268	262 267	sstrd	$⊢ N \in ℕ \to (N - 1 \dots N) \subseteq (0 \dots 2 \cdot N - 1)$
269	253 257 258 268	fsumless	$⊢ N \in ℕ \to \sum_{k = N - 1}^{N} (\binom{2 \cdot N - 1}{k}) \leq \sum_{k = 0}^{2 \cdot N - 1} (\binom{2 \cdot N - 1}{k})$
270	32	nn0zd	$⊢ N \in ℕ \to N - 1 \in ℤ$
271		bccmpl	$⊢ (2 \cdot N - 1 \in ℕ_{0} \land N \in ℤ) \to (\binom{2 \cdot N - 1}{N}) = (\binom{2 \cdot N - 1}{2 \cdot N - 1 - N})$
272	39 148 271	syl2anc	$⊢ N \in ℕ \to (\binom{2 \cdot N - 1}{N}) = (\binom{2 \cdot N - 1}{2 \cdot N - 1 - N})$
273	107	oveq2d	$⊢ N \in ℕ \to (\binom{2 \cdot N - 1}{2 \cdot N - 1 - N}) = (\binom{2 \cdot N - 1}{N - 1})$
274	272 273	eqtrd	$⊢ N \in ℕ \to (\binom{2 \cdot N - 1}{N}) = (\binom{2 \cdot N - 1}{N - 1})$
275	52	nncnd	$⊢ N \in ℕ \to (\binom{2 \cdot N - 1}{N}) \in ℂ$
276	274 275	eqeltrrd	$⊢ N \in ℕ \to (\binom{2 \cdot N - 1}{N - 1}) \in ℂ$
277		oveq2	$⊢ k = N - 1 \to (\binom{2 \cdot N - 1}{k}) = (\binom{2 \cdot N - 1}{N - 1})$
278	277	fsum1	$⊢ (N - 1 \in ℤ \land (\binom{2 \cdot N - 1}{N - 1}) \in ℂ) \to \sum_{k = N - 1}^{N - 1} (\binom{2 \cdot N - 1}{k}) = (\binom{2 \cdot N - 1}{N - 1})$
279	270 276 278	syl2anc	$⊢ N \in ℕ \to \sum_{k = N - 1}^{N - 1} (\binom{2 \cdot N - 1}{k}) = (\binom{2 \cdot N - 1}{N - 1})$
280	279 274	eqtr4d	$⊢ N \in ℕ \to \sum_{k = N - 1}^{N - 1} (\binom{2 \cdot N - 1}{k}) = (\binom{2 \cdot N - 1}{N})$
281	280	oveq1d	$⊢ N \in ℕ \to \sum_{k = N - 1}^{N - 1} (\binom{2 \cdot N - 1}{k}) + (\binom{2 \cdot N - 1}{N}) = (\binom{2 \cdot N - 1}{N}) + (\binom{2 \cdot N - 1}{N})$
282	21 104	npcand	$⊢ N \in ℕ \to N - 1 + 1 = N$
283		uzid	$⊢ N - 1 \in ℤ \to N - 1 \in ℤ_{\geq (N - 1)}$
284	270 283	syl	$⊢ N \in ℕ \to N - 1 \in ℤ_{\geq (N - 1)}$
285		peano2uz	$⊢ N - 1 \in ℤ_{\geq (N - 1)} \to N - 1 + 1 \in ℤ_{\geq (N - 1)}$
286	284 285	syl	$⊢ N \in ℕ \to N - 1 + 1 \in ℤ_{\geq (N - 1)}$
287	282 286	eqeltrrd	$⊢ N \in ℕ \to N \in ℤ_{\geq (N - 1)}$
288	268	sselda	$⊢ (N \in ℕ \land k \in (N - 1 \dots N)) \to k \in (0 \dots 2 \cdot N - 1)$
289	256	nn0cnd	$⊢ (N \in ℕ \land k \in (0 \dots 2 \cdot N - 1)) \to (\binom{2 \cdot N - 1}{k}) \in ℂ$
290	288 289	syldan	$⊢ (N \in ℕ \land k \in (N - 1 \dots N)) \to (\binom{2 \cdot N - 1}{k}) \in ℂ$
291		oveq2	$⊢ k = N \to (\binom{2 \cdot N - 1}{k}) = (\binom{2 \cdot N - 1}{N})$
292	287 290 291	fsumm1	$⊢ N \in ℕ \to \sum_{k = N - 1}^{N} (\binom{2 \cdot N - 1}{k}) = \sum_{k = N - 1}^{N - 1} (\binom{2 \cdot N - 1}{k}) + (\binom{2 \cdot N - 1}{N})$
293	275	2timesd	$⊢ N \in ℕ \to 2 (\binom{2 \cdot N - 1}{N}) = (\binom{2 \cdot N - 1}{N}) + (\binom{2 \cdot N - 1}{N})$
294	281 292 293	3eqtr4rd	$⊢ N \in ℕ \to 2 (\binom{2 \cdot N - 1}{N}) = \sum_{k = N - 1}^{N} (\binom{2 \cdot N - 1}{k})$
295		binom11	$⊢ 2 \cdot N - 1 \in ℕ_{0} \to 2^{2 \cdot N - 1} = \sum_{k = 0}^{2 \cdot N - 1} (\binom{2 \cdot N - 1}{k})$
296	39 295	syl	$⊢ N \in ℕ \to 2^{2 \cdot N - 1} = \sum_{k = 0}^{2 \cdot N - 1} (\binom{2 \cdot N - 1}{k})$
297	269 294 296	3brtr4d	$⊢ N \in ℕ \to 2 (\binom{2 \cdot N - 1}{N}) \leq 2^{2 \cdot N - 1}$
298		mulcom	$⊢ (2 \in ℂ \land (\binom{2 \cdot N - 1}{N}) \in ℂ) \to 2 (\binom{2 \cdot N - 1}{N}) = (\binom{2 \cdot N - 1}{N}) \cdot 2$
299	16 275 298	sylancr	$⊢ N \in ℕ \to 2 (\binom{2 \cdot N - 1}{N}) = (\binom{2 \cdot N - 1}{N}) \cdot 2$
300	30	oveq2d	$⊢ N \in ℕ \to 2^{2 \cdot N - 1} = 2^{2 (N - 1) + 1}$
301		expp1	$⊢ (2 \in ℂ \land 2 (N - 1) \in ℕ_{0}) \to 2^{2 (N - 1) + 1} = 2^{2 (N - 1)} \cdot 2$
302	16 34 301	sylancr	$⊢ N \in ℕ \to 2^{2 (N - 1) + 1} = 2^{2 (N - 1)} \cdot 2$
303	16	a1i	$⊢ N \in ℕ \to 2 \in ℂ$
304	31	a1i	$⊢ N \in ℕ \to 2 \in ℕ_{0}$
305	303 32 304	expmuld	$⊢ N \in ℕ \to 2^{2 (N - 1)} = {(2^{2})}^{N - 1}$
306		sq2	$⊢ 2^{2} = 4$
307	306	oveq1i	$⊢ {(2^{2})}^{N - 1} = 4^{N - 1}$
308	305 307	eqtrdi	$⊢ N \in ℕ \to 2^{2 (N - 1)} = 4^{N - 1}$
309	308	oveq1d	$⊢ N \in ℕ \to 2^{2 (N - 1)} \cdot 2 = 4^{N - 1} \cdot 2$
310	300 302 309	3eqtrd	$⊢ N \in ℕ \to 2^{2 \cdot N - 1} = 4^{N - 1} \cdot 2$
311	297 299 310	3brtr3d	$⊢ N \in ℕ \to (\binom{2 \cdot N - 1}{N}) \cdot 2 \leq 4^{N - 1} \cdot 2$
312	52	nnred	$⊢ N \in ℕ \to (\binom{2 \cdot N - 1}{N}) \in ℝ$
313		reexpcl	$⊢ (4 \in ℝ \land N - 1 \in ℕ_{0}) \to 4^{N - 1} \in ℝ$
314	56 32 313	sylancr	$⊢ N \in ℕ \to 4^{N - 1} \in ℝ$
315		2re	$⊢ 2 \in ℝ$
316		2pos	$⊢ 0 < 2$
317	315 316	pm3.2i	$⊢ (2 \in ℝ \land 0 < 2)$
318	317	a1i	$⊢ N \in ℕ \to (2 \in ℝ \land 0 < 2)$
319		lemul1	$⊢ ((\binom{2 \cdot N - 1}{N}) \in ℝ \land 4^{N - 1} \in ℝ \land (2 \in ℝ \land 0 < 2)) \to ((\binom{2 \cdot N - 1}{N}) \leq 4^{N - 1} \leftrightarrow (\binom{2 \cdot N - 1}{N}) \cdot 2 \leq 4^{N - 1} \cdot 2)$
320	312 314 318 319	syl3anc	$⊢ N \in ℕ \to ((\binom{2 \cdot N - 1}{N}) \leq 4^{N - 1} \leftrightarrow (\binom{2 \cdot N - 1}{N}) \cdot 2 \leq 4^{N - 1} \cdot 2)$
321	311 320	mpbird	$⊢ N \in ℕ \to (\binom{2 \cdot N - 1}{N}) \leq 4^{N - 1}$
322	60	recni	$⊢ \log 4 \in ℂ$
323		mulcom	$⊢ (\log 4 \in ℂ \land N - 1 \in ℂ) \to \log 4 (N - 1) = (N - 1) \log 4$
324	322 103 323	sylancr	$⊢ N \in ℕ \to \log 4 (N - 1) = (N - 1) \log 4$
325	324	fveq2d	$⊢ N \in ℕ \to e^{\log 4 (N - 1)} = e^{(N - 1) \log 4}$
326		reexplog	$⊢ (4 \in ℝ^{+} \land N - 1 \in ℤ) \to 4^{N - 1} = e^{(N - 1) \log 4}$
327	58 270 326	sylancr	$⊢ N \in ℕ \to 4^{N - 1} = e^{(N - 1) \log 4}$
328	325 327	eqtr4d	$⊢ N \in ℕ \to e^{\log 4 (N - 1)} = 4^{N - 1}$
329	321 246 328	3brtr4d	$⊢ N \in ℕ \to e^{\log (\binom{2 \cdot N - 1}{N})} \leq e^{\log 4 (N - 1)}$
330		efle	$⊢ (\log (\binom{2 \cdot N - 1}{N}) \in ℝ \land \log 4 (N - 1) \in ℝ) \to (\log (\binom{2 \cdot N - 1}{N}) \leq \log 4 (N - 1) \leftrightarrow e^{\log (\binom{2 \cdot N - 1}{N})} \leq e^{\log 4 (N - 1)})$
331	54 63 330	syl2anc	$⊢ N \in ℕ \to (\log (\binom{2 \cdot N - 1}{N}) \leq \log 4 (N - 1) \leftrightarrow e^{\log (\binom{2 \cdot N - 1}{N})} \leq e^{\log 4 (N - 1)})$
332	329 331	mpbird	$⊢ N \in ℕ \to \log (\binom{2 \cdot N - 1}{N}) \leq \log 4 (N - 1)$
333	54 63 11 332	leadd2dd	$⊢ N \in ℕ \to θ (N) + \log (\binom{2 \cdot N - 1}{N}) \leq θ (N) + \log 4 (N - 1)$
334	8 55 64 252 333	letrd	$⊢ N \in ℕ \to θ (2 \cdot N - 1) \leq θ (N) + \log 4 (N - 1)$

Metamath Proof Explorer

Theorem chtublem

Proof