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 ⊢ ∃ m ∈ ℕ 8 ⁢ 10 30 < m ∧ ∀ n ∈ Odd 7 < n ∧ n < m → n ∈ GoldbachOdd

Proof

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