Metamath Proof Explorer

Theorem 2ap1caineq

Description: Inequality for Theorem 6.6 for AKS. (Contributed by metakunt, 8-Jun-2024)

Ref Expression
Hypotheses 2ap1caineq.1 
|- ( ph -> N e. ZZ )
2ap1caineq.2 
|- ( ph -> 2 <_ N )
Assertion 2ap1caineq 
|- ( ph -> ( 2 ^ ( N + 1 ) ) < ( ( ( 2 x. N ) + 1 ) _C N ) )

Proof

Step Hyp Ref Expression
1 2ap1caineq.1 
 |-  ( ph -> N e. ZZ )
2 2ap1caineq.2 
 |-  ( ph -> 2 <_ N )
3 oveq1 
 |-  ( j = 2 -> ( j + 1 ) = ( 2 + 1 ) )
4 3 oveq2d 
 |-  ( j = 2 -> ( 2 ^ ( j + 1 ) ) = ( 2 ^ ( 2 + 1 ) ) )
5 oveq2 
 |-  ( j = 2 -> ( 2 x. j ) = ( 2 x. 2 ) )
6 5 oveq1d 
 |-  ( j = 2 -> ( ( 2 x. j ) + 1 ) = ( ( 2 x. 2 ) + 1 ) )
7 id 
 |-  ( j = 2 -> j = 2 )
8 6 7 oveq12d 
 |-  ( j = 2 -> ( ( ( 2 x. j ) + 1 ) _C j ) = ( ( ( 2 x. 2 ) + 1 ) _C 2 ) )
9 4 8 breq12d 
 |-  ( j = 2 -> ( ( 2 ^ ( j + 1 ) ) < ( ( ( 2 x. j ) + 1 ) _C j ) <-> ( 2 ^ ( 2 + 1 ) ) < ( ( ( 2 x. 2 ) + 1 ) _C 2 ) ) )
10 oveq1 
 |-  ( j = k -> ( j + 1 ) = ( k + 1 ) )
11 10 oveq2d 
 |-  ( j = k -> ( 2 ^ ( j + 1 ) ) = ( 2 ^ ( k + 1 ) ) )
12 oveq2 
 |-  ( j = k -> ( 2 x. j ) = ( 2 x. k ) )
13 12 oveq1d 
 |-  ( j = k -> ( ( 2 x. j ) + 1 ) = ( ( 2 x. k ) + 1 ) )
14 id 
 |-  ( j = k -> j = k )
15 13 14 oveq12d 
 |-  ( j = k -> ( ( ( 2 x. j ) + 1 ) _C j ) = ( ( ( 2 x. k ) + 1 ) _C k ) )
16 11 15 breq12d 
 |-  ( j = k -> ( ( 2 ^ ( j + 1 ) ) < ( ( ( 2 x. j ) + 1 ) _C j ) <-> ( 2 ^ ( k + 1 ) ) < ( ( ( 2 x. k ) + 1 ) _C k ) ) )
17 oveq1 
 |-  ( j = ( k + 1 ) -> ( j + 1 ) = ( ( k + 1 ) + 1 ) )
18 17 oveq2d 
 |-  ( j = ( k + 1 ) -> ( 2 ^ ( j + 1 ) ) = ( 2 ^ ( ( k + 1 ) + 1 ) ) )
19 oveq2 
 |-  ( j = ( k + 1 ) -> ( 2 x. j ) = ( 2 x. ( k + 1 ) ) )
20 19 oveq1d 
 |-  ( j = ( k + 1 ) -> ( ( 2 x. j ) + 1 ) = ( ( 2 x. ( k + 1 ) ) + 1 ) )
21 id 
 |-  ( j = ( k + 1 ) -> j = ( k + 1 ) )
22 20 21 oveq12d 
 |-  ( j = ( k + 1 ) -> ( ( ( 2 x. j ) + 1 ) _C j ) = ( ( ( 2 x. ( k + 1 ) ) + 1 ) _C ( k + 1 ) ) )
23 18 22 breq12d 
 |-  ( j = ( k + 1 ) -> ( ( 2 ^ ( j + 1 ) ) < ( ( ( 2 x. j ) + 1 ) _C j ) <-> ( 2 ^ ( ( k + 1 ) + 1 ) ) < ( ( ( 2 x. ( k + 1 ) ) + 1 ) _C ( k + 1 ) ) ) )
