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

Theorem bclbnd 24939
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 11371 . 2 4 ∈ ℤ
2 oveq2 6623 . . . 4 (𝑥 = 4 → (4↑𝑥) = (4↑4))
3 id 22 . . . 4 (𝑥 = 4 → 𝑥 = 4)
42, 3oveq12d 6633 . . 3 (𝑥 = 4 → ((4↑𝑥) / 𝑥) = ((4↑4) / 4))
5 oveq2 6623 . . . 4 (𝑥 = 4 → (2 · 𝑥) = (2 · 4))
65, 3oveq12d 6633 . . 3 (𝑥 = 4 → ((2 · 𝑥)C𝑥) = ((2 · 4)C4))
74, 6breq12d 4636 . 2 (𝑥 = 4 → (((4↑𝑥) / 𝑥) < ((2 · 𝑥)C𝑥) ↔ ((4↑4) / 4) < ((2 · 4)C4)))
8 oveq2 6623 . . . 4 (𝑥 = 𝑛 → (4↑𝑥) = (4↑𝑛))
9 id 22 . . . 4 (𝑥 = 𝑛𝑥 = 𝑛)
108, 9oveq12d 6633 . . 3 (𝑥 = 𝑛 → ((4↑𝑥) / 𝑥) = ((4↑𝑛) / 𝑛))
11 oveq2 6623 . . . 4 (𝑥 = 𝑛 → (2 · 𝑥) = (2 · 𝑛))
1211, 9oveq12d 6633 . . 3 (𝑥 = 𝑛 → ((2 · 𝑥)C𝑥) = ((2 · 𝑛)C𝑛))
1310, 12breq12d 4636 . 2 (𝑥 = 𝑛 → (((4↑𝑥) / 𝑥) < ((2 · 𝑥)C𝑥) ↔ ((4↑𝑛) / 𝑛) < ((2 · 𝑛)C𝑛)))
14 oveq2 6623 . . . 4 (𝑥 = (𝑛 + 1) → (4↑𝑥) = (4↑(𝑛 + 1)))
15 id 22 . . . 4 (𝑥 = (𝑛 + 1) → 𝑥 = (𝑛 + 1))
1614, 15oveq12d 6633 . . 3 (𝑥 = (𝑛 + 1) → ((4↑𝑥) / 𝑥) = ((4↑(𝑛 + 1)) / (𝑛 + 1)))
17 oveq2 6623 . . . 4 (𝑥 = (𝑛 + 1) → (2 · 𝑥) = (2 · (𝑛 + 1)))
1817, 15oveq12d 6633 . . 3 (𝑥 = (𝑛 + 1) → ((2 · 𝑥)C𝑥) = ((2 · (𝑛 + 1))C(𝑛 + 1)))
1916, 18breq12d 4636 . 2 (𝑥 = (𝑛 + 1) → (((4↑𝑥) / 𝑥) < ((2 · 𝑥)C𝑥) ↔ ((4↑(𝑛 + 1)) / (𝑛 + 1)) < ((2 · (𝑛 + 1))C(𝑛 + 1))))
20 oveq2 6623 . . . 4 (𝑥 = 𝑁 → (4↑𝑥) = (4↑𝑁))
21 id 22 . . . 4 (𝑥 = 𝑁𝑥 = 𝑁)
2220, 21oveq12d 6633 . . 3 (𝑥 = 𝑁 → ((4↑𝑥) / 𝑥) = ((4↑𝑁) / 𝑁))
23 oveq2 6623 . . . 4 (𝑥 = 𝑁 → (2 · 𝑥) = (2 · 𝑁))
2423, 21oveq12d 6633 . . 3 (𝑥 = 𝑁 → ((2 · 𝑥)C𝑥) = ((2 · 𝑁)C𝑁))
2522, 24breq12d 4636 . 2 (𝑥 = 𝑁 → (((4↑𝑥) / 𝑥) < ((2 · 𝑥)C𝑥) ↔ ((4↑𝑁) / 𝑁) < ((2 · 𝑁)C𝑁)))
26 6nn0 11273 . . . 4 6 ∈ ℕ0
27 7nn0 11274 . . . 4 7 ∈ ℕ0
28 4nn0 11271 . . . 4 4 ∈ ℕ0
29 0nn0 11267 . . . 4 0 ∈ ℕ0
30 4lt10 11638 . . . 4 4 < 10
31 6lt7 11169 . . . 4 6 < 7
3226, 27, 28, 29, 30, 31decltc 11492 . . 3 64 < 70
33 2cn 11051 . . . . . 6 2 ∈ ℂ
34 2nn0 11269 . . . . . 6 2 ∈ ℕ0
35 3nn0 11270 . . . . . 6 3 ∈ ℕ0
36 expmul 12861 . . . . . 6 ((2 ∈ ℂ ∧ 2 ∈ ℕ0 ∧ 3 ∈ ℕ0) → (2↑(2 · 3)) = ((2↑2)↑3))
3733, 34, 35, 36mp3an 1421 . . . . 5 (2↑(2 · 3)) = ((2↑2)↑3)
38 sq2 12916 . . . . . . 7 (2↑2) = 4
3938eqcomi 2630 . . . . . 6 4 = (2↑2)
40 4m1e3 11098 . . . . . 6 (4 − 1) = 3
4139, 40oveq12i 6627 . . . . 5 (4↑(4 − 1)) = ((2↑2)↑3)
4237, 41eqtr4i 2646 . . . 4 (2↑(2 · 3)) = (4↑(4 − 1))
43 3cn 11055 . . . . . . 7 3 ∈ ℂ
44 3t2e6 11139 . . . . . . 7 (3 · 2) = 6
4543, 33, 44mulcomli 10007 . . . . . 6 (2 · 3) = 6
4645oveq2i 6626 . . . . 5 (2↑(2 · 3)) = (2↑6)
47 2exp6 15738 . . . . 5 (2↑6) = 64
4846, 47eqtri 2643 . . . 4 (2↑(2 · 3)) = 64
49 4cn 11058 . . . . 5 4 ∈ ℂ
50 4ne0 11077 . . . . 5 4 ≠ 0
51 expm1 12866 . . . . 5 ((4 ∈ ℂ ∧ 4 ≠ 0 ∧ 4 ∈ ℤ) → (4↑(4 − 1)) = ((4↑4) / 4))
5249, 50, 1, 51mp3an 1421 . . . 4 (4↑(4 − 1)) = ((4↑4) / 4)
5342, 48, 523eqtr3ri 2652 . . 3 ((4↑4) / 4) = 64
54 df-4 11041 . . . . . . 7 4 = (3 + 1)
5554oveq2i 6626 . . . . . 6 (2 · 4) = (2 · (3 + 1))
5655, 54oveq12i 6627 . . . . 5 ((2 · 4)C4) = ((2 · (3 + 1))C(3 + 1))
57 bcp1ctr 24938 . . . . . 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 11040 . . . . . . . . 9 3 = (2 + 1)
6059oveq2i 6626 . . . . . . . 8 (2 · 3) = (2 · (2 + 1))
6160, 59oveq12i 6627 . . . . . . 7 ((2 · 3)C3) = ((2 · (2 + 1))C(2 + 1))
62 bcp1ctr 24938 . . . . . . . . 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 11039 . . . . . . . . . . . 12 2 = (1 + 1)
6564oveq2i 6626 . . . . . . . . . . 11 (2 · 2) = (2 · (1 + 1))
6665, 64oveq12i 6627 . . . . . . . . . 10 ((2 · 2)C2) = ((2 · (1 + 1))C(1 + 1))
67 1nn0 11268 . . . . . . . . . . 11 1 ∈ ℕ0
68 bcp1ctr 24938 . . . . . . . . . . 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 11512 . . . . . . . . . . . . . . 15 1 = (0 + 1)
7170oveq2i 6626 . . . . . . . . . . . . . 14 (2 · 1) = (2 · (0 + 1))
7271, 70oveq12i 6627 . . . . . . . . . . . . 13 ((2 · 1)C1) = ((2 · (0 + 1))C(0 + 1))
73 bcp1ctr 24938 . . . . . . . . . . . . . 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 11291 . . . . . . . . . . . . . . . 16 (2 · 0) ∈ ℕ0
76 bcn0 13053 . . . . . . . . . . . . . . . 16 ((2 · 0) ∈ ℕ0 → ((2 · 0)C0) = 1)
7775, 76ax-mp 5 . . . . . . . . . . . . . . 15 ((2 · 0)C0) = 1
78 2t0e0 11143 . . . . . . . . . . . . . . . . . . . . 21 (2 · 0) = 0
7978oveq1i 6625 . . . . . . . . . . . . . . . . . . . 20 ((2 · 0) + 1) = (0 + 1)
8079, 70eqtr4i 2646 . . . . . . . . . . . . . . . . . . 19 ((2 · 0) + 1) = 1
8170eqcomi 2630 . . . . . . . . . . . . . . . . . . 19 (0 + 1) = 1
8280, 81oveq12i 6627 . . . . . . . . . . . . . . . . . 18 (((2 · 0) + 1) / (0 + 1)) = (1 / 1)
83 1div1e1 10677 . . . . . . . . . . . . . . . . . 18 (1 / 1) = 1
8482, 83eqtri 2643 . . . . . . . . . . . . . . . . 17 (((2 · 0) + 1) / (0 + 1)) = 1
8584oveq2i 6626 . . . . . . . . . . . . . . . 16 (2 · (((2 · 0) + 1) / (0 + 1))) = (2 · 1)
86 2t1e2 11136 . . . . . . . . . . . . . . . 16 (2 · 1) = 2
8785, 86eqtri 2643 . . . . . . . . . . . . . . 15 (2 · (((2 · 0) + 1) / (0 + 1))) = 2
8877, 87oveq12i 6627 . . . . . . . . . . . . . 14 (((2 · 0)C0) · (2 · (((2 · 0) + 1) / (0 + 1)))) = (1 · 2)
8933mulid2i 10003 . . . . . . . . . . . . . 14 (1 · 2) = 2
9088, 89eqtri 2643 . . . . . . . . . . . . 13 (((2 · 0)C0) · (2 · (((2 · 0) + 1) / (0 + 1)))) = 2
9172, 74, 903eqtri 2647 . . . . . . . . . . . 12 ((2 · 1)C1) = 2
9286oveq1i 6625 . . . . . . . . . . . . . . . 16 ((2 · 1) + 1) = (2 + 1)
9392, 59eqtr4i 2646 . . . . . . . . . . . . . . 15 ((2 · 1) + 1) = 3
9464eqcomi 2630 . . . . . . . . . . . . . . 15 (1 + 1) = 2
9593, 94oveq12i 6627 . . . . . . . . . . . . . 14 (((2 · 1) + 1) / (1 + 1)) = (3 / 2)
9695oveq2i 6626 . . . . . . . . . . . . 13 (2 · (((2 · 1) + 1) / (1 + 1))) = (2 · (3 / 2))
97 2ne0 11073 . . . . . . . . . . . . . 14 2 ≠ 0
9843, 33, 97divcan2i 10728 . . . . . . . . . . . . 13 (2 · (3 / 2)) = 3
9996, 98eqtri 2643 . . . . . . . . . . . 12 (2 · (((2 · 1) + 1) / (1 + 1))) = 3
10091, 99oveq12i 6627 . . . . . . . . . . 11 (((2 · 1)C1) · (2 · (((2 · 1) + 1) / (1 + 1)))) = (2 · 3)
101100, 45eqtri 2643 . . . . . . . . . 10 (((2 · 1)C1) · (2 · (((2 · 1) + 1) / (1 + 1)))) = 6
10266, 69, 1013eqtri 2647 . . . . . . . . 9 ((2 · 2)C2) = 6
103 2t2e4 11137 . . . . . . . . . . . . . 14 (2 · 2) = 4
104103oveq1i 6625 . . . . . . . . . . . . 13 ((2 · 2) + 1) = (4 + 1)
105 df-5 11042 . . . . . . . . . . . . 13 5 = (4 + 1)
106104, 105eqtr4i 2646 . . . . . . . . . . . 12 ((2 · 2) + 1) = 5
10759eqcomi 2630 . . . . . . . . . . . 12 (2 + 1) = 3
108106, 107oveq12i 6627 . . . . . . . . . . 11 (((2 · 2) + 1) / (2 + 1)) = (5 / 3)
109108oveq2i 6626 . . . . . . . . . 10 (2 · (((2 · 2) + 1) / (2 + 1))) = (2 · (5 / 3))
110 5cn 11060 . . . . . . . . . . 11 5 ∈ ℂ
111 3ne0 11075 . . . . . . . . . . 11 3 ≠ 0
11233, 110, 43, 111divassi 10741 . . . . . . . . . 10 ((2 · 5) / 3) = (2 · (5 / 3))
113109, 112eqtr4i 2646 . . . . . . . . 9 (2 · (((2 · 2) + 1) / (2 + 1))) = ((2 · 5) / 3)
114102, 113oveq12i 6627 . . . . . . . 8 (((2 · 2)C2) · (2 · (((2 · 2) + 1) / (2 + 1)))) = (6 · ((2 · 5) / 3))
11563, 114eqtri 2643 . . . . . . 7 ((2 · (2 + 1))C(2 + 1)) = (6 · ((2 · 5) / 3))
116 6cn 11062 . . . . . . . . 9 6 ∈ ℂ
117 2nn 11145 . . . . . . . . . . 11 2 ∈ ℕ
118 5nn 11148 . . . . . . . . . . 11 5 ∈ ℕ
119117, 118nnmulcli 11004 . . . . . . . . . 10 (2 · 5) ∈ ℕ
120119nncni 10990 . . . . . . . . 9 (2 · 5) ∈ ℂ
12143, 111pm3.2i 471 . . . . . . . . 9 (3 ∈ ℂ ∧ 3 ≠ 0)
122 div12 10667 . . . . . . . . 9 ((6 ∈ ℂ ∧ (2 · 5) ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → (6 · ((2 · 5) / 3)) = ((2 · 5) · (6 / 3)))
123116, 120, 121, 122mp3an 1421 . . . . . . . 8 (6 · ((2 · 5) / 3)) = ((2 · 5) · (6 / 3))
124 5t2e10 11594 . . . . . . . . . 10 (5 · 2) = 10
125110, 33, 124mulcomli 10007 . . . . . . . . 9 (2 · 5) = 10
126116, 43, 33, 111divmuli 10739 . . . . . . . . . 10 ((6 / 3) = 2 ↔ (3 · 2) = 6)
12744, 126mpbir 221 . . . . . . . . 9 (6 / 3) = 2
128125, 127oveq12i 6627 . . . . . . . 8 ((2 · 5) · (6 / 3)) = (10 · 2)
129123, 128eqtri 2643 . . . . . . 7 (6 · ((2 · 5) / 3)) = (10 · 2)
13061, 115, 1293eqtri 2647 . . . . . 6 ((2 · 3)C3) = (10 · 2)
13145oveq1i 6625 . . . . . . . . 9 ((2 · 3) + 1) = (6 + 1)
132 df-7 11044 . . . . . . . . 9 7 = (6 + 1)
133131, 132eqtr4i 2646 . . . . . . . 8 ((2 · 3) + 1) = 7
134 3p1e4 11113 . . . . . . . 8 (3 + 1) = 4
135133, 134oveq12i 6627 . . . . . . 7 (((2 · 3) + 1) / (3 + 1)) = (7 / 4)
136135oveq2i 6626 . . . . . 6 (2 · (((2 · 3) + 1) / (3 + 1))) = (2 · (7 / 4))
137130, 136oveq12i 6627 . . . . 5 (((2 · 3)C3) · (2 · (((2 · 3) + 1) / (3 + 1)))) = ((10 · 2) · (2 · (7 / 4)))
13856, 58, 1373eqtri 2647 . . . 4 ((2 · 4)C4) = ((10 · 2) · (2 · (7 / 4)))
139 10nn 11474 . . . . . . 7 10 ∈ ℕ
140139nncni 10990 . . . . . 6 10 ∈ ℂ
141 7cn 11064 . . . . . . . 8 7 ∈ ℂ
142141, 49, 50divcli 10727 . . . . . . 7 (7 / 4) ∈ ℂ
14333, 142mulcli 10005 . . . . . 6 (2 · (7 / 4)) ∈ ℂ
144140, 33, 143mulassi 10009 . . . . 5 ((10 · 2) · (2 · (7 / 4))) = (10 · (2 · (2 · (7 / 4))))
145103oveq1i 6625 . . . . . . 7 ((2 · 2) · (7 / 4)) = (4 · (7 / 4))
14633, 33, 142mulassi 10009 . . . . . . 7 ((2 · 2) · (7 / 4)) = (2 · (2 · (7 / 4)))
147141, 49, 50divcan2i 10728 . . . . . . 7 (4 · (7 / 4)) = 7
148145, 146, 1473eqtr3i 2651 . . . . . 6 (2 · (2 · (7 / 4))) = 7
149148oveq2i 6626 . . . . 5 (10 · (2 · (2 · (7 / 4)))) = (10 · 7)
150144, 149eqtri 2643 . . . 4 ((10 · 2) · (2 · (7 / 4))) = (10 · 7)
15127dec0u 11480 . . . 4 (10 · 7) = 70
152138, 150, 1513eqtri 2647 . . 3 ((2 · 4)C4) = 70
15332, 53, 1523brtr4i 4653 . 2 ((4↑4) / 4) < ((2 · 4)C4)
154 4nn 11147 . . . 4 4 ∈ ℕ
155 eluznn 11718 . . . 4 ((4 ∈ ℕ ∧ 𝑛 ∈ (ℤ‘4)) → 𝑛 ∈ ℕ)
156154, 155mpan 705 . . 3 (𝑛 ∈ (ℤ‘4) → 𝑛 ∈ ℕ)
157 nnnn0 11259 . . . . . . . . . 10 (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
158 nnexpcl 12829 . . . . . . . . . 10 ((4 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → (4↑𝑛) ∈ ℕ)
159154, 157, 158sylancr 694 . . . . . . . . 9 (𝑛 ∈ ℕ → (4↑𝑛) ∈ ℕ)
160159nnrpd 11830 . . . . . . . 8 (𝑛 ∈ ℕ → (4↑𝑛) ∈ ℝ+)
161 nnrp 11802 . . . . . . . 8 (𝑛 ∈ ℕ → 𝑛 ∈ ℝ+)
162160, 161rpdivcld 11849 . . . . . . 7 (𝑛 ∈ ℕ → ((4↑𝑛) / 𝑛) ∈ ℝ+)
163162rpred 11832 . . . . . 6 (𝑛 ∈ ℕ → ((4↑𝑛) / 𝑛) ∈ ℝ)
164 nnmulcl 11003 . . . . . . . . . 10 ((2 ∈ ℕ ∧ 𝑛 ∈ ℕ) → (2 · 𝑛) ∈ ℕ)
165117, 164mpan 705 . . . . . . . . 9 (𝑛 ∈ ℕ → (2 · 𝑛) ∈ ℕ)
166165nnnn0d 11311 . . . . . . . 8 (𝑛 ∈ ℕ → (2 · 𝑛) ∈ ℕ0)
167 nnz 11359 . . . . . . . 8 (𝑛 ∈ ℕ → 𝑛 ∈ ℤ)
168 bccl 13065 . . . . . . . 8 (((2 · 𝑛) ∈ ℕ0𝑛 ∈ ℤ) → ((2 · 𝑛)C𝑛) ∈ ℕ0)
169166, 167, 168syl2anc 692 . . . . . . 7 (𝑛 ∈ ℕ → ((2 · 𝑛)C𝑛) ∈ ℕ0)
170169nn0red 11312 . . . . . 6 (𝑛 ∈ ℕ → ((2 · 𝑛)C𝑛) ∈ ℝ)
171 2rp 11797 . . . . . . 7 2 ∈ ℝ+
172165peano2nnd 10997 . . . . . . . . 9 (𝑛 ∈ ℕ → ((2 · 𝑛) + 1) ∈ ℕ)
173172nnrpd 11830 . . . . . . . 8 (𝑛 ∈ ℕ → ((2 · 𝑛) + 1) ∈ ℝ+)
174 peano2nn 10992 . . . . . . . . 9 (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℕ)
175174nnrpd 11830 . . . . . . . 8 (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℝ+)
176173, 175rpdivcld 11849 . . . . . . 7 (𝑛 ∈ ℕ → (((2 · 𝑛) + 1) / (𝑛 + 1)) ∈ ℝ+)
177 rpmulcl 11815 . . . . . . 7 ((2 ∈ ℝ+ ∧ (((2 · 𝑛) + 1) / (𝑛 + 1)) ∈ ℝ+) → (2 · (((2 · 𝑛) + 1) / (𝑛 + 1))) ∈ ℝ+)
178171, 176, 177sylancr 694 . . . . . 6 (𝑛 ∈ ℕ → (2 · (((2 · 𝑛) + 1) / (𝑛 + 1))) ∈ ℝ+)
179163, 170, 178ltmul1d 11873 . . . . 5 (𝑛 ∈ ℕ → (((4↑𝑛) / 𝑛) < ((2 · 𝑛)C𝑛) ↔ (((4↑𝑛) / 𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))) < (((2 · 𝑛)C𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1))))))
180 bcp1ctr 24938 . . . . . . 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 4635 . . . . 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 11050 . . . . . . . 8 2 ∈ ℝ
185184a1i 11 . . . . . . 7 (𝑛 ∈ ℕ → 2 ∈ ℝ)
186173, 161rpdivcld 11849 . . . . . . . 8 (𝑛 ∈ ℕ → (((2 · 𝑛) + 1) / 𝑛) ∈ ℝ+)
187186rpred 11832 . . . . . . 7 (𝑛 ∈ ℕ → (((2 · 𝑛) + 1) / 𝑛) ∈ ℝ)
188 nnmulcl 11003 . . . . . . . . . 10 (((4↑𝑛) ∈ ℕ ∧ 2 ∈ ℕ) → ((4↑𝑛) · 2) ∈ ℕ)
189159, 117, 188sylancl 693 . . . . . . . . 9 (𝑛 ∈ ℕ → ((4↑𝑛) · 2) ∈ ℕ)
190189nnrpd 11830 . . . . . . . 8 (𝑛 ∈ ℕ → ((4↑𝑛) · 2) ∈ ℝ+)
191190, 175rpdivcld 11849 . . . . . . 7 (𝑛 ∈ ℕ → (((4↑𝑛) · 2) / (𝑛 + 1)) ∈ ℝ+)
192161rpreccld 11842 . . . . . . . . 9 (𝑛 ∈ ℕ → (1 / 𝑛) ∈ ℝ+)
193 ltaddrp 11827 . . . . . . . . 9 ((2 ∈ ℝ ∧ (1 / 𝑛) ∈ ℝ+) → 2 < (2 + (1 / 𝑛)))
194184, 192, 193sylancr 694 . . . . . . . 8 (𝑛 ∈ ℕ → 2 < (2 + (1 / 𝑛)))
195165nncnd 10996 . . . . . . . . . 10 (𝑛 ∈ ℕ → (2 · 𝑛) ∈ ℂ)
196 1cnd 10016 . . . . . . . . . 10 (𝑛 ∈ ℕ → 1 ∈ ℂ)
197 nncn 10988 . . . . . . . . . 10 (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
198 nnne0 11013 . . . . . . . . . 10 (𝑛 ∈ ℕ → 𝑛 ≠ 0)
199195, 196, 197, 198divdird 10799 . . . . . . . . 9 (𝑛 ∈ ℕ → (((2 · 𝑛) + 1) / 𝑛) = (((2 · 𝑛) / 𝑛) + (1 / 𝑛)))
20033a1i 11 . . . . . . . . . . 11 (𝑛 ∈ ℕ → 2 ∈ ℂ)
201200, 197, 198divcan4d 10767 . . . . . . . . . 10 (𝑛 ∈ ℕ → ((2 · 𝑛) / 𝑛) = 2)
202201oveq1d 6630 . . . . . . . . 9 (𝑛 ∈ ℕ → (((2 · 𝑛) / 𝑛) + (1 / 𝑛)) = (2 + (1 / 𝑛)))
203199, 202eqtr2d 2656 . . . . . . . 8 (𝑛 ∈ ℕ → (2 + (1 / 𝑛)) = (((2 · 𝑛) + 1) / 𝑛))
204194, 203breqtrd 4649 . . . . . . 7 (𝑛 ∈ ℕ → 2 < (((2 · 𝑛) + 1) / 𝑛))
205185, 187, 191, 204ltmul2dd 11888 . . . . . 6 (𝑛 ∈ ℕ → ((((4↑𝑛) · 2) / (𝑛 + 1)) · 2) < ((((4↑𝑛) · 2) / (𝑛 + 1)) · (((2 · 𝑛) + 1) / 𝑛)))
206 expp1 12823 . . . . . . . . . 10 ((4 ∈ ℂ ∧ 𝑛 ∈ ℕ0) → (4↑(𝑛 + 1)) = ((4↑𝑛) · 4))
20749, 157, 206sylancr 694 . . . . . . . . 9 (𝑛 ∈ ℕ → (4↑(𝑛 + 1)) = ((4↑𝑛) · 4))
208159nncnd 10996 . . . . . . . . . . 11 (𝑛 ∈ ℕ → (4↑𝑛) ∈ ℂ)
209208, 200, 200mulassd 10023 . . . . . . . . . 10 (𝑛 ∈ ℕ → (((4↑𝑛) · 2) · 2) = ((4↑𝑛) · (2 · 2)))
210103oveq2i 6626 . . . . . . . . . 10 ((4↑𝑛) · (2 · 2)) = ((4↑𝑛) · 4)
211209, 210syl6eq 2671 . . . . . . . . 9 (𝑛 ∈ ℕ → (((4↑𝑛) · 2) · 2) = ((4↑𝑛) · 4))
212207, 211eqtr4d 2658 . . . . . . . 8 (𝑛 ∈ ℕ → (4↑(𝑛 + 1)) = (((4↑𝑛) · 2) · 2))
213212oveq1d 6630 . . . . . . 7 (𝑛 ∈ ℕ → ((4↑(𝑛 + 1)) / (𝑛 + 1)) = ((((4↑𝑛) · 2) · 2) / (𝑛 + 1)))
214189nncnd 10996 . . . . . . . 8 (𝑛 ∈ ℕ → ((4↑𝑛) · 2) ∈ ℂ)
215174nncnd 10996 . . . . . . . 8 (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℂ)
216174nnne0d 11025 . . . . . . . 8 (𝑛 ∈ ℕ → (𝑛 + 1) ≠ 0)
217214, 200, 215, 216div23d 10798 . . . . . . 7 (𝑛 ∈ ℕ → ((((4↑𝑛) · 2) · 2) / (𝑛 + 1)) = ((((4↑𝑛) · 2) / (𝑛 + 1)) · 2))
218213, 217eqtrd 2655 . . . . . 6 (𝑛 ∈ ℕ → ((4↑(𝑛 + 1)) / (𝑛 + 1)) = ((((4↑𝑛) · 2) / (𝑛 + 1)) · 2))
219208, 200, 197, 198div23d 10798 . . . . . . . 8 (𝑛 ∈ ℕ → (((4↑𝑛) · 2) / 𝑛) = (((4↑𝑛) / 𝑛) · 2))
220219oveq1d 6630 . . . . . . 7 (𝑛 ∈ ℕ → ((((4↑𝑛) · 2) / 𝑛) · (((2 · 𝑛) + 1) / (𝑛 + 1))) = ((((4↑𝑛) / 𝑛) · 2) · (((2 · 𝑛) + 1) / (𝑛 + 1))))
221172nncnd 10996 . . . . . . . 8 (𝑛 ∈ ℕ → ((2 · 𝑛) + 1) ∈ ℂ)
222214, 197, 221, 215, 198, 216divmul24d 10804 . . . . . . 7 (𝑛 ∈ ℕ → ((((4↑𝑛) · 2) / 𝑛) · (((2 · 𝑛) + 1) / (𝑛 + 1))) = ((((4↑𝑛) · 2) / (𝑛 + 1)) · (((2 · 𝑛) + 1) / 𝑛)))
223162rpcnd 11834 . . . . . . . 8 (𝑛 ∈ ℕ → ((4↑𝑛) / 𝑛) ∈ ℂ)
224176rpcnd 11834 . . . . . . . 8 (𝑛 ∈ ℕ → (((2 · 𝑛) + 1) / (𝑛 + 1)) ∈ ℂ)
225223, 200, 224mulassd 10023 . . . . . . 7 (𝑛 ∈ ℕ → ((((4↑𝑛) / 𝑛) · 2) · (((2 · 𝑛) + 1) / (𝑛 + 1))) = (((4↑𝑛) / 𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))))
226220, 222, 2253eqtr3rd 2664 . . . . . 6 (𝑛 ∈ ℕ → (((4↑𝑛) / 𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))) = ((((4↑𝑛) · 2) / (𝑛 + 1)) · (((2 · 𝑛) + 1) / 𝑛)))
227205, 218, 2263brtr4d 4655 . . . . 5 (𝑛 ∈ ℕ → ((4↑(𝑛 + 1)) / (𝑛 + 1)) < (((4↑𝑛) / 𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))))
228174nnnn0d 11311 . . . . . . . . . 10 (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℕ0)
229 nnexpcl 12829 . . . . . . . . . 10 ((4 ∈ ℕ ∧ (𝑛 + 1) ∈ ℕ0) → (4↑(𝑛 + 1)) ∈ ℕ)
230154, 228, 229sylancr 694 . . . . . . . . 9 (𝑛 ∈ ℕ → (4↑(𝑛 + 1)) ∈ ℕ)
231230nnrpd 11830 . . . . . . . 8 (𝑛 ∈ ℕ → (4↑(𝑛 + 1)) ∈ ℝ+)
232231, 175rpdivcld 11849 . . . . . . 7 (𝑛 ∈ ℕ → ((4↑(𝑛 + 1)) / (𝑛 + 1)) ∈ ℝ+)
233232rpred 11832 . . . . . 6 (𝑛 ∈ ℕ → ((4↑(𝑛 + 1)) / (𝑛 + 1)) ∈ ℝ)
234178rpred 11832 . . . . . . 7 (𝑛 ∈ ℕ → (2 · (((2 · 𝑛) + 1) / (𝑛 + 1))) ∈ ℝ)
235163, 234remulcld 10030 . . . . . 6 (𝑛 ∈ ℕ → (((4↑𝑛) / 𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))) ∈ ℝ)
236 nn0mulcl 11289 . . . . . . . . 9 ((2 ∈ ℕ0 ∧ (𝑛 + 1) ∈ ℕ0) → (2 · (𝑛 + 1)) ∈ ℕ0)
23734, 228, 236sylancr 694 . . . . . . . 8 (𝑛 ∈ ℕ → (2 · (𝑛 + 1)) ∈ ℕ0)
238174nnzd 11441 . . . . . . . 8 (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℤ)
239 bccl 13065 . . . . . . . 8 (((2 · (𝑛 + 1)) ∈ ℕ0 ∧ (𝑛 + 1) ∈ ℤ) → ((2 · (𝑛 + 1))C(𝑛 + 1)) ∈ ℕ0)
240237, 238, 239syl2anc 692 . . . . . . 7 (𝑛 ∈ ℕ → ((2 · (𝑛 + 1))C(𝑛 + 1)) ∈ ℕ0)
241240nn0red 11312 . . . . . 6 (𝑛 ∈ ℕ → ((2 · (𝑛 + 1))C(𝑛 + 1)) ∈ ℝ)
242 lttr 10074 . . . . . 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 1323 . . . . 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 710 . . . 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 11710 1 (𝑁 ∈ (ℤ‘4) → ((4↑𝑁) / 𝑁) < ((2 · 𝑁)C𝑁))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1480  wcel 1987  wne 2790   class class class wbr 4623  cfv 5857  (class class class)co 6615  cc 9894  cr 9895  0cc0 9896  1c1 9897   + caddc 9899   · cmul 9901   < clt 10034  cmin 10226   / cdiv 10644  cn 10980  2c2 11030  3c3 11031  4c4 11032  5c5 11033  6c6 11034  7c7 11035  0cn0 11252  cz 11337  cdc 11453  cuz 11647  +crp 11792  cexp 12816  Ccbc 13045
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4751  ax-nul 4759  ax-pow 4813  ax-pr 4877  ax-un 6914  ax-cnex 9952  ax-resscn 9953  ax-1cn 9954  ax-icn 9955  ax-addcl 9956  ax-addrcl 9957  ax-mulcl 9958  ax-mulrcl 9959  ax-mulcom 9960  ax-addass 9961  ax-mulass 9962  ax-distr 9963  ax-i2m1 9964  ax-1ne0 9965  ax-1rid 9966  ax-rnegex 9967  ax-rrecex 9968  ax-cnre 9969  ax-pre-lttri 9970  ax-pre-lttrn 9971  ax-pre-ltadd 9972  ax-pre-mulgt0 9973
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2913  df-rex 2914  df-reu 2915  df-rmo 2916  df-rab 2917  df-v 3192  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3898  df-if 4065  df-pw 4138  df-sn 4156  df-pr 4158  df-tp 4160  df-op 4162  df-uni 4410  df-iun 4494  df-br 4624  df-opab 4684  df-mpt 4685  df-tr 4723  df-eprel 4995  df-id 4999  df-po 5005  df-so 5006  df-fr 5043  df-we 5045  df-xp 5090  df-rel 5091  df-cnv 5092  df-co 5093  df-dm 5094  df-rn 5095  df-res 5096  df-ima 5097  df-pred 5649  df-ord 5695  df-on 5696  df-lim 5697  df-suc 5698  df-iota 5820  df-fun 5859  df-fn 5860  df-f 5861  df-f1 5862  df-fo 5863  df-f1o 5864  df-fv 5865  df-riota 6576  df-ov 6618  df-oprab 6619  df-mpt2 6620  df-om 7028  df-1st 7128  df-2nd 7129  df-wrecs 7367  df-recs 7428  df-rdg 7466  df-er 7702  df-en 7916  df-dom 7917  df-sdom 7918  df-pnf 10036  df-mnf 10037  df-xr 10038  df-ltxr 10039  df-le 10040  df-sub 10228  df-neg 10229  df-div 10645  df-nn 10981  df-2 11039  df-3 11040  df-4 11041  df-5 11042  df-6 11043  df-7 11044  df-8 11045  df-9 11046  df-n0 11253  df-z 11338  df-dec 11454  df-uz 11648  df-rp 11793  df-fz 12285  df-seq 12758  df-exp 12817  df-fac 13017  df-bc 13046
This theorem is referenced by:  bposlem6  24948  chebbnd1lem1  25092
  Copyright terms: Public domain W3C validator