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

Theorem bclbnd 26783
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 7417 . . . 4 (๐‘ฅ = 4 โ†’ (4โ†‘๐‘ฅ) = (4โ†‘4))
2 id 22 . . . 4 (๐‘ฅ = 4 โ†’ ๐‘ฅ = 4)
31, 2oveq12d 7427 . . 3 (๐‘ฅ = 4 โ†’ ((4โ†‘๐‘ฅ) / ๐‘ฅ) = ((4โ†‘4) / 4))
4 oveq2 7417 . . . 4 (๐‘ฅ = 4 โ†’ (2 ยท ๐‘ฅ) = (2 ยท 4))
54, 2oveq12d 7427 . . 3 (๐‘ฅ = 4 โ†’ ((2 ยท ๐‘ฅ)C๐‘ฅ) = ((2 ยท 4)C4))
63, 5breq12d 5162 . 2 (๐‘ฅ = 4 โ†’ (((4โ†‘๐‘ฅ) / ๐‘ฅ) < ((2 ยท ๐‘ฅ)C๐‘ฅ) โ†” ((4โ†‘4) / 4) < ((2 ยท 4)C4)))
7 oveq2 7417 . . . 4 (๐‘ฅ = ๐‘› โ†’ (4โ†‘๐‘ฅ) = (4โ†‘๐‘›))
8 id 22 . . . 4 (๐‘ฅ = ๐‘› โ†’ ๐‘ฅ = ๐‘›)
97, 8oveq12d 7427 . . 3 (๐‘ฅ = ๐‘› โ†’ ((4โ†‘๐‘ฅ) / ๐‘ฅ) = ((4โ†‘๐‘›) / ๐‘›))
10 oveq2 7417 . . . 4 (๐‘ฅ = ๐‘› โ†’ (2 ยท ๐‘ฅ) = (2 ยท ๐‘›))
1110, 8oveq12d 7427 . . 3 (๐‘ฅ = ๐‘› โ†’ ((2 ยท ๐‘ฅ)C๐‘ฅ) = ((2 ยท ๐‘›)C๐‘›))
129, 11breq12d 5162 . 2 (๐‘ฅ = ๐‘› โ†’ (((4โ†‘๐‘ฅ) / ๐‘ฅ) < ((2 ยท ๐‘ฅ)C๐‘ฅ) โ†” ((4โ†‘๐‘›) / ๐‘›) < ((2 ยท ๐‘›)C๐‘›)))
13 oveq2 7417 . . . 4 (๐‘ฅ = (๐‘› + 1) โ†’ (4โ†‘๐‘ฅ) = (4โ†‘(๐‘› + 1)))
14 id 22 . . . 4 (๐‘ฅ = (๐‘› + 1) โ†’ ๐‘ฅ = (๐‘› + 1))
1513, 14oveq12d 7427 . . 3 (๐‘ฅ = (๐‘› + 1) โ†’ ((4โ†‘๐‘ฅ) / ๐‘ฅ) = ((4โ†‘(๐‘› + 1)) / (๐‘› + 1)))
16 oveq2 7417 . . . 4 (๐‘ฅ = (๐‘› + 1) โ†’ (2 ยท ๐‘ฅ) = (2 ยท (๐‘› + 1)))
1716, 14oveq12d 7427 . . 3 (๐‘ฅ = (๐‘› + 1) โ†’ ((2 ยท ๐‘ฅ)C๐‘ฅ) = ((2 ยท (๐‘› + 1))C(๐‘› + 1)))
1815, 17breq12d 5162 . 2 (๐‘ฅ = (๐‘› + 1) โ†’ (((4โ†‘๐‘ฅ) / ๐‘ฅ) < ((2 ยท ๐‘ฅ)C๐‘ฅ) โ†” ((4โ†‘(๐‘› + 1)) / (๐‘› + 1)) < ((2 ยท (๐‘› + 1))C(๐‘› + 1))))
19 oveq2 7417 . . . 4 (๐‘ฅ = ๐‘ โ†’ (4โ†‘๐‘ฅ) = (4โ†‘๐‘))
20 id 22 . . . 4 (๐‘ฅ = ๐‘ โ†’ ๐‘ฅ = ๐‘)
2119, 20oveq12d 7427 . . 3 (๐‘ฅ = ๐‘ โ†’ ((4โ†‘๐‘ฅ) / ๐‘ฅ) = ((4โ†‘๐‘) / ๐‘))
22 oveq2 7417 . . . 4 (๐‘ฅ = ๐‘ โ†’ (2 ยท ๐‘ฅ) = (2 ยท ๐‘))
2322, 20oveq12d 7427 . . 3 (๐‘ฅ = ๐‘ โ†’ ((2 ยท ๐‘ฅ)C๐‘ฅ) = ((2 ยท ๐‘)C๐‘))
2421, 23breq12d 5162 . 2 (๐‘ฅ = ๐‘ โ†’ (((4โ†‘๐‘ฅ) / ๐‘ฅ) < ((2 ยท ๐‘ฅ)C๐‘ฅ) โ†” ((4โ†‘๐‘) / ๐‘) < ((2 ยท ๐‘)C๐‘)))
25 6nn0 12493 . . . 4 6 โˆˆ โ„•0
26 7nn0 12494 . . . 4 7 โˆˆ โ„•0
27 4nn0 12491 . . . 4 4 โˆˆ โ„•0
28 0nn0 12487 . . . 4 0 โˆˆ โ„•0
29 4lt10 12813 . . . 4 4 < 10
30 6lt7 12398 . . . 4 6 < 7
3125, 26, 27, 28, 29, 30decltc 12706 . . 3 64 < 70
32 2cn 12287 . . . . . 6 2 โˆˆ โ„‚
33 2nn0 12489 . . . . . 6 2 โˆˆ โ„•0
34 3nn0 12490 . . . . . 6 3 โˆˆ โ„•0
35 expmul 14073 . . . . . 6 ((2 โˆˆ โ„‚ โˆง 2 โˆˆ โ„•0 โˆง 3 โˆˆ โ„•0) โ†’ (2โ†‘(2 ยท 3)) = ((2โ†‘2)โ†‘3))
3632, 33, 34, 35mp3an 1462 . . . . 5 (2โ†‘(2 ยท 3)) = ((2โ†‘2)โ†‘3)
37 sq2 14161 . . . . . . 7 (2โ†‘2) = 4
3837eqcomi 2742 . . . . . 6 4 = (2โ†‘2)
39 4m1e3 12341 . . . . . 6 (4 โˆ’ 1) = 3
4038, 39oveq12i 7421 . . . . 5 (4โ†‘(4 โˆ’ 1)) = ((2โ†‘2)โ†‘3)
4136, 40eqtr4i 2764 . . . 4 (2โ†‘(2 ยท 3)) = (4โ†‘(4 โˆ’ 1))
42 3cn 12293 . . . . . . 7 3 โˆˆ โ„‚
43 3t2e6 12378 . . . . . . 7 (3 ยท 2) = 6
4442, 32, 43mulcomli 11223 . . . . . 6 (2 ยท 3) = 6
4544oveq2i 7420 . . . . 5 (2โ†‘(2 ยท 3)) = (2โ†‘6)
46 2exp6 17020 . . . . 5 (2โ†‘6) = 64
4745, 46eqtri 2761 . . . 4 (2โ†‘(2 ยท 3)) = 64
48 4cn 12297 . . . . 5 4 โˆˆ โ„‚
49 4ne0 12320 . . . . 5 4 โ‰  0
50 4z 12596 . . . . 5 4 โˆˆ โ„ค
51 expm1 14078 . . . . 5 ((4 โˆˆ โ„‚ โˆง 4 โ‰  0 โˆง 4 โˆˆ โ„ค) โ†’ (4โ†‘(4 โˆ’ 1)) = ((4โ†‘4) / 4))
5248, 49, 50, 51mp3an 1462 . . . 4 (4โ†‘(4 โˆ’ 1)) = ((4โ†‘4) / 4)
5341, 47, 523eqtr3ri 2770 . . 3 ((4โ†‘4) / 4) = 64
54 df-4 12277 . . . . . . 7 4 = (3 + 1)
5554oveq2i 7420 . . . . . 6 (2 ยท 4) = (2 ยท (3 + 1))
5655, 54oveq12i 7421 . . . . 5 ((2 ยท 4)C4) = ((2 ยท (3 + 1))C(3 + 1))
57 bcp1ctr 26782 . . . . . 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 12276 . . . . . . . . 9 3 = (2 + 1)
6059oveq2i 7420 . . . . . . . 8 (2 ยท 3) = (2 ยท (2 + 1))
6160, 59oveq12i 7421 . . . . . . 7 ((2 ยท 3)C3) = ((2 ยท (2 + 1))C(2 + 1))
62 bcp1ctr 26782 . . . . . . . . 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 12275 . . . . . . . . . . . 12 2 = (1 + 1)
6564oveq2i 7420 . . . . . . . . . . 11 (2 ยท 2) = (2 ยท (1 + 1))
6665, 64oveq12i 7421 . . . . . . . . . 10 ((2 ยท 2)C2) = ((2 ยท (1 + 1))C(1 + 1))
67 1nn0 12488 . . . . . . . . . . 11 1 โˆˆ โ„•0
68 bcp1ctr 26782 . . . . . . . . . . 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 12719 . . . . . . . . . . . . . . 15 1 = (0 + 1)
7170oveq2i 7420 . . . . . . . . . . . . . 14 (2 ยท 1) = (2 ยท (0 + 1))
7271, 70oveq12i 7421 . . . . . . . . . . . . 13 ((2 ยท 1)C1) = ((2 ยท (0 + 1))C(0 + 1))
73 bcp1ctr 26782 . . . . . . . . . . . . . 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 12510 . . . . . . . . . . . . . . . 16 (2 ยท 0) โˆˆ โ„•0
76 bcn0 14270 . . . . . . . . . . . . . . . 16 ((2 ยท 0) โˆˆ โ„•0 โ†’ ((2 ยท 0)C0) = 1)
7775, 76ax-mp 5 . . . . . . . . . . . . . . 15 ((2 ยท 0)C0) = 1
78 2t0e0 12381 . . . . . . . . . . . . . . . . . . . . 21 (2 ยท 0) = 0
7978oveq1i 7419 . . . . . . . . . . . . . . . . . . . 20 ((2 ยท 0) + 1) = (0 + 1)
8079, 70eqtr4i 2764 . . . . . . . . . . . . . . . . . . 19 ((2 ยท 0) + 1) = 1
8170eqcomi 2742 . . . . . . . . . . . . . . . . . . 19 (0 + 1) = 1
8280, 81oveq12i 7421 . . . . . . . . . . . . . . . . . 18 (((2 ยท 0) + 1) / (0 + 1)) = (1 / 1)
83 1div1e1 11904 . . . . . . . . . . . . . . . . . 18 (1 / 1) = 1
8482, 83eqtri 2761 . . . . . . . . . . . . . . . . 17 (((2 ยท 0) + 1) / (0 + 1)) = 1
8584oveq2i 7420 . . . . . . . . . . . . . . . 16 (2 ยท (((2 ยท 0) + 1) / (0 + 1))) = (2 ยท 1)
86 2t1e2 12375 . . . . . . . . . . . . . . . 16 (2 ยท 1) = 2
8785, 86eqtri 2761 . . . . . . . . . . . . . . 15 (2 ยท (((2 ยท 0) + 1) / (0 + 1))) = 2
8877, 87oveq12i 7421 . . . . . . . . . . . . . 14 (((2 ยท 0)C0) ยท (2 ยท (((2 ยท 0) + 1) / (0 + 1)))) = (1 ยท 2)
8932mullidi 11219 . . . . . . . . . . . . . 14 (1 ยท 2) = 2
9088, 89eqtri 2761 . . . . . . . . . . . . 13 (((2 ยท 0)C0) ยท (2 ยท (((2 ยท 0) + 1) / (0 + 1)))) = 2
9172, 74, 903eqtri 2765 . . . . . . . . . . . 12 ((2 ยท 1)C1) = 2
9286oveq1i 7419 . . . . . . . . . . . . . . . 16 ((2 ยท 1) + 1) = (2 + 1)
9392, 59eqtr4i 2764 . . . . . . . . . . . . . . 15 ((2 ยท 1) + 1) = 3
9464eqcomi 2742 . . . . . . . . . . . . . . 15 (1 + 1) = 2
9593, 94oveq12i 7421 . . . . . . . . . . . . . 14 (((2 ยท 1) + 1) / (1 + 1)) = (3 / 2)
9695oveq2i 7420 . . . . . . . . . . . . 13 (2 ยท (((2 ยท 1) + 1) / (1 + 1))) = (2 ยท (3 / 2))
97 2ne0 12316 . . . . . . . . . . . . . 14 2 โ‰  0
9842, 32, 97divcan2i 11957 . . . . . . . . . . . . 13 (2 ยท (3 / 2)) = 3
9996, 98eqtri 2761 . . . . . . . . . . . 12 (2 ยท (((2 ยท 1) + 1) / (1 + 1))) = 3
10091, 99oveq12i 7421 . . . . . . . . . . 11 (((2 ยท 1)C1) ยท (2 ยท (((2 ยท 1) + 1) / (1 + 1)))) = (2 ยท 3)
101100, 44eqtri 2761 . . . . . . . . . 10 (((2 ยท 1)C1) ยท (2 ยท (((2 ยท 1) + 1) / (1 + 1)))) = 6
10266, 69, 1013eqtri 2765 . . . . . . . . 9 ((2 ยท 2)C2) = 6
103 2t2e4 12376 . . . . . . . . . . . . . 14 (2 ยท 2) = 4
104103oveq1i 7419 . . . . . . . . . . . . 13 ((2 ยท 2) + 1) = (4 + 1)
105 df-5 12278 . . . . . . . . . . . . 13 5 = (4 + 1)
106104, 105eqtr4i 2764 . . . . . . . . . . . 12 ((2 ยท 2) + 1) = 5
10759eqcomi 2742 . . . . . . . . . . . 12 (2 + 1) = 3
108106, 107oveq12i 7421 . . . . . . . . . . 11 (((2 ยท 2) + 1) / (2 + 1)) = (5 / 3)
109108oveq2i 7420 . . . . . . . . . 10 (2 ยท (((2 ยท 2) + 1) / (2 + 1))) = (2 ยท (5 / 3))
110 5cn 12300 . . . . . . . . . . 11 5 โˆˆ โ„‚
111 3ne0 12318 . . . . . . . . . . 11 3 โ‰  0
11232, 110, 42, 111divassi 11970 . . . . . . . . . 10 ((2 ยท 5) / 3) = (2 ยท (5 / 3))
113109, 112eqtr4i 2764 . . . . . . . . 9 (2 ยท (((2 ยท 2) + 1) / (2 + 1))) = ((2 ยท 5) / 3)
114102, 113oveq12i 7421 . . . . . . . 8 (((2 ยท 2)C2) ยท (2 ยท (((2 ยท 2) + 1) / (2 + 1)))) = (6 ยท ((2 ยท 5) / 3))
11563, 114eqtri 2761 . . . . . . 7 ((2 ยท (2 + 1))C(2 + 1)) = (6 ยท ((2 ยท 5) / 3))
116 6cn 12303 . . . . . . . . 9 6 โˆˆ โ„‚
117 2nn 12285 . . . . . . . . . . 11 2 โˆˆ โ„•
118 5nn 12298 . . . . . . . . . . 11 5 โˆˆ โ„•
119117, 118nnmulcli 12237 . . . . . . . . . 10 (2 ยท 5) โˆˆ โ„•
120119nncni 12222 . . . . . . . . 9 (2 ยท 5) โˆˆ โ„‚
12142, 111pm3.2i 472 . . . . . . . . 9 (3 โˆˆ โ„‚ โˆง 3 โ‰  0)
122 div12 11894 . . . . . . . . 9 ((6 โˆˆ โ„‚ โˆง (2 ยท 5) โˆˆ โ„‚ โˆง (3 โˆˆ โ„‚ โˆง 3 โ‰  0)) โ†’ (6 ยท ((2 ยท 5) / 3)) = ((2 ยท 5) ยท (6 / 3)))
123116, 120, 121, 122mp3an 1462 . . . . . . . 8 (6 ยท ((2 ยท 5) / 3)) = ((2 ยท 5) ยท (6 / 3))
124 5t2e10 12777 . . . . . . . . . 10 (5 ยท 2) = 10
125110, 32, 124mulcomli 11223 . . . . . . . . 9 (2 ยท 5) = 10
126116, 42, 32, 111divmuli 11968 . . . . . . . . . 10 ((6 / 3) = 2 โ†” (3 ยท 2) = 6)
12743, 126mpbir 230 . . . . . . . . 9 (6 / 3) = 2
128125, 127oveq12i 7421 . . . . . . . 8 ((2 ยท 5) ยท (6 / 3)) = (10 ยท 2)
129123, 128eqtri 2761 . . . . . . 7 (6 ยท ((2 ยท 5) / 3)) = (10 ยท 2)
13061, 115, 1293eqtri 2765 . . . . . 6 ((2 ยท 3)C3) = (10 ยท 2)
13144oveq1i 7419 . . . . . . . . 9 ((2 ยท 3) + 1) = (6 + 1)
132 df-7 12280 . . . . . . . . 9 7 = (6 + 1)
133131, 132eqtr4i 2764 . . . . . . . 8 ((2 ยท 3) + 1) = 7
134 3p1e4 12357 . . . . . . . 8 (3 + 1) = 4
135133, 134oveq12i 7421 . . . . . . 7 (((2 ยท 3) + 1) / (3 + 1)) = (7 / 4)
136135oveq2i 7420 . . . . . 6 (2 ยท (((2 ยท 3) + 1) / (3 + 1))) = (2 ยท (7 / 4))
137130, 136oveq12i 7421 . . . . 5 (((2 ยท 3)C3) ยท (2 ยท (((2 ยท 3) + 1) / (3 + 1)))) = ((10 ยท 2) ยท (2 ยท (7 / 4)))
13856, 58, 1373eqtri 2765 . . . 4 ((2 ยท 4)C4) = ((10 ยท 2) ยท (2 ยท (7 / 4)))
139 10nn 12693 . . . . . . 7 10 โˆˆ โ„•
140139nncni 12222 . . . . . 6 10 โˆˆ โ„‚
141 7cn 12306 . . . . . . . 8 7 โˆˆ โ„‚
142141, 48, 49divcli 11956 . . . . . . 7 (7 / 4) โˆˆ โ„‚
14332, 142mulcli 11221 . . . . . 6 (2 ยท (7 / 4)) โˆˆ โ„‚
144140, 32, 143mulassi 11225 . . . . 5 ((10 ยท 2) ยท (2 ยท (7 / 4))) = (10 ยท (2 ยท (2 ยท (7 / 4))))
145103oveq1i 7419 . . . . . . 7 ((2 ยท 2) ยท (7 / 4)) = (4 ยท (7 / 4))
14632, 32, 142mulassi 11225 . . . . . . 7 ((2 ยท 2) ยท (7 / 4)) = (2 ยท (2 ยท (7 / 4)))
147141, 48, 49divcan2i 11957 . . . . . . 7 (4 ยท (7 / 4)) = 7
148145, 146, 1473eqtr3i 2769 . . . . . 6 (2 ยท (2 ยท (7 / 4))) = 7
149148oveq2i 7420 . . . . 5 (10 ยท (2 ยท (2 ยท (7 / 4)))) = (10 ยท 7)
150144, 149eqtri 2761 . . . 4 ((10 ยท 2) ยท (2 ยท (7 / 4))) = (10 ยท 7)
15126dec0u 12698 . . . 4 (10 ยท 7) = 70
152138, 150, 1513eqtri 2765 . . 3 ((2 ยท 4)C4) = 70
15331, 53, 1523brtr4i 5179 . 2 ((4โ†‘4) / 4) < ((2 ยท 4)C4)
154 4nn 12295 . . . 4 4 โˆˆ โ„•
155 eluznn 12902 . . . 4 ((4 โˆˆ โ„• โˆง ๐‘› โˆˆ (โ„คโ‰ฅโ€˜4)) โ†’ ๐‘› โˆˆ โ„•)
156154, 155mpan 689 . . 3 (๐‘› โˆˆ (โ„คโ‰ฅโ€˜4) โ†’ ๐‘› โˆˆ โ„•)
157 nnnn0 12479 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ ๐‘› โˆˆ โ„•0)
158 nnexpcl 14040 . . . . . . . . . 10 ((4 โˆˆ โ„• โˆง ๐‘› โˆˆ โ„•0) โ†’ (4โ†‘๐‘›) โˆˆ โ„•)
159154, 157, 158sylancr 588 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (4โ†‘๐‘›) โˆˆ โ„•)
160159nnrpd 13014 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (4โ†‘๐‘›) โˆˆ โ„+)
161 nnrp 12985 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ ๐‘› โˆˆ โ„+)
162160, 161rpdivcld 13033 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ ((4โ†‘๐‘›) / ๐‘›) โˆˆ โ„+)
163162rpred 13016 . . . . . 6 (๐‘› โˆˆ โ„• โ†’ ((4โ†‘๐‘›) / ๐‘›) โˆˆ โ„)
164 nnmulcl 12236 . . . . . . . . . 10 ((2 โˆˆ โ„• โˆง ๐‘› โˆˆ โ„•) โ†’ (2 ยท ๐‘›) โˆˆ โ„•)
165117, 164mpan 689 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (2 ยท ๐‘›) โˆˆ โ„•)
166165nnnn0d 12532 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (2 ยท ๐‘›) โˆˆ โ„•0)
167 nnz 12579 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ ๐‘› โˆˆ โ„ค)
168 bccl 14282 . . . . . . . 8 (((2 ยท ๐‘›) โˆˆ โ„•0 โˆง ๐‘› โˆˆ โ„ค) โ†’ ((2 ยท ๐‘›)C๐‘›) โˆˆ โ„•0)
169166, 167, 168syl2anc 585 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ ((2 ยท ๐‘›)C๐‘›) โˆˆ โ„•0)
170169nn0red 12533 . . . . . 6 (๐‘› โˆˆ โ„• โ†’ ((2 ยท ๐‘›)C๐‘›) โˆˆ โ„)
171 2rp 12979 . . . . . . 7 2 โˆˆ โ„+
172165peano2nnd 12229 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ ((2 ยท ๐‘›) + 1) โˆˆ โ„•)
173172nnrpd 13014 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ ((2 ยท ๐‘›) + 1) โˆˆ โ„+)
174 peano2nn 12224 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (๐‘› + 1) โˆˆ โ„•)
175174nnrpd 13014 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (๐‘› + 1) โˆˆ โ„+)
176173, 175rpdivcld 13033 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ (((2 ยท ๐‘›) + 1) / (๐‘› + 1)) โˆˆ โ„+)
177 rpmulcl 12997 . . . . . . 7 ((2 โˆˆ โ„+ โˆง (((2 ยท ๐‘›) + 1) / (๐‘› + 1)) โˆˆ โ„+) โ†’ (2 ยท (((2 ยท ๐‘›) + 1) / (๐‘› + 1))) โˆˆ โ„+)
178171, 176, 177sylancr 588 . . . . . 6 (๐‘› โˆˆ โ„• โ†’ (2 ยท (((2 ยท ๐‘›) + 1) / (๐‘› + 1))) โˆˆ โ„+)
179163, 170, 178ltmul1d 13057 . . . . 5 (๐‘› โˆˆ โ„• โ†’ (((4โ†‘๐‘›) / ๐‘›) < ((2 ยท ๐‘›)C๐‘›) โ†” (((4โ†‘๐‘›) / ๐‘›) ยท (2 ยท (((2 ยท ๐‘›) + 1) / (๐‘› + 1)))) < (((2 ยท ๐‘›)C๐‘›) ยท (2 ยท (((2 ยท ๐‘›) + 1) / (๐‘› + 1))))))
180 bcp1ctr 26782 . . . . . . 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 5161 . . . . 5 (๐‘› โˆˆ โ„• โ†’ ((((4โ†‘๐‘›) / ๐‘›) ยท (2 ยท (((2 ยท ๐‘›) + 1) / (๐‘› + 1)))) < ((2 ยท (๐‘› + 1))C(๐‘› + 1)) โ†” (((4โ†‘๐‘›) / ๐‘›) ยท (2 ยท (((2 ยท ๐‘›) + 1) / (๐‘› + 1)))) < (((2 ยท ๐‘›)C๐‘›) ยท (2 ยท (((2 ยท ๐‘›) + 1) / (๐‘› + 1))))))
183179, 182bitr4d 282 . . . 4 (๐‘› โˆˆ โ„• โ†’ (((4โ†‘๐‘›) / ๐‘›) < ((2 ยท ๐‘›)C๐‘›) โ†” (((4โ†‘๐‘›) / ๐‘›) ยท (2 ยท (((2 ยท ๐‘›) + 1) / (๐‘› + 1)))) < ((2 ยท (๐‘› + 1))C(๐‘› + 1))))
184 2re 12286 . . . . . . . 8 2 โˆˆ โ„
185184a1i 11 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ 2 โˆˆ โ„)
186173, 161rpdivcld 13033 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (((2 ยท ๐‘›) + 1) / ๐‘›) โˆˆ โ„+)
187186rpred 13016 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ (((2 ยท ๐‘›) + 1) / ๐‘›) โˆˆ โ„)
188 nnmulcl 12236 . . . . . . . . . 10 (((4โ†‘๐‘›) โˆˆ โ„• โˆง 2 โˆˆ โ„•) โ†’ ((4โ†‘๐‘›) ยท 2) โˆˆ โ„•)
189159, 117, 188sylancl 587 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ ((4โ†‘๐‘›) ยท 2) โˆˆ โ„•)
190189nnrpd 13014 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ ((4โ†‘๐‘›) ยท 2) โˆˆ โ„+)
191190, 175rpdivcld 13033 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ (((4โ†‘๐‘›) ยท 2) / (๐‘› + 1)) โˆˆ โ„+)
192161rpreccld 13026 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (1 / ๐‘›) โˆˆ โ„+)
193 ltaddrp 13011 . . . . . . . . 9 ((2 โˆˆ โ„ โˆง (1 / ๐‘›) โˆˆ โ„+) โ†’ 2 < (2 + (1 / ๐‘›)))
194184, 192, 193sylancr 588 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ 2 < (2 + (1 / ๐‘›)))
195165nncnd 12228 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ (2 ยท ๐‘›) โˆˆ โ„‚)
196 1cnd 11209 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ 1 โˆˆ โ„‚)
197 nncn 12220 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ ๐‘› โˆˆ โ„‚)
198 nnne0 12246 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ ๐‘› โ‰  0)
199195, 196, 197, 198divdird 12028 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (((2 ยท ๐‘›) + 1) / ๐‘›) = (((2 ยท ๐‘›) / ๐‘›) + (1 / ๐‘›)))
20032a1i 11 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ 2 โˆˆ โ„‚)
201200, 197, 198divcan4d 11996 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ ((2 ยท ๐‘›) / ๐‘›) = 2)
202201oveq1d 7424 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (((2 ยท ๐‘›) / ๐‘›) + (1 / ๐‘›)) = (2 + (1 / ๐‘›)))
203199, 202eqtr2d 2774 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (2 + (1 / ๐‘›)) = (((2 ยท ๐‘›) + 1) / ๐‘›))
204194, 203breqtrd 5175 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ 2 < (((2 ยท ๐‘›) + 1) / ๐‘›))
205185, 187, 191, 204ltmul2dd 13072 . . . . . 6 (๐‘› โˆˆ โ„• โ†’ ((((4โ†‘๐‘›) ยท 2) / (๐‘› + 1)) ยท 2) < ((((4โ†‘๐‘›) ยท 2) / (๐‘› + 1)) ยท (((2 ยท ๐‘›) + 1) / ๐‘›)))
206 expp1 14034 . . . . . . . . . 10 ((4 โˆˆ โ„‚ โˆง ๐‘› โˆˆ โ„•0) โ†’ (4โ†‘(๐‘› + 1)) = ((4โ†‘๐‘›) ยท 4))
20748, 157, 206sylancr 588 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (4โ†‘(๐‘› + 1)) = ((4โ†‘๐‘›) ยท 4))
208159nncnd 12228 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ (4โ†‘๐‘›) โˆˆ โ„‚)
209208, 200, 200mulassd 11237 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ (((4โ†‘๐‘›) ยท 2) ยท 2) = ((4โ†‘๐‘›) ยท (2 ยท 2)))
210103oveq2i 7420 . . . . . . . . . 10 ((4โ†‘๐‘›) ยท (2 ยท 2)) = ((4โ†‘๐‘›) ยท 4)
211209, 210eqtrdi 2789 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (((4โ†‘๐‘›) ยท 2) ยท 2) = ((4โ†‘๐‘›) ยท 4))
212207, 211eqtr4d 2776 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (4โ†‘(๐‘› + 1)) = (((4โ†‘๐‘›) ยท 2) ยท 2))
213212oveq1d 7424 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ ((4โ†‘(๐‘› + 1)) / (๐‘› + 1)) = ((((4โ†‘๐‘›) ยท 2) ยท 2) / (๐‘› + 1)))
214189nncnd 12228 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ ((4โ†‘๐‘›) ยท 2) โˆˆ โ„‚)
215174nncnd 12228 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (๐‘› + 1) โˆˆ โ„‚)
216174nnne0d 12262 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (๐‘› + 1) โ‰  0)
217214, 200, 215, 216div23d 12027 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ ((((4โ†‘๐‘›) ยท 2) ยท 2) / (๐‘› + 1)) = ((((4โ†‘๐‘›) ยท 2) / (๐‘› + 1)) ยท 2))
218213, 217eqtrd 2773 . . . . . 6 (๐‘› โˆˆ โ„• โ†’ ((4โ†‘(๐‘› + 1)) / (๐‘› + 1)) = ((((4โ†‘๐‘›) ยท 2) / (๐‘› + 1)) ยท 2))
219208, 200, 197, 198div23d 12027 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (((4โ†‘๐‘›) ยท 2) / ๐‘›) = (((4โ†‘๐‘›) / ๐‘›) ยท 2))
220219oveq1d 7424 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ ((((4โ†‘๐‘›) ยท 2) / ๐‘›) ยท (((2 ยท ๐‘›) + 1) / (๐‘› + 1))) = ((((4โ†‘๐‘›) / ๐‘›) ยท 2) ยท (((2 ยท ๐‘›) + 1) / (๐‘› + 1))))
221172nncnd 12228 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ ((2 ยท ๐‘›) + 1) โˆˆ โ„‚)
222214, 197, 221, 215, 198, 216divmul24d 12033 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ ((((4โ†‘๐‘›) ยท 2) / ๐‘›) ยท (((2 ยท ๐‘›) + 1) / (๐‘› + 1))) = ((((4โ†‘๐‘›) ยท 2) / (๐‘› + 1)) ยท (((2 ยท ๐‘›) + 1) / ๐‘›)))
223162rpcnd 13018 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ ((4โ†‘๐‘›) / ๐‘›) โˆˆ โ„‚)
224176rpcnd 13018 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (((2 ยท ๐‘›) + 1) / (๐‘› + 1)) โˆˆ โ„‚)
225223, 200, 224mulassd 11237 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ ((((4โ†‘๐‘›) / ๐‘›) ยท 2) ยท (((2 ยท ๐‘›) + 1) / (๐‘› + 1))) = (((4โ†‘๐‘›) / ๐‘›) ยท (2 ยท (((2 ยท ๐‘›) + 1) / (๐‘› + 1)))))
226220, 222, 2253eqtr3rd 2782 . . . . . 6 (๐‘› โˆˆ โ„• โ†’ (((4โ†‘๐‘›) / ๐‘›) ยท (2 ยท (((2 ยท ๐‘›) + 1) / (๐‘› + 1)))) = ((((4โ†‘๐‘›) ยท 2) / (๐‘› + 1)) ยท (((2 ยท ๐‘›) + 1) / ๐‘›)))
227205, 218, 2263brtr4d 5181 . . . . 5 (๐‘› โˆˆ โ„• โ†’ ((4โ†‘(๐‘› + 1)) / (๐‘› + 1)) < (((4โ†‘๐‘›) / ๐‘›) ยท (2 ยท (((2 ยท ๐‘›) + 1) / (๐‘› + 1)))))
228174nnnn0d 12532 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†’ (๐‘› + 1) โˆˆ โ„•0)
229 nnexpcl 14040 . . . . . . . . . 10 ((4 โˆˆ โ„• โˆง (๐‘› + 1) โˆˆ โ„•0) โ†’ (4โ†‘(๐‘› + 1)) โˆˆ โ„•)
230154, 228, 229sylancr 588 . . . . . . . . 9 (๐‘› โˆˆ โ„• โ†’ (4โ†‘(๐‘› + 1)) โˆˆ โ„•)
231230nnrpd 13014 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (4โ†‘(๐‘› + 1)) โˆˆ โ„+)
232231, 175rpdivcld 13033 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ ((4โ†‘(๐‘› + 1)) / (๐‘› + 1)) โˆˆ โ„+)
233232rpred 13016 . . . . . 6 (๐‘› โˆˆ โ„• โ†’ ((4โ†‘(๐‘› + 1)) / (๐‘› + 1)) โˆˆ โ„)
234178rpred 13016 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ (2 ยท (((2 ยท ๐‘›) + 1) / (๐‘› + 1))) โˆˆ โ„)
235163, 234remulcld 11244 . . . . . 6 (๐‘› โˆˆ โ„• โ†’ (((4โ†‘๐‘›) / ๐‘›) ยท (2 ยท (((2 ยท ๐‘›) + 1) / (๐‘› + 1)))) โˆˆ โ„)
236 nn0mulcl 12508 . . . . . . . . 9 ((2 โˆˆ โ„•0 โˆง (๐‘› + 1) โˆˆ โ„•0) โ†’ (2 ยท (๐‘› + 1)) โˆˆ โ„•0)
23733, 228, 236sylancr 588 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (2 ยท (๐‘› + 1)) โˆˆ โ„•0)
238174nnzd 12585 . . . . . . . 8 (๐‘› โˆˆ โ„• โ†’ (๐‘› + 1) โˆˆ โ„ค)
239 bccl 14282 . . . . . . . 8 (((2 ยท (๐‘› + 1)) โˆˆ โ„•0 โˆง (๐‘› + 1) โˆˆ โ„ค) โ†’ ((2 ยท (๐‘› + 1))C(๐‘› + 1)) โˆˆ โ„•0)
240237, 238, 239syl2anc 585 . . . . . . 7 (๐‘› โˆˆ โ„• โ†’ ((2 ยท (๐‘› + 1))C(๐‘› + 1)) โˆˆ โ„•0)
241240nn0red 12533 . . . . . 6 (๐‘› โˆˆ โ„• โ†’ ((2 ยท (๐‘› + 1))C(๐‘› + 1)) โˆˆ โ„)
242 lttr 11290 . . . . . 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 1372 . . . . 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 239 . . 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 12894 1 (๐‘ โˆˆ (โ„คโ‰ฅโ€˜4) โ†’ ((4โ†‘๐‘) / ๐‘) < ((2 ยท ๐‘)C๐‘))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โˆง wa 397   = wceq 1542   โˆˆ wcel 2107   โ‰  wne 2941   class class class wbr 5149  โ€˜cfv 6544  (class class class)co 7409  โ„‚cc 11108  โ„cr 11109  0cc0 11110  1c1 11111   + caddc 11113   ยท cmul 11115   < clt 11248   โˆ’ cmin 11444   / cdiv 11871  โ„•cn 12212  2c2 12267  3c3 12268  4c4 12269  5c5 12270  6c6 12271  7c7 12272  โ„•0cn0 12472  โ„คcz 12558  cdc 12677  โ„คโ‰ฅcuz 12822  โ„+crp 12974  โ†‘cexp 14027  Ccbc 14262
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-1st 7975  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-er 8703  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-div 11872  df-nn 12213  df-2 12275  df-3 12276  df-4 12277  df-5 12278  df-6 12279  df-7 12280  df-8 12281  df-9 12282  df-n0 12473  df-z 12559  df-dec 12678  df-uz 12823  df-rp 12975  df-fz 13485  df-seq 13967  df-exp 14028  df-fac 14234  df-bc 14263
This theorem is referenced by:  bposlem6  26792  chebbnd1lem1  26972
  Copyright terms: Public domain W3C validator