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