Metamath Proof Explorer

Theorem jm2.17b

Description: Weak form of the second half of lemma 2.17 of JonesMatijasevic p. 696, allowing induction to start lower. (Contributed by Stefan O'Rear, 15-Oct-2014)

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

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( a = 0 -> ( a + 1 ) = ( 0 + 1 ) )
2 1 oveq2d 
 |-  ( a = 0 -> ( A rmY ( a + 1 ) ) = ( A rmY ( 0 + 1 ) ) )
3 oveq2 
 |-  ( a = 0 -> ( ( 2 x. A ) ^ a ) = ( ( 2 x. A ) ^ 0 ) )
4 2 3 breq12d 
 |-  ( a = 0 -> ( ( A rmY ( a + 1 ) ) <_ ( ( 2 x. A ) ^ a ) <-> ( A rmY ( 0 + 1 ) ) <_ ( ( 2 x. A ) ^ 0 ) ) )
5 4 imbi2d 
 |-  ( a = 0 -> ( ( A e. ( ZZ>= ` 2 ) -> ( A rmY ( a + 1 ) ) <_ ( ( 2 x. A ) ^ a ) ) <-> ( A e. ( ZZ>= ` 2 ) -> ( A rmY ( 0 + 1 ) ) <_ ( ( 2 x. A ) ^ 0 ) ) ) )
6 oveq1 
 |-  ( a = b -> ( a + 1 ) = ( b + 1 ) )
7 6 oveq2d 
 |-  ( a = b -> ( A rmY ( a + 1 ) ) = ( A rmY ( b + 1 ) ) )
8 oveq2 
 |-  ( a = b -> ( ( 2 x. A ) ^ a ) = ( ( 2 x. A ) ^ b ) )
9 7 8 breq12d 
 |-  ( a = b -> ( ( A rmY ( a + 1 ) ) <_ ( ( 2 x. A ) ^ a ) <-> ( A rmY ( b + 1 ) ) <_ ( ( 2 x. A ) ^ b ) ) )
10 9 imbi2d 
 |-  ( a = b -> ( ( A e. ( ZZ>= ` 2 ) -> ( A rmY ( a + 1 ) ) <_ ( ( 2 x. A ) ^ a ) ) <-> ( A e. ( ZZ>= ` 2 ) -> ( A rmY ( b + 1 ) ) <_ ( ( 2 x. A ) ^ b ) ) ) )
11 oveq1 
 |-  ( a = ( b + 1 ) -> ( a + 1 ) = ( ( b + 1 ) + 1 ) )
12 11 oveq2d 
 |-  ( a = ( b + 1 ) -> ( A rmY ( a + 1 ) ) = ( A rmY ( ( b + 1 ) + 1 ) ) )
13 oveq2 
 |-  ( a = ( b + 1 ) -> ( ( 2 x. A ) ^ a ) = ( ( 2 x. A ) ^ ( b + 1 ) ) )
14 12 13 breq12d 
 |-  ( a = ( b + 1 ) -> ( ( A rmY ( a + 1 ) ) <_ ( ( 2 x. A ) ^ a ) <-> ( A rmY ( ( b + 1 ) + 1 ) ) <_ ( ( 2 x. A ) ^ ( b + 1 ) ) ) )
15 14 imbi2d 
 |-  ( a = ( b + 1 ) -> ( ( A e. ( ZZ>= ` 2 ) -> ( A rmY ( a + 1 ) ) <_ ( ( 2 x. A ) ^ a ) ) <-> ( A e. ( ZZ>= ` 2 ) -> ( A rmY ( ( b + 1 ) + 1 ) ) <_ ( ( 2 x. A ) ^ ( b + 1 ) ) ) ) )
16 oveq1 
 |-  ( a = N -> ( a + 1 ) = ( N + 1 ) )
17 16 oveq2d 
 |-  ( a = N -> ( A rmY ( a + 1 ) ) = ( A rmY ( N + 1 ) ) )
18 oveq2 
 |-  ( a = N -> ( ( 2 x. A ) ^ a ) = ( ( 2 x. A ) ^ N ) )
19 17 18 breq12d 
 |-  ( a = N -> ( ( A rmY ( a + 1 ) ) <_ ( ( 2 x. A ) ^ a ) <-> ( A rmY ( N + 1 ) ) <_ ( ( 2 x. A ) ^ N ) ) )
20 19 imbi2d 
 |-  ( a = N -> ( ( A e. ( ZZ>= ` 2 ) -> ( A rmY ( a + 1 ) ) <_ ( ( 2 x. A ) ^ a ) ) <-> ( A e. ( ZZ>= ` 2 ) -> ( A rmY ( N + 1 ) ) <_ ( ( 2 x. A ) ^ N ) ) ) )
21 1le1 
 |-  1 <_ 1
22 0p1e1 
 |-  ( 0 + 1 ) = 1
23 22 oveq2i 
 |-  ( A rmY ( 0 + 1 ) ) = ( A rmY 1 )
24 rmy1 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A rmY 1 ) = 1 )
25 23 24 eqtrid 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A rmY ( 0 + 1 ) ) = 1 )
26 2re 
 |-  2 e. RR
