Step | Hyp | Ref
| Expression |
1 | | vex 3451 |
. . . . . . . 8
โข ๐ค โ V |
2 | | oveq2 7369 |
. . . . . . . . . . 11
โข (๐ฃ = ๐ โ (๐ด ยท ๐ฃ) = (๐ด ยท ๐)) |
3 | 2 | eqeq2d 2744 |
. . . . . . . . . 10
โข (๐ฃ = ๐ โ (๐ง = (๐ด ยท ๐ฃ) โ ๐ง = (๐ด ยท ๐))) |
4 | 3 | cbvrexvw 3225 |
. . . . . . . . 9
โข
(โ๐ฃ โ
๐ต ๐ง = (๐ด ยท ๐ฃ) โ โ๐ โ ๐ต ๐ง = (๐ด ยท ๐)) |
5 | | eqeq1 2737 |
. . . . . . . . . 10
โข (๐ง = ๐ค โ (๐ง = (๐ด ยท ๐) โ ๐ค = (๐ด ยท ๐))) |
6 | 5 | rexbidv 3172 |
. . . . . . . . 9
โข (๐ง = ๐ค โ (โ๐ โ ๐ต ๐ง = (๐ด ยท ๐) โ โ๐ โ ๐ต ๐ค = (๐ด ยท ๐))) |
7 | 4, 6 | bitrid 283 |
. . . . . . . 8
โข (๐ง = ๐ค โ (โ๐ฃ โ ๐ต ๐ง = (๐ด ยท ๐ฃ) โ โ๐ โ ๐ต ๐ค = (๐ด ยท ๐))) |
8 | | supmul1.1 |
. . . . . . . 8
โข ๐ถ = {๐ง โฃ โ๐ฃ โ ๐ต ๐ง = (๐ด ยท ๐ฃ)} |
9 | 1, 7, 8 | elab2 3638 |
. . . . . . 7
โข (๐ค โ ๐ถ โ โ๐ โ ๐ต ๐ค = (๐ด ยท ๐)) |
10 | | supmul1.2 |
. . . . . . . . . . . . 13
โข (๐ โ ((๐ด โ โ โง 0 โค ๐ด โง โ๐ฅ โ ๐ต 0 โค ๐ฅ) โง (๐ต โ โ โง ๐ต โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ต ๐ฆ โค ๐ฅ))) |
11 | | simpr 486 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง 0 โค
๐ด โง โ๐ฅ โ ๐ต 0 โค ๐ฅ) โง (๐ต โ โ โง ๐ต โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ต ๐ฆ โค ๐ฅ)) โ (๐ต โ โ โง ๐ต โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ต ๐ฆ โค ๐ฅ)) |
12 | 10, 11 | sylbi 216 |
. . . . . . . . . . . 12
โข (๐ โ (๐ต โ โ โง ๐ต โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ต ๐ฆ โค ๐ฅ)) |
13 | 12 | simp1d 1143 |
. . . . . . . . . . 11
โข (๐ โ ๐ต โ โ) |
14 | 13 | sselda 3948 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐ต) โ ๐ โ โ) |
15 | | suprcl 12123 |
. . . . . . . . . . . 12
โข ((๐ต โ โ โง ๐ต โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ต ๐ฆ โค ๐ฅ) โ sup(๐ต, โ, < ) โ
โ) |
16 | 12, 15 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ sup(๐ต, โ, < ) โ
โ) |
17 | 16 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐ต) โ sup(๐ต, โ, < ) โ
โ) |
18 | | simpl1 1192 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง 0 โค
๐ด โง โ๐ฅ โ ๐ต 0 โค ๐ฅ) โง (๐ต โ โ โง ๐ต โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ต ๐ฆ โค ๐ฅ)) โ ๐ด โ โ) |
19 | 10, 18 | sylbi 216 |
. . . . . . . . . . . 12
โข (๐ โ ๐ด โ โ) |
20 | | simpl2 1193 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง 0 โค
๐ด โง โ๐ฅ โ ๐ต 0 โค ๐ฅ) โง (๐ต โ โ โง ๐ต โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ต ๐ฆ โค ๐ฅ)) โ 0 โค ๐ด) |
21 | 10, 20 | sylbi 216 |
. . . . . . . . . . . 12
โข (๐ โ 0 โค ๐ด) |
22 | 19, 21 | jca 513 |
. . . . . . . . . . 11
โข (๐ โ (๐ด โ โ โง 0 โค ๐ด)) |
23 | 22 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐ต) โ (๐ด โ โ โง 0 โค ๐ด)) |
24 | | suprub 12124 |
. . . . . . . . . . 11
โข (((๐ต โ โ โง ๐ต โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ต ๐ฆ โค ๐ฅ) โง ๐ โ ๐ต) โ ๐ โค sup(๐ต, โ, < )) |
25 | 12, 24 | sylan 581 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐ต) โ ๐ โค sup(๐ต, โ, < )) |
26 | | lemul2a 12018 |
. . . . . . . . . 10
โข (((๐ โ โ โง sup(๐ต, โ, < ) โ โ
โง (๐ด โ โ
โง 0 โค ๐ด)) โง
๐ โค sup(๐ต, โ, < )) โ (๐ด ยท ๐) โค (๐ด ยท sup(๐ต, โ, < ))) |
27 | 14, 17, 23, 25, 26 | syl31anc 1374 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐ต) โ (๐ด ยท ๐) โค (๐ด ยท sup(๐ต, โ, < ))) |
28 | | breq1 5112 |
. . . . . . . . 9
โข (๐ค = (๐ด ยท ๐) โ (๐ค โค (๐ด ยท sup(๐ต, โ, < )) โ (๐ด ยท ๐) โค (๐ด ยท sup(๐ต, โ, < )))) |
29 | 27, 28 | syl5ibrcom 247 |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐ต) โ (๐ค = (๐ด ยท ๐) โ ๐ค โค (๐ด ยท sup(๐ต, โ, < )))) |
30 | 29 | rexlimdva 3149 |
. . . . . . 7
โข (๐ โ (โ๐ โ ๐ต ๐ค = (๐ด ยท ๐) โ ๐ค โค (๐ด ยท sup(๐ต, โ, < )))) |
31 | 9, 30 | biimtrid 241 |
. . . . . 6
โข (๐ โ (๐ค โ ๐ถ โ ๐ค โค (๐ด ยท sup(๐ต, โ, < )))) |
32 | 31 | ralrimiv 3139 |
. . . . 5
โข (๐ โ โ๐ค โ ๐ถ ๐ค โค (๐ด ยท sup(๐ต, โ, < ))) |
33 | 19 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ ๐ต) โ ๐ด โ โ) |
34 | 33, 14 | remulcld 11193 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐ต) โ (๐ด ยท ๐) โ โ) |
35 | | eleq1a 2829 |
. . . . . . . . . . 11
โข ((๐ด ยท ๐) โ โ โ (๐ค = (๐ด ยท ๐) โ ๐ค โ โ)) |
36 | 34, 35 | syl 17 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐ต) โ (๐ค = (๐ด ยท ๐) โ ๐ค โ โ)) |
37 | 36 | rexlimdva 3149 |
. . . . . . . . 9
โข (๐ โ (โ๐ โ ๐ต ๐ค = (๐ด ยท ๐) โ ๐ค โ โ)) |
38 | 9, 37 | biimtrid 241 |
. . . . . . . 8
โข (๐ โ (๐ค โ ๐ถ โ ๐ค โ โ)) |
39 | 38 | ssrdv 3954 |
. . . . . . 7
โข (๐ โ ๐ถ โ โ) |
40 | | simpr2 1196 |
. . . . . . . . . 10
โข (((๐ด โ โ โง 0 โค
๐ด โง โ๐ฅ โ ๐ต 0 โค ๐ฅ) โง (๐ต โ โ โง ๐ต โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ต ๐ฆ โค ๐ฅ)) โ ๐ต โ โ
) |
41 | 10, 40 | sylbi 216 |
. . . . . . . . 9
โข (๐ โ ๐ต โ โ
) |
42 | | ovex 7394 |
. . . . . . . . . . 11
โข (๐ด ยท ๐) โ V |
43 | 42 | isseti 3462 |
. . . . . . . . . 10
โข
โ๐ค ๐ค = (๐ด ยท ๐) |
44 | 43 | rgenw 3065 |
. . . . . . . . 9
โข
โ๐ โ
๐ต โ๐ค ๐ค = (๐ด ยท ๐) |
45 | | r19.2z 4456 |
. . . . . . . . 9
โข ((๐ต โ โ
โง
โ๐ โ ๐ต โ๐ค ๐ค = (๐ด ยท ๐)) โ โ๐ โ ๐ต โ๐ค ๐ค = (๐ด ยท ๐)) |
46 | 41, 44, 45 | sylancl 587 |
. . . . . . . 8
โข (๐ โ โ๐ โ ๐ต โ๐ค ๐ค = (๐ด ยท ๐)) |
47 | 9 | exbii 1851 |
. . . . . . . . 9
โข
(โ๐ค ๐ค โ ๐ถ โ โ๐คโ๐ โ ๐ต ๐ค = (๐ด ยท ๐)) |
48 | | n0 4310 |
. . . . . . . . 9
โข (๐ถ โ โ
โ
โ๐ค ๐ค โ ๐ถ) |
49 | | rexcom4 3270 |
. . . . . . . . 9
โข
(โ๐ โ
๐ต โ๐ค ๐ค = (๐ด ยท ๐) โ โ๐คโ๐ โ ๐ต ๐ค = (๐ด ยท ๐)) |
50 | 47, 48, 49 | 3bitr4i 303 |
. . . . . . . 8
โข (๐ถ โ โ
โ
โ๐ โ ๐ต โ๐ค ๐ค = (๐ด ยท ๐)) |
51 | 46, 50 | sylibr 233 |
. . . . . . 7
โข (๐ โ ๐ถ โ โ
) |
52 | 19, 16 | remulcld 11193 |
. . . . . . . 8
โข (๐ โ (๐ด ยท sup(๐ต, โ, < )) โ
โ) |
53 | | brralrspcev 5169 |
. . . . . . . 8
โข (((๐ด ยท sup(๐ต, โ, < )) โ โ โง
โ๐ค โ ๐ถ ๐ค โค (๐ด ยท sup(๐ต, โ, < ))) โ โ๐ฅ โ โ โ๐ค โ ๐ถ ๐ค โค ๐ฅ) |
54 | 52, 32, 53 | syl2anc 585 |
. . . . . . 7
โข (๐ โ โ๐ฅ โ โ โ๐ค โ ๐ถ ๐ค โค ๐ฅ) |
55 | 39, 51, 54 | 3jca 1129 |
. . . . . 6
โข (๐ โ (๐ถ โ โ โง ๐ถ โ โ
โง โ๐ฅ โ โ โ๐ค โ ๐ถ ๐ค โค ๐ฅ)) |
56 | | suprleub 12129 |
. . . . . 6
โข (((๐ถ โ โ โง ๐ถ โ โ
โง โ๐ฅ โ โ โ๐ค โ ๐ถ ๐ค โค ๐ฅ) โง (๐ด ยท sup(๐ต, โ, < )) โ โ) โ
(sup(๐ถ, โ, < )
โค (๐ด ยท sup(๐ต, โ, < )) โ
โ๐ค โ ๐ถ ๐ค โค (๐ด ยท sup(๐ต, โ, < )))) |
57 | 55, 52, 56 | syl2anc 585 |
. . . . 5
โข (๐ โ (sup(๐ถ, โ, < ) โค (๐ด ยท sup(๐ต, โ, < )) โ โ๐ค โ ๐ถ ๐ค โค (๐ด ยท sup(๐ต, โ, < )))) |
58 | 32, 57 | mpbird 257 |
. . . 4
โข (๐ โ sup(๐ถ, โ, < ) โค (๐ด ยท sup(๐ต, โ, < ))) |
59 | | simpr 486 |
. . . . . . 7
โข ((๐ โง sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))) โ sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))) |
60 | | suprcl 12123 |
. . . . . . . . . 10
โข ((๐ถ โ โ โง ๐ถ โ โ
โง โ๐ฅ โ โ โ๐ค โ ๐ถ ๐ค โค ๐ฅ) โ sup(๐ถ, โ, < ) โ
โ) |
61 | 55, 60 | syl 17 |
. . . . . . . . 9
โข (๐ โ sup(๐ถ, โ, < ) โ
โ) |
62 | 61 | adantr 482 |
. . . . . . . 8
โข ((๐ โง sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))) โ sup(๐ถ, โ, < ) โ
โ) |
63 | 16 | adantr 482 |
. . . . . . . 8
โข ((๐ โง sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))) โ sup(๐ต, โ, < ) โ
โ) |
64 | 19 | adantr 482 |
. . . . . . . 8
โข ((๐ โง sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))) โ ๐ด โ โ) |
65 | | n0 4310 |
. . . . . . . . . . . 12
โข (๐ต โ โ
โ
โ๐ ๐ โ ๐ต) |
66 | | 0red 11166 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ ๐ต) โ 0 โ โ) |
67 | | simpl3 1194 |
. . . . . . . . . . . . . . . . 17
โข (((๐ด โ โ โง 0 โค
๐ด โง โ๐ฅ โ ๐ต 0 โค ๐ฅ) โง (๐ต โ โ โง ๐ต โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ต ๐ฆ โค ๐ฅ)) โ โ๐ฅ โ ๐ต 0 โค ๐ฅ) |
68 | 10, 67 | sylbi 216 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ๐ฅ โ ๐ต 0 โค ๐ฅ) |
69 | | breq2 5113 |
. . . . . . . . . . . . . . . . 17
โข (๐ฅ = ๐ โ (0 โค ๐ฅ โ 0 โค ๐)) |
70 | 69 | rspccva 3582 |
. . . . . . . . . . . . . . . 16
โข
((โ๐ฅ โ
๐ต 0 โค ๐ฅ โง ๐ โ ๐ต) โ 0 โค ๐) |
71 | 68, 70 | sylan 581 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ ๐ต) โ 0 โค ๐) |
72 | 66, 14, 17, 71, 25 | letrd 11320 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ ๐ต) โ 0 โค sup(๐ต, โ, < )) |
73 | 72 | ex 414 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ โ ๐ต โ 0 โค sup(๐ต, โ, < ))) |
74 | 73 | exlimdv 1937 |
. . . . . . . . . . . 12
โข (๐ โ (โ๐ ๐ โ ๐ต โ 0 โค sup(๐ต, โ, < ))) |
75 | 65, 74 | biimtrid 241 |
. . . . . . . . . . 11
โข (๐ โ (๐ต โ โ
โ 0 โค sup(๐ต, โ, <
))) |
76 | 41, 75 | mpd 15 |
. . . . . . . . . 10
โข (๐ โ 0 โค sup(๐ต, โ, <
)) |
77 | 76 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))) โ 0 โค sup(๐ต, โ, <
)) |
78 | | 0red 11166 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ค โ ๐ถ) โ 0 โ โ) |
79 | 38 | imp 408 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ค โ ๐ถ) โ ๐ค โ โ) |
80 | 61 | adantr 482 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ค โ ๐ถ) โ sup(๐ถ, โ, < ) โ
โ) |
81 | 21 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง ๐ โ ๐ต) โ 0 โค ๐ด) |
82 | 33, 14, 81, 71 | mulge0d 11740 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ๐ โ ๐ต) โ 0 โค (๐ด ยท ๐)) |
83 | | breq2 5113 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ค = (๐ด ยท ๐) โ (0 โค ๐ค โ 0 โค (๐ด ยท ๐))) |
84 | 82, 83 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ๐ โ ๐ต) โ (๐ค = (๐ด ยท ๐) โ 0 โค ๐ค)) |
85 | 84 | rexlimdva 3149 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (โ๐ โ ๐ต ๐ค = (๐ด ยท ๐) โ 0 โค ๐ค)) |
86 | 9, 85 | biimtrid 241 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (๐ค โ ๐ถ โ 0 โค ๐ค)) |
87 | 86 | imp 408 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ค โ ๐ถ) โ 0 โค ๐ค) |
88 | | suprub 12124 |
. . . . . . . . . . . . . . . . 17
โข (((๐ถ โ โ โง ๐ถ โ โ
โง โ๐ฅ โ โ โ๐ค โ ๐ถ ๐ค โค ๐ฅ) โง ๐ค โ ๐ถ) โ ๐ค โค sup(๐ถ, โ, < )) |
89 | 55, 88 | sylan 581 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ค โ ๐ถ) โ ๐ค โค sup(๐ถ, โ, < )) |
90 | 78, 79, 80, 87, 89 | letrd 11320 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ค โ ๐ถ) โ 0 โค sup(๐ถ, โ, < )) |
91 | 90 | ex 414 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ค โ ๐ถ โ 0 โค sup(๐ถ, โ, < ))) |
92 | 91 | exlimdv 1937 |
. . . . . . . . . . . . 13
โข (๐ โ (โ๐ค ๐ค โ ๐ถ โ 0 โค sup(๐ถ, โ, < ))) |
93 | 48, 92 | biimtrid 241 |
. . . . . . . . . . . 12
โข (๐ โ (๐ถ โ โ
โ 0 โค sup(๐ถ, โ, <
))) |
94 | 51, 93 | mpd 15 |
. . . . . . . . . . 11
โข (๐ โ 0 โค sup(๐ถ, โ, <
)) |
95 | 94 | anim1i 616 |
. . . . . . . . . 10
โข ((๐ โง sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))) โ (0 โค sup(๐ถ, โ, < ) โง
sup(๐ถ, โ, < ) <
(๐ด ยท sup(๐ต, โ, <
)))) |
96 | | 0red 11166 |
. . . . . . . . . . . 12
โข (๐ โ 0 โ
โ) |
97 | | lelttr 11253 |
. . . . . . . . . . . 12
โข ((0
โ โ โง sup(๐ถ,
โ, < ) โ โ โง (๐ด ยท sup(๐ต, โ, < )) โ โ) โ
((0 โค sup(๐ถ, โ,
< ) โง sup(๐ถ,
โ, < ) < (๐ด
ยท sup(๐ต, โ,
< ))) โ 0 < (๐ด
ยท sup(๐ต, โ,
< )))) |
98 | 96, 61, 52, 97 | syl3anc 1372 |
. . . . . . . . . . 11
โข (๐ โ ((0 โค sup(๐ถ, โ, < ) โง
sup(๐ถ, โ, < ) <
(๐ด ยท sup(๐ต, โ, < ))) โ 0
< (๐ด ยท sup(๐ต, โ, <
)))) |
99 | 98 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))) โ ((0 โค
sup(๐ถ, โ, < )
โง sup(๐ถ, โ, <
) < (๐ด ยท
sup(๐ต, โ, < )))
โ 0 < (๐ด ยท
sup(๐ต, โ, <
)))) |
100 | 95, 99 | mpd 15 |
. . . . . . . . 9
โข ((๐ โง sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))) โ 0 < (๐ด ยท sup(๐ต, โ, < ))) |
101 | | prodgt02 12011 |
. . . . . . . . 9
โข (((๐ด โ โ โง sup(๐ต, โ, < ) โ
โ) โง (0 โค sup(๐ต, โ, < ) โง 0 < (๐ด ยท sup(๐ต, โ, < )))) โ 0 < ๐ด) |
102 | 64, 63, 77, 100, 101 | syl22anc 838 |
. . . . . . . 8
โข ((๐ โง sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))) โ 0 < ๐ด) |
103 | | ltdivmul 12038 |
. . . . . . . 8
โข
((sup(๐ถ, โ,
< ) โ โ โง sup(๐ต, โ, < ) โ โ โง
(๐ด โ โ โง 0
< ๐ด)) โ ((sup(๐ถ, โ, < ) / ๐ด) < sup(๐ต, โ, < ) โ sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < )))) |
104 | 62, 63, 64, 102, 103 | syl112anc 1375 |
. . . . . . 7
โข ((๐ โง sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))) โ ((sup(๐ถ, โ, < ) / ๐ด) < sup(๐ต, โ, < ) โ sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < )))) |
105 | 59, 104 | mpbird 257 |
. . . . . 6
โข ((๐ โง sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))) โ (sup(๐ถ, โ, < ) / ๐ด) < sup(๐ต, โ, < )) |
106 | 12 | adantr 482 |
. . . . . . 7
โข ((๐ โง sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))) โ (๐ต โ โ โง ๐ต โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ต ๐ฆ โค ๐ฅ)) |
107 | 102 | gt0ne0d 11727 |
. . . . . . . 8
โข ((๐ โง sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))) โ ๐ด โ 0) |
108 | 62, 64, 107 | redivcld 11991 |
. . . . . . 7
โข ((๐ โง sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))) โ (sup(๐ถ, โ, < ) / ๐ด) โ
โ) |
109 | | suprlub 12127 |
. . . . . . 7
โข (((๐ต โ โ โง ๐ต โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ต ๐ฆ โค ๐ฅ) โง (sup(๐ถ, โ, < ) / ๐ด) โ โ) โ ((sup(๐ถ, โ, < ) / ๐ด) < sup(๐ต, โ, < ) โ โ๐ โ ๐ต (sup(๐ถ, โ, < ) / ๐ด) < ๐)) |
110 | 106, 108,
109 | syl2anc 585 |
. . . . . 6
โข ((๐ โง sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))) โ ((sup(๐ถ, โ, < ) / ๐ด) < sup(๐ต, โ, < ) โ โ๐ โ ๐ต (sup(๐ถ, โ, < ) / ๐ด) < ๐)) |
111 | 105, 110 | mpbid 231 |
. . . . 5
โข ((๐ โง sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))) โ โ๐ โ ๐ต (sup(๐ถ, โ, < ) / ๐ด) < ๐) |
112 | 34 | adantlr 714 |
. . . . . . . 8
โข (((๐ โง sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))) โง ๐ โ ๐ต) โ (๐ด ยท ๐) โ โ) |
113 | 61 | ad2antrr 725 |
. . . . . . . 8
โข (((๐ โง sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))) โง ๐ โ ๐ต) โ sup(๐ถ, โ, < ) โ
โ) |
114 | | rspe 3231 |
. . . . . . . . . . . . . . 15
โข ((๐ โ ๐ต โง ๐ค = (๐ด ยท ๐)) โ โ๐ โ ๐ต ๐ค = (๐ด ยท ๐)) |
115 | 114, 9 | sylibr 233 |
. . . . . . . . . . . . . 14
โข ((๐ โ ๐ต โง ๐ค = (๐ด ยท ๐)) โ ๐ค โ ๐ถ) |
116 | 115 | adantl 483 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ ๐ต โง ๐ค = (๐ด ยท ๐))) โ ๐ค โ ๐ถ) |
117 | | simplrr 777 |
. . . . . . . . . . . . . 14
โข (((๐ โง (๐ โ ๐ต โง ๐ค = (๐ด ยท ๐))) โง ๐ค โ ๐ถ) โ ๐ค = (๐ด ยท ๐)) |
118 | 89 | adantlr 714 |
. . . . . . . . . . . . . 14
โข (((๐ โง (๐ โ ๐ต โง ๐ค = (๐ด ยท ๐))) โง ๐ค โ ๐ถ) โ ๐ค โค sup(๐ถ, โ, < )) |
119 | 117, 118 | eqbrtrrd 5133 |
. . . . . . . . . . . . 13
โข (((๐ โง (๐ โ ๐ต โง ๐ค = (๐ด ยท ๐))) โง ๐ค โ ๐ถ) โ (๐ด ยท ๐) โค sup(๐ถ, โ, < )) |
120 | 116, 119 | mpdan 686 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ ๐ต โง ๐ค = (๐ด ยท ๐))) โ (๐ด ยท ๐) โค sup(๐ถ, โ, < )) |
121 | 120 | expr 458 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐ต) โ (๐ค = (๐ด ยท ๐) โ (๐ด ยท ๐) โค sup(๐ถ, โ, < ))) |
122 | 121 | exlimdv 1937 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐ต) โ (โ๐ค ๐ค = (๐ด ยท ๐) โ (๐ด ยท ๐) โค sup(๐ถ, โ, < ))) |
123 | 43, 122 | mpi 20 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐ต) โ (๐ด ยท ๐) โค sup(๐ถ, โ, < )) |
124 | 123 | adantlr 714 |
. . . . . . . 8
โข (((๐ โง sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))) โง ๐ โ ๐ต) โ (๐ด ยท ๐) โค sup(๐ถ, โ, < )) |
125 | 112, 113,
124 | lensymd 11314 |
. . . . . . 7
โข (((๐ โง sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))) โง ๐ โ ๐ต) โ ยฌ sup(๐ถ, โ, < ) < (๐ด ยท ๐)) |
126 | 14 | adantlr 714 |
. . . . . . . 8
โข (((๐ โง sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))) โง ๐ โ ๐ต) โ ๐ โ โ) |
127 | 19 | ad2antrr 725 |
. . . . . . . 8
โข (((๐ โง sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))) โง ๐ โ ๐ต) โ ๐ด โ โ) |
128 | 102 | adantr 482 |
. . . . . . . 8
โข (((๐ โง sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))) โง ๐ โ ๐ต) โ 0 < ๐ด) |
129 | | ltdivmul 12038 |
. . . . . . . 8
โข
((sup(๐ถ, โ,
< ) โ โ โง ๐ โ โ โง (๐ด โ โ โง 0 < ๐ด)) โ ((sup(๐ถ, โ, < ) / ๐ด) < ๐ โ sup(๐ถ, โ, < ) < (๐ด ยท ๐))) |
130 | 113, 126,
127, 128, 129 | syl112anc 1375 |
. . . . . . 7
โข (((๐ โง sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))) โง ๐ โ ๐ต) โ ((sup(๐ถ, โ, < ) / ๐ด) < ๐ โ sup(๐ถ, โ, < ) < (๐ด ยท ๐))) |
131 | 125, 130 | mtbird 325 |
. . . . . 6
โข (((๐ โง sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))) โง ๐ โ ๐ต) โ ยฌ (sup(๐ถ, โ, < ) / ๐ด) < ๐) |
132 | 131 | nrexdv 3143 |
. . . . 5
โข ((๐ โง sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))) โ ยฌ
โ๐ โ ๐ต (sup(๐ถ, โ, < ) / ๐ด) < ๐) |
133 | 111, 132 | pm2.65da 816 |
. . . 4
โข (๐ โ ยฌ sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))) |
134 | 58, 133 | jca 513 |
. . 3
โข (๐ โ (sup(๐ถ, โ, < ) โค (๐ด ยท sup(๐ต, โ, < )) โง ยฌ sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < )))) |
135 | 61, 52 | eqleltd 11307 |
. . 3
โข (๐ โ (sup(๐ถ, โ, < ) = (๐ด ยท sup(๐ต, โ, < )) โ (sup(๐ถ, โ, < ) โค (๐ด ยท sup(๐ต, โ, < )) โง ยฌ sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))))) |
136 | 134, 135 | mpbird 257 |
. 2
โข (๐ โ sup(๐ถ, โ, < ) = (๐ด ยท sup(๐ต, โ, < ))) |
137 | 136 | eqcomd 2739 |
1
โข (๐ โ (๐ด ยท sup(๐ต, โ, < )) = sup(๐ถ, โ, < )) |