Metamath Proof Explorer

Theorem modid

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

Ref Expression
Assertion modid ⊢A∈ℝ∧B∈ℝ+∧0≤A∧A<B→AmodB=A

Proof

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