ballotlemfp1

Description: If the J th ballot is for A, ( FC ) goes up 1. If the J th ballot is for B, ( FC ) goes down 1. (Contributed by Thierry Arnoux, 24-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\|))$
	ballotlemfp1.c	$⊢ φ \to C \in O$
	ballotlemfp1.j	$⊢ φ \to J \in ℕ$
Assertion	ballotlemfp1	$⊢ φ \to ((\neg J \in C \to F (C) (J) = F (C) (J - 1) - 1) \land (J \in C \to F (C) (J) = F (C) (J - 1) + 1))$

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		ballotlemfp1.c	$⊢ φ \to C \in O$
7		ballotlemfp1.j	$⊢ φ \to J \in ℕ$
8	7	nnzd	$⊢ φ \to J \in ℤ$
9	1 2 3 4 5 6 8	ballotlemfval	$⊢ φ \to F (C) (J) = \|(1 \dots J) \cap C\| - \|(1 \dots J) ∖ C\|$
10	9	adantr	$⊢ (φ \land \neg J \in C) \to F (C) (J) = \|(1 \dots J) \cap C\| - \|(1 \dots J) ∖ C\|$
11		fzfi	$⊢ (1 \dots J - 1) \in Fin$
12		inss1	$⊢ (1 \dots J - 1) \cap C \subseteq (1 \dots J - 1)$
13		ssfi	$⊢ ((1 \dots J - 1) \in Fin \land (1 \dots J - 1) \cap C \subseteq (1 \dots J - 1)) \to (1 \dots J - 1) \cap C \in Fin$
14	11 12 13	mp2an	$⊢ (1 \dots J - 1) \cap C \in Fin$
15		hashcl	$⊢ (1 \dots J - 1) \cap C \in Fin \to \|(1 \dots J - 1) \cap C\| \in ℕ_{0}$
16	14 15	ax-mp	$⊢ \|(1 \dots J - 1) \cap C\| \in ℕ_{0}$
17	16	nn0cni	$⊢ \|(1 \dots J - 1) \cap C\| \in ℂ$
18	17	a1i	$⊢ (φ \land \neg J \in C) \to \|(1 \dots J - 1) \cap C\| \in ℂ$
19		diffi	$⊢ (1 \dots J - 1) \in Fin \to (1 \dots J - 1) ∖ C \in Fin$
20	11 19	ax-mp	$⊢ (1 \dots J - 1) ∖ C \in Fin$
21		hashcl	$⊢ (1 \dots J - 1) ∖ C \in Fin \to \|(1 \dots J - 1) ∖ C\| \in ℕ_{0}$
22	20 21	ax-mp	$⊢ \|(1 \dots J - 1) ∖ C\| \in ℕ_{0}$
23	22	nn0cni	$⊢ \|(1 \dots J - 1) ∖ C\| \in ℂ$
24	23	a1i	$⊢ (φ \land \neg J \in C) \to \|(1 \dots J - 1) ∖ C\| \in ℂ$
25		1cnd	$⊢ (φ \land \neg J \in C) \to 1 \in ℂ$
26	18 24 25	subsub4d	$⊢ (φ \land \neg J \in C) \to \|(1 \dots J - 1) \cap C\| - \|(1 \dots J - 1) ∖ C\| - 1 = \|(1 \dots J - 1) \cap C\| - (\|(1 \dots J - 1) ∖ C\| + 1)$
27		1zzd	$⊢ φ \to 1 \in ℤ$
28	8 27	zsubcld	$⊢ φ \to J - 1 \in ℤ$
29	1 2 3 4 5 6 28	ballotlemfval	$⊢ φ \to F (C) (J - 1) = \|(1 \dots J - 1) \cap C\| - \|(1 \dots J - 1) ∖ C\|$
30	29	adantr	$⊢ (φ \land \neg J \in C) \to F (C) (J - 1) = \|(1 \dots J - 1) \cap C\| - \|(1 \dots J - 1) ∖ C\|$
31	30	oveq1d	$⊢ (φ \land \neg J \in C) \to F (C) (J - 1) - 1 = \|(1 \dots J - 1) \cap C\| - \|(1 \dots J - 1) ∖ C\| - 1$
32		elnnuz	$⊢ J \in ℕ \leftrightarrow J \in ℤ_{\geq 1}$
33	7 32	sylib	$⊢ φ \to J \in ℤ_{\geq 1}$
34		fzspl	$⊢ J \in ℤ_{\geq 1} \to (1 \dots J) = (1 \dots J - 1) \cup \{J\}$
35	34	ineq1d	$⊢ J \in ℤ_{\geq 1} \to (1 \dots J) \cap C = ((1 \dots J - 1) \cup \{J\}) \cap C$
36		indir	$⊢ ((1 \dots J - 1) \cup \{J\}) \cap C = ((1 \dots J - 1) \cap C) \cup (\{J\} \cap C)$
37	35 36	syl6eq	$⊢ J \in ℤ_{\geq 1} \to (1 \dots J) \cap C = ((1 \dots J - 1) \cap C) \cup (\{J\} \cap C)$
38	33 37	syl	$⊢ φ \to (1 \dots J) \cap C = ((1 \dots J - 1) \cap C) \cup (\{J\} \cap C)$
39	38	adantr	$⊢ (φ \land \neg J \in C) \to (1 \dots J) \cap C = ((1 \dots J - 1) \cap C) \cup (\{J\} \cap C)$
40		disjsn	$⊢ C \cap \{J\} = \emptyset \leftrightarrow \neg J \in C$
41		incom	$⊢ C \cap \{J\} = \{J\} \cap C$
42	41	eqeq1i	$⊢ C \cap \{J\} = \emptyset \leftrightarrow \{J\} \cap C = \emptyset$
43	40 42	sylbb1	$⊢ \neg J \in C \to \{J\} \cap C = \emptyset$
44	43	adantl	$⊢ (φ \land \neg J \in C) \to \{J\} \cap C = \emptyset$
45	44	uneq2d	$⊢ (φ \land \neg J \in C) \to ((1 \dots J - 1) \cap C) \cup (\{J\} \cap C) = ((1 \dots J - 1) \cap C) \cup \emptyset$
46		un0	$⊢ ((1 \dots J - 1) \cap C) \cup \emptyset = (1 \dots J - 1) \cap C$
47	45 46	syl6eq	$⊢ (φ \land \neg J \in C) \to ((1 \dots J - 1) \cap C) \cup (\{J\} \cap C) = (1 \dots J - 1) \cap C$
48	39 47	eqtrd	$⊢ (φ \land \neg J \in C) \to (1 \dots J) \cap C = (1 \dots J - 1) \cap C$
49	48	fveq2d	$⊢ (φ \land \neg J \in C) \to \|(1 \dots J) \cap C\| = \|(1 \dots J - 1) \cap C\|$
50	34	difeq1d	$⊢ J \in ℤ_{\geq 1} \to (1 \dots J) ∖ C = ((1 \dots J - 1) \cup \{J\}) ∖ C$
51		difundir	$⊢ ((1 \dots J - 1) \cup \{J\}) ∖ C = ((1 \dots J - 1) ∖ C) \cup (\{J\} ∖ C)$
52	50 51	syl6eq	$⊢ J \in ℤ_{\geq 1} \to (1 \dots J) ∖ C = ((1 \dots J - 1) ∖ C) \cup (\{J\} ∖ C)$
53	33 52	syl	$⊢ φ \to (1 \dots J) ∖ C = ((1 \dots J - 1) ∖ C) \cup (\{J\} ∖ C)$
54		disj3	$⊢ \{J\} \cap C = \emptyset \leftrightarrow \{J\} = \{J\} ∖ C$
55	43 54	sylib	$⊢ \neg J \in C \to \{J\} = \{J\} ∖ C$
56	55	eqcomd	$⊢ \neg J \in C \to \{J\} ∖ C = \{J\}$
57	56	uneq2d	$⊢ \neg J \in C \to ((1 \dots J - 1) ∖ C) \cup (\{J\} ∖ C) = ((1 \dots J - 1) ∖ C) \cup \{J\}$
58	53 57	sylan9eq	$⊢ (φ \land \neg J \in C) \to (1 \dots J) ∖ C = ((1 \dots J - 1) ∖ C) \cup \{J\}$
59	58	fveq2d	$⊢ (φ \land \neg J \in C) \to \|(1 \dots J) ∖ C\| = \|((1 \dots J - 1) ∖ C) \cup \{J\}\|$
60	8	adantr	$⊢ (φ \land \neg J \in C) \to J \in ℤ$
61		uzid	$⊢ J \in ℤ \to J \in ℤ_{\geq J}$
62		uznfz	$⊢ J \in ℤ_{\geq J} \to \neg J \in (1 \dots J - 1)$
63	8 61 62	3syl	$⊢ φ \to \neg J \in (1 \dots J - 1)$
64	63	adantr	$⊢ (φ \land \neg J \in C) \to \neg J \in (1 \dots J - 1)$
65		difss	$⊢ (1 \dots J - 1) ∖ C \subseteq (1 \dots J - 1)$
66	65	sseli	$⊢ J \in ((1 \dots J - 1) ∖ C) \to J \in (1 \dots J - 1)$
67	64 66	nsyl	$⊢ (φ \land \neg J \in C) \to \neg J \in ((1 \dots J - 1) ∖ C)$
68		ssfi	$⊢ ((1 \dots J - 1) \in Fin \land (1 \dots J - 1) ∖ C \subseteq (1 \dots J - 1)) \to (1 \dots J - 1) ∖ C \in Fin$
69	11 65 68	mp2an	$⊢ (1 \dots J - 1) ∖ C \in Fin$
70	67 69	jctil	$⊢ (φ \land \neg J \in C) \to ((1 \dots J - 1) ∖ C \in Fin \land \neg J \in ((1 \dots J - 1) ∖ C))$
71		hashunsng	$⊢ J \in ℤ \to (((1 \dots J - 1) ∖ C \in Fin \land \neg J \in ((1 \dots J - 1) ∖ C)) \to \|((1 \dots J - 1) ∖ C) \cup \{J\}\| = \|(1 \dots J - 1) ∖ C\| + 1)$
72	60 70 71	sylc	$⊢ (φ \land \neg J \in C) \to \|((1 \dots J - 1) ∖ C) \cup \{J\}\| = \|(1 \dots J - 1) ∖ C\| + 1$
73	59 72	eqtrd	$⊢ (φ \land \neg J \in C) \to \|(1 \dots J) ∖ C\| = \|(1 \dots J - 1) ∖ C\| + 1$
74	49 73	oveq12d	$⊢ (φ \land \neg J \in C) \to \|(1 \dots J) \cap C\| - \|(1 \dots J) ∖ C\| = \|(1 \dots J - 1) \cap C\| - (\|(1 \dots J - 1) ∖ C\| + 1)$
75	26 31 74	3eqtr4rd	$⊢ (φ \land \neg J \in C) \to \|(1 \dots J) \cap C\| - \|(1 \dots J) ∖ C\| = F (C) (J - 1) - 1$
76	10 75	eqtrd	$⊢ (φ \land \neg J \in C) \to F (C) (J) = F (C) (J - 1) - 1$
77	76	ex	$⊢ φ \to (\neg J \in C \to F (C) (J) = F (C) (J - 1) - 1)$
78	9	adantr	$⊢ (φ \land J \in C) \to F (C) (J) = \|(1 \dots J) \cap C\| - \|(1 \dots J) ∖ C\|$
79	17	a1i	$⊢ (φ \land J \in C) \to \|(1 \dots J - 1) \cap C\| \in ℂ$
80		1cnd	$⊢ (φ \land J \in C) \to 1 \in ℂ$
81	23	a1i	$⊢ (φ \land J \in C) \to \|(1 \dots J - 1) ∖ C\| \in ℂ$
82	79 80 81	addsubd	$⊢ (φ \land J \in C) \to \|(1 \dots J - 1) \cap C\| + 1 - \|(1 \dots J - 1) ∖ C\| = \|(1 \dots J - 1) \cap C\| - \|(1 \dots J - 1) ∖ C\| + 1$
83	38	fveq2d	$⊢ φ \to \|(1 \dots J) \cap C\| = \|((1 \dots J - 1) \cap C) \cup (\{J\} \cap C)\|$
84	83	adantr	$⊢ (φ \land J \in C) \to \|(1 \dots J) \cap C\| = \|((1 \dots J - 1) \cap C) \cup (\{J\} \cap C)\|$
85		snssi	$⊢ J \in C \to \{J\} \subseteq C$
86		df-ss	$⊢ \{J\} \subseteq C \leftrightarrow \{J\} \cap C = \{J\}$
87	85 86	sylib	$⊢ J \in C \to \{J\} \cap C = \{J\}$
88	87	uneq2d	$⊢ J \in C \to ((1 \dots J - 1) \cap C) \cup (\{J\} \cap C) = ((1 \dots J - 1) \cap C) \cup \{J\}$
89	88	fveq2d	$⊢ J \in C \to \|((1 \dots J - 1) \cap C) \cup (\{J\} \cap C)\| = \|((1 \dots J - 1) \cap C) \cup \{J\}\|$
90	89	adantl	$⊢ (φ \land J \in C) \to \|((1 \dots J - 1) \cap C) \cup (\{J\} \cap C)\| = \|((1 \dots J - 1) \cap C) \cup \{J\}\|$
91		simpr	$⊢ (φ \land J \in C) \to J \in C$
92	8	adantr	$⊢ (φ \land J \in C) \to J \in ℤ$
93	92 61 62	3syl	$⊢ (φ \land J \in C) \to \neg J \in (1 \dots J - 1)$
94	12	sseli	$⊢ J \in ((1 \dots J - 1) \cap C) \to J \in (1 \dots J - 1)$
95	93 94	nsyl	$⊢ (φ \land J \in C) \to \neg J \in ((1 \dots J - 1) \cap C)$
96	95 14	jctil	$⊢ (φ \land J \in C) \to ((1 \dots J - 1) \cap C \in Fin \land \neg J \in ((1 \dots J - 1) \cap C))$
97		hashunsng	$⊢ J \in C \to (((1 \dots J - 1) \cap C \in Fin \land \neg J \in ((1 \dots J - 1) \cap C)) \to \|((1 \dots J - 1) \cap C) \cup \{J\}\| = \|(1 \dots J - 1) \cap C\| + 1)$
98	91 96 97	sylc	$⊢ (φ \land J \in C) \to \|((1 \dots J - 1) \cap C) \cup \{J\}\| = \|(1 \dots J - 1) \cap C\| + 1$
99	84 90 98	3eqtrd	$⊢ (φ \land J \in C) \to \|(1 \dots J) \cap C\| = \|(1 \dots J - 1) \cap C\| + 1$
100	53	fveq2d	$⊢ φ \to \|(1 \dots J) ∖ C\| = \|((1 \dots J - 1) ∖ C) \cup (\{J\} ∖ C)\|$
101	100	adantr	$⊢ (φ \land J \in C) \to \|(1 \dots J) ∖ C\| = \|((1 \dots J - 1) ∖ C) \cup (\{J\} ∖ C)\|$
102		difin2	$⊢ \{J\} \subseteq C \to \{J\} ∖ C = (C ∖ C) \cap \{J\}$
103		difid	$⊢ C ∖ C = \emptyset$
104	103	ineq1i	$⊢ (C ∖ C) \cap \{J\} = \emptyset \cap \{J\}$
105		0in	$⊢ \emptyset \cap \{J\} = \emptyset$
106	104 105	eqtri	$⊢ (C ∖ C) \cap \{J\} = \emptyset$
107	102 106	syl6eq	$⊢ \{J\} \subseteq C \to \{J\} ∖ C = \emptyset$
108	85 107	syl	$⊢ J \in C \to \{J\} ∖ C = \emptyset$
109	108	uneq2d	$⊢ J \in C \to ((1 \dots J - 1) ∖ C) \cup (\{J\} ∖ C) = ((1 \dots J - 1) ∖ C) \cup \emptyset$
110	109	fveq2d	$⊢ J \in C \to \|((1 \dots J - 1) ∖ C) \cup (\{J\} ∖ C)\| = \|((1 \dots J - 1) ∖ C) \cup \emptyset\|$
111	110	adantl	$⊢ (φ \land J \in C) \to \|((1 \dots J - 1) ∖ C) \cup (\{J\} ∖ C)\| = \|((1 \dots J - 1) ∖ C) \cup \emptyset\|$
112		un0	$⊢ ((1 \dots J - 1) ∖ C) \cup \emptyset = (1 \dots J - 1) ∖ C$
113	112	a1i	$⊢ (φ \land J \in C) \to ((1 \dots J - 1) ∖ C) \cup \emptyset = (1 \dots J - 1) ∖ C$
114	113	fveq2d	$⊢ (φ \land J \in C) \to \|((1 \dots J - 1) ∖ C) \cup \emptyset\| = \|(1 \dots J - 1) ∖ C\|$
115	101 111 114	3eqtrd	$⊢ (φ \land J \in C) \to \|(1 \dots J) ∖ C\| = \|(1 \dots J - 1) ∖ C\|$
116	99 115	oveq12d	$⊢ (φ \land J \in C) \to \|(1 \dots J) \cap C\| - \|(1 \dots J) ∖ C\| = \|(1 \dots J - 1) \cap C\| + 1 - \|(1 \dots J - 1) ∖ C\|$
117	29	adantr	$⊢ (φ \land J \in C) \to F (C) (J - 1) = \|(1 \dots J - 1) \cap C\| - \|(1 \dots J - 1) ∖ C\|$
118	117	oveq1d	$⊢ (φ \land J \in C) \to F (C) (J - 1) + 1 = \|(1 \dots J - 1) \cap C\| - \|(1 \dots J - 1) ∖ C\| + 1$
119	82 116 118	3eqtr4d	$⊢ (φ \land J \in C) \to \|(1 \dots J) \cap C\| - \|(1 \dots J) ∖ C\| = F (C) (J - 1) + 1$
120	78 119	eqtrd	$⊢ (φ \land J \in C) \to F (C) (J) = F (C) (J - 1) + 1$
121	120	ex	$⊢ φ \to (J \in C \to F (C) (J) = F (C) (J - 1) + 1)$
122	77 121	jca	$⊢ φ \to ((\neg J \in C \to F (C) (J) = F (C) (J - 1) - 1) \land (J \in C \to F (C) (J) = F (C) (J - 1) + 1))$

Metamath Proof Explorer

Theorem ballotlemfp1

Proof