Metamath Proof Explorer


Theorem tgoldbachgtd

Description: Odd integers greater than ( ; 1 0 ^ ; 2 7 ) have at least a representation as a sum of three odd primes. Final statement in section 7.4 of Helfgott p. 70. (Contributed by Thierry Arnoux, 15-Dec-2021)

Ref Expression
Hypotheses tgoldbachgtd.o O = z | ¬ 2 z
tgoldbachgtd.n φ N O
tgoldbachgtd.1 φ 10 27 N
Assertion tgoldbachgtd φ 0 < O repr 3 N

Proof

Step Hyp Ref Expression
1 tgoldbachgtd.o O = z | ¬ 2 z
2 tgoldbachgtd.n φ N O
3 tgoldbachgtd.1 φ 10 27 N
4 2 ad3antrrr φ h 0 +∞ k 0 +∞ m k m 1.079955 m h m 1.414 0.00042248 N 2 0 1 Λ × f h vts N x Λ × f k vts N x 2 e i 2 π -N x dx N O
5 3 ad3antrrr φ h 0 +∞ k 0 +∞ m k m 1.079955 m h m 1.414 0.00042248 N 2 0 1 Λ × f h vts N x Λ × f k vts N x 2 e i 2 π -N x dx 10 27 N
6 elmapi h 0 +∞ h : 0 +∞
7 6 ad3antlr φ h 0 +∞ k 0 +∞ m k m 1.079955 m h m 1.414 0.00042248 N 2 0 1 Λ × f h vts N x Λ × f k vts N x 2 e i 2 π -N x dx h : 0 +∞
8 elmapi k 0 +∞ k : 0 +∞
9 8 ad2antlr φ h 0 +∞ k 0 +∞ m k m 1.079955 m h m 1.414 0.00042248 N 2 0 1 Λ × f h vts N x Λ × f k vts N x 2 e i 2 π -N x dx k : 0 +∞
10 simpr1 φ h 0 +∞ k 0 +∞ m k m 1.079955 m h m 1.414 0.00042248 N 2 0 1 Λ × f h vts N x Λ × f k vts N x 2 e i 2 π -N x dx m k m 1.079955
11 fveq2 m = n k m = k n
12 11 breq1d m = n k m 1.079955 k n 1.079955
13 12 cbvralvw m k m 1.079955 n k n 1.079955
14 10 13 sylib φ h 0 +∞ k 0 +∞ m k m 1.079955 m h m 1.414 0.00042248 N 2 0 1 Λ × f h vts N x Λ × f k vts N x 2 e i 2 π -N x dx n k n 1.079955
15 14 r19.21bi φ h 0 +∞ k 0 +∞ m k m 1.079955 m h m 1.414 0.00042248 N 2 0 1 Λ × f h vts N x Λ × f k vts N x 2 e i 2 π -N x dx n k n 1.079955
16 simpr2 φ h 0 +∞ k 0 +∞ m k m 1.079955 m h m 1.414 0.00042248 N 2 0 1 Λ × f h vts N x Λ × f k vts N x 2 e i 2 π -N x dx m h m 1.414
17 fveq2 m = n h m = h n
18 17 breq1d m = n h m 1.414 h n 1.414
19 18 cbvralvw m h m 1.414 n h n 1.414
20 16 19 sylib φ h 0 +∞ k 0 +∞ m k m 1.079955 m h m 1.414 0.00042248 N 2 0 1 Λ × f h vts N x Λ × f k vts N x 2 e i 2 π -N x dx n h n 1.414
21 20 r19.21bi φ h 0 +∞ k 0 +∞ m k m 1.079955 m h m 1.414 0.00042248 N 2 0 1 Λ × f h vts N x Λ × f k vts N x 2 e i 2 π -N x dx n h n 1.414
22 simpr3 φ h 0 +∞ k 0 +∞ m k m 1.079955 m h m 1.414 0.00042248 N 2 0 1 Λ × f h vts N x Λ × f k vts N x 2 e i 2 π -N x dx 0.00042248 N 2 0 1 Λ × f h vts N x Λ × f k vts N x 2 e i 2 π -N x dx
23 fveq2 x = y Λ × f h vts N x = Λ × f h vts N y
24 fveq2 x = y Λ × f k vts N x = Λ × f k vts N y
25 24 oveq1d x = y Λ × f k vts N x 2 = Λ × f k vts N y 2
26 23 25 oveq12d x = y Λ × f h vts N x Λ × f k vts N x 2 = Λ × f h vts N y Λ × f k vts N y 2
27 oveq2 x = y -N x = -N y
28 27 oveq2d x = y i 2 π -N x = i 2 π -N y
29 28 fveq2d x = y e i 2 π -N x = e i 2 π -N y
30 26 29 oveq12d x = y Λ × f h vts N x Λ × f k vts N x 2 e i 2 π -N x = Λ × f h vts N y Λ × f k vts N y 2 e i 2 π -N y
31 30 cbvitgv 0 1 Λ × f h vts N x Λ × f k vts N x 2 e i 2 π -N x dx = 0 1 Λ × f h vts N y Λ × f k vts N y 2 e i 2 π -N y dy
32 22 31 breqtrdi φ h 0 +∞ k 0 +∞ m k m 1.079955 m h m 1.414 0.00042248 N 2 0 1 Λ × f h vts N x Λ × f k vts N x 2 e i 2 π -N x dx 0.00042248 N 2 0 1 Λ × f h vts N y Λ × f k vts N y 2 e i 2 π -N y dy
33 1 4 5 7 9 15 21 32 tgoldbachgtda φ h 0 +∞ k 0 +∞ m k m 1.079955 m h m 1.414 0.00042248 N 2 0 1 Λ × f h vts N x Λ × f k vts N x 2 e i 2 π -N x dx 0 < O repr 3 N
34 1 2 3 hgt749d φ h 0 +∞ k 0 +∞ m k m 1.079955 m h m 1.414 0.00042248 N 2 0 1 Λ × f h vts N x Λ × f k vts N x 2 e i 2 π -N x dx
35 33 34 r19.29vva φ 0 < O repr 3 N