Metamath Proof Explorer

Theorem smonoord

Description: Ordering relation for a strictly monotonic sequence, increasing case. Analogous to monoord (except that the case M = N must be excluded). Duplicate of monoords ? (Contributed by AV, 12-Jul-2020)

Ref Expression
Hypotheses smonoord.0 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
smonoord.1 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) )
smonoord.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
smonoord.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ( 𝐹 ‘ 𝑘 ) < ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
Assertion smonoord ( 𝜑 → ( 𝐹 ‘ 𝑀 ) < ( 𝐹 ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 smonoord.0 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2 smonoord.1 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) )
3 smonoord.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
4 smonoord.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ( 𝐹 ‘ 𝑘 ) < ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
5 eluzfz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) → 𝑁 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) )
6 2 5 syl ⊢ ( 𝜑 → 𝑁 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) )
7 eleq1 ⊢ ( 𝑥 = ( 𝑀 + 1 ) → ( 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ↔ ( 𝑀 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
8 fveq2 ⊢ ( 𝑥 = ( 𝑀 + 1 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝑀 + 1 ) ) )
9 8 breq2d ⊢ ( 𝑥 = ( 𝑀 + 1 ) → ( ( 𝐹 ‘ 𝑀 ) < ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑀 ) < ( 𝐹 ‘ ( 𝑀 + 1 ) ) ) )
10 7 9 imbi12d ⊢ ( 𝑥 = ( 𝑀 + 1 ) → ( ( 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( 𝐹 ‘ 𝑀 ) < ( 𝐹 ‘ 𝑥 ) ) ↔ ( ( 𝑀 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( 𝐹 ‘ 𝑀 ) < ( 𝐹 ‘ ( 𝑀 + 1 ) ) ) ) )
11 10 imbi2d ⊢ ( 𝑥 = ( 𝑀 + 1 ) → ( ( 𝜑 → ( 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( 𝐹 ‘ 𝑀 ) < ( 𝐹 ‘ 𝑥 ) ) ) ↔ ( 𝜑 → ( ( 𝑀 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( 𝐹 ‘ 𝑀 ) < ( 𝐹 ‘ ( 𝑀 + 1 ) ) ) ) ) )
12 eleq1 ⊢ ( 𝑥 = 𝑛 → ( 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ↔ 𝑛 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
13 fveq2 ⊢ ( 𝑥 = 𝑛 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑛 ) )
14 13 breq2d ⊢ ( 𝑥 = 𝑛 → ( ( 𝐹 ‘ 𝑀 ) < ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑀 ) < ( 𝐹 ‘ 𝑛 ) ) )
15 12 14 imbi12d ⊢ ( 𝑥 = 𝑛 → ( ( 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( 𝐹 ‘ 𝑀 ) < ( 𝐹 ‘ 𝑥 ) ) ↔ ( 𝑛 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( 𝐹 ‘ 𝑀 ) < ( 𝐹 ‘ 𝑛 ) ) ) )
16 15 imbi2d ⊢ ( 𝑥 = 𝑛 → ( ( 𝜑 → ( 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( 𝐹 ‘ 𝑀 ) < ( 𝐹 ‘ 𝑥 ) ) ) ↔ ( 𝜑 → ( 𝑛 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( 𝐹 ‘ 𝑀 ) < ( 𝐹 ‘ 𝑛 ) ) ) ) )
17 eleq1 ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ↔ ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
18 fveq2 ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
19 18 breq2d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( 𝐹 ‘ 𝑀 ) < ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑀 ) < ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
20 17 19 imbi12d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( 𝐹 ‘ 𝑀 ) < ( 𝐹 ‘ 𝑥 ) ) ↔ ( ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( 𝐹 ‘ 𝑀 ) < ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) )
21 20 imbi2d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( 𝜑 → ( 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( 𝐹 ‘ 𝑀 ) < ( 𝐹 ‘ 𝑥 ) ) ) ↔ ( 𝜑 → ( ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( 𝐹 ‘ 𝑀 ) < ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) ) )
22 eleq1 ⊢ ( 𝑥 = 𝑁 → ( 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ↔ 𝑁 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
23 fveq2 ⊢ ( 𝑥 = 𝑁 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑁 ) )
24 23 breq2d ⊢ ( 𝑥 = 𝑁 → ( ( 𝐹 ‘ 𝑀 ) < ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑀 ) < ( 𝐹 ‘ 𝑁 ) ) )
25 22 24 imbi12d ⊢ ( 𝑥 = 𝑁 → ( ( 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( 𝐹 ‘ 𝑀 ) < ( 𝐹 ‘ 𝑥 ) ) ↔ ( 𝑁 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( 𝐹 ‘ 𝑀 ) < ( 𝐹 ‘ 𝑁 ) ) ) )
26 25 imbi2d ⊢ ( 𝑥 = 𝑁 → ( ( 𝜑 → ( 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( 𝐹 ‘ 𝑀 ) < ( 𝐹 ‘ 𝑥 ) ) ) ↔ ( 𝜑 → ( 𝑁 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( 𝐹 ‘ 𝑀 ) < ( 𝐹 ‘ 𝑁 ) ) ) ) )
27 eluzp1m1 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
28 1 2 27 syl2anc ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
29 eluzfz1 ⊢ ( ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) )
30 28 29 syl ⊢ ( 𝜑 → 𝑀 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) )
31 4 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ( 𝐹 ‘ 𝑘 ) < ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
32 fveq2 ⊢ ( 𝑘 = 𝑀 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑀 ) )
33 fvoveq1 ⊢ ( 𝑘 = 𝑀 → ( 𝐹 ‘ ( 𝑘 + 1 ) ) = ( 𝐹 ‘ ( 𝑀 + 1 ) ) )
34 32 33 breq12d ⊢ ( 𝑘 = 𝑀 → ( ( 𝐹 ‘ 𝑘 ) < ( 𝐹 ‘ ( 𝑘 + 1 ) ) ↔ ( 𝐹 ‘ 𝑀 ) < ( 𝐹 ‘ ( 𝑀 + 1 ) ) ) )
35 34 rspcv ⊢ ( 𝑀 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) → ( ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ( 𝐹 ‘ 𝑘 ) < ( 𝐹 ‘ ( 𝑘 + 1 ) ) → ( 𝐹 ‘ 𝑀 ) < ( 𝐹 ‘ ( 𝑀 + 1 ) ) ) )
36 30 31 35 sylc ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) < ( 𝐹 ‘ ( 𝑀 + 1 ) ) )
37 36 a1d ⊢ ( 𝜑 → ( ( 𝑀 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( 𝐹 ‘ 𝑀 ) < ( 𝐹 ‘ ( 𝑀 + 1 ) ) ) )
38 37 a1i ⊢ ( ( 𝑀 + 1 ) ∈ ℤ → ( 𝜑 → ( ( 𝑀 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( 𝐹 ‘ 𝑀 ) < ( 𝐹 ‘ ( 𝑀 + 1 ) ) ) ) )
39 peano2fzr ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → 𝑛 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) )
40 39 adantll ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ∧ ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → 𝑛 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) )
41 40 ex ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → 𝑛 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
42 41 imim1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( ( 𝑛 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( 𝐹 ‘ 𝑀 ) < ( 𝐹 ‘ 𝑛 ) ) → ( ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( 𝐹 ‘ 𝑀 ) < ( 𝐹 ‘ 𝑛 ) ) ) )
43 peano2uzr ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) )
44 43 ex ⊢ ( 𝑀 ∈ ℤ → ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ) )
45 44 1 syl11 ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) → ( 𝜑 → 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ) )
46 45 adantr ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → ( 𝜑 → 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ) )
47 46 impcom ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) )
48 eluzelz ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) → 𝑛 ∈ ℤ )
49 48 adantr ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → 𝑛 ∈ ℤ )
50 49 adantl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) → 𝑛 ∈ ℤ )
51 elfzuz3 ⊢ ( ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) )
52 51 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) )
53 eluzp1m1 ⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑛 ) )
54 50 52 53 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑛 ) )
55 elfzuzb ⊢ ( 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ↔ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑛 ) ) )
56 47 54 55 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) → 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) )
57 31 adantr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) → ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ( 𝐹 ‘ 𝑘 ) < ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
58 fveq2 ⊢ ( 𝑘 = 𝑛 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑛 ) )
59 fvoveq1 ⊢ ( 𝑘 = 𝑛 → ( 𝐹 ‘ ( 𝑘 + 1 ) ) = ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
60 58 59 breq12d ⊢ ( 𝑘 = 𝑛 → ( ( 𝐹 ‘ 𝑘 ) < ( 𝐹 ‘ ( 𝑘 + 1 ) ) ↔ ( 𝐹 ‘ 𝑛 ) < ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
61 60 rspcv ⊢ ( 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) → ( ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ( 𝐹 ‘ 𝑘 ) < ( 𝐹 ‘ ( 𝑘 + 1 ) ) → ( 𝐹 ‘ 𝑛 ) < ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
62 56 57 61 sylc ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) → ( 𝐹 ‘ 𝑛 ) < ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
63 zre ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
64 63 lep1d ⊢ ( 𝑀 ∈ ℤ → 𝑀 ≤ ( 𝑀 + 1 ) )
65 1 64 jccir ⊢ ( 𝜑 → ( 𝑀 ∈ ℤ ∧ 𝑀 ≤ ( 𝑀 + 1 ) ) )
66 eluzuzle ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≤ ( 𝑀 + 1 ) ) → ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) )
67 65 2 66 sylc ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
68 eluzfz1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ( 𝑀 ... 𝑁 ) )
69 67 68 syl ⊢ ( 𝜑 → 𝑀 ∈ ( 𝑀 ... 𝑁 ) )
70 3 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
71 32 eleq1d ⊢ ( 𝑘 = 𝑀 → ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ↔ ( 𝐹 ‘ 𝑀 ) ∈ ℝ ) )
72 71 rspcv ⊢ ( 𝑀 ∈ ( 𝑀 ... 𝑁 ) → ( ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ → ( 𝐹 ‘ 𝑀 ) ∈ ℝ ) )
73 69 70 72 sylc ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ∈ ℝ )
74 73 adantr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) → ( 𝐹 ‘ 𝑀 ) ∈ ℝ )
75 fzp1ss ⊢ ( 𝑀 ∈ ℤ → ( ( 𝑀 + 1 ) ... 𝑁 ) ⊆ ( 𝑀 ... 𝑁 ) )
76 1 75 syl ⊢ ( 𝜑 → ( ( 𝑀 + 1 ) ... 𝑁 ) ⊆ ( 𝑀 ... 𝑁 ) )
77 76 sseld ⊢ ( 𝜑 → ( ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) )
78 77 com12 ⊢ ( ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( 𝜑 → ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) )
79 78 adantl ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → ( 𝜑 → ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) )
80 79 impcom ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) → ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) )
81 peano2fzr ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → 𝑛 ∈ ( 𝑀 ... 𝑁 ) )
82 47 80 81 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) → 𝑛 ∈ ( 𝑀 ... 𝑁 ) )
83 70 adantr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) → ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
84 58 eleq1d ⊢ ( 𝑘 = 𝑛 → ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ↔ ( 𝐹 ‘ 𝑛 ) ∈ ℝ ) )
85 84 rspcv ⊢ ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) → ( ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ → ( 𝐹 ‘ 𝑛 ) ∈ ℝ ) )
86 82 83 85 sylc ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) → ( 𝐹 ‘ 𝑛 ) ∈ ℝ )
87 fveq2 ⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
88 87 eleq1d ⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ↔ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ℝ ) )
89 88 rspcv ⊢ ( ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → ( ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ℝ ) )
90 80 83 89 sylc ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ℝ )
91 lttr ⊢ ( ( ( 𝐹 ‘ 𝑀 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑛 ) ∈ ℝ ∧ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ℝ ) → ( ( ( 𝐹 ‘ 𝑀 ) < ( 𝐹 ‘ 𝑛 ) ∧ ( 𝐹 ‘ 𝑛 ) < ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) → ( 𝐹 ‘ 𝑀 ) < ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
92 74 86 90 91 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) → ( ( ( 𝐹 ‘ 𝑀 ) < ( 𝐹 ‘ 𝑛 ) ∧ ( 𝐹 ‘ 𝑛 ) < ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) → ( 𝐹 ‘ 𝑀 ) < ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
93 62 92 mpan2d ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) → ( ( 𝐹 ‘ 𝑀 ) < ( 𝐹 ‘ 𝑛 ) → ( 𝐹 ‘ 𝑀 ) < ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
94 42 93 animpimp2impd ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) → ( ( 𝜑 → ( 𝑛 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( 𝐹 ‘ 𝑀 ) < ( 𝐹 ‘ 𝑛 ) ) ) → ( 𝜑 → ( ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( 𝐹 ‘ 𝑀 ) < ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) ) )
95 11 16 21 26 38 94 uzind4 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) → ( 𝜑 → ( 𝑁 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( 𝐹 ‘ 𝑀 ) < ( 𝐹 ‘ 𝑁 ) ) ) )
96 2 95 mpcom ⊢ ( 𝜑 → ( 𝑁 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( 𝐹 ‘ 𝑀 ) < ( 𝐹 ‘ 𝑁 ) ) )
97 6 96 mpd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) < ( 𝐹 ‘ 𝑁 ) )