Step | Hyp | Ref
| Expression |
1 | | iscau3.3 |
. . . . . 6
β’ (π β π· β (βMetβπ)) |
2 | | elfvdm 6883 |
. . . . . 6
β’ (π· β (βMetβπ) β π β dom βMet) |
3 | 1, 2 | syl 17 |
. . . . 5
β’ (π β π β dom βMet) |
4 | | cnex 11140 |
. . . . 5
β’ β
β V |
5 | 3, 4 | jctir 522 |
. . . 4
β’ (π β (π β dom βMet β§ β β
V)) |
6 | | iscauf.7 |
. . . . 5
β’ (π β πΉ:πβΆπ) |
7 | | iscau3.2 |
. . . . . 6
β’ π =
(β€β₯βπ) |
8 | | uzssz 12792 |
. . . . . . 7
β’
(β€β₯βπ) β β€ |
9 | | zsscn 12515 |
. . . . . . 7
β’ β€
β β |
10 | 8, 9 | sstri 3957 |
. . . . . 6
β’
(β€β₯βπ) β β |
11 | 7, 10 | eqsstri 3982 |
. . . . 5
β’ π β
β |
12 | 6, 11 | jctir 522 |
. . . 4
β’ (π β (πΉ:πβΆπ β§ π β β)) |
13 | | elpm2r 8789 |
. . . 4
β’ (((π β dom βMet β§
β β V) β§ (πΉ:πβΆπ β§ π β β)) β πΉ β (π βpm
β)) |
14 | 5, 12, 13 | syl2anc 585 |
. . 3
β’ (π β πΉ β (π βpm
β)) |
15 | 14 | biantrurd 534 |
. 2
β’ (π β (βπ₯ β β+
βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ π΄ β π β§ (π΄π·π΅) < π₯) β (πΉ β (π βpm β) β§
βπ₯ β
β+ βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ π΄ β π β§ (π΄π·π΅) < π₯)))) |
16 | 1 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ (π β π β§ π β (β€β₯βπ))) β π· β (βMetβπ)) |
17 | | iscau4.6 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β (πΉβπ) = π΅) |
18 | 17 | adantrr 716 |
. . . . . . . . . 10
β’ ((π β§ (π β π β§ π β (β€β₯βπ))) β (πΉβπ) = π΅) |
19 | 6 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ (π β π β§ π β (β€β₯βπ))) β πΉ:πβΆπ) |
20 | | simprl 770 |
. . . . . . . . . . 11
β’ ((π β§ (π β π β§ π β (β€β₯βπ))) β π β π) |
21 | 19, 20 | ffvelcdmd 7040 |
. . . . . . . . . 10
β’ ((π β§ (π β π β§ π β (β€β₯βπ))) β (πΉβπ) β π) |
22 | 18, 21 | eqeltrrd 2835 |
. . . . . . . . 9
β’ ((π β§ (π β π β§ π β (β€β₯βπ))) β π΅ β π) |
23 | 7 | uztrn2 12790 |
. . . . . . . . . . 11
β’ ((π β π β§ π β (β€β₯βπ)) β π β π) |
24 | | iscau4.5 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β (πΉβπ) = π΄) |
25 | 23, 24 | sylan2 594 |
. . . . . . . . . 10
β’ ((π β§ (π β π β§ π β (β€β₯βπ))) β (πΉβπ) = π΄) |
26 | | ffvelcdm 7036 |
. . . . . . . . . . 11
β’ ((πΉ:πβΆπ β§ π β π) β (πΉβπ) β π) |
27 | 6, 23, 26 | syl2an 597 |
. . . . . . . . . 10
β’ ((π β§ (π β π β§ π β (β€β₯βπ))) β (πΉβπ) β π) |
28 | 25, 27 | eqeltrrd 2835 |
. . . . . . . . 9
β’ ((π β§ (π β π β§ π β (β€β₯βπ))) β π΄ β π) |
29 | | xmetsym 23723 |
. . . . . . . . 9
β’ ((π· β (βMetβπ) β§ π΅ β π β§ π΄ β π) β (π΅π·π΄) = (π΄π·π΅)) |
30 | 16, 22, 28, 29 | syl3anc 1372 |
. . . . . . . 8
β’ ((π β§ (π β π β§ π β (β€β₯βπ))) β (π΅π·π΄) = (π΄π·π΅)) |
31 | 30 | breq1d 5119 |
. . . . . . 7
β’ ((π β§ (π β π β§ π β (β€β₯βπ))) β ((π΅π·π΄) < π₯ β (π΄π·π΅) < π₯)) |
32 | | fdm 6681 |
. . . . . . . . . . . . 13
β’ (πΉ:πβΆπ β dom πΉ = π) |
33 | 32 | eleq2d 2820 |
. . . . . . . . . . . 12
β’ (πΉ:πβΆπ β (π β dom πΉ β π β π)) |
34 | 33 | biimpar 479 |
. . . . . . . . . . 11
β’ ((πΉ:πβΆπ β§ π β π) β π β dom πΉ) |
35 | 6, 23, 34 | syl2an 597 |
. . . . . . . . . 10
β’ ((π β§ (π β π β§ π β (β€β₯βπ))) β π β dom πΉ) |
36 | 35, 28 | jca 513 |
. . . . . . . . 9
β’ ((π β§ (π β π β§ π β (β€β₯βπ))) β (π β dom πΉ β§ π΄ β π)) |
37 | 36 | biantrurd 534 |
. . . . . . . 8
β’ ((π β§ (π β π β§ π β (β€β₯βπ))) β ((π΄π·π΅) < π₯ β ((π β dom πΉ β§ π΄ β π) β§ (π΄π·π΅) < π₯))) |
38 | | df-3an 1090 |
. . . . . . . 8
β’ ((π β dom πΉ β§ π΄ β π β§ (π΄π·π΅) < π₯) β ((π β dom πΉ β§ π΄ β π) β§ (π΄π·π΅) < π₯)) |
39 | 37, 38 | bitr4di 289 |
. . . . . . 7
β’ ((π β§ (π β π β§ π β (β€β₯βπ))) β ((π΄π·π΅) < π₯ β (π β dom πΉ β§ π΄ β π β§ (π΄π·π΅) < π₯))) |
40 | 31, 39 | bitrd 279 |
. . . . . 6
β’ ((π β§ (π β π β§ π β (β€β₯βπ))) β ((π΅π·π΄) < π₯ β (π β dom πΉ β§ π΄ β π β§ (π΄π·π΅) < π₯))) |
41 | 40 | anassrs 469 |
. . . . 5
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β ((π΅π·π΄) < π₯ β (π β dom πΉ β§ π΄ β π β§ (π΄π·π΅) < π₯))) |
42 | 41 | ralbidva 3169 |
. . . 4
β’ ((π β§ π β π) β (βπ β (β€β₯βπ)(π΅π·π΄) < π₯ β βπ β (β€β₯βπ)(π β dom πΉ β§ π΄ β π β§ (π΄π·π΅) < π₯))) |
43 | 42 | rexbidva 3170 |
. . 3
β’ (π β (βπ β π βπ β (β€β₯βπ)(π΅π·π΄) < π₯ β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ π΄ β π β§ (π΄π·π΅) < π₯))) |
44 | 43 | ralbidv 3171 |
. 2
β’ (π β (βπ₯ β β+
βπ β π βπ β (β€β₯βπ)(π΅π·π΄) < π₯ β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ π΄ β π β§ (π΄π·π΅) < π₯))) |
45 | | iscau3.4 |
. . 3
β’ (π β π β β€) |
46 | 7, 1, 45, 24, 17 | iscau4 24666 |
. 2
β’ (π β (πΉ β (Cauβπ·) β (πΉ β (π βpm β) β§
βπ₯ β
β+ βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ π΄ β π β§ (π΄π·π΅) < π₯)))) |
47 | 15, 44, 46 | 3bitr4rd 312 |
1
β’ (π β (πΉ β (Cauβπ·) β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(π΅π·π΄) < π₯)) |