metamath/valid/mathd-numbertheory-42.mm

$(
  @{
    mathd-numbertheory-42.0 @e |- ( ph -> U e. NN ) $@
    mathd-numbertheory-42.1 @e |- ( ph -> V e. NN ) $@
    mathd-numbertheory-42.2 @e |- ( ph -> ; 4 0 || ( ( ; 2 7 x. U ) - ; 1 7 ) ) $@
    mathd-numbertheory-42.3 @e |- ( ph -> ; 4 0 || ( ( ; 2 7 x. V ) - ; 1 7 ) ) $@
    mathd-numbertheory-42.4 @e |- ( ph -> U < ; 4 0 ) $@
    mathd-numbertheory-42.5 @e |- ( ph -> V < ; 8 0 ) $@
    mathd-numbertheory-42.6 @e |- ( ph -> ; 4 0 < V ) $@
    @( (Contributed by Kunhao Zheng, 4-May-2021.) @)
    mathd-numbertheory-42 @p |- ( ph -> ( U + V ) = ; 6 2 ) @=
      ? @.
  @}
$)