27 eluzelre 
 |-  ( A e. ( ZZ>= ` 2 ) -> A e. RR )
28 remulcl 
 |-  ( ( 2 e. RR /\ A e. RR ) -> ( 2 x. A ) e. RR )
29 26 27 28 sylancr 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( 2 x. A ) e. RR )
30 29 recnd 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( 2 x. A ) e. CC )
31 30 exp0d 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( 2 x. A ) ^ 0 ) = 1 )
32 25 31 breq12d 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A rmY ( 0 + 1 ) ) <_ ( ( 2 x. A ) ^ 0 ) <-> 1 <_ 1 ) )
33 21 32 mpbiri 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A rmY ( 0 + 1 ) ) <_ ( ( 2 x. A ) ^ 0 ) )
34 simpr 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> A e. ( ZZ>= ` 2 ) )
35 nn0z 
 |-  ( b e. NN0 -> b e. ZZ )
36 35 adantr 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> b e. ZZ )
37 36 peano2zd 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( b + 1 ) e. ZZ )
38 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 ) ) ) )
39 34 37 38 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 ) ) ) )
40 rmxypos 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ b e. NN0 ) -> ( 0 < ( A rmX b ) /\ 0 <_ ( A rmY b ) ) )
41 40 simprd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ b e. NN0 ) -> 0 <_ ( A rmY b ) )
42 41 ancoms 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> 0 <_ ( A rmY b ) )
43 nn0re 
 |-  ( b e. NN0 -> b e. RR )
44 43 adantr 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> b e. RR )
45 44 recnd 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> b e. CC )
46 ax-1cn 
 |-  1 e. CC
47 pncan 
 |-  ( ( b e. CC /\ 1 e. CC ) -> ( ( b + 1 ) - 1 ) = b )
48 45 46 47 sylancl 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( ( b + 1 ) - 1 ) = b )
49 48 oveq2d 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( A rmY ( ( b + 1 ) - 1 ) ) = ( A rmY b ) )
50 42 49 breqtrrd 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> 0 <_ ( A rmY ( ( b + 1 ) - 1 ) ) )
51 27 adantl 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> A e. RR )
52 26 51 28 sylancr 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( 2 x. A ) e. RR )
53 frmy 
 |-  rmY : ( ( ZZ>= ` 2 ) X. ZZ ) --> ZZ
54 53 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( b + 1 ) e. ZZ ) -> ( A rmY ( b + 1 ) ) e. ZZ )
55 54 zred 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( b + 1 ) e. ZZ ) -> ( A rmY ( b + 1 ) ) e. RR )
56 34 37 55 syl2anc 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( A rmY ( b + 1 ) ) e. RR )
57 52 56 remulcld 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( ( 2 x. A ) x. ( A rmY ( b + 1 ) ) ) e. RR )
58 53 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ b e. ZZ ) -> ( A rmY b ) e. ZZ )
59 58 zred 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ b e. ZZ ) -> ( A rmY b ) e. RR )
60 34 36 59 syl2anc 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( A rmY b ) e. RR )
61 49 60 eqeltrd 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( A rmY ( ( b + 1 ) - 1 ) ) e. RR )
62 57 61 subge02d 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( 0 <_ ( A rmY ( ( b + 1 ) - 1 ) ) <-> ( ( ( 2 x. A ) x. ( A rmY ( b + 1 ) ) ) - ( A rmY ( ( b + 1 ) - 1 ) ) ) <_ ( ( 2 x. A ) x. ( A rmY ( b + 1 ) ) ) ) )
63 50 62 mpbid 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( ( ( 2 x. A ) x. ( A rmY ( b + 1 ) ) ) - ( A rmY ( ( b + 1 ) - 1 ) ) ) <_ ( ( 2 x. A ) x. ( A rmY ( b + 1 ) ) ) )
64 39 63 eqbrtrd 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( A rmY ( ( b + 1 ) + 1 ) ) <_ ( ( 2 x. A ) x. ( A rmY ( b + 1 ) ) ) )
65 64 3adant3 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ ( A rmY ( b + 1 ) ) <_ ( ( 2 x. A ) ^ b ) ) -> ( A rmY ( ( b + 1 ) + 1 ) ) <_ ( ( 2 x. A ) x. ( A rmY ( b + 1 ) ) ) )
66 simpl 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> b e. NN0 )
67 52 66 reexpcld 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( ( 2 x. A ) ^ b ) e. RR )
68 2nn 
 |-  2 e. NN
69 eluz2nn 
 |-  ( A e. ( ZZ>= ` 2 ) -> A e. NN )
