tgoldbachgtde

	Ref	Expression
Hypotheses	tgoldbachgtda.o	$⊢ O = \{z \in ℤ \| \neg 2 ∥ z\}$
	tgoldbachgtda.n	$⊢ φ \to N \in O$
	tgoldbachgtda.0	$⊢ φ \to 10^{27} \leq N$
	tgoldbachgtda.h	$⊢ φ \to H : ℕ ⟶ [0, +∞)$
	tgoldbachgtda.k	$⊢ φ \to K : ℕ ⟶ [0, +∞)$
	tgoldbachgtda.1	$⊢ (φ \land m \in ℕ) \to K (m) \leq 1.079955$
	tgoldbachgtda.2	$⊢ (φ \land m \in ℕ) \to H (m) \leq 1.414$
	tgoldbachgtda.3	$⊢ φ \to 0.00042248 N^{2} \leq \int_{(0, 1)} ((Λ \times_{f} H) vts N) (x) {((Λ \times_{f} K) vts N) (x)}^{2} e^{i 2 π -N x} d x$
Assertion	tgoldbachgtde	$⊢ φ \to 0 < \sum_{n \in (O \cap ℙ) repr (3) N} Λ (n (0)) H (n (0)) Λ (n (1)) K (n (1)) Λ (n (2)) K (n (2))$

Proof

