Metamath Proof Explorer

Theorem monotoddzzfi

Description: A function which is odd and monotonic on NN0 is monotonic on ZZ . This proof is far too long. (Contributed by Stefan O'Rear, 25-Sep-2014)

Ref Expression
Hypotheses monotoddzzfi.1 
|- ( ( ph /\ x e. ZZ ) -> ( F ` x ) e. RR )
monotoddzzfi.2 
|- ( ( ph /\ x e. ZZ ) -> ( F ` -u x ) = -u ( F ` x ) )
monotoddzzfi.3 
|- ( ( ph /\ x e. NN0 /\ y e. NN0 ) -> ( x < y -> ( F ` x ) < ( F ` y ) ) )
Assertion monotoddzzfi 
|- ( ( ph /\ A e. ZZ /\ B e. ZZ ) -> ( A < B <-> ( F ` A ) < ( F ` B ) ) )

Proof

Step Hyp Ref Expression
1 monotoddzzfi.1 
 |-  ( ( ph /\ x e. ZZ ) -> ( F ` x ) e. RR )
2 monotoddzzfi.2 
 |-  ( ( ph /\ x e. ZZ ) -> ( F ` -u x ) = -u ( F ` x ) )
3 monotoddzzfi.3 
 |-  ( ( ph /\ x e. NN0 /\ y e. NN0 ) -> ( x < y -> ( F ` x ) < ( F ` y ) ) )
4 fveq2 
 |-  ( a = b -> ( F ` a ) = ( F ` b ) )
5 fveq2 
 |-  ( a = A -> ( F ` a ) = ( F ` A ) )
6 fveq2 
 |-  ( a = B -> ( F ` a ) = ( F ` B ) )
7 zssre 
 |-  ZZ C_ RR
8 eleq1 
 |-  ( x = a -> ( x e. ZZ <-> a e. ZZ ) )
9 8 anbi2d 
 |-  ( x = a -> ( ( ph /\ x e. ZZ ) <-> ( ph /\ a e. ZZ ) ) )
10 fveq2 
 |-  ( x = a -> ( F ` x ) = ( F ` a ) )
11 10 eleq1d 
 |-  ( x = a -> ( ( F ` x ) e. RR <-> ( F ` a ) e. RR ) )
12 9 11 imbi12d 
 |-  ( x = a -> ( ( ( ph /\ x e. ZZ ) -> ( F ` x ) e. RR ) <-> ( ( ph /\ a e. ZZ ) -> ( F ` a ) e. RR ) ) )
13 12 1 chvarvv 
 |-  ( ( ph /\ a e. ZZ ) -> ( F ` a ) e. RR )
14 elznn 
 |-  ( a e. ZZ <-> ( a e. RR /\ ( a e. NN \/ -u a e. NN0 ) ) )
15 14 simprbi 
 |-  ( a e. ZZ -> ( a e. NN \/ -u a e. NN0 ) )
16 elznn 
 |-  ( b e. ZZ <-> ( b e. RR /\ ( b e. NN \/ -u b e. NN0 ) ) )
17 16 simprbi 
 |-  ( b e. ZZ -> ( b e. NN \/ -u b e. NN0 ) )
18 15 17 anim12i 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> ( ( a e. NN \/ -u a e. NN0 ) /\ ( b e. NN \/ -u b e. NN0 ) ) )
19 18 adantl 
 |-  ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( a e. NN \/ -u a e. NN0 ) /\ ( b e. NN \/ -u b e. NN0 ) ) )
20 simpll 
 |-  ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( a e. NN /\ b e. NN ) ) -> ph )
21 nnnn0 
 |-  ( a e. NN -> a e. NN0 )
22 21 ad2antrl 
 |-  ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( a e. NN /\ b e. NN ) ) -> a e. NN0 )
23 nnnn0 
 |-  ( b e. NN -> b e. NN0 )
24 23 ad2antll 
 |-  ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( a e. NN /\ b e. NN ) ) -> b e. NN0 )
25 vex 
 |-  a e. _V
26 vex 
 |-  b e. _V
27 simpl 
 |-  ( ( x = a /\ y = b ) -> x = a )
28 27 eleq1d 
 |-  ( ( x = a /\ y = b ) -> ( x e. NN0 <-> a e. NN0 ) )
29 simpr 
 |-  ( ( x = a /\ y = b ) -> y = b )
30 29 eleq1d 
 |-  ( ( x = a /\ y = b ) -> ( y e. NN0 <-> b e. NN0 ) )
31 28 30 3anbi23d 
 |-  ( ( x = a /\ y = b ) -> ( ( ph /\ x e. NN0 /\ y e. NN0 ) <-> ( ph /\ a e. NN0 /\ b e. NN0 ) ) )
32 breq12 
 |-  ( ( x = a /\ y = b ) -> ( x < y <-> a < b ) )
33 fveq2 
 |-  ( y = b -> ( F ` y ) = ( F ` b ) )
34 10 33 breqan12d 
 |-  ( ( x = a /\ y = b ) -> ( ( F ` x ) < ( F ` y ) <-> ( F ` a ) < ( F ` b ) ) )
35 32 34 imbi12d 
 |-  ( ( x = a /\ y = b ) -> ( ( x < y -> ( F ` x ) < ( F ` y ) ) <-> ( a < b -> ( F ` a ) < ( F ` b ) ) ) )
36 31 35 imbi12d 
 |-  ( ( x = a /\ y = b ) -> ( ( ( ph /\ x e. NN0 /\ y e. NN0 ) -> ( x < y -> ( F ` x ) < ( F ` y ) ) ) <-> ( ( ph /\ a e. NN0 /\ b e. NN0 ) -> ( a < b -> ( F ` a ) < ( F ` b ) ) ) ) )
37 25 26 36 3 vtocl2 
 |-  ( ( ph /\ a e. NN0 /\ b e. NN0 ) -> ( a < b -> ( F ` a ) < ( F ` b ) ) )
38 20 22 24 37 syl3anc 
 |-  ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( a e. NN /\ b e. NN ) ) -> ( a < b -> ( F ` a ) < ( F ` b ) ) )
39 38 ex 
 |-  ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( a e. NN /\ b e. NN ) -> ( a < b -> ( F ` a ) < ( F ` b ) ) ) )
40 13 adantrr 
 |-  ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( F ` a ) e. RR )
41 40 adantr 
 |-  ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) -> ( F ` a ) e. RR )
42 0red 
 |-  ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) -> 0 e. RR )
43 eleq1 
 |-  ( x = b -> ( x e. ZZ <-> b e. ZZ ) )
44 43 anbi2d 
 |-  ( x = b -> ( ( ph /\ x e. ZZ ) <-> ( ph /\ b e. ZZ ) ) )
45 fveq2 
 |-  ( x = b -> ( F ` x ) = ( F ` b ) )
46 45 eleq1d 
 |-  ( x = b -> ( ( F ` x ) e. RR <-> ( F ` b ) e. RR ) )
47 44 46 imbi12d 
 |-  ( x = b -> ( ( ( ph /\ x e. ZZ ) -> ( F ` x ) e. RR ) <-> ( ( ph /\ b e. ZZ ) -> ( F ` b ) e. RR ) ) )
48 47 1 chvarvv 
 |-  ( ( ph /\ b e. ZZ ) -> ( F ` b ) e. RR )
