nonsq

Description: Any integer strictly between two adjacent squares has an irrational square root. (Contributed by Stefan O'Rear, 15-Sep-2014)

		Ref	Expression
	Assertion	nonsq	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0}) \land (B^{2} < A \land A < {(B + 1)}^{2})) \to \neg \sqrt{A} \in ℚ$

Proof

Step	Hyp	Ref	Expression
1		nn0z	$⊢ B \in ℕ_{0} \to B \in ℤ$
2	1	ad2antlr	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0}) \land (B^{2} < A \land A < {(B + 1)}^{2})) \to B \in ℤ$
3		simprl	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0}) \land (B^{2} < A \land A < {(B + 1)}^{2})) \to B^{2} < A$
4		nn0re	$⊢ A \in ℕ_{0} \to A \in ℝ$
5	4	ad2antrr	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0}) \land (B^{2} < A \land A < {(B + 1)}^{2})) \to A \in ℝ$
6	5	recnd	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0}) \land (B^{2} < A \land A < {(B + 1)}^{2})) \to A \in ℂ$
7	6	sqsqrtd	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0}) \land (B^{2} < A \land A < {(B + 1)}^{2})) \to {\sqrt{A}}^{2} = A$
8	3 7	breqtrrd	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0}) \land (B^{2} < A \land A < {(B + 1)}^{2})) \to B^{2} < {\sqrt{A}}^{2}$
9		nn0re	$⊢ B \in ℕ_{0} \to B \in ℝ$
10	9	ad2antlr	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0}) \land (B^{2} < A \land A < {(B + 1)}^{2})) \to B \in ℝ$
11		nn0ge0	$⊢ A \in ℕ_{0} \to 0 \leq A$
12	11	ad2antrr	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0}) \land (B^{2} < A \land A < {(B + 1)}^{2})) \to 0 \leq A$
13	5 12	resqrtcld	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0}) \land (B^{2} < A \land A < {(B + 1)}^{2})) \to \sqrt{A} \in ℝ$
14		nn0ge0	$⊢ B \in ℕ_{0} \to 0 \leq B$
15	14	ad2antlr	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0}) \land (B^{2} < A \land A < {(B + 1)}^{2})) \to 0 \leq B$
16	5 12	sqrtge0d	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0}) \land (B^{2} < A \land A < {(B + 1)}^{2})) \to 0 \leq \sqrt{A}$
17	10 13 15 16	lt2sqd	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0}) \land (B^{2} < A \land A < {(B + 1)}^{2})) \to (B < \sqrt{A} \leftrightarrow B^{2} < {\sqrt{A}}^{2})$
18	8 17	mpbird	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0}) \land (B^{2} < A \land A < {(B + 1)}^{2})) \to B < \sqrt{A}$
19		simprr	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0}) \land (B^{2} < A \land A < {(B + 1)}^{2})) \to A < {(B + 1)}^{2}$
20	7 19	eqbrtrd	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0}) \land (B^{2} < A \land A < {(B + 1)}^{2})) \to {\sqrt{A}}^{2} < {(B + 1)}^{2}$
21		peano2re	$⊢ B \in ℝ \to B + 1 \in ℝ$
22	10 21	syl	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0}) \land (B^{2} < A \land A < {(B + 1)}^{2})) \to B + 1 \in ℝ$
23		peano2nn0	$⊢ B \in ℕ_{0} \to B + 1 \in ℕ_{0}$
24		nn0ge0	$⊢ B + 1 \in ℕ_{0} \to 0 \leq B + 1$
25	23 24	syl	$⊢ B \in ℕ_{0} \to 0 \leq B + 1$
26	25	ad2antlr	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0}) \land (B^{2} < A \land A < {(B + 1)}^{2})) \to 0 \leq B + 1$
27	13 22 16 26	lt2sqd	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0}) \land (B^{2} < A \land A < {(B + 1)}^{2})) \to (\sqrt{A} < B + 1 \leftrightarrow {\sqrt{A}}^{2} < {(B + 1)}^{2})$
28	20 27	mpbird	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0}) \land (B^{2} < A \land A < {(B + 1)}^{2})) \to \sqrt{A} < B + 1$
29		btwnnz	$⊢ (B \in ℤ \land B < \sqrt{A} \land \sqrt{A} < B + 1) \to \neg \sqrt{A} \in ℤ$
30	2 18 28 29	syl3anc	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0}) \land (B^{2} < A \land A < {(B + 1)}^{2})) \to \neg \sqrt{A} \in ℤ$
31		nn0z	$⊢ A \in ℕ_{0} \to A \in ℤ$
32	31	ad2antrr	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0}) \land (B^{2} < A \land A < {(B + 1)}^{2})) \to A \in ℤ$
33		zsqrtelqelz	$⊢ (A \in ℤ \land \sqrt{A} \in ℚ) \to \sqrt{A} \in ℤ$
34	33	ex	$⊢ A \in ℤ \to (\sqrt{A} \in ℚ \to \sqrt{A} \in ℤ)$
35	32 34	syl	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0}) \land (B^{2} < A \land A < {(B + 1)}^{2})) \to (\sqrt{A} \in ℚ \to \sqrt{A} \in ℤ)$
36	30 35	mtod	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0}) \land (B^{2} < A \land A < {(B + 1)}^{2})) \to \neg \sqrt{A} \in ℚ$

Metamath Proof Explorer

Theorem nonsq

Proof