Metamath Proof Explorer

Theorem monoord2xrv

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

Ref Expression
Hypotheses monoord2xrv.n ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
monoord2xrv.x ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ* )
monoord2xrv.l ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐹 ‘ 𝑘 ) )
Assertion monoord2xrv ( 𝜑 → ( 𝐹 ‘ 𝑁 ) ≤ ( 𝐹 ‘ 𝑀 ) )

Proof

Step Hyp Ref Expression
1 monoord2xrv.n ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
2 monoord2xrv.x ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ* )
3 monoord2xrv.l ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐹 ‘ 𝑘 ) )
4 2 xnegcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → -𝑒 ( 𝐹 ‘ 𝑘 ) ∈ ℝ* )
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 fzp1elp1 ⊢ ( 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) → ( 𝑛 + 1 ) ∈ ( 𝑀 ... ( ( 𝑁 − 1 ) + 1 ) ) )
15 14 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ( 𝑛 + 1 ) ∈ ( 𝑀 ... ( ( 𝑁 − 1 ) + 1 ) ) )
16 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℤ )
17 1 16 syl ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
18 17 zcnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
19 ax-1cn ⊢ 1 ∈ ℂ
20 npcan ⊢ ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
21 18 19 20 sylancl ⊢ ( 𝜑 → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
22 21 oveq2d ⊢ ( 𝜑 → ( 𝑀 ... ( ( 𝑁 − 1 ) + 1 ) ) = ( 𝑀 ... 𝑁 ) )
23 22 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ( 𝑀 ... ( ( 𝑁 − 1 ) + 1 ) ) = ( 𝑀 ... 𝑁 ) )
24 15 23 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) )
25 2 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ* )
26 25 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ* )
27 fveq2 ⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
28 27 eleq1d ⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ* ↔ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ℝ* ) )
29 28 rspcv ⊢ ( ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → ( ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ* → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ℝ* ) )
30 24 26 29 sylc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ℝ* )
31 fzssp1 ⊢ ( 𝑀 ... ( 𝑁 − 1 ) ) ⊆ ( 𝑀 ... ( ( 𝑁 − 1 ) + 1 ) )
32 31 22 sseqtrid ⊢ ( 𝜑 → ( 𝑀 ... ( 𝑁 − 1 ) ) ⊆ ( 𝑀 ... 𝑁 ) )
33 32 sselda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → 𝑛 ∈ ( 𝑀 ... 𝑁 ) )
34 9 eleq1d ⊢ ( 𝑘 = 𝑛 → ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ* ↔ ( 𝐹 ‘ 𝑛 ) ∈ ℝ* ) )
35 34 rspcv ⊢ ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) → ( ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ* → ( 𝐹 ‘ 𝑛 ) ∈ ℝ* ) )
36 33 26 35 sylc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ( 𝐹 ‘ 𝑛 ) ∈ ℝ* )
37 xleneg ⊢ ( ( ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ℝ* ∧ ( 𝐹 ‘ 𝑛 ) ∈ ℝ* ) → ( ( 𝐹 ‘ ( 𝑛 + 1 ) ) ≤ ( 𝐹 ‘ 𝑛 ) ↔ -𝑒 ( 𝐹 ‘ 𝑛 ) ≤ -𝑒 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
38 30 36 37 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ( ( 𝐹 ‘ ( 𝑛 + 1 ) ) ≤ ( 𝐹 ‘ 𝑛 ) ↔ -𝑒 ( 𝐹 ‘ 𝑛 ) ≤ -𝑒 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
39 13 38 mpbid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → -𝑒 ( 𝐹 ‘ 𝑛 ) ≤ -𝑒 ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
40 9 xnegeqd ⊢ ( 𝑘 = 𝑛 → -𝑒 ( 𝐹 ‘ 𝑘 ) = -𝑒 ( 𝐹 ‘ 𝑛 ) )
41 eqid ⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ -𝑒 ( 𝐹 ‘ 𝑘 ) ) = ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ -𝑒 ( 𝐹 ‘ 𝑘 ) )
42 xnegex ⊢ -𝑒 ( 𝐹 ‘ 𝑛 ) ∈ V
43 40 41 42 fvmpt ⊢ ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ -𝑒 ( 𝐹 ‘ 𝑘 ) ) ‘ 𝑛 ) = -𝑒 ( 𝐹 ‘ 𝑛 ) )
44 33 43 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ -𝑒 ( 𝐹 ‘ 𝑘 ) ) ‘ 𝑛 ) = -𝑒 ( 𝐹 ‘ 𝑛 ) )
45 27 xnegeqd ⊢ ( 𝑘 = ( 𝑛 + 1 ) → -𝑒 ( 𝐹 ‘ 𝑘 ) = -𝑒 ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
46 xnegex ⊢ -𝑒 ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ V
47 45 41 46 fvmpt ⊢ ( ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ -𝑒 ( 𝐹 ‘ 𝑘 ) ) ‘ ( 𝑛 + 1 ) ) = -𝑒 ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
48 24 47 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ -𝑒 ( 𝐹 ‘ 𝑘 ) ) ‘ ( 𝑛 + 1 ) ) = -𝑒 ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
49 39 44 48 3brtr4d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ -𝑒 ( 𝐹 ‘ 𝑘 ) ) ‘ 𝑛 ) ≤ ( ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ -𝑒 ( 𝐹 ‘ 𝑘 ) ) ‘ ( 𝑛 + 1 ) ) )
50 1 6 49 monoordxrv ⊢ ( 𝜑 → ( ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ -𝑒 ( 𝐹 ‘ 𝑘 ) ) ‘ 𝑀 ) ≤ ( ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ -𝑒 ( 𝐹 ‘ 𝑘 ) ) ‘ 𝑁 ) )
51 eluzfz1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ( 𝑀 ... 𝑁 ) )
52 1 51 syl ⊢ ( 𝜑 → 𝑀 ∈ ( 𝑀 ... 𝑁 ) )
53 fveq2 ⊢ ( 𝑘 = 𝑀 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑀 ) )
54 53 xnegeqd ⊢ ( 𝑘 = 𝑀 → -𝑒 ( 𝐹 ‘ 𝑘 ) = -𝑒 ( 𝐹 ‘ 𝑀 ) )
55 xnegex ⊢ -𝑒 ( 𝐹 ‘ 𝑀 ) ∈ V
56 54 41 55 fvmpt ⊢ ( 𝑀 ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ -𝑒 ( 𝐹 ‘ 𝑘 ) ) ‘ 𝑀 ) = -𝑒 ( 𝐹 ‘ 𝑀 ) )
57 52 56 syl ⊢ ( 𝜑 → ( ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ -𝑒 ( 𝐹 ‘ 𝑘 ) ) ‘ 𝑀 ) = -𝑒 ( 𝐹 ‘ 𝑀 ) )
58 eluzfz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ( 𝑀 ... 𝑁 ) )
59 1 58 syl ⊢ ( 𝜑 → 𝑁 ∈ ( 𝑀 ... 𝑁 ) )
60 fveq2 ⊢ ( 𝑘 = 𝑁 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑁 ) )
61 60 xnegeqd ⊢ ( 𝑘 = 𝑁 → -𝑒 ( 𝐹 ‘ 𝑘 ) = -𝑒 ( 𝐹 ‘ 𝑁 ) )
62 xnegex ⊢ -𝑒 ( 𝐹 ‘ 𝑁 ) ∈ V
63 61 41 62 fvmpt ⊢ ( 𝑁 ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ -𝑒 ( 𝐹 ‘ 𝑘 ) ) ‘ 𝑁 ) = -𝑒 ( 𝐹 ‘ 𝑁 ) )
64 59 63 syl ⊢ ( 𝜑 → ( ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ -𝑒 ( 𝐹 ‘ 𝑘 ) ) ‘ 𝑁 ) = -𝑒 ( 𝐹 ‘ 𝑁 ) )
65 50 57 64 3brtr3d ⊢ ( 𝜑 → -𝑒 ( 𝐹 ‘ 𝑀 ) ≤ -𝑒 ( 𝐹 ‘ 𝑁 ) )
66 60 eleq1d ⊢ ( 𝑘 = 𝑁 → ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ* ↔ ( 𝐹 ‘ 𝑁 ) ∈ ℝ* ) )
67 66 rspcv ⊢ ( 𝑁 ∈ ( 𝑀 ... 𝑁 ) → ( ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ* → ( 𝐹 ‘ 𝑁 ) ∈ ℝ* ) )
68 59 25 67 sylc ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑁 ) ∈ ℝ* )
69 53 eleq1d ⊢ ( 𝑘 = 𝑀 → ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ* ↔ ( 𝐹 ‘ 𝑀 ) ∈ ℝ* ) )
70 69 rspcv ⊢ ( 𝑀 ∈ ( 𝑀 ... 𝑁 ) → ( ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ* → ( 𝐹 ‘ 𝑀 ) ∈ ℝ* ) )
71 52 25 70 sylc ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ∈ ℝ* )
72 xleneg ⊢ ( ( ( 𝐹 ‘ 𝑁 ) ∈ ℝ* ∧ ( 𝐹 ‘ 𝑀 ) ∈ ℝ* ) → ( ( 𝐹 ‘ 𝑁 ) ≤ ( 𝐹 ‘ 𝑀 ) ↔ -𝑒 ( 𝐹 ‘ 𝑀 ) ≤ -𝑒 ( 𝐹 ‘ 𝑁 ) ) )
73 68 71 72 syl2anc ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑁 ) ≤ ( 𝐹 ‘ 𝑀 ) ↔ -𝑒 ( 𝐹 ‘ 𝑀 ) ≤ -𝑒 ( 𝐹 ‘ 𝑁 ) ) )
74 65 73 mpbird ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑁 ) ≤ ( 𝐹 ‘ 𝑀 ) )