Proof of Theorem constrelextdg2
| Step | Hyp | Ref
| Expression |
| 1 | | constrelextdg2.f |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 ∈
(SubDRing‘ℂfld)) |
| 2 | | cnfldbas 21368 |
. . . . . . . . . . . . . 14
⊢ ℂ =
(Base‘ℂfld) |
| 3 | 2 | sdrgss 20794 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈
(SubDRing‘ℂfld) → 𝐹 ⊆ ℂ) |
| 4 | 1, 3 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 ⊆ ℂ) |
| 5 | 4 | ad7antr 738 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝐹 ⊆ ℂ) |
| 6 | | constrelextdg2.1 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐶‘𝑁) ⊆ 𝐹) |
| 7 | 6 | ad7antr 738 |
. . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (𝐶‘𝑁) ⊆ 𝐹) |
| 8 | | simp-7r 790 |
. . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑎 ∈ (𝐶‘𝑁)) |
| 9 | 7, 8 | sseldd 3984 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑎 ∈ 𝐹) |
| 10 | | simp-6r 788 |
. . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑏 ∈ (𝐶‘𝑁)) |
| 11 | 7, 10 | sseldd 3984 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑏 ∈ 𝐹) |
| 12 | | simp-5r 786 |
. . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑐 ∈ (𝐶‘𝑁)) |
| 13 | 7, 12 | sseldd 3984 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑐 ∈ 𝐹) |
| 14 | | simp-4r 784 |
. . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑑 ∈ (𝐶‘𝑁)) |
| 15 | 7, 14 | sseldd 3984 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑑 ∈ 𝐹) |
| 16 | | simpllr 776 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑡 ∈ ℝ) |
| 17 | | simplr 769 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑟 ∈ ℝ) |
| 18 | | simpr1 1195 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎)))) |
| 19 | | simpr2 1196 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐)))) |
| 20 | | simpr3 1197 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) →
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) |
| 21 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝑎 + (((((𝑎 − 𝑐) · ((∗‘𝑑) − (∗‘𝑐))) −
(((∗‘𝑎)
− (∗‘𝑐))
· (𝑑 − 𝑐))) / ((((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐)) − ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐))))) · (𝑏 − 𝑎))) = (𝑎 + (((((𝑎 − 𝑐) · ((∗‘𝑑) − (∗‘𝑐))) −
(((∗‘𝑎)
− (∗‘𝑐))
· (𝑑 − 𝑐))) / ((((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐)) − ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐))))) · (𝑏 − 𝑎))) |
| 22 | 5, 9, 11, 13, 15, 16, 17, 18, 19, 20, 21 | constrrtll 33772 |
. . . . . . . . . 10
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑋 = (𝑎 + (((((𝑎 − 𝑐) · ((∗‘𝑑) − (∗‘𝑐))) −
(((∗‘𝑎)
− (∗‘𝑐))
· (𝑑 − 𝑐))) / ((((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐)) − ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐))))) · (𝑏 − 𝑎)))) |
| 23 | | cnfldadd 21370 |
. . . . . . . . . . 11
⊢ + =
(+g‘ℂfld) |
| 24 | | sdrgsubrg 20792 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈
(SubDRing‘ℂfld) → 𝐹 ∈
(SubRing‘ℂfld)) |
| 25 | | subrgsubg 20577 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈
(SubRing‘ℂfld) → 𝐹 ∈
(SubGrp‘ℂfld)) |
| 26 | 1, 24, 25 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 ∈
(SubGrp‘ℂfld)) |
| 27 | 26 | ad7antr 738 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝐹 ∈
(SubGrp‘ℂfld)) |
| 28 | | cnfldmul 21372 |
. . . . . . . . . . . 12
⊢ ·
= (.r‘ℂfld) |
| 29 | 1, 24 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 ∈
(SubRing‘ℂfld)) |
| 30 | 29 | ad7antr 738 |
. . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝐹 ∈
(SubRing‘ℂfld)) |
| 31 | | cnflddiv 21413 |
. . . . . . . . . . . . 13
⊢ / =
(/r‘ℂfld) |
| 32 | | cnfld0 21405 |
. . . . . . . . . . . . 13
⊢ 0 =
(0g‘ℂfld) |
| 33 | 1 | ad7antr 738 |
. . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝐹 ∈
(SubDRing‘ℂfld)) |
| 34 | | cnfldsub 21410 |
. . . . . . . . . . . . . 14
⊢ −
= (-g‘ℂfld) |
| 35 | 34, 27, 9, 13 | subgsubcld 33047 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (𝑎 − 𝑐) ∈ 𝐹) |
| 36 | | constr0.1 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐶 = rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1}) |
| 37 | | constrelextdg2.n |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑁 ∈ On) |
| 38 | 37 | ad7antr 738 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑁 ∈ On) |
| 39 | 36, 38, 14 | constrconj 33786 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (∗‘𝑑) ∈ (𝐶‘𝑁)) |
| 40 | 7, 39 | sseldd 3984 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (∗‘𝑑) ∈ 𝐹) |
| 41 | 36, 38, 12 | constrconj 33786 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (∗‘𝑐) ∈ (𝐶‘𝑁)) |
| 42 | 7, 41 | sseldd 3984 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (∗‘𝑐) ∈ 𝐹) |
| 43 | 34, 27, 40, 42 | subgsubcld 33047 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → ((∗‘𝑑) − (∗‘𝑐)) ∈ 𝐹) |
| 44 | 28, 30, 35, 43 | subrgmcld 33237 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → ((𝑎 − 𝑐) · ((∗‘𝑑) − (∗‘𝑐))) ∈ 𝐹) |
| 45 | 36, 38, 8 | constrconj 33786 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (∗‘𝑎) ∈ (𝐶‘𝑁)) |
| 46 | 7, 45 | sseldd 3984 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (∗‘𝑎) ∈ 𝐹) |
| 47 | 34, 27, 46, 42 | subgsubcld 33047 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → ((∗‘𝑎) − (∗‘𝑐)) ∈ 𝐹) |
| 48 | 34, 27, 15, 13 | subgsubcld 33047 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (𝑑 − 𝑐) ∈ 𝐹) |
| 49 | 28, 30, 47, 48 | subrgmcld 33237 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (((∗‘𝑎) − (∗‘𝑐)) · (𝑑 − 𝑐)) ∈ 𝐹) |
| 50 | 34, 27, 44, 49 | subgsubcld 33047 |
. . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (((𝑎 − 𝑐) · ((∗‘𝑑) − (∗‘𝑐))) −
(((∗‘𝑎)
− (∗‘𝑐))
· (𝑑 − 𝑐))) ∈ 𝐹) |
| 51 | 36, 38, 10 | constrconj 33786 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (∗‘𝑏) ∈ (𝐶‘𝑁)) |
| 52 | 7, 51 | sseldd 3984 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (∗‘𝑏) ∈ 𝐹) |
| 53 | 34, 27, 52, 46 | subgsubcld 33047 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → ((∗‘𝑏) − (∗‘𝑎)) ∈ 𝐹) |
| 54 | 28, 30, 53, 48 | subrgmcld 33237 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐)) ∈ 𝐹) |
| 55 | 34, 27, 11, 9 | subgsubcld 33047 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (𝑏 − 𝑎) ∈ 𝐹) |
| 56 | 28, 30, 55, 43 | subrgmcld 33237 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐))) ∈ 𝐹) |
| 57 | 34, 27, 54, 56 | subgsubcld 33047 |
. . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → ((((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐)) − ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐)))) ∈ 𝐹) |
| 58 | 5, 11 | sseldd 3984 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑏 ∈ ℂ) |
| 59 | 5, 9 | sseldd 3984 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑎 ∈ ℂ) |
| 60 | 58, 59 | cjsubd 32752 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (∗‘(𝑏 − 𝑎)) = ((∗‘𝑏) − (∗‘𝑎))) |
| 61 | 60 | oveq1d 7446 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → ((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐)) = (((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐))) |
| 62 | 5, 55 | sseldd 3984 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (𝑏 − 𝑎) ∈ ℂ) |
| 63 | 62 | cjcld 15235 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (∗‘(𝑏 − 𝑎)) ∈ ℂ) |
| 64 | 5, 48 | sseldd 3984 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (𝑑 − 𝑐) ∈ ℂ) |
| 65 | 63, 64 | cjmuld 15260 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) →
(∗‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) = ((∗‘(∗‘(𝑏 − 𝑎))) · (∗‘(𝑑 − 𝑐)))) |
| 66 | 62 | cjcjd 15238 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) →
(∗‘(∗‘(𝑏 − 𝑎))) = (𝑏 − 𝑎)) |
| 67 | 5, 15 | sseldd 3984 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑑 ∈ ℂ) |
| 68 | 5, 13 | sseldd 3984 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑐 ∈ ℂ) |
| 69 | 67, 68 | cjsubd 32752 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (∗‘(𝑑 − 𝑐)) = ((∗‘𝑑) − (∗‘𝑐))) |
| 70 | 66, 69 | oveq12d 7449 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) →
((∗‘(∗‘(𝑏 − 𝑎))) · (∗‘(𝑑 − 𝑐))) = ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐)))) |
| 71 | 65, 70 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) →
(∗‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) = ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐)))) |
| 72 | 61, 71 | oveq12d 7449 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐)) −
(∗‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐)))) = ((((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐)) − ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐))))) |
| 73 | 63, 64 | mulcld 11281 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → ((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐)) ∈ ℂ) |
| 74 | | imval2 15190 |
. . . . . . . . . . . . . . . . . 18
⊢
(((∗‘(𝑏
− 𝑎)) · (𝑑 − 𝑐)) ∈ ℂ →
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) = ((((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐)) −
(∗‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐)))) / (2 · i))) |
| 75 | 73, 74 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) →
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) = ((((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐)) −
(∗‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐)))) / (2 · i))) |
| 76 | 75 | neeq1d 3000 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) →
((ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0 ↔ ((((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐)) −
(∗‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐)))) / (2 · i)) ≠
0)) |
| 77 | 20, 76 | mpbid 232 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → ((((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐)) −
(∗‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐)))) / (2 · i)) ≠
0) |
| 78 | 73 | cjcld 15235 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) →
(∗‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ∈ ℂ) |
| 79 | 73, 78 | subcld 11620 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐)) −
(∗‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐)))) ∈ ℂ) |
| 80 | | 2cnd 12344 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 2 ∈
ℂ) |
| 81 | | ax-icn 11214 |
. . . . . . . . . . . . . . . . . 18
⊢ i ∈
ℂ |
| 82 | 81 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → i ∈
ℂ) |
| 83 | 80, 82 | mulcld 11281 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (2 · i) ∈
ℂ) |
| 84 | | 2cn 12341 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ∈
ℂ |
| 85 | | 2ne0 12370 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ≠
0 |
| 86 | | ine0 11698 |
. . . . . . . . . . . . . . . . . 18
⊢ i ≠
0 |
| 87 | 84, 81, 85, 86 | mulne0i 11906 |
. . . . . . . . . . . . . . . . 17
⊢ (2
· i) ≠ 0 |
| 88 | 87 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (2 · i) ≠
0) |
| 89 | 79, 83, 88 | divne0bd 12055 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → ((((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐)) −
(∗‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐)))) ≠ 0 ↔ ((((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐)) −
(∗‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐)))) / (2 · i)) ≠
0)) |
| 90 | 77, 89 | mpbird 257 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐)) −
(∗‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐)))) ≠ 0) |
| 91 | 72, 90 | eqnetrrd 3009 |
. . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → ((((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐)) − ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐)))) ≠ 0) |
| 92 | 31, 32, 33, 50, 57, 91 | sdrgdvcl 33301 |
. . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → ((((𝑎 − 𝑐) · ((∗‘𝑑) − (∗‘𝑐))) −
(((∗‘𝑎)
− (∗‘𝑐))
· (𝑑 − 𝑐))) / ((((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐)) − ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐))))) ∈ 𝐹) |
| 93 | 28, 30, 92, 55 | subrgmcld 33237 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (((((𝑎 − 𝑐) · ((∗‘𝑑) − (∗‘𝑐))) −
(((∗‘𝑎)
− (∗‘𝑐))
· (𝑑 − 𝑐))) / ((((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐)) − ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐))))) · (𝑏 − 𝑎)) ∈ 𝐹) |
| 94 | 23, 27, 9, 93 | subgcld 33046 |
. . . . . . . . . 10
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (𝑎 + (((((𝑎 − 𝑐) · ((∗‘𝑑) − (∗‘𝑐))) −
(((∗‘𝑎)
− (∗‘𝑐))
· (𝑑 − 𝑐))) / ((((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐)) − ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐))))) · (𝑏 − 𝑎))) ∈ 𝐹) |
| 95 | 22, 94 | eqeltrd 2841 |
. . . . . . . . 9
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑋 ∈ 𝐹) |
| 96 | 95 | orcd 874 |
. . . . . . . 8
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (𝑋 ∈ 𝐹 ∨ (𝐿[:]𝐾) = 2)) |
| 97 | 96 | r19.29an 3158 |
. . . . . . 7
⊢
(((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ ∃𝑟 ∈ ℝ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (𝑋 ∈ 𝐹 ∨ (𝐿[:]𝐾) = 2)) |
| 98 | 97 | r19.29an 3158 |
. . . . . 6
⊢
((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (𝑋 ∈ 𝐹 ∨ (𝐿[:]𝐾) = 2)) |
| 99 | 98 | r19.29an 3158 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ ∃𝑑 ∈ (𝐶‘𝑁)∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (𝑋 ∈ 𝐹 ∨ (𝐿[:]𝐾) = 2)) |
| 100 | 99 | r19.29an 3158 |
. . . 4
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ ∃𝑐 ∈ (𝐶‘𝑁)∃𝑑 ∈ (𝐶‘𝑁)∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (𝑋 ∈ 𝐹 ∨ (𝐿[:]𝐾) = 2)) |
| 101 | 100 | r19.29an 3158 |
. . 3
⊢ (((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ ∃𝑏 ∈ (𝐶‘𝑁)∃𝑐 ∈ (𝐶‘𝑁)∃𝑑 ∈ (𝐶‘𝑁)∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (𝑋 ∈ 𝐹 ∨ (𝐿[:]𝐾) = 2)) |
| 102 | 101 | r19.29an 3158 |
. 2
⊢ ((𝜑 ∧ ∃𝑎 ∈ (𝐶‘𝑁)∃𝑏 ∈ (𝐶‘𝑁)∃𝑐 ∈ (𝐶‘𝑁)∃𝑑 ∈ (𝐶‘𝑁)∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (𝑋 ∈ 𝐹 ∨ (𝐿[:]𝐾) = 2)) |
| 103 | 36, 37 | constrsscn 33781 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐶‘𝑁) ⊆ ℂ) |
| 104 | 103 | ad8antr 740 |
. . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 = 𝑏) → (𝐶‘𝑁) ⊆ ℂ) |
| 105 | | simp-8r 792 |
. . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 = 𝑏) → 𝑎 ∈ (𝐶‘𝑁)) |
| 106 | | simp-7r 790 |
. . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 = 𝑏) → 𝑏 ∈ (𝐶‘𝑁)) |
| 107 | | simp-6r 788 |
. . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 = 𝑏) → 𝑐 ∈ (𝐶‘𝑁)) |
| 108 | | simp-5r 786 |
. . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 = 𝑏) → 𝑒 ∈ (𝐶‘𝑁)) |
| 109 | | simp-4r 784 |
. . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 = 𝑏) → 𝑓 ∈ (𝐶‘𝑁)) |
| 110 | | simpllr 776 |
. . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 = 𝑏) → 𝑡 ∈ ℝ) |
| 111 | | simplrl 777 |
. . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 = 𝑏) → 𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎)))) |
| 112 | | simplrr 778 |
. . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 = 𝑏) → (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓))) |
| 113 | | simpr 484 |
. . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 = 𝑏) → 𝑎 = 𝑏) |
| 114 | 104, 105,
106, 107, 108, 109, 110, 111, 112, 113 | constrrtlc2 33774 |
. . . . . . . . . . 11
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 = 𝑏) → 𝑋 = 𝑎) |
| 115 | 6 | ad8antr 740 |
. . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 = 𝑏) → (𝐶‘𝑁) ⊆ 𝐹) |
| 116 | 115, 105 | sseldd 3984 |
. . . . . . . . . . 11
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 = 𝑏) → 𝑎 ∈ 𝐹) |
| 117 | 114, 116 | eqeltrd 2841 |
. . . . . . . . . 10
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 = 𝑏) → 𝑋 ∈ 𝐹) |
| 118 | 117 | orcd 874 |
. . . . . . . . 9
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 = 𝑏) → (𝑋 ∈ 𝐹 ∨ (𝐿[:]𝐾) = 2)) |
| 119 | | constrelextdg2.k |
. . . . . . . . . 10
⊢ 𝐾 = (ℂfld
↾s 𝐹) |
| 120 | | constrelextdg2.l |
. . . . . . . . . 10
⊢ 𝐿 = (ℂfld
↾s (ℂfld fldGen (𝐹 ∪ {𝑋}))) |
| 121 | | eqid 2737 |
. . . . . . . . . 10
⊢
(Poly1‘𝐾) = (Poly1‘𝐾) |
| 122 | | eqid 2737 |
. . . . . . . . . 10
⊢
(.g‘(mulGrp‘ℂfld)) =
(.g‘(mulGrp‘ℂfld)) |
| 123 | | cnfldfld 33371 |
. . . . . . . . . . 11
⊢
ℂfld ∈ Field |
| 124 | 123 | a1i 11 |
. . . . . . . . . 10
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → ℂfld ∈
Field) |
| 125 | 1 | ad8antr 740 |
. . . . . . . . . 10
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → 𝐹 ∈
(SubDRing‘ℂfld)) |
| 126 | | constrelextdg2.x |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑋 ∈ (𝐶‘suc 𝑁)) |
| 127 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢ (𝐶‘𝑁) = (𝐶‘𝑁) |
| 128 | 36, 37, 127 | constrsuc 33779 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑋 ∈ (𝐶‘suc 𝑁) ↔ (𝑋 ∈ ℂ ∧ (∃𝑎 ∈ (𝐶‘𝑁)∃𝑏 ∈ (𝐶‘𝑁)∃𝑐 ∈ (𝐶‘𝑁)∃𝑑 ∈ (𝐶‘𝑁)∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ (𝐶‘𝑁)∃𝑏 ∈ (𝐶‘𝑁)∃𝑐 ∈ (𝐶‘𝑁)∃𝑒 ∈ (𝐶‘𝑁)∃𝑓 ∈ (𝐶‘𝑁)∃𝑡 ∈ ℝ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ (𝐶‘𝑁)∃𝑏 ∈ (𝐶‘𝑁)∃𝑐 ∈ (𝐶‘𝑁)∃𝑑 ∈ (𝐶‘𝑁)∃𝑒 ∈ (𝐶‘𝑁)∃𝑓 ∈ (𝐶‘𝑁)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓))))))) |
| 129 | 126, 128 | mpbid 232 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑋 ∈ ℂ ∧ (∃𝑎 ∈ (𝐶‘𝑁)∃𝑏 ∈ (𝐶‘𝑁)∃𝑐 ∈ (𝐶‘𝑁)∃𝑑 ∈ (𝐶‘𝑁)∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ (𝐶‘𝑁)∃𝑏 ∈ (𝐶‘𝑁)∃𝑐 ∈ (𝐶‘𝑁)∃𝑒 ∈ (𝐶‘𝑁)∃𝑓 ∈ (𝐶‘𝑁)∃𝑡 ∈ ℝ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ (𝐶‘𝑁)∃𝑏 ∈ (𝐶‘𝑁)∃𝑐 ∈ (𝐶‘𝑁)∃𝑑 ∈ (𝐶‘𝑁)∃𝑒 ∈ (𝐶‘𝑁)∃𝑓 ∈ (𝐶‘𝑁)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))))) |
| 130 | 129 | simpld 494 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈ ℂ) |
| 131 | 130 | ad8antr 740 |
. . . . . . . . . 10
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → 𝑋 ∈ ℂ) |
| 132 | 26 | ad8antr 740 |
. . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → 𝐹 ∈
(SubGrp‘ℂfld)) |
| 133 | 6 | ad8antr 740 |
. . . . . . . . . . . . . . 15
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → (𝐶‘𝑁) ⊆ 𝐹) |
| 134 | 37 | ad8antr 740 |
. . . . . . . . . . . . . . . 16
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → 𝑁 ∈ On) |
| 135 | | simp-8r 792 |
. . . . . . . . . . . . . . . 16
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → 𝑎 ∈ (𝐶‘𝑁)) |
| 136 | 36, 134, 135 | constrconj 33786 |
. . . . . . . . . . . . . . 15
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → (∗‘𝑎) ∈ (𝐶‘𝑁)) |
| 137 | 133, 136 | sseldd 3984 |
. . . . . . . . . . . . . 14
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → (∗‘𝑎) ∈ 𝐹) |
| 138 | 125, 24 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → 𝐹 ∈
(SubRing‘ℂfld)) |
| 139 | 133, 135 | sseldd 3984 |
. . . . . . . . . . . . . . 15
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → 𝑎 ∈ 𝐹) |
| 140 | | simp-7r 790 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → 𝑏 ∈ (𝐶‘𝑁)) |
| 141 | 36, 134, 140 | constrconj 33786 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → (∗‘𝑏) ∈ (𝐶‘𝑁)) |
| 142 | 133, 141 | sseldd 3984 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → (∗‘𝑏) ∈ 𝐹) |
| 143 | 34, 132, 142, 137 | subgsubcld 33047 |
. . . . . . . . . . . . . . . 16
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → ((∗‘𝑏) − (∗‘𝑎)) ∈ 𝐹) |
| 144 | 133, 140 | sseldd 3984 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → 𝑏 ∈ 𝐹) |
| 145 | 34, 132, 144, 139 | subgsubcld 33047 |
. . . . . . . . . . . . . . . 16
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → (𝑏 − 𝑎) ∈ 𝐹) |
| 146 | 103 | ad8antr 740 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → (𝐶‘𝑁) ⊆ ℂ) |
| 147 | 146, 140 | sseldd 3984 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → 𝑏 ∈ ℂ) |
| 148 | 146, 135 | sseldd 3984 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → 𝑎 ∈ ℂ) |
| 149 | | simpr 484 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → 𝑎 ≠ 𝑏) |
| 150 | 149 | necomd 2996 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → 𝑏 ≠ 𝑎) |
| 151 | 147, 148,
150 | subne0d 11629 |
. . . . . . . . . . . . . . . 16
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → (𝑏 − 𝑎) ≠ 0) |
| 152 | 31, 32, 125, 143, 145, 151 | sdrgdvcl 33301 |
. . . . . . . . . . . . . . 15
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)) ∈ 𝐹) |
| 153 | 28, 138, 139, 152 | subrgmcld 33237 |
. . . . . . . . . . . . . 14
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) ∈ 𝐹) |
| 154 | 34, 132, 137, 153 | subgsubcld 33047 |
. . . . . . . . . . . . 13
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → ((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) ∈ 𝐹) |
| 155 | | simp-6r 788 |
. . . . . . . . . . . . . . 15
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → 𝑐 ∈ (𝐶‘𝑁)) |
| 156 | 36, 134, 155 | constrconj 33786 |
. . . . . . . . . . . . . 14
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → (∗‘𝑐) ∈ (𝐶‘𝑁)) |
| 157 | 133, 156 | sseldd 3984 |
. . . . . . . . . . . . 13
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → (∗‘𝑐) ∈ 𝐹) |
| 158 | 34, 132, 154, 157 | subgsubcld 33047 |
. . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) ∈ 𝐹) |
| 159 | 133, 155 | sseldd 3984 |
. . . . . . . . . . . . 13
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → 𝑐 ∈ 𝐹) |
| 160 | 28, 138, 159, 152 | subrgmcld 33237 |
. . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) ∈ 𝐹) |
| 161 | 34, 132, 158, 160 | subgsubcld 33047 |
. . . . . . . . . . 11
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → ((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) ∈ 𝐹) |
| 162 | | simp-5r 786 |
. . . . . . . . . . . . 13
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → 𝑒 ∈ (𝐶‘𝑁)) |
| 163 | | simp-4r 784 |
. . . . . . . . . . . . 13
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → 𝑓 ∈ (𝐶‘𝑁)) |
| 164 | | simpllr 776 |
. . . . . . . . . . . . 13
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → 𝑡 ∈ ℝ) |
| 165 | | simplrl 777 |
. . . . . . . . . . . . 13
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → 𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎)))) |
| 166 | | simplrr 778 |
. . . . . . . . . . . . 13
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓))) |
| 167 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(((∗‘𝑏)
− (∗‘𝑎))
/ (𝑏 − 𝑎)) = (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)) |
| 168 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) = (((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) |
| 169 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ (-((𝑐 ·
(((∗‘𝑎)
− (𝑎 ·
(((∗‘𝑏)
− (∗‘𝑎))
/ (𝑏 − 𝑎)))) −
(∗‘𝑐))) +
((𝑒 − 𝑓) ·
((∗‘𝑒) −
(∗‘𝑓)))) /
(((∗‘𝑏)
− (∗‘𝑎))
/ (𝑏 − 𝑎))) = (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) |
| 170 | 146, 135,
140, 155, 162, 163, 164, 165, 166, 167, 168, 169, 149 | constrrtlc1 33773 |
. . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → (((𝑋↑2) + (((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) · 𝑋) + (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))))) = 0 ∧ (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)) ≠ 0)) |
| 171 | 170 | simprd 495 |
. . . . . . . . . . 11
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)) ≠ 0) |
| 172 | 31, 32, 125, 161, 152, 171 | sdrgdvcl 33301 |
. . . . . . . . . 10
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → (((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) ∈ 𝐹) |
| 173 | | df-neg 11495 |
. . . . . . . . . . . 12
⊢ -((𝑐 ·
(((∗‘𝑎)
− (𝑎 ·
(((∗‘𝑏)
− (∗‘𝑎))
/ (𝑏 − 𝑎)))) −
(∗‘𝑐))) +
((𝑒 − 𝑓) ·
((∗‘𝑒) −
(∗‘𝑓)))) = (0
− ((𝑐 ·
(((∗‘𝑎)
− (𝑎 ·
(((∗‘𝑏)
− (∗‘𝑎))
/ (𝑏 − 𝑎)))) −
(∗‘𝑐))) +
((𝑒 − 𝑓) ·
((∗‘𝑒) −
(∗‘𝑓))))) |
| 174 | 36, 134 | constr01 33783 |
. . . . . . . . . . . . . . 15
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → {0, 1} ⊆ (𝐶‘𝑁)) |
| 175 | 32 | fvexi 6920 |
. . . . . . . . . . . . . . . . 17
⊢ 0 ∈
V |
| 176 | 175 | prid1 4762 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
{0, 1} |
| 177 | 176 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → 0 ∈ {0, 1}) |
| 178 | 174, 177 | sseldd 3984 |
. . . . . . . . . . . . . 14
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → 0 ∈ (𝐶‘𝑁)) |
| 179 | 133, 178 | sseldd 3984 |
. . . . . . . . . . . . 13
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → 0 ∈ 𝐹) |
| 180 | 28, 138, 159, 158 | subrgmcld 33237 |
. . . . . . . . . . . . . 14
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → (𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) ∈ 𝐹) |
| 181 | 133, 162 | sseldd 3984 |
. . . . . . . . . . . . . . . 16
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → 𝑒 ∈ 𝐹) |
| 182 | 133, 163 | sseldd 3984 |
. . . . . . . . . . . . . . . 16
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → 𝑓 ∈ 𝐹) |
| 183 | 34, 132, 181, 182 | subgsubcld 33047 |
. . . . . . . . . . . . . . 15
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → (𝑒 − 𝑓) ∈ 𝐹) |
| 184 | 36, 134, 162 | constrconj 33786 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → (∗‘𝑒) ∈ (𝐶‘𝑁)) |
| 185 | 133, 184 | sseldd 3984 |
. . . . . . . . . . . . . . . 16
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → (∗‘𝑒) ∈ 𝐹) |
| 186 | 36, 134, 163 | constrconj 33786 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → (∗‘𝑓) ∈ (𝐶‘𝑁)) |
| 187 | 133, 186 | sseldd 3984 |
. . . . . . . . . . . . . . . 16
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → (∗‘𝑓) ∈ 𝐹) |
| 188 | 34, 132, 185, 187 | subgsubcld 33047 |
. . . . . . . . . . . . . . 15
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → ((∗‘𝑒) − (∗‘𝑓)) ∈ 𝐹) |
| 189 | 28, 138, 183, 188 | subrgmcld 33237 |
. . . . . . . . . . . . . 14
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓))) ∈ 𝐹) |
| 190 | 23, 132, 180, 189 | subgcld 33046 |
. . . . . . . . . . . . 13
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → ((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) ∈ 𝐹) |
| 191 | 34, 132, 179, 190 | subgsubcld 33047 |
. . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → (0 − ((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓))))) ∈ 𝐹) |
| 192 | 173, 191 | eqeltrid 2845 |
. . . . . . . . . . 11
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → -((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) ∈ 𝐹) |
| 193 | 31, 32, 125, 192, 152, 171 | sdrgdvcl 33301 |
. . . . . . . . . 10
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) ∈ 𝐹) |
| 194 | | 2nn0 12543 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℕ0 |
| 195 | 194 | a1i 11 |
. . . . . . . . . . . . 13
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → 2 ∈
ℕ0) |
| 196 | | cnfldexp 21417 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ∈ ℂ ∧ 2 ∈
ℕ0) →
(2(.g‘(mulGrp‘ℂfld))𝑋) = (𝑋↑2)) |
| 197 | 131, 195,
196 | syl2anc 584 |
. . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) →
(2(.g‘(mulGrp‘ℂfld))𝑋) = (𝑋↑2)) |
| 198 | 197 | oveq1d 7446 |
. . . . . . . . . . 11
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) →
((2(.g‘(mulGrp‘ℂfld))𝑋) + (((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) · 𝑋) + (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))))) = ((𝑋↑2) + (((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) · 𝑋) + (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))))) |
| 199 | 170 | simpld 494 |
. . . . . . . . . . 11
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → ((𝑋↑2) + (((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) · 𝑋) + (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))))) = 0) |
| 200 | 198, 199 | eqtrd 2777 |
. . . . . . . . . 10
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) →
((2(.g‘(mulGrp‘ℂfld))𝑋) + (((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) · 𝑋) + (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))))) = 0) |
| 201 | 119, 120,
32, 121, 2, 28, 23, 122, 124, 125, 131, 172, 193, 200 | rtelextdg2 33768 |
. . . . . . . . 9
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → (𝑋 ∈ 𝐹 ∨ (𝐿[:]𝐾) = 2)) |
| 202 | | exmidne 2950 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑏 ∨ 𝑎 ≠ 𝑏) |
| 203 | 202 | a1i 11 |
. . . . . . . . 9
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (𝑎 = 𝑏 ∨ 𝑎 ≠ 𝑏)) |
| 204 | 118, 201,
203 | mpjaodan 961 |
. . . . . . . 8
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (𝑋 ∈ 𝐹 ∨ (𝐿[:]𝐾) = 2)) |
| 205 | 204 | r19.29an 3158 |
. . . . . . 7
⊢
(((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ ∃𝑡 ∈ ℝ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (𝑋 ∈ 𝐹 ∨ (𝐿[:]𝐾) = 2)) |
| 206 | 205 | r19.29an 3158 |
. . . . . 6
⊢
((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ ∃𝑓 ∈ (𝐶‘𝑁)∃𝑡 ∈ ℝ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (𝑋 ∈ 𝐹 ∨ (𝐿[:]𝐾) = 2)) |
| 207 | 206 | r19.29an 3158 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ ∃𝑒 ∈ (𝐶‘𝑁)∃𝑓 ∈ (𝐶‘𝑁)∃𝑡 ∈ ℝ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (𝑋 ∈ 𝐹 ∨ (𝐿[:]𝐾) = 2)) |
| 208 | 207 | r19.29an 3158 |
. . . 4
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ ∃𝑐 ∈ (𝐶‘𝑁)∃𝑒 ∈ (𝐶‘𝑁)∃𝑓 ∈ (𝐶‘𝑁)∃𝑡 ∈ ℝ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (𝑋 ∈ 𝐹 ∨ (𝐿[:]𝐾) = 2)) |
| 209 | 208 | r19.29an 3158 |
. . 3
⊢ (((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ ∃𝑏 ∈ (𝐶‘𝑁)∃𝑐 ∈ (𝐶‘𝑁)∃𝑒 ∈ (𝐶‘𝑁)∃𝑓 ∈ (𝐶‘𝑁)∃𝑡 ∈ ℝ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (𝑋 ∈ 𝐹 ∨ (𝐿[:]𝐾) = 2)) |
| 210 | 209 | r19.29an 3158 |
. 2
⊢ ((𝜑 ∧ ∃𝑎 ∈ (𝐶‘𝑁)∃𝑏 ∈ (𝐶‘𝑁)∃𝑐 ∈ (𝐶‘𝑁)∃𝑒 ∈ (𝐶‘𝑁)∃𝑓 ∈ (𝐶‘𝑁)∃𝑡 ∈ ℝ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (𝑋 ∈ 𝐹 ∨ (𝐿[:]𝐾) = 2)) |
| 211 | 123 | a1i 11 |
. . . . . . . . 9
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ℂfld ∈
Field) |
| 212 | 1 | ad7antr 738 |
. . . . . . . . 9
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝐹 ∈
(SubDRing‘ℂfld)) |
| 213 | 130 | ad7antr 738 |
. . . . . . . . 9
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑋 ∈ ℂ) |
| 214 | 212, 24, 25 | 3syl 18 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝐹 ∈
(SubGrp‘ℂfld)) |
| 215 | 212, 24 | syl 17 |
. . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝐹 ∈
(SubRing‘ℂfld)) |
| 216 | 6 | ad7antr 738 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (𝐶‘𝑁) ⊆ 𝐹) |
| 217 | | simpllr 776 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑒 ∈ (𝐶‘𝑁)) |
| 218 | 216, 217 | sseldd 3984 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑒 ∈ 𝐹) |
| 219 | | simplr 769 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑓 ∈ (𝐶‘𝑁)) |
| 220 | 216, 219 | sseldd 3984 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑓 ∈ 𝐹) |
| 221 | 34, 214, 218, 220 | subgsubcld 33047 |
. . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (𝑒 − 𝑓) ∈ 𝐹) |
| 222 | 103 | ad7antr 738 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (𝐶‘𝑁) ⊆ ℂ) |
| 223 | 222, 217 | sseldd 3984 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑒 ∈ ℂ) |
| 224 | 222, 219 | sseldd 3984 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑓 ∈ ℂ) |
| 225 | 223, 224 | cjsubd 32752 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (∗‘(𝑒 − 𝑓)) = ((∗‘𝑒) − (∗‘𝑓))) |
| 226 | 37 | ad7antr 738 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑁 ∈ On) |
| 227 | 36, 226, 217 | constrconj 33786 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (∗‘𝑒) ∈ (𝐶‘𝑁)) |
| 228 | 216, 227 | sseldd 3984 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (∗‘𝑒) ∈ 𝐹) |
| 229 | 36, 226, 219 | constrconj 33786 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (∗‘𝑓) ∈ (𝐶‘𝑁)) |
| 230 | 216, 229 | sseldd 3984 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (∗‘𝑓) ∈ 𝐹) |
| 231 | 34, 214, 228, 230 | subgsubcld 33047 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((∗‘𝑒) − (∗‘𝑓)) ∈ 𝐹) |
| 232 | 225, 231 | eqeltrd 2841 |
. . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (∗‘(𝑒 − 𝑓)) ∈ 𝐹) |
| 233 | 28, 215, 221, 232 | subrgmcld 33237 |
. . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) ∈ 𝐹) |
| 234 | | simp-4r 784 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑑 ∈ (𝐶‘𝑁)) |
| 235 | 36, 226, 234 | constrconj 33786 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (∗‘𝑑) ∈ (𝐶‘𝑁)) |
| 236 | 216, 235 | sseldd 3984 |
. . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (∗‘𝑑) ∈ 𝐹) |
| 237 | 216, 234 | sseldd 3984 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑑 ∈ 𝐹) |
| 238 | | simp-7r 790 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑎 ∈ (𝐶‘𝑁)) |
| 239 | 216, 238 | sseldd 3984 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑎 ∈ 𝐹) |
| 240 | 23, 214, 237, 239 | subgcld 33046 |
. . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (𝑑 + 𝑎) ∈ 𝐹) |
| 241 | 28, 215, 236, 240 | subrgmcld 33237 |
. . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((∗‘𝑑) · (𝑑 + 𝑎)) ∈ 𝐹) |
| 242 | 34, 214, 233, 241 | subgsubcld 33047 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) ∈ 𝐹) |
| 243 | | simp-6r 788 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑏 ∈ (𝐶‘𝑁)) |
| 244 | 216, 243 | sseldd 3984 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑏 ∈ 𝐹) |
| 245 | | simp-5r 786 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑐 ∈ (𝐶‘𝑁)) |
| 246 | 216, 245 | sseldd 3984 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑐 ∈ 𝐹) |
| 247 | 34, 214, 244, 246 | subgsubcld 33047 |
. . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (𝑏 − 𝑐) ∈ 𝐹) |
| 248 | 222, 243 | sseldd 3984 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑏 ∈ ℂ) |
| 249 | 222, 245 | sseldd 3984 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑐 ∈ ℂ) |
| 250 | 248, 249 | cjsubd 32752 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (∗‘(𝑏 − 𝑐)) = ((∗‘𝑏) − (∗‘𝑐))) |
| 251 | 36, 226, 243 | constrconj 33786 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (∗‘𝑏) ∈ (𝐶‘𝑁)) |
| 252 | 216, 251 | sseldd 3984 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (∗‘𝑏) ∈ 𝐹) |
| 253 | 36, 226, 245 | constrconj 33786 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (∗‘𝑐) ∈ (𝐶‘𝑁)) |
| 254 | 216, 253 | sseldd 3984 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (∗‘𝑐) ∈ 𝐹) |
| 255 | 34, 214, 252, 254 | subgsubcld 33047 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((∗‘𝑏) − (∗‘𝑐)) ∈ 𝐹) |
| 256 | 250, 255 | eqeltrd 2841 |
. . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (∗‘(𝑏 − 𝑐)) ∈ 𝐹) |
| 257 | 28, 215, 247, 256 | subrgmcld 33237 |
. . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) ∈ 𝐹) |
| 258 | 36, 226, 238 | constrconj 33786 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (∗‘𝑎) ∈ (𝐶‘𝑁)) |
| 259 | 216, 258 | sseldd 3984 |
. . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (∗‘𝑎) ∈ 𝐹) |
| 260 | 28, 215, 259, 240 | subrgmcld 33237 |
. . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((∗‘𝑎) · (𝑑 + 𝑎)) ∈ 𝐹) |
| 261 | 34, 214, 257, 260 | subgsubcld 33047 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎))) ∈ 𝐹) |
| 262 | 34, 214, 242, 261 | subgsubcld 33047 |
. . . . . . . . . 10
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) ∈ 𝐹) |
| 263 | 34, 214, 236, 259 | subgsubcld 33047 |
. . . . . . . . . 10
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((∗‘𝑑) − (∗‘𝑎)) ∈ 𝐹) |
| 264 | 222, 234 | sseldd 3984 |
. . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑑 ∈ ℂ) |
| 265 | 222, 238 | sseldd 3984 |
. . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑎 ∈ ℂ) |
| 266 | 264, 265 | cjsubd 32752 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (∗‘(𝑑 − 𝑎)) = ((∗‘𝑑) − (∗‘𝑎))) |
| 267 | 264, 265 | subcld 11620 |
. . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (𝑑 − 𝑎) ∈ ℂ) |
| 268 | | simpr1 1195 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑎 ≠ 𝑑) |
| 269 | 268 | necomd 2996 |
. . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑑 ≠ 𝑎) |
| 270 | 264, 265,
269 | subne0d 11629 |
. . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (𝑑 − 𝑎) ≠ 0) |
| 271 | 267, 270 | cjne0d 15242 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (∗‘(𝑑 − 𝑎)) ≠ 0) |
| 272 | 266, 271 | eqnetrrd 3009 |
. . . . . . . . . 10
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((∗‘𝑑) − (∗‘𝑎)) ≠ 0) |
| 273 | 31, 32, 212, 262, 263, 272 | sdrgdvcl 33301 |
. . . . . . . . 9
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) ∈ 𝐹) |
| 274 | | df-neg 11495 |
. . . . . . . . . 10
⊢
-(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎))) = (0 − (((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎)))) |
| 275 | 36, 226 | constr01 33783 |
. . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → {0, 1} ⊆ (𝐶‘𝑁)) |
| 276 | 176 | a1i 11 |
. . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 0 ∈ {0, 1}) |
| 277 | 275, 276 | sseldd 3984 |
. . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 0 ∈ (𝐶‘𝑁)) |
| 278 | 216, 277 | sseldd 3984 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 0 ∈ 𝐹) |
| 279 | 28, 215, 237, 239 | subrgmcld 33237 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (𝑑 · 𝑎) ∈ 𝐹) |
| 280 | 28, 215, 259, 279 | subrgmcld 33237 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((∗‘𝑎) · (𝑑 · 𝑎)) ∈ 𝐹) |
| 281 | 28, 215, 257, 237 | subrgmcld 33237 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑) ∈ 𝐹) |
| 282 | 34, 214, 280, 281 | subgsubcld 33047 |
. . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) ∈ 𝐹) |
| 283 | 28, 215, 236, 279 | subrgmcld 33237 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((∗‘𝑑) · (𝑑 · 𝑎)) ∈ 𝐹) |
| 284 | 28, 215, 233, 239 | subrgmcld 33237 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎) ∈ 𝐹) |
| 285 | 34, 214, 283, 284 | subgsubcld 33047 |
. . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎)) ∈ 𝐹) |
| 286 | 34, 214, 282, 285 | subgsubcld 33047 |
. . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) ∈ 𝐹) |
| 287 | 31, 32, 212, 286, 263, 272 | sdrgdvcl 33301 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎))) ∈ 𝐹) |
| 288 | 34, 214, 278, 287 | subgsubcld 33047 |
. . . . . . . . . 10
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (0 −
(((((∗‘𝑎)
· (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎)))) ∈ 𝐹) |
| 289 | 274, 288 | eqeltrid 2845 |
. . . . . . . . 9
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎))) ∈ 𝐹) |
| 290 | 213, 194,
196 | sylancl 586 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) →
(2(.g‘(mulGrp‘ℂfld))𝑋) = (𝑋↑2)) |
| 291 | 290 | oveq1d 7446 |
. . . . . . . . . 10
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) →
((2(.g‘(mulGrp‘ℂfld))𝑋) + (((((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) · 𝑋) + -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎))))) = ((𝑋↑2) + (((((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) · 𝑋) + -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎)))))) |
| 292 | | simpr2 1196 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐))) |
| 293 | | simpr3 1197 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓))) |
| 294 | | eqid 2737 |
. . . . . . . . . . 11
⊢ ((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) = ((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) |
| 295 | | eqid 2737 |
. . . . . . . . . . 11
⊢ ((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) = ((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) |
| 296 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(((((𝑒 − 𝑓) ·
(∗‘(𝑒 −
𝑓))) −
((∗‘𝑑)
· (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) = (((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) |
| 297 | | eqid 2737 |
. . . . . . . . . . 11
⊢
-(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎))) = -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎))) |
| 298 | 222, 238,
243, 245, 234, 217, 219, 213, 268, 292, 293, 294, 295, 296, 297 | constrrtcc 33776 |
. . . . . . . . . 10
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((𝑋↑2) + (((((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) · 𝑋) + -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎))))) = 0) |
| 299 | 291, 298 | eqtrd 2777 |
. . . . . . . . 9
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) →
((2(.g‘(mulGrp‘ℂfld))𝑋) + (((((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) · 𝑋) + -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎))))) = 0) |
| 300 | 119, 120,
32, 121, 2, 28, 23, 122, 211, 212, 213, 273, 289, 299 | rtelextdg2 33768 |
. . . . . . . 8
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (𝑋 ∈ 𝐹 ∨ (𝐿[:]𝐾) = 2)) |
| 301 | 300 | r19.29an 3158 |
. . . . . . 7
⊢
(((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ ∃𝑓 ∈ (𝐶‘𝑁)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (𝑋 ∈ 𝐹 ∨ (𝐿[:]𝐾) = 2)) |
| 302 | 301 | r19.29an 3158 |
. . . . . 6
⊢
((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ ∃𝑒 ∈ (𝐶‘𝑁)∃𝑓 ∈ (𝐶‘𝑁)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (𝑋 ∈ 𝐹 ∨ (𝐿[:]𝐾) = 2)) |
| 303 | 302 | r19.29an 3158 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ ∃𝑑 ∈ (𝐶‘𝑁)∃𝑒 ∈ (𝐶‘𝑁)∃𝑓 ∈ (𝐶‘𝑁)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (𝑋 ∈ 𝐹 ∨ (𝐿[:]𝐾) = 2)) |
| 304 | 303 | r19.29an 3158 |
. . . 4
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ ∃𝑐 ∈ (𝐶‘𝑁)∃𝑑 ∈ (𝐶‘𝑁)∃𝑒 ∈ (𝐶‘𝑁)∃𝑓 ∈ (𝐶‘𝑁)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (𝑋 ∈ 𝐹 ∨ (𝐿[:]𝐾) = 2)) |
| 305 | 304 | r19.29an 3158 |
. . 3
⊢ (((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ ∃𝑏 ∈ (𝐶‘𝑁)∃𝑐 ∈ (𝐶‘𝑁)∃𝑑 ∈ (𝐶‘𝑁)∃𝑒 ∈ (𝐶‘𝑁)∃𝑓 ∈ (𝐶‘𝑁)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (𝑋 ∈ 𝐹 ∨ (𝐿[:]𝐾) = 2)) |
| 306 | 305 | r19.29an 3158 |
. 2
⊢ ((𝜑 ∧ ∃𝑎 ∈ (𝐶‘𝑁)∃𝑏 ∈ (𝐶‘𝑁)∃𝑐 ∈ (𝐶‘𝑁)∃𝑑 ∈ (𝐶‘𝑁)∃𝑒 ∈ (𝐶‘𝑁)∃𝑓 ∈ (𝐶‘𝑁)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (𝑋 ∈ 𝐹 ∨ (𝐿[:]𝐾) = 2)) |
| 307 | 129 | simprd 495 |
. 2
⊢ (𝜑 → (∃𝑎 ∈ (𝐶‘𝑁)∃𝑏 ∈ (𝐶‘𝑁)∃𝑐 ∈ (𝐶‘𝑁)∃𝑑 ∈ (𝐶‘𝑁)∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ (𝐶‘𝑁)∃𝑏 ∈ (𝐶‘𝑁)∃𝑐 ∈ (𝐶‘𝑁)∃𝑒 ∈ (𝐶‘𝑁)∃𝑓 ∈ (𝐶‘𝑁)∃𝑡 ∈ ℝ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ (𝐶‘𝑁)∃𝑏 ∈ (𝐶‘𝑁)∃𝑐 ∈ (𝐶‘𝑁)∃𝑑 ∈ (𝐶‘𝑁)∃𝑒 ∈ (𝐶‘𝑁)∃𝑓 ∈ (𝐶‘𝑁)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓))))) |
| 308 | 102, 210,
306, 307 | mpjao3dan 1434 |
1
⊢ (𝜑 → (𝑋 ∈ 𝐹 ∨ (𝐿[:]𝐾) = 2)) |