# 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 ${⊢}{\phi }\to {N}\in {ℤ}_{\ge {M}}$
monoord.2 ${⊢}\left({\phi }\wedge {k}\in \left({M}\dots {N}\right)\right)\to {F}\left({k}\right)\in ℝ$
monoord.3 ${⊢}\left({\phi }\wedge {k}\in \left({M}\dots {N}-1\right)\right)\to {F}\left({k}\right)\le {F}\left({k}+1\right)$
Assertion monoord ${⊢}{\phi }\to {F}\left({M}\right)\le {F}\left({N}\right)$

### Proof

Step Hyp Ref Expression
1 monoord.1 ${⊢}{\phi }\to {N}\in {ℤ}_{\ge {M}}$
2 monoord.2 ${⊢}\left({\phi }\wedge {k}\in \left({M}\dots {N}\right)\right)\to {F}\left({k}\right)\in ℝ$
3 monoord.3 ${⊢}\left({\phi }\wedge {k}\in \left({M}\dots {N}-1\right)\right)\to {F}\left({k}\right)\le {F}\left({k}+1\right)$
4 eluzfz2 ${⊢}{N}\in {ℤ}_{\ge {M}}\to {N}\in \left({M}\dots {N}\right)$
5 1 4 syl ${⊢}{\phi }\to {N}\in \left({M}\dots {N}\right)$
6 eleq1 ${⊢}{x}={M}\to \left({x}\in \left({M}\dots {N}\right)↔{M}\in \left({M}\dots {N}\right)\right)$
7 fveq2 ${⊢}{x}={M}\to {F}\left({x}\right)={F}\left({M}\right)$
8 7 breq2d ${⊢}{x}={M}\to \left({F}\left({M}\right)\le {F}\left({x}\right)↔{F}\left({M}\right)\le {F}\left({M}\right)\right)$
9 6 8 imbi12d ${⊢}{x}={M}\to \left(\left({x}\in \left({M}\dots {N}\right)\to {F}\left({M}\right)\le {F}\left({x}\right)\right)↔\left({M}\in \left({M}\dots {N}\right)\to {F}\left({M}\right)\le {F}\left({M}\right)\right)\right)$
10 9 imbi2d ${⊢}{x}={M}\to \left(\left({\phi }\to \left({x}\in \left({M}\dots {N}\right)\to {F}\left({M}\right)\le {F}\left({x}\right)\right)\right)↔\left({\phi }\to \left({M}\in \left({M}\dots {N}\right)\to {F}\left({M}\right)\le {F}\left({M}\right)\right)\right)\right)$
11 eleq1 ${⊢}{x}={n}\to \left({x}\in \left({M}\dots {N}\right)↔{n}\in \left({M}\dots {N}\right)\right)$
12 fveq2 ${⊢}{x}={n}\to {F}\left({x}\right)={F}\left({n}\right)$
13 12 breq2d ${⊢}{x}={n}\to \left({F}\left({M}\right)\le {F}\left({x}\right)↔{F}\left({M}\right)\le {F}\left({n}\right)\right)$
14 11 13 imbi12d ${⊢}{x}={n}\to \left(\left({x}\in \left({M}\dots {N}\right)\to {F}\left({M}\right)\le {F}\left({x}\right)\right)↔\left({n}\in \left({M}\dots {N}\right)\to {F}\left({M}\right)\le {F}\left({n}\right)\right)\right)$
15 14 imbi2d ${⊢}{x}={n}\to \left(\left({\phi }\to \left({x}\in \left({M}\dots {N}\right)\to {F}\left({M}\right)\le {F}\left({x}\right)\right)\right)↔\left({\phi }\to \left({n}\in \left({M}\dots {N}\right)\to {F}\left({M}\right)\le {F}\left({n}\right)\right)\right)\right)$
16 eleq1 ${⊢}{x}={n}+1\to \left({x}\in \left({M}\dots {N}\right)↔{n}+1\in \left({M}\dots {N}\right)\right)$
17 fveq2 ${⊢}{x}={n}+1\to {F}\left({x}\right)={F}\left({n}+1\right)$
18 17 breq2d ${⊢}{x}={n}+1\to \left({F}\left({M}\right)\le {F}\left({x}\right)↔{F}\left({M}\right)\le {F}\left({n}+1\right)\right)$
19 16 18 imbi12d ${⊢}{x}={n}+1\to \left(\left({x}\in \left({M}\dots {N}\right)\to {F}\left({M}\right)\le {F}\left({x}\right)\right)↔\left({n}+1\in \left({M}\dots {N}\right)\to {F}\left({M}\right)\le {F}\left({n}+1\right)\right)\right)$
20 19 imbi2d ${⊢}{x}={n}+1\to \left(\left({\phi }\to \left({x}\in \left({M}\dots {N}\right)\to {F}\left({M}\right)\le {F}\left({x}\right)\right)\right)↔\left({\phi }\to \left({n}+1\in \left({M}\dots {N}\right)\to {F}\left({M}\right)\le {F}\left({n}+1\right)\right)\right)\right)$
21 eleq1 ${⊢}{x}={N}\to \left({x}\in \left({M}\dots {N}\right)↔{N}\in \left({M}\dots {N}\right)\right)$
22 fveq2 ${⊢}{x}={N}\to {F}\left({x}\right)={F}\left({N}\right)$
23 22 breq2d ${⊢}{x}={N}\to \left({F}\left({M}\right)\le {F}\left({x}\right)↔{F}\left({M}\right)\le {F}\left({N}\right)\right)$
24 21 23 imbi12d ${⊢}{x}={N}\to \left(\left({x}\in \left({M}\dots {N}\right)\to {F}\left({M}\right)\le {F}\left({x}\right)\right)↔\left({N}\in \left({M}\dots {N}\right)\to {F}\left({M}\right)\le {F}\left({N}\right)\right)\right)$
25 24 imbi2d ${⊢}{x}={N}\to \left(\left({\phi }\to \left({x}\in \left({M}\dots {N}\right)\to {F}\left({M}\right)\le {F}\left({x}\right)\right)\right)↔\left({\phi }\to \left({N}\in \left({M}\dots {N}\right)\to {F}\left({M}\right)\le {F}\left({N}\right)\right)\right)\right)$
26 fveq2 ${⊢}{k}={M}\to {F}\left({k}\right)={F}\left({M}\right)$
27 26 eleq1d ${⊢}{k}={M}\to \left({F}\left({k}\right)\in ℝ↔{F}\left({M}\right)\in ℝ\right)$
28 2 ralrimiva ${⊢}{\phi }\to \forall {k}\in \left({M}\dots {N}\right)\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in ℝ$
29 eluzfz1 ${⊢}{N}\in {ℤ}_{\ge {M}}\to {M}\in \left({M}\dots {N}\right)$
30 1 29 syl ${⊢}{\phi }\to {M}\in \left({M}\dots {N}\right)$
31 27 28 30 rspcdva ${⊢}{\phi }\to {F}\left({M}\right)\in ℝ$
32 31 leidd ${⊢}{\phi }\to {F}\left({M}\right)\le {F}\left({M}\right)$
33 32 a1d ${⊢}{\phi }\to \left({M}\in \left({M}\dots {N}\right)\to {F}\left({M}\right)\le {F}\left({M}\right)\right)$
34 peano2fzr ${⊢}\left({n}\in {ℤ}_{\ge {M}}\wedge {n}+1\in \left({M}\dots {N}\right)\right)\to {n}\in \left({M}\dots {N}\right)$
35 34 adantl ${⊢}\left({\phi }\wedge \left({n}\in {ℤ}_{\ge {M}}\wedge {n}+1\in \left({M}\dots {N}\right)\right)\right)\to {n}\in \left({M}\dots {N}\right)$
36 35 expr ${⊢}\left({\phi }\wedge {n}\in {ℤ}_{\ge {M}}\right)\to \left({n}+1\in \left({M}\dots {N}\right)\to {n}\in \left({M}\dots {N}\right)\right)$
37 36 imim1d ${⊢}\left({\phi }\wedge {n}\in {ℤ}_{\ge {M}}\right)\to \left(\left({n}\in \left({M}\dots {N}\right)\to {F}\left({M}\right)\le {F}\left({n}\right)\right)\to \left({n}+1\in \left({M}\dots {N}\right)\to {F}\left({M}\right)\le {F}\left({n}\right)\right)\right)$
38 fveq2 ${⊢}{k}={n}\to {F}\left({k}\right)={F}\left({n}\right)$
39 fvoveq1 ${⊢}{k}={n}\to {F}\left({k}+1\right)={F}\left({n}+1\right)$
40 38 39 breq12d ${⊢}{k}={n}\to \left({F}\left({k}\right)\le {F}\left({k}+1\right)↔{F}\left({n}\right)\le {F}\left({n}+1\right)\right)$
41 3 ralrimiva ${⊢}{\phi }\to \forall {k}\in \left({M}\dots {N}-1\right)\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\le {F}\left({k}+1\right)$
42 41 adantr ${⊢}\left({\phi }\wedge \left({n}\in {ℤ}_{\ge {M}}\wedge {n}+1\in \left({M}\dots {N}\right)\right)\right)\to \forall {k}\in \left({M}\dots {N}-1\right)\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\le {F}\left({k}+1\right)$
43 simprl ${⊢}\left({\phi }\wedge \left({n}\in {ℤ}_{\ge {M}}\wedge {n}+1\in \left({M}\dots {N}\right)\right)\right)\to {n}\in {ℤ}_{\ge {M}}$
44 eluzelz ${⊢}{n}\in {ℤ}_{\ge {M}}\to {n}\in ℤ$
45 43 44 syl ${⊢}\left({\phi }\wedge \left({n}\in {ℤ}_{\ge {M}}\wedge {n}+1\in \left({M}\dots {N}\right)\right)\right)\to {n}\in ℤ$
46 simprr ${⊢}\left({\phi }\wedge \left({n}\in {ℤ}_{\ge {M}}\wedge {n}+1\in \left({M}\dots {N}\right)\right)\right)\to {n}+1\in \left({M}\dots {N}\right)$
47 elfzuz3 ${⊢}{n}+1\in \left({M}\dots {N}\right)\to {N}\in {ℤ}_{\ge \left({n}+1\right)}$
48 46 47 syl ${⊢}\left({\phi }\wedge \left({n}\in {ℤ}_{\ge {M}}\wedge {n}+1\in \left({M}\dots {N}\right)\right)\right)\to {N}\in {ℤ}_{\ge \left({n}+1\right)}$
49 eluzp1m1 ${⊢}\left({n}\in ℤ\wedge {N}\in {ℤ}_{\ge \left({n}+1\right)}\right)\to {N}-1\in {ℤ}_{\ge {n}}$
50 45 48 49 syl2anc ${⊢}\left({\phi }\wedge \left({n}\in {ℤ}_{\ge {M}}\wedge {n}+1\in \left({M}\dots {N}\right)\right)\right)\to {N}-1\in {ℤ}_{\ge {n}}$
51 elfzuzb ${⊢}{n}\in \left({M}\dots {N}-1\right)↔\left({n}\in {ℤ}_{\ge {M}}\wedge {N}-1\in {ℤ}_{\ge {n}}\right)$
52 43 50 51 sylanbrc ${⊢}\left({\phi }\wedge \left({n}\in {ℤ}_{\ge {M}}\wedge {n}+1\in \left({M}\dots {N}\right)\right)\right)\to {n}\in \left({M}\dots {N}-1\right)$
53 40 42 52 rspcdva ${⊢}\left({\phi }\wedge \left({n}\in {ℤ}_{\ge {M}}\wedge {n}+1\in \left({M}\dots {N}\right)\right)\right)\to {F}\left({n}\right)\le {F}\left({n}+1\right)$
54 31 adantr ${⊢}\left({\phi }\wedge \left({n}\in {ℤ}_{\ge {M}}\wedge {n}+1\in \left({M}\dots {N}\right)\right)\right)\to {F}\left({M}\right)\in ℝ$
55 38 eleq1d ${⊢}{k}={n}\to \left({F}\left({k}\right)\in ℝ↔{F}\left({n}\right)\in ℝ\right)$
56 28 adantr ${⊢}\left({\phi }\wedge \left({n}\in {ℤ}_{\ge {M}}\wedge {n}+1\in \left({M}\dots {N}\right)\right)\right)\to \forall {k}\in \left({M}\dots {N}\right)\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\in ℝ$
57 55 56 35 rspcdva ${⊢}\left({\phi }\wedge \left({n}\in {ℤ}_{\ge {M}}\wedge {n}+1\in \left({M}\dots {N}\right)\right)\right)\to {F}\left({n}\right)\in ℝ$
58 fveq2 ${⊢}{k}={n}+1\to {F}\left({k}\right)={F}\left({n}+1\right)$
59 58 eleq1d ${⊢}{k}={n}+1\to \left({F}\left({k}\right)\in ℝ↔{F}\left({n}+1\right)\in ℝ\right)$
60 59 56 46 rspcdva ${⊢}\left({\phi }\wedge \left({n}\in {ℤ}_{\ge {M}}\wedge {n}+1\in \left({M}\dots {N}\right)\right)\right)\to {F}\left({n}+1\right)\in ℝ$
61 letr ${⊢}\left({F}\left({M}\right)\in ℝ\wedge {F}\left({n}\right)\in ℝ\wedge {F}\left({n}+1\right)\in ℝ\right)\to \left(\left({F}\left({M}\right)\le {F}\left({n}\right)\wedge {F}\left({n}\right)\le {F}\left({n}+1\right)\right)\to {F}\left({M}\right)\le {F}\left({n}+1\right)\right)$
62 54 57 60 61 syl3anc ${⊢}\left({\phi }\wedge \left({n}\in {ℤ}_{\ge {M}}\wedge {n}+1\in \left({M}\dots {N}\right)\right)\right)\to \left(\left({F}\left({M}\right)\le {F}\left({n}\right)\wedge {F}\left({n}\right)\le {F}\left({n}+1\right)\right)\to {F}\left({M}\right)\le {F}\left({n}+1\right)\right)$
63 53 62 mpan2d ${⊢}\left({\phi }\wedge \left({n}\in {ℤ}_{\ge {M}}\wedge {n}+1\in \left({M}\dots {N}\right)\right)\right)\to \left({F}\left({M}\right)\le {F}\left({n}\right)\to {F}\left({M}\right)\le {F}\left({n}+1\right)\right)$
64 37 63 animpimp2impd ${⊢}{n}\in {ℤ}_{\ge {M}}\to \left(\left({\phi }\to \left({n}\in \left({M}\dots {N}\right)\to {F}\left({M}\right)\le {F}\left({n}\right)\right)\right)\to \left({\phi }\to \left({n}+1\in \left({M}\dots {N}\right)\to {F}\left({M}\right)\le {F}\left({n}+1\right)\right)\right)\right)$
65 10 15 20 25 33 64 uzind4i ${⊢}{N}\in {ℤ}_{\ge {M}}\to \left({\phi }\to \left({N}\in \left({M}\dots {N}\right)\to {F}\left({M}\right)\le {F}\left({N}\right)\right)\right)$
66 1 65 mpcom ${⊢}{\phi }\to \left({N}\in \left({M}\dots {N}\right)\to {F}\left({M}\right)\le {F}\left({N}\right)\right)$
67 5 66 mpd ${⊢}{\phi }\to {F}\left({M}\right)\le {F}\left({N}\right)$