Step | Hyp | Ref
| Expression |
1 | | simplll 774 |
. . . . . . . . . 10
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ ๐ด โ โค) |
2 | | simplrl 776 |
. . . . . . . . . 10
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ ๐ถ โ
โ0) |
3 | | dyadmbl.1 |
. . . . . . . . . . 11
โข ๐น = (๐ฅ โ โค, ๐ฆ โ โ0 โฆ
โจ(๐ฅ / (2โ๐ฆ)), ((๐ฅ + 1) / (2โ๐ฆ))โฉ) |
4 | 3 | dyadval 24979 |
. . . . . . . . . 10
โข ((๐ด โ โค โง ๐ถ โ โ0)
โ (๐ด๐น๐ถ) = โจ(๐ด / (2โ๐ถ)), ((๐ด + 1) / (2โ๐ถ))โฉ) |
5 | 1, 2, 4 | syl2anc 585 |
. . . . . . . . 9
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ (๐ด๐น๐ถ) = โจ(๐ด / (2โ๐ถ)), ((๐ด + 1) / (2โ๐ถ))โฉ) |
6 | 5 | fveq2d 6850 |
. . . . . . . 8
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ ((,)โ(๐ด๐น๐ถ)) = ((,)โโจ(๐ด / (2โ๐ถ)), ((๐ด + 1) / (2โ๐ถ))โฉ)) |
7 | | df-ov 7364 |
. . . . . . . 8
โข ((๐ด / (2โ๐ถ))(,)((๐ด + 1) / (2โ๐ถ))) = ((,)โโจ(๐ด / (2โ๐ถ)), ((๐ด + 1) / (2โ๐ถ))โฉ) |
8 | 6, 7 | eqtr4di 2791 |
. . . . . . 7
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ ((,)โ(๐ด๐น๐ถ)) = ((๐ด / (2โ๐ถ))(,)((๐ด + 1) / (2โ๐ถ)))) |
9 | | simpllr 775 |
. . . . . . . . . 10
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ ๐ต โ โค) |
10 | | simplrr 777 |
. . . . . . . . . 10
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ ๐ท โ
โ0) |
11 | 3 | dyadval 24979 |
. . . . . . . . . 10
โข ((๐ต โ โค โง ๐ท โ โ0)
โ (๐ต๐น๐ท) = โจ(๐ต / (2โ๐ท)), ((๐ต + 1) / (2โ๐ท))โฉ) |
12 | 9, 10, 11 | syl2anc 585 |
. . . . . . . . 9
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ (๐ต๐น๐ท) = โจ(๐ต / (2โ๐ท)), ((๐ต + 1) / (2โ๐ท))โฉ) |
13 | 12 | fveq2d 6850 |
. . . . . . . 8
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ ((,)โ(๐ต๐น๐ท)) = ((,)โโจ(๐ต / (2โ๐ท)), ((๐ต + 1) / (2โ๐ท))โฉ)) |
14 | | df-ov 7364 |
. . . . . . . 8
โข ((๐ต / (2โ๐ท))(,)((๐ต + 1) / (2โ๐ท))) = ((,)โโจ(๐ต / (2โ๐ท)), ((๐ต + 1) / (2โ๐ท))โฉ) |
15 | 13, 14 | eqtr4di 2791 |
. . . . . . 7
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ ((,)โ(๐ต๐น๐ท)) = ((๐ต / (2โ๐ท))(,)((๐ต + 1) / (2โ๐ท)))) |
16 | 8, 15 | ineq12d 4177 |
. . . . . 6
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ (((,)โ(๐ด๐น๐ถ)) โฉ ((,)โ(๐ต๐น๐ท))) = (((๐ด / (2โ๐ถ))(,)((๐ด + 1) / (2โ๐ถ))) โฉ ((๐ต / (2โ๐ท))(,)((๐ต + 1) / (2โ๐ท))))) |
17 | | incom 4165 |
. . . . . 6
โข (((๐ด / (2โ๐ถ))(,)((๐ด + 1) / (2โ๐ถ))) โฉ ((๐ต / (2โ๐ท))(,)((๐ต + 1) / (2โ๐ท)))) = (((๐ต / (2โ๐ท))(,)((๐ต + 1) / (2โ๐ท))) โฉ ((๐ด / (2โ๐ถ))(,)((๐ด + 1) / (2โ๐ถ)))) |
18 | 16, 17 | eqtrdi 2789 |
. . . . 5
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ (((,)โ(๐ด๐น๐ถ)) โฉ ((,)โ(๐ต๐น๐ท))) = (((๐ต / (2โ๐ท))(,)((๐ต + 1) / (2โ๐ท))) โฉ ((๐ด / (2โ๐ถ))(,)((๐ด + 1) / (2โ๐ถ))))) |
19 | 18 | adantr 482 |
. . . 4
โข
(((((๐ด โ
โค โง ๐ต โ
โค) โง (๐ถ โ
โ0 โง ๐ท
โ โ0)) โง ๐ถ โค ๐ท) โง (๐ต / (2โ๐ท)) < (๐ด / (2โ๐ถ))) โ (((,)โ(๐ด๐น๐ถ)) โฉ ((,)โ(๐ต๐น๐ท))) = (((๐ต / (2โ๐ท))(,)((๐ต + 1) / (2โ๐ท))) โฉ ((๐ด / (2โ๐ถ))(,)((๐ด + 1) / (2โ๐ถ))))) |
20 | 1 | zred 12615 |
. . . . . . . . . . 11
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ ๐ด โ โ) |
21 | 20 | recnd 11191 |
. . . . . . . . . 10
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ ๐ด โ โ) |
22 | | 2nn 12234 |
. . . . . . . . . . . 12
โข 2 โ
โ |
23 | | nnexpcl 13989 |
. . . . . . . . . . . 12
โข ((2
โ โ โง ๐ถ
โ โ0) โ (2โ๐ถ) โ โ) |
24 | 22, 2, 23 | sylancr 588 |
. . . . . . . . . . 11
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ (2โ๐ถ) โ โ) |
25 | 24 | nncnd 12177 |
. . . . . . . . . 10
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ (2โ๐ถ) โ โ) |
26 | | nnexpcl 13989 |
. . . . . . . . . . . 12
โข ((2
โ โ โง ๐ท
โ โ0) โ (2โ๐ท) โ โ) |
27 | 22, 10, 26 | sylancr 588 |
. . . . . . . . . . 11
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ (2โ๐ท) โ โ) |
28 | 27 | nncnd 12177 |
. . . . . . . . . 10
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ (2โ๐ท) โ โ) |
29 | 24 | nnne0d 12211 |
. . . . . . . . . 10
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ (2โ๐ถ) โ 0) |
30 | 21, 25, 28, 29 | div13d 11963 |
. . . . . . . . 9
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ ((๐ด / (2โ๐ถ)) ยท (2โ๐ท)) = (((2โ๐ท) / (2โ๐ถ)) ยท ๐ด)) |
31 | | 2cnd 12239 |
. . . . . . . . . . . 12
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ 2 โ โ) |
32 | | 2ne0 12265 |
. . . . . . . . . . . . 13
โข 2 โ
0 |
33 | 32 | a1i 11 |
. . . . . . . . . . . 12
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ 2 โ 0) |
34 | 2 | nn0zd 12533 |
. . . . . . . . . . . 12
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ ๐ถ โ โค) |
35 | 10 | nn0zd 12533 |
. . . . . . . . . . . 12
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ ๐ท โ โค) |
36 | 31, 33, 34, 35 | expsubd 14071 |
. . . . . . . . . . 11
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ (2โ(๐ท โ ๐ถ)) = ((2โ๐ท) / (2โ๐ถ))) |
37 | | 2z 12543 |
. . . . . . . . . . . 12
โข 2 โ
โค |
38 | | simpr 486 |
. . . . . . . . . . . . 13
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ ๐ถ โค ๐ท) |
39 | | znn0sub 12558 |
. . . . . . . . . . . . . 14
โข ((๐ถ โ โค โง ๐ท โ โค) โ (๐ถ โค ๐ท โ (๐ท โ ๐ถ) โ
โ0)) |
40 | 34, 35, 39 | syl2anc 585 |
. . . . . . . . . . . . 13
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ (๐ถ โค ๐ท โ (๐ท โ ๐ถ) โ
โ0)) |
41 | 38, 40 | mpbid 231 |
. . . . . . . . . . . 12
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ (๐ท โ ๐ถ) โ
โ0) |
42 | | zexpcl 13991 |
. . . . . . . . . . . 12
โข ((2
โ โค โง (๐ท
โ ๐ถ) โ
โ0) โ (2โ(๐ท โ ๐ถ)) โ โค) |
43 | 37, 41, 42 | sylancr 588 |
. . . . . . . . . . 11
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ (2โ(๐ท โ ๐ถ)) โ โค) |
44 | 36, 43 | eqeltrrd 2835 |
. . . . . . . . . 10
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ ((2โ๐ท) / (2โ๐ถ)) โ โค) |
45 | 44, 1 | zmulcld 12621 |
. . . . . . . . 9
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ (((2โ๐ท) / (2โ๐ถ)) ยท ๐ด) โ โค) |
46 | 30, 45 | eqeltrd 2834 |
. . . . . . . 8
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ ((๐ด / (2โ๐ถ)) ยท (2โ๐ท)) โ โค) |
47 | | zltp1le 12561 |
. . . . . . . 8
โข ((๐ต โ โค โง ((๐ด / (2โ๐ถ)) ยท (2โ๐ท)) โ โค) โ (๐ต < ((๐ด / (2โ๐ถ)) ยท (2โ๐ท)) โ (๐ต + 1) โค ((๐ด / (2โ๐ถ)) ยท (2โ๐ท)))) |
48 | 9, 46, 47 | syl2anc 585 |
. . . . . . 7
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ (๐ต < ((๐ด / (2โ๐ถ)) ยท (2โ๐ท)) โ (๐ต + 1) โค ((๐ด / (2โ๐ถ)) ยท (2โ๐ท)))) |
49 | 9 | zred 12615 |
. . . . . . . 8
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ ๐ต โ โ) |
50 | 20, 24 | nndivred 12215 |
. . . . . . . 8
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ (๐ด / (2โ๐ถ)) โ โ) |
51 | 27 | nnred 12176 |
. . . . . . . 8
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ (2โ๐ท) โ โ) |
52 | 27 | nngt0d 12210 |
. . . . . . . 8
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ 0 < (2โ๐ท)) |
53 | | ltdivmul2 12040 |
. . . . . . . 8
โข ((๐ต โ โ โง (๐ด / (2โ๐ถ)) โ โ โง ((2โ๐ท) โ โ โง 0 <
(2โ๐ท))) โ ((๐ต / (2โ๐ท)) < (๐ด / (2โ๐ถ)) โ ๐ต < ((๐ด / (2โ๐ถ)) ยท (2โ๐ท)))) |
54 | 49, 50, 51, 52, 53 | syl112anc 1375 |
. . . . . . 7
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ ((๐ต / (2โ๐ท)) < (๐ด / (2โ๐ถ)) โ ๐ต < ((๐ด / (2โ๐ถ)) ยท (2โ๐ท)))) |
55 | | peano2re 11336 |
. . . . . . . . 9
โข (๐ต โ โ โ (๐ต + 1) โ
โ) |
56 | 49, 55 | syl 17 |
. . . . . . . 8
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ (๐ต + 1) โ โ) |
57 | | ledivmul2 12042 |
. . . . . . . 8
โข (((๐ต + 1) โ โ โง
(๐ด / (2โ๐ถ)) โ โ โง
((2โ๐ท) โ โ
โง 0 < (2โ๐ท)))
โ (((๐ต + 1) /
(2โ๐ท)) โค (๐ด / (2โ๐ถ)) โ (๐ต + 1) โค ((๐ด / (2โ๐ถ)) ยท (2โ๐ท)))) |
58 | 56, 50, 51, 52, 57 | syl112anc 1375 |
. . . . . . 7
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ (((๐ต + 1) / (2โ๐ท)) โค (๐ด / (2โ๐ถ)) โ (๐ต + 1) โค ((๐ด / (2โ๐ถ)) ยท (2โ๐ท)))) |
59 | 48, 54, 58 | 3bitr4d 311 |
. . . . . 6
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ ((๐ต / (2โ๐ท)) < (๐ด / (2โ๐ถ)) โ ((๐ต + 1) / (2โ๐ท)) โค (๐ด / (2โ๐ถ)))) |
60 | 49, 27 | nndivred 12215 |
. . . . . . . 8
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ (๐ต / (2โ๐ท)) โ โ) |
61 | 60 | rexrd 11213 |
. . . . . . 7
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ (๐ต / (2โ๐ท)) โ
โ*) |
62 | 56, 27 | nndivred 12215 |
. . . . . . . 8
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ ((๐ต + 1) / (2โ๐ท)) โ โ) |
63 | 62 | rexrd 11213 |
. . . . . . 7
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ ((๐ต + 1) / (2โ๐ท)) โ
โ*) |
64 | 50 | rexrd 11213 |
. . . . . . 7
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ (๐ด / (2โ๐ถ)) โ
โ*) |
65 | | peano2re 11336 |
. . . . . . . . . 10
โข (๐ด โ โ โ (๐ด + 1) โ
โ) |
66 | 20, 65 | syl 17 |
. . . . . . . . 9
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ (๐ด + 1) โ โ) |
67 | 66, 24 | nndivred 12215 |
. . . . . . . 8
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ ((๐ด + 1) / (2โ๐ถ)) โ โ) |
68 | 67 | rexrd 11213 |
. . . . . . 7
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ ((๐ด + 1) / (2โ๐ถ)) โ
โ*) |
69 | | ioodisj 13408 |
. . . . . . . 8
โข
(((((๐ต /
(2โ๐ท)) โ
โ* โง ((๐ต + 1) / (2โ๐ท)) โ โ*) โง ((๐ด / (2โ๐ถ)) โ โ* โง ((๐ด + 1) / (2โ๐ถ)) โ โ*))
โง ((๐ต + 1) /
(2โ๐ท)) โค (๐ด / (2โ๐ถ))) โ (((๐ต / (2โ๐ท))(,)((๐ต + 1) / (2โ๐ท))) โฉ ((๐ด / (2โ๐ถ))(,)((๐ด + 1) / (2โ๐ถ)))) = โ
) |
70 | 69 | ex 414 |
. . . . . . 7
โข ((((๐ต / (2โ๐ท)) โ โ* โง ((๐ต + 1) / (2โ๐ท)) โ โ*)
โง ((๐ด / (2โ๐ถ)) โ โ*
โง ((๐ด + 1) /
(2โ๐ถ)) โ
โ*)) โ (((๐ต + 1) / (2โ๐ท)) โค (๐ด / (2โ๐ถ)) โ (((๐ต / (2โ๐ท))(,)((๐ต + 1) / (2โ๐ท))) โฉ ((๐ด / (2โ๐ถ))(,)((๐ด + 1) / (2โ๐ถ)))) = โ
)) |
71 | 61, 63, 64, 68, 70 | syl22anc 838 |
. . . . . 6
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ (((๐ต + 1) / (2โ๐ท)) โค (๐ด / (2โ๐ถ)) โ (((๐ต / (2โ๐ท))(,)((๐ต + 1) / (2โ๐ท))) โฉ ((๐ด / (2โ๐ถ))(,)((๐ด + 1) / (2โ๐ถ)))) = โ
)) |
72 | 59, 71 | sylbid 239 |
. . . . 5
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ ((๐ต / (2โ๐ท)) < (๐ด / (2โ๐ถ)) โ (((๐ต / (2โ๐ท))(,)((๐ต + 1) / (2โ๐ท))) โฉ ((๐ด / (2โ๐ถ))(,)((๐ด + 1) / (2โ๐ถ)))) = โ
)) |
73 | 72 | imp 408 |
. . . 4
โข
(((((๐ด โ
โค โง ๐ต โ
โค) โง (๐ถ โ
โ0 โง ๐ท
โ โ0)) โง ๐ถ โค ๐ท) โง (๐ต / (2โ๐ท)) < (๐ด / (2โ๐ถ))) โ (((๐ต / (2โ๐ท))(,)((๐ต + 1) / (2โ๐ท))) โฉ ((๐ด / (2โ๐ถ))(,)((๐ด + 1) / (2โ๐ถ)))) = โ
) |
74 | 19, 73 | eqtrd 2773 |
. . 3
โข
(((((๐ด โ
โค โง ๐ต โ
โค) โง (๐ถ โ
โ0 โง ๐ท
โ โ0)) โง ๐ถ โค ๐ท) โง (๐ต / (2โ๐ท)) < (๐ด / (2โ๐ถ))) โ (((,)โ(๐ด๐น๐ถ)) โฉ ((,)โ(๐ต๐น๐ท))) = โ
) |
75 | 74 | 3mix3d 1339 |
. 2
โข
(((((๐ด โ
โค โง ๐ต โ
โค) โง (๐ถ โ
โ0 โง ๐ท
โ โ0)) โง ๐ถ โค ๐ท) โง (๐ต / (2โ๐ท)) < (๐ด / (2โ๐ถ))) โ (([,]โ(๐ด๐น๐ถ)) โ ([,]โ(๐ต๐น๐ท)) โจ ([,]โ(๐ต๐น๐ท)) โ ([,]โ(๐ด๐น๐ถ)) โจ (((,)โ(๐ด๐น๐ถ)) โฉ ((,)โ(๐ต๐น๐ท))) = โ
)) |
76 | 50 | adantr 482 |
. . . . . . 7
โข
(((((๐ด โ
โค โง ๐ต โ
โค) โง (๐ถ โ
โ0 โง ๐ท
โ โ0)) โง ๐ถ โค ๐ท) โง ((๐ด / (2โ๐ถ)) โค (๐ต / (2โ๐ท)) โง (๐ต / (2โ๐ท)) < ((๐ด + 1) / (2โ๐ถ)))) โ (๐ด / (2โ๐ถ)) โ โ) |
77 | 67 | adantr 482 |
. . . . . . 7
โข
(((((๐ด โ
โค โง ๐ต โ
โค) โง (๐ถ โ
โ0 โง ๐ท
โ โ0)) โง ๐ถ โค ๐ท) โง ((๐ด / (2โ๐ถ)) โค (๐ต / (2โ๐ท)) โง (๐ต / (2โ๐ท)) < ((๐ด + 1) / (2โ๐ถ)))) โ ((๐ด + 1) / (2โ๐ถ)) โ โ) |
78 | | simprl 770 |
. . . . . . 7
โข
(((((๐ด โ
โค โง ๐ต โ
โค) โง (๐ถ โ
โ0 โง ๐ท
โ โ0)) โง ๐ถ โค ๐ท) โง ((๐ด / (2โ๐ถ)) โค (๐ต / (2โ๐ท)) โง (๐ต / (2โ๐ท)) < ((๐ด + 1) / (2โ๐ถ)))) โ (๐ด / (2โ๐ถ)) โค (๐ต / (2โ๐ท))) |
79 | 66 | recnd 11191 |
. . . . . . . . . . . . 13
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ (๐ด + 1) โ โ) |
80 | 79, 25, 28, 29 | div13d 11963 |
. . . . . . . . . . . 12
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ (((๐ด + 1) / (2โ๐ถ)) ยท (2โ๐ท)) = (((2โ๐ท) / (2โ๐ถ)) ยท (๐ด + 1))) |
81 | 1 | peano2zd 12618 |
. . . . . . . . . . . . 13
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ (๐ด + 1) โ โค) |
82 | 44, 81 | zmulcld 12621 |
. . . . . . . . . . . 12
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ (((2โ๐ท) / (2โ๐ถ)) ยท (๐ด + 1)) โ โค) |
83 | 80, 82 | eqeltrd 2834 |
. . . . . . . . . . 11
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ (((๐ด + 1) / (2โ๐ถ)) ยท (2โ๐ท)) โ โค) |
84 | | zltp1le 12561 |
. . . . . . . . . . 11
โข ((๐ต โ โค โง (((๐ด + 1) / (2โ๐ถ)) ยท (2โ๐ท)) โ โค) โ (๐ต < (((๐ด + 1) / (2โ๐ถ)) ยท (2โ๐ท)) โ (๐ต + 1) โค (((๐ด + 1) / (2โ๐ถ)) ยท (2โ๐ท)))) |
85 | 9, 83, 84 | syl2anc 585 |
. . . . . . . . . 10
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ (๐ต < (((๐ด + 1) / (2โ๐ถ)) ยท (2โ๐ท)) โ (๐ต + 1) โค (((๐ด + 1) / (2โ๐ถ)) ยท (2โ๐ท)))) |
86 | | ltdivmul2 12040 |
. . . . . . . . . . 11
โข ((๐ต โ โ โง ((๐ด + 1) / (2โ๐ถ)) โ โ โง
((2โ๐ท) โ โ
โง 0 < (2โ๐ท)))
โ ((๐ต / (2โ๐ท)) < ((๐ด + 1) / (2โ๐ถ)) โ ๐ต < (((๐ด + 1) / (2โ๐ถ)) ยท (2โ๐ท)))) |
87 | 49, 67, 51, 52, 86 | syl112anc 1375 |
. . . . . . . . . 10
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ ((๐ต / (2โ๐ท)) < ((๐ด + 1) / (2โ๐ถ)) โ ๐ต < (((๐ด + 1) / (2โ๐ถ)) ยท (2โ๐ท)))) |
88 | | ledivmul2 12042 |
. . . . . . . . . . 11
โข (((๐ต + 1) โ โ โง
((๐ด + 1) / (2โ๐ถ)) โ โ โง
((2โ๐ท) โ โ
โง 0 < (2โ๐ท)))
โ (((๐ต + 1) /
(2โ๐ท)) โค ((๐ด + 1) / (2โ๐ถ)) โ (๐ต + 1) โค (((๐ด + 1) / (2โ๐ถ)) ยท (2โ๐ท)))) |
89 | 56, 67, 51, 52, 88 | syl112anc 1375 |
. . . . . . . . . 10
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ (((๐ต + 1) / (2โ๐ท)) โค ((๐ด + 1) / (2โ๐ถ)) โ (๐ต + 1) โค (((๐ด + 1) / (2โ๐ถ)) ยท (2โ๐ท)))) |
90 | 85, 87, 89 | 3bitr4d 311 |
. . . . . . . . 9
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ ((๐ต / (2โ๐ท)) < ((๐ด + 1) / (2โ๐ถ)) โ ((๐ต + 1) / (2โ๐ท)) โค ((๐ด + 1) / (2โ๐ถ)))) |
91 | 90 | biimpa 478 |
. . . . . . . 8
โข
(((((๐ด โ
โค โง ๐ต โ
โค) โง (๐ถ โ
โ0 โง ๐ท
โ โ0)) โง ๐ถ โค ๐ท) โง (๐ต / (2โ๐ท)) < ((๐ด + 1) / (2โ๐ถ))) โ ((๐ต + 1) / (2โ๐ท)) โค ((๐ด + 1) / (2โ๐ถ))) |
92 | 91 | adantrl 715 |
. . . . . . 7
โข
(((((๐ด โ
โค โง ๐ต โ
โค) โง (๐ถ โ
โ0 โง ๐ท
โ โ0)) โง ๐ถ โค ๐ท) โง ((๐ด / (2โ๐ถ)) โค (๐ต / (2โ๐ท)) โง (๐ต / (2โ๐ท)) < ((๐ด + 1) / (2โ๐ถ)))) โ ((๐ต + 1) / (2โ๐ท)) โค ((๐ด + 1) / (2โ๐ถ))) |
93 | | iccss 13341 |
. . . . . . 7
โข ((((๐ด / (2โ๐ถ)) โ โ โง ((๐ด + 1) / (2โ๐ถ)) โ โ) โง ((๐ด / (2โ๐ถ)) โค (๐ต / (2โ๐ท)) โง ((๐ต + 1) / (2โ๐ท)) โค ((๐ด + 1) / (2โ๐ถ)))) โ ((๐ต / (2โ๐ท))[,]((๐ต + 1) / (2โ๐ท))) โ ((๐ด / (2โ๐ถ))[,]((๐ด + 1) / (2โ๐ถ)))) |
94 | 76, 77, 78, 92, 93 | syl22anc 838 |
. . . . . 6
โข
(((((๐ด โ
โค โง ๐ต โ
โค) โง (๐ถ โ
โ0 โง ๐ท
โ โ0)) โง ๐ถ โค ๐ท) โง ((๐ด / (2โ๐ถ)) โค (๐ต / (2โ๐ท)) โง (๐ต / (2โ๐ท)) < ((๐ด + 1) / (2โ๐ถ)))) โ ((๐ต / (2โ๐ท))[,]((๐ต + 1) / (2โ๐ท))) โ ((๐ด / (2โ๐ถ))[,]((๐ด + 1) / (2โ๐ถ)))) |
95 | 12 | fveq2d 6850 |
. . . . . . . 8
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ ([,]โ(๐ต๐น๐ท)) = ([,]โโจ(๐ต / (2โ๐ท)), ((๐ต + 1) / (2โ๐ท))โฉ)) |
96 | | df-ov 7364 |
. . . . . . . 8
โข ((๐ต / (2โ๐ท))[,]((๐ต + 1) / (2โ๐ท))) = ([,]โโจ(๐ต / (2โ๐ท)), ((๐ต + 1) / (2โ๐ท))โฉ) |
97 | 95, 96 | eqtr4di 2791 |
. . . . . . 7
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ ([,]โ(๐ต๐น๐ท)) = ((๐ต / (2โ๐ท))[,]((๐ต + 1) / (2โ๐ท)))) |
98 | 97 | adantr 482 |
. . . . . 6
โข
(((((๐ด โ
โค โง ๐ต โ
โค) โง (๐ถ โ
โ0 โง ๐ท
โ โ0)) โง ๐ถ โค ๐ท) โง ((๐ด / (2โ๐ถ)) โค (๐ต / (2โ๐ท)) โง (๐ต / (2โ๐ท)) < ((๐ด + 1) / (2โ๐ถ)))) โ ([,]โ(๐ต๐น๐ท)) = ((๐ต / (2โ๐ท))[,]((๐ต + 1) / (2โ๐ท)))) |
99 | 5 | fveq2d 6850 |
. . . . . . . 8
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ ([,]โ(๐ด๐น๐ถ)) = ([,]โโจ(๐ด / (2โ๐ถ)), ((๐ด + 1) / (2โ๐ถ))โฉ)) |
100 | | df-ov 7364 |
. . . . . . . 8
โข ((๐ด / (2โ๐ถ))[,]((๐ด + 1) / (2โ๐ถ))) = ([,]โโจ(๐ด / (2โ๐ถ)), ((๐ด + 1) / (2โ๐ถ))โฉ) |
101 | 99, 100 | eqtr4di 2791 |
. . . . . . 7
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ ([,]โ(๐ด๐น๐ถ)) = ((๐ด / (2โ๐ถ))[,]((๐ด + 1) / (2โ๐ถ)))) |
102 | 101 | adantr 482 |
. . . . . 6
โข
(((((๐ด โ
โค โง ๐ต โ
โค) โง (๐ถ โ
โ0 โง ๐ท
โ โ0)) โง ๐ถ โค ๐ท) โง ((๐ด / (2โ๐ถ)) โค (๐ต / (2โ๐ท)) โง (๐ต / (2โ๐ท)) < ((๐ด + 1) / (2โ๐ถ)))) โ ([,]โ(๐ด๐น๐ถ)) = ((๐ด / (2โ๐ถ))[,]((๐ด + 1) / (2โ๐ถ)))) |
103 | 94, 98, 102 | 3sstr4d 3995 |
. . . . 5
โข
(((((๐ด โ
โค โง ๐ต โ
โค) โง (๐ถ โ
โ0 โง ๐ท
โ โ0)) โง ๐ถ โค ๐ท) โง ((๐ด / (2โ๐ถ)) โค (๐ต / (2โ๐ท)) โง (๐ต / (2โ๐ท)) < ((๐ด + 1) / (2โ๐ถ)))) โ ([,]โ(๐ต๐น๐ท)) โ ([,]โ(๐ด๐น๐ถ))) |
104 | 103 | 3mix2d 1338 |
. . . 4
โข
(((((๐ด โ
โค โง ๐ต โ
โค) โง (๐ถ โ
โ0 โง ๐ท
โ โ0)) โง ๐ถ โค ๐ท) โง ((๐ด / (2โ๐ถ)) โค (๐ต / (2โ๐ท)) โง (๐ต / (2โ๐ท)) < ((๐ด + 1) / (2โ๐ถ)))) โ (([,]โ(๐ด๐น๐ถ)) โ ([,]โ(๐ต๐น๐ท)) โจ ([,]โ(๐ต๐น๐ท)) โ ([,]โ(๐ด๐น๐ถ)) โจ (((,)โ(๐ด๐น๐ถ)) โฉ ((,)โ(๐ต๐น๐ท))) = โ
)) |
105 | 104 | anassrs 469 |
. . 3
โข
((((((๐ด โ
โค โง ๐ต โ
โค) โง (๐ถ โ
โ0 โง ๐ท
โ โ0)) โง ๐ถ โค ๐ท) โง (๐ด / (2โ๐ถ)) โค (๐ต / (2โ๐ท))) โง (๐ต / (2โ๐ท)) < ((๐ด + 1) / (2โ๐ถ))) โ (([,]โ(๐ด๐น๐ถ)) โ ([,]โ(๐ต๐น๐ท)) โจ ([,]โ(๐ต๐น๐ท)) โ ([,]โ(๐ด๐น๐ถ)) โจ (((,)โ(๐ด๐น๐ถ)) โฉ ((,)โ(๐ต๐น๐ท))) = โ
)) |
106 | 16 | adantr 482 |
. . . . . 6
โข
(((((๐ด โ
โค โง ๐ต โ
โค) โง (๐ถ โ
โ0 โง ๐ท
โ โ0)) โง ๐ถ โค ๐ท) โง ((๐ด + 1) / (2โ๐ถ)) โค (๐ต / (2โ๐ท))) โ (((,)โ(๐ด๐น๐ถ)) โฉ ((,)โ(๐ต๐น๐ท))) = (((๐ด / (2โ๐ถ))(,)((๐ด + 1) / (2โ๐ถ))) โฉ ((๐ต / (2โ๐ท))(,)((๐ต + 1) / (2โ๐ท))))) |
107 | | ioodisj 13408 |
. . . . . . . . 9
โข
(((((๐ด /
(2โ๐ถ)) โ
โ* โง ((๐ด + 1) / (2โ๐ถ)) โ โ*) โง ((๐ต / (2โ๐ท)) โ โ* โง ((๐ต + 1) / (2โ๐ท)) โ โ*))
โง ((๐ด + 1) /
(2โ๐ถ)) โค (๐ต / (2โ๐ท))) โ (((๐ด / (2โ๐ถ))(,)((๐ด + 1) / (2โ๐ถ))) โฉ ((๐ต / (2โ๐ท))(,)((๐ต + 1) / (2โ๐ท)))) = โ
) |
108 | 107 | ex 414 |
. . . . . . . 8
โข ((((๐ด / (2โ๐ถ)) โ โ* โง ((๐ด + 1) / (2โ๐ถ)) โ โ*)
โง ((๐ต / (2โ๐ท)) โ โ*
โง ((๐ต + 1) /
(2โ๐ท)) โ
โ*)) โ (((๐ด + 1) / (2โ๐ถ)) โค (๐ต / (2โ๐ท)) โ (((๐ด / (2โ๐ถ))(,)((๐ด + 1) / (2โ๐ถ))) โฉ ((๐ต / (2โ๐ท))(,)((๐ต + 1) / (2โ๐ท)))) = โ
)) |
109 | 64, 68, 61, 63, 108 | syl22anc 838 |
. . . . . . 7
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ (((๐ด + 1) / (2โ๐ถ)) โค (๐ต / (2โ๐ท)) โ (((๐ด / (2โ๐ถ))(,)((๐ด + 1) / (2โ๐ถ))) โฉ ((๐ต / (2โ๐ท))(,)((๐ต + 1) / (2โ๐ท)))) = โ
)) |
110 | 109 | imp 408 |
. . . . . 6
โข
(((((๐ด โ
โค โง ๐ต โ
โค) โง (๐ถ โ
โ0 โง ๐ท
โ โ0)) โง ๐ถ โค ๐ท) โง ((๐ด + 1) / (2โ๐ถ)) โค (๐ต / (2โ๐ท))) โ (((๐ด / (2โ๐ถ))(,)((๐ด + 1) / (2โ๐ถ))) โฉ ((๐ต / (2โ๐ท))(,)((๐ต + 1) / (2โ๐ท)))) = โ
) |
111 | 106, 110 | eqtrd 2773 |
. . . . 5
โข
(((((๐ด โ
โค โง ๐ต โ
โค) โง (๐ถ โ
โ0 โง ๐ท
โ โ0)) โง ๐ถ โค ๐ท) โง ((๐ด + 1) / (2โ๐ถ)) โค (๐ต / (2โ๐ท))) โ (((,)โ(๐ด๐น๐ถ)) โฉ ((,)โ(๐ต๐น๐ท))) = โ
) |
112 | 111 | 3mix3d 1339 |
. . . 4
โข
(((((๐ด โ
โค โง ๐ต โ
โค) โง (๐ถ โ
โ0 โง ๐ท
โ โ0)) โง ๐ถ โค ๐ท) โง ((๐ด + 1) / (2โ๐ถ)) โค (๐ต / (2โ๐ท))) โ (([,]โ(๐ด๐น๐ถ)) โ ([,]โ(๐ต๐น๐ท)) โจ ([,]โ(๐ต๐น๐ท)) โ ([,]โ(๐ด๐น๐ถ)) โจ (((,)โ(๐ด๐น๐ถ)) โฉ ((,)โ(๐ต๐น๐ท))) = โ
)) |
113 | 112 | adantlr 714 |
. . 3
โข
((((((๐ด โ
โค โง ๐ต โ
โค) โง (๐ถ โ
โ0 โง ๐ท
โ โ0)) โง ๐ถ โค ๐ท) โง (๐ด / (2โ๐ถ)) โค (๐ต / (2โ๐ท))) โง ((๐ด + 1) / (2โ๐ถ)) โค (๐ต / (2โ๐ท))) โ (([,]โ(๐ด๐น๐ถ)) โ ([,]โ(๐ต๐น๐ท)) โจ ([,]โ(๐ต๐น๐ท)) โ ([,]โ(๐ด๐น๐ถ)) โจ (((,)โ(๐ด๐น๐ถ)) โฉ ((,)โ(๐ต๐น๐ท))) = โ
)) |
114 | 60 | adantr 482 |
. . 3
โข
(((((๐ด โ
โค โง ๐ต โ
โค) โง (๐ถ โ
โ0 โง ๐ท
โ โ0)) โง ๐ถ โค ๐ท) โง (๐ด / (2โ๐ถ)) โค (๐ต / (2โ๐ท))) โ (๐ต / (2โ๐ท)) โ โ) |
115 | 67 | adantr 482 |
. . 3
โข
(((((๐ด โ
โค โง ๐ต โ
โค) โง (๐ถ โ
โ0 โง ๐ท
โ โ0)) โง ๐ถ โค ๐ท) โง (๐ด / (2โ๐ถ)) โค (๐ต / (2โ๐ท))) โ ((๐ด + 1) / (2โ๐ถ)) โ โ) |
116 | 105, 113,
114, 115 | ltlecasei 11271 |
. 2
โข
(((((๐ด โ
โค โง ๐ต โ
โค) โง (๐ถ โ
โ0 โง ๐ท
โ โ0)) โง ๐ถ โค ๐ท) โง (๐ด / (2โ๐ถ)) โค (๐ต / (2โ๐ท))) โ (([,]โ(๐ด๐น๐ถ)) โ ([,]โ(๐ต๐น๐ท)) โจ ([,]โ(๐ต๐น๐ท)) โ ([,]โ(๐ด๐น๐ถ)) โจ (((,)โ(๐ด๐น๐ถ)) โฉ ((,)โ(๐ต๐น๐ท))) = โ
)) |
117 | 75, 116, 60, 50 | ltlecasei 11271 |
1
โข ((((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0
โง ๐ท โ
โ0)) โง ๐ถ โค ๐ท) โ (([,]โ(๐ด๐น๐ถ)) โ ([,]โ(๐ต๐น๐ท)) โจ ([,]โ(๐ต๐น๐ท)) โ ([,]โ(๐ด๐น๐ถ)) โจ (((,)โ(๐ด๐น๐ถ)) โฉ ((,)โ(๐ต๐น๐ท))) = โ
)) |