Step | Hyp | Ref
| Expression |
1 | | limccnp.j |
. . . . 5
β’ π½ = (πΎ βΎt π·) |
2 | | limccnpcntop.k |
. . . . . . 7
β’ πΎ = (MetOpenβ(abs β
β )) |
3 | 2 | cntoptopon 14303 |
. . . . . 6
β’ πΎ β
(TopOnββ) |
4 | | limccnp.d |
. . . . . 6
β’ (π β π· β β) |
5 | | resttopon 13942 |
. . . . . 6
β’ ((πΎ β (TopOnββ)
β§ π· β β)
β (πΎ
βΎt π·)
β (TopOnβπ·)) |
6 | 3, 4, 5 | sylancr 414 |
. . . . 5
β’ (π β (πΎ βΎt π·) β (TopOnβπ·)) |
7 | 1, 6 | eqeltrid 2274 |
. . . 4
β’ (π β π½ β (TopOnβπ·)) |
8 | 3 | a1i 9 |
. . . 4
β’ (π β πΎ β
(TopOnββ)) |
9 | | limccnp.b |
. . . 4
β’ (π β πΊ β ((π½ CnP πΎ)βπΆ)) |
10 | | cnpf2 13978 |
. . . 4
β’ ((π½ β (TopOnβπ·) β§ πΎ β (TopOnββ) β§ πΊ β ((π½ CnP πΎ)βπΆ)) β πΊ:π·βΆβ) |
11 | 7, 8, 9, 10 | syl3anc 1248 |
. . 3
β’ (π β πΊ:π·βΆβ) |
12 | 2 | cntoptop 14304 |
. . . . 5
β’ πΎ β Top |
13 | 12 | a1i 9 |
. . . 4
β’ (π β πΎ β Top) |
14 | | cnprcl2k 13977 |
. . . 4
β’ ((π½ β (TopOnβπ·) β§ πΎ β Top β§ πΊ β ((π½ CnP πΎ)βπΆ)) β πΆ β π·) |
15 | 7, 13, 9, 14 | syl3anc 1248 |
. . 3
β’ (π β πΆ β π·) |
16 | 11, 15 | ffvelcdmd 5665 |
. 2
β’ (π β (πΊβπΆ) β β) |
17 | | cnxmet 14302 |
. . . . . . . 8
β’ (abs
β β ) β (βMetββ) |
18 | | eqid 2187 |
. . . . . . . . 9
β’ ((abs
β β ) βΎ (π· Γ π·)) = ((abs β β ) βΎ (π· Γ π·)) |
19 | | eqid 2187 |
. . . . . . . . 9
β’
(MetOpenβ((abs β β ) βΎ (π· Γ π·))) = (MetOpenβ((abs β β )
βΎ (π· Γ π·))) |
20 | 18, 2, 19 | metrest 14277 |
. . . . . . . 8
β’ (((abs
β β ) β (βMetββ) β§ π· β β) β (πΎ βΎt π·) = (MetOpenβ((abs β β )
βΎ (π· Γ π·)))) |
21 | 17, 4, 20 | sylancr 414 |
. . . . . . 7
β’ (π β (πΎ βΎt π·) = (MetOpenβ((abs β β )
βΎ (π· Γ π·)))) |
22 | 1, 21 | eqtrid 2232 |
. . . . . 6
β’ (π β π½ = (MetOpenβ((abs β β )
βΎ (π· Γ π·)))) |
23 | 2 | a1i 9 |
. . . . . 6
β’ (π β πΎ = (MetOpenβ(abs β β
))) |
24 | | xmetres2 14150 |
. . . . . . 7
β’ (((abs
β β ) β (βMetββ) β§ π· β β) β ((abs β
β ) βΎ (π·
Γ π·)) β
(βMetβπ·)) |
25 | 17, 4, 24 | sylancr 414 |
. . . . . 6
β’ (π β ((abs β β )
βΎ (π· Γ π·)) β
(βMetβπ·)) |
26 | 17 | a1i 9 |
. . . . . 6
β’ (π β (abs β β )
β (βMetββ)) |
27 | 22, 23, 25, 26, 15 | metcnpd 14291 |
. . . . 5
β’ (π β (πΊ β ((π½ CnP πΎ)βπΆ) β (πΊ:π·βΆβ β§ βπ β β+
βπ β
β+ βπ€ β π· ((πΆ((abs β β ) βΎ (π· Γ π·))π€) < π β ((πΊβπΆ)(abs β β )(πΊβπ€)) < π)))) |
28 | 9, 27 | mpbid 147 |
. . . 4
β’ (π β (πΊ:π·βΆβ β§ βπ β β+
βπ β
β+ βπ€ β π· ((πΆ((abs β β ) βΎ (π· Γ π·))π€) < π β ((πΊβπΆ)(abs β β )(πΊβπ€)) < π))) |
29 | 28 | simprd 114 |
. . 3
β’ (π β βπ β β+ βπ β β+
βπ€ β π· ((πΆ((abs β β ) βΎ (π· Γ π·))π€) < π β ((πΊβπΆ)(abs β β )(πΊβπ€)) < π)) |
30 | | simplll 533 |
. . . . . . 7
β’ ((((π β§ π β β+) β§ π β β+)
β§ βπ€ β
π· ((πΆ((abs β β ) βΎ (π· Γ π·))π€) < π β ((πΊβπΆ)(abs β β )(πΊβπ€)) < π)) β π) |
31 | | simplr 528 |
. . . . . . 7
β’ ((((π β§ π β β+) β§ π β β+)
β§ βπ€ β
π· ((πΆ((abs β β ) βΎ (π· Γ π·))π€) < π β ((πΊβπΆ)(abs β β )(πΊβπ€)) < π)) β π β β+) |
32 | | limccnp.c |
. . . . . . . . . 10
β’ (π β πΆ β (πΉ limβ π΅)) |
33 | | limccnp.f |
. . . . . . . . . . . 12
β’ (π β πΉ:π΄βΆπ·) |
34 | 33, 4 | fssd 5390 |
. . . . . . . . . . 11
β’ (π β πΉ:π΄βΆβ) |
35 | 33 | fdmd 5384 |
. . . . . . . . . . . 12
β’ (π β dom πΉ = π΄) |
36 | | limcrcl 14398 |
. . . . . . . . . . . . . 14
β’ (πΆ β (πΉ limβ π΅) β (πΉ:dom πΉβΆβ β§ dom πΉ β β β§ π΅ β β)) |
37 | 32, 36 | syl 14 |
. . . . . . . . . . . . 13
β’ (π β (πΉ:dom πΉβΆβ β§ dom πΉ β β β§ π΅ β β)) |
38 | 37 | simp2d 1011 |
. . . . . . . . . . . 12
β’ (π β dom πΉ β β) |
39 | 35, 38 | eqsstrrd 3204 |
. . . . . . . . . . 11
β’ (π β π΄ β β) |
40 | 37 | simp3d 1012 |
. . . . . . . . . . 11
β’ (π β π΅ β β) |
41 | 34, 39, 40 | ellimc3ap 14401 |
. . . . . . . . . 10
β’ (π β (πΆ β (πΉ limβ π΅) β (πΆ β β β§ βπ β β+
βπ β
β+ βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β πΆ)) < π)))) |
42 | 32, 41 | mpbid 147 |
. . . . . . . . 9
β’ (π β (πΆ β β β§ βπ β β+
βπ β
β+ βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β πΆ)) < π))) |
43 | 42 | simprd 114 |
. . . . . . . 8
β’ (π β βπ β β+ βπ β β+
βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β πΆ)) < π)) |
44 | 43 | r19.21bi 2575 |
. . . . . . 7
β’ ((π β§ π β β+) β
βπ β
β+ βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β πΆ)) < π)) |
45 | 30, 31, 44 | syl2anc 411 |
. . . . . 6
β’ ((((π β§ π β β+) β§ π β β+)
β§ βπ€ β
π· ((πΆ((abs β β ) βΎ (π· Γ π·))π€) < π β ((πΊβπΆ)(abs β β )(πΊβπ€)) < π)) β βπ β β+ βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β πΆ)) < π)) |
46 | | oveq2 5896 |
. . . . . . . . . . . . 13
β’ (π€ = (πΉβπ§) β (πΆ((abs β β ) βΎ (π· Γ π·))π€) = (πΆ((abs β β ) βΎ (π· Γ π·))(πΉβπ§))) |
47 | 46 | breq1d 4025 |
. . . . . . . . . . . 12
β’ (π€ = (πΉβπ§) β ((πΆ((abs β β ) βΎ (π· Γ π·))π€) < π β (πΆ((abs β β ) βΎ (π· Γ π·))(πΉβπ§)) < π)) |
48 | | fveq2 5527 |
. . . . . . . . . . . . . 14
β’ (π€ = (πΉβπ§) β (πΊβπ€) = (πΊβ(πΉβπ§))) |
49 | 48 | oveq2d 5904 |
. . . . . . . . . . . . 13
β’ (π€ = (πΉβπ§) β ((πΊβπΆ)(abs β β )(πΊβπ€)) = ((πΊβπΆ)(abs β β )(πΊβ(πΉβπ§)))) |
50 | 49 | breq1d 4025 |
. . . . . . . . . . . 12
β’ (π€ = (πΉβπ§) β (((πΊβπΆ)(abs β β )(πΊβπ€)) < π β ((πΊβπΆ)(abs β β )(πΊβ(πΉβπ§))) < π)) |
51 | 47, 50 | imbi12d 234 |
. . . . . . . . . . 11
β’ (π€ = (πΉβπ§) β (((πΆ((abs β β ) βΎ (π· Γ π·))π€) < π β ((πΊβπΆ)(abs β β )(πΊβπ€)) < π) β ((πΆ((abs β β ) βΎ (π· Γ π·))(πΉβπ§)) < π β ((πΊβπΆ)(abs β β )(πΊβ(πΉβπ§))) < π))) |
52 | | simpllr 534 |
. . . . . . . . . . 11
β’
((((((π β§ π β β+)
β§ π β
β+) β§ βπ€ β π· ((πΆ((abs β β ) βΎ (π· Γ π·))π€) < π β ((πΊβπΆ)(abs β β )(πΊβπ€)) < π)) β§ π β β+) β§ π§ β π΄) β βπ€ β π· ((πΆ((abs β β ) βΎ (π· Γ π·))π€) < π β ((πΊβπΆ)(abs β β )(πΊβπ€)) < π)) |
53 | 33 | ad5antr 496 |
. . . . . . . . . . . 12
β’
((((((π β§ π β β+)
β§ π β
β+) β§ βπ€ β π· ((πΆ((abs β β ) βΎ (π· Γ π·))π€) < π β ((πΊβπΆ)(abs β β )(πΊβπ€)) < π)) β§ π β β+) β§ π§ β π΄) β πΉ:π΄βΆπ·) |
54 | | simpr 110 |
. . . . . . . . . . . 12
β’
((((((π β§ π β β+)
β§ π β
β+) β§ βπ€ β π· ((πΆ((abs β β ) βΎ (π· Γ π·))π€) < π β ((πΊβπΆ)(abs β β )(πΊβπ€)) < π)) β§ π β β+) β§ π§ β π΄) β π§ β π΄) |
55 | 53, 54 | ffvelcdmd 5665 |
. . . . . . . . . . 11
β’
((((((π β§ π β β+)
β§ π β
β+) β§ βπ€ β π· ((πΆ((abs β β ) βΎ (π· Γ π·))π€) < π β ((πΊβπΆ)(abs β β )(πΊβπ€)) < π)) β§ π β β+) β§ π§ β π΄) β (πΉβπ§) β π·) |
56 | 51, 52, 55 | rspcdva 2858 |
. . . . . . . . . 10
β’
((((((π β§ π β β+)
β§ π β
β+) β§ βπ€ β π· ((πΆ((abs β β ) βΎ (π· Γ π·))π€) < π β ((πΊβπΆ)(abs β β )(πΊβπ€)) < π)) β§ π β β+) β§ π§ β π΄) β ((πΆ((abs β β ) βΎ (π· Γ π·))(πΉβπ§)) < π β ((πΊβπΆ)(abs β β )(πΊβ(πΉβπ§))) < π)) |
57 | 15 | ad5antr 496 |
. . . . . . . . . . . . 13
β’
((((((π β§ π β β+)
β§ π β
β+) β§ βπ€ β π· ((πΆ((abs β β ) βΎ (π· Γ π·))π€) < π β ((πΊβπΆ)(abs β β )(πΊβπ€)) < π)) β§ π β β+) β§ π§ β π΄) β πΆ β π·) |
58 | 57, 55 | ovresd 6028 |
. . . . . . . . . . . 12
β’
((((((π β§ π β β+)
β§ π β
β+) β§ βπ€ β π· ((πΆ((abs β β ) βΎ (π· Γ π·))π€) < π β ((πΊβπΆ)(abs β β )(πΊβπ€)) < π)) β§ π β β+) β§ π§ β π΄) β (πΆ((abs β β ) βΎ (π· Γ π·))(πΉβπ§)) = (πΆ(abs β β )(πΉβπ§))) |
59 | 42 | simpld 112 |
. . . . . . . . . . . . . 14
β’ (π β πΆ β β) |
60 | 59 | ad5antr 496 |
. . . . . . . . . . . . 13
β’
((((((π β§ π β β+)
β§ π β
β+) β§ βπ€ β π· ((πΆ((abs β β ) βΎ (π· Γ π·))π€) < π β ((πΊβπΆ)(abs β β )(πΊβπ€)) < π)) β§ π β β+) β§ π§ β π΄) β πΆ β β) |
61 | 4 | ad5antr 496 |
. . . . . . . . . . . . . 14
β’
((((((π β§ π β β+)
β§ π β
β+) β§ βπ€ β π· ((πΆ((abs β β ) βΎ (π· Γ π·))π€) < π β ((πΊβπΆ)(abs β β )(πΊβπ€)) < π)) β§ π β β+) β§ π§ β π΄) β π· β β) |
62 | 61, 55 | sseldd 3168 |
. . . . . . . . . . . . 13
β’
((((((π β§ π β β+)
β§ π β
β+) β§ βπ€ β π· ((πΆ((abs β β ) βΎ (π· Γ π·))π€) < π β ((πΊβπΆ)(abs β β )(πΊβπ€)) < π)) β§ π β β+) β§ π§ β π΄) β (πΉβπ§) β β) |
63 | | eqid 2187 |
. . . . . . . . . . . . . 14
β’ (abs
β β ) = (abs β β ) |
64 | 63 | cnmetdval 14300 |
. . . . . . . . . . . . 13
β’ ((πΆ β β β§ (πΉβπ§) β β) β (πΆ(abs β β )(πΉβπ§)) = (absβ(πΆ β (πΉβπ§)))) |
65 | 60, 62, 64 | syl2anc 411 |
. . . . . . . . . . . 12
β’
((((((π β§ π β β+)
β§ π β
β+) β§ βπ€ β π· ((πΆ((abs β β ) βΎ (π· Γ π·))π€) < π β ((πΊβπΆ)(abs β β )(πΊβπ€)) < π)) β§ π β β+) β§ π§ β π΄) β (πΆ(abs β β )(πΉβπ§)) = (absβ(πΆ β (πΉβπ§)))) |
66 | 60, 62 | abssubd 11215 |
. . . . . . . . . . . 12
β’
((((((π β§ π β β+)
β§ π β
β+) β§ βπ€ β π· ((πΆ((abs β β ) βΎ (π· Γ π·))π€) < π β ((πΊβπΆ)(abs β β )(πΊβπ€)) < π)) β§ π β β+) β§ π§ β π΄) β (absβ(πΆ β (πΉβπ§))) = (absβ((πΉβπ§) β πΆ))) |
67 | 58, 65, 66 | 3eqtrd 2224 |
. . . . . . . . . . 11
β’
((((((π β§ π β β+)
β§ π β
β+) β§ βπ€ β π· ((πΆ((abs β β ) βΎ (π· Γ π·))π€) < π β ((πΊβπΆ)(abs β β )(πΊβπ€)) < π)) β§ π β β+) β§ π§ β π΄) β (πΆ((abs β β ) βΎ (π· Γ π·))(πΉβπ§)) = (absβ((πΉβπ§) β πΆ))) |
68 | 67 | breq1d 4025 |
. . . . . . . . . 10
β’
((((((π β§ π β β+)
β§ π β
β+) β§ βπ€ β π· ((πΆ((abs β β ) βΎ (π· Γ π·))π€) < π β ((πΊβπΆ)(abs β β )(πΊβπ€)) < π)) β§ π β β+) β§ π§ β π΄) β ((πΆ((abs β β ) βΎ (π· Γ π·))(πΉβπ§)) < π β (absβ((πΉβπ§) β πΆ)) < π)) |
69 | 16 | ad5antr 496 |
. . . . . . . . . . . . 13
β’
((((((π β§ π β β+)
β§ π β
β+) β§ βπ€ β π· ((πΆ((abs β β ) βΎ (π· Γ π·))π€) < π β ((πΊβπΆ)(abs β β )(πΊβπ€)) < π)) β§ π β β+) β§ π§ β π΄) β (πΊβπΆ) β β) |
70 | 11 | ad5antr 496 |
. . . . . . . . . . . . . 14
β’
((((((π β§ π β β+)
β§ π β
β+) β§ βπ€ β π· ((πΆ((abs β β ) βΎ (π· Γ π·))π€) < π β ((πΊβπΆ)(abs β β )(πΊβπ€)) < π)) β§ π β β+) β§ π§ β π΄) β πΊ:π·βΆβ) |
71 | 70, 55 | ffvelcdmd 5665 |
. . . . . . . . . . . . 13
β’
((((((π β§ π β β+)
β§ π β
β+) β§ βπ€ β π· ((πΆ((abs β β ) βΎ (π· Γ π·))π€) < π β ((πΊβπΆ)(abs β β )(πΊβπ€)) < π)) β§ π β β+) β§ π§ β π΄) β (πΊβ(πΉβπ§)) β β) |
72 | 63 | cnmetdval 14300 |
. . . . . . . . . . . . 13
β’ (((πΊβπΆ) β β β§ (πΊβ(πΉβπ§)) β β) β ((πΊβπΆ)(abs β β )(πΊβ(πΉβπ§))) = (absβ((πΊβπΆ) β (πΊβ(πΉβπ§))))) |
73 | 69, 71, 72 | syl2anc 411 |
. . . . . . . . . . . 12
β’
((((((π β§ π β β+)
β§ π β
β+) β§ βπ€ β π· ((πΆ((abs β β ) βΎ (π· Γ π·))π€) < π β ((πΊβπΆ)(abs β β )(πΊβπ€)) < π)) β§ π β β+) β§ π§ β π΄) β ((πΊβπΆ)(abs β β )(πΊβ(πΉβπ§))) = (absβ((πΊβπΆ) β (πΊβ(πΉβπ§))))) |
74 | | fvco3 5600 |
. . . . . . . . . . . . . . 15
β’ ((πΉ:π΄βΆπ· β§ π§ β π΄) β ((πΊ β πΉ)βπ§) = (πΊβ(πΉβπ§))) |
75 | 53, 54, 74 | syl2anc 411 |
. . . . . . . . . . . . . 14
β’
((((((π β§ π β β+)
β§ π β
β+) β§ βπ€ β π· ((πΆ((abs β β ) βΎ (π· Γ π·))π€) < π β ((πΊβπΆ)(abs β β )(πΊβπ€)) < π)) β§ π β β+) β§ π§ β π΄) β ((πΊ β πΉ)βπ§) = (πΊβ(πΉβπ§))) |
76 | 75 | oveq2d 5904 |
. . . . . . . . . . . . 13
β’
((((((π β§ π β β+)
β§ π β
β+) β§ βπ€ β π· ((πΆ((abs β β ) βΎ (π· Γ π·))π€) < π β ((πΊβπΆ)(abs β β )(πΊβπ€)) < π)) β§ π β β+) β§ π§ β π΄) β ((πΊβπΆ) β ((πΊ β πΉ)βπ§)) = ((πΊβπΆ) β (πΊβ(πΉβπ§)))) |
77 | 76 | fveq2d 5531 |
. . . . . . . . . . . 12
β’
((((((π β§ π β β+)
β§ π β
β+) β§ βπ€ β π· ((πΆ((abs β β ) βΎ (π· Γ π·))π€) < π β ((πΊβπΆ)(abs β β )(πΊβπ€)) < π)) β§ π β β+) β§ π§ β π΄) β (absβ((πΊβπΆ) β ((πΊ β πΉ)βπ§))) = (absβ((πΊβπΆ) β (πΊβ(πΉβπ§))))) |
78 | 75, 71 | eqeltrd 2264 |
. . . . . . . . . . . . 13
β’
((((((π β§ π β β+)
β§ π β
β+) β§ βπ€ β π· ((πΆ((abs β β ) βΎ (π· Γ π·))π€) < π β ((πΊβπΆ)(abs β β )(πΊβπ€)) < π)) β§ π β β+) β§ π§ β π΄) β ((πΊ β πΉ)βπ§) β β) |
79 | 69, 78 | abssubd 11215 |
. . . . . . . . . . . 12
β’
((((((π β§ π β β+)
β§ π β
β+) β§ βπ€ β π· ((πΆ((abs β β ) βΎ (π· Γ π·))π€) < π β ((πΊβπΆ)(abs β β )(πΊβπ€)) < π)) β§ π β β+) β§ π§ β π΄) β (absβ((πΊβπΆ) β ((πΊ β πΉ)βπ§))) = (absβ(((πΊ β πΉ)βπ§) β (πΊβπΆ)))) |
80 | 73, 77, 79 | 3eqtr2d 2226 |
. . . . . . . . . . 11
β’
((((((π β§ π β β+)
β§ π β
β+) β§ βπ€ β π· ((πΆ((abs β β ) βΎ (π· Γ π·))π€) < π β ((πΊβπΆ)(abs β β )(πΊβπ€)) < π)) β§ π β β+) β§ π§ β π΄) β ((πΊβπΆ)(abs β β )(πΊβ(πΉβπ§))) = (absβ(((πΊ β πΉ)βπ§) β (πΊβπΆ)))) |
81 | 80 | breq1d 4025 |
. . . . . . . . . 10
β’
((((((π β§ π β β+)
β§ π β
β+) β§ βπ€ β π· ((πΆ((abs β β ) βΎ (π· Γ π·))π€) < π β ((πΊβπΆ)(abs β β )(πΊβπ€)) < π)) β§ π β β+) β§ π§ β π΄) β (((πΊβπΆ)(abs β β )(πΊβ(πΉβπ§))) < π β (absβ(((πΊ β πΉ)βπ§) β (πΊβπΆ))) < π)) |
82 | 56, 68, 81 | 3imtr3d 202 |
. . . . . . . . 9
β’
((((((π β§ π β β+)
β§ π β
β+) β§ βπ€ β π· ((πΆ((abs β β ) βΎ (π· Γ π·))π€) < π β ((πΊβπΆ)(abs β β )(πΊβπ€)) < π)) β§ π β β+) β§ π§ β π΄) β ((absβ((πΉβπ§) β πΆ)) < π β (absβ(((πΊ β πΉ)βπ§) β (πΊβπΆ))) < π)) |
83 | 82 | imim2d 54 |
. . . . . . . 8
β’
((((((π β§ π β β+)
β§ π β
β+) β§ βπ€ β π· ((πΆ((abs β β ) βΎ (π· Γ π·))π€) < π β ((πΊβπΆ)(abs β β )(πΊβπ€)) < π)) β§ π β β+) β§ π§ β π΄) β (((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β πΆ)) < π) β ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ(((πΊ β πΉ)βπ§) β (πΊβπΆ))) < π))) |
84 | 83 | ralimdva 2554 |
. . . . . . 7
β’
(((((π β§ π β β+)
β§ π β
β+) β§ βπ€ β π· ((πΆ((abs β β ) βΎ (π· Γ π·))π€) < π β ((πΊβπΆ)(abs β β )(πΊβπ€)) < π)) β§ π β β+) β
(βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β πΆ)) < π) β βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ(((πΊ β πΉ)βπ§) β (πΊβπΆ))) < π))) |
85 | 84 | reximdva 2589 |
. . . . . 6
β’ ((((π β§ π β β+) β§ π β β+)
β§ βπ€ β
π· ((πΆ((abs β β ) βΎ (π· Γ π·))π€) < π β ((πΊβπΆ)(abs β β )(πΊβπ€)) < π)) β (βπ β β+ βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β πΆ)) < π) β βπ β β+ βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ(((πΊ β πΉ)βπ§) β (πΊβπΆ))) < π))) |
86 | 45, 85 | mpd 13 |
. . . . 5
β’ ((((π β§ π β β+) β§ π β β+)
β§ βπ€ β
π· ((πΆ((abs β β ) βΎ (π· Γ π·))π€) < π β ((πΊβπΆ)(abs β β )(πΊβπ€)) < π)) β βπ β β+ βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ(((πΊ β πΉ)βπ§) β (πΊβπΆ))) < π)) |
87 | 86 | rexlimdva2 2607 |
. . . 4
β’ ((π β§ π β β+) β
(βπ β
β+ βπ€ β π· ((πΆ((abs β β ) βΎ (π· Γ π·))π€) < π β ((πΊβπΆ)(abs β β )(πΊβπ€)) < π) β βπ β β+ βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ(((πΊ β πΉ)βπ§) β (πΊβπΆ))) < π))) |
88 | 87 | ralimdva 2554 |
. . 3
β’ (π β (βπ β β+
βπ β
β+ βπ€ β π· ((πΆ((abs β β ) βΎ (π· Γ π·))π€) < π β ((πΊβπΆ)(abs β β )(πΊβπ€)) < π) β βπ β β+ βπ β β+
βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ(((πΊ β πΉ)βπ§) β (πΊβπΆ))) < π))) |
89 | 29, 88 | mpd 13 |
. 2
β’ (π β βπ β β+ βπ β β+
βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ(((πΊ β πΉ)βπ§) β (πΊβπΆ))) < π)) |
90 | | fco 5393 |
. . . 4
β’ ((πΊ:π·βΆβ β§ πΉ:π΄βΆπ·) β (πΊ β πΉ):π΄βΆβ) |
91 | 11, 33, 90 | syl2anc 411 |
. . 3
β’ (π β (πΊ β πΉ):π΄βΆβ) |
92 | 91, 39, 40 | ellimc3ap 14401 |
. 2
β’ (π β ((πΊβπΆ) β ((πΊ β πΉ) limβ π΅) β ((πΊβπΆ) β β β§ βπ β β+
βπ β
β+ βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ(((πΊ β πΉ)βπ§) β (πΊβπΆ))) < π)))) |
93 | 16, 89, 92 | mpbir2and 945 |
1
β’ (π β (πΊβπΆ) β ((πΊ β πΉ) limβ π΅)) |