This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )