Theorem pidiv2halves

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

	Ref	Expression
Assertion	pidiv2halves	⊢ ( ( π / 2 ) + ( π / 2 ) ) = π

Proof

Step	Hyp	Ref	Expression
1		picn	⊢ π ∈ ℂ
2		2halves	⊢ ( π ∈ ℂ → ( ( π / 2 ) + ( π / 2 ) ) = π )
3	1 2	ax-mp	⊢ ( ( π / 2 ) + ( π / 2 ) ) = π