Step | Hyp | Ref
| Expression |
1 | | knoppcnlem4.f |
. . . 4
โข ๐น = (๐ฆ โ โ โฆ (๐ โ โ0 โฆ ((๐ถโ๐) ยท (๐โ(((2 ยท ๐)โ๐) ยท ๐ฆ))))) |
2 | | knoppcnlem4.2 |
. . . 4
โข (๐ โ ๐ด โ โ) |
3 | | knoppcnlem4.3 |
. . . 4
โข (๐ โ ๐ โ
โ0) |
4 | 1, 2, 3 | knoppcnlem1 35358 |
. . 3
โข (๐ โ ((๐นโ๐ด)โ๐) = ((๐ถโ๐) ยท (๐โ(((2 ยท ๐)โ๐) ยท ๐ด)))) |
5 | 4 | fveq2d 6893 |
. 2
โข (๐ โ (absโ((๐นโ๐ด)โ๐)) = (absโ((๐ถโ๐) ยท (๐โ(((2 ยท ๐)โ๐) ยท ๐ด))))) |
6 | | knoppcnlem4.1 |
. . . . . . . 8
โข (๐ โ ๐ถ โ โ) |
7 | 6 | recnd 11239 |
. . . . . . 7
โข (๐ โ ๐ถ โ โ) |
8 | 7, 3 | expcld 14108 |
. . . . . 6
โข (๐ โ (๐ถโ๐) โ โ) |
9 | | knoppcnlem4.t |
. . . . . . . 8
โข ๐ = (๐ฅ โ โ โฆ
(absโ((โโ(๐ฅ + (1 / 2))) โ ๐ฅ))) |
10 | | 2re 12283 |
. . . . . . . . . . . 12
โข 2 โ
โ |
11 | 10 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ 2 โ
โ) |
12 | | knoppcnlem4.n |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ โ) |
13 | | nnre 12216 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ๐ โ
โ) |
14 | 12, 13 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ โ) |
15 | 11, 14 | remulcld 11241 |
. . . . . . . . . 10
โข (๐ โ (2 ยท ๐) โ
โ) |
16 | 15, 3 | reexpcld 14125 |
. . . . . . . . 9
โข (๐ โ ((2 ยท ๐)โ๐) โ โ) |
17 | 16, 2 | remulcld 11241 |
. . . . . . . 8
โข (๐ โ (((2 ยท ๐)โ๐) ยท ๐ด) โ โ) |
18 | 9, 17 | dnicld2 35338 |
. . . . . . 7
โข (๐ โ (๐โ(((2 ยท ๐)โ๐) ยท ๐ด)) โ โ) |
19 | 18 | recnd 11239 |
. . . . . 6
โข (๐ โ (๐โ(((2 ยท ๐)โ๐) ยท ๐ด)) โ โ) |
20 | 8, 19 | absmuld 15398 |
. . . . 5
โข (๐ โ (absโ((๐ถโ๐) ยท (๐โ(((2 ยท ๐)โ๐) ยท ๐ด)))) = ((absโ(๐ถโ๐)) ยท (absโ(๐โ(((2 ยท ๐)โ๐) ยท ๐ด))))) |
21 | 7, 3 | absexpd 15396 |
. . . . . 6
โข (๐ โ (absโ(๐ถโ๐)) = ((absโ๐ถ)โ๐)) |
22 | 21 | oveq1d 7421 |
. . . . 5
โข (๐ โ ((absโ(๐ถโ๐)) ยท (absโ(๐โ(((2 ยท ๐)โ๐) ยท ๐ด)))) = (((absโ๐ถ)โ๐) ยท (absโ(๐โ(((2 ยท ๐)โ๐) ยท ๐ด))))) |
23 | 20, 22 | eqtrd 2773 |
. . . 4
โข (๐ โ (absโ((๐ถโ๐) ยท (๐โ(((2 ยท ๐)โ๐) ยท ๐ด)))) = (((absโ๐ถ)โ๐) ยท (absโ(๐โ(((2 ยท ๐)โ๐) ยท ๐ด))))) |
24 | 19 | abscld 15380 |
. . . . . 6
โข (๐ โ (absโ(๐โ(((2 ยท ๐)โ๐) ยท ๐ด))) โ โ) |
25 | | 1red 11212 |
. . . . . 6
โข (๐ โ 1 โ
โ) |
26 | 7 | abscld 15380 |
. . . . . . 7
โข (๐ โ (absโ๐ถ) โ
โ) |
27 | 26, 3 | reexpcld 14125 |
. . . . . 6
โข (๐ โ ((absโ๐ถ)โ๐) โ โ) |
28 | 7 | absge0d 15388 |
. . . . . . 7
โข (๐ โ 0 โค (absโ๐ถ)) |
29 | 26, 3, 28 | expge0d 14126 |
. . . . . 6
โข (๐ โ 0 โค ((absโ๐ถ)โ๐)) |
30 | 9 | dnival 35336 |
. . . . . . . . . 10
โข ((((2
ยท ๐)โ๐) ยท ๐ด) โ โ โ (๐โ(((2 ยท ๐)โ๐) ยท ๐ด)) = (absโ((โโ((((2
ยท ๐)โ๐) ยท ๐ด) + (1 / 2))) โ (((2 ยท ๐)โ๐) ยท ๐ด)))) |
31 | 17, 30 | syl 17 |
. . . . . . . . 9
โข (๐ โ (๐โ(((2 ยท ๐)โ๐) ยท ๐ด)) = (absโ((โโ((((2
ยท ๐)โ๐) ยท ๐ด) + (1 / 2))) โ (((2 ยท ๐)โ๐) ยท ๐ด)))) |
32 | 31 | fveq2d 6893 |
. . . . . . . 8
โข (๐ โ (absโ(๐โ(((2 ยท ๐)โ๐) ยท ๐ด))) =
(absโ(absโ((โโ((((2 ยท ๐)โ๐) ยท ๐ด) + (1 / 2))) โ (((2 ยท ๐)โ๐) ยท ๐ด))))) |
33 | | halfre 12423 |
. . . . . . . . . . . . . 14
โข (1 / 2)
โ โ |
34 | 33 | a1i 11 |
. . . . . . . . . . . . 13
โข (๐ โ (1 / 2) โ
โ) |
35 | 17, 34 | readdcld 11240 |
. . . . . . . . . . . 12
โข (๐ โ ((((2 ยท ๐)โ๐) ยท ๐ด) + (1 / 2)) โ
โ) |
36 | | reflcl 13758 |
. . . . . . . . . . . 12
โข (((((2
ยท ๐)โ๐) ยท ๐ด) + (1 / 2)) โ โ โ
(โโ((((2 ยท ๐)โ๐) ยท ๐ด) + (1 / 2))) โ
โ) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ (โโ((((2
ยท ๐)โ๐) ยท ๐ด) + (1 / 2))) โ
โ) |
38 | 37, 17 | resubcld 11639 |
. . . . . . . . . 10
โข (๐ โ ((โโ((((2
ยท ๐)โ๐) ยท ๐ด) + (1 / 2))) โ (((2 ยท ๐)โ๐) ยท ๐ด)) โ โ) |
39 | 38 | recnd 11239 |
. . . . . . . . 9
โข (๐ โ ((โโ((((2
ยท ๐)โ๐) ยท ๐ด) + (1 / 2))) โ (((2 ยท ๐)โ๐) ยท ๐ด)) โ โ) |
40 | | absidm 15267 |
. . . . . . . . 9
โข
(((โโ((((2 ยท ๐)โ๐) ยท ๐ด) + (1 / 2))) โ (((2 ยท ๐)โ๐) ยท ๐ด)) โ โ โ
(absโ(absโ((โโ((((2 ยท ๐)โ๐) ยท ๐ด) + (1 / 2))) โ (((2 ยท ๐)โ๐) ยท ๐ด)))) = (absโ((โโ((((2
ยท ๐)โ๐) ยท ๐ด) + (1 / 2))) โ (((2 ยท ๐)โ๐) ยท ๐ด)))) |
41 | 39, 40 | syl 17 |
. . . . . . . 8
โข (๐ โ
(absโ(absโ((โโ((((2 ยท ๐)โ๐) ยท ๐ด) + (1 / 2))) โ (((2 ยท ๐)โ๐) ยท ๐ด)))) = (absโ((โโ((((2
ยท ๐)โ๐) ยท ๐ด) + (1 / 2))) โ (((2 ยท ๐)โ๐) ยท ๐ด)))) |
42 | 32, 41 | eqtrd 2773 |
. . . . . . 7
โข (๐ โ (absโ(๐โ(((2 ยท ๐)โ๐) ยท ๐ด))) = (absโ((โโ((((2
ยท ๐)โ๐) ยท ๐ด) + (1 / 2))) โ (((2 ยท ๐)โ๐) ยท ๐ด)))) |
43 | 31, 18 | eqeltrrd 2835 |
. . . . . . . 8
โข (๐ โ
(absโ((โโ((((2 ยท ๐)โ๐) ยท ๐ด) + (1 / 2))) โ (((2 ยท ๐)โ๐) ยท ๐ด))) โ โ) |
44 | | rddif 15284 |
. . . . . . . . 9
โข ((((2
ยท ๐)โ๐) ยท ๐ด) โ โ โ
(absโ((โโ((((2 ยท ๐)โ๐) ยท ๐ด) + (1 / 2))) โ (((2 ยท ๐)โ๐) ยท ๐ด))) โค (1 / 2)) |
45 | 17, 44 | syl 17 |
. . . . . . . 8
โข (๐ โ
(absโ((โโ((((2 ยท ๐)โ๐) ยท ๐ด) + (1 / 2))) โ (((2 ยท ๐)โ๐) ยท ๐ด))) โค (1 / 2)) |
46 | | halflt1 12427 |
. . . . . . . . . 10
โข (1 / 2)
< 1 |
47 | | 1re 11211 |
. . . . . . . . . . 11
โข 1 โ
โ |
48 | 33, 47 | ltlei 11333 |
. . . . . . . . . 10
โข ((1 / 2)
< 1 โ (1 / 2) โค 1) |
49 | 46, 48 | ax-mp 5 |
. . . . . . . . 9
โข (1 / 2)
โค 1 |
50 | 49 | a1i 11 |
. . . . . . . 8
โข (๐ โ (1 / 2) โค
1) |
51 | 43, 34, 25, 45, 50 | letrd 11368 |
. . . . . . 7
โข (๐ โ
(absโ((โโ((((2 ยท ๐)โ๐) ยท ๐ด) + (1 / 2))) โ (((2 ยท ๐)โ๐) ยท ๐ด))) โค 1) |
52 | 42, 51 | eqbrtrd 5170 |
. . . . . 6
โข (๐ โ (absโ(๐โ(((2 ยท ๐)โ๐) ยท ๐ด))) โค 1) |
53 | 24, 25, 27, 29, 52 | lemul2ad 12151 |
. . . . 5
โข (๐ โ (((absโ๐ถ)โ๐) ยท (absโ(๐โ(((2 ยท ๐)โ๐) ยท ๐ด)))) โค (((absโ๐ถ)โ๐) ยท 1)) |
54 | | ax-1rid 11177 |
. . . . . 6
โข
(((absโ๐ถ)โ๐) โ โ โ (((absโ๐ถ)โ๐) ยท 1) = ((absโ๐ถ)โ๐)) |
55 | 27, 54 | syl 17 |
. . . . 5
โข (๐ โ (((absโ๐ถ)โ๐) ยท 1) = ((absโ๐ถ)โ๐)) |
56 | 53, 55 | breqtrd 5174 |
. . . 4
โข (๐ โ (((absโ๐ถ)โ๐) ยท (absโ(๐โ(((2 ยท ๐)โ๐) ยท ๐ด)))) โค ((absโ๐ถ)โ๐)) |
57 | 23, 56 | eqbrtrd 5170 |
. . 3
โข (๐ โ (absโ((๐ถโ๐) ยท (๐โ(((2 ยท ๐)โ๐) ยท ๐ด)))) โค ((absโ๐ถ)โ๐)) |
58 | | eqidd 2734 |
. . . . 5
โข (๐ โ (๐ โ โ0 โฆ
((absโ๐ถ)โ๐)) = (๐ โ โ0 โฆ
((absโ๐ถ)โ๐))) |
59 | | oveq2 7414 |
. . . . . 6
โข (๐ = ๐ โ ((absโ๐ถ)โ๐) = ((absโ๐ถ)โ๐)) |
60 | 59 | adantl 483 |
. . . . 5
โข ((๐ โง ๐ = ๐) โ ((absโ๐ถ)โ๐) = ((absโ๐ถ)โ๐)) |
61 | 58, 60, 3, 27 | fvmptd 7003 |
. . . 4
โข (๐ โ ((๐ โ โ0 โฆ
((absโ๐ถ)โ๐))โ๐) = ((absโ๐ถ)โ๐)) |
62 | 61 | eqcomd 2739 |
. . 3
โข (๐ โ ((absโ๐ถ)โ๐) = ((๐ โ โ0 โฆ
((absโ๐ถ)โ๐))โ๐)) |
63 | 57, 62 | breqtrd 5174 |
. 2
โข (๐ โ (absโ((๐ถโ๐) ยท (๐โ(((2 ยท ๐)โ๐) ยท ๐ด)))) โค ((๐ โ โ0 โฆ
((absโ๐ถ)โ๐))โ๐)) |
64 | 5, 63 | eqbrtrd 5170 |
1
โข (๐ โ (absโ((๐นโ๐ด)โ๐)) โค ((๐ โ โ0 โฆ
((absโ๐ถ)โ๐))โ๐)) |