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∈ℕ