Metamath Proof Explorer

Theorem jm2.17a

Description: First half of lemma 2.17 of JonesMatijasevic p. 696. (Contributed by Stefan O'Rear, 14-Oct-2014)

Ref Expression
Assertion jm2.17a 
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> ( ( ( 2 x. A ) - 1 ) ^ N ) <_ ( A rmY ( N + 1 ) ) )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( a = 0 -> ( ( ( 2 x. A ) - 1 ) ^ a ) = ( ( ( 2 x. A ) - 1 ) ^ 0 ) )
2 oveq1 
 |-  ( a = 0 -> ( a + 1 ) = ( 0 + 1 ) )
3 2 oveq2d 
 |-  ( a = 0 -> ( A rmY ( a + 1 ) ) = ( A rmY ( 0 + 1 ) ) )
4 1 3 breq12d 
 |-  ( a = 0 -> ( ( ( ( 2 x. A ) - 1 ) ^ a ) <_ ( A rmY ( a + 1 ) ) <-> ( ( ( 2 x. A ) - 1 ) ^ 0 ) <_ ( A rmY ( 0 + 1 ) ) ) )
5 4 imbi2d 
 |-  ( a = 0 -> ( ( A e. ( ZZ>= ` 2 ) -> ( ( ( 2 x. A ) - 1 ) ^ a ) <_ ( A rmY ( a + 1 ) ) ) <-> ( A e. ( ZZ>= ` 2 ) -> ( ( ( 2 x. A ) - 1 ) ^ 0 ) <_ ( A rmY ( 0 + 1 ) ) ) ) )
6 oveq2 
 |-  ( a = b -> ( ( ( 2 x. A ) - 1 ) ^ a ) = ( ( ( 2 x. A ) - 1 ) ^ b ) )
7 oveq1 
 |-  ( a = b -> ( a + 1 ) = ( b + 1 ) )
8 7 oveq2d 
 |-  ( a = b -> ( A rmY ( a + 1 ) ) = ( A rmY ( b + 1 ) ) )
9 6 8 breq12d 
 |-  ( a = b -> ( ( ( ( 2 x. A ) - 1 ) ^ a ) <_ ( A rmY ( a + 1 ) ) <-> ( ( ( 2 x. A ) - 1 ) ^ b ) <_ ( A rmY ( b + 1 ) ) ) )
10 9 imbi2d 
 |-  ( a = b -> ( ( A e. ( ZZ>= ` 2 ) -> ( ( ( 2 x. A ) - 1 ) ^ a ) <_ ( A rmY ( a + 1 ) ) ) <-> ( A e. ( ZZ>= ` 2 ) -> ( ( ( 2 x. A ) - 1 ) ^ b ) <_ ( A rmY ( b + 1 ) ) ) ) )
11 oveq2 
 |-  ( a = ( b + 1 ) -> ( ( ( 2 x. A ) - 1 ) ^ a ) = ( ( ( 2 x. A ) - 1 ) ^ ( b + 1 ) ) )
12 oveq1 
 |-  ( a = ( b + 1 ) -> ( a + 1 ) = ( ( b + 1 ) + 1 ) )
13 12 oveq2d 
 |-  ( a = ( b + 1 ) -> ( A rmY ( a + 1 ) ) = ( A rmY ( ( b + 1 ) + 1 ) ) )
14 11 13 breq12d 
 |-  ( a = ( b + 1 ) -> ( ( ( ( 2 x. A ) - 1 ) ^ a ) <_ ( A rmY ( a + 1 ) ) <-> ( ( ( 2 x. A ) - 1 ) ^ ( b + 1 ) ) <_ ( A rmY ( ( b + 1 ) + 1 ) ) ) )
15 14 imbi2d 
 |-  ( a = ( b + 1 ) -> ( ( A e. ( ZZ>= ` 2 ) -> ( ( ( 2 x. A ) - 1 ) ^ a ) <_ ( A rmY ( a + 1 ) ) ) <-> ( A e. ( ZZ>= ` 2 ) -> ( ( ( 2 x. A ) - 1 ) ^ ( b + 1 ) ) <_ ( A rmY ( ( b + 1 ) + 1 ) ) ) ) )
