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 = \frac{2 π}{n}$
	circum.2	$⊢ P = (n \in ℕ ⟼ 2 n R \sin (\frac{A}{2}))$
	circum.3	$⊢ R \in ℝ$
Assertion	circum	$⊢ P ⇝ 2 π R$

Proof

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

Metamath Proof Explorer

Theorem circum

Proof