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 ⊢ ( 𝜑 → ( 𝐴 ↑ 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 ⊢ ( 𝜑 → 𝐴 ∈ ℕ )