Step | Hyp | Ref
| Expression |
1 | | limccl 25262 |
. . . . . . . . . . . . 13
β’ ((πΉ βΎ (π΅(,)+β)) limβ π΅) β
β |
2 | | limclner.r |
. . . . . . . . . . . . 13
β’ (π β π
β ((πΉ βΎ (π΅(,)+β)) limβ π΅)) |
3 | 1, 2 | sselid 3946 |
. . . . . . . . . . . 12
β’ (π β π
β β) |
4 | 3 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β) β§ βπ¦ β β+
βπ§ β
β+ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β π
β β) |
5 | | limccl 25262 |
. . . . . . . . . . . . 13
β’ ((πΉ βΎ (-β(,)π΅)) limβ π΅) β
β |
6 | | limclner.l |
. . . . . . . . . . . . 13
β’ (π β πΏ β ((πΉ βΎ (-β(,)π΅)) limβ π΅)) |
7 | 5, 6 | sselid 3946 |
. . . . . . . . . . . 12
β’ (π β πΏ β β) |
8 | 7 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β) β§ βπ¦ β β+
βπ§ β
β+ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β πΏ β β) |
9 | 4, 8 | subcld 11520 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β) β§ βπ¦ β β+
βπ§ β
β+ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β (π
β πΏ) β β) |
10 | | limclner.lner |
. . . . . . . . . . . . 13
β’ (π β πΏ β π
) |
11 | 10 | necomd 2996 |
. . . . . . . . . . . 12
β’ (π β π
β πΏ) |
12 | 11 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β) β§ βπ¦ β β+
βπ§ β
β+ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β π
β πΏ) |
13 | 4, 8, 12 | subne0d 11529 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β) β§ βπ¦ β β+
βπ§ β
β+ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β (π
β πΏ) β 0) |
14 | 9, 13 | absrpcld 15342 |
. . . . . . . . 9
β’ (((π β§ π₯ β β) β§ βπ¦ β β+
βπ§ β
β+ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β (absβ(π
β πΏ)) β
β+) |
15 | | 4re 12245 |
. . . . . . . . . . 11
β’ 4 β
β |
16 | | 4pos 12268 |
. . . . . . . . . . 11
β’ 0 <
4 |
17 | 15, 16 | elrpii 12926 |
. . . . . . . . . 10
β’ 4 β
β+ |
18 | 17 | a1i 11 |
. . . . . . . . 9
β’ (((π β§ π₯ β β) β§ βπ¦ β β+
βπ§ β
β+ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β 4 β
β+) |
19 | 14, 18 | rpdivcld 12982 |
. . . . . . . 8
β’ (((π β§ π₯ β β) β§ βπ¦ β β+
βπ§ β
β+ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β ((absβ(π
β πΏ)) / 4) β
β+) |
20 | | nfv 1918 |
. . . . . . . . . . 11
β’
β²π¦(π β§ π₯ β β) |
21 | | nfra1 3266 |
. . . . . . . . . . 11
β’
β²π¦βπ¦ β β+ βπ§ β β+
βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦) |
22 | 20, 21 | nfan 1903 |
. . . . . . . . . 10
β’
β²π¦((π β§ π₯ β β) β§ βπ¦ β β+
βπ§ β
β+ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) |
23 | | nfv 1918 |
. . . . . . . . . 10
β’
β²π¦(((absβ(π
β πΏ)) / 4) β β+ β
βπ β π΄ βπ β π΄ (absβ(π
β πΏ)) < (4 Β· ((absβ(π
β πΏ)) / 4))) |
24 | 22, 23 | nfim 1900 |
. . . . . . . . 9
β’
β²π¦(((π β§ π₯ β β) β§ βπ¦ β β+
βπ§ β
β+ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β (((absβ(π
β πΏ)) / 4) β β+ β
βπ β π΄ βπ β π΄ (absβ(π
β πΏ)) < (4 Β· ((absβ(π
β πΏ)) / 4)))) |
25 | | ovex 7394 |
. . . . . . . . 9
β’
((absβ(π
β πΏ)) / 4) β
V |
26 | | eleq1 2822 |
. . . . . . . . . . 11
β’ (π¦ = ((absβ(π
β πΏ)) / 4) β (π¦ β β+ β
((absβ(π
β
πΏ)) / 4) β
β+)) |
27 | | oveq2 7369 |
. . . . . . . . . . . . 13
β’ (π¦ = ((absβ(π
β πΏ)) / 4) β (4 Β· π¦) = (4 Β·
((absβ(π
β
πΏ)) / 4))) |
28 | 27 | breq2d 5121 |
. . . . . . . . . . . 12
β’ (π¦ = ((absβ(π
β πΏ)) / 4) β ((absβ(π
β πΏ)) < (4 Β· π¦) β (absβ(π
β πΏ)) < (4 Β· ((absβ(π
β πΏ)) / 4)))) |
29 | 28 | 2rexbidv 3210 |
. . . . . . . . . . 11
β’ (π¦ = ((absβ(π
β πΏ)) / 4) β (βπ β π΄ βπ β π΄ (absβ(π
β πΏ)) < (4 Β· π¦) β βπ β π΄ βπ β π΄ (absβ(π
β πΏ)) < (4 Β· ((absβ(π
β πΏ)) / 4)))) |
30 | 26, 29 | imbi12d 345 |
. . . . . . . . . 10
β’ (π¦ = ((absβ(π
β πΏ)) / 4) β ((π¦ β β+ β
βπ β π΄ βπ β π΄ (absβ(π
β πΏ)) < (4 Β· π¦)) β (((absβ(π
β πΏ)) / 4) β β+ β
βπ β π΄ βπ β π΄ (absβ(π
β πΏ)) < (4 Β· ((absβ(π
β πΏ)) / 4))))) |
31 | 30 | imbi2d 341 |
. . . . . . . . 9
β’ (π¦ = ((absβ(π
β πΏ)) / 4) β ((((π β§ π₯ β β) β§ βπ¦ β β+
βπ§ β
β+ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β (π¦ β β+ β
βπ β π΄ βπ β π΄ (absβ(π
β πΏ)) < (4 Β· π¦))) β (((π β§ π₯ β β) β§ βπ¦ β β+
βπ§ β
β+ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β (((absβ(π
β πΏ)) / 4) β β+ β
βπ β π΄ βπ β π΄ (absβ(π
β πΏ)) < (4 Β· ((absβ(π
β πΏ)) / 4)))))) |
32 | | simpll 766 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β β) β§ βπ¦ β β+
βπ§ β
β+ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β§ π¦ β β+) β (π β§ π₯ β β)) |
33 | | simpr 486 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β β) β§ βπ¦ β β+
βπ§ β
β+ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β§ π¦ β β+) β π¦ β
β+) |
34 | | rspa 3230 |
. . . . . . . . . . . 12
β’
((βπ¦ β
β+ βπ§ β β+ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦) β§ π¦ β β+) β
βπ§ β
β+ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) |
35 | 34 | adantll 713 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β β) β§ βπ¦ β β+
βπ§ β
β+ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β§ π¦ β β+) β
βπ§ β
β+ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) |
36 | | limclner.f |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β πΉ:π΄βΆβ) |
37 | | fresin 6715 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (πΉ:π΄βΆβ β (πΉ βΎ (π΅(,)+β)):(π΄ β© (π΅(,)+β))βΆβ) |
38 | 36, 37 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (πΉ βΎ (π΅(,)+β)):(π΄ β© (π΅(,)+β))βΆβ) |
39 | | inss2 4193 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π΄ β© (π΅(,)+β)) β (π΅(,)+β) |
40 | | ioosscn 13335 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π΅(,)+β) β
β |
41 | 39, 40 | sstri 3957 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π΄ β© (π΅(,)+β)) β
β |
42 | 41 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (π΄ β© (π΅(,)+β)) β
β) |
43 | | limclner.j |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ π½ = (topGenβran
(,)) |
44 | | retop 24148 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
(topGenβran (,)) β Top |
45 | 43, 44 | eqeltri 2830 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ π½ β Top |
46 | | inss2 4193 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π΄ β© (-β(,)π΅)) β (-β(,)π΅) |
47 | | ioossre 13334 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
(-β(,)π΅)
β β |
48 | 46, 47 | sstri 3957 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π΄ β© (-β(,)π΅)) β
β |
49 | | uniretop 24149 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ β =
βͺ (topGenβran (,)) |
50 | 43 | unieqi 4882 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ βͺ π½ =
βͺ (topGenβran (,)) |
51 | 49, 50 | eqtr4i 2764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ β =
βͺ π½ |
52 | 51 | lpss 22516 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π½ β Top β§ (π΄ β© (-β(,)π΅)) β β) β
((limPtβπ½)β(π΄ β© (-β(,)π΅))) β β) |
53 | 45, 48, 52 | mp2an 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((limPtβπ½)β(π΄ β© (-β(,)π΅))) β β |
54 | | limclner.blp1 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β π΅ β ((limPtβπ½)β(π΄ β© (-β(,)π΅)))) |
55 | 53, 54 | sselid 3946 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β π΅ β β) |
56 | 55 | recnd 11191 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β π΅ β β) |
57 | 38, 42, 56 | ellimc3 25266 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (π
β ((πΉ βΎ (π΅(,)+β)) limβ π΅) β (π
β β β§ βπ¦ β β+
βπ£ β
β+ βπ€ β (π΄ β© (π΅(,)+β))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (π΅(,)+β))βπ€) β π
)) < π¦)))) |
58 | 2, 57 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (π
β β β§ βπ¦ β β+
βπ£ β
β+ βπ€ β (π΄ β© (π΅(,)+β))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (π΅(,)+β))βπ€) β π
)) < π¦))) |
59 | 58 | simprd 497 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β βπ¦ β β+ βπ£ β β+
βπ€ β (π΄ β© (π΅(,)+β))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (π΅(,)+β))βπ€) β π
)) < π¦)) |
60 | 59 | r19.21bi 3233 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π¦ β β+) β
βπ£ β
β+ βπ€ β (π΄ β© (π΅(,)+β))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (π΅(,)+β))βπ€) β π
)) < π¦)) |
61 | 60 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π¦ β β+) β§ π§ β β+
β§ βπ€ β
π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β βπ£ β β+ βπ€ β (π΄ β© (π΅(,)+β))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (π΅(,)+β))βπ€) β π
)) < π¦)) |
62 | | simp11l 1285 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π¦ β β+) β§ π§ β β+
β§ βπ€ β
π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β§ π£ β β+ β§
βπ€ β (π΄ β© (π΅(,)+β))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (π΅(,)+β))βπ€) β π
)) < π¦)) β π) |
63 | | simp12 1205 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π¦ β β+) β§ π§ β β+
β§ βπ€ β
π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β§ π£ β β+ β§
βπ€ β (π΄ β© (π΅(,)+β))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (π΅(,)+β))βπ€) β π
)) < π¦)) β π§ β β+) |
64 | | simp2 1138 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π¦ β β+) β§ π§ β β+
β§ βπ€ β
π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β§ π£ β β+ β§
βπ€ β (π΄ β© (π΅(,)+β))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (π΅(,)+β))βπ€) β π
)) < π¦)) β π£ β β+) |
65 | | breq2 5113 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π’ = if(π§ β€ π£, π§, π£) β ((absβ(π β π΅)) < π’ β (absβ(π β π΅)) < if(π§ β€ π£, π§, π£))) |
66 | 65 | rexbidv 3172 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π’ = if(π§ β€ π£, π§, π£) β (βπ β ((π΄ β© (π΅(,)+β)) β {π΅})(absβ(π β π΅)) < π’ β βπ β ((π΄ β© (π΅(,)+β)) β {π΅})(absβ(π β π΅)) < if(π§ β€ π£, π§, π£))) |
67 | | inss1 4192 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
(((limPtβπΎ)β(π΄ β© (π΅(,)+β))) β© β) β
((limPtβπΎ)β(π΄ β© (π΅(,)+β))) |
68 | 67 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β (((limPtβπΎ)β(π΄ β© (π΅(,)+β))) β© β) β
((limPtβπΎ)β(π΄ β© (π΅(,)+β)))) |
69 | | limclner.k |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ πΎ =
(TopOpenββfld) |
70 | 69 | cnfldtop 24170 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ πΎ β Top |
71 | 70 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π β πΎ β Top) |
72 | | ax-resscn 11116 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ β
β β |
73 | 72 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π β β β
β) |
74 | | ioossre 13334 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π΅(,)+β) β
β |
75 | 39, 74 | sstri 3957 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π΄ β© (π΅(,)+β)) β
β |
76 | 75 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π β (π΄ β© (π΅(,)+β)) β
β) |
77 | | unicntop 24172 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ β =
βͺ
(TopOpenββfld) |
78 | 69 | unieqi 4882 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ βͺ πΎ =
βͺ
(TopOpenββfld) |
79 | 77, 78 | eqtr4i 2764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ β =
βͺ πΎ |
80 | 69 | tgioo2 24189 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’
(topGenβran (,)) = (πΎ βΎt
β) |
81 | 43, 80 | eqtri 2761 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ π½ = (πΎ βΎt
β) |
82 | 79, 81 | restlp 22557 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((πΎ β Top β§ β
β β β§ (π΄
β© (π΅(,)+β))
β β) β ((limPtβπ½)β(π΄ β© (π΅(,)+β))) = (((limPtβπΎ)β(π΄ β© (π΅(,)+β))) β©
β)) |
83 | 71, 73, 76, 82 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β ((limPtβπ½)β(π΄ β© (π΅(,)+β))) = (((limPtβπΎ)β(π΄ β© (π΅(,)+β))) β©
β)) |
84 | 69 | eqcomi 2742 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’
(TopOpenββfld) = πΎ |
85 | 84 | fveq2i 6849 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’
(limPtβ(TopOpenββfld)) = (limPtβπΎ) |
86 | 85 | fveq1i 6847 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
((limPtβ(TopOpenββfld))β(π΄ β© (π΅(,)+β))) = ((limPtβπΎ)β(π΄ β© (π΅(,)+β))) |
87 | 86 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β
((limPtβ(TopOpenββfld))β(π΄ β© (π΅(,)+β))) = ((limPtβπΎ)β(π΄ β© (π΅(,)+β)))) |
88 | 68, 83, 87 | 3sstr4d 3995 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β ((limPtβπ½)β(π΄ β© (π΅(,)+β))) β
((limPtβ(TopOpenββfld))β(π΄ β© (π΅(,)+β)))) |
89 | | limclner.blp2 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β π΅ β ((limPtβπ½)β(π΄ β© (π΅(,)+β)))) |
90 | 88, 89 | sseldd 3949 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β π΅ β
((limPtβ(TopOpenββfld))β(π΄ β© (π΅(,)+β)))) |
91 | 42, 56 | islpcn 43970 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β (π΅ β
((limPtβ(TopOpenββfld))β(π΄ β© (π΅(,)+β))) β βπ’ β β+
βπ β ((π΄ β© (π΅(,)+β)) β {π΅})(absβ(π β π΅)) < π’)) |
92 | 90, 91 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β βπ’ β β+ βπ β ((π΄ β© (π΅(,)+β)) β {π΅})(absβ(π β π΅)) < π’) |
93 | 92 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π§ β β+ β§ π£ β β+)
β βπ’ β
β+ βπ β ((π΄ β© (π΅(,)+β)) β {π΅})(absβ(π β π΅)) < π’) |
94 | | ifcl 4535 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π§ β β+
β§ π£ β
β+) β if(π§ β€ π£, π§, π£) β
β+) |
95 | 94 | 3adant1 1131 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π§ β β+ β§ π£ β β+)
β if(π§ β€ π£, π§, π£) β
β+) |
96 | 66, 93, 95 | rspcdva 3584 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π§ β β+ β§ π£ β β+)
β βπ β
((π΄ β© (π΅(,)+β)) β {π΅})(absβ(π β π΅)) < if(π§ β€ π£, π§, π£)) |
97 | | eldifi 4090 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β ((π΄ β© (π΅(,)+β)) β {π΅}) β π β (π΄ β© (π΅(,)+β))) |
98 | 75, 97 | sselid 3946 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β ((π΄ β© (π΅(,)+β)) β {π΅}) β π β β) |
99 | 73 | sselda 3948 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((π β§ π β β) β π β β) |
100 | 56 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((π β§ π β β) β π΅ β β) |
101 | 99, 100 | subcld 11520 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π β§ π β β) β (π β π΅) β β) |
102 | 101 | abscld 15330 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π β§ π β β) β (absβ(π β π΅)) β β) |
103 | 102 | 3ad2antl1 1186 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π β§ π§ β β+ β§ π£ β β+)
β§ π β β)
β (absβ(π
β π΅)) β
β) |
104 | 103 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β§ π§ β β+ β§ π£ β β+)
β§ π β β)
β§ (absβ(π β
π΅)) < if(π§ β€ π£, π§, π£)) β (absβ(π β π΅)) β β) |
105 | 95 | rpred 12965 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β§ π§ β β+ β§ π£ β β+)
β if(π§ β€ π£, π§, π£) β β) |
106 | 105 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β§ π§ β β+ β§ π£ β β+)
β§ π β β)
β§ (absβ(π β
π΅)) < if(π§ β€ π£, π§, π£)) β if(π§ β€ π£, π§, π£) β β) |
107 | | rpre 12931 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π§ β β+
β π§ β
β) |
108 | 107 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β§ π§ β β+ β§ π£ β β+)
β π§ β
β) |
109 | 108 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β§ π§ β β+ β§ π£ β β+)
β§ π β β)
β§ (absβ(π β
π΅)) < if(π§ β€ π£, π§, π£)) β π§ β β) |
110 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β§ π§ β β+ β§ π£ β β+)
β§ π β β)
β§ (absβ(π β
π΅)) < if(π§ β€ π£, π§, π£)) β (absβ(π β π΅)) < if(π§ β€ π£, π§, π£)) |
111 | | rpre 12931 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π£ β β+
β π£ β
β) |
112 | | min1 13117 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π§ β β β§ π£ β β) β if(π§ β€ π£, π§, π£) β€ π§) |
113 | 107, 111,
112 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π§ β β+
β§ π£ β
β+) β if(π§ β€ π£, π§, π£) β€ π§) |
114 | 113 | 3adant1 1131 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β§ π§ β β+ β§ π£ β β+)
β if(π§ β€ π£, π§, π£) β€ π§) |
115 | 114 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β§ π§ β β+ β§ π£ β β+)
β§ π β β)
β§ (absβ(π β
π΅)) < if(π§ β€ π£, π§, π£)) β if(π§ β€ π£, π§, π£) β€ π§) |
116 | 104, 106,
109, 110, 115 | ltletrd 11323 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β§ π§ β β+ β§ π£ β β+)
β§ π β β)
β§ (absβ(π β
π΅)) < if(π§ β€ π£, π§, π£)) β (absβ(π β π΅)) < π§) |
117 | 111 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β§ π§ β β+ β§ π£ β β+)
β π£ β
β) |
118 | 117 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β§ π§ β β+ β§ π£ β β+)
β§ π β β)
β§ (absβ(π β
π΅)) < if(π§ β€ π£, π§, π£)) β π£ β β) |
119 | 109, 118 | min2d 43798 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β§ π§ β β+ β§ π£ β β+)
β§ π β β)
β§ (absβ(π β
π΅)) < if(π§ β€ π£, π§, π£)) β if(π§ β€ π£, π§, π£) β€ π£) |
120 | 104, 106,
118, 110, 119 | ltletrd 11323 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β§ π§ β β+ β§ π£ β β+)
β§ π β β)
β§ (absβ(π β
π΅)) < if(π§ β€ π£, π§, π£)) β (absβ(π β π΅)) < π£) |
121 | 116, 120 | jca 513 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ π§ β β+ β§ π£ β β+)
β§ π β β)
β§ (absβ(π β
π΅)) < if(π§ β€ π£, π§, π£)) β ((absβ(π β π΅)) < π§ β§ (absβ(π β π΅)) < π£)) |
122 | 121 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π§ β β+ β§ π£ β β+)
β§ π β β)
β ((absβ(π
β π΅)) < if(π§ β€ π£, π§, π£) β ((absβ(π β π΅)) < π§ β§ (absβ(π β π΅)) < π£))) |
123 | 98, 122 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π§ β β+ β§ π£ β β+)
β§ π β ((π΄ β© (π΅(,)+β)) β {π΅})) β ((absβ(π β π΅)) < if(π§ β€ π£, π§, π£) β ((absβ(π β π΅)) < π§ β§ (absβ(π β π΅)) < π£))) |
124 | 123 | reximdva 3162 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π§ β β+ β§ π£ β β+)
β (βπ β
((π΄ β© (π΅(,)+β)) β {π΅})(absβ(π β π΅)) < if(π§ β€ π£, π§, π£) β βπ β ((π΄ β© (π΅(,)+β)) β {π΅})((absβ(π β π΅)) < π§ β§ (absβ(π β π΅)) < π£))) |
125 | 96, 124 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π§ β β+ β§ π£ β β+)
β βπ β
((π΄ β© (π΅(,)+β)) β {π΅})((absβ(π β π΅)) < π§ β§ (absβ(π β π΅)) < π£)) |
126 | 62, 63, 64, 125 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π¦ β β+) β§ π§ β β+
β§ βπ€ β
π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β§ π£ β β+ β§
βπ€ β (π΄ β© (π΅(,)+β))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (π΅(,)+β))βπ€) β π
)) < π¦)) β βπ β ((π΄ β© (π΅(,)+β)) β {π΅})((absβ(π β π΅)) < π§ β§ (absβ(π β π΅)) < π£)) |
127 | | nfv 1918 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
β²π(((π β§ π¦ β β+) β§ π§ β β+
β§ βπ€ β
π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β§ π£ β β+ β§
βπ€ β (π΄ β© (π΅(,)+β))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (π΅(,)+β))βπ€) β π
)) < π¦)) |
128 | | nfre1 3267 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
β²πβπ β π΄ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β π
)) < π¦) |
129 | 97 | elin1d 4162 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β ((π΄ β© (π΅(,)+β)) β {π΅}) β π β π΄) |
130 | 129 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β§ π¦ β β+)
β§ π§ β
β+ β§ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β§ π£ β β+ β§
βπ€ β (π΄ β© (π΅(,)+β))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (π΅(,)+β))βπ€) β π
)) < π¦)) β§ π β ((π΄ β© (π΅(,)+β)) β {π΅}) β§ ((absβ(π β π΅)) < π§ β§ (absβ(π β π΅)) < π£)) β π β π΄) |
131 | | simp113 1305 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((π β§ π¦ β β+)
β§ π§ β
β+ β§ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β§ π£ β β+ β§
βπ€ β (π΄ β© (π΅(,)+β))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (π΅(,)+β))βπ€) β π
)) < π¦)) β§ π β ((π΄ β© (π΅(,)+β)) β {π΅}) β§ ((absβ(π β π΅)) < π§ β§ (absβ(π β π΅)) < π£)) β βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) |
132 | | eldifsni 4754 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β ((π΄ β© (π΅(,)+β)) β {π΅}) β π β π΅) |
133 | 132 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β ((π΄ β© (π΅(,)+β)) β {π΅}) β§ ((absβ(π β π΅)) < π§ β§ (absβ(π β π΅)) < π£)) β π β π΅) |
134 | | simprl 770 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β ((π΄ β© (π΅(,)+β)) β {π΅}) β§ ((absβ(π β π΅)) < π§ β§ (absβ(π β π΅)) < π£)) β (absβ(π β π΅)) < π§) |
135 | 133, 134 | jca 513 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β ((π΄ β© (π΅(,)+β)) β {π΅}) β§ ((absβ(π β π΅)) < π§ β§ (absβ(π β π΅)) < π£)) β (π β π΅ β§ (absβ(π β π΅)) < π§)) |
136 | 135 | 3adant1 1131 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((π β§ π¦ β β+)
β§ π§ β
β+ β§ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β§ π£ β β+ β§
βπ€ β (π΄ β© (π΅(,)+β))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (π΅(,)+β))βπ€) β π
)) < π¦)) β§ π β ((π΄ β© (π΅(,)+β)) β {π΅}) β§ ((absβ(π β π΅)) < π§ β§ (absβ(π β π΅)) < π£)) β (π β π΅ β§ (absβ(π β π΅)) < π§)) |
137 | | neeq1 3003 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π€ = π β (π€ β π΅ β π β π΅)) |
138 | | fvoveq1 7384 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π€ = π β (absβ(π€ β π΅)) = (absβ(π β π΅))) |
139 | 138 | breq1d 5119 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π€ = π β ((absβ(π€ β π΅)) < π§ β (absβ(π β π΅)) < π§)) |
140 | 137, 139 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π€ = π β ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (π β π΅ β§ (absβ(π β π΅)) < π§))) |
141 | 140 | imbrov2fvoveq 7386 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π€ = π β (((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦) β ((π β π΅ β§ (absβ(π β π΅)) < π§) β (absβ((πΉβπ) β π₯)) < π¦))) |
142 | 141 | rspcva 3581 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β π΄ β§ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β ((π β π΅ β§ (absβ(π β π΅)) < π§) β (absβ((πΉβπ) β π₯)) < π¦)) |
143 | 142 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β π΄ β§ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β§ (π β π΅ β§ (absβ(π β π΅)) < π§)) β (absβ((πΉβπ) β π₯)) < π¦) |
144 | 130, 131,
136, 143 | syl21anc 837 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β§ π¦ β β+)
β§ π§ β
β+ β§ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β§ π£ β β+ β§
βπ€ β (π΄ β© (π΅(,)+β))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (π΅(,)+β))βπ€) β π
)) < π¦)) β§ π β ((π΄ β© (π΅(,)+β)) β {π΅}) β§ ((absβ(π β π΅)) < π§ β§ (absβ(π β π΅)) < π£)) β (absβ((πΉβπ) β π₯)) < π¦) |
145 | 97 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((π β§ π¦ β β+)
β§ π§ β
β+ β§ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β§ π£ β β+ β§
βπ€ β (π΄ β© (π΅(,)+β))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (π΅(,)+β))βπ€) β π
)) < π¦)) β§ π β ((π΄ β© (π΅(,)+β)) β {π΅}) β§ ((absβ(π β π΅)) < π§ β§ (absβ(π β π΅)) < π£)) β π β (π΄ β© (π΅(,)+β))) |
146 | 62 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((((π β§ π¦ β β+)
β§ π§ β
β+ β§ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β§ π£ β β+ β§
βπ€ β (π΄ β© (π΅(,)+β))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (π΅(,)+β))βπ€) β π
)) < π¦)) β§ π β ((π΄ β© (π΅(,)+β)) β {π΅}) β§ ((absβ(π β π΅)) < π§ β§ (absβ(π β π΅)) < π£)) β π) |
147 | | simp13 1206 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((((π β§ π¦ β β+)
β§ π§ β
β+ β§ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β§ π£ β β+ β§
βπ€ β (π΄ β© (π΅(,)+β))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (π΅(,)+β))βπ€) β π
)) < π¦)) β§ π β ((π΄ β© (π΅(,)+β)) β {π΅}) β§ ((absβ(π β π΅)) < π§ β§ (absβ(π β π΅)) < π£)) β βπ€ β (π΄ β© (π΅(,)+β))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (π΅(,)+β))βπ€) β π
)) < π¦)) |
148 | | nfv 1918 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
β²π€π |
149 | | nfra1 3266 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
β²π€βπ€ β (π΄ β© (π΅(,)+β))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (π΅(,)+β))βπ€) β π
)) < π¦) |
150 | 148, 149 | nfan 1903 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
β²π€(π β§ βπ€ β (π΄ β© (π΅(,)+β))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (π΅(,)+β))βπ€) β π
)) < π¦)) |
151 | | elinel2 4160 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π€ β (π΄ β© (π΅(,)+β)) β π€ β (π΅(,)+β)) |
152 | 151 | fvresd 6866 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π€ β (π΄ β© (π΅(,)+β)) β ((πΉ βΎ (π΅(,)+β))βπ€) = (πΉβπ€)) |
153 | 152 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π€ β (π΄ β© (π΅(,)+β)) β (πΉβπ€) = ((πΉ βΎ (π΅(,)+β))βπ€)) |
154 | 153 | fvoveq1d 7383 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π€ β (π΄ β© (π΅(,)+β)) β (absβ((πΉβπ€) β π
)) = (absβ(((πΉ βΎ (π΅(,)+β))βπ€) β π
))) |
155 | 154 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π β§ βπ€ β (π΄ β© (π΅(,)+β))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (π΅(,)+β))βπ€) β π
)) < π¦)) β§ π€ β (π΄ β© (π΅(,)+β)) β§ (π€ β π΅ β§ (absβ(π€ β π΅)) < π£)) β (absβ((πΉβπ€) β π
)) = (absβ(((πΉ βΎ (π΅(,)+β))βπ€) β π
))) |
156 | | rspa 3230 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’
((βπ€ β
(π΄ β© (π΅(,)+β))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (π΅(,)+β))βπ€) β π
)) < π¦) β§ π€ β (π΄ β© (π΅(,)+β))) β ((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (π΅(,)+β))βπ€) β π
)) < π¦)) |
157 | 156 | 3impia 1118 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’
((βπ€ β
(π΄ β© (π΅(,)+β))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (π΅(,)+β))βπ€) β π
)) < π¦) β§ π€ β (π΄ β© (π΅(,)+β)) β§ (π€ β π΅ β§ (absβ(π€ β π΅)) < π£)) β (absβ(((πΉ βΎ (π΅(,)+β))βπ€) β π
)) < π¦) |
158 | 157 | 3adant1l 1177 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π β§ βπ€ β (π΄ β© (π΅(,)+β))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (π΅(,)+β))βπ€) β π
)) < π¦)) β§ π€ β (π΄ β© (π΅(,)+β)) β§ (π€ β π΅ β§ (absβ(π€ β π΅)) < π£)) β (absβ(((πΉ βΎ (π΅(,)+β))βπ€) β π
)) < π¦) |
159 | 155, 158 | eqbrtrd 5131 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β§ βπ€ β (π΄ β© (π΅(,)+β))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (π΅(,)+β))βπ€) β π
)) < π¦)) β§ π€ β (π΄ β© (π΅(,)+β)) β§ (π€ β π΅ β§ (absβ(π€ β π΅)) < π£)) β (absβ((πΉβπ€) β π
)) < π¦) |
160 | 159 | 3exp 1120 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ βπ€ β (π΄ β© (π΅(,)+β))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (π΅(,)+β))βπ€) β π
)) < π¦)) β (π€ β (π΄ β© (π΅(,)+β)) β ((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ((πΉβπ€) β π
)) < π¦))) |
161 | 150, 160 | ralrimi 3239 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ βπ€ β (π΄ β© (π΅(,)+β))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (π΅(,)+β))βπ€) β π
)) < π¦)) β βπ€ β (π΄ β© (π΅(,)+β))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ((πΉβπ€) β π
)) < π¦)) |
162 | 146, 147,
161 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((π β§ π¦ β β+)
β§ π§ β
β+ β§ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β§ π£ β β+ β§
βπ€ β (π΄ β© (π΅(,)+β))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (π΅(,)+β))βπ€) β π
)) < π¦)) β§ π β ((π΄ β© (π΅(,)+β)) β {π΅}) β§ ((absβ(π β π΅)) < π§ β§ (absβ(π β π΅)) < π£)) β βπ€ β (π΄ β© (π΅(,)+β))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ((πΉβπ€) β π
)) < π¦)) |
163 | 132 | anim1i 616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β ((π΄ β© (π΅(,)+β)) β {π΅}) β§ (absβ(π β π΅)) < π£) β (π β π΅ β§ (absβ(π β π΅)) < π£)) |
164 | 163 | adantrl 715 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β ((π΄ β© (π΅(,)+β)) β {π΅}) β§ ((absβ(π β π΅)) < π§ β§ (absβ(π β π΅)) < π£)) β (π β π΅ β§ (absβ(π β π΅)) < π£)) |
165 | 164 | 3adant1 1131 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((π β§ π¦ β β+)
β§ π§ β
β+ β§ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β§ π£ β β+ β§
βπ€ β (π΄ β© (π΅(,)+β))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (π΅(,)+β))βπ€) β π
)) < π¦)) β§ π β ((π΄ β© (π΅(,)+β)) β {π΅}) β§ ((absβ(π β π΅)) < π§ β§ (absβ(π β π΅)) < π£)) β (π β π΅ β§ (absβ(π β π΅)) < π£)) |
166 | 138 | breq1d 5119 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π€ = π β ((absβ(π€ β π΅)) < π£ β (absβ(π β π΅)) < π£)) |
167 | 137, 166 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π€ = π β ((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (π β π΅ β§ (absβ(π β π΅)) < π£))) |
168 | 167 | imbrov2fvoveq 7386 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π€ = π β (((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ((πΉβπ€) β π
)) < π¦) β ((π β π΅ β§ (absβ(π β π΅)) < π£) β (absβ((πΉβπ) β π
)) < π¦))) |
169 | 168 | rspcva 3581 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β (π΄ β© (π΅(,)+β)) β§ βπ€ β (π΄ β© (π΅(,)+β))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ((πΉβπ€) β π
)) < π¦)) β ((π β π΅ β§ (absβ(π β π΅)) < π£) β (absβ((πΉβπ) β π
)) < π¦)) |
170 | 169 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β (π΄ β© (π΅(,)+β)) β§ βπ€ β (π΄ β© (π΅(,)+β))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ((πΉβπ€) β π
)) < π¦)) β§ (π β π΅ β§ (absβ(π β π΅)) < π£)) β (absβ((πΉβπ) β π
)) < π¦) |
171 | 145, 162,
165, 170 | syl21anc 837 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β§ π¦ β β+)
β§ π§ β
β+ β§ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β§ π£ β β+ β§
βπ€ β (π΄ β© (π΅(,)+β))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (π΅(,)+β))βπ€) β π
)) < π¦)) β§ π β ((π΄ β© (π΅(,)+β)) β {π΅}) β§ ((absβ(π β π΅)) < π§ β§ (absβ(π β π΅)) < π£)) β (absβ((πΉβπ) β π
)) < π¦) |
172 | | rspe 3231 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β π΄ β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β π
)) < π¦)) β βπ β π΄ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β π
)) < π¦)) |
173 | 130, 144,
171, 172 | syl12anc 836 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π β§ π¦ β β+)
β§ π§ β
β+ β§ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β§ π£ β β+ β§
βπ€ β (π΄ β© (π΅(,)+β))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (π΅(,)+β))βπ€) β π
)) < π¦)) β§ π β ((π΄ β© (π΅(,)+β)) β {π΅}) β§ ((absβ(π β π΅)) < π§ β§ (absβ(π β π΅)) < π£)) β βπ β π΄ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β π
)) < π¦)) |
174 | 173 | 3exp 1120 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π¦ β β+) β§ π§ β β+
β§ βπ€ β
π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β§ π£ β β+ β§
βπ€ β (π΄ β© (π΅(,)+β))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (π΅(,)+β))βπ€) β π
)) < π¦)) β (π β ((π΄ β© (π΅(,)+β)) β {π΅}) β (((absβ(π β π΅)) < π§ β§ (absβ(π β π΅)) < π£) β βπ β π΄ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β π
)) < π¦)))) |
175 | 127, 128,
174 | rexlimd 3248 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π¦ β β+) β§ π§ β β+
β§ βπ€ β
π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β§ π£ β β+ β§
βπ€ β (π΄ β© (π΅(,)+β))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (π΅(,)+β))βπ€) β π
)) < π¦)) β (βπ β ((π΄ β© (π΅(,)+β)) β {π΅})((absβ(π β π΅)) < π§ β§ (absβ(π β π΅)) < π£) β βπ β π΄ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β π
)) < π¦))) |
176 | 126, 175 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π¦ β β+) β§ π§ β β+
β§ βπ€ β
π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β§ π£ β β+ β§
βπ€ β (π΄ β© (π΅(,)+β))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (π΅(,)+β))βπ€) β π
)) < π¦)) β βπ β π΄ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β π
)) < π¦)) |
177 | 176 | 3exp 1120 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π¦ β β+) β§ π§ β β+
β§ βπ€ β
π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β (π£ β β+ β
(βπ€ β (π΄ β© (π΅(,)+β))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (π΅(,)+β))βπ€) β π
)) < π¦) β βπ β π΄ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β π
)) < π¦)))) |
178 | 177 | rexlimdv 3147 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π¦ β β+) β§ π§ β β+
β§ βπ€ β
π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β (βπ£ β β+ βπ€ β (π΄ β© (π΅(,)+β))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (π΅(,)+β))βπ€) β π
)) < π¦) β βπ β π΄ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β π
)) < π¦))) |
179 | 61, 178 | mpd 15 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π¦ β β+) β§ π§ β β+
β§ βπ€ β
π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β βπ β π΄ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β π
)) < π¦)) |
180 | 179 | 3exp 1120 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π¦ β β+) β (π§ β β+
β (βπ€ β
π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦) β βπ β π΄ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β π
)) < π¦)))) |
181 | 180 | rexlimdv 3147 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π¦ β β+) β
(βπ§ β
β+ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦) β βπ β π΄ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β π
)) < π¦))) |
182 | 181 | imp 408 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π¦ β β+) β§
βπ§ β
β+ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β βπ β π΄ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β π
)) < π¦)) |
183 | 182 | adantllr 718 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π₯ β β) β§ π¦ β β+) β§
βπ§ β
β+ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β βπ β π΄ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β π
)) < π¦)) |
184 | 183 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’
((((((π β§ π₯ β β) β§ π¦ β β+)
β§ βπ§ β
β+ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦)) β βπ β π΄ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β π
)) < π¦)) |
185 | 3 | ad6antr 735 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((((π β§ π₯ β β) β§ π¦ β β+)
β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦)) β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β π
)) < π¦)) β π
β β) |
186 | 7 | ad6antr 735 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((((π β§ π₯ β β) β§ π¦ β β+)
β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦)) β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β π
)) < π¦)) β πΏ β β) |
187 | 185, 186 | subcld 11520 |
. . . . . . . . . . . . . . . . . 18
β’
(((((((π β§ π₯ β β) β§ π¦ β β+)
β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦)) β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β π
)) < π¦)) β (π
β πΏ) β β) |
188 | 187 | abscld 15330 |
. . . . . . . . . . . . . . . . 17
β’
(((((((π β§ π₯ β β) β§ π¦ β β+)
β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦)) β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β π
)) < π¦)) β (absβ(π
β πΏ)) β β) |
189 | | simp-6l 786 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((((π β§ π₯ β β) β§ π¦ β β+)
β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦)) β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β π
)) < π¦)) β π) |
190 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((((π β§ π₯ β β) β§ π¦ β β+)
β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦)) β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β π
)) < π¦)) β π β π΄) |
191 | 36 | ffvelcdmda 7039 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π β π΄) β (πΉβπ) β β) |
192 | 189, 190,
191 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((((π β§ π₯ β β) β§ π¦ β β+)
β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦)) β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β π
)) < π¦)) β (πΉβπ) β β) |
193 | 185, 192 | subcld 11520 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((((π β§ π₯ β β) β§ π¦ β β+)
β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦)) β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β π
)) < π¦)) β (π
β (πΉβπ)) β β) |
194 | 193 | abscld 15330 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((((π β§ π₯ β β) β§ π¦ β β+)
β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦)) β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β π
)) < π¦)) β (absβ(π
β (πΉβπ))) β β) |
195 | | simp-6r 787 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((((π β§ π₯ β β) β§ π¦ β β+)
β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦)) β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β π
)) < π¦)) β π₯ β β) |
196 | 192, 195 | subcld 11520 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((((π β§ π₯ β β) β§ π¦ β β+)
β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦)) β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β π
)) < π¦)) β ((πΉβπ) β π₯) β β) |
197 | 196 | abscld 15330 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((((π β§ π₯ β β) β§ π¦ β β+)
β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦)) β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β π
)) < π¦)) β (absβ((πΉβπ) β π₯)) β β) |
198 | 194, 197 | readdcld 11192 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((((π β§ π₯ β β) β§ π¦ β β+)
β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦)) β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β π
)) < π¦)) β ((absβ(π
β (πΉβπ))) + (absβ((πΉβπ) β π₯))) β β) |
199 | | simp-4r 783 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((((π β§ π₯ β β) β§ π¦ β β+)
β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦)) β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β π
)) < π¦)) β π β π΄) |
200 | 36 | ffvelcdmda 7039 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β π΄) β (πΉβπ) β β) |
201 | 189, 199,
200 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((((π β§ π₯ β β) β§ π¦ β β+)
β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦)) β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β π
)) < π¦)) β (πΉβπ) β β) |
202 | 195, 201 | subcld 11520 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((((π β§ π₯ β β) β§ π¦ β β+)
β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦)) β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β π
)) < π¦)) β (π₯ β (πΉβπ)) β β) |
203 | 202 | abscld 15330 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((((π β§ π₯ β β) β§ π¦ β β+)
β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦)) β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β π
)) < π¦)) β (absβ(π₯ β (πΉβπ))) β β) |
204 | 198, 203 | readdcld 11192 |
. . . . . . . . . . . . . . . . . 18
β’
(((((((π β§ π₯ β β) β§ π¦ β β+)
β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦)) β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β π
)) < π¦)) β (((absβ(π
β (πΉβπ))) + (absβ((πΉβπ) β π₯))) + (absβ(π₯ β (πΉβπ)))) β β) |
205 | 201, 186 | subcld 11520 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((((π β§ π₯ β β) β§ π¦ β β+)
β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦)) β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β π
)) < π¦)) β ((πΉβπ) β πΏ) β β) |
206 | 205 | abscld 15330 |
. . . . . . . . . . . . . . . . . 18
β’
(((((((π β§ π₯ β β) β§ π¦ β β+)
β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦)) β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β π
)) < π¦)) β (absβ((πΉβπ) β πΏ)) β β) |
207 | 204, 206 | readdcld 11192 |
. . . . . . . . . . . . . . . . 17
β’
(((((((π β§ π₯ β β) β§ π¦ β β+)
β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦)) β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β π
)) < π¦)) β ((((absβ(π
β (πΉβπ))) + (absβ((πΉβπ) β π₯))) + (absβ(π₯ β (πΉβπ)))) + (absβ((πΉβπ) β πΏ))) β β) |
208 | 15 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’
(((((((π β§ π₯ β β) β§ π¦ β β+)
β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦)) β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β π
)) < π¦)) β 4 β β) |
209 | | rpre 12931 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ β β+
β π¦ β
β) |
210 | 209 | ad5antlr 734 |
. . . . . . . . . . . . . . . . . 18
β’
(((((((π β§ π₯ β β) β§ π¦ β β+)
β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦)) β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β π
)) < π¦)) β π¦ β β) |
211 | 208, 210 | remulcld 11193 |
. . . . . . . . . . . . . . . . 17
β’
(((((((π β§ π₯ β β) β§ π¦ β β+)
β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦)) β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β π
)) < π¦)) β (4 Β· π¦) β β) |
212 | 185, 192,
195, 201, 186 | absnpncan3d 43632 |
. . . . . . . . . . . . . . . . 17
β’
(((((((π β§ π₯ β β) β§ π¦ β β+)
β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦)) β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β π
)) < π¦)) β (absβ(π
β πΏ)) β€ ((((absβ(π
β (πΉβπ))) + (absβ((πΉβπ) β π₯))) + (absβ(π₯ β (πΉβπ)))) + (absβ((πΉβπ) β πΏ)))) |
213 | 185, 192 | abssubd 15347 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((((π β§ π₯ β β) β§ π¦ β β+)
β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦)) β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β π
)) < π¦)) β (absβ(π
β (πΉβπ))) = (absβ((πΉβπ) β π
))) |
214 | | simprr 772 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((((π β§ π₯ β β) β§ π¦ β β+)
β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦)) β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β π
)) < π¦)) β (absβ((πΉβπ) β π
)) < π¦) |
215 | 213, 214 | eqbrtrd 5131 |
. . . . . . . . . . . . . . . . . 18
β’
(((((((π β§ π₯ β β) β§ π¦ β β+)
β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦)) β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β π
)) < π¦)) β (absβ(π
β (πΉβπ))) < π¦) |
216 | | simprl 770 |
. . . . . . . . . . . . . . . . . 18
β’
(((((((π β§ π₯ β β) β§ π¦ β β+)
β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦)) β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β π
)) < π¦)) β (absβ((πΉβπ) β π₯)) < π¦) |
217 | | simp-5r 785 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((π β§ π₯ β β) β§ π¦ β β+)
β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦)) β§ π β π΄) β π₯ β β) |
218 | 200 | ad5ant14 757 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π β§ π₯ β β) β§ π¦ β β+)
β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦)) β (πΉβπ) β β) |
219 | 218 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((π β§ π₯ β β) β§ π¦ β β+)
β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦)) β§ π β π΄) β (πΉβπ) β β) |
220 | 217, 219 | abssubd 15347 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π β§ π₯ β β) β§ π¦ β β+)
β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦)) β§ π β π΄) β (absβ(π₯ β (πΉβπ))) = (absβ((πΉβπ) β π₯))) |
221 | | simplrl 776 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π β§ π₯ β β) β§ π¦ β β+)
β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦)) β§ π β π΄) β (absβ((πΉβπ) β π₯)) < π¦) |
222 | 220, 221 | eqbrtrd 5131 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π β§ π₯ β β) β§ π¦ β β+)
β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦)) β§ π β π΄) β (absβ(π₯ β (πΉβπ))) < π¦) |
223 | 222 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’
(((((((π β§ π₯ β β) β§ π¦ β β+)
β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦)) β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β π
)) < π¦)) β (absβ(π₯ β (πΉβπ))) < π¦) |
224 | | simplrr 777 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π β§ π₯ β β) β§ π¦ β β+)
β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦)) β§ π β π΄) β (absβ((πΉβπ) β πΏ)) < π¦) |
225 | 224 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’
(((((((π β§ π₯ β β) β§ π¦ β β+)
β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦)) β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β π
)) < π¦)) β (absβ((πΉβπ) β πΏ)) < π¦) |
226 | 194, 197,
203, 206, 210, 215, 216, 223, 225 | lt4addmuld 43631 |
. . . . . . . . . . . . . . . . 17
β’
(((((((π β§ π₯ β β) β§ π¦ β β+)
β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦)) β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β π
)) < π¦)) β ((((absβ(π
β (πΉβπ))) + (absβ((πΉβπ) β π₯))) + (absβ(π₯ β (πΉβπ)))) + (absβ((πΉβπ) β πΏ))) < (4 Β· π¦)) |
227 | 188, 207,
211, 212, 226 | lelttrd 11321 |
. . . . . . . . . . . . . . . 16
β’
(((((((π β§ π₯ β β) β§ π¦ β β+)
β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦)) β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β π
)) < π¦)) β (absβ(π
β πΏ)) < (4 Β· π¦)) |
228 | 227 | ex 414 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ π₯ β β) β§ π¦ β β+)
β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦)) β§ π β π΄) β (((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β π
)) < π¦) β (absβ(π
β πΏ)) < (4 Β· π¦))) |
229 | 228 | adantl3r 749 |
. . . . . . . . . . . . . 14
β’
(((((((π β§ π₯ β β) β§ π¦ β β+)
β§ βπ§ β
β+ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦)) β§ π β π΄) β (((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β π
)) < π¦) β (absβ(π
β πΏ)) < (4 Β· π¦))) |
230 | 229 | reximdva 3162 |
. . . . . . . . . . . . 13
β’
((((((π β§ π₯ β β) β§ π¦ β β+)
β§ βπ§ β
β+ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦)) β (βπ β π΄ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β π
)) < π¦) β βπ β π΄ (absβ(π
β πΏ)) < (4 Β· π¦))) |
231 | 184, 230 | mpd 15 |
. . . . . . . . . . . 12
β’
((((((π β§ π₯ β β) β§ π¦ β β+)
β§ βπ§ β
β+ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β§ π β π΄) β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦)) β βπ β π΄ (absβ(π
β πΏ)) < (4 Β· π¦)) |
232 | | fresin 6715 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (πΉ:π΄βΆβ β (πΉ βΎ (-β(,)π΅)):(π΄ β© (-β(,)π΅))βΆβ) |
233 | 36, 232 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (πΉ βΎ (-β(,)π΅)):(π΄ β© (-β(,)π΅))βΆβ) |
234 | | ioosscn 13335 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(-β(,)π΅)
β β |
235 | 46, 234 | sstri 3957 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π΄ β© (-β(,)π΅)) β
β |
236 | 235 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (π΄ β© (-β(,)π΅)) β β) |
237 | 233, 236,
56 | ellimc3 25266 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (πΏ β ((πΉ βΎ (-β(,)π΅)) limβ π΅) β (πΏ β β β§ βπ¦ β β+
βπ£ β
β+ βπ€ β (π΄ β© (-β(,)π΅))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (-β(,)π΅))βπ€) β πΏ)) < π¦)))) |
238 | 6, 237 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (πΏ β β β§ βπ¦ β β+
βπ£ β
β+ βπ€ β (π΄ β© (-β(,)π΅))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (-β(,)π΅))βπ€) β πΏ)) < π¦))) |
239 | 238 | simprd 497 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β βπ¦ β β+ βπ£ β β+
βπ€ β (π΄ β© (-β(,)π΅))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (-β(,)π΅))βπ€) β πΏ)) < π¦)) |
240 | 239 | r19.21bi 3233 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π¦ β β+) β
βπ£ β
β+ βπ€ β (π΄ β© (-β(,)π΅))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (-β(,)π΅))βπ€) β πΏ)) < π¦)) |
241 | 240 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π¦ β β+) β§ π§ β β+
β§ βπ€ β
π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β βπ£ β β+ βπ€ β (π΄ β© (-β(,)π΅))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (-β(,)π΅))βπ€) β πΏ)) < π¦)) |
242 | | simp11l 1285 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π¦ β β+) β§ π§ β β+
β§ βπ€ β
π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β§ π£ β β+ β§
βπ€ β (π΄ β© (-β(,)π΅))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (-β(,)π΅))βπ€) β πΏ)) < π¦)) β π) |
243 | | simp12 1205 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π¦ β β+) β§ π§ β β+
β§ βπ€ β
π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β§ π£ β β+ β§
βπ€ β (π΄ β© (-β(,)π΅))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (-β(,)π΅))βπ€) β πΏ)) < π¦)) β π§ β β+) |
244 | | simp2 1138 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π¦ β β+) β§ π§ β β+
β§ βπ€ β
π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β§ π£ β β+ β§
βπ€ β (π΄ β© (-β(,)π΅))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (-β(,)π΅))βπ€) β πΏ)) < π¦)) β π£ β β+) |
245 | | breq2 5113 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π’ = if(π§ β€ π£, π§, π£) β ((absβ(π β π΅)) < π’ β (absβ(π β π΅)) < if(π§ β€ π£, π§, π£))) |
246 | 245 | rexbidv 3172 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π’ = if(π§ β€ π£, π§, π£) β (βπ β ((π΄ β© (-β(,)π΅)) β {π΅})(absβ(π β π΅)) < π’ β βπ β ((π΄ β© (-β(,)π΅)) β {π΅})(absβ(π β π΅)) < if(π§ β€ π£, π§, π£))) |
247 | | inss1 4192 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
(((limPtβπΎ)β(π΄ β© (-β(,)π΅))) β© β) β
((limPtβπΎ)β(π΄ β© (-β(,)π΅))) |
248 | 247 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β (((limPtβπΎ)β(π΄ β© (-β(,)π΅))) β© β) β
((limPtβπΎ)β(π΄ β© (-β(,)π΅)))) |
249 | 48 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β (π΄ β© (-β(,)π΅)) β β) |
250 | 79, 81 | restlp 22557 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((πΎ β Top β§ β
β β β§ (π΄
β© (-β(,)π΅))
β β) β ((limPtβπ½)β(π΄ β© (-β(,)π΅))) = (((limPtβπΎ)β(π΄ β© (-β(,)π΅))) β© β)) |
251 | 71, 73, 249, 250 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β ((limPtβπ½)β(π΄ β© (-β(,)π΅))) = (((limPtβπΎ)β(π΄ β© (-β(,)π΅))) β© β)) |
252 | 85 | fveq1i 6847 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
((limPtβ(TopOpenββfld))β(π΄ β© (-β(,)π΅))) = ((limPtβπΎ)β(π΄ β© (-β(,)π΅))) |
253 | 252 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β
((limPtβ(TopOpenββfld))β(π΄ β© (-β(,)π΅))) = ((limPtβπΎ)β(π΄ β© (-β(,)π΅)))) |
254 | 248, 251,
253 | 3sstr4d 3995 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β ((limPtβπ½)β(π΄ β© (-β(,)π΅))) β
((limPtβ(TopOpenββfld))β(π΄ β© (-β(,)π΅)))) |
255 | 254, 54 | sseldd 3949 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β π΅ β
((limPtβ(TopOpenββfld))β(π΄ β© (-β(,)π΅)))) |
256 | 236, 56 | islpcn 43970 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (π΅ β
((limPtβ(TopOpenββfld))β(π΄ β© (-β(,)π΅))) β βπ’ β β+ βπ β ((π΄ β© (-β(,)π΅)) β {π΅})(absβ(π β π΅)) < π’)) |
257 | 255, 256 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β βπ’ β β+ βπ β ((π΄ β© (-β(,)π΅)) β {π΅})(absβ(π β π΅)) < π’) |
258 | 257 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π§ β β+ β§ π£ β β+)
β βπ’ β
β+ βπ β ((π΄ β© (-β(,)π΅)) β {π΅})(absβ(π β π΅)) < π’) |
259 | 246, 258,
95 | rspcdva 3584 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π§ β β+ β§ π£ β β+)
β βπ β
((π΄ β© (-β(,)π΅)) β {π΅})(absβ(π β π΅)) < if(π§ β€ π£, π§, π£)) |
260 | | eldifi 4090 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β ((π΄ β© (-β(,)π΅)) β {π΅}) β π β (π΄ β© (-β(,)π΅))) |
261 | 48, 260 | sselid 3946 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β ((π΄ β© (-β(,)π΅)) β {π΅}) β π β β) |
262 | 73 | sselda 3948 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π β§ π β β) β π β β) |
263 | 56 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π β§ π β β) β π΅ β β) |
264 | 262, 263 | subcld 11520 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β§ π β β) β (π β π΅) β β) |
265 | 264 | abscld 15330 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β§ π β β) β (absβ(π β π΅)) β β) |
266 | 265 | 3ad2antl1 1186 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ π§ β β+ β§ π£ β β+)
β§ π β β)
β (absβ(π
β π΅)) β
β) |
267 | 266 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ π§ β β+ β§ π£ β β+)
β§ π β β)
β§ (absβ(π β
π΅)) < if(π§ β€ π£, π§, π£)) β (absβ(π β π΅)) β β) |
268 | 105 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ π§ β β+ β§ π£ β β+)
β§ π β β)
β§ (absβ(π β
π΅)) < if(π§ β€ π£, π§, π£)) β if(π§ β€ π£, π§, π£) β β) |
269 | 108 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ π§ β β+ β§ π£ β β+)
β§ π β β)
β§ (absβ(π β
π΅)) < if(π§ β€ π£, π§, π£)) β π§ β β) |
270 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ π§ β β+ β§ π£ β β+)
β§ π β β)
β§ (absβ(π β
π΅)) < if(π§ β€ π£, π§, π£)) β (absβ(π β π΅)) < if(π§ β€ π£, π§, π£)) |
271 | 114 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ π§ β β+ β§ π£ β β+)
β§ π β β)
β§ (absβ(π β
π΅)) < if(π§ β€ π£, π§, π£)) β if(π§ β€ π£, π§, π£) β€ π§) |
272 | 267, 268,
269, 270, 271 | ltletrd 11323 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ π§ β β+ β§ π£ β β+)
β§ π β β)
β§ (absβ(π β
π΅)) < if(π§ β€ π£, π§, π£)) β (absβ(π β π΅)) < π§) |
273 | 117 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ π§ β β+ β§ π£ β β+)
β§ π β β)
β§ (absβ(π β
π΅)) < if(π§ β€ π£, π§, π£)) β π£ β β) |
274 | | min2 13118 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π§ β β β§ π£ β β) β if(π§ β€ π£, π§, π£) β€ π£) |
275 | 107, 111,
274 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π§ β β+
β§ π£ β
β+) β if(π§ β€ π£, π§, π£) β€ π£) |
276 | 275 | 3adant1 1131 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ π§ β β+ β§ π£ β β+)
β if(π§ β€ π£, π§, π£) β€ π£) |
277 | 276 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ π§ β β+ β§ π£ β β+)
β§ π β β)
β§ (absβ(π β
π΅)) < if(π§ β€ π£, π§, π£)) β if(π§ β€ π£, π§, π£) β€ π£) |
278 | 267, 268,
273, 270, 277 | ltletrd 11323 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ π§ β β+ β§ π£ β β+)
β§ π β β)
β§ (absβ(π β
π΅)) < if(π§ β€ π£, π§, π£)) β (absβ(π β π΅)) < π£) |
279 | 272, 278 | jca 513 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ π§ β β+ β§ π£ β β+)
β§ π β β)
β§ (absβ(π β
π΅)) < if(π§ β€ π£, π§, π£)) β ((absβ(π β π΅)) < π§ β§ (absβ(π β π΅)) < π£)) |
280 | 279 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π§ β β+ β§ π£ β β+)
β§ π β β)
β ((absβ(π
β π΅)) < if(π§ β€ π£, π§, π£) β ((absβ(π β π΅)) < π§ β§ (absβ(π β π΅)) < π£))) |
281 | 261, 280 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π§ β β+ β§ π£ β β+)
β§ π β ((π΄ β© (-β(,)π΅)) β {π΅})) β ((absβ(π β π΅)) < if(π§ β€ π£, π§, π£) β ((absβ(π β π΅)) < π§ β§ (absβ(π β π΅)) < π£))) |
282 | 281 | reximdva 3162 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π§ β β+ β§ π£ β β+)
β (βπ β
((π΄ β© (-β(,)π΅)) β {π΅})(absβ(π β π΅)) < if(π§ β€ π£, π§, π£) β βπ β ((π΄ β© (-β(,)π΅)) β {π΅})((absβ(π β π΅)) < π§ β§ (absβ(π β π΅)) < π£))) |
283 | 259, 282 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π§ β β+ β§ π£ β β+)
β βπ β
((π΄ β© (-β(,)π΅)) β {π΅})((absβ(π β π΅)) < π§ β§ (absβ(π β π΅)) < π£)) |
284 | 242, 243,
244, 283 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π¦ β β+) β§ π§ β β+
β§ βπ€ β
π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β§ π£ β β+ β§
βπ€ β (π΄ β© (-β(,)π΅))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (-β(,)π΅))βπ€) β πΏ)) < π¦)) β βπ β ((π΄ β© (-β(,)π΅)) β {π΅})((absβ(π β π΅)) < π§ β§ (absβ(π β π΅)) < π£)) |
285 | | nfv 1918 |
. . . . . . . . . . . . . . . . . . . . 21
β’
β²π(((π β§ π¦ β β+) β§ π§ β β+
β§ βπ€ β
π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β§ π£ β β+ β§
βπ€ β (π΄ β© (-β(,)π΅))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (-β(,)π΅))βπ€) β πΏ)) < π¦)) |
286 | | nfre1 3267 |
. . . . . . . . . . . . . . . . . . . . 21
β’
β²πβπ β π΄ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦) |
287 | 260 | elin1d 4162 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β ((π΄ β© (-β(,)π΅)) β {π΅}) β π β π΄) |
288 | 287 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π β§ π¦ β β+)
β§ π§ β
β+ β§ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β§ π£ β β+ β§
βπ€ β (π΄ β© (-β(,)π΅))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (-β(,)π΅))βπ€) β πΏ)) < π¦)) β§ π β ((π΄ β© (-β(,)π΅)) β {π΅}) β§ ((absβ(π β π΅)) < π§ β§ (absβ(π β π΅)) < π£)) β π β π΄) |
289 | | simp113 1305 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π β§ π¦ β β+)
β§ π§ β
β+ β§ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β§ π£ β β+ β§
βπ€ β (π΄ β© (-β(,)π΅))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (-β(,)π΅))βπ€) β πΏ)) < π¦)) β§ π β ((π΄ β© (-β(,)π΅)) β {π΅}) β§ ((absβ(π β π΅)) < π§ β§ (absβ(π β π΅)) < π£)) β βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) |
290 | | eldifsni 4754 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β ((π΄ β© (-β(,)π΅)) β {π΅}) β π β π΅) |
291 | 290 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β ((π΄ β© (-β(,)π΅)) β {π΅}) β§ ((absβ(π β π΅)) < π§ β§ (absβ(π β π΅)) < π£)) β π β π΅) |
292 | | simprl 770 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β ((π΄ β© (-β(,)π΅)) β {π΅}) β§ ((absβ(π β π΅)) < π§ β§ (absβ(π β π΅)) < π£)) β (absβ(π β π΅)) < π§) |
293 | 291, 292 | jca 513 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β ((π΄ β© (-β(,)π΅)) β {π΅}) β§ ((absβ(π β π΅)) < π§ β§ (absβ(π β π΅)) < π£)) β (π β π΅ β§ (absβ(π β π΅)) < π§)) |
294 | 293 | 3adant1 1131 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π β§ π¦ β β+)
β§ π§ β
β+ β§ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β§ π£ β β+ β§
βπ€ β (π΄ β© (-β(,)π΅))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (-β(,)π΅))βπ€) β πΏ)) < π¦)) β§ π β ((π΄ β© (-β(,)π΅)) β {π΅}) β§ ((absβ(π β π΅)) < π§ β§ (absβ(π β π΅)) < π£)) β (π β π΅ β§ (absβ(π β π΅)) < π§)) |
295 | | neeq1 3003 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π€ = π β (π€ β π΅ β π β π΅)) |
296 | | fvoveq1 7384 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π€ = π β (absβ(π€ β π΅)) = (absβ(π β π΅))) |
297 | 296 | breq1d 5119 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π€ = π β ((absβ(π€ β π΅)) < π§ β (absβ(π β π΅)) < π§)) |
298 | 295, 297 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π€ = π β ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (π β π΅ β§ (absβ(π β π΅)) < π§))) |
299 | 298 | imbrov2fvoveq 7386 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π€ = π β (((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦) β ((π β π΅ β§ (absβ(π β π΅)) < π§) β (absβ((πΉβπ) β π₯)) < π¦))) |
300 | 299 | rspcva 3581 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β π΄ β§ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β ((π β π΅ β§ (absβ(π β π΅)) < π§) β (absβ((πΉβπ) β π₯)) < π¦)) |
301 | 300 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β π΄ β§ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β§ (π β π΅ β§ (absβ(π β π΅)) < π§)) β (absβ((πΉβπ) β π₯)) < π¦) |
302 | 288, 289,
294, 301 | syl21anc 837 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π β§ π¦ β β+)
β§ π§ β
β+ β§ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β§ π£ β β+ β§
βπ€ β (π΄ β© (-β(,)π΅))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (-β(,)π΅))βπ€) β πΏ)) < π¦)) β§ π β ((π΄ β© (-β(,)π΅)) β {π΅}) β§ ((absβ(π β π΅)) < π§ β§ (absβ(π β π΅)) < π£)) β (absβ((πΉβπ) β π₯)) < π¦) |
303 | 260 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π β§ π¦ β β+)
β§ π§ β
β+ β§ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β§ π£ β β+ β§
βπ€ β (π΄ β© (-β(,)π΅))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (-β(,)π΅))βπ€) β πΏ)) < π¦)) β§ π β ((π΄ β© (-β(,)π΅)) β {π΅}) β§ ((absβ(π β π΅)) < π§ β§ (absβ(π β π΅)) < π£)) β π β (π΄ β© (-β(,)π΅))) |
304 | 242 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β§ π¦ β β+)
β§ π§ β
β+ β§ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β§ π£ β β+ β§
βπ€ β (π΄ β© (-β(,)π΅))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (-β(,)π΅))βπ€) β πΏ)) < π¦)) β§ π β ((π΄ β© (-β(,)π΅)) β {π΅}) β§ ((absβ(π β π΅)) < π§ β§ (absβ(π β π΅)) < π£)) β π) |
305 | | simp13 1206 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β§ π¦ β β+)
β§ π§ β
β+ β§ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β§ π£ β β+ β§
βπ€ β (π΄ β© (-β(,)π΅))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (-β(,)π΅))βπ€) β πΏ)) < π¦)) β§ π β ((π΄ β© (-β(,)π΅)) β {π΅}) β§ ((absβ(π β π΅)) < π§ β§ (absβ(π β π΅)) < π£)) β βπ€ β (π΄ β© (-β(,)π΅))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (-β(,)π΅))βπ€) β πΏ)) < π¦)) |
306 | | nfra1 3266 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
β²π€βπ€ β (π΄ β© (-β(,)π΅))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (-β(,)π΅))βπ€) β πΏ)) < π¦) |
307 | 148, 306 | nfan 1903 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
β²π€(π β§ βπ€ β (π΄ β© (-β(,)π΅))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (-β(,)π΅))βπ€) β πΏ)) < π¦)) |
308 | | elinel2 4160 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π€ β (π΄ β© (-β(,)π΅)) β π€ β (-β(,)π΅)) |
309 | 308 | fvresd 6866 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π€ β (π΄ β© (-β(,)π΅)) β ((πΉ βΎ (-β(,)π΅))βπ€) = (πΉβπ€)) |
310 | 309 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π€ β (π΄ β© (-β(,)π΅)) β (πΉβπ€) = ((πΉ βΎ (-β(,)π΅))βπ€)) |
311 | 310 | fvoveq1d 7383 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π€ β (π΄ β© (-β(,)π΅)) β (absβ((πΉβπ€) β πΏ)) = (absβ(((πΉ βΎ (-β(,)π΅))βπ€) β πΏ))) |
312 | 311 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ βπ€ β (π΄ β© (-β(,)π΅))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (-β(,)π΅))βπ€) β πΏ)) < π¦)) β§ π€ β (π΄ β© (-β(,)π΅)) β§ (π€ β π΅ β§ (absβ(π€ β π΅)) < π£)) β (absβ((πΉβπ€) β πΏ)) = (absβ(((πΉ βΎ (-β(,)π΅))βπ€) β πΏ))) |
313 | | rspa 3230 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
((βπ€ β
(π΄ β© (-β(,)π΅))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (-β(,)π΅))βπ€) β πΏ)) < π¦) β§ π€ β (π΄ β© (-β(,)π΅))) β ((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (-β(,)π΅))βπ€) β πΏ)) < π¦)) |
314 | 313 | 3impia 1118 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
((βπ€ β
(π΄ β© (-β(,)π΅))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (-β(,)π΅))βπ€) β πΏ)) < π¦) β§ π€ β (π΄ β© (-β(,)π΅)) β§ (π€ β π΅ β§ (absβ(π€ β π΅)) < π£)) β (absβ(((πΉ βΎ (-β(,)π΅))βπ€) β πΏ)) < π¦) |
315 | 314 | 3adant1l 1177 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ βπ€ β (π΄ β© (-β(,)π΅))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (-β(,)π΅))βπ€) β πΏ)) < π¦)) β§ π€ β (π΄ β© (-β(,)π΅)) β§ (π€ β π΅ β§ (absβ(π€ β π΅)) < π£)) β (absβ(((πΉ βΎ (-β(,)π΅))βπ€) β πΏ)) < π¦) |
316 | 312, 315 | eqbrtrd 5131 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ βπ€ β (π΄ β© (-β(,)π΅))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (-β(,)π΅))βπ€) β πΏ)) < π¦)) β§ π€ β (π΄ β© (-β(,)π΅)) β§ (π€ β π΅ β§ (absβ(π€ β π΅)) < π£)) β (absβ((πΉβπ€) β πΏ)) < π¦) |
317 | 316 | 3exp 1120 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ βπ€ β (π΄ β© (-β(,)π΅))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (-β(,)π΅))βπ€) β πΏ)) < π¦)) β (π€ β (π΄ β© (-β(,)π΅)) β ((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ((πΉβπ€) β πΏ)) < π¦))) |
318 | 307, 317 | ralrimi 3239 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ βπ€ β (π΄ β© (-β(,)π΅))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (-β(,)π΅))βπ€) β πΏ)) < π¦)) β βπ€ β (π΄ β© (-β(,)π΅))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ((πΉβπ€) β πΏ)) < π¦)) |
319 | 304, 305,
318 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π β§ π¦ β β+)
β§ π§ β
β+ β§ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β§ π£ β β+ β§
βπ€ β (π΄ β© (-β(,)π΅))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (-β(,)π΅))βπ€) β πΏ)) < π¦)) β§ π β ((π΄ β© (-β(,)π΅)) β {π΅}) β§ ((absβ(π β π΅)) < π§ β§ (absβ(π β π΅)) < π£)) β βπ€ β (π΄ β© (-β(,)π΅))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ((πΉβπ€) β πΏ)) < π¦)) |
320 | 290 | anim1i 616 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β ((π΄ β© (-β(,)π΅)) β {π΅}) β§ (absβ(π β π΅)) < π£) β (π β π΅ β§ (absβ(π β π΅)) < π£)) |
321 | 320 | adantrl 715 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β ((π΄ β© (-β(,)π΅)) β {π΅}) β§ ((absβ(π β π΅)) < π§ β§ (absβ(π β π΅)) < π£)) β (π β π΅ β§ (absβ(π β π΅)) < π£)) |
322 | 321 | 3adant1 1131 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π β§ π¦ β β+)
β§ π§ β
β+ β§ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β§ π£ β β+ β§
βπ€ β (π΄ β© (-β(,)π΅))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (-β(,)π΅))βπ€) β πΏ)) < π¦)) β§ π β ((π΄ β© (-β(,)π΅)) β {π΅}) β§ ((absβ(π β π΅)) < π§ β§ (absβ(π β π΅)) < π£)) β (π β π΅ β§ (absβ(π β π΅)) < π£)) |
323 | 296 | breq1d 5119 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π€ = π β ((absβ(π€ β π΅)) < π£ β (absβ(π β π΅)) < π£)) |
324 | 295, 323 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π€ = π β ((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (π β π΅ β§ (absβ(π β π΅)) < π£))) |
325 | 324 | imbrov2fvoveq 7386 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π€ = π β (((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ((πΉβπ€) β πΏ)) < π¦) β ((π β π΅ β§ (absβ(π β π΅)) < π£) β (absβ((πΉβπ) β πΏ)) < π¦))) |
326 | 325 | rspcva 3581 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β (π΄ β© (-β(,)π΅)) β§ βπ€ β (π΄ β© (-β(,)π΅))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ((πΉβπ€) β πΏ)) < π¦)) β ((π β π΅ β§ (absβ(π β π΅)) < π£) β (absβ((πΉβπ) β πΏ)) < π¦)) |
327 | 326 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β (π΄ β© (-β(,)π΅)) β§ βπ€ β (π΄ β© (-β(,)π΅))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ((πΉβπ€) β πΏ)) < π¦)) β§ (π β π΅ β§ (absβ(π β π΅)) < π£)) β (absβ((πΉβπ) β πΏ)) < π¦) |
328 | 303, 319,
322, 327 | syl21anc 837 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π β§ π¦ β β+)
β§ π§ β
β+ β§ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β§ π£ β β+ β§
βπ€ β (π΄ β© (-β(,)π΅))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (-β(,)π΅))βπ€) β πΏ)) < π¦)) β§ π β ((π΄ β© (-β(,)π΅)) β {π΅}) β§ ((absβ(π β π΅)) < π§ β§ (absβ(π β π΅)) < π£)) β (absβ((πΉβπ) β πΏ)) < π¦) |
329 | | rspe 3231 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β π΄ β§ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦)) β βπ β π΄ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦)) |
330 | 288, 302,
328, 329 | syl12anc 836 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π β§ π¦ β β+)
β§ π§ β
β+ β§ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β§ π£ β β+ β§
βπ€ β (π΄ β© (-β(,)π΅))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (-β(,)π΅))βπ€) β πΏ)) < π¦)) β§ π β ((π΄ β© (-β(,)π΅)) β {π΅}) β§ ((absβ(π β π΅)) < π§ β§ (absβ(π β π΅)) < π£)) β βπ β π΄ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦)) |
331 | 330 | 3exp 1120 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π¦ β β+) β§ π§ β β+
β§ βπ€ β
π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β§ π£ β β+ β§
βπ€ β (π΄ β© (-β(,)π΅))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (-β(,)π΅))βπ€) β πΏ)) < π¦)) β (π β ((π΄ β© (-β(,)π΅)) β {π΅}) β (((absβ(π β π΅)) < π§ β§ (absβ(π β π΅)) < π£) β βπ β π΄ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦)))) |
332 | 285, 286,
331 | rexlimd 3248 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π¦ β β+) β§ π§ β β+
β§ βπ€ β
π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β§ π£ β β+ β§
βπ€ β (π΄ β© (-β(,)π΅))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (-β(,)π΅))βπ€) β πΏ)) < π¦)) β (βπ β ((π΄ β© (-β(,)π΅)) β {π΅})((absβ(π β π΅)) < π§ β§ (absβ(π β π΅)) < π£) β βπ β π΄ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦))) |
333 | 284, 332 | mpd 15 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π¦ β β+) β§ π§ β β+
β§ βπ€ β
π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β§ π£ β β+ β§
βπ€ β (π΄ β© (-β(,)π΅))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (-β(,)π΅))βπ€) β πΏ)) < π¦)) β βπ β π΄ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦)) |
334 | 333 | 3exp 1120 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π¦ β β+) β§ π§ β β+
β§ βπ€ β
π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β (π£ β β+ β
(βπ€ β (π΄ β© (-β(,)π΅))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (-β(,)π΅))βπ€) β πΏ)) < π¦) β βπ β π΄ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦)))) |
335 | 334 | rexlimdv 3147 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π¦ β β+) β§ π§ β β+
β§ βπ€ β
π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β (βπ£ β β+ βπ€ β (π΄ β© (-β(,)π΅))((π€ β π΅ β§ (absβ(π€ β π΅)) < π£) β (absβ(((πΉ βΎ (-β(,)π΅))βπ€) β πΏ)) < π¦) β βπ β π΄ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦))) |
336 | 241, 335 | mpd 15 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π¦ β β+) β§ π§ β β+
β§ βπ€ β
π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β βπ β π΄ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦)) |
337 | 336 | 3exp 1120 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π¦ β β+) β (π§ β β+
β (βπ€ β
π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦) β βπ β π΄ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦)))) |
338 | 337 | rexlimdv 3147 |
. . . . . . . . . . . . . 14
β’ ((π β§ π¦ β β+) β
(βπ§ β
β+ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦) β βπ β π΄ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦))) |
339 | 338 | imp 408 |
. . . . . . . . . . . . 13
β’ (((π β§ π¦ β β+) β§
βπ§ β
β+ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β βπ β π΄ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦)) |
340 | 339 | adantllr 718 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β β) β§ π¦ β β+) β§
βπ§ β
β+ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β βπ β π΄ ((absβ((πΉβπ) β π₯)) < π¦ β§ (absβ((πΉβπ) β πΏ)) < π¦)) |
341 | 231, 340 | reximddv3 43453 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β β) β§ π¦ β β+) β§
βπ§ β
β+ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β βπ β π΄ βπ β π΄ (absβ(π
β πΏ)) < (4 Β· π¦)) |
342 | 32, 33, 35, 341 | syl21anc 837 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β β) β§ βπ¦ β β+
βπ§ β
β+ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β§ π¦ β β+) β
βπ β π΄ βπ β π΄ (absβ(π
β πΏ)) < (4 Β· π¦)) |
343 | 342 | ex 414 |
. . . . . . . . 9
β’ (((π β§ π₯ β β) β§ βπ¦ β β+
βπ§ β
β+ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β (π¦ β β+ β
βπ β π΄ βπ β π΄ (absβ(π
β πΏ)) < (4 Β· π¦))) |
344 | 24, 25, 31, 343 | vtoclf 3518 |
. . . . . . . 8
β’ (((π β§ π₯ β β) β§ βπ¦ β β+
βπ§ β
β+ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β (((absβ(π
β πΏ)) / 4) β β+ β
βπ β π΄ βπ β π΄ (absβ(π
β πΏ)) < (4 Β· ((absβ(π
β πΏ)) / 4)))) |
345 | 19, 344 | mpd 15 |
. . . . . . 7
β’ (((π β§ π₯ β β) β§ βπ¦ β β+
βπ§ β
β+ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β βπ β π΄ βπ β π΄ (absβ(π
β πΏ)) < (4 Β· ((absβ(π
β πΏ)) / 4))) |
346 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((π β§ (absβ(π
β πΏ)) < (4 Β· ((absβ(π
β πΏ)) / 4))) β (absβ(π
β πΏ)) < (4 Β· ((absβ(π
β πΏ)) / 4))) |
347 | | abssubrp 43600 |
. . . . . . . . . . . . . . . 16
β’ ((π
β β β§ πΏ β β β§ π
β πΏ) β (absβ(π
β πΏ)) β
β+) |
348 | 3, 7, 11, 347 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ (π β (absβ(π
β πΏ)) β
β+) |
349 | 348 | rpcnd 12967 |
. . . . . . . . . . . . . 14
β’ (π β (absβ(π
β πΏ)) β β) |
350 | 349 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ (absβ(π
β πΏ)) < (4 Β· ((absβ(π
β πΏ)) / 4))) β (absβ(π
β πΏ)) β β) |
351 | | 4cn 12246 |
. . . . . . . . . . . . . 14
β’ 4 β
β |
352 | 351 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((π β§ (absβ(π
β πΏ)) < (4 Β· ((absβ(π
β πΏ)) / 4))) β 4 β
β) |
353 | | 4ne0 12269 |
. . . . . . . . . . . . . 14
β’ 4 β
0 |
354 | 353 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((π β§ (absβ(π
β πΏ)) < (4 Β· ((absβ(π
β πΏ)) / 4))) β 4 β 0) |
355 | 350, 352,
354 | divcan2d 11941 |
. . . . . . . . . . . 12
β’ ((π β§ (absβ(π
β πΏ)) < (4 Β· ((absβ(π
β πΏ)) / 4))) β (4 Β·
((absβ(π
β
πΏ)) / 4)) =
(absβ(π
β πΏ))) |
356 | 346, 355 | breqtrd 5135 |
. . . . . . . . . . 11
β’ ((π β§ (absβ(π
β πΏ)) < (4 Β· ((absβ(π
β πΏ)) / 4))) β (absβ(π
β πΏ)) < (absβ(π
β πΏ))) |
357 | 356 | ex 414 |
. . . . . . . . . 10
β’ (π β ((absβ(π
β πΏ)) < (4 Β· ((absβ(π
β πΏ)) / 4)) β (absβ(π
β πΏ)) < (absβ(π
β πΏ)))) |
358 | 357 | a1d 25 |
. . . . . . . . 9
β’ (π β ((π β π΄ β§ π β π΄) β ((absβ(π
β πΏ)) < (4 Β· ((absβ(π
β πΏ)) / 4)) β (absβ(π
β πΏ)) < (absβ(π
β πΏ))))) |
359 | 358 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π₯ β β) β§ βπ¦ β β+
βπ§ β
β+ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β ((π β π΄ β§ π β π΄) β ((absβ(π
β πΏ)) < (4 Β· ((absβ(π
β πΏ)) / 4)) β (absβ(π
β πΏ)) < (absβ(π
β πΏ))))) |
360 | 359 | rexlimdvv 3201 |
. . . . . . 7
β’ (((π β§ π₯ β β) β§ βπ¦ β β+
βπ§ β
β+ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β (βπ β π΄ βπ β π΄ (absβ(π
β πΏ)) < (4 Β· ((absβ(π
β πΏ)) / 4)) β (absβ(π
β πΏ)) < (absβ(π
β πΏ)))) |
361 | 345, 360 | mpd 15 |
. . . . . 6
β’ (((π β§ π₯ β β) β§ βπ¦ β β+
βπ§ β
β+ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β (absβ(π
β πΏ)) < (absβ(π
β πΏ))) |
362 | 9 | abscld 15330 |
. . . . . . 7
β’ (((π β§ π₯ β β) β§ βπ¦ β β+
βπ§ β
β+ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β (absβ(π
β πΏ)) β β) |
363 | 362 | ltnrd 11297 |
. . . . . 6
β’ (((π β§ π₯ β β) β§ βπ¦ β β+
βπ§ β
β+ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β Β¬ (absβ(π
β πΏ)) < (absβ(π
β πΏ))) |
364 | 361, 363 | pm2.65da 816 |
. . . . 5
β’ ((π β§ π₯ β β) β Β¬ βπ¦ β β+
βπ§ β
β+ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) |
365 | 364 | ex 414 |
. . . 4
β’ (π β (π₯ β β β Β¬ βπ¦ β β+
βπ§ β
β+ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦))) |
366 | | imnan 401 |
. . . 4
β’ ((π₯ β β β Β¬
βπ¦ β
β+ βπ§ β β+ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)) β Β¬ (π₯ β β β§ βπ¦ β β+
βπ§ β
β+ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦))) |
367 | 365, 366 | sylib 217 |
. . 3
β’ (π β Β¬ (π₯ β β β§ βπ¦ β β+
βπ§ β
β+ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦))) |
368 | | limclner.a |
. . . . 5
β’ (π β π΄ β β) |
369 | 368, 73 | sstrd 3958 |
. . . 4
β’ (π β π΄ β β) |
370 | 36, 369, 56 | ellimc3 25266 |
. . 3
β’ (π β (π₯ β (πΉ limβ π΅) β (π₯ β β β§ βπ¦ β β+
βπ§ β
β+ βπ€ β π΄ ((π€ β π΅ β§ (absβ(π€ β π΅)) < π§) β (absβ((πΉβπ€) β π₯)) < π¦)))) |
371 | 367, 370 | mtbird 325 |
. 2
β’ (π β Β¬ π₯ β (πΉ limβ π΅)) |
372 | 371 | eq0rdv 4368 |
1
β’ (π β (πΉ limβ π΅) = β
) |