24 oveq1 
 |-  ( j = N -> ( j + 1 ) = ( N + 1 ) )
25 24 oveq2d 
 |-  ( j = N -> ( 2 ^ ( j + 1 ) ) = ( 2 ^ ( N + 1 ) ) )
26 oveq2 
 |-  ( j = N -> ( 2 x. j ) = ( 2 x. N ) )
27 26 oveq1d 
 |-  ( j = N -> ( ( 2 x. j ) + 1 ) = ( ( 2 x. N ) + 1 ) )
28 id 
 |-  ( j = N -> j = N )
29 27 28 oveq12d 
 |-  ( j = N -> ( ( ( 2 x. j ) + 1 ) _C j ) = ( ( ( 2 x. N ) + 1 ) _C N ) )
30 25 29 breq12d 
 |-  ( j = N -> ( ( 2 ^ ( j + 1 ) ) < ( ( ( 2 x. j ) + 1 ) _C j ) <-> ( 2 ^ ( N + 1 ) ) < ( ( ( 2 x. N ) + 1 ) _C N ) ) )
31 8lt10 
 |-  8 < ; 1 0
32 eqid 
 |-  8 = 8
33 cu2 
 |-  ( 2 ^ 3 ) = 8
34 32 33 eqtr4i 
 |-  8 = ( 2 ^ 3 )
35 5bc2eq10 
 |-  ( 5 _C 2 ) = ; 1 0
36 35 eqcomi 
 |-  ; 1 0 = ( 5 _C 2 )
37 34 36 breq12i 
 |-  ( 8 < ; 1 0 <-> ( 2 ^ 3 ) < ( 5 _C 2 ) )
38 31 37 mpbi 
 |-  ( 2 ^ 3 ) < ( 5 _C 2 )
39 df-3 
 |-  3 = ( 2 + 1 )
40 39 oveq2i 
 |-  ( 2 ^ 3 ) = ( 2 ^ ( 2 + 1 ) )
41 eqid 
 |-  5 = 5
42 2t2e4 
 |-  ( 2 x. 2 ) = 4
43 42 oveq1i 
 |-  ( ( 2 x. 2 ) + 1 ) = ( 4 + 1 )
44 4p1e5 
 |-  ( 4 + 1 ) = 5
45 43 44 eqtri 
 |-  ( ( 2 x. 2 ) + 1 ) = 5
46 41 45 eqtr4i 
 |-  5 = ( ( 2 x. 2 ) + 1 )
47 46 oveq1i 
 |-  ( 5 _C 2 ) = ( ( ( 2 x. 2 ) + 1 ) _C 2 )
48 40 47 breq12i 
 |-  ( ( 2 ^ 3 ) < ( 5 _C 2 ) <-> ( 2 ^ ( 2 + 1 ) ) < ( ( ( 2 x. 2 ) + 1 ) _C 2 ) )
49 38 48 mpbi 
 |-  ( 2 ^ ( 2 + 1 ) ) < ( ( ( 2 x. 2 ) + 1 ) _C 2 )
50 49 a1i 
 |-  ( ph -> ( 2 ^ ( 2 + 1 ) ) < ( ( ( 2 x. 2 ) + 1 ) _C 2 ) )
51 2re 
 |-  2 e. RR
52 51 a1i 
 |-  ( ( ph /\ ( 2 ^ ( k + 1 ) ) < ( ( ( 2 x. k ) + 1 ) _C k ) /\ ( k e. ZZ /\ 2 <_ k ) ) -> 2 e. RR )
53 simpl 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> k e. ZZ )
54 0red 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> 0 e. RR )
55 51 a1i 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> 2 e. RR )
56 53 zred 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> k e. RR )
57 2pos 
 |-  0 < 2
58 57 a1i 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> 0 < 2 )
59 simpr 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> 2 <_ k )
60 54 55 56 58 59 ltletrd 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> 0 < k )
61 53 60 jca 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> ( k e. ZZ /\ 0 < k ) )
62 elnnz 
 |-  ( k e. NN <-> ( k e. ZZ /\ 0 < k ) )
