Step |
Hyp |
Ref |
Expression |
1 |
|
circum.1 |
|- A = ( ( 2 x. _pi ) / n ) |
2 |
|
circum.2 |
|- P = ( n e. NN |-> ( ( 2 x. n ) x. ( R x. ( sin ` ( A / 2 ) ) ) ) ) |
3 |
|
circum.3 |
|- R e. RR |
4 |
|
nnuz |
|- NN = ( ZZ>= ` 1 ) |
5 |
|
1zzd |
|- ( T. -> 1 e. ZZ ) |
6 |
|
pirp |
|- _pi e. RR+ |
7 |
|
nnrp |
|- ( n e. NN -> n e. RR+ ) |
8 |
|
rpdivcl |
|- ( ( _pi e. RR+ /\ n e. RR+ ) -> ( _pi / n ) e. RR+ ) |
9 |
6 7 8
|
sylancr |
|- ( n e. NN -> ( _pi / n ) e. RR+ ) |
10 |
9
|
rprene0d |
|- ( n e. NN -> ( ( _pi / n ) e. RR /\ ( _pi / n ) =/= 0 ) ) |
11 |
|
eldifsn |
|- ( ( _pi / n ) e. ( RR \ { 0 } ) <-> ( ( _pi / n ) e. RR /\ ( _pi / n ) =/= 0 ) ) |
12 |
10 11
|
sylibr |
|- ( n e. NN -> ( _pi / n ) e. ( RR \ { 0 } ) ) |
13 |
12
|
adantl |
|- ( ( T. /\ n e. NN ) -> ( _pi / n ) e. ( RR \ { 0 } ) ) |
14 |
|
eqidd |
|- ( T. -> ( n e. NN |-> ( _pi / n ) ) = ( n e. NN |-> ( _pi / n ) ) ) |
15 |
|
eqidd |
|- ( T. -> ( y e. ( RR \ { 0 } ) |-> ( ( sin ` y ) / y ) ) = ( y e. ( RR \ { 0 } ) |-> ( ( sin ` y ) / y ) ) ) |
16 |
|
fveq2 |
|- ( y = ( _pi / n ) -> ( sin ` y ) = ( sin ` ( _pi / n ) ) ) |
17 |
|
id |
|- ( y = ( _pi / n ) -> y = ( _pi / n ) ) |
18 |
16 17
|
oveq12d |
|- ( y = ( _pi / n ) -> ( ( sin ` y ) / y ) = ( ( sin ` ( _pi / n ) ) / ( _pi / n ) ) ) |
19 |
13 14 15 18
|
fmptco |
|- ( T. -> ( ( y e. ( RR \ { 0 } ) |-> ( ( sin ` y ) / y ) ) o. ( n e. NN |-> ( _pi / n ) ) ) = ( n e. NN |-> ( ( sin ` ( _pi / n ) ) / ( _pi / n ) ) ) ) |
20 |
|
eqid |
|- ( n e. NN |-> ( _pi / n ) ) = ( n e. NN |-> ( _pi / n ) ) |
21 |
20 12
|
fmpti |
|- ( n e. NN |-> ( _pi / n ) ) : NN --> ( RR \ { 0 } ) |
22 |
|
pire |
|- _pi e. RR |
23 |
22
|
recni |
|- _pi e. CC |
24 |
|
divcnv |
|- ( _pi e. CC -> ( n e. NN |-> ( _pi / n ) ) ~~> 0 ) |
25 |
23 24
|
mp1i |
|- ( T. -> ( n e. NN |-> ( _pi / n ) ) ~~> 0 ) |
26 |
|
sinccvg |
|- ( ( ( n e. NN |-> ( _pi / n ) ) : NN --> ( RR \ { 0 } ) /\ ( n e. NN |-> ( _pi / n ) ) ~~> 0 ) -> ( ( y e. ( RR \ { 0 } ) |-> ( ( sin ` y ) / y ) ) o. ( n e. NN |-> ( _pi / n ) ) ) ~~> 1 ) |
27 |
21 25 26
|
sylancr |
|- ( T. -> ( ( y e. ( RR \ { 0 } ) |-> ( ( sin ` y ) / y ) ) o. ( n e. NN |-> ( _pi / n ) ) ) ~~> 1 ) |
28 |
19 27
|
eqbrtrrd |
|- ( T. -> ( n e. NN |-> ( ( sin ` ( _pi / n ) ) / ( _pi / n ) ) ) ~~> 1 ) |
29 |
|
2re |
|- 2 e. RR |
30 |
29 22
|
remulcli |
|- ( 2 x. _pi ) e. RR |
31 |
30 3
|
remulcli |
|- ( ( 2 x. _pi ) x. R ) e. RR |
32 |
31
|
recni |
|- ( ( 2 x. _pi ) x. R ) e. CC |
33 |
32
|
a1i |
|- ( T. -> ( ( 2 x. _pi ) x. R ) e. CC ) |
34 |
|
nnex |
|- NN e. _V |
35 |
34
|
mptex |
|- ( n e. NN |-> ( ( 2 x. n ) x. ( R x. ( sin ` ( A / 2 ) ) ) ) ) e. _V |
36 |
2 35
|
eqeltri |
|- P e. _V |
37 |
36
|
a1i |
|- ( T. -> P e. _V ) |
38 |
|
eqid |
|- ( y e. ( RR \ { 0 } ) |-> ( ( sin ` y ) / y ) ) = ( y e. ( RR \ { 0 } ) |-> ( ( sin ` y ) / y ) ) |
39 |
|
eldifi |
|- ( y e. ( RR \ { 0 } ) -> y e. RR ) |
40 |
39
|
resincld |
|- ( y e. ( RR \ { 0 } ) -> ( sin ` y ) e. RR ) |
41 |
|
eldifsni |
|- ( y e. ( RR \ { 0 } ) -> y =/= 0 ) |
42 |
40 39 41
|
redivcld |
|- ( y e. ( RR \ { 0 } ) -> ( ( sin ` y ) / y ) e. RR ) |
43 |
38 42
|
fmpti |
|- ( y e. ( RR \ { 0 } ) |-> ( ( sin ` y ) / y ) ) : ( RR \ { 0 } ) --> RR |
44 |
|
fco |
|- ( ( ( y e. ( RR \ { 0 } ) |-> ( ( sin ` y ) / y ) ) : ( RR \ { 0 } ) --> RR /\ ( n e. NN |-> ( _pi / n ) ) : NN --> ( RR \ { 0 } ) ) -> ( ( y e. ( RR \ { 0 } ) |-> ( ( sin ` y ) / y ) ) o. ( n e. NN |-> ( _pi / n ) ) ) : NN --> RR ) |
45 |
43 21 44
|
mp2an |
|- ( ( y e. ( RR \ { 0 } ) |-> ( ( sin ` y ) / y ) ) o. ( n e. NN |-> ( _pi / n ) ) ) : NN --> RR |
46 |
19
|
mptru |
|- ( ( y e. ( RR \ { 0 } ) |-> ( ( sin ` y ) / y ) ) o. ( n e. NN |-> ( _pi / n ) ) ) = ( n e. NN |-> ( ( sin ` ( _pi / n ) ) / ( _pi / n ) ) ) |
47 |
46
|
feq1i |
|- ( ( ( y e. ( RR \ { 0 } ) |-> ( ( sin ` y ) / y ) ) o. ( n e. NN |-> ( _pi / n ) ) ) : NN --> RR <-> ( n e. NN |-> ( ( sin ` ( _pi / n ) ) / ( _pi / n ) ) ) : NN --> RR ) |
48 |
45 47
|
mpbi |
|- ( n e. NN |-> ( ( sin ` ( _pi / n ) ) / ( _pi / n ) ) ) : NN --> RR |
49 |
48
|
ffvelrni |
|- ( k e. NN -> ( ( n e. NN |-> ( ( sin ` ( _pi / n ) ) / ( _pi / n ) ) ) ` k ) e. RR ) |
50 |
49
|
adantl |
|- ( ( T. /\ k e. NN ) -> ( ( n e. NN |-> ( ( sin ` ( _pi / n ) ) / ( _pi / n ) ) ) ` k ) e. RR ) |
51 |
50
|
recnd |
|- ( ( T. /\ k e. NN ) -> ( ( n e. NN |-> ( ( sin ` ( _pi / n ) ) / ( _pi / n ) ) ) ` k ) e. CC ) |
52 |
29
|
recni |
|- 2 e. CC |
53 |
52
|
a1i |
|- ( ( T. /\ k e. NN ) -> 2 e. CC ) |
54 |
23
|
a1i |
|- ( ( T. /\ k e. NN ) -> _pi e. CC ) |
55 |
|
nncn |
|- ( k e. NN -> k e. CC ) |
56 |
55
|
adantl |
|- ( ( T. /\ k e. NN ) -> k e. CC ) |
57 |
|
nnne0 |
|- ( k e. NN -> k =/= 0 ) |
58 |
57
|
adantl |
|- ( ( T. /\ k e. NN ) -> k =/= 0 ) |
59 |
53 54 56 58
|
divassd |
|- ( ( T. /\ k e. NN ) -> ( ( 2 x. _pi ) / k ) = ( 2 x. ( _pi / k ) ) ) |
60 |
59
|
oveq1d |
|- ( ( T. /\ k e. NN ) -> ( ( ( 2 x. _pi ) / k ) / 2 ) = ( ( 2 x. ( _pi / k ) ) / 2 ) ) |
61 |
|
simpr |
|- ( ( T. /\ k e. NN ) -> k e. NN ) |
62 |
|
nndivre |
|- ( ( _pi e. RR /\ k e. NN ) -> ( _pi / k ) e. RR ) |
63 |
22 61 62
|
sylancr |
|- ( ( T. /\ k e. NN ) -> ( _pi / k ) e. RR ) |
64 |
63
|
recnd |
|- ( ( T. /\ k e. NN ) -> ( _pi / k ) e. CC ) |
65 |
|
2ne0 |
|- 2 =/= 0 |
66 |
65
|
a1i |
|- ( ( T. /\ k e. NN ) -> 2 =/= 0 ) |
67 |
64 53 66
|
divcan3d |
|- ( ( T. /\ k e. NN ) -> ( ( 2 x. ( _pi / k ) ) / 2 ) = ( _pi / k ) ) |
68 |
60 67
|
eqtrd |
|- ( ( T. /\ k e. NN ) -> ( ( ( 2 x. _pi ) / k ) / 2 ) = ( _pi / k ) ) |
69 |
68
|
fveq2d |
|- ( ( T. /\ k e. NN ) -> ( sin ` ( ( ( 2 x. _pi ) / k ) / 2 ) ) = ( sin ` ( _pi / k ) ) ) |
70 |
63
|
resincld |
|- ( ( T. /\ k e. NN ) -> ( sin ` ( _pi / k ) ) e. RR ) |
71 |
70
|
recnd |
|- ( ( T. /\ k e. NN ) -> ( sin ` ( _pi / k ) ) e. CC ) |
72 |
|
nnrp |
|- ( k e. NN -> k e. RR+ ) |
73 |
72
|
adantl |
|- ( ( T. /\ k e. NN ) -> k e. RR+ ) |
74 |
|
rpdivcl |
|- ( ( _pi e. RR+ /\ k e. RR+ ) -> ( _pi / k ) e. RR+ ) |
75 |
6 73 74
|
sylancr |
|- ( ( T. /\ k e. NN ) -> ( _pi / k ) e. RR+ ) |
76 |
75
|
rpne0d |
|- ( ( T. /\ k e. NN ) -> ( _pi / k ) =/= 0 ) |
77 |
71 64 76
|
divcan2d |
|- ( ( T. /\ k e. NN ) -> ( ( _pi / k ) x. ( ( sin ` ( _pi / k ) ) / ( _pi / k ) ) ) = ( sin ` ( _pi / k ) ) ) |
78 |
69 77
|
eqtr4d |
|- ( ( T. /\ k e. NN ) -> ( sin ` ( ( ( 2 x. _pi ) / k ) / 2 ) ) = ( ( _pi / k ) x. ( ( sin ` ( _pi / k ) ) / ( _pi / k ) ) ) ) |
79 |
78
|
oveq2d |
|- ( ( T. /\ k e. NN ) -> ( R x. ( sin ` ( ( ( 2 x. _pi ) / k ) / 2 ) ) ) = ( R x. ( ( _pi / k ) x. ( ( sin ` ( _pi / k ) ) / ( _pi / k ) ) ) ) ) |
80 |
3
|
recni |
|- R e. CC |
81 |
80
|
a1i |
|- ( ( T. /\ k e. NN ) -> R e. CC ) |
82 |
|
oveq2 |
|- ( n = k -> ( _pi / n ) = ( _pi / k ) ) |
83 |
82
|
fveq2d |
|- ( n = k -> ( sin ` ( _pi / n ) ) = ( sin ` ( _pi / k ) ) ) |
84 |
83 82
|
oveq12d |
|- ( n = k -> ( ( sin ` ( _pi / n ) ) / ( _pi / n ) ) = ( ( sin ` ( _pi / k ) ) / ( _pi / k ) ) ) |
85 |
|
eqid |
|- ( n e. NN |-> ( ( sin ` ( _pi / n ) ) / ( _pi / n ) ) ) = ( n e. NN |-> ( ( sin ` ( _pi / n ) ) / ( _pi / n ) ) ) |
86 |
|
ovex |
|- ( ( sin ` ( _pi / k ) ) / ( _pi / k ) ) e. _V |
87 |
84 85 86
|
fvmpt |
|- ( k e. NN -> ( ( n e. NN |-> ( ( sin ` ( _pi / n ) ) / ( _pi / n ) ) ) ` k ) = ( ( sin ` ( _pi / k ) ) / ( _pi / k ) ) ) |
88 |
87
|
adantl |
|- ( ( T. /\ k e. NN ) -> ( ( n e. NN |-> ( ( sin ` ( _pi / n ) ) / ( _pi / n ) ) ) ` k ) = ( ( sin ` ( _pi / k ) ) / ( _pi / k ) ) ) |
89 |
88 51
|
eqeltrrd |
|- ( ( T. /\ k e. NN ) -> ( ( sin ` ( _pi / k ) ) / ( _pi / k ) ) e. CC ) |
90 |
81 64 89
|
mulassd |
|- ( ( T. /\ k e. NN ) -> ( ( R x. ( _pi / k ) ) x. ( ( sin ` ( _pi / k ) ) / ( _pi / k ) ) ) = ( R x. ( ( _pi / k ) x. ( ( sin ` ( _pi / k ) ) / ( _pi / k ) ) ) ) ) |
91 |
79 90
|
eqtr4d |
|- ( ( T. /\ k e. NN ) -> ( R x. ( sin ` ( ( ( 2 x. _pi ) / k ) / 2 ) ) ) = ( ( R x. ( _pi / k ) ) x. ( ( sin ` ( _pi / k ) ) / ( _pi / k ) ) ) ) |
92 |
91
|
oveq2d |
|- ( ( T. /\ k e. NN ) -> ( ( 2 x. k ) x. ( R x. ( sin ` ( ( ( 2 x. _pi ) / k ) / 2 ) ) ) ) = ( ( 2 x. k ) x. ( ( R x. ( _pi / k ) ) x. ( ( sin ` ( _pi / k ) ) / ( _pi / k ) ) ) ) ) |
93 |
|
mulcl |
|- ( ( 2 e. CC /\ k e. CC ) -> ( 2 x. k ) e. CC ) |
94 |
52 56 93
|
sylancr |
|- ( ( T. /\ k e. NN ) -> ( 2 x. k ) e. CC ) |
95 |
|
mulcl |
|- ( ( R e. CC /\ ( _pi / k ) e. CC ) -> ( R x. ( _pi / k ) ) e. CC ) |
96 |
80 64 95
|
sylancr |
|- ( ( T. /\ k e. NN ) -> ( R x. ( _pi / k ) ) e. CC ) |
97 |
94 96 89
|
mulassd |
|- ( ( T. /\ k e. NN ) -> ( ( ( 2 x. k ) x. ( R x. ( _pi / k ) ) ) x. ( ( sin ` ( _pi / k ) ) / ( _pi / k ) ) ) = ( ( 2 x. k ) x. ( ( R x. ( _pi / k ) ) x. ( ( sin ` ( _pi / k ) ) / ( _pi / k ) ) ) ) ) |
98 |
53 56 81 64
|
mul4d |
|- ( ( T. /\ k e. NN ) -> ( ( 2 x. k ) x. ( R x. ( _pi / k ) ) ) = ( ( 2 x. R ) x. ( k x. ( _pi / k ) ) ) ) |
99 |
54 56 58
|
divcan2d |
|- ( ( T. /\ k e. NN ) -> ( k x. ( _pi / k ) ) = _pi ) |
100 |
99
|
oveq2d |
|- ( ( T. /\ k e. NN ) -> ( ( 2 x. R ) x. ( k x. ( _pi / k ) ) ) = ( ( 2 x. R ) x. _pi ) ) |
101 |
53 81 54
|
mul32d |
|- ( ( T. /\ k e. NN ) -> ( ( 2 x. R ) x. _pi ) = ( ( 2 x. _pi ) x. R ) ) |
102 |
100 101
|
eqtrd |
|- ( ( T. /\ k e. NN ) -> ( ( 2 x. R ) x. ( k x. ( _pi / k ) ) ) = ( ( 2 x. _pi ) x. R ) ) |
103 |
98 102
|
eqtrd |
|- ( ( T. /\ k e. NN ) -> ( ( 2 x. k ) x. ( R x. ( _pi / k ) ) ) = ( ( 2 x. _pi ) x. R ) ) |
104 |
103
|
oveq1d |
|- ( ( T. /\ k e. NN ) -> ( ( ( 2 x. k ) x. ( R x. ( _pi / k ) ) ) x. ( ( sin ` ( _pi / k ) ) / ( _pi / k ) ) ) = ( ( ( 2 x. _pi ) x. R ) x. ( ( sin ` ( _pi / k ) ) / ( _pi / k ) ) ) ) |
105 |
92 97 104
|
3eqtr2d |
|- ( ( T. /\ k e. NN ) -> ( ( 2 x. k ) x. ( R x. ( sin ` ( ( ( 2 x. _pi ) / k ) / 2 ) ) ) ) = ( ( ( 2 x. _pi ) x. R ) x. ( ( sin ` ( _pi / k ) ) / ( _pi / k ) ) ) ) |
106 |
|
oveq2 |
|- ( n = k -> ( 2 x. n ) = ( 2 x. k ) ) |
107 |
|
oveq2 |
|- ( n = k -> ( ( 2 x. _pi ) / n ) = ( ( 2 x. _pi ) / k ) ) |
108 |
1 107
|
syl5eq |
|- ( n = k -> A = ( ( 2 x. _pi ) / k ) ) |
109 |
108
|
oveq1d |
|- ( n = k -> ( A / 2 ) = ( ( ( 2 x. _pi ) / k ) / 2 ) ) |
110 |
109
|
fveq2d |
|- ( n = k -> ( sin ` ( A / 2 ) ) = ( sin ` ( ( ( 2 x. _pi ) / k ) / 2 ) ) ) |
111 |
110
|
oveq2d |
|- ( n = k -> ( R x. ( sin ` ( A / 2 ) ) ) = ( R x. ( sin ` ( ( ( 2 x. _pi ) / k ) / 2 ) ) ) ) |
112 |
106 111
|
oveq12d |
|- ( n = k -> ( ( 2 x. n ) x. ( R x. ( sin ` ( A / 2 ) ) ) ) = ( ( 2 x. k ) x. ( R x. ( sin ` ( ( ( 2 x. _pi ) / k ) / 2 ) ) ) ) ) |
113 |
|
ovex |
|- ( ( 2 x. k ) x. ( R x. ( sin ` ( ( ( 2 x. _pi ) / k ) / 2 ) ) ) ) e. _V |
114 |
112 2 113
|
fvmpt |
|- ( k e. NN -> ( P ` k ) = ( ( 2 x. k ) x. ( R x. ( sin ` ( ( ( 2 x. _pi ) / k ) / 2 ) ) ) ) ) |
115 |
114
|
adantl |
|- ( ( T. /\ k e. NN ) -> ( P ` k ) = ( ( 2 x. k ) x. ( R x. ( sin ` ( ( ( 2 x. _pi ) / k ) / 2 ) ) ) ) ) |
116 |
88
|
oveq2d |
|- ( ( T. /\ k e. NN ) -> ( ( ( 2 x. _pi ) x. R ) x. ( ( n e. NN |-> ( ( sin ` ( _pi / n ) ) / ( _pi / n ) ) ) ` k ) ) = ( ( ( 2 x. _pi ) x. R ) x. ( ( sin ` ( _pi / k ) ) / ( _pi / k ) ) ) ) |
117 |
105 115 116
|
3eqtr4d |
|- ( ( T. /\ k e. NN ) -> ( P ` k ) = ( ( ( 2 x. _pi ) x. R ) x. ( ( n e. NN |-> ( ( sin ` ( _pi / n ) ) / ( _pi / n ) ) ) ` k ) ) ) |
118 |
4 5 28 33 37 51 117
|
climmulc2 |
|- ( T. -> P ~~> ( ( ( 2 x. _pi ) x. R ) x. 1 ) ) |
119 |
118
|
mptru |
|- P ~~> ( ( ( 2 x. _pi ) x. R ) x. 1 ) |
120 |
32
|
mulid1i |
|- ( ( ( 2 x. _pi ) x. R ) x. 1 ) = ( ( 2 x. _pi ) x. R ) |
121 |
119 120
|
breqtri |
|- P ~~> ( ( 2 x. _pi ) x. R ) |