ballotlemsgt1

Description: S maps values less than ( IC ) to values greater than 1. (Contributed by Thierry Arnoux, 28-Apr-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) ⟼ inf (\{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	ballotlemsgt1	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to 1 < S (C) (J)$

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) ⟼ inf (\{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		elfzelz	$⊢ J \in (1 \dots M + N) \to J \in ℤ$
11	10	3ad2ant2	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to J \in ℤ$
12	11	zred	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to J \in ℝ$
13	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)$
14	13	simpld	$⊢ C \in (O ∖ E) \to I (C) \in (1 \dots M + N)$
15	14	elfzelzd	$⊢ C \in (O ∖ E) \to I (C) \in ℤ$
16	15	3ad2ant1	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to I (C) \in ℤ$
17	16	zred	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to I (C) \in ℝ$
18		1red	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to 1 \in ℝ$
19	17 18	readdcld	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to I (C) + 1 \in ℝ$
20		simp3	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to J < I (C)$
21	16	zcnd	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to I (C) \in ℂ$
22		1cnd	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to 1 \in ℂ$
23	21 22	pncand	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to I (C) + 1 - 1 = I (C)$
24	20 23	breqtrrd	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to J < I (C) + 1 - 1$
25	12 19 18 24	ltsub13d	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to 1 < I (C) + 1 - J$
26	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)$
27	26	3adant3	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to S (C) (J) = if (J \leq I (C), I (C) + 1 - J, J)$
28	12 17 20	ltled	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to J \leq I (C)$
29	28	iftrued	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to if (J \leq I (C), I (C) + 1 - J, J) = I (C) + 1 - J$
30	27 29	eqtrd	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to S (C) (J) = I (C) + 1 - J$
31	25 30	breqtrrd	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N) \land J < I (C)) \to 1 < S (C) (J)$

Metamath Proof Explorer

Theorem ballotlemsgt1

Proof