Step |
Hyp |
Ref |
Expression |
1 |
|
dp2lt.a |
|- A e. NN0 |
2 |
|
dp2lt.b |
|- B e. RR+ |
3 |
|
dp2ltsuc.1 |
|- B < ; 1 0 |
4 |
|
dp2ltsuc.2 |
|- ( A + 1 ) = C |
5 |
|
rpre |
|- ( B e. RR+ -> B e. RR ) |
6 |
2 5
|
ax-mp |
|- B e. RR |
7 |
|
10re |
|- ; 1 0 e. RR |
8 |
|
10pos |
|- 0 < ; 1 0 |
9 |
6 7 7 8
|
ltdiv1ii |
|- ( B < ; 1 0 <-> ( B / ; 1 0 ) < ( ; 1 0 / ; 1 0 ) ) |
10 |
3 9
|
mpbi |
|- ( B / ; 1 0 ) < ( ; 1 0 / ; 1 0 ) |
11 |
7
|
recni |
|- ; 1 0 e. CC |
12 |
|
10nn |
|- ; 1 0 e. NN |
13 |
12
|
nnne0i |
|- ; 1 0 =/= 0 |
14 |
11 13
|
dividi |
|- ( ; 1 0 / ; 1 0 ) = 1 |
15 |
10 14
|
breqtri |
|- ( B / ; 1 0 ) < 1 |
16 |
6 7 13
|
redivcli |
|- ( B / ; 1 0 ) e. RR |
17 |
|
1re |
|- 1 e. RR |
18 |
1
|
nn0rei |
|- A e. RR |
19 |
16 17 18
|
ltadd2i |
|- ( ( B / ; 1 0 ) < 1 <-> ( A + ( B / ; 1 0 ) ) < ( A + 1 ) ) |
20 |
15 19
|
mpbi |
|- ( A + ( B / ; 1 0 ) ) < ( A + 1 ) |
21 |
|
df-dp2 |
|- _ A B = ( A + ( B / ; 1 0 ) ) |
22 |
4
|
eqcomi |
|- C = ( A + 1 ) |
23 |
20 21 22
|
3brtr4i |
|- _ A B < C |