49 48 adantrl 
 |-  ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( F ` b ) e. RR )
50 49 adantr 
 |-  ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) -> ( F ` b ) e. RR )
51 0red 
 |-  ( ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) /\ -u a e. NN ) -> 0 e. RR )
52 znegcl 
 |-  ( a e. ZZ -> -u a e. ZZ )
53 52 ad2antrl 
 |-  ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) -> -u a e. ZZ )
54 negex 
 |-  -u a e. _V
55 eleq1 
 |-  ( x = -u a -> ( x e. ZZ <-> -u a e. ZZ ) )
56 55 anbi2d 
 |-  ( x = -u a -> ( ( ph /\ x e. ZZ ) <-> ( ph /\ -u a e. ZZ ) ) )
57 fveq2 
 |-  ( x = -u a -> ( F ` x ) = ( F ` -u a ) )
58 57 eleq1d 
 |-  ( x = -u a -> ( ( F ` x ) e. RR <-> ( F ` -u a ) e. RR ) )
59 56 58 imbi12d 
 |-  ( x = -u a -> ( ( ( ph /\ x e. ZZ ) -> ( F ` x ) e. RR ) <-> ( ( ph /\ -u a e. ZZ ) -> ( F ` -u a ) e. RR ) ) )
60 54 59 1 vtocl 
 |-  ( ( ph /\ -u a e. ZZ ) -> ( F ` -u a ) e. RR )
61 53 60 syldan 
 |-  ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( F ` -u a ) e. RR )
