Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem nn0subt 4587

Description: Subtraction of nonnegative integers.

**Assertion**
Ref	Expression
nn0subt	⊢ ((A ∈ ℕ₀ ∧ B ∈ ℕ₀) → (A ≤ B ↔ (B − A) ∈ ℕ₀))

**Proof of Theorem nn0subt**
Step	Hyp	Ref	Expression
1		nnsubt 4451	. . . . . . . 8 ⊢ ((A ∈ ℕ ∧ B ∈ ℕ) → (A < B ↔ (B − A) ∈ ℕ))
2	1	exp 291	. . . . . . 7 ⊢ (A ∈ ℕ → (B ∈ ℕ → (A < B ↔ (B − A) ∈ ℕ)))
3		breq2 2066	. . . . . . . . . 10 ⊢ (B = 0 → (A < B ↔ A < 0))
4		opreq1 3006	. . . . . . . . . . 11 ⊢ (B = 0 → (B − A) = (0 − A))
5	4	eleq1d 1155	. . . . . . . . . 10 ⊢ (B = 0 → ((B − A) ∈ ℕ ↔ (0 − A) ∈ ℕ))
6	3, 5	bibi12d 477	. . . . . . . . 9 ⊢ (B = 0 → ((A < B ↔ (B − A) ∈ ℕ) ↔ (A < 0 ↔ (0 − A) ∈ ℕ)))
7		nnret 4427	. . . . . . . . . . 11 ⊢ (A ∈ ℕ → A ∈ ℝ)
8		lt0neg1t 4370	. . . . . . . . . . 11 ⊢ (A ∈ ℝ → (A < 0 ↔ 0 < -A))
9	7, 8	syl 12	. . . . . . . . . 10 ⊢ (A ∈ ℕ → (A < 0 ↔ 0 < -A))
10		nnnegz 4566	. . . . . . . . . . . 12 ⊢ (A ∈ ℕ → -A ∈ ℤ)
11		elnnz 4572	. . . . . . . . . . . . 13 ⊢ (-A ∈ ℕ ↔ (-A ∈ ℤ ∧ 0 < -A))
12	11	baib 506	. . . . . . . . . . . 12 ⊢ (-A ∈ ℤ → (-A ∈ ℕ ↔ 0 < -A))
13	10, 12	syl 12	. . . . . . . . . . 11 ⊢ (A ∈ ℕ → (-A ∈ ℕ ↔ 0 < -A))
14		df-neg 4135	. . . . . . . . . . . 12 ⊢ -A = (0 − A)
15	14	eleq1i 1152	. . . . . . . . . . 11 ⊢ (-A ∈ ℕ ↔ (0 − A) ∈ ℕ)
16	13, 15	syl5rbbr 413	. . . . . . . . . 10 ⊢ (A ∈ ℕ → (0 < -A ↔ (0 − A) ∈ ℕ))
17	9, 16	bitrd 406	. . . . . . . . 9 ⊢ (A ∈ ℕ → (A < 0 ↔ (0 − A) ∈ ℕ))
18	6, 17	syl5bir 184	. . . . . . . 8 ⊢ (B = 0 → (A ∈ ℕ → (A < B ↔ (B − A) ∈ ℕ)))
19	18	com12 13	. . . . . . 7 ⊢ (A ∈ ℕ → (B = 0 → (A < B ↔ (B − A) ∈ ℕ)))
20	2, 19	jaod 329	. . . . . 6 ⊢ (A ∈ ℕ → ((B ∈ ℕ ∨ B = 0) → (A < B ↔ (B − A) ∈ ℕ)))
21		breq1 2065	. . . . . . . . 9 ⊢ (A = 0 → (A < B ↔ 0 < B))
22		opreq2 3007	. . . . . . . . . 10 ⊢ (A = 0 → (B − A) = (B − 0))
23	22	eleq1d 1155	. . . . . . . . 9 ⊢ (A = 0 → ((B − A) ∈ ℕ ↔ (B − 0) ∈ ℕ))
24	21, 23	bibi12d 477	. . . . . . . 8 ⊢ (A = 0 → ((A < B ↔ (B − A) ∈ ℕ) ↔ (0 < B ↔ (B − 0) ∈ ℕ)))
25		nnzt 4579	. . . . . . . . 9 ⊢ (B ∈ ℕ → B ∈ ℤ)
26		zcnt 4568	. . . . . . . . . . 11 ⊢ (B ∈ ℤ → B ∈ ℂ)
27		subid1t 4160	. . . . . . . . . . . 12 ⊢ (B ∈ ℂ → (B − 0) = B)
28	27	eleq1d 1155	. . . . . . . . . . 11 ⊢ (B ∈ ℂ → ((B − 0) ∈ ℕ ↔ B ∈ ℕ))
29	26, 28	syl 12	. . . . . . . . . 10 ⊢ (B ∈ ℤ → ((B − 0) ∈ ℕ ↔ B ∈ ℕ))
30		elnnz 4572	. . . . . . . . . . 11 ⊢ (B ∈ ℕ ↔ (B ∈ ℤ ∧ 0 < B))
31	30	baib 506	. . . . . . . . . 10 ⊢ (B ∈ ℤ → (B ∈ ℕ ↔ 0 < B))
32	29, 31	bitr2d 407	. . . . . . . . 9 ⊢ (B ∈ ℤ → (0 < B ↔ (B − 0) ∈ ℕ))
33	25, 32	syl 12	. . . . . . . 8 ⊢ (B ∈ ℕ → (0 < B ↔ (B − 0) ∈ ℕ))
34	24, 33	syl5bir 184	. . . . . . 7 ⊢ (A = 0 → (B ∈ ℕ → (A < B ↔ (B − A) ∈ ℕ)))
35		ax0re 4063	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ
36	35	ltnr 4338	. . . . . . . . . 10 ⊢ ¬ 0 < 0
37		0nnn 4443	. . . . . . . . . . 11 ⊢ ¬ 0 ∈ ℕ
38		0cn 4100	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℂ
39	38	subid 4155	. . . . . . . . . . . 12 ⊢ (0 − 0) = 0
40	39	eleq1i 1152	. . . . . . . . . . 11 ⊢ ((0 − 0) ∈ ℕ ↔ 0 ∈ ℕ)
41	37, 40	mtbir 167	. . . . . . . . . 10 ⊢ ¬ (0 − 0) ∈ ℕ
42		pm5.21 502	. . . . . . . . . 10 ⊢ ((¬ 0 < 0 ∧ ¬ (0 − 0) ∈ ℕ) → (0 < 0 ↔ (0 − 0) ∈ ℕ))
43	36, 41, 42	mp2an 520	. . . . . . . . 9 ⊢ (0 < 0 ↔ (0 − 0) ∈ ℕ)
44		breq2 2066	. . . . . . . . . 10 ⊢ (B = 0 → (0 < B ↔ 0 < 0))
45		opreq1 3006	. . . . . . . . . . 11 ⊢ (B = 0 → (B − 0) = (0 − 0))
46	45	eleq1d 1155	. . . . . . . . . 10 ⊢ (B = 0 → ((B − 0) ∈ ℕ ↔ (0 − 0) ∈ ℕ))
47	44, 46	bibi12d 477	. . . . . . . . 9 ⊢ (B = 0 → ((0 < B ↔ (B − 0) ∈ ℕ) ↔ (0 < 0 ↔ (0 − 0) ∈ ℕ)))
48	43, 47	mpbiri 169	. . . . . . . 8 ⊢ (B = 0 → (0 < B ↔ (B − 0) ∈ ℕ))
49	24, 48	syl5bir 184	. . . . . . 7 ⊢ (A = 0 → (B = 0 → (A < B ↔ (B − A) ∈ ℕ)))
50	34, 49	jaod 329	. . . . . 6 ⊢ (A = 0 → ((B ∈ ℕ ∨ B = 0) → (A < B ↔ (B − A) ∈ ℕ)))
51	20, 50	jaoi 275	. . . . 5 ⊢ ((A ∈ ℕ ∨ A = 0) → ((B ∈ ℕ ∨ B = 0) → (A < B ↔ (B − A) ∈ ℕ)))
52	51	imp 277	. . . 4 ⊢ (((A ∈ ℕ ∨ A = 0) ∧ (B ∈ ℕ ∨ B = 0)) → (A < B ↔ (B − A) ∈ ℕ))
53		subeq0t 4169	. . . . . . 7 ⊢ ((B ∈ ℂ ∧ A ∈ ℂ) → ((B − A) = 0 ↔ B = A))
54		cleqcom 1103	. . . . . . 7 ⊢ (A = B ↔ B = A)
55	53, 54	syl6rbbr 417	. . . . . 6 ⊢ ((B ∈ ℂ ∧ A ∈ ℂ) → (A = B ↔ (B − A) = 0))
56	55	ancoms 334	. . . . 5 ⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → (A = B ↔ (B − A) = 0))
57		nncnt 4428	. . . . . 6 ⊢ (A ∈ ℕ → A ∈ ℂ)
58		eleq1 1149	. . . . . . 7 ⊢ (A = 0 → (A ∈ ℂ ↔ 0 ∈ ℂ))
59	38, 58	mpbiri 169	. . . . . 6 ⊢ (A = 0 → A ∈ ℂ)
60	57, 59	jaoi 275	. . . . 5 ⊢ ((A ∈ ℕ ∨ A = 0) → A ∈ ℂ)
61		nncnt 4428	. . . . . 6 ⊢ (B ∈ ℕ → B ∈ ℂ)
62		eleq1 1149	. . . . . . 7 ⊢ (B = 0 → (B ∈ ℂ ↔ 0 ∈ ℂ))
63	38, 62	mpbiri 169	. . . . . 6 ⊢ (B = 0 → B ∈ ℂ)
64	61, 63	jaoi 275	. . . . 5 ⊢ ((B ∈ ℕ ∨ B = 0) → B ∈ ℂ)
65	56, 60, 64	syl2an 349	. . . 4 ⊢ (((A ∈ ℕ ∨ A = 0) ∧ (B ∈ ℕ ∨ B = 0)) → (A = B ↔ (B − A) = 0))
66	52, 65	orbi12d 475	. . 3 ⊢ (((A ∈ ℕ ∨ A = 0) ∧ (B ∈ ℕ ∨ B = 0)) → ((A < B ∨ A = B) ↔ ((B − A) ∈ ℕ ∨ (B − A) = 0)))
67		leloet 4284	. . . 4 ⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (A ≤ B ↔ (A < B ∨ A = B)))
68		eleq1 1149	. . . . . 6 ⊢ (A = 0 → (A ∈ ℝ ↔ 0 ∈ ℝ))
69	35, 68	mpbiri 169	. . . . 5 ⊢ (A = 0 → A ∈ ℝ)
70	7, 69	jaoi 275	. . . 4 ⊢ ((A ∈ ℕ ∨ A = 0) → A ∈ ℝ)
71		nnret 4427	. . . . 5 ⊢ (B ∈ ℕ → B ∈ ℝ)
72		eleq1 1149	. . . . . 6 ⊢ (B = 0 → (B ∈ ℝ ↔ 0 ∈ ℝ))
73	35, 72	mpbiri 169	. . . . 5 ⊢ (B = 0 → B ∈ ℝ)
74	71, 73	jaoi 275	. . . 4 ⊢ ((B ∈ ℕ ∨ B = 0) → B ∈ ℝ)
75	67, 70, 74	syl2an 349	. . 3 ⊢ (((A ∈ ℕ ∨ A = 0) ∧ (B ∈ ℕ ∨ B = 0)) → (A ≤ B ↔ (A < B ∨ A = B)))
76		elnn0 4536	. . . 4 ⊢ ((B − A) ∈ ℕ₀ ↔ ((B − A) ∈ ℕ ∨ (B − A) = 0))
77	76	a1i 7	. . 3 ⊢ (((A ∈ ℕ ∨ A = 0) ∧ (B ∈ ℕ ∨ B = 0)) → ((B − A) ∈ ℕ₀ ↔ ((B − A) ∈ ℕ ∨ (B − A) = 0)))
78	66, 75, 77	3bitr4d 424	. 2 ⊢ (((A ∈ ℕ ∨ A = 0) ∧ (B ∈ ℕ ∨ B = 0)) → (A ≤ B ↔ (B − A) ∈ ℕ₀))
79		elnn0 4536	. 2 ⊢ (A ∈ ℕ₀ ↔ (A ∈ ℕ ∨ A = 0))
80		elnn0 4536	. 2 ⊢ (B ∈ ℕ₀ ↔ (B ∈ ℕ ∨ B = 0))
81	78, 79, 80	syl2anb 350	1 ⊢ ((A ∈ ℕ₀ ∧ B ∈ ℕ₀) → (A ≤ B ↔ (B − A) ∈ ℕ₀))

