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 )