Step |
Hyp |
Ref |
Expression |
0 |
|
ccauold |
⊢ Cauchy |
1 |
|
vf |
⊢ 𝑓 |
2 |
|
chba |
⊢ ℋ |
3 |
|
cmap |
⊢ ↑m |
4 |
|
cn |
⊢ ℕ |
5 |
2 4 3
|
co |
⊢ ( ℋ ↑m ℕ ) |
6 |
|
vx |
⊢ 𝑥 |
7 |
|
crp |
⊢ ℝ+ |
8 |
|
vy |
⊢ 𝑦 |
9 |
|
vz |
⊢ 𝑧 |
10 |
|
cuz |
⊢ ℤ≥ |
11 |
8
|
cv |
⊢ 𝑦 |
12 |
11 10
|
cfv |
⊢ ( ℤ≥ ‘ 𝑦 ) |
13 |
|
cno |
⊢ normℎ |
14 |
1
|
cv |
⊢ 𝑓 |
15 |
11 14
|
cfv |
⊢ ( 𝑓 ‘ 𝑦 ) |
16 |
|
cmv |
⊢ −ℎ |
17 |
9
|
cv |
⊢ 𝑧 |
18 |
17 14
|
cfv |
⊢ ( 𝑓 ‘ 𝑧 ) |
19 |
15 18 16
|
co |
⊢ ( ( 𝑓 ‘ 𝑦 ) −ℎ ( 𝑓 ‘ 𝑧 ) ) |
20 |
19 13
|
cfv |
⊢ ( normℎ ‘ ( ( 𝑓 ‘ 𝑦 ) −ℎ ( 𝑓 ‘ 𝑧 ) ) ) |
21 |
|
clt |
⊢ < |
22 |
6
|
cv |
⊢ 𝑥 |
23 |
20 22 21
|
wbr |
⊢ ( normℎ ‘ ( ( 𝑓 ‘ 𝑦 ) −ℎ ( 𝑓 ‘ 𝑧 ) ) ) < 𝑥 |
24 |
23 9 12
|
wral |
⊢ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝑓 ‘ 𝑦 ) −ℎ ( 𝑓 ‘ 𝑧 ) ) ) < 𝑥 |
25 |
24 8 4
|
wrex |
⊢ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝑓 ‘ 𝑦 ) −ℎ ( 𝑓 ‘ 𝑧 ) ) ) < 𝑥 |
26 |
25 6 7
|
wral |
⊢ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝑓 ‘ 𝑦 ) −ℎ ( 𝑓 ‘ 𝑧 ) ) ) < 𝑥 |
27 |
26 1 5
|
crab |
⊢ { 𝑓 ∈ ( ℋ ↑m ℕ ) ∣ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝑓 ‘ 𝑦 ) −ℎ ( 𝑓 ‘ 𝑧 ) ) ) < 𝑥 } |
28 |
0 27
|
wceq |
⊢ Cauchy = { 𝑓 ∈ ( ℋ ↑m ℕ ) ∣ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝑓 ‘ 𝑦 ) −ℎ ( 𝑓 ‘ 𝑧 ) ) ) < 𝑥 } |