Metamath Proof Explorer

Theorem flsqrt

Description: A condition equivalent to the floor of a square root. (Contributed by AV, 17-Aug-2021)

Ref Expression
Assertion flsqrt 
|- ( ( ( A e. RR /\ 0 <_ A ) /\ B e. NN0 ) -> ( ( |_ ` ( sqrt ` A ) ) = B <-> ( ( B ^ 2 ) <_ A /\ A < ( ( B + 1 ) ^ 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 resqrtcl 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( sqrt ` A ) e. RR )
2 nn0z 
 |-  ( B e. NN0 -> B e. ZZ )
3 flbi 
 |-  ( ( ( sqrt ` A ) e. RR /\ B e. ZZ ) -> ( ( |_ ` ( sqrt ` A ) ) = B <-> ( B <_ ( sqrt ` A ) /\ ( sqrt ` A ) < ( B + 1 ) ) ) )
4 1 2 3 syl2an 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ B e. NN0 ) -> ( ( |_ ` ( sqrt ` A ) ) = B <-> ( B <_ ( sqrt ` A ) /\ ( sqrt ` A ) < ( B + 1 ) ) ) )
5 nn0re 
 |-  ( B e. NN0 -> B e. RR )
6 nn0ge0 
 |-  ( B e. NN0 -> 0 <_ B )
7 5 6 jca 
 |-  ( B e. NN0 -> ( B e. RR /\ 0 <_ B ) )
8 sqrtsq 
 |-  ( ( B e. RR /\ 0 <_ B ) -> ( sqrt ` ( B ^ 2 ) ) = B )
9 8 eqcomd 
 |-  ( ( B e. RR /\ 0 <_ B ) -> B = ( sqrt ` ( B ^ 2 ) ) )
10 7 9 syl 
 |-  ( B e. NN0 -> B = ( sqrt ` ( B ^ 2 ) ) )
11 10 breq1d 
 |-  ( B e. NN0 -> ( B <_ ( sqrt ` A ) <-> ( sqrt ` ( B ^ 2 ) ) <_ ( sqrt ` A ) ) )
12 11 adantl 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ B e. NN0 ) -> ( B <_ ( sqrt ` A ) <-> ( sqrt ` ( B ^ 2 ) ) <_ ( sqrt ` A ) ) )
13 nn0sqcl 
 |-  ( B e. NN0 -> ( B ^ 2 ) e. NN0 )
14 13 nn0red 
 |-  ( B e. NN0 -> ( B ^ 2 ) e. RR )
15 5 sqge0d 
 |-  ( B e. NN0 -> 0 <_ ( B ^ 2 ) )
16 14 15 jca 
 |-  ( B e. NN0 -> ( ( B ^ 2 ) e. RR /\ 0 <_ ( B ^ 2 ) ) )
17 16 anim2i 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ B e. NN0 ) -> ( ( A e. RR /\ 0 <_ A ) /\ ( ( B ^ 2 ) e. RR /\ 0 <_ ( B ^ 2 ) ) ) )
18 17 ancomd 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ B e. NN0 ) -> ( ( ( B ^ 2 ) e. RR /\ 0 <_ ( B ^ 2 ) ) /\ ( A e. RR /\ 0 <_ A ) ) )
19 sqrtle 
 |-  ( ( ( ( B ^ 2 ) e. RR /\ 0 <_ ( B ^ 2 ) ) /\ ( A e. RR /\ 0 <_ A ) ) -> ( ( B ^ 2 ) <_ A <-> ( sqrt ` ( B ^ 2 ) ) <_ ( sqrt ` A ) ) )
20 18 19 syl 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ B e. NN0 ) -> ( ( B ^ 2 ) <_ A <-> ( sqrt ` ( B ^ 2 ) ) <_ ( sqrt ` A ) ) )
21 12 20 bitr4d 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ B e. NN0 ) -> ( B <_ ( sqrt ` A ) <-> ( B ^ 2 ) <_ A ) )
22 peano2nn0 
 |-  ( B e. NN0 -> ( B + 1 ) e. NN0 )
23 22 nn0red 
 |-  ( B e. NN0 -> ( B + 1 ) e. RR )
24 1red 
 |-  ( B e. NN0 -> 1 e. RR )
25 0le1 
 |-  0 <_ 1
26 25 a1i 
 |-  ( B e. NN0 -> 0 <_ 1 )
27 5 24 6 26 addge0d 
 |-  ( B e. NN0 -> 0 <_ ( B + 1 ) )
28 23 27 sqrtsqd 
 |-  ( B e. NN0 -> ( sqrt ` ( ( B + 1 ) ^ 2 ) ) = ( B + 1 ) )
29 28 eqcomd 
 |-  ( B e. NN0 -> ( B + 1 ) = ( sqrt ` ( ( B + 1 ) ^ 2 ) ) )
30 29 breq2d 
 |-  ( B e. NN0 -> ( ( sqrt ` A ) < ( B + 1 ) <-> ( sqrt ` A ) < ( sqrt ` ( ( B + 1 ) ^ 2 ) ) ) )
31 30 adantl 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ B e. NN0 ) -> ( ( sqrt ` A ) < ( B + 1 ) <-> ( sqrt ` A ) < ( sqrt ` ( ( B + 1 ) ^ 2 ) ) ) )
32 2nn0 
 |-  2 e. NN0
33 32 a1i 
 |-  ( B e. NN0 -> 2 e. NN0 )
34 22 33 nn0expcld 
 |-  ( B e. NN0 -> ( ( B + 1 ) ^ 2 ) e. NN0 )
35 34 nn0red 
 |-  ( B e. NN0 -> ( ( B + 1 ) ^ 2 ) e. RR )
36 23 sqge0d 
 |-  ( B e. NN0 -> 0 <_ ( ( B + 1 ) ^ 2 ) )
37 35 36 jca 
 |-  ( B e. NN0 -> ( ( ( B + 1 ) ^ 2 ) e. RR /\ 0 <_ ( ( B + 1 ) ^ 2 ) ) )
38 sqrtlt 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( ( ( B + 1 ) ^ 2 ) e. RR /\ 0 <_ ( ( B + 1 ) ^ 2 ) ) ) -> ( A < ( ( B + 1 ) ^ 2 ) <-> ( sqrt ` A ) < ( sqrt ` ( ( B + 1 ) ^ 2 ) ) ) )
39 37 38 sylan2 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ B e. NN0 ) -> ( A < ( ( B + 1 ) ^ 2 ) <-> ( sqrt ` A ) < ( sqrt ` ( ( B + 1 ) ^ 2 ) ) ) )
40 31 39 bitr4d 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ B e. NN0 ) -> ( ( sqrt ` A ) < ( B + 1 ) <-> A < ( ( B + 1 ) ^ 2 ) ) )
41 21 40 anbi12d 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ B e. NN0 ) -> ( ( B <_ ( sqrt ` A ) /\ ( sqrt ` A ) < ( B + 1 ) ) <-> ( ( B ^ 2 ) <_ A /\ A < ( ( B + 1 ) ^ 2 ) ) ) )
42 4 41 bitrd 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ B e. NN0 ) -> ( ( |_ ` ( sqrt ` A ) ) = B <-> ( ( B ^ 2 ) <_ A /\ A < ( ( B + 1 ) ^ 2 ) ) ) )