Step |
Hyp |
Ref |
Expression |
1 |
|
0ne1 |
|- 0 =/= 1 |
2 |
|
0re |
|- 0 e. RR |
3 |
|
1re |
|- 1 e. RR |
4 |
2 3
|
lttri2i |
|- ( 0 =/= 1 <-> ( 0 < 1 \/ 1 < 0 ) ) |
5 |
1 4
|
mpbi |
|- ( 0 < 1 \/ 1 < 0 ) |
6 |
|
breq2 |
|- ( x = 1 -> ( 0 < x <-> 0 < 1 ) ) |
7 |
|
breq2 |
|- ( x = y -> ( 0 < x <-> 0 < y ) ) |
8 |
|
breq2 |
|- ( x = ( y + 1 ) -> ( 0 < x <-> 0 < ( y + 1 ) ) ) |
9 |
|
breq2 |
|- ( x = A -> ( 0 < x <-> 0 < A ) ) |
10 |
|
id |
|- ( 0 < 1 -> 0 < 1 ) |
11 |
|
nnre |
|- ( y e. NN -> y e. RR ) |
12 |
11
|
ad2antlr |
|- ( ( ( 0 < 1 /\ y e. NN ) /\ 0 < y ) -> y e. RR ) |
13 |
|
1red |
|- ( ( ( 0 < 1 /\ y e. NN ) /\ 0 < y ) -> 1 e. RR ) |
14 |
|
simpr |
|- ( ( ( 0 < 1 /\ y e. NN ) /\ 0 < y ) -> 0 < y ) |
15 |
|
simpll |
|- ( ( ( 0 < 1 /\ y e. NN ) /\ 0 < y ) -> 0 < 1 ) |
16 |
12 13 14 15
|
sn-addgt0d |
|- ( ( ( 0 < 1 /\ y e. NN ) /\ 0 < y ) -> 0 < ( y + 1 ) ) |
17 |
6 7 8 9 10 16
|
nnindd |
|- ( ( 0 < 1 /\ A e. NN ) -> 0 < A ) |
18 |
17
|
gt0ne0d |
|- ( ( 0 < 1 /\ A e. NN ) -> A =/= 0 ) |
19 |
18
|
ancoms |
|- ( ( A e. NN /\ 0 < 1 ) -> A =/= 0 ) |
20 |
|
breq1 |
|- ( x = 1 -> ( x < 0 <-> 1 < 0 ) ) |
21 |
|
breq1 |
|- ( x = y -> ( x < 0 <-> y < 0 ) ) |
22 |
|
breq1 |
|- ( x = ( y + 1 ) -> ( x < 0 <-> ( y + 1 ) < 0 ) ) |
23 |
|
breq1 |
|- ( x = A -> ( x < 0 <-> A < 0 ) ) |
24 |
|
id |
|- ( 1 < 0 -> 1 < 0 ) |
25 |
11
|
ad2antlr |
|- ( ( ( 1 < 0 /\ y e. NN ) /\ y < 0 ) -> y e. RR ) |
26 |
|
1red |
|- ( ( ( 1 < 0 /\ y e. NN ) /\ y < 0 ) -> 1 e. RR ) |
27 |
|
simpr |
|- ( ( ( 1 < 0 /\ y e. NN ) /\ y < 0 ) -> y < 0 ) |
28 |
|
simpll |
|- ( ( ( 1 < 0 /\ y e. NN ) /\ y < 0 ) -> 1 < 0 ) |
29 |
25 26 27 28
|
sn-addlt0d |
|- ( ( ( 1 < 0 /\ y e. NN ) /\ y < 0 ) -> ( y + 1 ) < 0 ) |
30 |
20 21 22 23 24 29
|
nnindd |
|- ( ( 1 < 0 /\ A e. NN ) -> A < 0 ) |
31 |
30
|
lt0ne0d |
|- ( ( 1 < 0 /\ A e. NN ) -> A =/= 0 ) |
32 |
31
|
ancoms |
|- ( ( A e. NN /\ 1 < 0 ) -> A =/= 0 ) |
33 |
19 32
|
jaodan |
|- ( ( A e. NN /\ ( 0 < 1 \/ 1 < 0 ) ) -> A =/= 0 ) |
34 |
5 33
|
mpan2 |
|- ( A e. NN -> A =/= 0 ) |