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

Theorem fznlem 8905
 Description: A finite set of sequential integers is empty if the bounds are reversed. (Contributed by Jim Kingdon, 16-Apr-2020.)
Assertion
Ref Expression
fznlem

Proof of Theorem fznlem
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 zre 8249 . . . . . . . . . . 11
2 zre 8249 . . . . . . . . . . 11
3 lenlt 7094 . . . . . . . . . . 11
41, 2, 3syl2an 273 . . . . . . . . . 10
54biimpd 132 . . . . . . . . 9
65con2d 554 . . . . . . . 8
76imp 115 . . . . . . 7
87adantr 261 . . . . . 6
9 simplll 485 . . . . . . . 8
109zred 8360 . . . . . . 7
11 simpr 103 . . . . . . . 8
1211zred 8360 . . . . . . 7
13 simpllr 486 . . . . . . . 8
1413zred 8360 . . . . . . 7
15 letr 7101 . . . . . . 7
1610, 12, 14, 15syl3anc 1135 . . . . . 6
178, 16mtod 589 . . . . 5
1817ralrimiva 2392 . . . 4
19 rabeq0 3247 . . . 4
2018, 19sylibr 137 . . 3
21 fzval 8876 . . . . 5
2221eqeq1d 2048 . . . 4