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 ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ( ( 𝐵 ↑ 2 ) < 𝐴 ∧ 𝐴 < ( ( 𝐵 + 1 ) ↑ 2 ) ) ) → ¬ ( √ ‘ 𝐴 ) ∈ ℚ )

Proof

Step Hyp Ref Expression
1 nn0z ⊢ ( 𝐵 ∈ ℕ0 → 𝐵 ∈ ℤ )
2 1 ad2antlr ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ( ( 𝐵 ↑ 2 ) < 𝐴 ∧ 𝐴 < ( ( 𝐵 + 1 ) ↑ 2 ) ) ) → 𝐵 ∈ ℤ )
3 simprl ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ( ( 𝐵 ↑ 2 ) < 𝐴 ∧ 𝐴 < ( ( 𝐵 + 1 ) ↑ 2 ) ) ) → ( 𝐵 ↑ 2 ) < 𝐴 )
4 nn0re ⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ℝ )
5 4 ad2antrr ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ( ( 𝐵 ↑ 2 ) < 𝐴 ∧ 𝐴 < ( ( 𝐵 + 1 ) ↑ 2 ) ) ) → 𝐴 ∈ ℝ )
6 5 recnd ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ( ( 𝐵 ↑ 2 ) < 𝐴 ∧ 𝐴 < ( ( 𝐵 + 1 ) ↑ 2 ) ) ) → 𝐴 ∈ ℂ )
7 6 sqsqrtd ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ( ( 𝐵 ↑ 2 ) < 𝐴 ∧ 𝐴 < ( ( 𝐵 + 1 ) ↑ 2 ) ) ) → ( ( √ ‘ 𝐴 ) ↑ 2 ) = 𝐴 )
8 3 7 breqtrrd ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ( ( 𝐵 ↑ 2 ) < 𝐴 ∧ 𝐴 < ( ( 𝐵 + 1 ) ↑ 2 ) ) ) → ( 𝐵 ↑ 2 ) < ( ( √ ‘ 𝐴 ) ↑ 2 ) )
9 nn0re ⊢ ( 𝐵 ∈ ℕ0 → 𝐵 ∈ ℝ )
10 9 ad2antlr ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ( ( 𝐵 ↑ 2 ) < 𝐴 ∧ 𝐴 < ( ( 𝐵 + 1 ) ↑ 2 ) ) ) → 𝐵 ∈ ℝ )
11 nn0ge0 ⊢ ( 𝐴 ∈ ℕ0 → 0 ≤ 𝐴 )
12 11 ad2antrr ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ( ( 𝐵 ↑ 2 ) < 𝐴 ∧ 𝐴 < ( ( 𝐵 + 1 ) ↑ 2 ) ) ) → 0 ≤ 𝐴 )
13 5 12 resqrtcld ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ( ( 𝐵 ↑ 2 ) < 𝐴 ∧ 𝐴 < ( ( 𝐵 + 1 ) ↑ 2 ) ) ) → ( √ ‘ 𝐴 ) ∈ ℝ )
14 nn0ge0 ⊢ ( 𝐵 ∈ ℕ0 → 0 ≤ 𝐵 )
15 14 ad2antlr ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ( ( 𝐵 ↑ 2 ) < 𝐴 ∧ 𝐴 < ( ( 𝐵 + 1 ) ↑ 2 ) ) ) → 0 ≤ 𝐵 )
16 5 12 sqrtge0d ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ( ( 𝐵 ↑ 2 ) < 𝐴 ∧ 𝐴 < ( ( 𝐵 + 1 ) ↑ 2 ) ) ) → 0 ≤ ( √ ‘ 𝐴 ) )
17 10 13 15 16 lt2sqd ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ( ( 𝐵 ↑ 2 ) < 𝐴 ∧ 𝐴 < ( ( 𝐵 + 1 ) ↑ 2 ) ) ) → ( 𝐵 < ( √ ‘ 𝐴 ) ↔ ( 𝐵 ↑ 2 ) < ( ( √ ‘ 𝐴 ) ↑ 2 ) ) )
18 8 17 mpbird ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ( ( 𝐵 ↑ 2 ) < 𝐴 ∧ 𝐴 < ( ( 𝐵 + 1 ) ↑ 2 ) ) ) → 𝐵 < ( √ ‘ 𝐴 ) )
19 simprr ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ( ( 𝐵 ↑ 2 ) < 𝐴 ∧ 𝐴 < ( ( 𝐵 + 1 ) ↑ 2 ) ) ) → 𝐴 < ( ( 𝐵 + 1 ) ↑ 2 ) )
20 7 19 eqbrtrd ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ( ( 𝐵 ↑ 2 ) < 𝐴 ∧ 𝐴 < ( ( 𝐵 + 1 ) ↑ 2 ) ) ) → ( ( √ ‘ 𝐴 ) ↑ 2 ) < ( ( 𝐵 + 1 ) ↑ 2 ) )
21 peano2re ⊢ ( 𝐵 ∈ ℝ → ( 𝐵 + 1 ) ∈ ℝ )
22 10 21 syl ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ( ( 𝐵 ↑ 2 ) < 𝐴 ∧ 𝐴 < ( ( 𝐵 + 1 ) ↑ 2 ) ) ) → ( 𝐵 + 1 ) ∈ ℝ )
23 peano2nn0 ⊢ ( 𝐵 ∈ ℕ0 → ( 𝐵 + 1 ) ∈ ℕ0 )
24 nn0ge0 ⊢ ( ( 𝐵 + 1 ) ∈ ℕ0 → 0 ≤ ( 𝐵 + 1 ) )
25 23 24 syl ⊢ ( 𝐵 ∈ ℕ0 → 0 ≤ ( 𝐵 + 1 ) )
26 25 ad2antlr ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ( ( 𝐵 ↑ 2 ) < 𝐴 ∧ 𝐴 < ( ( 𝐵 + 1 ) ↑ 2 ) ) ) → 0 ≤ ( 𝐵 + 1 ) )
27 13 22 16 26 lt2sqd ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ( ( 𝐵 ↑ 2 ) < 𝐴 ∧ 𝐴 < ( ( 𝐵 + 1 ) ↑ 2 ) ) ) → ( ( √ ‘ 𝐴 ) < ( 𝐵 + 1 ) ↔ ( ( √ ‘ 𝐴 ) ↑ 2 ) < ( ( 𝐵 + 1 ) ↑ 2 ) ) )
28 20 27 mpbird ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ( ( 𝐵 ↑ 2 ) < 𝐴 ∧ 𝐴 < ( ( 𝐵 + 1 ) ↑ 2 ) ) ) → ( √ ‘ 𝐴 ) < ( 𝐵 + 1 ) )
29 btwnnz ⊢ ( ( 𝐵 ∈ ℤ ∧ 𝐵 < ( √ ‘ 𝐴 ) ∧ ( √ ‘ 𝐴 ) < ( 𝐵 + 1 ) ) → ¬ ( √ ‘ 𝐴 ) ∈ ℤ )
30 2 18 28 29 syl3anc ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ( ( 𝐵 ↑ 2 ) < 𝐴 ∧ 𝐴 < ( ( 𝐵 + 1 ) ↑ 2 ) ) ) → ¬ ( √ ‘ 𝐴 ) ∈ ℤ )
31 nn0z ⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ℤ )
32 31 ad2antrr ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ( ( 𝐵 ↑ 2 ) < 𝐴 ∧ 𝐴 < ( ( 𝐵 + 1 ) ↑ 2 ) ) ) → 𝐴 ∈ ℤ )
33 zsqrtelqelz ⊢ ( ( 𝐴 ∈ ℤ ∧ ( √ ‘ 𝐴 ) ∈ ℚ ) → ( √ ‘ 𝐴 ) ∈ ℤ )
34 33 ex ⊢ ( 𝐴 ∈ ℤ → ( ( √ ‘ 𝐴 ) ∈ ℚ → ( √ ‘ 𝐴 ) ∈ ℤ ) )
35 32 34 syl ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ( ( 𝐵 ↑ 2 ) < 𝐴 ∧ 𝐴 < ( ( 𝐵 + 1 ) ↑ 2 ) ) ) → ( ( √ ‘ 𝐴 ) ∈ ℚ → ( √ ‘ 𝐴 ) ∈ ℤ ) )
36 30 35 mtod ⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ∧ ( ( 𝐵 ↑ 2 ) < 𝐴 ∧ 𝐴 < ( ( 𝐵 + 1 ) ↑ 2 ) ) ) → ¬ ( √ ‘ 𝐴 ) ∈ ℚ )