Metamath Proof Explorer

Theorem tgoldbach

Description: The ternary Goldbach conjecture is valid. Main theorem in Helfgott p. 2. This follows from tgoldbachlt and ax-tgoldbachgt . (Contributed by AV, 2-Aug-2020) (Revised by AV, 9-Sep-2021)

Ref Expression
Assertion tgoldbach 
|- A. n e. Odd ( 7 < n -> n e. GoldbachOdd )

Proof

Step Hyp Ref Expression
1 oddz 
 |-  ( n e. Odd -> n e. ZZ )
2 1 zred 
 |-  ( n e. Odd -> n e. RR )
3 10re 
 |-  ; 1 0 e. RR
4 2nn0 
 |-  2 e. NN0
5 7nn 
 |-  7 e. NN
6 4 5 decnncl 
 |-  ; 2 7 e. NN
7 6 nnnn0i 
 |-  ; 2 7 e. NN0
8 reexpcl 
 |-  ( ( ; 1 0 e. RR /\ ; 2 7 e. NN0 ) -> ( ; 1 0 ^ ; 2 7 ) e. RR )
9 3 7 8 mp2an 
 |-  ( ; 1 0 ^ ; 2 7 ) e. RR
10 lelttric 
 |-  ( ( n e. RR /\ ( ; 1 0 ^ ; 2 7 ) e. RR ) -> ( n <_ ( ; 1 0 ^ ; 2 7 ) \/ ( ; 1 0 ^ ; 2 7 ) < n ) )
11 2 9 10 sylancl 
 |-  ( n e. Odd -> ( n <_ ( ; 1 0 ^ ; 2 7 ) \/ ( ; 1 0 ^ ; 2 7 ) < n ) )
12 tgoldbachlt 
 |-  E. m e. NN ( ( 8 x. ( ; 1 0 ^ ; 3 0 ) ) < m /\ A. o e. Odd ( ( 7 < o /\ o < m ) -> o e. GoldbachOdd ) )
13 breq2 
 |-  ( o = n -> ( 7 < o <-> 7 < n ) )
14 breq1 
 |-  ( o = n -> ( o < m <-> n < m ) )
15 13 14 anbi12d 
 |-  ( o = n -> ( ( 7 < o /\ o < m ) <-> ( 7 < n /\ n < m ) ) )
16 eleq1w 
 |-  ( o = n -> ( o e. GoldbachOdd <-> n e. GoldbachOdd ) )
17 15 16 imbi12d 
 |-  ( o = n -> ( ( ( 7 < o /\ o < m ) -> o e. GoldbachOdd ) <-> ( ( 7 < n /\ n < m ) -> n e. GoldbachOdd ) ) )
18 17 rspcv 
 |-  ( n e. Odd -> ( A. o e. Odd ( ( 7 < o /\ o < m ) -> o e. GoldbachOdd ) -> ( ( 7 < n /\ n < m ) -> n e. GoldbachOdd ) ) )
19 9 recni 
 |-  ( ; 1 0 ^ ; 2 7 ) e. CC
20 19 mullidi 
 |-  ( 1 x. ( ; 1 0 ^ ; 2 7 ) ) = ( ; 1 0 ^ ; 2 7 )
21 1re 
 |-  1 e. RR
22 8re 
 |-  8 e. RR
23 21 22 pm3.2i 
 |-  ( 1 e. RR /\ 8 e. RR )
24 23 a1i 
 |-  ( ( n e. Odd /\ m e. NN ) -> ( 1 e. RR /\ 8 e. RR ) )
25 0le1 
 |-  0 <_ 1
26 1lt8 
 |-  1 < 8
27 25 26 pm3.2i 
 |-  ( 0 <_ 1 /\ 1 < 8 )
28 27 a1i 
 |-  ( ( n e. Odd /\ m e. NN ) -> ( 0 <_ 1 /\ 1 < 8 ) )
29 3nn 
 |-  3 e. NN
30 29 decnncl2 
 |-  ; 3 0 e. NN
31 30 nnnn0i 
 |-  ; 3 0 e. NN0
