Theorem ballotleme

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

	Ref	Expression
Hypotheses	ballotth.m	⊢ 𝑀 ∈ ℕ
	ballotth.n	⊢ 𝑁 ∈ ℕ
	ballotth.o	⊢ 𝑂 = { 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ♯ ‘ 𝑐 ) = 𝑀 }
	ballotth.p	⊢ 𝑃 = ( 𝑥 ∈ 𝒫 𝑂 ↦ ( ( ♯ ‘ 𝑥 ) / ( ♯ ‘ 𝑂 ) ) )
	ballotth.f	⊢ 𝐹 = ( 𝑐 ∈ 𝑂 ↦ ( 𝑖 ∈ ℤ ↦ ( ( ♯ ‘ ( ( 1 ... 𝑖 ) ∩ 𝑐 ) ) − ( ♯ ‘ ( ( 1 ... 𝑖 ) ∖ 𝑐 ) ) ) ) )
	ballotth.e	⊢ 𝐸 = { 𝑐 ∈ 𝑂 ∣ ∀ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) 0 < ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑖 ) }
Assertion	ballotleme	⊢ ( 𝐶 ∈ 𝐸 ↔ ( 𝐶 ∈ 𝑂 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) 0 < ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ballotth.m	⊢ 𝑀 ∈ ℕ
2		ballotth.n	⊢ 𝑁 ∈ ℕ
3		ballotth.o	⊢ 𝑂 = { 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ♯ ‘ 𝑐 ) = 𝑀 }
4		ballotth.p	⊢ 𝑃 = ( 𝑥 ∈ 𝒫 𝑂 ↦ ( ( ♯ ‘ 𝑥 ) / ( ♯ ‘ 𝑂 ) ) )
5		ballotth.f	⊢ 𝐹 = ( 𝑐 ∈ 𝑂 ↦ ( 𝑖 ∈ ℤ ↦ ( ( ♯ ‘ ( ( 1 ... 𝑖 ) ∩ 𝑐 ) ) − ( ♯ ‘ ( ( 1 ... 𝑖 ) ∖ 𝑐 ) ) ) ) )
6		ballotth.e	⊢ 𝐸 = { 𝑐 ∈ 𝑂 ∣ ∀ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) 0 < ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑖 ) }
7		fveq2	⊢ ( 𝑑 = 𝐶 → ( 𝐹 ‘ 𝑑 ) = ( 𝐹 ‘ 𝐶 ) )
8	7	fveq1d	⊢ ( 𝑑 = 𝐶 → ( ( 𝐹 ‘ 𝑑 ) ‘ 𝑖 ) = ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) )
9	8	breq2d	⊢ ( 𝑑 = 𝐶 → ( 0 < ( ( 𝐹 ‘ 𝑑 ) ‘ 𝑖 ) ↔ 0 < ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ) )
10	9	ralbidv	⊢ ( 𝑑 = 𝐶 → ( ∀ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) 0 < ( ( 𝐹 ‘ 𝑑 ) ‘ 𝑖 ) ↔ ∀ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) 0 < ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ) )
11		fveq2	⊢ ( 𝑐 = 𝑑 → ( 𝐹 ‘ 𝑐 ) = ( 𝐹 ‘ 𝑑 ) )
12	11	fveq1d	⊢ ( 𝑐 = 𝑑 → ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑖 ) = ( ( 𝐹 ‘ 𝑑 ) ‘ 𝑖 ) )
13	12	breq2d	⊢ ( 𝑐 = 𝑑 → ( 0 < ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑖 ) ↔ 0 < ( ( 𝐹 ‘ 𝑑 ) ‘ 𝑖 ) ) )
14	13	ralbidv	⊢ ( 𝑐 = 𝑑 → ( ∀ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) 0 < ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑖 ) ↔ ∀ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) 0 < ( ( 𝐹 ‘ 𝑑 ) ‘ 𝑖 ) ) )
15	14	cbvrabv	⊢ { 𝑐 ∈ 𝑂 ∣ ∀ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) 0 < ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑖 ) } = { 𝑑 ∈ 𝑂 ∣ ∀ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) 0 < ( ( 𝐹 ‘ 𝑑 ) ‘ 𝑖 ) }
16	6 15	eqtri	⊢ 𝐸 = { 𝑑 ∈ 𝑂 ∣ ∀ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) 0 < ( ( 𝐹 ‘ 𝑑 ) ‘ 𝑖 ) }
17	10 16	elrab2	⊢ ( 𝐶 ∈ 𝐸 ↔ ( 𝐶 ∈ 𝑂 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) 0 < ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ) )