Theorem line2 49957

Description: Example for a line 𝐺 passing through two different points in "standard form". (Contributed by AV, 3-Feb-2023.)

Hypotheses

Ref	Expression
line2.i	⊢ 𝐼 = (0..^2)
line2.e	⊢ 𝐸 = (ℝ^‘𝐼)
line2.p	⊢ 𝑃 = (ℝ ↑m 𝐼)
line2.l	⊢ 𝐿 = (LineM‘𝐸)
line2.g	⊢ 𝐺 = {𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘0)) + (𝐵 · (𝑝‘1))) = 𝐶}
line2.x	⊢ 𝑋 = ⟨“0(𝐶 / 𝐵)”⟩
line2.y	⊢ 𝑌 = ⟨“1((𝐶 − 𝐴) / 𝐵)”⟩

Assertion

Ref	Expression
line2	⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 𝐺 = (𝑋𝐿𝑌))

Distinct variable groups:   𝐴,𝑝   𝐵,𝑝   𝐶,𝑝   𝐸,𝑝   𝐼,𝑝   𝑃,𝑝   𝑋,𝑝   𝑌,𝑝

Allowed substitution hints:   𝐺(𝑝)   𝐿(𝑝)

Proof of Theorem line2

Step	Hyp	Ref	Expression
1		simp1 1154	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 𝐴 ∈ ℝ)
2	1	adantr 486	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → 𝐴 ∈ ℝ)
3		line2.i	. . . . . . . . . . . . . 14 ⊢ 𝐼 = (0..^2)
4		line2.p	. . . . . . . . . . . . . 14 ⊢ 𝑃 = (ℝ ↑m 𝐼)
5	3, 4	rrx2pxel 49916	. . . . . . . . . . . . 13 ⊢ (𝑝 ∈ 𝑃 → (𝑝‘0) ∈ ℝ)
6	5	adantl 487	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (𝑝‘0) ∈ ℝ)
7	2, 6	remulcld 11342	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (𝐴 · (𝑝‘0)) ∈ ℝ)
8	7	recnd 11340	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (𝐴 · (𝑝‘0)) ∈ ℂ)
9		simpl2l 1245	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → 𝐵 ∈ ℝ)
10	3, 4	rrx2pyel 49917	. . . . . . . . . . . . 13 ⊢ (𝑝 ∈ 𝑃 → (𝑝‘1) ∈ ℝ)
11	10	adantl 487	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (𝑝‘1) ∈ ℝ)
12	9, 11	remulcld 11342	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (𝐵 · (𝑝‘1)) ∈ ℝ)
13	12	recnd 11340	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (𝐵 · (𝑝‘1)) ∈ ℂ)
14		simpl 488	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → 𝐵 ∈ ℝ)
15	14	recnd 11340	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → 𝐵 ∈ ℂ)
16	15	3ad2ant2 1152	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 𝐵 ∈ ℂ)
17	16	adantr 486	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → 𝐵 ∈ ℂ)
18		simp2r 1219	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 𝐵 ≠ 0)
19	18	adantr 486	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → 𝐵 ≠ 0)
20	8, 13, 17, 19	divdird 12134	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (((𝐴 · (𝑝‘0)) + (𝐵 · (𝑝‘1))) / 𝐵) = (((𝐴 · (𝑝‘0)) / 𝐵) + ((𝐵 · (𝑝‘1)) / 𝐵)))
21	10	recnd 11340	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ 𝑃 → (𝑝‘1) ∈ ℂ)
22	21	adantl 487	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (𝑝‘1) ∈ ℂ)
23	22, 17, 19	divcan3d 12101	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ((𝐵 · (𝑝‘1)) / 𝐵) = (𝑝‘1))
24	23	oveq2d 7436	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (((𝐴 · (𝑝‘0)) / 𝐵) + ((𝐵 · (𝑝‘1)) / 𝐵)) = (((𝐴 · (𝑝‘0)) / 𝐵) + (𝑝‘1)))
25	20, 24	eqtrd 2795	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (((𝐴 · (𝑝‘0)) + (𝐵 · (𝑝‘1))) / 𝐵) = (((𝐴 · (𝑝‘0)) / 𝐵) + (𝑝‘1)))
26	25	eqeq1d 2762	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ((((𝐴 · (𝑝‘0)) + (𝐵 · (𝑝‘1))) / 𝐵) = (𝐶 / 𝐵) ↔ (((𝐴 · (𝑝‘0)) / 𝐵) + (𝑝‘1)) = (𝐶 / 𝐵)))
27	7, 9, 19	redivcld 12148	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ((𝐴 · (𝑝‘0)) / 𝐵) ∈ ℝ)
28	27	recnd 11340	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ((𝐴 · (𝑝‘0)) / 𝐵) ∈ ℂ)
29		simp3 1156	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 𝐶 ∈ ℝ)
30	14	3ad2ant2 1152	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 𝐵 ∈ ℝ)
31	29, 30, 18	redivcld 12148	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → (𝐶 / 𝐵) ∈ ℝ)
32	31	recnd 11340	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → (𝐶 / 𝐵) ∈ ℂ)
33	32	adantr 486	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (𝐶 / 𝐵) ∈ ℂ)
34	28, 22, 33	addrsub 11736	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ((((𝐴 · (𝑝‘0)) / 𝐵) + (𝑝‘1)) = (𝐶 / 𝐵) ↔ (𝑝‘1) = ((𝐶 / 𝐵) − ((𝐴 · (𝑝‘0)) / 𝐵))))
35	28, 33	negsubdi2d 11688	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → -(((𝐴 · (𝑝‘0)) / 𝐵) − (𝐶 / 𝐵)) = ((𝐶 / 𝐵) − ((𝐴 · (𝑝‘0)) / 𝐵)))
36	28, 33	negsubdid 11687	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → -(((𝐴 · (𝑝‘0)) / 𝐵) − (𝐶 / 𝐵)) = ( -((𝐴 · (𝑝‘0)) / 𝐵) + (𝐶 / 𝐵)))
37	35, 36	eqtr3d 2797	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ((𝐶 / 𝐵) − ((𝐴 · (𝑝‘0)) / 𝐵)) = ( -((𝐴 · (𝑝‘0)) / 𝐵) + (𝐶 / 𝐵)))
38	37	eqeq2d 2771	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ((𝑝‘1) = ((𝐶 / 𝐵) − ((𝐴 · (𝑝‘0)) / 𝐵)) ↔ (𝑝‘1) = ( -((𝐴 · (𝑝‘0)) / 𝐵) + (𝐶 / 𝐵))))
39	26, 34, 38	3bitrd 308	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ((((𝐴 · (𝑝‘0)) + (𝐵 · (𝑝‘1))) / 𝐵) = (𝐶 / 𝐵) ↔ (𝑝‘1) = ( -((𝐴 · (𝑝‘0)) / 𝐵) + (𝐶 / 𝐵))))
40	7, 12	readdcld 11341	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ((𝐴 · (𝑝‘0)) + (𝐵 · (𝑝‘1))) ∈ ℝ)
41	40	recnd 11340	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ((𝐴 · (𝑝‘0)) + (𝐵 · (𝑝‘1))) ∈ ℂ)
42	29	recnd 11340	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 𝐶 ∈ ℂ)
43	42	adantr 486	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → 𝐶 ∈ ℂ)
44		recn 11293	. . . . . . . . . 10 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℂ)
45	44	anim1i 627	. . . . . . . . 9 ⊢ ((𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0))
46	45	3ad2ant2 1152	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0))
47	46	adantr 486	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0))
48		div11 12005	. . . . . . 7 ⊢ ((((𝐴 · (𝑝‘0)) + (𝐵 · (𝑝‘1))) ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → ((((𝐴 · (𝑝‘0)) + (𝐵 · (𝑝‘1))) / 𝐵) = (𝐶 / 𝐵) ↔ ((𝐴 · (𝑝‘0)) + (𝐵 · (𝑝‘1))) = 𝐶))
49	41, 43, 47, 48	syl3anc 1398	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ((((𝐴 · (𝑝‘0)) + (𝐵 · (𝑝‘1))) / 𝐵) = (𝐶 / 𝐵) ↔ ((𝐴 · (𝑝‘0)) + (𝐵 · (𝑝‘1))) = 𝐶))
50	8, 17, 19	divnegd 12109	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → -((𝐴 · (𝑝‘0)) / 𝐵) = ( -(𝐴 · (𝑝‘0)) / 𝐵))
51	1	recnd 11340	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 𝐴 ∈ ℂ)
52	51	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → 𝐴 ∈ ℂ)
53	5	recnd 11340	. . . . . . . . . . . . . 14 ⊢ (𝑝 ∈ 𝑃 → (𝑝‘0) ∈ ℂ)
54	53	adantl 487	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (𝑝‘0) ∈ ℂ)
55	52, 54	mulneg1d 11772	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ( -𝐴 · (𝑝‘0)) = -(𝐴 · (𝑝‘0)))
56	55	eqcomd 2766	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → -(𝐴 · (𝑝‘0)) = ( -𝐴 · (𝑝‘0)))
57	56	oveq1d 7435	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ( -(𝐴 · (𝑝‘0)) / 𝐵) = (( -𝐴 · (𝑝‘0)) / 𝐵))
58	50, 57	eqtrd 2795	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → -((𝐴 · (𝑝‘0)) / 𝐵) = (( -𝐴 · (𝑝‘0)) / 𝐵))
59		renegcl 11624	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℝ → -𝐴 ∈ ℝ)
60	59	recnd 11340	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℝ → -𝐴 ∈ ℂ)
61	60	3ad2ant1 1151	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → -𝐴 ∈ ℂ)
62	61	adantr 486	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → -𝐴 ∈ ℂ)
63		div23 11996	. . . . . . . . . 10 ⊢ (( -𝐴 ∈ ℂ ∧ (𝑝‘0) ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → (( -𝐴 · (𝑝‘0)) / 𝐵) = (( -𝐴 / 𝐵) · (𝑝‘0)))
64	62, 54, 47, 63	syl3anc 1398	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (( -𝐴 · (𝑝‘0)) / 𝐵) = (( -𝐴 / 𝐵) · (𝑝‘0)))
65		line2.x	. . . . . . . . . . . . . . 15 ⊢ 𝑋 = ⟨“0(𝐶 / 𝐵)”⟩
66	65	fveq1i 6886	. . . . . . . . . . . . . 14 ⊢ (𝑋‘0) = (⟨“0(𝐶 / 𝐵)”⟩‘0)
67		0re 11313	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ ℝ
68		s2fv0 15042	. . . . . . . . . . . . . . 15 ⊢ (0 ∈ ℝ → (⟨“0(𝐶 / 𝐵)”⟩‘0) = 0)
69	67, 68	mp1i 14	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → (⟨“0(𝐶 / 𝐵)”⟩‘0) = 0)
70	66, 69	eqtrid 2807	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → (𝑋‘0) = 0)
71	70	adantr 486	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (𝑋‘0) = 0)
72	71	oveq2d 7436	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ((𝑝‘0) − (𝑋‘0)) = ((𝑝‘0) − 0))
73	54	subid1d 11661	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ((𝑝‘0) − 0) = (𝑝‘0))
74	72, 73	eqtr2d 2796	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (𝑝‘0) = ((𝑝‘0) − (𝑋‘0)))
75	74	oveq2d 7436	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (( -𝐴 / 𝐵) · (𝑝‘0)) = (( -𝐴 / 𝐵) · ((𝑝‘0) − (𝑋‘0))))
76	58, 64, 75	3eqtrd 2799	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → -((𝐴 · (𝑝‘0)) / 𝐵) = (( -𝐴 / 𝐵) · ((𝑝‘0) − (𝑋‘0))))
77	76	oveq1d 7435	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ( -((𝐴 · (𝑝‘0)) / 𝐵) + (𝐶 / 𝐵)) = ((( -𝐴 / 𝐵) · ((𝑝‘0) − (𝑋‘0))) + (𝐶 / 𝐵)))
78	77	eqeq2d 2771	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ((𝑝‘1) = ( -((𝐴 · (𝑝‘0)) / 𝐵) + (𝐶 / 𝐵)) ↔ (𝑝‘1) = ((( -𝐴 / 𝐵) · ((𝑝‘0) − (𝑋‘0))) + (𝐶 / 𝐵))))
79	39, 49, 78	3bitr3d 312	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (((𝐴 · (𝑝‘0)) + (𝐵 · (𝑝‘1))) = 𝐶 ↔ (𝑝‘1) = ((( -𝐴 / 𝐵) · ((𝑝‘0) − (𝑋‘0))) + (𝐶 / 𝐵))))
80		recn 11293	. . . . . . . . . . . . 13 ⊢ (𝐶 ∈ ℝ → 𝐶 ∈ ℂ)
81	80	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐶 ∈ ℂ)
82		recn 11293	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
83	82	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐴 ∈ ℂ)
84		sub32 11595	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐶 − 𝐴) − 𝐶) = ((𝐶 − 𝐶) − 𝐴))
85		subid 11580	. . . . . . . . . . . . . . . 16 ⊢ (𝐶 ∈ ℂ → (𝐶 − 𝐶) = 0)
86	85	3ad2ant1 1151	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐶 − 𝐶) = 0)
87	86	oveq1d 7435	. . . . . . . . . . . . . 14 ⊢ ((𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐶 − 𝐶) − 𝐴) = (0 − 𝐴))
88		df-neg 11547	. . . . . . . . . . . . . 14 ⊢ -𝐴 = (0 − 𝐴)
89	87, 88	eqtr4di 2813	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐶 − 𝐶) − 𝐴) = -𝐴)
90	84, 89	eqtr2d 2796	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ) → -𝐴 = ((𝐶 − 𝐴) − 𝐶))
91	81, 83, 81, 90	syl3anc 1398	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → -𝐴 = ((𝐶 − 𝐴) − 𝐶))
92	91	3adant2 1149	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → -𝐴 = ((𝐶 − 𝐴) − 𝐶))
93	92	oveq1d 7435	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → ( -𝐴 / 𝐵) = (((𝐶 − 𝐴) − 𝐶) / 𝐵))
94	93	adantr 486	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ( -𝐴 / 𝐵) = (((𝐶 − 𝐴) − 𝐶) / 𝐵))
95	94	oveq1d 7435	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (( -𝐴 / 𝐵) · ((𝑝‘0) − (𝑋‘0))) = ((((𝐶 − 𝐴) − 𝐶) / 𝐵) · ((𝑝‘0) − (𝑋‘0))))
96	95	oveq1d 7435	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ((( -𝐴 / 𝐵) · ((𝑝‘0) − (𝑋‘0))) + (𝐶 / 𝐵)) = (((((𝐶 − 𝐴) − 𝐶) / 𝐵) · ((𝑝‘0) − (𝑋‘0))) + (𝐶 / 𝐵)))
97	96	eqeq2d 2771	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ((𝑝‘1) = ((( -𝐴 / 𝐵) · ((𝑝‘0) − (𝑋‘0))) + (𝐶 / 𝐵)) ↔ (𝑝‘1) = (((((𝐶 − 𝐴) − 𝐶) / 𝐵) · ((𝑝‘0) − (𝑋‘0))) + (𝐶 / 𝐵))))
98	79, 97	bitrd 282	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (((𝐴 · (𝑝‘0)) + (𝐵 · (𝑝‘1))) = 𝐶 ↔ (𝑝‘1) = (((((𝐶 − 𝐴) − 𝐶) / 𝐵) · ((𝑝‘0) − (𝑋‘0))) + (𝐶 / 𝐵))))
99		line2.y	. . . . . . . . . . 11 ⊢ 𝑌 = ⟨“1((𝐶 − 𝐴) / 𝐵)”⟩
100	99	fveq1i 6886	. . . . . . . . . 10 ⊢ (𝑌‘1) = (⟨“1((𝐶 − 𝐴) / 𝐵)”⟩‘1)
101		resubcl 11625	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐶 − 𝐴) ∈ ℝ)
102	101	ancoms 464	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐶 − 𝐴) ∈ ℝ)
103	102	3adant2 1149	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → (𝐶 − 𝐴) ∈ ℝ)
104	103, 30, 18	redivcld 12148	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → ((𝐶 − 𝐴) / 𝐵) ∈ ℝ)
105	104	adantr 486	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ((𝐶 − 𝐴) / 𝐵) ∈ ℝ)
106		s2fv1 15043	. . . . . . . . . . 11 ⊢ (((𝐶 − 𝐴) / 𝐵) ∈ ℝ → (⟨“1((𝐶 − 𝐴) / 𝐵)”⟩‘1) = ((𝐶 − 𝐴) / 𝐵))
107	105, 106	syl 18	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (⟨“1((𝐶 − 𝐴) / 𝐵)”⟩‘1) = ((𝐶 − 𝐴) / 𝐵))
108	100, 107	eqtrid 2807	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (𝑌‘1) = ((𝐶 − 𝐴) / 𝐵))
109	65	fveq1i 6886	. . . . . . . . . . 11 ⊢ (𝑋‘1) = (⟨“0(𝐶 / 𝐵)”⟩‘1)
110		s2fv1 15043	. . . . . . . . . . . 12 ⊢ ((𝐶 / 𝐵) ∈ ℝ → (⟨“0(𝐶 / 𝐵)”⟩‘1) = (𝐶 / 𝐵))
111	31, 110	syl 18	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → (⟨“0(𝐶 / 𝐵)”⟩‘1) = (𝐶 / 𝐵))
112	109, 111	eqtrid 2807	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → (𝑋‘1) = (𝐶 / 𝐵))
113	112	adantr 486	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (𝑋‘1) = (𝐶 / 𝐵))
114	108, 113	oveq12d 7438	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ((𝑌‘1) − (𝑋‘1)) = (((𝐶 − 𝐴) / 𝐵) − (𝐶 / 𝐵)))
115	103	recnd 11340	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → (𝐶 − 𝐴) ∈ ℂ)
116		divsubdir 12013	. . . . . . . . . . 11 ⊢ (((𝐶 − 𝐴) ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → (((𝐶 − 𝐴) − 𝐶) / 𝐵) = (((𝐶 − 𝐴) / 𝐵) − (𝐶 / 𝐵)))
117	115, 42, 46, 116	syl3anc 1398	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → (((𝐶 − 𝐴) − 𝐶) / 𝐵) = (((𝐶 − 𝐴) / 𝐵) − (𝐶 / 𝐵)))
118	117	eqcomd 2766	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → (((𝐶 − 𝐴) / 𝐵) − (𝐶 / 𝐵)) = (((𝐶 − 𝐴) − 𝐶) / 𝐵))
119	118	adantr 486	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (((𝐶 − 𝐴) / 𝐵) − (𝐶 / 𝐵)) = (((𝐶 − 𝐴) − 𝐶) / 𝐵))
120	114, 119	eqtr2d 2796	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (((𝐶 − 𝐴) − 𝐶) / 𝐵) = ((𝑌‘1) − (𝑋‘1)))
121	120	oveq1d 7435	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ((((𝐶 − 𝐴) − 𝐶) / 𝐵) · ((𝑝‘0) − (𝑋‘0))) = (((𝑌‘1) − (𝑋‘1)) · ((𝑝‘0) − (𝑋‘0))))
122	121	oveq1d 7435	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (((((𝐶 − 𝐴) − 𝐶) / 𝐵) · ((𝑝‘0) − (𝑋‘0))) + (𝐶 / 𝐵)) = ((((𝑌‘1) − (𝑋‘1)) · ((𝑝‘0) − (𝑋‘0))) + (𝐶 / 𝐵)))
123	122	eqeq2d 2771	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ((𝑝‘1) = (((((𝐶 − 𝐴) − 𝐶) / 𝐵) · ((𝑝‘0) − (𝑋‘0))) + (𝐶 / 𝐵)) ↔ (𝑝‘1) = ((((𝑌‘1) − (𝑋‘1)) · ((𝑝‘0) − (𝑋‘0))) + (𝐶 / 𝐵))))
124	99	fveq1i 6886	. . . . . . . . . . . . . . 15 ⊢ (𝑌‘0) = (⟨“1((𝐶 − 𝐴) / 𝐵)”⟩‘0)
125		1re 11311	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℝ
126		s2fv0 15042	. . . . . . . . . . . . . . . 16 ⊢ (1 ∈ ℝ → (⟨“1((𝐶 − 𝐴) / 𝐵)”⟩‘0) = 1)
127	125, 126	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (⟨“1((𝐶 − 𝐴) / 𝐵)”⟩‘0) = 1
128	124, 127	eqtri 2783	. . . . . . . . . . . . . 14 ⊢ (𝑌‘0) = 1
129	67, 68	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (⟨“0(𝐶 / 𝐵)”⟩‘0) = 0
130	66, 129	eqtri 2783	. . . . . . . . . . . . . 14 ⊢ (𝑋‘0) = 0
131	128, 130	oveq12i 7432	. . . . . . . . . . . . 13 ⊢ ((𝑌‘0) − (𝑋‘0)) = (1 − 0)
132		1m0e1 12465	. . . . . . . . . . . . 13 ⊢ (1 − 0) = 1
133	131, 132	eqtri 2783	. . . . . . . . . . . 12 ⊢ ((𝑌‘0) − (𝑋‘0)) = 1
134	133	a1i 11	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → ((𝑌‘0) − (𝑋‘0)) = 1)
135	134	oveq2d 7436	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → (((𝑌‘1) − (𝑋‘1)) / ((𝑌‘0) − (𝑋‘0))) = (((𝑌‘1) − (𝑋‘1)) / 1))
136	104, 106	syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → (⟨“1((𝐶 − 𝐴) / 𝐵)”⟩‘1) = ((𝐶 − 𝐴) / 𝐵))
137	100, 136	eqtrid 2807	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → (𝑌‘1) = ((𝐶 − 𝐴) / 𝐵))
138	104	recnd 11340	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → ((𝐶 − 𝐴) / 𝐵) ∈ ℂ)
139	137, 138	eqeltrd 2860	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → (𝑌‘1) ∈ ℂ)
140	112, 32	eqeltrd 2860	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → (𝑋‘1) ∈ ℂ)
141	139, 140	subcld 11672	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → ((𝑌‘1) − (𝑋‘1)) ∈ ℂ)
142	141	div1d 12088	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → (((𝑌‘1) − (𝑋‘1)) / 1) = ((𝑌‘1) − (𝑋‘1)))
143	135, 142	eqtrd 2795	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → (((𝑌‘1) − (𝑋‘1)) / ((𝑌‘0) − (𝑋‘0))) = ((𝑌‘1) − (𝑋‘1)))
144	143	oveq1d 7435	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → ((((𝑌‘1) − (𝑋‘1)) / ((𝑌‘0) − (𝑋‘0))) · ((𝑝‘0) − (𝑋‘0))) = (((𝑌‘1) − (𝑋‘1)) · ((𝑝‘0) − (𝑋‘0))))
145	144, 112	oveq12d 7438	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → (((((𝑌‘1) − (𝑋‘1)) / ((𝑌‘0) − (𝑋‘0))) · ((𝑝‘0) − (𝑋‘0))) + (𝑋‘1)) = ((((𝑌‘1) − (𝑋‘1)) · ((𝑝‘0) − (𝑋‘0))) + (𝐶 / 𝐵)))
146	145	adantr 486	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (((((𝑌‘1) − (𝑋‘1)) / ((𝑌‘0) − (𝑋‘0))) · ((𝑝‘0) − (𝑋‘0))) + (𝑋‘1)) = ((((𝑌‘1) − (𝑋‘1)) · ((𝑝‘0) − (𝑋‘0))) + (𝐶 / 𝐵)))
147	146	eqcomd 2766	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ((((𝑌‘1) − (𝑋‘1)) · ((𝑝‘0) − (𝑋‘0))) + (𝐶 / 𝐵)) = (((((𝑌‘1) − (𝑋‘1)) / ((𝑌‘0) − (𝑋‘0))) · ((𝑝‘0) − (𝑋‘0))) + (𝑋‘1)))
148	147	eqeq2d 2771	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → ((𝑝‘1) = ((((𝑌‘1) − (𝑋‘1)) · ((𝑝‘0) − (𝑋‘0))) + (𝐶 / 𝐵)) ↔ (𝑝‘1) = (((((𝑌‘1) − (𝑋‘1)) / ((𝑌‘0) − (𝑋‘0))) · ((𝑝‘0) − (𝑋‘0))) + (𝑋‘1))))
149	98, 123, 148	3bitrd 308	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) ∧ 𝑝 ∈ 𝑃) → (((𝐴 · (𝑝‘0)) + (𝐵 · (𝑝‘1))) = 𝐶 ↔ (𝑝‘1) = (((((𝑌‘1) − (𝑋‘1)) / ((𝑌‘0) − (𝑋‘0))) · ((𝑝‘0) − (𝑋‘0))) + (𝑋‘1))))
150	149	rabbidva 3418	. 2 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → {𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘0)) + (𝐵 · (𝑝‘1))) = 𝐶} = {𝑝 ∈ 𝑃 ∣ (𝑝‘1) = (((((𝑌‘1) − (𝑋‘1)) / ((𝑌‘0) − (𝑋‘0))) · ((𝑝‘0) − (𝑋‘0))) + (𝑋‘1))})
151		line2.g	. . 3 ⊢ 𝐺 = {𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘0)) + (𝐵 · (𝑝‘1))) = 𝐶}
152	151	a1i 11	. 2 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 𝐺 = {𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘0)) + (𝐵 · (𝑝‘1))) = 𝐶})
153		1ex 11306	. . . . . . . . 9 ⊢ 1 ∈ V
154		2ex 12423	. . . . . . . . 9 ⊢ 2 ∈ V
155	153, 154	pm3.2i 476	. . . . . . . 8 ⊢ (1 ∈ V ∧ 2 ∈ V)
156		c0ex 11303	. . . . . . . . 9 ⊢ 0 ∈ V
157	31, 156	jctil 529	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → (0 ∈ V ∧ (𝐶 / 𝐵) ∈ ℝ))
158		1ne2 12556	. . . . . . . . 9 ⊢ 1 ≠ 2
159	158	a1i 11	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 1 ≠ 2)
160		s2len 15044	. . . . . . . . . . 11 ⊢ (♯‘⟨“0(𝐶 / 𝐵)”⟩) = 2
161	160	a1i 11	. . . . . . . . . 10 ⊢ (((1 ∈ V ∧ 2 ∈ V) ∧ (0 ∈ V ∧ (𝐶 / 𝐵) ∈ ℝ) ∧ 1 ≠ 2) → (♯‘⟨“0(𝐶 / 𝐵)”⟩) = 2)
162	161	eqcomd 2766	. . . . . . . . 9 ⊢ (((1 ∈ V ∧ 2 ∈ V) ∧ (0 ∈ V ∧ (𝐶 / 𝐵) ∈ ℝ) ∧ 1 ≠ 2) → 2 = (♯‘⟨“0(𝐶 / 𝐵)”⟩))
163		prid1g 4717	. . . . . . . . . . 11 ⊢ (0 ∈ ℝ → 0 ∈ {0, (𝐶 / 𝐵)})
164	67, 163	mp1i 14	. . . . . . . . . 10 ⊢ (((1 ∈ V ∧ 2 ∈ V) ∧ (0 ∈ V ∧ (𝐶 / 𝐵) ∈ ℝ) ∧ 1 ≠ 2) → 0 ∈ {0, (𝐶 / 𝐵)})
165		simp2r 1219	. . . . . . . . . . 11 ⊢ (((1 ∈ V ∧ 2 ∈ V) ∧ (0 ∈ V ∧ (𝐶 / 𝐵) ∈ ℝ) ∧ 1 ≠ 2) → (𝐶 / 𝐵) ∈ ℝ)
166		prid2g 4718	. . . . . . . . . . 11 ⊢ ((𝐶 / 𝐵) ∈ ℝ → (𝐶 / 𝐵) ∈ {0, (𝐶 / 𝐵)})
167	165, 166	syl 18	. . . . . . . . . 10 ⊢ (((1 ∈ V ∧ 2 ∈ V) ∧ (0 ∈ V ∧ (𝐶 / 𝐵) ∈ ℝ) ∧ 1 ≠ 2) → (𝐶 / 𝐵) ∈ {0, (𝐶 / 𝐵)})
168	164, 167	s2cld 15026	. . . . . . . . 9 ⊢ (((1 ∈ V ∧ 2 ∈ V) ∧ (0 ∈ V ∧ (𝐶 / 𝐵) ∈ ℝ) ∧ 1 ≠ 2) → ⟨“0(𝐶 / 𝐵)”⟩ ∈ Word {0, (𝐶 / 𝐵)})
169	162, 168	wrdfd 14667	. . . . . . . 8 ⊢ (((1 ∈ V ∧ 2 ∈ V) ∧ (0 ∈ V ∧ (𝐶 / 𝐵) ∈ ℝ) ∧ 1 ≠ 2) → ⟨“0(𝐶 / 𝐵)”⟩:(0..^2)⟶{0, (𝐶 / 𝐵)})
170	155, 157, 159, 169	mp3an2i 1495	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → ⟨“0(𝐶 / 𝐵)”⟩:(0..^2)⟶{0, (𝐶 / 𝐵)})
171		0red 11314	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 0 ∈ ℝ)
172	171, 31	prssd 4777	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → {0, (𝐶 / 𝐵)} ⊆ ℝ)
173	170, 172	fssd 6727	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → ⟨“0(𝐶 / 𝐵)”⟩:(0..^2)⟶ℝ)
174	65	feq1i 6700	. . . . . 6 ⊢ (𝑋:(0..^2)⟶ℝ ↔ ⟨“0(𝐶 / 𝐵)”⟩:(0..^2)⟶ℝ)
175	173, 174	sylibr 237	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 𝑋:(0..^2)⟶ℝ)
176		reex 11294	. . . . . 6 ⊢ ℝ ∈ V
177		ovex 7453	. . . . . 6 ⊢ (0..^2) ∈ V
178	176, 177	elmap 8902	. . . . 5 ⊢ (𝑋 ∈ (ℝ ↑m (0..^2)) ↔ 𝑋:(0..^2)⟶ℝ)
179	175, 178	sylibr 237	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 𝑋 ∈ (ℝ ↑m (0..^2)))
180	3	oveq2i 7431	. . . . 5 ⊢ (ℝ ↑m 𝐼) = (ℝ ↑m (0..^2))
181	4, 180	eqtri 2783	. . . 4 ⊢ 𝑃 = (ℝ ↑m (0..^2))
182	179, 181	eleqtrrdi 2871	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 𝑋 ∈ 𝑃)
183	104, 153	jctil 529	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → (1 ∈ V ∧ ((𝐶 − 𝐴) / 𝐵) ∈ ℝ))
184		s2len 15044	. . . . . . . . . . 11 ⊢ (♯‘⟨“1((𝐶 − 𝐴) / 𝐵)”⟩) = 2
185	184	a1i 11	. . . . . . . . . 10 ⊢ (((1 ∈ V ∧ 2 ∈ V) ∧ (1 ∈ V ∧ ((𝐶 − 𝐴) / 𝐵) ∈ ℝ) ∧ 1 ≠ 2) → (♯‘⟨“1((𝐶 − 𝐴) / 𝐵)”⟩) = 2)
186	185	eqcomd 2766	. . . . . . . . 9 ⊢ (((1 ∈ V ∧ 2 ∈ V) ∧ (1 ∈ V ∧ ((𝐶 − 𝐴) / 𝐵) ∈ ℝ) ∧ 1 ≠ 2) → 2 = (♯‘⟨“1((𝐶 − 𝐴) / 𝐵)”⟩))
187		prid1g 4717	. . . . . . . . . . 11 ⊢ (1 ∈ ℝ → 1 ∈ {1, ((𝐶 − 𝐴) / 𝐵)})
188	125, 187	mp1i 14	. . . . . . . . . 10 ⊢ (((1 ∈ V ∧ 2 ∈ V) ∧ (1 ∈ V ∧ ((𝐶 − 𝐴) / 𝐵) ∈ ℝ) ∧ 1 ≠ 2) → 1 ∈ {1, ((𝐶 − 𝐴) / 𝐵)})
189		simp2r 1219	. . . . . . . . . . 11 ⊢ (((1 ∈ V ∧ 2 ∈ V) ∧ (1 ∈ V ∧ ((𝐶 − 𝐴) / 𝐵) ∈ ℝ) ∧ 1 ≠ 2) → ((𝐶 − 𝐴) / 𝐵) ∈ ℝ)
190		prid2g 4718	. . . . . . . . . . 11 ⊢ (((𝐶 − 𝐴) / 𝐵) ∈ ℝ → ((𝐶 − 𝐴) / 𝐵) ∈ {1, ((𝐶 − 𝐴) / 𝐵)})
191	189, 190	syl 18	. . . . . . . . . 10 ⊢ (((1 ∈ V ∧ 2 ∈ V) ∧ (1 ∈ V ∧ ((𝐶 − 𝐴) / 𝐵) ∈ ℝ) ∧ 1 ≠ 2) → ((𝐶 − 𝐴) / 𝐵) ∈ {1, ((𝐶 − 𝐴) / 𝐵)})
192	188, 191	s2cld 15026	. . . . . . . . 9 ⊢ (((1 ∈ V ∧ 2 ∈ V) ∧ (1 ∈ V ∧ ((𝐶 − 𝐴) / 𝐵) ∈ ℝ) ∧ 1 ≠ 2) → ⟨“1((𝐶 − 𝐴) / 𝐵)”⟩ ∈ Word {1, ((𝐶 − 𝐴) / 𝐵)})
193	186, 192	wrdfd 14667	. . . . . . . 8 ⊢ (((1 ∈ V ∧ 2 ∈ V) ∧ (1 ∈ V ∧ ((𝐶 − 𝐴) / 𝐵) ∈ ℝ) ∧ 1 ≠ 2) → ⟨“1((𝐶 − 𝐴) / 𝐵)”⟩:(0..^2)⟶{1, ((𝐶 − 𝐴) / 𝐵)})
194	155, 183, 159, 193	mp3an2i 1495	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → ⟨“1((𝐶 − 𝐴) / 𝐵)”⟩:(0..^2)⟶{1, ((𝐶 − 𝐴) / 𝐵)})
195		1red 11312	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 1 ∈ ℝ)
196	195, 104	prssd 4777	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → {1, ((𝐶 − 𝐴) / 𝐵)} ⊆ ℝ)
197	194, 196	fssd 6727	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → ⟨“1((𝐶 − 𝐴) / 𝐵)”⟩:(0..^2)⟶ℝ)
198	99	feq1i 6700	. . . . . 6 ⊢ (𝑌:(0..^2)⟶ℝ ↔ ⟨“1((𝐶 − 𝐴) / 𝐵)”⟩:(0..^2)⟶ℝ)
199	197, 198	sylibr 237	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 𝑌:(0..^2)⟶ℝ)
200	176, 177	elmap 8902	. . . . 5 ⊢ (𝑌 ∈ (ℝ ↑m (0..^2)) ↔ 𝑌:(0..^2)⟶ℝ)
201	199, 200	sylibr 237	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 𝑌 ∈ (ℝ ↑m (0..^2)))
202	201, 181	eleqtrrdi 2871	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 𝑌 ∈ 𝑃)
203		0ne1 12417	. . . . 5 ⊢ 0 ≠ 1
204	130, 128	neeq12i 3021	. . . . 5 ⊢ ((𝑋‘0) ≠ (𝑌‘0) ↔ 0 ≠ 1)
205	203, 204	mpbir 234	. . . 4 ⊢ (𝑋‘0) ≠ (𝑌‘0)
206	205	a1i 11	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → (𝑋‘0) ≠ (𝑌‘0))
207		line2.e	. . . 4 ⊢ 𝐸 = (ℝ^‘𝐼)
208		line2.l	. . . 4 ⊢ 𝐿 = (LineM‘𝐸)
209		eqid 2760	. . . 4 ⊢ (((𝑌‘1) − (𝑋‘1)) / ((𝑌‘0) − (𝑋‘0))) = (((𝑌‘1) − (𝑋‘1)) / ((𝑌‘0) − (𝑋‘0)))
210	3, 207, 4, 208, 209	rrx2linesl 49948	. . 3 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘0) ≠ (𝑌‘0)) → (𝑋𝐿𝑌) = {𝑝 ∈ 𝑃 ∣ (𝑝‘1) = (((((𝑌‘1) − (𝑋‘1)) / ((𝑌‘0) − (𝑋‘0))) · ((𝑝‘0) − (𝑋‘0))) + (𝑋‘1))})
211	182, 202, 206, 210	syl3anc 1398	. 2 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → (𝑋𝐿𝑌) = {𝑝 ∈ 𝑃 ∣ (𝑝‘1) = (((((𝑌‘1) − (𝑋‘1)) / ((𝑌‘0) − (𝑋‘0))) · ((𝑝‘0) − (𝑋‘0))) + (𝑋‘1))})
212	150, 152, 211	3eqtr4d 2805	1 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℝ) → 𝐺 = (𝑋𝐿𝑌))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1569   ∈ wcel 2144   ≠ wne 2955  {crab 3412  Vcvv 3450  {cpr 4586  ⟶wf 6534  ‘cfv 6538  (class class class)co 7420   ↑_m cmap 8850  ℂcc 11201  ℝcr 11202  0cc0 11203  1c1 11204   + caddc 11206   · cmul 11208   − cmin 11544   -cneg 11545   / cdiv 11976  2c2 12400  ..^cfzo 13791  ♯chash 14477  ⟨“cs2 14996  ℝ^crrx 25709  Line_Mcline 49933

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-cnex 11259  ax-resscn 11260  ax-1cn 11261  ax-icn 11262  ax-addcl 11263  ax-addrcl 11264  ax-mulcl 11265  ax-mulrcl 11266  ax-mulcom 11267  ax-addass 11268  ax-mulass 11269  ax-distr 11270  ax-i2m1 11271  ax-1ne0 11272  ax-1rid 11273  ax-rnegex 11274  ax-rrecex 11275  ax-cnre 11276  ax-pre-lttri 11277  ax-pre-lttrn 11278  ax-pre-ltadd 11279  ax-pre-mulgt0 11280  ax-pre-sup 11281  ax-addf 11282  ax-mulf 11283

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4835  df-uni 4867  df-int 4907  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-of 7693  df-om 7878  df-1st 8001  df-2nd 8002  df-supp 8180  df-tpos 8246  df-frecs 8302  df-wrecs 8333  df-recs 8382  df-rdg 8421  df-1o 8479  df-er 8720  df-map 8852  df-ixp 8929  df-en 8977  df-dom 8978  df-sdom 8979  df-fin 8980  df-fsupp 9357  df-sup 9437  df-card 10023  df-pnf 11348  df-mnf 11349  df-xr 11350  df-ltxr 11351  df-le 11352  df-sub 11546  df-neg 11547  df-div 11977  df-nn 12339  df-2 12408  df-3 12409  df-4 12410  df-5 12411  df-6 12412  df-7 12413  df-8 12414  df-9 12415  df-n0 12610  df-z 12697  df-dec 12818  df-uz 12969  df-rp 13124  df-fz 13643  df-fzo 13792  df-seq 14148  df-exp 14208  df-hash 14478  df-word 14662  df-concat 14719  df-s1 14746  df-s2 15003  df-cj 15271  df-re 15272  df-im 15273  df-sqrt 15407  df-abs 15408  df-struct 17330  df-sets 17347  df-slot 17365  df-ndx 17377  df-base 17393  df-ress 17414  df-plusg 17446  df-mulr 17447  df-starv 17448  df-sca 17449  df-vsca 17450  df-ip 17451  df-tset 17452  df-ple 17453  df-ds 17455  df-unif 17456  df-hom 17457  df-cco 17458  df-0g 17617  df-prds 17623  df-pws 17625  df-mgm 18821  df-sgrp 18913  df-mnd 18929  df-mhm 18983  df-grp 19152  df-minusg 19153  df-sbg 19154  df-subg 19338  df-ghm 19433  df-cmn 20001  df-abl 20002  df-mgp 20366  df-rng 20380  df-ur 20413  df-ring 20466  df-cring 20467  df-oppr 20572  df-dvdsr 20592  df-unit 20593  df-invr 20623  df-dvr 20636  df-rhm 20707  df-subrng 20803  df-subrg 20827  df-drng 20987  df-field 20988  df-staf 21101  df-srng 21102  df-lmod 21142  df-lss 21212  df-sra 21453  df-rgmod 21454  df-cnfld 21684  df-refld 21916  df-dsmm 22043  df-frlm 22058  df-tng 24908  df-tcph 25495  df-rrx 25711  df-line 49935

This theorem is used by: (None)