Step | Hyp | Ref
| Expression |
1 | | limcrecl.4 |
. . 3
β’ (π β πΏ β (πΉ limβ π΅)) |
2 | 1 | adantr 480 |
. 2
β’ ((π β§ Β¬ πΏ β β) β πΏ β (πΉ limβ π΅)) |
3 | | limccl 25625 |
. . . . . . . . . 10
β’ (πΉ limβ π΅) β
β |
4 | 3, 1 | sselid 3980 |
. . . . . . . . 9
β’ (π β πΏ β β) |
5 | 4 | adantr 480 |
. . . . . . . 8
β’ ((π β§ Β¬ πΏ β β) β πΏ β β) |
6 | | simpr 484 |
. . . . . . . 8
β’ ((π β§ Β¬ πΏ β β) β Β¬ πΏ β
β) |
7 | 5, 6 | eldifd 3959 |
. . . . . . 7
β’ ((π β§ Β¬ πΏ β β) β πΏ β (β β
β)) |
8 | 7 | dstregt0 44290 |
. . . . . 6
β’ ((π β§ Β¬ πΏ β β) β βπ₯ β β+
βπ€ β β
π₯ < (absβ(πΏ β π€))) |
9 | | cnxmet 24510 |
. . . . . . . . . . . . . 14
β’ (abs
β β ) β (βMetββ) |
10 | 9 | a1i 11 |
. . . . . . . . . . . . 13
β’
(((((π β§ Β¬
πΏ β β) β§
π₯ β
β+) β§ βπ€ β β π₯ < (absβ(πΏ β π€))) β§ π¦ β β+) β (abs
β β ) β (βMetββ)) |
11 | | limcrecl.2 |
. . . . . . . . . . . . . . 15
β’ (π β π΄ β β) |
12 | 11 | ad4antr 729 |
. . . . . . . . . . . . . 14
β’
(((((π β§ Β¬
πΏ β β) β§
π₯ β
β+) β§ βπ€ β β π₯ < (absβ(πΏ β π€))) β§ π¦ β β+) β π΄ β
β) |
13 | 12 | ssdifssd 4142 |
. . . . . . . . . . . . 13
β’
(((((π β§ Β¬
πΏ β β) β§
π₯ β
β+) β§ βπ€ β β π₯ < (absβ(πΏ β π€))) β§ π¦ β β+) β (π΄ β {π΅}) β β) |
14 | | limcrecl.3 |
. . . . . . . . . . . . . . 15
β’ (π β π΅ β
((limPtβ(TopOpenββfld))βπ΄)) |
15 | | eqid 2731 |
. . . . . . . . . . . . . . . . . 18
β’
(TopOpenββfld) =
(TopOpenββfld) |
16 | 15 | cnfldtop 24521 |
. . . . . . . . . . . . . . . . 17
β’
(TopOpenββfld) β Top |
17 | 16 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (π β
(TopOpenββfld) β Top) |
18 | | unicntop 24523 |
. . . . . . . . . . . . . . . . 17
β’ β =
βͺ
(TopOpenββfld) |
19 | 11, 18 | sseqtrdi 4032 |
. . . . . . . . . . . . . . . 16
β’ (π β π΄ β βͺ
(TopOpenββfld)) |
20 | | eqid 2731 |
. . . . . . . . . . . . . . . . 17
β’ βͺ (TopOpenββfld) = βͺ (TopOpenββfld) |
21 | 20 | lpdifsn 22868 |
. . . . . . . . . . . . . . . 16
β’
(((TopOpenββfld) β Top β§ π΄ β βͺ (TopOpenββfld)) β (π΅ β
((limPtβ(TopOpenββfld))βπ΄) β π΅ β
((limPtβ(TopOpenββfld))β(π΄ β {π΅})))) |
22 | 17, 19, 21 | syl2anc 583 |
. . . . . . . . . . . . . . 15
β’ (π β (π΅ β
((limPtβ(TopOpenββfld))βπ΄) β π΅ β
((limPtβ(TopOpenββfld))β(π΄ β {π΅})))) |
23 | 14, 22 | mpbid 231 |
. . . . . . . . . . . . . 14
β’ (π β π΅ β
((limPtβ(TopOpenββfld))β(π΄ β {π΅}))) |
24 | 23 | ad4antr 729 |
. . . . . . . . . . . . 13
β’
(((((π β§ Β¬
πΏ β β) β§
π₯ β
β+) β§ βπ€ β β π₯ < (absβ(πΏ β π€))) β§ π¦ β β+) β π΅ β
((limPtβ(TopOpenββfld))β(π΄ β {π΅}))) |
25 | | simpr 484 |
. . . . . . . . . . . . 13
β’
(((((π β§ Β¬
πΏ β β) β§
π₯ β
β+) β§ βπ€ β β π₯ < (absβ(πΏ β π€))) β§ π¦ β β+) β π¦ β
β+) |
26 | 15 | cnfldtopn 24519 |
. . . . . . . . . . . . . 14
β’
(TopOpenββfld) = (MetOpenβ(abs β
β )) |
27 | 26 | lpbl 24233 |
. . . . . . . . . . . . 13
β’ ((((abs
β β ) β (βMetββ) β§ (π΄ β {π΅}) β β β§ π΅ β
((limPtβ(TopOpenββfld))β(π΄ β {π΅}))) β§ π¦ β β+) β
βπ§ β (π΄ β {π΅})π§ β (π΅(ballβ(abs β β ))π¦)) |
28 | 10, 13, 24, 25, 27 | syl31anc 1372 |
. . . . . . . . . . . 12
β’
(((((π β§ Β¬
πΏ β β) β§
π₯ β
β+) β§ βπ€ β β π₯ < (absβ(πΏ β π€))) β§ π¦ β β+) β
βπ§ β (π΄ β {π΅})π§ β (π΅(ballβ(abs β β ))π¦)) |
29 | | eldif 3958 |
. . . . . . . . . . . . . . 15
β’ (π§ β (π΄ β {π΅}) β (π§ β π΄ β§ Β¬ π§ β {π΅})) |
30 | 29 | anbi1i 623 |
. . . . . . . . . . . . . 14
β’ ((π§ β (π΄ β {π΅}) β§ π§ β (π΅(ballβ(abs β β ))π¦)) β ((π§ β π΄ β§ Β¬ π§ β {π΅}) β§ π§ β (π΅(ballβ(abs β β ))π¦))) |
31 | | anass 468 |
. . . . . . . . . . . . . 14
β’ (((π§ β π΄ β§ Β¬ π§ β {π΅}) β§ π§ β (π΅(ballβ(abs β β ))π¦)) β (π§ β π΄ β§ (Β¬ π§ β {π΅} β§ π§ β (π΅(ballβ(abs β β ))π¦)))) |
32 | 30, 31 | bitri 275 |
. . . . . . . . . . . . 13
β’ ((π§ β (π΄ β {π΅}) β§ π§ β (π΅(ballβ(abs β β ))π¦)) β (π§ β π΄ β§ (Β¬ π§ β {π΅} β§ π§ β (π΅(ballβ(abs β β ))π¦)))) |
33 | 32 | rexbii2 3089 |
. . . . . . . . . . . 12
β’
(βπ§ β
(π΄ β {π΅})π§ β (π΅(ballβ(abs β β ))π¦) β βπ§ β π΄ (Β¬ π§ β {π΅} β§ π§ β (π΅(ballβ(abs β β ))π¦))) |
34 | 28, 33 | sylib 217 |
. . . . . . . . . . 11
β’
(((((π β§ Β¬
πΏ β β) β§
π₯ β
β+) β§ βπ€ β β π₯ < (absβ(πΏ β π€))) β§ π¦ β β+) β
βπ§ β π΄ (Β¬ π§ β {π΅} β§ π§ β (π΅(ballβ(abs β β ))π¦))) |
35 | | simprl 768 |
. . . . . . . . . . . . . . . . 17
β’
((((((π β§ Β¬
πΏ β β) β§
π₯ β
β+) β§ βπ€ β β π₯ < (absβ(πΏ β π€))) β§ π¦ β β+) β§ (Β¬
π§ β {π΅} β§ π§ β (π΅(ballβ(abs β β ))π¦))) β Β¬ π§ β {π΅}) |
36 | | velsn 4644 |
. . . . . . . . . . . . . . . . . 18
β’ (π§ β {π΅} β π§ = π΅) |
37 | 36 | necon3bbii 2987 |
. . . . . . . . . . . . . . . . 17
β’ (Β¬
π§ β {π΅} β π§ β π΅) |
38 | 35, 37 | sylib 217 |
. . . . . . . . . . . . . . . 16
β’
((((((π β§ Β¬
πΏ β β) β§
π₯ β
β+) β§ βπ€ β β π₯ < (absβ(πΏ β π€))) β§ π¦ β β+) β§ (Β¬
π§ β {π΅} β§ π§ β (π΅(ballβ(abs β β ))π¦))) β π§ β π΅) |
39 | | simp-5l 782 |
. . . . . . . . . . . . . . . . 17
β’
((((((π β§ Β¬
πΏ β β) β§
π₯ β
β+) β§ βπ€ β β π₯ < (absβ(πΏ β π€))) β§ π¦ β β+) β§ (Β¬
π§ β {π΅} β§ π§ β (π΅(ballβ(abs β β ))π¦))) β π) |
40 | | simplr 766 |
. . . . . . . . . . . . . . . . 17
β’
((((((π β§ Β¬
πΏ β β) β§
π₯ β
β+) β§ βπ€ β β π₯ < (absβ(πΏ β π€))) β§ π¦ β β+) β§ (Β¬
π§ β {π΅} β§ π§ β (π΅(ballβ(abs β β ))π¦))) β π¦ β β+) |
41 | | simprr 770 |
. . . . . . . . . . . . . . . . 17
β’
((((((π β§ Β¬
πΏ β β) β§
π₯ β
β+) β§ βπ€ β β π₯ < (absβ(πΏ β π€))) β§ π¦ β β+) β§ (Β¬
π§ β {π΅} β§ π§ β (π΅(ballβ(abs β β ))π¦))) β π§ β (π΅(ballβ(abs β β ))π¦)) |
42 | | simp3 1137 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π¦ β β+ β§ π§ β (π΅(ballβ(abs β β ))π¦)) β π§ β (π΅(ballβ(abs β β ))π¦)) |
43 | 9 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π¦ β β+ β§ π§ β (π΅(ballβ(abs β β ))π¦)) β (abs β β )
β (βMetββ)) |
44 | 18 | lpss 22867 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((TopOpenββfld) β Top β§ π΄ β β) β
((limPtβ(TopOpenββfld))βπ΄) β β) |
45 | 17, 11, 44 | syl2anc 583 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β
((limPtβ(TopOpenββfld))βπ΄) β β) |
46 | 45, 14 | sseldd 3983 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β π΅ β β) |
47 | 46 | 3ad2ant1 1132 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π¦ β β+ β§ π§ β (π΅(ballβ(abs β β ))π¦)) β π΅ β β) |
48 | | rpxr 12988 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π¦ β β+
β π¦ β
β*) |
49 | 48 | 3ad2ant2 1133 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π¦ β β+ β§ π§ β (π΅(ballβ(abs β β ))π¦)) β π¦ β β*) |
50 | | elbl 24115 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((abs
β β ) β (βMetββ) β§ π΅ β β β§ π¦ β β*) β (π§ β (π΅(ballβ(abs β β ))π¦) β (π§ β β β§ (π΅(abs β β )π§) < π¦))) |
51 | 43, 47, 49, 50 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π¦ β β+ β§ π§ β (π΅(ballβ(abs β β ))π¦)) β (π§ β (π΅(ballβ(abs β β ))π¦) β (π§ β β β§ (π΅(abs β β )π§) < π¦))) |
52 | 42, 51 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π¦ β β+ β§ π§ β (π΅(ballβ(abs β β ))π¦)) β (π§ β β β§ (π΅(abs β β )π§) < π¦)) |
53 | 52 | simpld 494 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π¦ β β+ β§ π§ β (π΅(ballβ(abs β β ))π¦)) β π§ β β) |
54 | 53, 47 | abssubd 15405 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π¦ β β+ β§ π§ β (π΅(ballβ(abs β β ))π¦)) β (absβ(π§ β π΅)) = (absβ(π΅ β π§))) |
55 | | eqid 2731 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (abs
β β ) = (abs β β ) |
56 | 55 | cnmetdval 24508 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π΅ β β β§ π§ β β) β (π΅(abs β β )π§) = (absβ(π΅ β π§))) |
57 | 47, 53, 56 | syl2anc 583 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π¦ β β+ β§ π§ β (π΅(ballβ(abs β β ))π¦)) β (π΅(abs β β )π§) = (absβ(π΅ β π§))) |
58 | 52 | simprd 495 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π¦ β β+ β§ π§ β (π΅(ballβ(abs β β ))π¦)) β (π΅(abs β β )π§) < π¦) |
59 | 57, 58 | eqbrtrrd 5172 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π¦ β β+ β§ π§ β (π΅(ballβ(abs β β ))π¦)) β (absβ(π΅ β π§)) < π¦) |
60 | 54, 59 | eqbrtrd 5170 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π¦ β β+ β§ π§ β (π΅(ballβ(abs β β ))π¦)) β (absβ(π§ β π΅)) < π¦) |
61 | 39, 40, 41, 60 | syl3anc 1370 |
. . . . . . . . . . . . . . . 16
β’
((((((π β§ Β¬
πΏ β β) β§
π₯ β
β+) β§ βπ€ β β π₯ < (absβ(πΏ β π€))) β§ π¦ β β+) β§ (Β¬
π§ β {π΅} β§ π§ β (π΅(ballβ(abs β β ))π¦))) β (absβ(π§ β π΅)) < π¦) |
62 | 38, 61 | jca 511 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ Β¬
πΏ β β) β§
π₯ β
β+) β§ βπ€ β β π₯ < (absβ(πΏ β π€))) β§ π¦ β β+) β§ (Β¬
π§ β {π΅} β§ π§ β (π΅(ballβ(abs β β ))π¦))) β (π§ β π΅ β§ (absβ(π§ β π΅)) < π¦)) |
63 | 62 | adantlr 712 |
. . . . . . . . . . . . . 14
β’
(((((((π β§ Β¬
πΏ β β) β§
π₯ β
β+) β§ βπ€ β β π₯ < (absβ(πΏ β π€))) β§ π¦ β β+) β§ π§ β π΄) β§ (Β¬ π§ β {π΅} β§ π§ β (π΅(ballβ(abs β β ))π¦))) β (π§ β π΅ β§ (absβ(π§ β π΅)) < π¦)) |
64 | 39 | adantlr 712 |
. . . . . . . . . . . . . . . 16
β’
(((((((π β§ Β¬
πΏ β β) β§
π₯ β
β+) β§ βπ€ β β π₯ < (absβ(πΏ β π€))) β§ π¦ β β+) β§ π§ β π΄) β§ (Β¬ π§ β {π΅} β§ π§ β (π΅(ballβ(abs β β ))π¦))) β π) |
65 | | simplr 766 |
. . . . . . . . . . . . . . . 16
β’
(((((((π β§ Β¬
πΏ β β) β§
π₯ β
β+) β§ βπ€ β β π₯ < (absβ(πΏ β π€))) β§ π¦ β β+) β§ π§ β π΄) β§ (Β¬ π§ β {π΅} β§ π§ β (π΅(ballβ(abs β β ))π¦))) β π§ β π΄) |
66 | 64, 65 | jca 511 |
. . . . . . . . . . . . . . 15
β’
(((((((π β§ Β¬
πΏ β β) β§
π₯ β
β+) β§ βπ€ β β π₯ < (absβ(πΏ β π€))) β§ π¦ β β+) β§ π§ β π΄) β§ (Β¬ π§ β {π΅} β§ π§ β (π΅(ballβ(abs β β ))π¦))) β (π β§ π§ β π΄)) |
67 | | simp-5r 783 |
. . . . . . . . . . . . . . 15
β’
(((((((π β§ Β¬
πΏ β β) β§
π₯ β
β+) β§ βπ€ β β π₯ < (absβ(πΏ β π€))) β§ π¦ β β+) β§ π§ β π΄) β§ (Β¬ π§ β {π΅} β§ π§ β (π΅(ballβ(abs β β ))π¦))) β π₯ β β+) |
68 | | simp-4r 781 |
. . . . . . . . . . . . . . 15
β’
(((((((π β§ Β¬
πΏ β β) β§
π₯ β
β+) β§ βπ€ β β π₯ < (absβ(πΏ β π€))) β§ π¦ β β+) β§ π§ β π΄) β§ (Β¬ π§ β {π΅} β§ π§ β (π΅(ballβ(abs β β ))π¦))) β βπ€ β β π₯ < (absβ(πΏ β π€))) |
69 | | rpre 12987 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β β+
β π₯ β
β) |
70 | 69 | ad2antlr 724 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π§ β π΄) β§ π₯ β β+) β§
βπ€ β β
π₯ < (absβ(πΏ β π€))) β π₯ β β) |
71 | | limcrecl.1 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β πΉ:π΄βΆβ) |
72 | 71 | ffvelcdmda 7086 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π§ β π΄) β (πΉβπ§) β β) |
73 | 72 | recnd 11247 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π§ β π΄) β (πΉβπ§) β β) |
74 | 73 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π§ β π΄) β§ π₯ β β+) β§
βπ€ β β
π₯ < (absβ(πΏ β π€))) β (πΉβπ§) β β) |
75 | 4 | ad3antrrr 727 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π§ β π΄) β§ π₯ β β+) β§
βπ€ β β
π₯ < (absβ(πΏ β π€))) β πΏ β β) |
76 | 74, 75 | subcld 11576 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π§ β π΄) β§ π₯ β β+) β§
βπ€ β β
π₯ < (absβ(πΏ β π€))) β ((πΉβπ§) β πΏ) β β) |
77 | 76 | abscld 15388 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π§ β π΄) β§ π₯ β β+) β§
βπ€ β β
π₯ < (absβ(πΏ β π€))) β (absβ((πΉβπ§) β πΏ)) β β) |
78 | 72 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π§ β π΄) β§ βπ€ β β π₯ < (absβ(πΏ β π€))) β (πΉβπ§) β β) |
79 | | nfv 1916 |
. . . . . . . . . . . . . . . . . . . . 21
β’
β²π€π |
80 | | nfra1 3280 |
. . . . . . . . . . . . . . . . . . . . 21
β’
β²π€βπ€ β β π₯ < (absβ(πΏ β π€)) |
81 | 79, 80 | nfan 1901 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²π€(π β§ βπ€ β β π₯ < (absβ(πΏ β π€))) |
82 | | rspa 3244 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((βπ€ β
β π₯ <
(absβ(πΏ β π€)) β§ π€ β β) β π₯ < (absβ(πΏ β π€))) |
83 | 82 | adantll 711 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ βπ€ β β π₯ < (absβ(πΏ β π€))) β§ π€ β β) β π₯ < (absβ(πΏ β π€))) |
84 | 4 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π€ β β) β πΏ β β) |
85 | | ax-resscn 11170 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ β
β β |
86 | 85 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β β β
β) |
87 | 86 | sselda 3982 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π€ β β) β π€ β β) |
88 | 84, 87 | abssubd 15405 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π€ β β) β (absβ(πΏ β π€)) = (absβ(π€ β πΏ))) |
89 | 88 | adantlr 712 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ βπ€ β β π₯ < (absβ(πΏ β π€))) β§ π€ β β) β (absβ(πΏ β π€)) = (absβ(π€ β πΏ))) |
90 | 83, 89 | breqtrd 5174 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ βπ€ β β π₯ < (absβ(πΏ β π€))) β§ π€ β β) β π₯ < (absβ(π€ β πΏ))) |
91 | 90 | ex 412 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ βπ€ β β π₯ < (absβ(πΏ β π€))) β (π€ β β β π₯ < (absβ(π€ β πΏ)))) |
92 | 81, 91 | ralrimi 3253 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ βπ€ β β π₯ < (absβ(πΏ β π€))) β βπ€ β β π₯ < (absβ(π€ β πΏ))) |
93 | 92 | adantlr 712 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π§ β π΄) β§ βπ€ β β π₯ < (absβ(πΏ β π€))) β βπ€ β β π₯ < (absβ(π€ β πΏ))) |
94 | | fvoveq1 7435 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π€ = (πΉβπ§) β (absβ(π€ β πΏ)) = (absβ((πΉβπ§) β πΏ))) |
95 | 94 | breq2d 5160 |
. . . . . . . . . . . . . . . . . . 19
β’ (π€ = (πΉβπ§) β (π₯ < (absβ(π€ β πΏ)) β π₯ < (absβ((πΉβπ§) β πΏ)))) |
96 | 95 | rspcv 3608 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΉβπ§) β β β (βπ€ β β π₯ < (absβ(π€ β πΏ)) β π₯ < (absβ((πΉβπ§) β πΏ)))) |
97 | 78, 93, 96 | sylc 65 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π§ β π΄) β§ βπ€ β β π₯ < (absβ(πΏ β π€))) β π₯ < (absβ((πΉβπ§) β πΏ))) |
98 | 97 | adantlr 712 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π§ β π΄) β§ π₯ β β+) β§
βπ€ β β
π₯ < (absβ(πΏ β π€))) β π₯ < (absβ((πΉβπ§) β πΏ))) |
99 | 70, 77, 98 | ltnsymd 11368 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π§ β π΄) β§ π₯ β β+) β§
βπ€ β β
π₯ < (absβ(πΏ β π€))) β Β¬ (absβ((πΉβπ§) β πΏ)) < π₯) |
100 | 66, 67, 68, 99 | syl21anc 835 |
. . . . . . . . . . . . . 14
β’
(((((((π β§ Β¬
πΏ β β) β§
π₯ β
β+) β§ βπ€ β β π₯ < (absβ(πΏ β π€))) β§ π¦ β β+) β§ π§ β π΄) β§ (Β¬ π§ β {π΅} β§ π§ β (π΅(ballβ(abs β β ))π¦))) β Β¬
(absβ((πΉβπ§) β πΏ)) < π₯) |
101 | 63, 100 | jcnd 163 |
. . . . . . . . . . . . 13
β’
(((((((π β§ Β¬
πΏ β β) β§
π₯ β
β+) β§ βπ€ β β π₯ < (absβ(πΏ β π€))) β§ π¦ β β+) β§ π§ β π΄) β§ (Β¬ π§ β {π΅} β§ π§ β (π΅(ballβ(abs β β ))π¦))) β Β¬ ((π§ β π΅ β§ (absβ(π§ β π΅)) < π¦) β (absβ((πΉβπ§) β πΏ)) < π₯)) |
102 | 101 | ex 412 |
. . . . . . . . . . . 12
β’
((((((π β§ Β¬
πΏ β β) β§
π₯ β
β+) β§ βπ€ β β π₯ < (absβ(πΏ β π€))) β§ π¦ β β+) β§ π§ β π΄) β ((Β¬ π§ β {π΅} β§ π§ β (π΅(ballβ(abs β β ))π¦)) β Β¬ ((π§ β π΅ β§ (absβ(π§ β π΅)) < π¦) β (absβ((πΉβπ§) β πΏ)) < π₯))) |
103 | 102 | reximdva 3167 |
. . . . . . . . . . 11
β’
(((((π β§ Β¬
πΏ β β) β§
π₯ β
β+) β§ βπ€ β β π₯ < (absβ(πΏ β π€))) β§ π¦ β β+) β
(βπ§ β π΄ (Β¬ π§ β {π΅} β§ π§ β (π΅(ballβ(abs β β ))π¦)) β βπ§ β π΄ Β¬ ((π§ β π΅ β§ (absβ(π§ β π΅)) < π¦) β (absβ((πΉβπ§) β πΏ)) < π₯))) |
104 | 34, 103 | mpd 15 |
. . . . . . . . . 10
β’
(((((π β§ Β¬
πΏ β β) β§
π₯ β
β+) β§ βπ€ β β π₯ < (absβ(πΏ β π€))) β§ π¦ β β+) β
βπ§ β π΄ Β¬ ((π§ β π΅ β§ (absβ(π§ β π΅)) < π¦) β (absβ((πΉβπ§) β πΏ)) < π₯)) |
105 | | rexnal 3099 |
. . . . . . . . . 10
β’
(βπ§ β
π΄ Β¬ ((π§ β π΅ β§ (absβ(π§ β π΅)) < π¦) β (absβ((πΉβπ§) β πΏ)) < π₯) β Β¬ βπ§ β π΄ ((π§ β π΅ β§ (absβ(π§ β π΅)) < π¦) β (absβ((πΉβπ§) β πΏ)) < π₯)) |
106 | 104, 105 | sylib 217 |
. . . . . . . . 9
β’
(((((π β§ Β¬
πΏ β β) β§
π₯ β
β+) β§ βπ€ β β π₯ < (absβ(πΏ β π€))) β§ π¦ β β+) β Β¬
βπ§ β π΄ ((π§ β π΅ β§ (absβ(π§ β π΅)) < π¦) β (absβ((πΉβπ§) β πΏ)) < π₯)) |
107 | 106 | nrexdv 3148 |
. . . . . . . 8
β’ ((((π β§ Β¬ πΏ β β) β§ π₯ β β+) β§
βπ€ β β
π₯ < (absβ(πΏ β π€))) β Β¬ βπ¦ β β+ βπ§ β π΄ ((π§ β π΅ β§ (absβ(π§ β π΅)) < π¦) β (absβ((πΉβπ§) β πΏ)) < π₯)) |
108 | 107 | ex 412 |
. . . . . . 7
β’ (((π β§ Β¬ πΏ β β) β§ π₯ β β+) β
(βπ€ β β
π₯ < (absβ(πΏ β π€)) β Β¬ βπ¦ β β+ βπ§ β π΄ ((π§ β π΅ β§ (absβ(π§ β π΅)) < π¦) β (absβ((πΉβπ§) β πΏ)) < π₯))) |
109 | 108 | reximdva 3167 |
. . . . . 6
β’ ((π β§ Β¬ πΏ β β) β (βπ₯ β β+
βπ€ β β
π₯ < (absβ(πΏ β π€)) β βπ₯ β β+ Β¬
βπ¦ β
β+ βπ§ β π΄ ((π§ β π΅ β§ (absβ(π§ β π΅)) < π¦) β (absβ((πΉβπ§) β πΏ)) < π₯))) |
110 | 8, 109 | mpd 15 |
. . . . 5
β’ ((π β§ Β¬ πΏ β β) β βπ₯ β β+
Β¬ βπ¦ β
β+ βπ§ β π΄ ((π§ β π΅ β§ (absβ(π§ β π΅)) < π¦) β (absβ((πΉβπ§) β πΏ)) < π₯)) |
111 | | rexnal 3099 |
. . . . 5
β’
(βπ₯ β
β+ Β¬ βπ¦ β β+ βπ§ β π΄ ((π§ β π΅ β§ (absβ(π§ β π΅)) < π¦) β (absβ((πΉβπ§) β πΏ)) < π₯) β Β¬ βπ₯ β β+ βπ¦ β β+
βπ§ β π΄ ((π§ β π΅ β§ (absβ(π§ β π΅)) < π¦) β (absβ((πΉβπ§) β πΏ)) < π₯)) |
112 | 110, 111 | sylib 217 |
. . . 4
β’ ((π β§ Β¬ πΏ β β) β Β¬ βπ₯ β β+
βπ¦ β
β+ βπ§ β π΄ ((π§ β π΅ β§ (absβ(π§ β π΅)) < π¦) β (absβ((πΉβπ§) β πΏ)) < π₯)) |
113 | 112 | intnand 488 |
. . 3
β’ ((π β§ Β¬ πΏ β β) β Β¬ (πΏ β β β§
βπ₯ β
β+ βπ¦ β β+ βπ§ β π΄ ((π§ β π΅ β§ (absβ(π§ β π΅)) < π¦) β (absβ((πΉβπ§) β πΏ)) < π₯))) |
114 | 71, 86 | fssd 6735 |
. . . . 5
β’ (π β πΉ:π΄βΆβ) |
115 | 114, 11, 46 | ellimc3 25629 |
. . . 4
β’ (π β (πΏ β (πΉ limβ π΅) β (πΏ β β β§ βπ₯ β β+
βπ¦ β
β+ βπ§ β π΄ ((π§ β π΅ β§ (absβ(π§ β π΅)) < π¦) β (absβ((πΉβπ§) β πΏ)) < π₯)))) |
116 | 115 | adantr 480 |
. . 3
β’ ((π β§ Β¬ πΏ β β) β (πΏ β (πΉ limβ π΅) β (πΏ β β β§ βπ₯ β β+
βπ¦ β
β+ βπ§ β π΄ ((π§ β π΅ β§ (absβ(π§ β π΅)) < π¦) β (absβ((πΉβπ§) β πΏ)) < π₯)))) |
117 | 113, 116 | mtbird 325 |
. 2
β’ ((π β§ Β¬ πΏ β β) β Β¬ πΏ β (πΉ limβ π΅)) |
118 | 2, 117 | condan 815 |
1
β’ (π β πΏ β β) |