Theorem iscmet3lem3 23367

Description: Lemma for iscmet3 23370. (Contributed by Mario Carneiro, 15-Oct-2015.)

Hypothesis

Ref	Expression
iscmet3.1	⊢ 𝑍 = (ℤ≥‘𝑀)

Assertion

Ref	Expression
iscmet3lem3	⊢ ((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((1 / 2)↑𝑘) < 𝑅)

Distinct variable groups:   𝑗,𝑘,𝑅   𝑗,𝑍,𝑘   𝑗,𝑀,𝑘

Proof of Theorem iscmet3lem3

Dummy variable 𝑛 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		iscmet3.1	. . 3 ⊢ 𝑍 = (ℤ≥‘𝑀)
2		simpl 474	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+) → 𝑀 ∈ ℤ)
3		simpr 477	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+) → 𝑅 ∈ ℝ+)
4		eluzelz 11896	. . . . . 6 ⊢ (𝑘 ∈ (ℤ≥‘𝑀) → 𝑘 ∈ ℤ)
5	4, 1	eleq2s 2862	. . . . 5 ⊢ (𝑘 ∈ 𝑍 → 𝑘 ∈ ℤ)
6	5	adantl 473	. . . 4 ⊢ (((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+) ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ ℤ)
7		oveq2 6850	. . . . 5 ⊢ (𝑛 = 𝑘 → ((1 / 2)↑𝑛) = ((1 / 2)↑𝑘))
8		eqid 2765	. . . . 5 ⊢ (𝑛 ∈ ℤ ↦ ((1 / 2)↑𝑛)) = (𝑛 ∈ ℤ ↦ ((1 / 2)↑𝑛))
9		ovex 6874	. . . . 5 ⊢ ((1 / 2)↑𝑘) ∈ V
10	7, 8, 9	fvmpt 6471	. . . 4 ⊢ (𝑘 ∈ ℤ → ((𝑛 ∈ ℤ ↦ ((1 / 2)↑𝑛))‘𝑘) = ((1 / 2)↑𝑘))
11	6, 10	syl 17	. . 3 ⊢ (((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+) ∧ 𝑘 ∈ 𝑍) → ((𝑛 ∈ ℤ ↦ ((1 / 2)↑𝑛))‘𝑘) = ((1 / 2)↑𝑘))
12		nn0uz 11922	. . . . . . 7 ⊢ ℕ0 = (ℤ≥‘0)
13	12	reseq2i 5562	. . . . . 6 ⊢ ((𝑛 ∈ ℤ ↦ ((1 / 2)↑𝑛)) ↾ ℕ0) = ((𝑛 ∈ ℤ ↦ ((1 / 2)↑𝑛)) ↾ (ℤ≥‘0))
14		nn0ssz 11645	. . . . . . 7 ⊢ ℕ0 ⊆ ℤ
15		resmpt 5626	. . . . . . 7 ⊢ (ℕ0 ⊆ ℤ → ((𝑛 ∈ ℤ ↦ ((1 / 2)↑𝑛)) ↾ ℕ0) = (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛)))
16	14, 15	ax-mp 5	. . . . . 6 ⊢ ((𝑛 ∈ ℤ ↦ ((1 / 2)↑𝑛)) ↾ ℕ0) = (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))
17	13, 16	eqtr3i 2789	. . . . 5 ⊢ ((𝑛 ∈ ℤ ↦ ((1 / 2)↑𝑛)) ↾ (ℤ≥‘0)) = (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))
18		halfcn 11493	. . . . . . 7 ⊢ (1 / 2) ∈ ℂ
19	18	a1i 11	. . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+) → (1 / 2) ∈ ℂ)
20		halfre 11492	. . . . . . . . 9 ⊢ (1 / 2) ∈ ℝ
21		1rp 12032	. . . . . . . . . . 11 ⊢ 1 ∈ ℝ+
22		rphalfcl 12056	. . . . . . . . . . 11 ⊢ (1 ∈ ℝ+ → (1 / 2) ∈ ℝ+)
23	21, 22	ax-mp 5	. . . . . . . . . 10 ⊢ (1 / 2) ∈ ℝ+
24		rpge0 12043	. . . . . . . . . 10 ⊢ ((1 / 2) ∈ ℝ+ → 0 ≤ (1 / 2))
25	23, 24	ax-mp 5	. . . . . . . . 9 ⊢ 0 ≤ (1 / 2)
26		absid 14321	. . . . . . . . 9 ⊢ (((1 / 2) ∈ ℝ ∧ 0 ≤ (1 / 2)) → (abs‘(1 / 2)) = (1 / 2))
27	20, 25, 26	mp2an 683	. . . . . . . 8 ⊢ (abs‘(1 / 2)) = (1 / 2)
28		halflt1 11496	. . . . . . . 8 ⊢ (1 / 2) < 1
29	27, 28	eqbrtri 4830	. . . . . . 7 ⊢ (abs‘(1 / 2)) < 1
30	29	a1i 11	. . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+) → (abs‘(1 / 2)) < 1)
31	19, 30	expcnv 14880	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+) → (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛)) ⇝ 0)
32	17, 31	syl5eqbr 4844	. . . 4 ⊢ ((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+) → ((𝑛 ∈ ℤ ↦ ((1 / 2)↑𝑛)) ↾ (ℤ≥‘0)) ⇝ 0)
33		0z 11635	. . . . 5 ⊢ 0 ∈ ℤ
34		zex 11633	. . . . . . 7 ⊢ ℤ ∈ V
35	34	mptex 6679	. . . . . 6 ⊢ (𝑛 ∈ ℤ ↦ ((1 / 2)↑𝑛)) ∈ V
36	35	a1i 11	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+) → (𝑛 ∈ ℤ ↦ ((1 / 2)↑𝑛)) ∈ V)
37		climres 14591	. . . . 5 ⊢ ((0 ∈ ℤ ∧ (𝑛 ∈ ℤ ↦ ((1 / 2)↑𝑛)) ∈ V) → (((𝑛 ∈ ℤ ↦ ((1 / 2)↑𝑛)) ↾ (ℤ≥‘0)) ⇝ 0 ↔ (𝑛 ∈ ℤ ↦ ((1 / 2)↑𝑛)) ⇝ 0))
38	33, 36, 37	sylancr 581	. . . 4 ⊢ ((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+) → (((𝑛 ∈ ℤ ↦ ((1 / 2)↑𝑛)) ↾ (ℤ≥‘0)) ⇝ 0 ↔ (𝑛 ∈ ℤ ↦ ((1 / 2)↑𝑛)) ⇝ 0))
39	32, 38	mpbid 223	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+) → (𝑛 ∈ ℤ ↦ ((1 / 2)↑𝑛)) ⇝ 0)
40	1, 2, 3, 11, 39	climi0 14528	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((1 / 2)↑𝑘)) < 𝑅)
41	1	uztrn2 11904	. . . . . 6 ⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ 𝑍)
42		rpexpcl 13086	. . . . . . . . 9 ⊢ (((1 / 2) ∈ ℝ+ ∧ 𝑘 ∈ ℤ) → ((1 / 2)↑𝑘) ∈ ℝ+)
43	23, 6, 42	sylancr 581	. . . . . . . 8 ⊢ (((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+) ∧ 𝑘 ∈ 𝑍) → ((1 / 2)↑𝑘) ∈ ℝ+)
44		rpre 12036	. . . . . . . . 9 ⊢ (((1 / 2)↑𝑘) ∈ ℝ+ → ((1 / 2)↑𝑘) ∈ ℝ)
45		rpge0 12043	. . . . . . . . 9 ⊢ (((1 / 2)↑𝑘) ∈ ℝ+ → 0 ≤ ((1 / 2)↑𝑘))
46	44, 45	absidd 14446	. . . . . . . 8 ⊢ (((1 / 2)↑𝑘) ∈ ℝ+ → (abs‘((1 / 2)↑𝑘)) = ((1 / 2)↑𝑘))
47	43, 46	syl 17	. . . . . . 7 ⊢ (((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+) ∧ 𝑘 ∈ 𝑍) → (abs‘((1 / 2)↑𝑘)) = ((1 / 2)↑𝑘))
48	47	breq1d 4819	. . . . . 6 ⊢ (((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+) ∧ 𝑘 ∈ 𝑍) → ((abs‘((1 / 2)↑𝑘)) < 𝑅 ↔ ((1 / 2)↑𝑘) < 𝑅))
49	41, 48	sylan2 586	. . . . 5 ⊢ (((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → ((abs‘((1 / 2)↑𝑘)) < 𝑅 ↔ ((1 / 2)↑𝑘) < 𝑅))
50	49	anassrs 459	. . . 4 ⊢ ((((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((abs‘((1 / 2)↑𝑘)) < 𝑅 ↔ ((1 / 2)↑𝑘) < 𝑅))
51	50	ralbidva 3132	. . 3 ⊢ (((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) → (∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((1 / 2)↑𝑘)) < 𝑅 ↔ ∀𝑘 ∈ (ℤ≥‘𝑗)((1 / 2)↑𝑘) < 𝑅))
52	51	rexbidva 3196	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+) → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((1 / 2)↑𝑘)) < 𝑅 ↔ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((1 / 2)↑𝑘) < 𝑅))
53	40, 52	mpbid 223	1 ⊢ ((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((1 / 2)↑𝑘) < 𝑅)

Syntax hints:   → wi 4   ↔ wb 197   ∧ wa 384   = wceq 1652   ∈ wcel 2155  ∀wral 3055  ∃wrex 3056  Vcvv 3350   ⊆ wss 3732   class class class wbr 4809   ↦ cmpt 4888   ↾ cres 5279  ‘cfv 6068  (class class class)co 6842  ℂcc 10187  ℝcr 10188  0cc0 10189  1c1 10190   < clt 10328   ≤ cle 10329   / cdiv 10938  2c2 11327  ℕ₀cn0 11538  ℤcz 11624  ℤ_≥cuz 11886  ℝ⁺crp 12028  ↑cexp 13067  abscabs 14259   ⇝ cli 14500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266  ax-pre-sup 10267

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-om 7264  df-2nd 7367  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-er 7947  df-pm 8063  df-en 8161  df-dom 8162  df-sdom 8163  df-sup 8555  df-inf 8556  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-div 10939  df-nn 11275  df-2 11335  df-3 11336  df-n0 11539  df-z 11625  df-uz 11887  df-rp 12029  df-fl 12801  df-seq 13009  df-exp 13068  df-cj 14124  df-re 14125  df-im 14126  df-sqrt 14260  df-abs 14261  df-clim 14504  df-rlim 14505

This theorem is referenced by:  iscmet3lem1  23368  iscmet3lem2  23369