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