This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem znsqcld

Description: The square of a nonzero integer is a positive integer. (Contributed by Thierry Arnoux, 2-Feb-2020)

Ref Expression
Hypotheses znsqcld.1 
|- ( ph -> N e. ZZ )
znsqcld.2 
|- ( ph -> N =/= 0 )
Assertion znsqcld 
|- ( ph -> ( N ^ 2 ) e. NN )

Proof

Step Hyp Ref Expression
1 znsqcld.1 
 |-  ( ph -> N e. ZZ )
2 znsqcld.2 
 |-  ( ph -> N =/= 0 )
3 1 zcnd 
 |-  ( ph -> N e. CC )
4 2z 
 |-  2 e. ZZ
5 4 a1i 
 |-  ( ph -> 2 e. ZZ )
6 3 2 5 expne0d 
 |-  ( ph -> ( N ^ 2 ) =/= 0 )
7 6 neneqd 
 |-  ( ph -> -. ( N ^ 2 ) = 0 )
8 zsqcl2 
 |-  ( N e. ZZ -> ( N ^ 2 ) e. NN0 )
9 1 8 syl 
 |-  ( ph -> ( N ^ 2 ) e. NN0 )
10 elnn0 
 |-  ( ( N ^ 2 ) e. NN0 <-> ( ( N ^ 2 ) e. NN \/ ( N ^ 2 ) = 0 ) )
11 9 10 sylib 
 |-  ( ph -> ( ( N ^ 2 ) e. NN \/ ( N ^ 2 ) = 0 ) )
12 11 orcomd 
 |-  ( ph -> ( ( N ^ 2 ) = 0 \/ ( N ^ 2 ) e. NN ) )
13 12 ord 
 |-  ( ph -> ( -. ( N ^ 2 ) = 0 -> ( N ^ 2 ) e. NN ) )
14 7 13 mpd 
 |-  ( ph -> ( N ^ 2 ) e. NN )