Proof of Theorem ballotlemsel1i
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 1zzd 12650 | . 2
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → 1 ∈
ℤ) | 
| 2 |  | ballotth.m | . . . . . 6
⊢ 𝑀 ∈ ℕ | 
| 3 |  | ballotth.n | . . . . . 6
⊢ 𝑁 ∈ ℕ | 
| 4 |  | ballotth.o | . . . . . 6
⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} | 
| 5 |  | ballotth.p | . . . . . 6
⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) | 
| 6 |  | ballotth.f | . . . . . 6
⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦
((♯‘((1...𝑖)
∩ 𝑐)) −
(♯‘((1...𝑖)
∖ 𝑐))))) | 
| 7 |  | ballotth.e | . . . . . 6
⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} | 
| 8 |  | ballotth.mgtn | . . . . . 6
⊢ 𝑁 < 𝑀 | 
| 9 |  | ballotth.i | . . . . . 6
⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < )) | 
| 10 | 2, 3, 4, 5, 6, 7, 8, 9 | ballotlemiex 34505 | . . . . 5
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ((𝐼‘𝐶) ∈ (1...(𝑀 + 𝑁)) ∧ ((𝐹‘𝐶)‘(𝐼‘𝐶)) = 0)) | 
| 11 | 10 | simpld 494 | . . . 4
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝐼‘𝐶) ∈ (1...(𝑀 + 𝑁))) | 
| 12 | 11 | elfzelzd 13566 | . . 3
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝐼‘𝐶) ∈ ℤ) | 
| 13 | 12 | adantr 480 | . 2
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → (𝐼‘𝐶) ∈ ℤ) | 
| 14 |  | nnaddcl 12290 | . . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 + 𝑁) ∈ ℕ) | 
| 15 | 2, 3, 14 | mp2an 692 | . . . . . . . . 9
⊢ (𝑀 + 𝑁) ∈ ℕ | 
| 16 | 15 | nnzi 12643 | . . . . . . . 8
⊢ (𝑀 + 𝑁) ∈ ℤ | 
| 17 | 16 | a1i 11 | . . . . . . 7
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝑀 + 𝑁) ∈ ℤ) | 
| 18 |  | elfzle2 13569 | . . . . . . . 8
⊢ ((𝐼‘𝐶) ∈ (1...(𝑀 + 𝑁)) → (𝐼‘𝐶) ≤ (𝑀 + 𝑁)) | 
| 19 | 11, 18 | syl 17 | . . . . . . 7
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝐼‘𝐶) ≤ (𝑀 + 𝑁)) | 
| 20 |  | eluz2 12885 | . . . . . . 7
⊢ ((𝑀 + 𝑁) ∈
(ℤ≥‘(𝐼‘𝐶)) ↔ ((𝐼‘𝐶) ∈ ℤ ∧ (𝑀 + 𝑁) ∈ ℤ ∧ (𝐼‘𝐶) ≤ (𝑀 + 𝑁))) | 
| 21 | 12, 17, 19, 20 | syl3anbrc 1343 | . . . . . 6
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝑀 + 𝑁) ∈
(ℤ≥‘(𝐼‘𝐶))) | 
| 22 |  | fzss2 13605 | . . . . . 6
⊢ ((𝑀 + 𝑁) ∈
(ℤ≥‘(𝐼‘𝐶)) → (1...(𝐼‘𝐶)) ⊆ (1...(𝑀 + 𝑁))) | 
| 23 | 21, 22 | syl 17 | . . . . 5
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (1...(𝐼‘𝐶)) ⊆ (1...(𝑀 + 𝑁))) | 
| 24 | 23 | sselda 3982 | . . . 4
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → 𝐽 ∈ (1...(𝑀 + 𝑁))) | 
| 25 |  | ballotth.s | . . . . 5
⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖))) | 
| 26 | 2, 3, 4, 5, 6, 7, 8, 9, 25 | ballotlemsdom 34515 | . . . 4
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) → ((𝑆‘𝐶)‘𝐽) ∈ (1...(𝑀 + 𝑁))) | 
| 27 | 24, 26 | syldan 591 | . . 3
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → ((𝑆‘𝐶)‘𝐽) ∈ (1...(𝑀 + 𝑁))) | 
| 28 | 27 | elfzelzd 13566 | . 2
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → ((𝑆‘𝐶)‘𝐽) ∈ ℤ) | 
| 29 |  | elfzelz 13565 | . . . . . 6
⊢ (𝐽 ∈ (1...(𝐼‘𝐶)) → 𝐽 ∈ ℤ) | 
| 30 | 29 | adantl 481 | . . . . 5
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → 𝐽 ∈ ℤ) | 
| 31 | 30 | zred 12724 | . . . 4
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → 𝐽 ∈ ℝ) | 
| 32 | 13 | zred 12724 | . . . . 5
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → (𝐼‘𝐶) ∈ ℝ) | 
| 33 |  | 1red 11263 | . . . . 5
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → 1 ∈
ℝ) | 
| 34 | 32, 33 | readdcld 11291 | . . . 4
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → ((𝐼‘𝐶) + 1) ∈ ℝ) | 
| 35 |  | elfzle2 13569 | . . . . . 6
⊢ (𝐽 ∈ (1...(𝐼‘𝐶)) → 𝐽 ≤ (𝐼‘𝐶)) | 
| 36 | 35 | adantl 481 | . . . . 5
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → 𝐽 ≤ (𝐼‘𝐶)) | 
| 37 | 13 | zcnd 12725 | . . . . . 6
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → (𝐼‘𝐶) ∈ ℂ) | 
| 38 |  | 1cnd 11257 | . . . . . 6
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → 1 ∈
ℂ) | 
| 39 | 37, 38 | pncand 11622 | . . . . 5
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → (((𝐼‘𝐶) + 1) − 1) = (𝐼‘𝐶)) | 
| 40 | 36, 39 | breqtrrd 5170 | . . . 4
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → 𝐽 ≤ (((𝐼‘𝐶) + 1) − 1)) | 
| 41 | 31, 34, 33, 40 | lesubd 11868 | . . 3
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → 1 ≤ (((𝐼‘𝐶) + 1) − 𝐽)) | 
| 42 | 2, 3, 4, 5, 6, 7, 8, 9, 25 | ballotlemsv 34513 | . . . . 5
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) → ((𝑆‘𝐶)‘𝐽) = if(𝐽 ≤ (𝐼‘𝐶), (((𝐼‘𝐶) + 1) − 𝐽), 𝐽)) | 
| 43 | 24, 42 | syldan 591 | . . . 4
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → ((𝑆‘𝐶)‘𝐽) = if(𝐽 ≤ (𝐼‘𝐶), (((𝐼‘𝐶) + 1) − 𝐽), 𝐽)) | 
| 44 | 36 | iftrued 4532 | . . . 4
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → if(𝐽 ≤ (𝐼‘𝐶), (((𝐼‘𝐶) + 1) − 𝐽), 𝐽) = (((𝐼‘𝐶) + 1) − 𝐽)) | 
| 45 | 43, 44 | eqtrd 2776 | . . 3
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → ((𝑆‘𝐶)‘𝐽) = (((𝐼‘𝐶) + 1) − 𝐽)) | 
| 46 | 41, 45 | breqtrrd 5170 | . 2
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → 1 ≤ ((𝑆‘𝐶)‘𝐽)) | 
| 47 | 12 | adantr 480 | . . . . 5
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) → (𝐼‘𝐶) ∈ ℤ) | 
| 48 |  | elfznn 13594 | . . . . . 6
⊢ (𝐽 ∈ (1...(𝑀 + 𝑁)) → 𝐽 ∈ ℕ) | 
| 49 | 48 | adantl 481 | . . . . 5
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) → 𝐽 ∈ ℕ) | 
| 50 | 47, 49 | ltesubnnd 32825 | . . . 4
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) → (((𝐼‘𝐶) + 1) − 𝐽) ≤ (𝐼‘𝐶)) | 
| 51 | 24, 50 | syldan 591 | . . 3
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → (((𝐼‘𝐶) + 1) − 𝐽) ≤ (𝐼‘𝐶)) | 
| 52 | 45, 51 | eqbrtrd 5164 | . 2
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → ((𝑆‘𝐶)‘𝐽) ≤ (𝐼‘𝐶)) | 
| 53 | 1, 13, 28, 46, 52 | elfzd 13556 | 1
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → ((𝑆‘𝐶)‘𝐽) ∈ (1...(𝐼‘𝐶))) |