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 ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℕ0 ) → ( ( ⌊ ‘ ( √ ‘ 𝐴 ) ) = 𝐵 ↔ ( ( 𝐵 ↑ 2 ) ≤ 𝐴𝐴 < ( ( 𝐵 + 1 ) ↑ 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 resqrtcl ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( √ ‘ 𝐴 ) ∈ ℝ )
2 nn0z ( 𝐵 ∈ ℕ0𝐵 ∈ ℤ )
3 flbi ( ( ( √ ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℤ ) → ( ( ⌊ ‘ ( √ ‘ 𝐴 ) ) = 𝐵 ↔ ( 𝐵 ≤ ( √ ‘ 𝐴 ) ∧ ( √ ‘ 𝐴 ) < ( 𝐵 + 1 ) ) ) )
4 1 2 3 syl2an ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℕ0 ) → ( ( ⌊ ‘ ( √ ‘ 𝐴 ) ) = 𝐵 ↔ ( 𝐵 ≤ ( √ ‘ 𝐴 ) ∧ ( √ ‘ 𝐴 ) < ( 𝐵 + 1 ) ) ) )
5 nn0re ( 𝐵 ∈ ℕ0𝐵 ∈ ℝ )
6 nn0ge0 ( 𝐵 ∈ ℕ0 → 0 ≤ 𝐵 )
7 5 6 jca ( 𝐵 ∈ ℕ0 → ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) )
8 sqrtsq ( ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) → ( √ ‘ ( 𝐵 ↑ 2 ) ) = 𝐵 )
9 8 eqcomd ( ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) → 𝐵 = ( √ ‘ ( 𝐵 ↑ 2 ) ) )
10 7 9 syl ( 𝐵 ∈ ℕ0𝐵 = ( √ ‘ ( 𝐵 ↑ 2 ) ) )
11 10 breq1d ( 𝐵 ∈ ℕ0 → ( 𝐵 ≤ ( √ ‘ 𝐴 ) ↔ ( √ ‘ ( 𝐵 ↑ 2 ) ) ≤ ( √ ‘ 𝐴 ) ) )
12 11 adantl ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℕ0 ) → ( 𝐵 ≤ ( √ ‘ 𝐴 ) ↔ ( √ ‘ ( 𝐵 ↑ 2 ) ) ≤ ( √ ‘ 𝐴 ) ) )
13 nn0sqcl ( 𝐵 ∈ ℕ0 → ( 𝐵 ↑ 2 ) ∈ ℕ0 )
14 13 nn0red ( 𝐵 ∈ ℕ0 → ( 𝐵 ↑ 2 ) ∈ ℝ )
15 5 sqge0d ( 𝐵 ∈ ℕ0 → 0 ≤ ( 𝐵 ↑ 2 ) )
16 14 15 jca ( 𝐵 ∈ ℕ0 → ( ( 𝐵 ↑ 2 ) ∈ ℝ ∧ 0 ≤ ( 𝐵 ↑ 2 ) ) )
17 16 anim2i ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℕ0 ) → ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( ( 𝐵 ↑ 2 ) ∈ ℝ ∧ 0 ≤ ( 𝐵 ↑ 2 ) ) ) )
18 17 ancomd ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℕ0 ) → ( ( ( 𝐵 ↑ 2 ) ∈ ℝ ∧ 0 ≤ ( 𝐵 ↑ 2 ) ) ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ) )
19 sqrtle ( ( ( ( 𝐵 ↑ 2 ) ∈ ℝ ∧ 0 ≤ ( 𝐵 ↑ 2 ) ) ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ) → ( ( 𝐵 ↑ 2 ) ≤ 𝐴 ↔ ( √ ‘ ( 𝐵 ↑ 2 ) ) ≤ ( √ ‘ 𝐴 ) ) )
20 18 19 syl ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℕ0 ) → ( ( 𝐵 ↑ 2 ) ≤ 𝐴 ↔ ( √ ‘ ( 𝐵 ↑ 2 ) ) ≤ ( √ ‘ 𝐴 ) ) )
21 12 20 bitr4d ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℕ0 ) → ( 𝐵 ≤ ( √ ‘ 𝐴 ) ↔ ( 𝐵 ↑ 2 ) ≤ 𝐴 ) )
22 peano2nn0 ( 𝐵 ∈ ℕ0 → ( 𝐵 + 1 ) ∈ ℕ0 )
23 22 nn0red ( 𝐵 ∈ ℕ0 → ( 𝐵 + 1 ) ∈ ℝ )
24 1red ( 𝐵 ∈ ℕ0 → 1 ∈ ℝ )
25 0le1 0 ≤ 1
26 25 a1i ( 𝐵 ∈ ℕ0 → 0 ≤ 1 )
27 5 24 6 26 addge0d ( 𝐵 ∈ ℕ0 → 0 ≤ ( 𝐵 + 1 ) )
28 23 27 sqrtsqd ( 𝐵 ∈ ℕ0 → ( √ ‘ ( ( 𝐵 + 1 ) ↑ 2 ) ) = ( 𝐵 + 1 ) )
29 28 eqcomd ( 𝐵 ∈ ℕ0 → ( 𝐵 + 1 ) = ( √ ‘ ( ( 𝐵 + 1 ) ↑ 2 ) ) )
30 29 breq2d ( 𝐵 ∈ ℕ0 → ( ( √ ‘ 𝐴 ) < ( 𝐵 + 1 ) ↔ ( √ ‘ 𝐴 ) < ( √ ‘ ( ( 𝐵 + 1 ) ↑ 2 ) ) ) )
31 30 adantl ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℕ0 ) → ( ( √ ‘ 𝐴 ) < ( 𝐵 + 1 ) ↔ ( √ ‘ 𝐴 ) < ( √ ‘ ( ( 𝐵 + 1 ) ↑ 2 ) ) ) )
32 2nn0 2 ∈ ℕ0
33 32 a1i ( 𝐵 ∈ ℕ0 → 2 ∈ ℕ0 )
34 22 33 nn0expcld ( 𝐵 ∈ ℕ0 → ( ( 𝐵 + 1 ) ↑ 2 ) ∈ ℕ0 )
35 34 nn0red ( 𝐵 ∈ ℕ0 → ( ( 𝐵 + 1 ) ↑ 2 ) ∈ ℝ )
36 23 sqge0d ( 𝐵 ∈ ℕ0 → 0 ≤ ( ( 𝐵 + 1 ) ↑ 2 ) )
37 35 36 jca ( 𝐵 ∈ ℕ0 → ( ( ( 𝐵 + 1 ) ↑ 2 ) ∈ ℝ ∧ 0 ≤ ( ( 𝐵 + 1 ) ↑ 2 ) ) )
38 sqrtlt ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( ( ( 𝐵 + 1 ) ↑ 2 ) ∈ ℝ ∧ 0 ≤ ( ( 𝐵 + 1 ) ↑ 2 ) ) ) → ( 𝐴 < ( ( 𝐵 + 1 ) ↑ 2 ) ↔ ( √ ‘ 𝐴 ) < ( √ ‘ ( ( 𝐵 + 1 ) ↑ 2 ) ) ) )
39 37 38 sylan2 ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℕ0 ) → ( 𝐴 < ( ( 𝐵 + 1 ) ↑ 2 ) ↔ ( √ ‘ 𝐴 ) < ( √ ‘ ( ( 𝐵 + 1 ) ↑ 2 ) ) ) )
40 31 39 bitr4d ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℕ0 ) → ( ( √ ‘ 𝐴 ) < ( 𝐵 + 1 ) ↔ 𝐴 < ( ( 𝐵 + 1 ) ↑ 2 ) ) )
41 21 40 anbi12d ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℕ0 ) → ( ( 𝐵 ≤ ( √ ‘ 𝐴 ) ∧ ( √ ‘ 𝐴 ) < ( 𝐵 + 1 ) ) ↔ ( ( 𝐵 ↑ 2 ) ≤ 𝐴𝐴 < ( ( 𝐵 + 1 ) ↑ 2 ) ) ) )
42 4 41 bitrd ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℕ0 ) → ( ( ⌊ ‘ ( √ ‘ 𝐴 ) ) = 𝐵 ↔ ( ( 𝐵 ↑ 2 ) ≤ 𝐴𝐴 < ( ( 𝐵 + 1 ) ↑ 2 ) ) ) )