Metamath Proof Explorer

Theorem ballotlemsima

Description: The image by S of an interval before the first pick. (Contributed by Thierry Arnoux, 5-May-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 ) − 𝑖 ) , 𝑖 ) ) )
Assertion ballotlemsima ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 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 ballotth.s ⊢ 𝑆 = ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ↦ ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ↦ if ( 𝑖 ≤ ( 𝐼 ‘ 𝑐 ) , ( ( ( 𝐼 ‘ 𝑐 ) + 1 ) − 𝑖 ) , 𝑖 ) ) )
10 imassrn ⊢ ( ( 𝑆 ‘ 𝐶 ) “ ( 1 ... 𝐽 ) ) ⊆ ran ( 𝑆 ‘ 𝐶 )
11 1 2 3 4 5 6 7 8 9 ballotlemsf1o ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( 𝑆 ‘ 𝐶 ) : ( 1 ... ( 𝑀 + 𝑁 ) ) –1-1-onto→ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ◡ ( 𝑆 ‘ 𝐶 ) = ( 𝑆 ‘ 𝐶 ) ) )
12 11 simpld ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝑆 ‘ 𝐶 ) : ( 1 ... ( 𝑀 + 𝑁 ) ) –1-1-onto→ ( 1 ... ( 𝑀 + 𝑁 ) ) )
13 f1of ⊢ ( ( 𝑆 ‘ 𝐶 ) : ( 1 ... ( 𝑀 + 𝑁 ) ) –1-1-onto→ ( 1 ... ( 𝑀 + 𝑁 ) ) → ( 𝑆 ‘ 𝐶 ) : ( 1 ... ( 𝑀 + 𝑁 ) ) ⟶ ( 1 ... ( 𝑀 + 𝑁 ) ) )
14 frn ⊢ ( ( 𝑆 ‘ 𝐶 ) : ( 1 ... ( 𝑀 + 𝑁 ) ) ⟶ ( 1 ... ( 𝑀 + 𝑁 ) ) → ran ( 𝑆 ‘ 𝐶 ) ⊆ ( 1 ... ( 𝑀 + 𝑁 ) ) )
15 12 13 14 3syl ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ran ( 𝑆 ‘ 𝐶 ) ⊆ ( 1 ... ( 𝑀 + 𝑁 ) ) )
16 10 15 sstrid ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( 𝑆 ‘ 𝐶 ) “ ( 1 ... 𝐽 ) ) ⊆ ( 1 ... ( 𝑀 + 𝑁 ) ) )
17 fzssuz ⊢ ( 1 ... ( 𝑀 + 𝑁 ) ) ⊆ ( ℤ≥ ‘ 1 )
18 uzssz ⊢ ( ℤ≥ ‘ 1 ) ⊆ ℤ
19 17 18 sstri ⊢ ( 1 ... ( 𝑀 + 𝑁 ) ) ⊆ ℤ
20 16 19 sstrdi ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( 𝑆 ‘ 𝐶 ) “ ( 1 ... 𝐽 ) ) ⊆ ℤ )
21 20 adantr ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( 𝑆 ‘ 𝐶 ) “ ( 1 ... 𝐽 ) ) ⊆ ℤ )
22 21 sselda ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) ∧ 𝑘 ∈ ( ( 𝑆 ‘ 𝐶 ) “ ( 1 ... 𝐽 ) ) ) → 𝑘 ∈ ℤ )
23 elfzelz ⊢ ( 𝑘 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ... ( 𝐼 ‘ 𝐶 ) ) → 𝑘 ∈ ℤ )
24 23 adantl ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) ∧ 𝑘 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ... ( 𝐼 ‘ 𝐶 ) ) ) → 𝑘 ∈ ℤ )
25 f1ofn ⊢ ( ( 𝑆 ‘ 𝐶 ) : ( 1 ... ( 𝑀 + 𝑁 ) ) –1-1-onto→ ( 1 ... ( 𝑀 + 𝑁 ) ) → ( 𝑆 ‘ 𝐶 ) Fn ( 1 ... ( 𝑀 + 𝑁 ) ) )
26 12 25 syl ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝑆 ‘ 𝐶 ) Fn ( 1 ... ( 𝑀 + 𝑁 ) ) )
27 26 adantr ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( 𝑆 ‘ 𝐶 ) Fn ( 1 ... ( 𝑀 + 𝑁 ) ) )
28 1 2 3 4 5 6 7 8 ballotlemiex ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( 𝐼 ‘ 𝐶 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝐼 ‘ 𝐶 ) ) = 0 ) )
29 28 simpld ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝐼 ‘ 𝐶 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) )
30 29 adantr ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( 𝐼 ‘ 𝐶 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) )
31 elfzuz3 ⊢ ( ( 𝐼 ‘ 𝐶 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) → ( 𝑀 + 𝑁 ) ∈ ( ℤ≥ ‘ ( 𝐼 ‘ 𝐶 ) ) )
32 30 31 syl ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( 𝑀 + 𝑁 ) ∈ ( ℤ≥ ‘ ( 𝐼 ‘ 𝐶 ) ) )
33 elfzuz3 ⊢ ( 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) → ( 𝐼 ‘ 𝐶 ) ∈ ( ℤ≥ ‘ 𝐽 ) )
34 33 adantl ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( 𝐼 ‘ 𝐶 ) ∈ ( ℤ≥ ‘ 𝐽 ) )
35 uztrn ⊢ ( ( ( 𝑀 + 𝑁 ) ∈ ( ℤ≥ ‘ ( 𝐼 ‘ 𝐶 ) ) ∧ ( 𝐼 ‘ 𝐶 ) ∈ ( ℤ≥ ‘ 𝐽 ) ) → ( 𝑀 + 𝑁 ) ∈ ( ℤ≥ ‘ 𝐽 ) )
36 32 34 35 syl2anc ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( 𝑀 + 𝑁 ) ∈ ( ℤ≥ ‘ 𝐽 ) )
37 fzss2 ⊢ ( ( 𝑀 + 𝑁 ) ∈ ( ℤ≥ ‘ 𝐽 ) → ( 1 ... 𝐽 ) ⊆ ( 1 ... ( 𝑀 + 𝑁 ) ) )
38 36 37 syl ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( 1 ... 𝐽 ) ⊆ ( 1 ... ( 𝑀 + 𝑁 ) ) )
39 fvelimab ⊢ ( ( ( 𝑆 ‘ 𝐶 ) Fn ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ( 1 ... 𝐽 ) ⊆ ( 1 ... ( 𝑀 + 𝑁 ) ) ) → ( 𝑘 ∈ ( ( 𝑆 ‘ 𝐶 ) “ ( 1 ... 𝐽 ) ) ↔ ∃ 𝑗 ∈ ( 1 ... 𝐽 ) ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑗 ) = 𝑘 ) )
40 27 38 39 syl2anc ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( 𝑘 ∈ ( ( 𝑆 ‘ 𝐶 ) “ ( 1 ... 𝐽 ) ) ↔ ∃ 𝑗 ∈ ( 1 ... 𝐽 ) ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑗 ) = 𝑘 ) )
41 40 adantr ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) ∧ 𝑘 ∈ ℤ ) → ( 𝑘 ∈ ( ( 𝑆 ‘ 𝐶 ) “ ( 1 ... 𝐽 ) ) ↔ ∃ 𝑗 ∈ ( 1 ... 𝐽 ) ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑗 ) = 𝑘 ) )
42 1zzd ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → 1 ∈ ℤ )
43 1 nnzi ⊢ 𝑀 ∈ ℤ
44 2 nnzi ⊢ 𝑁 ∈ ℤ
45 zaddcl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 + 𝑁 ) ∈ ℤ )
46 43 44 45 mp2an ⊢ ( 𝑀 + 𝑁 ) ∈ ℤ
47 46 a1i ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( 𝑀 + 𝑁 ) ∈ ℤ )
48 elfzelz ⊢ ( 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) → 𝐽 ∈ ℤ )
49 48 adantl ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → 𝐽 ∈ ℤ )
50 elfzle1 ⊢ ( 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) → 1 ≤ 𝐽 )
51 50 adantl ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → 1 ≤ 𝐽 )
52 49 zred ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → 𝐽 ∈ ℝ )
53 elfzelz ⊢ ( ( 𝐼 ‘ 𝐶 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) → ( 𝐼 ‘ 𝐶 ) ∈ ℤ )
54 29 53 syl ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝐼 ‘ 𝐶 ) ∈ ℤ )
55 54 adantr ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( 𝐼 ‘ 𝐶 ) ∈ ℤ )
56 55 zred ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( 𝐼 ‘ 𝐶 ) ∈ ℝ )
57 47 zred ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( 𝑀 + 𝑁 ) ∈ ℝ )
58 elfzle2 ⊢ ( 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) → 𝐽 ≤ ( 𝐼 ‘ 𝐶 ) )
59 58 adantl ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → 𝐽 ≤ ( 𝐼 ‘ 𝐶 ) )
60 elfzle2 ⊢ ( ( 𝐼 ‘ 𝐶 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) → ( 𝐼 ‘ 𝐶 ) ≤ ( 𝑀 + 𝑁 ) )
61 29 60 syl ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝐼 ‘ 𝐶 ) ≤ ( 𝑀 + 𝑁 ) )
62 61 adantr ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( 𝐼 ‘ 𝐶 ) ≤ ( 𝑀 + 𝑁 ) )
63 52 56 57 59 62 letrd ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → 𝐽 ≤ ( 𝑀 + 𝑁 ) )
64 42 47 49 51 63 elfzd ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) )
65 1 2 3 4 5 6 7 8 9 ballotlemsv ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) = if ( 𝐽 ≤ ( 𝐼 ‘ 𝐶 ) , ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝐽 ) , 𝐽 ) )
66 64 65 syldan ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) = if ( 𝐽 ≤ ( 𝐼 ‘ 𝐶 ) , ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝐽 ) , 𝐽 ) )
67 simpr ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) )
68 iftrue ⊢ ( 𝐽 ≤ ( 𝐼 ‘ 𝐶 ) → if ( 𝐽 ≤ ( 𝐼 ‘ 𝐶 ) , ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝐽 ) , 𝐽 ) = ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝐽 ) )
69 67 58 68 3syl ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → if ( 𝐽 ≤ ( 𝐼 ‘ 𝐶 ) , ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝐽 ) , 𝐽 ) = ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝐽 ) )
70 66 69 eqtrd ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) = ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝐽 ) )
71 70 oveq1d ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ... ( 𝐼 ‘ 𝐶 ) ) = ( ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝐽 ) ... ( 𝐼 ‘ 𝐶 ) ) )
72 71 eleq2d ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( 𝑘 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ... ( 𝐼 ‘ 𝐶 ) ) ↔ 𝑘 ∈ ( ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝐽 ) ... ( 𝐼 ‘ 𝐶 ) ) ) )
73 72 adantr ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) ∧ 𝑘 ∈ ℤ ) → ( 𝑘 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ... ( 𝐼 ‘ 𝐶 ) ) ↔ 𝑘 ∈ ( ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝐽 ) ... ( 𝐼 ‘ 𝐶 ) ) ) )
74 54 ad2antrr ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) ∧ 𝑘 ∈ ℤ ) → ( 𝐼 ‘ 𝐶 ) ∈ ℤ )
75 74 zcnd ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) ∧ 𝑘 ∈ ℤ ) → ( 𝐼 ‘ 𝐶 ) ∈ ℂ )
76 1cnd ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) ∧ 𝑘 ∈ ℤ ) → 1 ∈ ℂ )
77 75 76 pncand ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) ∧ 𝑘 ∈ ℤ ) → ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 1 ) = ( 𝐼 ‘ 𝐶 ) )
78 77 oveq2d ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) ∧ 𝑘 ∈ ℤ ) → ( ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝐽 ) ... ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 1 ) ) = ( ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝐽 ) ... ( 𝐼 ‘ 𝐶 ) ) )
79 78 eleq2d ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) ∧ 𝑘 ∈ ℤ ) → ( 𝑘 ∈ ( ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝐽 ) ... ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 1 ) ) ↔ 𝑘 ∈ ( ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝐽 ) ... ( 𝐼 ‘ 𝐶 ) ) ) )
80 1zzd ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) ∧ 𝑘 ∈ ℤ ) → 1 ∈ ℤ )
81 48 ad2antlr ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) ∧ 𝑘 ∈ ℤ ) → 𝐽 ∈ ℤ )
82 74 peano2zd ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) ∧ 𝑘 ∈ ℤ ) → ( ( 𝐼 ‘ 𝐶 ) + 1 ) ∈ ℤ )
83 simpr ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) ∧ 𝑘 ∈ ℤ ) → 𝑘 ∈ ℤ )
84 fzrev ⊢ ( ( ( 1 ∈ ℤ ∧ 𝐽 ∈ ℤ ) ∧ ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) ∈ ℤ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑘 ∈ ( ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝐽 ) ... ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 1 ) ) ↔ ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑘 ) ∈ ( 1 ... 𝐽 ) ) )
85 80 81 82 83 84 syl22anc ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) ∧ 𝑘 ∈ ℤ ) → ( 𝑘 ∈ ( ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝐽 ) ... ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 1 ) ) ↔ ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑘 ) ∈ ( 1 ... 𝐽 ) ) )
86 73 79 85 3bitr2d ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) ∧ 𝑘 ∈ ℤ ) → ( 𝑘 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ... ( 𝐼 ‘ 𝐶 ) ) ↔ ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑘 ) ∈ ( 1 ... 𝐽 ) ) )
87 risset ⊢ ( ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑘 ) ∈ ( 1 ... 𝐽 ) ↔ ∃ 𝑗 ∈ ( 1 ... 𝐽 ) 𝑗 = ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑘 ) )
88 87 a1i ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) ∧ 𝑘 ∈ ℤ ) → ( ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑘 ) ∈ ( 1 ... 𝐽 ) ↔ ∃ 𝑗 ∈ ( 1 ... 𝐽 ) 𝑗 = ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑘 ) ) )
89 eqcom ⊢ ( ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑘 ) = 𝑗 ↔ 𝑗 = ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑘 ) )
90 54 ad2antrr ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝐽 ) ) → ( 𝐼 ‘ 𝐶 ) ∈ ℤ )
91 90 adantlr ⊢ ( ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ 𝑗 ∈ ( 1 ... 𝐽 ) ) → ( 𝐼 ‘ 𝐶 ) ∈ ℤ )
92 91 zcnd ⊢ ( ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ 𝑗 ∈ ( 1 ... 𝐽 ) ) → ( 𝐼 ‘ 𝐶 ) ∈ ℂ )
93 1cnd ⊢ ( ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ 𝑗 ∈ ( 1 ... 𝐽 ) ) → 1 ∈ ℂ )
94 92 93 addcld ⊢ ( ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ 𝑗 ∈ ( 1 ... 𝐽 ) ) → ( ( 𝐼 ‘ 𝐶 ) + 1 ) ∈ ℂ )
95 simplr ⊢ ( ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ 𝑗 ∈ ( 1 ... 𝐽 ) ) → 𝑘 ∈ ℤ )
96 95 zcnd ⊢ ( ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ 𝑗 ∈ ( 1 ... 𝐽 ) ) → 𝑘 ∈ ℂ )
97 elfzelz ⊢ ( 𝑗 ∈ ( 1 ... 𝐽 ) → 𝑗 ∈ ℤ )
98 97 adantl ⊢ ( ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ 𝑗 ∈ ( 1 ... 𝐽 ) ) → 𝑗 ∈ ℤ )
99 98 zcnd ⊢ ( ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ 𝑗 ∈ ( 1 ... 𝐽 ) ) → 𝑗 ∈ ℂ )
100 subsub23 ⊢ ( ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) ∈ ℂ ∧ 𝑘 ∈ ℂ ∧ 𝑗 ∈ ℂ ) → ( ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑘 ) = 𝑗 ↔ ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑗 ) = 𝑘 ) )
101 94 96 99 100 syl3anc ⊢ ( ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ 𝑗 ∈ ( 1 ... 𝐽 ) ) → ( ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑘 ) = 𝑗 ↔ ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑗 ) = 𝑘 ) )
102 89 101 bitr3id ⊢ ( ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ 𝑗 ∈ ( 1 ... 𝐽 ) ) → ( 𝑗 = ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑘 ) ↔ ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑗 ) = 𝑘 ) )
103 simpll ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝐽 ) ) → 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) )
104 38 sselda ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝐽 ) ) → 𝑗 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) )
105 1 2 3 4 5 6 7 8 9 ballotlemsv ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝑗 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑗 ) = if ( 𝑗 ≤ ( 𝐼 ‘ 𝐶 ) , ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑗 ) , 𝑗 ) )
106 103 104 105 syl2anc ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝐽 ) ) → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑗 ) = if ( 𝑗 ≤ ( 𝐼 ‘ 𝐶 ) , ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑗 ) , 𝑗 ) )
107 97 adantl ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝐽 ) ) → 𝑗 ∈ ℤ )
108 107 zred ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝐽 ) ) → 𝑗 ∈ ℝ )
109 48 ad2antlr ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝐽 ) ) → 𝐽 ∈ ℤ )
110 109 zred ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝐽 ) ) → 𝐽 ∈ ℝ )
111 90 zred ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝐽 ) ) → ( 𝐼 ‘ 𝐶 ) ∈ ℝ )
112 elfzle2 ⊢ ( 𝑗 ∈ ( 1 ... 𝐽 ) → 𝑗 ≤ 𝐽 )
113 112 adantl ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝐽 ) ) → 𝑗 ≤ 𝐽 )
114 58 ad2antlr ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝐽 ) ) → 𝐽 ≤ ( 𝐼 ‘ 𝐶 ) )
115 108 110 111 113 114 letrd ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝐽 ) ) → 𝑗 ≤ ( 𝐼 ‘ 𝐶 ) )
116 iftrue ⊢ ( 𝑗 ≤ ( 𝐼 ‘ 𝐶 ) → if ( 𝑗 ≤ ( 𝐼 ‘ 𝐶 ) , ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑗 ) , 𝑗 ) = ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑗 ) )
117 115 116 syl ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝐽 ) ) → if ( 𝑗 ≤ ( 𝐼 ‘ 𝐶 ) , ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑗 ) , 𝑗 ) = ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑗 ) )
118 106 117 eqtrd ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝐽 ) ) → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑗 ) = ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑗 ) )
119 118 eqeq1d ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) ∧ 𝑗 ∈ ( 1 ... 𝐽 ) ) → ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑗 ) = 𝑘 ↔ ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑗 ) = 𝑘 ) )
120 119 adantlr ⊢ ( ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ 𝑗 ∈ ( 1 ... 𝐽 ) ) → ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑗 ) = 𝑘 ↔ ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑗 ) = 𝑘 ) )
121 102 120 bitr4d ⊢ ( ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ 𝑗 ∈ ( 1 ... 𝐽 ) ) → ( 𝑗 = ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑘 ) ↔ ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑗 ) = 𝑘 ) )
122 121 rexbidva ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) ∧ 𝑘 ∈ ℤ ) → ( ∃ 𝑗 ∈ ( 1 ... 𝐽 ) 𝑗 = ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑘 ) ↔ ∃ 𝑗 ∈ ( 1 ... 𝐽 ) ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑗 ) = 𝑘 ) )
123 86 88 122 3bitrd ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) ∧ 𝑘 ∈ ℤ ) → ( 𝑘 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ... ( 𝐼 ‘ 𝐶 ) ) ↔ ∃ 𝑗 ∈ ( 1 ... 𝐽 ) ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑗 ) = 𝑘 ) )
124 41 123 bitr4d ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) ∧ 𝑘 ∈ ℤ ) → ( 𝑘 ∈ ( ( 𝑆 ‘ 𝐶 ) “ ( 1 ... 𝐽 ) ) ↔ 𝑘 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ... ( 𝐼 ‘ 𝐶 ) ) ) )
125 22 24 124 eqrdav ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝐼 ‘ 𝐶 ) ) ) → ( ( 𝑆 ‘ 𝐶 ) “ ( 1 ... 𝐽 ) ) = ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) ... ( 𝐼 ‘ 𝐶 ) ) )