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 ∈ Fin ∧ F ∈ P ∧ N ⁡ F = − 1 → F ∈ 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 ∈ Fin ∧ F ∈ P ∧ N ⁡ F = − 1 → F ∈ P
5 1 2 3 psgnevpm ⊢ D ∈ Fin ∧ F ∈ pmEven ⁡ D → N ⁡ F = 1
6 5 ex ⊢ D ∈ Fin → F ∈ pmEven ⁡ D → N ⁡ F = 1
7 6 adantr ⊢ D ∈ Fin ∧ F ∈ P → F ∈ pmEven ⁡ D → N ⁡ F = 1
8 neg1rr ⊢ − 1 ∈ ℝ
9 neg1lt0 ⊢ − 1 < 0
10 0lt1 ⊢ 0 < 1
11 0re ⊢ 0 ∈ ℝ
12 1re ⊢ 1 ∈ ℝ
13 8 11 12 lttri ⊢ − 1 < 0 ∧ 0 < 1 → − 1 < 1
14 9 10 13 mp2an ⊢ − 1 < 1
15 8 14 gtneii ⊢ 1 ≠ − 1
16 neeq1 ⊢ N ⁡ F = 1 → N ⁡ F ≠ − 1 ↔ 1 ≠ − 1
17 15 16 mpbiri ⊢ N ⁡ F = 1 → N ⁡ F ≠ − 1
18 7 17 syl6 ⊢ D ∈ Fin ∧ F ∈ P → F ∈ pmEven ⁡ D → N ⁡ F ≠ − 1
19 18 necon2bd ⊢ D ∈ Fin ∧ F ∈ P → N ⁡ F = − 1 → ¬ F ∈ pmEven ⁡ D
20 19 3impia ⊢ D ∈ Fin ∧ F ∈ P ∧ N ⁡ F = − 1 → ¬ F ∈ pmEven ⁡ D
21 4 20 eldifd ⊢ D ∈ Fin ∧ F ∈ P ∧ N ⁡ F = − 1 → F ∈ P ∖ pmEven ⁡ D