isosctrlem3

Description: Lemma for isosctr . Corresponds to the case where one vertex is at 0. (Contributed by Saveliy Skresanov, 1-Jan-2017)

		Ref	Expression
	Hypothesis	isosctrlem3.1	$⊢ F = (x \in (ℂ ∖ \{0\}), y \in (ℂ ∖ \{0\}) ⟼ ℑ (\log (\frac{y}{x})))$
	Assertion	isosctrlem3	$⊢ ((A \in ℂ \land B \in ℂ) \land (A \neq 0 \land B \neq 0 \land A \neq B) \land \|A\| = \|B\|) \to (- A) F (B - A) = (A - B) F (- B)$

Proof

Step	Hyp	Ref	Expression
1		isosctrlem3.1	$⊢ F = (x \in (ℂ ∖ \{0\}), y \in (ℂ ∖ \{0\}) ⟼ ℑ (\log (\frac{y}{x})))$
2		simp1l	$⊢ ((A \in ℂ \land B \in ℂ) \land (A \neq 0 \land B \neq 0 \land A \neq B) \land \|A\| = \|B\|) \to A \in ℂ$
3		simp21	$⊢ ((A \in ℂ \land B \in ℂ) \land (A \neq 0 \land B \neq 0 \land A \neq B) \land \|A\| = \|B\|) \to A \neq 0$
4		simp1r	$⊢ ((A \in ℂ \land B \in ℂ) \land (A \neq 0 \land B \neq 0 \land A \neq B) \land \|A\| = \|B\|) \to B \in ℂ$
5	2 4	subcld	$⊢ ((A \in ℂ \land B \in ℂ) \land (A \neq 0 \land B \neq 0 \land A \neq B) \land \|A\| = \|B\|) \to A - B \in ℂ$
6		simp23	$⊢ ((A \in ℂ \land B \in ℂ) \land (A \neq 0 \land B \neq 0 \land A \neq B) \land \|A\| = \|B\|) \to A \neq B$
7	2 4 6	subne0d	$⊢ ((A \in ℂ \land B \in ℂ) \land (A \neq 0 \land B \neq 0 \land A \neq B) \land \|A\| = \|B\|) \to A - B \neq 0$
8	1	angneg	$⊢ ((A \in ℂ \land A \neq 0) \land (A - B \in ℂ \land A - B \neq 0)) \to (- A) F (- (A - B)) = A F (A - B)$
9	2 3 5 7 8	syl22anc	$⊢ ((A \in ℂ \land B \in ℂ) \land (A \neq 0 \land B \neq 0 \land A \neq B) \land \|A\| = \|B\|) \to (- A) F (- (A - B)) = A F (A - B)$
10	2 4	negsubdi2d	$⊢ ((A \in ℂ \land B \in ℂ) \land (A \neq 0 \land B \neq 0 \land A \neq B) \land \|A\| = \|B\|) \to - (A - B) = B - A$
11	10	oveq2d	$⊢ ((A \in ℂ \land B \in ℂ) \land (A \neq 0 \land B \neq 0 \land A \neq B) \land \|A\| = \|B\|) \to (- A) F (- (A - B)) = (- A) F (B - A)$
12		1cnd	$⊢ ((A \in ℂ \land B \in ℂ) \land (A \neq 0 \land B \neq 0 \land A \neq B) \land \|A\| = \|B\|) \to 1 \in ℂ$
13		ax-1ne0	$⊢ 1 \neq 0$
14	13	a1i	$⊢ ((A \in ℂ \land B \in ℂ) \land (A \neq 0 \land B \neq 0 \land A \neq B) \land \|A\| = \|B\|) \to 1 \neq 0$
15	4 2 3	divcld	$⊢ ((A \in ℂ \land B \in ℂ) \land (A \neq 0 \land B \neq 0 \land A \neq B) \land \|A\| = \|B\|) \to \frac{B}{A} \in ℂ$
16	12 15	subcld	$⊢ ((A \in ℂ \land B \in ℂ) \land (A \neq 0 \land B \neq 0 \land A \neq B) \land \|A\| = \|B\|) \to 1 - (\frac{B}{A}) \in ℂ$
17	6	necomd	$⊢ ((A \in ℂ \land B \in ℂ) \land (A \neq 0 \land B \neq 0 \land A \neq B) \land \|A\| = \|B\|) \to B \neq A$
18	4 2 3 17	divne1d	$⊢ ((A \in ℂ \land B \in ℂ) \land (A \neq 0 \land B \neq 0 \land A \neq B) \land \|A\| = \|B\|) \to \frac{B}{A} \neq 1$
19	18	necomd	$⊢ ((A \in ℂ \land B \in ℂ) \land (A \neq 0 \land B \neq 0 \land A \neq B) \land \|A\| = \|B\|) \to 1 \neq \frac{B}{A}$
20	12 15 19	subne0d	$⊢ ((A \in ℂ \land B \in ℂ) \land (A \neq 0 \land B \neq 0 \land A \neq B) \land \|A\| = \|B\|) \to 1 - (\frac{B}{A}) \neq 0$
21	1 12 14 16 20	angvald	$⊢ ((A \in ℂ \land B \in ℂ) \land (A \neq 0 \land B \neq 0 \land A \neq B) \land \|A\| = \|B\|) \to 1 F (1 - (\frac{B}{A})) = ℑ (\log (\frac{1 - (\frac{B}{A})}{1}))$
22	16	div1d	$⊢ ((A \in ℂ \land B \in ℂ) \land (A \neq 0 \land B \neq 0 \land A \neq B) \land \|A\| = \|B\|) \to \frac{1 - (\frac{B}{A})}{1} = 1 - (\frac{B}{A})$
23	22	fveq2d	$⊢ ((A \in ℂ \land B \in ℂ) \land (A \neq 0 \land B \neq 0 \land A \neq B) \land \|A\| = \|B\|) \to \log (\frac{1 - (\frac{B}{A})}{1}) = \log (1 - (\frac{B}{A}))$
24	23	fveq2d	$⊢ ((A \in ℂ \land B \in ℂ) \land (A \neq 0 \land B \neq 0 \land A \neq B) \land \|A\| = \|B\|) \to ℑ (\log (\frac{1 - (\frac{B}{A})}{1})) = ℑ (\log (1 - (\frac{B}{A})))$
25	4 2 3	absdivd	$⊢ ((A \in ℂ \land B \in ℂ) \land (A \neq 0 \land B \neq 0 \land A \neq B) \land \|A\| = \|B\|) \to \|\frac{B}{A}\| = \frac{\|B\|}{\|A\|}$
26		simp3	$⊢ ((A \in ℂ \land B \in ℂ) \land (A \neq 0 \land B \neq 0 \land A \neq B) \land \|A\| = \|B\|) \to \|A\| = \|B\|$
27	26	eqcomd	$⊢ ((A \in ℂ \land B \in ℂ) \land (A \neq 0 \land B \neq 0 \land A \neq B) \land \|A\| = \|B\|) \to \|B\| = \|A\|$
28	27	oveq1d	$⊢ ((A \in ℂ \land B \in ℂ) \land (A \neq 0 \land B \neq 0 \land A \neq B) \land \|A\| = \|B\|) \to \frac{\|B\|}{\|A\|} = \frac{\|A\|}{\|A\|}$
29	2	abscld	$⊢ ((A \in ℂ \land B \in ℂ) \land (A \neq 0 \land B \neq 0 \land A \neq B) \land \|A\| = \|B\|) \to \|A\| \in ℝ$
30	29	recnd	$⊢ ((A \in ℂ \land B \in ℂ) \land (A \neq 0 \land B \neq 0 \land A \neq B) \land \|A\| = \|B\|) \to \|A\| \in ℂ$
31	2 3	absne0d	$⊢ ((A \in ℂ \land B \in ℂ) \land (A \neq 0 \land B \neq 0 \land A \neq B) \land \|A\| = \|B\|) \to \|A\| \neq 0$
32	30 31	dividd	$⊢ ((A \in ℂ \land B \in ℂ) \land (A \neq 0 \land B \neq 0 \land A \neq B) \land \|A\| = \|B\|) \to \frac{\|A\|}{\|A\|} = 1$
33	25 28 32	3eqtrd	$⊢ ((A \in ℂ \land B \in ℂ) \land (A \neq 0 \land B \neq 0 \land A \neq B) \land \|A\| = \|B\|) \to \|\frac{B}{A}\| = 1$
34	19	neneqd	$⊢ ((A \in ℂ \land B \in ℂ) \land (A \neq 0 \land B \neq 0 \land A \neq B) \land \|A\| = \|B\|) \to \neg 1 = \frac{B}{A}$
35		isosctrlem2	$⊢ (\frac{B}{A} \in ℂ \land \|\frac{B}{A}\| = 1 \land \neg 1 = \frac{B}{A}) \to ℑ (\log (1 - (\frac{B}{A}))) = ℑ (\log (\frac{- \frac{B}{A}}{1 - (\frac{B}{A})}))$
36	15 33 34 35	syl3anc	$⊢ ((A \in ℂ \land B \in ℂ) \land (A \neq 0 \land B \neq 0 \land A \neq B) \land \|A\| = \|B\|) \to ℑ (\log (1 - (\frac{B}{A}))) = ℑ (\log (\frac{- \frac{B}{A}}{1 - (\frac{B}{A})}))$
37	15	negcld	$⊢ ((A \in ℂ \land B \in ℂ) \land (A \neq 0 \land B \neq 0 \land A \neq B) \land \|A\| = \|B\|) \to - \frac{B}{A} \in ℂ$
38		simp22	$⊢ ((A \in ℂ \land B \in ℂ) \land (A \neq 0 \land B \neq 0 \land A \neq B) \land \|A\| = \|B\|) \to B \neq 0$
39	4 2 38 3	divne0d	$⊢ ((A \in ℂ \land B \in ℂ) \land (A \neq 0 \land B \neq 0 \land A \neq B) \land \|A\| = \|B\|) \to \frac{B}{A} \neq 0$
40	15 39	negne0d	$⊢ ((A \in ℂ \land B \in ℂ) \land (A \neq 0 \land B \neq 0 \land A \neq B) \land \|A\| = \|B\|) \to - \frac{B}{A} \neq 0$
41	1 16 20 37 40	angvald	$⊢ ((A \in ℂ \land B \in ℂ) \land (A \neq 0 \land B \neq 0 \land A \neq B) \land \|A\| = \|B\|) \to (1 - (\frac{B}{A})) F (- \frac{B}{A}) = ℑ (\log (\frac{- \frac{B}{A}}{1 - (\frac{B}{A})}))$
42	36 41	eqtr4d	$⊢ ((A \in ℂ \land B \in ℂ) \land (A \neq 0 \land B \neq 0 \land A \neq B) \land \|A\| = \|B\|) \to ℑ (\log (1 - (\frac{B}{A}))) = (1 - (\frac{B}{A})) F (- \frac{B}{A})$
43	21 24 42	3eqtrd	$⊢ ((A \in ℂ \land B \in ℂ) \land (A \neq 0 \land B \neq 0 \land A \neq B) \land \|A\| = \|B\|) \to 1 F (1 - (\frac{B}{A})) = (1 - (\frac{B}{A})) F (- \frac{B}{A})$
44	2	mulid1d	$⊢ ((A \in ℂ \land B \in ℂ) \land (A \neq 0 \land B \neq 0 \land A \neq B) \land \|A\| = \|B\|) \to A \cdot 1 = A$
45	2 12 15	subdid	$⊢ ((A \in ℂ \land B \in ℂ) \land (A \neq 0 \land B \neq 0 \land A \neq B) \land \|A\| = \|B\|) \to A (1 - (\frac{B}{A})) = A \cdot 1 - A (\frac{B}{A})$
46	4 2 3	divcan2d	$⊢ ((A \in ℂ \land B \in ℂ) \land (A \neq 0 \land B \neq 0 \land A \neq B) \land \|A\| = \|B\|) \to A (\frac{B}{A}) = B$
47	44 46	oveq12d	$⊢ ((A \in ℂ \land B \in ℂ) \land (A \neq 0 \land B \neq 0 \land A \neq B) \land \|A\| = \|B\|) \to A \cdot 1 - A (\frac{B}{A}) = A - B$
48	45 47	eqtrd	$⊢ ((A \in ℂ \land B \in ℂ) \land (A \neq 0 \land B \neq 0 \land A \neq B) \land \|A\| = \|B\|) \to A (1 - (\frac{B}{A})) = A - B$
49	44 48	oveq12d	$⊢ ((A \in ℂ \land B \in ℂ) \land (A \neq 0 \land B \neq 0 \land A \neq B) \land \|A\| = \|B\|) \to A \cdot 1 F A (1 - (\frac{B}{A})) = A F (A - B)$
50	1	angcan	$⊢ ((1 \in ℂ \land 1 \neq 0) \land (1 - (\frac{B}{A}) \in ℂ \land 1 - (\frac{B}{A}) \neq 0) \land (A \in ℂ \land A \neq 0)) \to A \cdot 1 F A (1 - (\frac{B}{A})) = 1 F (1 - (\frac{B}{A}))$
51	12 14 16 20 2 3 50	syl222anc	$⊢ ((A \in ℂ \land B \in ℂ) \land (A \neq 0 \land B \neq 0 \land A \neq B) \land \|A\| = \|B\|) \to A \cdot 1 F A (1 - (\frac{B}{A})) = 1 F (1 - (\frac{B}{A}))$
52	49 51	eqtr3d	$⊢ ((A \in ℂ \land B \in ℂ) \land (A \neq 0 \land B \neq 0 \land A \neq B) \land \|A\| = \|B\|) \to A F (A - B) = 1 F (1 - (\frac{B}{A}))$
53	2 15	mulneg2d	$⊢ ((A \in ℂ \land B \in ℂ) \land (A \neq 0 \land B \neq 0 \land A \neq B) \land \|A\| = \|B\|) \to A (- \frac{B}{A}) = - A (\frac{B}{A})$
54	46	negeqd	$⊢ ((A \in ℂ \land B \in ℂ) \land (A \neq 0 \land B \neq 0 \land A \neq B) \land \|A\| = \|B\|) \to - A (\frac{B}{A}) = - B$
55	53 54	eqtrd	$⊢ ((A \in ℂ \land B \in ℂ) \land (A \neq 0 \land B \neq 0 \land A \neq B) \land \|A\| = \|B\|) \to A (- \frac{B}{A}) = - B$
56	48 55	oveq12d	$⊢ ((A \in ℂ \land B \in ℂ) \land (A \neq 0 \land B \neq 0 \land A \neq B) \land \|A\| = \|B\|) \to A (1 - (\frac{B}{A})) F A (- \frac{B}{A}) = (A - B) F (- B)$
57	1	angcan	$⊢ ((1 - (\frac{B}{A}) \in ℂ \land 1 - (\frac{B}{A}) \neq 0) \land (- \frac{B}{A} \in ℂ \land - \frac{B}{A} \neq 0) \land (A \in ℂ \land A \neq 0)) \to A (1 - (\frac{B}{A})) F A (- \frac{B}{A}) = (1 - (\frac{B}{A})) F (- \frac{B}{A})$
58	16 20 37 40 2 3 57	syl222anc	$⊢ ((A \in ℂ \land B \in ℂ) \land (A \neq 0 \land B \neq 0 \land A \neq B) \land \|A\| = \|B\|) \to A (1 - (\frac{B}{A})) F A (- \frac{B}{A}) = (1 - (\frac{B}{A})) F (- \frac{B}{A})$
59	56 58	eqtr3d	$⊢ ((A \in ℂ \land B \in ℂ) \land (A \neq 0 \land B \neq 0 \land A \neq B) \land \|A\| = \|B\|) \to (A - B) F (- B) = (1 - (\frac{B}{A})) F (- \frac{B}{A})$
60	43 52 59	3eqtr4d	$⊢ ((A \in ℂ \land B \in ℂ) \land (A \neq 0 \land B \neq 0 \land A \neq B) \land \|A\| = \|B\|) \to A F (A - B) = (A - B) F (- B)$
61	9 11 60	3eqtr3d	$⊢ ((A \in ℂ \land B \in ℂ) \land (A \neq 0 \land B \neq 0 \land A \neq B) \land \|A\| = \|B\|) \to (- A) F (B - A) = (A - B) F (- B)$

Metamath Proof Explorer

Theorem isosctrlem3

Proof