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 ) |