Proof of Theorem constrelextdg2
Step | Hyp | Ref
| Expression |
1 | | constrelextdg2.f |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 ∈
(SubDRing‘ℂfld)) |
2 | | cnfldbas 21391 |
. . . . . . . . . . . . . 14
⊢ ℂ =
(Base‘ℂfld) |
3 | 2 | sdrgss 20816 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈
(SubDRing‘ℂfld) → 𝐹 ⊆ ℂ) |
4 | 1, 3 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 ⊆ ℂ) |
5 | 4 | ad7antr 737 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝐹 ⊆ ℂ) |
6 | | constrelextdg2.1 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐶‘𝑁) ⊆ 𝐹) |
7 | 6 | ad7antr 737 |
. . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (𝐶‘𝑁) ⊆ 𝐹) |
8 | | simp-7r 789 |
. . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑎 ∈ (𝐶‘𝑁)) |
9 | 7, 8 | sseldd 4009 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑎 ∈ 𝐹) |
10 | | simp-6r 787 |
. . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑏 ∈ (𝐶‘𝑁)) |
11 | 7, 10 | sseldd 4009 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑏 ∈ 𝐹) |
12 | | simp-5r 785 |
. . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑐 ∈ (𝐶‘𝑁)) |
13 | 7, 12 | sseldd 4009 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑐 ∈ 𝐹) |
14 | | simp-4r 783 |
. . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑑 ∈ (𝐶‘𝑁)) |
15 | 7, 14 | sseldd 4009 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑑 ∈ 𝐹) |
16 | | simpllr 775 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑡 ∈ ℝ) |
17 | | simplr 768 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑟 ∈ ℝ) |
18 | | simpr1 1194 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎)))) |
19 | | simpr2 1195 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐)))) |
20 | | simpr3 1196 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) →
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) |
21 | | eqid 2740 |
. . . . . . . . . . 11
⊢ (𝑎 + (((((𝑎 − 𝑐) · ((∗‘𝑑) − (∗‘𝑐))) −
(((∗‘𝑎)
− (∗‘𝑐))
· (𝑑 − 𝑐))) / ((((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐)) − ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐))))) · (𝑏 − 𝑎))) = (𝑎 + (((((𝑎 − 𝑐) · ((∗‘𝑑) − (∗‘𝑐))) −
(((∗‘𝑎)
− (∗‘𝑐))
· (𝑑 − 𝑐))) / ((((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐)) − ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐))))) · (𝑏 − 𝑎))) |
22 | 5, 9, 11, 13, 15, 16, 17, 18, 19, 20, 21 | constrrtll 33722 |
. . . . . . . . . 10
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑋 = (𝑎 + (((((𝑎 − 𝑐) · ((∗‘𝑑) − (∗‘𝑐))) −
(((∗‘𝑎)
− (∗‘𝑐))
· (𝑑 − 𝑐))) / ((((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐)) − ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐))))) · (𝑏 − 𝑎)))) |
23 | | cnfldadd 21393 |
. . . . . . . . . . 11
⊢ + =
(+g‘ℂfld) |
24 | | sdrgsubrg 20814 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈
(SubDRing‘ℂfld) → 𝐹 ∈
(SubRing‘ℂfld)) |
25 | | subrgsubg 20605 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈
(SubRing‘ℂfld) → 𝐹 ∈
(SubGrp‘ℂfld)) |
26 | 1, 24, 25 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 ∈
(SubGrp‘ℂfld)) |
27 | 26 | ad7antr 737 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝐹 ∈
(SubGrp‘ℂfld)) |
28 | | cnfldmul 21395 |
. . . . . . . . . . . 12
⊢ ·
= (.r‘ℂfld) |
29 | 1, 24 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 ∈
(SubRing‘ℂfld)) |
30 | 29 | ad7antr 737 |
. . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝐹 ∈
(SubRing‘ℂfld)) |
31 | | cnflddiv 21436 |
. . . . . . . . . . . . 13
⊢ / =
(/r‘ℂfld) |
32 | | cnfld0 21428 |
. . . . . . . . . . . . 13
⊢ 0 =
(0g‘ℂfld) |
33 | 1 | ad7antr 737 |
. . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝐹 ∈
(SubDRing‘ℂfld)) |
34 | | cnfldsub 21433 |
. . . . . . . . . . . . . 14
⊢ −
= (-g‘ℂfld) |
35 | 34, 27, 9, 13 | subgsubcld 33028 |
. . . . . . . . . . . . . . 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 737 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑁 ∈ On) |
39 | 36, 38, 14 | constrconj 33735 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (∗‘𝑑) ∈ (𝐶‘𝑁)) |
40 | 7, 39 | sseldd 4009 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (∗‘𝑑) ∈ 𝐹) |
41 | 36, 38, 12 | constrconj 33735 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (∗‘𝑐) ∈ (𝐶‘𝑁)) |
42 | 7, 41 | sseldd 4009 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (∗‘𝑐) ∈ 𝐹) |
43 | 34, 27, 40, 42 | subgsubcld 33028 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → ((∗‘𝑑) − (∗‘𝑐)) ∈ 𝐹) |
44 | 28, 30, 35, 43 | subrgmcld 33213 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → ((𝑎 − 𝑐) · ((∗‘𝑑) − (∗‘𝑐))) ∈ 𝐹) |
45 | 36, 38, 8 | constrconj 33735 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (∗‘𝑎) ∈ (𝐶‘𝑁)) |
46 | 7, 45 | sseldd 4009 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (∗‘𝑎) ∈ 𝐹) |
47 | 34, 27, 46, 42 | subgsubcld 33028 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → ((∗‘𝑎) − (∗‘𝑐)) ∈ 𝐹) |
48 | 34, 27, 15, 13 | subgsubcld 33028 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (𝑑 − 𝑐) ∈ 𝐹) |
49 | 28, 30, 47, 48 | subrgmcld 33213 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (((∗‘𝑎) − (∗‘𝑐)) · (𝑑 − 𝑐)) ∈ 𝐹) |
50 | 34, 27, 44, 49 | subgsubcld 33028 |
. . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (((𝑎 − 𝑐) · ((∗‘𝑑) − (∗‘𝑐))) −
(((∗‘𝑎)
− (∗‘𝑐))
· (𝑑 − 𝑐))) ∈ 𝐹) |
51 | 36, 38, 10 | constrconj 33735 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (∗‘𝑏) ∈ (𝐶‘𝑁)) |
52 | 7, 51 | sseldd 4009 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (∗‘𝑏) ∈ 𝐹) |
53 | 34, 27, 52, 46 | subgsubcld 33028 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → ((∗‘𝑏) − (∗‘𝑎)) ∈ 𝐹) |
54 | 28, 30, 53, 48 | subrgmcld 33213 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐)) ∈ 𝐹) |
55 | 34, 27, 11, 9 | subgsubcld 33028 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (𝑏 − 𝑎) ∈ 𝐹) |
56 | 28, 30, 55, 43 | subrgmcld 33213 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐))) ∈ 𝐹) |
57 | 34, 27, 54, 56 | subgsubcld 33028 |
. . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → ((((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐)) − ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐)))) ∈ 𝐹) |
58 | 5, 11 | sseldd 4009 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑏 ∈ ℂ) |
59 | 5, 9 | sseldd 4009 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑎 ∈ ℂ) |
60 | 58, 59 | cjsubd 32755 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (∗‘(𝑏 − 𝑎)) = ((∗‘𝑏) − (∗‘𝑎))) |
61 | 60 | oveq1d 7463 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → ((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐)) = (((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐))) |
62 | 5, 55 | sseldd 4009 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (𝑏 − 𝑎) ∈ ℂ) |
63 | 62 | cjcld 15245 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (∗‘(𝑏 − 𝑎)) ∈ ℂ) |
64 | 5, 48 | sseldd 4009 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (𝑑 − 𝑐) ∈ ℂ) |
65 | 63, 64 | cjmuld 15270 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) →
(∗‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) = ((∗‘(∗‘(𝑏 − 𝑎))) · (∗‘(𝑑 − 𝑐)))) |
66 | 62 | cjcjd 15248 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) →
(∗‘(∗‘(𝑏 − 𝑎))) = (𝑏 − 𝑎)) |
67 | 5, 15 | sseldd 4009 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑑 ∈ ℂ) |
68 | 5, 13 | sseldd 4009 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑐 ∈ ℂ) |
69 | 67, 68 | cjsubd 32755 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (∗‘(𝑑 − 𝑐)) = ((∗‘𝑑) − (∗‘𝑐))) |
70 | 66, 69 | oveq12d 7466 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) →
((∗‘(∗‘(𝑏 − 𝑎))) · (∗‘(𝑑 − 𝑐))) = ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐)))) |
71 | 65, 70 | eqtrd 2780 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) →
(∗‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) = ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐)))) |
72 | 61, 71 | oveq12d 7466 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐)) −
(∗‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐)))) = ((((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐)) − ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐))))) |
73 | 63, 64 | mulcld 11310 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → ((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐)) ∈ ℂ) |
74 | | imval2 15200 |
. . . . . . . . . . . . . . . . . 18
⊢
(((∗‘(𝑏
− 𝑎)) · (𝑑 − 𝑐)) ∈ ℂ →
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) = ((((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐)) −
(∗‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐)))) / (2 · i))) |
75 | 73, 74 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) →
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) = ((((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐)) −
(∗‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐)))) / (2 · i))) |
76 | 75 | neeq1d 3006 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) →
((ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0 ↔ ((((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐)) −
(∗‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐)))) / (2 · i)) ≠
0)) |
77 | 20, 76 | mpbid 232 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → ((((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐)) −
(∗‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐)))) / (2 · i)) ≠
0) |
78 | 73 | cjcld 15245 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) →
(∗‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ∈ ℂ) |
79 | 73, 78 | subcld 11647 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐)) −
(∗‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐)))) ∈ ℂ) |
80 | | 2cnd 12371 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 2 ∈
ℂ) |
81 | | ax-icn 11243 |
. . . . . . . . . . . . . . . . . 18
⊢ i ∈
ℂ |
82 | 81 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → i ∈
ℂ) |
83 | 80, 82 | mulcld 11310 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (2 · i) ∈
ℂ) |
84 | | 2cn 12368 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ∈
ℂ |
85 | | 2ne0 12397 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ≠
0 |
86 | | ine0 11725 |
. . . . . . . . . . . . . . . . . 18
⊢ i ≠
0 |
87 | 84, 81, 85, 86 | mulne0i 11933 |
. . . . . . . . . . . . . . . . 17
⊢ (2
· i) ≠ 0 |
88 | 87 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (2 · i) ≠
0) |
89 | 79, 83, 88 | divne0bd 12082 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → ((((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐)) −
(∗‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐)))) ≠ 0 ↔ ((((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐)) −
(∗‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐)))) / (2 · i)) ≠
0)) |
90 | 77, 89 | mpbird 257 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐)) −
(∗‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐)))) ≠ 0) |
91 | 72, 90 | eqnetrrd 3015 |
. . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → ((((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐)) − ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐)))) ≠ 0) |
92 | 31, 32, 33, 50, 57, 91 | sdrgdvcl 33266 |
. . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → ((((𝑎 − 𝑐) · ((∗‘𝑑) − (∗‘𝑐))) −
(((∗‘𝑎)
− (∗‘𝑐))
· (𝑑 − 𝑐))) / ((((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐)) − ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐))))) ∈ 𝐹) |
93 | 28, 30, 92, 55 | subrgmcld 33213 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (((((𝑎 − 𝑐) · ((∗‘𝑑) − (∗‘𝑐))) −
(((∗‘𝑎)
− (∗‘𝑐))
· (𝑑 − 𝑐))) / ((((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐)) − ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐))))) · (𝑏 − 𝑎)) ∈ 𝐹) |
94 | 23, 27, 9, 93 | subgcld 33027 |
. . . . . . . . . 10
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (𝑎 + (((((𝑎 − 𝑐) · ((∗‘𝑑) − (∗‘𝑐))) −
(((∗‘𝑎)
− (∗‘𝑐))
· (𝑑 − 𝑐))) / ((((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐)) − ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐))))) · (𝑏 − 𝑎))) ∈ 𝐹) |
95 | 22, 94 | eqeltrd 2844 |
. . . . . . . . 9
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑋 ∈ 𝐹) |
96 | 95 | orcd 872 |
. . . . . . . 8
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (𝑋 ∈ 𝐹 ∨ (𝐿[:]𝐾) = 2)) |
97 | 96 | r19.29an 3164 |
. . . . . . 7
⊢
(((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ ∃𝑟 ∈ ℝ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (𝑋 ∈ 𝐹 ∨ (𝐿[:]𝐾) = 2)) |
98 | 97 | r19.29an 3164 |
. . . . . 6
⊢
((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (𝑋 ∈ 𝐹 ∨ (𝐿[:]𝐾) = 2)) |
99 | 98 | r19.29an 3164 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ ∃𝑑 ∈ (𝐶‘𝑁)∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (𝑋 ∈ 𝐹 ∨ (𝐿[:]𝐾) = 2)) |
100 | 99 | r19.29an 3164 |
. . . 4
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ ∃𝑐 ∈ (𝐶‘𝑁)∃𝑑 ∈ (𝐶‘𝑁)∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (𝑋 ∈ 𝐹 ∨ (𝐿[:]𝐾) = 2)) |
101 | 100 | r19.29an 3164 |
. . 3
⊢ (((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ ∃𝑏 ∈ (𝐶‘𝑁)∃𝑐 ∈ (𝐶‘𝑁)∃𝑑 ∈ (𝐶‘𝑁)∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (𝑋 ∈ 𝐹 ∨ (𝐿[:]𝐾) = 2)) |
102 | 101 | r19.29an 3164 |
. 2
⊢ ((𝜑 ∧ ∃𝑎 ∈ (𝐶‘𝑁)∃𝑏 ∈ (𝐶‘𝑁)∃𝑐 ∈ (𝐶‘𝑁)∃𝑑 ∈ (𝐶‘𝑁)∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (𝑋 ∈ 𝐹 ∨ (𝐿[:]𝐾) = 2)) |
103 | 36, 37 | constrsscn 33730 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐶‘𝑁) ⊆ ℂ) |
104 | 103 | ad8antr 739 |
. . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 = 𝑏) → (𝐶‘𝑁) ⊆ ℂ) |
105 | | simp-8r 791 |
. . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 = 𝑏) → 𝑎 ∈ (𝐶‘𝑁)) |
106 | | simp-7r 789 |
. . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 = 𝑏) → 𝑏 ∈ (𝐶‘𝑁)) |
107 | | simp-6r 787 |
. . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 = 𝑏) → 𝑐 ∈ (𝐶‘𝑁)) |
108 | | simp-5r 785 |
. . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 = 𝑏) → 𝑒 ∈ (𝐶‘𝑁)) |
109 | | simp-4r 783 |
. . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 = 𝑏) → 𝑓 ∈ (𝐶‘𝑁)) |
110 | | simpllr 775 |
. . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 = 𝑏) → 𝑡 ∈ ℝ) |
111 | | simplrl 776 |
. . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 = 𝑏) → 𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎)))) |
112 | | simplrr 777 |
. . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 = 𝑏) → (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓))) |
113 | | simpr 484 |
. . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 = 𝑏) → 𝑎 = 𝑏) |
114 | 104, 105,
106, 107, 108, 109, 110, 111, 112, 113 | constrrtlc2 33724 |
. . . . . . . . . . 11
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 = 𝑏) → 𝑋 = 𝑎) |
115 | 6 | ad8antr 739 |
. . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 = 𝑏) → (𝐶‘𝑁) ⊆ 𝐹) |
116 | 115, 105 | sseldd 4009 |
. . . . . . . . . . 11
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 = 𝑏) → 𝑎 ∈ 𝐹) |
117 | 114, 116 | eqeltrd 2844 |
. . . . . . . . . 10
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 = 𝑏) → 𝑋 ∈ 𝐹) |
118 | 117 | orcd 872 |
. . . . . . . . 9
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 = 𝑏) → (𝑋 ∈ 𝐹 ∨ (𝐿[:]𝐾) = 2)) |
119 | | constrelextdg2.k |
. . . . . . . . . 10
⊢ 𝐾 = (ℂfld
↾s 𝐹) |
120 | | constrelextdg2.l |
. . . . . . . . . 10
⊢ 𝐿 = (ℂfld
↾s (ℂfld fldGen (𝐹 ∪ {𝑋}))) |
121 | | eqid 2740 |
. . . . . . . . . 10
⊢
(Poly1‘𝐾) = (Poly1‘𝐾) |
122 | | eqid 2740 |
. . . . . . . . . 10
⊢
(.g‘(mulGrp‘ℂfld)) =
(.g‘(mulGrp‘ℂfld)) |
123 | | cnfldfld 33336 |
. . . . . . . . . . 11
⊢
ℂfld ∈ Field |
124 | 123 | a1i 11 |
. . . . . . . . . 10
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → ℂfld ∈
Field) |
125 | 1 | ad8antr 739 |
. . . . . . . . . 10
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → 𝐹 ∈
(SubDRing‘ℂfld)) |
126 | | constrelextdg2.x |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑋 ∈ (𝐶‘suc 𝑁)) |
127 | | eqid 2740 |
. . . . . . . . . . . . . 14
⊢ (𝐶‘𝑁) = (𝐶‘𝑁) |
128 | 36, 37, 127 | constrsuc 33728 |
. . . . . . . . . . . . 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 739 |
. . . . . . . . . 10
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → 𝑋 ∈ ℂ) |
132 | 26 | ad8antr 739 |
. . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → 𝐹 ∈
(SubGrp‘ℂfld)) |
133 | 6 | ad8antr 739 |
. . . . . . . . . . . . . . 15
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → (𝐶‘𝑁) ⊆ 𝐹) |
134 | 37 | ad8antr 739 |
. . . . . . . . . . . . . . . 16
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → 𝑁 ∈ On) |
135 | | simp-8r 791 |
. . . . . . . . . . . . . . . 16
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → 𝑎 ∈ (𝐶‘𝑁)) |
136 | 36, 134, 135 | constrconj 33735 |
. . . . . . . . . . . . . . 15
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → (∗‘𝑎) ∈ (𝐶‘𝑁)) |
137 | 133, 136 | sseldd 4009 |
. . . . . . . . . . . . . 14
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → (∗‘𝑎) ∈ 𝐹) |
138 | 125, 24 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → 𝐹 ∈
(SubRing‘ℂfld)) |
139 | 133, 135 | sseldd 4009 |
. . . . . . . . . . . . . . 15
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → 𝑎 ∈ 𝐹) |
140 | | simp-7r 789 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → 𝑏 ∈ (𝐶‘𝑁)) |
141 | 36, 134, 140 | constrconj 33735 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → (∗‘𝑏) ∈ (𝐶‘𝑁)) |
142 | 133, 141 | sseldd 4009 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → (∗‘𝑏) ∈ 𝐹) |
143 | 34, 132, 142, 137 | subgsubcld 33028 |
. . . . . . . . . . . . . . . 16
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → ((∗‘𝑏) − (∗‘𝑎)) ∈ 𝐹) |
144 | 133, 140 | sseldd 4009 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → 𝑏 ∈ 𝐹) |
145 | 34, 132, 144, 139 | subgsubcld 33028 |
. . . . . . . . . . . . . . . 16
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → (𝑏 − 𝑎) ∈ 𝐹) |
146 | 103 | ad8antr 739 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → (𝐶‘𝑁) ⊆ ℂ) |
147 | 146, 140 | sseldd 4009 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → 𝑏 ∈ ℂ) |
148 | 146, 135 | sseldd 4009 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → 𝑎 ∈ ℂ) |
149 | | simpr 484 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → 𝑎 ≠ 𝑏) |
150 | 149 | necomd 3002 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → 𝑏 ≠ 𝑎) |
151 | 147, 148,
150 | subne0d 11656 |
. . . . . . . . . . . . . . . 16
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → (𝑏 − 𝑎) ≠ 0) |
152 | 31, 32, 125, 143, 145, 151 | sdrgdvcl 33266 |
. . . . . . . . . . . . . . 15
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)) ∈ 𝐹) |
153 | 28, 138, 139, 152 | subrgmcld 33213 |
. . . . . . . . . . . . . 14
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) ∈ 𝐹) |
154 | 34, 132, 137, 153 | subgsubcld 33028 |
. . . . . . . . . . . . 13
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → ((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) ∈ 𝐹) |
155 | | simp-6r 787 |
. . . . . . . . . . . . . . 15
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → 𝑐 ∈ (𝐶‘𝑁)) |
156 | 36, 134, 155 | constrconj 33735 |
. . . . . . . . . . . . . 14
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → (∗‘𝑐) ∈ (𝐶‘𝑁)) |
157 | 133, 156 | sseldd 4009 |
. . . . . . . . . . . . 13
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → (∗‘𝑐) ∈ 𝐹) |
158 | 34, 132, 154, 157 | subgsubcld 33028 |
. . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) ∈ 𝐹) |
159 | 133, 155 | sseldd 4009 |
. . . . . . . . . . . . 13
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → 𝑐 ∈ 𝐹) |
160 | 28, 138, 159, 152 | subrgmcld 33213 |
. . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) ∈ 𝐹) |
161 | 34, 132, 158, 160 | subgsubcld 33028 |
. . . . . . . . . . 11
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → ((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) ∈ 𝐹) |
162 | | simp-5r 785 |
. . . . . . . . . . . . 13
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → 𝑒 ∈ (𝐶‘𝑁)) |
163 | | simp-4r 783 |
. . . . . . . . . . . . 13
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → 𝑓 ∈ (𝐶‘𝑁)) |
164 | | simpllr 775 |
. . . . . . . . . . . . 13
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → 𝑡 ∈ ℝ) |
165 | | simplrl 776 |
. . . . . . . . . . . . 13
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → 𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎)))) |
166 | | simplrr 777 |
. . . . . . . . . . . . 13
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓))) |
167 | | eqid 2740 |
. . . . . . . . . . . . 13
⊢
(((∗‘𝑏)
− (∗‘𝑎))
/ (𝑏 − 𝑎)) = (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)) |
168 | | eqid 2740 |
. . . . . . . . . . . . 13
⊢
(((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) = (((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) |
169 | | eqid 2740 |
. . . . . . . . . . . . 13
⊢ (-((𝑐 ·
(((∗‘𝑎)
− (𝑎 ·
(((∗‘𝑏)
− (∗‘𝑎))
/ (𝑏 − 𝑎)))) −
(∗‘𝑐))) +
((𝑒 − 𝑓) ·
((∗‘𝑒) −
(∗‘𝑓)))) /
(((∗‘𝑏)
− (∗‘𝑎))
/ (𝑏 − 𝑎))) = (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) |
170 | 146, 135,
140, 155, 162, 163, 164, 165, 166, 167, 168, 169, 149 | constrrtlc1 33723 |
. . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → (((𝑋↑2) + (((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) · 𝑋) + (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))))) = 0 ∧ (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)) ≠ 0)) |
171 | 170 | simprd 495 |
. . . . . . . . . . 11
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)) ≠ 0) |
172 | 31, 32, 125, 161, 152, 171 | sdrgdvcl 33266 |
. . . . . . . . . 10
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → (((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) ∈ 𝐹) |
173 | | df-neg 11523 |
. . . . . . . . . . . 12
⊢ -((𝑐 ·
(((∗‘𝑎)
− (𝑎 ·
(((∗‘𝑏)
− (∗‘𝑎))
/ (𝑏 − 𝑎)))) −
(∗‘𝑐))) +
((𝑒 − 𝑓) ·
((∗‘𝑒) −
(∗‘𝑓)))) = (0
− ((𝑐 ·
(((∗‘𝑎)
− (𝑎 ·
(((∗‘𝑏)
− (∗‘𝑎))
/ (𝑏 − 𝑎)))) −
(∗‘𝑐))) +
((𝑒 − 𝑓) ·
((∗‘𝑒) −
(∗‘𝑓))))) |
174 | 36, 134 | constr01 33732 |
. . . . . . . . . . . . . . 15
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → {0, 1} ⊆ (𝐶‘𝑁)) |
175 | 32 | fvexi 6934 |
. . . . . . . . . . . . . . . . 17
⊢ 0 ∈
V |
176 | 175 | prid1 4787 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
{0, 1} |
177 | 176 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → 0 ∈ {0, 1}) |
178 | 174, 177 | sseldd 4009 |
. . . . . . . . . . . . . 14
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → 0 ∈ (𝐶‘𝑁)) |
179 | 133, 178 | sseldd 4009 |
. . . . . . . . . . . . 13
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → 0 ∈ 𝐹) |
180 | 28, 138, 159, 158 | subrgmcld 33213 |
. . . . . . . . . . . . . 14
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → (𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) ∈ 𝐹) |
181 | 133, 162 | sseldd 4009 |
. . . . . . . . . . . . . . . 16
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → 𝑒 ∈ 𝐹) |
182 | 133, 163 | sseldd 4009 |
. . . . . . . . . . . . . . . 16
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → 𝑓 ∈ 𝐹) |
183 | 34, 132, 181, 182 | subgsubcld 33028 |
. . . . . . . . . . . . . . 15
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → (𝑒 − 𝑓) ∈ 𝐹) |
184 | 36, 134, 162 | constrconj 33735 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → (∗‘𝑒) ∈ (𝐶‘𝑁)) |
185 | 133, 184 | sseldd 4009 |
. . . . . . . . . . . . . . . 16
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → (∗‘𝑒) ∈ 𝐹) |
186 | 36, 134, 163 | constrconj 33735 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → (∗‘𝑓) ∈ (𝐶‘𝑁)) |
187 | 133, 186 | sseldd 4009 |
. . . . . . . . . . . . . . . 16
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → (∗‘𝑓) ∈ 𝐹) |
188 | 34, 132, 185, 187 | subgsubcld 33028 |
. . . . . . . . . . . . . . 15
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → ((∗‘𝑒) − (∗‘𝑓)) ∈ 𝐹) |
189 | 28, 138, 183, 188 | subrgmcld 33213 |
. . . . . . . . . . . . . 14
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓))) ∈ 𝐹) |
190 | 23, 132, 180, 189 | subgcld 33027 |
. . . . . . . . . . . . 13
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → ((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) ∈ 𝐹) |
191 | 34, 132, 179, 190 | subgsubcld 33028 |
. . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → (0 − ((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓))))) ∈ 𝐹) |
192 | 173, 191 | eqeltrid 2848 |
. . . . . . . . . . 11
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → -((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) ∈ 𝐹) |
193 | 31, 32, 125, 192, 152, 171 | sdrgdvcl 33266 |
. . . . . . . . . 10
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) ∈ 𝐹) |
194 | | 2nn0 12570 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℕ0 |
195 | 194 | a1i 11 |
. . . . . . . . . . . . 13
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → 2 ∈
ℕ0) |
196 | | cnfldexp 21440 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ∈ ℂ ∧ 2 ∈
ℕ0) →
(2(.g‘(mulGrp‘ℂfld))𝑋) = (𝑋↑2)) |
197 | 131, 195,
196 | syl2anc 583 |
. . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) →
(2(.g‘(mulGrp‘ℂfld))𝑋) = (𝑋↑2)) |
198 | 197 | oveq1d 7463 |
. . . . . . . . . . 11
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) →
((2(.g‘(mulGrp‘ℂfld))𝑋) + (((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) · 𝑋) + (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))))) = ((𝑋↑2) + (((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) · 𝑋) + (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))))) |
199 | 170 | simpld 494 |
. . . . . . . . . . 11
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → ((𝑋↑2) + (((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) · 𝑋) + (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))))) = 0) |
200 | 198, 199 | eqtrd 2780 |
. . . . . . . . . 10
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) →
((2(.g‘(mulGrp‘ℂfld))𝑋) + (((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) · 𝑋) + (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))))) = 0) |
201 | 119, 120,
32, 121, 2, 28, 23, 122, 124, 125, 131, 172, 193, 200 | rtelextdg2 33718 |
. . . . . . . . 9
⊢
(((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ∧ 𝑎 ≠ 𝑏) → (𝑋 ∈ 𝐹 ∨ (𝐿[:]𝐾) = 2)) |
202 | | exmidne 2956 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑏 ∨ 𝑎 ≠ 𝑏) |
203 | 202 | a1i 11 |
. . . . . . . . 9
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (𝑎 = 𝑏 ∨ 𝑎 ≠ 𝑏)) |
204 | 118, 201,
203 | mpjaodan 959 |
. . . . . . . 8
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ 𝑡 ∈ ℝ) ∧ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (𝑋 ∈ 𝐹 ∨ (𝐿[:]𝐾) = 2)) |
205 | 204 | r19.29an 3164 |
. . . . . . 7
⊢
(((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ ∃𝑡 ∈ ℝ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (𝑋 ∈ 𝐹 ∨ (𝐿[:]𝐾) = 2)) |
206 | 205 | r19.29an 3164 |
. . . . . 6
⊢
((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ ∃𝑓 ∈ (𝐶‘𝑁)∃𝑡 ∈ ℝ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (𝑋 ∈ 𝐹 ∨ (𝐿[:]𝐾) = 2)) |
207 | 206 | r19.29an 3164 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ ∃𝑒 ∈ (𝐶‘𝑁)∃𝑓 ∈ (𝐶‘𝑁)∃𝑡 ∈ ℝ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (𝑋 ∈ 𝐹 ∨ (𝐿[:]𝐾) = 2)) |
208 | 207 | r19.29an 3164 |
. . . 4
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ ∃𝑐 ∈ (𝐶‘𝑁)∃𝑒 ∈ (𝐶‘𝑁)∃𝑓 ∈ (𝐶‘𝑁)∃𝑡 ∈ ℝ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (𝑋 ∈ 𝐹 ∨ (𝐿[:]𝐾) = 2)) |
209 | 208 | r19.29an 3164 |
. . 3
⊢ (((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ ∃𝑏 ∈ (𝐶‘𝑁)∃𝑐 ∈ (𝐶‘𝑁)∃𝑒 ∈ (𝐶‘𝑁)∃𝑓 ∈ (𝐶‘𝑁)∃𝑡 ∈ ℝ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (𝑋 ∈ 𝐹 ∨ (𝐿[:]𝐾) = 2)) |
210 | 209 | r19.29an 3164 |
. 2
⊢ ((𝜑 ∧ ∃𝑎 ∈ (𝐶‘𝑁)∃𝑏 ∈ (𝐶‘𝑁)∃𝑐 ∈ (𝐶‘𝑁)∃𝑒 ∈ (𝐶‘𝑁)∃𝑓 ∈ (𝐶‘𝑁)∃𝑡 ∈ ℝ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (𝑋 ∈ 𝐹 ∨ (𝐿[:]𝐾) = 2)) |
211 | 123 | a1i 11 |
. . . . . . . . 9
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ℂfld ∈
Field) |
212 | 1 | ad7antr 737 |
. . . . . . . . 9
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝐹 ∈
(SubDRing‘ℂfld)) |
213 | 130 | ad7antr 737 |
. . . . . . . . 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 737 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (𝐶‘𝑁) ⊆ 𝐹) |
217 | | simpllr 775 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑒 ∈ (𝐶‘𝑁)) |
218 | 216, 217 | sseldd 4009 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑒 ∈ 𝐹) |
219 | | simplr 768 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑓 ∈ (𝐶‘𝑁)) |
220 | 216, 219 | sseldd 4009 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑓 ∈ 𝐹) |
221 | 34, 214, 218, 220 | subgsubcld 33028 |
. . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (𝑒 − 𝑓) ∈ 𝐹) |
222 | 103 | ad7antr 737 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (𝐶‘𝑁) ⊆ ℂ) |
223 | 222, 217 | sseldd 4009 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑒 ∈ ℂ) |
224 | 222, 219 | sseldd 4009 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑓 ∈ ℂ) |
225 | 223, 224 | cjsubd 32755 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (∗‘(𝑒 − 𝑓)) = ((∗‘𝑒) − (∗‘𝑓))) |
226 | 37 | ad7antr 737 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑁 ∈ On) |
227 | 36, 226, 217 | constrconj 33735 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (∗‘𝑒) ∈ (𝐶‘𝑁)) |
228 | 216, 227 | sseldd 4009 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (∗‘𝑒) ∈ 𝐹) |
229 | 36, 226, 219 | constrconj 33735 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (∗‘𝑓) ∈ (𝐶‘𝑁)) |
230 | 216, 229 | sseldd 4009 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (∗‘𝑓) ∈ 𝐹) |
231 | 34, 214, 228, 230 | subgsubcld 33028 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((∗‘𝑒) − (∗‘𝑓)) ∈ 𝐹) |
232 | 225, 231 | eqeltrd 2844 |
. . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (∗‘(𝑒 − 𝑓)) ∈ 𝐹) |
233 | 28, 215, 221, 232 | subrgmcld 33213 |
. . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) ∈ 𝐹) |
234 | | simp-4r 783 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑑 ∈ (𝐶‘𝑁)) |
235 | 36, 226, 234 | constrconj 33735 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (∗‘𝑑) ∈ (𝐶‘𝑁)) |
236 | 216, 235 | sseldd 4009 |
. . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (∗‘𝑑) ∈ 𝐹) |
237 | 216, 234 | sseldd 4009 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑑 ∈ 𝐹) |
238 | | simp-7r 789 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑎 ∈ (𝐶‘𝑁)) |
239 | 216, 238 | sseldd 4009 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑎 ∈ 𝐹) |
240 | 23, 214, 237, 239 | subgcld 33027 |
. . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (𝑑 + 𝑎) ∈ 𝐹) |
241 | 28, 215, 236, 240 | subrgmcld 33213 |
. . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((∗‘𝑑) · (𝑑 + 𝑎)) ∈ 𝐹) |
242 | 34, 214, 233, 241 | subgsubcld 33028 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) ∈ 𝐹) |
243 | | simp-6r 787 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑏 ∈ (𝐶‘𝑁)) |
244 | 216, 243 | sseldd 4009 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑏 ∈ 𝐹) |
245 | | simp-5r 785 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑐 ∈ (𝐶‘𝑁)) |
246 | 216, 245 | sseldd 4009 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑐 ∈ 𝐹) |
247 | 34, 214, 244, 246 | subgsubcld 33028 |
. . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (𝑏 − 𝑐) ∈ 𝐹) |
248 | 222, 243 | sseldd 4009 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑏 ∈ ℂ) |
249 | 222, 245 | sseldd 4009 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑐 ∈ ℂ) |
250 | 248, 249 | cjsubd 32755 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (∗‘(𝑏 − 𝑐)) = ((∗‘𝑏) − (∗‘𝑐))) |
251 | 36, 226, 243 | constrconj 33735 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (∗‘𝑏) ∈ (𝐶‘𝑁)) |
252 | 216, 251 | sseldd 4009 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (∗‘𝑏) ∈ 𝐹) |
253 | 36, 226, 245 | constrconj 33735 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (∗‘𝑐) ∈ (𝐶‘𝑁)) |
254 | 216, 253 | sseldd 4009 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (∗‘𝑐) ∈ 𝐹) |
255 | 34, 214, 252, 254 | subgsubcld 33028 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((∗‘𝑏) − (∗‘𝑐)) ∈ 𝐹) |
256 | 250, 255 | eqeltrd 2844 |
. . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (∗‘(𝑏 − 𝑐)) ∈ 𝐹) |
257 | 28, 215, 247, 256 | subrgmcld 33213 |
. . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) ∈ 𝐹) |
258 | 36, 226, 238 | constrconj 33735 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (∗‘𝑎) ∈ (𝐶‘𝑁)) |
259 | 216, 258 | sseldd 4009 |
. . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (∗‘𝑎) ∈ 𝐹) |
260 | 28, 215, 259, 240 | subrgmcld 33213 |
. . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((∗‘𝑎) · (𝑑 + 𝑎)) ∈ 𝐹) |
261 | 34, 214, 257, 260 | subgsubcld 33028 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎))) ∈ 𝐹) |
262 | 34, 214, 242, 261 | subgsubcld 33028 |
. . . . . . . . . 10
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) ∈ 𝐹) |
263 | 34, 214, 236, 259 | subgsubcld 33028 |
. . . . . . . . . 10
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((∗‘𝑑) − (∗‘𝑎)) ∈ 𝐹) |
264 | 222, 234 | sseldd 4009 |
. . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑑 ∈ ℂ) |
265 | 222, 238 | sseldd 4009 |
. . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑎 ∈ ℂ) |
266 | 264, 265 | cjsubd 32755 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (∗‘(𝑑 − 𝑎)) = ((∗‘𝑑) − (∗‘𝑎))) |
267 | 264, 265 | subcld 11647 |
. . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (𝑑 − 𝑎) ∈ ℂ) |
268 | | simpr1 1194 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑎 ≠ 𝑑) |
269 | 268 | necomd 3002 |
. . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑑 ≠ 𝑎) |
270 | 264, 265,
269 | subne0d 11656 |
. . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (𝑑 − 𝑎) ≠ 0) |
271 | 267, 270 | cjne0d 15252 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (∗‘(𝑑 − 𝑎)) ≠ 0) |
272 | 266, 271 | eqnetrrd 3015 |
. . . . . . . . . 10
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((∗‘𝑑) − (∗‘𝑎)) ≠ 0) |
273 | 31, 32, 212, 262, 263, 272 | sdrgdvcl 33266 |
. . . . . . . . 9
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) ∈ 𝐹) |
274 | | df-neg 11523 |
. . . . . . . . . 10
⊢
-(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎))) = (0 − (((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎)))) |
275 | 36, 226 | constr01 33732 |
. . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → {0, 1} ⊆ (𝐶‘𝑁)) |
276 | 176 | a1i 11 |
. . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 0 ∈ {0, 1}) |
277 | 275, 276 | sseldd 4009 |
. . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 0 ∈ (𝐶‘𝑁)) |
278 | 216, 277 | sseldd 4009 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 0 ∈ 𝐹) |
279 | 28, 215, 237, 239 | subrgmcld 33213 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (𝑑 · 𝑎) ∈ 𝐹) |
280 | 28, 215, 259, 279 | subrgmcld 33213 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((∗‘𝑎) · (𝑑 · 𝑎)) ∈ 𝐹) |
281 | 28, 215, 257, 237 | subrgmcld 33213 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑) ∈ 𝐹) |
282 | 34, 214, 280, 281 | subgsubcld 33028 |
. . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) ∈ 𝐹) |
283 | 28, 215, 236, 279 | subrgmcld 33213 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((∗‘𝑑) · (𝑑 · 𝑎)) ∈ 𝐹) |
284 | 28, 215, 233, 239 | subrgmcld 33213 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎) ∈ 𝐹) |
285 | 34, 214, 283, 284 | subgsubcld 33028 |
. . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎)) ∈ 𝐹) |
286 | 34, 214, 282, 285 | subgsubcld 33028 |
. . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) ∈ 𝐹) |
287 | 31, 32, 212, 286, 263, 272 | sdrgdvcl 33266 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎))) ∈ 𝐹) |
288 | 34, 214, 278, 287 | subgsubcld 33028 |
. . . . . . . . . 10
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (0 −
(((((∗‘𝑎)
· (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎)))) ∈ 𝐹) |
289 | 274, 288 | eqeltrid 2848 |
. . . . . . . . 9
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎))) ∈ 𝐹) |
290 | 213, 194,
196 | sylancl 585 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) →
(2(.g‘(mulGrp‘ℂfld))𝑋) = (𝑋↑2)) |
291 | 290 | oveq1d 7463 |
. . . . . . . . . 10
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) →
((2(.g‘(mulGrp‘ℂfld))𝑋) + (((((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) · 𝑋) + -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎))))) = ((𝑋↑2) + (((((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) · 𝑋) + -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎)))))) |
292 | | simpr2 1195 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐))) |
293 | | simpr3 1196 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓))) |
294 | | eqid 2740 |
. . . . . . . . . . 11
⊢ ((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) = ((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) |
295 | | eqid 2740 |
. . . . . . . . . . 11
⊢ ((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) = ((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) |
296 | | eqid 2740 |
. . . . . . . . . . 11
⊢
(((((𝑒 − 𝑓) ·
(∗‘(𝑒 −
𝑓))) −
((∗‘𝑑)
· (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) = (((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) |
297 | | eqid 2740 |
. . . . . . . . . . 11
⊢
-(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎))) = -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎))) |
298 | 222, 238,
243, 245, 234, 217, 219, 213, 268, 292, 293, 294, 295, 296, 297 | constrrtcc 33726 |
. . . . . . . . . 10
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((𝑋↑2) + (((((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) · 𝑋) + -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎))))) = 0) |
299 | 291, 298 | eqtrd 2780 |
. . . . . . . . 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 33718 |
. . . . . . . 8
⊢
((((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ 𝑓 ∈ (𝐶‘𝑁)) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (𝑋 ∈ 𝐹 ∨ (𝐿[:]𝐾) = 2)) |
301 | 300 | r19.29an 3164 |
. . . . . . 7
⊢
(((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ 𝑒 ∈ (𝐶‘𝑁)) ∧ ∃𝑓 ∈ (𝐶‘𝑁)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (𝑋 ∈ 𝐹 ∨ (𝐿[:]𝐾) = 2)) |
302 | 301 | r19.29an 3164 |
. . . . . 6
⊢
((((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ 𝑑 ∈ (𝐶‘𝑁)) ∧ ∃𝑒 ∈ (𝐶‘𝑁)∃𝑓 ∈ (𝐶‘𝑁)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (𝑋 ∈ 𝐹 ∨ (𝐿[:]𝐾) = 2)) |
303 | 302 | r19.29an 3164 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ 𝑐 ∈ (𝐶‘𝑁)) ∧ ∃𝑑 ∈ (𝐶‘𝑁)∃𝑒 ∈ (𝐶‘𝑁)∃𝑓 ∈ (𝐶‘𝑁)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (𝑋 ∈ 𝐹 ∨ (𝐿[:]𝐾) = 2)) |
304 | 303 | r19.29an 3164 |
. . . 4
⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ 𝑏 ∈ (𝐶‘𝑁)) ∧ ∃𝑐 ∈ (𝐶‘𝑁)∃𝑑 ∈ (𝐶‘𝑁)∃𝑒 ∈ (𝐶‘𝑁)∃𝑓 ∈ (𝐶‘𝑁)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (𝑋 ∈ 𝐹 ∨ (𝐿[:]𝐾) = 2)) |
305 | 304 | r19.29an 3164 |
. . 3
⊢ (((𝜑 ∧ 𝑎 ∈ (𝐶‘𝑁)) ∧ ∃𝑏 ∈ (𝐶‘𝑁)∃𝑐 ∈ (𝐶‘𝑁)∃𝑑 ∈ (𝐶‘𝑁)∃𝑒 ∈ (𝐶‘𝑁)∃𝑓 ∈ (𝐶‘𝑁)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (𝑋 ∈ 𝐹 ∨ (𝐿[:]𝐾) = 2)) |
306 | 305 | r19.29an 3164 |
. 2
⊢ ((𝜑 ∧ ∃𝑎 ∈ (𝐶‘𝑁)∃𝑏 ∈ (𝐶‘𝑁)∃𝑐 ∈ (𝐶‘𝑁)∃𝑑 ∈ (𝐶‘𝑁)∃𝑒 ∈ (𝐶‘𝑁)∃𝑓 ∈ (𝐶‘𝑁)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (𝑋 ∈ 𝐹 ∨ (𝐿[:]𝐾) = 2)) |
307 | 129 | simprd 495 |
. 2
⊢ (𝜑 → (∃𝑎 ∈ (𝐶‘𝑁)∃𝑏 ∈ (𝐶‘𝑁)∃𝑐 ∈ (𝐶‘𝑁)∃𝑑 ∈ (𝐶‘𝑁)∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ (𝐶‘𝑁)∃𝑏 ∈ (𝐶‘𝑁)∃𝑐 ∈ (𝐶‘𝑁)∃𝑒 ∈ (𝐶‘𝑁)∃𝑓 ∈ (𝐶‘𝑁)∃𝑡 ∈ ℝ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ (𝐶‘𝑁)∃𝑏 ∈ (𝐶‘𝑁)∃𝑐 ∈ (𝐶‘𝑁)∃𝑑 ∈ (𝐶‘𝑁)∃𝑒 ∈ (𝐶‘𝑁)∃𝑓 ∈ (𝐶‘𝑁)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓))))) |
308 | 102, 210,
306, 307 | mpjao3dan 1432 |
1
⊢ (𝜑 → (𝑋 ∈ 𝐹 ∨ (𝐿[:]𝐾) = 2)) |