Metamath Proof Explorer

Theorem modifeq2int

Description: If a nonnegative integer is less than twice a positive integer, the nonnegative integer modulo the positive integer equals the nonnegative integer or the nonnegative integer minus the positive integer. (Contributed by Alexander van der Vekens, 21-May-2018)

Ref Expression
Assertion modifeq2int ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ∧ 𝐴 < ( 2 · 𝐵 ) ) → ( 𝐴 mod 𝐵 ) = if ( 𝐴 < 𝐵 , 𝐴 , ( 𝐴 − 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 nn0re ⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ℝ )
2 nnrp ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℝ+ )
3 1 2 anim12i ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) )
4 3 3adant3 ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ∧ 𝐴 < ( 2 · 𝐵 ) ) → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) )
5 nn0ge0 ⊢ ( 𝐴 ∈ ℕ0 → 0 ≤ 𝐴 )
6 5 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ∧ 𝐴 < ( 2 · 𝐵 ) ) → 0 ≤ 𝐴 )
7 6 anim1i ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ∧ 𝐴 < ( 2 · 𝐵 ) ) ∧ 𝐴 < 𝐵 ) → ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) )
8 7 ancoms ⊢ ( ( 𝐴 < 𝐵 ∧ ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ∧ 𝐴 < ( 2 · 𝐵 ) ) ) → ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) )
9 modid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) → ( 𝐴 mod 𝐵 ) = 𝐴 )
10 4 8 9 syl2an2 ⊢ ( ( 𝐴 < 𝐵 ∧ ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ∧ 𝐴 < ( 2 · 𝐵 ) ) ) → ( 𝐴 mod 𝐵 ) = 𝐴 )
11 iftrue ⊢ ( 𝐴 < 𝐵 → if ( 𝐴 < 𝐵 , 𝐴 , ( 𝐴 − 𝐵 ) ) = 𝐴 )
12 11 eqcomd ⊢ ( 𝐴 < 𝐵 → 𝐴 = if ( 𝐴 < 𝐵 , 𝐴 , ( 𝐴 − 𝐵 ) ) )
13 12 adantr ⊢ ( ( 𝐴 < 𝐵 ∧ ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ∧ 𝐴 < ( 2 · 𝐵 ) ) ) → 𝐴 = if ( 𝐴 < 𝐵 , 𝐴 , ( 𝐴 − 𝐵 ) ) )
14 10 13 eqtrd ⊢ ( ( 𝐴 < 𝐵 ∧ ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ∧ 𝐴 < ( 2 · 𝐵 ) ) ) → ( 𝐴 mod 𝐵 ) = if ( 𝐴 < 𝐵 , 𝐴 , ( 𝐴 − 𝐵 ) ) )
15 14 ex ⊢ ( 𝐴 < 𝐵 → ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ∧ 𝐴 < ( 2 · 𝐵 ) ) → ( 𝐴 mod 𝐵 ) = if ( 𝐴 < 𝐵 , 𝐴 , ( 𝐴 − 𝐵 ) ) ) )
16 4 adantr ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ∧ 𝐴 < ( 2 · 𝐵 ) ) ∧ ¬ 𝐴 < 𝐵 ) → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) )
17 nnre ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℝ )
18 lenlt ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵 ) )
19 17 1 18 syl2anr ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → ( 𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵 ) )
20 19 3adant3 ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ∧ 𝐴 < ( 2 · 𝐵 ) ) → ( 𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵 ) )
21 20 biimpar ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ∧ 𝐴 < ( 2 · 𝐵 ) ) ∧ ¬ 𝐴 < 𝐵 ) → 𝐵 ≤ 𝐴 )
22 simpl3 ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ∧ 𝐴 < ( 2 · 𝐵 ) ) ∧ ¬ 𝐴 < 𝐵 ) → 𝐴 < ( 2 · 𝐵 ) )
23 2submod ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝐵 ≤ 𝐴 ∧ 𝐴 < ( 2 · 𝐵 ) ) ) → ( 𝐴 mod 𝐵 ) = ( 𝐴 − 𝐵 ) )
24 16 21 22 23 syl12anc ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ∧ 𝐴 < ( 2 · 𝐵 ) ) ∧ ¬ 𝐴 < 𝐵 ) → ( 𝐴 mod 𝐵 ) = ( 𝐴 − 𝐵 ) )
25 iffalse ⊢ ( ¬ 𝐴 < 𝐵 → if ( 𝐴 < 𝐵 , 𝐴 , ( 𝐴 − 𝐵 ) ) = ( 𝐴 − 𝐵 ) )
26 25 adantl ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ∧ 𝐴 < ( 2 · 𝐵 ) ) ∧ ¬ 𝐴 < 𝐵 ) → if ( 𝐴 < 𝐵 , 𝐴 , ( 𝐴 − 𝐵 ) ) = ( 𝐴 − 𝐵 ) )
27 26 eqcomd ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ∧ 𝐴 < ( 2 · 𝐵 ) ) ∧ ¬ 𝐴 < 𝐵 ) → ( 𝐴 − 𝐵 ) = if ( 𝐴 < 𝐵 , 𝐴 , ( 𝐴 − 𝐵 ) ) )
28 24 27 eqtrd ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ∧ 𝐴 < ( 2 · 𝐵 ) ) ∧ ¬ 𝐴 < 𝐵 ) → ( 𝐴 mod 𝐵 ) = if ( 𝐴 < 𝐵 , 𝐴 , ( 𝐴 − 𝐵 ) ) )
29 28 expcom ⊢ ( ¬ 𝐴 < 𝐵 → ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ∧ 𝐴 < ( 2 · 𝐵 ) ) → ( 𝐴 mod 𝐵 ) = if ( 𝐴 < 𝐵 , 𝐴 , ( 𝐴 − 𝐵 ) ) ) )
30 15 29 pm2.61i ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ∧ 𝐴 < ( 2 · 𝐵 ) ) → ( 𝐴 mod 𝐵 ) = if ( 𝐴 < 𝐵 , 𝐴 , ( 𝐴 − 𝐵 ) ) )