Step | Hyp | Ref
| Expression |
1 | | supmul.2 |
. . . . . . 7
โข (๐ โ ((โ๐ฅ โ ๐ด 0 โค ๐ฅ โง โ๐ฅ โ ๐ต 0 โค ๐ฅ) โง (๐ด โ โ โง ๐ด โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ) โง (๐ต โ โ โง ๐ต โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ต ๐ฆ โค ๐ฅ))) |
2 | 1 | simp2bi 1147 |
. . . . . 6
โข (๐ โ (๐ด โ โ โง ๐ด โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ)) |
3 | | suprcl 12123 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ) โ sup(๐ด, โ, < ) โ
โ) |
4 | 2, 3 | syl 17 |
. . . . 5
โข (๐ โ sup(๐ด, โ, < ) โ
โ) |
5 | 1 | simp3bi 1148 |
. . . . . 6
โข (๐ โ (๐ต โ โ โง ๐ต โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ต ๐ฆ โค ๐ฅ)) |
6 | | suprcl 12123 |
. . . . . 6
โข ((๐ต โ โ โง ๐ต โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ต ๐ฆ โค ๐ฅ) โ sup(๐ต, โ, < ) โ
โ) |
7 | 5, 6 | syl 17 |
. . . . 5
โข (๐ โ sup(๐ต, โ, < ) โ
โ) |
8 | | recn 11149 |
. . . . . 6
โข
(sup(๐ด, โ,
< ) โ โ โ sup(๐ด, โ, < ) โ
โ) |
9 | | recn 11149 |
. . . . . 6
โข
(sup(๐ต, โ,
< ) โ โ โ sup(๐ต, โ, < ) โ
โ) |
10 | | mulcom 11145 |
. . . . . 6
โข
((sup(๐ด, โ,
< ) โ โ โง sup(๐ต, โ, < ) โ โ) โ
(sup(๐ด, โ, < )
ยท sup(๐ต, โ,
< )) = (sup(๐ต, โ,
< ) ยท sup(๐ด,
โ, < ))) |
11 | 8, 9, 10 | syl2an 597 |
. . . . 5
โข
((sup(๐ด, โ,
< ) โ โ โง sup(๐ต, โ, < ) โ โ) โ
(sup(๐ด, โ, < )
ยท sup(๐ต, โ,
< )) = (sup(๐ต, โ,
< ) ยท sup(๐ด,
โ, < ))) |
12 | 4, 7, 11 | syl2anc 585 |
. . . 4
โข (๐ โ (sup(๐ด, โ, < ) ยท sup(๐ต, โ, < )) = (sup(๐ต, โ, < ) ยท
sup(๐ด, โ, <
))) |
13 | 5 | simp2d 1144 |
. . . . . . 7
โข (๐ โ ๐ต โ โ
) |
14 | | n0 4310 |
. . . . . . 7
โข (๐ต โ โ
โ
โ๐ ๐ โ ๐ต) |
15 | 13, 14 | sylib 217 |
. . . . . 6
โข (๐ โ โ๐ ๐ โ ๐ต) |
16 | | 0red 11166 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐ต) โ 0 โ โ) |
17 | 5 | simp1d 1143 |
. . . . . . . 8
โข (๐ โ ๐ต โ โ) |
18 | 17 | sselda 3948 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐ต) โ ๐ โ โ) |
19 | 7 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐ต) โ sup(๐ต, โ, < ) โ
โ) |
20 | | simp1r 1199 |
. . . . . . . . . 10
โข
(((โ๐ฅ โ
๐ด 0 โค ๐ฅ โง โ๐ฅ โ ๐ต 0 โค ๐ฅ) โง (๐ด โ โ โง ๐ด โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ) โง (๐ต โ โ โง ๐ต โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ต ๐ฆ โค ๐ฅ)) โ โ๐ฅ โ ๐ต 0 โค ๐ฅ) |
21 | 1, 20 | sylbi 216 |
. . . . . . . . 9
โข (๐ โ โ๐ฅ โ ๐ต 0 โค ๐ฅ) |
22 | | breq2 5113 |
. . . . . . . . . 10
โข (๐ฅ = ๐ โ (0 โค ๐ฅ โ 0 โค ๐)) |
23 | 22 | rspccv 3580 |
. . . . . . . . 9
โข
(โ๐ฅ โ
๐ต 0 โค ๐ฅ โ (๐ โ ๐ต โ 0 โค ๐)) |
24 | 21, 23 | syl 17 |
. . . . . . . 8
โข (๐ โ (๐ โ ๐ต โ 0 โค ๐)) |
25 | 24 | imp 408 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐ต) โ 0 โค ๐) |
26 | | suprub 12124 |
. . . . . . . 8
โข (((๐ต โ โ โง ๐ต โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ต ๐ฆ โค ๐ฅ) โง ๐ โ ๐ต) โ ๐ โค sup(๐ต, โ, < )) |
27 | 5, 26 | sylan 581 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐ต) โ ๐ โค sup(๐ต, โ, < )) |
28 | 16, 18, 19, 25, 27 | letrd 11320 |
. . . . . 6
โข ((๐ โง ๐ โ ๐ต) โ 0 โค sup(๐ต, โ, < )) |
29 | 15, 28 | exlimddv 1939 |
. . . . 5
โข (๐ โ 0 โค sup(๐ต, โ, <
)) |
30 | | simp1l 1198 |
. . . . . 6
โข
(((โ๐ฅ โ
๐ด 0 โค ๐ฅ โง โ๐ฅ โ ๐ต 0 โค ๐ฅ) โง (๐ด โ โ โง ๐ด โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ) โง (๐ต โ โ โง ๐ต โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ต ๐ฆ โค ๐ฅ)) โ โ๐ฅ โ ๐ด 0 โค ๐ฅ) |
31 | 1, 30 | sylbi 216 |
. . . . 5
โข (๐ โ โ๐ฅ โ ๐ด 0 โค ๐ฅ) |
32 | | eqid 2733 |
. . . . . 6
โข {๐ง โฃ โ๐ โ ๐ด ๐ง = (sup(๐ต, โ, < ) ยท ๐)} = {๐ง โฃ โ๐ โ ๐ด ๐ง = (sup(๐ต, โ, < ) ยท ๐)} |
33 | | biid 261 |
. . . . . 6
โข
(((sup(๐ต, โ,
< ) โ โ โง 0 โค sup(๐ต, โ, < ) โง โ๐ฅ โ ๐ด 0 โค ๐ฅ) โง (๐ด โ โ โง ๐ด โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ)) โ ((sup(๐ต, โ, < ) โ โ โง 0
โค sup(๐ต, โ, < )
โง โ๐ฅ โ
๐ด 0 โค ๐ฅ) โง (๐ด โ โ โง ๐ด โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ))) |
34 | 32, 33 | supmul1 12132 |
. . . . 5
โข
(((sup(๐ต, โ,
< ) โ โ โง 0 โค sup(๐ต, โ, < ) โง โ๐ฅ โ ๐ด 0 โค ๐ฅ) โง (๐ด โ โ โง ๐ด โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ)) โ (sup(๐ต, โ, < ) ยท sup(๐ด, โ, < )) = sup({๐ง โฃ โ๐ โ ๐ด ๐ง = (sup(๐ต, โ, < ) ยท ๐)}, โ, <
)) |
35 | 7, 29, 31, 2, 34 | syl31anc 1374 |
. . . 4
โข (๐ โ (sup(๐ต, โ, < ) ยท sup(๐ด, โ, < )) = sup({๐ง โฃ โ๐ โ ๐ด ๐ง = (sup(๐ต, โ, < ) ยท ๐)}, โ, <
)) |
36 | 12, 35 | eqtrd 2773 |
. . 3
โข (๐ โ (sup(๐ด, โ, < ) ยท sup(๐ต, โ, < )) = sup({๐ง โฃ โ๐ โ ๐ด ๐ง = (sup(๐ต, โ, < ) ยท ๐)}, โ, <
)) |
37 | | vex 3451 |
. . . . . . 7
โข ๐ค โ V |
38 | | eqeq1 2737 |
. . . . . . . 8
โข (๐ง = ๐ค โ (๐ง = (sup(๐ต, โ, < ) ยท ๐) โ ๐ค = (sup(๐ต, โ, < ) ยท ๐))) |
39 | 38 | rexbidv 3172 |
. . . . . . 7
โข (๐ง = ๐ค โ (โ๐ โ ๐ด ๐ง = (sup(๐ต, โ, < ) ยท ๐) โ โ๐ โ ๐ด ๐ค = (sup(๐ต, โ, < ) ยท ๐))) |
40 | 37, 39 | elab 3634 |
. . . . . 6
โข (๐ค โ {๐ง โฃ โ๐ โ ๐ด ๐ง = (sup(๐ต, โ, < ) ยท ๐)} โ โ๐ โ ๐ด ๐ค = (sup(๐ต, โ, < ) ยท ๐)) |
41 | 7 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐ด) โ sup(๐ต, โ, < ) โ
โ) |
42 | 2 | simp1d 1143 |
. . . . . . . . . . 11
โข (๐ โ ๐ด โ โ) |
43 | 42 | sselda 3948 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐ด) โ ๐ โ โ) |
44 | | recn 11149 |
. . . . . . . . . . 11
โข (๐ โ โ โ ๐ โ
โ) |
45 | | mulcom 11145 |
. . . . . . . . . . 11
โข
((sup(๐ต, โ,
< ) โ โ โง ๐ โ โ) โ (sup(๐ต, โ, < ) ยท ๐) = (๐ ยท sup(๐ต, โ, < ))) |
46 | 9, 44, 45 | syl2an 597 |
. . . . . . . . . 10
โข
((sup(๐ต, โ,
< ) โ โ โง ๐ โ โ) โ (sup(๐ต, โ, < ) ยท ๐) = (๐ ยท sup(๐ต, โ, < ))) |
47 | 41, 43, 46 | syl2anc 585 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐ด) โ (sup(๐ต, โ, < ) ยท ๐) = (๐ ยท sup(๐ต, โ, < ))) |
48 | | breq2 5113 |
. . . . . . . . . . . . . 14
โข (๐ฅ = ๐ โ (0 โค ๐ฅ โ 0 โค ๐)) |
49 | 48 | rspccv 3580 |
. . . . . . . . . . . . 13
โข
(โ๐ฅ โ
๐ด 0 โค ๐ฅ โ (๐ โ ๐ด โ 0 โค ๐)) |
50 | 31, 49 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ (๐ โ ๐ด โ 0 โค ๐)) |
51 | 50 | imp 408 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐ด) โ 0 โค ๐) |
52 | 21 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐ด) โ โ๐ฅ โ ๐ต 0 โค ๐ฅ) |
53 | 5 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐ด) โ (๐ต โ โ โง ๐ต โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ต ๐ฆ โค ๐ฅ)) |
54 | | eqid 2733 |
. . . . . . . . . . . 12
โข {๐ง โฃ โ๐ โ ๐ต ๐ง = (๐ ยท ๐)} = {๐ง โฃ โ๐ โ ๐ต ๐ง = (๐ ยท ๐)} |
55 | | biid 261 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง 0 โค
๐ โง โ๐ฅ โ ๐ต 0 โค ๐ฅ) โง (๐ต โ โ โง ๐ต โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ต ๐ฆ โค ๐ฅ)) โ ((๐ โ โ โง 0 โค ๐ โง โ๐ฅ โ ๐ต 0 โค ๐ฅ) โง (๐ต โ โ โง ๐ต โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ต ๐ฆ โค ๐ฅ))) |
56 | 54, 55 | supmul1 12132 |
. . . . . . . . . . 11
โข (((๐ โ โ โง 0 โค
๐ โง โ๐ฅ โ ๐ต 0 โค ๐ฅ) โง (๐ต โ โ โง ๐ต โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ต ๐ฆ โค ๐ฅ)) โ (๐ ยท sup(๐ต, โ, < )) = sup({๐ง โฃ โ๐ โ ๐ต ๐ง = (๐ ยท ๐)}, โ, < )) |
57 | 43, 51, 52, 53, 56 | syl31anc 1374 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐ด) โ (๐ ยท sup(๐ต, โ, < )) = sup({๐ง โฃ โ๐ โ ๐ต ๐ง = (๐ ยท ๐)}, โ, < )) |
58 | | eqeq1 2737 |
. . . . . . . . . . . . . . 15
โข (๐ง = ๐ค โ (๐ง = (๐ ยท ๐) โ ๐ค = (๐ ยท ๐))) |
59 | 58 | rexbidv 3172 |
. . . . . . . . . . . . . 14
โข (๐ง = ๐ค โ (โ๐ โ ๐ต ๐ง = (๐ ยท ๐) โ โ๐ โ ๐ต ๐ค = (๐ ยท ๐))) |
60 | 37, 59 | elab 3634 |
. . . . . . . . . . . . 13
โข (๐ค โ {๐ง โฃ โ๐ โ ๐ต ๐ง = (๐ ยท ๐)} โ โ๐ โ ๐ต ๐ค = (๐ ยท ๐)) |
61 | | rspe 3231 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ ๐ด โง โ๐ โ ๐ต ๐ค = (๐ ยท ๐)) โ โ๐ โ ๐ด โ๐ โ ๐ต ๐ค = (๐ ยท ๐)) |
62 | | oveq1 7368 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ฃ = ๐ โ (๐ฃ ยท ๐) = (๐ ยท ๐)) |
63 | 62 | eqeq2d 2744 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ฃ = ๐ โ (๐ง = (๐ฃ ยท ๐) โ ๐ง = (๐ ยท ๐))) |
64 | 63 | rexbidv 3172 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฃ = ๐ โ (โ๐ โ ๐ต ๐ง = (๐ฃ ยท ๐) โ โ๐ โ ๐ต ๐ง = (๐ ยท ๐))) |
65 | 64 | cbvrexvw 3225 |
. . . . . . . . . . . . . . . . . 18
โข
(โ๐ฃ โ
๐ด โ๐ โ ๐ต ๐ง = (๐ฃ ยท ๐) โ โ๐ โ ๐ด โ๐ โ ๐ต ๐ง = (๐ ยท ๐)) |
66 | 58 | 2rexbidv 3210 |
. . . . . . . . . . . . . . . . . 18
โข (๐ง = ๐ค โ (โ๐ โ ๐ด โ๐ โ ๐ต ๐ง = (๐ ยท ๐) โ โ๐ โ ๐ด โ๐ โ ๐ต ๐ค = (๐ ยท ๐))) |
67 | 65, 66 | bitrid 283 |
. . . . . . . . . . . . . . . . 17
โข (๐ง = ๐ค โ (โ๐ฃ โ ๐ด โ๐ โ ๐ต ๐ง = (๐ฃ ยท ๐) โ โ๐ โ ๐ด โ๐ โ ๐ต ๐ค = (๐ ยท ๐))) |
68 | | supmul.1 |
. . . . . . . . . . . . . . . . 17
โข ๐ถ = {๐ง โฃ โ๐ฃ โ ๐ด โ๐ โ ๐ต ๐ง = (๐ฃ ยท ๐)} |
69 | 37, 67, 68 | elab2 3638 |
. . . . . . . . . . . . . . . 16
โข (๐ค โ ๐ถ โ โ๐ โ ๐ด โ๐ โ ๐ต ๐ค = (๐ ยท ๐)) |
70 | 61, 69 | sylibr 233 |
. . . . . . . . . . . . . . 15
โข ((๐ โ ๐ด โง โ๐ โ ๐ต ๐ค = (๐ ยท ๐)) โ ๐ค โ ๐ถ) |
71 | 70 | ex 414 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ด โ (โ๐ โ ๐ต ๐ค = (๐ ยท ๐) โ ๐ค โ ๐ถ)) |
72 | 68, 1 | supmullem2 12134 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐ถ โ โ โง ๐ถ โ โ
โง โ๐ฅ โ โ โ๐ค โ ๐ถ ๐ค โค ๐ฅ)) |
73 | | suprub 12124 |
. . . . . . . . . . . . . . . 16
โข (((๐ถ โ โ โง ๐ถ โ โ
โง โ๐ฅ โ โ โ๐ค โ ๐ถ ๐ค โค ๐ฅ) โง ๐ค โ ๐ถ) โ ๐ค โค sup(๐ถ, โ, < )) |
74 | 73 | ex 414 |
. . . . . . . . . . . . . . 15
โข ((๐ถ โ โ โง ๐ถ โ โ
โง โ๐ฅ โ โ โ๐ค โ ๐ถ ๐ค โค ๐ฅ) โ (๐ค โ ๐ถ โ ๐ค โค sup(๐ถ, โ, < ))) |
75 | 72, 74 | syl 17 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ค โ ๐ถ โ ๐ค โค sup(๐ถ, โ, < ))) |
76 | 71, 75 | sylan9r 510 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ ๐ด) โ (โ๐ โ ๐ต ๐ค = (๐ ยท ๐) โ ๐ค โค sup(๐ถ, โ, < ))) |
77 | 60, 76 | biimtrid 241 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ ๐ด) โ (๐ค โ {๐ง โฃ โ๐ โ ๐ต ๐ง = (๐ ยท ๐)} โ ๐ค โค sup(๐ถ, โ, < ))) |
78 | 77 | ralrimiv 3139 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐ด) โ โ๐ค โ {๐ง โฃ โ๐ โ ๐ต ๐ง = (๐ ยท ๐)}๐ค โค sup(๐ถ, โ, < )) |
79 | 43 | adantr 482 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ โ ๐ด) โง ๐ โ ๐ต) โ ๐ โ โ) |
80 | 18 | adantlr 714 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ โ ๐ด) โง ๐ โ ๐ต) โ ๐ โ โ) |
81 | 79, 80 | remulcld 11193 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ โ ๐ด) โง ๐ โ ๐ต) โ (๐ ยท ๐) โ โ) |
82 | | eleq1a 2829 |
. . . . . . . . . . . . . . 15
โข ((๐ ยท ๐) โ โ โ (๐ง = (๐ ยท ๐) โ ๐ง โ โ)) |
83 | 81, 82 | syl 17 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ ๐ด) โง ๐ โ ๐ต) โ (๐ง = (๐ ยท ๐) โ ๐ง โ โ)) |
84 | 83 | rexlimdva 3149 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ ๐ด) โ (โ๐ โ ๐ต ๐ง = (๐ ยท ๐) โ ๐ง โ โ)) |
85 | 84 | abssdv 4029 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ ๐ด) โ {๐ง โฃ โ๐ โ ๐ต ๐ง = (๐ ยท ๐)} โ โ) |
86 | | ovex 7394 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ ยท ๐) โ V |
87 | 86 | isseti 3462 |
. . . . . . . . . . . . . . . . . 18
โข
โ๐ค ๐ค = (๐ ยท ๐) |
88 | 87 | rgenw 3065 |
. . . . . . . . . . . . . . . . 17
โข
โ๐ โ
๐ต โ๐ค ๐ค = (๐ ยท ๐) |
89 | | r19.2z 4456 |
. . . . . . . . . . . . . . . . 17
โข ((๐ต โ โ
โง
โ๐ โ ๐ต โ๐ค ๐ค = (๐ ยท ๐)) โ โ๐ โ ๐ต โ๐ค ๐ค = (๐ ยท ๐)) |
90 | 13, 88, 89 | sylancl 587 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ๐ โ ๐ต โ๐ค ๐ค = (๐ ยท ๐)) |
91 | | rexcom4 3270 |
. . . . . . . . . . . . . . . 16
โข
(โ๐ โ
๐ต โ๐ค ๐ค = (๐ ยท ๐) โ โ๐คโ๐ โ ๐ต ๐ค = (๐ ยท ๐)) |
92 | 90, 91 | sylib 217 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ๐คโ๐ โ ๐ต ๐ค = (๐ ยท ๐)) |
93 | 59 | cbvexvw 2041 |
. . . . . . . . . . . . . . 15
โข
(โ๐งโ๐ โ ๐ต ๐ง = (๐ ยท ๐) โ โ๐คโ๐ โ ๐ต ๐ค = (๐ ยท ๐)) |
94 | 92, 93 | sylibr 233 |
. . . . . . . . . . . . . 14
โข (๐ โ โ๐งโ๐ โ ๐ต ๐ง = (๐ ยท ๐)) |
95 | | abn0 4344 |
. . . . . . . . . . . . . 14
โข ({๐ง โฃ โ๐ โ ๐ต ๐ง = (๐ ยท ๐)} โ โ
โ โ๐งโ๐ โ ๐ต ๐ง = (๐ ยท ๐)) |
96 | 94, 95 | sylibr 233 |
. . . . . . . . . . . . 13
โข (๐ โ {๐ง โฃ โ๐ โ ๐ต ๐ง = (๐ ยท ๐)} โ โ
) |
97 | 96 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ ๐ด) โ {๐ง โฃ โ๐ โ ๐ต ๐ง = (๐ ยท ๐)} โ โ
) |
98 | | suprcl 12123 |
. . . . . . . . . . . . . . 15
โข ((๐ถ โ โ โง ๐ถ โ โ
โง โ๐ฅ โ โ โ๐ค โ ๐ถ ๐ค โค ๐ฅ) โ sup(๐ถ, โ, < ) โ
โ) |
99 | 72, 98 | syl 17 |
. . . . . . . . . . . . . 14
โข (๐ โ sup(๐ถ, โ, < ) โ
โ) |
100 | 99 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ ๐ด) โ sup(๐ถ, โ, < ) โ
โ) |
101 | | brralrspcev 5169 |
. . . . . . . . . . . . 13
โข
((sup(๐ถ, โ,
< ) โ โ โง โ๐ค โ {๐ง โฃ โ๐ โ ๐ต ๐ง = (๐ ยท ๐)}๐ค โค sup(๐ถ, โ, < )) โ โ๐ฅ โ โ โ๐ค โ {๐ง โฃ โ๐ โ ๐ต ๐ง = (๐ ยท ๐)}๐ค โค ๐ฅ) |
102 | 100, 78, 101 | syl2anc 585 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ ๐ด) โ โ๐ฅ โ โ โ๐ค โ {๐ง โฃ โ๐ โ ๐ต ๐ง = (๐ ยท ๐)}๐ค โค ๐ฅ) |
103 | | suprleub 12129 |
. . . . . . . . . . . 12
โข ((({๐ง โฃ โ๐ โ ๐ต ๐ง = (๐ ยท ๐)} โ โ โง {๐ง โฃ โ๐ โ ๐ต ๐ง = (๐ ยท ๐)} โ โ
โง โ๐ฅ โ โ โ๐ค โ {๐ง โฃ โ๐ โ ๐ต ๐ง = (๐ ยท ๐)}๐ค โค ๐ฅ) โง sup(๐ถ, โ, < ) โ โ) โ
(sup({๐ง โฃ
โ๐ โ ๐ต ๐ง = (๐ ยท ๐)}, โ, < ) โค sup(๐ถ, โ, < ) โ
โ๐ค โ {๐ง โฃ โ๐ โ ๐ต ๐ง = (๐ ยท ๐)}๐ค โค sup(๐ถ, โ, < ))) |
104 | 85, 97, 102, 100, 103 | syl31anc 1374 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐ด) โ (sup({๐ง โฃ โ๐ โ ๐ต ๐ง = (๐ ยท ๐)}, โ, < ) โค sup(๐ถ, โ, < ) โ
โ๐ค โ {๐ง โฃ โ๐ โ ๐ต ๐ง = (๐ ยท ๐)}๐ค โค sup(๐ถ, โ, < ))) |
105 | 78, 104 | mpbird 257 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐ด) โ sup({๐ง โฃ โ๐ โ ๐ต ๐ง = (๐ ยท ๐)}, โ, < ) โค sup(๐ถ, โ, <
)) |
106 | 57, 105 | eqbrtrd 5131 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐ด) โ (๐ ยท sup(๐ต, โ, < )) โค sup(๐ถ, โ, <
)) |
107 | 47, 106 | eqbrtrd 5131 |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐ด) โ (sup(๐ต, โ, < ) ยท ๐) โค sup(๐ถ, โ, < )) |
108 | | breq1 5112 |
. . . . . . . 8
โข (๐ค = (sup(๐ต, โ, < ) ยท ๐) โ (๐ค โค sup(๐ถ, โ, < ) โ (sup(๐ต, โ, < ) ยท ๐) โค sup(๐ถ, โ, < ))) |
109 | 107, 108 | syl5ibrcom 247 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐ด) โ (๐ค = (sup(๐ต, โ, < ) ยท ๐) โ ๐ค โค sup(๐ถ, โ, < ))) |
110 | 109 | rexlimdva 3149 |
. . . . . 6
โข (๐ โ (โ๐ โ ๐ด ๐ค = (sup(๐ต, โ, < ) ยท ๐) โ ๐ค โค sup(๐ถ, โ, < ))) |
111 | 40, 110 | biimtrid 241 |
. . . . 5
โข (๐ โ (๐ค โ {๐ง โฃ โ๐ โ ๐ด ๐ง = (sup(๐ต, โ, < ) ยท ๐)} โ ๐ค โค sup(๐ถ, โ, < ))) |
112 | 111 | ralrimiv 3139 |
. . . 4
โข (๐ โ โ๐ค โ {๐ง โฃ โ๐ โ ๐ด ๐ง = (sup(๐ต, โ, < ) ยท ๐)}๐ค โค sup(๐ถ, โ, < )) |
113 | 41, 43 | remulcld 11193 |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐ด) โ (sup(๐ต, โ, < ) ยท ๐) โ
โ) |
114 | | eleq1a 2829 |
. . . . . . . 8
โข
((sup(๐ต, โ,
< ) ยท ๐) โ
โ โ (๐ง =
(sup(๐ต, โ, < )
ยท ๐) โ ๐ง โ
โ)) |
115 | 113, 114 | syl 17 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐ด) โ (๐ง = (sup(๐ต, โ, < ) ยท ๐) โ ๐ง โ โ)) |
116 | 115 | rexlimdva 3149 |
. . . . . 6
โข (๐ โ (โ๐ โ ๐ด ๐ง = (sup(๐ต, โ, < ) ยท ๐) โ ๐ง โ โ)) |
117 | 116 | abssdv 4029 |
. . . . 5
โข (๐ โ {๐ง โฃ โ๐ โ ๐ด ๐ง = (sup(๐ต, โ, < ) ยท ๐)} โ
โ) |
118 | 2 | simp2d 1144 |
. . . . . . . 8
โข (๐ โ ๐ด โ โ
) |
119 | | ovex 7394 |
. . . . . . . . . 10
โข
(sup(๐ต, โ,
< ) ยท ๐) โ
V |
120 | 119 | isseti 3462 |
. . . . . . . . 9
โข
โ๐ง ๐ง = (sup(๐ต, โ, < ) ยท ๐) |
121 | 120 | rgenw 3065 |
. . . . . . . 8
โข
โ๐ โ
๐ด โ๐ง ๐ง = (sup(๐ต, โ, < ) ยท ๐) |
122 | | r19.2z 4456 |
. . . . . . . 8
โข ((๐ด โ โ
โง
โ๐ โ ๐ด โ๐ง ๐ง = (sup(๐ต, โ, < ) ยท ๐)) โ โ๐ โ ๐ด โ๐ง ๐ง = (sup(๐ต, โ, < ) ยท ๐)) |
123 | 118, 121,
122 | sylancl 587 |
. . . . . . 7
โข (๐ โ โ๐ โ ๐ด โ๐ง ๐ง = (sup(๐ต, โ, < ) ยท ๐)) |
124 | | rexcom4 3270 |
. . . . . . 7
โข
(โ๐ โ
๐ด โ๐ง ๐ง = (sup(๐ต, โ, < ) ยท ๐) โ โ๐งโ๐ โ ๐ด ๐ง = (sup(๐ต, โ, < ) ยท ๐)) |
125 | 123, 124 | sylib 217 |
. . . . . 6
โข (๐ โ โ๐งโ๐ โ ๐ด ๐ง = (sup(๐ต, โ, < ) ยท ๐)) |
126 | | abn0 4344 |
. . . . . 6
โข ({๐ง โฃ โ๐ โ ๐ด ๐ง = (sup(๐ต, โ, < ) ยท ๐)} โ โ
โ
โ๐งโ๐ โ ๐ด ๐ง = (sup(๐ต, โ, < ) ยท ๐)) |
127 | 125, 126 | sylibr 233 |
. . . . 5
โข (๐ โ {๐ง โฃ โ๐ โ ๐ด ๐ง = (sup(๐ต, โ, < ) ยท ๐)} โ
โ
) |
128 | | brralrspcev 5169 |
. . . . . 6
โข
((sup(๐ถ, โ,
< ) โ โ โง โ๐ค โ {๐ง โฃ โ๐ โ ๐ด ๐ง = (sup(๐ต, โ, < ) ยท ๐)}๐ค โค sup(๐ถ, โ, < )) โ โ๐ฅ โ โ โ๐ค โ {๐ง โฃ โ๐ โ ๐ด ๐ง = (sup(๐ต, โ, < ) ยท ๐)}๐ค โค ๐ฅ) |
129 | 99, 112, 128 | syl2anc 585 |
. . . . 5
โข (๐ โ โ๐ฅ โ โ โ๐ค โ {๐ง โฃ โ๐ โ ๐ด ๐ง = (sup(๐ต, โ, < ) ยท ๐)}๐ค โค ๐ฅ) |
130 | | suprleub 12129 |
. . . . 5
โข ((({๐ง โฃ โ๐ โ ๐ด ๐ง = (sup(๐ต, โ, < ) ยท ๐)} โ โ โง {๐ง โฃ โ๐ โ ๐ด ๐ง = (sup(๐ต, โ, < ) ยท ๐)} โ โ
โง
โ๐ฅ โ โ
โ๐ค โ {๐ง โฃ โ๐ โ ๐ด ๐ง = (sup(๐ต, โ, < ) ยท ๐)}๐ค โค ๐ฅ) โง sup(๐ถ, โ, < ) โ โ) โ
(sup({๐ง โฃ
โ๐ โ ๐ด ๐ง = (sup(๐ต, โ, < ) ยท ๐)}, โ, < ) โค
sup(๐ถ, โ, < )
โ โ๐ค โ
{๐ง โฃ โ๐ โ ๐ด ๐ง = (sup(๐ต, โ, < ) ยท ๐)}๐ค โค sup(๐ถ, โ, < ))) |
131 | 117, 127,
129, 99, 130 | syl31anc 1374 |
. . . 4
โข (๐ โ (sup({๐ง โฃ โ๐ โ ๐ด ๐ง = (sup(๐ต, โ, < ) ยท ๐)}, โ, < ) โค
sup(๐ถ, โ, < )
โ โ๐ค โ
{๐ง โฃ โ๐ โ ๐ด ๐ง = (sup(๐ต, โ, < ) ยท ๐)}๐ค โค sup(๐ถ, โ, < ))) |
132 | 112, 131 | mpbird 257 |
. . 3
โข (๐ โ sup({๐ง โฃ โ๐ โ ๐ด ๐ง = (sup(๐ต, โ, < ) ยท ๐)}, โ, < ) โค
sup(๐ถ, โ, <
)) |
133 | 36, 132 | eqbrtrd 5131 |
. 2
โข (๐ โ (sup(๐ด, โ, < ) ยท sup(๐ต, โ, < )) โค
sup(๐ถ, โ, <
)) |
134 | 68, 1 | supmullem1 12133 |
. . 3
โข (๐ โ โ๐ค โ ๐ถ ๐ค โค (sup(๐ด, โ, < ) ยท sup(๐ต, โ, <
))) |
135 | 4, 7 | remulcld 11193 |
. . . 4
โข (๐ โ (sup(๐ด, โ, < ) ยท sup(๐ต, โ, < )) โ
โ) |
136 | | suprleub 12129 |
. . . 4
โข (((๐ถ โ โ โง ๐ถ โ โ
โง โ๐ฅ โ โ โ๐ค โ ๐ถ ๐ค โค ๐ฅ) โง (sup(๐ด, โ, < ) ยท sup(๐ต, โ, < )) โ
โ) โ (sup(๐ถ,
โ, < ) โค (sup(๐ด, โ, < ) ยท sup(๐ต, โ, < )) โ
โ๐ค โ ๐ถ ๐ค โค (sup(๐ด, โ, < ) ยท sup(๐ต, โ, <
)))) |
137 | 72, 135, 136 | syl2anc 585 |
. . 3
โข (๐ โ (sup(๐ถ, โ, < ) โค (sup(๐ด, โ, < ) ยท
sup(๐ต, โ, < ))
โ โ๐ค โ
๐ถ ๐ค โค (sup(๐ด, โ, < ) ยท sup(๐ต, โ, <
)))) |
138 | 134, 137 | mpbird 257 |
. 2
โข (๐ โ sup(๐ถ, โ, < ) โค (sup(๐ด, โ, < ) ยท
sup(๐ต, โ, <
))) |
139 | 135, 99 | letri3d 11305 |
. 2
โข (๐ โ ((sup(๐ด, โ, < ) ยท sup(๐ต, โ, < )) = sup(๐ถ, โ, < ) โ
((sup(๐ด, โ, < )
ยท sup(๐ต, โ,
< )) โค sup(๐ถ,
โ, < ) โง sup(๐ถ, โ, < ) โค (sup(๐ด, โ, < ) ยท
sup(๐ต, โ, <
))))) |
140 | 133, 138,
139 | mpbir2and 712 |
1
โข (๐ โ (sup(๐ด, โ, < ) ยท sup(๐ต, โ, < )) = sup(๐ถ, โ, <
)) |