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}=\mathrm{SymGrp}\left({D}\right)$
evpmss.p ${⊢}{P}={\mathrm{Base}}_{{S}}$
psgnevpmb.n ${⊢}{N}=\mathrm{pmSgn}\left({D}\right)$
Assertion psgnodpmr ${⊢}\left({D}\in \mathrm{Fin}\wedge {F}\in {P}\wedge {N}\left({F}\right)=-1\right)\to {F}\in \left({P}\setminus \mathrm{pmEven}\left({D}\right)\right)$

Proof

Step Hyp Ref Expression
1 evpmss.s ${⊢}{S}=\mathrm{SymGrp}\left({D}\right)$
2 evpmss.p ${⊢}{P}={\mathrm{Base}}_{{S}}$
3 psgnevpmb.n ${⊢}{N}=\mathrm{pmSgn}\left({D}\right)$
4 simp2 ${⊢}\left({D}\in \mathrm{Fin}\wedge {F}\in {P}\wedge {N}\left({F}\right)=-1\right)\to {F}\in {P}$
5 1 2 3 psgnevpm ${⊢}\left({D}\in \mathrm{Fin}\wedge {F}\in \mathrm{pmEven}\left({D}\right)\right)\to {N}\left({F}\right)=1$
6 5 ex ${⊢}{D}\in \mathrm{Fin}\to \left({F}\in \mathrm{pmEven}\left({D}\right)\to {N}\left({F}\right)=1\right)$
7 6 adantr ${⊢}\left({D}\in \mathrm{Fin}\wedge {F}\in {P}\right)\to \left({F}\in \mathrm{pmEven}\left({D}\right)\to {N}\left({F}\right)=1\right)$
8 neg1rr ${⊢}-1\in ℝ$
9 neg1lt0 ${⊢}-1<0$
10 0lt1 ${⊢}0<1$
11 0re ${⊢}0\in ℝ$
12 1re ${⊢}1\in ℝ$
13 8 11 12 lttri ${⊢}\left(-1<0\wedge 0<1\right)\to -1<1$
14 9 10 13 mp2an ${⊢}-1<1$
15 8 14 gtneii ${⊢}1\ne -1$
16 neeq1 ${⊢}{N}\left({F}\right)=1\to \left({N}\left({F}\right)\ne -1↔1\ne -1\right)$
17 15 16 mpbiri ${⊢}{N}\left({F}\right)=1\to {N}\left({F}\right)\ne -1$
18 7 17 syl6 ${⊢}\left({D}\in \mathrm{Fin}\wedge {F}\in {P}\right)\to \left({F}\in \mathrm{pmEven}\left({D}\right)\to {N}\left({F}\right)\ne -1\right)$
19 18 necon2bd ${⊢}\left({D}\in \mathrm{Fin}\wedge {F}\in {P}\right)\to \left({N}\left({F}\right)=-1\to ¬{F}\in \mathrm{pmEven}\left({D}\right)\right)$
20 19 3impia ${⊢}\left({D}\in \mathrm{Fin}\wedge {F}\in {P}\wedge {N}\left({F}\right)=-1\right)\to ¬{F}\in \mathrm{pmEven}\left({D}\right)$
21 4 20 eldifd ${⊢}\left({D}\in \mathrm{Fin}\wedge {F}\in {P}\wedge {N}\left({F}\right)=-1\right)\to {F}\in \left({P}\setminus \mathrm{pmEven}\left({D}\right)\right)$