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 e. ZZ | -. 2 || z }
tgoldbachgtd.n 
|- ( ph -> N e. O )
tgoldbachgtd.1 
|- ( ph -> ( ; 1 0 ^ ; 2 7 ) <_ N )
Assertion tgoldbachgtd 
|- ( ph -> 0 < ( # ` ( ( O i^i Prime ) ( repr ` 3 ) N ) ) )

Proof

Step Hyp Ref Expression
1 tgoldbachgtd.o 
 |-  O = { z e. ZZ | -. 2 || z }
2 tgoldbachgtd.n 
 |-  ( ph -> N e. O )
3 tgoldbachgtd.1 
 |-  ( ph -> ( ; 1 0 ^ ; 2 7 ) <_ N )
4 2 ad3antrrr 
 |-  ( ( ( ( ph /\ h e. ( ( 0 [,) +oo ) ^m NN ) ) /\ k e. ( ( 0 [,) +oo ) ^m NN ) ) /\ ( A. m e. NN ( k ` m ) <_ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) /\ A. m e. NN ( h ` m ) <_ ( 1 . _ 4 _ 1 4 ) /\ ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( N ^ 2 ) ) <_ S. ( 0 (,) 1 ) ( ( ( ( ( Lam oF x. h ) vts N ) ` x ) x. ( ( ( ( Lam oF x. k ) vts N ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) _d x ) ) -> N e. O )
5 3 ad3antrrr 
 |-  ( ( ( ( ph /\ h e. ( ( 0 [,) +oo ) ^m NN ) ) /\ k e. ( ( 0 [,) +oo ) ^m NN ) ) /\ ( A. m e. NN ( k ` m ) <_ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) /\ A. m e. NN ( h ` m ) <_ ( 1 . _ 4 _ 1 4 ) /\ ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( N ^ 2 ) ) <_ S. ( 0 (,) 1 ) ( ( ( ( ( Lam oF x. h ) vts N ) ` x ) x. ( ( ( ( Lam oF x. k ) vts N ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) _d x ) ) -> ( ; 1 0 ^ ; 2 7 ) <_ N )
6 elmapi 
 |-  ( h e. ( ( 0 [,) +oo ) ^m NN ) -> h : NN --> ( 0 [,) +oo ) )
7 6 ad3antlr 
 |-  ( ( ( ( ph /\ h e. ( ( 0 [,) +oo ) ^m NN ) ) /\ k e. ( ( 0 [,) +oo ) ^m NN ) ) /\ ( A. m e. NN ( k ` m ) <_ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) /\ A. m e. NN ( h ` m ) <_ ( 1 . _ 4 _ 1 4 ) /\ ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( N ^ 2 ) ) <_ S. ( 0 (,) 1 ) ( ( ( ( ( Lam oF x. h ) vts N ) ` x ) x. ( ( ( ( Lam oF x. k ) vts N ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) _d x ) ) -> h : NN --> ( 0 [,) +oo ) )
8 elmapi 
 |-  ( k e. ( ( 0 [,) +oo ) ^m NN ) -> k : NN --> ( 0 [,) +oo ) )
9 8 ad2antlr 
 |-  ( ( ( ( ph /\ h e. ( ( 0 [,) +oo ) ^m NN ) ) /\ k e. ( ( 0 [,) +oo ) ^m NN ) ) /\ ( A. m e. NN ( k ` m ) <_ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) /\ A. m e. NN ( h ` m ) <_ ( 1 . _ 4 _ 1 4 ) /\ ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( N ^ 2 ) ) <_ S. ( 0 (,) 1 ) ( ( ( ( ( Lam oF x. h ) vts N ) ` x ) x. ( ( ( ( Lam oF x. k ) vts N ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) _d x ) ) -> k : NN --> ( 0 [,) +oo ) )
10 simpr1 
 |-  ( ( ( ( ph /\ h e. ( ( 0 [,) +oo ) ^m NN ) ) /\ k e. ( ( 0 [,) +oo ) ^m NN ) ) /\ ( A. m e. NN ( k ` m ) <_ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) /\ A. m e. NN ( h ` m ) <_ ( 1 . _ 4 _ 1 4 ) /\ ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( N ^ 2 ) ) <_ S. ( 0 (,) 1 ) ( ( ( ( ( Lam oF x. h ) vts N ) ` x ) x. ( ( ( ( Lam oF x. k ) vts N ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) _d x ) ) -> A. m e. NN ( k ` m ) <_ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) )
11 fveq2 
 |-  ( m = n -> ( k ` m ) = ( k ` n ) )
12 11 breq1d 
 |-  ( m = n -> ( ( k ` m ) <_ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) <-> ( k ` n ) <_ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ) )
13 12 cbvralvw 
 |-  ( A. m e. NN ( k ` m ) <_ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) <-> A. n e. NN ( k ` n ) <_ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) )
14 10 13 sylib 
 |-  ( ( ( ( ph /\ h e. ( ( 0 [,) +oo ) ^m NN ) ) /\ k e. ( ( 0 [,) +oo ) ^m NN ) ) /\ ( A. m e. NN ( k ` m ) <_ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) /\ A. m e. NN ( h ` m ) <_ ( 1 . _ 4 _ 1 4 ) /\ ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( N ^ 2 ) ) <_ S. ( 0 (,) 1 ) ( ( ( ( ( Lam oF x. h ) vts N ) ` x ) x. ( ( ( ( Lam oF x. k ) vts N ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) _d x ) ) -> A. n e. NN ( k ` n ) <_ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) )
15 14 r19.21bi 
 |-  ( ( ( ( ( ph /\ h e. ( ( 0 [,) +oo ) ^m NN ) ) /\ k e. ( ( 0 [,) +oo ) ^m NN ) ) /\ ( A. m e. NN ( k ` m ) <_ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) /\ A. m e. NN ( h ` m ) <_ ( 1 . _ 4 _ 1 4 ) /\ ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( N ^ 2 ) ) <_ S. ( 0 (,) 1 ) ( ( ( ( ( Lam oF x. h ) vts N ) ` x ) x. ( ( ( ( Lam oF x. k ) vts N ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) _d x ) ) /\ n e. NN ) -> ( k ` n ) <_ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) )
16 simpr2 
 |-  ( ( ( ( ph /\ h e. ( ( 0 [,) +oo ) ^m NN ) ) /\ k e. ( ( 0 [,) +oo ) ^m NN ) ) /\ ( A. m e. NN ( k ` m ) <_ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) /\ A. m e. NN ( h ` m ) <_ ( 1 . _ 4 _ 1 4 ) /\ ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( N ^ 2 ) ) <_ S. ( 0 (,) 1 ) ( ( ( ( ( Lam oF x. h ) vts N ) ` x ) x. ( ( ( ( Lam oF x. k ) vts N ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) _d x ) ) -> A. m e. NN ( h ` m ) <_ ( 1 . _ 4 _ 1 4 ) )
17 fveq2 
 |-  ( m = n -> ( h ` m ) = ( h ` n ) )
18 17 breq1d 
 |-  ( m = n -> ( ( h ` m ) <_ ( 1 . _ 4 _ 1 4 ) <-> ( h ` n ) <_ ( 1 . _ 4 _ 1 4 ) ) )
19 18 cbvralvw 
 |-  ( A. m e. NN ( h ` m ) <_ ( 1 . _ 4 _ 1 4 ) <-> A. n e. NN ( h ` n ) <_ ( 1 . _ 4 _ 1 4 ) )
20 16 19 sylib 
 |-  ( ( ( ( ph /\ h e. ( ( 0 [,) +oo ) ^m NN ) ) /\ k e. ( ( 0 [,) +oo ) ^m NN ) ) /\ ( A. m e. NN ( k ` m ) <_ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) /\ A. m e. NN ( h ` m ) <_ ( 1 . _ 4 _ 1 4 ) /\ ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( N ^ 2 ) ) <_ S. ( 0 (,) 1 ) ( ( ( ( ( Lam oF x. h ) vts N ) ` x ) x. ( ( ( ( Lam oF x. k ) vts N ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) _d x ) ) -> A. n e. NN ( h ` n ) <_ ( 1 . _ 4 _ 1 4 ) )
21 20 r19.21bi 
 |-  ( ( ( ( ( ph /\ h e. ( ( 0 [,) +oo ) ^m NN ) ) /\ k e. ( ( 0 [,) +oo ) ^m NN ) ) /\ ( A. m e. NN ( k ` m ) <_ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) /\ A. m e. NN ( h ` m ) <_ ( 1 . _ 4 _ 1 4 ) /\ ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( N ^ 2 ) ) <_ S. ( 0 (,) 1 ) ( ( ( ( ( Lam oF x. h ) vts N ) ` x ) x. ( ( ( ( Lam oF x. k ) vts N ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) _d x ) ) /\ n e. NN ) -> ( h ` n ) <_ ( 1 . _ 4 _ 1 4 ) )
22 simpr3 
 |-  ( ( ( ( ph /\ h e. ( ( 0 [,) +oo ) ^m NN ) ) /\ k e. ( ( 0 [,) +oo ) ^m NN ) ) /\ ( A. m e. NN ( k ` m ) <_ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) /\ A. m e. NN ( h ` m ) <_ ( 1 . _ 4 _ 1 4 ) /\ ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( N ^ 2 ) ) <_ S. ( 0 (,) 1 ) ( ( ( ( ( Lam oF x. h ) vts N ) ` x ) x. ( ( ( ( Lam oF x. k ) vts N ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) _d x ) ) -> ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( N ^ 2 ) ) <_ S. ( 0 (,) 1 ) ( ( ( ( ( Lam oF x. h ) vts N ) ` x ) x. ( ( ( ( Lam oF x. k ) vts N ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) _d x )
23 fveq2 
 |-  ( x = y -> ( ( ( Lam oF x. h ) vts N ) ` x ) = ( ( ( Lam oF x. h ) vts N ) ` y ) )
24 fveq2 
 |-  ( x = y -> ( ( ( Lam oF x. k ) vts N ) ` x ) = ( ( ( Lam oF x. k ) vts N ) ` y ) )
25 24 oveq1d 
 |-  ( x = y -> ( ( ( ( Lam oF x. k ) vts N ) ` x ) ^ 2 ) = ( ( ( ( Lam oF x. k ) vts N ) ` y ) ^ 2 ) )
26 23 25 oveq12d 
 |-  ( x = y -> ( ( ( ( Lam oF x. h ) vts N ) ` x ) x. ( ( ( ( Lam oF x. k ) vts N ) ` x ) ^ 2 ) ) = ( ( ( ( Lam oF x. h ) vts N ) ` y ) x. ( ( ( ( Lam oF x. k ) vts N ) ` y ) ^ 2 ) ) )
27 oveq2 
 |-  ( x = y -> ( -u N x. x ) = ( -u N x. y ) )
28 27 oveq2d 
 |-  ( x = y -> ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) = ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. y ) ) )
29 28 fveq2d 
 |-  ( x = y -> ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) = ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. y ) ) ) )
30 26 29 oveq12d 
 |-  ( x = y -> ( ( ( ( ( Lam oF x. h ) vts N ) ` x ) x. ( ( ( ( Lam oF x. k ) vts N ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) = ( ( ( ( ( Lam oF x. h ) vts N ) ` y ) x. ( ( ( ( Lam oF x. k ) vts N ) ` y ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. y ) ) ) ) )
31 30 cbvitgv 
 |-  S. ( 0 (,) 1 ) ( ( ( ( ( Lam oF x. h ) vts N ) ` x ) x. ( ( ( ( Lam oF x. k ) vts N ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) _d x = S. ( 0 (,) 1 ) ( ( ( ( ( Lam oF x. h ) vts N ) ` y ) x. ( ( ( ( Lam oF x. k ) vts N ) ` y ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. y ) ) ) ) _d y
32 22 31 breqtrdi 
 |-  ( ( ( ( ph /\ h e. ( ( 0 [,) +oo ) ^m NN ) ) /\ k e. ( ( 0 [,) +oo ) ^m NN ) ) /\ ( A. m e. NN ( k ` m ) <_ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) /\ A. m e. NN ( h ` m ) <_ ( 1 . _ 4 _ 1 4 ) /\ ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( N ^ 2 ) ) <_ S. ( 0 (,) 1 ) ( ( ( ( ( Lam oF x. h ) vts N ) ` x ) x. ( ( ( ( Lam oF x. k ) vts N ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) _d x ) ) -> ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( N ^ 2 ) ) <_ S. ( 0 (,) 1 ) ( ( ( ( ( Lam oF x. h ) vts N ) ` y ) x. ( ( ( ( Lam oF x. k ) vts N ) ` y ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. y ) ) ) ) _d y )
33 1 4 5 7 9 15 21 32 tgoldbachgtda 
 |-  ( ( ( ( ph /\ h e. ( ( 0 [,) +oo ) ^m NN ) ) /\ k e. ( ( 0 [,) +oo ) ^m NN ) ) /\ ( A. m e. NN ( k ` m ) <_ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) /\ A. m e. NN ( h ` m ) <_ ( 1 . _ 4 _ 1 4 ) /\ ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( N ^ 2 ) ) <_ S. ( 0 (,) 1 ) ( ( ( ( ( Lam oF x. h ) vts N ) ` x ) x. ( ( ( ( Lam oF x. k ) vts N ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) _d x ) ) -> 0 < ( # ` ( ( O i^i Prime ) ( repr ` 3 ) N ) ) )
34 1 2 3 hgt749d 
 |-  ( ph -> E. h e. ( ( 0 [,) +oo ) ^m NN ) E. k e. ( ( 0 [,) +oo ) ^m NN ) ( A. m e. NN ( k ` m ) <_ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) /\ A. m e. NN ( h ` m ) <_ ( 1 . _ 4 _ 1 4 ) /\ ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( N ^ 2 ) ) <_ S. ( 0 (,) 1 ) ( ( ( ( ( Lam oF x. h ) vts N ) ` x ) x. ( ( ( ( Lam oF x. k ) vts N ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) _d x ) )
35 33 34 r19.29vva 
 |-  ( ph -> 0 < ( # ` ( ( O i^i Prime ) ( repr ` 3 ) N ) ) )