bclbnd - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > bclbnd		GIF version

Theorem bclbnd 16127

Description: A bound on the binomial coefficient. (Contributed by Mario Carneiro, 11-Mar-2014.)

**Assertion**
Ref	Expression
bclbnd	⊢ (𝑁 ∈ (ℤ_≥‘4) → ((4↑𝑁) / 𝑁) < ((2 · 𝑁)C𝑁))

Proof of Theorem bclbnd Dummy variables 𝑥 𝑛 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		oveq2 6093	. . . 4 ⊢ (𝑥 = 4 → (4↑𝑥) = (4↑4))
2		id 19	. . . 4 ⊢ (𝑥 = 4 → 𝑥 = 4)
3	1, 2	oveq12d 6103	. . 3 ⊢ (𝑥 = 4 → ((4↑𝑥) / 𝑥) = ((4↑4) / 4))
4		oveq2 6093	. . . 4 ⊢ (𝑥 = 4 → (2 · 𝑥) = (2 · 4))
5	4, 2	oveq12d 6103	. . 3 ⊢ (𝑥 = 4 → ((2 · 𝑥)C𝑥) = ((2 · 4)C4))
6	3, 5	breq12d 4143	. 2 ⊢ (𝑥 = 4 → (((4↑𝑥) / 𝑥) < ((2 · 𝑥)C𝑥) ↔ ((4↑4) / 4) < ((2 · 4)C4)))
7		oveq2 6093	. . . 4 ⊢ (𝑥 = 𝑛 → (4↑𝑥) = (4↑𝑛))
8		id 19	. . . 4 ⊢ (𝑥 = 𝑛 → 𝑥 = 𝑛)
9	7, 8	oveq12d 6103	. . 3 ⊢ (𝑥 = 𝑛 → ((4↑𝑥) / 𝑥) = ((4↑𝑛) / 𝑛))
10		oveq2 6093	. . . 4 ⊢ (𝑥 = 𝑛 → (2 · 𝑥) = (2 · 𝑛))
11	10, 8	oveq12d 6103	. . 3 ⊢ (𝑥 = 𝑛 → ((2 · 𝑥)C𝑥) = ((2 · 𝑛)C𝑛))
12	9, 11	breq12d 4143	. 2 ⊢ (𝑥 = 𝑛 → (((4↑𝑥) / 𝑥) < ((2 · 𝑥)C𝑥) ↔ ((4↑𝑛) / 𝑛) < ((2 · 𝑛)C𝑛)))
13		oveq2 6093	. . . 4 ⊢ (𝑥 = (𝑛 + 1) → (4↑𝑥) = (4↑(𝑛 + 1)))
14		id 19	. . . 4 ⊢ (𝑥 = (𝑛 + 1) → 𝑥 = (𝑛 + 1))
15	13, 14	oveq12d 6103	. . 3 ⊢ (𝑥 = (𝑛 + 1) → ((4↑𝑥) / 𝑥) = ((4↑(𝑛 + 1)) / (𝑛 + 1)))
16		oveq2 6093	. . . 4 ⊢ (𝑥 = (𝑛 + 1) → (2 · 𝑥) = (2 · (𝑛 + 1)))
17	16, 14	oveq12d 6103	. . 3 ⊢ (𝑥 = (𝑛 + 1) → ((2 · 𝑥)C𝑥) = ((2 · (𝑛 + 1))C(𝑛 + 1)))
18	15, 17	breq12d 4143	. 2 ⊢ (𝑥 = (𝑛 + 1) → (((4↑𝑥) / 𝑥) < ((2 · 𝑥)C𝑥) ↔ ((4↑(𝑛 + 1)) / (𝑛 + 1)) < ((2 · (𝑛 + 1))C(𝑛 + 1))))
19		oveq2 6093	. . . 4 ⊢ (𝑥 = 𝑁 → (4↑𝑥) = (4↑𝑁))
20		id 19	. . . 4 ⊢ (𝑥 = 𝑁 → 𝑥 = 𝑁)
21	19, 20	oveq12d 6103	. . 3 ⊢ (𝑥 = 𝑁 → ((4↑𝑥) / 𝑥) = ((4↑𝑁) / 𝑁))
22		oveq2 6093	. . . 4 ⊢ (𝑥 = 𝑁 → (2 · 𝑥) = (2 · 𝑁))
23	22, 20	oveq12d 6103	. . 3 ⊢ (𝑥 = 𝑁 → ((2 · 𝑥)C𝑥) = ((2 · 𝑁)C𝑁))
24	21, 23	breq12d 4143	. 2 ⊢ (𝑥 = 𝑁 → (((4↑𝑥) / 𝑥) < ((2 · 𝑥)C𝑥) ↔ ((4↑𝑁) / 𝑁) < ((2 · 𝑁)C𝑁)))
25		6nn0 9586	. . . 4 ⊢ 6 ∈ ℕ₀
26		7nn0 9587	. . . 4 ⊢ 7 ∈ ℕ₀
27		4nn0 9584	. . . 4 ⊢ 4 ∈ ℕ₀
28		0nn0 9580	. . . 4 ⊢ 0 ∈ ℕ₀
29		4lt10 9914	. . . 4 ⊢ 4 < ;10
30		6lt7 9491	. . . 4 ⊢ 6 < 7
31	25, 26, 27, 28, 29, 30	decltc 9807	. . 3 ⊢ ;64 < ;70
32		2cn 9376	. . . . . 6 ⊢ 2 ∈ ℂ
33		2nn0 9582	. . . . . 6 ⊢ 2 ∈ ℕ₀
34		3nn0 9583	. . . . . 6 ⊢ 3 ∈ ℕ₀
35		expmul 11023	. . . . . 6 ⊢ ((2 ∈ ℂ ∧ 2 ∈ ℕ₀ ∧ 3 ∈ ℕ₀) → (2↑(2 · 3)) = ((2↑2)↑3))
36	32, 33, 34, 35	mp3an 1378	. . . . 5 ⊢ (2↑(2 · 3)) = ((2↑2)↑3)
37		sq2 11074	. . . . . . 7 ⊢ (2↑2) = 4
38	37	eqcomi 2242	. . . . . 6 ⊢ 4 = (2↑2)
39		4m1e3 9426	. . . . . 6 ⊢ (4 − 1) = 3
40	38, 39	oveq12i 6097	. . . . 5 ⊢ (4↑(4 − 1)) = ((2↑2)↑3)
41	36, 40	eqtr4i 2262	. . . 4 ⊢ (2↑(2 · 3)) = (4↑(4 − 1))
42		2t3e6 9463	. . . . . 6 ⊢ (2 · 3) = 6
43	42	oveq2i 6096	. . . . 5 ⊢ (2↑(2 · 3)) = (2↑6)
44		2exp6 13214	. . . . 5 ⊢ (2↑6) = ;64
45	43, 44	eqtri 2259	. . . 4 ⊢ (2↑(2 · 3)) = ;64
46		4cn 9383	. . . . 5 ⊢ 4 ∈ ℂ
47		4ap0 9404	. . . . 5 ⊢ 4 # 0
48		4z 9676	. . . . 5 ⊢ 4 ∈ ℤ
49		expm1ap 11028	. . . . 5 ⊢ ((4 ∈ ℂ ∧ 4 # 0 ∧ 4 ∈ ℤ) → (4↑(4 − 1)) = ((4↑4) / 4))
50	46, 47, 48, 49	mp3an 1378	. . . 4 ⊢ (4↑(4 − 1)) = ((4↑4) / 4)
51	41, 45, 50	3eqtr3ri 2268	. . 3 ⊢ ((4↑4) / 4) = ;64
52		df-4 9366	. . . . . . 7 ⊢ 4 = (3 + 1)
53	52	oveq2i 6096	. . . . . 6 ⊢ (2 · 4) = (2 · (3 + 1))
54	53, 52	oveq12i 6097	. . . . 5 ⊢ ((2 · 4)C4) = ((2 · (3 + 1))C(3 + 1))
55		bcp1ctr 16126	. . . . . 6 ⊢ (3 ∈ ℕ₀ → ((2 · (3 + 1))C(3 + 1)) = (((2 · 3)C3) · (2 · (((2 · 3) + 1) / (3 + 1)))))
56	34, 55	ax-mp 5	. . . . 5 ⊢ ((2 · (3 + 1))C(3 + 1)) = (((2 · 3)C3) · (2 · (((2 · 3) + 1) / (3 + 1))))
57		df-3 9365	. . . . . . . . 9 ⊢ 3 = (2 + 1)
58	57	oveq2i 6096	. . . . . . . 8 ⊢ (2 · 3) = (2 · (2 + 1))
59	58, 57	oveq12i 6097	. . . . . . 7 ⊢ ((2 · 3)C3) = ((2 · (2 + 1))C(2 + 1))
60		bcp1ctr 16126	. . . . . . . . 9 ⊢ (2 ∈ ℕ₀ → ((2 · (2 + 1))C(2 + 1)) = (((2 · 2)C2) · (2 · (((2 · 2) + 1) / (2 + 1)))))
61	33, 60	ax-mp 5	. . . . . . . 8 ⊢ ((2 · (2 + 1))C(2 + 1)) = (((2 · 2)C2) · (2 · (((2 · 2) + 1) / (2 + 1))))
62		df-2 9364	. . . . . . . . . . . 12 ⊢ 2 = (1 + 1)
63	62	oveq2i 6096	. . . . . . . . . . 11 ⊢ (2 · 2) = (2 · (1 + 1))
64	63, 62	oveq12i 6097	. . . . . . . . . 10 ⊢ ((2 · 2)C2) = ((2 · (1 + 1))C(1 + 1))
65		1nn0 9581	. . . . . . . . . . 11 ⊢ 1 ∈ ℕ₀
66		bcp1ctr 16126	. . . . . . . . . . 11 ⊢ (1 ∈ ℕ₀ → ((2 · (1 + 1))C(1 + 1)) = (((2 · 1)C1) · (2 · (((2 · 1) + 1) / (1 + 1)))))
67	65, 66	ax-mp 5	. . . . . . . . . 10 ⊢ ((2 · (1 + 1))C(1 + 1)) = (((2 · 1)C1) · (2 · (((2 · 1) + 1) / (1 + 1))))
68		1e0p1 9820	. . . . . . . . . . . . . . 15 ⊢ 1 = (0 + 1)
69	68	oveq2i 6096	. . . . . . . . . . . . . 14 ⊢ (2 · 1) = (2 · (0 + 1))
70	69, 68	oveq12i 6097	. . . . . . . . . . . . 13 ⊢ ((2 · 1)C1) = ((2 · (0 + 1))C(0 + 1))
71		bcp1ctr 16126	. . . . . . . . . . . . . 14 ⊢ (0 ∈ ℕ₀ → ((2 · (0 + 1))C(0 + 1)) = (((2 · 0)C0) · (2 · (((2 · 0) + 1) / (0 + 1)))))
72	28, 71	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ((2 · (0 + 1))C(0 + 1)) = (((2 · 0)C0) · (2 · (((2 · 0) + 1) / (0 + 1))))
73	33, 28	nn0mulcli 9603	. . . . . . . . . . . . . . . 16 ⊢ (2 · 0) ∈ ℕ₀
74		bcn0 11195	. . . . . . . . . . . . . . . 16 ⊢ ((2 · 0) ∈ ℕ₀ → ((2 · 0)C0) = 1)
75	73, 74	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ((2 · 0)C0) = 1
76		2t0e0 9466	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (2 · 0) = 0
77	76	oveq1i 6095	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2 · 0) + 1) = (0 + 1)
78	77, 68	eqtr4i 2262	. . . . . . . . . . . . . . . . . . 19 ⊢ ((2 · 0) + 1) = 1
79	68	eqcomi 2242	. . . . . . . . . . . . . . . . . . 19 ⊢ (0 + 1) = 1
80	78, 79	oveq12i 6097	. . . . . . . . . . . . . . . . . 18 ⊢ (((2 · 0) + 1) / (0 + 1)) = (1 / 1)
81		1div1e1 9035	. . . . . . . . . . . . . . . . . 18 ⊢ (1 / 1) = 1
82	80, 81	eqtri 2259	. . . . . . . . . . . . . . . . 17 ⊢ (((2 · 0) + 1) / (0 + 1)) = 1
83	82	oveq2i 6096	. . . . . . . . . . . . . . . 16 ⊢ (2 · (((2 · 0) + 1) / (0 + 1))) = (2 · 1)
84		2t1e2 9459	. . . . . . . . . . . . . . . 16 ⊢ (2 · 1) = 2
85	83, 84	eqtri 2259	. . . . . . . . . . . . . . 15 ⊢ (2 · (((2 · 0) + 1) / (0 + 1))) = 2
86	75, 85	oveq12i 6097	. . . . . . . . . . . . . 14 ⊢ (((2 · 0)C0) · (2 · (((2 · 0) + 1) / (0 + 1)))) = (1 · 2)
87	32	mullidi 8329	. . . . . . . . . . . . . 14 ⊢ (1 · 2) = 2
88	86, 87	eqtri 2259	. . . . . . . . . . . . 13 ⊢ (((2 · 0)C0) · (2 · (((2 · 0) + 1) / (0 + 1)))) = 2
89	70, 72, 88	3eqtri 2263	. . . . . . . . . . . 12 ⊢ ((2 · 1)C1) = 2
90	84	oveq1i 6095	. . . . . . . . . . . . . . . 16 ⊢ ((2 · 1) + 1) = (2 + 1)
91	90, 57	eqtr4i 2262	. . . . . . . . . . . . . . 15 ⊢ ((2 · 1) + 1) = 3
92	62	eqcomi 2242	. . . . . . . . . . . . . . 15 ⊢ (1 + 1) = 2
93	91, 92	oveq12i 6097	. . . . . . . . . . . . . 14 ⊢ (((2 · 1) + 1) / (1 + 1)) = (3 / 2)
94	93	oveq2i 6096	. . . . . . . . . . . . 13 ⊢ (2 · (((2 · 1) + 1) / (1 + 1))) = (2 · (3 / 2))
95		3cn 9380	. . . . . . . . . . . . . 14 ⊢ 3 ∈ ℂ
96		2ap0 9398	. . . . . . . . . . . . . 14 ⊢ 2 # 0
97	95, 32, 96	divcanap2i 9086	. . . . . . . . . . . . 13 ⊢ (2 · (3 / 2)) = 3
98	94, 97	eqtri 2259	. . . . . . . . . . . 12 ⊢ (2 · (((2 · 1) + 1) / (1 + 1))) = 3
99	89, 98	oveq12i 6097	. . . . . . . . . . 11 ⊢ (((2 · 1)C1) · (2 · (((2 · 1) + 1) / (1 + 1)))) = (2 · 3)
100	99, 42	eqtri 2259	. . . . . . . . . 10 ⊢ (((2 · 1)C1) · (2 · (((2 · 1) + 1) / (1 + 1)))) = 6
101	64, 67, 100	3eqtri 2263	. . . . . . . . 9 ⊢ ((2 · 2)C2) = 6
102		2t2e4 9460	. . . . . . . . . . . . . 14 ⊢ (2 · 2) = 4
103	102	oveq1i 6095	. . . . . . . . . . . . 13 ⊢ ((2 · 2) + 1) = (4 + 1)
104		df-5 9367	. . . . . . . . . . . . 13 ⊢ 5 = (4 + 1)
105	103, 104	eqtr4i 2262	. . . . . . . . . . . 12 ⊢ ((2 · 2) + 1) = 5
106	57	eqcomi 2242	. . . . . . . . . . . 12 ⊢ (2 + 1) = 3
107	105, 106	oveq12i 6097	. . . . . . . . . . 11 ⊢ (((2 · 2) + 1) / (2 + 1)) = (5 / 3)
108	107	oveq2i 6096	. . . . . . . . . 10 ⊢ (2 · (((2 · 2) + 1) / (2 + 1))) = (2 · (5 / 3))
109		5cn 9385	. . . . . . . . . . 11 ⊢ 5 ∈ ℂ
110		3ap0 9401	. . . . . . . . . . 11 ⊢ 3 # 0
111	32, 109, 95, 110	divassapi 9099	. . . . . . . . . 10 ⊢ ((2 · 5) / 3) = (2 · (5 / 3))
112	108, 111	eqtr4i 2262	. . . . . . . . 9 ⊢ (2 · (((2 · 2) + 1) / (2 + 1))) = ((2 · 5) / 3)
113	101, 112	oveq12i 6097	. . . . . . . 8 ⊢ (((2 · 2)C2) · (2 · (((2 · 2) + 1) / (2 + 1)))) = (6 · ((2 · 5) / 3))
114	61, 113	eqtri 2259	. . . . . . 7 ⊢ ((2 · (2 + 1))C(2 + 1)) = (6 · ((2 · 5) / 3))
115		6cn 9387	. . . . . . . . 9 ⊢ 6 ∈ ℂ
116		2nn 9468	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ
117		5nn 9471	. . . . . . . . . . 11 ⊢ 5 ∈ ℕ
118	116, 117	nnmulcli 9327	. . . . . . . . . 10 ⊢ (2 · 5) ∈ ℕ
119	118	nncni 9315	. . . . . . . . 9 ⊢ (2 · 5) ∈ ℂ
120	95, 110	pm3.2i 272	. . . . . . . . 9 ⊢ (3 ∈ ℂ ∧ 3 # 0)
121		div12ap 9025	. . . . . . . . 9 ⊢ ((6 ∈ ℂ ∧ (2 · 5) ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 # 0)) → (6 · ((2 · 5) / 3)) = ((2 · 5) · (6 / 3)))
122	115, 119, 120, 121	mp3an 1378	. . . . . . . 8 ⊢ (6 · ((2 · 5) / 3)) = ((2 · 5) · (6 / 3))
123		5t2e10 9878	. . . . . . . . . 10 ⊢ (5 · 2) = ;10
124	109, 32, 123	mulcomli 8333	. . . . . . . . 9 ⊢ (2 · 5) = ;10
125		3t2e6 9462	. . . . . . . . . 10 ⊢ (3 · 2) = 6
126	115, 95, 32, 110	divmulapi 9097	. . . . . . . . . 10 ⊢ ((6 / 3) = 2 ↔ (3 · 2) = 6)
127	125, 126	mpbir 146	. . . . . . . . 9 ⊢ (6 / 3) = 2
128	124, 127	oveq12i 6097	. . . . . . . 8 ⊢ ((2 · 5) · (6 / 3)) = (;10 · 2)
129	122, 128	eqtri 2259	. . . . . . 7 ⊢ (6 · ((2 · 5) / 3)) = (;10 · 2)
130	59, 114, 129	3eqtri 2263	. . . . . 6 ⊢ ((2 · 3)C3) = (;10 · 2)
131	42	oveq1i 6095	. . . . . . . . 9 ⊢ ((2 · 3) + 1) = (6 + 1)
132		df-7 9369	. . . . . . . . 9 ⊢ 7 = (6 + 1)
133	131, 132	eqtr4i 2262	. . . . . . . 8 ⊢ ((2 · 3) + 1) = 7
134		3p1e4 9441	. . . . . . . 8 ⊢ (3 + 1) = 4
135	133, 134	oveq12i 6097	. . . . . . 7 ⊢ (((2 · 3) + 1) / (3 + 1)) = (7 / 4)
136	135	oveq2i 6096	. . . . . 6 ⊢ (2 · (((2 · 3) + 1) / (3 + 1))) = (2 · (7 / 4))
137	130, 136	oveq12i 6097	. . . . 5 ⊢ (((2 · 3)C3) · (2 · (((2 · 3) + 1) / (3 + 1)))) = ((;10 · 2) · (2 · (7 / 4)))
138	54, 56, 137	3eqtri 2263	. . . 4 ⊢ ((2 · 4)C4) = ((;10 · 2) · (2 · (7 / 4)))
139		10nn 9794	. . . . . . 7 ⊢ ;10 ∈ ℕ
140	139	nncni 9315	. . . . . 6 ⊢ ;10 ∈ ℂ
141		7cn 9389	. . . . . . . 8 ⊢ 7 ∈ ℂ
142	141, 46, 47	divclapi 9085	. . . . . . 7 ⊢ (7 / 4) ∈ ℂ
143	32, 142	mulcli 8331	. . . . . 6 ⊢ (2 · (7 / 4)) ∈ ℂ
144	140, 32, 143	mulassi 8335	. . . . 5 ⊢ ((;10 · 2) · (2 · (7 / 4))) = (;10 · (2 · (2 · (7 / 4))))
145	102	oveq1i 6095	. . . . . . 7 ⊢ ((2 · 2) · (7 / 4)) = (4 · (7 / 4))
146	32, 32, 142	mulassi 8335	. . . . . . 7 ⊢ ((2 · 2) · (7 / 4)) = (2 · (2 · (7 / 4)))
147	141, 46, 47	divcanap2i 9086	. . . . . . 7 ⊢ (4 · (7 / 4)) = 7
148	145, 146, 147	3eqtr3i 2267	. . . . . 6 ⊢ (2 · (2 · (7 / 4))) = 7
149	148	oveq2i 6096	. . . . 5 ⊢ (;10 · (2 · (2 · (7 / 4)))) = (;10 · 7)
150	144, 149	eqtri 2259	. . . 4 ⊢ ((;10 · 2) · (2 · (7 / 4))) = (;10 · 7)
151	26	dec0u 9799	. . . 4 ⊢ (;10 · 7) = ;70
152	138, 150, 151	3eqtri 2263	. . 3 ⊢ ((2 · 4)C4) = ;70
153	31, 51, 152	3brtr4i 4160	. 2 ⊢ ((4↑4) / 4) < ((2 · 4)C4)
154		eluz4nn 9971	. . 3 ⊢ (𝑛 ∈ (ℤ_≥‘4) → 𝑛 ∈ ℕ)
155		4nn 9470	. . . . . . . . . 10 ⊢ 4 ∈ ℕ
156		nnnn0 9572	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℕ₀)
157		nnexpcl 10991	. . . . . . . . . 10 ⊢ ((4 ∈ ℕ ∧ 𝑛 ∈ ℕ₀) → (4↑𝑛) ∈ ℕ)
158	155, 156, 157	sylancr 418	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ → (4↑𝑛) ∈ ℕ)
159	158	nnrpd 10097	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ → (4↑𝑛) ∈ ℝ⁺)
160		nnrp 10066	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℝ⁺)
161	159, 160	rpdivcld 10117	. . . . . . 7 ⊢ (𝑛 ∈ ℕ → ((4↑𝑛) / 𝑛) ∈ ℝ⁺)
162	161	rpred 10099	. . . . . 6 ⊢ (𝑛 ∈ ℕ → ((4↑𝑛) / 𝑛) ∈ ℝ)
163		nnmulcl 9326	. . . . . . . . . 10 ⊢ ((2 ∈ ℕ ∧ 𝑛 ∈ ℕ) → (2 · 𝑛) ∈ ℕ)
164	116, 163	mpan 428	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ → (2 · 𝑛) ∈ ℕ)
165	164	nnnn0d 9622	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ → (2 · 𝑛) ∈ ℕ₀)
166		nnz 9665	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℤ)
167		bccl 11207	. . . . . . . 8 ⊢ (((2 · 𝑛) ∈ ℕ₀ ∧ 𝑛 ∈ ℤ) → ((2 · 𝑛)C𝑛) ∈ ℕ₀)
168	165, 166, 167	syl2anc 415	. . . . . . 7 ⊢ (𝑛 ∈ ℕ → ((2 · 𝑛)C𝑛) ∈ ℕ₀)
169	168	nn0red 9623	. . . . . 6 ⊢ (𝑛 ∈ ℕ → ((2 · 𝑛)C𝑛) ∈ ℝ)
170		2rp 10061	. . . . . . 7 ⊢ 2 ∈ ℝ⁺
171	164	peano2nnd 9320	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ → ((2 · 𝑛) + 1) ∈ ℕ)
172	171	nnrpd 10097	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ → ((2 · 𝑛) + 1) ∈ ℝ⁺)
173		peano2nn 9317	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℕ)
174	173	nnrpd 10097	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℝ⁺)
175	172, 174	rpdivcld 10117	. . . . . . 7 ⊢ (𝑛 ∈ ℕ → (((2 · 𝑛) + 1) / (𝑛 + 1)) ∈ ℝ⁺)
176		rpmulcl 10081	. . . . . . 7 ⊢ ((2 ∈ ℝ⁺ ∧ (((2 · 𝑛) + 1) / (𝑛 + 1)) ∈ ℝ⁺) → (2 · (((2 · 𝑛) + 1) / (𝑛 + 1))) ∈ ℝ⁺)
177	170, 175, 176	sylancr 418	. . . . . 6 ⊢ (𝑛 ∈ ℕ → (2 · (((2 · 𝑛) + 1) / (𝑛 + 1))) ∈ ℝ⁺)
178	162, 169, 177	ltmul1d 10141	. . . . 5 ⊢ (𝑛 ∈ ℕ → (((4↑𝑛) / 𝑛) < ((2 · 𝑛)C𝑛) ↔ (((4↑𝑛) / 𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))) < (((2 · 𝑛)C𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1))))))
179		bcp1ctr 16126	. . . . . . 7 ⊢ (𝑛 ∈ ℕ₀ → ((2 · (𝑛 + 1))C(𝑛 + 1)) = (((2 · 𝑛)C𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))))
180	156, 179	syl 14	. . . . . 6 ⊢ (𝑛 ∈ ℕ → ((2 · (𝑛 + 1))C(𝑛 + 1)) = (((2 · 𝑛)C𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))))
181	180	breq2d 4142	. . . . 5 ⊢ (𝑛 ∈ ℕ → ((((4↑𝑛) / 𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))) < ((2 · (𝑛 + 1))C(𝑛 + 1)) ↔ (((4↑𝑛) / 𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))) < (((2 · 𝑛)C𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1))))))
182	178, 181	bitr4d 191	. . . 4 ⊢ (𝑛 ∈ ℕ → (((4↑𝑛) / 𝑛) < ((2 · 𝑛)C𝑛) ↔ (((4↑𝑛) / 𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))) < ((2 · (𝑛 + 1))C(𝑛 + 1))))
183		2re 9375	. . . . . . . 8 ⊢ 2 ∈ ℝ
184	183	a1i 9	. . . . . . 7 ⊢ (𝑛 ∈ ℕ → 2 ∈ ℝ)
185	172, 160	rpdivcld 10117	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ → (((2 · 𝑛) + 1) / 𝑛) ∈ ℝ⁺)
186	185	rpred 10099	. . . . . . 7 ⊢ (𝑛 ∈ ℕ → (((2 · 𝑛) + 1) / 𝑛) ∈ ℝ)
187		nnmulcl 9326	. . . . . . . . . 10 ⊢ (((4↑𝑛) ∈ ℕ ∧ 2 ∈ ℕ) → ((4↑𝑛) · 2) ∈ ℕ)
188	158, 116, 187	sylancl 417	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ → ((4↑𝑛) · 2) ∈ ℕ)
189	188	nnrpd 10097	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ → ((4↑𝑛) · 2) ∈ ℝ⁺)
190	189, 174	rpdivcld 10117	. . . . . . 7 ⊢ (𝑛 ∈ ℕ → (((4↑𝑛) · 2) / (𝑛 + 1)) ∈ ℝ⁺)
191	160	rpreccld 10110	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ → (1 / 𝑛) ∈ ℝ⁺)
192		ltaddrp 10094	. . . . . . . . 9 ⊢ ((2 ∈ ℝ ∧ (1 / 𝑛) ∈ ℝ⁺) → 2 < (2 + (1 / 𝑛)))
193	183, 191, 192	sylancr 418	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ → 2 < (2 + (1 / 𝑛)))
194	164	nncnd 9319	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → (2 · 𝑛) ∈ ℂ)
195		1cnd 8342	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → 1 ∈ ℂ)
196		nncn 9313	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
197		nnap0 9334	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → 𝑛 # 0)
198	194, 195, 196, 197	divdirapd 9160	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ → (((2 · 𝑛) + 1) / 𝑛) = (((2 · 𝑛) / 𝑛) + (1 / 𝑛)))
199		2cnd 9378	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ → 2 ∈ ℂ)
200	199, 196, 197	divcanap4d 9127	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → ((2 · 𝑛) / 𝑛) = 2)
201	200	oveq1d 6100	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ → (((2 · 𝑛) / 𝑛) + (1 / 𝑛)) = (2 + (1 / 𝑛)))
202	198, 201	eqtr2d 2272	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ → (2 + (1 / 𝑛)) = (((2 · 𝑛) + 1) / 𝑛))
203	193, 202	breqtrd 4156	. . . . . . 7 ⊢ (𝑛 ∈ ℕ → 2 < (((2 · 𝑛) + 1) / 𝑛))
204	184, 186, 190, 203	ltmul2dd 10156	. . . . . 6 ⊢ (𝑛 ∈ ℕ → ((((4↑𝑛) · 2) / (𝑛 + 1)) · 2) < ((((4↑𝑛) · 2) / (𝑛 + 1)) · (((2 · 𝑛) + 1) / 𝑛)))
205		expp1 10985	. . . . . . . . . 10 ⊢ ((4 ∈ ℂ ∧ 𝑛 ∈ ℕ₀) → (4↑(𝑛 + 1)) = ((4↑𝑛) · 4))
206	46, 156, 205	sylancr 418	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ → (4↑(𝑛 + 1)) = ((4↑𝑛) · 4))
207	158	nncnd 9319	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ → (4↑𝑛) ∈ ℂ)
208	207, 199, 199	mulassd 8349	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → (((4↑𝑛) · 2) · 2) = ((4↑𝑛) · (2 · 2)))
209	102	oveq2i 6096	. . . . . . . . . 10 ⊢ ((4↑𝑛) · (2 · 2)) = ((4↑𝑛) · 4)
210	208, 209	eqtrdi 2287	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ → (((4↑𝑛) · 2) · 2) = ((4↑𝑛) · 4))
211	206, 210	eqtr4d 2274	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ → (4↑(𝑛 + 1)) = (((4↑𝑛) · 2) · 2))
212	211	oveq1d 6100	. . . . . . 7 ⊢ (𝑛 ∈ ℕ → ((4↑(𝑛 + 1)) / (𝑛 + 1)) = ((((4↑𝑛) · 2) · 2) / (𝑛 + 1)))
213	188	nncnd 9319	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ → ((4↑𝑛) · 2) ∈ ℂ)
214	173	nncnd 9319	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℂ)
215	173	nnap0d 9351	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ → (𝑛 + 1) # 0)
216	213, 199, 214, 215	div23apd 9159	. . . . . . 7 ⊢ (𝑛 ∈ ℕ → ((((4↑𝑛) · 2) · 2) / (𝑛 + 1)) = ((((4↑𝑛) · 2) / (𝑛 + 1)) · 2))
217	212, 216	eqtrd 2271	. . . . . 6 ⊢ (𝑛 ∈ ℕ → ((4↑(𝑛 + 1)) / (𝑛 + 1)) = ((((4↑𝑛) · 2) / (𝑛 + 1)) · 2))
218	207, 199, 196, 197	div23apd 9159	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ → (((4↑𝑛) · 2) / 𝑛) = (((4↑𝑛) / 𝑛) · 2))
219	218	oveq1d 6100	. . . . . . 7 ⊢ (𝑛 ∈ ℕ → ((((4↑𝑛) · 2) / 𝑛) · (((2 · 𝑛) + 1) / (𝑛 + 1))) = ((((4↑𝑛) / 𝑛) · 2) · (((2 · 𝑛) + 1) / (𝑛 + 1))))
220	171	nncnd 9319	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ → ((2 · 𝑛) + 1) ∈ ℂ)
221	196, 197	jca 306	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ → (𝑛 ∈ ℂ ∧ 𝑛 # 0))
222	214, 215	jca 306	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ → ((𝑛 + 1) ∈ ℂ ∧ (𝑛 + 1) # 0))
223		divmul24ap 9047	. . . . . . . 8 ⊢ (((((4↑𝑛) · 2) ∈ ℂ ∧ ((2 · 𝑛) + 1) ∈ ℂ) ∧ ((𝑛 ∈ ℂ ∧ 𝑛 # 0) ∧ ((𝑛 + 1) ∈ ℂ ∧ (𝑛 + 1) # 0))) → ((((4↑𝑛) · 2) / 𝑛) · (((2 · 𝑛) + 1) / (𝑛 + 1))) = ((((4↑𝑛) · 2) / (𝑛 + 1)) · (((2 · 𝑛) + 1) / 𝑛)))
224	213, 220, 221, 222, 223	syl22anc 1279	. . . . . . 7 ⊢ (𝑛 ∈ ℕ → ((((4↑𝑛) · 2) / 𝑛) · (((2 · 𝑛) + 1) / (𝑛 + 1))) = ((((4↑𝑛) · 2) / (𝑛 + 1)) · (((2 · 𝑛) + 1) / 𝑛)))
225	161	rpcnd 10101	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ → ((4↑𝑛) / 𝑛) ∈ ℂ)
226	175	rpcnd 10101	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ → (((2 · 𝑛) + 1) / (𝑛 + 1)) ∈ ℂ)
227	225, 199, 226	mulassd 8349	. . . . . . 7 ⊢ (𝑛 ∈ ℕ → ((((4↑𝑛) / 𝑛) · 2) · (((2 · 𝑛) + 1) / (𝑛 + 1))) = (((4↑𝑛) / 𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))))
228	219, 224, 227	3eqtr3rd 2280	. . . . . 6 ⊢ (𝑛 ∈ ℕ → (((4↑𝑛) / 𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))) = ((((4↑𝑛) · 2) / (𝑛 + 1)) · (((2 · 𝑛) + 1) / 𝑛)))
229	204, 217, 228	3brtr4d 4162	. . . . 5 ⊢ (𝑛 ∈ ℕ → ((4↑(𝑛 + 1)) / (𝑛 + 1)) < (((4↑𝑛) / 𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))))
230	173	nnnn0d 9622	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℕ₀)
231		nnexpcl 10991	. . . . . . . . . 10 ⊢ ((4 ∈ ℕ ∧ (𝑛 + 1) ∈ ℕ₀) → (4↑(𝑛 + 1)) ∈ ℕ)
232	155, 230, 231	sylancr 418	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ → (4↑(𝑛 + 1)) ∈ ℕ)
233	232	nnrpd 10097	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ → (4↑(𝑛 + 1)) ∈ ℝ⁺)
234	233, 174	rpdivcld 10117	. . . . . . 7 ⊢ (𝑛 ∈ ℕ → ((4↑(𝑛 + 1)) / (𝑛 + 1)) ∈ ℝ⁺)
235	234	rpred 10099	. . . . . 6 ⊢ (𝑛 ∈ ℕ → ((4↑(𝑛 + 1)) / (𝑛 + 1)) ∈ ℝ)
236	177	rpred 10099	. . . . . . 7 ⊢ (𝑛 ∈ ℕ → (2 · (((2 · 𝑛) + 1) / (𝑛 + 1))) ∈ ℝ)
237	162, 236	remulcld 8356	. . . . . 6 ⊢ (𝑛 ∈ ℕ → (((4↑𝑛) / 𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))) ∈ ℝ)
238		nn0mulcl 9601	. . . . . . . . 9 ⊢ ((2 ∈ ℕ₀ ∧ (𝑛 + 1) ∈ ℕ₀) → (2 · (𝑛 + 1)) ∈ ℕ₀)
239	33, 230, 238	sylancr 418	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ → (2 · (𝑛 + 1)) ∈ ℕ₀)
240	173	nnzd 9769	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℤ)
241		bccl 11207	. . . . . . . 8 ⊢ (((2 · (𝑛 + 1)) ∈ ℕ₀ ∧ (𝑛 + 1) ∈ ℤ) → ((2 · (𝑛 + 1))C(𝑛 + 1)) ∈ ℕ₀)
242	239, 240, 241	syl2anc 415	. . . . . . 7 ⊢ (𝑛 ∈ ℕ → ((2 · (𝑛 + 1))C(𝑛 + 1)) ∈ ℕ₀)
243	242	nn0red 9623	. . . . . 6 ⊢ (𝑛 ∈ ℕ → ((2 · (𝑛 + 1))C(𝑛 + 1)) ∈ ℝ)
244		lttr 8399	. . . . . 6 ⊢ ((((4↑(𝑛 + 1)) / (𝑛 + 1)) ∈ ℝ ∧ (((4↑𝑛) / 𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))) ∈ ℝ ∧ ((2 · (𝑛 + 1))C(𝑛 + 1)) ∈ ℝ) → ((((4↑(𝑛 + 1)) / (𝑛 + 1)) < (((4↑𝑛) / 𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))) ∧ (((4↑𝑛) / 𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))) < ((2 · (𝑛 + 1))C(𝑛 + 1))) → ((4↑(𝑛 + 1)) / (𝑛 + 1)) < ((2 · (𝑛 + 1))C(𝑛 + 1))))
245	235, 237, 243, 244	syl3anc 1278	. . . . 5 ⊢ (𝑛 ∈ ℕ → ((((4↑(𝑛 + 1)) / (𝑛 + 1)) < (((4↑𝑛) / 𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))) ∧ (((4↑𝑛) / 𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))) < ((2 · (𝑛 + 1))C(𝑛 + 1))) → ((4↑(𝑛 + 1)) / (𝑛 + 1)) < ((2 · (𝑛 + 1))C(𝑛 + 1))))
246	229, 245	mpand 433	. . . 4 ⊢ (𝑛 ∈ ℕ → ((((4↑𝑛) / 𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))) < ((2 · (𝑛 + 1))C(𝑛 + 1)) → ((4↑(𝑛 + 1)) / (𝑛 + 1)) < ((2 · (𝑛 + 1))C(𝑛 + 1))))
247	182, 246	sylbid 150	. . 3 ⊢ (𝑛 ∈ ℕ → (((4↑𝑛) / 𝑛) < ((2 · 𝑛)C𝑛) → ((4↑(𝑛 + 1)) / (𝑛 + 1)) < ((2 · (𝑛 + 1))C(𝑛 + 1))))
248	154, 247	syl 14	. 2 ⊢ (𝑛 ∈ (ℤ_≥‘4) → (((4↑𝑛) / 𝑛) < ((2 · 𝑛)C𝑛) → ((4↑(𝑛 + 1)) / (𝑛 + 1)) < ((2 · (𝑛 + 1))C(𝑛 + 1))))
249	6, 12, 18, 24, 153, 248	uzind4i 9994	1 ⊢ (𝑁 ∈ (ℤ_≥‘4) → ((4↑𝑁) / 𝑁) < ((2 · 𝑁)C𝑁))

