This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )