Metamath Proof Explorer

Theorem goldrapos

Description: Golden ratio is positive. (Contributed by Ender Ting, 16-Apr-2026)

Ref Expression
Hypothesis goldra.val ⊢ F = 2 ⁢ cos ⁡ π 5
Assertion goldrapos ⊢ 0 < F

Proof

Step Hyp Ref Expression
1 goldra.val ⊢ F = 2 ⁢ cos ⁡ π 5
2 2re ⊢ 2 ∈ ℝ
3 pire ⊢ π ∈ ℝ
4 5re ⊢ 5 ∈ ℝ
5 5pos ⊢ 0 < 5
6 4 5 gt0ne0ii ⊢ 5 ≠ 0
7 3 4 6 redivcli ⊢ π 5 ∈ ℝ
8 recoscl ⊢ π 5 ∈ ℝ → cos ⁡ π 5 ∈ ℝ
9 7 8 ax-mp ⊢ cos ⁡ π 5 ∈ ℝ
10 2pos ⊢ 0 < 2
11 pipos ⊢ 0 < π
12 3 2 11 10 divgt0ii ⊢ 0 < π 2
13 halfpire ⊢ π 2 ∈ ℝ
14 lt0neg2 ⊢ π 2 ∈ ℝ → 0 < π 2 ↔ − π 2 < 0
15 13 14 ax-mp ⊢ 0 < π 2 ↔ − π 2 < 0
16 12 15 mpbi ⊢ − π 2 < 0
17 3 4 11 5 divgt0ii ⊢ 0 < π 5
18 neghalfpire ⊢ − π 2 ∈ ℝ
19 0re ⊢ 0 ∈ ℝ
20 18 19 7 lttri ⊢ − π 2 < 0 ∧ 0 < π 5 → − π 2 < π 5
21 16 17 20 mp2an ⊢ − π 2 < π 5
22 2lt5 ⊢ 2 < 5
23 2rp ⊢ 2 ∈ ℝ +
24 23 a1i ⊢ ⊤ → 2 ∈ ℝ +
25 5rp ⊢ 5 ∈ ℝ +
26 25 a1i ⊢ ⊤ → 5 ∈ ℝ +
27 pirp ⊢ π ∈ ℝ +
28 27 a1i ⊢ ⊤ → π ∈ ℝ +
29 24 26 28 ltdiv2d ⊢ ⊤ → 2 < 5 ↔ π 5 < π 2
30 29 mptru ⊢ 2 < 5 ↔ π 5 < π 2
31 22 30 mpbi ⊢ π 5 < π 2
32 neghalfpirx ⊢ − π 2 ∈ ℝ *
33 13 rexri ⊢ π 2 ∈ ℝ *
34 elioo2 ⊢ − π 2 ∈ ℝ * ∧ π 2 ∈ ℝ * → π 5 ∈ − π 2 π 2 ↔ π 5 ∈ ℝ ∧ − π 2 < π 5 ∧ π 5 < π 2
35 32 33 34 mp2an ⊢ π 5 ∈ − π 2 π 2 ↔ π 5 ∈ ℝ ∧ − π 2 < π 5 ∧ π 5 < π 2
36 7 21 31 35 mpbir3an ⊢ π 5 ∈ − π 2 π 2
37 cosq14gt0 ⊢ π 5 ∈ − π 2 π 2 → 0 < cos ⁡ π 5
38 36 37 ax-mp ⊢ 0 < cos ⁡ π 5
39 2 9 10 38 mulgt0ii ⊢ 0 < 2 ⁢ cos ⁡ π 5
40 39 1 breqtrri ⊢ 0 < F