Theorem ballotlemii

Description: The first tie cannot be reached at the first pick. (Contributed by Thierry Arnoux, 4-Apr-2017)

	Ref	Expression
Hypotheses	ballotth.m	⊢ 𝑀 ∈ ℕ
	ballotth.n	⊢ 𝑁 ∈ ℕ
	ballotth.o	⊢ 𝑂 = { 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ♯ ‘ 𝑐 ) = 𝑀 }
	ballotth.p	⊢ 𝑃 = ( 𝑥 ∈ 𝒫 𝑂 ↦ ( ( ♯ ‘ 𝑥 ) / ( ♯ ‘ 𝑂 ) ) )
	ballotth.f	⊢ 𝐹 = ( 𝑐 ∈ 𝑂 ↦ ( 𝑖 ∈ ℤ ↦ ( ( ♯ ‘ ( ( 1 ... 𝑖 ) ∩ 𝑐 ) ) − ( ♯ ‘ ( ( 1 ... 𝑖 ) ∖ 𝑐 ) ) ) ) )
	ballotth.e	⊢ 𝐸 = { 𝑐 ∈ 𝑂 ∣ ∀ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) 0 < ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑖 ) }
	ballotth.mgtn	⊢ 𝑁 < 𝑀
	ballotth.i	⊢ 𝐼 = ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ↦ inf ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑘 ) = 0 } , ℝ , < ) )
Assertion	ballotlemii	⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 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		ballotth.e	⊢ 𝐸 = { 𝑐 ∈ 𝑂 ∣ ∀ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) 0 < ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑖 ) }
7		ballotth.mgtn	⊢ 𝑁 < 𝑀
8		ballotth.i	⊢ 𝐼 = ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ↦ inf ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑘 ) = 0 } , ℝ , < ) )
9		1e0p1	⊢ 1 = ( 0 + 1 )
10		ax-1ne0	⊢ 1 ≠ 0
11	9 10	eqnetrri	⊢ ( 0 + 1 ) ≠ 0
12	11	neii	⊢ ¬ ( 0 + 1 ) = 0
13		eldifi	⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → 𝐶 ∈ 𝑂 )
14		1nn	⊢ 1 ∈ ℕ
15	14	a1i	⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → 1 ∈ ℕ )
16	1 2 3 4 5 13 15	ballotlemfp1	⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( ¬ 1 ∈ 𝐶 → ( ( 𝐹 ‘ 𝐶 ) ‘ 1 ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 1 − 1 ) ) − 1 ) ) ∧ ( 1 ∈ 𝐶 → ( ( 𝐹 ‘ 𝐶 ) ‘ 1 ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 1 − 1 ) ) + 1 ) ) ) )
17	16	simprd	⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 1 ∈ 𝐶 → ( ( 𝐹 ‘ 𝐶 ) ‘ 1 ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 1 − 1 ) ) + 1 ) ) )
18	17	imp	⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 1 ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ 1 ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 1 − 1 ) ) + 1 ) )
19		1m1e0	⊢ ( 1 − 1 ) = 0
20	19	fveq2i	⊢ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 1 − 1 ) ) = ( ( 𝐹 ‘ 𝐶 ) ‘ 0 )
21	20	oveq1i	⊢ ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 1 − 1 ) ) + 1 ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ 0 ) + 1 )
22	21	a1i	⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 1 ∈ 𝐶 ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 1 − 1 ) ) + 1 ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ 0 ) + 1 ) )
23	1 2 3 4 5	ballotlemfval0	⊢ ( 𝐶 ∈ 𝑂 → ( ( 𝐹 ‘ 𝐶 ) ‘ 0 ) = 0 )
24	13 23	syl	⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ 0 ) = 0 )
25	24	adantr	⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 1 ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ 0 ) = 0 )
26	25	oveq1d	⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 1 ∈ 𝐶 ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ 0 ) + 1 ) = ( 0 + 1 ) )
27	18 22 26	3eqtrrd	⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 1 ∈ 𝐶 ) → ( 0 + 1 ) = ( ( 𝐹 ‘ 𝐶 ) ‘ 1 ) )
28	27	eqeq1d	⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 1 ∈ 𝐶 ) → ( ( 0 + 1 ) = 0 ↔ ( ( 𝐹 ‘ 𝐶 ) ‘ 1 ) = 0 ) )
29	12 28	mtbii	⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 1 ∈ 𝐶 ) → ¬ ( ( 𝐹 ‘ 𝐶 ) ‘ 1 ) = 0 )
30	1 2 3 4 5 6 7 8	ballotlemiex	⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( 𝐼 ‘ 𝐶 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝐼 ‘ 𝐶 ) ) = 0 ) )
31	30	simprd	⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝐼 ‘ 𝐶 ) ) = 0 )
32	31	ad2antrr	⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 1 ∈ 𝐶 ) ∧ ( 𝐼 ‘ 𝐶 ) = 1 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝐼 ‘ 𝐶 ) ) = 0 )
33		fveqeq2	⊢ ( ( 𝐼 ‘ 𝐶 ) = 1 → ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝐼 ‘ 𝐶 ) ) = 0 ↔ ( ( 𝐹 ‘ 𝐶 ) ‘ 1 ) = 0 ) )
34	33	adantl	⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 1 ∈ 𝐶 ) ∧ ( 𝐼 ‘ 𝐶 ) = 1 ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝐼 ‘ 𝐶 ) ) = 0 ↔ ( ( 𝐹 ‘ 𝐶 ) ‘ 1 ) = 0 ) )
35	32 34	mpbid	⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 1 ∈ 𝐶 ) ∧ ( 𝐼 ‘ 𝐶 ) = 1 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ 1 ) = 0 )
36	29 35	mtand	⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 1 ∈ 𝐶 ) → ¬ ( 𝐼 ‘ 𝐶 ) = 1 )
37	36	neqned	⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 1 ∈ 𝐶 ) → ( 𝐼 ‘ 𝐶 ) ≠ 1 )