metamath/valid/aime-1983-p9.mm

$(
  @{
    aime-1983-p9.0 @e |- ( ph -> X e. RR ) $@
    aime-1983-p9.1 @e |- ( ph -> ( 0 < X /\ X < _pi ) ) $@
    @( (Contributed by Kunhao Zheng, 4-May-2021.) @)
    aime-1983-p9 @p |- ( ph -> ; 1 2 <_ ( ( ( 9 x. ( ( X ^ 2 ) x. ( ( sin ` X ) ^ 2 ) ) ) + 4 ) / ( X x. ( sin ` X ) ) ) ) @=
      ? @.
  @}
$)