Metamath Proof Explorer

Theorem rmygeid

Description: Y(n) increases faster than n. Used implicitly without proof or comment in lemma 2.27 of JonesMatijasevic p. 697. (Contributed by Stefan O'Rear, 4-Oct-2014)

Ref Expression
Assertion rmygeid 
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> N <_ ( A rmY N ) )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( a = 0 -> a = 0 )
2 oveq2 
 |-  ( a = 0 -> ( A rmY a ) = ( A rmY 0 ) )
3 1 2 breq12d 
 |-  ( a = 0 -> ( a <_ ( A rmY a ) <-> 0 <_ ( A rmY 0 ) ) )
4 3 imbi2d 
 |-  ( a = 0 -> ( ( A e. ( ZZ>= ` 2 ) -> a <_ ( A rmY a ) ) <-> ( A e. ( ZZ>= ` 2 ) -> 0 <_ ( A rmY 0 ) ) ) )
5 id 
 |-  ( a = b -> a = b )
6 oveq2 
 |-  ( a = b -> ( A rmY a ) = ( A rmY b ) )
7 5 6 breq12d 
 |-  ( a = b -> ( a <_ ( A rmY a ) <-> b <_ ( A rmY b ) ) )
8 7 imbi2d 
 |-  ( a = b -> ( ( A e. ( ZZ>= ` 2 ) -> a <_ ( A rmY a ) ) <-> ( A e. ( ZZ>= ` 2 ) -> b <_ ( A rmY b ) ) ) )
9 id 
 |-  ( a = ( b + 1 ) -> a = ( b + 1 ) )
10 oveq2 
 |-  ( a = ( b + 1 ) -> ( A rmY a ) = ( A rmY ( b + 1 ) ) )
11 9 10 breq12d 
 |-  ( a = ( b + 1 ) -> ( a <_ ( A rmY a ) <-> ( b + 1 ) <_ ( A rmY ( b + 1 ) ) ) )
12 11 imbi2d 
 |-  ( a = ( b + 1 ) -> ( ( A e. ( ZZ>= ` 2 ) -> a <_ ( A rmY a ) ) <-> ( A e. ( ZZ>= ` 2 ) -> ( b + 1 ) <_ ( A rmY ( b + 1 ) ) ) ) )
13 id 
 |-  ( a = N -> a = N )
14 oveq2 
 |-  ( a = N -> ( A rmY a ) = ( A rmY N ) )
15 13 14 breq12d 
 |-  ( a = N -> ( a <_ ( A rmY a ) <-> N <_ ( A rmY N ) ) )
16 15 imbi2d 
 |-  ( a = N -> ( ( A e. ( ZZ>= ` 2 ) -> a <_ ( A rmY a ) ) <-> ( A e. ( ZZ>= ` 2 ) -> N <_ ( A rmY N ) ) ) )
17 0le0 
 |-  0 <_ 0
18 rmy0 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A rmY 0 ) = 0 )
19 17 18 breqtrrid 
 |-  ( A e. ( ZZ>= ` 2 ) -> 0 <_ ( A rmY 0 ) )
20 nn0z 
 |-  ( b e. NN0 -> b e. ZZ )
21 20 3ad2ant1 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ b <_ ( A rmY b ) ) -> b e. ZZ )
22 21 peano2zd 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ b <_ ( A rmY b ) ) -> ( b + 1 ) e. ZZ )
23 22 zred 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ b <_ ( A rmY b ) ) -> ( b + 1 ) e. RR )
24 simp2 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ b <_ ( A rmY b ) ) -> A e. ( ZZ>= ` 2 ) )
25 frmy 
 |-  rmY : ( ( ZZ>= ` 2 ) X. ZZ ) --> ZZ
26 25 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ b e. ZZ ) -> ( A rmY b ) e. ZZ )
27 24 21 26 syl2anc 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ b <_ ( A rmY b ) ) -> ( A rmY b ) e. ZZ )
28 27 peano2zd 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ b <_ ( A rmY b ) ) -> ( ( A rmY b ) + 1 ) e. ZZ )
29 28 zred 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ b <_ ( A rmY b ) ) -> ( ( A rmY b ) + 1 ) e. RR )
30 25 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( b + 1 ) e. ZZ ) -> ( A rmY ( b + 1 ) ) e. ZZ )
31 24 22 30 syl2anc 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ b <_ ( A rmY b ) ) -> ( A rmY ( b + 1 ) ) e. ZZ )
32 31 zred 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ b <_ ( A rmY b ) ) -> ( A rmY ( b + 1 ) ) e. RR )
33 nn0re 
 |-  ( b e. NN0 -> b e. RR )
34 33 3ad2ant1 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ b <_ ( A rmY b ) ) -> b e. RR )
35 27 zred 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ b <_ ( A rmY b ) ) -> ( A rmY b ) e. RR )
36 1red 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ b <_ ( A rmY b ) ) -> 1 e. RR )
37 simp3 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ b <_ ( A rmY b ) ) -> b <_ ( A rmY b ) )
38 34 35 36 37 leadd1dd 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ b <_ ( A rmY b ) ) -> ( b + 1 ) <_ ( ( A rmY b ) + 1 ) )
39 34 ltp1d 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ b <_ ( A rmY b ) ) -> b < ( b + 1 ) )
40 ltrmy 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ b e. ZZ /\ ( b + 1 ) e. ZZ ) -> ( b < ( b + 1 ) <-> ( A rmY b ) < ( A rmY ( b + 1 ) ) ) )
41 24 21 22 40 syl3anc 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ b <_ ( A rmY b ) ) -> ( b < ( b + 1 ) <-> ( A rmY b ) < ( A rmY ( b + 1 ) ) ) )
42 39 41 mpbid 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ b <_ ( A rmY b ) ) -> ( A rmY b ) < ( A rmY ( b + 1 ) ) )
43 zltp1le 
 |-  ( ( ( A rmY b ) e. ZZ /\ ( A rmY ( b + 1 ) ) e. ZZ ) -> ( ( A rmY b ) < ( A rmY ( b + 1 ) ) <-> ( ( A rmY b ) + 1 ) <_ ( A rmY ( b + 1 ) ) ) )
44 27 31 43 syl2anc 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ b <_ ( A rmY b ) ) -> ( ( A rmY b ) < ( A rmY ( b + 1 ) ) <-> ( ( A rmY b ) + 1 ) <_ ( A rmY ( b + 1 ) ) ) )
45 42 44 mpbid 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ b <_ ( A rmY b ) ) -> ( ( A rmY b ) + 1 ) <_ ( A rmY ( b + 1 ) ) )
46 23 29 32 38 45 letrd 
 |-  ( ( b e. NN0 /\ A e. ( ZZ>= ` 2 ) /\ b <_ ( A rmY b ) ) -> ( b + 1 ) <_ ( A rmY ( b + 1 ) ) )
47 46 3exp 
 |-  ( b e. NN0 -> ( A e. ( ZZ>= ` 2 ) -> ( b <_ ( A rmY b ) -> ( b + 1 ) <_ ( A rmY ( b + 1 ) ) ) ) )
48 47 a2d 
 |-  ( b e. NN0 -> ( ( A e. ( ZZ>= ` 2 ) -> b <_ ( A rmY b ) ) -> ( A e. ( ZZ>= ` 2 ) -> ( b + 1 ) <_ ( A rmY ( b + 1 ) ) ) ) )
49 4 8 12 16 19 48 nn0ind 
 |-  ( N e. NN0 -> ( A e. ( ZZ>= ` 2 ) -> N <_ ( A rmY N ) ) )
50 49 impcom 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> N <_ ( A rmY N ) )