prmreclem5

Description: Lemma for prmrec . Here we show the inequality N / 2 < # M by decomposing the set ( 1 ... N ) into the disjoint union of the set M of those numbers that are not divisible by any "large" primes (above K ) and the indexed union over K < k of the numbers Wk that divide the prime k . By prmreclem4 the second of these has size less than N times the prime reciprocal series, which is less than 1 / 2 by assumption, we find that the complementary part M must be at least N / 2 large. (Contributed by Mario Carneiro, 6-Aug-2014)

	Ref	Expression
Hypotheses	prmrec.1	$⊢ F = (n \in ℕ ⟼ if (n \in ℙ, \frac{1}{n}, 0))$
	prmrec.2	$⊢ φ \to K \in ℕ$
	prmrec.3	$⊢ φ \to N \in ℕ$
	prmrec.4	$⊢ M = \{n \in (1 \dots N) \| \forall p \in (ℙ ∖ (1 \dots K)) \neg p ∥ n\}$
	prmrec.5	$⊢ φ \to seq 1 (+ F) \in dom ⇝$
	prmrec.6	$⊢ φ \to \sum_{k \in ℤ_{\geq (K + 1)}} if (k \in ℙ, \frac{1}{k}, 0) < \frac{1}{2}$
	prmrec.7	$⊢ W = (p \in ℕ ⟼ \{n \in (1 \dots N) \| (p \in ℙ \land p ∥ n)\})$
Assertion	prmreclem5	$⊢ φ \to \frac{N}{2} < 2^{K} \sqrt{N}$

Proof

