Step | Hyp | Ref
| Expression |
1 | | recn 11148 |
. . . 4
โข (๐ด โ โ โ ๐ด โ
โ) |
2 | | ax-icn 11117 |
. . . . 5
โข i โ
โ |
3 | | recn 11148 |
. . . . 5
โข (๐ต โ โ โ ๐ต โ
โ) |
4 | | mulcl 11142 |
. . . . 5
โข ((i
โ โ โง ๐ต
โ โ) โ (i ยท ๐ต) โ โ) |
5 | 2, 3, 4 | sylancr 588 |
. . . 4
โข (๐ต โ โ โ (i
ยท ๐ต) โ
โ) |
6 | | addcl 11140 |
. . . 4
โข ((๐ด โ โ โง (i
ยท ๐ต) โ โ)
โ (๐ด + (i ยท
๐ต)) โ
โ) |
7 | 1, 5, 6 | syl2an 597 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด + (i ยท ๐ต)) โ โ) |
8 | | reval 14998 |
. . 3
โข ((๐ด + (i ยท ๐ต)) โ โ โ
(โโ(๐ด + (i
ยท ๐ต))) = (((๐ด + (i ยท ๐ต)) + (โโ(๐ด + (i ยท ๐ต)))) / 2)) |
9 | 7, 8 | syl 17 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ(๐ด + (i
ยท ๐ต))) = (((๐ด + (i ยท ๐ต)) + (โโ(๐ด + (i ยท ๐ต)))) / 2)) |
10 | | cjcl 14997 |
. . . . . 6
โข ((๐ด + (i ยท ๐ต)) โ โ โ
(โโ(๐ด + (i
ยท ๐ต))) โ
โ) |
11 | 7, 10 | syl 17 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ(๐ด + (i
ยท ๐ต))) โ
โ) |
12 | 7, 11 | addcld 11181 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด + (i ยท ๐ต)) + (โโ(๐ด + (i ยท ๐ต)))) โ โ) |
13 | 12 | halfcld 12405 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐ด + (i ยท ๐ต)) + (โโ(๐ด + (i ยท ๐ต)))) / 2) โ โ) |
14 | 1 | adantr 482 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ ๐ด โ
โ) |
15 | | recl 15002 |
. . . . . . 7
โข ((๐ด + (i ยท ๐ต)) โ โ โ
(โโ(๐ด + (i
ยท ๐ต))) โ
โ) |
16 | 7, 15 | syl 17 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ(๐ด + (i
ยท ๐ต))) โ
โ) |
17 | 9, 16 | eqeltrrd 2839 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐ด + (i ยท ๐ต)) + (โโ(๐ด + (i ยท ๐ต)))) / 2) โ โ) |
18 | | simpl 484 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ ๐ด โ
โ) |
19 | 17, 18 | resubcld 11590 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ
((((๐ด + (i ยท ๐ต)) + (โโ(๐ด + (i ยท ๐ต)))) / 2) โ ๐ด) โ โ) |
20 | 2 | a1i 11 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ i โ
โ) |
21 | 3 | adantl 483 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ ๐ต โ
โ) |
22 | 2, 21, 4 | sylancr 588 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ (i
ยท ๐ต) โ
โ) |
23 | 7, 11 | subcld 11519 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด + (i ยท ๐ต)) โ (โโ(๐ด + (i ยท ๐ต)))) โ โ) |
24 | 23 | halfcld 12405 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐ด + (i ยท ๐ต)) โ (โโ(๐ด + (i ยท ๐ต)))) / 2) โ โ) |
25 | 20, 22, 24 | subdid 11618 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ (i
ยท ((i ยท ๐ต)
โ (((๐ด + (i ยท
๐ต)) โ
(โโ(๐ด + (i
ยท ๐ต)))) / 2))) = ((i
ยท (i ยท ๐ต))
โ (i ยท (((๐ด +
(i ยท ๐ต)) โ
(โโ(๐ด + (i
ยท ๐ต)))) /
2)))) |
26 | 14, 22, 14 | pnpcand 11556 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด + (i ยท ๐ต)) โ (๐ด + ๐ด)) = ((i ยท ๐ต) โ ๐ด)) |
27 | 22, 14, 22 | pnpcan2d 11557 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โ โง ๐ต โ โ) โ (((i
ยท ๐ต) + (i ยท
๐ต)) โ (๐ด + (i ยท ๐ต))) = ((i ยท ๐ต) โ ๐ด)) |
28 | 26, 27 | eqtr4d 2780 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด + (i ยท ๐ต)) โ (๐ด + ๐ด)) = (((i ยท ๐ต) + (i ยท ๐ต)) โ (๐ด + (i ยท ๐ต)))) |
29 | 28 | oveq1d 7377 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐ด + (i ยท ๐ต)) โ (๐ด + ๐ด)) + (โโ(๐ด + (i ยท ๐ต)))) = ((((i ยท ๐ต) + (i ยท ๐ต)) โ (๐ด + (i ยท ๐ต))) + (โโ(๐ด + (i ยท ๐ต))))) |
30 | 14, 14 | addcld 11181 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด + ๐ด) โ โ) |
31 | 7, 11, 30 | addsubd 11540 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐ด + (i ยท ๐ต)) + (โโ(๐ด + (i ยท ๐ต)))) โ (๐ด + ๐ด)) = (((๐ด + (i ยท ๐ต)) โ (๐ด + ๐ด)) + (โโ(๐ด + (i ยท ๐ต))))) |
32 | 22, 22 | addcld 11181 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ โง ๐ต โ โ) โ ((i
ยท ๐ต) + (i ยท
๐ต)) โ
โ) |
33 | 32, 7, 11 | subsubd 11547 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ต โ โ) โ (((i
ยท ๐ต) + (i ยท
๐ต)) โ ((๐ด + (i ยท ๐ต)) โ (โโ(๐ด + (i ยท ๐ต))))) = ((((i ยท ๐ต) + (i ยท ๐ต)) โ (๐ด + (i ยท ๐ต))) + (โโ(๐ด + (i ยท ๐ต))))) |
34 | 29, 31, 33 | 3eqtr4d 2787 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐ด + (i ยท ๐ต)) + (โโ(๐ด + (i ยท ๐ต)))) โ (๐ด + ๐ด)) = (((i ยท ๐ต) + (i ยท ๐ต)) โ ((๐ด + (i ยท ๐ต)) โ (โโ(๐ด + (i ยท ๐ต)))))) |
35 | 14 | 2timesd 12403 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ต โ โ) โ (2
ยท ๐ด) = (๐ด + ๐ด)) |
36 | 35 | oveq2d 7378 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐ด + (i ยท ๐ต)) + (โโ(๐ด + (i ยท ๐ต)))) โ (2 ยท ๐ด)) = (((๐ด + (i ยท ๐ต)) + (โโ(๐ด + (i ยท ๐ต)))) โ (๐ด + ๐ด))) |
37 | 22 | 2timesd 12403 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ต โ โ) โ (2
ยท (i ยท ๐ต)) =
((i ยท ๐ต) + (i
ยท ๐ต))) |
38 | 37 | oveq1d 7377 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ต โ โ) โ ((2
ยท (i ยท ๐ต))
โ ((๐ด + (i ยท
๐ต)) โ
(โโ(๐ด + (i
ยท ๐ต))))) = (((i
ยท ๐ต) + (i ยท
๐ต)) โ ((๐ด + (i ยท ๐ต)) โ (โโ(๐ด + (i ยท ๐ต)))))) |
39 | 34, 36, 38 | 3eqtr4d 2787 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐ด + (i ยท ๐ต)) + (โโ(๐ด + (i ยท ๐ต)))) โ (2 ยท ๐ด)) = ((2 ยท (i ยท ๐ต)) โ ((๐ด + (i ยท ๐ต)) โ (โโ(๐ด + (i ยท ๐ต)))))) |
40 | 39 | oveq1d 7377 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ) โ
((((๐ด + (i ยท ๐ต)) + (โโ(๐ด + (i ยท ๐ต)))) โ (2 ยท ๐ด)) / 2) = (((2 ยท (i ยท ๐ต)) โ ((๐ด + (i ยท ๐ต)) โ (โโ(๐ด + (i ยท ๐ต))))) / 2)) |
41 | | 2cn 12235 |
. . . . . . . . . . 11
โข 2 โ
โ |
42 | | mulcl 11142 |
. . . . . . . . . . 11
โข ((2
โ โ โง ๐ด
โ โ) โ (2 ยท ๐ด) โ โ) |
43 | 41, 14, 42 | sylancr 588 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ) โ (2
ยท ๐ด) โ
โ) |
44 | 41 | a1i 11 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ) โ 2 โ
โ) |
45 | | 2ne0 12264 |
. . . . . . . . . . 11
โข 2 โ
0 |
46 | 45 | a1i 11 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ) โ 2 โ
0) |
47 | 12, 43, 44, 46 | divsubdird 11977 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ) โ
((((๐ด + (i ยท ๐ต)) + (โโ(๐ด + (i ยท ๐ต)))) โ (2 ยท ๐ด)) / 2) = ((((๐ด + (i ยท ๐ต)) + (โโ(๐ด + (i ยท ๐ต)))) / 2) โ ((2 ยท ๐ด) / 2))) |
48 | | mulcl 11142 |
. . . . . . . . . . 11
โข ((2
โ โ โง (i ยท ๐ต) โ โ) โ (2 ยท (i
ยท ๐ต)) โ
โ) |
49 | 41, 22, 48 | sylancr 588 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ) โ (2
ยท (i ยท ๐ต))
โ โ) |
50 | 49, 23, 44, 46 | divsubdird 11977 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ) โ (((2
ยท (i ยท ๐ต))
โ ((๐ด + (i ยท
๐ต)) โ
(โโ(๐ด + (i
ยท ๐ต))))) / 2) = (((2
ยท (i ยท ๐ต)) /
2) โ (((๐ด + (i
ยท ๐ต)) โ
(โโ(๐ด + (i
ยท ๐ต)))) /
2))) |
51 | 40, 47, 50 | 3eqtr3d 2785 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ
((((๐ด + (i ยท ๐ต)) + (โโ(๐ด + (i ยท ๐ต)))) / 2) โ ((2 ยท ๐ด) / 2)) = (((2 ยท (i
ยท ๐ต)) / 2) โ
(((๐ด + (i ยท ๐ต)) โ
(โโ(๐ด + (i
ยท ๐ต)))) /
2))) |
52 | 14, 44, 46 | divcan3d 11943 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ) โ ((2
ยท ๐ด) / 2) = ๐ด) |
53 | 52 | oveq2d 7378 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ
((((๐ด + (i ยท ๐ต)) + (โโ(๐ด + (i ยท ๐ต)))) / 2) โ ((2 ยท ๐ด) / 2)) = ((((๐ด + (i ยท ๐ต)) + (โโ(๐ด + (i ยท ๐ต)))) / 2) โ ๐ด)) |
54 | 22, 44, 46 | divcan3d 11943 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ) โ ((2
ยท (i ยท ๐ต)) /
2) = (i ยท ๐ต)) |
55 | 54 | oveq1d 7377 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ (((2
ยท (i ยท ๐ต)) /
2) โ (((๐ด + (i
ยท ๐ต)) โ
(โโ(๐ด + (i
ยท ๐ต)))) / 2)) = ((i
ยท ๐ต) โ
(((๐ด + (i ยท ๐ต)) โ
(โโ(๐ด + (i
ยท ๐ต)))) /
2))) |
56 | 51, 53, 55 | 3eqtr3d 2785 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ
((((๐ด + (i ยท ๐ต)) + (โโ(๐ด + (i ยท ๐ต)))) / 2) โ ๐ด) = ((i ยท ๐ต) โ (((๐ด + (i ยท ๐ต)) โ (โโ(๐ด + (i ยท ๐ต)))) / 2))) |
57 | 56 | oveq2d 7378 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ (i
ยท ((((๐ด + (i
ยท ๐ต)) +
(โโ(๐ด + (i
ยท ๐ต)))) / 2) โ
๐ด)) = (i ยท ((i
ยท ๐ต) โ
(((๐ด + (i ยท ๐ต)) โ
(โโ(๐ด + (i
ยท ๐ต)))) /
2)))) |
58 | 20, 20, 21 | mulassd 11185 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ ((i
ยท i) ยท ๐ต) =
(i ยท (i ยท ๐ต))) |
59 | 20, 23, 44, 46 | divassd 11973 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ ((i
ยท ((๐ด + (i ยท
๐ต)) โ
(โโ(๐ด + (i
ยท ๐ต))))) / 2) = (i
ยท (((๐ด + (i ยท
๐ต)) โ
(โโ(๐ด + (i
ยท ๐ต)))) /
2))) |
60 | 58, 59 | oveq12d 7380 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ (((i
ยท i) ยท ๐ต)
โ ((i ยท ((๐ด +
(i ยท ๐ต)) โ
(โโ(๐ด + (i
ยท ๐ต))))) / 2)) = ((i
ยท (i ยท ๐ต))
โ (i ยท (((๐ด +
(i ยท ๐ต)) โ
(โโ(๐ด + (i
ยท ๐ต)))) /
2)))) |
61 | 25, 57, 60 | 3eqtr4d 2787 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ (i
ยท ((((๐ด + (i
ยท ๐ต)) +
(โโ(๐ด + (i
ยท ๐ต)))) / 2) โ
๐ด)) = (((i ยท i)
ยท ๐ต) โ ((i
ยท ((๐ด + (i ยท
๐ต)) โ
(โโ(๐ด + (i
ยท ๐ต))))) /
2))) |
62 | | ixi 11791 |
. . . . . . . 8
โข (i
ยท i) = -1 |
63 | | neg1rr 12275 |
. . . . . . . 8
โข -1 โ
โ |
64 | 62, 63 | eqeltri 2834 |
. . . . . . 7
โข (i
ยท i) โ โ |
65 | | simpr 486 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ ๐ต โ
โ) |
66 | | remulcl 11143 |
. . . . . . 7
โข (((i
ยท i) โ โ โง ๐ต โ โ) โ ((i ยท i)
ยท ๐ต) โ
โ) |
67 | 64, 65, 66 | sylancr 588 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ ((i
ยท i) ยท ๐ต)
โ โ) |
68 | | cjth 14995 |
. . . . . . . . 9
โข ((๐ด + (i ยท ๐ต)) โ โ โ (((๐ด + (i ยท ๐ต)) + (โโ(๐ด + (i ยท ๐ต)))) โ โ โง (i ยท
((๐ด + (i ยท ๐ต)) โ
(โโ(๐ด + (i
ยท ๐ต))))) โ
โ)) |
69 | 68 | simprd 497 |
. . . . . . . 8
โข ((๐ด + (i ยท ๐ต)) โ โ โ (i ยท ((๐ด + (i ยท ๐ต)) โ (โโ(๐ด + (i ยท ๐ต))))) โ โ) |
70 | 7, 69 | syl 17 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ (i
ยท ((๐ด + (i ยท
๐ต)) โ
(โโ(๐ด + (i
ยท ๐ต))))) โ
โ) |
71 | 70 | rehalfcld 12407 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ ((i
ยท ((๐ด + (i ยท
๐ต)) โ
(โโ(๐ด + (i
ยท ๐ต))))) / 2) โ
โ) |
72 | 67, 71 | resubcld 11590 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ (((i
ยท i) ยท ๐ต)
โ ((i ยท ((๐ด +
(i ยท ๐ต)) โ
(โโ(๐ด + (i
ยท ๐ต))))) / 2))
โ โ) |
73 | 61, 72 | eqeltrd 2838 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ (i
ยท ((((๐ด + (i
ยท ๐ต)) +
(โโ(๐ด + (i
ยท ๐ต)))) / 2) โ
๐ด)) โ
โ) |
74 | | rimul 12151 |
. . . 4
โข
((((((๐ด + (i
ยท ๐ต)) +
(โโ(๐ด + (i
ยท ๐ต)))) / 2) โ
๐ด) โ โ โง (i
ยท ((((๐ด + (i
ยท ๐ต)) +
(โโ(๐ด + (i
ยท ๐ต)))) / 2) โ
๐ด)) โ โ) โ
((((๐ด + (i ยท ๐ต)) + (โโ(๐ด + (i ยท ๐ต)))) / 2) โ ๐ด) = 0) |
75 | 19, 73, 74 | syl2anc 585 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ
((((๐ด + (i ยท ๐ต)) + (โโ(๐ด + (i ยท ๐ต)))) / 2) โ ๐ด) = 0) |
76 | 13, 14, 75 | subeq0d 11527 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐ด + (i ยท ๐ต)) + (โโ(๐ด + (i ยท ๐ต)))) / 2) = ๐ด) |
77 | 9, 76 | eqtrd 2777 |
1
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ(๐ด + (i
ยท ๐ต))) = ๐ด) |