Step | Hyp | Ref
| Expression |
1 | | knoppndvlem14.t |
. . . . . 6
โข ๐ = (๐ฅ โ โ โฆ
(absโ((โโ(๐ฅ + (1 / 2))) โ ๐ฅ))) |
2 | | knoppndvlem14.f |
. . . . . 6
โข ๐น = (๐ฆ โ โ โฆ (๐ โ โ0 โฆ ((๐ถโ๐) ยท (๐โ(((2 ยท ๐)โ๐) ยท ๐ฆ))))) |
3 | | knoppndvlem14.b |
. . . . . . . 8
โข ๐ต = ((((2 ยท ๐)โ-๐ฝ) / 2) ยท (๐ + 1)) |
4 | 3 | a1i 11 |
. . . . . . 7
โข (๐ โ ๐ต = ((((2 ยท ๐)โ-๐ฝ) / 2) ยท (๐ + 1))) |
5 | | knoppndvlem14.n |
. . . . . . . 8
โข (๐ โ ๐ โ โ) |
6 | | knoppndvlem14.j |
. . . . . . . . 9
โข (๐ โ ๐ฝ โ
โ0) |
7 | 6 | nn0zd 12534 |
. . . . . . . 8
โข (๐ โ ๐ฝ โ โค) |
8 | | knoppndvlem14.m |
. . . . . . . . 9
โข (๐ โ ๐ โ โค) |
9 | 8 | peano2zd 12619 |
. . . . . . . 8
โข (๐ โ (๐ + 1) โ โค) |
10 | 5, 7, 9 | knoppndvlem1 35051 |
. . . . . . 7
โข (๐ โ ((((2 ยท ๐)โ-๐ฝ) / 2) ยท (๐ + 1)) โ โ) |
11 | 4, 10 | eqeltrd 2832 |
. . . . . 6
โข (๐ โ ๐ต โ โ) |
12 | | knoppndvlem14.c |
. . . . . . . 8
โข (๐ โ ๐ถ โ (-1(,)1)) |
13 | 12 | knoppndvlem3 35053 |
. . . . . . 7
โข (๐ โ (๐ถ โ โ โง (absโ๐ถ) < 1)) |
14 | 13 | simpld 495 |
. . . . . 6
โข (๐ โ ๐ถ โ โ) |
15 | 1, 2, 11, 14, 5 | knoppndvlem5 35055 |
. . . . 5
โข (๐ โ ฮฃ๐ โ (0...(๐ฝ โ 1))((๐นโ๐ต)โ๐) โ โ) |
16 | | knoppndvlem14.a |
. . . . . . . 8
โข ๐ด = ((((2 ยท ๐)โ-๐ฝ) / 2) ยท ๐) |
17 | 16 | a1i 11 |
. . . . . . 7
โข (๐ โ ๐ด = ((((2 ยท ๐)โ-๐ฝ) / 2) ยท ๐)) |
18 | 5, 7, 8 | knoppndvlem1 35051 |
. . . . . . 7
โข (๐ โ ((((2 ยท ๐)โ-๐ฝ) / 2) ยท ๐) โ โ) |
19 | 17, 18 | eqeltrd 2832 |
. . . . . 6
โข (๐ โ ๐ด โ โ) |
20 | 1, 2, 19, 14, 5 | knoppndvlem5 35055 |
. . . . 5
โข (๐ โ ฮฃ๐ โ (0...(๐ฝ โ 1))((๐นโ๐ด)โ๐) โ โ) |
21 | 15, 20 | resubcld 11592 |
. . . 4
โข (๐ โ (ฮฃ๐ โ (0...(๐ฝ โ 1))((๐นโ๐ต)โ๐) โ ฮฃ๐ โ (0...(๐ฝ โ 1))((๐นโ๐ด)โ๐)) โ โ) |
22 | 21 | recnd 11192 |
. . 3
โข (๐ โ (ฮฃ๐ โ (0...(๐ฝ โ 1))((๐นโ๐ต)โ๐) โ ฮฃ๐ โ (0...(๐ฝ โ 1))((๐นโ๐ด)โ๐)) โ โ) |
23 | 22 | abscld 15333 |
. 2
โข (๐ โ (absโ(ฮฃ๐ โ (0...(๐ฝ โ 1))((๐นโ๐ต)โ๐) โ ฮฃ๐ โ (0...(๐ฝ โ 1))((๐นโ๐ด)โ๐))) โ โ) |
24 | 11, 19 | resubcld 11592 |
. . . . 5
โข (๐ โ (๐ต โ ๐ด) โ โ) |
25 | 24 | recnd 11192 |
. . . 4
โข (๐ โ (๐ต โ ๐ด) โ โ) |
26 | 25 | abscld 15333 |
. . 3
โข (๐ โ (absโ(๐ต โ ๐ด)) โ โ) |
27 | | fzfid 13888 |
. . . 4
โข (๐ โ (0...(๐ฝ โ 1)) โ Fin) |
28 | | 2re 12236 |
. . . . . . . . 9
โข 2 โ
โ |
29 | 28 | a1i 11 |
. . . . . . . 8
โข (๐ โ 2 โ
โ) |
30 | | nnre 12169 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ
โ) |
31 | 5, 30 | syl 17 |
. . . . . . . 8
โข (๐ โ ๐ โ โ) |
32 | 29, 31 | remulcld 11194 |
. . . . . . 7
โข (๐ โ (2 ยท ๐) โ
โ) |
33 | 14 | recnd 11192 |
. . . . . . . 8
โข (๐ โ ๐ถ โ โ) |
34 | 33 | abscld 15333 |
. . . . . . 7
โข (๐ โ (absโ๐ถ) โ
โ) |
35 | 32, 34 | remulcld 11194 |
. . . . . 6
โข (๐ โ ((2 ยท ๐) ยท (absโ๐ถ)) โ
โ) |
36 | 35 | adantr 481 |
. . . . 5
โข ((๐ โง ๐ โ (0...(๐ฝ โ 1))) โ ((2 ยท ๐) ยท (absโ๐ถ)) โ
โ) |
37 | | elfznn0 13544 |
. . . . . 6
โข (๐ โ (0...(๐ฝ โ 1)) โ ๐ โ โ0) |
38 | 37 | adantl 482 |
. . . . 5
โข ((๐ โง ๐ โ (0...(๐ฝ โ 1))) โ ๐ โ โ0) |
39 | 36, 38 | reexpcld 14078 |
. . . 4
โข ((๐ โง ๐ โ (0...(๐ฝ โ 1))) โ (((2 ยท ๐) ยท (absโ๐ถ))โ๐) โ โ) |
40 | 27, 39 | fsumrecl 15630 |
. . 3
โข (๐ โ ฮฃ๐ โ (0...(๐ฝ โ 1))(((2 ยท ๐) ยท (absโ๐ถ))โ๐) โ โ) |
41 | 26, 40 | remulcld 11194 |
. 2
โข (๐ โ ((absโ(๐ต โ ๐ด)) ยท ฮฃ๐ โ (0...(๐ฝ โ 1))(((2 ยท ๐) ยท (absโ๐ถ))โ๐)) โ โ) |
42 | 34, 6 | reexpcld 14078 |
. . . 4
โข (๐ โ ((absโ๐ถ)โ๐ฝ) โ โ) |
43 | | 2ne0 12266 |
. . . . 5
โข 2 โ
0 |
44 | 43 | a1i 11 |
. . . 4
โข (๐ โ 2 โ 0) |
45 | 42, 29, 44 | redivcld 11992 |
. . 3
โข (๐ โ (((absโ๐ถ)โ๐ฝ) / 2) โ โ) |
46 | | 1red 11165 |
. . . 4
โข (๐ โ 1 โ
โ) |
47 | 35, 46 | resubcld 11592 |
. . . 4
โข (๐ โ (((2 ยท ๐) ยท (absโ๐ถ)) โ 1) โ
โ) |
48 | | 0red 11167 |
. . . . . 6
โข (๐ โ 0 โ
โ) |
49 | | 0lt1 11686 |
. . . . . . . 8
โข 0 <
1 |
50 | 49 | a1i 11 |
. . . . . . 7
โข (๐ โ 0 < 1) |
51 | | knoppndvlem14.1 |
. . . . . . . . 9
โข (๐ โ 1 < (๐ ยท (absโ๐ถ))) |
52 | 12, 5, 51 | knoppndvlem12 35062 |
. . . . . . . 8
โข (๐ โ (((2 ยท ๐) ยท (absโ๐ถ)) โ 1 โง 1 < (((2
ยท ๐) ยท
(absโ๐ถ)) โ
1))) |
53 | 52 | simprd 496 |
. . . . . . 7
โข (๐ โ 1 < (((2 ยท ๐) ยท (absโ๐ถ)) โ 1)) |
54 | 48, 46, 47, 50, 53 | lttrd 11325 |
. . . . . 6
โข (๐ โ 0 < (((2 ยท ๐) ยท (absโ๐ถ)) โ 1)) |
55 | 48, 54 | jca 512 |
. . . . 5
โข (๐ โ (0 โ โ โง 0
< (((2 ยท ๐)
ยท (absโ๐ถ))
โ 1))) |
56 | | ltne 11261 |
. . . . 5
โข ((0
โ โ โง 0 < (((2 ยท ๐) ยท (absโ๐ถ)) โ 1)) โ (((2 ยท ๐) ยท (absโ๐ถ)) โ 1) โ
0) |
57 | 55, 56 | syl 17 |
. . . 4
โข (๐ โ (((2 ยท ๐) ยท (absโ๐ถ)) โ 1) โ
0) |
58 | 46, 47, 57 | redivcld 11992 |
. . 3
โข (๐ โ (1 / (((2 ยท ๐) ยท (absโ๐ถ)) โ 1)) โ
โ) |
59 | 45, 58 | remulcld 11194 |
. 2
โข (๐ โ ((((absโ๐ถ)โ๐ฝ) / 2) ยท (1 / (((2 ยท ๐) ยท (absโ๐ถ)) โ 1))) โ
โ) |
60 | 1, 2, 19, 11, 12, 6, 5 | knoppndvlem11 35061 |
. 2
โข (๐ โ (absโ(ฮฃ๐ โ (0...(๐ฝ โ 1))((๐นโ๐ต)โ๐) โ ฮฃ๐ โ (0...(๐ฝ โ 1))((๐นโ๐ด)โ๐))) โค ((absโ(๐ต โ ๐ด)) ยท ฮฃ๐ โ (0...(๐ฝ โ 1))(((2 ยท ๐) ยท (absโ๐ถ))โ๐))) |
61 | 4, 17 | oveq12d 7380 |
. . . . . . 7
โข (๐ โ (๐ต โ ๐ด) = (((((2 ยท ๐)โ-๐ฝ) / 2) ยท (๐ + 1)) โ ((((2 ยท ๐)โ-๐ฝ) / 2) ยท ๐))) |
62 | 29 | recnd 11192 |
. . . . . . . . . . . . . 14
โข (๐ โ 2 โ
โ) |
63 | 31 | recnd 11192 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ โ โ) |
64 | | nnge1 12190 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ โ 1 โค
๐) |
65 | 5, 64 | syl 17 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ 1 โค ๐) |
66 | 48, 46, 31, 50, 65 | ltletrd 11324 |
. . . . . . . . . . . . . . . 16
โข (๐ โ 0 < ๐) |
67 | 48, 66 | jca 512 |
. . . . . . . . . . . . . . 15
โข (๐ โ (0 โ โ โง 0
< ๐)) |
68 | | ltne 11261 |
. . . . . . . . . . . . . . 15
โข ((0
โ โ โง 0 < ๐) โ ๐ โ 0) |
69 | 67, 68 | syl 17 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ โ 0) |
70 | 62, 63, 44, 69 | mulne0d 11816 |
. . . . . . . . . . . . 13
โข (๐ โ (2 ยท ๐) โ 0) |
71 | 7 | znegcld 12618 |
. . . . . . . . . . . . 13
โข (๐ โ -๐ฝ โ โค) |
72 | 32, 70, 71 | reexpclzd 14162 |
. . . . . . . . . . . 12
โข (๐ โ ((2 ยท ๐)โ-๐ฝ) โ โ) |
73 | 72, 29, 44 | redivcld 11992 |
. . . . . . . . . . 11
โข (๐ โ (((2 ยท ๐)โ-๐ฝ) / 2) โ โ) |
74 | 73 | recnd 11192 |
. . . . . . . . . 10
โข (๐ โ (((2 ยท ๐)โ-๐ฝ) / 2) โ โ) |
75 | 9 | zcnd 12617 |
. . . . . . . . . 10
โข (๐ โ (๐ + 1) โ โ) |
76 | 8 | zcnd 12617 |
. . . . . . . . . 10
โข (๐ โ ๐ โ โ) |
77 | 74, 75, 76 | subdid 11620 |
. . . . . . . . 9
โข (๐ โ ((((2 ยท ๐)โ-๐ฝ) / 2) ยท ((๐ + 1) โ ๐)) = (((((2 ยท ๐)โ-๐ฝ) / 2) ยท (๐ + 1)) โ ((((2 ยท ๐)โ-๐ฝ) / 2) ยท ๐))) |
78 | 77 | eqcomd 2737 |
. . . . . . . 8
โข (๐ โ (((((2 ยท ๐)โ-๐ฝ) / 2) ยท (๐ + 1)) โ ((((2 ยท ๐)โ-๐ฝ) / 2) ยท ๐)) = ((((2 ยท ๐)โ-๐ฝ) / 2) ยท ((๐ + 1) โ ๐))) |
79 | | 1cnd 11159 |
. . . . . . . . . 10
โข (๐ โ 1 โ
โ) |
80 | 76, 79 | pncan2d 11523 |
. . . . . . . . 9
โข (๐ โ ((๐ + 1) โ ๐) = 1) |
81 | 80 | oveq2d 7378 |
. . . . . . . 8
โข (๐ โ ((((2 ยท ๐)โ-๐ฝ) / 2) ยท ((๐ + 1) โ ๐)) = ((((2 ยท ๐)โ-๐ฝ) / 2) ยท 1)) |
82 | 74 | mulridd 11181 |
. . . . . . . 8
โข (๐ โ ((((2 ยท ๐)โ-๐ฝ) / 2) ยท 1) = (((2 ยท ๐)โ-๐ฝ) / 2)) |
83 | 78, 81, 82 | 3eqtrd 2775 |
. . . . . . 7
โข (๐ โ (((((2 ยท ๐)โ-๐ฝ) / 2) ยท (๐ + 1)) โ ((((2 ยท ๐)โ-๐ฝ) / 2) ยท ๐)) = (((2 ยท ๐)โ-๐ฝ) / 2)) |
84 | 61, 83 | eqtrd 2771 |
. . . . . 6
โข (๐ โ (๐ต โ ๐ด) = (((2 ยท ๐)โ-๐ฝ) / 2)) |
85 | 84 | fveq2d 6851 |
. . . . 5
โข (๐ โ (absโ(๐ต โ ๐ด)) = (absโ(((2 ยท ๐)โ-๐ฝ) / 2))) |
86 | 72 | recnd 11192 |
. . . . . . 7
โข (๐ โ ((2 ยท ๐)โ-๐ฝ) โ โ) |
87 | 86, 62, 44 | absdivd 15352 |
. . . . . 6
โข (๐ โ (absโ(((2 ยท
๐)โ-๐ฝ) / 2)) = ((absโ((2 ยท ๐)โ-๐ฝ)) / (absโ2))) |
88 | 62, 63 | mulcld 11184 |
. . . . . . . . . 10
โข (๐ โ (2 ยท ๐) โ
โ) |
89 | 88, 70, 71 | 3jca 1128 |
. . . . . . . . 9
โข (๐ โ ((2 ยท ๐) โ โ โง (2
ยท ๐) โ 0 โง
-๐ฝ โ
โค)) |
90 | | absexpz 15202 |
. . . . . . . . 9
โข (((2
ยท ๐) โ โ
โง (2 ยท ๐) โ 0
โง -๐ฝ โ โค)
โ (absโ((2 ยท ๐)โ-๐ฝ)) = ((absโ(2 ยท ๐))โ-๐ฝ)) |
91 | 89, 90 | syl 17 |
. . . . . . . 8
โข (๐ โ (absโ((2 ยท
๐)โ-๐ฝ)) = ((absโ(2 ยท ๐))โ-๐ฝ)) |
92 | 62, 63 | absmuld 15351 |
. . . . . . . . . 10
โข (๐ โ (absโ(2 ยท
๐)) = ((absโ2)
ยท (absโ๐))) |
93 | | 0le2 12264 |
. . . . . . . . . . . . . 14
โข 0 โค
2 |
94 | 28, 93 | pm3.2i 471 |
. . . . . . . . . . . . 13
โข (2 โ
โ โง 0 โค 2) |
95 | | absid 15193 |
. . . . . . . . . . . . 13
โข ((2
โ โ โง 0 โค 2) โ (absโ2) = 2) |
96 | 94, 95 | ax-mp 5 |
. . . . . . . . . . . 12
โข
(absโ2) = 2 |
97 | 96 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ (absโ2) =
2) |
98 | 48, 31, 66 | ltled 11312 |
. . . . . . . . . . . 12
โข (๐ โ 0 โค ๐) |
99 | 31, 98 | absidd 15319 |
. . . . . . . . . . 11
โข (๐ โ (absโ๐) = ๐) |
100 | 97, 99 | oveq12d 7380 |
. . . . . . . . . 10
โข (๐ โ ((absโ2) ยท
(absโ๐)) = (2
ยท ๐)) |
101 | 92, 100 | eqtrd 2771 |
. . . . . . . . 9
โข (๐ โ (absโ(2 ยท
๐)) = (2 ยท ๐)) |
102 | 101 | oveq1d 7377 |
. . . . . . . 8
โข (๐ โ ((absโ(2 ยท
๐))โ-๐ฝ) = ((2 ยท ๐)โ-๐ฝ)) |
103 | 91, 102 | eqtrd 2771 |
. . . . . . 7
โข (๐ โ (absโ((2 ยท
๐)โ-๐ฝ)) = ((2 ยท ๐)โ-๐ฝ)) |
104 | 103, 97 | oveq12d 7380 |
. . . . . 6
โข (๐ โ ((absโ((2 ยท
๐)โ-๐ฝ)) / (absโ2)) = (((2 ยท ๐)โ-๐ฝ) / 2)) |
105 | 87, 104 | eqtrd 2771 |
. . . . 5
โข (๐ โ (absโ(((2 ยท
๐)โ-๐ฝ) / 2)) = (((2 ยท ๐)โ-๐ฝ) / 2)) |
106 | 85, 105 | eqtrd 2771 |
. . . 4
โข (๐ โ (absโ(๐ต โ ๐ด)) = (((2 ยท ๐)โ-๐ฝ) / 2)) |
107 | 35 | recnd 11192 |
. . . . . 6
โข (๐ โ ((2 ยท ๐) ยท (absโ๐ถ)) โ
โ) |
108 | 52 | simpld 495 |
. . . . . 6
โข (๐ โ ((2 ยท ๐) ยท (absโ๐ถ)) โ 1) |
109 | 107, 108,
6 | geoser 15763 |
. . . . 5
โข (๐ โ ฮฃ๐ โ (0...(๐ฝ โ 1))(((2 ยท ๐) ยท (absโ๐ถ))โ๐) = ((1 โ (((2 ยท ๐) ยท (absโ๐ถ))โ๐ฝ)) / (1 โ ((2 ยท ๐) ยท (absโ๐ถ))))) |
110 | 107, 6 | expcld 14061 |
. . . . . 6
โข (๐ โ (((2 ยท ๐) ยท (absโ๐ถ))โ๐ฝ) โ โ) |
111 | 108 | necomd 2995 |
. . . . . 6
โข (๐ โ 1 โ ((2 ยท ๐) ยท (absโ๐ถ))) |
112 | 79, 110, 79, 107, 111 | div2subd 11990 |
. . . . 5
โข (๐ โ ((1 โ (((2 ยท
๐) ยท
(absโ๐ถ))โ๐ฝ)) / (1 โ ((2 ยท
๐) ยท
(absโ๐ถ)))) = (((((2
ยท ๐) ยท
(absโ๐ถ))โ๐ฝ) โ 1) / (((2 ยท
๐) ยท
(absโ๐ถ)) โ
1))) |
113 | 109, 112 | eqtrd 2771 |
. . . 4
โข (๐ โ ฮฃ๐ โ (0...(๐ฝ โ 1))(((2 ยท ๐) ยท (absโ๐ถ))โ๐) = (((((2 ยท ๐) ยท (absโ๐ถ))โ๐ฝ) โ 1) / (((2 ยท ๐) ยท (absโ๐ถ)) โ 1))) |
114 | 106, 113 | oveq12d 7380 |
. . 3
โข (๐ โ ((absโ(๐ต โ ๐ด)) ยท ฮฃ๐ โ (0...(๐ฝ โ 1))(((2 ยท ๐) ยท (absโ๐ถ))โ๐)) = ((((2 ยท ๐)โ-๐ฝ) / 2) ยท (((((2 ยท ๐) ยท (absโ๐ถ))โ๐ฝ) โ 1) / (((2 ยท ๐) ยท (absโ๐ถ)) โ
1)))) |
115 | 113, 40 | eqeltrrd 2833 |
. . . . 5
โข (๐ โ (((((2 ยท ๐) ยท (absโ๐ถ))โ๐ฝ) โ 1) / (((2 ยท ๐) ยท (absโ๐ถ)) โ 1)) โ
โ) |
116 | 35, 6 | reexpcld 14078 |
. . . . . 6
โข (๐ โ (((2 ยท ๐) ยท (absโ๐ถ))โ๐ฝ) โ โ) |
117 | 116, 47, 57 | redivcld 11992 |
. . . . 5
โข (๐ โ ((((2 ยท ๐) ยท (absโ๐ถ))โ๐ฝ) / (((2 ยท ๐) ยท (absโ๐ถ)) โ 1)) โ
โ) |
118 | | 2rp 12929 |
. . . . . . 7
โข 2 โ
โ+ |
119 | 118 | a1i 11 |
. . . . . 6
โข (๐ โ 2 โ
โ+) |
120 | 119 | rpgt0d 12969 |
. . . . . . . . . 10
โข (๐ โ 0 < 2) |
121 | 29, 31, 120, 66 | mulgt0d 11319 |
. . . . . . . . 9
โข (๐ โ 0 < (2 ยท ๐)) |
122 | 32, 71, 121 | 3jca 1128 |
. . . . . . . 8
โข (๐ โ ((2 ยท ๐) โ โ โง -๐ฝ โ โค โง 0 < (2
ยท ๐))) |
123 | | expgt0 14011 |
. . . . . . . 8
โข (((2
ยท ๐) โ โ
โง -๐ฝ โ โค
โง 0 < (2 ยท ๐)) โ 0 < ((2 ยท ๐)โ-๐ฝ)) |
124 | 122, 123 | syl 17 |
. . . . . . 7
โข (๐ โ 0 < ((2 ยท ๐)โ-๐ฝ)) |
125 | 48, 72, 124 | ltled 11312 |
. . . . . 6
โข (๐ โ 0 โค ((2 ยท ๐)โ-๐ฝ)) |
126 | 72, 119, 125 | divge0d 13006 |
. . . . 5
โข (๐ โ 0 โค (((2 ยท ๐)โ-๐ฝ) / 2)) |
127 | 116, 46 | resubcld 11592 |
. . . . . 6
โข (๐ โ ((((2 ยท ๐) ยท (absโ๐ถ))โ๐ฝ) โ 1) โ
โ) |
128 | 47, 54 | elrpd 12963 |
. . . . . 6
โข (๐ โ (((2 ยท ๐) ยท (absโ๐ถ)) โ 1) โ
โ+) |
129 | 116 | lem1d 12097 |
. . . . . 6
โข (๐ โ ((((2 ยท ๐) ยท (absโ๐ถ))โ๐ฝ) โ 1) โค (((2 ยท ๐) ยท (absโ๐ถ))โ๐ฝ)) |
130 | 127, 116,
128, 129 | lediv1dd 13024 |
. . . . 5
โข (๐ โ (((((2 ยท ๐) ยท (absโ๐ถ))โ๐ฝ) โ 1) / (((2 ยท ๐) ยท (absโ๐ถ)) โ 1)) โค ((((2
ยท ๐) ยท
(absโ๐ถ))โ๐ฝ) / (((2 ยท ๐) ยท (absโ๐ถ)) โ 1))) |
131 | 115, 117,
73, 126, 130 | lemul2ad 12104 |
. . . 4
โข (๐ โ ((((2 ยท ๐)โ-๐ฝ) / 2) ยท (((((2 ยท ๐) ยท (absโ๐ถ))โ๐ฝ) โ 1) / (((2 ยท ๐) ยท (absโ๐ถ)) โ 1))) โค ((((2
ยท ๐)โ-๐ฝ) / 2) ยท ((((2 ยท
๐) ยท
(absโ๐ถ))โ๐ฝ) / (((2 ยท ๐) ยท (absโ๐ถ)) โ
1)))) |
132 | 47 | recnd 11192 |
. . . . . . 7
โข (๐ โ (((2 ยท ๐) ยท (absโ๐ถ)) โ 1) โ
โ) |
133 | 110, 132,
57 | divrecd 11943 |
. . . . . 6
โข (๐ โ ((((2 ยท ๐) ยท (absโ๐ถ))โ๐ฝ) / (((2 ยท ๐) ยท (absโ๐ถ)) โ 1)) = ((((2 ยท ๐) ยท (absโ๐ถ))โ๐ฝ) ยท (1 / (((2 ยท ๐) ยท (absโ๐ถ)) โ
1)))) |
134 | 133 | oveq2d 7378 |
. . . . 5
โข (๐ โ ((((2 ยท ๐)โ-๐ฝ) / 2) ยท ((((2 ยท ๐) ยท (absโ๐ถ))โ๐ฝ) / (((2 ยท ๐) ยท (absโ๐ถ)) โ 1))) = ((((2 ยท ๐)โ-๐ฝ) / 2) ยท ((((2 ยท ๐) ยท (absโ๐ถ))โ๐ฝ) ยท (1 / (((2 ยท ๐) ยท (absโ๐ถ)) โ
1))))) |
135 | 58 | recnd 11192 |
. . . . . . 7
โข (๐ โ (1 / (((2 ยท ๐) ยท (absโ๐ถ)) โ 1)) โ
โ) |
136 | 74, 110, 135 | mulassd 11187 |
. . . . . 6
โข (๐ โ (((((2 ยท ๐)โ-๐ฝ) / 2) ยท (((2 ยท ๐) ยท (absโ๐ถ))โ๐ฝ)) ยท (1 / (((2 ยท ๐) ยท (absโ๐ถ)) โ 1))) = ((((2 ยท
๐)โ-๐ฝ) / 2) ยท ((((2 ยท ๐) ยท (absโ๐ถ))โ๐ฝ) ยท (1 / (((2 ยท ๐) ยท (absโ๐ถ)) โ
1))))) |
137 | 136 | eqcomd 2737 |
. . . . 5
โข (๐ โ ((((2 ยท ๐)โ-๐ฝ) / 2) ยท ((((2 ยท ๐) ยท (absโ๐ถ))โ๐ฝ) ยท (1 / (((2 ยท ๐) ยท (absโ๐ถ)) โ 1)))) = (((((2
ยท ๐)โ-๐ฝ) / 2) ยท (((2 ยท
๐) ยท
(absโ๐ถ))โ๐ฝ)) ยท (1 / (((2 ยท
๐) ยท
(absโ๐ถ)) โ
1)))) |
138 | 86, 110, 62, 44 | div23d 11977 |
. . . . . . . 8
โข (๐ โ ((((2 ยท ๐)โ-๐ฝ) ยท (((2 ยท ๐) ยท (absโ๐ถ))โ๐ฝ)) / 2) = ((((2 ยท ๐)โ-๐ฝ) / 2) ยท (((2 ยท ๐) ยท (absโ๐ถ))โ๐ฝ))) |
139 | 138 | eqcomd 2737 |
. . . . . . 7
โข (๐ โ ((((2 ยท ๐)โ-๐ฝ) / 2) ยท (((2 ยท ๐) ยท (absโ๐ถ))โ๐ฝ)) = ((((2 ยท ๐)โ-๐ฝ) ยท (((2 ยท ๐) ยท (absโ๐ถ))โ๐ฝ)) / 2)) |
140 | 88, 70 | jca 512 |
. . . . . . . . . . . 12
โข (๐ โ ((2 ยท ๐) โ โ โง (2
ยท ๐) โ
0)) |
141 | 34 | recnd 11192 |
. . . . . . . . . . . . 13
โข (๐ โ (absโ๐ถ) โ
โ) |
142 | 12, 5, 51 | knoppndvlem13 35063 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ถ โ 0) |
143 | 33, 142 | absne0d 15344 |
. . . . . . . . . . . . 13
โข (๐ โ (absโ๐ถ) โ 0) |
144 | 141, 143 | jca 512 |
. . . . . . . . . . . 12
โข (๐ โ ((absโ๐ถ) โ โ โง
(absโ๐ถ) โ
0)) |
145 | 140, 144,
7 | 3jca 1128 |
. . . . . . . . . . 11
โข (๐ โ (((2 ยท ๐) โ โ โง (2
ยท ๐) โ 0) โง
((absโ๐ถ) โ
โ โง (absโ๐ถ)
โ 0) โง ๐ฝ โ
โค)) |
146 | | mulexpz 14018 |
. . . . . . . . . . 11
โข ((((2
ยท ๐) โ โ
โง (2 ยท ๐) โ
0) โง ((absโ๐ถ)
โ โ โง (absโ๐ถ) โ 0) โง ๐ฝ โ โค) โ (((2 ยท ๐) ยท (absโ๐ถ))โ๐ฝ) = (((2 ยท ๐)โ๐ฝ) ยท ((absโ๐ถ)โ๐ฝ))) |
147 | 145, 146 | syl 17 |
. . . . . . . . . 10
โข (๐ โ (((2 ยท ๐) ยท (absโ๐ถ))โ๐ฝ) = (((2 ยท ๐)โ๐ฝ) ยท ((absโ๐ถ)โ๐ฝ))) |
148 | 147 | oveq2d 7378 |
. . . . . . . . 9
โข (๐ โ (((2 ยท ๐)โ-๐ฝ) ยท (((2 ยท ๐) ยท (absโ๐ถ))โ๐ฝ)) = (((2 ยท ๐)โ-๐ฝ) ยท (((2 ยท ๐)โ๐ฝ) ยท ((absโ๐ถ)โ๐ฝ)))) |
149 | 88, 6 | expcld 14061 |
. . . . . . . . . . 11
โข (๐ โ ((2 ยท ๐)โ๐ฝ) โ โ) |
150 | 42 | recnd 11192 |
. . . . . . . . . . 11
โข (๐ โ ((absโ๐ถ)โ๐ฝ) โ โ) |
151 | 86, 149, 150 | mulassd 11187 |
. . . . . . . . . 10
โข (๐ โ ((((2 ยท ๐)โ-๐ฝ) ยท ((2 ยท ๐)โ๐ฝ)) ยท ((absโ๐ถ)โ๐ฝ)) = (((2 ยท ๐)โ-๐ฝ) ยท (((2 ยท ๐)โ๐ฝ) ยท ((absโ๐ถ)โ๐ฝ)))) |
152 | 151 | eqcomd 2737 |
. . . . . . . . 9
โข (๐ โ (((2 ยท ๐)โ-๐ฝ) ยท (((2 ยท ๐)โ๐ฝ) ยท ((absโ๐ถ)โ๐ฝ))) = ((((2 ยท ๐)โ-๐ฝ) ยท ((2 ยท ๐)โ๐ฝ)) ยท ((absโ๐ถ)โ๐ฝ))) |
153 | 140, 71, 7 | jca32 516 |
. . . . . . . . . . . . . 14
โข (๐ โ (((2 ยท ๐) โ โ โง (2
ยท ๐) โ 0) โง
(-๐ฝ โ โค โง
๐ฝ โ
โค))) |
154 | | expaddz 14022 |
. . . . . . . . . . . . . 14
โข ((((2
ยท ๐) โ โ
โง (2 ยท ๐) โ
0) โง (-๐ฝ โ โค
โง ๐ฝ โ โค))
โ ((2 ยท ๐)โ(-๐ฝ + ๐ฝ)) = (((2 ยท ๐)โ-๐ฝ) ยท ((2 ยท ๐)โ๐ฝ))) |
155 | 153, 154 | syl 17 |
. . . . . . . . . . . . 13
โข (๐ โ ((2 ยท ๐)โ(-๐ฝ + ๐ฝ)) = (((2 ยท ๐)โ-๐ฝ) ยท ((2 ยท ๐)โ๐ฝ))) |
156 | 155 | eqcomd 2737 |
. . . . . . . . . . . 12
โข (๐ โ (((2 ยท ๐)โ-๐ฝ) ยท ((2 ยท ๐)โ๐ฝ)) = ((2 ยท ๐)โ(-๐ฝ + ๐ฝ))) |
157 | 71 | zcnd 12617 |
. . . . . . . . . . . . . . 15
โข (๐ โ -๐ฝ โ โ) |
158 | 6 | nn0cnd 12484 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ฝ โ โ) |
159 | 157, 158 | addcomd 11366 |
. . . . . . . . . . . . . 14
โข (๐ โ (-๐ฝ + ๐ฝ) = (๐ฝ + -๐ฝ)) |
160 | 158 | negidd 11511 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ฝ + -๐ฝ) = 0) |
161 | 159, 160 | eqtrd 2771 |
. . . . . . . . . . . . 13
โข (๐ โ (-๐ฝ + ๐ฝ) = 0) |
162 | 161 | oveq2d 7378 |
. . . . . . . . . . . 12
โข (๐ โ ((2 ยท ๐)โ(-๐ฝ + ๐ฝ)) = ((2 ยท ๐)โ0)) |
163 | 88 | exp0d 14055 |
. . . . . . . . . . . 12
โข (๐ โ ((2 ยท ๐)โ0) = 1) |
164 | 156, 162,
163 | 3eqtrd 2775 |
. . . . . . . . . . 11
โข (๐ โ (((2 ยท ๐)โ-๐ฝ) ยท ((2 ยท ๐)โ๐ฝ)) = 1) |
165 | 164 | oveq1d 7377 |
. . . . . . . . . 10
โข (๐ โ ((((2 ยท ๐)โ-๐ฝ) ยท ((2 ยท ๐)โ๐ฝ)) ยท ((absโ๐ถ)โ๐ฝ)) = (1 ยท ((absโ๐ถ)โ๐ฝ))) |
166 | 150 | mullidd 11182 |
. . . . . . . . . 10
โข (๐ โ (1 ยท
((absโ๐ถ)โ๐ฝ)) = ((absโ๐ถ)โ๐ฝ)) |
167 | 165, 166 | eqtrd 2771 |
. . . . . . . . 9
โข (๐ โ ((((2 ยท ๐)โ-๐ฝ) ยท ((2 ยท ๐)โ๐ฝ)) ยท ((absโ๐ถ)โ๐ฝ)) = ((absโ๐ถ)โ๐ฝ)) |
168 | 148, 152,
167 | 3eqtrd 2775 |
. . . . . . . 8
โข (๐ โ (((2 ยท ๐)โ-๐ฝ) ยท (((2 ยท ๐) ยท (absโ๐ถ))โ๐ฝ)) = ((absโ๐ถ)โ๐ฝ)) |
169 | 168 | oveq1d 7377 |
. . . . . . 7
โข (๐ โ ((((2 ยท ๐)โ-๐ฝ) ยท (((2 ยท ๐) ยท (absโ๐ถ))โ๐ฝ)) / 2) = (((absโ๐ถ)โ๐ฝ) / 2)) |
170 | 139, 169 | eqtrd 2771 |
. . . . . 6
โข (๐ โ ((((2 ยท ๐)โ-๐ฝ) / 2) ยท (((2 ยท ๐) ยท (absโ๐ถ))โ๐ฝ)) = (((absโ๐ถ)โ๐ฝ) / 2)) |
171 | 170 | oveq1d 7377 |
. . . . 5
โข (๐ โ (((((2 ยท ๐)โ-๐ฝ) / 2) ยท (((2 ยท ๐) ยท (absโ๐ถ))โ๐ฝ)) ยท (1 / (((2 ยท ๐) ยท (absโ๐ถ)) โ 1))) =
((((absโ๐ถ)โ๐ฝ) / 2) ยท (1 / (((2
ยท ๐) ยท
(absโ๐ถ)) โ
1)))) |
172 | 134, 137,
171 | 3eqtrd 2775 |
. . . 4
โข (๐ โ ((((2 ยท ๐)โ-๐ฝ) / 2) ยท ((((2 ยท ๐) ยท (absโ๐ถ))โ๐ฝ) / (((2 ยท ๐) ยท (absโ๐ถ)) โ 1))) = ((((absโ๐ถ)โ๐ฝ) / 2) ยท (1 / (((2 ยท ๐) ยท (absโ๐ถ)) โ
1)))) |
173 | 131, 172 | breqtrd 5136 |
. . 3
โข (๐ โ ((((2 ยท ๐)โ-๐ฝ) / 2) ยท (((((2 ยท ๐) ยท (absโ๐ถ))โ๐ฝ) โ 1) / (((2 ยท ๐) ยท (absโ๐ถ)) โ 1))) โค
((((absโ๐ถ)โ๐ฝ) / 2) ยท (1 / (((2
ยท ๐) ยท
(absโ๐ถ)) โ
1)))) |
174 | 114, 173 | eqbrtrd 5132 |
. 2
โข (๐ โ ((absโ(๐ต โ ๐ด)) ยท ฮฃ๐ โ (0...(๐ฝ โ 1))(((2 ยท ๐) ยท (absโ๐ถ))โ๐)) โค ((((absโ๐ถ)โ๐ฝ) / 2) ยท (1 / (((2 ยท ๐) ยท (absโ๐ถ)) โ
1)))) |
175 | 23, 41, 59, 60, 174 | letrd 11321 |
1
โข (๐ โ (absโ(ฮฃ๐ โ (0...(๐ฝ โ 1))((๐นโ๐ต)โ๐) โ ฮฃ๐ โ (0...(๐ฝ โ 1))((๐นโ๐ด)โ๐))) โค ((((absโ๐ถ)โ๐ฝ) / 2) ยท (1 / (((2 ยท ๐) ยท (absโ๐ถ)) โ
1)))) |