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 ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ) → ( ( 2 5 ≤ 𝑋𝑋 < 3 6 ) ↔ ( ⌊ ‘ ( √ ‘ 𝑋 ) ) = 5 ) )

Proof

Step Hyp Ref Expression
1 5nn0 5 ∈ ℕ0
2 flsqrt ( ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ) ∧ 5 ∈ ℕ0 ) → ( ( ⌊ ‘ ( √ ‘ 𝑋 ) ) = 5 ↔ ( ( 5 ↑ 2 ) ≤ 𝑋𝑋 < ( ( 5 + 1 ) ↑ 2 ) ) ) )
3 1 2 mpan2 ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ) → ( ( ⌊ ‘ ( √ ‘ 𝑋 ) ) = 5 ↔ ( ( 5 ↑ 2 ) ≤ 𝑋𝑋 < ( ( 5 + 1 ) ↑ 2 ) ) ) )
4 5cn 5 ∈ ℂ
5 4 sqvali ( 5 ↑ 2 ) = ( 5 · 5 )
6 5t5e25 ( 5 · 5 ) = 2 5
7 5 6 eqtri ( 5 ↑ 2 ) = 2 5
8 7 breq1i ( ( 5 ↑ 2 ) ≤ 𝑋 2 5 ≤ 𝑋 )
9 8 a1i ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ) → ( ( 5 ↑ 2 ) ≤ 𝑋 2 5 ≤ 𝑋 ) )
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 ) = 3 6
15 13 14 eqtri ( 6 ↑ 2 ) = 3 6
16 11 15 eqtri ( ( 5 + 1 ) ↑ 2 ) = 3 6
17 16 breq2i ( 𝑋 < ( ( 5 + 1 ) ↑ 2 ) ↔ 𝑋 < 3 6 )
18 17 a1i ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ) → ( 𝑋 < ( ( 5 + 1 ) ↑ 2 ) ↔ 𝑋 < 3 6 ) )
19 9 18 anbi12d ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ) → ( ( ( 5 ↑ 2 ) ≤ 𝑋𝑋 < ( ( 5 + 1 ) ↑ 2 ) ) ↔ ( 2 5 ≤ 𝑋𝑋 < 3 6 ) ) )
20 3 19 bitr2d ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ) → ( ( 2 5 ≤ 𝑋𝑋 < 3 6 ) ↔ ( ⌊ ‘ ( √ ‘ 𝑋 ) ) = 5 ) )