Metamath Proof Explorer

Theorem jm2.24

Description: Lemma 2.24 of JonesMatijasevic p. 697 extended to ZZ . Could be eliminated with a more careful proof of jm2.26lem3 . (Contributed by Stefan O'Rear, 3-Oct-2014)

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

Proof

Step Hyp Ref Expression
1 simpll 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ N <_ 0 ) -> A e. ( ZZ>= ` 2 ) )
2 peano2zm 
 |-  ( N e. ZZ -> ( N - 1 ) e. ZZ )
3 2 ad2antlr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ N <_ 0 ) -> ( N - 1 ) e. ZZ )
4 frmy 
 |-  rmY : ( ( ZZ>= ` 2 ) X. ZZ ) --> ZZ
5 4 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( N - 1 ) e. ZZ ) -> ( A rmY ( N - 1 ) ) e. ZZ )
6 1 3 5 syl2anc 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ N <_ 0 ) -> ( A rmY ( N - 1 ) ) e. ZZ )
7 6 zred 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ N <_ 0 ) -> ( A rmY ( N - 1 ) ) e. RR )
8 4 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmY N ) e. ZZ )
9 8 zred 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmY N ) e. RR )
10 9 adantr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ N <_ 0 ) -> ( A rmY N ) e. RR )
11 7 10 readdcld 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ N <_ 0 ) -> ( ( A rmY ( N - 1 ) ) + ( A rmY N ) ) e. RR )
12 0red 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ N <_ 0 ) -> 0 e. RR )
13 frmx 
 |-  rmX : ( ( ZZ>= ` 2 ) X. ZZ ) --> NN0
14 13 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX N ) e. NN0 )
15 14 adantr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ N <_ 0 ) -> ( A rmX N ) e. NN0 )
16 15 nn0red 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ N <_ 0 ) -> ( A rmX N ) e. RR )
17 znegcl 
 |-  ( N e. ZZ -> -u N e. ZZ )
18 17 ad2antlr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ N <_ 0 ) -> -u N e. ZZ )
19 18 peano2zd 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ N <_ 0 ) -> ( -u N + 1 ) e. ZZ )
20 4 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( -u N + 1 ) e. ZZ ) -> ( A rmY ( -u N + 1 ) ) e. ZZ )
21 1 19 20 syl2anc 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ N <_ 0 ) -> ( A rmY ( -u N + 1 ) ) e. ZZ )
22 21 zred 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ N <_ 0 ) -> ( A rmY ( -u N + 1 ) ) e. RR )
23 4 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ -u N e. ZZ ) -> ( A rmY -u N ) e. ZZ )
24 1 18 23 syl2anc 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ N <_ 0 ) -> ( A rmY -u N ) e. ZZ )
25 24 zred 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ N <_ 0 ) -> ( A rmY -u N ) e. RR )
26 rmy0 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A rmY 0 ) = 0 )
27 26 ad2antrr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ N <_ 0 ) -> ( A rmY 0 ) = 0 )
28 simpr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ N <_ 0 ) -> N <_ 0 )
29 zre 
 |-  ( N e. ZZ -> N e. RR )
30 29 ad2antlr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ N <_ 0 ) -> N e. RR )
31 30 le0neg1d 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ N <_ 0 ) -> ( N <_ 0 <-> 0 <_ -u N ) )
32 28 31 mpbid 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ N <_ 0 ) -> 0 <_ -u N )
33 0zd 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ N <_ 0 ) -> 0 e. ZZ )
34 zleltp1 
 |-  ( ( 0 e. ZZ /\ -u N e. ZZ ) -> ( 0 <_ -u N <-> 0 < ( -u N + 1 ) ) )
35 33 18 34 syl2anc 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ N <_ 0 ) -> ( 0 <_ -u N <-> 0 < ( -u N + 1 ) ) )
36 32 35 mpbid 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ N <_ 0 ) -> 0 < ( -u N + 1 ) )
37 ltrmy 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ 0 e. ZZ /\ ( -u N + 1 ) e. ZZ ) -> ( 0 < ( -u N + 1 ) <-> ( A rmY 0 ) < ( A rmY ( -u N + 1 ) ) ) )
38 1 33 19 37 syl3anc 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ N <_ 0 ) -> ( 0 < ( -u N + 1 ) <-> ( A rmY 0 ) < ( A rmY ( -u N + 1 ) ) ) )
39 36 38 mpbid 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ N <_ 0 ) -> ( A rmY 0 ) < ( A rmY ( -u N + 1 ) ) )
40 27 39 eqbrtrrd 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ N <_ 0 ) -> 0 < ( A rmY ( -u N + 1 ) ) )
41 lermy 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ 0 e. ZZ /\ -u N e. ZZ ) -> ( 0 <_ -u N <-> ( A rmY 0 ) <_ ( A rmY -u N ) ) )
42 1 33 18 41 syl3anc 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ N <_ 0 ) -> ( 0 <_ -u N <-> ( A rmY 0 ) <_ ( A rmY -u N ) ) )
43 32 42 mpbid 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ N <_ 0 ) -> ( A rmY 0 ) <_ ( A rmY -u N ) )
44 27 43 eqbrtrrd 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ N <_ 0 ) -> 0 <_ ( A rmY -u N ) )
45 22 25 40 44 addgtge0d 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ N <_ 0 ) -> 0 < ( ( A rmY ( -u N + 1 ) ) + ( A rmY -u N ) ) )
46 7 recnd 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ N <_ 0 ) -> ( A rmY ( N - 1 ) ) e. CC )
47 10 recnd 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ N <_ 0 ) -> ( A rmY N ) e. CC )
48 46 47 negdid 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ N <_ 0 ) -> -u ( ( A rmY ( N - 1 ) ) + ( A rmY N ) ) = ( -u ( A rmY ( N - 1 ) ) + -u ( A rmY N ) ) )
49 rmyneg 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( N - 1 ) e. ZZ ) -> ( A rmY -u ( N - 1 ) ) = -u ( A rmY ( N - 1 ) ) )
50 1 3 49 syl2anc 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ N <_ 0 ) -> ( A rmY -u ( N - 1 ) ) = -u ( A rmY ( N - 1 ) ) )
51 rmyneg 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmY -u N ) = -u ( A rmY N ) )
52 51 adantr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ N <_ 0 ) -> ( A rmY -u N ) = -u ( A rmY N ) )
53 50 52 oveq12d 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ N <_ 0 ) -> ( ( A rmY -u ( N - 1 ) ) + ( A rmY -u N ) ) = ( -u ( A rmY ( N - 1 ) ) + -u ( A rmY N ) ) )
54 zcn 
 |-  ( N e. ZZ -> N e. CC )
55 54 ad2antlr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ N <_ 0 ) -> N e. CC )
56 ax-1cn 
 |-  1 e. CC
57 negsubdi 
 |-  ( ( N e. CC /\ 1 e. CC ) -> -u ( N - 1 ) = ( -u N + 1 ) )
58 55 56 57 sylancl 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ N <_ 0 ) -> -u ( N - 1 ) = ( -u N + 1 ) )
59 58 oveq2d 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ N <_ 0 ) -> ( A rmY -u ( N - 1 ) ) = ( A rmY ( -u N + 1 ) ) )
60 59 oveq1d 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ N <_ 0 ) -> ( ( A rmY -u ( N - 1 ) ) + ( A rmY -u N ) ) = ( ( A rmY ( -u N + 1 ) ) + ( A rmY -u N ) ) )
61 48 53 60 3eqtr2d 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ N <_ 0 ) -> -u ( ( A rmY ( N - 1 ) ) + ( A rmY N ) ) = ( ( A rmY ( -u N + 1 ) ) + ( A rmY -u N ) ) )
62 45 61 breqtrrd 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ N <_ 0 ) -> 0 < -u ( ( A rmY ( N - 1 ) ) + ( A rmY N ) ) )
63 11 lt0neg1d 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ N <_ 0 ) -> ( ( ( A rmY ( N - 1 ) ) + ( A rmY N ) ) < 0 <-> 0 < -u ( ( A rmY ( N - 1 ) ) + ( A rmY N ) ) ) )
64 62 63 mpbird 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ N <_ 0 ) -> ( ( A rmY ( N - 1 ) ) + ( A rmY N ) ) < 0 )
65 15 nn0ge0d 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ N <_ 0 ) -> 0 <_ ( A rmX N ) )
66 11 12 16 64 65 ltletrd 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ N <_ 0 ) -> ( ( A rmY ( N - 1 ) ) + ( A rmY N ) ) < ( A rmX N ) )
67 simpll 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ 0 < N ) -> A e. ( ZZ>= ` 2 ) )
68 elnnz 
 |-  ( N e. NN <-> ( N e. ZZ /\ 0 < N ) )
69 68 biimpri 
 |-  ( ( N e. ZZ /\ 0 < N ) -> N e. NN )
70 69 adantll 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ 0 < N ) -> N e. NN )
71 jm2.24nn 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( ( A rmY ( N - 1 ) ) + ( A rmY N ) ) < ( A rmX N ) )
72 67 70 71 syl2anc 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ 0 < N ) -> ( ( A rmY ( N - 1 ) ) + ( A rmY N ) ) < ( A rmX N ) )
73 29 adantl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> N e. RR )
74 0re 
 |-  0 e. RR
75 lelttric 
 |-  ( ( N e. RR /\ 0 e. RR ) -> ( N <_ 0 \/ 0 < N ) )
76 73 74 75 sylancl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( N <_ 0 \/ 0 < N ) )
77 66 72 76 mpjaodan 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A rmY ( N - 1 ) ) + ( A rmY N ) ) < ( A rmX N ) )