Metamath Proof Explorer

Theorem modid

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

Ref Expression
Assertion modid ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) → ( 𝐴 mod 𝐵 ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 modval ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 mod 𝐵 ) = ( 𝐴 − ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) ) )
2 1 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) → ( 𝐴 mod 𝐵 ) = ( 𝐴 − ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) ) )
3 rerpdivcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 / 𝐵 ) ∈ ℝ )
4 3 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) → ( 𝐴 / 𝐵 ) ∈ ℝ )
5 4 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) → ( 𝐴 / 𝐵 ) ∈ ℂ )
6 addid2 ⊢ ( ( 𝐴 / 𝐵 ) ∈ ℂ → ( 0 + ( 𝐴 / 𝐵 ) ) = ( 𝐴 / 𝐵 ) )
7 6 fveq2d ⊢ ( ( 𝐴 / 𝐵 ) ∈ ℂ → ( ⌊ ‘ ( 0 + ( 𝐴 / 𝐵 ) ) ) = ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) )
8 5 7 syl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) → ( ⌊ ‘ ( 0 + ( 𝐴 / 𝐵 ) ) ) = ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) )
9 rpregt0 ⊢ ( 𝐵 ∈ ℝ+ → ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) )
10 divge0 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → 0 ≤ ( 𝐴 / 𝐵 ) )
11 9 10 sylan2 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ+ ) → 0 ≤ ( 𝐴 / 𝐵 ) )
12 11 an32s ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) ∧ 0 ≤ 𝐴 ) → 0 ≤ ( 𝐴 / 𝐵 ) )
13 12 adantrr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) → 0 ≤ ( 𝐴 / 𝐵 ) )
14 simpr ⊢ ( ( 𝐵 ∈ ℝ+ ∧ 𝐴 < 𝐵 ) → 𝐴 < 𝐵 )
15 rpcn ⊢ ( 𝐵 ∈ ℝ+ → 𝐵 ∈ ℂ )
16 15 mulid1d ⊢ ( 𝐵 ∈ ℝ+ → ( 𝐵 · 1 ) = 𝐵 )
17 16 adantr ⊢ ( ( 𝐵 ∈ ℝ+ ∧ 𝐴 < 𝐵 ) → ( 𝐵 · 1 ) = 𝐵 )
18 14 17 breqtrrd ⊢ ( ( 𝐵 ∈ ℝ+ ∧ 𝐴 < 𝐵 ) → 𝐴 < ( 𝐵 · 1 ) )
19 18 ad2ant2l ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) → 𝐴 < ( 𝐵 · 1 ) )
20 simpll ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) → 𝐴 ∈ ℝ )
21 9 ad2antlr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) → ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) )
22 1re ⊢ 1 ∈ ℝ
23 ltdivmul ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → ( ( 𝐴 / 𝐵 ) < 1 ↔ 𝐴 < ( 𝐵 · 1 ) ) )
24 22 23 mp3an2 ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → ( ( 𝐴 / 𝐵 ) < 1 ↔ 𝐴 < ( 𝐵 · 1 ) ) )
25 20 21 24 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) → ( ( 𝐴 / 𝐵 ) < 1 ↔ 𝐴 < ( 𝐵 · 1 ) ) )
26 19 25 mpbird ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) → ( 𝐴 / 𝐵 ) < 1 )
27 0z ⊢ 0 ∈ ℤ
28 flbi2 ⊢ ( ( 0 ∈ ℤ ∧ ( 𝐴 / 𝐵 ) ∈ ℝ ) → ( ( ⌊ ‘ ( 0 + ( 𝐴 / 𝐵 ) ) ) = 0 ↔ ( 0 ≤ ( 𝐴 / 𝐵 ) ∧ ( 𝐴 / 𝐵 ) < 1 ) ) )
29 27 4 28 sylancr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) → ( ( ⌊ ‘ ( 0 + ( 𝐴 / 𝐵 ) ) ) = 0 ↔ ( 0 ≤ ( 𝐴 / 𝐵 ) ∧ ( 𝐴 / 𝐵 ) < 1 ) ) )
30 13 26 29 mpbir2and ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) → ( ⌊ ‘ ( 0 + ( 𝐴 / 𝐵 ) ) ) = 0 )
31 8 30 eqtr3d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) → ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) = 0 )
32 31 oveq2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) → ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) = ( 𝐵 · 0 ) )
33 15 mul01d ⊢ ( 𝐵 ∈ ℝ+ → ( 𝐵 · 0 ) = 0 )
34 33 ad2antlr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) → ( 𝐵 · 0 ) = 0 )
35 32 34 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) → ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) = 0 )
36 35 oveq2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) → ( 𝐴 − ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) ) = ( 𝐴 − 0 ) )
37 recn ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
38 37 subid1d ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 − 0 ) = 𝐴 )
39 38 ad2antrr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) → ( 𝐴 − 0 ) = 𝐴 )
40 36 39 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) → ( 𝐴 − ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) ) = 𝐴 )
41 2 40 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) → ( 𝐴 mod 𝐵 ) = 𝐴 )