16 oveq2 
 |-  ( a = N -> ( ( ( 2 x. A ) - 1 ) ^ a ) = ( ( ( 2 x. A ) - 1 ) ^ N ) )
17 oveq1 
 |-  ( a = N -> ( a + 1 ) = ( N + 1 ) )
18 17 oveq2d 
 |-  ( a = N -> ( A rmY ( a + 1 ) ) = ( A rmY ( N + 1 ) ) )
19 16 18 breq12d 
 |-  ( a = N -> ( ( ( ( 2 x. A ) - 1 ) ^ a ) <_ ( A rmY ( a + 1 ) ) <-> ( ( ( 2 x. A ) - 1 ) ^ N ) <_ ( A rmY ( N + 1 ) ) ) )
20 19 imbi2d 
 |-  ( a = N -> ( ( A e. ( ZZ>= ` 2 ) -> ( ( ( 2 x. A ) - 1 ) ^ a ) <_ ( A rmY ( a + 1 ) ) ) <-> ( A e. ( ZZ>= ` 2 ) -> ( ( ( 2 x. A ) - 1 ) ^ N ) <_ ( A rmY ( N + 1 ) ) ) ) )
21 1le1 
 |-  1 <_ 1
22 21 a1i 
 |-  ( A e. ( ZZ>= ` 2 ) -> 1 <_ 1 )
23 2cn 
 |-  2 e. CC
24 eluzelcn 
 |-  ( A e. ( ZZ>= ` 2 ) -> A e. CC )
25 mulcl 
 |-  ( ( 2 e. CC /\ A e. CC ) -> ( 2 x. A ) e. CC )
26 23 24 25 sylancr 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( 2 x. A ) e. CC )
27 ax-1cn 
 |-  1 e. CC
28 subcl 
 |-  ( ( ( 2 x. A ) e. CC /\ 1 e. CC ) -> ( ( 2 x. A ) - 1 ) e. CC )
29 26 27 28 sylancl 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( 2 x. A ) - 1 ) e. CC )
30 29 exp0d 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( ( 2 x. A ) - 1 ) ^ 0 ) = 1 )
31 0p1e1 
 |-  ( 0 + 1 ) = 1
32 31 oveq2i 
 |-  ( A rmY ( 0 + 1 ) ) = ( A rmY 1 )
33 rmy1 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A rmY 1 ) = 1 )
34 32 33 syl5eq 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A rmY ( 0 + 1 ) ) = 1 )
35 22 30 34 3brtr4d 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( ( 2 x. A ) - 1 ) ^ 0 ) <_ ( A rmY ( 0 + 1 ) ) )
36 2re 
 |-  2 e. RR
37 eluzelre 
 |-  ( A e. ( ZZ>= ` 2 ) -> A e. RR )
38 37 adantl 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> A e. RR )
39 remulcl 
 |-  ( ( 2 e. RR /\ A e. RR ) -> ( 2 x. A ) e. RR )
40 36 38 39 sylancr 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( 2 x. A ) e. RR )
41 1re 
 |-  1 e. RR
42 resubcl 
 |-  ( ( ( 2 x. A ) e. RR /\ 1 e. RR ) -> ( ( 2 x. A ) - 1 ) e. RR )
43 40 41 42 sylancl 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( ( 2 x. A ) - 1 ) e. RR )
44 peano2nn0 
 |-  ( b e. NN0 -> ( b + 1 ) e. NN0 )
45 44 adantr 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( b + 1 ) e. NN0 )
46 43 45 reexpcld 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( ( ( 2 x. A ) - 1 ) ^ ( b + 1 ) ) e. RR )
47 46 3adant3 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ ( ( ( 2 x. A ) - 1 ) ^ b ) <_ ( A rmY ( b + 1 ) ) ) -> ( ( ( 2 x. A ) - 1 ) ^ ( b + 1 ) ) e. RR )
48 simpr 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> A e. ( ZZ>= ` 2 ) )
49 nn0z 
 |-  ( b e. NN0 -> b e. ZZ )
