Step | Hyp | Ref
| Expression |
1 | | vex 3478 |
. . . . . . . 8
โข ๐ค โ V |
2 | | oveq2 7416 |
. . . . . . . . . . 11
โข (๐ฃ = ๐ โ (๐ด ยท ๐ฃ) = (๐ด ยท ๐)) |
3 | 2 | eqeq2d 2743 |
. . . . . . . . . 10
โข (๐ฃ = ๐ โ (๐ง = (๐ด ยท ๐ฃ) โ ๐ง = (๐ด ยท ๐))) |
4 | 3 | cbvrexvw 3235 |
. . . . . . . . 9
โข
(โ๐ฃ โ
๐ต ๐ง = (๐ด ยท ๐ฃ) โ โ๐ โ ๐ต ๐ง = (๐ด ยท ๐)) |
5 | | eqeq1 2736 |
. . . . . . . . . 10
โข (๐ง = ๐ค โ (๐ง = (๐ด ยท ๐) โ ๐ค = (๐ด ยท ๐))) |
6 | 5 | rexbidv 3178 |
. . . . . . . . 9
โข (๐ง = ๐ค โ (โ๐ โ ๐ต ๐ง = (๐ด ยท ๐) โ โ๐ โ ๐ต ๐ค = (๐ด ยท ๐))) |
7 | 4, 6 | bitrid 282 |
. . . . . . . 8
โข (๐ง = ๐ค โ (โ๐ฃ โ ๐ต ๐ง = (๐ด ยท ๐ฃ) โ โ๐ โ ๐ต ๐ค = (๐ด ยท ๐))) |
8 | | supmul1.1 |
. . . . . . . 8
โข ๐ถ = {๐ง โฃ โ๐ฃ โ ๐ต ๐ง = (๐ด ยท ๐ฃ)} |
9 | 1, 7, 8 | elab2 3672 |
. . . . . . 7
โข (๐ค โ ๐ถ โ โ๐ โ ๐ต ๐ค = (๐ด ยท ๐)) |
10 | | supmul1.2 |
. . . . . . . . . . . . 13
โข (๐ โ ((๐ด โ โ โง 0 โค ๐ด โง โ๐ฅ โ ๐ต 0 โค ๐ฅ) โง (๐ต โ โ โง ๐ต โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ต ๐ฆ โค ๐ฅ))) |
11 | | simpr 485 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง 0 โค
๐ด โง โ๐ฅ โ ๐ต 0 โค ๐ฅ) โง (๐ต โ โ โง ๐ต โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ต ๐ฆ โค ๐ฅ)) โ (๐ต โ โ โง ๐ต โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ต ๐ฆ โค ๐ฅ)) |
12 | 10, 11 | sylbi 216 |
. . . . . . . . . . . 12
โข (๐ โ (๐ต โ โ โง ๐ต โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ต ๐ฆ โค ๐ฅ)) |
13 | 12 | simp1d 1142 |
. . . . . . . . . . 11
โข (๐ โ ๐ต โ โ) |
14 | 13 | sselda 3982 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐ต) โ ๐ โ โ) |
15 | | suprcl 12173 |
. . . . . . . . . . . 12
โข ((๐ต โ โ โง ๐ต โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ต ๐ฆ โค ๐ฅ) โ sup(๐ต, โ, < ) โ
โ) |
16 | 12, 15 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ sup(๐ต, โ, < ) โ
โ) |
17 | 16 | adantr 481 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐ต) โ sup(๐ต, โ, < ) โ
โ) |
18 | | simpl1 1191 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง 0 โค
๐ด โง โ๐ฅ โ ๐ต 0 โค ๐ฅ) โง (๐ต โ โ โง ๐ต โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ต ๐ฆ โค ๐ฅ)) โ ๐ด โ โ) |
19 | 10, 18 | sylbi 216 |
. . . . . . . . . . . 12
โข (๐ โ ๐ด โ โ) |
20 | | simpl2 1192 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง 0 โค
๐ด โง โ๐ฅ โ ๐ต 0 โค ๐ฅ) โง (๐ต โ โ โง ๐ต โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ต ๐ฆ โค ๐ฅ)) โ 0 โค ๐ด) |
21 | 10, 20 | sylbi 216 |
. . . . . . . . . . . 12
โข (๐ โ 0 โค ๐ด) |
22 | 19, 21 | jca 512 |
. . . . . . . . . . 11
โข (๐ โ (๐ด โ โ โง 0 โค ๐ด)) |
23 | 22 | adantr 481 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐ต) โ (๐ด โ โ โง 0 โค ๐ด)) |
24 | | suprub 12174 |
. . . . . . . . . . 11
โข (((๐ต โ โ โง ๐ต โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ต ๐ฆ โค ๐ฅ) โง ๐ โ ๐ต) โ ๐ โค sup(๐ต, โ, < )) |
25 | 12, 24 | sylan 580 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐ต) โ ๐ โค sup(๐ต, โ, < )) |
26 | | lemul2a 12068 |
. . . . . . . . . 10
โข (((๐ โ โ โง sup(๐ต, โ, < ) โ โ
โง (๐ด โ โ
โง 0 โค ๐ด)) โง
๐ โค sup(๐ต, โ, < )) โ (๐ด ยท ๐) โค (๐ด ยท sup(๐ต, โ, < ))) |
27 | 14, 17, 23, 25, 26 | syl31anc 1373 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐ต) โ (๐ด ยท ๐) โค (๐ด ยท sup(๐ต, โ, < ))) |
28 | | breq1 5151 |
. . . . . . . . 9
โข (๐ค = (๐ด ยท ๐) โ (๐ค โค (๐ด ยท sup(๐ต, โ, < )) โ (๐ด ยท ๐) โค (๐ด ยท sup(๐ต, โ, < )))) |
29 | 27, 28 | syl5ibrcom 246 |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐ต) โ (๐ค = (๐ด ยท ๐) โ ๐ค โค (๐ด ยท sup(๐ต, โ, < )))) |
30 | 29 | rexlimdva 3155 |
. . . . . . 7
โข (๐ โ (โ๐ โ ๐ต ๐ค = (๐ด ยท ๐) โ ๐ค โค (๐ด ยท sup(๐ต, โ, < )))) |
31 | 9, 30 | biimtrid 241 |
. . . . . 6
โข (๐ โ (๐ค โ ๐ถ โ ๐ค โค (๐ด ยท sup(๐ต, โ, < )))) |
32 | 31 | ralrimiv 3145 |
. . . . 5
โข (๐ โ โ๐ค โ ๐ถ ๐ค โค (๐ด ยท sup(๐ต, โ, < ))) |
33 | 19 | adantr 481 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ ๐ต) โ ๐ด โ โ) |
34 | 33, 14 | remulcld 11243 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐ต) โ (๐ด ยท ๐) โ โ) |
35 | | eleq1a 2828 |
. . . . . . . . . . 11
โข ((๐ด ยท ๐) โ โ โ (๐ค = (๐ด ยท ๐) โ ๐ค โ โ)) |
36 | 34, 35 | syl 17 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐ต) โ (๐ค = (๐ด ยท ๐) โ ๐ค โ โ)) |
37 | 36 | rexlimdva 3155 |
. . . . . . . . 9
โข (๐ โ (โ๐ โ ๐ต ๐ค = (๐ด ยท ๐) โ ๐ค โ โ)) |
38 | 9, 37 | biimtrid 241 |
. . . . . . . 8
โข (๐ โ (๐ค โ ๐ถ โ ๐ค โ โ)) |
39 | 38 | ssrdv 3988 |
. . . . . . 7
โข (๐ โ ๐ถ โ โ) |
40 | | simpr2 1195 |
. . . . . . . . . 10
โข (((๐ด โ โ โง 0 โค
๐ด โง โ๐ฅ โ ๐ต 0 โค ๐ฅ) โง (๐ต โ โ โง ๐ต โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ต ๐ฆ โค ๐ฅ)) โ ๐ต โ โ
) |
41 | 10, 40 | sylbi 216 |
. . . . . . . . 9
โข (๐ โ ๐ต โ โ
) |
42 | | ovex 7441 |
. . . . . . . . . . 11
โข (๐ด ยท ๐) โ V |
43 | 42 | isseti 3489 |
. . . . . . . . . 10
โข
โ๐ค ๐ค = (๐ด ยท ๐) |
44 | 43 | rgenw 3065 |
. . . . . . . . 9
โข
โ๐ โ
๐ต โ๐ค ๐ค = (๐ด ยท ๐) |
45 | | r19.2z 4494 |
. . . . . . . . 9
โข ((๐ต โ โ
โง
โ๐ โ ๐ต โ๐ค ๐ค = (๐ด ยท ๐)) โ โ๐ โ ๐ต โ๐ค ๐ค = (๐ด ยท ๐)) |
46 | 41, 44, 45 | sylancl 586 |
. . . . . . . 8
โข (๐ โ โ๐ โ ๐ต โ๐ค ๐ค = (๐ด ยท ๐)) |
47 | 9 | exbii 1850 |
. . . . . . . . 9
โข
(โ๐ค ๐ค โ ๐ถ โ โ๐คโ๐ โ ๐ต ๐ค = (๐ด ยท ๐)) |
48 | | n0 4346 |
. . . . . . . . 9
โข (๐ถ โ โ
โ
โ๐ค ๐ค โ ๐ถ) |
49 | | rexcom4 3285 |
. . . . . . . . 9
โข
(โ๐ โ
๐ต โ๐ค ๐ค = (๐ด ยท ๐) โ โ๐คโ๐ โ ๐ต ๐ค = (๐ด ยท ๐)) |
50 | 47, 48, 49 | 3bitr4i 302 |
. . . . . . . 8
โข (๐ถ โ โ
โ
โ๐ โ ๐ต โ๐ค ๐ค = (๐ด ยท ๐)) |
51 | 46, 50 | sylibr 233 |
. . . . . . 7
โข (๐ โ ๐ถ โ โ
) |
52 | 19, 16 | remulcld 11243 |
. . . . . . . 8
โข (๐ โ (๐ด ยท sup(๐ต, โ, < )) โ
โ) |
53 | | brralrspcev 5208 |
. . . . . . . 8
โข (((๐ด ยท sup(๐ต, โ, < )) โ โ โง
โ๐ค โ ๐ถ ๐ค โค (๐ด ยท sup(๐ต, โ, < ))) โ โ๐ฅ โ โ โ๐ค โ ๐ถ ๐ค โค ๐ฅ) |
54 | 52, 32, 53 | syl2anc 584 |
. . . . . . 7
โข (๐ โ โ๐ฅ โ โ โ๐ค โ ๐ถ ๐ค โค ๐ฅ) |
55 | 39, 51, 54 | 3jca 1128 |
. . . . . 6
โข (๐ โ (๐ถ โ โ โง ๐ถ โ โ
โง โ๐ฅ โ โ โ๐ค โ ๐ถ ๐ค โค ๐ฅ)) |
56 | | suprleub 12179 |
. . . . . 6
โข (((๐ถ โ โ โง ๐ถ โ โ
โง โ๐ฅ โ โ โ๐ค โ ๐ถ ๐ค โค ๐ฅ) โง (๐ด ยท sup(๐ต, โ, < )) โ โ) โ
(sup(๐ถ, โ, < )
โค (๐ด ยท sup(๐ต, โ, < )) โ
โ๐ค โ ๐ถ ๐ค โค (๐ด ยท sup(๐ต, โ, < )))) |
57 | 55, 52, 56 | syl2anc 584 |
. . . . 5
โข (๐ โ (sup(๐ถ, โ, < ) โค (๐ด ยท sup(๐ต, โ, < )) โ โ๐ค โ ๐ถ ๐ค โค (๐ด ยท sup(๐ต, โ, < )))) |
58 | 32, 57 | mpbird 256 |
. . . 4
โข (๐ โ sup(๐ถ, โ, < ) โค (๐ด ยท sup(๐ต, โ, < ))) |
59 | | simpr 485 |
. . . . . . 7
โข ((๐ โง sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))) โ sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))) |
60 | | suprcl 12173 |
. . . . . . . . . 10
โข ((๐ถ โ โ โง ๐ถ โ โ
โง โ๐ฅ โ โ โ๐ค โ ๐ถ ๐ค โค ๐ฅ) โ sup(๐ถ, โ, < ) โ
โ) |
61 | 55, 60 | syl 17 |
. . . . . . . . 9
โข (๐ โ sup(๐ถ, โ, < ) โ
โ) |
62 | 61 | adantr 481 |
. . . . . . . 8
โข ((๐ โง sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))) โ sup(๐ถ, โ, < ) โ
โ) |
63 | 16 | adantr 481 |
. . . . . . . 8
โข ((๐ โง sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))) โ sup(๐ต, โ, < ) โ
โ) |
64 | 19 | adantr 481 |
. . . . . . . 8
โข ((๐ โง sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))) โ ๐ด โ โ) |
65 | | n0 4346 |
. . . . . . . . . . . 12
โข (๐ต โ โ
โ
โ๐ ๐ โ ๐ต) |
66 | | 0red 11216 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ ๐ต) โ 0 โ โ) |
67 | | simpl3 1193 |
. . . . . . . . . . . . . . . . 17
โข (((๐ด โ โ โง 0 โค
๐ด โง โ๐ฅ โ ๐ต 0 โค ๐ฅ) โง (๐ต โ โ โง ๐ต โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ต ๐ฆ โค ๐ฅ)) โ โ๐ฅ โ ๐ต 0 โค ๐ฅ) |
68 | 10, 67 | sylbi 216 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ๐ฅ โ ๐ต 0 โค ๐ฅ) |
69 | | breq2 5152 |
. . . . . . . . . . . . . . . . 17
โข (๐ฅ = ๐ โ (0 โค ๐ฅ โ 0 โค ๐)) |
70 | 69 | rspccva 3611 |
. . . . . . . . . . . . . . . 16
โข
((โ๐ฅ โ
๐ต 0 โค ๐ฅ โง ๐ โ ๐ต) โ 0 โค ๐) |
71 | 68, 70 | sylan 580 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ ๐ต) โ 0 โค ๐) |
72 | 66, 14, 17, 71, 25 | letrd 11370 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ ๐ต) โ 0 โค sup(๐ต, โ, < )) |
73 | 72 | ex 413 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ โ ๐ต โ 0 โค sup(๐ต, โ, < ))) |
74 | 73 | exlimdv 1936 |
. . . . . . . . . . . 12
โข (๐ โ (โ๐ ๐ โ ๐ต โ 0 โค sup(๐ต, โ, < ))) |
75 | 65, 74 | biimtrid 241 |
. . . . . . . . . . 11
โข (๐ โ (๐ต โ โ
โ 0 โค sup(๐ต, โ, <
))) |
76 | 41, 75 | mpd 15 |
. . . . . . . . . 10
โข (๐ โ 0 โค sup(๐ต, โ, <
)) |
77 | 76 | adantr 481 |
. . . . . . . . 9
โข ((๐ โง sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))) โ 0 โค sup(๐ต, โ, <
)) |
78 | | 0red 11216 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ค โ ๐ถ) โ 0 โ โ) |
79 | 38 | imp 407 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ค โ ๐ถ) โ ๐ค โ โ) |
80 | 61 | adantr 481 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ค โ ๐ถ) โ sup(๐ถ, โ, < ) โ
โ) |
81 | 21 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง ๐ โ ๐ต) โ 0 โค ๐ด) |
82 | 33, 14, 81, 71 | mulge0d 11790 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ๐ โ ๐ต) โ 0 โค (๐ด ยท ๐)) |
83 | | breq2 5152 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ค = (๐ด ยท ๐) โ (0 โค ๐ค โ 0 โค (๐ด ยท ๐))) |
84 | 82, 83 | syl5ibrcom 246 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ๐ โ ๐ต) โ (๐ค = (๐ด ยท ๐) โ 0 โค ๐ค)) |
85 | 84 | rexlimdva 3155 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (โ๐ โ ๐ต ๐ค = (๐ด ยท ๐) โ 0 โค ๐ค)) |
86 | 9, 85 | biimtrid 241 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (๐ค โ ๐ถ โ 0 โค ๐ค)) |
87 | 86 | imp 407 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ค โ ๐ถ) โ 0 โค ๐ค) |
88 | | suprub 12174 |
. . . . . . . . . . . . . . . . 17
โข (((๐ถ โ โ โง ๐ถ โ โ
โง โ๐ฅ โ โ โ๐ค โ ๐ถ ๐ค โค ๐ฅ) โง ๐ค โ ๐ถ) โ ๐ค โค sup(๐ถ, โ, < )) |
89 | 55, 88 | sylan 580 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ค โ ๐ถ) โ ๐ค โค sup(๐ถ, โ, < )) |
90 | 78, 79, 80, 87, 89 | letrd 11370 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ค โ ๐ถ) โ 0 โค sup(๐ถ, โ, < )) |
91 | 90 | ex 413 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ค โ ๐ถ โ 0 โค sup(๐ถ, โ, < ))) |
92 | 91 | exlimdv 1936 |
. . . . . . . . . . . . 13
โข (๐ โ (โ๐ค ๐ค โ ๐ถ โ 0 โค sup(๐ถ, โ, < ))) |
93 | 48, 92 | biimtrid 241 |
. . . . . . . . . . . 12
โข (๐ โ (๐ถ โ โ
โ 0 โค sup(๐ถ, โ, <
))) |
94 | 51, 93 | mpd 15 |
. . . . . . . . . . 11
โข (๐ โ 0 โค sup(๐ถ, โ, <
)) |
95 | 94 | anim1i 615 |
. . . . . . . . . 10
โข ((๐ โง sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))) โ (0 โค sup(๐ถ, โ, < ) โง
sup(๐ถ, โ, < ) <
(๐ด ยท sup(๐ต, โ, <
)))) |
96 | | 0red 11216 |
. . . . . . . . . . . 12
โข (๐ โ 0 โ
โ) |
97 | | lelttr 11303 |
. . . . . . . . . . . 12
โข ((0
โ โ โง sup(๐ถ,
โ, < ) โ โ โง (๐ด ยท sup(๐ต, โ, < )) โ โ) โ
((0 โค sup(๐ถ, โ,
< ) โง sup(๐ถ,
โ, < ) < (๐ด
ยท sup(๐ต, โ,
< ))) โ 0 < (๐ด
ยท sup(๐ต, โ,
< )))) |
98 | 96, 61, 52, 97 | syl3anc 1371 |
. . . . . . . . . . 11
โข (๐ โ ((0 โค sup(๐ถ, โ, < ) โง
sup(๐ถ, โ, < ) <
(๐ด ยท sup(๐ต, โ, < ))) โ 0
< (๐ด ยท sup(๐ต, โ, <
)))) |
99 | 98 | adantr 481 |
. . . . . . . . . 10
โข ((๐ โง sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))) โ ((0 โค
sup(๐ถ, โ, < )
โง sup(๐ถ, โ, <
) < (๐ด ยท
sup(๐ต, โ, < )))
โ 0 < (๐ด ยท
sup(๐ต, โ, <
)))) |
100 | 95, 99 | mpd 15 |
. . . . . . . . 9
โข ((๐ โง sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))) โ 0 < (๐ด ยท sup(๐ต, โ, < ))) |
101 | | prodgt02 12061 |
. . . . . . . . 9
โข (((๐ด โ โ โง sup(๐ต, โ, < ) โ
โ) โง (0 โค sup(๐ต, โ, < ) โง 0 < (๐ด ยท sup(๐ต, โ, < )))) โ 0 < ๐ด) |
102 | 64, 63, 77, 100, 101 | syl22anc 837 |
. . . . . . . 8
โข ((๐ โง sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))) โ 0 < ๐ด) |
103 | | ltdivmul 12088 |
. . . . . . . 8
โข
((sup(๐ถ, โ,
< ) โ โ โง sup(๐ต, โ, < ) โ โ โง
(๐ด โ โ โง 0
< ๐ด)) โ ((sup(๐ถ, โ, < ) / ๐ด) < sup(๐ต, โ, < ) โ sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < )))) |
104 | 62, 63, 64, 102, 103 | syl112anc 1374 |
. . . . . . 7
โข ((๐ โง sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))) โ ((sup(๐ถ, โ, < ) / ๐ด) < sup(๐ต, โ, < ) โ sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < )))) |
105 | 59, 104 | mpbird 256 |
. . . . . 6
โข ((๐ โง sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))) โ (sup(๐ถ, โ, < ) / ๐ด) < sup(๐ต, โ, < )) |
106 | 12 | adantr 481 |
. . . . . . 7
โข ((๐ โง sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))) โ (๐ต โ โ โง ๐ต โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ต ๐ฆ โค ๐ฅ)) |
107 | 102 | gt0ne0d 11777 |
. . . . . . . 8
โข ((๐ โง sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))) โ ๐ด โ 0) |
108 | 62, 64, 107 | redivcld 12041 |
. . . . . . 7
โข ((๐ โง sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))) โ (sup(๐ถ, โ, < ) / ๐ด) โ
โ) |
109 | | suprlub 12177 |
. . . . . . 7
โข (((๐ต โ โ โง ๐ต โ โ
โง โ๐ฅ โ โ โ๐ฆ โ ๐ต ๐ฆ โค ๐ฅ) โง (sup(๐ถ, โ, < ) / ๐ด) โ โ) โ ((sup(๐ถ, โ, < ) / ๐ด) < sup(๐ต, โ, < ) โ โ๐ โ ๐ต (sup(๐ถ, โ, < ) / ๐ด) < ๐)) |
110 | 106, 108,
109 | syl2anc 584 |
. . . . . 6
โข ((๐ โง sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))) โ ((sup(๐ถ, โ, < ) / ๐ด) < sup(๐ต, โ, < ) โ โ๐ โ ๐ต (sup(๐ถ, โ, < ) / ๐ด) < ๐)) |
111 | 105, 110 | mpbid 231 |
. . . . 5
โข ((๐ โง sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))) โ โ๐ โ ๐ต (sup(๐ถ, โ, < ) / ๐ด) < ๐) |
112 | 34 | adantlr 713 |
. . . . . . . 8
โข (((๐ โง sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))) โง ๐ โ ๐ต) โ (๐ด ยท ๐) โ โ) |
113 | 61 | ad2antrr 724 |
. . . . . . . 8
โข (((๐ โง sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))) โง ๐ โ ๐ต) โ sup(๐ถ, โ, < ) โ
โ) |
114 | | rspe 3246 |
. . . . . . . . . . . . . . 15
โข ((๐ โ ๐ต โง ๐ค = (๐ด ยท ๐)) โ โ๐ โ ๐ต ๐ค = (๐ด ยท ๐)) |
115 | 114, 9 | sylibr 233 |
. . . . . . . . . . . . . 14
โข ((๐ โ ๐ต โง ๐ค = (๐ด ยท ๐)) โ ๐ค โ ๐ถ) |
116 | 115 | adantl 482 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ ๐ต โง ๐ค = (๐ด ยท ๐))) โ ๐ค โ ๐ถ) |
117 | | simplrr 776 |
. . . . . . . . . . . . . 14
โข (((๐ โง (๐ โ ๐ต โง ๐ค = (๐ด ยท ๐))) โง ๐ค โ ๐ถ) โ ๐ค = (๐ด ยท ๐)) |
118 | 89 | adantlr 713 |
. . . . . . . . . . . . . 14
โข (((๐ โง (๐ โ ๐ต โง ๐ค = (๐ด ยท ๐))) โง ๐ค โ ๐ถ) โ ๐ค โค sup(๐ถ, โ, < )) |
119 | 117, 118 | eqbrtrrd 5172 |
. . . . . . . . . . . . 13
โข (((๐ โง (๐ โ ๐ต โง ๐ค = (๐ด ยท ๐))) โง ๐ค โ ๐ถ) โ (๐ด ยท ๐) โค sup(๐ถ, โ, < )) |
120 | 116, 119 | mpdan 685 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ ๐ต โง ๐ค = (๐ด ยท ๐))) โ (๐ด ยท ๐) โค sup(๐ถ, โ, < )) |
121 | 120 | expr 457 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐ต) โ (๐ค = (๐ด ยท ๐) โ (๐ด ยท ๐) โค sup(๐ถ, โ, < ))) |
122 | 121 | exlimdv 1936 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐ต) โ (โ๐ค ๐ค = (๐ด ยท ๐) โ (๐ด ยท ๐) โค sup(๐ถ, โ, < ))) |
123 | 43, 122 | mpi 20 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐ต) โ (๐ด ยท ๐) โค sup(๐ถ, โ, < )) |
124 | 123 | adantlr 713 |
. . . . . . . 8
โข (((๐ โง sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))) โง ๐ โ ๐ต) โ (๐ด ยท ๐) โค sup(๐ถ, โ, < )) |
125 | 112, 113,
124 | lensymd 11364 |
. . . . . . 7
โข (((๐ โง sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))) โง ๐ โ ๐ต) โ ยฌ sup(๐ถ, โ, < ) < (๐ด ยท ๐)) |
126 | 14 | adantlr 713 |
. . . . . . . 8
โข (((๐ โง sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))) โง ๐ โ ๐ต) โ ๐ โ โ) |
127 | 19 | ad2antrr 724 |
. . . . . . . 8
โข (((๐ โง sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))) โง ๐ โ ๐ต) โ ๐ด โ โ) |
128 | 102 | adantr 481 |
. . . . . . . 8
โข (((๐ โง sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))) โง ๐ โ ๐ต) โ 0 < ๐ด) |
129 | | ltdivmul 12088 |
. . . . . . . 8
โข
((sup(๐ถ, โ,
< ) โ โ โง ๐ โ โ โง (๐ด โ โ โง 0 < ๐ด)) โ ((sup(๐ถ, โ, < ) / ๐ด) < ๐ โ sup(๐ถ, โ, < ) < (๐ด ยท ๐))) |
130 | 113, 126,
127, 128, 129 | syl112anc 1374 |
. . . . . . 7
โข (((๐ โง sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))) โง ๐ โ ๐ต) โ ((sup(๐ถ, โ, < ) / ๐ด) < ๐ โ sup(๐ถ, โ, < ) < (๐ด ยท ๐))) |
131 | 125, 130 | mtbird 324 |
. . . . . 6
โข (((๐ โง sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))) โง ๐ โ ๐ต) โ ยฌ (sup(๐ถ, โ, < ) / ๐ด) < ๐) |
132 | 131 | nrexdv 3149 |
. . . . 5
โข ((๐ โง sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))) โ ยฌ
โ๐ โ ๐ต (sup(๐ถ, โ, < ) / ๐ด) < ๐) |
133 | 111, 132 | pm2.65da 815 |
. . . 4
โข (๐ โ ยฌ sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))) |
134 | 58, 133 | jca 512 |
. . 3
โข (๐ โ (sup(๐ถ, โ, < ) โค (๐ด ยท sup(๐ต, โ, < )) โง ยฌ sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < )))) |
135 | 61, 52 | eqleltd 11357 |
. . 3
โข (๐ โ (sup(๐ถ, โ, < ) = (๐ด ยท sup(๐ต, โ, < )) โ (sup(๐ถ, โ, < ) โค (๐ด ยท sup(๐ต, โ, < )) โง ยฌ sup(๐ถ, โ, < ) < (๐ด ยท sup(๐ต, โ, < ))))) |
136 | 134, 135 | mpbird 256 |
. 2
โข (๐ โ sup(๐ถ, โ, < ) = (๐ด ยท sup(๐ต, โ, < ))) |
137 | 136 | eqcomd 2738 |
1
โข (๐ โ (๐ด ยท sup(๐ต, โ, < )) = sup(๐ถ, โ, < )) |