Metamath Proof Explorer

Theorem tgoldbachlt

Description: The ternary Goldbach conjecture is valid for small odd numbers (i.e. for all odd numbers less than a fixed big m greater than 8 x 10^30). This is verified for m = 8.875694 x 10^30 by Helfgott, see tgblthelfgott . (Contributed by AV, 4-Aug-2020) (Revised by AV, 9-Sep-2021)

Ref Expression
Assertion tgoldbachlt 
|- E. m e. NN ( ( 8 x. ( ; 1 0 ^ ; 3 0 ) ) < m /\ A. n e. Odd ( ( 7 < n /\ n < m ) -> n e. GoldbachOdd ) )

Proof

Step Hyp Ref Expression
1 8nn0 
 |-  8 e. NN0
2 8nn 
 |-  8 e. NN
3 1 2 decnncl 
 |-  ; 8 8 e. NN
4 10nn 
 |-  ; 1 0 e. NN
5 2nn0 
 |-  2 e. NN0
6 9nn0 
 |-  9 e. NN0
7 5 6 deccl 
 |-  ; 2 9 e. NN0
8 nnexpcl 
 |-  ( ( ; 1 0 e. NN /\ ; 2 9 e. NN0 ) -> ( ; 1 0 ^ ; 2 9 ) e. NN )
9 4 7 8 mp2an 
 |-  ( ; 1 0 ^ ; 2 9 ) e. NN
10 3 9 nnmulcli 
 |-  ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) e. NN
11 id 
 |-  ( ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) e. NN -> ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) e. NN )
12 breq2 
 |-  ( m = ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) -> ( ( 8 x. ( ; 1 0 ^ ; 3 0 ) ) < m <-> ( 8 x. ( ; 1 0 ^ ; 3 0 ) ) < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) ) )
13 breq2 
 |-  ( m = ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) -> ( n < m <-> n < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) ) )
14 13 anbi2d 
 |-  ( m = ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) -> ( ( 7 < n /\ n < m ) <-> ( 7 < n /\ n < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) ) ) )
15 14 imbi1d 
 |-  ( m = ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) -> ( ( ( 7 < n /\ n < m ) -> n e. GoldbachOdd ) <-> ( ( 7 < n /\ n < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) ) -> n e. GoldbachOdd ) ) )
16 15 ralbidv 
 |-  ( m = ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) -> ( A. n e. Odd ( ( 7 < n /\ n < m ) -> n e. GoldbachOdd ) <-> A. n e. Odd ( ( 7 < n /\ n < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) ) -> n e. GoldbachOdd ) ) )
17 12 16 anbi12d 
 |-  ( m = ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) -> ( ( ( 8 x. ( ; 1 0 ^ ; 3 0 ) ) < m /\ A. n e. Odd ( ( 7 < n /\ n < m ) -> n e. GoldbachOdd ) ) <-> ( ( 8 x. ( ; 1 0 ^ ; 3 0 ) ) < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) /\ A. n e. Odd ( ( 7 < n /\ n < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) ) -> n e. GoldbachOdd ) ) ) )
18 17 adantl 
 |-  ( ( ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) e. NN /\ m = ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) ) -> ( ( ( 8 x. ( ; 1 0 ^ ; 3 0 ) ) < m /\ A. n e. Odd ( ( 7 < n /\ n < m ) -> n e. GoldbachOdd ) ) <-> ( ( 8 x. ( ; 1 0 ^ ; 3 0 ) ) < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) /\ A. n e. Odd ( ( 7 < n /\ n < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) ) -> n e. GoldbachOdd ) ) ) )
19 simplr 
 |-  ( ( ( ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) e. NN /\ n e. Odd ) /\ ( 7 < n /\ n < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) ) ) -> n e. Odd )
20 simprl 
 |-  ( ( ( ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) e. NN /\ n e. Odd ) /\ ( 7 < n /\ n < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) ) ) -> 7 < n )
21 simprr 
 |-  ( ( ( ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) e. NN /\ n e. Odd ) /\ ( 7 < n /\ n < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) ) ) -> n < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) )
22 tgblthelfgott 
 |-  ( ( n e. Odd /\ 7 < n /\ n < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) ) -> n e. GoldbachOdd )
23 19 20 21 22 syl3anc 
 |-  ( ( ( ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) e. NN /\ n e. Odd ) /\ ( 7 < n /\ n < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) ) ) -> n e. GoldbachOdd )
24 23 ex 
 |-  ( ( ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) e. NN /\ n e. Odd ) -> ( ( 7 < n /\ n < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) ) -> n e. GoldbachOdd ) )
