Metamath Proof Explorer


Theorem tgoldbachgtda

Description: Lemma for tgoldbachgtd . (Contributed by Thierry Arnoux, 15-Dec-2021)

Ref Expression
Hypotheses tgoldbachgtda.o O = z | ¬ 2 z
tgoldbachgtda.n φ N O
tgoldbachgtda.0 φ 10 27 N
tgoldbachgtda.h φ H : 0 +∞
tgoldbachgtda.k φ K : 0 +∞
tgoldbachgtda.1 φ m K m 1.079955
tgoldbachgtda.2 φ m H m 1.414
tgoldbachgtda.3 φ 0.00042248 N 2 0 1 Λ × f H vts N x Λ × f K vts N x 2 e i 2 π -N x dx
Assertion tgoldbachgtda φ 0 < O repr 3 N

Proof

Step Hyp Ref Expression
1 tgoldbachgtda.o O = z | ¬ 2 z
2 tgoldbachgtda.n φ N O
3 tgoldbachgtda.0 φ 10 27 N
4 tgoldbachgtda.h φ H : 0 +∞
5 tgoldbachgtda.k φ K : 0 +∞
6 tgoldbachgtda.1 φ m K m 1.079955
7 tgoldbachgtda.2 φ m H m 1.414
8 tgoldbachgtda.3 φ 0.00042248 N 2 0 1 Λ × f H vts N x Λ × f K vts N x 2 e i 2 π -N x dx
9 1 2 3 tgoldbachgnn φ N
10 9 nnnn0d φ N 0
11 3nn0 3 0
12 11 a1i φ 3 0
13 inss2 O
14 prmssnn
15 13 14 sstri O
16 15 a1i φ O
17 10 12 16 reprfi2 φ O repr 3 N Fin
18 1 2 3 4 5 6 7 8 tgoldbachgtde φ 0 < n O repr 3 N Λ n 0 H n 0 Λ n 1 K n 1 Λ n 2 K n 2
19 18 gt0ne0d φ n O repr 3 N Λ n 0 H n 0 Λ n 1 K n 1 Λ n 2 K n 2 0
20 19 neneqd φ ¬ n O repr 3 N Λ n 0 H n 0 Λ n 1 K n 1 Λ n 2 K n 2 = 0
21 simpr φ O repr 3 N = O repr 3 N =
22 21 sumeq1d φ O repr 3 N = n O repr 3 N Λ n 0 H n 0 Λ n 1 K n 1 Λ n 2 K n 2 = n Λ n 0 H n 0 Λ n 1 K n 1 Λ n 2 K n 2
23 sum0 n Λ n 0 H n 0 Λ n 1 K n 1 Λ n 2 K n 2 = 0
24 22 23 eqtrdi φ O repr 3 N = n O repr 3 N Λ n 0 H n 0 Λ n 1 K n 1 Λ n 2 K n 2 = 0
25 20 24 mtand φ ¬ O repr 3 N =
26 25 neqned φ O repr 3 N
27 hashnncl O repr 3 N Fin O repr 3 N O repr 3 N
28 27 biimpar O repr 3 N Fin O repr 3 N O repr 3 N
29 17 26 28 syl2anc φ O repr 3 N
30 nngt0 O repr 3 N 0 < O repr 3 N
31 29 30 syl φ 0 < O repr 3 N