metamath/valid/mathd-numbertheory-13.mm

$(
  @{
    mathd-numbertheory-13.0 @e |- ( ph -> U e. NN ) $@
    mathd-numbertheory-13.1 @e |- ( ph -> V e. NN ) $@
    mathd-numbertheory-13.2 @e |- ( ph -> ; ; 1 0 0 || ( ( ; 1 4 x. U ) - ; 4 6 ) ) $@
    mathd-numbertheory-13.3 @e |- ( ph -> ; ; 1 0 0 || ( ( ; 1 4 x. V ) - ; 4 6 ) ) $@
    mathd-numbertheory-13.4 @e |- ( ph -> U < ; 5 0 ) $@
    mathd-numbertheory-13.5 @e |- ( ph -> V < ; ; 1 0 0 ) $@
    mathd-numbertheory-13.6 @e |- ( ph -> ; 5 0 < V ) $@
    @( (Contributed by Kunhao Zheng, 4-May-2021.) @)
    mathd-numbertheory-13 @p |- ( ph -> ( ( U + V ) / 2 ) = ; 6 4 ) @=
      ? @.
  @}
$)