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	⊢ ( 𝑋 ∈ ℝ+ → ( ( 2 · 𝑋 ) mod 𝑋 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		2cnd	⊢ ( 𝑋 ∈ ℝ+ → 2 ∈ ℂ )
2		rpcn	⊢ ( 𝑋 ∈ ℝ+ → 𝑋 ∈ ℂ )
3		rpne0	⊢ ( 𝑋 ∈ ℝ+ → 𝑋 ≠ 0 )
4	1 2 3	divcan4d	⊢ ( 𝑋 ∈ ℝ+ → ( ( 2 · 𝑋 ) / 𝑋 ) = 2 )
5		2z	⊢ 2 ∈ ℤ
6	4 5	eqeltrdi	⊢ ( 𝑋 ∈ ℝ+ → ( ( 2 · 𝑋 ) / 𝑋 ) ∈ ℤ )
7		2re	⊢ 2 ∈ ℝ
8	7	a1i	⊢ ( 𝑋 ∈ ℝ+ → 2 ∈ ℝ )
9		rpre	⊢ ( 𝑋 ∈ ℝ+ → 𝑋 ∈ ℝ )
10	8 9	remulcld	⊢ ( 𝑋 ∈ ℝ+ → ( 2 · 𝑋 ) ∈ ℝ )
11		mod0	⊢ ( ( ( 2 · 𝑋 ) ∈ ℝ ∧ 𝑋 ∈ ℝ+ ) → ( ( ( 2 · 𝑋 ) mod 𝑋 ) = 0 ↔ ( ( 2 · 𝑋 ) / 𝑋 ) ∈ ℤ ) )
12	10 11	mpancom	⊢ ( 𝑋 ∈ ℝ+ → ( ( ( 2 · 𝑋 ) mod 𝑋 ) = 0 ↔ ( ( 2 · 𝑋 ) / 𝑋 ) ∈ ℤ ) )
13	6 12	mpbird	⊢ ( 𝑋 ∈ ℝ+ → ( ( 2 · 𝑋 ) mod 𝑋 ) = 0 )