Proof of Theorem flsqrt
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | resqrtcl 15293 | . . 3
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) →
(√‘𝐴) ∈
ℝ) | 
| 2 |  | nn0z 12640 | . . 3
⊢ (𝐵 ∈ ℕ0
→ 𝐵 ∈
ℤ) | 
| 3 |  | flbi 13857 | . . 3
⊢
(((√‘𝐴)
∈ ℝ ∧ 𝐵
∈ ℤ) → ((⌊‘(√‘𝐴)) = 𝐵 ↔ (𝐵 ≤ (√‘𝐴) ∧ (√‘𝐴) < (𝐵 + 1)))) | 
| 4 | 1, 2, 3 | syl2an 596 | . 2
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝐵 ∈ ℕ0) →
((⌊‘(√‘𝐴)) = 𝐵 ↔ (𝐵 ≤ (√‘𝐴) ∧ (√‘𝐴) < (𝐵 + 1)))) | 
| 5 |  | nn0re 12537 | . . . . . . . 8
⊢ (𝐵 ∈ ℕ0
→ 𝐵 ∈
ℝ) | 
| 6 |  | nn0ge0 12553 | . . . . . . . 8
⊢ (𝐵 ∈ ℕ0
→ 0 ≤ 𝐵) | 
| 7 | 5, 6 | jca 511 | . . . . . . 7
⊢ (𝐵 ∈ ℕ0
→ (𝐵 ∈ ℝ
∧ 0 ≤ 𝐵)) | 
| 8 |  | sqrtsq 15309 | . . . . . . . 8
⊢ ((𝐵 ∈ ℝ ∧ 0 ≤
𝐵) →
(√‘(𝐵↑2))
= 𝐵) | 
| 9 | 8 | eqcomd 2742 | . . . . . . 7
⊢ ((𝐵 ∈ ℝ ∧ 0 ≤
𝐵) → 𝐵 = (√‘(𝐵↑2))) | 
| 10 | 7, 9 | syl 17 | . . . . . 6
⊢ (𝐵 ∈ ℕ0
→ 𝐵 =
(√‘(𝐵↑2))) | 
| 11 | 10 | breq1d 5152 | . . . . 5
⊢ (𝐵 ∈ ℕ0
→ (𝐵 ≤
(√‘𝐴) ↔
(√‘(𝐵↑2))
≤ (√‘𝐴))) | 
| 12 | 11 | adantl 481 | . . . 4
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝐵 ∈ ℕ0) → (𝐵 ≤ (√‘𝐴) ↔ (√‘(𝐵↑2)) ≤
(√‘𝐴))) | 
| 13 |  | nn0sqcl 14131 | . . . . . . . . 9
⊢ (𝐵 ∈ ℕ0
→ (𝐵↑2) ∈
ℕ0) | 
| 14 | 13 | nn0red 12590 | . . . . . . . 8
⊢ (𝐵 ∈ ℕ0
→ (𝐵↑2) ∈
ℝ) | 
| 15 | 5 | sqge0d 14178 | . . . . . . . 8
⊢ (𝐵 ∈ ℕ0
→ 0 ≤ (𝐵↑2)) | 
| 16 | 14, 15 | jca 511 | . . . . . . 7
⊢ (𝐵 ∈ ℕ0
→ ((𝐵↑2) ∈
ℝ ∧ 0 ≤ (𝐵↑2))) | 
| 17 | 16 | anim2i 617 | . . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝐵 ∈ ℕ0) → ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ ((𝐵↑2) ∈ ℝ ∧ 0
≤ (𝐵↑2)))) | 
| 18 | 17 | ancomd 461 | . . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝐵 ∈ ℕ0) → (((𝐵↑2) ∈ ℝ ∧ 0
≤ (𝐵↑2)) ∧
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴))) | 
| 19 |  | sqrtle 15300 | . . . . 5
⊢ ((((𝐵↑2) ∈ ℝ ∧ 0
≤ (𝐵↑2)) ∧
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) → ((𝐵↑2) ≤ 𝐴 ↔ (√‘(𝐵↑2)) ≤ (√‘𝐴))) | 
| 20 | 18, 19 | syl 17 | . . . 4
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝐵 ∈ ℕ0) → ((𝐵↑2) ≤ 𝐴 ↔ (√‘(𝐵↑2)) ≤ (√‘𝐴))) | 
| 21 | 12, 20 | bitr4d 282 | . . 3
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝐵 ∈ ℕ0) → (𝐵 ≤ (√‘𝐴) ↔ (𝐵↑2) ≤ 𝐴)) | 
| 22 |  | peano2nn0 12568 | . . . . . . . . 9
⊢ (𝐵 ∈ ℕ0
→ (𝐵 + 1) ∈
ℕ0) | 
| 23 | 22 | nn0red 12590 | . . . . . . . 8
⊢ (𝐵 ∈ ℕ0
→ (𝐵 + 1) ∈
ℝ) | 
| 24 |  | 1red 11263 | . . . . . . . . 9
⊢ (𝐵 ∈ ℕ0
→ 1 ∈ ℝ) | 
| 25 |  | 0le1 11787 | . . . . . . . . . 10
⊢ 0 ≤
1 | 
| 26 | 25 | a1i 11 | . . . . . . . . 9
⊢ (𝐵 ∈ ℕ0
→ 0 ≤ 1) | 
| 27 | 5, 24, 6, 26 | addge0d 11840 | . . . . . . . 8
⊢ (𝐵 ∈ ℕ0
→ 0 ≤ (𝐵 +
1)) | 
| 28 | 23, 27 | sqrtsqd 15459 | . . . . . . 7
⊢ (𝐵 ∈ ℕ0
→ (√‘((𝐵 +
1)↑2)) = (𝐵 +
1)) | 
| 29 | 28 | eqcomd 2742 | . . . . . 6
⊢ (𝐵 ∈ ℕ0
→ (𝐵 + 1) =
(√‘((𝐵 +
1)↑2))) | 
| 30 | 29 | breq2d 5154 | . . . . 5
⊢ (𝐵 ∈ ℕ0
→ ((√‘𝐴)
< (𝐵 + 1) ↔
(√‘𝐴) <
(√‘((𝐵 +
1)↑2)))) | 
| 31 | 30 | adantl 481 | . . . 4
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝐵 ∈ ℕ0) →
((√‘𝐴) <
(𝐵 + 1) ↔
(√‘𝐴) <
(√‘((𝐵 +
1)↑2)))) | 
| 32 |  | 2nn0 12545 | . . . . . . . . 9
⊢ 2 ∈
ℕ0 | 
| 33 | 32 | a1i 11 | . . . . . . . 8
⊢ (𝐵 ∈ ℕ0
→ 2 ∈ ℕ0) | 
| 34 | 22, 33 | nn0expcld 14286 | . . . . . . 7
⊢ (𝐵 ∈ ℕ0
→ ((𝐵 + 1)↑2)
∈ ℕ0) | 
| 35 | 34 | nn0red 12590 | . . . . . 6
⊢ (𝐵 ∈ ℕ0
→ ((𝐵 + 1)↑2)
∈ ℝ) | 
| 36 | 23 | sqge0d 14178 | . . . . . 6
⊢ (𝐵 ∈ ℕ0
→ 0 ≤ ((𝐵 +
1)↑2)) | 
| 37 | 35, 36 | jca 511 | . . . . 5
⊢ (𝐵 ∈ ℕ0
→ (((𝐵 + 1)↑2)
∈ ℝ ∧ 0 ≤ ((𝐵 + 1)↑2))) | 
| 38 |  | sqrtlt 15301 | . . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (((𝐵 + 1)↑2) ∈ ℝ
∧ 0 ≤ ((𝐵 +
1)↑2))) → (𝐴 <
((𝐵 + 1)↑2) ↔
(√‘𝐴) <
(√‘((𝐵 +
1)↑2)))) | 
| 39 | 37, 38 | sylan2 593 | . . . 4
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝐵 ∈ ℕ0) → (𝐴 < ((𝐵 + 1)↑2) ↔ (√‘𝐴) < (√‘((𝐵 +
1)↑2)))) | 
| 40 | 31, 39 | bitr4d 282 | . . 3
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝐵 ∈ ℕ0) →
((√‘𝐴) <
(𝐵 + 1) ↔ 𝐴 < ((𝐵 + 1)↑2))) | 
| 41 | 21, 40 | anbi12d 632 | . 2
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝐵 ∈ ℕ0) → ((𝐵 ≤ (√‘𝐴) ∧ (√‘𝐴) < (𝐵 + 1)) ↔ ((𝐵↑2) ≤ 𝐴 ∧ 𝐴 < ((𝐵 + 1)↑2)))) | 
| 42 | 4, 41 | bitrd 279 | 1
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝐵 ∈ ℕ0) →
((⌊‘(√‘𝐴)) = 𝐵 ↔ ((𝐵↑2) ≤ 𝐴 ∧ 𝐴 < ((𝐵 + 1)↑2)))) |