Theorem psgnodpmr

Description: If a permutation has sign -1 it is odd (not even). (Contributed by SO, 9-Jul-2018)

	Ref	Expression
Hypotheses	evpmss.s	|- S = ( SymGrp ` D )
	evpmss.p	|- P = ( Base ` S )
	psgnevpmb.n	|- N = ( pmSgn ` D )
Assertion	psgnodpmr	|- ( ( D e. Fin /\ F e. P /\ ( N ` F ) = -u 1 ) -> F e. ( P \ ( pmEven ` D ) ) )

Proof

Step	Hyp	Ref	Expression
1		evpmss.s	|- S = ( SymGrp ` D )
2		evpmss.p	|- P = ( Base ` S )
3		psgnevpmb.n	|- N = ( pmSgn ` D )
4		simp2	|- ( ( D e. Fin /\ F e. P /\ ( N ` F ) = -u 1 ) -> F e. P )
5	1 2 3	psgnevpm	|- ( ( D e. Fin /\ F e. ( pmEven ` D ) ) -> ( N ` F ) = 1 )
6	5	ex	|- ( D e. Fin -> ( F e. ( pmEven ` D ) -> ( N ` F ) = 1 ) )
7	6	adantr	|- ( ( D e. Fin /\ F e. P ) -> ( F e. ( pmEven ` D ) -> ( N ` F ) = 1 ) )
8		neg1rr	|- -u 1 e. RR
9		neg1lt0	|- -u 1 < 0
10		0lt1	|- 0 < 1
11		0re	|- 0 e. RR
12		1re	|- 1 e. RR
13	8 11 12	lttri	|- ( ( -u 1 < 0 /\ 0 < 1 ) -> -u 1 < 1 )
14	9 10 13	mp2an	|- -u 1 < 1
15	8 14	gtneii	|- 1 =/= -u 1
16		neeq1	|- ( ( N ` F ) = 1 -> ( ( N ` F ) =/= -u 1 <-> 1 =/= -u 1 ) )
17	15 16	mpbiri	|- ( ( N ` F ) = 1 -> ( N ` F ) =/= -u 1 )
18	7 17	syl6	|- ( ( D e. Fin /\ F e. P ) -> ( F e. ( pmEven ` D ) -> ( N ` F ) =/= -u 1 ) )
19	18	necon2bd	|- ( ( D e. Fin /\ F e. P ) -> ( ( N ` F ) = -u 1 -> -. F e. ( pmEven ` D ) ) )
20	19	3impia	|- ( ( D e. Fin /\ F e. P /\ ( N ` F ) = -u 1 ) -> -. F e. ( pmEven ` D ) )
21	4 20	eldifd	|- ( ( D e. Fin /\ F e. P /\ ( N ` F ) = -u 1 ) -> F e. ( P \ ( pmEven ` D ) ) )