Metamath Proof Explorer


Theorem ballotlemfp1

Description: If the J th ballot is for A, ( FC ) goes up 1. If the J th ballot is for B, ( FC ) goes down 1. (Contributed by Thierry Arnoux, 24-Nov-2016)

Ref Expression
Hypotheses ballotth.m M
ballotth.n N
ballotth.o O = c 𝒫 1 M + N | c = M
ballotth.p P = x 𝒫 O x O
ballotth.f F = c O i 1 i c 1 i c
ballotlemfp1.c φ C O
ballotlemfp1.j φ J
Assertion ballotlemfp1 φ ¬ J C F C J = F C J 1 1 J C F C J = F C J 1 + 1

Proof

Step Hyp Ref Expression
1 ballotth.m M
2 ballotth.n N
3 ballotth.o O = c 𝒫 1 M + N | c = M
4 ballotth.p P = x 𝒫 O x O
5 ballotth.f F = c O i 1 i c 1 i c
6 ballotlemfp1.c φ C O
7 ballotlemfp1.j φ J
8 7 nnzd φ J
9 1 2 3 4 5 6 8 ballotlemfval φ F C J = 1 J C 1 J C
10 9 adantr φ ¬ J C F C J = 1 J C 1 J C
11 fzfi 1 J 1 Fin
12 inss1 1 J 1 C 1 J 1
13 ssfi 1 J 1 Fin 1 J 1 C 1 J 1 1 J 1 C Fin
14 11 12 13 mp2an 1 J 1 C Fin
15 hashcl 1 J 1 C Fin 1 J 1 C 0
16 14 15 ax-mp 1 J 1 C 0
17 16 nn0cni 1 J 1 C
18 17 a1i φ ¬ J C 1 J 1 C
19 diffi 1 J 1 Fin 1 J 1 C Fin
20 11 19 ax-mp 1 J 1 C Fin
21 hashcl 1 J 1 C Fin 1 J 1 C 0
22 20 21 ax-mp 1 J 1 C 0
23 22 nn0cni 1 J 1 C
24 23 a1i φ ¬ J C 1 J 1 C
25 1cnd φ ¬ J C 1
26 18 24 25 subsub4d φ ¬ J C 1 J 1 C - 1 J 1 C - 1 = 1 J 1 C 1 J 1 C + 1
27 1zzd φ 1
28 8 27 zsubcld φ J 1
29 1 2 3 4 5 6 28 ballotlemfval φ F C J 1 = 1 J 1 C 1 J 1 C
30 29 adantr φ ¬ J C F C J 1 = 1 J 1 C 1 J 1 C
31 30 oveq1d φ ¬ J C F C J 1 1 = 1 J 1 C - 1 J 1 C - 1
32 elnnuz J J 1
33 7 32 sylib φ J 1
34 fzspl J 1 1 J = 1 J 1 J
35 34 ineq1d J 1 1 J C = 1 J 1 J C
36 indir 1 J 1 J C = 1 J 1 C J C
37 35 36 eqtrdi J 1 1 J C = 1 J 1 C J C
38 33 37 syl φ 1 J C = 1 J 1 C J C
39 38 adantr φ ¬ J C 1 J C = 1 J 1 C J C
40 disjsn C J = ¬ J C
41 incom C J = J C
42 41 eqeq1i C J = J C =
43 40 42 sylbb1 ¬ J C J C =
44 43 adantl φ ¬ J C J C =
45 44 uneq2d φ ¬ J C 1 J 1 C J C = 1 J 1 C
46 un0 1 J 1 C = 1 J 1 C
47 45 46 eqtrdi φ ¬ J C 1 J 1 C J C = 1 J 1 C
48 39 47 eqtrd φ ¬ J C 1 J C = 1 J 1 C
49 48 fveq2d φ ¬ J C 1 J C = 1 J 1 C
50 34 difeq1d J 1 1 J C = 1 J 1 J C
51 difundir 1 J 1 J C = 1 J 1 C J C
52 50 51 eqtrdi J 1 1 J C = 1 J 1 C J C
53 33 52 syl φ 1 J C = 1 J 1 C J C
54 disj3 J C = J = J C
55 43 54 sylib ¬ J C J = J C
56 55 eqcomd ¬ J C J C = J
57 56 uneq2d ¬ J C 1 J 1 C J C = 1 J 1 C J
58 53 57 sylan9eq φ ¬ J C 1 J C = 1 J 1 C J
59 58 fveq2d φ ¬ J C 1 J C = 1 J 1 C J
60 8 adantr φ ¬ J C J
61 uzid J J J
62 uznfz J J ¬ J 1 J 1
63 8 61 62 3syl φ ¬ J 1 J 1
64 63 adantr φ ¬ J C ¬ J 1 J 1
65 difss 1 J 1 C 1 J 1
66 65 sseli J 1 J 1 C J 1 J 1
67 64 66 nsyl φ ¬ J C ¬ J 1 J 1 C
68 ssfi 1 J 1 Fin 1 J 1 C 1 J 1 1 J 1 C Fin
69 11 65 68 mp2an 1 J 1 C Fin
70 67 69 jctil φ ¬ J C 1 J 1 C Fin ¬ J 1 J 1 C
71 hashunsng J 1 J 1 C Fin ¬ J 1 J 1 C 1 J 1 C J = 1 J 1 C + 1
72 60 70 71 sylc φ ¬ J C 1 J 1 C J = 1 J 1 C + 1
73 59 72 eqtrd φ ¬ J C 1 J C = 1 J 1 C + 1
74 49 73 oveq12d φ ¬ J C 1 J C 1 J C = 1 J 1 C 1 J 1 C + 1
75 26 31 74 3eqtr4rd φ ¬ J C 1 J C 1 J C = F C J 1 1
76 10 75 eqtrd φ ¬ J C F C J = F C J 1 1
77 76 ex φ ¬ J C F C J = F C J 1 1
78 9 adantr φ J C F C J = 1 J C 1 J C
79 17 a1i φ J C 1 J 1 C
80 1cnd φ J C 1
81 23 a1i φ J C 1 J 1 C
82 79 80 81 addsubd φ J C 1 J 1 C + 1 - 1 J 1 C = 1 J 1 C - 1 J 1 C + 1
83 38 fveq2d φ 1 J C = 1 J 1 C J C
84 83 adantr φ J C 1 J C = 1 J 1 C J C
85 snssi J C J C
86 df-ss J C J C = J
87 85 86 sylib J C J C = J
88 87 uneq2d J C 1 J 1 C J C = 1 J 1 C J
89 88 fveq2d J C 1 J 1 C J C = 1 J 1 C J
90 89 adantl φ J C 1 J 1 C J C = 1 J 1 C J
91 simpr φ J C J C
92 8 adantr φ J C J
93 92 61 62 3syl φ J C ¬ J 1 J 1
94 12 sseli J 1 J 1 C J 1 J 1
95 93 94 nsyl φ J C ¬ J 1 J 1 C
96 95 14 jctil φ J C 1 J 1 C Fin ¬ J 1 J 1 C
97 hashunsng J C 1 J 1 C Fin ¬ J 1 J 1 C 1 J 1 C J = 1 J 1 C + 1
98 91 96 97 sylc φ J C 1 J 1 C J = 1 J 1 C + 1
99 84 90 98 3eqtrd φ J C 1 J C = 1 J 1 C + 1
100 53 fveq2d φ 1 J C = 1 J 1 C J C
101 100 adantr φ J C 1 J C = 1 J 1 C J C
102 difin2 J C J C = C C J
103 difid C C =
104 103 ineq1i C C J = J
105 0in J =
106 104 105 eqtri C C J =
107 102 106 eqtrdi J C J C =
108 85 107 syl J C J C =
109 108 uneq2d J C 1 J 1 C J C = 1 J 1 C
110 109 fveq2d J C 1 J 1 C J C = 1 J 1 C
111 110 adantl φ J C 1 J 1 C J C = 1 J 1 C
112 un0 1 J 1 C = 1 J 1 C
113 112 a1i φ J C 1 J 1 C = 1 J 1 C
114 113 fveq2d φ J C 1 J 1 C = 1 J 1 C
115 101 111 114 3eqtrd φ J C 1 J C = 1 J 1 C
116 99 115 oveq12d φ J C 1 J C 1 J C = 1 J 1 C + 1 - 1 J 1 C
117 29 adantr φ J C F C J 1 = 1 J 1 C 1 J 1 C
118 117 oveq1d φ J C F C J 1 + 1 = 1 J 1 C - 1 J 1 C + 1
119 82 116 118 3eqtr4d φ J C 1 J C 1 J C = F C J 1 + 1
120 78 119 eqtrd φ J C F C J = F C J 1 + 1
121 120 ex φ J C F C J = F C J 1 + 1
122 77 121 jca φ ¬ J C F C J = F C J 1 1 J C F C J = F C J 1 + 1