| Step |
Hyp |
Ref |
Expression |
| 1 |
|
1re |
|- 1 e. RR |
| 2 |
|
readdlid |
|- ( 1 e. RR -> ( 0 + 1 ) = 1 ) |
| 3 |
1 2
|
ax-mp |
|- ( 0 + 1 ) = 1 |
| 4 |
|
sn-1ne2 |
|- 1 =/= 2 |
| 5 |
|
2re |
|- 2 e. RR |
| 6 |
1 5
|
lttri2i |
|- ( 1 =/= 2 <-> ( 1 < 2 \/ 2 < 1 ) ) |
| 7 |
4 6
|
mpbi |
|- ( 1 < 2 \/ 2 < 1 ) |
| 8 |
|
1red |
|- ( 1 < 2 -> 1 e. RR ) |
| 9 |
1 5 1
|
ltadd2i |
|- ( 1 < 2 <-> ( 1 + 1 ) < ( 1 + 2 ) ) |
| 10 |
9
|
biimpi |
|- ( 1 < 2 -> ( 1 + 1 ) < ( 1 + 2 ) ) |
| 11 |
|
1p1e2 |
|- ( 1 + 1 ) = 2 |
| 12 |
|
1p2e3 |
|- ( 1 + 2 ) = 3 |
| 13 |
10 11 12
|
3brtr3g |
|- ( 1 < 2 -> 2 < 3 ) |
| 14 |
|
3re |
|- 3 e. RR |
| 15 |
1 5 14
|
lttri |
|- ( ( 1 < 2 /\ 2 < 3 ) -> 1 < 3 ) |
| 16 |
13 15
|
mpdan |
|- ( 1 < 2 -> 1 < 3 ) |
| 17 |
8 16
|
ltned |
|- ( 1 < 2 -> 1 =/= 3 ) |
| 18 |
14
|
a1i |
|- ( 2 < 1 -> 3 e. RR ) |
| 19 |
5 1 1
|
ltadd2i |
|- ( 2 < 1 <-> ( 1 + 2 ) < ( 1 + 1 ) ) |
| 20 |
19
|
biimpi |
|- ( 2 < 1 -> ( 1 + 2 ) < ( 1 + 1 ) ) |
| 21 |
20 12 11
|
3brtr3g |
|- ( 2 < 1 -> 3 < 2 ) |
| 22 |
14 5 1
|
lttri |
|- ( ( 3 < 2 /\ 2 < 1 ) -> 3 < 1 ) |
| 23 |
21 22
|
mpancom |
|- ( 2 < 1 -> 3 < 1 ) |
| 24 |
18 23
|
gtned |
|- ( 2 < 1 -> 1 =/= 3 ) |
| 25 |
17 24
|
jaoi |
|- ( ( 1 < 2 \/ 2 < 1 ) -> 1 =/= 3 ) |
| 26 |
7 25
|
ax-mp |
|- 1 =/= 3 |
| 27 |
|
df-3 |
|- 3 = ( 2 + 1 ) |
| 28 |
26 27
|
neeqtri |
|- 1 =/= ( 2 + 1 ) |
| 29 |
3 28
|
eqnetri |
|- ( 0 + 1 ) =/= ( 2 + 1 ) |
| 30 |
|
oveq1 |
|- ( 0 = 2 -> ( 0 + 1 ) = ( 2 + 1 ) ) |
| 31 |
30
|
necon3i |
|- ( ( 0 + 1 ) =/= ( 2 + 1 ) -> 0 =/= 2 ) |
| 32 |
29 31
|
ax-mp |
|- 0 =/= 2 |