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

Metamath Proof Explorer

Theorem modabs

Description: Absorption law for modulo. (Contributed by NM, 29-Dec-2008)

Ref Expression
Assertion modabs ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) ∧ 𝐵 ≤ 𝐶 ) → ( ( 𝐴 mod 𝐵 ) mod 𝐶 ) = ( 𝐴 mod 𝐵 ) )

Proof

Step Hyp Ref Expression
1 modcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 mod 𝐵 ) ∈ ℝ )
2 1 anim1i ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) ∧ 𝐶 ∈ ℝ+ ) → ( ( 𝐴 mod 𝐵 ) ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) )
3 2 3impa ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) → ( ( 𝐴 mod 𝐵 ) ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) )
4 3 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) ∧ 𝐵 ≤ 𝐶 ) → ( ( 𝐴 mod 𝐵 ) ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) )
5 modge0 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → 0 ≤ ( 𝐴 mod 𝐵 ) )
6 5 3adant3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) → 0 ≤ ( 𝐴 mod 𝐵 ) )
7 6 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) ∧ 𝐵 ≤ 𝐶 ) → 0 ≤ ( 𝐴 mod 𝐵 ) )
8 1 3adant3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐴 mod 𝐵 ) ∈ ℝ )
9 8 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) ∧ 𝐵 ≤ 𝐶 ) → ( 𝐴 mod 𝐵 ) ∈ ℝ )
10 rpre ⊢ ( 𝐵 ∈ ℝ+ → 𝐵 ∈ ℝ )
11 10 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) → 𝐵 ∈ ℝ )
12 11 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) ∧ 𝐵 ≤ 𝐶 ) → 𝐵 ∈ ℝ )
13 rpre ⊢ ( 𝐶 ∈ ℝ+ → 𝐶 ∈ ℝ )
14 13 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) → 𝐶 ∈ ℝ )
15 14 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) ∧ 𝐵 ≤ 𝐶 ) → 𝐶 ∈ ℝ )
16 modlt ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 mod 𝐵 ) < 𝐵 )
17 16 3adant3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐴 mod 𝐵 ) < 𝐵 )
18 17 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) ∧ 𝐵 ≤ 𝐶 ) → ( 𝐴 mod 𝐵 ) < 𝐵 )
19 simpr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) ∧ 𝐵 ≤ 𝐶 ) → 𝐵 ≤ 𝐶 )
20 9 12 15 18 19 ltletrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) ∧ 𝐵 ≤ 𝐶 ) → ( 𝐴 mod 𝐵 ) < 𝐶 )
21 modid ⊢ ( ( ( ( 𝐴 mod 𝐵 ) ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) ∧ ( 0 ≤ ( 𝐴 mod 𝐵 ) ∧ ( 𝐴 mod 𝐵 ) < 𝐶 ) ) → ( ( 𝐴 mod 𝐵 ) mod 𝐶 ) = ( 𝐴 mod 𝐵 ) )
22 4 7 20 21 syl12anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) ∧ 𝐵 ≤ 𝐶 ) → ( ( 𝐴 mod 𝐵 ) mod 𝐶 ) = ( 𝐴 mod 𝐵 ) )