63 61 62 sylibr 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> k e. NN )
64 nnnn0 
 |-  ( k e. NN -> k e. NN0 )
65 63 64 syl 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> k e. NN0 )
66 65 nn0red 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> k e. RR )
67 54 55 66 58 59 ltletrd 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> 0 < k )
68 53 67 jca 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> ( k e. ZZ /\ 0 < k ) )
69 68 62 sylibr 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> k e. NN )
70 69 nnred 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> k e. RR )
71 70 3ad2ant3 
 |-  ( ( ph /\ ( 2 ^ ( k + 1 ) ) < ( ( ( 2 x. k ) + 1 ) _C k ) /\ ( k e. ZZ /\ 2 <_ k ) ) -> k e. RR )
72 52 71 remulcld 
 |-  ( ( ph /\ ( 2 ^ ( k + 1 ) ) < ( ( ( 2 x. k ) + 1 ) _C k ) /\ ( k e. ZZ /\ 2 <_ k ) ) -> ( 2 x. k ) e. RR )
73 3re 
 |-  3 e. RR
74 73 a1i 
 |-  ( ( ph /\ ( 2 ^ ( k + 1 ) ) < ( ( ( 2 x. k ) + 1 ) _C k ) /\ ( k e. ZZ /\ 2 <_ k ) ) -> 3 e. RR )
75 72 74 readdcld 
 |-  ( ( ph /\ ( 2 ^ ( k + 1 ) ) < ( ( ( 2 x. k ) + 1 ) _C k ) /\ ( k e. ZZ /\ 2 <_ k ) ) -> ( ( 2 x. k ) + 3 ) e. RR )
76 71 52 readdcld 
 |-  ( ( ph /\ ( 2 ^ ( k + 1 ) ) < ( ( ( 2 x. k ) + 1 ) _C k ) /\ ( k e. ZZ /\ 2 <_ k ) ) -> ( k + 2 ) e. RR )
77 70 55 readdcld 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> ( k + 2 ) e. RR )
78 69 nngt0d 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> 0 < k )
79 2rp 
 |-  2 e. RR+
80 79 a1i 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> 2 e. RR+ )
81 70 80 ltaddrpd 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> k < ( k + 2 ) )
82 54 70 77 78 81 lttrd 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> 0 < ( k + 2 ) )
83 54 82 ltned 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> 0 =/= ( k + 2 ) )
84 83 necomd 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> ( k + 2 ) =/= 0 )
85 84 3ad2ant3 
 |-  ( ( ph /\ ( 2 ^ ( k + 1 ) ) < ( ( ( 2 x. k ) + 1 ) _C k ) /\ ( k e. ZZ /\ 2 <_ k ) ) -> ( k + 2 ) =/= 0 )
86 75 76 85 redivcld 
 |-  ( ( ph /\ ( 2 ^ ( k + 1 ) ) < ( ( ( 2 x. k ) + 1 ) _C k ) /\ ( k e. ZZ /\ 2 <_ k ) ) -> ( ( ( 2 x. k ) + 3 ) / ( k + 2 ) ) e. RR )
87 52 86 remulcld 
 |-  ( ( ph /\ ( 2 ^ ( k + 1 ) ) < ( ( ( 2 x. k ) + 1 ) _C k ) /\ ( k e. ZZ /\ 2 <_ k ) ) -> ( 2 x. ( ( ( 2 x. k ) + 3 ) / ( k + 2 ) ) ) e. RR )
88 1nn0 
 |-  1 e. NN0
89 88 a1i 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> 1 e. NN0 )
90 65 89 nn0addcld 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> ( k + 1 ) e. NN0 )
91 55 90 reexpcld 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> ( 2 ^ ( k + 1 ) ) e. RR )
92 91 3ad2ant3 
 |-  ( ( ph /\ ( 2 ^ ( k + 1 ) ) < ( ( ( 2 x. k ) + 1 ) _C k ) /\ ( k e. ZZ /\ 2 <_ k ) ) -> ( 2 ^ ( k + 1 ) ) e. RR )
93 2nn0 
 |-  2 e. NN0
