Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  difelfznle Structured version   Visualization version   Unicode version

Theorem difelfznle 11902
 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 11882 . . . . . 6
2 nn0addcl 10902 . . . . . . . 8
32nn0zd 11035 . . . . . . 7
433adant3 1027 . . . . . 6
51, 4sylbi 199 . . . . 5
6 elfzelz 11797 . . . . 5
7 zsubcl 10976 . . . . 5
85, 6, 7syl2anr 481 . . . 4
106zred 11037 . . . . . . 7
1110adantr 467 . . . . . 6
12 elfzel2 11795 . . . . . . . 8
1312zred 11037 . . . . . . 7
1413adantr 467 . . . . . 6
15 nn0readdcl 10928 . . . . . . . . 9
16153adant3 1027 . . . . . . . 8
171, 16sylbi 199 . . . . . . 7
1817adantl 468 . . . . . 6
19 elfzle2 11800 . . . . . . 7
20 elfzle1 11799 . . . . . . . 8
21 nn0re 10875 . . . . . . . . . . . 12
22 nn0re 10875 . . . . . . . . . . . 12
2321, 22anim12ci 570 . . . . . . . . . . 11
24233adant3 1027 . . . . . . . . . 10
251, 24sylbi 199 . . . . . . . . 9
26 addge02 10122 . . . . . . . . 9
2725, 26syl 17 . . . . . . . 8
2820, 27mpbid 214 . . . . . . 7
2919, 28anim12i 569 . . . . . 6
30 letr 9724 . . . . . . 7
3130imp 431 . . . . . 6
3211, 14, 18, 29, 31syl31anc 1270 . . . . 5
33323adant3 1027 . . . 4
34 zre 10938 . . . . . . . 8
3521, 22anim12i 569 . . . . . . . . . . 11
36353adant3 1027 . . . . . . . . . 10
371, 36sylbi 199 . . . . . . . . 9
38 readdcl 9619 . . . . . . . . 9
3937, 38syl 17 . . . . . . . 8
4034, 39anim12ci 570 . . . . . . 7
416, 40sylan 474 . . . . . 6
42413adant3 1027 . . . . 5
43 subge0 10124 . . . . 5
4442, 43syl 17 . . . 4
4533, 44mpbird 236 . . 3
46 elnn0z 10947 . . 3
479, 45, 46sylanbrc 669 . 2
48 elfz3nn0 11885 . . 3
50 elfzelz 11797 . . . . . 6
51 zre 10938 . . . . . . 7
52 ltnle 9710 . . . . . . . . 9
5352ancoms 455 . . . . . . . 8
54 ltle 9719 . . . . . . . . 9
5554ancoms 455 . . . . . . . 8
5653, 55sylbird 239 . . . . . . 7
5734, 51, 56syl2an 480 . . . . . 6
586, 50, 57syl2an 480 . . . . 5
59583impia 1204 . . . 4
6050zred 11037 . . . . . . 7
6160adantl 468 . . . . . 6
6261, 11, 14leadd1d 10204 . . . . 5
63623adant3 1027 . . . 4
6459, 63mpbid 214 . . 3
6518, 11, 14lesubadd2d 10209 . . . 4