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

Theorem heiborlem6 33286
Description: Lemma for heibor 33291. 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 11259 . . . 4 (𝑘 ∈ ℕ → 𝑘 ∈ ℕ0)
2 heibor.6 . . . . . . . 8 (𝜑𝐷 ∈ (CMet‘𝑋))
3 cmetmet 23024 . . . . . . . 8 (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋))
42, 3syl 17 . . . . . . 7 (𝜑𝐷 ∈ (Met‘𝑋))
5 metxmet 22079 . . . . . . 7 (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋))
64, 5syl 17 . . . . . 6 (𝜑𝐷 ∈ (∞Met‘𝑋))
76adantr 481 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → 𝐷 ∈ (∞Met‘𝑋))
8 heibor.7 . . . . . . . . 9 (𝜑𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin))
9 inss1 3817 . . . . . . . . 9 (𝒫 𝑋 ∩ Fin) ⊆ 𝒫 𝑋
10 fss 6023 . . . . . . . . 9 ((𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin) ∧ (𝒫 𝑋 ∩ Fin) ⊆ 𝒫 𝑋) → 𝐹:ℕ0⟶𝒫 𝑋)
118, 9, 10sylancl 693 . . . . . . . 8 (𝜑𝐹:ℕ0⟶𝒫 𝑋)
12 peano2nn0 11293 . . . . . . . 8 (𝑘 ∈ ℕ0 → (𝑘 + 1) ∈ ℕ0)
13 ffvelrn 6323 . . . . . . . 8 ((𝐹:ℕ0⟶𝒫 𝑋 ∧ (𝑘 + 1) ∈ ℕ0) → (𝐹‘(𝑘 + 1)) ∈ 𝒫 𝑋)
1411, 12, 13syl2an 494 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (𝐹‘(𝑘 + 1)) ∈ 𝒫 𝑋)
1514elpwid 4148 . . . . . 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 33284 . . . . . . . 8 ((𝜑 ∧ (𝑘 + 1) ∈ ℕ0) → (𝑆‘(𝑘 + 1))𝐺(𝑘 + 1))
2512, 24sylan2 491 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (𝑆‘(𝑘 + 1))𝐺(𝑘 + 1))
26 fvex 6168 . . . . . . . . 9 (𝑆‘(𝑘 + 1)) ∈ V
27 ovex 6643 . . . . . . . . 9 (𝑘 + 1) ∈ V
2816, 17, 18, 26, 27heiborlem2 33282 . . . . . . . 8 ((𝑆‘(𝑘 + 1))𝐺(𝑘 + 1) ↔ ((𝑘 + 1) ∈ ℕ0 ∧ (𝑆‘(𝑘 + 1)) ∈ (𝐹‘(𝑘 + 1)) ∧ ((𝑆‘(𝑘 + 1))𝐵(𝑘 + 1)) ∈ 𝐾))
2928simp2bi 1075 . . . . . . 7 ((𝑆‘(𝑘 + 1))𝐺(𝑘 + 1) → (𝑆‘(𝑘 + 1)) ∈ (𝐹‘(𝑘 + 1)))
3025, 29syl 17 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (𝑆‘(𝑘 + 1)) ∈ (𝐹‘(𝑘 + 1)))
3115, 30sseldd 3589 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → (𝑆‘(𝑘 + 1)) ∈ 𝑋)
3211ffvelrnda 6325 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (𝐹𝑘) ∈ 𝒫 𝑋)
3332elpwid 4148 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (𝐹𝑘) ⊆ 𝑋)
3416, 17, 18, 19, 2, 8, 20, 21, 22, 23heiborlem4 33284 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (𝑆𝑘)𝐺𝑘)
35 fvex 6168 . . . . . . . . 9 (𝑆𝑘) ∈ V
36 vex 3193 . . . . . . . . 9 𝑘 ∈ V
3716, 17, 18, 35, 36heiborlem2 33282 . . . . . . . 8 ((𝑆𝑘)𝐺𝑘 ↔ (𝑘 ∈ ℕ0 ∧ (𝑆𝑘) ∈ (𝐹𝑘) ∧ ((𝑆𝑘)𝐵𝑘) ∈ 𝐾))
3837simp2bi 1075 . . . . . . 7 ((𝑆𝑘)𝐺𝑘 → (𝑆𝑘) ∈ (𝐹𝑘))
3934, 38syl 17 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (𝑆𝑘) ∈ (𝐹𝑘))
4033, 39sseldd 3589 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → (𝑆𝑘) ∈ 𝑋)
41 3re 11054 . . . . . 6 3 ∈ ℝ
42 2nn 11145 . . . . . . . . 9 2 ∈ ℕ
43 nnexpcl 12829 . . . . . . . . 9 ((2 ∈ ℕ ∧ (𝑘 + 1) ∈ ℕ0) → (2↑(𝑘 + 1)) ∈ ℕ)
4442, 12, 43sylancr 694 . . . . . . . 8 (𝑘 ∈ ℕ0 → (2↑(𝑘 + 1)) ∈ ℕ)
4544nnrpd 11830 . . . . . . 7 (𝑘 ∈ ℕ0 → (2↑(𝑘 + 1)) ∈ ℝ+)
4645adantl 482 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (2↑(𝑘 + 1)) ∈ ℝ+)
47 rerpdivcl 11821 . . . . . 6 ((3 ∈ ℝ ∧ (2↑(𝑘 + 1)) ∈ ℝ+) → (3 / (2↑(𝑘 + 1))) ∈ ℝ)
4841, 46, 47sylancr 694 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → (3 / (2↑(𝑘 + 1))) ∈ ℝ)
49 nnexpcl 12829 . . . . . . . . 9 ((2 ∈ ℕ ∧ 𝑘 ∈ ℕ0) → (2↑𝑘) ∈ ℕ)
5042, 49mpan 705 . . . . . . . 8 (𝑘 ∈ ℕ0 → (2↑𝑘) ∈ ℕ)
5150nnrpd 11830 . . . . . . 7 (𝑘 ∈ ℕ0 → (2↑𝑘) ∈ ℝ+)
5251adantl 482 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (2↑𝑘) ∈ ℝ+)
53 rerpdivcl 11821 . . . . . 6 ((3 ∈ ℝ ∧ (2↑𝑘) ∈ ℝ+) → (3 / (2↑𝑘)) ∈ ℝ)
5441, 52, 53sylancr 694 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → (3 / (2↑𝑘)) ∈ ℝ)
55 oveq1 6622 . . . . . . . . . . . 12 (𝑧 = (𝑆𝑘) → (𝑧(ball‘𝐷)(1 / (2↑𝑚))) = ((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑚))))
56 oveq2 6623 . . . . . . . . . . . . . 14 (𝑚 = 𝑘 → (2↑𝑚) = (2↑𝑘))
5756oveq2d 6631 . . . . . . . . . . . . 13 (𝑚 = 𝑘 → (1 / (2↑𝑚)) = (1 / (2↑𝑘)))
5857oveq2d 6631 . . . . . . . . . . . 12 (𝑚 = 𝑘 → ((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑚))) = ((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑘))))
59 ovex 6643 . . . . . . . . . . . 12 ((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∈ V
6055, 58, 19, 59ovmpt2 6761 . . . . . . . . . . 11 (((𝑆𝑘) ∈ 𝑋𝑘 ∈ ℕ0) → ((𝑆𝑘)𝐵𝑘) = ((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑘))))
6140, 60sylancom 700 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → ((𝑆𝑘)𝐵𝑘) = ((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑘))))
62 df-br 4624 . . . . . . . . . . . . . . . . 17 ((𝑆𝑘)𝐺𝑘 ↔ ⟨(𝑆𝑘), 𝑘⟩ ∈ 𝐺)
63 fveq2 6158 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = ⟨(𝑆𝑘), 𝑘⟩ → (𝑇𝑥) = (𝑇‘⟨(𝑆𝑘), 𝑘⟩))
64 df-ov 6618 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑆𝑘)𝑇𝑘) = (𝑇‘⟨(𝑆𝑘), 𝑘⟩)
6563, 64syl6eqr 2673 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = ⟨(𝑆𝑘), 𝑘⟩ → (𝑇𝑥) = ((𝑆𝑘)𝑇𝑘))
6635, 36op2ndd 7139 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = ⟨(𝑆𝑘), 𝑘⟩ → (2nd𝑥) = 𝑘)
6766oveq1d 6630 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = ⟨(𝑆𝑘), 𝑘⟩ → ((2nd𝑥) + 1) = (𝑘 + 1))
6865, 67breq12d 4636 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = ⟨(𝑆𝑘), 𝑘⟩ → ((𝑇𝑥)𝐺((2nd𝑥) + 1) ↔ ((𝑆𝑘)𝑇𝑘)𝐺(𝑘 + 1)))
69 fveq2 6158 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = ⟨(𝑆𝑘), 𝑘⟩ → (𝐵𝑥) = (𝐵‘⟨(𝑆𝑘), 𝑘⟩))
70 df-ov 6618 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑆𝑘)𝐵𝑘) = (𝐵‘⟨(𝑆𝑘), 𝑘⟩)
7169, 70syl6eqr 2673 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = ⟨(𝑆𝑘), 𝑘⟩ → (𝐵𝑥) = ((𝑆𝑘)𝐵𝑘))
7265, 67oveq12d 6633 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = ⟨(𝑆𝑘), 𝑘⟩ → ((𝑇𝑥)𝐵((2nd𝑥) + 1)) = (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1)))
7371, 72ineq12d 3799 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = ⟨(𝑆𝑘), 𝑘⟩ → ((𝐵𝑥) ∩ ((𝑇𝑥)𝐵((2nd𝑥) + 1))) = (((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))))
7473eleq1d 2683 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = ⟨(𝑆𝑘), 𝑘⟩ → (((𝐵𝑥) ∩ ((𝑇𝑥)𝐵((2nd𝑥) + 1))) ∈ 𝐾 ↔ (((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾))
7568, 74anbi12d 746 . . . . . . . . . . . . . . . . . . 19 (𝑥 = ⟨(𝑆𝑘), 𝑘⟩ → (((𝑇𝑥)𝐺((2nd𝑥) + 1) ∧ ((𝐵𝑥) ∩ ((𝑇𝑥)𝐵((2nd𝑥) + 1))) ∈ 𝐾) ↔ (((𝑆𝑘)𝑇𝑘)𝐺(𝑘 + 1) ∧ (((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾)))
7675rspccv 3296 . . . . . . . . . . . . . . . . . 18 (∀𝑥𝐺 ((𝑇𝑥)𝐺((2nd𝑥) + 1) ∧ ((𝐵𝑥) ∩ ((𝑇𝑥)𝐵((2nd𝑥) + 1))) ∈ 𝐾) → (⟨(𝑆𝑘), 𝑘⟩ ∈ 𝐺 → (((𝑆𝑘)𝑇𝑘)𝐺(𝑘 + 1) ∧ (((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾)))
7721, 76syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (⟨(𝑆𝑘), 𝑘⟩ ∈ 𝐺 → (((𝑆𝑘)𝑇𝑘)𝐺(𝑘 + 1) ∧ (((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾)))
7862, 77syl5bi 232 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑆𝑘)𝐺𝑘 → (((𝑆𝑘)𝑇𝑘)𝐺(𝑘 + 1) ∧ (((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾)))
7978adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ℕ0) → ((𝑆𝑘)𝐺𝑘 → (((𝑆𝑘)𝑇𝑘)𝐺(𝑘 + 1) ∧ (((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾)))
8034, 79mpd 15 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ0) → (((𝑆𝑘)𝑇𝑘)𝐺(𝑘 + 1) ∧ (((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾))
8180simpld 475 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ0) → ((𝑆𝑘)𝑇𝑘)𝐺(𝑘 + 1))
82 ovex 6643 . . . . . . . . . . . . . . 15 ((𝑆𝑘)𝑇𝑘) ∈ V
8316, 17, 18, 82, 27heiborlem2 33282 . . . . . . . . . . . . . 14 (((𝑆𝑘)𝑇𝑘)𝐺(𝑘 + 1) ↔ ((𝑘 + 1) ∈ ℕ0 ∧ ((𝑆𝑘)𝑇𝑘) ∈ (𝐹‘(𝑘 + 1)) ∧ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1)) ∈ 𝐾))
8483simp2bi 1075 . . . . . . . . . . . . 13 (((𝑆𝑘)𝑇𝑘)𝐺(𝑘 + 1) → ((𝑆𝑘)𝑇𝑘) ∈ (𝐹‘(𝑘 + 1)))
8581, 84syl 17 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → ((𝑆𝑘)𝑇𝑘) ∈ (𝐹‘(𝑘 + 1)))
8615, 85sseldd 3589 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → ((𝑆𝑘)𝑇𝑘) ∈ 𝑋)
8712adantl 482 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → (𝑘 + 1) ∈ ℕ0)
88 oveq1 6622 . . . . . . . . . . . 12 (𝑧 = ((𝑆𝑘)𝑇𝑘) → (𝑧(ball‘𝐷)(1 / (2↑𝑚))) = (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑𝑚))))
89 oveq2 6623 . . . . . . . . . . . . . 14 (𝑚 = (𝑘 + 1) → (2↑𝑚) = (2↑(𝑘 + 1)))
9089oveq2d 6631 . . . . . . . . . . . . 13 (𝑚 = (𝑘 + 1) → (1 / (2↑𝑚)) = (1 / (2↑(𝑘 + 1))))
9190oveq2d 6631 . . . . . . . . . . . 12 (𝑚 = (𝑘 + 1) → (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑𝑚))) = (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1)))))
92 ovex 6643 . . . . . . . . . . . 12 (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1)))) ∈ V
9388, 91, 19, 92ovmpt2 6761 . . . . . . . . . . 11 ((((𝑆𝑘)𝑇𝑘) ∈ 𝑋 ∧ (𝑘 + 1) ∈ ℕ0) → (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1)) = (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1)))))
9486, 87, 93syl2anc 692 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1)) = (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1)))))
9561, 94ineq12d 3799 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → (((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))) = (((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))))
9680simprd 479 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → (((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾)
97 0elpw 4804 . . . . . . . . . . . . 13 ∅ ∈ 𝒫 𝑈
98 0fin 8148 . . . . . . . . . . . . 13 ∅ ∈ Fin
99 elin 3780 . . . . . . . . . . . . 13 (∅ ∈ (𝒫 𝑈 ∩ Fin) ↔ (∅ ∈ 𝒫 𝑈 ∧ ∅ ∈ Fin))
10097, 98, 99mpbir2an 954 . . . . . . . . . . . 12 ∅ ∈ (𝒫 𝑈 ∩ Fin)
101 0ss 3950 . . . . . . . . . . . 12 ∅ ⊆
102 unieq 4417 . . . . . . . . . . . . . 14 (𝑣 = ∅ → 𝑣 = ∅)
103102sseq2d 3618 . . . . . . . . . . . . 13 (𝑣 = ∅ → (∅ ⊆ 𝑣 ↔ ∅ ⊆ ∅))
104103rspcev 3299 . . . . . . . . . . . 12 ((∅ ∈ (𝒫 𝑈 ∩ Fin) ∧ ∅ ⊆ ∅) → ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ 𝑣)
105100, 101, 104mp2an 707 . . . . . . . . . . 11 𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ 𝑣
106 0ex 4760 . . . . . . . . . . . . 13 ∅ ∈ V
107 sseq1 3611 . . . . . . . . . . . . . . 15 (𝑢 = ∅ → (𝑢 𝑣 ↔ ∅ ⊆ 𝑣))
108107rexbidv 3047 . . . . . . . . . . . . . 14 (𝑢 = ∅ → (∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 𝑣 ↔ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ 𝑣))
109108notbid 308 . . . . . . . . . . . . 13 (𝑢 = ∅ → (¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 𝑣 ↔ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ 𝑣))
110106, 109, 17elab2 3342 . . . . . . . . . . . 12 (∅ ∈ 𝐾 ↔ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ 𝑣)
111110con2bii 347 . . . . . . . . . . 11 (∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ 𝑣 ↔ ¬ ∅ ∈ 𝐾)
112105, 111mpbi 220 . . . . . . . . . 10 ¬ ∅ ∈ 𝐾
113 nelne2 2887 . . . . . . . . . 10 (((((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾 ∧ ¬ ∅ ∈ 𝐾) → (((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ≠ ∅)
11496, 112, 113sylancl 693 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → (((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ≠ ∅)
11595, 114eqnetrrd 2858 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → (((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))) ≠ ∅)
11651rpreccld 11842 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ0 → (1 / (2↑𝑘)) ∈ ℝ+)
117116adantl 482 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ0) → (1 / (2↑𝑘)) ∈ ℝ+)
118117rpred 11832 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → (1 / (2↑𝑘)) ∈ ℝ)
11945rpreccld 11842 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ0 → (1 / (2↑(𝑘 + 1))) ∈ ℝ+)
120119adantl 482 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ0) → (1 / (2↑(𝑘 + 1))) ∈ ℝ+)
121120rpred 11832 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → (1 / (2↑(𝑘 + 1))) ∈ ℝ)
122 rexadd 12022 . . . . . . . . . . . 12 (((1 / (2↑𝑘)) ∈ ℝ ∧ (1 / (2↑(𝑘 + 1))) ∈ ℝ) → ((1 / (2↑𝑘)) +𝑒 (1 / (2↑(𝑘 + 1)))) = ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))))
123118, 121, 122syl2anc 692 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → ((1 / (2↑𝑘)) +𝑒 (1 / (2↑(𝑘 + 1)))) = ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))))
124123breq1d 4633 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → (((1 / (2↑𝑘)) +𝑒 (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)) ↔ ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘))))
125117rpxrd 11833 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → (1 / (2↑𝑘)) ∈ ℝ*)
126120rpxrd 11833 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → (1 / (2↑(𝑘 + 1))) ∈ ℝ*)
127 bldisj 22143 . . . . . . . . . . . . 13 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑆𝑘) ∈ 𝑋 ∧ ((𝑆𝑘)𝑇𝑘) ∈ 𝑋) ∧ ((1 / (2↑𝑘)) ∈ ℝ* ∧ (1 / (2↑(𝑘 + 1))) ∈ ℝ* ∧ ((1 / (2↑𝑘)) +𝑒 (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)))) → (((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))) = ∅)
1281273exp2 1282 . . . . . . . . . . . 12 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑆𝑘) ∈ 𝑋 ∧ ((𝑆𝑘)𝑇𝑘) ∈ 𝑋) → ((1 / (2↑𝑘)) ∈ ℝ* → ((1 / (2↑(𝑘 + 1))) ∈ ℝ* → (((1 / (2↑𝑘)) +𝑒 (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)) → (((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))) = ∅))))
129128imp32 449 . . . . . . . . . . 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 1331 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → (((1 / (2↑𝑘)) +𝑒 (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)) → (((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))) = ∅))
131124, 130sylbird 250 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → (((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)) → (((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))) = ∅))
132131necon3ad 2803 . . . . . . . 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 11847 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ∈ ℝ+)
135134rpred 11832 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ∈ ℝ)
1364adantr 481 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → 𝐷 ∈ (Met‘𝑋))
137 metcl 22077 . . . . . . . . . 10 ((𝐷 ∈ (Met‘𝑋) ∧ (𝑆𝑘) ∈ 𝑋 ∧ ((𝑆𝑘)𝑇𝑘) ∈ 𝑋) → ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)) ∈ ℝ)
138136, 40, 86, 137syl3anc 1323 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)) ∈ ℝ)
139135, 138letrid 10149 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → (((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)) ∨ ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)) ≤ ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1))))))
140139ord 392 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (¬ ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)) → ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)) ≤ ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1))))))
141133, 140mpd 15 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)) ≤ ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))))
142 seqp1 12772 . . . . . . . . . . . 12 (𝑘 ∈ (ℤ‘0) → (seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘(𝑘 + 1)) = ((seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1))))
143 nn0uz 11682 . . . . . . . . . . . 12 0 = (ℤ‘0)
144142, 143eleq2s 2716 . . . . . . . . . . 11 (𝑘 ∈ ℕ0 → (seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘(𝑘 + 1)) = ((seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1))))
14523fveq1i 6159 . . . . . . . . . . 11 (𝑆‘(𝑘 + 1)) = (seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘(𝑘 + 1))
14623fveq1i 6159 . . . . . . . . . . . 12 (𝑆𝑘) = (seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘𝑘)
147146oveq1i 6625 . . . . . . . . . . 11 ((𝑆𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1))) = ((seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1)))
148144, 145, 1473eqtr4g 2680 . . . . . . . . . 10 (𝑘 ∈ ℕ0 → (𝑆‘(𝑘 + 1)) = ((𝑆𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1))))
149 nn0p1nn 11292 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℕ0 → (𝑘 + 1) ∈ ℕ)
150 nnne0 11013 . . . . . . . . . . . . . . . . 17 ((𝑘 + 1) ∈ ℕ → (𝑘 + 1) ≠ 0)
151150neneqd 2795 . . . . . . . . . . . . . . . 16 ((𝑘 + 1) ∈ ℕ → ¬ (𝑘 + 1) = 0)
152149, 151syl 17 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℕ0 → ¬ (𝑘 + 1) = 0)
153152iffalsed 4075 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ0 → if((𝑘 + 1) = 0, 𝐶, ((𝑘 + 1) − 1)) = ((𝑘 + 1) − 1))
154 ovex 6643 . . . . . . . . . . . . . 14 ((𝑘 + 1) − 1) ∈ V
155153, 154syl6eqel 2706 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ0 → if((𝑘 + 1) = 0, 𝐶, ((𝑘 + 1) − 1)) ∈ V)
156 eqeq1 2625 . . . . . . . . . . . . . . 15 (𝑚 = (𝑘 + 1) → (𝑚 = 0 ↔ (𝑘 + 1) = 0))
157 oveq1 6622 . . . . . . . . . . . . . . 15 (𝑚 = (𝑘 + 1) → (𝑚 − 1) = ((𝑘 + 1) − 1))
158156, 157ifbieq2d 4089 . . . . . . . . . . . . . 14 (𝑚 = (𝑘 + 1) → if(𝑚 = 0, 𝐶, (𝑚 − 1)) = if((𝑘 + 1) = 0, 𝐶, ((𝑘 + 1) − 1)))
159 eqid 2621 . . . . . . . . . . . . . 14 (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))) = (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))
160158, 159fvmptg 6247 . . . . . . . . . . . . 13 (((𝑘 + 1) ∈ ℕ0 ∧ if((𝑘 + 1) = 0, 𝐶, ((𝑘 + 1) − 1)) ∈ V) → ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1)) = if((𝑘 + 1) = 0, 𝐶, ((𝑘 + 1) − 1)))
16112, 155, 160syl2anc 692 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 → ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1)) = if((𝑘 + 1) = 0, 𝐶, ((𝑘 + 1) − 1)))
162 nn0cn 11262 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ0𝑘 ∈ ℂ)
163 ax-1cn 9954 . . . . . . . . . . . . 13 1 ∈ ℂ
164 pncan 10247 . . . . . . . . . . . . 13 ((𝑘 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑘 + 1) − 1) = 𝑘)
165162, 163, 164sylancl 693 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 → ((𝑘 + 1) − 1) = 𝑘)
166161, 153, 1653eqtrd 2659 . . . . . . . . . . 11 (𝑘 ∈ ℕ0 → ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1)) = 𝑘)
167166oveq2d 6631 . . . . . . . . . 10 (𝑘 ∈ ℕ0 → ((𝑆𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1))) = ((𝑆𝑘)𝑇𝑘))
168148, 167eqtrd 2655 . . . . . . . . 9 (𝑘 ∈ ℕ0 → (𝑆‘(𝑘 + 1)) = ((𝑆𝑘)𝑇𝑘))
169168adantl 482 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → (𝑆‘(𝑘 + 1)) = ((𝑆𝑘)𝑇𝑘))
170169oveq1d 6630 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → ((𝑆‘(𝑘 + 1))𝐷(𝑆𝑘)) = (((𝑆𝑘)𝑇𝑘)𝐷(𝑆𝑘)))
171 metsym 22095 . . . . . . . 8 ((𝐷 ∈ (Met‘𝑋) ∧ ((𝑆𝑘)𝑇𝑘) ∈ 𝑋 ∧ (𝑆𝑘) ∈ 𝑋) → (((𝑆𝑘)𝑇𝑘)𝐷(𝑆𝑘)) = ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)))
172136, 86, 40, 171syl3anc 1323 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (((𝑆𝑘)𝑇𝑘)𝐷(𝑆𝑘)) = ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)))
173170, 172eqtrd 2655 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → ((𝑆‘(𝑘 + 1))𝐷(𝑆𝑘)) = ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)))
174 3cn 11055 . . . . . . . . . . . . 13 3 ∈ ℂ
1751742timesi 11107 . . . . . . . . . . . 12 (2 · 3) = (3 + 3)
176175oveq1i 6625 . . . . . . . . . . 11 ((2 · 3) − 3) = ((3 + 3) − 3)
177174, 174pncan3oi 10257 . . . . . . . . . . 11 ((3 + 3) − 3) = 3
178 df-3 11040 . . . . . . . . . . 11 3 = (2 + 1)
179176, 177, 1783eqtri 2647 . . . . . . . . . 10 ((2 · 3) − 3) = (2 + 1)
180179oveq1i 6625 . . . . . . . . 9 (((2 · 3) − 3) / (2↑(𝑘 + 1))) = ((2 + 1) / (2↑(𝑘 + 1)))
181 rpcn 11801 . . . . . . . . . . 11 ((2↑(𝑘 + 1)) ∈ ℝ+ → (2↑(𝑘 + 1)) ∈ ℂ)
182 rpne0 11808 . . . . . . . . . . 11 ((2↑(𝑘 + 1)) ∈ ℝ+ → (2↑(𝑘 + 1)) ≠ 0)
183 2cn 11051 . . . . . . . . . . . . 13 2 ∈ ℂ
184183, 174mulcli 10005 . . . . . . . . . . . 12 (2 · 3) ∈ ℂ
185 divsubdir 10681 . . . . . . . . . . . 12 (((2 · 3) ∈ ℂ ∧ 3 ∈ ℂ ∧ ((2↑(𝑘 + 1)) ∈ ℂ ∧ (2↑(𝑘 + 1)) ≠ 0)) → (((2 · 3) − 3) / (2↑(𝑘 + 1))) = (((2 · 3) / (2↑(𝑘 + 1))) − (3 / (2↑(𝑘 + 1)))))
186184, 174, 185mp3an12 1411 . . . . . . . . . . 11 (((2↑(𝑘 + 1)) ∈ ℂ ∧ (2↑(𝑘 + 1)) ≠ 0) → (((2 · 3) − 3) / (2↑(𝑘 + 1))) = (((2 · 3) / (2↑(𝑘 + 1))) − (3 / (2↑(𝑘 + 1)))))
187181, 182, 186syl2anc 692 . . . . . . . . . 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 10670 . . . . . . . . . . . 12 ((2 ∈ ℂ ∧ 1 ∈ ℂ ∧ ((2↑(𝑘 + 1)) ∈ ℂ ∧ (2↑(𝑘 + 1)) ≠ 0)) → ((2 + 1) / (2↑(𝑘 + 1))) = ((2 / (2↑(𝑘 + 1))) + (1 / (2↑(𝑘 + 1)))))
190183, 163, 189mp3an12 1411 . . . . . . . . . . 11 (((2↑(𝑘 + 1)) ∈ ℂ ∧ (2↑(𝑘 + 1)) ≠ 0) → ((2 + 1) / (2↑(𝑘 + 1))) = ((2 / (2↑(𝑘 + 1))) + (1 / (2↑(𝑘 + 1)))))
191181, 182, 190syl2anc 692 . . . . . . . . . 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 2679 . . . . . . . 8 (𝑘 ∈ ℕ0 → (((2 · 3) / (2↑(𝑘 + 1))) − (3 / (2↑(𝑘 + 1)))) = ((2 / (2↑(𝑘 + 1))) + (1 / (2↑(𝑘 + 1)))))
194 rpcn 11801 . . . . . . . . . . . 12 ((2↑𝑘) ∈ ℝ+ → (2↑𝑘) ∈ ℂ)
195 rpne0 11808 . . . . . . . . . . . 12 ((2↑𝑘) ∈ ℝ+ → (2↑𝑘) ≠ 0)
196 2cnne0 11202 . . . . . . . . . . . . 13 (2 ∈ ℂ ∧ 2 ≠ 0)
197 divcan5 10687 . . . . . . . . . . . . 13 ((3 ∈ ℂ ∧ ((2↑𝑘) ∈ ℂ ∧ (2↑𝑘) ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · 3) / (2 · (2↑𝑘))) = (3 / (2↑𝑘)))
198174, 196, 197mp3an13 1412 . . . . . . . . . . . 12 (((2↑𝑘) ∈ ℂ ∧ (2↑𝑘) ≠ 0) → ((2 · 3) / (2 · (2↑𝑘))) = (3 / (2↑𝑘)))
199194, 195, 198syl2anc 692 . . . . . . . . . . 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 9982 . . . . . . . . . . . . 13 ((2 ∈ ℂ ∧ (2↑𝑘) ∈ ℂ) → (2 · (2↑𝑘)) = ((2↑𝑘) · 2))
203183, 201, 202sylancr 694 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 → (2 · (2↑𝑘)) = ((2↑𝑘) · 2))
204 expp1 12823 . . . . . . . . . . . . 13 ((2 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (2↑(𝑘 + 1)) = ((2↑𝑘) · 2))
205183, 204mpan 705 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 → (2↑(𝑘 + 1)) = ((2↑𝑘) · 2))
206203, 205eqtr4d 2658 . . . . . . . . . . 11 (𝑘 ∈ ℕ0 → (2 · (2↑𝑘)) = (2↑(𝑘 + 1)))
207206oveq2d 6631 . . . . . . . . . 10 (𝑘 ∈ ℕ0 → ((2 · 3) / (2 · (2↑𝑘))) = ((2 · 3) / (2↑(𝑘 + 1))))
208200, 207eqtr3d 2657 . . . . . . . . 9 (𝑘 ∈ ℕ0 → (3 / (2↑𝑘)) = ((2 · 3) / (2↑(𝑘 + 1))))
209208oveq1d 6630 . . . . . . . 8 (𝑘 ∈ ℕ0 → ((3 / (2↑𝑘)) − (3 / (2↑(𝑘 + 1)))) = (((2 · 3) / (2↑(𝑘 + 1))) − (3 / (2↑(𝑘 + 1)))))
210 divcan5 10687 . . . . . . . . . . . . 13 ((1 ∈ ℂ ∧ ((2↑𝑘) ∈ ℂ ∧ (2↑𝑘) ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · 1) / (2 · (2↑𝑘))) = (1 / (2↑𝑘)))
211163, 196, 210mp3an13 1412 . . . . . . . . . . . 12 (((2↑𝑘) ∈ ℂ ∧ (2↑𝑘) ≠ 0) → ((2 · 1) / (2 · (2↑𝑘))) = (1 / (2↑𝑘)))
212194, 195, 211syl2anc 692 . . . . . . . . . . 11 ((2↑𝑘) ∈ ℝ+ → ((2 · 1) / (2 · (2↑𝑘))) = (1 / (2↑𝑘)))
21351, 212syl 17 . . . . . . . . . 10 (𝑘 ∈ ℕ0 → ((2 · 1) / (2 · (2↑𝑘))) = (1 / (2↑𝑘)))
214 2t1e2 11136 . . . . . . . . . . . 12 (2 · 1) = 2
215214a1i 11 . . . . . . . . . . 11 (𝑘 ∈ ℕ0 → (2 · 1) = 2)
216215, 206oveq12d 6633 . . . . . . . . . 10 (𝑘 ∈ ℕ0 → ((2 · 1) / (2 · (2↑𝑘))) = (2 / (2↑(𝑘 + 1))))
217213, 216eqtr3d 2657 . . . . . . . . 9 (𝑘 ∈ ℕ0 → (1 / (2↑𝑘)) = (2 / (2↑(𝑘 + 1))))
218217oveq1d 6630 . . . . . . . 8 (𝑘 ∈ ℕ0 → ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) = ((2 / (2↑(𝑘 + 1))) + (1 / (2↑(𝑘 + 1)))))
219193, 209, 2183eqtr4d 2665 . . . . . . 7 (𝑘 ∈ ℕ0 → ((3 / (2↑𝑘)) − (3 / (2↑(𝑘 + 1)))) = ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))))
220219adantl 482 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → ((3 / (2↑𝑘)) − (3 / (2↑(𝑘 + 1)))) = ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))))
221141, 173, 2203brtr4d 4655 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → ((𝑆‘(𝑘 + 1))𝐷(𝑆𝑘)) ≤ ((3 / (2↑𝑘)) − (3 / (2↑(𝑘 + 1)))))
222 blss2 22149 . . . . 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 1338 . . . 4 ((𝜑𝑘 ∈ ℕ0) → ((𝑆‘(𝑘 + 1))(ball‘𝐷)(3 / (2↑(𝑘 + 1)))) ⊆ ((𝑆𝑘)(ball‘𝐷)(3 / (2↑𝑘))))
2241, 223sylan2 491 . . 3 ((𝜑𝑘 ∈ ℕ) → ((𝑆‘(𝑘 + 1))(ball‘𝐷)(3 / (2↑(𝑘 + 1)))) ⊆ ((𝑆𝑘)(ball‘𝐷)(3 / (2↑𝑘))))
225 peano2nn 10992 . . . . . . 7 (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
226 fveq2 6158 . . . . . . . . 9 (𝑛 = (𝑘 + 1) → (𝑆𝑛) = (𝑆‘(𝑘 + 1)))
227 oveq2 6623 . . . . . . . . . 10 (𝑛 = (𝑘 + 1) → (2↑𝑛) = (2↑(𝑘 + 1)))
228227oveq2d 6631 . . . . . . . . 9 (𝑛 = (𝑘 + 1) → (3 / (2↑𝑛)) = (3 / (2↑(𝑘 + 1))))
229226, 228opeq12d 4385 . . . . . . . 8 (𝑛 = (𝑘 + 1) → ⟨(𝑆𝑛), (3 / (2↑𝑛))⟩ = ⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩)
230 heibor.12 . . . . . . . 8 𝑀 = (𝑛 ∈ ℕ ↦ ⟨(𝑆𝑛), (3 / (2↑𝑛))⟩)
231 opex 4903 . . . . . . . 8 ⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩ ∈ V
232229, 230, 231fvmpt 6249 . . . . . . 7 ((𝑘 + 1) ∈ ℕ → (𝑀‘(𝑘 + 1)) = ⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩)
233225, 232syl 17 . . . . . 6 (𝑘 ∈ ℕ → (𝑀‘(𝑘 + 1)) = ⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩)
234233adantl 482 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (𝑀‘(𝑘 + 1)) = ⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩)
235234fveq2d 6162 . . . 4 ((𝜑𝑘 ∈ ℕ) → ((ball‘𝐷)‘(𝑀‘(𝑘 + 1))) = ((ball‘𝐷)‘⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩))
236 df-ov 6618 . . . 4 ((𝑆‘(𝑘 + 1))(ball‘𝐷)(3 / (2↑(𝑘 + 1)))) = ((ball‘𝐷)‘⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩)
237235, 236syl6eqr 2673 . . 3 ((𝜑𝑘 ∈ ℕ) → ((ball‘𝐷)‘(𝑀‘(𝑘 + 1))) = ((𝑆‘(𝑘 + 1))(ball‘𝐷)(3 / (2↑(𝑘 + 1)))))
238 fveq2 6158 . . . . . . . 8 (𝑛 = 𝑘 → (𝑆𝑛) = (𝑆𝑘))
239 oveq2 6623 . . . . . . . . 9 (𝑛 = 𝑘 → (2↑𝑛) = (2↑𝑘))
240239oveq2d 6631 . . . . . . . 8 (𝑛 = 𝑘 → (3 / (2↑𝑛)) = (3 / (2↑𝑘)))
241238, 240opeq12d 4385 . . . . . . 7 (𝑛 = 𝑘 → ⟨(𝑆𝑛), (3 / (2↑𝑛))⟩ = ⟨(𝑆𝑘), (3 / (2↑𝑘))⟩)
242 opex 4903 . . . . . . 7 ⟨(𝑆𝑘), (3 / (2↑𝑘))⟩ ∈ V
243241, 230, 242fvmpt 6249 . . . . . 6 (𝑘 ∈ ℕ → (𝑀𝑘) = ⟨(𝑆𝑘), (3 / (2↑𝑘))⟩)
244243fveq2d 6162 . . . . 5 (𝑘 ∈ ℕ → ((ball‘𝐷)‘(𝑀𝑘)) = ((ball‘𝐷)‘⟨(𝑆𝑘), (3 / (2↑𝑘))⟩))
245 df-ov 6618 . . . . 5 ((𝑆𝑘)(ball‘𝐷)(3 / (2↑𝑘))) = ((ball‘𝐷)‘⟨(𝑆𝑘), (3 / (2↑𝑘))⟩)
246244, 245syl6eqr 2673 . . . 4 (𝑘 ∈ ℕ → ((ball‘𝐷)‘(𝑀𝑘)) = ((𝑆𝑘)(ball‘𝐷)(3 / (2↑𝑘))))
247246adantl 482 . . 3 ((𝜑𝑘 ∈ ℕ) → ((ball‘𝐷)‘(𝑀𝑘)) = ((𝑆𝑘)(ball‘𝐷)(3 / (2↑𝑘))))
248224, 237, 2473sstr4d 3633 . 2 ((𝜑𝑘 ∈ ℕ) → ((ball‘𝐷)‘(𝑀‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝑀𝑘)))
249248ralrimiva 2962 1 (𝜑 → ∀𝑘 ∈ ℕ ((ball‘𝐷)‘(𝑀‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝑀𝑘)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 384  w3a 1036   = wceq 1480  wcel 1987  {cab 2607  wne 2790  wral 2908  wrex 2909  Vcvv 3190  cin 3559  wss 3560  c0 3897  ifcif 4064  𝒫 cpw 4136  cop 4161   cuni 4409   ciun 4492   class class class wbr 4623  {copab 4682  cmpt 4683  wf 5853  cfv 5857  (class class class)co 6615  cmpt2 6617  2nd c2nd 7127  Fincfn 7915  cc 9894  cr 9895  0cc0 9896  1c1 9897   + caddc 9899   · cmul 9901  *cxr 10033  cle 10035  cmin 10226   / cdiv 10644  cn 10980  2c2 11030  3c3 11031  0cn0 11252  cuz 11647  +crp 11792   +𝑒 cxad 11904  seqcseq 12757  cexp 12816  ∞Metcxmt 19671  Metcme 19672  ballcbl 19673  MetOpencmopn 19676  CMetcms 22992
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4751  ax-nul 4759  ax-pow 4813  ax-pr 4877  ax-un 6914  ax-cnex 9952  ax-resscn 9953  ax-1cn 9954  ax-icn 9955  ax-addcl 9956  ax-addrcl 9957  ax-mulcl 9958  ax-mulrcl 9959  ax-mulcom 9960  ax-addass 9961  ax-mulass 9962  ax-distr 9963  ax-i2m1 9964  ax-1ne0 9965  ax-1rid 9966  ax-rnegex 9967  ax-rrecex 9968  ax-cnre 9969  ax-pre-lttri 9970  ax-pre-lttrn 9971  ax-pre-ltadd 9972  ax-pre-mulgt0 9973
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2913  df-rex 2914  df-reu 2915  df-rmo 2916  df-rab 2917  df-v 3192  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3898  df-if 4065  df-pw 4138  df-sn 4156  df-pr 4158  df-tp 4160  df-op 4162  df-uni 4410  df-iun 4494  df-br 4624  df-opab 4684  df-mpt 4685  df-tr 4723  df-eprel 4995  df-id 4999  df-po 5005  df-so 5006  df-fr 5043  df-we 5045  df-xp 5090  df-rel 5091  df-cnv 5092  df-co 5093  df-dm 5094  df-rn 5095  df-res 5096  df-ima 5097  df-pred 5649  df-ord 5695  df-on 5696  df-lim 5697  df-suc 5698  df-iota 5820  df-fun 5859  df-fn 5860  df-f 5861  df-f1 5862  df-fo 5863  df-f1o 5864  df-fv 5865  df-riota 6576  df-ov 6618  df-oprab 6619  df-mpt2 6620  df-om 7028  df-1st 7128  df-2nd 7129  df-wrecs 7367  df-recs 7428  df-rdg 7466  df-er 7702  df-map 7819  df-en 7916  df-dom 7917  df-sdom 7918  df-fin 7919  df-pnf 10036  df-mnf 10037  df-xr 10038  df-ltxr 10039  df-le 10040  df-sub 10228  df-neg 10229  df-div 10645  df-nn 10981  df-2 11039  df-3 11040  df-n0 11253  df-z 11338  df-uz 11648  df-rp 11793  df-xneg 11906  df-xadd 11907  df-xmul 11908  df-seq 12758  df-exp 12817  df-psmet 19678  df-xmet 19679  df-met 19680  df-bl 19681  df-cmet 22995
This theorem is referenced by:  heiborlem8  33288  heiborlem9  33289
  Copyright terms: Public domain W3C validator