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 \in Fin \land F \in P \land N (F) = - 1) \to F \in (P ∖ pmEven (D))$

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 \in Fin \land F \in P \land N (F) = - 1) \to F \in P$
5	1 2 3	psgnevpm	$⊢ (D \in Fin \land F \in pmEven (D)) \to N (F) = 1$
6	5	ex	$⊢ D \in Fin \to (F \in pmEven (D) \to N (F) = 1)$
7	6	adantr	$⊢ (D \in Fin \land F \in P) \to (F \in pmEven (D) \to N (F) = 1)$
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	$⊢ (- 1 < 0 \land 0 < 1) \to - 1 < 1$
14	9 10 13	mp2an	$⊢ - 1 < 1$
15	8 14	gtneii	$⊢ 1 \neq - 1$
16		neeq1	$⊢ N (F) = 1 \to (N (F) \neq - 1 \leftrightarrow 1 \neq - 1)$
17	15 16	mpbiri	$⊢ N (F) = 1 \to N (F) \neq - 1$
18	7 17	syl6	$⊢ (D \in Fin \land F \in P) \to (F \in pmEven (D) \to N (F) \neq - 1)$
19	18	necon2bd	$⊢ (D \in Fin \land F \in P) \to (N (F) = - 1 \to \neg F \in pmEven (D))$
20	19	3impia	$⊢ (D \in Fin \land F \in P \land N (F) = - 1) \to \neg F \in pmEven (D)$
21	4 20	eldifd	$⊢ (D \in Fin \land F \in P \land N (F) = - 1) \to F \in (P ∖ pmEven (D))$

Metamath Proof Explorer