70 nnmulcl 
 |-  ( ( 2 e. NN /\ A e. NN ) -> ( 2 x. A ) e. NN )
71 68 69 70 sylancr 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( 2 x. A ) e. NN )
72 71 nngt0d 
 |-  ( A e. ( ZZ>= ` 2 ) -> 0 < ( 2 x. A ) )
73 72 adantl 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> 0 < ( 2 x. A ) )
74 lemul2 
 |-  ( ( ( A rmY ( b + 1 ) ) e. RR /\ ( ( 2 x. A ) ^ b ) e. RR /\ ( ( 2 x. A ) e. RR /\ 0 < ( 2 x. A ) ) ) -> ( ( A rmY ( b + 1 ) ) <_ ( ( 2 x. A ) ^ b ) <-> ( ( 2 x. A ) x. ( A rmY ( b + 1 ) ) ) <_ ( ( 2 x. A ) x. ( ( 2 x. A ) ^ b ) ) ) )
75 56 67 52 73 74 syl112anc 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( ( A rmY ( b + 1 ) ) <_ ( ( 2 x. A ) ^ b ) <-> ( ( 2 x. A ) x. ( A rmY ( b + 1 ) ) ) <_ ( ( 2 x. A ) x. ( ( 2 x. A ) ^ b ) ) ) )
76 75 biimp3a 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ ( A rmY ( b + 1 ) ) <_ ( ( 2 x. A ) ^ b ) ) -> ( ( 2 x. A ) x. ( A rmY ( b + 1 ) ) ) <_ ( ( 2 x. A ) x. ( ( 2 x. A ) ^ b ) ) )
77 52 recnd 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( 2 x. A ) e. CC )
78 77 66 expp1d 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( ( 2 x. A ) ^ ( b + 1 ) ) = ( ( ( 2 x. A ) ^ b ) x. ( 2 x. A ) ) )
79 67 recnd 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( ( 2 x. A ) ^ b ) e. CC )
80 79 77 mulcomd 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( ( ( 2 x. A ) ^ b ) x. ( 2 x. A ) ) = ( ( 2 x. A ) x. ( ( 2 x. A ) ^ b ) ) )
81 78 80 eqtrd 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( ( 2 x. A ) ^ ( b + 1 ) ) = ( ( 2 x. A ) x. ( ( 2 x. A ) ^ b ) ) )
82 81 3adant3 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ ( A rmY ( b + 1 ) ) <_ ( ( 2 x. A ) ^ b ) ) -> ( ( 2 x. A ) ^ ( b + 1 ) ) = ( ( 2 x. A ) x. ( ( 2 x. A ) ^ b ) ) )
83 76 82 breqtrrd 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ ( A rmY ( b + 1 ) ) <_ ( ( 2 x. A ) ^ b ) ) -> ( ( 2 x. A ) x. ( A rmY ( b + 1 ) ) ) <_ ( ( 2 x. A ) ^ ( b + 1 ) ) )
84 37 peano2zd 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( ( b + 1 ) + 1 ) e. ZZ )
85 53 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( ( b + 1 ) + 1 ) e. ZZ ) -> ( A rmY ( ( b + 1 ) + 1 ) ) e. ZZ )
86 85 zred 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( ( b + 1 ) + 1 ) e. ZZ ) -> ( A rmY ( ( b + 1 ) + 1 ) ) e. RR )
87 34 84 86 syl2anc 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( A rmY ( ( b + 1 ) + 1 ) ) e. RR )
88 peano2nn0 
 |-  ( b e. NN0 -> ( b + 1 ) e. NN0 )
89 88 adantr 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( b + 1 ) e. NN0 )
90 52 89 reexpcld 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( ( 2 x. A ) ^ ( b + 1 ) ) e. RR )
91 letr 
 |-  ( ( ( A rmY ( ( b + 1 ) + 1 ) ) e. RR /\ ( ( 2 x. A ) x. ( A rmY ( b + 1 ) ) ) e. RR /\ ( ( 2 x. A ) ^ ( b + 1 ) ) e. RR ) -> ( ( ( A rmY ( ( b + 1 ) + 1 ) ) <_ ( ( 2 x. A ) x. ( A rmY ( b + 1 ) ) ) /\ ( ( 2 x. A ) x. ( A rmY ( b + 1 ) ) ) <_ ( ( 2 x. A ) ^ ( b + 1 ) ) ) -> ( A rmY ( ( b + 1 ) + 1 ) ) <_ ( ( 2 x. A ) ^ ( b + 1 ) ) ) )
92 87 57 90 91 syl3anc 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) ) -> ( ( ( A rmY ( ( b + 1 ) + 1 ) ) <_ ( ( 2 x. A ) x. ( A rmY ( b + 1 ) ) ) /\ ( ( 2 x. A ) x. ( A rmY ( b + 1 ) ) ) <_ ( ( 2 x. A ) ^ ( b + 1 ) ) ) -> ( A rmY ( ( b + 1 ) + 1 ) ) <_ ( ( 2 x. A ) ^ ( b + 1 ) ) ) )
93 92 3adant3 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ ( A rmY ( b + 1 ) ) <_ ( ( 2 x. A ) ^ b ) ) -> ( ( ( A rmY ( ( b + 1 ) + 1 ) ) <_ ( ( 2 x. A ) x. ( A rmY ( b + 1 ) ) ) /\ ( ( 2 x. A ) x. ( A rmY ( b + 1 ) ) ) <_ ( ( 2 x. A ) ^ ( b + 1 ) ) ) -> ( A rmY ( ( b + 1 ) + 1 ) ) <_ ( ( 2 x. A ) ^ ( b + 1 ) ) ) )
94 65 83 93 mp2and 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ ( A rmY ( b + 1 ) ) <_ ( ( 2 x. A ) ^ b ) ) -> ( A rmY ( ( b + 1 ) + 1 ) ) <_ ( ( 2 x. A ) ^ ( b + 1 ) ) )
95 94 3exp 
 |-  ( b e. NN0 -> ( A e. ( ZZ>= ` 2 ) -> ( ( A rmY ( b + 1 ) ) <_ ( ( 2 x. A ) ^ b ) -> ( A rmY ( ( b + 1 ) + 1 ) ) <_ ( ( 2 x. A ) ^ ( b + 1 ) ) ) ) )
96 95 a2d 
 |-  ( b e. NN0 -> ( ( A e. ( ZZ>= ` 2 ) -> ( A rmY ( b + 1 ) ) <_ ( ( 2 x. A ) ^ b ) ) -> ( A e. ( ZZ>= ` 2 ) -> ( A rmY ( ( b + 1 ) + 1 ) ) <_ ( ( 2 x. A ) ^ ( b + 1 ) ) ) ) )
97 5 10 15 20 33 96 nn0ind 
 |-  ( N e. NN0 -> ( A e. ( ZZ>= ` 2 ) -> ( A rmY ( N + 1 ) ) <_ ( ( 2 x. A ) ^ N ) ) )
98 97 impcom 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> ( A rmY ( N + 1 ) ) <_ ( ( 2 x. A ) ^ N ) )