Step |
Hyp |
Ref |
Expression |
1 |
|
oveq2 |
⊢ ( 𝑥 = 4 → ( 4 ↑ 𝑥 ) = ( 4 ↑ 4 ) ) |
2 |
|
id |
⊢ ( 𝑥 = 4 → 𝑥 = 4 ) |
3 |
1 2
|
oveq12d |
⊢ ( 𝑥 = 4 → ( ( 4 ↑ 𝑥 ) / 𝑥 ) = ( ( 4 ↑ 4 ) / 4 ) ) |
4 |
|
oveq2 |
⊢ ( 𝑥 = 4 → ( 2 · 𝑥 ) = ( 2 · 4 ) ) |
5 |
4 2
|
oveq12d |
⊢ ( 𝑥 = 4 → ( ( 2 · 𝑥 ) C 𝑥 ) = ( ( 2 · 4 ) C 4 ) ) |
6 |
3 5
|
breq12d |
⊢ ( 𝑥 = 4 → ( ( ( 4 ↑ 𝑥 ) / 𝑥 ) < ( ( 2 · 𝑥 ) C 𝑥 ) ↔ ( ( 4 ↑ 4 ) / 4 ) < ( ( 2 · 4 ) C 4 ) ) ) |
7 |
|
oveq2 |
⊢ ( 𝑥 = 𝑛 → ( 4 ↑ 𝑥 ) = ( 4 ↑ 𝑛 ) ) |
8 |
|
id |
⊢ ( 𝑥 = 𝑛 → 𝑥 = 𝑛 ) |
9 |
7 8
|
oveq12d |
⊢ ( 𝑥 = 𝑛 → ( ( 4 ↑ 𝑥 ) / 𝑥 ) = ( ( 4 ↑ 𝑛 ) / 𝑛 ) ) |
10 |
|
oveq2 |
⊢ ( 𝑥 = 𝑛 → ( 2 · 𝑥 ) = ( 2 · 𝑛 ) ) |
11 |
10 8
|
oveq12d |
⊢ ( 𝑥 = 𝑛 → ( ( 2 · 𝑥 ) C 𝑥 ) = ( ( 2 · 𝑛 ) C 𝑛 ) ) |
12 |
9 11
|
breq12d |
⊢ ( 𝑥 = 𝑛 → ( ( ( 4 ↑ 𝑥 ) / 𝑥 ) < ( ( 2 · 𝑥 ) C 𝑥 ) ↔ ( ( 4 ↑ 𝑛 ) / 𝑛 ) < ( ( 2 · 𝑛 ) C 𝑛 ) ) ) |
13 |
|
oveq2 |
⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( 4 ↑ 𝑥 ) = ( 4 ↑ ( 𝑛 + 1 ) ) ) |
14 |
|
id |
⊢ ( 𝑥 = ( 𝑛 + 1 ) → 𝑥 = ( 𝑛 + 1 ) ) |
15 |
13 14
|
oveq12d |
⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( 4 ↑ 𝑥 ) / 𝑥 ) = ( ( 4 ↑ ( 𝑛 + 1 ) ) / ( 𝑛 + 1 ) ) ) |
16 |
|
oveq2 |
⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( 2 · 𝑥 ) = ( 2 · ( 𝑛 + 1 ) ) ) |
17 |
16 14
|
oveq12d |
⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( 2 · 𝑥 ) C 𝑥 ) = ( ( 2 · ( 𝑛 + 1 ) ) C ( 𝑛 + 1 ) ) ) |
18 |
15 17
|
breq12d |
⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( ( 4 ↑ 𝑥 ) / 𝑥 ) < ( ( 2 · 𝑥 ) C 𝑥 ) ↔ ( ( 4 ↑ ( 𝑛 + 1 ) ) / ( 𝑛 + 1 ) ) < ( ( 2 · ( 𝑛 + 1 ) ) C ( 𝑛 + 1 ) ) ) ) |
19 |
|
oveq2 |
⊢ ( 𝑥 = 𝑁 → ( 4 ↑ 𝑥 ) = ( 4 ↑ 𝑁 ) ) |
20 |
|
id |
⊢ ( 𝑥 = 𝑁 → 𝑥 = 𝑁 ) |
21 |
19 20
|
oveq12d |
⊢ ( 𝑥 = 𝑁 → ( ( 4 ↑ 𝑥 ) / 𝑥 ) = ( ( 4 ↑ 𝑁 ) / 𝑁 ) ) |
22 |
|
oveq2 |
⊢ ( 𝑥 = 𝑁 → ( 2 · 𝑥 ) = ( 2 · 𝑁 ) ) |
23 |
22 20
|
oveq12d |
⊢ ( 𝑥 = 𝑁 → ( ( 2 · 𝑥 ) C 𝑥 ) = ( ( 2 · 𝑁 ) C 𝑁 ) ) |
24 |
21 23
|
breq12d |
⊢ ( 𝑥 = 𝑁 → ( ( ( 4 ↑ 𝑥 ) / 𝑥 ) < ( ( 2 · 𝑥 ) C 𝑥 ) ↔ ( ( 4 ↑ 𝑁 ) / 𝑁 ) < ( ( 2 · 𝑁 ) C 𝑁 ) ) ) |
25 |
|
6nn0 |
⊢ 6 ∈ ℕ0 |
26 |
|
7nn0 |
⊢ 7 ∈ ℕ0 |
27 |
|
4nn0 |
⊢ 4 ∈ ℕ0 |
28 |
|
0nn0 |
⊢ 0 ∈ ℕ0 |
29 |
|
4lt10 |
⊢ 4 < ; 1 0 |
30 |
|
6lt7 |
⊢ 6 < 7 |
31 |
25 26 27 28 29 30
|
decltc |
⊢ ; 6 4 < ; 7 0 |
32 |
|
2cn |
⊢ 2 ∈ ℂ |
33 |
|
2nn0 |
⊢ 2 ∈ ℕ0 |
34 |
|
3nn0 |
⊢ 3 ∈ ℕ0 |
35 |
|
expmul |
⊢ ( ( 2 ∈ ℂ ∧ 2 ∈ ℕ0 ∧ 3 ∈ ℕ0 ) → ( 2 ↑ ( 2 · 3 ) ) = ( ( 2 ↑ 2 ) ↑ 3 ) ) |
36 |
32 33 34 35
|
mp3an |
⊢ ( 2 ↑ ( 2 · 3 ) ) = ( ( 2 ↑ 2 ) ↑ 3 ) |
37 |
|
sq2 |
⊢ ( 2 ↑ 2 ) = 4 |
38 |
37
|
eqcomi |
⊢ 4 = ( 2 ↑ 2 ) |
39 |
|
4m1e3 |
⊢ ( 4 − 1 ) = 3 |
40 |
38 39
|
oveq12i |
⊢ ( 4 ↑ ( 4 − 1 ) ) = ( ( 2 ↑ 2 ) ↑ 3 ) |
41 |
36 40
|
eqtr4i |
⊢ ( 2 ↑ ( 2 · 3 ) ) = ( 4 ↑ ( 4 − 1 ) ) |
42 |
|
3cn |
⊢ 3 ∈ ℂ |
43 |
|
3t2e6 |
⊢ ( 3 · 2 ) = 6 |
44 |
42 32 43
|
mulcomli |
⊢ ( 2 · 3 ) = 6 |
45 |
44
|
oveq2i |
⊢ ( 2 ↑ ( 2 · 3 ) ) = ( 2 ↑ 6 ) |
46 |
|
2exp6 |
⊢ ( 2 ↑ 6 ) = ; 6 4 |
47 |
45 46
|
eqtri |
⊢ ( 2 ↑ ( 2 · 3 ) ) = ; 6 4 |
48 |
|
4cn |
⊢ 4 ∈ ℂ |
49 |
|
4ne0 |
⊢ 4 ≠ 0 |
50 |
|
4z |
⊢ 4 ∈ ℤ |
51 |
|
expm1 |
⊢ ( ( 4 ∈ ℂ ∧ 4 ≠ 0 ∧ 4 ∈ ℤ ) → ( 4 ↑ ( 4 − 1 ) ) = ( ( 4 ↑ 4 ) / 4 ) ) |
52 |
48 49 50 51
|
mp3an |
⊢ ( 4 ↑ ( 4 − 1 ) ) = ( ( 4 ↑ 4 ) / 4 ) |
53 |
41 47 52
|
3eqtr3ri |
⊢ ( ( 4 ↑ 4 ) / 4 ) = ; 6 4 |
54 |
|
df-4 |
⊢ 4 = ( 3 + 1 ) |
55 |
54
|
oveq2i |
⊢ ( 2 · 4 ) = ( 2 · ( 3 + 1 ) ) |
56 |
55 54
|
oveq12i |
⊢ ( ( 2 · 4 ) C 4 ) = ( ( 2 · ( 3 + 1 ) ) C ( 3 + 1 ) ) |
57 |
|
bcp1ctr |
⊢ ( 3 ∈ ℕ0 → ( ( 2 · ( 3 + 1 ) ) C ( 3 + 1 ) ) = ( ( ( 2 · 3 ) C 3 ) · ( 2 · ( ( ( 2 · 3 ) + 1 ) / ( 3 + 1 ) ) ) ) ) |
58 |
34 57
|
ax-mp |
⊢ ( ( 2 · ( 3 + 1 ) ) C ( 3 + 1 ) ) = ( ( ( 2 · 3 ) C 3 ) · ( 2 · ( ( ( 2 · 3 ) + 1 ) / ( 3 + 1 ) ) ) ) |
59 |
|
df-3 |
⊢ 3 = ( 2 + 1 ) |
60 |
59
|
oveq2i |
⊢ ( 2 · 3 ) = ( 2 · ( 2 + 1 ) ) |
61 |
60 59
|
oveq12i |
⊢ ( ( 2 · 3 ) C 3 ) = ( ( 2 · ( 2 + 1 ) ) C ( 2 + 1 ) ) |
62 |
|
bcp1ctr |
⊢ ( 2 ∈ ℕ0 → ( ( 2 · ( 2 + 1 ) ) C ( 2 + 1 ) ) = ( ( ( 2 · 2 ) C 2 ) · ( 2 · ( ( ( 2 · 2 ) + 1 ) / ( 2 + 1 ) ) ) ) ) |
63 |
33 62
|
ax-mp |
⊢ ( ( 2 · ( 2 + 1 ) ) C ( 2 + 1 ) ) = ( ( ( 2 · 2 ) C 2 ) · ( 2 · ( ( ( 2 · 2 ) + 1 ) / ( 2 + 1 ) ) ) ) |
64 |
|
df-2 |
⊢ 2 = ( 1 + 1 ) |
65 |
64
|
oveq2i |
⊢ ( 2 · 2 ) = ( 2 · ( 1 + 1 ) ) |
66 |
65 64
|
oveq12i |
⊢ ( ( 2 · 2 ) C 2 ) = ( ( 2 · ( 1 + 1 ) ) C ( 1 + 1 ) ) |
67 |
|
1nn0 |
⊢ 1 ∈ ℕ0 |
68 |
|
bcp1ctr |
⊢ ( 1 ∈ ℕ0 → ( ( 2 · ( 1 + 1 ) ) C ( 1 + 1 ) ) = ( ( ( 2 · 1 ) C 1 ) · ( 2 · ( ( ( 2 · 1 ) + 1 ) / ( 1 + 1 ) ) ) ) ) |
69 |
67 68
|
ax-mp |
⊢ ( ( 2 · ( 1 + 1 ) ) C ( 1 + 1 ) ) = ( ( ( 2 · 1 ) C 1 ) · ( 2 · ( ( ( 2 · 1 ) + 1 ) / ( 1 + 1 ) ) ) ) |
70 |
|
1e0p1 |
⊢ 1 = ( 0 + 1 ) |
71 |
70
|
oveq2i |
⊢ ( 2 · 1 ) = ( 2 · ( 0 + 1 ) ) |
72 |
71 70
|
oveq12i |
⊢ ( ( 2 · 1 ) C 1 ) = ( ( 2 · ( 0 + 1 ) ) C ( 0 + 1 ) ) |
73 |
|
bcp1ctr |
⊢ ( 0 ∈ ℕ0 → ( ( 2 · ( 0 + 1 ) ) C ( 0 + 1 ) ) = ( ( ( 2 · 0 ) C 0 ) · ( 2 · ( ( ( 2 · 0 ) + 1 ) / ( 0 + 1 ) ) ) ) ) |
74 |
28 73
|
ax-mp |
⊢ ( ( 2 · ( 0 + 1 ) ) C ( 0 + 1 ) ) = ( ( ( 2 · 0 ) C 0 ) · ( 2 · ( ( ( 2 · 0 ) + 1 ) / ( 0 + 1 ) ) ) ) |
75 |
33 28
|
nn0mulcli |
⊢ ( 2 · 0 ) ∈ ℕ0 |
76 |
|
bcn0 |
⊢ ( ( 2 · 0 ) ∈ ℕ0 → ( ( 2 · 0 ) C 0 ) = 1 ) |
77 |
75 76
|
ax-mp |
⊢ ( ( 2 · 0 ) C 0 ) = 1 |
78 |
|
2t0e0 |
⊢ ( 2 · 0 ) = 0 |
79 |
78
|
oveq1i |
⊢ ( ( 2 · 0 ) + 1 ) = ( 0 + 1 ) |
80 |
79 70
|
eqtr4i |
⊢ ( ( 2 · 0 ) + 1 ) = 1 |
81 |
70
|
eqcomi |
⊢ ( 0 + 1 ) = 1 |
82 |
80 81
|
oveq12i |
⊢ ( ( ( 2 · 0 ) + 1 ) / ( 0 + 1 ) ) = ( 1 / 1 ) |
83 |
|
1div1e1 |
⊢ ( 1 / 1 ) = 1 |
84 |
82 83
|
eqtri |
⊢ ( ( ( 2 · 0 ) + 1 ) / ( 0 + 1 ) ) = 1 |
85 |
84
|
oveq2i |
⊢ ( 2 · ( ( ( 2 · 0 ) + 1 ) / ( 0 + 1 ) ) ) = ( 2 · 1 ) |
86 |
|
2t1e2 |
⊢ ( 2 · 1 ) = 2 |
87 |
85 86
|
eqtri |
⊢ ( 2 · ( ( ( 2 · 0 ) + 1 ) / ( 0 + 1 ) ) ) = 2 |
88 |
77 87
|
oveq12i |
⊢ ( ( ( 2 · 0 ) C 0 ) · ( 2 · ( ( ( 2 · 0 ) + 1 ) / ( 0 + 1 ) ) ) ) = ( 1 · 2 ) |
89 |
32
|
mulid2i |
⊢ ( 1 · 2 ) = 2 |
90 |
88 89
|
eqtri |
⊢ ( ( ( 2 · 0 ) C 0 ) · ( 2 · ( ( ( 2 · 0 ) + 1 ) / ( 0 + 1 ) ) ) ) = 2 |
91 |
72 74 90
|
3eqtri |
⊢ ( ( 2 · 1 ) C 1 ) = 2 |
92 |
86
|
oveq1i |
⊢ ( ( 2 · 1 ) + 1 ) = ( 2 + 1 ) |
93 |
92 59
|
eqtr4i |
⊢ ( ( 2 · 1 ) + 1 ) = 3 |
94 |
64
|
eqcomi |
⊢ ( 1 + 1 ) = 2 |
95 |
93 94
|
oveq12i |
⊢ ( ( ( 2 · 1 ) + 1 ) / ( 1 + 1 ) ) = ( 3 / 2 ) |
96 |
95
|
oveq2i |
⊢ ( 2 · ( ( ( 2 · 1 ) + 1 ) / ( 1 + 1 ) ) ) = ( 2 · ( 3 / 2 ) ) |
97 |
|
2ne0 |
⊢ 2 ≠ 0 |
98 |
42 32 97
|
divcan2i |
⊢ ( 2 · ( 3 / 2 ) ) = 3 |
99 |
96 98
|
eqtri |
⊢ ( 2 · ( ( ( 2 · 1 ) + 1 ) / ( 1 + 1 ) ) ) = 3 |
100 |
91 99
|
oveq12i |
⊢ ( ( ( 2 · 1 ) C 1 ) · ( 2 · ( ( ( 2 · 1 ) + 1 ) / ( 1 + 1 ) ) ) ) = ( 2 · 3 ) |
101 |
100 44
|
eqtri |
⊢ ( ( ( 2 · 1 ) C 1 ) · ( 2 · ( ( ( 2 · 1 ) + 1 ) / ( 1 + 1 ) ) ) ) = 6 |
102 |
66 69 101
|
3eqtri |
⊢ ( ( 2 · 2 ) C 2 ) = 6 |
103 |
|
2t2e4 |
⊢ ( 2 · 2 ) = 4 |
104 |
103
|
oveq1i |
⊢ ( ( 2 · 2 ) + 1 ) = ( 4 + 1 ) |
105 |
|
df-5 |
⊢ 5 = ( 4 + 1 ) |
106 |
104 105
|
eqtr4i |
⊢ ( ( 2 · 2 ) + 1 ) = 5 |
107 |
59
|
eqcomi |
⊢ ( 2 + 1 ) = 3 |
108 |
106 107
|
oveq12i |
⊢ ( ( ( 2 · 2 ) + 1 ) / ( 2 + 1 ) ) = ( 5 / 3 ) |
109 |
108
|
oveq2i |
⊢ ( 2 · ( ( ( 2 · 2 ) + 1 ) / ( 2 + 1 ) ) ) = ( 2 · ( 5 / 3 ) ) |
110 |
|
5cn |
⊢ 5 ∈ ℂ |
111 |
|
3ne0 |
⊢ 3 ≠ 0 |
112 |
32 110 42 111
|
divassi |
⊢ ( ( 2 · 5 ) / 3 ) = ( 2 · ( 5 / 3 ) ) |
113 |
109 112
|
eqtr4i |
⊢ ( 2 · ( ( ( 2 · 2 ) + 1 ) / ( 2 + 1 ) ) ) = ( ( 2 · 5 ) / 3 ) |
114 |
102 113
|
oveq12i |
⊢ ( ( ( 2 · 2 ) C 2 ) · ( 2 · ( ( ( 2 · 2 ) + 1 ) / ( 2 + 1 ) ) ) ) = ( 6 · ( ( 2 · 5 ) / 3 ) ) |
115 |
63 114
|
eqtri |
⊢ ( ( 2 · ( 2 + 1 ) ) C ( 2 + 1 ) ) = ( 6 · ( ( 2 · 5 ) / 3 ) ) |
116 |
|
6cn |
⊢ 6 ∈ ℂ |
117 |
|
2nn |
⊢ 2 ∈ ℕ |
118 |
|
5nn |
⊢ 5 ∈ ℕ |
119 |
117 118
|
nnmulcli |
⊢ ( 2 · 5 ) ∈ ℕ |
120 |
119
|
nncni |
⊢ ( 2 · 5 ) ∈ ℂ |
121 |
42 111
|
pm3.2i |
⊢ ( 3 ∈ ℂ ∧ 3 ≠ 0 ) |
122 |
|
div12 |
⊢ ( ( 6 ∈ ℂ ∧ ( 2 · 5 ) ∈ ℂ ∧ ( 3 ∈ ℂ ∧ 3 ≠ 0 ) ) → ( 6 · ( ( 2 · 5 ) / 3 ) ) = ( ( 2 · 5 ) · ( 6 / 3 ) ) ) |
123 |
116 120 121 122
|
mp3an |
⊢ ( 6 · ( ( 2 · 5 ) / 3 ) ) = ( ( 2 · 5 ) · ( 6 / 3 ) ) |
124 |
|
5t2e10 |
⊢ ( 5 · 2 ) = ; 1 0 |
125 |
110 32 124
|
mulcomli |
⊢ ( 2 · 5 ) = ; 1 0 |
126 |
116 42 32 111
|
divmuli |
⊢ ( ( 6 / 3 ) = 2 ↔ ( 3 · 2 ) = 6 ) |
127 |
43 126
|
mpbir |
⊢ ( 6 / 3 ) = 2 |
128 |
125 127
|
oveq12i |
⊢ ( ( 2 · 5 ) · ( 6 / 3 ) ) = ( ; 1 0 · 2 ) |
129 |
123 128
|
eqtri |
⊢ ( 6 · ( ( 2 · 5 ) / 3 ) ) = ( ; 1 0 · 2 ) |
130 |
61 115 129
|
3eqtri |
⊢ ( ( 2 · 3 ) C 3 ) = ( ; 1 0 · 2 ) |
131 |
44
|
oveq1i |
⊢ ( ( 2 · 3 ) + 1 ) = ( 6 + 1 ) |
132 |
|
df-7 |
⊢ 7 = ( 6 + 1 ) |
133 |
131 132
|
eqtr4i |
⊢ ( ( 2 · 3 ) + 1 ) = 7 |
134 |
|
3p1e4 |
⊢ ( 3 + 1 ) = 4 |
135 |
133 134
|
oveq12i |
⊢ ( ( ( 2 · 3 ) + 1 ) / ( 3 + 1 ) ) = ( 7 / 4 ) |
136 |
135
|
oveq2i |
⊢ ( 2 · ( ( ( 2 · 3 ) + 1 ) / ( 3 + 1 ) ) ) = ( 2 · ( 7 / 4 ) ) |
137 |
130 136
|
oveq12i |
⊢ ( ( ( 2 · 3 ) C 3 ) · ( 2 · ( ( ( 2 · 3 ) + 1 ) / ( 3 + 1 ) ) ) ) = ( ( ; 1 0 · 2 ) · ( 2 · ( 7 / 4 ) ) ) |
138 |
56 58 137
|
3eqtri |
⊢ ( ( 2 · 4 ) C 4 ) = ( ( ; 1 0 · 2 ) · ( 2 · ( 7 / 4 ) ) ) |
139 |
|
10nn |
⊢ ; 1 0 ∈ ℕ |
140 |
139
|
nncni |
⊢ ; 1 0 ∈ ℂ |
141 |
|
7cn |
⊢ 7 ∈ ℂ |
142 |
141 48 49
|
divcli |
⊢ ( 7 / 4 ) ∈ ℂ |
143 |
32 142
|
mulcli |
⊢ ( 2 · ( 7 / 4 ) ) ∈ ℂ |
144 |
140 32 143
|
mulassi |
⊢ ( ( ; 1 0 · 2 ) · ( 2 · ( 7 / 4 ) ) ) = ( ; 1 0 · ( 2 · ( 2 · ( 7 / 4 ) ) ) ) |
145 |
103
|
oveq1i |
⊢ ( ( 2 · 2 ) · ( 7 / 4 ) ) = ( 4 · ( 7 / 4 ) ) |
146 |
32 32 142
|
mulassi |
⊢ ( ( 2 · 2 ) · ( 7 / 4 ) ) = ( 2 · ( 2 · ( 7 / 4 ) ) ) |
147 |
141 48 49
|
divcan2i |
⊢ ( 4 · ( 7 / 4 ) ) = 7 |
148 |
145 146 147
|
3eqtr3i |
⊢ ( 2 · ( 2 · ( 7 / 4 ) ) ) = 7 |
149 |
148
|
oveq2i |
⊢ ( ; 1 0 · ( 2 · ( 2 · ( 7 / 4 ) ) ) ) = ( ; 1 0 · 7 ) |
150 |
144 149
|
eqtri |
⊢ ( ( ; 1 0 · 2 ) · ( 2 · ( 7 / 4 ) ) ) = ( ; 1 0 · 7 ) |
151 |
26
|
dec0u |
⊢ ( ; 1 0 · 7 ) = ; 7 0 |
152 |
138 150 151
|
3eqtri |
⊢ ( ( 2 · 4 ) C 4 ) = ; 7 0 |
153 |
31 53 152
|
3brtr4i |
⊢ ( ( 4 ↑ 4 ) / 4 ) < ( ( 2 · 4 ) C 4 ) |
154 |
|
4nn |
⊢ 4 ∈ ℕ |
155 |
|
eluznn |
⊢ ( ( 4 ∈ ℕ ∧ 𝑛 ∈ ( ℤ≥ ‘ 4 ) ) → 𝑛 ∈ ℕ ) |
156 |
154 155
|
mpan |
⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 4 ) → 𝑛 ∈ ℕ ) |
157 |
|
nnnn0 |
⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ0 ) |
158 |
|
nnexpcl |
⊢ ( ( 4 ∈ ℕ ∧ 𝑛 ∈ ℕ0 ) → ( 4 ↑ 𝑛 ) ∈ ℕ ) |
159 |
154 157 158
|
sylancr |
⊢ ( 𝑛 ∈ ℕ → ( 4 ↑ 𝑛 ) ∈ ℕ ) |
160 |
159
|
nnrpd |
⊢ ( 𝑛 ∈ ℕ → ( 4 ↑ 𝑛 ) ∈ ℝ+ ) |
161 |
|
nnrp |
⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℝ+ ) |
162 |
160 161
|
rpdivcld |
⊢ ( 𝑛 ∈ ℕ → ( ( 4 ↑ 𝑛 ) / 𝑛 ) ∈ ℝ+ ) |
163 |
162
|
rpred |
⊢ ( 𝑛 ∈ ℕ → ( ( 4 ↑ 𝑛 ) / 𝑛 ) ∈ ℝ ) |
164 |
|
nnmulcl |
⊢ ( ( 2 ∈ ℕ ∧ 𝑛 ∈ ℕ ) → ( 2 · 𝑛 ) ∈ ℕ ) |
165 |
117 164
|
mpan |
⊢ ( 𝑛 ∈ ℕ → ( 2 · 𝑛 ) ∈ ℕ ) |
166 |
165
|
nnnn0d |
⊢ ( 𝑛 ∈ ℕ → ( 2 · 𝑛 ) ∈ ℕ0 ) |
167 |
|
nnz |
⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℤ ) |
168 |
|
bccl |
⊢ ( ( ( 2 · 𝑛 ) ∈ ℕ0 ∧ 𝑛 ∈ ℤ ) → ( ( 2 · 𝑛 ) C 𝑛 ) ∈ ℕ0 ) |
169 |
166 167 168
|
syl2anc |
⊢ ( 𝑛 ∈ ℕ → ( ( 2 · 𝑛 ) C 𝑛 ) ∈ ℕ0 ) |
170 |
169
|
nn0red |
⊢ ( 𝑛 ∈ ℕ → ( ( 2 · 𝑛 ) C 𝑛 ) ∈ ℝ ) |
171 |
|
2rp |
⊢ 2 ∈ ℝ+ |
172 |
165
|
peano2nnd |
⊢ ( 𝑛 ∈ ℕ → ( ( 2 · 𝑛 ) + 1 ) ∈ ℕ ) |
173 |
172
|
nnrpd |
⊢ ( 𝑛 ∈ ℕ → ( ( 2 · 𝑛 ) + 1 ) ∈ ℝ+ ) |
174 |
|
peano2nn |
⊢ ( 𝑛 ∈ ℕ → ( 𝑛 + 1 ) ∈ ℕ ) |
175 |
174
|
nnrpd |
⊢ ( 𝑛 ∈ ℕ → ( 𝑛 + 1 ) ∈ ℝ+ ) |
176 |
173 175
|
rpdivcld |
⊢ ( 𝑛 ∈ ℕ → ( ( ( 2 · 𝑛 ) + 1 ) / ( 𝑛 + 1 ) ) ∈ ℝ+ ) |
177 |
|
rpmulcl |
⊢ ( ( 2 ∈ ℝ+ ∧ ( ( ( 2 · 𝑛 ) + 1 ) / ( 𝑛 + 1 ) ) ∈ ℝ+ ) → ( 2 · ( ( ( 2 · 𝑛 ) + 1 ) / ( 𝑛 + 1 ) ) ) ∈ ℝ+ ) |
178 |
171 176 177
|
sylancr |
⊢ ( 𝑛 ∈ ℕ → ( 2 · ( ( ( 2 · 𝑛 ) + 1 ) / ( 𝑛 + 1 ) ) ) ∈ ℝ+ ) |
179 |
163 170 178
|
ltmul1d |
⊢ ( 𝑛 ∈ ℕ → ( ( ( 4 ↑ 𝑛 ) / 𝑛 ) < ( ( 2 · 𝑛 ) C 𝑛 ) ↔ ( ( ( 4 ↑ 𝑛 ) / 𝑛 ) · ( 2 · ( ( ( 2 · 𝑛 ) + 1 ) / ( 𝑛 + 1 ) ) ) ) < ( ( ( 2 · 𝑛 ) C 𝑛 ) · ( 2 · ( ( ( 2 · 𝑛 ) + 1 ) / ( 𝑛 + 1 ) ) ) ) ) ) |
180 |
|
bcp1ctr |
⊢ ( 𝑛 ∈ ℕ0 → ( ( 2 · ( 𝑛 + 1 ) ) C ( 𝑛 + 1 ) ) = ( ( ( 2 · 𝑛 ) C 𝑛 ) · ( 2 · ( ( ( 2 · 𝑛 ) + 1 ) / ( 𝑛 + 1 ) ) ) ) ) |
181 |
157 180
|
syl |
⊢ ( 𝑛 ∈ ℕ → ( ( 2 · ( 𝑛 + 1 ) ) C ( 𝑛 + 1 ) ) = ( ( ( 2 · 𝑛 ) C 𝑛 ) · ( 2 · ( ( ( 2 · 𝑛 ) + 1 ) / ( 𝑛 + 1 ) ) ) ) ) |
182 |
181
|
breq2d |
⊢ ( 𝑛 ∈ ℕ → ( ( ( ( 4 ↑ 𝑛 ) / 𝑛 ) · ( 2 · ( ( ( 2 · 𝑛 ) + 1 ) / ( 𝑛 + 1 ) ) ) ) < ( ( 2 · ( 𝑛 + 1 ) ) C ( 𝑛 + 1 ) ) ↔ ( ( ( 4 ↑ 𝑛 ) / 𝑛 ) · ( 2 · ( ( ( 2 · 𝑛 ) + 1 ) / ( 𝑛 + 1 ) ) ) ) < ( ( ( 2 · 𝑛 ) C 𝑛 ) · ( 2 · ( ( ( 2 · 𝑛 ) + 1 ) / ( 𝑛 + 1 ) ) ) ) ) ) |
183 |
179 182
|
bitr4d |
⊢ ( 𝑛 ∈ ℕ → ( ( ( 4 ↑ 𝑛 ) / 𝑛 ) < ( ( 2 · 𝑛 ) C 𝑛 ) ↔ ( ( ( 4 ↑ 𝑛 ) / 𝑛 ) · ( 2 · ( ( ( 2 · 𝑛 ) + 1 ) / ( 𝑛 + 1 ) ) ) ) < ( ( 2 · ( 𝑛 + 1 ) ) C ( 𝑛 + 1 ) ) ) ) |
184 |
|
2re |
⊢ 2 ∈ ℝ |
185 |
184
|
a1i |
⊢ ( 𝑛 ∈ ℕ → 2 ∈ ℝ ) |
186 |
173 161
|
rpdivcld |
⊢ ( 𝑛 ∈ ℕ → ( ( ( 2 · 𝑛 ) + 1 ) / 𝑛 ) ∈ ℝ+ ) |
187 |
186
|
rpred |
⊢ ( 𝑛 ∈ ℕ → ( ( ( 2 · 𝑛 ) + 1 ) / 𝑛 ) ∈ ℝ ) |
188 |
|
nnmulcl |
⊢ ( ( ( 4 ↑ 𝑛 ) ∈ ℕ ∧ 2 ∈ ℕ ) → ( ( 4 ↑ 𝑛 ) · 2 ) ∈ ℕ ) |
189 |
159 117 188
|
sylancl |
⊢ ( 𝑛 ∈ ℕ → ( ( 4 ↑ 𝑛 ) · 2 ) ∈ ℕ ) |
190 |
189
|
nnrpd |
⊢ ( 𝑛 ∈ ℕ → ( ( 4 ↑ 𝑛 ) · 2 ) ∈ ℝ+ ) |
191 |
190 175
|
rpdivcld |
⊢ ( 𝑛 ∈ ℕ → ( ( ( 4 ↑ 𝑛 ) · 2 ) / ( 𝑛 + 1 ) ) ∈ ℝ+ ) |
192 |
161
|
rpreccld |
⊢ ( 𝑛 ∈ ℕ → ( 1 / 𝑛 ) ∈ ℝ+ ) |
193 |
|
ltaddrp |
⊢ ( ( 2 ∈ ℝ ∧ ( 1 / 𝑛 ) ∈ ℝ+ ) → 2 < ( 2 + ( 1 / 𝑛 ) ) ) |
194 |
184 192 193
|
sylancr |
⊢ ( 𝑛 ∈ ℕ → 2 < ( 2 + ( 1 / 𝑛 ) ) ) |
195 |
165
|
nncnd |
⊢ ( 𝑛 ∈ ℕ → ( 2 · 𝑛 ) ∈ ℂ ) |
196 |
|
1cnd |
⊢ ( 𝑛 ∈ ℕ → 1 ∈ ℂ ) |
197 |
|
nncn |
⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℂ ) |
198 |
|
nnne0 |
⊢ ( 𝑛 ∈ ℕ → 𝑛 ≠ 0 ) |
199 |
195 196 197 198
|
divdird |
⊢ ( 𝑛 ∈ ℕ → ( ( ( 2 · 𝑛 ) + 1 ) / 𝑛 ) = ( ( ( 2 · 𝑛 ) / 𝑛 ) + ( 1 / 𝑛 ) ) ) |
200 |
32
|
a1i |
⊢ ( 𝑛 ∈ ℕ → 2 ∈ ℂ ) |
201 |
200 197 198
|
divcan4d |
⊢ ( 𝑛 ∈ ℕ → ( ( 2 · 𝑛 ) / 𝑛 ) = 2 ) |
202 |
201
|
oveq1d |
⊢ ( 𝑛 ∈ ℕ → ( ( ( 2 · 𝑛 ) / 𝑛 ) + ( 1 / 𝑛 ) ) = ( 2 + ( 1 / 𝑛 ) ) ) |
203 |
199 202
|
eqtr2d |
⊢ ( 𝑛 ∈ ℕ → ( 2 + ( 1 / 𝑛 ) ) = ( ( ( 2 · 𝑛 ) + 1 ) / 𝑛 ) ) |
204 |
194 203
|
breqtrd |
⊢ ( 𝑛 ∈ ℕ → 2 < ( ( ( 2 · 𝑛 ) + 1 ) / 𝑛 ) ) |
205 |
185 187 191 204
|
ltmul2dd |
⊢ ( 𝑛 ∈ ℕ → ( ( ( ( 4 ↑ 𝑛 ) · 2 ) / ( 𝑛 + 1 ) ) · 2 ) < ( ( ( ( 4 ↑ 𝑛 ) · 2 ) / ( 𝑛 + 1 ) ) · ( ( ( 2 · 𝑛 ) + 1 ) / 𝑛 ) ) ) |
206 |
|
expp1 |
⊢ ( ( 4 ∈ ℂ ∧ 𝑛 ∈ ℕ0 ) → ( 4 ↑ ( 𝑛 + 1 ) ) = ( ( 4 ↑ 𝑛 ) · 4 ) ) |
207 |
48 157 206
|
sylancr |
⊢ ( 𝑛 ∈ ℕ → ( 4 ↑ ( 𝑛 + 1 ) ) = ( ( 4 ↑ 𝑛 ) · 4 ) ) |
208 |
159
|
nncnd |
⊢ ( 𝑛 ∈ ℕ → ( 4 ↑ 𝑛 ) ∈ ℂ ) |
209 |
208 200 200
|
mulassd |
⊢ ( 𝑛 ∈ ℕ → ( ( ( 4 ↑ 𝑛 ) · 2 ) · 2 ) = ( ( 4 ↑ 𝑛 ) · ( 2 · 2 ) ) ) |
210 |
103
|
oveq2i |
⊢ ( ( 4 ↑ 𝑛 ) · ( 2 · 2 ) ) = ( ( 4 ↑ 𝑛 ) · 4 ) |
211 |
209 210
|
eqtrdi |
⊢ ( 𝑛 ∈ ℕ → ( ( ( 4 ↑ 𝑛 ) · 2 ) · 2 ) = ( ( 4 ↑ 𝑛 ) · 4 ) ) |
212 |
207 211
|
eqtr4d |
⊢ ( 𝑛 ∈ ℕ → ( 4 ↑ ( 𝑛 + 1 ) ) = ( ( ( 4 ↑ 𝑛 ) · 2 ) · 2 ) ) |
213 |
212
|
oveq1d |
⊢ ( 𝑛 ∈ ℕ → ( ( 4 ↑ ( 𝑛 + 1 ) ) / ( 𝑛 + 1 ) ) = ( ( ( ( 4 ↑ 𝑛 ) · 2 ) · 2 ) / ( 𝑛 + 1 ) ) ) |
214 |
189
|
nncnd |
⊢ ( 𝑛 ∈ ℕ → ( ( 4 ↑ 𝑛 ) · 2 ) ∈ ℂ ) |
215 |
174
|
nncnd |
⊢ ( 𝑛 ∈ ℕ → ( 𝑛 + 1 ) ∈ ℂ ) |
216 |
174
|
nnne0d |
⊢ ( 𝑛 ∈ ℕ → ( 𝑛 + 1 ) ≠ 0 ) |
217 |
214 200 215 216
|
div23d |
⊢ ( 𝑛 ∈ ℕ → ( ( ( ( 4 ↑ 𝑛 ) · 2 ) · 2 ) / ( 𝑛 + 1 ) ) = ( ( ( ( 4 ↑ 𝑛 ) · 2 ) / ( 𝑛 + 1 ) ) · 2 ) ) |
218 |
213 217
|
eqtrd |
⊢ ( 𝑛 ∈ ℕ → ( ( 4 ↑ ( 𝑛 + 1 ) ) / ( 𝑛 + 1 ) ) = ( ( ( ( 4 ↑ 𝑛 ) · 2 ) / ( 𝑛 + 1 ) ) · 2 ) ) |
219 |
208 200 197 198
|
div23d |
⊢ ( 𝑛 ∈ ℕ → ( ( ( 4 ↑ 𝑛 ) · 2 ) / 𝑛 ) = ( ( ( 4 ↑ 𝑛 ) / 𝑛 ) · 2 ) ) |
220 |
219
|
oveq1d |
⊢ ( 𝑛 ∈ ℕ → ( ( ( ( 4 ↑ 𝑛 ) · 2 ) / 𝑛 ) · ( ( ( 2 · 𝑛 ) + 1 ) / ( 𝑛 + 1 ) ) ) = ( ( ( ( 4 ↑ 𝑛 ) / 𝑛 ) · 2 ) · ( ( ( 2 · 𝑛 ) + 1 ) / ( 𝑛 + 1 ) ) ) ) |
221 |
172
|
nncnd |
⊢ ( 𝑛 ∈ ℕ → ( ( 2 · 𝑛 ) + 1 ) ∈ ℂ ) |
222 |
214 197 221 215 198 216
|
divmul24d |
⊢ ( 𝑛 ∈ ℕ → ( ( ( ( 4 ↑ 𝑛 ) · 2 ) / 𝑛 ) · ( ( ( 2 · 𝑛 ) + 1 ) / ( 𝑛 + 1 ) ) ) = ( ( ( ( 4 ↑ 𝑛 ) · 2 ) / ( 𝑛 + 1 ) ) · ( ( ( 2 · 𝑛 ) + 1 ) / 𝑛 ) ) ) |
223 |
162
|
rpcnd |
⊢ ( 𝑛 ∈ ℕ → ( ( 4 ↑ 𝑛 ) / 𝑛 ) ∈ ℂ ) |
224 |
176
|
rpcnd |
⊢ ( 𝑛 ∈ ℕ → ( ( ( 2 · 𝑛 ) + 1 ) / ( 𝑛 + 1 ) ) ∈ ℂ ) |
225 |
223 200 224
|
mulassd |
⊢ ( 𝑛 ∈ ℕ → ( ( ( ( 4 ↑ 𝑛 ) / 𝑛 ) · 2 ) · ( ( ( 2 · 𝑛 ) + 1 ) / ( 𝑛 + 1 ) ) ) = ( ( ( 4 ↑ 𝑛 ) / 𝑛 ) · ( 2 · ( ( ( 2 · 𝑛 ) + 1 ) / ( 𝑛 + 1 ) ) ) ) ) |
226 |
220 222 225
|
3eqtr3rd |
⊢ ( 𝑛 ∈ ℕ → ( ( ( 4 ↑ 𝑛 ) / 𝑛 ) · ( 2 · ( ( ( 2 · 𝑛 ) + 1 ) / ( 𝑛 + 1 ) ) ) ) = ( ( ( ( 4 ↑ 𝑛 ) · 2 ) / ( 𝑛 + 1 ) ) · ( ( ( 2 · 𝑛 ) + 1 ) / 𝑛 ) ) ) |
227 |
205 218 226
|
3brtr4d |
⊢ ( 𝑛 ∈ ℕ → ( ( 4 ↑ ( 𝑛 + 1 ) ) / ( 𝑛 + 1 ) ) < ( ( ( 4 ↑ 𝑛 ) / 𝑛 ) · ( 2 · ( ( ( 2 · 𝑛 ) + 1 ) / ( 𝑛 + 1 ) ) ) ) ) |
228 |
174
|
nnnn0d |
⊢ ( 𝑛 ∈ ℕ → ( 𝑛 + 1 ) ∈ ℕ0 ) |
229 |
|
nnexpcl |
⊢ ( ( 4 ∈ ℕ ∧ ( 𝑛 + 1 ) ∈ ℕ0 ) → ( 4 ↑ ( 𝑛 + 1 ) ) ∈ ℕ ) |
230 |
154 228 229
|
sylancr |
⊢ ( 𝑛 ∈ ℕ → ( 4 ↑ ( 𝑛 + 1 ) ) ∈ ℕ ) |
231 |
230
|
nnrpd |
⊢ ( 𝑛 ∈ ℕ → ( 4 ↑ ( 𝑛 + 1 ) ) ∈ ℝ+ ) |
232 |
231 175
|
rpdivcld |
⊢ ( 𝑛 ∈ ℕ → ( ( 4 ↑ ( 𝑛 + 1 ) ) / ( 𝑛 + 1 ) ) ∈ ℝ+ ) |
233 |
232
|
rpred |
⊢ ( 𝑛 ∈ ℕ → ( ( 4 ↑ ( 𝑛 + 1 ) ) / ( 𝑛 + 1 ) ) ∈ ℝ ) |
234 |
178
|
rpred |
⊢ ( 𝑛 ∈ ℕ → ( 2 · ( ( ( 2 · 𝑛 ) + 1 ) / ( 𝑛 + 1 ) ) ) ∈ ℝ ) |
235 |
163 234
|
remulcld |
⊢ ( 𝑛 ∈ ℕ → ( ( ( 4 ↑ 𝑛 ) / 𝑛 ) · ( 2 · ( ( ( 2 · 𝑛 ) + 1 ) / ( 𝑛 + 1 ) ) ) ) ∈ ℝ ) |
236 |
|
nn0mulcl |
⊢ ( ( 2 ∈ ℕ0 ∧ ( 𝑛 + 1 ) ∈ ℕ0 ) → ( 2 · ( 𝑛 + 1 ) ) ∈ ℕ0 ) |
237 |
33 228 236
|
sylancr |
⊢ ( 𝑛 ∈ ℕ → ( 2 · ( 𝑛 + 1 ) ) ∈ ℕ0 ) |
238 |
174
|
nnzd |
⊢ ( 𝑛 ∈ ℕ → ( 𝑛 + 1 ) ∈ ℤ ) |
239 |
|
bccl |
⊢ ( ( ( 2 · ( 𝑛 + 1 ) ) ∈ ℕ0 ∧ ( 𝑛 + 1 ) ∈ ℤ ) → ( ( 2 · ( 𝑛 + 1 ) ) C ( 𝑛 + 1 ) ) ∈ ℕ0 ) |
240 |
237 238 239
|
syl2anc |
⊢ ( 𝑛 ∈ ℕ → ( ( 2 · ( 𝑛 + 1 ) ) C ( 𝑛 + 1 ) ) ∈ ℕ0 ) |
241 |
240
|
nn0red |
⊢ ( 𝑛 ∈ ℕ → ( ( 2 · ( 𝑛 + 1 ) ) C ( 𝑛 + 1 ) ) ∈ ℝ ) |
242 |
|
lttr |
⊢ ( ( ( ( 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 ) ) ) ) |
243 |
233 235 241 242
|
syl3anc |
⊢ ( 𝑛 ∈ ℕ → ( ( ( ( 4 ↑ ( 𝑛 + 1 ) ) / ( 𝑛 + 1 ) ) < ( ( ( 4 ↑ 𝑛 ) / 𝑛 ) · ( 2 · ( ( ( 2 · 𝑛 ) + 1 ) / ( 𝑛 + 1 ) ) ) ) ∧ ( ( ( 4 ↑ 𝑛 ) / 𝑛 ) · ( 2 · ( ( ( 2 · 𝑛 ) + 1 ) / ( 𝑛 + 1 ) ) ) ) < ( ( 2 · ( 𝑛 + 1 ) ) C ( 𝑛 + 1 ) ) ) → ( ( 4 ↑ ( 𝑛 + 1 ) ) / ( 𝑛 + 1 ) ) < ( ( 2 · ( 𝑛 + 1 ) ) C ( 𝑛 + 1 ) ) ) ) |
244 |
227 243
|
mpand |
⊢ ( 𝑛 ∈ ℕ → ( ( ( ( 4 ↑ 𝑛 ) / 𝑛 ) · ( 2 · ( ( ( 2 · 𝑛 ) + 1 ) / ( 𝑛 + 1 ) ) ) ) < ( ( 2 · ( 𝑛 + 1 ) ) C ( 𝑛 + 1 ) ) → ( ( 4 ↑ ( 𝑛 + 1 ) ) / ( 𝑛 + 1 ) ) < ( ( 2 · ( 𝑛 + 1 ) ) C ( 𝑛 + 1 ) ) ) ) |
245 |
183 244
|
sylbid |
⊢ ( 𝑛 ∈ ℕ → ( ( ( 4 ↑ 𝑛 ) / 𝑛 ) < ( ( 2 · 𝑛 ) C 𝑛 ) → ( ( 4 ↑ ( 𝑛 + 1 ) ) / ( 𝑛 + 1 ) ) < ( ( 2 · ( 𝑛 + 1 ) ) C ( 𝑛 + 1 ) ) ) ) |
246 |
156 245
|
syl |
⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 4 ) → ( ( ( 4 ↑ 𝑛 ) / 𝑛 ) < ( ( 2 · 𝑛 ) C 𝑛 ) → ( ( 4 ↑ ( 𝑛 + 1 ) ) / ( 𝑛 + 1 ) ) < ( ( 2 · ( 𝑛 + 1 ) ) C ( 𝑛 + 1 ) ) ) ) |
247 |
6 12 18 24 153 246
|
uzind4i |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( ( 4 ↑ 𝑁 ) / 𝑁 ) < ( ( 2 · 𝑁 ) C 𝑁 ) ) |