25 24 ralrimiva 
 |-  ( ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) e. NN -> A. n e. Odd ( ( 7 < n /\ n < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) ) -> n e. GoldbachOdd ) )
26 2 9 nnmulcli 
 |-  ( 8 x. ( ; 1 0 ^ ; 2 9 ) ) e. NN
27 26 nngt0i 
 |-  0 < ( 8 x. ( ; 1 0 ^ ; 2 9 ) )
28 26 nnrei 
 |-  ( 8 x. ( ; 1 0 ^ ; 2 9 ) ) e. RR
29 3nn0 
 |-  3 e. NN0
30 0nn0 
 |-  0 e. NN0
31 29 30 deccl 
 |-  ; 3 0 e. NN0
32 nnexpcl 
 |-  ( ( ; 1 0 e. NN /\ ; 3 0 e. NN0 ) -> ( ; 1 0 ^ ; 3 0 ) e. NN )
33 4 31 32 mp2an 
 |-  ( ; 1 0 ^ ; 3 0 ) e. NN
34 2 33 nnmulcli 
 |-  ( 8 x. ( ; 1 0 ^ ; 3 0 ) ) e. NN
35 34 nnrei 
 |-  ( 8 x. ( ; 1 0 ^ ; 3 0 ) ) e. RR
36 28 35 ltaddposi 
 |-  ( 0 < ( 8 x. ( ; 1 0 ^ ; 2 9 ) ) <-> ( 8 x. ( ; 1 0 ^ ; 3 0 ) ) < ( ( 8 x. ( ; 1 0 ^ ; 3 0 ) ) + ( 8 x. ( ; 1 0 ^ ; 2 9 ) ) ) )
37 27 36 mpbi 
 |-  ( 8 x. ( ; 1 0 ^ ; 3 0 ) ) < ( ( 8 x. ( ; 1 0 ^ ; 3 0 ) ) + ( 8 x. ( ; 1 0 ^ ; 2 9 ) ) )
38 dfdec10 
 |-  ; 8 8 = ( ( ; 1 0 x. 8 ) + 8 )
39 38 oveq1i 
 |-  ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) = ( ( ( ; 1 0 x. 8 ) + 8 ) x. ( ; 1 0 ^ ; 2 9 ) )
40 4 2 nnmulcli 
 |-  ( ; 1 0 x. 8 ) e. NN
41 40 nncni 
 |-  ( ; 1 0 x. 8 ) e. CC
42 8cn 
 |-  8 e. CC
43 9 nncni 
 |-  ( ; 1 0 ^ ; 2 9 ) e. CC
44 41 42 43 adddiri 
 |-  ( ( ( ; 1 0 x. 8 ) + 8 ) x. ( ; 1 0 ^ ; 2 9 ) ) = ( ( ( ; 1 0 x. 8 ) x. ( ; 1 0 ^ ; 2 9 ) ) + ( 8 x. ( ; 1 0 ^ ; 2 9 ) ) )
45 41 43 mulcomi 
 |-  ( ( ; 1 0 x. 8 ) x. ( ; 1 0 ^ ; 2 9 ) ) = ( ( ; 1 0 ^ ; 2 9 ) x. ( ; 1 0 x. 8 ) )
46 4 nncni 
 |-  ; 1 0 e. CC
47 43 46 42 mulassi 
 |-  ( ( ( ; 1 0 ^ ; 2 9 ) x. ; 1 0 ) x. 8 ) = ( ( ; 1 0 ^ ; 2 9 ) x. ( ; 1 0 x. 8 ) )
48 nncn 
 |-  ( ; 1 0 e. NN -> ; 1 0 e. CC )
49 7 a1i 
 |-  ( ; 1 0 e. NN -> ; 2 9 e. NN0 )
50 48 49 expp1d 
 |-  ( ; 1 0 e. NN -> ( ; 1 0 ^ ( ; 2 9 + 1 ) ) = ( ( ; 1 0 ^ ; 2 9 ) x. ; 1 0 ) )
51 4 50 ax-mp 
 |-  ( ; 1 0 ^ ( ; 2 9 + 1 ) ) = ( ( ; 1 0 ^ ; 2 9 ) x. ; 1 0 )
52 51 eqcomi 
 |-  ( ( ; 1 0 ^ ; 2 9 ) x. ; 1 0 ) = ( ; 1 0 ^ ( ; 2 9 + 1 ) )
53 52 oveq1i 
 |-  ( ( ( ; 1 0 ^ ; 2 9 ) x. ; 1 0 ) x. 8 ) = ( ( ; 1 0 ^ ( ; 2 9 + 1 ) ) x. 8 )
