| Step |
Hyp |
Ref |
Expression |
| 1 |
|
modval |
|- ( ( A e. RR /\ B e. RR+ ) -> ( A mod B ) = ( A - ( B x. ( |_ ` ( A / B ) ) ) ) ) |
| 2 |
1
|
adantr |
|- ( ( ( A e. RR /\ B e. RR+ ) /\ ( 0 <_ A /\ A < B ) ) -> ( A mod B ) = ( A - ( B x. ( |_ ` ( A / B ) ) ) ) ) |
| 3 |
|
rerpdivcl |
|- ( ( A e. RR /\ B e. RR+ ) -> ( A / B ) e. RR ) |
| 4 |
3
|
adantr |
|- ( ( ( A e. RR /\ B e. RR+ ) /\ ( 0 <_ A /\ A < B ) ) -> ( A / B ) e. RR ) |
| 5 |
4
|
recnd |
|- ( ( ( A e. RR /\ B e. RR+ ) /\ ( 0 <_ A /\ A < B ) ) -> ( A / B ) e. CC ) |
| 6 |
|
addlid |
|- ( ( A / B ) e. CC -> ( 0 + ( A / B ) ) = ( A / B ) ) |
| 7 |
6
|
fveq2d |
|- ( ( A / B ) e. CC -> ( |_ ` ( 0 + ( A / B ) ) ) = ( |_ ` ( A / B ) ) ) |
| 8 |
5 7
|
syl |
|- ( ( ( A e. RR /\ B e. RR+ ) /\ ( 0 <_ A /\ A < B ) ) -> ( |_ ` ( 0 + ( A / B ) ) ) = ( |_ ` ( A / B ) ) ) |
| 9 |
|
rpregt0 |
|- ( B e. RR+ -> ( B e. RR /\ 0 < B ) ) |
| 10 |
|
divge0 |
|- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 < B ) ) -> 0 <_ ( A / B ) ) |
| 11 |
9 10
|
sylan2 |
|- ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR+ ) -> 0 <_ ( A / B ) ) |
| 12 |
11
|
an32s |
|- ( ( ( A e. RR /\ B e. RR+ ) /\ 0 <_ A ) -> 0 <_ ( A / B ) ) |
| 13 |
12
|
adantrr |
|- ( ( ( A e. RR /\ B e. RR+ ) /\ ( 0 <_ A /\ A < B ) ) -> 0 <_ ( A / B ) ) |
| 14 |
|
simpr |
|- ( ( B e. RR+ /\ A < B ) -> A < B ) |
| 15 |
|
rpcn |
|- ( B e. RR+ -> B e. CC ) |
| 16 |
15
|
mulridd |
|- ( B e. RR+ -> ( B x. 1 ) = B ) |
| 17 |
16
|
adantr |
|- ( ( B e. RR+ /\ A < B ) -> ( B x. 1 ) = B ) |
| 18 |
14 17
|
breqtrrd |
|- ( ( B e. RR+ /\ A < B ) -> A < ( B x. 1 ) ) |
| 19 |
18
|
ad2ant2l |
|- ( ( ( A e. RR /\ B e. RR+ ) /\ ( 0 <_ A /\ A < B ) ) -> A < ( B x. 1 ) ) |
| 20 |
|
simpll |
|- ( ( ( A e. RR /\ B e. RR+ ) /\ ( 0 <_ A /\ A < B ) ) -> A e. RR ) |
| 21 |
9
|
ad2antlr |
|- ( ( ( A e. RR /\ B e. RR+ ) /\ ( 0 <_ A /\ A < B ) ) -> ( B e. RR /\ 0 < B ) ) |
| 22 |
|
1re |
|- 1 e. RR |
| 23 |
|
ltdivmul |
|- ( ( A e. RR /\ 1 e. RR /\ ( B e. RR /\ 0 < B ) ) -> ( ( A / B ) < 1 <-> A < ( B x. 1 ) ) ) |
| 24 |
22 23
|
mp3an2 |
|- ( ( A e. RR /\ ( B e. RR /\ 0 < B ) ) -> ( ( A / B ) < 1 <-> A < ( B x. 1 ) ) ) |
| 25 |
20 21 24
|
syl2anc |
|- ( ( ( A e. RR /\ B e. RR+ ) /\ ( 0 <_ A /\ A < B ) ) -> ( ( A / B ) < 1 <-> A < ( B x. 1 ) ) ) |
| 26 |
19 25
|
mpbird |
|- ( ( ( A e. RR /\ B e. RR+ ) /\ ( 0 <_ A /\ A < B ) ) -> ( A / B ) < 1 ) |
| 27 |
|
0z |
|- 0 e. ZZ |
| 28 |
|
flbi2 |
|- ( ( 0 e. ZZ /\ ( A / B ) e. RR ) -> ( ( |_ ` ( 0 + ( A / B ) ) ) = 0 <-> ( 0 <_ ( A / B ) /\ ( A / B ) < 1 ) ) ) |
| 29 |
27 4 28
|
sylancr |
|- ( ( ( A e. RR /\ B e. RR+ ) /\ ( 0 <_ A /\ A < B ) ) -> ( ( |_ ` ( 0 + ( A / B ) ) ) = 0 <-> ( 0 <_ ( A / B ) /\ ( A / B ) < 1 ) ) ) |
| 30 |
13 26 29
|
mpbir2and |
|- ( ( ( A e. RR /\ B e. RR+ ) /\ ( 0 <_ A /\ A < B ) ) -> ( |_ ` ( 0 + ( A / B ) ) ) = 0 ) |
| 31 |
8 30
|
eqtr3d |
|- ( ( ( A e. RR /\ B e. RR+ ) /\ ( 0 <_ A /\ A < B ) ) -> ( |_ ` ( A / B ) ) = 0 ) |
| 32 |
31
|
oveq2d |
|- ( ( ( A e. RR /\ B e. RR+ ) /\ ( 0 <_ A /\ A < B ) ) -> ( B x. ( |_ ` ( A / B ) ) ) = ( B x. 0 ) ) |
| 33 |
15
|
mul01d |
|- ( B e. RR+ -> ( B x. 0 ) = 0 ) |
| 34 |
33
|
ad2antlr |
|- ( ( ( A e. RR /\ B e. RR+ ) /\ ( 0 <_ A /\ A < B ) ) -> ( B x. 0 ) = 0 ) |
| 35 |
32 34
|
eqtrd |
|- ( ( ( A e. RR /\ B e. RR+ ) /\ ( 0 <_ A /\ A < B ) ) -> ( B x. ( |_ ` ( A / B ) ) ) = 0 ) |
| 36 |
35
|
oveq2d |
|- ( ( ( A e. RR /\ B e. RR+ ) /\ ( 0 <_ A /\ A < B ) ) -> ( A - ( B x. ( |_ ` ( A / B ) ) ) ) = ( A - 0 ) ) |
| 37 |
|
recn |
|- ( A e. RR -> A e. CC ) |
| 38 |
37
|
subid1d |
|- ( A e. RR -> ( A - 0 ) = A ) |
| 39 |
38
|
ad2antrr |
|- ( ( ( A e. RR /\ B e. RR+ ) /\ ( 0 <_ A /\ A < B ) ) -> ( A - 0 ) = A ) |
| 40 |
36 39
|
eqtrd |
|- ( ( ( A e. RR /\ B e. RR+ ) /\ ( 0 <_ A /\ A < B ) ) -> ( A - ( B x. ( |_ ` ( A / B ) ) ) ) = A ) |
| 41 |
2 40
|
eqtrd |
|- ( ( ( A e. RR /\ B e. RR+ ) /\ ( 0 <_ A /\ A < B ) ) -> ( A mod B ) = A ) |