Theorem lgslem2

Description: The set Z of all integers with absolute value at most 1 contains { -u 1 , 0 , 1 } . (Contributed by Mario Carneiro, 4-Feb-2015)

	Ref	Expression
Hypothesis	lgslem2.z	|- Z = { x e. ZZ | ( abs ` x ) <_ 1 }
Assertion	lgslem2	|- ( -u 1 e. Z /\ 0 e. Z /\ 1 e. Z )

Proof

Step	Hyp	Ref	Expression
1		lgslem2.z	|- Z = { x e. ZZ | ( abs ` x ) <_ 1 }
2		neg1z	|- -u 1 e. ZZ
3		1le1	|- 1 <_ 1
4		fveq2	|- ( x = -u 1 -> ( abs ` x ) = ( abs ` -u 1 ) )
5		ax-1cn	|- 1 e. CC
6	5	absnegi	|- ( abs ` -u 1 ) = ( abs ` 1 )
7		abs1	|- ( abs ` 1 ) = 1
8	6 7	eqtri	|- ( abs ` -u 1 ) = 1
9	4 8	eqtrdi	|- ( x = -u 1 -> ( abs ` x ) = 1 )
10	9	breq1d	|- ( x = -u 1 -> ( ( abs ` x ) <_ 1 <-> 1 <_ 1 ) )
11	10 1	elrab2	|- ( -u 1 e. Z <-> ( -u 1 e. ZZ /\ 1 <_ 1 ) )
12	2 3 11	mpbir2an	|- -u 1 e. Z
13		0z	|- 0 e. ZZ
14		0le1	|- 0 <_ 1
15		fveq2	|- ( x = 0 -> ( abs ` x ) = ( abs ` 0 ) )
16		abs0	|- ( abs ` 0 ) = 0
17	15 16	eqtrdi	|- ( x = 0 -> ( abs ` x ) = 0 )
18	17	breq1d	|- ( x = 0 -> ( ( abs ` x ) <_ 1 <-> 0 <_ 1 ) )
19	18 1	elrab2	|- ( 0 e. Z <-> ( 0 e. ZZ /\ 0 <_ 1 ) )
20	13 14 19	mpbir2an	|- 0 e. Z
21		1z	|- 1 e. ZZ
22		fveq2	|- ( x = 1 -> ( abs ` x ) = ( abs ` 1 ) )
23	22 7	eqtrdi	|- ( x = 1 -> ( abs ` x ) = 1 )
24	23	breq1d	|- ( x = 1 -> ( ( abs ` x ) <_ 1 <-> 1 <_ 1 ) )
25	24 1	elrab2	|- ( 1 e. Z <-> ( 1 e. ZZ /\ 1 <_ 1 ) )
26	21 3 25	mpbir2an	|- 1 e. Z
27	12 20 26	3pm3.2i	|- ( -u 1 e. Z /\ 0 e. Z /\ 1 e. Z )