iscmet3lem3

		Ref	Expression
	Hypothesis	iscmet3.1	$⊢ Z = ℤ_{\geq M}$
	Assertion	iscmet3lem3	$⊢ (M \in ℤ \land R \in ℝ^{+}) \to \exists j \in Z \forall k \in ℤ_{\geq j} {(\frac{1}{2})}^{k} < R$

Proof

Step	Hyp	Ref	Expression
1		iscmet3.1	$⊢ Z = ℤ_{\geq M}$
2		simpl	$⊢ (M \in ℤ \land R \in ℝ^{+}) \to M \in ℤ$
3		simpr	$⊢ (M \in ℤ \land R \in ℝ^{+}) \to R \in ℝ^{+}$
4		eluzelz	$⊢ k \in ℤ_{\geq M} \to k \in ℤ$
5	4 1	eleq2s	$⊢ k \in Z \to k \in ℤ$
6	5	adantl	$⊢ ((M \in ℤ \land R \in ℝ^{+}) \land k \in Z) \to k \in ℤ$
7		oveq2	$⊢ n = k \to {(\frac{1}{2})}^{n} = {(\frac{1}{2})}^{k}$
8		eqid	$⊢ (n \in ℤ ⟼ {(\frac{1}{2})}^{n}) = (n \in ℤ ⟼ {(\frac{1}{2})}^{n})$
9		ovex	$⊢ {(\frac{1}{2})}^{k} \in V$
10	7 8 9	fvmpt	$⊢ k \in ℤ \to (n \in ℤ ⟼ {(\frac{1}{2})}^{n}) (k) = {(\frac{1}{2})}^{k}$
11	6 10	syl	$⊢ ((M \in ℤ \land R \in ℝ^{+}) \land k \in Z) \to (n \in ℤ ⟼ {(\frac{1}{2})}^{n}) (k) = {(\frac{1}{2})}^{k}$
12		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
13	12	reseq2i	$⊢ {(n \in ℤ ⟼ {(\frac{1}{2})}^{n}) ↾}_{ℕ_{0}} = {(n \in ℤ ⟼ {(\frac{1}{2})}^{n}) ↾}_{ℤ_{\geq 0}}$
14		nn0ssz	$⊢ ℕ_{0} \subseteq ℤ$
15		resmpt	$⊢ ℕ_{0} \subseteq ℤ \to {(n \in ℤ ⟼ {(\frac{1}{2})}^{n}) ↾}_{ℕ_{0}} = (n \in ℕ_{0} ⟼ {(\frac{1}{2})}^{n})$
16	14 15	ax-mp	$⊢ {(n \in ℤ ⟼ {(\frac{1}{2})}^{n}) ↾}_{ℕ_{0}} = (n \in ℕ_{0} ⟼ {(\frac{1}{2})}^{n})$
17	13 16	eqtr3i	$⊢ {(n \in ℤ ⟼ {(\frac{1}{2})}^{n}) ↾}_{ℤ_{\geq 0}} = (n \in ℕ_{0} ⟼ {(\frac{1}{2})}^{n})$
18		halfcn	$⊢ \frac{1}{2} \in ℂ$
19	18	a1i	$⊢ (M \in ℤ \land R \in ℝ^{+}) \to \frac{1}{2} \in ℂ$
20		halfre	$⊢ \frac{1}{2} \in ℝ$
21		halfge0	$⊢ 0 \leq \frac{1}{2}$
22		absid	$⊢ (\frac{1}{2} \in ℝ \land 0 \leq \frac{1}{2}) \to \|\frac{1}{2}\| = \frac{1}{2}$
23	20 21 22	mp2an	$⊢ \|\frac{1}{2}\| = \frac{1}{2}$
24		halflt1	$⊢ \frac{1}{2} < 1$
25	23 24	eqbrtri	$⊢ \|\frac{1}{2}\| < 1$
26	25	a1i	$⊢ (M \in ℤ \land R \in ℝ^{+}) \to \|\frac{1}{2}\| < 1$
27	19 26	expcnv	$⊢ (M \in ℤ \land R \in ℝ^{+}) \to (n \in ℕ_{0} ⟼ {(\frac{1}{2})}^{n}) ⇝ 0$
28	17 27	eqbrtrid	$⊢ (M \in ℤ \land R \in ℝ^{+}) \to ({(n \in ℤ ⟼ {(\frac{1}{2})}^{n}) ↾}_{ℤ_{\geq 0}}) ⇝ 0$
29		0z	$⊢ 0 \in ℤ$
30		zex	$⊢ ℤ \in V$
31	30	mptex	$⊢ (n \in ℤ ⟼ {(\frac{1}{2})}^{n}) \in V$
32	31	a1i	$⊢ (M \in ℤ \land R \in ℝ^{+}) \to (n \in ℤ ⟼ {(\frac{1}{2})}^{n}) \in V$
33		climres	$⊢ (0 \in ℤ \land (n \in ℤ ⟼ {(\frac{1}{2})}^{n}) \in V) \to (({(n \in ℤ ⟼ {(\frac{1}{2})}^{n}) ↾}_{ℤ_{\geq 0}}) ⇝ 0 \leftrightarrow (n \in ℤ ⟼ {(\frac{1}{2})}^{n}) ⇝ 0)$
34	29 32 33	sylancr	$⊢ (M \in ℤ \land R \in ℝ^{+}) \to (({(n \in ℤ ⟼ {(\frac{1}{2})}^{n}) ↾}_{ℤ_{\geq 0}}) ⇝ 0 \leftrightarrow (n \in ℤ ⟼ {(\frac{1}{2})}^{n}) ⇝ 0)$
35	28 34	mpbid	$⊢ (M \in ℤ \land R \in ℝ^{+}) \to (n \in ℤ ⟼ {(\frac{1}{2})}^{n}) ⇝ 0$
36	1 2 3 11 35	climi0	$⊢ (M \in ℤ \land R \in ℝ^{+}) \to \exists j \in Z \forall k \in ℤ_{\geq j} \|{(\frac{1}{2})}^{k}\| < R$
37	1	uztrn2	$⊢ (j \in Z \land k \in ℤ_{\geq j}) \to k \in Z$
38		1rp	$⊢ 1 \in ℝ^{+}$
39		rphalfcl	$⊢ 1 \in ℝ^{+} \to \frac{1}{2} \in ℝ^{+}$
40	38 39	ax-mp	$⊢ \frac{1}{2} \in ℝ^{+}$
41		rpexpcl	$⊢ (\frac{1}{2} \in ℝ^{+} \land k \in ℤ) \to {(\frac{1}{2})}^{k} \in ℝ^{+}$
42	40 6 41	sylancr	$⊢ ((M \in ℤ \land R \in ℝ^{+}) \land k \in Z) \to {(\frac{1}{2})}^{k} \in ℝ^{+}$
43		rpre	$⊢ {(\frac{1}{2})}^{k} \in ℝ^{+} \to {(\frac{1}{2})}^{k} \in ℝ$
44		rpge0	$⊢ {(\frac{1}{2})}^{k} \in ℝ^{+} \to 0 \leq {(\frac{1}{2})}^{k}$
45	43 44	absidd	$⊢ {(\frac{1}{2})}^{k} \in ℝ^{+} \to \|{(\frac{1}{2})}^{k}\| = {(\frac{1}{2})}^{k}$
46	42 45	syl	$⊢ ((M \in ℤ \land R \in ℝ^{+}) \land k \in Z) \to \|{(\frac{1}{2})}^{k}\| = {(\frac{1}{2})}^{k}$
47	46	breq1d	$⊢ ((M \in ℤ \land R \in ℝ^{+}) \land k \in Z) \to (\|{(\frac{1}{2})}^{k}\| < R \leftrightarrow {(\frac{1}{2})}^{k} < R)$
48	37 47	sylan2	$⊢ ((M \in ℤ \land R \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \to (\|{(\frac{1}{2})}^{k}\| < R \leftrightarrow {(\frac{1}{2})}^{k} < R)$
49	48	anassrs	$⊢ (((M \in ℤ \land R \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \to (\|{(\frac{1}{2})}^{k}\| < R \leftrightarrow {(\frac{1}{2})}^{k} < R)$
50	49	ralbidva	$⊢ ((M \in ℤ \land R \in ℝ^{+}) \land j \in Z) \to (\forall k \in ℤ_{\geq j} \|{(\frac{1}{2})}^{k}\| < R \leftrightarrow \forall k \in ℤ_{\geq j} {(\frac{1}{2})}^{k} < R)$
51	50	rexbidva	$⊢ (M \in ℤ \land R \in ℝ^{+}) \to (\exists j \in Z \forall k \in ℤ_{\geq j} \|{(\frac{1}{2})}^{k}\| < R \leftrightarrow \exists j \in Z \forall k \in ℤ_{\geq j} {(\frac{1}{2})}^{k} < R)$
52	36 51	mpbid	$⊢ (M \in ℤ \land R \in ℝ^{+}) \to \exists j \in Z \forall k \in ℤ_{\geq j} {(\frac{1}{2})}^{k} < R$

Metamath Proof Explorer

Theorem iscmet3lem3

Proof