Theorem sharhght 39703

Description: Let 𝐴𝐵𝐶 be a triangle, and let 𝐷 lie on the line 𝐴𝐵. Then (doubled) areas of triangles 𝐴𝐷𝐶 and 𝐶𝐷𝐵 relate as lengths of corresponding bases 𝐴𝐷 and 𝐷𝐵. (Contributed by Saveliy Skresanov, 23-Sep-2017.)

Hypotheses

Ref	Expression
sharhght.sigar	⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦)))
sharhght.a	⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ))
sharhght.b	⊢ (𝜑 → (𝐷 ∈ ℂ ∧ ((𝐴 − 𝐷)𝐺(𝐵 − 𝐷)) = 0))

Assertion

Ref	Expression
sharhght	⊢ (𝜑 → (((𝐶 − 𝐴)𝐺(𝐷 − 𝐴)) · (𝐵 − 𝐷)) = (((𝐶 − 𝐵)𝐺(𝐷 − 𝐵)) · (𝐴 − 𝐷)))

Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝑥,𝐶,𝑦   𝑥,𝐷,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐺(𝑥,𝑦)

Proof of Theorem sharhght

Step	Hyp	Ref	Expression
1		sharhght.a	. . . . . . . . 9 ⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ))
2	1	simp3d 1068	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ ℂ)
3	1	simp1d 1066	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ ℂ)
4	2, 3	subcld 10271	. . . . . . 7 ⊢ (𝜑 → (𝐶 − 𝐴) ∈ ℂ)
5	4	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝐵 = 𝐷) → (𝐶 − 𝐴) ∈ ℂ)
6		sharhght.b	. . . . . . . . 9 ⊢ (𝜑 → (𝐷 ∈ ℂ ∧ ((𝐴 − 𝐷)𝐺(𝐵 − 𝐷)) = 0))
7	6	simpld 474	. . . . . . . 8 ⊢ (𝜑 → 𝐷 ∈ ℂ)
8	7, 3	subcld 10271	. . . . . . 7 ⊢ (𝜑 → (𝐷 − 𝐴) ∈ ℂ)
9	8	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝐵 = 𝐷) → (𝐷 − 𝐴) ∈ ℂ)
10		sharhght.sigar	. . . . . . 7 ⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦)))
11	10	sigarim 39689	. . . . . 6 ⊢ (((𝐶 − 𝐴) ∈ ℂ ∧ (𝐷 − 𝐴) ∈ ℂ) → ((𝐶 − 𝐴)𝐺(𝐷 − 𝐴)) ∈ ℝ)
12	5, 9, 11	syl2anc 691	. . . . 5 ⊢ ((𝜑 ∧ 𝐵 = 𝐷) → ((𝐶 − 𝐴)𝐺(𝐷 − 𝐴)) ∈ ℝ)
13	12	recnd 9947	. . . 4 ⊢ ((𝜑 ∧ 𝐵 = 𝐷) → ((𝐶 − 𝐴)𝐺(𝐷 − 𝐴)) ∈ ℂ)
14	13	mul01d 10114	. . 3 ⊢ ((𝜑 ∧ 𝐵 = 𝐷) → (((𝐶 − 𝐴)𝐺(𝐷 − 𝐴)) · 0) = 0)
15	1	simp2d 1067	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ ℂ)
16	15	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝐵 = 𝐷) → 𝐵 ∈ ℂ)
17		simpr 476	. . . . 5 ⊢ ((𝜑 ∧ 𝐵 = 𝐷) → 𝐵 = 𝐷)
18	16, 17	subeq0bd 10335	. . . 4 ⊢ ((𝜑 ∧ 𝐵 = 𝐷) → (𝐵 − 𝐷) = 0)
19	18	oveq2d 6565	. . 3 ⊢ ((𝜑 ∧ 𝐵 = 𝐷) → (((𝐶 − 𝐴)𝐺(𝐷 − 𝐴)) · (𝐵 − 𝐷)) = (((𝐶 − 𝐴)𝐺(𝐷 − 𝐴)) · 0))
20	2, 15	subcld 10271	. . . . . . . 8 ⊢ (𝜑 → (𝐶 − 𝐵) ∈ ℂ)
21	20	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐵 = 𝐷) → (𝐶 − 𝐵) ∈ ℂ)
22	7, 15	subcld 10271	. . . . . . . 8 ⊢ (𝜑 → (𝐷 − 𝐵) ∈ ℂ)
23	22	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐵 = 𝐷) → (𝐷 − 𝐵) ∈ ℂ)
24	10	sigarval 39688	. . . . . . 7 ⊢ (((𝐶 − 𝐵) ∈ ℂ ∧ (𝐷 − 𝐵) ∈ ℂ) → ((𝐶 − 𝐵)𝐺(𝐷 − 𝐵)) = (ℑ‘((∗‘(𝐶 − 𝐵)) · (𝐷 − 𝐵))))
25	21, 23, 24	syl2anc 691	. . . . . 6 ⊢ ((𝜑 ∧ 𝐵 = 𝐷) → ((𝐶 − 𝐵)𝐺(𝐷 − 𝐵)) = (ℑ‘((∗‘(𝐶 − 𝐵)) · (𝐷 − 𝐵))))
26	7	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 = 𝐷) → 𝐷 ∈ ℂ)
27	17	eqcomd 2616	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 = 𝐷) → 𝐷 = 𝐵)
28	26, 27	subeq0bd 10335	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐵 = 𝐷) → (𝐷 − 𝐵) = 0)
29	28	oveq2d 6565	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐵 = 𝐷) → ((∗‘(𝐶 − 𝐵)) · (𝐷 − 𝐵)) = ((∗‘(𝐶 − 𝐵)) · 0))
30	21	cjcld 13784	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐵 = 𝐷) → (∗‘(𝐶 − 𝐵)) ∈ ℂ)
31	30	mul01d 10114	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐵 = 𝐷) → ((∗‘(𝐶 − 𝐵)) · 0) = 0)
32	29, 31	eqtrd 2644	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐵 = 𝐷) → ((∗‘(𝐶 − 𝐵)) · (𝐷 − 𝐵)) = 0)
33	32	fveq2d 6107	. . . . . 6 ⊢ ((𝜑 ∧ 𝐵 = 𝐷) → (ℑ‘((∗‘(𝐶 − 𝐵)) · (𝐷 − 𝐵))) = (ℑ‘0))
34		0red 9920	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐵 = 𝐷) → 0 ∈ ℝ)
35	34	reim0d 13813	. . . . . 6 ⊢ ((𝜑 ∧ 𝐵 = 𝐷) → (ℑ‘0) = 0)
36	25, 33, 35	3eqtrd 2648	. . . . 5 ⊢ ((𝜑 ∧ 𝐵 = 𝐷) → ((𝐶 − 𝐵)𝐺(𝐷 − 𝐵)) = 0)
37	36	oveq1d 6564	. . . 4 ⊢ ((𝜑 ∧ 𝐵 = 𝐷) → (((𝐶 − 𝐵)𝐺(𝐷 − 𝐵)) · (𝐴 − 𝐷)) = (0 · (𝐴 − 𝐷)))
38	3	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝐵 = 𝐷) → 𝐴 ∈ ℂ)
39	38, 26	subcld 10271	. . . . 5 ⊢ ((𝜑 ∧ 𝐵 = 𝐷) → (𝐴 − 𝐷) ∈ ℂ)
40	39	mul02d 10113	. . . 4 ⊢ ((𝜑 ∧ 𝐵 = 𝐷) → (0 · (𝐴 − 𝐷)) = 0)
41	37, 40	eqtrd 2644	. . 3 ⊢ ((𝜑 ∧ 𝐵 = 𝐷) → (((𝐶 − 𝐵)𝐺(𝐷 − 𝐵)) · (𝐴 − 𝐷)) = 0)
42	14, 19, 41	3eqtr4d 2654	. 2 ⊢ ((𝜑 ∧ 𝐵 = 𝐷) → (((𝐶 − 𝐴)𝐺(𝐷 − 𝐴)) · (𝐵 − 𝐷)) = (((𝐶 − 𝐵)𝐺(𝐷 − 𝐵)) · (𝐴 − 𝐷)))
43	2	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐷) → 𝐶 ∈ ℂ)
44	15	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐷) → 𝐵 ∈ ℂ)
45	3	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐷) → 𝐴 ∈ ℂ)
46	43, 44, 45	npncand 10295	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐷) → ((𝐶 − 𝐵) + (𝐵 − 𝐴)) = (𝐶 − 𝐴))
47	46	oveq1d 6564	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐷) → (((𝐶 − 𝐵) + (𝐵 − 𝐴))𝐺(𝐷 − 𝐴)) = ((𝐶 − 𝐴)𝐺(𝐷 − 𝐴)))
48	43, 44	subcld 10271	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐷) → (𝐶 − 𝐵) ∈ ℂ)
49	8	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐷) → (𝐷 − 𝐴) ∈ ℂ)
50	44, 45	subcld 10271	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐷) → (𝐵 − 𝐴) ∈ ℂ)
51	10	sigaraf 39691	. . . . . . . 8 ⊢ (((𝐶 − 𝐵) ∈ ℂ ∧ (𝐷 − 𝐴) ∈ ℂ ∧ (𝐵 − 𝐴) ∈ ℂ) → (((𝐶 − 𝐵) + (𝐵 − 𝐴))𝐺(𝐷 − 𝐴)) = (((𝐶 − 𝐵)𝐺(𝐷 − 𝐴)) + ((𝐵 − 𝐴)𝐺(𝐷 − 𝐴))))
52	48, 49, 50, 51	syl3anc 1318	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐷) → (((𝐶 − 𝐵) + (𝐵 − 𝐴))𝐺(𝐷 − 𝐴)) = (((𝐶 − 𝐵)𝐺(𝐷 − 𝐴)) + ((𝐵 − 𝐴)𝐺(𝐷 − 𝐴))))
53	47, 52	eqtr3d 2646	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐷) → ((𝐶 − 𝐴)𝐺(𝐷 − 𝐴)) = (((𝐶 − 𝐵)𝐺(𝐷 − 𝐴)) + ((𝐵 − 𝐴)𝐺(𝐷 − 𝐴))))
54	6	simprd 478	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴 − 𝐷)𝐺(𝐵 − 𝐷)) = 0)
55	54	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐷) → ((𝐴 − 𝐷)𝐺(𝐵 − 𝐷)) = 0)
56	7	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐷) → 𝐷 ∈ ℂ)
57	10	sigarperm 39698	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ) → ((𝐴 − 𝐷)𝐺(𝐵 − 𝐷)) = ((𝐵 − 𝐴)𝐺(𝐷 − 𝐴)))
58	45, 44, 56, 57	syl3anc 1318	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐷) → ((𝐴 − 𝐷)𝐺(𝐵 − 𝐷)) = ((𝐵 − 𝐴)𝐺(𝐷 − 𝐴)))
59	55, 58	eqtr3d 2646	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐷) → 0 = ((𝐵 − 𝐴)𝐺(𝐷 − 𝐴)))
60	59	oveq2d 6565	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐷) → (((𝐶 − 𝐵)𝐺(𝐷 − 𝐴)) + 0) = (((𝐶 − 𝐵)𝐺(𝐷 − 𝐴)) + ((𝐵 − 𝐴)𝐺(𝐷 − 𝐴))))
61	10	sigarim 39689	. . . . . . . . 9 ⊢ (((𝐶 − 𝐵) ∈ ℂ ∧ (𝐷 − 𝐴) ∈ ℂ) → ((𝐶 − 𝐵)𝐺(𝐷 − 𝐴)) ∈ ℝ)
62	48, 49, 61	syl2anc 691	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐷) → ((𝐶 − 𝐵)𝐺(𝐷 − 𝐴)) ∈ ℝ)
63	62	recnd 9947	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐷) → ((𝐶 − 𝐵)𝐺(𝐷 − 𝐴)) ∈ ℂ)
64	63	addid1d 10115	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐷) → (((𝐶 − 𝐵)𝐺(𝐷 − 𝐴)) + 0) = ((𝐶 − 𝐵)𝐺(𝐷 − 𝐴)))
65	53, 60, 64	3eqtr2d 2650	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐷) → ((𝐶 − 𝐴)𝐺(𝐷 − 𝐴)) = ((𝐶 − 𝐵)𝐺(𝐷 − 𝐴)))
66	44, 56	negsubdi2d 10287	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐷) → -(𝐵 − 𝐷) = (𝐷 − 𝐵))
67	66	eqcomd 2616	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐷) → (𝐷 − 𝐵) = -(𝐵 − 𝐷))
68	67	oveq1d 6564	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐷) → ((𝐷 − 𝐵) / (𝐵 − 𝐷)) = (-(𝐵 − 𝐷) / (𝐵 − 𝐷)))
69	44, 56	subcld 10271	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐷) → (𝐵 − 𝐷) ∈ ℂ)
70		simpr 476	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐷) → ¬ 𝐵 = 𝐷)
71	70	neqned 2789	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐷) → 𝐵 ≠ 𝐷)
72	44, 56, 71	subne0d 10280	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐷) → (𝐵 − 𝐷) ≠ 0)
73	69, 69, 72	divnegd 10693	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐷) → -((𝐵 − 𝐷) / (𝐵 − 𝐷)) = (-(𝐵 − 𝐷) / (𝐵 − 𝐷)))
74	69, 72	dividd 10678	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐷) → ((𝐵 − 𝐷) / (𝐵 − 𝐷)) = 1)
75	74	negeqd 10154	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐷) → -((𝐵 − 𝐷) / (𝐵 − 𝐷)) = -1)
76	68, 73, 75	3eqtr2d 2650	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐷) → ((𝐷 − 𝐵) / (𝐵 − 𝐷)) = -1)
77	76	oveq1d 6564	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐷) → (((𝐷 − 𝐵) / (𝐵 − 𝐷)) · (𝐴 − 𝐷)) = (-1 · (𝐴 − 𝐷)))
78	45, 56	subcld 10271	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐷) → (𝐴 − 𝐷) ∈ ℂ)
79	78	mulm1d 10361	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐷) → (-1 · (𝐴 − 𝐷)) = -(𝐴 − 𝐷))
80	45, 56	negsubdi2d 10287	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐷) → -(𝐴 − 𝐷) = (𝐷 − 𝐴))
81	77, 79, 80	3eqtrd 2648	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐷) → (((𝐷 − 𝐵) / (𝐵 − 𝐷)) · (𝐴 − 𝐷)) = (𝐷 − 𝐴))
82	56, 44	subcld 10271	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐷) → (𝐷 − 𝐵) ∈ ℂ)
83	82, 69, 78, 72	div32d 10703	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐷) → (((𝐷 − 𝐵) / (𝐵 − 𝐷)) · (𝐴 − 𝐷)) = ((𝐷 − 𝐵) · ((𝐴 − 𝐷) / (𝐵 − 𝐷))))
84	81, 83	eqtr3d 2646	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐷) → (𝐷 − 𝐴) = ((𝐷 − 𝐵) · ((𝐴 − 𝐷) / (𝐵 − 𝐷))))
85	84	oveq2d 6565	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐷) → ((𝐶 − 𝐵)𝐺(𝐷 − 𝐴)) = ((𝐶 − 𝐵)𝐺((𝐷 − 𝐵) · ((𝐴 − 𝐷) / (𝐵 − 𝐷)))))
86	56, 45, 44	3jca 1235	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐷) → (𝐷 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ))
87	10, 86, 70, 55	sigardiv 39699	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐷) → ((𝐴 − 𝐷) / (𝐵 − 𝐷)) ∈ ℝ)
88	10	sigarls 39695	. . . . . 6 ⊢ (((𝐶 − 𝐵) ∈ ℂ ∧ (𝐷 − 𝐵) ∈ ℂ ∧ ((𝐴 − 𝐷) / (𝐵 − 𝐷)) ∈ ℝ) → ((𝐶 − 𝐵)𝐺((𝐷 − 𝐵) · ((𝐴 − 𝐷) / (𝐵 − 𝐷)))) = (((𝐶 − 𝐵)𝐺(𝐷 − 𝐵)) · ((𝐴 − 𝐷) / (𝐵 − 𝐷))))
89	48, 82, 87, 88	syl3anc 1318	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐷) → ((𝐶 − 𝐵)𝐺((𝐷 − 𝐵) · ((𝐴 − 𝐷) / (𝐵 − 𝐷)))) = (((𝐶 − 𝐵)𝐺(𝐷 − 𝐵)) · ((𝐴 − 𝐷) / (𝐵 − 𝐷))))
90	65, 85, 89	3eqtrd 2648	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐷) → ((𝐶 − 𝐴)𝐺(𝐷 − 𝐴)) = (((𝐶 − 𝐵)𝐺(𝐷 − 𝐵)) · ((𝐴 − 𝐷) / (𝐵 − 𝐷))))
91	90	oveq1d 6564	. . 3 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐷) → (((𝐶 − 𝐴)𝐺(𝐷 − 𝐴)) · (𝐵 − 𝐷)) = ((((𝐶 − 𝐵)𝐺(𝐷 − 𝐵)) · ((𝐴 − 𝐷) / (𝐵 − 𝐷))) · (𝐵 − 𝐷)))
92	10	sigarim 39689	. . . . . 6 ⊢ (((𝐶 − 𝐵) ∈ ℂ ∧ (𝐷 − 𝐵) ∈ ℂ) → ((𝐶 − 𝐵)𝐺(𝐷 − 𝐵)) ∈ ℝ)
93	92	recnd 9947	. . . . 5 ⊢ (((𝐶 − 𝐵) ∈ ℂ ∧ (𝐷 − 𝐵) ∈ ℂ) → ((𝐶 − 𝐵)𝐺(𝐷 − 𝐵)) ∈ ℂ)
94	48, 82, 93	syl2anc 691	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐷) → ((𝐶 − 𝐵)𝐺(𝐷 − 𝐵)) ∈ ℂ)
95	78, 69, 72	divcld 10680	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐷) → ((𝐴 − 𝐷) / (𝐵 − 𝐷)) ∈ ℂ)
96	94, 95, 69	mulassd 9942	. . 3 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐷) → ((((𝐶 − 𝐵)𝐺(𝐷 − 𝐵)) · ((𝐴 − 𝐷) / (𝐵 − 𝐷))) · (𝐵 − 𝐷)) = (((𝐶 − 𝐵)𝐺(𝐷 − 𝐵)) · (((𝐴 − 𝐷) / (𝐵 − 𝐷)) · (𝐵 − 𝐷))))
97	78, 69, 72	divcan1d 10681	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐷) → (((𝐴 − 𝐷) / (𝐵 − 𝐷)) · (𝐵 − 𝐷)) = (𝐴 − 𝐷))
98	97	oveq2d 6565	. . 3 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐷) → (((𝐶 − 𝐵)𝐺(𝐷 − 𝐵)) · (((𝐴 − 𝐷) / (𝐵 − 𝐷)) · (𝐵 − 𝐷))) = (((𝐶 − 𝐵)𝐺(𝐷 − 𝐵)) · (𝐴 − 𝐷)))
99	91, 96, 98	3eqtrd 2648	. 2 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐷) → (((𝐶 − 𝐴)𝐺(𝐷 − 𝐴)) · (𝐵 − 𝐷)) = (((𝐶 − 𝐵)𝐺(𝐷 − 𝐵)) · (𝐴 − 𝐷)))
100	42, 99	pm2.61dan 828	1 ⊢ (𝜑 → (((𝐶 − 𝐴)𝐺(𝐷 − 𝐴)) · (𝐵 − 𝐷)) = (((𝐶 − 𝐵)𝐺(𝐷 − 𝐵)) · (𝐴 − 𝐷)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977  ‘cfv 5804  (class class class)co 6549   ↦ cmpt2 6551  ℂcc 9813  ℝcr 9814  0cc0 9815  1c1 9816   + caddc 9818   · cmul 9820   − cmin 10145  -cneg 10146   / cdiv 10563  ∗ccj 13684  ℑcim 13686

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-po 4959  df-so 4960  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-2 10956  df-cj 13687  df-re 13688  df-im 13689

This theorem is referenced by:  cevathlem2  39706