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 ⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
evpmss.p ⊢ 𝑃 = ( Base ‘ 𝑆 )
psgnevpmb.n ⊢ 𝑁 = ( pmSgn ‘ 𝐷 )
Assertion psgnodpmr ( ( 𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃 ∧ ( 𝑁 ‘ 𝐹 ) = - 1 ) → 𝐹 ∈ ( 𝑃 ∖ ( pmEven ‘ 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 evpmss.s ⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
2 evpmss.p ⊢ 𝑃 = ( Base ‘ 𝑆 )
3 psgnevpmb.n ⊢ 𝑁 = ( pmSgn ‘ 𝐷 )
4 simp2 ⊢ ( ( 𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃 ∧ ( 𝑁 ‘ 𝐹 ) = - 1 ) → 𝐹 ∈ 𝑃 )
5 1 2 3 psgnevpm ⊢ ( ( 𝐷 ∈ Fin ∧ 𝐹 ∈ ( pmEven ‘ 𝐷 ) ) → ( 𝑁 ‘ 𝐹 ) = 1 )
6 5 ex ⊢ ( 𝐷 ∈ Fin → ( 𝐹 ∈ ( pmEven ‘ 𝐷 ) → ( 𝑁 ‘ 𝐹 ) = 1 ) )
7 6 adantr ⊢ ( ( 𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃 ) → ( 𝐹 ∈ ( pmEven ‘ 𝐷 ) → ( 𝑁 ‘ 𝐹 ) = 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 ⊢ ( ( 𝑁 ‘ 𝐹 ) = 1 → ( ( 𝑁 ‘ 𝐹 ) ≠ - 1 ↔ 1 ≠ - 1 ) )
17 15 16 mpbiri ⊢ ( ( 𝑁 ‘ 𝐹 ) = 1 → ( 𝑁 ‘ 𝐹 ) ≠ - 1 )
18 7 17 syl6 ⊢ ( ( 𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃 ) → ( 𝐹 ∈ ( pmEven ‘ 𝐷 ) → ( 𝑁 ‘ 𝐹 ) ≠ - 1 ) )
19 18 necon2bd ⊢ ( ( 𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃 ) → ( ( 𝑁 ‘ 𝐹 ) = - 1 → ¬ 𝐹 ∈ ( pmEven ‘ 𝐷 ) ) )
20 19 3impia ⊢ ( ( 𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃 ∧ ( 𝑁 ‘ 𝐹 ) = - 1 ) → ¬ 𝐹 ∈ ( pmEven ‘ 𝐷 ) )
21 4 20 eldifd ⊢ ( ( 𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃 ∧ ( 𝑁 ‘ 𝐹 ) = - 1 ) → 𝐹 ∈ ( 𝑃 ∖ ( pmEven ‘ 𝐷 ) ) )