32 reexpcl 
 |-  ( ( ; 1 0 e. RR /\ ; 3 0 e. NN0 ) -> ( ; 1 0 ^ ; 3 0 ) e. RR )
33 3 31 32 mp2an 
 |-  ( ; 1 0 ^ ; 3 0 ) e. RR
34 9 33 pm3.2i 
 |-  ( ( ; 1 0 ^ ; 2 7 ) e. RR /\ ( ; 1 0 ^ ; 3 0 ) e. RR )
35 34 a1i 
 |-  ( ( n e. Odd /\ m e. NN ) -> ( ( ; 1 0 ^ ; 2 7 ) e. RR /\ ( ; 1 0 ^ ; 3 0 ) e. RR ) )
36 10nn0 
 |-  ; 1 0 e. NN0
37 36 7 nn0expcli 
 |-  ( ; 1 0 ^ ; 2 7 ) e. NN0
38 37 nn0ge0i 
 |-  0 <_ ( ; 1 0 ^ ; 2 7 )
39 6 nnzi 
 |-  ; 2 7 e. ZZ
40 30 nnzi 
 |-  ; 3 0 e. ZZ
41 3 39 40 3pm3.2i 
 |-  ( ; 1 0 e. RR /\ ; 2 7 e. ZZ /\ ; 3 0 e. ZZ )
42 1lt10 
 |-  1 < ; 1 0
43 3nn0 
 |-  3 e. NN0
44 7nn0 
 |-  7 e. NN0
45 0nn0 
 |-  0 e. NN0
46 7lt10 
 |-  7 < ; 1 0
47 2lt3 
 |-  2 < 3
48 4 43 44 45 46 47 decltc 
 |-  ; 2 7 < ; 3 0
49 42 48 pm3.2i 
 |-  ( 1 < ; 1 0 /\ ; 2 7 < ; 3 0 )
50 ltexp2a 
 |-  ( ( ( ; 1 0 e. RR /\ ; 2 7 e. ZZ /\ ; 3 0 e. ZZ ) /\ ( 1 < ; 1 0 /\ ; 2 7 < ; 3 0 ) ) -> ( ; 1 0 ^ ; 2 7 ) < ( ; 1 0 ^ ; 3 0 ) )
51 41 49 50 mp2an 
 |-  ( ; 1 0 ^ ; 2 7 ) < ( ; 1 0 ^ ; 3 0 )
52 38 51 pm3.2i 
 |-  ( 0 <_ ( ; 1 0 ^ ; 2 7 ) /\ ( ; 1 0 ^ ; 2 7 ) < ( ; 1 0 ^ ; 3 0 ) )
53 52 a1i 
 |-  ( ( n e. Odd /\ m e. NN ) -> ( 0 <_ ( ; 1 0 ^ ; 2 7 ) /\ ( ; 1 0 ^ ; 2 7 ) < ( ; 1 0 ^ ; 3 0 ) ) )
54 ltmul12a 
 |-  ( ( ( ( 1 e. RR /\ 8 e. RR ) /\ ( 0 <_ 1 /\ 1 < 8 ) ) /\ ( ( ( ; 1 0 ^ ; 2 7 ) e. RR /\ ( ; 1 0 ^ ; 3 0 ) e. RR ) /\ ( 0 <_ ( ; 1 0 ^ ; 2 7 ) /\ ( ; 1 0 ^ ; 2 7 ) < ( ; 1 0 ^ ; 3 0 ) ) ) ) -> ( 1 x. ( ; 1 0 ^ ; 2 7 ) ) < ( 8 x. ( ; 1 0 ^ ; 3 0 ) ) )
55 24 28 35 53 54 syl22anc 
 |-  ( ( n e. Odd /\ m e. NN ) -> ( 1 x. ( ; 1 0 ^ ; 2 7 ) ) < ( 8 x. ( ; 1 0 ^ ; 3 0 ) ) )
56 20 55 eqbrtrrid 
 |-  ( ( n e. Odd /\ m e. NN ) -> ( ; 1 0 ^ ; 2 7 ) < ( 8 x. ( ; 1 0 ^ ; 3 0 ) ) )
