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