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 35711
Description: Lemma for heibor 35716. 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 12097 . . . 4 (𝑘 ∈ ℕ → 𝑘 ∈ ℕ0)
2 heibor.6 . . . . . . . 8 (𝜑𝐷 ∈ (CMet‘𝑋))
3 cmetmet 24183 . . . . . . . 8 (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋))
42, 3syl 17 . . . . . . 7 (𝜑𝐷 ∈ (Met‘𝑋))
5 metxmet 23232 . . . . . . 7 (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋))
64, 5syl 17 . . . . . 6 (𝜑𝐷 ∈ (∞Met‘𝑋))
76adantr 484 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → 𝐷 ∈ (∞Met‘𝑋))
8 heibor.7 . . . . . . . . 9 (𝜑𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin))
9 inss1 4143 . . . . . . . . 9 (𝒫 𝑋 ∩ Fin) ⊆ 𝒫 𝑋
10 fss 6562 . . . . . . . . 9 ((𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin) ∧ (𝒫 𝑋 ∩ Fin) ⊆ 𝒫 𝑋) → 𝐹:ℕ0⟶𝒫 𝑋)
118, 9, 10sylancl 589 . . . . . . . 8 (𝜑𝐹:ℕ0⟶𝒫 𝑋)
12 peano2nn0 12130 . . . . . . . 8 (𝑘 ∈ ℕ0 → (𝑘 + 1) ∈ ℕ0)
13 ffvelrn 6902 . . . . . . . 8 ((𝐹:ℕ0⟶𝒫 𝑋 ∧ (𝑘 + 1) ∈ ℕ0) → (𝐹‘(𝑘 + 1)) ∈ 𝒫 𝑋)
1411, 12, 13syl2an 599 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (𝐹‘(𝑘 + 1)) ∈ 𝒫 𝑋)
1514elpwid 4524 . . . . . 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 35709 . . . . . . . 8 ((𝜑 ∧ (𝑘 + 1) ∈ ℕ0) → (𝑆‘(𝑘 + 1))𝐺(𝑘 + 1))
2512, 24sylan2 596 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (𝑆‘(𝑘 + 1))𝐺(𝑘 + 1))
26 fvex 6730 . . . . . . . . 9 (𝑆‘(𝑘 + 1)) ∈ V
27 ovex 7246 . . . . . . . . 9 (𝑘 + 1) ∈ V
2816, 17, 18, 26, 27heiborlem2 35707 . . . . . . . 8 ((𝑆‘(𝑘 + 1))𝐺(𝑘 + 1) ↔ ((𝑘 + 1) ∈ ℕ0 ∧ (𝑆‘(𝑘 + 1)) ∈ (𝐹‘(𝑘 + 1)) ∧ ((𝑆‘(𝑘 + 1))𝐵(𝑘 + 1)) ∈ 𝐾))
2928simp2bi 1148 . . . . . . 7 ((𝑆‘(𝑘 + 1))𝐺(𝑘 + 1) → (𝑆‘(𝑘 + 1)) ∈ (𝐹‘(𝑘 + 1)))
3025, 29syl 17 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (𝑆‘(𝑘 + 1)) ∈ (𝐹‘(𝑘 + 1)))
3115, 30sseldd 3902 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → (𝑆‘(𝑘 + 1)) ∈ 𝑋)
3211ffvelrnda 6904 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (𝐹𝑘) ∈ 𝒫 𝑋)
3332elpwid 4524 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (𝐹𝑘) ⊆ 𝑋)
3416, 17, 18, 19, 2, 8, 20, 21, 22, 23heiborlem4 35709 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (𝑆𝑘)𝐺𝑘)
35 fvex 6730 . . . . . . . . 9 (𝑆𝑘) ∈ V
36 vex 3412 . . . . . . . . 9 𝑘 ∈ V
3716, 17, 18, 35, 36heiborlem2 35707 . . . . . . . 8 ((𝑆𝑘)𝐺𝑘 ↔ (𝑘 ∈ ℕ0 ∧ (𝑆𝑘) ∈ (𝐹𝑘) ∧ ((𝑆𝑘)𝐵𝑘) ∈ 𝐾))
3837simp2bi 1148 . . . . . . 7 ((𝑆𝑘)𝐺𝑘 → (𝑆𝑘) ∈ (𝐹𝑘))
3934, 38syl 17 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (𝑆𝑘) ∈ (𝐹𝑘))
4033, 39sseldd 3902 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → (𝑆𝑘) ∈ 𝑋)
41 3re 11910 . . . . . 6 3 ∈ ℝ
42 2nn 11903 . . . . . . . . 9 2 ∈ ℕ
43 nnexpcl 13648 . . . . . . . . 9 ((2 ∈ ℕ ∧ (𝑘 + 1) ∈ ℕ0) → (2↑(𝑘 + 1)) ∈ ℕ)
4442, 12, 43sylancr 590 . . . . . . . 8 (𝑘 ∈ ℕ0 → (2↑(𝑘 + 1)) ∈ ℕ)
4544nnrpd 12626 . . . . . . 7 (𝑘 ∈ ℕ0 → (2↑(𝑘 + 1)) ∈ ℝ+)
4645adantl 485 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (2↑(𝑘 + 1)) ∈ ℝ+)
47 rerpdivcl 12616 . . . . . 6 ((3 ∈ ℝ ∧ (2↑(𝑘 + 1)) ∈ ℝ+) → (3 / (2↑(𝑘 + 1))) ∈ ℝ)
4841, 46, 47sylancr 590 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → (3 / (2↑(𝑘 + 1))) ∈ ℝ)
49 nnexpcl 13648 . . . . . . . . 9 ((2 ∈ ℕ ∧ 𝑘 ∈ ℕ0) → (2↑𝑘) ∈ ℕ)
5042, 49mpan 690 . . . . . . . 8 (𝑘 ∈ ℕ0 → (2↑𝑘) ∈ ℕ)
5150nnrpd 12626 . . . . . . 7 (𝑘 ∈ ℕ0 → (2↑𝑘) ∈ ℝ+)
5251adantl 485 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (2↑𝑘) ∈ ℝ+)
53 rerpdivcl 12616 . . . . . 6 ((3 ∈ ℝ ∧ (2↑𝑘) ∈ ℝ+) → (3 / (2↑𝑘)) ∈ ℝ)
5441, 52, 53sylancr 590 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → (3 / (2↑𝑘)) ∈ ℝ)
55 oveq1 7220 . . . . . . . . . . . 12 (𝑧 = (𝑆𝑘) → (𝑧(ball‘𝐷)(1 / (2↑𝑚))) = ((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑚))))
56 oveq2 7221 . . . . . . . . . . . . . 14 (𝑚 = 𝑘 → (2↑𝑚) = (2↑𝑘))
5756oveq2d 7229 . . . . . . . . . . . . 13 (𝑚 = 𝑘 → (1 / (2↑𝑚)) = (1 / (2↑𝑘)))
5857oveq2d 7229 . . . . . . . . . . . 12 (𝑚 = 𝑘 → ((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑚))) = ((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑘))))
59 ovex 7246 . . . . . . . . . . . 12 ((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∈ V
6055, 58, 19, 59ovmpo 7369 . . . . . . . . . . 11 (((𝑆𝑘) ∈ 𝑋𝑘 ∈ ℕ0) → ((𝑆𝑘)𝐵𝑘) = ((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑘))))
6140, 60sylancom 591 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → ((𝑆𝑘)𝐵𝑘) = ((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑘))))
62 df-br 5054 . . . . . . . . . . . . . . . . 17 ((𝑆𝑘)𝐺𝑘 ↔ ⟨(𝑆𝑘), 𝑘⟩ ∈ 𝐺)
63 fveq2 6717 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = ⟨(𝑆𝑘), 𝑘⟩ → (𝑇𝑥) = (𝑇‘⟨(𝑆𝑘), 𝑘⟩))
64 df-ov 7216 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑆𝑘)𝑇𝑘) = (𝑇‘⟨(𝑆𝑘), 𝑘⟩)
6563, 64eqtr4di 2796 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = ⟨(𝑆𝑘), 𝑘⟩ → (𝑇𝑥) = ((𝑆𝑘)𝑇𝑘))
6635, 36op2ndd 7772 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = ⟨(𝑆𝑘), 𝑘⟩ → (2nd𝑥) = 𝑘)
6766oveq1d 7228 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = ⟨(𝑆𝑘), 𝑘⟩ → ((2nd𝑥) + 1) = (𝑘 + 1))
6865, 67breq12d 5066 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = ⟨(𝑆𝑘), 𝑘⟩ → ((𝑇𝑥)𝐺((2nd𝑥) + 1) ↔ ((𝑆𝑘)𝑇𝑘)𝐺(𝑘 + 1)))
69 fveq2 6717 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = ⟨(𝑆𝑘), 𝑘⟩ → (𝐵𝑥) = (𝐵‘⟨(𝑆𝑘), 𝑘⟩))
70 df-ov 7216 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑆𝑘)𝐵𝑘) = (𝐵‘⟨(𝑆𝑘), 𝑘⟩)
7169, 70eqtr4di 2796 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = ⟨(𝑆𝑘), 𝑘⟩ → (𝐵𝑥) = ((𝑆𝑘)𝐵𝑘))
7265, 67oveq12d 7231 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = ⟨(𝑆𝑘), 𝑘⟩ → ((𝑇𝑥)𝐵((2nd𝑥) + 1)) = (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1)))
7371, 72ineq12d 4128 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = ⟨(𝑆𝑘), 𝑘⟩ → ((𝐵𝑥) ∩ ((𝑇𝑥)𝐵((2nd𝑥) + 1))) = (((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))))
7473eleq1d 2822 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = ⟨(𝑆𝑘), 𝑘⟩ → (((𝐵𝑥) ∩ ((𝑇𝑥)𝐵((2nd𝑥) + 1))) ∈ 𝐾 ↔ (((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾))
7568, 74anbi12d 634 . . . . . . . . . . . . . . . . . . 19 (𝑥 = ⟨(𝑆𝑘), 𝑘⟩ → (((𝑇𝑥)𝐺((2nd𝑥) + 1) ∧ ((𝐵𝑥) ∩ ((𝑇𝑥)𝐵((2nd𝑥) + 1))) ∈ 𝐾) ↔ (((𝑆𝑘)𝑇𝑘)𝐺(𝑘 + 1) ∧ (((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾)))
7675rspccv 3534 . . . . . . . . . . . . . . . . . 18 (∀𝑥𝐺 ((𝑇𝑥)𝐺((2nd𝑥) + 1) ∧ ((𝐵𝑥) ∩ ((𝑇𝑥)𝐵((2nd𝑥) + 1))) ∈ 𝐾) → (⟨(𝑆𝑘), 𝑘⟩ ∈ 𝐺 → (((𝑆𝑘)𝑇𝑘)𝐺(𝑘 + 1) ∧ (((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾)))
7721, 76syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (⟨(𝑆𝑘), 𝑘⟩ ∈ 𝐺 → (((𝑆𝑘)𝑇𝑘)𝐺(𝑘 + 1) ∧ (((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾)))
7862, 77syl5bi 245 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑆𝑘)𝐺𝑘 → (((𝑆𝑘)𝑇𝑘)𝐺(𝑘 + 1) ∧ (((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾)))
7978adantr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ℕ0) → ((𝑆𝑘)𝐺𝑘 → (((𝑆𝑘)𝑇𝑘)𝐺(𝑘 + 1) ∧ (((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾)))
8034, 79mpd 15 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ0) → (((𝑆𝑘)𝑇𝑘)𝐺(𝑘 + 1) ∧ (((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾))
8180simpld 498 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ0) → ((𝑆𝑘)𝑇𝑘)𝐺(𝑘 + 1))
82 ovex 7246 . . . . . . . . . . . . . . 15 ((𝑆𝑘)𝑇𝑘) ∈ V
8316, 17, 18, 82, 27heiborlem2 35707 . . . . . . . . . . . . . 14 (((𝑆𝑘)𝑇𝑘)𝐺(𝑘 + 1) ↔ ((𝑘 + 1) ∈ ℕ0 ∧ ((𝑆𝑘)𝑇𝑘) ∈ (𝐹‘(𝑘 + 1)) ∧ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1)) ∈ 𝐾))
8483simp2bi 1148 . . . . . . . . . . . . 13 (((𝑆𝑘)𝑇𝑘)𝐺(𝑘 + 1) → ((𝑆𝑘)𝑇𝑘) ∈ (𝐹‘(𝑘 + 1)))
8581, 84syl 17 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → ((𝑆𝑘)𝑇𝑘) ∈ (𝐹‘(𝑘 + 1)))
8615, 85sseldd 3902 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → ((𝑆𝑘)𝑇𝑘) ∈ 𝑋)
8712adantl 485 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → (𝑘 + 1) ∈ ℕ0)
88 oveq1 7220 . . . . . . . . . . . 12 (𝑧 = ((𝑆𝑘)𝑇𝑘) → (𝑧(ball‘𝐷)(1 / (2↑𝑚))) = (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑𝑚))))
89 oveq2 7221 . . . . . . . . . . . . . 14 (𝑚 = (𝑘 + 1) → (2↑𝑚) = (2↑(𝑘 + 1)))
9089oveq2d 7229 . . . . . . . . . . . . 13 (𝑚 = (𝑘 + 1) → (1 / (2↑𝑚)) = (1 / (2↑(𝑘 + 1))))
9190oveq2d 7229 . . . . . . . . . . . 12 (𝑚 = (𝑘 + 1) → (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑𝑚))) = (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1)))))
92 ovex 7246 . . . . . . . . . . . 12 (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1)))) ∈ V
9388, 91, 19, 92ovmpo 7369 . . . . . . . . . . 11 ((((𝑆𝑘)𝑇𝑘) ∈ 𝑋 ∧ (𝑘 + 1) ∈ ℕ0) → (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1)) = (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1)))))
9486, 87, 93syl2anc 587 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1)) = (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1)))))
9561, 94ineq12d 4128 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → (((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))) = (((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))))
9680simprd 499 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → (((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾)
97 0elpw 5247 . . . . . . . . . . . . 13 ∅ ∈ 𝒫 𝑈
98 0fin 8849 . . . . . . . . . . . . 13 ∅ ∈ Fin
99 elin 3882 . . . . . . . . . . . . 13 (∅ ∈ (𝒫 𝑈 ∩ Fin) ↔ (∅ ∈ 𝒫 𝑈 ∧ ∅ ∈ Fin))
10097, 98, 99mpbir2an 711 . . . . . . . . . . . 12 ∅ ∈ (𝒫 𝑈 ∩ Fin)
101 0ss 4311 . . . . . . . . . . . 12 ∅ ⊆
102 unieq 4830 . . . . . . . . . . . . . 14 (𝑣 = ∅ → 𝑣 = ∅)
103102sseq2d 3933 . . . . . . . . . . . . 13 (𝑣 = ∅ → (∅ ⊆ 𝑣 ↔ ∅ ⊆ ∅))
104103rspcev 3537 . . . . . . . . . . . 12 ((∅ ∈ (𝒫 𝑈 ∩ Fin) ∧ ∅ ⊆ ∅) → ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ 𝑣)
105100, 101, 104mp2an 692 . . . . . . . . . . 11 𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ 𝑣
106 0ex 5200 . . . . . . . . . . . . 13 ∅ ∈ V
107 sseq1 3926 . . . . . . . . . . . . . . 15 (𝑢 = ∅ → (𝑢 𝑣 ↔ ∅ ⊆ 𝑣))
108107rexbidv 3216 . . . . . . . . . . . . . 14 (𝑢 = ∅ → (∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 𝑣 ↔ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ 𝑣))
109108notbid 321 . . . . . . . . . . . . 13 (𝑢 = ∅ → (¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 𝑣 ↔ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ 𝑣))
110106, 109, 17elab2 3591 . . . . . . . . . . . 12 (∅ ∈ 𝐾 ↔ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ 𝑣)
111110con2bii 361 . . . . . . . . . . 11 (∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ 𝑣 ↔ ¬ ∅ ∈ 𝐾)
112105, 111mpbi 233 . . . . . . . . . 10 ¬ ∅ ∈ 𝐾
113 nelne2 3039 . . . . . . . . . 10 (((((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾 ∧ ¬ ∅ ∈ 𝐾) → (((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ≠ ∅)
11496, 112, 113sylancl 589 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → (((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ≠ ∅)
11595, 114eqnetrrd 3009 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → (((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))) ≠ ∅)
11651rpreccld 12638 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ0 → (1 / (2↑𝑘)) ∈ ℝ+)
117116adantl 485 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ0) → (1 / (2↑𝑘)) ∈ ℝ+)
118117rpred 12628 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → (1 / (2↑𝑘)) ∈ ℝ)
11945rpreccld 12638 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ0 → (1 / (2↑(𝑘 + 1))) ∈ ℝ+)
120119adantl 485 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ0) → (1 / (2↑(𝑘 + 1))) ∈ ℝ+)
121120rpred 12628 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → (1 / (2↑(𝑘 + 1))) ∈ ℝ)
122 rexadd 12822 . . . . . . . . . . . 12 (((1 / (2↑𝑘)) ∈ ℝ ∧ (1 / (2↑(𝑘 + 1))) ∈ ℝ) → ((1 / (2↑𝑘)) +𝑒 (1 / (2↑(𝑘 + 1)))) = ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))))
123118, 121, 122syl2anc 587 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → ((1 / (2↑𝑘)) +𝑒 (1 / (2↑(𝑘 + 1)))) = ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))))
124123breq1d 5063 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → (((1 / (2↑𝑘)) +𝑒 (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)) ↔ ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘))))
125117rpxrd 12629 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → (1 / (2↑𝑘)) ∈ ℝ*)
126120rpxrd 12629 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → (1 / (2↑(𝑘 + 1))) ∈ ℝ*)
127 bldisj 23296 . . . . . . . . . . . . 13 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑆𝑘) ∈ 𝑋 ∧ ((𝑆𝑘)𝑇𝑘) ∈ 𝑋) ∧ ((1 / (2↑𝑘)) ∈ ℝ* ∧ (1 / (2↑(𝑘 + 1))) ∈ ℝ* ∧ ((1 / (2↑𝑘)) +𝑒 (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)))) → (((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))) = ∅)
1281273exp2 1356 . . . . . . . . . . . 12 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑆𝑘) ∈ 𝑋 ∧ ((𝑆𝑘)𝑇𝑘) ∈ 𝑋) → ((1 / (2↑𝑘)) ∈ ℝ* → ((1 / (2↑(𝑘 + 1))) ∈ ℝ* → (((1 / (2↑𝑘)) +𝑒 (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)) → (((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))) = ∅))))
129128imp32 422 . . . . . . . . . . 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 1380 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → (((1 / (2↑𝑘)) +𝑒 (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)) → (((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))) = ∅))
131124, 130sylbird 263 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → (((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)) → (((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))) = ∅))
132131necon3ad 2953 . . . . . . . 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 12643 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ∈ ℝ+)
135134rpred 12628 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ∈ ℝ)
1364adantr 484 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → 𝐷 ∈ (Met‘𝑋))
137 metcl 23230 . . . . . . . . . 10 ((𝐷 ∈ (Met‘𝑋) ∧ (𝑆𝑘) ∈ 𝑋 ∧ ((𝑆𝑘)𝑇𝑘) ∈ 𝑋) → ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)) ∈ ℝ)
138136, 40, 86, 137syl3anc 1373 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)) ∈ ℝ)
139135, 138letrid 10984 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → (((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)) ∨ ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)) ≤ ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1))))))
140139ord 864 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (¬ ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)) → ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)) ≤ ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1))))))
141133, 140mpd 15 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)) ≤ ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))))
142 seqp1 13589 . . . . . . . . . . . 12 (𝑘 ∈ (ℤ‘0) → (seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘(𝑘 + 1)) = ((seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1))))
143 nn0uz 12476 . . . . . . . . . . . 12 0 = (ℤ‘0)
144142, 143eleq2s 2856 . . . . . . . . . . 11 (𝑘 ∈ ℕ0 → (seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘(𝑘 + 1)) = ((seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1))))
14523fveq1i 6718 . . . . . . . . . . 11 (𝑆‘(𝑘 + 1)) = (seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘(𝑘 + 1))
14623fveq1i 6718 . . . . . . . . . . . 12 (𝑆𝑘) = (seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘𝑘)
147146oveq1i 7223 . . . . . . . . . . 11 ((𝑆𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1))) = ((seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1)))
148144, 145, 1473eqtr4g 2803 . . . . . . . . . 10 (𝑘 ∈ ℕ0 → (𝑆‘(𝑘 + 1)) = ((𝑆𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1))))
149 eqid 2737 . . . . . . . . . . . . 13 (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))) = (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))
150 eqeq1 2741 . . . . . . . . . . . . . 14 (𝑚 = (𝑘 + 1) → (𝑚 = 0 ↔ (𝑘 + 1) = 0))
151 oveq1 7220 . . . . . . . . . . . . . 14 (𝑚 = (𝑘 + 1) → (𝑚 − 1) = ((𝑘 + 1) − 1))
152150, 151ifbieq2d 4465 . . . . . . . . . . . . 13 (𝑚 = (𝑘 + 1) → if(𝑚 = 0, 𝐶, (𝑚 − 1)) = if((𝑘 + 1) = 0, 𝐶, ((𝑘 + 1) − 1)))
153 nn0p1nn 12129 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℕ0 → (𝑘 + 1) ∈ ℕ)
154 nnne0 11864 . . . . . . . . . . . . . . . . 17 ((𝑘 + 1) ∈ ℕ → (𝑘 + 1) ≠ 0)
155154neneqd 2945 . . . . . . . . . . . . . . . 16 ((𝑘 + 1) ∈ ℕ → ¬ (𝑘 + 1) = 0)
156153, 155syl 17 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℕ0 → ¬ (𝑘 + 1) = 0)
157156iffalsed 4450 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ0 → if((𝑘 + 1) = 0, 𝐶, ((𝑘 + 1) − 1)) = ((𝑘 + 1) − 1))
158 ovex 7246 . . . . . . . . . . . . . 14 ((𝑘 + 1) − 1) ∈ V
159157, 158eqeltrdi 2846 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ0 → if((𝑘 + 1) = 0, 𝐶, ((𝑘 + 1) − 1)) ∈ V)
160149, 152, 12, 159fvmptd3 6841 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 → ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1)) = if((𝑘 + 1) = 0, 𝐶, ((𝑘 + 1) − 1)))
161 nn0cn 12100 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ0𝑘 ∈ ℂ)
162 ax-1cn 10787 . . . . . . . . . . . . 13 1 ∈ ℂ
163 pncan 11084 . . . . . . . . . . . . 13 ((𝑘 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑘 + 1) − 1) = 𝑘)
164161, 162, 163sylancl 589 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 → ((𝑘 + 1) − 1) = 𝑘)
165160, 157, 1643eqtrd 2781 . . . . . . . . . . 11 (𝑘 ∈ ℕ0 → ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1)) = 𝑘)
166165oveq2d 7229 . . . . . . . . . 10 (𝑘 ∈ ℕ0 → ((𝑆𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1))) = ((𝑆𝑘)𝑇𝑘))
167148, 166eqtrd 2777 . . . . . . . . 9 (𝑘 ∈ ℕ0 → (𝑆‘(𝑘 + 1)) = ((𝑆𝑘)𝑇𝑘))
168167adantl 485 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → (𝑆‘(𝑘 + 1)) = ((𝑆𝑘)𝑇𝑘))
169168oveq1d 7228 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → ((𝑆‘(𝑘 + 1))𝐷(𝑆𝑘)) = (((𝑆𝑘)𝑇𝑘)𝐷(𝑆𝑘)))
170 metsym 23248 . . . . . . . 8 ((𝐷 ∈ (Met‘𝑋) ∧ ((𝑆𝑘)𝑇𝑘) ∈ 𝑋 ∧ (𝑆𝑘) ∈ 𝑋) → (((𝑆𝑘)𝑇𝑘)𝐷(𝑆𝑘)) = ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)))
171136, 86, 40, 170syl3anc 1373 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (((𝑆𝑘)𝑇𝑘)𝐷(𝑆𝑘)) = ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)))
172169, 171eqtrd 2777 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → ((𝑆‘(𝑘 + 1))𝐷(𝑆𝑘)) = ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)))
173 3cn 11911 . . . . . . . . . . . . 13 3 ∈ ℂ
1741732timesi 11968 . . . . . . . . . . . 12 (2 · 3) = (3 + 3)
175174oveq1i 7223 . . . . . . . . . . 11 ((2 · 3) − 3) = ((3 + 3) − 3)
176173, 173pncan3oi 11094 . . . . . . . . . . 11 ((3 + 3) − 3) = 3
177 df-3 11894 . . . . . . . . . . 11 3 = (2 + 1)
178175, 176, 1773eqtri 2769 . . . . . . . . . 10 ((2 · 3) − 3) = (2 + 1)
179178oveq1i 7223 . . . . . . . . 9 (((2 · 3) − 3) / (2↑(𝑘 + 1))) = ((2 + 1) / (2↑(𝑘 + 1)))
180 rpcn 12596 . . . . . . . . . . 11 ((2↑(𝑘 + 1)) ∈ ℝ+ → (2↑(𝑘 + 1)) ∈ ℂ)
181 rpne0 12602 . . . . . . . . . . 11 ((2↑(𝑘 + 1)) ∈ ℝ+ → (2↑(𝑘 + 1)) ≠ 0)
182 2cn 11905 . . . . . . . . . . . . 13 2 ∈ ℂ
183182, 173mulcli 10840 . . . . . . . . . . . 12 (2 · 3) ∈ ℂ
184 divsubdir 11526 . . . . . . . . . . . 12 (((2 · 3) ∈ ℂ ∧ 3 ∈ ℂ ∧ ((2↑(𝑘 + 1)) ∈ ℂ ∧ (2↑(𝑘 + 1)) ≠ 0)) → (((2 · 3) − 3) / (2↑(𝑘 + 1))) = (((2 · 3) / (2↑(𝑘 + 1))) − (3 / (2↑(𝑘 + 1)))))
185183, 173, 184mp3an12 1453 . . . . . . . . . . 11 (((2↑(𝑘 + 1)) ∈ ℂ ∧ (2↑(𝑘 + 1)) ≠ 0) → (((2 · 3) − 3) / (2↑(𝑘 + 1))) = (((2 · 3) / (2↑(𝑘 + 1))) − (3 / (2↑(𝑘 + 1)))))
186180, 181, 185syl2anc 587 . . . . . . . . . 10 ((2↑(𝑘 + 1)) ∈ ℝ+ → (((2 · 3) − 3) / (2↑(𝑘 + 1))) = (((2 · 3) / (2↑(𝑘 + 1))) − (3 / (2↑(𝑘 + 1)))))
18745, 186syl 17 . . . . . . . . 9 (𝑘 ∈ ℕ0 → (((2 · 3) − 3) / (2↑(𝑘 + 1))) = (((2 · 3) / (2↑(𝑘 + 1))) − (3 / (2↑(𝑘 + 1)))))
188 divdir 11515 . . . . . . . . . . . 12 ((2 ∈ ℂ ∧ 1 ∈ ℂ ∧ ((2↑(𝑘 + 1)) ∈ ℂ ∧ (2↑(𝑘 + 1)) ≠ 0)) → ((2 + 1) / (2↑(𝑘 + 1))) = ((2 / (2↑(𝑘 + 1))) + (1 / (2↑(𝑘 + 1)))))
189182, 162, 188mp3an12 1453 . . . . . . . . . . 11 (((2↑(𝑘 + 1)) ∈ ℂ ∧ (2↑(𝑘 + 1)) ≠ 0) → ((2 + 1) / (2↑(𝑘 + 1))) = ((2 / (2↑(𝑘 + 1))) + (1 / (2↑(𝑘 + 1)))))
190180, 181, 189syl2anc 587 . . . . . . . . . 10 ((2↑(𝑘 + 1)) ∈ ℝ+ → ((2 + 1) / (2↑(𝑘 + 1))) = ((2 / (2↑(𝑘 + 1))) + (1 / (2↑(𝑘 + 1)))))
19145, 190syl 17 . . . . . . . . 9 (𝑘 ∈ ℕ0 → ((2 + 1) / (2↑(𝑘 + 1))) = ((2 / (2↑(𝑘 + 1))) + (1 / (2↑(𝑘 + 1)))))
192179, 187, 1913eqtr3a 2802 . . . . . . . 8 (𝑘 ∈ ℕ0 → (((2 · 3) / (2↑(𝑘 + 1))) − (3 / (2↑(𝑘 + 1)))) = ((2 / (2↑(𝑘 + 1))) + (1 / (2↑(𝑘 + 1)))))
193 rpcn 12596 . . . . . . . . . . . 12 ((2↑𝑘) ∈ ℝ+ → (2↑𝑘) ∈ ℂ)
194 rpne0 12602 . . . . . . . . . . . 12 ((2↑𝑘) ∈ ℝ+ → (2↑𝑘) ≠ 0)
195 2cnne0 12040 . . . . . . . . . . . . 13 (2 ∈ ℂ ∧ 2 ≠ 0)
196 divcan5 11534 . . . . . . . . . . . . 13 ((3 ∈ ℂ ∧ ((2↑𝑘) ∈ ℂ ∧ (2↑𝑘) ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · 3) / (2 · (2↑𝑘))) = (3 / (2↑𝑘)))
197173, 195, 196mp3an13 1454 . . . . . . . . . . . 12 (((2↑𝑘) ∈ ℂ ∧ (2↑𝑘) ≠ 0) → ((2 · 3) / (2 · (2↑𝑘))) = (3 / (2↑𝑘)))
198193, 194, 197syl2anc 587 . . . . . . . . . . 11 ((2↑𝑘) ∈ ℝ+ → ((2 · 3) / (2 · (2↑𝑘))) = (3 / (2↑𝑘)))
19951, 198syl 17 . . . . . . . . . 10 (𝑘 ∈ ℕ0 → ((2 · 3) / (2 · (2↑𝑘))) = (3 / (2↑𝑘)))
20051, 193syl 17 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ0 → (2↑𝑘) ∈ ℂ)
201 mulcom 10815 . . . . . . . . . . . . 13 ((2 ∈ ℂ ∧ (2↑𝑘) ∈ ℂ) → (2 · (2↑𝑘)) = ((2↑𝑘) · 2))
202182, 200, 201sylancr 590 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 → (2 · (2↑𝑘)) = ((2↑𝑘) · 2))
203 expp1 13642 . . . . . . . . . . . . 13 ((2 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (2↑(𝑘 + 1)) = ((2↑𝑘) · 2))
204182, 203mpan 690 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 → (2↑(𝑘 + 1)) = ((2↑𝑘) · 2))
205202, 204eqtr4d 2780 . . . . . . . . . . 11 (𝑘 ∈ ℕ0 → (2 · (2↑𝑘)) = (2↑(𝑘 + 1)))
206205oveq2d 7229 . . . . . . . . . 10 (𝑘 ∈ ℕ0 → ((2 · 3) / (2 · (2↑𝑘))) = ((2 · 3) / (2↑(𝑘 + 1))))
207199, 206eqtr3d 2779 . . . . . . . . 9 (𝑘 ∈ ℕ0 → (3 / (2↑𝑘)) = ((2 · 3) / (2↑(𝑘 + 1))))
208207oveq1d 7228 . . . . . . . 8 (𝑘 ∈ ℕ0 → ((3 / (2↑𝑘)) − (3 / (2↑(𝑘 + 1)))) = (((2 · 3) / (2↑(𝑘 + 1))) − (3 / (2↑(𝑘 + 1)))))
209 divcan5 11534 . . . . . . . . . . . . 13 ((1 ∈ ℂ ∧ ((2↑𝑘) ∈ ℂ ∧ (2↑𝑘) ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · 1) / (2 · (2↑𝑘))) = (1 / (2↑𝑘)))
210162, 195, 209mp3an13 1454 . . . . . . . . . . . 12 (((2↑𝑘) ∈ ℂ ∧ (2↑𝑘) ≠ 0) → ((2 · 1) / (2 · (2↑𝑘))) = (1 / (2↑𝑘)))
211193, 194, 210syl2anc 587 . . . . . . . . . . 11 ((2↑𝑘) ∈ ℝ+ → ((2 · 1) / (2 · (2↑𝑘))) = (1 / (2↑𝑘)))
21251, 211syl 17 . . . . . . . . . 10 (𝑘 ∈ ℕ0 → ((2 · 1) / (2 · (2↑𝑘))) = (1 / (2↑𝑘)))
213 2t1e2 11993 . . . . . . . . . . . 12 (2 · 1) = 2
214213a1i 11 . . . . . . . . . . 11 (𝑘 ∈ ℕ0 → (2 · 1) = 2)
215214, 205oveq12d 7231 . . . . . . . . . 10 (𝑘 ∈ ℕ0 → ((2 · 1) / (2 · (2↑𝑘))) = (2 / (2↑(𝑘 + 1))))
216212, 215eqtr3d 2779 . . . . . . . . 9 (𝑘 ∈ ℕ0 → (1 / (2↑𝑘)) = (2 / (2↑(𝑘 + 1))))
217216oveq1d 7228 . . . . . . . 8 (𝑘 ∈ ℕ0 → ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) = ((2 / (2↑(𝑘 + 1))) + (1 / (2↑(𝑘 + 1)))))
218192, 208, 2173eqtr4d 2787 . . . . . . 7 (𝑘 ∈ ℕ0 → ((3 / (2↑𝑘)) − (3 / (2↑(𝑘 + 1)))) = ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))))
219218adantl 485 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → ((3 / (2↑𝑘)) − (3 / (2↑(𝑘 + 1)))) = ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))))
220141, 172, 2193brtr4d 5085 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → ((𝑆‘(𝑘 + 1))𝐷(𝑆𝑘)) ≤ ((3 / (2↑𝑘)) − (3 / (2↑(𝑘 + 1)))))
221 blss2 23302 . . . . 5 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑆‘(𝑘 + 1)) ∈ 𝑋 ∧ (𝑆𝑘) ∈ 𝑋) ∧ ((3 / (2↑(𝑘 + 1))) ∈ ℝ ∧ (3 / (2↑𝑘)) ∈ ℝ ∧ ((𝑆‘(𝑘 + 1))𝐷(𝑆𝑘)) ≤ ((3 / (2↑𝑘)) − (3 / (2↑(𝑘 + 1)))))) → ((𝑆‘(𝑘 + 1))(ball‘𝐷)(3 / (2↑(𝑘 + 1)))) ⊆ ((𝑆𝑘)(ball‘𝐷)(3 / (2↑𝑘))))
2227, 31, 40, 48, 54, 220, 221syl33anc 1387 . . . 4 ((𝜑𝑘 ∈ ℕ0) → ((𝑆‘(𝑘 + 1))(ball‘𝐷)(3 / (2↑(𝑘 + 1)))) ⊆ ((𝑆𝑘)(ball‘𝐷)(3 / (2↑𝑘))))
2231, 222sylan2 596 . . 3 ((𝜑𝑘 ∈ ℕ) → ((𝑆‘(𝑘 + 1))(ball‘𝐷)(3 / (2↑(𝑘 + 1)))) ⊆ ((𝑆𝑘)(ball‘𝐷)(3 / (2↑𝑘))))
224 peano2nn 11842 . . . . . . 7 (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
225 fveq2 6717 . . . . . . . . 9 (𝑛 = (𝑘 + 1) → (𝑆𝑛) = (𝑆‘(𝑘 + 1)))
226 oveq2 7221 . . . . . . . . . 10 (𝑛 = (𝑘 + 1) → (2↑𝑛) = (2↑(𝑘 + 1)))
227226oveq2d 7229 . . . . . . . . 9 (𝑛 = (𝑘 + 1) → (3 / (2↑𝑛)) = (3 / (2↑(𝑘 + 1))))
228225, 227opeq12d 4792 . . . . . . . 8 (𝑛 = (𝑘 + 1) → ⟨(𝑆𝑛), (3 / (2↑𝑛))⟩ = ⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩)
229 heibor.12 . . . . . . . 8 𝑀 = (𝑛 ∈ ℕ ↦ ⟨(𝑆𝑛), (3 / (2↑𝑛))⟩)
230 opex 5348 . . . . . . . 8 ⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩ ∈ V
231228, 229, 230fvmpt 6818 . . . . . . 7 ((𝑘 + 1) ∈ ℕ → (𝑀‘(𝑘 + 1)) = ⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩)
232224, 231syl 17 . . . . . 6 (𝑘 ∈ ℕ → (𝑀‘(𝑘 + 1)) = ⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩)
233232adantl 485 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (𝑀‘(𝑘 + 1)) = ⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩)
234233fveq2d 6721 . . . 4 ((𝜑𝑘 ∈ ℕ) → ((ball‘𝐷)‘(𝑀‘(𝑘 + 1))) = ((ball‘𝐷)‘⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩))
235 df-ov 7216 . . . 4 ((𝑆‘(𝑘 + 1))(ball‘𝐷)(3 / (2↑(𝑘 + 1)))) = ((ball‘𝐷)‘⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩)
236234, 235eqtr4di 2796 . . 3 ((𝜑𝑘 ∈ ℕ) → ((ball‘𝐷)‘(𝑀‘(𝑘 + 1))) = ((𝑆‘(𝑘 + 1))(ball‘𝐷)(3 / (2↑(𝑘 + 1)))))
237 fveq2 6717 . . . . . . . 8 (𝑛 = 𝑘 → (𝑆𝑛) = (𝑆𝑘))
238 oveq2 7221 . . . . . . . . 9 (𝑛 = 𝑘 → (2↑𝑛) = (2↑𝑘))
239238oveq2d 7229 . . . . . . . 8 (𝑛 = 𝑘 → (3 / (2↑𝑛)) = (3 / (2↑𝑘)))
240237, 239opeq12d 4792 . . . . . . 7 (𝑛 = 𝑘 → ⟨(𝑆𝑛), (3 / (2↑𝑛))⟩ = ⟨(𝑆𝑘), (3 / (2↑𝑘))⟩)
241 opex 5348 . . . . . . 7 ⟨(𝑆𝑘), (3 / (2↑𝑘))⟩ ∈ V
242240, 229, 241fvmpt 6818 . . . . . 6 (𝑘 ∈ ℕ → (𝑀𝑘) = ⟨(𝑆𝑘), (3 / (2↑𝑘))⟩)
243242fveq2d 6721 . . . . 5 (𝑘 ∈ ℕ → ((ball‘𝐷)‘(𝑀𝑘)) = ((ball‘𝐷)‘⟨(𝑆𝑘), (3 / (2↑𝑘))⟩))
244 df-ov 7216 . . . . 5 ((𝑆𝑘)(ball‘𝐷)(3 / (2↑𝑘))) = ((ball‘𝐷)‘⟨(𝑆𝑘), (3 / (2↑𝑘))⟩)
245243, 244eqtr4di 2796 . . . 4 (𝑘 ∈ ℕ → ((ball‘𝐷)‘(𝑀𝑘)) = ((𝑆𝑘)(ball‘𝐷)(3 / (2↑𝑘))))
246245adantl 485 . . 3 ((𝜑𝑘 ∈ ℕ) → ((ball‘𝐷)‘(𝑀𝑘)) = ((𝑆𝑘)(ball‘𝐷)(3 / (2↑𝑘))))
247223, 236, 2463sstr4d 3948 . 2 ((𝜑𝑘 ∈ ℕ) → ((ball‘𝐷)‘(𝑀‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝑀𝑘)))
248247ralrimiva 3105 1 (𝜑 → ∀𝑘 ∈ ℕ ((ball‘𝐷)‘(𝑀‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝑀𝑘)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 399  w3a 1089   = wceq 1543  wcel 2110  {cab 2714  wne 2940  wral 3061  wrex 3062  Vcvv 3408  cin 3865  wss 3866  c0 4237  ifcif 4439  𝒫 cpw 4513  cop 4547   cuni 4819   ciun 4904   class class class wbr 5053  {copab 5115  cmpt 5135  wf 6376  cfv 6380  (class class class)co 7213  cmpo 7215  2nd c2nd 7760  Fincfn 8626  cc 10727  cr 10728  0cc0 10729  1c1 10730   + caddc 10732   · cmul 10734  *cxr 10866  cle 10868  cmin 11062   / cdiv 11489  cn 11830  2c2 11885  3c3 11886  0cn0 12090  cuz 12438  +crp 12586   +𝑒 cxad 12702  seqcseq 13574  cexp 13635  ∞Metcxmet 20348  Metcmet 20349  ballcbl 20350  MetOpencmopn 20353  CMetccmet 24151
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523  ax-cnex 10785  ax-resscn 10786  ax-1cn 10787  ax-icn 10788  ax-addcl 10789  ax-addrcl 10790  ax-mulcl 10791  ax-mulrcl 10792  ax-mulcom 10793  ax-addass 10794  ax-mulass 10795  ax-distr 10796  ax-i2m1 10797  ax-1ne0 10798  ax-1rid 10799  ax-rnegex 10800  ax-rrecex 10801  ax-cnre 10802  ax-pre-lttri 10803  ax-pre-lttrn 10804  ax-pre-ltadd 10805  ax-pre-mulgt0 10806
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-pss 3885  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-tp 4546  df-op 4548  df-uni 4820  df-iun 4906  df-br 5054  df-opab 5116  df-mpt 5136  df-tr 5162  df-id 5455  df-eprel 5460  df-po 5468  df-so 5469  df-fr 5509  df-we 5511  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-pred 6160  df-ord 6216  df-on 6217  df-lim 6218  df-suc 6219  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-riota 7170  df-ov 7216  df-oprab 7217  df-mpo 7218  df-om 7645  df-1st 7761  df-2nd 7762  df-wrecs 8047  df-recs 8108  df-rdg 8146  df-er 8391  df-map 8510  df-en 8627  df-dom 8628  df-sdom 8629  df-fin 8630  df-pnf 10869  df-mnf 10870  df-xr 10871  df-ltxr 10872  df-le 10873  df-sub 11064  df-neg 11065  df-div 11490  df-nn 11831  df-2 11893  df-3 11894  df-n0 12091  df-z 12177  df-uz 12439  df-rp 12587  df-xneg 12704  df-xadd 12705  df-xmul 12706  df-seq 13575  df-exp 13636  df-psmet 20355  df-xmet 20356  df-met 20357  df-bl 20358  df-cmet 24154
This theorem is referenced by:  heiborlem8  35713  heiborlem9  35714
  Copyright terms: Public domain W3C validator