57 9 a1i 
 |-  ( ( n e. Odd /\ m e. NN ) -> ( ; 1 0 ^ ; 2 7 ) e. RR )
58 22 33 remulcli 
 |-  ( 8 x. ( ; 1 0 ^ ; 3 0 ) ) e. RR
59 58 a1i 
 |-  ( ( n e. Odd /\ m e. NN ) -> ( 8 x. ( ; 1 0 ^ ; 3 0 ) ) e. RR )
60 nnre 
 |-  ( m e. NN -> m e. RR )
61 60 adantl 
 |-  ( ( n e. Odd /\ m e. NN ) -> m e. RR )
62 lttr 
 |-  ( ( ( ; 1 0 ^ ; 2 7 ) e. RR /\ ( 8 x. ( ; 1 0 ^ ; 3 0 ) ) e. RR /\ m e. RR ) -> ( ( ( ; 1 0 ^ ; 2 7 ) < ( 8 x. ( ; 1 0 ^ ; 3 0 ) ) /\ ( 8 x. ( ; 1 0 ^ ; 3 0 ) ) < m ) -> ( ; 1 0 ^ ; 2 7 ) < m ) )
63 57 59 61 62 syl3anc 
 |-  ( ( n e. Odd /\ m e. NN ) -> ( ( ( ; 1 0 ^ ; 2 7 ) < ( 8 x. ( ; 1 0 ^ ; 3 0 ) ) /\ ( 8 x. ( ; 1 0 ^ ; 3 0 ) ) < m ) -> ( ; 1 0 ^ ; 2 7 ) < m ) )
64 56 63 mpand 
 |-  ( ( n e. Odd /\ m e. NN ) -> ( ( 8 x. ( ; 1 0 ^ ; 3 0 ) ) < m -> ( ; 1 0 ^ ; 2 7 ) < m ) )
65 64 imp 
 |-  ( ( ( n e. Odd /\ m e. NN ) /\ ( 8 x. ( ; 1 0 ^ ; 3 0 ) ) < m ) -> ( ; 1 0 ^ ; 2 7 ) < m )
66 2 adantr 
 |-  ( ( n e. Odd /\ m e. NN ) -> n e. RR )
67 66 57 61 3jca 
 |-  ( ( n e. Odd /\ m e. NN ) -> ( n e. RR /\ ( ; 1 0 ^ ; 2 7 ) e. RR /\ m e. RR ) )
68 67 adantr 
 |-  ( ( ( n e. Odd /\ m e. NN ) /\ ( 8 x. ( ; 1 0 ^ ; 3 0 ) ) < m ) -> ( n e. RR /\ ( ; 1 0 ^ ; 2 7 ) e. RR /\ m e. RR ) )
69 lelttr 
 |-  ( ( n e. RR /\ ( ; 1 0 ^ ; 2 7 ) e. RR /\ m e. RR ) -> ( ( n <_ ( ; 1 0 ^ ; 2 7 ) /\ ( ; 1 0 ^ ; 2 7 ) < m ) -> n < m ) )
70 68 69 syl 
 |-  ( ( ( n e. Odd /\ m e. NN ) /\ ( 8 x. ( ; 1 0 ^ ; 3 0 ) ) < m ) -> ( ( n <_ ( ; 1 0 ^ ; 2 7 ) /\ ( ; 1 0 ^ ; 2 7 ) < m ) -> n < m ) )
71 65 70 mpan2d 
 |-  ( ( ( n e. Odd /\ m e. NN ) /\ ( 8 x. ( ; 1 0 ^ ; 3 0 ) ) < m ) -> ( n <_ ( ; 1 0 ^ ; 2 7 ) -> n < m ) )
72 71 imp 
 |-  ( ( ( ( n e. Odd /\ m e. NN ) /\ ( 8 x. ( ; 1 0 ^ ; 3 0 ) ) < m ) /\ n <_ ( ; 1 0 ^ ; 2 7 ) ) -> n < m )
