ang180lem5

Description: Lemma for ang180 : Reduce the statement to two variables. (Contributed by Mario Carneiro, 23-Sep-2014)

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

Proof

Step	Hyp	Ref	Expression
1		ang.1	$⊢ F = (x \in (ℂ ∖ \{0\}), y \in (ℂ ∖ \{0\}) ⟼ ℑ (\log (\frac{y}{x})))$
2		simp1l	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0) \land A \neq B) \to A \in ℂ$
3		1cnd	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0) \land A \neq B) \to 1 \in ℂ$
4		simp2l	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0) \land A \neq B) \to B \in ℂ$
5		simp1r	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0) \land A \neq B) \to A \neq 0$
6	4 2 5	divcld	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0) \land A \neq B) \to \frac{B}{A} \in ℂ$
7	2 3 6	subdid	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0) \land A \neq B) \to A (1 - (\frac{B}{A})) = A \cdot 1 - A (\frac{B}{A})$
8	2	mulridd	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0) \land A \neq B) \to A \cdot 1 = A$
9	4 2 5	divcan2d	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0) \land A \neq B) \to A (\frac{B}{A}) = B$
10	8 9	oveq12d	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0) \land A \neq B) \to A \cdot 1 - A (\frac{B}{A}) = A - B$
11	7 10	eqtrd	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0) \land A \neq B) \to A (1 - (\frac{B}{A})) = A - B$
12	11 8	oveq12d	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0) \land A \neq B) \to A (1 - (\frac{B}{A})) F A \cdot 1 = (A - B) F A$
13	3 6	subcld	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0) \land A \neq B) \to 1 - (\frac{B}{A}) \in ℂ$
14		simp3	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0) \land A \neq B) \to A \neq B$
15	14	necomd	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0) \land A \neq B) \to B \neq A$
16	4 2 5 15	divne1d	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0) \land A \neq B) \to \frac{B}{A} \neq 1$
17	16	necomd	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0) \land A \neq B) \to 1 \neq \frac{B}{A}$
18	3 6 17	subne0d	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0) \land A \neq B) \to 1 - (\frac{B}{A}) \neq 0$
19		ax-1ne0	$⊢ 1 \neq 0$
20	19	a1i	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0) \land A \neq B) \to 1 \neq 0$
21	1	angcan	$⊢ ((1 - (\frac{B}{A}) \in ℂ \land 1 - (\frac{B}{A}) \neq 0) \land (1 \in ℂ \land 1 \neq 0) \land (A \in ℂ \land A \neq 0)) \to A (1 - (\frac{B}{A})) F A \cdot 1 = (1 - (\frac{B}{A})) F 1$
22	13 18 3 20 2 5 21	syl222anc	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0) \land A \neq B) \to A (1 - (\frac{B}{A})) F A \cdot 1 = (1 - (\frac{B}{A})) F 1$
23	12 22	eqtr3d	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0) \land A \neq B) \to (A - B) F A = (1 - (\frac{B}{A})) F 1$
24	2 6 3	subdid	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0) \land A \neq B) \to A ((\frac{B}{A}) - 1) = A (\frac{B}{A}) - A \cdot 1$
25	9 8	oveq12d	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0) \land A \neq B) \to A (\frac{B}{A}) - A \cdot 1 = B - A$
26	24 25	eqtrd	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0) \land A \neq B) \to A ((\frac{B}{A}) - 1) = B - A$
27	9 26	oveq12d	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0) \land A \neq B) \to A (\frac{B}{A}) F A ((\frac{B}{A}) - 1) = B F (B - A)$
28		simp2r	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0) \land A \neq B) \to B \neq 0$
29	4 2 28 5	divne0d	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0) \land A \neq B) \to \frac{B}{A} \neq 0$
30	6 3	subcld	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0) \land A \neq B) \to (\frac{B}{A}) - 1 \in ℂ$
31	6 3 16	subne0d	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0) \land A \neq B) \to (\frac{B}{A}) - 1 \neq 0$
32	1	angcan	$⊢ ((\frac{B}{A} \in ℂ \land \frac{B}{A} \neq 0) \land ((\frac{B}{A}) - 1 \in ℂ \land (\frac{B}{A}) - 1 \neq 0) \land (A \in ℂ \land A \neq 0)) \to A (\frac{B}{A}) F A ((\frac{B}{A}) - 1) = (\frac{B}{A}) F ((\frac{B}{A}) - 1)$
33	6 29 30 31 2 5 32	syl222anc	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0) \land A \neq B) \to A (\frac{B}{A}) F A ((\frac{B}{A}) - 1) = (\frac{B}{A}) F ((\frac{B}{A}) - 1)$
34	27 33	eqtr3d	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0) \land A \neq B) \to B F (B - A) = (\frac{B}{A}) F ((\frac{B}{A}) - 1)$
35	23 34	oveq12d	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0) \land A \neq B) \to ((A - B) F A) + (B F (B - A)) = ((1 - (\frac{B}{A})) F 1) + ((\frac{B}{A}) F ((\frac{B}{A}) - 1))$
36	8 9	oveq12d	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0) \land A \neq B) \to A \cdot 1 F A (\frac{B}{A}) = A F B$
37	1	angcan	$⊢ ((1 \in ℂ \land 1 \neq 0) \land (\frac{B}{A} \in ℂ \land \frac{B}{A} \neq 0) \land (A \in ℂ \land A \neq 0)) \to A \cdot 1 F A (\frac{B}{A}) = 1 F (\frac{B}{A})$
38	3 20 6 29 2 5 37	syl222anc	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0) \land A \neq B) \to A \cdot 1 F A (\frac{B}{A}) = 1 F (\frac{B}{A})$
39	36 38	eqtr3d	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0) \land A \neq B) \to A F B = 1 F (\frac{B}{A})$
40	35 39	oveq12d	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0) \land A \neq B) \to ((A - B) F A) + (B F (B - A)) + (A F B) = ((1 - (\frac{B}{A})) F 1) + ((\frac{B}{A}) F ((\frac{B}{A}) - 1)) + (1 F (\frac{B}{A}))$
41	1	ang180lem4	$⊢ (\frac{B}{A} \in ℂ \land \frac{B}{A} \neq 0 \land \frac{B}{A} \neq 1) \to ((1 - (\frac{B}{A})) F 1) + ((\frac{B}{A}) F ((\frac{B}{A}) - 1)) + (1 F (\frac{B}{A})) \in \{- π, π\}$
42	6 29 16 41	syl3anc	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0) \land A \neq B) \to ((1 - (\frac{B}{A})) F 1) + ((\frac{B}{A}) F ((\frac{B}{A}) - 1)) + (1 F (\frac{B}{A})) \in \{- π, π\}$
43	40 42	eqeltrd	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0) \land A \neq B) \to ((A - B) F A) + (B F (B - A)) + (A F B) \in \{- π, π\}$

Metamath Proof Explorer

Theorem ang180lem5

Proof