Theorem taupilem1

Description: Lemma for taupi . A positive real whose cosine is one is at least 2 x. _pi . (Contributed by Jim Kingdon, 19-Feb-2019)

	Ref	Expression
Assertion	taupilem1	$$⊢\left(A\in {ℝ}^{+}\wedge \cos A=1\right)\to 2\mathrm{\pi }\le A$$

Proof

Step	Hyp	Ref	Expression
1		2rp	$$⊢2\in {ℝ}^{+}$$
2		pirp	$$⊢\mathrm{\pi }\in {ℝ}^{+}$$
3		rpmulcl	$$⊢\left(2\in {ℝ}^{+}\wedge \mathrm{\pi }\in {ℝ}^{+}\right)\to 2\mathrm{\pi }\in {ℝ}^{+}$$
4	1 2 3	mp2an	$$⊢2\mathrm{\pi }\in {ℝ}^{+}$$
5		rpre	$$⊢2\mathrm{\pi }\in {ℝ}^{+}\to 2\mathrm{\pi }\in ℝ$$
6	4 5	ax-mp	$$⊢2\mathrm{\pi }\in ℝ$$
7	6	recni	$$⊢2\mathrm{\pi }\in ℂ$$
8		rpgt0	$$⊢2\mathrm{\pi }\in {ℝ}^{+}\to 0<2\mathrm{\pi }$$
9	4 8	ax-mp	$$⊢0<2\mathrm{\pi }$$
10	6 9	gt0ne0ii	$$⊢2\mathrm{\pi }\ne 0$$
11	7 10	dividi	$$⊢\frac{2\mathrm{\pi }}{2\mathrm{\pi }}=1$$
12		rpdivcl	$$⊢\left(A\in {ℝ}^{+}\wedge 2\mathrm{\pi }\in {ℝ}^{+}\right)\to \frac{A}{2\mathrm{\pi }}\in {ℝ}^{+}$$
13	12	rpgt0d	$$⊢\left(A\in {ℝ}^{+}\wedge 2\mathrm{\pi }\in {ℝ}^{+}\right)\to 0<\frac{A}{2\mathrm{\pi }}$$
14	4 13	mpan2	$$⊢A\in {ℝ}^{+}\to 0<\frac{A}{2\mathrm{\pi }}$$
15	14	adantr	$$⊢\left(A\in {ℝ}^{+}\wedge \cos A=1\right)\to 0<\frac{A}{2\mathrm{\pi }}$$
16		rpcn	$$⊢A\in {ℝ}^{+}\to A\in ℂ$$
17		coseq1	$$⊢A\in ℂ\to \left(\cos A=1\leftrightarrow \frac{A}{2\mathrm{\pi }}\in \mathbb{Z}\right)$$
18	16 17	syl	$$⊢A\in {ℝ}^{+}\to \left(\cos A=1\leftrightarrow \frac{A}{2\mathrm{\pi }}\in \mathbb{Z}\right)$$
19	18	biimpa	$$⊢\left(A\in {ℝ}^{+}\wedge \cos A=1\right)\to \frac{A}{2\mathrm{\pi }}\in \mathbb{Z}$$
20		zgt0ge1	$$⊢\frac{A}{2\mathrm{\pi }}\in \mathbb{Z}\to \left(0<\frac{A}{2\mathrm{\pi }}\leftrightarrow 1\le \frac{A}{2\mathrm{\pi }}\right)$$
21	19 20	syl	$$⊢\left(A\in {ℝ}^{+}\wedge \cos A=1\right)\to \left(0<\frac{A}{2\mathrm{\pi }}\leftrightarrow 1\le \frac{A}{2\mathrm{\pi }}\right)$$
22	15 21	mpbid	$$⊢\left(A\in {ℝ}^{+}\wedge \cos A=1\right)\to 1\le \frac{A}{2\mathrm{\pi }}$$
23	11 22	eqbrtrid	$$⊢\left(A\in {ℝ}^{+}\wedge \cos A=1\right)\to \frac{2\mathrm{\pi }}{2\mathrm{\pi }}\le \frac{A}{2\mathrm{\pi }}$$
24		rpre	$$⊢A\in {ℝ}^{+}\to A\in ℝ$$
25	24	adantr	$$⊢\left(A\in {ℝ}^{+}\wedge \cos A=1\right)\to A\in ℝ$$
26	6 9	pm3.2i	$$⊢\left(2\mathrm{\pi }\in ℝ\wedge 0<2\mathrm{\pi }\right)$$
27		lediv1	$$⊢\left(2\mathrm{\pi }\in ℝ\wedge A\in ℝ\wedge \left(2\mathrm{\pi }\in ℝ\wedge 0<2\mathrm{\pi }\right)\right)\to \left(2\mathrm{\pi }\le A\leftrightarrow \frac{2\mathrm{\pi }}{2\mathrm{\pi }}\le \frac{A}{2\mathrm{\pi }}\right)$$
28	6 26 27	mp3an13	$$⊢A\in ℝ\to \left(2\mathrm{\pi }\le A\leftrightarrow \frac{2\mathrm{\pi }}{2\mathrm{\pi }}\le \frac{A}{2\mathrm{\pi }}\right)$$
29	25 28	syl	$$⊢\left(A\in {ℝ}^{+}\wedge \cos A=1\right)\to \left(2\mathrm{\pi }\le A\leftrightarrow \frac{2\mathrm{\pi }}{2\mathrm{\pi }}\le \frac{A}{2\mathrm{\pi }}\right)$$
30	23 29	mpbird	$$⊢\left(A\in {ℝ}^{+}\wedge \cos A=1\right)\to 2\mathrm{\pi }\le A$$