chpchtsum

Description: The second Chebyshev function is the sum of the theta function at arguments quickly approaching zero. (This is usually stated as an infinite sum, but after a certain point, the terms are all zero, and it is easier for us to use an explicit finite sum.) (Contributed by Mario Carneiro, 7-Apr-2016)

		Ref	Expression
	Assertion	chpchtsum	$⊢ A \in ℝ \to ψ (A) = \sum_{k = 1}^{⌊A⌋} θ (A^{\frac{1}{k}})$

Proof

Step	Hyp	Ref	Expression
1		fzfid	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to (1 \dots ⌊\frac{\log A}{\log p}⌋) \in Fin$
2		simpr	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to p \in ([0, A] \cap ℙ)$
3	2	elin2d	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to p \in ℙ$
4		prmnn	$⊢ p \in ℙ \to p \in ℕ$
5	3 4	syl	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to p \in ℕ$
6	5	nnrpd	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to p \in ℝ^{+}$
7	6	relogcld	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to \log p \in ℝ$
8	7	recnd	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to \log p \in ℂ$
9		fsumconst	$⊢ ((1 \dots ⌊\frac{\log A}{\log p}⌋) \in Fin \land \log p \in ℂ) \to \sum_{k = 1}^{⌊\frac{\log A}{\log p}⌋} \log p = \|(1 \dots ⌊\frac{\log A}{\log p}⌋)\| \log p$
10	1 8 9	syl2anc	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to \sum_{k = 1}^{⌊\frac{\log A}{\log p}⌋} \log p = \|(1 \dots ⌊\frac{\log A}{\log p}⌋)\| \log p$
11		simpl	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to A \in ℝ$
12		1red	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to 1 \in ℝ$
13	5	nnred	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to p \in ℝ$
14		prmuz2	$⊢ p \in ℙ \to p \in ℤ_{\geq 2}$
15	3 14	syl	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to p \in ℤ_{\geq 2}$
16		eluz2gt1	$⊢ p \in ℤ_{\geq 2} \to 1 < p$
17	15 16	syl	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to 1 < p$
18	2	elin1d	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to p \in [0, A]$
19		0re	$⊢ 0 \in ℝ$
20		elicc2	$⊢ (0 \in ℝ \land A \in ℝ) \to (p \in [0, A] \leftrightarrow (p \in ℝ \land 0 \leq p \land p \leq A))$
21	19 11 20	sylancr	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to (p \in [0, A] \leftrightarrow (p \in ℝ \land 0 \leq p \land p \leq A))$
22	18 21	mpbid	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to (p \in ℝ \land 0 \leq p \land p \leq A)$
23	22	simp3d	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to p \leq A$
24	12 13 11 17 23	ltletrd	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to 1 < A$
25	11 24	rplogcld	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to \log A \in ℝ^{+}$
26	13 17	rplogcld	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to \log p \in ℝ^{+}$
27	25 26	rpdivcld	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to \frac{\log A}{\log p} \in ℝ^{+}$
28	27	rpred	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to \frac{\log A}{\log p} \in ℝ$
29	27	rpge0d	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to 0 \leq \frac{\log A}{\log p}$
30		flge0nn0	$⊢ (\frac{\log A}{\log p} \in ℝ \land 0 \leq \frac{\log A}{\log p}) \to ⌊\frac{\log A}{\log p}⌋ \in ℕ_{0}$
31	28 29 30	syl2anc	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to ⌊\frac{\log A}{\log p}⌋ \in ℕ_{0}$
32		hashfz1	$⊢ ⌊\frac{\log A}{\log p}⌋ \in ℕ_{0} \to \|(1 \dots ⌊\frac{\log A}{\log p}⌋)\| = ⌊\frac{\log A}{\log p}⌋$
33	31 32	syl	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to \|(1 \dots ⌊\frac{\log A}{\log p}⌋)\| = ⌊\frac{\log A}{\log p}⌋$
34	33	oveq1d	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to \|(1 \dots ⌊\frac{\log A}{\log p}⌋)\| \log p = ⌊\frac{\log A}{\log p}⌋ \log p$
35	28	flcld	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to ⌊\frac{\log A}{\log p}⌋ \in ℤ$
36	35	zcnd	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to ⌊\frac{\log A}{\log p}⌋ \in ℂ$
37	36 8	mulcomd	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to ⌊\frac{\log A}{\log p}⌋ \log p = \log p ⌊\frac{\log A}{\log p}⌋$
38	10 34 37	3eqtrrd	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to \log p ⌊\frac{\log A}{\log p}⌋ = \sum_{k = 1}^{⌊\frac{\log A}{\log p}⌋} \log p$
39	38	sumeq2dv	$⊢ A \in ℝ \to \sum_{p \in [0, A] \cap ℙ} \log p ⌊\frac{\log A}{\log p}⌋ = \sum_{p \in [0, A] \cap ℙ} \sum_{k = 1}^{⌊\frac{\log A}{\log p}⌋} \log p$
40		chpval2	$⊢ A \in ℝ \to ψ (A) = \sum_{p \in [0, A] \cap ℙ} \log p ⌊\frac{\log A}{\log p}⌋$
41		simpl	$⊢ (A \in ℝ \land k \in (1 \dots ⌊A⌋)) \to A \in ℝ$
42		0red	$⊢ (A \in ℝ \land k \in (1 \dots ⌊A⌋)) \to 0 \in ℝ$
43		1red	$⊢ (A \in ℝ \land k \in (1 \dots ⌊A⌋)) \to 1 \in ℝ$
44		0lt1	$⊢ 0 < 1$
45	44	a1i	$⊢ (A \in ℝ \land k \in (1 \dots ⌊A⌋)) \to 0 < 1$
46		elfzuz2	$⊢ k \in (1 \dots ⌊A⌋) \to ⌊A⌋ \in ℤ_{\geq 1}$
47		eluzle	$⊢ ⌊A⌋ \in ℤ_{\geq 1} \to 1 \leq ⌊A⌋$
48	47	adantl	$⊢ (A \in ℝ \land ⌊A⌋ \in ℤ_{\geq 1}) \to 1 \leq ⌊A⌋$
49		simpl	$⊢ (A \in ℝ \land ⌊A⌋ \in ℤ_{\geq 1}) \to A \in ℝ$
50		1z	$⊢ 1 \in ℤ$
51		flge	$⊢ (A \in ℝ \land 1 \in ℤ) \to (1 \leq A \leftrightarrow 1 \leq ⌊A⌋)$
52	49 50 51	sylancl	$⊢ (A \in ℝ \land ⌊A⌋ \in ℤ_{\geq 1}) \to (1 \leq A \leftrightarrow 1 \leq ⌊A⌋)$
53	48 52	mpbird	$⊢ (A \in ℝ \land ⌊A⌋ \in ℤ_{\geq 1}) \to 1 \leq A$
54	46 53	sylan2	$⊢ (A \in ℝ \land k \in (1 \dots ⌊A⌋)) \to 1 \leq A$
55	42 43 41 45 54	ltletrd	$⊢ (A \in ℝ \land k \in (1 \dots ⌊A⌋)) \to 0 < A$
56	42 41 55	ltled	$⊢ (A \in ℝ \land k \in (1 \dots ⌊A⌋)) \to 0 \leq A$
57		elfznn	$⊢ k \in (1 \dots ⌊A⌋) \to k \in ℕ$
58	57	adantl	$⊢ (A \in ℝ \land k \in (1 \dots ⌊A⌋)) \to k \in ℕ$
59	58	nnrecred	$⊢ (A \in ℝ \land k \in (1 \dots ⌊A⌋)) \to \frac{1}{k} \in ℝ$
60	41 56 59	recxpcld	$⊢ (A \in ℝ \land k \in (1 \dots ⌊A⌋)) \to A^{\frac{1}{k}} \in ℝ$
61		chtval	$⊢ A^{\frac{1}{k}} \in ℝ \to θ (A^{\frac{1}{k}}) = \sum_{p \in [0, A^{\frac{1}{k}}] \cap ℙ} \log p$
62	60 61	syl	$⊢ (A \in ℝ \land k \in (1 \dots ⌊A⌋)) \to θ (A^{\frac{1}{k}}) = \sum_{p \in [0, A^{\frac{1}{k}}] \cap ℙ} \log p$
63	62	sumeq2dv	$⊢ A \in ℝ \to \sum_{k = 1}^{⌊A⌋} θ (A^{\frac{1}{k}}) = \sum_{k = 1}^{⌊A⌋} \sum_{p \in [0, A^{\frac{1}{k}}] \cap ℙ} \log p$
64		ppifi	$⊢ A \in ℝ \to [0, A] \cap ℙ \in Fin$
65		fzfid	$⊢ A \in ℝ \to (1 \dots ⌊A⌋) \in Fin$
66		elinel2	$⊢ p \in ([0, A] \cap ℙ) \to p \in ℙ$
67		elfznn	$⊢ k \in (1 \dots ⌊\frac{\log A}{\log p}⌋) \to k \in ℕ$
68	66 67	anim12i	$⊢ (p \in ([0, A] \cap ℙ) \land k \in (1 \dots ⌊\frac{\log A}{\log p}⌋)) \to (p \in ℙ \land k \in ℕ)$
69	68	a1i	$⊢ A \in ℝ \to ((p \in ([0, A] \cap ℙ) \land k \in (1 \dots ⌊\frac{\log A}{\log p}⌋)) \to (p \in ℙ \land k \in ℕ))$
70		0red	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to 0 \in ℝ$
71		inss2	$⊢ [0, A] \cap ℙ \subseteq ℙ$
72	71	a1i	$⊢ A \in ℝ \to [0, A] \cap ℙ \subseteq ℙ$
73	72	sselda	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to p \in ℙ$
74	73 4	syl	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to p \in ℕ$
75	74	nnred	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to p \in ℝ$
76	74	nngt0d	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to 0 < p$
77	70 75 11 76 23	ltletrd	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to 0 < A$
78	77	ex	$⊢ A \in ℝ \to (p \in ([0, A] \cap ℙ) \to 0 < A)$
79	78	adantrd	$⊢ A \in ℝ \to ((p \in ([0, A] \cap ℙ) \land k \in (1 \dots ⌊\frac{\log A}{\log p}⌋)) \to 0 < A)$
80	69 79	jcad	$⊢ A \in ℝ \to ((p \in ([0, A] \cap ℙ) \land k \in (1 \dots ⌊\frac{\log A}{\log p}⌋)) \to ((p \in ℙ \land k \in ℕ) \land 0 < A))$
81		elinel2	$⊢ p \in ([0, A^{\frac{1}{k}}] \cap ℙ) \to p \in ℙ$
82	57 81	anim12ci	$⊢ (k \in (1 \dots ⌊A⌋) \land p \in ([0, A^{\frac{1}{k}}] \cap ℙ)) \to (p \in ℙ \land k \in ℕ)$
83	82	a1i	$⊢ A \in ℝ \to ((k \in (1 \dots ⌊A⌋) \land p \in ([0, A^{\frac{1}{k}}] \cap ℙ)) \to (p \in ℙ \land k \in ℕ))$
84	55	ex	$⊢ A \in ℝ \to (k \in (1 \dots ⌊A⌋) \to 0 < A)$
85	84	adantrd	$⊢ A \in ℝ \to ((k \in (1 \dots ⌊A⌋) \land p \in ([0, A^{\frac{1}{k}}] \cap ℙ)) \to 0 < A)$
86	83 85	jcad	$⊢ A \in ℝ \to ((k \in (1 \dots ⌊A⌋) \land p \in ([0, A^{\frac{1}{k}}] \cap ℙ)) \to ((p \in ℙ \land k \in ℕ) \land 0 < A))$
87		elin	$⊢ p \in ([0, A] \cap ℙ) \leftrightarrow (p \in [0, A] \land p \in ℙ)$
88		simprll	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to p \in ℙ$
89	88	biantrud	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to (p \in [0, A] \leftrightarrow (p \in [0, A] \land p \in ℙ))$
90		0red	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to 0 \in ℝ$
91		simpl	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to A \in ℝ$
92	88 4	syl	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to p \in ℕ$
93	92	nnred	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to p \in ℝ$
94	92	nnnn0d	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to p \in ℕ_{0}$
95	94	nn0ge0d	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to 0 \leq p$
96		df-3an	$⊢ (p \in ℝ \land 0 \leq p \land p \leq A) \leftrightarrow ((p \in ℝ \land 0 \leq p) \land p \leq A)$
97	20 96	bitrdi	$⊢ (0 \in ℝ \land A \in ℝ) \to (p \in [0, A] \leftrightarrow ((p \in ℝ \land 0 \leq p) \land p \leq A))$
98	97	baibd	$⊢ ((0 \in ℝ \land A \in ℝ) \land (p \in ℝ \land 0 \leq p)) \to (p \in [0, A] \leftrightarrow p \leq A)$
99	90 91 93 95 98	syl22anc	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to (p \in [0, A] \leftrightarrow p \leq A)$
100	89 99	bitr3d	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to ((p \in [0, A] \land p \in ℙ) \leftrightarrow p \leq A)$
101	87 100	syl5bb	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to (p \in ([0, A] \cap ℙ) \leftrightarrow p \leq A)$
102		simprr	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to 0 < A$
103	91 102	elrpd	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to A \in ℝ^{+}$
104	103	relogcld	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to \log A \in ℝ$
105	88 14	syl	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to p \in ℤ_{\geq 2}$
106	105 16	syl	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to 1 < p$
107	93 106	rplogcld	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to \log p \in ℝ^{+}$
108	104 107	rerpdivcld	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to \frac{\log A}{\log p} \in ℝ$
109		simprlr	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to k \in ℕ$
110	109	nnzd	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to k \in ℤ$
111		flge	$⊢ (\frac{\log A}{\log p} \in ℝ \land k \in ℤ) \to (k \leq \frac{\log A}{\log p} \leftrightarrow k \leq ⌊\frac{\log A}{\log p}⌋)$
112	108 110 111	syl2anc	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to (k \leq \frac{\log A}{\log p} \leftrightarrow k \leq ⌊\frac{\log A}{\log p}⌋)$
113	109	nnnn0d	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to k \in ℕ_{0}$
114	92 113	nnexpcld	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to p^{k} \in ℕ$
115	114	nnrpd	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to p^{k} \in ℝ^{+}$
116	115 103	logled	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to (p^{k} \leq A \leftrightarrow \log p^{k} \leq \log A)$
117	92	nnrpd	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to p \in ℝ^{+}$
118		relogexp	$⊢ (p \in ℝ^{+} \land k \in ℤ) \to \log p^{k} = k \log p$
119	117 110 118	syl2anc	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to \log p^{k} = k \log p$
120	119	breq1d	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to (\log p^{k} \leq \log A \leftrightarrow k \log p \leq \log A)$
121	109	nnred	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to k \in ℝ$
122	121 104 107	lemuldivd	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to (k \log p \leq \log A \leftrightarrow k \leq \frac{\log A}{\log p})$
123	116 120 122	3bitrd	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to (p^{k} \leq A \leftrightarrow k \leq \frac{\log A}{\log p})$
124		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
125	109 124	eleqtrdi	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to k \in ℤ_{\geq 1}$
126	108	flcld	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to ⌊\frac{\log A}{\log p}⌋ \in ℤ$
127		elfz5	$⊢ (k \in ℤ_{\geq 1} \land ⌊\frac{\log A}{\log p}⌋ \in ℤ) \to (k \in (1 \dots ⌊\frac{\log A}{\log p}⌋) \leftrightarrow k \leq ⌊\frac{\log A}{\log p}⌋)$
128	125 126 127	syl2anc	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to (k \in (1 \dots ⌊\frac{\log A}{\log p}⌋) \leftrightarrow k \leq ⌊\frac{\log A}{\log p}⌋)$
129	112 123 128	3bitr4rd	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to (k \in (1 \dots ⌊\frac{\log A}{\log p}⌋) \leftrightarrow p^{k} \leq A)$
130	101 129	anbi12d	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to ((p \in ([0, A] \cap ℙ) \land k \in (1 \dots ⌊\frac{\log A}{\log p}⌋)) \leftrightarrow (p \leq A \land p^{k} \leq A))$
131	91	flcld	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to ⌊A⌋ \in ℤ$
132		elfz5	$⊢ (k \in ℤ_{\geq 1} \land ⌊A⌋ \in ℤ) \to (k \in (1 \dots ⌊A⌋) \leftrightarrow k \leq ⌊A⌋)$
133	125 131 132	syl2anc	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to (k \in (1 \dots ⌊A⌋) \leftrightarrow k \leq ⌊A⌋)$
134		flge	$⊢ (A \in ℝ \land k \in ℤ) \to (k \leq A \leftrightarrow k \leq ⌊A⌋)$
135	91 110 134	syl2anc	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to (k \leq A \leftrightarrow k \leq ⌊A⌋)$
136	133 135	bitr4d	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to (k \in (1 \dots ⌊A⌋) \leftrightarrow k \leq A)$
137		elin	$⊢ p \in ([0, A^{\frac{1}{k}}] \cap ℙ) \leftrightarrow (p \in [0, A^{\frac{1}{k}}] \land p \in ℙ)$
138	88	biantrud	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to (p \in [0, A^{\frac{1}{k}}] \leftrightarrow (p \in [0, A^{\frac{1}{k}}] \land p \in ℙ))$
139	103	rpge0d	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to 0 \leq A$
140	109	nnrecred	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to \frac{1}{k} \in ℝ$
141	91 139 140	recxpcld	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to A^{\frac{1}{k}} \in ℝ$
142		elicc2	$⊢ (0 \in ℝ \land A^{\frac{1}{k}} \in ℝ) \to (p \in [0, A^{\frac{1}{k}}] \leftrightarrow (p \in ℝ \land 0 \leq p \land p \leq A^{\frac{1}{k}}))$
143		df-3an	$⊢ (p \in ℝ \land 0 \leq p \land p \leq A^{\frac{1}{k}}) \leftrightarrow ((p \in ℝ \land 0 \leq p) \land p \leq A^{\frac{1}{k}})$
144	142 143	bitrdi	$⊢ (0 \in ℝ \land A^{\frac{1}{k}} \in ℝ) \to (p \in [0, A^{\frac{1}{k}}] \leftrightarrow ((p \in ℝ \land 0 \leq p) \land p \leq A^{\frac{1}{k}}))$
145	144	baibd	$⊢ ((0 \in ℝ \land A^{\frac{1}{k}} \in ℝ) \land (p \in ℝ \land 0 \leq p)) \to (p \in [0, A^{\frac{1}{k}}] \leftrightarrow p \leq A^{\frac{1}{k}})$
146	90 141 93 95 145	syl22anc	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to (p \in [0, A^{\frac{1}{k}}] \leftrightarrow p \leq A^{\frac{1}{k}})$
147	138 146	bitr3d	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to ((p \in [0, A^{\frac{1}{k}}] \land p \in ℙ) \leftrightarrow p \leq A^{\frac{1}{k}})$
148	91 139 140	cxpge0d	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to 0 \leq A^{\frac{1}{k}}$
149	109	nnrpd	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to k \in ℝ^{+}$
150	93 95 141 148 149	cxple2d	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to (p \leq A^{\frac{1}{k}} \leftrightarrow p^{k} \leq {(A^{\frac{1}{k}})}^{k})$
151	92	nncnd	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to p \in ℂ$
152		cxpexp	$⊢ (p \in ℂ \land k \in ℕ_{0}) \to p^{k} = p^{k}$
153	151 113 152	syl2anc	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to p^{k} = p^{k}$
154	109	nncnd	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to k \in ℂ$
155	109	nnne0d	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to k \neq 0$
156	154 155	recid2d	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to (\frac{1}{k}) k = 1$
157	156	oveq2d	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to A^{(\frac{1}{k}) k} = A^{1}$
158	103 140 154	cxpmuld	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to A^{(\frac{1}{k}) k} = {(A^{\frac{1}{k}})}^{k}$
159	91	recnd	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to A \in ℂ$
160	159	cxp1d	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to A^{1} = A$
161	157 158 160	3eqtr3d	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to {(A^{\frac{1}{k}})}^{k} = A$
162	153 161	breq12d	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to (p^{k} \leq {(A^{\frac{1}{k}})}^{k} \leftrightarrow p^{k} \leq A)$
163	147 150 162	3bitrd	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to ((p \in [0, A^{\frac{1}{k}}] \land p \in ℙ) \leftrightarrow p^{k} \leq A)$
164	137 163	syl5bb	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to (p \in ([0, A^{\frac{1}{k}}] \cap ℙ) \leftrightarrow p^{k} \leq A)$
165	136 164	anbi12d	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to ((k \in (1 \dots ⌊A⌋) \land p \in ([0, A^{\frac{1}{k}}] \cap ℙ)) \leftrightarrow (k \leq A \land p^{k} \leq A))$
166	114	nnred	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to p^{k} \in ℝ$
167		bernneq3	$⊢ (p \in ℤ_{\geq 2} \land k \in ℕ_{0}) \to k < p^{k}$
168	105 113 167	syl2anc	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to k < p^{k}$
169	121 166 168	ltled	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to k \leq p^{k}$
170		letr	$⊢ (k \in ℝ \land p^{k} \in ℝ \land A \in ℝ) \to ((k \leq p^{k} \land p^{k} \leq A) \to k \leq A)$
171	121 166 91 170	syl3anc	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to ((k \leq p^{k} \land p^{k} \leq A) \to k \leq A)$
172	169 171	mpand	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to (p^{k} \leq A \to k \leq A)$
173	172	pm4.71rd	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to (p^{k} \leq A \leftrightarrow (k \leq A \land p^{k} \leq A))$
174	151	exp1d	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to p^{1} = p$
175	92	nnge1d	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to 1 \leq p$
176	93 175 125	leexp2ad	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to p^{1} \leq p^{k}$
177	174 176	eqbrtrrd	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to p \leq p^{k}$
178		letr	$⊢ (p \in ℝ \land p^{k} \in ℝ \land A \in ℝ) \to ((p \leq p^{k} \land p^{k} \leq A) \to p \leq A)$
179	93 166 91 178	syl3anc	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to ((p \leq p^{k} \land p^{k} \leq A) \to p \leq A)$
180	177 179	mpand	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to (p^{k} \leq A \to p \leq A)$
181	180	pm4.71rd	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to (p^{k} \leq A \leftrightarrow (p \leq A \land p^{k} \leq A))$
182	165 173 181	3bitr2rd	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to ((p \leq A \land p^{k} \leq A) \leftrightarrow (k \in (1 \dots ⌊A⌋) \land p \in ([0, A^{\frac{1}{k}}] \cap ℙ)))$
183	130 182	bitrd	$⊢ (A \in ℝ \land ((p \in ℙ \land k \in ℕ) \land 0 < A)) \to ((p \in ([0, A] \cap ℙ) \land k \in (1 \dots ⌊\frac{\log A}{\log p}⌋)) \leftrightarrow (k \in (1 \dots ⌊A⌋) \land p \in ([0, A^{\frac{1}{k}}] \cap ℙ)))$
184	183	ex	$⊢ A \in ℝ \to (((p \in ℙ \land k \in ℕ) \land 0 < A) \to ((p \in ([0, A] \cap ℙ) \land k \in (1 \dots ⌊\frac{\log A}{\log p}⌋)) \leftrightarrow (k \in (1 \dots ⌊A⌋) \land p \in ([0, A^{\frac{1}{k}}] \cap ℙ))))$
185	80 86 184	pm5.21ndd	$⊢ A \in ℝ \to ((p \in ([0, A] \cap ℙ) \land k \in (1 \dots ⌊\frac{\log A}{\log p}⌋)) \leftrightarrow (k \in (1 \dots ⌊A⌋) \land p \in ([0, A^{\frac{1}{k}}] \cap ℙ)))$
186	8	adantrr	$⊢ (A \in ℝ \land (p \in ([0, A] \cap ℙ) \land k \in (1 \dots ⌊\frac{\log A}{\log p}⌋))) \to \log p \in ℂ$
187	64 65 1 185 186	fsumcom2	$⊢ A \in ℝ \to \sum_{p \in [0, A] \cap ℙ} \sum_{k = 1}^{⌊\frac{\log A}{\log p}⌋} \log p = \sum_{k = 1}^{⌊A⌋} \sum_{p \in [0, A^{\frac{1}{k}}] \cap ℙ} \log p$
188	63 187	eqtr4d	$⊢ A \in ℝ \to \sum_{k = 1}^{⌊A⌋} θ (A^{\frac{1}{k}}) = \sum_{p \in [0, A] \cap ℙ} \sum_{k = 1}^{⌊\frac{\log A}{\log p}⌋} \log p$
189	39 40 188	3eqtr4d	$⊢ A \in ℝ \to ψ (A) = \sum_{k = 1}^{⌊A⌋} θ (A^{\frac{1}{k}})$

Metamath Proof Explorer

Theorem chpchtsum

Proof