Step |
Hyp |
Ref |
Expression |
1 |
|
1re |
|- 1 e. RR |
2 |
|
readdid2 |
|- ( 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 |