Step	Hyp	Ref	Expression
1		tgoldbachgtda.o	$⊢ O = \{z \in ℤ \| \neg 2 ∥ z\}$
2		tgoldbachgtda.n	$⊢ φ \to N \in O$
3		tgoldbachgtda.0	$⊢ φ \to 10^{27} \leq N$
4		tgoldbachgtda.h	$⊢ φ \to H : ℕ ⟶ [0, +∞)$
5		tgoldbachgtda.k	$⊢ φ \to K : ℕ ⟶ [0, +∞)$
6		tgoldbachgtda.1	$⊢ (φ \land m \in ℕ) \to K (m) \leq 1.079955$
7		tgoldbachgtda.2	$⊢ (φ \land m \in ℕ) \to H (m) \leq 1.414$
8		tgoldbachgtda.3	$⊢ φ \to 0.00042248 N^{2} \leq \int_{(0, 1)} ((Λ \times_{f} H) vts N) (x) {((Λ \times_{f} K) vts N) (x)}^{2} e^{i 2 π -N x} d x$
9	1 2 3	tgoldbachgnn	$⊢ φ \to N \in ℕ$
10	9	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
11		3nn0	$⊢ 3 \in ℕ_{0}$
12	11	a1i	$⊢ φ \to 3 \in ℕ_{0}$
13		ssidd	$⊢ φ \to ℕ \subseteq ℕ$
14	10 12 13	reprfi2	$⊢ φ \to ℕ repr (3) N \in Fin$
15		diffi	$⊢ ℕ repr (3) N \in Fin \to (ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N) \in Fin$
16	14 15	syl	$⊢ φ \to (ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N) \in Fin$
17		difssd	$⊢ φ \to (ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N) \subseteq ℕ repr (3) N$
18	17	sselda	$⊢ (φ \land n \in ((ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N))) \to n \in (ℕ repr (3) N)$
19		vmaf	$⊢ Λ : ℕ ⟶ ℝ$
20	19	a1i	$⊢ (φ \land n \in (ℕ repr (3) N)) \to Λ : ℕ ⟶ ℝ$
21		ssidd	$⊢ (φ \land n \in (ℕ repr (3) N)) \to ℕ \subseteq ℕ$
22	10	nn0zd	$⊢ φ \to N \in ℤ$
23	22	adantr	$⊢ (φ \land n \in (ℕ repr (3) N)) \to N \in ℤ$
24	11	a1i	$⊢ (φ \land n \in (ℕ repr (3) N)) \to 3 \in ℕ_{0}$
25		simpr	$⊢ (φ \land n \in (ℕ repr (3) N)) \to n \in (ℕ repr (3) N)$
26	21 23 24 25	reprf	$⊢ (φ \land n \in (ℕ repr (3) N)) \to n : (0 ..^3) ⟶ ℕ$
27		c0ex	$⊢ 0 \in V$
28	27	tpid1	$⊢ 0 \in \{0, 1, 2\}$
29		fzo0to3tp	$⊢ (0 ..^3) = \{0, 1, 2\}$
30	28 29	eleqtrri	$⊢ 0 \in (0 ..^3)$
31	30	a1i	$⊢ (φ \land n \in (ℕ repr (3) N)) \to 0 \in (0 ..^3)$
32	26 31	ffvelcdmd	$⊢ (φ \land n \in (ℕ repr (3) N)) \to n (0) \in ℕ$
33	20 32	ffvelcdmd	$⊢ (φ \land n \in (ℕ repr (3) N)) \to Λ (n (0)) \in ℝ$
34		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
35		fss	$⊢ (H : ℕ ⟶ [0, +∞) \land [0, +∞) \subseteq ℝ) \to H : ℕ ⟶ ℝ$
36	4 34 35	sylancl	$⊢ φ \to H : ℕ ⟶ ℝ$
37	36	adantr	$⊢ (φ \land n \in (ℕ repr (3) N)) \to H : ℕ ⟶ ℝ$
38	37 32	ffvelcdmd	$⊢ (φ \land n \in (ℕ repr (3) N)) \to H (n (0)) \in ℝ$
39	33 38	remulcld	$⊢ (φ \land n \in (ℕ repr (3) N)) \to Λ (n (0)) H (n (0)) \in ℝ$
40		1ex	$⊢ 1 \in V$
41	40	tpid2	$⊢ 1 \in \{0, 1, 2\}$
42	41 29	eleqtrri	$⊢ 1 \in (0 ..^3)$
43	42	a1i	$⊢ (φ \land n \in (ℕ repr (3) N)) \to 1 \in (0 ..^3)$
44	26 43	ffvelcdmd	$⊢ (φ \land n \in (ℕ repr (3) N)) \to n (1) \in ℕ$
45	20 44	ffvelcdmd	$⊢ (φ \land n \in (ℕ repr (3) N)) \to Λ (n (1)) \in ℝ$
46		fss	$⊢ (K : ℕ ⟶ [0, +∞) \land [0, +∞) \subseteq ℝ) \to K : ℕ ⟶ ℝ$
47	5 34 46	sylancl	$⊢ φ \to K : ℕ ⟶ ℝ$
48	47	adantr	$⊢ (φ \land n \in (ℕ repr (3) N)) \to K : ℕ ⟶ ℝ$
49	48 44	ffvelcdmd	$⊢ (φ \land n \in (ℕ repr (3) N)) \to K (n (1)) \in ℝ$
50	45 49	remulcld	$⊢ (φ \land n \in (ℕ repr (3) N)) \to Λ (n (1)) K (n (1)) \in ℝ$
51		2ex	$⊢ 2 \in V$
52	51	tpid3	$⊢ 2 \in \{0, 1, 2\}$
53	52 29	eleqtrri	$⊢ 2 \in (0 ..^3)$
54	53	a1i	$⊢ (φ \land n \in (ℕ repr (3) N)) \to 2 \in (0 ..^3)$
55	26 54	ffvelcdmd	$⊢ (φ \land n \in (ℕ repr (3) N)) \to n (2) \in ℕ$
56	20 55	ffvelcdmd	$⊢ (φ \land n \in (ℕ repr (3) N)) \to Λ (n (2)) \in ℝ$
57	48 55	ffvelcdmd	$⊢ (φ \land n \in (ℕ repr (3) N)) \to K (n (2)) \in ℝ$
58	56 57	remulcld	$⊢ (φ \land n \in (ℕ repr (3) N)) \to Λ (n (2)) K (n (2)) \in ℝ$
59	50 58	remulcld	$⊢ (φ \land n \in (ℕ repr (3) N)) \to Λ (n (1)) K (n (1)) Λ (n (2)) K (n (2)) \in ℝ$
60	39 59	remulcld	$⊢ (φ \land n \in (ℕ repr (3) N)) \to Λ (n (0)) H (n (0)) Λ (n (1)) K (n (1)) Λ (n (2)) K (n (2)) \in ℝ$
61	18 60	syldan	$⊢ (φ \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 ℝ$
62	16 61	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 ℝ$
63		0nn0	$⊢ 0 \in ℕ_{0}$
64		qssre	$⊢ ℚ \subseteq ℝ$
65		4nn0	$⊢ 4 \in ℕ_{0}$
66		2nn0	$⊢ 2 \in ℕ_{0}$
67		nn0ssq	$⊢ ℕ_{0} \subseteq ℚ$
68		8nn0	$⊢ 8 \in ℕ_{0}$
69	67 68	sselii	$⊢ 8 \in ℚ$
70	65 69	dp2clq	$⊢ 48 \in ℚ$
71	66 70	dp2clq	$⊢ 248 \in ℚ$
72	66 71	dp2clq	$⊢ 2248 \in ℚ$
73	65 72	dp2clq	$⊢ 42248 \in ℚ$
74	63 73	dp2clq	$⊢ 042248 \in ℚ$
75	63 74	dp2clq	$⊢ 0042248 \in ℚ$
76	63 75	dp2clq	$⊢ 00042248 \in ℚ$
77	64 76	sselii	$⊢ 00042248 \in ℝ$
78		dpcl	$⊢ (0 \in ℕ_{0} \land 00042248 \in ℝ) \to 0.00042248 \in ℝ$
79	63 77 78	mp2an	$⊢ 0.00042248 \in ℝ$
80	79	a1i	$⊢ φ \to 0.00042248 \in ℝ$
81	9	nnred	$⊢ φ \to N \in ℝ$
82	81	resqcld	$⊢ φ \to N^{2} \in ℝ$
83	80 82	remulcld	$⊢ φ \to 0.00042248 N^{2} \in ℝ$
84	14 60	fsumrecl	$⊢ φ \to \sum_{n \in ℕ repr (3) N} Λ (n (0)) H (n (0)) Λ (n (1)) K (n (1)) Λ (n (2)) K (n (2)) \in ℝ$
85		7nn0	$⊢ 7 \in ℕ_{0}$
86	11 70	dp2clq	$⊢ 348 \in ℚ$
87	64 86	sselii	$⊢ 348 \in ℝ$
88		dpcl	$⊢ (7 \in ℕ_{0} \land 348 \in ℝ) \to 7.348 \in ℝ$
89	85 87 88	mp2an	$⊢ 7.348 \in ℝ$
90	89	a1i	$⊢ φ \to 7.348 \in ℝ$
91	9	nnrpd	$⊢ φ \to N \in ℝ^{+}$
92	91	relogcld	$⊢ φ \to \log N \in ℝ$
93	10	nn0ge0d	$⊢ φ \to 0 \leq N$
94	81 93	resqrtcld	$⊢ φ \to \sqrt{N} \in ℝ$
95	91	sqrtgt0d	$⊢ φ \to 0 < \sqrt{N}$
96	95	gt0ne0d	$⊢ φ \to \sqrt{N} \neq 0$
97	92 94 96	redivcld	$⊢ φ \to \frac{\log N}{\sqrt{N}} \in ℝ$
98	90 97	remulcld	$⊢ φ \to 7.348 (\frac{\log N}{\sqrt{N}}) \in ℝ$
99	98 82	remulcld	$⊢ φ \to 7.348 (\frac{\log N}{\sqrt{N}}) N^{2} \in ℝ$
100	1 9 3 4 5 6 7	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}$
101		2z	$⊢ 2 \in ℤ$
102	101	a1i	$⊢ φ \to 2 \in ℤ$
103	91 102	rpexpcld	$⊢ φ \to N^{2} \in ℝ^{+}$
104		hgt750lem	$⊢ (N \in ℕ_{0} \land 10^{27} \leq N) \to 7.348 (\frac{\log N}{\sqrt{N}}) < 0.00042248$
105	10 3 104	syl2anc	$⊢ φ \to 7.348 (\frac{\log N}{\sqrt{N}}) < 0.00042248$
106	98 80 103 105	ltmul1dd	$⊢ φ \to 7.348 (\frac{\log N}{\sqrt{N}}) N^{2} < 0.00042248 N^{2}$
107	62 99 83 100 106	lelttrd	$⊢ φ \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)) < 0.00042248 N^{2}$
108	36 47 10	circlemethhgt	$⊢ φ \to \sum_{n \in ℕ repr (3) N} Λ (n (0)) H (n (0)) Λ (n (1)) K (n (1)) Λ (n (2)) K (n (2)) = \int_{(0, 1)} ((Λ \times_{f} H) vts N) (x) {((Λ \times_{f} K) vts N) (x)}^{2} e^{i 2 π -N x} d x$
109	8 108	breqtrrd	$⊢ φ \to 0.00042248 N^{2} \leq \sum_{n \in ℕ repr (3) N} Λ (n (0)) H (n (0)) Λ (n (1)) K (n (1)) Λ (n (2)) K (n (2))$
110	62 83 84 107 109	ltletrd	$⊢ φ \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)) < \sum_{n \in ℕ repr (3) N} Λ (n (0)) H (n (0)) Λ (n (1)) K (n (1)) Λ (n (2)) K (n (2))$
111	62 84	posdifd	$⊢ φ \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)) < \sum_{n \in ℕ repr (3) N} Λ (n (0)) H (n (0)) Λ (n (1)) K (n (1)) Λ (n (2)) K (n (2)) \leftrightarrow 0 < \sum_{n \in ℕ repr (3) N} Λ (n (0)) H (n (0)) Λ (n (1)) K (n (1)) Λ (n (2)) K (n (2)) - \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)))$
112	110 111	mpbid	$⊢ φ \to 0 < \sum_{n \in ℕ repr (3) N} Λ (n (0)) H (n (0)) Λ (n (1)) K (n (1)) Λ (n (2)) K (n (2)) - \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))$
113		inss2	$⊢ O \cap ℙ \subseteq ℙ$
114		prmssnn	$⊢ ℙ \subseteq ℕ$
115	113 114	sstri	$⊢ O \cap ℙ \subseteq ℕ$
116	115	a1i	$⊢ φ \to O \cap ℙ \subseteq ℕ$
117	13 22 12 116	reprss	$⊢ φ \to (O \cap ℙ) repr (3) N \subseteq ℕ repr (3) N$
118	14 117	ssfid	$⊢ φ \to (O \cap ℙ) repr (3) N \in Fin$
119	117	sselda	$⊢ (φ \land n \in ((O \cap ℙ) repr (3) N)) \to n \in (ℕ repr (3) N)$
120	60	recnd	$⊢ (φ \land n \in (ℕ repr (3) N)) \to Λ (n (0)) H (n (0)) Λ (n (1)) K (n (1)) Λ (n (2)) K (n (2)) \in ℂ$
121	119 120	syldan	$⊢ (φ \land n \in ((O \cap ℙ) repr (3) N)) \to Λ (n (0)) H (n (0)) Λ (n (1)) K (n (1)) Λ (n (2)) K (n (2)) \in ℂ$
122	118 121	fsumcl	$⊢ φ \to \sum_{n \in (O \cap ℙ) repr (3) N} Λ (n (0)) H (n (0)) Λ (n (1)) K (n (1)) Λ (n (2)) K (n (2)) \in ℂ$
123	62	recnd	$⊢ φ \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 ℂ$
124		disjdif	$⊢ ((O \cap ℙ) repr (3) N) \cap ((ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N)) = \emptyset$
125	124	a1i	$⊢ φ \to ((O \cap ℙ) repr (3) N) \cap ((ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N)) = \emptyset$
126		undif	$⊢ (O \cap ℙ) repr (3) N \subseteq ℕ repr (3) N \leftrightarrow ((O \cap ℙ) repr (3) N) \cup ((ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N)) = ℕ repr (3) N$
127	117 126	sylib	$⊢ φ \to ((O \cap ℙ) repr (3) N) \cup ((ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N)) = ℕ repr (3) N$
128	127	eqcomd	$⊢ φ \to ℕ repr (3) N = ((O \cap ℙ) repr (3) N) \cup ((ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N))$
129	125 128 14 120	fsumsplit	$⊢ φ \to \sum_{n \in ℕ repr (3) N} Λ (n (0)) H (n (0)) Λ (n (1)) K (n (1)) Λ (n (2)) K (n (2)) = \sum_{n \in (O \cap ℙ) repr (3) N} Λ (n (0)) H (n (0)) Λ (n (1)) K (n (1)) Λ (n (2)) K (n (2)) + \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))$
130	122 123 129	mvrraddd	$⊢ φ \to \sum_{n \in ℕ repr (3) N} Λ (n (0)) H (n (0)) Λ (n (1)) K (n (1)) Λ (n (2)) K (n (2)) - \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)) = \sum_{n \in (O \cap ℙ) repr (3) N} Λ (n (0)) H (n (0)) Λ (n (1)) K (n (1)) Λ (n (2)) K (n (2))$
131	112 130	breqtrd	$⊢ φ \to 0 < \sum_{n \in (O \cap ℙ) repr (3) N} Λ (n (0)) H (n (0)) Λ (n (1)) K (n (1)) Λ (n (2)) K (n (2))$

Metamath Proof Explorer

Theorem tgoldbachgtde

Proof