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 ∃ 𝑚 ∈ ℕ ( ( 8 · ( 1 0 ↑ 3 0 ) ) < 𝑚 ∧ ∀ 𝑛 ∈ Odd ( ( 7 < 𝑛 ∧ 𝑛 < 𝑚 ) → 𝑛 ∈ GoldbachOdd ) )

Proof

Step Hyp Ref Expression
1 8nn0 ⊢ 8 ∈ ℕ0
2 8nn ⊢ 8 ∈ ℕ
3 1 2 decnncl ⊢ 8 8 ∈ ℕ
4 10nn ⊢ 1 0 ∈ ℕ
5 2nn0 ⊢ 2 ∈ ℕ0
6 9nn0 ⊢ 9 ∈ ℕ0
7 5 6 deccl ⊢ 2 9 ∈ ℕ0
8 nnexpcl ⊢ ( ( 1 0 ∈ ℕ ∧ 2 9 ∈ ℕ0 ) → ( 1 0 ↑ 2 9 ) ∈ ℕ )
9 4 7 8 mp2an ⊢ ( 1 0 ↑ 2 9 ) ∈ ℕ
10 3 9 nnmulcli ⊢ ( 8 8 · ( 1 0 ↑ 2 9 ) ) ∈ ℕ
11 id ⊢ ( ( 8 8 · ( 1 0 ↑ 2 9 ) ) ∈ ℕ → ( 8 8 · ( 1 0 ↑ 2 9 ) ) ∈ ℕ )
12 breq2 ⊢ ( 𝑚 = ( 8 8 · ( 1 0 ↑ 2 9 ) ) → ( ( 8 · ( 1 0 ↑ 3 0 ) ) < 𝑚 ↔ ( 8 · ( 1 0 ↑ 3 0 ) ) < ( 8 8 · ( 1 0 ↑ 2 9 ) ) ) )
13 breq2 ⊢ ( 𝑚 = ( 8 8 · ( 1 0 ↑ 2 9 ) ) → ( 𝑛 < 𝑚 ↔ 𝑛 < ( 8 8 · ( 1 0 ↑ 2 9 ) ) ) )
14 13 anbi2d ⊢ ( 𝑚 = ( 8 8 · ( 1 0 ↑ 2 9 ) ) → ( ( 7 < 𝑛 ∧ 𝑛 < 𝑚 ) ↔ ( 7 < 𝑛 ∧ 𝑛 < ( 8 8 · ( 1 0 ↑ 2 9 ) ) ) ) )
15 14 imbi1d ⊢ ( 𝑚 = ( 8 8 · ( 1 0 ↑ 2 9 ) ) → ( ( ( 7 < 𝑛 ∧ 𝑛 < 𝑚 ) → 𝑛 ∈ GoldbachOdd ) ↔ ( ( 7 < 𝑛 ∧ 𝑛 < ( 8 8 · ( 1 0 ↑ 2 9 ) ) ) → 𝑛 ∈ GoldbachOdd ) ) )
16 15 ralbidv ⊢ ( 𝑚 = ( 8 8 · ( 1 0 ↑ 2 9 ) ) → ( ∀ 𝑛 ∈ Odd ( ( 7 < 𝑛 ∧ 𝑛 < 𝑚 ) → 𝑛 ∈ GoldbachOdd ) ↔ ∀ 𝑛 ∈ Odd ( ( 7 < 𝑛 ∧ 𝑛 < ( 8 8 · ( 1 0 ↑ 2 9 ) ) ) → 𝑛 ∈ GoldbachOdd ) ) )
17 12 16 anbi12d ⊢ ( 𝑚 = ( 8 8 · ( 1 0 ↑ 2 9 ) ) → ( ( ( 8 · ( 1 0 ↑ 3 0 ) ) < 𝑚 ∧ ∀ 𝑛 ∈ Odd ( ( 7 < 𝑛 ∧ 𝑛 < 𝑚 ) → 𝑛 ∈ GoldbachOdd ) ) ↔ ( ( 8 · ( 1 0 ↑ 3 0 ) ) < ( 8 8 · ( 1 0 ↑ 2 9 ) ) ∧ ∀ 𝑛 ∈ Odd ( ( 7 < 𝑛 ∧ 𝑛 < ( 8 8 · ( 1 0 ↑ 2 9 ) ) ) → 𝑛 ∈ GoldbachOdd ) ) ) )
18 17 adantl ⊢ ( ( ( 8 8 · ( 1 0 ↑ 2 9 ) ) ∈ ℕ ∧ 𝑚 = ( 8 8 · ( 1 0 ↑ 2 9 ) ) ) → ( ( ( 8 · ( 1 0 ↑ 3 0 ) ) < 𝑚 ∧ ∀ 𝑛 ∈ Odd ( ( 7 < 𝑛 ∧ 𝑛 < 𝑚 ) → 𝑛 ∈ GoldbachOdd ) ) ↔ ( ( 8 · ( 1 0 ↑ 3 0 ) ) < ( 8 8 · ( 1 0 ↑ 2 9 ) ) ∧ ∀ 𝑛 ∈ Odd ( ( 7 < 𝑛 ∧ 𝑛 < ( 8 8 · ( 1 0 ↑ 2 9 ) ) ) → 𝑛 ∈ GoldbachOdd ) ) ) )
19 simplr ⊢ ( ( ( ( 8 8 · ( 1 0 ↑ 2 9 ) ) ∈ ℕ ∧ 𝑛 ∈ Odd ) ∧ ( 7 < 𝑛 ∧ 𝑛 < ( 8 8 · ( 1 0 ↑ 2 9 ) ) ) ) → 𝑛 ∈ Odd )
20 simprl ⊢ ( ( ( ( 8 8 · ( 1 0 ↑ 2 9 ) ) ∈ ℕ ∧ 𝑛 ∈ Odd ) ∧ ( 7 < 𝑛 ∧ 𝑛 < ( 8 8 · ( 1 0 ↑ 2 9 ) ) ) ) → 7 < 𝑛 )
21 simprr ⊢ ( ( ( ( 8 8 · ( 1 0 ↑ 2 9 ) ) ∈ ℕ ∧ 𝑛 ∈ Odd ) ∧ ( 7 < 𝑛 ∧ 𝑛 < ( 8 8 · ( 1 0 ↑ 2 9 ) ) ) ) → 𝑛 < ( 8 8 · ( 1 0 ↑ 2 9 ) ) )
22 tgblthelfgott ⊢ ( ( 𝑛 ∈ Odd ∧ 7 < 𝑛 ∧ 𝑛 < ( 8 8 · ( 1 0 ↑ 2 9 ) ) ) → 𝑛 ∈ GoldbachOdd )
23 19 20 21 22 syl3anc ⊢ ( ( ( ( 8 8 · ( 1 0 ↑ 2 9 ) ) ∈ ℕ ∧ 𝑛 ∈ Odd ) ∧ ( 7 < 𝑛 ∧ 𝑛 < ( 8 8 · ( 1 0 ↑ 2 9 ) ) ) ) → 𝑛 ∈ GoldbachOdd )
24 23 ex ⊢ ( ( ( 8 8 · ( 1 0 ↑ 2 9 ) ) ∈ ℕ ∧ 𝑛 ∈ Odd ) → ( ( 7 < 𝑛 ∧ 𝑛 < ( 8 8 · ( 1 0 ↑ 2 9 ) ) ) → 𝑛 ∈ GoldbachOdd ) )
25 24 ralrimiva ⊢ ( ( 8 8 · ( 1 0 ↑ 2 9 ) ) ∈ ℕ → ∀ 𝑛 ∈ Odd ( ( 7 < 𝑛 ∧ 𝑛 < ( 8 8 · ( 1 0 ↑ 2 9 ) ) ) → 𝑛 ∈ GoldbachOdd ) )
26 2 9 nnmulcli ⊢ ( 8 · ( 1 0 ↑ 2 9 ) ) ∈ ℕ
27 26 nngt0i ⊢ 0 < ( 8 · ( 1 0 ↑ 2 9 ) )
28 26 nnrei ⊢ ( 8 · ( 1 0 ↑ 2 9 ) ) ∈ ℝ
29 3nn0 ⊢ 3 ∈ ℕ0
30 0nn0 ⊢ 0 ∈ ℕ0
31 29 30 deccl ⊢ 3 0 ∈ ℕ0
32 nnexpcl ⊢ ( ( 1 0 ∈ ℕ ∧ 3 0 ∈ ℕ0 ) → ( 1 0 ↑ 3 0 ) ∈ ℕ )
33 4 31 32 mp2an ⊢ ( 1 0 ↑ 3 0 ) ∈ ℕ
34 2 33 nnmulcli ⊢ ( 8 · ( 1 0 ↑ 3 0 ) ) ∈ ℕ
35 34 nnrei ⊢ ( 8 · ( 1 0 ↑ 3 0 ) ) ∈ ℝ
36 28 35 ltaddposi ⊢ ( 0 < ( 8 · ( 1 0 ↑ 2 9 ) ) ↔ ( 8 · ( 1 0 ↑ 3 0 ) ) < ( ( 8 · ( 1 0 ↑ 3 0 ) ) + ( 8 · ( 1 0 ↑ 2 9 ) ) ) )
37 27 36 mpbi ⊢ ( 8 · ( 1 0 ↑ 3 0 ) ) < ( ( 8 · ( 1 0 ↑ 3 0 ) ) + ( 8 · ( 1 0 ↑ 2 9 ) ) )
38 dfdec10 ⊢ 8 8 = ( ( 1 0 · 8 ) + 8 )
39 38 oveq1i ⊢ ( 8 8 · ( 1 0 ↑ 2 9 ) ) = ( ( ( 1 0 · 8 ) + 8 ) · ( 1 0 ↑ 2 9 ) )
40 4 2 nnmulcli ⊢ ( 1 0 · 8 ) ∈ ℕ
41 40 nncni ⊢ ( 1 0 · 8 ) ∈ ℂ
42 8cn ⊢ 8 ∈ ℂ
43 9 nncni ⊢ ( 1 0 ↑ 2 9 ) ∈ ℂ
44 41 42 43 adddiri ⊢ ( ( ( 1 0 · 8 ) + 8 ) · ( 1 0 ↑ 2 9 ) ) = ( ( ( 1 0 · 8 ) · ( 1 0 ↑ 2 9 ) ) + ( 8 · ( 1 0 ↑ 2 9 ) ) )
45 41 43 mulcomi ⊢ ( ( 1 0 · 8 ) · ( 1 0 ↑ 2 9 ) ) = ( ( 1 0 ↑ 2 9 ) · ( 1 0 · 8 ) )
46 4 nncni ⊢ 1 0 ∈ ℂ
47 43 46 42 mulassi ⊢ ( ( ( 1 0 ↑ 2 9 ) · 1 0 ) · 8 ) = ( ( 1 0 ↑ 2 9 ) · ( 1 0 · 8 ) )
48 nncn ⊢ ( 1 0 ∈ ℕ → 1 0 ∈ ℂ )
49 7 a1i ⊢ ( 1 0 ∈ ℕ → 2 9 ∈ ℕ0 )
50 48 49 expp1d ⊢ ( 1 0 ∈ ℕ → ( 1 0 ↑ ( 2 9 + 1 ) ) = ( ( 1 0 ↑ 2 9 ) · 1 0 ) )
51 4 50 ax-mp ⊢ ( 1 0 ↑ ( 2 9 + 1 ) ) = ( ( 1 0 ↑ 2 9 ) · 1 0 )
52 51 eqcomi ⊢ ( ( 1 0 ↑ 2 9 ) · 1 0 ) = ( 1 0 ↑ ( 2 9 + 1 ) )
53 52 oveq1i ⊢ ( ( ( 1 0 ↑ 2 9 ) · 1 0 ) · 8 ) = ( ( 1 0 ↑ ( 2 9 + 1 ) ) · 8 )
54 45 47 53 3eqtr2i ⊢ ( ( 1 0 · 8 ) · ( 1 0 ↑ 2 9 ) ) = ( ( 1 0 ↑ ( 2 9 + 1 ) ) · 8 )
55 54 oveq1i ⊢ ( ( ( 1 0 · 8 ) · ( 1 0 ↑ 2 9 ) ) + ( 8 · ( 1 0 ↑ 2 9 ) ) ) = ( ( ( 1 0 ↑ ( 2 9 + 1 ) ) · 8 ) + ( 8 · ( 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 ) ) · 8 ) = ( ( 1 0 ↑ 3 0 ) · 8 )
61 60 oveq1i ⊢ ( ( ( 1 0 ↑ ( 2 9 + 1 ) ) · 8 ) + ( 8 · ( 1 0 ↑ 2 9 ) ) ) = ( ( ( 1 0 ↑ 3 0 ) · 8 ) + ( 8 · ( 1 0 ↑ 2 9 ) ) )
62 33 nncni ⊢ ( 1 0 ↑ 3 0 ) ∈ ℂ
63 mulcom ⊢ ( ( ( 1 0 ↑ 3 0 ) ∈ ℂ ∧ 8 ∈ ℂ ) → ( ( 1 0 ↑ 3 0 ) · 8 ) = ( 8 · ( 1 0 ↑ 3 0 ) ) )
64 63 oveq1d ⊢ ( ( ( 1 0 ↑ 3 0 ) ∈ ℂ ∧ 8 ∈ ℂ ) → ( ( ( 1 0 ↑ 3 0 ) · 8 ) + ( 8 · ( 1 0 ↑ 2 9 ) ) ) = ( ( 8 · ( 1 0 ↑ 3 0 ) ) + ( 8 · ( 1 0 ↑ 2 9 ) ) ) )
65 62 42 64 mp2an ⊢ ( ( ( 1 0 ↑ 3 0 ) · 8 ) + ( 8 · ( 1 0 ↑ 2 9 ) ) ) = ( ( 8 · ( 1 0 ↑ 3 0 ) ) + ( 8 · ( 1 0 ↑ 2 9 ) ) )
66 55 61 65 3eqtri ⊢ ( ( ( 1 0 · 8 ) · ( 1 0 ↑ 2 9 ) ) + ( 8 · ( 1 0 ↑ 2 9 ) ) ) = ( ( 8 · ( 1 0 ↑ 3 0 ) ) + ( 8 · ( 1 0 ↑ 2 9 ) ) )
67 39 44 66 3eqtri ⊢ ( 8 8 · ( 1 0 ↑ 2 9 ) ) = ( ( 8 · ( 1 0 ↑ 3 0 ) ) + ( 8 · ( 1 0 ↑ 2 9 ) ) )
68 37 67 breqtrri ⊢ ( 8 · ( 1 0 ↑ 3 0 ) ) < ( 8 8 · ( 1 0 ↑ 2 9 ) )
69 25 68 jctil ⊢ ( ( 8 8 · ( 1 0 ↑ 2 9 ) ) ∈ ℕ → ( ( 8 · ( 1 0 ↑ 3 0 ) ) < ( 8 8 · ( 1 0 ↑ 2 9 ) ) ∧ ∀ 𝑛 ∈ Odd ( ( 7 < 𝑛 ∧ 𝑛 < ( 8 8 · ( 1 0 ↑ 2 9 ) ) ) → 𝑛 ∈ GoldbachOdd ) ) )
70 11 18 69 rspcedvd ⊢ ( ( 8 8 · ( 1 0 ↑ 2 9 ) ) ∈ ℕ → ∃ 𝑚 ∈ ℕ ( ( 8 · ( 1 0 ↑ 3 0 ) ) < 𝑚 ∧ ∀ 𝑛 ∈ Odd ( ( 7 < 𝑛 ∧ 𝑛 < 𝑚 ) → 𝑛 ∈ GoldbachOdd ) ) )
71 10 70 ax-mp ⊢ ∃ 𝑚 ∈ ℕ ( ( 8 · ( 1 0 ↑ 3 0 ) ) < 𝑚 ∧ ∀ 𝑛 ∈ Odd ( ( 7 < 𝑛 ∧ 𝑛 < 𝑚 ) → 𝑛 ∈ GoldbachOdd ) )