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 ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 < 𝐵 ↔ ( 𝐵 − 𝐴 ) ∈ ℕ ) )

Proof

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