Step | Hyp | Ref
| Expression |
1 | | fveq2 6717 |
. . . . . . 7
⊢ (𝑖 = 𝑘 → ((𝐹‘𝐶)‘𝑖) = ((𝐹‘𝐶)‘𝑘)) |
2 | 1 | breq1d 5063 |
. . . . . 6
⊢ (𝑖 = 𝑘 → (((𝐹‘𝐶)‘𝑖) ≤ 0 ↔ ((𝐹‘𝐶)‘𝑘) ≤ 0)) |
3 | 2 | elrab 3602 |
. . . . 5
⊢ (𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ↔ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) |
4 | 3 | anbi1i 627 |
. . . 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 13153 |
. . . . . . . . . . . . . 14
⊢
(1...𝐽) ⊆
(ℤ≥‘1) |
9 | | uzssz 12459 |
. . . . . . . . . . . . . 14
⊢
(ℤ≥‘1) ⊆ ℤ |
10 | 8, 9 | sstri 3910 |
. . . . . . . . . . . . 13
⊢
(1...𝐽) ⊆
ℤ |
11 | | zssre 12183 |
. . . . . . . . . . . . 13
⊢ ℤ
⊆ ℝ |
12 | 10, 11 | sstri 3910 |
. . . . . . . . . . . 12
⊢
(1...𝐽) ⊆
ℝ |
13 | 12 | sseli 3896 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (1...𝐽) → 𝑘 ∈ ℝ) |
14 | 13 | ltp1d 11762 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (1...𝐽) → 𝑘 < (𝑘 + 1)) |
15 | | 1red 10834 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (1...𝐽) → 1 ∈ ℝ) |
16 | 13, 15 | readdcld 10862 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (1...𝐽) → (𝑘 + 1) ∈ ℝ) |
17 | 13, 16 | ltnled 10979 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (1...𝐽) → (𝑘 < (𝑘 + 1) ↔ ¬ (𝑘 + 1) ≤ 𝑘)) |
18 | 14, 17 | mpbid 235 |
. . . . . . . . 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 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 = 𝐽) → 0 < ((𝐹‘𝐶)‘𝐽)) |
23 | | simpr 488 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 = 𝐽) → 𝑘 = 𝐽) |
24 | 23 | fveq2d 6721 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 = 𝐽) → ((𝐹‘𝐶)‘𝑘) = ((𝐹‘𝐶)‘𝐽)) |
25 | 24 | breq2d 5065 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 = 𝐽) → (0 < ((𝐹‘𝐶)‘𝑘) ↔ 0 < ((𝐹‘𝐶)‘𝐽))) |
26 | | ballotlemfp1.j |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝐽 ∈ ℕ) |
27 | | elnnuz 12478 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐽 ∈ ℕ ↔ 𝐽 ∈
(ℤ≥‘1)) |
28 | 26, 27 | sylib 221 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐽 ∈
(ℤ≥‘1)) |
29 | | eluzfz2 13120 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐽 ∈
(ℤ≥‘1) → 𝐽 ∈ (1...𝐽)) |
30 | 28, 29 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐽 ∈ (1...𝐽)) |
31 | | eleq1 2825 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝐽 → (𝑘 ∈ (1...𝐽) ↔ 𝐽 ∈ (1...𝐽))) |
32 | 30, 31 | syl5ibrcom 250 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑘 = 𝐽 → 𝑘 ∈ (1...𝐽))) |
33 | 32 | anc2li 559 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑘 = 𝐽 → (𝜑 ∧ 𝑘 ∈ (1...𝐽)))) |
34 | | 1eluzge0 12488 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 1 ∈
(ℤ≥‘0) |
35 | | fzss1 13151 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (1 ∈
(ℤ≥‘0) → (1...𝐽) ⊆ (0...𝐽)) |
36 | 35 | sseld 3900 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (1 ∈
(ℤ≥‘0) → (𝑘 ∈ (1...𝐽) → 𝑘 ∈ (0...𝐽))) |
37 | 34, 36 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ (1...𝐽) → 𝑘 ∈ (0...𝐽)) |
38 | | 0red 10836 |
. . . . . . . . . . . . . . . . . . . 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 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → 𝐶 ∈ 𝑂) |
46 | | elfzelz 13112 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℤ) |
47 | 46 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → 𝑘 ∈ ℤ) |
48 | 39, 40, 41, 42, 43, 45, 47 | ballotlemfelz 32169 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → ((𝐹‘𝐶)‘𝑘) ∈ ℤ) |
49 | 48 | zred 12282 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → ((𝐹‘𝐶)‘𝑘) ∈ ℝ) |
50 | 38, 49 | ltnled 10979 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → (0 < ((𝐹‘𝐶)‘𝑘) ↔ ¬ ((𝐹‘𝐶)‘𝑘) ≤ 0)) |
51 | 37, 50 | sylan2 596 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝐽)) → (0 < ((𝐹‘𝐶)‘𝑘) ↔ ¬ ((𝐹‘𝐶)‘𝑘) ≤ 0)) |
52 | 33, 51 | syl6 35 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑘 = 𝐽 → (0 < ((𝐹‘𝐶)‘𝑘) ↔ ¬ ((𝐹‘𝐶)‘𝑘) ≤ 0))) |
53 | 52 | imp 410 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 = 𝐽) → (0 < ((𝐹‘𝐶)‘𝑘) ↔ ¬ ((𝐹‘𝐶)‘𝑘) ≤ 0)) |
54 | 25, 53 | bitr3d 284 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 = 𝐽) → (0 < ((𝐹‘𝐶)‘𝐽) ↔ ¬ ((𝐹‘𝐶)‘𝑘) ≤ 0)) |
55 | 22, 54 | mpbid 235 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 = 𝐽) → ¬ ((𝐹‘𝐶)‘𝑘) ≤ 0) |
56 | 55 | ex 416 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑘 = 𝐽 → ¬ ((𝐹‘𝐶)‘𝑘) ≤ 0)) |
57 | 56 | con2d 136 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝐹‘𝐶)‘𝑘) ≤ 0 → ¬ 𝑘 = 𝐽)) |
58 | | nn1m1nn 11851 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐽 ∈ ℕ → (𝐽 = 1 ∨ (𝐽 − 1) ∈
ℕ)) |
59 | 26, 58 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐽 = 1 ∨ (𝐽 − 1) ∈
ℕ)) |
60 | | ballotlemfc0.3 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → ∃𝑖 ∈ (1...𝐽)((𝐹‘𝐶)‘𝑖) ≤ 0) |
61 | 60 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝐽 = 1) → ∃𝑖 ∈ (1...𝐽)((𝐹‘𝐶)‘𝑖) ≤ 0) |
62 | | oveq1 7220 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐽 = 1 → (𝐽...𝐽) = (1...𝐽)) |
63 | 62 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝐽 = 1) → (𝐽...𝐽) = (1...𝐽)) |
64 | 26 | nnzd 12281 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → 𝐽 ∈ ℤ) |
65 | | fzsn 13154 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝐽 ∈ ℤ → (𝐽...𝐽) = {𝐽}) |
66 | 64, 65 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → (𝐽...𝐽) = {𝐽}) |
67 | 66 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝐽 = 1) → (𝐽...𝐽) = {𝐽}) |
68 | 63, 67 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝐽 = 1) → (1...𝐽) = {𝐽}) |
69 | 68 | rexeqdv 3326 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝐽 = 1) → (∃𝑖 ∈ (1...𝐽)((𝐹‘𝐶)‘𝑖) ≤ 0 ↔ ∃𝑖 ∈ {𝐽} ((𝐹‘𝐶)‘𝑖) ≤ 0)) |
70 | 61, 69 | mpbid 235 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝐽 = 1) → ∃𝑖 ∈ {𝐽} ((𝐹‘𝐶)‘𝑖) ≤ 0) |
71 | | fveq2 6717 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑖 = 𝐽 → ((𝐹‘𝐶)‘𝑖) = ((𝐹‘𝐶)‘𝐽)) |
72 | 71 | breq1d 5063 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑖 = 𝐽 → (((𝐹‘𝐶)‘𝑖) ≤ 0 ↔ ((𝐹‘𝐶)‘𝐽) ≤ 0)) |
73 | 72 | rexsng 4590 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐽 ∈ ℕ →
(∃𝑖 ∈ {𝐽} ((𝐹‘𝐶)‘𝑖) ≤ 0 ↔ ((𝐹‘𝐶)‘𝐽) ≤ 0)) |
74 | 26, 73 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (∃𝑖 ∈ {𝐽} ((𝐹‘𝐶)‘𝑖) ≤ 0 ↔ ((𝐹‘𝐶)‘𝐽) ≤ 0)) |
75 | 74 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝐽 = 1) → (∃𝑖 ∈ {𝐽} ((𝐹‘𝐶)‘𝑖) ≤ 0 ↔ ((𝐹‘𝐶)‘𝐽) ≤ 0)) |
76 | 70, 75 | mpbid 235 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝐽 = 1) → ((𝐹‘𝐶)‘𝐽) ≤ 0) |
77 | 21 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝐽 = 1) → 0 < ((𝐹‘𝐶)‘𝐽)) |
78 | | 0red 10836 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 0 ∈
ℝ) |
79 | 39, 40, 41, 42, 43, 44, 64 | ballotlemfelz 32169 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → ((𝐹‘𝐶)‘𝐽) ∈ ℤ) |
80 | 79 | zred 12282 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → ((𝐹‘𝐶)‘𝐽) ∈ ℝ) |
81 | 78, 80 | ltnled 10979 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (0 < ((𝐹‘𝐶)‘𝐽) ↔ ¬ ((𝐹‘𝐶)‘𝐽) ≤ 0)) |
82 | 81 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝐽 = 1) → (0 < ((𝐹‘𝐶)‘𝐽) ↔ ¬ ((𝐹‘𝐶)‘𝐽) ≤ 0)) |
83 | 77, 82 | mpbid 235 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝐽 = 1) → ¬ ((𝐹‘𝐶)‘𝐽) ≤ 0) |
84 | 76, 83 | pm2.65da 817 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ¬ 𝐽 = 1) |
85 | | biortn 938 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (¬
𝐽 = 1 → ((𝐽 − 1) ∈ ℕ
↔ (¬ ¬ 𝐽 = 1
∨ (𝐽 − 1) ∈
ℕ))) |
86 | 84, 85 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝐽 − 1) ∈ ℕ ↔ (¬
¬ 𝐽 = 1 ∨ (𝐽 − 1) ∈
ℕ))) |
87 | | notnotb 318 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐽 = 1 ↔ ¬ ¬ 𝐽 = 1) |
88 | 87 | orbi1i 914 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐽 = 1 ∨ (𝐽 − 1) ∈ ℕ) ↔ (¬
¬ 𝐽 = 1 ∨ (𝐽 − 1) ∈
ℕ)) |
89 | 86, 88 | bitr4di 292 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝐽 − 1) ∈ ℕ ↔ (𝐽 = 1 ∨ (𝐽 − 1) ∈
ℕ))) |
90 | 59, 89 | mpbird 260 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐽 − 1) ∈ ℕ) |
91 | | elnnuz 12478 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐽 − 1) ∈ ℕ
↔ (𝐽 − 1) ∈
(ℤ≥‘1)) |
92 | 90, 91 | sylib 221 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐽 − 1) ∈
(ℤ≥‘1)) |
93 | | elfzp1 13162 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐽 − 1) ∈
(ℤ≥‘1) → (𝑘 ∈ (1...((𝐽 − 1) + 1)) ↔ (𝑘 ∈ (1...(𝐽 − 1)) ∨ 𝑘 = ((𝐽 − 1) + 1)))) |
94 | 92, 93 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑘 ∈ (1...((𝐽 − 1) + 1)) ↔ (𝑘 ∈ (1...(𝐽 − 1)) ∨ 𝑘 = ((𝐽 − 1) + 1)))) |
95 | 26 | nncnd 11846 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐽 ∈ ℂ) |
96 | | 1cnd 10828 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 1 ∈
ℂ) |
97 | 95, 96 | npcand 11193 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝐽 − 1) + 1) = 𝐽) |
98 | 97 | oveq2d 7229 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (1...((𝐽 − 1) + 1)) = (1...𝐽)) |
99 | 98 | eleq2d 2823 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑘 ∈ (1...((𝐽 − 1) + 1)) ↔ 𝑘 ∈ (1...𝐽))) |
100 | 97 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑘 = ((𝐽 − 1) + 1) ↔ 𝑘 = 𝐽)) |
101 | 100 | orbi2d 916 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑘 ∈ (1...(𝐽 − 1)) ∨ 𝑘 = ((𝐽 − 1) + 1)) ↔ (𝑘 ∈ (1...(𝐽 − 1)) ∨ 𝑘 = 𝐽))) |
102 | 94, 99, 101 | 3bitr3d 312 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑘 ∈ (1...𝐽) ↔ (𝑘 ∈ (1...(𝐽 − 1)) ∨ 𝑘 = 𝐽))) |
103 | | orcom 870 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ (1...(𝐽 − 1)) ∨ 𝑘 = 𝐽) ↔ (𝑘 = 𝐽 ∨ 𝑘 ∈ (1...(𝐽 − 1)))) |
104 | 102, 103 | bitrdi 290 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑘 ∈ (1...𝐽) ↔ (𝑘 = 𝐽 ∨ 𝑘 ∈ (1...(𝐽 − 1))))) |
105 | 104 | biimpd 232 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑘 ∈ (1...𝐽) → (𝑘 = 𝐽 ∨ 𝑘 ∈ (1...(𝐽 − 1))))) |
106 | | pm5.6 1002 |
. . . . . . . . . . . . . 14
⊢ (((𝑘 ∈ (1...𝐽) ∧ ¬ 𝑘 = 𝐽) → 𝑘 ∈ (1...(𝐽 − 1))) ↔ (𝑘 ∈ (1...𝐽) → (𝑘 = 𝐽 ∨ 𝑘 ∈ (1...(𝐽 − 1))))) |
107 | 105, 106 | sylibr 237 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑘 ∈ (1...𝐽) ∧ ¬ 𝑘 = 𝐽) → 𝑘 ∈ (1...(𝐽 − 1)))) |
108 | 90 | nnzd 12281 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐽 − 1) ∈ ℤ) |
109 | | 1z 12207 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℤ |
110 | 108, 109 | jctil 523 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (1 ∈ ℤ ∧
(𝐽 − 1) ∈
ℤ)) |
111 | | elfzelz 13112 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ (1...(𝐽 − 1)) → 𝑘 ∈ ℤ) |
112 | 111, 109 | jctir 524 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ (1...(𝐽 − 1)) → (𝑘 ∈ ℤ ∧ 1 ∈
ℤ)) |
113 | | fzaddel 13146 |
. . . . . . . . . . . . . . . . . 18
⊢ (((1
∈ ℤ ∧ (𝐽
− 1) ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ 1 ∈ ℤ))
→ (𝑘 ∈
(1...(𝐽 − 1)) ↔
(𝑘 + 1) ∈ ((1 +
1)...((𝐽 − 1) +
1)))) |
114 | 110, 112,
113 | syl2an 599 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐽 − 1))) → (𝑘 ∈ (1...(𝐽 − 1)) ↔ (𝑘 + 1) ∈ ((1 + 1)...((𝐽 − 1) + 1)))) |
115 | 114 | biimp3a 1471 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐽 − 1)) ∧ 𝑘 ∈ (1...(𝐽 − 1))) → (𝑘 + 1) ∈ ((1 + 1)...((𝐽 − 1) + 1))) |
116 | 115 | 3anidm23 1423 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐽 − 1))) → (𝑘 + 1) ∈ ((1 + 1)...((𝐽 − 1) + 1))) |
117 | | 1p1e2 11955 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (1 + 1) =
2 |
118 | 117 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (1 + 1) =
2) |
119 | 118, 97 | oveq12d 7231 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((1 + 1)...((𝐽 − 1) + 1)) = (2...𝐽)) |
120 | 119 | eleq2d 2823 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑘 + 1) ∈ ((1 + 1)...((𝐽 − 1) + 1)) ↔ (𝑘 + 1) ∈ (2...𝐽))) |
121 | | 2eluzge1 12490 |
. . . . . . . . . . . . . . . . . . 19
⊢ 2 ∈
(ℤ≥‘1) |
122 | | fzss1 13151 |
. . . . . . . . . . . . . . . . . . 19
⊢ (2 ∈
(ℤ≥‘1) → (2...𝐽) ⊆ (1...𝐽)) |
123 | 121, 122 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢
(2...𝐽) ⊆
(1...𝐽) |
124 | 123 | sseli 3896 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 + 1) ∈ (2...𝐽) → (𝑘 + 1) ∈ (1...𝐽)) |
125 | 120, 124 | syl6bi 256 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑘 + 1) ∈ ((1 + 1)...((𝐽 − 1) + 1)) → (𝑘 + 1) ∈ (1...𝐽))) |
126 | 125 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐽 − 1))) → ((𝑘 + 1) ∈ ((1 + 1)...((𝐽 − 1) + 1)) → (𝑘 + 1) ∈ (1...𝐽))) |
127 | 116, 126 | mpd 15 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐽 − 1))) → (𝑘 + 1) ∈ (1...𝐽)) |
128 | 127 | ex 416 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑘 ∈ (1...(𝐽 − 1)) → (𝑘 + 1) ∈ (1...𝐽))) |
129 | 107, 128 | syld 47 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑘 ∈ (1...𝐽) ∧ ¬ 𝑘 = 𝐽) → (𝑘 + 1) ∈ (1...𝐽))) |
130 | 57, 129 | sylan2d 608 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) → (𝑘 + 1) ∈ (1...𝐽))) |
131 | 130 | imp 410 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) → (𝑘 + 1) ∈ (1...𝐽)) |
132 | 131 | adantrr 717 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → (𝑘 + 1) ∈ (1...𝐽)) |
133 | | fveq2 6717 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = (𝑘 + 1) → ((𝐹‘𝐶)‘𝑖) = ((𝐹‘𝐶)‘(𝑘 + 1))) |
134 | 133 | breq1d 5063 |
. . . . . . . . . . . . 13
⊢ (𝑖 = (𝑘 + 1) → (((𝐹‘𝐶)‘𝑖) ≤ 0 ↔ ((𝐹‘𝐶)‘(𝑘 + 1)) ≤ 0)) |
135 | 134 | elrab 3602 |
. . . . . . . . . . . 12
⊢ ((𝑘 + 1) ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ↔ ((𝑘 + 1) ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘(𝑘 + 1)) ≤ 0)) |
136 | | breq1 5056 |
. . . . . . . . . . . . 13
⊢ (𝑗 = (𝑘 + 1) → (𝑗 ≤ 𝑘 ↔ (𝑘 + 1) ≤ 𝑘)) |
137 | 136 | rspccva 3536 |
. . . . . . . . . . . 12
⊢
((∀𝑗 ∈
{𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘 ∧ (𝑘 + 1) ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}) → (𝑘 + 1) ≤ 𝑘) |
138 | 135, 137 | sylan2br 598 |
. . . . . . . . . . 11
⊢
((∀𝑗 ∈
{𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘 ∧ ((𝑘 + 1) ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘(𝑘 + 1)) ≤ 0)) → (𝑘 + 1) ≤ 𝑘) |
139 | 138 | expr 460 |
. . . . . . . . . 10
⊢
((∀𝑗 ∈
{𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘 ∧ (𝑘 + 1) ∈ (1...𝐽)) → (((𝐹‘𝐶)‘(𝑘 + 1)) ≤ 0 → (𝑘 + 1) ≤ 𝑘)) |
140 | 139 | con3d 155 |
. . . . . . . . 9
⊢
((∀𝑗 ∈
{𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘 ∧ (𝑘 + 1) ∈ (1...𝐽)) → (¬ (𝑘 + 1) ≤ 𝑘 → ¬ ((𝐹‘𝐶)‘(𝑘 + 1)) ≤ 0)) |
141 | 20, 132, 140 | syl2anc 587 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → (¬ (𝑘 + 1) ≤ 𝑘 → ¬ ((𝐹‘𝐶)‘(𝑘 + 1)) ≤ 0)) |
142 | 19, 141 | mpd 15 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → ¬ ((𝐹‘𝐶)‘(𝑘 + 1)) ≤ 0) |
143 | | simplrr 778 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘) |
144 | 132 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → (𝑘 + 1) ∈ (1...𝐽)) |
145 | | simpll 767 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → 𝜑) |
146 | 131 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → (𝑘 + 1) ∈ (1...𝐽)) |
147 | 35 | sseld 3900 |
. . . . . . . . . . . . . . 15
⊢ (1 ∈
(ℤ≥‘0) → ((𝑘 + 1) ∈ (1...𝐽) → (𝑘 + 1) ∈ (0...𝐽))) |
148 | 34, 146, 147 | mpsyl 68 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → (𝑘 + 1) ∈ (0...𝐽)) |
149 | 44 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (0...𝐽)) → 𝐶 ∈ 𝑂) |
150 | | elfzelz 13112 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 + 1) ∈ (0...𝐽) → (𝑘 + 1) ∈ ℤ) |
151 | 150 | adantl 485 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (0...𝐽)) → (𝑘 + 1) ∈ ℤ) |
152 | 39, 40, 41, 42, 43, 149, 151 | ballotlemfelz 32169 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (0...𝐽)) → ((𝐹‘𝐶)‘(𝑘 + 1)) ∈ ℤ) |
153 | 152 | zred 12282 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (0...𝐽)) → ((𝐹‘𝐶)‘(𝑘 + 1)) ∈ ℝ) |
154 | 145, 148,
153 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) ∈ ℝ) |
155 | | 0red 10836 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → 0 ∈ ℝ) |
156 | | simplrr 778 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘𝑘) ≤ 0) |
157 | 6 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → 𝑘 ∈ (1...𝐽)) |
158 | 157, 37 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → 𝑘 ∈ (0...𝐽)) |
159 | 130 | imdistani 572 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) → (𝜑 ∧ (𝑘 + 1) ∈ (1...𝐽))) |
160 | 44 | adantr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (1...𝐽)) → 𝐶 ∈ 𝑂) |
161 | | elfznn 13141 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 + 1) ∈ (1...𝐽) → (𝑘 + 1) ∈ ℕ) |
162 | 161 | adantl 485 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (1...𝐽)) → (𝑘 + 1) ∈ ℕ) |
163 | 39, 40, 41, 42, 43, 160, 162 | ballotlemfp1 32170 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (1...𝐽)) → ((¬ (𝑘 + 1) ∈ 𝐶 → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) − 1)) ∧ ((𝑘 + 1) ∈ 𝐶 → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) + 1)))) |
164 | 163 | simpld 498 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (1...𝐽)) → (¬ (𝑘 + 1) ∈ 𝐶 → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) −
1))) |
165 | 164 | imp 410 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑘 + 1) ∈ (1...𝐽)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) −
1)) |
166 | 159, 165 | sylan 583 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) −
1)) |
167 | | elfzelz 13112 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 ∈ (1...𝐽) → 𝑘 ∈ ℤ) |
168 | 167 | zcnd 12283 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ (1...𝐽) → 𝑘 ∈ ℂ) |
169 | | 1cnd 10828 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ (1...𝐽) → 1 ∈ ℂ) |
170 | 168, 169 | pncand 11190 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ (1...𝐽) → ((𝑘 + 1) − 1) = 𝑘) |
171 | 170 | fveq2d 6721 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ (1...𝐽) → ((𝐹‘𝐶)‘((𝑘 + 1) − 1)) = ((𝐹‘𝐶)‘𝑘)) |
172 | 171 | oveq1d 7228 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ (1...𝐽) → (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) − 1) = (((𝐹‘𝐶)‘𝑘) − 1)) |
173 | 172 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ (1...𝐽) → (((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) − 1) ↔ ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) − 1))) |
174 | 157, 173 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → (((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) − 1) ↔ ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) − 1))) |
175 | 166, 174 | mpbid 235 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) − 1)) |
176 | | 0z 12187 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 ∈
ℤ |
177 | | zlem1lt 12229 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹‘𝐶)‘𝑘) ∈ ℤ ∧ 0 ∈ ℤ)
→ (((𝐹‘𝐶)‘𝑘) ≤ 0 ↔ (((𝐹‘𝐶)‘𝑘) − 1) < 0)) |
178 | 48, 176, 177 | sylancl 589 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐽)) → (((𝐹‘𝐶)‘𝑘) ≤ 0 ↔ (((𝐹‘𝐶)‘𝑘) − 1) < 0)) |
179 | 178 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽)) ∧ ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) − 1)) → (((𝐹‘𝐶)‘𝑘) ≤ 0 ↔ (((𝐹‘𝐶)‘𝑘) − 1) < 0)) |
180 | | breq1 5056 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) − 1) → (((𝐹‘𝐶)‘(𝑘 + 1)) < 0 ↔ (((𝐹‘𝐶)‘𝑘) − 1) < 0)) |
181 | 180 | adantl 485 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽)) ∧ ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) − 1)) → (((𝐹‘𝐶)‘(𝑘 + 1)) < 0 ↔ (((𝐹‘𝐶)‘𝑘) − 1) < 0)) |
182 | 179, 181 | bitr4d 285 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝐽)) ∧ ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) − 1)) → (((𝐹‘𝐶)‘𝑘) ≤ 0 ↔ ((𝐹‘𝐶)‘(𝑘 + 1)) < 0)) |
183 | 145, 158,
175, 182 | syl21anc 838 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → (((𝐹‘𝐶)‘𝑘) ≤ 0 ↔ ((𝐹‘𝐶)‘(𝑘 + 1)) < 0)) |
184 | 156, 183 | mpbid 235 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) < 0) |
185 | 154, 155,
184 | ltled 10980 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) ≤ 0) |
186 | 185 | adantlrr 721 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) ≤ 0) |
187 | 143, 144,
186, 138 | syl12anc 837 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → (𝑘 + 1) ≤ 𝑘) |
188 | 19 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) ∧ ¬ (𝑘 + 1) ∈ 𝐶) → ¬ (𝑘 + 1) ≤ 𝑘) |
189 | 187, 188 | condan 818 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → (𝑘 + 1) ∈ 𝐶) |
190 | 163 | simprd 499 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (1...𝐽)) → ((𝑘 + 1) ∈ 𝐶 → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) + 1))) |
191 | 190 | imp 410 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑘 + 1) ∈ (1...𝐽)) ∧ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) + 1)) |
192 | 159, 191 | sylan 583 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) + 1)) |
193 | 6 | adantr 484 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ (𝑘 + 1) ∈ 𝐶) → 𝑘 ∈ (1...𝐽)) |
194 | 171 | oveq1d 7228 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (1...𝐽) → (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) + 1) = (((𝐹‘𝐶)‘𝑘) + 1)) |
195 | 194 | eqeq2d 2748 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (1...𝐽) → (((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) + 1) ↔ ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) + 1))) |
196 | 193, 195 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ (𝑘 + 1) ∈ 𝐶) → (((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘((𝑘 + 1) − 1)) + 1) ↔ ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) + 1))) |
197 | 192, 196 | mpbid 235 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) ∧ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) + 1)) |
198 | 197 | adantlrr 721 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) ∧ (𝑘 + 1) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) + 1)) |
199 | 189, 198 | mpdan 687 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → ((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) + 1)) |
200 | | breq1 5056 |
. . . . . . . . 9
⊢ (((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) + 1) → (((𝐹‘𝐶)‘(𝑘 + 1)) ≤ 0 ↔ (((𝐹‘𝐶)‘𝑘) + 1) ≤ 0)) |
201 | 200 | notbid 321 |
. . . . . . . 8
⊢ (((𝐹‘𝐶)‘(𝑘 + 1)) = (((𝐹‘𝐶)‘𝑘) + 1) → (¬ ((𝐹‘𝐶)‘(𝑘 + 1)) ≤ 0 ↔ ¬ (((𝐹‘𝐶)‘𝑘) + 1) ≤ 0)) |
202 | 199, 201 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → (¬ ((𝐹‘𝐶)‘(𝑘 + 1)) ≤ 0 ↔ ¬ (((𝐹‘𝐶)‘𝑘) + 1) ≤ 0)) |
203 | 142, 202 | mpbid 235 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → ¬ (((𝐹‘𝐶)‘𝑘) + 1) ≤ 0) |
204 | 6, 37 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) → 𝑘 ∈ (0...𝐽)) |
205 | 204, 48 | syldan 594 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0)) → ((𝐹‘𝐶)‘𝑘) ∈ ℤ) |
206 | 205 | adantrr 717 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → ((𝐹‘𝐶)‘𝑘) ∈ ℤ) |
207 | | zleltp1 12228 |
. . . . . . . . 9
⊢ ((0
∈ ℤ ∧ ((𝐹‘𝐶)‘𝑘) ∈ ℤ) → (0 ≤ ((𝐹‘𝐶)‘𝑘) ↔ 0 < (((𝐹‘𝐶)‘𝑘) + 1))) |
208 | 176, 207 | mpan 690 |
. . . . . . . 8
⊢ (((𝐹‘𝐶)‘𝑘) ∈ ℤ → (0 ≤ ((𝐹‘𝐶)‘𝑘) ↔ 0 < (((𝐹‘𝐶)‘𝑘) + 1))) |
209 | | 0red 10836 |
. . . . . . . . 9
⊢ (((𝐹‘𝐶)‘𝑘) ∈ ℤ → 0 ∈
ℝ) |
210 | | zre 12180 |
. . . . . . . . . 10
⊢ (((𝐹‘𝐶)‘𝑘) ∈ ℤ → ((𝐹‘𝐶)‘𝑘) ∈ ℝ) |
211 | | 1red 10834 |
. . . . . . . . . 10
⊢ (((𝐹‘𝐶)‘𝑘) ∈ ℤ → 1 ∈
ℝ) |
212 | 210, 211 | readdcld 10862 |
. . . . . . . . 9
⊢ (((𝐹‘𝐶)‘𝑘) ∈ ℤ → (((𝐹‘𝐶)‘𝑘) + 1) ∈ ℝ) |
213 | 209, 212 | ltnled 10979 |
. . . . . . . 8
⊢ (((𝐹‘𝐶)‘𝑘) ∈ ℤ → (0 < (((𝐹‘𝐶)‘𝑘) + 1) ↔ ¬ (((𝐹‘𝐶)‘𝑘) + 1) ≤ 0)) |
214 | 208, 213 | bitrd 282 |
. . . . . . 7
⊢ (((𝐹‘𝐶)‘𝑘) ∈ ℤ → (0 ≤ ((𝐹‘𝐶)‘𝑘) ↔ ¬ (((𝐹‘𝐶)‘𝑘) + 1) ≤ 0)) |
215 | 206, 214 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → (0 ≤ ((𝐹‘𝐶)‘𝑘) ↔ ¬ (((𝐹‘𝐶)‘𝑘) + 1) ≤ 0)) |
216 | 203, 215 | mpbird 260 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → 0 ≤ ((𝐹‘𝐶)‘𝑘)) |
217 | 206 | zred 12282 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → ((𝐹‘𝐶)‘𝑘) ∈ ℝ) |
218 | | 0red 10836 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → 0 ∈ ℝ) |
219 | 217, 218 | letri3d 10974 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → (((𝐹‘𝐶)‘𝑘) = 0 ↔ (((𝐹‘𝐶)‘𝑘) ≤ 0 ∧ 0 ≤ ((𝐹‘𝐶)‘𝑘)))) |
220 | 5, 216, 219 | mpbir2and 713 |
. . . 4
⊢ ((𝜑 ∧ ((𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) ≤ 0) ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → ((𝐹‘𝐶)‘𝑘) = 0) |
221 | 4, 220 | sylan2b 597 |
. . 3
⊢ ((𝜑 ∧ (𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ∧ ∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘)) → ((𝐹‘𝐶)‘𝑘) = 0) |
222 | | ssrab2 3993 |
. . . . . 6
⊢ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ⊆ (1...𝐽) |
223 | 222, 12 | sstri 3910 |
. . . . 5
⊢ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ⊆ ℝ |
224 | 223 | a1i 11 |
. . . 4
⊢ (𝜑 → {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ⊆ ℝ) |
225 | | fzfi 13545 |
. . . . . 6
⊢
(1...𝐽) ∈
Fin |
226 | | ssfi 8851 |
. . . . . 6
⊢
(((1...𝐽) ∈ Fin
∧ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ⊆ (1...𝐽)) → {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ∈ Fin) |
227 | 225, 222,
226 | mp2an 692 |
. . . . 5
⊢ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ∈ Fin |
228 | 227 | a1i 11 |
. . . 4
⊢ (𝜑 → {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ∈ Fin) |
229 | | rabn0 4300 |
. . . . 5
⊢ ({𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ≠ ∅ ↔ ∃𝑖 ∈ (1...𝐽)((𝐹‘𝐶)‘𝑖) ≤ 0) |
230 | 60, 229 | sylibr 237 |
. . . 4
⊢ (𝜑 → {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ≠ ∅) |
231 | | fimaxre 11776 |
. . . 4
⊢ (({𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ⊆ ℝ ∧ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ∈ Fin ∧ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ≠ ∅) → ∃𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘) |
232 | 224, 228,
230, 231 | syl3anc 1373 |
. . 3
⊢ (𝜑 → ∃𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}∀𝑗 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0}𝑗 ≤ 𝑘) |
233 | 221, 232 | reximddv 3194 |
. 2
⊢ (𝜑 → ∃𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ((𝐹‘𝐶)‘𝑘) = 0) |
234 | | elrabi 3596 |
. . . 4
⊢ (𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} → 𝑘 ∈ (1...𝐽)) |
235 | 234 | anim1i 618 |
. . 3
⊢ ((𝑘 ∈ {𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ∧ ((𝐹‘𝐶)‘𝑘) = 0) → (𝑘 ∈ (1...𝐽) ∧ ((𝐹‘𝐶)‘𝑘) = 0)) |
236 | 235 | reximi2 3167 |
. 2
⊢
(∃𝑘 ∈
{𝑖 ∈ (1...𝐽) ∣ ((𝐹‘𝐶)‘𝑖) ≤ 0} ((𝐹‘𝐶)‘𝑘) = 0 → ∃𝑘 ∈ (1...𝐽)((𝐹‘𝐶)‘𝑘) = 0) |
237 | 233, 236 | syl 17 |
1
⊢ (𝜑 → ∃𝑘 ∈ (1...𝐽)((𝐹‘𝐶)‘𝑘) = 0) |