Mathbox for Jeff Madsen < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  heiborlem6 Structured version   Visualization version   GIF version

Theorem heiborlem6 32785
 Description: Lemma for heibor 32790. Since the sequence of balls connected by the function 𝑇 ensures that each ball nontrivially intersects with the next (since the empty set has a finite subcover, the intersection of any two successive balls in the sequence is nonempty), and each ball is half the size of the previous one, the distance between the centers is at most 3 / 2 times the size of the larger, and so if we expand each ball by a factor of 3 we get a nested sequence of balls. (Contributed by Jeff Madsen, 23-Jan-2014.)
Hypotheses
Ref Expression
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 𝑆 = seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))
heibor.12 𝑀 = (𝑛 ∈ ℕ ↦ ⟨(𝑆𝑛), (3 / (2↑𝑛))⟩)
Assertion
Ref Expression
heiborlem6 (𝜑 → ∀𝑘 ∈ ℕ ((ball‘𝐷)‘(𝑀‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝑀𝑘)))
Distinct variable groups:   𝑥,𝑛,𝑦,𝑘,𝑢,𝐹   𝑘,𝐺,𝑥   𝜑,𝑘,𝑥   𝑘,𝑚,𝑣,𝑧,𝐷,𝑛,𝑢,𝑥,𝑦   𝑘,𝑀,𝑚,𝑢,𝑥,𝑦,𝑧   𝑇,𝑚,𝑛,𝑥,𝑦,𝑧   𝐵,𝑛,𝑢,𝑣,𝑦   𝑘,𝐽,𝑚,𝑛,𝑢,𝑣,𝑥,𝑦,𝑧   𝑈,𝑛,𝑢,𝑣,𝑥,𝑦,𝑧   𝑆,𝑘,𝑚,𝑛,𝑢,𝑣,𝑥,𝑦,𝑧   𝑘,𝑋,𝑚,𝑛,𝑢,𝑣,𝑥,𝑦,𝑧   𝐶,𝑚,𝑛,𝑢,𝑣,𝑦   𝑛,𝐾,𝑥,𝑦,𝑧   𝑥,𝐵
Allowed substitution hints:   𝜑(𝑦,𝑧,𝑣,𝑢,𝑚,𝑛)   𝐵(𝑧,𝑘,𝑚)   𝐶(𝑥,𝑧,𝑘)   𝑇(𝑣,𝑢,𝑘)   𝑈(𝑘,𝑚)   𝐹(𝑧,𝑣,𝑚)   𝐺(𝑦,𝑧,𝑣,𝑢,𝑚,𝑛)   𝐾(𝑣,𝑢,𝑘,𝑚)   𝑀(𝑣,𝑛)

