Metamath Proof Explorer

Theorem monoords

Description: Ordering relation for a strictly monotonic sequence, increasing case. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses monoords.fk ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
monoords.flt ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) < ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
monoords.i ⊢ ( 𝜑 → 𝐼 ∈ ( 𝑀 ... 𝑁 ) )
monoords.j ⊢ ( 𝜑 → 𝐽 ∈ ( 𝑀 ... 𝑁 ) )
monoords.iltj ⊢ ( 𝜑 → 𝐼 < 𝐽 )
Assertion monoords ( 𝜑 → ( 𝐹 ‘ 𝐼 ) < ( 𝐹 ‘ 𝐽 ) )

Proof

Step Hyp Ref Expression
1 monoords.fk ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
2 monoords.flt ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) < ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
3 monoords.i ⊢ ( 𝜑 → 𝐼 ∈ ( 𝑀 ... 𝑁 ) )
4 monoords.j ⊢ ( 𝜑 → 𝐽 ∈ ( 𝑀 ... 𝑁 ) )
5 monoords.iltj ⊢ ( 𝜑 → 𝐼 < 𝐽 )
6 3 ancli ⊢ ( 𝜑 → ( 𝜑 ∧ 𝐼 ∈ ( 𝑀 ... 𝑁 ) ) )
7 eleq1 ⊢ ( 𝑘 = 𝐼 → ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↔ 𝐼 ∈ ( 𝑀 ... 𝑁 ) ) )
8 7 anbi2d ⊢ ( 𝑘 = 𝐼 → ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) ↔ ( 𝜑 ∧ 𝐼 ∈ ( 𝑀 ... 𝑁 ) ) ) )
9 fveq2 ⊢ ( 𝑘 = 𝐼 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝐼 ) )
10 9 eleq1d ⊢ ( 𝑘 = 𝐼 → ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ↔ ( 𝐹 ‘ 𝐼 ) ∈ ℝ ) )
11 8 10 imbi12d ⊢ ( 𝑘 = 𝐼 → ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) ↔ ( ( 𝜑 ∧ 𝐼 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝐼 ) ∈ ℝ ) ) )
12 11 1 vtoclg ⊢ ( 𝐼 ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝜑 ∧ 𝐼 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝐼 ) ∈ ℝ ) )
13 3 6 12 sylc ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐼 ) ∈ ℝ )
14 elfzel1 ⊢ ( 𝐼 ∈ ( 𝑀 ... 𝑁 ) → 𝑀 ∈ ℤ )
15 3 14 syl ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
16 3 elfzelzd ⊢ ( 𝜑 → 𝐼 ∈ ℤ )
17 elfzle1 ⊢ ( 𝐼 ∈ ( 𝑀 ... 𝑁 ) → 𝑀 ≤ 𝐼 )
18 3 17 syl ⊢ ( 𝜑 → 𝑀 ≤ 𝐼 )
19 eluz2 ⊢ ( 𝐼 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ 𝐼 ∈ ℤ ∧ 𝑀 ≤ 𝐼 ) )
20 15 16 18 19 syl3anbrc ⊢ ( 𝜑 → 𝐼 ∈ ( ℤ≥ ‘ 𝑀 ) )
21 elfzuz2 ⊢ ( 𝐼 ∈ ( 𝑀 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
22 3 21 syl ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
23 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℤ )
24 22 23 syl ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
25 16 zred ⊢ ( 𝜑 → 𝐼 ∈ ℝ )
26 4 elfzelzd ⊢ ( 𝜑 → 𝐽 ∈ ℤ )
27 26 zred ⊢ ( 𝜑 → 𝐽 ∈ ℝ )
28 24 zred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
29 elfzle2 ⊢ ( 𝐽 ∈ ( 𝑀 ... 𝑁 ) → 𝐽 ≤ 𝑁 )
30 4 29 syl ⊢ ( 𝜑 → 𝐽 ≤ 𝑁 )
31 25 27 28 5 30 ltletrd ⊢ ( 𝜑 → 𝐼 < 𝑁 )
32 elfzo2 ⊢ ( 𝐼 ∈ ( 𝑀 ..^ 𝑁 ) ↔ ( 𝐼 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ℤ ∧ 𝐼 < 𝑁 ) )
33 20 24 31 32 syl3anbrc ⊢ ( 𝜑 → 𝐼 ∈ ( 𝑀 ..^ 𝑁 ) )
34 fzofzp1 ⊢ ( 𝐼 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝐼 + 1 ) ∈ ( 𝑀 ... 𝑁 ) )
35 33 34 syl ⊢ ( 𝜑 → ( 𝐼 + 1 ) ∈ ( 𝑀 ... 𝑁 ) )
36 35 ancli ⊢ ( 𝜑 → ( 𝜑 ∧ ( 𝐼 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) )
37 eleq1 ⊢ ( 𝑘 = ( 𝐼 + 1 ) → ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝐼 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) )
38 37 anbi2d ⊢ ( 𝑘 = ( 𝐼 + 1 ) → ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) ↔ ( 𝜑 ∧ ( 𝐼 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) )
39 fveq2 ⊢ ( 𝑘 = ( 𝐼 + 1 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ ( 𝐼 + 1 ) ) )
40 39 eleq1d ⊢ ( 𝑘 = ( 𝐼 + 1 ) → ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ↔ ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ) )
41 38 40 imbi12d ⊢ ( 𝑘 = ( 𝐼 + 1 ) → ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) ↔ ( ( 𝜑 ∧ ( 𝐼 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ) ) )
42 41 1 vtoclg ⊢ ( ( 𝐼 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝜑 ∧ ( 𝐼 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ) )
43 35 36 42 sylc ⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ )
44 4 ancli ⊢ ( 𝜑 → ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) )
45 eleq1 ⊢ ( 𝑘 = 𝐽 → ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↔ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) )
46 45 anbi2d ⊢ ( 𝑘 = 𝐽 → ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) ↔ ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) ) )
47 fveq2 ⊢ ( 𝑘 = 𝐽 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝐽 ) )
48 47 eleq1d ⊢ ( 𝑘 = 𝐽 → ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ↔ ( 𝐹 ‘ 𝐽 ) ∈ ℝ ) )
49 46 48 imbi12d ⊢ ( 𝑘 = 𝐽 → ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) ↔ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝐽 ) ∈ ℝ ) ) )
50 49 1 vtoclg ⊢ ( 𝐽 ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝐽 ) ∈ ℝ ) )
51 4 44 50 sylc ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐽 ) ∈ ℝ )
52 33 ancli ⊢ ( 𝜑 → ( 𝜑 ∧ 𝐼 ∈ ( 𝑀 ..^ 𝑁 ) ) )
53 eleq1 ⊢ ( 𝑘 = 𝐼 → ( 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ↔ 𝐼 ∈ ( 𝑀 ..^ 𝑁 ) ) )
54 53 anbi2d ⊢ ( 𝑘 = 𝐼 → ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ↔ ( 𝜑 ∧ 𝐼 ∈ ( 𝑀 ..^ 𝑁 ) ) ) )
55 fvoveq1 ⊢ ( 𝑘 = 𝐼 → ( 𝐹 ‘ ( 𝑘 + 1 ) ) = ( 𝐹 ‘ ( 𝐼 + 1 ) ) )
56 9 55 breq12d ⊢ ( 𝑘 = 𝐼 → ( ( 𝐹 ‘ 𝑘 ) < ( 𝐹 ‘ ( 𝑘 + 1 ) ) ↔ ( 𝐹 ‘ 𝐼 ) < ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) )
57 54 56 imbi12d ⊢ ( 𝑘 = 𝐼 → ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) < ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ↔ ( ( 𝜑 ∧ 𝐼 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐹 ‘ 𝐼 ) < ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) ) )
58 57 2 vtoclg ⊢ ( 𝐼 ∈ ( 𝑀 ..^ 𝑁 ) → ( ( 𝜑 ∧ 𝐼 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐹 ‘ 𝐼 ) < ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) )
59 33 52 58 sylc ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐼 ) < ( 𝐹 ‘ ( 𝐼 + 1 ) ) )
60 16 peano2zd ⊢ ( 𝜑 → ( 𝐼 + 1 ) ∈ ℤ )
61 zltp1le ⊢ ( ( 𝐼 ∈ ℤ ∧ 𝐽 ∈ ℤ ) → ( 𝐼 < 𝐽 ↔ ( 𝐼 + 1 ) ≤ 𝐽 ) )
62 16 26 61 syl2anc ⊢ ( 𝜑 → ( 𝐼 < 𝐽 ↔ ( 𝐼 + 1 ) ≤ 𝐽 ) )
63 5 62 mpbid ⊢ ( 𝜑 → ( 𝐼 + 1 ) ≤ 𝐽 )
64 eluz2 ⊢ ( 𝐽 ∈ ( ℤ≥ ‘ ( 𝐼 + 1 ) ) ↔ ( ( 𝐼 + 1 ) ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ ( 𝐼 + 1 ) ≤ 𝐽 ) )
65 60 26 63 64 syl3anbrc ⊢ ( 𝜑 → 𝐽 ∈ ( ℤ≥ ‘ ( 𝐼 + 1 ) ) )
66 15 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐼 + 1 ) ... 𝐽 ) ) → 𝑀 ∈ ℤ )
67 24 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐼 + 1 ) ... 𝐽 ) ) → 𝑁 ∈ ℤ )
68 elfzelz ⊢ ( 𝑘 ∈ ( ( 𝐼 + 1 ) ... 𝐽 ) → 𝑘 ∈ ℤ )
69 68 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐼 + 1 ) ... 𝐽 ) ) → 𝑘 ∈ ℤ )
70 66 zred ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐼 + 1 ) ... 𝐽 ) ) → 𝑀 ∈ ℝ )
71 69 zred ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐼 + 1 ) ... 𝐽 ) ) → 𝑘 ∈ ℝ )
72 60 zred ⊢ ( 𝜑 → ( 𝐼 + 1 ) ∈ ℝ )
73 72 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐼 + 1 ) ... 𝐽 ) ) → ( 𝐼 + 1 ) ∈ ℝ )
74 25 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐼 + 1 ) ... 𝐽 ) ) → 𝐼 ∈ ℝ )
75 18 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐼 + 1 ) ... 𝐽 ) ) → 𝑀 ≤ 𝐼 )
76 74 ltp1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐼 + 1 ) ... 𝐽 ) ) → 𝐼 < ( 𝐼 + 1 ) )
77 70 74 73 75 76 lelttrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐼 + 1 ) ... 𝐽 ) ) → 𝑀 < ( 𝐼 + 1 ) )
78 elfzle1 ⊢ ( 𝑘 ∈ ( ( 𝐼 + 1 ) ... 𝐽 ) → ( 𝐼 + 1 ) ≤ 𝑘 )
79 78 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐼 + 1 ) ... 𝐽 ) ) → ( 𝐼 + 1 ) ≤ 𝑘 )
80 70 73 71 77 79 ltletrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐼 + 1 ) ... 𝐽 ) ) → 𝑀 < 𝑘 )
81 70 71 80 ltled ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐼 + 1 ) ... 𝐽 ) ) → 𝑀 ≤ 𝑘 )
82 27 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐼 + 1 ) ... 𝐽 ) ) → 𝐽 ∈ ℝ )
83 67 zred ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐼 + 1 ) ... 𝐽 ) ) → 𝑁 ∈ ℝ )
84 elfzle2 ⊢ ( 𝑘 ∈ ( ( 𝐼 + 1 ) ... 𝐽 ) → 𝑘 ≤ 𝐽 )
85 84 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐼 + 1 ) ... 𝐽 ) ) → 𝑘 ≤ 𝐽 )
86 30 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐼 + 1 ) ... 𝐽 ) ) → 𝐽 ≤ 𝑁 )
87 71 82 83 85 86 letrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐼 + 1 ) ... 𝐽 ) ) → 𝑘 ≤ 𝑁 )
88 66 67 69 81 87 elfzd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐼 + 1 ) ... 𝐽 ) ) → 𝑘 ∈ ( 𝑀 ... 𝑁 ) )
89 88 1 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐼 + 1 ) ... 𝐽 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
90 15 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐼 + 1 ) ... ( 𝐽 − 1 ) ) ) → 𝑀 ∈ ℤ )
91 24 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐼 + 1 ) ... ( 𝐽 − 1 ) ) ) → 𝑁 ∈ ℤ )
92 elfzelz ⊢ ( 𝑘 ∈ ( ( 𝐼 + 1 ) ... ( 𝐽 − 1 ) ) → 𝑘 ∈ ℤ )
93 92 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐼 + 1 ) ... ( 𝐽 − 1 ) ) ) → 𝑘 ∈ ℤ )
94 90 zred ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐼 + 1 ) ... ( 𝐽 − 1 ) ) ) → 𝑀 ∈ ℝ )
95 93 zred ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐼 + 1 ) ... ( 𝐽 − 1 ) ) ) → 𝑘 ∈ ℝ )
96 72 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐼 + 1 ) ... ( 𝐽 − 1 ) ) ) → ( 𝐼 + 1 ) ∈ ℝ )
97 15 zred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
98 25 ltp1d ⊢ ( 𝜑 → 𝐼 < ( 𝐼 + 1 ) )
99 97 25 72 18 98 lelttrd ⊢ ( 𝜑 → 𝑀 < ( 𝐼 + 1 ) )
100 99 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐼 + 1 ) ... ( 𝐽 − 1 ) ) ) → 𝑀 < ( 𝐼 + 1 ) )
101 elfzle1 ⊢ ( 𝑘 ∈ ( ( 𝐼 + 1 ) ... ( 𝐽 − 1 ) ) → ( 𝐼 + 1 ) ≤ 𝑘 )
102 101 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐼 + 1 ) ... ( 𝐽 − 1 ) ) ) → ( 𝐼 + 1 ) ≤ 𝑘 )
103 94 96 95 100 102 ltletrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐼 + 1 ) ... ( 𝐽 − 1 ) ) ) → 𝑀 < 𝑘 )
104 94 95 103 ltled ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐼 + 1 ) ... ( 𝐽 − 1 ) ) ) → 𝑀 ≤ 𝑘 )
105 91 zred ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐼 + 1 ) ... ( 𝐽 − 1 ) ) ) → 𝑁 ∈ ℝ )
106 peano2rem ⊢ ( 𝐽 ∈ ℝ → ( 𝐽 − 1 ) ∈ ℝ )
107 27 106 syl ⊢ ( 𝜑 → ( 𝐽 − 1 ) ∈ ℝ )
108 107 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐼 + 1 ) ... ( 𝐽 − 1 ) ) ) → ( 𝐽 − 1 ) ∈ ℝ )
109 elfzle2 ⊢ ( 𝑘 ∈ ( ( 𝐼 + 1 ) ... ( 𝐽 − 1 ) ) → 𝑘 ≤ ( 𝐽 − 1 ) )
110 109 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐼 + 1 ) ... ( 𝐽 − 1 ) ) ) → 𝑘 ≤ ( 𝐽 − 1 ) )
111 27 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐼 + 1 ) ... ( 𝐽 − 1 ) ) ) → 𝐽 ∈ ℝ )
112 111 ltm1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐼 + 1 ) ... ( 𝐽 − 1 ) ) ) → ( 𝐽 − 1 ) < 𝐽 )
113 30 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐼 + 1 ) ... ( 𝐽 − 1 ) ) ) → 𝐽 ≤ 𝑁 )
114 108 111 105 112 113 ltletrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐼 + 1 ) ... ( 𝐽 − 1 ) ) ) → ( 𝐽 − 1 ) < 𝑁 )
115 95 108 105 110 114 lelttrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐼 + 1 ) ... ( 𝐽 − 1 ) ) ) → 𝑘 < 𝑁 )
116 95 105 115 ltled ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐼 + 1 ) ... ( 𝐽 − 1 ) ) ) → 𝑘 ≤ 𝑁 )
117 90 91 93 104 116 elfzd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐼 + 1 ) ... ( 𝐽 − 1 ) ) ) → 𝑘 ∈ ( 𝑀 ... 𝑁 ) )
118 117 1 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐼 + 1 ) ... ( 𝐽 − 1 ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
119 peano2zm ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 − 1 ) ∈ ℤ )
120 91 119 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐼 + 1 ) ... ( 𝐽 − 1 ) ) ) → ( 𝑁 − 1 ) ∈ ℤ )
121 120 zred ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐼 + 1 ) ... ( 𝐽 − 1 ) ) ) → ( 𝑁 − 1 ) ∈ ℝ )
122 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
123 27 28 122 30 lesub1dd ⊢ ( 𝜑 → ( 𝐽 − 1 ) ≤ ( 𝑁 − 1 ) )
124 123 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐼 + 1 ) ... ( 𝐽 − 1 ) ) ) → ( 𝐽 − 1 ) ≤ ( 𝑁 − 1 ) )
125 95 108 121 110 124 letrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐼 + 1 ) ... ( 𝐽 − 1 ) ) ) → 𝑘 ≤ ( 𝑁 − 1 ) )
126 90 120 93 104 125 elfzd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐼 + 1 ) ... ( 𝐽 − 1 ) ) ) → 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) )
127 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) )
128 fzoval ⊢ ( 𝑁 ∈ ℤ → ( 𝑀 ..^ 𝑁 ) = ( 𝑀 ... ( 𝑁 − 1 ) ) )
129 24 128 syl ⊢ ( 𝜑 → ( 𝑀 ..^ 𝑁 ) = ( 𝑀 ... ( 𝑁 − 1 ) ) )
130 129 eqcomd ⊢ ( 𝜑 → ( 𝑀 ... ( 𝑁 − 1 ) ) = ( 𝑀 ..^ 𝑁 ) )
131 130 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ( 𝑀 ... ( 𝑁 − 1 ) ) = ( 𝑀 ..^ 𝑁 ) )
132 127 131 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) )
133 fzofzp1 ⊢ ( 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝑘 + 1 ) ∈ ( 𝑀 ... 𝑁 ) )
134 132 133 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ( 𝑘 + 1 ) ∈ ( 𝑀 ... 𝑁 ) )
135 simpl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → 𝜑 )
136 135 134 jca ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ( 𝜑 ∧ ( 𝑘 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) )
137 eleq1 ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 𝑗 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝑘 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) )
138 137 anbi2d ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) ↔ ( 𝜑 ∧ ( 𝑘 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) )
139 fveq2 ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 𝐹 ‘ 𝑗 ) = ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
140 139 eleq1d ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( 𝐹 ‘ 𝑗 ) ∈ ℝ ↔ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ ℝ ) )
141 138 140 imbi12d ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ ) ↔ ( ( 𝜑 ∧ ( 𝑘 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ ℝ ) ) )
142 eleq1 ⊢ ( 𝑘 = 𝑗 → ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↔ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) )
143 142 anbi2d ⊢ ( 𝑘 = 𝑗 → ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) ↔ ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) ) )
144 fveq2 ⊢ ( 𝑘 = 𝑗 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑗 ) )
145 144 eleq1d ⊢ ( 𝑘 = 𝑗 → ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ↔ ( 𝐹 ‘ 𝑗 ) ∈ ℝ ) )
146 143 145 imbi12d ⊢ ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ ) ) )
147 146 1 chvarvv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ )
148 141 147 vtoclg ⊢ ( ( 𝑘 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝜑 ∧ ( 𝑘 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ ℝ ) )
149 134 136 148 sylc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ ℝ )
150 126 149 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐼 + 1 ) ... ( 𝐽 − 1 ) ) ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ ℝ )
151 132 2 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ( 𝐹 ‘ 𝑘 ) < ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
152 126 151 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐼 + 1 ) ... ( 𝐽 − 1 ) ) ) → ( 𝐹 ‘ 𝑘 ) < ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
153 118 150 152 ltled ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐼 + 1 ) ... ( 𝐽 − 1 ) ) ) → ( 𝐹 ‘ 𝑘 ) ≤ ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
154 65 89 153 monoord ⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝐹 ‘ 𝐽 ) )
155 13 43 51 59 154 ltletrd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐼 ) < ( 𝐹 ‘ 𝐽 ) )