Theorem nn0sub

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

	Ref	Expression
Assertion	nn0sub	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 ≤ 𝑁 ↔ ( 𝑁 − 𝑀 ) ∈ ℕ0 ) )

Proof

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