Metamath Proof Explorer

Theorem circum

Description: The circumference of a circle of radius R , defined as the limit as n ~> +oo of the perimeter of an inscribed n-sided isogons, is ( ( 2 x. _pi ) x. R ) . (Contributed by Paul Chapman, 10-Nov-2012) (Proof shortened by Mario Carneiro, 21-May-2014)

Ref Expression
Hypotheses circum.1 
|- A = ( ( 2 x. _pi ) / n )
circum.2 
|- P = ( n e. NN |-> ( ( 2 x. n ) x. ( R x. ( sin ` ( A / 2 ) ) ) ) )
circum.3 
|- R e. RR
Assertion circum 
|- P ~~> ( ( 2 x. _pi ) x. R )

Proof

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 ffvelcdmi 
 |-  ( 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 eqtrid 
 |-  ( 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 mulridi 
 |-  ( ( ( 2 x. _pi ) x. R ) x. 1 ) = ( ( 2 x. _pi ) x. R )
121 119 120 breqtri 
 |-  P ~~> ( ( 2 x. _pi ) x. R )