Metamath Proof Explorer

Theorem jm2.24nn

Description: X(n) is strictly greater than Y(n) + Y(n-1). Lemma 2.24 of JonesMatijasevic p. 697 restricted to NN . (Contributed by Stefan O'Rear, 3-Oct-2014)

Ref Expression
Assertion jm2.24nn 
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( ( A rmY ( N - 1 ) ) + ( A rmY N ) ) < ( A rmX N ) )

Proof

Step Hyp Ref Expression
1 nnz 
 |-  ( N e. NN -> N e. ZZ )
2 1z 
 |-  1 e. ZZ
3 zsubcl 
 |-  ( ( N e. ZZ /\ 1 e. ZZ ) -> ( N - 1 ) e. ZZ )
4 1 2 3 sylancl 
 |-  ( N e. NN -> ( N - 1 ) e. ZZ )
5 frmy 
 |-  rmY : ( ( ZZ>= ` 2 ) X. ZZ ) --> ZZ
6 5 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( N - 1 ) e. ZZ ) -> ( A rmY ( N - 1 ) ) e. ZZ )
7 4 6 sylan2 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( A rmY ( N - 1 ) ) e. ZZ )
8 7 zred 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( A rmY ( N - 1 ) ) e. RR )
9 5 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmY N ) e. ZZ )
10 1 9 sylan2 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( A rmY N ) e. ZZ )
11 10 zred 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( A rmY N ) e. RR )
12 8 11 readdcld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( ( A rmY ( N - 1 ) ) + ( A rmY N ) ) e. RR )
13 2re 
 |-  2 e. RR
14 remulcl 
 |-  ( ( 2 e. RR /\ ( A rmY N ) e. RR ) -> ( 2 x. ( A rmY N ) ) e. RR )
15 13 11 14 sylancr 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( 2 x. ( A rmY N ) ) e. RR )
16 15 8 resubcld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( ( 2 x. ( A rmY N ) ) - ( A rmY ( N - 1 ) ) ) e. RR )
17 frmx 
 |-  rmX : ( ( ZZ>= ` 2 ) X. ZZ ) --> NN0
18 17 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX N ) e. NN0 )
19 1 18 sylan2 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( A rmX N ) e. NN0 )
20 19 nn0red 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( A rmX N ) e. RR )
21 11 8 resubcld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( ( A rmY N ) - ( A rmY ( N - 1 ) ) ) e. RR )
22 remulcl 
 |-  ( ( 2 e. RR /\ ( A rmY ( N - 1 ) ) e. RR ) -> ( 2 x. ( A rmY ( N - 1 ) ) ) e. RR )
23 13 8 22 sylancr 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( 2 x. ( A rmY ( N - 1 ) ) ) e. RR )
24 eluzelre 
 |-  ( A e. ( ZZ>= ` 2 ) -> A e. RR )
25 24 adantr 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> A e. RR )
26 25 8 remulcld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( A x. ( A rmY ( N - 1 ) ) ) e. RR )
27 8 25 remulcld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( ( A rmY ( N - 1 ) ) x. A ) e. RR )
28 17 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( N - 1 ) e. ZZ ) -> ( A rmX ( N - 1 ) ) e. NN0 )
29 4 28 sylan2 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( A rmX ( N - 1 ) ) e. NN0 )
30 29 nn0red 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( A rmX ( N - 1 ) ) e. RR )
31 27 30 readdcld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( ( ( A rmY ( N - 1 ) ) x. A ) + ( A rmX ( N - 1 ) ) ) e. RR )
32 13 a1i 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> 2 e. RR )
33 nnm1nn0 
 |-  ( N e. NN -> ( N - 1 ) e. NN0 )
34 rmxypos 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( N - 1 ) e. NN0 ) -> ( 0 < ( A rmX ( N - 1 ) ) /\ 0 <_ ( A rmY ( N - 1 ) ) ) )
35 34 simprd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( N - 1 ) e. NN0 ) -> 0 <_ ( A rmY ( N - 1 ) ) )
36 33 35 sylan2 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> 0 <_ ( A rmY ( N - 1 ) ) )
37 eluzle 
 |-  ( A e. ( ZZ>= ` 2 ) -> 2 <_ A )
