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	addlidi	$⊢ 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		breq2	$⊢ x = 1 \to (0 < x \leftrightarrow 0 < 1)$
35	34	imbi2d	$⊢ x = 1 \to ((0 < 1 \to 0 < x) \leftrightarrow (0 < 1 \to 0 < 1))$
36		breq2	$⊢ x = y \to (0 < x \leftrightarrow 0 < y)$
37	36	imbi2d	$⊢ x = y \to ((0 < 1 \to 0 < x) \leftrightarrow (0 < 1 \to 0 < y))$
38		breq2	$⊢ x = y + 1 \to (0 < x \leftrightarrow 0 < y + 1)$
39	38	imbi2d	$⊢ x = y + 1 \to ((0 < 1 \to 0 < x) \leftrightarrow (0 < 1 \to 0 < y + 1))$
40		breq2	$⊢ x = A \to (0 < x \leftrightarrow 0 < A)$
41	40	imbi2d	$⊢ x = A \to ((0 < 1 \to 0 < x) \leftrightarrow (0 < 1 \to 0 < A))$
42		id	$⊢ 0 < 1 \to 0 < 1$
43		simp1	$⊢ (y \in ℕ \land 0 < 1 \land 0 < y) \to y \in ℕ$
44	43	nnred	$⊢ (y \in ℕ \land 0 < 1 \land 0 < y) \to y \in ℝ$
45		1red	$⊢ (y \in ℕ \land 0 < 1 \land 0 < y) \to 1 \in ℝ$
46		simp3	$⊢ (y \in ℕ \land 0 < 1 \land 0 < y) \to 0 < y$
47		simp2	$⊢ (y \in ℕ \land 0 < 1 \land 0 < y) \to 0 < 1$
48	44 45 46 47	addgt0d	$⊢ (y \in ℕ \land 0 < 1 \land 0 < y) \to 0 < y + 1$
49	48	3exp	$⊢ y \in ℕ \to (0 < 1 \to (0 < y \to 0 < y + 1))$
50	49	a2d	$⊢ y \in ℕ \to ((0 < 1 \to 0 < y) \to (0 < 1 \to 0 < y + 1))$
51	35 37 39 41 42 50	nnind	$⊢ A \in ℕ \to (0 < 1 \to 0 < A)$
52	51	imp	$⊢ (A \in ℕ \land 0 < 1) \to 0 < A$
53	52	gt0ne0d	$⊢ (A \in ℕ \land 0 < 1) \to A \neq 0$
54	33 53	jaodan	$⊢ (A \in ℕ \land (1 < 0 \lor 0 < 1)) \to A \neq 0$
55	5 54	mpan2	$⊢ A \in ℕ \to A \neq 0$

Metamath Proof Explorer

Theorem nnne0

Proof