Proof of Theorem ballotlemfp1
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ballotth.m | . . . . . 6
⊢ 𝑀 ∈ ℕ | 
| 2 |  | ballotth.n | . . . . . 6
⊢ 𝑁 ∈ ℕ | 
| 3 |  | ballotth.o | . . . . . 6
⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} | 
| 4 |  | ballotth.p | . . . . . 6
⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) | 
| 5 |  | ballotth.f | . . . . . 6
⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦
((♯‘((1...𝑖)
∩ 𝑐)) −
(♯‘((1...𝑖)
∖ 𝑐))))) | 
| 6 |  | ballotlemfp1.c | . . . . . 6
⊢ (𝜑 → 𝐶 ∈ 𝑂) | 
| 7 |  | ballotlemfp1.j | . . . . . . 7
⊢ (𝜑 → 𝐽 ∈ ℕ) | 
| 8 | 7 | nnzd 12642 | . . . . . 6
⊢ (𝜑 → 𝐽 ∈ ℤ) | 
| 9 | 1, 2, 3, 4, 5, 6, 8 | ballotlemfval 34493 | . . . . 5
⊢ (𝜑 → ((𝐹‘𝐶)‘𝐽) = ((♯‘((1...𝐽) ∩ 𝐶)) − (♯‘((1...𝐽) ∖ 𝐶)))) | 
| 10 | 9 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ ¬ 𝐽 ∈ 𝐶) → ((𝐹‘𝐶)‘𝐽) = ((♯‘((1...𝐽) ∩ 𝐶)) − (♯‘((1...𝐽) ∖ 𝐶)))) | 
| 11 |  | fzfi 14014 | . . . . . . . . . 10
⊢
(1...(𝐽 − 1))
∈ Fin | 
| 12 |  | inss1 4236 | . . . . . . . . . 10
⊢
((1...(𝐽 − 1))
∩ 𝐶) ⊆
(1...(𝐽 −
1)) | 
| 13 |  | ssfi 9214 | . . . . . . . . . 10
⊢
(((1...(𝐽 −
1)) ∈ Fin ∧ ((1...(𝐽 − 1)) ∩ 𝐶) ⊆ (1...(𝐽 − 1))) → ((1...(𝐽 − 1)) ∩ 𝐶) ∈ Fin) | 
| 14 | 11, 12, 13 | mp2an 692 | . . . . . . . . 9
⊢
((1...(𝐽 − 1))
∩ 𝐶) ∈
Fin | 
| 15 |  | hashcl 14396 | . . . . . . . . 9
⊢
(((1...(𝐽 −
1)) ∩ 𝐶) ∈ Fin
→ (♯‘((1...(𝐽 − 1)) ∩ 𝐶)) ∈
ℕ0) | 
| 16 | 14, 15 | ax-mp 5 | . . . . . . . 8
⊢
(♯‘((1...(𝐽 − 1)) ∩ 𝐶)) ∈
ℕ0 | 
| 17 | 16 | nn0cni 12540 | . . . . . . 7
⊢
(♯‘((1...(𝐽 − 1)) ∩ 𝐶)) ∈ ℂ | 
| 18 | 17 | a1i 11 | . . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐽 ∈ 𝐶) → (♯‘((1...(𝐽 − 1)) ∩ 𝐶)) ∈
ℂ) | 
| 19 |  | diffi 9216 | . . . . . . . . . 10
⊢
((1...(𝐽 − 1))
∈ Fin → ((1...(𝐽
− 1)) ∖ 𝐶)
∈ Fin) | 
| 20 | 11, 19 | ax-mp 5 | . . . . . . . . 9
⊢
((1...(𝐽 − 1))
∖ 𝐶) ∈
Fin | 
| 21 |  | hashcl 14396 | . . . . . . . . 9
⊢
(((1...(𝐽 −
1)) ∖ 𝐶) ∈ Fin
→ (♯‘((1...(𝐽 − 1)) ∖ 𝐶)) ∈
ℕ0) | 
| 22 | 20, 21 | ax-mp 5 | . . . . . . . 8
⊢
(♯‘((1...(𝐽 − 1)) ∖ 𝐶)) ∈
ℕ0 | 
| 23 | 22 | nn0cni 12540 | . . . . . . 7
⊢
(♯‘((1...(𝐽 − 1)) ∖ 𝐶)) ∈ ℂ | 
| 24 | 23 | a1i 11 | . . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐽 ∈ 𝐶) → (♯‘((1...(𝐽 − 1)) ∖ 𝐶)) ∈
ℂ) | 
| 25 |  | 1cnd 11257 | . . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐽 ∈ 𝐶) → 1 ∈ ℂ) | 
| 26 | 18, 24, 25 | subsub4d 11652 | . . . . 5
⊢ ((𝜑 ∧ ¬ 𝐽 ∈ 𝐶) → (((♯‘((1...(𝐽 − 1)) ∩ 𝐶)) −
(♯‘((1...(𝐽
− 1)) ∖ 𝐶)))
− 1) = ((♯‘((1...(𝐽 − 1)) ∩ 𝐶)) − ((♯‘((1...(𝐽 − 1)) ∖ 𝐶)) + 1))) | 
| 27 |  | 1zzd 12650 | . . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℤ) | 
| 28 | 8, 27 | zsubcld 12729 | . . . . . . . 8
⊢ (𝜑 → (𝐽 − 1) ∈ ℤ) | 
| 29 | 1, 2, 3, 4, 5, 6, 28 | ballotlemfval 34493 | . . . . . . 7
⊢ (𝜑 → ((𝐹‘𝐶)‘(𝐽 − 1)) = ((♯‘((1...(𝐽 − 1)) ∩ 𝐶)) −
(♯‘((1...(𝐽
− 1)) ∖ 𝐶)))) | 
| 30 | 29 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐽 ∈ 𝐶) → ((𝐹‘𝐶)‘(𝐽 − 1)) = ((♯‘((1...(𝐽 − 1)) ∩ 𝐶)) −
(♯‘((1...(𝐽
− 1)) ∖ 𝐶)))) | 
| 31 | 30 | oveq1d 7447 | . . . . 5
⊢ ((𝜑 ∧ ¬ 𝐽 ∈ 𝐶) → (((𝐹‘𝐶)‘(𝐽 − 1)) − 1) =
(((♯‘((1...(𝐽
− 1)) ∩ 𝐶))
− (♯‘((1...(𝐽 − 1)) ∖ 𝐶))) − 1)) | 
| 32 |  | elnnuz 12923 | . . . . . . . . . . 11
⊢ (𝐽 ∈ ℕ ↔ 𝐽 ∈
(ℤ≥‘1)) | 
| 33 | 7, 32 | sylib 218 | . . . . . . . . . 10
⊢ (𝜑 → 𝐽 ∈
(ℤ≥‘1)) | 
| 34 |  | fzspl 32792 | . . . . . . . . . . . 12
⊢ (𝐽 ∈
(ℤ≥‘1) → (1...𝐽) = ((1...(𝐽 − 1)) ∪ {𝐽})) | 
| 35 | 34 | ineq1d 4218 | . . . . . . . . . . 11
⊢ (𝐽 ∈
(ℤ≥‘1) → ((1...𝐽) ∩ 𝐶) = (((1...(𝐽 − 1)) ∪ {𝐽}) ∩ 𝐶)) | 
| 36 |  | indir 4285 | . . . . . . . . . . 11
⊢
(((1...(𝐽 −
1)) ∪ {𝐽}) ∩ 𝐶) = (((1...(𝐽 − 1)) ∩ 𝐶) ∪ ({𝐽} ∩ 𝐶)) | 
| 37 | 35, 36 | eqtrdi 2792 | . . . . . . . . . 10
⊢ (𝐽 ∈
(ℤ≥‘1) → ((1...𝐽) ∩ 𝐶) = (((1...(𝐽 − 1)) ∩ 𝐶) ∪ ({𝐽} ∩ 𝐶))) | 
| 38 | 33, 37 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → ((1...𝐽) ∩ 𝐶) = (((1...(𝐽 − 1)) ∩ 𝐶) ∪ ({𝐽} ∩ 𝐶))) | 
| 39 | 38 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐽 ∈ 𝐶) → ((1...𝐽) ∩ 𝐶) = (((1...(𝐽 − 1)) ∩ 𝐶) ∪ ({𝐽} ∩ 𝐶))) | 
| 40 |  | disjsn 4710 | . . . . . . . . . . . 12
⊢ ((𝐶 ∩ {𝐽}) = ∅ ↔ ¬ 𝐽 ∈ 𝐶) | 
| 41 |  | incom 4208 | . . . . . . . . . . . . 13
⊢ (𝐶 ∩ {𝐽}) = ({𝐽} ∩ 𝐶) | 
| 42 | 41 | eqeq1i 2741 | . . . . . . . . . . . 12
⊢ ((𝐶 ∩ {𝐽}) = ∅ ↔ ({𝐽} ∩ 𝐶) = ∅) | 
| 43 | 40, 42 | sylbb1 237 | . . . . . . . . . . 11
⊢ (¬
𝐽 ∈ 𝐶 → ({𝐽} ∩ 𝐶) = ∅) | 
| 44 | 43 | adantl 481 | . . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 𝐽 ∈ 𝐶) → ({𝐽} ∩ 𝐶) = ∅) | 
| 45 | 44 | uneq2d 4167 | . . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝐽 ∈ 𝐶) → (((1...(𝐽 − 1)) ∩ 𝐶) ∪ ({𝐽} ∩ 𝐶)) = (((1...(𝐽 − 1)) ∩ 𝐶) ∪ ∅)) | 
| 46 |  | un0 4393 | . . . . . . . . 9
⊢
(((1...(𝐽 −
1)) ∩ 𝐶) ∪ ∅)
= ((1...(𝐽 − 1))
∩ 𝐶) | 
| 47 | 45, 46 | eqtrdi 2792 | . . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐽 ∈ 𝐶) → (((1...(𝐽 − 1)) ∩ 𝐶) ∪ ({𝐽} ∩ 𝐶)) = ((1...(𝐽 − 1)) ∩ 𝐶)) | 
| 48 | 39, 47 | eqtrd 2776 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐽 ∈ 𝐶) → ((1...𝐽) ∩ 𝐶) = ((1...(𝐽 − 1)) ∩ 𝐶)) | 
| 49 | 48 | fveq2d 6909 | . . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐽 ∈ 𝐶) → (♯‘((1...𝐽) ∩ 𝐶)) = (♯‘((1...(𝐽 − 1)) ∩ 𝐶))) | 
| 50 | 34 | difeq1d 4124 | . . . . . . . . . . 11
⊢ (𝐽 ∈
(ℤ≥‘1) → ((1...𝐽) ∖ 𝐶) = (((1...(𝐽 − 1)) ∪ {𝐽}) ∖ 𝐶)) | 
| 51 |  | difundir 4290 | . . . . . . . . . . 11
⊢
(((1...(𝐽 −
1)) ∪ {𝐽}) ∖
𝐶) = (((1...(𝐽 − 1)) ∖ 𝐶) ∪ ({𝐽} ∖ 𝐶)) | 
| 52 | 50, 51 | eqtrdi 2792 | . . . . . . . . . 10
⊢ (𝐽 ∈
(ℤ≥‘1) → ((1...𝐽) ∖ 𝐶) = (((1...(𝐽 − 1)) ∖ 𝐶) ∪ ({𝐽} ∖ 𝐶))) | 
| 53 | 33, 52 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → ((1...𝐽) ∖ 𝐶) = (((1...(𝐽 − 1)) ∖ 𝐶) ∪ ({𝐽} ∖ 𝐶))) | 
| 54 |  | disj3 4453 | . . . . . . . . . . . 12
⊢ (({𝐽} ∩ 𝐶) = ∅ ↔ {𝐽} = ({𝐽} ∖ 𝐶)) | 
| 55 | 43, 54 | sylib 218 | . . . . . . . . . . 11
⊢ (¬
𝐽 ∈ 𝐶 → {𝐽} = ({𝐽} ∖ 𝐶)) | 
| 56 | 55 | eqcomd 2742 | . . . . . . . . . 10
⊢ (¬
𝐽 ∈ 𝐶 → ({𝐽} ∖ 𝐶) = {𝐽}) | 
| 57 | 56 | uneq2d 4167 | . . . . . . . . 9
⊢ (¬
𝐽 ∈ 𝐶 → (((1...(𝐽 − 1)) ∖ 𝐶) ∪ ({𝐽} ∖ 𝐶)) = (((1...(𝐽 − 1)) ∖ 𝐶) ∪ {𝐽})) | 
| 58 | 53, 57 | sylan9eq 2796 | . . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐽 ∈ 𝐶) → ((1...𝐽) ∖ 𝐶) = (((1...(𝐽 − 1)) ∖ 𝐶) ∪ {𝐽})) | 
| 59 | 58 | fveq2d 6909 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐽 ∈ 𝐶) → (♯‘((1...𝐽) ∖ 𝐶)) = (♯‘(((1...(𝐽 − 1)) ∖ 𝐶) ∪ {𝐽}))) | 
| 60 | 8 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐽 ∈ 𝐶) → 𝐽 ∈ ℤ) | 
| 61 |  | uzid 12894 | . . . . . . . . . . . 12
⊢ (𝐽 ∈ ℤ → 𝐽 ∈
(ℤ≥‘𝐽)) | 
| 62 |  | uznfz 13651 | . . . . . . . . . . . 12
⊢ (𝐽 ∈
(ℤ≥‘𝐽) → ¬ 𝐽 ∈ (1...(𝐽 − 1))) | 
| 63 | 8, 61, 62 | 3syl 18 | . . . . . . . . . . 11
⊢ (𝜑 → ¬ 𝐽 ∈ (1...(𝐽 − 1))) | 
| 64 | 63 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 𝐽 ∈ 𝐶) → ¬ 𝐽 ∈ (1...(𝐽 − 1))) | 
| 65 |  | difss 4135 | . . . . . . . . . . 11
⊢
((1...(𝐽 − 1))
∖ 𝐶) ⊆
(1...(𝐽 −
1)) | 
| 66 | 65 | sseli 3978 | . . . . . . . . . 10
⊢ (𝐽 ∈ ((1...(𝐽 − 1)) ∖ 𝐶) → 𝐽 ∈ (1...(𝐽 − 1))) | 
| 67 | 64, 66 | nsyl 140 | . . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝐽 ∈ 𝐶) → ¬ 𝐽 ∈ ((1...(𝐽 − 1)) ∖ 𝐶)) | 
| 68 |  | ssfi 9214 | . . . . . . . . . 10
⊢
(((1...(𝐽 −
1)) ∈ Fin ∧ ((1...(𝐽 − 1)) ∖ 𝐶) ⊆ (1...(𝐽 − 1))) → ((1...(𝐽 − 1)) ∖ 𝐶) ∈ Fin) | 
| 69 | 11, 65, 68 | mp2an 692 | . . . . . . . . 9
⊢
((1...(𝐽 − 1))
∖ 𝐶) ∈
Fin | 
| 70 | 67, 69 | jctil 519 | . . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐽 ∈ 𝐶) → (((1...(𝐽 − 1)) ∖ 𝐶) ∈ Fin ∧ ¬ 𝐽 ∈ ((1...(𝐽 − 1)) ∖ 𝐶))) | 
| 71 |  | hashunsng 14432 | . . . . . . . 8
⊢ (𝐽 ∈ ℤ →
((((1...(𝐽 − 1))
∖ 𝐶) ∈ Fin ∧
¬ 𝐽 ∈ ((1...(𝐽 − 1)) ∖ 𝐶)) →
(♯‘(((1...(𝐽
− 1)) ∖ 𝐶)
∪ {𝐽})) =
((♯‘((1...(𝐽
− 1)) ∖ 𝐶)) +
1))) | 
| 72 | 60, 70, 71 | sylc 65 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐽 ∈ 𝐶) → (♯‘(((1...(𝐽 − 1)) ∖ 𝐶) ∪ {𝐽})) = ((♯‘((1...(𝐽 − 1)) ∖ 𝐶)) + 1)) | 
| 73 | 59, 72 | eqtrd 2776 | . . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐽 ∈ 𝐶) → (♯‘((1...𝐽) ∖ 𝐶)) = ((♯‘((1...(𝐽 − 1)) ∖ 𝐶)) + 1)) | 
| 74 | 49, 73 | oveq12d 7450 | . . . . 5
⊢ ((𝜑 ∧ ¬ 𝐽 ∈ 𝐶) → ((♯‘((1...𝐽) ∩ 𝐶)) − (♯‘((1...𝐽) ∖ 𝐶))) = ((♯‘((1...(𝐽 − 1)) ∩ 𝐶)) −
((♯‘((1...(𝐽
− 1)) ∖ 𝐶)) +
1))) | 
| 75 | 26, 31, 74 | 3eqtr4rd 2787 | . . . 4
⊢ ((𝜑 ∧ ¬ 𝐽 ∈ 𝐶) → ((♯‘((1...𝐽) ∩ 𝐶)) − (♯‘((1...𝐽) ∖ 𝐶))) = (((𝐹‘𝐶)‘(𝐽 − 1)) − 1)) | 
| 76 | 10, 75 | eqtrd 2776 | . . 3
⊢ ((𝜑 ∧ ¬ 𝐽 ∈ 𝐶) → ((𝐹‘𝐶)‘𝐽) = (((𝐹‘𝐶)‘(𝐽 − 1)) − 1)) | 
| 77 | 76 | ex 412 | . 2
⊢ (𝜑 → (¬ 𝐽 ∈ 𝐶 → ((𝐹‘𝐶)‘𝐽) = (((𝐹‘𝐶)‘(𝐽 − 1)) − 1))) | 
| 78 | 9 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝐽 ∈ 𝐶) → ((𝐹‘𝐶)‘𝐽) = ((♯‘((1...𝐽) ∩ 𝐶)) − (♯‘((1...𝐽) ∖ 𝐶)))) | 
| 79 | 17 | a1i 11 | . . . . . 6
⊢ ((𝜑 ∧ 𝐽 ∈ 𝐶) → (♯‘((1...(𝐽 − 1)) ∩ 𝐶)) ∈
ℂ) | 
| 80 |  | 1cnd 11257 | . . . . . 6
⊢ ((𝜑 ∧ 𝐽 ∈ 𝐶) → 1 ∈ ℂ) | 
| 81 | 23 | a1i 11 | . . . . . 6
⊢ ((𝜑 ∧ 𝐽 ∈ 𝐶) → (♯‘((1...(𝐽 − 1)) ∖ 𝐶)) ∈
ℂ) | 
| 82 | 79, 80, 81 | addsubd 11642 | . . . . 5
⊢ ((𝜑 ∧ 𝐽 ∈ 𝐶) → (((♯‘((1...(𝐽 − 1)) ∩ 𝐶)) + 1) −
(♯‘((1...(𝐽
− 1)) ∖ 𝐶))) =
(((♯‘((1...(𝐽
− 1)) ∩ 𝐶))
− (♯‘((1...(𝐽 − 1)) ∖ 𝐶))) + 1)) | 
| 83 | 38 | fveq2d 6909 | . . . . . . . 8
⊢ (𝜑 → (♯‘((1...𝐽) ∩ 𝐶)) = (♯‘(((1...(𝐽 − 1)) ∩ 𝐶) ∪ ({𝐽} ∩ 𝐶)))) | 
| 84 | 83 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐽 ∈ 𝐶) → (♯‘((1...𝐽) ∩ 𝐶)) = (♯‘(((1...(𝐽 − 1)) ∩ 𝐶) ∪ ({𝐽} ∩ 𝐶)))) | 
| 85 |  | snssi 4807 | . . . . . . . . . . 11
⊢ (𝐽 ∈ 𝐶 → {𝐽} ⊆ 𝐶) | 
| 86 |  | dfss2 3968 | . . . . . . . . . . 11
⊢ ({𝐽} ⊆ 𝐶 ↔ ({𝐽} ∩ 𝐶) = {𝐽}) | 
| 87 | 85, 86 | sylib 218 | . . . . . . . . . 10
⊢ (𝐽 ∈ 𝐶 → ({𝐽} ∩ 𝐶) = {𝐽}) | 
| 88 | 87 | uneq2d 4167 | . . . . . . . . 9
⊢ (𝐽 ∈ 𝐶 → (((1...(𝐽 − 1)) ∩ 𝐶) ∪ ({𝐽} ∩ 𝐶)) = (((1...(𝐽 − 1)) ∩ 𝐶) ∪ {𝐽})) | 
| 89 | 88 | fveq2d 6909 | . . . . . . . 8
⊢ (𝐽 ∈ 𝐶 → (♯‘(((1...(𝐽 − 1)) ∩ 𝐶) ∪ ({𝐽} ∩ 𝐶))) = (♯‘(((1...(𝐽 − 1)) ∩ 𝐶) ∪ {𝐽}))) | 
| 90 | 89 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐽 ∈ 𝐶) → (♯‘(((1...(𝐽 − 1)) ∩ 𝐶) ∪ ({𝐽} ∩ 𝐶))) = (♯‘(((1...(𝐽 − 1)) ∩ 𝐶) ∪ {𝐽}))) | 
| 91 |  | simpr 484 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐽 ∈ 𝐶) → 𝐽 ∈ 𝐶) | 
| 92 | 8 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐽 ∈ 𝐶) → 𝐽 ∈ ℤ) | 
| 93 | 92, 61, 62 | 3syl 18 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐽 ∈ 𝐶) → ¬ 𝐽 ∈ (1...(𝐽 − 1))) | 
| 94 | 12 | sseli 3978 | . . . . . . . . . 10
⊢ (𝐽 ∈ ((1...(𝐽 − 1)) ∩ 𝐶) → 𝐽 ∈ (1...(𝐽 − 1))) | 
| 95 | 93, 94 | nsyl 140 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐽 ∈ 𝐶) → ¬ 𝐽 ∈ ((1...(𝐽 − 1)) ∩ 𝐶)) | 
| 96 | 95, 14 | jctil 519 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐽 ∈ 𝐶) → (((1...(𝐽 − 1)) ∩ 𝐶) ∈ Fin ∧ ¬ 𝐽 ∈ ((1...(𝐽 − 1)) ∩ 𝐶))) | 
| 97 |  | hashunsng 14432 | . . . . . . . 8
⊢ (𝐽 ∈ 𝐶 → ((((1...(𝐽 − 1)) ∩ 𝐶) ∈ Fin ∧ ¬ 𝐽 ∈ ((1...(𝐽 − 1)) ∩ 𝐶)) → (♯‘(((1...(𝐽 − 1)) ∩ 𝐶) ∪ {𝐽})) = ((♯‘((1...(𝐽 − 1)) ∩ 𝐶)) + 1))) | 
| 98 | 91, 96, 97 | sylc 65 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐽 ∈ 𝐶) → (♯‘(((1...(𝐽 − 1)) ∩ 𝐶) ∪ {𝐽})) = ((♯‘((1...(𝐽 − 1)) ∩ 𝐶)) + 1)) | 
| 99 | 84, 90, 98 | 3eqtrd 2780 | . . . . . 6
⊢ ((𝜑 ∧ 𝐽 ∈ 𝐶) → (♯‘((1...𝐽) ∩ 𝐶)) = ((♯‘((1...(𝐽 − 1)) ∩ 𝐶)) + 1)) | 
| 100 | 53 | fveq2d 6909 | . . . . . . . 8
⊢ (𝜑 → (♯‘((1...𝐽) ∖ 𝐶)) = (♯‘(((1...(𝐽 − 1)) ∖ 𝐶) ∪ ({𝐽} ∖ 𝐶)))) | 
| 101 | 100 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐽 ∈ 𝐶) → (♯‘((1...𝐽) ∖ 𝐶)) = (♯‘(((1...(𝐽 − 1)) ∖ 𝐶) ∪ ({𝐽} ∖ 𝐶)))) | 
| 102 |  | difin2 4300 | . . . . . . . . . . . 12
⊢ ({𝐽} ⊆ 𝐶 → ({𝐽} ∖ 𝐶) = ((𝐶 ∖ 𝐶) ∩ {𝐽})) | 
| 103 |  | difid 4375 | . . . . . . . . . . . . . 14
⊢ (𝐶 ∖ 𝐶) = ∅ | 
| 104 | 103 | ineq1i 4215 | . . . . . . . . . . . . 13
⊢ ((𝐶 ∖ 𝐶) ∩ {𝐽}) = (∅ ∩ {𝐽}) | 
| 105 |  | 0in 4396 | . . . . . . . . . . . . 13
⊢ (∅
∩ {𝐽}) =
∅ | 
| 106 | 104, 105 | eqtri 2764 | . . . . . . . . . . . 12
⊢ ((𝐶 ∖ 𝐶) ∩ {𝐽}) = ∅ | 
| 107 | 102, 106 | eqtrdi 2792 | . . . . . . . . . . 11
⊢ ({𝐽} ⊆ 𝐶 → ({𝐽} ∖ 𝐶) = ∅) | 
| 108 | 85, 107 | syl 17 | . . . . . . . . . 10
⊢ (𝐽 ∈ 𝐶 → ({𝐽} ∖ 𝐶) = ∅) | 
| 109 | 108 | uneq2d 4167 | . . . . . . . . 9
⊢ (𝐽 ∈ 𝐶 → (((1...(𝐽 − 1)) ∖ 𝐶) ∪ ({𝐽} ∖ 𝐶)) = (((1...(𝐽 − 1)) ∖ 𝐶) ∪ ∅)) | 
| 110 | 109 | fveq2d 6909 | . . . . . . . 8
⊢ (𝐽 ∈ 𝐶 → (♯‘(((1...(𝐽 − 1)) ∖ 𝐶) ∪ ({𝐽} ∖ 𝐶))) = (♯‘(((1...(𝐽 − 1)) ∖ 𝐶) ∪
∅))) | 
| 111 | 110 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐽 ∈ 𝐶) → (♯‘(((1...(𝐽 − 1)) ∖ 𝐶) ∪ ({𝐽} ∖ 𝐶))) = (♯‘(((1...(𝐽 − 1)) ∖ 𝐶) ∪
∅))) | 
| 112 |  | un0 4393 | . . . . . . . . 9
⊢
(((1...(𝐽 −
1)) ∖ 𝐶) ∪
∅) = ((1...(𝐽 −
1)) ∖ 𝐶) | 
| 113 | 112 | a1i 11 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐽 ∈ 𝐶) → (((1...(𝐽 − 1)) ∖ 𝐶) ∪ ∅) = ((1...(𝐽 − 1)) ∖ 𝐶)) | 
| 114 | 113 | fveq2d 6909 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐽 ∈ 𝐶) → (♯‘(((1...(𝐽 − 1)) ∖ 𝐶) ∪ ∅)) =
(♯‘((1...(𝐽
− 1)) ∖ 𝐶))) | 
| 115 | 101, 111,
114 | 3eqtrd 2780 | . . . . . 6
⊢ ((𝜑 ∧ 𝐽 ∈ 𝐶) → (♯‘((1...𝐽) ∖ 𝐶)) = (♯‘((1...(𝐽 − 1)) ∖ 𝐶))) | 
| 116 | 99, 115 | oveq12d 7450 | . . . . 5
⊢ ((𝜑 ∧ 𝐽 ∈ 𝐶) → ((♯‘((1...𝐽) ∩ 𝐶)) − (♯‘((1...𝐽) ∖ 𝐶))) = (((♯‘((1...(𝐽 − 1)) ∩ 𝐶)) + 1) −
(♯‘((1...(𝐽
− 1)) ∖ 𝐶)))) | 
| 117 | 29 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝐽 ∈ 𝐶) → ((𝐹‘𝐶)‘(𝐽 − 1)) = ((♯‘((1...(𝐽 − 1)) ∩ 𝐶)) −
(♯‘((1...(𝐽
− 1)) ∖ 𝐶)))) | 
| 118 | 117 | oveq1d 7447 | . . . . 5
⊢ ((𝜑 ∧ 𝐽 ∈ 𝐶) → (((𝐹‘𝐶)‘(𝐽 − 1)) + 1) =
(((♯‘((1...(𝐽
− 1)) ∩ 𝐶))
− (♯‘((1...(𝐽 − 1)) ∖ 𝐶))) + 1)) | 
| 119 | 82, 116, 118 | 3eqtr4d 2786 | . . . 4
⊢ ((𝜑 ∧ 𝐽 ∈ 𝐶) → ((♯‘((1...𝐽) ∩ 𝐶)) − (♯‘((1...𝐽) ∖ 𝐶))) = (((𝐹‘𝐶)‘(𝐽 − 1)) + 1)) | 
| 120 | 78, 119 | eqtrd 2776 | . . 3
⊢ ((𝜑 ∧ 𝐽 ∈ 𝐶) → ((𝐹‘𝐶)‘𝐽) = (((𝐹‘𝐶)‘(𝐽 − 1)) + 1)) | 
| 121 | 120 | ex 412 | . 2
⊢ (𝜑 → (𝐽 ∈ 𝐶 → ((𝐹‘𝐶)‘𝐽) = (((𝐹‘𝐶)‘(𝐽 − 1)) + 1))) | 
| 122 | 77, 121 | jca 511 | 1
⊢ (𝜑 → ((¬ 𝐽 ∈ 𝐶 → ((𝐹‘𝐶)‘𝐽) = (((𝐹‘𝐶)‘(𝐽 − 1)) − 1)) ∧ (𝐽 ∈ 𝐶 → ((𝐹‘𝐶)‘𝐽) = (((𝐹‘𝐶)‘(𝐽 − 1)) + 1)))) |