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 36275
Description: Lemma for heibor 36280. 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 12420 . . . 4 (𝑘 ∈ ℕ → 𝑘 ∈ ℕ0)
2 heibor.6 . . . . . . . 8 (𝜑𝐷 ∈ (CMet‘𝑋))
3 cmetmet 24650 . . . . . . . 8 (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋))
42, 3syl 17 . . . . . . 7 (𝜑𝐷 ∈ (Met‘𝑋))
5 metxmet 23687 . . . . . . 7 (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋))
64, 5syl 17 . . . . . 6 (𝜑𝐷 ∈ (∞Met‘𝑋))
76adantr 481 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → 𝐷 ∈ (∞Met‘𝑋))
8 heibor.7 . . . . . . . . 9 (𝜑𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin))
9 inss1 4188 . . . . . . . . 9 (𝒫 𝑋 ∩ Fin) ⊆ 𝒫 𝑋
10 fss 6685 . . . . . . . . 9 ((𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin) ∧ (𝒫 𝑋 ∩ Fin) ⊆ 𝒫 𝑋) → 𝐹:ℕ0⟶𝒫 𝑋)
118, 9, 10sylancl 586 . . . . . . . 8 (𝜑𝐹:ℕ0⟶𝒫 𝑋)
12 peano2nn0 12453 . . . . . . . 8 (𝑘 ∈ ℕ0 → (𝑘 + 1) ∈ ℕ0)
13 ffvelcdm 7032 . . . . . . . 8 ((𝐹:ℕ0⟶𝒫 𝑋 ∧ (𝑘 + 1) ∈ ℕ0) → (𝐹‘(𝑘 + 1)) ∈ 𝒫 𝑋)
1411, 12, 13syl2an 596 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (𝐹‘(𝑘 + 1)) ∈ 𝒫 𝑋)
1514elpwid 4569 . . . . . 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 36273 . . . . . . . 8 ((𝜑 ∧ (𝑘 + 1) ∈ ℕ0) → (𝑆‘(𝑘 + 1))𝐺(𝑘 + 1))
2512, 24sylan2 593 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (𝑆‘(𝑘 + 1))𝐺(𝑘 + 1))
26 fvex 6855 . . . . . . . . 9 (𝑆‘(𝑘 + 1)) ∈ V
27 ovex 7390 . . . . . . . . 9 (𝑘 + 1) ∈ V
2816, 17, 18, 26, 27heiborlem2 36271 . . . . . . . 8 ((𝑆‘(𝑘 + 1))𝐺(𝑘 + 1) ↔ ((𝑘 + 1) ∈ ℕ0 ∧ (𝑆‘(𝑘 + 1)) ∈ (𝐹‘(𝑘 + 1)) ∧ ((𝑆‘(𝑘 + 1))𝐵(𝑘 + 1)) ∈ 𝐾))
2928simp2bi 1146 . . . . . . 7 ((𝑆‘(𝑘 + 1))𝐺(𝑘 + 1) → (𝑆‘(𝑘 + 1)) ∈ (𝐹‘(𝑘 + 1)))
3025, 29syl 17 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (𝑆‘(𝑘 + 1)) ∈ (𝐹‘(𝑘 + 1)))
3115, 30sseldd 3945 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → (𝑆‘(𝑘 + 1)) ∈ 𝑋)
3211ffvelcdmda 7035 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (𝐹𝑘) ∈ 𝒫 𝑋)
3332elpwid 4569 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (𝐹𝑘) ⊆ 𝑋)
3416, 17, 18, 19, 2, 8, 20, 21, 22, 23heiborlem4 36273 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (𝑆𝑘)𝐺𝑘)
35 fvex 6855 . . . . . . . . 9 (𝑆𝑘) ∈ V
36 vex 3449 . . . . . . . . 9 𝑘 ∈ V
3716, 17, 18, 35, 36heiborlem2 36271 . . . . . . . 8 ((𝑆𝑘)𝐺𝑘 ↔ (𝑘 ∈ ℕ0 ∧ (𝑆𝑘) ∈ (𝐹𝑘) ∧ ((𝑆𝑘)𝐵𝑘) ∈ 𝐾))
3837simp2bi 1146 . . . . . . 7 ((𝑆𝑘)𝐺𝑘 → (𝑆𝑘) ∈ (𝐹𝑘))
3934, 38syl 17 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (𝑆𝑘) ∈ (𝐹𝑘))
4033, 39sseldd 3945 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → (𝑆𝑘) ∈ 𝑋)
41 3re 12233 . . . . . 6 3 ∈ ℝ
42 2nn 12226 . . . . . . . . 9 2 ∈ ℕ
43 nnexpcl 13980 . . . . . . . . 9 ((2 ∈ ℕ ∧ (𝑘 + 1) ∈ ℕ0) → (2↑(𝑘 + 1)) ∈ ℕ)
4442, 12, 43sylancr 587 . . . . . . . 8 (𝑘 ∈ ℕ0 → (2↑(𝑘 + 1)) ∈ ℕ)
4544nnrpd 12955 . . . . . . 7 (𝑘 ∈ ℕ0 → (2↑(𝑘 + 1)) ∈ ℝ+)
4645adantl 482 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (2↑(𝑘 + 1)) ∈ ℝ+)
47 rerpdivcl 12945 . . . . . 6 ((3 ∈ ℝ ∧ (2↑(𝑘 + 1)) ∈ ℝ+) → (3 / (2↑(𝑘 + 1))) ∈ ℝ)
4841, 46, 47sylancr 587 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → (3 / (2↑(𝑘 + 1))) ∈ ℝ)
49 nnexpcl 13980 . . . . . . . . 9 ((2 ∈ ℕ ∧ 𝑘 ∈ ℕ0) → (2↑𝑘) ∈ ℕ)
5042, 49mpan 688 . . . . . . . 8 (𝑘 ∈ ℕ0 → (2↑𝑘) ∈ ℕ)
5150nnrpd 12955 . . . . . . 7 (𝑘 ∈ ℕ0 → (2↑𝑘) ∈ ℝ+)
5251adantl 482 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (2↑𝑘) ∈ ℝ+)
53 rerpdivcl 12945 . . . . . 6 ((3 ∈ ℝ ∧ (2↑𝑘) ∈ ℝ+) → (3 / (2↑𝑘)) ∈ ℝ)
5441, 52, 53sylancr 587 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → (3 / (2↑𝑘)) ∈ ℝ)
55 oveq1 7364 . . . . . . . . . . . 12 (𝑧 = (𝑆𝑘) → (𝑧(ball‘𝐷)(1 / (2↑𝑚))) = ((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑚))))
56 oveq2 7365 . . . . . . . . . . . . . 14 (𝑚 = 𝑘 → (2↑𝑚) = (2↑𝑘))
5756oveq2d 7373 . . . . . . . . . . . . 13 (𝑚 = 𝑘 → (1 / (2↑𝑚)) = (1 / (2↑𝑘)))
5857oveq2d 7373 . . . . . . . . . . . 12 (𝑚 = 𝑘 → ((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑚))) = ((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑘))))
59 ovex 7390 . . . . . . . . . . . 12 ((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∈ V
6055, 58, 19, 59ovmpo 7515 . . . . . . . . . . 11 (((𝑆𝑘) ∈ 𝑋𝑘 ∈ ℕ0) → ((𝑆𝑘)𝐵𝑘) = ((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑘))))
6140, 60sylancom 588 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → ((𝑆𝑘)𝐵𝑘) = ((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑘))))
62 df-br 5106 . . . . . . . . . . . . . . . . 17 ((𝑆𝑘)𝐺𝑘 ↔ ⟨(𝑆𝑘), 𝑘⟩ ∈ 𝐺)
63 fveq2 6842 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = ⟨(𝑆𝑘), 𝑘⟩ → (𝑇𝑥) = (𝑇‘⟨(𝑆𝑘), 𝑘⟩))
64 df-ov 7360 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑆𝑘)𝑇𝑘) = (𝑇‘⟨(𝑆𝑘), 𝑘⟩)
6563, 64eqtr4di 2794 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = ⟨(𝑆𝑘), 𝑘⟩ → (𝑇𝑥) = ((𝑆𝑘)𝑇𝑘))
6635, 36op2ndd 7932 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = ⟨(𝑆𝑘), 𝑘⟩ → (2nd𝑥) = 𝑘)
6766oveq1d 7372 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = ⟨(𝑆𝑘), 𝑘⟩ → ((2nd𝑥) + 1) = (𝑘 + 1))
6865, 67breq12d 5118 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = ⟨(𝑆𝑘), 𝑘⟩ → ((𝑇𝑥)𝐺((2nd𝑥) + 1) ↔ ((𝑆𝑘)𝑇𝑘)𝐺(𝑘 + 1)))
69 fveq2 6842 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = ⟨(𝑆𝑘), 𝑘⟩ → (𝐵𝑥) = (𝐵‘⟨(𝑆𝑘), 𝑘⟩))
70 df-ov 7360 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑆𝑘)𝐵𝑘) = (𝐵‘⟨(𝑆𝑘), 𝑘⟩)
7169, 70eqtr4di 2794 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = ⟨(𝑆𝑘), 𝑘⟩ → (𝐵𝑥) = ((𝑆𝑘)𝐵𝑘))
7265, 67oveq12d 7375 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = ⟨(𝑆𝑘), 𝑘⟩ → ((𝑇𝑥)𝐵((2nd𝑥) + 1)) = (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1)))
7371, 72ineq12d 4173 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = ⟨(𝑆𝑘), 𝑘⟩ → ((𝐵𝑥) ∩ ((𝑇𝑥)𝐵((2nd𝑥) + 1))) = (((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))))
7473eleq1d 2822 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = ⟨(𝑆𝑘), 𝑘⟩ → (((𝐵𝑥) ∩ ((𝑇𝑥)𝐵((2nd𝑥) + 1))) ∈ 𝐾 ↔ (((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾))
7568, 74anbi12d 631 . . . . . . . . . . . . . . . . . . 19 (𝑥 = ⟨(𝑆𝑘), 𝑘⟩ → (((𝑇𝑥)𝐺((2nd𝑥) + 1) ∧ ((𝐵𝑥) ∩ ((𝑇𝑥)𝐵((2nd𝑥) + 1))) ∈ 𝐾) ↔ (((𝑆𝑘)𝑇𝑘)𝐺(𝑘 + 1) ∧ (((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾)))
7675rspccv 3578 . . . . . . . . . . . . . . . . . 18 (∀𝑥𝐺 ((𝑇𝑥)𝐺((2nd𝑥) + 1) ∧ ((𝐵𝑥) ∩ ((𝑇𝑥)𝐵((2nd𝑥) + 1))) ∈ 𝐾) → (⟨(𝑆𝑘), 𝑘⟩ ∈ 𝐺 → (((𝑆𝑘)𝑇𝑘)𝐺(𝑘 + 1) ∧ (((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾)))
7721, 76syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (⟨(𝑆𝑘), 𝑘⟩ ∈ 𝐺 → (((𝑆𝑘)𝑇𝑘)𝐺(𝑘 + 1) ∧ (((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾)))
7862, 77biimtrid 241 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑆𝑘)𝐺𝑘 → (((𝑆𝑘)𝑇𝑘)𝐺(𝑘 + 1) ∧ (((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾)))
7978adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ℕ0) → ((𝑆𝑘)𝐺𝑘 → (((𝑆𝑘)𝑇𝑘)𝐺(𝑘 + 1) ∧ (((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾)))
8034, 79mpd 15 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ℕ0) → (((𝑆𝑘)𝑇𝑘)𝐺(𝑘 + 1) ∧ (((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾))
8180simpld 495 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ0) → ((𝑆𝑘)𝑇𝑘)𝐺(𝑘 + 1))
82 ovex 7390 . . . . . . . . . . . . . . 15 ((𝑆𝑘)𝑇𝑘) ∈ V
8316, 17, 18, 82, 27heiborlem2 36271 . . . . . . . . . . . . . 14 (((𝑆𝑘)𝑇𝑘)𝐺(𝑘 + 1) ↔ ((𝑘 + 1) ∈ ℕ0 ∧ ((𝑆𝑘)𝑇𝑘) ∈ (𝐹‘(𝑘 + 1)) ∧ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1)) ∈ 𝐾))
8483simp2bi 1146 . . . . . . . . . . . . 13 (((𝑆𝑘)𝑇𝑘)𝐺(𝑘 + 1) → ((𝑆𝑘)𝑇𝑘) ∈ (𝐹‘(𝑘 + 1)))
8581, 84syl 17 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → ((𝑆𝑘)𝑇𝑘) ∈ (𝐹‘(𝑘 + 1)))
8615, 85sseldd 3945 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → ((𝑆𝑘)𝑇𝑘) ∈ 𝑋)
8712adantl 482 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → (𝑘 + 1) ∈ ℕ0)
88 oveq1 7364 . . . . . . . . . . . 12 (𝑧 = ((𝑆𝑘)𝑇𝑘) → (𝑧(ball‘𝐷)(1 / (2↑𝑚))) = (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑𝑚))))
89 oveq2 7365 . . . . . . . . . . . . . 14 (𝑚 = (𝑘 + 1) → (2↑𝑚) = (2↑(𝑘 + 1)))
9089oveq2d 7373 . . . . . . . . . . . . 13 (𝑚 = (𝑘 + 1) → (1 / (2↑𝑚)) = (1 / (2↑(𝑘 + 1))))
9190oveq2d 7373 . . . . . . . . . . . 12 (𝑚 = (𝑘 + 1) → (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑𝑚))) = (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1)))))
92 ovex 7390 . . . . . . . . . . . 12 (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1)))) ∈ V
9388, 91, 19, 92ovmpo 7515 . . . . . . . . . . 11 ((((𝑆𝑘)𝑇𝑘) ∈ 𝑋 ∧ (𝑘 + 1) ∈ ℕ0) → (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1)) = (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1)))))
9486, 87, 93syl2anc 584 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1)) = (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1)))))
9561, 94ineq12d 4173 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → (((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))) = (((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))))
9680simprd 496 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → (((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾)
97 0elpw 5311 . . . . . . . . . . . . 13 ∅ ∈ 𝒫 𝑈
98 0fin 9115 . . . . . . . . . . . . 13 ∅ ∈ Fin
99 elin 3926 . . . . . . . . . . . . 13 (∅ ∈ (𝒫 𝑈 ∩ Fin) ↔ (∅ ∈ 𝒫 𝑈 ∧ ∅ ∈ Fin))
10097, 98, 99mpbir2an 709 . . . . . . . . . . . 12 ∅ ∈ (𝒫 𝑈 ∩ Fin)
101 0ss 4356 . . . . . . . . . . . 12 ∅ ⊆
102 unieq 4876 . . . . . . . . . . . . . 14 (𝑣 = ∅ → 𝑣 = ∅)
103102sseq2d 3976 . . . . . . . . . . . . 13 (𝑣 = ∅ → (∅ ⊆ 𝑣 ↔ ∅ ⊆ ∅))
104103rspcev 3581 . . . . . . . . . . . 12 ((∅ ∈ (𝒫 𝑈 ∩ Fin) ∧ ∅ ⊆ ∅) → ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ 𝑣)
105100, 101, 104mp2an 690 . . . . . . . . . . 11 𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ 𝑣
106 0ex 5264 . . . . . . . . . . . . 13 ∅ ∈ V
107 sseq1 3969 . . . . . . . . . . . . . . 15 (𝑢 = ∅ → (𝑢 𝑣 ↔ ∅ ⊆ 𝑣))
108107rexbidv 3175 . . . . . . . . . . . . . 14 (𝑢 = ∅ → (∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 𝑣 ↔ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ 𝑣))
109108notbid 317 . . . . . . . . . . . . 13 (𝑢 = ∅ → (¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 𝑣 ↔ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ 𝑣))
110106, 109, 17elab2 3634 . . . . . . . . . . . 12 (∅ ∈ 𝐾 ↔ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ 𝑣)
111110con2bii 357 . . . . . . . . . . 11 (∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ 𝑣 ↔ ¬ ∅ ∈ 𝐾)
112105, 111mpbi 229 . . . . . . . . . 10 ¬ ∅ ∈ 𝐾
113 nelne2 3042 . . . . . . . . . 10 (((((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾 ∧ ¬ ∅ ∈ 𝐾) → (((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ≠ ∅)
11496, 112, 113sylancl 586 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → (((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ≠ ∅)
11595, 114eqnetrrd 3012 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → (((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))) ≠ ∅)
11651rpreccld 12967 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ0 → (1 / (2↑𝑘)) ∈ ℝ+)
117116adantl 482 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ0) → (1 / (2↑𝑘)) ∈ ℝ+)
118117rpred 12957 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → (1 / (2↑𝑘)) ∈ ℝ)
11945rpreccld 12967 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ0 → (1 / (2↑(𝑘 + 1))) ∈ ℝ+)
120119adantl 482 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ0) → (1 / (2↑(𝑘 + 1))) ∈ ℝ+)
121120rpred 12957 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → (1 / (2↑(𝑘 + 1))) ∈ ℝ)
122 rexadd 13151 . . . . . . . . . . . 12 (((1 / (2↑𝑘)) ∈ ℝ ∧ (1 / (2↑(𝑘 + 1))) ∈ ℝ) → ((1 / (2↑𝑘)) +𝑒 (1 / (2↑(𝑘 + 1)))) = ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))))
123118, 121, 122syl2anc 584 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → ((1 / (2↑𝑘)) +𝑒 (1 / (2↑(𝑘 + 1)))) = ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))))
124123breq1d 5115 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → (((1 / (2↑𝑘)) +𝑒 (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)) ↔ ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘))))
125117rpxrd 12958 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → (1 / (2↑𝑘)) ∈ ℝ*)
126120rpxrd 12958 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → (1 / (2↑(𝑘 + 1))) ∈ ℝ*)
127 bldisj 23751 . . . . . . . . . . . . 13 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑆𝑘) ∈ 𝑋 ∧ ((𝑆𝑘)𝑇𝑘) ∈ 𝑋) ∧ ((1 / (2↑𝑘)) ∈ ℝ* ∧ (1 / (2↑(𝑘 + 1))) ∈ ℝ* ∧ ((1 / (2↑𝑘)) +𝑒 (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)))) → (((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))) = ∅)
1281273exp2 1354 . . . . . . . . . . . 12 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑆𝑘) ∈ 𝑋 ∧ ((𝑆𝑘)𝑇𝑘) ∈ 𝑋) → ((1 / (2↑𝑘)) ∈ ℝ* → ((1 / (2↑(𝑘 + 1))) ∈ ℝ* → (((1 / (2↑𝑘)) +𝑒 (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)) → (((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))) = ∅))))
129128imp32 419 . . . . . . . . . . 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 1378 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → (((1 / (2↑𝑘)) +𝑒 (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)) → (((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))) = ∅))
131124, 130sylbird 259 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → (((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)) → (((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))) = ∅))
132131necon3ad 2956 . . . . . . . 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 12972 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ∈ ℝ+)
135134rpred 12957 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ∈ ℝ)
1364adantr 481 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → 𝐷 ∈ (Met‘𝑋))
137 metcl 23685 . . . . . . . . . 10 ((𝐷 ∈ (Met‘𝑋) ∧ (𝑆𝑘) ∈ 𝑋 ∧ ((𝑆𝑘)𝑇𝑘) ∈ 𝑋) → ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)) ∈ ℝ)
138136, 40, 86, 137syl3anc 1371 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)) ∈ ℝ)
139135, 138letrid 11307 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → (((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)) ∨ ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)) ≤ ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1))))))
140139ord 862 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (¬ ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)) → ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)) ≤ ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1))))))
141133, 140mpd 15 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)) ≤ ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))))
142 seqp1 13921 . . . . . . . . . . . 12 (𝑘 ∈ (ℤ‘0) → (seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘(𝑘 + 1)) = ((seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1))))
143 nn0uz 12805 . . . . . . . . . . . 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 6843 . . . . . . . . . . 11 (𝑆‘(𝑘 + 1)) = (seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘(𝑘 + 1))
14623fveq1i 6843 . . . . . . . . . . . 12 (𝑆𝑘) = (seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘𝑘)
147146oveq1i 7367 . . . . . . . . . . 11 ((𝑆𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1))) = ((seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1)))
148144, 145, 1473eqtr4g 2801 . . . . . . . . . 10 (𝑘 ∈ ℕ0 → (𝑆‘(𝑘 + 1)) = ((𝑆𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1))))
149 eqid 2736 . . . . . . . . . . . . 13 (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))) = (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))
150 eqeq1 2740 . . . . . . . . . . . . . 14 (𝑚 = (𝑘 + 1) → (𝑚 = 0 ↔ (𝑘 + 1) = 0))
151 oveq1 7364 . . . . . . . . . . . . . 14 (𝑚 = (𝑘 + 1) → (𝑚 − 1) = ((𝑘 + 1) − 1))
152150, 151ifbieq2d 4512 . . . . . . . . . . . . 13 (𝑚 = (𝑘 + 1) → if(𝑚 = 0, 𝐶, (𝑚 − 1)) = if((𝑘 + 1) = 0, 𝐶, ((𝑘 + 1) − 1)))
153 nn0p1nn 12452 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℕ0 → (𝑘 + 1) ∈ ℕ)
154 nnne0 12187 . . . . . . . . . . . . . . . . 17 ((𝑘 + 1) ∈ ℕ → (𝑘 + 1) ≠ 0)
155154neneqd 2948 . . . . . . . . . . . . . . . 16 ((𝑘 + 1) ∈ ℕ → ¬ (𝑘 + 1) = 0)
156153, 155syl 17 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℕ0 → ¬ (𝑘 + 1) = 0)
157156iffalsed 4497 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ0 → if((𝑘 + 1) = 0, 𝐶, ((𝑘 + 1) − 1)) = ((𝑘 + 1) − 1))
158 ovex 7390 . . . . . . . . . . . . . 14 ((𝑘 + 1) − 1) ∈ V
159157, 158eqeltrdi 2846 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ0 → if((𝑘 + 1) = 0, 𝐶, ((𝑘 + 1) − 1)) ∈ V)
160149, 152, 12, 159fvmptd3 6971 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 → ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1)) = if((𝑘 + 1) = 0, 𝐶, ((𝑘 + 1) − 1)))
161 nn0cn 12423 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ0𝑘 ∈ ℂ)
162 ax-1cn 11109 . . . . . . . . . . . . 13 1 ∈ ℂ
163 pncan 11407 . . . . . . . . . . . . 13 ((𝑘 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑘 + 1) − 1) = 𝑘)
164161, 162, 163sylancl 586 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 → ((𝑘 + 1) − 1) = 𝑘)
165160, 157, 1643eqtrd 2780 . . . . . . . . . . 11 (𝑘 ∈ ℕ0 → ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1)) = 𝑘)
166165oveq2d 7373 . . . . . . . . . 10 (𝑘 ∈ ℕ0 → ((𝑆𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1))) = ((𝑆𝑘)𝑇𝑘))
167148, 166eqtrd 2776 . . . . . . . . 9 (𝑘 ∈ ℕ0 → (𝑆‘(𝑘 + 1)) = ((𝑆𝑘)𝑇𝑘))
168167adantl 482 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → (𝑆‘(𝑘 + 1)) = ((𝑆𝑘)𝑇𝑘))
169168oveq1d 7372 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → ((𝑆‘(𝑘 + 1))𝐷(𝑆𝑘)) = (((𝑆𝑘)𝑇𝑘)𝐷(𝑆𝑘)))
170 metsym 23703 . . . . . . . 8 ((𝐷 ∈ (Met‘𝑋) ∧ ((𝑆𝑘)𝑇𝑘) ∈ 𝑋 ∧ (𝑆𝑘) ∈ 𝑋) → (((𝑆𝑘)𝑇𝑘)𝐷(𝑆𝑘)) = ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)))
171136, 86, 40, 170syl3anc 1371 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (((𝑆𝑘)𝑇𝑘)𝐷(𝑆𝑘)) = ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)))
172169, 171eqtrd 2776 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → ((𝑆‘(𝑘 + 1))𝐷(𝑆𝑘)) = ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)))
173 3cn 12234 . . . . . . . . . . . . 13 3 ∈ ℂ
1741732timesi 12291 . . . . . . . . . . . 12 (2 · 3) = (3 + 3)
175174oveq1i 7367 . . . . . . . . . . 11 ((2 · 3) − 3) = ((3 + 3) − 3)
176173, 173pncan3oi 11417 . . . . . . . . . . 11 ((3 + 3) − 3) = 3
177 df-3 12217 . . . . . . . . . . 11 3 = (2 + 1)
178175, 176, 1773eqtri 2768 . . . . . . . . . 10 ((2 · 3) − 3) = (2 + 1)
179178oveq1i 7367 . . . . . . . . 9 (((2 · 3) − 3) / (2↑(𝑘 + 1))) = ((2 + 1) / (2↑(𝑘 + 1)))
180 rpcn 12925 . . . . . . . . . . 11 ((2↑(𝑘 + 1)) ∈ ℝ+ → (2↑(𝑘 + 1)) ∈ ℂ)
181 rpne0 12931 . . . . . . . . . . 11 ((2↑(𝑘 + 1)) ∈ ℝ+ → (2↑(𝑘 + 1)) ≠ 0)
182 2cn 12228 . . . . . . . . . . . . 13 2 ∈ ℂ
183182, 173mulcli 11162 . . . . . . . . . . . 12 (2 · 3) ∈ ℂ
184 divsubdir 11849 . . . . . . . . . . . 12 (((2 · 3) ∈ ℂ ∧ 3 ∈ ℂ ∧ ((2↑(𝑘 + 1)) ∈ ℂ ∧ (2↑(𝑘 + 1)) ≠ 0)) → (((2 · 3) − 3) / (2↑(𝑘 + 1))) = (((2 · 3) / (2↑(𝑘 + 1))) − (3 / (2↑(𝑘 + 1)))))
185183, 173, 184mp3an12 1451 . . . . . . . . . . 11 (((2↑(𝑘 + 1)) ∈ ℂ ∧ (2↑(𝑘 + 1)) ≠ 0) → (((2 · 3) − 3) / (2↑(𝑘 + 1))) = (((2 · 3) / (2↑(𝑘 + 1))) − (3 / (2↑(𝑘 + 1)))))
186180, 181, 185syl2anc 584 . . . . . . . . . 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 11838 . . . . . . . . . . . 12 ((2 ∈ ℂ ∧ 1 ∈ ℂ ∧ ((2↑(𝑘 + 1)) ∈ ℂ ∧ (2↑(𝑘 + 1)) ≠ 0)) → ((2 + 1) / (2↑(𝑘 + 1))) = ((2 / (2↑(𝑘 + 1))) + (1 / (2↑(𝑘 + 1)))))
189182, 162, 188mp3an12 1451 . . . . . . . . . . 11 (((2↑(𝑘 + 1)) ∈ ℂ ∧ (2↑(𝑘 + 1)) ≠ 0) → ((2 + 1) / (2↑(𝑘 + 1))) = ((2 / (2↑(𝑘 + 1))) + (1 / (2↑(𝑘 + 1)))))
190180, 181, 189syl2anc 584 . . . . . . . . . 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 2800 . . . . . . . 8 (𝑘 ∈ ℕ0 → (((2 · 3) / (2↑(𝑘 + 1))) − (3 / (2↑(𝑘 + 1)))) = ((2 / (2↑(𝑘 + 1))) + (1 / (2↑(𝑘 + 1)))))
193 rpcn 12925 . . . . . . . . . . . 12 ((2↑𝑘) ∈ ℝ+ → (2↑𝑘) ∈ ℂ)
194 rpne0 12931 . . . . . . . . . . . 12 ((2↑𝑘) ∈ ℝ+ → (2↑𝑘) ≠ 0)
195 2cnne0 12363 . . . . . . . . . . . . 13 (2 ∈ ℂ ∧ 2 ≠ 0)
196 divcan5 11857 . . . . . . . . . . . . 13 ((3 ∈ ℂ ∧ ((2↑𝑘) ∈ ℂ ∧ (2↑𝑘) ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · 3) / (2 · (2↑𝑘))) = (3 / (2↑𝑘)))
197173, 195, 196mp3an13 1452 . . . . . . . . . . . 12 (((2↑𝑘) ∈ ℂ ∧ (2↑𝑘) ≠ 0) → ((2 · 3) / (2 · (2↑𝑘))) = (3 / (2↑𝑘)))
198193, 194, 197syl2anc 584 . . . . . . . . . . 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 11137 . . . . . . . . . . . . 13 ((2 ∈ ℂ ∧ (2↑𝑘) ∈ ℂ) → (2 · (2↑𝑘)) = ((2↑𝑘) · 2))
202182, 200, 201sylancr 587 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 → (2 · (2↑𝑘)) = ((2↑𝑘) · 2))
203 expp1 13974 . . . . . . . . . . . . 13 ((2 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (2↑(𝑘 + 1)) = ((2↑𝑘) · 2))
204182, 203mpan 688 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 → (2↑(𝑘 + 1)) = ((2↑𝑘) · 2))
205202, 204eqtr4d 2779 . . . . . . . . . . 11 (𝑘 ∈ ℕ0 → (2 · (2↑𝑘)) = (2↑(𝑘 + 1)))
206205oveq2d 7373 . . . . . . . . . 10 (𝑘 ∈ ℕ0 → ((2 · 3) / (2 · (2↑𝑘))) = ((2 · 3) / (2↑(𝑘 + 1))))
207199, 206eqtr3d 2778 . . . . . . . . 9 (𝑘 ∈ ℕ0 → (3 / (2↑𝑘)) = ((2 · 3) / (2↑(𝑘 + 1))))
208207oveq1d 7372 . . . . . . . 8 (𝑘 ∈ ℕ0 → ((3 / (2↑𝑘)) − (3 / (2↑(𝑘 + 1)))) = (((2 · 3) / (2↑(𝑘 + 1))) − (3 / (2↑(𝑘 + 1)))))
209 divcan5 11857 . . . . . . . . . . . . 13 ((1 ∈ ℂ ∧ ((2↑𝑘) ∈ ℂ ∧ (2↑𝑘) ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · 1) / (2 · (2↑𝑘))) = (1 / (2↑𝑘)))
210162, 195, 209mp3an13 1452 . . . . . . . . . . . 12 (((2↑𝑘) ∈ ℂ ∧ (2↑𝑘) ≠ 0) → ((2 · 1) / (2 · (2↑𝑘))) = (1 / (2↑𝑘)))
211193, 194, 210syl2anc 584 . . . . . . . . . . 11 ((2↑𝑘) ∈ ℝ+ → ((2 · 1) / (2 · (2↑𝑘))) = (1 / (2↑𝑘)))
21251, 211syl 17 . . . . . . . . . 10 (𝑘 ∈ ℕ0 → ((2 · 1) / (2 · (2↑𝑘))) = (1 / (2↑𝑘)))
213 2t1e2 12316 . . . . . . . . . . . 12 (2 · 1) = 2
214213a1i 11 . . . . . . . . . . 11 (𝑘 ∈ ℕ0 → (2 · 1) = 2)
215214, 205oveq12d 7375 . . . . . . . . . 10 (𝑘 ∈ ℕ0 → ((2 · 1) / (2 · (2↑𝑘))) = (2 / (2↑(𝑘 + 1))))
216212, 215eqtr3d 2778 . . . . . . . . 9 (𝑘 ∈ ℕ0 → (1 / (2↑𝑘)) = (2 / (2↑(𝑘 + 1))))
217216oveq1d 7372 . . . . . . . 8 (𝑘 ∈ ℕ0 → ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) = ((2 / (2↑(𝑘 + 1))) + (1 / (2↑(𝑘 + 1)))))
218192, 208, 2173eqtr4d 2786 . . . . . . 7 (𝑘 ∈ ℕ0 → ((3 / (2↑𝑘)) − (3 / (2↑(𝑘 + 1)))) = ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))))
219218adantl 482 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → ((3 / (2↑𝑘)) − (3 / (2↑(𝑘 + 1)))) = ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))))
220141, 172, 2193brtr4d 5137 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → ((𝑆‘(𝑘 + 1))𝐷(𝑆𝑘)) ≤ ((3 / (2↑𝑘)) − (3 / (2↑(𝑘 + 1)))))
221 blss2 23757 . . . . 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 1385 . . . 4 ((𝜑𝑘 ∈ ℕ0) → ((𝑆‘(𝑘 + 1))(ball‘𝐷)(3 / (2↑(𝑘 + 1)))) ⊆ ((𝑆𝑘)(ball‘𝐷)(3 / (2↑𝑘))))
2231, 222sylan2 593 . . 3 ((𝜑𝑘 ∈ ℕ) → ((𝑆‘(𝑘 + 1))(ball‘𝐷)(3 / (2↑(𝑘 + 1)))) ⊆ ((𝑆𝑘)(ball‘𝐷)(3 / (2↑𝑘))))
224 peano2nn 12165 . . . . . . 7 (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
225 fveq2 6842 . . . . . . . . 9 (𝑛 = (𝑘 + 1) → (𝑆𝑛) = (𝑆‘(𝑘 + 1)))
226 oveq2 7365 . . . . . . . . . 10 (𝑛 = (𝑘 + 1) → (2↑𝑛) = (2↑(𝑘 + 1)))
227226oveq2d 7373 . . . . . . . . 9 (𝑛 = (𝑘 + 1) → (3 / (2↑𝑛)) = (3 / (2↑(𝑘 + 1))))
228225, 227opeq12d 4838 . . . . . . . 8 (𝑛 = (𝑘 + 1) → ⟨(𝑆𝑛), (3 / (2↑𝑛))⟩ = ⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩)
229 heibor.12 . . . . . . . 8 𝑀 = (𝑛 ∈ ℕ ↦ ⟨(𝑆𝑛), (3 / (2↑𝑛))⟩)
230 opex 5421 . . . . . . . 8 ⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩ ∈ V
231228, 229, 230fvmpt 6948 . . . . . . 7 ((𝑘 + 1) ∈ ℕ → (𝑀‘(𝑘 + 1)) = ⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩)
232224, 231syl 17 . . . . . 6 (𝑘 ∈ ℕ → (𝑀‘(𝑘 + 1)) = ⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩)
233232adantl 482 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (𝑀‘(𝑘 + 1)) = ⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩)
234233fveq2d 6846 . . . 4 ((𝜑𝑘 ∈ ℕ) → ((ball‘𝐷)‘(𝑀‘(𝑘 + 1))) = ((ball‘𝐷)‘⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩))
235 df-ov 7360 . . . 4 ((𝑆‘(𝑘 + 1))(ball‘𝐷)(3 / (2↑(𝑘 + 1)))) = ((ball‘𝐷)‘⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩)
236234, 235eqtr4di 2794 . . 3 ((𝜑𝑘 ∈ ℕ) → ((ball‘𝐷)‘(𝑀‘(𝑘 + 1))) = ((𝑆‘(𝑘 + 1))(ball‘𝐷)(3 / (2↑(𝑘 + 1)))))
237 fveq2 6842 . . . . . . . 8 (𝑛 = 𝑘 → (𝑆𝑛) = (𝑆𝑘))
238 oveq2 7365 . . . . . . . . 9 (𝑛 = 𝑘 → (2↑𝑛) = (2↑𝑘))
239238oveq2d 7373 . . . . . . . 8 (𝑛 = 𝑘 → (3 / (2↑𝑛)) = (3 / (2↑𝑘)))
240237, 239opeq12d 4838 . . . . . . 7 (𝑛 = 𝑘 → ⟨(𝑆𝑛), (3 / (2↑𝑛))⟩ = ⟨(𝑆𝑘), (3 / (2↑𝑘))⟩)
241 opex 5421 . . . . . . 7 ⟨(𝑆𝑘), (3 / (2↑𝑘))⟩ ∈ V
242240, 229, 241fvmpt 6948 . . . . . 6 (𝑘 ∈ ℕ → (𝑀𝑘) = ⟨(𝑆𝑘), (3 / (2↑𝑘))⟩)
243242fveq2d 6846 . . . . 5 (𝑘 ∈ ℕ → ((ball‘𝐷)‘(𝑀𝑘)) = ((ball‘𝐷)‘⟨(𝑆𝑘), (3 / (2↑𝑘))⟩))
244 df-ov 7360 . . . . 5 ((𝑆𝑘)(ball‘𝐷)(3 / (2↑𝑘))) = ((ball‘𝐷)‘⟨(𝑆𝑘), (3 / (2↑𝑘))⟩)
245243, 244eqtr4di 2794 . . . 4 (𝑘 ∈ ℕ → ((ball‘𝐷)‘(𝑀𝑘)) = ((𝑆𝑘)(ball‘𝐷)(3 / (2↑𝑘))))
246245adantl 482 . . 3 ((𝜑𝑘 ∈ ℕ) → ((ball‘𝐷)‘(𝑀𝑘)) = ((𝑆𝑘)(ball‘𝐷)(3 / (2↑𝑘))))
247223, 236, 2463sstr4d 3991 . 2 ((𝜑𝑘 ∈ ℕ) → ((ball‘𝐷)‘(𝑀‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝑀𝑘)))
248247ralrimiva 3143 1 (𝜑 → ∀𝑘 ∈ ℕ ((ball‘𝐷)‘(𝑀‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝑀𝑘)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  w3a 1087   = wceq 1541  wcel 2106  {cab 2713  wne 2943  wral 3064  wrex 3073  Vcvv 3445  cin 3909  wss 3910  c0 4282  ifcif 4486  𝒫 cpw 4560  cop 4592   cuni 4865   ciun 4954   class class class wbr 5105  {copab 5167  cmpt 5188  wf 6492  cfv 6496  (class class class)co 7357  cmpo 7359  2nd c2nd 7920  Fincfn 8883  cc 11049  cr 11050  0cc0 11051  1c1 11052   + caddc 11054   · cmul 11056  *cxr 11188  cle 11190  cmin 11385   / cdiv 11812  cn 12153  2c2 12208  3c3 12209  0cn0 12413  cuz 12763  +crp 12915   +𝑒 cxad 13031  seqcseq 13906  cexp 13967  ∞Metcxmet 20781  Metcmet 20782  ballcbl 20783  MetOpencmopn 20786  CMetccmet 24618
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-er 8648  df-map 8767  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-n0 12414  df-z 12500  df-uz 12764  df-rp 12916  df-xneg 13033  df-xadd 13034  df-xmul 13035  df-seq 13907  df-exp 13968  df-psmet 20788  df-xmet 20789  df-met 20790  df-bl 20791  df-cmet 24621
This theorem is referenced by:  heiborlem8  36277  heiborlem9  36278
  Copyright terms: Public domain W3C validator