Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Asger C. Ipsen
Continuous nowhere differentiable functions
cnndvlem2
Next ⟩
cnndv
Metamath Proof Explorer
Ascii
Unicode
Theorem
cnndvlem2
Description:
Lemma for
cnndv
.
(Contributed by
Asger C. Ipsen
, 26-Aug-2021)
Ref
Expression
Hypotheses
cnndvlem2.t
⊢
T
=
x
∈
ℝ
⟼
x
+
1
2
−
x
cnndvlem2.f
⊢
F
=
y
∈
ℝ
⟼
n
∈
ℕ
0
⟼
1
2
n
⁢
T
⁡
2
⋅
3
n
⁢
y
cnndvlem2.w
⊢
W
=
w
∈
ℝ
⟼
∑
i
∈
ℕ
0
F
⁡
w
⁡
i
Assertion
cnndvlem2
⊢
∃
f
f
:
ℝ
⟶
cn
ℝ
∧
dom
⁡
f
ℝ
′
=
∅
Proof
Step
Hyp
Ref
Expression
1
cnndvlem2.t
⊢
T
=
x
∈
ℝ
⟼
x
+
1
2
−
x
2
cnndvlem2.f
⊢
F
=
y
∈
ℝ
⟼
n
∈
ℕ
0
⟼
1
2
n
⁢
T
⁡
2
⋅
3
n
⁢
y
3
cnndvlem2.w
⊢
W
=
w
∈
ℝ
⟼
∑
i
∈
ℕ
0
F
⁡
w
⁡
i
4
1
2
3
cnndvlem1
⊢
W
:
ℝ
⟶
cn
ℝ
∧
dom
⁡
W
ℝ
′
=
∅
5
reex
⊢
ℝ
∈
V
6
5
mptex
⊢
w
∈
ℝ
⟼
∑
i
∈
ℕ
0
F
⁡
w
⁡
i
∈
V
7
3
6
eqeltri
⊢
W
∈
V
8
eleq1
⊢
f
=
W
→
f
:
ℝ
⟶
cn
ℝ
↔
W
:
ℝ
⟶
cn
ℝ
9
oveq2
⊢
f
=
W
→
ℝ
D
f
=
ℝ
D
W
10
9
dmeqd
⊢
f
=
W
→
dom
⁡
f
ℝ
′
=
dom
⁡
W
ℝ
′
11
10
eqeq1d
⊢
f
=
W
→
dom
⁡
f
ℝ
′
=
∅
↔
dom
⁡
W
ℝ
′
=
∅
12
8
11
anbi12d
⊢
f
=
W
→
f
:
ℝ
⟶
cn
ℝ
∧
dom
⁡
f
ℝ
′
=
∅
↔
W
:
ℝ
⟶
cn
ℝ
∧
dom
⁡
W
ℝ
′
=
∅
13
7
12
spcev
⊢
W
:
ℝ
⟶
cn
ℝ
∧
dom
⁡
W
ℝ
′
=
∅
→
∃
f
f
:
ℝ
⟶
cn
ℝ
∧
dom
⁡
f
ℝ
′
=
∅
14
4
13
ax-mp
⊢
∃
f
f
:
ℝ
⟶
cn
ℝ
∧
dom
⁡
f
ℝ
′
=
∅