# 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 𝑀 ) )