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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2cnd | |
|
2 | rpcn | |
|
3 | rpne0 | |
|
4 | 1 2 3 | divcan4d | |
5 | 2z | |
|
6 | 4 5 | eqeltrdi | |
7 | 2re | |
|
8 | 7 | a1i | |
9 | rpre | |
|
10 | 8 9 | remulcld | |
11 | mod0 | |
|
12 | 10 11 | mpancom | |
13 | 6 12 | mpbird | |