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\in {ℝ}^{+}\to 2X\mathrm{mod}X=0$$

Proof

Step	Hyp	Ref	Expression
1		2cnd	$$⊢X\in {ℝ}^{+}\to 2\in ℂ$$
2		rpcn	$$⊢X\in {ℝ}^{+}\to X\in ℂ$$
3		rpne0	$$⊢X\in {ℝ}^{+}\to X\ne 0$$
4	1 2 3	divcan4d	$$⊢X\in {ℝ}^{+}\to \frac{2X}{X}=2$$
5		2z	$$⊢2\in \mathbb{Z}$$
6	4 5	eqeltrdi	$$⊢X\in {ℝ}^{+}\to \frac{2X}{X}\in \mathbb{Z}$$
7		2re	$$⊢2\in ℝ$$
8	7	a1i	$$⊢X\in {ℝ}^{+}\to 2\in ℝ$$
9		rpre	$$⊢X\in {ℝ}^{+}\to X\in ℝ$$
10	8 9	remulcld	$$⊢X\in {ℝ}^{+}\to 2X\in ℝ$$
11		mod0	$$⊢\left(2X\in ℝ\wedge X\in {ℝ}^{+}\right)\to \left(2X\mathrm{mod}X=0\leftrightarrow \frac{2X}{X}\in \mathbb{Z}\right)$$
12	10 11	mpancom	$$⊢X\in {ℝ}^{+}\to \left(2X\mathrm{mod}X=0\leftrightarrow \frac{2X}{X}\in \mathbb{Z}\right)$$
13	6 12	mpbird	$$⊢X\in {ℝ}^{+}\to 2X\mathrm{mod}X=0$$