Theorem monoord2xrv 40129

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

Hypotheses

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

Assertion

Ref	Expression
monoord2xrv	⊢ (𝜑 → (𝐹‘𝑁) ≤ (𝐹‘𝑀))

Distinct variable groups:   𝑘,𝐹   𝑘,𝑀   𝑘,𝑁   𝜑,𝑘

Proof of Theorem monoord2xrv

Dummy variable 𝑛 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		monoord2xrv.n	. . . 4 ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))
2		monoord2xrv.x	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ*)
3	2	xnegcld 12244	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → -𝑒(𝐹‘𝑘) ∈ ℝ*)
4		eqid 2724	. . . . . 6 ⊢ (𝑘 ∈ (𝑀...𝑁) ↦ -𝑒(𝐹‘𝑘)) = (𝑘 ∈ (𝑀...𝑁) ↦ -𝑒(𝐹‘𝑘))
5	3, 4	fmptd 6500	. . . . 5 ⊢ (𝜑 → (𝑘 ∈ (𝑀...𝑁) ↦ -𝑒(𝐹‘𝑘)):(𝑀...𝑁)⟶ℝ*)
6	5	ffvelrnda 6474	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...𝑁)) → ((𝑘 ∈ (𝑀...𝑁) ↦ -𝑒(𝐹‘𝑘))‘𝑛) ∈ ℝ*)
7		monoord2xrv.l	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘))
8	7	ralrimiva 3068	. . . . . . . 8 ⊢ (𝜑 → ∀𝑘 ∈ (𝑀...(𝑁 − 1))(𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘))
9		oveq1 6772	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑛 → (𝑘 + 1) = (𝑛 + 1))
10	9	fveq2d 6308	. . . . . . . . . 10 ⊢ (𝑘 = 𝑛 → (𝐹‘(𝑘 + 1)) = (𝐹‘(𝑛 + 1)))
11		fveq2 6304	. . . . . . . . . 10 ⊢ (𝑘 = 𝑛 → (𝐹‘𝑘) = (𝐹‘𝑛))
12	10, 11	breq12d 4773	. . . . . . . . 9 ⊢ (𝑘 = 𝑛 → ((𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘) ↔ (𝐹‘(𝑛 + 1)) ≤ (𝐹‘𝑛)))
13	12	cbvralv 3274	. . . . . . . 8 ⊢ (∀𝑘 ∈ (𝑀...(𝑁 − 1))(𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘) ↔ ∀𝑛 ∈ (𝑀...(𝑁 − 1))(𝐹‘(𝑛 + 1)) ≤ (𝐹‘𝑛))
14	8, 13	sylib 208	. . . . . . 7 ⊢ (𝜑 → ∀𝑛 ∈ (𝑀...(𝑁 − 1))(𝐹‘(𝑛 + 1)) ≤ (𝐹‘𝑛))
15	14	r19.21bi 3034	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘(𝑛 + 1)) ≤ (𝐹‘𝑛))
16		fzp1elp1 12508	. . . . . . . . . 10 ⊢ (𝑛 ∈ (𝑀...(𝑁 − 1)) → (𝑛 + 1) ∈ (𝑀...((𝑁 − 1) + 1)))
17	16	adantl 473	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → (𝑛 + 1) ∈ (𝑀...((𝑁 − 1) + 1)))
18		eluzelz 11810	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℤ)
19	1, 18	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℤ)
20	19	zcnd 11596	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℂ)
21		ax-1cn 10107	. . . . . . . . . . . 12 ⊢ 1 ∈ ℂ
22		npcan 10403	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 − 1) + 1) = 𝑁)
23	20, 21, 22	sylancl 697	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
24	23	oveq2d 6781	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀...((𝑁 − 1) + 1)) = (𝑀...𝑁))
25	24	adantr 472	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → (𝑀...((𝑁 − 1) + 1)) = (𝑀...𝑁))
26	17, 25	eleqtrd 2805	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → (𝑛 + 1) ∈ (𝑀...𝑁))
27	2	ralrimiva 3068	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑘 ∈ (𝑀...𝑁)(𝐹‘𝑘) ∈ ℝ*)
28	27	adantr 472	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → ∀𝑘 ∈ (𝑀...𝑁)(𝐹‘𝑘) ∈ ℝ*)
29		fveq2 6304	. . . . . . . . . 10 ⊢ (𝑘 = (𝑛 + 1) → (𝐹‘𝑘) = (𝐹‘(𝑛 + 1)))
30	29	eleq1d 2788	. . . . . . . . 9 ⊢ (𝑘 = (𝑛 + 1) → ((𝐹‘𝑘) ∈ ℝ* ↔ (𝐹‘(𝑛 + 1)) ∈ ℝ*))
31	30	rspcv 3409	. . . . . . . 8 ⊢ ((𝑛 + 1) ∈ (𝑀...𝑁) → (∀𝑘 ∈ (𝑀...𝑁)(𝐹‘𝑘) ∈ ℝ* → (𝐹‘(𝑛 + 1)) ∈ ℝ*))
32	26, 28, 31	sylc 65	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘(𝑛 + 1)) ∈ ℝ*)
33		fzssp1 12498	. . . . . . . . . 10 ⊢ (𝑀...(𝑁 − 1)) ⊆ (𝑀...((𝑁 − 1) + 1))
34	33, 24	syl5sseq 3759	. . . . . . . . 9 ⊢ (𝜑 → (𝑀...(𝑁 − 1)) ⊆ (𝑀...𝑁))
35	34	sselda 3709	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → 𝑛 ∈ (𝑀...𝑁))
36	11	eleq1d 2788	. . . . . . . . 9 ⊢ (𝑘 = 𝑛 → ((𝐹‘𝑘) ∈ ℝ* ↔ (𝐹‘𝑛) ∈ ℝ*))
37	36	rspcv 3409	. . . . . . . 8 ⊢ (𝑛 ∈ (𝑀...𝑁) → (∀𝑘 ∈ (𝑀...𝑁)(𝐹‘𝑘) ∈ ℝ* → (𝐹‘𝑛) ∈ ℝ*))
38	35, 28, 37	sylc 65	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘𝑛) ∈ ℝ*)
39		xleneg 12163	. . . . . . 7 ⊢ (((𝐹‘(𝑛 + 1)) ∈ ℝ* ∧ (𝐹‘𝑛) ∈ ℝ*) → ((𝐹‘(𝑛 + 1)) ≤ (𝐹‘𝑛) ↔ -𝑒(𝐹‘𝑛) ≤ -𝑒(𝐹‘(𝑛 + 1))))
40	32, 38, 39	syl2anc 696	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → ((𝐹‘(𝑛 + 1)) ≤ (𝐹‘𝑛) ↔ -𝑒(𝐹‘𝑛) ≤ -𝑒(𝐹‘(𝑛 + 1))))
41	15, 40	mpbid 222	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → -𝑒(𝐹‘𝑛) ≤ -𝑒(𝐹‘(𝑛 + 1)))
42	11	xnegeqd 40079	. . . . . . 7 ⊢ (𝑘 = 𝑛 → -𝑒(𝐹‘𝑘) = -𝑒(𝐹‘𝑛))
43		xnegex 12153	. . . . . . 7 ⊢ -𝑒(𝐹‘𝑛) ∈ V
44	42, 4, 43	fvmpt 6396	. . . . . 6 ⊢ (𝑛 ∈ (𝑀...𝑁) → ((𝑘 ∈ (𝑀...𝑁) ↦ -𝑒(𝐹‘𝑘))‘𝑛) = -𝑒(𝐹‘𝑛))
45	35, 44	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → ((𝑘 ∈ (𝑀...𝑁) ↦ -𝑒(𝐹‘𝑘))‘𝑛) = -𝑒(𝐹‘𝑛))
46	29	xnegeqd 40079	. . . . . . 7 ⊢ (𝑘 = (𝑛 + 1) → -𝑒(𝐹‘𝑘) = -𝑒(𝐹‘(𝑛 + 1)))
47		xnegex 12153	. . . . . . 7 ⊢ -𝑒(𝐹‘(𝑛 + 1)) ∈ V
48	46, 4, 47	fvmpt 6396	. . . . . 6 ⊢ ((𝑛 + 1) ∈ (𝑀...𝑁) → ((𝑘 ∈ (𝑀...𝑁) ↦ -𝑒(𝐹‘𝑘))‘(𝑛 + 1)) = -𝑒(𝐹‘(𝑛 + 1)))
49	26, 48	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → ((𝑘 ∈ (𝑀...𝑁) ↦ -𝑒(𝐹‘𝑘))‘(𝑛 + 1)) = -𝑒(𝐹‘(𝑛 + 1)))
50	41, 45, 49	3brtr4d 4792	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → ((𝑘 ∈ (𝑀...𝑁) ↦ -𝑒(𝐹‘𝑘))‘𝑛) ≤ ((𝑘 ∈ (𝑀...𝑁) ↦ -𝑒(𝐹‘𝑘))‘(𝑛 + 1)))
51	1, 6, 50	monoordxrv 40127	. . 3 ⊢ (𝜑 → ((𝑘 ∈ (𝑀...𝑁) ↦ -𝑒(𝐹‘𝑘))‘𝑀) ≤ ((𝑘 ∈ (𝑀...𝑁) ↦ -𝑒(𝐹‘𝑘))‘𝑁))
52		eluzfz1 12462	. . . . 5 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ (𝑀...𝑁))
53	1, 52	syl 17	. . . 4 ⊢ (𝜑 → 𝑀 ∈ (𝑀...𝑁))
54		fveq2 6304	. . . . . 6 ⊢ (𝑘 = 𝑀 → (𝐹‘𝑘) = (𝐹‘𝑀))
55	54	xnegeqd 40079	. . . . 5 ⊢ (𝑘 = 𝑀 → -𝑒(𝐹‘𝑘) = -𝑒(𝐹‘𝑀))
56		xnegex 12153	. . . . 5 ⊢ -𝑒(𝐹‘𝑀) ∈ V
57	55, 4, 56	fvmpt 6396	. . . 4 ⊢ (𝑀 ∈ (𝑀...𝑁) → ((𝑘 ∈ (𝑀...𝑁) ↦ -𝑒(𝐹‘𝑘))‘𝑀) = -𝑒(𝐹‘𝑀))
58	53, 57	syl 17	. . 3 ⊢ (𝜑 → ((𝑘 ∈ (𝑀...𝑁) ↦ -𝑒(𝐹‘𝑘))‘𝑀) = -𝑒(𝐹‘𝑀))
59		eluzfz2 12463	. . . . 5 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ (𝑀...𝑁))
60	1, 59	syl 17	. . . 4 ⊢ (𝜑 → 𝑁 ∈ (𝑀...𝑁))
61		fveq2 6304	. . . . . 6 ⊢ (𝑘 = 𝑁 → (𝐹‘𝑘) = (𝐹‘𝑁))
62	61	xnegeqd 40079	. . . . 5 ⊢ (𝑘 = 𝑁 → -𝑒(𝐹‘𝑘) = -𝑒(𝐹‘𝑁))
63		xnegex 12153	. . . . 5 ⊢ -𝑒(𝐹‘𝑁) ∈ V
64	62, 4, 63	fvmpt 6396	. . . 4 ⊢ (𝑁 ∈ (𝑀...𝑁) → ((𝑘 ∈ (𝑀...𝑁) ↦ -𝑒(𝐹‘𝑘))‘𝑁) = -𝑒(𝐹‘𝑁))
65	60, 64	syl 17	. . 3 ⊢ (𝜑 → ((𝑘 ∈ (𝑀...𝑁) ↦ -𝑒(𝐹‘𝑘))‘𝑁) = -𝑒(𝐹‘𝑁))
66	51, 58, 65	3brtr3d 4791	. 2 ⊢ (𝜑 → -𝑒(𝐹‘𝑀) ≤ -𝑒(𝐹‘𝑁))
67	61	eleq1d 2788	. . . . 5 ⊢ (𝑘 = 𝑁 → ((𝐹‘𝑘) ∈ ℝ* ↔ (𝐹‘𝑁) ∈ ℝ*))
68	67	rspcv 3409	. . . 4 ⊢ (𝑁 ∈ (𝑀...𝑁) → (∀𝑘 ∈ (𝑀...𝑁)(𝐹‘𝑘) ∈ ℝ* → (𝐹‘𝑁) ∈ ℝ*))
69	60, 27, 68	sylc 65	. . 3 ⊢ (𝜑 → (𝐹‘𝑁) ∈ ℝ*)
70	54	eleq1d 2788	. . . . 5 ⊢ (𝑘 = 𝑀 → ((𝐹‘𝑘) ∈ ℝ* ↔ (𝐹‘𝑀) ∈ ℝ*))
71	70	rspcv 3409	. . . 4 ⊢ (𝑀 ∈ (𝑀...𝑁) → (∀𝑘 ∈ (𝑀...𝑁)(𝐹‘𝑘) ∈ ℝ* → (𝐹‘𝑀) ∈ ℝ*))
72	53, 27, 71	sylc 65	. . 3 ⊢ (𝜑 → (𝐹‘𝑀) ∈ ℝ*)
73		xleneg 12163	. . 3 ⊢ (((𝐹‘𝑁) ∈ ℝ* ∧ (𝐹‘𝑀) ∈ ℝ*) → ((𝐹‘𝑁) ≤ (𝐹‘𝑀) ↔ -𝑒(𝐹‘𝑀) ≤ -𝑒(𝐹‘𝑁)))
74	69, 72, 73	syl2anc 696	. 2 ⊢ (𝜑 → ((𝐹‘𝑁) ≤ (𝐹‘𝑀) ↔ -𝑒(𝐹‘𝑀) ≤ -𝑒(𝐹‘𝑁)))
75	66, 74	mpbird 247	1 ⊢ (𝜑 → (𝐹‘𝑁) ≤ (𝐹‘𝑀))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1596   ∈ wcel 2103  ∀wral 3014   class class class wbr 4760   ↦ cmpt 4837  ‘cfv 6001  (class class class)co 6765  ℂcc 10047  1c1 10050   + caddc 10052  ℝ^*cxr 10186   ≤ cle 10188   − cmin 10379  ℤcz 11490  ℤ_≥cuz 11800  -_𝑒cxne 12057  ...cfz 12440

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-8 2105  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-sep 4889  ax-nul 4897  ax-pow 4948  ax-pr 5011  ax-un 7066  ax-cnex 10105  ax-resscn 10106  ax-1cn 10107  ax-icn 10108  ax-addcl 10109  ax-addrcl 10110  ax-mulcl 10111  ax-mulrcl 10112  ax-mulcom 10113  ax-addass 10114  ax-mulass 10115  ax-distr 10116  ax-i2m1 10117  ax-1ne0 10118  ax-1rid 10119  ax-rnegex 10120  ax-rrecex 10121  ax-cnre 10122  ax-pre-lttri 10123  ax-pre-lttrn 10124  ax-pre-ltadd 10125  ax-pre-mulgt0 10126

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-eu 2575  df-mo 2576  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ne 2897  df-nel 3000  df-ral 3019  df-rex 3020  df-reu 3021  df-rab 3023  df-v 3306  df-sbc 3542  df-csb 3640  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-pss 3696  df-nul 4024  df-if 4195  df-pw 4268  df-sn 4286  df-pr 4288  df-tp 4290  df-op 4292  df-uni 4545  df-iun 4630  df-br 4761  df-opab 4821  df-mpt 4838  df-tr 4861  df-id 5128  df-eprel 5133  df-po 5139  df-so 5140  df-fr 5177  df-we 5179  df-xp 5224  df-rel 5225  df-cnv 5226  df-co 5227  df-dm 5228  df-rn 5229  df-res 5230  df-ima 5231  df-pred 5793  df-ord 5839  df-on 5840  df-lim 5841  df-suc 5842  df-iota 5964  df-fun 6003  df-fn 6004  df-f 6005  df-f1 6006  df-fo 6007  df-f1o 6008  df-fv 6009  df-riota 6726  df-ov 6768  df-oprab 6769  df-mpt2 6770  df-om 7183  df-1st 7285  df-2nd 7286  df-wrecs 7527  df-recs 7588  df-rdg 7626  df-er 7862  df-en 8073  df-dom 8074  df-sdom 8075  df-pnf 10189  df-mnf 10190  df-xr 10191  df-ltxr 10192  df-le 10193  df-sub 10381  df-neg 10382  df-nn 11134  df-n0 11406  df-z 11491  df-uz 11801  df-xneg 12060  df-fz 12441

This theorem is referenced by:  monoord2xr  40130