Metamath Proof Explorer


Theorem nndiffz1

Description: Upper set of the positive integers. (Contributed by Thierry Arnoux, 22-Aug-2017)

Ref Expression
Assertion nndiffz1 N 0 1 N = N + 1

Proof

Step Hyp Ref Expression
1 1z 1
2 nn0z N 0 N
3 elfz1 1 N j 1 N j 1 j j N
4 1 2 3 sylancr N 0 j 1 N j 1 j j N
5 3anass j 1 j j N j 1 j j N
6 4 5 bitrdi N 0 j 1 N j 1 j j N
7 6 baibd N 0 j j 1 N 1 j j N
8 7 baibd N 0 j 1 j j 1 N j N
9 8 notbid N 0 j 1 j ¬ j 1 N ¬ j N
10 simpl N j N
11 10 zred N j N
12 simpr N j j
13 12 zred N j j
14 11 13 ltnled N j N < j ¬ j N
15 zltp1le N j N < j N + 1 j
16 14 15 bitr3d N j ¬ j N N + 1 j
17 2 16 sylan N 0 j ¬ j N N + 1 j
18 17 adantr N 0 j 1 j ¬ j N N + 1 j
19 9 18 bitrd N 0 j 1 j ¬ j 1 N N + 1 j
20 19 pm5.32da N 0 j 1 j ¬ j 1 N 1 j N + 1 j
21 1red N 0 j N + 1 j 1
22 simpll N 0 j N + 1 j N 0
23 22 nn0red N 0 j N + 1 j N
24 23 21 readdcld N 0 j N + 1 j N + 1
25 simplr N 0 j N + 1 j j
26 25 zred N 0 j N + 1 j j
27 0p1e1 0 + 1 = 1
28 0red N 0 j N + 1 j 0
29 22 nn0ge0d N 0 j N + 1 j 0 N
30 28 23 21 29 leadd1dd N 0 j N + 1 j 0 + 1 N + 1
31 27 30 eqbrtrrid N 0 j N + 1 j 1 N + 1
32 simpr N 0 j N + 1 j N + 1 j
33 21 24 26 31 32 letrd N 0 j N + 1 j 1 j
34 33 ex N 0 j N + 1 j 1 j
35 34 pm4.71rd N 0 j N + 1 j 1 j N + 1 j
36 20 35 bitr4d N 0 j 1 j ¬ j 1 N N + 1 j
37 36 pm5.32da N 0 j 1 j ¬ j 1 N j N + 1 j
38 eldif j 1 N j ¬ j 1 N
39 elnnz1 j j 1 j
40 39 anbi1i j ¬ j 1 N j 1 j ¬ j 1 N
41 anass j 1 j ¬ j 1 N j 1 j ¬ j 1 N
42 38 40 41 3bitri j 1 N j 1 j ¬ j 1 N
43 42 a1i N 0 j 1 N j 1 j ¬ j 1 N
44 peano2nn0 N 0 N + 1 0
45 44 nn0zd N 0 N + 1
46 eluz1 N + 1 j N + 1 j N + 1 j
47 45 46 syl N 0 j N + 1 j N + 1 j
48 37 43 47 3bitr4d N 0 j 1 N j N + 1
49 48 eqrdv N 0 1 N = N + 1