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

Metamath Proof Explorer

Theorem climsuselem1

Proof