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