Metamath Proof Explorer

Theorem monotoddzz

Description: A function (given implicitly) 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 monotoddzz.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) → ( 𝑥 < 𝑦 → 𝐸 < 𝐹 ) )
monotoddzz.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℤ ) → 𝐸 ∈ ℝ )
monotoddzz.3 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℤ ) → 𝐺 = - 𝐹 )
monotoddzz.4 ⊢ ( 𝑥 = 𝐴 → 𝐸 = 𝐶 )
monotoddzz.5 ⊢ ( 𝑥 = 𝐵 → 𝐸 = 𝐷 )
monotoddzz.6 ⊢ ( 𝑥 = 𝑦 → 𝐸 = 𝐹 )
monotoddzz.7 ⊢ ( 𝑥 = - 𝑦 → 𝐸 = 𝐺 )
Assertion monotoddzz ( ( 𝜑 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 < 𝐵 ↔ 𝐶 < 𝐷 ) )

Proof

Step Hyp Ref Expression
1 monotoddzz.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) → ( 𝑥 < 𝑦 → 𝐸 < 𝐹 ) )
2 monotoddzz.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℤ ) → 𝐸 ∈ ℝ )
3 monotoddzz.3 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℤ ) → 𝐺 = - 𝐹 )
4 monotoddzz.4 ⊢ ( 𝑥 = 𝐴 → 𝐸 = 𝐶 )
5 monotoddzz.5 ⊢ ( 𝑥 = 𝐵 → 𝐸 = 𝐷 )
6 monotoddzz.6 ⊢ ( 𝑥 = 𝑦 → 𝐸 = 𝐹 )
7 monotoddzz.7 ⊢ ( 𝑥 = - 𝑦 → 𝐸 = 𝐺 )
8 nfv ⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑎 ∈ ℤ )
9 nffvmpt1 ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑎 )
10 9 nfel1 ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑎 ) ∈ ℝ
11 8 10 nfim ⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ 𝑎 ∈ ℤ ) → ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑎 ) ∈ ℝ )
12 eleq1 ⊢ ( 𝑥 = 𝑎 → ( 𝑥 ∈ ℤ ↔ 𝑎 ∈ ℤ ) )
13 12 anbi2d ⊢ ( 𝑥 = 𝑎 → ( ( 𝜑 ∧ 𝑥 ∈ ℤ ) ↔ ( 𝜑 ∧ 𝑎 ∈ ℤ ) ) )
14 fveq2 ⊢ ( 𝑥 = 𝑎 → ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑎 ) )
15 14 eleq1d ⊢ ( 𝑥 = 𝑎 → ( ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑥 ) ∈ ℝ ↔ ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑎 ) ∈ ℝ ) )
16 13 15 imbi12d ⊢ ( 𝑥 = 𝑎 → ( ( ( 𝜑 ∧ 𝑥 ∈ ℤ ) → ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑥 ) ∈ ℝ ) ↔ ( ( 𝜑 ∧ 𝑎 ∈ ℤ ) → ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑎 ) ∈ ℝ ) ) )
17 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℤ ) → 𝑥 ∈ ℤ )
18 eqid ⊢ ( 𝑥 ∈ ℤ ↦ 𝐸 ) = ( 𝑥 ∈ ℤ ↦ 𝐸 )
19 18 fvmpt2 ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝐸 ∈ ℝ ) → ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑥 ) = 𝐸 )
20 17 2 19 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℤ ) → ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑥 ) = 𝐸 )
21 20 2 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℤ ) → ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑥 ) ∈ ℝ )
22 11 16 21 chvarfv ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℤ ) → ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑎 ) ∈ ℝ )
23 eleq1 ⊢ ( 𝑦 = 𝑎 → ( 𝑦 ∈ ℤ ↔ 𝑎 ∈ ℤ ) )
24 23 anbi2d ⊢ ( 𝑦 = 𝑎 → ( ( 𝜑 ∧ 𝑦 ∈ ℤ ) ↔ ( 𝜑 ∧ 𝑎 ∈ ℤ ) ) )
25 negeq ⊢ ( 𝑦 = 𝑎 → - 𝑦 = - 𝑎 )
26 25 fveq2d ⊢ ( 𝑦 = 𝑎 → ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ - 𝑦 ) = ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ - 𝑎 ) )
27 fveq2 ⊢ ( 𝑦 = 𝑎 → ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑦 ) = ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑎 ) )
28 27 negeqd ⊢ ( 𝑦 = 𝑎 → - ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑦 ) = - ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑎 ) )
29 26 28 eqeq12d ⊢ ( 𝑦 = 𝑎 → ( ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ - 𝑦 ) = - ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑦 ) ↔ ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ - 𝑎 ) = - ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑎 ) ) )
30 24 29 imbi12d ⊢ ( 𝑦 = 𝑎 → ( ( ( 𝜑 ∧ 𝑦 ∈ ℤ ) → ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ - 𝑦 ) = - ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑦 ) ) ↔ ( ( 𝜑 ∧ 𝑎 ∈ ℤ ) → ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ - 𝑎 ) = - ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑎 ) ) ) )
31 znegcl ⊢ ( 𝑦 ∈ ℤ → - 𝑦 ∈ ℤ )
32 31 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℤ ) → - 𝑦 ∈ ℤ )
33 negex ⊢ - 𝑦 ∈ V
34 eleq1 ⊢ ( 𝑥 = - 𝑦 → ( 𝑥 ∈ ℤ ↔ - 𝑦 ∈ ℤ ) )
35 34 anbi2d ⊢ ( 𝑥 = - 𝑦 → ( ( 𝜑 ∧ 𝑥 ∈ ℤ ) ↔ ( 𝜑 ∧ - 𝑦 ∈ ℤ ) ) )
36 7 eleq1d ⊢ ( 𝑥 = - 𝑦 → ( 𝐸 ∈ ℝ ↔ 𝐺 ∈ ℝ ) )
37 35 36 imbi12d ⊢ ( 𝑥 = - 𝑦 → ( ( ( 𝜑 ∧ 𝑥 ∈ ℤ ) → 𝐸 ∈ ℝ ) ↔ ( ( 𝜑 ∧ - 𝑦 ∈ ℤ ) → 𝐺 ∈ ℝ ) ) )
38 33 37 2 vtocl ⊢ ( ( 𝜑 ∧ - 𝑦 ∈ ℤ ) → 𝐺 ∈ ℝ )
39 31 38 sylan2 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℤ ) → 𝐺 ∈ ℝ )
40 18 7 32 39 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℤ ) → ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ - 𝑦 ) = 𝐺 )
41 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℤ ) → 𝑦 ∈ ℤ )
42 eleq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ ℤ ↔ 𝑦 ∈ ℤ ) )
43 42 anbi2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝜑 ∧ 𝑥 ∈ ℤ ) ↔ ( 𝜑 ∧ 𝑦 ∈ ℤ ) ) )
44 6 eleq1d ⊢ ( 𝑥 = 𝑦 → ( 𝐸 ∈ ℝ ↔ 𝐹 ∈ ℝ ) )
45 43 44 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝜑 ∧ 𝑥 ∈ ℤ ) → 𝐸 ∈ ℝ ) ↔ ( ( 𝜑 ∧ 𝑦 ∈ ℤ ) → 𝐹 ∈ ℝ ) ) )
46 45 2 chvarvv ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℤ ) → 𝐹 ∈ ℝ )
47 18 6 41 46 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℤ ) → ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑦 ) = 𝐹 )
48 47 negeqd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℤ ) → - ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑦 ) = - 𝐹 )
49 3 40 48 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℤ ) → ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ - 𝑦 ) = - ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑦 ) )
50 30 49 chvarvv ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℤ ) → ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ - 𝑎 ) = - ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑎 ) )
51 nfv ⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 )
52 nfv ⊢ Ⅎ 𝑥 𝑎 < 𝑏
53 nfcv ⊢ Ⅎ 𝑥 <
54 nffvmpt1 ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑏 )
55 9 53 54 nfbr ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑎 ) < ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑏 )
56 52 55 nfim ⊢ Ⅎ 𝑥 ( 𝑎 < 𝑏 → ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑎 ) < ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑏 ) )
57 51 56 nfim ⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) → ( 𝑎 < 𝑏 → ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑎 ) < ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑏 ) ) )
58 eleq1 ⊢ ( 𝑥 = 𝑎 → ( 𝑥 ∈ ℕ0 ↔ 𝑎 ∈ ℕ0 ) )
59 58 3anbi2d ⊢ ( 𝑥 = 𝑎 → ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ↔ ( 𝜑 ∧ 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ) )
60 breq1 ⊢ ( 𝑥 = 𝑎 → ( 𝑥 < 𝑏 ↔ 𝑎 < 𝑏 ) )
61 14 breq1d ⊢ ( 𝑥 = 𝑎 → ( ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑥 ) < ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑏 ) ↔ ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑎 ) < ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑏 ) ) )
62 60 61 imbi12d ⊢ ( 𝑥 = 𝑎 → ( ( 𝑥 < 𝑏 → ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑥 ) < ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑏 ) ) ↔ ( 𝑎 < 𝑏 → ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑎 ) < ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑏 ) ) ) )
63 59 62 imbi12d ⊢ ( 𝑥 = 𝑎 → ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) → ( 𝑥 < 𝑏 → ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑥 ) < ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑏 ) ) ) ↔ ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) → ( 𝑎 < 𝑏 → ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑎 ) < ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑏 ) ) ) ) )
64 eleq1 ⊢ ( 𝑦 = 𝑏 → ( 𝑦 ∈ ℕ0 ↔ 𝑏 ∈ ℕ0 ) )
65 64 3anbi3d ⊢ ( 𝑦 = 𝑏 → ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) ↔ ( 𝜑 ∧ 𝑥 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) ) )
66 breq2 ⊢ ( 𝑦 = 𝑏 → ( 𝑥 < 𝑦 ↔ 𝑥 < 𝑏 ) )
67 fveq2 ⊢ ( 𝑦 = 𝑏 → ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑦 ) = ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑏 ) )
68 67 breq2d ⊢ ( 𝑦 = 𝑏 → ( ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑥 ) < ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑦 ) ↔ ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑥 ) < ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑏 ) ) )
69 66 68 imbi12d ⊢ ( 𝑦 = 𝑏 → ( ( 𝑥 < 𝑦 → ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑥 ) < ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑦 ) ) ↔ ( 𝑥 < 𝑏 → ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑥 ) < ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑏 ) ) ) )
70 65 69 imbi12d ⊢ ( 𝑦 = 𝑏 → ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) → ( 𝑥 < 𝑦 → ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑥 ) < ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑦 ) ) ) ↔ ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) → ( 𝑥 < 𝑏 → ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑥 ) < ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑏 ) ) ) ) )
71 nn0z ⊢ ( 𝑥 ∈ ℕ0 → 𝑥 ∈ ℤ )
72 71 20 sylan2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑥 ) = 𝐸 )
73 72 3adant3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) → ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑥 ) = 𝐸 )
74 nfv ⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑦 ∈ ℕ0 )
75 nffvmpt1 ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑦 )
76 75 nfeq1 ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑦 ) = 𝐹
77 74 76 nfim ⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) → ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑦 ) = 𝐹 )
78 eleq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ ℕ0 ↔ 𝑦 ∈ ℕ0 ) )
79 78 anbi2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ↔ ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ) )
80 fveq2 ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑦 ) )
81 80 6 eqeq12d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑥 ) = 𝐸 ↔ ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑦 ) = 𝐹 ) )
82 79 81 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑥 ) = 𝐸 ) ↔ ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) → ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑦 ) = 𝐹 ) ) )
83 77 82 72 chvarfv ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) → ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑦 ) = 𝐹 )
84 83 3adant2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) → ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑦 ) = 𝐹 )
85 73 84 breq12d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) → ( ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑥 ) < ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑦 ) ↔ 𝐸 < 𝐹 ) )
86 1 85 sylibrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) → ( 𝑥 < 𝑦 → ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑥 ) < ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑦 ) ) )
87 70 86 chvarvv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) → ( 𝑥 < 𝑏 → ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑥 ) < ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑏 ) ) )
88 57 63 87 chvarfv ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ) → ( 𝑎 < 𝑏 → ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑎 ) < ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝑏 ) ) )
89 22 50 88 monotoddzzfi ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 < 𝐵 ↔ ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝐴 ) < ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝐵 ) ) )
90 simp2 ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 𝐴 ∈ ℤ )
91 eleq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ ℤ ↔ 𝐴 ∈ ℤ ) )
92 91 anbi2d ⊢ ( 𝑥 = 𝐴 → ( ( 𝜑 ∧ 𝑥 ∈ ℤ ) ↔ ( 𝜑 ∧ 𝐴 ∈ ℤ ) ) )
93 4 eleq1d ⊢ ( 𝑥 = 𝐴 → ( 𝐸 ∈ ℝ ↔ 𝐶 ∈ ℝ ) )
94 92 93 imbi12d ⊢ ( 𝑥 = 𝐴 → ( ( ( 𝜑 ∧ 𝑥 ∈ ℤ ) → 𝐸 ∈ ℝ ) ↔ ( ( 𝜑 ∧ 𝐴 ∈ ℤ ) → 𝐶 ∈ ℝ ) ) )
95 94 2 vtoclg ⊢ ( 𝐴 ∈ ℤ → ( ( 𝜑 ∧ 𝐴 ∈ ℤ ) → 𝐶 ∈ ℝ ) )
96 95 anabsi7 ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℤ ) → 𝐶 ∈ ℝ )
97 96 3adant3 ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 𝐶 ∈ ℝ )
98 18 4 90 97 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝐴 ) = 𝐶 )
99 simp3 ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 𝐵 ∈ ℤ )
100 eleq1 ⊢ ( 𝑥 = 𝐵 → ( 𝑥 ∈ ℤ ↔ 𝐵 ∈ ℤ ) )
101 100 anbi2d ⊢ ( 𝑥 = 𝐵 → ( ( 𝜑 ∧ 𝑥 ∈ ℤ ) ↔ ( 𝜑 ∧ 𝐵 ∈ ℤ ) ) )
102 5 eleq1d ⊢ ( 𝑥 = 𝐵 → ( 𝐸 ∈ ℝ ↔ 𝐷 ∈ ℝ ) )
103 101 102 imbi12d ⊢ ( 𝑥 = 𝐵 → ( ( ( 𝜑 ∧ 𝑥 ∈ ℤ ) → 𝐸 ∈ ℝ ) ↔ ( ( 𝜑 ∧ 𝐵 ∈ ℤ ) → 𝐷 ∈ ℝ ) ) )
104 103 2 vtoclg ⊢ ( 𝐵 ∈ ℤ → ( ( 𝜑 ∧ 𝐵 ∈ ℤ ) → 𝐷 ∈ ℝ ) )
105 104 anabsi7 ⊢ ( ( 𝜑 ∧ 𝐵 ∈ ℤ ) → 𝐷 ∈ ℝ )
106 105 3adant2 ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 𝐷 ∈ ℝ )
107 18 5 99 106 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝐵 ) = 𝐷 )
108 98 107 breq12d ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝐴 ) < ( ( 𝑥 ∈ ℤ ↦ 𝐸 ) ‘ 𝐵 ) ↔ 𝐶 < 𝐷 ) )
109 89 108 bitrd ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 < 𝐵 ↔ 𝐶 < 𝐷 ) )