62 61 ad2antrr 
 |-  ( ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) /\ -u a e. NN ) -> ( F ` -u a ) e. RR )
63 0z 
 |-  0 e. ZZ
64 c0ex 
 |-  0 e. _V
65 eleq1 
 |-  ( x = 0 -> ( x e. ZZ <-> 0 e. ZZ ) )
66 65 anbi2d 
 |-  ( x = 0 -> ( ( ph /\ x e. ZZ ) <-> ( ph /\ 0 e. ZZ ) ) )
67 fveq2 
 |-  ( x = 0 -> ( F ` x ) = ( F ` 0 ) )
68 67 eleq1d 
 |-  ( x = 0 -> ( ( F ` x ) e. RR <-> ( F ` 0 ) e. RR ) )
69 66 68 imbi12d 
 |-  ( x = 0 -> ( ( ( ph /\ x e. ZZ ) -> ( F ` x ) e. RR ) <-> ( ( ph /\ 0 e. ZZ ) -> ( F ` 0 ) e. RR ) ) )
70 64 69 1 vtocl 
 |-  ( ( ph /\ 0 e. ZZ ) -> ( F ` 0 ) e. RR )
71 63 70 mpan2 
 |-  ( ph -> ( F ` 0 ) e. RR )
72 71 recnd 
 |-  ( ph -> ( F ` 0 ) e. CC )
73 neg0 
 |-  -u 0 = 0
74 73 fveq2i 
 |-  ( F ` -u 0 ) = ( F ` 0 )
75 negeq 
 |-  ( x = 0 -> -u x = -u 0 )
76 75 fveq2d 
 |-  ( x = 0 -> ( F ` -u x ) = ( F ` -u 0 ) )
77 67 negeqd 
 |-  ( x = 0 -> -u ( F ` x ) = -u ( F ` 0 ) )
78 76 77 eqeq12d 
 |-  ( x = 0 -> ( ( F ` -u x ) = -u ( F ` x ) <-> ( F ` -u 0 ) = -u ( F ` 0 ) ) )
79 66 78 imbi12d 
 |-  ( x = 0 -> ( ( ( ph /\ x e. ZZ ) -> ( F ` -u x ) = -u ( F ` x ) ) <-> ( ( ph /\ 0 e. ZZ ) -> ( F ` -u 0 ) = -u ( F ` 0 ) ) ) )
80 64 79 2 vtocl 
 |-  ( ( ph /\ 0 e. ZZ ) -> ( F ` -u 0 ) = -u ( F ` 0 ) )
81 63 80 mpan2 
 |-  ( ph -> ( F ` -u 0 ) = -u ( F ` 0 ) )
82 74 81 eqtr3id 
 |-  ( ph -> ( F ` 0 ) = -u ( F ` 0 ) )
83 72 82 eqnegad 
 |-  ( ph -> ( F ` 0 ) = 0 )
84 83 adantr 
 |-  ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( F ` 0 ) = 0 )
