Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  ubmelm1fzo Unicode version

Theorem ubmelm1fzo 9996
 Description: The result of subtracting 1 and an integer of a half-open range of nonnegative integers from the upper bound of this range is contained in this range. (Contributed by AV, 23-Mar-2018.) (Revised by AV, 30-Oct-2018.)
Assertion
Ref Expression
ubmelm1fzo ..^ ..^

Proof of Theorem ubmelm1fzo
StepHypRef Expression
1 elfzo0 9952 . 2 ..^
2 nnz 9066 . . . . . . . . 9
32adantr 274 . . . . . . . 8
4 nn0z 9067 . . . . . . . . 9
54adantl 275 . . . . . . . 8
63, 5zsubcld 9171 . . . . . . 7
76ancoms 266 . . . . . 6
8 peano2zm 9085 . . . . . 6
97, 8syl 14 . . . . 5
1093adant3 1001 . . . 4
11 simp3 983 . . . . . 6
124, 2anim12i 336 . . . . . . . 8
13123adant3 1001 . . . . . . 7
14 znnsub 9098 . . . . . . 7
1513, 14syl 14 . . . . . 6
1611, 15mpbid 146 . . . . 5
17 nnm1ge0 9130 . . . . 5
1816, 17syl 14 . . . 4
19 elnn0z 9060 . . . 4
2010, 18, 19sylanbrc 413 . . 3
21 simp2 982 . . 3
22 nncn 8721 . . . . . . 7
2322adantl 275 . . . . . 6
24 nn0cn 8980 . . . . . . 7
2524adantr 274 . . . . . 6
26 1cnd 7775 . . . . . 6
2723, 25, 26subsub4d 8097 . . . . 5
28 nn0p1gt0 8999 . . . . . . 7
2928adantr 274 . . . . . 6
30 nn0re 8979 . . . . . . . 8
31 peano2re 7891 . . . . . . . 8
3230, 31syl 14 . . . . . . 7
33 nnre 8720 . . . . . . 7
34 ltsubpos 8209 . . . . . . 7
3532, 33, 34syl2an 287 . . . . . 6
3629, 35mpbid 146 . . . . 5
3727, 36eqbrtrd 3945 . . . 4