Step | Hyp | Ref
| Expression |
1 | | vex 3451 |
. . . . 5
โข ๐ค โ V |
2 | | oveq1 7368 |
. . . . . . . . 9
โข (๐ฃ = ๐ โ (๐ฃ ยท ๐) = (๐ ยท ๐)) |
3 | 2 | eqeq2d 2744 |
. . . . . . . 8
โข (๐ฃ = ๐ โ (๐ง = (๐ฃ ยท ๐) โ ๐ง = (๐ ยท ๐))) |
4 | 3 | rexbidv 3172 |
. . . . . . 7
โข (๐ฃ = ๐ โ (โ๐ โ ๐ต ๐ง = (๐ฃ ยท ๐) โ โ๐ โ ๐ต ๐ง = (๐ ยท ๐))) |
5 | 4 | cbvrexvw 3225 |
. . . . . 6
โข
(โ๐ฃ โ
๐ด โ๐ โ ๐ต ๐ง = (๐ฃ ยท ๐) โ โ๐ โ ๐ด โ๐ โ ๐ต ๐ง = (๐ ยท ๐)) |
6 | | eqeq1 2737 |
. . . . . . 7
โข (๐ง = ๐ค โ (๐ง = (๐ ยท ๐) โ ๐ค = (๐ ยท ๐))) |
7 | 6 | 2rexbidv 3210 |
. . . . . 6
โข (๐ง = ๐ค โ (โ๐ โ ๐ด โ๐ โ ๐ต ๐ง = (๐ ยท ๐) โ โ๐ โ ๐ด โ๐ โ ๐ต ๐ค = (๐ ยท ๐))) |
8 | 5, 7 | bitrid 283 |
. . . . 5
โข (๐ง = ๐ค โ (โ๐ฃ โ ๐ด โ๐ โ ๐ต ๐ง = (๐ฃ ยท ๐) โ โ๐ โ ๐ด โ๐ โ ๐ต ๐ค = (๐ ยท ๐))) |
9 | | supmul.1 |
. . . . 5
โข ๐ถ = {๐ง โฃ โ๐ฃ โ ๐ด โ๐ โ ๐ต ๐ง = (๐ฃ ยท ๐)} |
10 | 1, 8, 9 | elab2 3638 |
. . . 4
โข (๐ค โ ๐ถ โ โ๐ โ ๐ด โ๐ โ ๐ต ๐ค = (๐ ยท ๐)) |
11 | | supmul.2 |
. . . . . . . . . . 11
โข (๐ โ ((โ๐ฅ โ ๐ด 0 โค ๐ฅ โง โ๐ฅ โ ๐ต 0 โค ๐ฅ) โง (๐ด โ โ โง ๐ด โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ) โง (๐ต โ โ โง ๐ต โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ต ๐ฆ โค ๐ฅ))) |
12 | 11 | simp2bi 1147 |
. . . . . . . . . 10
โข (๐ โ (๐ด โ โ โง ๐ด โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ)) |
13 | 12 | simp1d 1143 |
. . . . . . . . 9
โข (๐ โ ๐ด โ โ) |
14 | 13 | sseld 3947 |
. . . . . . . 8
โข (๐ โ (๐ โ ๐ด โ ๐ โ โ)) |
15 | 11 | simp3bi 1148 |
. . . . . . . . . 10
โข (๐ โ (๐ต โ โ โง ๐ต โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ต ๐ฆ โค ๐ฅ)) |
16 | 15 | simp1d 1143 |
. . . . . . . . 9
โข (๐ โ ๐ต โ โ) |
17 | 16 | sseld 3947 |
. . . . . . . 8
โข (๐ โ (๐ โ ๐ต โ ๐ โ โ)) |
18 | 14, 17 | anim12d 610 |
. . . . . . 7
โข (๐ โ ((๐ โ ๐ด โง ๐ โ ๐ต) โ (๐ โ โ โง ๐ โ โ))) |
19 | | remulcl 11144 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ โ) โ (๐ ยท ๐) โ โ) |
20 | 18, 19 | syl6 35 |
. . . . . 6
โข (๐ โ ((๐ โ ๐ด โง ๐ โ ๐ต) โ (๐ ยท ๐) โ โ)) |
21 | | eleq1a 2829 |
. . . . . 6
โข ((๐ ยท ๐) โ โ โ (๐ค = (๐ ยท ๐) โ ๐ค โ โ)) |
22 | 20, 21 | syl6 35 |
. . . . 5
โข (๐ โ ((๐ โ ๐ด โง ๐ โ ๐ต) โ (๐ค = (๐ ยท ๐) โ ๐ค โ โ))) |
23 | 22 | rexlimdvv 3201 |
. . . 4
โข (๐ โ (โ๐ โ ๐ด โ๐ โ ๐ต ๐ค = (๐ ยท ๐) โ ๐ค โ โ)) |
24 | 10, 23 | biimtrid 241 |
. . 3
โข (๐ โ (๐ค โ ๐ถ โ ๐ค โ โ)) |
25 | 24 | ssrdv 3954 |
. 2
โข (๐ โ ๐ถ โ โ) |
26 | 12 | simp2d 1144 |
. . . . 5
โข (๐ โ ๐ด โ โ
) |
27 | 15 | simp2d 1144 |
. . . . . . . 8
โข (๐ โ ๐ต โ โ
) |
28 | | ovex 7394 |
. . . . . . . . . 10
โข (๐ ยท ๐) โ V |
29 | 28 | isseti 3462 |
. . . . . . . . 9
โข
โ๐ค ๐ค = (๐ ยท ๐) |
30 | 29 | rgenw 3065 |
. . . . . . . 8
โข
โ๐ โ
๐ต โ๐ค ๐ค = (๐ ยท ๐) |
31 | | r19.2z 4456 |
. . . . . . . 8
โข ((๐ต โ โ
โง
โ๐ โ ๐ต โ๐ค ๐ค = (๐ ยท ๐)) โ โ๐ โ ๐ต โ๐ค ๐ค = (๐ ยท ๐)) |
32 | 27, 30, 31 | sylancl 587 |
. . . . . . 7
โข (๐ โ โ๐ โ ๐ต โ๐ค ๐ค = (๐ ยท ๐)) |
33 | | rexcom4 3270 |
. . . . . . 7
โข
(โ๐ โ
๐ต โ๐ค ๐ค = (๐ ยท ๐) โ โ๐คโ๐ โ ๐ต ๐ค = (๐ ยท ๐)) |
34 | 32, 33 | sylib 217 |
. . . . . 6
โข (๐ โ โ๐คโ๐ โ ๐ต ๐ค = (๐ ยท ๐)) |
35 | 34 | ralrimivw 3144 |
. . . . 5
โข (๐ โ โ๐ โ ๐ด โ๐คโ๐ โ ๐ต ๐ค = (๐ ยท ๐)) |
36 | | r19.2z 4456 |
. . . . 5
โข ((๐ด โ โ
โง
โ๐ โ ๐ด โ๐คโ๐ โ ๐ต ๐ค = (๐ ยท ๐)) โ โ๐ โ ๐ด โ๐คโ๐ โ ๐ต ๐ค = (๐ ยท ๐)) |
37 | 26, 35, 36 | syl2anc 585 |
. . . 4
โข (๐ โ โ๐ โ ๐ด โ๐คโ๐ โ ๐ต ๐ค = (๐ ยท ๐)) |
38 | | rexcom4 3270 |
. . . 4
โข
(โ๐ โ
๐ด โ๐คโ๐ โ ๐ต ๐ค = (๐ ยท ๐) โ โ๐คโ๐ โ ๐ด โ๐ โ ๐ต ๐ค = (๐ ยท ๐)) |
39 | 37, 38 | sylib 217 |
. . 3
โข (๐ โ โ๐คโ๐ โ ๐ด โ๐ โ ๐ต ๐ค = (๐ ยท ๐)) |
40 | | n0 4310 |
. . . 4
โข (๐ถ โ โ
โ
โ๐ค ๐ค โ ๐ถ) |
41 | 10 | exbii 1851 |
. . . 4
โข
(โ๐ค ๐ค โ ๐ถ โ โ๐คโ๐ โ ๐ด โ๐ โ ๐ต ๐ค = (๐ ยท ๐)) |
42 | 40, 41 | bitri 275 |
. . 3
โข (๐ถ โ โ
โ
โ๐คโ๐ โ ๐ด โ๐ โ ๐ต ๐ค = (๐ ยท ๐)) |
43 | 39, 42 | sylibr 233 |
. 2
โข (๐ โ ๐ถ โ โ
) |
44 | | suprcl 12123 |
. . . . 5
โข ((๐ด โ โ โง ๐ด โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ) โ sup(๐ด, โ, < ) โ
โ) |
45 | 12, 44 | syl 17 |
. . . 4
โข (๐ โ sup(๐ด, โ, < ) โ
โ) |
46 | | suprcl 12123 |
. . . . 5
โข ((๐ต โ โ โง ๐ต โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ต ๐ฆ โค ๐ฅ) โ sup(๐ต, โ, < ) โ
โ) |
47 | 15, 46 | syl 17 |
. . . 4
โข (๐ โ sup(๐ต, โ, < ) โ
โ) |
48 | 45, 47 | remulcld 11193 |
. . 3
โข (๐ โ (sup(๐ด, โ, < ) ยท sup(๐ต, โ, < )) โ
โ) |
49 | 9, 11 | supmullem1 12133 |
. . 3
โข (๐ โ โ๐ค โ ๐ถ ๐ค โค (sup(๐ด, โ, < ) ยท sup(๐ต, โ, <
))) |
50 | | brralrspcev 5169 |
. . 3
โข
(((sup(๐ด, โ,
< ) ยท sup(๐ต,
โ, < )) โ โ โง โ๐ค โ ๐ถ ๐ค โค (sup(๐ด, โ, < ) ยท sup(๐ต, โ, < ))) โ
โ๐ฅ โ โ
โ๐ค โ ๐ถ ๐ค โค ๐ฅ) |
51 | 48, 49, 50 | syl2anc 585 |
. 2
โข (๐ โ โ๐ฅ โ โ โ๐ค โ ๐ถ ๐ค โค ๐ฅ) |
52 | 25, 43, 51 | 3jca 1129 |
1
โข (๐ โ (๐ถ โ โ โง ๐ถ โ โ
โง โ๐ฅ โ โ โ๐ค โ ๐ถ ๐ค โค ๐ฅ)) |