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 ${⊢}\left({\phi }\wedge {x}\in ℤ\right)\to {F}\left({x}\right)\in ℝ$
monotoddzzfi.2 ${⊢}\left({\phi }\wedge {x}\in ℤ\right)\to {F}\left(-{x}\right)=-{F}\left({x}\right)$
monotoddzzfi.3 ${⊢}\left({\phi }\wedge {x}\in {ℕ}_{0}\wedge {y}\in {ℕ}_{0}\right)\to \left({x}<{y}\to {F}\left({x}\right)<{F}\left({y}\right)\right)$
Assertion monotoddzzfi ${⊢}\left({\phi }\wedge {A}\in ℤ\wedge {B}\in ℤ\right)\to \left({A}<{B}↔{F}\left({A}\right)<{F}\left({B}\right)\right)$

Proof

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