prmreclem6

Description: Lemma for prmrec . If the series F was convergent, there would be some k such that the sum starting from k + 1 sums to less than 1 / 2 ; this is a sufficient hypothesis for prmreclem5 to produce the contradictory bound N / 2 < ( 2 ^ k ) sqrt N , which is false for N = 2 ^ ( 2 k + 2 ) . (Contributed by Mario Carneiro, 6-Aug-2014)

		Ref	Expression
	Hypothesis	prmrec.1	$⊢ F = (n \in ℕ ⟼ if (n \in ℙ, \frac{1}{n}, 0))$
	Assertion	prmreclem6	$⊢ \neg seq 1 (+ F) \in dom ⇝$

Proof

Step	Hyp	Ref	Expression
1		prmrec.1	$⊢ F = (n \in ℕ ⟼ if (n \in ℙ, \frac{1}{n}, 0))$
2		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
3		1zzd	$⊢ ⊤ \to 1 \in ℤ$
4		nnrecre	$⊢ n \in ℕ \to \frac{1}{n} \in ℝ$
5	4	adantl	$⊢ (⊤ \land n \in ℕ) \to \frac{1}{n} \in ℝ$
6		0re	$⊢ 0 \in ℝ$
7		ifcl	$⊢ (\frac{1}{n} \in ℝ \land 0 \in ℝ) \to if (n \in ℙ, \frac{1}{n}, 0) \in ℝ$
8	5 6 7	sylancl	$⊢ (⊤ \land n \in ℕ) \to if (n \in ℙ, \frac{1}{n}, 0) \in ℝ$
9	8 1	fmptd	$⊢ ⊤ \to F : ℕ ⟶ ℝ$
10	9	ffvelcdmda	$⊢ (⊤ \land j \in ℕ) \to F (j) \in ℝ$
11	2 3 10	serfre	$⊢ ⊤ \to seq 1 (+ F) : ℕ ⟶ ℝ$
12	11	mptru	$⊢ seq 1 (+ F) : ℕ ⟶ ℝ$
13		frn	$⊢ seq 1 (+ F) : ℕ ⟶ ℝ \to ran seq 1 (+ F) \subseteq ℝ$
14	12 13	mp1i	$⊢ seq 1 (+ F) \in dom ⇝ \to ran seq 1 (+ F) \subseteq ℝ$
15		1nn	$⊢ 1 \in ℕ$
16	12	fdmi	$⊢ dom seq 1 (+ F) = ℕ$
17	15 16	eleqtrri	$⊢ 1 \in dom seq 1 (+ F)$
18		ne0i	$⊢ 1 \in dom seq 1 (+ F) \to dom seq 1 (+ F) \neq \emptyset$
19		dm0rn0	$⊢ dom seq 1 (+ F) = \emptyset \leftrightarrow ran seq 1 (+ F) = \emptyset$
20	19	necon3bii	$⊢ dom seq 1 (+ F) \neq \emptyset \leftrightarrow ran seq 1 (+ F) \neq \emptyset$
21	18 20	sylib	$⊢ 1 \in dom seq 1 (+ F) \to ran seq 1 (+ F) \neq \emptyset$
22	17 21	mp1i	$⊢ seq 1 (+ F) \in dom ⇝ \to ran seq 1 (+ F) \neq \emptyset$
23		1zzd	$⊢ seq 1 (+ F) \in dom ⇝ \to 1 \in ℤ$
24		climdm	$⊢ seq 1 (+ F) \in dom ⇝ \leftrightarrow seq 1 (+ F) ⇝ ⇝ (seq 1 (+ F))$
25	24	biimpi	$⊢ seq 1 (+ F) \in dom ⇝ \to seq 1 (+ F) ⇝ ⇝ (seq 1 (+ F))$
26	12	a1i	$⊢ seq 1 (+ F) \in dom ⇝ \to seq 1 (+ F) : ℕ ⟶ ℝ$
27	26	ffvelcdmda	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to seq 1 (+ F) (k) \in ℝ$
28	2 23 25 27	climrecl	$⊢ seq 1 (+ F) \in dom ⇝ \to ⇝ (seq 1 (+ F)) \in ℝ$
29		simpr	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to k \in ℕ$
30	25	adantr	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to seq 1 (+ F) ⇝ ⇝ (seq 1 (+ F))$
31		eleq1w	$⊢ n = j \to (n \in ℙ \leftrightarrow j \in ℙ)$
32		oveq2	$⊢ n = j \to \frac{1}{n} = \frac{1}{j}$
33	31 32	ifbieq1d	$⊢ n = j \to if (n \in ℙ, \frac{1}{n}, 0) = if (j \in ℙ, \frac{1}{j}, 0)$
34		prmnn	$⊢ j \in ℙ \to j \in ℕ$
35	34	adantl	$⊢ (⊤ \land j \in ℙ) \to j \in ℕ$
36	35	nnrecred	$⊢ (⊤ \land j \in ℙ) \to \frac{1}{j} \in ℝ$
37	6	a1i	$⊢ (⊤ \land \neg j \in ℙ) \to 0 \in ℝ$
38	36 37	ifclda	$⊢ ⊤ \to if (j \in ℙ, \frac{1}{j}, 0) \in ℝ$
39	38	mptru	$⊢ if (j \in ℙ, \frac{1}{j}, 0) \in ℝ$
40	39	elexi	$⊢ if (j \in ℙ, \frac{1}{j}, 0) \in V$
41	33 1 40	fvmpt	$⊢ j \in ℕ \to F (j) = if (j \in ℙ, \frac{1}{j}, 0)$
42	41	adantl	$⊢ (seq 1 (+ F) \in dom ⇝ \land j \in ℕ) \to F (j) = if (j \in ℙ, \frac{1}{j}, 0)$
43	39	a1i	$⊢ (seq 1 (+ F) \in dom ⇝ \land j \in ℕ) \to if (j \in ℙ, \frac{1}{j}, 0) \in ℝ$
44	42 43	eqeltrd	$⊢ (seq 1 (+ F) \in dom ⇝ \land j \in ℕ) \to F (j) \in ℝ$
45	44	adantlr	$⊢ ((seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \land j \in ℕ) \to F (j) \in ℝ$
46		nnrp	$⊢ j \in ℕ \to j \in ℝ^{+}$
47	46	adantl	$⊢ (seq 1 (+ F) \in dom ⇝ \land j \in ℕ) \to j \in ℝ^{+}$
48	47	rpreccld	$⊢ (seq 1 (+ F) \in dom ⇝ \land j \in ℕ) \to \frac{1}{j} \in ℝ^{+}$
49	48	rpge0d	$⊢ (seq 1 (+ F) \in dom ⇝ \land j \in ℕ) \to 0 \leq \frac{1}{j}$
50		0le0	$⊢ 0 \leq 0$
51		breq2	$⊢ \frac{1}{j} = if (j \in ℙ, \frac{1}{j}, 0) \to (0 \leq \frac{1}{j} \leftrightarrow 0 \leq if (j \in ℙ, \frac{1}{j}, 0))$
52		breq2	$⊢ 0 = if (j \in ℙ, \frac{1}{j}, 0) \to (0 \leq 0 \leftrightarrow 0 \leq if (j \in ℙ, \frac{1}{j}, 0))$
53	51 52	ifboth	$⊢ (0 \leq \frac{1}{j} \land 0 \leq 0) \to 0 \leq if (j \in ℙ, \frac{1}{j}, 0)$
54	49 50 53	sylancl	$⊢ (seq 1 (+ F) \in dom ⇝ \land j \in ℕ) \to 0 \leq if (j \in ℙ, \frac{1}{j}, 0)$
55	54 42	breqtrrd	$⊢ (seq 1 (+ F) \in dom ⇝ \land j \in ℕ) \to 0 \leq F (j)$
56	55	adantlr	$⊢ ((seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \land j \in ℕ) \to 0 \leq F (j)$
57	2 29 30 45 56	climserle	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to seq 1 (+ F) (k) \leq ⇝ (seq 1 (+ F))$
58	57	ralrimiva	$⊢ seq 1 (+ F) \in dom ⇝ \to \forall k \in ℕ seq 1 (+ F) (k) \leq ⇝ (seq 1 (+ F))$
59		brralrspcev	$⊢ (⇝ (seq 1 (+ F)) \in ℝ \land \forall k \in ℕ seq 1 (+ F) (k) \leq ⇝ (seq 1 (+ F))) \to \exists x \in ℝ \forall k \in ℕ seq 1 (+ F) (k) \leq x$
60	28 58 59	syl2anc	$⊢ seq 1 (+ F) \in dom ⇝ \to \exists x \in ℝ \forall k \in ℕ seq 1 (+ F) (k) \leq x$
61		ffn	$⊢ seq 1 (+ F) : ℕ ⟶ ℝ \to seq 1 (+ F) Fn ℕ$
62		breq1	$⊢ z = seq 1 (+ F) (k) \to (z \leq x \leftrightarrow seq 1 (+ F) (k) \leq x)$
63	62	ralrn	$⊢ seq 1 (+ F) Fn ℕ \to (\forall z \in ran seq 1 (+ F) z \leq x \leftrightarrow \forall k \in ℕ seq 1 (+ F) (k) \leq x)$
64	12 61 63	mp2b	$⊢ \forall z \in ran seq 1 (+ F) z \leq x \leftrightarrow \forall k \in ℕ seq 1 (+ F) (k) \leq x$
65	64	rexbii	$⊢ \exists x \in ℝ \forall z \in ran seq 1 (+ F) z \leq x \leftrightarrow \exists x \in ℝ \forall k \in ℕ seq 1 (+ F) (k) \leq x$
66	60 65	sylibr	$⊢ seq 1 (+ F) \in dom ⇝ \to \exists x \in ℝ \forall z \in ran seq 1 (+ F) z \leq x$
67	14 22 66	suprcld	$⊢ seq 1 (+ F) \in dom ⇝ \to sup (ran seq 1 (+ F) ℝ <) \in ℝ$
68		2rp	$⊢ 2 \in ℝ^{+}$
69		rpreccl	$⊢ 2 \in ℝ^{+} \to \frac{1}{2} \in ℝ^{+}$
70	68 69	ax-mp	$⊢ \frac{1}{2} \in ℝ^{+}$
71		ltsubrp	$⊢ (sup (ran seq 1 (+ F) ℝ <) \in ℝ \land \frac{1}{2} \in ℝ^{+}) \to sup (ran seq 1 (+ F) ℝ <) - (\frac{1}{2}) < sup (ran seq 1 (+ F) ℝ <)$
72	67 70 71	sylancl	$⊢ seq 1 (+ F) \in dom ⇝ \to sup (ran seq 1 (+ F) ℝ <) - (\frac{1}{2}) < sup (ran seq 1 (+ F) ℝ <)$
73		halfre	$⊢ \frac{1}{2} \in ℝ$
74		resubcl	$⊢ (sup (ran seq 1 (+ F) ℝ <) \in ℝ \land \frac{1}{2} \in ℝ) \to sup (ran seq 1 (+ F) ℝ <) - (\frac{1}{2}) \in ℝ$
75	67 73 74	sylancl	$⊢ seq 1 (+ F) \in dom ⇝ \to sup (ran seq 1 (+ F) ℝ <) - (\frac{1}{2}) \in ℝ$
76		suprlub	$⊢ ((ran seq 1 (+ F) \subseteq ℝ \land ran seq 1 (+ F) \neq \emptyset \land \exists x \in ℝ \forall z \in ran seq 1 (+ F) z \leq x) \land sup (ran seq 1 (+ F) ℝ <) - (\frac{1}{2}) \in ℝ) \to (sup (ran seq 1 (+ F) ℝ <) - (\frac{1}{2}) < sup (ran seq 1 (+ F) ℝ <) \leftrightarrow \exists y \in ran seq 1 (+ F) sup (ran seq 1 (+ F) ℝ <) - (\frac{1}{2}) < y)$
77	14 22 66 75 76	syl31anc	$⊢ seq 1 (+ F) \in dom ⇝ \to (sup (ran seq 1 (+ F) ℝ <) - (\frac{1}{2}) < sup (ran seq 1 (+ F) ℝ <) \leftrightarrow \exists y \in ran seq 1 (+ F) sup (ran seq 1 (+ F) ℝ <) - (\frac{1}{2}) < y)$
78	72 77	mpbid	$⊢ seq 1 (+ F) \in dom ⇝ \to \exists y \in ran seq 1 (+ F) sup (ran seq 1 (+ F) ℝ <) - (\frac{1}{2}) < y$
79		breq2	$⊢ y = seq 1 (+ F) (k) \to (sup (ran seq 1 (+ F) ℝ <) - (\frac{1}{2}) < y \leftrightarrow sup (ran seq 1 (+ F) ℝ <) - (\frac{1}{2}) < seq 1 (+ F) (k))$
80	79	rexrn	$⊢ seq 1 (+ F) Fn ℕ \to (\exists y \in ran seq 1 (+ F) sup (ran seq 1 (+ F) ℝ <) - (\frac{1}{2}) < y \leftrightarrow \exists k \in ℕ sup (ran seq 1 (+ F) ℝ <) - (\frac{1}{2}) < seq 1 (+ F) (k))$
81	12 61 80	mp2b	$⊢ \exists y \in ran seq 1 (+ F) sup (ran seq 1 (+ F) ℝ <) - (\frac{1}{2}) < y \leftrightarrow \exists k \in ℕ sup (ran seq 1 (+ F) ℝ <) - (\frac{1}{2}) < seq 1 (+ F) (k)$
82	78 81	sylib	$⊢ seq 1 (+ F) \in dom ⇝ \to \exists k \in ℕ sup (ran seq 1 (+ F) ℝ <) - (\frac{1}{2}) < seq 1 (+ F) (k)$
83		2re	$⊢ 2 \in ℝ$
84		2nn	$⊢ 2 \in ℕ$
85		nnmulcl	$⊢ (2 \in ℕ \land k \in ℕ) \to 2 k \in ℕ$
86	84 29 85	sylancr	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to 2 k \in ℕ$
87	86	peano2nnd	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to 2 k + 1 \in ℕ$
88	87	nnnn0d	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to 2 k + 1 \in ℕ_{0}$
89		reexpcl	$⊢ (2 \in ℝ \land 2 k + 1 \in ℕ_{0}) \to 2^{2 k + 1} \in ℝ$
90	83 88 89	sylancr	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to 2^{2 k + 1} \in ℝ$
91	90	ltnrd	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to \neg 2^{2 k + 1} < 2^{2 k + 1}$
92	29	adantr	$⊢ ((seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \land \sum_{j \in ℤ_{\geq (k + 1)}} if (j \in ℙ, \frac{1}{j}, 0) < \frac{1}{2}) \to k \in ℕ$
93		peano2nn	$⊢ k \in ℕ \to k + 1 \in ℕ$
94	93	adantl	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to k + 1 \in ℕ$
95	94	nnnn0d	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to k + 1 \in ℕ_{0}$
96		nnexpcl	$⊢ (2 \in ℕ \land k + 1 \in ℕ_{0}) \to 2^{k + 1} \in ℕ$
97	84 95 96	sylancr	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to 2^{k + 1} \in ℕ$
98	97	nnsqcld	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to {(2^{k + 1})}^{2} \in ℕ$
99	98	adantr	$⊢ ((seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \land \sum_{j \in ℤ_{\geq (k + 1)}} if (j \in ℙ, \frac{1}{j}, 0) < \frac{1}{2}) \to {(2^{k + 1})}^{2} \in ℕ$
100		breq1	$⊢ p = w \to (p ∥ r \leftrightarrow w ∥ r)$
101	100	notbid	$⊢ p = w \to (\neg p ∥ r \leftrightarrow \neg w ∥ r)$
102	101	cbvralvw	$⊢ \forall p \in (ℙ ∖ (1 \dots k)) \neg p ∥ r \leftrightarrow \forall w \in (ℙ ∖ (1 \dots k)) \neg w ∥ r$
103		breq2	$⊢ r = n \to (w ∥ r \leftrightarrow w ∥ n)$
104	103	notbid	$⊢ r = n \to (\neg w ∥ r \leftrightarrow \neg w ∥ n)$
105	104	ralbidv	$⊢ r = n \to (\forall w \in (ℙ ∖ (1 \dots k)) \neg w ∥ r \leftrightarrow \forall w \in (ℙ ∖ (1 \dots k)) \neg w ∥ n)$
106	102 105	bitrid	$⊢ r = n \to (\forall p \in (ℙ ∖ (1 \dots k)) \neg p ∥ r \leftrightarrow \forall w \in (ℙ ∖ (1 \dots k)) \neg w ∥ n)$
107	106	cbvrabv	$⊢ \{r \in (1 \dots {(2^{k + 1})}^{2}) \| \forall p \in (ℙ ∖ (1 \dots k)) \neg p ∥ r\} = \{n \in (1 \dots {(2^{k + 1})}^{2}) \| \forall w \in (ℙ ∖ (1 \dots k)) \neg w ∥ n\}$
108		simpll	$⊢ ((seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \land \sum_{j \in ℤ_{\geq (k + 1)}} if (j \in ℙ, \frac{1}{j}, 0) < \frac{1}{2}) \to seq 1 (+ F) \in dom ⇝$
109		eleq1w	$⊢ m = j \to (m \in ℙ \leftrightarrow j \in ℙ)$
110		oveq2	$⊢ m = j \to \frac{1}{m} = \frac{1}{j}$
111	109 110	ifbieq1d	$⊢ m = j \to if (m \in ℙ, \frac{1}{m}, 0) = if (j \in ℙ, \frac{1}{j}, 0)$
112	111	cbvsumv	$⊢ \sum_{m \in ℤ_{\geq (k + 1)}} if (m \in ℙ, \frac{1}{m}, 0) = \sum_{j \in ℤ_{\geq (k + 1)}} if (j \in ℙ, \frac{1}{j}, 0)$
113		simpr	$⊢ ((seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \land \sum_{j \in ℤ_{\geq (k + 1)}} if (j \in ℙ, \frac{1}{j}, 0) < \frac{1}{2}) \to \sum_{j \in ℤ_{\geq (k + 1)}} if (j \in ℙ, \frac{1}{j}, 0) < \frac{1}{2}$
114	112 113	eqbrtrid	$⊢ ((seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \land \sum_{j \in ℤ_{\geq (k + 1)}} if (j \in ℙ, \frac{1}{j}, 0) < \frac{1}{2}) \to \sum_{m \in ℤ_{\geq (k + 1)}} if (m \in ℙ, \frac{1}{m}, 0) < \frac{1}{2}$
115		eqid	$⊢ (w \in ℕ ⟼ \{n \in (1 \dots {(2^{k + 1})}^{2}) \| (w \in ℙ \land w ∥ n)\}) = (w \in ℕ ⟼ \{n \in (1 \dots {(2^{k + 1})}^{2}) \| (w \in ℙ \land w ∥ n)\})$
116	1 92 99 107 108 114 115	prmreclem5	$⊢ ((seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \land \sum_{j \in ℤ_{\geq (k + 1)}} if (j \in ℙ, \frac{1}{j}, 0) < \frac{1}{2}) \to \frac{{(2^{k + 1})}^{2}}{2} < 2^{k} \sqrt{{(2^{k + 1})}^{2}}$
117	116	ex	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to (\sum_{j \in ℤ_{\geq (k + 1)}} if (j \in ℙ, \frac{1}{j}, 0) < \frac{1}{2} \to \frac{{(2^{k + 1})}^{2}}{2} < 2^{k} \sqrt{{(2^{k + 1})}^{2}})$
118		eqid	$⊢ ℤ_{\geq (k + 1)} = ℤ_{\geq (k + 1)}$
119	94	nnzd	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to k + 1 \in ℤ$
120		eluznn	$⊢ (k + 1 \in ℕ \land j \in ℤ_{\geq (k + 1)}) \to j \in ℕ$
121	94 120	sylan	$⊢ ((seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \land j \in ℤ_{\geq (k + 1)}) \to j \in ℕ$
122	121 41	syl	$⊢ ((seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \land j \in ℤ_{\geq (k + 1)}) \to F (j) = if (j \in ℙ, \frac{1}{j}, 0)$
123	39	a1i	$⊢ ((seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \land j \in ℤ_{\geq (k + 1)}) \to if (j \in ℙ, \frac{1}{j}, 0) \in ℝ$
124		simpl	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to seq 1 (+ F) \in dom ⇝$
125	41	adantl	$⊢ ((seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \land j \in ℕ) \to F (j) = if (j \in ℙ, \frac{1}{j}, 0)$
126	39	recni	$⊢ if (j \in ℙ, \frac{1}{j}, 0) \in ℂ$
127	126	a1i	$⊢ ((seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \land j \in ℕ) \to if (j \in ℙ, \frac{1}{j}, 0) \in ℂ$
128	125 127	eqeltrd	$⊢ ((seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \land j \in ℕ) \to F (j) \in ℂ$
129	2 94 128	iserex	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to (seq 1 (+ F) \in dom ⇝ \leftrightarrow seq (k + 1) (+ F) \in dom ⇝)$
130	124 129	mpbid	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to seq (k + 1) (+ F) \in dom ⇝$
131	118 119 122 123 130	isumrecl	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to \sum_{j \in ℤ_{\geq (k + 1)}} if (j \in ℙ, \frac{1}{j}, 0) \in ℝ$
132	73	a1i	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to \frac{1}{2} \in ℝ$
133		elfznn	$⊢ j \in (1 \dots k) \to j \in ℕ$
134	133	adantl	$⊢ ((seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \land j \in (1 \dots k)) \to j \in ℕ$
135	134 41	syl	$⊢ ((seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \land j \in (1 \dots k)) \to F (j) = if (j \in ℙ, \frac{1}{j}, 0)$
136	29 2	eleqtrdi	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to k \in ℤ_{\geq 1}$
137	126	a1i	$⊢ ((seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \land j \in (1 \dots k)) \to if (j \in ℙ, \frac{1}{j}, 0) \in ℂ$
138	135 136 137	fsumser	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to \sum_{j = 1}^{k} if (j \in ℙ, \frac{1}{j}, 0) = seq 1 (+ F) (k)$
139	138 27	eqeltrd	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to \sum_{j = 1}^{k} if (j \in ℙ, \frac{1}{j}, 0) \in ℝ$
140	131 132 139	ltadd2d	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to (\sum_{j \in ℤ_{\geq (k + 1)}} if (j \in ℙ, \frac{1}{j}, 0) < \frac{1}{2} \leftrightarrow \sum_{j = 1}^{k} if (j \in ℙ, \frac{1}{j}, 0) + \sum_{j \in ℤ_{\geq (k + 1)}} if (j \in ℙ, \frac{1}{j}, 0) < \sum_{j = 1}^{k} if (j \in ℙ, \frac{1}{j}, 0) + (\frac{1}{2}))$
141	2 118 94 125 127 124	isumsplit	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to \sum_{j \in ℕ} if (j \in ℙ, \frac{1}{j}, 0) = \sum_{j = 1}^{k + 1 - 1} if (j \in ℙ, \frac{1}{j}, 0) + \sum_{j \in ℤ_{\geq (k + 1)}} if (j \in ℙ, \frac{1}{j}, 0)$
142		nncn	$⊢ k \in ℕ \to k \in ℂ$
143	142	adantl	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to k \in ℂ$
144		ax-1cn	$⊢ 1 \in ℂ$
145		pncan	$⊢ (k \in ℂ \land 1 \in ℂ) \to k + 1 - 1 = k$
146	143 144 145	sylancl	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to k + 1 - 1 = k$
147	146	oveq2d	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to (1 \dots k + 1 - 1) = (1 \dots k)$
148	147	sumeq1d	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to \sum_{j = 1}^{k + 1 - 1} if (j \in ℙ, \frac{1}{j}, 0) = \sum_{j = 1}^{k} if (j \in ℙ, \frac{1}{j}, 0)$
149	148	oveq1d	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to \sum_{j = 1}^{k + 1 - 1} if (j \in ℙ, \frac{1}{j}, 0) + \sum_{j \in ℤ_{\geq (k + 1)}} if (j \in ℙ, \frac{1}{j}, 0) = \sum_{j = 1}^{k} if (j \in ℙ, \frac{1}{j}, 0) + \sum_{j \in ℤ_{\geq (k + 1)}} if (j \in ℙ, \frac{1}{j}, 0)$
150	141 149	eqtrd	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to \sum_{j \in ℕ} if (j \in ℙ, \frac{1}{j}, 0) = \sum_{j = 1}^{k} if (j \in ℙ, \frac{1}{j}, 0) + \sum_{j \in ℤ_{\geq (k + 1)}} if (j \in ℙ, \frac{1}{j}, 0)$
151	150	breq1d	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to (\sum_{j \in ℕ} if (j \in ℙ, \frac{1}{j}, 0) < \sum_{j = 1}^{k} if (j \in ℙ, \frac{1}{j}, 0) + (\frac{1}{2}) \leftrightarrow \sum_{j = 1}^{k} if (j \in ℙ, \frac{1}{j}, 0) + \sum_{j \in ℤ_{\geq (k + 1)}} if (j \in ℙ, \frac{1}{j}, 0) < \sum_{j = 1}^{k} if (j \in ℙ, \frac{1}{j}, 0) + (\frac{1}{2}))$
152	140 151	bitr4d	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to (\sum_{j \in ℤ_{\geq (k + 1)}} if (j \in ℙ, \frac{1}{j}, 0) < \frac{1}{2} \leftrightarrow \sum_{j \in ℕ} if (j \in ℙ, \frac{1}{j}, 0) < \sum_{j = 1}^{k} if (j \in ℙ, \frac{1}{j}, 0) + (\frac{1}{2}))$
153		eqid	$⊢ seq 1 (+ F) = seq 1 (+ F)$
154	2 153 23 42 43 54 60	isumsup	$⊢ seq 1 (+ F) \in dom ⇝ \to \sum_{j \in ℕ} if (j \in ℙ, \frac{1}{j}, 0) = sup (ran seq 1 (+ F) ℝ <)$
155	154 67	eqeltrd	$⊢ seq 1 (+ F) \in dom ⇝ \to \sum_{j \in ℕ} if (j \in ℙ, \frac{1}{j}, 0) \in ℝ$
156	155	adantr	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to \sum_{j \in ℕ} if (j \in ℙ, \frac{1}{j}, 0) \in ℝ$
157	156 132 139	ltsubaddd	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to (\sum_{j \in ℕ} if (j \in ℙ, \frac{1}{j}, 0) - (\frac{1}{2}) < \sum_{j = 1}^{k} if (j \in ℙ, \frac{1}{j}, 0) \leftrightarrow \sum_{j \in ℕ} if (j \in ℙ, \frac{1}{j}, 0) < \sum_{j = 1}^{k} if (j \in ℙ, \frac{1}{j}, 0) + (\frac{1}{2}))$
158	154	adantr	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to \sum_{j \in ℕ} if (j \in ℙ, \frac{1}{j}, 0) = sup (ran seq 1 (+ F) ℝ <)$
159	158	oveq1d	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to \sum_{j \in ℕ} if (j \in ℙ, \frac{1}{j}, 0) - (\frac{1}{2}) = sup (ran seq 1 (+ F) ℝ <) - (\frac{1}{2})$
160	159 138	breq12d	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to (\sum_{j \in ℕ} if (j \in ℙ, \frac{1}{j}, 0) - (\frac{1}{2}) < \sum_{j = 1}^{k} if (j \in ℙ, \frac{1}{j}, 0) \leftrightarrow sup (ran seq 1 (+ F) ℝ <) - (\frac{1}{2}) < seq 1 (+ F) (k))$
161	152 157 160	3bitr2d	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to (\sum_{j \in ℤ_{\geq (k + 1)}} if (j \in ℙ, \frac{1}{j}, 0) < \frac{1}{2} \leftrightarrow sup (ran seq 1 (+ F) ℝ <) - (\frac{1}{2}) < seq 1 (+ F) (k))$
162		2cn	$⊢ 2 \in ℂ$
163	162	a1i	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to 2 \in ℂ$
164	144	a1i	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to 1 \in ℂ$
165	163 143 164	adddid	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to 2 (k + 1) = 2 k + 2 \cdot 1$
166	94	nncnd	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to k + 1 \in ℂ$
167		mulcom	$⊢ (k + 1 \in ℂ \land 2 \in ℂ) \to (k + 1) \cdot 2 = 2 (k + 1)$
168	166 162 167	sylancl	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to (k + 1) \cdot 2 = 2 (k + 1)$
169	86	nncnd	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to 2 k \in ℂ$
170	169 164 164	addassd	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to 2 k + 1 + 1 = 2 k + 1 + 1$
171	144	2timesi	$⊢ 2 \cdot 1 = 1 + 1$
172	171	oveq2i	$⊢ 2 k + 2 \cdot 1 = 2 k + 1 + 1$
173	170 172	eqtr4di	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to 2 k + 1 + 1 = 2 k + 2 \cdot 1$
174	165 168 173	3eqtr4d	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to (k + 1) \cdot 2 = 2 k + 1 + 1$
175	174	oveq2d	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to 2^{(k + 1) \cdot 2} = 2^{2 k + 1 + 1}$
176		2nn0	$⊢ 2 \in ℕ_{0}$
177	176	a1i	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to 2 \in ℕ_{0}$
178	163 177 95	expmuld	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to 2^{(k + 1) \cdot 2} = {(2^{k + 1})}^{2}$
179		expp1	$⊢ (2 \in ℂ \land 2 k + 1 \in ℕ_{0}) \to 2^{2 k + 1 + 1} = 2^{2 k + 1} \cdot 2$
180	162 88 179	sylancr	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to 2^{2 k + 1 + 1} = 2^{2 k + 1} \cdot 2$
181	175 178 180	3eqtr3d	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to {(2^{k + 1})}^{2} = 2^{2 k + 1} \cdot 2$
182	181	oveq1d	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to \frac{{(2^{k + 1})}^{2}}{2} = \frac{2^{2 k + 1} \cdot 2}{2}$
183		expcl	$⊢ (2 \in ℂ \land 2 k + 1 \in ℕ_{0}) \to 2^{2 k + 1} \in ℂ$
184	162 88 183	sylancr	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to 2^{2 k + 1} \in ℂ$
185		2ne0	$⊢ 2 \neq 0$
186		divcan4	$⊢ (2^{2 k + 1} \in ℂ \land 2 \in ℂ \land 2 \neq 0) \to \frac{2^{2 k + 1} \cdot 2}{2} = 2^{2 k + 1}$
187	162 185 186	mp3an23	$⊢ 2^{2 k + 1} \in ℂ \to \frac{2^{2 k + 1} \cdot 2}{2} = 2^{2 k + 1}$
188	184 187	syl	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to \frac{2^{2 k + 1} \cdot 2}{2} = 2^{2 k + 1}$
189	182 188	eqtrd	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to \frac{{(2^{k + 1})}^{2}}{2} = 2^{2 k + 1}$
190		nnnn0	$⊢ k \in ℕ \to k \in ℕ_{0}$
191	190	adantl	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to k \in ℕ_{0}$
192	163 95 191	expaddd	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to 2^{k + k + 1} = 2^{k} 2^{k + 1}$
193	143	2timesd	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to 2 k = k + k$
194	193	oveq1d	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to 2 k + 1 = k + k + 1$
195	143 143 164	addassd	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to k + k + 1 = k + k + 1$
196	194 195	eqtrd	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to 2 k + 1 = k + k + 1$
197	196	oveq2d	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to 2^{2 k + 1} = 2^{k + k + 1}$
198	97	nnrpd	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to 2^{k + 1} \in ℝ^{+}$
199	198	rprege0d	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to (2^{k + 1} \in ℝ \land 0 \leq 2^{k + 1})$
200		sqrtsq	$⊢ (2^{k + 1} \in ℝ \land 0 \leq 2^{k + 1}) \to \sqrt{{(2^{k + 1})}^{2}} = 2^{k + 1}$
201	199 200	syl	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to \sqrt{{(2^{k + 1})}^{2}} = 2^{k + 1}$
202	201	oveq2d	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to 2^{k} \sqrt{{(2^{k + 1})}^{2}} = 2^{k} 2^{k + 1}$
203	192 197 202	3eqtr4rd	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to 2^{k} \sqrt{{(2^{k + 1})}^{2}} = 2^{2 k + 1}$
204	189 203	breq12d	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to (\frac{{(2^{k + 1})}^{2}}{2} < 2^{k} \sqrt{{(2^{k + 1})}^{2}} \leftrightarrow 2^{2 k + 1} < 2^{2 k + 1})$
205	117 161 204	3imtr3d	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to (sup (ran seq 1 (+ F) ℝ <) - (\frac{1}{2}) < seq 1 (+ F) (k) \to 2^{2 k + 1} < 2^{2 k + 1})$
206	91 205	mtod	$⊢ (seq 1 (+ F) \in dom ⇝ \land k \in ℕ) \to \neg sup (ran seq 1 (+ F) ℝ <) - (\frac{1}{2}) < seq 1 (+ F) (k)$
207	206	nrexdv	$⊢ seq 1 (+ F) \in dom ⇝ \to \neg \exists k \in ℕ sup (ran seq 1 (+ F) ℝ <) - (\frac{1}{2}) < seq 1 (+ F) (k)$
208	82 207	pm2.65i	$⊢ \neg seq 1 (+ F) \in dom ⇝$

Metamath Proof Explorer

Theorem prmreclem6

Proof