Step |
Hyp |
Ref |
Expression |
1 |
|
rpre |
|- ( B e. RR+ -> B e. RR ) |
2 |
|
ax-1rid |
|- ( B e. RR -> ( B x. 1 ) = B ) |
3 |
1 2
|
syl |
|- ( B e. RR+ -> ( B x. 1 ) = B ) |
4 |
3
|
adantl |
|- ( ( A e. RR /\ B e. RR+ ) -> ( B x. 1 ) = B ) |
5 |
4
|
oveq2d |
|- ( ( A e. RR /\ B e. RR+ ) -> ( A - ( B x. 1 ) ) = ( A - B ) ) |
6 |
5
|
oveq1d |
|- ( ( A e. RR /\ B e. RR+ ) -> ( ( A - ( B x. 1 ) ) mod B ) = ( ( A - B ) mod B ) ) |
7 |
6
|
adantr |
|- ( ( ( A e. RR /\ B e. RR+ ) /\ ( B <_ A /\ A < ( 2 x. B ) ) ) -> ( ( A - ( B x. 1 ) ) mod B ) = ( ( A - B ) mod B ) ) |
8 |
|
simpl |
|- ( ( A e. RR /\ B e. RR+ ) -> A e. RR ) |
9 |
|
simpr |
|- ( ( A e. RR /\ B e. RR+ ) -> B e. RR+ ) |
10 |
|
1zzd |
|- ( ( A e. RR /\ B e. RR+ ) -> 1 e. ZZ ) |
11 |
8 9 10
|
3jca |
|- ( ( A e. RR /\ B e. RR+ ) -> ( A e. RR /\ B e. RR+ /\ 1 e. ZZ ) ) |
12 |
11
|
adantr |
|- ( ( ( A e. RR /\ B e. RR+ ) /\ ( B <_ A /\ A < ( 2 x. B ) ) ) -> ( A e. RR /\ B e. RR+ /\ 1 e. ZZ ) ) |
13 |
|
modcyc2 |
|- ( ( A e. RR /\ B e. RR+ /\ 1 e. ZZ ) -> ( ( A - ( B x. 1 ) ) mod B ) = ( A mod B ) ) |
14 |
12 13
|
syl |
|- ( ( ( A e. RR /\ B e. RR+ ) /\ ( B <_ A /\ A < ( 2 x. B ) ) ) -> ( ( A - ( B x. 1 ) ) mod B ) = ( A mod B ) ) |
15 |
|
resubcl |
|- ( ( A e. RR /\ B e. RR ) -> ( A - B ) e. RR ) |
16 |
1 15
|
sylan2 |
|- ( ( A e. RR /\ B e. RR+ ) -> ( A - B ) e. RR ) |
17 |
16 9
|
jca |
|- ( ( A e. RR /\ B e. RR+ ) -> ( ( A - B ) e. RR /\ B e. RR+ ) ) |
18 |
|
subge0 |
|- ( ( A e. RR /\ B e. RR ) -> ( 0 <_ ( A - B ) <-> B <_ A ) ) |
19 |
1 18
|
sylan2 |
|- ( ( A e. RR /\ B e. RR+ ) -> ( 0 <_ ( A - B ) <-> B <_ A ) ) |
20 |
19
|
bicomd |
|- ( ( A e. RR /\ B e. RR+ ) -> ( B <_ A <-> 0 <_ ( A - B ) ) ) |
21 |
|
rpcn |
|- ( B e. RR+ -> B e. CC ) |
22 |
21
|
2timesd |
|- ( B e. RR+ -> ( 2 x. B ) = ( B + B ) ) |
23 |
22
|
adantl |
|- ( ( A e. RR /\ B e. RR+ ) -> ( 2 x. B ) = ( B + B ) ) |
24 |
23
|
breq2d |
|- ( ( A e. RR /\ B e. RR+ ) -> ( A < ( 2 x. B ) <-> A < ( B + B ) ) ) |
25 |
1
|
adantl |
|- ( ( A e. RR /\ B e. RR+ ) -> B e. RR ) |
26 |
8 25 25
|
ltsubaddd |
|- ( ( A e. RR /\ B e. RR+ ) -> ( ( A - B ) < B <-> A < ( B + B ) ) ) |
27 |
24 26
|
bitr4d |
|- ( ( A e. RR /\ B e. RR+ ) -> ( A < ( 2 x. B ) <-> ( A - B ) < B ) ) |
28 |
20 27
|
anbi12d |
|- ( ( A e. RR /\ B e. RR+ ) -> ( ( B <_ A /\ A < ( 2 x. B ) ) <-> ( 0 <_ ( A - B ) /\ ( A - B ) < B ) ) ) |
29 |
28
|
biimpa |
|- ( ( ( A e. RR /\ B e. RR+ ) /\ ( B <_ A /\ A < ( 2 x. B ) ) ) -> ( 0 <_ ( A - B ) /\ ( A - B ) < B ) ) |
30 |
|
modid |
|- ( ( ( ( A - B ) e. RR /\ B e. RR+ ) /\ ( 0 <_ ( A - B ) /\ ( A - B ) < B ) ) -> ( ( A - B ) mod B ) = ( A - B ) ) |
31 |
17 29 30
|
syl2an2r |
|- ( ( ( A e. RR /\ B e. RR+ ) /\ ( B <_ A /\ A < ( 2 x. B ) ) ) -> ( ( A - B ) mod B ) = ( A - B ) ) |
32 |
7 14 31
|
3eqtr3d |
|- ( ( ( A e. RR /\ B e. RR+ ) /\ ( B <_ A /\ A < ( 2 x. B ) ) ) -> ( A mod B ) = ( A - B ) ) |