50 49 adantr 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> b e. ZZ )
51 50 peano2zd 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( b + 1 ) e. ZZ )
52 frmy 
 |-  rmY : ( ( ZZ>= ` 2 ) X. ZZ ) --> ZZ
53 52 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( b + 1 ) e. ZZ ) -> ( A rmY ( b + 1 ) ) e. ZZ )
54 53 zred 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( b + 1 ) e. ZZ ) -> ( A rmY ( b + 1 ) ) e. RR )
55 48 51 54 syl2anc 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( A rmY ( b + 1 ) ) e. RR )
56 55 43 remulcld 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( ( A rmY ( b + 1 ) ) x. ( ( 2 x. A ) - 1 ) ) e. RR )
57 56 3adant3 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ ( ( ( 2 x. A ) - 1 ) ^ b ) <_ ( A rmY ( b + 1 ) ) ) -> ( ( A rmY ( b + 1 ) ) x. ( ( 2 x. A ) - 1 ) ) e. RR )
58 51 peano2zd 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( ( b + 1 ) + 1 ) e. ZZ )
59 52 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( ( b + 1 ) + 1 ) e. ZZ ) -> ( A rmY ( ( b + 1 ) + 1 ) ) e. ZZ )
60 59 zred 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( ( b + 1 ) + 1 ) e. ZZ ) -> ( A rmY ( ( b + 1 ) + 1 ) ) e. RR )
61 48 58 60 syl2anc 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( A rmY ( ( b + 1 ) + 1 ) ) e. RR )
62 61 3adant3 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ ( ( ( 2 x. A ) - 1 ) ^ b ) <_ ( A rmY ( b + 1 ) ) ) -> ( A rmY ( ( b + 1 ) + 1 ) ) e. RR )
63 29 3ad2ant2 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ ( ( ( 2 x. A ) - 1 ) ^ b ) <_ ( A rmY ( b + 1 ) ) ) -> ( ( 2 x. A ) - 1 ) e. CC )
64 simp1 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ ( ( ( 2 x. A ) - 1 ) ^ b ) <_ ( A rmY ( b + 1 ) ) ) -> b e. NN0 )
65 63 64 expp1d 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ ( ( ( 2 x. A ) - 1 ) ^ b ) <_ ( A rmY ( b + 1 ) ) ) -> ( ( ( 2 x. A ) - 1 ) ^ ( b + 1 ) ) = ( ( ( ( 2 x. A ) - 1 ) ^ b ) x. ( ( 2 x. A ) - 1 ) ) )
66 simpl 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> b e. NN0 )
67 43 66 reexpcld 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( ( ( 2 x. A ) - 1 ) ^ b ) e. RR )
68 2nn 
 |-  2 e. NN
69 eluz2nn 
 |-  ( A e. ( ZZ>= ` 2 ) -> A e. NN )
70 69 adantl 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> A e. NN )
71 nnmulcl 
 |-  ( ( 2 e. NN /\ A e. NN ) -> ( 2 x. A ) e. NN )
72 68 70 71 sylancr 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( 2 x. A ) e. NN )
73 nnm1nn0 
 |-  ( ( 2 x. A ) e. NN -> ( ( 2 x. A ) - 1 ) e. NN0 )
74 nn0ge0 
 |-  ( ( ( 2 x. A ) - 1 ) e. NN0 -> 0 <_ ( ( 2 x. A ) - 1 ) )
75 72 73 74 3syl 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> 0 <_ ( ( 2 x. A ) - 1 ) )
76 43 75 jca 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( ( ( 2 x. A ) - 1 ) e. RR /\ 0 <_ ( ( 2 x. A ) - 1 ) ) )
77 67 55 76 3jca 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( ( ( ( 2 x. A ) - 1 ) ^ b ) e. RR /\ ( A rmY ( b + 1 ) ) e. RR /\ ( ( ( 2 x. A ) - 1 ) e. RR /\ 0 <_ ( ( 2 x. A ) - 1 ) ) ) )
78 lemul1a 
 |-  ( ( ( ( ( ( 2 x. A ) - 1 ) ^ b ) e. RR /\ ( A rmY ( b + 1 ) ) e. RR /\ ( ( ( 2 x. A ) - 1 ) e. RR /\ 0 <_ ( ( 2 x. A ) - 1 ) ) ) /\ ( ( ( 2 x. A ) - 1 ) ^ b ) <_ ( A rmY ( b + 1 ) ) ) -> ( ( ( ( 2 x. A ) - 1 ) ^ b ) x. ( ( 2 x. A ) - 1 ) ) <_ ( ( A rmY ( b + 1 ) ) x. ( ( 2 x. A ) - 1 ) ) )
