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 e. RR+ -> ( ( 2 x. X ) mod X ) = 0 )

Proof

Step Hyp Ref Expression
1 2cnd
 |-  ( X e. RR+ -> 2 e. CC )
2 rpcn
 |-  ( X e. RR+ -> X e. CC )
3 rpne0
 |-  ( X e. RR+ -> X =/= 0 )
4 1 2 3 divcan4d
 |-  ( X e. RR+ -> ( ( 2 x. X ) / X ) = 2 )
5 2z
 |-  2 e. ZZ
6 4 5 eqeltrdi
 |-  ( X e. RR+ -> ( ( 2 x. X ) / X ) e. ZZ )
7 2re
 |-  2 e. RR
8 7 a1i
 |-  ( X e. RR+ -> 2 e. RR )
9 rpre
 |-  ( X e. RR+ -> X e. RR )
10 8 9 remulcld
 |-  ( X e. RR+ -> ( 2 x. X ) e. RR )
11 mod0
 |-  ( ( ( 2 x. X ) e. RR /\ X e. RR+ ) -> ( ( ( 2 x. X ) mod X ) = 0 <-> ( ( 2 x. X ) / X ) e. ZZ ) )
12 10 11 mpancom
 |-  ( X e. RR+ -> ( ( ( 2 x. X ) mod X ) = 0 <-> ( ( 2 x. X ) / X ) e. ZZ ) )
13 6 12 mpbird
 |-  ( X e. RR+ -> ( ( 2 x. X ) mod X ) = 0 )