Step | Hyp | Ref
| Expression |
1 | | vex 3451 |
. . . 4
โข ๐ค โ V |
2 | | oveq1 7368 |
. . . . . . . 8
โข (๐ฃ = ๐ โ (๐ฃ ยท ๐) = (๐ ยท ๐)) |
3 | 2 | eqeq2d 2744 |
. . . . . . 7
โข (๐ฃ = ๐ โ (๐ง = (๐ฃ ยท ๐) โ ๐ง = (๐ ยท ๐))) |
4 | 3 | rexbidv 3172 |
. . . . . 6
โข (๐ฃ = ๐ โ (โ๐ โ ๐ต ๐ง = (๐ฃ ยท ๐) โ โ๐ โ ๐ต ๐ง = (๐ ยท ๐))) |
5 | 4 | cbvrexvw 3225 |
. . . . 5
โข
(โ๐ฃ โ
๐ด โ๐ โ ๐ต ๐ง = (๐ฃ ยท ๐) โ โ๐ โ ๐ด โ๐ โ ๐ต ๐ง = (๐ ยท ๐)) |
6 | | eqeq1 2737 |
. . . . . 6
โข (๐ง = ๐ค โ (๐ง = (๐ ยท ๐) โ ๐ค = (๐ ยท ๐))) |
7 | 6 | 2rexbidv 3210 |
. . . . 5
โข (๐ง = ๐ค โ (โ๐ โ ๐ด โ๐ โ ๐ต ๐ง = (๐ ยท ๐) โ โ๐ โ ๐ด โ๐ โ ๐ต ๐ค = (๐ ยท ๐))) |
8 | 5, 7 | bitrid 283 |
. . . 4
โข (๐ง = ๐ค โ (โ๐ฃ โ ๐ด โ๐ โ ๐ต ๐ง = (๐ฃ ยท ๐) โ โ๐ โ ๐ด โ๐ โ ๐ต ๐ค = (๐ ยท ๐))) |
9 | | supmul.1 |
. . . 4
โข ๐ถ = {๐ง โฃ โ๐ฃ โ ๐ด โ๐ โ ๐ต ๐ง = (๐ฃ ยท ๐)} |
10 | 1, 8, 9 | elab2 3638 |
. . 3
โข (๐ค โ ๐ถ โ โ๐ โ ๐ด โ๐ โ ๐ต ๐ค = (๐ ยท ๐)) |
11 | | supmul.2 |
. . . . . . . . . . 11
โข (๐ โ ((โ๐ฅ โ ๐ด 0 โค ๐ฅ โง โ๐ฅ โ ๐ต 0 โค ๐ฅ) โง (๐ด โ โ โง ๐ด โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ) โง (๐ต โ โ โง ๐ต โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ต ๐ฆ โค ๐ฅ))) |
12 | 11 | simp2bi 1147 |
. . . . . . . . . 10
โข (๐ โ (๐ด โ โ โง ๐ด โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ)) |
13 | 12 | simp1d 1143 |
. . . . . . . . 9
โข (๐ โ ๐ด โ โ) |
14 | 13 | sselda 3948 |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐ด) โ ๐ โ โ) |
15 | 14 | adantrr 716 |
. . . . . . 7
โข ((๐ โง (๐ โ ๐ด โง ๐ โ ๐ต)) โ ๐ โ โ) |
16 | | suprcl 12123 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ด โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ) โ sup(๐ด, โ, < ) โ
โ) |
17 | 12, 16 | syl 17 |
. . . . . . . 8
โข (๐ โ sup(๐ด, โ, < ) โ
โ) |
18 | 17 | adantr 482 |
. . . . . . 7
โข ((๐ โง (๐ โ ๐ด โง ๐ โ ๐ต)) โ sup(๐ด, โ, < ) โ
โ) |
19 | 11 | simp3bi 1148 |
. . . . . . . . . 10
โข (๐ โ (๐ต โ โ โง ๐ต โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ต ๐ฆ โค ๐ฅ)) |
20 | 19 | simp1d 1143 |
. . . . . . . . 9
โข (๐ โ ๐ต โ โ) |
21 | 20 | sselda 3948 |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐ต) โ ๐ โ โ) |
22 | 21 | adantrl 715 |
. . . . . . 7
โข ((๐ โง (๐ โ ๐ด โง ๐ โ ๐ต)) โ ๐ โ โ) |
23 | | suprcl 12123 |
. . . . . . . . 9
โข ((๐ต โ โ โง ๐ต โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ต ๐ฆ โค ๐ฅ) โ sup(๐ต, โ, < ) โ
โ) |
24 | 19, 23 | syl 17 |
. . . . . . . 8
โข (๐ โ sup(๐ต, โ, < ) โ
โ) |
25 | 24 | adantr 482 |
. . . . . . 7
โข ((๐ โง (๐ โ ๐ด โง ๐ โ ๐ต)) โ sup(๐ต, โ, < ) โ
โ) |
26 | | simp1l 1198 |
. . . . . . . . . . 11
โข
(((โ๐ฅ โ
๐ด 0 โค ๐ฅ โง โ๐ฅ โ ๐ต 0 โค ๐ฅ) โง (๐ด โ โ โง ๐ด โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ) โง (๐ต โ โ โง ๐ต โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ต ๐ฆ โค ๐ฅ)) โ โ๐ฅ โ ๐ด 0 โค ๐ฅ) |
27 | 11, 26 | sylbi 216 |
. . . . . . . . . 10
โข (๐ โ โ๐ฅ โ ๐ด 0 โค ๐ฅ) |
28 | | breq2 5113 |
. . . . . . . . . . 11
โข (๐ฅ = ๐ โ (0 โค ๐ฅ โ 0 โค ๐)) |
29 | 28 | rspccv 3580 |
. . . . . . . . . 10
โข
(โ๐ฅ โ
๐ด 0 โค ๐ฅ โ (๐ โ ๐ด โ 0 โค ๐)) |
30 | 27, 29 | syl 17 |
. . . . . . . . 9
โข (๐ โ (๐ โ ๐ด โ 0 โค ๐)) |
31 | 30 | imp 408 |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐ด) โ 0 โค ๐) |
32 | 31 | adantrr 716 |
. . . . . . 7
โข ((๐ โง (๐ โ ๐ด โง ๐ โ ๐ต)) โ 0 โค ๐) |
33 | | simp1r 1199 |
. . . . . . . . . . 11
โข
(((โ๐ฅ โ
๐ด 0 โค ๐ฅ โง โ๐ฅ โ ๐ต 0 โค ๐ฅ) โง (๐ด โ โ โง ๐ด โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ) โง (๐ต โ โ โง ๐ต โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ต ๐ฆ โค ๐ฅ)) โ โ๐ฅ โ ๐ต 0 โค ๐ฅ) |
34 | 11, 33 | sylbi 216 |
. . . . . . . . . 10
โข (๐ โ โ๐ฅ โ ๐ต 0 โค ๐ฅ) |
35 | | breq2 5113 |
. . . . . . . . . . 11
โข (๐ฅ = ๐ โ (0 โค ๐ฅ โ 0 โค ๐)) |
36 | 35 | rspccv 3580 |
. . . . . . . . . 10
โข
(โ๐ฅ โ
๐ต 0 โค ๐ฅ โ (๐ โ ๐ต โ 0 โค ๐)) |
37 | 34, 36 | syl 17 |
. . . . . . . . 9
โข (๐ โ (๐ โ ๐ต โ 0 โค ๐)) |
38 | 37 | imp 408 |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐ต) โ 0 โค ๐) |
39 | 38 | adantrl 715 |
. . . . . . 7
โข ((๐ โง (๐ โ ๐ด โง ๐ โ ๐ต)) โ 0 โค ๐) |
40 | | suprub 12124 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ด โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ) โง ๐ โ ๐ด) โ ๐ โค sup(๐ด, โ, < )) |
41 | 12, 40 | sylan 581 |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐ด) โ ๐ โค sup(๐ด, โ, < )) |
42 | 41 | adantrr 716 |
. . . . . . 7
โข ((๐ โง (๐ โ ๐ด โง ๐ โ ๐ต)) โ ๐ โค sup(๐ด, โ, < )) |
43 | | suprub 12124 |
. . . . . . . . 9
โข (((๐ต โ โ โง ๐ต โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ต ๐ฆ โค ๐ฅ) โง ๐ โ ๐ต) โ ๐ โค sup(๐ต, โ, < )) |
44 | 19, 43 | sylan 581 |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐ต) โ ๐ โค sup(๐ต, โ, < )) |
45 | 44 | adantrl 715 |
. . . . . . 7
โข ((๐ โง (๐ โ ๐ด โง ๐ โ ๐ต)) โ ๐ โค sup(๐ต, โ, < )) |
46 | 15, 18, 22, 25, 32, 39, 42, 45 | lemul12ad 12105 |
. . . . . 6
โข ((๐ โง (๐ โ ๐ด โง ๐ โ ๐ต)) โ (๐ ยท ๐) โค (sup(๐ด, โ, < ) ยท sup(๐ต, โ, <
))) |
47 | 46 | ex 414 |
. . . . 5
โข (๐ โ ((๐ โ ๐ด โง ๐ โ ๐ต) โ (๐ ยท ๐) โค (sup(๐ด, โ, < ) ยท sup(๐ต, โ, <
)))) |
48 | | breq1 5112 |
. . . . . 6
โข (๐ค = (๐ ยท ๐) โ (๐ค โค (sup(๐ด, โ, < ) ยท sup(๐ต, โ, < )) โ (๐ ยท ๐) โค (sup(๐ด, โ, < ) ยท sup(๐ต, โ, <
)))) |
49 | 48 | biimprcd 250 |
. . . . 5
โข ((๐ ยท ๐) โค (sup(๐ด, โ, < ) ยท sup(๐ต, โ, < )) โ (๐ค = (๐ ยท ๐) โ ๐ค โค (sup(๐ด, โ, < ) ยท sup(๐ต, โ, <
)))) |
50 | 47, 49 | syl6 35 |
. . . 4
โข (๐ โ ((๐ โ ๐ด โง ๐ โ ๐ต) โ (๐ค = (๐ ยท ๐) โ ๐ค โค (sup(๐ด, โ, < ) ยท sup(๐ต, โ, <
))))) |
51 | 50 | rexlimdvv 3201 |
. . 3
โข (๐ โ (โ๐ โ ๐ด โ๐ โ ๐ต ๐ค = (๐ ยท ๐) โ ๐ค โค (sup(๐ด, โ, < ) ยท sup(๐ต, โ, <
)))) |
52 | 10, 51 | biimtrid 241 |
. 2
โข (๐ โ (๐ค โ ๐ถ โ ๐ค โค (sup(๐ด, โ, < ) ยท sup(๐ต, โ, <
)))) |
53 | 52 | ralrimiv 3139 |
1
โข (๐ โ โ๐ค โ ๐ถ ๐ค โค (sup(๐ด, โ, < ) ยท sup(๐ต, โ, <
))) |