79 77 78 stoic3 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ ( ( ( 2 x. A ) - 1 ) ^ b ) <_ ( A rmY ( b + 1 ) ) ) -> ( ( ( ( 2 x. A ) - 1 ) ^ b ) x. ( ( 2 x. A ) - 1 ) ) <_ ( ( A rmY ( b + 1 ) ) x. ( ( 2 x. A ) - 1 ) ) )
80 65 79 eqbrtrd 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ ( ( ( 2 x. A ) - 1 ) ^ b ) <_ ( A rmY ( b + 1 ) ) ) -> ( ( ( 2 x. A ) - 1 ) ^ ( b + 1 ) ) <_ ( ( A rmY ( b + 1 ) ) x. ( ( 2 x. A ) - 1 ) ) )
81 nn0cn 
 |-  ( b e. NN0 -> b e. CC )
82 81 adantr 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> b e. CC )
83 pncan 
 |-  ( ( b e. CC /\ 1 e. CC ) -> ( ( b + 1 ) - 1 ) = b )
84 82 27 83 sylancl 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( ( b + 1 ) - 1 ) = b )
85 84 oveq2d 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( A rmY ( ( b + 1 ) - 1 ) ) = ( A rmY b ) )
86 52 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ b e. ZZ ) -> ( A rmY b ) e. ZZ )
87 86 zred 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ b e. ZZ ) -> ( A rmY b ) e. RR )
88 48 50 87 syl2anc 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( A rmY b ) e. RR )
89 85 88 eqeltrd 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( A rmY ( ( b + 1 ) - 1 ) ) e. RR )
90 remulcl 
 |-  ( ( ( A rmY ( b + 1 ) ) e. RR /\ 1 e. RR ) -> ( ( A rmY ( b + 1 ) ) x. 1 ) e. RR )
91 55 41 90 sylancl 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( ( A rmY ( b + 1 ) ) x. 1 ) e. RR )
92 40 55 remulcld 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( ( 2 x. A ) x. ( A rmY ( b + 1 ) ) ) e. RR )
93 nn0re 
 |-  ( b e. NN0 -> b e. RR )
