| Step |
Hyp |
Ref |
Expression |
| 1 |
|
recn |
|- ( A e. RR -> A e. CC ) |
| 2 |
1
|
adantr |
|- ( ( A e. RR /\ B e. NN ) -> A e. CC ) |
| 3 |
|
nncn |
|- ( B e. NN -> B e. CC ) |
| 4 |
3
|
adantl |
|- ( ( A e. RR /\ B e. NN ) -> B e. CC ) |
| 5 |
|
1cnd |
|- ( ( A e. RR /\ B e. NN ) -> 1 e. CC ) |
| 6 |
|
subsub |
|- ( ( A e. CC /\ B e. CC /\ 1 e. CC ) -> ( A - ( B - 1 ) ) = ( ( A - B ) + 1 ) ) |
| 7 |
6
|
eqcomd |
|- ( ( A e. CC /\ B e. CC /\ 1 e. CC ) -> ( ( A - B ) + 1 ) = ( A - ( B - 1 ) ) ) |
| 8 |
2 4 5 7
|
syl3anc |
|- ( ( A e. RR /\ B e. NN ) -> ( ( A - B ) + 1 ) = ( A - ( B - 1 ) ) ) |
| 9 |
|
nnm1ge0 |
|- ( B e. NN -> 0 <_ ( B - 1 ) ) |
| 10 |
9
|
adantl |
|- ( ( A e. RR /\ B e. NN ) -> 0 <_ ( B - 1 ) ) |
| 11 |
|
nnre |
|- ( B e. NN -> B e. RR ) |
| 12 |
|
peano2rem |
|- ( B e. RR -> ( B - 1 ) e. RR ) |
| 13 |
11 12
|
syl |
|- ( B e. NN -> ( B - 1 ) e. RR ) |
| 14 |
|
subge02 |
|- ( ( A e. RR /\ ( B - 1 ) e. RR ) -> ( 0 <_ ( B - 1 ) <-> ( A - ( B - 1 ) ) <_ A ) ) |
| 15 |
14
|
bicomd |
|- ( ( A e. RR /\ ( B - 1 ) e. RR ) -> ( ( A - ( B - 1 ) ) <_ A <-> 0 <_ ( B - 1 ) ) ) |
| 16 |
13 15
|
sylan2 |
|- ( ( A e. RR /\ B e. NN ) -> ( ( A - ( B - 1 ) ) <_ A <-> 0 <_ ( B - 1 ) ) ) |
| 17 |
10 16
|
mpbird |
|- ( ( A e. RR /\ B e. NN ) -> ( A - ( B - 1 ) ) <_ A ) |
| 18 |
8 17
|
eqbrtrd |
|- ( ( A e. RR /\ B e. NN ) -> ( ( A - B ) + 1 ) <_ A ) |