94 93 a1i 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> 2 e. NN0 )
95 94 65 nn0mulcld 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> ( 2 x. k ) e. NN0 )
96 95 89 nn0addcld 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> ( ( 2 x. k ) + 1 ) e. NN0 )
97 bccl 
 |-  ( ( ( ( 2 x. k ) + 1 ) e. NN0 /\ k e. ZZ ) -> ( ( ( 2 x. k ) + 1 ) _C k ) e. NN0 )
98 96 53 97 syl2anc 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> ( ( ( 2 x. k ) + 1 ) _C k ) e. NN0 )
99 98 nn0red 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> ( ( ( 2 x. k ) + 1 ) _C k ) e. RR )
100 99 3ad2ant3 
 |-  ( ( ph /\ ( 2 ^ ( k + 1 ) ) < ( ( ( 2 x. k ) + 1 ) _C k ) /\ ( k e. ZZ /\ 2 <_ k ) ) -> ( ( ( 2 x. k ) + 1 ) _C k ) e. RR )
101 0le2 
 |-  0 <_ 2
102 101 a1i 
 |-  ( ( ph /\ ( 2 ^ ( k + 1 ) ) < ( ( ( 2 x. k ) + 1 ) _C k ) /\ ( k e. ZZ /\ 2 <_ k ) ) -> 0 <_ 2 )
103 eqid 
 |-  2 = 2
104 2t1e2 
 |-  ( 2 x. 1 ) = 2
105 103 104 eqtr4i 
 |-  2 = ( 2 x. 1 )
106 105 a1i 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> 2 = ( 2 x. 1 ) )
107 1red 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> 1 e. RR )
108 55 70 remulcld 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> ( 2 x. k ) e. RR )
109 73 a1i 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> 3 e. RR )
110 108 109 readdcld 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> ( ( 2 x. k ) + 3 ) e. RR )
111 110 77 84 redivcld 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> ( ( ( 2 x. k ) + 3 ) / ( k + 2 ) ) e. RR )
112 nnrp 
 |-  ( k e. NN -> k e. RR+ )
113 79 a1i 
 |-  ( k e. NN -> 2 e. RR+ )
114 112 113 rpaddcld 
 |-  ( k e. NN -> ( k + 2 ) e. RR+ )
115 114 rpcnd 
 |-  ( k e. NN -> ( k + 2 ) e. CC )
116 115 mulid1d 
 |-  ( k e. NN -> ( ( k + 2 ) x. 1 ) = ( k + 2 ) )
117 nnre 
 |-  ( k e. NN -> k e. RR )
118 51 a1i 
 |-  ( k e. NN -> 2 e. RR )
119 118 117 remulcld 
 |-  ( k e. NN -> ( 2 x. k ) e. RR )
120 73 a1i 
 |-  ( k e. NN -> 3 e. RR )
121 112 rpge0d 
 |-  ( k e. NN -> 0 <_ k )
122 1le2 
 |-  1 <_ 2
123 122 a1i 
 |-  ( k e. NN -> 1 <_ 2 )
124 117 118 121 123 lemulge12d 
 |-  ( k e. NN -> k <_ ( 2 x. k ) )
125 2lt3 
 |-  2 < 3
126 125 a1i 
 |-  ( k e. NN -> 2 < 3 )
127 117 118 119 120 124 126 leltaddd 
 |-  ( k e. NN -> ( k + 2 ) < ( ( 2 x. k ) + 3 ) )
128 116 127 eqbrtrd 
 |-  ( k e. NN -> ( ( k + 2 ) x. 1 ) < ( ( 2 x. k ) + 3 ) )
129 1red 
 |-  ( k e. NN -> 1 e. RR )
130 119 120 readdcld 
 |-  ( k e. NN -> ( ( 2 x. k ) + 3 ) e. RR )
131 129 130 114 ltmuldiv2d 
 |-  ( k e. NN -> ( ( ( k + 2 ) x. 1 ) < ( ( 2 x. k ) + 3 ) <-> 1 < ( ( ( 2 x. k ) + 3 ) / ( k + 2 ) ) ) )
132 128 131 mpbid 
 |-  ( k e. NN -> 1 < ( ( ( 2 x. k ) + 3 ) / ( k + 2 ) ) )
