Metamath Proof Explorer

Theorem 2pire

Description: ( 2 x. _pi ) is a real number. (Contributed by Umit Teoman Dogan, 10-Jun-2026)

Ref Expression
Assertion 2pire 
|- ( 2 x. _pi ) e. RR

Proof

Step Hyp Ref Expression
1 2re 
 |-  2 e. RR
2 pire 
 |-  _pi e. RR
3 1 2 remulcli 
 |-  ( 2 x. _pi ) e. RR