Step | Hyp | Ref
| Expression |
1 | | picn 25960 |
. . . . . . 7
โข ฯ
โ โ |
2 | | 2re 12282 |
. . . . . . . . . 10
โข 2 โ
โ |
3 | | pire 25959 |
. . . . . . . . . 10
โข ฯ
โ โ |
4 | 2, 3 | remulcli 11226 |
. . . . . . . . 9
โข (2
ยท ฯ) โ โ |
5 | 4 | recni 11224 |
. . . . . . . 8
โข (2
ยท ฯ) โ โ |
6 | | 2pos 12311 |
. . . . . . . . . 10
โข 0 <
2 |
7 | | pipos 25961 |
. . . . . . . . . 10
โข 0 <
ฯ |
8 | 2, 3, 6, 7 | mulgt0ii 11343 |
. . . . . . . . 9
โข 0 < (2
ยท ฯ) |
9 | 4, 8 | gt0ne0ii 11746 |
. . . . . . . 8
โข (2
ยท ฯ) โ 0 |
10 | 5, 9 | pm3.2i 471 |
. . . . . . 7
โข ((2
ยท ฯ) โ โ โง (2 ยท ฯ) โ 0) |
11 | | ax-icn 11165 |
. . . . . . . 8
โข i โ
โ |
12 | | ine0 11645 |
. . . . . . . 8
โข i โ
0 |
13 | 11, 12 | pm3.2i 471 |
. . . . . . 7
โข (i โ
โ โง i โ 0) |
14 | | divcan5 11912 |
. . . . . . 7
โข ((ฯ
โ โ โง ((2 ยท ฯ) โ โ โง (2 ยท ฯ)
โ 0) โง (i โ โ โง i โ 0)) โ ((i ยท ฯ) / (i
ยท (2 ยท ฯ))) = (ฯ / (2 ยท ฯ))) |
15 | 1, 10, 13, 14 | mp3an 1461 |
. . . . . 6
โข ((i
ยท ฯ) / (i ยท (2 ยท ฯ))) = (ฯ / (2 ยท
ฯ)) |
16 | 3, 7 | gt0ne0ii 11746 |
. . . . . . 7
โข ฯ โ
0 |
17 | | recdiv 11916 |
. . . . . . 7
โข ((((2
ยท ฯ) โ โ โง (2 ยท ฯ) โ 0) โง (ฯ
โ โ โง ฯ โ 0)) โ (1 / ((2 ยท ฯ) / ฯ)) =
(ฯ / (2 ยท ฯ))) |
18 | 5, 9, 1, 16, 17 | mp4an 691 |
. . . . . 6
โข (1 / ((2
ยท ฯ) / ฯ)) = (ฯ / (2 ยท ฯ)) |
19 | 2 | recni 11224 |
. . . . . . . 8
โข 2 โ
โ |
20 | 19, 1, 16 | divcan4i 11957 |
. . . . . . 7
โข ((2
ยท ฯ) / ฯ) = 2 |
21 | 20 | oveq2i 7416 |
. . . . . 6
โข (1 / ((2
ยท ฯ) / ฯ)) = (1 / 2) |
22 | 15, 18, 21 | 3eqtr2i 2766 |
. . . . 5
โข ((i
ยท ฯ) / (i ยท (2 ยท ฯ))) = (1 / 2) |
23 | 22 | oveq2i 7416 |
. . . 4
โข ((๐ / (i ยท (2 ยท
ฯ))) โ ((i ยท ฯ) / (i ยท (2 ยท ฯ)))) = ((๐ / (i ยท (2 ยท
ฯ))) โ (1 / 2)) |
24 | | ang180lem1.2 |
. . . . . 6
โข ๐ = (((logโ(1 / (1 โ
๐ด))) + (logโ((๐ด โ 1) / ๐ด))) + (logโ๐ด)) |
25 | | ax-1cn 11164 |
. . . . . . . . . . 11
โข 1 โ
โ |
26 | | simp1 1136 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ๐ด โ โ) |
27 | | subcl 11455 |
. . . . . . . . . . 11
โข ((1
โ โ โง ๐ด
โ โ) โ (1 โ ๐ด) โ โ) |
28 | 25, 26, 27 | sylancr 587 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (1 โ ๐ด) โ โ) |
29 | | simp3 1138 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ๐ด โ 1) |
30 | 29 | necomd 2996 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ 1 โ ๐ด) |
31 | | subeq0 11482 |
. . . . . . . . . . . . 13
โข ((1
โ โ โง ๐ด
โ โ) โ ((1 โ ๐ด) = 0 โ 1 = ๐ด)) |
32 | 25, 26, 31 | sylancr 587 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ((1 โ ๐ด) = 0 โ 1 = ๐ด)) |
33 | 32 | necon3bid 2985 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ((1 โ ๐ด) โ 0 โ 1 โ ๐ด)) |
34 | 30, 33 | mpbird 256 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (1 โ ๐ด) โ 0) |
35 | 28, 34 | reccld 11979 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (1 / (1 โ ๐ด)) โ
โ) |
36 | 28, 34 | recne0d 11980 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (1 / (1 โ ๐ด)) โ 0) |
37 | 35, 36 | logcld 26070 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (logโ(1 / (1 โ
๐ด))) โ
โ) |
38 | | subcl 11455 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง 1 โ
โ) โ (๐ด โ
1) โ โ) |
39 | 26, 25, 38 | sylancl 586 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (๐ด โ 1) โ โ) |
40 | | simp2 1137 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ๐ด โ 0) |
41 | 39, 26, 40 | divcld 11986 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ((๐ด โ 1) / ๐ด) โ โ) |
42 | | subeq0 11482 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ โง 1 โ
โ) โ ((๐ด โ
1) = 0 โ ๐ด =
1)) |
43 | 26, 25, 42 | sylancl 586 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ((๐ด โ 1) = 0 โ ๐ด = 1)) |
44 | 43 | necon3bid 2985 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ((๐ด โ 1) โ 0 โ ๐ด โ 1)) |
45 | 29, 44 | mpbird 256 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (๐ด โ 1) โ 0) |
46 | 39, 26, 45, 40 | divne0d 12002 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ((๐ด โ 1) / ๐ด) โ 0) |
47 | 41, 46 | logcld 26070 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (logโ((๐ด โ 1) / ๐ด)) โ โ) |
48 | 37, 47 | addcld 11229 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ((logโ(1 / (1 โ
๐ด))) + (logโ((๐ด โ 1) / ๐ด))) โ โ) |
49 | 26, 40 | logcld 26070 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (logโ๐ด) โ โ) |
50 | 48, 49 | addcld 11229 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (((logโ(1 / (1 โ
๐ด))) + (logโ((๐ด โ 1) / ๐ด))) + (logโ๐ด)) โ โ) |
51 | 24, 50 | eqeltrid 2837 |
. . . . 5
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ๐ โ โ) |
52 | 11, 1 | mulcli 11217 |
. . . . . 6
โข (i
ยท ฯ) โ โ |
53 | 52 | a1i 11 |
. . . . 5
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (i ยท ฯ) โ
โ) |
54 | 11, 5 | mulcli 11217 |
. . . . . 6
โข (i
ยท (2 ยท ฯ)) โ โ |
55 | 54 | a1i 11 |
. . . . 5
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (i ยท (2 ยท
ฯ)) โ โ) |
56 | 11, 5, 12, 9 | mulne0i 11853 |
. . . . . 6
โข (i
ยท (2 ยท ฯ)) โ 0 |
57 | 56 | a1i 11 |
. . . . 5
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (i ยท (2 ยท
ฯ)) โ 0) |
58 | 51, 53, 55, 57 | divsubdird 12025 |
. . . 4
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ((๐ โ (i ยท ฯ)) / (i ยท (2
ยท ฯ))) = ((๐ / (i
ยท (2 ยท ฯ))) โ ((i ยท ฯ) / (i ยท (2
ยท ฯ))))) |
59 | | ang180lem1.3 |
. . . . 5
โข ๐ = (((๐ / i) / (2 ยท ฯ)) โ (1 /
2)) |
60 | 13 | a1i 11 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (i โ โ โง i
โ 0)) |
61 | 10 | a1i 11 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ((2 ยท ฯ) โ
โ โง (2 ยท ฯ) โ 0)) |
62 | | divdiv1 11921 |
. . . . . . 7
โข ((๐ โ โ โง (i โ
โ โง i โ 0) โง ((2 ยท ฯ) โ โ โง (2
ยท ฯ) โ 0)) โ ((๐ / i) / (2 ยท ฯ)) = (๐ / (i ยท (2 ยท
ฯ)))) |
63 | 51, 60, 61, 62 | syl3anc 1371 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ((๐ / i) / (2 ยท ฯ)) = (๐ / (i ยท (2 ยท
ฯ)))) |
64 | 63 | oveq1d 7420 |
. . . . 5
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (((๐ / i) / (2 ยท ฯ)) โ (1 / 2))
= ((๐ / (i ยท (2
ยท ฯ))) โ (1 / 2))) |
65 | 59, 64 | eqtrid 2784 |
. . . 4
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ๐ = ((๐ / (i ยท (2 ยท ฯ))) โ
(1 / 2))) |
66 | 23, 58, 65 | 3eqtr4a 2798 |
. . 3
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ((๐ โ (i ยท ฯ)) / (i ยท (2
ยท ฯ))) = ๐) |
67 | | efsub 16039 |
. . . . . 6
โข ((๐ โ โ โง (i
ยท ฯ) โ โ) โ (expโ(๐ โ (i ยท ฯ))) =
((expโ๐) /
(expโ(i ยท ฯ)))) |
68 | 51, 52, 67 | sylancl 586 |
. . . . 5
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (expโ(๐ โ (i ยท ฯ))) =
((expโ๐) /
(expโ(i ยท ฯ)))) |
69 | | efipi 25974 |
. . . . . . 7
โข
(expโ(i ยท ฯ)) = -1 |
70 | 69 | oveq2i 7416 |
. . . . . 6
โข
((expโ๐) /
(expโ(i ยท ฯ))) = ((expโ๐) / -1) |
71 | 24 | fveq2i 6891 |
. . . . . . . . 9
โข
(expโ๐) =
(expโ(((logโ(1 / (1 โ ๐ด))) + (logโ((๐ด โ 1) / ๐ด))) + (logโ๐ด))) |
72 | | efadd 16033 |
. . . . . . . . . . 11
โข
((((logโ(1 / (1 โ ๐ด))) + (logโ((๐ด โ 1) / ๐ด))) โ โ โง (logโ๐ด) โ โ) โ
(expโ(((logโ(1 / (1 โ ๐ด))) + (logโ((๐ด โ 1) / ๐ด))) + (logโ๐ด))) = ((expโ((logโ(1 / (1
โ ๐ด))) +
(logโ((๐ด โ 1) /
๐ด)))) ยท
(expโ(logโ๐ด)))) |
73 | 48, 49, 72 | syl2anc 584 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (expโ(((logโ(1 /
(1 โ ๐ด))) +
(logโ((๐ด โ 1) /
๐ด))) + (logโ๐ด))) = ((expโ((logโ(1
/ (1 โ ๐ด))) +
(logโ((๐ด โ 1) /
๐ด)))) ยท
(expโ(logโ๐ด)))) |
74 | | efadd 16033 |
. . . . . . . . . . . . 13
โข
(((logโ(1 / (1 โ ๐ด))) โ โ โง (logโ((๐ด โ 1) / ๐ด)) โ โ) โ
(expโ((logโ(1 / (1 โ ๐ด))) + (logโ((๐ด โ 1) / ๐ด)))) = ((expโ(logโ(1 / (1
โ ๐ด)))) ยท
(expโ(logโ((๐ด
โ 1) / ๐ด))))) |
75 | 37, 47, 74 | syl2anc 584 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (expโ((logโ(1 /
(1 โ ๐ด))) +
(logโ((๐ด โ 1) /
๐ด)))) =
((expโ(logโ(1 / (1 โ ๐ด)))) ยท (expโ(logโ((๐ด โ 1) / ๐ด))))) |
76 | | eflog 26076 |
. . . . . . . . . . . . . 14
โข (((1 / (1
โ ๐ด)) โ โ
โง (1 / (1 โ ๐ด))
โ 0) โ (expโ(logโ(1 / (1 โ ๐ด)))) = (1 / (1 โ ๐ด))) |
77 | 35, 36, 76 | syl2anc 584 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (expโ(logโ(1 /
(1 โ ๐ด)))) = (1 / (1
โ ๐ด))) |
78 | | eflog 26076 |
. . . . . . . . . . . . . 14
โข ((((๐ด โ 1) / ๐ด) โ โ โง ((๐ด โ 1) / ๐ด) โ 0) โ
(expโ(logโ((๐ด
โ 1) / ๐ด))) = ((๐ด โ 1) / ๐ด)) |
79 | 41, 46, 78 | syl2anc 584 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ
(expโ(logโ((๐ด
โ 1) / ๐ด))) = ((๐ด โ 1) / ๐ด)) |
80 | 77, 79 | oveq12d 7423 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ((expโ(logโ(1 /
(1 โ ๐ด)))) ยท
(expโ(logโ((๐ด
โ 1) / ๐ด)))) = ((1 /
(1 โ ๐ด)) ยท
((๐ด โ 1) / ๐ด))) |
81 | 35, 41 | mulcomd 11231 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ((1 / (1 โ ๐ด)) ยท ((๐ด โ 1) / ๐ด)) = (((๐ด โ 1) / ๐ด) ยท (1 / (1 โ ๐ด)))) |
82 | 25 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ 1 โ
โ) |
83 | 82, 28, 34 | div2negd 12001 |
. . . . . . . . . . . . . . 15
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (-1 / -(1 โ ๐ด)) = (1 / (1 โ ๐ด))) |
84 | | negsubdi2 11515 |
. . . . . . . . . . . . . . . . 17
โข ((1
โ โ โง ๐ด
โ โ) โ -(1 โ ๐ด) = (๐ด โ 1)) |
85 | 25, 26, 84 | sylancr 587 |
. . . . . . . . . . . . . . . 16
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ -(1 โ ๐ด) = (๐ด โ 1)) |
86 | 85 | oveq2d 7421 |
. . . . . . . . . . . . . . 15
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (-1 / -(1 โ ๐ด)) = (-1 / (๐ด โ 1))) |
87 | 83, 86 | eqtr3d 2774 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (1 / (1 โ ๐ด)) = (-1 / (๐ด โ 1))) |
88 | 87 | oveq2d 7421 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (((๐ด โ 1) / ๐ด) ยท (1 / (1 โ ๐ด))) = (((๐ด โ 1) / ๐ด) ยท (-1 / (๐ด โ 1)))) |
89 | | neg1cn 12322 |
. . . . . . . . . . . . . . 15
โข -1 โ
โ |
90 | 89 | a1i 11 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ -1 โ
โ) |
91 | 90, 39, 26, 45, 40 | dmdcand 12015 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (((๐ด โ 1) / ๐ด) ยท (-1 / (๐ด โ 1))) = (-1 / ๐ด)) |
92 | 81, 88, 91 | 3eqtrd 2776 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ((1 / (1 โ ๐ด)) ยท ((๐ด โ 1) / ๐ด)) = (-1 / ๐ด)) |
93 | 75, 80, 92 | 3eqtrd 2776 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (expโ((logโ(1 /
(1 โ ๐ด))) +
(logโ((๐ด โ 1) /
๐ด)))) = (-1 / ๐ด)) |
94 | | eflog 26076 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ด โ 0) โ
(expโ(logโ๐ด)) =
๐ด) |
95 | 26, 40, 94 | syl2anc 584 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (expโ(logโ๐ด)) = ๐ด) |
96 | 93, 95 | oveq12d 7423 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ((expโ((logโ(1 /
(1 โ ๐ด))) +
(logโ((๐ด โ 1) /
๐ด)))) ยท
(expโ(logโ๐ด)))
= ((-1 / ๐ด) ยท ๐ด)) |
97 | 90, 26, 40 | divcan1d 11987 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ((-1 / ๐ด) ยท ๐ด) = -1) |
98 | 73, 96, 97 | 3eqtrd 2776 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (expโ(((logโ(1 /
(1 โ ๐ด))) +
(logโ((๐ด โ 1) /
๐ด))) + (logโ๐ด))) = -1) |
99 | 71, 98 | eqtrid 2784 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (expโ๐) = -1) |
100 | 99 | oveq1d 7420 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ((expโ๐) / -1) = (-1 /
-1)) |
101 | | neg1ne0 12324 |
. . . . . . . 8
โข -1 โ
0 |
102 | 89, 101 | dividi 11943 |
. . . . . . 7
โข (-1 / -1)
= 1 |
103 | 100, 102 | eqtrdi 2788 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ((expโ๐) / -1) = 1) |
104 | 70, 103 | eqtrid 2784 |
. . . . 5
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ((expโ๐) / (expโ(i ยท
ฯ))) = 1) |
105 | 68, 104 | eqtrd 2772 |
. . . 4
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (expโ(๐ โ (i ยท ฯ))) =
1) |
106 | | subcl 11455 |
. . . . . 6
โข ((๐ โ โ โง (i
ยท ฯ) โ โ) โ (๐ โ (i ยท ฯ)) โ
โ) |
107 | 51, 52, 106 | sylancl 586 |
. . . . 5
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (๐ โ (i ยท ฯ)) โ
โ) |
108 | | efeq1 26028 |
. . . . 5
โข ((๐ โ (i ยท ฯ))
โ โ โ ((expโ(๐ โ (i ยท ฯ))) = 1 โ
((๐ โ (i ยท
ฯ)) / (i ยท (2 ยท ฯ))) โ โค)) |
109 | 107, 108 | syl 17 |
. . . 4
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ((expโ(๐ โ (i ยท ฯ))) = 1
โ ((๐ โ (i
ยท ฯ)) / (i ยท (2 ยท ฯ))) โ
โค)) |
110 | 105, 109 | mpbid 231 |
. . 3
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ((๐ โ (i ยท ฯ)) / (i ยท (2
ยท ฯ))) โ โค) |
111 | 66, 110 | eqeltrrd 2834 |
. 2
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ๐ โ โค) |
112 | 11 | a1i 11 |
. . . . 5
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ i โ
โ) |
113 | 12 | a1i 11 |
. . . . 5
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ i โ 0) |
114 | 51, 112, 113 | divcld 11986 |
. . . 4
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (๐ / i) โ โ) |
115 | 5 | a1i 11 |
. . . 4
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (2 ยท ฯ) โ
โ) |
116 | 9 | a1i 11 |
. . . 4
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (2 ยท ฯ) โ
0) |
117 | 114, 115,
116 | divcan1d 11987 |
. . 3
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (((๐ / i) / (2 ยท ฯ)) ยท (2
ยท ฯ)) = (๐ /
i)) |
118 | 59 | oveq1i 7415 |
. . . . . 6
โข (๐ + (1 / 2)) = ((((๐ / i) / (2 ยท ฯ))
โ (1 / 2)) + (1 / 2)) |
119 | 114, 115,
116 | divcld 11986 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ((๐ / i) / (2 ยท ฯ)) โ
โ) |
120 | | halfre 12422 |
. . . . . . . 8
โข (1 / 2)
โ โ |
121 | 120 | recni 11224 |
. . . . . . 7
โข (1 / 2)
โ โ |
122 | | npcan 11465 |
. . . . . . 7
โข ((((๐ / i) / (2 ยท ฯ))
โ โ โง (1 / 2) โ โ) โ ((((๐ / i) / (2 ยท ฯ)) โ (1 / 2))
+ (1 / 2)) = ((๐ / i) / (2
ยท ฯ))) |
123 | 119, 121,
122 | sylancl 586 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ((((๐ / i) / (2 ยท ฯ)) โ (1 / 2))
+ (1 / 2)) = ((๐ / i) / (2
ยท ฯ))) |
124 | 118, 123 | eqtrid 2784 |
. . . . 5
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (๐ + (1 / 2)) = ((๐ / i) / (2 ยท ฯ))) |
125 | 111 | zred 12662 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ๐ โ โ) |
126 | | readdcl 11189 |
. . . . . 6
โข ((๐ โ โ โง (1 / 2)
โ โ) โ (๐ +
(1 / 2)) โ โ) |
127 | 125, 120,
126 | sylancl 586 |
. . . . 5
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (๐ + (1 / 2)) โ โ) |
128 | 124, 127 | eqeltrrd 2834 |
. . . 4
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ((๐ / i) / (2 ยท ฯ)) โ
โ) |
129 | | remulcl 11191 |
. . . 4
โข ((((๐ / i) / (2 ยท ฯ))
โ โ โง (2 ยท ฯ) โ โ) โ (((๐ / i) / (2 ยท ฯ))
ยท (2 ยท ฯ)) โ โ) |
130 | 128, 4, 129 | sylancl 586 |
. . 3
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (((๐ / i) / (2 ยท ฯ)) ยท (2
ยท ฯ)) โ โ) |
131 | 117, 130 | eqeltrrd 2834 |
. 2
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (๐ / i) โ โ) |
132 | 111, 131 | jca 512 |
1
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (๐ โ โค โง (๐ / i) โ โ)) |