smonoord

Description: Ordering relation for a strictly monotonic sequence, increasing case. Analogous to monoord (except that the case M = N must be excluded). Duplicate of monoords ? (Contributed by AV, 12-Jul-2020)

	Ref	Expression
Hypotheses	smonoord.0	$⊢ φ \to M \in ℤ$
	smonoord.1	$⊢ φ \to N \in ℤ_{\geq (M + 1)}$
	smonoord.2	$⊢ (φ \land k \in (M \dots N)) \to F (k) \in ℝ$
	smonoord.3	$⊢ (φ \land k \in (M \dots N - 1)) \to F (k) < F (k + 1)$
Assertion	smonoord	$⊢ φ \to F (M) < F (N)$

Proof

Step	Hyp	Ref	Expression
1		smonoord.0	$⊢ φ \to M \in ℤ$
2		smonoord.1	$⊢ φ \to N \in ℤ_{\geq (M + 1)}$
3		smonoord.2	$⊢ (φ \land k \in (M \dots N)) \to F (k) \in ℝ$
4		smonoord.3	$⊢ (φ \land k \in (M \dots N - 1)) \to F (k) < F (k + 1)$
5		eluzfz2	$⊢ N \in ℤ_{\geq (M + 1)} \to N \in (M + 1 \dots N)$
6	2 5	syl	$⊢ φ \to N \in (M + 1 \dots N)$
7		eleq1	$⊢ x = M + 1 \to (x \in (M + 1 \dots N) \leftrightarrow M + 1 \in (M + 1 \dots N))$
8		fveq2	$⊢ x = M + 1 \to F (x) = F (M + 1)$
9	8	breq2d	$⊢ x = M + 1 \to (F (M) < F (x) \leftrightarrow F (M) < F (M + 1))$
10	7 9	imbi12d	$⊢ x = M + 1 \to ((x \in (M + 1 \dots N) \to F (M) < F (x)) \leftrightarrow (M + 1 \in (M + 1 \dots N) \to F (M) < F (M + 1)))$
11	10	imbi2d	$⊢ x = M + 1 \to ((φ \to (x \in (M + 1 \dots N) \to F (M) < F (x))) \leftrightarrow (φ \to (M + 1 \in (M + 1 \dots N) \to F (M) < F (M + 1))))$
12		eleq1	$⊢ x = n \to (x \in (M + 1 \dots N) \leftrightarrow n \in (M + 1 \dots N))$
13		fveq2	$⊢ x = n \to F (x) = F (n)$
14	13	breq2d	$⊢ x = n \to (F (M) < F (x) \leftrightarrow F (M) < F (n))$
15	12 14	imbi12d	$⊢ x = n \to ((x \in (M + 1 \dots N) \to F (M) < F (x)) \leftrightarrow (n \in (M + 1 \dots N) \to F (M) < F (n)))$
16	15	imbi2d	$⊢ x = n \to ((φ \to (x \in (M + 1 \dots N) \to F (M) < F (x))) \leftrightarrow (φ \to (n \in (M + 1 \dots N) \to F (M) < F (n))))$
17		eleq1	$⊢ x = n + 1 \to (x \in (M + 1 \dots N) \leftrightarrow n + 1 \in (M + 1 \dots N))$
18		fveq2	$⊢ x = n + 1 \to F (x) = F (n + 1)$
19	18	breq2d	$⊢ x = n + 1 \to (F (M) < F (x) \leftrightarrow F (M) < F (n + 1))$
20	17 19	imbi12d	$⊢ x = n + 1 \to ((x \in (M + 1 \dots N) \to F (M) < F (x)) \leftrightarrow (n + 1 \in (M + 1 \dots N) \to F (M) < F (n + 1)))$
21	20	imbi2d	$⊢ x = n + 1 \to ((φ \to (x \in (M + 1 \dots N) \to F (M) < F (x))) \leftrightarrow (φ \to (n + 1 \in (M + 1 \dots N) \to F (M) < F (n + 1))))$
22		eleq1	$⊢ x = N \to (x \in (M + 1 \dots N) \leftrightarrow N \in (M + 1 \dots N))$
23		fveq2	$⊢ x = N \to F (x) = F (N)$
24	23	breq2d	$⊢ x = N \to (F (M) < F (x) \leftrightarrow F (M) < F (N))$
25	22 24	imbi12d	$⊢ x = N \to ((x \in (M + 1 \dots N) \to F (M) < F (x)) \leftrightarrow (N \in (M + 1 \dots N) \to F (M) < F (N)))$
26	25	imbi2d	$⊢ x = N \to ((φ \to (x \in (M + 1 \dots N) \to F (M) < F (x))) \leftrightarrow (φ \to (N \in (M + 1 \dots N) \to F (M) < F (N))))$
27		eluzp1m1	$⊢ (M \in ℤ \land N \in ℤ_{\geq (M + 1)}) \to N - 1 \in ℤ_{\geq M}$
28	1 2 27	syl2anc	$⊢ φ \to N - 1 \in ℤ_{\geq M}$
29		eluzfz1	$⊢ N - 1 \in ℤ_{\geq M} \to M \in (M \dots N - 1)$
30	28 29	syl	$⊢ φ \to M \in (M \dots N - 1)$
31	4	ralrimiva	$⊢ φ \to \forall k \in (M \dots N - 1) F (k) < F (k + 1)$
32		fveq2	$⊢ k = M \to F (k) = F (M)$
33		fvoveq1	$⊢ k = M \to F (k + 1) = F (M + 1)$
34	32 33	breq12d	$⊢ k = M \to (F (k) < F (k + 1) \leftrightarrow F (M) < F (M + 1))$
35	34	rspcv	$⊢ M \in (M \dots N - 1) \to (\forall k \in (M \dots N - 1) F (k) < F (k + 1) \to F (M) < F (M + 1))$
36	30 31 35	sylc	$⊢ φ \to F (M) < F (M + 1)$
37	36	a1d	$⊢ φ \to (M + 1 \in (M + 1 \dots N) \to F (M) < F (M + 1))$
38	37	a1i	$⊢ M + 1 \in ℤ \to (φ \to (M + 1 \in (M + 1 \dots N) \to F (M) < F (M + 1)))$
39		peano2fzr	$⊢ (n \in ℤ_{\geq (M + 1)} \land n + 1 \in (M + 1 \dots N)) \to n \in (M + 1 \dots N)$
40	39	adantll	$⊢ ((φ \land n \in ℤ_{\geq (M + 1)}) \land n + 1 \in (M + 1 \dots N)) \to n \in (M + 1 \dots N)$
41	40	ex	$⊢ (φ \land n \in ℤ_{\geq (M + 1)}) \to (n + 1 \in (M + 1 \dots N) \to n \in (M + 1 \dots N))$
42	41	imim1d	$⊢ (φ \land n \in ℤ_{\geq (M + 1)}) \to ((n \in (M + 1 \dots N) \to F (M) < F (n)) \to (n + 1 \in (M + 1 \dots N) \to F (M) < F (n)))$
43		peano2uzr	$⊢ (M \in ℤ \land n \in ℤ_{\geq (M + 1)}) \to n \in ℤ_{\geq M}$
44	43	ex	$⊢ M \in ℤ \to (n \in ℤ_{\geq (M + 1)} \to n \in ℤ_{\geq M})$
45	44 1	syl11	$⊢ n \in ℤ_{\geq (M + 1)} \to (φ \to n \in ℤ_{\geq M})$
46	45	adantr	$⊢ (n \in ℤ_{\geq (M + 1)} \land n + 1 \in (M + 1 \dots N)) \to (φ \to n \in ℤ_{\geq M})$
47	46	impcom	$⊢ (φ \land (n \in ℤ_{\geq (M + 1)} \land n + 1 \in (M + 1 \dots N))) \to n \in ℤ_{\geq M}$
48		eluzelz	$⊢ n \in ℤ_{\geq (M + 1)} \to n \in ℤ$
49	48	adantr	$⊢ (n \in ℤ_{\geq (M + 1)} \land n + 1 \in (M + 1 \dots N)) \to n \in ℤ$
50	49	adantl	$⊢ (φ \land (n \in ℤ_{\geq (M + 1)} \land n + 1 \in (M + 1 \dots N))) \to n \in ℤ$
51		elfzuz3	$⊢ n + 1 \in (M + 1 \dots N) \to N \in ℤ_{\geq (n + 1)}$
52	51	ad2antll	$⊢ (φ \land (n \in ℤ_{\geq (M + 1)} \land n + 1 \in (M + 1 \dots N))) \to N \in ℤ_{\geq (n + 1)}$
53		eluzp1m1	$⊢ (n \in ℤ \land N \in ℤ_{\geq (n + 1)}) \to N - 1 \in ℤ_{\geq n}$
54	50 52 53	syl2anc	$⊢ (φ \land (n \in ℤ_{\geq (M + 1)} \land n + 1 \in (M + 1 \dots N))) \to N - 1 \in ℤ_{\geq n}$
55		elfzuzb	$⊢ n \in (M \dots N - 1) \leftrightarrow (n \in ℤ_{\geq M} \land N - 1 \in ℤ_{\geq n})$
56	47 54 55	sylanbrc	$⊢ (φ \land (n \in ℤ_{\geq (M + 1)} \land n + 1 \in (M + 1 \dots N))) \to n \in (M \dots N - 1)$
57	31	adantr	$⊢ (φ \land (n \in ℤ_{\geq (M + 1)} \land n + 1 \in (M + 1 \dots N))) \to \forall k \in (M \dots N - 1) F (k) < F (k + 1)$
58		fveq2	$⊢ k = n \to F (k) = F (n)$
59		fvoveq1	$⊢ k = n \to F (k + 1) = F (n + 1)$
60	58 59	breq12d	$⊢ k = n \to (F (k) < F (k + 1) \leftrightarrow F (n) < F (n + 1))$
61	60	rspcv	$⊢ n \in (M \dots N - 1) \to (\forall k \in (M \dots N - 1) F (k) < F (k + 1) \to F (n) < F (n + 1))$
62	56 57 61	sylc	$⊢ (φ \land (n \in ℤ_{\geq (M + 1)} \land n + 1 \in (M + 1 \dots N))) \to F (n) < F (n + 1)$
63		zre	$⊢ M \in ℤ \to M \in ℝ$
64	63	lep1d	$⊢ M \in ℤ \to M \leq M + 1$
65	1 64	jccir	$⊢ φ \to (M \in ℤ \land M \leq M + 1)$
66		eluzuzle	$⊢ (M \in ℤ \land M \leq M + 1) \to (N \in ℤ_{\geq (M + 1)} \to N \in ℤ_{\geq M})$
67	65 2 66	sylc	$⊢ φ \to N \in ℤ_{\geq M}$
68		eluzfz1	$⊢ N \in ℤ_{\geq M} \to M \in (M \dots N)$
69	67 68	syl	$⊢ φ \to M \in (M \dots N)$
70	3	ralrimiva	$⊢ φ \to \forall k \in (M \dots N) F (k) \in ℝ$
71	32	eleq1d	$⊢ k = M \to (F (k) \in ℝ \leftrightarrow F (M) \in ℝ)$
72	71	rspcv	$⊢ M \in (M \dots N) \to (\forall k \in (M \dots N) F (k) \in ℝ \to F (M) \in ℝ)$
73	69 70 72	sylc	$⊢ φ \to F (M) \in ℝ$
74	73	adantr	$⊢ (φ \land (n \in ℤ_{\geq (M + 1)} \land n + 1 \in (M + 1 \dots N))) \to F (M) \in ℝ$
75		fzp1ss	$⊢ M \in ℤ \to (M + 1 \dots N) \subseteq (M \dots N)$
76	1 75	syl	$⊢ φ \to (M + 1 \dots N) \subseteq (M \dots N)$
77	76	sseld	$⊢ φ \to (n + 1 \in (M + 1 \dots N) \to n + 1 \in (M \dots N))$
78	77	com12	$⊢ n + 1 \in (M + 1 \dots N) \to (φ \to n + 1 \in (M \dots N))$
79	78	adantl	$⊢ (n \in ℤ_{\geq (M + 1)} \land n + 1 \in (M + 1 \dots N)) \to (φ \to n + 1 \in (M \dots N))$
80	79	impcom	$⊢ (φ \land (n \in ℤ_{\geq (M + 1)} \land n + 1 \in (M + 1 \dots N))) \to n + 1 \in (M \dots N)$
81		peano2fzr	$⊢ (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \to n \in (M \dots N)$
82	47 80 81	syl2anc	$⊢ (φ \land (n \in ℤ_{\geq (M + 1)} \land n + 1 \in (M + 1 \dots N))) \to n \in (M \dots N)$
83	70	adantr	$⊢ (φ \land (n \in ℤ_{\geq (M + 1)} \land n + 1 \in (M + 1 \dots N))) \to \forall k \in (M \dots N) F (k) \in ℝ$
84	58	eleq1d	$⊢ k = n \to (F (k) \in ℝ \leftrightarrow F (n) \in ℝ)$
85	84	rspcv	$⊢ n \in (M \dots N) \to (\forall k \in (M \dots N) F (k) \in ℝ \to F (n) \in ℝ)$
86	82 83 85	sylc	$⊢ (φ \land (n \in ℤ_{\geq (M + 1)} \land n + 1 \in (M + 1 \dots N))) \to F (n) \in ℝ$
87		fveq2	$⊢ k = n + 1 \to F (k) = F (n + 1)$
88	87	eleq1d	$⊢ k = n + 1 \to (F (k) \in ℝ \leftrightarrow F (n + 1) \in ℝ)$
89	88	rspcv	$⊢ n + 1 \in (M \dots N) \to (\forall k \in (M \dots N) F (k) \in ℝ \to F (n + 1) \in ℝ)$
90	80 83 89	sylc	$⊢ (φ \land (n \in ℤ_{\geq (M + 1)} \land n + 1 \in (M + 1 \dots N))) \to F (n + 1) \in ℝ$
91		lttr	$⊢ (F (M) \in ℝ \land F (n) \in ℝ \land F (n + 1) \in ℝ) \to ((F (M) < F (n) \land F (n) < F (n + 1)) \to F (M) < F (n + 1))$
92	74 86 90 91	syl3anc	$⊢ (φ \land (n \in ℤ_{\geq (M + 1)} \land n + 1 \in (M + 1 \dots N))) \to ((F (M) < F (n) \land F (n) < F (n + 1)) \to F (M) < F (n + 1))$
93	62 92	mpan2d	$⊢ (φ \land (n \in ℤ_{\geq (M + 1)} \land n + 1 \in (M + 1 \dots N))) \to (F (M) < F (n) \to F (M) < F (n + 1))$
94	42 93	animpimp2impd	$⊢ n \in ℤ_{\geq (M + 1)} \to ((φ \to (n \in (M + 1 \dots N) \to F (M) < F (n))) \to (φ \to (n + 1 \in (M + 1 \dots N) \to F (M) < F (n + 1))))$
95	11 16 21 26 38 94	uzind4	$⊢ N \in ℤ_{\geq (M + 1)} \to (φ \to (N \in (M + 1 \dots N) \to F (M) < F (N)))$
96	2 95	mpcom	$⊢ φ \to (N \in (M + 1 \dots N) \to F (M) < F (N))$
97	6 96	mpd	$⊢ φ \to F (M) < F (N)$

Metamath Proof Explorer

Theorem smonoord

Proof