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

Theorem bclbnd 24749
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 11246 . 2 4 ∈ ℤ
2 oveq2 6534 . . . 4 (𝑥 = 4 → (4↑𝑥) = (4↑4))
3 id 22 . . . 4 (𝑥 = 4 → 𝑥 = 4)
42, 3oveq12d 6544 . . 3 (𝑥 = 4 → ((4↑𝑥) / 𝑥) = ((4↑4) / 4))
5 oveq2 6534 . . . 4 (𝑥 = 4 → (2 · 𝑥) = (2 · 4))
65, 3oveq12d 6544 . . 3 (𝑥 = 4 → ((2 · 𝑥)C𝑥) = ((2 · 4)C4))
74, 6breq12d 4590 . 2 (𝑥 = 4 → (((4↑𝑥) / 𝑥) < ((2 · 𝑥)C𝑥) ↔ ((4↑4) / 4) < ((2 · 4)C4)))
8 oveq2 6534 . . . 4 (𝑥 = 𝑛 → (4↑𝑥) = (4↑𝑛))
9 id 22 . . . 4 (𝑥 = 𝑛𝑥 = 𝑛)
108, 9oveq12d 6544 . . 3 (𝑥 = 𝑛 → ((4↑𝑥) / 𝑥) = ((4↑𝑛) / 𝑛))
11 oveq2 6534 . . . 4 (𝑥 = 𝑛 → (2 · 𝑥) = (2 · 𝑛))
1211, 9oveq12d 6544 . . 3 (𝑥 = 𝑛 → ((2 · 𝑥)C𝑥) = ((2 · 𝑛)C𝑛))
1310, 12breq12d 4590 . 2 (𝑥 = 𝑛 → (((4↑𝑥) / 𝑥) < ((2 · 𝑥)C𝑥) ↔ ((4↑𝑛) / 𝑛) < ((2 · 𝑛)C𝑛)))
14 oveq2 6534 . . . 4 (𝑥 = (𝑛 + 1) → (4↑𝑥) = (4↑(𝑛 + 1)))
15 id 22 . . . 4 (𝑥 = (𝑛 + 1) → 𝑥 = (𝑛 + 1))
1614, 15oveq12d 6544 . . 3 (𝑥 = (𝑛 + 1) → ((4↑𝑥) / 𝑥) = ((4↑(𝑛 + 1)) / (𝑛 + 1)))
17 oveq2 6534 . . . 4 (𝑥 = (𝑛 + 1) → (2 · 𝑥) = (2 · (𝑛 + 1)))
1817, 15oveq12d 6544 . . 3 (𝑥 = (𝑛 + 1) → ((2 · 𝑥)C𝑥) = ((2 · (𝑛 + 1))C(𝑛 + 1)))
1916, 18breq12d 4590 . 2 (𝑥 = (𝑛 + 1) → (((4↑𝑥) / 𝑥) < ((2 · 𝑥)C𝑥) ↔ ((4↑(𝑛 + 1)) / (𝑛 + 1)) < ((2 · (𝑛 + 1))C(𝑛 + 1))))
20 oveq2 6534 . . . 4 (𝑥 = 𝑁 → (4↑𝑥) = (4↑𝑁))
21 id 22 . . . 4 (𝑥 = 𝑁𝑥 = 𝑁)
2220, 21oveq12d 6544 . . 3 (𝑥 = 𝑁 → ((4↑𝑥) / 𝑥) = ((4↑𝑁) / 𝑁))
23 oveq2 6534 . . . 4 (𝑥 = 𝑁 → (2 · 𝑥) = (2 · 𝑁))
2423, 21oveq12d 6544 . . 3 (𝑥 = 𝑁 → ((2 · 𝑥)C𝑥) = ((2 · 𝑁)C𝑁))
2522, 24breq12d 4590 . 2 (𝑥 = 𝑁 → (((4↑𝑥) / 𝑥) < ((2 · 𝑥)C𝑥) ↔ ((4↑𝑁) / 𝑁) < ((2 · 𝑁)C𝑁)))
26 6nn0 11162 . . . 4 6 ∈ ℕ0
27 7nn0 11163 . . . 4 7 ∈ ℕ0
28 4nn0 11160 . . . 4 4 ∈ ℕ0
29 0nn0 11156 . . . 4 0 ∈ ℕ0
30 4lt10 11512 . . . 4 4 < 10
31 6lt7 11058 . . . 4 6 < 7
3226, 27, 28, 29, 30, 31decltc 11366 . . 3 64 < 70
33 2cn 10940 . . . . . 6 2 ∈ ℂ
34 2nn0 11158 . . . . . 6 2 ∈ ℕ0
35 3nn0 11159 . . . . . 6 3 ∈ ℕ0
36 expmul 12724 . . . . . 6 ((2 ∈ ℂ ∧ 2 ∈ ℕ0 ∧ 3 ∈ ℕ0) → (2↑(2 · 3)) = ((2↑2)↑3))
3733, 34, 35, 36mp3an 1415 . . . . 5 (2↑(2 · 3)) = ((2↑2)↑3)
38 sq2 12779 . . . . . . 7 (2↑2) = 4
3938eqcomi 2618 . . . . . 6 4 = (2↑2)
40 4m1e3 10987 . . . . . 6 (4 − 1) = 3
4139, 40oveq12i 6538 . . . . 5 (4↑(4 − 1)) = ((2↑2)↑3)
4237, 41eqtr4i 2634 . . . 4 (2↑(2 · 3)) = (4↑(4 − 1))
43 3cn 10944 . . . . . . 7 3 ∈ ℂ
44 3t2e6 11028 . . . . . . 7 (3 · 2) = 6
4543, 33, 44mulcomli 9903 . . . . . 6 (2 · 3) = 6
4645oveq2i 6537 . . . . 5 (2↑(2 · 3)) = (2↑6)
47 2exp6 15581 . . . . 5 (2↑6) = 64
4846, 47eqtri 2631 . . . 4 (2↑(2 · 3)) = 64
49 4cn 10947 . . . . 5 4 ∈ ℂ
50 4ne0 10966 . . . . 5 4 ≠ 0
51 expm1 12729 . . . . 5 ((4 ∈ ℂ ∧ 4 ≠ 0 ∧ 4 ∈ ℤ) → (4↑(4 − 1)) = ((4↑4) / 4))
5249, 50, 1, 51mp3an 1415 . . . 4 (4↑(4 − 1)) = ((4↑4) / 4)
5342, 48, 523eqtr3ri 2640 . . 3 ((4↑4) / 4) = 64
54 df-4 10930 . . . . . . 7 4 = (3 + 1)
5554oveq2i 6537 . . . . . 6 (2 · 4) = (2 · (3 + 1))
5655, 54oveq12i 6538 . . . . 5 ((2 · 4)C4) = ((2 · (3 + 1))C(3 + 1))
57 bcp1ctr 24748 . . . . . 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 10929 . . . . . . . . 9 3 = (2 + 1)
6059oveq2i 6537 . . . . . . . 8 (2 · 3) = (2 · (2 + 1))
6160, 59oveq12i 6538 . . . . . . 7 ((2 · 3)C3) = ((2 · (2 + 1))C(2 + 1))
62 bcp1ctr 24748 . . . . . . . . 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 10928 . . . . . . . . . . . 12 2 = (1 + 1)
6564oveq2i 6537 . . . . . . . . . . 11 (2 · 2) = (2 · (1 + 1))
6665, 64oveq12i 6538 . . . . . . . . . 10 ((2 · 2)C2) = ((2 · (1 + 1))C(1 + 1))
67 1nn0 11157 . . . . . . . . . . 11 1 ∈ ℕ0
68 bcp1ctr 24748 . . . . . . . . . . 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 11386 . . . . . . . . . . . . . . 15 1 = (0 + 1)
7170oveq2i 6537 . . . . . . . . . . . . . 14 (2 · 1) = (2 · (0 + 1))
7271, 70oveq12i 6538 . . . . . . . . . . . . 13 ((2 · 1)C1) = ((2 · (0 + 1))C(0 + 1))
73 bcp1ctr 24748 . . . . . . . . . . . . . 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 11180 . . . . . . . . . . . . . . . 16 (2 · 0) ∈ ℕ0
76 bcn0 12916 . . . . . . . . . . . . . . . 16 ((2 · 0) ∈ ℕ0 → ((2 · 0)C0) = 1)
7775, 76ax-mp 5 . . . . . . . . . . . . . . 15 ((2 · 0)C0) = 1
78 2t0e0 11032 . . . . . . . . . . . . . . . . . . . . 21 (2 · 0) = 0
7978oveq1i 6536 . . . . . . . . . . . . . . . . . . . 20 ((2 · 0) + 1) = (0 + 1)
8079, 70eqtr4i 2634 . . . . . . . . . . . . . . . . . . 19 ((2 · 0) + 1) = 1
8170eqcomi 2618 . . . . . . . . . . . . . . . . . . 19 (0 + 1) = 1
8280, 81oveq12i 6538 . . . . . . . . . . . . . . . . . 18 (((2 · 0) + 1) / (0 + 1)) = (1 / 1)
83 1div1e1 10568 . . . . . . . . . . . . . . . . . 18 (1 / 1) = 1
8482, 83eqtri 2631 . . . . . . . . . . . . . . . . 17 (((2 · 0) + 1) / (0 + 1)) = 1
8584oveq2i 6537 . . . . . . . . . . . . . . . 16 (2 · (((2 · 0) + 1) / (0 + 1))) = (2 · 1)
86 2t1e2 11025 . . . . . . . . . . . . . . . 16 (2 · 1) = 2
8785, 86eqtri 2631 . . . . . . . . . . . . . . 15 (2 · (((2 · 0) + 1) / (0 + 1))) = 2
8877, 87oveq12i 6538 . . . . . . . . . . . . . 14 (((2 · 0)C0) · (2 · (((2 · 0) + 1) / (0 + 1)))) = (1 · 2)
8933mulid2i 9899 . . . . . . . . . . . . . 14 (1 · 2) = 2
9088, 89eqtri 2631 . . . . . . . . . . . . 13 (((2 · 0)C0) · (2 · (((2 · 0) + 1) / (0 + 1)))) = 2
9172, 74, 903eqtri 2635 . . . . . . . . . . . 12 ((2 · 1)C1) = 2
9286oveq1i 6536 . . . . . . . . . . . . . . . 16 ((2 · 1) + 1) = (2 + 1)
9392, 59eqtr4i 2634 . . . . . . . . . . . . . . 15 ((2 · 1) + 1) = 3
9464eqcomi 2618 . . . . . . . . . . . . . . 15 (1 + 1) = 2
9593, 94oveq12i 6538 . . . . . . . . . . . . . 14 (((2 · 1) + 1) / (1 + 1)) = (3 / 2)
9695oveq2i 6537 . . . . . . . . . . . . 13 (2 · (((2 · 1) + 1) / (1 + 1))) = (2 · (3 / 2))
97 2ne0 10962 . . . . . . . . . . . . . 14 2 ≠ 0
9843, 33, 97divcan2i 10619 . . . . . . . . . . . . 13 (2 · (3 / 2)) = 3
9996, 98eqtri 2631 . . . . . . . . . . . 12 (2 · (((2 · 1) + 1) / (1 + 1))) = 3
10091, 99oveq12i 6538 . . . . . . . . . . 11 (((2 · 1)C1) · (2 · (((2 · 1) + 1) / (1 + 1)))) = (2 · 3)
101100, 45eqtri 2631 . . . . . . . . . 10 (((2 · 1)C1) · (2 · (((2 · 1) + 1) / (1 + 1)))) = 6
10266, 69, 1013eqtri 2635 . . . . . . . . 9 ((2 · 2)C2) = 6
103 2t2e4 11026 . . . . . . . . . . . . . 14 (2 · 2) = 4
104103oveq1i 6536 . . . . . . . . . . . . 13 ((2 · 2) + 1) = (4 + 1)
105 df-5 10931 . . . . . . . . . . . . 13 5 = (4 + 1)
106104, 105eqtr4i 2634 . . . . . . . . . . . 12 ((2 · 2) + 1) = 5
10759eqcomi 2618 . . . . . . . . . . . 12 (2 + 1) = 3
108106, 107oveq12i 6538 . . . . . . . . . . 11 (((2 · 2) + 1) / (2 + 1)) = (5 / 3)
109108oveq2i 6537 . . . . . . . . . 10 (2 · (((2 · 2) + 1) / (2 + 1))) = (2 · (5 / 3))
110 5cn 10949 . . . . . . . . . . 11 5 ∈ ℂ
111 3ne0 10964 . . . . . . . . . . 11 3 ≠ 0
11233, 110, 43, 111divassi 10632 . . . . . . . . . 10 ((2 · 5) / 3) = (2 · (5 / 3))
113109, 112eqtr4i 2634 . . . . . . . . 9 (2 · (((2 · 2) + 1) / (2 + 1))) = ((2 · 5) / 3)
114102, 113oveq12i 6538 . . . . . . . 8 (((2 · 2)C2) · (2 · (((2 · 2) + 1) / (2 + 1)))) = (6 · ((2 · 5) / 3))
11563, 114eqtri 2631 . . . . . . 7 ((2 · (2 + 1))C(2 + 1)) = (6 · ((2 · 5) / 3))
116 6cn 10951 . . . . . . . . 9 6 ∈ ℂ
117 2nn 11034 . . . . . . . . . . 11 2 ∈ ℕ
118 5nn 11037 . . . . . . . . . . 11 5 ∈ ℕ
119117, 118nnmulcli 10893 . . . . . . . . . 10 (2 · 5) ∈ ℕ
120119nncni 10879 . . . . . . . . 9 (2 · 5) ∈ ℂ
12143, 111pm3.2i 469 . . . . . . . . 9 (3 ∈ ℂ ∧ 3 ≠ 0)
122 div12 10558 . . . . . . . . 9 ((6 ∈ ℂ ∧ (2 · 5) ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → (6 · ((2 · 5) / 3)) = ((2 · 5) · (6 / 3)))
123116, 120, 121, 122mp3an 1415 . . . . . . . 8 (6 · ((2 · 5) / 3)) = ((2 · 5) · (6 / 3))
124 5t2e10 11468 . . . . . . . . . 10 (5 · 2) = 10
125110, 33, 124mulcomli 9903 . . . . . . . . 9 (2 · 5) = 10
126116, 43, 33, 111divmuli 10630 . . . . . . . . . 10 ((6 / 3) = 2 ↔ (3 · 2) = 6)
12744, 126mpbir 219 . . . . . . . . 9 (6 / 3) = 2
128125, 127oveq12i 6538 . . . . . . . 8 ((2 · 5) · (6 / 3)) = (10 · 2)
129123, 128eqtri 2631 . . . . . . 7 (6 · ((2 · 5) / 3)) = (10 · 2)
13061, 115, 1293eqtri 2635 . . . . . 6 ((2 · 3)C3) = (10 · 2)
13145oveq1i 6536 . . . . . . . . 9 ((2 · 3) + 1) = (6 + 1)
132 df-7 10933 . . . . . . . . 9 7 = (6 + 1)
133131, 132eqtr4i 2634 . . . . . . . 8 ((2 · 3) + 1) = 7
134 3p1e4 11002 . . . . . . . 8 (3 + 1) = 4
135133, 134oveq12i 6538 . . . . . . 7 (((2 · 3) + 1) / (3 + 1)) = (7 / 4)
136135oveq2i 6537 . . . . . 6 (2 · (((2 · 3) + 1) / (3 + 1))) = (2 · (7 / 4))
137130, 136oveq12i 6538 . . . . 5 (((2 · 3)C3) · (2 · (((2 · 3) + 1) / (3 + 1)))) = ((10 · 2) · (2 · (7 / 4)))
13856, 58, 1373eqtri 2635 . . . 4 ((2 · 4)C4) = ((10 · 2) · (2 · (7 / 4)))
139 10nn 11348 . . . . . . 7 10 ∈ ℕ
140139nncni 10879 . . . . . 6 10 ∈ ℂ
141 7cn 10953 . . . . . . . 8 7 ∈ ℂ
142141, 49, 50divcli 10618 . . . . . . 7 (7 / 4) ∈ ℂ
14333, 142mulcli 9901 . . . . . 6 (2 · (7 / 4)) ∈ ℂ
144140, 33, 143mulassi 9905 . . . . 5 ((10 · 2) · (2 · (7 / 4))) = (10 · (2 · (2 · (7 / 4))))
145103oveq1i 6536 . . . . . . 7 ((2 · 2) · (7 / 4)) = (4 · (7 / 4))
14633, 33, 142mulassi 9905 . . . . . . 7 ((2 · 2) · (7 / 4)) = (2 · (2 · (7 / 4)))
147141, 49, 50divcan2i 10619 . . . . . . 7 (4 · (7 / 4)) = 7
148145, 146, 1473eqtr3i 2639 . . . . . 6 (2 · (2 · (7 / 4))) = 7
149148oveq2i 6537 . . . . 5 (10 · (2 · (2 · (7 / 4)))) = (10 · 7)
150144, 149eqtri 2631 . . . 4 ((10 · 2) · (2 · (7 / 4))) = (10 · 7)
15127dec0u 11354 . . . 4 (10 · 7) = 70
152138, 150, 1513eqtri 2635 . . 3 ((2 · 4)C4) = 70
15332, 53, 1523brtr4i 4607 . 2 ((4↑4) / 4) < ((2 · 4)C4)
154 4nn 11036 . . . 4 4 ∈ ℕ
155 eluznn 11592 . . . 4 ((4 ∈ ℕ ∧ 𝑛 ∈ (ℤ‘4)) → 𝑛 ∈ ℕ)
156154, 155mpan 701 . . 3 (𝑛 ∈ (ℤ‘4) → 𝑛 ∈ ℕ)
157 nnnn0 11148 . . . . . . . . . 10 (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
158 nnexpcl 12692 . . . . . . . . . 10 ((4 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → (4↑𝑛) ∈ ℕ)
159154, 157, 158sylancr 693 . . . . . . . . 9 (𝑛 ∈ ℕ → (4↑𝑛) ∈ ℕ)
160159nnrpd 11704 . . . . . . . 8 (𝑛 ∈ ℕ → (4↑𝑛) ∈ ℝ+)
161 nnrp 11676 . . . . . . . 8 (𝑛 ∈ ℕ → 𝑛 ∈ ℝ+)
162160, 161rpdivcld 11723 . . . . . . 7 (𝑛 ∈ ℕ → ((4↑𝑛) / 𝑛) ∈ ℝ+)
163162rpred 11706 . . . . . 6 (𝑛 ∈ ℕ → ((4↑𝑛) / 𝑛) ∈ ℝ)
164 nnmulcl 10892 . . . . . . . . . 10 ((2 ∈ ℕ ∧ 𝑛 ∈ ℕ) → (2 · 𝑛) ∈ ℕ)
165117, 164mpan 701 . . . . . . . . 9 (𝑛 ∈ ℕ → (2 · 𝑛) ∈ ℕ)
166165nnnn0d 11200 . . . . . . . 8 (𝑛 ∈ ℕ → (2 · 𝑛) ∈ ℕ0)
167 nnz 11234 . . . . . . . 8 (𝑛 ∈ ℕ → 𝑛 ∈ ℤ)
168 bccl 12928 . . . . . . . 8 (((2 · 𝑛) ∈ ℕ0𝑛 ∈ ℤ) → ((2 · 𝑛)C𝑛) ∈ ℕ0)
169166, 167, 168syl2anc 690 . . . . . . 7 (𝑛 ∈ ℕ → ((2 · 𝑛)C𝑛) ∈ ℕ0)
170169nn0red 11201 . . . . . 6 (𝑛 ∈ ℕ → ((2 · 𝑛)C𝑛) ∈ ℝ)
171 2rp 11671 . . . . . . 7 2 ∈ ℝ+
172165peano2nnd 10886 . . . . . . . . 9 (𝑛 ∈ ℕ → ((2 · 𝑛) + 1) ∈ ℕ)
173172nnrpd 11704 . . . . . . . 8 (𝑛 ∈ ℕ → ((2 · 𝑛) + 1) ∈ ℝ+)
174 peano2nn 10881 . . . . . . . . 9 (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℕ)
175174nnrpd 11704 . . . . . . . 8 (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℝ+)
176173, 175rpdivcld 11723 . . . . . . 7 (𝑛 ∈ ℕ → (((2 · 𝑛) + 1) / (𝑛 + 1)) ∈ ℝ+)
177 rpmulcl 11689 . . . . . . 7 ((2 ∈ ℝ+ ∧ (((2 · 𝑛) + 1) / (𝑛 + 1)) ∈ ℝ+) → (2 · (((2 · 𝑛) + 1) / (𝑛 + 1))) ∈ ℝ+)
178171, 176, 177sylancr 693 . . . . . 6 (𝑛 ∈ ℕ → (2 · (((2 · 𝑛) + 1) / (𝑛 + 1))) ∈ ℝ+)
179163, 170, 178ltmul1d 11747 . . . . 5 (𝑛 ∈ ℕ → (((4↑𝑛) / 𝑛) < ((2 · 𝑛)C𝑛) ↔ (((4↑𝑛) / 𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))) < (((2 · 𝑛)C𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1))))))
180 bcp1ctr 24748 . . . . . . 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 4589 . . . . 5 (𝑛 ∈ ℕ → ((((4↑𝑛) / 𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))) < ((2 · (𝑛 + 1))C(𝑛 + 1)) ↔ (((4↑𝑛) / 𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))) < (((2 · 𝑛)C𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1))))))
183179, 182bitr4d 269 . . . 4 (𝑛 ∈ ℕ → (((4↑𝑛) / 𝑛) < ((2 · 𝑛)C𝑛) ↔ (((4↑𝑛) / 𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))) < ((2 · (𝑛 + 1))C(𝑛 + 1))))
184 2re 10939 . . . . . . . 8 2 ∈ ℝ
185184a1i 11 . . . . . . 7 (𝑛 ∈ ℕ → 2 ∈ ℝ)
186173, 161rpdivcld 11723 . . . . . . . 8 (𝑛 ∈ ℕ → (((2 · 𝑛) + 1) / 𝑛) ∈ ℝ+)
187186rpred 11706 . . . . . . 7 (𝑛 ∈ ℕ → (((2 · 𝑛) + 1) / 𝑛) ∈ ℝ)
188 nnmulcl 10892 . . . . . . . . . 10 (((4↑𝑛) ∈ ℕ ∧ 2 ∈ ℕ) → ((4↑𝑛) · 2) ∈ ℕ)
189159, 117, 188sylancl 692 . . . . . . . . 9 (𝑛 ∈ ℕ → ((4↑𝑛) · 2) ∈ ℕ)
190189nnrpd 11704 . . . . . . . 8 (𝑛 ∈ ℕ → ((4↑𝑛) · 2) ∈ ℝ+)
191190, 175rpdivcld 11723 . . . . . . 7 (𝑛 ∈ ℕ → (((4↑𝑛) · 2) / (𝑛 + 1)) ∈ ℝ+)
192161rpreccld 11716 . . . . . . . . 9 (𝑛 ∈ ℕ → (1 / 𝑛) ∈ ℝ+)
193 ltaddrp 11701 . . . . . . . . 9 ((2 ∈ ℝ ∧ (1 / 𝑛) ∈ ℝ+) → 2 < (2 + (1 / 𝑛)))
194184, 192, 193sylancr 693 . . . . . . . 8 (𝑛 ∈ ℕ → 2 < (2 + (1 / 𝑛)))
195165nncnd 10885 . . . . . . . . . 10 (𝑛 ∈ ℕ → (2 · 𝑛) ∈ ℂ)
196 1cnd 9912 . . . . . . . . . 10 (𝑛 ∈ ℕ → 1 ∈ ℂ)
197 nncn 10877 . . . . . . . . . 10 (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
198 nnne0 10902 . . . . . . . . . 10 (𝑛 ∈ ℕ → 𝑛 ≠ 0)
199195, 196, 197, 198divdird 10690 . . . . . . . . 9 (𝑛 ∈ ℕ → (((2 · 𝑛) + 1) / 𝑛) = (((2 · 𝑛) / 𝑛) + (1 / 𝑛)))
20033a1i 11 . . . . . . . . . . 11 (𝑛 ∈ ℕ → 2 ∈ ℂ)
201200, 197, 198divcan4d 10658 . . . . . . . . . 10 (𝑛 ∈ ℕ → ((2 · 𝑛) / 𝑛) = 2)
202201oveq1d 6541 . . . . . . . . 9 (𝑛 ∈ ℕ → (((2 · 𝑛) / 𝑛) + (1 / 𝑛)) = (2 + (1 / 𝑛)))
203199, 202eqtr2d 2644 . . . . . . . 8 (𝑛 ∈ ℕ → (2 + (1 / 𝑛)) = (((2 · 𝑛) + 1) / 𝑛))
204194, 203breqtrd 4603 . . . . . . 7 (𝑛 ∈ ℕ → 2 < (((2 · 𝑛) + 1) / 𝑛))
205185, 187, 191, 204ltmul2dd 11762 . . . . . 6 (𝑛 ∈ ℕ → ((((4↑𝑛) · 2) / (𝑛 + 1)) · 2) < ((((4↑𝑛) · 2) / (𝑛 + 1)) · (((2 · 𝑛) + 1) / 𝑛)))
206 expp1 12686 . . . . . . . . . 10 ((4 ∈ ℂ ∧ 𝑛 ∈ ℕ0) → (4↑(𝑛 + 1)) = ((4↑𝑛) · 4))
20749, 157, 206sylancr 693 . . . . . . . . 9 (𝑛 ∈ ℕ → (4↑(𝑛 + 1)) = ((4↑𝑛) · 4))
208159nncnd 10885 . . . . . . . . . . 11 (𝑛 ∈ ℕ → (4↑𝑛) ∈ ℂ)
209208, 200, 200mulassd 9919 . . . . . . . . . 10 (𝑛 ∈ ℕ → (((4↑𝑛) · 2) · 2) = ((4↑𝑛) · (2 · 2)))
210103oveq2i 6537 . . . . . . . . . 10 ((4↑𝑛) · (2 · 2)) = ((4↑𝑛) · 4)
211209, 210syl6eq 2659 . . . . . . . . 9 (𝑛 ∈ ℕ → (((4↑𝑛) · 2) · 2) = ((4↑𝑛) · 4))
212207, 211eqtr4d 2646 . . . . . . . 8 (𝑛 ∈ ℕ → (4↑(𝑛 + 1)) = (((4↑𝑛) · 2) · 2))
213212oveq1d 6541 . . . . . . 7 (𝑛 ∈ ℕ → ((4↑(𝑛 + 1)) / (𝑛 + 1)) = ((((4↑𝑛) · 2) · 2) / (𝑛 + 1)))
214189nncnd 10885 . . . . . . . 8 (𝑛 ∈ ℕ → ((4↑𝑛) · 2) ∈ ℂ)
215174nncnd 10885 . . . . . . . 8 (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℂ)
216174nnne0d 10914 . . . . . . . 8 (𝑛 ∈ ℕ → (𝑛 + 1) ≠ 0)
217214, 200, 215, 216div23d 10689 . . . . . . 7 (𝑛 ∈ ℕ → ((((4↑𝑛) · 2) · 2) / (𝑛 + 1)) = ((((4↑𝑛) · 2) / (𝑛 + 1)) · 2))
218213, 217eqtrd 2643 . . . . . 6 (𝑛 ∈ ℕ → ((4↑(𝑛 + 1)) / (𝑛 + 1)) = ((((4↑𝑛) · 2) / (𝑛 + 1)) · 2))
219208, 200, 197, 198div23d 10689 . . . . . . . 8 (𝑛 ∈ ℕ → (((4↑𝑛) · 2) / 𝑛) = (((4↑𝑛) / 𝑛) · 2))
220219oveq1d 6541 . . . . . . 7 (𝑛 ∈ ℕ → ((((4↑𝑛) · 2) / 𝑛) · (((2 · 𝑛) + 1) / (𝑛 + 1))) = ((((4↑𝑛) / 𝑛) · 2) · (((2 · 𝑛) + 1) / (𝑛 + 1))))
221172nncnd 10885 . . . . . . . 8 (𝑛 ∈ ℕ → ((2 · 𝑛) + 1) ∈ ℂ)
222214, 197, 221, 215, 198, 216divmul24d 10695 . . . . . . 7 (𝑛 ∈ ℕ → ((((4↑𝑛) · 2) / 𝑛) · (((2 · 𝑛) + 1) / (𝑛 + 1))) = ((((4↑𝑛) · 2) / (𝑛 + 1)) · (((2 · 𝑛) + 1) / 𝑛)))
223162rpcnd 11708 . . . . . . . 8 (𝑛 ∈ ℕ → ((4↑𝑛) / 𝑛) ∈ ℂ)
224176rpcnd 11708 . . . . . . . 8 (𝑛 ∈ ℕ → (((2 · 𝑛) + 1) / (𝑛 + 1)) ∈ ℂ)
225223, 200, 224mulassd 9919 . . . . . . 7 (𝑛 ∈ ℕ → ((((4↑𝑛) / 𝑛) · 2) · (((2 · 𝑛) + 1) / (𝑛 + 1))) = (((4↑𝑛) / 𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))))
226220, 222, 2253eqtr3rd 2652 . . . . . 6 (𝑛 ∈ ℕ → (((4↑𝑛) / 𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))) = ((((4↑𝑛) · 2) / (𝑛 + 1)) · (((2 · 𝑛) + 1) / 𝑛)))
227205, 218, 2263brtr4d 4609 . . . . 5 (𝑛 ∈ ℕ → ((4↑(𝑛 + 1)) / (𝑛 + 1)) < (((4↑𝑛) / 𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))))
228174nnnn0d 11200 . . . . . . . . . 10 (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℕ0)
229 nnexpcl 12692 . . . . . . . . . 10 ((4 ∈ ℕ ∧ (𝑛 + 1) ∈ ℕ0) → (4↑(𝑛 + 1)) ∈ ℕ)
230154, 228, 229sylancr 693 . . . . . . . . 9 (𝑛 ∈ ℕ → (4↑(𝑛 + 1)) ∈ ℕ)
231230nnrpd 11704 . . . . . . . 8 (𝑛 ∈ ℕ → (4↑(𝑛 + 1)) ∈ ℝ+)
232231, 175rpdivcld 11723 . . . . . . 7 (𝑛 ∈ ℕ → ((4↑(𝑛 + 1)) / (𝑛 + 1)) ∈ ℝ+)
233232rpred 11706 . . . . . 6 (𝑛 ∈ ℕ → ((4↑(𝑛 + 1)) / (𝑛 + 1)) ∈ ℝ)
234178rpred 11706 . . . . . . 7 (𝑛 ∈ ℕ → (2 · (((2 · 𝑛) + 1) / (𝑛 + 1))) ∈ ℝ)
235163, 234remulcld 9926 . . . . . 6 (𝑛 ∈ ℕ → (((4↑𝑛) / 𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))) ∈ ℝ)
236 nn0mulcl 11178 . . . . . . . . 9 ((2 ∈ ℕ0 ∧ (𝑛 + 1) ∈ ℕ0) → (2 · (𝑛 + 1)) ∈ ℕ0)
23734, 228, 236sylancr 693 . . . . . . . 8 (𝑛 ∈ ℕ → (2 · (𝑛 + 1)) ∈ ℕ0)
238174nnzd 11315 . . . . . . . 8 (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℤ)
239 bccl 12928 . . . . . . . 8 (((2 · (𝑛 + 1)) ∈ ℕ0 ∧ (𝑛 + 1) ∈ ℤ) → ((2 · (𝑛 + 1))C(𝑛 + 1)) ∈ ℕ0)
240237, 238, 239syl2anc 690 . . . . . . 7 (𝑛 ∈ ℕ → ((2 · (𝑛 + 1))C(𝑛 + 1)) ∈ ℕ0)
241240nn0red 11201 . . . . . 6 (𝑛 ∈ ℕ → ((2 · (𝑛 + 1))C(𝑛 + 1)) ∈ ℝ)
242 lttr 9965 . . . . . 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 1317 . . . . 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 706 . . . 4 (𝑛 ∈ ℕ → ((((4↑𝑛) / 𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))) < ((2 · (𝑛 + 1))C(𝑛 + 1)) → ((4↑(𝑛 + 1)) / (𝑛 + 1)) < ((2 · (𝑛 + 1))C(𝑛 + 1))))
245183, 244sylbid 228 . . 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 11584 1 (𝑁 ∈ (ℤ‘4) → ((4↑𝑁) / 𝑁) < ((2 · 𝑁)C𝑁))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1474  wcel 1976  wne 2779   class class class wbr 4577  cfv 5789  (class class class)co 6526  cc 9790  cr 9791  0cc0 9792  1c1 9793   + caddc 9795   · cmul 9797   < clt 9930  cmin 10117   / cdiv 10535  cn 10869  2c2 10919  3c3 10920  4c4 10921  5c5 10922  6c6 10923  7c7 10924  0cn0 11141  cz 11212  cdc 11327  cuz 11521  +crp 11666  cexp 12679  Ccbc 12908
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4711  ax-pow 4763  ax-pr 4827  ax-un 6824  ax-cnex 9848  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-mulcom 9856  ax-addass 9857  ax-mulass 9858  ax-distr 9859  ax-i2m1 9860  ax-1ne0 9861  ax-1rid 9862  ax-rnegex 9863  ax-rrecex 9864  ax-cnre 9865  ax-pre-lttri 9866  ax-pre-lttrn 9867  ax-pre-ltadd 9868  ax-pre-mulgt0 9869
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4938  df-id 4942  df-po 4948  df-so 4949  df-fr 4986  df-we 4988  df-xp 5033  df-rel 5034  df-cnv 5035  df-co 5036  df-dm 5037  df-rn 5038  df-res 5039  df-ima 5040  df-pred 5582  df-ord 5628  df-on 5629  df-lim 5630  df-suc 5631  df-iota 5753  df-fun 5791  df-fn 5792  df-f 5793  df-f1 5794  df-fo 5795  df-f1o 5796  df-fv 5797  df-riota 6488  df-ov 6529  df-oprab 6530  df-mpt2 6531  df-om 6935  df-1st 7036  df-2nd 7037  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-er 7606  df-en 7819  df-dom 7820  df-sdom 7821  df-pnf 9932  df-mnf 9933  df-xr 9934  df-ltxr 9935  df-le 9936  df-sub 10119  df-neg 10120  df-div 10536  df-nn 10870  df-2 10928  df-3 10929  df-4 10930  df-5 10931  df-6 10932  df-7 10933  df-8 10934  df-9 10935  df-n0 11142  df-z 11213  df-dec 11328  df-uz 11522  df-rp 11667  df-fz 12155  df-seq 12621  df-exp 12680  df-fac 12880  df-bc 12909
This theorem is referenced by:  bposlem6  24758  chebbnd1lem1  24902
  Copyright terms: Public domain W3C validator