Metamath Proof Explorer

Theorem eluz2cnn0n1

Description: An integer greater than 1 is a complex number not equal to 0 or 1. (Contributed by AV, 23-May-2020)

Ref Expression
Assertion eluz2cnn0n1 
|- ( B e. ( ZZ>= ` 2 ) -> B e. ( CC \ { 0 , 1 } ) )

Proof

Step Hyp Ref Expression
1 nncn 
 |-  ( B e. NN -> B e. CC )
2 1 adantr 
 |-  ( ( B e. NN /\ B =/= 1 ) -> B e. CC )
3 nnne0 
 |-  ( B e. NN -> B =/= 0 )
4 3 adantr 
 |-  ( ( B e. NN /\ B =/= 1 ) -> B =/= 0 )
5 simpr 
 |-  ( ( B e. NN /\ B =/= 1 ) -> B =/= 1 )
6 2 4 5 3jca 
 |-  ( ( B e. NN /\ B =/= 1 ) -> ( B e. CC /\ B =/= 0 /\ B =/= 1 ) )
7 eluz2b3 
 |-  ( B e. ( ZZ>= ` 2 ) <-> ( B e. NN /\ B =/= 1 ) )
8 eldifpr 
 |-  ( B e. ( CC \ { 0 , 1 } ) <-> ( B e. CC /\ B =/= 0 /\ B =/= 1 ) )
9 6 7 8 3imtr4i 
 |-  ( B e. ( ZZ>= ` 2 ) -> B e. ( CC \ { 0 , 1 } ) )