Proof of Theorem cnre2csqlem
| Step | Hyp | Ref
| Expression |
| 1 | | cnre2csqlem.3 |
. . . . . . 7
⊢ 𝐺 Fn V |
| 2 | | ssv 4008 |
. . . . . . 7
⊢ (ℝ
× ℝ) ⊆ V |
| 3 | | fnssres 6691 |
. . . . . . 7
⊢ ((𝐺 Fn V ∧ (ℝ ×
ℝ) ⊆ V) → (𝐺 ↾ (ℝ × ℝ)) Fn
(ℝ × ℝ)) |
| 4 | 1, 2, 3 | mp2an 692 |
. . . . . 6
⊢ (𝐺 ↾ (ℝ ×
ℝ)) Fn (ℝ × ℝ) |
| 5 | | elpreima 7078 |
. . . . . 6
⊢ ((𝐺 ↾ (ℝ ×
ℝ)) Fn (ℝ × ℝ) → (𝑌 ∈ (◡(𝐺 ↾ (ℝ × ℝ)) “
(((𝐺‘𝑋) − 𝐷)(,)((𝐺‘𝑋) + 𝐷))) ↔ (𝑌 ∈ (ℝ × ℝ) ∧
((𝐺 ↾ (ℝ
× ℝ))‘𝑌)
∈ (((𝐺‘𝑋) − 𝐷)(,)((𝐺‘𝑋) + 𝐷))))) |
| 6 | 4, 5 | mp1i 13 |
. . . . 5
⊢ ((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝑌 ∈
(ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) → (𝑌 ∈ (◡(𝐺 ↾ (ℝ × ℝ)) “
(((𝐺‘𝑋) − 𝐷)(,)((𝐺‘𝑋) + 𝐷))) ↔ (𝑌 ∈ (ℝ × ℝ) ∧
((𝐺 ↾ (ℝ
× ℝ))‘𝑌)
∈ (((𝐺‘𝑋) − 𝐷)(,)((𝐺‘𝑋) + 𝐷))))) |
| 7 | 6 | simplbda 499 |
. . . 4
⊢ (((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝑌 ∈
(ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) ∧ 𝑌 ∈ (◡(𝐺 ↾ (ℝ × ℝ)) “
(((𝐺‘𝑋) − 𝐷)(,)((𝐺‘𝑋) + 𝐷)))) → ((𝐺 ↾ (ℝ ×
ℝ))‘𝑌) ∈
(((𝐺‘𝑋) − 𝐷)(,)((𝐺‘𝑋) + 𝐷))) |
| 8 | 7 | ex 412 |
. . 3
⊢ ((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝑌 ∈
(ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) → (𝑌 ∈ (◡(𝐺 ↾ (ℝ × ℝ)) “
(((𝐺‘𝑋) − 𝐷)(,)((𝐺‘𝑋) + 𝐷))) → ((𝐺 ↾ (ℝ ×
ℝ))‘𝑌) ∈
(((𝐺‘𝑋) − 𝐷)(,)((𝐺‘𝑋) + 𝐷)))) |
| 9 | | simp2 1138 |
. . . . . 6
⊢ ((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝑌 ∈
(ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) → 𝑌 ∈ (ℝ ×
ℝ)) |
| 10 | | fvres 6925 |
. . . . . 6
⊢ (𝑌 ∈ (ℝ ×
ℝ) → ((𝐺 ↾
(ℝ × ℝ))‘𝑌) = (𝐺‘𝑌)) |
| 11 | 9, 10 | syl 17 |
. . . . 5
⊢ ((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝑌 ∈
(ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) → ((𝐺 ↾ (ℝ ×
ℝ))‘𝑌) = (𝐺‘𝑌)) |
| 12 | 11 | eleq1d 2826 |
. . . 4
⊢ ((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝑌 ∈
(ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) → (((𝐺 ↾ (ℝ ×
ℝ))‘𝑌) ∈
(((𝐺‘𝑋) − 𝐷)(,)((𝐺‘𝑋) + 𝐷)) ↔ (𝐺‘𝑌) ∈ (((𝐺‘𝑋) − 𝐷)(,)((𝐺‘𝑋) + 𝐷)))) |
| 13 | | simp1 1137 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝑌 ∈
(ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) → 𝑋 ∈ (ℝ ×
ℝ)) |
| 14 | | fveq2 6906 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑋 → (𝐺‘𝑥) = (𝐺‘𝑋)) |
| 15 | 14 | eleq1d 2826 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑋 → ((𝐺‘𝑥) ∈ ℝ ↔ (𝐺‘𝑋) ∈ ℝ)) |
| 16 | | cnre2csqlem.4 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (ℝ ×
ℝ) → (𝐺‘𝑥) ∈ ℝ) |
| 17 | 15, 16 | vtoclga 3577 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ (ℝ ×
ℝ) → (𝐺‘𝑋) ∈ ℝ) |
| 18 | 13, 17 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝑌 ∈
(ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) → (𝐺‘𝑋) ∈ ℝ) |
| 19 | | simp3 1139 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝑌 ∈
(ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) → 𝐷 ∈
ℝ+) |
| 20 | 19 | rpred 13077 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝑌 ∈
(ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) → 𝐷 ∈
ℝ) |
| 21 | 18, 20 | resubcld 11691 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝑌 ∈
(ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) → ((𝐺‘𝑋) − 𝐷) ∈ ℝ) |
| 22 | 21 | rexrd 11311 |
. . . . . . . . 9
⊢ ((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝑌 ∈
(ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) → ((𝐺‘𝑋) − 𝐷) ∈
ℝ*) |
| 23 | 18, 20 | readdcld 11290 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝑌 ∈
(ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) → ((𝐺‘𝑋) + 𝐷) ∈ ℝ) |
| 24 | 23 | rexrd 11311 |
. . . . . . . . 9
⊢ ((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝑌 ∈
(ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) → ((𝐺‘𝑋) + 𝐷) ∈
ℝ*) |
| 25 | | elioo2 13428 |
. . . . . . . . 9
⊢ ((((𝐺‘𝑋) − 𝐷) ∈ ℝ* ∧ ((𝐺‘𝑋) + 𝐷) ∈ ℝ*) → ((𝐺‘𝑌) ∈ (((𝐺‘𝑋) − 𝐷)(,)((𝐺‘𝑋) + 𝐷)) ↔ ((𝐺‘𝑌) ∈ ℝ ∧ ((𝐺‘𝑋) − 𝐷) < (𝐺‘𝑌) ∧ (𝐺‘𝑌) < ((𝐺‘𝑋) + 𝐷)))) |
| 26 | 22, 24, 25 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝑌 ∈
(ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) → ((𝐺‘𝑌) ∈ (((𝐺‘𝑋) − 𝐷)(,)((𝐺‘𝑋) + 𝐷)) ↔ ((𝐺‘𝑌) ∈ ℝ ∧ ((𝐺‘𝑋) − 𝐷) < (𝐺‘𝑌) ∧ (𝐺‘𝑌) < ((𝐺‘𝑋) + 𝐷)))) |
| 27 | 26 | biimpa 476 |
. . . . . . 7
⊢ (((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝑌 ∈
(ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) ∧ (𝐺‘𝑌) ∈ (((𝐺‘𝑋) − 𝐷)(,)((𝐺‘𝑋) + 𝐷))) → ((𝐺‘𝑌) ∈ ℝ ∧ ((𝐺‘𝑋) − 𝐷) < (𝐺‘𝑌) ∧ (𝐺‘𝑌) < ((𝐺‘𝑋) + 𝐷))) |
| 28 | 27 | simp2d 1144 |
. . . . . 6
⊢ (((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝑌 ∈
(ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) ∧ (𝐺‘𝑌) ∈ (((𝐺‘𝑋) − 𝐷)(,)((𝐺‘𝑋) + 𝐷))) → ((𝐺‘𝑋) − 𝐷) < (𝐺‘𝑌)) |
| 29 | 27 | simp3d 1145 |
. . . . . 6
⊢ (((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝑌 ∈
(ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) ∧ (𝐺‘𝑌) ∈ (((𝐺‘𝑋) − 𝐷)(,)((𝐺‘𝑋) + 𝐷))) → (𝐺‘𝑌) < ((𝐺‘𝑋) + 𝐷)) |
| 30 | 28, 29 | jca 511 |
. . . . 5
⊢ (((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝑌 ∈
(ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) ∧ (𝐺‘𝑌) ∈ (((𝐺‘𝑋) − 𝐷)(,)((𝐺‘𝑋) + 𝐷))) → (((𝐺‘𝑋) − 𝐷) < (𝐺‘𝑌) ∧ (𝐺‘𝑌) < ((𝐺‘𝑋) + 𝐷))) |
| 31 | 30 | ex 412 |
. . . 4
⊢ ((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝑌 ∈
(ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) → ((𝐺‘𝑌) ∈ (((𝐺‘𝑋) − 𝐷)(,)((𝐺‘𝑋) + 𝐷)) → (((𝐺‘𝑋) − 𝐷) < (𝐺‘𝑌) ∧ (𝐺‘𝑌) < ((𝐺‘𝑋) + 𝐷)))) |
| 32 | 12, 31 | sylbid 240 |
. . 3
⊢ ((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝑌 ∈
(ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) → (((𝐺 ↾ (ℝ ×
ℝ))‘𝑌) ∈
(((𝐺‘𝑋) − 𝐷)(,)((𝐺‘𝑋) + 𝐷)) → (((𝐺‘𝑋) − 𝐷) < (𝐺‘𝑌) ∧ (𝐺‘𝑌) < ((𝐺‘𝑋) + 𝐷)))) |
| 33 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑥 = 𝑌 → (𝐺‘𝑥) = (𝐺‘𝑌)) |
| 34 | 33 | eleq1d 2826 |
. . . . . 6
⊢ (𝑥 = 𝑌 → ((𝐺‘𝑥) ∈ ℝ ↔ (𝐺‘𝑌) ∈ ℝ)) |
| 35 | 34, 16 | vtoclga 3577 |
. . . . 5
⊢ (𝑌 ∈ (ℝ ×
ℝ) → (𝐺‘𝑌) ∈ ℝ) |
| 36 | 9, 35 | syl 17 |
. . . 4
⊢ ((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝑌 ∈
(ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) → (𝐺‘𝑌) ∈ ℝ) |
| 37 | | absdiflt 15356 |
. . . . 5
⊢ (((𝐺‘𝑌) ∈ ℝ ∧ (𝐺‘𝑋) ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((abs‘((𝐺‘𝑌) − (𝐺‘𝑋))) < 𝐷 ↔ (((𝐺‘𝑋) − 𝐷) < (𝐺‘𝑌) ∧ (𝐺‘𝑌) < ((𝐺‘𝑋) + 𝐷)))) |
| 38 | 37 | biimprd 248 |
. . . 4
⊢ (((𝐺‘𝑌) ∈ ℝ ∧ (𝐺‘𝑋) ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((((𝐺‘𝑋) − 𝐷) < (𝐺‘𝑌) ∧ (𝐺‘𝑌) < ((𝐺‘𝑋) + 𝐷)) → (abs‘((𝐺‘𝑌) − (𝐺‘𝑋))) < 𝐷)) |
| 39 | 36, 18, 20, 38 | syl3anc 1373 |
. . 3
⊢ ((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝑌 ∈
(ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) →
((((𝐺‘𝑋) − 𝐷) < (𝐺‘𝑌) ∧ (𝐺‘𝑌) < ((𝐺‘𝑋) + 𝐷)) → (abs‘((𝐺‘𝑌) − (𝐺‘𝑋))) < 𝐷)) |
| 40 | 8, 32, 39 | 3syld 60 |
. 2
⊢ ((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝑌 ∈
(ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) → (𝑌 ∈ (◡(𝐺 ↾ (ℝ × ℝ)) “
(((𝐺‘𝑋) − 𝐷)(,)((𝐺‘𝑋) + 𝐷))) → (abs‘((𝐺‘𝑌) − (𝐺‘𝑋))) < 𝐷)) |
| 41 | | cnre2csqlem.2 |
. . . . . . 7
⊢ 𝐹 Fn (ℝ ×
ℝ) |
| 42 | | fnfvelrn 7100 |
. . . . . . 7
⊢ ((𝐹 Fn (ℝ × ℝ)
∧ 𝑌 ∈ (ℝ
× ℝ)) → (𝐹‘𝑌) ∈ ran 𝐹) |
| 43 | 41, 9, 42 | sylancr 587 |
. . . . . 6
⊢ ((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝑌 ∈
(ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) → (𝐹‘𝑌) ∈ ran 𝐹) |
| 44 | | fnfvelrn 7100 |
. . . . . . 7
⊢ ((𝐹 Fn (ℝ × ℝ)
∧ 𝑋 ∈ (ℝ
× ℝ)) → (𝐹‘𝑋) ∈ ran 𝐹) |
| 45 | 41, 13, 44 | sylancr 587 |
. . . . . 6
⊢ ((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝑌 ∈
(ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) → (𝐹‘𝑋) ∈ ran 𝐹) |
| 46 | | fvoveq1 7454 |
. . . . . . . 8
⊢ (𝑥 = (𝐹‘𝑌) → (𝐻‘(𝑥 − 𝑦)) = (𝐻‘((𝐹‘𝑌) − 𝑦))) |
| 47 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑥 = (𝐹‘𝑌) → (𝐻‘𝑥) = (𝐻‘(𝐹‘𝑌))) |
| 48 | 47 | oveq1d 7446 |
. . . . . . . 8
⊢ (𝑥 = (𝐹‘𝑌) → ((𝐻‘𝑥) − (𝐻‘𝑦)) = ((𝐻‘(𝐹‘𝑌)) − (𝐻‘𝑦))) |
| 49 | 46, 48 | eqeq12d 2753 |
. . . . . . 7
⊢ (𝑥 = (𝐹‘𝑌) → ((𝐻‘(𝑥 − 𝑦)) = ((𝐻‘𝑥) − (𝐻‘𝑦)) ↔ (𝐻‘((𝐹‘𝑌) − 𝑦)) = ((𝐻‘(𝐹‘𝑌)) − (𝐻‘𝑦)))) |
| 50 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑦 = (𝐹‘𝑋) → ((𝐹‘𝑌) − 𝑦) = ((𝐹‘𝑌) − (𝐹‘𝑋))) |
| 51 | 50 | fveq2d 6910 |
. . . . . . . 8
⊢ (𝑦 = (𝐹‘𝑋) → (𝐻‘((𝐹‘𝑌) − 𝑦)) = (𝐻‘((𝐹‘𝑌) − (𝐹‘𝑋)))) |
| 52 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑦 = (𝐹‘𝑋) → (𝐻‘𝑦) = (𝐻‘(𝐹‘𝑋))) |
| 53 | 52 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝑦 = (𝐹‘𝑋) → ((𝐻‘(𝐹‘𝑌)) − (𝐻‘𝑦)) = ((𝐻‘(𝐹‘𝑌)) − (𝐻‘(𝐹‘𝑋)))) |
| 54 | 51, 53 | eqeq12d 2753 |
. . . . . . 7
⊢ (𝑦 = (𝐹‘𝑋) → ((𝐻‘((𝐹‘𝑌) − 𝑦)) = ((𝐻‘(𝐹‘𝑌)) − (𝐻‘𝑦)) ↔ (𝐻‘((𝐹‘𝑌) − (𝐹‘𝑋))) = ((𝐻‘(𝐹‘𝑌)) − (𝐻‘(𝐹‘𝑋))))) |
| 55 | | cnre2csqlem.5 |
. . . . . . 7
⊢ ((𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹) → (𝐻‘(𝑥 − 𝑦)) = ((𝐻‘𝑥) − (𝐻‘𝑦))) |
| 56 | 49, 54, 55 | vtocl2ga 3578 |
. . . . . 6
⊢ (((𝐹‘𝑌) ∈ ran 𝐹 ∧ (𝐹‘𝑋) ∈ ran 𝐹) → (𝐻‘((𝐹‘𝑌) − (𝐹‘𝑋))) = ((𝐻‘(𝐹‘𝑌)) − (𝐻‘(𝐹‘𝑋)))) |
| 57 | 43, 45, 56 | syl2anc 584 |
. . . . 5
⊢ ((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝑌 ∈
(ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) → (𝐻‘((𝐹‘𝑌) − (𝐹‘𝑋))) = ((𝐻‘(𝐹‘𝑌)) − (𝐻‘(𝐹‘𝑋)))) |
| 58 | | cnre2csqlem.1 |
. . . . . . . 8
⊢ (𝐺 ↾ (ℝ ×
ℝ)) = (𝐻 ∘
𝐹) |
| 59 | 58 | fveq1i 6907 |
. . . . . . 7
⊢ ((𝐺 ↾ (ℝ ×
ℝ))‘𝑌) =
((𝐻 ∘ 𝐹)‘𝑌) |
| 60 | | fvco2 7006 |
. . . . . . . 8
⊢ ((𝐹 Fn (ℝ × ℝ)
∧ 𝑌 ∈ (ℝ
× ℝ)) → ((𝐻 ∘ 𝐹)‘𝑌) = (𝐻‘(𝐹‘𝑌))) |
| 61 | 41, 9, 60 | sylancr 587 |
. . . . . . 7
⊢ ((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝑌 ∈
(ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) → ((𝐻 ∘ 𝐹)‘𝑌) = (𝐻‘(𝐹‘𝑌))) |
| 62 | 59, 11, 61 | 3eqtr3a 2801 |
. . . . . 6
⊢ ((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝑌 ∈
(ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) → (𝐺‘𝑌) = (𝐻‘(𝐹‘𝑌))) |
| 63 | 58 | fveq1i 6907 |
. . . . . . 7
⊢ ((𝐺 ↾ (ℝ ×
ℝ))‘𝑋) =
((𝐻 ∘ 𝐹)‘𝑋) |
| 64 | | fvres 6925 |
. . . . . . . 8
⊢ (𝑋 ∈ (ℝ ×
ℝ) → ((𝐺 ↾
(ℝ × ℝ))‘𝑋) = (𝐺‘𝑋)) |
| 65 | 13, 64 | syl 17 |
. . . . . . 7
⊢ ((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝑌 ∈
(ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) → ((𝐺 ↾ (ℝ ×
ℝ))‘𝑋) = (𝐺‘𝑋)) |
| 66 | | fvco2 7006 |
. . . . . . . 8
⊢ ((𝐹 Fn (ℝ × ℝ)
∧ 𝑋 ∈ (ℝ
× ℝ)) → ((𝐻 ∘ 𝐹)‘𝑋) = (𝐻‘(𝐹‘𝑋))) |
| 67 | 41, 13, 66 | sylancr 587 |
. . . . . . 7
⊢ ((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝑌 ∈
(ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) → ((𝐻 ∘ 𝐹)‘𝑋) = (𝐻‘(𝐹‘𝑋))) |
| 68 | 63, 65, 67 | 3eqtr3a 2801 |
. . . . . 6
⊢ ((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝑌 ∈
(ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) → (𝐺‘𝑋) = (𝐻‘(𝐹‘𝑋))) |
| 69 | 62, 68 | oveq12d 7449 |
. . . . 5
⊢ ((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝑌 ∈
(ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) → ((𝐺‘𝑌) − (𝐺‘𝑋)) = ((𝐻‘(𝐹‘𝑌)) − (𝐻‘(𝐹‘𝑋)))) |
| 70 | 57, 69 | eqtr4d 2780 |
. . . 4
⊢ ((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝑌 ∈
(ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) → (𝐻‘((𝐹‘𝑌) − (𝐹‘𝑋))) = ((𝐺‘𝑌) − (𝐺‘𝑋))) |
| 71 | 70 | fveq2d 6910 |
. . 3
⊢ ((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝑌 ∈
(ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) →
(abs‘(𝐻‘((𝐹‘𝑌) − (𝐹‘𝑋)))) = (abs‘((𝐺‘𝑌) − (𝐺‘𝑋)))) |
| 72 | 71 | breq1d 5153 |
. 2
⊢ ((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝑌 ∈
(ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) →
((abs‘(𝐻‘((𝐹‘𝑌) − (𝐹‘𝑋)))) < 𝐷 ↔ (abs‘((𝐺‘𝑌) − (𝐺‘𝑋))) < 𝐷)) |
| 73 | 40, 72 | sylibrd 259 |
1
⊢ ((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝑌 ∈
(ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) → (𝑌 ∈ (◡(𝐺 ↾ (ℝ × ℝ)) “
(((𝐺‘𝑋) − 𝐷)(,)((𝐺‘𝑋) + 𝐷))) → (abs‘(𝐻‘((𝐹‘𝑌) − (𝐹‘𝑋)))) < 𝐷)) |