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 φ x F x
monotoddzzfi.2 φ x F x = F x
monotoddzzfi.3 φ x 0 y 0 x < y F x < F y
Assertion monotoddzzfi φ A B A < B F A < F B

Proof

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