Proof of Theorem heiborlem6
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | nnnn0 12533 | . . . 4
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℕ0) | 
| 2 |  | heibor.6 | . . . . . . . 8
⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋)) | 
| 3 |  | cmetmet 25320 | . . . . . . . 8
⊢ (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋)) | 
| 4 | 2, 3 | syl 17 | . . . . . . 7
⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) | 
| 5 |  | metxmet 24344 | . . . . . . 7
⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋)) | 
| 6 | 4, 5 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) | 
| 7 | 6 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐷 ∈ (∞Met‘𝑋)) | 
| 8 |  | heibor.7 | . . . . . . . . 9
⊢ (𝜑 → 𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin)) | 
| 9 |  | inss1 4237 | . . . . . . . . 9
⊢
(𝒫 𝑋 ∩
Fin) ⊆ 𝒫 𝑋 | 
| 10 |  | fss 6752 | . . . . . . . . 9
⊢ ((𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin) ∧ (𝒫
𝑋 ∩ Fin) ⊆
𝒫 𝑋) → 𝐹:ℕ0⟶𝒫 𝑋) | 
| 11 | 8, 9, 10 | sylancl 586 | . . . . . . . 8
⊢ (𝜑 → 𝐹:ℕ0⟶𝒫 𝑋) | 
| 12 |  | peano2nn0 12566 | . . . . . . . 8
⊢ (𝑘 ∈ ℕ0
→ (𝑘 + 1) ∈
ℕ0) | 
| 13 |  | ffvelcdm 7101 | . . . . . . . 8
⊢ ((𝐹:ℕ0⟶𝒫 𝑋 ∧ (𝑘 + 1) ∈ ℕ0) →
(𝐹‘(𝑘 + 1)) ∈ 𝒫 𝑋) | 
| 14 | 11, 12, 13 | syl2an 596 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐹‘(𝑘 + 1)) ∈ 𝒫 𝑋) | 
| 15 | 14 | elpwid 4609 | . . . . . 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)))) | 
| 24 | 16, 17, 18, 19, 2, 8, 20, 21, 22, 23 | heiborlem4 37821 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 + 1) ∈ ℕ0) →
(𝑆‘(𝑘 + 1))𝐺(𝑘 + 1)) | 
| 25 | 12, 24 | sylan2 593 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑆‘(𝑘 + 1))𝐺(𝑘 + 1)) | 
| 26 |  | fvex 6919 | . . . . . . . . 9
⊢ (𝑆‘(𝑘 + 1)) ∈ V | 
| 27 |  | ovex 7464 | . . . . . . . . 9
⊢ (𝑘 + 1) ∈ V | 
| 28 | 16, 17, 18, 26, 27 | heiborlem2 37819 | . . . . . . . 8
⊢ ((𝑆‘(𝑘 + 1))𝐺(𝑘 + 1) ↔ ((𝑘 + 1) ∈ ℕ0 ∧ (𝑆‘(𝑘 + 1)) ∈ (𝐹‘(𝑘 + 1)) ∧ ((𝑆‘(𝑘 + 1))𝐵(𝑘 + 1)) ∈ 𝐾)) | 
| 29 | 28 | simp2bi 1147 | . . . . . . 7
⊢ ((𝑆‘(𝑘 + 1))𝐺(𝑘 + 1) → (𝑆‘(𝑘 + 1)) ∈ (𝐹‘(𝑘 + 1))) | 
| 30 | 25, 29 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑆‘(𝑘 + 1)) ∈ (𝐹‘(𝑘 + 1))) | 
| 31 | 15, 30 | sseldd 3984 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑆‘(𝑘 + 1)) ∈ 𝑋) | 
| 32 | 11 | ffvelcdmda 7104 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐹‘𝑘) ∈ 𝒫 𝑋) | 
| 33 | 32 | elpwid 4609 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐹‘𝑘) ⊆ 𝑋) | 
| 34 | 16, 17, 18, 19, 2, 8, 20, 21, 22, 23 | heiborlem4 37821 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑆‘𝑘)𝐺𝑘) | 
| 35 |  | fvex 6919 | . . . . . . . . 9
⊢ (𝑆‘𝑘) ∈ V | 
| 36 |  | vex 3484 | . . . . . . . . 9
⊢ 𝑘 ∈ V | 
| 37 | 16, 17, 18, 35, 36 | heiborlem2 37819 | . . . . . . . 8
⊢ ((𝑆‘𝑘)𝐺𝑘 ↔ (𝑘 ∈ ℕ0 ∧ (𝑆‘𝑘) ∈ (𝐹‘𝑘) ∧ ((𝑆‘𝑘)𝐵𝑘) ∈ 𝐾)) | 
| 38 | 37 | simp2bi 1147 | . . . . . . 7
⊢ ((𝑆‘𝑘)𝐺𝑘 → (𝑆‘𝑘) ∈ (𝐹‘𝑘)) | 
| 39 | 34, 38 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑆‘𝑘) ∈ (𝐹‘𝑘)) | 
| 40 | 33, 39 | sseldd 3984 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑆‘𝑘) ∈ 𝑋) | 
| 41 |  | 3re 12346 | . . . . . 6
⊢ 3 ∈
ℝ | 
| 42 |  | 2nn 12339 | . . . . . . . . 9
⊢ 2 ∈
ℕ | 
| 43 |  | nnexpcl 14115 | . . . . . . . . 9
⊢ ((2
∈ ℕ ∧ (𝑘 +
1) ∈ ℕ0) → (2↑(𝑘 + 1)) ∈ ℕ) | 
| 44 | 42, 12, 43 | sylancr 587 | . . . . . . . 8
⊢ (𝑘 ∈ ℕ0
→ (2↑(𝑘 + 1))
∈ ℕ) | 
| 45 | 44 | nnrpd 13075 | . . . . . . 7
⊢ (𝑘 ∈ ℕ0
→ (2↑(𝑘 + 1))
∈ ℝ+) | 
| 46 | 45 | adantl 481 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(2↑(𝑘 + 1)) ∈
ℝ+) | 
| 47 |  | rerpdivcl 13065 | . . . . . 6
⊢ ((3
∈ ℝ ∧ (2↑(𝑘 + 1)) ∈ ℝ+) → (3
/ (2↑(𝑘 + 1))) ∈
ℝ) | 
| 48 | 41, 46, 47 | sylancr 587 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (3 /
(2↑(𝑘 + 1))) ∈
ℝ) | 
| 49 |  | nnexpcl 14115 | . . . . . . . . 9
⊢ ((2
∈ ℕ ∧ 𝑘
∈ ℕ0) → (2↑𝑘) ∈ ℕ) | 
| 50 | 42, 49 | mpan 690 | . . . . . . . 8
⊢ (𝑘 ∈ ℕ0
→ (2↑𝑘) ∈
ℕ) | 
| 51 | 50 | nnrpd 13075 | . . . . . . 7
⊢ (𝑘 ∈ ℕ0
→ (2↑𝑘) ∈
ℝ+) | 
| 52 | 51 | adantl 481 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(2↑𝑘) ∈
ℝ+) | 
| 53 |  | rerpdivcl 13065 | . . . . . 6
⊢ ((3
∈ ℝ ∧ (2↑𝑘) ∈ ℝ+) → (3 /
(2↑𝑘)) ∈
ℝ) | 
| 54 | 41, 52, 53 | sylancr 587 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (3 /
(2↑𝑘)) ∈
ℝ) | 
| 55 |  | oveq1 7438 | . . . . . . . . . . . 12
⊢ (𝑧 = (𝑆‘𝑘) → (𝑧(ball‘𝐷)(1 / (2↑𝑚))) = ((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑚)))) | 
| 56 |  | oveq2 7439 | . . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑘 → (2↑𝑚) = (2↑𝑘)) | 
| 57 | 56 | oveq2d 7447 | . . . . . . . . . . . . 13
⊢ (𝑚 = 𝑘 → (1 / (2↑𝑚)) = (1 / (2↑𝑘))) | 
| 58 | 57 | oveq2d 7447 | . . . . . . . . . . . 12
⊢ (𝑚 = 𝑘 → ((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑚))) = ((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘)))) | 
| 59 |  | ovex 7464 | . . . . . . . . . . . 12
⊢ ((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∈ V | 
| 60 | 55, 58, 19, 59 | ovmpo 7593 | . . . . . . . . . . 11
⊢ (((𝑆‘𝑘) ∈ 𝑋 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘𝑘)𝐵𝑘) = ((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘)))) | 
| 61 | 40, 60 | sylancom 588 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘𝑘)𝐵𝑘) = ((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘)))) | 
| 62 |  | df-br 5144 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑆‘𝑘)𝐺𝑘 ↔ 〈(𝑆‘𝑘), 𝑘〉 ∈ 𝐺) | 
| 63 |  | fveq2 6906 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 〈(𝑆‘𝑘), 𝑘〉 → (𝑇‘𝑥) = (𝑇‘〈(𝑆‘𝑘), 𝑘〉)) | 
| 64 |  | df-ov 7434 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑆‘𝑘)𝑇𝑘) = (𝑇‘〈(𝑆‘𝑘), 𝑘〉) | 
| 65 | 63, 64 | eqtr4di 2795 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 〈(𝑆‘𝑘), 𝑘〉 → (𝑇‘𝑥) = ((𝑆‘𝑘)𝑇𝑘)) | 
| 66 | 35, 36 | op2ndd 8025 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 〈(𝑆‘𝑘), 𝑘〉 → (2nd ‘𝑥) = 𝑘) | 
| 67 | 66 | oveq1d 7446 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 〈(𝑆‘𝑘), 𝑘〉 → ((2nd ‘𝑥) + 1) = (𝑘 + 1)) | 
| 68 | 65, 67 | breq12d 5156 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 〈(𝑆‘𝑘), 𝑘〉 → ((𝑇‘𝑥)𝐺((2nd ‘𝑥) + 1) ↔ ((𝑆‘𝑘)𝑇𝑘)𝐺(𝑘 + 1))) | 
| 69 |  | fveq2 6906 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 〈(𝑆‘𝑘), 𝑘〉 → (𝐵‘𝑥) = (𝐵‘〈(𝑆‘𝑘), 𝑘〉)) | 
| 70 |  | df-ov 7434 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑆‘𝑘)𝐵𝑘) = (𝐵‘〈(𝑆‘𝑘), 𝑘〉) | 
| 71 | 69, 70 | eqtr4di 2795 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 〈(𝑆‘𝑘), 𝑘〉 → (𝐵‘𝑥) = ((𝑆‘𝑘)𝐵𝑘)) | 
| 72 | 65, 67 | oveq12d 7449 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 〈(𝑆‘𝑘), 𝑘〉 → ((𝑇‘𝑥)𝐵((2nd ‘𝑥) + 1)) = (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) | 
| 73 | 71, 72 | ineq12d 4221 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 〈(𝑆‘𝑘), 𝑘〉 → ((𝐵‘𝑥) ∩ ((𝑇‘𝑥)𝐵((2nd ‘𝑥) + 1))) = (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1)))) | 
| 74 | 73 | eleq1d 2826 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 〈(𝑆‘𝑘), 𝑘〉 → (((𝐵‘𝑥) ∩ ((𝑇‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾 ↔ (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾)) | 
| 75 | 68, 74 | anbi12d 632 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 〈(𝑆‘𝑘), 𝑘〉 → (((𝑇‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑇‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾) ↔ (((𝑆‘𝑘)𝑇𝑘)𝐺(𝑘 + 1) ∧ (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾))) | 
| 76 | 75 | rspccv 3619 | . . . . . . . . . . . . . . . . . 18
⊢
(∀𝑥 ∈
𝐺 ((𝑇‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑇‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾) → (〈(𝑆‘𝑘), 𝑘〉 ∈ 𝐺 → (((𝑆‘𝑘)𝑇𝑘)𝐺(𝑘 + 1) ∧ (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾))) | 
| 77 | 21, 76 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (〈(𝑆‘𝑘), 𝑘〉 ∈ 𝐺 → (((𝑆‘𝑘)𝑇𝑘)𝐺(𝑘 + 1) ∧ (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾))) | 
| 78 | 62, 77 | biimtrid 242 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑆‘𝑘)𝐺𝑘 → (((𝑆‘𝑘)𝑇𝑘)𝐺(𝑘 + 1) ∧ (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾))) | 
| 79 | 78 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘𝑘)𝐺𝑘 → (((𝑆‘𝑘)𝑇𝑘)𝐺(𝑘 + 1) ∧ (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾))) | 
| 80 | 34, 79 | mpd 15 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑆‘𝑘)𝑇𝑘)𝐺(𝑘 + 1) ∧ (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾)) | 
| 81 | 80 | simpld 494 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘𝑘)𝑇𝑘)𝐺(𝑘 + 1)) | 
| 82 |  | ovex 7464 | . . . . . . . . . . . . . . 15
⊢ ((𝑆‘𝑘)𝑇𝑘) ∈ V | 
| 83 | 16, 17, 18, 82, 27 | heiborlem2 37819 | . . . . . . . . . . . . . 14
⊢ (((𝑆‘𝑘)𝑇𝑘)𝐺(𝑘 + 1) ↔ ((𝑘 + 1) ∈ ℕ0 ∧
((𝑆‘𝑘)𝑇𝑘) ∈ (𝐹‘(𝑘 + 1)) ∧ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1)) ∈ 𝐾)) | 
| 84 | 83 | simp2bi 1147 | . . . . . . . . . . . . 13
⊢ (((𝑆‘𝑘)𝑇𝑘)𝐺(𝑘 + 1) → ((𝑆‘𝑘)𝑇𝑘) ∈ (𝐹‘(𝑘 + 1))) | 
| 85 | 81, 84 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘𝑘)𝑇𝑘) ∈ (𝐹‘(𝑘 + 1))) | 
| 86 | 15, 85 | sseldd 3984 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘𝑘)𝑇𝑘) ∈ 𝑋) | 
| 87 | 12 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑘 + 1) ∈
ℕ0) | 
| 88 |  | oveq1 7438 | . . . . . . . . . . . 12
⊢ (𝑧 = ((𝑆‘𝑘)𝑇𝑘) → (𝑧(ball‘𝐷)(1 / (2↑𝑚))) = (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑𝑚)))) | 
| 89 |  | oveq2 7439 | . . . . . . . . . . . . . 14
⊢ (𝑚 = (𝑘 + 1) → (2↑𝑚) = (2↑(𝑘 + 1))) | 
| 90 | 89 | oveq2d 7447 | . . . . . . . . . . . . 13
⊢ (𝑚 = (𝑘 + 1) → (1 / (2↑𝑚)) = (1 / (2↑(𝑘 + 1)))) | 
| 91 | 90 | oveq2d 7447 | . . . . . . . . . . . 12
⊢ (𝑚 = (𝑘 + 1) → (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑𝑚))) = (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))) | 
| 92 |  | ovex 7464 | . . . . . . . . . . . 12
⊢ (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1)))) ∈ V | 
| 93 | 88, 91, 19, 92 | ovmpo 7593 | . . . . . . . . . . 11
⊢ ((((𝑆‘𝑘)𝑇𝑘) ∈ 𝑋 ∧ (𝑘 + 1) ∈ ℕ0) →
(((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1)) = (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))) | 
| 94 | 86, 87, 93 | syl2anc 584 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1)) = (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))) | 
| 95 | 61, 94 | ineq12d 4221 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) = (((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1)))))) | 
| 96 | 80 | simprd 495 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾) | 
| 97 |  | 0elpw 5356 | . . . . . . . . . . . . 13
⊢ ∅
∈ 𝒫 𝑈 | 
| 98 |  | 0fi 9082 | . . . . . . . . . . . . 13
⊢ ∅
∈ Fin | 
| 99 |  | elin 3967 | . . . . . . . . . . . . 13
⊢ (∅
∈ (𝒫 𝑈 ∩
Fin) ↔ (∅ ∈ 𝒫 𝑈 ∧ ∅ ∈ Fin)) | 
| 100 | 97, 98, 99 | mpbir2an 711 | . . . . . . . . . . . 12
⊢ ∅
∈ (𝒫 𝑈 ∩
Fin) | 
| 101 |  | 0ss 4400 | . . . . . . . . . . . 12
⊢ ∅
⊆ ∪ ∅ | 
| 102 |  | unieq 4918 | . . . . . . . . . . . . . 14
⊢ (𝑣 = ∅ → ∪ 𝑣 =
∪ ∅) | 
| 103 | 102 | sseq2d 4016 | . . . . . . . . . . . . 13
⊢ (𝑣 = ∅ → (∅
⊆ ∪ 𝑣 ↔ ∅ ⊆ ∪ ∅)) | 
| 104 | 103 | rspcev 3622 | . . . . . . . . . . . 12
⊢ ((∅
∈ (𝒫 𝑈 ∩
Fin) ∧ ∅ ⊆ ∪ ∅) →
∃𝑣 ∈ (𝒫
𝑈 ∩ Fin)∅ ⊆
∪ 𝑣) | 
| 105 | 100, 101,
104 | mp2an 692 | . . . . . . . . . . 11
⊢
∃𝑣 ∈
(𝒫 𝑈 ∩
Fin)∅ ⊆ ∪ 𝑣 | 
| 106 |  | 0ex 5307 | . . . . . . . . . . . . 13
⊢ ∅
∈ V | 
| 107 |  | sseq1 4009 | . . . . . . . . . . . . . . 15
⊢ (𝑢 = ∅ → (𝑢 ⊆ ∪ 𝑣
↔ ∅ ⊆ ∪ 𝑣)) | 
| 108 | 107 | rexbidv 3179 | . . . . . . . . . . . . . 14
⊢ (𝑢 = ∅ → (∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣 ↔ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∅ ⊆ ∪ 𝑣)) | 
| 109 | 108 | notbid 318 | . . . . . . . . . . . . 13
⊢ (𝑢 = ∅ → (¬
∃𝑣 ∈ (𝒫
𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣
↔ ¬ ∃𝑣
∈ (𝒫 𝑈 ∩
Fin)∅ ⊆ ∪ 𝑣)) | 
| 110 | 106, 109,
17 | elab2 3682 | . . . . . . . . . . . 12
⊢ (∅
∈ 𝐾 ↔ ¬
∃𝑣 ∈ (𝒫
𝑈 ∩ Fin)∅ ⊆
∪ 𝑣) | 
| 111 | 110 | con2bii 357 | . . . . . . . . . . 11
⊢
(∃𝑣 ∈
(𝒫 𝑈 ∩
Fin)∅ ⊆ ∪ 𝑣 ↔ ¬ ∅ ∈ 𝐾) | 
| 112 | 105, 111 | mpbi 230 | . . . . . . . . . 10
⊢  ¬
∅ ∈ 𝐾 | 
| 113 |  | nelne2 3040 | . . . . . . . . . 10
⊢
(((((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ∈ 𝐾 ∧ ¬ ∅ ∈ 𝐾) → (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ≠ ∅) | 
| 114 | 96, 112, 113 | sylancl 586 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑆‘𝑘)𝐵𝑘) ∩ (((𝑆‘𝑘)𝑇𝑘)𝐵(𝑘 + 1))) ≠ ∅) | 
| 115 | 95, 114 | eqnetrrd 3009 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))) ≠ ∅) | 
| 116 | 51 | rpreccld 13087 | . . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ0
→ (1 / (2↑𝑘))
∈ ℝ+) | 
| 117 | 116 | adantl 481 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (1 /
(2↑𝑘)) ∈
ℝ+) | 
| 118 | 117 | rpred 13077 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (1 /
(2↑𝑘)) ∈
ℝ) | 
| 119 | 45 | rpreccld 13087 | . . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ0
→ (1 / (2↑(𝑘 +
1))) ∈ ℝ+) | 
| 120 | 119 | adantl 481 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (1 /
(2↑(𝑘 + 1))) ∈
ℝ+) | 
| 121 | 120 | rpred 13077 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (1 /
(2↑(𝑘 + 1))) ∈
ℝ) | 
| 122 |  | rexadd 13274 | . . . . . . . . . . . 12
⊢ (((1 /
(2↑𝑘)) ∈ ℝ
∧ (1 / (2↑(𝑘 +
1))) ∈ ℝ) → ((1 / (2↑𝑘)) +𝑒 (1 / (2↑(𝑘 + 1)))) = ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1))))) | 
| 123 | 118, 121,
122 | syl2anc 584 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((1 /
(2↑𝑘))
+𝑒 (1 / (2↑(𝑘 + 1)))) = ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1))))) | 
| 124 | 123 | breq1d 5153 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((1 /
(2↑𝑘))
+𝑒 (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)) ↔ ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)))) | 
| 125 | 117 | rpxrd 13078 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (1 /
(2↑𝑘)) ∈
ℝ*) | 
| 126 | 120 | rpxrd 13078 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (1 /
(2↑(𝑘 + 1))) ∈
ℝ*) | 
| 127 |  | bldisj 24408 | . . . . . . . . . . . . 13
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑆‘𝑘) ∈ 𝑋 ∧ ((𝑆‘𝑘)𝑇𝑘) ∈ 𝑋) ∧ ((1 / (2↑𝑘)) ∈ ℝ* ∧ (1 /
(2↑(𝑘 + 1))) ∈
ℝ* ∧ ((1 / (2↑𝑘)) +𝑒 (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)))) → (((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))) = ∅) | 
| 128 | 127 | 3exp2 1355 | . . . . . . . . . . . 12
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑆‘𝑘) ∈ 𝑋 ∧ ((𝑆‘𝑘)𝑇𝑘) ∈ 𝑋) → ((1 / (2↑𝑘)) ∈ ℝ* → ((1 /
(2↑(𝑘 + 1))) ∈
ℝ* → (((1 / (2↑𝑘)) +𝑒 (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)) → (((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))) = ∅)))) | 
| 129 | 128 | imp32 418 | . . . . . . . . . . 11
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑆‘𝑘) ∈ 𝑋 ∧ ((𝑆‘𝑘)𝑇𝑘) ∈ 𝑋) ∧ ((1 / (2↑𝑘)) ∈ ℝ* ∧ (1 /
(2↑(𝑘 + 1))) ∈
ℝ*)) → (((1 / (2↑𝑘)) +𝑒 (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)) → (((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))) = ∅)) | 
| 130 | 7, 40, 86, 125, 126, 129 | syl32anc 1380 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((1 /
(2↑𝑘))
+𝑒 (1 / (2↑(𝑘 + 1)))) ≤ ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)) → (((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))) = ∅)) | 
| 131 | 124, 130 | sylbird 260 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((1 /
(2↑𝑘)) + (1 /
(2↑(𝑘 + 1)))) ≤
((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)) → (((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))) = ∅)) | 
| 132 | 131 | necon3ad 2953 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((((𝑆‘𝑘)(ball‘𝐷)(1 / (2↑𝑘))) ∩ (((𝑆‘𝑘)𝑇𝑘)(ball‘𝐷)(1 / (2↑(𝑘 + 1))))) ≠ ∅ → ¬ ((1 /
(2↑𝑘)) + (1 /
(2↑(𝑘 + 1)))) ≤
((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)))) | 
| 133 | 115, 132 | mpd 15 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ¬ ((1
/ (2↑𝑘)) + (1 /
(2↑(𝑘 + 1)))) ≤
((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘))) | 
| 134 | 117, 120 | rpaddcld 13092 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((1 /
(2↑𝑘)) + (1 /
(2↑(𝑘 + 1)))) ∈
ℝ+) | 
| 135 | 134 | rpred 13077 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((1 /
(2↑𝑘)) + (1 /
(2↑(𝑘 + 1)))) ∈
ℝ) | 
| 136 | 4 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐷 ∈ (Met‘𝑋)) | 
| 137 |  | metcl 24342 | . . . . . . . . . 10
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝑆‘𝑘) ∈ 𝑋 ∧ ((𝑆‘𝑘)𝑇𝑘) ∈ 𝑋) → ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)) ∈ ℝ) | 
| 138 | 136, 40, 86, 137 | syl3anc 1373 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)) ∈ ℝ) | 
| 139 | 135, 138 | letrid 11413 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((1 /
(2↑𝑘)) + (1 /
(2↑(𝑘 + 1)))) ≤
((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)) ∨ ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)) ≤ ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))))) | 
| 140 | 139 | ord 865 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (¬
((1 / (2↑𝑘)) + (1 /
(2↑(𝑘 + 1)))) ≤
((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)) → ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)) ≤ ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1)))))) | 
| 141 | 133, 140 | mpd 15 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘)) ≤ ((1 / (2↑𝑘)) + (1 / (2↑(𝑘 + 1))))) | 
| 142 |  | seqp1 14057 | . . . . . . . . . . . 12
⊢ (𝑘 ∈
(ℤ≥‘0) → (seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘(𝑘 + 1)) = ((seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1)))) | 
| 143 |  | nn0uz 12920 | . . . . . . . . . . . 12
⊢
ℕ0 = (ℤ≥‘0) | 
| 144 | 142, 143 | eleq2s 2859 | . . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
→ (seq0(𝑇, (𝑚 ∈ ℕ0
↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘(𝑘 + 1)) = ((seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1)))) | 
| 145 | 23 | fveq1i 6907 | . . . . . . . . . . 11
⊢ (𝑆‘(𝑘 + 1)) = (seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘(𝑘 + 1)) | 
| 146 | 23 | fveq1i 6907 | . . . . . . . . . . . 12
⊢ (𝑆‘𝑘) = (seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘𝑘) | 
| 147 | 146 | oveq1i 7441 | . . . . . . . . . . 11
⊢ ((𝑆‘𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1))) = ((seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))‘𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1))) | 
| 148 | 144, 145,
147 | 3eqtr4g 2802 | . . . . . . . . . 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 7438 | . . . . . . . . . . . . . 14
⊢ (𝑚 = (𝑘 + 1) → (𝑚 − 1) = ((𝑘 + 1) − 1)) | 
| 152 | 150, 151 | ifbieq2d 4552 | . . . . . . . . . . . . 13
⊢ (𝑚 = (𝑘 + 1) → if(𝑚 = 0, 𝐶, (𝑚 − 1)) = if((𝑘 + 1) = 0, 𝐶, ((𝑘 + 1) − 1))) | 
| 153 |  | nn0p1nn 12565 | . . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ0
→ (𝑘 + 1) ∈
ℕ) | 
| 154 |  | nnne0 12300 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑘 + 1) ∈ ℕ →
(𝑘 + 1) ≠
0) | 
| 155 | 154 | neneqd 2945 | . . . . . . . . . . . . . . . 16
⊢ ((𝑘 + 1) ∈ ℕ →
¬ (𝑘 + 1) =
0) | 
| 156 | 153, 155 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ0
→ ¬ (𝑘 + 1) =
0) | 
| 157 | 156 | iffalsed 4536 | . . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ0
→ if((𝑘 + 1) = 0,
𝐶, ((𝑘 + 1) − 1)) = ((𝑘 + 1) − 1)) | 
| 158 |  | ovex 7464 | . . . . . . . . . . . . . 14
⊢ ((𝑘 + 1) − 1) ∈
V | 
| 159 | 157, 158 | eqeltrdi 2849 | . . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ0
→ if((𝑘 + 1) = 0,
𝐶, ((𝑘 + 1) − 1)) ∈ V) | 
| 160 | 149, 152,
12, 159 | fvmptd3 7039 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ0
→ ((𝑚 ∈
ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1)) = if((𝑘 + 1) = 0, 𝐶, ((𝑘 + 1) − 1))) | 
| 161 |  | nn0cn 12536 | . . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℂ) | 
| 162 |  | ax-1cn 11213 | . . . . . . . . . . . . 13
⊢ 1 ∈
ℂ | 
| 163 |  | pncan 11514 | . . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑘 + 1)
− 1) = 𝑘) | 
| 164 | 161, 162,
163 | sylancl 586 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ0
→ ((𝑘 + 1) − 1)
= 𝑘) | 
| 165 | 160, 157,
164 | 3eqtrd 2781 | . . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
→ ((𝑚 ∈
ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1)) = 𝑘) | 
| 166 | 165 | oveq2d 7447 | . . . . . . . . . 10
⊢ (𝑘 ∈ ℕ0
→ ((𝑆‘𝑘)𝑇((𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1)))‘(𝑘 + 1))) = ((𝑆‘𝑘)𝑇𝑘)) | 
| 167 | 148, 166 | eqtrd 2777 | . . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
→ (𝑆‘(𝑘 + 1)) = ((𝑆‘𝑘)𝑇𝑘)) | 
| 168 | 167 | adantl 481 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑆‘(𝑘 + 1)) = ((𝑆‘𝑘)𝑇𝑘)) | 
| 169 | 168 | oveq1d 7446 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘(𝑘 + 1))𝐷(𝑆‘𝑘)) = (((𝑆‘𝑘)𝑇𝑘)𝐷(𝑆‘𝑘))) | 
| 170 |  | metsym 24360 | . . . . . . . 8
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ ((𝑆‘𝑘)𝑇𝑘) ∈ 𝑋 ∧ (𝑆‘𝑘) ∈ 𝑋) → (((𝑆‘𝑘)𝑇𝑘)𝐷(𝑆‘𝑘)) = ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘))) | 
| 171 | 136, 86, 40, 170 | syl3anc 1373 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑆‘𝑘)𝑇𝑘)𝐷(𝑆‘𝑘)) = ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘))) | 
| 172 | 169, 171 | eqtrd 2777 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘(𝑘 + 1))𝐷(𝑆‘𝑘)) = ((𝑆‘𝑘)𝐷((𝑆‘𝑘)𝑇𝑘))) | 
| 173 |  | 3cn 12347 | . . . . . . . . . . . . 13
⊢ 3 ∈
ℂ | 
| 174 | 173 | 2timesi 12404 | . . . . . . . . . . . 12
⊢ (2
· 3) = (3 + 3) | 
| 175 | 174 | oveq1i 7441 | . . . . . . . . . . 11
⊢ ((2
· 3) − 3) = ((3 + 3) − 3) | 
| 176 | 173, 173 | pncan3oi 11524 | . . . . . . . . . . 11
⊢ ((3 + 3)
− 3) = 3 | 
| 177 |  | df-3 12330 | . . . . . . . . . . 11
⊢ 3 = (2 +
1) | 
| 178 | 175, 176,
177 | 3eqtri 2769 | . . . . . . . . . 10
⊢ ((2
· 3) − 3) = (2 + 1) | 
| 179 | 178 | oveq1i 7441 | . . . . . . . . 9
⊢ (((2
· 3) − 3) / (2↑(𝑘 + 1))) = ((2 + 1) / (2↑(𝑘 + 1))) | 
| 180 |  | rpcn 13045 | . . . . . . . . . . 11
⊢
((2↑(𝑘 + 1))
∈ ℝ+ → (2↑(𝑘 + 1)) ∈ ℂ) | 
| 181 |  | rpne0 13051 | . . . . . . . . . . 11
⊢
((2↑(𝑘 + 1))
∈ ℝ+ → (2↑(𝑘 + 1)) ≠ 0) | 
| 182 |  | 2cn 12341 | . . . . . . . . . . . . 13
⊢ 2 ∈
ℂ | 
| 183 | 182, 173 | mulcli 11268 | . . . . . . . . . . . 12
⊢ (2
· 3) ∈ ℂ | 
| 184 |  | divsubdir 11961 | . . . . . . . . . . . 12
⊢ (((2
· 3) ∈ ℂ ∧ 3 ∈ ℂ ∧ ((2↑(𝑘 + 1)) ∈ ℂ ∧
(2↑(𝑘 + 1)) ≠ 0))
→ (((2 · 3) − 3) / (2↑(𝑘 + 1))) = (((2 · 3) / (2↑(𝑘 + 1))) − (3 /
(2↑(𝑘 +
1))))) | 
| 185 | 183, 173,
184 | mp3an12 1453 | . . . . . . . . . . 11
⊢
(((2↑(𝑘 + 1))
∈ ℂ ∧ (2↑(𝑘 + 1)) ≠ 0) → (((2 · 3)
− 3) / (2↑(𝑘 +
1))) = (((2 · 3) / (2↑(𝑘 + 1))) − (3 / (2↑(𝑘 + 1))))) | 
| 186 | 180, 181,
185 | syl2anc 584 | . . . . . . . . . 10
⊢
((2↑(𝑘 + 1))
∈ ℝ+ → (((2 · 3) − 3) / (2↑(𝑘 + 1))) = (((2 · 3) /
(2↑(𝑘 + 1))) −
(3 / (2↑(𝑘 +
1))))) | 
| 187 | 45, 186 | syl 17 | . . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
→ (((2 · 3) − 3) / (2↑(𝑘 + 1))) = (((2 · 3) / (2↑(𝑘 + 1))) − (3 /
(2↑(𝑘 +
1))))) | 
| 188 |  | divdir 11947 | . . . . . . . . . . . 12
⊢ ((2
∈ ℂ ∧ 1 ∈ ℂ ∧ ((2↑(𝑘 + 1)) ∈ ℂ ∧ (2↑(𝑘 + 1)) ≠ 0)) → ((2 + 1)
/ (2↑(𝑘 + 1))) = ((2 /
(2↑(𝑘 + 1))) + (1 /
(2↑(𝑘 +
1))))) | 
| 189 | 182, 162,
188 | mp3an12 1453 | . . . . . . . . . . 11
⊢
(((2↑(𝑘 + 1))
∈ ℂ ∧ (2↑(𝑘 + 1)) ≠ 0) → ((2 + 1) /
(2↑(𝑘 + 1))) = ((2 /
(2↑(𝑘 + 1))) + (1 /
(2↑(𝑘 +
1))))) | 
| 190 | 180, 181,
189 | syl2anc 584 | . . . . . . . . . 10
⊢
((2↑(𝑘 + 1))
∈ ℝ+ → ((2 + 1) / (2↑(𝑘 + 1))) = ((2 / (2↑(𝑘 + 1))) + (1 / (2↑(𝑘 + 1))))) | 
| 191 | 45, 190 | syl 17 | . . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
→ ((2 + 1) / (2↑(𝑘 + 1))) = ((2 / (2↑(𝑘 + 1))) + (1 / (2↑(𝑘 + 1))))) | 
| 192 | 179, 187,
191 | 3eqtr3a 2801 | . . . . . . . 8
⊢ (𝑘 ∈ ℕ0
→ (((2 · 3) / (2↑(𝑘 + 1))) − (3 / (2↑(𝑘 + 1)))) = ((2 / (2↑(𝑘 + 1))) + (1 / (2↑(𝑘 + 1))))) | 
| 193 |  | rpcn 13045 | . . . . . . . . . . . 12
⊢
((2↑𝑘) ∈
ℝ+ → (2↑𝑘) ∈ ℂ) | 
| 194 |  | rpne0 13051 | . . . . . . . . . . . 12
⊢
((2↑𝑘) ∈
ℝ+ → (2↑𝑘) ≠ 0) | 
| 195 |  | 2cnne0 12476 | . . . . . . . . . . . . 13
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) | 
| 196 |  | divcan5 11969 | . . . . . . . . . . . . 13
⊢ ((3
∈ ℂ ∧ ((2↑𝑘) ∈ ℂ ∧ (2↑𝑘) ≠ 0) ∧ (2 ∈
ℂ ∧ 2 ≠ 0)) → ((2 · 3) / (2 · (2↑𝑘))) = (3 / (2↑𝑘))) | 
| 197 | 173, 195,
196 | mp3an13 1454 | . . . . . . . . . . . 12
⊢
(((2↑𝑘) ∈
ℂ ∧ (2↑𝑘)
≠ 0) → ((2 · 3) / (2 · (2↑𝑘))) = (3 / (2↑𝑘))) | 
| 198 | 193, 194,
197 | syl2anc 584 | . . . . . . . . . . 11
⊢
((2↑𝑘) ∈
ℝ+ → ((2 · 3) / (2 · (2↑𝑘))) = (3 / (2↑𝑘))) | 
| 199 | 51, 198 | syl 17 | . . . . . . . . . 10
⊢ (𝑘 ∈ ℕ0
→ ((2 · 3) / (2 · (2↑𝑘))) = (3 / (2↑𝑘))) | 
| 200 | 51, 193 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ0
→ (2↑𝑘) ∈
ℂ) | 
| 201 |  | mulcom 11241 | . . . . . . . . . . . . 13
⊢ ((2
∈ ℂ ∧ (2↑𝑘) ∈ ℂ) → (2 ·
(2↑𝑘)) =
((2↑𝑘) ·
2)) | 
| 202 | 182, 200,
201 | sylancr 587 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ0
→ (2 · (2↑𝑘)) = ((2↑𝑘) · 2)) | 
| 203 |  | expp1 14109 | . . . . . . . . . . . . 13
⊢ ((2
∈ ℂ ∧ 𝑘
∈ ℕ0) → (2↑(𝑘 + 1)) = ((2↑𝑘) · 2)) | 
| 204 | 182, 203 | mpan 690 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ0
→ (2↑(𝑘 + 1)) =
((2↑𝑘) ·
2)) | 
| 205 | 202, 204 | eqtr4d 2780 | . . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
→ (2 · (2↑𝑘)) = (2↑(𝑘 + 1))) | 
| 206 | 205 | oveq2d 7447 | . . . . . . . . . 10
⊢ (𝑘 ∈ ℕ0
→ ((2 · 3) / (2 · (2↑𝑘))) = ((2 · 3) / (2↑(𝑘 + 1)))) | 
| 207 | 199, 206 | eqtr3d 2779 | . . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
→ (3 / (2↑𝑘)) =
((2 · 3) / (2↑(𝑘 + 1)))) | 
| 208 | 207 | oveq1d 7446 | . . . . . . . 8
⊢ (𝑘 ∈ ℕ0
→ ((3 / (2↑𝑘))
− (3 / (2↑(𝑘 +
1)))) = (((2 · 3) / (2↑(𝑘 + 1))) − (3 / (2↑(𝑘 + 1))))) | 
| 209 |  | divcan5 11969 | . . . . . . . . . . . . 13
⊢ ((1
∈ ℂ ∧ ((2↑𝑘) ∈ ℂ ∧ (2↑𝑘) ≠ 0) ∧ (2 ∈
ℂ ∧ 2 ≠ 0)) → ((2 · 1) / (2 · (2↑𝑘))) = (1 / (2↑𝑘))) | 
| 210 | 162, 195,
209 | mp3an13 1454 | . . . . . . . . . . . 12
⊢
(((2↑𝑘) ∈
ℂ ∧ (2↑𝑘)
≠ 0) → ((2 · 1) / (2 · (2↑𝑘))) = (1 / (2↑𝑘))) | 
| 211 | 193, 194,
210 | syl2anc 584 | . . . . . . . . . . 11
⊢
((2↑𝑘) ∈
ℝ+ → ((2 · 1) / (2 · (2↑𝑘))) = (1 / (2↑𝑘))) | 
| 212 | 51, 211 | syl 17 | . . . . . . . . . 10
⊢ (𝑘 ∈ ℕ0
→ ((2 · 1) / (2 · (2↑𝑘))) = (1 / (2↑𝑘))) | 
| 213 |  | 2t1e2 12429 | . . . . . . . . . . . 12
⊢ (2
· 1) = 2 | 
| 214 | 213 | a1i 11 | . . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
→ (2 · 1) = 2) | 
| 215 | 214, 205 | oveq12d 7449 | . . . . . . . . . 10
⊢ (𝑘 ∈ ℕ0
→ ((2 · 1) / (2 · (2↑𝑘))) = (2 / (2↑(𝑘 + 1)))) | 
| 216 | 212, 215 | eqtr3d 2779 | . . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
→ (1 / (2↑𝑘)) =
(2 / (2↑(𝑘 +
1)))) | 
| 217 | 216 | oveq1d 7446 | . . . . . . . 8
⊢ (𝑘 ∈ ℕ0
→ ((1 / (2↑𝑘)) +
(1 / (2↑(𝑘 + 1)))) =
((2 / (2↑(𝑘 + 1))) +
(1 / (2↑(𝑘 +
1))))) | 
| 218 | 192, 208,
217 | 3eqtr4d 2787 | . . . . . . 7
⊢ (𝑘 ∈ ℕ0
→ ((3 / (2↑𝑘))
− (3 / (2↑(𝑘 +
1)))) = ((1 / (2↑𝑘)) +
(1 / (2↑(𝑘 +
1))))) | 
| 219 | 218 | adantl 481 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((3 /
(2↑𝑘)) − (3 /
(2↑(𝑘 + 1)))) = ((1 /
(2↑𝑘)) + (1 /
(2↑(𝑘 +
1))))) | 
| 220 | 141, 172,
219 | 3brtr4d 5175 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘(𝑘 + 1))𝐷(𝑆‘𝑘)) ≤ ((3 / (2↑𝑘)) − (3 / (2↑(𝑘 + 1))))) | 
| 221 |  | blss2 24414 | . . . . 5
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑆‘(𝑘 + 1)) ∈ 𝑋 ∧ (𝑆‘𝑘) ∈ 𝑋) ∧ ((3 / (2↑(𝑘 + 1))) ∈ ℝ ∧ (3 /
(2↑𝑘)) ∈ ℝ
∧ ((𝑆‘(𝑘 + 1))𝐷(𝑆‘𝑘)) ≤ ((3 / (2↑𝑘)) − (3 / (2↑(𝑘 + 1)))))) → ((𝑆‘(𝑘 + 1))(ball‘𝐷)(3 / (2↑(𝑘 + 1)))) ⊆ ((𝑆‘𝑘)(ball‘𝐷)(3 / (2↑𝑘)))) | 
| 222 | 7, 31, 40, 48, 54, 220, 221 | syl33anc 1387 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑆‘(𝑘 + 1))(ball‘𝐷)(3 / (2↑(𝑘 + 1)))) ⊆ ((𝑆‘𝑘)(ball‘𝐷)(3 / (2↑𝑘)))) | 
| 223 | 1, 222 | sylan2 593 | . . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑆‘(𝑘 + 1))(ball‘𝐷)(3 / (2↑(𝑘 + 1)))) ⊆ ((𝑆‘𝑘)(ball‘𝐷)(3 / (2↑𝑘)))) | 
| 224 |  | peano2nn 12278 | . . . . . . 7
⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈
ℕ) | 
| 225 |  | fveq2 6906 | . . . . . . . . 9
⊢ (𝑛 = (𝑘 + 1) → (𝑆‘𝑛) = (𝑆‘(𝑘 + 1))) | 
| 226 |  | oveq2 7439 | . . . . . . . . . 10
⊢ (𝑛 = (𝑘 + 1) → (2↑𝑛) = (2↑(𝑘 + 1))) | 
| 227 | 226 | oveq2d 7447 | . . . . . . . . 9
⊢ (𝑛 = (𝑘 + 1) → (3 / (2↑𝑛)) = (3 / (2↑(𝑘 + 1)))) | 
| 228 | 225, 227 | opeq12d 4881 | . . . . . . . 8
⊢ (𝑛 = (𝑘 + 1) → 〈(𝑆‘𝑛), (3 / (2↑𝑛))〉 = 〈(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))〉) | 
| 229 |  | heibor.12 | . . . . . . . 8
⊢ 𝑀 = (𝑛 ∈ ℕ ↦ 〈(𝑆‘𝑛), (3 / (2↑𝑛))〉) | 
| 230 |  | opex 5469 | . . . . . . . 8
⊢
〈(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))〉 ∈ V | 
| 231 | 228, 229,
230 | fvmpt 7016 | . . . . . . 7
⊢ ((𝑘 + 1) ∈ ℕ →
(𝑀‘(𝑘 + 1)) = 〈(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))〉) | 
| 232 | 224, 231 | syl 17 | . . . . . 6
⊢ (𝑘 ∈ ℕ → (𝑀‘(𝑘 + 1)) = 〈(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))〉) | 
| 233 | 232 | adantl 481 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑀‘(𝑘 + 1)) = 〈(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))〉) | 
| 234 | 233 | fveq2d 6910 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((ball‘𝐷)‘(𝑀‘(𝑘 + 1))) = ((ball‘𝐷)‘〈(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))〉)) | 
| 235 |  | df-ov 7434 | . . . 4
⊢ ((𝑆‘(𝑘 + 1))(ball‘𝐷)(3 / (2↑(𝑘 + 1)))) = ((ball‘𝐷)‘〈(𝑆‘(𝑘 + 1)), (3 / (2↑(𝑘 + 1)))〉) | 
| 236 | 234, 235 | eqtr4di 2795 | . . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((ball‘𝐷)‘(𝑀‘(𝑘 + 1))) = ((𝑆‘(𝑘 + 1))(ball‘𝐷)(3 / (2↑(𝑘 + 1))))) | 
| 237 |  | fveq2 6906 | . . . . . . . 8
⊢ (𝑛 = 𝑘 → (𝑆‘𝑛) = (𝑆‘𝑘)) | 
| 238 |  | oveq2 7439 | . . . . . . . . 9
⊢ (𝑛 = 𝑘 → (2↑𝑛) = (2↑𝑘)) | 
| 239 | 238 | oveq2d 7447 | . . . . . . . 8
⊢ (𝑛 = 𝑘 → (3 / (2↑𝑛)) = (3 / (2↑𝑘))) | 
| 240 | 237, 239 | opeq12d 4881 | . . . . . . 7
⊢ (𝑛 = 𝑘 → 〈(𝑆‘𝑛), (3 / (2↑𝑛))〉 = 〈(𝑆‘𝑘), (3 / (2↑𝑘))〉) | 
| 241 |  | opex 5469 | . . . . . . 7
⊢
〈(𝑆‘𝑘), (3 / (2↑𝑘))〉 ∈
V | 
| 242 | 240, 229,
241 | fvmpt 7016 | . . . . . 6
⊢ (𝑘 ∈ ℕ → (𝑀‘𝑘) = 〈(𝑆‘𝑘), (3 / (2↑𝑘))〉) | 
| 243 | 242 | fveq2d 6910 | . . . . 5
⊢ (𝑘 ∈ ℕ →
((ball‘𝐷)‘(𝑀‘𝑘)) = ((ball‘𝐷)‘〈(𝑆‘𝑘), (3 / (2↑𝑘))〉)) | 
| 244 |  | df-ov 7434 | . . . . 5
⊢ ((𝑆‘𝑘)(ball‘𝐷)(3 / (2↑𝑘))) = ((ball‘𝐷)‘〈(𝑆‘𝑘), (3 / (2↑𝑘))〉) | 
| 245 | 243, 244 | eqtr4di 2795 | . . . 4
⊢ (𝑘 ∈ ℕ →
((ball‘𝐷)‘(𝑀‘𝑘)) = ((𝑆‘𝑘)(ball‘𝐷)(3 / (2↑𝑘)))) | 
| 246 | 245 | adantl 481 | . . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((ball‘𝐷)‘(𝑀‘𝑘)) = ((𝑆‘𝑘)(ball‘𝐷)(3 / (2↑𝑘)))) | 
| 247 | 223, 236,
246 | 3sstr4d 4039 | . 2
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((ball‘𝐷)‘(𝑀‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝑀‘𝑘))) | 
| 248 | 247 | ralrimiva 3146 | 1
⊢ (𝜑 → ∀𝑘 ∈ ℕ ((ball‘𝐷)‘(𝑀‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝑀‘𝑘))) |