Description: The golden ratio is a real value. (Contributed by Ender Ting, 15-Mar-2026)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | goldra.val | |- F = ( 2 x. ( cos ` ( _pi / 5 ) ) ) |
|
| Assertion | goldrarr | |- F e. RR |
| 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 | 2 9 | remulcli | |- ( 2 x. ( cos ` ( _pi / 5 ) ) ) e. RR |
| 11 | 1 10 | eqeltri | |- F e. RR |