73 72 anim1i 
 |-  ( ( ( ( ( n e. Odd /\ m e. NN ) /\ ( 8 x. ( ; 1 0 ^ ; 3 0 ) ) < m ) /\ n <_ ( ; 1 0 ^ ; 2 7 ) ) /\ 7 < n ) -> ( n < m /\ 7 < n ) )
74 73 ancomd 
 |-  ( ( ( ( ( n e. Odd /\ m e. NN ) /\ ( 8 x. ( ; 1 0 ^ ; 3 0 ) ) < m ) /\ n <_ ( ; 1 0 ^ ; 2 7 ) ) /\ 7 < n ) -> ( 7 < n /\ n < m ) )
75 pm2.27 
 |-  ( ( 7 < n /\ n < m ) -> ( ( ( 7 < n /\ n < m ) -> n e. GoldbachOdd ) -> n e. GoldbachOdd ) )
76 74 75 syl 
 |-  ( ( ( ( ( n e. Odd /\ m e. NN ) /\ ( 8 x. ( ; 1 0 ^ ; 3 0 ) ) < m ) /\ n <_ ( ; 1 0 ^ ; 2 7 ) ) /\ 7 < n ) -> ( ( ( 7 < n /\ n < m ) -> n e. GoldbachOdd ) -> n e. GoldbachOdd ) )
77 76 ex 
 |-  ( ( ( ( n e. Odd /\ m e. NN ) /\ ( 8 x. ( ; 1 0 ^ ; 3 0 ) ) < m ) /\ n <_ ( ; 1 0 ^ ; 2 7 ) ) -> ( 7 < n -> ( ( ( 7 < n /\ n < m ) -> n e. GoldbachOdd ) -> n e. GoldbachOdd ) ) )
78 77 com23 
 |-  ( ( ( ( n e. Odd /\ m e. NN ) /\ ( 8 x. ( ; 1 0 ^ ; 3 0 ) ) < m ) /\ n <_ ( ; 1 0 ^ ; 2 7 ) ) -> ( ( ( 7 < n /\ n < m ) -> n e. GoldbachOdd ) -> ( 7 < n -> n e. GoldbachOdd ) ) )
79 78 exp41 
 |-  ( n e. Odd -> ( m e. NN -> ( ( 8 x. ( ; 1 0 ^ ; 3 0 ) ) < m -> ( n <_ ( ; 1 0 ^ ; 2 7 ) -> ( ( ( 7 < n /\ n < m ) -> n e. GoldbachOdd ) -> ( 7 < n -> n e. GoldbachOdd ) ) ) ) ) )
80 79 com25 
 |-  ( n e. Odd -> ( ( ( 7 < n /\ n < m ) -> n e. GoldbachOdd ) -> ( ( 8 x. ( ; 1 0 ^ ; 3 0 ) ) < m -> ( n <_ ( ; 1 0 ^ ; 2 7 ) -> ( m e. NN -> ( 7 < n -> n e. GoldbachOdd ) ) ) ) ) )
81 18 80 syld 
 |-  ( n e. Odd -> ( A. o e. Odd ( ( 7 < o /\ o < m ) -> o e. GoldbachOdd ) -> ( ( 8 x. ( ; 1 0 ^ ; 3 0 ) ) < m -> ( n <_ ( ; 1 0 ^ ; 2 7 ) -> ( m e. NN -> ( 7 < n -> n e. GoldbachOdd ) ) ) ) ) )
82 81 com15 
 |-  ( m e. NN -> ( A. o e. Odd ( ( 7 < o /\ o < m ) -> o e. GoldbachOdd ) -> ( ( 8 x. ( ; 1 0 ^ ; 3 0 ) ) < m -> ( n <_ ( ; 1 0 ^ ; 2 7 ) -> ( n e. Odd -> ( 7 < n -> n e. GoldbachOdd ) ) ) ) ) )
83 82 com23 
 |-  ( m e. NN -> ( ( 8 x. ( ; 1 0 ^ ; 3 0 ) ) < m -> ( A. o e. Odd ( ( 7 < o /\ o < m ) -> o e. GoldbachOdd ) -> ( n <_ ( ; 1 0 ^ ; 2 7 ) -> ( n e. Odd -> ( 7 < n -> n e. GoldbachOdd ) ) ) ) ) )
