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	⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) ∈ ℤ )
	posqsqznn.2	⊢ ( 𝜑 → 𝐴 ∈ ℚ )
	posqsqznn.3	⊢ ( 𝜑 → 0 < 𝐴 )
Assertion	posqsqznn	⊢ ( 𝜑 → 𝐴 ∈ ℕ )

Proof

Step	Hyp	Ref	Expression
1		posqsqznn.1	⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) ∈ ℤ )
2		posqsqznn.2	⊢ ( 𝜑 → 𝐴 ∈ ℚ )
3		posqsqznn.3	⊢ ( 𝜑 → 0 < 𝐴 )
4	2	qred	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
5		0red	⊢ ( 𝜑 → 0 ∈ ℝ )
6	5 4 3	ltled	⊢ ( 𝜑 → 0 ≤ 𝐴 )
7	4 6	sqrtsqd	⊢ ( 𝜑 → ( √ ‘ ( 𝐴 ↑ 2 ) ) = 𝐴 )
8	7 2	eqeltrd	⊢ ( 𝜑 → ( √ ‘ ( 𝐴 ↑ 2 ) ) ∈ ℚ )
9		zsqrtelqelz	⊢ ( ( ( 𝐴 ↑ 2 ) ∈ ℤ ∧ ( √ ‘ ( 𝐴 ↑ 2 ) ) ∈ ℚ ) → ( √ ‘ ( 𝐴 ↑ 2 ) ) ∈ ℤ )
10	1 8 9	syl2anc	⊢ ( 𝜑 → ( √ ‘ ( 𝐴 ↑ 2 ) ) ∈ ℤ )
11	7 10	eqeltrrd	⊢ ( 𝜑 → 𝐴 ∈ ℤ )
12		elnnz	⊢ ( 𝐴 ∈ ℕ ↔ ( 𝐴 ∈ ℤ ∧ 0 < 𝐴 ) )
13	11 3 12	sylanbrc	⊢ ( 𝜑 → 𝐴 ∈ ℕ )