Colors of variables: wff set class

This proof depends on syntax axioms: → wi 4 ∧ wa 104 = wceq 1402 ∈ wcel 2209 class class class wbr 4130 ‘cfv 5377 (class class class)co 6085 ℂcc 8177 ℝcr 8178 0cc0 8179 1c1 8180 + caddc 8182 · cmul 8184 < clt 8360 − cmin 8497 # cap 8910 / cdiv 9003 ℕcn 9305 2c2 9356 3c3 9357 4c4 9358 5c5 9359 6c6 9360 7c7 9361 ℕ₀cn0 9565 ℤcz 9646 cdc 9779 ℤ_≥cuz 9923 ℝ⁺crp 10056 ↑cexp 10977 Ccbc 11187

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 623 ax-in2 624 ax-io 721 ax-5 1500 ax-7 1501 ax-gen 1502 ax-ie1 1546 ax-ie2 1547 ax-8 1557 ax-10 1558 ax-11 1559 ax-i12 1560 ax-bndl 1562 ax-4 1563 ax-17 1579 ax-i9 1583 ax-ial 1587 ax-i5r 1588 ax-14 2212 ax-ext 2220 ax-coll 4246 ax-sep 4249 ax-nul 4259 ax-pow 4311 ax-pr 4346 ax-un 4578 ax-setind 4684 ax-iinf 4735 ax-cnex 8270 ax-resscn 8271 ax-1cn 8272 ax-1re 8273 ax-icn 8274 ax-addcl 8275 ax-addrcl 8276 ax-mulcl 8277 ax-mulrcl 8278 ax-addcom 8279 ax-mulcom 8280 ax-addass 8281 ax-mulass 8282 ax-distr 8283 ax-i2m1 8284 ax-0lt1 8285 ax-1rid 8286 ax-0id 8287 ax-rnegex 8288 ax-precex 8289 ax-cnre 8290 ax-pre-ltirr 8291 ax-pre-ltwlin 8292 ax-pre-lttrn 8293 ax-pre-apti 8294 ax-pre-ltadd 8295 ax-pre-mulgt0 8296 ax-pre-mulext 8297

This proof depends on definitions: df-bi 117 df-dc 847 df-3or 1010 df-3an 1011 df-tru 1405 df-fal 1408 df-nf 1514 df-sb 1816 df-eu 2089 df-mo 2090 df-clab 2225 df-cleq 2231 df-clel 2234 df-nfc 2381 df-ne 2421 df-nel 2516 df-ral 2533 df-rex 2534 df-reu 2535 df-rmo 2536 df-rab 2537 df-v 2823 df-sbc 3052 df-csb 3148 df-dif 3222 df-un 3224 df-in 3226 df-ss 3233 df-nul 3521 df-if 3639 df-pw 3690 df-sn 3715 df-pr 3716 df-op 3718 df-uni 3936 df-int 3971 df-iun 4014 df-br 4131 df-opab 4193 df-mpt 4194 df-tr 4230 df-id 4438 df-po 4441 df-iso 4442 df-iord 4511 df-on 4513 df-ilim 4514 df-suc 4516 df-iom 4738 df-xp 4780 df-rel 4781 df-cnv 4782 df-co 4783 df-dm 4784 df-rn 4785 df-res 4786 df-ima 4787 df-iota 5337 df-fun 5379 df-fn 5380 df-f 5381 df-f1 5382 df-fo 5383 df-f1o 5384 df-fv 5385 df-riota 6038 df-ov 6088 df-oprab 6089 df-mpo 6090 df-1st 6374 df-2nd 6375 df-recs 6576 df-frec 6662 df-pnf 8362 df-mnf 8363 df-xr 8364 df-ltxr 8365 df-le 8366 df-sub 8499 df-neg 8500 df-reap 8904 df-ap 8911 df-div 9004 df-inn 9306 df-2 9364 df-3 9365 df-4 9366 df-5 9367 df-6 9368 df-7 9369 df-8 9370 df-9 9371 df-n0 9566 df-z 9647 df-dec 9780 df-uz 9924 df-q 10022 df-rp 10057 df-fz 10414 df-seqfrec 10887 df-exp 10978 df-fac 11166 df-bc 11188

This theorem is used by: (None)

W3C validator