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 )