# Metamath Proof Explorer

## Theorem 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 ${⊢}\left(\left({A}\in {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\right)\wedge \left({{B}}^{2}<{A}\wedge {A}<{\left({B}+1\right)}^{2}\right)\right)\to ¬\sqrt{{A}}\in ℚ$

### Proof

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