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 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 )