84 83 imp32 
 |-  ( ( m e. NN /\ ( ( 8 x. ( ; 1 0 ^ ; 3 0 ) ) < m /\ A. o e. Odd ( ( 7 < o /\ o < m ) -> o e. GoldbachOdd ) ) ) -> ( n <_ ( ; 1 0 ^ ; 2 7 ) -> ( n e. Odd -> ( 7 < n -> n e. GoldbachOdd ) ) ) )
85 84 rexlimiva 
 |-  ( E. m e. NN ( ( 8 x. ( ; 1 0 ^ ; 3 0 ) ) < m /\ A. o e. Odd ( ( 7 < o /\ o < m ) -> o e. GoldbachOdd ) ) -> ( n <_ ( ; 1 0 ^ ; 2 7 ) -> ( n e. Odd -> ( 7 < n -> n e. GoldbachOdd ) ) ) )
86 12 85 ax-mp 
 |-  ( n <_ ( ; 1 0 ^ ; 2 7 ) -> ( n e. Odd -> ( 7 < n -> n e. GoldbachOdd ) ) )
87 tgoldbachgtALTV 
 |-  E. m e. NN ( m <_ ( ; 1 0 ^ ; 2 7 ) /\ A. o e. Odd ( m < o -> o e. GoldbachOdd ) )
88 breq2 
 |-  ( o = n -> ( m < o <-> m < n ) )
89 88 16 imbi12d 
 |-  ( o = n -> ( ( m < o -> o e. GoldbachOdd ) <-> ( m < n -> n e. GoldbachOdd ) ) )
90 89 rspcv 
 |-  ( n e. Odd -> ( A. o e. Odd ( m < o -> o e. GoldbachOdd ) -> ( m < n -> n e. GoldbachOdd ) ) )
91 lelttr 
 |-  ( ( m e. RR /\ ( ; 1 0 ^ ; 2 7 ) e. RR /\ n e. RR ) -> ( ( m <_ ( ; 1 0 ^ ; 2 7 ) /\ ( ; 1 0 ^ ; 2 7 ) < n ) -> m < n ) )
92 61 57 66 91 syl3anc 
 |-  ( ( n e. Odd /\ m e. NN ) -> ( ( m <_ ( ; 1 0 ^ ; 2 7 ) /\ ( ; 1 0 ^ ; 2 7 ) < n ) -> m < n ) )
93 92 expcomd 
 |-  ( ( n e. Odd /\ m e. NN ) -> ( ( ; 1 0 ^ ; 2 7 ) < n -> ( m <_ ( ; 1 0 ^ ; 2 7 ) -> m < n ) ) )
94 93 ex 
 |-  ( n e. Odd -> ( m e. NN -> ( ( ; 1 0 ^ ; 2 7 ) < n -> ( m <_ ( ; 1 0 ^ ; 2 7 ) -> m < n ) ) ) )
95 94 com23 
 |-  ( n e. Odd -> ( ( ; 1 0 ^ ; 2 7 ) < n -> ( m e. NN -> ( m <_ ( ; 1 0 ^ ; 2 7 ) -> m < n ) ) ) )
96 95 imp43 
 |-  ( ( ( n e. Odd /\ ( ; 1 0 ^ ; 2 7 ) < n ) /\ ( m e. NN /\ m <_ ( ; 1 0 ^ ; 2 7 ) ) ) -> m < n )
97 pm2.27 
 |-  ( m < n -> ( ( m < n -> n e. GoldbachOdd ) -> n e. GoldbachOdd ) )
98 96 97 syl 
 |-  ( ( ( n e. Odd /\ ( ; 1 0 ^ ; 2 7 ) < n ) /\ ( m e. NN /\ m <_ ( ; 1 0 ^ ; 2 7 ) ) ) -> ( ( m < n -> n e. GoldbachOdd ) -> n e. GoldbachOdd ) )
