nn0sub

Description: Subtraction of nonnegative integers. (Contributed by NM, 9-May-2004) (Proof shortened by Mario Carneiro, 16-May-2014)

		Ref	Expression
	Assertion	nn0sub	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (M \leq N \leftrightarrow N - M \in ℕ_{0})$

Proof

Step	Hyp	Ref	Expression
1		nn0re	$⊢ M \in ℕ_{0} \to M \in ℝ$
2		nn0re	$⊢ N \in ℕ_{0} \to N \in ℝ$
3		leloe	$⊢ (M \in ℝ \land N \in ℝ) \to (M \leq N \leftrightarrow (M < N \lor M = N))$
4	1 2 3	syl2an	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (M \leq N \leftrightarrow (M < N \lor M = N))$
5		elnn0	$⊢ N \in ℕ_{0} \leftrightarrow (N \in ℕ \lor N = 0)$
6		elnn0	$⊢ M \in ℕ_{0} \leftrightarrow (M \in ℕ \lor M = 0)$
7		nnsub	$⊢ (M \in ℕ \land N \in ℕ) \to (M < N \leftrightarrow N - M \in ℕ)$
8	7	ex	$⊢ M \in ℕ \to (N \in ℕ \to (M < N \leftrightarrow N - M \in ℕ))$
9		nngt0	$⊢ N \in ℕ \to 0 < N$
10		nncn	$⊢ N \in ℕ \to N \in ℂ$
11	10	subid1d	$⊢ N \in ℕ \to N - 0 = N$
12		id	$⊢ N \in ℕ \to N \in ℕ$
13	11 12	eqeltrd	$⊢ N \in ℕ \to N - 0 \in ℕ$
14	9 13	2thd	$⊢ N \in ℕ \to (0 < N \leftrightarrow N - 0 \in ℕ)$
15		breq1	$⊢ M = 0 \to (M < N \leftrightarrow 0 < N)$
16		oveq2	$⊢ M = 0 \to N - M = N - 0$
17	16	eleq1d	$⊢ M = 0 \to (N - M \in ℕ \leftrightarrow N - 0 \in ℕ)$
18	15 17	bibi12d	$⊢ M = 0 \to ((M < N \leftrightarrow N - M \in ℕ) \leftrightarrow (0 < N \leftrightarrow N - 0 \in ℕ))$
19	14 18	syl5ibr	$⊢ M = 0 \to (N \in ℕ \to (M < N \leftrightarrow N - M \in ℕ))$
20	8 19	jaoi	$⊢ (M \in ℕ \lor M = 0) \to (N \in ℕ \to (M < N \leftrightarrow N - M \in ℕ))$
21	6 20	sylbi	$⊢ M \in ℕ_{0} \to (N \in ℕ \to (M < N \leftrightarrow N - M \in ℕ))$
22		nn0nlt0	$⊢ M \in ℕ_{0} \to \neg M < 0$
23	22	pm2.21d	$⊢ M \in ℕ_{0} \to (M < 0 \to 0 - M \in ℕ)$
24		nngt0	$⊢ 0 - M \in ℕ \to 0 < 0 - M$
25		0re	$⊢ 0 \in ℝ$
26		posdif	$⊢ (M \in ℝ \land 0 \in ℝ) \to (M < 0 \leftrightarrow 0 < 0 - M)$
27	1 25 26	sylancl	$⊢ M \in ℕ_{0} \to (M < 0 \leftrightarrow 0 < 0 - M)$
28	24 27	syl5ibr	$⊢ M \in ℕ_{0} \to (0 - M \in ℕ \to M < 0)$
29	23 28	impbid	$⊢ M \in ℕ_{0} \to (M < 0 \leftrightarrow 0 - M \in ℕ)$
30		breq2	$⊢ N = 0 \to (M < N \leftrightarrow M < 0)$
31		oveq1	$⊢ N = 0 \to N - M = 0 - M$
32	31	eleq1d	$⊢ N = 0 \to (N - M \in ℕ \leftrightarrow 0 - M \in ℕ)$
33	30 32	bibi12d	$⊢ N = 0 \to ((M < N \leftrightarrow N - M \in ℕ) \leftrightarrow (M < 0 \leftrightarrow 0 - M \in ℕ))$
34	29 33	syl5ibrcom	$⊢ M \in ℕ_{0} \to (N = 0 \to (M < N \leftrightarrow N - M \in ℕ))$
35	21 34	jaod	$⊢ M \in ℕ_{0} \to ((N \in ℕ \lor N = 0) \to (M < N \leftrightarrow N - M \in ℕ))$
36	5 35	syl5bi	$⊢ M \in ℕ_{0} \to (N \in ℕ_{0} \to (M < N \leftrightarrow N - M \in ℕ))$
37	36	imp	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (M < N \leftrightarrow N - M \in ℕ)$
38		nn0cn	$⊢ N \in ℕ_{0} \to N \in ℂ$
39		nn0cn	$⊢ M \in ℕ_{0} \to M \in ℂ$
40		subeq0	$⊢ (N \in ℂ \land M \in ℂ) \to (N - M = 0 \leftrightarrow N = M)$
41	38 39 40	syl2anr	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (N - M = 0 \leftrightarrow N = M)$
42		eqcom	$⊢ N = M \leftrightarrow M = N$
43	41 42	bitr2di	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (M = N \leftrightarrow N - M = 0)$
44	37 43	orbi12d	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to ((M < N \lor M = N) \leftrightarrow (N - M \in ℕ \lor N - M = 0))$
45	4 44	bitrd	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (M \leq N \leftrightarrow (N - M \in ℕ \lor N - M = 0))$
46		elnn0	$⊢ N - M \in ℕ_{0} \leftrightarrow (N - M \in ℕ \lor N - M = 0)$
47	45 46	bitr4di	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (M \leq N \leftrightarrow N - M \in ℕ_{0})$

Metamath Proof Explorer

Theorem nn0sub

Proof