Metamath Proof Explorer

Theorem monoordxrv

Description: Ordering relation for a monotonic sequence, increasing case. (Contributed by Glauco Siliprandi, 13-Feb-2022)

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

Proof

Step Hyp Ref Expression
1 monoordxrv.1 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
2 monoordxrv.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ* )
3 monoordxrv.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ( 𝐹 ‘ 𝑘 ) ≤ ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
4 eluzfz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ( 𝑀 ... 𝑁 ) )
5 1 4 syl ⊢ ( 𝜑 → 𝑁 ∈ ( 𝑀 ... 𝑁 ) )
6 eleq1 ⊢ ( 𝑥 = 𝑀 → ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↔ 𝑀 ∈ ( 𝑀 ... 𝑁 ) ) )
7 fveq2 ⊢ ( 𝑥 = 𝑀 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑀 ) )
8 7 breq2d ⊢ ( 𝑥 = 𝑀 → ( ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐹 ‘ 𝑀 ) ) )
9 6 8 imbi12d ⊢ ( 𝑥 = 𝑀 → ( ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ↔ ( 𝑀 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐹 ‘ 𝑀 ) ) ) )
10 9 imbi2d ⊢ ( 𝑥 = 𝑀 → ( ( 𝜑 → ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ) ↔ ( 𝜑 → ( 𝑀 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐹 ‘ 𝑀 ) ) ) ) )
11 eleq1 ⊢ ( 𝑥 = 𝑛 → ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↔ 𝑛 ∈ ( 𝑀 ... 𝑁 ) ) )
12 fveq2 ⊢ ( 𝑥 = 𝑛 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑛 ) )
13 12 breq2d ⊢ ( 𝑥 = 𝑛 → ( ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐹 ‘ 𝑛 ) ) )
14 11 13 imbi12d ⊢ ( 𝑥 = 𝑛 → ( ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ↔ ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐹 ‘ 𝑛 ) ) ) )
15 14 imbi2d ⊢ ( 𝑥 = 𝑛 → ( ( 𝜑 → ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ) ↔ ( 𝜑 → ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐹 ‘ 𝑛 ) ) ) ) )
16 eleq1 ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) )
17 fveq2 ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
18 17 breq2d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
19 16 18 imbi12d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ↔ ( ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) )
20 19 imbi2d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( 𝜑 → ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ) ↔ ( 𝜑 → ( ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) ) )
21 eleq1 ⊢ ( 𝑥 = 𝑁 → ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↔ 𝑁 ∈ ( 𝑀 ... 𝑁 ) ) )
22 fveq2 ⊢ ( 𝑥 = 𝑁 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑁 ) )
23 22 breq2d ⊢ ( 𝑥 = 𝑁 → ( ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐹 ‘ 𝑁 ) ) )
24 21 23 imbi12d ⊢ ( 𝑥 = 𝑁 → ( ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ↔ ( 𝑁 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐹 ‘ 𝑁 ) ) ) )
25 24 imbi2d ⊢ ( 𝑥 = 𝑁 → ( ( 𝜑 → ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ) ↔ ( 𝜑 → ( 𝑁 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐹 ‘ 𝑁 ) ) ) ) )
26 eluzfz1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ( 𝑀 ... 𝑁 ) )
27 1 26 syl ⊢ ( 𝜑 → 𝑀 ∈ ( 𝑀 ... 𝑁 ) )
28 2 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ* )
29 fveq2 ⊢ ( 𝑘 = 𝑀 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑀 ) )
30 29 eleq1d ⊢ ( 𝑘 = 𝑀 → ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ* ↔ ( 𝐹 ‘ 𝑀 ) ∈ ℝ* ) )
31 30 rspcv ⊢ ( 𝑀 ∈ ( 𝑀 ... 𝑁 ) → ( ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ* → ( 𝐹 ‘ 𝑀 ) ∈ ℝ* ) )
32 27 28 31 sylc ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ∈ ℝ* )
33 32 xrleidd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐹 ‘ 𝑀 ) )
34 33 a1d ⊢ ( 𝜑 → ( 𝑀 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐹 ‘ 𝑀 ) ) )
35 34 a1i ⊢ ( 𝑀 ∈ ℤ → ( 𝜑 → ( 𝑀 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐹 ‘ 𝑀 ) ) ) )
36 simprl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) )
37 simprr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) )
38 peano2fzr ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → 𝑛 ∈ ( 𝑀 ... 𝑁 ) )
39 36 37 38 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → 𝑛 ∈ ( 𝑀 ... 𝑁 ) )
40 39 expr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → 𝑛 ∈ ( 𝑀 ... 𝑁 ) ) )
41 40 imim1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐹 ‘ 𝑛 ) ) → ( ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐹 ‘ 𝑛 ) ) ) )
42 eluzelz ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑛 ∈ ℤ )
43 36 42 syl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → 𝑛 ∈ ℤ )
44 elfzuz3 ⊢ ( ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) )
45 37 44 syl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) )
46 eluzp1m1 ⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑛 ) )
47 43 45 46 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑛 ) )
48 elfzuzb ⊢ ( 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ↔ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑛 ) ) )
49 36 47 48 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) )
50 3 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ( 𝐹 ‘ 𝑘 ) ≤ ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
51 50 adantr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ( 𝐹 ‘ 𝑘 ) ≤ ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
52 fveq2 ⊢ ( 𝑘 = 𝑛 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑛 ) )
53 fvoveq1 ⊢ ( 𝑘 = 𝑛 → ( 𝐹 ‘ ( 𝑘 + 1 ) ) = ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
54 52 53 breq12d ⊢ ( 𝑘 = 𝑛 → ( ( 𝐹 ‘ 𝑘 ) ≤ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ↔ ( 𝐹 ‘ 𝑛 ) ≤ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
55 54 rspcv ⊢ ( 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) → ( ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ( 𝐹 ‘ 𝑘 ) ≤ ( 𝐹 ‘ ( 𝑘 + 1 ) ) → ( 𝐹 ‘ 𝑛 ) ≤ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
56 49 51 55 sylc ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ( 𝐹 ‘ 𝑛 ) ≤ ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
57 32 adantr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ( 𝐹 ‘ 𝑀 ) ∈ ℝ* )
58 28 adantr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ* )
59 52 eleq1d ⊢ ( 𝑘 = 𝑛 → ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ* ↔ ( 𝐹 ‘ 𝑛 ) ∈ ℝ* ) )
60 59 rspcv ⊢ ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) → ( ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ* → ( 𝐹 ‘ 𝑛 ) ∈ ℝ* ) )
61 39 58 60 sylc ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ( 𝐹 ‘ 𝑛 ) ∈ ℝ* )
62 fveq2 ⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
63 62 eleq1d ⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ* ↔ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ℝ* ) )
64 63 rspcv ⊢ ( ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → ( ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ* → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ℝ* ) )
65 37 58 64 sylc ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ℝ* )
66 xrletr ⊢ ( ( ( 𝐹 ‘ 𝑀 ) ∈ ℝ* ∧ ( 𝐹 ‘ 𝑛 ) ∈ ℝ* ∧ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ℝ* ) → ( ( ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐹 ‘ 𝑛 ) ∧ ( 𝐹 ‘ 𝑛 ) ≤ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) → ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
67 57 61 65 66 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ( ( ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐹 ‘ 𝑛 ) ∧ ( 𝐹 ‘ 𝑛 ) ≤ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) → ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
68 56 67 mpan2d ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ( ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐹 ‘ 𝑛 ) → ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
69 41 68 animpimp2impd ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝜑 → ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐹 ‘ 𝑛 ) ) ) → ( 𝜑 → ( ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) ) )
70 10 15 20 25 35 69 uzind4 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝜑 → ( 𝑁 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐹 ‘ 𝑁 ) ) ) )
71 1 70 mpcom ⊢ ( 𝜑 → ( 𝑁 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐹 ‘ 𝑁 ) ) )
72 5 71 mpd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐹 ‘ 𝑁 ) )