Metamath Proof Explorer

Theorem pidiv2halves

Description: Adding _pi / 2 to itself gives _pi . See 2halves . (Contributed by David A. Wheeler, 8-Dec-2018)

Ref Expression
Assertion pidiv2halves 
|- ( ( _pi / 2 ) + ( _pi / 2 ) ) = _pi

Proof

Step Hyp Ref Expression
1 picn 
 |-  _pi e. CC
2 2halves 
 |-  ( _pi e. CC -> ( ( _pi / 2 ) + ( _pi / 2 ) ) = _pi )
3 1 2 ax-mp 
 |-  ( ( _pi / 2 ) + ( _pi / 2 ) ) = _pi