ballotlem4

Description: If the first pick is a vote for B, A is not ahead throughout the count. (Contributed by Thierry Arnoux, 25-Nov-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	ballotlem4	$⊢ C \in O \to (\neg 1 \in C \to \neg C \in E)$

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		nnaddcl	$⊢ (M \in ℕ \land N \in ℕ) \to M + N \in ℕ$
8	1 2 7	mp2an	$⊢ M + N \in ℕ$
9		elnnuz	$⊢ M + N \in ℕ \leftrightarrow M + N \in ℤ_{\geq 1}$
10	8 9	mpbi	$⊢ M + N \in ℤ_{\geq 1}$
11		eluzfz1	$⊢ M + N \in ℤ_{\geq 1} \to 1 \in (1 \dots M + N)$
12	10 11	ax-mp	$⊢ 1 \in (1 \dots M + N)$
13		0le1	$⊢ 0 \leq 1$
14		0re	$⊢ 0 \in ℝ$
15		1re	$⊢ 1 \in ℝ$
16	14 15	lenlti	$⊢ 0 \leq 1 \leftrightarrow \neg 1 < 0$
17	13 16	mpbi	$⊢ \neg 1 < 0$
18		ltsub13	$⊢ (0 \in ℝ \land 0 \in ℝ \land 1 \in ℝ) \to (0 < 0 - 1 \leftrightarrow 1 < 0 - 0)$
19	14 14 15 18	mp3an	$⊢ 0 < 0 - 1 \leftrightarrow 1 < 0 - 0$
20		0m0e0	$⊢ 0 - 0 = 0$
21	20	breq2i	$⊢ 1 < 0 - 0 \leftrightarrow 1 < 0$
22	19 21	bitri	$⊢ 0 < 0 - 1 \leftrightarrow 1 < 0$
23	17 22	mtbir	$⊢ \neg 0 < 0 - 1$
24		1m1e0	$⊢ 1 - 1 = 0$
25	24	fveq2i	$⊢ F (C) (1 - 1) = F (C) (0)$
26	1 2 3 4 5	ballotlemfval0	$⊢ C \in O \to F (C) (0) = 0$
27	25 26	eqtrid	$⊢ C \in O \to F (C) (1 - 1) = 0$
28	27	oveq1d	$⊢ C \in O \to F (C) (1 - 1) - 1 = 0 - 1$
29	28	breq2d	$⊢ C \in O \to (0 < F (C) (1 - 1) - 1 \leftrightarrow 0 < 0 - 1)$
30	23 29	mtbiri	$⊢ C \in O \to \neg 0 < F (C) (1 - 1) - 1$
31	30	adantr	$⊢ (C \in O \land \neg 1 \in C) \to \neg 0 < F (C) (1 - 1) - 1$
32		simpl	$⊢ (C \in O \land 1 \in (1 \dots M + N)) \to C \in O$
33		1nn	$⊢ 1 \in ℕ$
34	33	a1i	$⊢ (C \in O \land 1 \in (1 \dots M + N)) \to 1 \in ℕ$
35	1 2 3 4 5 32 34	ballotlemfp1	$⊢ (C \in O \land 1 \in (1 \dots M + N)) \to ((\neg 1 \in C \to F (C) (1) = F (C) (1 - 1) - 1) \land (1 \in C \to F (C) (1) = F (C) (1 - 1) + 1))$
36	35	simpld	$⊢ (C \in O \land 1 \in (1 \dots M + N)) \to (\neg 1 \in C \to F (C) (1) = F (C) (1 - 1) - 1)$
37	12 36	mpan2	$⊢ C \in O \to (\neg 1 \in C \to F (C) (1) = F (C) (1 - 1) - 1)$
38	37	imp	$⊢ (C \in O \land \neg 1 \in C) \to F (C) (1) = F (C) (1 - 1) - 1$
39	38	breq2d	$⊢ (C \in O \land \neg 1 \in C) \to (0 < F (C) (1) \leftrightarrow 0 < F (C) (1 - 1) - 1)$
40	31 39	mtbird	$⊢ (C \in O \land \neg 1 \in C) \to \neg 0 < F (C) (1)$
41		fveq2	$⊢ i = 1 \to F (C) (i) = F (C) (1)$
42	41	breq2d	$⊢ i = 1 \to (0 < F (C) (i) \leftrightarrow 0 < F (C) (1))$
43	42	notbid	$⊢ i = 1 \to (\neg 0 < F (C) (i) \leftrightarrow \neg 0 < F (C) (1))$
44	43	rspcev	$⊢ (1 \in (1 \dots M + N) \land \neg 0 < F (C) (1)) \to \exists i \in (1 \dots M + N) \neg 0 < F (C) (i)$
45	12 40 44	sylancr	$⊢ (C \in O \land \neg 1 \in C) \to \exists i \in (1 \dots M + N) \neg 0 < F (C) (i)$
46		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)$
47	45 46	sylib	$⊢ (C \in O \land \neg 1 \in C) \to \neg \forall i \in (1 \dots M + N) 0 < F (C) (i)$
48	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))$
49	48	simprbi	$⊢ C \in E \to \forall i \in (1 \dots M + N) 0 < F (C) (i)$
50	47 49	nsyl	$⊢ (C \in O \land \neg 1 \in C) \to \neg C \in E$
51	50	ex	$⊢ C \in O \to (\neg 1 \in C \to \neg C \in E)$

Metamath Proof Explorer

Theorem ballotlem4

Proof