Step | Hyp | Ref
| Expression |
1 | | breq2 5151 |
. . . . . . . . . . 11
β’ (π = π¦ β (((πβπ₯)π·(πβπ€)) < π β ((πβπ₯)π·(πβπ€)) < π¦)) |
2 | 1 | imbi2d 341 |
. . . . . . . . . 10
β’ (π = π¦ β (((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π) β ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π¦))) |
3 | 2 | 2ralbidv 3219 |
. . . . . . . . 9
β’ (π = π¦ β (βπ₯ β π βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π) β βπ₯ β π βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π¦))) |
4 | 3 | rexbidv 3179 |
. . . . . . . 8
β’ (π = π¦ β (βπ§ β β+ βπ₯ β π βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π) β βπ§ β β+ βπ₯ β π βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π¦))) |
5 | 4 | cbvralvw 3235 |
. . . . . . 7
β’
(βπ β
β+ βπ§ β β+ βπ₯ β π βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π) β βπ¦ β β+ βπ§ β β+
βπ₯ β π βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π¦)) |
6 | | r19.12 3312 |
. . . . . . . 8
β’
(βπ§ β
β+ βπ₯ β π βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π¦) β βπ₯ β π βπ§ β β+ βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π¦)) |
7 | 6 | ralimi 3084 |
. . . . . . 7
β’
(βπ¦ β
β+ βπ§ β β+ βπ₯ β π βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π¦) β βπ¦ β β+ βπ₯ β π βπ§ β β+ βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π¦)) |
8 | 5, 7 | sylbi 216 |
. . . . . 6
β’
(βπ β
β+ βπ§ β β+ βπ₯ β π βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π) β βπ¦ β β+ βπ₯ β π βπ§ β β+ βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π¦)) |
9 | | rphalfcl 12997 |
. . . . . . . . 9
β’ (π β β+
β (π / 2) β
β+) |
10 | | breq2 5151 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = (π / 2) β (((πβπ₯)π·(πβπ€)) < π¦ β ((πβπ₯)π·(πβπ€)) < (π / 2))) |
11 | 10 | imbi2d 341 |
. . . . . . . . . . . . . . 15
β’ (π¦ = (π / 2) β (((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π¦) β ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < (π / 2)))) |
12 | 11 | ralbidv 3178 |
. . . . . . . . . . . . . 14
β’ (π¦ = (π / 2) β (βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π¦) β βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < (π / 2)))) |
13 | 12 | rexbidv 3179 |
. . . . . . . . . . . . 13
β’ (π¦ = (π / 2) β (βπ§ β β+ βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π¦) β βπ§ β β+ βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < (π / 2)))) |
14 | 13 | ralbidv 3178 |
. . . . . . . . . . . 12
β’ (π¦ = (π / 2) β (βπ₯ β π βπ§ β β+ βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π¦) β βπ₯ β π βπ§ β β+ βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < (π / 2)))) |
15 | 14 | rspcva 3610 |
. . . . . . . . . . 11
β’ (((π / 2) β β+
β§ βπ¦ β
β+ βπ₯ β π βπ§ β β+ βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π¦)) β βπ₯ β π βπ§ β β+ βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < (π / 2))) |
16 | | heicant.j |
. . . . . . . . . . . . . . 15
β’ (π β (MetOpenβπΆ) β Comp) |
17 | 16 | ad3antrrr 729 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π:πβΆπ) β§ π β β+) β§
βπ₯ β π βπ§ β β+ βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < (π / 2))) β (MetOpenβπΆ) β Comp) |
18 | | heicant.c |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β πΆ β (βMetβπ)) |
19 | 18 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π:πβΆπ) β§ π β β+) β πΆ β (βMetβπ)) |
20 | 19 | anim1i 616 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π:πβΆπ) β§ π β β+) β§ π₯ β π) β (πΆ β (βMetβπ) β§ π₯ β π)) |
21 | | rphalfcl 12997 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π§ β β+
β (π§ / 2) β
β+) |
22 | 21 | rpxrd 13013 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π§ β β+
β (π§ / 2) β
β*) |
23 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(MetOpenβπΆ) =
(MetOpenβπΆ) |
24 | 23 | blopn 23991 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((πΆ β (βMetβπ) β§ π₯ β π β§ (π§ / 2) β β*) β
(π₯(ballβπΆ)(π§ / 2)) β (MetOpenβπΆ)) |
25 | 24 | 3expa 1119 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((πΆ β (βMetβπ) β§ π₯ β π) β§ (π§ / 2) β β*) β
(π₯(ballβπΆ)(π§ / 2)) β (MetOpenβπΆ)) |
26 | 20, 22, 25 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ π:πβΆπ) β§ π β β+) β§ π₯ β π) β§ π§ β β+) β (π₯(ballβπΆ)(π§ / 2)) β (MetOpenβπΆ)) |
27 | 26 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π β§ π:πβΆπ) β§ π β β+) β§ π₯ β π) β§ π§ β β+) β§
βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < (π / 2))) β (π₯(ballβπΆ)(π§ / 2)) β (MetOpenβπΆ)) |
28 | 21 | rpgt0d 13015 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π§ β β+
β 0 < (π§ /
2)) |
29 | 22, 28 | jca 513 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π§ β β+
β ((π§ / 2) β
β* β§ 0 < (π§ / 2))) |
30 | | xblcntr 23899 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((πΆ β (βMetβπ) β§ π₯ β π β§ ((π§ / 2) β β* β§ 0 <
(π§ / 2))) β π₯ β (π₯(ballβπΆ)(π§ / 2))) |
31 | 30 | 3expa 1119 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((πΆ β (βMetβπ) β§ π₯ β π) β§ ((π§ / 2) β β* β§ 0 <
(π§ / 2))) β π₯ β (π₯(ballβπΆ)(π§ / 2))) |
32 | 20, 29, 31 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ π:πβΆπ) β§ π β β+) β§ π₯ β π) β§ π§ β β+) β π₯ β (π₯(ballβπΆ)(π§ / 2))) |
33 | 32 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π β§ π:πβΆπ) β§ π β β+) β§ π₯ β π) β§ π§ β β+) β§
βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < (π / 2))) β π₯ β (π₯(ballβπΆ)(π§ / 2))) |
34 | | opelxpi 5712 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π₯ β π β§ (π§ / 2) β β+) β
β¨π₯, (π§ / 2)β© β (π Γ
β+)) |
35 | 21, 34 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π₯ β π β§ π§ β β+) β
β¨π₯, (π§ / 2)β© β (π Γ
β+)) |
36 | 35 | ad4ant23 752 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π β§ π:πβΆπ) β§ π β β+) β§ π₯ β π) β§ π§ β β+) β§
βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < (π / 2))) β β¨π₯, (π§ / 2)β© β (π Γ
β+)) |
37 | | rpcn 12980 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π§ β β+
β π§ β
β) |
38 | 37 | 2halvesd 12454 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π§ β β+
β ((π§ / 2) + (π§ / 2)) = π§) |
39 | 38 | breq2d 5159 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π§ β β+
β ((π₯πΆπ) < ((π§ / 2) + (π§ / 2)) β (π₯πΆπ) < π§)) |
40 | 39 | imbi1d 342 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π§ β β+
β (((π₯πΆπ) < ((π§ / 2) + (π§ / 2)) β ((πβπ₯)π·(πβπ)) < (π / 2)) β ((π₯πΆπ) < π§ β ((πβπ₯)π·(πβπ)) < (π / 2)))) |
41 | 40 | ralbidv 3178 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π§ β β+
β (βπ β
π ((π₯πΆπ) < ((π§ / 2) + (π§ / 2)) β ((πβπ₯)π·(πβπ)) < (π / 2)) β βπ β π ((π₯πΆπ) < π§ β ((πβπ₯)π·(πβπ)) < (π / 2)))) |
42 | | oveq2 7412 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π = π€ β (π₯πΆπ) = (π₯πΆπ€)) |
43 | 42 | breq1d 5157 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = π€ β ((π₯πΆπ) < π§ β (π₯πΆπ€) < π§)) |
44 | | fveq2 6888 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π = π€ β (πβπ) = (πβπ€)) |
45 | 44 | oveq2d 7420 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π = π€ β ((πβπ₯)π·(πβπ)) = ((πβπ₯)π·(πβπ€))) |
46 | 45 | breq1d 5157 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = π€ β (((πβπ₯)π·(πβπ)) < (π / 2) β ((πβπ₯)π·(πβπ€)) < (π / 2))) |
47 | 43, 46 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = π€ β (((π₯πΆπ) < π§ β ((πβπ₯)π·(πβπ)) < (π / 2)) β ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < (π / 2)))) |
48 | 47 | cbvralvw 3235 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(βπ β
π ((π₯πΆπ) < π§ β ((πβπ₯)π·(πβπ)) < (π / 2)) β βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < (π / 2))) |
49 | 41, 48 | bitrdi 287 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π§ β β+
β (βπ β
π ((π₯πΆπ) < ((π§ / 2) + (π§ / 2)) β ((πβπ₯)π·(πβπ)) < (π / 2)) β βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < (π / 2)))) |
50 | 49 | biimpar 479 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π§ β β+
β§ βπ€ β
π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < (π / 2))) β βπ β π ((π₯πΆπ) < ((π§ / 2) + (π§ / 2)) β ((πβπ₯)π·(πβπ)) < (π / 2))) |
51 | 50 | adantll 713 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π β§ π:πβΆπ) β§ π β β+) β§ π₯ β π) β§ π§ β β+) β§
βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < (π / 2))) β βπ β π ((π₯πΆπ) < ((π§ / 2) + (π§ / 2)) β ((πβπ₯)π·(πβπ)) < (π / 2))) |
52 | | vex 3479 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ π₯ β V |
53 | | ovex 7437 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π§ / 2) β V |
54 | 52, 53 | op1std 7980 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = β¨π₯, (π§ / 2)β© β (1st
βπ) = π₯) |
55 | 52, 53 | op2ndd 7981 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = β¨π₯, (π§ / 2)β© β (2nd
βπ) = (π§ / 2)) |
56 | 54, 55 | oveq12d 7422 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = β¨π₯, (π§ / 2)β© β ((1st
βπ)(ballβπΆ)(2nd βπ)) = (π₯(ballβπΆ)(π§ / 2))) |
57 | 56 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = β¨π₯, (π§ / 2)β© β (π₯(ballβπΆ)(π§ / 2)) = ((1st βπ)(ballβπΆ)(2nd βπ))) |
58 | 57 | biantrurd 534 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = β¨π₯, (π§ / 2)β© β (βπ β π (((1st βπ)πΆπ) < ((2nd βπ) + (2nd βπ)) β ((πβ(1st βπ))π·(πβπ)) < (π / 2)) β ((π₯(ballβπΆ)(π§ / 2)) = ((1st βπ)(ballβπΆ)(2nd βπ)) β§ βπ β π (((1st βπ)πΆπ) < ((2nd βπ) + (2nd βπ)) β ((πβ(1st βπ))π·(πβπ)) < (π / 2))))) |
59 | 54 | oveq1d 7419 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = β¨π₯, (π§ / 2)β© β ((1st
βπ)πΆπ) = (π₯πΆπ)) |
60 | 55, 55 | oveq12d 7422 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = β¨π₯, (π§ / 2)β© β ((2nd
βπ) + (2nd
βπ)) = ((π§ / 2) + (π§ / 2))) |
61 | 59, 60 | breq12d 5160 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = β¨π₯, (π§ / 2)β© β (((1st
βπ)πΆπ) < ((2nd βπ) + (2nd βπ)) β (π₯πΆπ) < ((π§ / 2) + (π§ / 2)))) |
62 | 54 | fveq2d 6892 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π = β¨π₯, (π§ / 2)β© β (πβ(1st βπ)) = (πβπ₯)) |
63 | 62 | oveq1d 7419 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = β¨π₯, (π§ / 2)β© β ((πβ(1st βπ))π·(πβπ)) = ((πβπ₯)π·(πβπ))) |
64 | 63 | breq1d 5157 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = β¨π₯, (π§ / 2)β© β (((πβ(1st βπ))π·(πβπ)) < (π / 2) β ((πβπ₯)π·(πβπ)) < (π / 2))) |
65 | 61, 64 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = β¨π₯, (π§ / 2)β© β ((((1st
βπ)πΆπ) < ((2nd βπ) + (2nd βπ)) β ((πβ(1st βπ))π·(πβπ)) < (π / 2)) β ((π₯πΆπ) < ((π§ / 2) + (π§ / 2)) β ((πβπ₯)π·(πβπ)) < (π / 2)))) |
66 | 65 | ralbidv 3178 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = β¨π₯, (π§ / 2)β© β (βπ β π (((1st βπ)πΆπ) < ((2nd βπ) + (2nd βπ)) β ((πβ(1st βπ))π·(πβπ)) < (π / 2)) β βπ β π ((π₯πΆπ) < ((π§ / 2) + (π§ / 2)) β ((πβπ₯)π·(πβπ)) < (π / 2)))) |
67 | 58, 66 | bitr3d 281 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = β¨π₯, (π§ / 2)β© β (((π₯(ballβπΆ)(π§ / 2)) = ((1st βπ)(ballβπΆ)(2nd βπ)) β§ βπ β π (((1st βπ)πΆπ) < ((2nd βπ) + (2nd βπ)) β ((πβ(1st βπ))π·(πβπ)) < (π / 2))) β βπ β π ((π₯πΆπ) < ((π§ / 2) + (π§ / 2)) β ((πβπ₯)π·(πβπ)) < (π / 2)))) |
68 | 67 | rspcev 3612 |
. . . . . . . . . . . . . . . . . . . 20
β’
((β¨π₯, (π§ / 2)β© β (π Γ β+)
β§ βπ β
π ((π₯πΆπ) < ((π§ / 2) + (π§ / 2)) β ((πβπ₯)π·(πβπ)) < (π / 2))) β βπ β (π Γ β+)((π₯(ballβπΆ)(π§ / 2)) = ((1st βπ)(ballβπΆ)(2nd βπ)) β§ βπ β π (((1st βπ)πΆπ) < ((2nd βπ) + (2nd βπ)) β ((πβ(1st βπ))π·(πβπ)) < (π / 2)))) |
69 | 36, 51, 68 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π β§ π:πβΆπ) β§ π β β+) β§ π₯ β π) β§ π§ β β+) β§
βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < (π / 2))) β βπ β (π Γ β+)((π₯(ballβπΆ)(π§ / 2)) = ((1st βπ)(ballβπΆ)(2nd βπ)) β§ βπ β π (((1st βπ)πΆπ) < ((2nd βπ) + (2nd βπ)) β ((πβ(1st βπ))π·(πβπ)) < (π / 2)))) |
70 | | eleq2 2823 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (π₯(ballβπΆ)(π§ / 2)) β (π₯ β π β π₯ β (π₯(ballβπΆ)(π§ / 2)))) |
71 | | eqeq1 2737 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = (π₯(ballβπΆ)(π§ / 2)) β (π = ((1st βπ)(ballβπΆ)(2nd βπ)) β (π₯(ballβπΆ)(π§ / 2)) = ((1st βπ)(ballβπΆ)(2nd βπ)))) |
72 | 71 | anbi1d 631 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = (π₯(ballβπΆ)(π§ / 2)) β ((π = ((1st βπ)(ballβπΆ)(2nd βπ)) β§ βπ β π (((1st βπ)πΆπ) < ((2nd βπ) + (2nd βπ)) β ((πβ(1st βπ))π·(πβπ)) < (π / 2))) β ((π₯(ballβπΆ)(π§ / 2)) = ((1st βπ)(ballβπΆ)(2nd βπ)) β§ βπ β π (((1st βπ)πΆπ) < ((2nd βπ) + (2nd βπ)) β ((πβ(1st βπ))π·(πβπ)) < (π / 2))))) |
73 | 72 | rexbidv 3179 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (π₯(ballβπΆ)(π§ / 2)) β (βπ β (π Γ β+)(π = ((1st βπ)(ballβπΆ)(2nd βπ)) β§ βπ β π (((1st βπ)πΆπ) < ((2nd βπ) + (2nd βπ)) β ((πβ(1st βπ))π·(πβπ)) < (π / 2))) β βπ β (π Γ β+)((π₯(ballβπΆ)(π§ / 2)) = ((1st βπ)(ballβπΆ)(2nd βπ)) β§ βπ β π (((1st βπ)πΆπ) < ((2nd βπ) + (2nd βπ)) β ((πβ(1st βπ))π·(πβπ)) < (π / 2))))) |
74 | 70, 73 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = (π₯(ballβπΆ)(π§ / 2)) β ((π₯ β π β§ βπ β (π Γ β+)(π = ((1st βπ)(ballβπΆ)(2nd βπ)) β§ βπ β π (((1st βπ)πΆπ) < ((2nd βπ) + (2nd βπ)) β ((πβ(1st βπ))π·(πβπ)) < (π / 2)))) β (π₯ β (π₯(ballβπΆ)(π§ / 2)) β§ βπ β (π Γ β+)((π₯(ballβπΆ)(π§ / 2)) = ((1st βπ)(ballβπΆ)(2nd βπ)) β§ βπ β π (((1st βπ)πΆπ) < ((2nd βπ) + (2nd βπ)) β ((πβ(1st βπ))π·(πβπ)) < (π / 2)))))) |
75 | 74 | rspcev 3612 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π₯(ballβπΆ)(π§ / 2)) β (MetOpenβπΆ) β§ (π₯ β (π₯(ballβπΆ)(π§ / 2)) β§ βπ β (π Γ β+)((π₯(ballβπΆ)(π§ / 2)) = ((1st βπ)(ballβπΆ)(2nd βπ)) β§ βπ β π (((1st βπ)πΆπ) < ((2nd βπ) + (2nd βπ)) β ((πβ(1st βπ))π·(πβπ)) < (π / 2))))) β βπ β (MetOpenβπΆ)(π₯ β π β§ βπ β (π Γ β+)(π = ((1st βπ)(ballβπΆ)(2nd βπ)) β§ βπ β π (((1st βπ)πΆπ) < ((2nd βπ) + (2nd βπ)) β ((πβ(1st βπ))π·(πβπ)) < (π / 2))))) |
76 | 27, 33, 69, 75 | syl12anc 836 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π β§ π:πβΆπ) β§ π β β+) β§ π₯ β π) β§ π§ β β+) β§
βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < (π / 2))) β βπ β (MetOpenβπΆ)(π₯ β π β§ βπ β (π Γ β+)(π = ((1st βπ)(ballβπΆ)(2nd βπ)) β§ βπ β π (((1st βπ)πΆπ) < ((2nd βπ) + (2nd βπ)) β ((πβ(1st βπ))π·(πβπ)) < (π / 2))))) |
77 | 76 | rexlimdva2 3158 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π:πβΆπ) β§ π β β+) β§ π₯ β π) β (βπ§ β β+ βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < (π / 2)) β βπ β (MetOpenβπΆ)(π₯ β π β§ βπ β (π Γ β+)(π = ((1st βπ)(ballβπΆ)(2nd βπ)) β§ βπ β π (((1st βπ)πΆπ) < ((2nd βπ) + (2nd βπ)) β ((πβ(1st βπ))π·(πβπ)) < (π / 2)))))) |
78 | 77 | ralimdva 3168 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π:πβΆπ) β§ π β β+) β
(βπ₯ β π βπ§ β β+ βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < (π / 2)) β βπ₯ β π βπ β (MetOpenβπΆ)(π₯ β π β§ βπ β (π Γ β+)(π = ((1st βπ)(ballβπΆ)(2nd βπ)) β§ βπ β π (((1st βπ)πΆπ) < ((2nd βπ) + (2nd βπ)) β ((πβ(1st βπ))π·(πβπ)) < (π / 2)))))) |
79 | 78 | imp 408 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π:πβΆπ) β§ π β β+) β§
βπ₯ β π βπ§ β β+ βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < (π / 2))) β βπ₯ β π βπ β (MetOpenβπΆ)(π₯ β π β§ βπ β (π Γ β+)(π = ((1st βπ)(ballβπΆ)(2nd βπ)) β§ βπ β π (((1st βπ)πΆπ) < ((2nd βπ) + (2nd βπ)) β ((πβ(1st βπ))π·(πβπ)) < (π / 2))))) |
80 | 23 | mopnuni 23929 |
. . . . . . . . . . . . . . . . . 18
β’ (πΆ β (βMetβπ) β π = βͺ
(MetOpenβπΆ)) |
81 | 18, 80 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β π = βͺ
(MetOpenβπΆ)) |
82 | 81 | raleqdv 3326 |
. . . . . . . . . . . . . . . 16
β’ (π β (βπ₯ β π βπ β (MetOpenβπΆ)(π₯ β π β§ βπ β (π Γ β+)(π = ((1st βπ)(ballβπΆ)(2nd βπ)) β§ βπ β π (((1st βπ)πΆπ) < ((2nd βπ) + (2nd βπ)) β ((πβ(1st βπ))π·(πβπ)) < (π / 2)))) β βπ₯ β βͺ
(MetOpenβπΆ)βπ β (MetOpenβπΆ)(π₯ β π β§ βπ β (π Γ β+)(π = ((1st βπ)(ballβπΆ)(2nd βπ)) β§ βπ β π (((1st βπ)πΆπ) < ((2nd βπ) + (2nd βπ)) β ((πβ(1st βπ))π·(πβπ)) < (π / 2)))))) |
83 | 82 | ad3antrrr 729 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π:πβΆπ) β§ π β β+) β§
βπ₯ β π βπ§ β β+ βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < (π / 2))) β (βπ₯ β π βπ β (MetOpenβπΆ)(π₯ β π β§ βπ β (π Γ β+)(π = ((1st βπ)(ballβπΆ)(2nd βπ)) β§ βπ β π (((1st βπ)πΆπ) < ((2nd βπ) + (2nd βπ)) β ((πβ(1st βπ))π·(πβπ)) < (π / 2)))) β βπ₯ β βͺ
(MetOpenβπΆ)βπ β (MetOpenβπΆ)(π₯ β π β§ βπ β (π Γ β+)(π = ((1st βπ)(ballβπΆ)(2nd βπ)) β§ βπ β π (((1st βπ)πΆπ) < ((2nd βπ) + (2nd βπ)) β ((πβ(1st βπ))π·(πβπ)) < (π / 2)))))) |
84 | 79, 83 | mpbid 231 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π:πβΆπ) β§ π β β+) β§
βπ₯ β π βπ§ β β+ βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < (π / 2))) β βπ₯ β βͺ
(MetOpenβπΆ)βπ β (MetOpenβπΆ)(π₯ β π β§ βπ β (π Γ β+)(π = ((1st βπ)(ballβπΆ)(2nd βπ)) β§ βπ β π (((1st βπ)πΆπ) < ((2nd βπ) + (2nd βπ)) β ((πβ(1st βπ))π·(πβπ)) < (π / 2))))) |
85 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’ βͺ (MetOpenβπΆ) = βͺ
(MetOpenβπΆ) |
86 | | fveq2 6888 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (πβπ) β (1st βπ) = (1st
β(πβπ))) |
87 | | fveq2 6888 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (πβπ) β (2nd βπ) = (2nd
β(πβπ))) |
88 | 86, 87 | oveq12d 7422 |
. . . . . . . . . . . . . . . . 17
β’ (π = (πβπ) β ((1st βπ)(ballβπΆ)(2nd βπ)) = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) |
89 | 88 | eqeq2d 2744 |
. . . . . . . . . . . . . . . 16
β’ (π = (πβπ) β (π = ((1st βπ)(ballβπΆ)(2nd βπ)) β π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ))))) |
90 | 86 | oveq1d 7419 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (πβπ) β ((1st βπ)πΆπ) = ((1st β(πβπ))πΆπ)) |
91 | 87, 87 | oveq12d 7422 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (πβπ) β ((2nd βπ) + (2nd βπ)) = ((2nd
β(πβπ)) + (2nd
β(πβπ)))) |
92 | 90, 91 | breq12d 5160 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (πβπ) β (((1st βπ)πΆπ) < ((2nd βπ) + (2nd βπ)) β ((1st
β(πβπ))πΆπ) < ((2nd β(πβπ)) + (2nd β(πβπ))))) |
93 | 86 | fveq2d 6892 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = (πβπ) β (πβ(1st βπ)) = (πβ(1st β(πβπ)))) |
94 | 93 | oveq1d 7419 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (πβπ) β ((πβ(1st βπ))π·(πβπ)) = ((πβ(1st β(πβπ)))π·(πβπ))) |
95 | 94 | breq1d 5157 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (πβπ) β (((πβ(1st βπ))π·(πβπ)) < (π / 2) β ((πβ(1st β(πβπ)))π·(πβπ)) < (π / 2))) |
96 | 92, 95 | imbi12d 345 |
. . . . . . . . . . . . . . . . 17
β’ (π = (πβπ) β ((((1st βπ)πΆπ) < ((2nd βπ) + (2nd βπ)) β ((πβ(1st βπ))π·(πβπ)) < (π / 2)) β (((1st β(πβπ))πΆπ) < ((2nd β(πβπ)) + (2nd β(πβπ))) β ((πβ(1st β(πβπ)))π·(πβπ)) < (π / 2)))) |
97 | 96 | ralbidv 3178 |
. . . . . . . . . . . . . . . 16
β’ (π = (πβπ) β (βπ β π (((1st βπ)πΆπ) < ((2nd βπ) + (2nd βπ)) β ((πβ(1st βπ))π·(πβπ)) < (π / 2)) β βπ β π (((1st β(πβπ))πΆπ) < ((2nd β(πβπ)) + (2nd β(πβπ))) β ((πβ(1st β(πβπ)))π·(πβπ)) < (π / 2)))) |
98 | 89, 97 | anbi12d 632 |
. . . . . . . . . . . . . . 15
β’ (π = (πβπ) β ((π = ((1st βπ)(ballβπΆ)(2nd βπ)) β§ βπ β π (((1st βπ)πΆπ) < ((2nd βπ) + (2nd βπ)) β ((πβ(1st βπ))π·(πβπ)) < (π / 2))) β (π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ))) β§ βπ β π (((1st β(πβπ))πΆπ) < ((2nd β(πβπ)) + (2nd β(πβπ))) β ((πβ(1st β(πβπ)))π·(πβπ)) < (π / 2))))) |
99 | 85, 98 | cmpcovf 22877 |
. . . . . . . . . . . . . 14
β’
(((MetOpenβπΆ)
β Comp β§ βπ₯
β βͺ (MetOpenβπΆ)βπ β (MetOpenβπΆ)(π₯ β π β§ βπ β (π Γ β+)(π = ((1st βπ)(ballβπΆ)(2nd βπ)) β§ βπ β π (((1st βπ)πΆπ) < ((2nd βπ) + (2nd βπ)) β ((πβ(1st βπ))π·(πβπ)) < (π / 2))))) β βπ β (π« (MetOpenβπΆ) β© Fin)(βͺ (MetOpenβπΆ) = βͺ π β§ βπ(π:π βΆ(π Γ β+) β§
βπ β π (π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ))) β§ βπ β π (((1st β(πβπ))πΆπ) < ((2nd β(πβπ)) + (2nd β(πβπ))) β ((πβ(1st β(πβπ)))π·(πβπ)) < (π / 2)))))) |
100 | 17, 84, 99 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((((π β§ π:πβΆπ) β§ π β β+) β§
βπ₯ β π βπ§ β β+ βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < (π / 2))) β βπ β (π« (MetOpenβπΆ) β© Fin)(βͺ (MetOpenβπΆ) = βͺ π β§ βπ(π:π βΆ(π Γ β+) β§
βπ β π (π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ))) β§ βπ β π (((1st β(πβπ))πΆπ) < ((2nd β(πβπ)) + (2nd β(πβπ))) β ((πβ(1st β(πβπ)))π·(πβπ)) < (π / 2)))))) |
101 | 100 | ex 414 |
. . . . . . . . . . . 12
β’ (((π β§ π:πβΆπ) β§ π β β+) β
(βπ₯ β π βπ§ β β+ βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < (π / 2)) β βπ β (π« (MetOpenβπΆ) β© Fin)(βͺ (MetOpenβπΆ) = βͺ π β§ βπ(π:π βΆ(π Γ β+) β§
βπ β π (π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ))) β§ βπ β π (((1st β(πβπ))πΆπ) < ((2nd β(πβπ)) + (2nd β(πβπ))) β ((πβ(1st β(πβπ)))π·(πβπ)) < (π / 2))))))) |
102 | | elinel2 4195 |
. . . . . . . . . . . . . 14
β’ (π β (π«
(MetOpenβπΆ) β©
Fin) β π β
Fin) |
103 | | simpll 766 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π:πβΆπ) β§ π β β+) β π) |
104 | 103 | anim1i 616 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π:πβΆπ) β§ π β β+) β§ π β Fin) β (π β§ π β Fin)) |
105 | | frn 6721 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π:π βΆ(π Γ β+) β ran
π β (π Γ
β+)) |
106 | | rnss 5936 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (ran
π β (π Γ β+)
β ran ran π β
ran (π Γ
β+)) |
107 | 105, 106 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π:π βΆ(π Γ β+) β ran ran
π β ran (π Γ
β+)) |
108 | | rnxpss 6168 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ran
(π Γ
β+) β β+ |
109 | 107, 108 | sstrdi 3993 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π:π βΆ(π Γ β+) β ran ran
π β
β+) |
110 | 109 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π β Fin) β§ βͺ (MetOpenβπΆ) = βͺ π ) β§ π:π βΆ(π Γ β+)) β ran
ran π β
β+) |
111 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π β Fin) β§ βͺ (MetOpenβπΆ) = βͺ π ) β π β Fin) |
112 | | ffun 6717 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π:π βΆ(π Γ β+) β Fun
π) |
113 | | vex 3479 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ π β V |
114 | 113 | fundmen 9027 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (Fun
π β dom π β π) |
115 | 114 | ensymd 8997 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (Fun
π β π β dom π) |
116 | 112, 115 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π:π βΆ(π Γ β+) β π β dom π) |
117 | | fdm 6723 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π:π βΆ(π Γ β+) β dom
π = π ) |
118 | 116, 117 | breqtrd 5173 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π:π βΆ(π Γ β+) β π β π ) |
119 | | enfii 9185 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β Fin β§ π β π ) β π β Fin) |
120 | 118, 119 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β Fin β§ π:π βΆ(π Γ β+)) β π β Fin) |
121 | | rnfi 9331 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β Fin β ran π β Fin) |
122 | | rnfi 9331 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (ran
π β Fin β ran ran
π β
Fin) |
123 | 120, 121,
122 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β Fin β§ π:π βΆ(π Γ β+)) β ran
ran π β
Fin) |
124 | 111, 123 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π β Fin) β§ βͺ (MetOpenβπΆ) = βͺ π ) β§ π:π βΆ(π Γ β+)) β ran
ran π β
Fin) |
125 | 117 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ βͺ (MetOpenβπΆ) = βͺ π ) β§ π:π βΆ(π Γ β+)) β dom
π = π ) |
126 | | eqtr 2756 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π = βͺ
(MetOpenβπΆ) β§
βͺ (MetOpenβπΆ) = βͺ π ) β π = βͺ π ) |
127 | 81, 126 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β§ βͺ (MetOpenβπΆ) = βͺ π ) β π = βͺ π ) |
128 | | heicant.x |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π β π β β
) |
129 | 128 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β§ βͺ (MetOpenβπΆ) = βͺ π ) β π β β
) |
130 | 127, 129 | eqnetrrd 3010 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ βͺ (MetOpenβπΆ) = βͺ π ) β βͺ π
β β
) |
131 | | unieq 4918 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π = β
β βͺ π =
βͺ β
) |
132 | | uni0 4938 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ βͺ β
= β
|
133 | 131, 132 | eqtrdi 2789 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π = β
β βͺ π =
β
) |
134 | 133 | necon3i 2974 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (βͺ π
β β
β π β
β
) |
135 | 130, 134 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ βͺ (MetOpenβπΆ) = βͺ π ) β π β β
) |
136 | 135 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ βͺ (MetOpenβπΆ) = βͺ π ) β§ π:π βΆ(π Γ β+)) β π β β
) |
137 | 125, 136 | eqnetrd 3009 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ βͺ (MetOpenβπΆ) = βͺ π ) β§ π:π βΆ(π Γ β+)) β dom
π β
β
) |
138 | | dm0rn0 5922 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (dom
π = β
β ran
π =
β
) |
139 | 138 | necon3bii 2994 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (dom
π β β
β ran
π β
β
) |
140 | 137, 139 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ βͺ (MetOpenβπΆ) = βͺ π ) β§ π:π βΆ(π Γ β+)) β ran
π β
β
) |
141 | | relxp 5693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ Rel
(π Γ
β+) |
142 | | relss 5779 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (ran
π β (π Γ β+)
β (Rel (π Γ
β+) β Rel ran π)) |
143 | 105, 141,
142 | mpisyl 21 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π:π βΆ(π Γ β+) β Rel ran
π) |
144 | | relrn0 5966 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (Rel ran
π β (ran π = β
β ran ran π = β
)) |
145 | 144 | necon3bid 2986 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (Rel ran
π β (ran π β β
β ran ran
π β
β
)) |
146 | 143, 145 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π:π βΆ(π Γ β+) β (ran
π β β
β ran
ran π β
β
)) |
147 | 146 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ βͺ (MetOpenβπΆ) = βͺ π ) β§ π:π βΆ(π Γ β+)) β (ran
π β β
β ran
ran π β
β
)) |
148 | 140, 147 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ βͺ (MetOpenβπΆ) = βͺ π ) β§ π:π βΆ(π Γ β+)) β ran
ran π β
β
) |
149 | 148 | adantllr 718 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π β Fin) β§ βͺ (MetOpenβπΆ) = βͺ π ) β§ π:π βΆ(π Γ β+)) β ran
ran π β
β
) |
150 | | rpssre 12977 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
β+ β β |
151 | 110, 150 | sstrdi 3993 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π β Fin) β§ βͺ (MetOpenβπΆ) = βͺ π ) β§ π:π βΆ(π Γ β+)) β ran
ran π β
β) |
152 | | ltso 11290 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ < Or
β |
153 | | fiinfcl 9492 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (( <
Or β β§ (ran ran π
β Fin β§ ran ran π
β β
β§ ran ran π β β)) β inf(ran ran π, β, < ) β ran ran
π) |
154 | 152, 153 | mpan 689 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((ran ran
π β Fin β§ ran ran
π β β
β§ ran
ran π β β)
β inf(ran ran π,
β, < ) β ran ran π) |
155 | 124, 149,
151, 154 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π β Fin) β§ βͺ (MetOpenβπΆ) = βͺ π ) β§ π:π βΆ(π Γ β+)) β
inf(ran ran π, β,
< ) β ran ran π) |
156 | 110, 155 | sseldd 3982 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β Fin) β§ βͺ (MetOpenβπΆ) = βͺ π ) β§ π:π βΆ(π Γ β+)) β
inf(ran ran π, β,
< ) β β+) |
157 | 104, 156 | sylanl1 679 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π β§ π:πβΆπ) β§ π β β+) β§ π β Fin) β§ βͺ (MetOpenβπΆ) = βͺ π ) β§ π:π βΆ(π Γ β+)) β
inf(ran ran π, β,
< ) β β+) |
158 | 157 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’
(((((((π β§ π:πβΆπ) β§ π β β+) β§ π β Fin) β§ βͺ (MetOpenβπΆ) = βͺ π ) β§ π:π βΆ(π Γ β+)) β§
βπ β π (π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ))) β§ βπ β π (((1st β(πβπ))πΆπ) < ((2nd β(πβπ)) + (2nd β(πβπ))) β ((πβ(1st β(πβπ)))π·(πβπ)) < (π / 2)))) β inf(ran ran π, β, < ) β
β+) |
159 | 81 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π:πβΆπ) β§ π β β+) β§ π β Fin) β π = βͺ
(MetOpenβπΆ)) |
160 | 159 | anim1i 616 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π β§ π:πβΆπ) β§ π β β+) β§ π β Fin) β§ βͺ (MetOpenβπΆ) = βͺ π ) β (π = βͺ
(MetOpenβπΆ) β§
βͺ (MetOpenβπΆ) = βͺ π )) |
161 | 160 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((((π β§ π:πβΆπ) β§ π β β+) β§ π β Fin) β§ βͺ (MetOpenβπΆ) = βͺ π ) β§ π:π βΆ(π Γ β+)) β§
βπ β π (π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ))) β§ βπ β π (((1st β(πβπ))πΆπ) < ((2nd β(πβπ)) + (2nd β(πβπ))) β ((πβ(1st β(πβπ)))π·(πβπ)) < (π / 2)))) β (π = βͺ
(MetOpenβπΆ) β§
βͺ (MetOpenβπΆ) = βͺ π )) |
162 | | simpl 484 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π₯ β π β§ π€ β π) β π₯ β π) |
163 | 126 | eleq2d 2820 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π = βͺ
(MetOpenβπΆ) β§
βͺ (MetOpenβπΆ) = βͺ π ) β (π₯ β π β π₯ β βͺ π )) |
164 | | eluni2 4911 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π₯ β βͺ π
β βπ β
π π₯ β π) |
165 | 163, 164 | bitrdi 287 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π = βͺ
(MetOpenβπΆ) β§
βͺ (MetOpenβπΆ) = βͺ π ) β (π₯ β π β βπ β π π₯ β π)) |
166 | 165 | biimpa 478 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π = βͺ
(MetOpenβπΆ) β§
βͺ (MetOpenβπΆ) = βͺ π ) β§ π₯ β π) β βπ β π π₯ β π) |
167 | 161, 162,
166 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((((π β§ π:πβΆπ) β§ π β β+) β§ π β Fin) β§ βͺ (MetOpenβπΆ) = βͺ π ) β§ π:π βΆ(π Γ β+)) β§
βπ β π (π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ))) β§ βπ β π (((1st β(πβπ))πΆπ) < ((2nd β(πβπ)) + (2nd β(πβπ))) β ((πβ(1st β(πβπ)))π·(πβπ)) < (π / 2)))) β§ (π₯ β π β§ π€ β π)) β βπ β π π₯ β π) |
168 | | nfv 1918 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
β²π(((((π β§ π:πβΆπ) β§ π β β+) β§ π β Fin) β§ βͺ (MetOpenβπΆ) = βͺ π ) β§ π:π βΆ(π Γ
β+)) |
169 | | nfra1 3282 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
β²πβπ β π (π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ))) β§ βπ β π (((1st β(πβπ))πΆπ) < ((2nd β(πβπ)) + (2nd β(πβπ))) β ((πβ(1st β(πβπ)))π·(πβπ)) < (π / 2))) |
170 | 168, 169 | nfan 1903 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
β²π((((((π β§ π:πβΆπ) β§ π β β+) β§ π β Fin) β§ βͺ (MetOpenβπΆ) = βͺ π ) β§ π:π βΆ(π Γ β+)) β§
βπ β π (π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ))) β§ βπ β π (((1st β(πβπ))πΆπ) < ((2nd β(πβπ)) + (2nd β(πβπ))) β ((πβ(1st β(πβπ)))π·(πβπ)) < (π / 2)))) |
171 | | nfv 1918 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
β²π(π₯ β π β§ π€ β π) |
172 | 170, 171 | nfan 1903 |
. . . . . . . . . . . . . . . . . . . . 21
β’
β²π(((((((π β§ π:πβΆπ) β§ π β β+) β§ π β Fin) β§ βͺ (MetOpenβπΆ) = βͺ π ) β§ π:π βΆ(π Γ β+)) β§
βπ β π (π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ))) β§ βπ β π (((1st β(πβπ))πΆπ) < ((2nd β(πβπ)) + (2nd β(πβπ))) β ((πβ(1st β(πβπ)))π·(πβπ)) < (π / 2)))) β§ (π₯ β π β§ π€ β π)) |
173 | | nfv 1918 |
. . . . . . . . . . . . . . . . . . . . 21
β’
β²π((π₯πΆπ€) < inf(ran ran π, β, < ) β ((πβπ₯)π·(πβπ€)) < π) |
174 | | rspa 3246 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((βπ β
π (π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ))) β§ βπ β π (((1st β(πβπ))πΆπ) < ((2nd β(πβπ)) + (2nd β(πβπ))) β ((πβ(1st β(πβπ)))π·(πβπ)) < (π / 2))) β§ π β π ) β (π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ))) β§ βπ β π (((1st β(πβπ))πΆπ) < ((2nd β(πβπ)) + (2nd β(πβπ))) β ((πβ(1st β(πβπ)))π·(πβπ)) < (π / 2)))) |
175 | | oveq2 7412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π = π₯ β ((1st β(πβπ))πΆπ) = ((1st β(πβπ))πΆπ₯)) |
176 | 175 | breq1d 5157 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π = π₯ β (((1st β(πβπ))πΆπ) < ((2nd β(πβπ)) + (2nd β(πβπ))) β ((1st β(πβπ))πΆπ₯) < ((2nd β(πβπ)) + (2nd β(πβπ))))) |
177 | | fveq2 6888 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (π = π₯ β (πβπ) = (πβπ₯)) |
178 | 177 | oveq2d 7420 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π = π₯ β ((πβ(1st β(πβπ)))π·(πβπ)) = ((πβ(1st β(πβπ)))π·(πβπ₯))) |
179 | 178 | breq1d 5157 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π = π₯ β (((πβ(1st β(πβπ)))π·(πβπ)) < (π / 2) β ((πβ(1st β(πβπ)))π·(πβπ₯)) < (π / 2))) |
180 | 176, 179 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π = π₯ β ((((1st β(πβπ))πΆπ) < ((2nd β(πβπ)) + (2nd β(πβπ))) β ((πβ(1st β(πβπ)))π·(πβπ)) < (π / 2)) β (((1st β(πβπ))πΆπ₯) < ((2nd β(πβπ)) + (2nd β(πβπ))) β ((πβ(1st β(πβπ)))π·(πβπ₯)) < (π / 2)))) |
181 | 180 | rspcva 3610 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π₯ β π β§ βπ β π (((1st β(πβπ))πΆπ) < ((2nd β(πβπ)) + (2nd β(πβπ))) β ((πβ(1st β(πβπ)))π·(πβπ)) < (π / 2))) β (((1st
β(πβπ))πΆπ₯) < ((2nd β(πβπ)) + (2nd β(πβπ))) β ((πβ(1st β(πβπ)))π·(πβπ₯)) < (π / 2))) |
182 | | oveq2 7412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π = π€ β ((1st β(πβπ))πΆπ) = ((1st β(πβπ))πΆπ€)) |
183 | 182 | breq1d 5157 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π = π€ β (((1st β(πβπ))πΆπ) < ((2nd β(πβπ)) + (2nd β(πβπ))) β ((1st β(πβπ))πΆπ€) < ((2nd β(πβπ)) + (2nd β(πβπ))))) |
184 | 44 | oveq2d 7420 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π = π€ β ((πβ(1st β(πβπ)))π·(πβπ)) = ((πβ(1st β(πβπ)))π·(πβπ€))) |
185 | 184 | breq1d 5157 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π = π€ β (((πβ(1st β(πβπ)))π·(πβπ)) < (π / 2) β ((πβ(1st β(πβπ)))π·(πβπ€)) < (π / 2))) |
186 | 183, 185 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π = π€ β ((((1st β(πβπ))πΆπ) < ((2nd β(πβπ)) + (2nd β(πβπ))) β ((πβ(1st β(πβπ)))π·(πβπ)) < (π / 2)) β (((1st β(πβπ))πΆπ€) < ((2nd β(πβπ)) + (2nd β(πβπ))) β ((πβ(1st β(πβπ)))π·(πβπ€)) < (π / 2)))) |
187 | 186 | rspcva 3610 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π€ β π β§ βπ β π (((1st β(πβπ))πΆπ) < ((2nd β(πβπ)) + (2nd β(πβπ))) β ((πβ(1st β(πβπ)))π·(πβπ)) < (π / 2))) β (((1st
β(πβπ))πΆπ€) < ((2nd β(πβπ)) + (2nd β(πβπ))) β ((πβ(1st β(πβπ)))π·(πβπ€)) < (π / 2))) |
188 | 181, 187 | anim12i 614 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (((π₯ β π β§ βπ β π (((1st β(πβπ))πΆπ) < ((2nd β(πβπ)) + (2nd β(πβπ))) β ((πβ(1st β(πβπ)))π·(πβπ)) < (π / 2))) β§ (π€ β π β§ βπ β π (((1st β(πβπ))πΆπ) < ((2nd β(πβπ)) + (2nd β(πβπ))) β ((πβ(1st β(πβπ)))π·(πβπ)) < (π / 2)))) β ((((1st
β(πβπ))πΆπ₯) < ((2nd β(πβπ)) + (2nd β(πβπ))) β ((πβ(1st β(πβπ)))π·(πβπ₯)) < (π / 2)) β§ (((1st β(πβπ))πΆπ€) < ((2nd β(πβπ)) + (2nd β(πβπ))) β ((πβ(1st β(πβπ)))π·(πβπ€)) < (π / 2)))) |
189 | 188 | anandirs 678 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π₯ β π β§ π€ β π) β§ βπ β π (((1st β(πβπ))πΆπ) < ((2nd β(πβπ)) + (2nd β(πβπ))) β ((πβ(1st β(πβπ)))π·(πβπ)) < (π / 2))) β ((((1st
β(πβπ))πΆπ₯) < ((2nd β(πβπ)) + (2nd β(πβπ))) β ((πβ(1st β(πβπ)))π·(πβπ₯)) < (π / 2)) β§ (((1st β(πβπ))πΆπ€) < ((2nd β(πβπ)) + (2nd β(πβπ))) β ((πβ(1st β(πβπ)))π·(πβπ€)) < (π / 2)))) |
190 | | anim12 808 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
(((((1st β(πβπ))πΆπ₯) < ((2nd β(πβπ)) + (2nd β(πβπ))) β ((πβ(1st β(πβπ)))π·(πβπ₯)) < (π / 2)) β§ (((1st β(πβπ))πΆπ€) < ((2nd β(πβπ)) + (2nd β(πβπ))) β ((πβ(1st β(πβπ)))π·(πβπ€)) < (π / 2))) β ((((1st
β(πβπ))πΆπ₯) < ((2nd β(πβπ)) + (2nd β(πβπ))) β§ ((1st β(πβπ))πΆπ€) < ((2nd β(πβπ)) + (2nd β(πβπ)))) β (((πβ(1st β(πβπ)))π·(πβπ₯)) < (π / 2) β§ ((πβ(1st β(πβπ)))π·(πβπ€)) < (π / 2)))) |
191 | 189, 190 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π₯ β π β§ π€ β π) β§ βπ β π (((1st β(πβπ))πΆπ) < ((2nd β(πβπ)) + (2nd β(πβπ))) β ((πβ(1st β(πβπ)))π·(πβπ)) < (π / 2))) β ((((1st
β(πβπ))πΆπ₯) < ((2nd β(πβπ)) + (2nd β(πβπ))) β§ ((1st β(πβπ))πΆπ€) < ((2nd β(πβπ)) + (2nd β(πβπ)))) β (((πβ(1st β(πβπ)))π·(πβπ₯)) < (π / 2) β§ ((πβ(1st β(πβπ)))π·(πβπ€)) < (π / 2)))) |
192 | 191 | adantrl 715 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π₯ β π β§ π€ β π) β§ (π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ))) β§ βπ β π (((1st β(πβπ))πΆπ) < ((2nd β(πβπ)) + (2nd β(πβπ))) β ((πβ(1st β(πβπ)))π·(πβπ)) < (π / 2)))) β ((((1st
β(πβπ))πΆπ₯) < ((2nd β(πβπ)) + (2nd β(πβπ))) β§ ((1st β(πβπ))πΆπ€) < ((2nd β(πβπ)) + (2nd β(πβπ)))) β (((πβ(1st β(πβπ)))π·(πβπ₯)) < (π / 2) β§ ((πβ(1st β(πβπ)))π·(πβπ€)) < (π / 2)))) |
193 | 192 | ad4ant23 752 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((((((((π β§ π:πβΆπ) β§ π β β+) β§ π β Fin) β§ βͺ (MetOpenβπΆ) = βͺ π ) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ (π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ))) β§ βπ β π (((1st β(πβπ))πΆπ) < ((2nd β(πβπ)) + (2nd β(πβπ))) β ((πβ(1st β(πβπ)))π·(πβπ)) < (π / 2)))) β§ (π β π β§ π₯ β π)) β ((((1st β(πβπ))πΆπ₯) < ((2nd β(πβπ)) + (2nd β(πβπ))) β§ ((1st β(πβπ))πΆπ€) < ((2nd β(πβπ)) + (2nd β(πβπ)))) β (((πβ(1st β(πβπ)))π·(πβπ₯)) < (π / 2) β§ ((πβ(1st β(πβπ)))π·(πβπ€)) < (π / 2)))) |
194 | | simpll 766 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’
(((((π β§ π:πβΆπ) β§ π β β+) β§ π β Fin) β§ βͺ (MetOpenβπΆ) = βͺ π ) β ((π β§ π:πβΆπ) β§ π β
β+)) |
195 | 194 | anim1i 616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
((((((π β§ π:πβΆπ) β§ π β β+) β§ π β Fin) β§ βͺ (MetOpenβπΆ) = βͺ π ) β§ π:π βΆ(π Γ β+)) β
(((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ
β+))) |
196 | 195 | anim1i 616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
(((((((π β§ π:πβΆπ) β§ π β β+) β§ π β Fin) β§ βͺ (MetOpenβπΆ) = βͺ π ) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β ((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π))) |
197 | 109, 150 | sstrdi 3993 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (π:π βΆ(π Γ β+) β ran ran
π β
β) |
198 | 197 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((π:π βΆ(π Γ β+) β§ π β π ) β ran ran π β β) |
199 | | 0re 11212 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ 0 β
β |
200 | | rpge0 12983 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ (π¦ β β+
β 0 β€ π¦) |
201 | 200 | rgen 3064 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’
βπ¦ β
β+ 0 β€ π¦ |
202 | | ssralv 4049 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ (ran ran
π β
β+ β (βπ¦ β β+ 0 β€ π¦ β βπ¦ β ran ran π0 β€ π¦)) |
203 | 109, 201,
202 | mpisyl 21 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ (π:π βΆ(π Γ β+) β
βπ¦ β ran ran
π0 β€ π¦) |
204 | | breq1 5150 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ (π₯ = 0 β (π₯ β€ π¦ β 0 β€ π¦)) |
205 | 204 | ralbidv 3178 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ (π₯ = 0 β (βπ¦ β ran ran π π₯ β€ π¦ β βπ¦ β ran ran π0 β€ π¦)) |
206 | 205 | rspcev 3612 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ ((0
β β β§ βπ¦ β ran ran π0 β€ π¦) β βπ₯ β β βπ¦ β ran ran π π₯ β€ π¦) |
207 | 199, 203,
206 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (π:π βΆ(π Γ β+) β
βπ₯ β β
βπ¦ β ran ran
π π₯ β€ π¦) |
208 | 207 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((π:π βΆ(π Γ β+) β§ π β π ) β βπ₯ β β βπ¦ β ran ran π π₯ β€ π¦) |
209 | 143 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ ((π:π βΆ(π Γ β+) β§ π β π ) β Rel ran π) |
210 | | ffn 6714 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ (π:π βΆ(π Γ β+) β π Fn π ) |
211 | | fnfvelrn 7078 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ ((π Fn π β§ π β π ) β (πβπ) β ran π) |
212 | 210, 211 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ ((π:π βΆ(π Γ β+) β§ π β π ) β (πβπ) β ran π) |
213 | | 2ndrn 8022 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ ((Rel ran
π β§ (πβπ) β ran π) β (2nd β(πβπ)) β ran ran π) |
214 | 209, 212,
213 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((π:π βΆ(π Γ β+) β§ π β π ) β (2nd β(πβπ)) β ran ran π) |
215 | | infrelb 12195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((ran ran
π β β β§
βπ₯ β β
βπ¦ β ran ran
π π₯ β€ π¦ β§ (2nd β(πβπ)) β ran ran π) β inf(ran ran π, β, < ) β€ (2nd
β(πβπ))) |
216 | 198, 208,
214, 215 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ ((π:π βΆ(π Γ β+) β§ π β π ) β inf(ran ran π, β, < ) β€ (2nd
β(πβπ))) |
217 | 216 | adantll 713 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’
(((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ π β π ) β inf(ran ran π, β, < ) β€ (2nd
β(πβπ))) |
218 | 217 | ad2ant2r 746 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’
((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ (π β π β§ π₯ β π)) β inf(ran ran π, β, < ) β€ (2nd
β(πβπ))) |
219 | 18 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β πΆ β (βMetβπ)) |
220 | | xmetcl 23819 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ ((πΆ β (βMetβπ) β§ π₯ β π β§ π€ β π) β (π₯πΆπ€) β
β*) |
221 | 220 | 3expb 1121 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((πΆ β (βMetβπ) β§ (π₯ β π β§ π€ β π)) β (π₯πΆπ€) β
β*) |
222 | 219, 221 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’
(((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β (π₯πΆπ€) β
β*) |
223 | 222 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’
((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ (π β π β§ π₯ β π)) β (π₯πΆπ€) β
β*) |
224 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’
(((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β π:π βΆ(π Γ
β+)) |
225 | | simpl 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ ((π β π β§ π₯ β π) β π β π ) |
226 | 214 | ne0d 4334 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ ((π:π βΆ(π Γ β+) β§ π β π ) β ran ran π β β
) |
227 | | infrecl 12192 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ ((ran ran
π β β β§ ran
ran π β β
β§
βπ₯ β β
βπ¦ β ran ran
π π₯ β€ π¦) β inf(ran ran π, β, < ) β
β) |
228 | 198, 226,
208, 227 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((π:π βΆ(π Γ β+) β§ π β π ) β inf(ran ran π, β, < ) β
β) |
229 | 228 | rexrd 11260 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ ((π:π βΆ(π Γ β+) β§ π β π ) β inf(ran ran π, β, < ) β
β*) |
230 | 224, 225,
229 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’
((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ (π β π β§ π₯ β π)) β inf(ran ran π, β, < ) β
β*) |
231 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ ((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β π:π βΆ(π Γ
β+)) |
232 | 231 | ffvelcdmda 7082 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’
(((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ π β π ) β (πβπ) β (π Γ
β+)) |
233 | | xp2nd 8003 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ ((πβπ) β (π Γ β+) β
(2nd β(πβπ)) β
β+) |
234 | 232, 233 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’
(((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ π β π ) β (2nd β(πβπ)) β
β+) |
235 | 234 | rpxrd 13013 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’
(((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ π β π ) β (2nd β(πβπ)) β
β*) |
236 | 235 | ad2ant2r 746 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’
((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ (π β π β§ π₯ β π)) β (2nd β(πβπ)) β
β*) |
237 | | xrltletr 13132 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (((π₯πΆπ€) β β* β§ inf(ran
ran π, β, < )
β β* β§ (2nd β(πβπ)) β β*) β
(((π₯πΆπ€) < inf(ran ran π, β, < ) β§ inf(ran ran π, β, < ) β€
(2nd β(πβπ))) β (π₯πΆπ€) < (2nd β(πβπ)))) |
238 | 223, 230,
236, 237 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’
((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ (π β π β§ π₯ β π)) β (((π₯πΆπ€) < inf(ran ran π, β, < ) β§ inf(ran ran π, β, < ) β€
(2nd β(πβπ))) β (π₯πΆπ€) < (2nd β(πβπ)))) |
239 | 218, 238 | mpan2d 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’
((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ (π β π β§ π₯ β π)) β ((π₯πΆπ€) < inf(ran ran π, β, < ) β (π₯πΆπ€) < (2nd β(πβπ)))) |
240 | 239 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’
(((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β ((π₯πΆπ€) < inf(ran ran π, β, < ) β (π₯πΆπ€) < (2nd β(πβπ)))) |
241 | 18 | ad6antr 735 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’
(((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β πΆ β (βMetβπ)) |
242 | | simpllr 775 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’
((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β π:π βΆ(π Γ
β+)) |
243 | | ffvelcdm 7079 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ ((π:π βΆ(π Γ β+) β§ π β π ) β (πβπ) β (π Γ
β+)) |
244 | | xp1st 8002 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ ((πβπ) β (π Γ β+) β
(1st β(πβπ)) β π) |
245 | 243, 244 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ ((π:π βΆ(π Γ β+) β§ π β π ) β (1st β(πβπ)) β π) |
246 | 242, 225,
245 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’
(((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β (1st β(πβπ)) β π) |
247 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ ((π₯ β π β§ π€ β π) β π€ β π) |
248 | 247 | ad3antlr 730 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’
(((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β π€ β π) |
249 | | xmetcl 23819 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((πΆ β (βMetβπ) β§ (1st
β(πβπ)) β π β§ π€ β π) β ((1st β(πβπ))πΆπ€) β
β*) |
250 | 241, 246,
248, 249 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’
(((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β ((1st β(πβπ))πΆπ€) β
β*) |
251 | 250 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’
((((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β§ (π₯πΆπ€) < (2nd β(πβπ))) β ((1st β(πβπ))πΆπ€) β
β*) |
252 | 243, 233 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ ((π:π βΆ(π Γ β+) β§ π β π ) β (2nd β(πβπ)) β
β+) |
253 | 224, 252 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’
((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π β π ) β (2nd β(πβπ)) β
β+) |
254 | 253 | ad2ant2r 746 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’
(((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β (2nd β(πβπ)) β
β+) |
255 | 254 | rpred 13012 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’
(((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β (2nd β(πβπ)) β β) |
256 | 162 | ad3antlr 730 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’
(((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β π₯ β π) |
257 | | xmetcl 23819 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ ((πΆ β (βMetβπ) β§ (1st
β(πβπ)) β π β§ π₯ β π) β ((1st β(πβπ))πΆπ₯) β
β*) |
258 | 241, 246,
256, 257 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’
(((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β ((1st β(πβπ))πΆπ₯) β
β*) |
259 | 252 | rpxrd 13013 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ ((π:π βΆ(π Γ β+) β§ π β π ) β (2nd β(πβπ)) β
β*) |
260 | 242, 225,
259 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’
(((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β (2nd β(πβπ)) β
β*) |
261 | | eleq2 2823 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
β’ (π = ((1st
β(πβπ))(ballβπΆ)(2nd β(πβπ))) β (π₯ β π β π₯ β ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ))))) |
262 | 18 | ad5antr 733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
β’
((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π β π ) β πΆ β (βMetβπ)) |
263 | 224, 245 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
β’
((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π β π ) β (1st β(πβπ)) β π) |
264 | 253 | rpxrd 13013 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
β’
((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π β π ) β (2nd β(πβπ)) β
β*) |
265 | | elbl 23876 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
β’ ((πΆ β (βMetβπ) β§ (1st
β(πβπ)) β π β§ (2nd β(πβπ)) β β*) β (π₯ β ((1st
β(πβπ))(ballβπΆ)(2nd β(πβπ))) β (π₯ β π β§ ((1st β(πβπ))πΆπ₯) < (2nd β(πβπ))))) |
266 | 262, 263,
264, 265 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
β’
((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π β π ) β (π₯ β ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ))) β (π₯ β π β§ ((1st β(πβπ))πΆπ₯) < (2nd β(πβπ))))) |
267 | 261, 266 | sylan9bbr 512 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’
(((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π β π ) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β (π₯ β π β (π₯ β π β§ ((1st β(πβπ))πΆπ₯) < (2nd β(πβπ))))) |
268 | 267 | biimpd 228 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’
(((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π β π ) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β (π₯ β π β (π₯ β π β§ ((1st β(πβπ))πΆπ₯) < (2nd β(πβπ))))) |
269 | 268 | an32s 651 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’
(((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ π β π ) β (π₯ β π β (π₯ β π β§ ((1st β(πβπ))πΆπ₯) < (2nd β(πβπ))))) |
270 | 269 | impr 456 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’
(((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β (π₯ β π β§ ((1st β(πβπ))πΆπ₯) < (2nd β(πβπ)))) |
271 | 270 | simprd 497 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’
(((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β ((1st β(πβπ))πΆπ₯) < (2nd β(πβπ))) |
272 | 258, 260,
271 | xrltled 13125 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’
(((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β ((1st β(πβπ))πΆπ₯) β€ (2nd β(πβπ))) |
273 | 224 | ffvelcdmda 7082 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’
((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π β π ) β (πβπ) β (π Γ
β+)) |
274 | 273, 244 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’
((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π β π ) β (1st β(πβπ)) β π) |
275 | | simplrl 776 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’
((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π β π ) β π₯ β π) |
276 | 262, 274,
275, 257 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’
((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π β π ) β ((1st β(πβπ))πΆπ₯) β
β*) |
277 | | xmetge0 23832 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ ((πΆ β (βMetβπ) β§ (1st
β(πβπ)) β π β§ π₯ β π) β 0 β€ ((1st
β(πβπ))πΆπ₯)) |
278 | 262, 274,
275, 277 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’
((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π β π ) β 0 β€ ((1st
β(πβπ))πΆπ₯)) |
279 | | xrrege0 13149 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’
(((((1st β(πβπ))πΆπ₯) β β* β§
(2nd β(πβπ)) β β) β§ (0 β€
((1st β(πβπ))πΆπ₯) β§ ((1st β(πβπ))πΆπ₯) β€ (2nd β(πβπ)))) β ((1st β(πβπ))πΆπ₯) β β) |
280 | 279 | an4s 659 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’
(((((1st β(πβπ))πΆπ₯) β β* β§ 0 β€
((1st β(πβπ))πΆπ₯)) β§ ((2nd β(πβπ)) β β β§ ((1st
β(πβπ))πΆπ₯) β€ (2nd β(πβπ)))) β ((1st β(πβπ))πΆπ₯) β β) |
281 | 280 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’
((((1st β(πβπ))πΆπ₯) β β* β§ 0 β€
((1st β(πβπ))πΆπ₯)) β (((2nd β(πβπ)) β β β§ ((1st
β(πβπ))πΆπ₯) β€ (2nd β(πβπ))) β ((1st β(πβπ))πΆπ₯) β β)) |
282 | 276, 278,
281 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’
((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π β π ) β (((2nd β(πβπ)) β β β§ ((1st
β(πβπ))πΆπ₯) β€ (2nd β(πβπ))) β ((1st β(πβπ))πΆπ₯) β β)) |
283 | 282 | ad2ant2r 746 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’
(((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β (((2nd β(πβπ)) β β β§ ((1st
β(πβπ))πΆπ₯) β€ (2nd β(πβπ))) β ((1st β(πβπ))πΆπ₯) β β)) |
284 | 255, 272,
283 | mp2and 698 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’
(((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β ((1st β(πβπ))πΆπ₯) β β) |
285 | 284 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’
((((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β§ (π₯πΆπ€) < (2nd β(πβπ))) β ((1st β(πβπ))πΆπ₯) β β) |
286 | | xrltle 13124 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ (((π₯πΆπ€) β β* β§
(2nd β(πβπ)) β β*) β ((π₯πΆπ€) < (2nd β(πβπ)) β (π₯πΆπ€) β€ (2nd β(πβπ)))) |
287 | 223, 236,
286 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’
((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ (π β π β§ π₯ β π)) β ((π₯πΆπ€) < (2nd β(πβπ)) β (π₯πΆπ€) β€ (2nd β(πβπ)))) |
288 | | xmetge0 23832 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ ((πΆ β (βMetβπ) β§ π₯ β π β§ π€ β π) β 0 β€ (π₯πΆπ€)) |
289 | 288 | 3expb 1121 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’ ((πΆ β (βMetβπ) β§ (π₯ β π β§ π€ β π)) β 0 β€ (π₯πΆπ€)) |
290 | 219, 289 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’
(((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β 0 β€ (π₯πΆπ€)) |
291 | 290 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’
((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ (π β π β§ π₯ β π)) β 0 β€ (π₯πΆπ€)) |
292 | 234 | rpred 13012 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’
(((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ π β π ) β (2nd β(πβπ)) β β) |
293 | 292 | ad2ant2r 746 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’
((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ (π β π β§ π₯ β π)) β (2nd β(πβπ)) β β) |
294 | | xrrege0 13149 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’ ((((π₯πΆπ€) β β* β§
(2nd β(πβπ)) β β) β§ (0 β€ (π₯πΆπ€) β§ (π₯πΆπ€) β€ (2nd β(πβπ)))) β (π₯πΆπ€) β β) |
295 | 294 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ (((π₯πΆπ€) β β* β§
(2nd β(πβπ)) β β) β ((0 β€ (π₯πΆπ€) β§ (π₯πΆπ€) β€ (2nd β(πβπ))) β (π₯πΆπ€) β β)) |
296 | 223, 293,
295 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’
((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ (π β π β§ π₯ β π)) β ((0 β€ (π₯πΆπ€) β§ (π₯πΆπ€) β€ (2nd β(πβπ))) β (π₯πΆπ€) β β)) |
297 | 291, 296 | mpand 694 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’
((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ (π β π β§ π₯ β π)) β ((π₯πΆπ€) β€ (2nd β(πβπ)) β (π₯πΆπ€) β β)) |
298 | 287, 297 | syld 47 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’
((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ (π β π β§ π₯ β π)) β ((π₯πΆπ€) < (2nd β(πβπ)) β (π₯πΆπ€) β β)) |
299 | 298 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’
(((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β ((π₯πΆπ€) < (2nd β(πβπ)) β (π₯πΆπ€) β β)) |
300 | 299 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’
((((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β§ (π₯πΆπ€) < (2nd β(πβπ))) β (π₯πΆπ€) β β) |
301 | 285, 300 | readdcld 11239 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’
((((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β§ (π₯πΆπ€) < (2nd β(πβπ))) β (((1st β(πβπ))πΆπ₯) + (π₯πΆπ€)) β β) |
302 | 301 | rexrd 11260 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’
((((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β§ (π₯πΆπ€) < (2nd β(πβπ))) β (((1st β(πβπ))πΆπ₯) + (π₯πΆπ€)) β
β*) |
303 | 254, 254 | rpaddcld 13027 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’
(((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β ((2nd β(πβπ)) + (2nd β(πβπ))) β
β+) |
304 | 303 | rpxrd 13013 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’
(((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β ((2nd β(πβπ)) + (2nd β(πβπ))) β
β*) |
305 | 304 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’
((((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β§ (π₯πΆπ€) < (2nd β(πβπ))) β ((2nd β(πβπ)) + (2nd β(πβπ))) β
β*) |
306 | | xmettri 23839 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ ((πΆ β (βMetβπ) β§ ((1st
β(πβπ)) β π β§ π€ β π β§ π₯ β π)) β ((1st β(πβπ))πΆπ€) β€ (((1st β(πβπ))πΆπ₯) +π (π₯πΆπ€))) |
307 | 241, 246,
248, 256, 306 | syl13anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’
(((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β ((1st β(πβπ))πΆπ€) β€ (((1st β(πβπ))πΆπ₯) +π (π₯πΆπ€))) |
308 | 307 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’
((((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β§ (π₯πΆπ€) < (2nd β(πβπ))) β ((1st β(πβπ))πΆπ€) β€ (((1st β(πβπ))πΆπ₯) +π (π₯πΆπ€))) |
309 | | rexadd 13207 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’
((((1st β(πβπ))πΆπ₯) β β β§ (π₯πΆπ€) β β) β (((1st
β(πβπ))πΆπ₯) +π (π₯πΆπ€)) = (((1st β(πβπ))πΆπ₯) + (π₯πΆπ€))) |
310 | 285, 300,
309 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’
((((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β§ (π₯πΆπ€) < (2nd β(πβπ))) β (((1st β(πβπ))πΆπ₯) +π (π₯πΆπ€)) = (((1st β(πβπ))πΆπ₯) + (π₯πΆπ€))) |
311 | 308, 310 | breqtrd 5173 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’
((((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β§ (π₯πΆπ€) < (2nd β(πβπ))) β ((1st β(πβπ))πΆπ€) β€ (((1st β(πβπ))πΆπ₯) + (π₯πΆπ€))) |
312 | 255 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’
((((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β§ (π₯πΆπ€) < (2nd β(πβπ))) β (2nd β(πβπ)) β β) |
313 | 271 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’
((((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β§ (π₯πΆπ€) < (2nd β(πβπ))) β ((1st β(πβπ))πΆπ₯) < (2nd β(πβπ))) |
314 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’
((((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β§ (π₯πΆπ€) < (2nd β(πβπ))) β (π₯πΆπ€) < (2nd β(πβπ))) |
315 | 285, 300,
312, 312, 313, 314 | lt2addd 11833 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’
((((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β§ (π₯πΆπ€) < (2nd β(πβπ))) β (((1st β(πβπ))πΆπ₯) + (π₯πΆπ€)) < ((2nd β(πβπ)) + (2nd β(πβπ)))) |
316 | 251, 302,
305, 311, 315 | xrlelttrd 13135 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’
((((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β§ (π₯πΆπ€) < (2nd β(πβπ))) β ((1st β(πβπ))πΆπ€) < ((2nd β(πβπ)) + (2nd β(πβπ)))) |
317 | 316 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’
(((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β ((π₯πΆπ€) < (2nd β(πβπ)) β ((1st β(πβπ))πΆπ€) < ((2nd β(πβπ)) + (2nd β(πβπ))))) |
318 | 252 | rpred 13012 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ ((π:π βΆ(π Γ β+) β§ π β π ) β (2nd β(πβπ)) β β) |
319 | 318, 252 | ltaddrpd 13045 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((π:π βΆ(π Γ β+) β§ π β π ) β (2nd β(πβπ)) < ((2nd β(πβπ)) + (2nd β(πβπ)))) |
320 | 242, 225,
319 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’
(((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β (2nd β(πβπ)) < ((2nd β(πβπ)) + (2nd β(πβπ)))) |
321 | 258, 260,
304, 271, 320 | xrlttrd 13134 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’
(((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β ((1st β(πβπ))πΆπ₯) < ((2nd β(πβπ)) + (2nd β(πβπ)))) |
322 | 317, 321 | jctild 527 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’
(((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β ((π₯πΆπ€) < (2nd β(πβπ)) β (((1st β(πβπ))πΆπ₯) < ((2nd β(πβπ)) + (2nd β(πβπ))) β§ ((1st β(πβπ))πΆπ€) < ((2nd β(πβπ)) + (2nd β(πβπ)))))) |
323 | 240, 322 | syld 47 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
(((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β ((π₯πΆπ€) < inf(ran ran π, β, < ) β (((1st
β(πβπ))πΆπ₯) < ((2nd β(πβπ)) + (2nd β(πβπ))) β§ ((1st β(πβπ))πΆπ€) < ((2nd β(πβπ)) + (2nd β(πβπ)))))) |
324 | | simpll 766 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β (π β§ π:πβΆπ)) |
325 | | heicant.d |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (π β π· β (βMetβπ)) |
326 | | ffvelcdm 7079 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ ((π:πβΆπ β§ π₯ β π) β (πβπ₯) β π) |
327 | | ffvelcdm 7079 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ ((π:πβΆπ β§ π€ β π) β (πβπ€) β π) |
328 | 326, 327 | anim12dan 620 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((π:πβΆπ β§ (π₯ β π β§ π€ β π)) β ((πβπ₯) β π β§ (πβπ€) β π)) |
329 | | xmetcl 23819 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ ((π· β (βMetβπ) β§ (πβπ₯) β π β§ (πβπ€) β π) β ((πβπ₯)π·(πβπ€)) β
β*) |
330 | 329 | 3expb 1121 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((π· β (βMetβπ) β§ ((πβπ₯) β π β§ (πβπ€) β π)) β ((πβπ₯)π·(πβπ€)) β
β*) |
331 | 325, 328,
330 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ ((π β§ (π:πβΆπ β§ (π₯ β π β§ π€ β π))) β ((πβπ₯)π·(πβπ€)) β
β*) |
332 | 331 | anassrs 469 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (((π β§ π:πβΆπ) β§ (π₯ β π β§ π€ β π)) β ((πβπ₯)π·(πβπ€)) β
β*) |
333 | 324, 332 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’
(((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β ((πβπ₯)π·(πβπ€)) β
β*) |
334 | 333 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’
((((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β§ (((πβ(1st β(πβπ)))π·(πβπ₯)) < (π / 2) β§ ((πβ(1st β(πβπ)))π·(πβπ€)) < (π / 2))) β ((πβπ₯)π·(πβπ€)) β
β*) |
335 | 325 | ad5antr 733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’
((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π β π ) β π· β (βMetβπ)) |
336 | | simp-5r 785 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’
((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π β π ) β π:πβΆπ) |
337 | 336, 274 | ffvelcdmd 7083 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’
((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π β π ) β (πβ(1st β(πβπ))) β π) |
338 | | simpllr 775 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ ((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β π:πβΆπ) |
339 | 338 | ffvelcdmda 7082 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’
(((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ π₯ β π) β (πβπ₯) β π) |
340 | 339 | adantrr 716 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’
(((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β (πβπ₯) β π) |
341 | 340 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’
((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π β π ) β (πβπ₯) β π) |
342 | | xmetcl 23819 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ ((π· β (βMetβπ) β§ (πβ(1st β(πβπ))) β π β§ (πβπ₯) β π) β ((πβ(1st β(πβπ)))π·(πβπ₯)) β
β*) |
343 | 335, 337,
341, 342 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’
((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π β π ) β ((πβ(1st β(πβπ)))π·(πβπ₯)) β
β*) |
344 | 9 | rpxrd 13013 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ (π β β+
β (π / 2) β
β*) |
345 | 344 | ad4antlr 732 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’
((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π β π ) β (π / 2) β
β*) |
346 | | xrltle 13124 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ ((((πβ(1st
β(πβπ)))π·(πβπ₯)) β β* β§ (π / 2) β
β*) β (((πβ(1st β(πβπ)))π·(πβπ₯)) < (π / 2) β ((πβ(1st β(πβπ)))π·(πβπ₯)) β€ (π / 2))) |
347 | 343, 345,
346 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’
((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π β π ) β (((πβ(1st β(πβπ)))π·(πβπ₯)) < (π / 2) β ((πβ(1st β(πβπ)))π·(πβπ₯)) β€ (π / 2))) |
348 | | xmetge0 23832 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ ((π· β (βMetβπ) β§ (πβ(1st β(πβπ))) β π β§ (πβπ₯) β π) β 0 β€ ((πβ(1st β(πβπ)))π·(πβπ₯))) |
349 | 335, 337,
341, 348 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’
((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π β π ) β 0 β€ ((πβ(1st β(πβπ)))π·(πβπ₯))) |
350 | 9 | rpred 13012 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ (π β β+
β (π / 2) β
β) |
351 | 350 | ad4antlr 732 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’
((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π β π ) β (π / 2) β β) |
352 | | xrrege0 13149 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’
(((((πβ(1st β(πβπ)))π·(πβπ₯)) β β* β§ (π / 2) β β) β§ (0
β€ ((πβ(1st β(πβπ)))π·(πβπ₯)) β§ ((πβ(1st β(πβπ)))π·(πβπ₯)) β€ (π / 2))) β ((πβ(1st β(πβπ)))π·(πβπ₯)) β β) |
353 | 352 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ ((((πβ(1st
β(πβπ)))π·(πβπ₯)) β β* β§ (π / 2) β β) β ((0
β€ ((πβ(1st β(πβπ)))π·(πβπ₯)) β§ ((πβ(1st β(πβπ)))π·(πβπ₯)) β€ (π / 2)) β ((πβ(1st β(πβπ)))π·(πβπ₯)) β β)) |
354 | 343, 351,
353 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’
((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π β π ) β ((0 β€ ((πβ(1st β(πβπ)))π·(πβπ₯)) β§ ((πβ(1st β(πβπ)))π·(πβπ₯)) β€ (π / 2)) β ((πβ(1st β(πβπ)))π·(πβπ₯)) β β)) |
355 | 349, 354 | mpand 694 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’
((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π β π ) β (((πβ(1st β(πβπ)))π·(πβπ₯)) β€ (π / 2) β ((πβ(1st β(πβπ)))π·(πβπ₯)) β β)) |
356 | 347, 355 | syld 47 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’
((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π β π ) β (((πβ(1st β(πβπ)))π·(πβπ₯)) < (π / 2) β ((πβ(1st β(πβπ)))π·(πβπ₯)) β β)) |
357 | 356 | ad2ant2r 746 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’
(((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β (((πβ(1st β(πβπ)))π·(πβπ₯)) < (π / 2) β ((πβ(1st β(πβπ)))π·(πβπ₯)) β β)) |
358 | 357 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’
((((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β§ ((πβ(1st β(πβπ)))π·(πβπ₯)) < (π / 2)) β ((πβ(1st β(πβπ)))π·(πβπ₯)) β β) |
359 | 338 | ffvelcdmda 7082 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’
(((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ π€ β π) β (πβπ€) β π) |
360 | 359 | adantrl 715 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’
(((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β (πβπ€) β π) |
361 | 360 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’
((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π β π ) β (πβπ€) β π) |
362 | | xmetcl 23819 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ ((π· β (βMetβπ) β§ (πβ(1st β(πβπ))) β π β§ (πβπ€) β π) β ((πβ(1st β(πβπ)))π·(πβπ€)) β
β*) |
363 | 335, 337,
361, 362 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’
((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π β π ) β ((πβ(1st β(πβπ)))π·(πβπ€)) β
β*) |
364 | | xrltle 13124 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ ((((πβ(1st
β(πβπ)))π·(πβπ€)) β β* β§ (π / 2) β
β*) β (((πβ(1st β(πβπ)))π·(πβπ€)) < (π / 2) β ((πβ(1st β(πβπ)))π·(πβπ€)) β€ (π / 2))) |
365 | 363, 345,
364 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’
((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π β π ) β (((πβ(1st β(πβπ)))π·(πβπ€)) < (π / 2) β ((πβ(1st β(πβπ)))π·(πβπ€)) β€ (π / 2))) |
366 | | xmetge0 23832 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ ((π· β (βMetβπ) β§ (πβ(1st β(πβπ))) β π β§ (πβπ€) β π) β 0 β€ ((πβ(1st β(πβπ)))π·(πβπ€))) |
367 | 335, 337,
361, 366 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’
((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π β π ) β 0 β€ ((πβ(1st β(πβπ)))π·(πβπ€))) |
368 | | xrrege0 13149 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’
(((((πβ(1st β(πβπ)))π·(πβπ€)) β β* β§ (π / 2) β β) β§ (0
β€ ((πβ(1st β(πβπ)))π·(πβπ€)) β§ ((πβ(1st β(πβπ)))π·(πβπ€)) β€ (π / 2))) β ((πβ(1st β(πβπ)))π·(πβπ€)) β β) |
369 | 368 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ ((((πβ(1st
β(πβπ)))π·(πβπ€)) β β* β§ (π / 2) β β) β ((0
β€ ((πβ(1st β(πβπ)))π·(πβπ€)) β§ ((πβ(1st β(πβπ)))π·(πβπ€)) β€ (π / 2)) β ((πβ(1st β(πβπ)))π·(πβπ€)) β β)) |
370 | 363, 351,
369 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’
((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π β π ) β ((0 β€ ((πβ(1st β(πβπ)))π·(πβπ€)) β§ ((πβ(1st β(πβπ)))π·(πβπ€)) β€ (π / 2)) β ((πβ(1st β(πβπ)))π·(πβπ€)) β β)) |
371 | 367, 370 | mpand 694 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’
((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π β π ) β (((πβ(1st β(πβπ)))π·(πβπ€)) β€ (π / 2) β ((πβ(1st β(πβπ)))π·(πβπ€)) β β)) |
372 | 365, 371 | syld 47 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’
((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π β π ) β (((πβ(1st β(πβπ)))π·(πβπ€)) < (π / 2) β ((πβ(1st β(πβπ)))π·(πβπ€)) β β)) |
373 | 372 | ad2ant2r 746 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’
(((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β (((πβ(1st β(πβπ)))π·(πβπ€)) < (π / 2) β ((πβ(1st β(πβπ)))π·(πβπ€)) β β)) |
374 | 373 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’
((((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β§ ((πβ(1st β(πβπ)))π·(πβπ€)) < (π / 2)) β ((πβ(1st β(πβπ)))π·(πβπ€)) β β) |
375 | | readdcl 11189 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ ((((πβ(1st
β(πβπ)))π·(πβπ₯)) β β β§ ((πβ(1st β(πβπ)))π·(πβπ€)) β β) β (((πβ(1st
β(πβπ)))π·(πβπ₯)) + ((πβ(1st β(πβπ)))π·(πβπ€))) β β) |
376 | 358, 374,
375 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’
(((((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β§ ((πβ(1st β(πβπ)))π·(πβπ₯)) < (π / 2)) β§ (((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β§ ((πβ(1st β(πβπ)))π·(πβπ€)) < (π / 2))) β (((πβ(1st β(πβπ)))π·(πβπ₯)) + ((πβ(1st β(πβπ)))π·(πβπ€))) β β) |
377 | 376 | anandis 677 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’
((((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β§ (((πβ(1st β(πβπ)))π·(πβπ₯)) < (π / 2) β§ ((πβ(1st β(πβπ)))π·(πβπ€)) < (π / 2))) β (((πβ(1st β(πβπ)))π·(πβπ₯)) + ((πβ(1st β(πβπ)))π·(πβπ€))) β β) |
378 | 377 | rexrd 11260 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’
((((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β§ (((πβ(1st β(πβπ)))π·(πβπ₯)) < (π / 2) β§ ((πβ(1st β(πβπ)))π·(πβπ€)) < (π / 2))) β (((πβ(1st β(πβπ)))π·(πβπ₯)) + ((πβ(1st β(πβπ)))π·(πβπ€))) β
β*) |
379 | | rpxr 12979 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π β β+
β π β
β*) |
380 | 379 | ad6antlr 736 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’
((((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β§ (((πβ(1st β(πβπ)))π·(πβπ₯)) < (π / 2) β§ ((πβ(1st β(πβπ)))π·(πβπ€)) < (π / 2))) β π β β*) |
381 | | xmettri 23839 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((π· β (βMetβπ) β§ ((πβπ₯) β π β§ (πβπ€) β π β§ (πβ(1st β(πβπ))) β π)) β ((πβπ₯)π·(πβπ€)) β€ (((πβπ₯)π·(πβ(1st β(πβπ)))) +π ((πβ(1st
β(πβπ)))π·(πβπ€)))) |
382 | 335, 341,
361, 337, 381 | syl13anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’
((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π β π ) β ((πβπ₯)π·(πβπ€)) β€ (((πβπ₯)π·(πβ(1st β(πβπ)))) +π ((πβ(1st
β(πβπ)))π·(πβπ€)))) |
383 | 382 | ad2ant2r 746 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’
(((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β ((πβπ₯)π·(πβπ€)) β€ (((πβπ₯)π·(πβ(1st β(πβπ)))) +π ((πβ(1st
β(πβπ)))π·(πβπ€)))) |
384 | 383 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’
((((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β§ (((πβ(1st β(πβπ)))π·(πβπ₯)) < (π / 2) β§ ((πβ(1st β(πβπ)))π·(πβπ€)) < (π / 2))) β ((πβπ₯)π·(πβπ€)) β€ (((πβπ₯)π·(πβ(1st β(πβπ)))) +π ((πβ(1st
β(πβπ)))π·(πβπ€)))) |
385 | | xmetsym 23835 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ ((π· β (βMetβπ) β§ (πβπ₯) β π β§ (πβ(1st β(πβπ))) β π) β ((πβπ₯)π·(πβ(1st β(πβπ)))) = ((πβ(1st β(πβπ)))π·(πβπ₯))) |
386 | 335, 341,
337, 385 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’
((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π β π ) β ((πβπ₯)π·(πβ(1st β(πβπ)))) = ((πβ(1st β(πβπ)))π·(πβπ₯))) |
387 | 386 | ad2ant2r 746 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’
(((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β ((πβπ₯)π·(πβ(1st β(πβπ)))) = ((πβ(1st β(πβπ)))π·(πβπ₯))) |
388 | 387 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’
((((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β§ (((πβ(1st β(πβπ)))π·(πβπ₯)) < (π / 2) β§ ((πβ(1st β(πβπ)))π·(πβπ€)) < (π / 2))) β ((πβπ₯)π·(πβ(1st β(πβπ)))) = ((πβ(1st β(πβπ)))π·(πβπ₯))) |
389 | 388 | oveq1d 7419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’
((((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β§ (((πβ(1st β(πβπ)))π·(πβπ₯)) < (π / 2) β§ ((πβ(1st β(πβπ)))π·(πβπ€)) < (π / 2))) β (((πβπ₯)π·(πβ(1st β(πβπ)))) +π ((πβ(1st
β(πβπ)))π·(πβπ€))) = (((πβ(1st β(πβπ)))π·(πβπ₯)) +π ((πβ(1st β(πβπ)))π·(πβπ€)))) |
390 | | rexadd 13207 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((((πβ(1st
β(πβπ)))π·(πβπ₯)) β β β§ ((πβ(1st β(πβπ)))π·(πβπ€)) β β) β (((πβ(1st
β(πβπ)))π·(πβπ₯)) +π ((πβ(1st β(πβπ)))π·(πβπ€))) = (((πβ(1st β(πβπ)))π·(πβπ₯)) + ((πβ(1st β(πβπ)))π·(πβπ€)))) |
391 | 358, 374,
390 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’
(((((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β§ ((πβ(1st β(πβπ)))π·(πβπ₯)) < (π / 2)) β§ (((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β§ ((πβ(1st β(πβπ)))π·(πβπ€)) < (π / 2))) β (((πβ(1st β(πβπ)))π·(πβπ₯)) +π ((πβ(1st β(πβπ)))π·(πβπ€))) = (((πβ(1st β(πβπ)))π·(πβπ₯)) + ((πβ(1st β(πβπ)))π·(πβπ€)))) |
392 | 391 | anandis 677 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’
((((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β§ (((πβ(1st β(πβπ)))π·(πβπ₯)) < (π / 2) β§ ((πβ(1st β(πβπ)))π·(πβπ€)) < (π / 2))) β (((πβ(1st β(πβπ)))π·(πβπ₯)) +π ((πβ(1st β(πβπ)))π·(πβπ€))) = (((πβ(1st β(πβπ)))π·(πβπ₯)) + ((πβ(1st β(πβπ)))π·(πβπ€)))) |
393 | 389, 392 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’
((((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β§ (((πβ(1st β(πβπ)))π·(πβπ₯)) < (π / 2) β§ ((πβ(1st β(πβπ)))π·(πβπ€)) < (π / 2))) β (((πβπ₯)π·(πβ(1st β(πβπ)))) +π ((πβ(1st
β(πβπ)))π·(πβπ€))) = (((πβ(1st β(πβπ)))π·(πβπ₯)) + ((πβ(1st β(πβπ)))π·(πβπ€)))) |
394 | 384, 393 | breqtrd 5173 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’
((((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β§ (((πβ(1st β(πβπ)))π·(πβπ₯)) < (π / 2) β§ ((πβ(1st β(πβπ)))π·(πβπ€)) < (π / 2))) β ((πβπ₯)π·(πβπ€)) β€ (((πβ(1st β(πβπ)))π·(πβπ₯)) + ((πβ(1st β(πβπ)))π·(πβπ€)))) |
395 | | lt2add 11695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’
(((((πβ(1st β(πβπ)))π·(πβπ₯)) β β β§ ((πβ(1st β(πβπ)))π·(πβπ€)) β β) β§ ((π / 2) β β β§ (π / 2) β β)) β
((((πβ(1st
β(πβπ)))π·(πβπ₯)) < (π / 2) β§ ((πβ(1st β(πβπ)))π·(πβπ€)) < (π / 2)) β (((πβ(1st β(πβπ)))π·(πβπ₯)) + ((πβ(1st β(πβπ)))π·(πβπ€))) < ((π / 2) + (π / 2)))) |
396 | 395 | expcom 415 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ (((π / 2) β β β§
(π / 2) β β)
β ((((πβ(1st β(πβπ)))π·(πβπ₯)) β β β§ ((πβ(1st β(πβπ)))π·(πβπ€)) β β) β ((((πβ(1st
β(πβπ)))π·(πβπ₯)) < (π / 2) β§ ((πβ(1st β(πβπ)))π·(πβπ€)) < (π / 2)) β (((πβ(1st β(πβπ)))π·(πβπ₯)) + ((πβ(1st β(πβπ)))π·(πβπ€))) < ((π / 2) + (π / 2))))) |
397 | 351, 351,
396 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’
((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π β π ) β ((((πβ(1st β(πβπ)))π·(πβπ₯)) β β β§ ((πβ(1st β(πβπ)))π·(πβπ€)) β β) β ((((πβ(1st
β(πβπ)))π·(πβπ₯)) < (π / 2) β§ ((πβ(1st β(πβπ)))π·(πβπ€)) < (π / 2)) β (((πβ(1st β(πβπ)))π·(πβπ₯)) + ((πβ(1st β(πβπ)))π·(πβπ€))) < ((π / 2) + (π / 2))))) |
398 | 356, 372,
397 | syl2and 609 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’
((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π β π ) β ((((πβ(1st β(πβπ)))π·(πβπ₯)) < (π / 2) β§ ((πβ(1st β(πβπ)))π·(πβπ€)) < (π / 2)) β ((((πβ(1st β(πβπ)))π·(πβπ₯)) < (π / 2) β§ ((πβ(1st β(πβπ)))π·(πβπ€)) < (π / 2)) β (((πβ(1st β(πβπ)))π·(πβπ₯)) + ((πβ(1st β(πβπ)))π·(πβπ€))) < ((π / 2) + (π / 2))))) |
399 | 398 | pm2.43d 53 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’
((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π β π ) β ((((πβ(1st β(πβπ)))π·(πβπ₯)) < (π / 2) β§ ((πβ(1st β(πβπ)))π·(πβπ€)) < (π / 2)) β (((πβ(1st β(πβπ)))π·(πβπ₯)) + ((πβ(1st β(πβπ)))π·(πβπ€))) < ((π / 2) + (π / 2)))) |
400 | 399 | ad2ant2r 746 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’
(((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β ((((πβ(1st β(πβπ)))π·(πβπ₯)) < (π / 2) β§ ((πβ(1st β(πβπ)))π·(πβπ€)) < (π / 2)) β (((πβ(1st β(πβπ)))π·(πβπ₯)) + ((πβ(1st β(πβπ)))π·(πβπ€))) < ((π / 2) + (π / 2)))) |
401 | 400 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’
((((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β§ (((πβ(1st β(πβπ)))π·(πβπ₯)) < (π / 2) β§ ((πβ(1st β(πβπ)))π·(πβπ€)) < (π / 2))) β (((πβ(1st β(πβπ)))π·(πβπ₯)) + ((πβ(1st β(πβπ)))π·(πβπ€))) < ((π / 2) + (π / 2))) |
402 | | rpcn 12980 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π β β+
β π β
β) |
403 | 402 | 2halvesd 12454 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π β β+
β ((π / 2) + (π / 2)) = π) |
404 | 403 | ad6antlr 736 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’
((((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β§ (((πβ(1st β(πβπ)))π·(πβπ₯)) < (π / 2) β§ ((πβ(1st β(πβπ)))π·(πβπ€)) < (π / 2))) β ((π / 2) + (π / 2)) = π) |
405 | 401, 404 | breqtrd 5173 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’
((((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β§ (((πβ(1st β(πβπ)))π·(πβπ₯)) < (π / 2) β§ ((πβ(1st β(πβπ)))π·(πβπ€)) < (π / 2))) β (((πβ(1st β(πβπ)))π·(πβπ₯)) + ((πβ(1st β(πβπ)))π·(πβπ€))) < π) |
406 | 334, 378,
380, 394, 405 | xrlelttrd 13135 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’
((((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β§ (((πβ(1st β(πβπ)))π·(πβπ₯)) < (π / 2) β§ ((πβ(1st β(πβπ)))π·(πβπ€)) < (π / 2))) β ((πβπ₯)π·(πβπ€)) < π) |
407 | 406 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
(((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β ((((πβ(1st β(πβπ)))π·(πβπ₯)) < (π / 2) β§ ((πβ(1st β(πβπ)))π·(πβπ€)) < (π / 2)) β ((πβπ₯)π·(πβπ€)) < π)) |
408 | 323, 407 | imim12d 81 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
(((((((π β§ π:πβΆπ) β§ π β β+) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β (((((1st β(πβπ))πΆπ₯) < ((2nd β(πβπ)) + (2nd β(πβπ))) β§ ((1st β(πβπ))πΆπ€) < ((2nd β(πβπ)) + (2nd β(πβπ)))) β (((πβ(1st β(πβπ)))π·(πβπ₯)) < (π / 2) β§ ((πβ(1st β(πβπ)))π·(πβπ€)) < (π / 2))) β ((π₯πΆπ€) < inf(ran ran π, β, < ) β ((πβπ₯)π·(πβπ€)) < π))) |
409 | 196, 408 | sylanl1 679 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
(((((((((π β§ π:πβΆπ) β§ π β β+) β§ π β Fin) β§ βͺ (MetOpenβπΆ) = βͺ π ) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ)))) β§ (π β π β§ π₯ β π)) β (((((1st β(πβπ))πΆπ₯) < ((2nd β(πβπ)) + (2nd β(πβπ))) β§ ((1st β(πβπ))πΆπ€) < ((2nd β(πβπ)) + (2nd β(πβπ)))) β (((πβ(1st β(πβπ)))π·(πβπ₯)) < (π / 2) β§ ((πβ(1st β(πβπ)))π·(πβπ€)) < (π / 2))) β ((π₯πΆπ€) < inf(ran ran π, β, < ) β ((πβπ₯)π·(πβπ€)) < π))) |
410 | 409 | adantlrr 720 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((((((((π β§ π:πβΆπ) β§ π β β+) β§ π β Fin) β§ βͺ (MetOpenβπΆ) = βͺ π ) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ (π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ))) β§ βπ β π (((1st β(πβπ))πΆπ) < ((2nd β(πβπ)) + (2nd β(πβπ))) β ((πβ(1st β(πβπ)))π·(πβπ)) < (π / 2)))) β§ (π β π β§ π₯ β π)) β (((((1st β(πβπ))πΆπ₯) < ((2nd β(πβπ)) + (2nd β(πβπ))) β§ ((1st β(πβπ))πΆπ€) < ((2nd β(πβπ)) + (2nd β(πβπ)))) β (((πβ(1st β(πβπ)))π·(πβπ₯)) < (π / 2) β§ ((πβ(1st β(πβπ)))π·(πβπ€)) < (π / 2))) β ((π₯πΆπ€) < inf(ran ran π, β, < ) β ((πβπ₯)π·(πβπ€)) < π))) |
411 | 193, 410 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((((((π β§ π:πβΆπ) β§ π β β+) β§ π β Fin) β§ βͺ (MetOpenβπΆ) = βͺ π ) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ (π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ))) β§ βπ β π (((1st β(πβπ))πΆπ) < ((2nd β(πβπ)) + (2nd β(πβπ))) β ((πβ(1st β(πβπ)))π·(πβπ)) < (π / 2)))) β§ (π β π β§ π₯ β π)) β ((π₯πΆπ€) < inf(ran ran π, β, < ) β ((πβπ₯)π·(πβπ€)) < π)) |
412 | 411 | exp32 422 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((((((((π β§ π:πβΆπ) β§ π β β+) β§ π β Fin) β§ βͺ (MetOpenβπΆ) = βͺ π ) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ (π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ))) β§ βπ β π (((1st β(πβπ))πΆπ) < ((2nd β(πβπ)) + (2nd β(πβπ))) β ((πβ(1st β(πβπ)))π·(πβπ)) < (π / 2)))) β (π β π β (π₯ β π β ((π₯πΆπ€) < inf(ran ran π, β, < ) β ((πβπ₯)π·(πβπ€)) < π)))) |
413 | 174, 412 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((((((((π β§ π:πβΆπ) β§ π β β+) β§ π β Fin) β§ βͺ (MetOpenβπΆ) = βͺ π ) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ (βπ β π (π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ))) β§ βπ β π (((1st β(πβπ))πΆπ) < ((2nd β(πβπ)) + (2nd β(πβπ))) β ((πβ(1st β(πβπ)))π·(πβπ)) < (π / 2))) β§ π β π )) β (π β π β (π₯ β π β ((π₯πΆπ€) < inf(ran ran π, β, < ) β ((πβπ₯)π·(πβπ€)) < π)))) |
414 | 413 | expr 458 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((((((((π β§ π:πβΆπ) β§ π β β+) β§ π β Fin) β§ βͺ (MetOpenβπΆ) = βͺ π ) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ βπ β π (π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ))) β§ βπ β π (((1st β(πβπ))πΆπ) < ((2nd β(πβπ)) + (2nd β(πβπ))) β ((πβ(1st β(πβπ)))π·(πβπ)) < (π / 2)))) β (π β π β (π β π β (π₯ β π β ((π₯πΆπ€) < inf(ran ran π, β, < ) β ((πβπ₯)π·(πβπ€)) < π))))) |
415 | 414 | pm2.43d 53 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((((((π β§ π:πβΆπ) β§ π β β+) β§ π β Fin) β§ βͺ (MetOpenβπΆ) = βͺ π ) β§ π:π βΆ(π Γ β+)) β§ (π₯ β π β§ π€ β π)) β§ βπ β π (π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ))) β§ βπ β π (((1st β(πβπ))πΆπ) < ((2nd β(πβπ)) + (2nd β(πβπ))) β ((πβ(1st β(πβπ)))π·(πβπ)) < (π / 2)))) β (π β π β (π₯ β π β ((π₯πΆπ€) < inf(ran ran π, β, < ) β ((πβπ₯)π·(πβπ€)) < π)))) |
416 | 415 | an32s 651 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((((π β§ π:πβΆπ) β§ π β β+) β§ π β Fin) β§ βͺ (MetOpenβπΆ) = βͺ π ) β§ π:π βΆ(π Γ β+)) β§
βπ β π (π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ))) β§ βπ β π (((1st β(πβπ))πΆπ) < ((2nd β(πβπ)) + (2nd β(πβπ))) β ((πβ(1st β(πβπ)))π·(πβπ)) < (π / 2)))) β§ (π₯ β π β§ π€ β π)) β (π β π β (π₯ β π β ((π₯πΆπ€) < inf(ran ran π, β, < ) β ((πβπ₯)π·(πβπ€)) < π)))) |
417 | 172, 173,
416 | rexlimd 3264 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((((π β§ π:πβΆπ) β§ π β β+) β§ π β Fin) β§ βͺ (MetOpenβπΆ) = βͺ π ) β§ π:π βΆ(π Γ β+)) β§
βπ β π (π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ))) β§ βπ β π (((1st β(πβπ))πΆπ) < ((2nd β(πβπ)) + (2nd β(πβπ))) β ((πβ(1st β(πβπ)))π·(πβπ)) < (π / 2)))) β§ (π₯ β π β§ π€ β π)) β (βπ β π π₯ β π β ((π₯πΆπ€) < inf(ran ran π, β, < ) β ((πβπ₯)π·(πβπ€)) < π))) |
418 | 167, 417 | mpd 15 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((((π β§ π:πβΆπ) β§ π β β+) β§ π β Fin) β§ βͺ (MetOpenβπΆ) = βͺ π ) β§ π:π βΆ(π Γ β+)) β§
βπ β π (π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ))) β§ βπ β π (((1st β(πβπ))πΆπ) < ((2nd β(πβπ)) + (2nd β(πβπ))) β ((πβ(1st β(πβπ)))π·(πβπ)) < (π / 2)))) β§ (π₯ β π β§ π€ β π)) β ((π₯πΆπ€) < inf(ran ran π, β, < ) β ((πβπ₯)π·(πβπ€)) < π)) |
419 | 418 | ralrimivva 3201 |
. . . . . . . . . . . . . . . . . 18
β’
(((((((π β§ π:πβΆπ) β§ π β β+) β§ π β Fin) β§ βͺ (MetOpenβπΆ) = βͺ π ) β§ π:π βΆ(π Γ β+)) β§
βπ β π (π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ))) β§ βπ β π (((1st β(πβπ))πΆπ) < ((2nd β(πβπ)) + (2nd β(πβπ))) β ((πβ(1st β(πβπ)))π·(πβπ)) < (π / 2)))) β βπ₯ β π βπ€ β π ((π₯πΆπ€) < inf(ran ran π, β, < ) β ((πβπ₯)π·(πβπ€)) < π)) |
420 | | breq2 5151 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π§ = inf(ran ran π, β, < ) β ((π₯πΆπ€) < π§ β (π₯πΆπ€) < inf(ran ran π, β, < ))) |
421 | 420 | imbi1d 342 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π§ = inf(ran ran π, β, < ) β
(((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π) β ((π₯πΆπ€) < inf(ran ran π, β, < ) β ((πβπ₯)π·(πβπ€)) < π))) |
422 | 421 | 2ralbidv 3219 |
. . . . . . . . . . . . . . . . . . 19
β’ (π§ = inf(ran ran π, β, < ) β
(βπ₯ β π βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π) β βπ₯ β π βπ€ β π ((π₯πΆπ€) < inf(ran ran π, β, < ) β ((πβπ₯)π·(πβπ€)) < π))) |
423 | 422 | rspcev 3612 |
. . . . . . . . . . . . . . . . . 18
β’ ((inf(ran
ran π, β, < )
β β+ β§ βπ₯ β π βπ€ β π ((π₯πΆπ€) < inf(ran ran π, β, < ) β ((πβπ₯)π·(πβπ€)) < π)) β βπ§ β β+ βπ₯ β π βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π)) |
424 | 158, 419,
423 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’
(((((((π β§ π:πβΆπ) β§ π β β+) β§ π β Fin) β§ βͺ (MetOpenβπΆ) = βͺ π ) β§ π:π βΆ(π Γ β+)) β§
βπ β π (π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ))) β§ βπ β π (((1st β(πβπ))πΆπ) < ((2nd β(πβπ)) + (2nd β(πβπ))) β ((πβ(1st β(πβπ)))π·(πβπ)) < (π / 2)))) β βπ§ β β+ βπ₯ β π βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π)) |
425 | 424 | expl 459 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π:πβΆπ) β§ π β β+) β§ π β Fin) β§ βͺ (MetOpenβπΆ) = βͺ π ) β ((π:π βΆ(π Γ β+) β§
βπ β π (π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ))) β§ βπ β π (((1st β(πβπ))πΆπ) < ((2nd β(πβπ)) + (2nd β(πβπ))) β ((πβ(1st β(πβπ)))π·(πβπ)) < (π / 2)))) β βπ§ β β+ βπ₯ β π βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π))) |
426 | 425 | exlimdv 1937 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π:πβΆπ) β§ π β β+) β§ π β Fin) β§ βͺ (MetOpenβπΆ) = βͺ π ) β (βπ(π:π βΆ(π Γ β+) β§
βπ β π (π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ))) β§ βπ β π (((1st β(πβπ))πΆπ) < ((2nd β(πβπ)) + (2nd β(πβπ))) β ((πβ(1st β(πβπ)))π·(πβπ)) < (π / 2)))) β βπ§ β β+ βπ₯ β π βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π))) |
427 | 426 | expimpd 455 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π:πβΆπ) β§ π β β+) β§ π β Fin) β ((βͺ (MetOpenβπΆ) = βͺ π β§ βπ(π:π βΆ(π Γ β+) β§
βπ β π (π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ))) β§ βπ β π (((1st β(πβπ))πΆπ) < ((2nd β(πβπ)) + (2nd β(πβπ))) β ((πβ(1st β(πβπ)))π·(πβπ)) < (π / 2))))) β βπ§ β β+ βπ₯ β π βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π))) |
428 | 102, 427 | sylan2 594 |
. . . . . . . . . . . . 13
β’ ((((π β§ π:πβΆπ) β§ π β β+) β§ π β (π«
(MetOpenβπΆ) β©
Fin)) β ((βͺ (MetOpenβπΆ) = βͺ π β§ βπ(π:π βΆ(π Γ β+) β§
βπ β π (π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ))) β§ βπ β π (((1st β(πβπ))πΆπ) < ((2nd β(πβπ)) + (2nd β(πβπ))) β ((πβ(1st β(πβπ)))π·(πβπ)) < (π / 2))))) β βπ§ β β+ βπ₯ β π βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π))) |
429 | 428 | rexlimdva 3156 |
. . . . . . . . . . . 12
β’ (((π β§ π:πβΆπ) β§ π β β+) β
(βπ β (π«
(MetOpenβπΆ) β©
Fin)(βͺ (MetOpenβπΆ) = βͺ π β§ βπ(π:π βΆ(π Γ β+) β§
βπ β π (π = ((1st β(πβπ))(ballβπΆ)(2nd β(πβπ))) β§ βπ β π (((1st β(πβπ))πΆπ) < ((2nd β(πβπ)) + (2nd β(πβπ))) β ((πβ(1st β(πβπ)))π·(πβπ)) < (π / 2))))) β βπ§ β β+ βπ₯ β π βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π))) |
430 | 101, 429 | syld 47 |
. . . . . . . . . . 11
β’ (((π β§ π:πβΆπ) β§ π β β+) β
(βπ₯ β π βπ§ β β+ βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < (π / 2)) β βπ§ β β+ βπ₯ β π βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π))) |
431 | 15, 430 | syl5 34 |
. . . . . . . . . 10
β’ (((π β§ π:πβΆπ) β§ π β β+) β (((π / 2) β β+
β§ βπ¦ β
β+ βπ₯ β π βπ§ β β+ βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π¦)) β βπ§ β β+ βπ₯ β π βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π))) |
432 | 431 | exp4b 432 |
. . . . . . . . 9
β’ ((π β§ π:πβΆπ) β (π β β+ β ((π / 2) β β+
β (βπ¦ β
β+ βπ₯ β π βπ§ β β+ βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π¦) β βπ§ β β+ βπ₯ β π βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π))))) |
433 | 9, 432 | mpdi 45 |
. . . . . . . 8
β’ ((π β§ π:πβΆπ) β (π β β+ β
(βπ¦ β
β+ βπ₯ β π βπ§ β β+ βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π¦) β βπ§ β β+ βπ₯ β π βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π)))) |
434 | 433 | ralrimiv 3146 |
. . . . . . 7
β’ ((π β§ π:πβΆπ) β βπ β β+ (βπ¦ β β+
βπ₯ β π βπ§ β β+ βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π¦) β βπ§ β β+ βπ₯ β π βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π))) |
435 | | r19.21v 3180 |
. . . . . . 7
β’
(βπ β
β+ (βπ¦ β β+ βπ₯ β π βπ§ β β+ βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π¦) β βπ§ β β+ βπ₯ β π βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π)) β (βπ¦ β β+ βπ₯ β π βπ§ β β+ βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π¦) β βπ β β+ βπ§ β β+
βπ₯ β π βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π))) |
436 | 434, 435 | sylib 217 |
. . . . . 6
β’ ((π β§ π:πβΆπ) β (βπ¦ β β+ βπ₯ β π βπ§ β β+ βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π¦) β βπ β β+ βπ§ β β+
βπ₯ β π βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π))) |
437 | 8, 436 | impbid2 225 |
. . . . 5
β’ ((π β§ π:πβΆπ) β (βπ β β+ βπ§ β β+
βπ₯ β π βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π) β βπ¦ β β+ βπ₯ β π βπ§ β β+ βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π¦))) |
438 | | ralcom 3287 |
. . . . 5
β’
(βπ¦ β
β+ βπ₯ β π βπ§ β β+ βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π¦) β βπ₯ β π βπ¦ β β+ βπ§ β β+
βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π¦)) |
439 | 437, 438 | bitrdi 287 |
. . . 4
β’ ((π β§ π:πβΆπ) β (βπ β β+ βπ§ β β+
βπ₯ β π βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π) β βπ₯ β π βπ¦ β β+ βπ§ β β+
βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π¦))) |
440 | 439 | pm5.32da 580 |
. . 3
β’ (π β ((π:πβΆπ β§ βπ β β+ βπ§ β β+
βπ₯ β π βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π)) β (π:πβΆπ β§ βπ₯ β π βπ¦ β β+ βπ§ β β+
βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π¦)))) |
441 | | eqid 2733 |
. . . 4
β’
(metUnifβπΆ) =
(metUnifβπΆ) |
442 | | eqid 2733 |
. . . 4
β’
(metUnifβπ·) =
(metUnifβπ·) |
443 | | heicant.y |
. . . 4
β’ (π β π β β
) |
444 | | xmetpsmet 23836 |
. . . . 5
β’ (πΆ β (βMetβπ) β πΆ β (PsMetβπ)) |
445 | 18, 444 | syl 17 |
. . . 4
β’ (π β πΆ β (PsMetβπ)) |
446 | | xmetpsmet 23836 |
. . . . 5
β’ (π· β (βMetβπ) β π· β (PsMetβπ)) |
447 | 325, 446 | syl 17 |
. . . 4
β’ (π β π· β (PsMetβπ)) |
448 | 441, 442,
128, 443, 445, 447 | metucn 24062 |
. . 3
β’ (π β (π β ((metUnifβπΆ) Cnu(metUnifβπ·)) β (π:πβΆπ β§ βπ β β+ βπ§ β β+
βπ₯ β π βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π)))) |
449 | | eqid 2733 |
. . . . 5
β’
(MetOpenβπ·) =
(MetOpenβπ·) |
450 | 23, 449 | metcn 24034 |
. . . 4
β’ ((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β (π β ((MetOpenβπΆ) Cn (MetOpenβπ·)) β (π:πβΆπ β§ βπ₯ β π βπ¦ β β+ βπ§ β β+
βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π¦)))) |
451 | 18, 325, 450 | syl2anc 585 |
. . 3
β’ (π β (π β ((MetOpenβπΆ) Cn (MetOpenβπ·)) β (π:πβΆπ β§ βπ₯ β π βπ¦ β β+ βπ§ β β+
βπ€ β π ((π₯πΆπ€) < π§ β ((πβπ₯)π·(πβπ€)) < π¦)))) |
452 | 440, 448,
451 | 3bitr4d 311 |
. 2
β’ (π β (π β ((metUnifβπΆ) Cnu(metUnifβπ·)) β π β ((MetOpenβπΆ) Cn (MetOpenβπ·)))) |
453 | 452 | eqrdv 2731 |
1
β’ (π β ((metUnifβπΆ)
Cnu(metUnifβπ·)) = ((MetOpenβπΆ) Cn (MetOpenβπ·))) |