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

Theorem difelfznle 9095
 Description: The difference of two integers from a finite set of sequential nonnegative integers increased by the upper bound is also element of this finite set of sequential integers. (Contributed by Alexander van der Vekens, 12-Jun-2018.)
Assertion
Ref Expression
difelfznle

Proof of Theorem difelfznle
StepHypRef Expression
1 elfz2nn0 9075 . . . . . 6
2 nn0addcl 8274 . . . . . . . 8
32nn0zd 8417 . . . . . . 7
433adant3 935 . . . . . 6
51, 4sylbi 118 . . . . 5
6 elfzelz 8992 . . . . 5
7 zsubcl 8343 . . . . 5
85, 6, 7syl2anr 278 . . . 4
106zred 8419 . . . . . . 7
1110adantr 265 . . . . . 6
12 elfzel2 8990 . . . . . . . 8
1312zred 8419 . . . . . . 7
1413adantr 265 . . . . . 6
15 nn0readdcl 8298 . . . . . . . . 9
16153adant3 935 . . . . . . . 8
171, 16sylbi 118 . . . . . . 7
1817adantl 266 . . . . . 6
19 elfzle2 8994 . . . . . . 7
20 elfzle1 8993 . . . . . . . 8
21 nn0re 8248 . . . . . . . . . . . 12
22 nn0re 8248 . . . . . . . . . . . 12
2321, 22anim12ci 326 . . . . . . . . . . 11
24233adant3 935 . . . . . . . . . 10
251, 24sylbi 118 . . . . . . . . 9
26 addge02 7542 . . . . . . . . 9
2725, 26syl 14 . . . . . . . 8
2820, 27mpbid 139 . . . . . . 7
2919, 28anim12i 325 . . . . . 6
30 letr 7160 . . . . . . 7
3130imp 119 . . . . . 6
3211, 14, 18, 29, 31syl31anc 1149 . . . . 5
33323adant3 935 . . . 4
34 zre 8306 . . . . . . . 8
3521, 22anim12i 325 . . . . . . . . . . 11
36353adant3 935 . . . . . . . . . 10
371, 36sylbi 118 . . . . . . . . 9
38 readdcl 7065 . . . . . . . . 9
3937, 38syl 14 . . . . . . . 8
4034, 39anim12ci 326 . . . . . . 7
416, 40sylan 271 . . . . . 6
42413adant3 935 . . . . 5
43 subge0 7544 . . . . 5
4442, 43syl 14 . . . 4
4533, 44mpbird 160 . . 3
46 elnn0z 8315 . . 3
479, 45, 46sylanbrc 402 . 2
48 elfz3nn0 9078 . . 3
50 elfzelz 8992 . . . . . 6
51 zltnle 8348 . . . . . . . 8
5251ancoms 259 . . . . . . 7
53 zre 8306 . . . . . . . 8
54 ltle 7164 . . . . . . . 8
5553, 34, 54syl2anr 278 . . . . . . 7
5652, 55sylbird 163 . . . . . 6
576, 50, 56syl2an 277 . . . . 5
58573impia 1112 . . . 4
5950zred 8419 . . . . . . 7
6059adantl 266 . . . . . 6
6160, 11, 14leadd1d 7604 . . . . 5
62613adant3 935 . . . 4
6358, 62mpbid 139 . . 3
6418, 11, 14lesubadd2d 7609 . . . 4