Step | Hyp | Ref
| Expression |
1 | | iscau3.2 |
. . . . 5
β’ π =
(β€β₯βπ) |
2 | | iscau3.3 |
. . . . 5
β’ (π β π· β (βMetβπ)) |
3 | | iscau3.4 |
. . . . 5
β’ (π β π β β€) |
4 | 1, 2, 3 | iscau3 24665 |
. . . 4
β’ (π β (πΉ β (Cauβπ·) β (πΉ β (π βpm β) β§
βπ₯ β
β+ βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯)))) |
5 | | simpr 486 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π) β π β π) |
6 | 5, 1 | eleqtrdi 2844 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π) β π β (β€β₯βπ)) |
7 | | eluzelz 12781 |
. . . . . . . . . . . . . 14
β’ (π β
(β€β₯βπ) β π β β€) |
8 | | uzid 12786 |
. . . . . . . . . . . . . 14
β’ (π β β€ β π β
(β€β₯βπ)) |
9 | 6, 7, 8 | 3syl 18 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β π β (β€β₯βπ)) |
10 | | fveq2 6846 |
. . . . . . . . . . . . . . 15
β’ (π = π β (β€β₯βπ) =
(β€β₯βπ)) |
11 | | fveq2 6846 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (πΉβπ) = (πΉβπ)) |
12 | 11 | oveq1d 7376 |
. . . . . . . . . . . . . . . 16
β’ (π = π β ((πΉβπ)π·(πΉβπ)) = ((πΉβπ)π·(πΉβπ))) |
13 | 12 | breq1d 5119 |
. . . . . . . . . . . . . . 15
β’ (π = π β (((πΉβπ)π·(πΉβπ)) < π₯ β ((πΉβπ)π·(πΉβπ)) < π₯)) |
14 | 10, 13 | raleqbidv 3318 |
. . . . . . . . . . . . . 14
β’ (π = π β (βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯ β βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯)) |
15 | 14 | rspcv 3579 |
. . . . . . . . . . . . 13
β’ (π β
(β€β₯βπ) β (βπ β (β€β₯βπ)βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯ β βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯)) |
16 | 9, 15 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β (βπ β (β€β₯βπ)βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯ β βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯)) |
17 | 16 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π)) β (βπ β (β€β₯βπ)βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯ β βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯)) |
18 | | fveq2 6846 |
. . . . . . . . . . . . . . 15
β’ (π = π β (πΉβπ) = (πΉβπ)) |
19 | 18 | oveq2d 7377 |
. . . . . . . . . . . . . 14
β’ (π = π β ((πΉβπ)π·(πΉβπ)) = ((πΉβπ)π·(πΉβπ))) |
20 | 19 | breq1d 5119 |
. . . . . . . . . . . . 13
β’ (π = π β (((πΉβπ)π·(πΉβπ)) < π₯ β ((πΉβπ)π·(πΉβπ)) < π₯)) |
21 | 20 | cbvralvw 3224 |
. . . . . . . . . . . 12
β’
(βπ β
(β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯ β βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯) |
22 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ ((π β dom πΉ β§ (πΉβπ) β π) β (πΉβπ) β π) |
23 | 22 | ralimi 3083 |
. . . . . . . . . . . . . . 15
β’
(βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π) β βπ β (β€β₯βπ)(πΉβπ) β π) |
24 | 11 | eleq1d 2819 |
. . . . . . . . . . . . . . . 16
β’ (π = π β ((πΉβπ) β π β (πΉβπ) β π)) |
25 | 24 | rspcv 3579 |
. . . . . . . . . . . . . . 15
β’ (π β
(β€β₯βπ) β (βπ β (β€β₯βπ)(πΉβπ) β π β (πΉβπ) β π)) |
26 | 9, 23, 25 | syl2im 40 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π) β (βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π) β (πΉβπ) β π)) |
27 | 26 | imp 408 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π) β§ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π)) β (πΉβπ) β π) |
28 | | r19.26 3111 |
. . . . . . . . . . . . . . . 16
β’
(βπ β
(β€β₯βπ)((π β dom πΉ β§ (πΉβπ) β π) β§ ((πΉβπ)π·(πΉβπ)) < π₯) β (βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π) β§ βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯)) |
29 | 2 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π β π) β§ (πΉβπ) β π) β§ (π β dom πΉ β§ (πΉβπ) β π)) β π· β (βMetβπ)) |
30 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π β π) β§ (πΉβπ) β π) β§ (π β dom πΉ β§ (πΉβπ) β π)) β (πΉβπ) β π) |
31 | | simprr 772 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π β π) β§ (πΉβπ) β π) β§ (π β dom πΉ β§ (πΉβπ) β π)) β (πΉβπ) β π) |
32 | | xmetsym 23723 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π· β (βMetβπ) β§ (πΉβπ) β π β§ (πΉβπ) β π) β ((πΉβπ)π·(πΉβπ)) = ((πΉβπ)π·(πΉβπ))) |
33 | 29, 30, 31, 32 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β π) β§ (πΉβπ) β π) β§ (π β dom πΉ β§ (πΉβπ) β π)) β ((πΉβπ)π·(πΉβπ)) = ((πΉβπ)π·(πΉβπ))) |
34 | 33 | breq1d 5119 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β π) β§ (πΉβπ) β π) β§ (π β dom πΉ β§ (πΉβπ) β π)) β (((πΉβπ)π·(πΉβπ)) < π₯ β ((πΉβπ)π·(πΉβπ)) < π₯)) |
35 | 34 | biimpd 228 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β π) β§ (πΉβπ) β π) β§ (π β dom πΉ β§ (πΉβπ) β π)) β (((πΉβπ)π·(πΉβπ)) < π₯ β ((πΉβπ)π·(πΉβπ)) < π₯)) |
36 | 35 | expimpd 455 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β π) β§ (πΉβπ) β π) β (((π β dom πΉ β§ (πΉβπ) β π) β§ ((πΉβπ)π·(πΉβπ)) < π₯) β ((πΉβπ)π·(πΉβπ)) < π₯)) |
37 | 36 | ralimdv 3163 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β π) β§ (πΉβπ) β π) β (βπ β (β€β₯βπ)((π β dom πΉ β§ (πΉβπ) β π) β§ ((πΉβπ)π·(πΉβπ)) < π₯) β βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯)) |
38 | 28, 37 | biimtrrid 242 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β π) β§ (πΉβπ) β π) β ((βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π) β§ βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯) β βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯)) |
39 | 38 | expd 417 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π) β§ (πΉβπ) β π) β (βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π) β (βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯ β βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯))) |
40 | 39 | impancom 453 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π) β§ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π)) β ((πΉβπ) β π β (βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯ β βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯))) |
41 | 27, 40 | mpd 15 |
. . . . . . . . . . . 12
β’ (((π β§ π β π) β§ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π)) β (βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯ β βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯)) |
42 | 21, 41 | biimtrid 241 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π)) β (βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯ β βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯)) |
43 | 17, 42 | syld 47 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π)) β (βπ β (β€β₯βπ)βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯ β βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯)) |
44 | 43 | imdistanda 573 |
. . . . . . . . 9
β’ ((π β§ π β π) β ((βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π) β§ βπ β (β€β₯βπ)βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯) β (βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π) β§ βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯))) |
45 | | r19.26 3111 |
. . . . . . . . 9
β’
(βπ β
(β€β₯βπ)((π β dom πΉ β§ (πΉβπ) β π) β§ βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯) β (βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π) β§ βπ β (β€β₯βπ)βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯)) |
46 | | r19.26 3111 |
. . . . . . . . 9
β’
(βπ β
(β€β₯βπ)((π β dom πΉ β§ (πΉβπ) β π) β§ ((πΉβπ)π·(πΉβπ)) < π₯) β (βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π) β§ βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯)) |
47 | 44, 45, 46 | 3imtr4g 296 |
. . . . . . . 8
β’ ((π β§ π β π) β (βπ β (β€β₯βπ)((π β dom πΉ β§ (πΉβπ) β π) β§ βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯) β βπ β (β€β₯βπ)((π β dom πΉ β§ (πΉβπ) β π) β§ ((πΉβπ)π·(πΉβπ)) < π₯))) |
48 | | df-3an 1090 |
. . . . . . . . 9
β’ ((π β dom πΉ β§ (πΉβπ) β π β§ βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯) β ((π β dom πΉ β§ (πΉβπ) β π) β§ βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯)) |
49 | 48 | ralbii 3093 |
. . . . . . . 8
β’
(βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯) β βπ β (β€β₯βπ)((π β dom πΉ β§ (πΉβπ) β π) β§ βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯)) |
50 | | df-3an 1090 |
. . . . . . . . 9
β’ ((π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯) β ((π β dom πΉ β§ (πΉβπ) β π) β§ ((πΉβπ)π·(πΉβπ)) < π₯)) |
51 | 50 | ralbii 3093 |
. . . . . . . 8
β’
(βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯) β βπ β (β€β₯βπ)((π β dom πΉ β§ (πΉβπ) β π) β§ ((πΉβπ)π·(πΉβπ)) < π₯)) |
52 | 47, 49, 51 | 3imtr4g 296 |
. . . . . . 7
β’ ((π β§ π β π) β (βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯) β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯))) |
53 | 52 | reximdva 3162 |
. . . . . 6
β’ (π β (βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯) β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯))) |
54 | 53 | ralimdv 3163 |
. . . . 5
β’ (π β (βπ₯ β β+
βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯) β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯))) |
55 | 54 | anim2d 613 |
. . . 4
β’ (π β ((πΉ β (π βpm β) β§
βπ₯ β
β+ βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯)) β (πΉ β (π βpm β) β§
βπ₯ β
β+ βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯)))) |
56 | 4, 55 | sylbid 239 |
. . 3
β’ (π β (πΉ β (Cauβπ·) β (πΉ β (π βpm β) β§
βπ₯ β
β+ βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯)))) |
57 | | uzssz 12792 |
. . . . . . . . 9
β’
(β€β₯βπ) β β€ |
58 | 1, 57 | eqsstri 3982 |
. . . . . . . 8
β’ π β
β€ |
59 | | ssrexv 4015 |
. . . . . . . 8
β’ (π β β€ β
(βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯) β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯))) |
60 | 58, 59 | ax-mp 5 |
. . . . . . 7
β’
(βπ β
π βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯) β βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯)) |
61 | 60 | ralimi 3083 |
. . . . . 6
β’
(βπ₯ β
β+ βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯) β βπ₯ β β+ βπ β β€ βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯)) |
62 | 61 | anim2i 618 |
. . . . 5
β’ ((πΉ β (π βpm β) β§
βπ₯ β
β+ βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯)) β (πΉ β (π βpm β) β§
βπ₯ β
β+ βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯))) |
63 | | iscau2 24664 |
. . . . 5
β’ (π· β (βMetβπ) β (πΉ β (Cauβπ·) β (πΉ β (π βpm β) β§
βπ₯ β
β+ βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯)))) |
64 | 62, 63 | syl5ibr 246 |
. . . 4
β’ (π· β (βMetβπ) β ((πΉ β (π βpm β) β§
βπ₯ β
β+ βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯)) β πΉ β (Cauβπ·))) |
65 | 2, 64 | syl 17 |
. . 3
β’ (π β ((πΉ β (π βpm β) β§
βπ₯ β
β+ βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯)) β πΉ β (Cauβπ·))) |
66 | 56, 65 | impbid 211 |
. 2
β’ (π β (πΉ β (Cauβπ·) β (πΉ β (π βpm β) β§
βπ₯ β
β+ βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯)))) |
67 | | simpl 484 |
. . . . . . . . 9
β’ ((π β π β§ π β (β€β₯βπ)) β π β π) |
68 | 1 | uztrn2 12790 |
. . . . . . . . 9
β’ ((π β π β§ π β (β€β₯βπ)) β π β π) |
69 | 67, 68 | jca 513 |
. . . . . . . 8
β’ ((π β π β§ π β (β€β₯βπ)) β (π β π β§ π β π)) |
70 | | iscau4.5 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β (πΉβπ) = π΄) |
71 | 70 | adantrl 715 |
. . . . . . . . . 10
β’ ((π β§ (π β π β§ π β π)) β (πΉβπ) = π΄) |
72 | 71 | eleq1d 2819 |
. . . . . . . . 9
β’ ((π β§ (π β π β§ π β π)) β ((πΉβπ) β π β π΄ β π)) |
73 | | iscau4.6 |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β (πΉβπ) = π΅) |
74 | 73 | adantrr 716 |
. . . . . . . . . . 11
β’ ((π β§ (π β π β§ π β π)) β (πΉβπ) = π΅) |
75 | 71, 74 | oveq12d 7379 |
. . . . . . . . . 10
β’ ((π β§ (π β π β§ π β π)) β ((πΉβπ)π·(πΉβπ)) = (π΄π·π΅)) |
76 | 75 | breq1d 5119 |
. . . . . . . . 9
β’ ((π β§ (π β π β§ π β π)) β (((πΉβπ)π·(πΉβπ)) < π₯ β (π΄π·π΅) < π₯)) |
77 | 72, 76 | 3anbi23d 1440 |
. . . . . . . 8
β’ ((π β§ (π β π β§ π β π)) β ((π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯) β (π β dom πΉ β§ π΄ β π β§ (π΄π·π΅) < π₯))) |
78 | 69, 77 | sylan2 594 |
. . . . . . 7
β’ ((π β§ (π β π β§ π β (β€β₯βπ))) β ((π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯) β (π β dom πΉ β§ π΄ β π β§ (π΄π·π΅) < π₯))) |
79 | 78 | anassrs 469 |
. . . . . 6
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β ((π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯) β (π β dom πΉ β§ π΄ β π β§ (π΄π·π΅) < π₯))) |
80 | 79 | ralbidva 3169 |
. . . . 5
β’ ((π β§ π β π) β (βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯) β βπ β (β€β₯βπ)(π β dom πΉ β§ π΄ β π β§ (π΄π·π΅) < π₯))) |
81 | 80 | rexbidva 3170 |
. . . 4
β’ (π β (βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯) β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ π΄ β π β§ (π΄π·π΅) < π₯))) |
82 | 81 | ralbidv 3171 |
. . 3
β’ (π β (βπ₯ β β+
βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯) β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ π΄ β π β§ (π΄π·π΅) < π₯))) |
83 | 82 | anbi2d 630 |
. 2
β’ (π β ((πΉ β (π βpm β) β§
βπ₯ β
β+ βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯)) β (πΉ β (π βpm β) β§
βπ₯ β
β+ βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ π΄ β π β§ (π΄π·π΅) < π₯)))) |
84 | 66, 83 | bitrd 279 |
1
β’ (π β (πΉ β (Cauβπ·) β (πΉ β (π βpm β) β§
βπ₯ β
β+ βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ π΄ β π β§ (π΄π·π΅) < π₯)))) |