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 ) ) ) |