ballotlemodife

Description: Elements of ( O \ E ) . (Contributed by Thierry Arnoux, 7-Dec-2016)

	Ref	Expression
Hypotheses	ballotth.m	$⊢ M \in ℕ$
	ballotth.n	$⊢ N \in ℕ$
	ballotth.o	$⊢ O = \{c \in 𝒫 (1 \dots M + N) \| \|c\| = M\}$
	ballotth.p	$⊢ P = (x \in 𝒫 O ⟼ \frac{\|x\|}{\|O\|})$
	ballotth.f	$⊢ F = (c \in O ⟼ (i \in ℤ ⟼ \|(1 \dots i) \cap c\| - \|(1 \dots i) ∖ c\|))$
	ballotth.e	$⊢ E = \{c \in O \| \forall i \in (1 \dots M + N) 0 < F (c) (i)\}$
Assertion	ballotlemodife	$⊢ C \in (O ∖ E) \leftrightarrow (C \in O \land \exists i \in (1 \dots M + N) F (C) (i) \leq 0)$

Proof

Step	Hyp	Ref	Expression
1		ballotth.m	$⊢ M \in ℕ$
2		ballotth.n	$⊢ N \in ℕ$
3		ballotth.o	$⊢ O = \{c \in 𝒫 (1 \dots M + N) \| \|c\| = M\}$
4		ballotth.p	$⊢ P = (x \in 𝒫 O ⟼ \frac{\|x\|}{\|O\|})$
5		ballotth.f	$⊢ F = (c \in O ⟼ (i \in ℤ ⟼ \|(1 \dots i) \cap c\| - \|(1 \dots i) ∖ c\|))$
6		ballotth.e	$⊢ E = \{c \in O \| \forall i \in (1 \dots M + N) 0 < F (c) (i)\}$
7		eldif	$⊢ C \in (O ∖ E) \leftrightarrow (C \in O \land \neg C \in E)$
8		df-or	$⊢ ((C \in O \land \neg C \in O) \lor (C \in O \land \neg \forall i \in (1 \dots M + N) 0 < F (C) (i))) \leftrightarrow (\neg (C \in O \land \neg C \in O) \to (C \in O \land \neg \forall i \in (1 \dots M + N) 0 < F (C) (i)))$
9		pm3.24	$⊢ \neg (C \in O \land \neg C \in O)$
10	9	a1bi	$⊢ (C \in O \land \neg \forall i \in (1 \dots M + N) 0 < F (C) (i)) \leftrightarrow (\neg (C \in O \land \neg C \in O) \to (C \in O \land \neg \forall i \in (1 \dots M + N) 0 < F (C) (i)))$
11	8 10	bitr4i	$⊢ ((C \in O \land \neg C \in O) \lor (C \in O \land \neg \forall i \in (1 \dots M + N) 0 < F (C) (i))) \leftrightarrow (C \in O \land \neg \forall i \in (1 \dots M + N) 0 < F (C) (i))$
12	1 2 3 4 5 6	ballotleme	$⊢ C \in E \leftrightarrow (C \in O \land \forall i \in (1 \dots M + N) 0 < F (C) (i))$
13	12	notbii	$⊢ \neg C \in E \leftrightarrow \neg (C \in O \land \forall i \in (1 \dots M + N) 0 < F (C) (i))$
14	13	anbi2i	$⊢ (C \in O \land \neg C \in E) \leftrightarrow (C \in O \land \neg (C \in O \land \forall i \in (1 \dots M + N) 0 < F (C) (i)))$
15		ianor	$⊢ \neg (C \in O \land \forall i \in (1 \dots M + N) 0 < F (C) (i)) \leftrightarrow (\neg C \in O \lor \neg \forall i \in (1 \dots M + N) 0 < F (C) (i))$
16	15	anbi2i	$⊢ (C \in O \land \neg (C \in O \land \forall i \in (1 \dots M + N) 0 < F (C) (i))) \leftrightarrow (C \in O \land (\neg C \in O \lor \neg \forall i \in (1 \dots M + N) 0 < F (C) (i)))$
17		andi	$⊢ (C \in O \land (\neg C \in O \lor \neg \forall i \in (1 \dots M + N) 0 < F (C) (i))) \leftrightarrow ((C \in O \land \neg C \in O) \lor (C \in O \land \neg \forall i \in (1 \dots M + N) 0 < F (C) (i)))$
18	14 16 17	3bitri	$⊢ (C \in O \land \neg C \in E) \leftrightarrow ((C \in O \land \neg C \in O) \lor (C \in O \land \neg \forall i \in (1 \dots M + N) 0 < F (C) (i)))$
19		fz1ssfz0	$⊢ (1 \dots M + N) \subseteq (0 \dots M + N)$
20	19	a1i	$⊢ C \in O \to (1 \dots M + N) \subseteq (0 \dots M + N)$
21	20	sseld	$⊢ C \in O \to (i \in (1 \dots M + N) \to i \in (0 \dots M + N))$
22	21	imdistani	$⊢ (C \in O \land i \in (1 \dots M + N)) \to (C \in O \land i \in (0 \dots M + N))$
23		simpl	$⊢ (C \in O \land j \in (0 \dots M + N)) \to C \in O$
24		elfzelz	$⊢ j \in (0 \dots M + N) \to j \in ℤ$
25	24	adantl	$⊢ (C \in O \land j \in (0 \dots M + N)) \to j \in ℤ$
26	1 2 3 4 5 23 25	ballotlemfelz	$⊢ (C \in O \land j \in (0 \dots M + N)) \to F (C) (j) \in ℤ$
27	26	zred	$⊢ (C \in O \land j \in (0 \dots M + N)) \to F (C) (j) \in ℝ$
28	27	sbimi	$⊢ [i/ j] (C \in O \land j \in (0 \dots M + N)) \to [i/ j] F (C) (j) \in ℝ$
29		sban	$⊢ [i/ j] (C \in O \land j \in (0 \dots M + N)) \leftrightarrow ([i/ j] C \in O \land [i/ j] j \in (0 \dots M + N))$
30		sbv	$⊢ [i/ j] C \in O \leftrightarrow C \in O$
31		clelsb1	$⊢ [i/ j] j \in (0 \dots M + N) \leftrightarrow i \in (0 \dots M + N)$
32	30 31	anbi12i	$⊢ ([i/ j] C \in O \land [i/ j] j \in (0 \dots M + N)) \leftrightarrow (C \in O \land i \in (0 \dots M + N))$
33	29 32	bitri	$⊢ [i/ j] (C \in O \land j \in (0 \dots M + N)) \leftrightarrow (C \in O \land i \in (0 \dots M + N))$
34		nfv	$⊢ Ⅎ j F (C) (i) \in ℝ$
35		fveq2	$⊢ j = i \to F (C) (j) = F (C) (i)$
36	35	eleq1d	$⊢ j = i \to (F (C) (j) \in ℝ \leftrightarrow F (C) (i) \in ℝ)$
37	34 36	sbiev	$⊢ [i/ j] F (C) (j) \in ℝ \leftrightarrow F (C) (i) \in ℝ$
38	28 33 37	3imtr3i	$⊢ (C \in O \land i \in (0 \dots M + N)) \to F (C) (i) \in ℝ$
39	22 38	syl	$⊢ (C \in O \land i \in (1 \dots M + N)) \to F (C) (i) \in ℝ$
40		0red	$⊢ (C \in O \land i \in (1 \dots M + N)) \to 0 \in ℝ$
41	39 40	lenltd	$⊢ (C \in O \land i \in (1 \dots M + N)) \to (F (C) (i) \leq 0 \leftrightarrow \neg 0 < F (C) (i))$
42	41	rexbidva	$⊢ C \in O \to (\exists i \in (1 \dots M + N) F (C) (i) \leq 0 \leftrightarrow \exists i \in (1 \dots M + N) \neg 0 < F (C) (i))$
43		rexnal	$⊢ \exists i \in (1 \dots M + N) \neg 0 < F (C) (i) \leftrightarrow \neg \forall i \in (1 \dots M + N) 0 < F (C) (i)$
44	42 43	bitrdi	$⊢ C \in O \to (\exists i \in (1 \dots M + N) F (C) (i) \leq 0 \leftrightarrow \neg \forall i \in (1 \dots M + N) 0 < F (C) (i))$
45	44	pm5.32i	$⊢ (C \in O \land \exists i \in (1 \dots M + N) F (C) (i) \leq 0) \leftrightarrow (C \in O \land \neg \forall i \in (1 \dots M + N) 0 < F (C) (i))$
46	11 18 45	3bitr4i	$⊢ (C \in O \land \neg C \in E) \leftrightarrow (C \in O \land \exists i \in (1 \dots M + N) F (C) (i) \leq 0)$
47	7 46	bitri	$⊢ C \in (O ∖ E) \leftrightarrow (C \in O \land \exists i \in (1 \dots M + N) F (C) (i) \leq 0)$

Metamath Proof Explorer

Theorem ballotlemodife

Proof