99 98 a1dd 
 |-  ( ( ( n e. Odd /\ ( ; 1 0 ^ ; 2 7 ) < n ) /\ ( m e. NN /\ m <_ ( ; 1 0 ^ ; 2 7 ) ) ) -> ( ( m < n -> n e. GoldbachOdd ) -> ( 7 < n -> n e. GoldbachOdd ) ) )
100 99 ex 
 |-  ( ( n e. Odd /\ ( ; 1 0 ^ ; 2 7 ) < n ) -> ( ( m e. NN /\ m <_ ( ; 1 0 ^ ; 2 7 ) ) -> ( ( m < n -> n e. GoldbachOdd ) -> ( 7 < n -> n e. GoldbachOdd ) ) ) )
101 100 com23 
 |-  ( ( n e. Odd /\ ( ; 1 0 ^ ; 2 7 ) < n ) -> ( ( m < n -> n e. GoldbachOdd ) -> ( ( m e. NN /\ m <_ ( ; 1 0 ^ ; 2 7 ) ) -> ( 7 < n -> n e. GoldbachOdd ) ) ) )
102 101 ex 
 |-  ( n e. Odd -> ( ( ; 1 0 ^ ; 2 7 ) < n -> ( ( m < n -> n e. GoldbachOdd ) -> ( ( m e. NN /\ m <_ ( ; 1 0 ^ ; 2 7 ) ) -> ( 7 < n -> n e. GoldbachOdd ) ) ) ) )
103 102 com23 
 |-  ( n e. Odd -> ( ( m < n -> n e. GoldbachOdd ) -> ( ( ; 1 0 ^ ; 2 7 ) < n -> ( ( m e. NN /\ m <_ ( ; 1 0 ^ ; 2 7 ) ) -> ( 7 < n -> n e. GoldbachOdd ) ) ) ) )
104 90 103 syld 
 |-  ( n e. Odd -> ( A. o e. Odd ( m < o -> o e. GoldbachOdd ) -> ( ( ; 1 0 ^ ; 2 7 ) < n -> ( ( m e. NN /\ m <_ ( ; 1 0 ^ ; 2 7 ) ) -> ( 7 < n -> n e. GoldbachOdd ) ) ) ) )
105 104 com14 
 |-  ( ( m e. NN /\ m <_ ( ; 1 0 ^ ; 2 7 ) ) -> ( A. o e. Odd ( m < o -> o e. GoldbachOdd ) -> ( ( ; 1 0 ^ ; 2 7 ) < n -> ( n e. Odd -> ( 7 < n -> n e. GoldbachOdd ) ) ) ) )
106 105 impr 
 |-  ( ( m e. NN /\ ( m <_ ( ; 1 0 ^ ; 2 7 ) /\ A. o e. Odd ( m < o -> o e. GoldbachOdd ) ) ) -> ( ( ; 1 0 ^ ; 2 7 ) < n -> ( n e. Odd -> ( 7 < n -> n e. GoldbachOdd ) ) ) )
107 106 rexlimiva 
 |-  ( E. m e. NN ( m <_ ( ; 1 0 ^ ; 2 7 ) /\ A. o e. Odd ( m < o -> o e. GoldbachOdd ) ) -> ( ( ; 1 0 ^ ; 2 7 ) < n -> ( n e. Odd -> ( 7 < n -> n e. GoldbachOdd ) ) ) )
108 87 107 ax-mp 
 |-  ( ( ; 1 0 ^ ; 2 7 ) < n -> ( n e. Odd -> ( 7 < n -> n e. GoldbachOdd ) ) )
109 86 108 jaoi 
 |-  ( ( n <_ ( ; 1 0 ^ ; 2 7 ) \/ ( ; 1 0 ^ ; 2 7 ) < n ) -> ( n e. Odd -> ( 7 < n -> n e. GoldbachOdd ) ) )
110 11 109 mpcom 
 |-  ( n e. Odd -> ( 7 < n -> n e. GoldbachOdd ) )
111 110 rgen 
 |-  A. n e. Odd ( 7 < n -> n e. GoldbachOdd )