Metamath Proof Explorer

Theorem tgoldbachgnn

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

Ref Expression
Hypotheses tgoldbachgtda.o ⊢ 𝑂 = { 𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧 }
tgoldbachgtda.n ⊢ ( 𝜑 → 𝑁 ∈ 𝑂 )
tgoldbachgtda.0 ⊢ ( 𝜑 → ( 1 0 ↑ 2 7 ) ≤ 𝑁 )
Assertion tgoldbachgnn ( 𝜑 → 𝑁 ∈ ℕ )

Proof

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