Metamath Proof Explorer

Theorem goldrapos

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

Ref Expression
Hypothesis goldra.val 
|- F = ( 2 x. ( cos ` ( _pi / 5 ) ) )
Assertion goldrapos 
|- 0 < F

Proof

Step Hyp Ref Expression
1 goldra.val 
 |-  F = ( 2 x. ( cos ` ( _pi / 5 ) ) )
2 2re 
 |-  2 e. RR
3 pire 
 |-  _pi e. RR
4 5re 
 |-  5 e. RR
5 5pos 
 |-  0 < 5
6 4 5 gt0ne0ii 
 |-  5 =/= 0
7 3 4 6 redivcli 
 |-  ( _pi / 5 ) e. RR
8 recoscl 
 |-  ( ( _pi / 5 ) e. RR -> ( cos ` ( _pi / 5 ) ) e. RR )
9 7 8 ax-mp 
 |-  ( cos ` ( _pi / 5 ) ) e. RR
10 2pos 
 |-  0 < 2
11 pipos 
 |-  0 < _pi
12 3 2 11 10 divgt0ii 
 |-  0 < ( _pi / 2 )
13 halfpire 
 |-  ( _pi / 2 ) e. RR
14 lt0neg2 
 |-  ( ( _pi / 2 ) e. RR -> ( 0 < ( _pi / 2 ) <-> -u ( _pi / 2 ) < 0 ) )
15 13 14 ax-mp 
 |-  ( 0 < ( _pi / 2 ) <-> -u ( _pi / 2 ) < 0 )
16 12 15 mpbi 
 |-  -u ( _pi / 2 ) < 0
17 3 4 11 5 divgt0ii 
 |-  0 < ( _pi / 5 )
18 neghalfpire 
 |-  -u ( _pi / 2 ) e. RR
19 0re 
 |-  0 e. RR
20 18 19 7 lttri 
 |-  ( ( -u ( _pi / 2 ) < 0 /\ 0 < ( _pi / 5 ) ) -> -u ( _pi / 2 ) < ( _pi / 5 ) )
21 16 17 20 mp2an 
 |-  -u ( _pi / 2 ) < ( _pi / 5 )
22 2lt5 
 |-  2 < 5
23 2rp 
 |-  2 e. RR+
24 23 a1i 
 |-  ( T. -> 2 e. RR+ )
25 5rp 
 |-  5 e. RR+
26 25 a1i 
 |-  ( T. -> 5 e. RR+ )
27 pirp 
 |-  _pi e. RR+
28 27 a1i 
 |-  ( T. -> _pi e. RR+ )
29 24 26 28 ltdiv2d 
 |-  ( T. -> ( 2 < 5 <-> ( _pi / 5 ) < ( _pi / 2 ) ) )
30 29 mptru 
 |-  ( 2 < 5 <-> ( _pi / 5 ) < ( _pi / 2 ) )
31 22 30 mpbi 
 |-  ( _pi / 5 ) < ( _pi / 2 )
32 neghalfpirx 
 |-  -u ( _pi / 2 ) e. RR*
33 13 rexri 
 |-  ( _pi / 2 ) e. RR*
34 elioo2 
 |-  ( ( -u ( _pi / 2 ) e. RR* /\ ( _pi / 2 ) e. RR* ) -> ( ( _pi / 5 ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) <-> ( ( _pi / 5 ) e. RR /\ -u ( _pi / 2 ) < ( _pi / 5 ) /\ ( _pi / 5 ) < ( _pi / 2 ) ) ) )
35 32 33 34 mp2an 
 |-  ( ( _pi / 5 ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) <-> ( ( _pi / 5 ) e. RR /\ -u ( _pi / 2 ) < ( _pi / 5 ) /\ ( _pi / 5 ) < ( _pi / 2 ) ) )
36 7 21 31 35 mpbir3an 
 |-  ( _pi / 5 ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) )
37 cosq14gt0 
 |-  ( ( _pi / 5 ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) -> 0 < ( cos ` ( _pi / 5 ) ) )
38 36 37 ax-mp 
 |-  0 < ( cos ` ( _pi / 5 ) )
39 2 9 10 38 mulgt0ii 
 |-  0 < ( 2 x. ( cos ` ( _pi / 5 ) ) )
40 39 1 breqtrri 
 |-  0 < F