94 93 adantr 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> b e. RR )
95 94 lep1d 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> b <_ ( b + 1 ) )
96 lermy 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ b e. ZZ /\ ( b + 1 ) e. ZZ ) -> ( b <_ ( b + 1 ) <-> ( A rmY b ) <_ ( A rmY ( b + 1 ) ) ) )
97 48 50 51 96 syl3anc 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( b <_ ( b + 1 ) <-> ( A rmY b ) <_ ( A rmY ( b + 1 ) ) ) )
98 95 97 mpbid 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( A rmY b ) <_ ( A rmY ( b + 1 ) ) )
99 55 recnd 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( A rmY ( b + 1 ) ) e. CC )
100 99 mulid1d 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( ( A rmY ( b + 1 ) ) x. 1 ) = ( A rmY ( b + 1 ) ) )
101 98 85 100 3brtr4d 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( A rmY ( ( b + 1 ) - 1 ) ) <_ ( ( A rmY ( b + 1 ) ) x. 1 ) )
102 89 91 92 101 lesub2dd 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( ( ( 2 x. A ) x. ( A rmY ( b + 1 ) ) ) - ( ( A rmY ( b + 1 ) ) x. 1 ) ) <_ ( ( ( 2 x. A ) x. ( A rmY ( b + 1 ) ) ) - ( A rmY ( ( b + 1 ) - 1 ) ) ) )
103 40 recnd 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( 2 x. A ) e. CC )
104 27 a1i 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> 1 e. CC )
105 99 103 104 subdid 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( ( A rmY ( b + 1 ) ) x. ( ( 2 x. A ) - 1 ) ) = ( ( ( A rmY ( b + 1 ) ) x. ( 2 x. A ) ) - ( ( A rmY ( b + 1 ) ) x. 1 ) ) )
106 99 103 mulcomd 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( ( A rmY ( b + 1 ) ) x. ( 2 x. A ) ) = ( ( 2 x. A ) x. ( A rmY ( b + 1 ) ) ) )
107 106 oveq1d 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( ( ( A rmY ( b + 1 ) ) x. ( 2 x. A ) ) - ( ( A rmY ( b + 1 ) ) x. 1 ) ) = ( ( ( 2 x. A ) x. ( A rmY ( b + 1 ) ) ) - ( ( A rmY ( b + 1 ) ) x. 1 ) ) )
108 105 107 eqtrd 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( ( A rmY ( b + 1 ) ) x. ( ( 2 x. A ) - 1 ) ) = ( ( ( 2 x. A ) x. ( A rmY ( b + 1 ) ) ) - ( ( A rmY ( b + 1 ) ) x. 1 ) ) )
109 rmyluc2 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( b + 1 ) e. ZZ ) -> ( A rmY ( ( b + 1 ) + 1 ) ) = ( ( ( 2 x. A ) x. ( A rmY ( b + 1 ) ) ) - ( A rmY ( ( b + 1 ) - 1 ) ) ) )
110 48 51 109 syl2anc 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( A rmY ( ( b + 1 ) + 1 ) ) = ( ( ( 2 x. A ) x. ( A rmY ( b + 1 ) ) ) - ( A rmY ( ( b + 1 ) - 1 ) ) ) )
111 102 108 110 3brtr4d 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( ( A rmY ( b + 1 ) ) x. ( ( 2 x. A ) - 1 ) ) <_ ( A rmY ( ( b + 1 ) + 1 ) ) )
112 111 3adant3 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ ( ( ( 2 x. A ) - 1 ) ^ b ) <_ ( A rmY ( b + 1 ) ) ) -> ( ( A rmY ( b + 1 ) ) x. ( ( 2 x. A ) - 1 ) ) <_ ( A rmY ( ( b + 1 ) + 1 ) ) )
113 47 57 62 80 112 letrd 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ ( ( ( 2 x. A ) - 1 ) ^ b ) <_ ( A rmY ( b + 1 ) ) ) -> ( ( ( 2 x. A ) - 1 ) ^ ( b + 1 ) ) <_ ( A rmY ( ( b + 1 ) + 1 ) ) )
114 113 3exp 
 |-  ( b e. NN0 -> ( A e. ( ZZ>= ` 2 ) -> ( ( ( ( 2 x. A ) - 1 ) ^ b ) <_ ( A rmY ( b + 1 ) ) -> ( ( ( 2 x. A ) - 1 ) ^ ( b + 1 ) ) <_ ( A rmY ( ( b + 1 ) + 1 ) ) ) ) )
115 114 a2d 
 |-  ( b e. NN0 -> ( ( A e. ( ZZ>= ` 2 ) -> ( ( ( 2 x. A ) - 1 ) ^ b ) <_ ( A rmY ( b + 1 ) ) ) -> ( A e. ( ZZ>= ` 2 ) -> ( ( ( 2 x. A ) - 1 ) ^ ( b + 1 ) ) <_ ( A rmY ( ( b + 1 ) + 1 ) ) ) ) )
116 5 10 15 20 35 115 nn0ind 
 |-  ( N e. NN0 -> ( A e. ( ZZ>= ` 2 ) -> ( ( ( 2 x. A ) - 1 ) ^ N ) <_ ( A rmY ( N + 1 ) ) ) )
117 116 impcom 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> ( ( ( 2 x. A ) - 1 ) ^ N ) <_ ( A rmY ( N + 1 ) ) )