Step | Hyp | Ref
| Expression |
1 | | oveq1 7365 |
. . . 4
โข (๐ = 2 โ (๐ + 1) = (2 + 1)) |
2 | 1 | oveq2d 7374 |
. . 3
โข (๐ = 2 โ (2โ(๐ + 1)) = (2โ(2 +
1))) |
3 | | oveq2 7366 |
. . . . 5
โข (๐ = 2 โ (2 ยท ๐) = (2 ยท
2)) |
4 | 3 | oveq1d 7373 |
. . . 4
โข (๐ = 2 โ ((2 ยท ๐) + 1) = ((2 ยท 2) +
1)) |
5 | | id 22 |
. . . 4
โข (๐ = 2 โ ๐ = 2) |
6 | 4, 5 | oveq12d 7376 |
. . 3
โข (๐ = 2 โ (((2 ยท ๐) + 1)C๐) = (((2 ยท 2) +
1)C2)) |
7 | 2, 6 | breq12d 5119 |
. 2
โข (๐ = 2 โ ((2โ(๐ + 1)) < (((2 ยท ๐) + 1)C๐) โ (2โ(2 + 1)) < (((2 ยท
2) + 1)C2))) |
8 | | oveq1 7365 |
. . . 4
โข (๐ = ๐ โ (๐ + 1) = (๐ + 1)) |
9 | 8 | oveq2d 7374 |
. . 3
โข (๐ = ๐ โ (2โ(๐ + 1)) = (2โ(๐ + 1))) |
10 | | oveq2 7366 |
. . . . 5
โข (๐ = ๐ โ (2 ยท ๐) = (2 ยท ๐)) |
11 | 10 | oveq1d 7373 |
. . . 4
โข (๐ = ๐ โ ((2 ยท ๐) + 1) = ((2 ยท ๐) + 1)) |
12 | | id 22 |
. . . 4
โข (๐ = ๐ โ ๐ = ๐) |
13 | 11, 12 | oveq12d 7376 |
. . 3
โข (๐ = ๐ โ (((2 ยท ๐) + 1)C๐) = (((2 ยท ๐) + 1)C๐)) |
14 | 9, 13 | breq12d 5119 |
. 2
โข (๐ = ๐ โ ((2โ(๐ + 1)) < (((2 ยท ๐) + 1)C๐) โ (2โ(๐ + 1)) < (((2 ยท ๐) + 1)C๐))) |
15 | | oveq1 7365 |
. . . 4
โข (๐ = (๐ + 1) โ (๐ + 1) = ((๐ + 1) + 1)) |
16 | 15 | oveq2d 7374 |
. . 3
โข (๐ = (๐ + 1) โ (2โ(๐ + 1)) = (2โ((๐ + 1) + 1))) |
17 | | oveq2 7366 |
. . . . 5
โข (๐ = (๐ + 1) โ (2 ยท ๐) = (2 ยท (๐ + 1))) |
18 | 17 | oveq1d 7373 |
. . . 4
โข (๐ = (๐ + 1) โ ((2 ยท ๐) + 1) = ((2 ยท (๐ + 1)) + 1)) |
19 | | id 22 |
. . . 4
โข (๐ = (๐ + 1) โ ๐ = (๐ + 1)) |
20 | 18, 19 | oveq12d 7376 |
. . 3
โข (๐ = (๐ + 1) โ (((2 ยท ๐) + 1)C๐) = (((2 ยท (๐ + 1)) + 1)C(๐ + 1))) |
21 | 16, 20 | breq12d 5119 |
. 2
โข (๐ = (๐ + 1) โ ((2โ(๐ + 1)) < (((2 ยท ๐) + 1)C๐) โ (2โ((๐ + 1) + 1)) < (((2 ยท (๐ + 1)) + 1)C(๐ + 1)))) |
22 | | oveq1 7365 |
. . . 4
โข (๐ = ๐ โ (๐ + 1) = (๐ + 1)) |
23 | 22 | oveq2d 7374 |
. . 3
โข (๐ = ๐ โ (2โ(๐ + 1)) = (2โ(๐ + 1))) |
24 | | oveq2 7366 |
. . . . 5
โข (๐ = ๐ โ (2 ยท ๐) = (2 ยท ๐)) |
25 | 24 | oveq1d 7373 |
. . . 4
โข (๐ = ๐ โ ((2 ยท ๐) + 1) = ((2 ยท ๐) + 1)) |
26 | | id 22 |
. . . 4
โข (๐ = ๐ โ ๐ = ๐) |
27 | 25, 26 | oveq12d 7376 |
. . 3
โข (๐ = ๐ โ (((2 ยท ๐) + 1)C๐) = (((2 ยท ๐) + 1)C๐)) |
28 | 23, 27 | breq12d 5119 |
. 2
โข (๐ = ๐ โ ((2โ(๐ + 1)) < (((2 ยท ๐) + 1)C๐) โ (2โ(๐ + 1)) < (((2 ยท ๐) + 1)C๐))) |
29 | | 8lt10 12755 |
. . . . 5
โข 8 <
;10 |
30 | | eqid 2733 |
. . . . . . 7
โข 8 =
8 |
31 | | cu2 14110 |
. . . . . . 7
โข
(2โ3) = 8 |
32 | 30, 31 | eqtr4i 2764 |
. . . . . 6
โข 8 =
(2โ3) |
33 | | 5bc2eq10 40596 |
. . . . . . 7
โข (5C2) =
;10 |
34 | 33 | eqcomi 2742 |
. . . . . 6
โข ;10 = (5C2) |
35 | 32, 34 | breq12i 5115 |
. . . . 5
โข (8 <
;10 โ (2โ3) <
(5C2)) |
36 | 29, 35 | mpbi 229 |
. . . 4
โข
(2โ3) < (5C2) |
37 | | df-3 12222 |
. . . . . 6
โข 3 = (2 +
1) |
38 | 37 | oveq2i 7369 |
. . . . 5
โข
(2โ3) = (2โ(2 + 1)) |
39 | | eqid 2733 |
. . . . . . 7
โข 5 =
5 |
40 | | 2t2e4 12322 |
. . . . . . . . 9
โข (2
ยท 2) = 4 |
41 | 40 | oveq1i 7368 |
. . . . . . . 8
โข ((2
ยท 2) + 1) = (4 + 1) |
42 | | 4p1e5 12304 |
. . . . . . . 8
โข (4 + 1) =
5 |
43 | 41, 42 | eqtri 2761 |
. . . . . . 7
โข ((2
ยท 2) + 1) = 5 |
44 | 39, 43 | eqtr4i 2764 |
. . . . . 6
โข 5 = ((2
ยท 2) + 1) |
45 | 44 | oveq1i 7368 |
. . . . 5
โข (5C2) =
(((2 ยท 2) + 1)C2) |
46 | 38, 45 | breq12i 5115 |
. . . 4
โข
((2โ3) < (5C2) โ (2โ(2 + 1)) < (((2 ยท 2) +
1)C2)) |
47 | 36, 46 | mpbi 229 |
. . 3
โข
(2โ(2 + 1)) < (((2 ยท 2) + 1)C2) |
48 | 47 | a1i 11 |
. 2
โข (๐ โ (2โ(2 + 1)) < (((2
ยท 2) + 1)C2)) |
49 | | 2re 12232 |
. . . . 5
โข 2 โ
โ |
50 | 49 | a1i 11 |
. . . 4
โข ((๐ โง (2โ(๐ + 1)) < (((2 ยท ๐) + 1)C๐) โง (๐ โ โค โง 2 โค ๐)) โ 2 โ
โ) |
51 | | simpl 484 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง 2 โค
๐) โ ๐ โ
โค) |
52 | | 0red 11163 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โง 2 โค
๐) โ 0 โ
โ) |
53 | 49 | a1i 11 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โง 2 โค
๐) โ 2 โ
โ) |
54 | 51 | zred 12612 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โค โง 2 โค
๐) โ ๐ โ
โ) |
55 | | 2pos 12261 |
. . . . . . . . . . . . . . . . . . 19
โข 0 <
2 |
56 | 55 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โค โง 2 โค
๐) โ 0 <
2) |
57 | | simpr 486 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โค โง 2 โค
๐) โ 2 โค ๐) |
58 | 52, 53, 54, 56, 57 | ltletrd 11320 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โค โง 2 โค
๐) โ 0 < ๐) |
59 | 51, 58 | jca 513 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โค โง 2 โค
๐) โ (๐ โ โค โง 0 <
๐)) |
60 | | elnnz 12514 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ (๐ โ โค โง 0 <
๐)) |
61 | 59, 60 | sylibr 233 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โค โง 2 โค
๐) โ ๐ โ
โ) |
62 | | nnnn0 12425 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ ๐ โ
โ0) |
63 | 61, 62 | syl 17 |
. . . . . . . . . . . . . 14
โข ((๐ โ โค โง 2 โค
๐) โ ๐ โ
โ0) |
64 | 63 | nn0red 12479 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โง 2 โค
๐) โ ๐ โ
โ) |
65 | 52, 53, 64, 56, 57 | ltletrd 11320 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง 2 โค
๐) โ 0 < ๐) |
66 | 51, 65 | jca 513 |
. . . . . . . . . . 11
โข ((๐ โ โค โง 2 โค
๐) โ (๐ โ โค โง 0 <
๐)) |
67 | 66, 60 | sylibr 233 |
. . . . . . . . . 10
โข ((๐ โ โค โง 2 โค
๐) โ ๐ โ
โ) |
68 | 67 | nnred 12173 |
. . . . . . . . 9
โข ((๐ โ โค โง 2 โค
๐) โ ๐ โ
โ) |
69 | 68 | 3ad2ant3 1136 |
. . . . . . . 8
โข ((๐ โง (2โ(๐ + 1)) < (((2 ยท ๐) + 1)C๐) โง (๐ โ โค โง 2 โค ๐)) โ ๐ โ โ) |
70 | 50, 69 | remulcld 11190 |
. . . . . . 7
โข ((๐ โง (2โ(๐ + 1)) < (((2 ยท ๐) + 1)C๐) โง (๐ โ โค โง 2 โค ๐)) โ (2 ยท ๐) โ
โ) |
71 | | 3re 12238 |
. . . . . . . 8
โข 3 โ
โ |
72 | 71 | a1i 11 |
. . . . . . 7
โข ((๐ โง (2โ(๐ + 1)) < (((2 ยท ๐) + 1)C๐) โง (๐ โ โค โง 2 โค ๐)) โ 3 โ
โ) |
73 | 70, 72 | readdcld 11189 |
. . . . . 6
โข ((๐ โง (2โ(๐ + 1)) < (((2 ยท ๐) + 1)C๐) โง (๐ โ โค โง 2 โค ๐)) โ ((2 ยท ๐) + 3) โ
โ) |
74 | 69, 50 | readdcld 11189 |
. . . . . 6
โข ((๐ โง (2โ(๐ + 1)) < (((2 ยท ๐) + 1)C๐) โง (๐ โ โค โง 2 โค ๐)) โ (๐ + 2) โ โ) |
75 | 68, 53 | readdcld 11189 |
. . . . . . . . . 10
โข ((๐ โ โค โง 2 โค
๐) โ (๐ + 2) โ
โ) |
76 | 67 | nngt0d 12207 |
. . . . . . . . . 10
โข ((๐ โ โค โง 2 โค
๐) โ 0 < ๐) |
77 | | 2rp 12925 |
. . . . . . . . . . . 12
โข 2 โ
โ+ |
78 | 77 | a1i 11 |
. . . . . . . . . . 11
โข ((๐ โ โค โง 2 โค
๐) โ 2 โ
โ+) |
79 | 68, 78 | ltaddrpd 12995 |
. . . . . . . . . 10
โข ((๐ โ โค โง 2 โค
๐) โ ๐ < (๐ + 2)) |
80 | 52, 68, 75, 76, 79 | lttrd 11321 |
. . . . . . . . 9
โข ((๐ โ โค โง 2 โค
๐) โ 0 < (๐ + 2)) |
81 | 52, 80 | ltned 11296 |
. . . . . . . 8
โข ((๐ โ โค โง 2 โค
๐) โ 0 โ (๐ + 2)) |
82 | 81 | necomd 2996 |
. . . . . . 7
โข ((๐ โ โค โง 2 โค
๐) โ (๐ + 2) โ 0) |
83 | 82 | 3ad2ant3 1136 |
. . . . . 6
โข ((๐ โง (2โ(๐ + 1)) < (((2 ยท ๐) + 1)C๐) โง (๐ โ โค โง 2 โค ๐)) โ (๐ + 2) โ 0) |
84 | 73, 74, 83 | redivcld 11988 |
. . . . 5
โข ((๐ โง (2โ(๐ + 1)) < (((2 ยท ๐) + 1)C๐) โง (๐ โ โค โง 2 โค ๐)) โ (((2 ยท ๐) + 3) / (๐ + 2)) โ โ) |
85 | 50, 84 | remulcld 11190 |
. . . 4
โข ((๐ โง (2โ(๐ + 1)) < (((2 ยท ๐) + 1)C๐) โง (๐ โ โค โง 2 โค ๐)) โ (2 ยท (((2
ยท ๐) + 3) / (๐ + 2))) โ
โ) |
86 | | 1nn0 12434 |
. . . . . . . 8
โข 1 โ
โ0 |
87 | 86 | a1i 11 |
. . . . . . 7
โข ((๐ โ โค โง 2 โค
๐) โ 1 โ
โ0) |
88 | 63, 87 | nn0addcld 12482 |
. . . . . 6
โข ((๐ โ โค โง 2 โค
๐) โ (๐ + 1) โ
โ0) |
89 | 53, 88 | reexpcld 14074 |
. . . . 5
โข ((๐ โ โค โง 2 โค
๐) โ (2โ(๐ + 1)) โ
โ) |
90 | 89 | 3ad2ant3 1136 |
. . . 4
โข ((๐ โง (2โ(๐ + 1)) < (((2 ยท ๐) + 1)C๐) โง (๐ โ โค โง 2 โค ๐)) โ (2โ(๐ + 1)) โ
โ) |
91 | | 2nn0 12435 |
. . . . . . . . . 10
โข 2 โ
โ0 |
92 | 91 | a1i 11 |
. . . . . . . . 9
โข ((๐ โ โค โง 2 โค
๐) โ 2 โ
โ0) |
93 | 92, 63 | nn0mulcld 12483 |
. . . . . . . 8
โข ((๐ โ โค โง 2 โค
๐) โ (2 ยท ๐) โ
โ0) |
94 | 93, 87 | nn0addcld 12482 |
. . . . . . 7
โข ((๐ โ โค โง 2 โค
๐) โ ((2 ยท
๐) + 1) โ
โ0) |
95 | | bccl 14228 |
. . . . . . 7
โข ((((2
ยท ๐) + 1) โ
โ0 โง ๐
โ โค) โ (((2 ยท ๐) + 1)C๐) โ
โ0) |
96 | 94, 51, 95 | syl2anc 585 |
. . . . . 6
โข ((๐ โ โค โง 2 โค
๐) โ (((2 ยท
๐) + 1)C๐) โ
โ0) |
97 | 96 | nn0red 12479 |
. . . . 5
โข ((๐ โ โค โง 2 โค
๐) โ (((2 ยท
๐) + 1)C๐) โ โ) |
98 | 97 | 3ad2ant3 1136 |
. . . 4
โข ((๐ โง (2โ(๐ + 1)) < (((2 ยท ๐) + 1)C๐) โง (๐ โ โค โง 2 โค ๐)) โ (((2 ยท ๐) + 1)C๐) โ โ) |
99 | | 0le2 12260 |
. . . . 5
โข 0 โค
2 |
100 | 99 | a1i 11 |
. . . 4
โข ((๐ โง (2โ(๐ + 1)) < (((2 ยท ๐) + 1)C๐) โง (๐ โ โค โง 2 โค ๐)) โ 0 โค
2) |
101 | | eqid 2733 |
. . . . . . . 8
โข 2 =
2 |
102 | | 2t1e2 12321 |
. . . . . . . 8
โข (2
ยท 1) = 2 |
103 | 101, 102 | eqtr4i 2764 |
. . . . . . 7
โข 2 = (2
ยท 1) |
104 | 103 | a1i 11 |
. . . . . 6
โข ((๐ โ โค โง 2 โค
๐) โ 2 = (2 ยท
1)) |
105 | | 1red 11161 |
. . . . . . 7
โข ((๐ โ โค โง 2 โค
๐) โ 1 โ
โ) |
106 | 53, 68 | remulcld 11190 |
. . . . . . . . 9
โข ((๐ โ โค โง 2 โค
๐) โ (2 ยท ๐) โ
โ) |
107 | 71 | a1i 11 |
. . . . . . . . 9
โข ((๐ โ โค โง 2 โค
๐) โ 3 โ
โ) |
108 | 106, 107 | readdcld 11189 |
. . . . . . . 8
โข ((๐ โ โค โง 2 โค
๐) โ ((2 ยท
๐) + 3) โ
โ) |
109 | 108, 75, 82 | redivcld 11988 |
. . . . . . 7
โข ((๐ โ โค โง 2 โค
๐) โ (((2 ยท
๐) + 3) / (๐ + 2)) โ
โ) |
110 | | nnrp 12931 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ๐ โ
โ+) |
111 | 77 | a1i 11 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ 2 โ
โ+) |
112 | 110, 111 | rpaddcld 12977 |
. . . . . . . . . . . 12
โข (๐ โ โ โ (๐ + 2) โ
โ+) |
113 | 112 | rpcnd 12964 |
. . . . . . . . . . 11
โข (๐ โ โ โ (๐ + 2) โ
โ) |
114 | 113 | mulid1d 11177 |
. . . . . . . . . 10
โข (๐ โ โ โ ((๐ + 2) ยท 1) = (๐ + 2)) |
115 | | nnre 12165 |
. . . . . . . . . . 11
โข (๐ โ โ โ ๐ โ
โ) |
116 | 49 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ โ โ 2 โ
โ) |
117 | 116, 115 | remulcld 11190 |
. . . . . . . . . . 11
โข (๐ โ โ โ (2
ยท ๐) โ
โ) |
118 | 71 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ โ โ 3 โ
โ) |
119 | 110 | rpge0d 12966 |
. . . . . . . . . . . 12
โข (๐ โ โ โ 0 โค
๐) |
120 | | 1le2 12367 |
. . . . . . . . . . . . 13
โข 1 โค
2 |
121 | 120 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ โ โ 1 โค
2) |
122 | 115, 116,
119, 121 | lemulge12d 12098 |
. . . . . . . . . . 11
โข (๐ โ โ โ ๐ โค (2 ยท ๐)) |
123 | | 2lt3 12330 |
. . . . . . . . . . . 12
โข 2 <
3 |
124 | 123 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ โ โ 2 <
3) |
125 | 115, 116,
117, 118, 122, 124 | leltaddd 11782 |
. . . . . . . . . 10
โข (๐ โ โ โ (๐ + 2) < ((2 ยท ๐) + 3)) |
126 | 114, 125 | eqbrtrd 5128 |
. . . . . . . . 9
โข (๐ โ โ โ ((๐ + 2) ยท 1) < ((2
ยท ๐) +
3)) |
127 | | 1red 11161 |
. . . . . . . . . 10
โข (๐ โ โ โ 1 โ
โ) |
128 | 117, 118 | readdcld 11189 |
. . . . . . . . . 10
โข (๐ โ โ โ ((2
ยท ๐) + 3) โ
โ) |
129 | 127, 128,
112 | ltmuldiv2d 13010 |
. . . . . . . . 9
โข (๐ โ โ โ (((๐ + 2) ยท 1) < ((2
ยท ๐) + 3) โ 1
< (((2 ยท ๐) + 3)
/ (๐ +
2)))) |
130 | 126, 129 | mpbid 231 |
. . . . . . . 8
โข (๐ โ โ โ 1 <
(((2 ยท ๐) + 3) /
(๐ + 2))) |
131 | 67, 130 | syl 17 |
. . . . . . 7
โข ((๐ โ โค โง 2 โค
๐) โ 1 < (((2
ยท ๐) + 3) / (๐ + 2))) |
132 | 105, 109,
78, 131 | ltmul2dd 13018 |
. . . . . 6
โข ((๐ โ โค โง 2 โค
๐) โ (2 ยท 1)
< (2 ยท (((2 ยท ๐) + 3) / (๐ + 2)))) |
133 | 104, 132 | eqbrtrd 5128 |
. . . . 5
โข ((๐ โ โค โง 2 โค
๐) โ 2 < (2
ยท (((2 ยท ๐) +
3) / (๐ +
2)))) |
134 | 133 | 3ad2ant3 1136 |
. . . 4
โข ((๐ โง (2โ(๐ + 1)) < (((2 ยท ๐) + 1)C๐) โง (๐ โ โค โง 2 โค ๐)) โ 2 < (2 ยท
(((2 ยท ๐) + 3) /
(๐ + 2)))) |
135 | 99 | a1i 11 |
. . . . . 6
โข ((๐ โ โค โง 2 โค
๐) โ 0 โค
2) |
136 | 53, 88, 135 | expge0d 14075 |
. . . . 5
โข ((๐ โ โค โง 2 โค
๐) โ 0 โค
(2โ(๐ +
1))) |
137 | 136 | 3ad2ant3 1136 |
. . . 4
โข ((๐ โง (2โ(๐ + 1)) < (((2 ยท ๐) + 1)C๐) โง (๐ โ โค โง 2 โค ๐)) โ 0 โค (2โ(๐ + 1))) |
138 | | simp2 1138 |
. . . 4
โข ((๐ โง (2โ(๐ + 1)) < (((2 ยท ๐) + 1)C๐) โง (๐ โ โค โง 2 โค ๐)) โ (2โ(๐ + 1)) < (((2 ยท ๐) + 1)C๐)) |
139 | 50, 85, 90, 98, 100, 134, 137, 138 | ltmul12ad 12101 |
. . 3
โข ((๐ โง (2โ(๐ + 1)) < (((2 ยท ๐) + 1)C๐) โง (๐ โ โค โง 2 โค ๐)) โ (2 ยท
(2โ(๐ + 1))) < ((2
ยท (((2 ยท ๐) +
3) / (๐ + 2))) ยท
(((2 ยท ๐) + 1)C๐))) |
140 | | 2cnd 12236 |
. . . . . . . 8
โข ((๐ โ โค โง 2 โค
๐) โ 2 โ
โ) |
141 | 140, 87, 88 | expaddd 14059 |
. . . . . . 7
โข ((๐ โ โค โง 2 โค
๐) โ (2โ((๐ + 1) + 1)) = ((2โ(๐ + 1)) ยท
(2โ1))) |
142 | 140, 88 | expcld 14057 |
. . . . . . . . 9
โข ((๐ โ โค โง 2 โค
๐) โ (2โ(๐ + 1)) โ
โ) |
143 | 140, 87 | expcld 14057 |
. . . . . . . . 9
โข ((๐ โ โค โง 2 โค
๐) โ (2โ1) โ
โ) |
144 | 142, 143 | mulcomd 11181 |
. . . . . . . 8
โข ((๐ โ โค โง 2 โค
๐) โ ((2โ(๐ + 1)) ยท (2โ1)) =
((2โ1) ยท (2โ(๐ + 1)))) |
145 | 140 | exp1d 14052 |
. . . . . . . . 9
โข ((๐ โ โค โง 2 โค
๐) โ (2โ1) =
2) |
146 | 145 | oveq1d 7373 |
. . . . . . . 8
โข ((๐ โ โค โง 2 โค
๐) โ ((2โ1)
ยท (2โ(๐ + 1)))
= (2 ยท (2โ(๐ +
1)))) |
147 | | eqidd 2734 |
. . . . . . . 8
โข ((๐ โ โค โง 2 โค
๐) โ (2 ยท
(2โ(๐ + 1))) = (2
ยท (2โ(๐ +
1)))) |
148 | 144, 146,
147 | 3eqtrd 2777 |
. . . . . . 7
โข ((๐ โ โค โง 2 โค
๐) โ ((2โ(๐ + 1)) ยท (2โ1)) = (2
ยท (2โ(๐ +
1)))) |
149 | 141, 148 | eqtrd 2773 |
. . . . . 6
โข ((๐ โ โค โง 2 โค
๐) โ (2โ((๐ + 1) + 1)) = (2 ยท
(2โ(๐ +
1)))) |
150 | 149 | eqcomd 2739 |
. . . . 5
โข ((๐ โ โค โง 2 โค
๐) โ (2 ยท
(2โ(๐ + 1))) =
(2โ((๐ + 1) +
1))) |
151 | 150 | 3ad2ant3 1136 |
. . . 4
โข ((๐ โง (2โ(๐ + 1)) < (((2 ยท ๐) + 1)C๐) โง (๐ โ โค โง 2 โค ๐)) โ (2 ยท
(2โ(๐ + 1))) =
(2โ((๐ + 1) +
1))) |
152 | 63 | 2np3bcnp1 40598 |
. . . . . . 7
โข ((๐ โ โค โง 2 โค
๐) โ (((2 ยท
(๐ + 1)) + 1)C(๐ + 1)) = ((((2 ยท ๐) + 1)C๐) ยท (2 ยท (((2 ยท ๐) + 3) / (๐ + 2))))) |
153 | 96 | nn0cnd 12480 |
. . . . . . . 8
โข ((๐ โ โค โง 2 โค
๐) โ (((2 ยท
๐) + 1)C๐) โ โ) |
154 | 67 | nncnd 12174 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง 2 โค
๐) โ ๐ โ
โ) |
155 | 140, 154 | mulcld 11180 |
. . . . . . . . . . 11
โข ((๐ โ โค โง 2 โค
๐) โ (2 ยท ๐) โ
โ) |
156 | | 3cn 12239 |
. . . . . . . . . . . 12
โข 3 โ
โ |
157 | 156 | a1i 11 |
. . . . . . . . . . 11
โข ((๐ โ โค โง 2 โค
๐) โ 3 โ
โ) |
158 | 155, 157 | addcld 11179 |
. . . . . . . . . 10
โข ((๐ โ โค โง 2 โค
๐) โ ((2 ยท
๐) + 3) โ
โ) |
159 | 154, 140 | addcld 11179 |
. . . . . . . . . 10
โข ((๐ โ โค โง 2 โค
๐) โ (๐ + 2) โ
โ) |
160 | 158, 159,
82 | divcld 11936 |
. . . . . . . . 9
โข ((๐ โ โค โง 2 โค
๐) โ (((2 ยท
๐) + 3) / (๐ + 2)) โ
โ) |
161 | 140, 160 | mulcld 11180 |
. . . . . . . 8
โข ((๐ โ โค โง 2 โค
๐) โ (2 ยท (((2
ยท ๐) + 3) / (๐ + 2))) โ
โ) |
162 | 153, 161 | mulcomd 11181 |
. . . . . . 7
โข ((๐ โ โค โง 2 โค
๐) โ ((((2 ยท
๐) + 1)C๐) ยท (2 ยท (((2 ยท ๐) + 3) / (๐ + 2)))) = ((2 ยท (((2 ยท ๐) + 3) / (๐ + 2))) ยท (((2 ยท ๐) + 1)C๐))) |
163 | 152, 162 | eqtrd 2773 |
. . . . . 6
โข ((๐ โ โค โง 2 โค
๐) โ (((2 ยท
(๐ + 1)) + 1)C(๐ + 1)) = ((2 ยท (((2
ยท ๐) + 3) / (๐ + 2))) ยท (((2 ยท
๐) + 1)C๐))) |
164 | 163 | eqcomd 2739 |
. . . . 5
โข ((๐ โ โค โง 2 โค
๐) โ ((2 ยท (((2
ยท ๐) + 3) / (๐ + 2))) ยท (((2 ยท
๐) + 1)C๐)) = (((2 ยท (๐ + 1)) + 1)C(๐ + 1))) |
165 | 164 | 3ad2ant3 1136 |
. . . 4
โข ((๐ โง (2โ(๐ + 1)) < (((2 ยท ๐) + 1)C๐) โง (๐ โ โค โง 2 โค ๐)) โ ((2 ยท (((2
ยท ๐) + 3) / (๐ + 2))) ยท (((2 ยท
๐) + 1)C๐)) = (((2 ยท (๐ + 1)) + 1)C(๐ + 1))) |
166 | 151, 165 | breq12d 5119 |
. . 3
โข ((๐ โง (2โ(๐ + 1)) < (((2 ยท ๐) + 1)C๐) โง (๐ โ โค โง 2 โค ๐)) โ ((2 ยท
(2โ(๐ + 1))) < ((2
ยท (((2 ยท ๐) +
3) / (๐ + 2))) ยท
(((2 ยท ๐) + 1)C๐)) โ (2โ((๐ + 1) + 1)) < (((2 ยท
(๐ + 1)) + 1)C(๐ + 1)))) |
167 | 139, 166 | mpbid 231 |
. 2
โข ((๐ โง (2โ(๐ + 1)) < (((2 ยท ๐) + 1)C๐) โง (๐ โ โค โง 2 โค ๐)) โ (2โ((๐ + 1) + 1)) < (((2 ยท
(๐ + 1)) + 1)C(๐ + 1))) |
168 | | 2z 12540 |
. . 3
โข 2 โ
โค |
169 | 168 | a1i 11 |
. 2
โข (๐ โ 2 โ
โค) |
170 | | 2ap1caineq.1 |
. 2
โข (๐ โ ๐ โ โค) |
171 | | 2ap1caineq.2 |
. 2
โข (๐ โ 2 โค ๐) |
172 | 7, 14, 21, 28, 48, 167, 169, 170, 171 | uzindd 40480 |
1
โข (๐ โ (2โ(๐ + 1)) < (((2 ยท ๐) + 1)C๐)) |