38 37 adantr 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> 2 <_ A )
39 32 25 8 36 38 lemul1ad 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( 2 x. ( A rmY ( N - 1 ) ) ) <_ ( A x. ( A rmY ( N - 1 ) ) ) )
40 25 recnd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> A e. CC )
41 8 recnd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( A rmY ( N - 1 ) ) e. CC )
42 40 41 mulcomd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( A x. ( A rmY ( N - 1 ) ) ) = ( ( A rmY ( N - 1 ) ) x. A ) )
43 34 simpld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( N - 1 ) e. NN0 ) -> 0 < ( A rmX ( N - 1 ) ) )
44 33 43 sylan2 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> 0 < ( A rmX ( N - 1 ) ) )
45 30 27 ltaddposd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( 0 < ( A rmX ( N - 1 ) ) <-> ( ( A rmY ( N - 1 ) ) x. A ) < ( ( ( A rmY ( N - 1 ) ) x. A ) + ( A rmX ( N - 1 ) ) ) ) )
46 44 45 mpbid 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( ( A rmY ( N - 1 ) ) x. A ) < ( ( ( A rmY ( N - 1 ) ) x. A ) + ( A rmX ( N - 1 ) ) ) )
47 42 46 eqbrtrd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( A x. ( A rmY ( N - 1 ) ) ) < ( ( ( A rmY ( N - 1 ) ) x. A ) + ( A rmX ( N - 1 ) ) ) )
48 23 26 31 39 47 lelttrd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( 2 x. ( A rmY ( N - 1 ) ) ) < ( ( ( A rmY ( N - 1 ) ) x. A ) + ( A rmX ( N - 1 ) ) ) )
49 41 2timesd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( 2 x. ( A rmY ( N - 1 ) ) ) = ( ( A rmY ( N - 1 ) ) + ( A rmY ( N - 1 ) ) ) )
50 rmyp1 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( N - 1 ) e. ZZ ) -> ( A rmY ( ( N - 1 ) + 1 ) ) = ( ( ( A rmY ( N - 1 ) ) x. A ) + ( A rmX ( N - 1 ) ) ) )
51 4 50 sylan2 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( A rmY ( ( N - 1 ) + 1 ) ) = ( ( ( A rmY ( N - 1 ) ) x. A ) + ( A rmX ( N - 1 ) ) ) )
52 nnre 
 |-  ( N e. NN -> N e. RR )
53 52 adantl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> N e. RR )
54 53 recnd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> N e. CC )
55 ax-1cn 
 |-  1 e. CC
56 npcan 
 |-  ( ( N e. CC /\ 1 e. CC ) -> ( ( N - 1 ) + 1 ) = N )
57 54 55 56 sylancl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( ( N - 1 ) + 1 ) = N )
58 57 oveq2d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( A rmY ( ( N - 1 ) + 1 ) ) = ( A rmY N ) )
59 51 58 eqtr3d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( ( ( A rmY ( N - 1 ) ) x. A ) + ( A rmX ( N - 1 ) ) ) = ( A rmY N ) )
60 48 49 59 3brtr3d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( ( A rmY ( N - 1 ) ) + ( A rmY ( N - 1 ) ) ) < ( A rmY N ) )
61 8 8 11 ltaddsubd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( ( ( A rmY ( N - 1 ) ) + ( A rmY ( N - 1 ) ) ) < ( A rmY N ) <-> ( A rmY ( N - 1 ) ) < ( ( A rmY N ) - ( A rmY ( N - 1 ) ) ) ) )
62 60 61 mpbid 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( A rmY ( N - 1 ) ) < ( ( A rmY N ) - ( A rmY ( N - 1 ) ) ) )
63 8 21 11 62 ltadd1dd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( ( A rmY ( N - 1 ) ) + ( A rmY N ) ) < ( ( ( A rmY N ) - ( A rmY ( N - 1 ) ) ) + ( A rmY N ) ) )
64 11 recnd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( A rmY N ) e. CC )
65 64 2timesd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( 2 x. ( A rmY N ) ) = ( ( A rmY N ) + ( A rmY N ) ) )
66 65 oveq1d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( ( 2 x. ( A rmY N ) ) - ( A rmY ( N - 1 ) ) ) = ( ( ( A rmY N ) + ( A rmY N ) ) - ( A rmY ( N - 1 ) ) ) )
67 64 64 41 addsubd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( ( ( A rmY N ) + ( A rmY N ) ) - ( A rmY ( N - 1 ) ) ) = ( ( ( A rmY N ) - ( A rmY ( N - 1 ) ) ) + ( A rmY N ) ) )
68 66 67 eqtrd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( ( 2 x. ( A rmY N ) ) - ( A rmY ( N - 1 ) ) ) = ( ( ( A rmY N ) - ( A rmY ( N - 1 ) ) ) + ( A rmY N ) ) )
69 63 68 breqtrrd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( ( A rmY ( N - 1 ) ) + ( A rmY N ) ) < ( ( 2 x. ( A rmY N ) ) - ( A rmY ( N - 1 ) ) ) )
70 25 11 remulcld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( A x. ( A rmY N ) ) e. RR )
71 rmy0 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A rmY 0 ) = 0 )
72 71 adantr 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( A rmY 0 ) = 0 )
73 nngt0 
 |-  ( N e. NN -> 0 < N )
