Step | Hyp | Ref
| Expression |
1 | | reex 11149 |
. . . . . . 7
β’ β
β V |
2 | | mapdm0 8787 |
. . . . . . 7
β’ (β
β V β (β βm β
) =
{β
}) |
3 | 1, 2 | ax-mp 5 |
. . . . . 6
β’ (β
βm β
) = {β
} |
4 | 3 | a1i 11 |
. . . . 5
β’ (π = β
β (β
βm β
) = {β
}) |
5 | | oveq2 7370 |
. . . . 5
β’ (π = β
β (β
βm π) =
(β βm β
)) |
6 | | ixpeq1 8853 |
. . . . . . 7
β’ (π = β
β Xπ β
π (([,) β (πΌβπ))βπ) = Xπ β β
(([,) β
(πΌβπ))βπ)) |
7 | 6 | iuneq2d 4988 |
. . . . . 6
β’ (π = β
β βͺ π β β Xπ β π (([,) β (πΌβπ))βπ) = βͺ π β β Xπ β
β
(([,) β (πΌβπ))βπ)) |
8 | | ixp0x 8871 |
. . . . . . . . . 10
β’ Xπ β
β
(([,) β (πΌβπ))βπ) = {β
} |
9 | 8 | a1i 11 |
. . . . . . . . 9
β’ (π β β β Xπ β
β
(([,) β (πΌβπ))βπ) = {β
}) |
10 | 9 | iuneq2i 4980 |
. . . . . . . 8
β’ βͺ π β β Xπ β β
(([,) β
(πΌβπ))βπ) = βͺ π β β
{β
} |
11 | | 1nn 12171 |
. . . . . . . . . 10
β’ 1 β
β |
12 | 11 | ne0ii 4302 |
. . . . . . . . 9
β’ β
β β
|
13 | | iunconst 4968 |
. . . . . . . . 9
β’ (β
β β
β βͺ π β β {β
} =
{β
}) |
14 | 12, 13 | ax-mp 5 |
. . . . . . . 8
β’ βͺ π β β {β
} =
{β
} |
15 | 10, 14 | eqtri 2765 |
. . . . . . 7
β’ βͺ π β β Xπ β β
(([,) β
(πΌβπ))βπ) = {β
} |
16 | 15 | a1i 11 |
. . . . . 6
β’ (π = β
β βͺ π β β Xπ β β
(([,) β
(πΌβπ))βπ) = {β
}) |
17 | 7, 16 | eqtrd 2777 |
. . . . 5
β’ (π = β
β βͺ π β β Xπ β π (([,) β (πΌβπ))βπ) = {β
}) |
18 | 4, 5, 17 | 3eqtr4d 2787 |
. . . 4
β’ (π = β
β (β
βm π) =
βͺ π β β Xπ β π (([,) β (πΌβπ))βπ)) |
19 | | eqimss 4005 |
. . . 4
β’ ((β
βm π) =
βͺ π β β Xπ β π (([,) β (πΌβπ))βπ) β (β βm π) β βͺ π β β Xπ β π (([,) β (πΌβπ))βπ)) |
20 | 18, 19 | syl 17 |
. . 3
β’ (π = β
β (β
βm π)
β βͺ π β β Xπ β π (([,) β (πΌβπ))βπ)) |
21 | 20 | adantl 483 |
. 2
β’ ((π β§ π = β
) β (β
βm π)
β βͺ π β β Xπ β π (([,) β (πΌβπ))βπ)) |
22 | | simpll 766 |
. . . . . 6
β’ (((π β§ Β¬ π = β
) β§ π β (β βm π)) β π) |
23 | | simpr 486 |
. . . . . 6
β’ (((π β§ Β¬ π = β
) β§ π β (β βm π)) β π β (β βm π)) |
24 | | simplr 768 |
. . . . . 6
β’ (((π β§ Β¬ π = β
) β§ π β (β βm π)) β Β¬ π = β
) |
25 | | rncoss 5932 |
. . . . . . . . . . 11
β’ ran (abs
β π) β ran
abs |
26 | | absf 15229 |
. . . . . . . . . . . 12
β’
abs:ββΆβ |
27 | | frn 6680 |
. . . . . . . . . . . 12
β’
(abs:ββΆβ β ran abs β
β) |
28 | 26, 27 | ax-mp 5 |
. . . . . . . . . . 11
β’ ran abs
β β |
29 | 25, 28 | sstri 3958 |
. . . . . . . . . 10
β’ ran (abs
β π) β
β |
30 | 29 | a1i 11 |
. . . . . . . . 9
β’ (((π β§ π β (β βm π)) β§ Β¬ π = β
) β ran (abs β π) β
β) |
31 | | ltso 11242 |
. . . . . . . . . . 11
β’ < Or
β |
32 | 31 | a1i 11 |
. . . . . . . . . 10
β’ (((π β§ π β (β βm π)) β§ Β¬ π = β
) β < Or
β) |
33 | 26 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (β βm π)) β
abs:ββΆβ) |
34 | | elmapi 8794 |
. . . . . . . . . . . . . . 15
β’ (π β (β
βm π)
β π:πβΆβ) |
35 | 34 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (β βm π)) β π:πβΆβ) |
36 | | ax-resscn 11115 |
. . . . . . . . . . . . . . 15
β’ β
β β |
37 | 36 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (β βm π)) β β β
β) |
38 | 35, 37 | fssd 6691 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (β βm π)) β π:πβΆβ) |
39 | | fco 6697 |
. . . . . . . . . . . . 13
β’
((abs:ββΆβ β§ π:πβΆβ) β (abs β π):πβΆβ) |
40 | 33, 38, 39 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π β§ π β (β βm π)) β (abs β π):πβΆβ) |
41 | | hoicvr.3 |
. . . . . . . . . . . . 13
β’ (π β π β Fin) |
42 | 41 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β (β βm π)) β π β Fin) |
43 | | rnffi 43466 |
. . . . . . . . . . . 12
β’ (((abs
β π):πβΆβ β§ π β Fin) β ran (abs
β π) β
Fin) |
44 | 40, 42, 43 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((π β§ π β (β βm π)) β ran (abs β π) β Fin) |
45 | 44 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π β (β βm π)) β§ Β¬ π = β
) β ran (abs β π) β Fin) |
46 | 34 | frnd 6681 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (β
βm π)
β ran π β
β) |
47 | 26 | fdmi 6685 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ dom abs =
β |
48 | 47 | eqcomi 2746 |
. . . . . . . . . . . . . . . . . . . . 21
β’ β =
dom abs |
49 | 36, 48 | sseqtri 3985 |
. . . . . . . . . . . . . . . . . . . 20
β’ β
β dom abs |
50 | 49 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (β
βm π)
β β β dom abs) |
51 | 46, 50 | sstrd 3959 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (β
βm π)
β ran π β dom
abs) |
52 | | dmcosseq 5933 |
. . . . . . . . . . . . . . . . . 18
β’ (ran
π β dom abs β
dom (abs β π) = dom
π) |
53 | 51, 52 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β (β
βm π)
β dom (abs β π)
= dom π) |
54 | 34 | fdmd 6684 |
. . . . . . . . . . . . . . . . 17
β’ (π β (β
βm π)
β dom π = π) |
55 | 53, 54 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
β’ (π β (β
βm π)
β dom (abs β π)
= π) |
56 | 55 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β (β
βm π) β§
Β¬ π = β
) β
dom (abs β π) = π) |
57 | | neqne 2952 |
. . . . . . . . . . . . . . . 16
β’ (Β¬
π = β
β π β β
) |
58 | 57 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π β (β
βm π) β§
Β¬ π = β
) β
π β
β
) |
59 | 56, 58 | eqnetrd 3012 |
. . . . . . . . . . . . . 14
β’ ((π β (β
βm π) β§
Β¬ π = β
) β
dom (abs β π) β
β
) |
60 | 59 | neneqd 2949 |
. . . . . . . . . . . . 13
β’ ((π β (β
βm π) β§
Β¬ π = β
) β
Β¬ dom (abs β π) =
β
) |
61 | | dm0rn0 5885 |
. . . . . . . . . . . . 13
β’ (dom (abs
β π) = β
β
ran (abs β π) =
β
) |
62 | 60, 61 | sylnib 328 |
. . . . . . . . . . . 12
β’ ((π β (β
βm π) β§
Β¬ π = β
) β
Β¬ ran (abs β π) =
β
) |
63 | 62 | neqned 2951 |
. . . . . . . . . . 11
β’ ((π β (β
βm π) β§
Β¬ π = β
) β
ran (abs β π) β
β
) |
64 | 63 | adantll 713 |
. . . . . . . . . 10
β’ (((π β§ π β (β βm π)) β§ Β¬ π = β
) β ran (abs β π) β β
) |
65 | | fisupcl 9412 |
. . . . . . . . . 10
β’ (( <
Or β β§ (ran (abs β π) β Fin β§ ran (abs β π) β β
β§ ran (abs
β π) β
β)) β sup(ran (abs β π), β, < ) β ran (abs β
π)) |
66 | 32, 45, 64, 30, 65 | syl13anc 1373 |
. . . . . . . . 9
β’ (((π β§ π β (β βm π)) β§ Β¬ π = β
) β sup(ran (abs β
π), β, < ) β
ran (abs β π)) |
67 | 30, 66 | sseldd 3950 |
. . . . . . . 8
β’ (((π β§ π β (β βm π)) β§ Β¬ π = β
) β sup(ran (abs β
π), β, < ) β
β) |
68 | | arch 12417 |
. . . . . . . 8
β’ (sup(ran
(abs β π), β,
< ) β β β βπ β β sup(ran (abs β π), β, < ) < π) |
69 | 67, 68 | syl 17 |
. . . . . . 7
β’ (((π β§ π β (β βm π)) β§ Β¬ π = β
) β βπ β β sup(ran (abs β π), β, < ) < π) |
70 | 35 | ffnd 6674 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (β βm π)) β π Fn π) |
71 | 70 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (β βm π)) β§ Β¬ π = β
) β§ sup(ran (abs β π), β, < ) < π) β π Fn π) |
72 | 71 | adantlr 714 |
. . . . . . . . . . 11
β’
(((((π β§ π β (β
βm π))
β§ Β¬ π = β
)
β§ π β β)
β§ sup(ran (abs β π), β, < ) < π) β π Fn π) |
73 | | simplll 774 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π β (β
βm π))
β§ π β β)
β§ sup(ran (abs β π), β, < ) < π) β§ π β π) β (π β§ π β (β βm π))) |
74 | | id 22 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β π β
β) |
75 | 74 | ad3antlr 730 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π β (β
βm π))
β§ π β β)
β§ sup(ran (abs β π), β, < ) < π) β§ π β π) β π β β) |
76 | | simplr 768 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π β (β
βm π))
β§ π β β)
β§ sup(ran (abs β π), β, < ) < π) β§ π β π) β sup(ran (abs β π), β, < ) < π) |
77 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π β (β
βm π))
β§ π β β)
β§ sup(ran (abs β π), β, < ) < π) β§ π β π) β π β π) |
78 | | simp2 1138 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β (β βm π)) β§ π β β β§ sup(ran (abs β
π), β, < ) <
π) β π β
β) |
79 | | zssre 12513 |
. . . . . . . . . . . . . . . . . . . . 21
β’ β€
β β |
80 | | ressxr 11206 |
. . . . . . . . . . . . . . . . . . . . 21
β’ β
β β* |
81 | 79, 80 | sstri 3958 |
. . . . . . . . . . . . . . . . . . . 20
β’ β€
β β* |
82 | | nnnegz 12509 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β β -π β
β€) |
83 | 81, 82 | sselid 3947 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β β -π β
β*) |
84 | 83 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β β§ π β π) β -π β β*) |
85 | 78, 84 | sylan 581 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β (β βm π)) β§ π β β β§ sup(ran (abs β
π), β, < ) <
π) β§ π β π) β -π β β*) |
86 | 74 | nnxrd 43581 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β β π β
β*) |
87 | 86 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β β§ π β π) β π β β*) |
88 | 78, 87 | sylan 581 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β (β βm π)) β§ π β β β§ sup(ran (abs β
π), β, < ) <
π) β§ π β π) β π β β*) |
89 | 34 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β (β
βm π) β§
π β β β§
sup(ran (abs β π),
β, < ) < π)
β π:πβΆβ) |
90 | 80 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β (β
βm π) β§
π β β β§
sup(ran (abs β π),
β, < ) < π)
β β β β*) |
91 | 89, 90 | fssd 6691 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β (β
βm π) β§
π β β β§
sup(ran (abs β π),
β, < ) < π)
β π:πβΆβ*) |
92 | 91 | 3adant1l 1177 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β (β βm π)) β§ π β β β§ sup(ran (abs β
π), β, < ) <
π) β π:πβΆβ*) |
93 | 92 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β (β βm π)) β§ π β β β§ sup(ran (abs β
π), β, < ) <
π) β§ π β π) β (πβπ) β
β*) |
94 | | nnre 12167 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β β π β
β) |
95 | 94 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β β§ π β π) β π β β) |
96 | 95 | 3ad2antl2 1187 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β (β βm π)) β§ π β β β§ sup(ran (abs β
π), β, < ) <
π) β§ π β π) β π β β) |
97 | 96 | renegcld 11589 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β (β βm π)) β§ π β β β§ sup(ran (abs β
π), β, < ) <
π) β§ π β π) β -π β β) |
98 | 35 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β (β βm π)) β§ π β π) β (πβπ) β β) |
99 | 98 | 3ad2antl1 1186 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β (β βm π)) β§ π β β β§ sup(ran (abs β
π), β, < ) <
π) β§ π β π) β (πβπ) β β) |
100 | 99 | renegcld 11589 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π β (β βm π)) β§ π β β β§ sup(ran (abs β
π), β, < ) <
π) β§ π β π) β -(πβπ) β β) |
101 | | simpll 766 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π β (β βm π)) β§ π β π) β π) |
102 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π β (β βm π)) β§ π β π) β π β (β βm π)) |
103 | | n0i 4298 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β π β Β¬ π = β
) |
104 | 103 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π β (β βm π)) β§ π β π) β Β¬ π = β
) |
105 | 101, 102,
104, 67 | syl21anc 837 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β (β βm π)) β§ π β π) β sup(ran (abs β π), β, < ) β
β) |
106 | 105 | 3ad2antl1 1186 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π β (β βm π)) β§ π β β β§ sup(ran (abs β
π), β, < ) <
π) β§ π β π) β sup(ran (abs β π), β, < ) β
β) |
107 | 34 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β (β
βm π) β§
π β π) β (πβπ) β β) |
108 | 36, 107 | sselid 3947 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β (β
βm π) β§
π β π) β (πβπ) β β) |
109 | 108 | abscld 15328 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β (β
βm π) β§
π β π) β (absβ(πβπ)) β β) |
110 | 109 | adantll 713 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π β (β βm π)) β§ π β π) β (absβ(πβπ)) β β) |
111 | 110 | 3ad2antl1 1186 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π β (β βm π)) β§ π β β β§ sup(ran (abs β
π), β, < ) <
π) β§ π β π) β (absβ(πβπ)) β β) |
112 | 107 | renegcld 11589 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β (β
βm π) β§
π β π) β -(πβπ) β β) |
113 | 112 | leabsd 15306 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β (β
βm π) β§
π β π) β -(πβπ) β€ (absβ-(πβπ))) |
114 | 108 | absnegd 15341 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β (β
βm π) β§
π β π) β (absβ-(πβπ)) = (absβ(πβπ))) |
115 | 113, 114 | breqtrd 5136 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β (β
βm π) β§
π β π) β -(πβπ) β€ (absβ(πβπ))) |
116 | 115 | adantll 713 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π β (β βm π)) β§ π β π) β -(πβπ) β€ (absβ(πβπ))) |
117 | 116 | 3ad2antl1 1186 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π β (β βm π)) β§ π β β β§ sup(ran (abs β
π), β, < ) <
π) β§ π β π) β -(πβπ) β€ (absβ(πβπ))) |
118 | 29 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π β (β βm π)) β§ π β β β§ sup(ran (abs β
π), β, < ) <
π) β§ π β π) β ran (abs β π) β β) |
119 | 104, 64 | syldan 592 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π β (β βm π)) β§ π β π) β ran (abs β π) β β
) |
120 | 119 | 3ad2antl1 1186 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π β (β βm π)) β§ π β β β§ sup(ran (abs β
π), β, < ) <
π) β§ π β π) β ran (abs β π) β β
) |
121 | | fimaxre2 12107 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((ran
(abs β π) β
β β§ ran (abs β π) β Fin) β βπ¦ β β βπ§ β ran (abs β π)π§ β€ π¦) |
122 | 29, 44, 121 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π β (β βm π)) β βπ¦ β β βπ§ β ran (abs β π)π§ β€ π¦) |
123 | 122 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π β (β βm π)) β§ π β π) β βπ¦ β β βπ§ β ran (abs β π)π§ β€ π¦) |
124 | 123 | 3ad2antl1 1186 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π β (β βm π)) β§ π β β β§ sup(ran (abs β
π), β, < ) <
π) β§ π β π) β βπ¦ β β βπ§ β ran (abs β π)π§ β€ π¦) |
125 | | elmapfun 8811 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β (β
βm π)
β Fun π) |
126 | 125 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β (β
βm π) β§
π β π) β Fun π) |
127 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β (β
βm π) β§
π β π) β π β π) |
128 | 54 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π β (β
βm π)
β π = dom π) |
129 | 128 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β (β
βm π) β§
π β π) β π = dom π) |
130 | 127, 129 | eleqtrd 2840 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β (β
βm π) β§
π β π) β π β dom π) |
131 | | fvco 6944 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((Fun
π β§ π β dom π) β ((abs β π)βπ) = (absβ(πβπ))) |
132 | 126, 130,
131 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β (β
βm π) β§
π β π) β ((abs β π)βπ) = (absβ(πβπ))) |
133 | 132 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β (β
βm π) β§
π β π) β (absβ(πβπ)) = ((abs β π)βπ)) |
134 | | absfun 43658 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ Fun
abs |
135 | 134 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β (β
βm π)
β Fun abs) |
136 | | funco 6546 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((Fun abs
β§ Fun π) β Fun
(abs β π)) |
137 | 135, 125,
136 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β (β
βm π)
β Fun (abs β π)) |
138 | 137 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β (β
βm π) β§
π β π) β Fun (abs β π)) |
139 | 108, 48 | eleqtrdi 2848 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β (β
βm π) β§
π β π) β (πβπ) β dom abs) |
140 | | dmfco 6942 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((Fun
π β§ π β dom π) β (π β dom (abs β π) β (πβπ) β dom abs)) |
141 | 126, 130,
140 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β (β
βm π) β§
π β π) β (π β dom (abs β π) β (πβπ) β dom abs)) |
142 | 139, 141 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β (β
βm π) β§
π β π) β π β dom (abs β π)) |
143 | | fvelrn 7032 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((Fun
(abs β π) β§ π β dom (abs β π)) β ((abs β π)βπ) β ran (abs β π)) |
144 | 138, 142,
143 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β (β
βm π) β§
π β π) β ((abs β π)βπ) β ran (abs β π)) |
145 | 133, 144 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β (β
βm π) β§
π β π) β (absβ(πβπ)) β ran (abs β π)) |
146 | 145 | adantll 713 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π β (β βm π)) β§ π β π) β (absβ(πβπ)) β ran (abs β π)) |
147 | 146 | 3ad2antl1 1186 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π β (β βm π)) β§ π β β β§ sup(ran (abs β
π), β, < ) <
π) β§ π β π) β (absβ(πβπ)) β ran (abs β π)) |
148 | | suprub 12123 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((ran
(abs β π) β
β β§ ran (abs β π) β β
β§ βπ¦ β β βπ§ β ran (abs β π)π§ β€ π¦) β§ (absβ(πβπ)) β ran (abs β π)) β (absβ(πβπ)) β€ sup(ran (abs β π), β, <
)) |
149 | 118, 120,
124, 147, 148 | syl31anc 1374 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π β (β βm π)) β§ π β β β§ sup(ran (abs β
π), β, < ) <
π) β§ π β π) β (absβ(πβπ)) β€ sup(ran (abs β π), β, <
)) |
150 | 100, 111,
106, 117, 149 | letrd 11319 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π β (β βm π)) β§ π β β β§ sup(ran (abs β
π), β, < ) <
π) β§ π β π) β -(πβπ) β€ sup(ran (abs β π), β, <
)) |
151 | | simpl3 1194 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π β (β βm π)) β§ π β β β§ sup(ran (abs β
π), β, < ) <
π) β§ π β π) β sup(ran (abs β π), β, < ) < π) |
152 | 100, 106,
96, 150, 151 | lelttrd 11320 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β (β βm π)) β§ π β β β§ sup(ran (abs β
π), β, < ) <
π) β§ π β π) β -(πβπ) < π) |
153 | 100, 96 | ltnegd 11740 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β (β βm π)) β§ π β β β§ sup(ran (abs β
π), β, < ) <
π) β§ π β π) β (-(πβπ) < π β -π < --(πβπ))) |
154 | 152, 153 | mpbid 231 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β (β βm π)) β§ π β β β§ sup(ran (abs β
π), β, < ) <
π) β§ π β π) β -π < --(πβπ)) |
155 | 36, 99 | sselid 3947 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β (β βm π)) β§ π β β β§ sup(ran (abs β
π), β, < ) <
π) β§ π β π) β (πβπ) β β) |
156 | 155 | negnegd 11510 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β (β βm π)) β§ π β β β§ sup(ran (abs β
π), β, < ) <
π) β§ π β π) β --(πβπ) = (πβπ)) |
157 | 154, 156 | breqtrd 5136 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β (β βm π)) β§ π β β β§ sup(ran (abs β
π), β, < ) <
π) β§ π β π) β -π < (πβπ)) |
158 | 97, 99, 157 | ltled 11310 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β (β βm π)) β§ π β β β§ sup(ran (abs β
π), β, < ) <
π) β§ π β π) β -π β€ (πβπ)) |
159 | 99 | leabsd 15306 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β (β βm π)) β§ π β β β§ sup(ran (abs β
π), β, < ) <
π) β§ π β π) β (πβπ) β€ (absβ(πβπ))) |
160 | 99, 111, 106, 159, 149 | letrd 11319 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β (β βm π)) β§ π β β β§ sup(ran (abs β
π), β, < ) <
π) β§ π β π) β (πβπ) β€ sup(ran (abs β π), β, <
)) |
161 | 99, 106, 96, 160, 151 | lelttrd 11320 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β (β βm π)) β§ π β β β§ sup(ran (abs β
π), β, < ) <
π) β§ π β π) β (πβπ) < π) |
162 | 85, 88, 93, 158, 161 | elicod 13321 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β (β βm π)) β§ π β β β§ sup(ran (abs β
π), β, < ) <
π) β§ π β π) β (πβπ) β (-π[,)π)) |
163 | 73, 75, 76, 77, 162 | syl31anc 1374 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π β (β
βm π))
β§ π β β)
β§ sup(ran (abs β π), β, < ) < π) β§ π β π) β (πβπ) β (-π[,)π)) |
164 | 163 | adantl3r 749 |
. . . . . . . . . . . . . 14
β’
((((((π β§ π β (β
βm π))
β§ Β¬ π = β
)
β§ π β β)
β§ sup(ran (abs β π), β, < ) < π) β§ π β π) β (πβπ) β (-π[,)π)) |
165 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π β β) β π β β) |
166 | | mptexg 7176 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β Fin β (π₯ β π β¦ β¨-π, πβ©) β V) |
167 | 41, 166 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (π₯ β π β¦ β¨-π, πβ©) β V) |
168 | 167 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π β β) β (π₯ β π β¦ β¨-π, πβ©) β V) |
169 | | hoicvr.2 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ πΌ = (π β β β¦ (π₯ β π β¦ β¨-π, πβ©)) |
170 | 169 | fvmpt2 6964 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β β β§ (π₯ β π β¦ β¨-π, πβ©) β V) β (πΌβπ) = (π₯ β π β¦ β¨-π, πβ©)) |
171 | 165, 168,
170 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π β β) β (πΌβπ) = (π₯ β π β¦ β¨-π, πβ©)) |
172 | 171 | fveq1d 6849 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β β) β ((πΌβπ)βπ) = ((π₯ β π β¦ β¨-π, πβ©)βπ)) |
173 | 172 | 3adant3 1133 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β β β§ π β π) β ((πΌβπ)βπ) = ((π₯ β π β¦ β¨-π, πβ©)βπ)) |
174 | | eqidd 2738 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β π β (π₯ β π β¦ β¨-π, πβ©) = (π₯ β π β¦ β¨-π, πβ©)) |
175 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
β¨-π, πβ© = β¨-π, πβ© |
176 | 175 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β π β§ π₯ = π) β β¨-π, πβ© = β¨-π, πβ©) |
177 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β π β π β π) |
178 | | opex 5426 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
β¨-π, πβ© β V |
179 | 178 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β π β β¨-π, πβ© β V) |
180 | 174, 176,
177, 179 | fvmptd 6960 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β π β ((π₯ β π β¦ β¨-π, πβ©)βπ) = β¨-π, πβ©) |
181 | 180 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β β β§ π β π) β ((π₯ β π β¦ β¨-π, πβ©)βπ) = β¨-π, πβ©) |
182 | 173, 181 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β β β§ π β π) β ((πΌβπ)βπ) = β¨-π, πβ©) |
183 | 182 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β β β§ π β π) β (1st β((πΌβπ)βπ)) = (1st ββ¨-π, πβ©)) |
184 | | negex 11406 |
. . . . . . . . . . . . . . . . . . . . 21
β’ -π β V |
185 | | vex 3452 |
. . . . . . . . . . . . . . . . . . . . 21
β’ π β V |
186 | 184, 185 | op1st 7934 |
. . . . . . . . . . . . . . . . . . . 20
β’
(1st ββ¨-π, πβ©) = -π |
187 | 186 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β β β§ π β π) β (1st ββ¨-π, πβ©) = -π) |
188 | 183, 187 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β β§ π β π) β (1st β((πΌβπ)βπ)) = -π) |
189 | 182 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β β β§ π β π) β (2nd β((πΌβπ)βπ)) = (2nd ββ¨-π, πβ©)) |
190 | 184, 185 | op2nd 7935 |
. . . . . . . . . . . . . . . . . . . 20
β’
(2nd ββ¨-π, πβ©) = π |
191 | 190 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β β β§ π β π) β (2nd ββ¨-π, πβ©) = π) |
192 | 189, 191 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β β§ π β π) β (2nd β((πΌβπ)βπ)) = π) |
193 | 188, 192 | oveq12d 7380 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β β§ π β π) β ((1st β((πΌβπ)βπ))[,)(2nd β((πΌβπ)βπ))) = (-π[,)π)) |
194 | 193 | eqcomd 2743 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β β§ π β π) β (-π[,)π) = ((1st β((πΌβπ)βπ))[,)(2nd β((πΌβπ)βπ)))) |
195 | 194 | 3adant1r 1178 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (β βm π)) β§ π β β β§ π β π) β (-π[,)π) = ((1st β((πΌβπ)βπ))[,)(2nd β((πΌβπ)βπ)))) |
196 | 195 | ad5ant135 1369 |
. . . . . . . . . . . . . 14
β’
((((((π β§ π β (β
βm π))
β§ Β¬ π = β
)
β§ π β β)
β§ sup(ran (abs β π), β, < ) < π) β§ π β π) β (-π[,)π) = ((1st β((πΌβπ)βπ))[,)(2nd β((πΌβπ)βπ)))) |
197 | 164, 196 | eleqtrd 2840 |
. . . . . . . . . . . . 13
β’
((((((π β§ π β (β
βm π))
β§ Β¬ π = β
)
β§ π β β)
β§ sup(ran (abs β π), β, < ) < π) β§ π β π) β (πβπ) β ((1st β((πΌβπ)βπ))[,)(2nd β((πΌβπ)βπ)))) |
198 | 79, 82 | sselid 3947 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β β -π β
β) |
199 | | opelxpi 5675 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((-π β β β§ π β β) β
β¨-π, πβ© β (β Γ
β)) |
200 | 198, 94, 199 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β β
β¨-π, πβ© β (β Γ
β)) |
201 | 200 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β β) β§ π₯ β π) β β¨-π, πβ© β (β Γ
β)) |
202 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ β π β¦ β¨-π, πβ©) = (π₯ β π β¦ β¨-π, πβ©) |
203 | 201, 202 | fmptd 7067 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β) β (π₯ β π β¦ β¨-π, πβ©):πβΆ(β Γ
β)) |
204 | 171 | feq1d 6658 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β) β ((πΌβπ):πβΆ(β Γ β) β
(π₯ β π β¦ β¨-π, πβ©):πβΆ(β Γ
β))) |
205 | 203, 204 | mpbird 257 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β) β (πΌβπ):πβΆ(β Γ
β)) |
206 | 205 | ad4ant14 751 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β (β βm π)) β§ Β¬ π = β
) β§ π β β) β (πΌβπ):πβΆ(β Γ
β)) |
207 | 206 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ π β (β
βm π))
β§ Β¬ π = β
)
β§ π β β)
β§ sup(ran (abs β π), β, < ) < π) β§ π β π) β (πΌβπ):πβΆ(β Γ
β)) |
208 | | simpr 486 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ π β (β
βm π))
β§ Β¬ π = β
)
β§ π β β)
β§ sup(ran (abs β π), β, < ) < π) β§ π β π) β π β π) |
209 | 207, 208 | fvovco 43487 |
. . . . . . . . . . . . . 14
β’
((((((π β§ π β (β
βm π))
β§ Β¬ π = β
)
β§ π β β)
β§ sup(ran (abs β π), β, < ) < π) β§ π β π) β (([,) β (πΌβπ))βπ) = ((1st β((πΌβπ)βπ))[,)(2nd β((πΌβπ)βπ)))) |
210 | 209 | eqcomd 2743 |
. . . . . . . . . . . . 13
β’
((((((π β§ π β (β
βm π))
β§ Β¬ π = β
)
β§ π β β)
β§ sup(ran (abs β π), β, < ) < π) β§ π β π) β ((1st β((πΌβπ)βπ))[,)(2nd β((πΌβπ)βπ))) = (([,) β (πΌβπ))βπ)) |
211 | 197, 210 | eleqtrd 2840 |
. . . . . . . . . . . 12
β’
((((((π β§ π β (β
βm π))
β§ Β¬ π = β
)
β§ π β β)
β§ sup(ran (abs β π), β, < ) < π) β§ π β π) β (πβπ) β (([,) β (πΌβπ))βπ)) |
212 | 211 | ralrimiva 3144 |
. . . . . . . . . . 11
β’
(((((π β§ π β (β
βm π))
β§ Β¬ π = β
)
β§ π β β)
β§ sup(ran (abs β π), β, < ) < π) β βπ β π (πβπ) β (([,) β (πΌβπ))βπ)) |
213 | 72, 212 | jca 513 |
. . . . . . . . . 10
β’
(((((π β§ π β (β
βm π))
β§ Β¬ π = β
)
β§ π β β)
β§ sup(ran (abs β π), β, < ) < π) β (π Fn π β§ βπ β π (πβπ) β (([,) β (πΌβπ))βπ))) |
214 | | vex 3452 |
. . . . . . . . . . 11
β’ π β V |
215 | 214 | elixp 8849 |
. . . . . . . . . 10
β’ (π β Xπ β
π (([,) β (πΌβπ))βπ) β (π Fn π β§ βπ β π (πβπ) β (([,) β (πΌβπ))βπ))) |
216 | 213, 215 | sylibr 233 |
. . . . . . . . 9
β’
(((((π β§ π β (β
βm π))
β§ Β¬ π = β
)
β§ π β β)
β§ sup(ran (abs β π), β, < ) < π) β π β Xπ β π (([,) β (πΌβπ))βπ)) |
217 | 216 | ex 414 |
. . . . . . . 8
β’ ((((π β§ π β (β βm π)) β§ Β¬ π = β
) β§ π β β) β (sup(ran (abs β
π), β, < ) <
π β π β Xπ β π (([,) β (πΌβπ))βπ))) |
218 | 217 | reximdva 3166 |
. . . . . . 7
β’ (((π β§ π β (β βm π)) β§ Β¬ π = β
) β (βπ β β sup(ran (abs
β π), β, < )
< π β βπ β β π β Xπ β
π (([,) β (πΌβπ))βπ))) |
219 | 69, 218 | mpd 15 |
. . . . . 6
β’ (((π β§ π β (β βm π)) β§ Β¬ π = β
) β βπ β β π β Xπ β π (([,) β (πΌβπ))βπ)) |
220 | 22, 23, 24, 219 | syl21anc 837 |
. . . . 5
β’ (((π β§ Β¬ π = β
) β§ π β (β βm π)) β βπ β β π β Xπ β
π (([,) β (πΌβπ))βπ)) |
221 | | eliun 4963 |
. . . . 5
β’ (π β βͺ π β β Xπ β π (([,) β (πΌβπ))βπ) β βπ β β π β Xπ β π (([,) β (πΌβπ))βπ)) |
222 | 220, 221 | sylibr 233 |
. . . 4
β’ (((π β§ Β¬ π = β
) β§ π β (β βm π)) β π β βͺ
π β β Xπ β
π (([,) β (πΌβπ))βπ)) |
223 | 222 | ralrimiva 3144 |
. . 3
β’ ((π β§ Β¬ π = β
) β βπ β (β
βm π)π β βͺ π β β Xπ β π (([,) β (πΌβπ))βπ)) |
224 | | dfss3 3937 |
. . 3
β’ ((β
βm π)
β βͺ π β β Xπ β π (([,) β (πΌβπ))βπ) β βπ β (β βm π)π β βͺ
π β β Xπ β
π (([,) β (πΌβπ))βπ)) |
225 | 223, 224 | sylibr 233 |
. 2
β’ ((π β§ Β¬ π = β
) β (β
βm π)
β βͺ π β β Xπ β π (([,) β (πΌβπ))βπ)) |
226 | 21, 225 | pm2.61dan 812 |
1
β’ (π β (β
βm π)
β βͺ π β β Xπ β π (([,) β (πΌβπ))βπ)) |