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

Theorem bclbnd 24805
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 11288 . 2 4 ∈ ℤ
2 oveq2 6557 . . . 4 (𝑥 = 4 → (4↑𝑥) = (4↑4))
3 id 22 . . . 4 (𝑥 = 4 → 𝑥 = 4)
42, 3oveq12d 6567 . . 3 (𝑥 = 4 → ((4↑𝑥) / 𝑥) = ((4↑4) / 4))
5 oveq2 6557 . . . 4 (𝑥 = 4 → (2 · 𝑥) = (2 · 4))
65, 3oveq12d 6567 . . 3 (𝑥 = 4 → ((2 · 𝑥)C𝑥) = ((2 · 4)C4))
74, 6breq12d 4596 . 2 (𝑥 = 4 → (((4↑𝑥) / 𝑥) < ((2 · 𝑥)C𝑥) ↔ ((4↑4) / 4) < ((2 · 4)C4)))
8 oveq2 6557 . . . 4 (𝑥 = 𝑛 → (4↑𝑥) = (4↑𝑛))
9 id 22 . . . 4 (𝑥 = 𝑛𝑥 = 𝑛)
108, 9oveq12d 6567 . . 3 (𝑥 = 𝑛 → ((4↑𝑥) / 𝑥) = ((4↑𝑛) / 𝑛))
11 oveq2 6557 . . . 4 (𝑥 = 𝑛 → (2 · 𝑥) = (2 · 𝑛))
1211, 9oveq12d 6567 . . 3 (𝑥 = 𝑛 → ((2 · 𝑥)C𝑥) = ((2 · 𝑛)C𝑛))
1310, 12breq12d 4596 . 2 (𝑥 = 𝑛 → (((4↑𝑥) / 𝑥) < ((2 · 𝑥)C𝑥) ↔ ((4↑𝑛) / 𝑛) < ((2 · 𝑛)C𝑛)))
14 oveq2 6557 . . . 4 (𝑥 = (𝑛 + 1) → (4↑𝑥) = (4↑(𝑛 + 1)))
15 id 22 . . . 4 (𝑥 = (𝑛 + 1) → 𝑥 = (𝑛 + 1))
1614, 15oveq12d 6567 . . 3 (𝑥 = (𝑛 + 1) → ((4↑𝑥) / 𝑥) = ((4↑(𝑛 + 1)) / (𝑛 + 1)))
17 oveq2 6557 . . . 4 (𝑥 = (𝑛 + 1) → (2 · 𝑥) = (2 · (𝑛 + 1)))
1817, 15oveq12d 6567 . . 3 (𝑥 = (𝑛 + 1) → ((2 · 𝑥)C𝑥) = ((2 · (𝑛 + 1))C(𝑛 + 1)))
1916, 18breq12d 4596 . 2 (𝑥 = (𝑛 + 1) → (((4↑𝑥) / 𝑥) < ((2 · 𝑥)C𝑥) ↔ ((4↑(𝑛 + 1)) / (𝑛 + 1)) < ((2 · (𝑛 + 1))C(𝑛 + 1))))
20 oveq2 6557 . . . 4 (𝑥 = 𝑁 → (4↑𝑥) = (4↑𝑁))
21 id 22 . . . 4 (𝑥 = 𝑁𝑥 = 𝑁)
2220, 21oveq12d 6567 . . 3 (𝑥 = 𝑁 → ((4↑𝑥) / 𝑥) = ((4↑𝑁) / 𝑁))
23 oveq2 6557 . . . 4 (𝑥 = 𝑁 → (2 · 𝑥) = (2 · 𝑁))
2423, 21oveq12d 6567 . . 3 (𝑥 = 𝑁 → ((2 · 𝑥)C𝑥) = ((2 · 𝑁)C𝑁))
2522, 24breq12d 4596 . 2 (𝑥 = 𝑁 → (((4↑𝑥) / 𝑥) < ((2 · 𝑥)C𝑥) ↔ ((4↑𝑁) / 𝑁) < ((2 · 𝑁)C𝑁)))
26 6nn0 11190 . . . 4 6 ∈ ℕ0
27 7nn0 11191 . . . 4 7 ∈ ℕ0
28 4nn0 11188 . . . 4 4 ∈ ℕ0
29 0nn0 11184 . . . 4 0 ∈ ℕ0
30 4lt10 11554 . . . 4 4 < 10
31 6lt7 11086 . . . 4 6 < 7
3226, 27, 28, 29, 30, 31decltc 11408 . . 3 64 < 70
33 2cn 10968 . . . . . 6 2 ∈ ℂ
34 2nn0 11186 . . . . . 6 2 ∈ ℕ0
35 3nn0 11187 . . . . . 6 3 ∈ ℕ0
36 expmul 12767 . . . . . 6 ((2 ∈ ℂ ∧ 2 ∈ ℕ0 ∧ 3 ∈ ℕ0) → (2↑(2 · 3)) = ((2↑2)↑3))
3733, 34, 35, 36mp3an 1416 . . . . 5 (2↑(2 · 3)) = ((2↑2)↑3)
38 sq2 12822 . . . . . . 7 (2↑2) = 4
3938eqcomi 2619 . . . . . 6 4 = (2↑2)
40 4m1e3 11015 . . . . . 6 (4 − 1) = 3
4139, 40oveq12i 6561 . . . . 5 (4↑(4 − 1)) = ((2↑2)↑3)
4237, 41eqtr4i 2635 . . . 4 (2↑(2 · 3)) = (4↑(4 − 1))
43 3cn 10972 . . . . . . 7 3 ∈ ℂ
44 3t2e6 11056 . . . . . . 7 (3 · 2) = 6
4543, 33, 44mulcomli 9926 . . . . . 6 (2 · 3) = 6
4645oveq2i 6560 . . . . 5 (2↑(2 · 3)) = (2↑6)
47 2exp6 15633 . . . . 5 (2↑6) = 64
4846, 47eqtri 2632 . . . 4 (2↑(2 · 3)) = 64
49 4cn 10975 . . . . 5 4 ∈ ℂ
50 4ne0 10994 . . . . 5 4 ≠ 0
51 expm1 12772 . . . . 5 ((4 ∈ ℂ ∧ 4 ≠ 0 ∧ 4 ∈ ℤ) → (4↑(4 − 1)) = ((4↑4) / 4))
5249, 50, 1, 51mp3an 1416 . . . 4 (4↑(4 − 1)) = ((4↑4) / 4)
5342, 48, 523eqtr3ri 2641 . . 3 ((4↑4) / 4) = 64
54 df-4 10958 . . . . . . 7 4 = (3 + 1)
5554oveq2i 6560 . . . . . 6 (2 · 4) = (2 · (3 + 1))
5655, 54oveq12i 6561 . . . . 5 ((2 · 4)C4) = ((2 · (3 + 1))C(3 + 1))
57 bcp1ctr 24804 . . . . . 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 10957 . . . . . . . . 9 3 = (2 + 1)
6059oveq2i 6560 . . . . . . . 8 (2 · 3) = (2 · (2 + 1))
6160, 59oveq12i 6561 . . . . . . 7 ((2 · 3)C3) = ((2 · (2 + 1))C(2 + 1))
62 bcp1ctr 24804 . . . . . . . . 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 10956 . . . . . . . . . . . 12 2 = (1 + 1)
6564oveq2i 6560 . . . . . . . . . . 11 (2 · 2) = (2 · (1 + 1))
6665, 64oveq12i 6561 . . . . . . . . . 10 ((2 · 2)C2) = ((2 · (1 + 1))C(1 + 1))
67 1nn0 11185 . . . . . . . . . . 11 1 ∈ ℕ0
68 bcp1ctr 24804 . . . . . . . . . . 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 11428 . . . . . . . . . . . . . . 15 1 = (0 + 1)
7170oveq2i 6560 . . . . . . . . . . . . . 14 (2 · 1) = (2 · (0 + 1))
7271, 70oveq12i 6561 . . . . . . . . . . . . 13 ((2 · 1)C1) = ((2 · (0 + 1))C(0 + 1))
73 bcp1ctr 24804 . . . . . . . . . . . . . 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 11208 . . . . . . . . . . . . . . . 16 (2 · 0) ∈ ℕ0
76 bcn0 12959 . . . . . . . . . . . . . . . 16 ((2 · 0) ∈ ℕ0 → ((2 · 0)C0) = 1)
7775, 76ax-mp 5 . . . . . . . . . . . . . . 15 ((2 · 0)C0) = 1
78 2t0e0 11060 . . . . . . . . . . . . . . . . . . . . 21 (2 · 0) = 0
7978oveq1i 6559 . . . . . . . . . . . . . . . . . . . 20 ((2 · 0) + 1) = (0 + 1)
8079, 70eqtr4i 2635 . . . . . . . . . . . . . . . . . . 19 ((2 · 0) + 1) = 1
8170eqcomi 2619 . . . . . . . . . . . . . . . . . . 19 (0 + 1) = 1
8280, 81oveq12i 6561 . . . . . . . . . . . . . . . . . 18 (((2 · 0) + 1) / (0 + 1)) = (1 / 1)
83 1div1e1 10596 . . . . . . . . . . . . . . . . . 18 (1 / 1) = 1
8482, 83eqtri 2632 . . . . . . . . . . . . . . . . 17 (((2 · 0) + 1) / (0 + 1)) = 1
8584oveq2i 6560 . . . . . . . . . . . . . . . 16 (2 · (((2 · 0) + 1) / (0 + 1))) = (2 · 1)
86 2t1e2 11053 . . . . . . . . . . . . . . . 16 (2 · 1) = 2
8785, 86eqtri 2632 . . . . . . . . . . . . . . 15 (2 · (((2 · 0) + 1) / (0 + 1))) = 2
8877, 87oveq12i 6561 . . . . . . . . . . . . . 14 (((2 · 0)C0) · (2 · (((2 · 0) + 1) / (0 + 1)))) = (1 · 2)
8933mulid2i 9922 . . . . . . . . . . . . . 14 (1 · 2) = 2
9088, 89eqtri 2632 . . . . . . . . . . . . 13 (((2 · 0)C0) · (2 · (((2 · 0) + 1) / (0 + 1)))) = 2
9172, 74, 903eqtri 2636 . . . . . . . . . . . 12 ((2 · 1)C1) = 2
9286oveq1i 6559 . . . . . . . . . . . . . . . 16 ((2 · 1) + 1) = (2 + 1)
9392, 59eqtr4i 2635 . . . . . . . . . . . . . . 15 ((2 · 1) + 1) = 3
9464eqcomi 2619 . . . . . . . . . . . . . . 15 (1 + 1) = 2
9593, 94oveq12i 6561 . . . . . . . . . . . . . 14 (((2 · 1) + 1) / (1 + 1)) = (3 / 2)
9695oveq2i 6560 . . . . . . . . . . . . 13 (2 · (((2 · 1) + 1) / (1 + 1))) = (2 · (3 / 2))
97 2ne0 10990 . . . . . . . . . . . . . 14 2 ≠ 0
9843, 33, 97divcan2i 10647 . . . . . . . . . . . . 13 (2 · (3 / 2)) = 3
9996, 98eqtri 2632 . . . . . . . . . . . 12 (2 · (((2 · 1) + 1) / (1 + 1))) = 3
10091, 99oveq12i 6561 . . . . . . . . . . 11 (((2 · 1)C1) · (2 · (((2 · 1) + 1) / (1 + 1)))) = (2 · 3)
101100, 45eqtri 2632 . . . . . . . . . 10 (((2 · 1)C1) · (2 · (((2 · 1) + 1) / (1 + 1)))) = 6
10266, 69, 1013eqtri 2636 . . . . . . . . 9 ((2 · 2)C2) = 6
103 2t2e4 11054 . . . . . . . . . . . . . 14 (2 · 2) = 4
104103oveq1i 6559 . . . . . . . . . . . . 13 ((2 · 2) + 1) = (4 + 1)
105 df-5 10959 . . . . . . . . . . . . 13 5 = (4 + 1)
106104, 105eqtr4i 2635 . . . . . . . . . . . 12 ((2 · 2) + 1) = 5
10759eqcomi 2619 . . . . . . . . . . . 12 (2 + 1) = 3
108106, 107oveq12i 6561 . . . . . . . . . . 11 (((2 · 2) + 1) / (2 + 1)) = (5 / 3)
109108oveq2i 6560 . . . . . . . . . 10 (2 · (((2 · 2) + 1) / (2 + 1))) = (2 · (5 / 3))
110 5cn 10977 . . . . . . . . . . 11 5 ∈ ℂ
111 3ne0 10992 . . . . . . . . . . 11 3 ≠ 0
11233, 110, 43, 111divassi 10660 . . . . . . . . . 10 ((2 · 5) / 3) = (2 · (5 / 3))
113109, 112eqtr4i 2635 . . . . . . . . 9 (2 · (((2 · 2) + 1) / (2 + 1))) = ((2 · 5) / 3)
114102, 113oveq12i 6561 . . . . . . . 8 (((2 · 2)C2) · (2 · (((2 · 2) + 1) / (2 + 1)))) = (6 · ((2 · 5) / 3))
11563, 114eqtri 2632 . . . . . . 7 ((2 · (2 + 1))C(2 + 1)) = (6 · ((2 · 5) / 3))
116 6cn 10979 . . . . . . . . 9 6 ∈ ℂ
117 2nn 11062 . . . . . . . . . . 11 2 ∈ ℕ
118 5nn 11065 . . . . . . . . . . 11 5 ∈ ℕ
119117, 118nnmulcli 10921 . . . . . . . . . 10 (2 · 5) ∈ ℕ
120119nncni 10907 . . . . . . . . 9 (2 · 5) ∈ ℂ
12143, 111pm3.2i 470 . . . . . . . . 9 (3 ∈ ℂ ∧ 3 ≠ 0)
122 div12 10586 . . . . . . . . 9 ((6 ∈ ℂ ∧ (2 · 5) ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → (6 · ((2 · 5) / 3)) = ((2 · 5) · (6 / 3)))
123116, 120, 121, 122mp3an 1416 . . . . . . . 8 (6 · ((2 · 5) / 3)) = ((2 · 5) · (6 / 3))
124 5t2e10 11510 . . . . . . . . . 10 (5 · 2) = 10
125110, 33, 124mulcomli 9926 . . . . . . . . 9 (2 · 5) = 10
126116, 43, 33, 111divmuli 10658 . . . . . . . . . 10 ((6 / 3) = 2 ↔ (3 · 2) = 6)
12744, 126mpbir 220 . . . . . . . . 9 (6 / 3) = 2
128125, 127oveq12i 6561 . . . . . . . 8 ((2 · 5) · (6 / 3)) = (10 · 2)
129123, 128eqtri 2632 . . . . . . 7 (6 · ((2 · 5) / 3)) = (10 · 2)
13061, 115, 1293eqtri 2636 . . . . . 6 ((2 · 3)C3) = (10 · 2)
13145oveq1i 6559 . . . . . . . . 9 ((2 · 3) + 1) = (6 + 1)
132 df-7 10961 . . . . . . . . 9 7 = (6 + 1)
133131, 132eqtr4i 2635 . . . . . . . 8 ((2 · 3) + 1) = 7
134 3p1e4 11030 . . . . . . . 8 (3 + 1) = 4
135133, 134oveq12i 6561 . . . . . . 7 (((2 · 3) + 1) / (3 + 1)) = (7 / 4)
136135oveq2i 6560 . . . . . 6 (2 · (((2 · 3) + 1) / (3 + 1))) = (2 · (7 / 4))
137130, 136oveq12i 6561 . . . . 5 (((2 · 3)C3) · (2 · (((2 · 3) + 1) / (3 + 1)))) = ((10 · 2) · (2 · (7 / 4)))
13856, 58, 1373eqtri 2636 . . . 4 ((2 · 4)C4) = ((10 · 2) · (2 · (7 / 4)))
139 10nn 11390 . . . . . . 7 10 ∈ ℕ
140139nncni 10907 . . . . . 6 10 ∈ ℂ
141 7cn 10981 . . . . . . . 8 7 ∈ ℂ
142141, 49, 50divcli 10646 . . . . . . 7 (7 / 4) ∈ ℂ
14333, 142mulcli 9924 . . . . . 6 (2 · (7 / 4)) ∈ ℂ
144140, 33, 143mulassi 9928 . . . . 5 ((10 · 2) · (2 · (7 / 4))) = (10 · (2 · (2 · (7 / 4))))
145103oveq1i 6559 . . . . . . 7 ((2 · 2) · (7 / 4)) = (4 · (7 / 4))
14633, 33, 142mulassi 9928 . . . . . . 7 ((2 · 2) · (7 / 4)) = (2 · (2 · (7 / 4)))
147141, 49, 50divcan2i 10647 . . . . . . 7 (4 · (7 / 4)) = 7
148145, 146, 1473eqtr3i 2640 . . . . . 6 (2 · (2 · (7 / 4))) = 7
149148oveq2i 6560 . . . . 5 (10 · (2 · (2 · (7 / 4)))) = (10 · 7)
150144, 149eqtri 2632 . . . 4 ((10 · 2) · (2 · (7 / 4))) = (10 · 7)
15127dec0u 11396 . . . 4 (10 · 7) = 70
152138, 150, 1513eqtri 2636 . . 3 ((2 · 4)C4) = 70
15332, 53, 1523brtr4i 4613 . 2 ((4↑4) / 4) < ((2 · 4)C4)
154 4nn 11064 . . . 4 4 ∈ ℕ
155 eluznn 11634 . . . 4 ((4 ∈ ℕ ∧ 𝑛 ∈ (ℤ‘4)) → 𝑛 ∈ ℕ)
156154, 155mpan 702 . . 3 (𝑛 ∈ (ℤ‘4) → 𝑛 ∈ ℕ)
157 nnnn0 11176 . . . . . . . . . 10 (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
158 nnexpcl 12735 . . . . . . . . . 10 ((4 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → (4↑𝑛) ∈ ℕ)
159154, 157, 158sylancr 694 . . . . . . . . 9 (𝑛 ∈ ℕ → (4↑𝑛) ∈ ℕ)
160159nnrpd 11746 . . . . . . . 8 (𝑛 ∈ ℕ → (4↑𝑛) ∈ ℝ+)
161 nnrp 11718 . . . . . . . 8 (𝑛 ∈ ℕ → 𝑛 ∈ ℝ+)
162160, 161rpdivcld 11765 . . . . . . 7 (𝑛 ∈ ℕ → ((4↑𝑛) / 𝑛) ∈ ℝ+)
163162rpred 11748 . . . . . 6 (𝑛 ∈ ℕ → ((4↑𝑛) / 𝑛) ∈ ℝ)
164 nnmulcl 10920 . . . . . . . . . 10 ((2 ∈ ℕ ∧ 𝑛 ∈ ℕ) → (2 · 𝑛) ∈ ℕ)
165117, 164mpan 702 . . . . . . . . 9 (𝑛 ∈ ℕ → (2 · 𝑛) ∈ ℕ)
166165nnnn0d 11228 . . . . . . . 8 (𝑛 ∈ ℕ → (2 · 𝑛) ∈ ℕ0)
167 nnz 11276 . . . . . . . 8 (𝑛 ∈ ℕ → 𝑛 ∈ ℤ)
168 bccl 12971 . . . . . . . 8 (((2 · 𝑛) ∈ ℕ0𝑛 ∈ ℤ) → ((2 · 𝑛)C𝑛) ∈ ℕ0)
169166, 167, 168syl2anc 691 . . . . . . 7 (𝑛 ∈ ℕ → ((2 · 𝑛)C𝑛) ∈ ℕ0)
170169nn0red 11229 . . . . . 6 (𝑛 ∈ ℕ → ((2 · 𝑛)C𝑛) ∈ ℝ)
171 2rp 11713 . . . . . . 7 2 ∈ ℝ+
172165peano2nnd 10914 . . . . . . . . 9 (𝑛 ∈ ℕ → ((2 · 𝑛) + 1) ∈ ℕ)
173172nnrpd 11746 . . . . . . . 8 (𝑛 ∈ ℕ → ((2 · 𝑛) + 1) ∈ ℝ+)
174 peano2nn 10909 . . . . . . . . 9 (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℕ)
175174nnrpd 11746 . . . . . . . 8 (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℝ+)
176173, 175rpdivcld 11765 . . . . . . 7 (𝑛 ∈ ℕ → (((2 · 𝑛) + 1) / (𝑛 + 1)) ∈ ℝ+)
177 rpmulcl 11731 . . . . . . 7 ((2 ∈ ℝ+ ∧ (((2 · 𝑛) + 1) / (𝑛 + 1)) ∈ ℝ+) → (2 · (((2 · 𝑛) + 1) / (𝑛 + 1))) ∈ ℝ+)
178171, 176, 177sylancr 694 . . . . . 6 (𝑛 ∈ ℕ → (2 · (((2 · 𝑛) + 1) / (𝑛 + 1))) ∈ ℝ+)
179163, 170, 178ltmul1d 11789 . . . . 5 (𝑛 ∈ ℕ → (((4↑𝑛) / 𝑛) < ((2 · 𝑛)C𝑛) ↔ (((4↑𝑛) / 𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))) < (((2 · 𝑛)C𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1))))))
180 bcp1ctr 24804 . . . . . . 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 4595 . . . . 5 (𝑛 ∈ ℕ → ((((4↑𝑛) / 𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))) < ((2 · (𝑛 + 1))C(𝑛 + 1)) ↔ (((4↑𝑛) / 𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))) < (((2 · 𝑛)C𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1))))))
183179, 182bitr4d 270 . . . 4 (𝑛 ∈ ℕ → (((4↑𝑛) / 𝑛) < ((2 · 𝑛)C𝑛) ↔ (((4↑𝑛) / 𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))) < ((2 · (𝑛 + 1))C(𝑛 + 1))))
184 2re 10967 . . . . . . . 8 2 ∈ ℝ
185184a1i 11 . . . . . . 7 (𝑛 ∈ ℕ → 2 ∈ ℝ)
186173, 161rpdivcld 11765 . . . . . . . 8 (𝑛 ∈ ℕ → (((2 · 𝑛) + 1) / 𝑛) ∈ ℝ+)
187186rpred 11748 . . . . . . 7 (𝑛 ∈ ℕ → (((2 · 𝑛) + 1) / 𝑛) ∈ ℝ)
188 nnmulcl 10920 . . . . . . . . . 10 (((4↑𝑛) ∈ ℕ ∧ 2 ∈ ℕ) → ((4↑𝑛) · 2) ∈ ℕ)
189159, 117, 188sylancl 693 . . . . . . . . 9 (𝑛 ∈ ℕ → ((4↑𝑛) · 2) ∈ ℕ)
190189nnrpd 11746 . . . . . . . 8 (𝑛 ∈ ℕ → ((4↑𝑛) · 2) ∈ ℝ+)
191190, 175rpdivcld 11765 . . . . . . 7 (𝑛 ∈ ℕ → (((4↑𝑛) · 2) / (𝑛 + 1)) ∈ ℝ+)
192161rpreccld 11758 . . . . . . . . 9 (𝑛 ∈ ℕ → (1 / 𝑛) ∈ ℝ+)
193 ltaddrp 11743 . . . . . . . . 9 ((2 ∈ ℝ ∧ (1 / 𝑛) ∈ ℝ+) → 2 < (2 + (1 / 𝑛)))
194184, 192, 193sylancr 694 . . . . . . . 8 (𝑛 ∈ ℕ → 2 < (2 + (1 / 𝑛)))
195165nncnd 10913 . . . . . . . . . 10 (𝑛 ∈ ℕ → (2 · 𝑛) ∈ ℂ)
196 1cnd 9935 . . . . . . . . . 10 (𝑛 ∈ ℕ → 1 ∈ ℂ)
197 nncn 10905 . . . . . . . . . 10 (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
198 nnne0 10930 . . . . . . . . . 10 (𝑛 ∈ ℕ → 𝑛 ≠ 0)
199195, 196, 197, 198divdird 10718 . . . . . . . . 9 (𝑛 ∈ ℕ → (((2 · 𝑛) + 1) / 𝑛) = (((2 · 𝑛) / 𝑛) + (1 / 𝑛)))
20033a1i 11 . . . . . . . . . . 11 (𝑛 ∈ ℕ → 2 ∈ ℂ)
201200, 197, 198divcan4d 10686 . . . . . . . . . 10 (𝑛 ∈ ℕ → ((2 · 𝑛) / 𝑛) = 2)
202201oveq1d 6564 . . . . . . . . 9 (𝑛 ∈ ℕ → (((2 · 𝑛) / 𝑛) + (1 / 𝑛)) = (2 + (1 / 𝑛)))
203199, 202eqtr2d 2645 . . . . . . . 8 (𝑛 ∈ ℕ → (2 + (1 / 𝑛)) = (((2 · 𝑛) + 1) / 𝑛))
204194, 203breqtrd 4609 . . . . . . 7 (𝑛 ∈ ℕ → 2 < (((2 · 𝑛) + 1) / 𝑛))
205185, 187, 191, 204ltmul2dd 11804 . . . . . 6 (𝑛 ∈ ℕ → ((((4↑𝑛) · 2) / (𝑛 + 1)) · 2) < ((((4↑𝑛) · 2) / (𝑛 + 1)) · (((2 · 𝑛) + 1) / 𝑛)))
206 expp1 12729 . . . . . . . . . 10 ((4 ∈ ℂ ∧ 𝑛 ∈ ℕ0) → (4↑(𝑛 + 1)) = ((4↑𝑛) · 4))
20749, 157, 206sylancr 694 . . . . . . . . 9 (𝑛 ∈ ℕ → (4↑(𝑛 + 1)) = ((4↑𝑛) · 4))
208159nncnd 10913 . . . . . . . . . . 11 (𝑛 ∈ ℕ → (4↑𝑛) ∈ ℂ)
209208, 200, 200mulassd 9942 . . . . . . . . . 10 (𝑛 ∈ ℕ → (((4↑𝑛) · 2) · 2) = ((4↑𝑛) · (2 · 2)))
210103oveq2i 6560 . . . . . . . . . 10 ((4↑𝑛) · (2 · 2)) = ((4↑𝑛) · 4)
211209, 210syl6eq 2660 . . . . . . . . 9 (𝑛 ∈ ℕ → (((4↑𝑛) · 2) · 2) = ((4↑𝑛) · 4))
212207, 211eqtr4d 2647 . . . . . . . 8 (𝑛 ∈ ℕ → (4↑(𝑛 + 1)) = (((4↑𝑛) · 2) · 2))
213212oveq1d 6564 . . . . . . 7 (𝑛 ∈ ℕ → ((4↑(𝑛 + 1)) / (𝑛 + 1)) = ((((4↑𝑛) · 2) · 2) / (𝑛 + 1)))
214189nncnd 10913 . . . . . . . 8 (𝑛 ∈ ℕ → ((4↑𝑛) · 2) ∈ ℂ)
215174nncnd 10913 . . . . . . . 8 (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℂ)
216174nnne0d 10942 . . . . . . . 8 (𝑛 ∈ ℕ → (𝑛 + 1) ≠ 0)
217214, 200, 215, 216div23d 10717 . . . . . . 7 (𝑛 ∈ ℕ → ((((4↑𝑛) · 2) · 2) / (𝑛 + 1)) = ((((4↑𝑛) · 2) / (𝑛 + 1)) · 2))
218213, 217eqtrd 2644 . . . . . 6 (𝑛 ∈ ℕ → ((4↑(𝑛 + 1)) / (𝑛 + 1)) = ((((4↑𝑛) · 2) / (𝑛 + 1)) · 2))
219208, 200, 197, 198div23d 10717 . . . . . . . 8 (𝑛 ∈ ℕ → (((4↑𝑛) · 2) / 𝑛) = (((4↑𝑛) / 𝑛) · 2))
220219oveq1d 6564 . . . . . . 7 (𝑛 ∈ ℕ → ((((4↑𝑛) · 2) / 𝑛) · (((2 · 𝑛) + 1) / (𝑛 + 1))) = ((((4↑𝑛) / 𝑛) · 2) · (((2 · 𝑛) + 1) / (𝑛 + 1))))
221172nncnd 10913 . . . . . . . 8 (𝑛 ∈ ℕ → ((2 · 𝑛) + 1) ∈ ℂ)
222214, 197, 221, 215, 198, 216divmul24d 10723 . . . . . . 7 (𝑛 ∈ ℕ → ((((4↑𝑛) · 2) / 𝑛) · (((2 · 𝑛) + 1) / (𝑛 + 1))) = ((((4↑𝑛) · 2) / (𝑛 + 1)) · (((2 · 𝑛) + 1) / 𝑛)))
223162rpcnd 11750 . . . . . . . 8 (𝑛 ∈ ℕ → ((4↑𝑛) / 𝑛) ∈ ℂ)
224176rpcnd 11750 . . . . . . . 8 (𝑛 ∈ ℕ → (((2 · 𝑛) + 1) / (𝑛 + 1)) ∈ ℂ)
225223, 200, 224mulassd 9942 . . . . . . 7 (𝑛 ∈ ℕ → ((((4↑𝑛) / 𝑛) · 2) · (((2 · 𝑛) + 1) / (𝑛 + 1))) = (((4↑𝑛) / 𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))))
226220, 222, 2253eqtr3rd 2653 . . . . . 6 (𝑛 ∈ ℕ → (((4↑𝑛) / 𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))) = ((((4↑𝑛) · 2) / (𝑛 + 1)) · (((2 · 𝑛) + 1) / 𝑛)))
227205, 218, 2263brtr4d 4615 . . . . 5 (𝑛 ∈ ℕ → ((4↑(𝑛 + 1)) / (𝑛 + 1)) < (((4↑𝑛) / 𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))))
228174nnnn0d 11228 . . . . . . . . . 10 (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℕ0)
229 nnexpcl 12735 . . . . . . . . . 10 ((4 ∈ ℕ ∧ (𝑛 + 1) ∈ ℕ0) → (4↑(𝑛 + 1)) ∈ ℕ)
230154, 228, 229sylancr 694 . . . . . . . . 9 (𝑛 ∈ ℕ → (4↑(𝑛 + 1)) ∈ ℕ)
231230nnrpd 11746 . . . . . . . 8 (𝑛 ∈ ℕ → (4↑(𝑛 + 1)) ∈ ℝ+)
232231, 175rpdivcld 11765 . . . . . . 7 (𝑛 ∈ ℕ → ((4↑(𝑛 + 1)) / (𝑛 + 1)) ∈ ℝ+)
233232rpred 11748 . . . . . 6 (𝑛 ∈ ℕ → ((4↑(𝑛 + 1)) / (𝑛 + 1)) ∈ ℝ)
234178rpred 11748 . . . . . . 7 (𝑛 ∈ ℕ → (2 · (((2 · 𝑛) + 1) / (𝑛 + 1))) ∈ ℝ)
235163, 234remulcld 9949 . . . . . 6 (𝑛 ∈ ℕ → (((4↑𝑛) / 𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))) ∈ ℝ)
236 nn0mulcl 11206 . . . . . . . . 9 ((2 ∈ ℕ0 ∧ (𝑛 + 1) ∈ ℕ0) → (2 · (𝑛 + 1)) ∈ ℕ0)
23734, 228, 236sylancr 694 . . . . . . . 8 (𝑛 ∈ ℕ → (2 · (𝑛 + 1)) ∈ ℕ0)
238174nnzd 11357 . . . . . . . 8 (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℤ)
239 bccl 12971 . . . . . . . 8 (((2 · (𝑛 + 1)) ∈ ℕ0 ∧ (𝑛 + 1) ∈ ℤ) → ((2 · (𝑛 + 1))C(𝑛 + 1)) ∈ ℕ0)
240237, 238, 239syl2anc 691 . . . . . . 7 (𝑛 ∈ ℕ → ((2 · (𝑛 + 1))C(𝑛 + 1)) ∈ ℕ0)
241240nn0red 11229 . . . . . 6 (𝑛 ∈ ℕ → ((2 · (𝑛 + 1))C(𝑛 + 1)) ∈ ℝ)
242 lttr 9993 . . . . . 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 1318 . . . . 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 707 . . . 4 (𝑛 ∈ ℕ → ((((4↑𝑛) / 𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))) < ((2 · (𝑛 + 1))C(𝑛 + 1)) → ((4↑(𝑛 + 1)) / (𝑛 + 1)) < ((2 · (𝑛 + 1))C(𝑛 + 1))))
245183, 244sylbid 229 . . 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 11626 1 (𝑁 ∈ (ℤ‘4) → ((4↑𝑁) / 𝑁) < ((2 · 𝑁)C𝑁))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1475  wcel 1977  wne 2780   class class class wbr 4583  cfv 5804  (class class class)co 6549  cc 9813  cr 9814  0cc0 9815  1c1 9816   + caddc 9818   · cmul 9820   < clt 9953  cmin 10145   / cdiv 10563  cn 10897  2c2 10947  3c3 10948  4c4 10949  5c5 10950  6c6 10951  7c7 10952  0cn0 11169  cz 11254  cdc 11369  cuz 11563  +crp 11708  cexp 12722  Ccbc 12951
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-4 10958  df-5 10959  df-6 10960  df-7 10961  df-8 10962  df-9 10963  df-n0 11170  df-z 11255  df-dec 11370  df-uz 11564  df-rp 11709  df-fz 12198  df-seq 12664  df-exp 12723  df-fac 12923  df-bc 12952
This theorem is referenced by:  bposlem6  24814  chebbnd1lem1  24958
  Copyright terms: Public domain W3C validator