Metamath Proof Explorer


Theorem monoordxr

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

Ref Expression
Hypotheses monoordxr.p k φ
monoordxr.k _ k F
monoordxr.n φ N M
monoordxr.x φ k M N F k *
monoordxr.l φ k M N 1 F k F k + 1
Assertion monoordxr φ F M F N

Proof

Step Hyp Ref Expression
1 monoordxr.p k φ
2 monoordxr.k _ k F
3 monoordxr.n φ N M
4 monoordxr.x φ k M N F k *
5 monoordxr.l φ k M N 1 F k F k + 1
6 nfv k j M N
7 1 6 nfan k φ j M N
8 nfcv _ k j
9 2 8 nffv _ k F j
10 nfcv _ k *
11 9 10 nfel k F j *
12 7 11 nfim k φ j M N F j *
13 eleq1w k = j k M N j M N
14 13 anbi2d k = j φ k M N φ j M N
15 fveq2 k = j F k = F j
16 15 eleq1d k = j F k * F j *
17 14 16 imbi12d k = j φ k M N F k * φ j M N F j *
18 12 17 4 chvarfv φ j M N F j *
19 nfv k j M N 1
20 1 19 nfan k φ j M N 1
21 nfcv _ k
22 nfcv _ k j + 1
23 2 22 nffv _ k F j + 1
24 9 21 23 nfbr k F j F j + 1
25 20 24 nfim k φ j M N 1 F j F j + 1
26 eleq1w k = j k M N 1 j M N 1
27 26 anbi2d k = j φ k M N 1 φ j M N 1
28 fvoveq1 k = j F k + 1 = F j + 1
29 15 28 breq12d k = j F k F k + 1 F j F j + 1
30 27 29 imbi12d k = j φ k M N 1 F k F k + 1 φ j M N 1 F j F j + 1
31 25 30 5 chvarfv φ j M N 1 F j F j + 1
32 3 18 31 monoordxrv φ F M F N