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 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℤ ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
monotoddzzfi.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℤ ) → ( 𝐹 ‘ - 𝑥 ) = - ( 𝐹 ‘ 𝑥 ) )
monotoddzzfi.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) → ( 𝑥 < 𝑦 → ( 𝐹 ‘ 𝑥 ) < ( 𝐹 ‘ 𝑦 ) ) )
Assertion monotoddzzfi ( ( 𝜑 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 < 𝐵 ↔ ( 𝐹 ‘ 𝐴 ) < ( 𝐹 ‘ 𝐵 ) ) )

Proof

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