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

Metamath Proof Explorer

Theorem monoords

Proof