85 84 ad2antrr 
 |-  ( ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) /\ -u a e. NN ) -> ( F ` 0 ) = 0 )
86 nngt0 
 |-  ( -u a e. NN -> 0 < -u a )
87 86 adantl 
 |-  ( ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) /\ -u a e. NN ) -> 0 < -u a )
88 simplll 
 |-  ( ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) /\ -u a e. NN ) -> ph )
89 0nn0 
 |-  0 e. NN0
90 89 a1i 
 |-  ( ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) /\ -u a e. NN ) -> 0 e. NN0 )
91 simplrl 
 |-  ( ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) /\ -u a e. NN ) -> -u a e. NN0 )
92 simpl 
 |-  ( ( x = 0 /\ y = -u a ) -> x = 0 )
93 92 eleq1d 
 |-  ( ( x = 0 /\ y = -u a ) -> ( x e. NN0 <-> 0 e. NN0 ) )
94 simpr 
 |-  ( ( x = 0 /\ y = -u a ) -> y = -u a )
95 94 eleq1d 
 |-  ( ( x = 0 /\ y = -u a ) -> ( y e. NN0 <-> -u a e. NN0 ) )
96 93 95 3anbi23d 
 |-  ( ( x = 0 /\ y = -u a ) -> ( ( ph /\ x e. NN0 /\ y e. NN0 ) <-> ( ph /\ 0 e. NN0 /\ -u a e. NN0 ) ) )
97 breq12 
 |-  ( ( x = 0 /\ y = -u a ) -> ( x < y <-> 0 < -u a ) )
98 92 fveq2d 
 |-  ( ( x = 0 /\ y = -u a ) -> ( F ` x ) = ( F ` 0 ) )
99 94 fveq2d 
 |-  ( ( x = 0 /\ y = -u a ) -> ( F ` y ) = ( F ` -u a ) )
100 98 99 breq12d 
 |-  ( ( x = 0 /\ y = -u a ) -> ( ( F ` x ) < ( F ` y ) <-> ( F ` 0 ) < ( F ` -u a ) ) )
101 97 100 imbi12d 
 |-  ( ( x = 0 /\ y = -u a ) -> ( ( x < y -> ( F ` x ) < ( F ` y ) ) <-> ( 0 < -u a -> ( F ` 0 ) < ( F ` -u a ) ) ) )
102 96 101 imbi12d 
 |-  ( ( x = 0 /\ y = -u a ) -> ( ( ( ph /\ x e. NN0 /\ y e. NN0 ) -> ( x < y -> ( F ` x ) < ( F ` y ) ) ) <-> ( ( ph /\ 0 e. NN0 /\ -u a e. NN0 ) -> ( 0 < -u a -> ( F ` 0 ) < ( F ` -u a ) ) ) ) )
103 64 54 102 3 vtocl2 
 |-  ( ( ph /\ 0 e. NN0 /\ -u a e. NN0 ) -> ( 0 < -u a -> ( F ` 0 ) < ( F ` -u a ) ) )
104 88 90 91 103 syl3anc 
 |-  ( ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) /\ -u a e. NN ) -> ( 0 < -u a -> ( F ` 0 ) < ( F ` -u a ) ) )
105 87 104 mpd 
 |-  ( ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) /\ -u a e. NN ) -> ( F ` 0 ) < ( F ` -u a ) )
106 85 105 eqbrtrrd 
 |-  ( ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) /\ -u a e. NN ) -> 0 < ( F ` -u a ) )
107 51 62 106 ltled 
 |-  ( ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) /\ -u a e. NN ) -> 0 <_ ( F ` -u a ) )
108 0le0 
 |-  0 <_ 0
109 84 ad2antrr 
 |-  ( ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) /\ -u a = 0 ) -> ( F ` 0 ) = 0 )
110 108 109 breqtrrid 
 |-  ( ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) /\ -u a = 0 ) -> 0 <_ ( F ` 0 ) )
111 fveq2 
 |-  ( -u a = 0 -> ( F ` -u a ) = ( F ` 0 ) )
112 111 breq2d 
 |-  ( -u a = 0 -> ( 0 <_ ( F ` -u a ) <-> 0 <_ ( F ` 0 ) ) )
113 112 adantl 
 |-  ( ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) /\ -u a = 0 ) -> ( 0 <_ ( F ` -u a ) <-> 0 <_ ( F ` 0 ) ) )
114 110 113 mpbird 
 |-  ( ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) /\ -u a = 0 ) -> 0 <_ ( F ` -u a ) )
115 elnn0 
 |-  ( -u a e. NN0 <-> ( -u a e. NN \/ -u a = 0 ) )
116 115 biimpi 
 |-  ( -u a e. NN0 -> ( -u a e. NN \/ -u a = 0 ) )
117 116 ad2antrl 
 |-  ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) -> ( -u a e. NN \/ -u a = 0 ) )
118 107 114 117 mpjaodan 
 |-  ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) -> 0 <_ ( F ` -u a ) )
119 negeq 
 |-  ( x = a -> -u x = -u a )
120 119 fveq2d 
 |-  ( x = a -> ( F ` -u x ) = ( F ` -u a ) )
121 10 negeqd 
 |-  ( x = a -> -u ( F ` x ) = -u ( F ` a ) )
122 120 121 eqeq12d 
 |-  ( x = a -> ( ( F ` -u x ) = -u ( F ` x ) <-> ( F ` -u a ) = -u ( F ` a ) ) )
123 9 122 imbi12d 
 |-  ( x = a -> ( ( ( ph /\ x e. ZZ ) -> ( F ` -u x ) = -u ( F ` x ) ) <-> ( ( ph /\ a e. ZZ ) -> ( F ` -u a ) = -u ( F ` a ) ) ) )
124 123 2 chvarvv 
 |-  ( ( ph /\ a e. ZZ ) -> ( F ` -u a ) = -u ( F ` a ) )
125 124 adantrr 
 |-  ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( F ` -u a ) = -u ( F ` a ) )
126 125 adantr 
 |-  ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) -> ( F ` -u a ) = -u ( F ` a ) )
127 118 126 breqtrd 
 |-  ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) -> 0 <_ -u ( F ` a ) )
