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	⊢ 𝑀 ∈ ℕ
	ballotth.n	⊢ 𝑁 ∈ ℕ
	ballotth.o	⊢ 𝑂 = { 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ♯ ‘ 𝑐 ) = 𝑀 }
	ballotth.p	⊢ 𝑃 = ( 𝑥 ∈ 𝒫 𝑂 ↦ ( ( ♯ ‘ 𝑥 ) / ( ♯ ‘ 𝑂 ) ) )
	ballotth.f	⊢ 𝐹 = ( 𝑐 ∈ 𝑂 ↦ ( 𝑖 ∈ ℤ ↦ ( ( ♯ ‘ ( ( 1 ... 𝑖 ) ∩ 𝑐 ) ) − ( ♯ ‘ ( ( 1 ... 𝑖 ) ∖ 𝑐 ) ) ) ) )
	ballotlemfp1.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑂 )
	ballotlemfp1.j	⊢ ( 𝜑 → 𝐽 ∈ ℕ )
Assertion	ballotlemfp1	⊢ ( 𝜑 → ( ( ¬ 𝐽 ∈ 𝐶 → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝐽 ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝐽 − 1 ) ) − 1 ) ) ∧ ( 𝐽 ∈ 𝐶 → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝐽 ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝐽 − 1 ) ) + 1 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ballotth.m	⊢ 𝑀 ∈ ℕ
2		ballotth.n	⊢ 𝑁 ∈ ℕ
3		ballotth.o	⊢ 𝑂 = { 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ♯ ‘ 𝑐 ) = 𝑀 }
4		ballotth.p	⊢ 𝑃 = ( 𝑥 ∈ 𝒫 𝑂 ↦ ( ( ♯ ‘ 𝑥 ) / ( ♯ ‘ 𝑂 ) ) )
5		ballotth.f	⊢ 𝐹 = ( 𝑐 ∈ 𝑂 ↦ ( 𝑖 ∈ ℤ ↦ ( ( ♯ ‘ ( ( 1 ... 𝑖 ) ∩ 𝑐 ) ) − ( ♯ ‘ ( ( 1 ... 𝑖 ) ∖ 𝑐 ) ) ) ) )
6		ballotlemfp1.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑂 )
7		ballotlemfp1.j	⊢ ( 𝜑 → 𝐽 ∈ ℕ )
8	7	nnzd	⊢ ( 𝜑 → 𝐽 ∈ ℤ )
9	1 2 3 4 5 6 8	ballotlemfval	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝐽 ) = ( ( ♯ ‘ ( ( 1 ... 𝐽 ) ∩ 𝐶 ) ) − ( ♯ ‘ ( ( 1 ... 𝐽 ) ∖ 𝐶 ) ) ) )
10	9	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐽 ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝐽 ) = ( ( ♯ ‘ ( ( 1 ... 𝐽 ) ∩ 𝐶 ) ) − ( ♯ ‘ ( ( 1 ... 𝐽 ) ∖ 𝐶 ) ) ) )
11		fzfi	⊢ ( 1 ... ( 𝐽 − 1 ) ) ∈ Fin
12		inss1	⊢ ( ( 1 ... ( 𝐽 − 1 ) ) ∩ 𝐶 ) ⊆ ( 1 ... ( 𝐽 − 1 ) )
13		ssfi	⊢ ( ( ( 1 ... ( 𝐽 − 1 ) ) ∈ Fin ∧ ( ( 1 ... ( 𝐽 − 1 ) ) ∩ 𝐶 ) ⊆ ( 1 ... ( 𝐽 − 1 ) ) ) → ( ( 1 ... ( 𝐽 − 1 ) ) ∩ 𝐶 ) ∈ Fin )
14	11 12 13	mp2an	⊢ ( ( 1 ... ( 𝐽 − 1 ) ) ∩ 𝐶 ) ∈ Fin
15		hashcl	⊢ ( ( ( 1 ... ( 𝐽 − 1 ) ) ∩ 𝐶 ) ∈ Fin → ( ♯ ‘ ( ( 1 ... ( 𝐽 − 1 ) ) ∩ 𝐶 ) ) ∈ ℕ₀ )
16	14 15	ax-mp	⊢ ( ♯ ‘ ( ( 1 ... ( 𝐽 − 1 ) ) ∩ 𝐶 ) ) ∈ ℕ₀
17	16	nn0cni	⊢ ( ♯ ‘ ( ( 1 ... ( 𝐽 − 1 ) ) ∩ 𝐶 ) ) ∈ ℂ
18	17	a1i	⊢ ( ( 𝜑 ∧ ¬ 𝐽 ∈ 𝐶 ) → ( ♯ ‘ ( ( 1 ... ( 𝐽 − 1 ) ) ∩ 𝐶 ) ) ∈ ℂ )
19		diffi	⊢ ( ( 1 ... ( 𝐽 − 1 ) ) ∈ Fin → ( ( 1 ... ( 𝐽 − 1 ) ) ∖ 𝐶 ) ∈ Fin )
20	11 19	ax-mp	⊢ ( ( 1 ... ( 𝐽 − 1 ) ) ∖ 𝐶 ) ∈ Fin
21		hashcl	⊢ ( ( ( 1 ... ( 𝐽 − 1 ) ) ∖ 𝐶 ) ∈ Fin → ( ♯ ‘ ( ( 1 ... ( 𝐽 − 1 ) ) ∖ 𝐶 ) ) ∈ ℕ₀ )
22	20 21	ax-mp	⊢ ( ♯ ‘ ( ( 1 ... ( 𝐽 − 1 ) ) ∖ 𝐶 ) ) ∈ ℕ₀
23	22	nn0cni	⊢ ( ♯ ‘ ( ( 1 ... ( 𝐽 − 1 ) ) ∖ 𝐶 ) ) ∈ ℂ
24	23	a1i	⊢ ( ( 𝜑 ∧ ¬ 𝐽 ∈ 𝐶 ) → ( ♯ ‘ ( ( 1 ... ( 𝐽 − 1 ) ) ∖ 𝐶 ) ) ∈ ℂ )
25		1cnd	⊢ ( ( 𝜑 ∧ ¬ 𝐽 ∈ 𝐶 ) → 1 ∈ ℂ )
26	18 24 25	subsub4d	⊢ ( ( 𝜑 ∧ ¬ 𝐽 ∈ 𝐶 ) → ( ( ( ♯ ‘ ( ( 1 ... ( 𝐽 − 1 ) ) ∩ 𝐶 ) ) − ( ♯ ‘ ( ( 1 ... ( 𝐽 − 1 ) ) ∖ 𝐶 ) ) ) − 1 ) = ( ( ♯ ‘ ( ( 1 ... ( 𝐽 − 1 ) ) ∩ 𝐶 ) ) − ( ( ♯ ‘ ( ( 1 ... ( 𝐽 − 1 ) ) ∖ 𝐶 ) ) + 1 ) ) )
27		1zzd	⊢ ( 𝜑 → 1 ∈ ℤ )
28	8 27	zsubcld	⊢ ( 𝜑 → ( 𝐽 − 1 ) ∈ ℤ )
29	1 2 3 4 5 6 28	ballotlemfval	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝐽 − 1 ) ) = ( ( ♯ ‘ ( ( 1 ... ( 𝐽 − 1 ) ) ∩ 𝐶 ) ) − ( ♯ ‘ ( ( 1 ... ( 𝐽 − 1 ) ) ∖ 𝐶 ) ) ) )
30	29	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐽 ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝐽 − 1 ) ) = ( ( ♯ ‘ ( ( 1 ... ( 𝐽 − 1 ) ) ∩ 𝐶 ) ) − ( ♯ ‘ ( ( 1 ... ( 𝐽 − 1 ) ) ∖ 𝐶 ) ) ) )
31	30	oveq1d	⊢ ( ( 𝜑 ∧ ¬ 𝐽 ∈ 𝐶 ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝐽 − 1 ) ) − 1 ) = ( ( ( ♯ ‘ ( ( 1 ... ( 𝐽 − 1 ) ) ∩ 𝐶 ) ) − ( ♯ ‘ ( ( 1 ... ( 𝐽 − 1 ) ) ∖ 𝐶 ) ) ) − 1 ) )
32		elnnuz	⊢ ( 𝐽 ∈ ℕ ↔ 𝐽 ∈ ( ℤ_≥ ‘ 1 ) )
33	7 32	sylib	⊢ ( 𝜑 → 𝐽 ∈ ( ℤ_≥ ‘ 1 ) )
34		fzspl	⊢ ( 𝐽 ∈ ( ℤ_≥ ‘ 1 ) → ( 1 ... 𝐽 ) = ( ( 1 ... ( 𝐽 − 1 ) ) ∪ { 𝐽 } ) )
35	34	ineq1d	⊢ ( 𝐽 ∈ ( ℤ_≥ ‘ 1 ) → ( ( 1 ... 𝐽 ) ∩ 𝐶 ) = ( ( ( 1 ... ( 𝐽 − 1 ) ) ∪ { 𝐽 } ) ∩ 𝐶 ) )
36		indir	⊢ ( ( ( 1 ... ( 𝐽 − 1 ) ) ∪ { 𝐽 } ) ∩ 𝐶 ) = ( ( ( 1 ... ( 𝐽 − 1 ) ) ∩ 𝐶 ) ∪ ( { 𝐽 } ∩ 𝐶 ) )
37	35 36	eqtrdi	⊢ ( 𝐽 ∈ ( ℤ_≥ ‘ 1 ) → ( ( 1 ... 𝐽 ) ∩ 𝐶 ) = ( ( ( 1 ... ( 𝐽 − 1 ) ) ∩ 𝐶 ) ∪ ( { 𝐽 } ∩ 𝐶 ) ) )
38	33 37	syl	⊢ ( 𝜑 → ( ( 1 ... 𝐽 ) ∩ 𝐶 ) = ( ( ( 1 ... ( 𝐽 − 1 ) ) ∩ 𝐶 ) ∪ ( { 𝐽 } ∩ 𝐶 ) ) )
39	38	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐽 ∈ 𝐶 ) → ( ( 1 ... 𝐽 ) ∩ 𝐶 ) = ( ( ( 1 ... ( 𝐽 − 1 ) ) ∩ 𝐶 ) ∪ ( { 𝐽 } ∩ 𝐶 ) ) )
40		disjsn	⊢ ( ( 𝐶 ∩ { 𝐽 } ) = ∅ ↔ ¬ 𝐽 ∈ 𝐶 )
41		incom	⊢ ( 𝐶 ∩ { 𝐽 } ) = ( { 𝐽 } ∩ 𝐶 )
42	41	eqeq1i	⊢ ( ( 𝐶 ∩ { 𝐽 } ) = ∅ ↔ ( { 𝐽 } ∩ 𝐶 ) = ∅ )
43	40 42	sylbb1	⊢ ( ¬ 𝐽 ∈ 𝐶 → ( { 𝐽 } ∩ 𝐶 ) = ∅ )
44	43	adantl	⊢ ( ( 𝜑 ∧ ¬ 𝐽 ∈ 𝐶 ) → ( { 𝐽 } ∩ 𝐶 ) = ∅ )
45	44	uneq2d	⊢ ( ( 𝜑 ∧ ¬ 𝐽 ∈ 𝐶 ) → ( ( ( 1 ... ( 𝐽 − 1 ) ) ∩ 𝐶 ) ∪ ( { 𝐽 } ∩ 𝐶 ) ) = ( ( ( 1 ... ( 𝐽 − 1 ) ) ∩ 𝐶 ) ∪ ∅ ) )
46		un0	⊢ ( ( ( 1 ... ( 𝐽 − 1 ) ) ∩ 𝐶 ) ∪ ∅ ) = ( ( 1 ... ( 𝐽 − 1 ) ) ∩ 𝐶 )
47	45 46	eqtrdi	⊢ ( ( 𝜑 ∧ ¬ 𝐽 ∈ 𝐶 ) → ( ( ( 1 ... ( 𝐽 − 1 ) ) ∩ 𝐶 ) ∪ ( { 𝐽 } ∩ 𝐶 ) ) = ( ( 1 ... ( 𝐽 − 1 ) ) ∩ 𝐶 ) )
48	39 47	eqtrd	⊢ ( ( 𝜑 ∧ ¬ 𝐽 ∈ 𝐶 ) → ( ( 1 ... 𝐽 ) ∩ 𝐶 ) = ( ( 1 ... ( 𝐽 − 1 ) ) ∩ 𝐶 ) )
49	48	fveq2d	⊢ ( ( 𝜑 ∧ ¬ 𝐽 ∈ 𝐶 ) → ( ♯ ‘ ( ( 1 ... 𝐽 ) ∩ 𝐶 ) ) = ( ♯ ‘ ( ( 1 ... ( 𝐽 − 1 ) ) ∩ 𝐶 ) ) )
50	34	difeq1d	⊢ ( 𝐽 ∈ ( ℤ_≥ ‘ 1 ) → ( ( 1 ... 𝐽 ) ∖ 𝐶 ) = ( ( ( 1 ... ( 𝐽 − 1 ) ) ∪ { 𝐽 } ) ∖ 𝐶 ) )
51		difundir	⊢ ( ( ( 1 ... ( 𝐽 − 1 ) ) ∪ { 𝐽 } ) ∖ 𝐶 ) = ( ( ( 1 ... ( 𝐽 − 1 ) ) ∖ 𝐶 ) ∪ ( { 𝐽 } ∖ 𝐶 ) )
52	50 51	eqtrdi	⊢ ( 𝐽 ∈ ( ℤ_≥ ‘ 1 ) → ( ( 1 ... 𝐽 ) ∖ 𝐶 ) = ( ( ( 1 ... ( 𝐽 − 1 ) ) ∖ 𝐶 ) ∪ ( { 𝐽 } ∖ 𝐶 ) ) )
53	33 52	syl	⊢ ( 𝜑 → ( ( 1 ... 𝐽 ) ∖ 𝐶 ) = ( ( ( 1 ... ( 𝐽 − 1 ) ) ∖ 𝐶 ) ∪ ( { 𝐽 } ∖ 𝐶 ) ) )
54		disj3	⊢ ( ( { 𝐽 } ∩ 𝐶 ) = ∅ ↔ { 𝐽 } = ( { 𝐽 } ∖ 𝐶 ) )
55	43 54	sylib	⊢ ( ¬ 𝐽 ∈ 𝐶 → { 𝐽 } = ( { 𝐽 } ∖ 𝐶 ) )
56	55	eqcomd	⊢ ( ¬ 𝐽 ∈ 𝐶 → ( { 𝐽 } ∖ 𝐶 ) = { 𝐽 } )
57	56	uneq2d	⊢ ( ¬ 𝐽 ∈ 𝐶 → ( ( ( 1 ... ( 𝐽 − 1 ) ) ∖ 𝐶 ) ∪ ( { 𝐽 } ∖ 𝐶 ) ) = ( ( ( 1 ... ( 𝐽 − 1 ) ) ∖ 𝐶 ) ∪ { 𝐽 } ) )
58	53 57	sylan9eq	⊢ ( ( 𝜑 ∧ ¬ 𝐽 ∈ 𝐶 ) → ( ( 1 ... 𝐽 ) ∖ 𝐶 ) = ( ( ( 1 ... ( 𝐽 − 1 ) ) ∖ 𝐶 ) ∪ { 𝐽 } ) )
59	58	fveq2d	⊢ ( ( 𝜑 ∧ ¬ 𝐽 ∈ 𝐶 ) → ( ♯ ‘ ( ( 1 ... 𝐽 ) ∖ 𝐶 ) ) = ( ♯ ‘ ( ( ( 1 ... ( 𝐽 − 1 ) ) ∖ 𝐶 ) ∪ { 𝐽 } ) ) )
60	8	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐽 ∈ 𝐶 ) → 𝐽 ∈ ℤ )
61		uzid	⊢ ( 𝐽 ∈ ℤ → 𝐽 ∈ ( ℤ_≥ ‘ 𝐽 ) )
62		uznfz	⊢ ( 𝐽 ∈ ( ℤ_≥ ‘ 𝐽 ) → ¬ 𝐽 ∈ ( 1 ... ( 𝐽 − 1 ) ) )
63	8 61 62	3syl	⊢ ( 𝜑 → ¬ 𝐽 ∈ ( 1 ... ( 𝐽 − 1 ) ) )
64	63	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐽 ∈ 𝐶 ) → ¬ 𝐽 ∈ ( 1 ... ( 𝐽 − 1 ) ) )
65		difss	⊢ ( ( 1 ... ( 𝐽 − 1 ) ) ∖ 𝐶 ) ⊆ ( 1 ... ( 𝐽 − 1 ) )
66	65	sseli	⊢ ( 𝐽 ∈ ( ( 1 ... ( 𝐽 − 1 ) ) ∖ 𝐶 ) → 𝐽 ∈ ( 1 ... ( 𝐽 − 1 ) ) )
67	64 66	nsyl	⊢ ( ( 𝜑 ∧ ¬ 𝐽 ∈ 𝐶 ) → ¬ 𝐽 ∈ ( ( 1 ... ( 𝐽 − 1 ) ) ∖ 𝐶 ) )
68		ssfi	⊢ ( ( ( 1 ... ( 𝐽 − 1 ) ) ∈ Fin ∧ ( ( 1 ... ( 𝐽 − 1 ) ) ∖ 𝐶 ) ⊆ ( 1 ... ( 𝐽 − 1 ) ) ) → ( ( 1 ... ( 𝐽 − 1 ) ) ∖ 𝐶 ) ∈ Fin )
69	11 65 68	mp2an	⊢ ( ( 1 ... ( 𝐽 − 1 ) ) ∖ 𝐶 ) ∈ Fin
70	67 69	jctil	⊢ ( ( 𝜑 ∧ ¬ 𝐽 ∈ 𝐶 ) → ( ( ( 1 ... ( 𝐽 − 1 ) ) ∖ 𝐶 ) ∈ Fin ∧ ¬ 𝐽 ∈ ( ( 1 ... ( 𝐽 − 1 ) ) ∖ 𝐶 ) ) )
71		hashunsng	⊢ ( 𝐽 ∈ ℤ → ( ( ( ( 1 ... ( 𝐽 − 1 ) ) ∖ 𝐶 ) ∈ Fin ∧ ¬ 𝐽 ∈ ( ( 1 ... ( 𝐽 − 1 ) ) ∖ 𝐶 ) ) → ( ♯ ‘ ( ( ( 1 ... ( 𝐽 − 1 ) ) ∖ 𝐶 ) ∪ { 𝐽 } ) ) = ( ( ♯ ‘ ( ( 1 ... ( 𝐽 − 1 ) ) ∖ 𝐶 ) ) + 1 ) ) )
72	60 70 71	sylc	⊢ ( ( 𝜑 ∧ ¬ 𝐽 ∈ 𝐶 ) → ( ♯ ‘ ( ( ( 1 ... ( 𝐽 − 1 ) ) ∖ 𝐶 ) ∪ { 𝐽 } ) ) = ( ( ♯ ‘ ( ( 1 ... ( 𝐽 − 1 ) ) ∖ 𝐶 ) ) + 1 ) )
73	59 72	eqtrd	⊢ ( ( 𝜑 ∧ ¬ 𝐽 ∈ 𝐶 ) → ( ♯ ‘ ( ( 1 ... 𝐽 ) ∖ 𝐶 ) ) = ( ( ♯ ‘ ( ( 1 ... ( 𝐽 − 1 ) ) ∖ 𝐶 ) ) + 1 ) )
74	49 73	oveq12d	⊢ ( ( 𝜑 ∧ ¬ 𝐽 ∈ 𝐶 ) → ( ( ♯ ‘ ( ( 1 ... 𝐽 ) ∩ 𝐶 ) ) − ( ♯ ‘ ( ( 1 ... 𝐽 ) ∖ 𝐶 ) ) ) = ( ( ♯ ‘ ( ( 1 ... ( 𝐽 − 1 ) ) ∩ 𝐶 ) ) − ( ( ♯ ‘ ( ( 1 ... ( 𝐽 − 1 ) ) ∖ 𝐶 ) ) + 1 ) ) )
75	26 31 74	3eqtr4rd	⊢ ( ( 𝜑 ∧ ¬ 𝐽 ∈ 𝐶 ) → ( ( ♯ ‘ ( ( 1 ... 𝐽 ) ∩ 𝐶 ) ) − ( ♯ ‘ ( ( 1 ... 𝐽 ) ∖ 𝐶 ) ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝐽 − 1 ) ) − 1 ) )
76	10 75	eqtrd	⊢ ( ( 𝜑 ∧ ¬ 𝐽 ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝐽 ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝐽 − 1 ) ) − 1 ) )
77	76	ex	⊢ ( 𝜑 → ( ¬ 𝐽 ∈ 𝐶 → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝐽 ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝐽 − 1 ) ) − 1 ) ) )
78	9	adantr	⊢ ( ( 𝜑 ∧ 𝐽 ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝐽 ) = ( ( ♯ ‘ ( ( 1 ... 𝐽 ) ∩ 𝐶 ) ) − ( ♯ ‘ ( ( 1 ... 𝐽 ) ∖ 𝐶 ) ) ) )
79	17	a1i	⊢ ( ( 𝜑 ∧ 𝐽 ∈ 𝐶 ) → ( ♯ ‘ ( ( 1 ... ( 𝐽 − 1 ) ) ∩ 𝐶 ) ) ∈ ℂ )
80		1cnd	⊢ ( ( 𝜑 ∧ 𝐽 ∈ 𝐶 ) → 1 ∈ ℂ )
81	23	a1i	⊢ ( ( 𝜑 ∧ 𝐽 ∈ 𝐶 ) → ( ♯ ‘ ( ( 1 ... ( 𝐽 − 1 ) ) ∖ 𝐶 ) ) ∈ ℂ )
82	79 80 81	addsubd	⊢ ( ( 𝜑 ∧ 𝐽 ∈ 𝐶 ) → ( ( ( ♯ ‘ ( ( 1 ... ( 𝐽 − 1 ) ) ∩ 𝐶 ) ) + 1 ) − ( ♯ ‘ ( ( 1 ... ( 𝐽 − 1 ) ) ∖ 𝐶 ) ) ) = ( ( ( ♯ ‘ ( ( 1 ... ( 𝐽 − 1 ) ) ∩ 𝐶 ) ) − ( ♯ ‘ ( ( 1 ... ( 𝐽 − 1 ) ) ∖ 𝐶 ) ) ) + 1 ) )
83	38	fveq2d	⊢ ( 𝜑 → ( ♯ ‘ ( ( 1 ... 𝐽 ) ∩ 𝐶 ) ) = ( ♯ ‘ ( ( ( 1 ... ( 𝐽 − 1 ) ) ∩ 𝐶 ) ∪ ( { 𝐽 } ∩ 𝐶 ) ) ) )
84	83	adantr	⊢ ( ( 𝜑 ∧ 𝐽 ∈ 𝐶 ) → ( ♯ ‘ ( ( 1 ... 𝐽 ) ∩ 𝐶 ) ) = ( ♯ ‘ ( ( ( 1 ... ( 𝐽 − 1 ) ) ∩ 𝐶 ) ∪ ( { 𝐽 } ∩ 𝐶 ) ) ) )
85		snssi	⊢ ( 𝐽 ∈ 𝐶 → { 𝐽 } ⊆ 𝐶 )
86		dfss2	⊢ ( { 𝐽 } ⊆ 𝐶 ↔ ( { 𝐽 } ∩ 𝐶 ) = { 𝐽 } )
87	85 86	sylib	⊢ ( 𝐽 ∈ 𝐶 → ( { 𝐽 } ∩ 𝐶 ) = { 𝐽 } )
88	87	uneq2d	⊢ ( 𝐽 ∈ 𝐶 → ( ( ( 1 ... ( 𝐽 − 1 ) ) ∩ 𝐶 ) ∪ ( { 𝐽 } ∩ 𝐶 ) ) = ( ( ( 1 ... ( 𝐽 − 1 ) ) ∩ 𝐶 ) ∪ { 𝐽 } ) )
89	88	fveq2d	⊢ ( 𝐽 ∈ 𝐶 → ( ♯ ‘ ( ( ( 1 ... ( 𝐽 − 1 ) ) ∩ 𝐶 ) ∪ ( { 𝐽 } ∩ 𝐶 ) ) ) = ( ♯ ‘ ( ( ( 1 ... ( 𝐽 − 1 ) ) ∩ 𝐶 ) ∪ { 𝐽 } ) ) )
90	89	adantl	⊢ ( ( 𝜑 ∧ 𝐽 ∈ 𝐶 ) → ( ♯ ‘ ( ( ( 1 ... ( 𝐽 − 1 ) ) ∩ 𝐶 ) ∪ ( { 𝐽 } ∩ 𝐶 ) ) ) = ( ♯ ‘ ( ( ( 1 ... ( 𝐽 − 1 ) ) ∩ 𝐶 ) ∪ { 𝐽 } ) ) )
91		simpr	⊢ ( ( 𝜑 ∧ 𝐽 ∈ 𝐶 ) → 𝐽 ∈ 𝐶 )
92	8	adantr	⊢ ( ( 𝜑 ∧ 𝐽 ∈ 𝐶 ) → 𝐽 ∈ ℤ )
93	92 61 62	3syl	⊢ ( ( 𝜑 ∧ 𝐽 ∈ 𝐶 ) → ¬ 𝐽 ∈ ( 1 ... ( 𝐽 − 1 ) ) )
94	12	sseli	⊢ ( 𝐽 ∈ ( ( 1 ... ( 𝐽 − 1 ) ) ∩ 𝐶 ) → 𝐽 ∈ ( 1 ... ( 𝐽 − 1 ) ) )
95	93 94	nsyl	⊢ ( ( 𝜑 ∧ 𝐽 ∈ 𝐶 ) → ¬ 𝐽 ∈ ( ( 1 ... ( 𝐽 − 1 ) ) ∩ 𝐶 ) )
96	95 14	jctil	⊢ ( ( 𝜑 ∧ 𝐽 ∈ 𝐶 ) → ( ( ( 1 ... ( 𝐽 − 1 ) ) ∩ 𝐶 ) ∈ Fin ∧ ¬ 𝐽 ∈ ( ( 1 ... ( 𝐽 − 1 ) ) ∩ 𝐶 ) ) )
97		hashunsng	⊢ ( 𝐽 ∈ 𝐶 → ( ( ( ( 1 ... ( 𝐽 − 1 ) ) ∩ 𝐶 ) ∈ Fin ∧ ¬ 𝐽 ∈ ( ( 1 ... ( 𝐽 − 1 ) ) ∩ 𝐶 ) ) → ( ♯ ‘ ( ( ( 1 ... ( 𝐽 − 1 ) ) ∩ 𝐶 ) ∪ { 𝐽 } ) ) = ( ( ♯ ‘ ( ( 1 ... ( 𝐽 − 1 ) ) ∩ 𝐶 ) ) + 1 ) ) )
98	91 96 97	sylc	⊢ ( ( 𝜑 ∧ 𝐽 ∈ 𝐶 ) → ( ♯ ‘ ( ( ( 1 ... ( 𝐽 − 1 ) ) ∩ 𝐶 ) ∪ { 𝐽 } ) ) = ( ( ♯ ‘ ( ( 1 ... ( 𝐽 − 1 ) ) ∩ 𝐶 ) ) + 1 ) )
99	84 90 98	3eqtrd	⊢ ( ( 𝜑 ∧ 𝐽 ∈ 𝐶 ) → ( ♯ ‘ ( ( 1 ... 𝐽 ) ∩ 𝐶 ) ) = ( ( ♯ ‘ ( ( 1 ... ( 𝐽 − 1 ) ) ∩ 𝐶 ) ) + 1 ) )
100	53	fveq2d	⊢ ( 𝜑 → ( ♯ ‘ ( ( 1 ... 𝐽 ) ∖ 𝐶 ) ) = ( ♯ ‘ ( ( ( 1 ... ( 𝐽 − 1 ) ) ∖ 𝐶 ) ∪ ( { 𝐽 } ∖ 𝐶 ) ) ) )
101	100	adantr	⊢ ( ( 𝜑 ∧ 𝐽 ∈ 𝐶 ) → ( ♯ ‘ ( ( 1 ... 𝐽 ) ∖ 𝐶 ) ) = ( ♯ ‘ ( ( ( 1 ... ( 𝐽 − 1 ) ) ∖ 𝐶 ) ∪ ( { 𝐽 } ∖ 𝐶 ) ) ) )
102		difin2	⊢ ( { 𝐽 } ⊆ 𝐶 → ( { 𝐽 } ∖ 𝐶 ) = ( ( 𝐶 ∖ 𝐶 ) ∩ { 𝐽 } ) )
103		difid	⊢ ( 𝐶 ∖ 𝐶 ) = ∅
104	103	ineq1i	⊢ ( ( 𝐶 ∖ 𝐶 ) ∩ { 𝐽 } ) = ( ∅ ∩ { 𝐽 } )
105		0in	⊢ ( ∅ ∩ { 𝐽 } ) = ∅
106	104 105	eqtri	⊢ ( ( 𝐶 ∖ 𝐶 ) ∩ { 𝐽 } ) = ∅
107	102 106	eqtrdi	⊢ ( { 𝐽 } ⊆ 𝐶 → ( { 𝐽 } ∖ 𝐶 ) = ∅ )
108	85 107	syl	⊢ ( 𝐽 ∈ 𝐶 → ( { 𝐽 } ∖ 𝐶 ) = ∅ )
109	108	uneq2d	⊢ ( 𝐽 ∈ 𝐶 → ( ( ( 1 ... ( 𝐽 − 1 ) ) ∖ 𝐶 ) ∪ ( { 𝐽 } ∖ 𝐶 ) ) = ( ( ( 1 ... ( 𝐽 − 1 ) ) ∖ 𝐶 ) ∪ ∅ ) )
110	109	fveq2d	⊢ ( 𝐽 ∈ 𝐶 → ( ♯ ‘ ( ( ( 1 ... ( 𝐽 − 1 ) ) ∖ 𝐶 ) ∪ ( { 𝐽 } ∖ 𝐶 ) ) ) = ( ♯ ‘ ( ( ( 1 ... ( 𝐽 − 1 ) ) ∖ 𝐶 ) ∪ ∅ ) ) )
111	110	adantl	⊢ ( ( 𝜑 ∧ 𝐽 ∈ 𝐶 ) → ( ♯ ‘ ( ( ( 1 ... ( 𝐽 − 1 ) ) ∖ 𝐶 ) ∪ ( { 𝐽 } ∖ 𝐶 ) ) ) = ( ♯ ‘ ( ( ( 1 ... ( 𝐽 − 1 ) ) ∖ 𝐶 ) ∪ ∅ ) ) )
112		un0	⊢ ( ( ( 1 ... ( 𝐽 − 1 ) ) ∖ 𝐶 ) ∪ ∅ ) = ( ( 1 ... ( 𝐽 − 1 ) ) ∖ 𝐶 )
113	112	a1i	⊢ ( ( 𝜑 ∧ 𝐽 ∈ 𝐶 ) → ( ( ( 1 ... ( 𝐽 − 1 ) ) ∖ 𝐶 ) ∪ ∅ ) = ( ( 1 ... ( 𝐽 − 1 ) ) ∖ 𝐶 ) )
114	113	fveq2d	⊢ ( ( 𝜑 ∧ 𝐽 ∈ 𝐶 ) → ( ♯ ‘ ( ( ( 1 ... ( 𝐽 − 1 ) ) ∖ 𝐶 ) ∪ ∅ ) ) = ( ♯ ‘ ( ( 1 ... ( 𝐽 − 1 ) ) ∖ 𝐶 ) ) )
115	101 111 114	3eqtrd	⊢ ( ( 𝜑 ∧ 𝐽 ∈ 𝐶 ) → ( ♯ ‘ ( ( 1 ... 𝐽 ) ∖ 𝐶 ) ) = ( ♯ ‘ ( ( 1 ... ( 𝐽 − 1 ) ) ∖ 𝐶 ) ) )
116	99 115	oveq12d	⊢ ( ( 𝜑 ∧ 𝐽 ∈ 𝐶 ) → ( ( ♯ ‘ ( ( 1 ... 𝐽 ) ∩ 𝐶 ) ) − ( ♯ ‘ ( ( 1 ... 𝐽 ) ∖ 𝐶 ) ) ) = ( ( ( ♯ ‘ ( ( 1 ... ( 𝐽 − 1 ) ) ∩ 𝐶 ) ) + 1 ) − ( ♯ ‘ ( ( 1 ... ( 𝐽 − 1 ) ) ∖ 𝐶 ) ) ) )
117	29	adantr	⊢ ( ( 𝜑 ∧ 𝐽 ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝐽 − 1 ) ) = ( ( ♯ ‘ ( ( 1 ... ( 𝐽 − 1 ) ) ∩ 𝐶 ) ) − ( ♯ ‘ ( ( 1 ... ( 𝐽 − 1 ) ) ∖ 𝐶 ) ) ) )
118	117	oveq1d	⊢ ( ( 𝜑 ∧ 𝐽 ∈ 𝐶 ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝐽 − 1 ) ) + 1 ) = ( ( ( ♯ ‘ ( ( 1 ... ( 𝐽 − 1 ) ) ∩ 𝐶 ) ) − ( ♯ ‘ ( ( 1 ... ( 𝐽 − 1 ) ) ∖ 𝐶 ) ) ) + 1 ) )
119	82 116 118	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝐽 ∈ 𝐶 ) → ( ( ♯ ‘ ( ( 1 ... 𝐽 ) ∩ 𝐶 ) ) − ( ♯ ‘ ( ( 1 ... 𝐽 ) ∖ 𝐶 ) ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝐽 − 1 ) ) + 1 ) )
120	78 119	eqtrd	⊢ ( ( 𝜑 ∧ 𝐽 ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝐽 ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝐽 − 1 ) ) + 1 ) )
121	120	ex	⊢ ( 𝜑 → ( 𝐽 ∈ 𝐶 → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝐽 ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝐽 − 1 ) ) + 1 ) ) )
122	77 121	jca	⊢ ( 𝜑 → ( ( ¬ 𝐽 ∈ 𝐶 → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝐽 ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝐽 − 1 ) ) − 1 ) ) ∧ ( 𝐽 ∈ 𝐶 → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝐽 ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝐽 − 1 ) ) + 1 ) ) ) )

Metamath Proof Explorer

Theorem ballotlemfp1

Proof