Metamath Proof Explorer


Theorem eluzsubiOLD

Description: Obsolete version of eluzsubi as of 7-Feb-2025. (Contributed by Paul Chapman, 22-Nov-2007) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses eluzsubi.1 M
eluzsubi.2 K
Assertion eluzsubiOLD N M + K N K M

Proof

Step Hyp Ref Expression
1 eluzsubi.1 M
2 eluzsubi.2 K
3 eluzelz N M + K N
4 zsubcl N K N K
5 3 2 4 sylancl N M + K N K
6 zaddcl M K M + K
7 1 2 6 mp2an M + K
8 7 eluz1i N M + K N M + K N
9 1 zrei M
10 2 zrei K
11 zre N N
12 leaddsub M K N M + K N M N K
13 9 10 11 12 mp3an12i N M + K N M N K
14 13 biimpa N M + K N M N K
15 8 14 sylbi N M + K M N K
16 1 eluz1i N K M N K M N K
17 5 15 16 sylanbrc N M + K N K M