Proof of Theorem itscnhlinecirc02plem3
Step | Hyp | Ref
| Expression |
1 | | itscnhlinecirc02p.i |
. . . . . 6
⊢ 𝐼 = {1, 2} |
2 | | itscnhlinecirc02p.p |
. . . . . 6
⊢ 𝑃 = (ℝ ↑m
𝐼) |
3 | 1, 2 | rrx2pxel 45776 |
. . . . 5
⊢ (𝑋 ∈ 𝑃 → (𝑋‘1) ∈ ℝ) |
4 | 1, 2 | rrx2pyel 45777 |
. . . . 5
⊢ (𝑋 ∈ 𝑃 → (𝑋‘2) ∈ ℝ) |
5 | 3, 4 | jca 515 |
. . . 4
⊢ (𝑋 ∈ 𝑃 → ((𝑋‘1) ∈ ℝ ∧ (𝑋‘2) ∈
ℝ)) |
6 | 5 | 3ad2ant1 1135 |
. . 3
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) → ((𝑋‘1) ∈ ℝ ∧ (𝑋‘2) ∈
ℝ)) |
7 | 6 | adantr 484 |
. 2
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) → ((𝑋‘1) ∈ ℝ ∧ (𝑋‘2) ∈
ℝ)) |
8 | 1, 2 | rrx2pxel 45776 |
. . . . 5
⊢ (𝑌 ∈ 𝑃 → (𝑌‘1) ∈ ℝ) |
9 | 1, 2 | rrx2pyel 45777 |
. . . . 5
⊢ (𝑌 ∈ 𝑃 → (𝑌‘2) ∈ ℝ) |
10 | 8, 9 | jca 515 |
. . . 4
⊢ (𝑌 ∈ 𝑃 → ((𝑌‘1) ∈ ℝ ∧ (𝑌‘2) ∈
ℝ)) |
11 | 10 | 3ad2ant2 1136 |
. . 3
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) → ((𝑌‘1) ∈ ℝ ∧ (𝑌‘2) ∈
ℝ)) |
12 | 11 | adantr 484 |
. 2
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) → ((𝑌‘1) ∈ ℝ ∧ (𝑌‘2) ∈
ℝ)) |
13 | | simpl3 1195 |
. 2
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) → (𝑋‘2) ≠ (𝑌‘2)) |
14 | | rpre 12624 |
. . . 4
⊢ (𝑅 ∈ ℝ+
→ 𝑅 ∈
ℝ) |
15 | 14 | adantr 484 |
. . 3
⊢ ((𝑅 ∈ ℝ+
∧ (𝑋𝐷 0 ) < 𝑅) → 𝑅 ∈ ℝ) |
16 | 15 | adantl 485 |
. 2
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) → 𝑅 ∈ ℝ) |
17 | | simpl1 1193 |
. . . . . 6
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ 𝑅 ∈ ℝ+) → 𝑋 ∈ 𝑃) |
18 | | itscnhlinecirc02p.e |
. . . . . . . 8
⊢ 𝐸 = (ℝ^‘𝐼) |
19 | | 2nn0 12137 |
. . . . . . . . . 10
⊢ 2 ∈
ℕ0 |
20 | | eqid 2739 |
. . . . . . . . . . 11
⊢
(𝔼hil‘2) =
(𝔼hil‘2) |
21 | 20 | ehlval 24343 |
. . . . . . . . . 10
⊢ (2 ∈
ℕ0 → (𝔼hil‘2) =
(ℝ^‘(1...2))) |
22 | 19, 21 | ax-mp 5 |
. . . . . . . . 9
⊢
(𝔼hil‘2) =
(ℝ^‘(1...2)) |
23 | | fz12pr 13199 |
. . . . . . . . . . 11
⊢ (1...2) =
{1, 2} |
24 | 23, 1 | eqtr4i 2770 |
. . . . . . . . . 10
⊢ (1...2) =
𝐼 |
25 | 24 | fveq2i 6742 |
. . . . . . . . 9
⊢
(ℝ^‘(1...2)) = (ℝ^‘𝐼) |
26 | 22, 25 | eqtri 2767 |
. . . . . . . 8
⊢
(𝔼hil‘2) = (ℝ^‘𝐼) |
27 | 18, 26 | eqtr4i 2770 |
. . . . . . 7
⊢ 𝐸 =
(𝔼hil‘2) |
28 | 1 | oveq2i 7246 |
. . . . . . . 8
⊢ (ℝ
↑m 𝐼) =
(ℝ ↑m {1, 2}) |
29 | 2, 28 | eqtri 2767 |
. . . . . . 7
⊢ 𝑃 = (ℝ ↑m
{1, 2}) |
30 | | itscnhlinecirc02p.d |
. . . . . . 7
⊢ 𝐷 = (dist‘𝐸) |
31 | | itscnhlinecirc02p.0 |
. . . . . . . 8
⊢ 0 = (𝐼 × {0}) |
32 | 1 | xpeq1i 5595 |
. . . . . . . 8
⊢ (𝐼 × {0}) = ({1, 2} ×
{0}) |
33 | 31, 32 | eqtri 2767 |
. . . . . . 7
⊢ 0 = ({1, 2}
× {0}) |
34 | 27, 29, 30, 33 | ehl2eudisval0 45790 |
. . . . . 6
⊢ (𝑋 ∈ 𝑃 → (𝑋𝐷 0 ) =
(√‘(((𝑋‘1)↑2) + ((𝑋‘2)↑2)))) |
35 | 17, 34 | syl 17 |
. . . . 5
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ 𝑅 ∈ ℝ+) → (𝑋𝐷 0 ) =
(√‘(((𝑋‘1)↑2) + ((𝑋‘2)↑2)))) |
36 | 35 | breq1d 5080 |
. . . 4
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ 𝑅 ∈ ℝ+) → ((𝑋𝐷 0 ) < 𝑅 ↔ (√‘(((𝑋‘1)↑2) + ((𝑋‘2)↑2))) < 𝑅)) |
37 | | rpge0 12629 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ ℝ+
→ 0 ≤ 𝑅) |
38 | 14, 37 | sqrtsqd 15016 |
. . . . . . . . . 10
⊢ (𝑅 ∈ ℝ+
→ (√‘(𝑅↑2)) = 𝑅) |
39 | 38 | eqcomd 2745 |
. . . . . . . . 9
⊢ (𝑅 ∈ ℝ+
→ 𝑅 =
(√‘(𝑅↑2))) |
40 | 39 | adantl 485 |
. . . . . . . 8
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ 𝑅 ∈ ℝ+) → 𝑅 = (√‘(𝑅↑2))) |
41 | 40 | breq2d 5082 |
. . . . . . 7
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ 𝑅 ∈ ℝ+) →
((√‘(((𝑋‘1)↑2) + ((𝑋‘2)↑2))) < 𝑅 ↔ (√‘(((𝑋‘1)↑2) + ((𝑋‘2)↑2))) <
(√‘(𝑅↑2)))) |
42 | 41 | biimpa 480 |
. . . . . 6
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ 𝑅 ∈ ℝ+) ∧
(√‘(((𝑋‘1)↑2) + ((𝑋‘2)↑2))) < 𝑅) → (√‘(((𝑋‘1)↑2) + ((𝑋‘2)↑2))) <
(√‘(𝑅↑2))) |
43 | 17, 3 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ 𝑅 ∈ ℝ+) → (𝑋‘1) ∈
ℝ) |
44 | 43 | adantr 484 |
. . . . . . . . 9
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ 𝑅 ∈ ℝ+) ∧
(√‘(((𝑋‘1)↑2) + ((𝑋‘2)↑2))) < 𝑅) → (𝑋‘1) ∈ ℝ) |
45 | 44 | resqcld 13850 |
. . . . . . . 8
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ 𝑅 ∈ ℝ+) ∧
(√‘(((𝑋‘1)↑2) + ((𝑋‘2)↑2))) < 𝑅) → ((𝑋‘1)↑2) ∈
ℝ) |
46 | 17, 4 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ 𝑅 ∈ ℝ+) → (𝑋‘2) ∈
ℝ) |
47 | 46 | adantr 484 |
. . . . . . . . 9
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ 𝑅 ∈ ℝ+) ∧
(√‘(((𝑋‘1)↑2) + ((𝑋‘2)↑2))) < 𝑅) → (𝑋‘2) ∈ ℝ) |
48 | 47 | resqcld 13850 |
. . . . . . . 8
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ 𝑅 ∈ ℝ+) ∧
(√‘(((𝑋‘1)↑2) + ((𝑋‘2)↑2))) < 𝑅) → ((𝑋‘2)↑2) ∈
ℝ) |
49 | 45, 48 | readdcld 10892 |
. . . . . . 7
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ 𝑅 ∈ ℝ+) ∧
(√‘(((𝑋‘1)↑2) + ((𝑋‘2)↑2))) < 𝑅) → (((𝑋‘1)↑2) + ((𝑋‘2)↑2)) ∈
ℝ) |
50 | 44 | sqge0d 13851 |
. . . . . . . 8
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ 𝑅 ∈ ℝ+) ∧
(√‘(((𝑋‘1)↑2) + ((𝑋‘2)↑2))) < 𝑅) → 0 ≤ ((𝑋‘1)↑2)) |
51 | 47 | sqge0d 13851 |
. . . . . . . 8
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ 𝑅 ∈ ℝ+) ∧
(√‘(((𝑋‘1)↑2) + ((𝑋‘2)↑2))) < 𝑅) → 0 ≤ ((𝑋‘2)↑2)) |
52 | 45, 48, 50, 51 | addge0d 11438 |
. . . . . . 7
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ 𝑅 ∈ ℝ+) ∧
(√‘(((𝑋‘1)↑2) + ((𝑋‘2)↑2))) < 𝑅) → 0 ≤ (((𝑋‘1)↑2) + ((𝑋‘2)↑2))) |
53 | 14 | adantl 485 |
. . . . . . . . 9
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ 𝑅 ∈ ℝ+) → 𝑅 ∈
ℝ) |
54 | 53 | adantr 484 |
. . . . . . . 8
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ 𝑅 ∈ ℝ+) ∧
(√‘(((𝑋‘1)↑2) + ((𝑋‘2)↑2))) < 𝑅) → 𝑅 ∈ ℝ) |
55 | 54 | resqcld 13850 |
. . . . . . 7
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ 𝑅 ∈ ℝ+) ∧
(√‘(((𝑋‘1)↑2) + ((𝑋‘2)↑2))) < 𝑅) → (𝑅↑2) ∈ ℝ) |
56 | 54 | sqge0d 13851 |
. . . . . . 7
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ 𝑅 ∈ ℝ+) ∧
(√‘(((𝑋‘1)↑2) + ((𝑋‘2)↑2))) < 𝑅) → 0 ≤ (𝑅↑2)) |
57 | 49, 52, 55, 56 | sqrtltd 15024 |
. . . . . 6
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ 𝑅 ∈ ℝ+) ∧
(√‘(((𝑋‘1)↑2) + ((𝑋‘2)↑2))) < 𝑅) → ((((𝑋‘1)↑2) + ((𝑋‘2)↑2)) < (𝑅↑2) ↔ (√‘(((𝑋‘1)↑2) + ((𝑋‘2)↑2))) <
(√‘(𝑅↑2)))) |
58 | 42, 57 | mpbird 260 |
. . . . 5
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ 𝑅 ∈ ℝ+) ∧
(√‘(((𝑋‘1)↑2) + ((𝑋‘2)↑2))) < 𝑅) → (((𝑋‘1)↑2) + ((𝑋‘2)↑2)) < (𝑅↑2)) |
59 | 58 | ex 416 |
. . . 4
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ 𝑅 ∈ ℝ+) →
((√‘(((𝑋‘1)↑2) + ((𝑋‘2)↑2))) < 𝑅 → (((𝑋‘1)↑2) + ((𝑋‘2)↑2)) < (𝑅↑2))) |
60 | 36, 59 | sylbid 243 |
. . 3
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ 𝑅 ∈ ℝ+) → ((𝑋𝐷 0 ) < 𝑅 → (((𝑋‘1)↑2) + ((𝑋‘2)↑2)) < (𝑅↑2))) |
61 | 60 | impr 458 |
. 2
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) → (((𝑋‘1)↑2) + ((𝑋‘2)↑2)) < (𝑅↑2)) |
62 | | eqid 2739 |
. . 3
⊢ ((𝑌‘1) − (𝑋‘1)) = ((𝑌‘1) − (𝑋‘1)) |
63 | | eqid 2739 |
. . 3
⊢ ((𝑋‘2) − (𝑌‘2)) = ((𝑋‘2) − (𝑌‘2)) |
64 | | eqid 2739 |
. . 3
⊢ (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))) = (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))) |
65 | 62, 63, 64 | itscnhlinecirc02plem2 45848 |
. 2
⊢
(((((𝑋‘1)
∈ ℝ ∧ (𝑋‘2) ∈ ℝ) ∧ ((𝑌‘1) ∈ ℝ ∧
(𝑌‘2) ∈ ℝ)
∧ (𝑋‘2) ≠
(𝑌‘2)) ∧ (𝑅 ∈ ℝ ∧ (((𝑋‘1)↑2) + ((𝑋‘2)↑2)) < (𝑅↑2))) → 0 < ((-(2
· (((𝑌‘1)
− (𝑋‘1))
· (((𝑋‘2)
· (𝑌‘1))
− ((𝑋‘1)
· (𝑌‘2)))))↑2) − (4 ·
(((((𝑋‘2) −
(𝑌‘2))↑2) +
(((𝑌‘1) −
(𝑋‘1))↑2))
· (((((𝑋‘2)
· (𝑌‘1))
− ((𝑋‘1)
· (𝑌‘2)))↑2) − ((((𝑋‘2) − (𝑌‘2))↑2) ·
(𝑅↑2))))))) |
66 | 7, 12, 13, 16, 61, 65 | syl32anc 1380 |
1
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) → 0 < ((-(2 · (((𝑌‘1) − (𝑋‘1)) · (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))))↑2) − (4
· (((((𝑋‘2)
− (𝑌‘2))↑2) + (((𝑌‘1) − (𝑋‘1))↑2)) · (((((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))↑2) −
((((𝑋‘2) −
(𝑌‘2))↑2)
· (𝑅↑2))))))) |