Metamath Proof Explorer

Theorem nnsub

Description: Subtraction of positive integers. (Contributed by NM, 20-Aug-2001) (Revised by Mario Carneiro, 16-May-2014)

Ref Expression
Assertion nnsub ⊢ A ∈ ℕ ∧ B ∈ ℕ → A < B ↔ B − A ∈ ℕ

Proof

Step Hyp Ref Expression
1 breq2 ⊢ x = 1 → z < x ↔ z < 1
2 oveq1 ⊢ x = 1 → x − z = 1 − z
3 2 eleq1d ⊢ x = 1 → x − z ∈ ℕ ↔ 1 − z ∈ ℕ
4 1 3 imbi12d ⊢ x = 1 → z < x → x − z ∈ ℕ ↔ z < 1 → 1 − z ∈ ℕ
5 4 ralbidv ⊢ x = 1 → ∀ z ∈ ℕ z < x → x − z ∈ ℕ ↔ ∀ z ∈ ℕ z < 1 → 1 − z ∈ ℕ
6 breq2 ⊢ x = y → z < x ↔ z < y
7 oveq1 ⊢ x = y → x − z = y − z
8 7 eleq1d ⊢ x = y → x − z ∈ ℕ ↔ y − z ∈ ℕ
9 6 8 imbi12d ⊢ x = y → z < x → x − z ∈ ℕ ↔ z < y → y − z ∈ ℕ
10 9 ralbidv ⊢ x = y → ∀ z ∈ ℕ z < x → x − z ∈ ℕ ↔ ∀ z ∈ ℕ z < y → y − z ∈ ℕ
11 breq2 ⊢ x = y + 1 → z < x ↔ z < y + 1
12 oveq1 ⊢ x = y + 1 → x − z = y + 1 - z
13 12 eleq1d ⊢ x = y + 1 → x − z ∈ ℕ ↔ y + 1 - z ∈ ℕ
14 11 13 imbi12d ⊢ x = y + 1 → z < x → x − z ∈ ℕ ↔ z < y + 1 → y + 1 - z ∈ ℕ
15 14 ralbidv ⊢ x = y + 1 → ∀ z ∈ ℕ z < x → x − z ∈ ℕ ↔ ∀ z ∈ ℕ z < y + 1 → y + 1 - z ∈ ℕ
16 breq2 ⊢ x = B → z < x ↔ z < B
17 oveq1 ⊢ x = B → x − z = B − z
18 17 eleq1d ⊢ x = B → x − z ∈ ℕ ↔ B − z ∈ ℕ
19 16 18 imbi12d ⊢ x = B → z < x → x − z ∈ ℕ ↔ z < B → B − z ∈ ℕ
20 19 ralbidv ⊢ x = B → ∀ z ∈ ℕ z < x → x − z ∈ ℕ ↔ ∀ z ∈ ℕ z < B → B − z ∈ ℕ
21 nnnlt1 ⊢ z ∈ ℕ → ¬ z < 1
22 21 pm2.21d ⊢ z ∈ ℕ → z < 1 → 1 − z ∈ ℕ
23 22 rgen ⊢ ∀ z ∈ ℕ z < 1 → 1 − z ∈ ℕ
24 breq1 ⊢ z = x → z < y ↔ x < y
25 oveq2 ⊢ z = x → y − z = y − x
26 25 eleq1d ⊢ z = x → y − z ∈ ℕ ↔ y − x ∈ ℕ
27 24 26 imbi12d ⊢ z = x → z < y → y − z ∈ ℕ ↔ x < y → y − x ∈ ℕ
28 27 cbvralvw ⊢ ∀ z ∈ ℕ z < y → y − z ∈ ℕ ↔ ∀ x ∈ ℕ x < y → y − x ∈ ℕ
29 nncn ⊢ y ∈ ℕ → y ∈ ℂ
30 29 adantr ⊢ y ∈ ℕ ∧ z ∈ ℕ → y ∈ ℂ
31 ax-1cn ⊢ 1 ∈ ℂ
32 pncan ⊢ y ∈ ℂ ∧ 1 ∈ ℂ → y + 1 - 1 = y
33 30 31 32 sylancl ⊢ y ∈ ℕ ∧ z ∈ ℕ → y + 1 - 1 = y
34 simpl ⊢ y ∈ ℕ ∧ z ∈ ℕ → y ∈ ℕ
35 33 34 eqeltrd ⊢ y ∈ ℕ ∧ z ∈ ℕ → y + 1 - 1 ∈ ℕ
36 oveq2 ⊢ z = 1 → y + 1 - z = y + 1 - 1
37 36 eleq1d ⊢ z = 1 → y + 1 - z ∈ ℕ ↔ y + 1 - 1 ∈ ℕ
38 35 37 syl5ibrcom ⊢ y ∈ ℕ ∧ z ∈ ℕ → z = 1 → y + 1 - z ∈ ℕ
39 38 2a1dd ⊢ y ∈ ℕ ∧ z ∈ ℕ → z = 1 → ∀ x ∈ ℕ x < y → y − x ∈ ℕ → z < y + 1 → y + 1 - z ∈ ℕ
40 breq1 ⊢ x = z − 1 → x < y ↔ z − 1 < y
41 oveq2 ⊢ x = z − 1 → y − x = y − z − 1
42 41 eleq1d ⊢ x = z − 1 → y − x ∈ ℕ ↔ y − z − 1 ∈ ℕ
43 40 42 imbi12d ⊢ x = z − 1 → x < y → y − x ∈ ℕ ↔ z − 1 < y → y − z − 1 ∈ ℕ
44 43 rspcv ⊢ z − 1 ∈ ℕ → ∀ x ∈ ℕ x < y → y − x ∈ ℕ → z − 1 < y → y − z − 1 ∈ ℕ
45 nnre ⊢ z ∈ ℕ → z ∈ ℝ
46 nnre ⊢ y ∈ ℕ → y ∈ ℝ
47 1re ⊢ 1 ∈ ℝ
48 ltsubadd ⊢ z ∈ ℝ ∧ 1 ∈ ℝ ∧ y ∈ ℝ → z − 1 < y ↔ z < y + 1
49 47 48 mp3an2 ⊢ z ∈ ℝ ∧ y ∈ ℝ → z − 1 < y ↔ z < y + 1
50 45 46 49 syl2anr ⊢ y ∈ ℕ ∧ z ∈ ℕ → z − 1 < y ↔ z < y + 1
51 nncn ⊢ z ∈ ℕ → z ∈ ℂ
52 subsub3 ⊢ y ∈ ℂ ∧ z ∈ ℂ ∧ 1 ∈ ℂ → y − z − 1 = y + 1 - z
53 31 52 mp3an3 ⊢ y ∈ ℂ ∧ z ∈ ℂ → y − z − 1 = y + 1 - z
54 29 51 53 syl2an ⊢ y ∈ ℕ ∧ z ∈ ℕ → y − z − 1 = y + 1 - z
55 54 eleq1d ⊢ y ∈ ℕ ∧ z ∈ ℕ → y − z − 1 ∈ ℕ ↔ y + 1 - z ∈ ℕ
56 50 55 imbi12d ⊢ y ∈ ℕ ∧ z ∈ ℕ → z − 1 < y → y − z − 1 ∈ ℕ ↔ z < y + 1 → y + 1 - z ∈ ℕ
57 56 biimpd ⊢ y ∈ ℕ ∧ z ∈ ℕ → z − 1 < y → y − z − 1 ∈ ℕ → z < y + 1 → y + 1 - z ∈ ℕ
58 44 57 syl9r ⊢ y ∈ ℕ ∧ z ∈ ℕ → z − 1 ∈ ℕ → ∀ x ∈ ℕ x < y → y − x ∈ ℕ → z < y + 1 → y + 1 - z ∈ ℕ
59 nn1m1nn ⊢ z ∈ ℕ → z = 1 ∨ z − 1 ∈ ℕ
60 59 adantl ⊢ y ∈ ℕ ∧ z ∈ ℕ → z = 1 ∨ z − 1 ∈ ℕ
61 39 58 60 mpjaod ⊢ y ∈ ℕ ∧ z ∈ ℕ → ∀ x ∈ ℕ x < y → y − x ∈ ℕ → z < y + 1 → y + 1 - z ∈ ℕ
62 61 ralrimdva ⊢ y ∈ ℕ → ∀ x ∈ ℕ x < y → y − x ∈ ℕ → ∀ z ∈ ℕ z < y + 1 → y + 1 - z ∈ ℕ
63 28 62 biimtrid ⊢ y ∈ ℕ → ∀ z ∈ ℕ z < y → y − z ∈ ℕ → ∀ z ∈ ℕ z < y + 1 → y + 1 - z ∈ ℕ
64 5 10 15 20 23 63 nnind ⊢ B ∈ ℕ → ∀ z ∈ ℕ z < B → B − z ∈ ℕ
65 breq1 ⊢ z = A → z < B ↔ A < B
66 oveq2 ⊢ z = A → B − z = B − A
67 66 eleq1d ⊢ z = A → B − z ∈ ℕ ↔ B − A ∈ ℕ
68 65 67 imbi12d ⊢ z = A → z < B → B − z ∈ ℕ ↔ A < B → B − A ∈ ℕ
69 68 rspcva ⊢ A ∈ ℕ ∧ ∀ z ∈ ℕ z < B → B − z ∈ ℕ → A < B → B − A ∈ ℕ
70 64 69 sylan2 ⊢ A ∈ ℕ ∧ B ∈ ℕ → A < B → B − A ∈ ℕ
71 nngt0 ⊢ B − A ∈ ℕ → 0 < B − A
72 nnre ⊢ A ∈ ℕ → A ∈ ℝ
73 nnre ⊢ B ∈ ℕ → B ∈ ℝ
74 posdif ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B ↔ 0 < B − A
75 72 73 74 syl2an ⊢ A ∈ ℕ ∧ B ∈ ℕ → A < B ↔ 0 < B − A
76 71 75 imbitrrid ⊢ A ∈ ℕ ∧ B ∈ ℕ → B − A ∈ ℕ → A < B
77 70 76 impbid ⊢ A ∈ ℕ ∧ B ∈ ℕ → A < B ↔ B − A ∈ ℕ