nnne0

Description: A positive integer is nonzero. See nnne0ALT for a shorter proof using ax-pre-mulgt0 . This proof avoids 0lt1 , and thus ax-pre-mulgt0 , by splitting ax-1ne0 into the two separate cases 0 < 1 and 1 < 0 . (Contributed by NM, 27-Sep-1999) Remove dependency on ax-pre-mulgt0 . (Revised by Steven Nguyen, 30-Jan-2023)

		Ref	Expression
	Assertion	nnne0	$⊢ A \in ℕ \to A \neq 0$

Proof

Step	Hyp	Ref	Expression
1		ax-1ne0	$⊢ 1 \neq 0$
2		1re	$⊢ 1 \in ℝ$
3		0re	$⊢ 0 \in ℝ$
4	2 3	lttri2i	$⊢ 1 \neq 0 \leftrightarrow (1 < 0 \lor 0 < 1)$
5	1 4	mpbi	$⊢ (1 < 0 \lor 0 < 1)$
6		breq1	$⊢ x = 1 \to (x < 0 \leftrightarrow 1 < 0)$
7	6	imbi2d	$⊢ x = 1 \to ((1 < 0 \to x < 0) \leftrightarrow (1 < 0 \to 1 < 0))$
8		breq1	$⊢ x = y \to (x < 0 \leftrightarrow y < 0)$
9	8	imbi2d	$⊢ x = y \to ((1 < 0 \to x < 0) \leftrightarrow (1 < 0 \to y < 0))$
10		breq1	$⊢ x = y + 1 \to (x < 0 \leftrightarrow y + 1 < 0)$
11	10	imbi2d	$⊢ x = y + 1 \to ((1 < 0 \to x < 0) \leftrightarrow (1 < 0 \to y + 1 < 0))$
12		breq1	$⊢ x = A \to (x < 0 \leftrightarrow A < 0)$
13	12	imbi2d	$⊢ x = A \to ((1 < 0 \to x < 0) \leftrightarrow (1 < 0 \to A < 0))$
14		id	$⊢ 1 < 0 \to 1 < 0$
15		simp1	$⊢ (y \in ℕ \land 1 < 0 \land y < 0) \to y \in ℕ$
16	15	nnred	$⊢ (y \in ℕ \land 1 < 0 \land y < 0) \to y \in ℝ$
17		1red	$⊢ (y \in ℕ \land 1 < 0 \land y < 0) \to 1 \in ℝ$
18	16 17	readdcld	$⊢ (y \in ℕ \land 1 < 0 \land y < 0) \to y + 1 \in ℝ$
19	3 2	readdcli	$⊢ 0 + 1 \in ℝ$
20	19	a1i	$⊢ (y \in ℕ \land 1 < 0 \land y < 0) \to 0 + 1 \in ℝ$
21		0red	$⊢ (y \in ℕ \land 1 < 0 \land y < 0) \to 0 \in ℝ$
22		simp3	$⊢ (y \in ℕ \land 1 < 0 \land y < 0) \to y < 0$
23	16 21 17 22	ltadd1dd	$⊢ (y \in ℕ \land 1 < 0 \land y < 0) \to y + 1 < 0 + 1$
24		ax-1cn	$⊢ 1 \in ℂ$
25	24	addid2i	$⊢ 0 + 1 = 1$
26		simp2	$⊢ (y \in ℕ \land 1 < 0 \land y < 0) \to 1 < 0$
27	25 26	eqbrtrid	$⊢ (y \in ℕ \land 1 < 0 \land y < 0) \to 0 + 1 < 0$
28	18 20 21 23 27	lttrd	$⊢ (y \in ℕ \land 1 < 0 \land y < 0) \to y + 1 < 0$
29	28	3exp	$⊢ y \in ℕ \to (1 < 0 \to (y < 0 \to y + 1 < 0))$
30	29	a2d	$⊢ y \in ℕ \to ((1 < 0 \to y < 0) \to (1 < 0 \to y + 1 < 0))$
31	7 9 11 13 14 30	nnind	$⊢ A \in ℕ \to (1 < 0 \to A < 0)$
32	31	imp	$⊢ (A \in ℕ \land 1 < 0) \to A < 0$
33	32	lt0ne0d	$⊢ (A \in ℕ \land 1 < 0) \to A \neq 0$
34	33	ex	$⊢ A \in ℕ \to (1 < 0 \to A \neq 0)$
35		breq2	$⊢ x = 1 \to (0 < x \leftrightarrow 0 < 1)$
36	35	imbi2d	$⊢ x = 1 \to ((0 < 1 \to 0 < x) \leftrightarrow (0 < 1 \to 0 < 1))$
37		breq2	$⊢ x = y \to (0 < x \leftrightarrow 0 < y)$
38	37	imbi2d	$⊢ x = y \to ((0 < 1 \to 0 < x) \leftrightarrow (0 < 1 \to 0 < y))$
39		breq2	$⊢ x = y + 1 \to (0 < x \leftrightarrow 0 < y + 1)$
40	39	imbi2d	$⊢ x = y + 1 \to ((0 < 1 \to 0 < x) \leftrightarrow (0 < 1 \to 0 < y + 1))$
41		breq2	$⊢ x = A \to (0 < x \leftrightarrow 0 < A)$
42	41	imbi2d	$⊢ x = A \to ((0 < 1 \to 0 < x) \leftrightarrow (0 < 1 \to 0 < A))$
43		id	$⊢ 0 < 1 \to 0 < 1$
44		simp1	$⊢ (y \in ℕ \land 0 < 1 \land 0 < y) \to y \in ℕ$
45	44	nnred	$⊢ (y \in ℕ \land 0 < 1 \land 0 < y) \to y \in ℝ$
46		1red	$⊢ (y \in ℕ \land 0 < 1 \land 0 < y) \to 1 \in ℝ$
47		simp3	$⊢ (y \in ℕ \land 0 < 1 \land 0 < y) \to 0 < y$
48		simp2	$⊢ (y \in ℕ \land 0 < 1 \land 0 < y) \to 0 < 1$
49	45 46 47 48	addgt0d	$⊢ (y \in ℕ \land 0 < 1 \land 0 < y) \to 0 < y + 1$
50	49	3exp	$⊢ y \in ℕ \to (0 < 1 \to (0 < y \to 0 < y + 1))$
51	50	a2d	$⊢ y \in ℕ \to ((0 < 1 \to 0 < y) \to (0 < 1 \to 0 < y + 1))$
52	36 38 40 42 43 51	nnind	$⊢ A \in ℕ \to (0 < 1 \to 0 < A)$
53	52	imp	$⊢ (A \in ℕ \land 0 < 1) \to 0 < A$
54	53	gt0ne0d	$⊢ (A \in ℕ \land 0 < 1) \to A \neq 0$
55	54	ex	$⊢ A \in ℕ \to (0 < 1 \to A \neq 0)$
56	34 55	jaod	$⊢ A \in ℕ \to ((1 < 0 \lor 0 < 1) \to A \neq 0)$
57	5 56	mpi	$⊢ A \in ℕ \to A \neq 0$

Metamath Proof Explorer

Theorem nnne0

Proof