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

Theorem bclbnd 25977
 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 oveq2 7164 . . . 4 (𝑥 = 4 → (4↑𝑥) = (4↑4))
2 id 22 . . . 4 (𝑥 = 4 → 𝑥 = 4)
31, 2oveq12d 7174 . . 3 (𝑥 = 4 → ((4↑𝑥) / 𝑥) = ((4↑4) / 4))
4 oveq2 7164 . . . 4 (𝑥 = 4 → (2 · 𝑥) = (2 · 4))
54, 2oveq12d 7174 . . 3 (𝑥 = 4 → ((2 · 𝑥)C𝑥) = ((2 · 4)C4))
63, 5breq12d 5049 . 2 (𝑥 = 4 → (((4↑𝑥) / 𝑥) < ((2 · 𝑥)C𝑥) ↔ ((4↑4) / 4) < ((2 · 4)C4)))
7 oveq2 7164 . . . 4 (𝑥 = 𝑛 → (4↑𝑥) = (4↑𝑛))
8 id 22 . . . 4 (𝑥 = 𝑛𝑥 = 𝑛)
97, 8oveq12d 7174 . . 3 (𝑥 = 𝑛 → ((4↑𝑥) / 𝑥) = ((4↑𝑛) / 𝑛))
10 oveq2 7164 . . . 4 (𝑥 = 𝑛 → (2 · 𝑥) = (2 · 𝑛))
1110, 8oveq12d 7174 . . 3 (𝑥 = 𝑛 → ((2 · 𝑥)C𝑥) = ((2 · 𝑛)C𝑛))
129, 11breq12d 5049 . 2 (𝑥 = 𝑛 → (((4↑𝑥) / 𝑥) < ((2 · 𝑥)C𝑥) ↔ ((4↑𝑛) / 𝑛) < ((2 · 𝑛)C𝑛)))
13 oveq2 7164 . . . 4 (𝑥 = (𝑛 + 1) → (4↑𝑥) = (4↑(𝑛 + 1)))
14 id 22 . . . 4 (𝑥 = (𝑛 + 1) → 𝑥 = (𝑛 + 1))
1513, 14oveq12d 7174 . . 3 (𝑥 = (𝑛 + 1) → ((4↑𝑥) / 𝑥) = ((4↑(𝑛 + 1)) / (𝑛 + 1)))
16 oveq2 7164 . . . 4 (𝑥 = (𝑛 + 1) → (2 · 𝑥) = (2 · (𝑛 + 1)))
1716, 14oveq12d 7174 . . 3 (𝑥 = (𝑛 + 1) → ((2 · 𝑥)C𝑥) = ((2 · (𝑛 + 1))C(𝑛 + 1)))
1815, 17breq12d 5049 . 2 (𝑥 = (𝑛 + 1) → (((4↑𝑥) / 𝑥) < ((2 · 𝑥)C𝑥) ↔ ((4↑(𝑛 + 1)) / (𝑛 + 1)) < ((2 · (𝑛 + 1))C(𝑛 + 1))))
19 oveq2 7164 . . . 4 (𝑥 = 𝑁 → (4↑𝑥) = (4↑𝑁))
20 id 22 . . . 4 (𝑥 = 𝑁𝑥 = 𝑁)
2119, 20oveq12d 7174 . . 3 (𝑥 = 𝑁 → ((4↑𝑥) / 𝑥) = ((4↑𝑁) / 𝑁))
22 oveq2 7164 . . . 4 (𝑥 = 𝑁 → (2 · 𝑥) = (2 · 𝑁))
2322, 20oveq12d 7174 . . 3 (𝑥 = 𝑁 → ((2 · 𝑥)C𝑥) = ((2 · 𝑁)C𝑁))
2421, 23breq12d 5049 . 2 (𝑥 = 𝑁 → (((4↑𝑥) / 𝑥) < ((2 · 𝑥)C𝑥) ↔ ((4↑𝑁) / 𝑁) < ((2 · 𝑁)C𝑁)))
25 6nn0 11968 . . . 4 6 ∈ ℕ0
26 7nn0 11969 . . . 4 7 ∈ ℕ0
27 4nn0 11966 . . . 4 4 ∈ ℕ0
28 0nn0 11962 . . . 4 0 ∈ ℕ0
29 4lt10 12286 . . . 4 4 < 10
30 6lt7 11873 . . . 4 6 < 7
3125, 26, 27, 28, 29, 30decltc 12179 . . 3 64 < 70
32 2cn 11762 . . . . . 6 2 ∈ ℂ
33 2nn0 11964 . . . . . 6 2 ∈ ℕ0
34 3nn0 11965 . . . . . 6 3 ∈ ℕ0
35 expmul 13537 . . . . . 6 ((2 ∈ ℂ ∧ 2 ∈ ℕ0 ∧ 3 ∈ ℕ0) → (2↑(2 · 3)) = ((2↑2)↑3))
3632, 33, 34, 35mp3an 1458 . . . . 5 (2↑(2 · 3)) = ((2↑2)↑3)
37 sq2 13623 . . . . . . 7 (2↑2) = 4
3837eqcomi 2767 . . . . . 6 4 = (2↑2)
39 4m1e3 11816 . . . . . 6 (4 − 1) = 3
4038, 39oveq12i 7168 . . . . 5 (4↑(4 − 1)) = ((2↑2)↑3)
4136, 40eqtr4i 2784 . . . 4 (2↑(2 · 3)) = (4↑(4 − 1))
42 3cn 11768 . . . . . . 7 3 ∈ ℂ
43 3t2e6 11853 . . . . . . 7 (3 · 2) = 6
4442, 32, 43mulcomli 10701 . . . . . 6 (2 · 3) = 6
4544oveq2i 7167 . . . . 5 (2↑(2 · 3)) = (2↑6)
46 2exp6 16492 . . . . 5 (2↑6) = 64
4745, 46eqtri 2781 . . . 4 (2↑(2 · 3)) = 64
48 4cn 11772 . . . . 5 4 ∈ ℂ
49 4ne0 11795 . . . . 5 4 ≠ 0
50 4z 12068 . . . . 5 4 ∈ ℤ
51 expm1 13542 . . . . 5 ((4 ∈ ℂ ∧ 4 ≠ 0 ∧ 4 ∈ ℤ) → (4↑(4 − 1)) = ((4↑4) / 4))
5248, 49, 50, 51mp3an 1458 . . . 4 (4↑(4 − 1)) = ((4↑4) / 4)
5341, 47, 523eqtr3ri 2790 . . 3 ((4↑4) / 4) = 64
54 df-4 11752 . . . . . . 7 4 = (3 + 1)
5554oveq2i 7167 . . . . . 6 (2 · 4) = (2 · (3 + 1))
5655, 54oveq12i 7168 . . . . 5 ((2 · 4)C4) = ((2 · (3 + 1))C(3 + 1))
57 bcp1ctr 25976 . . . . . 6 (3 ∈ ℕ0 → ((2 · (3 + 1))C(3 + 1)) = (((2 · 3)C3) · (2 · (((2 · 3) + 1) / (3 + 1)))))
5834, 57ax-mp 5 . . . . 5 ((2 · (3 + 1))C(3 + 1)) = (((2 · 3)C3) · (2 · (((2 · 3) + 1) / (3 + 1))))
59 df-3 11751 . . . . . . . . 9 3 = (2 + 1)
6059oveq2i 7167 . . . . . . . 8 (2 · 3) = (2 · (2 + 1))
6160, 59oveq12i 7168 . . . . . . 7 ((2 · 3)C3) = ((2 · (2 + 1))C(2 + 1))
62 bcp1ctr 25976 . . . . . . . . 9 (2 ∈ ℕ0 → ((2 · (2 + 1))C(2 + 1)) = (((2 · 2)C2) · (2 · (((2 · 2) + 1) / (2 + 1)))))
6333, 62ax-mp 5 . . . . . . . 8 ((2 · (2 + 1))C(2 + 1)) = (((2 · 2)C2) · (2 · (((2 · 2) + 1) / (2 + 1))))
64 df-2 11750 . . . . . . . . . . . 12 2 = (1 + 1)
6564oveq2i 7167 . . . . . . . . . . 11 (2 · 2) = (2 · (1 + 1))
6665, 64oveq12i 7168 . . . . . . . . . 10 ((2 · 2)C2) = ((2 · (1 + 1))C(1 + 1))
67 1nn0 11963 . . . . . . . . . . 11 1 ∈ ℕ0
68 bcp1ctr 25976 . . . . . . . . . . 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 12192 . . . . . . . . . . . . . . 15 1 = (0 + 1)
7170oveq2i 7167 . . . . . . . . . . . . . 14 (2 · 1) = (2 · (0 + 1))
7271, 70oveq12i 7168 . . . . . . . . . . . . 13 ((2 · 1)C1) = ((2 · (0 + 1))C(0 + 1))
73 bcp1ctr 25976 . . . . . . . . . . . . . 14 (0 ∈ ℕ0 → ((2 · (0 + 1))C(0 + 1)) = (((2 · 0)C0) · (2 · (((2 · 0) + 1) / (0 + 1)))))
7428, 73ax-mp 5 . . . . . . . . . . . . 13 ((2 · (0 + 1))C(0 + 1)) = (((2 · 0)C0) · (2 · (((2 · 0) + 1) / (0 + 1))))
7533, 28nn0mulcli 11985 . . . . . . . . . . . . . . . 16 (2 · 0) ∈ ℕ0
76 bcn0 13733 . . . . . . . . . . . . . . . 16 ((2 · 0) ∈ ℕ0 → ((2 · 0)C0) = 1)
7775, 76ax-mp 5 . . . . . . . . . . . . . . 15 ((2 · 0)C0) = 1
78 2t0e0 11856 . . . . . . . . . . . . . . . . . . . . 21 (2 · 0) = 0
7978oveq1i 7166 . . . . . . . . . . . . . . . . . . . 20 ((2 · 0) + 1) = (0 + 1)
8079, 70eqtr4i 2784 . . . . . . . . . . . . . . . . . . 19 ((2 · 0) + 1) = 1
8170eqcomi 2767 . . . . . . . . . . . . . . . . . . 19 (0 + 1) = 1
8280, 81oveq12i 7168 . . . . . . . . . . . . . . . . . 18 (((2 · 0) + 1) / (0 + 1)) = (1 / 1)
83 1div1e1 11381 . . . . . . . . . . . . . . . . . 18 (1 / 1) = 1
8482, 83eqtri 2781 . . . . . . . . . . . . . . . . 17 (((2 · 0) + 1) / (0 + 1)) = 1
8584oveq2i 7167 . . . . . . . . . . . . . . . 16 (2 · (((2 · 0) + 1) / (0 + 1))) = (2 · 1)
86 2t1e2 11850 . . . . . . . . . . . . . . . 16 (2 · 1) = 2
8785, 86eqtri 2781 . . . . . . . . . . . . . . 15 (2 · (((2 · 0) + 1) / (0 + 1))) = 2
8877, 87oveq12i 7168 . . . . . . . . . . . . . 14 (((2 · 0)C0) · (2 · (((2 · 0) + 1) / (0 + 1)))) = (1 · 2)
8932mulid2i 10697 . . . . . . . . . . . . . 14 (1 · 2) = 2
9088, 89eqtri 2781 . . . . . . . . . . . . 13 (((2 · 0)C0) · (2 · (((2 · 0) + 1) / (0 + 1)))) = 2
9172, 74, 903eqtri 2785 . . . . . . . . . . . 12 ((2 · 1)C1) = 2
9286oveq1i 7166 . . . . . . . . . . . . . . . 16 ((2 · 1) + 1) = (2 + 1)
9392, 59eqtr4i 2784 . . . . . . . . . . . . . . 15 ((2 · 1) + 1) = 3
9464eqcomi 2767 . . . . . . . . . . . . . . 15 (1 + 1) = 2
9593, 94oveq12i 7168 . . . . . . . . . . . . . 14 (((2 · 1) + 1) / (1 + 1)) = (3 / 2)
9695oveq2i 7167 . . . . . . . . . . . . 13 (2 · (((2 · 1) + 1) / (1 + 1))) = (2 · (3 / 2))
97 2ne0 11791 . . . . . . . . . . . . . 14 2 ≠ 0
9842, 32, 97divcan2i 11434 . . . . . . . . . . . . 13 (2 · (3 / 2)) = 3
9996, 98eqtri 2781 . . . . . . . . . . . 12 (2 · (((2 · 1) + 1) / (1 + 1))) = 3
10091, 99oveq12i 7168 . . . . . . . . . . 11 (((2 · 1)C1) · (2 · (((2 · 1) + 1) / (1 + 1)))) = (2 · 3)
101100, 44eqtri 2781 . . . . . . . . . 10 (((2 · 1)C1) · (2 · (((2 · 1) + 1) / (1 + 1)))) = 6
10266, 69, 1013eqtri 2785 . . . . . . . . 9 ((2 · 2)C2) = 6
103 2t2e4 11851 . . . . . . . . . . . . . 14 (2 · 2) = 4
104103oveq1i 7166 . . . . . . . . . . . . 13 ((2 · 2) + 1) = (4 + 1)
105 df-5 11753 . . . . . . . . . . . . 13 5 = (4 + 1)
106104, 105eqtr4i 2784 . . . . . . . . . . . 12 ((2 · 2) + 1) = 5
10759eqcomi 2767 . . . . . . . . . . . 12 (2 + 1) = 3
108106, 107oveq12i 7168 . . . . . . . . . . 11 (((2 · 2) + 1) / (2 + 1)) = (5 / 3)
109108oveq2i 7167 . . . . . . . . . 10 (2 · (((2 · 2) + 1) / (2 + 1))) = (2 · (5 / 3))
110 5cn 11775 . . . . . . . . . . 11 5 ∈ ℂ
111 3ne0 11793 . . . . . . . . . . 11 3 ≠ 0
11232, 110, 42, 111divassi 11447 . . . . . . . . . 10 ((2 · 5) / 3) = (2 · (5 / 3))
113109, 112eqtr4i 2784 . . . . . . . . 9 (2 · (((2 · 2) + 1) / (2 + 1))) = ((2 · 5) / 3)
114102, 113oveq12i 7168 . . . . . . . 8 (((2 · 2)C2) · (2 · (((2 · 2) + 1) / (2 + 1)))) = (6 · ((2 · 5) / 3))
11563, 114eqtri 2781 . . . . . . 7 ((2 · (2 + 1))C(2 + 1)) = (6 · ((2 · 5) / 3))
116 6cn 11778 . . . . . . . . 9 6 ∈ ℂ
117 2nn 11760 . . . . . . . . . . 11 2 ∈ ℕ
118 5nn 11773 . . . . . . . . . . 11 5 ∈ ℕ
119117, 118nnmulcli 11712 . . . . . . . . . 10 (2 · 5) ∈ ℕ
120119nncni 11697 . . . . . . . . 9 (2 · 5) ∈ ℂ
12142, 111pm3.2i 474 . . . . . . . . 9 (3 ∈ ℂ ∧ 3 ≠ 0)
122 div12 11371 . . . . . . . . 9 ((6 ∈ ℂ ∧ (2 · 5) ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → (6 · ((2 · 5) / 3)) = ((2 · 5) · (6 / 3)))
123116, 120, 121, 122mp3an 1458 . . . . . . . 8 (6 · ((2 · 5) / 3)) = ((2 · 5) · (6 / 3))
124 5t2e10 12250 . . . . . . . . . 10 (5 · 2) = 10
125110, 32, 124mulcomli 10701 . . . . . . . . 9 (2 · 5) = 10
126116, 42, 32, 111divmuli 11445 . . . . . . . . . 10 ((6 / 3) = 2 ↔ (3 · 2) = 6)
12743, 126mpbir 234 . . . . . . . . 9 (6 / 3) = 2
128125, 127oveq12i 7168 . . . . . . . 8 ((2 · 5) · (6 / 3)) = (10 · 2)
129123, 128eqtri 2781 . . . . . . 7 (6 · ((2 · 5) / 3)) = (10 · 2)
13061, 115, 1293eqtri 2785 . . . . . 6 ((2 · 3)C3) = (10 · 2)
13144oveq1i 7166 . . . . . . . . 9 ((2 · 3) + 1) = (6 + 1)
132 df-7 11755 . . . . . . . . 9 7 = (6 + 1)
133131, 132eqtr4i 2784 . . . . . . . 8 ((2 · 3) + 1) = 7
134 3p1e4 11832 . . . . . . . 8 (3 + 1) = 4
135133, 134oveq12i 7168 . . . . . . 7 (((2 · 3) + 1) / (3 + 1)) = (7 / 4)
136135oveq2i 7167 . . . . . 6 (2 · (((2 · 3) + 1) / (3 + 1))) = (2 · (7 / 4))
137130, 136oveq12i 7168 . . . . 5 (((2 · 3)C3) · (2 · (((2 · 3) + 1) / (3 + 1)))) = ((10 · 2) · (2 · (7 / 4)))
13856, 58, 1373eqtri 2785 . . . 4 ((2 · 4)C4) = ((10 · 2) · (2 · (7 / 4)))
139 10nn 12166 . . . . . . 7 10 ∈ ℕ
140139nncni 11697 . . . . . 6 10 ∈ ℂ
141 7cn 11781 . . . . . . . 8 7 ∈ ℂ
142141, 48, 49divcli 11433 . . . . . . 7 (7 / 4) ∈ ℂ
14332, 142mulcli 10699 . . . . . 6 (2 · (7 / 4)) ∈ ℂ
144140, 32, 143mulassi 10703 . . . . 5 ((10 · 2) · (2 · (7 / 4))) = (10 · (2 · (2 · (7 / 4))))
145103oveq1i 7166 . . . . . . 7 ((2 · 2) · (7 / 4)) = (4 · (7 / 4))
14632, 32, 142mulassi 10703 . . . . . . 7 ((2 · 2) · (7 / 4)) = (2 · (2 · (7 / 4)))
147141, 48, 49divcan2i 11434 . . . . . . 7 (4 · (7 / 4)) = 7
148145, 146, 1473eqtr3i 2789 . . . . . 6 (2 · (2 · (7 / 4))) = 7
149148oveq2i 7167 . . . . 5 (10 · (2 · (2 · (7 / 4)))) = (10 · 7)
150144, 149eqtri 2781 . . . 4 ((10 · 2) · (2 · (7 / 4))) = (10 · 7)
15126dec0u 12171 . . . 4 (10 · 7) = 70
152138, 150, 1513eqtri 2785 . . 3 ((2 · 4)C4) = 70
15331, 53, 1523brtr4i 5066 . 2 ((4↑4) / 4) < ((2 · 4)C4)
154 4nn 11770 . . . 4 4 ∈ ℕ
155 eluznn 12371 . . . 4 ((4 ∈ ℕ ∧ 𝑛 ∈ (ℤ‘4)) → 𝑛 ∈ ℕ)
156154, 155mpan 689 . . 3 (𝑛 ∈ (ℤ‘4) → 𝑛 ∈ ℕ)
157 nnnn0 11954 . . . . . . . . . 10 (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
158 nnexpcl 13505 . . . . . . . . . 10 ((4 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → (4↑𝑛) ∈ ℕ)
159154, 157, 158sylancr 590 . . . . . . . . 9 (𝑛 ∈ ℕ → (4↑𝑛) ∈ ℕ)
160159nnrpd 12483 . . . . . . . 8 (𝑛 ∈ ℕ → (4↑𝑛) ∈ ℝ+)
161 nnrp 12454 . . . . . . . 8 (𝑛 ∈ ℕ → 𝑛 ∈ ℝ+)
162160, 161rpdivcld 12502 . . . . . . 7 (𝑛 ∈ ℕ → ((4↑𝑛) / 𝑛) ∈ ℝ+)
163162rpred 12485 . . . . . 6 (𝑛 ∈ ℕ → ((4↑𝑛) / 𝑛) ∈ ℝ)
164 nnmulcl 11711 . . . . . . . . . 10 ((2 ∈ ℕ ∧ 𝑛 ∈ ℕ) → (2 · 𝑛) ∈ ℕ)
165117, 164mpan 689 . . . . . . . . 9 (𝑛 ∈ ℕ → (2 · 𝑛) ∈ ℕ)
166165nnnn0d 12007 . . . . . . . 8 (𝑛 ∈ ℕ → (2 · 𝑛) ∈ ℕ0)
167 nnz 12056 . . . . . . . 8 (𝑛 ∈ ℕ → 𝑛 ∈ ℤ)
168 bccl 13745 . . . . . . . 8 (((2 · 𝑛) ∈ ℕ0𝑛 ∈ ℤ) → ((2 · 𝑛)C𝑛) ∈ ℕ0)
169166, 167, 168syl2anc 587 . . . . . . 7 (𝑛 ∈ ℕ → ((2 · 𝑛)C𝑛) ∈ ℕ0)
170169nn0red 12008 . . . . . 6 (𝑛 ∈ ℕ → ((2 · 𝑛)C𝑛) ∈ ℝ)
171 2rp 12448 . . . . . . 7 2 ∈ ℝ+
172165peano2nnd 11704 . . . . . . . . 9 (𝑛 ∈ ℕ → ((2 · 𝑛) + 1) ∈ ℕ)
173172nnrpd 12483 . . . . . . . 8 (𝑛 ∈ ℕ → ((2 · 𝑛) + 1) ∈ ℝ+)
174 peano2nn 11699 . . . . . . . . 9 (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℕ)
175174nnrpd 12483 . . . . . . . 8 (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℝ+)
176173, 175rpdivcld 12502 . . . . . . 7 (𝑛 ∈ ℕ → (((2 · 𝑛) + 1) / (𝑛 + 1)) ∈ ℝ+)
177 rpmulcl 12466 . . . . . . 7 ((2 ∈ ℝ+ ∧ (((2 · 𝑛) + 1) / (𝑛 + 1)) ∈ ℝ+) → (2 · (((2 · 𝑛) + 1) / (𝑛 + 1))) ∈ ℝ+)
178171, 176, 177sylancr 590 . . . . . 6 (𝑛 ∈ ℕ → (2 · (((2 · 𝑛) + 1) / (𝑛 + 1))) ∈ ℝ+)
179163, 170, 178ltmul1d 12526 . . . . 5 (𝑛 ∈ ℕ → (((4↑𝑛) / 𝑛) < ((2 · 𝑛)C𝑛) ↔ (((4↑𝑛) / 𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))) < (((2 · 𝑛)C𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1))))))
180 bcp1ctr 25976 . . . . . . 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 5048 . . . . 5 (𝑛 ∈ ℕ → ((((4↑𝑛) / 𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))) < ((2 · (𝑛 + 1))C(𝑛 + 1)) ↔ (((4↑𝑛) / 𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))) < (((2 · 𝑛)C𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1))))))
183179, 182bitr4d 285 . . . 4 (𝑛 ∈ ℕ → (((4↑𝑛) / 𝑛) < ((2 · 𝑛)C𝑛) ↔ (((4↑𝑛) / 𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))) < ((2 · (𝑛 + 1))C(𝑛 + 1))))
184 2re 11761 . . . . . . . 8 2 ∈ ℝ
185184a1i 11 . . . . . . 7 (𝑛 ∈ ℕ → 2 ∈ ℝ)
186173, 161rpdivcld 12502 . . . . . . . 8 (𝑛 ∈ ℕ → (((2 · 𝑛) + 1) / 𝑛) ∈ ℝ+)
187186rpred 12485 . . . . . . 7 (𝑛 ∈ ℕ → (((2 · 𝑛) + 1) / 𝑛) ∈ ℝ)
188 nnmulcl 11711 . . . . . . . . . 10 (((4↑𝑛) ∈ ℕ ∧ 2 ∈ ℕ) → ((4↑𝑛) · 2) ∈ ℕ)
189159, 117, 188sylancl 589 . . . . . . . . 9 (𝑛 ∈ ℕ → ((4↑𝑛) · 2) ∈ ℕ)
190189nnrpd 12483 . . . . . . . 8 (𝑛 ∈ ℕ → ((4↑𝑛) · 2) ∈ ℝ+)
191190, 175rpdivcld 12502 . . . . . . 7 (𝑛 ∈ ℕ → (((4↑𝑛) · 2) / (𝑛 + 1)) ∈ ℝ+)
192161rpreccld 12495 . . . . . . . . 9 (𝑛 ∈ ℕ → (1 / 𝑛) ∈ ℝ+)
193 ltaddrp 12480 . . . . . . . . 9 ((2 ∈ ℝ ∧ (1 / 𝑛) ∈ ℝ+) → 2 < (2 + (1 / 𝑛)))
194184, 192, 193sylancr 590 . . . . . . . 8 (𝑛 ∈ ℕ → 2 < (2 + (1 / 𝑛)))
195165nncnd 11703 . . . . . . . . . 10 (𝑛 ∈ ℕ → (2 · 𝑛) ∈ ℂ)
196 1cnd 10687 . . . . . . . . . 10 (𝑛 ∈ ℕ → 1 ∈ ℂ)
197 nncn 11695 . . . . . . . . . 10 (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
198 nnne0 11721 . . . . . . . . . 10 (𝑛 ∈ ℕ → 𝑛 ≠ 0)
199195, 196, 197, 198divdird 11505 . . . . . . . . 9 (𝑛 ∈ ℕ → (((2 · 𝑛) + 1) / 𝑛) = (((2 · 𝑛) / 𝑛) + (1 / 𝑛)))
20032a1i 11 . . . . . . . . . . 11 (𝑛 ∈ ℕ → 2 ∈ ℂ)
201200, 197, 198divcan4d 11473 . . . . . . . . . 10 (𝑛 ∈ ℕ → ((2 · 𝑛) / 𝑛) = 2)
202201oveq1d 7171 . . . . . . . . 9 (𝑛 ∈ ℕ → (((2 · 𝑛) / 𝑛) + (1 / 𝑛)) = (2 + (1 / 𝑛)))
203199, 202eqtr2d 2794 . . . . . . . 8 (𝑛 ∈ ℕ → (2 + (1 / 𝑛)) = (((2 · 𝑛) + 1) / 𝑛))
204194, 203breqtrd 5062 . . . . . . 7 (𝑛 ∈ ℕ → 2 < (((2 · 𝑛) + 1) / 𝑛))
205185, 187, 191, 204ltmul2dd 12541 . . . . . 6 (𝑛 ∈ ℕ → ((((4↑𝑛) · 2) / (𝑛 + 1)) · 2) < ((((4↑𝑛) · 2) / (𝑛 + 1)) · (((2 · 𝑛) + 1) / 𝑛)))
206 expp1 13499 . . . . . . . . . 10 ((4 ∈ ℂ ∧ 𝑛 ∈ ℕ0) → (4↑(𝑛 + 1)) = ((4↑𝑛) · 4))
20748, 157, 206sylancr 590 . . . . . . . . 9 (𝑛 ∈ ℕ → (4↑(𝑛 + 1)) = ((4↑𝑛) · 4))
208159nncnd 11703 . . . . . . . . . . 11 (𝑛 ∈ ℕ → (4↑𝑛) ∈ ℂ)
209208, 200, 200mulassd 10715 . . . . . . . . . 10 (𝑛 ∈ ℕ → (((4↑𝑛) · 2) · 2) = ((4↑𝑛) · (2 · 2)))
210103oveq2i 7167 . . . . . . . . . 10 ((4↑𝑛) · (2 · 2)) = ((4↑𝑛) · 4)
211209, 210eqtrdi 2809 . . . . . . . . 9 (𝑛 ∈ ℕ → (((4↑𝑛) · 2) · 2) = ((4↑𝑛) · 4))
212207, 211eqtr4d 2796 . . . . . . . 8 (𝑛 ∈ ℕ → (4↑(𝑛 + 1)) = (((4↑𝑛) · 2) · 2))
213212oveq1d 7171 . . . . . . 7 (𝑛 ∈ ℕ → ((4↑(𝑛 + 1)) / (𝑛 + 1)) = ((((4↑𝑛) · 2) · 2) / (𝑛 + 1)))
214189nncnd 11703 . . . . . . . 8 (𝑛 ∈ ℕ → ((4↑𝑛) · 2) ∈ ℂ)
215174nncnd 11703 . . . . . . . 8 (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℂ)
216174nnne0d 11737 . . . . . . . 8 (𝑛 ∈ ℕ → (𝑛 + 1) ≠ 0)
217214, 200, 215, 216div23d 11504 . . . . . . 7 (𝑛 ∈ ℕ → ((((4↑𝑛) · 2) · 2) / (𝑛 + 1)) = ((((4↑𝑛) · 2) / (𝑛 + 1)) · 2))
218213, 217eqtrd 2793 . . . . . 6 (𝑛 ∈ ℕ → ((4↑(𝑛 + 1)) / (𝑛 + 1)) = ((((4↑𝑛) · 2) / (𝑛 + 1)) · 2))
219208, 200, 197, 198div23d 11504 . . . . . . . 8 (𝑛 ∈ ℕ → (((4↑𝑛) · 2) / 𝑛) = (((4↑𝑛) / 𝑛) · 2))
220219oveq1d 7171 . . . . . . 7 (𝑛 ∈ ℕ → ((((4↑𝑛) · 2) / 𝑛) · (((2 · 𝑛) + 1) / (𝑛 + 1))) = ((((4↑𝑛) / 𝑛) · 2) · (((2 · 𝑛) + 1) / (𝑛 + 1))))
221172nncnd 11703 . . . . . . . 8 (𝑛 ∈ ℕ → ((2 · 𝑛) + 1) ∈ ℂ)
222214, 197, 221, 215, 198, 216divmul24d 11510 . . . . . . 7 (𝑛 ∈ ℕ → ((((4↑𝑛) · 2) / 𝑛) · (((2 · 𝑛) + 1) / (𝑛 + 1))) = ((((4↑𝑛) · 2) / (𝑛 + 1)) · (((2 · 𝑛) + 1) / 𝑛)))
223162rpcnd 12487 . . . . . . . 8 (𝑛 ∈ ℕ → ((4↑𝑛) / 𝑛) ∈ ℂ)
224176rpcnd 12487 . . . . . . . 8 (𝑛 ∈ ℕ → (((2 · 𝑛) + 1) / (𝑛 + 1)) ∈ ℂ)
225223, 200, 224mulassd 10715 . . . . . . 7 (𝑛 ∈ ℕ → ((((4↑𝑛) / 𝑛) · 2) · (((2 · 𝑛) + 1) / (𝑛 + 1))) = (((4↑𝑛) / 𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))))
226220, 222, 2253eqtr3rd 2802 . . . . . 6 (𝑛 ∈ ℕ → (((4↑𝑛) / 𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))) = ((((4↑𝑛) · 2) / (𝑛 + 1)) · (((2 · 𝑛) + 1) / 𝑛)))
227205, 218, 2263brtr4d 5068 . . . . 5 (𝑛 ∈ ℕ → ((4↑(𝑛 + 1)) / (𝑛 + 1)) < (((4↑𝑛) / 𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))))
228174nnnn0d 12007 . . . . . . . . . 10 (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℕ0)
229 nnexpcl 13505 . . . . . . . . . 10 ((4 ∈ ℕ ∧ (𝑛 + 1) ∈ ℕ0) → (4↑(𝑛 + 1)) ∈ ℕ)
230154, 228, 229sylancr 590 . . . . . . . . 9 (𝑛 ∈ ℕ → (4↑(𝑛 + 1)) ∈ ℕ)
231230nnrpd 12483 . . . . . . . 8 (𝑛 ∈ ℕ → (4↑(𝑛 + 1)) ∈ ℝ+)
232231, 175rpdivcld 12502 . . . . . . 7 (𝑛 ∈ ℕ → ((4↑(𝑛 + 1)) / (𝑛 + 1)) ∈ ℝ+)
233232rpred 12485 . . . . . 6 (𝑛 ∈ ℕ → ((4↑(𝑛 + 1)) / (𝑛 + 1)) ∈ ℝ)
234178rpred 12485 . . . . . . 7 (𝑛 ∈ ℕ → (2 · (((2 · 𝑛) + 1) / (𝑛 + 1))) ∈ ℝ)
235163, 234remulcld 10722 . . . . . 6 (𝑛 ∈ ℕ → (((4↑𝑛) / 𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))) ∈ ℝ)
236 nn0mulcl 11983 . . . . . . . . 9 ((2 ∈ ℕ0 ∧ (𝑛 + 1) ∈ ℕ0) → (2 · (𝑛 + 1)) ∈ ℕ0)
23733, 228, 236sylancr 590 . . . . . . . 8 (𝑛 ∈ ℕ → (2 · (𝑛 + 1)) ∈ ℕ0)
238174nnzd 12138 . . . . . . . 8 (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℤ)
239 bccl 13745 . . . . . . . 8 (((2 · (𝑛 + 1)) ∈ ℕ0 ∧ (𝑛 + 1) ∈ ℤ) → ((2 · (𝑛 + 1))C(𝑛 + 1)) ∈ ℕ0)
240237, 238, 239syl2anc 587 . . . . . . 7 (𝑛 ∈ ℕ → ((2 · (𝑛 + 1))C(𝑛 + 1)) ∈ ℕ0)
241240nn0red 12008 . . . . . 6 (𝑛 ∈ ℕ → ((2 · (𝑛 + 1))C(𝑛 + 1)) ∈ ℝ)
242 lttr 10768 . . . . . 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 1368 . . . . 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 694 . . . 4 (𝑛 ∈ ℕ → ((((4↑𝑛) / 𝑛) · (2 · (((2 · 𝑛) + 1) / (𝑛 + 1)))) < ((2 · (𝑛 + 1))C(𝑛 + 1)) → ((4↑(𝑛 + 1)) / (𝑛 + 1)) < ((2 · (𝑛 + 1))C(𝑛 + 1))))
245183, 244sylbid 243 . . 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))))
2476, 12, 18, 24, 153, 246uzind4i 12363 1 (𝑁 ∈ (ℤ‘4) → ((4↑𝑁) / 𝑁) < ((2 · 𝑁)C𝑁))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111   ≠ wne 2951   class class class wbr 5036  ‘cfv 6340  (class class class)co 7156  ℂcc 10586  ℝcr 10587  0cc0 10588  1c1 10589   + caddc 10591   · cmul 10593   < clt 10726   − cmin 10921   / cdiv 11348  ℕcn 11687  2c2 11742  3c3 11743  4c4 11744  5c5 11745  6c6 11746  7c7 11747  ℕ0cn0 11947  ℤcz 12033  ;cdc 12150  ℤ≥cuz 12295  ℝ+crp 12443  ↑cexp 13492  Ccbc 13725 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5173  ax-nul 5180  ax-pow 5238  ax-pr 5302  ax-un 7465  ax-cnex 10644  ax-resscn 10645  ax-1cn 10646  ax-icn 10647  ax-addcl 10648  ax-addrcl 10649  ax-mulcl 10650  ax-mulrcl 10651  ax-mulcom 10652  ax-addass 10653  ax-mulass 10654  ax-distr 10655  ax-i2m1 10656  ax-1ne0 10657  ax-1rid 10658  ax-rnegex 10659  ax-rrecex 10660  ax-cnre 10661  ax-pre-lttri 10662  ax-pre-lttrn 10663  ax-pre-ltadd 10664  ax-pre-mulgt0 10665 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-nel 3056  df-ral 3075  df-rex 3076  df-reu 3077  df-rmo 3078  df-rab 3079  df-v 3411  df-sbc 3699  df-csb 3808  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-pss 3879  df-nul 4228  df-if 4424  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-iun 4888  df-br 5037  df-opab 5099  df-mpt 5117  df-tr 5143  df-id 5434  df-eprel 5439  df-po 5447  df-so 5448  df-fr 5487  df-we 5489  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-res 5540  df-ima 5541  df-pred 6131  df-ord 6177  df-on 6178  df-lim 6179  df-suc 6180  df-iota 6299  df-fun 6342  df-fn 6343  df-f 6344  df-f1 6345  df-fo 6346  df-f1o 6347  df-fv 6348  df-riota 7114  df-ov 7159  df-oprab 7160  df-mpo 7161  df-om 7586  df-1st 7699  df-2nd 7700  df-wrecs 7963  df-recs 8024  df-rdg 8062  df-er 8305  df-en 8541  df-dom 8542  df-sdom 8543  df-pnf 10728  df-mnf 10729  df-xr 10730  df-ltxr 10731  df-le 10732  df-sub 10923  df-neg 10924  df-div 11349  df-nn 11688  df-2 11750  df-3 11751  df-4 11752  df-5 11753  df-6 11754  df-7 11755  df-8 11756  df-9 11757  df-n0 11948  df-z 12034  df-dec 12151  df-uz 12296  df-rp 12444  df-fz 12953  df-seq 13432  df-exp 13493  df-fac 13697  df-bc 13726 This theorem is referenced by:  bposlem6  25986  chebbnd1lem1  26166
 Copyright terms: Public domain W3C validator