Description: The golden ratio is a positive real. (Contributed by Ender Ting, 16-Apr-2026)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | goldra.val | |- F = ( 2 x. ( cos ` ( _pi / 5 ) ) ) |
|
| Assertion | goldrarp | |- F e. RR+ |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | goldra.val | |- F = ( 2 x. ( cos ` ( _pi / 5 ) ) ) |
|
| 2 | 1 | goldrarr | |- F e. RR |
| 3 | 1 | goldrapos | |- 0 < F |
| 4 | 2 3 | elrpii | |- F e. RR+ |