Step | Hyp | Ref
| Expression |
1 | | cfilfil 24654 |
. . 3
β’ ((π· β (βMetβπ) β§ πΉ β (CauFilβπ·)) β πΉ β (Filβπ)) |
2 | | cfil3i 24656 |
. . . . 5
β’ ((π· β (βMetβπ) β§ πΉ β (CauFilβπ·) β§ π β β+) β
βπ₯ β π (π₯(ballβπ·)π) β πΉ) |
3 | 2 | 3expa 1119 |
. . . 4
β’ (((π· β (βMetβπ) β§ πΉ β (CauFilβπ·)) β§ π β β+) β
βπ₯ β π (π₯(ballβπ·)π) β πΉ) |
4 | 3 | ralrimiva 3140 |
. . 3
β’ ((π· β (βMetβπ) β§ πΉ β (CauFilβπ·)) β βπ β β+ βπ₯ β π (π₯(ballβπ·)π) β πΉ) |
5 | 1, 4 | jca 513 |
. 2
β’ ((π· β (βMetβπ) β§ πΉ β (CauFilβπ·)) β (πΉ β (Filβπ) β§ βπ β β+ βπ₯ β π (π₯(ballβπ·)π) β πΉ)) |
6 | | simprl 770 |
. . 3
β’ ((π· β (βMetβπ) β§ (πΉ β (Filβπ) β§ βπ β β+ βπ₯ β π (π₯(ballβπ·)π) β πΉ)) β πΉ β (Filβπ)) |
7 | | rphalfcl 12950 |
. . . . . . . 8
β’ (π β β+
β (π / 2) β
β+) |
8 | 7 | adantl 483 |
. . . . . . 7
β’ (((π· β (βMetβπ) β§ πΉ β (Filβπ)) β§ π β β+) β (π / 2) β
β+) |
9 | | oveq2 7369 |
. . . . . . . . . 10
β’ (π = (π / 2) β (π₯(ballβπ·)π) = (π₯(ballβπ·)(π / 2))) |
10 | 9 | eleq1d 2819 |
. . . . . . . . 9
β’ (π = (π / 2) β ((π₯(ballβπ·)π) β πΉ β (π₯(ballβπ·)(π / 2)) β πΉ)) |
11 | 10 | rexbidv 3172 |
. . . . . . . 8
β’ (π = (π / 2) β (βπ₯ β π (π₯(ballβπ·)π) β πΉ β βπ₯ β π (π₯(ballβπ·)(π / 2)) β πΉ)) |
12 | 11 | rspcv 3579 |
. . . . . . 7
β’ ((π / 2) β β+
β (βπ β
β+ βπ₯ β π (π₯(ballβπ·)π) β πΉ β βπ₯ β π (π₯(ballβπ·)(π / 2)) β πΉ)) |
13 | 8, 12 | syl 17 |
. . . . . 6
β’ (((π· β (βMetβπ) β§ πΉ β (Filβπ)) β§ π β β+) β
(βπ β
β+ βπ₯ β π (π₯(ballβπ·)π) β πΉ β βπ₯ β π (π₯(ballβπ·)(π / 2)) β πΉ)) |
14 | | simprr 772 |
. . . . . . . 8
β’ ((((π· β (βMetβπ) β§ πΉ β (Filβπ)) β§ π β β+) β§ (π₯ β π β§ (π₯(ballβπ·)(π / 2)) β πΉ)) β (π₯(ballβπ·)(π / 2)) β πΉ) |
15 | | simp-4l 782 |
. . . . . . . . . . . 12
β’
(((((π· β
(βMetβπ) β§
πΉ β (Filβπ)) β§ π β β+) β§ (π₯ β π β§ (π₯(ballβπ·)(π / 2)) β πΉ)) β§ (π’ β (π₯(ballβπ·)(π / 2)) β§ π£ β (π₯(ballβπ·)(π / 2)))) β π· β (βMetβπ)) |
16 | | simplrl 776 |
. . . . . . . . . . . 12
β’
(((((π· β
(βMetβπ) β§
πΉ β (Filβπ)) β§ π β β+) β§ (π₯ β π β§ (π₯(ballβπ·)(π / 2)) β πΉ)) β§ (π’ β (π₯(ballβπ·)(π / 2)) β§ π£ β (π₯(ballβπ·)(π / 2)))) β π₯ β π) |
17 | | simpllr 775 |
. . . . . . . . . . . . 13
β’
(((((π· β
(βMetβπ) β§
πΉ β (Filβπ)) β§ π β β+) β§ (π₯ β π β§ (π₯(ballβπ·)(π / 2)) β πΉ)) β§ (π’ β (π₯(ballβπ·)(π / 2)) β§ π£ β (π₯(ballβπ·)(π / 2)))) β π β β+) |
18 | 17 | rpred 12965 |
. . . . . . . . . . . 12
β’
(((((π· β
(βMetβπ) β§
πΉ β (Filβπ)) β§ π β β+) β§ (π₯ β π β§ (π₯(ballβπ·)(π / 2)) β πΉ)) β§ (π’ β (π₯(ballβπ·)(π / 2)) β§ π£ β (π₯(ballβπ·)(π / 2)))) β π β β) |
19 | | simprl 770 |
. . . . . . . . . . . 12
β’
(((((π· β
(βMetβπ) β§
πΉ β (Filβπ)) β§ π β β+) β§ (π₯ β π β§ (π₯(ballβπ·)(π / 2)) β πΉ)) β§ (π’ β (π₯(ballβπ·)(π / 2)) β§ π£ β (π₯(ballβπ·)(π / 2)))) β π’ β (π₯(ballβπ·)(π / 2))) |
20 | | blhalf 23781 |
. . . . . . . . . . . 12
β’ (((π· β (βMetβπ) β§ π₯ β π) β§ (π β β β§ π’ β (π₯(ballβπ·)(π / 2)))) β (π₯(ballβπ·)(π / 2)) β (π’(ballβπ·)π )) |
21 | 15, 16, 18, 19, 20 | syl22anc 838 |
. . . . . . . . . . 11
β’
(((((π· β
(βMetβπ) β§
πΉ β (Filβπ)) β§ π β β+) β§ (π₯ β π β§ (π₯(ballβπ·)(π / 2)) β πΉ)) β§ (π’ β (π₯(ballβπ·)(π / 2)) β§ π£ β (π₯(ballβπ·)(π / 2)))) β (π₯(ballβπ·)(π / 2)) β (π’(ballβπ·)π )) |
22 | | simprr 772 |
. . . . . . . . . . 11
β’
(((((π· β
(βMetβπ) β§
πΉ β (Filβπ)) β§ π β β+) β§ (π₯ β π β§ (π₯(ballβπ·)(π / 2)) β πΉ)) β§ (π’ β (π₯(ballβπ·)(π / 2)) β§ π£ β (π₯(ballβπ·)(π / 2)))) β π£ β (π₯(ballβπ·)(π / 2))) |
23 | 21, 22 | sseldd 3949 |
. . . . . . . . . 10
β’
(((((π· β
(βMetβπ) β§
πΉ β (Filβπ)) β§ π β β+) β§ (π₯ β π β§ (π₯(ballβπ·)(π / 2)) β πΉ)) β§ (π’ β (π₯(ballβπ·)(π / 2)) β§ π£ β (π₯(ballβπ·)(π / 2)))) β π£ β (π’(ballβπ·)π )) |
24 | 17 | rpxrd 12966 |
. . . . . . . . . . 11
β’
(((((π· β
(βMetβπ) β§
πΉ β (Filβπ)) β§ π β β+) β§ (π₯ β π β§ (π₯(ballβπ·)(π / 2)) β πΉ)) β§ (π’ β (π₯(ballβπ·)(π / 2)) β§ π£ β (π₯(ballβπ·)(π / 2)))) β π β β*) |
25 | 17, 7 | syl 17 |
. . . . . . . . . . . . . 14
β’
(((((π· β
(βMetβπ) β§
πΉ β (Filβπ)) β§ π β β+) β§ (π₯ β π β§ (π₯(ballβπ·)(π / 2)) β πΉ)) β§ (π’ β (π₯(ballβπ·)(π / 2)) β§ π£ β (π₯(ballβπ·)(π / 2)))) β (π / 2) β
β+) |
26 | 25 | rpxrd 12966 |
. . . . . . . . . . . . 13
β’
(((((π· β
(βMetβπ) β§
πΉ β (Filβπ)) β§ π β β+) β§ (π₯ β π β§ (π₯(ballβπ·)(π / 2)) β πΉ)) β§ (π’ β (π₯(ballβπ·)(π / 2)) β§ π£ β (π₯(ballβπ·)(π / 2)))) β (π / 2) β
β*) |
27 | | blssm 23794 |
. . . . . . . . . . . . 13
β’ ((π· β (βMetβπ) β§ π₯ β π β§ (π / 2) β β*) β
(π₯(ballβπ·)(π / 2)) β π) |
28 | 15, 16, 26, 27 | syl3anc 1372 |
. . . . . . . . . . . 12
β’
(((((π· β
(βMetβπ) β§
πΉ β (Filβπ)) β§ π β β+) β§ (π₯ β π β§ (π₯(ballβπ·)(π / 2)) β πΉ)) β§ (π’ β (π₯(ballβπ·)(π / 2)) β§ π£ β (π₯(ballβπ·)(π / 2)))) β (π₯(ballβπ·)(π / 2)) β π) |
29 | 28, 19 | sseldd 3949 |
. . . . . . . . . . 11
β’
(((((π· β
(βMetβπ) β§
πΉ β (Filβπ)) β§ π β β+) β§ (π₯ β π β§ (π₯(ballβπ·)(π / 2)) β πΉ)) β§ (π’ β (π₯(ballβπ·)(π / 2)) β§ π£ β (π₯(ballβπ·)(π / 2)))) β π’ β π) |
30 | 28, 22 | sseldd 3949 |
. . . . . . . . . . 11
β’
(((((π· β
(βMetβπ) β§
πΉ β (Filβπ)) β§ π β β+) β§ (π₯ β π β§ (π₯(ballβπ·)(π / 2)) β πΉ)) β§ (π’ β (π₯(ballβπ·)(π / 2)) β§ π£ β (π₯(ballβπ·)(π / 2)))) β π£ β π) |
31 | | elbl2 23766 |
. . . . . . . . . . 11
β’ (((π· β (βMetβπ) β§ π β β*) β§ (π’ β π β§ π£ β π)) β (π£ β (π’(ballβπ·)π ) β (π’π·π£) < π )) |
32 | 15, 24, 29, 30, 31 | syl22anc 838 |
. . . . . . . . . 10
β’
(((((π· β
(βMetβπ) β§
πΉ β (Filβπ)) β§ π β β+) β§ (π₯ β π β§ (π₯(ballβπ·)(π / 2)) β πΉ)) β§ (π’ β (π₯(ballβπ·)(π / 2)) β§ π£ β (π₯(ballβπ·)(π / 2)))) β (π£ β (π’(ballβπ·)π ) β (π’π·π£) < π )) |
33 | 23, 32 | mpbid 231 |
. . . . . . . . 9
β’
(((((π· β
(βMetβπ) β§
πΉ β (Filβπ)) β§ π β β+) β§ (π₯ β π β§ (π₯(ballβπ·)(π / 2)) β πΉ)) β§ (π’ β (π₯(ballβπ·)(π / 2)) β§ π£ β (π₯(ballβπ·)(π / 2)))) β (π’π·π£) < π ) |
34 | 33 | ralrimivva 3194 |
. . . . . . . 8
β’ ((((π· β (βMetβπ) β§ πΉ β (Filβπ)) β§ π β β+) β§ (π₯ β π β§ (π₯(ballβπ·)(π / 2)) β πΉ)) β βπ’ β (π₯(ballβπ·)(π / 2))βπ£ β (π₯(ballβπ·)(π / 2))(π’π·π£) < π ) |
35 | | raleq 3308 |
. . . . . . . . . 10
β’ (π¦ = (π₯(ballβπ·)(π / 2)) β (βπ£ β π¦ (π’π·π£) < π β βπ£ β (π₯(ballβπ·)(π / 2))(π’π·π£) < π )) |
36 | 35 | raleqbi1dv 3306 |
. . . . . . . . 9
β’ (π¦ = (π₯(ballβπ·)(π / 2)) β (βπ’ β π¦ βπ£ β π¦ (π’π·π£) < π β βπ’ β (π₯(ballβπ·)(π / 2))βπ£ β (π₯(ballβπ·)(π / 2))(π’π·π£) < π )) |
37 | 36 | rspcev 3583 |
. . . . . . . 8
β’ (((π₯(ballβπ·)(π / 2)) β πΉ β§ βπ’ β (π₯(ballβπ·)(π / 2))βπ£ β (π₯(ballβπ·)(π / 2))(π’π·π£) < π ) β βπ¦ β πΉ βπ’ β π¦ βπ£ β π¦ (π’π·π£) < π ) |
38 | 14, 34, 37 | syl2anc 585 |
. . . . . . 7
β’ ((((π· β (βMetβπ) β§ πΉ β (Filβπ)) β§ π β β+) β§ (π₯ β π β§ (π₯(ballβπ·)(π / 2)) β πΉ)) β βπ¦ β πΉ βπ’ β π¦ βπ£ β π¦ (π’π·π£) < π ) |
39 | 38 | rexlimdvaa 3150 |
. . . . . 6
β’ (((π· β (βMetβπ) β§ πΉ β (Filβπ)) β§ π β β+) β
(βπ₯ β π (π₯(ballβπ·)(π / 2)) β πΉ β βπ¦ β πΉ βπ’ β π¦ βπ£ β π¦ (π’π·π£) < π )) |
40 | 13, 39 | syld 47 |
. . . . 5
β’ (((π· β (βMetβπ) β§ πΉ β (Filβπ)) β§ π β β+) β
(βπ β
β+ βπ₯ β π (π₯(ballβπ·)π) β πΉ β βπ¦ β πΉ βπ’ β π¦ βπ£ β π¦ (π’π·π£) < π )) |
41 | 40 | ralrimdva 3148 |
. . . 4
β’ ((π· β (βMetβπ) β§ πΉ β (Filβπ)) β (βπ β β+ βπ₯ β π (π₯(ballβπ·)π) β πΉ β βπ β β+ βπ¦ β πΉ βπ’ β π¦ βπ£ β π¦ (π’π·π£) < π )) |
42 | 41 | impr 456 |
. . 3
β’ ((π· β (βMetβπ) β§ (πΉ β (Filβπ) β§ βπ β β+ βπ₯ β π (π₯(ballβπ·)π) β πΉ)) β βπ β β+ βπ¦ β πΉ βπ’ β π¦ βπ£ β π¦ (π’π·π£) < π ) |
43 | | iscfil2 24653 |
. . . 4
β’ (π· β (βMetβπ) β (πΉ β (CauFilβπ·) β (πΉ β (Filβπ) β§ βπ β β+ βπ¦ β πΉ βπ’ β π¦ βπ£ β π¦ (π’π·π£) < π ))) |
44 | 43 | adantr 482 |
. . 3
β’ ((π· β (βMetβπ) β§ (πΉ β (Filβπ) β§ βπ β β+ βπ₯ β π (π₯(ballβπ·)π) β πΉ)) β (πΉ β (CauFilβπ·) β (πΉ β (Filβπ) β§ βπ β β+ βπ¦ β πΉ βπ’ β π¦ βπ£ β π¦ (π’π·π£) < π ))) |
45 | 6, 42, 44 | mpbir2and 712 |
. 2
β’ ((π· β (βMetβπ) β§ (πΉ β (Filβπ) β§ βπ β β+ βπ₯ β π (π₯(ballβπ·)π) β πΉ)) β πΉ β (CauFilβπ·)) |
46 | 5, 45 | impbida 800 |
1
β’ (π· β (βMetβπ) β (πΉ β (CauFilβπ·) β (πΉ β (Filβπ) β§ βπ β β+ βπ₯ β π (π₯(ballβπ·)π) β πΉ))) |