Metamath Proof Explorer

Theorem flsqrt5

Description: The floor of the square root of a nonnegative number is 5 iff the number is between 25 and 35. (Contributed by AV, 17-Aug-2021)

Ref Expression
Assertion flsqrt5 ⊢ X ∈ ℝ ∧ 0 ≤ X → 25 ≤ X ∧ X < 36 ↔ X = 5

Proof

Step Hyp Ref Expression
1 5nn0 ⊢ 5 ∈ ℕ 0
2 flsqrt ⊢ X ∈ ℝ ∧ 0 ≤ X ∧ 5 ∈ ℕ 0 → X = 5 ↔ 5 2 ≤ X ∧ X < 5 + 1 2
3 1 2 mpan2 ⊢ X ∈ ℝ ∧ 0 ≤ X → X = 5 ↔ 5 2 ≤ X ∧ X < 5 + 1 2
4 5cn ⊢ 5 ∈ ℂ
5 4 sqvali ⊢ 5 2 = 5 ⋅ 5
6 5t5e25 ⊢ 5 ⋅ 5 = 25
7 5 6 eqtri ⊢ 5 2 = 25
8 7 breq1i ⊢ 5 2 ≤ X ↔ 25 ≤ X
9 8 a1i ⊢ X ∈ ℝ ∧ 0 ≤ X → 5 2 ≤ X ↔ 25 ≤ X
10 5p1e6 ⊢ 5 + 1 = 6
11 10 oveq1i ⊢ 5 + 1 2 = 6 2
12 6cn ⊢ 6 ∈ ℂ
13 12 sqvali ⊢ 6 2 = 6 ⋅ 6
14 6t6e36 ⊢ 6 ⋅ 6 = 36
15 13 14 eqtri ⊢ 6 2 = 36
16 11 15 eqtri ⊢ 5 + 1 2 = 36
17 16 breq2i ⊢ X < 5 + 1 2 ↔ X < 36
18 17 a1i ⊢ X ∈ ℝ ∧ 0 ≤ X → X < 5 + 1 2 ↔ X < 36
19 9 18 anbi12d ⊢ X ∈ ℝ ∧ 0 ≤ X → 5 2 ≤ X ∧ X < 5 + 1 2 ↔ 25 ≤ X ∧ X < 36
20 3 19 bitr2d ⊢ X ∈ ℝ ∧ 0 ≤ X → 25 ≤ X ∧ X < 36 ↔ X = 5