hgt750leme

Description: An upper bound on the contribution of the non-prime terms in the Statement 7.50 of Helfgott p. 69. (Contributed by Thierry Arnoux, 29-Dec-2021)

	Ref	Expression
Hypotheses	hgt750leme.o	$⊢ O = \{z \in ℤ \| \neg 2 ∥ z\}$
	hgt750leme.n	$⊢ φ \to N \in ℕ$
	hgt750leme.0	$⊢ φ \to 10^{27} \leq N$
	hgt750leme.h	$⊢ φ \to H : ℕ ⟶ [0, +∞)$
	hgt750leme.k	$⊢ φ \to K : ℕ ⟶ [0, +∞)$
	hgt750leme.1	$⊢ (φ \land m \in ℕ) \to K (m) \leq 1.079955$
	hgt750leme.2	$⊢ (φ \land m \in ℕ) \to H (m) \leq 1.414$
Assertion	hgt750leme	$⊢ φ \to \sum_{n \in (ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N)} Λ (n (0)) H (n (0)) Λ (n (1)) K (n (1)) Λ (n (2)) K (n (2)) \leq 7.348 (\frac{\log N}{\sqrt{N}}) N^{2}$

Proof

Step	Hyp	Ref	Expression
1		hgt750leme.o	$⊢ O = \{z \in ℤ \| \neg 2 ∥ z\}$
2		hgt750leme.n	$⊢ φ \to N \in ℕ$
3		hgt750leme.0	$⊢ φ \to 10^{27} \leq N$
4		hgt750leme.h	$⊢ φ \to H : ℕ ⟶ [0, +∞)$
5		hgt750leme.k	$⊢ φ \to K : ℕ ⟶ [0, +∞)$
6		hgt750leme.1	$⊢ (φ \land m \in ℕ) \to K (m) \leq 1.079955$
7		hgt750leme.2	$⊢ (φ \land m \in ℕ) \to H (m) \leq 1.414$
8	2	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
9		3nn0	$⊢ 3 \in ℕ_{0}$
10	9	a1i	$⊢ φ \to 3 \in ℕ_{0}$
11		ssidd	$⊢ φ \to ℕ \subseteq ℕ$
12	8 10 11	reprfi2	$⊢ φ \to ℕ repr (3) N \in Fin$
13		diffi	$⊢ ℕ repr (3) N \in Fin \to (ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N) \in Fin$
14	12 13	syl	$⊢ φ \to (ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N) \in Fin$
15		vmaf	$⊢ Λ : ℕ ⟶ ℝ$
16	15	a1i	$⊢ (φ \land n \in ((ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N))) \to Λ : ℕ ⟶ ℝ$
17		ssidd	$⊢ (φ \land n \in ((ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N))) \to ℕ \subseteq ℕ$
18	2	nnzd	$⊢ φ \to N \in ℤ$
19	18	adantr	$⊢ (φ \land n \in ((ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N))) \to N \in ℤ$
20	9	a1i	$⊢ (φ \land n \in ((ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N))) \to 3 \in ℕ_{0}$
21		simpr	$⊢ (φ \land n \in ((ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N))) \to n \in ((ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N))$
22	21	eldifad	$⊢ (φ \land n \in ((ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N))) \to n \in (ℕ repr (3) N)$
23	17 19 20 22	reprf	$⊢ (φ \land n \in ((ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N))) \to n : (0 ..^3) ⟶ ℕ$
24		c0ex	$⊢ 0 \in V$
25	24	tpid1	$⊢ 0 \in \{0, 1, 2\}$
26		fzo0to3tp	$⊢ (0 ..^3) = \{0, 1, 2\}$
27	25 26	eleqtrri	$⊢ 0 \in (0 ..^3)$
28	27	a1i	$⊢ (φ \land n \in ((ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N))) \to 0 \in (0 ..^3)$
29	23 28	ffvelrnd	$⊢ (φ \land n \in ((ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N))) \to n (0) \in ℕ$
30	16 29	ffvelrnd	$⊢ (φ \land n \in ((ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N))) \to Λ (n (0)) \in ℝ$
31		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
32	4	adantr	$⊢ (φ \land n \in ((ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N))) \to H : ℕ ⟶ [0, +∞)$
33	32 29	ffvelrnd	$⊢ (φ \land n \in ((ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N))) \to H (n (0)) \in [0, +∞)$
34	31 33	sseldi	$⊢ (φ \land n \in ((ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N))) \to H (n (0)) \in ℝ$
35	30 34	remulcld	$⊢ (φ \land n \in ((ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N))) \to Λ (n (0)) H (n (0)) \in ℝ$
36		1ex	$⊢ 1 \in V$
37	36	tpid2	$⊢ 1 \in \{0, 1, 2\}$
38	37 26	eleqtrri	$⊢ 1 \in (0 ..^3)$
39	38	a1i	$⊢ (φ \land n \in ((ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N))) \to 1 \in (0 ..^3)$
40	23 39	ffvelrnd	$⊢ (φ \land n \in ((ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N))) \to n (1) \in ℕ$
41	16 40	ffvelrnd	$⊢ (φ \land n \in ((ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N))) \to Λ (n (1)) \in ℝ$
42	5	adantr	$⊢ (φ \land n \in ((ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N))) \to K : ℕ ⟶ [0, +∞)$
43	42 40	ffvelrnd	$⊢ (φ \land n \in ((ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N))) \to K (n (1)) \in [0, +∞)$
44	31 43	sseldi	$⊢ (φ \land n \in ((ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N))) \to K (n (1)) \in ℝ$
45	41 44	remulcld	$⊢ (φ \land n \in ((ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N))) \to Λ (n (1)) K (n (1)) \in ℝ$
46		2ex	$⊢ 2 \in V$
47	46	tpid3	$⊢ 2 \in \{0, 1, 2\}$
48	47 26	eleqtrri	$⊢ 2 \in (0 ..^3)$
49	48	a1i	$⊢ (φ \land n \in ((ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N))) \to 2 \in (0 ..^3)$
50	23 49	ffvelrnd	$⊢ (φ \land n \in ((ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N))) \to n (2) \in ℕ$
51	16 50	ffvelrnd	$⊢ (φ \land n \in ((ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N))) \to Λ (n (2)) \in ℝ$
52	42 50	ffvelrnd	$⊢ (φ \land n \in ((ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N))) \to K (n (2)) \in [0, +∞)$
53	31 52	sseldi	$⊢ (φ \land n \in ((ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N))) \to K (n (2)) \in ℝ$
54	51 53	remulcld	$⊢ (φ \land n \in ((ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N))) \to Λ (n (2)) K (n (2)) \in ℝ$
55	45 54	remulcld	$⊢ (φ \land n \in ((ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N))) \to Λ (n (1)) K (n (1)) Λ (n (2)) K (n (2)) \in ℝ$
56	35 55	remulcld	$⊢ (φ \land n \in ((ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N))) \to Λ (n (0)) H (n (0)) Λ (n (1)) K (n (1)) Λ (n (2)) K (n (2)) \in ℝ$
57	14 56	fsumrecl	$⊢ φ \to \sum_{n \in (ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N)} Λ (n (0)) H (n (0)) Λ (n (1)) K (n (1)) Λ (n (2)) K (n (2)) \in ℝ$
58		3re	$⊢ 3 \in ℝ$
59	58	a1i	$⊢ φ \to 3 \in ℝ$
60		1nn0	$⊢ 1 \in ℕ_{0}$
61		0nn0	$⊢ 0 \in ℕ_{0}$
62		7nn0	$⊢ 7 \in ℕ_{0}$
63		9nn0	$⊢ 9 \in ℕ_{0}$
64		5nn0	$⊢ 5 \in ℕ_{0}$
65		5nn	$⊢ 5 \in ℕ$
66		nnrp	$⊢ 5 \in ℕ \to 5 \in ℝ^{+}$
67	65 66	ax-mp	$⊢ 5 \in ℝ^{+}$
68	64 67	rpdp2cl	$⊢ 55 \in ℝ^{+}$
69	63 68	rpdp2cl	$⊢ 955 \in ℝ^{+}$
70	63 69	rpdp2cl	$⊢ 9955 \in ℝ^{+}$
71	62 70	rpdp2cl	$⊢ 79955 \in ℝ^{+}$
72	61 71	rpdp2cl	$⊢ 079955 \in ℝ^{+}$
73	60 72	rpdpcl	$⊢ 1.079955 \in ℝ^{+}$
74	73	a1i	$⊢ φ \to 1.079955 \in ℝ^{+}$
75	74	rpred	$⊢ φ \to 1.079955 \in ℝ$
76	75	resqcld	$⊢ φ \to {1.079955}^{2} \in ℝ$
77		4nn0	$⊢ 4 \in ℕ_{0}$
78		4nn	$⊢ 4 \in ℕ$
79		nnrp	$⊢ 4 \in ℕ \to 4 \in ℝ^{+}$
80	78 79	ax-mp	$⊢ 4 \in ℝ^{+}$
81	60 80	rpdp2cl	$⊢ 14 \in ℝ^{+}$
82	77 81	rpdp2cl	$⊢ 414 \in ℝ^{+}$
83	60 82	rpdpcl	$⊢ 1.414 \in ℝ^{+}$
84	83	a1i	$⊢ φ \to 1.414 \in ℝ^{+}$
85	84	rpred	$⊢ φ \to 1.414 \in ℝ$
86	76 85	remulcld	$⊢ φ \to {1.079955}^{2} \cdot 1.414 \in ℝ$
87		fveq1	$⊢ d = c \to d (0) = c (0)$
88	87	eleq1d	$⊢ d = c \to (d (0) \in (O \cap ℙ) \leftrightarrow c (0) \in (O \cap ℙ))$
89	88	notbid	$⊢ d = c \to (\neg d (0) \in (O \cap ℙ) \leftrightarrow \neg c (0) \in (O \cap ℙ))$
90	89	cbvrabv	$⊢ \{d \in (ℕ repr (3) N) \| \neg d (0) \in (O \cap ℙ)\} = \{c \in (ℕ repr (3) N) \| \neg c (0) \in (O \cap ℙ)\}$
91	90	ssrab3	$⊢ \{d \in (ℕ repr (3) N) \| \neg d (0) \in (O \cap ℙ)\} \subseteq ℕ repr (3) N$
92		ssfi	$⊢ (ℕ repr (3) N \in Fin \land \{d \in (ℕ repr (3) N) \| \neg d (0) \in (O \cap ℙ)\} \subseteq ℕ repr (3) N) \to \{d \in (ℕ repr (3) N) \| \neg d (0) \in (O \cap ℙ)\} \in Fin$
93	12 91 92	sylancl	$⊢ φ \to \{d \in (ℕ repr (3) N) \| \neg d (0) \in (O \cap ℙ)\} \in Fin$
94	15	a1i	$⊢ (φ \land n \in \{d \in (ℕ repr (3) N) \| \neg d (0) \in (O \cap ℙ)\}) \to Λ : ℕ ⟶ ℝ$
95		ssidd	$⊢ (φ \land n \in \{d \in (ℕ repr (3) N) \| \neg d (0) \in (O \cap ℙ)\}) \to ℕ \subseteq ℕ$
96	18	adantr	$⊢ (φ \land n \in \{d \in (ℕ repr (3) N) \| \neg d (0) \in (O \cap ℙ)\}) \to N \in ℤ$
97	9	a1i	$⊢ (φ \land n \in \{d \in (ℕ repr (3) N) \| \neg d (0) \in (O \cap ℙ)\}) \to 3 \in ℕ_{0}$
98	91	a1i	$⊢ φ \to \{d \in (ℕ repr (3) N) \| \neg d (0) \in (O \cap ℙ)\} \subseteq ℕ repr (3) N$
99	98	sselda	$⊢ (φ \land n \in \{d \in (ℕ repr (3) N) \| \neg d (0) \in (O \cap ℙ)\}) \to n \in (ℕ repr (3) N)$
100	95 96 97 99	reprf	$⊢ (φ \land n \in \{d \in (ℕ repr (3) N) \| \neg d (0) \in (O \cap ℙ)\}) \to n : (0 ..^3) ⟶ ℕ$
101	27	a1i	$⊢ (φ \land n \in \{d \in (ℕ repr (3) N) \| \neg d (0) \in (O \cap ℙ)\}) \to 0 \in (0 ..^3)$
102	100 101	ffvelrnd	$⊢ (φ \land n \in \{d \in (ℕ repr (3) N) \| \neg d (0) \in (O \cap ℙ)\}) \to n (0) \in ℕ$
103	94 102	ffvelrnd	$⊢ (φ \land n \in \{d \in (ℕ repr (3) N) \| \neg d (0) \in (O \cap ℙ)\}) \to Λ (n (0)) \in ℝ$
104	38	a1i	$⊢ (φ \land n \in \{d \in (ℕ repr (3) N) \| \neg d (0) \in (O \cap ℙ)\}) \to 1 \in (0 ..^3)$
105	100 104	ffvelrnd	$⊢ (φ \land n \in \{d \in (ℕ repr (3) N) \| \neg d (0) \in (O \cap ℙ)\}) \to n (1) \in ℕ$
106	94 105	ffvelrnd	$⊢ (φ \land n \in \{d \in (ℕ repr (3) N) \| \neg d (0) \in (O \cap ℙ)\}) \to Λ (n (1)) \in ℝ$
107	48	a1i	$⊢ (φ \land n \in \{d \in (ℕ repr (3) N) \| \neg d (0) \in (O \cap ℙ)\}) \to 2 \in (0 ..^3)$
108	100 107	ffvelrnd	$⊢ (φ \land n \in \{d \in (ℕ repr (3) N) \| \neg d (0) \in (O \cap ℙ)\}) \to n (2) \in ℕ$
109	94 108	ffvelrnd	$⊢ (φ \land n \in \{d \in (ℕ repr (3) N) \| \neg d (0) \in (O \cap ℙ)\}) \to Λ (n (2)) \in ℝ$
110	106 109	remulcld	$⊢ (φ \land n \in \{d \in (ℕ repr (3) N) \| \neg d (0) \in (O \cap ℙ)\}) \to Λ (n (1)) Λ (n (2)) \in ℝ$
111	103 110	remulcld	$⊢ (φ \land n \in \{d \in (ℕ repr (3) N) \| \neg d (0) \in (O \cap ℙ)\}) \to Λ (n (0)) Λ (n (1)) Λ (n (2)) \in ℝ$
112	93 111	fsumrecl	$⊢ φ \to \sum_{n \in \{d \in (ℕ repr (3) N) \| \neg d (0) \in (O \cap ℙ)\}} Λ (n (0)) Λ (n (1)) Λ (n (2)) \in ℝ$
113	86 112	remulcld	$⊢ φ \to {1.079955}^{2} \cdot 1.414 \sum_{n \in \{d \in (ℕ repr (3) N) \| \neg d (0) \in (O \cap ℙ)\}} Λ (n (0)) Λ (n (1)) Λ (n (2)) \in ℝ$
114	59 113	remulcld	$⊢ φ \to 3 {1.079955}^{2} \cdot 1.414 \sum_{n \in \{d \in (ℕ repr (3) N) \| \neg d (0) \in (O \cap ℙ)\}} Λ (n (0)) Λ (n (1)) Λ (n (2)) \in ℝ$
115		4re	$⊢ 4 \in ℝ$
116		8re	$⊢ 8 \in ℝ$
117	115 116	pm3.2i	$⊢ (4 \in ℝ \land 8 \in ℝ)$
118		dp2cl	$⊢ (4 \in ℝ \land 8 \in ℝ) \to 48 \in ℝ$
119	117 118	ax-mp	$⊢ 48 \in ℝ$
120	58 119	pm3.2i	$⊢ (3 \in ℝ \land 48 \in ℝ)$
121		dp2cl	$⊢ (3 \in ℝ \land 48 \in ℝ) \to 348 \in ℝ$
122	120 121	ax-mp	$⊢ 348 \in ℝ$
123		dpcl	$⊢ (7 \in ℕ_{0} \land 348 \in ℝ) \to 7.348 \in ℝ$
124	62 122 123	mp2an	$⊢ 7.348 \in ℝ$
125	124	a1i	$⊢ φ \to 7.348 \in ℝ$
126	2	nnrpd	$⊢ φ \to N \in ℝ^{+}$
127	126	relogcld	$⊢ φ \to \log N \in ℝ$
128	2	nnred	$⊢ φ \to N \in ℝ$
129	126	rpge0d	$⊢ φ \to 0 \leq N$
130	128 129	resqrtcld	$⊢ φ \to \sqrt{N} \in ℝ$
131	126	rpsqrtcld	$⊢ φ \to \sqrt{N} \in ℝ^{+}$
132	131	rpne0d	$⊢ φ \to \sqrt{N} \neq 0$
133	127 130 132	redivcld	$⊢ φ \to \frac{\log N}{\sqrt{N}} \in ℝ$
134	125 133	remulcld	$⊢ φ \to 7.348 (\frac{\log N}{\sqrt{N}}) \in ℝ$
135	128	resqcld	$⊢ φ \to N^{2} \in ℝ$
136	134 135	remulcld	$⊢ φ \to 7.348 (\frac{\log N}{\sqrt{N}}) N^{2} \in ℝ$
137		0re	$⊢ 0 \in ℝ$
138		7re	$⊢ 7 \in ℝ$
139		9re	$⊢ 9 \in ℝ$
140		5re	$⊢ 5 \in ℝ$
141	140 140	pm3.2i	$⊢ (5 \in ℝ \land 5 \in ℝ)$
142		dp2cl	$⊢ (5 \in ℝ \land 5 \in ℝ) \to 55 \in ℝ$
143	141 142	ax-mp	$⊢ 55 \in ℝ$
144	139 143	pm3.2i	$⊢ (9 \in ℝ \land 55 \in ℝ)$
145		dp2cl	$⊢ (9 \in ℝ \land 55 \in ℝ) \to 955 \in ℝ$
146	144 145	ax-mp	$⊢ 955 \in ℝ$
147	139 146	pm3.2i	$⊢ (9 \in ℝ \land 955 \in ℝ)$
148		dp2cl	$⊢ (9 \in ℝ \land 955 \in ℝ) \to 9955 \in ℝ$
149	147 148	ax-mp	$⊢ 9955 \in ℝ$
150	138 149	pm3.2i	$⊢ (7 \in ℝ \land 9955 \in ℝ)$
151		dp2cl	$⊢ (7 \in ℝ \land 9955 \in ℝ) \to 79955 \in ℝ$
152	150 151	ax-mp	$⊢ 79955 \in ℝ$
153	137 152	pm3.2i	$⊢ (0 \in ℝ \land 79955 \in ℝ)$
154		dp2cl	$⊢ (0 \in ℝ \land 79955 \in ℝ) \to 079955 \in ℝ$
155	153 154	ax-mp	$⊢ 079955 \in ℝ$
156		dpcl	$⊢ (1 \in ℕ_{0} \land 079955 \in ℝ) \to 1.079955 \in ℝ$
157	60 155 156	mp2an	$⊢ 1.079955 \in ℝ$
158	157	a1i	$⊢ φ \to 1.079955 \in ℝ$
159	158	resqcld	$⊢ φ \to {1.079955}^{2} \in ℝ$
160		1re	$⊢ 1 \in ℝ$
161	160 115	pm3.2i	$⊢ (1 \in ℝ \land 4 \in ℝ)$
162		dp2cl	$⊢ (1 \in ℝ \land 4 \in ℝ) \to 14 \in ℝ$
163	161 162	ax-mp	$⊢ 14 \in ℝ$
164	115 163	pm3.2i	$⊢ (4 \in ℝ \land 14 \in ℝ)$
165		dp2cl	$⊢ (4 \in ℝ \land 14 \in ℝ) \to 414 \in ℝ$
166	164 165	ax-mp	$⊢ 414 \in ℝ$
167		dpcl	$⊢ (1 \in ℕ_{0} \land 414 \in ℝ) \to 1.414 \in ℝ$
168	60 166 167	mp2an	$⊢ 1.414 \in ℝ$
169	168	a1i	$⊢ φ \to 1.414 \in ℝ$
170	159 169	remulcld	$⊢ φ \to {1.079955}^{2} \cdot 1.414 \in ℝ$
171	41 51	remulcld	$⊢ (φ \land n \in ((ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N))) \to Λ (n (1)) Λ (n (2)) \in ℝ$
172	30 171	remulcld	$⊢ (φ \land n \in ((ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N))) \to Λ (n (0)) Λ (n (1)) Λ (n (2)) \in ℝ$
173	14 172	fsumrecl	$⊢ φ \to \sum_{n \in (ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N)} Λ (n (0)) Λ (n (1)) Λ (n (2)) \in ℝ$
174	170 173	remulcld	$⊢ φ \to {1.079955}^{2} \cdot 1.414 \sum_{n \in (ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N)} Λ (n (0)) Λ (n (1)) Λ (n (2)) \in ℝ$
175	59 112	remulcld	$⊢ φ \to 3 \sum_{n \in \{d \in (ℕ repr (3) N) \| \neg d (0) \in (O \cap ℙ)\}} Λ (n (0)) Λ (n (1)) Λ (n (2)) \in ℝ$
176	170 175	remulcld	$⊢ φ \to {1.079955}^{2} \cdot 1.414 3 \sum_{n \in \{d \in (ℕ repr (3) N) \| \neg d (0) \in (O \cap ℙ)\}} Λ (n (0)) Λ (n (1)) Λ (n (2)) \in ℝ$
177	14 158 169 4 5 29 40 50 6 7	hgt750lemf	$⊢ φ \to \sum_{n \in (ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N)} Λ (n (0)) H (n (0)) Λ (n (1)) K (n (1)) Λ (n (2)) K (n (2)) \leq {1.079955}^{2} \cdot 1.414 \sum_{n \in (ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N)} Λ (n (0)) Λ (n (1)) Λ (n (2))$
178		2re	$⊢ 2 \in ℝ$
179	178	a1i	$⊢ φ \to 2 \in ℝ$
180		10nn0	$⊢ 10 \in ℕ_{0}$
181		2nn0	$⊢ 2 \in ℕ_{0}$
182	181 62	deccl	$⊢ 27 \in ℕ_{0}$
183	180 182	nn0expcli	$⊢ 10^{27} \in ℕ_{0}$
184	183	nn0rei	$⊢ 10^{27} \in ℝ$
185	184	a1i	$⊢ φ \to 10^{27} \in ℝ$
186	180	numexp1	$⊢ 10^{1} = 10$
187	180	nn0rei	$⊢ 10 \in ℝ$
188	186 187	eqeltri	$⊢ 10^{1} \in ℝ$
189	188	a1i	$⊢ φ \to 10^{1} \in ℝ$
190		1nn	$⊢ 1 \in ℕ$
191		2lt9	$⊢ 2 < 9$
192	178 139 191	ltleii	$⊢ 2 \leq 9$
193	190 61 181 192	declei	$⊢ 2 \leq 10$
194	193 186	breqtrri	$⊢ 2 \leq 10^{1}$
195	194	a1i	$⊢ φ \to 2 \leq 10^{1}$
196		1z	$⊢ 1 \in ℤ$
197	182	nn0zi	$⊢ 27 \in ℤ$
198	187 196 197	3pm3.2i	$⊢ (10 \in ℝ \land 1 \in ℤ \land 27 \in ℤ)$
199		1lt10	$⊢ 1 < 10$
200	198 199	pm3.2i	$⊢ ((10 \in ℝ \land 1 \in ℤ \land 27 \in ℤ) \land 1 < 10)$
201		2nn	$⊢ 2 \in ℕ$
202		1lt9	$⊢ 1 < 9$
203	160 139 202	ltleii	$⊢ 1 \leq 9$
204	201 62 60 203	declei	$⊢ 1 \leq 27$
205		leexp2	$⊢ ((10 \in ℝ \land 1 \in ℤ \land 27 \in ℤ) \land 1 < 10) \to (1 \leq 27 \leftrightarrow 10^{1} \leq 10^{27})$
206	205	biimpa	$⊢ (((10 \in ℝ \land 1 \in ℤ \land 27 \in ℤ) \land 1 < 10) \land 1 \leq 27) \to 10^{1} \leq 10^{27}$
207	200 204 206	mp2an	$⊢ 10^{1} \leq 10^{27}$
208	207	a1i	$⊢ φ \to 10^{1} \leq 10^{27}$
209	179 189 185 195 208	letrd	$⊢ φ \to 2 \leq 10^{27}$
210	179 185 128 209 3	letrd	$⊢ φ \to 2 \leq N$
211		eqid	$⊢ (e \in \{c \in (ℕ repr (3) N) \| \neg c (a) \in (O \cap ℙ)\} ⟼ e \circ if (a = 0, {I ↾}_{(0 ..^3)}, pmTrsp ((0 ..^3)) (\{a, 0\}))) = (e \in \{c \in (ℕ repr (3) N) \| \neg c (a) \in (O \cap ℙ)\} ⟼ e \circ if (a = 0, {I ↾}_{(0 ..^3)}, pmTrsp ((0 ..^3)) (\{a, 0\})))$
212	1 2 210 90 211	hgt750lema	$⊢ φ \to \sum_{n \in (ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N)} Λ (n (0)) Λ (n (1)) Λ (n (2)) \leq 3 \sum_{n \in \{d \in (ℕ repr (3) N) \| \neg d (0) \in (O \cap ℙ)\}} Λ (n (0)) Λ (n (1)) Λ (n (2))$
213		2z	$⊢ 2 \in ℤ$
214	213	a1i	$⊢ φ \to 2 \in ℤ$
215	74 214	rpexpcld	$⊢ φ \to {1.079955}^{2} \in ℝ^{+}$
216	215 84	rpmulcld	$⊢ φ \to {1.079955}^{2} \cdot 1.414 \in ℝ^{+}$
217	173 175 216	lemul2d	$⊢ φ \to (\sum_{n \in (ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N)} Λ (n (0)) Λ (n (1)) Λ (n (2)) \leq 3 \sum_{n \in \{d \in (ℕ repr (3) N) \| \neg d (0) \in (O \cap ℙ)\}} Λ (n (0)) Λ (n (1)) Λ (n (2)) \leftrightarrow {1.079955}^{2} \cdot 1.414 \sum_{n \in (ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N)} Λ (n (0)) Λ (n (1)) Λ (n (2)) \leq {1.079955}^{2} \cdot 1.414 3 \sum_{n \in \{d \in (ℕ repr (3) N) \| \neg d (0) \in (O \cap ℙ)\}} Λ (n (0)) Λ (n (1)) Λ (n (2)))$
218	212 217	mpbid	$⊢ φ \to {1.079955}^{2} \cdot 1.414 \sum_{n \in (ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N)} Λ (n (0)) Λ (n (1)) Λ (n (2)) \leq {1.079955}^{2} \cdot 1.414 3 \sum_{n \in \{d \in (ℕ repr (3) N) \| \neg d (0) \in (O \cap ℙ)\}} Λ (n (0)) Λ (n (1)) Λ (n (2))$
219	57 174 176 177 218	letrd	$⊢ φ \to \sum_{n \in (ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N)} Λ (n (0)) H (n (0)) Λ (n (1)) K (n (1)) Λ (n (2)) K (n (2)) \leq {1.079955}^{2} \cdot 1.414 3 \sum_{n \in \{d \in (ℕ repr (3) N) \| \neg d (0) \in (O \cap ℙ)\}} Λ (n (0)) Λ (n (1)) Λ (n (2))$
220	158	recnd	$⊢ φ \to 1.079955 \in ℂ$
221	220	sqcld	$⊢ φ \to {1.079955}^{2} \in ℂ$
222	169	recnd	$⊢ φ \to 1.414 \in ℂ$
223	221 222	mulcld	$⊢ φ \to {1.079955}^{2} \cdot 1.414 \in ℂ$
224		3cn	$⊢ 3 \in ℂ$
225	224	a1i	$⊢ φ \to 3 \in ℂ$
226	112	recnd	$⊢ φ \to \sum_{n \in \{d \in (ℕ repr (3) N) \| \neg d (0) \in (O \cap ℙ)\}} Λ (n (0)) Λ (n (1)) Λ (n (2)) \in ℂ$
227	223 225 226	mul12d	$⊢ φ \to {1.079955}^{2} \cdot 1.414 3 \sum_{n \in \{d \in (ℕ repr (3) N) \| \neg d (0) \in (O \cap ℙ)\}} Λ (n (0)) Λ (n (1)) Λ (n (2)) = 3 {1.079955}^{2} \cdot 1.414 \sum_{n \in \{d \in (ℕ repr (3) N) \| \neg d (0) \in (O \cap ℙ)\}} Λ (n (0)) Λ (n (1)) Λ (n (2))$
228	219 227	breqtrd	$⊢ φ \to \sum_{n \in (ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N)} Λ (n (0)) H (n (0)) Λ (n (1)) K (n (1)) Λ (n (2)) K (n (2)) \leq 3 {1.079955}^{2} \cdot 1.414 \sum_{n \in \{d \in (ℕ repr (3) N) \| \neg d (0) \in (O \cap ℙ)\}} Λ (n (0)) Λ (n (1)) Λ (n (2))$
229		fzfi	$⊢ (1 \dots N) \in Fin$
230		diffi	$⊢ (1 \dots N) \in Fin \to (1 \dots N) ∖ ℙ \in Fin$
231	229 230	ax-mp	$⊢ (1 \dots N) ∖ ℙ \in Fin$
232		snfi	$⊢ \{2\} \in Fin$
233		unfi	$⊢ ((1 \dots N) ∖ ℙ \in Fin \land \{2\} \in Fin) \to ((1 \dots N) ∖ ℙ) \cup \{2\} \in Fin$
234	231 232 233	mp2an	$⊢ ((1 \dots N) ∖ ℙ) \cup \{2\} \in Fin$
235	234	a1i	$⊢ φ \to ((1 \dots N) ∖ ℙ) \cup \{2\} \in Fin$
236	15	a1i	$⊢ (φ \land i \in (((1 \dots N) ∖ ℙ) \cup \{2\})) \to Λ : ℕ ⟶ ℝ$
237		fz1ssnn	$⊢ (1 \dots N) \subseteq ℕ$
238	237	a1i	$⊢ φ \to (1 \dots N) \subseteq ℕ$
239	238	ssdifssd	$⊢ φ \to (1 \dots N) ∖ ℙ \subseteq ℕ$
240	201	a1i	$⊢ φ \to 2 \in ℕ$
241	240	snssd	$⊢ φ \to \{2\} \subseteq ℕ$
242	239 241	unssd	$⊢ φ \to ((1 \dots N) ∖ ℙ) \cup \{2\} \subseteq ℕ$
243	242	sselda	$⊢ (φ \land i \in (((1 \dots N) ∖ ℙ) \cup \{2\})) \to i \in ℕ$
244	236 243	ffvelrnd	$⊢ (φ \land i \in (((1 \dots N) ∖ ℙ) \cup \{2\})) \to Λ (i) \in ℝ$
245	235 244	fsumrecl	$⊢ φ \to \sum_{i \in ((1 \dots N) ∖ ℙ) \cup \{2\}} Λ (i) \in ℝ$
246		chpvalz	$⊢ N \in ℤ \to ψ (N) = \sum_{j = 1}^{N} Λ (j)$
247	18 246	syl	$⊢ φ \to ψ (N) = \sum_{j = 1}^{N} Λ (j)$
248		chpf	$⊢ ψ : ℝ ⟶ ℝ$
249	248	a1i	$⊢ φ \to ψ : ℝ ⟶ ℝ$
250	249 128	ffvelrnd	$⊢ φ \to ψ (N) \in ℝ$
251	247 250	eqeltrrd	$⊢ φ \to \sum_{j = 1}^{N} Λ (j) \in ℝ$
252	245 251	remulcld	$⊢ φ \to \sum_{i \in ((1 \dots N) ∖ ℙ) \cup \{2\}} Λ (i) \sum_{j = 1}^{N} Λ (j) \in ℝ$
253	127 252	remulcld	$⊢ φ \to \log N \sum_{i \in ((1 \dots N) ∖ ℙ) \cup \{2\}} Λ (i) \sum_{j = 1}^{N} Λ (j) \in ℝ$
254	86 253	remulcld	$⊢ φ \to {1.079955}^{2} \cdot 1.414 \log N \sum_{i \in ((1 \dots N) ∖ ℙ) \cup \{2\}} Λ (i) \sum_{j = 1}^{N} Λ (j) \in ℝ$
255	59 254	remulcld	$⊢ φ \to 3 {1.079955}^{2} \cdot 1.414 \log N \sum_{i \in ((1 \dots N) ∖ ℙ) \cup \{2\}} Λ (i) \sum_{j = 1}^{N} Λ (j) \in ℝ$
256	1 2 210 90	hgt750lemb	$⊢ φ \to \sum_{n \in \{d \in (ℕ repr (3) N) \| \neg d (0) \in (O \cap ℙ)\}} Λ (n (0)) Λ (n (1)) Λ (n (2)) \leq \log N \sum_{i \in ((1 \dots N) ∖ ℙ) \cup \{2\}} Λ (i) \sum_{j = 1}^{N} Λ (j)$
257	112 253 216	lemul2d	$⊢ φ \to (\sum_{n \in \{d \in (ℕ repr (3) N) \| \neg d (0) \in (O \cap ℙ)\}} Λ (n (0)) Λ (n (1)) Λ (n (2)) \leq \log N \sum_{i \in ((1 \dots N) ∖ ℙ) \cup \{2\}} Λ (i) \sum_{j = 1}^{N} Λ (j) \leftrightarrow {1.079955}^{2} \cdot 1.414 \sum_{n \in \{d \in (ℕ repr (3) N) \| \neg d (0) \in (O \cap ℙ)\}} Λ (n (0)) Λ (n (1)) Λ (n (2)) \leq {1.079955}^{2} \cdot 1.414 \log N \sum_{i \in ((1 \dots N) ∖ ℙ) \cup \{2\}} Λ (i) \sum_{j = 1}^{N} Λ (j))$
258	256 257	mpbid	$⊢ φ \to {1.079955}^{2} \cdot 1.414 \sum_{n \in \{d \in (ℕ repr (3) N) \| \neg d (0) \in (O \cap ℙ)\}} Λ (n (0)) Λ (n (1)) Λ (n (2)) \leq {1.079955}^{2} \cdot 1.414 \log N \sum_{i \in ((1 \dots N) ∖ ℙ) \cup \{2\}} Λ (i) \sum_{j = 1}^{N} Λ (j)$
259		3rp	$⊢ 3 \in ℝ^{+}$
260	259	a1i	$⊢ φ \to 3 \in ℝ^{+}$
261	113 254 260	lemul2d	$⊢ φ \to ({1.079955}^{2} \cdot 1.414 \sum_{n \in \{d \in (ℕ repr (3) N) \| \neg d (0) \in (O \cap ℙ)\}} Λ (n (0)) Λ (n (1)) Λ (n (2)) \leq {1.079955}^{2} \cdot 1.414 \log N \sum_{i \in ((1 \dots N) ∖ ℙ) \cup \{2\}} Λ (i) \sum_{j = 1}^{N} Λ (j) \leftrightarrow 3 {1.079955}^{2} \cdot 1.414 \sum_{n \in \{d \in (ℕ repr (3) N) \| \neg d (0) \in (O \cap ℙ)\}} Λ (n (0)) Λ (n (1)) Λ (n (2)) \leq 3 {1.079955}^{2} \cdot 1.414 \log N \sum_{i \in ((1 \dots N) ∖ ℙ) \cup \{2\}} Λ (i) \sum_{j = 1}^{N} Λ (j))$
262	258 261	mpbid	$⊢ φ \to 3 {1.079955}^{2} \cdot 1.414 \sum_{n \in \{d \in (ℕ repr (3) N) \| \neg d (0) \in (O \cap ℙ)\}} Λ (n (0)) Λ (n (1)) Λ (n (2)) \leq 3 {1.079955}^{2} \cdot 1.414 \log N \sum_{i \in ((1 \dots N) ∖ ℙ) \cup \{2\}} Λ (i) \sum_{j = 1}^{N} Λ (j)$
263		6re	$⊢ 6 \in ℝ$
264	263 58	pm3.2i	$⊢ (6 \in ℝ \land 3 \in ℝ)$
265		dp2cl	$⊢ (6 \in ℝ \land 3 \in ℝ) \to 63 \in ℝ$
266	264 265	ax-mp	$⊢ 63 \in ℝ$
267	178 266	pm3.2i	$⊢ (2 \in ℝ \land 63 \in ℝ)$
268		dp2cl	$⊢ (2 \in ℝ \land 63 \in ℝ) \to 263 \in ℝ$
269	267 268	ax-mp	$⊢ 263 \in ℝ$
270	115 269	pm3.2i	$⊢ (4 \in ℝ \land 263 \in ℝ)$
271		dp2cl	$⊢ (4 \in ℝ \land 263 \in ℝ) \to 4263 \in ℝ$
272	270 271	ax-mp	$⊢ 4263 \in ℝ$
273		dpcl	$⊢ (1 \in ℕ_{0} \land 4263 \in ℝ) \to 1.4263 \in ℝ$
274	60 272 273	mp2an	$⊢ 1.4263 \in ℝ$
275	274	a1i	$⊢ φ \to 1.4263 \in ℝ$
276	275 130	remulcld	$⊢ φ \to 1.4263 \sqrt{N} \in ℝ$
277	116 58	pm3.2i	$⊢ (8 \in ℝ \land 3 \in ℝ)$
278		dp2cl	$⊢ (8 \in ℝ \land 3 \in ℝ) \to 83 \in ℝ$
279	277 278	ax-mp	$⊢ 83 \in ℝ$
280	116 279	pm3.2i	$⊢ (8 \in ℝ \land 83 \in ℝ)$
281		dp2cl	$⊢ (8 \in ℝ \land 83 \in ℝ) \to 883 \in ℝ$
282	280 281	ax-mp	$⊢ 883 \in ℝ$
283	58 282	pm3.2i	$⊢ (3 \in ℝ \land 883 \in ℝ)$
284		dp2cl	$⊢ (3 \in ℝ \land 883 \in ℝ) \to 3883 \in ℝ$
285	283 284	ax-mp	$⊢ 3883 \in ℝ$
286	137 285	pm3.2i	$⊢ (0 \in ℝ \land 3883 \in ℝ)$
287		dp2cl	$⊢ (0 \in ℝ \land 3883 \in ℝ) \to 03883 \in ℝ$
288	286 287	ax-mp	$⊢ 03883 \in ℝ$
289		dpcl	$⊢ (1 \in ℕ_{0} \land 03883 \in ℝ) \to 1.03883 \in ℝ$
290	60 288 289	mp2an	$⊢ 1.03883 \in ℝ$
291	290	a1i	$⊢ φ \to 1.03883 \in ℝ$
292	291 128	remulcld	$⊢ φ \to 1.03883 \cdot N \in ℝ$
293	276 292	remulcld	$⊢ φ \to 1.4263 \sqrt{N} 1.03883 \cdot N \in ℝ$
294	127 293	remulcld	$⊢ φ \to \log N 1.4263 \sqrt{N} 1.03883 \cdot N \in ℝ$
295	86 294	remulcld	$⊢ φ \to {1.079955}^{2} \cdot 1.414 \log N 1.4263 \sqrt{N} 1.03883 \cdot N \in ℝ$
296	59 295	remulcld	$⊢ φ \to 3 {1.079955}^{2} \cdot 1.414 \log N 1.4263 \sqrt{N} 1.03883 \cdot N \in ℝ$
297		vmage0	$⊢ i \in ℕ \to 0 \leq Λ (i)$
298	243 297	syl	$⊢ (φ \land i \in (((1 \dots N) ∖ ℙ) \cup \{2\})) \to 0 \leq Λ (i)$
299	235 244 298	fsumge0	$⊢ φ \to 0 \leq \sum_{i \in ((1 \dots N) ∖ ℙ) \cup \{2\}} Λ (i)$
300	2 3	hgt750lemd	$⊢ φ \to \sum_{i \in ((1 \dots N) ∖ ℙ) \cup \{2\}} Λ (i) < 1.4263 \sqrt{N}$
301		fzfid	$⊢ φ \to (1 \dots N) \in Fin$
302	15	a1i	$⊢ (φ \land j \in (1 \dots N)) \to Λ : ℕ ⟶ ℝ$
303	238	sselda	$⊢ (φ \land j \in (1 \dots N)) \to j \in ℕ$
304	302 303	ffvelrnd	$⊢ (φ \land j \in (1 \dots N)) \to Λ (j) \in ℝ$
305		vmage0	$⊢ j \in ℕ \to 0 \leq Λ (j)$
306	303 305	syl	$⊢ (φ \land j \in (1 \dots N)) \to 0 \leq Λ (j)$
307	301 304 306	fsumge0	$⊢ φ \to 0 \leq \sum_{j = 1}^{N} Λ (j)$
308	2	hgt750lemc	$⊢ φ \to \sum_{j = 1}^{N} Λ (j) < 1.03883 \cdot N$
309	245 276 251 292 299 300 307 308	ltmul12ad	$⊢ φ \to \sum_{i \in ((1 \dots N) ∖ ℙ) \cup \{2\}} Λ (i) \sum_{j = 1}^{N} Λ (j) < 1.4263 \sqrt{N} 1.03883 \cdot N$
310	252 293 309	ltled	$⊢ φ \to \sum_{i \in ((1 \dots N) ∖ ℙ) \cup \{2\}} Λ (i) \sum_{j = 1}^{N} Λ (j) \leq 1.4263 \sqrt{N} 1.03883 \cdot N$
311	160	a1i	$⊢ φ \to 1 \in ℝ$
312		1lt2	$⊢ 1 < 2$
313	312	a1i	$⊢ φ \to 1 < 2$
314	311 179 128 313 210	ltletrd	$⊢ φ \to 1 < N$
315	128 314	rplogcld	$⊢ φ \to \log N \in ℝ^{+}$
316	252 293 315	lemul2d	$⊢ φ \to (\sum_{i \in ((1 \dots N) ∖ ℙ) \cup \{2\}} Λ (i) \sum_{j = 1}^{N} Λ (j) \leq 1.4263 \sqrt{N} 1.03883 \cdot N \leftrightarrow \log N \sum_{i \in ((1 \dots N) ∖ ℙ) \cup \{2\}} Λ (i) \sum_{j = 1}^{N} Λ (j) \leq \log N 1.4263 \sqrt{N} 1.03883 \cdot N)$
317	310 316	mpbid	$⊢ φ \to \log N \sum_{i \in ((1 \dots N) ∖ ℙ) \cup \{2\}} Λ (i) \sum_{j = 1}^{N} Λ (j) \leq \log N 1.4263 \sqrt{N} 1.03883 \cdot N$
318	253 294 216	lemul2d	$⊢ φ \to (\log N \sum_{i \in ((1 \dots N) ∖ ℙ) \cup \{2\}} Λ (i) \sum_{j = 1}^{N} Λ (j) \leq \log N 1.4263 \sqrt{N} 1.03883 \cdot N \leftrightarrow {1.079955}^{2} \cdot 1.414 \log N \sum_{i \in ((1 \dots N) ∖ ℙ) \cup \{2\}} Λ (i) \sum_{j = 1}^{N} Λ (j) \leq {1.079955}^{2} \cdot 1.414 \log N 1.4263 \sqrt{N} 1.03883 \cdot N)$
319	317 318	mpbid	$⊢ φ \to {1.079955}^{2} \cdot 1.414 \log N \sum_{i \in ((1 \dots N) ∖ ℙ) \cup \{2\}} Λ (i) \sum_{j = 1}^{N} Λ (j) \leq {1.079955}^{2} \cdot 1.414 \log N 1.4263 \sqrt{N} 1.03883 \cdot N$
320	254 295 260	lemul2d	$⊢ φ \to ({1.079955}^{2} \cdot 1.414 \log N \sum_{i \in ((1 \dots N) ∖ ℙ) \cup \{2\}} Λ (i) \sum_{j = 1}^{N} Λ (j) \leq {1.079955}^{2} \cdot 1.414 \log N 1.4263 \sqrt{N} 1.03883 \cdot N \leftrightarrow 3 {1.079955}^{2} \cdot 1.414 \log N \sum_{i \in ((1 \dots N) ∖ ℙ) \cup \{2\}} Λ (i) \sum_{j = 1}^{N} Λ (j) \leq 3 {1.079955}^{2} \cdot 1.414 \log N 1.4263 \sqrt{N} 1.03883 \cdot N)$
321	319 320	mpbid	$⊢ φ \to 3 {1.079955}^{2} \cdot 1.414 \log N \sum_{i \in ((1 \dots N) ∖ ℙ) \cup \{2\}} Λ (i) \sum_{j = 1}^{N} Λ (j) \leq 3 {1.079955}^{2} \cdot 1.414 \log N 1.4263 \sqrt{N} 1.03883 \cdot N$
322	157	resqcli	$⊢ {1.079955}^{2} \in ℝ$
323	322 168	remulcli	$⊢ {1.079955}^{2} \cdot 1.414 \in ℝ$
324	274 290	remulcli	$⊢ 1.4263 \cdot 1.03883 \in ℝ$
325	323 324	remulcli	$⊢ {1.079955}^{2} \cdot 1.414 1.4263 \cdot 1.03883 \in ℝ$
326	58 325	remulcli	$⊢ 3 {1.079955}^{2} \cdot 1.414 1.4263 \cdot 1.03883 \in ℝ$
327		hgt750lem2	$⊢ 3 {1.079955}^{2} \cdot 1.414 1.4263 \cdot 1.03883 < 7.348$
328	326 124 327	ltleii	$⊢ 3 {1.079955}^{2} \cdot 1.414 1.4263 \cdot 1.03883 \leq 7.348$
329	326	a1i	$⊢ φ \to 3 {1.079955}^{2} \cdot 1.414 1.4263 \cdot 1.03883 \in ℝ$
330	315 131	rpdivcld	$⊢ φ \to \frac{\log N}{\sqrt{N}} \in ℝ^{+}$
331	126 214	rpexpcld	$⊢ φ \to N^{2} \in ℝ^{+}$
332	330 331	rpmulcld	$⊢ φ \to (\frac{\log N}{\sqrt{N}}) N^{2} \in ℝ^{+}$
333	329 125 332	lemul1d	$⊢ φ \to (3 {1.079955}^{2} \cdot 1.414 1.4263 \cdot 1.03883 \leq 7.348 \leftrightarrow 3 {1.079955}^{2} \cdot 1.414 1.4263 \cdot 1.03883 (\frac{\log N}{\sqrt{N}}) N^{2} \leq 7.348 (\frac{\log N}{\sqrt{N}}) N^{2})$
334	328 333	mpbii	$⊢ φ \to 3 {1.079955}^{2} \cdot 1.414 1.4263 \cdot 1.03883 (\frac{\log N}{\sqrt{N}}) N^{2} \leq 7.348 (\frac{\log N}{\sqrt{N}}) N^{2}$
335	275	recnd	$⊢ φ \to 1.4263 \in ℂ$
336	130	recnd	$⊢ φ \to \sqrt{N} \in ℂ$
337	291	recnd	$⊢ φ \to 1.03883 \in ℂ$
338	128	recnd	$⊢ φ \to N \in ℂ$
339	335 336 337 338	mul4d	$⊢ φ \to 1.4263 \sqrt{N} 1.03883 \cdot N = 1.4263 \cdot 1.03883 \sqrt{N} \cdot N$
340	339	oveq2d	$⊢ φ \to \log N 1.4263 \sqrt{N} 1.03883 \cdot N = \log N 1.4263 \cdot 1.03883 \sqrt{N} \cdot N$
341	127	recnd	$⊢ φ \to \log N \in ℂ$
342	335 337	mulcld	$⊢ φ \to 1.4263 \cdot 1.03883 \in ℂ$
343	336 338	mulcld	$⊢ φ \to \sqrt{N} \cdot N \in ℂ$
344	342 343	mulcld	$⊢ φ \to 1.4263 \cdot 1.03883 \sqrt{N} \cdot N \in ℂ$
345	341 344	mulcomd	$⊢ φ \to \log N 1.4263 \cdot 1.03883 \sqrt{N} \cdot N = 1.4263 \cdot 1.03883 \sqrt{N} \cdot N \log N$
346	340 345	eqtrd	$⊢ φ \to \log N 1.4263 \sqrt{N} 1.03883 \cdot N = 1.4263 \cdot 1.03883 \sqrt{N} \cdot N \log N$
347	342 343 341	mulassd	$⊢ φ \to 1.4263 \cdot 1.03883 \sqrt{N} \cdot N \log N = 1.4263 \cdot 1.03883 \sqrt{N} \cdot N \log N$
348	346 347	eqtrd	$⊢ φ \to \log N 1.4263 \sqrt{N} 1.03883 \cdot N = 1.4263 \cdot 1.03883 \sqrt{N} \cdot N \log N$
349	348	oveq2d	$⊢ φ \to {1.079955}^{2} \cdot 1.414 \log N 1.4263 \sqrt{N} 1.03883 \cdot N = {1.079955}^{2} \cdot 1.414 1.4263 \cdot 1.03883 \sqrt{N} \cdot N \log N$
350	86	recnd	$⊢ φ \to {1.079955}^{2} \cdot 1.414 \in ℂ$
351	343 341	mulcld	$⊢ φ \to \sqrt{N} \cdot N \log N \in ℂ$
352	350 342 351	mulassd	$⊢ φ \to {1.079955}^{2} \cdot 1.414 1.4263 \cdot 1.03883 \sqrt{N} \cdot N \log N = {1.079955}^{2} \cdot 1.414 1.4263 \cdot 1.03883 \sqrt{N} \cdot N \log N$
353	349 352	eqtr4d	$⊢ φ \to {1.079955}^{2} \cdot 1.414 \log N 1.4263 \sqrt{N} 1.03883 \cdot N = {1.079955}^{2} \cdot 1.414 1.4263 \cdot 1.03883 \sqrt{N} \cdot N \log N$
354	353	oveq2d	$⊢ φ \to 3 {1.079955}^{2} \cdot 1.414 \log N 1.4263 \sqrt{N} 1.03883 \cdot N = 3 {1.079955}^{2} \cdot 1.414 1.4263 \cdot 1.03883 \sqrt{N} \cdot N \log N$
355	59	recnd	$⊢ φ \to 3 \in ℂ$
356	350 342	mulcld	$⊢ φ \to {1.079955}^{2} \cdot 1.414 1.4263 \cdot 1.03883 \in ℂ$
357	355 356 351	mulassd	$⊢ φ \to 3 {1.079955}^{2} \cdot 1.414 1.4263 \cdot 1.03883 \sqrt{N} \cdot N \log N = 3 {1.079955}^{2} \cdot 1.414 1.4263 \cdot 1.03883 \sqrt{N} \cdot N \log N$
358	354 357	eqtr4d	$⊢ φ \to 3 {1.079955}^{2} \cdot 1.414 \log N 1.4263 \sqrt{N} 1.03883 \cdot N = 3 {1.079955}^{2} \cdot 1.414 1.4263 \cdot 1.03883 \sqrt{N} \cdot N \log N$
359	135	recnd	$⊢ φ \to N^{2} \in ℂ$
360	341 336 359 132	div32d	$⊢ φ \to (\frac{\log N}{\sqrt{N}}) N^{2} = \log N (\frac{N^{2}}{\sqrt{N}})$
361	359 336 132	divcld	$⊢ φ \to \frac{N^{2}}{\sqrt{N}} \in ℂ$
362	341 361	mulcomd	$⊢ φ \to \log N (\frac{N^{2}}{\sqrt{N}}) = (\frac{N^{2}}{\sqrt{N}}) \log N$
363	338	sqvald	$⊢ φ \to N^{2} = N \cdot N$
364	363	oveq1d	$⊢ φ \to \frac{N^{2}}{\sqrt{N}} = \frac{N \cdot N}{\sqrt{N}}$
365	338 338 336 132	divassd	$⊢ φ \to \frac{N \cdot N}{\sqrt{N}} = N (\frac{N}{\sqrt{N}})$
366		divsqrtid	$⊢ N \in ℝ^{+} \to \frac{N}{\sqrt{N}} = \sqrt{N}$
367	126 366	syl	$⊢ φ \to \frac{N}{\sqrt{N}} = \sqrt{N}$
368	367	oveq2d	$⊢ φ \to N (\frac{N}{\sqrt{N}}) = N \sqrt{N}$
369	364 365 368	3eqtrd	$⊢ φ \to \frac{N^{2}}{\sqrt{N}} = N \sqrt{N}$
370	338 336	mulcomd	$⊢ φ \to N \sqrt{N} = \sqrt{N} \cdot N$
371	369 370	eqtrd	$⊢ φ \to \frac{N^{2}}{\sqrt{N}} = \sqrt{N} \cdot N$
372	371	oveq1d	$⊢ φ \to (\frac{N^{2}}{\sqrt{N}}) \log N = \sqrt{N} \cdot N \log N$
373	360 362 372	3eqtrrd	$⊢ φ \to \sqrt{N} \cdot N \log N = (\frac{\log N}{\sqrt{N}}) N^{2}$
374	373	oveq2d	$⊢ φ \to 3 {1.079955}^{2} \cdot 1.414 1.4263 \cdot 1.03883 \sqrt{N} \cdot N \log N = 3 {1.079955}^{2} \cdot 1.414 1.4263 \cdot 1.03883 (\frac{\log N}{\sqrt{N}}) N^{2}$
375	358 374	eqtrd	$⊢ φ \to 3 {1.079955}^{2} \cdot 1.414 \log N 1.4263 \sqrt{N} 1.03883 \cdot N = 3 {1.079955}^{2} \cdot 1.414 1.4263 \cdot 1.03883 (\frac{\log N}{\sqrt{N}}) N^{2}$
376	125	recnd	$⊢ φ \to 7.348 \in ℂ$
377	133	recnd	$⊢ φ \to \frac{\log N}{\sqrt{N}} \in ℂ$
378	376 377 359	mulassd	$⊢ φ \to 7.348 (\frac{\log N}{\sqrt{N}}) N^{2} = 7.348 (\frac{\log N}{\sqrt{N}}) N^{2}$
379	334 375 378	3brtr4d	$⊢ φ \to 3 {1.079955}^{2} \cdot 1.414 \log N 1.4263 \sqrt{N} 1.03883 \cdot N \leq 7.348 (\frac{\log N}{\sqrt{N}}) N^{2}$
380	255 296 136 321 379	letrd	$⊢ φ \to 3 {1.079955}^{2} \cdot 1.414 \log N \sum_{i \in ((1 \dots N) ∖ ℙ) \cup \{2\}} Λ (i) \sum_{j = 1}^{N} Λ (j) \leq 7.348 (\frac{\log N}{\sqrt{N}}) N^{2}$
381	114 255 136 262 380	letrd	$⊢ φ \to 3 {1.079955}^{2} \cdot 1.414 \sum_{n \in \{d \in (ℕ repr (3) N) \| \neg d (0) \in (O \cap ℙ)\}} Λ (n (0)) Λ (n (1)) Λ (n (2)) \leq 7.348 (\frac{\log N}{\sqrt{N}}) N^{2}$
382	57 114 136 228 381	letrd	$⊢ φ \to \sum_{n \in (ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N)} Λ (n (0)) H (n (0)) Λ (n (1)) K (n (1)) Λ (n (2)) K (n (2)) \leq 7.348 (\frac{\log N}{\sqrt{N}}) N^{2}$

Metamath Proof Explorer

Theorem hgt750leme

Proof