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

Theorem znege1 10781
 Description: The absolute value of the difference between two unequal integers is at least one. (Contributed by Jim Kingdon, 31-Jan-2022.)
Assertion
Ref Expression
znege1

Proof of Theorem znege1
StepHypRef Expression
1 zltp1le 8556 . . . . . 6
213adant3 959 . . . . 5
32biimpa 290 . . . 4
4 simpl1 942 . . . . . 6
54zred 8620 . . . . 5
6 1red 7266 . . . . 5
7 simpl2 943 . . . . . 6
87zred 8620 . . . . 5
95, 6, 8leaddsub2d 7784 . . . 4
103, 9mpbid 145 . . 3
11 simpr 108 . . . . 5
125, 8, 11ltled 7365 . . . 4
135, 8, 12abssuble0d 10282 . . 3
1410, 13breqtrrd 3831 . 2
15 simpr 108 . . 3
16 simpl3 944 . . 3
1715, 16pm2.21ddne 2332 . 2
18 simpr 108 . . . . 5
19 simpl2 943 . . . . . 6
20 simpl1 942 . . . . . 6
21 zltp1le 8556 . . . . . 6
2219, 20, 21syl2anc 403 . . . . 5
2318, 22mpbid 145 . . . 4
2419zred 8620 . . . . 5
25 1red 7266 . . . . 5
2620zred 8620 . . . . 5
2724, 25, 26leaddsub2d 7784 . . . 4
2823, 27mpbid 145 . . 3
2924, 26, 18ltled 7365 . . . 4
3024, 26, 29abssubge0d 10281 . . 3
3128, 30breqtrrd 3831 . 2
32 ztri3or 8545 . . 3