Proof of Theorem 2sphere
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 2sphere.i | . . . 4
⊢ 𝐼 = {1, 2} | 
| 2 |  | prfi 9363 | . . . 4
⊢ {1, 2}
∈ Fin | 
| 3 | 1, 2 | eqeltri 2837 | . . 3
⊢ 𝐼 ∈ Fin | 
| 4 |  | simpl 482 | . . 3
⊢ ((𝑀 ∈ 𝑃 ∧ 𝑅 ∈ (0[,)+∞)) → 𝑀 ∈ 𝑃) | 
| 5 |  | elrege0 13494 | . . . . 5
⊢ (𝑅 ∈ (0[,)+∞) ↔
(𝑅 ∈ ℝ ∧ 0
≤ 𝑅)) | 
| 6 | 5 | simplbi 497 | . . . 4
⊢ (𝑅 ∈ (0[,)+∞) →
𝑅 ∈
ℝ) | 
| 7 | 6 | adantl 481 | . . 3
⊢ ((𝑀 ∈ 𝑃 ∧ 𝑅 ∈ (0[,)+∞)) → 𝑅 ∈
ℝ) | 
| 8 |  | 2sphere.e | . . . 4
⊢ 𝐸 = (ℝ^‘𝐼) | 
| 9 |  | 2sphere.p | . . . 4
⊢ 𝑃 = (ℝ ↑m
𝐼) | 
| 10 |  | eqid 2737 | . . . 4
⊢
(dist‘𝐸) =
(dist‘𝐸) | 
| 11 |  | 2sphere.s | . . . 4
⊢ 𝑆 = (Sphere‘𝐸) | 
| 12 | 8, 9, 10, 11 | rrxsphere 48669 | . . 3
⊢ ((𝐼 ∈ Fin ∧ 𝑀 ∈ 𝑃 ∧ 𝑅 ∈ ℝ) → (𝑀𝑆𝑅) = {𝑝 ∈ 𝑃 ∣ (𝑝(dist‘𝐸)𝑀) = 𝑅}) | 
| 13 | 3, 4, 7, 12 | mp3an2i 1468 | . 2
⊢ ((𝑀 ∈ 𝑃 ∧ 𝑅 ∈ (0[,)+∞)) → (𝑀𝑆𝑅) = {𝑝 ∈ 𝑃 ∣ (𝑝(dist‘𝐸)𝑀) = 𝑅}) | 
| 14 |  | 2sphere.c | . . 3
⊢ 𝐶 = {𝑝 ∈ 𝑃 ∣ ((((𝑝‘1) − (𝑀‘1))↑2) + (((𝑝‘2) − (𝑀‘2))↑2)) = (𝑅↑2)} | 
| 15 | 5 | biimpi 216 | . . . . . . . 8
⊢ (𝑅 ∈ (0[,)+∞) →
(𝑅 ∈ ℝ ∧ 0
≤ 𝑅)) | 
| 16 | 15 | ad2antlr 727 | . . . . . . 7
⊢ (((𝑀 ∈ 𝑃 ∧ 𝑅 ∈ (0[,)+∞)) ∧ 𝑝 ∈ 𝑃) → (𝑅 ∈ ℝ ∧ 0 ≤ 𝑅)) | 
| 17 |  | sqrtsq 15308 | . . . . . . 7
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤
𝑅) →
(√‘(𝑅↑2))
= 𝑅) | 
| 18 | 16, 17 | syl 17 | . . . . . 6
⊢ (((𝑀 ∈ 𝑃 ∧ 𝑅 ∈ (0[,)+∞)) ∧ 𝑝 ∈ 𝑃) → (√‘(𝑅↑2)) = 𝑅) | 
| 19 | 18 | eqeq2d 2748 | . . . . 5
⊢ (((𝑀 ∈ 𝑃 ∧ 𝑅 ∈ (0[,)+∞)) ∧ 𝑝 ∈ 𝑃) → ((√‘((((𝑝‘1) − (𝑀‘1))↑2) + (((𝑝‘2) − (𝑀‘2))↑2))) =
(√‘(𝑅↑2))
↔ (√‘((((𝑝‘1) − (𝑀‘1))↑2) + (((𝑝‘2) − (𝑀‘2))↑2))) = 𝑅)) | 
| 20 | 1, 9 | rrx2pxel 48632 | . . . . . . . . . . . 12
⊢ (𝑝 ∈ 𝑃 → (𝑝‘1) ∈ ℝ) | 
| 21 | 20 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝑀 ∈ 𝑃 ∧ 𝑝 ∈ 𝑃) → (𝑝‘1) ∈ ℝ) | 
| 22 | 1, 9 | rrx2pxel 48632 | . . . . . . . . . . . 12
⊢ (𝑀 ∈ 𝑃 → (𝑀‘1) ∈ ℝ) | 
| 23 | 22 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝑀 ∈ 𝑃 ∧ 𝑝 ∈ 𝑃) → (𝑀‘1) ∈ ℝ) | 
| 24 | 21, 23 | resubcld 11691 | . . . . . . . . . 10
⊢ ((𝑀 ∈ 𝑃 ∧ 𝑝 ∈ 𝑃) → ((𝑝‘1) − (𝑀‘1)) ∈ ℝ) | 
| 25 | 24 | resqcld 14165 | . . . . . . . . 9
⊢ ((𝑀 ∈ 𝑃 ∧ 𝑝 ∈ 𝑃) → (((𝑝‘1) − (𝑀‘1))↑2) ∈
ℝ) | 
| 26 | 1, 9 | rrx2pyel 48633 | . . . . . . . . . . . 12
⊢ (𝑝 ∈ 𝑃 → (𝑝‘2) ∈ ℝ) | 
| 27 | 26 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝑀 ∈ 𝑃 ∧ 𝑝 ∈ 𝑃) → (𝑝‘2) ∈ ℝ) | 
| 28 | 1, 9 | rrx2pyel 48633 | . . . . . . . . . . . 12
⊢ (𝑀 ∈ 𝑃 → (𝑀‘2) ∈ ℝ) | 
| 29 | 28 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝑀 ∈ 𝑃 ∧ 𝑝 ∈ 𝑃) → (𝑀‘2) ∈ ℝ) | 
| 30 | 27, 29 | resubcld 11691 | . . . . . . . . . 10
⊢ ((𝑀 ∈ 𝑃 ∧ 𝑝 ∈ 𝑃) → ((𝑝‘2) − (𝑀‘2)) ∈ ℝ) | 
| 31 | 30 | resqcld 14165 | . . . . . . . . 9
⊢ ((𝑀 ∈ 𝑃 ∧ 𝑝 ∈ 𝑃) → (((𝑝‘2) − (𝑀‘2))↑2) ∈
ℝ) | 
| 32 | 25, 31 | readdcld 11290 | . . . . . . . 8
⊢ ((𝑀 ∈ 𝑃 ∧ 𝑝 ∈ 𝑃) → ((((𝑝‘1) − (𝑀‘1))↑2) + (((𝑝‘2) − (𝑀‘2))↑2)) ∈
ℝ) | 
| 33 | 24 | sqge0d 14177 | . . . . . . . . 9
⊢ ((𝑀 ∈ 𝑃 ∧ 𝑝 ∈ 𝑃) → 0 ≤ (((𝑝‘1) − (𝑀‘1))↑2)) | 
| 34 | 30 | sqge0d 14177 | . . . . . . . . 9
⊢ ((𝑀 ∈ 𝑃 ∧ 𝑝 ∈ 𝑃) → 0 ≤ (((𝑝‘2) − (𝑀‘2))↑2)) | 
| 35 | 25, 31, 33, 34 | addge0d 11839 | . . . . . . . 8
⊢ ((𝑀 ∈ 𝑃 ∧ 𝑝 ∈ 𝑃) → 0 ≤ ((((𝑝‘1) − (𝑀‘1))↑2) + (((𝑝‘2) − (𝑀‘2))↑2))) | 
| 36 | 32, 35 | jca 511 | . . . . . . 7
⊢ ((𝑀 ∈ 𝑃 ∧ 𝑝 ∈ 𝑃) → (((((𝑝‘1) − (𝑀‘1))↑2) + (((𝑝‘2) − (𝑀‘2))↑2)) ∈ ℝ ∧ 0
≤ ((((𝑝‘1) −
(𝑀‘1))↑2) +
(((𝑝‘2) −
(𝑀‘2))↑2)))) | 
| 37 | 36 | adantlr 715 | . . . . . 6
⊢ (((𝑀 ∈ 𝑃 ∧ 𝑅 ∈ (0[,)+∞)) ∧ 𝑝 ∈ 𝑃) → (((((𝑝‘1) − (𝑀‘1))↑2) + (((𝑝‘2) − (𝑀‘2))↑2)) ∈ ℝ ∧ 0
≤ ((((𝑝‘1) −
(𝑀‘1))↑2) +
(((𝑝‘2) −
(𝑀‘2))↑2)))) | 
| 38 |  | resqcl 14164 | . . . . . . . . 9
⊢ (𝑅 ∈ ℝ → (𝑅↑2) ∈
ℝ) | 
| 39 |  | sqge0 14176 | . . . . . . . . 9
⊢ (𝑅 ∈ ℝ → 0 ≤
(𝑅↑2)) | 
| 40 | 38, 39 | jca 511 | . . . . . . . 8
⊢ (𝑅 ∈ ℝ → ((𝑅↑2) ∈ ℝ ∧ 0
≤ (𝑅↑2))) | 
| 41 | 6, 40 | syl 17 | . . . . . . 7
⊢ (𝑅 ∈ (0[,)+∞) →
((𝑅↑2) ∈ ℝ
∧ 0 ≤ (𝑅↑2))) | 
| 42 | 41 | ad2antlr 727 | . . . . . 6
⊢ (((𝑀 ∈ 𝑃 ∧ 𝑅 ∈ (0[,)+∞)) ∧ 𝑝 ∈ 𝑃) → ((𝑅↑2) ∈ ℝ ∧ 0 ≤ (𝑅↑2))) | 
| 43 |  | sqrt11 15301 | . . . . . 6
⊢
(((((((𝑝‘1)
− (𝑀‘1))↑2) + (((𝑝‘2) − (𝑀‘2))↑2)) ∈ ℝ ∧ 0
≤ ((((𝑝‘1) −
(𝑀‘1))↑2) +
(((𝑝‘2) −
(𝑀‘2))↑2)))
∧ ((𝑅↑2) ∈
ℝ ∧ 0 ≤ (𝑅↑2))) → ((√‘((((𝑝‘1) − (𝑀‘1))↑2) + (((𝑝‘2) − (𝑀‘2))↑2))) =
(√‘(𝑅↑2))
↔ ((((𝑝‘1)
− (𝑀‘1))↑2) + (((𝑝‘2) − (𝑀‘2))↑2)) = (𝑅↑2))) | 
| 44 | 37, 42, 43 | syl2anc 584 | . . . . 5
⊢ (((𝑀 ∈ 𝑃 ∧ 𝑅 ∈ (0[,)+∞)) ∧ 𝑝 ∈ 𝑃) → ((√‘((((𝑝‘1) − (𝑀‘1))↑2) + (((𝑝‘2) − (𝑀‘2))↑2))) =
(√‘(𝑅↑2))
↔ ((((𝑝‘1)
− (𝑀‘1))↑2) + (((𝑝‘2) − (𝑀‘2))↑2)) = (𝑅↑2))) | 
| 45 | 4 | anim1ci 616 | . . . . . . . 8
⊢ (((𝑀 ∈ 𝑃 ∧ 𝑅 ∈ (0[,)+∞)) ∧ 𝑝 ∈ 𝑃) → (𝑝 ∈ 𝑃 ∧ 𝑀 ∈ 𝑃)) | 
| 46 |  | 2nn0 12543 | . . . . . . . . . . . 12
⊢ 2 ∈
ℕ0 | 
| 47 |  | eqid 2737 | . . . . . . . . . . . . 13
⊢
(𝔼hil‘2) =
(𝔼hil‘2) | 
| 48 | 47 | ehlval 25448 | . . . . . . . . . . . 12
⊢ (2 ∈
ℕ0 → (𝔼hil‘2) =
(ℝ^‘(1...2))) | 
| 49 | 46, 48 | ax-mp 5 | . . . . . . . . . . 11
⊢
(𝔼hil‘2) =
(ℝ^‘(1...2)) | 
| 50 |  | fz12pr 13621 | . . . . . . . . . . . . 13
⊢ (1...2) =
{1, 2} | 
| 51 | 50, 1 | eqtr4i 2768 | . . . . . . . . . . . 12
⊢ (1...2) =
𝐼 | 
| 52 | 51 | fveq2i 6909 | . . . . . . . . . . 11
⊢
(ℝ^‘(1...2)) = (ℝ^‘𝐼) | 
| 53 | 49, 52 | eqtri 2765 | . . . . . . . . . 10
⊢
(𝔼hil‘2) = (ℝ^‘𝐼) | 
| 54 | 8, 53 | eqtr4i 2768 | . . . . . . . . 9
⊢ 𝐸 =
(𝔼hil‘2) | 
| 55 | 1 | oveq2i 7442 | . . . . . . . . . 10
⊢ (ℝ
↑m 𝐼) =
(ℝ ↑m {1, 2}) | 
| 56 | 9, 55 | eqtri 2765 | . . . . . . . . 9
⊢ 𝑃 = (ℝ ↑m
{1, 2}) | 
| 57 | 54, 56, 10 | ehl2eudisval 25457 | . . . . . . . 8
⊢ ((𝑝 ∈ 𝑃 ∧ 𝑀 ∈ 𝑃) → (𝑝(dist‘𝐸)𝑀) = (√‘((((𝑝‘1) − (𝑀‘1))↑2) + (((𝑝‘2) − (𝑀‘2))↑2)))) | 
| 58 | 45, 57 | syl 17 | . . . . . . 7
⊢ (((𝑀 ∈ 𝑃 ∧ 𝑅 ∈ (0[,)+∞)) ∧ 𝑝 ∈ 𝑃) → (𝑝(dist‘𝐸)𝑀) = (√‘((((𝑝‘1) − (𝑀‘1))↑2) + (((𝑝‘2) − (𝑀‘2))↑2)))) | 
| 59 | 58 | eqcomd 2743 | . . . . . 6
⊢ (((𝑀 ∈ 𝑃 ∧ 𝑅 ∈ (0[,)+∞)) ∧ 𝑝 ∈ 𝑃) → (√‘((((𝑝‘1) − (𝑀‘1))↑2) + (((𝑝‘2) − (𝑀‘2))↑2))) = (𝑝(dist‘𝐸)𝑀)) | 
| 60 | 59 | eqeq1d 2739 | . . . . 5
⊢ (((𝑀 ∈ 𝑃 ∧ 𝑅 ∈ (0[,)+∞)) ∧ 𝑝 ∈ 𝑃) → ((√‘((((𝑝‘1) − (𝑀‘1))↑2) + (((𝑝‘2) − (𝑀‘2))↑2))) = 𝑅 ↔ (𝑝(dist‘𝐸)𝑀) = 𝑅)) | 
| 61 | 19, 44, 60 | 3bitr3d 309 | . . . 4
⊢ (((𝑀 ∈ 𝑃 ∧ 𝑅 ∈ (0[,)+∞)) ∧ 𝑝 ∈ 𝑃) → (((((𝑝‘1) − (𝑀‘1))↑2) + (((𝑝‘2) − (𝑀‘2))↑2)) = (𝑅↑2) ↔ (𝑝(dist‘𝐸)𝑀) = 𝑅)) | 
| 62 | 61 | rabbidva 3443 | . . 3
⊢ ((𝑀 ∈ 𝑃 ∧ 𝑅 ∈ (0[,)+∞)) → {𝑝 ∈ 𝑃 ∣ ((((𝑝‘1) − (𝑀‘1))↑2) + (((𝑝‘2) − (𝑀‘2))↑2)) = (𝑅↑2)} = {𝑝 ∈ 𝑃 ∣ (𝑝(dist‘𝐸)𝑀) = 𝑅}) | 
| 63 | 14, 62 | eqtr2id 2790 | . 2
⊢ ((𝑀 ∈ 𝑃 ∧ 𝑅 ∈ (0[,)+∞)) → {𝑝 ∈ 𝑃 ∣ (𝑝(dist‘𝐸)𝑀) = 𝑅} = 𝐶) | 
| 64 | 13, 63 | eqtrd 2777 | 1
⊢ ((𝑀 ∈ 𝑃 ∧ 𝑅 ∈ (0[,)+∞)) → (𝑀𝑆𝑅) = 𝐶) |