Step | Hyp | Ref
| Expression |
1 | | rlimuni.3 |
. . . . . . . . . . . 12
β’ (π β πΉ βπ π΅) |
2 | | rlimcl 15447 |
. . . . . . . . . . . 12
β’ (πΉ βπ
π΅ β π΅ β β) |
3 | 1, 2 | syl 17 |
. . . . . . . . . . 11
β’ (π β π΅ β β) |
4 | 3 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β π΄) β π΅ β β) |
5 | | rlimuni.4 |
. . . . . . . . . . . 12
β’ (π β πΉ βπ πΆ) |
6 | | rlimcl 15447 |
. . . . . . . . . . . 12
β’ (πΉ βπ
πΆ β πΆ β β) |
7 | 5, 6 | syl 17 |
. . . . . . . . . . 11
β’ (π β πΆ β β) |
8 | 7 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β π΄) β πΆ β β) |
9 | 4, 8 | subcld 11571 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β π΄) β (π΅ β πΆ) β β) |
10 | 9 | abscld 15383 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β π΄) β (absβ(π΅ β πΆ)) β β) |
11 | 10 | ltnrd 11348 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β π΄) β Β¬ (absβ(π΅ β πΆ)) < (absβ(π΅ β πΆ))) |
12 | | rlimuni.1 |
. . . . . . . . . . . . . . 15
β’ (π β πΉ:π΄βΆβ) |
13 | 12 | ffvelcdmda 7087 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π΄) β (πΉβπ) β β) |
14 | 13 | adantlr 714 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ π β π΄) β (πΉβπ) β β) |
15 | 14, 4 | abssubd 15400 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π β π΄) β (absβ((πΉβπ) β π΅)) = (absβ(π΅ β (πΉβπ)))) |
16 | 15 | breq1d 5159 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β π΄) β ((absβ((πΉβπ) β π΅)) < ((absβ(π΅ β πΆ)) / 2) β (absβ(π΅ β (πΉβπ))) < ((absβ(π΅ β πΆ)) / 2))) |
17 | 16 | anbi1d 631 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β π΄) β (((absβ((πΉβπ) β π΅)) < ((absβ(π΅ β πΆ)) / 2) β§ (absβ((πΉβπ) β πΆ)) < ((absβ(π΅ β πΆ)) / 2)) β ((absβ(π΅ β (πΉβπ))) < ((absβ(π΅ β πΆ)) / 2) β§ (absβ((πΉβπ) β πΆ)) < ((absβ(π΅ β πΆ)) / 2)))) |
18 | | abs3lem 15285 |
. . . . . . . . . . 11
β’ (((π΅ β β β§ πΆ β β) β§ ((πΉβπ) β β β§ (absβ(π΅ β πΆ)) β β)) β
(((absβ(π΅ β
(πΉβπ))) < ((absβ(π΅ β πΆ)) / 2) β§ (absβ((πΉβπ) β πΆ)) < ((absβ(π΅ β πΆ)) / 2)) β (absβ(π΅ β πΆ)) < (absβ(π΅ β πΆ)))) |
19 | 4, 8, 14, 10, 18 | syl22anc 838 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β π΄) β (((absβ(π΅ β (πΉβπ))) < ((absβ(π΅ β πΆ)) / 2) β§ (absβ((πΉβπ) β πΆ)) < ((absβ(π΅ β πΆ)) / 2)) β (absβ(π΅ β πΆ)) < (absβ(π΅ β πΆ)))) |
20 | 17, 19 | sylbid 239 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β π΄) β (((absβ((πΉβπ) β π΅)) < ((absβ(π΅ β πΆ)) / 2) β§ (absβ((πΉβπ) β πΆ)) < ((absβ(π΅ β πΆ)) / 2)) β (absβ(π΅ β πΆ)) < (absβ(π΅ β πΆ)))) |
21 | 20 | imim2d 57 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β π΄) β ((π β€ π β ((absβ((πΉβπ) β π΅)) < ((absβ(π΅ β πΆ)) / 2) β§ (absβ((πΉβπ) β πΆ)) < ((absβ(π΅ β πΆ)) / 2))) β (π β€ π β (absβ(π΅ β πΆ)) < (absβ(π΅ β πΆ))))) |
22 | 21 | impcomd 413 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β π΄) β ((π β€ π β§ (π β€ π β ((absβ((πΉβπ) β π΅)) < ((absβ(π΅ β πΆ)) / 2) β§ (absβ((πΉβπ) β πΆ)) < ((absβ(π΅ β πΆ)) / 2)))) β (absβ(π΅ β πΆ)) < (absβ(π΅ β πΆ)))) |
23 | 11, 22 | mtod 197 |
. . . . . 6
β’ (((π β§ π β β) β§ π β π΄) β Β¬ (π β€ π β§ (π β€ π β ((absβ((πΉβπ) β π΅)) < ((absβ(π΅ β πΆ)) / 2) β§ (absβ((πΉβπ) β πΆ)) < ((absβ(π΅ β πΆ)) / 2))))) |
24 | 23 | nrexdv 3150 |
. . . . 5
β’ ((π β§ π β β) β Β¬ βπ β π΄ (π β€ π β§ (π β€ π β ((absβ((πΉβπ) β π΅)) < ((absβ(π΅ β πΆ)) / 2) β§ (absβ((πΉβπ) β πΆ)) < ((absβ(π΅ β πΆ)) / 2))))) |
25 | | r19.29r 3117 |
. . . . 5
β’
((βπ β
π΄ π β€ π β§ βπ β π΄ (π β€ π β ((absβ((πΉβπ) β π΅)) < ((absβ(π΅ β πΆ)) / 2) β§ (absβ((πΉβπ) β πΆ)) < ((absβ(π΅ β πΆ)) / 2)))) β βπ β π΄ (π β€ π β§ (π β€ π β ((absβ((πΉβπ) β π΅)) < ((absβ(π΅ β πΆ)) / 2) β§ (absβ((πΉβπ) β πΆ)) < ((absβ(π΅ β πΆ)) / 2))))) |
26 | 24, 25 | nsyl 140 |
. . . 4
β’ ((π β§ π β β) β Β¬ (βπ β π΄ π β€ π β§ βπ β π΄ (π β€ π β ((absβ((πΉβπ) β π΅)) < ((absβ(π΅ β πΆ)) / 2) β§ (absβ((πΉβπ) β πΆ)) < ((absβ(π΅ β πΆ)) / 2))))) |
27 | 26 | nrexdv 3150 |
. . 3
β’ (π β Β¬ βπ β β (βπ β π΄ π β€ π β§ βπ β π΄ (π β€ π β ((absβ((πΉβπ) β π΅)) < ((absβ(π΅ β πΆ)) / 2) β§ (absβ((πΉβπ) β πΆ)) < ((absβ(π΅ β πΆ)) / 2))))) |
28 | | rlimuni.2 |
. . . . 5
β’ (π β sup(π΄, β*, < ) =
+β) |
29 | 12 | fdmd 6729 |
. . . . . . . 8
β’ (π β dom πΉ = π΄) |
30 | | rlimss 15446 |
. . . . . . . . 9
β’ (πΉ βπ
π΅ β dom πΉ β
β) |
31 | 1, 30 | syl 17 |
. . . . . . . 8
β’ (π β dom πΉ β β) |
32 | 29, 31 | eqsstrrd 4022 |
. . . . . . 7
β’ (π β π΄ β β) |
33 | | ressxr 11258 |
. . . . . . 7
β’ β
β β* |
34 | 32, 33 | sstrdi 3995 |
. . . . . 6
β’ (π β π΄ β
β*) |
35 | | supxrunb1 13298 |
. . . . . 6
β’ (π΄ β β*
β (βπ β
β βπ β
π΄ π β€ π β sup(π΄, β*, < ) =
+β)) |
36 | 34, 35 | syl 17 |
. . . . 5
β’ (π β (βπ β β βπ β π΄ π β€ π β sup(π΄, β*, < ) =
+β)) |
37 | 28, 36 | mpbird 257 |
. . . 4
β’ (π β βπ β β βπ β π΄ π β€ π) |
38 | | r19.29 3115 |
. . . . 5
β’
((βπ β
β βπ β
π΄ π β€ π β§ βπ β β βπ β π΄ (π β€ π β ((absβ((πΉβπ) β π΅)) < ((absβ(π΅ β πΆ)) / 2) β§ (absβ((πΉβπ) β πΆ)) < ((absβ(π΅ β πΆ)) / 2)))) β βπ β β (βπ β π΄ π β€ π β§ βπ β π΄ (π β€ π β ((absβ((πΉβπ) β π΅)) < ((absβ(π΅ β πΆ)) / 2) β§ (absβ((πΉβπ) β πΆ)) < ((absβ(π΅ β πΆ)) / 2))))) |
39 | 38 | ex 414 |
. . . 4
β’
(βπ β
β βπ β
π΄ π β€ π β (βπ β β βπ β π΄ (π β€ π β ((absβ((πΉβπ) β π΅)) < ((absβ(π΅ β πΆ)) / 2) β§ (absβ((πΉβπ) β πΆ)) < ((absβ(π΅ β πΆ)) / 2))) β βπ β β (βπ β π΄ π β€ π β§ βπ β π΄ (π β€ π β ((absβ((πΉβπ) β π΅)) < ((absβ(π΅ β πΆ)) / 2) β§ (absβ((πΉβπ) β πΆ)) < ((absβ(π΅ β πΆ)) / 2)))))) |
40 | 37, 39 | syl 17 |
. . 3
β’ (π β (βπ β β βπ β π΄ (π β€ π β ((absβ((πΉβπ) β π΅)) < ((absβ(π΅ β πΆ)) / 2) β§ (absβ((πΉβπ) β πΆ)) < ((absβ(π΅ β πΆ)) / 2))) β βπ β β (βπ β π΄ π β€ π β§ βπ β π΄ (π β€ π β ((absβ((πΉβπ) β π΅)) < ((absβ(π΅ β πΆ)) / 2) β§ (absβ((πΉβπ) β πΆ)) < ((absβ(π΅ β πΆ)) / 2)))))) |
41 | 27, 40 | mtod 197 |
. 2
β’ (π β Β¬ βπ β β βπ β π΄ (π β€ π β ((absβ((πΉβπ) β π΅)) < ((absβ(π΅ β πΆ)) / 2) β§ (absβ((πΉβπ) β πΆ)) < ((absβ(π΅ β πΆ)) / 2)))) |
42 | 12 | adantr 482 |
. . . . . . 7
β’ ((π β§ π΅ β πΆ) β πΉ:π΄βΆβ) |
43 | | ffvelcdm 7084 |
. . . . . . . 8
β’ ((πΉ:π΄βΆβ β§ π β π΄) β (πΉβπ) β β) |
44 | 43 | ralrimiva 3147 |
. . . . . . 7
β’ (πΉ:π΄βΆβ β βπ β π΄ (πΉβπ) β β) |
45 | 42, 44 | syl 17 |
. . . . . 6
β’ ((π β§ π΅ β πΆ) β βπ β π΄ (πΉβπ) β β) |
46 | 3 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π΅ β πΆ) β π΅ β β) |
47 | 7 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π΅ β πΆ) β πΆ β β) |
48 | 46, 47 | subcld 11571 |
. . . . . . . 8
β’ ((π β§ π΅ β πΆ) β (π΅ β πΆ) β β) |
49 | | simpr 486 |
. . . . . . . . 9
β’ ((π β§ π΅ β πΆ) β π΅ β πΆ) |
50 | 46, 47, 49 | subne0d 11580 |
. . . . . . . 8
β’ ((π β§ π΅ β πΆ) β (π΅ β πΆ) β 0) |
51 | 48, 50 | absrpcld 15395 |
. . . . . . 7
β’ ((π β§ π΅ β πΆ) β (absβ(π΅ β πΆ)) β
β+) |
52 | 51 | rphalfcld 13028 |
. . . . . 6
β’ ((π β§ π΅ β πΆ) β ((absβ(π΅ β πΆ)) / 2) β
β+) |
53 | 42 | feqmptd 6961 |
. . . . . . 7
β’ ((π β§ π΅ β πΆ) β πΉ = (π β π΄ β¦ (πΉβπ))) |
54 | 1 | adantr 482 |
. . . . . . 7
β’ ((π β§ π΅ β πΆ) β πΉ βπ π΅) |
55 | 53, 54 | eqbrtrrd 5173 |
. . . . . 6
β’ ((π β§ π΅ β πΆ) β (π β π΄ β¦ (πΉβπ)) βπ π΅) |
56 | 45, 52, 55 | rlimi 15457 |
. . . . 5
β’ ((π β§ π΅ β πΆ) β βπ β β βπ β π΄ (π β€ π β (absβ((πΉβπ) β π΅)) < ((absβ(π΅ β πΆ)) / 2))) |
57 | 5 | adantr 482 |
. . . . . . 7
β’ ((π β§ π΅ β πΆ) β πΉ βπ πΆ) |
58 | 53, 57 | eqbrtrrd 5173 |
. . . . . 6
β’ ((π β§ π΅ β πΆ) β (π β π΄ β¦ (πΉβπ)) βπ πΆ) |
59 | 45, 52, 58 | rlimi 15457 |
. . . . 5
β’ ((π β§ π΅ β πΆ) β βπ β β βπ β π΄ (π β€ π β (absβ((πΉβπ) β πΆ)) < ((absβ(π΅ β πΆ)) / 2))) |
60 | 32 | adantr 482 |
. . . . . 6
β’ ((π β§ π΅ β πΆ) β π΄ β β) |
61 | | rexanre 15293 |
. . . . . 6
β’ (π΄ β β β
(βπ β β
βπ β π΄ (π β€ π β ((absβ((πΉβπ) β π΅)) < ((absβ(π΅ β πΆ)) / 2) β§ (absβ((πΉβπ) β πΆ)) < ((absβ(π΅ β πΆ)) / 2))) β (βπ β β βπ β π΄ (π β€ π β (absβ((πΉβπ) β π΅)) < ((absβ(π΅ β πΆ)) / 2)) β§ βπ β β βπ β π΄ (π β€ π β (absβ((πΉβπ) β πΆ)) < ((absβ(π΅ β πΆ)) / 2))))) |
62 | 60, 61 | syl 17 |
. . . . 5
β’ ((π β§ π΅ β πΆ) β (βπ β β βπ β π΄ (π β€ π β ((absβ((πΉβπ) β π΅)) < ((absβ(π΅ β πΆ)) / 2) β§ (absβ((πΉβπ) β πΆ)) < ((absβ(π΅ β πΆ)) / 2))) β (βπ β β βπ β π΄ (π β€ π β (absβ((πΉβπ) β π΅)) < ((absβ(π΅ β πΆ)) / 2)) β§ βπ β β βπ β π΄ (π β€ π β (absβ((πΉβπ) β πΆ)) < ((absβ(π΅ β πΆ)) / 2))))) |
63 | 56, 59, 62 | mpbir2and 712 |
. . . 4
β’ ((π β§ π΅ β πΆ) β βπ β β βπ β π΄ (π β€ π β ((absβ((πΉβπ) β π΅)) < ((absβ(π΅ β πΆ)) / 2) β§ (absβ((πΉβπ) β πΆ)) < ((absβ(π΅ β πΆ)) / 2)))) |
64 | 63 | ex 414 |
. . 3
β’ (π β (π΅ β πΆ β βπ β β βπ β π΄ (π β€ π β ((absβ((πΉβπ) β π΅)) < ((absβ(π΅ β πΆ)) / 2) β§ (absβ((πΉβπ) β πΆ)) < ((absβ(π΅ β πΆ)) / 2))))) |
65 | 64 | necon1bd 2959 |
. 2
β’ (π β (Β¬ βπ β β βπ β π΄ (π β€ π β ((absβ((πΉβπ) β π΅)) < ((absβ(π΅ β πΆ)) / 2) β§ (absβ((πΉβπ) β πΆ)) < ((absβ(π΅ β πΆ)) / 2))) β π΅ = πΆ)) |
66 | 41, 65 | mpd 15 |
1
β’ (π β π΅ = πΆ) |