fsumvma2

Description: Apply fsumvma for the common case of all numbers less than a real number A . (Contributed by Mario Carneiro, 30-Apr-2016)

	Ref	Expression
Hypotheses	fsumvma2.1	$⊢ x = p^{k} \to B = C$
	fsumvma2.2	$⊢ φ \to A \in ℝ$
	fsumvma2.3	$⊢ (φ \land x \in (1 \dots ⌊A⌋)) \to B \in ℂ$
	fsumvma2.4	$⊢ (φ \land (x \in (1 \dots ⌊A⌋) \land Λ (x) = 0)) \to B = 0$
Assertion	fsumvma2	$⊢ φ \to \sum_{x = 1}^{⌊A⌋} B = \sum_{p \in [0, A] \cap ℙ} \sum_{k = 1}^{⌊\frac{\log A}{\log p}⌋} C$

Proof

Step	Hyp	Ref	Expression
1		fsumvma2.1	$⊢ x = p^{k} \to B = C$
2		fsumvma2.2	$⊢ φ \to A \in ℝ$
3		fsumvma2.3	$⊢ (φ \land x \in (1 \dots ⌊A⌋)) \to B \in ℂ$
4		fsumvma2.4	$⊢ (φ \land (x \in (1 \dots ⌊A⌋) \land Λ (x) = 0)) \to B = 0$
5		fzfid	$⊢ φ \to (1 \dots ⌊A⌋) \in Fin$
6		fz1ssnn	$⊢ (1 \dots ⌊A⌋) \subseteq ℕ$
7	6	a1i	$⊢ φ \to (1 \dots ⌊A⌋) \subseteq ℕ$
8		ppifi	$⊢ A \in ℝ \to [0, A] \cap ℙ \in Fin$
9	2 8	syl	$⊢ φ \to [0, A] \cap ℙ \in Fin$
10		elinel2	$⊢ p \in ([0, A] \cap ℙ) \to p \in ℙ$
11		elfznn	$⊢ k \in (1 \dots ⌊\frac{\log A}{\log p}⌋) \to k \in ℕ$
12	10 11	anim12i	$⊢ (p \in ([0, A] \cap ℙ) \land k \in (1 \dots ⌊\frac{\log A}{\log p}⌋)) \to (p \in ℙ \land k \in ℕ)$
13	12	pm4.71ri	$⊢ (p \in ([0, A] \cap ℙ) \land k \in (1 \dots ⌊\frac{\log A}{\log p}⌋)) \leftrightarrow ((p \in ℙ \land k \in ℕ) \land (p \in ([0, A] \cap ℙ) \land k \in (1 \dots ⌊\frac{\log A}{\log p}⌋)))$
14	2	adantr	$⊢ (φ \land (p \in ℙ \land k \in ℕ)) \to A \in ℝ$
15		prmnn	$⊢ p \in ℙ \to p \in ℕ$
16	15	ad2antrl	$⊢ (φ \land (p \in ℙ \land k \in ℕ)) \to p \in ℕ$
17		nnnn0	$⊢ k \in ℕ \to k \in ℕ_{0}$
18	17	ad2antll	$⊢ (φ \land (p \in ℙ \land k \in ℕ)) \to k \in ℕ_{0}$
19	16 18	nnexpcld	$⊢ (φ \land (p \in ℙ \land k \in ℕ)) \to p^{k} \in ℕ$
20	19	nnzd	$⊢ (φ \land (p \in ℙ \land k \in ℕ)) \to p^{k} \in ℤ$
21		flge	$⊢ (A \in ℝ \land p^{k} \in ℤ) \to (p^{k} \leq A \leftrightarrow p^{k} \leq ⌊A⌋)$
22	14 20 21	syl2anc	$⊢ (φ \land (p \in ℙ \land k \in ℕ)) \to (p^{k} \leq A \leftrightarrow p^{k} \leq ⌊A⌋)$
23		simplrl	$⊢ ((φ \land (p \in ℙ \land k \in ℕ)) \land p \in [0, A]) \to p \in ℙ$
24	23 15	syl	$⊢ ((φ \land (p \in ℙ \land k \in ℕ)) \land p \in [0, A]) \to p \in ℕ$
25	24	nnrpd	$⊢ ((φ \land (p \in ℙ \land k \in ℕ)) \land p \in [0, A]) \to p \in ℝ^{+}$
26		simplrr	$⊢ ((φ \land (p \in ℙ \land k \in ℕ)) \land p \in [0, A]) \to k \in ℕ$
27	26	nnzd	$⊢ ((φ \land (p \in ℙ \land k \in ℕ)) \land p \in [0, A]) \to k \in ℤ$
28		relogexp	$⊢ (p \in ℝ^{+} \land k \in ℤ) \to \log p^{k} = k \log p$
29	25 27 28	syl2anc	$⊢ ((φ \land (p \in ℙ \land k \in ℕ)) \land p \in [0, A]) \to \log p^{k} = k \log p$
30	29	breq1d	$⊢ ((φ \land (p \in ℙ \land k \in ℕ)) \land p \in [0, A]) \to (\log p^{k} \leq \log A \leftrightarrow k \log p \leq \log A)$
31	26	nnred	$⊢ ((φ \land (p \in ℙ \land k \in ℕ)) \land p \in [0, A]) \to k \in ℝ$
32	14	adantr	$⊢ ((φ \land (p \in ℙ \land k \in ℕ)) \land p \in [0, A]) \to A \in ℝ$
33		0red	$⊢ ((φ \land (p \in ℙ \land k \in ℕ)) \land p \in [0, A]) \to 0 \in ℝ$
34	16	nnred	$⊢ (φ \land (p \in ℙ \land k \in ℕ)) \to p \in ℝ$
35	34	adantr	$⊢ ((φ \land (p \in ℙ \land k \in ℕ)) \land p \in [0, A]) \to p \in ℝ$
36	24	nngt0d	$⊢ ((φ \land (p \in ℙ \land k \in ℕ)) \land p \in [0, A]) \to 0 < p$
37		0red	$⊢ (φ \land (p \in ℙ \land k \in ℕ)) \to 0 \in ℝ$
38	16	nnnn0d	$⊢ (φ \land (p \in ℙ \land k \in ℕ)) \to p \in ℕ_{0}$
39	38	nn0ge0d	$⊢ (φ \land (p \in ℙ \land k \in ℕ)) \to 0 \leq p$
40		elicc2	$⊢ (0 \in ℝ \land A \in ℝ) \to (p \in [0, A] \leftrightarrow (p \in ℝ \land 0 \leq p \land p \leq A))$
41		df-3an	$⊢ (p \in ℝ \land 0 \leq p \land p \leq A) \leftrightarrow ((p \in ℝ \land 0 \leq p) \land p \leq A)$
42	40 41	bitrdi	$⊢ (0 \in ℝ \land A \in ℝ) \to (p \in [0, A] \leftrightarrow ((p \in ℝ \land 0 \leq p) \land p \leq A))$
43	42	baibd	$⊢ ((0 \in ℝ \land A \in ℝ) \land (p \in ℝ \land 0 \leq p)) \to (p \in [0, A] \leftrightarrow p \leq A)$
44	37 14 34 39 43	syl22anc	$⊢ (φ \land (p \in ℙ \land k \in ℕ)) \to (p \in [0, A] \leftrightarrow p \leq A)$
45	44	biimpa	$⊢ ((φ \land (p \in ℙ \land k \in ℕ)) \land p \in [0, A]) \to p \leq A$
46	33 35 32 36 45	ltletrd	$⊢ ((φ \land (p \in ℙ \land k \in ℕ)) \land p \in [0, A]) \to 0 < A$
47	32 46	elrpd	$⊢ ((φ \land (p \in ℙ \land k \in ℕ)) \land p \in [0, A]) \to A \in ℝ^{+}$
48	47	relogcld	$⊢ ((φ \land (p \in ℙ \land k \in ℕ)) \land p \in [0, A]) \to \log A \in ℝ$
49		prmuz2	$⊢ p \in ℙ \to p \in ℤ_{\geq 2}$
50		eluzelre	$⊢ p \in ℤ_{\geq 2} \to p \in ℝ$
51		eluz2gt1	$⊢ p \in ℤ_{\geq 2} \to 1 < p$
52	50 51	rplogcld	$⊢ p \in ℤ_{\geq 2} \to \log p \in ℝ^{+}$
53	23 49 52	3syl	$⊢ ((φ \land (p \in ℙ \land k \in ℕ)) \land p \in [0, A]) \to \log p \in ℝ^{+}$
54	31 48 53	lemuldivd	$⊢ ((φ \land (p \in ℙ \land k \in ℕ)) \land p \in [0, A]) \to (k \log p \leq \log A \leftrightarrow k \leq \frac{\log A}{\log p})$
55	48 53	rerpdivcld	$⊢ ((φ \land (p \in ℙ \land k \in ℕ)) \land p \in [0, A]) \to \frac{\log A}{\log p} \in ℝ$
56		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}⌋)$
57	55 27 56	syl2anc	$⊢ ((φ \land (p \in ℙ \land k \in ℕ)) \land p \in [0, A]) \to (k \leq \frac{\log A}{\log p} \leftrightarrow k \leq ⌊\frac{\log A}{\log p}⌋)$
58	30 54 57	3bitrd	$⊢ ((φ \land (p \in ℙ \land k \in ℕ)) \land p \in [0, A]) \to (\log p^{k} \leq \log A \leftrightarrow k \leq ⌊\frac{\log A}{\log p}⌋)$
59	19	adantr	$⊢ ((φ \land (p \in ℙ \land k \in ℕ)) \land p \in [0, A]) \to p^{k} \in ℕ$
60	59	nnrpd	$⊢ ((φ \land (p \in ℙ \land k \in ℕ)) \land p \in [0, A]) \to p^{k} \in ℝ^{+}$
61	60 47	logled	$⊢ ((φ \land (p \in ℙ \land k \in ℕ)) \land p \in [0, A]) \to (p^{k} \leq A \leftrightarrow \log p^{k} \leq \log A)$
62		simprr	$⊢ (φ \land (p \in ℙ \land k \in ℕ)) \to k \in ℕ$
63		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
64	62 63	eleqtrdi	$⊢ (φ \land (p \in ℙ \land k \in ℕ)) \to k \in ℤ_{\geq 1}$
65	64	adantr	$⊢ ((φ \land (p \in ℙ \land k \in ℕ)) \land p \in [0, A]) \to k \in ℤ_{\geq 1}$
66	55	flcld	$⊢ ((φ \land (p \in ℙ \land k \in ℕ)) \land p \in [0, A]) \to ⌊\frac{\log A}{\log p}⌋ \in ℤ$
67		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}⌋)$
68	65 66 67	syl2anc	$⊢ ((φ \land (p \in ℙ \land k \in ℕ)) \land p \in [0, A]) \to (k \in (1 \dots ⌊\frac{\log A}{\log p}⌋) \leftrightarrow k \leq ⌊\frac{\log A}{\log p}⌋)$
69	58 61 68	3bitr4d	$⊢ ((φ \land (p \in ℙ \land k \in ℕ)) \land p \in [0, A]) \to (p^{k} \leq A \leftrightarrow k \in (1 \dots ⌊\frac{\log A}{\log p}⌋))$
70	69	pm5.32da	$⊢ (φ \land (p \in ℙ \land k \in ℕ)) \to ((p \in [0, A] \land p^{k} \leq A) \leftrightarrow (p \in [0, A] \land k \in (1 \dots ⌊\frac{\log A}{\log p}⌋)))$
71	16	nncnd	$⊢ (φ \land (p \in ℙ \land k \in ℕ)) \to p \in ℂ$
72	71	exp1d	$⊢ (φ \land (p \in ℙ \land k \in ℕ)) \to p^{1} = p$
73	16	nnge1d	$⊢ (φ \land (p \in ℙ \land k \in ℕ)) \to 1 \leq p$
74	34 73 64	leexp2ad	$⊢ (φ \land (p \in ℙ \land k \in ℕ)) \to p^{1} \leq p^{k}$
75	72 74	eqbrtrrd	$⊢ (φ \land (p \in ℙ \land k \in ℕ)) \to p \leq p^{k}$
76	19	nnred	$⊢ (φ \land (p \in ℙ \land k \in ℕ)) \to p^{k} \in ℝ$
77		letr	$⊢ (p \in ℝ \land p^{k} \in ℝ \land A \in ℝ) \to ((p \leq p^{k} \land p^{k} \leq A) \to p \leq A)$
78	34 76 14 77	syl3anc	$⊢ (φ \land (p \in ℙ \land k \in ℕ)) \to ((p \leq p^{k} \land p^{k} \leq A) \to p \leq A)$
79	75 78	mpand	$⊢ (φ \land (p \in ℙ \land k \in ℕ)) \to (p^{k} \leq A \to p \leq A)$
80	79 44	sylibrd	$⊢ (φ \land (p \in ℙ \land k \in ℕ)) \to (p^{k} \leq A \to p \in [0, A])$
81	80	pm4.71rd	$⊢ (φ \land (p \in ℙ \land k \in ℕ)) \to (p^{k} \leq A \leftrightarrow (p \in [0, A] \land p^{k} \leq A))$
82		elin	$⊢ p \in ([0, A] \cap ℙ) \leftrightarrow (p \in [0, A] \land p \in ℙ)$
83	82	rbaib	$⊢ p \in ℙ \to (p \in ([0, A] \cap ℙ) \leftrightarrow p \in [0, A])$
84	83	ad2antrl	$⊢ (φ \land (p \in ℙ \land k \in ℕ)) \to (p \in ([0, A] \cap ℙ) \leftrightarrow p \in [0, A])$
85	84	anbi1d	$⊢ (φ \land (p \in ℙ \land k \in ℕ)) \to ((p \in ([0, A] \cap ℙ) \land k \in (1 \dots ⌊\frac{\log A}{\log p}⌋)) \leftrightarrow (p \in [0, A] \land k \in (1 \dots ⌊\frac{\log A}{\log p}⌋)))$
86	70 81 85	3bitr4rd	$⊢ (φ \land (p \in ℙ \land k \in ℕ)) \to ((p \in ([0, A] \cap ℙ) \land k \in (1 \dots ⌊\frac{\log A}{\log p}⌋)) \leftrightarrow p^{k} \leq A)$
87	19 63	eleqtrdi	$⊢ (φ \land (p \in ℙ \land k \in ℕ)) \to p^{k} \in ℤ_{\geq 1}$
88	14	flcld	$⊢ (φ \land (p \in ℙ \land k \in ℕ)) \to ⌊A⌋ \in ℤ$
89		elfz5	$⊢ (p^{k} \in ℤ_{\geq 1} \land ⌊A⌋ \in ℤ) \to (p^{k} \in (1 \dots ⌊A⌋) \leftrightarrow p^{k} \leq ⌊A⌋)$
90	87 88 89	syl2anc	$⊢ (φ \land (p \in ℙ \land k \in ℕ)) \to (p^{k} \in (1 \dots ⌊A⌋) \leftrightarrow p^{k} \leq ⌊A⌋)$
91	22 86 90	3bitr4d	$⊢ (φ \land (p \in ℙ \land k \in ℕ)) \to ((p \in ([0, A] \cap ℙ) \land k \in (1 \dots ⌊\frac{\log A}{\log p}⌋)) \leftrightarrow p^{k} \in (1 \dots ⌊A⌋))$
92	91	pm5.32da	$⊢ φ \to (((p \in ℙ \land k \in ℕ) \land (p \in ([0, A] \cap ℙ) \land k \in (1 \dots ⌊\frac{\log A}{\log p}⌋))) \leftrightarrow ((p \in ℙ \land k \in ℕ) \land p^{k} \in (1 \dots ⌊A⌋)))$
93	13 92	syl5bb	$⊢ φ \to ((p \in ([0, A] \cap ℙ) \land k \in (1 \dots ⌊\frac{\log A}{\log p}⌋)) \leftrightarrow ((p \in ℙ \land k \in ℕ) \land p^{k} \in (1 \dots ⌊A⌋)))$
94	1 5 7 9 93 3 4	fsumvma	$⊢ φ \to \sum_{x = 1}^{⌊A⌋} B = \sum_{p \in [0, A] \cap ℙ} \sum_{k = 1}^{⌊\frac{\log A}{\log p}⌋} C$

Metamath Proof Explorer

Theorem fsumvma2

Proof