133 69 132 syl 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> 1 < ( ( ( 2 x. k ) + 3 ) / ( k + 2 ) ) )
134 107 111 80 133 ltmul2dd 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> ( 2 x. 1 ) < ( 2 x. ( ( ( 2 x. k ) + 3 ) / ( k + 2 ) ) ) )
135 106 134 eqbrtrd 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> 2 < ( 2 x. ( ( ( 2 x. k ) + 3 ) / ( k + 2 ) ) ) )
136 135 3ad2ant3 
 |-  ( ( ph /\ ( 2 ^ ( k + 1 ) ) < ( ( ( 2 x. k ) + 1 ) _C k ) /\ ( k e. ZZ /\ 2 <_ k ) ) -> 2 < ( 2 x. ( ( ( 2 x. k ) + 3 ) / ( k + 2 ) ) ) )
137 101 a1i 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> 0 <_ 2 )
138 55 90 137 expge0d 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> 0 <_ ( 2 ^ ( k + 1 ) ) )
139 138 3ad2ant3 
 |-  ( ( ph /\ ( 2 ^ ( k + 1 ) ) < ( ( ( 2 x. k ) + 1 ) _C k ) /\ ( k e. ZZ /\ 2 <_ k ) ) -> 0 <_ ( 2 ^ ( k + 1 ) ) )
140 simp2 
 |-  ( ( ph /\ ( 2 ^ ( k + 1 ) ) < ( ( ( 2 x. k ) + 1 ) _C k ) /\ ( k e. ZZ /\ 2 <_ k ) ) -> ( 2 ^ ( k + 1 ) ) < ( ( ( 2 x. k ) + 1 ) _C k ) )
141 52 87 92 100 102 136 139 140 ltmul12ad 
 |-  ( ( ph /\ ( 2 ^ ( k + 1 ) ) < ( ( ( 2 x. k ) + 1 ) _C k ) /\ ( k e. ZZ /\ 2 <_ k ) ) -> ( 2 x. ( 2 ^ ( k + 1 ) ) ) < ( ( 2 x. ( ( ( 2 x. k ) + 3 ) / ( k + 2 ) ) ) x. ( ( ( 2 x. k ) + 1 ) _C k ) ) )
142 2cnd 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> 2 e. CC )
143 142 89 90 expaddd 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> ( 2 ^ ( ( k + 1 ) + 1 ) ) = ( ( 2 ^ ( k + 1 ) ) x. ( 2 ^ 1 ) ) )
144 142 90 expcld 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> ( 2 ^ ( k + 1 ) ) e. CC )
145 142 89 expcld 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> ( 2 ^ 1 ) e. CC )
146 144 145 mulcomd 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> ( ( 2 ^ ( k + 1 ) ) x. ( 2 ^ 1 ) ) = ( ( 2 ^ 1 ) x. ( 2 ^ ( k + 1 ) ) ) )
147 142 exp1d 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> ( 2 ^ 1 ) = 2 )
148 147 oveq1d 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> ( ( 2 ^ 1 ) x. ( 2 ^ ( k + 1 ) ) ) = ( 2 x. ( 2 ^ ( k + 1 ) ) ) )
149 eqidd 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> ( 2 x. ( 2 ^ ( k + 1 ) ) ) = ( 2 x. ( 2 ^ ( k + 1 ) ) ) )
150 146 148 149 3eqtrd 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> ( ( 2 ^ ( k + 1 ) ) x. ( 2 ^ 1 ) ) = ( 2 x. ( 2 ^ ( k + 1 ) ) ) )
151 143 150 eqtrd 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> ( 2 ^ ( ( k + 1 ) + 1 ) ) = ( 2 x. ( 2 ^ ( k + 1 ) ) ) )
152 151 eqcomd 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> ( 2 x. ( 2 ^ ( k + 1 ) ) ) = ( 2 ^ ( ( k + 1 ) + 1 ) ) )
153 152 3ad2ant3 
 |-  ( ( ph /\ ( 2 ^ ( k + 1 ) ) < ( ( ( 2 x. k ) + 1 ) _C k ) /\ ( k e. ZZ /\ 2 <_ k ) ) -> ( 2 x. ( 2 ^ ( k + 1 ) ) ) = ( 2 ^ ( ( k + 1 ) + 1 ) ) )
