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 2 X \mod X = 0$

Step	Hyp	Ref	Expression
1		2cnd	$⊢ X \in ℝ^{+} \to 2 \in ℂ$
2		rpcn	$⊢ X \in ℝ^{+} \to X \in ℂ$
3		rpne0	$⊢ X \in ℝ^{+} \to X \neq 0$
4	1 2 3	divcan4d	$⊢ X \in ℝ^{+} \to \frac{2 X}{X} = 2$
5		2z	$⊢ 2 \in ℤ$
6	4 5	eqeltrdi	$⊢ X \in ℝ^{+} \to \frac{2 X}{X} \in ℤ$
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 2 X \in ℝ$
11		mod0	$⊢ (2 X \in ℝ \land X \in ℝ^{+}) \to (2 X \mod X = 0 \leftrightarrow \frac{2 X}{X} \in ℤ)$
12	10 11	mpancom	$⊢ X \in ℝ^{+} \to (2 X \mod X = 0 \leftrightarrow \frac{2 X}{X} \in ℤ)$
13	6 12	mpbird	$⊢ X \in ℝ^{+} \to 2 X \mod X = 0$

Metamath Proof Explorer