128 41 le0neg1d 
 |-  ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) -> ( ( F ` a ) <_ 0 <-> 0 <_ -u ( F ` a ) ) )
129 127 128 mpbird 
 |-  ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) -> ( F ` a ) <_ 0 )
130 84 adantr 
 |-  ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) -> ( F ` 0 ) = 0 )
131 nngt0 
 |-  ( b e. NN -> 0 < b )
132 131 ad2antll 
 |-  ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) -> 0 < b )
133 simpll 
 |-  ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) -> ph )
134 89 a1i 
 |-  ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) -> 0 e. NN0 )
135 23 ad2antll 
 |-  ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) -> b e. NN0 )
136 simpl 
 |-  ( ( x = 0 /\ y = b ) -> x = 0 )
137 136 eleq1d 
 |-  ( ( x = 0 /\ y = b ) -> ( x e. NN0 <-> 0 e. NN0 ) )
138 simpr 
 |-  ( ( x = 0 /\ y = b ) -> y = b )
139 138 eleq1d 
 |-  ( ( x = 0 /\ y = b ) -> ( y e. NN0 <-> b e. NN0 ) )
140 137 139 3anbi23d 
 |-  ( ( x = 0 /\ y = b ) -> ( ( ph /\ x e. NN0 /\ y e. NN0 ) <-> ( ph /\ 0 e. NN0 /\ b e. NN0 ) ) )
141 breq12 
 |-  ( ( x = 0 /\ y = b ) -> ( x < y <-> 0 < b ) )
142 67 33 breqan12d 
 |-  ( ( x = 0 /\ y = b ) -> ( ( F ` x ) < ( F ` y ) <-> ( F ` 0 ) < ( F ` b ) ) )
143 141 142 imbi12d 
 |-  ( ( x = 0 /\ y = b ) -> ( ( x < y -> ( F ` x ) < ( F ` y ) ) <-> ( 0 < b -> ( F ` 0 ) < ( F ` b ) ) ) )
144 140 143 imbi12d 
 |-  ( ( x = 0 /\ y = b ) -> ( ( ( ph /\ x e. NN0 /\ y e. NN0 ) -> ( x < y -> ( F ` x ) < ( F ` y ) ) ) <-> ( ( ph /\ 0 e. NN0 /\ b e. NN0 ) -> ( 0 < b -> ( F ` 0 ) < ( F ` b ) ) ) ) )
145 64 26 144 3 vtocl2 
 |-  ( ( ph /\ 0 e. NN0 /\ b e. NN0 ) -> ( 0 < b -> ( F ` 0 ) < ( F ` b ) ) )
146 133 134 135 145 syl3anc 
 |-  ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) -> ( 0 < b -> ( F ` 0 ) < ( F ` b ) ) )
147 132 146 mpd 
 |-  ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) -> ( F ` 0 ) < ( F ` b ) )