154 65 2np3bcnp1 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> ( ( ( 2 x. ( k + 1 ) ) + 1 ) _C ( k + 1 ) ) = ( ( ( ( 2 x. k ) + 1 ) _C k ) x. ( 2 x. ( ( ( 2 x. k ) + 3 ) / ( k + 2 ) ) ) ) )
155 98 nn0cnd 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> ( ( ( 2 x. k ) + 1 ) _C k ) e. CC )
156 69 nncnd 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> k e. CC )
157 142 156 mulcld 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> ( 2 x. k ) e. CC )
158 3cn 
 |-  3 e. CC
159 158 a1i 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> 3 e. CC )
160 157 159 addcld 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> ( ( 2 x. k ) + 3 ) e. CC )
161 156 142 addcld 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> ( k + 2 ) e. CC )
162 160 161 84 divcld 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> ( ( ( 2 x. k ) + 3 ) / ( k + 2 ) ) e. CC )
163 142 162 mulcld 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> ( 2 x. ( ( ( 2 x. k ) + 3 ) / ( k + 2 ) ) ) e. CC )
164 155 163 mulcomd 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> ( ( ( ( 2 x. k ) + 1 ) _C k ) x. ( 2 x. ( ( ( 2 x. k ) + 3 ) / ( k + 2 ) ) ) ) = ( ( 2 x. ( ( ( 2 x. k ) + 3 ) / ( k + 2 ) ) ) x. ( ( ( 2 x. k ) + 1 ) _C k ) ) )
165 154 164 eqtrd 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> ( ( ( 2 x. ( k + 1 ) ) + 1 ) _C ( k + 1 ) ) = ( ( 2 x. ( ( ( 2 x. k ) + 3 ) / ( k + 2 ) ) ) x. ( ( ( 2 x. k ) + 1 ) _C k ) ) )
166 165 eqcomd 
 |-  ( ( k e. ZZ /\ 2 <_ k ) -> ( ( 2 x. ( ( ( 2 x. k ) + 3 ) / ( k + 2 ) ) ) x. ( ( ( 2 x. k ) + 1 ) _C k ) ) = ( ( ( 2 x. ( k + 1 ) ) + 1 ) _C ( k + 1 ) ) )
167 166 3ad2ant3 
 |-  ( ( ph /\ ( 2 ^ ( k + 1 ) ) < ( ( ( 2 x. k ) + 1 ) _C k ) /\ ( k e. ZZ /\ 2 <_ k ) ) -> ( ( 2 x. ( ( ( 2 x. k ) + 3 ) / ( k + 2 ) ) ) x. ( ( ( 2 x. k ) + 1 ) _C k ) ) = ( ( ( 2 x. ( k + 1 ) ) + 1 ) _C ( k + 1 ) ) )
168 153 167 breq12d 
 |-  ( ( ph /\ ( 2 ^ ( k + 1 ) ) < ( ( ( 2 x. k ) + 1 ) _C k ) /\ ( k e. ZZ /\ 2 <_ k ) ) -> ( ( 2 x. ( 2 ^ ( k + 1 ) ) ) < ( ( 2 x. ( ( ( 2 x. k ) + 3 ) / ( k + 2 ) ) ) x. ( ( ( 2 x. k ) + 1 ) _C k ) ) <-> ( 2 ^ ( ( k + 1 ) + 1 ) ) < ( ( ( 2 x. ( k + 1 ) ) + 1 ) _C ( k + 1 ) ) ) )
169 141 168 mpbid 
 |-  ( ( ph /\ ( 2 ^ ( k + 1 ) ) < ( ( ( 2 x. k ) + 1 ) _C k ) /\ ( k e. ZZ /\ 2 <_ k ) ) -> ( 2 ^ ( ( k + 1 ) + 1 ) ) < ( ( ( 2 x. ( k + 1 ) ) + 1 ) _C ( k + 1 ) ) )
170 2z 
 |-  2 e. ZZ
171 170 a1i 
 |-  ( ph -> 2 e. ZZ )
172 9 16 23 30 50 169 171 1 2 uzindd 
 |-  ( ph -> ( 2 ^ ( N + 1 ) ) < ( ( ( 2 x. N ) + 1 ) _C N ) )