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		1eltp012	$⊢ 1 \in \{0, 1, 2\}$
41	40 29	eleqtrri	$⊢ 1 \in (0 ..^3)$
42	41	a1i	$⊢ (φ \land n \in (ℕ repr (3) N)) \to 1 \in (0 ..^3)$
43	26 42	ffvelcdmd	$⊢ (φ \land n \in (ℕ repr (3) N)) \to n (1) \in ℕ$
44	20 43	ffvelcdmd	$⊢ (φ \land n \in (ℕ repr (3) N)) \to Λ (n (1)) \in ℝ$
45		fss	$⊢ (K : ℕ ⟶ [0, +∞) \land [0, +∞) \subseteq ℝ) \to K : ℕ ⟶ ℝ$
46	5 34 45	sylancl	$⊢ φ \to K : ℕ ⟶ ℝ$
47	46	adantr	$⊢ (φ \land n \in (ℕ repr (3) N)) \to K : ℕ ⟶ ℝ$
48	47 43	ffvelcdmd	$⊢ (φ \land n \in (ℕ repr (3) N)) \to K (n (1)) \in ℝ$
49	44 48	remulcld	$⊢ (φ \land n \in (ℕ repr (3) N)) \to Λ (n (1)) K (n (1)) \in ℝ$
50		2ex	$⊢ 2 \in V$
51	50	tpid3	$⊢ 2 \in \{0, 1, 2\}$
52	51 29	eleqtrri	$⊢ 2 \in (0 ..^3)$
53	52	a1i	$⊢ (φ \land n \in (ℕ repr (3) N)) \to 2 \in (0 ..^3)$
54	26 53	ffvelcdmd	$⊢ (φ \land n \in (ℕ repr (3) N)) \to n (2) \in ℕ$
55	20 54	ffvelcdmd	$⊢ (φ \land n \in (ℕ repr (3) N)) \to Λ (n (2)) \in ℝ$
56	47 54	ffvelcdmd	$⊢ (φ \land n \in (ℕ repr (3) N)) \to K (n (2)) \in ℝ$
57	55 56	remulcld	$⊢ (φ \land n \in (ℕ repr (3) N)) \to Λ (n (2)) K (n (2)) \in ℝ$
58	49 57	remulcld	$⊢ (φ \land n \in (ℕ repr (3) N)) \to Λ (n (1)) K (n (1)) Λ (n (2)) K (n (2)) \in ℝ$
59	39 58	remulcld	$⊢ (φ \land n \in (ℕ repr (3) N)) \to Λ (n (0)) H (n (0)) Λ (n (1)) K (n (1)) Λ (n (2)) K (n (2)) \in ℝ$
60	18 59	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 ℝ$
61	16 60	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 ℝ$
62		0nn0	$⊢ 0 \in ℕ_{0}$
63		qssre	$⊢ ℚ \subseteq ℝ$
64		4nn0	$⊢ 4 \in ℕ_{0}$
65		2nn0	$⊢ 2 \in ℕ_{0}$
66		nn0ssq	$⊢ ℕ_{0} \subseteq ℚ$
67		8nn0	$⊢ 8 \in ℕ_{0}$
68	66 67	sselii	$⊢ 8 \in ℚ$
69	64 68	dp2clq	$⊢ 48 \in ℚ$
70	65 69	dp2clq	$⊢ 248 \in ℚ$
71	65 70	dp2clq	$⊢ 2248 \in ℚ$
72	64 71	dp2clq	$⊢ 42248 \in ℚ$
73	62 72	dp2clq	$⊢ 042248 \in ℚ$
74	62 73	dp2clq	$⊢ 0042248 \in ℚ$
75	62 74	dp2clq	$⊢ 00042248 \in ℚ$
76	63 75	sselii	$⊢ 00042248 \in ℝ$
77		dpcl	$⊢ (0 \in ℕ_{0} \land 00042248 \in ℝ) \to 0.00042248 \in ℝ$
78	62 76 77	mp2an	$⊢ 0.00042248 \in ℝ$
79	78	a1i	$⊢ φ \to 0.00042248 \in ℝ$
80	9	nnred	$⊢ φ \to N \in ℝ$
81	80	resqcld	$⊢ φ \to N^{2} \in ℝ$
82	79 81	remulcld	$⊢ φ \to 0.00042248 N^{2} \in ℝ$
83	14 59	fsumrecl	$⊢ φ \to \sum_{n \in ℕ repr (3) N} Λ (n (0)) H (n (0)) Λ (n (1)) K (n (1)) Λ (n (2)) K (n (2)) \in ℝ$
84		7nn0	$⊢ 7 \in ℕ_{0}$
85	11 69	dp2clq	$⊢ 348 \in ℚ$
86	63 85	sselii	$⊢ 348 \in ℝ$
87		dpcl	$⊢ (7 \in ℕ_{0} \land 348 \in ℝ) \to 7.348 \in ℝ$
88	84 86 87	mp2an	$⊢ 7.348 \in ℝ$
89	88	a1i	$⊢ φ \to 7.348 \in ℝ$
90	9	nnrpd	$⊢ φ \to N \in ℝ^{+}$
91	90	relogcld	$⊢ φ \to \log N \in ℝ$
92	10	nn0ge0d	$⊢ φ \to 0 \leq N$
93	80 92	resqrtcld	$⊢ φ \to \sqrt{N} \in ℝ$
94	90	sqrtgt0d	$⊢ φ \to 0 < \sqrt{N}$
95	94	gt0ne0d	$⊢ φ \to \sqrt{N} \neq 0$
96	91 93 95	redivcld	$⊢ φ \to \frac{\log N}{\sqrt{N}} \in ℝ$
97	89 96	remulcld	$⊢ φ \to 7.348 (\frac{\log N}{\sqrt{N}}) \in ℝ$
98	97 81	remulcld	$⊢ φ \to 7.348 (\frac{\log N}{\sqrt{N}}) N^{2} \in ℝ$
99	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}$
100		2z	$⊢ 2 \in ℤ$
101	100	a1i	$⊢ φ \to 2 \in ℤ$
102	90 101	rpexpcld	$⊢ φ \to N^{2} \in ℝ^{+}$
103		hgt750lem	$⊢ (N \in ℕ_{0} \land 10^{27} \leq N) \to 7.348 (\frac{\log N}{\sqrt{N}}) < 0.00042248$
104	10 3 103	syl2anc	$⊢ φ \to 7.348 (\frac{\log N}{\sqrt{N}}) < 0.00042248$
105	97 79 102 104	ltmul1dd	$⊢ φ \to 7.348 (\frac{\log N}{\sqrt{N}}) N^{2} < 0.00042248 N^{2}$
106	61 98 82 99 105	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}$
107	36 46 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$
108	8 107	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))$
109	61 82 83 106 108	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))$
110	61 83	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)))$
111	109 110	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))$
112		inss2	$⊢ O \cap ℙ \subseteq ℙ$
113		prmssnn	$⊢ ℙ \subseteq ℕ$
114	112 113	sstri	$⊢ O \cap ℙ \subseteq ℕ$
115	114	a1i	$⊢ φ \to O \cap ℙ \subseteq ℕ$
116	13 22 12 115	reprss	$⊢ φ \to (O \cap ℙ) repr (3) N \subseteq ℕ repr (3) N$
117	14 116	ssfid	$⊢ φ \to (O \cap ℙ) repr (3) N \in Fin$
118	116	sselda	$⊢ (φ \land n \in ((O \cap ℙ) repr (3) N)) \to n \in (ℕ repr (3) N)$
119	59	recnd	$⊢ (φ \land n \in (ℕ repr (3) N)) \to Λ (n (0)) H (n (0)) Λ (n (1)) K (n (1)) Λ (n (2)) K (n (2)) \in ℂ$
120	118 119	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 ℂ$
121	117 120	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 ℂ$
122	61	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 ℂ$
123		disjdif	$⊢ ((O \cap ℙ) repr (3) N) \cap ((ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N)) = \emptyset$
124	123	a1i	$⊢ φ \to ((O \cap ℙ) repr (3) N) \cap ((ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N)) = \emptyset$
125		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$
126	116 125	sylib	$⊢ φ \to ((O \cap ℙ) repr (3) N) \cup ((ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N)) = ℕ repr (3) N$
127	126	eqcomd	$⊢ φ \to ℕ repr (3) N = ((O \cap ℙ) repr (3) N) \cup ((ℕ repr (3) N) ∖ ((O \cap ℙ) repr (3) N))$
128	124 127 14 119	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))$
129	121 122 128	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))$
130	111 129	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