Step |
Hyp |
Ref |
Expression |
1 |
|
heibor.1 |
⊢ 𝐽 = ( MetOpen ‘ 𝐷 ) |
2 |
|
heibor.3 |
⊢ 𝐾 = { 𝑢 ∣ ¬ ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑢 ⊆ ∪ 𝑣 } |
3 |
|
heibor.4 |
⊢ 𝐺 = { 〈 𝑦 , 𝑛 〉 ∣ ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑛 ) ∧ ( 𝑦 𝐵 𝑛 ) ∈ 𝐾 ) } |
4 |
|
heibor.5 |
⊢ 𝐵 = ( 𝑧 ∈ 𝑋 , 𝑚 ∈ ℕ0 ↦ ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) ) |
5 |
|
heibor.6 |
⊢ ( 𝜑 → 𝐷 ∈ ( CMet ‘ 𝑋 ) ) |
6 |
|
heibor.7 |
⊢ ( 𝜑 → 𝐹 : ℕ0 ⟶ ( 𝒫 𝑋 ∩ Fin ) ) |
7 |
|
heibor.8 |
⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑛 ) ( 𝑦 𝐵 𝑛 ) ) |
8 |
|
heibor.9 |
⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐺 ( ( 𝑇 ‘ 𝑥 ) 𝐺 ( ( 2nd ‘ 𝑥 ) + 1 ) ∧ ( ( 𝐵 ‘ 𝑥 ) ∩ ( ( 𝑇 ‘ 𝑥 ) 𝐵 ( ( 2nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ) ) |
9 |
|
heibor.10 |
⊢ ( 𝜑 → 𝐶 𝐺 0 ) |
10 |
|
heibor.11 |
⊢ 𝑆 = seq 0 ( 𝑇 , ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) ) |
11 |
|
heibor.12 |
⊢ 𝑀 = ( 𝑛 ∈ ℕ ↦ 〈 ( 𝑆 ‘ 𝑛 ) , ( 3 / ( 2 ↑ 𝑛 ) ) 〉 ) |
12 |
|
nnnn0 |
⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℕ0 ) |
13 |
|
cmetmet |
⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → 𝐷 ∈ ( Met ‘ 𝑋 ) ) |
14 |
5 13
|
syl |
⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝑋 ) ) |
15 |
|
metxmet |
⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) |
16 |
14 15
|
syl |
⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) |
17 |
16
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) |
18 |
|
inss1 |
⊢ ( 𝒫 𝑋 ∩ Fin ) ⊆ 𝒫 𝑋 |
19 |
|
fss |
⊢ ( ( 𝐹 : ℕ0 ⟶ ( 𝒫 𝑋 ∩ Fin ) ∧ ( 𝒫 𝑋 ∩ Fin ) ⊆ 𝒫 𝑋 ) → 𝐹 : ℕ0 ⟶ 𝒫 𝑋 ) |
20 |
6 18 19
|
sylancl |
⊢ ( 𝜑 → 𝐹 : ℕ0 ⟶ 𝒫 𝑋 ) |
21 |
|
peano2nn0 |
⊢ ( 𝑘 ∈ ℕ0 → ( 𝑘 + 1 ) ∈ ℕ0 ) |
22 |
|
ffvelrn |
⊢ ( ( 𝐹 : ℕ0 ⟶ 𝒫 𝑋 ∧ ( 𝑘 + 1 ) ∈ ℕ0 ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ 𝒫 𝑋 ) |
23 |
20 21 22
|
syl2an |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ 𝒫 𝑋 ) |
24 |
23
|
elpwid |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ⊆ 𝑋 ) |
25 |
1 2 3 4 5 6 7 8 9 10
|
heiborlem4 |
⊢ ( ( 𝜑 ∧ ( 𝑘 + 1 ) ∈ ℕ0 ) → ( 𝑆 ‘ ( 𝑘 + 1 ) ) 𝐺 ( 𝑘 + 1 ) ) |
26 |
21 25
|
sylan2 |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑆 ‘ ( 𝑘 + 1 ) ) 𝐺 ( 𝑘 + 1 ) ) |
27 |
|
fvex |
⊢ ( 𝑆 ‘ ( 𝑘 + 1 ) ) ∈ V |
28 |
|
ovex |
⊢ ( 𝑘 + 1 ) ∈ V |
29 |
1 2 3 27 28
|
heiborlem2 |
⊢ ( ( 𝑆 ‘ ( 𝑘 + 1 ) ) 𝐺 ( 𝑘 + 1 ) ↔ ( ( 𝑘 + 1 ) ∈ ℕ0 ∧ ( 𝑆 ‘ ( 𝑘 + 1 ) ) ∈ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∧ ( ( 𝑆 ‘ ( 𝑘 + 1 ) ) 𝐵 ( 𝑘 + 1 ) ) ∈ 𝐾 ) ) |
30 |
29
|
simp2bi |
⊢ ( ( 𝑆 ‘ ( 𝑘 + 1 ) ) 𝐺 ( 𝑘 + 1 ) → ( 𝑆 ‘ ( 𝑘 + 1 ) ) ∈ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) |
31 |
26 30
|
syl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑆 ‘ ( 𝑘 + 1 ) ) ∈ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) |
32 |
24 31
|
sseldd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑆 ‘ ( 𝑘 + 1 ) ) ∈ 𝑋 ) |
33 |
20
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝒫 𝑋 ) |
34 |
33
|
elpwid |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑘 ) ⊆ 𝑋 ) |
35 |
1 2 3 4 5 6 7 8 9 10
|
heiborlem4 |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑆 ‘ 𝑘 ) 𝐺 𝑘 ) |
36 |
|
fvex |
⊢ ( 𝑆 ‘ 𝑘 ) ∈ V |
37 |
|
vex |
⊢ 𝑘 ∈ V |
38 |
1 2 3 36 37
|
heiborlem2 |
⊢ ( ( 𝑆 ‘ 𝑘 ) 𝐺 𝑘 ↔ ( 𝑘 ∈ ℕ0 ∧ ( 𝑆 ‘ 𝑘 ) ∈ ( 𝐹 ‘ 𝑘 ) ∧ ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ∈ 𝐾 ) ) |
39 |
38
|
simp2bi |
⊢ ( ( 𝑆 ‘ 𝑘 ) 𝐺 𝑘 → ( 𝑆 ‘ 𝑘 ) ∈ ( 𝐹 ‘ 𝑘 ) ) |
40 |
35 39
|
syl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑆 ‘ 𝑘 ) ∈ ( 𝐹 ‘ 𝑘 ) ) |
41 |
34 40
|
sseldd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑆 ‘ 𝑘 ) ∈ 𝑋 ) |
42 |
|
3re |
⊢ 3 ∈ ℝ |
43 |
|
2nn |
⊢ 2 ∈ ℕ |
44 |
|
nnexpcl |
⊢ ( ( 2 ∈ ℕ ∧ ( 𝑘 + 1 ) ∈ ℕ0 ) → ( 2 ↑ ( 𝑘 + 1 ) ) ∈ ℕ ) |
45 |
43 21 44
|
sylancr |
⊢ ( 𝑘 ∈ ℕ0 → ( 2 ↑ ( 𝑘 + 1 ) ) ∈ ℕ ) |
46 |
45
|
nnrpd |
⊢ ( 𝑘 ∈ ℕ0 → ( 2 ↑ ( 𝑘 + 1 ) ) ∈ ℝ+ ) |
47 |
46
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 2 ↑ ( 𝑘 + 1 ) ) ∈ ℝ+ ) |
48 |
|
rerpdivcl |
⊢ ( ( 3 ∈ ℝ ∧ ( 2 ↑ ( 𝑘 + 1 ) ) ∈ ℝ+ ) → ( 3 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ∈ ℝ ) |
49 |
42 47 48
|
sylancr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 3 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ∈ ℝ ) |
50 |
|
nnexpcl |
⊢ ( ( 2 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( 2 ↑ 𝑘 ) ∈ ℕ ) |
51 |
43 50
|
mpan |
⊢ ( 𝑘 ∈ ℕ0 → ( 2 ↑ 𝑘 ) ∈ ℕ ) |
52 |
51
|
nnrpd |
⊢ ( 𝑘 ∈ ℕ0 → ( 2 ↑ 𝑘 ) ∈ ℝ+ ) |
53 |
52
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 2 ↑ 𝑘 ) ∈ ℝ+ ) |
54 |
|
rerpdivcl |
⊢ ( ( 3 ∈ ℝ ∧ ( 2 ↑ 𝑘 ) ∈ ℝ+ ) → ( 3 / ( 2 ↑ 𝑘 ) ) ∈ ℝ ) |
55 |
42 53 54
|
sylancr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 3 / ( 2 ↑ 𝑘 ) ) ∈ ℝ ) |
56 |
|
oveq1 |
⊢ ( 𝑧 = ( 𝑆 ‘ 𝑘 ) → ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) = ( ( 𝑆 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) ) |
57 |
|
oveq2 |
⊢ ( 𝑚 = 𝑘 → ( 2 ↑ 𝑚 ) = ( 2 ↑ 𝑘 ) ) |
58 |
57
|
oveq2d |
⊢ ( 𝑚 = 𝑘 → ( 1 / ( 2 ↑ 𝑚 ) ) = ( 1 / ( 2 ↑ 𝑘 ) ) ) |
59 |
58
|
oveq2d |
⊢ ( 𝑚 = 𝑘 → ( ( 𝑆 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) = ( ( 𝑆 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑘 ) ) ) ) |
60 |
|
ovex |
⊢ ( ( 𝑆 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑘 ) ) ) ∈ V |
61 |
56 59 4 60
|
ovmpo |
⊢ ( ( ( 𝑆 ‘ 𝑘 ) ∈ 𝑋 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) = ( ( 𝑆 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑘 ) ) ) ) |
62 |
41 61
|
sylancom |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) = ( ( 𝑆 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑘 ) ) ) ) |
63 |
|
df-br |
⊢ ( ( 𝑆 ‘ 𝑘 ) 𝐺 𝑘 ↔ 〈 ( 𝑆 ‘ 𝑘 ) , 𝑘 〉 ∈ 𝐺 ) |
64 |
|
fveq2 |
⊢ ( 𝑥 = 〈 ( 𝑆 ‘ 𝑘 ) , 𝑘 〉 → ( 𝑇 ‘ 𝑥 ) = ( 𝑇 ‘ 〈 ( 𝑆 ‘ 𝑘 ) , 𝑘 〉 ) ) |
65 |
|
df-ov |
⊢ ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) = ( 𝑇 ‘ 〈 ( 𝑆 ‘ 𝑘 ) , 𝑘 〉 ) |
66 |
64 65
|
eqtr4di |
⊢ ( 𝑥 = 〈 ( 𝑆 ‘ 𝑘 ) , 𝑘 〉 → ( 𝑇 ‘ 𝑥 ) = ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ) |
67 |
36 37
|
op2ndd |
⊢ ( 𝑥 = 〈 ( 𝑆 ‘ 𝑘 ) , 𝑘 〉 → ( 2nd ‘ 𝑥 ) = 𝑘 ) |
68 |
67
|
oveq1d |
⊢ ( 𝑥 = 〈 ( 𝑆 ‘ 𝑘 ) , 𝑘 〉 → ( ( 2nd ‘ 𝑥 ) + 1 ) = ( 𝑘 + 1 ) ) |
69 |
66 68
|
breq12d |
⊢ ( 𝑥 = 〈 ( 𝑆 ‘ 𝑘 ) , 𝑘 〉 → ( ( 𝑇 ‘ 𝑥 ) 𝐺 ( ( 2nd ‘ 𝑥 ) + 1 ) ↔ ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐺 ( 𝑘 + 1 ) ) ) |
70 |
|
fveq2 |
⊢ ( 𝑥 = 〈 ( 𝑆 ‘ 𝑘 ) , 𝑘 〉 → ( 𝐵 ‘ 𝑥 ) = ( 𝐵 ‘ 〈 ( 𝑆 ‘ 𝑘 ) , 𝑘 〉 ) ) |
71 |
|
df-ov |
⊢ ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) = ( 𝐵 ‘ 〈 ( 𝑆 ‘ 𝑘 ) , 𝑘 〉 ) |
72 |
70 71
|
eqtr4di |
⊢ ( 𝑥 = 〈 ( 𝑆 ‘ 𝑘 ) , 𝑘 〉 → ( 𝐵 ‘ 𝑥 ) = ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ) |
73 |
66 68
|
oveq12d |
⊢ ( 𝑥 = 〈 ( 𝑆 ‘ 𝑘 ) , 𝑘 〉 → ( ( 𝑇 ‘ 𝑥 ) 𝐵 ( ( 2nd ‘ 𝑥 ) + 1 ) ) = ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐵 ( 𝑘 + 1 ) ) ) |
74 |
72 73
|
ineq12d |
⊢ ( 𝑥 = 〈 ( 𝑆 ‘ 𝑘 ) , 𝑘 〉 → ( ( 𝐵 ‘ 𝑥 ) ∩ ( ( 𝑇 ‘ 𝑥 ) 𝐵 ( ( 2nd ‘ 𝑥 ) + 1 ) ) ) = ( ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ∩ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐵 ( 𝑘 + 1 ) ) ) ) |
75 |
74
|
eleq1d |
⊢ ( 𝑥 = 〈 ( 𝑆 ‘ 𝑘 ) , 𝑘 〉 → ( ( ( 𝐵 ‘ 𝑥 ) ∩ ( ( 𝑇 ‘ 𝑥 ) 𝐵 ( ( 2nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ↔ ( ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ∩ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐵 ( 𝑘 + 1 ) ) ) ∈ 𝐾 ) ) |
76 |
69 75
|
anbi12d |
⊢ ( 𝑥 = 〈 ( 𝑆 ‘ 𝑘 ) , 𝑘 〉 → ( ( ( 𝑇 ‘ 𝑥 ) 𝐺 ( ( 2nd ‘ 𝑥 ) + 1 ) ∧ ( ( 𝐵 ‘ 𝑥 ) ∩ ( ( 𝑇 ‘ 𝑥 ) 𝐵 ( ( 2nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ) ↔ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐺 ( 𝑘 + 1 ) ∧ ( ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ∩ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐵 ( 𝑘 + 1 ) ) ) ∈ 𝐾 ) ) ) |
77 |
76
|
rspccv |
⊢ ( ∀ 𝑥 ∈ 𝐺 ( ( 𝑇 ‘ 𝑥 ) 𝐺 ( ( 2nd ‘ 𝑥 ) + 1 ) ∧ ( ( 𝐵 ‘ 𝑥 ) ∩ ( ( 𝑇 ‘ 𝑥 ) 𝐵 ( ( 2nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ) → ( 〈 ( 𝑆 ‘ 𝑘 ) , 𝑘 〉 ∈ 𝐺 → ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐺 ( 𝑘 + 1 ) ∧ ( ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ∩ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐵 ( 𝑘 + 1 ) ) ) ∈ 𝐾 ) ) ) |
78 |
8 77
|
syl |
⊢ ( 𝜑 → ( 〈 ( 𝑆 ‘ 𝑘 ) , 𝑘 〉 ∈ 𝐺 → ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐺 ( 𝑘 + 1 ) ∧ ( ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ∩ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐵 ( 𝑘 + 1 ) ) ) ∈ 𝐾 ) ) ) |
79 |
63 78
|
syl5bi |
⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝑘 ) 𝐺 𝑘 → ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐺 ( 𝑘 + 1 ) ∧ ( ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ∩ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐵 ( 𝑘 + 1 ) ) ) ∈ 𝐾 ) ) ) |
80 |
79
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑆 ‘ 𝑘 ) 𝐺 𝑘 → ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐺 ( 𝑘 + 1 ) ∧ ( ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ∩ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐵 ( 𝑘 + 1 ) ) ) ∈ 𝐾 ) ) ) |
81 |
35 80
|
mpd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐺 ( 𝑘 + 1 ) ∧ ( ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ∩ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐵 ( 𝑘 + 1 ) ) ) ∈ 𝐾 ) ) |
82 |
81
|
simpld |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐺 ( 𝑘 + 1 ) ) |
83 |
|
ovex |
⊢ ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ∈ V |
84 |
1 2 3 83 28
|
heiborlem2 |
⊢ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐺 ( 𝑘 + 1 ) ↔ ( ( 𝑘 + 1 ) ∈ ℕ0 ∧ ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∧ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐵 ( 𝑘 + 1 ) ) ∈ 𝐾 ) ) |
85 |
84
|
simp2bi |
⊢ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐺 ( 𝑘 + 1 ) → ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) |
86 |
82 85
|
syl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) |
87 |
24 86
|
sseldd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ∈ 𝑋 ) |
88 |
21
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 + 1 ) ∈ ℕ0 ) |
89 |
|
oveq1 |
⊢ ( 𝑧 = ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) → ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) = ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) ) |
90 |
|
oveq2 |
⊢ ( 𝑚 = ( 𝑘 + 1 ) → ( 2 ↑ 𝑚 ) = ( 2 ↑ ( 𝑘 + 1 ) ) ) |
91 |
90
|
oveq2d |
⊢ ( 𝑚 = ( 𝑘 + 1 ) → ( 1 / ( 2 ↑ 𝑚 ) ) = ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) |
92 |
91
|
oveq2d |
⊢ ( 𝑚 = ( 𝑘 + 1 ) → ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) = ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ) |
93 |
|
ovex |
⊢ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ∈ V |
94 |
89 92 4 93
|
ovmpo |
⊢ ( ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ∈ 𝑋 ∧ ( 𝑘 + 1 ) ∈ ℕ0 ) → ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐵 ( 𝑘 + 1 ) ) = ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ) |
95 |
87 88 94
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐵 ( 𝑘 + 1 ) ) = ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ) |
96 |
62 95
|
ineq12d |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ∩ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐵 ( 𝑘 + 1 ) ) ) = ( ( ( 𝑆 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑘 ) ) ) ∩ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ) ) |
97 |
81
|
simprd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ∩ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐵 ( 𝑘 + 1 ) ) ) ∈ 𝐾 ) |
98 |
|
0elpw |
⊢ ∅ ∈ 𝒫 𝑈 |
99 |
|
0fin |
⊢ ∅ ∈ Fin |
100 |
|
elin |
⊢ ( ∅ ∈ ( 𝒫 𝑈 ∩ Fin ) ↔ ( ∅ ∈ 𝒫 𝑈 ∧ ∅ ∈ Fin ) ) |
101 |
98 99 100
|
mpbir2an |
⊢ ∅ ∈ ( 𝒫 𝑈 ∩ Fin ) |
102 |
|
0ss |
⊢ ∅ ⊆ ∪ ∅ |
103 |
|
unieq |
⊢ ( 𝑣 = ∅ → ∪ 𝑣 = ∪ ∅ ) |
104 |
103
|
sseq2d |
⊢ ( 𝑣 = ∅ → ( ∅ ⊆ ∪ 𝑣 ↔ ∅ ⊆ ∪ ∅ ) ) |
105 |
104
|
rspcev |
⊢ ( ( ∅ ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ∅ ⊆ ∪ ∅ ) → ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) ∅ ⊆ ∪ 𝑣 ) |
106 |
101 102 105
|
mp2an |
⊢ ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) ∅ ⊆ ∪ 𝑣 |
107 |
|
0ex |
⊢ ∅ ∈ V |
108 |
|
sseq1 |
⊢ ( 𝑢 = ∅ → ( 𝑢 ⊆ ∪ 𝑣 ↔ ∅ ⊆ ∪ 𝑣 ) ) |
109 |
108
|
rexbidv |
⊢ ( 𝑢 = ∅ → ( ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑢 ⊆ ∪ 𝑣 ↔ ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) ∅ ⊆ ∪ 𝑣 ) ) |
110 |
109
|
notbid |
⊢ ( 𝑢 = ∅ → ( ¬ ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑢 ⊆ ∪ 𝑣 ↔ ¬ ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) ∅ ⊆ ∪ 𝑣 ) ) |
111 |
107 110 2
|
elab2 |
⊢ ( ∅ ∈ 𝐾 ↔ ¬ ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) ∅ ⊆ ∪ 𝑣 ) |
112 |
111
|
con2bii |
⊢ ( ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) ∅ ⊆ ∪ 𝑣 ↔ ¬ ∅ ∈ 𝐾 ) |
113 |
106 112
|
mpbi |
⊢ ¬ ∅ ∈ 𝐾 |
114 |
|
nelne2 |
⊢ ( ( ( ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ∩ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐵 ( 𝑘 + 1 ) ) ) ∈ 𝐾 ∧ ¬ ∅ ∈ 𝐾 ) → ( ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ∩ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐵 ( 𝑘 + 1 ) ) ) ≠ ∅ ) |
115 |
97 113 114
|
sylancl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ∩ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐵 ( 𝑘 + 1 ) ) ) ≠ ∅ ) |
116 |
96 115
|
eqnetrrd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝑆 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑘 ) ) ) ∩ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ) ≠ ∅ ) |
117 |
52
|
rpreccld |
⊢ ( 𝑘 ∈ ℕ0 → ( 1 / ( 2 ↑ 𝑘 ) ) ∈ ℝ+ ) |
118 |
117
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 1 / ( 2 ↑ 𝑘 ) ) ∈ ℝ+ ) |
119 |
118
|
rpred |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 1 / ( 2 ↑ 𝑘 ) ) ∈ ℝ ) |
120 |
46
|
rpreccld |
⊢ ( 𝑘 ∈ ℕ0 → ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ∈ ℝ+ ) |
121 |
120
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ∈ ℝ+ ) |
122 |
121
|
rpred |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ∈ ℝ ) |
123 |
|
rexadd |
⊢ ( ( ( 1 / ( 2 ↑ 𝑘 ) ) ∈ ℝ ∧ ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ∈ ℝ ) → ( ( 1 / ( 2 ↑ 𝑘 ) ) +𝑒 ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) = ( ( 1 / ( 2 ↑ 𝑘 ) ) + ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ) |
124 |
119 122 123
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 1 / ( 2 ↑ 𝑘 ) ) +𝑒 ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) = ( ( 1 / ( 2 ↑ 𝑘 ) ) + ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ) |
125 |
124
|
breq1d |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 1 / ( 2 ↑ 𝑘 ) ) +𝑒 ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ≤ ( ( 𝑆 ‘ 𝑘 ) 𝐷 ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ) ↔ ( ( 1 / ( 2 ↑ 𝑘 ) ) + ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ≤ ( ( 𝑆 ‘ 𝑘 ) 𝐷 ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ) ) ) |
126 |
118
|
rpxrd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 1 / ( 2 ↑ 𝑘 ) ) ∈ ℝ* ) |
127 |
121
|
rpxrd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ∈ ℝ* ) |
128 |
|
bldisj |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑆 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ∈ 𝑋 ) ∧ ( ( 1 / ( 2 ↑ 𝑘 ) ) ∈ ℝ* ∧ ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ∈ ℝ* ∧ ( ( 1 / ( 2 ↑ 𝑘 ) ) +𝑒 ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ≤ ( ( 𝑆 ‘ 𝑘 ) 𝐷 ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ) ) ) → ( ( ( 𝑆 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑘 ) ) ) ∩ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ) = ∅ ) |
129 |
128
|
3exp2 |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑆 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ∈ 𝑋 ) → ( ( 1 / ( 2 ↑ 𝑘 ) ) ∈ ℝ* → ( ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ∈ ℝ* → ( ( ( 1 / ( 2 ↑ 𝑘 ) ) +𝑒 ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ≤ ( ( 𝑆 ‘ 𝑘 ) 𝐷 ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ) → ( ( ( 𝑆 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑘 ) ) ) ∩ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ) = ∅ ) ) ) ) |
130 |
129
|
imp32 |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑆 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ∈ 𝑋 ) ∧ ( ( 1 / ( 2 ↑ 𝑘 ) ) ∈ ℝ* ∧ ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ∈ ℝ* ) ) → ( ( ( 1 / ( 2 ↑ 𝑘 ) ) +𝑒 ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ≤ ( ( 𝑆 ‘ 𝑘 ) 𝐷 ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ) → ( ( ( 𝑆 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑘 ) ) ) ∩ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ) = ∅ ) ) |
131 |
17 41 87 126 127 130
|
syl32anc |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 1 / ( 2 ↑ 𝑘 ) ) +𝑒 ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ≤ ( ( 𝑆 ‘ 𝑘 ) 𝐷 ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ) → ( ( ( 𝑆 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑘 ) ) ) ∩ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ) = ∅ ) ) |
132 |
125 131
|
sylbird |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 1 / ( 2 ↑ 𝑘 ) ) + ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ≤ ( ( 𝑆 ‘ 𝑘 ) 𝐷 ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ) → ( ( ( 𝑆 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑘 ) ) ) ∩ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ) = ∅ ) ) |
133 |
132
|
necon3ad |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( ( 𝑆 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑘 ) ) ) ∩ ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ) ≠ ∅ → ¬ ( ( 1 / ( 2 ↑ 𝑘 ) ) + ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ≤ ( ( 𝑆 ‘ 𝑘 ) 𝐷 ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ) ) ) |
134 |
116 133
|
mpd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ¬ ( ( 1 / ( 2 ↑ 𝑘 ) ) + ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ≤ ( ( 𝑆 ‘ 𝑘 ) 𝐷 ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ) ) |
135 |
118 121
|
rpaddcld |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 1 / ( 2 ↑ 𝑘 ) ) + ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ∈ ℝ+ ) |
136 |
135
|
rpred |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 1 / ( 2 ↑ 𝑘 ) ) + ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ∈ ℝ ) |
137 |
14
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝐷 ∈ ( Met ‘ 𝑋 ) ) |
138 |
|
metcl |
⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝑆 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ∈ 𝑋 ) → ( ( 𝑆 ‘ 𝑘 ) 𝐷 ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ) ∈ ℝ ) |
139 |
137 41 87 138
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑆 ‘ 𝑘 ) 𝐷 ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ) ∈ ℝ ) |
140 |
136 139
|
letrid |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 1 / ( 2 ↑ 𝑘 ) ) + ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ≤ ( ( 𝑆 ‘ 𝑘 ) 𝐷 ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ) ∨ ( ( 𝑆 ‘ 𝑘 ) 𝐷 ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ) ≤ ( ( 1 / ( 2 ↑ 𝑘 ) ) + ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ) ) |
141 |
140
|
ord |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ¬ ( ( 1 / ( 2 ↑ 𝑘 ) ) + ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ≤ ( ( 𝑆 ‘ 𝑘 ) 𝐷 ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ) → ( ( 𝑆 ‘ 𝑘 ) 𝐷 ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ) ≤ ( ( 1 / ( 2 ↑ 𝑘 ) ) + ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ) ) |
142 |
134 141
|
mpd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑆 ‘ 𝑘 ) 𝐷 ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ) ≤ ( ( 1 / ( 2 ↑ 𝑘 ) ) + ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ) |
143 |
|
seqp1 |
⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 0 ) → ( seq 0 ( 𝑇 , ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) ) ‘ ( 𝑘 + 1 ) ) = ( ( seq 0 ( 𝑇 , ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) ) ‘ 𝑘 ) 𝑇 ( ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) ‘ ( 𝑘 + 1 ) ) ) ) |
144 |
|
nn0uz |
⊢ ℕ0 = ( ℤ≥ ‘ 0 ) |
145 |
143 144
|
eleq2s |
⊢ ( 𝑘 ∈ ℕ0 → ( seq 0 ( 𝑇 , ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) ) ‘ ( 𝑘 + 1 ) ) = ( ( seq 0 ( 𝑇 , ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) ) ‘ 𝑘 ) 𝑇 ( ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) ‘ ( 𝑘 + 1 ) ) ) ) |
146 |
10
|
fveq1i |
⊢ ( 𝑆 ‘ ( 𝑘 + 1 ) ) = ( seq 0 ( 𝑇 , ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) ) ‘ ( 𝑘 + 1 ) ) |
147 |
10
|
fveq1i |
⊢ ( 𝑆 ‘ 𝑘 ) = ( seq 0 ( 𝑇 , ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) ) ‘ 𝑘 ) |
148 |
147
|
oveq1i |
⊢ ( ( 𝑆 ‘ 𝑘 ) 𝑇 ( ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) ‘ ( 𝑘 + 1 ) ) ) = ( ( seq 0 ( 𝑇 , ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) ) ‘ 𝑘 ) 𝑇 ( ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) ‘ ( 𝑘 + 1 ) ) ) |
149 |
145 146 148
|
3eqtr4g |
⊢ ( 𝑘 ∈ ℕ0 → ( 𝑆 ‘ ( 𝑘 + 1 ) ) = ( ( 𝑆 ‘ 𝑘 ) 𝑇 ( ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) ‘ ( 𝑘 + 1 ) ) ) ) |
150 |
|
eqid |
⊢ ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) = ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) |
151 |
|
eqeq1 |
⊢ ( 𝑚 = ( 𝑘 + 1 ) → ( 𝑚 = 0 ↔ ( 𝑘 + 1 ) = 0 ) ) |
152 |
|
oveq1 |
⊢ ( 𝑚 = ( 𝑘 + 1 ) → ( 𝑚 − 1 ) = ( ( 𝑘 + 1 ) − 1 ) ) |
153 |
151 152
|
ifbieq2d |
⊢ ( 𝑚 = ( 𝑘 + 1 ) → if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) = if ( ( 𝑘 + 1 ) = 0 , 𝐶 , ( ( 𝑘 + 1 ) − 1 ) ) ) |
154 |
|
nn0p1nn |
⊢ ( 𝑘 ∈ ℕ0 → ( 𝑘 + 1 ) ∈ ℕ ) |
155 |
|
nnne0 |
⊢ ( ( 𝑘 + 1 ) ∈ ℕ → ( 𝑘 + 1 ) ≠ 0 ) |
156 |
155
|
neneqd |
⊢ ( ( 𝑘 + 1 ) ∈ ℕ → ¬ ( 𝑘 + 1 ) = 0 ) |
157 |
154 156
|
syl |
⊢ ( 𝑘 ∈ ℕ0 → ¬ ( 𝑘 + 1 ) = 0 ) |
158 |
157
|
iffalsed |
⊢ ( 𝑘 ∈ ℕ0 → if ( ( 𝑘 + 1 ) = 0 , 𝐶 , ( ( 𝑘 + 1 ) − 1 ) ) = ( ( 𝑘 + 1 ) − 1 ) ) |
159 |
|
ovex |
⊢ ( ( 𝑘 + 1 ) − 1 ) ∈ V |
160 |
158 159
|
eqeltrdi |
⊢ ( 𝑘 ∈ ℕ0 → if ( ( 𝑘 + 1 ) = 0 , 𝐶 , ( ( 𝑘 + 1 ) − 1 ) ) ∈ V ) |
161 |
150 153 21 160
|
fvmptd3 |
⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) ‘ ( 𝑘 + 1 ) ) = if ( ( 𝑘 + 1 ) = 0 , 𝐶 , ( ( 𝑘 + 1 ) − 1 ) ) ) |
162 |
|
nn0cn |
⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℂ ) |
163 |
|
ax-1cn |
⊢ 1 ∈ ℂ |
164 |
|
pncan |
⊢ ( ( 𝑘 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑘 + 1 ) − 1 ) = 𝑘 ) |
165 |
162 163 164
|
sylancl |
⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝑘 + 1 ) − 1 ) = 𝑘 ) |
166 |
161 158 165
|
3eqtrd |
⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) ‘ ( 𝑘 + 1 ) ) = 𝑘 ) |
167 |
166
|
oveq2d |
⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝑆 ‘ 𝑘 ) 𝑇 ( ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) ‘ ( 𝑘 + 1 ) ) ) = ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ) |
168 |
149 167
|
eqtrd |
⊢ ( 𝑘 ∈ ℕ0 → ( 𝑆 ‘ ( 𝑘 + 1 ) ) = ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ) |
169 |
168
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑆 ‘ ( 𝑘 + 1 ) ) = ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ) |
170 |
169
|
oveq1d |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑆 ‘ ( 𝑘 + 1 ) ) 𝐷 ( 𝑆 ‘ 𝑘 ) ) = ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐷 ( 𝑆 ‘ 𝑘 ) ) ) |
171 |
|
metsym |
⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ∈ 𝑋 ∧ ( 𝑆 ‘ 𝑘 ) ∈ 𝑋 ) → ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐷 ( 𝑆 ‘ 𝑘 ) ) = ( ( 𝑆 ‘ 𝑘 ) 𝐷 ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ) ) |
172 |
137 87 41 171
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) 𝐷 ( 𝑆 ‘ 𝑘 ) ) = ( ( 𝑆 ‘ 𝑘 ) 𝐷 ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ) ) |
173 |
170 172
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑆 ‘ ( 𝑘 + 1 ) ) 𝐷 ( 𝑆 ‘ 𝑘 ) ) = ( ( 𝑆 ‘ 𝑘 ) 𝐷 ( ( 𝑆 ‘ 𝑘 ) 𝑇 𝑘 ) ) ) |
174 |
|
3cn |
⊢ 3 ∈ ℂ |
175 |
174
|
2timesi |
⊢ ( 2 · 3 ) = ( 3 + 3 ) |
176 |
175
|
oveq1i |
⊢ ( ( 2 · 3 ) − 3 ) = ( ( 3 + 3 ) − 3 ) |
177 |
174 174
|
pncan3oi |
⊢ ( ( 3 + 3 ) − 3 ) = 3 |
178 |
|
df-3 |
⊢ 3 = ( 2 + 1 ) |
179 |
176 177 178
|
3eqtri |
⊢ ( ( 2 · 3 ) − 3 ) = ( 2 + 1 ) |
180 |
179
|
oveq1i |
⊢ ( ( ( 2 · 3 ) − 3 ) / ( 2 ↑ ( 𝑘 + 1 ) ) ) = ( ( 2 + 1 ) / ( 2 ↑ ( 𝑘 + 1 ) ) ) |
181 |
|
rpcn |
⊢ ( ( 2 ↑ ( 𝑘 + 1 ) ) ∈ ℝ+ → ( 2 ↑ ( 𝑘 + 1 ) ) ∈ ℂ ) |
182 |
|
rpne0 |
⊢ ( ( 2 ↑ ( 𝑘 + 1 ) ) ∈ ℝ+ → ( 2 ↑ ( 𝑘 + 1 ) ) ≠ 0 ) |
183 |
|
2cn |
⊢ 2 ∈ ℂ |
184 |
183 174
|
mulcli |
⊢ ( 2 · 3 ) ∈ ℂ |
185 |
|
divsubdir |
⊢ ( ( ( 2 · 3 ) ∈ ℂ ∧ 3 ∈ ℂ ∧ ( ( 2 ↑ ( 𝑘 + 1 ) ) ∈ ℂ ∧ ( 2 ↑ ( 𝑘 + 1 ) ) ≠ 0 ) ) → ( ( ( 2 · 3 ) − 3 ) / ( 2 ↑ ( 𝑘 + 1 ) ) ) = ( ( ( 2 · 3 ) / ( 2 ↑ ( 𝑘 + 1 ) ) ) − ( 3 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ) |
186 |
184 174 185
|
mp3an12 |
⊢ ( ( ( 2 ↑ ( 𝑘 + 1 ) ) ∈ ℂ ∧ ( 2 ↑ ( 𝑘 + 1 ) ) ≠ 0 ) → ( ( ( 2 · 3 ) − 3 ) / ( 2 ↑ ( 𝑘 + 1 ) ) ) = ( ( ( 2 · 3 ) / ( 2 ↑ ( 𝑘 + 1 ) ) ) − ( 3 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ) |
187 |
181 182 186
|
syl2anc |
⊢ ( ( 2 ↑ ( 𝑘 + 1 ) ) ∈ ℝ+ → ( ( ( 2 · 3 ) − 3 ) / ( 2 ↑ ( 𝑘 + 1 ) ) ) = ( ( ( 2 · 3 ) / ( 2 ↑ ( 𝑘 + 1 ) ) ) − ( 3 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ) |
188 |
46 187
|
syl |
⊢ ( 𝑘 ∈ ℕ0 → ( ( ( 2 · 3 ) − 3 ) / ( 2 ↑ ( 𝑘 + 1 ) ) ) = ( ( ( 2 · 3 ) / ( 2 ↑ ( 𝑘 + 1 ) ) ) − ( 3 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ) |
189 |
|
divdir |
⊢ ( ( 2 ∈ ℂ ∧ 1 ∈ ℂ ∧ ( ( 2 ↑ ( 𝑘 + 1 ) ) ∈ ℂ ∧ ( 2 ↑ ( 𝑘 + 1 ) ) ≠ 0 ) ) → ( ( 2 + 1 ) / ( 2 ↑ ( 𝑘 + 1 ) ) ) = ( ( 2 / ( 2 ↑ ( 𝑘 + 1 ) ) ) + ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ) |
190 |
183 163 189
|
mp3an12 |
⊢ ( ( ( 2 ↑ ( 𝑘 + 1 ) ) ∈ ℂ ∧ ( 2 ↑ ( 𝑘 + 1 ) ) ≠ 0 ) → ( ( 2 + 1 ) / ( 2 ↑ ( 𝑘 + 1 ) ) ) = ( ( 2 / ( 2 ↑ ( 𝑘 + 1 ) ) ) + ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ) |
191 |
181 182 190
|
syl2anc |
⊢ ( ( 2 ↑ ( 𝑘 + 1 ) ) ∈ ℝ+ → ( ( 2 + 1 ) / ( 2 ↑ ( 𝑘 + 1 ) ) ) = ( ( 2 / ( 2 ↑ ( 𝑘 + 1 ) ) ) + ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ) |
192 |
46 191
|
syl |
⊢ ( 𝑘 ∈ ℕ0 → ( ( 2 + 1 ) / ( 2 ↑ ( 𝑘 + 1 ) ) ) = ( ( 2 / ( 2 ↑ ( 𝑘 + 1 ) ) ) + ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ) |
193 |
180 188 192
|
3eqtr3a |
⊢ ( 𝑘 ∈ ℕ0 → ( ( ( 2 · 3 ) / ( 2 ↑ ( 𝑘 + 1 ) ) ) − ( 3 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) = ( ( 2 / ( 2 ↑ ( 𝑘 + 1 ) ) ) + ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ) |
194 |
|
rpcn |
⊢ ( ( 2 ↑ 𝑘 ) ∈ ℝ+ → ( 2 ↑ 𝑘 ) ∈ ℂ ) |
195 |
|
rpne0 |
⊢ ( ( 2 ↑ 𝑘 ) ∈ ℝ+ → ( 2 ↑ 𝑘 ) ≠ 0 ) |
196 |
|
2cnne0 |
⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) |
197 |
|
divcan5 |
⊢ ( ( 3 ∈ ℂ ∧ ( ( 2 ↑ 𝑘 ) ∈ ℂ ∧ ( 2 ↑ 𝑘 ) ≠ 0 ) ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( 2 · 3 ) / ( 2 · ( 2 ↑ 𝑘 ) ) ) = ( 3 / ( 2 ↑ 𝑘 ) ) ) |
198 |
174 196 197
|
mp3an13 |
⊢ ( ( ( 2 ↑ 𝑘 ) ∈ ℂ ∧ ( 2 ↑ 𝑘 ) ≠ 0 ) → ( ( 2 · 3 ) / ( 2 · ( 2 ↑ 𝑘 ) ) ) = ( 3 / ( 2 ↑ 𝑘 ) ) ) |
199 |
194 195 198
|
syl2anc |
⊢ ( ( 2 ↑ 𝑘 ) ∈ ℝ+ → ( ( 2 · 3 ) / ( 2 · ( 2 ↑ 𝑘 ) ) ) = ( 3 / ( 2 ↑ 𝑘 ) ) ) |
200 |
52 199
|
syl |
⊢ ( 𝑘 ∈ ℕ0 → ( ( 2 · 3 ) / ( 2 · ( 2 ↑ 𝑘 ) ) ) = ( 3 / ( 2 ↑ 𝑘 ) ) ) |
201 |
52 194
|
syl |
⊢ ( 𝑘 ∈ ℕ0 → ( 2 ↑ 𝑘 ) ∈ ℂ ) |
202 |
|
mulcom |
⊢ ( ( 2 ∈ ℂ ∧ ( 2 ↑ 𝑘 ) ∈ ℂ ) → ( 2 · ( 2 ↑ 𝑘 ) ) = ( ( 2 ↑ 𝑘 ) · 2 ) ) |
203 |
183 201 202
|
sylancr |
⊢ ( 𝑘 ∈ ℕ0 → ( 2 · ( 2 ↑ 𝑘 ) ) = ( ( 2 ↑ 𝑘 ) · 2 ) ) |
204 |
|
expp1 |
⊢ ( ( 2 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 2 ↑ ( 𝑘 + 1 ) ) = ( ( 2 ↑ 𝑘 ) · 2 ) ) |
205 |
183 204
|
mpan |
⊢ ( 𝑘 ∈ ℕ0 → ( 2 ↑ ( 𝑘 + 1 ) ) = ( ( 2 ↑ 𝑘 ) · 2 ) ) |
206 |
203 205
|
eqtr4d |
⊢ ( 𝑘 ∈ ℕ0 → ( 2 · ( 2 ↑ 𝑘 ) ) = ( 2 ↑ ( 𝑘 + 1 ) ) ) |
207 |
206
|
oveq2d |
⊢ ( 𝑘 ∈ ℕ0 → ( ( 2 · 3 ) / ( 2 · ( 2 ↑ 𝑘 ) ) ) = ( ( 2 · 3 ) / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) |
208 |
200 207
|
eqtr3d |
⊢ ( 𝑘 ∈ ℕ0 → ( 3 / ( 2 ↑ 𝑘 ) ) = ( ( 2 · 3 ) / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) |
209 |
208
|
oveq1d |
⊢ ( 𝑘 ∈ ℕ0 → ( ( 3 / ( 2 ↑ 𝑘 ) ) − ( 3 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) = ( ( ( 2 · 3 ) / ( 2 ↑ ( 𝑘 + 1 ) ) ) − ( 3 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ) |
210 |
|
divcan5 |
⊢ ( ( 1 ∈ ℂ ∧ ( ( 2 ↑ 𝑘 ) ∈ ℂ ∧ ( 2 ↑ 𝑘 ) ≠ 0 ) ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( 2 · 1 ) / ( 2 · ( 2 ↑ 𝑘 ) ) ) = ( 1 / ( 2 ↑ 𝑘 ) ) ) |
211 |
163 196 210
|
mp3an13 |
⊢ ( ( ( 2 ↑ 𝑘 ) ∈ ℂ ∧ ( 2 ↑ 𝑘 ) ≠ 0 ) → ( ( 2 · 1 ) / ( 2 · ( 2 ↑ 𝑘 ) ) ) = ( 1 / ( 2 ↑ 𝑘 ) ) ) |
212 |
194 195 211
|
syl2anc |
⊢ ( ( 2 ↑ 𝑘 ) ∈ ℝ+ → ( ( 2 · 1 ) / ( 2 · ( 2 ↑ 𝑘 ) ) ) = ( 1 / ( 2 ↑ 𝑘 ) ) ) |
213 |
52 212
|
syl |
⊢ ( 𝑘 ∈ ℕ0 → ( ( 2 · 1 ) / ( 2 · ( 2 ↑ 𝑘 ) ) ) = ( 1 / ( 2 ↑ 𝑘 ) ) ) |
214 |
|
2t1e2 |
⊢ ( 2 · 1 ) = 2 |
215 |
214
|
a1i |
⊢ ( 𝑘 ∈ ℕ0 → ( 2 · 1 ) = 2 ) |
216 |
215 206
|
oveq12d |
⊢ ( 𝑘 ∈ ℕ0 → ( ( 2 · 1 ) / ( 2 · ( 2 ↑ 𝑘 ) ) ) = ( 2 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) |
217 |
213 216
|
eqtr3d |
⊢ ( 𝑘 ∈ ℕ0 → ( 1 / ( 2 ↑ 𝑘 ) ) = ( 2 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) |
218 |
217
|
oveq1d |
⊢ ( 𝑘 ∈ ℕ0 → ( ( 1 / ( 2 ↑ 𝑘 ) ) + ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) = ( ( 2 / ( 2 ↑ ( 𝑘 + 1 ) ) ) + ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ) |
219 |
193 209 218
|
3eqtr4d |
⊢ ( 𝑘 ∈ ℕ0 → ( ( 3 / ( 2 ↑ 𝑘 ) ) − ( 3 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) = ( ( 1 / ( 2 ↑ 𝑘 ) ) + ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ) |
220 |
219
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 3 / ( 2 ↑ 𝑘 ) ) − ( 3 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) = ( ( 1 / ( 2 ↑ 𝑘 ) ) + ( 1 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ) |
221 |
142 173 220
|
3brtr4d |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑆 ‘ ( 𝑘 + 1 ) ) 𝐷 ( 𝑆 ‘ 𝑘 ) ) ≤ ( ( 3 / ( 2 ↑ 𝑘 ) ) − ( 3 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ) |
222 |
|
blss2 |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑆 ‘ ( 𝑘 + 1 ) ) ∈ 𝑋 ∧ ( 𝑆 ‘ 𝑘 ) ∈ 𝑋 ) ∧ ( ( 3 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ∈ ℝ ∧ ( 3 / ( 2 ↑ 𝑘 ) ) ∈ ℝ ∧ ( ( 𝑆 ‘ ( 𝑘 + 1 ) ) 𝐷 ( 𝑆 ‘ 𝑘 ) ) ≤ ( ( 3 / ( 2 ↑ 𝑘 ) ) − ( 3 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ) ) → ( ( 𝑆 ‘ ( 𝑘 + 1 ) ) ( ball ‘ 𝐷 ) ( 3 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ⊆ ( ( 𝑆 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 3 / ( 2 ↑ 𝑘 ) ) ) ) |
223 |
17 32 41 49 55 221 222
|
syl33anc |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑆 ‘ ( 𝑘 + 1 ) ) ( ball ‘ 𝐷 ) ( 3 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ⊆ ( ( 𝑆 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 3 / ( 2 ↑ 𝑘 ) ) ) ) |
224 |
12 223
|
sylan2 |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑆 ‘ ( 𝑘 + 1 ) ) ( ball ‘ 𝐷 ) ( 3 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ⊆ ( ( 𝑆 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 3 / ( 2 ↑ 𝑘 ) ) ) ) |
225 |
|
peano2nn |
⊢ ( 𝑘 ∈ ℕ → ( 𝑘 + 1 ) ∈ ℕ ) |
226 |
|
fveq2 |
⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( 𝑆 ‘ 𝑛 ) = ( 𝑆 ‘ ( 𝑘 + 1 ) ) ) |
227 |
|
oveq2 |
⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( 2 ↑ 𝑛 ) = ( 2 ↑ ( 𝑘 + 1 ) ) ) |
228 |
227
|
oveq2d |
⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( 3 / ( 2 ↑ 𝑛 ) ) = ( 3 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) |
229 |
226 228
|
opeq12d |
⊢ ( 𝑛 = ( 𝑘 + 1 ) → 〈 ( 𝑆 ‘ 𝑛 ) , ( 3 / ( 2 ↑ 𝑛 ) ) 〉 = 〈 ( 𝑆 ‘ ( 𝑘 + 1 ) ) , ( 3 / ( 2 ↑ ( 𝑘 + 1 ) ) ) 〉 ) |
230 |
|
opex |
⊢ 〈 ( 𝑆 ‘ ( 𝑘 + 1 ) ) , ( 3 / ( 2 ↑ ( 𝑘 + 1 ) ) ) 〉 ∈ V |
231 |
229 11 230
|
fvmpt |
⊢ ( ( 𝑘 + 1 ) ∈ ℕ → ( 𝑀 ‘ ( 𝑘 + 1 ) ) = 〈 ( 𝑆 ‘ ( 𝑘 + 1 ) ) , ( 3 / ( 2 ↑ ( 𝑘 + 1 ) ) ) 〉 ) |
232 |
225 231
|
syl |
⊢ ( 𝑘 ∈ ℕ → ( 𝑀 ‘ ( 𝑘 + 1 ) ) = 〈 ( 𝑆 ‘ ( 𝑘 + 1 ) ) , ( 3 / ( 2 ↑ ( 𝑘 + 1 ) ) ) 〉 ) |
233 |
232
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑀 ‘ ( 𝑘 + 1 ) ) = 〈 ( 𝑆 ‘ ( 𝑘 + 1 ) ) , ( 3 / ( 2 ↑ ( 𝑘 + 1 ) ) ) 〉 ) |
234 |
233
|
fveq2d |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝑀 ‘ ( 𝑘 + 1 ) ) ) = ( ( ball ‘ 𝐷 ) ‘ 〈 ( 𝑆 ‘ ( 𝑘 + 1 ) ) , ( 3 / ( 2 ↑ ( 𝑘 + 1 ) ) ) 〉 ) ) |
235 |
|
df-ov |
⊢ ( ( 𝑆 ‘ ( 𝑘 + 1 ) ) ( ball ‘ 𝐷 ) ( 3 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) = ( ( ball ‘ 𝐷 ) ‘ 〈 ( 𝑆 ‘ ( 𝑘 + 1 ) ) , ( 3 / ( 2 ↑ ( 𝑘 + 1 ) ) ) 〉 ) |
236 |
234 235
|
eqtr4di |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝑀 ‘ ( 𝑘 + 1 ) ) ) = ( ( 𝑆 ‘ ( 𝑘 + 1 ) ) ( ball ‘ 𝐷 ) ( 3 / ( 2 ↑ ( 𝑘 + 1 ) ) ) ) ) |
237 |
|
fveq2 |
⊢ ( 𝑛 = 𝑘 → ( 𝑆 ‘ 𝑛 ) = ( 𝑆 ‘ 𝑘 ) ) |
238 |
|
oveq2 |
⊢ ( 𝑛 = 𝑘 → ( 2 ↑ 𝑛 ) = ( 2 ↑ 𝑘 ) ) |
239 |
238
|
oveq2d |
⊢ ( 𝑛 = 𝑘 → ( 3 / ( 2 ↑ 𝑛 ) ) = ( 3 / ( 2 ↑ 𝑘 ) ) ) |
240 |
237 239
|
opeq12d |
⊢ ( 𝑛 = 𝑘 → 〈 ( 𝑆 ‘ 𝑛 ) , ( 3 / ( 2 ↑ 𝑛 ) ) 〉 = 〈 ( 𝑆 ‘ 𝑘 ) , ( 3 / ( 2 ↑ 𝑘 ) ) 〉 ) |
241 |
|
opex |
⊢ 〈 ( 𝑆 ‘ 𝑘 ) , ( 3 / ( 2 ↑ 𝑘 ) ) 〉 ∈ V |
242 |
240 11 241
|
fvmpt |
⊢ ( 𝑘 ∈ ℕ → ( 𝑀 ‘ 𝑘 ) = 〈 ( 𝑆 ‘ 𝑘 ) , ( 3 / ( 2 ↑ 𝑘 ) ) 〉 ) |
243 |
242
|
fveq2d |
⊢ ( 𝑘 ∈ ℕ → ( ( ball ‘ 𝐷 ) ‘ ( 𝑀 ‘ 𝑘 ) ) = ( ( ball ‘ 𝐷 ) ‘ 〈 ( 𝑆 ‘ 𝑘 ) , ( 3 / ( 2 ↑ 𝑘 ) ) 〉 ) ) |
244 |
|
df-ov |
⊢ ( ( 𝑆 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 3 / ( 2 ↑ 𝑘 ) ) ) = ( ( ball ‘ 𝐷 ) ‘ 〈 ( 𝑆 ‘ 𝑘 ) , ( 3 / ( 2 ↑ 𝑘 ) ) 〉 ) |
245 |
243 244
|
eqtr4di |
⊢ ( 𝑘 ∈ ℕ → ( ( ball ‘ 𝐷 ) ‘ ( 𝑀 ‘ 𝑘 ) ) = ( ( 𝑆 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 3 / ( 2 ↑ 𝑘 ) ) ) ) |
246 |
245
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝑀 ‘ 𝑘 ) ) = ( ( 𝑆 ‘ 𝑘 ) ( ball ‘ 𝐷 ) ( 3 / ( 2 ↑ 𝑘 ) ) ) ) |
247 |
224 236 246
|
3sstr4d |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝑀 ‘ ( 𝑘 + 1 ) ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝑀 ‘ 𝑘 ) ) ) |
248 |
247
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ ( ( ball ‘ 𝐷 ) ‘ ( 𝑀 ‘ ( 𝑘 + 1 ) ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝑀 ‘ 𝑘 ) ) ) |