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 ⊢ 𝐴 = ( ( 2 · π ) / 𝑛 )
circum.2 ⊢ 𝑃 = ( 𝑛 ∈ ℕ ↦ ( ( 2 · 𝑛 ) · ( 𝑅 · ( sin ‘ ( 𝐴 / 2 ) ) ) ) )
circum.3 ⊢ 𝑅 ∈ ℝ
Assertion circum 𝑃 ⇝ ( ( 2 · π ) · 𝑅 )

Proof

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