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	42 47 49 51 63	elfzd	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to J \in (1 \dots M + N)$
65	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)$
66	64 65	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)$
67		simpr	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to J \in (1 \dots I (C))$
68		iftrue	$⊢ J \leq I (C) \to if (J \leq I (C), I (C) + 1 - J, J) = I (C) + 1 - J$
69	67 58 68	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$
70	66 69	eqtrd	$⊢ (C \in (O ∖ E) \land J \in (1 \dots I (C))) \to S (C) (J) = I (C) + 1 - J$
71	70	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))$
72	71	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)))$
73	72	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)))$
74	54	ad2antrr	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land k \in ℤ) \to I (C) \in ℤ$
75	74	zcnd	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land k \in ℤ) \to I (C) \in ℂ$
76		1cnd	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land k \in ℤ) \to 1 \in ℂ$
77	75 76	pncand	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land k \in ℤ) \to I (C) + 1 - 1 = I (C)$
78	77	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))$
79	78	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)))$
80		1zzd	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land k \in ℤ) \to 1 \in ℤ$
81	48	ad2antlr	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land k \in ℤ) \to J \in ℤ$
82	74	peano2zd	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land k \in ℤ) \to I (C) + 1 \in ℤ$
83		simpr	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land k \in ℤ) \to k \in ℤ$
84		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))$
85	80 81 82 83 84	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))$
86	73 79 85	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))$
87		risset	$⊢ I (C) + 1 - k \in (1 \dots J) \leftrightarrow \exists j \in (1 \dots J) j = I (C) + 1 - k$
88	87	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)$
89		eqcom	$⊢ I (C) + 1 - k = j \leftrightarrow j = I (C) + 1 - k$
90	54	ad2antrr	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land j \in (1 \dots J)) \to I (C) \in ℤ$
91	90	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 ℤ$
92	91	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 ℂ$
93		1cnd	$⊢ (((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land k \in ℤ) \land j \in (1 \dots J)) \to 1 \in ℂ$
94	92 93	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 ℂ$
95		simplr	$⊢ (((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land k \in ℤ) \land j \in (1 \dots J)) \to k \in ℤ$
96	95	zcnd	$⊢ (((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land k \in ℤ) \land j \in (1 \dots J)) \to k \in ℂ$
97		elfzelz	$⊢ j \in (1 \dots J) \to j \in ℤ$
98	97	adantl	$⊢ (((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land k \in ℤ) \land j \in (1 \dots J)) \to j \in ℤ$
99	98	zcnd	$⊢ (((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land k \in ℤ) \land j \in (1 \dots J)) \to j \in ℂ$
100		subsub23	$⊢ (I (C) + 1 \in ℂ \land k \in ℂ \land j \in ℂ) \to (I (C) + 1 - k = j \leftrightarrow I (C) + 1 - j = k)$
101	94 96 99 100	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)$
102	89 101	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)$
103		simpll	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land j \in (1 \dots J)) \to C \in (O ∖ E)$
104	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)$
105	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)$
106	103 104 105	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)$
107	97	adantl	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land j \in (1 \dots J)) \to j \in ℤ$
108	107	zred	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land j \in (1 \dots J)) \to j \in ℝ$
109	48	ad2antlr	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land j \in (1 \dots J)) \to J \in ℤ$
110	109	zred	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land j \in (1 \dots J)) \to J \in ℝ$
111	90	zred	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land j \in (1 \dots J)) \to I (C) \in ℝ$
112		elfzle2	$⊢ j \in (1 \dots J) \to j \leq J$
113	112	adantl	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land j \in (1 \dots J)) \to j \leq J$
114	58	ad2antlr	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land j \in (1 \dots J)) \to J \leq I (C)$
115	108 110 111 113 114	letrd	$⊢ ((C \in (O ∖ E) \land J \in (1 \dots I (C))) \land j \in (1 \dots J)) \to j \leq I (C)$
116		iftrue	$⊢ j \leq I (C) \to if (j \leq I (C), I (C) + 1 - j, j) = I (C) + 1 - j$
117	115 116	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$
118	106 117	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$
119	118	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)$
120	119	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)$
121	102 120	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)$
122	121	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)$
123	86 88 122	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)$
124	41 123	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)))$
125	22 24 124	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