Metamath Proof Explorer

Theorem monoord

Description: Ordering relation for a monotonic sequence, increasing case. (Contributed by NM, 13-Mar-2005) (Revised by Mario Carneiro, 9-Feb-2014)

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

Proof

Step Hyp Ref Expression
1 monoord.1 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
2 monoord.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
3 monoord.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 fveq2 ⊢ ( 𝑘 = 𝑀 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑀 ) )
27 26 eleq1d ⊢ ( 𝑘 = 𝑀 → ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ↔ ( 𝐹 ‘ 𝑀 ) ∈ ℝ ) )
28 2 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
29 eluzfz1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ( 𝑀 ... 𝑁 ) )
30 1 29 syl ⊢ ( 𝜑 → 𝑀 ∈ ( 𝑀 ... 𝑁 ) )
31 27 28 30 rspcdva ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ∈ ℝ )
32 31 leidd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐹 ‘ 𝑀 ) )
33 32 a1d ⊢ ( 𝜑 → ( 𝑀 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐹 ‘ 𝑀 ) ) )
34 peano2fzr ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → 𝑛 ∈ ( 𝑀 ... 𝑁 ) )
35 34 adantl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → 𝑛 ∈ ( 𝑀 ... 𝑁 ) )
36 35 expr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → 𝑛 ∈ ( 𝑀 ... 𝑁 ) ) )
37 36 imim1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐹 ‘ 𝑛 ) ) → ( ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐹 ‘ 𝑛 ) ) ) )
38 fveq2 ⊢ ( 𝑘 = 𝑛 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑛 ) )
39 fvoveq1 ⊢ ( 𝑘 = 𝑛 → ( 𝐹 ‘ ( 𝑘 + 1 ) ) = ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
40 38 39 breq12d ⊢ ( 𝑘 = 𝑛 → ( ( 𝐹 ‘ 𝑘 ) ≤ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ↔ ( 𝐹 ‘ 𝑛 ) ≤ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
41 3 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ( 𝐹 ‘ 𝑘 ) ≤ ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
42 41 adantr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ( 𝐹 ‘ 𝑘 ) ≤ ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
43 simprl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) )
44 eluzelz ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑛 ∈ ℤ )
45 43 44 syl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → 𝑛 ∈ ℤ )
46 simprr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) )
47 elfzuz3 ⊢ ( ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) )
48 46 47 syl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) )
49 eluzp1m1 ⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑛 ) )
50 45 48 49 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑛 ) )
51 elfzuzb ⊢ ( 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ↔ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑛 ) ) )
52 43 50 51 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) )
53 40 42 52 rspcdva ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ( 𝐹 ‘ 𝑛 ) ≤ ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
54 31 adantr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ( 𝐹 ‘ 𝑀 ) ∈ ℝ )
55 38 eleq1d ⊢ ( 𝑘 = 𝑛 → ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ↔ ( 𝐹 ‘ 𝑛 ) ∈ ℝ ) )
56 28 adantr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
57 55 56 35 rspcdva ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ( 𝐹 ‘ 𝑛 ) ∈ ℝ )
58 fveq2 ⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
59 58 eleq1d ⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ↔ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ℝ ) )
60 59 56 46 rspcdva ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ℝ )
61 letr ⊢ ( ( ( 𝐹 ‘ 𝑀 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑛 ) ∈ ℝ ∧ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ℝ ) → ( ( ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐹 ‘ 𝑛 ) ∧ ( 𝐹 ‘ 𝑛 ) ≤ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) → ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
62 54 57 60 61 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ( ( ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐹 ‘ 𝑛 ) ∧ ( 𝐹 ‘ 𝑛 ) ≤ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) → ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
63 53 62 mpan2d ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ( ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐹 ‘ 𝑛 ) → ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
64 37 63 animpimp2impd ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝜑 → ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐹 ‘ 𝑛 ) ) ) → ( 𝜑 → ( ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) ) )
65 10 15 20 25 33 64 uzind4i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝜑 → ( 𝑁 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐹 ‘ 𝑁 ) ) ) )
66 1 65 mpcom ⊢ ( 𝜑 → ( 𝑁 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐹 ‘ 𝑁 ) ) )
67 5 66 mpd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐹 ‘ 𝑁 ) )