metamath/valid/algebra-sqineq-2unitcircatblt1.mm

$(
  @{
    algebra-sqineq-2unitcircatblt1.0 @e |- ( ph -> A e. RR ) $@
    algebra-sqineq-2unitcircatblt1.1 @e |- ( ph -> B e. RR ) $@
    algebra-sqineq-2unitcircatblt1.2 @e |- ( ph -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = 2 ) $@
    @( (Contributed by Kunhao Zheng, 4-May-2021.) @)
    algebra-sqineq-2unitcircatblt1 @p |- ( ph -> ( A x. B ) <_ 1 ) @=
      ? @.
  @}
$)