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	$$⊢\phi \to A^2\in \mathbb{Z}$$
	posqsqznn.2	$$⊢\phi \to A\in \mathbb{Q}$$
	posqsqznn.3	$$⊢\phi \to 0<A$$
Assertion	posqsqznn	$$⊢\phi \to A\in \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		posqsqznn.1	$$⊢\phi \to A^2\in \mathbb{Z}$$
2		posqsqznn.2	$$⊢\phi \to A\in \mathbb{Q}$$
3		posqsqznn.3	$$⊢\phi \to 0<A$$
4	2	qred	$$⊢\phi \to A\in ℝ$$
5		0red	$$⊢\phi \to 0\in ℝ$$
6	5 4 3	ltled	$$⊢\phi \to 0\le A$$
7	4 6	sqrtsqd	$$⊢\phi \to \sqrt{A^2}=A$$
8	7 2	eqeltrd	$$⊢\phi \to \sqrt{A^2}\in \mathbb{Q}$$
9		zsqrtelqelz	$$⊢\left(A^2\in \mathbb{Z}\wedge \sqrt{A^2}\in \mathbb{Q}\right)\to \sqrt{A^2}\in \mathbb{Z}$$
10	1 8 9	syl2anc	$$⊢\phi \to \sqrt{A^2}\in \mathbb{Z}$$
11	7 10	eqeltrrd	$$⊢\phi \to A\in \mathbb{Z}$$
12		elnnz	$$⊢A\in \mathbb{N}\leftrightarrow \left(A\in \mathbb{Z}\wedge 0<A\right)$$
13	11 3 12	sylanbrc	$$⊢\phi \to A\in \mathbb{N}$$