monoords

Description: Ordering relation for a strictly monotonic sequence, increasing case. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	monoords.fk	$⊢ (φ \land k \in (M \dots N)) \to F (k) \in ℝ$
	monoords.flt	$⊢ (φ \land k \in (M ..^N)) \to F (k) < F (k + 1)$
	monoords.i	$⊢ φ \to I \in (M \dots N)$
	monoords.j	$⊢ φ \to J \in (M \dots N)$
	monoords.iltj	$⊢ φ \to I < J$
Assertion	monoords	$⊢ φ \to F (I) < F (J)$

Proof

Step	Hyp	Ref	Expression
1		monoords.fk	$⊢ (φ \land k \in (M \dots N)) \to F (k) \in ℝ$
2		monoords.flt	$⊢ (φ \land k \in (M ..^N)) \to F (k) < F (k + 1)$
3		monoords.i	$⊢ φ \to I \in (M \dots N)$
4		monoords.j	$⊢ φ \to J \in (M \dots N)$
5		monoords.iltj	$⊢ φ \to I < J$
6	3	ancli	$⊢ φ \to (φ \land I \in (M \dots N))$
7		eleq1	$⊢ k = I \to (k \in (M \dots N) \leftrightarrow I \in (M \dots N))$
8	7	anbi2d	$⊢ k = I \to ((φ \land k \in (M \dots N)) \leftrightarrow (φ \land I \in (M \dots N)))$
9		fveq2	$⊢ k = I \to F (k) = F (I)$
10	9	eleq1d	$⊢ k = I \to (F (k) \in ℝ \leftrightarrow F (I) \in ℝ)$
11	8 10	imbi12d	$⊢ k = I \to (((φ \land k \in (M \dots N)) \to F (k) \in ℝ) \leftrightarrow ((φ \land I \in (M \dots N)) \to F (I) \in ℝ))$
12	11 1	vtoclg	$⊢ I \in (M \dots N) \to ((φ \land I \in (M \dots N)) \to F (I) \in ℝ)$
13	3 6 12	sylc	$⊢ φ \to F (I) \in ℝ$
14		elfzel1	$⊢ I \in (M \dots N) \to M \in ℤ$
15	3 14	syl	$⊢ φ \to M \in ℤ$
16		elfzelz	$⊢ I \in (M \dots N) \to I \in ℤ$
17	3 16	syl	$⊢ φ \to I \in ℤ$
18		elfzle1	$⊢ I \in (M \dots N) \to M \leq I$
19	3 18	syl	$⊢ φ \to M \leq I$
20		eluz2	$⊢ I \in ℤ_{\geq M} \leftrightarrow (M \in ℤ \land I \in ℤ \land M \leq I)$
21	15 17 19 20	syl3anbrc	$⊢ φ \to I \in ℤ_{\geq M}$
22		elfzuz2	$⊢ I \in (M \dots N) \to N \in ℤ_{\geq M}$
23	3 22	syl	$⊢ φ \to N \in ℤ_{\geq M}$
24		eluzelz	$⊢ N \in ℤ_{\geq M} \to N \in ℤ$
25	23 24	syl	$⊢ φ \to N \in ℤ$
26	17	zred	$⊢ φ \to I \in ℝ$
27		elfzelz	$⊢ J \in (M \dots N) \to J \in ℤ$
28	4 27	syl	$⊢ φ \to J \in ℤ$
29	28	zred	$⊢ φ \to J \in ℝ$
30	25	zred	$⊢ φ \to N \in ℝ$
31		elfzle2	$⊢ J \in (M \dots N) \to J \leq N$
32	4 31	syl	$⊢ φ \to J \leq N$
33	26 29 30 5 32	ltletrd	$⊢ φ \to I < N$
34		elfzo2	$⊢ I \in (M ..^N) \leftrightarrow (I \in ℤ_{\geq M} \land N \in ℤ \land I < N)$
35	21 25 33 34	syl3anbrc	$⊢ φ \to I \in (M ..^N)$
36		fzofzp1	$⊢ I \in (M ..^N) \to I + 1 \in (M \dots N)$
37	35 36	syl	$⊢ φ \to I + 1 \in (M \dots N)$
38	37	ancli	$⊢ φ \to (φ \land I + 1 \in (M \dots N))$
39		eleq1	$⊢ k = I + 1 \to (k \in (M \dots N) \leftrightarrow I + 1 \in (M \dots N))$
40	39	anbi2d	$⊢ k = I + 1 \to ((φ \land k \in (M \dots N)) \leftrightarrow (φ \land I + 1 \in (M \dots N)))$
41		fveq2	$⊢ k = I + 1 \to F (k) = F (I + 1)$
42	41	eleq1d	$⊢ k = I + 1 \to (F (k) \in ℝ \leftrightarrow F (I + 1) \in ℝ)$
43	40 42	imbi12d	$⊢ k = I + 1 \to (((φ \land k \in (M \dots N)) \to F (k) \in ℝ) \leftrightarrow ((φ \land I + 1 \in (M \dots N)) \to F (I + 1) \in ℝ))$
44	43 1	vtoclg	$⊢ I + 1 \in (M \dots N) \to ((φ \land I + 1 \in (M \dots N)) \to F (I + 1) \in ℝ)$
45	37 38 44	sylc	$⊢ φ \to F (I + 1) \in ℝ$
46	4	ancli	$⊢ φ \to (φ \land J \in (M \dots N))$
47		eleq1	$⊢ k = J \to (k \in (M \dots N) \leftrightarrow J \in (M \dots N))$
48	47	anbi2d	$⊢ k = J \to ((φ \land k \in (M \dots N)) \leftrightarrow (φ \land J \in (M \dots N)))$
49		fveq2	$⊢ k = J \to F (k) = F (J)$
50	49	eleq1d	$⊢ k = J \to (F (k) \in ℝ \leftrightarrow F (J) \in ℝ)$
51	48 50	imbi12d	$⊢ k = J \to (((φ \land k \in (M \dots N)) \to F (k) \in ℝ) \leftrightarrow ((φ \land J \in (M \dots N)) \to F (J) \in ℝ))$
52	51 1	vtoclg	$⊢ J \in (M \dots N) \to ((φ \land J \in (M \dots N)) \to F (J) \in ℝ)$
53	4 46 52	sylc	$⊢ φ \to F (J) \in ℝ$
54	35	ancli	$⊢ φ \to (φ \land I \in (M ..^N))$
55		eleq1	$⊢ k = I \to (k \in (M ..^N) \leftrightarrow I \in (M ..^N))$
56	55	anbi2d	$⊢ k = I \to ((φ \land k \in (M ..^N)) \leftrightarrow (φ \land I \in (M ..^N)))$
57		fvoveq1	$⊢ k = I \to F (k + 1) = F (I + 1)$
58	9 57	breq12d	$⊢ k = I \to (F (k) < F (k + 1) \leftrightarrow F (I) < F (I + 1))$
59	56 58	imbi12d	$⊢ k = I \to (((φ \land k \in (M ..^N)) \to F (k) < F (k + 1)) \leftrightarrow ((φ \land I \in (M ..^N)) \to F (I) < F (I + 1)))$
60	59 2	vtoclg	$⊢ I \in (M ..^N) \to ((φ \land I \in (M ..^N)) \to F (I) < F (I + 1))$
61	35 54 60	sylc	$⊢ φ \to F (I) < F (I + 1)$
62	17	peano2zd	$⊢ φ \to I + 1 \in ℤ$
63		zltp1le	$⊢ (I \in ℤ \land J \in ℤ) \to (I < J \leftrightarrow I + 1 \leq J)$
64	17 28 63	syl2anc	$⊢ φ \to (I < J \leftrightarrow I + 1 \leq J)$
65	5 64	mpbid	$⊢ φ \to I + 1 \leq J$
66		eluz2	$⊢ J \in ℤ_{\geq (I + 1)} \leftrightarrow (I + 1 \in ℤ \land J \in ℤ \land I + 1 \leq J)$
67	62 28 65 66	syl3anbrc	$⊢ φ \to J \in ℤ_{\geq (I + 1)}$
68	15	adantr	$⊢ (φ \land k \in (I + 1 \dots J)) \to M \in ℤ$
69	25	adantr	$⊢ (φ \land k \in (I + 1 \dots J)) \to N \in ℤ$
70		elfzelz	$⊢ k \in (I + 1 \dots J) \to k \in ℤ$
71	70	adantl	$⊢ (φ \land k \in (I + 1 \dots J)) \to k \in ℤ$
72	68 69 71	3jca	$⊢ (φ \land k \in (I + 1 \dots J)) \to (M \in ℤ \land N \in ℤ \land k \in ℤ)$
73	68	zred	$⊢ (φ \land k \in (I + 1 \dots J)) \to M \in ℝ$
74	71	zred	$⊢ (φ \land k \in (I + 1 \dots J)) \to k \in ℝ$
75	62	zred	$⊢ φ \to I + 1 \in ℝ$
76	75	adantr	$⊢ (φ \land k \in (I + 1 \dots J)) \to I + 1 \in ℝ$
77	26	adantr	$⊢ (φ \land k \in (I + 1 \dots J)) \to I \in ℝ$
78	19	adantr	$⊢ (φ \land k \in (I + 1 \dots J)) \to M \leq I$
79	77	ltp1d	$⊢ (φ \land k \in (I + 1 \dots J)) \to I < I + 1$
80	73 77 76 78 79	lelttrd	$⊢ (φ \land k \in (I + 1 \dots J)) \to M < I + 1$
81		elfzle1	$⊢ k \in (I + 1 \dots J) \to I + 1 \leq k$
82	81	adantl	$⊢ (φ \land k \in (I + 1 \dots J)) \to I + 1 \leq k$
83	73 76 74 80 82	ltletrd	$⊢ (φ \land k \in (I + 1 \dots J)) \to M < k$
84	73 74 83	ltled	$⊢ (φ \land k \in (I + 1 \dots J)) \to M \leq k$
85	29	adantr	$⊢ (φ \land k \in (I + 1 \dots J)) \to J \in ℝ$
86	69	zred	$⊢ (φ \land k \in (I + 1 \dots J)) \to N \in ℝ$
87		elfzle2	$⊢ k \in (I + 1 \dots J) \to k \leq J$
88	87	adantl	$⊢ (φ \land k \in (I + 1 \dots J)) \to k \leq J$
89	32	adantr	$⊢ (φ \land k \in (I + 1 \dots J)) \to J \leq N$
90	74 85 86 88 89	letrd	$⊢ (φ \land k \in (I + 1 \dots J)) \to k \leq N$
91	72 84 90	jca32	$⊢ (φ \land k \in (I + 1 \dots J)) \to ((M \in ℤ \land N \in ℤ \land k \in ℤ) \land (M \leq k \land k \leq N))$
92		elfz2	$⊢ k \in (M \dots N) \leftrightarrow ((M \in ℤ \land N \in ℤ \land k \in ℤ) \land (M \leq k \land k \leq N))$
93	91 92	sylibr	$⊢ (φ \land k \in (I + 1 \dots J)) \to k \in (M \dots N)$
94	93 1	syldan	$⊢ (φ \land k \in (I + 1 \dots J)) \to F (k) \in ℝ$
95	15	adantr	$⊢ (φ \land k \in (I + 1 \dots J - 1)) \to M \in ℤ$
96	25	adantr	$⊢ (φ \land k \in (I + 1 \dots J - 1)) \to N \in ℤ$
97		elfzelz	$⊢ k \in (I + 1 \dots J - 1) \to k \in ℤ$
98	97	adantl	$⊢ (φ \land k \in (I + 1 \dots J - 1)) \to k \in ℤ$
99	95 96 98	3jca	$⊢ (φ \land k \in (I + 1 \dots J - 1)) \to (M \in ℤ \land N \in ℤ \land k \in ℤ)$
100	95	zred	$⊢ (φ \land k \in (I + 1 \dots J - 1)) \to M \in ℝ$
101	98	zred	$⊢ (φ \land k \in (I + 1 \dots J - 1)) \to k \in ℝ$
102	75	adantr	$⊢ (φ \land k \in (I + 1 \dots J - 1)) \to I + 1 \in ℝ$
103	15	zred	$⊢ φ \to M \in ℝ$
104	26	ltp1d	$⊢ φ \to I < I + 1$
105	103 26 75 19 104	lelttrd	$⊢ φ \to M < I + 1$
106	105	adantr	$⊢ (φ \land k \in (I + 1 \dots J - 1)) \to M < I + 1$
107		elfzle1	$⊢ k \in (I + 1 \dots J - 1) \to I + 1 \leq k$
108	107	adantl	$⊢ (φ \land k \in (I + 1 \dots J - 1)) \to I + 1 \leq k$
109	100 102 101 106 108	ltletrd	$⊢ (φ \land k \in (I + 1 \dots J - 1)) \to M < k$
110	100 101 109	ltled	$⊢ (φ \land k \in (I + 1 \dots J - 1)) \to M \leq k$
111	96	zred	$⊢ (φ \land k \in (I + 1 \dots J - 1)) \to N \in ℝ$
112		peano2rem	$⊢ J \in ℝ \to J - 1 \in ℝ$
113	29 112	syl	$⊢ φ \to J - 1 \in ℝ$
114	113	adantr	$⊢ (φ \land k \in (I + 1 \dots J - 1)) \to J - 1 \in ℝ$
115		elfzle2	$⊢ k \in (I + 1 \dots J - 1) \to k \leq J - 1$
116	115	adantl	$⊢ (φ \land k \in (I + 1 \dots J - 1)) \to k \leq J - 1$
117	29	adantr	$⊢ (φ \land k \in (I + 1 \dots J - 1)) \to J \in ℝ$
118	117	ltm1d	$⊢ (φ \land k \in (I + 1 \dots J - 1)) \to J - 1 < J$
119	32	adantr	$⊢ (φ \land k \in (I + 1 \dots J - 1)) \to J \leq N$
120	114 117 111 118 119	ltletrd	$⊢ (φ \land k \in (I + 1 \dots J - 1)) \to J - 1 < N$
121	101 114 111 116 120	lelttrd	$⊢ (φ \land k \in (I + 1 \dots J - 1)) \to k < N$
122	101 111 121	ltled	$⊢ (φ \land k \in (I + 1 \dots J - 1)) \to k \leq N$
123	99 110 122	jca32	$⊢ (φ \land k \in (I + 1 \dots J - 1)) \to ((M \in ℤ \land N \in ℤ \land k \in ℤ) \land (M \leq k \land k \leq N))$
124	123 92	sylibr	$⊢ (φ \land k \in (I + 1 \dots J - 1)) \to k \in (M \dots N)$
125	124 1	syldan	$⊢ (φ \land k \in (I + 1 \dots J - 1)) \to F (k) \in ℝ$
126		peano2zm	$⊢ N \in ℤ \to N - 1 \in ℤ$
127	96 126	syl	$⊢ (φ \land k \in (I + 1 \dots J - 1)) \to N - 1 \in ℤ$
128	95 127 98	3jca	$⊢ (φ \land k \in (I + 1 \dots J - 1)) \to (M \in ℤ \land N - 1 \in ℤ \land k \in ℤ)$
129	127	zred	$⊢ (φ \land k \in (I + 1 \dots J - 1)) \to N - 1 \in ℝ$
130		1red	$⊢ φ \to 1 \in ℝ$
131	29 30 130 32	lesub1dd	$⊢ φ \to J - 1 \leq N - 1$
132	131	adantr	$⊢ (φ \land k \in (I + 1 \dots J - 1)) \to J - 1 \leq N - 1$
133	101 114 129 116 132	letrd	$⊢ (φ \land k \in (I + 1 \dots J - 1)) \to k \leq N - 1$
134	128 110 133	jca32	$⊢ (φ \land k \in (I + 1 \dots J - 1)) \to ((M \in ℤ \land N - 1 \in ℤ \land k \in ℤ) \land (M \leq k \land k \leq N - 1))$
135		elfz2	$⊢ k \in (M \dots N - 1) \leftrightarrow ((M \in ℤ \land N - 1 \in ℤ \land k \in ℤ) \land (M \leq k \land k \leq N - 1))$
136	134 135	sylibr	$⊢ (φ \land k \in (I + 1 \dots J - 1)) \to k \in (M \dots N - 1)$
137		simpr	$⊢ (φ \land k \in (M \dots N - 1)) \to k \in (M \dots N - 1)$
138		fzoval	$⊢ N \in ℤ \to (M ..^N) = (M \dots N - 1)$
139	25 138	syl	$⊢ φ \to (M ..^N) = (M \dots N - 1)$
140	139	eqcomd	$⊢ φ \to (M \dots N - 1) = (M ..^N)$
141	140	adantr	$⊢ (φ \land k \in (M \dots N - 1)) \to (M \dots N - 1) = (M ..^N)$
142	137 141	eleqtrd	$⊢ (φ \land k \in (M \dots N - 1)) \to k \in (M ..^N)$
143		fzofzp1	$⊢ k \in (M ..^N) \to k + 1 \in (M \dots N)$
144	142 143	syl	$⊢ (φ \land k \in (M \dots N - 1)) \to k + 1 \in (M \dots N)$
145		simpl	$⊢ (φ \land k \in (M \dots N - 1)) \to φ$
146	145 144	jca	$⊢ (φ \land k \in (M \dots N - 1)) \to (φ \land k + 1 \in (M \dots N))$
147		eleq1	$⊢ j = k + 1 \to (j \in (M \dots N) \leftrightarrow k + 1 \in (M \dots N))$
148	147	anbi2d	$⊢ j = k + 1 \to ((φ \land j \in (M \dots N)) \leftrightarrow (φ \land k + 1 \in (M \dots N)))$
149		fveq2	$⊢ j = k + 1 \to F (j) = F (k + 1)$
150	149	eleq1d	$⊢ j = k + 1 \to (F (j) \in ℝ \leftrightarrow F (k + 1) \in ℝ)$
151	148 150	imbi12d	$⊢ j = k + 1 \to (((φ \land j \in (M \dots N)) \to F (j) \in ℝ) \leftrightarrow ((φ \land k + 1 \in (M \dots N)) \to F (k + 1) \in ℝ))$
152		eleq1	$⊢ k = j \to (k \in (M \dots N) \leftrightarrow j \in (M \dots N))$
153	152	anbi2d	$⊢ k = j \to ((φ \land k \in (M \dots N)) \leftrightarrow (φ \land j \in (M \dots N)))$
154		fveq2	$⊢ k = j \to F (k) = F (j)$
155	154	eleq1d	$⊢ k = j \to (F (k) \in ℝ \leftrightarrow F (j) \in ℝ)$
156	153 155	imbi12d	$⊢ k = j \to (((φ \land k \in (M \dots N)) \to F (k) \in ℝ) \leftrightarrow ((φ \land j \in (M \dots N)) \to F (j) \in ℝ))$
157	156 1	chvarvv	$⊢ (φ \land j \in (M \dots N)) \to F (j) \in ℝ$
158	151 157	vtoclg	$⊢ k + 1 \in (M \dots N) \to ((φ \land k + 1 \in (M \dots N)) \to F (k + 1) \in ℝ)$
159	144 146 158	sylc	$⊢ (φ \land k \in (M \dots N - 1)) \to F (k + 1) \in ℝ$
160	136 159	syldan	$⊢ (φ \land k \in (I + 1 \dots J - 1)) \to F (k + 1) \in ℝ$
161	142 2	syldan	$⊢ (φ \land k \in (M \dots N - 1)) \to F (k) < F (k + 1)$
162	136 161	syldan	$⊢ (φ \land k \in (I + 1 \dots J - 1)) \to F (k) < F (k + 1)$
163	125 160 162	ltled	$⊢ (φ \land k \in (I + 1 \dots J - 1)) \to F (k) \leq F (k + 1)$
164	67 94 163	monoord	$⊢ φ \to F (I + 1) \leq F (J)$
165	13 45 53 61 164	ltletrd	$⊢ φ \to F (I) < F (J)$

Metamath Proof Explorer

Theorem monoords

Proof