ballotlemsima

Description: The image by S of an interval before the first pick. (Contributed by Thierry Arnoux, 5-May-2017)

	Ref	Expression
Hypotheses	ballotth.m	$⊢ M \in ℕ$
	ballotth.n	$⊢ N \in ℕ$
	ballotth.o	$⊢ O = \{c \in 𝒫 (1 \dots M + N) \| \|c\| = M\}$
	ballotth.p	$⊢ P = (x \in 𝒫 O ⟼ \frac{\|x\|}{\|O\|})$
	ballotth.f	$⊢ F = (c \in O ⟼ (i \in ℤ ⟼ \|(1 \dots i) \cap c\| - \|(1 \dots i) ∖ c\|))$
	ballotth.e	$⊢ E = \{c \in O \| \forall i \in (1 \dots M + N) 0 < F (c) (i)\}$
	ballotth.mgtn	$⊢ N < M$
	ballotth.i	$⊢ I = (c \in (O ∖ E) ⟼ sup (\{k \in (1 \dots M + N) \| F (c) (k) = 0\} ℝ <))$
	ballotth.s	$⊢ S = (c \in (O ∖ E) ⟼ (i \in (1 \dots M + N) ⟼ if (i \leq I (c), I (c) + 1 - i, i)))$
Assertion	ballotlemsima	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to S (C) [(1 \dots J)] = (S (C) (J) \dots I (C))$

Proof

