Metamath Proof Explorer

Theorem tgblthelfgott

Description: The ternary Goldbach conjecture is valid for all odd numbers less than 8.8 x 10^30 (actually 8.875694 x 10^30, see section 1.2.2 in Helfgott p. 4, using bgoldbachlt , ax-hgprmladder and bgoldbtbnd . (Contributed by AV, 4-Aug-2020) (Revised by AV, 9-Sep-2021)

Ref Expression
Assertion tgblthelfgott ( ( 𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < ( 8 8 · ( 1 0 ↑ 2 9 ) ) ) → 𝑁 ∈ GoldbachOdd )

Proof

Step Hyp Ref Expression
1 ax-hgprmladder ⊢ ∃ 𝑑 ∈ ( ℤ≥ ‘ 3 ) ∃ 𝑓 ∈ ( RePart ‘ 𝑑 ) ( ( ( 𝑓 ‘ 0 ) = 7 ∧ ( 𝑓 ‘ 1 ) = 1 3 ∧ ( 𝑓 ‘ 𝑑 ) = ( 8 9 · ( 1 0 ↑ 2 9 ) ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑑 ) ( ( 𝑓 ‘ 𝑖 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) < ( ( 4 · ( 1 0 ↑ 1 8 ) ) − 4 ) ∧ 4 < ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) ) )
2 1nn0 ⊢ 1 ∈ ℕ0
3 1nn ⊢ 1 ∈ ℕ
4 2 3 decnncl ⊢ 1 1 ∈ ℕ
5 4 nnzi ⊢ 1 1 ∈ ℤ
6 8nn0 ⊢ 8 ∈ ℕ0
7 8nn ⊢ 8 ∈ ℕ
8 6 7 decnncl ⊢ 8 8 ∈ ℕ
9 10nn ⊢ 1 0 ∈ ℕ
10 2nn0 ⊢ 2 ∈ ℕ0
11 9nn ⊢ 9 ∈ ℕ
12 10 11 decnncl ⊢ 2 9 ∈ ℕ
13 12 nnnn0i ⊢ 2 9 ∈ ℕ0
14 nnexpcl ⊢ ( ( 1 0 ∈ ℕ ∧ 2 9 ∈ ℕ0 ) → ( 1 0 ↑ 2 9 ) ∈ ℕ )
15 9 13 14 mp2an ⊢ ( 1 0 ↑ 2 9 ) ∈ ℕ
16 8 15 nnmulcli ⊢ ( 8 8 · ( 1 0 ↑ 2 9 ) ) ∈ ℕ
17 16 nnzi ⊢ ( 8 8 · ( 1 0 ↑ 2 9 ) ) ∈ ℤ
18 1re ⊢ 1 ∈ ℝ
19 8 nnrei ⊢ 8 8 ∈ ℝ
20 18 19 pm3.2i ⊢ ( 1 ∈ ℝ ∧ 8 8 ∈ ℝ )
21 0le1 ⊢ 0 ≤ 1
22 1lt10 ⊢ 1 < 1 0
23 7 6 2 22 declti ⊢ 1 < 8 8
24 21 23 pm3.2i ⊢ ( 0 ≤ 1 ∧ 1 < 8 8 )
25 nnexpcl ⊢ ( ( 1 0 ∈ ℕ ∧ 1 ∈ ℕ0 ) → ( 1 0 ↑ 1 ) ∈ ℕ )
26 9 2 25 mp2an ⊢ ( 1 0 ↑ 1 ) ∈ ℕ
27 26 nnrei ⊢ ( 1 0 ↑ 1 ) ∈ ℝ
28 15 nnrei ⊢ ( 1 0 ↑ 2 9 ) ∈ ℝ
29 27 28 pm3.2i ⊢ ( ( 1 0 ↑ 1 ) ∈ ℝ ∧ ( 1 0 ↑ 2 9 ) ∈ ℝ )
30 0re ⊢ 0 ∈ ℝ
31 10re ⊢ 1 0 ∈ ℝ
32 10pos ⊢ 0 < 1 0
33 30 31 32 ltleii ⊢ 0 ≤ 1 0
34 9 nncni ⊢ 1 0 ∈ ℂ
35 exp1 ⊢ ( 1 0 ∈ ℂ → ( 1 0 ↑ 1 ) = 1 0 )
36 34 35 ax-mp ⊢ ( 1 0 ↑ 1 ) = 1 0
37 33 36 breqtrri ⊢ 0 ≤ ( 1 0 ↑ 1 )
38 1z ⊢ 1 ∈ ℤ
39 12 nnzi ⊢ 2 9 ∈ ℤ
40 31 38 39 3pm3.2i ⊢ ( 1 0 ∈ ℝ ∧ 1 ∈ ℤ ∧ 2 9 ∈ ℤ )
41 2nn ⊢ 2 ∈ ℕ
42 9nn0 ⊢ 9 ∈ ℕ0
43 41 42 2 22 declti ⊢ 1 < 2 9
44 22 43 pm3.2i ⊢ ( 1 < 1 0 ∧ 1 < 2 9 )
45 ltexp2a ⊢ ( ( ( 1 0 ∈ ℝ ∧ 1 ∈ ℤ ∧ 2 9 ∈ ℤ ) ∧ ( 1 < 1 0 ∧ 1 < 2 9 ) ) → ( 1 0 ↑ 1 ) < ( 1 0 ↑ 2 9 ) )
46 40 44 45 mp2an ⊢ ( 1 0 ↑ 1 ) < ( 1 0 ↑ 2 9 )
47 37 46 pm3.2i ⊢ ( 0 ≤ ( 1 0 ↑ 1 ) ∧ ( 1 0 ↑ 1 ) < ( 1 0 ↑ 2 9 ) )
48 ltmul12a ⊢ ( ( ( ( 1 ∈ ℝ ∧ 8 8 ∈ ℝ ) ∧ ( 0 ≤ 1 ∧ 1 < 8 8 ) ) ∧ ( ( ( 1 0 ↑ 1 ) ∈ ℝ ∧ ( 1 0 ↑ 2 9 ) ∈ ℝ ) ∧ ( 0 ≤ ( 1 0 ↑ 1 ) ∧ ( 1 0 ↑ 1 ) < ( 1 0 ↑ 2 9 ) ) ) ) → ( 1 · ( 1 0 ↑ 1 ) ) < ( 8 8 · ( 1 0 ↑ 2 9 ) ) )
49 20 24 29 47 48 mp4an ⊢ ( 1 · ( 1 0 ↑ 1 ) ) < ( 8 8 · ( 1 0 ↑ 2 9 ) )
50 26 nnzi ⊢ ( 1 0 ↑ 1 ) ∈ ℤ
51 zmulcl ⊢ ( ( 1 ∈ ℤ ∧ ( 1 0 ↑ 1 ) ∈ ℤ ) → ( 1 · ( 1 0 ↑ 1 ) ) ∈ ℤ )
52 38 50 51 mp2an ⊢ ( 1 · ( 1 0 ↑ 1 ) ) ∈ ℤ
53 zltp1le ⊢ ( ( ( 1 · ( 1 0 ↑ 1 ) ) ∈ ℤ ∧ ( 8 8 · ( 1 0 ↑ 2 9 ) ) ∈ ℤ ) → ( ( 1 · ( 1 0 ↑ 1 ) ) < ( 8 8 · ( 1 0 ↑ 2 9 ) ) ↔ ( ( 1 · ( 1 0 ↑ 1 ) ) + 1 ) ≤ ( 8 8 · ( 1 0 ↑ 2 9 ) ) ) )
54 52 17 53 mp2an ⊢ ( ( 1 · ( 1 0 ↑ 1 ) ) < ( 8 8 · ( 1 0 ↑ 2 9 ) ) ↔ ( ( 1 · ( 1 0 ↑ 1 ) ) + 1 ) ≤ ( 8 8 · ( 1 0 ↑ 2 9 ) ) )
55 1t10e1p1e11 ⊢ 1 1 = ( ( 1 · ( 1 0 ↑ 1 ) ) + 1 )
56 55 eqcomi ⊢ ( ( 1 · ( 1 0 ↑ 1 ) ) + 1 ) = 1 1
57 56 breq1i ⊢ ( ( ( 1 · ( 1 0 ↑ 1 ) ) + 1 ) ≤ ( 8 8 · ( 1 0 ↑ 2 9 ) ) ↔ 1 1 ≤ ( 8 8 · ( 1 0 ↑ 2 9 ) ) )
58 54 57 bitri ⊢ ( ( 1 · ( 1 0 ↑ 1 ) ) < ( 8 8 · ( 1 0 ↑ 2 9 ) ) ↔ 1 1 ≤ ( 8 8 · ( 1 0 ↑ 2 9 ) ) )
59 49 58 mpbi ⊢ 1 1 ≤ ( 8 8 · ( 1 0 ↑ 2 9 ) )
60 eluz2 ⊢ ( ( 8 8 · ( 1 0 ↑ 2 9 ) ) ∈ ( ℤ≥ ‘ 1 1 ) ↔ ( 1 1 ∈ ℤ ∧ ( 8 8 · ( 1 0 ↑ 2 9 ) ) ∈ ℤ ∧ 1 1 ≤ ( 8 8 · ( 1 0 ↑ 2 9 ) ) ) )
61 5 17 59 60 mpbir3an ⊢ ( 8 8 · ( 1 0 ↑ 2 9 ) ) ∈ ( ℤ≥ ‘ 1 1 )
62 61 a1i ⊢ ( ( ( ( 𝑑 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑓 ∈ ( RePart ‘ 𝑑 ) ) ∧ ( ( ( 𝑓 ‘ 0 ) = 7 ∧ ( 𝑓 ‘ 1 ) = 1 3 ∧ ( 𝑓 ‘ 𝑑 ) = ( 8 9 · ( 1 0 ↑ 2 9 ) ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑑 ) ( ( 𝑓 ‘ 𝑖 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) < ( ( 4 · ( 1 0 ↑ 1 8 ) ) − 4 ) ∧ 4 < ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) ) ) ) ∧ ( 𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < ( 8 8 · ( 1 0 ↑ 2 9 ) ) ) ) → ( 8 8 · ( 1 0 ↑ 2 9 ) ) ∈ ( ℤ≥ ‘ 1 1 ) )
63 4nn ⊢ 4 ∈ ℕ
64 2 7 decnncl ⊢ 1 8 ∈ ℕ
65 64 nnnn0i ⊢ 1 8 ∈ ℕ0
66 nnexpcl ⊢ ( ( 1 0 ∈ ℕ ∧ 1 8 ∈ ℕ0 ) → ( 1 0 ↑ 1 8 ) ∈ ℕ )
67 9 65 66 mp2an ⊢ ( 1 0 ↑ 1 8 ) ∈ ℕ
68 63 67 nnmulcli ⊢ ( 4 · ( 1 0 ↑ 1 8 ) ) ∈ ℕ
69 68 nnzi ⊢ ( 4 · ( 1 0 ↑ 1 8 ) ) ∈ ℤ
70 4re ⊢ 4 ∈ ℝ
71 18 70 pm3.2i ⊢ ( 1 ∈ ℝ ∧ 4 ∈ ℝ )
72 1lt4 ⊢ 1 < 4
73 21 72 pm3.2i ⊢ ( 0 ≤ 1 ∧ 1 < 4 )
74 67 nnrei ⊢ ( 1 0 ↑ 1 8 ) ∈ ℝ
75 27 74 pm3.2i ⊢ ( ( 1 0 ↑ 1 ) ∈ ℝ ∧ ( 1 0 ↑ 1 8 ) ∈ ℝ )
76 64 nnzi ⊢ 1 8 ∈ ℤ
77 31 38 76 3pm3.2i ⊢ ( 1 0 ∈ ℝ ∧ 1 ∈ ℤ ∧ 1 8 ∈ ℤ )
78 3 6 2 22 declti ⊢ 1 < 1 8
79 22 78 pm3.2i ⊢ ( 1 < 1 0 ∧ 1 < 1 8 )
80 ltexp2a ⊢ ( ( ( 1 0 ∈ ℝ ∧ 1 ∈ ℤ ∧ 1 8 ∈ ℤ ) ∧ ( 1 < 1 0 ∧ 1 < 1 8 ) ) → ( 1 0 ↑ 1 ) < ( 1 0 ↑ 1 8 ) )
81 77 79 80 mp2an ⊢ ( 1 0 ↑ 1 ) < ( 1 0 ↑ 1 8 )
82 37 81 pm3.2i ⊢ ( 0 ≤ ( 1 0 ↑ 1 ) ∧ ( 1 0 ↑ 1 ) < ( 1 0 ↑ 1 8 ) )
83 ltmul12a ⊢ ( ( ( ( 1 ∈ ℝ ∧ 4 ∈ ℝ ) ∧ ( 0 ≤ 1 ∧ 1 < 4 ) ) ∧ ( ( ( 1 0 ↑ 1 ) ∈ ℝ ∧ ( 1 0 ↑ 1 8 ) ∈ ℝ ) ∧ ( 0 ≤ ( 1 0 ↑ 1 ) ∧ ( 1 0 ↑ 1 ) < ( 1 0 ↑ 1 8 ) ) ) ) → ( 1 · ( 1 0 ↑ 1 ) ) < ( 4 · ( 1 0 ↑ 1 8 ) ) )
84 71 73 75 82 83 mp4an ⊢ ( 1 · ( 1 0 ↑ 1 ) ) < ( 4 · ( 1 0 ↑ 1 8 ) )
85 4z ⊢ 4 ∈ ℤ
86 67 nnzi ⊢ ( 1 0 ↑ 1 8 ) ∈ ℤ
87 zmulcl ⊢ ( ( 4 ∈ ℤ ∧ ( 1 0 ↑ 1 8 ) ∈ ℤ ) → ( 4 · ( 1 0 ↑ 1 8 ) ) ∈ ℤ )
88 85 86 87 mp2an ⊢ ( 4 · ( 1 0 ↑ 1 8 ) ) ∈ ℤ
89 zltp1le ⊢ ( ( ( 1 · ( 1 0 ↑ 1 ) ) ∈ ℤ ∧ ( 4 · ( 1 0 ↑ 1 8 ) ) ∈ ℤ ) → ( ( 1 · ( 1 0 ↑ 1 ) ) < ( 4 · ( 1 0 ↑ 1 8 ) ) ↔ ( ( 1 · ( 1 0 ↑ 1 ) ) + 1 ) ≤ ( 4 · ( 1 0 ↑ 1 8 ) ) ) )
90 52 88 89 mp2an ⊢ ( ( 1 · ( 1 0 ↑ 1 ) ) < ( 4 · ( 1 0 ↑ 1 8 ) ) ↔ ( ( 1 · ( 1 0 ↑ 1 ) ) + 1 ) ≤ ( 4 · ( 1 0 ↑ 1 8 ) ) )
91 56 breq1i ⊢ ( ( ( 1 · ( 1 0 ↑ 1 ) ) + 1 ) ≤ ( 4 · ( 1 0 ↑ 1 8 ) ) ↔ 1 1 ≤ ( 4 · ( 1 0 ↑ 1 8 ) ) )
92 90 91 bitri ⊢ ( ( 1 · ( 1 0 ↑ 1 ) ) < ( 4 · ( 1 0 ↑ 1 8 ) ) ↔ 1 1 ≤ ( 4 · ( 1 0 ↑ 1 8 ) ) )
93 84 92 mpbi ⊢ 1 1 ≤ ( 4 · ( 1 0 ↑ 1 8 ) )
94 eluz2 ⊢ ( ( 4 · ( 1 0 ↑ 1 8 ) ) ∈ ( ℤ≥ ‘ 1 1 ) ↔ ( 1 1 ∈ ℤ ∧ ( 4 · ( 1 0 ↑ 1 8 ) ) ∈ ℤ ∧ 1 1 ≤ ( 4 · ( 1 0 ↑ 1 8 ) ) ) )
95 5 69 93 94 mpbir3an ⊢ ( 4 · ( 1 0 ↑ 1 8 ) ) ∈ ( ℤ≥ ‘ 1 1 )
96 95 a1i ⊢ ( ( ( ( 𝑑 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑓 ∈ ( RePart ‘ 𝑑 ) ) ∧ ( ( ( 𝑓 ‘ 0 ) = 7 ∧ ( 𝑓 ‘ 1 ) = 1 3 ∧ ( 𝑓 ‘ 𝑑 ) = ( 8 9 · ( 1 0 ↑ 2 9 ) ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑑 ) ( ( 𝑓 ‘ 𝑖 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) < ( ( 4 · ( 1 0 ↑ 1 8 ) ) − 4 ) ∧ 4 < ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) ) ) ) ∧ ( 𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < ( 8 8 · ( 1 0 ↑ 2 9 ) ) ) ) → ( 4 · ( 1 0 ↑ 1 8 ) ) ∈ ( ℤ≥ ‘ 1 1 ) )
97 simpl ⊢ ( ( 𝑛 ∈ Even ∧ ( 4 < 𝑛 ∧ 𝑛 < ( 4 · ( 1 0 ↑ 1 8 ) ) ) ) → 𝑛 ∈ Even )
98 simprl ⊢ ( ( 𝑛 ∈ Even ∧ ( 4 < 𝑛 ∧ 𝑛 < ( 4 · ( 1 0 ↑ 1 8 ) ) ) ) → 4 < 𝑛 )
99 evenz ⊢ ( 𝑛 ∈ Even → 𝑛 ∈ ℤ )
100 99 zred ⊢ ( 𝑛 ∈ Even → 𝑛 ∈ ℝ )
101 68 nnrei ⊢ ( 4 · ( 1 0 ↑ 1 8 ) ) ∈ ℝ
102 ltle ⊢ ( ( 𝑛 ∈ ℝ ∧ ( 4 · ( 1 0 ↑ 1 8 ) ) ∈ ℝ ) → ( 𝑛 < ( 4 · ( 1 0 ↑ 1 8 ) ) → 𝑛 ≤ ( 4 · ( 1 0 ↑ 1 8 ) ) ) )
103 100 101 102 sylancl ⊢ ( 𝑛 ∈ Even → ( 𝑛 < ( 4 · ( 1 0 ↑ 1 8 ) ) → 𝑛 ≤ ( 4 · ( 1 0 ↑ 1 8 ) ) ) )
104 103 a1d ⊢ ( 𝑛 ∈ Even → ( 4 < 𝑛 → ( 𝑛 < ( 4 · ( 1 0 ↑ 1 8 ) ) → 𝑛 ≤ ( 4 · ( 1 0 ↑ 1 8 ) ) ) ) )
105 104 imp32 ⊢ ( ( 𝑛 ∈ Even ∧ ( 4 < 𝑛 ∧ 𝑛 < ( 4 · ( 1 0 ↑ 1 8 ) ) ) ) → 𝑛 ≤ ( 4 · ( 1 0 ↑ 1 8 ) ) )
106 ax-bgbltosilva ⊢ ( ( 𝑛 ∈ Even ∧ 4 < 𝑛 ∧ 𝑛 ≤ ( 4 · ( 1 0 ↑ 1 8 ) ) ) → 𝑛 ∈ GoldbachEven )
107 97 98 105 106 syl3anc ⊢ ( ( 𝑛 ∈ Even ∧ ( 4 < 𝑛 ∧ 𝑛 < ( 4 · ( 1 0 ↑ 1 8 ) ) ) ) → 𝑛 ∈ GoldbachEven )
108 107 ex ⊢ ( 𝑛 ∈ Even → ( ( 4 < 𝑛 ∧ 𝑛 < ( 4 · ( 1 0 ↑ 1 8 ) ) ) → 𝑛 ∈ GoldbachEven ) )
109 108 a1i ⊢ ( ( ( ( 𝑑 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑓 ∈ ( RePart ‘ 𝑑 ) ) ∧ ( ( ( 𝑓 ‘ 0 ) = 7 ∧ ( 𝑓 ‘ 1 ) = 1 3 ∧ ( 𝑓 ‘ 𝑑 ) = ( 8 9 · ( 1 0 ↑ 2 9 ) ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑑 ) ( ( 𝑓 ‘ 𝑖 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) < ( ( 4 · ( 1 0 ↑ 1 8 ) ) − 4 ) ∧ 4 < ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) ) ) ) ∧ ( 𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < ( 8 8 · ( 1 0 ↑ 2 9 ) ) ) ) → ( 𝑛 ∈ Even → ( ( 4 < 𝑛 ∧ 𝑛 < ( 4 · ( 1 0 ↑ 1 8 ) ) ) → 𝑛 ∈ GoldbachEven ) ) )
110 109 ralrimiv ⊢ ( ( ( ( 𝑑 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑓 ∈ ( RePart ‘ 𝑑 ) ) ∧ ( ( ( 𝑓 ‘ 0 ) = 7 ∧ ( 𝑓 ‘ 1 ) = 1 3 ∧ ( 𝑓 ‘ 𝑑 ) = ( 8 9 · ( 1 0 ↑ 2 9 ) ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑑 ) ( ( 𝑓 ‘ 𝑖 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) < ( ( 4 · ( 1 0 ↑ 1 8 ) ) − 4 ) ∧ 4 < ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) ) ) ) ∧ ( 𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < ( 8 8 · ( 1 0 ↑ 2 9 ) ) ) ) → ∀ 𝑛 ∈ Even ( ( 4 < 𝑛 ∧ 𝑛 < ( 4 · ( 1 0 ↑ 1 8 ) ) ) → 𝑛 ∈ GoldbachEven ) )
111 simpl ⊢ ( ( 𝑑 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑓 ∈ ( RePart ‘ 𝑑 ) ) → 𝑑 ∈ ( ℤ≥ ‘ 3 ) )
112 111 ad2antrr ⊢ ( ( ( ( 𝑑 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑓 ∈ ( RePart ‘ 𝑑 ) ) ∧ ( ( ( 𝑓 ‘ 0 ) = 7 ∧ ( 𝑓 ‘ 1 ) = 1 3 ∧ ( 𝑓 ‘ 𝑑 ) = ( 8 9 · ( 1 0 ↑ 2 9 ) ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑑 ) ( ( 𝑓 ‘ 𝑖 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) < ( ( 4 · ( 1 0 ↑ 1 8 ) ) − 4 ) ∧ 4 < ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) ) ) ) ∧ ( 𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < ( 8 8 · ( 1 0 ↑ 2 9 ) ) ) ) → 𝑑 ∈ ( ℤ≥ ‘ 3 ) )
113 simpr ⊢ ( ( 𝑑 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑓 ∈ ( RePart ‘ 𝑑 ) ) → 𝑓 ∈ ( RePart ‘ 𝑑 ) )
114 113 ad2antrr ⊢ ( ( ( ( 𝑑 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑓 ∈ ( RePart ‘ 𝑑 ) ) ∧ ( ( ( 𝑓 ‘ 0 ) = 7 ∧ ( 𝑓 ‘ 1 ) = 1 3 ∧ ( 𝑓 ‘ 𝑑 ) = ( 8 9 · ( 1 0 ↑ 2 9 ) ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑑 ) ( ( 𝑓 ‘ 𝑖 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) < ( ( 4 · ( 1 0 ↑ 1 8 ) ) − 4 ) ∧ 4 < ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) ) ) ) ∧ ( 𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < ( 8 8 · ( 1 0 ↑ 2 9 ) ) ) ) → 𝑓 ∈ ( RePart ‘ 𝑑 ) )
115 simpr ⊢ ( ( ( ( 𝑓 ‘ 0 ) = 7 ∧ ( 𝑓 ‘ 1 ) = 1 3 ∧ ( 𝑓 ‘ 𝑑 ) = ( 8 9 · ( 1 0 ↑ 2 9 ) ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑑 ) ( ( 𝑓 ‘ 𝑖 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) < ( ( 4 · ( 1 0 ↑ 1 8 ) ) − 4 ) ∧ 4 < ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) ) ) → ∀ 𝑖 ∈ ( 0 ..^ 𝑑 ) ( ( 𝑓 ‘ 𝑖 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) < ( ( 4 · ( 1 0 ↑ 1 8 ) ) − 4 ) ∧ 4 < ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) ) )
116 115 ad2antlr ⊢ ( ( ( ( 𝑑 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑓 ∈ ( RePart ‘ 𝑑 ) ) ∧ ( ( ( 𝑓 ‘ 0 ) = 7 ∧ ( 𝑓 ‘ 1 ) = 1 3 ∧ ( 𝑓 ‘ 𝑑 ) = ( 8 9 · ( 1 0 ↑ 2 9 ) ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑑 ) ( ( 𝑓 ‘ 𝑖 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) < ( ( 4 · ( 1 0 ↑ 1 8 ) ) − 4 ) ∧ 4 < ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) ) ) ) ∧ ( 𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < ( 8 8 · ( 1 0 ↑ 2 9 ) ) ) ) → ∀ 𝑖 ∈ ( 0 ..^ 𝑑 ) ( ( 𝑓 ‘ 𝑖 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) < ( ( 4 · ( 1 0 ↑ 1 8 ) ) − 4 ) ∧ 4 < ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) ) )
117 simpl1 ⊢ ( ( ( ( 𝑓 ‘ 0 ) = 7 ∧ ( 𝑓 ‘ 1 ) = 1 3 ∧ ( 𝑓 ‘ 𝑑 ) = ( 8 9 · ( 1 0 ↑ 2 9 ) ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑑 ) ( ( 𝑓 ‘ 𝑖 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) < ( ( 4 · ( 1 0 ↑ 1 8 ) ) − 4 ) ∧ 4 < ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) ) ) → ( 𝑓 ‘ 0 ) = 7 )
118 117 ad2antlr ⊢ ( ( ( ( 𝑑 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑓 ∈ ( RePart ‘ 𝑑 ) ) ∧ ( ( ( 𝑓 ‘ 0 ) = 7 ∧ ( 𝑓 ‘ 1 ) = 1 3 ∧ ( 𝑓 ‘ 𝑑 ) = ( 8 9 · ( 1 0 ↑ 2 9 ) ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑑 ) ( ( 𝑓 ‘ 𝑖 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) < ( ( 4 · ( 1 0 ↑ 1 8 ) ) − 4 ) ∧ 4 < ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) ) ) ) ∧ ( 𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < ( 8 8 · ( 1 0 ↑ 2 9 ) ) ) ) → ( 𝑓 ‘ 0 ) = 7 )
119 simpl2 ⊢ ( ( ( ( 𝑓 ‘ 0 ) = 7 ∧ ( 𝑓 ‘ 1 ) = 1 3 ∧ ( 𝑓 ‘ 𝑑 ) = ( 8 9 · ( 1 0 ↑ 2 9 ) ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑑 ) ( ( 𝑓 ‘ 𝑖 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) < ( ( 4 · ( 1 0 ↑ 1 8 ) ) − 4 ) ∧ 4 < ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) ) ) → ( 𝑓 ‘ 1 ) = 1 3 )
120 119 ad2antlr ⊢ ( ( ( ( 𝑑 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑓 ∈ ( RePart ‘ 𝑑 ) ) ∧ ( ( ( 𝑓 ‘ 0 ) = 7 ∧ ( 𝑓 ‘ 1 ) = 1 3 ∧ ( 𝑓 ‘ 𝑑 ) = ( 8 9 · ( 1 0 ↑ 2 9 ) ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑑 ) ( ( 𝑓 ‘ 𝑖 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) < ( ( 4 · ( 1 0 ↑ 1 8 ) ) − 4 ) ∧ 4 < ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) ) ) ) ∧ ( 𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < ( 8 8 · ( 1 0 ↑ 2 9 ) ) ) ) → ( 𝑓 ‘ 1 ) = 1 3 )
121 6 11 decnncl ⊢ 8 9 ∈ ℕ
122 121 nnrei ⊢ 8 9 ∈ ℝ
123 15 nngt0i ⊢ 0 < ( 1 0 ↑ 2 9 )
124 28 123 pm3.2i ⊢ ( ( 1 0 ↑ 2 9 ) ∈ ℝ ∧ 0 < ( 1 0 ↑ 2 9 ) )
125 19 122 124 3pm3.2i ⊢ ( 8 8 ∈ ℝ ∧ 8 9 ∈ ℝ ∧ ( ( 1 0 ↑ 2 9 ) ∈ ℝ ∧ 0 < ( 1 0 ↑ 2 9 ) ) )
126 8lt9 ⊢ 8 < 9
127 6 6 11 126 declt ⊢ 8 8 < 8 9
128 ltmul1a ⊢ ( ( ( 8 8 ∈ ℝ ∧ 8 9 ∈ ℝ ∧ ( ( 1 0 ↑ 2 9 ) ∈ ℝ ∧ 0 < ( 1 0 ↑ 2 9 ) ) ) ∧ 8 8 < 8 9 ) → ( 8 8 · ( 1 0 ↑ 2 9 ) ) < ( 8 9 · ( 1 0 ↑ 2 9 ) ) )
129 125 127 128 mp2an ⊢ ( 8 8 · ( 1 0 ↑ 2 9 ) ) < ( 8 9 · ( 1 0 ↑ 2 9 ) )
130 breq2 ⊢ ( ( 𝑓 ‘ 𝑑 ) = ( 8 9 · ( 1 0 ↑ 2 9 ) ) → ( ( 8 8 · ( 1 0 ↑ 2 9 ) ) < ( 𝑓 ‘ 𝑑 ) ↔ ( 8 8 · ( 1 0 ↑ 2 9 ) ) < ( 8 9 · ( 1 0 ↑ 2 9 ) ) ) )
131 129 130 mpbiri ⊢ ( ( 𝑓 ‘ 𝑑 ) = ( 8 9 · ( 1 0 ↑ 2 9 ) ) → ( 8 8 · ( 1 0 ↑ 2 9 ) ) < ( 𝑓 ‘ 𝑑 ) )
132 131 3ad2ant3 ⊢ ( ( ( 𝑓 ‘ 0 ) = 7 ∧ ( 𝑓 ‘ 1 ) = 1 3 ∧ ( 𝑓 ‘ 𝑑 ) = ( 8 9 · ( 1 0 ↑ 2 9 ) ) ) → ( 8 8 · ( 1 0 ↑ 2 9 ) ) < ( 𝑓 ‘ 𝑑 ) )
133 132 adantr ⊢ ( ( ( ( 𝑓 ‘ 0 ) = 7 ∧ ( 𝑓 ‘ 1 ) = 1 3 ∧ ( 𝑓 ‘ 𝑑 ) = ( 8 9 · ( 1 0 ↑ 2 9 ) ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑑 ) ( ( 𝑓 ‘ 𝑖 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) < ( ( 4 · ( 1 0 ↑ 1 8 ) ) − 4 ) ∧ 4 < ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) ) ) → ( 8 8 · ( 1 0 ↑ 2 9 ) ) < ( 𝑓 ‘ 𝑑 ) )
134 133 ad2antlr ⊢ ( ( ( ( 𝑑 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑓 ∈ ( RePart ‘ 𝑑 ) ) ∧ ( ( ( 𝑓 ‘ 0 ) = 7 ∧ ( 𝑓 ‘ 1 ) = 1 3 ∧ ( 𝑓 ‘ 𝑑 ) = ( 8 9 · ( 1 0 ↑ 2 9 ) ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑑 ) ( ( 𝑓 ‘ 𝑖 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) < ( ( 4 · ( 1 0 ↑ 1 8 ) ) − 4 ) ∧ 4 < ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) ) ) ) ∧ ( 𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < ( 8 8 · ( 1 0 ↑ 2 9 ) ) ) ) → ( 8 8 · ( 1 0 ↑ 2 9 ) ) < ( 𝑓 ‘ 𝑑 ) )
135 121 15 nnmulcli ⊢ ( 8 9 · ( 1 0 ↑ 2 9 ) ) ∈ ℕ
136 135 nnrei ⊢ ( 8 9 · ( 1 0 ↑ 2 9 ) ) ∈ ℝ
137 eleq1 ⊢ ( ( 𝑓 ‘ 𝑑 ) = ( 8 9 · ( 1 0 ↑ 2 9 ) ) → ( ( 𝑓 ‘ 𝑑 ) ∈ ℝ ↔ ( 8 9 · ( 1 0 ↑ 2 9 ) ) ∈ ℝ ) )
138 136 137 mpbiri ⊢ ( ( 𝑓 ‘ 𝑑 ) = ( 8 9 · ( 1 0 ↑ 2 9 ) ) → ( 𝑓 ‘ 𝑑 ) ∈ ℝ )
139 138 3ad2ant3 ⊢ ( ( ( 𝑓 ‘ 0 ) = 7 ∧ ( 𝑓 ‘ 1 ) = 1 3 ∧ ( 𝑓 ‘ 𝑑 ) = ( 8 9 · ( 1 0 ↑ 2 9 ) ) ) → ( 𝑓 ‘ 𝑑 ) ∈ ℝ )
140 139 adantr ⊢ ( ( ( ( 𝑓 ‘ 0 ) = 7 ∧ ( 𝑓 ‘ 1 ) = 1 3 ∧ ( 𝑓 ‘ 𝑑 ) = ( 8 9 · ( 1 0 ↑ 2 9 ) ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑑 ) ( ( 𝑓 ‘ 𝑖 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) < ( ( 4 · ( 1 0 ↑ 1 8 ) ) − 4 ) ∧ 4 < ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) ) ) → ( 𝑓 ‘ 𝑑 ) ∈ ℝ )
141 140 ad2antlr ⊢ ( ( ( ( 𝑑 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑓 ∈ ( RePart ‘ 𝑑 ) ) ∧ ( ( ( 𝑓 ‘ 0 ) = 7 ∧ ( 𝑓 ‘ 1 ) = 1 3 ∧ ( 𝑓 ‘ 𝑑 ) = ( 8 9 · ( 1 0 ↑ 2 9 ) ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑑 ) ( ( 𝑓 ‘ 𝑖 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) < ( ( 4 · ( 1 0 ↑ 1 8 ) ) − 4 ) ∧ 4 < ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) ) ) ) ∧ ( 𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < ( 8 8 · ( 1 0 ↑ 2 9 ) ) ) ) → ( 𝑓 ‘ 𝑑 ) ∈ ℝ )
142 62 96 110 112 114 116 118 120 134 141 bgoldbtbnd ⊢ ( ( ( ( 𝑑 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑓 ∈ ( RePart ‘ 𝑑 ) ) ∧ ( ( ( 𝑓 ‘ 0 ) = 7 ∧ ( 𝑓 ‘ 1 ) = 1 3 ∧ ( 𝑓 ‘ 𝑑 ) = ( 8 9 · ( 1 0 ↑ 2 9 ) ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑑 ) ( ( 𝑓 ‘ 𝑖 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) < ( ( 4 · ( 1 0 ↑ 1 8 ) ) − 4 ) ∧ 4 < ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) ) ) ) ∧ ( 𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < ( 8 8 · ( 1 0 ↑ 2 9 ) ) ) ) → ∀ 𝑛 ∈ Odd ( ( 7 < 𝑛 ∧ 𝑛 < ( 8 8 · ( 1 0 ↑ 2 9 ) ) ) → 𝑛 ∈ GoldbachOdd ) )
143 142 exp31 ⊢ ( ( 𝑑 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑓 ∈ ( RePart ‘ 𝑑 ) ) → ( ( ( ( 𝑓 ‘ 0 ) = 7 ∧ ( 𝑓 ‘ 1 ) = 1 3 ∧ ( 𝑓 ‘ 𝑑 ) = ( 8 9 · ( 1 0 ↑ 2 9 ) ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑑 ) ( ( 𝑓 ‘ 𝑖 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) < ( ( 4 · ( 1 0 ↑ 1 8 ) ) − 4 ) ∧ 4 < ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) ) ) → ( ( 𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < ( 8 8 · ( 1 0 ↑ 2 9 ) ) ) → ∀ 𝑛 ∈ Odd ( ( 7 < 𝑛 ∧ 𝑛 < ( 8 8 · ( 1 0 ↑ 2 9 ) ) ) → 𝑛 ∈ GoldbachOdd ) ) ) )
144 143 rexlimivv ⊢ ( ∃ 𝑑 ∈ ( ℤ≥ ‘ 3 ) ∃ 𝑓 ∈ ( RePart ‘ 𝑑 ) ( ( ( 𝑓 ‘ 0 ) = 7 ∧ ( 𝑓 ‘ 1 ) = 1 3 ∧ ( 𝑓 ‘ 𝑑 ) = ( 8 9 · ( 1 0 ↑ 2 9 ) ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑑 ) ( ( 𝑓 ‘ 𝑖 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) < ( ( 4 · ( 1 0 ↑ 1 8 ) ) − 4 ) ∧ 4 < ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) ) ) → ( ( 𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < ( 8 8 · ( 1 0 ↑ 2 9 ) ) ) → ∀ 𝑛 ∈ Odd ( ( 7 < 𝑛 ∧ 𝑛 < ( 8 8 · ( 1 0 ↑ 2 9 ) ) ) → 𝑛 ∈ GoldbachOdd ) ) )
145 breq2 ⊢ ( 𝑛 = 𝑁 → ( 7 < 𝑛 ↔ 7 < 𝑁 ) )
146 breq1 ⊢ ( 𝑛 = 𝑁 → ( 𝑛 < ( 8 8 · ( 1 0 ↑ 2 9 ) ) ↔ 𝑁 < ( 8 8 · ( 1 0 ↑ 2 9 ) ) ) )
147 145 146 anbi12d ⊢ ( 𝑛 = 𝑁 → ( ( 7 < 𝑛 ∧ 𝑛 < ( 8 8 · ( 1 0 ↑ 2 9 ) ) ) ↔ ( 7 < 𝑁 ∧ 𝑁 < ( 8 8 · ( 1 0 ↑ 2 9 ) ) ) ) )
148 eleq1 ⊢ ( 𝑛 = 𝑁 → ( 𝑛 ∈ GoldbachOdd ↔ 𝑁 ∈ GoldbachOdd ) )
149 147 148 imbi12d ⊢ ( 𝑛 = 𝑁 → ( ( ( 7 < 𝑛 ∧ 𝑛 < ( 8 8 · ( 1 0 ↑ 2 9 ) ) ) → 𝑛 ∈ GoldbachOdd ) ↔ ( ( 7 < 𝑁 ∧ 𝑁 < ( 8 8 · ( 1 0 ↑ 2 9 ) ) ) → 𝑁 ∈ GoldbachOdd ) ) )
150 149 rspcv ⊢ ( 𝑁 ∈ Odd → ( ∀ 𝑛 ∈ Odd ( ( 7 < 𝑛 ∧ 𝑛 < ( 8 8 · ( 1 0 ↑ 2 9 ) ) ) → 𝑛 ∈ GoldbachOdd ) → ( ( 7 < 𝑁 ∧ 𝑁 < ( 8 8 · ( 1 0 ↑ 2 9 ) ) ) → 𝑁 ∈ GoldbachOdd ) ) )
151 150 com23 ⊢ ( 𝑁 ∈ Odd → ( ( 7 < 𝑁 ∧ 𝑁 < ( 8 8 · ( 1 0 ↑ 2 9 ) ) ) → ( ∀ 𝑛 ∈ Odd ( ( 7 < 𝑛 ∧ 𝑛 < ( 8 8 · ( 1 0 ↑ 2 9 ) ) ) → 𝑛 ∈ GoldbachOdd ) → 𝑁 ∈ GoldbachOdd ) ) )
152 151 3impib ⊢ ( ( 𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < ( 8 8 · ( 1 0 ↑ 2 9 ) ) ) → ( ∀ 𝑛 ∈ Odd ( ( 7 < 𝑛 ∧ 𝑛 < ( 8 8 · ( 1 0 ↑ 2 9 ) ) ) → 𝑛 ∈ GoldbachOdd ) → 𝑁 ∈ GoldbachOdd ) )
153 144 152 sylcom ⊢ ( ∃ 𝑑 ∈ ( ℤ≥ ‘ 3 ) ∃ 𝑓 ∈ ( RePart ‘ 𝑑 ) ( ( ( 𝑓 ‘ 0 ) = 7 ∧ ( 𝑓 ‘ 1 ) = 1 3 ∧ ( 𝑓 ‘ 𝑑 ) = ( 8 9 · ( 1 0 ↑ 2 9 ) ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑑 ) ( ( 𝑓 ‘ 𝑖 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) < ( ( 4 · ( 1 0 ↑ 1 8 ) ) − 4 ) ∧ 4 < ( ( 𝑓 ‘ ( 𝑖 + 1 ) ) − ( 𝑓 ‘ 𝑖 ) ) ) ) → ( ( 𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < ( 8 8 · ( 1 0 ↑ 2 9 ) ) ) → 𝑁 ∈ GoldbachOdd ) )
154 1 153 ax-mp ⊢ ( ( 𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < ( 8 8 · ( 1 0 ↑ 2 9 ) ) ) → 𝑁 ∈ GoldbachOdd )