Metamath Proof Explorer


Theorem znmulOLD

Description: Obsolete version of znadd as of 3-Nov-2024. The multiplicative structure of Z/nZ is the same as the quotient ring it is based on. (Contributed by Mario Carneiro, 15-Jun-2015) (Revised by AV, 13-Jun-2019) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses znval2.s S=RSpanring
znval2.u U=ring/𝑠ring~QGSN
znval2.y Y=/N
Assertion znmulOLD N0U=Y

Proof

Step Hyp Ref Expression
1 znval2.s S=RSpanring
2 znval2.u U=ring/𝑠ring~QGSN
3 znval2.y Y=/N
4 df-mulr 𝑟=Slot3
5 3nn 3
6 3lt10 3<10
7 1 2 3 4 5 6 znbaslemOLD N0U=Y