Theorem heiborlem7

Description: Lemma for heibor . Since the sizes of the balls decrease exponentially, the sequence converges to zero. (Contributed by Jeff Madsen, 23-Jan-2014)

	Ref	Expression
Hypotheses	heibor.1	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
	heibor.3	⊢ 𝐾 = { 𝑢 ∣ ¬ ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑢 ⊆ ∪ 𝑣 }
	heibor.4	⊢ 𝐺 = { ⟨ 𝑦 , 𝑛 ⟩ ∣ ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑛 ) ∧ ( 𝑦 𝐵 𝑛 ) ∈ 𝐾 ) }
	heibor.5	⊢ 𝐵 = ( 𝑧 ∈ 𝑋 , 𝑚 ∈ ℕ0 ↦ ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) )
	heibor.6	⊢ ( 𝜑 → 𝐷 ∈ ( CMet ‘ 𝑋 ) )
	heibor.7	⊢ ( 𝜑 → 𝐹 : ℕ0 ⟶ ( 𝒫 𝑋 ∩ Fin ) )
	heibor.8	⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑛 ) ( 𝑦 𝐵 𝑛 ) )
	heibor.9	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐺 ( ( 𝑇 ‘ 𝑥 ) 𝐺 ( ( 2nd ‘ 𝑥 ) + 1 ) ∧ ( ( 𝐵 ‘ 𝑥 ) ∩ ( ( 𝑇 ‘ 𝑥 ) 𝐵 ( ( 2nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ) )
	heibor.10	⊢ ( 𝜑 → 𝐶 𝐺 0 )
	heibor.11	⊢ 𝑆 = seq 0 ( 𝑇 , ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) )
	heibor.12	⊢ 𝑀 = ( 𝑛 ∈ ℕ ↦ ⟨ ( 𝑆 ‘ 𝑛 ) , ( 3 / ( 2 ↑ 𝑛 ) ) ⟩ )
Assertion	heiborlem7	⊢ ∀ 𝑟 ∈ ℝ+ ∃ 𝑘 ∈ ℕ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < 𝑟

Proof

Step	Hyp	Ref	Expression
1		heibor.1	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2		heibor.3	⊢ 𝐾 = { 𝑢 ∣ ¬ ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑢 ⊆ ∪ 𝑣 }
3		heibor.4	⊢ 𝐺 = { ⟨ 𝑦 , 𝑛 ⟩ ∣ ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑛 ) ∧ ( 𝑦 𝐵 𝑛 ) ∈ 𝐾 ) }
4		heibor.5	⊢ 𝐵 = ( 𝑧 ∈ 𝑋 , 𝑚 ∈ ℕ0 ↦ ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) )
5		heibor.6	⊢ ( 𝜑 → 𝐷 ∈ ( CMet ‘ 𝑋 ) )
6		heibor.7	⊢ ( 𝜑 → 𝐹 : ℕ0 ⟶ ( 𝒫 𝑋 ∩ Fin ) )
7		heibor.8	⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑛 ) ( 𝑦 𝐵 𝑛 ) )
8		heibor.9	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐺 ( ( 𝑇 ‘ 𝑥 ) 𝐺 ( ( 2nd ‘ 𝑥 ) + 1 ) ∧ ( ( 𝐵 ‘ 𝑥 ) ∩ ( ( 𝑇 ‘ 𝑥 ) 𝐵 ( ( 2nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ) )
9		heibor.10	⊢ ( 𝜑 → 𝐶 𝐺 0 )
10		heibor.11	⊢ 𝑆 = seq 0 ( 𝑇 , ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) )
11		heibor.12	⊢ 𝑀 = ( 𝑛 ∈ ℕ ↦ ⟨ ( 𝑆 ‘ 𝑛 ) , ( 3 / ( 2 ↑ 𝑛 ) ) ⟩ )
12		3re	⊢ 3 ∈ ℝ
13		3pos	⊢ 0 < 3
14	12 13	elrpii	⊢ 3 ∈ ℝ+
15		rpdivcl	⊢ ( ( 𝑟 ∈ ℝ+ ∧ 3 ∈ ℝ+ ) → ( 𝑟 / 3 ) ∈ ℝ+ )
16	14 15	mpan2	⊢ ( 𝑟 ∈ ℝ+ → ( 𝑟 / 3 ) ∈ ℝ+ )
17		2re	⊢ 2 ∈ ℝ
18		1lt2	⊢ 1 < 2
19		expnlbnd	⊢ ( ( ( 𝑟 / 3 ) ∈ ℝ+ ∧ 2 ∈ ℝ ∧ 1 < 2 ) → ∃ 𝑘 ∈ ℕ ( 1 / ( 2 ↑ 𝑘 ) ) < ( 𝑟 / 3 ) )
20	17 18 19	mp3an23	⊢ ( ( 𝑟 / 3 ) ∈ ℝ+ → ∃ 𝑘 ∈ ℕ ( 1 / ( 2 ↑ 𝑘 ) ) < ( 𝑟 / 3 ) )
21	16 20	syl	⊢ ( 𝑟 ∈ ℝ+ → ∃ 𝑘 ∈ ℕ ( 1 / ( 2 ↑ 𝑘 ) ) < ( 𝑟 / 3 ) )
22		2nn	⊢ 2 ∈ ℕ
23		nnnn0	⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℕ0 )
24		nnexpcl	⊢ ( ( 2 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( 2 ↑ 𝑘 ) ∈ ℕ )
25	22 23 24	sylancr	⊢ ( 𝑘 ∈ ℕ → ( 2 ↑ 𝑘 ) ∈ ℕ )
26	25	nnrpd	⊢ ( 𝑘 ∈ ℕ → ( 2 ↑ 𝑘 ) ∈ ℝ+ )
27		rpcn	⊢ ( ( 2 ↑ 𝑘 ) ∈ ℝ+ → ( 2 ↑ 𝑘 ) ∈ ℂ )
28		rpne0	⊢ ( ( 2 ↑ 𝑘 ) ∈ ℝ+ → ( 2 ↑ 𝑘 ) ≠ 0 )
29		3cn	⊢ 3 ∈ ℂ
30		divrec	⊢ ( ( 3 ∈ ℂ ∧ ( 2 ↑ 𝑘 ) ∈ ℂ ∧ ( 2 ↑ 𝑘 ) ≠ 0 ) → ( 3 / ( 2 ↑ 𝑘 ) ) = ( 3 · ( 1 / ( 2 ↑ 𝑘 ) ) ) )
31	29 30	mp3an1	⊢ ( ( ( 2 ↑ 𝑘 ) ∈ ℂ ∧ ( 2 ↑ 𝑘 ) ≠ 0 ) → ( 3 / ( 2 ↑ 𝑘 ) ) = ( 3 · ( 1 / ( 2 ↑ 𝑘 ) ) ) )
32	27 28 31	syl2anc	⊢ ( ( 2 ↑ 𝑘 ) ∈ ℝ+ → ( 3 / ( 2 ↑ 𝑘 ) ) = ( 3 · ( 1 / ( 2 ↑ 𝑘 ) ) ) )
33	26 32	syl	⊢ ( 𝑘 ∈ ℕ → ( 3 / ( 2 ↑ 𝑘 ) ) = ( 3 · ( 1 / ( 2 ↑ 𝑘 ) ) ) )
34	33	adantl	⊢ ( ( 𝑟 ∈ ℝ+ ∧ 𝑘 ∈ ℕ ) → ( 3 / ( 2 ↑ 𝑘 ) ) = ( 3 · ( 1 / ( 2 ↑ 𝑘 ) ) ) )
35	34	breq1d	⊢ ( ( 𝑟 ∈ ℝ+ ∧ 𝑘 ∈ ℕ ) → ( ( 3 / ( 2 ↑ 𝑘 ) ) < 𝑟 ↔ ( 3 · ( 1 / ( 2 ↑ 𝑘 ) ) ) < 𝑟 ) )
36	25	nnrecred	⊢ ( 𝑘 ∈ ℕ → ( 1 / ( 2 ↑ 𝑘 ) ) ∈ ℝ )
37		rpre	⊢ ( 𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ )
38	12 13	pm3.2i	⊢ ( 3 ∈ ℝ ∧ 0 < 3 )
39		ltmuldiv2	⊢ ( ( ( 1 / ( 2 ↑ 𝑘 ) ) ∈ ℝ ∧ 𝑟 ∈ ℝ ∧ ( 3 ∈ ℝ ∧ 0 < 3 ) ) → ( ( 3 · ( 1 / ( 2 ↑ 𝑘 ) ) ) < 𝑟 ↔ ( 1 / ( 2 ↑ 𝑘 ) ) < ( 𝑟 / 3 ) ) )
40	38 39	mp3an3	⊢ ( ( ( 1 / ( 2 ↑ 𝑘 ) ) ∈ ℝ ∧ 𝑟 ∈ ℝ ) → ( ( 3 · ( 1 / ( 2 ↑ 𝑘 ) ) ) < 𝑟 ↔ ( 1 / ( 2 ↑ 𝑘 ) ) < ( 𝑟 / 3 ) ) )
41	36 37 40	syl2anr	⊢ ( ( 𝑟 ∈ ℝ+ ∧ 𝑘 ∈ ℕ ) → ( ( 3 · ( 1 / ( 2 ↑ 𝑘 ) ) ) < 𝑟 ↔ ( 1 / ( 2 ↑ 𝑘 ) ) < ( 𝑟 / 3 ) ) )
42	35 41	bitrd	⊢ ( ( 𝑟 ∈ ℝ+ ∧ 𝑘 ∈ ℕ ) → ( ( 3 / ( 2 ↑ 𝑘 ) ) < 𝑟 ↔ ( 1 / ( 2 ↑ 𝑘 ) ) < ( 𝑟 / 3 ) ) )
43	42	rexbidva	⊢ ( 𝑟 ∈ ℝ+ → ( ∃ 𝑘 ∈ ℕ ( 3 / ( 2 ↑ 𝑘 ) ) < 𝑟 ↔ ∃ 𝑘 ∈ ℕ ( 1 / ( 2 ↑ 𝑘 ) ) < ( 𝑟 / 3 ) ) )
44	21 43	mpbird	⊢ ( 𝑟 ∈ ℝ+ → ∃ 𝑘 ∈ ℕ ( 3 / ( 2 ↑ 𝑘 ) ) < 𝑟 )
45		fveq2	⊢ ( 𝑛 = 𝑘 → ( 𝑆 ‘ 𝑛 ) = ( 𝑆 ‘ 𝑘 ) )
46		oveq2	⊢ ( 𝑛 = 𝑘 → ( 2 ↑ 𝑛 ) = ( 2 ↑ 𝑘 ) )
47	46	oveq2d	⊢ ( 𝑛 = 𝑘 → ( 3 / ( 2 ↑ 𝑛 ) ) = ( 3 / ( 2 ↑ 𝑘 ) ) )
48	45 47	opeq12d	⊢ ( 𝑛 = 𝑘 → ⟨ ( 𝑆 ‘ 𝑛 ) , ( 3 / ( 2 ↑ 𝑛 ) ) ⟩ = ⟨ ( 𝑆 ‘ 𝑘 ) , ( 3 / ( 2 ↑ 𝑘 ) ) ⟩ )
49		opex	⊢ ⟨ ( 𝑆 ‘ 𝑘 ) , ( 3 / ( 2 ↑ 𝑘 ) ) ⟩ ∈ V
50	48 11 49	fvmpt	⊢ ( 𝑘 ∈ ℕ → ( 𝑀 ‘ 𝑘 ) = ⟨ ( 𝑆 ‘ 𝑘 ) , ( 3 / ( 2 ↑ 𝑘 ) ) ⟩ )
51	50	fveq2d	⊢ ( 𝑘 ∈ ℕ → ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) = ( 2nd ‘ ⟨ ( 𝑆 ‘ 𝑘 ) , ( 3 / ( 2 ↑ 𝑘 ) ) ⟩ ) )
52		fvex	⊢ ( 𝑆 ‘ 𝑘 ) ∈ V
53		ovex	⊢ ( 3 / ( 2 ↑ 𝑘 ) ) ∈ V
54	52 53	op2nd	⊢ ( 2nd ‘ ⟨ ( 𝑆 ‘ 𝑘 ) , ( 3 / ( 2 ↑ 𝑘 ) ) ⟩ ) = ( 3 / ( 2 ↑ 𝑘 ) )
55	51 54	eqtrdi	⊢ ( 𝑘 ∈ ℕ → ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) = ( 3 / ( 2 ↑ 𝑘 ) ) )
56	55	breq1d	⊢ ( 𝑘 ∈ ℕ → ( ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < 𝑟 ↔ ( 3 / ( 2 ↑ 𝑘 ) ) < 𝑟 ) )
57	56	rexbiia	⊢ ( ∃ 𝑘 ∈ ℕ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < 𝑟 ↔ ∃ 𝑘 ∈ ℕ ( 3 / ( 2 ↑ 𝑘 ) ) < 𝑟 )
58	44 57	sylibr	⊢ ( 𝑟 ∈ ℝ+ → ∃ 𝑘 ∈ ℕ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < 𝑟 )
59	58	rgen	⊢ ∀ 𝑟 ∈ ℝ+ ∃ 𝑘 ∈ ℕ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < 𝑟