Metamath Proof Explorer


Theorem modid0

Description: A positive real number modulo itself is 0. (Contributed by Alexander van der Vekens, 15-May-2018)

Ref Expression
Assertion modid0 N+NmodN=0

Proof

Step Hyp Ref Expression
1 rpcn N+N
2 rpne0 N+N0
3 1 2 dividd N+NN=1
4 1z 1
5 3 4 eqeltrdi N+NN
6 rpre N+N
7 mod0 NN+NmodN=0NN
8 6 7 mpancom N+NmodN=0NN
9 5 8 mpbird N+NmodN=0