Proof of Theorem line2
Step | Hyp | Ref
| Expression |
1 | | simp1 1138 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 𝐴 ∈ ℝ) |
2 | 1 | adantr 484 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → 𝐴 ∈ ℝ) |
3 | | line2.i |
. . . . . . . . . . . . . 14
⊢ 𝐼 = {1, 2} |
4 | | line2.p |
. . . . . . . . . . . . . 14
⊢ 𝑃 = (ℝ ↑m
𝐼) |
5 | 3, 4 | rrx2pxel 45738 |
. . . . . . . . . . . . 13
⊢ (𝑝 ∈ 𝑃 → (𝑝‘1) ∈ ℝ) |
6 | 5 | adantl 485 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (𝑝‘1) ∈ ℝ) |
7 | 2, 6 | remulcld 10868 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (𝐴 · (𝑝‘1)) ∈ ℝ) |
8 | 7 | recnd 10866 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (𝐴 · (𝑝‘1)) ∈ ℂ) |
9 | | simpl2l 1228 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → 𝐵 ∈ ℝ) |
10 | 3, 4 | rrx2pyel 45739 |
. . . . . . . . . . . . 13
⊢ (𝑝 ∈ 𝑃 → (𝑝‘2) ∈ ℝ) |
11 | 10 | adantl 485 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (𝑝‘2) ∈ ℝ) |
12 | 9, 11 | remulcld 10868 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (𝐵 · (𝑝‘2)) ∈ ℝ) |
13 | 12 | recnd 10866 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (𝐵 · (𝑝‘2)) ∈ ℂ) |
14 | | simpl 486 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → 𝐵 ∈
ℝ) |
15 | 14 | recnd 10866 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → 𝐵 ∈
ℂ) |
16 | 15 | 3ad2ant2 1136 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 𝐵 ∈ ℂ) |
17 | 16 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → 𝐵 ∈ ℂ) |
18 | | simp2r 1202 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 𝐵 ≠ 0) |
19 | 18 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → 𝐵 ≠ 0) |
20 | 8, 13, 17, 19 | divdird 11651 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) / 𝐵) = (((𝐴 · (𝑝‘1)) / 𝐵) + ((𝐵 · (𝑝‘2)) / 𝐵))) |
21 | 10 | recnd 10866 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈ 𝑃 → (𝑝‘2) ∈ ℂ) |
22 | 21 | adantl 485 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (𝑝‘2) ∈ ℂ) |
23 | 22, 17, 19 | divcan3d 11618 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ((𝐵 · (𝑝‘2)) / 𝐵) = (𝑝‘2)) |
24 | 23 | oveq2d 7234 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (((𝐴 · (𝑝‘1)) / 𝐵) + ((𝐵 · (𝑝‘2)) / 𝐵)) = (((𝐴 · (𝑝‘1)) / 𝐵) + (𝑝‘2))) |
25 | 20, 24 | eqtrd 2777 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) / 𝐵) = (((𝐴 · (𝑝‘1)) / 𝐵) + (𝑝‘2))) |
26 | 25 | eqeq1d 2739 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ((((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) / 𝐵) = (𝐶 / 𝐵) ↔ (((𝐴 · (𝑝‘1)) / 𝐵) + (𝑝‘2)) = (𝐶 / 𝐵))) |
27 | 7, 9, 19 | redivcld 11665 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ((𝐴 · (𝑝‘1)) / 𝐵) ∈ ℝ) |
28 | 27 | recnd 10866 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ((𝐴 · (𝑝‘1)) / 𝐵) ∈ ℂ) |
29 | | simp3 1140 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 𝐶 ∈ ℝ) |
30 | 14 | 3ad2ant2 1136 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 𝐵 ∈ ℝ) |
31 | 29, 30, 18 | redivcld 11665 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → (𝐶 / 𝐵) ∈ ℝ) |
32 | 31 | recnd 10866 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → (𝐶 / 𝐵) ∈ ℂ) |
33 | 32 | adantr 484 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (𝐶 / 𝐵) ∈ ℂ) |
34 | 28, 22, 33 | addrsub 11254 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ((((𝐴 · (𝑝‘1)) / 𝐵) + (𝑝‘2)) = (𝐶 / 𝐵) ↔ (𝑝‘2) = ((𝐶 / 𝐵) − ((𝐴 · (𝑝‘1)) / 𝐵)))) |
35 | | simpl3 1195 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → 𝐶 ∈ ℝ) |
36 | 35, 9, 19 | redivcld 11665 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (𝐶 / 𝐵) ∈ ℝ) |
37 | 36 | recnd 10866 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (𝐶 / 𝐵) ∈ ℂ) |
38 | 28, 37 | negsubdi2d 11210 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → -(((𝐴 · (𝑝‘1)) / 𝐵) − (𝐶 / 𝐵)) = ((𝐶 / 𝐵) − ((𝐴 · (𝑝‘1)) / 𝐵))) |
39 | 28, 37 | negsubdid 11209 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → -(((𝐴 · (𝑝‘1)) / 𝐵) − (𝐶 / 𝐵)) = (-((𝐴 · (𝑝‘1)) / 𝐵) + (𝐶 / 𝐵))) |
40 | 38, 39 | eqtr3d 2779 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ((𝐶 / 𝐵) − ((𝐴 · (𝑝‘1)) / 𝐵)) = (-((𝐴 · (𝑝‘1)) / 𝐵) + (𝐶 / 𝐵))) |
41 | 40 | eqeq2d 2748 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ((𝑝‘2) = ((𝐶 / 𝐵) − ((𝐴 · (𝑝‘1)) / 𝐵)) ↔ (𝑝‘2) = (-((𝐴 · (𝑝‘1)) / 𝐵) + (𝐶 / 𝐵)))) |
42 | 26, 34, 41 | 3bitrd 308 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ((((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) / 𝐵) = (𝐶 / 𝐵) ↔ (𝑝‘2) = (-((𝐴 · (𝑝‘1)) / 𝐵) + (𝐶 / 𝐵)))) |
43 | 7, 12 | readdcld 10867 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) ∈ ℝ) |
44 | 43 | recnd 10866 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) ∈ ℂ) |
45 | 29 | recnd 10866 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 𝐶 ∈ ℂ) |
46 | 45 | adantr 484 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → 𝐶 ∈ ℂ) |
47 | | recn 10824 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ℝ → 𝐵 ∈
ℂ) |
48 | 47 | anim1i 618 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) |
49 | 48 | 3ad2ant2 1136 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) |
50 | 49 | adantr 484 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) |
51 | | div11 11523 |
. . . . . . 7
⊢ ((((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → ((((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) / 𝐵) = (𝐶 / 𝐵) ↔ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶)) |
52 | 44, 46, 50, 51 | syl3anc 1373 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ((((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) / 𝐵) = (𝐶 / 𝐵) ↔ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶)) |
53 | 8, 17, 19 | divnegd 11626 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → -((𝐴 · (𝑝‘1)) / 𝐵) = (-(𝐴 · (𝑝‘1)) / 𝐵)) |
54 | 1 | recnd 10866 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 𝐴 ∈ ℂ) |
55 | 54 | adantr 484 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → 𝐴 ∈ ℂ) |
56 | 5 | recnd 10866 |
. . . . . . . . . . . . . 14
⊢ (𝑝 ∈ 𝑃 → (𝑝‘1) ∈ ℂ) |
57 | 56 | adantl 485 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (𝑝‘1) ∈ ℂ) |
58 | 55, 57 | mulneg1d 11290 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (-𝐴 · (𝑝‘1)) = -(𝐴 · (𝑝‘1))) |
59 | 58 | eqcomd 2743 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → -(𝐴 · (𝑝‘1)) = (-𝐴 · (𝑝‘1))) |
60 | 59 | oveq1d 7233 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (-(𝐴 · (𝑝‘1)) / 𝐵) = ((-𝐴 · (𝑝‘1)) / 𝐵)) |
61 | 53, 60 | eqtrd 2777 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → -((𝐴 · (𝑝‘1)) / 𝐵) = ((-𝐴 · (𝑝‘1)) / 𝐵)) |
62 | | renegcl 11146 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℝ → -𝐴 ∈
ℝ) |
63 | 62 | recnd 10866 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ → -𝐴 ∈
ℂ) |
64 | 63 | 3ad2ant1 1135 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → -𝐴 ∈ ℂ) |
65 | 64 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → -𝐴 ∈ ℂ) |
66 | | div23 11514 |
. . . . . . . . . 10
⊢ ((-𝐴 ∈ ℂ ∧ (𝑝‘1) ∈ ℂ ∧
(𝐵 ∈ ℂ ∧
𝐵 ≠ 0)) → ((-𝐴 · (𝑝‘1)) / 𝐵) = ((-𝐴 / 𝐵) · (𝑝‘1))) |
67 | 65, 57, 50, 66 | syl3anc 1373 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ((-𝐴 · (𝑝‘1)) / 𝐵) = ((-𝐴 / 𝐵) · (𝑝‘1))) |
68 | | line2.x |
. . . . . . . . . . . . . . 15
⊢ 𝑋 = {〈1, 0〉, 〈2,
(𝐶 / 𝐵)〉} |
69 | 68 | fveq1i 6723 |
. . . . . . . . . . . . . 14
⊢ (𝑋‘1) = ({〈1, 0〉,
〈2, (𝐶 / 𝐵)〉}‘1) |
70 | | 1ex 10834 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
V |
71 | | c0ex 10832 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
V |
72 | | 1ne2 12043 |
. . . . . . . . . . . . . . . 16
⊢ 1 ≠
2 |
73 | 70, 71, 72 | 3pm3.2i 1341 |
. . . . . . . . . . . . . . 15
⊢ (1 ∈
V ∧ 0 ∈ V ∧ 1 ≠ 2) |
74 | | fvpr1g 7012 |
. . . . . . . . . . . . . . 15
⊢ ((1
∈ V ∧ 0 ∈ V ∧ 1 ≠ 2) → ({〈1, 0〉, 〈2,
(𝐶 / 𝐵)〉}‘1) = 0) |
75 | 73, 74 | mp1i 13 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → ({〈1, 0〉,
〈2, (𝐶 / 𝐵)〉}‘1) =
0) |
76 | 69, 75 | syl5eq 2790 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → (𝑋‘1) = 0) |
77 | 76 | adantr 484 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (𝑋‘1) = 0) |
78 | 77 | oveq2d 7234 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ((𝑝‘1) − (𝑋‘1)) = ((𝑝‘1) − 0)) |
79 | 57 | subid1d 11183 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ((𝑝‘1) − 0) = (𝑝‘1)) |
80 | 78, 79 | eqtr2d 2778 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (𝑝‘1) = ((𝑝‘1) − (𝑋‘1))) |
81 | 80 | oveq2d 7234 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ((-𝐴 / 𝐵) · (𝑝‘1)) = ((-𝐴 / 𝐵) · ((𝑝‘1) − (𝑋‘1)))) |
82 | 61, 67, 81 | 3eqtrd 2781 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → -((𝐴 · (𝑝‘1)) / 𝐵) = ((-𝐴 / 𝐵) · ((𝑝‘1) − (𝑋‘1)))) |
83 | 82 | oveq1d 7233 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (-((𝐴 · (𝑝‘1)) / 𝐵) + (𝐶 / 𝐵)) = (((-𝐴 / 𝐵) · ((𝑝‘1) − (𝑋‘1))) + (𝐶 / 𝐵))) |
84 | 83 | eqeq2d 2748 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ((𝑝‘2) = (-((𝐴 · (𝑝‘1)) / 𝐵) + (𝐶 / 𝐵)) ↔ (𝑝‘2) = (((-𝐴 / 𝐵) · ((𝑝‘1) − (𝑋‘1))) + (𝐶 / 𝐵)))) |
85 | 42, 52, 84 | 3bitr3d 312 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = (((-𝐴 / 𝐵) · ((𝑝‘1) − (𝑋‘1))) + (𝐶 / 𝐵)))) |
86 | | recn 10824 |
. . . . . . . . . . . . 13
⊢ (𝐶 ∈ ℝ → 𝐶 ∈
ℂ) |
87 | 86 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐶 ∈
ℂ) |
88 | | recn 10824 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) |
89 | 88 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐴 ∈
ℂ) |
90 | | sub32 11117 |
. . . . . . . . . . . . 13
⊢ ((𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐶 − 𝐴) − 𝐶) = ((𝐶 − 𝐶) − 𝐴)) |
91 | | subid 11102 |
. . . . . . . . . . . . . . . 16
⊢ (𝐶 ∈ ℂ → (𝐶 − 𝐶) = 0) |
92 | 91 | 3ad2ant1 1135 |
. . . . . . . . . . . . . . 15
⊢ ((𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐶 − 𝐶) = 0) |
93 | 92 | oveq1d 7233 |
. . . . . . . . . . . . . 14
⊢ ((𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐶 − 𝐶) − 𝐴) = (0 − 𝐴)) |
94 | | df-neg 11070 |
. . . . . . . . . . . . . 14
⊢ -𝐴 = (0 − 𝐴) |
95 | 93, 94 | eqtr4di 2796 |
. . . . . . . . . . . . 13
⊢ ((𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐶 − 𝐶) − 𝐴) = -𝐴) |
96 | 90, 95 | eqtr2d 2778 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ) → -𝐴 = ((𝐶 − 𝐴) − 𝐶)) |
97 | 87, 89, 87, 96 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → -𝐴 = ((𝐶 − 𝐴) − 𝐶)) |
98 | 97 | 3adant2 1133 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → -𝐴 = ((𝐶 − 𝐴) − 𝐶)) |
99 | 98 | oveq1d 7233 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → (-𝐴 / 𝐵) = (((𝐶 − 𝐴) − 𝐶) / 𝐵)) |
100 | 99 | adantr 484 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (-𝐴 / 𝐵) = (((𝐶 − 𝐴) − 𝐶) / 𝐵)) |
101 | 100 | oveq1d 7233 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ((-𝐴 / 𝐵) · ((𝑝‘1) − (𝑋‘1))) = ((((𝐶 − 𝐴) − 𝐶) / 𝐵) · ((𝑝‘1) − (𝑋‘1)))) |
102 | 101 | oveq1d 7233 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (((-𝐴 / 𝐵) · ((𝑝‘1) − (𝑋‘1))) + (𝐶 / 𝐵)) = (((((𝐶 − 𝐴) − 𝐶) / 𝐵) · ((𝑝‘1) − (𝑋‘1))) + (𝐶 / 𝐵))) |
103 | 102 | eqeq2d 2748 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ((𝑝‘2) = (((-𝐴 / 𝐵) · ((𝑝‘1) − (𝑋‘1))) + (𝐶 / 𝐵)) ↔ (𝑝‘2) = (((((𝐶 − 𝐴) − 𝐶) / 𝐵) · ((𝑝‘1) − (𝑋‘1))) + (𝐶 / 𝐵)))) |
104 | 85, 103 | bitrd 282 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = (((((𝐶 − 𝐴) − 𝐶) / 𝐵) · ((𝑝‘1) − (𝑋‘1))) + (𝐶 / 𝐵)))) |
105 | | line2.y |
. . . . . . . . . . 11
⊢ 𝑌 = {〈1, 1〉, 〈2,
((𝐶 − 𝐴) / 𝐵)〉} |
106 | 105 | fveq1i 6723 |
. . . . . . . . . 10
⊢ (𝑌‘2) = ({〈1, 1〉,
〈2, ((𝐶 − 𝐴) / 𝐵)〉}‘2) |
107 | | 2ex 11912 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
V |
108 | 107 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 2 ∈
V) |
109 | | resubcl 11147 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐶 − 𝐴) ∈ ℝ) |
110 | 109 | ancoms 462 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐶 − 𝐴) ∈ ℝ) |
111 | 110 | 3adant2 1133 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → (𝐶 − 𝐴) ∈ ℝ) |
112 | 111, 30, 18 | redivcld 11665 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → ((𝐶 − 𝐴) / 𝐵) ∈ ℝ) |
113 | 72 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 1 ≠
2) |
114 | 108, 112,
113 | 3jca 1130 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → (2 ∈ V ∧
((𝐶 − 𝐴) / 𝐵) ∈ ℝ ∧ 1 ≠
2)) |
115 | 114 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (2 ∈ V ∧ ((𝐶 − 𝐴) / 𝐵) ∈ ℝ ∧ 1 ≠
2)) |
116 | | fvpr2g 7013 |
. . . . . . . . . . 11
⊢ ((2
∈ V ∧ ((𝐶 −
𝐴) / 𝐵) ∈ ℝ ∧ 1 ≠ 2) →
({〈1, 1〉, 〈2, ((𝐶 − 𝐴) / 𝐵)〉}‘2) = ((𝐶 − 𝐴) / 𝐵)) |
117 | 115, 116 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ({〈1, 1〉, 〈2,
((𝐶 − 𝐴) / 𝐵)〉}‘2) = ((𝐶 − 𝐴) / 𝐵)) |
118 | 106, 117 | syl5eq 2790 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (𝑌‘2) = ((𝐶 − 𝐴) / 𝐵)) |
119 | 68 | fveq1i 6723 |
. . . . . . . . . . 11
⊢ (𝑋‘2) = ({〈1, 0〉,
〈2, (𝐶 / 𝐵)〉}‘2) |
120 | | fvpr2g 7013 |
. . . . . . . . . . . 12
⊢ ((2
∈ V ∧ (𝐶 / 𝐵) ∈ ℝ ∧ 1 ≠ 2)
→ ({〈1, 0〉, 〈2, (𝐶 / 𝐵)〉}‘2) = (𝐶 / 𝐵)) |
121 | 107, 31, 113, 120 | mp3an2i 1468 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → ({〈1, 0〉,
〈2, (𝐶 / 𝐵)〉}‘2) = (𝐶 / 𝐵)) |
122 | 119, 121 | syl5eq 2790 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → (𝑋‘2) = (𝐶 / 𝐵)) |
123 | 122 | adantr 484 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (𝑋‘2) = (𝐶 / 𝐵)) |
124 | 118, 123 | oveq12d 7236 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ((𝑌‘2) − (𝑋‘2)) = (((𝐶 − 𝐴) / 𝐵) − (𝐶 / 𝐵))) |
125 | 29, 1 | resubcld 11265 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → (𝐶 − 𝐴) ∈ ℝ) |
126 | 125 | recnd 10866 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → (𝐶 − 𝐴) ∈ ℂ) |
127 | | divsubdir 11531 |
. . . . . . . . . . 11
⊢ (((𝐶 − 𝐴) ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → (((𝐶 − 𝐴) − 𝐶) / 𝐵) = (((𝐶 − 𝐴) / 𝐵) − (𝐶 / 𝐵))) |
128 | 126, 45, 49, 127 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → (((𝐶 − 𝐴) − 𝐶) / 𝐵) = (((𝐶 − 𝐴) / 𝐵) − (𝐶 / 𝐵))) |
129 | 128 | eqcomd 2743 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → (((𝐶 − 𝐴) / 𝐵) − (𝐶 / 𝐵)) = (((𝐶 − 𝐴) − 𝐶) / 𝐵)) |
130 | 129 | adantr 484 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (((𝐶 − 𝐴) / 𝐵) − (𝐶 / 𝐵)) = (((𝐶 − 𝐴) − 𝐶) / 𝐵)) |
131 | 124, 130 | eqtr2d 2778 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (((𝐶 − 𝐴) − 𝐶) / 𝐵) = ((𝑌‘2) − (𝑋‘2))) |
132 | 131 | oveq1d 7233 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ((((𝐶 − 𝐴) − 𝐶) / 𝐵) · ((𝑝‘1) − (𝑋‘1))) = (((𝑌‘2) − (𝑋‘2)) · ((𝑝‘1) − (𝑋‘1)))) |
133 | 132 | oveq1d 7233 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (((((𝐶 − 𝐴) − 𝐶) / 𝐵) · ((𝑝‘1) − (𝑋‘1))) + (𝐶 / 𝐵)) = ((((𝑌‘2) − (𝑋‘2)) · ((𝑝‘1) − (𝑋‘1))) + (𝐶 / 𝐵))) |
134 | 133 | eqeq2d 2748 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ((𝑝‘2) = (((((𝐶 − 𝐴) − 𝐶) / 𝐵) · ((𝑝‘1) − (𝑋‘1))) + (𝐶 / 𝐵)) ↔ (𝑝‘2) = ((((𝑌‘2) − (𝑋‘2)) · ((𝑝‘1) − (𝑋‘1))) + (𝐶 / 𝐵)))) |
135 | 105 | fveq1i 6723 |
. . . . . . . . . . . . . . 15
⊢ (𝑌‘1) = ({〈1, 1〉,
〈2, ((𝐶 − 𝐴) / 𝐵)〉}‘1) |
136 | 70, 70 | fvpr1 7010 |
. . . . . . . . . . . . . . . 16
⊢ (1 ≠ 2
→ ({〈1, 1〉, 〈2, ((𝐶 − 𝐴) / 𝐵)〉}‘1) = 1) |
137 | 72, 136 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢
({〈1, 1〉, 〈2, ((𝐶 − 𝐴) / 𝐵)〉}‘1) = 1 |
138 | 135, 137 | eqtri 2765 |
. . . . . . . . . . . . . 14
⊢ (𝑌‘1) = 1 |
139 | 70, 71 | fvpr1 7010 |
. . . . . . . . . . . . . . . 16
⊢ (1 ≠ 2
→ ({〈1, 0〉, 〈2, (𝐶 / 𝐵)〉}‘1) = 0) |
140 | 72, 139 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢
({〈1, 0〉, 〈2, (𝐶 / 𝐵)〉}‘1) = 0 |
141 | 69, 140 | eqtri 2765 |
. . . . . . . . . . . . . 14
⊢ (𝑋‘1) = 0 |
142 | 138, 141 | oveq12i 7230 |
. . . . . . . . . . . . 13
⊢ ((𝑌‘1) − (𝑋‘1)) = (1 −
0) |
143 | | 1m0e1 11956 |
. . . . . . . . . . . . 13
⊢ (1
− 0) = 1 |
144 | 142, 143 | eqtri 2765 |
. . . . . . . . . . . 12
⊢ ((𝑌‘1) − (𝑋‘1)) = 1 |
145 | 144 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → ((𝑌‘1) − (𝑋‘1)) = 1) |
146 | 145 | oveq2d 7234 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → (((𝑌‘2) − (𝑋‘2)) / ((𝑌‘1) − (𝑋‘1))) = (((𝑌‘2) − (𝑋‘2)) / 1)) |
147 | 107, 112,
113, 116 | mp3an2i 1468 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → ({〈1, 1〉,
〈2, ((𝐶 − 𝐴) / 𝐵)〉}‘2) = ((𝐶 − 𝐴) / 𝐵)) |
148 | 106, 147 | syl5eq 2790 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → (𝑌‘2) = ((𝐶 − 𝐴) / 𝐵)) |
149 | 112 | recnd 10866 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → ((𝐶 − 𝐴) / 𝐵) ∈ ℂ) |
150 | 148, 149 | eqeltrd 2838 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → (𝑌‘2) ∈ ℂ) |
151 | 122, 32 | eqeltrd 2838 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → (𝑋‘2) ∈ ℂ) |
152 | 150, 151 | subcld 11194 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → ((𝑌‘2) − (𝑋‘2)) ∈ ℂ) |
153 | 152 | div1d 11605 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → (((𝑌‘2) − (𝑋‘2)) / 1) = ((𝑌‘2) − (𝑋‘2))) |
154 | 146, 153 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → (((𝑌‘2) − (𝑋‘2)) / ((𝑌‘1) − (𝑋‘1))) = ((𝑌‘2) − (𝑋‘2))) |
155 | 154 | oveq1d 7233 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → ((((𝑌‘2) − (𝑋‘2)) / ((𝑌‘1) − (𝑋‘1))) · ((𝑝‘1) − (𝑋‘1))) = (((𝑌‘2) − (𝑋‘2)) · ((𝑝‘1) − (𝑋‘1)))) |
156 | 155, 122 | oveq12d 7236 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → (((((𝑌‘2) − (𝑋‘2)) / ((𝑌‘1) − (𝑋‘1))) · ((𝑝‘1) − (𝑋‘1))) + (𝑋‘2)) = ((((𝑌‘2) − (𝑋‘2)) · ((𝑝‘1) − (𝑋‘1))) + (𝐶 / 𝐵))) |
157 | 156 | adantr 484 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (((((𝑌‘2) − (𝑋‘2)) / ((𝑌‘1) − (𝑋‘1))) · ((𝑝‘1) − (𝑋‘1))) + (𝑋‘2)) = ((((𝑌‘2) − (𝑋‘2)) · ((𝑝‘1) − (𝑋‘1))) + (𝐶 / 𝐵))) |
158 | 157 | eqcomd 2743 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ((((𝑌‘2) − (𝑋‘2)) · ((𝑝‘1) − (𝑋‘1))) + (𝐶 / 𝐵)) = (((((𝑌‘2) − (𝑋‘2)) / ((𝑌‘1) − (𝑋‘1))) · ((𝑝‘1) − (𝑋‘1))) + (𝑋‘2))) |
159 | 158 | eqeq2d 2748 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ((𝑝‘2) = ((((𝑌‘2) − (𝑋‘2)) · ((𝑝‘1) − (𝑋‘1))) + (𝐶 / 𝐵)) ↔ (𝑝‘2) = (((((𝑌‘2) − (𝑋‘2)) / ((𝑌‘1) − (𝑋‘1))) · ((𝑝‘1) − (𝑋‘1))) + (𝑋‘2)))) |
160 | 104, 134,
159 | 3bitrd 308 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘2) = (((((𝑌‘2) − (𝑋‘2)) / ((𝑌‘1) − (𝑋‘1))) · ((𝑝‘1) − (𝑋‘1))) + (𝑋‘2)))) |
161 | 160 | rabbidva 3393 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → {𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶} = {𝑝 ∈ 𝑃 ∣ (𝑝‘2) = (((((𝑌‘2) − (𝑋‘2)) / ((𝑌‘1) − (𝑋‘1))) · ((𝑝‘1) − (𝑋‘1))) + (𝑋‘2))}) |
162 | | line2.g |
. . 3
⊢ 𝐺 = {𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶} |
163 | 162 | a1i 11 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 𝐺 = {𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶}) |
164 | 70, 107 | pm3.2i 474 |
. . . . . . . 8
⊢ (1 ∈
V ∧ 2 ∈ V) |
165 | 31, 71 | jctil 523 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → (0 ∈ V ∧
(𝐶 / 𝐵) ∈ ℝ)) |
166 | | fprg 6975 |
. . . . . . . 8
⊢ (((1
∈ V ∧ 2 ∈ V) ∧ (0 ∈ V ∧ (𝐶 / 𝐵) ∈ ℝ) ∧ 1 ≠ 2) →
{〈1, 0〉, 〈2, (𝐶 / 𝐵)〉}:{1, 2}⟶{0, (𝐶 / 𝐵)}) |
167 | 164, 165,
113, 166 | mp3an2i 1468 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → {〈1, 0〉,
〈2, (𝐶 / 𝐵)〉}:{1, 2}⟶{0,
(𝐶 / 𝐵)}) |
168 | | 0red 10841 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 0 ∈
ℝ) |
169 | 168, 31 | prssd 4740 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → {0, (𝐶 / 𝐵)} ⊆ ℝ) |
170 | 167, 169 | fssd 6568 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → {〈1, 0〉,
〈2, (𝐶 / 𝐵)〉}:{1,
2}⟶ℝ) |
171 | 68 | feq1i 6541 |
. . . . . 6
⊢ (𝑋:{1, 2}⟶ℝ ↔
{〈1, 0〉, 〈2, (𝐶 / 𝐵)〉}:{1,
2}⟶ℝ) |
172 | 170, 171 | sylibr 237 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 𝑋:{1, 2}⟶ℝ) |
173 | | reex 10825 |
. . . . . 6
⊢ ℝ
∈ V |
174 | | prex 5330 |
. . . . . 6
⊢ {1, 2}
∈ V |
175 | 173, 174 | elmap 8557 |
. . . . 5
⊢ (𝑋 ∈ (ℝ
↑m {1, 2}) ↔ 𝑋:{1, 2}⟶ℝ) |
176 | 172, 175 | sylibr 237 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 𝑋 ∈ (ℝ ↑m {1,
2})) |
177 | 3 | oveq2i 7229 |
. . . . 5
⊢ (ℝ
↑m 𝐼) =
(ℝ ↑m {1, 2}) |
178 | 4, 177 | eqtri 2765 |
. . . 4
⊢ 𝑃 = (ℝ ↑m
{1, 2}) |
179 | 176, 178 | eleqtrrdi 2849 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 𝑋 ∈ 𝑃) |
180 | 112, 70 | jctil 523 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → (1 ∈ V ∧
((𝐶 − 𝐴) / 𝐵) ∈ ℝ)) |
181 | | fprg 6975 |
. . . . . . . 8
⊢ (((1
∈ V ∧ 2 ∈ V) ∧ (1 ∈ V ∧ ((𝐶 − 𝐴) / 𝐵) ∈ ℝ) ∧ 1 ≠ 2) →
{〈1, 1〉, 〈2, ((𝐶 − 𝐴) / 𝐵)〉}:{1, 2}⟶{1, ((𝐶 − 𝐴) / 𝐵)}) |
182 | 164, 180,
113, 181 | mp3an2i 1468 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → {〈1, 1〉,
〈2, ((𝐶 − 𝐴) / 𝐵)〉}:{1, 2}⟶{1, ((𝐶 − 𝐴) / 𝐵)}) |
183 | | 1red 10839 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 1 ∈
ℝ) |
184 | 183, 112 | prssd 4740 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → {1, ((𝐶 − 𝐴) / 𝐵)} ⊆ ℝ) |
185 | 182, 184 | fssd 6568 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → {〈1, 1〉,
〈2, ((𝐶 − 𝐴) / 𝐵)〉}:{1,
2}⟶ℝ) |
186 | 105 | feq1i 6541 |
. . . . . 6
⊢ (𝑌:{1, 2}⟶ℝ ↔
{〈1, 1〉, 〈2, ((𝐶 − 𝐴) / 𝐵)〉}:{1,
2}⟶ℝ) |
187 | 185, 186 | sylibr 237 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 𝑌:{1, 2}⟶ℝ) |
188 | 173, 174 | elmap 8557 |
. . . . 5
⊢ (𝑌 ∈ (ℝ
↑m {1, 2}) ↔ 𝑌:{1, 2}⟶ℝ) |
189 | 187, 188 | sylibr 237 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 𝑌 ∈ (ℝ ↑m {1,
2})) |
190 | 189, 178 | eleqtrrdi 2849 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 𝑌 ∈ 𝑃) |
191 | | 0ne1 11906 |
. . . . 5
⊢ 0 ≠
1 |
192 | 73, 74 | ax-mp 5 |
. . . . . . 7
⊢
({〈1, 0〉, 〈2, (𝐶 / 𝐵)〉}‘1) = 0 |
193 | 69, 192 | eqtri 2765 |
. . . . . 6
⊢ (𝑋‘1) = 0 |
194 | 70, 70, 72 | 3pm3.2i 1341 |
. . . . . . . 8
⊢ (1 ∈
V ∧ 1 ∈ V ∧ 1 ≠ 2) |
195 | | fvpr1g 7012 |
. . . . . . . 8
⊢ ((1
∈ V ∧ 1 ∈ V ∧ 1 ≠ 2) → ({〈1, 1〉, 〈2,
((𝐶 − 𝐴) / 𝐵)〉}‘1) = 1) |
196 | 194, 195 | ax-mp 5 |
. . . . . . 7
⊢
({〈1, 1〉, 〈2, ((𝐶 − 𝐴) / 𝐵)〉}‘1) = 1 |
197 | 135, 196 | eqtri 2765 |
. . . . . 6
⊢ (𝑌‘1) = 1 |
198 | 193, 197 | neeq12i 3007 |
. . . . 5
⊢ ((𝑋‘1) ≠ (𝑌‘1) ↔ 0 ≠
1) |
199 | 191, 198 | mpbir 234 |
. . . 4
⊢ (𝑋‘1) ≠ (𝑌‘1) |
200 | 199 | a1i 11 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → (𝑋‘1) ≠ (𝑌‘1)) |
201 | | line2.e |
. . . 4
⊢ 𝐸 = (ℝ^‘𝐼) |
202 | | line2.l |
. . . 4
⊢ 𝐿 = (LineM‘𝐸) |
203 | | eqid 2737 |
. . . 4
⊢ (((𝑌‘2) − (𝑋‘2)) / ((𝑌‘1) − (𝑋‘1))) = (((𝑌‘2) − (𝑋‘2)) / ((𝑌‘1) − (𝑋‘1))) |
204 | 3, 201, 4, 202, 203 | rrx2linesl 45770 |
. . 3
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘1) ≠ (𝑌‘1)) → (𝑋𝐿𝑌) = {𝑝 ∈ 𝑃 ∣ (𝑝‘2) = (((((𝑌‘2) − (𝑋‘2)) / ((𝑌‘1) − (𝑋‘1))) · ((𝑝‘1) − (𝑋‘1))) + (𝑋‘2))}) |
205 | 179, 190,
200, 204 | syl3anc 1373 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → (𝑋𝐿𝑌) = {𝑝 ∈ 𝑃 ∣ (𝑝‘2) = (((((𝑌‘2) − (𝑋‘2)) / ((𝑌‘1) − (𝑋‘1))) · ((𝑝‘1) − (𝑋‘1))) + (𝑋‘2))}) |
206 | 161, 163,
205 | 3eqtr4d 2787 |
1
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 𝐺 = (𝑋𝐿𝑌)) |