Step | Hyp | Ref
| Expression |
1 | | knoppndvlem17.c |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ถ โ (-1(,)1)) |
2 | 1 | knoppndvlem3 35390 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ถ โ โ โง (absโ๐ถ) < 1)) |
3 | 2 | simpld 496 |
. . . . . . . . . . . 12
โข (๐ โ ๐ถ โ โ) |
4 | 3 | recnd 11242 |
. . . . . . . . . . 11
โข (๐ โ ๐ถ โ โ) |
5 | 4 | abscld 15383 |
. . . . . . . . . 10
โข (๐ โ (absโ๐ถ) โ
โ) |
6 | | knoppndvlem17.j |
. . . . . . . . . 10
โข (๐ โ ๐ฝ โ
โ0) |
7 | 5, 6 | reexpcld 14128 |
. . . . . . . . 9
โข (๐ โ ((absโ๐ถ)โ๐ฝ) โ โ) |
8 | | 2re 12286 |
. . . . . . . . . 10
โข 2 โ
โ |
9 | 8 | a1i 11 |
. . . . . . . . 9
โข (๐ โ 2 โ
โ) |
10 | | 2ne0 12316 |
. . . . . . . . . 10
โข 2 โ
0 |
11 | 10 | a1i 11 |
. . . . . . . . 9
โข (๐ โ 2 โ 0) |
12 | 7, 9, 11 | redivcld 12042 |
. . . . . . . 8
โข (๐ โ (((absโ๐ถ)โ๐ฝ) / 2) โ โ) |
13 | 12 | recnd 11242 |
. . . . . . 7
โข (๐ โ (((absโ๐ถ)โ๐ฝ) / 2) โ โ) |
14 | | 1red 11215 |
. . . . . . . . 9
โข (๐ โ 1 โ
โ) |
15 | | knoppndvlem17.n |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ โ โ) |
16 | 15 | nnred 12227 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ โ) |
17 | 9, 16 | remulcld 11244 |
. . . . . . . . . . . 12
โข (๐ โ (2 ยท ๐) โ
โ) |
18 | 17, 5 | remulcld 11244 |
. . . . . . . . . . 11
โข (๐ โ ((2 ยท ๐) ยท (absโ๐ถ)) โ
โ) |
19 | 18, 14 | resubcld 11642 |
. . . . . . . . . 10
โข (๐ โ (((2 ยท ๐) ยท (absโ๐ถ)) โ 1) โ
โ) |
20 | | 0red 11217 |
. . . . . . . . . . . . 13
โข (๐ โ 0 โ
โ) |
21 | | 0lt1 11736 |
. . . . . . . . . . . . . 14
โข 0 <
1 |
22 | 21 | a1i 11 |
. . . . . . . . . . . . 13
โข (๐ โ 0 < 1) |
23 | | knoppndvlem17.1 |
. . . . . . . . . . . . . . 15
โข (๐ โ 1 < (๐ ยท (absโ๐ถ))) |
24 | 1, 15, 23 | knoppndvlem12 35399 |
. . . . . . . . . . . . . 14
โข (๐ โ (((2 ยท ๐) ยท (absโ๐ถ)) โ 1 โง 1 < (((2
ยท ๐) ยท
(absโ๐ถ)) โ
1))) |
25 | 24 | simprd 497 |
. . . . . . . . . . . . 13
โข (๐ โ 1 < (((2 ยท ๐) ยท (absโ๐ถ)) โ 1)) |
26 | 20, 14, 19, 22, 25 | lttrd 11375 |
. . . . . . . . . . . 12
โข (๐ โ 0 < (((2 ยท ๐) ยท (absโ๐ถ)) โ 1)) |
27 | 19, 26 | jca 513 |
. . . . . . . . . . 11
โข (๐ โ ((((2 ยท ๐) ยท (absโ๐ถ)) โ 1) โ โ
โง 0 < (((2 ยท ๐) ยท (absโ๐ถ)) โ 1))) |
28 | | gt0ne0 11679 |
. . . . . . . . . . 11
โข (((((2
ยท ๐) ยท
(absโ๐ถ)) โ 1)
โ โ โง 0 < (((2 ยท ๐) ยท (absโ๐ถ)) โ 1)) โ (((2 ยท ๐) ยท (absโ๐ถ)) โ 1) โ
0) |
29 | 27, 28 | syl 17 |
. . . . . . . . . 10
โข (๐ โ (((2 ยท ๐) ยท (absโ๐ถ)) โ 1) โ
0) |
30 | 14, 19, 29 | redivcld 12042 |
. . . . . . . . 9
โข (๐ โ (1 / (((2 ยท ๐) ยท (absโ๐ถ)) โ 1)) โ
โ) |
31 | 14, 30 | resubcld 11642 |
. . . . . . . 8
โข (๐ โ (1 โ (1 / (((2
ยท ๐) ยท
(absโ๐ถ)) โ 1)))
โ โ) |
32 | 31 | recnd 11242 |
. . . . . . 7
โข (๐ โ (1 โ (1 / (((2
ยท ๐) ยท
(absโ๐ถ)) โ 1)))
โ โ) |
33 | 13, 32 | mulcomd 11235 |
. . . . . 6
โข (๐ โ ((((absโ๐ถ)โ๐ฝ) / 2) ยท (1 โ (1 / (((2
ยท ๐) ยท
(absโ๐ถ)) โ
1)))) = ((1 โ (1 / (((2 ยท ๐) ยท (absโ๐ถ)) โ 1))) ยท (((absโ๐ถ)โ๐ฝ) / 2))) |
34 | 33 | oveq1d 7424 |
. . . . 5
โข (๐ โ (((((absโ๐ถ)โ๐ฝ) / 2) ยท (1 โ (1 / (((2
ยท ๐) ยท
(absโ๐ถ)) โ
1)))) / (((2 ยท ๐)โ-๐ฝ) / 2)) = (((1 โ (1 / (((2 ยท
๐) ยท
(absโ๐ถ)) โ 1)))
ยท (((absโ๐ถ)โ๐ฝ) / 2)) / (((2 ยท ๐)โ-๐ฝ) / 2))) |
35 | | 2rp 12979 |
. . . . . . . . . . 11
โข 2 โ
โ+ |
36 | 35 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ 2 โ
โ+) |
37 | 15 | nnrpd 13014 |
. . . . . . . . . 10
โข (๐ โ ๐ โ
โ+) |
38 | 36, 37 | rpmulcld 13032 |
. . . . . . . . 9
โข (๐ โ (2 ยท ๐) โ
โ+) |
39 | 6 | nn0zd 12584 |
. . . . . . . . . 10
โข (๐ โ ๐ฝ โ โค) |
40 | 39 | znegcld 12668 |
. . . . . . . . 9
โข (๐ โ -๐ฝ โ โค) |
41 | 38, 40 | rpexpcld 14210 |
. . . . . . . 8
โข (๐ โ ((2 ยท ๐)โ-๐ฝ) โ
โ+) |
42 | 41 | rphalfcld 13028 |
. . . . . . 7
โข (๐ โ (((2 ยท ๐)โ-๐ฝ) / 2) โ
โ+) |
43 | 42 | rpcnd 13018 |
. . . . . 6
โข (๐ โ (((2 ยท ๐)โ-๐ฝ) / 2) โ โ) |
44 | 42 | rpne0d 13021 |
. . . . . 6
โข (๐ โ (((2 ยท ๐)โ-๐ฝ) / 2) โ 0) |
45 | 32, 13, 43, 44 | divassd 12025 |
. . . . 5
โข (๐ โ (((1 โ (1 / (((2
ยท ๐) ยท
(absโ๐ถ)) โ 1)))
ยท (((absโ๐ถ)โ๐ฝ) / 2)) / (((2 ยท ๐)โ-๐ฝ) / 2)) = ((1 โ (1 / (((2 ยท
๐) ยท
(absโ๐ถ)) โ 1)))
ยท ((((absโ๐ถ)โ๐ฝ) / 2) / (((2 ยท ๐)โ-๐ฝ) / 2)))) |
46 | 13, 43, 44 | divcld 11990 |
. . . . . . 7
โข (๐ โ ((((absโ๐ถ)โ๐ฝ) / 2) / (((2 ยท ๐)โ-๐ฝ) / 2)) โ โ) |
47 | 32, 46 | mulcomd 11235 |
. . . . . 6
โข (๐ โ ((1 โ (1 / (((2
ยท ๐) ยท
(absโ๐ถ)) โ 1)))
ยท ((((absโ๐ถ)โ๐ฝ) / 2) / (((2 ยท ๐)โ-๐ฝ) / 2))) = (((((absโ๐ถ)โ๐ฝ) / 2) / (((2 ยท ๐)โ-๐ฝ) / 2)) ยท (1 โ (1 / (((2
ยท ๐) ยท
(absโ๐ถ)) โ
1))))) |
48 | 7 | recnd 11242 |
. . . . . . . . 9
โข (๐ โ ((absโ๐ถ)โ๐ฝ) โ โ) |
49 | 41 | rpcnd 13018 |
. . . . . . . . 9
โข (๐ โ ((2 ยท ๐)โ-๐ฝ) โ โ) |
50 | 9 | recnd 11242 |
. . . . . . . . 9
โข (๐ โ 2 โ
โ) |
51 | 41 | rpne0d 13021 |
. . . . . . . . 9
โข (๐ โ ((2 ยท ๐)โ-๐ฝ) โ 0) |
52 | 48, 49, 50, 51, 11 | divcan7d 12018 |
. . . . . . . 8
โข (๐ โ ((((absโ๐ถ)โ๐ฝ) / 2) / (((2 ยท ๐)โ-๐ฝ) / 2)) = (((absโ๐ถ)โ๐ฝ) / ((2 ยท ๐)โ-๐ฝ))) |
53 | 17 | recnd 11242 |
. . . . . . . . . . 11
โข (๐ โ (2 ยท ๐) โ
โ) |
54 | 38 | rpne0d 13021 |
. . . . . . . . . . 11
โข (๐ โ (2 ยท ๐) โ 0) |
55 | 53, 54, 39 | expnegd 14118 |
. . . . . . . . . 10
โข (๐ โ ((2 ยท ๐)โ-๐ฝ) = (1 / ((2 ยท ๐)โ๐ฝ))) |
56 | 55 | oveq2d 7425 |
. . . . . . . . 9
โข (๐ โ (((absโ๐ถ)โ๐ฝ) / ((2 ยท ๐)โ-๐ฝ)) = (((absโ๐ถ)โ๐ฝ) / (1 / ((2 ยท ๐)โ๐ฝ)))) |
57 | | 1cnd 11209 |
. . . . . . . . . 10
โข (๐ โ 1 โ
โ) |
58 | 53, 6 | expcld 14111 |
. . . . . . . . . 10
โข (๐ โ ((2 ยท ๐)โ๐ฝ) โ โ) |
59 | 20, 22 | gtned 11349 |
. . . . . . . . . 10
โข (๐ โ 1 โ 0) |
60 | 53, 54, 39 | expne0d 14117 |
. . . . . . . . . 10
โข (๐ โ ((2 ยท ๐)โ๐ฝ) โ 0) |
61 | 48, 57, 58, 59, 60 | divdiv2d 12022 |
. . . . . . . . 9
โข (๐ โ (((absโ๐ถ)โ๐ฝ) / (1 / ((2 ยท ๐)โ๐ฝ))) = ((((absโ๐ถ)โ๐ฝ) ยท ((2 ยท ๐)โ๐ฝ)) / 1)) |
62 | 48, 58 | mulcld 11234 |
. . . . . . . . . . 11
โข (๐ โ (((absโ๐ถ)โ๐ฝ) ยท ((2 ยท ๐)โ๐ฝ)) โ โ) |
63 | 62 | div1d 11982 |
. . . . . . . . . 10
โข (๐ โ ((((absโ๐ถ)โ๐ฝ) ยท ((2 ยท ๐)โ๐ฝ)) / 1) = (((absโ๐ถ)โ๐ฝ) ยท ((2 ยท ๐)โ๐ฝ))) |
64 | 48, 58 | mulcomd 11235 |
. . . . . . . . . 10
โข (๐ โ (((absโ๐ถ)โ๐ฝ) ยท ((2 ยท ๐)โ๐ฝ)) = (((2 ยท ๐)โ๐ฝ) ยท ((absโ๐ถ)โ๐ฝ))) |
65 | 53, 54 | jca 513 |
. . . . . . . . . . . . 13
โข (๐ โ ((2 ยท ๐) โ โ โง (2
ยท ๐) โ
0)) |
66 | 5 | recnd 11242 |
. . . . . . . . . . . . . 14
โข (๐ โ (absโ๐ถ) โ
โ) |
67 | 1, 15, 23 | knoppndvlem13 35400 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ถ โ 0) |
68 | 4, 67 | absne0d 15394 |
. . . . . . . . . . . . . 14
โข (๐ โ (absโ๐ถ) โ 0) |
69 | 66, 68 | jca 513 |
. . . . . . . . . . . . 13
โข (๐ โ ((absโ๐ถ) โ โ โง
(absโ๐ถ) โ
0)) |
70 | 65, 69, 39 | 3jca 1129 |
. . . . . . . . . . . 12
โข (๐ โ (((2 ยท ๐) โ โ โง (2
ยท ๐) โ 0) โง
((absโ๐ถ) โ
โ โง (absโ๐ถ)
โ 0) โง ๐ฝ โ
โค)) |
71 | | mulexpz 14068 |
. . . . . . . . . . . 12
โข ((((2
ยท ๐) โ โ
โง (2 ยท ๐) โ
0) โง ((absโ๐ถ)
โ โ โง (absโ๐ถ) โ 0) โง ๐ฝ โ โค) โ (((2 ยท ๐) ยท (absโ๐ถ))โ๐ฝ) = (((2 ยท ๐)โ๐ฝ) ยท ((absโ๐ถ)โ๐ฝ))) |
72 | 70, 71 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ (((2 ยท ๐) ยท (absโ๐ถ))โ๐ฝ) = (((2 ยท ๐)โ๐ฝ) ยท ((absโ๐ถ)โ๐ฝ))) |
73 | 72 | eqcomd 2739 |
. . . . . . . . . 10
โข (๐ โ (((2 ยท ๐)โ๐ฝ) ยท ((absโ๐ถ)โ๐ฝ)) = (((2 ยท ๐) ยท (absโ๐ถ))โ๐ฝ)) |
74 | 63, 64, 73 | 3eqtrd 2777 |
. . . . . . . . 9
โข (๐ โ ((((absโ๐ถ)โ๐ฝ) ยท ((2 ยท ๐)โ๐ฝ)) / 1) = (((2 ยท ๐) ยท (absโ๐ถ))โ๐ฝ)) |
75 | 56, 61, 74 | 3eqtrd 2777 |
. . . . . . . 8
โข (๐ โ (((absโ๐ถ)โ๐ฝ) / ((2 ยท ๐)โ-๐ฝ)) = (((2 ยท ๐) ยท (absโ๐ถ))โ๐ฝ)) |
76 | 52, 75 | eqtrd 2773 |
. . . . . . 7
โข (๐ โ ((((absโ๐ถ)โ๐ฝ) / 2) / (((2 ยท ๐)โ-๐ฝ) / 2)) = (((2 ยท ๐) ยท (absโ๐ถ))โ๐ฝ)) |
77 | 76 | oveq1d 7424 |
. . . . . 6
โข (๐ โ (((((absโ๐ถ)โ๐ฝ) / 2) / (((2 ยท ๐)โ-๐ฝ) / 2)) ยท (1 โ (1 / (((2
ยท ๐) ยท
(absโ๐ถ)) โ
1)))) = ((((2 ยท ๐)
ยท (absโ๐ถ))โ๐ฝ) ยท (1 โ (1 / (((2 ยท
๐) ยท
(absโ๐ถ)) โ
1))))) |
78 | 47, 77 | eqtrd 2773 |
. . . . 5
โข (๐ โ ((1 โ (1 / (((2
ยท ๐) ยท
(absโ๐ถ)) โ 1)))
ยท ((((absโ๐ถ)โ๐ฝ) / 2) / (((2 ยท ๐)โ-๐ฝ) / 2))) = ((((2 ยท ๐) ยท (absโ๐ถ))โ๐ฝ) ยท (1 โ (1 / (((2 ยท
๐) ยท
(absโ๐ถ)) โ
1))))) |
79 | 34, 45, 78 | 3eqtrd 2777 |
. . . 4
โข (๐ โ (((((absโ๐ถ)โ๐ฝ) / 2) ยท (1 โ (1 / (((2
ยท ๐) ยท
(absโ๐ถ)) โ
1)))) / (((2 ยท ๐)โ-๐ฝ) / 2)) = ((((2 ยท ๐) ยท (absโ๐ถ))โ๐ฝ) ยท (1 โ (1 / (((2 ยท
๐) ยท
(absโ๐ถ)) โ
1))))) |
80 | 79 | eqcomd 2739 |
. . 3
โข (๐ โ ((((2 ยท ๐) ยท (absโ๐ถ))โ๐ฝ) ยท (1 โ (1 / (((2 ยท
๐) ยท
(absโ๐ถ)) โ
1)))) = (((((absโ๐ถ)โ๐ฝ) / 2) ยท (1 โ (1 / (((2
ยท ๐) ยท
(absโ๐ถ)) โ
1)))) / (((2 ยท ๐)โ-๐ฝ) / 2))) |
81 | 12, 31 | remulcld 11244 |
. . . 4
โข (๐ โ ((((absโ๐ถ)โ๐ฝ) / 2) ยท (1 โ (1 / (((2
ยท ๐) ยท
(absโ๐ถ)) โ
1)))) โ โ) |
82 | | knoppndvlem17.t |
. . . . . . 7
โข ๐ = (๐ฅ โ โ โฆ
(absโ((โโ(๐ฅ + (1 / 2))) โ ๐ฅ))) |
83 | | knoppndvlem17.f |
. . . . . . 7
โข ๐น = (๐ฆ โ โ โฆ (๐ โ โ0 โฆ ((๐ถโ๐) ยท (๐โ(((2 ยท ๐)โ๐) ยท ๐ฆ))))) |
84 | | knoppndvlem17.w |
. . . . . . 7
โข ๐ = (๐ค โ โ โฆ ฮฃ๐ โ โ0
((๐นโ๐ค)โ๐)) |
85 | | knoppndvlem17.b |
. . . . . . . . 9
โข ๐ต = ((((2 ยท ๐)โ-๐ฝ) / 2) ยท (๐ + 1)) |
86 | 85 | a1i 11 |
. . . . . . . 8
โข (๐ โ ๐ต = ((((2 ยท ๐)โ-๐ฝ) / 2) ยท (๐ + 1))) |
87 | | knoppndvlem17.m |
. . . . . . . . . 10
โข (๐ โ ๐ โ โค) |
88 | 87 | peano2zd 12669 |
. . . . . . . . 9
โข (๐ โ (๐ + 1) โ โค) |
89 | 15, 39, 88 | knoppndvlem1 35388 |
. . . . . . . 8
โข (๐ โ ((((2 ยท ๐)โ-๐ฝ) / 2) ยท (๐ + 1)) โ โ) |
90 | 86, 89 | eqeltrd 2834 |
. . . . . . 7
โข (๐ โ ๐ต โ โ) |
91 | 2 | simprd 497 |
. . . . . . 7
โข (๐ โ (absโ๐ถ) < 1) |
92 | 82, 83, 84, 90, 15, 3, 91 | knoppcld 35381 |
. . . . . 6
โข (๐ โ (๐โ๐ต) โ โ) |
93 | | knoppndvlem17.a |
. . . . . . . . 9
โข ๐ด = ((((2 ยท ๐)โ-๐ฝ) / 2) ยท ๐) |
94 | 93 | a1i 11 |
. . . . . . . 8
โข (๐ โ ๐ด = ((((2 ยท ๐)โ-๐ฝ) / 2) ยท ๐)) |
95 | 15, 39, 87 | knoppndvlem1 35388 |
. . . . . . . 8
โข (๐ โ ((((2 ยท ๐)โ-๐ฝ) / 2) ยท ๐) โ โ) |
96 | 94, 95 | eqeltrd 2834 |
. . . . . . 7
โข (๐ โ ๐ด โ โ) |
97 | 82, 83, 84, 96, 15, 3, 91 | knoppcld 35381 |
. . . . . 6
โข (๐ โ (๐โ๐ด) โ โ) |
98 | 92, 97 | subcld 11571 |
. . . . 5
โข (๐ โ ((๐โ๐ต) โ (๐โ๐ด)) โ โ) |
99 | 98 | abscld 15383 |
. . . 4
โข (๐ โ (absโ((๐โ๐ต) โ (๐โ๐ด))) โ โ) |
100 | 82, 83, 84, 93, 85, 1, 6, 87, 15, 23 | knoppndvlem15 35402 |
. . . 4
โข (๐ โ ((((absโ๐ถ)โ๐ฝ) / 2) ยท (1 โ (1 / (((2
ยท ๐) ยท
(absโ๐ถ)) โ
1)))) โค (absโ((๐โ๐ต) โ (๐โ๐ด)))) |
101 | 81, 99, 42, 100 | lediv1dd 13074 |
. . 3
โข (๐ โ (((((absโ๐ถ)โ๐ฝ) / 2) ยท (1 โ (1 / (((2
ยท ๐) ยท
(absโ๐ถ)) โ
1)))) / (((2 ยท ๐)โ-๐ฝ) / 2)) โค ((absโ((๐โ๐ต) โ (๐โ๐ด))) / (((2 ยท ๐)โ-๐ฝ) / 2))) |
102 | 80, 101 | eqbrtrd 5171 |
. 2
โข (๐ โ ((((2 ยท ๐) ยท (absโ๐ถ))โ๐ฝ) ยท (1 โ (1 / (((2 ยท
๐) ยท
(absโ๐ถ)) โ
1)))) โค ((absโ((๐โ๐ต) โ (๐โ๐ด))) / (((2 ยท ๐)โ-๐ฝ) / 2))) |
103 | 93, 85, 6, 87, 15 | knoppndvlem16 35403 |
. . . 4
โข (๐ โ (๐ต โ ๐ด) = (((2 ยท ๐)โ-๐ฝ) / 2)) |
104 | 103 | eqcomd 2739 |
. . 3
โข (๐ โ (((2 ยท ๐)โ-๐ฝ) / 2) = (๐ต โ ๐ด)) |
105 | 104 | oveq2d 7425 |
. 2
โข (๐ โ ((absโ((๐โ๐ต) โ (๐โ๐ด))) / (((2 ยท ๐)โ-๐ฝ) / 2)) = ((absโ((๐โ๐ต) โ (๐โ๐ด))) / (๐ต โ ๐ด))) |
106 | 102, 105 | breqtrd 5175 |
1
โข (๐ โ ((((2 ยท ๐) ยท (absโ๐ถ))โ๐ฝ) ยท (1 โ (1 / (((2 ยท
๐) ยท
(absโ๐ถ)) โ
1)))) โค ((absโ((๐โ๐ต) โ (๐โ๐ด))) / (๐ต โ ๐ด))) |