Step | Hyp | Ref
| Expression |
1 | | 1rp 12926 |
. . . 4
β’ 1 β
β+ |
2 | 1 | ne0ii 4302 |
. . 3
β’
β+ β β
|
3 | | iscau2 24657 |
. . . 4
β’ (π· β (βMetβπ) β (πΉ β (Cauβπ·) β (πΉ β (π βpm β) β§
βπ₯ β
β+ βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯)))) |
4 | 3 | simplbda 501 |
. . 3
β’ ((π· β (βMetβπ) β§ πΉ β (Cauβπ·)) β βπ₯ β β+ βπ β β€ βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯)) |
5 | | r19.2z 4457 |
. . 3
β’
((β+ β β
β§ βπ₯ β β+ βπ β β€ βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯)) β βπ₯ β β+ βπ β β€ βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯)) |
6 | 2, 4, 5 | sylancr 588 |
. 2
β’ ((π· β (βMetβπ) β§ πΉ β (Cauβπ·)) β βπ₯ β β+ βπ β β€ βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯)) |
7 | | uzid 12785 |
. . . . . 6
β’ (π β β€ β π β
(β€β₯βπ)) |
8 | | ne0i 4299 |
. . . . . 6
β’ (π β
(β€β₯βπ) β (β€β₯βπ) β β
) |
9 | | r19.2z 4457 |
. . . . . . 7
β’
(((β€β₯βπ) β β
β§ βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯)) β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯)) |
10 | 9 | ex 414 |
. . . . . 6
β’
((β€β₯βπ) β β
β (βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯) β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯))) |
11 | 7, 8, 10 | 3syl 18 |
. . . . 5
β’ (π β β€ β
(βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯) β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯))) |
12 | | ne0i 4299 |
. . . . . . 7
β’ ((πΉβπ) β π β π β β
) |
13 | 12 | 3ad2ant2 1135 |
. . . . . 6
β’ ((π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯) β π β β
) |
14 | 13 | rexlimivw 3149 |
. . . . 5
β’
(βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯) β π β β
) |
15 | 11, 14 | syl6 35 |
. . . 4
β’ (π β β€ β
(βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯) β π β β
)) |
16 | 15 | rexlimiv 3146 |
. . 3
β’
(βπ β
β€ βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯) β π β β
) |
17 | 16 | rexlimivw 3149 |
. 2
β’
(βπ₯ β
β+ βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯) β π β β
) |
18 | 6, 17 | syl 17 |
1
β’ ((π· β (βMetβπ) β§ πΉ β (Cauβπ·)) β π β β
) |