This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem tgoldbachgnn

Description: Lemma for tgoldbachgtd . (Contributed by Thierry Arnoux, 15-Dec-2021)

Ref Expression
Hypotheses tgoldbachgtda.o ⊢ O = z ∈ ℤ | ¬ 2 ∥ z
tgoldbachgtda.n ⊢ φ → N ∈ O
tgoldbachgtda.0 ⊢ φ → 10 27 ≤ N
Assertion tgoldbachgnn ⊢ φ → N ∈ ℕ

Proof

Step Hyp Ref Expression
1 tgoldbachgtda.o ⊢ O = z ∈ ℤ | ¬ 2 ∥ z
2 tgoldbachgtda.n ⊢ φ → N ∈ O
3 tgoldbachgtda.0 ⊢ φ → 10 27 ≤ N
4 2 1 eleqtrdi ⊢ φ → N ∈ z ∈ ℤ | ¬ 2 ∥ z
5 elrabi ⊢ N ∈ z ∈ ℤ | ¬ 2 ∥ z → N ∈ ℤ
6 4 5 syl ⊢ φ → N ∈ ℤ
7 1red ⊢ φ → 1 ∈ ℝ
8 10nn0 ⊢ 10 ∈ ℕ 0
9 8 nn0rei ⊢ 10 ∈ ℝ
10 2nn0 ⊢ 2 ∈ ℕ 0
11 7nn0 ⊢ 7 ∈ ℕ 0
12 10 11 deccl ⊢ 27 ∈ ℕ 0
13 reexpcl ⊢ 10 ∈ ℝ ∧ 27 ∈ ℕ 0 → 10 27 ∈ ℝ
14 9 12 13 mp2an ⊢ 10 27 ∈ ℝ
15 14 a1i ⊢ φ → 10 27 ∈ ℝ
16 6 zred ⊢ φ → N ∈ ℝ
17 1re ⊢ 1 ∈ ℝ
18 1lt10 ⊢ 1 < 10
19 17 9 18 ltleii ⊢ 1 ≤ 10
20 expge1 ⊢ 10 ∈ ℝ ∧ 27 ∈ ℕ 0 ∧ 1 ≤ 10 → 1 ≤ 10 27
21 9 12 19 20 mp3an ⊢ 1 ≤ 10 27
22 21 a1i ⊢ φ → 1 ≤ 10 27
23 7 15 16 22 3 letrd ⊢ φ → 1 ≤ N
24 elnnz1 ⊢ N ∈ ℕ ↔ N ∈ ℤ ∧ 1 ≤ N
25 6 23 24 sylanbrc ⊢ φ → N ∈ ℕ