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