climsuselem1

Description: The subsequence index I has the expected properties: it belongs to the same upper integers as the original index, and it is always greater than or equal to the original index. (Contributed by Glauco Siliprandi, 29-Jun-2017)

	Ref	Expression
Hypotheses	climsuselem1.1	$⊢ Z = ℤ_{\geq M}$
	climsuselem1.2	$⊢ φ \to M \in ℤ$
	climsuselem1.3	$⊢ φ \to I (M) \in Z$
	climsuselem1.4	$⊢ (φ \land k \in Z) \to I (k + 1) \in ℤ_{\geq (I (k) + 1)}$
Assertion	climsuselem1	$⊢ (φ \land K \in Z) \to I (K) \in ℤ_{\geq K}$

Proof

Step	Hyp	Ref	Expression
1		climsuselem1.1	$⊢ Z = ℤ_{\geq M}$
2		climsuselem1.2	$⊢ φ \to M \in ℤ$
3		climsuselem1.3	$⊢ φ \to I (M) \in Z$
4		climsuselem1.4	$⊢ (φ \land k \in Z) \to I (k + 1) \in ℤ_{\geq (I (k) + 1)}$
5	1	eleq2i	$⊢ K \in Z \leftrightarrow K \in ℤ_{\geq M}$
6	5	bilani	$⊢ (φ \land K \in Z) \to K \in ℤ_{\geq M}$
7		simpl	$⊢ (φ \land K \in Z) \to φ$
8		fveq2	$⊢ j = M \to I (j) = I (M)$
9		fveq2	$⊢ j = M \to ℤ_{\geq j} = ℤ_{\geq M}$
10	8 9	eleq12d	$⊢ j = M \to (I (j) \in ℤ_{\geq j} \leftrightarrow I (M) \in ℤ_{\geq M})$
11	10	imbi2d	$⊢ j = M \to ((φ \to I (j) \in ℤ_{\geq j}) \leftrightarrow (φ \to I (M) \in ℤ_{\geq M}))$
12		fveq2	$⊢ j = k \to I (j) = I (k)$
13		fveq2	$⊢ j = k \to ℤ_{\geq j} = ℤ_{\geq k}$
14	12 13	eleq12d	$⊢ j = k \to (I (j) \in ℤ_{\geq j} \leftrightarrow I (k) \in ℤ_{\geq k})$
15	14	imbi2d	$⊢ j = k \to ((φ \to I (j) \in ℤ_{\geq j}) \leftrightarrow (φ \to I (k) \in ℤ_{\geq k}))$
16		fveq2	$⊢ j = k + 1 \to I (j) = I (k + 1)$
17		fveq2	$⊢ j = k + 1 \to ℤ_{\geq j} = ℤ_{\geq (k + 1)}$
18	16 17	eleq12d	$⊢ j = k + 1 \to (I (j) \in ℤ_{\geq j} \leftrightarrow I (k + 1) \in ℤ_{\geq (k + 1)})$
19	18	imbi2d	$⊢ j = k + 1 \to ((φ \to I (j) \in ℤ_{\geq j}) \leftrightarrow (φ \to I (k + 1) \in ℤ_{\geq (k + 1)}))$
20		fveq2	$⊢ j = K \to I (j) = I (K)$
21		fveq2	$⊢ j = K \to ℤ_{\geq j} = ℤ_{\geq K}$
22	20 21	eleq12d	$⊢ j = K \to (I (j) \in ℤ_{\geq j} \leftrightarrow I (K) \in ℤ_{\geq K})$
23	22	imbi2d	$⊢ j = K \to ((φ \to I (j) \in ℤ_{\geq j}) \leftrightarrow (φ \to I (K) \in ℤ_{\geq K}))$
24	3 1	eleqtrdi	$⊢ φ \to I (M) \in ℤ_{\geq M}$
25	24	a1i	$⊢ M \in ℤ \to (φ \to I (M) \in ℤ_{\geq M})$
26		simpr	$⊢ ((k \in ℤ_{\geq M} \land (φ \to I (k) \in ℤ_{\geq k})) \land φ) \to φ$
27		simpll	$⊢ ((k \in ℤ_{\geq M} \land (φ \to I (k) \in ℤ_{\geq k})) \land φ) \to k \in ℤ_{\geq M}$
28		simplr	$⊢ ((k \in ℤ_{\geq M} \land (φ \to I (k) \in ℤ_{\geq k})) \land φ) \to (φ \to I (k) \in ℤ_{\geq k})$
29	26 28	mpd	$⊢ ((k \in ℤ_{\geq M} \land (φ \to I (k) \in ℤ_{\geq k})) \land φ) \to I (k) \in ℤ_{\geq k}$
30		eluzelz	$⊢ k \in ℤ_{\geq M} \to k \in ℤ$
31	30	3ad2ant2	$⊢ (φ \land k \in ℤ_{\geq M} \land I (k) \in ℤ_{\geq k}) \to k \in ℤ$
32	31	peano2zd	$⊢ (φ \land k \in ℤ_{\geq M} \land I (k) \in ℤ_{\geq k}) \to k + 1 \in ℤ$
33	32	zred	$⊢ (φ \land k \in ℤ_{\geq M} \land I (k) \in ℤ_{\geq k}) \to k + 1 \in ℝ$
34		eluzelre	$⊢ I (k) \in ℤ_{\geq k} \to I (k) \in ℝ$
35	34	3ad2ant3	$⊢ (φ \land k \in ℤ_{\geq M} \land I (k) \in ℤ_{\geq k}) \to I (k) \in ℝ$
36		1red	$⊢ (φ \land k \in ℤ_{\geq M} \land I (k) \in ℤ_{\geq k}) \to 1 \in ℝ$
37	35 36	readdcld	$⊢ (φ \land k \in ℤ_{\geq M} \land I (k) \in ℤ_{\geq k}) \to I (k) + 1 \in ℝ$
38	1	eqimss2i	$⊢ ℤ_{\geq M} \subseteq Z$
39	38	a1i	$⊢ φ \to ℤ_{\geq M} \subseteq Z$
40	39	sseld	$⊢ φ \to (k \in ℤ_{\geq M} \to k \in Z)$
41	40	imdistani	$⊢ (φ \land k \in ℤ_{\geq M}) \to (φ \land k \in Z)$
42	41 4	syl	$⊢ (φ \land k \in ℤ_{\geq M}) \to I (k + 1) \in ℤ_{\geq (I (k) + 1)}$
43	42	3adant3	$⊢ (φ \land k \in ℤ_{\geq M} \land I (k) \in ℤ_{\geq k}) \to I (k + 1) \in ℤ_{\geq (I (k) + 1)}$
44		eluzelz	$⊢ I (k + 1) \in ℤ_{\geq (I (k) + 1)} \to I (k + 1) \in ℤ$
45	43 44	syl	$⊢ (φ \land k \in ℤ_{\geq M} \land I (k) \in ℤ_{\geq k}) \to I (k + 1) \in ℤ$
46	45	zred	$⊢ (φ \land k \in ℤ_{\geq M} \land I (k) \in ℤ_{\geq k}) \to I (k + 1) \in ℝ$
47	31	zred	$⊢ (φ \land k \in ℤ_{\geq M} \land I (k) \in ℤ_{\geq k}) \to k \in ℝ$
48		eluzle	$⊢ I (k) \in ℤ_{\geq k} \to k \leq I (k)$
49	48	3ad2ant3	$⊢ (φ \land k \in ℤ_{\geq M} \land I (k) \in ℤ_{\geq k}) \to k \leq I (k)$
50	47 35 36 49	leadd1dd	$⊢ (φ \land k \in ℤ_{\geq M} \land I (k) \in ℤ_{\geq k}) \to k + 1 \leq I (k) + 1$
51		eluzle	$⊢ I (k + 1) \in ℤ_{\geq (I (k) + 1)} \to I (k) + 1 \leq I (k + 1)$
52	43 51	syl	$⊢ (φ \land k \in ℤ_{\geq M} \land I (k) \in ℤ_{\geq k}) \to I (k) + 1 \leq I (k + 1)$
53	33 37 46 50 52	letrd	$⊢ (φ \land k \in ℤ_{\geq M} \land I (k) \in ℤ_{\geq k}) \to k + 1 \leq I (k + 1)$
54		eluz	$⊢ (k + 1 \in ℤ \land I (k + 1) \in ℤ) \to (I (k + 1) \in ℤ_{\geq (k + 1)} \leftrightarrow k + 1 \leq I (k + 1))$
55	32 45 54	syl2anc	$⊢ (φ \land k \in ℤ_{\geq M} \land I (k) \in ℤ_{\geq k}) \to (I (k + 1) \in ℤ_{\geq (k + 1)} \leftrightarrow k + 1 \leq I (k + 1))$
56	53 55	mpbird	$⊢ (φ \land k \in ℤ_{\geq M} \land I (k) \in ℤ_{\geq k}) \to I (k + 1) \in ℤ_{\geq (k + 1)}$
57	26 27 29 56	syl3anc	$⊢ ((k \in ℤ_{\geq M} \land (φ \to I (k) \in ℤ_{\geq k})) \land φ) \to I (k + 1) \in ℤ_{\geq (k + 1)}$
58	57	exp31	$⊢ k \in ℤ_{\geq M} \to ((φ \to I (k) \in ℤ_{\geq k}) \to (φ \to I (k + 1) \in ℤ_{\geq (k + 1)}))$
59	11 15 19 23 25 58	uzind4	$⊢ K \in ℤ_{\geq M} \to (φ \to I (K) \in ℤ_{\geq K})$
60	6 7 59	sylc	$⊢ (φ \land K \in Z) \to I (K) \in ℤ_{\geq K}$

Metamath Proof Explorer

Theorem climsuselem1

Proof