Metamath Proof Explorer

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 ( ( 𝐴 ∈ ℝ+ ∧ ( cos ‘ 𝐴 ) = 1 ) → ( 2 · π ) ≤ 𝐴 )

Proof

Step Hyp Ref Expression
1 2rp ⊢ 2 ∈ ℝ+
2 pirp ⊢ π ∈ ℝ+
3 rpmulcl ⊢ ( ( 2 ∈ ℝ+ ∧ π ∈ ℝ+ ) → ( 2 · π ) ∈ ℝ+ )
4 1 2 3 mp2an ⊢ ( 2 · π ) ∈ ℝ+
5 rpre ⊢ ( ( 2 · π ) ∈ ℝ+ → ( 2 · π ) ∈ ℝ )
6 4 5 ax-mp ⊢ ( 2 · π ) ∈ ℝ
7 6 recni ⊢ ( 2 · π ) ∈ ℂ
8 rpgt0 ⊢ ( ( 2 · π ) ∈ ℝ+ → 0 < ( 2 · π ) )
9 4 8 ax-mp ⊢ 0 < ( 2 · π )
10 6 9 gt0ne0ii ⊢ ( 2 · π ) ≠ 0
11 7 10 dividi ⊢ ( ( 2 · π ) / ( 2 · π ) ) = 1
12 rpdivcl ⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( 2 · π ) ∈ ℝ+ ) → ( 𝐴 / ( 2 · π ) ) ∈ ℝ+ )
13 12 rpgt0d ⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( 2 · π ) ∈ ℝ+ ) → 0 < ( 𝐴 / ( 2 · π ) ) )
14 4 13 mpan2 ⊢ ( 𝐴 ∈ ℝ+ → 0 < ( 𝐴 / ( 2 · π ) ) )
15 14 adantr ⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( cos ‘ 𝐴 ) = 1 ) → 0 < ( 𝐴 / ( 2 · π ) ) )
16 rpcn ⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℂ )
17 coseq1 ⊢ ( 𝐴 ∈ ℂ → ( ( cos ‘ 𝐴 ) = 1 ↔ ( 𝐴 / ( 2 · π ) ) ∈ ℤ ) )
18 16 17 syl ⊢ ( 𝐴 ∈ ℝ+ → ( ( cos ‘ 𝐴 ) = 1 ↔ ( 𝐴 / ( 2 · π ) ) ∈ ℤ ) )
19 18 biimpa ⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( cos ‘ 𝐴 ) = 1 ) → ( 𝐴 / ( 2 · π ) ) ∈ ℤ )
20 zgt0ge1 ⊢ ( ( 𝐴 / ( 2 · π ) ) ∈ ℤ → ( 0 < ( 𝐴 / ( 2 · π ) ) ↔ 1 ≤ ( 𝐴 / ( 2 · π ) ) ) )
21 19 20 syl ⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( cos ‘ 𝐴 ) = 1 ) → ( 0 < ( 𝐴 / ( 2 · π ) ) ↔ 1 ≤ ( 𝐴 / ( 2 · π ) ) ) )
22 15 21 mpbid ⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( cos ‘ 𝐴 ) = 1 ) → 1 ≤ ( 𝐴 / ( 2 · π ) ) )
23 11 22 eqbrtrid ⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( cos ‘ 𝐴 ) = 1 ) → ( ( 2 · π ) / ( 2 · π ) ) ≤ ( 𝐴 / ( 2 · π ) ) )
24 rpre ⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ )
25 24 adantr ⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( cos ‘ 𝐴 ) = 1 ) → 𝐴 ∈ ℝ )
26 6 9 pm3.2i ⊢ ( ( 2 · π ) ∈ ℝ ∧ 0 < ( 2 · π ) )
27 lediv1 ⊢ ( ( ( 2 · π ) ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ ( ( 2 · π ) ∈ ℝ ∧ 0 < ( 2 · π ) ) ) → ( ( 2 · π ) ≤ 𝐴 ↔ ( ( 2 · π ) / ( 2 · π ) ) ≤ ( 𝐴 / ( 2 · π ) ) ) )
28 6 26 27 mp3an13 ⊢ ( 𝐴 ∈ ℝ → ( ( 2 · π ) ≤ 𝐴 ↔ ( ( 2 · π ) / ( 2 · π ) ) ≤ ( 𝐴 / ( 2 · π ) ) ) )
29 25 28 syl ⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( cos ‘ 𝐴 ) = 1 ) → ( ( 2 · π ) ≤ 𝐴 ↔ ( ( 2 · π ) / ( 2 · π ) ) ≤ ( 𝐴 / ( 2 · π ) ) ) )
30 23 29 mpbird ⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( cos ‘ 𝐴 ) = 1 ) → ( 2 · π ) ≤ 𝐴 )