Step | Hyp | Ref
| Expression |
1 | | caucvgr.2 |
. . . . 5
β’ (π β πΉ:π΄βΆβ) |
2 | 1 | feqmptd 6911 |
. . . 4
β’ (π β πΉ = (π β π΄ β¦ (πΉβπ))) |
3 | 1 | ffvelcdmda 7036 |
. . . . . 6
β’ ((π β§ π β π΄) β (πΉβπ) β β) |
4 | 3 | replimd 15088 |
. . . . 5
β’ ((π β§ π β π΄) β (πΉβπ) = ((ββ(πΉβπ)) + (i Β· (ββ(πΉβπ))))) |
5 | 4 | mpteq2dva 5206 |
. . . 4
β’ (π β (π β π΄ β¦ (πΉβπ)) = (π β π΄ β¦ ((ββ(πΉβπ)) + (i Β· (ββ(πΉβπ)))))) |
6 | 2, 5 | eqtrd 2773 |
. . 3
β’ (π β πΉ = (π β π΄ β¦ ((ββ(πΉβπ)) + (i Β· (ββ(πΉβπ)))))) |
7 | | fvexd 6858 |
. . . 4
β’ ((π β§ π β π΄) β (ββ(πΉβπ)) β V) |
8 | | ovexd 7393 |
. . . 4
β’ ((π β§ π β π΄) β (i Β· (ββ(πΉβπ))) β V) |
9 | | caucvgr.1 |
. . . . 5
β’ (π β π΄ β β) |
10 | | caucvgr.3 |
. . . . 5
β’ (π β sup(π΄, β*, < ) =
+β) |
11 | | caucvgr.4 |
. . . . 5
β’ (π β βπ₯ β β+ βπ β π΄ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π₯)) |
12 | | ref 15003 |
. . . . 5
β’
β:ββΆβ |
13 | | resub 15018 |
. . . . . . 7
β’ (((πΉβπ) β β β§ (πΉβπ) β β) β
(ββ((πΉβπ) β (πΉβπ))) = ((ββ(πΉβπ)) β (ββ(πΉβπ)))) |
14 | 13 | fveq2d 6847 |
. . . . . 6
β’ (((πΉβπ) β β β§ (πΉβπ) β β) β
(absβ(ββ((πΉβπ) β (πΉβπ)))) = (absβ((ββ(πΉβπ)) β (ββ(πΉβπ))))) |
15 | | subcl 11405 |
. . . . . . 7
β’ (((πΉβπ) β β β§ (πΉβπ) β β) β ((πΉβπ) β (πΉβπ)) β β) |
16 | | absrele 15199 |
. . . . . . 7
β’ (((πΉβπ) β (πΉβπ)) β β β
(absβ(ββ((πΉβπ) β (πΉβπ)))) β€ (absβ((πΉβπ) β (πΉβπ)))) |
17 | 15, 16 | syl 17 |
. . . . . 6
β’ (((πΉβπ) β β β§ (πΉβπ) β β) β
(absβ(ββ((πΉβπ) β (πΉβπ)))) β€ (absβ((πΉβπ) β (πΉβπ)))) |
18 | 14, 17 | eqbrtrrd 5130 |
. . . . 5
β’ (((πΉβπ) β β β§ (πΉβπ) β β) β
(absβ((ββ(πΉβπ)) β (ββ(πΉβπ)))) β€ (absβ((πΉβπ) β (πΉβπ)))) |
19 | 9, 1, 10, 11, 12, 18 | caucvgrlem2 15565 |
. . . 4
β’ (π β (π β π΄ β¦ (ββ(πΉβπ))) βπ (
βπ β(β β πΉ))) |
20 | | ax-icn 11115 |
. . . . . . 7
β’ i β
β |
21 | 20 | elexi 3463 |
. . . . . 6
β’ i β
V |
22 | 21 | a1i 11 |
. . . . 5
β’ ((π β§ π β π΄) β i β V) |
23 | | fvexd 6858 |
. . . . 5
β’ ((π β§ π β π΄) β (ββ(πΉβπ)) β V) |
24 | | rlimconst 15432 |
. . . . . 6
β’ ((π΄ β β β§ i β
β) β (π β
π΄ β¦ i)
βπ i) |
25 | 9, 20, 24 | sylancl 587 |
. . . . 5
β’ (π β (π β π΄ β¦ i) βπ
i) |
26 | | imf 15004 |
. . . . . 6
β’
β:ββΆβ |
27 | | imsub 15026 |
. . . . . . . 8
β’ (((πΉβπ) β β β§ (πΉβπ) β β) β
(ββ((πΉβπ) β (πΉβπ))) = ((ββ(πΉβπ)) β (ββ(πΉβπ)))) |
28 | 27 | fveq2d 6847 |
. . . . . . 7
β’ (((πΉβπ) β β β§ (πΉβπ) β β) β
(absβ(ββ((πΉβπ) β (πΉβπ)))) = (absβ((ββ(πΉβπ)) β (ββ(πΉβπ))))) |
29 | | absimle 15200 |
. . . . . . . 8
β’ (((πΉβπ) β (πΉβπ)) β β β
(absβ(ββ((πΉβπ) β (πΉβπ)))) β€ (absβ((πΉβπ) β (πΉβπ)))) |
30 | 15, 29 | syl 17 |
. . . . . . 7
β’ (((πΉβπ) β β β§ (πΉβπ) β β) β
(absβ(ββ((πΉβπ) β (πΉβπ)))) β€ (absβ((πΉβπ) β (πΉβπ)))) |
31 | 28, 30 | eqbrtrrd 5130 |
. . . . . 6
β’ (((πΉβπ) β β β§ (πΉβπ) β β) β
(absβ((ββ(πΉβπ)) β (ββ(πΉβπ)))) β€ (absβ((πΉβπ) β (πΉβπ)))) |
32 | 9, 1, 10, 11, 26, 31 | caucvgrlem2 15565 |
. . . . 5
β’ (π β (π β π΄ β¦ (ββ(πΉβπ))) βπ (
βπ β(β β πΉ))) |
33 | 22, 23, 25, 32 | rlimmul 15534 |
. . . 4
β’ (π β (π β π΄ β¦ (i Β· (ββ(πΉβπ)))) βπ (i Β·
( βπ β(β β πΉ)))) |
34 | 7, 8, 19, 33 | rlimadd 15531 |
. . 3
β’ (π β (π β π΄ β¦ ((ββ(πΉβπ)) + (i Β· (ββ(πΉβπ))))) βπ ((
βπ β(β β πΉ)) + (i Β· (
βπ β(β β πΉ))))) |
35 | 6, 34 | eqbrtrd 5128 |
. 2
β’ (π β πΉ βπ ((
βπ β(β β πΉ)) + (i Β· (
βπ β(β β πΉ))))) |
36 | | rlimrel 15381 |
. . 3
β’ Rel
βπ |
37 | 36 | releldmi 5904 |
. 2
β’ (πΉ βπ ((
βπ β(β β πΉ)) + (i Β· (
βπ β(β β πΉ)))) β πΉ β dom βπ
) |
38 | 35, 37 | syl 17 |
1
β’ (π β πΉ β dom βπ
) |