Description: Partition of a division into its integer part and the remainder. (Contributed by Alexander van der Vekens, 14-Apr-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | flpmodeq | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | modvalr | |
|
2 | 1 | eqcomd | |
3 | recn | |
|
4 | 3 | adantr | |
5 | rerpdivcl | |
|
6 | flcl | |
|
7 | 6 | zcnd | |
8 | 5 7 | syl | |
9 | rpcn | |
|
10 | 9 | adantl | |
11 | 8 10 | mulcld | |
12 | modcl | |
|
13 | 12 | recnd | |
14 | 4 11 13 | subaddd | |
15 | 2 14 | mpbid | |