Metamath Proof Explorer

Theorem monoord2

Description: Ordering relation for a monotonic sequence, decreasing case. (Contributed by Mario Carneiro, 18-Jul-2014)

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

Proof

Step Hyp Ref Expression
1 monoord2.1 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
2 monoord2.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
3 monoord2.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐹 ‘ 𝑘 ) )
4 2 renegcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → - ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
5 4 fmpttd ⊢ ( 𝜑 → ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ - ( 𝐹 ‘ 𝑘 ) ) : ( 𝑀 ... 𝑁 ) ⟶ ℝ )
6 5 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ - ( 𝐹 ‘ 𝑘 ) ) ‘ 𝑛 ) ∈ ℝ )
7 3 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐹 ‘ 𝑘 ) )
8 fvoveq1 ⊢ ( 𝑘 = 𝑛 → ( 𝐹 ‘ ( 𝑘 + 1 ) ) = ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
9 fveq2 ⊢ ( 𝑘 = 𝑛 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑛 ) )
10 8 9 breq12d ⊢ ( 𝑘 = 𝑛 → ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐹 ‘ 𝑘 ) ↔ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ≤ ( 𝐹 ‘ 𝑛 ) ) )
11 10 cbvralvw ⊢ ( ∀ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐹 ‘ 𝑘 ) ↔ ∀ 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ( 𝐹 ‘ ( 𝑛 + 1 ) ) ≤ ( 𝐹 ‘ 𝑛 ) )
12 7 11 sylib ⊢ ( 𝜑 → ∀ 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ( 𝐹 ‘ ( 𝑛 + 1 ) ) ≤ ( 𝐹 ‘ 𝑛 ) )
13 12 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ≤ ( 𝐹 ‘ 𝑛 ) )
14 fveq2 ⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
15 14 eleq1d ⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ↔ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ℝ ) )
16 2 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
17 16 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
18 fzp1elp1 ⊢ ( 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) → ( 𝑛 + 1 ) ∈ ( 𝑀 ... ( ( 𝑁 − 1 ) + 1 ) ) )
19 18 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ( 𝑛 + 1 ) ∈ ( 𝑀 ... ( ( 𝑁 − 1 ) + 1 ) ) )
20 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℤ )
21 1 20 syl ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
22 21 zcnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
23 ax-1cn ⊢ 1 ∈ ℂ
24 npcan ⊢ ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
25 22 23 24 sylancl ⊢ ( 𝜑 → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
26 25 oveq2d ⊢ ( 𝜑 → ( 𝑀 ... ( ( 𝑁 − 1 ) + 1 ) ) = ( 𝑀 ... 𝑁 ) )
27 26 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ( 𝑀 ... ( ( 𝑁 − 1 ) + 1 ) ) = ( 𝑀 ... 𝑁 ) )
28 19 27 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) )
29 15 17 28 rspcdva ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ℝ )
30 9 eleq1d ⊢ ( 𝑘 = 𝑛 → ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ↔ ( 𝐹 ‘ 𝑛 ) ∈ ℝ ) )
31 fzssp1 ⊢ ( 𝑀 ... ( 𝑁 − 1 ) ) ⊆ ( 𝑀 ... ( ( 𝑁 − 1 ) + 1 ) )
32 31 26 sseqtrid ⊢ ( 𝜑 → ( 𝑀 ... ( 𝑁 − 1 ) ) ⊆ ( 𝑀 ... 𝑁 ) )
33 32 sselda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → 𝑛 ∈ ( 𝑀 ... 𝑁 ) )
34 30 17 33 rspcdva ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ( 𝐹 ‘ 𝑛 ) ∈ ℝ )
35 29 34 lenegd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ( ( 𝐹 ‘ ( 𝑛 + 1 ) ) ≤ ( 𝐹 ‘ 𝑛 ) ↔ - ( 𝐹 ‘ 𝑛 ) ≤ - ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
36 13 35 mpbid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → - ( 𝐹 ‘ 𝑛 ) ≤ - ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
37 9 negeqd ⊢ ( 𝑘 = 𝑛 → - ( 𝐹 ‘ 𝑘 ) = - ( 𝐹 ‘ 𝑛 ) )
38 eqid ⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ - ( 𝐹 ‘ 𝑘 ) ) = ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ - ( 𝐹 ‘ 𝑘 ) )
39 negex ⊢ - ( 𝐹 ‘ 𝑛 ) ∈ V
40 37 38 39 fvmpt ⊢ ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ - ( 𝐹 ‘ 𝑘 ) ) ‘ 𝑛 ) = - ( 𝐹 ‘ 𝑛 ) )
41 33 40 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ - ( 𝐹 ‘ 𝑘 ) ) ‘ 𝑛 ) = - ( 𝐹 ‘ 𝑛 ) )
42 14 negeqd ⊢ ( 𝑘 = ( 𝑛 + 1 ) → - ( 𝐹 ‘ 𝑘 ) = - ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
43 negex ⊢ - ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ V
44 42 38 43 fvmpt ⊢ ( ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ - ( 𝐹 ‘ 𝑘 ) ) ‘ ( 𝑛 + 1 ) ) = - ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
45 28 44 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ - ( 𝐹 ‘ 𝑘 ) ) ‘ ( 𝑛 + 1 ) ) = - ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
46 36 41 45 3brtr4d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ - ( 𝐹 ‘ 𝑘 ) ) ‘ 𝑛 ) ≤ ( ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ - ( 𝐹 ‘ 𝑘 ) ) ‘ ( 𝑛 + 1 ) ) )
47 1 6 46 monoord ⊢ ( 𝜑 → ( ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ - ( 𝐹 ‘ 𝑘 ) ) ‘ 𝑀 ) ≤ ( ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ - ( 𝐹 ‘ 𝑘 ) ) ‘ 𝑁 ) )
48 eluzfz1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ( 𝑀 ... 𝑁 ) )
49 1 48 syl ⊢ ( 𝜑 → 𝑀 ∈ ( 𝑀 ... 𝑁 ) )
50 fveq2 ⊢ ( 𝑘 = 𝑀 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑀 ) )
51 50 negeqd ⊢ ( 𝑘 = 𝑀 → - ( 𝐹 ‘ 𝑘 ) = - ( 𝐹 ‘ 𝑀 ) )
52 negex ⊢ - ( 𝐹 ‘ 𝑀 ) ∈ V
53 51 38 52 fvmpt ⊢ ( 𝑀 ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ - ( 𝐹 ‘ 𝑘 ) ) ‘ 𝑀 ) = - ( 𝐹 ‘ 𝑀 ) )
54 49 53 syl ⊢ ( 𝜑 → ( ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ - ( 𝐹 ‘ 𝑘 ) ) ‘ 𝑀 ) = - ( 𝐹 ‘ 𝑀 ) )
55 eluzfz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ( 𝑀 ... 𝑁 ) )
56 1 55 syl ⊢ ( 𝜑 → 𝑁 ∈ ( 𝑀 ... 𝑁 ) )
57 fveq2 ⊢ ( 𝑘 = 𝑁 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑁 ) )
58 57 negeqd ⊢ ( 𝑘 = 𝑁 → - ( 𝐹 ‘ 𝑘 ) = - ( 𝐹 ‘ 𝑁 ) )
59 negex ⊢ - ( 𝐹 ‘ 𝑁 ) ∈ V
60 58 38 59 fvmpt ⊢ ( 𝑁 ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ - ( 𝐹 ‘ 𝑘 ) ) ‘ 𝑁 ) = - ( 𝐹 ‘ 𝑁 ) )
61 56 60 syl ⊢ ( 𝜑 → ( ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ - ( 𝐹 ‘ 𝑘 ) ) ‘ 𝑁 ) = - ( 𝐹 ‘ 𝑁 ) )
62 47 54 61 3brtr3d ⊢ ( 𝜑 → - ( 𝐹 ‘ 𝑀 ) ≤ - ( 𝐹 ‘ 𝑁 ) )
63 57 eleq1d ⊢ ( 𝑘 = 𝑁 → ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ↔ ( 𝐹 ‘ 𝑁 ) ∈ ℝ ) )
64 63 16 56 rspcdva ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑁 ) ∈ ℝ )
65 50 eleq1d ⊢ ( 𝑘 = 𝑀 → ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ↔ ( 𝐹 ‘ 𝑀 ) ∈ ℝ ) )
66 65 16 49 rspcdva ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ∈ ℝ )
67 64 66 lenegd ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑁 ) ≤ ( 𝐹 ‘ 𝑀 ) ↔ - ( 𝐹 ‘ 𝑀 ) ≤ - ( 𝐹 ‘ 𝑁 ) ) )
68 62 67 mpbird ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑁 ) ≤ ( 𝐹 ‘ 𝑀 ) )