metamath/valid/mathd-numbertheory-232.mm

$(
  @{
    mathd-numbertheory-232.0 @e |- ( ph -> A e. NN0 ) $@
    mathd-numbertheory-232.1 @e |- ( ph -> B e. NN0 ) $@
    mathd-numbertheory-232.2 @e |- ( ph -> C e. NN0 ) $@
    mathd-numbertheory-232.3 @e |- Y = ( Z/nZ ` ; 3 1 ) $@
    mathd-numbertheory-232.4 @e |- I = ( invr ` Y ) $@
    mathd-numbertheory-232.5 @e |- R = ( ZZring ~QG ( ( RSpan ` ZZring ) ` { ; 3 1 } ) ) $@
    mathd-numbertheory-232.6 @e |- ( ph -> ( I ` [ 3 ] R ) = [ A ] R ) $@
    mathd-numbertheory-232.7 @e |- ( ph -> ( I ` [ 6 ] R ) = [ B ] R ) $@
    mathd-numbertheory-232.8 @e |- ( ph -> ( I ` [ ( A + B ) ] R ) = [ C ] R ) $@
    @( (Contributed by Kunhao Zheng, 14-Jun-2021.) @)
    mathd-numbertheory-232 @p |- ( ph -> [ C ] R = [ ; 2 9 ] R ) @=
      ? @.
  @}
$)