Step | Hyp | Ref
| Expression |
1 | | supeq1 9382 |
. . . . 5
β’ (π΄ = β
β sup(π΄, β*, < ) =
sup(β
, β*, < )) |
2 | | xrsup0 13243 |
. . . . . 6
β’
sup(β
, β*, < ) = -β |
3 | 2 | a1i 11 |
. . . . 5
β’ (π΄ = β
β sup(β
,
β*, < ) = -β) |
4 | 1, 3 | eqtrd 2777 |
. . . 4
β’ (π΄ = β
β sup(π΄, β*, < ) =
-β) |
5 | 4 | adantl 483 |
. . 3
β’ ((π β§ π΄ = β
) β sup(π΄, β*, < ) =
-β) |
6 | | eleq2 2827 |
. . . . . . . . . 10
β’ (π΄ = β
β (-π₯ β π΄ β -π₯ β β
)) |
7 | 6 | rabbidv 3416 |
. . . . . . . . 9
β’ (π΄ = β
β {π₯ β β β£ -π₯ β π΄} = {π₯ β β β£ -π₯ β β
}) |
8 | | noel 4291 |
. . . . . . . . . . . . 13
β’ Β¬
-π₯ β
β
|
9 | 8 | a1i 11 |
. . . . . . . . . . . 12
β’ (π₯ β β β Β¬
-π₯ β
β
) |
10 | 9 | rgen 3067 |
. . . . . . . . . . 11
β’
βπ₯ β
β Β¬ -π₯ β
β
|
11 | | rabeq0 4345 |
. . . . . . . . . . 11
β’ ({π₯ β β β£ -π₯ β β
} = β
β βπ₯ β
β Β¬ -π₯ β
β
) |
12 | 10, 11 | mpbir 230 |
. . . . . . . . . 10
β’ {π₯ β β β£ -π₯ β β
} =
β
|
13 | 12 | a1i 11 |
. . . . . . . . 9
β’ (π΄ = β
β {π₯ β β β£ -π₯ β β
} =
β
) |
14 | 7, 13 | eqtrd 2777 |
. . . . . . . 8
β’ (π΄ = β
β {π₯ β β β£ -π₯ β π΄} = β
) |
15 | 14 | infeq1d 9414 |
. . . . . . 7
β’ (π΄ = β
β inf({π₯ β β β£ -π₯ β π΄}, β*, < ) =
inf(β
, β*, < )) |
16 | | xrinf0 13258 |
. . . . . . . 8
β’
inf(β
, β*, < ) = +β |
17 | 16 | a1i 11 |
. . . . . . 7
β’ (π΄ = β
β inf(β
,
β*, < ) = +β) |
18 | 15, 17 | eqtrd 2777 |
. . . . . 6
β’ (π΄ = β
β inf({π₯ β β β£ -π₯ β π΄}, β*, < ) =
+β) |
19 | 18 | xnegeqd 43679 |
. . . . 5
β’ (π΄ = β
β
-πinf({π₯
β β β£ -π₯
β π΄},
β*, < ) = -π+β) |
20 | | xnegpnf 13129 |
. . . . . 6
β’
-π+β = -β |
21 | 20 | a1i 11 |
. . . . 5
β’ (π΄ = β
β
-π+β = -β) |
22 | 19, 21 | eqtrd 2777 |
. . . 4
β’ (π΄ = β
β
-πinf({π₯
β β β£ -π₯
β π΄},
β*, < ) = -β) |
23 | 22 | adantl 483 |
. . 3
β’ ((π β§ π΄ = β
) β
-πinf({π₯
β β β£ -π₯
β π΄},
β*, < ) = -β) |
24 | 5, 23 | eqtr4d 2780 |
. 2
β’ ((π β§ π΄ = β
) β sup(π΄, β*, < ) =
-πinf({π₯
β β β£ -π₯
β π΄},
β*, < )) |
25 | | neqne 2952 |
. . 3
β’ (Β¬
π΄ = β
β π΄ β β
) |
26 | | supminfxr.1 |
. . . . . . 7
β’ (π β π΄ β β) |
27 | 26 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π΄ β β
) β§ βπ¦ β β βπ§ β π΄ π§ β€ π¦) β π΄ β β) |
28 | | simplr 768 |
. . . . . 6
β’ (((π β§ π΄ β β
) β§ βπ¦ β β βπ§ β π΄ π§ β€ π¦) β π΄ β β
) |
29 | | simpr 486 |
. . . . . 6
β’ (((π β§ π΄ β β
) β§ βπ¦ β β βπ§ β π΄ π§ β€ π¦) β βπ¦ β β βπ§ β π΄ π§ β€ π¦) |
30 | | negn0 11585 |
. . . . . . . . . 10
β’ ((π΄ β β β§ π΄ β β
) β {π₯ β β β£ -π₯ β π΄} β β
) |
31 | | ublbneg 12859 |
. . . . . . . . . 10
β’
(βπ¦ β
β βπ§ β
π΄ π§ β€ π¦ β βπ¦ β β βπ§ β {π₯ β β β£ -π₯ β π΄}π¦ β€ π§) |
32 | | ssrab2 4038 |
. . . . . . . . . . 11
β’ {π₯ β β β£ -π₯ β π΄} β β |
33 | | infrenegsup 12139 |
. . . . . . . . . . 11
β’ (({π₯ β β β£ -π₯ β π΄} β β β§ {π₯ β β β£ -π₯ β π΄} β β
β§ βπ¦ β β βπ§ β {π₯ β β β£ -π₯ β π΄}π¦ β€ π§) β inf({π₯ β β β£ -π₯ β π΄}, β, < ) = -sup({π€ β β β£ -π€ β {π₯ β β β£ -π₯ β π΄}}, β, < )) |
34 | 32, 33 | mp3an1 1449 |
. . . . . . . . . 10
β’ (({π₯ β β β£ -π₯ β π΄} β β
β§ βπ¦ β β βπ§ β {π₯ β β β£ -π₯ β π΄}π¦ β€ π§) β inf({π₯ β β β£ -π₯ β π΄}, β, < ) = -sup({π€ β β β£ -π€ β {π₯ β β β£ -π₯ β π΄}}, β, < )) |
35 | 30, 31, 34 | syl2an 597 |
. . . . . . . . 9
β’ (((π΄ β β β§ π΄ β β
) β§
βπ¦ β β
βπ§ β π΄ π§ β€ π¦) β inf({π₯ β β β£ -π₯ β π΄}, β, < ) = -sup({π€ β β β£ -π€ β {π₯ β β β£ -π₯ β π΄}}, β, < )) |
36 | 35 | 3impa 1111 |
. . . . . . . 8
β’ ((π΄ β β β§ π΄ β β
β§ βπ¦ β β βπ§ β π΄ π§ β€ π¦) β inf({π₯ β β β£ -π₯ β π΄}, β, < ) = -sup({π€ β β β£ -π€ β {π₯ β β β£ -π₯ β π΄}}, β, < )) |
37 | | elrabi 3640 |
. . . . . . . . . . . . 13
β’ (π¦ β {π€ β β β£ -π€ β {π₯ β β β£ -π₯ β π΄}} β π¦ β β) |
38 | 37 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ π¦ β {π€ β β β£ -π€ β {π₯ β β β£ -π₯ β π΄}}) β π¦ β β) |
39 | | ssel2 3940 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ π¦ β π΄) β π¦ β β) |
40 | | negeq 11394 |
. . . . . . . . . . . . . . . 16
β’ (π€ = π¦ β -π€ = -π¦) |
41 | 40 | eleq1d 2823 |
. . . . . . . . . . . . . . 15
β’ (π€ = π¦ β (-π€ β {π₯ β β β£ -π₯ β π΄} β -π¦ β {π₯ β β β£ -π₯ β π΄})) |
42 | 41 | elrab3 3647 |
. . . . . . . . . . . . . 14
β’ (π¦ β β β (π¦ β {π€ β β β£ -π€ β {π₯ β β β£ -π₯ β π΄}} β -π¦ β {π₯ β β β£ -π₯ β π΄})) |
43 | | renegcl 11465 |
. . . . . . . . . . . . . . 15
β’ (π¦ β β β -π¦ β
β) |
44 | | negeq 11394 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = -π¦ β -π₯ = --π¦) |
45 | 44 | eleq1d 2823 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = -π¦ β (-π₯ β π΄ β --π¦ β π΄)) |
46 | 45 | elrab3 3647 |
. . . . . . . . . . . . . . 15
β’ (-π¦ β β β (-π¦ β {π₯ β β β£ -π₯ β π΄} β --π¦ β π΄)) |
47 | 43, 46 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π¦ β β β (-π¦ β {π₯ β β β£ -π₯ β π΄} β --π¦ β π΄)) |
48 | | recn 11142 |
. . . . . . . . . . . . . . . 16
β’ (π¦ β β β π¦ β
β) |
49 | 48 | negnegd 11504 |
. . . . . . . . . . . . . . 15
β’ (π¦ β β β --π¦ = π¦) |
50 | 49 | eleq1d 2823 |
. . . . . . . . . . . . . 14
β’ (π¦ β β β (--π¦ β π΄ β π¦ β π΄)) |
51 | 42, 47, 50 | 3bitrd 305 |
. . . . . . . . . . . . 13
β’ (π¦ β β β (π¦ β {π€ β β β£ -π€ β {π₯ β β β£ -π₯ β π΄}} β π¦ β π΄)) |
52 | 51 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ π¦ β β) β (π¦ β {π€ β β β£ -π€ β {π₯ β β β£ -π₯ β π΄}} β π¦ β π΄)) |
53 | 38, 39, 52 | eqrdav 2736 |
. . . . . . . . . . 11
β’ (π΄ β β β {π€ β β β£ -π€ β {π₯ β β β£ -π₯ β π΄}} = π΄) |
54 | 53 | supeq1d 9383 |
. . . . . . . . . 10
β’ (π΄ β β β
sup({π€ β β
β£ -π€ β {π₯ β β β£ -π₯ β π΄}}, β, < ) = sup(π΄, β, < )) |
55 | 54 | 3ad2ant1 1134 |
. . . . . . . . 9
β’ ((π΄ β β β§ π΄ β β
β§ βπ¦ β β βπ§ β π΄ π§ β€ π¦) β sup({π€ β β β£ -π€ β {π₯ β β β£ -π₯ β π΄}}, β, < ) = sup(π΄, β, < )) |
56 | 55 | negeqd 11396 |
. . . . . . . 8
β’ ((π΄ β β β§ π΄ β β
β§ βπ¦ β β βπ§ β π΄ π§ β€ π¦) β -sup({π€ β β β£ -π€ β {π₯ β β β£ -π₯ β π΄}}, β, < ) = -sup(π΄, β, < )) |
57 | 36, 56 | eqtrd 2777 |
. . . . . . 7
β’ ((π΄ β β β§ π΄ β β
β§ βπ¦ β β βπ§ β π΄ π§ β€ π¦) β inf({π₯ β β β£ -π₯ β π΄}, β, < ) = -sup(π΄, β, < )) |
58 | | infrecl 12138 |
. . . . . . . . . . 11
β’ (({π₯ β β β£ -π₯ β π΄} β β β§ {π₯ β β β£ -π₯ β π΄} β β
β§ βπ¦ β β βπ§ β {π₯ β β β£ -π₯ β π΄}π¦ β€ π§) β inf({π₯ β β β£ -π₯ β π΄}, β, < ) β
β) |
59 | 32, 58 | mp3an1 1449 |
. . . . . . . . . 10
β’ (({π₯ β β β£ -π₯ β π΄} β β
β§ βπ¦ β β βπ§ β {π₯ β β β£ -π₯ β π΄}π¦ β€ π§) β inf({π₯ β β β£ -π₯ β π΄}, β, < ) β
β) |
60 | 30, 31, 59 | syl2an 597 |
. . . . . . . . 9
β’ (((π΄ β β β§ π΄ β β
) β§
βπ¦ β β
βπ§ β π΄ π§ β€ π¦) β inf({π₯ β β β£ -π₯ β π΄}, β, < ) β
β) |
61 | 60 | 3impa 1111 |
. . . . . . . 8
β’ ((π΄ β β β§ π΄ β β
β§ βπ¦ β β βπ§ β π΄ π§ β€ π¦) β inf({π₯ β β β£ -π₯ β π΄}, β, < ) β
β) |
62 | | suprcl 12116 |
. . . . . . . 8
β’ ((π΄ β β β§ π΄ β β
β§ βπ¦ β β βπ§ β π΄ π§ β€ π¦) β sup(π΄, β, < ) β
β) |
63 | | recn 11142 |
. . . . . . . . 9
β’
(inf({π₯ β
β β£ -π₯ β
π΄}, β, < ) β
β β inf({π₯
β β β£ -π₯
β π΄}, β, < )
β β) |
64 | | recn 11142 |
. . . . . . . . 9
β’
(sup(π΄, β,
< ) β β β sup(π΄, β, < ) β
β) |
65 | | negcon2 11455 |
. . . . . . . . 9
β’
((inf({π₯ β
β β£ -π₯ β
π΄}, β, < ) β
β β§ sup(π΄,
β, < ) β β) β (inf({π₯ β β β£ -π₯ β π΄}, β, < ) = -sup(π΄, β, < ) β sup(π΄, β, < ) = -inf({π₯ β β β£ -π₯ β π΄}, β, < ))) |
66 | 63, 64, 65 | syl2an 597 |
. . . . . . . 8
β’
((inf({π₯ β
β β£ -π₯ β
π΄}, β, < ) β
β β§ sup(π΄,
β, < ) β β) β (inf({π₯ β β β£ -π₯ β π΄}, β, < ) = -sup(π΄, β, < ) β sup(π΄, β, < ) = -inf({π₯ β β β£ -π₯ β π΄}, β, < ))) |
67 | 61, 62, 66 | syl2anc 585 |
. . . . . . 7
β’ ((π΄ β β β§ π΄ β β
β§ βπ¦ β β βπ§ β π΄ π§ β€ π¦) β (inf({π₯ β β β£ -π₯ β π΄}, β, < ) = -sup(π΄, β, < ) β sup(π΄, β, < ) = -inf({π₯ β β β£ -π₯ β π΄}, β, < ))) |
68 | 57, 67 | mpbid 231 |
. . . . . 6
β’ ((π΄ β β β§ π΄ β β
β§ βπ¦ β β βπ§ β π΄ π§ β€ π¦) β sup(π΄, β, < ) = -inf({π₯ β β β£ -π₯ β π΄}, β, < )) |
69 | 27, 28, 29, 68 | syl3anc 1372 |
. . . . 5
β’ (((π β§ π΄ β β
) β§ βπ¦ β β βπ§ β π΄ π§ β€ π¦) β sup(π΄, β, < ) = -inf({π₯ β β β£ -π₯ β π΄}, β, < )) |
70 | | supxrre 13247 |
. . . . . 6
β’ ((π΄ β β β§ π΄ β β
β§ βπ¦ β β βπ§ β π΄ π§ β€ π¦) β sup(π΄, β*, < ) = sup(π΄, β, <
)) |
71 | 27, 28, 29, 70 | syl3anc 1372 |
. . . . 5
β’ (((π β§ π΄ β β
) β§ βπ¦ β β βπ§ β π΄ π§ β€ π¦) β sup(π΄, β*, < ) = sup(π΄, β, <
)) |
72 | 32 | a1i 11 |
. . . . . . . 8
β’ (((π β§ π΄ β β
) β§ βπ¦ β β βπ§ β π΄ π§ β€ π¦) β {π₯ β β β£ -π₯ β π΄} β β) |
73 | 27, 28, 30 | syl2anc 585 |
. . . . . . . 8
β’ (((π β§ π΄ β β
) β§ βπ¦ β β βπ§ β π΄ π§ β€ π¦) β {π₯ β β β£ -π₯ β π΄} β β
) |
74 | 29, 31 | syl 17 |
. . . . . . . 8
β’ (((π β§ π΄ β β
) β§ βπ¦ β β βπ§ β π΄ π§ β€ π¦) β βπ¦ β β βπ§ β {π₯ β β β£ -π₯ β π΄}π¦ β€ π§) |
75 | | infxrre 13256 |
. . . . . . . 8
β’ (({π₯ β β β£ -π₯ β π΄} β β β§ {π₯ β β β£ -π₯ β π΄} β β
β§ βπ¦ β β βπ§ β {π₯ β β β£ -π₯ β π΄}π¦ β€ π§) β inf({π₯ β β β£ -π₯ β π΄}, β*, < ) = inf({π₯ β β β£ -π₯ β π΄}, β, < )) |
76 | 72, 73, 74, 75 | syl3anc 1372 |
. . . . . . 7
β’ (((π β§ π΄ β β
) β§ βπ¦ β β βπ§ β π΄ π§ β€ π¦) β inf({π₯ β β β£ -π₯ β π΄}, β*, < ) = inf({π₯ β β β£ -π₯ β π΄}, β, < )) |
77 | 76 | xnegeqd 43679 |
. . . . . 6
β’ (((π β§ π΄ β β
) β§ βπ¦ β β βπ§ β π΄ π§ β€ π¦) β -πinf({π₯ β β β£ -π₯ β π΄}, β*, < ) =
-πinf({π₯
β β β£ -π₯
β π΄}, β, <
)) |
78 | 26, 60 | sylanl1 679 |
. . . . . . 7
β’ (((π β§ π΄ β β
) β§ βπ¦ β β βπ§ β π΄ π§ β€ π¦) β inf({π₯ β β β£ -π₯ β π΄}, β, < ) β
β) |
79 | 78 | rexnegd 43360 |
. . . . . 6
β’ (((π β§ π΄ β β
) β§ βπ¦ β β βπ§ β π΄ π§ β€ π¦) β -πinf({π₯ β β β£ -π₯ β π΄}, β, < ) = -inf({π₯ β β β£ -π₯ β π΄}, β, < )) |
80 | 77, 79 | eqtrd 2777 |
. . . . 5
β’ (((π β§ π΄ β β
) β§ βπ¦ β β βπ§ β π΄ π§ β€ π¦) β -πinf({π₯ β β β£ -π₯ β π΄}, β*, < ) = -inf({π₯ β β β£ -π₯ β π΄}, β, < )) |
81 | 69, 71, 80 | 3eqtr4d 2787 |
. . . 4
β’ (((π β§ π΄ β β
) β§ βπ¦ β β βπ§ β π΄ π§ β€ π¦) β sup(π΄, β*, < ) =
-πinf({π₯
β β β£ -π₯
β π΄},
β*, < )) |
82 | | simpr 486 |
. . . . . . 7
β’ ((π β§ Β¬ βπ¦ β β βπ§ β π΄ π§ β€ π¦) β Β¬ βπ¦ β β βπ§ β π΄ π§ β€ π¦) |
83 | | simplr 768 |
. . . . . . . . . . . . 13
β’ (((π β§ π¦ β β) β§ π§ β π΄) β π¦ β β) |
84 | 26 | sselda 3945 |
. . . . . . . . . . . . . 14
β’ ((π β§ π§ β π΄) β π§ β β) |
85 | 84 | adantlr 714 |
. . . . . . . . . . . . 13
β’ (((π β§ π¦ β β) β§ π§ β π΄) β π§ β β) |
86 | 83, 85 | ltnled 11303 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β β) β§ π§ β π΄) β (π¦ < π§ β Β¬ π§ β€ π¦)) |
87 | 86 | rexbidva 3174 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β β) β (βπ§ β π΄ π¦ < π§ β βπ§ β π΄ Β¬ π§ β€ π¦)) |
88 | | rexnal 3104 |
. . . . . . . . . . . 12
β’
(βπ§ β
π΄ Β¬ π§ β€ π¦ β Β¬ βπ§ β π΄ π§ β€ π¦) |
89 | 88 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β β) β (βπ§ β π΄ Β¬ π§ β€ π¦ β Β¬ βπ§ β π΄ π§ β€ π¦)) |
90 | 87, 89 | bitrd 279 |
. . . . . . . . . 10
β’ ((π β§ π¦ β β) β (βπ§ β π΄ π¦ < π§ β Β¬ βπ§ β π΄ π§ β€ π¦)) |
91 | 90 | ralbidva 3173 |
. . . . . . . . 9
β’ (π β (βπ¦ β β βπ§ β π΄ π¦ < π§ β βπ¦ β β Β¬ βπ§ β π΄ π§ β€ π¦)) |
92 | | ralnex 3076 |
. . . . . . . . . 10
β’
(βπ¦ β
β Β¬ βπ§
β π΄ π§ β€ π¦ β Β¬ βπ¦ β β βπ§ β π΄ π§ β€ π¦) |
93 | 92 | a1i 11 |
. . . . . . . . 9
β’ (π β (βπ¦ β β Β¬
βπ§ β π΄ π§ β€ π¦ β Β¬ βπ¦ β β βπ§ β π΄ π§ β€ π¦)) |
94 | 91, 93 | bitrd 279 |
. . . . . . . 8
β’ (π β (βπ¦ β β βπ§ β π΄ π¦ < π§ β Β¬ βπ¦ β β βπ§ β π΄ π§ β€ π¦)) |
95 | 94 | adantr 482 |
. . . . . . 7
β’ ((π β§ Β¬ βπ¦ β β βπ§ β π΄ π§ β€ π¦) β (βπ¦ β β βπ§ β π΄ π¦ < π§ β Β¬ βπ¦ β β βπ§ β π΄ π§ β€ π¦)) |
96 | 82, 95 | mpbird 257 |
. . . . . 6
β’ ((π β§ Β¬ βπ¦ β β βπ§ β π΄ π§ β€ π¦) β βπ¦ β β βπ§ β π΄ π¦ < π§) |
97 | | xnegmnf 13130 |
. . . . . . . . 9
β’
-π-β = +β |
98 | 97 | eqcomi 2746 |
. . . . . . . 8
β’ +β
= -π-β |
99 | 98 | a1i 11 |
. . . . . . 7
β’ ((π β§ βπ¦ β β βπ§ β π΄ π¦ < π§) β +β =
-π-β) |
100 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ βπ¦ β β βπ§ β π΄ π¦ < π§) β βπ¦ β β βπ§ β π΄ π¦ < π§) |
101 | | ressxr 11200 |
. . . . . . . . . . . 12
β’ β
β β* |
102 | 101 | a1i 11 |
. . . . . . . . . . 11
β’ (π β β β
β*) |
103 | 26, 102 | sstrd 3955 |
. . . . . . . . . 10
β’ (π β π΄ β
β*) |
104 | | supxrunb2 13240 |
. . . . . . . . . 10
β’ (π΄ β β*
β (βπ¦ β
β βπ§ β
π΄ π¦ < π§ β sup(π΄, β*, < ) =
+β)) |
105 | 103, 104 | syl 17 |
. . . . . . . . 9
β’ (π β (βπ¦ β β βπ§ β π΄ π¦ < π§ β sup(π΄, β*, < ) =
+β)) |
106 | 105 | adantr 482 |
. . . . . . . 8
β’ ((π β§ βπ¦ β β βπ§ β π΄ π¦ < π§) β (βπ¦ β β βπ§ β π΄ π¦ < π§ β sup(π΄, β*, < ) =
+β)) |
107 | 100, 106 | mpbid 231 |
. . . . . . 7
β’ ((π β§ βπ¦ β β βπ§ β π΄ π¦ < π§) β sup(π΄, β*, < ) =
+β) |
108 | | renegcl 11465 |
. . . . . . . . . . . . . 14
β’ (π£ β β β -π£ β
β) |
109 | 108 | adantl 483 |
. . . . . . . . . . . . 13
β’
((βπ¦ β
β βπ§ β
π΄ π¦ < π§ β§ π£ β β) β -π£ β β) |
110 | | simpl 484 |
. . . . . . . . . . . . 13
β’
((βπ¦ β
β βπ§ β
π΄ π¦ < π§ β§ π£ β β) β βπ¦ β β βπ§ β π΄ π¦ < π§) |
111 | | breq1 5109 |
. . . . . . . . . . . . . . 15
β’ (π¦ = -π£ β (π¦ < π§ β -π£ < π§)) |
112 | 111 | rexbidv 3176 |
. . . . . . . . . . . . . 14
β’ (π¦ = -π£ β (βπ§ β π΄ π¦ < π§ β βπ§ β π΄ -π£ < π§)) |
113 | 112 | rspcva 3580 |
. . . . . . . . . . . . 13
β’ ((-π£ β β β§
βπ¦ β β
βπ§ β π΄ π¦ < π§) β βπ§ β π΄ -π£ < π§) |
114 | 109, 110,
113 | syl2anc 585 |
. . . . . . . . . . . 12
β’
((βπ¦ β
β βπ§ β
π΄ π¦ < π§ β§ π£ β β) β βπ§ β π΄ -π£ < π§) |
115 | 114 | adantll 713 |
. . . . . . . . . . 11
β’ (((π β§ βπ¦ β β βπ§ β π΄ π¦ < π§) β§ π£ β β) β βπ§ β π΄ -π£ < π§) |
116 | | negeq 11394 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = -π§ β -π₯ = --π§) |
117 | 116 | eleq1d 2823 |
. . . . . . . . . . . . . . 15
β’ (π₯ = -π§ β (-π₯ β π΄ β --π§ β π΄)) |
118 | 84 | renegcld 11583 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π§ β π΄) β -π§ β β) |
119 | 118 | ad4ant13 750 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π£ β β) β§ π§ β π΄) β§ -π£ < π§) β -π§ β β) |
120 | 84 | recnd 11184 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π§ β π΄) β π§ β β) |
121 | 120 | negnegd 11504 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π§ β π΄) β --π§ = π§) |
122 | | simpr 486 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π§ β π΄) β π§ β π΄) |
123 | 121, 122 | eqeltrd 2838 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π§ β π΄) β --π§ β π΄) |
124 | 123 | ad4ant13 750 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π£ β β) β§ π§ β π΄) β§ -π£ < π§) β --π§ β π΄) |
125 | 117, 119,
124 | elrabd 3648 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π£ β β) β§ π§ β π΄) β§ -π£ < π§) β -π§ β {π₯ β β β£ -π₯ β π΄}) |
126 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π£ β β) β§ π§ β π΄) β§ -π£ < π§) β -π£ < π§) |
127 | 108 | ad3antlr 730 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π£ β β) β§ π§ β π΄) β§ -π£ < π§) β -π£ β β) |
128 | 84 | ad4ant13 750 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π£ β β) β§ π§ β π΄) β§ -π£ < π§) β π§ β β) |
129 | 127, 128 | ltnegd 11734 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π£ β β) β§ π§ β π΄) β§ -π£ < π§) β (-π£ < π§ β -π§ < --π£)) |
130 | 126, 129 | mpbid 231 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π£ β β) β§ π§ β π΄) β§ -π£ < π§) β -π§ < --π£) |
131 | | simpllr 775 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π£ β β) β§ π§ β π΄) β§ -π£ < π§) β π£ β β) |
132 | | recn 11142 |
. . . . . . . . . . . . . . . 16
β’ (π£ β β β π£ β
β) |
133 | | negneg 11452 |
. . . . . . . . . . . . . . . 16
β’ (π£ β β β --π£ = π£) |
134 | 131, 132,
133 | 3syl 18 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π£ β β) β§ π§ β π΄) β§ -π£ < π§) β --π£ = π£) |
135 | 130, 134 | breqtrd 5132 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π£ β β) β§ π§ β π΄) β§ -π£ < π§) β -π§ < π£) |
136 | | breq1 5109 |
. . . . . . . . . . . . . . 15
β’ (π€ = -π§ β (π€ < π£ β -π§ < π£)) |
137 | 136 | rspcev 3582 |
. . . . . . . . . . . . . 14
β’ ((-π§ β {π₯ β β β£ -π₯ β π΄} β§ -π§ < π£) β βπ€ β {π₯ β β β£ -π₯ β π΄}π€ < π£) |
138 | 125, 135,
137 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((((π β§ π£ β β) β§ π§ β π΄) β§ -π£ < π§) β βπ€ β {π₯ β β β£ -π₯ β π΄}π€ < π£) |
139 | 138 | rexlimdva2 3155 |
. . . . . . . . . . . 12
β’ ((π β§ π£ β β) β (βπ§ β π΄ -π£ < π§ β βπ€ β {π₯ β β β£ -π₯ β π΄}π€ < π£)) |
140 | 139 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π β§ βπ¦ β β βπ§ β π΄ π¦ < π§) β§ π£ β β) β (βπ§ β π΄ -π£ < π§ β βπ€ β {π₯ β β β£ -π₯ β π΄}π€ < π£)) |
141 | 115, 140 | mpd 15 |
. . . . . . . . . 10
β’ (((π β§ βπ¦ β β βπ§ β π΄ π¦ < π§) β§ π£ β β) β βπ€ β {π₯ β β β£ -π₯ β π΄}π€ < π£) |
142 | 141 | ralrimiva 3144 |
. . . . . . . . 9
β’ ((π β§ βπ¦ β β βπ§ β π΄ π¦ < π§) β βπ£ β β βπ€ β {π₯ β β β£ -π₯ β π΄}π€ < π£) |
143 | 32, 101 | sstri 3954 |
. . . . . . . . . 10
β’ {π₯ β β β£ -π₯ β π΄} β
β* |
144 | | infxrunb2 43609 |
. . . . . . . . . 10
β’ ({π₯ β β β£ -π₯ β π΄} β β* β
(βπ£ β β
βπ€ β {π₯ β β β£ -π₯ β π΄}π€ < π£ β inf({π₯ β β β£ -π₯ β π΄}, β*, < ) =
-β)) |
145 | 143, 144 | ax-mp 5 |
. . . . . . . . 9
β’
(βπ£ β
β βπ€ β
{π₯ β β β£
-π₯ β π΄}π€ < π£ β inf({π₯ β β β£ -π₯ β π΄}, β*, < ) =
-β) |
146 | 142, 145 | sylib 217 |
. . . . . . . 8
β’ ((π β§ βπ¦ β β βπ§ β π΄ π¦ < π§) β inf({π₯ β β β£ -π₯ β π΄}, β*, < ) =
-β) |
147 | 146 | xnegeqd 43679 |
. . . . . . 7
β’ ((π β§ βπ¦ β β βπ§ β π΄ π¦ < π§) β -πinf({π₯ β β β£ -π₯ β π΄}, β*, < ) =
-π-β) |
148 | 99, 107, 147 | 3eqtr4d 2787 |
. . . . . 6
β’ ((π β§ βπ¦ β β βπ§ β π΄ π¦ < π§) β sup(π΄, β*, < ) =
-πinf({π₯
β β β£ -π₯
β π΄},
β*, < )) |
149 | 96, 148 | syldan 592 |
. . . . 5
β’ ((π β§ Β¬ βπ¦ β β βπ§ β π΄ π§ β€ π¦) β sup(π΄, β*, < ) =
-πinf({π₯
β β β£ -π₯
β π΄},
β*, < )) |
150 | 149 | adantlr 714 |
. . . 4
β’ (((π β§ π΄ β β
) β§ Β¬ βπ¦ β β βπ§ β π΄ π§ β€ π¦) β sup(π΄, β*, < ) =
-πinf({π₯
β β β£ -π₯
β π΄},
β*, < )) |
151 | 81, 150 | pm2.61dan 812 |
. . 3
β’ ((π β§ π΄ β β
) β sup(π΄, β*, < ) =
-πinf({π₯
β β β£ -π₯
β π΄},
β*, < )) |
152 | 25, 151 | sylan2 594 |
. 2
β’ ((π β§ Β¬ π΄ = β
) β sup(π΄, β*, < ) =
-πinf({π₯
β β β£ -π₯
β π΄},
β*, < )) |
153 | 24, 152 | pm2.61dan 812 |
1
β’ (π β sup(π΄, β*, < ) =
-πinf({π₯
β β β£ -π₯
β π΄},
β*, < )) |