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 ∀ 𝑛 ∈ Odd ( 7 < 𝑛 → 𝑛 ∈ GoldbachOdd )

Proof

Step Hyp Ref Expression
1 oddz ⊢ ( 𝑛 ∈ Odd → 𝑛 ∈ ℤ )
2 1 zred ⊢ ( 𝑛 ∈ Odd → 𝑛 ∈ ℝ )
3 10re ⊢ 1 0 ∈ ℝ
4 2nn0 ⊢ 2 ∈ ℕ0
5 7nn ⊢ 7 ∈ ℕ
6 4 5 decnncl ⊢ 2 7 ∈ ℕ
7 6 nnnn0i ⊢ 2 7 ∈ ℕ0
8 reexpcl ⊢ ( ( 1 0 ∈ ℝ ∧ 2 7 ∈ ℕ0 ) → ( 1 0 ↑ 2 7 ) ∈ ℝ )
9 3 7 8 mp2an ⊢ ( 1 0 ↑ 2 7 ) ∈ ℝ
10 lelttric ⊢ ( ( 𝑛 ∈ ℝ ∧ ( 1 0 ↑ 2 7 ) ∈ ℝ ) → ( 𝑛 ≤ ( 1 0 ↑ 2 7 ) ∨ ( 1 0 ↑ 2 7 ) < 𝑛 ) )
11 2 9 10 sylancl ⊢ ( 𝑛 ∈ Odd → ( 𝑛 ≤ ( 1 0 ↑ 2 7 ) ∨ ( 1 0 ↑ 2 7 ) < 𝑛 ) )
12 tgoldbachlt ⊢ ∃ 𝑚 ∈ ℕ ( ( 8 · ( 1 0 ↑ 3 0 ) ) < 𝑚 ∧ ∀ 𝑜 ∈ Odd ( ( 7 < 𝑜 ∧ 𝑜 < 𝑚 ) → 𝑜 ∈ GoldbachOdd ) )
13 breq2 ⊢ ( 𝑜 = 𝑛 → ( 7 < 𝑜 ↔ 7 < 𝑛 ) )
14 breq1 ⊢ ( 𝑜 = 𝑛 → ( 𝑜 < 𝑚 ↔ 𝑛 < 𝑚 ) )
15 13 14 anbi12d ⊢ ( 𝑜 = 𝑛 → ( ( 7 < 𝑜 ∧ 𝑜 < 𝑚 ) ↔ ( 7 < 𝑛 ∧ 𝑛 < 𝑚 ) ) )
16 eleq1w ⊢ ( 𝑜 = 𝑛 → ( 𝑜 ∈ GoldbachOdd ↔ 𝑛 ∈ GoldbachOdd ) )
17 15 16 imbi12d ⊢ ( 𝑜 = 𝑛 → ( ( ( 7 < 𝑜 ∧ 𝑜 < 𝑚 ) → 𝑜 ∈ GoldbachOdd ) ↔ ( ( 7 < 𝑛 ∧ 𝑛 < 𝑚 ) → 𝑛 ∈ GoldbachOdd ) ) )
18 17 rspcv ⊢ ( 𝑛 ∈ Odd → ( ∀ 𝑜 ∈ Odd ( ( 7 < 𝑜 ∧ 𝑜 < 𝑚 ) → 𝑜 ∈ GoldbachOdd ) → ( ( 7 < 𝑛 ∧ 𝑛 < 𝑚 ) → 𝑛 ∈ GoldbachOdd ) ) )
19 9 recni ⊢ ( 1 0 ↑ 2 7 ) ∈ ℂ
20 19 mullidi ⊢ ( 1 · ( 1 0 ↑ 2 7 ) ) = ( 1 0 ↑ 2 7 )
21 1re ⊢ 1 ∈ ℝ
22 8re ⊢ 8 ∈ ℝ
23 21 22 pm3.2i ⊢ ( 1 ∈ ℝ ∧ 8 ∈ ℝ )
24 23 a1i ⊢ ( ( 𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ ) → ( 1 ∈ ℝ ∧ 8 ∈ ℝ ) )
25 0le1 ⊢ 0 ≤ 1
26 1lt8 ⊢ 1 < 8
27 25 26 pm3.2i ⊢ ( 0 ≤ 1 ∧ 1 < 8 )
28 27 a1i ⊢ ( ( 𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ ) → ( 0 ≤ 1 ∧ 1 < 8 ) )
29 3nn ⊢ 3 ∈ ℕ
30 29 decnncl2 ⊢ 3 0 ∈ ℕ
31 30 nnnn0i ⊢ 3 0 ∈ ℕ0
32 reexpcl ⊢ ( ( 1 0 ∈ ℝ ∧ 3 0 ∈ ℕ0 ) → ( 1 0 ↑ 3 0 ) ∈ ℝ )
33 3 31 32 mp2an ⊢ ( 1 0 ↑ 3 0 ) ∈ ℝ
34 9 33 pm3.2i ⊢ ( ( 1 0 ↑ 2 7 ) ∈ ℝ ∧ ( 1 0 ↑ 3 0 ) ∈ ℝ )
35 34 a1i ⊢ ( ( 𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ ) → ( ( 1 0 ↑ 2 7 ) ∈ ℝ ∧ ( 1 0 ↑ 3 0 ) ∈ ℝ ) )
36 10nn0 ⊢ 1 0 ∈ ℕ0
37 36 7 nn0expcli ⊢ ( 1 0 ↑ 2 7 ) ∈ ℕ0
38 37 nn0ge0i ⊢ 0 ≤ ( 1 0 ↑ 2 7 )
39 6 nnzi ⊢ 2 7 ∈ ℤ
40 30 nnzi ⊢ 3 0 ∈ ℤ
41 3 39 40 3pm3.2i ⊢ ( 1 0 ∈ ℝ ∧ 2 7 ∈ ℤ ∧ 3 0 ∈ ℤ )
42 1lt10 ⊢ 1 < 1 0
43 3nn0 ⊢ 3 ∈ ℕ0
44 7nn0 ⊢ 7 ∈ ℕ0
45 0nn0 ⊢ 0 ∈ ℕ0
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 ∈ ℝ ∧ 2 7 ∈ ℤ ∧ 3 0 ∈ ℤ ) ∧ ( 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 ⊢ ( ( 𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ ) → ( 0 ≤ ( 1 0 ↑ 2 7 ) ∧ ( 1 0 ↑ 2 7 ) < ( 1 0 ↑ 3 0 ) ) )
54 ltmul12a ⊢ ( ( ( ( 1 ∈ ℝ ∧ 8 ∈ ℝ ) ∧ ( 0 ≤ 1 ∧ 1 < 8 ) ) ∧ ( ( ( 1 0 ↑ 2 7 ) ∈ ℝ ∧ ( 1 0 ↑ 3 0 ) ∈ ℝ ) ∧ ( 0 ≤ ( 1 0 ↑ 2 7 ) ∧ ( 1 0 ↑ 2 7 ) < ( 1 0 ↑ 3 0 ) ) ) ) → ( 1 · ( 1 0 ↑ 2 7 ) ) < ( 8 · ( 1 0 ↑ 3 0 ) ) )
55 24 28 35 53 54 syl22anc ⊢ ( ( 𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ ) → ( 1 · ( 1 0 ↑ 2 7 ) ) < ( 8 · ( 1 0 ↑ 3 0 ) ) )
56 20 55 eqbrtrrid ⊢ ( ( 𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ ) → ( 1 0 ↑ 2 7 ) < ( 8 · ( 1 0 ↑ 3 0 ) ) )
57 9 a1i ⊢ ( ( 𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ ) → ( 1 0 ↑ 2 7 ) ∈ ℝ )
58 22 33 remulcli ⊢ ( 8 · ( 1 0 ↑ 3 0 ) ) ∈ ℝ
59 58 a1i ⊢ ( ( 𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ ) → ( 8 · ( 1 0 ↑ 3 0 ) ) ∈ ℝ )
60 nnre ⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℝ )
61 60 adantl ⊢ ( ( 𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ℝ )
62 lttr ⊢ ( ( ( 1 0 ↑ 2 7 ) ∈ ℝ ∧ ( 8 · ( 1 0 ↑ 3 0 ) ) ∈ ℝ ∧ 𝑚 ∈ ℝ ) → ( ( ( 1 0 ↑ 2 7 ) < ( 8 · ( 1 0 ↑ 3 0 ) ) ∧ ( 8 · ( 1 0 ↑ 3 0 ) ) < 𝑚 ) → ( 1 0 ↑ 2 7 ) < 𝑚 ) )
63 57 59 61 62 syl3anc ⊢ ( ( 𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ ) → ( ( ( 1 0 ↑ 2 7 ) < ( 8 · ( 1 0 ↑ 3 0 ) ) ∧ ( 8 · ( 1 0 ↑ 3 0 ) ) < 𝑚 ) → ( 1 0 ↑ 2 7 ) < 𝑚 ) )
64 56 63 mpand ⊢ ( ( 𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ ) → ( ( 8 · ( 1 0 ↑ 3 0 ) ) < 𝑚 → ( 1 0 ↑ 2 7 ) < 𝑚 ) )
65 64 imp ⊢ ( ( ( 𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ ) ∧ ( 8 · ( 1 0 ↑ 3 0 ) ) < 𝑚 ) → ( 1 0 ↑ 2 7 ) < 𝑚 )
66 2 adantr ⊢ ( ( 𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ ) → 𝑛 ∈ ℝ )
67 66 57 61 3jca ⊢ ( ( 𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ ) → ( 𝑛 ∈ ℝ ∧ ( 1 0 ↑ 2 7 ) ∈ ℝ ∧ 𝑚 ∈ ℝ ) )
68 67 adantr ⊢ ( ( ( 𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ ) ∧ ( 8 · ( 1 0 ↑ 3 0 ) ) < 𝑚 ) → ( 𝑛 ∈ ℝ ∧ ( 1 0 ↑ 2 7 ) ∈ ℝ ∧ 𝑚 ∈ ℝ ) )
69 lelttr ⊢ ( ( 𝑛 ∈ ℝ ∧ ( 1 0 ↑ 2 7 ) ∈ ℝ ∧ 𝑚 ∈ ℝ ) → ( ( 𝑛 ≤ ( 1 0 ↑ 2 7 ) ∧ ( 1 0 ↑ 2 7 ) < 𝑚 ) → 𝑛 < 𝑚 ) )
70 68 69 syl ⊢ ( ( ( 𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ ) ∧ ( 8 · ( 1 0 ↑ 3 0 ) ) < 𝑚 ) → ( ( 𝑛 ≤ ( 1 0 ↑ 2 7 ) ∧ ( 1 0 ↑ 2 7 ) < 𝑚 ) → 𝑛 < 𝑚 ) )
71 65 70 mpan2d ⊢ ( ( ( 𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ ) ∧ ( 8 · ( 1 0 ↑ 3 0 ) ) < 𝑚 ) → ( 𝑛 ≤ ( 1 0 ↑ 2 7 ) → 𝑛 < 𝑚 ) )
72 71 imp ⊢ ( ( ( ( 𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ ) ∧ ( 8 · ( 1 0 ↑ 3 0 ) ) < 𝑚 ) ∧ 𝑛 ≤ ( 1 0 ↑ 2 7 ) ) → 𝑛 < 𝑚 )
73 72 anim1i ⊢ ( ( ( ( ( 𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ ) ∧ ( 8 · ( 1 0 ↑ 3 0 ) ) < 𝑚 ) ∧ 𝑛 ≤ ( 1 0 ↑ 2 7 ) ) ∧ 7 < 𝑛 ) → ( 𝑛 < 𝑚 ∧ 7 < 𝑛 ) )
74 73 ancomd ⊢ ( ( ( ( ( 𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ ) ∧ ( 8 · ( 1 0 ↑ 3 0 ) ) < 𝑚 ) ∧ 𝑛 ≤ ( 1 0 ↑ 2 7 ) ) ∧ 7 < 𝑛 ) → ( 7 < 𝑛 ∧ 𝑛 < 𝑚 ) )
75 pm2.27 ⊢ ( ( 7 < 𝑛 ∧ 𝑛 < 𝑚 ) → ( ( ( 7 < 𝑛 ∧ 𝑛 < 𝑚 ) → 𝑛 ∈ GoldbachOdd ) → 𝑛 ∈ GoldbachOdd ) )
76 74 75 syl ⊢ ( ( ( ( ( 𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ ) ∧ ( 8 · ( 1 0 ↑ 3 0 ) ) < 𝑚 ) ∧ 𝑛 ≤ ( 1 0 ↑ 2 7 ) ) ∧ 7 < 𝑛 ) → ( ( ( 7 < 𝑛 ∧ 𝑛 < 𝑚 ) → 𝑛 ∈ GoldbachOdd ) → 𝑛 ∈ GoldbachOdd ) )
77 76 ex ⊢ ( ( ( ( 𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ ) ∧ ( 8 · ( 1 0 ↑ 3 0 ) ) < 𝑚 ) ∧ 𝑛 ≤ ( 1 0 ↑ 2 7 ) ) → ( 7 < 𝑛 → ( ( ( 7 < 𝑛 ∧ 𝑛 < 𝑚 ) → 𝑛 ∈ GoldbachOdd ) → 𝑛 ∈ GoldbachOdd ) ) )
78 77 com23 ⊢ ( ( ( ( 𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ ) ∧ ( 8 · ( 1 0 ↑ 3 0 ) ) < 𝑚 ) ∧ 𝑛 ≤ ( 1 0 ↑ 2 7 ) ) → ( ( ( 7 < 𝑛 ∧ 𝑛 < 𝑚 ) → 𝑛 ∈ GoldbachOdd ) → ( 7 < 𝑛 → 𝑛 ∈ GoldbachOdd ) ) )
79 78 exp41 ⊢ ( 𝑛 ∈ Odd → ( 𝑚 ∈ ℕ → ( ( 8 · ( 1 0 ↑ 3 0 ) ) < 𝑚 → ( 𝑛 ≤ ( 1 0 ↑ 2 7 ) → ( ( ( 7 < 𝑛 ∧ 𝑛 < 𝑚 ) → 𝑛 ∈ GoldbachOdd ) → ( 7 < 𝑛 → 𝑛 ∈ GoldbachOdd ) ) ) ) ) )
80 79 com25 ⊢ ( 𝑛 ∈ Odd → ( ( ( 7 < 𝑛 ∧ 𝑛 < 𝑚 ) → 𝑛 ∈ GoldbachOdd ) → ( ( 8 · ( 1 0 ↑ 3 0 ) ) < 𝑚 → ( 𝑛 ≤ ( 1 0 ↑ 2 7 ) → ( 𝑚 ∈ ℕ → ( 7 < 𝑛 → 𝑛 ∈ GoldbachOdd ) ) ) ) ) )
81 18 80 syld ⊢ ( 𝑛 ∈ Odd → ( ∀ 𝑜 ∈ Odd ( ( 7 < 𝑜 ∧ 𝑜 < 𝑚 ) → 𝑜 ∈ GoldbachOdd ) → ( ( 8 · ( 1 0 ↑ 3 0 ) ) < 𝑚 → ( 𝑛 ≤ ( 1 0 ↑ 2 7 ) → ( 𝑚 ∈ ℕ → ( 7 < 𝑛 → 𝑛 ∈ GoldbachOdd ) ) ) ) ) )
82 81 com15 ⊢ ( 𝑚 ∈ ℕ → ( ∀ 𝑜 ∈ Odd ( ( 7 < 𝑜 ∧ 𝑜 < 𝑚 ) → 𝑜 ∈ GoldbachOdd ) → ( ( 8 · ( 1 0 ↑ 3 0 ) ) < 𝑚 → ( 𝑛 ≤ ( 1 0 ↑ 2 7 ) → ( 𝑛 ∈ Odd → ( 7 < 𝑛 → 𝑛 ∈ GoldbachOdd ) ) ) ) ) )
83 82 com23 ⊢ ( 𝑚 ∈ ℕ → ( ( 8 · ( 1 0 ↑ 3 0 ) ) < 𝑚 → ( ∀ 𝑜 ∈ Odd ( ( 7 < 𝑜 ∧ 𝑜 < 𝑚 ) → 𝑜 ∈ GoldbachOdd ) → ( 𝑛 ≤ ( 1 0 ↑ 2 7 ) → ( 𝑛 ∈ Odd → ( 7 < 𝑛 → 𝑛 ∈ GoldbachOdd ) ) ) ) ) )
84 83 imp32 ⊢ ( ( 𝑚 ∈ ℕ ∧ ( ( 8 · ( 1 0 ↑ 3 0 ) ) < 𝑚 ∧ ∀ 𝑜 ∈ Odd ( ( 7 < 𝑜 ∧ 𝑜 < 𝑚 ) → 𝑜 ∈ GoldbachOdd ) ) ) → ( 𝑛 ≤ ( 1 0 ↑ 2 7 ) → ( 𝑛 ∈ Odd → ( 7 < 𝑛 → 𝑛 ∈ GoldbachOdd ) ) ) )
85 84 rexlimiva ⊢ ( ∃ 𝑚 ∈ ℕ ( ( 8 · ( 1 0 ↑ 3 0 ) ) < 𝑚 ∧ ∀ 𝑜 ∈ Odd ( ( 7 < 𝑜 ∧ 𝑜 < 𝑚 ) → 𝑜 ∈ GoldbachOdd ) ) → ( 𝑛 ≤ ( 1 0 ↑ 2 7 ) → ( 𝑛 ∈ Odd → ( 7 < 𝑛 → 𝑛 ∈ GoldbachOdd ) ) ) )
86 12 85 ax-mp ⊢ ( 𝑛 ≤ ( 1 0 ↑ 2 7 ) → ( 𝑛 ∈ Odd → ( 7 < 𝑛 → 𝑛 ∈ GoldbachOdd ) ) )
87 tgoldbachgtALTV ⊢ ∃ 𝑚 ∈ ℕ ( 𝑚 ≤ ( 1 0 ↑ 2 7 ) ∧ ∀ 𝑜 ∈ Odd ( 𝑚 < 𝑜 → 𝑜 ∈ GoldbachOdd ) )
88 breq2 ⊢ ( 𝑜 = 𝑛 → ( 𝑚 < 𝑜 ↔ 𝑚 < 𝑛 ) )
89 88 16 imbi12d ⊢ ( 𝑜 = 𝑛 → ( ( 𝑚 < 𝑜 → 𝑜 ∈ GoldbachOdd ) ↔ ( 𝑚 < 𝑛 → 𝑛 ∈ GoldbachOdd ) ) )
90 89 rspcv ⊢ ( 𝑛 ∈ Odd → ( ∀ 𝑜 ∈ Odd ( 𝑚 < 𝑜 → 𝑜 ∈ GoldbachOdd ) → ( 𝑚 < 𝑛 → 𝑛 ∈ GoldbachOdd ) ) )
91 lelttr ⊢ ( ( 𝑚 ∈ ℝ ∧ ( 1 0 ↑ 2 7 ) ∈ ℝ ∧ 𝑛 ∈ ℝ ) → ( ( 𝑚 ≤ ( 1 0 ↑ 2 7 ) ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) → 𝑚 < 𝑛 ) )
92 61 57 66 91 syl3anc ⊢ ( ( 𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ ) → ( ( 𝑚 ≤ ( 1 0 ↑ 2 7 ) ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) → 𝑚 < 𝑛 ) )
93 92 expcomd ⊢ ( ( 𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ ) → ( ( 1 0 ↑ 2 7 ) < 𝑛 → ( 𝑚 ≤ ( 1 0 ↑ 2 7 ) → 𝑚 < 𝑛 ) ) )
94 93 ex ⊢ ( 𝑛 ∈ Odd → ( 𝑚 ∈ ℕ → ( ( 1 0 ↑ 2 7 ) < 𝑛 → ( 𝑚 ≤ ( 1 0 ↑ 2 7 ) → 𝑚 < 𝑛 ) ) ) )
95 94 com23 ⊢ ( 𝑛 ∈ Odd → ( ( 1 0 ↑ 2 7 ) < 𝑛 → ( 𝑚 ∈ ℕ → ( 𝑚 ≤ ( 1 0 ↑ 2 7 ) → 𝑚 < 𝑛 ) ) ) )
96 95 imp43 ⊢ ( ( ( 𝑛 ∈ Odd ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑚 ≤ ( 1 0 ↑ 2 7 ) ) ) → 𝑚 < 𝑛 )
97 pm2.27 ⊢ ( 𝑚 < 𝑛 → ( ( 𝑚 < 𝑛 → 𝑛 ∈ GoldbachOdd ) → 𝑛 ∈ GoldbachOdd ) )
98 96 97 syl ⊢ ( ( ( 𝑛 ∈ Odd ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑚 ≤ ( 1 0 ↑ 2 7 ) ) ) → ( ( 𝑚 < 𝑛 → 𝑛 ∈ GoldbachOdd ) → 𝑛 ∈ GoldbachOdd ) )
99 98 a1dd ⊢ ( ( ( 𝑛 ∈ Odd ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑚 ≤ ( 1 0 ↑ 2 7 ) ) ) → ( ( 𝑚 < 𝑛 → 𝑛 ∈ GoldbachOdd ) → ( 7 < 𝑛 → 𝑛 ∈ GoldbachOdd ) ) )
100 99 ex ⊢ ( ( 𝑛 ∈ Odd ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) → ( ( 𝑚 ∈ ℕ ∧ 𝑚 ≤ ( 1 0 ↑ 2 7 ) ) → ( ( 𝑚 < 𝑛 → 𝑛 ∈ GoldbachOdd ) → ( 7 < 𝑛 → 𝑛 ∈ GoldbachOdd ) ) ) )
101 100 com23 ⊢ ( ( 𝑛 ∈ Odd ∧ ( 1 0 ↑ 2 7 ) < 𝑛 ) → ( ( 𝑚 < 𝑛 → 𝑛 ∈ GoldbachOdd ) → ( ( 𝑚 ∈ ℕ ∧ 𝑚 ≤ ( 1 0 ↑ 2 7 ) ) → ( 7 < 𝑛 → 𝑛 ∈ GoldbachOdd ) ) ) )
102 101 ex ⊢ ( 𝑛 ∈ Odd → ( ( 1 0 ↑ 2 7 ) < 𝑛 → ( ( 𝑚 < 𝑛 → 𝑛 ∈ GoldbachOdd ) → ( ( 𝑚 ∈ ℕ ∧ 𝑚 ≤ ( 1 0 ↑ 2 7 ) ) → ( 7 < 𝑛 → 𝑛 ∈ GoldbachOdd ) ) ) ) )
103 102 com23 ⊢ ( 𝑛 ∈ Odd → ( ( 𝑚 < 𝑛 → 𝑛 ∈ GoldbachOdd ) → ( ( 1 0 ↑ 2 7 ) < 𝑛 → ( ( 𝑚 ∈ ℕ ∧ 𝑚 ≤ ( 1 0 ↑ 2 7 ) ) → ( 7 < 𝑛 → 𝑛 ∈ GoldbachOdd ) ) ) ) )
104 90 103 syld ⊢ ( 𝑛 ∈ Odd → ( ∀ 𝑜 ∈ Odd ( 𝑚 < 𝑜 → 𝑜 ∈ GoldbachOdd ) → ( ( 1 0 ↑ 2 7 ) < 𝑛 → ( ( 𝑚 ∈ ℕ ∧ 𝑚 ≤ ( 1 0 ↑ 2 7 ) ) → ( 7 < 𝑛 → 𝑛 ∈ GoldbachOdd ) ) ) ) )
105 104 com14 ⊢ ( ( 𝑚 ∈ ℕ ∧ 𝑚 ≤ ( 1 0 ↑ 2 7 ) ) → ( ∀ 𝑜 ∈ Odd ( 𝑚 < 𝑜 → 𝑜 ∈ GoldbachOdd ) → ( ( 1 0 ↑ 2 7 ) < 𝑛 → ( 𝑛 ∈ Odd → ( 7 < 𝑛 → 𝑛 ∈ GoldbachOdd ) ) ) ) )
106 105 impr ⊢ ( ( 𝑚 ∈ ℕ ∧ ( 𝑚 ≤ ( 1 0 ↑ 2 7 ) ∧ ∀ 𝑜 ∈ Odd ( 𝑚 < 𝑜 → 𝑜 ∈ GoldbachOdd ) ) ) → ( ( 1 0 ↑ 2 7 ) < 𝑛 → ( 𝑛 ∈ Odd → ( 7 < 𝑛 → 𝑛 ∈ GoldbachOdd ) ) ) )
107 106 rexlimiva ⊢ ( ∃ 𝑚 ∈ ℕ ( 𝑚 ≤ ( 1 0 ↑ 2 7 ) ∧ ∀ 𝑜 ∈ Odd ( 𝑚 < 𝑜 → 𝑜 ∈ GoldbachOdd ) ) → ( ( 1 0 ↑ 2 7 ) < 𝑛 → ( 𝑛 ∈ Odd → ( 7 < 𝑛 → 𝑛 ∈ GoldbachOdd ) ) ) )
108 87 107 ax-mp ⊢ ( ( 1 0 ↑ 2 7 ) < 𝑛 → ( 𝑛 ∈ Odd → ( 7 < 𝑛 → 𝑛 ∈ GoldbachOdd ) ) )
109 86 108 jaoi ⊢ ( ( 𝑛 ≤ ( 1 0 ↑ 2 7 ) ∨ ( 1 0 ↑ 2 7 ) < 𝑛 ) → ( 𝑛 ∈ Odd → ( 7 < 𝑛 → 𝑛 ∈ GoldbachOdd ) ) )
110 11 109 mpcom ⊢ ( 𝑛 ∈ Odd → ( 7 < 𝑛 → 𝑛 ∈ GoldbachOdd ) )
111 110 rgen ⊢ ∀ 𝑛 ∈ Odd ( 7 < 𝑛 → 𝑛 ∈ GoldbachOdd )