Step	Hyp	Ref	Expression
1		prmrec.1	$⊢ F = (n \in ℕ ⟼ if (n \in ℙ, \frac{1}{n}, 0))$
2		prmrec.2	$⊢ φ \to K \in ℕ$
3		prmrec.3	$⊢ φ \to N \in ℕ$
4		prmrec.4	$⊢ M = \{n \in (1 \dots N) \| \forall p \in (ℙ ∖ (1 \dots K)) \neg p ∥ n\}$
5		prmrec.5	$⊢ φ \to seq 1 (+ F) \in dom ⇝$
6		prmrec.6	$⊢ φ \to \sum_{k \in ℤ_{\geq (K + 1)}} if (k \in ℙ, \frac{1}{k}, 0) < \frac{1}{2}$
7		prmrec.7	$⊢ W = (p \in ℕ ⟼ \{n \in (1 \dots N) \| (p \in ℙ \land p ∥ n)\})$
8	3	nnred	$⊢ φ \to N \in ℝ$
9	8	rehalfcld	$⊢ φ \to \frac{N}{2} \in ℝ$
10		fzfi	$⊢ (1 \dots N) \in Fin$
11	4	ssrab3	$⊢ M \subseteq (1 \dots N)$
12		ssfi	$⊢ ((1 \dots N) \in Fin \land M \subseteq (1 \dots N)) \to M \in Fin$
13	10 11 12	mp2an	$⊢ M \in Fin$
14		hashcl	$⊢ M \in Fin \to \|M\| \in ℕ_{0}$
15	13 14	ax-mp	$⊢ \|M\| \in ℕ_{0}$
16	15	nn0rei	$⊢ \|M\| \in ℝ$
17	16	a1i	$⊢ φ \to \|M\| \in ℝ$
18		2nn	$⊢ 2 \in ℕ$
19	2	nnnn0d	$⊢ φ \to K \in ℕ_{0}$
20		nnexpcl	$⊢ (2 \in ℕ \land K \in ℕ_{0}) \to 2^{K} \in ℕ$
21	18 19 20	sylancr	$⊢ φ \to 2^{K} \in ℕ$
22	21	nnred	$⊢ φ \to 2^{K} \in ℝ$
23	3	nnrpd	$⊢ φ \to N \in ℝ^{+}$
24	23	rpsqrtcld	$⊢ φ \to \sqrt{N} \in ℝ^{+}$
25	24	rpred	$⊢ φ \to \sqrt{N} \in ℝ$
26	22 25	remulcld	$⊢ φ \to 2^{K} \sqrt{N} \in ℝ$
27	8	recnd	$⊢ φ \to N \in ℂ$
28	27	2halvesd	$⊢ φ \to (\frac{N}{2}) + (\frac{N}{2}) = N$
29	11	a1i	$⊢ φ \to M \subseteq (1 \dots N)$
30	2	peano2nnd	$⊢ φ \to K + 1 \in ℕ$
31		elfzuz	$⊢ k \in (K + 1 \dots N) \to k \in ℤ_{\geq (K + 1)}$
32		eluznn	$⊢ (K + 1 \in ℕ \land k \in ℤ_{\geq (K + 1)}) \to k \in ℕ$
33	30 31 32	syl2an	$⊢ (φ \land k \in (K + 1 \dots N)) \to k \in ℕ$
34		eleq1w	$⊢ p = k \to (p \in ℙ \leftrightarrow k \in ℙ)$
35		breq1	$⊢ p = k \to (p ∥ n \leftrightarrow k ∥ n)$
36	34 35	anbi12d	$⊢ p = k \to ((p \in ℙ \land p ∥ n) \leftrightarrow (k \in ℙ \land k ∥ n))$
37	36	rabbidv	$⊢ p = k \to \{n \in (1 \dots N) \| (p \in ℙ \land p ∥ n)\} = \{n \in (1 \dots N) \| (k \in ℙ \land k ∥ n)\}$
38		ovex	$⊢ (1 \dots N) \in V$
39	38	rabex	$⊢ \{n \in (1 \dots N) \| (k \in ℙ \land k ∥ n)\} \in V$
40	37 7 39	fvmpt	$⊢ k \in ℕ \to W (k) = \{n \in (1 \dots N) \| (k \in ℙ \land k ∥ n)\}$
41	40	adantl	$⊢ (φ \land k \in ℕ) \to W (k) = \{n \in (1 \dots N) \| (k \in ℙ \land k ∥ n)\}$
42		ssrab2	$⊢ \{n \in (1 \dots N) \| (k \in ℙ \land k ∥ n)\} \subseteq (1 \dots N)$
43	41 42	eqsstrdi	$⊢ (φ \land k \in ℕ) \to W (k) \subseteq (1 \dots N)$
44	33 43	syldan	$⊢ (φ \land k \in (K + 1 \dots N)) \to W (k) \subseteq (1 \dots N)$
45	44	ralrimiva	$⊢ φ \to \forall k \in (K + 1 \dots N) W (k) \subseteq (1 \dots N)$
46		iunss	$⊢ ⋃_{k = K + 1}^{N} W (k) \subseteq (1 \dots N) \leftrightarrow \forall k \in (K + 1 \dots N) W (k) \subseteq (1 \dots N)$
47	45 46	sylibr	$⊢ φ \to ⋃_{k = K + 1}^{N} W (k) \subseteq (1 \dots N)$
48	29 47	unssd	$⊢ φ \to M \cup ⋃_{k = K + 1}^{N} W (k) \subseteq (1 \dots N)$
49		breq1	$⊢ p = q \to (p ∥ n \leftrightarrow q ∥ n)$
50	49	notbid	$⊢ p = q \to (\neg p ∥ n \leftrightarrow \neg q ∥ n)$
51	50	cbvralvw	$⊢ \forall p \in (ℙ ∖ (1 \dots K)) \neg p ∥ n \leftrightarrow \forall q \in (ℙ ∖ (1 \dots K)) \neg q ∥ n$
52		breq2	$⊢ n = x \to (q ∥ n \leftrightarrow q ∥ x)$
53	52	notbid	$⊢ n = x \to (\neg q ∥ n \leftrightarrow \neg q ∥ x)$
54	53	ralbidv	$⊢ n = x \to (\forall q \in (ℙ ∖ (1 \dots K)) \neg q ∥ n \leftrightarrow \forall q \in (ℙ ∖ (1 \dots K)) \neg q ∥ x)$
55	51 54	syl5bb	$⊢ n = x \to (\forall p \in (ℙ ∖ (1 \dots K)) \neg p ∥ n \leftrightarrow \forall q \in (ℙ ∖ (1 \dots K)) \neg q ∥ x)$
56	55 4	elrab2	$⊢ x \in M \leftrightarrow (x \in (1 \dots N) \land \forall q \in (ℙ ∖ (1 \dots K)) \neg q ∥ x)$
57		elun1	$⊢ x \in M \to x \in (M \cup ⋃_{k = K + 1}^{N} W (k))$
58	56 57	sylbir	$⊢ (x \in (1 \dots N) \land \forall q \in (ℙ ∖ (1 \dots K)) \neg q ∥ x) \to x \in (M \cup ⋃_{k = K + 1}^{N} W (k))$
59	58	ex	$⊢ x \in (1 \dots N) \to (\forall q \in (ℙ ∖ (1 \dots K)) \neg q ∥ x \to x \in (M \cup ⋃_{k = K + 1}^{N} W (k)))$
60	59	adantl	$⊢ (φ \land x \in (1 \dots N)) \to (\forall q \in (ℙ ∖ (1 \dots K)) \neg q ∥ x \to x \in (M \cup ⋃_{k = K + 1}^{N} W (k)))$
61		dfrex2	$⊢ \exists q \in (ℙ ∖ (1 \dots K)) q ∥ x \leftrightarrow \neg \forall q \in (ℙ ∖ (1 \dots K)) \neg q ∥ x$
62	2	nnzd	$⊢ φ \to K \in ℤ$
63	62	peano2zd	$⊢ φ \to K + 1 \in ℤ$
64	63	ad2antrr	$⊢ ((φ \land x \in (1 \dots N)) \land (q \in (ℙ ∖ (1 \dots K)) \land q ∥ x)) \to K + 1 \in ℤ$
65	3	nnzd	$⊢ φ \to N \in ℤ$
66	65	ad2antrr	$⊢ ((φ \land x \in (1 \dots N)) \land (q \in (ℙ ∖ (1 \dots K)) \land q ∥ x)) \to N \in ℤ$
67		eldifi	$⊢ q \in (ℙ ∖ (1 \dots K)) \to q \in ℙ$
68	67	ad2antrl	$⊢ ((φ \land x \in (1 \dots N)) \land (q \in (ℙ ∖ (1 \dots K)) \land q ∥ x)) \to q \in ℙ$
69		prmz	$⊢ q \in ℙ \to q \in ℤ$
70	68 69	syl	$⊢ ((φ \land x \in (1 \dots N)) \land (q \in (ℙ ∖ (1 \dots K)) \land q ∥ x)) \to q \in ℤ$
71		eldifn	$⊢ q \in (ℙ ∖ (1 \dots K)) \to \neg q \in (1 \dots K)$
72	71	ad2antrl	$⊢ ((φ \land x \in (1 \dots N)) \land (q \in (ℙ ∖ (1 \dots K)) \land q ∥ x)) \to \neg q \in (1 \dots K)$
73		prmnn	$⊢ q \in ℙ \to q \in ℕ$
74	68 73	syl	$⊢ ((φ \land x \in (1 \dots N)) \land (q \in (ℙ ∖ (1 \dots K)) \land q ∥ x)) \to q \in ℕ$
75		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
76	74 75	eleqtrdi	$⊢ ((φ \land x \in (1 \dots N)) \land (q \in (ℙ ∖ (1 \dots K)) \land q ∥ x)) \to q \in ℤ_{\geq 1}$
77	62	ad2antrr	$⊢ ((φ \land x \in (1 \dots N)) \land (q \in (ℙ ∖ (1 \dots K)) \land q ∥ x)) \to K \in ℤ$
78		elfz5	$⊢ (q \in ℤ_{\geq 1} \land K \in ℤ) \to (q \in (1 \dots K) \leftrightarrow q \leq K)$
79	76 77 78	syl2anc	$⊢ ((φ \land x \in (1 \dots N)) \land (q \in (ℙ ∖ (1 \dots K)) \land q ∥ x)) \to (q \in (1 \dots K) \leftrightarrow q \leq K)$
80	72 79	mtbid	$⊢ ((φ \land x \in (1 \dots N)) \land (q \in (ℙ ∖ (1 \dots K)) \land q ∥ x)) \to \neg q \leq K$
81	2	nnred	$⊢ φ \to K \in ℝ$
82	81	ad2antrr	$⊢ ((φ \land x \in (1 \dots N)) \land (q \in (ℙ ∖ (1 \dots K)) \land q ∥ x)) \to K \in ℝ$
83	74	nnred	$⊢ ((φ \land x \in (1 \dots N)) \land (q \in (ℙ ∖ (1 \dots K)) \land q ∥ x)) \to q \in ℝ$
84	82 83	ltnled	$⊢ ((φ \land x \in (1 \dots N)) \land (q \in (ℙ ∖ (1 \dots K)) \land q ∥ x)) \to (K < q \leftrightarrow \neg q \leq K)$
85	80 84	mpbird	$⊢ ((φ \land x \in (1 \dots N)) \land (q \in (ℙ ∖ (1 \dots K)) \land q ∥ x)) \to K < q$
86		zltp1le	$⊢ (K \in ℤ \land q \in ℤ) \to (K < q \leftrightarrow K + 1 \leq q)$
87	77 70 86	syl2anc	$⊢ ((φ \land x \in (1 \dots N)) \land (q \in (ℙ ∖ (1 \dots K)) \land q ∥ x)) \to (K < q \leftrightarrow K + 1 \leq q)$
88	85 87	mpbid	$⊢ ((φ \land x \in (1 \dots N)) \land (q \in (ℙ ∖ (1 \dots K)) \land q ∥ x)) \to K + 1 \leq q$
89		elfznn	$⊢ x \in (1 \dots N) \to x \in ℕ$
90	89	ad2antlr	$⊢ ((φ \land x \in (1 \dots N)) \land (q \in (ℙ ∖ (1 \dots K)) \land q ∥ x)) \to x \in ℕ$
91	90	nnred	$⊢ ((φ \land x \in (1 \dots N)) \land (q \in (ℙ ∖ (1 \dots K)) \land q ∥ x)) \to x \in ℝ$
92	8	ad2antrr	$⊢ ((φ \land x \in (1 \dots N)) \land (q \in (ℙ ∖ (1 \dots K)) \land q ∥ x)) \to N \in ℝ$
93		simprr	$⊢ ((φ \land x \in (1 \dots N)) \land (q \in (ℙ ∖ (1 \dots K)) \land q ∥ x)) \to q ∥ x$
94		dvdsle	$⊢ (q \in ℤ \land x \in ℕ) \to (q ∥ x \to q \leq x)$
95	70 90 94	syl2anc	$⊢ ((φ \land x \in (1 \dots N)) \land (q \in (ℙ ∖ (1 \dots K)) \land q ∥ x)) \to (q ∥ x \to q \leq x)$
96	93 95	mpd	$⊢ ((φ \land x \in (1 \dots N)) \land (q \in (ℙ ∖ (1 \dots K)) \land q ∥ x)) \to q \leq x$
97		elfzle2	$⊢ x \in (1 \dots N) \to x \leq N$
98	97	ad2antlr	$⊢ ((φ \land x \in (1 \dots N)) \land (q \in (ℙ ∖ (1 \dots K)) \land q ∥ x)) \to x \leq N$
99	83 91 92 96 98	letrd	$⊢ ((φ \land x \in (1 \dots N)) \land (q \in (ℙ ∖ (1 \dots K)) \land q ∥ x)) \to q \leq N$
100	64 66 70 88 99	elfzd	$⊢ ((φ \land x \in (1 \dots N)) \land (q \in (ℙ ∖ (1 \dots K)) \land q ∥ x)) \to q \in (K + 1 \dots N)$
101	52	anbi2d	$⊢ n = x \to ((q \in ℙ \land q ∥ n) \leftrightarrow (q \in ℙ \land q ∥ x))$
102		simplr	$⊢ ((φ \land x \in (1 \dots N)) \land (q \in (ℙ ∖ (1 \dots K)) \land q ∥ x)) \to x \in (1 \dots N)$
103	68 93	jca	$⊢ ((φ \land x \in (1 \dots N)) \land (q \in (ℙ ∖ (1 \dots K)) \land q ∥ x)) \to (q \in ℙ \land q ∥ x)$
104	101 102 103	elrabd	$⊢ ((φ \land x \in (1 \dots N)) \land (q \in (ℙ ∖ (1 \dots K)) \land q ∥ x)) \to x \in \{n \in (1 \dots N) \| (q \in ℙ \land q ∥ n)\}$
105		eleq1w	$⊢ p = q \to (p \in ℙ \leftrightarrow q \in ℙ)$
106	105 49	anbi12d	$⊢ p = q \to ((p \in ℙ \land p ∥ n) \leftrightarrow (q \in ℙ \land q ∥ n))$
107	106	rabbidv	$⊢ p = q \to \{n \in (1 \dots N) \| (p \in ℙ \land p ∥ n)\} = \{n \in (1 \dots N) \| (q \in ℙ \land q ∥ n)\}$
108	38	rabex	$⊢ \{n \in (1 \dots N) \| (q \in ℙ \land q ∥ n)\} \in V$
109	107 7 108	fvmpt	$⊢ q \in ℕ \to W (q) = \{n \in (1 \dots N) \| (q \in ℙ \land q ∥ n)\}$
110	74 109	syl	$⊢ ((φ \land x \in (1 \dots N)) \land (q \in (ℙ ∖ (1 \dots K)) \land q ∥ x)) \to W (q) = \{n \in (1 \dots N) \| (q \in ℙ \land q ∥ n)\}$
111	104 110	eleqtrrd	$⊢ ((φ \land x \in (1 \dots N)) \land (q \in (ℙ ∖ (1 \dots K)) \land q ∥ x)) \to x \in W (q)$
112		fveq2	$⊢ k = q \to W (k) = W (q)$
113	112	eliuni	$⊢ (q \in (K + 1 \dots N) \land x \in W (q)) \to x \in ⋃_{k = K + 1}^{N} W (k)$
114	100 111 113	syl2anc	$⊢ ((φ \land x \in (1 \dots N)) \land (q \in (ℙ ∖ (1 \dots K)) \land q ∥ x)) \to x \in ⋃_{k = K + 1}^{N} W (k)$
115		elun2	$⊢ x \in ⋃_{k = K + 1}^{N} W (k) \to x \in (M \cup ⋃_{k = K + 1}^{N} W (k))$
116	114 115	syl	$⊢ ((φ \land x \in (1 \dots N)) \land (q \in (ℙ ∖ (1 \dots K)) \land q ∥ x)) \to x \in (M \cup ⋃_{k = K + 1}^{N} W (k))$
117	116	rexlimdvaa	$⊢ (φ \land x \in (1 \dots N)) \to (\exists q \in (ℙ ∖ (1 \dots K)) q ∥ x \to x \in (M \cup ⋃_{k = K + 1}^{N} W (k)))$
118	61 117	syl5bir	$⊢ (φ \land x \in (1 \dots N)) \to (\neg \forall q \in (ℙ ∖ (1 \dots K)) \neg q ∥ x \to x \in (M \cup ⋃_{k = K + 1}^{N} W (k)))$
119	60 118	pm2.61d	$⊢ (φ \land x \in (1 \dots N)) \to x \in (M \cup ⋃_{k = K + 1}^{N} W (k))$
120	48 119	eqelssd	$⊢ φ \to M \cup ⋃_{k = K + 1}^{N} W (k) = (1 \dots N)$
121	120	fveq2d	$⊢ φ \to \|M \cup ⋃_{k = K + 1}^{N} W (k)\| = \|(1 \dots N)\|$
122	3	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
123		hashfz1	$⊢ N \in ℕ_{0} \to \|(1 \dots N)\| = N$
124	122 123	syl	$⊢ φ \to \|(1 \dots N)\| = N$
125	121 124	eqtr2d	$⊢ φ \to N = \|M \cup ⋃_{k = K + 1}^{N} W (k)\|$
126	13	a1i	$⊢ φ \to M \in Fin$
127		ssfi	$⊢ ((1 \dots N) \in Fin \land ⋃_{k = K + 1}^{N} W (k) \subseteq (1 \dots N)) \to ⋃_{k = K + 1}^{N} W (k) \in Fin$
128	10 47 127	sylancr	$⊢ φ \to ⋃_{k = K + 1}^{N} W (k) \in Fin$
129		breq1	$⊢ p = k \to (p ∥ x \leftrightarrow k ∥ x)$
130	129	notbid	$⊢ p = k \to (\neg p ∥ x \leftrightarrow \neg k ∥ x)$
131		breq2	$⊢ n = x \to (p ∥ n \leftrightarrow p ∥ x)$
132	131	notbid	$⊢ n = x \to (\neg p ∥ n \leftrightarrow \neg p ∥ x)$
133	132	ralbidv	$⊢ n = x \to (\forall p \in (ℙ ∖ (1 \dots K)) \neg p ∥ n \leftrightarrow \forall p \in (ℙ ∖ (1 \dots K)) \neg p ∥ x)$
134	133 4	elrab2	$⊢ x \in M \leftrightarrow (x \in (1 \dots N) \land \forall p \in (ℙ ∖ (1 \dots K)) \neg p ∥ x)$
135	134	simprbi	$⊢ x \in M \to \forall p \in (ℙ ∖ (1 \dots K)) \neg p ∥ x$
136	135	ad2antlr	$⊢ ((φ \land x \in M) \land (k \in (K + 1 \dots N) \land k \in ℙ)) \to \forall p \in (ℙ ∖ (1 \dots K)) \neg p ∥ x$
137		simprr	$⊢ ((φ \land x \in M) \land (k \in (K + 1 \dots N) \land k \in ℙ)) \to k \in ℙ$
138		noel	$⊢ \neg k \in \emptyset$
139		simprl	$⊢ ((φ \land x \in M) \land (k \in (K + 1 \dots N) \land k \in ℙ)) \to k \in (K + 1 \dots N)$
140	139	biantrud	$⊢ ((φ \land x \in M) \land (k \in (K + 1 \dots N) \land k \in ℙ)) \to (k \in (1 \dots K) \leftrightarrow (k \in (1 \dots K) \land k \in (K + 1 \dots N)))$
141		elin	$⊢ k \in ((1 \dots K) \cap (K + 1 \dots N)) \leftrightarrow (k \in (1 \dots K) \land k \in (K + 1 \dots N))$
142	140 141	bitr4di	$⊢ ((φ \land x \in M) \land (k \in (K + 1 \dots N) \land k \in ℙ)) \to (k \in (1 \dots K) \leftrightarrow k \in ((1 \dots K) \cap (K + 1 \dots N)))$
143	81	ltp1d	$⊢ φ \to K < K + 1$
144		fzdisj	$⊢ K < K + 1 \to (1 \dots K) \cap (K + 1 \dots N) = \emptyset$
145	143 144	syl	$⊢ φ \to (1 \dots K) \cap (K + 1 \dots N) = \emptyset$
146	145	ad2antrr	$⊢ ((φ \land x \in M) \land (k \in (K + 1 \dots N) \land k \in ℙ)) \to (1 \dots K) \cap (K + 1 \dots N) = \emptyset$
147	146	eleq2d	$⊢ ((φ \land x \in M) \land (k \in (K + 1 \dots N) \land k \in ℙ)) \to (k \in ((1 \dots K) \cap (K + 1 \dots N)) \leftrightarrow k \in \emptyset)$
148	142 147	bitrd	$⊢ ((φ \land x \in M) \land (k \in (K + 1 \dots N) \land k \in ℙ)) \to (k \in (1 \dots K) \leftrightarrow k \in \emptyset)$
149	138 148	mtbiri	$⊢ ((φ \land x \in M) \land (k \in (K + 1 \dots N) \land k \in ℙ)) \to \neg k \in (1 \dots K)$
150	137 149	eldifd	$⊢ ((φ \land x \in M) \land (k \in (K + 1 \dots N) \land k \in ℙ)) \to k \in (ℙ ∖ (1 \dots K))$
151	130 136 150	rspcdva	$⊢ ((φ \land x \in M) \land (k \in (K + 1 \dots N) \land k \in ℙ)) \to \neg k ∥ x$
152	151	expr	$⊢ ((φ \land x \in M) \land k \in (K + 1 \dots N)) \to (k \in ℙ \to \neg k ∥ x)$
153		imnan	$⊢ (k \in ℙ \to \neg k ∥ x) \leftrightarrow \neg (k \in ℙ \land k ∥ x)$
154	152 153	sylib	$⊢ ((φ \land x \in M) \land k \in (K + 1 \dots N)) \to \neg (k \in ℙ \land k ∥ x)$
155	33	adantlr	$⊢ ((φ \land x \in M) \land k \in (K + 1 \dots N)) \to k \in ℕ$
156	155 40	syl	$⊢ ((φ \land x \in M) \land k \in (K + 1 \dots N)) \to W (k) = \{n \in (1 \dots N) \| (k \in ℙ \land k ∥ n)\}$
157	156	eleq2d	$⊢ ((φ \land x \in M) \land k \in (K + 1 \dots N)) \to (x \in W (k) \leftrightarrow x \in \{n \in (1 \dots N) \| (k \in ℙ \land k ∥ n)\})$
158		breq2	$⊢ n = x \to (k ∥ n \leftrightarrow k ∥ x)$
159	158	anbi2d	$⊢ n = x \to ((k \in ℙ \land k ∥ n) \leftrightarrow (k \in ℙ \land k ∥ x))$
160	159	elrab	$⊢ x \in \{n \in (1 \dots N) \| (k \in ℙ \land k ∥ n)\} \leftrightarrow (x \in (1 \dots N) \land (k \in ℙ \land k ∥ x))$
161	160	simprbi	$⊢ x \in \{n \in (1 \dots N) \| (k \in ℙ \land k ∥ n)\} \to (k \in ℙ \land k ∥ x)$
162	157 161	syl6bi	$⊢ ((φ \land x \in M) \land k \in (K + 1 \dots N)) \to (x \in W (k) \to (k \in ℙ \land k ∥ x))$
163	154 162	mtod	$⊢ ((φ \land x \in M) \land k \in (K + 1 \dots N)) \to \neg x \in W (k)$
164	163	nrexdv	$⊢ (φ \land x \in M) \to \neg \exists k \in (K + 1 \dots N) x \in W (k)$
165		eliun	$⊢ x \in ⋃_{k = K + 1}^{N} W (k) \leftrightarrow \exists k \in (K + 1 \dots N) x \in W (k)$
166	164 165	sylnibr	$⊢ (φ \land x \in M) \to \neg x \in ⋃_{k = K + 1}^{N} W (k)$
167	166	ex	$⊢ φ \to (x \in M \to \neg x \in ⋃_{k = K + 1}^{N} W (k))$
168		imnan	$⊢ (x \in M \to \neg x \in ⋃_{k = K + 1}^{N} W (k)) \leftrightarrow \neg (x \in M \land x \in ⋃_{k = K + 1}^{N} W (k))$
169	167 168	sylib	$⊢ φ \to \neg (x \in M \land x \in ⋃_{k = K + 1}^{N} W (k))$
170		elin	$⊢ x \in (M \cap ⋃_{k = K + 1}^{N} W (k)) \leftrightarrow (x \in M \land x \in ⋃_{k = K + 1}^{N} W (k))$
171	169 170	sylnibr	$⊢ φ \to \neg x \in (M \cap ⋃_{k = K + 1}^{N} W (k))$
172	171	eq0rdv	$⊢ φ \to M \cap ⋃_{k = K + 1}^{N} W (k) = \emptyset$
173		hashun	$⊢ (M \in Fin \land ⋃_{k = K + 1}^{N} W (k) \in Fin \land M \cap ⋃_{k = K + 1}^{N} W (k) = \emptyset) \to \|M \cup ⋃_{k = K + 1}^{N} W (k)\| = \|M\| + \|⋃_{k = K + 1}^{N} W (k)\|$
174	126 128 172 173	syl3anc	$⊢ φ \to \|M \cup ⋃_{k = K + 1}^{N} W (k)\| = \|M\| + \|⋃_{k = K + 1}^{N} W (k)\|$
175	28 125 174	3eqtrd	$⊢ φ \to (\frac{N}{2}) + (\frac{N}{2}) = \|M\| + \|⋃_{k = K + 1}^{N} W (k)\|$
176		hashcl	$⊢ ⋃_{k = K + 1}^{N} W (k) \in Fin \to \|⋃_{k = K + 1}^{N} W (k)\| \in ℕ_{0}$
177	128 176	syl	$⊢ φ \to \|⋃_{k = K + 1}^{N} W (k)\| \in ℕ_{0}$
178	177	nn0red	$⊢ φ \to \|⋃_{k = K + 1}^{N} W (k)\| \in ℝ$
179		fzfid	$⊢ φ \to (K + 1 \dots N) \in Fin$
180	30 32	sylan	$⊢ (φ \land k \in ℤ_{\geq (K + 1)}) \to k \in ℕ$
181		nnrecre	$⊢ k \in ℕ \to \frac{1}{k} \in ℝ$
182		0re	$⊢ 0 \in ℝ$
183		ifcl	$⊢ (\frac{1}{k} \in ℝ \land 0 \in ℝ) \to if (k \in ℙ, \frac{1}{k}, 0) \in ℝ$
184	181 182 183	sylancl	$⊢ k \in ℕ \to if (k \in ℙ, \frac{1}{k}, 0) \in ℝ$
185	180 184	syl	$⊢ (φ \land k \in ℤ_{\geq (K + 1)}) \to if (k \in ℙ, \frac{1}{k}, 0) \in ℝ$
186	31 185	sylan2	$⊢ (φ \land k \in (K + 1 \dots N)) \to if (k \in ℙ, \frac{1}{k}, 0) \in ℝ$
187	179 186	fsumrecl	$⊢ φ \to \sum_{k = K + 1}^{N} if (k \in ℙ, \frac{1}{k}, 0) \in ℝ$
188	8 187	remulcld	$⊢ φ \to N \sum_{k = K + 1}^{N} if (k \in ℙ, \frac{1}{k}, 0) \in ℝ$
189	1 2 3 4 5 6 7	prmreclem4	$⊢ φ \to (N \in ℤ_{\geq K} \to \|⋃_{k = K + 1}^{N} W (k)\| \leq N \sum_{k = K + 1}^{N} if (k \in ℙ, \frac{1}{k}, 0))$
190		eluz	$⊢ (N \in ℤ \land K \in ℤ) \to (K \in ℤ_{\geq N} \leftrightarrow N \leq K)$
191	65 62 190	syl2anc	$⊢ φ \to (K \in ℤ_{\geq N} \leftrightarrow N \leq K)$
192		nnleltp1	$⊢ (N \in ℕ \land K \in ℕ) \to (N \leq K \leftrightarrow N < K + 1)$
193	3 2 192	syl2anc	$⊢ φ \to (N \leq K \leftrightarrow N < K + 1)$
194		fzn	$⊢ (K + 1 \in ℤ \land N \in ℤ) \to (N < K + 1 \leftrightarrow (K + 1 \dots N) = \emptyset)$
195	63 65 194	syl2anc	$⊢ φ \to (N < K + 1 \leftrightarrow (K + 1 \dots N) = \emptyset)$
196	191 193 195	3bitrd	$⊢ φ \to (K \in ℤ_{\geq N} \leftrightarrow (K + 1 \dots N) = \emptyset)$
197		0le0	$⊢ 0 \leq 0$
198	27	mul01d	$⊢ φ \to N \cdot 0 = 0$
199	197 198	breqtrrid	$⊢ φ \to 0 \leq N \cdot 0$
200		iuneq1	$⊢ (K + 1 \dots N) = \emptyset \to ⋃_{k = K + 1}^{N} W (k) = ⋃_{k \in \emptyset} W (k)$
201		0iun	$⊢ ⋃_{k \in \emptyset} W (k) = \emptyset$
202	200 201	eqtrdi	$⊢ (K + 1 \dots N) = \emptyset \to ⋃_{k = K + 1}^{N} W (k) = \emptyset$
203	202	fveq2d	$⊢ (K + 1 \dots N) = \emptyset \to \|⋃_{k = K + 1}^{N} W (k)\| = \|\emptyset\|$
204		hash0	$⊢ \|\emptyset\| = 0$
205	203 204	eqtrdi	$⊢ (K + 1 \dots N) = \emptyset \to \|⋃_{k = K + 1}^{N} W (k)\| = 0$
206		sumeq1	$⊢ (K + 1 \dots N) = \emptyset \to \sum_{k = K + 1}^{N} if (k \in ℙ, \frac{1}{k}, 0) = \sum_{k \in \emptyset} if (k \in ℙ, \frac{1}{k}, 0)$
207		sum0	$⊢ \sum_{k \in \emptyset} if (k \in ℙ, \frac{1}{k}, 0) = 0$
208	206 207	eqtrdi	$⊢ (K + 1 \dots N) = \emptyset \to \sum_{k = K + 1}^{N} if (k \in ℙ, \frac{1}{k}, 0) = 0$
209	208	oveq2d	$⊢ (K + 1 \dots N) = \emptyset \to N \sum_{k = K + 1}^{N} if (k \in ℙ, \frac{1}{k}, 0) = N \cdot 0$
210	205 209	breq12d	$⊢ (K + 1 \dots N) = \emptyset \to (\|⋃_{k = K + 1}^{N} W (k)\| \leq N \sum_{k = K + 1}^{N} if (k \in ℙ, \frac{1}{k}, 0) \leftrightarrow 0 \leq N \cdot 0)$
211	199 210	syl5ibrcom	$⊢ φ \to ((K + 1 \dots N) = \emptyset \to \|⋃_{k = K + 1}^{N} W (k)\| \leq N \sum_{k = K + 1}^{N} if (k \in ℙ, \frac{1}{k}, 0))$
212	196 211	sylbid	$⊢ φ \to (K \in ℤ_{\geq N} \to \|⋃_{k = K + 1}^{N} W (k)\| \leq N \sum_{k = K + 1}^{N} if (k \in ℙ, \frac{1}{k}, 0))$
213		uztric	$⊢ (K \in ℤ \land N \in ℤ) \to (N \in ℤ_{\geq K} \lor K \in ℤ_{\geq N})$
214	62 65 213	syl2anc	$⊢ φ \to (N \in ℤ_{\geq K} \lor K \in ℤ_{\geq N})$
215	189 212 214	mpjaod	$⊢ φ \to \|⋃_{k = K + 1}^{N} W (k)\| \leq N \sum_{k = K + 1}^{N} if (k \in ℙ, \frac{1}{k}, 0)$
216		eqid	$⊢ ℤ_{\geq (K + 1)} = ℤ_{\geq (K + 1)}$
217		eleq1w	$⊢ n = k \to (n \in ℙ \leftrightarrow k \in ℙ)$
218		oveq2	$⊢ n = k \to \frac{1}{n} = \frac{1}{k}$
219	217 218	ifbieq1d	$⊢ n = k \to if (n \in ℙ, \frac{1}{n}, 0) = if (k \in ℙ, \frac{1}{k}, 0)$
220		ovex	$⊢ \frac{1}{k} \in V$
221		c0ex	$⊢ 0 \in V$
222	220 221	ifex	$⊢ if (k \in ℙ, \frac{1}{k}, 0) \in V$
223	219 1 222	fvmpt	$⊢ k \in ℕ \to F (k) = if (k \in ℙ, \frac{1}{k}, 0)$
224	180 223	syl	$⊢ (φ \land k \in ℤ_{\geq (K + 1)}) \to F (k) = if (k \in ℙ, \frac{1}{k}, 0)$
225	184	recnd	$⊢ k \in ℕ \to if (k \in ℙ, \frac{1}{k}, 0) \in ℂ$
226	223 225	eqeltrd	$⊢ k \in ℕ \to F (k) \in ℂ$
227	226	adantl	$⊢ (φ \land k \in ℕ) \to F (k) \in ℂ$
228	75 30 227	iserex	$⊢ φ \to (seq 1 (+ F) \in dom ⇝ \leftrightarrow seq (K + 1) (+ F) \in dom ⇝)$
229	5 228	mpbid	$⊢ φ \to seq (K + 1) (+ F) \in dom ⇝$
230	216 63 224 185 229	isumrecl	$⊢ φ \to \sum_{k \in ℤ_{\geq (K + 1)}} if (k \in ℙ, \frac{1}{k}, 0) \in ℝ$
231		halfre	$⊢ \frac{1}{2} \in ℝ$
232	231	a1i	$⊢ φ \to \frac{1}{2} \in ℝ$
233		fzssuz	$⊢ (K + 1 \dots N) \subseteq ℤ_{\geq (K + 1)}$
234	233	a1i	$⊢ φ \to (K + 1 \dots N) \subseteq ℤ_{\geq (K + 1)}$
235		nnrp	$⊢ k \in ℕ \to k \in ℝ^{+}$
236	235	rpreccld	$⊢ k \in ℕ \to \frac{1}{k} \in ℝ^{+}$
237	236	rpge0d	$⊢ k \in ℕ \to 0 \leq \frac{1}{k}$
238		breq2	$⊢ \frac{1}{k} = if (k \in ℙ, \frac{1}{k}, 0) \to (0 \leq \frac{1}{k} \leftrightarrow 0 \leq if (k \in ℙ, \frac{1}{k}, 0))$
239		breq2	$⊢ 0 = if (k \in ℙ, \frac{1}{k}, 0) \to (0 \leq 0 \leftrightarrow 0 \leq if (k \in ℙ, \frac{1}{k}, 0))$
240	238 239	ifboth	$⊢ (0 \leq \frac{1}{k} \land 0 \leq 0) \to 0 \leq if (k \in ℙ, \frac{1}{k}, 0)$
241	237 197 240	sylancl	$⊢ k \in ℕ \to 0 \leq if (k \in ℙ, \frac{1}{k}, 0)$
242	180 241	syl	$⊢ (φ \land k \in ℤ_{\geq (K + 1)}) \to 0 \leq if (k \in ℙ, \frac{1}{k}, 0)$
243	216 63 179 234 224 185 242 229	isumless	$⊢ φ \to \sum_{k = K + 1}^{N} if (k \in ℙ, \frac{1}{k}, 0) \leq \sum_{k \in ℤ_{\geq (K + 1)}} if (k \in ℙ, \frac{1}{k}, 0)$
244	187 230 232 243 6	lelttrd	$⊢ φ \to \sum_{k = K + 1}^{N} if (k \in ℙ, \frac{1}{k}, 0) < \frac{1}{2}$
245	3	nngt0d	$⊢ φ \to 0 < N$
246		ltmul2	$⊢ (\sum_{k = K + 1}^{N} if (k \in ℙ, \frac{1}{k}, 0) \in ℝ \land \frac{1}{2} \in ℝ \land (N \in ℝ \land 0 < N)) \to (\sum_{k = K + 1}^{N} if (k \in ℙ, \frac{1}{k}, 0) < \frac{1}{2} \leftrightarrow N \sum_{k = K + 1}^{N} if (k \in ℙ, \frac{1}{k}, 0) < N (\frac{1}{2}))$
247	187 232 8 245 246	syl112anc	$⊢ φ \to (\sum_{k = K + 1}^{N} if (k \in ℙ, \frac{1}{k}, 0) < \frac{1}{2} \leftrightarrow N \sum_{k = K + 1}^{N} if (k \in ℙ, \frac{1}{k}, 0) < N (\frac{1}{2}))$
248	244 247	mpbid	$⊢ φ \to N \sum_{k = K + 1}^{N} if (k \in ℙ, \frac{1}{k}, 0) < N (\frac{1}{2})$
249		2cn	$⊢ 2 \in ℂ$
250		2ne0	$⊢ 2 \neq 0$
251		divrec	$⊢ (N \in ℂ \land 2 \in ℂ \land 2 \neq 0) \to \frac{N}{2} = N (\frac{1}{2})$
252	249 250 251	mp3an23	$⊢ N \in ℂ \to \frac{N}{2} = N (\frac{1}{2})$
253	27 252	syl	$⊢ φ \to \frac{N}{2} = N (\frac{1}{2})$
254	248 253	breqtrrd	$⊢ φ \to N \sum_{k = K + 1}^{N} if (k \in ℙ, \frac{1}{k}, 0) < \frac{N}{2}$
255	178 188 9 215 254	lelttrd	$⊢ φ \to \|⋃_{k = K + 1}^{N} W (k)\| < \frac{N}{2}$
256	178 9 17 255	ltadd2dd	$⊢ φ \to \|M\| + \|⋃_{k = K + 1}^{N} W (k)\| < \|M\| + (\frac{N}{2})$
257	175 256	eqbrtrd	$⊢ φ \to (\frac{N}{2}) + (\frac{N}{2}) < \|M\| + (\frac{N}{2})$
258	9 17 9	ltadd1d	$⊢ φ \to (\frac{N}{2} < \|M\| \leftrightarrow (\frac{N}{2}) + (\frac{N}{2}) < \|M\| + (\frac{N}{2}))$
259	257 258	mpbird	$⊢ φ \to \frac{N}{2} < \|M\|$
260		oveq1	$⊢ k = r \to k^{2} = r^{2}$
261	260	breq1d	$⊢ k = r \to (k^{2} ∥ x \leftrightarrow r^{2} ∥ x)$
262	261	cbvrabv	$⊢ \{k \in ℕ \| k^{2} ∥ x\} = \{r \in ℕ \| r^{2} ∥ x\}$
263		breq2	$⊢ x = n \to (r^{2} ∥ x \leftrightarrow r^{2} ∥ n)$
264	263	rabbidv	$⊢ x = n \to \{r \in ℕ \| r^{2} ∥ x\} = \{r \in ℕ \| r^{2} ∥ n\}$
265	262 264	eqtrid	$⊢ x = n \to \{k \in ℕ \| k^{2} ∥ x\} = \{r \in ℕ \| r^{2} ∥ n\}$
266	265	supeq1d	$⊢ x = n \to sup (\{k \in ℕ \| k^{2} ∥ x\} ℝ <) = sup (\{r \in ℕ \| r^{2} ∥ n\} ℝ <)$
267	266	cbvmptv	$⊢ (x \in ℕ ⟼ sup (\{k \in ℕ \| k^{2} ∥ x\} ℝ <)) = (n \in ℕ ⟼ sup (\{r \in ℕ \| r^{2} ∥ n\} ℝ <))$
268	1 2 3 4 267	prmreclem3	$⊢ φ \to \|M\| \leq 2^{K} \sqrt{N}$
269	9 17 26 259 268	ltletrd	$⊢ φ \to \frac{N}{2} < 2^{K} \sqrt{N}$

Metamath Proof Explorer

Theorem prmreclem5

Proof