148 130 147 eqbrtrrd 
 |-  ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) -> 0 < ( F ` b ) )
149 41 42 50 129 148 lelttrd 
 |-  ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) -> ( F ` a ) < ( F ` b ) )
150 149 a1d 
 |-  ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) -> ( a < b -> ( F ` a ) < ( F ` b ) ) )
151 150 ex 
 |-  ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( -u a e. NN0 /\ b e. NN ) -> ( a < b -> ( F ` a ) < ( F ` b ) ) ) )
152 simp3 
 |-  ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( a e. NN /\ -u b e. NN0 ) /\ a < b ) -> a < b )
153 zre 
 |-  ( b e. ZZ -> b e. RR )
154 153 adantl 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> b e. RR )
155 154 ad2antlr 
 |-  ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( a e. NN /\ -u b e. NN0 ) ) -> b e. RR )
156 1red 
 |-  ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( a e. NN /\ -u b e. NN0 ) ) -> 1 e. RR )
157 nnre 
 |-  ( a e. NN -> a e. RR )
158 157 ad2antrl 
 |-  ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( a e. NN /\ -u b e. NN0 ) ) -> a e. RR )
159 0red 
 |-  ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( a e. NN /\ -u b e. NN0 ) ) -> 0 e. RR )
160 nn0ge0 
 |-  ( -u b e. NN0 -> 0 <_ -u b )
161 160 ad2antll 
 |-  ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( a e. NN /\ -u b e. NN0 ) ) -> 0 <_ -u b )
162 155 le0neg1d 
 |-  ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( a e. NN /\ -u b e. NN0 ) ) -> ( b <_ 0 <-> 0 <_ -u b ) )
163 161 162 mpbird 
 |-  ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( a e. NN /\ -u b e. NN0 ) ) -> b <_ 0 )
164 0le1 
 |-  0 <_ 1
165 164 a1i 
 |-  ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( a e. NN /\ -u b e. NN0 ) ) -> 0 <_ 1 )
166 155 159 156 163 165 letrd 
 |-  ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( a e. NN /\ -u b e. NN0 ) ) -> b <_ 1 )
167 nnge1 
 |-  ( a e. NN -> 1 <_ a )
168 167 ad2antrl 
 |-  ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( a e. NN /\ -u b e. NN0 ) ) -> 1 <_ a )
169 155 156 158 166 168 letrd 
 |-  ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( a e. NN /\ -u b e. NN0 ) ) -> b <_ a )
170 155 158 lenltd 
 |-  ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( a e. NN /\ -u b e. NN0 ) ) -> ( b <_ a <-> -. a < b ) )
171 169 170 mpbid 
 |-  ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( a e. NN /\ -u b e. NN0 ) ) -> -. a < b )
172 171 3adant3 
 |-  ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( a e. NN /\ -u b e. NN0 ) /\ a < b ) -> -. a < b )
173 152 172 pm2.21dd 
 |-  ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( a e. NN /\ -u b e. NN0 ) /\ a < b ) -> ( F ` a ) < ( F ` b ) )
174 173 3exp 
 |-  ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( a e. NN /\ -u b e. NN0 ) -> ( a < b -> ( F ` a ) < ( F ` b ) ) ) )
175 negex 
 |-  -u b e. _V
176 simpl 
 |-  ( ( x = -u b /\ y = -u a ) -> x = -u b )
177 176 eleq1d 
 |-  ( ( x = -u b /\ y = -u a ) -> ( x e. NN0 <-> -u b e. NN0 ) )
178 simpr 
 |-  ( ( x = -u b /\ y = -u a ) -> y = -u a )
179 178 eleq1d 
 |-  ( ( x = -u b /\ y = -u a ) -> ( y e. NN0 <-> -u a e. NN0 ) )
180 177 179 3anbi23d 
 |-  ( ( x = -u b /\ y = -u a ) -> ( ( ph /\ x e. NN0 /\ y e. NN0 ) <-> ( ph /\ -u b e. NN0 /\ -u a e. NN0 ) ) )
181 breq12 
 |-  ( ( x = -u b /\ y = -u a ) -> ( x < y <-> -u b < -u a ) )
182 fveq2 
 |-  ( x = -u b -> ( F ` x ) = ( F ` -u b ) )
183 fveq2 
 |-  ( y = -u a -> ( F ` y ) = ( F ` -u a ) )
184 182 183 breqan12d 
 |-  ( ( x = -u b /\ y = -u a ) -> ( ( F ` x ) < ( F ` y ) <-> ( F ` -u b ) < ( F ` -u a ) ) )
185 181 184 imbi12d 
 |-  ( ( x = -u b /\ y = -u a ) -> ( ( x < y -> ( F ` x ) < ( F ` y ) ) <-> ( -u b < -u a -> ( F ` -u b ) < ( F ` -u a ) ) ) )
186 180 185 imbi12d 
 |-  ( ( x = -u b /\ y = -u a ) -> ( ( ( ph /\ x e. NN0 /\ y e. NN0 ) -> ( x < y -> ( F ` x ) < ( F ` y ) ) ) <-> ( ( ph /\ -u b e. NN0 /\ -u a e. NN0 ) -> ( -u b < -u a -> ( F ` -u b ) < ( F ` -u a ) ) ) ) )
187 175 54 186 3 vtocl2 
 |-  ( ( ph /\ -u b e. NN0 /\ -u a e. NN0 ) -> ( -u b < -u a -> ( F ` -u b ) < ( F ` -u a ) ) )
188 187 3com23 
 |-  ( ( ph /\ -u a e. NN0 /\ -u b e. NN0 ) -> ( -u b < -u a -> ( F ` -u b ) < ( F ` -u a ) ) )
189 188 3expb 
 |-  ( ( ph /\ ( -u a e. NN0 /\ -u b e. NN0 ) ) -> ( -u b < -u a -> ( F ` -u b ) < ( F ` -u a ) ) )
190 189 adantlr 
 |-  ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ -u b e. NN0 ) ) -> ( -u b < -u a -> ( F ` -u b ) < ( F ` -u a ) ) )
191 negeq 
 |-  ( x = b -> -u x = -u b )
192 191 fveq2d 
 |-  ( x = b -> ( F ` -u x ) = ( F ` -u b ) )
193 45 negeqd 
 |-  ( x = b -> -u ( F ` x ) = -u ( F ` b ) )
194 192 193 eqeq12d 
 |-  ( x = b -> ( ( F ` -u x ) = -u ( F ` x ) <-> ( F ` -u b ) = -u ( F ` b ) ) )
195 44 194 imbi12d 
 |-  ( x = b -> ( ( ( ph /\ x e. ZZ ) -> ( F ` -u x ) = -u ( F ` x ) ) <-> ( ( ph /\ b e. ZZ ) -> ( F ` -u b ) = -u ( F ` b ) ) ) )
196 195 2 chvarvv 
 |-  ( ( ph /\ b e. ZZ ) -> ( F ` -u b ) = -u ( F ` b ) )
197 196 adantrl 
 |-  ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( F ` -u b ) = -u ( F ` b ) )
198 197 adantr 
 |-  ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ -u b e. NN0 ) ) -> ( F ` -u b ) = -u ( F ` b ) )
199 125 adantr 
 |-  ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ -u b e. NN0 ) ) -> ( F ` -u a ) = -u ( F ` a ) )
200 198 199 breq12d 
 |-  ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ -u b e. NN0 ) ) -> ( ( F ` -u b ) < ( F ` -u a ) <-> -u ( F ` b ) < -u ( F ` a ) ) )
201 190 200 sylibd 
 |-  ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ -u b e. NN0 ) ) -> ( -u b < -u a -> -u ( F ` b ) < -u ( F ` a ) ) )
202 zre 
 |-  ( a e. ZZ -> a e. RR )
203 202 ad2antrl 
 |-  ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) -> a e. RR )
204 203 adantr 
 |-  ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ -u b e. NN0 ) ) -> a e. RR )
205 154 ad2antlr 
 |-  ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ -u b e. NN0 ) ) -> b e. RR )
206 204 205 ltnegd 
 |-  ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ -u b e. NN0 ) ) -> ( a < b <-> -u b < -u a ) )
207 40 adantr 
 |-  ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ -u b e. NN0 ) ) -> ( F ` a ) e. RR )
