isosctrlem2

Description: Lemma for isosctr . Corresponds to the case where one vertex is at 0, another at 1 and the third lies on the unit circle. (Contributed by Saveliy Skresanov, 31-Dec-2016)

		Ref	Expression
	Assertion	isosctrlem2	$⊢ (A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \to ℑ (\log (1 - A)) = ℑ (\log (\frac{- A}{1 - A}))$

Proof

Step	Hyp	Ref	Expression
1		1cnd	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) = 0) \to 1 \in ℂ$
2		simpl1	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) = 0) \to A \in ℂ$
3	1 2	negsubd	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) = 0) \to 1 + (- A) = 1 - A$
4		1rp	$⊢ 1 \in ℝ^{+}$
5	4	a1i	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) = 0) \to 1 \in ℝ^{+}$
6		simpl3	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) = 0) \to \neg 1 = A$
7		simpl2	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) = 0) \to \|A\| = 1$
8	1 2 1	sub32d	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) = 0) \to 1 - A - 1 = 1 - 1 - A$
9		1m1e0	$⊢ 1 - 1 = 0$
10	9	oveq1i	$⊢ 1 - 1 - A = 0 - A$
11		df-neg	$⊢ - A = 0 - A$
12	10 11	eqtr4i	$⊢ 1 - 1 - A = - A$
13	8 12	eqtrdi	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) = 0) \to 1 - A - 1 = - A$
14		1cnd	$⊢ (A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \to 1 \in ℂ$
15		simp1	$⊢ (A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \to A \in ℂ$
16	14 15	subcld	$⊢ (A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \to 1 - A \in ℂ$
17	16	adantr	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) = 0) \to 1 - A \in ℂ$
18		ax-1cn	$⊢ 1 \in ℂ$
19		subeq0	$⊢ (1 \in ℂ \land A \in ℂ) \to (1 - A = 0 \leftrightarrow 1 = A)$
20	18 19	mpan	$⊢ A \in ℂ \to (1 - A = 0 \leftrightarrow 1 = A)$
21	20	biimpd	$⊢ A \in ℂ \to (1 - A = 0 \to 1 = A)$
22	21	con3dimp	$⊢ (A \in ℂ \land \neg 1 = A) \to \neg 1 - A = 0$
23	22	neqned	$⊢ (A \in ℂ \land \neg 1 = A) \to 1 - A \neq 0$
24	23	3adant2	$⊢ (A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \to 1 - A \neq 0$
25	24	adantr	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) = 0) \to 1 - A \neq 0$
26	17 25	recrecd	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) = 0) \to \frac{1}{\frac{1}{1 - A}} = 1 - A$
27	14 16 24	div2negd	$⊢ (A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \to \frac{- 1}{- (1 - A)} = \frac{1}{1 - A}$
28	27	adantr	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) = 0) \to \frac{- 1}{- (1 - A)} = \frac{1}{1 - A}$
29	15	negcld	$⊢ (A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \to - A \in ℂ$
30	29 16 24	cjdivd	$⊢ (A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \to \overline{\frac{- A}{1 - A}} = \frac{\overline{- A}}{\overline{1 - A}}$
31	15	cjnegd	$⊢ (A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \to \overline{- A} = - \overline{A}$
32		fveq2	$⊢ A = 0 \to \|A\| = \|0\|$
33		abs0	$⊢ \|0\| = 0$
34	32 33	eqtrdi	$⊢ A = 0 \to \|A\| = 0$
35		eqtr2	$⊢ (\|A\| = 1 \land \|A\| = 0) \to 1 = 0$
36	34 35	sylan2	$⊢ (\|A\| = 1 \land A = 0) \to 1 = 0$
37		ax-1ne0	$⊢ 1 \neq 0$
38		neneq	$⊢ 1 \neq 0 \to \neg 1 = 0$
39	37 38	mp1i	$⊢ (\|A\| = 1 \land A = 0) \to \neg 1 = 0$
40	36 39	pm2.65da	$⊢ \|A\| = 1 \to \neg A = 0$
41	40	adantl	$⊢ (A \in ℂ \land \|A\| = 1) \to \neg A = 0$
42		df-ne	$⊢ A \neq 0 \leftrightarrow \neg A = 0$
43		oveq1	$⊢ \|A\| = 1 \to {\|A\|}^{2} = 1^{2}$
44		sq1	$⊢ 1^{2} = 1$
45	43 44	eqtrdi	$⊢ \|A\| = 1 \to {\|A\|}^{2} = 1$
46	45	adantl	$⊢ (A \in ℂ \land \|A\| = 1) \to {\|A\|}^{2} = 1$
47		absvalsq	$⊢ A \in ℂ \to {\|A\|}^{2} = A \overline{A}$
48	47	adantr	$⊢ (A \in ℂ \land \|A\| = 1) \to {\|A\|}^{2} = A \overline{A}$
49	46 48	eqtr3d	$⊢ (A \in ℂ \land \|A\| = 1) \to 1 = A \overline{A}$
50	49	3adant3	$⊢ (A \in ℂ \land \|A\| = 1 \land A \neq 0) \to 1 = A \overline{A}$
51	50	oveq1d	$⊢ (A \in ℂ \land \|A\| = 1 \land A \neq 0) \to \frac{1}{A} = \frac{A \overline{A}}{A}$
52		simp1	$⊢ (A \in ℂ \land \|A\| = 1 \land A \neq 0) \to A \in ℂ$
53	52	cjcld	$⊢ (A \in ℂ \land \|A\| = 1 \land A \neq 0) \to \overline{A} \in ℂ$
54		simp3	$⊢ (A \in ℂ \land \|A\| = 1 \land A \neq 0) \to A \neq 0$
55	53 52 54	divcan3d	$⊢ (A \in ℂ \land \|A\| = 1 \land A \neq 0) \to \frac{A \overline{A}}{A} = \overline{A}$
56	51 55	eqtrd	$⊢ (A \in ℂ \land \|A\| = 1 \land A \neq 0) \to \frac{1}{A} = \overline{A}$
57	42 56	syl3an3br	$⊢ (A \in ℂ \land \|A\| = 1 \land \neg A = 0) \to \frac{1}{A} = \overline{A}$
58	41 57	mpd3an3	$⊢ (A \in ℂ \land \|A\| = 1) \to \frac{1}{A} = \overline{A}$
59	58	eqcomd	$⊢ (A \in ℂ \land \|A\| = 1) \to \overline{A} = \frac{1}{A}$
60	59	3adant3	$⊢ (A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \to \overline{A} = \frac{1}{A}$
61	60	negeqd	$⊢ (A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \to - \overline{A} = - \frac{1}{A}$
62	31 61	eqtrd	$⊢ (A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \to \overline{- A} = - \frac{1}{A}$
63	62	oveq1d	$⊢ (A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \to \frac{\overline{- A}}{\overline{1 - A}} = \frac{- \frac{1}{A}}{\overline{1 - A}}$
64		cjsub	$⊢ (1 \in ℂ \land A \in ℂ) \to \overline{1 - A} = \overline{1} - \overline{A}$
65	18 64	mpan	$⊢ A \in ℂ \to \overline{1 - A} = \overline{1} - \overline{A}$
66		1red	$⊢ A \in ℂ \to 1 \in ℝ$
67	66	cjred	$⊢ A \in ℂ \to \overline{1} = 1$
68	67	oveq1d	$⊢ A \in ℂ \to \overline{1} - \overline{A} = 1 - \overline{A}$
69	65 68	eqtrd	$⊢ A \in ℂ \to \overline{1 - A} = 1 - \overline{A}$
70	69	adantr	$⊢ (A \in ℂ \land \|A\| = 1) \to \overline{1 - A} = 1 - \overline{A}$
71	59	oveq2d	$⊢ (A \in ℂ \land \|A\| = 1) \to 1 - \overline{A} = 1 - (\frac{1}{A})$
72	70 71	eqtrd	$⊢ (A \in ℂ \land \|A\| = 1) \to \overline{1 - A} = 1 - (\frac{1}{A})$
73	72	3adant3	$⊢ (A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \to \overline{1 - A} = 1 - (\frac{1}{A})$
74	73	oveq2d	$⊢ (A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \to \frac{- \frac{1}{A}}{\overline{1 - A}} = \frac{- \frac{1}{A}}{1 - (\frac{1}{A})}$
75	30 63 74	3eqtrd	$⊢ (A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \to \overline{\frac{- A}{1 - A}} = \frac{- \frac{1}{A}}{1 - (\frac{1}{A})}$
76	40	3ad2ant2	$⊢ (A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \to \neg A = 0$
77	76	neqned	$⊢ (A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \to A \neq 0$
78		1cnd	$⊢ (A \in ℂ \land A \neq 0) \to 1 \in ℂ$
79		simpl	$⊢ (A \in ℂ \land A \neq 0) \to A \in ℂ$
80		simpr	$⊢ (A \in ℂ \land A \neq 0) \to A \neq 0$
81	78 79 80	divnegd	$⊢ (A \in ℂ \land A \neq 0) \to - \frac{1}{A} = \frac{- 1}{A}$
82	81	oveq1d	$⊢ (A \in ℂ \land A \neq 0) \to \frac{- \frac{1}{A}}{1 - (\frac{1}{A})} = \frac{\frac{- 1}{A}}{1 - (\frac{1}{A})}$
83	15 77 82	syl2anc	$⊢ (A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \to \frac{- \frac{1}{A}}{1 - (\frac{1}{A})} = \frac{\frac{- 1}{A}}{1 - (\frac{1}{A})}$
84	14	negcld	$⊢ (A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \to - 1 \in ℂ$
85	84 15 77	divcld	$⊢ (A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \to \frac{- 1}{A} \in ℂ$
86	15 77	reccld	$⊢ (A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \to \frac{1}{A} \in ℂ$
87	14 86	subcld	$⊢ (A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \to 1 - (\frac{1}{A}) \in ℂ$
88	16 24	cjne0d	$⊢ (A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \to \overline{1 - A} \neq 0$
89	73 88	eqnetrrd	$⊢ (A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \to 1 - (\frac{1}{A}) \neq 0$
90	85 87 15 89 77	divcan5d	$⊢ (A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \to \frac{A (\frac{- 1}{A})}{A (1 - (\frac{1}{A}))} = \frac{\frac{- 1}{A}}{1 - (\frac{1}{A})}$
91	84 15 77	divcan2d	$⊢ (A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \to A (\frac{- 1}{A}) = - 1$
92	15 14 86	subdid	$⊢ (A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \to A (1 - (\frac{1}{A})) = A \cdot 1 - A (\frac{1}{A})$
93	15	mulid1d	$⊢ (A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \to A \cdot 1 = A$
94	15 77	recidd	$⊢ (A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \to A (\frac{1}{A}) = 1$
95	93 94	oveq12d	$⊢ (A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \to A \cdot 1 - A (\frac{1}{A}) = A - 1$
96	92 95	eqtrd	$⊢ (A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \to A (1 - (\frac{1}{A})) = A - 1$
97	91 96	oveq12d	$⊢ (A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \to \frac{A (\frac{- 1}{A})}{A (1 - (\frac{1}{A}))} = \frac{- 1}{A - 1}$
98	83 90 97	3eqtr2d	$⊢ (A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \to \frac{- \frac{1}{A}}{1 - (\frac{1}{A})} = \frac{- 1}{A - 1}$
99		subcl	$⊢ (A \in ℂ \land 1 \in ℂ) \to A - 1 \in ℂ$
100	99	negnegd	$⊢ (A \in ℂ \land 1 \in ℂ) \to - (- (A - 1)) = A - 1$
101		negsubdi2	$⊢ (A \in ℂ \land 1 \in ℂ) \to - (A - 1) = 1 - A$
102	101	negeqd	$⊢ (A \in ℂ \land 1 \in ℂ) \to - (- (A - 1)) = - (1 - A)$
103	100 102	eqtr3d	$⊢ (A \in ℂ \land 1 \in ℂ) \to A - 1 = - (1 - A)$
104	15 14 103	syl2anc	$⊢ (A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \to A - 1 = - (1 - A)$
105	104	oveq2d	$⊢ (A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \to \frac{- 1}{A - 1} = \frac{- 1}{- (1 - A)}$
106	75 98 105	3eqtrd	$⊢ (A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \to \overline{\frac{- A}{1 - A}} = \frac{- 1}{- (1 - A)}$
107	106	adantr	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) = 0) \to \overline{\frac{- A}{1 - A}} = \frac{- 1}{- (1 - A)}$
108	29 16 24	divcld	$⊢ (A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \to \frac{- A}{1 - A} \in ℂ$
109	108	adantr	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) = 0) \to \frac{- A}{1 - A} \in ℂ$
110		simpr	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) = 0) \to ℑ (\frac{- A}{1 - A}) = 0$
111	109 110	reim0bd	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) = 0) \to \frac{- A}{1 - A} \in ℝ$
112	111	cjred	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) = 0) \to \overline{\frac{- A}{1 - A}} = \frac{- A}{1 - A}$
113	112 111	eqeltrd	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) = 0) \to \overline{\frac{- A}{1 - A}} \in ℝ$
114	107 113	eqeltrrd	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) = 0) \to \frac{- 1}{- (1 - A)} \in ℝ$
115	28 114	eqeltrrd	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) = 0) \to \frac{1}{1 - A} \in ℝ$
116	16 24	recne0d	$⊢ (A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \to \frac{1}{1 - A} \neq 0$
117	116	adantr	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) = 0) \to \frac{1}{1 - A} \neq 0$
118	115 117	rereccld	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) = 0) \to \frac{1}{\frac{1}{1 - A}} \in ℝ$
119	26 118	eqeltrrd	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) = 0) \to 1 - A \in ℝ$
120		1red	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) = 0) \to 1 \in ℝ$
121	119 120	resubcld	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) = 0) \to 1 - A - 1 \in ℝ$
122	13 121	eqeltrrd	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) = 0) \to - A \in ℝ$
123	2 122	negrebd	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) = 0) \to A \in ℝ$
124	123	absord	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) = 0) \to (\|A\| = A \lor \|A\| = - A)$
125		eqeq1	$⊢ \|A\| = 1 \to (\|A\| = A \leftrightarrow 1 = A)$
126	125	biimpd	$⊢ \|A\| = 1 \to (\|A\| = A \to 1 = A)$
127		eqeq1	$⊢ \|A\| = 1 \to (\|A\| = - A \leftrightarrow 1 = - A)$
128	127	biimpd	$⊢ \|A\| = 1 \to (\|A\| = - A \to 1 = - A)$
129	126 128	orim12d	$⊢ \|A\| = 1 \to ((\|A\| = A \lor \|A\| = - A) \to (1 = A \lor 1 = - A))$
130	7 124 129	sylc	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) = 0) \to (1 = A \lor 1 = - A)$
131	130	ord	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) = 0) \to (\neg 1 = A \to 1 = - A)$
132	6 131	mpd	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) = 0) \to 1 = - A$
133	132 5	eqeltrrd	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) = 0) \to - A \in ℝ^{+}$
134	5 133	rpaddcld	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) = 0) \to 1 + (- A) \in ℝ^{+}$
135	3 134	eqeltrrd	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) = 0) \to 1 - A \in ℝ^{+}$
136	135	relogcld	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) = 0) \to \log (1 - A) \in ℝ$
137	136	reim0d	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) = 0) \to ℑ (\log (1 - A)) = 0$
138	133 135	rpdivcld	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) = 0) \to \frac{- A}{1 - A} \in ℝ^{+}$
139	138	relogcld	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) = 0) \to \log (\frac{- A}{1 - A}) \in ℝ$
140	139	reim0d	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) = 0) \to ℑ (\log (\frac{- A}{1 - A})) = 0$
141	137 140	eqtr4d	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) = 0) \to ℑ (\log (1 - A)) = ℑ (\log (\frac{- A}{1 - A}))$
142	16 24	logcld	$⊢ (A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \to \log (1 - A) \in ℂ$
143	142	adantr	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) \neq 0) \to \log (1 - A) \in ℂ$
144	143	imcld	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) \neq 0) \to ℑ (\log (1 - A)) \in ℝ$
145	144	recnd	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) \neq 0) \to ℑ (\log (1 - A)) \in ℂ$
146	108	adantr	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) \neq 0) \to \frac{- A}{1 - A} \in ℂ$
147	15 77	negne0d	$⊢ (A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \to - A \neq 0$
148	29 16 147 24	divne0d	$⊢ (A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \to \frac{- A}{1 - A} \neq 0$
149	148	adantr	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) \neq 0) \to \frac{- A}{1 - A} \neq 0$
150	146 149	logcld	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) \neq 0) \to \log (\frac{- A}{1 - A}) \in ℂ$
151	150	imcld	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) \neq 0) \to ℑ (\log (\frac{- A}{1 - A})) \in ℝ$
152	151	recnd	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) \neq 0) \to ℑ (\log (\frac{- A}{1 - A})) \in ℂ$
153	106	fveq2d	$⊢ (A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \to \log \overline{\frac{- A}{1 - A}} = \log (\frac{- 1}{- (1 - A)})$
154	153	adantr	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) \neq 0) \to \log \overline{\frac{- A}{1 - A}} = \log (\frac{- 1}{- (1 - A)})$
155		logcj	$⊢ (\frac{- A}{1 - A} \in ℂ \land ℑ (\frac{- A}{1 - A}) \neq 0) \to \log \overline{\frac{- A}{1 - A}} = \overline{\log (\frac{- A}{1 - A})}$
156	108 155	sylan	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) \neq 0) \to \log \overline{\frac{- A}{1 - A}} = \overline{\log (\frac{- A}{1 - A})}$
157	16 24	reccld	$⊢ (A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \to \frac{1}{1 - A} \in ℂ$
158	157 116	logcld	$⊢ (A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \to \log (\frac{1}{1 - A}) \in ℂ$
159	158	negnegd	$⊢ (A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \to - (- \log (\frac{1}{1 - A})) = \log (\frac{1}{1 - A})$
160		isosctrlem1	$⊢ (A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \to ℑ (\log (1 - A)) \neq π$
161		logrec	$⊢ (1 - A \in ℂ \land 1 - A \neq 0 \land ℑ (\log (1 - A)) \neq π) \to \log (1 - A) = - \log (\frac{1}{1 - A})$
162	16 24 160 161	syl3anc	$⊢ (A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \to \log (1 - A) = - \log (\frac{1}{1 - A})$
163	162	negeqd	$⊢ (A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \to - \log (1 - A) = - (- \log (\frac{1}{1 - A}))$
164	27	fveq2d	$⊢ (A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \to \log (\frac{- 1}{- (1 - A)}) = \log (\frac{1}{1 - A})$
165	159 163 164	3eqtr4rd	$⊢ (A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \to \log (\frac{- 1}{- (1 - A)}) = - \log (1 - A)$
166	165	adantr	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) \neq 0) \to \log (\frac{- 1}{- (1 - A)}) = - \log (1 - A)$
167	154 156 166	3eqtr3rd	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) \neq 0) \to - \log (1 - A) = \overline{\log (\frac{- A}{1 - A})}$
168	167	fveq2d	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) \neq 0) \to ℑ (- \log (1 - A)) = ℑ (\overline{\log (\frac{- A}{1 - A})})$
169	143	imnegd	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) \neq 0) \to ℑ (- \log (1 - A)) = - ℑ (\log (1 - A))$
170	150	imcjd	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) \neq 0) \to ℑ (\overline{\log (\frac{- A}{1 - A})}) = - ℑ (\log (\frac{- A}{1 - A}))$
171	168 169 170	3eqtr3d	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) \neq 0) \to - ℑ (\log (1 - A)) = - ℑ (\log (\frac{- A}{1 - A}))$
172	145 152 171	neg11d	$⊢ ((A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \land ℑ (\frac{- A}{1 - A}) \neq 0) \to ℑ (\log (1 - A)) = ℑ (\log (\frac{- A}{1 - A}))$
173	141 172	pm2.61dane	$⊢ (A \in ℂ \land \|A\| = 1 \land \neg 1 = A) \to ℑ (\log (1 - A)) = ℑ (\log (\frac{- A}{1 - A}))$

Metamath Proof Explorer

Theorem isosctrlem2

Proof