Metamath Proof Explorer


Theorem faclbnd4

Description: Variant of faclbnd5 providing a non-strict lower bound. (Contributed by NM, 23-Dec-2005)

Ref Expression
Assertion faclbnd4 N0K0M0NKMN2K2MM+KN!

Proof

Step Hyp Ref Expression
1 elnn0 N0NN=0
2 faclbnd4lem4 NK0M0NKMN2K2MM+KN!
3 2 3com13 M0K0NNKMN2K2MM+KN!
4 3 3expa M0K0NNKMN2K2MM+KN!
5 faclbnd4lem3 M0K0N=0NKMN2K2MM+KN!
6 4 5 jaodan M0K0NN=0NKMN2K2MM+KN!
7 1 6 sylan2b M0K0N0NKMN2K2MM+KN!
8 7 3impa M0K0N0NKMN2K2MM+KN!
9 8 3com13 N0K0M0NKMN2K2MM+KN!