208 49 adantr 
 |-  ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ -u b e. NN0 ) ) -> ( F ` b ) e. RR )
209 207 208 ltnegd 
 |-  ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ -u b e. NN0 ) ) -> ( ( F ` a ) < ( F ` b ) <-> -u ( F ` b ) < -u ( F ` a ) ) )
210 201 206 209 3imtr4d 
 |-  ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ -u b e. NN0 ) ) -> ( a < b -> ( F ` a ) < ( F ` b ) ) )
211 210 ex 
 |-  ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( -u a e. NN0 /\ -u b e. NN0 ) -> ( a < b -> ( F ` a ) < ( F ` b ) ) ) )
212 39 151 174 211 ccased 
 |-  ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( ( a e. NN \/ -u a e. NN0 ) /\ ( b e. NN \/ -u b e. NN0 ) ) -> ( a < b -> ( F ` a ) < ( F ` b ) ) ) )
213 19 212 mpd 
 |-  ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( a < b -> ( F ` a ) < ( F ` b ) ) )
214 4 5 6 7 13 213 ltord1 
 |-  ( ( ph /\ ( A e. ZZ /\ B e. ZZ ) ) -> ( A < B <-> ( F ` A ) < ( F ` B ) ) )
215 214 3impb 
 |-  ( ( ph /\ A e. ZZ /\ B e. ZZ ) -> ( A < B <-> ( F ` A ) < ( F ` B ) ) )