Metamath Proof Explorer


Theorem 2txmodxeq0

Description: Two times a positive real number modulo the real number is zero. (Contributed by Alexander van der Vekens, 8-Jun-2018)

Ref Expression
Assertion 2txmodxeq0 X+2XmodX=0

Proof

Step Hyp Ref Expression
1 2cnd X+2
2 rpcn X+X
3 rpne0 X+X0
4 1 2 3 divcan4d X+2XX=2
5 2z 2
6 4 5 eqeltrdi X+2XX
7 2re 2
8 7 a1i X+2
9 rpre X+X
10 8 9 remulcld X+2X
11 mod0 2XX+2XmodX=02XX
12 10 11 mpancom X+2XmodX=02XX
13 6 12 mpbird X+2XmodX=0