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 36207
Description: Lemma for heibor 36212. 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 12378 . . . 4 (𝑘 ∈ ℕ → 𝑘 ∈ ℕ0)
2 heibor.6 . . . . . . . 8 (𝜑𝐷 ∈ (CMet‘𝑋))
3 cmetmet 24596 . . . . . . . 8 (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋))
42, 3syl 17 . . . . . . 7 (𝜑𝐷 ∈ (Met‘𝑋))
5 metxmet 23633 . . . . . . 7 (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋))
64, 5syl 17 . . . . . 6 (𝜑𝐷 ∈ (∞Met‘𝑋))
76adantr 481 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → 𝐷 ∈ (∞Met‘𝑋))
8 heibor.7 . . . . . . . . 9 (𝜑𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin))
9 inss1 4186 . . . . . . . . 9 (𝒫 𝑋 ∩ Fin) ⊆ 𝒫 𝑋
10 fss 6682 . . . . . . . . 9 ((𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin) ∧ (𝒫 𝑋 ∩ Fin) ⊆ 𝒫 𝑋) → 𝐹:ℕ0⟶𝒫 𝑋)
118, 9, 10sylancl 586 . . . . . . . 8 (𝜑𝐹:ℕ0⟶𝒫 𝑋)
12 peano2nn0 12411 . . . . . . . 8 (𝑘 ∈ ℕ0 → (𝑘 + 1) ∈ ℕ0)
13 ffvelcdm 7029 . . . . . . . 8 ((𝐹:ℕ0⟶𝒫 𝑋 ∧ (𝑘 + 1) ∈ ℕ0) → (𝐹‘(𝑘 + 1)) ∈ 𝒫 𝑋)
1411, 12, 13syl2an 596 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (𝐹‘(𝑘 + 1)) ∈ 𝒫 𝑋)
1514elpwid 4567 . . . . . 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 36205 . . . . . . . 8 ((𝜑 ∧ (𝑘 + 1) ∈ ℕ0) → (𝑆‘(𝑘 + 1))𝐺(𝑘 + 1))
2512, 24sylan2 593 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (𝑆‘(𝑘 + 1))𝐺(𝑘 + 1))
26 fvex 6852 . . . . . . . . 9 (𝑆‘(𝑘 + 1)) ∈ V
27 ovex 7384 . . . . . . . . 9 (𝑘 + 1) ∈ V
2816, 17, 18, 26, 27heiborlem2 36203 . . . . . . . 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 3943 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → (𝑆‘(𝑘 + 1)) ∈ 𝑋)
3211ffvelcdmda 7031 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (𝐹𝑘) ∈ 𝒫 𝑋)
3332elpwid 4567 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (𝐹𝑘) ⊆ 𝑋)
3416, 17, 18, 19, 2, 8, 20, 21, 22, 23heiborlem4 36205 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (𝑆𝑘)𝐺𝑘)
35 fvex 6852 . . . . . . . . 9 (𝑆𝑘) ∈ V
36 vex 3447 . . . . . . . . 9 𝑘 ∈ V
3716, 17, 18, 35, 36heiborlem2 36203 . . . . . . . 8 ((𝑆𝑘)𝐺𝑘 ↔ (𝑘 ∈ ℕ0 ∧ (𝑆𝑘) ∈ (𝐹𝑘) ∧ ((𝑆𝑘)𝐵𝑘) ∈ 𝐾))
3837simp2bi 1146 . . . . . . 7 ((𝑆𝑘)𝐺𝑘 → (𝑆𝑘) ∈ (𝐹𝑘))
3934, 38syl 17 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (𝑆𝑘) ∈ (𝐹𝑘))
4033, 39sseldd 3943 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → (𝑆𝑘) ∈ 𝑋)
41 3re 12191 . . . . . 6 3 ∈ ℝ
42 2nn 12184 . . . . . . . . 9 2 ∈ ℕ
43 nnexpcl 13934 . . . . . . . . 9 ((2 ∈ ℕ ∧ (𝑘 + 1) ∈ ℕ0) → (2↑(𝑘 + 1)) ∈ ℕ)
4442, 12, 43sylancr 587 . . . . . . . 8 (𝑘 ∈ ℕ0 → (2↑(𝑘 + 1)) ∈ ℕ)
4544nnrpd 12909 . . . . . . 7 (𝑘 ∈ ℕ0 → (2↑(𝑘 + 1)) ∈ ℝ+)
4645adantl 482 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (2↑(𝑘 + 1)) ∈ ℝ+)
47 rerpdivcl 12899 . . . . . 6 ((3 ∈ ℝ ∧ (2↑(𝑘 + 1)) ∈ ℝ+) → (3 / (2↑(𝑘 + 1))) ∈ ℝ)
4841, 46, 47sylancr 587 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → (3 / (2↑(𝑘 + 1))) ∈ ℝ)
49 nnexpcl 13934 . . . . . . . . 9 ((2 ∈ ℕ ∧ 𝑘 ∈ ℕ0) → (2↑𝑘) ∈ ℕ)
5042, 49mpan 688 . . . . . . . 8 (𝑘 ∈ ℕ0 → (2↑𝑘) ∈ ℕ)
5150nnrpd 12909 . . . . . . 7 (𝑘 ∈ ℕ0 → (2↑𝑘) ∈ ℝ+)
5251adantl 482 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (2↑𝑘) ∈ ℝ+)
53 rerpdivcl 12899 . . . . . 6 ((3 ∈ ℝ ∧ (2↑𝑘) ∈ ℝ+) → (3 / (2↑𝑘)) ∈ ℝ)
5441, 52, 53sylancr 587 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → (3 / (2↑𝑘)) ∈ ℝ)
55 oveq1 7358 . . . . . . . . . . . 12 (𝑧 = (𝑆𝑘) → (𝑧(ball‘𝐷)(1 / (2↑𝑚))) = ((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑚))))
56 oveq2 7359 . . . . . . . . . . . . . 14 (𝑚 = 𝑘 → (2↑𝑚) = (2↑𝑘))
5756oveq2d 7367 . . . . . . . . . . . . 13 (𝑚 = 𝑘 → (1 / (2↑𝑚)) = (1 / (2↑𝑘)))
5857oveq2d 7367 . . . . . . . . . . . 12 (𝑚 = 𝑘 → ((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑚))) = ((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑘))))
59 ovex 7384 . . . . . . . . . . . 12 ((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∈ V
6055, 58, 19, 59ovmpo 7509 . . . . . . . . . . 11 (((𝑆𝑘) ∈ 𝑋𝑘 ∈ ℕ0) → ((𝑆𝑘)𝐵𝑘) = ((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑘))))
6140, 60sylancom 588 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → ((𝑆𝑘)𝐵𝑘) = ((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑘))))
62 df-br 5104 . . . . . . . . . . . . . . . . 17 ((𝑆𝑘)𝐺𝑘 ↔ ⟨(𝑆𝑘), 𝑘⟩ ∈ 𝐺)
63 fveq2 6839 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = ⟨(𝑆𝑘), 𝑘⟩ → (𝑇𝑥) = (𝑇‘⟨(𝑆𝑘), 𝑘⟩))
64 df-ov 7354 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑆𝑘)𝑇𝑘) = (𝑇‘⟨(𝑆𝑘), 𝑘⟩)
6563, 64eqtr4di 2794 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = ⟨(𝑆𝑘), 𝑘⟩ → (𝑇𝑥) = ((𝑆𝑘)𝑇𝑘))
6635, 36op2ndd 7924 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = ⟨(𝑆𝑘), 𝑘⟩ → (2nd𝑥) = 𝑘)
6766oveq1d 7366 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = ⟨(𝑆𝑘), 𝑘⟩ → ((2nd𝑥) + 1) = (𝑘 + 1))
6865, 67breq12d 5116 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = ⟨(𝑆𝑘), 𝑘⟩ → ((𝑇𝑥)𝐺((2nd𝑥) + 1) ↔ ((𝑆𝑘)𝑇𝑘)𝐺(𝑘 + 1)))
69 fveq2 6839 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = ⟨(𝑆𝑘), 𝑘⟩ → (𝐵𝑥) = (𝐵‘⟨(𝑆𝑘), 𝑘⟩))
70 df-ov 7354 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑆𝑘)𝐵𝑘) = (𝐵‘⟨(𝑆𝑘), 𝑘⟩)
7169, 70eqtr4di 2794 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = ⟨(𝑆𝑘), 𝑘⟩ → (𝐵𝑥) = ((𝑆𝑘)𝐵𝑘))
7265, 67oveq12d 7369 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = ⟨(𝑆𝑘), 𝑘⟩ → ((𝑇𝑥)𝐵((2nd𝑥) + 1)) = (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1)))
7371, 72ineq12d 4171 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = ⟨(𝑆𝑘), 𝑘⟩ → ((𝐵𝑥) ∩ ((𝑇𝑥)𝐵((2nd𝑥) + 1))) = (((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))))
7473eleq1d 2822 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = ⟨(𝑆𝑘), 𝑘⟩ → (((𝐵𝑥) ∩ ((𝑇𝑥)𝐵((2nd𝑥) + 1))) ∈ 𝐾 ↔ (((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾))
7568, 74anbi12d 631 . . . . . . . . . . . . . . . . . . 19 (𝑥 = ⟨(𝑆𝑘), 𝑘⟩ → (((𝑇𝑥)𝐺((2nd𝑥) + 1) ∧ ((𝐵𝑥) ∩ ((𝑇𝑥)𝐵((2nd𝑥) + 1))) ∈ 𝐾) ↔ (((𝑆𝑘)𝑇𝑘)𝐺(𝑘 + 1) ∧ (((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾)))
7675rspccv 3576 . . . . . . . . . . . . . . . . . 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 7384 . . . . . . . . . . . . . . 15 ((𝑆𝑘)𝑇𝑘) ∈ V
8316, 17, 18, 82, 27heiborlem2 36203 . . . . . . . . . . . . . 14 (((𝑆𝑘)𝑇𝑘)𝐺(𝑘 + 1) ↔ ((𝑘 + 1) ∈ ℕ0 ∧ ((𝑆𝑘)𝑇𝑘) ∈ (𝐹‘(𝑘 + 1)) ∧ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1)) ∈ 𝐾))
8483simp2bi 1146 . . . . . . . . . . . . 13 (((𝑆𝑘)𝑇𝑘)𝐺(𝑘 + 1) → ((𝑆𝑘)𝑇𝑘) ∈ (𝐹‘(𝑘 + 1)))
8581, 84syl 17 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → ((𝑆𝑘)𝑇𝑘) ∈ (𝐹‘(𝑘 + 1)))
8615, 85sseldd 3943 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → ((𝑆𝑘)𝑇𝑘) ∈ 𝑋)
8712adantl 482 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → (𝑘 + 1) ∈ ℕ0)
88 oveq1 7358 . . . . . . . . . . . 12 (𝑧 = ((𝑆𝑘)𝑇𝑘) → (𝑧(ball‘𝐷)(1 / (2↑𝑚))) = (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑𝑚))))
89 oveq2 7359 . . . . . . . . . . . . . 14 (𝑚 = (𝑘 + 1) → (2↑𝑚) = (2↑(𝑘 + 1)))
9089oveq2d 7367 . . . . . . . . . . . . 13 (𝑚 = (𝑘 + 1) → (1 / (2↑𝑚)) = (1 / (2↑(𝑘 + 1))))
9190oveq2d 7367 . . . . . . . . . . . 12 (𝑚 = (𝑘 + 1) → (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑𝑚))) = (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1)))))
92 ovex 7384 . . . . . . . . . . . 12 (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1)))) ∈ V
9388, 91, 19, 92ovmpo 7509 . . . . . . . . . . 11 ((((𝑆𝑘)𝑇𝑘) ∈ 𝑋 ∧ (𝑘 + 1) ∈ ℕ0) → (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1)) = (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1)))))
9486, 87, 93syl2anc 584 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1)) = (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1)))))
9561, 94ineq12d 4171 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → (((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))) = (((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))))
9680simprd 496 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → (((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾)
97 0elpw 5309 . . . . . . . . . . . . 13 ∅ ∈ 𝒫 𝑈
98 0fin 9073 . . . . . . . . . . . . 13 ∅ ∈ Fin
99 elin 3924 . . . . . . . . . . . . 13 (∅ ∈ (𝒫 𝑈 ∩ Fin) ↔ (∅ ∈ 𝒫 𝑈 ∧ ∅ ∈ Fin))
10097, 98, 99mpbir2an 709 . . . . . . . . . . . 12 ∅ ∈ (𝒫 𝑈 ∩ Fin)
101 0ss 4354 . . . . . . . . . . . 12 ∅ ⊆
102 unieq 4874 . . . . . . . . . . . . . 14 (𝑣 = ∅ → 𝑣 = ∅)
103102sseq2d 3974 . . . . . . . . . . . . 13 (𝑣 = ∅ → (∅ ⊆ 𝑣 ↔ ∅ ⊆ ∅))
104103rspcev 3579 . . . . . . . . . . . 12 ((∅ ∈ (𝒫 𝑈 ∩ Fin) ∧ ∅ ⊆ ∅) → ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ 𝑣)
105100, 101, 104mp2an 690 . . . . . . . . . . 11 𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ 𝑣
106 0ex 5262 . . . . . . . . . . . . 13 ∅ ∈ V
107 sseq1 3967 . . . . . . . . . . . . . . 15 (𝑢 = ∅ → (𝑢 𝑣 ↔ ∅ ⊆ 𝑣))
108107rexbidv 3173 . . . . . . . . . . . . . 14 (𝑢 = ∅ → (∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 𝑣 ↔ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ 𝑣))
109108notbid 317 . . . . . . . . . . . . 13 (𝑢 = ∅ → (¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 𝑣 ↔ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ 𝑣))
110106, 109, 17elab2 3632 . . . . . . . . . . . 12 (∅ ∈ 𝐾 ↔ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ 𝑣)
111110con2bii 357 . . . . . . . . . . 11 (∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ 𝑣 ↔ ¬ ∅ ∈ 𝐾)
112105, 111mpbi 229 . . . . . . . . . 10 ¬ ∅ ∈ 𝐾
113 nelne2 3040 . . . . . . . . . 10 (((((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾 ∧ ¬ ∅ ∈ 𝐾) → (((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ≠ ∅)
11496, 112, 113sylancl 586 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → (((𝑆𝑘)𝐵𝑘) ∩ (((𝑆𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ≠ ∅)
11595, 114eqnetrrd 3010 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → (((𝑆𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))) ≠ ∅)
11651rpreccld 12921 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ0 → (1 / (2↑𝑘)) ∈ ℝ+)
117116adantl 482 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ0) → (1 / (2↑𝑘)) ∈ ℝ+)
118117rpred 12911 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → (1 / (2↑𝑘)) ∈ ℝ)
11945rpreccld 12921 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ0 → (1 / (2↑(𝑘 + 1))) ∈ ℝ+)
120119adantl 482 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ0) → (1 / (2↑(𝑘 + 1))) ∈ ℝ+)
121120rpred 12911 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → (1 / (2↑(𝑘 + 1))) ∈ ℝ)
122 rexadd 13105 . . . . . . . . . . . 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 5113 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → (((1 / (2↑𝑘)) +𝑒 (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)) ↔ ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘))))
125117rpxrd 12912 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → (1 / (2↑𝑘)) ∈ ℝ*)
126120rpxrd 12912 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → (1 / (2↑(𝑘 + 1))) ∈ ℝ*)
127 bldisj 23697 . . . . . . . . . . . . 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 2954 . . . . . . . 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 12926 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ∈ ℝ+)
135134rpred 12911 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ∈ ℝ)
1364adantr 481 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → 𝐷 ∈ (Met‘𝑋))
137 metcl 23631 . . . . . . . . . 10 ((𝐷 ∈ (Met‘𝑋) ∧ (𝑆𝑘) ∈ 𝑋 ∧ ((𝑆𝑘)𝑇𝑘) ∈ 𝑋) → ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)) ∈ ℝ)
138136, 40, 86, 137syl3anc 1371 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)) ∈ ℝ)
139135, 138letrid 11265 . . . . . . . 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 13875 . . . . . . . . . . . 12 (𝑘 ∈ (ℤ‘0) → (seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘(𝑘 + 1)) = ((seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1))))
143 nn0uz 12759 . . . . . . . . . . . 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 6840 . . . . . . . . . . 11 (𝑆‘(𝑘 + 1)) = (seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘(𝑘 + 1))
14623fveq1i 6840 . . . . . . . . . . . 12 (𝑆𝑘) = (seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘𝑘)
147146oveq1i 7361 . . . . . . . . . . 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 7358 . . . . . . . . . . . . . 14 (𝑚 = (𝑘 + 1) → (𝑚 − 1) = ((𝑘 + 1) − 1))
152150, 151ifbieq2d 4510 . . . . . . . . . . . . 13 (𝑚 = (𝑘 + 1) → if(𝑚 = 0, 𝐶, (𝑚 − 1)) = if((𝑘 + 1) = 0, 𝐶, ((𝑘 + 1) − 1)))
153 nn0p1nn 12410 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℕ0 → (𝑘 + 1) ∈ ℕ)
154 nnne0 12145 . . . . . . . . . . . . . . . . 17 ((𝑘 + 1) ∈ ℕ → (𝑘 + 1) ≠ 0)
155154neneqd 2946 . . . . . . . . . . . . . . . 16 ((𝑘 + 1) ∈ ℕ → ¬ (𝑘 + 1) = 0)
156153, 155syl 17 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℕ0 → ¬ (𝑘 + 1) = 0)
157156iffalsed 4495 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ0 → if((𝑘 + 1) = 0, 𝐶, ((𝑘 + 1) − 1)) = ((𝑘 + 1) − 1))
158 ovex 7384 . . . . . . . . . . . . . 14 ((𝑘 + 1) − 1) ∈ V
159157, 158eqeltrdi 2846 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ0 → if((𝑘 + 1) = 0, 𝐶, ((𝑘 + 1) − 1)) ∈ V)
160149, 152, 12, 159fvmptd3 6968 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 → ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1)) = if((𝑘 + 1) = 0, 𝐶, ((𝑘 + 1) − 1)))
161 nn0cn 12381 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ0𝑘 ∈ ℂ)
162 ax-1cn 11067 . . . . . . . . . . . . 13 1 ∈ ℂ
163 pncan 11365 . . . . . . . . . . . . 13 ((𝑘 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑘 + 1) − 1) = 𝑘)
164161, 162, 163sylancl 586 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 → ((𝑘 + 1) − 1) = 𝑘)
165160, 157, 1643eqtrd 2780 . . . . . . . . . . 11 (𝑘 ∈ ℕ0 → ((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1)) = 𝑘)
166165oveq2d 7367 . . . . . . . . . 10 (𝑘 ∈ ℕ0 → ((𝑆𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1))) = ((𝑆𝑘)𝑇𝑘))
167148, 166eqtrd 2776 . . . . . . . . 9 (𝑘 ∈ ℕ0 → (𝑆‘(𝑘 + 1)) = ((𝑆𝑘)𝑇𝑘))
168167adantl 482 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → (𝑆‘(𝑘 + 1)) = ((𝑆𝑘)𝑇𝑘))
169168oveq1d 7366 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → ((𝑆‘(𝑘 + 1))𝐷(𝑆𝑘)) = (((𝑆𝑘)𝑇𝑘)𝐷(𝑆𝑘)))
170 metsym 23649 . . . . . . . 8 ((𝐷 ∈ (Met‘𝑋) ∧ ((𝑆𝑘)𝑇𝑘) ∈ 𝑋 ∧ (𝑆𝑘) ∈ 𝑋) → (((𝑆𝑘)𝑇𝑘)𝐷(𝑆𝑘)) = ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)))
171136, 86, 40, 170syl3anc 1371 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (((𝑆𝑘)𝑇𝑘)𝐷(𝑆𝑘)) = ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)))
172169, 171eqtrd 2776 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → ((𝑆‘(𝑘 + 1))𝐷(𝑆𝑘)) = ((𝑆𝑘)𝐷((𝑆𝑘)𝑇𝑘)))
173 3cn 12192 . . . . . . . . . . . . 13 3 ∈ ℂ
1741732timesi 12249 . . . . . . . . . . . 12 (2 · 3) = (3 + 3)
175174oveq1i 7361 . . . . . . . . . . 11 ((2 · 3) − 3) = ((3 + 3) − 3)
176173, 173pncan3oi 11375 . . . . . . . . . . 11 ((3 + 3) − 3) = 3
177 df-3 12175 . . . . . . . . . . 11 3 = (2 + 1)
178175, 176, 1773eqtri 2768 . . . . . . . . . 10 ((2 · 3) − 3) = (2 + 1)
179178oveq1i 7361 . . . . . . . . 9 (((2 · 3) − 3) / (2↑(𝑘 + 1))) = ((2 + 1) / (2↑(𝑘 + 1)))
180 rpcn 12879 . . . . . . . . . . 11 ((2↑(𝑘 + 1)) ∈ ℝ+ → (2↑(𝑘 + 1)) ∈ ℂ)
181 rpne0 12885 . . . . . . . . . . 11 ((2↑(𝑘 + 1)) ∈ ℝ+ → (2↑(𝑘 + 1)) ≠ 0)
182 2cn 12186 . . . . . . . . . . . . 13 2 ∈ ℂ
183182, 173mulcli 11120 . . . . . . . . . . . 12 (2 · 3) ∈ ℂ
184 divsubdir 11807 . . . . . . . . . . . 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 11796 . . . . . . . . . . . 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 12879 . . . . . . . . . . . 12 ((2↑𝑘) ∈ ℝ+ → (2↑𝑘) ∈ ℂ)
194 rpne0 12885 . . . . . . . . . . . 12 ((2↑𝑘) ∈ ℝ+ → (2↑𝑘) ≠ 0)
195 2cnne0 12321 . . . . . . . . . . . . 13 (2 ∈ ℂ ∧ 2 ≠ 0)
196 divcan5 11815 . . . . . . . . . . . . 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 11095 . . . . . . . . . . . . 13 ((2 ∈ ℂ ∧ (2↑𝑘) ∈ ℂ) → (2 · (2↑𝑘)) = ((2↑𝑘) · 2))
202182, 200, 201sylancr 587 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 → (2 · (2↑𝑘)) = ((2↑𝑘) · 2))
203 expp1 13928 . . . . . . . . . . . . 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 7367 . . . . . . . . . 10 (𝑘 ∈ ℕ0 → ((2 · 3) / (2 · (2↑𝑘))) = ((2 · 3) / (2↑(𝑘 + 1))))
207199, 206eqtr3d 2778 . . . . . . . . 9 (𝑘 ∈ ℕ0 → (3 / (2↑𝑘)) = ((2 · 3) / (2↑(𝑘 + 1))))
208207oveq1d 7366 . . . . . . . 8 (𝑘 ∈ ℕ0 → ((3 / (2↑𝑘)) − (3 / (2↑(𝑘 + 1)))) = (((2 · 3) / (2↑(𝑘 + 1))) − (3 / (2↑(𝑘 + 1)))))
209 divcan5 11815 . . . . . . . . . . . . 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 12274 . . . . . . . . . . . 12 (2 · 1) = 2
214213a1i 11 . . . . . . . . . . 11 (𝑘 ∈ ℕ0 → (2 · 1) = 2)
215214, 205oveq12d 7369 . . . . . . . . . 10 (𝑘 ∈ ℕ0 → ((2 · 1) / (2 · (2↑𝑘))) = (2 / (2↑(𝑘 + 1))))
216212, 215eqtr3d 2778 . . . . . . . . 9 (𝑘 ∈ ℕ0 → (1 / (2↑𝑘)) = (2 / (2↑(𝑘 + 1))))
217216oveq1d 7366 . . . . . . . 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 5135 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → ((𝑆‘(𝑘 + 1))𝐷(𝑆𝑘)) ≤ ((3 / (2↑𝑘)) − (3 / (2↑(𝑘 + 1)))))
221 blss2 23703 . . . . 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 12123 . . . . . . 7 (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
225 fveq2 6839 . . . . . . . . 9 (𝑛 = (𝑘 + 1) → (𝑆𝑛) = (𝑆‘(𝑘 + 1)))
226 oveq2 7359 . . . . . . . . . 10 (𝑛 = (𝑘 + 1) → (2↑𝑛) = (2↑(𝑘 + 1)))
227226oveq2d 7367 . . . . . . . . 9 (𝑛 = (𝑘 + 1) → (3 / (2↑𝑛)) = (3 / (2↑(𝑘 + 1))))
228225, 227opeq12d 4836 . . . . . . . 8 (𝑛 = (𝑘 + 1) → ⟨(𝑆𝑛), (3 / (2↑𝑛))⟩ = ⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩)
229 heibor.12 . . . . . . . 8 𝑀 = (𝑛 ∈ ℕ ↦ ⟨(𝑆𝑛), (3 / (2↑𝑛))⟩)
230 opex 5419 . . . . . . . 8 ⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩ ∈ V
231228, 229, 230fvmpt 6945 . . . . . . 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 6843 . . . 4 ((𝜑𝑘 ∈ ℕ) → ((ball‘𝐷)‘(𝑀‘(𝑘 + 1))) = ((ball‘𝐷)‘⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩))
235 df-ov 7354 . . . 4 ((𝑆‘(𝑘 + 1))(ball‘𝐷)(3 / (2↑(𝑘 + 1)))) = ((ball‘𝐷)‘⟨(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))⟩)
236234, 235eqtr4di 2794 . . 3 ((𝜑𝑘 ∈ ℕ) → ((ball‘𝐷)‘(𝑀‘(𝑘 + 1))) = ((𝑆‘(𝑘 + 1))(ball‘𝐷)(3 / (2↑(𝑘 + 1)))))
237 fveq2 6839 . . . . . . . 8 (𝑛 = 𝑘 → (𝑆𝑛) = (𝑆𝑘))
238 oveq2 7359 . . . . . . . . 9 (𝑛 = 𝑘 → (2↑𝑛) = (2↑𝑘))
239238oveq2d 7367 . . . . . . . 8 (𝑛 = 𝑘 → (3 / (2↑𝑛)) = (3 / (2↑𝑘)))
240237, 239opeq12d 4836 . . . . . . 7 (𝑛 = 𝑘 → ⟨(𝑆𝑛), (3 / (2↑𝑛))⟩ = ⟨(𝑆𝑘), (3 / (2↑𝑘))⟩)
241 opex 5419 . . . . . . 7 ⟨(𝑆𝑘), (3 / (2↑𝑘))⟩ ∈ V
242240, 229, 241fvmpt 6945 . . . . . 6 (𝑘 ∈ ℕ → (𝑀𝑘) = ⟨(𝑆𝑘), (3 / (2↑𝑘))⟩)
243242fveq2d 6843 . . . . 5 (𝑘 ∈ ℕ → ((ball‘𝐷)‘(𝑀𝑘)) = ((ball‘𝐷)‘⟨(𝑆𝑘), (3 / (2↑𝑘))⟩))
244 df-ov 7354 . . . . 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 3989 . 2 ((𝜑𝑘 ∈ ℕ) → ((ball‘𝐷)‘(𝑀‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝑀𝑘)))
248247ralrimiva 3141 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 2941  wral 3062  wrex 3071  Vcvv 3443  cin 3907  wss 3908  c0 4280  ifcif 4484  𝒫 cpw 4558  cop 4590   cuni 4863   ciun 4952   class class class wbr 5103  {copab 5165  cmpt 5186  wf 6489  cfv 6493  (class class class)co 7351  cmpo 7353  2nd c2nd 7912  Fincfn 8841  cc 11007  cr 11008  0cc0 11009  1c1 11010   + caddc 11012   · cmul 11014  *cxr 11146  cle 11148  cmin 11343   / cdiv 11770  cn 12111  2c2 12166  3c3 12167  0cn0 12371  cuz 12721  +crp 12869   +𝑒 cxad 12985  seqcseq 13860  cexp 13921  ∞Metcxmet 20728  Metcmet 20729  ballcbl 20730  MetOpencmopn 20733  CMetccmet 24564
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 5254  ax-nul 5261  ax-pow 5318  ax-pr 5382  ax-un 7664  ax-cnex 11065  ax-resscn 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-mulcom 11073  ax-addass 11074  ax-mulass 11075  ax-distr 11076  ax-i2m1 11077  ax-1ne0 11078  ax-1rid 11079  ax-rnegex 11080  ax-rrecex 11081  ax-cnre 11082  ax-pre-lttri 11083  ax-pre-lttrn 11084  ax-pre-ltadd 11085  ax-pre-mulgt0 11086
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 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3351  df-reu 3352  df-rab 3406  df-v 3445  df-sbc 3738  df-csb 3854  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-nul 4281  df-if 4485  df-pw 4560  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4864  df-iun 4954  df-br 5104  df-opab 5166  df-mpt 5187  df-tr 5221  df-id 5529  df-eprel 5535  df-po 5543  df-so 5544  df-fr 5586  df-we 5588  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6251  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-iota 6445  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-riota 7307  df-ov 7354  df-oprab 7355  df-mpo 7356  df-om 7795  df-1st 7913  df-2nd 7914  df-frecs 8204  df-wrecs 8235  df-recs 8309  df-rdg 8348  df-er 8606  df-map 8725  df-en 8842  df-dom 8843  df-sdom 8844  df-fin 8845  df-pnf 11149  df-mnf 11150  df-xr 11151  df-ltxr 11152  df-le 11153  df-sub 11345  df-neg 11346  df-div 11771  df-nn 12112  df-2 12174  df-3 12175  df-n0 12372  df-z 12458  df-uz 12722  df-rp 12870  df-xneg 12987  df-xadd 12988  df-xmul 12989  df-seq 13861  df-exp 13922  df-psmet 20735  df-xmet 20736  df-met 20737  df-bl 20738  df-cmet 24567
This theorem is referenced by:  heiborlem8  36209  heiborlem9  36210
  Copyright terms: Public domain W3C validator