Step |
Hyp |
Ref |
Expression |
1 |
|
dp2lt.a |
|- A e. NN0 |
2 |
|
dp2lt.b |
|- B e. RR+ |
3 |
|
dp2lt.c |
|- C e. RR+ |
4 |
|
dp2lt.l |
|- B < C |
5 |
|
rpssre |
|- RR+ C_ RR |
6 |
5 2
|
sselii |
|- B e. RR |
7 |
|
10re |
|- ; 1 0 e. RR |
8 |
|
0re |
|- 0 e. RR |
9 |
|
10pos |
|- 0 < ; 1 0 |
10 |
8 9
|
gtneii |
|- ; 1 0 =/= 0 |
11 |
|
redivcl |
|- ( ( B e. RR /\ ; 1 0 e. RR /\ ; 1 0 =/= 0 ) -> ( B / ; 1 0 ) e. RR ) |
12 |
6 7 10 11
|
mp3an |
|- ( B / ; 1 0 ) e. RR |
13 |
5 3
|
sselii |
|- C e. RR |
14 |
|
redivcl |
|- ( ( C e. RR /\ ; 1 0 e. RR /\ ; 1 0 =/= 0 ) -> ( C / ; 1 0 ) e. RR ) |
15 |
13 7 10 14
|
mp3an |
|- ( C / ; 1 0 ) e. RR |
16 |
1
|
nn0rei |
|- A e. RR |
17 |
12 15 16
|
3pm3.2i |
|- ( ( B / ; 1 0 ) e. RR /\ ( C / ; 1 0 ) e. RR /\ A e. RR ) |
18 |
7 9
|
pm3.2i |
|- ( ; 1 0 e. RR /\ 0 < ; 1 0 ) |
19 |
|
ltdiv1 |
|- ( ( B e. RR /\ C e. RR /\ ( ; 1 0 e. RR /\ 0 < ; 1 0 ) ) -> ( B < C <-> ( B / ; 1 0 ) < ( C / ; 1 0 ) ) ) |
20 |
6 13 18 19
|
mp3an |
|- ( B < C <-> ( B / ; 1 0 ) < ( C / ; 1 0 ) ) |
21 |
4 20
|
mpbi |
|- ( B / ; 1 0 ) < ( C / ; 1 0 ) |
22 |
|
axltadd |
|- ( ( ( B / ; 1 0 ) e. RR /\ ( C / ; 1 0 ) e. RR /\ A e. RR ) -> ( ( B / ; 1 0 ) < ( C / ; 1 0 ) -> ( A + ( B / ; 1 0 ) ) < ( A + ( C / ; 1 0 ) ) ) ) |
23 |
22
|
imp |
|- ( ( ( ( B / ; 1 0 ) e. RR /\ ( C / ; 1 0 ) e. RR /\ A e. RR ) /\ ( B / ; 1 0 ) < ( C / ; 1 0 ) ) -> ( A + ( B / ; 1 0 ) ) < ( A + ( C / ; 1 0 ) ) ) |
24 |
17 21 23
|
mp2an |
|- ( A + ( B / ; 1 0 ) ) < ( A + ( C / ; 1 0 ) ) |
25 |
|
df-dp2 |
|- _ A B = ( A + ( B / ; 1 0 ) ) |
26 |
|
df-dp2 |
|- _ A C = ( A + ( C / ; 1 0 ) ) |
27 |
24 25 26
|
3brtr4i |
|- _ A B < _ A C |