Step	Hyp	Ref	Expression
1		ballotth.m	$⊢ M \in ℕ$
2		ballotth.n	$⊢ N \in ℕ$
3		ballotth.o	$⊢ O = \{c \in 𝒫 (1 \dots M + N) \| \|c\| = M\}$
4		ballotth.p	$⊢ P = (x \in 𝒫 O ⟼ \frac{\|x\|}{\|O\|})$
5		ballotth.f	$⊢ F = (c \in O ⟼ (i \in ℤ ⟼ \|(1 \dots i) \cap c\| - \|(1 \dots i) ∖ c\|))$
6		ballotth.e	$⊢ E = \{c \in O \| \forall i \in (1 \dots M + N) 0 < F (c) (i)\}$
7		ballotth.mgtn	$⊢ N < M$
8		ballotth.i	$⊢ I = (c \in (O ∖ E) ⟼ sup (\{k \in (1 \dots M + N) \| F (c) (k) = 0\} ℝ <))$
9		ballotth.s	$⊢ S = (c \in (O ∖ E) ⟼ (i \in (1 \dots M + N) ⟼ if (i \leq I (c), I (c) + 1 - i, i)))$
10		imassrn	$⊢ S (C) [(1 \dots J)] \subseteq ran S (C)$
11	1 2 3 4 5 6 7 8 9	ballotlemsf1o	$⊢ C \in (O ∖ E) \to (S (C) : (1 \dots M + N) \underset{1-1 onto}{⟶} (1 \dots M + N) \land {S (C)}^{-1} = S (C))$
12	11	simpld	$⊢ C \in (O ∖ E) \to S (C) : (1 \dots M + N) \underset{1-1 onto}{⟶} (1 \dots M + N)$
13		f1of	$⊢ S (C) : (1 \dots M + N) \underset{1-1 onto}{⟶} (1 \dots M + N) \to S (C) : (1 \dots M + N) ⟶ (1 \dots M + N)$
14		frn	$⊢ S (C) : (1 \dots M + N) ⟶ (1 \dots M + N) \to ran S (C) \subseteq (1 \dots M + N)$
15	12 13 14	3syl	$⊢ C \in (O ∖ E) \to ran S (C) \subseteq (1 \dots M + N)$
16	10 15	sstrid	$⊢ C \in (O ∖ E) \to S (C) [(1 \dots J)] \subseteq (1 \dots M + N)$
17		fzssuz	$⊢ (1 \dots M + N) \subseteq ℤ_{\geq 1}$
18		uzssz	$⊢ ℤ_{\geq 1} \subseteq ℤ$
19	17 18	sstri	$⊢ (1 \dots M + N) \subseteq ℤ$
20	16 19	sstrdi	$⊢ C \in (O ∖ E) \to S (C) [(1 \dots J)] \subseteq ℤ$
21	20	adantr	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to S (C) [(1 \dots J)] \subseteq ℤ$
22	21	sselda	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land k \in S (C) [(1 \dots J)]) \to k \in ℤ$
23		elfzelz	$⊢ k \in (S (C) (J) \dots I (C)) \to k \in ℤ$
24	23	adantl	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land k \in (S (C) (J) \dots I (C))) \to k \in ℤ$
25		f1ofn	$⊢ S (C) : (1 \dots M + N) \underset{1-1 onto}{⟶} (1 \dots M + N) \to S (C) Fn (1 \dots M + N)$
26	12 25	syl	$⊢ C \in (O ∖ E) \to S (C) Fn (1 \dots M + N)$
27	26	adantr	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to S (C) Fn (1 \dots M + N)$
28	1 2 3 4 5 6 7 8	ballotlemiex	$⊢ C \in (O ∖ E) \to (I (C) \in (1 \dots M + N) \land F (C) (I (C)) = 0)$
29	28	simpld	$⊢ C \in (O ∖ E) \to I (C) \in (1 \dots M + N)$
30	29	adantr	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to I (C) \in (1 \dots M + N)$
31		elfzuz3	$⊢ I (C) \in (1 \dots M + N) \to M + N \in ℤ_{\geq I (C)}$
32	30 31	syl	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to M + N \in ℤ_{\geq I (C)}$
33		elfzuz3	$⊢ J \in (1 \dots I (C)) \to I (C) \in ℤ_{\geq J}$
34	33	adantl	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to I (C) \in ℤ_{\geq J}$
35		uztrn	$⊢ (M + N \in ℤ_{\geq I (C)} \land I (C) \in ℤ_{\geq J}) \to M + N \in ℤ_{\geq J}$
36	32 34 35	syl2anc	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to M + N \in ℤ_{\geq J}$
37		fzss2	$⊢ M + N \in ℤ_{\geq J} \to (1 \dots J) \subseteq (1 \dots M + N)$
38	36 37	syl	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to (1 \dots J) \subseteq (1 \dots M + N)$
39		fvelimab	$⊢ (S (C) Fn (1 \dots M + N) \land (1 \dots J) \subseteq (1 \dots M + N)) \to (k \in S (C) [(1 \dots J)] \leftrightarrow \exists j \in (1 \dots J) S (C) (j) = k)$
40	27 38 39	syl2anc	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to (k \in S (C) [(1 \dots J)] \leftrightarrow \exists j \in (1 \dots J) S (C) (j) = k)$
41	40	adantr	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land k \in ℤ) \to (k \in S (C) [(1 \dots J)] \leftrightarrow \exists j \in (1 \dots J) S (C) (j) = k)$
42		1zzd	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to 1 \in ℤ$
43	1	nnzi	$⊢ M \in ℤ$
44	2	nnzi	$⊢ N \in ℤ$
45		zaddcl	$⊢ (M \in ℤ \land N \in ℤ) \to M + N \in ℤ$
46	43 44 45	mp2an	$⊢ M + N \in ℤ$
47	46	a1i	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to M + N \in ℤ$
48		elfzelz	$⊢ J \in (1 \dots I (C)) \to J \in ℤ$
49	48	adantl	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to J \in ℤ$
50		elfzle1	$⊢ J \in (1 \dots I (C)) \to 1 \leq J$
51	50	adantl	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to 1 \leq J$
52	49	zred	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to J \in ℝ$
53		elfzelz	$⊢ I (C) \in (1 \dots M + N) \to I (C) \in ℤ$
54	29 53	syl	$⊢ C \in (O ∖ E) \to I (C) \in ℤ$
55	54	adantr	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to I (C) \in ℤ$
56	55	zred	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to I (C) \in ℝ$
57	47	zred	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to M + N \in ℝ$
58		elfzle2	$⊢ J \in (1 \dots I (C)) \to J \leq I (C)$
59	58	adantl	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to J \leq I (C)$
60		elfzle2	$⊢ I (C) \in (1 \dots M + N) \to I (C) \leq M + N$
61	29 60	syl	$⊢ C \in (O ∖ E) \to I (C) \leq M + N$
62	61	adantr	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to I (C) \leq M + N$
63	52 56 57 59 62	letrd	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to J \leq M + N$
64		elfz4	$⊢ ((1 \in ℤ \land M + N \in ℤ \land J \in ℤ) \land (1 \leq J \land J \leq M + N)) \to J \in (1 \dots M + N)$
65	42 47 49 51 63 64	syl32anc	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to J \in (1 \dots M + N)$
66	1 2 3 4 5 6 7 8 9	ballotlemsv	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N)) \to S (C) (J) = if (J \leq I (C), I (C) + 1 - J, J)$
67	65 66	syldan	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to S (C) (J) = if (J \leq I (C), I (C) + 1 - J, J)$
68		simpr	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to J \in (1 \dots I (C))$
69		iftrue	$⊢ J \leq I (C) \to if (J \leq I (C), I (C) + 1 - J, J) = I (C) + 1 - J$
70	68 58 69	3syl	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to if (J \leq I (C), I (C) + 1 - J, J) = I (C) + 1 - J$
71	67 70	eqtrd	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to S (C) (J) = I (C) + 1 - J$
72	71	oveq1d	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to (S (C) (J) \dots I (C)) = (I (C) + 1 - J \dots I (C))$
73	72	eleq2d	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to (k \in (S (C) (J) \dots I (C)) \leftrightarrow k \in (I (C) + 1 - J \dots I (C)))$
74	73	adantr	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land k \in ℤ) \to (k \in (S (C) (J) \dots I (C)) \leftrightarrow k \in (I (C) + 1 - J \dots I (C)))$
75	54	ad2antrr	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land k \in ℤ) \to I (C) \in ℤ$
76	75	zcnd	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land k \in ℤ) \to I (C) \in ℂ$
77		1cnd	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land k \in ℤ) \to 1 \in ℂ$
78	76 77	pncand	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land k \in ℤ) \to I (C) + 1 - 1 = I (C)$
79	78	oveq2d	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land k \in ℤ) \to (I (C) + 1 - J \dots I (C) + 1 - 1) = (I (C) + 1 - J \dots I (C))$
80	79	eleq2d	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land k \in ℤ) \to (k \in (I (C) + 1 - J \dots I (C) + 1 - 1) \leftrightarrow k \in (I (C) + 1 - J \dots I (C)))$
81		1zzd	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land k \in ℤ) \to 1 \in ℤ$
82	48	ad2antlr	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land k \in ℤ) \to J \in ℤ$
83	75	peano2zd	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land k \in ℤ) \to I (C) + 1 \in ℤ$
84		simpr	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land k \in ℤ) \to k \in ℤ$
85		fzrev	$⊢ ((1 \in ℤ \land J \in ℤ) \land (I (C) + 1 \in ℤ \land k \in ℤ)) \to (k \in (I (C) + 1 - J \dots I (C) + 1 - 1) \leftrightarrow I (C) + 1 - k \in (1 \dots J))$
86	81 82 83 84 85	syl22anc	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land k \in ℤ) \to (k \in (I (C) + 1 - J \dots I (C) + 1 - 1) \leftrightarrow I (C) + 1 - k \in (1 \dots J))$
87	74 80 86	3bitr2d	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land k \in ℤ) \to (k \in (S (C) (J) \dots I (C)) \leftrightarrow I (C) + 1 - k \in (1 \dots J))$
88		risset	$⊢ I (C) + 1 - k \in (1 \dots J) \leftrightarrow \exists j \in (1 \dots J) j = I (C) + 1 - k$
89	88	a1i	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land k \in ℤ) \to (I (C) + 1 - k \in (1 \dots J) \leftrightarrow \exists j \in (1 \dots J) j = I (C) + 1 - k)$
90		eqcom	$⊢ I (C) + 1 - k = j \leftrightarrow j = I (C) + 1 - k$
91	54	ad2antrr	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land j \in (1 \dots J)) \to I (C) \in ℤ$
92	91	adantlr	$⊢ (((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land k \in ℤ) \land j \in (1 \dots J)) \to I (C) \in ℤ$
93	92	zcnd	$⊢ (((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land k \in ℤ) \land j \in (1 \dots J)) \to I (C) \in ℂ$
94		1cnd	$⊢ (((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land k \in ℤ) \land j \in (1 \dots J)) \to 1 \in ℂ$
95	93 94	addcld	$⊢ (((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land k \in ℤ) \land j \in (1 \dots J)) \to I (C) + 1 \in ℂ$
96		simplr	$⊢ (((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land k \in ℤ) \land j \in (1 \dots J)) \to k \in ℤ$
97	96	zcnd	$⊢ (((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land k \in ℤ) \land j \in (1 \dots J)) \to k \in ℂ$
98		elfzelz	$⊢ j \in (1 \dots J) \to j \in ℤ$
99	98	adantl	$⊢ (((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land k \in ℤ) \land j \in (1 \dots J)) \to j \in ℤ$
100	99	zcnd	$⊢ (((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land k \in ℤ) \land j \in (1 \dots J)) \to j \in ℂ$
101		subsub23	$⊢ (I (C) + 1 \in ℂ \land k \in ℂ \land j \in ℂ) \to (I (C) + 1 - k = j \leftrightarrow I (C) + 1 - j = k)$
102	95 97 100 101	syl3anc	$⊢ (((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land k \in ℤ) \land j \in (1 \dots J)) \to (I (C) + 1 - k = j \leftrightarrow I (C) + 1 - j = k)$
103	90 102	bitr3id	$⊢ (((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land k \in ℤ) \land j \in (1 \dots J)) \to (j = I (C) + 1 - k \leftrightarrow I (C) + 1 - j = k)$
104		simpll	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land j \in (1 \dots J)) \to C \in (O ∖ E)$
105	38	sselda	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land j \in (1 \dots J)) \to j \in (1 \dots M + N)$
106	1 2 3 4 5 6 7 8 9	ballotlemsv	$⊢ (C \in (O ∖ E) \land j \in (1 \dots M + N)) \to S (C) (j) = if (j \leq I (C), I (C) + 1 - j, j)$
107	104 105 106	syl2anc	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land j \in (1 \dots J)) \to S (C) (j) = if (j \leq I (C), I (C) + 1 - j, j)$
108	98	adantl	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land j \in (1 \dots J)) \to j \in ℤ$
109	108	zred	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land j \in (1 \dots J)) \to j \in ℝ$
110	48	ad2antlr	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land j \in (1 \dots J)) \to J \in ℤ$
111	110	zred	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land j \in (1 \dots J)) \to J \in ℝ$
112	91	zred	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land j \in (1 \dots J)) \to I (C) \in ℝ$
113		elfzle2	$⊢ j \in (1 \dots J) \to j \leq J$
114	113	adantl	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land j \in (1 \dots J)) \to j \leq J$
115	58	ad2antlr	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land j \in (1 \dots J)) \to J \leq I (C)$
116	109 111 112 114 115	letrd	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land j \in (1 \dots J)) \to j \leq I (C)$
117		iftrue	$⊢ j \leq I (C) \to if (j \leq I (C), I (C) + 1 - j, j) = I (C) + 1 - j$
118	116 117	syl	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land j \in (1 \dots J)) \to if (j \leq I (C), I (C) + 1 - j, j) = I (C) + 1 - j$
119	107 118	eqtrd	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land j \in (1 \dots J)) \to S (C) (j) = I (C) + 1 - j$
120	119	eqeq1d	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land j \in (1 \dots J)) \to (S (C) (j) = k \leftrightarrow I (C) + 1 - j = k)$
121	120	adantlr	$⊢ (((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land k \in ℤ) \land j \in (1 \dots J)) \to (S (C) (j) = k \leftrightarrow I (C) + 1 - j = k)$
122	103 121	bitr4d	$⊢ (((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land k \in ℤ) \land j \in (1 \dots J)) \to (j = I (C) + 1 - k \leftrightarrow S (C) (j) = k)$
123	122	rexbidva	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land k \in ℤ) \to (\exists j \in (1 \dots J) j = I (C) + 1 - k \leftrightarrow \exists j \in (1 \dots J) S (C) (j) = k)$
124	87 89 123	3bitrd	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land k \in ℤ) \to (k \in (S (C) (J) \dots I (C)) \leftrightarrow \exists j \in (1 \dots J) S (C) (j) = k)$
125	41 124	bitr4d	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land k \in ℤ) \to (k \in S (C) [(1 \dots J)] \leftrightarrow k \in (S (C) (J) \dots I (C)))$
126	22 24 125	eqrdav	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to S (C) [(1 \dots J)] = (S (C) (J) \dots I (C))$

Metamath Proof Explorer

Theorem ballotlemsima

Proof