74 73 adantl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> 0 < N )
75 simpl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> A e. ( ZZ>= ` 2 ) )
76 0zd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> 0 e. ZZ )
77 1 adantl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> N e. ZZ )
78 ltrmy 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ 0 e. ZZ /\ N e. ZZ ) -> ( 0 < N <-> ( A rmY 0 ) < ( A rmY N ) ) )
79 75 76 77 78 syl3anc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( 0 < N <-> ( A rmY 0 ) < ( A rmY N ) ) )
80 74 79 mpbid 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( A rmY 0 ) < ( A rmY N ) )
81 72 80 eqbrtrrd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> 0 < ( A rmY N ) )
82 lemul1 
 |-  ( ( 2 e. RR /\ A e. RR /\ ( ( A rmY N ) e. RR /\ 0 < ( A rmY N ) ) ) -> ( 2 <_ A <-> ( 2 x. ( A rmY N ) ) <_ ( A x. ( A rmY N ) ) ) )
83 32 25 11 81 82 syl112anc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( 2 <_ A <-> ( 2 x. ( A rmY N ) ) <_ ( A x. ( A rmY N ) ) ) )
84 38 83 mpbid 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( 2 x. ( A rmY N ) ) <_ ( A x. ( A rmY N ) ) )
85 15 70 8 84 lesub1dd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( ( 2 x. ( A rmY N ) ) - ( A rmY ( N - 1 ) ) ) <_ ( ( A x. ( A rmY N ) ) - ( A rmY ( N - 1 ) ) ) )
86 rmym1 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmY ( N - 1 ) ) = ( ( ( A rmY N ) x. A ) - ( A rmX N ) ) )
87 1 86 sylan2 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( A rmY ( N - 1 ) ) = ( ( ( A rmY N ) x. A ) - ( A rmX N ) ) )
88 64 40 mulcomd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( ( A rmY N ) x. A ) = ( A x. ( A rmY N ) ) )
89 88 oveq1d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( ( ( A rmY N ) x. A ) - ( A rmX N ) ) = ( ( A x. ( A rmY N ) ) - ( A rmX N ) ) )
90 87 89 eqtr2d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( ( A x. ( A rmY N ) ) - ( A rmX N ) ) = ( A rmY ( N - 1 ) ) )
91 70 recnd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( A x. ( A rmY N ) ) e. CC )
92 20 recnd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( A rmX N ) e. CC )
93 subsub23 
 |-  ( ( ( A x. ( A rmY N ) ) e. CC /\ ( A rmX N ) e. CC /\ ( A rmY ( N - 1 ) ) e. CC ) -> ( ( ( A x. ( A rmY N ) ) - ( A rmX N ) ) = ( A rmY ( N - 1 ) ) <-> ( ( A x. ( A rmY N ) ) - ( A rmY ( N - 1 ) ) ) = ( A rmX N ) ) )
94 91 92 41 93 syl3anc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( ( ( A x. ( A rmY N ) ) - ( A rmX N ) ) = ( A rmY ( N - 1 ) ) <-> ( ( A x. ( A rmY N ) ) - ( A rmY ( N - 1 ) ) ) = ( A rmX N ) ) )
95 90 94 mpbid 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( ( A x. ( A rmY N ) ) - ( A rmY ( N - 1 ) ) ) = ( A rmX N ) )
96 85 95 breqtrd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( ( 2 x. ( A rmY N ) ) - ( A rmY ( N - 1 ) ) ) <_ ( A rmX N ) )
97 12 16 20 69 96 ltletrd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( ( A rmY ( N - 1 ) ) + ( A rmY N ) ) < ( A rmX N ) )