Step | Hyp | Ref
| Expression |
1 | | knoppndvlem10.t |
. . . . . . 7
โข ๐ = (๐ฅ โ โ โฆ
(absโ((โโ(๐ฅ + (1 / 2))) โ ๐ฅ))) |
2 | | knoppndvlem10.f |
. . . . . . 7
โข ๐น = (๐ฆ โ โ โฆ (๐ โ โ0 โฆ ((๐ถโ๐) ยท (๐โ(((2 ยท ๐)โ๐) ยท ๐ฆ))))) |
3 | | knoppndvlem10.b |
. . . . . . 7
โข ๐ต = ((((2 ยท ๐)โ-๐ฝ) / 2) ยท (๐ + 1)) |
4 | | knoppndvlem10.c |
. . . . . . . 8
โข (๐ โ ๐ถ โ (-1(,)1)) |
5 | 4 | adantr 482 |
. . . . . . 7
โข ((๐ โง 2 โฅ ๐) โ ๐ถ โ (-1(,)1)) |
6 | | knoppndvlem10.j |
. . . . . . . 8
โข (๐ โ ๐ฝ โ
โ0) |
7 | 6 | adantr 482 |
. . . . . . 7
โข ((๐ โง 2 โฅ ๐) โ ๐ฝ โ
โ0) |
8 | | knoppndvlem10.m |
. . . . . . . . 9
โข (๐ โ ๐ โ โค) |
9 | 8 | peano2zd 12615 |
. . . . . . . 8
โข (๐ โ (๐ + 1) โ โค) |
10 | 9 | adantr 482 |
. . . . . . 7
โข ((๐ โง 2 โฅ ๐) โ (๐ + 1) โ โค) |
11 | | knoppndvlem10.n |
. . . . . . . 8
โข (๐ โ ๐ โ โ) |
12 | 11 | adantr 482 |
. . . . . . 7
โข ((๐ โง 2 โฅ ๐) โ ๐ โ โ) |
13 | | notnot 142 |
. . . . . . . . 9
โข (2
โฅ ๐ โ ยฌ
ยฌ 2 โฅ ๐) |
14 | 13 | adantl 483 |
. . . . . . . 8
โข ((๐ โง 2 โฅ ๐) โ ยฌ ยฌ 2 โฅ ๐) |
15 | 8 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง 2 โฅ ๐) โ ๐ โ โค) |
16 | | oddp1even 16231 |
. . . . . . . . 9
โข (๐ โ โค โ (ยฌ 2
โฅ ๐ โ 2 โฅ
(๐ + 1))) |
17 | 15, 16 | syl 17 |
. . . . . . . 8
โข ((๐ โง 2 โฅ ๐) โ (ยฌ 2 โฅ ๐ โ 2 โฅ (๐ + 1))) |
18 | 14, 17 | mtbid 324 |
. . . . . . 7
โข ((๐ โง 2 โฅ ๐) โ ยฌ 2 โฅ (๐ + 1)) |
19 | 1, 2, 3, 5, 7, 10,
12, 18 | knoppndvlem9 35029 |
. . . . . 6
โข ((๐ โง 2 โฅ ๐) โ ((๐นโ๐ต)โ๐ฝ) = ((๐ถโ๐ฝ) / 2)) |
20 | | knoppndvlem10.a |
. . . . . . 7
โข ๐ด = ((((2 ยท ๐)โ-๐ฝ) / 2) ยท ๐) |
21 | 14 | notnotrd 133 |
. . . . . . 7
โข ((๐ โง 2 โฅ ๐) โ 2 โฅ ๐) |
22 | 1, 2, 20, 5, 7, 15, 12, 21 | knoppndvlem8 35028 |
. . . . . 6
โข ((๐ โง 2 โฅ ๐) โ ((๐นโ๐ด)โ๐ฝ) = 0) |
23 | 19, 22 | oveq12d 7376 |
. . . . 5
โข ((๐ โง 2 โฅ ๐) โ (((๐นโ๐ต)โ๐ฝ) โ ((๐นโ๐ด)โ๐ฝ)) = (((๐ถโ๐ฝ) / 2) โ 0)) |
24 | 4 | knoppndvlem3 35023 |
. . . . . . . . . . 11
โข (๐ โ (๐ถ โ โ โง (absโ๐ถ) < 1)) |
25 | 24 | simpld 496 |
. . . . . . . . . 10
โข (๐ โ ๐ถ โ โ) |
26 | 25 | recnd 11188 |
. . . . . . . . 9
โข (๐ โ ๐ถ โ โ) |
27 | 26, 6 | expcld 14057 |
. . . . . . . 8
โข (๐ โ (๐ถโ๐ฝ) โ โ) |
28 | | 2cnd 12236 |
. . . . . . . 8
โข (๐ โ 2 โ
โ) |
29 | | 2ne0 12262 |
. . . . . . . . 9
โข 2 โ
0 |
30 | 29 | a1i 11 |
. . . . . . . 8
โข (๐ โ 2 โ 0) |
31 | 27, 28, 30 | divcld 11936 |
. . . . . . 7
โข (๐ โ ((๐ถโ๐ฝ) / 2) โ โ) |
32 | 31 | subid1d 11506 |
. . . . . 6
โข (๐ โ (((๐ถโ๐ฝ) / 2) โ 0) = ((๐ถโ๐ฝ) / 2)) |
33 | 32 | adantr 482 |
. . . . 5
โข ((๐ โง 2 โฅ ๐) โ (((๐ถโ๐ฝ) / 2) โ 0) = ((๐ถโ๐ฝ) / 2)) |
34 | 23, 33 | eqtrd 2773 |
. . . 4
โข ((๐ โง 2 โฅ ๐) โ (((๐นโ๐ต)โ๐ฝ) โ ((๐นโ๐ด)โ๐ฝ)) = ((๐ถโ๐ฝ) / 2)) |
35 | 34 | fveq2d 6847 |
. . 3
โข ((๐ โง 2 โฅ ๐) โ (absโ(((๐นโ๐ต)โ๐ฝ) โ ((๐นโ๐ด)โ๐ฝ))) = (absโ((๐ถโ๐ฝ) / 2))) |
36 | 3 | a1i 11 |
. . . . . . . . 9
โข (๐ โ ๐ต = ((((2 ยท ๐)โ-๐ฝ) / 2) ยท (๐ + 1))) |
37 | 6 | nn0zd 12530 |
. . . . . . . . . 10
โข (๐ โ ๐ฝ โ โค) |
38 | 11, 37, 9 | knoppndvlem1 35021 |
. . . . . . . . 9
โข (๐ โ ((((2 ยท ๐)โ-๐ฝ) / 2) ยท (๐ + 1)) โ โ) |
39 | 36, 38 | eqeltrd 2834 |
. . . . . . . 8
โข (๐ โ ๐ต โ โ) |
40 | 1, 2, 11, 25, 39, 6 | knoppcnlem3 35004 |
. . . . . . 7
โข (๐ โ ((๐นโ๐ต)โ๐ฝ) โ โ) |
41 | 40 | recnd 11188 |
. . . . . 6
โข (๐ โ ((๐นโ๐ต)โ๐ฝ) โ โ) |
42 | 20 | a1i 11 |
. . . . . . . . 9
โข (๐ โ ๐ด = ((((2 ยท ๐)โ-๐ฝ) / 2) ยท ๐)) |
43 | 11, 37, 8 | knoppndvlem1 35021 |
. . . . . . . . 9
โข (๐ โ ((((2 ยท ๐)โ-๐ฝ) / 2) ยท ๐) โ โ) |
44 | 42, 43 | eqeltrd 2834 |
. . . . . . . 8
โข (๐ โ ๐ด โ โ) |
45 | 1, 2, 11, 25, 44, 6 | knoppcnlem3 35004 |
. . . . . . 7
โข (๐ โ ((๐นโ๐ด)โ๐ฝ) โ โ) |
46 | 45 | recnd 11188 |
. . . . . 6
โข (๐ โ ((๐นโ๐ด)โ๐ฝ) โ โ) |
47 | 41, 46 | abssubd 15344 |
. . . . 5
โข (๐ โ (absโ(((๐นโ๐ต)โ๐ฝ) โ ((๐นโ๐ด)โ๐ฝ))) = (absโ(((๐นโ๐ด)โ๐ฝ) โ ((๐นโ๐ต)โ๐ฝ)))) |
48 | 47 | adantr 482 |
. . . 4
โข ((๐ โง ยฌ 2 โฅ ๐) โ (absโ(((๐นโ๐ต)โ๐ฝ) โ ((๐นโ๐ด)โ๐ฝ))) = (absโ(((๐นโ๐ด)โ๐ฝ) โ ((๐นโ๐ต)โ๐ฝ)))) |
49 | 4 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ยฌ 2 โฅ ๐) โ ๐ถ โ (-1(,)1)) |
50 | 6 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ยฌ 2 โฅ ๐) โ ๐ฝ โ
โ0) |
51 | 8 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ยฌ 2 โฅ ๐) โ ๐ โ โค) |
52 | 11 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ยฌ 2 โฅ ๐) โ ๐ โ โ) |
53 | | simpr 486 |
. . . . . . . 8
โข ((๐ โง ยฌ 2 โฅ ๐) โ ยฌ 2 โฅ ๐) |
54 | 1, 2, 20, 49, 50, 51, 52, 53 | knoppndvlem9 35029 |
. . . . . . 7
โข ((๐ โง ยฌ 2 โฅ ๐) โ ((๐นโ๐ด)โ๐ฝ) = ((๐ถโ๐ฝ) / 2)) |
55 | 9 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ยฌ 2 โฅ ๐) โ (๐ + 1) โ โค) |
56 | 51, 16 | syl 17 |
. . . . . . . . 9
โข ((๐ โง ยฌ 2 โฅ ๐) โ (ยฌ 2 โฅ ๐ โ 2 โฅ (๐ + 1))) |
57 | 53, 56 | mpbid 231 |
. . . . . . . 8
โข ((๐ โง ยฌ 2 โฅ ๐) โ 2 โฅ (๐ + 1)) |
58 | 1, 2, 3, 49, 50, 55, 52, 57 | knoppndvlem8 35028 |
. . . . . . 7
โข ((๐ โง ยฌ 2 โฅ ๐) โ ((๐นโ๐ต)โ๐ฝ) = 0) |
59 | 54, 58 | oveq12d 7376 |
. . . . . 6
โข ((๐ โง ยฌ 2 โฅ ๐) โ (((๐นโ๐ด)โ๐ฝ) โ ((๐นโ๐ต)โ๐ฝ)) = (((๐ถโ๐ฝ) / 2) โ 0)) |
60 | 32 | adantr 482 |
. . . . . 6
โข ((๐ โง ยฌ 2 โฅ ๐) โ (((๐ถโ๐ฝ) / 2) โ 0) = ((๐ถโ๐ฝ) / 2)) |
61 | 59, 60 | eqtrd 2773 |
. . . . 5
โข ((๐ โง ยฌ 2 โฅ ๐) โ (((๐นโ๐ด)โ๐ฝ) โ ((๐นโ๐ต)โ๐ฝ)) = ((๐ถโ๐ฝ) / 2)) |
62 | 61 | fveq2d 6847 |
. . . 4
โข ((๐ โง ยฌ 2 โฅ ๐) โ (absโ(((๐นโ๐ด)โ๐ฝ) โ ((๐นโ๐ต)โ๐ฝ))) = (absโ((๐ถโ๐ฝ) / 2))) |
63 | 48, 62 | eqtrd 2773 |
. . 3
โข ((๐ โง ยฌ 2 โฅ ๐) โ (absโ(((๐นโ๐ต)โ๐ฝ) โ ((๐นโ๐ด)โ๐ฝ))) = (absโ((๐ถโ๐ฝ) / 2))) |
64 | 35, 63 | pm2.61dan 812 |
. 2
โข (๐ โ (absโ(((๐นโ๐ต)โ๐ฝ) โ ((๐นโ๐ด)โ๐ฝ))) = (absโ((๐ถโ๐ฝ) / 2))) |
65 | 27, 28, 30 | absdivd 15346 |
. . 3
โข (๐ โ (absโ((๐ถโ๐ฝ) / 2)) = ((absโ(๐ถโ๐ฝ)) / (absโ2))) |
66 | 26, 6 | absexpd 15343 |
. . . 4
โข (๐ โ (absโ(๐ถโ๐ฝ)) = ((absโ๐ถ)โ๐ฝ)) |
67 | | 0le2 12260 |
. . . . . 6
โข 0 โค
2 |
68 | | 2re 12232 |
. . . . . . 7
โข 2 โ
โ |
69 | 68 | absidi 15268 |
. . . . . 6
โข (0 โค 2
โ (absโ2) = 2) |
70 | 67, 69 | ax-mp 5 |
. . . . 5
โข
(absโ2) = 2 |
71 | 70 | a1i 11 |
. . . 4
โข (๐ โ (absโ2) =
2) |
72 | 66, 71 | oveq12d 7376 |
. . 3
โข (๐ โ ((absโ(๐ถโ๐ฝ)) / (absโ2)) = (((absโ๐ถ)โ๐ฝ) / 2)) |
73 | 65, 72 | eqtrd 2773 |
. 2
โข (๐ โ (absโ((๐ถโ๐ฝ) / 2)) = (((absโ๐ถ)โ๐ฝ) / 2)) |
74 | 64, 73 | eqtrd 2773 |
1
โข (๐ โ (absโ(((๐นโ๐ต)โ๐ฝ) โ ((๐นโ๐ด)โ๐ฝ))) = (((absโ๐ถ)โ๐ฝ) / 2)) |