Description: -u _pi is a real number. (Contributed by David A. Wheeler, 8-Dec-2018)
|- -u _pi e. CC
|- _pi e. CC