Proof of Theorem heiborlem6
StepHypRef Expression
1 nnnn0 11176 . . . 4 (𝑘 ∈ ℕ → 𝑘 ∈ ℕ0)
2 heibor.6 . . . . . . . 8 (𝜑𝐷 ∈ (CMet‘𝑋))
3 cmetmet 22892 . . . . . . . 8 (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋))
42, 3syl 17 . . . . . . 7 (𝜑𝐷 ∈ (Met‘𝑋))
5 metxmet 21949 . . . . . . 7 (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋))
64, 5syl 17 . . . . . 6 (𝜑𝐷 ∈ (∞Met‘𝑋))
76adantr 480 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → 𝐷 ∈ (∞Met‘𝑋))
8 heibor.7 . . . . . . . . 9 (𝜑𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin))
9 inss1 3795 . . . . . . . . 9 (𝒫 𝑋 ∩ Fin) ⊆ 𝒫 𝑋
10 fss 5969 . . . . . . . . 9 ((𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin) ∧ (𝒫 𝑋 ∩ Fin) ⊆ 𝒫 𝑋) → 𝐹:ℕ0⟶𝒫 𝑋)
118, 9, 10sylancl 693 . . . . . . . 8 (𝜑𝐹:ℕ0⟶𝒫 𝑋)
12 peano2nn0 11210 . . . . . . . 8 (𝑘 ∈ ℕ0 → (𝑘 + 1) ∈ ℕ0)
13 ffvelrn 6265 . . . . . . . 8 ((𝐹:ℕ0⟶𝒫 𝑋 ∧ (𝑘 + 1) ∈ ℕ0) → (𝐹‘(𝑘 + 1)) ∈ 𝒫 𝑋)
1411, 12, 13syl2an 493 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (𝐹‘(𝑘 + 1)) ∈ 𝒫 𝑋)
1514elpwid 4118 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (𝐹‘(𝑘 + 1)) ⊆ 𝑋)
16 heibor.1 . . . . . . . . 9 𝐽 = (MetOpen‘𝐷)
17 heibor.3 . . . . . . . . 9 𝐾 = {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 𝑣}
18 heibor.4 . . . . . . . . 9 𝐺 = {⟨𝑦, 𝑛⟩ ∣ (𝑛 ∈ ℕ0𝑦 ∈ (𝐹𝑛) ∧ (𝑦𝐵𝑛) ∈ 𝐾)}
19 heibor.5 . . . . . . . . 9 𝐵 = (𝑧𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))
20 heibor.8 . . . . . . . . 9 (𝜑 → ∀𝑛 ∈ ℕ0 𝑋 = 𝑦 ∈ (𝐹𝑛)(𝑦𝐵𝑛))
21 heibor.9 . . . . . . . . 9 (𝜑 → ∀𝑥𝐺 ((𝑇𝑥)𝐺((2nd𝑥) + 1) ∧ ((𝐵𝑥) ∩ ((𝑇𝑥)𝐵((2nd𝑥) + 1))) ∈ 𝐾))
22 heibor.10 . . . . . . . . 9 (𝜑𝐶𝐺0)
23 heibor.11 . . . . . . . . 9 𝑆 = seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))
2416, 17, 18, 19, 2, 8, 20, 21, 22, 23heiborlem4 32783 . . . . . . . 8 ((𝜑 ∧ (𝑘 + 1) ∈ ℕ0) → (𝑆‘(𝑘 + 1))𝐺(𝑘 + 1))
2512, 24sylan2 490 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (𝑆‘(𝑘 + 1))𝐺(𝑘 + 1))
26 fvex 6113 . . . . . . . . 9 (𝑆‘(𝑘 + 1)) ∈ V
27 ovex 6577 . . . . . . . . 9 (𝑘 + 1) ∈ V
2816, 17, 18, 26, 27heiborlem2 32781 . . . . . . . 8 ((𝑆‘(𝑘 + 1))𝐺(𝑘 + 1) ↔ ((𝑘 + 1) ∈ ℕ0 ∧ (𝑆‘(𝑘 + 1)) ∈ (𝐹‘(𝑘 + 1)) ∧ ((𝑆‘(𝑘 + 1))𝐵(𝑘 + 1)) ∈ 𝐾))
2928simp2bi 1070 . . . . . . 7 ((𝑆‘(𝑘 + 1))𝐺(𝑘 + 1) → (𝑆‘(𝑘 + 1)) ∈ (𝐹‘(𝑘 + 1)))
3025, 29syl 17 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (𝑆‘(𝑘 + 1)) ∈ (𝐹‘(𝑘 + 1)))
3115, 30sseldd 3569 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → (𝑆‘(𝑘 + 1)) ∈ 𝑋)
3211ffvelrnda 6267 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (𝐹𝑘) ∈ 𝒫 𝑋)
3332elpwid 4118 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (𝐹𝑘) ⊆ 𝑋)
3416, 17, 18, 19, 2, 8, 20, 21, 22, 23heiborlem4 32783 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (𝑆𝑘)𝐺𝑘)
35 fvex 6113 . . . . . . . . 9 (𝑆𝑘) ∈ V
36 vex 3176 . . . . . . . . 9 𝑘 ∈ V
3716, 17, 18, 35, 36heiborlem2 32781 . . . . . . . 8 ((𝑆𝑘)𝐺𝑘 ↔ (𝑘 ∈ ℕ0 ∧ (𝑆𝑘) ∈ (𝐹𝑘) ∧ ((𝑆𝑘)𝐵𝑘) ∈ 𝐾))
3837simp2bi 1070 . . . . . . 7 ((𝑆𝑘)𝐺𝑘 → (𝑆𝑘) ∈ (𝐹𝑘))
3934, 38syl 17 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (𝑆𝑘) ∈ (𝐹𝑘))
4033, 39sseldd 3569 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → (𝑆𝑘) ∈ 𝑋)
41 3re 10971 . . . . . 6 3 ∈ ℝ
42 2nn 11062 . . . . . . . . 9 2 ∈ ℕ
43 nnexpcl 12735 . . . . . . . . 9 ((2 ∈ ℕ ∧ (𝑘 + 1) ∈ ℕ0) → (2↑(𝑘 + 1)) ∈ ℕ)
4442, 12, 43sylancr 694 . . . . . . . 8 (𝑘 ∈ ℕ0 → (2↑(𝑘 + 1)) ∈ ℕ)
4544nnrpd 11746 . . . . . . 7 (𝑘 ∈ ℕ0 → (2↑(𝑘 + 1)) ∈ ℝ+)
4645adantl 481 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (2↑(𝑘 + 1)) ∈ ℝ+)
47 rerpdivcl 11737 . . . . . 6 ((3 ∈ ℝ ∧ (2↑(𝑘 + 1)) ∈ ℝ+) → (3 / (2↑(𝑘 + 1))) ∈ ℝ)
4841, 46, 47sylancr 694 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → (3 / (2↑(𝑘 + 1))) ∈ ℝ)
49 nnexpcl 12735 . . . . . . . . 9 ((2 ∈ ℕ ∧ 𝑘 ∈ ℕ0) → (2↑𝑘) ∈ ℕ)
5042, 49mpan 702 . . . . . . . 8 (𝑘 ∈ ℕ0 → (2↑𝑘) ∈ ℕ)
5150nnrpd 11746 . . . . . . 7 (𝑘 ∈ ℕ0 → (2↑𝑘) ∈ ℝ+)
5251adantl 481 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (2↑𝑘) ∈ ℝ+)
53 rerpdivcl 11737 . . . . . 6 ((3 ∈ ℝ ∧ (2↑𝑘) ∈ ℝ+) → (3 / (2↑𝑘)) ∈ ℝ)
5441, 52, 53sylancr 694 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → (3 / (2↑𝑘)) ∈ ℝ)
55 oveq1 6556 . . . . . . . . . . . 12 (𝑧 = (𝑆𝑘) → (𝑧(ball‘𝐷)(1 / (2↑𝑚))) = ((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑚))))
56 oveq2 6557 . . . . . . . . . . . . . 14 (𝑚 = 𝑘 → (2↑𝑚) = (2↑𝑘))
5756oveq2d 6565 . . . . . . . . . . . . 13 (𝑚 = 𝑘 → (1 / (2↑𝑚)) = (1 / (2↑𝑘)))
5857oveq2d 6565 . . . . . . . . . . . 12 (𝑚 = 𝑘 → ((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑚))) = ((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑘))))
59 ovex 6577 . . . . . . . . . . . 12 ((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∈ V
6055, 58, 19, 59ovmpt2 6694 . . . . . . . . . . 11 (((𝑆𝑘) ∈ 𝑋𝑘 ∈ ℕ0) → ((𝑆𝑘)𝐵𝑘) = ((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑘))))
6140, 60sylancom 698 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → ((𝑆𝑘)𝐵𝑘) = ((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑘))))
62 df-br 4584 . . . . . . . . . . . . . . . . 17 ((𝑆𝑘)𝐺𝑘 ↔ ⟨(𝑆𝑘), 𝑘⟩ ∈ 𝐺)
63 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = ⟨(𝑆𝑘), 𝑘⟩ → (𝑇𝑥) = (𝑇‘⟨(𝑆𝑘), 𝑘⟩))
64 df-ov 6552 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑆𝑘)𝑇𝑘) = (𝑇‘⟨(𝑆𝑘), 𝑘⟩)
6563, 64syl6eqr 2662 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = ⟨(𝑆𝑘), 𝑘⟩ → (𝑇𝑥) = ((𝑆𝑘)𝑇𝑘))
6635, 36op2ndd 7070 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = ⟨(𝑆𝑘), 𝑘⟩ → (2nd𝑥) = 𝑘)
6766oveq1d 6564 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = ⟨(𝑆𝑘), 𝑘⟩ → ((2nd𝑥) + 1) = (𝑘 + 1))
6865, 67breq12d 4596 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = ⟨(𝑆𝑘), 𝑘⟩ → ((𝑇𝑥)𝐺((2nd𝑥) + 1) ↔ ((𝑆𝑘)𝑇𝑘)𝐺(𝑘 + 1)))
69 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = ⟨(𝑆𝑘), 𝑘⟩ → (𝐵𝑥) = (𝐵‘⟨(𝑆𝑘), 𝑘⟩))
70 df-ov 6552 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑆𝑘)𝐵𝑘) = (𝐵‘⟨(𝑆𝑘), 𝑘⟩)
7169, 70syl6eqr 2662 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = ⟨(𝑆𝑘), 𝑘⟩ → (𝐵𝑥) = ((𝑆𝑘)𝐵𝑘))
7265, 67oveq12d 6567 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = ⟨(𝑆𝑘), 𝑘⟩ → ((𝑇𝑥)𝐵((2nd𝑥) + 1)) = (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1)))
7371, 72ineq12d 3777 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = ⟨(𝑆𝑘), 𝑘⟩ → ((𝐵𝑥) ∩ ((𝑇𝑥)𝐵((2nd𝑥) + 1))) = (((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))))
7473eleq1d 2672 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = ⟨(𝑆𝑘), 𝑘⟩ → (((𝐵𝑥) ∩ ((𝑇𝑥)𝐵((2nd𝑥) + 1))) ∈ 𝐾 ↔ (((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾))
7568, 74anbi12d 743 . . . . . . . . . . . . . . . . . . 19 (𝑥 = ⟨(𝑆𝑘), 𝑘⟩ → (((𝑇𝑥)𝐺((2nd𝑥) + 1) ∧ ((𝐵𝑥) ∩ ((𝑇𝑥)𝐵((2nd𝑥) + 1))) ∈ 𝐾) ↔ (((𝑆𝑘)𝑇𝑘)𝐺(𝑘 + 1) ∧ (((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾)))
7675rspccv 3279 . . . . . . . . . . . . . . . . . 18 (∀𝑥𝐺 ((𝑇𝑥)𝐺((2nd𝑥) + 1) ∧ ((𝐵𝑥) ∩ ((𝑇𝑥)𝐵((2nd𝑥) + 1))) ∈ 𝐾) → (⟨(𝑆𝑘), 𝑘⟩ ∈ 𝐺 → (((𝑆𝑘)𝑇𝑘)𝐺(𝑘 + 1) ∧ (((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾)))
7721, 76syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (⟨(𝑆𝑘), 𝑘⟩ ∈ 𝐺 → (((𝑆𝑘)𝑇𝑘)𝐺(𝑘 + 1) ∧ (((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾)))
7862, 77syl5bi 231 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑆𝑘)𝐺𝑘 → (((𝑆𝑘)𝑇𝑘)𝐺(𝑘 + 1) ∧ (((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾)))
7978adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ℕ0) → ((𝑆𝑘)𝐺𝑘 → (((𝑆𝑘)𝑇𝑘)𝐺(𝑘 + 1) ∧ (((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾)))
8034, 79mpd 15 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ0) → (((𝑆𝑘)𝑇𝑘)𝐺(𝑘 + 1) ∧ (((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾))
8180simpld 474 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ0) → ((𝑆𝑘)𝑇𝑘)𝐺(𝑘 + 1))
82 ovex 6577 . . . . . . . . . . . . . . 15 ((𝑆𝑘)𝑇𝑘) ∈ V
8316, 17, 18, 82, 27heiborlem2 32781 . . . . . . . . . . . . . 14 (((𝑆𝑘)𝑇𝑘)𝐺(𝑘 + 1) ↔ ((𝑘 + 1) ∈ ℕ0 ∧ ((𝑆𝑘)𝑇𝑘) ∈ (𝐹‘(𝑘 + 1)) ∧ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1)) ∈ 𝐾))
8483simp2bi 1070 . . . . . . . . . . . . 13 (((𝑆𝑘)𝑇𝑘)𝐺(𝑘 + 1) → ((𝑆𝑘)𝑇𝑘) ∈ (𝐹‘(𝑘 + 1)))
8581, 84syl 17 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → ((𝑆𝑘)𝑇𝑘) ∈ (𝐹‘(𝑘 + 1)))
8615, 85sseldd 3569 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → ((𝑆𝑘)𝑇𝑘) ∈ 𝑋)
8712adantl 481 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → (𝑘 + 1) ∈ ℕ0)
88 oveq1 6556 . . . . . . . . . . . 12 (𝑧 = ((𝑆𝑘)𝑇𝑘) → (𝑧(ball‘𝐷)(1 / (2↑𝑚))) = (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑𝑚))))
89 oveq2 6557 . . . . . . . . . . . . . 14 (𝑚 = (𝑘 + 1) → (2↑𝑚) = (2↑(𝑘 + 1)))
9089oveq2d 6565 . . . . . . . . . . . . 13 (𝑚 = (𝑘 + 1) → (1 / (2↑𝑚)) = (1 / (2↑(𝑘 + 1))))
9190oveq2d 6565 . . . . . . . . . . . 12 (𝑚 = (𝑘 + 1) → (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑𝑚))) = (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1)))))
92 ovex 6577 . . . . . . . . . . . 12 (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1)))) ∈ V
9388, 91, 19, 92ovmpt2 6694 . . . . . . . . . . 11 ((((𝑆𝑘)𝑇𝑘) ∈ 𝑋 ∧ (𝑘 + 1) ∈ ℕ0) → (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1)) = (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1)))))
9486, 87, 93syl2anc 691 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1)) = (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1)))))
9561, 94ineq12d 3777 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → (((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))) = (((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))))
9680simprd 478 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → (((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾)
97 0elpw 4760 . . . . . . . . . . . . 13 ∅ ∈ 𝒫 𝑈
98 0fin 8073 . . . . . . . . . . . . 13 ∅ ∈ Fin
99 elin 3758 . . . . . . . . . . . . 13 (∅ ∈ (𝒫 𝑈 ∩ Fin) ↔ (∅ ∈ 𝒫 𝑈 ∧ ∅ ∈ Fin))
10097, 98, 99mpbir2an 957 . . . . . . . . . . . 12 ∅ ∈ (𝒫 𝑈 ∩ Fin)
101 0ss 3924 . . . . . . . . . . . 12 ∅ ⊆
102 unieq 4380 . . . . . . . . . . . . . 14 (𝑣 = ∅ → 𝑣 = ∅)
103102sseq2d 3596 . . . . . . . . . . . . 13 (𝑣 = ∅ → (∅ ⊆ 𝑣 ↔ ∅ ⊆ ∅))
104103rspcev 3282 . . . . . . . . . . . 12 ((∅ ∈ (𝒫 𝑈 ∩ Fin) ∧ ∅ ⊆ ∅) → ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ 𝑣)
105100, 101, 104mp2an 704 . . . . . . . . . . 11 𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ 𝑣
106 0ex 4718 . . . . . . . . . . . . 13 ∅ ∈ V
107 sseq1 3589 . . . . . . . . . . . . . . 15 (𝑢 = ∅ → (𝑢 𝑣 ↔ ∅ ⊆ 𝑣))
108107rexbidv 3034 . . . . . . . . . . . . . 14 (𝑢 = ∅ → (∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 𝑣 ↔ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ 𝑣))
109108notbid 307 . . . . . . . . . . . . 13 (𝑢 = ∅ → (¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 𝑣 ↔ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ 𝑣))
110106, 109, 17elab2 3323 . . . . . . . . . . . 12 (∅ ∈ 𝐾 ↔ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ 𝑣)
111110con2bii 346 . . . . . . . . . . 11 (∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ 𝑣 ↔ ¬ ∅ ∈ 𝐾)
112105, 111mpbi 219 . . . . . . . . . 10 ¬ ∅ ∈ 𝐾
113 nelne2 2879 . . . . . . . . . 10 (((((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾 ∧ ¬ ∅ ∈ 𝐾) → (((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ≠ ∅)
11496, 112, 113sylancl 693 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → (((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ≠ ∅)
11595, 114eqnetrrd 2850 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → (((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))) ≠ ∅)
11651rpreccld 11758 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ0 → (1 / (2↑𝑘)) ∈ ℝ+)
117116adantl 481 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ0) → (1 / (2↑𝑘)) ∈ ℝ+)
118117rpred 11748 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → (1 / (2↑𝑘)) ∈ ℝ)
11945rpreccld 11758 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ0 → (1 / (2↑(𝑘 + 1))) ∈ ℝ+)
120119adantl 481 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ0) → (1 / (2↑(𝑘 + 1))) ∈ ℝ+)
121120rpred 11748 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → (1 / (2↑(𝑘 + 1))) ∈ ℝ)
122 rexadd 11937 . . . . . . . . . . . 12 (((1 / (2↑𝑘)) ∈ ℝ ∧ (1 / (2↑(𝑘 + 1))) ∈ ℝ) → ((1 / (2↑𝑘)) +𝑒 (1 / (2↑(𝑘 + 1)))) = ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))))
123118, 121, 122syl2anc 691 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → ((1 / (2↑𝑘)) +𝑒 (1 / (2↑(𝑘 + 1)))) = ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))))
124123breq1d 4593 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → (((1 / (2↑𝑘)) +𝑒 (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)) ↔ ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘))))
125117rpxrd 11749 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → (1 / (2↑𝑘)) ∈ ℝ*)
126120rpxrd 11749 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → (1 / (2↑(𝑘 + 1))) ∈ ℝ*)
127 bldisj 22013 . . . . . . . . . . . . 13 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑆𝑘) ∈ 𝑋 ∧ ((𝑆𝑘)𝑇𝑘) ∈ 𝑋) ∧ ((1 / (2↑𝑘)) ∈ ℝ* ∧ (1 / (2↑(𝑘 + 1))) ∈ ℝ* ∧ ((1 / (2↑𝑘)) +𝑒 (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)))) → (((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))) = ∅)
1281273exp2 1277 . . . . . . . . . . . 12 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑆𝑘) ∈ 𝑋 ∧ ((𝑆𝑘)𝑇𝑘) ∈ 𝑋) → ((1 / (2↑𝑘)) ∈ ℝ* → ((1 / (2↑(𝑘 + 1))) ∈ ℝ* → (((1 / (2↑𝑘)) +𝑒 (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)) → (((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))) = ∅))))
129128imp32 448 . . . . . . . . . . 11 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑆𝑘) ∈ 𝑋 ∧ ((𝑆𝑘)𝑇𝑘) ∈ 𝑋) ∧ ((1 / (2↑𝑘)) ∈ ℝ* ∧ (1 / (2↑(𝑘 + 1))) ∈ ℝ*)) → (((1 / (2↑𝑘)) +𝑒 (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)) → (((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))) = ∅))
1307, 40, 86, 125, 126, 129syl32anc 1326 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → (((1 / (2↑𝑘)) +𝑒 (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)) → (((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))) = ∅))
131124, 130sylbird 249 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → (((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)) → (((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))) = ∅))
132131necon3ad 2795 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → ((((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))) ≠ ∅ → ¬ ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘))))
133115, 132mpd 15 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → ¬ ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)))
134117, 120rpaddcld 11763 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ∈ ℝ+)
135134rpred 11748 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ∈ ℝ)
1364adantr 480 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → 𝐷 ∈ (Met‘𝑋))
137 metcl 21947 . . . . . . . . . 10 ((𝐷 ∈ (Met‘𝑋) ∧ (𝑆𝑘) ∈ 𝑋 ∧ ((𝑆𝑘)𝑇𝑘) ∈ 𝑋) → ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)) ∈ ℝ)
138136, 40, 86, 137syl3anc 1318 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)) ∈ ℝ)
139135, 138letrid 10068 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → (((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)) ∨ ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)) ≤ ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1))))))
140139ord 391 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (¬ ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)) → ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)) ≤ ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1))))))
141133, 140mpd 15 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)) ≤ ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))))
142 seqp1 12678 . . . . . . . . . . . 12 (𝑘 ∈ (ℤ‘0) → (seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘(𝑘 + 1)) = ((seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1))))
143 nn0uz 11598 . . . . . . . . . . . 12 0 = (ℤ‘0)
144142, 143eleq2s 2706 . . . . . . . . . . 11 (𝑘 ∈ ℕ0 → (seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘(𝑘 + 1)) = ((seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1))))
14523fveq1i 6104 . . . . . . . . . . 11 (𝑆‘(𝑘 + 1)) = (seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘(𝑘 + 1))
14623fveq1i 6104 . . . . . . . . . . . 12 (𝑆𝑘) = (seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘𝑘)
147146oveq1i 6559 . . . . . . . . . . 11 ((𝑆𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1))) = ((seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1)))
148144, 145, 1473eqtr4g 2669 . . . . . . . . . 10 (𝑘 ∈ ℕ0 → (𝑆‘(𝑘 + 1)) = ((𝑆𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1))))
149 nn0p1nn 11209 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℕ0 → (𝑘 + 1) ∈ ℕ)
150 nnne0 10930 . . . . . . . . . . . . . . . . 17 ((𝑘 + 1) ∈ ℕ → (𝑘 + 1) ≠ 0)
151150neneqd 2787 . . . . . . . . . . . . . . . 16 ((𝑘 + 1) ∈ ℕ → ¬ (𝑘 + 1) = 0)
152149, 151syl 17 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℕ0 → ¬ (𝑘 + 1) = 0)
153152iffalsed 4047 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ0 → if((𝑘 + 1) = 0, 𝐶, ((𝑘 + 1) − 1)) = ((𝑘 + 1) − 1))
154 ovex 6577 . . . . . . . . . . . . . 14 ((𝑘 + 1) − 1) ∈ V
155153, 154syl6eqel 2696 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ0 → if((𝑘 + 1) = 0, 𝐶, ((𝑘 + 1) − 1)) ∈ V)
156 eqeq1 2614 . . . . . . . . . . . . . . 15 (𝑚 = (𝑘 + 1) → (𝑚 = 0 ↔ (𝑘 + 1) = 0))
157 oveq1 6556 . . . . . . . . . . . . . . 15 (𝑚 = (𝑘 + 1) → (𝑚 − 1) = ((𝑘 + 1) − 1))
158156, 157ifbieq2d 4061 . . . . . . . . . . . . . 14 (𝑚 = (𝑘 + 1) → if(𝑚 = 0, 𝐶, (𝑚 − 1)) = if((𝑘 + 1) = 0, 𝐶, ((𝑘 + 1) − 1)))
159 eqid 2610 . . . . . . . . . . . . . 14 (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))) = (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))
160158, 159fvmptg 6189 . . . . . . . . . . . . 13 (((𝑘 + 1) ∈ ℕ0 ∧ if((𝑘 + 1) = 0, 𝐶, ((𝑘 + 1) − 1)) ∈ V) → ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1)) = if((𝑘 + 1) = 0, 𝐶, ((𝑘 + 1) − 1)))
16112, 155, 160syl2anc 691 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 → ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1)) = if((𝑘 + 1) = 0, 𝐶, ((𝑘 + 1) − 1)))
162 nn0cn 11179 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ0𝑘 ∈ ℂ)
163 ax-1cn 9873 . . . . . . . . . . . . 13 1 ∈ ℂ
164 pncan 10166 . . . . . . . . . . . . 13 ((𝑘 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑘 + 1) − 1) = 𝑘)
165162, 163, 164sylancl 693 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 → ((𝑘 + 1) − 1) = 𝑘)
166161, 153, 1653eqtrd 2648 . . . . . . . . . . 11 (𝑘 ∈ ℕ0 → ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1)) = 𝑘)
167166oveq2d 6565 . . . . . . . . . 10 (𝑘 ∈ ℕ0 → ((𝑆𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1))) = ((𝑆𝑘)𝑇𝑘))
168148, 167eqtrd 2644 . . . . . . . . 9 (𝑘 ∈ ℕ0 → (𝑆‘(𝑘 + 1)) = ((𝑆𝑘)𝑇𝑘))
169168adantl 481 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → (𝑆‘(𝑘 + 1)) = ((𝑆𝑘)𝑇𝑘))
170169oveq1d 6564 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → ((𝑆‘(𝑘 + 1))𝐷(𝑆𝑘)) = (((𝑆𝑘)𝑇𝑘)𝐷(𝑆𝑘)))
171 metsym 21965 . . . . . . . 8 ((𝐷 ∈ (Met‘𝑋) ∧ ((𝑆𝑘)𝑇𝑘) ∈ 𝑋 ∧ (𝑆𝑘) ∈ 𝑋) → (((𝑆𝑘)𝑇𝑘)𝐷(𝑆𝑘)) = ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)))
172136, 86, 40, 171syl3anc 1318 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (((𝑆𝑘)𝑇𝑘)𝐷(𝑆𝑘)) = ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)))
173170, 172eqtrd 2644 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → ((𝑆‘(𝑘 + 1))𝐷(𝑆𝑘)) = ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)))
174 3cn 10972 . . . . . . . . . . . . 13 3 ∈ ℂ
1751742timesi 11024 . . . . . . . . . . . 12 (2 · 3) = (3 + 3)
176175oveq1i 6559 . . . . . . . . . . 11 ((2 · 3) − 3) = ((3 + 3) − 3)
177174, 174pncan3oi 10176 . . . . . . . . . . 11 ((3 + 3) − 3) = 3
178 df-3 10957 . . . . . . . . . . 11 3 = (2 + 1)
179176, 177, 1783eqtri 2636 . . . . . . . . . 10 ((2 · 3) − 3) = (2 + 1)
180179oveq1i 6559 . . . . . . . . 9 (((2 · 3) − 3) / (2↑(𝑘 + 1))) = ((2 + 1) / (2↑(𝑘 + 1)))
181 rpcn 11717 . . . . . . . . . . 11 ((2↑(𝑘 + 1)) ∈ ℝ+ → (2↑(𝑘 + 1)) ∈ ℂ)
182 rpne0 11724 . . . . . . . . . . 11 ((2↑(𝑘 + 1)) ∈ ℝ+ → (2↑(𝑘 + 1)) ≠ 0)
183 2cn 10968 . . . . . . . . . . . . 13 2 ∈ ℂ
184183, 174mulcli 9924 . . . . . . . . . . . 12 (2 · 3) ∈ ℂ
185 divsubdir 10600 . . . . . . . . . . . 12 (((2 · 3) ∈ ℂ ∧ 3 ∈ ℂ ∧ ((2↑(𝑘 + 1)) ∈ ℂ ∧ (2↑(𝑘 + 1)) ≠ 0)) → (((2 · 3) − 3) / (2↑(𝑘 + 1))) = (((2 · 3) / (2↑(𝑘 + 1))) − (3 / (2↑(𝑘 + 1)))))
186184, 174, 185mp3an12 1406 . . . . . . . . . . 11 (((2↑(𝑘 + 1)) ∈ ℂ ∧ (2↑(𝑘 + 1)) ≠ 0) → (((2 · 3) − 3) / (2↑(𝑘 + 1))) = (((2 · 3) / (2↑(𝑘 + 1))) − (3 / (2↑(𝑘 + 1)))))
187181, 182, 186syl2anc 691 . . . . . . . . . 10 ((2↑(𝑘 + 1)) ∈ ℝ+ → (((2 · 3) − 3) / (2↑(𝑘 + 1))) = (((2 · 3) / (2↑(𝑘 + 1))) − (3 / (2↑(𝑘 + 1)))))
18845, 187syl 17 . . . . . . . . 9 (𝑘 ∈ ℕ0 → (((2 · 3) − 3) / (2↑(𝑘 + 1))) = (((2 · 3) / (2↑(𝑘 + 1))) − (3 / (2↑(𝑘 + 1)))))
189 divdir 10589 . . . . . . . . . . . 12 ((2 ∈ ℂ ∧ 1 ∈ ℂ ∧ ((2↑(𝑘 + 1)) ∈ ℂ ∧ (2↑(𝑘 + 1)) ≠ 0)) → ((2 + 1) / (2↑(𝑘 + 1))) = ((2 / (2↑(𝑘 + 1))) + (1 / (2↑(𝑘 + 1)))))
190183, 163, 189mp3an12 1406 . . . . . . . . . . 11 (((2↑(𝑘 + 1)) ∈ ℂ ∧ (2↑(𝑘 + 1)) ≠ 0) → ((2 + 1) / (2↑(𝑘 + 1))) = ((2 / (2↑(𝑘 + 1))) + (1 / (2↑(𝑘 + 1)))))
191181, 182, 190syl2anc 691 . . . . . . . . . 10 ((2↑(𝑘 + 1)) ∈ ℝ+ → ((2 + 1) / (2↑(𝑘 + 1))) = ((2 / (2↑(𝑘 + 1))) + (1 / (2↑(𝑘 + 1)))))
19245, 191syl 17 . . . . . . . . 9 (𝑘 ∈ ℕ0 → ((2 + 1) / (2↑(𝑘 + 1))) = ((2 / (2↑(𝑘 + 1))) + (1 / (2↑(𝑘 + 1)))))
193180, 188, 1923eqtr3a 2668 . . . . . . . 8 (𝑘 ∈ ℕ0 → (((2 · 3) / (2↑(𝑘 + 1))) − (3 / (2↑(𝑘 + 1)))) = ((2 / (2↑(𝑘 + 1))) + (1 / (2↑(𝑘 + 1)))))
194 rpcn 11717 . . . . . . . . . . . 12 ((2↑𝑘) ∈ ℝ+ → (2↑𝑘) ∈ ℂ)
195 rpne0 11724 . . . . . . . . . . . 12 ((2↑𝑘) ∈ ℝ+ → (2↑𝑘) ≠ 0)
196 2cnne0 11119 . . . . . . . . . . . . 13 (2 ∈ ℂ ∧ 2 ≠ 0)
197 divcan5 10606 . . . . . . . . . . . . 13 ((3 ∈ ℂ ∧ ((2↑𝑘) ∈ ℂ ∧ (2↑𝑘) ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · 3) / (2 · (2↑𝑘))) = (3 / (2↑𝑘)))
198174, 196, 197mp3an13 1407 . . . . . . . . . . . 12 (((2↑𝑘) ∈ ℂ ∧ (2↑𝑘) ≠ 0) → ((2 · 3) / (2 · (2↑𝑘))) = (3 / (2↑𝑘)))
199194, 195, 198syl2anc 691 . . . . . . . . . . 11 ((2↑𝑘) ∈ ℝ+ → ((2 · 3) / (2 · (2↑𝑘))) = (3 / (2↑𝑘)))
20051, 199syl 17 . . . . . . . . . 10 (𝑘 ∈ ℕ0 → ((2 · 3) / (2 · (2↑𝑘))) = (3 / (2↑𝑘)))
20151, 194syl 17 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ0 → (2↑𝑘) ∈ ℂ)
202 mulcom 9901 . . . . . . . . . . . . 13 ((2 ∈ ℂ ∧ (2↑𝑘) ∈ ℂ) → (2 · (2↑𝑘)) = ((2↑𝑘) · 2))
203183, 201, 202sylancr 694 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 → (2 · (2↑𝑘)) = ((2↑𝑘) · 2))
204 expp1 12729 . . . . . . . . . . . . 13 ((2 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (2↑(𝑘 + 1)) = ((2↑𝑘) · 2))
205183, 204mpan 702 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 → (2↑(𝑘 + 1)) = ((2↑𝑘) · 2))
206203, 205eqtr4d 2647 . . . . . . . . . . 11 (𝑘 ∈ ℕ0 → (2 · (2↑𝑘)) = (2↑(𝑘 + 1)))
207206oveq2d 6565 . . . . . . . . . 10 (𝑘 ∈ ℕ0 → ((2 · 3) / (2 · (2↑𝑘))) = ((2 · 3) / (2↑(𝑘 + 1))))
208200, 207eqtr3d 2646 . . . . . . . . 9 (𝑘 ∈ ℕ0 → (3 / (2↑𝑘)) = ((2 · 3) / (2↑(𝑘 + 1))))
209208oveq1d 6564 . . . . . . . 8 (𝑘 ∈ ℕ0 → ((3 / (2↑𝑘)) − (3 / (2↑(𝑘 + 1)))) = (((2 · 3) / (2↑(𝑘 + 1))) − (3 / (2↑(𝑘 + 1)))))
210 divcan5 10606 . . . . . . . . . . . . 13 ((1 ∈ ℂ ∧ ((2↑𝑘) ∈ ℂ ∧ (2↑𝑘) ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · 1) / (2 · (2↑𝑘))) = (1 / (2↑𝑘)))
211163, 196, 210mp3an13 1407 . . . . . . . . . . . 12 (((2↑𝑘) ∈ ℂ ∧ (2↑𝑘) ≠ 0) → ((2 · 1) / (2 · (2↑𝑘))) = (1 / (2↑𝑘)))
212194, 195, 211syl2anc 691 . . . . . . . . . . 11 ((2↑𝑘) ∈ ℝ+ → ((2 · 1) / (2 · (2↑𝑘))) = (1 / (2↑𝑘)))
21351, 212syl 17 . . . . . . . . . 10 (𝑘 ∈ ℕ0 → ((2 · 1) / (2 · (2↑𝑘))) = (1 / (2↑𝑘)))
214 2t1e2 11053 . . . . . . . . . . . 12 (2 · 1) = 2
215214a1i 11 . . . . . . . . . . 11 (𝑘 ∈ ℕ0 → (2 · 1) = 2)
216215, 206oveq12d 6567 . . . . . . . . . 10 (𝑘 ∈ ℕ0 → ((2 · 1) / (2 · (2↑𝑘))) = (2 / (2↑(𝑘 + 1))))
217213, 216eqtr3d 2646 . . . . . . . . 9 (𝑘 ∈ ℕ0 → (1 / (2↑𝑘)) = (2 / (2↑(𝑘 + 1))))
218217oveq1d 6564 . . . . . . . 8 (𝑘 ∈ ℕ0 → ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) = ((2 / (2↑(𝑘 + 1))) + (1 / (2↑(𝑘 + 1)))))
219193, 209, 2183eqtr4d 2654 . . . . . . 7 (𝑘 ∈ ℕ0 → ((3 / (2↑𝑘)) − (3 / (2↑(𝑘 + 1)))) = ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))))
220219adantl 481 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → ((3 / (2↑𝑘)) − (3 / (2↑(𝑘 + 1)))) = ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))))
221141, 173, 2203brtr4d 4615 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → ((𝑆‘(𝑘 + 1))𝐷(𝑆𝑘)) ≤ ((3 / (2↑𝑘)) − (3 / (2↑(𝑘 + 1)))))
222 blss2 22019 . . . . 5 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑆‘(𝑘 + 1)) ∈ 𝑋 ∧ (𝑆𝑘) ∈ 𝑋) ∧ ((3 / (2↑(𝑘 + 1))) ∈ ℝ ∧ (3 / (2↑𝑘)) ∈ ℝ ∧ ((𝑆‘(𝑘 + 1))𝐷(𝑆𝑘)) ≤ ((3 / (2↑𝑘)) − (3 / (2↑(𝑘 + 1)))))) → ((𝑆‘(𝑘 + 1))(ball‘𝐷)(3 / (2↑(𝑘 + 1)))) ⊆ ((𝑆𝑘)(ball‘𝐷)(3 / (2↑𝑘))))
2237, 31, 40, 48, 54, 221, 222syl33anc 1333 . . . 4 ((𝜑𝑘 ∈ ℕ0) → ((𝑆‘(𝑘 + 1))(ball‘𝐷)(3 / (2↑(𝑘 + 1)))) ⊆ ((𝑆𝑘)(ball‘𝐷)(3 / (2↑𝑘))))
2241, 223sylan2 490 . . 3 ((𝜑𝑘 ∈ ℕ) → ((𝑆‘(𝑘 + 1))(ball‘𝐷)(3 / (2↑(𝑘 + 1)))) ⊆ ((𝑆𝑘)(ball‘𝐷)(3 / (2↑𝑘))))
225 peano2nn 10909 . . . . . . 7 (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
226 fveq2 6103 . . . . . . . . 9 (𝑛 = (𝑘 + 1) → (𝑆𝑛) = (𝑆‘(𝑘 + 1)))
227 oveq2 6557 . . . . . . . . . 10 (𝑛 = (𝑘 + 1) → (2↑𝑛) = (2↑(𝑘 + 1)))
228227oveq2d 6565 . . . . . . . . 9 (𝑛 = (𝑘 + 1) → (3 / (2↑𝑛)) = (3 / (2↑(𝑘 + 1))))
229226, 228opeq12d 4348 . . . . . . . 8 (𝑛 = (𝑘 + 1) → ⟨(𝑆𝑛), (3 / (2↑𝑛))⟩ = ⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩)
230 heibor.12 . . . . . . . 8 𝑀 = (𝑛 ∈ ℕ ↦ ⟨(𝑆𝑛), (3 / (2↑𝑛))⟩)
231 opex 4859 . . . . . . . 8 ⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩ ∈ V
232229, 230, 231fvmpt 6191 . . . . . . 7 ((𝑘 + 1) ∈ ℕ → (𝑀‘(𝑘 + 1)) = ⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩)
233225, 232syl 17 . . . . . 6 (𝑘 ∈ ℕ → (𝑀‘(𝑘 + 1)) = ⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩)
234233adantl 481 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (𝑀‘(𝑘 + 1)) = ⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩)
235234fveq2d 6107 . . . 4 ((𝜑𝑘 ∈ ℕ) → ((ball‘𝐷)‘(𝑀‘(𝑘 + 1))) = ((ball‘𝐷)‘⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩))
236 df-ov 6552 . . . 4 ((𝑆‘(𝑘 + 1))(ball‘𝐷)(3 / (2↑(𝑘 + 1)))) = ((ball‘𝐷)‘⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩)
237235, 236syl6eqr 2662 . . 3 ((𝜑𝑘 ∈ ℕ) → ((ball‘𝐷)‘(𝑀‘(𝑘 + 1))) = ((𝑆‘(𝑘 + 1))(ball‘𝐷)(3 / (2↑(𝑘 + 1)))))
238 fveq2 6103 . . . . . . . 8 (𝑛 = 𝑘 → (𝑆𝑛) = (𝑆𝑘))
239 oveq2 6557 . . . . . . . . 9 (𝑛 = 𝑘 → (2↑𝑛) = (2↑𝑘))
240239oveq2d 6565 . . . . . . . 8 (𝑛 = 𝑘 → (3 / (2↑𝑛)) = (3 / (2↑𝑘)))
241238, 240opeq12d 4348 . . . . . . 7 (𝑛 = 𝑘 → ⟨(𝑆𝑛), (3 / (2↑𝑛))⟩ = ⟨(𝑆𝑘), (3 / (2↑𝑘))⟩)
242 opex 4859 . . . . . . 7 ⟨(𝑆𝑘), (3 / (2↑𝑘))⟩ ∈ V
243241, 230, 242fvmpt 6191 . . . . . 6 (𝑘 ∈ ℕ → (𝑀𝑘) = ⟨(𝑆𝑘), (3 / (2↑𝑘))⟩)
244243fveq2d 6107 . . . . 5 (𝑘 ∈ ℕ → ((ball‘𝐷)‘(𝑀𝑘)) = ((ball‘𝐷)‘⟨(𝑆𝑘), (3 / (2↑𝑘))⟩))
245 df-ov 6552 . . . . 5 ((𝑆𝑘)(ball‘𝐷)(3 / (2↑𝑘))) = ((ball‘𝐷)‘⟨(𝑆𝑘), (3 / (2↑𝑘))⟩)
246244, 245syl6eqr 2662 . . . 4 (𝑘 ∈ ℕ → ((ball‘𝐷)‘(𝑀𝑘)) = ((𝑆𝑘)(ball‘𝐷)(3 / (2↑𝑘))))
247246adantl 481 . . 3 ((𝜑𝑘 ∈ ℕ) → ((ball‘𝐷)‘(𝑀𝑘)) = ((𝑆𝑘)(ball‘𝐷)(3 / (2↑𝑘))))
248224, 237, 2473sstr4d 3611 . 2 ((𝜑𝑘 ∈ ℕ) → ((ball‘𝐷)‘(𝑀‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝑀𝑘)))
249248ralrimiva 2949 1 (𝜑 → ∀𝑘 ∈ ℕ ((ball‘𝐷)‘(𝑀‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝑀𝑘)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977  {cab 2596   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  Vcvv 3173   ∩ cin 3539   ⊆ wss 3540  ∅c0 3874  ifcif 4036  𝒫 cpw 4108  ⟨cop 4131  ∪ cuni 4372  ∪ ciun 4455   class class class wbr 4583  {copab 4642   ↦ cmpt 4643  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549   ↦ cmpt2 6551  2nd c2nd 7058  Fincfn 7841  ℂcc 9813  ℝcr 9814  0cc0 9815  1c1 9816   + caddc 9818   · cmul 9820  ℝ*cxr 9952   ≤ cle 9954   − cmin 10145   / cdiv 10563  ℕcn 10897  2c2 10947  3c3 10948  ℕ0cn0 11169  ℤ≥cuz 11563  ℝ+crp 11708   +𝑒 cxad 11820  seqcseq 12663  ↑cexp 12722  ∞Metcxmt 19552  Metcme 19553  ballcbl 19554  MetOpencmopn 19557  CMetcms 22860 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-er 7629  df-map 7746  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-n0 11170  df-z 11255  df-uz 11564  df-rp 11709  df-xneg 11822  df-xadd 11823  df-xmul 11824  df-seq 12664  df-exp 12723  df-psmet 19559  df-xmet 19560  df-met 19561  df-bl 19562  df-cmet 22863 This theorem is referenced by:  heiborlem8  32787  heiborlem9  32788
 Copyright terms: Public domain W3C validator