Step |
Hyp |
Ref |
Expression |
1 |
|
c1lip2.a |
⊢ ( 𝜑 → 𝐴 ∈ ℝ ) |
2 |
|
c1lip2.b |
⊢ ( 𝜑 → 𝐵 ∈ ℝ ) |
3 |
|
c1lip2.f |
⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝓑C𝑛 ‘ ℝ ) ‘ 1 ) ) |
4 |
|
c1lip2.rn |
⊢ ( 𝜑 → ran 𝐹 ⊆ ℝ ) |
5 |
|
c1lip2.dm |
⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ dom 𝐹 ) |
6 |
|
ax-resscn |
⊢ ℝ ⊆ ℂ |
7 |
|
1nn0 |
⊢ 1 ∈ ℕ0 |
8 |
|
elcpn |
⊢ ( ( ℝ ⊆ ℂ ∧ 1 ∈ ℕ0 ) → ( 𝐹 ∈ ( ( 𝓑C𝑛 ‘ ℝ ) ‘ 1 ) ↔ ( 𝐹 ∈ ( ℂ ↑pm ℝ ) ∧ ( ( ℝ D𝑛 𝐹 ) ‘ 1 ) ∈ ( dom 𝐹 –cn→ ℂ ) ) ) ) |
9 |
6 7 8
|
mp2an |
⊢ ( 𝐹 ∈ ( ( 𝓑C𝑛 ‘ ℝ ) ‘ 1 ) ↔ ( 𝐹 ∈ ( ℂ ↑pm ℝ ) ∧ ( ( ℝ D𝑛 𝐹 ) ‘ 1 ) ∈ ( dom 𝐹 –cn→ ℂ ) ) ) |
10 |
9
|
simplbi |
⊢ ( 𝐹 ∈ ( ( 𝓑C𝑛 ‘ ℝ ) ‘ 1 ) → 𝐹 ∈ ( ℂ ↑pm ℝ ) ) |
11 |
3 10
|
syl |
⊢ ( 𝜑 → 𝐹 ∈ ( ℂ ↑pm ℝ ) ) |
12 |
|
pmfun |
⊢ ( 𝐹 ∈ ( ℂ ↑pm ℝ ) → Fun 𝐹 ) |
13 |
11 12
|
syl |
⊢ ( 𝜑 → Fun 𝐹 ) |
14 |
13
|
funfnd |
⊢ ( 𝜑 → 𝐹 Fn dom 𝐹 ) |
15 |
|
df-f |
⊢ ( 𝐹 : dom 𝐹 ⟶ ℝ ↔ ( 𝐹 Fn dom 𝐹 ∧ ran 𝐹 ⊆ ℝ ) ) |
16 |
14 4 15
|
sylanbrc |
⊢ ( 𝜑 → 𝐹 : dom 𝐹 ⟶ ℝ ) |
17 |
|
cnex |
⊢ ℂ ∈ V |
18 |
|
reex |
⊢ ℝ ∈ V |
19 |
17 18
|
elpm2 |
⊢ ( 𝐹 ∈ ( ℂ ↑pm ℝ ) ↔ ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ ℝ ) ) |
20 |
19
|
simprbi |
⊢ ( 𝐹 ∈ ( ℂ ↑pm ℝ ) → dom 𝐹 ⊆ ℝ ) |
21 |
11 20
|
syl |
⊢ ( 𝜑 → dom 𝐹 ⊆ ℝ ) |
22 |
|
dvfre |
⊢ ( ( 𝐹 : dom 𝐹 ⟶ ℝ ∧ dom 𝐹 ⊆ ℝ ) → ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℝ ) |
23 |
16 21 22
|
syl2anc |
⊢ ( 𝜑 → ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℝ ) |
24 |
|
0p1e1 |
⊢ ( 0 + 1 ) = 1 |
25 |
24
|
fveq2i |
⊢ ( ( ℝ D𝑛 𝐹 ) ‘ ( 0 + 1 ) ) = ( ( ℝ D𝑛 𝐹 ) ‘ 1 ) |
26 |
|
0nn0 |
⊢ 0 ∈ ℕ0 |
27 |
|
dvnp1 |
⊢ ( ( ℝ ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm ℝ ) ∧ 0 ∈ ℕ0 ) → ( ( ℝ D𝑛 𝐹 ) ‘ ( 0 + 1 ) ) = ( ℝ D ( ( ℝ D𝑛 𝐹 ) ‘ 0 ) ) ) |
28 |
6 26 27
|
mp3an13 |
⊢ ( 𝐹 ∈ ( ℂ ↑pm ℝ ) → ( ( ℝ D𝑛 𝐹 ) ‘ ( 0 + 1 ) ) = ( ℝ D ( ( ℝ D𝑛 𝐹 ) ‘ 0 ) ) ) |
29 |
11 28
|
syl |
⊢ ( 𝜑 → ( ( ℝ D𝑛 𝐹 ) ‘ ( 0 + 1 ) ) = ( ℝ D ( ( ℝ D𝑛 𝐹 ) ‘ 0 ) ) ) |
30 |
25 29
|
syl5eqr |
⊢ ( 𝜑 → ( ( ℝ D𝑛 𝐹 ) ‘ 1 ) = ( ℝ D ( ( ℝ D𝑛 𝐹 ) ‘ 0 ) ) ) |
31 |
|
dvn0 |
⊢ ( ( ℝ ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm ℝ ) ) → ( ( ℝ D𝑛 𝐹 ) ‘ 0 ) = 𝐹 ) |
32 |
6 11 31
|
sylancr |
⊢ ( 𝜑 → ( ( ℝ D𝑛 𝐹 ) ‘ 0 ) = 𝐹 ) |
33 |
32
|
oveq2d |
⊢ ( 𝜑 → ( ℝ D ( ( ℝ D𝑛 𝐹 ) ‘ 0 ) ) = ( ℝ D 𝐹 ) ) |
34 |
30 33
|
eqtrd |
⊢ ( 𝜑 → ( ( ℝ D𝑛 𝐹 ) ‘ 1 ) = ( ℝ D 𝐹 ) ) |
35 |
9
|
simprbi |
⊢ ( 𝐹 ∈ ( ( 𝓑C𝑛 ‘ ℝ ) ‘ 1 ) → ( ( ℝ D𝑛 𝐹 ) ‘ 1 ) ∈ ( dom 𝐹 –cn→ ℂ ) ) |
36 |
3 35
|
syl |
⊢ ( 𝜑 → ( ( ℝ D𝑛 𝐹 ) ‘ 1 ) ∈ ( dom 𝐹 –cn→ ℂ ) ) |
37 |
34 36
|
eqeltrrd |
⊢ ( 𝜑 → ( ℝ D 𝐹 ) ∈ ( dom 𝐹 –cn→ ℂ ) ) |
38 |
|
cncff |
⊢ ( ( ℝ D 𝐹 ) ∈ ( dom 𝐹 –cn→ ℂ ) → ( ℝ D 𝐹 ) : dom 𝐹 ⟶ ℂ ) |
39 |
|
fdm |
⊢ ( ( ℝ D 𝐹 ) : dom 𝐹 ⟶ ℂ → dom ( ℝ D 𝐹 ) = dom 𝐹 ) |
40 |
37 38 39
|
3syl |
⊢ ( 𝜑 → dom ( ℝ D 𝐹 ) = dom 𝐹 ) |
41 |
40
|
feq2d |
⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℝ ↔ ( ℝ D 𝐹 ) : dom 𝐹 ⟶ ℝ ) ) |
42 |
23 41
|
mpbid |
⊢ ( 𝜑 → ( ℝ D 𝐹 ) : dom 𝐹 ⟶ ℝ ) |
43 |
|
cncffvrn |
⊢ ( ( ℝ ⊆ ℂ ∧ ( ℝ D 𝐹 ) ∈ ( dom 𝐹 –cn→ ℂ ) ) → ( ( ℝ D 𝐹 ) ∈ ( dom 𝐹 –cn→ ℝ ) ↔ ( ℝ D 𝐹 ) : dom 𝐹 ⟶ ℝ ) ) |
44 |
6 37 43
|
sylancr |
⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ∈ ( dom 𝐹 –cn→ ℝ ) ↔ ( ℝ D 𝐹 ) : dom 𝐹 ⟶ ℝ ) ) |
45 |
42 44
|
mpbird |
⊢ ( 𝜑 → ( ℝ D 𝐹 ) ∈ ( dom 𝐹 –cn→ ℝ ) ) |
46 |
|
rescncf |
⊢ ( ( 𝐴 [,] 𝐵 ) ⊆ dom 𝐹 → ( ( ℝ D 𝐹 ) ∈ ( dom 𝐹 –cn→ ℝ ) → ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) ) ) |
47 |
5 45 46
|
sylc |
⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) ) |
48 |
18
|
prid1 |
⊢ ℝ ∈ { ℝ , ℂ } |
49 |
|
1eluzge0 |
⊢ 1 ∈ ( ℤ≥ ‘ 0 ) |
50 |
|
cpnord |
⊢ ( ( ℝ ∈ { ℝ , ℂ } ∧ 0 ∈ ℕ0 ∧ 1 ∈ ( ℤ≥ ‘ 0 ) ) → ( ( 𝓑C𝑛 ‘ ℝ ) ‘ 1 ) ⊆ ( ( 𝓑C𝑛 ‘ ℝ ) ‘ 0 ) ) |
51 |
48 26 49 50
|
mp3an |
⊢ ( ( 𝓑C𝑛 ‘ ℝ ) ‘ 1 ) ⊆ ( ( 𝓑C𝑛 ‘ ℝ ) ‘ 0 ) |
52 |
51 3
|
sseldi |
⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝓑C𝑛 ‘ ℝ ) ‘ 0 ) ) |
53 |
|
elcpn |
⊢ ( ( ℝ ⊆ ℂ ∧ 0 ∈ ℕ0 ) → ( 𝐹 ∈ ( ( 𝓑C𝑛 ‘ ℝ ) ‘ 0 ) ↔ ( 𝐹 ∈ ( ℂ ↑pm ℝ ) ∧ ( ( ℝ D𝑛 𝐹 ) ‘ 0 ) ∈ ( dom 𝐹 –cn→ ℂ ) ) ) ) |
54 |
6 26 53
|
mp2an |
⊢ ( 𝐹 ∈ ( ( 𝓑C𝑛 ‘ ℝ ) ‘ 0 ) ↔ ( 𝐹 ∈ ( ℂ ↑pm ℝ ) ∧ ( ( ℝ D𝑛 𝐹 ) ‘ 0 ) ∈ ( dom 𝐹 –cn→ ℂ ) ) ) |
55 |
54
|
simprbi |
⊢ ( 𝐹 ∈ ( ( 𝓑C𝑛 ‘ ℝ ) ‘ 0 ) → ( ( ℝ D𝑛 𝐹 ) ‘ 0 ) ∈ ( dom 𝐹 –cn→ ℂ ) ) |
56 |
52 55
|
syl |
⊢ ( 𝜑 → ( ( ℝ D𝑛 𝐹 ) ‘ 0 ) ∈ ( dom 𝐹 –cn→ ℂ ) ) |
57 |
32 56
|
eqeltrrd |
⊢ ( 𝜑 → 𝐹 ∈ ( dom 𝐹 –cn→ ℂ ) ) |
58 |
|
cncffvrn |
⊢ ( ( ℝ ⊆ ℂ ∧ 𝐹 ∈ ( dom 𝐹 –cn→ ℂ ) ) → ( 𝐹 ∈ ( dom 𝐹 –cn→ ℝ ) ↔ 𝐹 : dom 𝐹 ⟶ ℝ ) ) |
59 |
6 57 58
|
sylancr |
⊢ ( 𝜑 → ( 𝐹 ∈ ( dom 𝐹 –cn→ ℝ ) ↔ 𝐹 : dom 𝐹 ⟶ ℝ ) ) |
60 |
16 59
|
mpbird |
⊢ ( 𝜑 → 𝐹 ∈ ( dom 𝐹 –cn→ ℝ ) ) |
61 |
|
rescncf |
⊢ ( ( 𝐴 [,] 𝐵 ) ⊆ dom 𝐹 → ( 𝐹 ∈ ( dom 𝐹 –cn→ ℝ ) → ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) ) ) |
62 |
5 60 61
|
sylc |
⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) ) |
63 |
1 2 11 47 62
|
c1lip1 |
⊢ ( 𝜑 → ∃ 𝑘 ∈ ℝ ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( 𝑦 − 𝑥 ) ) ) ) |