cvmliftlem2

Description: Lemma for cvmlift . W = [ ( k - 1 ) / N , k / N ] is a subset of [ 0 , 1 ] for each M e. ( 1 ... N ) . (Contributed by Mario Carneiro, 16-Feb-2015)

	Ref	Expression
Hypotheses	cvmliftlem.1	$⊢ S = (k \in J ⟼ \{s \in (𝒫 C ∖ \{\emptyset\}) \| (⋃ s = F^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {F ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k))))\})$
	cvmliftlem.b	$⊢ B = ⋃ C$
	cvmliftlem.x	$⊢ X = ⋃ J$
	cvmliftlem.f	$⊢ φ \to F \in (C CovMap J)$
	cvmliftlem.g	$⊢ φ \to G \in (II Cn J)$
	cvmliftlem.p	$⊢ φ \to P \in B$
	cvmliftlem.e	$⊢ φ \to F (P) = G (0)$
	cvmliftlem.n	$⊢ φ \to N \in ℕ$
	cvmliftlem.t	$⊢ φ \to T : (1 \dots N) ⟶ ⋃_{j \in J} (\{j\} \times S (j))$
	cvmliftlem.a	$⊢ φ \to \forall k \in (1 \dots N) G [[\frac{k - 1}{N}, \frac{k}{N}]] \subseteq 1^{st} (T (k))$
	cvmliftlem.l	$⊢ L = topGen (ran (.))$
	cvmliftlem1.m	$⊢ (φ \land ψ) \to M \in (1 \dots N)$
	cvmliftlem3.3	$⊢ W = [\frac{M - 1}{N}, \frac{M}{N}]$
Assertion	cvmliftlem2	$⊢ (φ \land ψ) \to W \subseteq [0, 1]$

Proof

Step	Hyp	Ref	Expression
1		cvmliftlem.1	$⊢ S = (k \in J ⟼ \{s \in (𝒫 C ∖ \{\emptyset\}) \| (⋃ s = F^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {F ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k))))\})$
2		cvmliftlem.b	$⊢ B = ⋃ C$
3		cvmliftlem.x	$⊢ X = ⋃ J$
4		cvmliftlem.f	$⊢ φ \to F \in (C CovMap J)$
5		cvmliftlem.g	$⊢ φ \to G \in (II Cn J)$
6		cvmliftlem.p	$⊢ φ \to P \in B$
7		cvmliftlem.e	$⊢ φ \to F (P) = G (0)$
8		cvmliftlem.n	$⊢ φ \to N \in ℕ$
9		cvmliftlem.t	$⊢ φ \to T : (1 \dots N) ⟶ ⋃_{j \in J} (\{j\} \times S (j))$
10		cvmliftlem.a	$⊢ φ \to \forall k \in (1 \dots N) G [[\frac{k - 1}{N}, \frac{k}{N}]] \subseteq 1^{st} (T (k))$
11		cvmliftlem.l	$⊢ L = topGen (ran (.))$
12		cvmliftlem1.m	$⊢ (φ \land ψ) \to M \in (1 \dots N)$
13		cvmliftlem3.3	$⊢ W = [\frac{M - 1}{N}, \frac{M}{N}]$
14		0red	$⊢ (φ \land ψ) \to 0 \in ℝ$
15		1red	$⊢ (φ \land ψ) \to 1 \in ℝ$
16		elfznn	$⊢ M \in (1 \dots N) \to M \in ℕ$
17	12 16	syl	$⊢ (φ \land ψ) \to M \in ℕ$
18	17	nnred	$⊢ (φ \land ψ) \to M \in ℝ$
19		peano2rem	$⊢ M \in ℝ \to M - 1 \in ℝ$
20	18 19	syl	$⊢ (φ \land ψ) \to M - 1 \in ℝ$
21		nnm1nn0	$⊢ M \in ℕ \to M - 1 \in ℕ_{0}$
22	17 21	syl	$⊢ (φ \land ψ) \to M - 1 \in ℕ_{0}$
23	22	nn0ge0d	$⊢ (φ \land ψ) \to 0 \leq M - 1$
24	8	adantr	$⊢ (φ \land ψ) \to N \in ℕ$
25	24	nnred	$⊢ (φ \land ψ) \to N \in ℝ$
26	24	nngt0d	$⊢ (φ \land ψ) \to 0 < N$
27		divge0	$⊢ ((M - 1 \in ℝ \land 0 \leq M - 1) \land (N \in ℝ \land 0 < N)) \to 0 \leq \frac{M - 1}{N}$
28	20 23 25 26 27	syl22anc	$⊢ (φ \land ψ) \to 0 \leq \frac{M - 1}{N}$
29		elfzle2	$⊢ M \in (1 \dots N) \to M \leq N$
30	12 29	syl	$⊢ (φ \land ψ) \to M \leq N$
31	24	nncnd	$⊢ (φ \land ψ) \to N \in ℂ$
32	31	mulid1d	$⊢ (φ \land ψ) \to N \cdot 1 = N$
33	30 32	breqtrrd	$⊢ (φ \land ψ) \to M \leq N \cdot 1$
34		ledivmul	$⊢ (M \in ℝ \land 1 \in ℝ \land (N \in ℝ \land 0 < N)) \to (\frac{M}{N} \leq 1 \leftrightarrow M \leq N \cdot 1)$
35	18 15 25 26 34	syl112anc	$⊢ (φ \land ψ) \to (\frac{M}{N} \leq 1 \leftrightarrow M \leq N \cdot 1)$
36	33 35	mpbird	$⊢ (φ \land ψ) \to \frac{M}{N} \leq 1$
37		iccss	$⊢ ((0 \in ℝ \land 1 \in ℝ) \land (0 \leq \frac{M - 1}{N} \land \frac{M}{N} \leq 1)) \to [\frac{M - 1}{N}, \frac{M}{N}] \subseteq [0, 1]$
38	14 15 28 36 37	syl22anc	$⊢ (φ \land ψ) \to [\frac{M - 1}{N}, \frac{M}{N}] \subseteq [0, 1]$
39	13 38	eqsstrid	$⊢ (φ \land ψ) \to W \subseteq [0, 1]$

Metamath Proof Explorer

Theorem cvmliftlem2

Proof