Theorem hgt750lemd

Description: An upper bound to the summatory function of the von Mangoldt function on non-primes. (Contributed by Thierry Arnoux, 29-Dec-2021)

	Ref	Expression
Hypotheses	hgt750lemc.n	$$⊢\phi \to N\in \mathbb{N}$$
	hgt750lemd.0	$$⊢\phi \to {10}^{27}\le N$$
Assertion	hgt750lemd	$$⊢\phi \to \sum _{i\in \left(\left(1\dots N\right)\setminus \mathbb{P}\right)\cup \left\{2\right\}}\Lambda \left(i\right)<\mathrm{1<mi\; href="df-dp.html">.</mi>4263}\sqrt{N}$$

Proof

Step	Hyp	Ref	Expression
1		hgt750lemc.n	$$⊢\phi \to N\in \mathbb{N}$$
2		hgt750lemd.0	$$⊢\phi \to {10}^{27}\le N$$
3		fzfid	$$⊢\phi \to \left(1\dots N\right)\in \mathrm{Fin}$$
4		diffi	$$⊢\left(1\dots N\right)\in \mathrm{Fin}\to \left(1\dots N\right)\setminus \mathbb{P}\in \mathrm{Fin}$$
5	3 4	syl	$$⊢\phi \to \left(1\dots N\right)\setminus \mathbb{P}\in \mathrm{Fin}$$
6		vmaf	$$⊢\Lambda :\mathbb{N}⟶ℝ$$
7	6	a1i	$$⊢\left(\phi \wedge i\in \left(\left(1\dots N\right)\setminus \mathbb{P}\right)\right)\to \Lambda :\mathbb{N}⟶ℝ$$
8		fz1ssnn	$$⊢\left(1\dots N\right)\subseteq \mathbb{N}$$
9	8	a1i	$$⊢\phi \to \left(1\dots N\right)\subseteq \mathbb{N}$$
10	9	ssdifssd	$$⊢\phi \to \left(1\dots N\right)\setminus \mathbb{P}\subseteq \mathbb{N}$$
11	10	sselda	$$⊢\left(\phi \wedge i\in \left(\left(1\dots N\right)\setminus \mathbb{P}\right)\right)\to i\in \mathbb{N}$$
12	7 11	ffvelrnd	$$⊢\left(\phi \wedge i\in \left(\left(1\dots N\right)\setminus \mathbb{P}\right)\right)\to \Lambda \left(i\right)\in ℝ$$
13	5 12	fsumrecl	$$⊢\phi \to \sum _{i\in \left(1\dots N\right)\setminus \mathbb{P}}\Lambda \left(i\right)\in ℝ$$
14		2rp	$$⊢2\in {ℝ}^{+}$$
15	14	a1i	$$⊢\phi \to 2\in {ℝ}^{+}$$
16	15	relogcld	$$⊢\phi \to \log 2\in ℝ$$
17		1nn0	$$⊢1\in {\mathbb{N}}_0$$
18		4re	$$⊢4\in ℝ$$
19		2re	$$⊢2\in ℝ$$
20		6re	$$⊢6\in ℝ$$
21	20 19	pm3.2i	$$⊢\left(6\in ℝ\wedge 2\in ℝ\right)$$
22		dp2cl	$$⊢\left(6\in ℝ\wedge 2\in ℝ\right)\to 62\in ℝ$$
23	21 22	ax-mp	$$⊢62\in ℝ$$
24	19 23	pm3.2i	$$⊢\left(2\in ℝ\wedge 62\in ℝ\right)$$
25		dp2cl	$$⊢\left(2\in ℝ\wedge 62\in ℝ\right)\to 262\in ℝ$$
26	24 25	ax-mp	$$⊢262\in ℝ$$
27	18 26	pm3.2i	$$⊢\left(4\in ℝ\wedge 262\in ℝ\right)$$
28		dp2cl	$$⊢\left(4\in ℝ\wedge 262\in ℝ\right)\to 4262\in ℝ$$
29	27 28	ax-mp	$$⊢4262\in ℝ$$
30		dpcl	$$⊢\left(1\in {\mathbb{N}}_0\wedge 4262\in ℝ\right)\to \mathrm{1<mi\; href="df-dp.html">.</mi>4262}\in ℝ$$
31	17 29 30	mp2an	$$⊢\mathrm{1<mi\; href="df-dp.html">.</mi>4262}\in ℝ$$
32	31	a1i	$$⊢\phi \to \mathrm{1<mi\; href="df-dp.html">.</mi>4262}\in ℝ$$
33	1	nnred	$$⊢\phi \to N\in ℝ$$
34	1	nnrpd	$$⊢\phi \to N\in {ℝ}^{+}$$
35	34	rpge0d	$$⊢\phi \to 0\le N$$
36	33 35	resqrtcld	$$⊢\phi \to \sqrt{N}\in ℝ$$
37	32 36	remulcld	$$⊢\phi \to \mathrm{1<mi\; href="df-dp.html">.</mi>4262}\sqrt{N}\in ℝ$$
38		0nn0	$$⊢0\in {\mathbb{N}}_0$$
39		0re	$$⊢0\in ℝ$$
40		1re	$$⊢1\in ℝ$$
41	39 40	pm3.2i	$$⊢\left(0\in ℝ\wedge 1\in ℝ\right)$$
42		dp2cl	$$⊢\left(0\in ℝ\wedge 1\in ℝ\right)\to 01\in ℝ$$
43	41 42	ax-mp	$$⊢01\in ℝ$$
44	39 43	pm3.2i	$$⊢\left(0\in ℝ\wedge 01\in ℝ\right)$$
45		dp2cl	$$⊢\left(0\in ℝ\wedge 01\in ℝ\right)\to 001\in ℝ$$
46	44 45	ax-mp	$$⊢001\in ℝ$$
47	39 46	pm3.2i	$$⊢\left(0\in ℝ\wedge 001\in ℝ\right)$$
48		dp2cl	$$⊢\left(0\in ℝ\wedge 001\in ℝ\right)\to 0001\in ℝ$$
49	47 48	ax-mp	$$⊢0001\in ℝ$$
50		dpcl	$$⊢\left(0\in {\mathbb{N}}_0\wedge 0001\in ℝ\right)\to \mathrm{0<mi\; href="df-dp.html">.</mi>0001}\in ℝ$$
51	38 49 50	mp2an	$$⊢\mathrm{0<mi\; href="df-dp.html">.</mi>0001}\in ℝ$$
52	51	a1i	$$⊢\phi \to \mathrm{0<mi\; href="df-dp.html">.</mi>0001}\in ℝ$$
53	52 36	remulcld	$$⊢\phi \to \mathrm{0<mi\; href="df-dp.html">.</mi>0001}\sqrt{N}\in ℝ$$
54	1	nnzd	$$⊢\phi \to N\in \mathbb{Z}$$
55		chpvalz	$$⊢N\in \mathbb{Z}\to \psi \left(N\right)=\sum _{i=1}^N\Lambda \left(i\right)$$
56	54 55	syl	$$⊢\phi \to \psi \left(N\right)=\sum _{i=1}^N\Lambda \left(i\right)$$
57		chtvalz	$$⊢N\in \mathbb{Z}\to \theta \left(N\right)=\sum _{i\in \left(1\dots N\right)\cap \mathbb{P}}\log i$$
58	54 57	syl	$$⊢\phi \to \theta \left(N\right)=\sum _{i\in \left(1\dots N\right)\cap \mathbb{P}}\log i$$
59		inss2	$$⊢\left(1\dots N\right)\cap \mathbb{P}\subseteq \mathbb{P}$$
60	59	a1i	$$⊢\phi \to \left(1\dots N\right)\cap \mathbb{P}\subseteq \mathbb{P}$$
61	60	sselda	$$⊢\left(\phi \wedge i\in \left(\left(1\dots N\right)\cap \mathbb{P}\right)\right)\to i\in \mathbb{P}$$
62		vmaprm	$$⊢i\in \mathbb{P}\to \Lambda \left(i\right)=\log i$$
63	61 62	syl	$$⊢\left(\phi \wedge i\in \left(\left(1\dots N\right)\cap \mathbb{P}\right)\right)\to \Lambda \left(i\right)=\log i$$
64	63	sumeq2dv	$$⊢\phi \to \sum _{i\in \left(1\dots N\right)\cap \mathbb{P}}\Lambda \left(i\right)=\sum _{i\in \left(1\dots N\right)\cap \mathbb{P}}\log i$$
65	58 64	eqtr4d	$$⊢\phi \to \theta \left(N\right)=\sum _{i\in \left(1\dots N\right)\cap \mathbb{P}}\Lambda \left(i\right)$$
66	56 65	oveq12d	$$⊢\phi \to \psi \left(N\right)-\theta \left(N\right)=\sum _{i=1}^N\Lambda \left(i\right)-\sum _{i\in \left(1\dots N\right)\cap \mathbb{P}}\Lambda \left(i\right)$$
67		infi	$$⊢\left(1\dots N\right)\in \mathrm{Fin}\to \left(1\dots N\right)\cap \mathbb{P}\in \mathrm{Fin}$$
68	3 67	syl	$$⊢\phi \to \left(1\dots N\right)\cap \mathbb{P}\in \mathrm{Fin}$$
69	6	a1i	$$⊢\left(\phi \wedge i\in \left(\left(1\dots N\right)\cap \mathbb{P}\right)\right)\to \Lambda :\mathbb{N}⟶ℝ$$
70		inss1	$$⊢\left(1\dots N\right)\cap \mathbb{P}\subseteq \left(1\dots N\right)$$
71	70 8	sstri	$$⊢\left(1\dots N\right)\cap \mathbb{P}\subseteq \mathbb{N}$$
72	71	a1i	$$⊢\phi \to \left(1\dots N\right)\cap \mathbb{P}\subseteq \mathbb{N}$$
73	72	sselda	$$⊢\left(\phi \wedge i\in \left(\left(1\dots N\right)\cap \mathbb{P}\right)\right)\to i\in \mathbb{N}$$
74	69 73	ffvelrnd	$$⊢\left(\phi \wedge i\in \left(\left(1\dots N\right)\cap \mathbb{P}\right)\right)\to \Lambda \left(i\right)\in ℝ$$
75	74	recnd	$$⊢\left(\phi \wedge i\in \left(\left(1\dots N\right)\cap \mathbb{P}\right)\right)\to \Lambda \left(i\right)\in ℂ$$
76	68 75	fsumcl	$$⊢\phi \to \sum _{i\in \left(1\dots N\right)\cap \mathbb{P}}\Lambda \left(i\right)\in ℂ$$
77	12	recnd	$$⊢\left(\phi \wedge i\in \left(\left(1\dots N\right)\setminus \mathbb{P}\right)\right)\to \Lambda \left(i\right)\in ℂ$$
78	5 77	fsumcl	$$⊢\phi \to \sum _{i\in \left(1\dots N\right)\setminus \mathbb{P}}\Lambda \left(i\right)\in ℂ$$
79		inindif	$$⊢\left(\left(1\dots N\right)\cap \mathbb{P}\right)\cap \left(\left(1\dots N\right)\setminus \mathbb{P}\right)=\varnothing$$
80	79	a1i	$$⊢\phi \to \left(\left(1\dots N\right)\cap \mathbb{P}\right)\cap \left(\left(1\dots N\right)\setminus \mathbb{P}\right)=\varnothing$$
81		inundif	$$⊢\left(\left(1\dots N\right)\cap \mathbb{P}\right)\cup \left(\left(1\dots N\right)\setminus \mathbb{P}\right)=\left(1\dots N\right)$$
82	81	eqcomi	$$⊢\left(1\dots N\right)=\left(\left(1\dots N\right)\cap \mathbb{P}\right)\cup \left(\left(1\dots N\right)\setminus \mathbb{P}\right)$$
83	82	a1i	$$⊢\phi \to \left(1\dots N\right)=\left(\left(1\dots N\right)\cap \mathbb{P}\right)\cup \left(\left(1\dots N\right)\setminus \mathbb{P}\right)$$
84	6	a1i	$$⊢\left(\phi \wedge i\in \left(1\dots N\right)\right)\to \Lambda :\mathbb{N}⟶ℝ$$
85	9	sselda	$$⊢\left(\phi \wedge i\in \left(1\dots N\right)\right)\to i\in \mathbb{N}$$
86	84 85	ffvelrnd	$$⊢\left(\phi \wedge i\in \left(1\dots N\right)\right)\to \Lambda \left(i\right)\in ℝ$$
87	86	recnd	$$⊢\left(\phi \wedge i\in \left(1\dots N\right)\right)\to \Lambda \left(i\right)\in ℂ$$
88	80 83 3 87	fsumsplit	$$⊢\phi \to \sum _{i=1}^N\Lambda \left(i\right)=\sum _{i\in \left(1\dots N\right)\cap \mathbb{P}}\Lambda \left(i\right)+\sum _{i\in \left(1\dots N\right)\setminus \mathbb{P}}\Lambda \left(i\right)$$
89	76 78 88	mvrladdd	$$⊢\phi \to \sum _{i=1}^N\Lambda \left(i\right)-\sum _{i\in \left(1\dots N\right)\cap \mathbb{P}}\Lambda \left(i\right)=\sum _{i\in \left(1\dots N\right)\setminus \mathbb{P}}\Lambda \left(i\right)$$
90	66 89	eqtr2d	$$⊢\phi \to \sum _{i\in \left(1\dots N\right)\setminus \mathbb{P}}\Lambda \left(i\right)=\psi \left(N\right)-\theta \left(N\right)$$
91		fveq2	$$⊢x=N\to \psi \left(x\right)=\psi \left(N\right)$$
92		fveq2	$$⊢x=N\to \theta \left(x\right)=\theta \left(N\right)$$
93	91 92	oveq12d	$$⊢x=N\to \psi \left(x\right)-\theta \left(x\right)=\psi \left(N\right)-\theta \left(N\right)$$
94		fveq2	$$⊢x=N\to \sqrt{x}=\sqrt{N}$$
95	94	oveq2d	$$⊢x=N\to \mathrm{1<mi\; href="df-dp.html">.</mi>4262}\sqrt{x}=\mathrm{1<mi\; href="df-dp.html">.</mi>4262}\sqrt{N}$$
96	93 95	breq12d	$$⊢x=N\to \left(\psi \left(x\right)-\theta \left(x\right)<\mathrm{1<mi\; href="df-dp.html">.</mi>4262}\sqrt{x}\leftrightarrow \psi \left(N\right)-\theta \left(N\right)<\mathrm{1<mi\; href="df-dp.html">.</mi>4262}\sqrt{N}\right)$$
97		ax-ros336	$$⊢\forall x\in {ℝ}^{+}\psi \left(x\right)-\theta \left(x\right)<\mathrm{1<mi\; href="df-dp.html">.</mi>4262}\sqrt{x}$$
98	97	a1i	$$⊢\phi \to \forall x\in {ℝ}^{+}\psi \left(x\right)-\theta \left(x\right)<\mathrm{1<mi\; href="df-dp.html">.</mi>4262}\sqrt{x}$$
99	96 98 34	rspcdva	$$⊢\phi \to \psi \left(N\right)-\theta \left(N\right)<\mathrm{1<mi\; href="df-dp.html">.</mi>4262}\sqrt{N}$$
100	90 99	eqbrtrd	$$⊢\phi \to \sum _{i\in \left(1\dots N\right)\setminus \mathbb{P}}\Lambda \left(i\right)<\mathrm{1<mi\; href="df-dp.html">.</mi>4262}\sqrt{N}$$
101	40	a1i	$$⊢\phi \to 1\in ℝ$$
102		log2le1	$$⊢\log 2<1$$
103	102	a1i	$$⊢\phi \to \log 2<1$$
104		10nn0	$$⊢10\in {\mathbb{N}}_0$$
105		7nn0	$$⊢7\in {\mathbb{N}}_0$$
106	104 105	nn0expcli	$$⊢{10}^7\in {\mathbb{N}}_0$$
107	106	nn0rei	$$⊢{10}^7\in ℝ$$
108	107	a1i	$$⊢\phi \to {10}^7\in ℝ$$
109	52 108	remulcld	$$⊢\phi \to \mathrm{0<mi\; href="df-dp.html">.</mi>0001}{10}^7\in ℝ$$
110	104	nn0rei	$$⊢10\in ℝ$$
111		0z	$$⊢0\in \mathbb{Z}$$
112		3z	$$⊢3\in \mathbb{Z}$$
113	110 111 112	3pm3.2i	$$⊢\left(10\in ℝ\wedge 0\in \mathbb{Z}\wedge 3\in \mathbb{Z}\right)$$
114		1lt10	$$⊢1<10$$
115		3pos	$$⊢0<3$$
116	114 115	pm3.2i	$$⊢\left(1<10\wedge 0<3\right)$$
117		ltexp2a	$$⊢\left(\left(10\in ℝ\wedge 0\in \mathbb{Z}\wedge 3\in \mathbb{Z}\right)\wedge \left(1<10\wedge 0<3\right)\right)\to {10}^0<{10}^3$$
118	113 116 117	mp2an	$$⊢{10}^0<{10}^3$$
119	104	numexp0	$$⊢{10}^0=1$$
120	119	eqcomi	$$⊢1={10}^0$$
121	110	recni	$$⊢10\in ℂ$$
122		10pos	$$⊢0<10$$
123	39 122	gtneii	$$⊢10\ne 0$$
124		4z	$$⊢4\in \mathbb{Z}$$
125		expm1	$$⊢\left(10\in ℂ\wedge 10\ne 0\wedge 4\in \mathbb{Z}\right)\to {10}^{4-1}=\frac{{10}^4}{10}$$
126	121 123 124 125	mp3an	$$⊢{10}^{4-1}=\frac{{10}^4}{10}$$
127		4m1e3	$$⊢4-1=3$$
128	127	oveq2i	$$⊢{10}^{4-1}={10}^3$$
129		4nn0	$$⊢4\in {\mathbb{N}}_0$$
130	104 129	nn0expcli	$$⊢{10}^4\in {\mathbb{N}}_0$$
131	130	nn0cni	$$⊢{10}^4\in ℂ$$
132		divrec2	$$⊢\left({10}^4\in ℂ\wedge 10\in ℂ\wedge 10\ne 0\right)\to \frac{{10}^4}{10}=\left(\frac{1}{10}\right){10}^4$$
133	131 121 123 132	mp3an	$$⊢\frac{{10}^4}{10}=\left(\frac{1}{10}\right){10}^4$$
134	126 128 133	3eqtr3ri	$$⊢\left(\frac{1}{10}\right){10}^4={10}^3$$
135	118 120 134	3brtr4i	$$⊢1<\left(\frac{1}{10}\right){10}^4$$
136		1rp	$$⊢1\in {ℝ}^{+}$$
137	136	dp0h	$$⊢\mathrm{0<mi\; href="df-dp.html">.</mi>1}=\frac{1}{10}$$
138	137	oveq1i	$$⊢\mathrm{0<mi\; href="df-dp.html">.</mi>1}{10}^4=\left(\frac{1}{10}\right){10}^4$$
139	135 138	breqtrri	$$⊢1<\mathrm{0<mi\; href="df-dp.html">.</mi>1}{10}^4$$
140	139	a1i	$$⊢\phi \to 1<\mathrm{0<mi\; href="df-dp.html">.</mi>1}{10}^4$$
141		4p1e5	$$⊢4+1=5$$
142		5nn0	$$⊢5\in {\mathbb{N}}_0$$
143	142	nn0zi	$$⊢5\in \mathbb{Z}$$
144	38 136 141 124 143	dpexpp1	$$⊢\mathrm{0<mi\; href="df-dp.html">.</mi>1}{10}^4=\mathrm{0<mi\; href="df-dp.html">.</mi>01}{10}^5$$
145	38 136	rpdp2cl	$$⊢01\in {ℝ}^{+}$$
146		5p1e6	$$⊢5+1=6$$
147		6nn0	$$⊢6\in {\mathbb{N}}_0$$
148	147	nn0zi	$$⊢6\in \mathbb{Z}$$
149	38 145 146 143 148	dpexpp1	$$⊢\mathrm{0<mi\; href="df-dp.html">.</mi>01}{10}^5=\mathrm{0<mi\; href="df-dp.html">.</mi>001}{10}^6$$
150	38 145	rpdp2cl	$$⊢001\in {ℝ}^{+}$$
151		6p1e7	$$⊢6+1=7$$
152	105	nn0zi	$$⊢7\in \mathbb{Z}$$
153	38 150 151 148 152	dpexpp1	$$⊢\mathrm{0<mi\; href="df-dp.html">.</mi>001}{10}^6=\mathrm{0<mi\; href="df-dp.html">.</mi>0001}{10}^7$$
154	144 149 153	3eqtrri	$$⊢\mathrm{0<mi\; href="df-dp.html">.</mi>0001}{10}^7=\mathrm{0<mi\; href="df-dp.html">.</mi>1}{10}^4$$
155	140 154	breqtrrdi	$$⊢\phi \to 1<\mathrm{0<mi\; href="df-dp.html">.</mi>0001}{10}^7$$
156	38 150	rpdp2cl	$$⊢0001\in {ℝ}^{+}$$
157	38 156	rpdpcl	$$⊢\mathrm{0<mi\; href="df-dp.html">.</mi>0001}\in {ℝ}^{+}$$
158	157	a1i	$$⊢\phi \to \mathrm{0<mi\; href="df-dp.html">.</mi>0001}\in {ℝ}^{+}$$
159		2nn0	$$⊢2\in {\mathbb{N}}_0$$
160	159 105	deccl	$$⊢27\in {\mathbb{N}}_0$$
161	104 160	nn0expcli	$$⊢{10}^{27}\in {\mathbb{N}}_0$$
162	161	nn0rei	$$⊢{10}^{27}\in ℝ$$
163	162	a1i	$$⊢\phi \to {10}^{27}\in ℝ$$
164	161	nn0ge0i	$$⊢0\le {10}^{27}$$
165	164	a1i	$$⊢\phi \to 0\le {10}^{27}$$
166	163 165	resqrtcld	$$⊢\phi \to \sqrt{{10}^{27}}\in ℝ$$
167		expmul	$$⊢\left(10\in ℂ\wedge 7\in {\mathbb{N}}_0\wedge 2\in {\mathbb{N}}_0\right)\to {10}^{7\cdot 2}={\left({10}^7\right)}^2$$
168	121 105 159 167	mp3an	$$⊢{10}^{7\cdot 2}={\left({10}^7\right)}^2$$
169		7t2e14	$$⊢7\cdot 2=14$$
170	169	oveq2i	$$⊢{10}^{7\cdot 2}={10}^{14}$$
171	168 170	eqtr3i	$$⊢{\left({10}^7\right)}^2={10}^{14}$$
172	171	fveq2i	$$⊢\sqrt{{\left({10}^7\right)}^2}=\sqrt{{10}^{14}}$$
173		expgt0	$$⊢\left(10\in ℝ\wedge 7\in \mathbb{Z}\wedge 0<10\right)\to 0<{10}^7$$
174	110 152 122 173	mp3an	$$⊢0<{10}^7$$
175	39 107 174	ltleii	$$⊢0\le {10}^7$$
176		sqrtsq	$$⊢\left({10}^7\in ℝ\wedge 0\le {10}^7\right)\to \sqrt{{\left({10}^7\right)}^2}={10}^7$$
177	107 175 176	mp2an	$$⊢\sqrt{{\left({10}^7\right)}^2}={10}^7$$
178	172 177	eqtr3i	$$⊢\sqrt{{10}^{14}}={10}^7$$
179	17 129	deccl	$$⊢14\in {\mathbb{N}}_0$$
180	179	nn0zi	$$⊢14\in \mathbb{Z}$$
181	160	nn0zi	$$⊢27\in \mathbb{Z}$$
182	110 180 181	3pm3.2i	$$⊢\left(10\in ℝ\wedge 14\in \mathbb{Z}\wedge 27\in \mathbb{Z}\right)$$
183		4lt10	$$⊢4<10$$
184		1lt2	$$⊢1<2$$
185	17 159 129 105 183 184	decltc	$$⊢14<27$$
186	114 185	pm3.2i	$$⊢\left(1<10\wedge 14<27\right)$$
187		ltexp2a	$$⊢\left(\left(10\in ℝ\wedge 14\in \mathbb{Z}\wedge 27\in \mathbb{Z}\right)\wedge \left(1<10\wedge 14<27\right)\right)\to {10}^{14}<{10}^{27}$$
188	182 186 187	mp2an	$$⊢{10}^{14}<{10}^{27}$$
189	104 179	nn0expcli	$$⊢{10}^{14}\in {\mathbb{N}}_0$$
190	189	nn0rei	$$⊢{10}^{14}\in ℝ$$
191		expgt0	$$⊢\left(10\in ℝ\wedge 14\in \mathbb{Z}\wedge 0<10\right)\to 0<{10}^{14}$$
192	110 180 122 191	mp3an	$$⊢0<{10}^{14}$$
193	39 190 192	ltleii	$$⊢0\le {10}^{14}$$
194	190 193	pm3.2i	$$⊢\left({10}^{14}\in ℝ\wedge 0\le {10}^{14}\right)$$
195	162 164	pm3.2i	$$⊢\left({10}^{27}\in ℝ\wedge 0\le {10}^{27}\right)$$
196		sqrtlt	$$⊢\left(\left({10}^{14}\in ℝ\wedge 0\le {10}^{14}\right)\wedge \left({10}^{27}\in ℝ\wedge 0\le {10}^{27}\right)\right)\to \left({10}^{14}<{10}^{27}\leftrightarrow \sqrt{{10}^{14}}<\sqrt{{10}^{27}}\right)$$
197	194 195 196	mp2an	$$⊢{10}^{14}<{10}^{27}\leftrightarrow \sqrt{{10}^{14}}<\sqrt{{10}^{27}}$$
198	188 197	mpbi	$$⊢\sqrt{{10}^{14}}<\sqrt{{10}^{27}}$$
199	178 198	eqbrtrri	$$⊢{10}^7<\sqrt{{10}^{27}}$$
200	199	a1i	$$⊢\phi \to {10}^7<\sqrt{{10}^{27}}$$
201	163 165 33 35	sqrtled	$$⊢\phi \to \left({10}^{27}\le N\leftrightarrow \sqrt{{10}^{27}}\le \sqrt{N}\right)$$
202	2 201	mpbid	$$⊢\phi \to \sqrt{{10}^{27}}\le \sqrt{N}$$
203	108 166 36 200 202	ltletrd	$$⊢\phi \to {10}^7<\sqrt{N}$$
204	108 36 158 203	ltmul2dd	$$⊢\phi \to \mathrm{0<mi\; href="df-dp.html">.</mi>0001}{10}^7<\mathrm{0<mi\; href="df-dp.html">.</mi>0001}\sqrt{N}$$
205	101 109 53 155 204	lttrd	$$⊢\phi \to 1<\mathrm{0<mi\; href="df-dp.html">.</mi>0001}\sqrt{N}$$
206	16 101 53 103 205	lttrd	$$⊢\phi \to \log 2<\mathrm{0<mi\; href="df-dp.html">.</mi>0001}\sqrt{N}$$
207	13 16 37 53 100 206	lt2addd	$$⊢\phi \to \sum _{i\in \left(1\dots N\right)\setminus \mathbb{P}}\Lambda \left(i\right)+\log 2<\mathrm{1<mi\; href="df-dp.html">.</mi>4262}\sqrt{N}+\mathrm{0<mi\; href="df-dp.html">.</mi>0001}\sqrt{N}$$
208		nfv	$$⊢Ⅎi\phi$$
209		nfcv	$$⊢\underset{\_}{Ⅎ}i\log 2$$
210		2prm	$$⊢2\in \mathbb{P}$$
211	210	a1i	$$⊢\phi \to 2\in \mathbb{P}$$
212		elndif	$$⊢2\in \mathbb{P}\to \neg 2\in \left(\left(1\dots N\right)\setminus \mathbb{P}\right)$$
213	211 212	syl	$$⊢\phi \to \neg 2\in \left(\left(1\dots N\right)\setminus \mathbb{P}\right)$$
214		fveq2	$$⊢i=2\to \Lambda \left(i\right)=\Lambda \left(2\right)$$
215		vmaprm	$$⊢2\in \mathbb{P}\to \Lambda \left(2\right)=\log 2$$
216	210 215	ax-mp	$$⊢\Lambda \left(2\right)=\log 2$$
217	214 216	eqtrdi	$$⊢i=2\to \Lambda \left(i\right)=\log 2$$
218		2cnd	$$⊢\phi \to 2\in ℂ$$
219		2ne0	$$⊢2\ne 0$$
220	219	a1i	$$⊢\phi \to 2\ne 0$$
221	218 220	logcld	$$⊢\phi \to \log 2\in ℂ$$
222	208 209 5 211 213 77 217 221	fsumsplitsn	$$⊢\phi \to \sum _{i\in \left(\left(1\dots N\right)\setminus \mathbb{P}\right)\cup \left\{2\right\}}\Lambda \left(i\right)=\sum _{i\in \left(1\dots N\right)\setminus \mathbb{P}}\Lambda \left(i\right)+\log 2$$
223	147 14	rpdp2cl	$$⊢62\in {ℝ}^{+}$$
224	159 223	rpdp2cl	$$⊢262\in {ℝ}^{+}$$
225		3rp	$$⊢3\in {ℝ}^{+}$$
226	147 225	rpdp2cl	$$⊢63\in {ℝ}^{+}$$
227	159 226	rpdp2cl	$$⊢263\in {ℝ}^{+}$$
228		1p0e1	$$⊢1+0=1$$
229		4cn	$$⊢4\in ℂ$$
230	229	addid1i	$$⊢4+0=4$$
231		2cn	$$⊢2\in ℂ$$
232	231	addid1i	$$⊢2+0=2$$
233		3nn0	$$⊢3\in {\mathbb{N}}_0$$
234		eqid	$$⊢62=62$$
235		eqid	$$⊢01=01$$
236		6cn	$$⊢6\in ℂ$$
237	236	addid1i	$$⊢6+0=6$$
238		2p1e3	$$⊢2+1=3$$
239	147 159 38 17 234 235 237 238	decadd	$$⊢62+01=63$$
240	147 159 38 17 147 233 239	dpadd	$$⊢\mathrm{6<mi\; href="df-dp.html">.</mi>2}+\mathrm{0<mi\; href="df-dp.html">.</mi>1}=\mathrm{6<mi\; href="df-dp.html">.</mi>3}$$
241	147 14 38 136 147 225 159 38 232 240	dpadd2	$$⊢\mathrm{2<mi\; href="df-dp.html">.</mi>62}+\mathrm{0<mi\; href="df-dp.html">.</mi>01}=\mathrm{2<mi\; href="df-dp.html">.</mi>63}$$
242	159 223 38 145 159 226 129 38 230 241	dpadd2	$$⊢\mathrm{4<mi\; href="df-dp.html">.</mi>262}+\mathrm{0<mi\; href="df-dp.html">.</mi>001}=\mathrm{4<mi\; href="df-dp.html">.</mi>263}$$
243	129 224 38 150 129 227 17 38 228 242	dpadd2	$$⊢\mathrm{1<mi\; href="df-dp.html">.</mi>4262}+\mathrm{0<mi\; href="df-dp.html">.</mi>0001}=\mathrm{1<mi\; href="df-dp.html">.</mi>4263}$$
244	243	oveq1i	$$⊢\left(\mathrm{1<mi\; href="df-dp.html">.</mi>4262}+\mathrm{0<mi\; href="df-dp.html">.</mi>0001}\right)\sqrt{N}=\mathrm{1<mi\; href="df-dp.html">.</mi>4263}\sqrt{N}$$
245	32	recnd	$$⊢\phi \to \mathrm{1<mi\; href="df-dp.html">.</mi>4262}\in ℂ$$
246	52	recnd	$$⊢\phi \to \mathrm{0<mi\; href="df-dp.html">.</mi>0001}\in ℂ$$
247	36	recnd	$$⊢\phi \to \sqrt{N}\in ℂ$$
248	245 246 247	adddird	$$⊢\phi \to \left(\mathrm{1<mi\; href="df-dp.html">.</mi>4262}+\mathrm{0<mi\; href="df-dp.html">.</mi>0001}\right)\sqrt{N}=\mathrm{1<mi\; href="df-dp.html">.</mi>4262}\sqrt{N}+\mathrm{0<mi\; href="df-dp.html">.</mi>0001}\sqrt{N}$$
249	244 248	eqtr3id	$$⊢\phi \to \mathrm{1<mi\; href="df-dp.html">.</mi>4263}\sqrt{N}=\mathrm{1<mi\; href="df-dp.html">.</mi>4262}\sqrt{N}+\mathrm{0<mi\; href="df-dp.html">.</mi>0001}\sqrt{N}$$
250	207 222 249	3brtr4d	$$⊢\phi \to \sum _{i\in \left(\left(1\dots N\right)\setminus \mathbb{P}\right)\cup \left\{2\right\}}\Lambda \left(i\right)<\mathrm{1<mi\; href="df-dp.html">.</mi>4263}\sqrt{N}$$