Step | Hyp | Ref
| Expression |
1 | | simpl 109 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ+)
โ ๐ด โ
โ) |
2 | 1 | recld 10946 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ+)
โ (โโ๐ด)
โ โ) |
3 | | simpr 110 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ+)
โ ๐ต โ
โ+) |
4 | 3 | rphalfcld 9708 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ+)
โ (๐ต / 2) โ
โ+) |
5 | | qdenre 11210 |
. . 3
โข
(((โโ๐ด)
โ โ โง (๐ต /
2) โ โ+) โ โ๐ข โ โ (absโ(๐ข โ (โโ๐ด))) < (๐ต / 2)) |
6 | 2, 4, 5 | syl2anc 411 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ+)
โ โ๐ข โ
โ (absโ(๐ข
โ (โโ๐ด)))
< (๐ต /
2)) |
7 | | simpll 527 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โ ๐ด โ
โ) |
8 | 7 | imcld 10947 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โ
(โโ๐ด) โ
โ) |
9 | 4 | adantr 276 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โ (๐ต / 2) โ
โ+) |
10 | | qdenre 11210 |
. . . 4
โข
(((โโ๐ด)
โ โ โง (๐ต /
2) โ โ+) โ โ๐ฃ โ โ (absโ(๐ฃ โ (โโ๐ด))) < (๐ต / 2)) |
11 | 8, 9, 10 | syl2anc 411 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โ
โ๐ฃ โ โ
(absโ(๐ฃ โ
(โโ๐ด))) <
(๐ต / 2)) |
12 | | qcn 9633 |
. . . . . . . 8
โข (๐ข โ โ โ ๐ข โ
โ) |
13 | 12 | ad2antrl 490 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โ ๐ข โ
โ) |
14 | 13 | adantr 276 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โง (๐ฃ โ โ โง
(absโ(๐ฃ โ
(โโ๐ด))) <
(๐ต / 2))) โ ๐ข โ
โ) |
15 | | ax-icn 7905 |
. . . . . . . 8
โข i โ
โ |
16 | 15 | a1i 9 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โง (๐ฃ โ โ โง
(absโ(๐ฃ โ
(โโ๐ด))) <
(๐ต / 2))) โ i โ
โ) |
17 | | qcn 9633 |
. . . . . . . 8
โข (๐ฃ โ โ โ ๐ฃ โ
โ) |
18 | 17 | ad2antrl 490 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โง (๐ฃ โ โ โง
(absโ(๐ฃ โ
(โโ๐ด))) <
(๐ต / 2))) โ ๐ฃ โ
โ) |
19 | 16, 18 | mulcld 7977 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โง (๐ฃ โ โ โง
(absโ(๐ฃ โ
(โโ๐ด))) <
(๐ต / 2))) โ (i
ยท ๐ฃ) โ
โ) |
20 | 14, 19 | addcld 7976 |
. . . . 5
โข ((((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โง (๐ฃ โ โ โง
(absโ(๐ฃ โ
(โโ๐ด))) <
(๐ต / 2))) โ (๐ข + (i ยท ๐ฃ)) โ
โ) |
21 | | qre 9624 |
. . . . . . . . . 10
โข (๐ข โ โ โ ๐ข โ
โ) |
22 | 21 | ad2antrl 490 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โ ๐ข โ
โ) |
23 | 22 | adantr 276 |
. . . . . . . 8
โข ((((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โง (๐ฃ โ โ โง
(absโ(๐ฃ โ
(โโ๐ด))) <
(๐ต / 2))) โ ๐ข โ
โ) |
24 | | qre 9624 |
. . . . . . . . 9
โข (๐ฃ โ โ โ ๐ฃ โ
โ) |
25 | 24 | ad2antrl 490 |
. . . . . . . 8
โข ((((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โง (๐ฃ โ โ โง
(absโ(๐ฃ โ
(โโ๐ด))) <
(๐ต / 2))) โ ๐ฃ โ
โ) |
26 | 23, 25 | crred 10984 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โง (๐ฃ โ โ โง
(absโ(๐ฃ โ
(โโ๐ด))) <
(๐ต / 2))) โ
(โโ(๐ข + (i
ยท ๐ฃ))) = ๐ข) |
27 | | simplrl 535 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โง (๐ฃ โ โ โง
(absโ(๐ฃ โ
(โโ๐ด))) <
(๐ต / 2))) โ ๐ข โ
โ) |
28 | 26, 27 | eqeltrd 2254 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โง (๐ฃ โ โ โง
(absโ(๐ฃ โ
(โโ๐ด))) <
(๐ต / 2))) โ
(โโ(๐ข + (i
ยท ๐ฃ))) โ
โ) |
29 | 23, 25 | crimd 10985 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โง (๐ฃ โ โ โง
(absโ(๐ฃ โ
(โโ๐ด))) <
(๐ต / 2))) โ
(โโ(๐ข + (i
ยท ๐ฃ))) = ๐ฃ) |
30 | | simprl 529 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โง (๐ฃ โ โ โง
(absโ(๐ฃ โ
(โโ๐ด))) <
(๐ต / 2))) โ ๐ฃ โ
โ) |
31 | 29, 30 | eqeltrd 2254 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โง (๐ฃ โ โ โง
(absโ(๐ฃ โ
(โโ๐ด))) <
(๐ต / 2))) โ
(โโ(๐ข + (i
ยท ๐ฃ))) โ
โ) |
32 | 28, 31 | jca 306 |
. . . . 5
โข ((((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โง (๐ฃ โ โ โง
(absโ(๐ฃ โ
(โโ๐ด))) <
(๐ต / 2))) โ
((โโ(๐ข + (i
ยท ๐ฃ))) โ
โ โง (โโ(๐ข + (i ยท ๐ฃ))) โ โ)) |
33 | | fveq2 5515 |
. . . . . . . 8
โข (๐ง = (๐ข + (i ยท ๐ฃ)) โ (โโ๐ง) = (โโ(๐ข + (i ยท ๐ฃ)))) |
34 | 33 | eleq1d 2246 |
. . . . . . 7
โข (๐ง = (๐ข + (i ยท ๐ฃ)) โ ((โโ๐ง) โ โ โ (โโ(๐ข + (i ยท ๐ฃ))) โ
โ)) |
35 | | fveq2 5515 |
. . . . . . . 8
โข (๐ง = (๐ข + (i ยท ๐ฃ)) โ (โโ๐ง) = (โโ(๐ข + (i ยท ๐ฃ)))) |
36 | 35 | eleq1d 2246 |
. . . . . . 7
โข (๐ง = (๐ข + (i ยท ๐ฃ)) โ ((โโ๐ง) โ โ โ (โโ(๐ข + (i ยท ๐ฃ))) โ
โ)) |
37 | 34, 36 | anbi12d 473 |
. . . . . 6
โข (๐ง = (๐ข + (i ยท ๐ฃ)) โ (((โโ๐ง) โ โ โง (โโ๐ง) โ โ) โ
((โโ(๐ข + (i
ยท ๐ฃ))) โ
โ โง (โโ(๐ข + (i ยท ๐ฃ))) โ โ))) |
38 | | qdencn.q |
. . . . . 6
โข ๐ = {๐ง โ โ โฃ ((โโ๐ง) โ โ โง
(โโ๐ง) โ
โ)} |
39 | 37, 38 | elrab2 2896 |
. . . . 5
โข ((๐ข + (i ยท ๐ฃ)) โ ๐ โ ((๐ข + (i ยท ๐ฃ)) โ โ โง ((โโ(๐ข + (i ยท ๐ฃ))) โ โ โง
(โโ(๐ข + (i
ยท ๐ฃ))) โ
โ))) |
40 | 20, 32, 39 | sylanbrc 417 |
. . . 4
โข ((((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โง (๐ฃ โ โ โง
(absโ(๐ฃ โ
(โโ๐ด))) <
(๐ต / 2))) โ (๐ข + (i ยท ๐ฃ)) โ ๐) |
41 | 7 | adantr 276 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โง (๐ฃ โ โ โง
(absโ(๐ฃ โ
(โโ๐ด))) <
(๐ต / 2))) โ ๐ด โ
โ) |
42 | 20, 41 | subcld 8267 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โง (๐ฃ โ โ โง
(absโ(๐ฃ โ
(โโ๐ด))) <
(๐ต / 2))) โ ((๐ข + (i ยท ๐ฃ)) โ ๐ด) โ โ) |
43 | 42 | abscld 11189 |
. . . . 5
โข ((((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โง (๐ฃ โ โ โง
(absโ(๐ฃ โ
(โโ๐ด))) <
(๐ต / 2))) โ
(absโ((๐ข + (i
ยท ๐ฃ)) โ ๐ด)) โ
โ) |
44 | 2 | ad2antrr 488 |
. . . . . . . . 9
โข ((((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โง (๐ฃ โ โ โง
(absโ(๐ฃ โ
(โโ๐ด))) <
(๐ต / 2))) โ
(โโ๐ด) โ
โ) |
45 | 44 | recnd 7985 |
. . . . . . . 8
โข ((((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โง (๐ฃ โ โ โง
(absโ(๐ฃ โ
(โโ๐ด))) <
(๐ต / 2))) โ
(โโ๐ด) โ
โ) |
46 | 14, 45 | subcld 8267 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โง (๐ฃ โ โ โง
(absโ(๐ฃ โ
(โโ๐ด))) <
(๐ต / 2))) โ (๐ข โ (โโ๐ด)) โ
โ) |
47 | 46 | abscld 11189 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โง (๐ฃ โ โ โง
(absโ(๐ฃ โ
(โโ๐ด))) <
(๐ต / 2))) โ
(absโ(๐ข โ
(โโ๐ด))) โ
โ) |
48 | 8 | adantr 276 |
. . . . . . . . 9
โข ((((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โง (๐ฃ โ โ โง
(absโ(๐ฃ โ
(โโ๐ด))) <
(๐ต / 2))) โ
(โโ๐ด) โ
โ) |
49 | 48 | recnd 7985 |
. . . . . . . 8
โข ((((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โง (๐ฃ โ โ โง
(absโ(๐ฃ โ
(โโ๐ด))) <
(๐ต / 2))) โ
(โโ๐ด) โ
โ) |
50 | 18, 49 | subcld 8267 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โง (๐ฃ โ โ โง
(absโ(๐ฃ โ
(โโ๐ด))) <
(๐ต / 2))) โ (๐ฃ โ (โโ๐ด)) โ
โ) |
51 | 50 | abscld 11189 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โง (๐ฃ โ โ โง
(absโ(๐ฃ โ
(โโ๐ด))) <
(๐ต / 2))) โ
(absโ(๐ฃ โ
(โโ๐ด))) โ
โ) |
52 | 47, 51 | readdcld 7986 |
. . . . 5
โข ((((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โง (๐ฃ โ โ โง
(absโ(๐ฃ โ
(โโ๐ด))) <
(๐ต / 2))) โ
((absโ(๐ข โ
(โโ๐ด))) +
(absโ(๐ฃ โ
(โโ๐ด)))) โ
โ) |
53 | 3 | ad2antrr 488 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โง (๐ฃ โ โ โง
(absโ(๐ฃ โ
(โโ๐ด))) <
(๐ต / 2))) โ ๐ต โ
โ+) |
54 | 53 | rpred 9695 |
. . . . 5
โข ((((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โง (๐ฃ โ โ โง
(absโ(๐ฃ โ
(โโ๐ด))) <
(๐ต / 2))) โ ๐ต โ
โ) |
55 | 1 | replimd 10949 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ต โ โ+)
โ ๐ด =
((โโ๐ด) + (i
ยท (โโ๐ด)))) |
56 | 55 | oveq2d 5890 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ+)
โ ((๐ข + (i ยท
๐ฃ)) โ ๐ด) = ((๐ข + (i ยท ๐ฃ)) โ ((โโ๐ด) + (i ยท (โโ๐ด))))) |
57 | 56 | ad2antrr 488 |
. . . . . . . . 9
โข ((((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โง (๐ฃ โ โ โง
(absโ(๐ฃ โ
(โโ๐ด))) <
(๐ต / 2))) โ ((๐ข + (i ยท ๐ฃ)) โ ๐ด) = ((๐ข + (i ยท ๐ฃ)) โ ((โโ๐ด) + (i ยท (โโ๐ด))))) |
58 | 16, 49 | mulcld 7977 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โง (๐ฃ โ โ โง
(absโ(๐ฃ โ
(โโ๐ด))) <
(๐ต / 2))) โ (i
ยท (โโ๐ด))
โ โ) |
59 | 14, 19, 45, 58 | addsub4d 8314 |
. . . . . . . . 9
โข ((((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โง (๐ฃ โ โ โง
(absโ(๐ฃ โ
(โโ๐ด))) <
(๐ต / 2))) โ ((๐ข + (i ยท ๐ฃ)) โ ((โโ๐ด) + (i ยท
(โโ๐ด)))) =
((๐ข โ
(โโ๐ด)) + ((i
ยท ๐ฃ) โ (i
ยท (โโ๐ด))))) |
60 | 57, 59 | eqtrd 2210 |
. . . . . . . 8
โข ((((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โง (๐ฃ โ โ โง
(absโ(๐ฃ โ
(โโ๐ด))) <
(๐ต / 2))) โ ((๐ข + (i ยท ๐ฃ)) โ ๐ด) = ((๐ข โ (โโ๐ด)) + ((i ยท ๐ฃ) โ (i ยท (โโ๐ด))))) |
61 | 60 | fveq2d 5519 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โง (๐ฃ โ โ โง
(absโ(๐ฃ โ
(โโ๐ด))) <
(๐ต / 2))) โ
(absโ((๐ข + (i
ยท ๐ฃ)) โ ๐ด)) = (absโ((๐ข โ (โโ๐ด)) + ((i ยท ๐ฃ) โ (i ยท
(โโ๐ด)))))) |
62 | 19, 58 | subcld 8267 |
. . . . . . . 8
โข ((((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โง (๐ฃ โ โ โง
(absโ(๐ฃ โ
(โโ๐ด))) <
(๐ต / 2))) โ ((i
ยท ๐ฃ) โ (i
ยท (โโ๐ด))) โ โ) |
63 | 46, 62 | abstrid 11204 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โง (๐ฃ โ โ โง
(absโ(๐ฃ โ
(โโ๐ด))) <
(๐ต / 2))) โ
(absโ((๐ข โ
(โโ๐ด)) + ((i
ยท ๐ฃ) โ (i
ยท (โโ๐ด))))) โค ((absโ(๐ข โ (โโ๐ด))) + (absโ((i ยท ๐ฃ) โ (i ยท
(โโ๐ด)))))) |
64 | 61, 63 | eqbrtrd 4025 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โง (๐ฃ โ โ โง
(absโ(๐ฃ โ
(โโ๐ด))) <
(๐ต / 2))) โ
(absโ((๐ข + (i
ยท ๐ฃ)) โ ๐ด)) โค ((absโ(๐ข โ (โโ๐ด))) + (absโ((i ยท
๐ฃ) โ (i ยท
(โโ๐ด)))))) |
65 | 16, 50 | absmuld 11202 |
. . . . . . . 8
โข ((((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โง (๐ฃ โ โ โง
(absโ(๐ฃ โ
(โโ๐ด))) <
(๐ต / 2))) โ
(absโ(i ยท (๐ฃ
โ (โโ๐ด)))) = ((absโi) ยท
(absโ(๐ฃ โ
(โโ๐ด))))) |
66 | 16, 18, 49 | subdid 8370 |
. . . . . . . . 9
โข ((((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โง (๐ฃ โ โ โง
(absโ(๐ฃ โ
(โโ๐ด))) <
(๐ต / 2))) โ (i
ยท (๐ฃ โ
(โโ๐ด))) = ((i
ยท ๐ฃ) โ (i
ยท (โโ๐ด)))) |
67 | 66 | fveq2d 5519 |
. . . . . . . 8
โข ((((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โง (๐ฃ โ โ โง
(absโ(๐ฃ โ
(โโ๐ด))) <
(๐ต / 2))) โ
(absโ(i ยท (๐ฃ
โ (โโ๐ด)))) = (absโ((i ยท ๐ฃ) โ (i ยท
(โโ๐ด))))) |
68 | | absi 11067 |
. . . . . . . . . 10
โข
(absโi) = 1 |
69 | 68 | oveq1i 5884 |
. . . . . . . . 9
โข
((absโi) ยท (absโ(๐ฃ โ (โโ๐ด)))) = (1 ยท (absโ(๐ฃ โ (โโ๐ด)))) |
70 | 51 | recnd 7985 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โง (๐ฃ โ โ โง
(absโ(๐ฃ โ
(โโ๐ด))) <
(๐ต / 2))) โ
(absโ(๐ฃ โ
(โโ๐ด))) โ
โ) |
71 | 70 | mulid2d 7975 |
. . . . . . . . 9
โข ((((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โง (๐ฃ โ โ โง
(absโ(๐ฃ โ
(โโ๐ด))) <
(๐ต / 2))) โ (1
ยท (absโ(๐ฃ
โ (โโ๐ด)))) = (absโ(๐ฃ โ (โโ๐ด)))) |
72 | 69, 71 | eqtrid 2222 |
. . . . . . . 8
โข ((((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โง (๐ฃ โ โ โง
(absโ(๐ฃ โ
(โโ๐ด))) <
(๐ต / 2))) โ
((absโi) ยท (absโ(๐ฃ โ (โโ๐ด)))) = (absโ(๐ฃ โ (โโ๐ด)))) |
73 | 65, 67, 72 | 3eqtr3d 2218 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โง (๐ฃ โ โ โง
(absโ(๐ฃ โ
(โโ๐ด))) <
(๐ต / 2))) โ
(absโ((i ยท ๐ฃ)
โ (i ยท (โโ๐ด)))) = (absโ(๐ฃ โ (โโ๐ด)))) |
74 | 73 | oveq2d 5890 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โง (๐ฃ โ โ โง
(absโ(๐ฃ โ
(โโ๐ด))) <
(๐ต / 2))) โ
((absโ(๐ข โ
(โโ๐ด))) +
(absโ((i ยท ๐ฃ)
โ (i ยท (โโ๐ด))))) = ((absโ(๐ข โ (โโ๐ด))) + (absโ(๐ฃ โ (โโ๐ด))))) |
75 | 64, 74 | breqtrd 4029 |
. . . . 5
โข ((((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โง (๐ฃ โ โ โง
(absโ(๐ฃ โ
(โโ๐ด))) <
(๐ต / 2))) โ
(absโ((๐ข + (i
ยท ๐ฃ)) โ ๐ด)) โค ((absโ(๐ข โ (โโ๐ด))) + (absโ(๐ฃ โ (โโ๐ด))))) |
76 | | simplrr 536 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โง (๐ฃ โ โ โง
(absโ(๐ฃ โ
(โโ๐ด))) <
(๐ต / 2))) โ
(absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2)) |
77 | | simprr 531 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โง (๐ฃ โ โ โง
(absโ(๐ฃ โ
(โโ๐ด))) <
(๐ต / 2))) โ
(absโ(๐ฃ โ
(โโ๐ด))) <
(๐ต / 2)) |
78 | 47, 51, 54, 76, 77 | lt2halvesd 9165 |
. . . . 5
โข ((((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โง (๐ฃ โ โ โง
(absโ(๐ฃ โ
(โโ๐ด))) <
(๐ต / 2))) โ
((absโ(๐ข โ
(โโ๐ด))) +
(absโ(๐ฃ โ
(โโ๐ด)))) <
๐ต) |
79 | 43, 52, 54, 75, 78 | lelttrd 8081 |
. . . 4
โข ((((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โง (๐ฃ โ โ โง
(absโ(๐ฃ โ
(โโ๐ด))) <
(๐ต / 2))) โ
(absโ((๐ข + (i
ยท ๐ฃ)) โ ๐ด)) < ๐ต) |
80 | | oveq1 5881 |
. . . . . . 7
โข (๐ฅ = (๐ข + (i ยท ๐ฃ)) โ (๐ฅ โ ๐ด) = ((๐ข + (i ยท ๐ฃ)) โ ๐ด)) |
81 | 80 | fveq2d 5519 |
. . . . . 6
โข (๐ฅ = (๐ข + (i ยท ๐ฃ)) โ (absโ(๐ฅ โ ๐ด)) = (absโ((๐ข + (i ยท ๐ฃ)) โ ๐ด))) |
82 | 81 | breq1d 4013 |
. . . . 5
โข (๐ฅ = (๐ข + (i ยท ๐ฃ)) โ ((absโ(๐ฅ โ ๐ด)) < ๐ต โ (absโ((๐ข + (i ยท ๐ฃ)) โ ๐ด)) < ๐ต)) |
83 | 82 | rspcev 2841 |
. . . 4
โข (((๐ข + (i ยท ๐ฃ)) โ ๐ โง (absโ((๐ข + (i ยท ๐ฃ)) โ ๐ด)) < ๐ต) โ โ๐ฅ โ ๐ (absโ(๐ฅ โ ๐ด)) < ๐ต) |
84 | 40, 79, 83 | syl2anc 411 |
. . 3
โข ((((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โง (๐ฃ โ โ โง
(absโ(๐ฃ โ
(โโ๐ด))) <
(๐ต / 2))) โ
โ๐ฅ โ ๐ (absโ(๐ฅ โ ๐ด)) < ๐ต) |
85 | 11, 84 | rexlimddv 2599 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ข โ โ
โง (absโ(๐ข โ
(โโ๐ด))) <
(๐ต / 2))) โ
โ๐ฅ โ ๐ (absโ(๐ฅ โ ๐ด)) < ๐ต) |
86 | 6, 85 | rexlimddv 2599 |
1
โข ((๐ด โ โ โง ๐ต โ โ+)
โ โ๐ฅ โ
๐ (absโ(๐ฅ โ ๐ด)) < ๐ต) |