Metamath Proof Explorer

Theorem bgoldbachlt

Description: The binary Goldbach conjecture is valid for small even numbers (i.e. for all even numbers less than or equal to a fixed big m ). This is verified for m = 4 x 10^18 by Oliveira e Silva, see ax-bgbltosilva . (Contributed by AV, 3-Aug-2020) (Revised by AV, 9-Sep-2021)

Ref Expression
Assertion bgoldbachlt 
|- E. m e. NN ( ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) <_ m /\ A. n e. Even ( ( 4 < n /\ n < m ) -> n e. GoldbachEven ) )

Proof

Step Hyp Ref Expression
1 4nn 
 |-  4 e. NN
2 10nn 
 |-  ; 1 0 e. NN
3 1nn0 
 |-  1 e. NN0
4 8nn0 
 |-  8 e. NN0
5 3 4 deccl 
 |-  ; 1 8 e. NN0
6 nnexpcl 
 |-  ( ( ; 1 0 e. NN /\ ; 1 8 e. NN0 ) -> ( ; 1 0 ^ ; 1 8 ) e. NN )
7 2 5 6 mp2an 
 |-  ( ; 1 0 ^ ; 1 8 ) e. NN
8 1 7 nnmulcli 
 |-  ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) e. NN
9 id 
 |-  ( ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) e. NN -> ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) e. NN )
10 breq2 
 |-  ( m = ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) -> ( ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) <_ m <-> ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) <_ ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) ) )
11 breq2 
 |-  ( m = ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) -> ( n < m <-> n < ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) ) )
12 11 anbi2d 
 |-  ( m = ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) -> ( ( 4 < n /\ n < m ) <-> ( 4 < n /\ n < ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) ) ) )
13 12 imbi1d 
 |-  ( m = ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) -> ( ( ( 4 < n /\ n < m ) -> n e. GoldbachEven ) <-> ( ( 4 < n /\ n < ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) ) -> n e. GoldbachEven ) ) )
14 13 ralbidv 
 |-  ( m = ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) -> ( A. n e. Even ( ( 4 < n /\ n < m ) -> n e. GoldbachEven ) <-> A. n e. Even ( ( 4 < n /\ n < ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) ) -> n e. GoldbachEven ) ) )
15 10 14 anbi12d 
 |-  ( m = ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) -> ( ( ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) <_ m /\ A. n e. Even ( ( 4 < n /\ n < m ) -> n e. GoldbachEven ) ) <-> ( ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) <_ ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) /\ A. n e. Even ( ( 4 < n /\ n < ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) ) -> n e. GoldbachEven ) ) ) )
16 15 adantl 
 |-  ( ( ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) e. NN /\ m = ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) ) -> ( ( ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) <_ m /\ A. n e. Even ( ( 4 < n /\ n < m ) -> n e. GoldbachEven ) ) <-> ( ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) <_ ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) /\ A. n e. Even ( ( 4 < n /\ n < ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) ) -> n e. GoldbachEven ) ) ) )
17 nnre 
 |-  ( ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) e. NN -> ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) e. RR )
18 17 leidd 
 |-  ( ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) e. NN -> ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) <_ ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) )
19 simplr 
 |-  ( ( ( ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) e. NN /\ n e. Even ) /\ ( 4 < n /\ n < ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) ) ) -> n e. Even )
20 simprl 
 |-  ( ( ( ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) e. NN /\ n e. Even ) /\ ( 4 < n /\ n < ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) ) ) -> 4 < n )
21 evenz 
 |-  ( n e. Even -> n e. ZZ )
22 21 zred 
 |-  ( n e. Even -> n e. RR )
23 ltle 
 |-  ( ( n e. RR /\ ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) e. RR ) -> ( n < ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) -> n <_ ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) ) )
24 22 17 23 syl2anr 
 |-  ( ( ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) e. NN /\ n e. Even ) -> ( n < ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) -> n <_ ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) ) )
25 24 a1d 
 |-  ( ( ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) e. NN /\ n e. Even ) -> ( 4 < n -> ( n < ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) -> n <_ ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) ) ) )
26 25 imp32 
 |-  ( ( ( ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) e. NN /\ n e. Even ) /\ ( 4 < n /\ n < ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) ) ) -> n <_ ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) )
27 ax-bgbltosilva 
 |-  ( ( n e. Even /\ 4 < n /\ n <_ ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) ) -> n e. GoldbachEven )
28 19 20 26 27 syl3anc 
 |-  ( ( ( ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) e. NN /\ n e. Even ) /\ ( 4 < n /\ n < ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) ) ) -> n e. GoldbachEven )
29 28 ex 
 |-  ( ( ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) e. NN /\ n e. Even ) -> ( ( 4 < n /\ n < ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) ) -> n e. GoldbachEven ) )
30 29 ralrimiva 
 |-  ( ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) e. NN -> A. n e. Even ( ( 4 < n /\ n < ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) ) -> n e. GoldbachEven ) )
31 18 30 jca 
 |-  ( ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) e. NN -> ( ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) <_ ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) /\ A. n e. Even ( ( 4 < n /\ n < ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) ) -> n e. GoldbachEven ) ) )
32 9 16 31 rspcedvd 
 |-  ( ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) e. NN -> E. m e. NN ( ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) <_ m /\ A. n e. Even ( ( 4 < n /\ n < m ) -> n e. GoldbachEven ) ) )
33 8 32 ax-mp 
 |-  E. m e. NN ( ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) <_ m /\ A. n e. Even ( ( 4 < n /\ n < m ) -> n e. GoldbachEven ) )