flsqrt

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

		Ref	Expression
	Assertion	flsqrt	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℕ_{0}) \to (⌊\sqrt{A}⌋ = B \leftrightarrow (B^{2} \leq A \land A < {(B + 1)}^{2}))$

Proof

Step	Hyp	Ref	Expression
1		resqrtcl	$⊢ (A \in ℝ \land 0 \leq A) \to \sqrt{A} \in ℝ$
2		nn0z	$⊢ B \in ℕ_{0} \to B \in ℤ$
3		flbi	$⊢ (\sqrt{A} \in ℝ \land B \in ℤ) \to (⌊\sqrt{A}⌋ = B \leftrightarrow (B \leq \sqrt{A} \land \sqrt{A} < B + 1))$
4	1 2 3	syl2an	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℕ_{0}) \to (⌊\sqrt{A}⌋ = B \leftrightarrow (B \leq \sqrt{A} \land \sqrt{A} < B + 1))$
5		nn0re	$⊢ B \in ℕ_{0} \to B \in ℝ$
6		nn0ge0	$⊢ B \in ℕ_{0} \to 0 \leq B$
7	5 6	jca	$⊢ B \in ℕ_{0} \to (B \in ℝ \land 0 \leq B)$
8		sqrtsq	$⊢ (B \in ℝ \land 0 \leq B) \to \sqrt{B^{2}} = B$
9	8	eqcomd	$⊢ (B \in ℝ \land 0 \leq B) \to B = \sqrt{B^{2}}$
10	7 9	syl	$⊢ B \in ℕ_{0} \to B = \sqrt{B^{2}}$
11	10	breq1d	$⊢ B \in ℕ_{0} \to (B \leq \sqrt{A} \leftrightarrow \sqrt{B^{2}} \leq \sqrt{A})$
12	11	adantl	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℕ_{0}) \to (B \leq \sqrt{A} \leftrightarrow \sqrt{B^{2}} \leq \sqrt{A})$
13		nn0sqcl	$⊢ B \in ℕ_{0} \to B^{2} \in ℕ_{0}$
14	13	nn0red	$⊢ B \in ℕ_{0} \to B^{2} \in ℝ$
15	5	sqge0d	$⊢ B \in ℕ_{0} \to 0 \leq B^{2}$
16	14 15	jca	$⊢ B \in ℕ_{0} \to (B^{2} \in ℝ \land 0 \leq B^{2})$
17	16	anim2i	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℕ_{0}) \to ((A \in ℝ \land 0 \leq A) \land (B^{2} \in ℝ \land 0 \leq B^{2}))$
18	17	ancomd	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℕ_{0}) \to ((B^{2} \in ℝ \land 0 \leq B^{2}) \land (A \in ℝ \land 0 \leq A))$
19		sqrtle	$⊢ ((B^{2} \in ℝ \land 0 \leq B^{2}) \land (A \in ℝ \land 0 \leq A)) \to (B^{2} \leq A \leftrightarrow \sqrt{B^{2}} \leq \sqrt{A})$
20	18 19	syl	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℕ_{0}) \to (B^{2} \leq A \leftrightarrow \sqrt{B^{2}} \leq \sqrt{A})$
21	12 20	bitr4d	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℕ_{0}) \to (B \leq \sqrt{A} \leftrightarrow B^{2} \leq A)$
22		peano2nn0	$⊢ B \in ℕ_{0} \to B + 1 \in ℕ_{0}$
23	22	nn0red	$⊢ B \in ℕ_{0} \to B + 1 \in ℝ$
24		1red	$⊢ B \in ℕ_{0} \to 1 \in ℝ$
25		0le1	$⊢ 0 \leq 1$
26	25	a1i	$⊢ B \in ℕ_{0} \to 0 \leq 1$
27	5 24 6 26	addge0d	$⊢ B \in ℕ_{0} \to 0 \leq B + 1$
28	23 27	sqrtsqd	$⊢ B \in ℕ_{0} \to \sqrt{{(B + 1)}^{2}} = B + 1$
29	28	eqcomd	$⊢ B \in ℕ_{0} \to B + 1 = \sqrt{{(B + 1)}^{2}}$
30	29	breq2d	$⊢ B \in ℕ_{0} \to (\sqrt{A} < B + 1 \leftrightarrow \sqrt{A} < \sqrt{{(B + 1)}^{2}})$
31	30	adantl	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℕ_{0}) \to (\sqrt{A} < B + 1 \leftrightarrow \sqrt{A} < \sqrt{{(B + 1)}^{2}})$
32		2nn0	$⊢ 2 \in ℕ_{0}$
33	32	a1i	$⊢ B \in ℕ_{0} \to 2 \in ℕ_{0}$
34	22 33	nn0expcld	$⊢ B \in ℕ_{0} \to {(B + 1)}^{2} \in ℕ_{0}$
35	34	nn0red	$⊢ B \in ℕ_{0} \to {(B + 1)}^{2} \in ℝ$
36	23	sqge0d	$⊢ B \in ℕ_{0} \to 0 \leq {(B + 1)}^{2}$
37	35 36	jca	$⊢ B \in ℕ_{0} \to ({(B + 1)}^{2} \in ℝ \land 0 \leq {(B + 1)}^{2})$
38		sqrtlt	$⊢ ((A \in ℝ \land 0 \leq A) \land ({(B + 1)}^{2} \in ℝ \land 0 \leq {(B + 1)}^{2})) \to (A < {(B + 1)}^{2} \leftrightarrow \sqrt{A} < \sqrt{{(B + 1)}^{2}})$
39	37 38	sylan2	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℕ_{0}) \to (A < {(B + 1)}^{2} \leftrightarrow \sqrt{A} < \sqrt{{(B + 1)}^{2}})$
40	31 39	bitr4d	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℕ_{0}) \to (\sqrt{A} < B + 1 \leftrightarrow A < {(B + 1)}^{2})$
41	21 40	anbi12d	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℕ_{0}) \to ((B \leq \sqrt{A} \land \sqrt{A} < B + 1) \leftrightarrow (B^{2} \leq A \land A < {(B + 1)}^{2}))$
42	4 41	bitrd	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℕ_{0}) \to (⌊\sqrt{A}⌋ = B \leftrightarrow (B^{2} \leq A \land A < {(B + 1)}^{2}))$

Metamath Proof Explorer

Theorem flsqrt

Proof