Colors of variables: wff set class

Syntax hints: ¬ wn 1 → wi 2 ↔ wb 127 ∨ wo 195 ∧ wa 196 = wceq 1091 ∈ wcel 1092 class class class wbr 2054 (class class class)co 3001 ℂcc 4026 ℝcr 4027 0cc0 4028 < clt 4033 − cmin 4089 -cneg 4090 ≤ cle 4092 ℕcn 4093 ℕ₀cn0 4094 ℤcz 4095

This theorem is referenced by: zaddclt 4590

This theorem was proved from axioms: ax-1 3 ax-2 4 ax-3 5 ax-mp 6 ax-4 673 ax-5 674 ax-6 675 ax-7 676 ax-gen 677 ax-8 798 ax-9 799 ax-10 800 ax-11 801 ax-12 802 ax-13 804 ax-14 805 ax-16 922 ax-17 925 ax-ext 1074 ax-rep 1075 ax-un 1076 ax-pow 1077 ax-reg 1078 ax-inf 1079

This theorem depends on definitions: df-bi 128 df-or 197 df-an 198 df-3or 582 df-3an 583 df-ex 679 df-sb 853 df-eu 1009 df-mo 1010 df-clab 1093 df-cleq 1097 df-clel 1099 df-ne 1192 df-ral 1205 df-rex 1206 df-reu 1207 df-rab 1208 df-v 1349 df-sbc 1441 df-dif 1489 df-un 1490 df-in 1491 df-ss 1492 df-pss 1494 df-nul 1708 df-if 1777 df-pw 1799 df-sn 1811 df-pr 1812 df-tp 1814 df-op 1815 df-uni 1920 df-int 1966 df-iun 1996 df-tr 2042 df-br 2063 df-opab 2098 df-eprel 2122 df-id 2125 df-po 2128 df-so 2138 df-fr 2169 df-we 2186 df-ord 2202 df-on 2203 df-lim 2204 df-suc 2205 df-om 2373 df-xp 2424 df-rel 2425 df-cnv 2426 df-co 2427 df-dm 2428 df-rn 2429 df-res 2430 df-ima 2431 df-fun 2432 df-fn 2433 df-f 2434 df-f1 2435 df-fv 2438 df-rdg 2970 df-opr 3003 df-oprab 3004 df-1o 3104 df-oadd 3106 df-omul 3107 df-er 3200 df-ec 3202 df-qs 3205 df-ni 3794 df-pli 3795 df-mi 3796 df-lti 3797 df-plpq 3829 df-mpq 3830 df-enq 3831 df-nq 3832 df-plq 3833 df-mq 3834 df-rq 3835 df-ltq 3836 df-1q 3837 df-np 3880 df-1p 3881 df-plp 3882 df-mp 3883 df-ltp 3884 df-plpr 3958 df-mpr 3959 df-enr 3960 df-nr 3961 df-plr 3962 df-mr 3963 df-ltr 3964 df-0r 3965 df-1r 3966 df-m1r 3967 df-c 4034 df-0 4035 df-1 4036 df-r 4038 df-plus 4039 df-mul 4040 df-lt 4041 df-sub 4133 df-neg 4135 df-le 4277 df-n 4423 df-n0 4535 df-z 4564

metamath.org