| Step | Hyp | Ref
| Expression |
| 1 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑖 = 𝑘 → ((𝐹‘𝐶)‘𝑖) = ((𝐹‘𝐶)‘𝑘)) |
| 2 | 1 | breq2d 5155 |
. . . . . 6
⊢ (𝑖 = 𝑘 → (0 ≤ ((𝐹‘𝐶)‘𝑖) ↔ 0 ≤ ((𝐹‘𝐶)‘𝑘))) |
| 3 | 2 | elrab 3692 |
. . . . 5
⊢ (𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ↔ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) |
| 4 | 3 | anbi1i 624 |
. . . 4
⊢ ((𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘) ↔ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) |
| 5 | | simprl 771 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) → 𝑘 ∈ (1...𝐽)) |
| 6 | 5 | adantrr 717 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → 𝑘 ∈ (1...𝐽)) |
| 7 | | fzssuz 13605 |
. . . . . . . . . . . . . 14
⊢
(1...𝐽) ⊆
(ℤ≥‘1) |
| 8 | | uzssz 12899 |
. . . . . . . . . . . . . 14
⊢
(ℤ≥‘1) ⊆ ℤ |
| 9 | 7, 8 | sstri 3993 |
. . . . . . . . . . . . 13
⊢
(1...𝐽) ⊆
ℤ |
| 10 | | zssre 12620 |
. . . . . . . . . . . . 13
⊢ ℤ
⊆ ℝ |
| 11 | 9, 10 | sstri 3993 |
. . . . . . . . . . . 12
⊢
(1...𝐽) ⊆
ℝ |
| 12 | 11 | sseli 3979 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (1...𝐽) → 𝑘 ∈ ℝ) |
| 13 | 12 | ltp1d 12198 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (1...𝐽) → 𝑘 < (𝑘 + 1)) |
| 14 | | 1red 11262 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (1...𝐽) → 1 ∈ ℝ) |
| 15 | 12, 14 | readdcld 11290 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (1...𝐽) → (𝑘 + 1) ∈ ℝ) |
| 16 | 12, 15 | ltnled 11408 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (1...𝐽) → (𝑘 < (𝑘 + 1) ↔ ¬ (𝑘 + 1) ≤ 𝑘)) |
| 17 | 13, 16 | mpbid 232 |
. . . . . . . . 9
⊢ (𝑘 ∈ (1...𝐽) → ¬ (𝑘 + 1) ≤ 𝑘) |
| 18 | 6, 17 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → ¬ (𝑘 + 1) ≤ 𝑘) |
| 19 | | simprr 773 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘) |
| 20 | | ballotlemfcc.4 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐹‘𝐶)‘𝐽) < 0) |
| 21 | 20 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 = 𝐽) → ((𝐹‘𝐶)‘𝐽) < 0) |
| 22 | | simpr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 = 𝐽) → 𝑘 = 𝐽) |
| 23 | 22 | fveq2d 6910 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 = 𝐽) → ((𝐹‘𝐶)‘𝑘) = ((𝐹‘𝐶)‘𝐽)) |
| 24 | 23 | breq1d 5153 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 = 𝐽) → (((𝐹‘𝐶)‘𝑘) < 0 ↔ ((𝐹‘𝐶)‘𝐽) < 0)) |
| 25 | | ballotlemfcc.j |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝐽 ∈ ℕ) |
| 26 | | elnnuz 12922 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐽 ∈ ℕ ↔ 𝐽 ∈
(ℤ≥‘1)) |
| 27 | 25, 26 | sylib 218 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐽 ∈
(ℤ≥‘1)) |
| 28 | | eluzfz2 13572 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐽 ∈
(ℤ≥‘1) → 𝐽 ∈ (1...𝐽)) |
| 29 | 27, 28 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐽 ∈ (1...𝐽)) |
| 30 | | eleq1 2829 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝐽 → (𝑘 ∈ (1...𝐽) ↔ 𝐽 ∈ (1...𝐽))) |
| 31 | 29, 30 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑘 = 𝐽 → 𝑘 ∈ (1...𝐽))) |
| 32 | 31 | anc2li 555 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑘 = 𝐽 → (𝜑 ∧ 𝑘 ∈ (1...𝐽)))) |
| 33 | | 1eluzge0 12934 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 1 ∈
(ℤ≥‘0) |
| 34 | | fzss1 13603 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (1 ∈
(ℤ≥‘0) → (1...𝐽) ⊆ (0...𝐽)) |
| 35 | 34 | sseld 3982 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (1 ∈
(ℤ≥‘0) → (𝑘 ∈ (1...𝐽) → 𝑘 ∈ (0...𝐽))) |
| 36 | 33, 35 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ (1...𝐽) → 𝑘 ∈ (0...𝐽)) |
| 37 | | ballotth.m |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑀 ∈ ℕ |
| 38 | | ballotth.n |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑁 ∈ ℕ |
| 39 | | ballotth.o |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} |
| 40 | | ballotth.p |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) |
| 41 | | ballotth.f |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦
((♯‘((1...𝑖)
∩ 𝑐)) −
(♯‘((1...𝑖)
∖ 𝑐))))) |
| 42 | | ballotlemfcc.c |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝐶 ∈ 𝑂) |
| 43 | 42 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → 𝐶 ∈ 𝑂) |
| 44 | | elfzelz 13564 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℤ) |
| 45 | 44 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → 𝑘 ∈ ℤ) |
| 46 | 37, 38, 39, 40, 41, 43, 45 | ballotlemfelz 34493 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → ((𝐹‘𝐶)‘𝑘) ∈ ℤ) |
| 47 | 46 | zred 12722 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → ((𝐹‘𝐶)‘𝑘) ∈ ℝ) |
| 48 | | 0red 11264 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → 0 ∈ ℝ) |
| 49 | 47, 48 | ltnled 11408 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → (((𝐹‘𝐶)‘𝑘) < 0 ↔ ¬ 0 ≤ ((𝐹‘𝐶)‘𝑘))) |
| 50 | 36, 49 | sylan2 593 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐽)) → (((𝐹‘𝐶)‘𝑘) < 0 ↔ ¬ 0 ≤ ((𝐹‘𝐶)‘𝑘))) |
| 51 | 32, 50 | syl6 35 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑘 = 𝐽 → (((𝐹‘𝐶)‘𝑘) < 0 ↔ ¬ 0 ≤ ((𝐹‘𝐶)‘𝑘)))) |
| 52 | 51 | imp 406 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 = 𝐽) → (((𝐹‘𝐶)‘𝑘) < 0 ↔ ¬ 0 ≤ ((𝐹‘𝐶)‘𝑘))) |
| 53 | 24, 52 | bitr3d 281 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 = 𝐽) → (((𝐹‘𝐶)‘𝐽) < 0 ↔ ¬ 0 ≤ ((𝐹‘𝐶)‘𝑘))) |
| 54 | 21, 53 | mpbid 232 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 = 𝐽) → ¬ 0 ≤ ((𝐹‘𝐶)‘𝑘)) |
| 55 | 54 | ex 412 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑘 = 𝐽 → ¬ 0 ≤ ((𝐹‘𝐶)‘𝑘))) |
| 56 | 55 | con2d 134 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0 ≤ ((𝐹‘𝐶)‘𝑘) → ¬ 𝑘 = 𝐽)) |
| 57 | | nn1m1nn 12287 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐽 ∈ ℕ → (𝐽 = 1 ∨ (𝐽 − 1) ∈
ℕ)) |
| 58 | 25, 57 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐽 = 1 ∨ (𝐽 − 1) ∈
ℕ)) |
| 59 | | ballotlemfcc.3 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → ∃𝑖 ∈ (1...𝐽)0 ≤ ((𝐹‘𝐶)‘𝑖)) |
| 60 | 59 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝐽 = 1) → ∃𝑖 ∈ (1...𝐽)0 ≤ ((𝐹‘𝐶)‘𝑖)) |
| 61 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐽 = 1 → (𝐽...𝐽) = (1...𝐽)) |
| 62 | 61 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝐽 = 1) → (𝐽...𝐽) = (1...𝐽)) |
| 63 | 25 | nnzd 12640 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → 𝐽 ∈ ℤ) |
| 64 | | fzsn 13606 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐽 ∈ ℤ → (𝐽...𝐽) = {𝐽}) |
| 65 | 63, 64 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (𝐽...𝐽) = {𝐽}) |
| 66 | 65 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝐽 = 1) → (𝐽...𝐽) = {𝐽}) |
| 67 | 62, 66 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝐽 = 1) → (1...𝐽) = {𝐽}) |
| 68 | 60, 67 | rexeqtrdv 3329 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝐽 = 1) → ∃𝑖 ∈ {𝐽}0 ≤ ((𝐹‘𝐶)‘𝑖)) |
| 69 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑖 = 𝐽 → ((𝐹‘𝐶)‘𝑖) = ((𝐹‘𝐶)‘𝐽)) |
| 70 | 69 | breq2d 5155 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑖 = 𝐽 → (0 ≤ ((𝐹‘𝐶)‘𝑖) ↔ 0 ≤ ((𝐹‘𝐶)‘𝐽))) |
| 71 | 70 | rexsng 4676 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐽 ∈ ℕ →
(∃𝑖 ∈ {𝐽}0 ≤ ((𝐹‘𝐶)‘𝑖) ↔ 0 ≤ ((𝐹‘𝐶)‘𝐽))) |
| 72 | 25, 71 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (∃𝑖 ∈ {𝐽}0 ≤ ((𝐹‘𝐶)‘𝑖) ↔ 0 ≤ ((𝐹‘𝐶)‘𝐽))) |
| 73 | 72 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝐽 = 1) → (∃𝑖 ∈ {𝐽}0 ≤ ((𝐹‘𝐶)‘𝑖) ↔ 0 ≤ ((𝐹‘𝐶)‘𝐽))) |
| 74 | 68, 73 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝐽 = 1) → 0 ≤ ((𝐹‘𝐶)‘𝐽)) |
| 75 | 20 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝐽 = 1) → ((𝐹‘𝐶)‘𝐽) < 0) |
| 76 | 37, 38, 39, 40, 41, 42, 63 | ballotlemfelz 34493 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → ((𝐹‘𝐶)‘𝐽) ∈ ℤ) |
| 77 | 76 | zred 12722 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → ((𝐹‘𝐶)‘𝐽) ∈ ℝ) |
| 78 | | 0red 11264 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 0 ∈
ℝ) |
| 79 | 77, 78 | ltnled 11408 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (((𝐹‘𝐶)‘𝐽) < 0 ↔ ¬ 0 ≤ ((𝐹‘𝐶)‘𝐽))) |
| 80 | 79 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝐽 = 1) → (((𝐹‘𝐶)‘𝐽) < 0 ↔ ¬ 0 ≤ ((𝐹‘𝐶)‘𝐽))) |
| 81 | 75, 80 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝐽 = 1) → ¬ 0 ≤ ((𝐹‘𝐶)‘𝐽)) |
| 82 | 74, 81 | pm2.65da 817 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ¬ 𝐽 = 1) |
| 83 | | biortn 938 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (¬
𝐽 = 1 → ((𝐽 − 1) ∈ ℕ
↔ (¬ ¬ 𝐽 = 1
∨ (𝐽 − 1) ∈
ℕ))) |
| 84 | 82, 83 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝐽 − 1) ∈ ℕ ↔ (¬
¬ 𝐽 = 1 ∨ (𝐽 − 1) ∈
ℕ))) |
| 85 | | notnotb 315 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐽 = 1 ↔ ¬ ¬ 𝐽 = 1) |
| 86 | 85 | orbi1i 914 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐽 = 1 ∨ (𝐽 − 1) ∈ ℕ) ↔ (¬
¬ 𝐽 = 1 ∨ (𝐽 − 1) ∈
ℕ)) |
| 87 | 84, 86 | bitr4di 289 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝐽 − 1) ∈ ℕ ↔ (𝐽 = 1 ∨ (𝐽 − 1) ∈
ℕ))) |
| 88 | 58, 87 | mpbird 257 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐽 − 1) ∈ ℕ) |
| 89 | | elnnuz 12922 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐽 − 1) ∈ ℕ
↔ (𝐽 − 1) ∈
(ℤ≥‘1)) |
| 90 | 88, 89 | sylib 218 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐽 − 1) ∈
(ℤ≥‘1)) |
| 91 | | elfzp1 13614 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐽 − 1) ∈
(ℤ≥‘1) → (𝑘 ∈ (1...((𝐽 − 1) + 1)) ↔ (𝑘 ∈ (1...(𝐽 − 1)) ∨ 𝑘 = ((𝐽 − 1) + 1)))) |
| 92 | 90, 91 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑘 ∈ (1...((𝐽 − 1) + 1)) ↔ (𝑘 ∈ (1...(𝐽 − 1)) ∨ 𝑘 = ((𝐽 − 1) + 1)))) |
| 93 | 25 | nncnd 12282 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐽 ∈ ℂ) |
| 94 | | 1cnd 11256 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 1 ∈
ℂ) |
| 95 | 93, 94 | npcand 11624 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝐽 − 1) + 1) = 𝐽) |
| 96 | 95 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (1...((𝐽 − 1) + 1)) = (1...𝐽)) |
| 97 | 96 | eleq2d 2827 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑘 ∈ (1...((𝐽 − 1) + 1)) ↔ 𝑘 ∈ (1...𝐽))) |
| 98 | 95 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑘 = ((𝐽 − 1) + 1) ↔ 𝑘 = 𝐽)) |
| 99 | 98 | orbi2d 916 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑘 ∈ (1...(𝐽 − 1)) ∨ 𝑘 = ((𝐽 − 1) + 1)) ↔ (𝑘 ∈ (1...(𝐽 − 1)) ∨ 𝑘 = 𝐽))) |
| 100 | 92, 97, 99 | 3bitr3d 309 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑘 ∈ (1...𝐽) ↔ (𝑘 ∈ (1...(𝐽 − 1)) ∨ 𝑘 = 𝐽))) |
| 101 | | orcom 871 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ (1...(𝐽 − 1)) ∨ 𝑘 = 𝐽) ↔ (𝑘 = 𝐽 ∨ 𝑘 ∈ (1...(𝐽 − 1)))) |
| 102 | 100, 101 | bitrdi 287 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑘 ∈ (1...𝐽) ↔ (𝑘 = 𝐽 ∨ 𝑘 ∈ (1...(𝐽 − 1))))) |
| 103 | 102 | biimpd 229 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑘 ∈ (1...𝐽) → (𝑘 = 𝐽 ∨ 𝑘 ∈ (1...(𝐽 − 1))))) |
| 104 | | pm5.6 1004 |
. . . . . . . . . . . . . 14
⊢ (((𝑘 ∈ (1...𝐽) ∧ ¬ 𝑘 = 𝐽) → 𝑘 ∈ (1...(𝐽 − 1))) ↔ (𝑘 ∈ (1...𝐽) → (𝑘 = 𝐽 ∨ 𝑘 ∈ (1...(𝐽 − 1))))) |
| 105 | 103, 104 | sylibr 234 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑘 ∈ (1...𝐽) ∧ ¬ 𝑘 = 𝐽) → 𝑘 ∈ (1...(𝐽 − 1)))) |
| 106 | 88 | nnzd 12640 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐽 − 1) ∈ ℤ) |
| 107 | | 1z 12647 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℤ |
| 108 | 106, 107 | jctil 519 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (1 ∈ ℤ ∧
(𝐽 − 1) ∈
ℤ)) |
| 109 | | elfzelz 13564 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ (1...(𝐽 − 1)) → 𝑘 ∈ ℤ) |
| 110 | 109, 107 | jctir 520 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ (1...(𝐽 − 1)) → (𝑘 ∈ ℤ ∧ 1 ∈
ℤ)) |
| 111 | | fzaddel 13598 |
. . . . . . . . . . . . . . . . . 18
⊢ (((1
∈ ℤ ∧ (𝐽
− 1) ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ 1 ∈ ℤ))
→ (𝑘 ∈
(1...(𝐽 − 1)) ↔
(𝑘 + 1) ∈ ((1 +
1)...((𝐽 − 1) +
1)))) |
| 112 | 108, 110,
111 | syl2an 596 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐽 − 1))) → (𝑘 ∈ (1...(𝐽 − 1)) ↔ (𝑘 + 1) ∈ ((1 + 1)...((𝐽 − 1) + 1)))) |
| 113 | 112 | biimp3a 1471 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐽 − 1)) ∧ 𝑘 ∈ (1...(𝐽 − 1))) → (𝑘 + 1) ∈ ((1 + 1)...((𝐽 − 1) + 1))) |
| 114 | 113 | 3anidm23 1423 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐽 − 1))) → (𝑘 + 1) ∈ ((1 + 1)...((𝐽 − 1) + 1))) |
| 115 | | 1p1e2 12391 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (1 + 1) =
2 |
| 116 | 115 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (1 + 1) =
2) |
| 117 | 116, 95 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((1 + 1)...((𝐽 − 1) + 1)) = (2...𝐽)) |
| 118 | 117 | eleq2d 2827 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑘 + 1) ∈ ((1 + 1)...((𝐽 − 1) + 1)) ↔ (𝑘 + 1) ∈ (2...𝐽))) |
| 119 | | 2eluzge1 12936 |
. . . . . . . . . . . . . . . . . . 19
⊢ 2 ∈
(ℤ≥‘1) |
| 120 | | fzss1 13603 |
. . . . . . . . . . . . . . . . . . 19
⊢ (2 ∈
(ℤ≥‘1) → (2...𝐽) ⊆ (1...𝐽)) |
| 121 | 119, 120 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢
(2...𝐽) ⊆
(1...𝐽) |
| 122 | 121 | sseli 3979 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 + 1) ∈ (2...𝐽) → (𝑘 + 1) ∈ (1...𝐽)) |
| 123 | 118, 122 | biimtrdi 253 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑘 + 1) ∈ ((1 + 1)...((𝐽 − 1) + 1)) → (𝑘 + 1) ∈ (1...𝐽))) |
| 124 | 123 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐽 − 1))) → ((𝑘 + 1) ∈ ((1 + 1)...((𝐽 − 1) + 1)) → (𝑘 + 1) ∈ (1...𝐽))) |
| 125 | 114, 124 | mpd 15 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐽 − 1))) → (𝑘 + 1) ∈ (1...𝐽)) |
| 126 | 125 | ex 412 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑘 ∈ (1...(𝐽 − 1)) → (𝑘 + 1) ∈ (1...𝐽))) |
| 127 | 105, 126 | syld 47 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑘 ∈ (1...𝐽) ∧ ¬ 𝑘 = 𝐽) → (𝑘 + 1) ∈ (1...𝐽))) |
| 128 | 56, 127 | sylan2d 605 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) → (𝑘 + 1) ∈ (1...𝐽))) |
| 129 | 128 | imp 406 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) → (𝑘 + 1) ∈ (1...𝐽)) |
| 130 | 129 | adantrr 717 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → (𝑘 + 1) ∈ (1...𝐽)) |
| 131 | | fveq2 6906 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = (𝑘 + 1) → ((𝐹‘𝐶)‘𝑖) = ((𝐹‘𝐶)‘(𝑘 + 1))) |
| 132 | 131 | breq2d 5155 |
. . . . . . . . . . . . 13
⊢ (𝑖 = (𝑘 + 1) → (0 ≤ ((𝐹‘𝐶)‘𝑖) ↔ 0 ≤ ((𝐹‘𝐶)‘(𝑘 + 1)))) |
| 133 | 132 | elrab 3692 |
. . . . . . . . . . . 12
⊢ ((𝑘 + 1) ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ↔ ((𝑘 + 1) ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘(𝑘 + 1)))) |
| 134 | | breq1 5146 |
. . . . . . . . . . . . 13
⊢ (𝑗 = (𝑘 + 1) → (𝑗 ≤ 𝑘 ↔ (𝑘 + 1) ≤ 𝑘)) |
| 135 | 134 | rspccva 3621 |
. . . . . . . . . . . 12
⊢
((∀𝑗 ∈
{𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘 ∧ (𝑘 + 1) ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}) → (𝑘 + 1) ≤ 𝑘) |
| 136 | 133, 135 | sylan2br 595 |
. . . . . . . . . . 11
⊢
((∀𝑗 ∈
{𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘 ∧ ((𝑘 + 1) ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘(𝑘 + 1)))) → (𝑘 + 1) ≤ 𝑘) |
| 137 | 136 | expr 456 |
. . . . . . . . . 10
⊢
((∀𝑗 ∈
{𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘 ∧ (𝑘 + 1) ∈ (1...𝐽)) → (0 ≤ ((𝐹‘𝐶)‘(𝑘 + 1)) → (𝑘 + 1) ≤ 𝑘)) |
| 138 | 137 | con3d 152 |
. . . . . . . . 9
⊢
((∀𝑗 ∈
{𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘 ∧ (𝑘 + 1) ∈ (1...𝐽)) → (¬ (𝑘 + 1) ≤ 𝑘 → ¬ 0 ≤ ((𝐹‘𝐶)‘(𝑘 + 1)))) |
| 139 | 19, 130, 138 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → (¬ (𝑘 + 1) ≤ 𝑘 → ¬ 0 ≤ ((𝐹‘𝐶)‘(𝑘 + 1)))) |
| 140 | 18, 139 | mpd 15 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → ¬ 0 ≤ ((𝐹‘𝐶)‘(𝑘 + 1))) |
| 141 | | simplrr 778 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) ∧ (𝑘 + 1) ∈ 𝐶) → ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘) |
| 142 | 130 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) ∧ (𝑘 + 1) ∈ 𝐶) → (𝑘 + 1) ∈ (1...𝐽)) |
| 143 | | 0red 11264 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) ∧ (𝑘 + 1) ∈ 𝐶) → 0 ∈ ℝ) |
| 144 | | simpll 767 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) ∧ (𝑘 + 1) ∈ 𝐶) → 𝜑) |
| 145 | 129 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) ∧ (𝑘 + 1) ∈ 𝐶) → (𝑘 + 1) ∈ (1...𝐽)) |
| 146 | 34 | sseld 3982 |
. . . . . . . . . . . . . . 15
⊢ (1 ∈
(ℤ≥‘0) → ((𝑘 + 1) ∈ (1...𝐽) → (𝑘 + 1) ∈ (0...𝐽))) |
| 147 | 33, 145, 146 | mpsyl 68 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) ∧ (𝑘 + 1) ∈ 𝐶) → (𝑘 + 1) ∈ (0...𝐽)) |
| 148 | 42 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (0...𝐽)) → 𝐶 ∈ 𝑂) |
| 149 | | elfzelz 13564 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 + 1) ∈ (0...𝐽) → (𝑘 + 1) ∈ ℤ) |
| 150 | 149 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (0...𝐽)) → (𝑘 + 1) ∈ ℤ) |
| 151 | 37, 38, 39, 40, 41, 148, 150 | ballotlemfelz 34493 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (0...𝐽)) → ((𝐹‘𝐶)‘(𝑘 + 1)) ∈ ℤ) |
| 152 | 151 | zred 12722 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (0...𝐽)) → ((𝐹‘𝐶)‘(𝑘 + 1)) ∈ ℝ) |
| 153 | 144, 147,
152 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) ∧ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) ∈ ℝ) |
| 154 | | simplrr 778 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) ∧ (𝑘 + 1) ∈ 𝐶) → 0 ≤ ((𝐹‘𝐶)‘𝑘)) |
| 155 | 5 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) ∧ (𝑘 + 1) ∈ 𝐶) → 𝑘 ∈ (1...𝐽)) |
| 156 | 155, 36 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) ∧ (𝑘 + 1) ∈ 𝐶) → 𝑘 ∈ (0...𝐽)) |
| 157 | 128 | imdistani 568 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) → (𝜑 ∧ (𝑘 + 1) ∈ (1...𝐽))) |
| 158 | 42 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (1...𝐽)) → 𝐶 ∈ 𝑂) |
| 159 | | elfznn 13593 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 + 1) ∈ (1...𝐽) → (𝑘 + 1) ∈ ℕ) |
| 160 | 159 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (1...𝐽)) → (𝑘 + 1) ∈ ℕ) |
| 161 | 37, 38, 39, 40, 41, 158, 160 | ballotlemfp1 34494 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (1...𝐽)) → ((¬ (𝑘 + 1) ∈ 𝐶 → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) − 1)) ∧ ((𝑘 + 1) ∈ 𝐶 → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) + 1)))) |
| 162 | 161 | simprd 495 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (1...𝐽)) → ((𝑘 + 1) ∈ 𝐶 → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) + 1))) |
| 163 | 162 | imp 406 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑘 + 1) ∈ (1...𝐽)) ∧ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) + 1)) |
| 164 | 157, 163 | sylan 580 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) ∧ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) + 1)) |
| 165 | | elfzelz 13564 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 ∈ (1...𝐽) → 𝑘 ∈ ℤ) |
| 166 | 165 | zcnd 12723 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ (1...𝐽) → 𝑘 ∈ ℂ) |
| 167 | | 1cnd 11256 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ (1...𝐽) → 1 ∈ ℂ) |
| 168 | 166, 167 | pncand 11621 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ (1...𝐽) → ((𝑘 + 1) − 1) = 𝑘) |
| 169 | 168 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ (1...𝐽) → ((𝐹‘𝐶)‘((𝑘 + 1) − 1)) = ((𝐹‘𝐶)‘𝑘)) |
| 170 | 169 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ (1...𝐽) → (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) + 1) = (((𝐹‘𝐶)‘𝑘) + 1)) |
| 171 | 170 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ (1...𝐽) → (((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) + 1) ↔ ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) + 1))) |
| 172 | 155, 171 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) ∧ (𝑘 + 1) ∈ 𝐶) → (((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) + 1) ↔ ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) + 1))) |
| 173 | 164, 172 | mpbid 232 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) ∧ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) + 1)) |
| 174 | | 0z 12624 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 ∈
ℤ |
| 175 | | zleltp1 12668 |
. . . . . . . . . . . . . . . . . 18
⊢ ((0
∈ ℤ ∧ ((𝐹‘𝐶)‘𝑘) ∈ ℤ) → (0 ≤ ((𝐹‘𝐶)‘𝑘) ↔ 0 < (((𝐹‘𝐶)‘𝑘) + 1))) |
| 176 | 174, 46, 175 | sylancr 587 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → (0 ≤ ((𝐹‘𝐶)‘𝑘) ↔ 0 < (((𝐹‘𝐶)‘𝑘) + 1))) |
| 177 | 176 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽)) ∧ ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) + 1)) → (0 ≤ ((𝐹‘𝐶)‘𝑘) ↔ 0 < (((𝐹‘𝐶)‘𝑘) + 1))) |
| 178 | | breq2 5147 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) + 1) → (0 < ((𝐹‘𝐶)‘(𝑘 + 1)) ↔ 0 < (((𝐹‘𝐶)‘𝑘) + 1))) |
| 179 | 178 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽)) ∧ ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) + 1)) → (0 < ((𝐹‘𝐶)‘(𝑘 + 1)) ↔ 0 < (((𝐹‘𝐶)‘𝑘) + 1))) |
| 180 | 177, 179 | bitr4d 282 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽)) ∧ ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) + 1)) → (0 ≤ ((𝐹‘𝐶)‘𝑘) ↔ 0 < ((𝐹‘𝐶)‘(𝑘 + 1)))) |
| 181 | 144, 156,
173, 180 | syl21anc 838 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) ∧ (𝑘 + 1) ∈ 𝐶) → (0 ≤ ((𝐹‘𝐶)‘𝑘) ↔ 0 < ((𝐹‘𝐶)‘(𝑘 + 1)))) |
| 182 | 154, 181 | mpbid 232 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) ∧ (𝑘 + 1) ∈ 𝐶) → 0 < ((𝐹‘𝐶)‘(𝑘 + 1))) |
| 183 | 143, 153,
182 | ltled 11409 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) ∧ (𝑘 + 1) ∈ 𝐶) → 0 ≤ ((𝐹‘𝐶)‘(𝑘 + 1))) |
| 184 | 183 | adantlrr 721 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) ∧ (𝑘 + 1) ∈ 𝐶) → 0 ≤ ((𝐹‘𝐶)‘(𝑘 + 1))) |
| 185 | 141, 142,
184, 136 | syl12anc 837 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) ∧ (𝑘 + 1) ∈ 𝐶) → (𝑘 + 1) ≤ 𝑘) |
| 186 | 18, 185 | mtand 816 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → ¬ (𝑘 + 1) ∈ 𝐶) |
| 187 | 161 | simpld 494 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (1...𝐽)) → (¬ (𝑘 + 1) ∈ 𝐶 → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) −
1))) |
| 188 | 187 | imp 406 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑘 + 1) ∈ (1...𝐽)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) −
1)) |
| 189 | 157, 188 | sylan 580 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) −
1)) |
| 190 | 5 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → 𝑘 ∈ (1...𝐽)) |
| 191 | 169 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (1...𝐽) → (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) − 1) = (((𝐹‘𝐶)‘𝑘) − 1)) |
| 192 | 191 | eqeq2d 2748 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (1...𝐽) → (((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) − 1) ↔ ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) − 1))) |
| 193 | 190, 192 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → (((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) − 1) ↔ ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) − 1))) |
| 194 | 189, 193 | mpbid 232 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) − 1)) |
| 195 | 194 | adantlrr 721 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) − 1)) |
| 196 | 186, 195 | mpdan 687 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) − 1)) |
| 197 | | breq2 5147 |
. . . . . . . . 9
⊢ (((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) − 1) → (0 ≤ ((𝐹‘𝐶)‘(𝑘 + 1)) ↔ 0 ≤ (((𝐹‘𝐶)‘𝑘) − 1))) |
| 198 | 197 | notbid 318 |
. . . . . . . 8
⊢ (((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) − 1) → (¬ 0 ≤ ((𝐹‘𝐶)‘(𝑘 + 1)) ↔ ¬ 0 ≤ (((𝐹‘𝐶)‘𝑘) − 1))) |
| 199 | 196, 198 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → (¬ 0 ≤ ((𝐹‘𝐶)‘(𝑘 + 1)) ↔ ¬ 0 ≤ (((𝐹‘𝐶)‘𝑘) − 1))) |
| 200 | 140, 199 | mpbid 232 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → ¬ 0 ≤ (((𝐹‘𝐶)‘𝑘) − 1)) |
| 201 | 5, 36 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) → 𝑘 ∈ (0...𝐽)) |
| 202 | 201, 46 | syldan 591 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘))) → ((𝐹‘𝐶)‘𝑘) ∈ ℤ) |
| 203 | 202 | adantrr 717 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → ((𝐹‘𝐶)‘𝑘) ∈ ℤ) |
| 204 | | zlem1lt 12669 |
. . . . . . . . 9
⊢ ((((𝐹‘𝐶)‘𝑘) ∈ ℤ ∧ 0 ∈ ℤ)
→ (((𝐹‘𝐶)‘𝑘) ≤ 0 ↔ (((𝐹‘𝐶)‘𝑘) − 1) < 0)) |
| 205 | 174, 204 | mpan2 691 |
. . . . . . . 8
⊢ (((𝐹‘𝐶)‘𝑘) ∈ ℤ → (((𝐹‘𝐶)‘𝑘) ≤ 0 ↔ (((𝐹‘𝐶)‘𝑘) − 1) < 0)) |
| 206 | | zre 12617 |
. . . . . . . . . 10
⊢ (((𝐹‘𝐶)‘𝑘) ∈ ℤ → ((𝐹‘𝐶)‘𝑘) ∈ ℝ) |
| 207 | | 1red 11262 |
. . . . . . . . . 10
⊢ (((𝐹‘𝐶)‘𝑘) ∈ ℤ → 1 ∈
ℝ) |
| 208 | 206, 207 | resubcld 11691 |
. . . . . . . . 9
⊢ (((𝐹‘𝐶)‘𝑘) ∈ ℤ → (((𝐹‘𝐶)‘𝑘) − 1) ∈ ℝ) |
| 209 | | 0red 11264 |
. . . . . . . . 9
⊢ (((𝐹‘𝐶)‘𝑘) ∈ ℤ → 0 ∈
ℝ) |
| 210 | 208, 209 | ltnled 11408 |
. . . . . . . 8
⊢ (((𝐹‘𝐶)‘𝑘) ∈ ℤ → ((((𝐹‘𝐶)‘𝑘) − 1) < 0 ↔ ¬ 0 ≤
(((𝐹‘𝐶)‘𝑘) − 1))) |
| 211 | 205, 210 | bitrd 279 |
. . . . . . 7
⊢ (((𝐹‘𝐶)‘𝑘) ∈ ℤ → (((𝐹‘𝐶)‘𝑘) ≤ 0 ↔ ¬ 0 ≤ (((𝐹‘𝐶)‘𝑘) − 1))) |
| 212 | 203, 211 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → (((𝐹‘𝐶)‘𝑘) ≤ 0 ↔ ¬ 0 ≤ (((𝐹‘𝐶)‘𝑘) − 1))) |
| 213 | 200, 212 | mpbird 257 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → ((𝐹‘𝐶)‘𝑘) ≤ 0) |
| 214 | | simprlr 780 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → 0 ≤ ((𝐹‘𝐶)‘𝑘)) |
| 215 | 203 | zred 12722 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → ((𝐹‘𝐶)‘𝑘) ∈ ℝ) |
| 216 | | 0red 11264 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → 0 ∈ ℝ) |
| 217 | 215, 216 | letri3d 11403 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → (((𝐹‘𝐶)‘𝑘) = 0 ↔ (((𝐹‘𝐶)‘𝑘) ≤ 0 ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)))) |
| 218 | 213, 214,
217 | mpbir2and 713 |
. . . 4
⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → ((𝐹‘𝐶)‘𝑘) = 0) |
| 219 | 4, 218 | sylan2b 594 |
. . 3
⊢ ((𝜑 ∧ (𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘)) → ((𝐹‘𝐶)‘𝑘) = 0) |
| 220 | | ssrab2 4080 |
. . . . . 6
⊢ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ⊆ (1...𝐽) |
| 221 | 220, 11 | sstri 3993 |
. . . . 5
⊢ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ⊆ ℝ |
| 222 | 221 | a1i 11 |
. . . 4
⊢ (𝜑 → {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ⊆ ℝ) |
| 223 | | fzfi 14013 |
. . . . . 6
⊢
(1...𝐽) ∈
Fin |
| 224 | | ssfi 9213 |
. . . . . 6
⊢
(((1...𝐽) ∈ Fin
∧ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ⊆ (1...𝐽)) → {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ∈ Fin) |
| 225 | 223, 220,
224 | mp2an 692 |
. . . . 5
⊢ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ∈ Fin |
| 226 | 225 | a1i 11 |
. . . 4
⊢ (𝜑 → {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ∈ Fin) |
| 227 | | rabn0 4389 |
. . . . 5
⊢ ({𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ≠ ∅ ↔ ∃𝑖 ∈ (1...𝐽)0 ≤ ((𝐹‘𝐶)‘𝑖)) |
| 228 | 59, 227 | sylibr 234 |
. . . 4
⊢ (𝜑 → {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ≠ ∅) |
| 229 | | fimaxre 12212 |
. . . 4
⊢ (({𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ⊆ ℝ ∧ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ∈ Fin ∧ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ≠ ∅) → ∃𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘) |
| 230 | 222, 226,
228, 229 | syl3anc 1373 |
. . 3
⊢ (𝜑 → ∃𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)}𝑗 ≤ 𝑘) |
| 231 | 219, 230 | reximddv 3171 |
. 2
⊢ (𝜑 → ∃𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ((𝐹‘𝐶)‘𝑘) = 0) |
| 232 | | elrabi 3687 |
. . . 4
⊢ (𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} → 𝑘 ∈ (1...𝐽)) |
| 233 | 232 | anim1i 615 |
. . 3
⊢ ((𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ∧ ((𝐹‘𝐶)‘𝑘) = 0) → (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) = 0)) |
| 234 | 233 | reximi2 3079 |
. 2
⊢
(∃𝑘 ∈
{𝑖 ∈ (1...𝐽) ∣ 0 ≤ ((𝐹‘𝐶)‘𝑖)} ((𝐹‘𝐶)‘𝑘) = 0 → ∃𝑘 ∈ (1...𝐽)((𝐹‘𝐶)‘𝑘) = 0) |
| 235 | 231, 234 | syl 17 |
1
⊢ (𝜑 → ∃𝑘 ∈ (1...𝐽)((𝐹‘𝐶)‘𝑘) = 0) |