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 e. RR /\ 0 <_ X ) -> ( ( ; 2 5 <_ X /\ X < ; 3 6 ) <-> ( |_ ` ( sqrt ` X ) ) = 5 ) )

Proof

Step	Hyp	Ref	Expression
1		5nn0	|- 5 e. NN0
2		flsqrt	|- ( ( ( X e. RR /\ 0 <_ X ) /\ 5 e. NN0 ) -> ( ( |_ ` ( sqrt ` X ) ) = 5 <-> ( ( 5 ^ 2 ) <_ X /\ X < ( ( 5 + 1 ) ^ 2 ) ) ) )
3	1 2	mpan2	|- ( ( X e. RR /\ 0 <_ X ) -> ( ( |_ ` ( sqrt ` X ) ) = 5 <-> ( ( 5 ^ 2 ) <_ X /\ X < ( ( 5 + 1 ) ^ 2 ) ) ) )
4		5cn	|- 5 e. CC
5	4	sqvali	|- ( 5 ^ 2 ) = ( 5 x. 5 )
6		5t5e25	|- ( 5 x. 5 ) = ; 2 5
7	5 6	eqtri	|- ( 5 ^ 2 ) = ; 2 5
8	7	breq1i	|- ( ( 5 ^ 2 ) <_ X <-> ; 2 5 <_ X )
9	8	a1i	|- ( ( X e. RR /\ 0 <_ X ) -> ( ( 5 ^ 2 ) <_ X <-> ; 2 5 <_ X ) )
10		5p1e6	|- ( 5 + 1 ) = 6
11	10	oveq1i	|- ( ( 5 + 1 ) ^ 2 ) = ( 6 ^ 2 )
12		6cn	|- 6 e. CC
13	12	sqvali	|- ( 6 ^ 2 ) = ( 6 x. 6 )
14		6t6e36	|- ( 6 x. 6 ) = ; 3 6
15	13 14	eqtri	|- ( 6 ^ 2 ) = ; 3 6
16	11 15	eqtri	|- ( ( 5 + 1 ) ^ 2 ) = ; 3 6
17	16	breq2i	|- ( X < ( ( 5 + 1 ) ^ 2 ) <-> X < ; 3 6 )
18	17	a1i	|- ( ( X e. RR /\ 0 <_ X ) -> ( X < ( ( 5 + 1 ) ^ 2 ) <-> X < ; 3 6 ) )
19	9 18	anbi12d	|- ( ( X e. RR /\ 0 <_ X ) -> ( ( ( 5 ^ 2 ) <_ X /\ X < ( ( 5 + 1 ) ^ 2 ) ) <-> ( ; 2 5 <_ X /\ X < ; 3 6 ) ) )
20	3 19	bitr2d	|- ( ( X e. RR /\ 0 <_ X ) -> ( ( ; 2 5 <_ X /\ X < ; 3 6 ) <-> ( |_ ` ( sqrt ` X ) ) = 5 ) )