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	$⊢ φ \to A^{2} \in ℤ$
		posqsqznn.2	$⊢ φ \to A \in ℚ$
		posqsqznn.3	$⊢ φ \to 0 < A$
	Assertion	posqsqznn	$⊢ φ \to A \in ℕ$

Proof

Step	Hyp	Ref	Expression
1		posqsqznn.1	$⊢ φ \to A^{2} \in ℤ$
2		posqsqznn.2	$⊢ φ \to A \in ℚ$
3		posqsqznn.3	$⊢ φ \to 0 < A$
4	2	qred	$⊢ φ \to A \in ℝ$
5		0red	$⊢ φ \to 0 \in ℝ$
6	5 4 3	ltled	$⊢ φ \to 0 \leq A$
7	4 6	sqrtsqd	$⊢ φ \to \sqrt{A^{2}} = A$
8	7 2	eqeltrd	$⊢ φ \to \sqrt{A^{2}} \in ℚ$
9		zsqrtelqelz	$⊢ (A^{2} \in ℤ \land \sqrt{A^{2}} \in ℚ) \to \sqrt{A^{2}} \in ℤ$
10	1 8 9	syl2anc	$⊢ φ \to \sqrt{A^{2}} \in ℤ$
11	7 10	eqeltrrd	$⊢ φ \to A \in ℤ$
12		elnnz	$⊢ A \in ℕ \leftrightarrow (A \in ℤ \land 0 < A)$
13	11 3 12	sylanbrc	$⊢ φ \to A \in ℕ$