Theorem tgoldbachgnn

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

	Ref	Expression
Hypotheses	tgoldbachgtda.o	$$⊢O=\left\{z\in \mathbb{Z}|\neg 2\parallel z\right\}$$
	tgoldbachgtda.n	$$⊢\phi \to N\in O$$
	tgoldbachgtda.0	$$⊢\phi \to {10}^{27}\le N$$
Assertion	tgoldbachgnn	$$⊢\phi \to N\in \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		tgoldbachgtda.o	$$⊢O=\left\{z\in \mathbb{Z}|\neg 2\parallel z\right\}$$
2		tgoldbachgtda.n	$$⊢\phi \to N\in O$$
3		tgoldbachgtda.0	$$⊢\phi \to {10}^{27}\le N$$
4	2 1	eleqtrdi	$$⊢\phi \to N\in \left\{z\in \mathbb{Z}|\neg 2\parallel z\right\}$$
5		elrabi	$$⊢N\in \left\{z\in \mathbb{Z}|\neg 2\parallel z\right\}\to N\in \mathbb{Z}$$
6	4 5	syl	$$⊢\phi \to N\in \mathbb{Z}$$
7		1red	$$⊢\phi \to 1\in ℝ$$
8		10nn0	$$⊢10\in {\mathbb{N}}_0$$
9	8	nn0rei	$$⊢10\in ℝ$$
10		2nn0	$$⊢2\in {\mathbb{N}}_0$$
11		7nn0	$$⊢7\in {\mathbb{N}}_0$$
12	10 11	deccl	$$⊢27\in {\mathbb{N}}_0$$
13		reexpcl	$$⊢\left(10\in ℝ\wedge 27\in {\mathbb{N}}_0\right)\to {10}^{27}\in ℝ$$
14	9 12 13	mp2an	$$⊢{10}^{27}\in ℝ$$
15	14	a1i	$$⊢\phi \to {10}^{27}\in ℝ$$
16	6	zred	$$⊢\phi \to N\in ℝ$$
17		1re	$$⊢1\in ℝ$$
18		1lt10	$$⊢1<10$$
19	17 9 18	ltleii	$$⊢1\le 10$$
20		expge1	$$⊢\left(10\in ℝ\wedge 27\in {\mathbb{N}}_0\wedge 1\le 10\right)\to 1\le {10}^{27}$$
21	9 12 19 20	mp3an	$$⊢1\le {10}^{27}$$
22	21	a1i	$$⊢\phi \to 1\le {10}^{27}$$
23	7 15 16 22 3	letrd	$$⊢\phi \to 1\le N$$
24		elnnz1	$$⊢N\in \mathbb{N}\leftrightarrow \left(N\in \mathbb{Z}\wedge 1\le N\right)$$
25	6 23 24	sylanbrc	$$⊢\phi \to N\in \mathbb{N}$$