Step |
Hyp |
Ref |
Expression |
1 |
|
rpgt0 |
|- ( A e. RR+ -> 0 < A ) |
2 |
1
|
3ad2ant3 |
|- ( ( M e. RR /\ N e. RR /\ A e. RR+ ) -> 0 < A ) |
3 |
|
rpre |
|- ( A e. RR+ -> A e. RR ) |
4 |
3
|
3ad2ant3 |
|- ( ( M e. RR /\ N e. RR /\ A e. RR+ ) -> A e. RR ) |
5 |
|
simp1 |
|- ( ( M e. RR /\ N e. RR /\ A e. RR+ ) -> M e. RR ) |
6 |
4 5
|
ltaddposd |
|- ( ( M e. RR /\ N e. RR /\ A e. RR+ ) -> ( 0 < A <-> M < ( M + A ) ) ) |
7 |
2 6
|
mpbid |
|- ( ( M e. RR /\ N e. RR /\ A e. RR+ ) -> M < ( M + A ) ) |
8 |
|
simpl |
|- ( ( M e. RR /\ A e. RR+ ) -> M e. RR ) |
9 |
3
|
adantl |
|- ( ( M e. RR /\ A e. RR+ ) -> A e. RR ) |
10 |
8 9
|
readdcld |
|- ( ( M e. RR /\ A e. RR+ ) -> ( M + A ) e. RR ) |
11 |
10
|
3adant2 |
|- ( ( M e. RR /\ N e. RR /\ A e. RR+ ) -> ( M + A ) e. RR ) |
12 |
|
simp2 |
|- ( ( M e. RR /\ N e. RR /\ A e. RR+ ) -> N e. RR ) |
13 |
|
ltletr |
|- ( ( M e. RR /\ ( M + A ) e. RR /\ N e. RR ) -> ( ( M < ( M + A ) /\ ( M + A ) <_ N ) -> M < N ) ) |
14 |
5 11 12 13
|
syl3anc |
|- ( ( M e. RR /\ N e. RR /\ A e. RR+ ) -> ( ( M < ( M + A ) /\ ( M + A ) <_ N ) -> M < N ) ) |
15 |
7 14
|
mpand |
|- ( ( M e. RR /\ N e. RR /\ A e. RR+ ) -> ( ( M + A ) <_ N -> M < N ) ) |