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 ) )