54 45 47 53 3eqtr2i 
 |-  ( ( ; 1 0 x. 8 ) x. ( ; 1 0 ^ ; 2 9 ) ) = ( ( ; 1 0 ^ ( ; 2 9 + 1 ) ) x. 8 )
55 54 oveq1i 
 |-  ( ( ( ; 1 0 x. 8 ) x. ( ; 1 0 ^ ; 2 9 ) ) + ( 8 x. ( ; 1 0 ^ ; 2 9 ) ) ) = ( ( ( ; 1 0 ^ ( ; 2 9 + 1 ) ) x. 8 ) + ( 8 x. ( ; 1 0 ^ ; 2 9 ) ) )
56 2p1e3 
 |-  ( 2 + 1 ) = 3
57 eqid 
 |-  ; 2 9 = ; 2 9
58 5 56 57 decsucc 
 |-  ( ; 2 9 + 1 ) = ; 3 0
59 58 oveq2i 
 |-  ( ; 1 0 ^ ( ; 2 9 + 1 ) ) = ( ; 1 0 ^ ; 3 0 )
60 59 oveq1i 
 |-  ( ( ; 1 0 ^ ( ; 2 9 + 1 ) ) x. 8 ) = ( ( ; 1 0 ^ ; 3 0 ) x. 8 )
61 60 oveq1i 
 |-  ( ( ( ; 1 0 ^ ( ; 2 9 + 1 ) ) x. 8 ) + ( 8 x. ( ; 1 0 ^ ; 2 9 ) ) ) = ( ( ( ; 1 0 ^ ; 3 0 ) x. 8 ) + ( 8 x. ( ; 1 0 ^ ; 2 9 ) ) )
62 33 nncni 
 |-  ( ; 1 0 ^ ; 3 0 ) e. CC
63 mulcom 
 |-  ( ( ( ; 1 0 ^ ; 3 0 ) e. CC /\ 8 e. CC ) -> ( ( ; 1 0 ^ ; 3 0 ) x. 8 ) = ( 8 x. ( ; 1 0 ^ ; 3 0 ) ) )
64 63 oveq1d 
 |-  ( ( ( ; 1 0 ^ ; 3 0 ) e. CC /\ 8 e. CC ) -> ( ( ( ; 1 0 ^ ; 3 0 ) x. 8 ) + ( 8 x. ( ; 1 0 ^ ; 2 9 ) ) ) = ( ( 8 x. ( ; 1 0 ^ ; 3 0 ) ) + ( 8 x. ( ; 1 0 ^ ; 2 9 ) ) ) )
65 62 42 64 mp2an 
 |-  ( ( ( ; 1 0 ^ ; 3 0 ) x. 8 ) + ( 8 x. ( ; 1 0 ^ ; 2 9 ) ) ) = ( ( 8 x. ( ; 1 0 ^ ; 3 0 ) ) + ( 8 x. ( ; 1 0 ^ ; 2 9 ) ) )
66 55 61 65 3eqtri 
 |-  ( ( ( ; 1 0 x. 8 ) x. ( ; 1 0 ^ ; 2 9 ) ) + ( 8 x. ( ; 1 0 ^ ; 2 9 ) ) ) = ( ( 8 x. ( ; 1 0 ^ ; 3 0 ) ) + ( 8 x. ( ; 1 0 ^ ; 2 9 ) ) )
67 39 44 66 3eqtri 
 |-  ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) = ( ( 8 x. ( ; 1 0 ^ ; 3 0 ) ) + ( 8 x. ( ; 1 0 ^ ; 2 9 ) ) )
68 37 67 breqtrri 
 |-  ( 8 x. ( ; 1 0 ^ ; 3 0 ) ) < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) )
69 25 68 jctil 
 |-  ( ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) e. NN -> ( ( 8 x. ( ; 1 0 ^ ; 3 0 ) ) < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) /\ A. n e. Odd ( ( 7 < n /\ n < ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) ) -> n e. GoldbachOdd ) ) )
70 11 18 69 rspcedvd 
 |-  ( ( ; 8 8 x. ( ; 1 0 ^ ; 2 9 ) ) e. NN -> E. m e. NN ( ( 8 x. ( ; 1 0 ^ ; 3 0 ) ) < m /\ A. n e. Odd ( ( 7 < n /\ n < m ) -> n e. GoldbachOdd ) ) )
71 10 70 ax-mp 
 |-  E. m e. NN ( ( 8 x. ( ; 1 0 ^ ; 3 0 ) ) < m /\ A. n e. Odd ( ( 7 < n /\ n < m ) -> n e. GoldbachOdd ) )