prmreclem4

Description: Lemma for prmrec . Show by induction that the indexed (nondisjoint) union Wk is at most the size of the prime reciprocal series. The key counting lemma is hashdvds , to show that the number of numbers in 1 ... N that divide k is at most N / k . (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	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))$

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		oveq2	$⊢ x = K \to (K + 1 \dots x) = (K + 1 \dots K)$
9	8	iuneq1d	$⊢ x = K \to ⋃_{k = K + 1}^{x} W (k) = ⋃_{k = K + 1}^{K} W (k)$
10	9	fveq2d	$⊢ x = K \to \|⋃_{k = K + 1}^{x} W (k)\| = \|⋃_{k = K + 1}^{K} W (k)\|$
11	8	sumeq1d	$⊢ x = K \to \sum_{k = K + 1}^{x} if (k \in ℙ, \frac{1}{k}, 0) = \sum_{k = K + 1}^{K} if (k \in ℙ, \frac{1}{k}, 0)$
12	11	oveq2d	$⊢ x = K \to N \sum_{k = K + 1}^{x} if (k \in ℙ, \frac{1}{k}, 0) = N \sum_{k = K + 1}^{K} if (k \in ℙ, \frac{1}{k}, 0)$
13	10 12	breq12d	$⊢ x = K \to (\|⋃_{k = K + 1}^{x} W (k)\| \leq N \sum_{k = K + 1}^{x} if (k \in ℙ, \frac{1}{k}, 0) \leftrightarrow \|⋃_{k = K + 1}^{K} W (k)\| \leq N \sum_{k = K + 1}^{K} if (k \in ℙ, \frac{1}{k}, 0))$
14	13	imbi2d	$⊢ x = K \to ((φ \to \|⋃_{k = K + 1}^{x} W (k)\| \leq N \sum_{k = K + 1}^{x} if (k \in ℙ, \frac{1}{k}, 0)) \leftrightarrow (φ \to \|⋃_{k = K + 1}^{K} W (k)\| \leq N \sum_{k = K + 1}^{K} if (k \in ℙ, \frac{1}{k}, 0)))$
15		oveq2	$⊢ x = j \to (K + 1 \dots x) = (K + 1 \dots j)$
16	15	iuneq1d	$⊢ x = j \to ⋃_{k = K + 1}^{x} W (k) = ⋃_{k = K + 1}^{j} W (k)$
17	16	fveq2d	$⊢ x = j \to \|⋃_{k = K + 1}^{x} W (k)\| = \|⋃_{k = K + 1}^{j} W (k)\|$
18	15	sumeq1d	$⊢ x = j \to \sum_{k = K + 1}^{x} if (k \in ℙ, \frac{1}{k}, 0) = \sum_{k = K + 1}^{j} if (k \in ℙ, \frac{1}{k}, 0)$
19	18	oveq2d	$⊢ x = j \to N \sum_{k = K + 1}^{x} if (k \in ℙ, \frac{1}{k}, 0) = N \sum_{k = K + 1}^{j} if (k \in ℙ, \frac{1}{k}, 0)$
20	17 19	breq12d	$⊢ x = j \to (\|⋃_{k = K + 1}^{x} W (k)\| \leq N \sum_{k = K + 1}^{x} if (k \in ℙ, \frac{1}{k}, 0) \leftrightarrow \|⋃_{k = K + 1}^{j} W (k)\| \leq N \sum_{k = K + 1}^{j} if (k \in ℙ, \frac{1}{k}, 0))$
21	20	imbi2d	$⊢ x = j \to ((φ \to \|⋃_{k = K + 1}^{x} W (k)\| \leq N \sum_{k = K + 1}^{x} if (k \in ℙ, \frac{1}{k}, 0)) \leftrightarrow (φ \to \|⋃_{k = K + 1}^{j} W (k)\| \leq N \sum_{k = K + 1}^{j} if (k \in ℙ, \frac{1}{k}, 0)))$
22		oveq2	$⊢ x = j + 1 \to (K + 1 \dots x) = (K + 1 \dots j + 1)$
23	22	iuneq1d	$⊢ x = j + 1 \to ⋃_{k = K + 1}^{x} W (k) = ⋃_{k = K + 1}^{j + 1} W (k)$
24	23	fveq2d	$⊢ x = j + 1 \to \|⋃_{k = K + 1}^{x} W (k)\| = \|⋃_{k = K + 1}^{j + 1} W (k)\|$
25	22	sumeq1d	$⊢ x = j + 1 \to \sum_{k = K + 1}^{x} if (k \in ℙ, \frac{1}{k}, 0) = \sum_{k = K + 1}^{j + 1} if (k \in ℙ, \frac{1}{k}, 0)$
26	25	oveq2d	$⊢ x = j + 1 \to N \sum_{k = K + 1}^{x} if (k \in ℙ, \frac{1}{k}, 0) = N \sum_{k = K + 1}^{j + 1} if (k \in ℙ, \frac{1}{k}, 0)$
27	24 26	breq12d	$⊢ x = j + 1 \to (\|⋃_{k = K + 1}^{x} W (k)\| \leq N \sum_{k = K + 1}^{x} if (k \in ℙ, \frac{1}{k}, 0) \leftrightarrow \|⋃_{k = K + 1}^{j + 1} W (k)\| \leq N \sum_{k = K + 1}^{j + 1} if (k \in ℙ, \frac{1}{k}, 0))$
28	27	imbi2d	$⊢ x = j + 1 \to ((φ \to \|⋃_{k = K + 1}^{x} W (k)\| \leq N \sum_{k = K + 1}^{x} if (k \in ℙ, \frac{1}{k}, 0)) \leftrightarrow (φ \to \|⋃_{k = K + 1}^{j + 1} W (k)\| \leq N \sum_{k = K + 1}^{j + 1} if (k \in ℙ, \frac{1}{k}, 0)))$
29		oveq2	$⊢ x = N \to (K + 1 \dots x) = (K + 1 \dots N)$
30	29	iuneq1d	$⊢ x = N \to ⋃_{k = K + 1}^{x} W (k) = ⋃_{k = K + 1}^{N} W (k)$
31	30	fveq2d	$⊢ x = N \to \|⋃_{k = K + 1}^{x} W (k)\| = \|⋃_{k = K + 1}^{N} W (k)\|$
32	29	sumeq1d	$⊢ x = N \to \sum_{k = K + 1}^{x} if (k \in ℙ, \frac{1}{k}, 0) = \sum_{k = K + 1}^{N} if (k \in ℙ, \frac{1}{k}, 0)$
33	32	oveq2d	$⊢ x = N \to N \sum_{k = K + 1}^{x} if (k \in ℙ, \frac{1}{k}, 0) = N \sum_{k = K + 1}^{N} if (k \in ℙ, \frac{1}{k}, 0)$
34	31 33	breq12d	$⊢ x = N \to (\|⋃_{k = K + 1}^{x} W (k)\| \leq N \sum_{k = K + 1}^{x} if (k \in ℙ, \frac{1}{k}, 0) \leftrightarrow \|⋃_{k = K + 1}^{N} W (k)\| \leq N \sum_{k = K + 1}^{N} if (k \in ℙ, \frac{1}{k}, 0))$
35	34	imbi2d	$⊢ x = N \to ((φ \to \|⋃_{k = K + 1}^{x} W (k)\| \leq N \sum_{k = K + 1}^{x} if (k \in ℙ, \frac{1}{k}, 0)) \leftrightarrow (φ \to \|⋃_{k = K + 1}^{N} W (k)\| \leq N \sum_{k = K + 1}^{N} if (k \in ℙ, \frac{1}{k}, 0)))$
36		0le0	$⊢ 0 \leq 0$
37	3	nncnd	$⊢ φ \to N \in ℂ$
38	37	mul01d	$⊢ φ \to N \cdot 0 = 0$
39	36 38	breqtrrid	$⊢ φ \to 0 \leq N \cdot 0$
40	2	nnred	$⊢ φ \to K \in ℝ$
41	40	ltp1d	$⊢ φ \to K < K + 1$
42	2	nnzd	$⊢ φ \to K \in ℤ$
43	42	peano2zd	$⊢ φ \to K + 1 \in ℤ$
44		fzn	$⊢ (K + 1 \in ℤ \land K \in ℤ) \to (K < K + 1 \leftrightarrow (K + 1 \dots K) = \emptyset)$
45	43 42 44	syl2anc	$⊢ φ \to (K < K + 1 \leftrightarrow (K + 1 \dots K) = \emptyset)$
46	41 45	mpbid	$⊢ φ \to (K + 1 \dots K) = \emptyset$
47	46	iuneq1d	$⊢ φ \to ⋃_{k = K + 1}^{K} W (k) = ⋃_{k \in \emptyset} W (k)$
48		0iun	$⊢ ⋃_{k \in \emptyset} W (k) = \emptyset$
49	47 48	syl6eq	$⊢ φ \to ⋃_{k = K + 1}^{K} W (k) = \emptyset$
50	49	fveq2d	$⊢ φ \to \|⋃_{k = K + 1}^{K} W (k)\| = \|\emptyset\|$
51		hash0	$⊢ \|\emptyset\| = 0$
52	50 51	syl6eq	$⊢ φ \to \|⋃_{k = K + 1}^{K} W (k)\| = 0$
53	46	sumeq1d	$⊢ φ \to \sum_{k = K + 1}^{K} if (k \in ℙ, \frac{1}{k}, 0) = \sum_{k \in \emptyset} if (k \in ℙ, \frac{1}{k}, 0)$
54		sum0	$⊢ \sum_{k \in \emptyset} if (k \in ℙ, \frac{1}{k}, 0) = 0$
55	53 54	syl6eq	$⊢ φ \to \sum_{k = K + 1}^{K} if (k \in ℙ, \frac{1}{k}, 0) = 0$
56	55	oveq2d	$⊢ φ \to N \sum_{k = K + 1}^{K} if (k \in ℙ, \frac{1}{k}, 0) = N \cdot 0$
57	39 52 56	3brtr4d	$⊢ φ \to \|⋃_{k = K + 1}^{K} W (k)\| \leq N \sum_{k = K + 1}^{K} if (k \in ℙ, \frac{1}{k}, 0)$
58		fzfi	$⊢ (1 \dots N) \in Fin$
59		elfzuz	$⊢ k \in (K + 1 \dots j) \to k \in ℤ_{\geq (K + 1)}$
60	2	peano2nnd	$⊢ φ \to K + 1 \in ℕ$
61		eluznn	$⊢ (K + 1 \in ℕ \land k \in ℤ_{\geq (K + 1)}) \to k \in ℕ$
62	60 61	sylan	$⊢ (φ \land k \in ℤ_{\geq (K + 1)}) \to k \in ℕ$
63		eleq1	$⊢ p = k \to (p \in ℙ \leftrightarrow k \in ℙ)$
64		breq1	$⊢ p = k \to (p ∥ n \leftrightarrow k ∥ n)$
65	63 64	anbi12d	$⊢ p = k \to ((p \in ℙ \land p ∥ n) \leftrightarrow (k \in ℙ \land k ∥ n))$
66	65	rabbidv	$⊢ p = k \to \{n \in (1 \dots N) \| (p \in ℙ \land p ∥ n)\} = \{n \in (1 \dots N) \| (k \in ℙ \land k ∥ n)\}$
67		ovex	$⊢ (1 \dots N) \in V$
68	67	rabex	$⊢ \{n \in (1 \dots N) \| (k \in ℙ \land k ∥ n)\} \in V$
69	66 7 68	fvmpt	$⊢ k \in ℕ \to W (k) = \{n \in (1 \dots N) \| (k \in ℙ \land k ∥ n)\}$
70	69	adantl	$⊢ (φ \land k \in ℕ) \to W (k) = \{n \in (1 \dots N) \| (k \in ℙ \land k ∥ n)\}$
71		ssrab2	$⊢ \{n \in (1 \dots N) \| (k \in ℙ \land k ∥ n)\} \subseteq (1 \dots N)$
72	70 71	eqsstrdi	$⊢ (φ \land k \in ℕ) \to W (k) \subseteq (1 \dots N)$
73	62 72	syldan	$⊢ (φ \land k \in ℤ_{\geq (K + 1)}) \to W (k) \subseteq (1 \dots N)$
74	59 73	sylan2	$⊢ (φ \land k \in (K + 1 \dots j)) \to W (k) \subseteq (1 \dots N)$
75	74	ralrimiva	$⊢ φ \to \forall k \in (K + 1 \dots j) W (k) \subseteq (1 \dots N)$
76	75	adantr	$⊢ (φ \land j \in ℤ_{\geq K}) \to \forall k \in (K + 1 \dots j) W (k) \subseteq (1 \dots N)$
77		iunss	$⊢ ⋃_{k = K + 1}^{j} W (k) \subseteq (1 \dots N) \leftrightarrow \forall k \in (K + 1 \dots j) W (k) \subseteq (1 \dots N)$
78	76 77	sylibr	$⊢ (φ \land j \in ℤ_{\geq K}) \to ⋃_{k = K + 1}^{j} W (k) \subseteq (1 \dots N)$
79		ssfi	$⊢ ((1 \dots N) \in Fin \land ⋃_{k = K + 1}^{j} W (k) \subseteq (1 \dots N)) \to ⋃_{k = K + 1}^{j} W (k) \in Fin$
80	58 78 79	sylancr	$⊢ (φ \land j \in ℤ_{\geq K}) \to ⋃_{k = K + 1}^{j} W (k) \in Fin$
81		hashcl	$⊢ ⋃_{k = K + 1}^{j} W (k) \in Fin \to \|⋃_{k = K + 1}^{j} W (k)\| \in ℕ_{0}$
82	80 81	syl	$⊢ (φ \land j \in ℤ_{\geq K}) \to \|⋃_{k = K + 1}^{j} W (k)\| \in ℕ_{0}$
83	82	nn0red	$⊢ (φ \land j \in ℤ_{\geq K}) \to \|⋃_{k = K + 1}^{j} W (k)\| \in ℝ$
84	3	nnred	$⊢ φ \to N \in ℝ$
85	84	adantr	$⊢ (φ \land j \in ℤ_{\geq K}) \to N \in ℝ$
86		fzfid	$⊢ (φ \land j \in ℤ_{\geq K}) \to (K + 1 \dots j) \in Fin$
87	60	adantr	$⊢ (φ \land j \in ℤ_{\geq K}) \to K + 1 \in ℕ$
88	87 59 61	syl2an	$⊢ ((φ \land j \in ℤ_{\geq K}) \land k \in (K + 1 \dots j)) \to k \in ℕ$
89		nnrecre	$⊢ k \in ℕ \to \frac{1}{k} \in ℝ$
90		0re	$⊢ 0 \in ℝ$
91		ifcl	$⊢ (\frac{1}{k} \in ℝ \land 0 \in ℝ) \to if (k \in ℙ, \frac{1}{k}, 0) \in ℝ$
92	89 90 91	sylancl	$⊢ k \in ℕ \to if (k \in ℙ, \frac{1}{k}, 0) \in ℝ$
93	88 92	syl	$⊢ ((φ \land j \in ℤ_{\geq K}) \land k \in (K + 1 \dots j)) \to if (k \in ℙ, \frac{1}{k}, 0) \in ℝ$
94	86 93	fsumrecl	$⊢ (φ \land j \in ℤ_{\geq K}) \to \sum_{k = K + 1}^{j} if (k \in ℙ, \frac{1}{k}, 0) \in ℝ$
95	85 94	remulcld	$⊢ (φ \land j \in ℤ_{\geq K}) \to N \sum_{k = K + 1}^{j} if (k \in ℙ, \frac{1}{k}, 0) \in ℝ$
96		prmnn	$⊢ j + 1 \in ℙ \to j + 1 \in ℕ$
97	96	nnrecred	$⊢ j + 1 \in ℙ \to \frac{1}{j + 1} \in ℝ$
98	97	adantl	$⊢ ((φ \land j \in ℤ_{\geq K}) \land j + 1 \in ℙ) \to \frac{1}{j + 1} \in ℝ$
99		0red	$⊢ ((φ \land j \in ℤ_{\geq K}) \land \neg j + 1 \in ℙ) \to 0 \in ℝ$
100	98 99	ifclda	$⊢ (φ \land j \in ℤ_{\geq K}) \to if (j + 1 \in ℙ, \frac{1}{j + 1}, 0) \in ℝ$
101	85 100	remulcld	$⊢ (φ \land j \in ℤ_{\geq K}) \to N if (j + 1 \in ℙ, \frac{1}{j + 1}, 0) \in ℝ$
102	83 95 101	leadd1d	$⊢ (φ \land j \in ℤ_{\geq K}) \to (\|⋃_{k = K + 1}^{j} W (k)\| \leq N \sum_{k = K + 1}^{j} if (k \in ℙ, \frac{1}{k}, 0) \leftrightarrow \|⋃_{k = K + 1}^{j} W (k)\| + N if (j + 1 \in ℙ, \frac{1}{j + 1}, 0) \leq N \sum_{k = K + 1}^{j} if (k \in ℙ, \frac{1}{k}, 0) + N if (j + 1 \in ℙ, \frac{1}{j + 1}, 0))$
103		eluzp1p1	$⊢ j \in ℤ_{\geq K} \to j + 1 \in ℤ_{\geq (K + 1)}$
104	103	adantl	$⊢ (φ \land j \in ℤ_{\geq K}) \to j + 1 \in ℤ_{\geq (K + 1)}$
105		simpl	$⊢ (φ \land j \in ℤ_{\geq K}) \to φ$
106		elfzuz	$⊢ k \in (K + 1 \dots j + 1) \to k \in ℤ_{\geq (K + 1)}$
107	92	recnd	$⊢ k \in ℕ \to if (k \in ℙ, \frac{1}{k}, 0) \in ℂ$
108	62 107	syl	$⊢ (φ \land k \in ℤ_{\geq (K + 1)}) \to if (k \in ℙ, \frac{1}{k}, 0) \in ℂ$
109	105 106 108	syl2an	$⊢ ((φ \land j \in ℤ_{\geq K}) \land k \in (K + 1 \dots j + 1)) \to if (k \in ℙ, \frac{1}{k}, 0) \in ℂ$
110		eleq1	$⊢ k = j + 1 \to (k \in ℙ \leftrightarrow j + 1 \in ℙ)$
111		oveq2	$⊢ k = j + 1 \to \frac{1}{k} = \frac{1}{j + 1}$
112	110 111	ifbieq1d	$⊢ k = j + 1 \to if (k \in ℙ, \frac{1}{k}, 0) = if (j + 1 \in ℙ, \frac{1}{j + 1}, 0)$
113	104 109 112	fsumm1	$⊢ (φ \land j \in ℤ_{\geq K}) \to \sum_{k = K + 1}^{j + 1} if (k \in ℙ, \frac{1}{k}, 0) = \sum_{k = K + 1}^{j + 1 - 1} if (k \in ℙ, \frac{1}{k}, 0) + if (j + 1 \in ℙ, \frac{1}{j + 1}, 0)$
114		eluzelz	$⊢ j \in ℤ_{\geq K} \to j \in ℤ$
115	114	adantl	$⊢ (φ \land j \in ℤ_{\geq K}) \to j \in ℤ$
116	115	zcnd	$⊢ (φ \land j \in ℤ_{\geq K}) \to j \in ℂ$
117		ax-1cn	$⊢ 1 \in ℂ$
118		pncan	$⊢ (j \in ℂ \land 1 \in ℂ) \to j + 1 - 1 = j$
119	116 117 118	sylancl	$⊢ (φ \land j \in ℤ_{\geq K}) \to j + 1 - 1 = j$
120	119	oveq2d	$⊢ (φ \land j \in ℤ_{\geq K}) \to (K + 1 \dots j + 1 - 1) = (K + 1 \dots j)$
121	120	sumeq1d	$⊢ (φ \land j \in ℤ_{\geq K}) \to \sum_{k = K + 1}^{j + 1 - 1} if (k \in ℙ, \frac{1}{k}, 0) = \sum_{k = K + 1}^{j} if (k \in ℙ, \frac{1}{k}, 0)$
122	121	oveq1d	$⊢ (φ \land j \in ℤ_{\geq K}) \to \sum_{k = K + 1}^{j + 1 - 1} if (k \in ℙ, \frac{1}{k}, 0) + if (j + 1 \in ℙ, \frac{1}{j + 1}, 0) = \sum_{k = K + 1}^{j} if (k \in ℙ, \frac{1}{k}, 0) + if (j + 1 \in ℙ, \frac{1}{j + 1}, 0)$
123	113 122	eqtrd	$⊢ (φ \land j \in ℤ_{\geq K}) \to \sum_{k = K + 1}^{j + 1} if (k \in ℙ, \frac{1}{k}, 0) = \sum_{k = K + 1}^{j} if (k \in ℙ, \frac{1}{k}, 0) + if (j + 1 \in ℙ, \frac{1}{j + 1}, 0)$
124	123	oveq2d	$⊢ (φ \land j \in ℤ_{\geq K}) \to N \sum_{k = K + 1}^{j + 1} if (k \in ℙ, \frac{1}{k}, 0) = N (\sum_{k = K + 1}^{j} if (k \in ℙ, \frac{1}{k}, 0) + if (j + 1 \in ℙ, \frac{1}{j + 1}, 0))$
125	37	adantr	$⊢ (φ \land j \in ℤ_{\geq K}) \to N \in ℂ$
126	94	recnd	$⊢ (φ \land j \in ℤ_{\geq K}) \to \sum_{k = K + 1}^{j} if (k \in ℙ, \frac{1}{k}, 0) \in ℂ$
127	100	recnd	$⊢ (φ \land j \in ℤ_{\geq K}) \to if (j + 1 \in ℙ, \frac{1}{j + 1}, 0) \in ℂ$
128	125 126 127	adddid	$⊢ (φ \land j \in ℤ_{\geq K}) \to N (\sum_{k = K + 1}^{j} if (k \in ℙ, \frac{1}{k}, 0) + if (j + 1 \in ℙ, \frac{1}{j + 1}, 0)) = N \sum_{k = K + 1}^{j} if (k \in ℙ, \frac{1}{k}, 0) + N if (j + 1 \in ℙ, \frac{1}{j + 1}, 0)$
129	124 128	eqtrd	$⊢ (φ \land j \in ℤ_{\geq K}) \to N \sum_{k = K + 1}^{j + 1} if (k \in ℙ, \frac{1}{k}, 0) = N \sum_{k = K + 1}^{j} if (k \in ℙ, \frac{1}{k}, 0) + N if (j + 1 \in ℙ, \frac{1}{j + 1}, 0)$
130	129	breq2d	$⊢ (φ \land j \in ℤ_{\geq K}) \to (\|⋃_{k = K + 1}^{j} W (k)\| + N if (j + 1 \in ℙ, \frac{1}{j + 1}, 0) \leq N \sum_{k = K + 1}^{j + 1} if (k \in ℙ, \frac{1}{k}, 0) \leftrightarrow \|⋃_{k = K + 1}^{j} W (k)\| + N if (j + 1 \in ℙ, \frac{1}{j + 1}, 0) \leq N \sum_{k = K + 1}^{j} if (k \in ℙ, \frac{1}{k}, 0) + N if (j + 1 \in ℙ, \frac{1}{j + 1}, 0))$
131	102 130	bitr4d	$⊢ (φ \land j \in ℤ_{\geq K}) \to (\|⋃_{k = K + 1}^{j} W (k)\| \leq N \sum_{k = K + 1}^{j} if (k \in ℙ, \frac{1}{k}, 0) \leftrightarrow \|⋃_{k = K + 1}^{j} W (k)\| + N if (j + 1 \in ℙ, \frac{1}{j + 1}, 0) \leq N \sum_{k = K + 1}^{j + 1} if (k \in ℙ, \frac{1}{k}, 0))$
132	106 73	sylan2	$⊢ (φ \land k \in (K + 1 \dots j + 1)) \to W (k) \subseteq (1 \dots N)$
133	132	ralrimiva	$⊢ φ \to \forall k \in (K + 1 \dots j + 1) W (k) \subseteq (1 \dots N)$
134	133	adantr	$⊢ (φ \land j \in ℤ_{\geq K}) \to \forall k \in (K + 1 \dots j + 1) W (k) \subseteq (1 \dots N)$
135		iunss	$⊢ ⋃_{k = K + 1}^{j + 1} W (k) \subseteq (1 \dots N) \leftrightarrow \forall k \in (K + 1 \dots j + 1) W (k) \subseteq (1 \dots N)$
136	134 135	sylibr	$⊢ (φ \land j \in ℤ_{\geq K}) \to ⋃_{k = K + 1}^{j + 1} W (k) \subseteq (1 \dots N)$
137		ssfi	$⊢ ((1 \dots N) \in Fin \land ⋃_{k = K + 1}^{j + 1} W (k) \subseteq (1 \dots N)) \to ⋃_{k = K + 1}^{j + 1} W (k) \in Fin$
138	58 136 137	sylancr	$⊢ (φ \land j \in ℤ_{\geq K}) \to ⋃_{k = K + 1}^{j + 1} W (k) \in Fin$
139		hashcl	$⊢ ⋃_{k = K + 1}^{j + 1} W (k) \in Fin \to \|⋃_{k = K + 1}^{j + 1} W (k)\| \in ℕ_{0}$
140	138 139	syl	$⊢ (φ \land j \in ℤ_{\geq K}) \to \|⋃_{k = K + 1}^{j + 1} W (k)\| \in ℕ_{0}$
141	140	nn0red	$⊢ (φ \land j \in ℤ_{\geq K}) \to \|⋃_{k = K + 1}^{j + 1} W (k)\| \in ℝ$
142		fveq2	$⊢ k = j + 1 \to W (k) = W (j + 1)$
143	142	sseq1d	$⊢ k = j + 1 \to (W (k) \subseteq (1 \dots N) \leftrightarrow W (j + 1) \subseteq (1 \dots N))$
144	72	ralrimiva	$⊢ φ \to \forall k \in ℕ W (k) \subseteq (1 \dots N)$
145	144	adantr	$⊢ (φ \land j \in ℤ_{\geq K}) \to \forall k \in ℕ W (k) \subseteq (1 \dots N)$
146		eluznn	$⊢ (K \in ℕ \land j \in ℤ_{\geq K}) \to j \in ℕ$
147	2 146	sylan	$⊢ (φ \land j \in ℤ_{\geq K}) \to j \in ℕ$
148	147	peano2nnd	$⊢ (φ \land j \in ℤ_{\geq K}) \to j + 1 \in ℕ$
149	143 145 148	rspcdva	$⊢ (φ \land j \in ℤ_{\geq K}) \to W (j + 1) \subseteq (1 \dots N)$
150		ssfi	$⊢ ((1 \dots N) \in Fin \land W (j + 1) \subseteq (1 \dots N)) \to W (j + 1) \in Fin$
151	58 149 150	sylancr	$⊢ (φ \land j \in ℤ_{\geq K}) \to W (j + 1) \in Fin$
152		hashcl	$⊢ W (j + 1) \in Fin \to \|W (j + 1)\| \in ℕ_{0}$
153	151 152	syl	$⊢ (φ \land j \in ℤ_{\geq K}) \to \|W (j + 1)\| \in ℕ_{0}$
154	153	nn0red	$⊢ (φ \land j \in ℤ_{\geq K}) \to \|W (j + 1)\| \in ℝ$
155	83 154	readdcld	$⊢ (φ \land j \in ℤ_{\geq K}) \to \|⋃_{k = K + 1}^{j} W (k)\| + \|W (j + 1)\| \in ℝ$
156	83 101	readdcld	$⊢ (φ \land j \in ℤ_{\geq K}) \to \|⋃_{k = K + 1}^{j} W (k)\| + N if (j + 1 \in ℙ, \frac{1}{j + 1}, 0) \in ℝ$
157	43	adantr	$⊢ (φ \land j \in ℤ_{\geq K}) \to K + 1 \in ℤ$
158		simpr	$⊢ (φ \land j \in ℤ_{\geq K}) \to j \in ℤ_{\geq K}$
159	2	nncnd	$⊢ φ \to K \in ℂ$
160	159	adantr	$⊢ (φ \land j \in ℤ_{\geq K}) \to K \in ℂ$
161		pncan	$⊢ (K \in ℂ \land 1 \in ℂ) \to K + 1 - 1 = K$
162	160 117 161	sylancl	$⊢ (φ \land j \in ℤ_{\geq K}) \to K + 1 - 1 = K$
163	162	fveq2d	$⊢ (φ \land j \in ℤ_{\geq K}) \to ℤ_{\geq (K + 1 - 1)} = ℤ_{\geq K}$
164	158 163	eleqtrrd	$⊢ (φ \land j \in ℤ_{\geq K}) \to j \in ℤ_{\geq (K + 1 - 1)}$
165		fzsuc2	$⊢ (K + 1 \in ℤ \land j \in ℤ_{\geq (K + 1 - 1)}) \to (K + 1 \dots j + 1) = (K + 1 \dots j) \cup \{j + 1\}$
166	157 164 165	syl2anc	$⊢ (φ \land j \in ℤ_{\geq K}) \to (K + 1 \dots j + 1) = (K + 1 \dots j) \cup \{j + 1\}$
167	166	iuneq1d	$⊢ (φ \land j \in ℤ_{\geq K}) \to ⋃_{k = K + 1}^{j + 1} W (k) = ⋃_{k \in (K + 1 \dots j) \cup \{j + 1\}} W (k)$
168		iunxun	$⊢ ⋃_{k \in (K + 1 \dots j) \cup \{j + 1\}} W (k) = ⋃_{k = K + 1}^{j} W (k) \cup ⋃_{k \in \{j + 1\}} W (k)$
169		ovex	$⊢ j + 1 \in V$
170	169 142	iunxsn	$⊢ ⋃_{k \in \{j + 1\}} W (k) = W (j + 1)$
171	170	uneq2i	$⊢ ⋃_{k = K + 1}^{j} W (k) \cup ⋃_{k \in \{j + 1\}} W (k) = ⋃_{k = K + 1}^{j} W (k) \cup W (j + 1)$
172	168 171	eqtri	$⊢ ⋃_{k \in (K + 1 \dots j) \cup \{j + 1\}} W (k) = ⋃_{k = K + 1}^{j} W (k) \cup W (j + 1)$
173	167 172	syl6eq	$⊢ (φ \land j \in ℤ_{\geq K}) \to ⋃_{k = K + 1}^{j + 1} W (k) = ⋃_{k = K + 1}^{j} W (k) \cup W (j + 1)$
174	173	fveq2d	$⊢ (φ \land j \in ℤ_{\geq K}) \to \|⋃_{k = K + 1}^{j + 1} W (k)\| = \|⋃_{k = K + 1}^{j} W (k) \cup W (j + 1)\|$
175		hashun2	$⊢ (⋃_{k = K + 1}^{j} W (k) \in Fin \land W (j + 1) \in Fin) \to \|⋃_{k = K + 1}^{j} W (k) \cup W (j + 1)\| \leq \|⋃_{k = K + 1}^{j} W (k)\| + \|W (j + 1)\|$
176	80 151 175	syl2anc	$⊢ (φ \land j \in ℤ_{\geq K}) \to \|⋃_{k = K + 1}^{j} W (k) \cup W (j + 1)\| \leq \|⋃_{k = K + 1}^{j} W (k)\| + \|W (j + 1)\|$
177	174 176	eqbrtrd	$⊢ (φ \land j \in ℤ_{\geq K}) \to \|⋃_{k = K + 1}^{j + 1} W (k)\| \leq \|⋃_{k = K + 1}^{j} W (k)\| + \|W (j + 1)\|$
178	85 148	nndivred	$⊢ (φ \land j \in ℤ_{\geq K}) \to \frac{N}{j + 1} \in ℝ$
179		flle	$⊢ \frac{N}{j + 1} \in ℝ \to ⌊\frac{N}{j + 1}⌋ \leq \frac{N}{j + 1}$
180	178 179	syl	$⊢ (φ \land j \in ℤ_{\geq K}) \to ⌊\frac{N}{j + 1}⌋ \leq \frac{N}{j + 1}$
181		elfznn	$⊢ n \in (1 \dots N) \to n \in ℕ$
182	181	nncnd	$⊢ n \in (1 \dots N) \to n \in ℂ$
183	182	subid1d	$⊢ n \in (1 \dots N) \to n - 0 = n$
184	183	breq2d	$⊢ n \in (1 \dots N) \to ((j + 1) ∥ (n - 0) \leftrightarrow (j + 1) ∥ n)$
185	184	rabbiia	$⊢ \{n \in (1 \dots N) \| (j + 1) ∥ (n - 0)\} = \{n \in (1 \dots N) \| (j + 1) ∥ n\}$
186	185	fveq2i	$⊢ \|\{n \in (1 \dots N) \| (j + 1) ∥ (n - 0)\}\| = \|\{n \in (1 \dots N) \| (j + 1) ∥ n\}\|$
187		1zzd	$⊢ (φ \land j \in ℤ_{\geq K}) \to 1 \in ℤ$
188	3	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
189		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
190		1m1e0	$⊢ 1 - 1 = 0$
191	190	fveq2i	$⊢ ℤ_{\geq (1 - 1)} = ℤ_{\geq 0}$
192	189 191	eqtr4i	$⊢ ℕ_{0} = ℤ_{\geq (1 - 1)}$
193	188 192	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq (1 - 1)}$
194	193	adantr	$⊢ (φ \land j \in ℤ_{\geq K}) \to N \in ℤ_{\geq (1 - 1)}$
195		0zd	$⊢ (φ \land j \in ℤ_{\geq K}) \to 0 \in ℤ$
196	148 187 194 195	hashdvds	$⊢ (φ \land j \in ℤ_{\geq K}) \to \|\{n \in (1 \dots N) \| (j + 1) ∥ (n - 0)\}\| = ⌊\frac{N - 0}{j + 1}⌋ - ⌊\frac{1 - 1 - 0}{j + 1}⌋$
197	125	subid1d	$⊢ (φ \land j \in ℤ_{\geq K}) \to N - 0 = N$
198	197	fvoveq1d	$⊢ (φ \land j \in ℤ_{\geq K}) \to ⌊\frac{N - 0}{j + 1}⌋ = ⌊\frac{N}{j + 1}⌋$
199	190	oveq1i	$⊢ 1 - 1 - 0 = 0 - 0$
200		0m0e0	$⊢ 0 - 0 = 0$
201	199 200	eqtri	$⊢ 1 - 1 - 0 = 0$
202	201	oveq1i	$⊢ \frac{1 - 1 - 0}{j + 1} = \frac{0}{j + 1}$
203	148	nncnd	$⊢ (φ \land j \in ℤ_{\geq K}) \to j + 1 \in ℂ$
204	148	nnne0d	$⊢ (φ \land j \in ℤ_{\geq K}) \to j + 1 \neq 0$
205	203 204	div0d	$⊢ (φ \land j \in ℤ_{\geq K}) \to \frac{0}{j + 1} = 0$
206	202 205	syl5eq	$⊢ (φ \land j \in ℤ_{\geq K}) \to \frac{1 - 1 - 0}{j + 1} = 0$
207	206	fveq2d	$⊢ (φ \land j \in ℤ_{\geq K}) \to ⌊\frac{1 - 1 - 0}{j + 1}⌋ = ⌊0⌋$
208		0z	$⊢ 0 \in ℤ$
209		flid	$⊢ 0 \in ℤ \to ⌊0⌋ = 0$
210	208 209	ax-mp	$⊢ ⌊0⌋ = 0$
211	207 210	syl6eq	$⊢ (φ \land j \in ℤ_{\geq K}) \to ⌊\frac{1 - 1 - 0}{j + 1}⌋ = 0$
212	198 211	oveq12d	$⊢ (φ \land j \in ℤ_{\geq K}) \to ⌊\frac{N - 0}{j + 1}⌋ - ⌊\frac{1 - 1 - 0}{j + 1}⌋ = ⌊\frac{N}{j + 1}⌋ - 0$
213	178	flcld	$⊢ (φ \land j \in ℤ_{\geq K}) \to ⌊\frac{N}{j + 1}⌋ \in ℤ$
214	213	zcnd	$⊢ (φ \land j \in ℤ_{\geq K}) \to ⌊\frac{N}{j + 1}⌋ \in ℂ$
215	214	subid1d	$⊢ (φ \land j \in ℤ_{\geq K}) \to ⌊\frac{N}{j + 1}⌋ - 0 = ⌊\frac{N}{j + 1}⌋$
216	196 212 215	3eqtrd	$⊢ (φ \land j \in ℤ_{\geq K}) \to \|\{n \in (1 \dots N) \| (j + 1) ∥ (n - 0)\}\| = ⌊\frac{N}{j + 1}⌋$
217	186 216	syl5eqr	$⊢ (φ \land j \in ℤ_{\geq K}) \to \|\{n \in (1 \dots N) \| (j + 1) ∥ n\}\| = ⌊\frac{N}{j + 1}⌋$
218	125 203 204	divrecd	$⊢ (φ \land j \in ℤ_{\geq K}) \to \frac{N}{j + 1} = N (\frac{1}{j + 1})$
219	218	eqcomd	$⊢ (φ \land j \in ℤ_{\geq K}) \to N (\frac{1}{j + 1}) = \frac{N}{j + 1}$
220	180 217 219	3brtr4d	$⊢ (φ \land j \in ℤ_{\geq K}) \to \|\{n \in (1 \dots N) \| (j + 1) ∥ n\}\| \leq N (\frac{1}{j + 1})$
221	220	adantr	$⊢ ((φ \land j \in ℤ_{\geq K}) \land j + 1 \in ℙ) \to \|\{n \in (1 \dots N) \| (j + 1) ∥ n\}\| \leq N (\frac{1}{j + 1})$
222		eleq1	$⊢ p = j + 1 \to (p \in ℙ \leftrightarrow j + 1 \in ℙ)$
223		breq1	$⊢ p = j + 1 \to (p ∥ n \leftrightarrow (j + 1) ∥ n)$
224	222 223	anbi12d	$⊢ p = j + 1 \to ((p \in ℙ \land p ∥ n) \leftrightarrow (j + 1 \in ℙ \land (j + 1) ∥ n))$
225	224	rabbidv	$⊢ p = j + 1 \to \{n \in (1 \dots N) \| (p \in ℙ \land p ∥ n)\} = \{n \in (1 \dots N) \| (j + 1 \in ℙ \land (j + 1) ∥ n)\}$
226	67	rabex	$⊢ \{n \in (1 \dots N) \| (j + 1 \in ℙ \land (j + 1) ∥ n)\} \in V$
227	225 7 226	fvmpt	$⊢ j + 1 \in ℕ \to W (j + 1) = \{n \in (1 \dots N) \| (j + 1 \in ℙ \land (j + 1) ∥ n)\}$
228	148 227	syl	$⊢ (φ \land j \in ℤ_{\geq K}) \to W (j + 1) = \{n \in (1 \dots N) \| (j + 1 \in ℙ \land (j + 1) ∥ n)\}$
229	228	adantr	$⊢ ((φ \land j \in ℤ_{\geq K}) \land j + 1 \in ℙ) \to W (j + 1) = \{n \in (1 \dots N) \| (j + 1 \in ℙ \land (j + 1) ∥ n)\}$
230		simpr	$⊢ ((φ \land j \in ℤ_{\geq K}) \land j + 1 \in ℙ) \to j + 1 \in ℙ$
231	230	biantrurd	$⊢ ((φ \land j \in ℤ_{\geq K}) \land j + 1 \in ℙ) \to ((j + 1) ∥ n \leftrightarrow (j + 1 \in ℙ \land (j + 1) ∥ n))$
232	231	rabbidv	$⊢ ((φ \land j \in ℤ_{\geq K}) \land j + 1 \in ℙ) \to \{n \in (1 \dots N) \| (j + 1) ∥ n\} = \{n \in (1 \dots N) \| (j + 1 \in ℙ \land (j + 1) ∥ n)\}$
233	229 232	eqtr4d	$⊢ ((φ \land j \in ℤ_{\geq K}) \land j + 1 \in ℙ) \to W (j + 1) = \{n \in (1 \dots N) \| (j + 1) ∥ n\}$
234	233	fveq2d	$⊢ ((φ \land j \in ℤ_{\geq K}) \land j + 1 \in ℙ) \to \|W (j + 1)\| = \|\{n \in (1 \dots N) \| (j + 1) ∥ n\}\|$
235		iftrue	$⊢ j + 1 \in ℙ \to if (j + 1 \in ℙ, \frac{1}{j + 1}, 0) = \frac{1}{j + 1}$
236	235	adantl	$⊢ ((φ \land j \in ℤ_{\geq K}) \land j + 1 \in ℙ) \to if (j + 1 \in ℙ, \frac{1}{j + 1}, 0) = \frac{1}{j + 1}$
237	236	oveq2d	$⊢ ((φ \land j \in ℤ_{\geq K}) \land j + 1 \in ℙ) \to N if (j + 1 \in ℙ, \frac{1}{j + 1}, 0) = N (\frac{1}{j + 1})$
238	221 234 237	3brtr4d	$⊢ ((φ \land j \in ℤ_{\geq K}) \land j + 1 \in ℙ) \to \|W (j + 1)\| \leq N if (j + 1 \in ℙ, \frac{1}{j + 1}, 0)$
239	36	a1i	$⊢ ((φ \land j \in ℤ_{\geq K}) \land \neg j + 1 \in ℙ) \to 0 \leq 0$
240		simpl	$⊢ (j + 1 \in ℙ \land (j + 1) ∥ n) \to j + 1 \in ℙ$
241	240	con3i	$⊢ \neg j + 1 \in ℙ \to \neg (j + 1 \in ℙ \land (j + 1) ∥ n)$
242	241	ralrimivw	$⊢ \neg j + 1 \in ℙ \to \forall n \in (1 \dots N) \neg (j + 1 \in ℙ \land (j + 1) ∥ n)$
243		rabeq0	$⊢ \{n \in (1 \dots N) \| (j + 1 \in ℙ \land (j + 1) ∥ n)\} = \emptyset \leftrightarrow \forall n \in (1 \dots N) \neg (j + 1 \in ℙ \land (j + 1) ∥ n)$
244	242 243	sylibr	$⊢ \neg j + 1 \in ℙ \to \{n \in (1 \dots N) \| (j + 1 \in ℙ \land (j + 1) ∥ n)\} = \emptyset$
245	228 244	sylan9eq	$⊢ ((φ \land j \in ℤ_{\geq K}) \land \neg j + 1 \in ℙ) \to W (j + 1) = \emptyset$
246	245	fveq2d	$⊢ ((φ \land j \in ℤ_{\geq K}) \land \neg j + 1 \in ℙ) \to \|W (j + 1)\| = \|\emptyset\|$
247	246 51	syl6eq	$⊢ ((φ \land j \in ℤ_{\geq K}) \land \neg j + 1 \in ℙ) \to \|W (j + 1)\| = 0$
248		iffalse	$⊢ \neg j + 1 \in ℙ \to if (j + 1 \in ℙ, \frac{1}{j + 1}, 0) = 0$
249	248	oveq2d	$⊢ \neg j + 1 \in ℙ \to N if (j + 1 \in ℙ, \frac{1}{j + 1}, 0) = N \cdot 0$
250	38	adantr	$⊢ (φ \land j \in ℤ_{\geq K}) \to N \cdot 0 = 0$
251	249 250	sylan9eqr	$⊢ ((φ \land j \in ℤ_{\geq K}) \land \neg j + 1 \in ℙ) \to N if (j + 1 \in ℙ, \frac{1}{j + 1}, 0) = 0$
252	239 247 251	3brtr4d	$⊢ ((φ \land j \in ℤ_{\geq K}) \land \neg j + 1 \in ℙ) \to \|W (j + 1)\| \leq N if (j + 1 \in ℙ, \frac{1}{j + 1}, 0)$
253	238 252	pm2.61dan	$⊢ (φ \land j \in ℤ_{\geq K}) \to \|W (j + 1)\| \leq N if (j + 1 \in ℙ, \frac{1}{j + 1}, 0)$
254	154 101 83 253	leadd2dd	$⊢ (φ \land j \in ℤ_{\geq K}) \to \|⋃_{k = K + 1}^{j} W (k)\| + \|W (j + 1)\| \leq \|⋃_{k = K + 1}^{j} W (k)\| + N if (j + 1 \in ℙ, \frac{1}{j + 1}, 0)$
255	141 155 156 177 254	letrd	$⊢ (φ \land j \in ℤ_{\geq K}) \to \|⋃_{k = K + 1}^{j + 1} W (k)\| \leq \|⋃_{k = K + 1}^{j} W (k)\| + N if (j + 1 \in ℙ, \frac{1}{j + 1}, 0)$
256		fzfid	$⊢ (φ \land j \in ℤ_{\geq K}) \to (K + 1 \dots j + 1) \in Fin$
257	62 92	syl	$⊢ (φ \land k \in ℤ_{\geq (K + 1)}) \to if (k \in ℙ, \frac{1}{k}, 0) \in ℝ$
258	105 106 257	syl2an	$⊢ ((φ \land j \in ℤ_{\geq K}) \land k \in (K + 1 \dots j + 1)) \to if (k \in ℙ, \frac{1}{k}, 0) \in ℝ$
259	256 258	fsumrecl	$⊢ (φ \land j \in ℤ_{\geq K}) \to \sum_{k = K + 1}^{j + 1} if (k \in ℙ, \frac{1}{k}, 0) \in ℝ$
260	85 259	remulcld	$⊢ (φ \land j \in ℤ_{\geq K}) \to N \sum_{k = K + 1}^{j + 1} if (k \in ℙ, \frac{1}{k}, 0) \in ℝ$
261		letr	$⊢ (\|⋃_{k = K + 1}^{j + 1} W (k)\| \in ℝ \land \|⋃_{k = K + 1}^{j} W (k)\| + N if (j + 1 \in ℙ, \frac{1}{j + 1}, 0) \in ℝ \land N \sum_{k = K + 1}^{j + 1} if (k \in ℙ, \frac{1}{k}, 0) \in ℝ) \to ((\|⋃_{k = K + 1}^{j + 1} W (k)\| \leq \|⋃_{k = K + 1}^{j} W (k)\| + N if (j + 1 \in ℙ, \frac{1}{j + 1}, 0) \land \|⋃_{k = K + 1}^{j} W (k)\| + N if (j + 1 \in ℙ, \frac{1}{j + 1}, 0) \leq N \sum_{k = K + 1}^{j + 1} if (k \in ℙ, \frac{1}{k}, 0)) \to \|⋃_{k = K + 1}^{j + 1} W (k)\| \leq N \sum_{k = K + 1}^{j + 1} if (k \in ℙ, \frac{1}{k}, 0))$
262	141 156 260 261	syl3anc	$⊢ (φ \land j \in ℤ_{\geq K}) \to ((\|⋃_{k = K + 1}^{j + 1} W (k)\| \leq \|⋃_{k = K + 1}^{j} W (k)\| + N if (j + 1 \in ℙ, \frac{1}{j + 1}, 0) \land \|⋃_{k = K + 1}^{j} W (k)\| + N if (j + 1 \in ℙ, \frac{1}{j + 1}, 0) \leq N \sum_{k = K + 1}^{j + 1} if (k \in ℙ, \frac{1}{k}, 0)) \to \|⋃_{k = K + 1}^{j + 1} W (k)\| \leq N \sum_{k = K + 1}^{j + 1} if (k \in ℙ, \frac{1}{k}, 0))$
263	255 262	mpand	$⊢ (φ \land j \in ℤ_{\geq K}) \to (\|⋃_{k = K + 1}^{j} W (k)\| + N if (j + 1 \in ℙ, \frac{1}{j + 1}, 0) \leq N \sum_{k = K + 1}^{j + 1} if (k \in ℙ, \frac{1}{k}, 0) \to \|⋃_{k = K + 1}^{j + 1} W (k)\| \leq N \sum_{k = K + 1}^{j + 1} if (k \in ℙ, \frac{1}{k}, 0))$
264	131 263	sylbid	$⊢ (φ \land j \in ℤ_{\geq K}) \to (\|⋃_{k = K + 1}^{j} W (k)\| \leq N \sum_{k = K + 1}^{j} if (k \in ℙ, \frac{1}{k}, 0) \to \|⋃_{k = K + 1}^{j + 1} W (k)\| \leq N \sum_{k = K + 1}^{j + 1} if (k \in ℙ, \frac{1}{k}, 0))$
265	264	expcom	$⊢ j \in ℤ_{\geq K} \to (φ \to (\|⋃_{k = K + 1}^{j} W (k)\| \leq N \sum_{k = K + 1}^{j} if (k \in ℙ, \frac{1}{k}, 0) \to \|⋃_{k = K + 1}^{j + 1} W (k)\| \leq N \sum_{k = K + 1}^{j + 1} if (k \in ℙ, \frac{1}{k}, 0)))$
266	265	a2d	$⊢ j \in ℤ_{\geq K} \to ((φ \to \|⋃_{k = K + 1}^{j} W (k)\| \leq N \sum_{k = K + 1}^{j} if (k \in ℙ, \frac{1}{k}, 0)) \to (φ \to \|⋃_{k = K + 1}^{j + 1} W (k)\| \leq N \sum_{k = K + 1}^{j + 1} if (k \in ℙ, \frac{1}{k}, 0)))$
267	14 21 28 35 57 266	uzind4i	$⊢ N \in ℤ_{\geq K} \to (φ \to \|⋃_{k = K + 1}^{N} W (k)\| \leq N \sum_{k = K + 1}^{N} if (k \in ℙ, \frac{1}{k}, 0))$
268	267	com12	$⊢ φ \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))$

Metamath Proof Explorer

Theorem prmreclem4

Proof