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

Metamath Proof Explorer

Theorem posqsqznn

Description: When a positive rational squared is an integer, the rational is a positive integer. zsqrtelqelz with all terms squared and positive. (Contributed by SN, 23-Aug-2024)

Ref Expression
Hypotheses posqsqznn.1 
|- ( ph -> ( A ^ 2 ) e. ZZ )
posqsqznn.2 
|- ( ph -> A e. QQ )
posqsqznn.3 
|- ( ph -> 0 < A )
Assertion posqsqznn 
|- ( ph -> A e. NN )

Proof

Step Hyp Ref Expression
1 posqsqznn.1 
 |-  ( ph -> ( A ^ 2 ) e. ZZ )
2 posqsqznn.2 
 |-  ( ph -> A e. QQ )
3 posqsqznn.3 
 |-  ( ph -> 0 < A )
4 2 qred 
 |-  ( ph -> A e. RR )
5 0red 
 |-  ( ph -> 0 e. RR )
6 5 4 3 ltled 
 |-  ( ph -> 0 <_ A )
7 4 6 sqrtsqd 
 |-  ( ph -> ( sqrt ` ( A ^ 2 ) ) = A )
8 7 2 eqeltrd 
 |-  ( ph -> ( sqrt ` ( A ^ 2 ) ) e. QQ )
9 zsqrtelqelz 
 |-  ( ( ( A ^ 2 ) e. ZZ /\ ( sqrt ` ( A ^ 2 ) ) e. QQ ) -> ( sqrt ` ( A ^ 2 ) ) e. ZZ )
10 1 8 9 syl2anc 
 |-  ( ph -> ( sqrt ` ( A ^ 2 ) ) e. ZZ )
11 7 10 eqeltrrd 
 |-  ( ph -> A e. ZZ )
12 elnnz 
 |-  ( A e. NN <-> ( A e. ZZ /\ 0 < A ) )
13 11 3 12 sylanbrc 
 |-  ( ph -> A e. NN )