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 \in ℝ \land 0 \leq X) \to ((25 \leq X \land X < 36) \leftrightarrow ⌊\sqrt{X}⌋ = 5)$

Step	Hyp	Ref	Expression
1		5nn0	$⊢ 5 \in ℕ_{0}$
2		flsqrt	$⊢ ((X \in ℝ \land 0 \leq X) \land 5 \in ℕ_{0}) \to (⌊\sqrt{X}⌋ = 5 \leftrightarrow (5^{2} \leq X \land X < {(5 + 1)}^{2}))$
3	1 2	mpan2	$⊢ (X \in ℝ \land 0 \leq X) \to (⌊\sqrt{X}⌋ = 5 \leftrightarrow (5^{2} \leq X \land X < {(5 + 1)}^{2}))$
4		5cn	$⊢ 5 \in ℂ$
5	4	sqvali	$⊢ 5^{2} = 5 \cdot 5$
6		5t5e25	$⊢ 5 \cdot 5 = 25$
7	5 6	eqtri	$⊢ 5^{2} = 25$
8	7	breq1i	$⊢ 5^{2} \leq X \leftrightarrow 25 \leq X$
9	8	a1i	$⊢ (X \in ℝ \land 0 \leq X) \to (5^{2} \leq X \leftrightarrow 25 \leq X)$
10		5p1e6	$⊢ 5 + 1 = 6$
11	10	oveq1i	$⊢ {(5 + 1)}^{2} = 6^{2}$
12		6cn	$⊢ 6 \in ℂ$
13	12	sqvali	$⊢ 6^{2} = 6 \cdot 6$
14		6t6e36	$⊢ 6 \cdot 6 = 36$
15	13 14	eqtri	$⊢ 6^{2} = 36$
16	11 15	eqtri	$⊢ {(5 + 1)}^{2} = 36$
17	16	breq2i	$⊢ X < {(5 + 1)}^{2} \leftrightarrow X < 36$
18	17	a1i	$⊢ (X \in ℝ \land 0 \leq X) \to (X < {(5 + 1)}^{2} \leftrightarrow X < 36)$
19	9 18	anbi12d	$⊢ (X \in ℝ \land 0 \leq X) \to ((5^{2} \leq X \land X < {(5 + 1)}^{2}) \leftrightarrow (25 \leq X \land X < 36))$
20	3 19	bitr2d	$⊢ (X \in ℝ \land 0 \leq X) \to ((25 \leq X \land X < 36) \leftrightarrow ⌊\sqrt{X}⌋ = 5)$

Metamath Proof Explorer