Metamath Proof Explorer


Theorem uzuzle23

Description: An integer in the upper set of integers starting at 3 is element of the upper set of integers starting at 2. (Contributed by Alexander van der Vekens, 17-Sep-2018)

Ref Expression
Assertion uzuzle23 A3A2

Proof

Step Hyp Ref Expression
1 2z 2
2 2re 2
3 3re 3
4 2lt3 2<3
5 2 3 4 ltleii 23
6 eluzuzle 223A3A2
7 1 5 6 mp2an A3A2