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

Metamath Proof Explorer

Theorem modeqmodmin

Description: A real number equals the difference of the real number and a positive real number modulo the positive real number. (Contributed by AV, 3-Nov-2018)

		Ref	Expression
	Assertion	modeqmodmin	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ⁺ ) → ( 𝐴 mod 𝑀 ) = ( ( 𝐴 − 𝑀 ) mod 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		modid0	⊢ ( 𝑀 ∈ ℝ⁺ → ( 𝑀 mod 𝑀 ) = 0 )
2	1	adantl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ⁺ ) → ( 𝑀 mod 𝑀 ) = 0 )
3		modge0	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ⁺ ) → 0 ≤ ( 𝐴 mod 𝑀 ) )
4	2 3	eqbrtrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ⁺ ) → ( 𝑀 mod 𝑀 ) ≤ ( 𝐴 mod 𝑀 ) )
5		simpl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ⁺ ) → 𝐴 ∈ ℝ )
6		rpre	⊢ ( 𝑀 ∈ ℝ⁺ → 𝑀 ∈ ℝ )
7	6	adantl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ⁺ ) → 𝑀 ∈ ℝ )
8		simpr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ⁺ ) → 𝑀 ∈ ℝ⁺ )
9		modsubdir	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑀 ∈ ℝ⁺ ) → ( ( 𝑀 mod 𝑀 ) ≤ ( 𝐴 mod 𝑀 ) ↔ ( ( 𝐴 − 𝑀 ) mod 𝑀 ) = ( ( 𝐴 mod 𝑀 ) − ( 𝑀 mod 𝑀 ) ) ) )
10	5 7 8 9	syl3anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ⁺ ) → ( ( 𝑀 mod 𝑀 ) ≤ ( 𝐴 mod 𝑀 ) ↔ ( ( 𝐴 − 𝑀 ) mod 𝑀 ) = ( ( 𝐴 mod 𝑀 ) − ( 𝑀 mod 𝑀 ) ) ) )
11	4 10	mpbid	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ⁺ ) → ( ( 𝐴 − 𝑀 ) mod 𝑀 ) = ( ( 𝐴 mod 𝑀 ) − ( 𝑀 mod 𝑀 ) ) )
12	2	eqcomd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ⁺ ) → 0 = ( 𝑀 mod 𝑀 ) )
13	12	oveq2d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ⁺ ) → ( ( 𝐴 mod 𝑀 ) − 0 ) = ( ( 𝐴 mod 𝑀 ) − ( 𝑀 mod 𝑀 ) ) )
14		modcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ⁺ ) → ( 𝐴 mod 𝑀 ) ∈ ℝ )
15	14	recnd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ⁺ ) → ( 𝐴 mod 𝑀 ) ∈ ℂ )
16	15	subid1d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ⁺ ) → ( ( 𝐴 mod 𝑀 ) − 0 ) = ( 𝐴 mod 𝑀 ) )
17	11 13 16	3eqtr2rd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ⁺ ) → ( 𝐴 mod 𝑀 ) = ( ( 𝐴 − 𝑀 ) mod 𝑀 ) )