MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bclbnd Structured version   Visualization version   GIF version

Theorem bclbnd 25204
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.
StepHypRef Expression
1 4z 11603 . 2 4 ∈ ℤ
2 oveq2 6821 . . . 4 (𝑥 = 4 → (4↑𝑥) = (4↑4))
3 id 22 . . . 4 (𝑥 = 4 → 𝑥 = 4)
42, 3oveq12d 6831 . . 3 (𝑥 = 4 → ((4↑𝑥) / 𝑥) = ((4↑4) / 4))
5 oveq2 6821 . . . 4 (𝑥 = 4 → (2 · 𝑥) = (2 · 4))
65, 3oveq12d 6831 . . 3 (𝑥 = 4 → ((2 · 𝑥)C𝑥) = ((2 · 4)C4))
74, 6breq12d 4817 . 2 (𝑥 = 4 → (((4↑𝑥) / 𝑥) < ((2 · 𝑥)C𝑥) ↔ ((4↑4) / 4) < ((2 · 4)C4)))
8 oveq2 6821 . . . 4 (𝑥 = 𝑛 → (4↑𝑥) = (4↑𝑛))
9 id 22 . . . 4 (𝑥 = 𝑛𝑥 = 𝑛)
108, 9oveq12d 6831 . . 3 (𝑥 = 𝑛 → ((4↑𝑥) / 𝑥) = ((4↑𝑛) / 𝑛))
11 oveq2 6821 . . . 4 (𝑥 = 𝑛 → (2 · 𝑥) = (2 · 𝑛))
1211, 9oveq12d 6831 . . 3 (𝑥 = 𝑛 → ((2 · 𝑥)C𝑥) = ((2 · 𝑛)C𝑛))
1310, 12breq12d 4817 . 2 (𝑥 = 𝑛 → (((4↑𝑥) / 𝑥) < ((2 · 𝑥)C𝑥) ↔ ((4↑𝑛) / 𝑛) < ((2 · 𝑛)C𝑛)))
14 oveq2 6821 . . . 4 (𝑥 = (𝑛 + 1) → (4↑𝑥) = (4↑(𝑛 + 1)))
15 id 22 . . . 4 (𝑥 = (𝑛 + 1) → 𝑥 = (𝑛 + 1))
1614, 15oveq12d 6831 . . 3 (𝑥 = (𝑛 + 1) → ((4↑𝑥) / 𝑥) = ((4↑(𝑛 + 1)) / (𝑛 + 1)))
17 oveq2 6821 . . . 4 (𝑥 = (𝑛 + 1) → (2 · 𝑥) = (2 · (𝑛 + 1)))
1817, 15oveq12d 6831 . . 3 (𝑥 = (𝑛 + 1) → ((2 · 𝑥)C𝑥) = ((2 · (𝑛 + 1))C(𝑛 + 1)))
1916, 18breq12d 4817 . 2 (𝑥 = (𝑛 + 1) → (((4↑𝑥) / 𝑥) < ((2 · 𝑥)C𝑥) ↔ ((4↑(𝑛 + 1)) / (𝑛 + 1)) < ((2 · (𝑛 + 1))C(𝑛 + 1))))
20 oveq2 6821 . . . 4 (𝑥 = 𝑁 → (4↑𝑥) = (4↑𝑁))
21 id 22 . . . 4 (𝑥 = 𝑁𝑥 = 𝑁)
2220, 21oveq12d 6831 . . 3 (𝑥 = 𝑁 → ((4↑𝑥) / 𝑥) = ((4↑𝑁) / 𝑁))
23 oveq2 6821 . . . 4 (𝑥 = 𝑁 → (2 · 𝑥) = (2 · 𝑁))
2423, 21oveq12d 6831 . . 3 (𝑥 = 𝑁 → ((2 · 𝑥)C𝑥) = ((2 · 𝑁)C𝑁))
2522, 24breq12d 4817 . 2 (𝑥 = 𝑁 → (((4↑𝑥) / 𝑥) < ((2 · 𝑥)C𝑥) ↔ ((4↑𝑁) / 𝑁) < ((2 · 𝑁)C𝑁)))
26 6nn0 11505 . . . 4 6 ∈ ℕ0
27 7nn0 11506 . . . 4 7 ∈ ℕ0
28 4nn0 11503 . . . 4 4 ∈ ℕ0
29 0nn0 11499 . . . 4 0 ∈ ℕ0
30 4lt10 11870 . . . 4 4 < 10
31 6lt7 11401 . . . 4 6 < 7
3226, 27, 28, 29, 30, 31decltc 11724 . . 3 64 < 70
33 2cn 11283 . . . . . 6 2 ∈ ℂ
34 2nn0 11501 . . . . . 6 2 ∈ ℕ0
35 3nn0 11502 . . . . . 6 3 ∈ ℕ0
36 expmul 13099 . . . . . 6 ((2 ∈ ℂ ∧ 2 ∈ ℕ0 ∧ 3 ∈ ℕ0) → (2↑(2 · 3)) = ((2↑2)↑3))
3733, 34, 35, 36mp3an 1573 . . . . 5 (2↑(2 · 3)) = ((2↑2)↑3)
38 sq2 13154 . . . . . . 7 (2↑2) = 4
3938eqcomi 2769 . . . . . 6 4 = (2↑2)
40 4m1e3 11330 . . . . . 6 (4 − 1) = 3
4139, 40oveq12i 6825 . . . . 5 (4↑(4 − 1)) = ((2↑2)↑3)
4237, 41eqtr4i 2785 . . . 4 (2↑(2 · 3)) = (4↑(4 − 1))
43 3cn 11287 . . . . . . 7 3 ∈ ℂ
44 3t2e6 11371 . . . . . . 7 (3 · 2) = 6
4543, 33, 44mulcomli 10239 . . . . . 6 (2 · 3) = 6
4645oveq2i 6824 . . . . 5 (2↑(2 · 3)) = (2↑6)
47 2exp6 15997 . . . . 5 (2↑6) = 64
4846, 47eqtri 2782 . . . 4 (2↑(2 · 3)) = 64
49 4cn 11290 . . . . 5 4 ∈ ℂ
50 4ne0 11309 . . . . 5 4 ≠ 0
51 expm1 13104 . . . . 5 ((4 ∈ ℂ ∧ 4 ≠ 0 ∧ 4 ∈ ℤ) → (4↑(4 − 1)) = ((4↑4) / 4))
5249, 50, 1, 51mp3an 1573 . . . 4 (4↑(4 − 1)) = ((4↑4) / 4)
5342, 48, 523eqtr3ri 2791 . . 3 ((4↑4) / 4) = 64
54 df-4 11273 . . . . . . 7 4 = (3 + 1)
5554oveq2i 6824 . . . . . 6 (2 · 4) = (2 · (3 + 1))
5655, 54oveq12i 6825 . . . . 5 ((2 · 4)C4) = ((2 · (3 + 1))C(3 + 1))
57 bcp1ctr 25203 . . . . . 6 (3 ∈ ℕ0 → ((2 · (3 + 1))C(3 + 1)) = (((2 · 3)C3) · (2 · (((2 · 3) + 1) / (3 + 1)))))
5835, 57ax-mp 5 . . . . 5 ((2 · (3 + 1))C(3 + 1)) = (((2 · 3)C3) · (2 · (((2 · 3) + 1) / (3 + 1))))
59 df-3 11272 . . . . . . . . 9 3 = (2 + 1)
6059oveq2i 6824 . . . . . . . 8 (2 · 3) = (2 · (2 + 1))
6160, 59oveq12i 6825 . . . . . . 7 ((2 · 3)C3) = ((2 · (2 + 1))C(2 + 1))
62 bcp1ctr 25203 . . . . . . . . 9 (2 ∈ ℕ0 → ((2 · (2 + 1))C(2 + 1)) = (((2 · 2)C2) · (2 · (((2 · 2) + 1) / (2 + 1)))))
6334, 62ax-mp 5 . . . . . . . 8 ((2 · (2 + 1))C(2 + 1)) = (((2 · 2)C2) · (2 · (((2 · 2) + 1) / (2 + 1))))
64 df-2 11271 . . . . . . . . . . . 12 2 = (1 + 1)
6564oveq2i 6824 . . . . . . . . . . 11 (2 · 2) = (2 · (1 + 1))
6665, 64oveq12i 6825 . . . . . . . . . 10 ((2 · 2)C2) = ((2 · (1 + 1))C(1 + 1))
67 1nn0 11500 . . . . . . . . . . 11 1 ∈ ℕ0
68 bcp1ctr 25203 . . . . . . . . . . 11 (1 ∈ ℕ0 → ((2 · (1 + 1))C(1 + 1)) = (((2 · 1)C1) · (2 · (((2 · 1) + 1) / (1 + 1)))))
6967, 68ax-mp 5 . . . . . . . . . 10 ((2 · (1 + 1))C(1 + 1)) = (((2 · 1)C1) · (2 · (((2 · 1) + 1) / (1 + 1))))
70 1e0p1 11744 . . . . . . . . . . . . . . 15 1 = (0 + 1)
7170oveq2i 6824 . . . . . . . . . . . . . 14 (2 · 1) = (2 · (0 + 1))
7271, 70oveq12i 6825 . . . . . . . . . . . . 13 ((2 · 1)C1) = ((2 · (0 + 1))C(0 + 1))
73 bcp1ctr 25203 . . . . . . . . . . . . . 14 (0 ∈ ℕ0 → ((2 · (0 + 1))C(0 + 1)) = (((2 · 0)C0) · (2 · (((2 · 0) + 1) / (0 + 1)))))
7429, 73ax-mp 5 . . . . . . . . . . . . 13 ((2 · (0 + 1))C(0 + 1)) = (((2 · 0)C0) · (2 · (((2 · 0) + 1) / (0 + 1))))
7534, 29nn0mulcli 11523 . . . . . . . . . . . . . . . 16 (2 · 0) ∈ ℕ0
76 bcn0 13291 . . . . . . . . . . . . . . . 16 ((2 · 0) ∈ ℕ0 → ((2 · 0)C0) = 1)
7775, 76ax-mp 5 . . . . . . . . . . . . . . 15 ((2 · 0)C0) = 1
78 2t0e0 11375 . . . . . . . . . . . . . . . . . . . . 21 (2 · 0) = 0
7978oveq1i 6823 . . . . . . . . . . . . . . . . . . . 20 ((2 · 0) + 1) = (0 + 1)
8079, 70eqtr4i 2785 . . . . . . . . . . . . . . . . . . 19 ((2 · 0) + 1) = 1
8170eqcomi 2769 . . . . . . . . . . . . . . . . . . 19 (0 + 1) = 1
8280, 81oveq12i 6825 . . . . . . . . . . . . . . . . . 18 (((2 · 0) + 1) / (0 + 1)) = (1 / 1)
83 1div1e1 10909 . . . . . . . . . . . . . . . . . 18 (1 / 1) = 1
8482, 83eqtri 2782 . . . . . . . . . . . . . . . . 17 (((2 · 0) + 1) / (0 + 1)) = 1
8584oveq2i 6824 . . . . . . . . . . . . . . . 16 (2 · (((2 · 0) + 1) / (0 + 1))) = (2 · 1)
86 2t1e2 11368 . . . . . . . . . . . . . . . 16 (2 · 1) = 2
8785, 86eqtri 2782 . . . . . . . . . . . . . . 15 (2 · (((2 · 0) + 1) / (0 + 1))) = 2
8877, 87oveq12i 6825 . . . . . . . . . . . . . 14 (((2 · 0)C0) · (2 · (((2 · 0) + 1) / (0 + 1)))) = (1 · 2)
8933mulid2i 10235 . . . . . . . . . . . . . 14 (1 · 2) = 2
9088, 89eqtri 2782 . . . . . . . . . . . . 13 (((2 · 0)C0) · (2 · (((2 · 0) + 1) / (0 + 1)))) = 2
9172, 74, 903eqtri 2786 . . . . . . . . . . . 12 ((2 · 1)C1) = 2
9286oveq1i 6823 . . . . . . . . . . . . . . . 16 ((2 · 1) + 1) = (2 + 1)
9392, 59eqtr4i 2785 . . . . . . . . . . . . . . 15 ((2 · 1) + 1) = 3
9464eqcomi 2769 . . . . . . . . . . . . . . 15 (1 + 1) = 2
9593, 94oveq12i 6825 . . . . . . . . . . . . . 14 (((2 · 1) + 1) / (1 + 1)) = (3 / 2)
9695oveq2i 6824 . . . . . . . . . . . . 13 (2 · (((2 · 1) + 1) / (1 + 1))) = (2 · (3 / 2))
97 2ne0 11305 . . . . . . . . . . . . . 14 2 ≠ 0
9843, 33, 97divcan2i 10960 . . . . . . . . . . . . 13 (2 · (3 / 2)) = 3
9996, 98eqtri 2782 . . . . . . . . . . . 12 (2 · (((2 · 1) + 1) / (1 + 1))) = 3
10091, 99oveq12i 6825 . . . . . . . . . . 11 (((2 · 1)C1) · (2 · (((2 · 1) + 1) / (1 + 1)))) = (2 · 3)
101100, 45eqtri 2782 . . . . . . . . . 10 (((2 · 1)C1) · (2 · (((2 · 1) + 1) / (1 + 1)))) = 6
10266, 69, 1013eqtri 2786 . . . . . . . . 9 ((2 · 2)C2) = 6
103 2t2e4 11369 . . . . . . . . . . . . . 14 (2 · 2) = 4
104103oveq1i 6823 . . . . . . . . . . . . 13 ((2 · 2) + 1) = (4 + 1)
105 df-5 11274 . . . . . . . . . . . . 13 5 = (4 + 1)
106104, 105eqtr4i 2785 . . . . . . . . . . . 12 ((2 · 2) + 1) = 5
10759eqcomi 2769 . . . . . . . . . . . 12 (2 + 1) = 3
108106, 107oveq12i 6825 . . . . . . . . . . 11 (((2 · 2) + 1) / (2 + 1)) = (5 / 3)
109108oveq2i 6824 . . . . . . . . . 10 (2 · (((2 · 2) + 1) / (2 + 1))) = (2 · (5 / 3))
110 5cn 11292 . . . . . . . . . . 11 5 ∈ ℂ
111 3ne0 11307 . . . . . . . . . . 11 3 ≠ 0
11233, 110, 43, 111divassi 10973 . . . . . . . . . 10 ((2 · 5) / 3) = (2 · (5 / 3))
113109, 112eqtr4i 2785 . . . . . . . . 9 (2 · (((2 · 2) + 1) / (2 + 1))) = ((2 · 5) / 3)
114102, 113oveq12i 6825 . . . . . . . 8 (((2 · 2)C2) · (2 · (((2 · 2) + 1) / (2 + 1)))) = (6 · ((2 · 5) / 3))
11563, 114eqtri 2782 . . . . . . 7 ((2 · (2 + 1))C(2 + 1)) = (6 · ((2 · 5) / 3))
116 6cn 11294 . . . . . . . . 9 6 ∈ ℂ
117 2nn 11377 . . . . . . . . . . 11 2 ∈ ℕ
118 5nn 11380 . . . . . . . . . . 11 5 ∈ ℕ
119117, 118nnmulcli 11236 . . . . . . . . . 10 (2 · 5) ∈ ℕ
120119nncni 11222 . . . . . . . . 9 (2 · 5) ∈ ℂ
12143, 111pm3.2i 470 . . . . . . . . 9 (3 ∈ ℂ ∧ 3 ≠ 0)
122 div12 10899 . . . . . . . . 9 ((6 ∈ ℂ ∧ (2 · 5) ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → (6 · ((2 · 5) / 3)) = ((2 · 5) · (6 / 3)))
123116, 120, 121, 122mp3an 1573 . . . . . . . 8 (6 · ((2 · 5) / 3)) = ((2 · 5) · (6 / 3))
124 5t2e10 11826 . . . . . . . . . 10 (5 · 2) = 10
125110, 33, 124mulcomli 10239 . . . . . . . . 9 (2 · 5) = 10
126116, 43, 33, 111divmuli 10971 . . . . . . . . . 10 ((6 / 3) = 2 ↔ (3 · 2) = 6)
12744, 126mpbir 221 . . . . . . . . 9 (6 / 3) = 2
128125, 127oveq12i 6825 . . . . . . . 8 ((2 · 5) · (6 / 3)) = (10 · 2)
129123, 128eqtri 2782 . . . . . . 7 (6 · ((2 · 5) / 3)) = (10 · 2)
13061, 115, 1293eqtri 2786 . . . . . 6 ((2 · 3)C3) = (10 · 2)
13145oveq1i 6823 . . . . . . . . 9 ((2 · 3) + 1) = (6 + 1)
132 df-7 11276 . . . . . . . . 9 7 = (6 + 1)
133131, 132eqtr4i 2785 . . . . . . . 8 ((2 · 3) + 1) = 7
134 3p1e4 11345 . . . . . . . 8 (3 + 1) = 4
135133, 134oveq12i 6825 . . . . . . 7 (((2 · 3) + 1) / (3 + 1)) = (7 / 4)
136135oveq2i 6824 . . . . . 6 (2 · (((2 · 3) + 1) / (3 + 1))) = (2 · (7 / 4))
137130, 136oveq12i 6825 . . . . 5 (((2 · 3)C3) · (2 · (((2 · 3) + 1) / (3 + 1)))) = ((10 · 2) · (2 · (7 / 4)))
13856, 58, 1373eqtri 2786 . . . 4 ((2 · 4)C4) = ((10 · 2) · (2 · (7 / 4)))
139 10nn 11706 . . . . . . 7 10 ∈ ℕ
140139nncni 11222 . . . . . 6 10 ∈ ℂ
141 7cn 11296 . . . . . . . 8 7 ∈ ℂ
142141, 49, 50divcli 10959 . . . . . . 7 (7 / 4) ∈ ℂ
14333, 142mulcli 10237 . . . . . 6 (2 · (7 / 4)) ∈ ℂ
144140, 33, 143mulassi 10241 . . . . 5 ((10 · 2) · (2 · (7 / 4))) = (10 · (2 · (2 · (7 / 4))))
145103oveq1i 6823 . . . . . . 7 ((2 · 2) · (7 / 4)) = (4 · (7 / 4))
14633, 33, 142mulassi 10241 . . . . . . 7 ((2 · 2) · (7 / 4)) = (2 · (2 · (7 / 4)))
147141, 49, 50divcan2i 10960 . . . . . . 7 (4 · (7 / 4)) = 7
148145, 146, 1473eqtr3i 2790 . . . . . 6 (2 · (2 · (7 / 4))) = 7
149148oveq2i 6824 . . . . 5 (10 · (2 · (2 · (7 / 4)))) = (10 · 7)
150144, 149eqtri 2782 . . . 4 ((10 · 2) · (2 · (7 / 4))) = (10 · 7)
15127dec0u 11712 . . . 4 (10 · 7) = 70
152138, 150, 1513eqtri 2786 . . 3 ((2 · 4)C4) = 70
15332, 53, 1523brtr4i 4834 . 2 ((4↑4) / 4) < ((2 · 4)C4)
154 4nn 11379 . . . 4 4 ∈ ℕ
155 eluznn 11951 . . . 4 ((4 ∈ ℕ ∧ 𝑛 ∈ (ℤ‘4)) → 𝑛 ∈ ℕ)
156154, 155mpan 708 . . 3 (𝑛 ∈ (ℤ‘4) → 𝑛 ∈ ℕ)
157 nnnn0 11491 . . . . . . . . . 10 (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
158 nnexpcl 13067 . . . . . . . . . 10 ((4 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → (4↑𝑛) ∈ ℕ)
159154, 157, 158sylancr 698 . . . . . . . . 9 (𝑛 ∈ ℕ → (4↑𝑛) ∈ ℕ)
160159nnrpd 12063 . . . . . . . 8 (𝑛 ∈ ℕ → (4↑𝑛) ∈ ℝ+)
161 nnrp 12035 . . . . . . . 8 (𝑛 ∈ ℕ → 𝑛 ∈ ℝ+)
162160, 161rpdivcld 12082 . . . . . . 7 (𝑛 ∈ ℕ → ((4↑𝑛) / 𝑛) ∈ ℝ+)
163162rpred 12065 . . . . . 6 (𝑛 ∈ ℕ → ((4↑𝑛) / 𝑛) ∈ ℝ)
164 nnmulcl 11235 . . . . . . . . . 10 ((2 ∈ ℕ ∧ 𝑛 ∈ ℕ) → (2 · 𝑛) ∈ ℕ)
165117, 164mpan 708 . . . . . . . . 9 (𝑛 ∈ ℕ → (2 · 𝑛) ∈ ℕ)
166165nnnn0d 11543 . . . . . . . 8 (𝑛 ∈ ℕ → (2 · 𝑛) ∈ ℕ0)
167 nnz 11591 . . . . . . . 8 (𝑛 ∈ ℕ → 𝑛 ∈ ℤ)
168 bccl 13303 . . . . . . . 8 (((2 · 𝑛) ∈ ℕ0𝑛 ∈ ℤ) → ((2 · 𝑛)C𝑛) ∈ ℕ0)
169166, 167, 168syl2anc 696 . . . . . . 7 (𝑛 ∈ ℕ → ((2 · 𝑛)C𝑛) ∈ ℕ0)
170169nn0red 11544 . . . . . 6 (𝑛 ∈ ℕ → ((2 · 𝑛)C𝑛) ∈ ℝ)
171 2rp 12030 . . . . . . 7 2 ∈ ℝ+
172165peano2nnd 11229 . . . . . . . . 9 (𝑛 ∈ ℕ → ((2 · 𝑛) + 1) ∈ ℕ)
173172nnrpd 12063 . . . . . . . 8 (𝑛 ∈ ℕ → ((2 · 𝑛) + 1) ∈ ℝ+)
174 peano2nn 11224 . . . . . . . . 9 (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℕ)
175174nnrpd 12063 . . . . . . . 8 (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℝ+)
176173, 175rpdivcld 12082 . . . . . . 7 (𝑛 ∈ ℕ → (((2 · 𝑛) + 1) / (𝑛 + 1)) ∈ ℝ+)
177 rpmulcl 12048 . . . . . . 7 ((2 ∈ ℝ+ ∧ (((2 · 𝑛) + 1) / (𝑛 + 1)) ∈ ℝ+) → (2 · (((2 · 𝑛) + 1) / (𝑛 + 1))) ∈ ℝ+)
178171, 176, 177sylancr 698 . . . . . 6 (𝑛 ∈ ℕ → (2 · (((2 · 𝑛) + 1) / (𝑛 + 1))) ∈ ℝ+)
179163, 170, 178ltmul1d 12106 . . . . 5 (𝑛 ∈ ℕ → (((4↑𝑛) / 𝑛) < ((2 · 𝑛)C𝑛) ↔ (((4↑𝑛) / 𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))) < (((2 · 𝑛)C𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1))))))
180 bcp1ctr 25203 . . . . . . 7 (𝑛 ∈ ℕ0 → ((2 · (𝑛 + 1))C(𝑛 + 1)) = (((2 · 𝑛)C𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))))
181157, 180syl 17 . . . . . 6 (𝑛 ∈ ℕ → ((2 · (𝑛 + 1))C(𝑛 + 1)) = (((2 · 𝑛)C𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))))
182181breq2d 4816 . . . . 5 (𝑛 ∈ ℕ → ((((4↑𝑛) / 𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))) < ((2 · (𝑛 + 1))C(𝑛 + 1)) ↔ (((4↑𝑛) / 𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))) < (((2 · 𝑛)C𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1))))))
183179, 182bitr4d 271 . . . 4 (𝑛 ∈ ℕ → (((4↑𝑛) / 𝑛) < ((2 · 𝑛)C𝑛) ↔ (((4↑𝑛) / 𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))) < ((2 · (𝑛 + 1))C(𝑛 + 1))))
184 2re 11282 . . . . . . . 8 2 ∈ ℝ
185184a1i 11 . . . . . . 7 (𝑛 ∈ ℕ → 2 ∈ ℝ)
186173, 161rpdivcld 12082 . . . . . . . 8 (𝑛 ∈ ℕ → (((2 · 𝑛) + 1) / 𝑛) ∈ ℝ+)
187186rpred 12065 . . . . . . 7 (𝑛 ∈ ℕ → (((2 · 𝑛) + 1) / 𝑛) ∈ ℝ)
188 nnmulcl 11235 . . . . . . . . . 10 (((4↑𝑛) ∈ ℕ ∧ 2 ∈ ℕ) → ((4↑𝑛) · 2) ∈ ℕ)
189159, 117, 188sylancl 697 . . . . . . . . 9 (𝑛 ∈ ℕ → ((4↑𝑛) · 2) ∈ ℕ)
190189nnrpd 12063 . . . . . . . 8 (𝑛 ∈ ℕ → ((4↑𝑛) · 2) ∈ ℝ+)
191190, 175rpdivcld 12082 . . . . . . 7 (𝑛 ∈ ℕ → (((4↑𝑛) · 2) / (𝑛 + 1)) ∈ ℝ+)
192161rpreccld 12075 . . . . . . . . 9 (𝑛 ∈ ℕ → (1 / 𝑛) ∈ ℝ+)
193 ltaddrp 12060 . . . . . . . . 9 ((2 ∈ ℝ ∧ (1 / 𝑛) ∈ ℝ+) → 2 < (2 + (1 / 𝑛)))
194184, 192, 193sylancr 698 . . . . . . . 8 (𝑛 ∈ ℕ → 2 < (2 + (1 / 𝑛)))
195165nncnd 11228 . . . . . . . . . 10 (𝑛 ∈ ℕ → (2 · 𝑛) ∈ ℂ)
196 1cnd 10248 . . . . . . . . . 10 (𝑛 ∈ ℕ → 1 ∈ ℂ)
197 nncn 11220 . . . . . . . . . 10 (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
198 nnne0 11245 . . . . . . . . . 10 (𝑛 ∈ ℕ → 𝑛 ≠ 0)
199195, 196, 197, 198divdird 11031 . . . . . . . . 9 (𝑛 ∈ ℕ → (((2 · 𝑛) + 1) / 𝑛) = (((2 · 𝑛) / 𝑛) + (1 / 𝑛)))
20033a1i 11 . . . . . . . . . . 11 (𝑛 ∈ ℕ → 2 ∈ ℂ)
201200, 197, 198divcan4d 10999 . . . . . . . . . 10 (𝑛 ∈ ℕ → ((2 · 𝑛) / 𝑛) = 2)
202201oveq1d 6828 . . . . . . . . 9 (𝑛 ∈ ℕ → (((2 · 𝑛) / 𝑛) + (1 / 𝑛)) = (2 + (1 / 𝑛)))
203199, 202eqtr2d 2795 . . . . . . . 8 (𝑛 ∈ ℕ → (2 + (1 / 𝑛)) = (((2 · 𝑛) + 1) / 𝑛))
204194, 203breqtrd 4830 . . . . . . 7 (𝑛 ∈ ℕ → 2 < (((2 · 𝑛) + 1) / 𝑛))
205185, 187, 191, 204ltmul2dd 12121 . . . . . 6 (𝑛 ∈ ℕ → ((((4↑𝑛) · 2) / (𝑛 + 1)) · 2) < ((((4↑𝑛) · 2) / (𝑛 + 1)) · (((2 · 𝑛) + 1) / 𝑛)))
206 expp1 13061 . . . . . . . . . 10 ((4 ∈ ℂ ∧ 𝑛 ∈ ℕ0) → (4↑(𝑛 + 1)) = ((4↑𝑛) · 4))
20749, 157, 206sylancr 698 . . . . . . . . 9 (𝑛 ∈ ℕ → (4↑(𝑛 + 1)) = ((4↑𝑛) · 4))
208159nncnd 11228 . . . . . . . . . . 11 (𝑛 ∈ ℕ → (4↑𝑛) ∈ ℂ)
209208, 200, 200mulassd 10255 . . . . . . . . . 10 (𝑛 ∈ ℕ → (((4↑𝑛) · 2) · 2) = ((4↑𝑛) · (2 · 2)))
210103oveq2i 6824 . . . . . . . . . 10 ((4↑𝑛) · (2 · 2)) = ((4↑𝑛) · 4)
211209, 210syl6eq 2810 . . . . . . . . 9 (𝑛 ∈ ℕ → (((4↑𝑛) · 2) · 2) = ((4↑𝑛) · 4))
212207, 211eqtr4d 2797 . . . . . . . 8 (𝑛 ∈ ℕ → (4↑(𝑛 + 1)) = (((4↑𝑛) · 2) · 2))
213212oveq1d 6828 . . . . . . 7 (𝑛 ∈ ℕ → ((4↑(𝑛 + 1)) / (𝑛 + 1)) = ((((4↑𝑛) · 2) · 2) / (𝑛 + 1)))
214189nncnd 11228 . . . . . . . 8 (𝑛 ∈ ℕ → ((4↑𝑛) · 2) ∈ ℂ)
215174nncnd 11228 . . . . . . . 8 (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℂ)
216174nnne0d 11257 . . . . . . . 8 (𝑛 ∈ ℕ → (𝑛 + 1) ≠ 0)
217214, 200, 215, 216div23d 11030 . . . . . . 7 (𝑛 ∈ ℕ → ((((4↑𝑛) · 2) · 2) / (𝑛 + 1)) = ((((4↑𝑛) · 2) / (𝑛 + 1)) · 2))
218213, 217eqtrd 2794 . . . . . 6 (𝑛 ∈ ℕ → ((4↑(𝑛 + 1)) / (𝑛 + 1)) = ((((4↑𝑛) · 2) / (𝑛 + 1)) · 2))
219208, 200, 197, 198div23d 11030 . . . . . . . 8 (𝑛 ∈ ℕ → (((4↑𝑛) · 2) / 𝑛) = (((4↑𝑛) / 𝑛) · 2))
220219oveq1d 6828 . . . . . . 7 (𝑛 ∈ ℕ → ((((4↑𝑛) · 2) / 𝑛) · (((2 · 𝑛) + 1) / (𝑛 + 1))) = ((((4↑𝑛) / 𝑛) · 2) · (((2 · 𝑛) + 1) / (𝑛 + 1))))
221172nncnd 11228 . . . . . . . 8 (𝑛 ∈ ℕ → ((2 · 𝑛) + 1) ∈ ℂ)
222214, 197, 221, 215, 198, 216divmul24d 11036 . . . . . . 7 (𝑛 ∈ ℕ → ((((4↑𝑛) · 2) / 𝑛) · (((2 · 𝑛) + 1) / (𝑛 + 1))) = ((((4↑𝑛) · 2) / (𝑛 + 1)) · (((2 · 𝑛) + 1) / 𝑛)))
223162rpcnd 12067 . . . . . . . 8 (𝑛 ∈ ℕ → ((4↑𝑛) / 𝑛) ∈ ℂ)
224176rpcnd 12067 . . . . . . . 8 (𝑛 ∈ ℕ → (((2 · 𝑛) + 1) / (𝑛 + 1)) ∈ ℂ)
225223, 200, 224mulassd 10255 . . . . . . 7 (𝑛 ∈ ℕ → ((((4↑𝑛) / 𝑛) · 2) · (((2 · 𝑛) + 1) / (𝑛 + 1))) = (((4↑𝑛) / 𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))))
226220, 222, 2253eqtr3rd 2803 . . . . . 6 (𝑛 ∈ ℕ → (((4↑𝑛) / 𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))) = ((((4↑𝑛) · 2) / (𝑛 + 1)) · (((2 · 𝑛) + 1) / 𝑛)))
227205, 218, 2263brtr4d 4836 . . . . 5 (𝑛 ∈ ℕ → ((4↑(𝑛 + 1)) / (𝑛 + 1)) < (((4↑𝑛) / 𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))))
228174nnnn0d 11543 . . . . . . . . . 10 (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℕ0)
229 nnexpcl 13067 . . . . . . . . . 10 ((4 ∈ ℕ ∧ (𝑛 + 1) ∈ ℕ0) → (4↑(𝑛 + 1)) ∈ ℕ)
230154, 228, 229sylancr 698 . . . . . . . . 9 (𝑛 ∈ ℕ → (4↑(𝑛 + 1)) ∈ ℕ)
231230nnrpd 12063 . . . . . . . 8 (𝑛 ∈ ℕ → (4↑(𝑛 + 1)) ∈ ℝ+)
232231, 175rpdivcld 12082 . . . . . . 7 (𝑛 ∈ ℕ → ((4↑(𝑛 + 1)) / (𝑛 + 1)) ∈ ℝ+)
233232rpred 12065 . . . . . 6 (𝑛 ∈ ℕ → ((4↑(𝑛 + 1)) / (𝑛 + 1)) ∈ ℝ)
234178rpred 12065 . . . . . . 7 (𝑛 ∈ ℕ → (2 · (((2 · 𝑛) + 1) / (𝑛 + 1))) ∈ ℝ)
235163, 234remulcld 10262 . . . . . 6 (𝑛 ∈ ℕ → (((4↑𝑛) / 𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))) ∈ ℝ)
236 nn0mulcl 11521 . . . . . . . . 9 ((2 ∈ ℕ0 ∧ (𝑛 + 1) ∈ ℕ0) → (2 · (𝑛 + 1)) ∈ ℕ0)
23734, 228, 236sylancr 698 . . . . . . . 8 (𝑛 ∈ ℕ → (2 · (𝑛 + 1)) ∈ ℕ0)
238174nnzd 11673 . . . . . . . 8 (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℤ)
239 bccl 13303 . . . . . . . 8 (((2 · (𝑛 + 1)) ∈ ℕ0 ∧ (𝑛 + 1) ∈ ℤ) → ((2 · (𝑛 + 1))C(𝑛 + 1)) ∈ ℕ0)
240237, 238, 239syl2anc 696 . . . . . . 7 (𝑛 ∈ ℕ → ((2 · (𝑛 + 1))C(𝑛 + 1)) ∈ ℕ0)
241240nn0red 11544 . . . . . 6 (𝑛 ∈ ℕ → ((2 · (𝑛 + 1))C(𝑛 + 1)) ∈ ℝ)
242 lttr 10306 . . . . . 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))))
243233, 235, 241, 242syl3anc 1477 . . . . 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))))
244227, 243mpand 713 . . . 4 (𝑛 ∈ ℕ → ((((4↑𝑛) / 𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))) < ((2 · (𝑛 + 1))C(𝑛 + 1)) → ((4↑(𝑛 + 1)) / (𝑛 + 1)) < ((2 · (𝑛 + 1))C(𝑛 + 1))))
245183, 244sylbid 230 . . 3 (𝑛 ∈ ℕ → (((4↑𝑛) / 𝑛) < ((2 · 𝑛)C𝑛) → ((4↑(𝑛 + 1)) / (𝑛 + 1)) < ((2 · (𝑛 + 1))C(𝑛 + 1))))
246156, 245syl 17 . 2 (𝑛 ∈ (ℤ‘4) → (((4↑𝑛) / 𝑛) < ((2 · 𝑛)C𝑛) → ((4↑(𝑛 + 1)) / (𝑛 + 1)) < ((2 · (𝑛 + 1))C(𝑛 + 1))))
2471, 7, 13, 19, 25, 153, 246uzind4i 11943 1 (𝑁 ∈ (ℤ‘4) → ((4↑𝑁) / 𝑁) < ((2 · 𝑁)C𝑁))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1632  wcel 2139  wne 2932   class class class wbr 4804  cfv 6049  (class class class)co 6813  cc 10126  cr 10127  0cc0 10128  1c1 10129   + caddc 10131   · cmul 10133   < clt 10266  cmin 10458   / cdiv 10876  cn 11212  2c2 11262  3c3 11263  4c4 11264  5c5 11265  6c6 11266  7c7 11267  0cn0 11484  cz 11569  cdc 11685  cuz 11879  +crp 12025  cexp 13054  Ccbc 13283
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-cnex 10184  ax-resscn 10185  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-addrcl 10189  ax-mulcl 10190  ax-mulrcl 10191  ax-mulcom 10192  ax-addass 10193  ax-mulass 10194  ax-distr 10195  ax-i2m1 10196  ax-1ne0 10197  ax-1rid 10198  ax-rnegex 10199  ax-rrecex 10200  ax-cnre 10201  ax-pre-lttri 10202  ax-pre-lttrn 10203  ax-pre-ltadd 10204  ax-pre-mulgt0 10205
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-riota 6774  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-om 7231  df-1st 7333  df-2nd 7334  df-wrecs 7576  df-recs 7637  df-rdg 7675  df-er 7911  df-en 8122  df-dom 8123  df-sdom 8124  df-pnf 10268  df-mnf 10269  df-xr 10270  df-ltxr 10271  df-le 10272  df-sub 10460  df-neg 10461  df-div 10877  df-nn 11213  df-2 11271  df-3 11272  df-4 11273  df-5 11274  df-6 11275  df-7 11276  df-8 11277  df-9 11278  df-n0 11485  df-z 11570  df-dec 11686  df-uz 11880  df-rp 12026  df-fz 12520  df-seq 12996  df-exp 13055  df-fac 13255  df-bc 13284
This theorem is referenced by:  bposlem6  25213  chebbnd1lem1  25357
  Copyright terms: Public domain W3C validator