Theorem ballotlemrv2

Description: Value of R after the tie. (Contributed by Thierry Arnoux, 11-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 } , ℝ , < ) )
	ballotth.s	⊢ 𝑆 = ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ↦ ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ↦ if ( 𝑖 ≤ ( 𝐼 ‘ 𝑐 ) , ( ( ( 𝐼 ‘ 𝑐 ) + 1 ) − 𝑖 ) , 𝑖 ) ) )
	ballotth.r	⊢ 𝑅 = ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ↦ ( ( 𝑆 ‘ 𝑐 ) “ 𝑐 ) )
Assertion	ballotlemrv2	⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 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		ballotth.s	⊢ 𝑆 = ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ↦ ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ↦ if ( 𝑖 ≤ ( 𝐼 ‘ 𝑐 ) , ( ( ( 𝐼 ‘ 𝑐 ) + 1 ) − 𝑖 ) , 𝑖 ) ) )
10		ballotth.r	⊢ 𝑅 = ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ↦ ( ( 𝑆 ‘ 𝑐 ) “ 𝑐 ) )
11	1 2 3 4 5 6 7 8 9 10	ballotlemrv	⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) → ( 𝐽 ∈ ( 𝑅 ‘ 𝐶 ) ↔ if ( 𝐽 ≤ ( 𝐼 ‘ 𝐶 ) , ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝐽 ) , 𝐽 ) ∈ 𝐶 ) )
12	11	3adant3	⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ( 𝐼 ‘ 𝐶 ) < 𝐽 ) → ( 𝐽 ∈ ( 𝑅 ‘ 𝐶 ) ↔ if ( 𝐽 ≤ ( 𝐼 ‘ 𝐶 ) , ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝐽 ) , 𝐽 ) ∈ 𝐶 ) )
13		fzssuz	⊢ ( 1 ... ( 𝑀 + 𝑁 ) ) ⊆ ( ℤ≥ ‘ 1 )
14		uzssz	⊢ ( ℤ≥ ‘ 1 ) ⊆ ℤ
15	13 14	sstri	⊢ ( 1 ... ( 𝑀 + 𝑁 ) ) ⊆ ℤ
16	1 2 3 4 5 6 7 8	ballotlemiex	⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( 𝐼 ‘ 𝐶 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝐼 ‘ 𝐶 ) ) = 0 ) )
17	16	simpld	⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝐼 ‘ 𝐶 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) )
18	15 17	sselid	⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝐼 ‘ 𝐶 ) ∈ ℤ )
19	18	adantr	⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) → ( 𝐼 ‘ 𝐶 ) ∈ ℤ )
20	19	zred	⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) → ( 𝐼 ‘ 𝐶 ) ∈ ℝ )
21		simpr	⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) → 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) )
22	15 21	sselid	⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) → 𝐽 ∈ ℤ )
23	22	zred	⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) → 𝐽 ∈ ℝ )
24	20 23	ltnled	⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) → ( ( 𝐼 ‘ 𝐶 ) < 𝐽 ↔ ¬ 𝐽 ≤ ( 𝐼 ‘ 𝐶 ) ) )
25	24	biimp3a	⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ( 𝐼 ‘ 𝐶 ) < 𝐽 ) → ¬ 𝐽 ≤ ( 𝐼 ‘ 𝐶 ) )
26	25	iffalsed	⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ( 𝐼 ‘ 𝐶 ) < 𝐽 ) → if ( 𝐽 ≤ ( 𝐼 ‘ 𝐶 ) , ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝐽 ) , 𝐽 ) = 𝐽 )
27	26	eleq1d	⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ( 𝐼 ‘ 𝐶 ) < 𝐽 ) → ( if ( 𝐽 ≤ ( 𝐼 ‘ 𝐶 ) , ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝐽 ) , 𝐽 ) ∈ 𝐶 ↔ 𝐽 ∈ 𝐶 ) )
28	12 27	bitrd	⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ( 𝐼 ‘ 𝐶 ) < 𝐽 ) → ( 𝐽 ∈ ( 𝑅 ‘ 𝐶 ) ↔ 𝐽 ∈ 𝐶 ) )