Theorem isosctrlem1ALT

Description: Lemma for isosctr . This proof was automatically derived by completeusersproof from its Virtual Deduction proof counterpart https://us.metamath.org/other/completeusersproof/isosctrlem1altvd.html . As it is verified by the Metamath program, isosctrlem1ALT verifies https://us.metamath.org/other/completeusersproof/isosctrlem1altvd.html . (Contributed by Alan Sare, 22-Apr-2018) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	isosctrlem1ALT	$$⊢\left(A\in ℂ\wedge \left|A\right|=1\wedge \neg 1=A\right)\to \Im \left(\log \left(1-A\right)\right)\ne \mathrm{\pi }$$

Proof

Step	Hyp	Ref	Expression
1		ax-1cn	$$⊢1\in ℂ$$
2	1	a1i	$$⊢A\in ℂ\to 1\in ℂ$$
3		id	$$⊢A\in ℂ\to A\in ℂ$$
4	2 3	subcld	$$⊢A\in ℂ\to 1-A\in ℂ$$
5	4	adantr	$$⊢\left(A\in ℂ\wedge \neg 1=A\right)\to 1-A\in ℂ$$
6		subeq0	$$⊢\left(1\in ℂ\wedge A\in ℂ\right)\to \left(1-A=0\leftrightarrow 1=A\right)$$
7	6	biimpd	$$⊢\left(1\in ℂ\wedge A\in ℂ\right)\to \left(1-A=0\to 1=A\right)$$
8	7	idiALT	$$⊢\left(1\in ℂ\wedge A\in ℂ\right)\to \left(1-A=0\to 1=A\right)$$
9	1 3 8	sylancr	$$⊢A\in ℂ\to \left(1-A=0\to 1=A\right)$$
10	9	con3d	$$⊢A\in ℂ\to \left(\neg 1=A\to \neg 1-A=0\right)$$
11		df-ne	$$⊢1-A\ne 0\leftrightarrow \neg 1-A=0$$
12	11	biimpri	$$⊢\neg 1-A=0\to 1-A\ne 0$$
13	10 12	syl6	$$⊢A\in ℂ\to \left(\neg 1=A\to 1-A\ne 0\right)$$
14	13	imp	$$⊢\left(A\in ℂ\wedge \neg 1=A\right)\to 1-A\ne 0$$
15	5 14	logcld	$$⊢\left(A\in ℂ\wedge \neg 1=A\right)\to \log \left(1-A\right)\in ℂ$$
16	15	imcld	$$⊢\left(A\in ℂ\wedge \neg 1=A\right)\to \Im \left(\log \left(1-A\right)\right)\in ℝ$$
17	16	3adant2	$$⊢\left(A\in ℂ\wedge \left|A\right|=1\wedge \neg 1=A\right)\to \Im \left(\log \left(1-A\right)\right)\in ℝ$$
18		pire	$$⊢\mathrm{\pi }\in ℝ$$
19		2re	$$⊢2\in ℝ$$
20		2ne0	$$⊢2\ne 0$$
21	18 19 20	redivcli	$$⊢\frac{\mathrm{\pi }}{2}\in ℝ$$
22	21	a1i	$$⊢\left(A\in ℂ\wedge \left|A\right|=1\wedge \neg 1=A\right)\to \frac{\mathrm{\pi }}{2}\in ℝ$$
23	18	a1i	$$⊢\left(A\in ℂ\wedge \left|A\right|=1\wedge \neg 1=A\right)\to \mathrm{\pi }\in ℝ$$
24		neghalfpirx	$$⊢-\frac{\mathrm{\pi }}{2}\in {ℝ}^{*}$$
25	21	rexri	$$⊢\frac{\mathrm{\pi }}{2}\in {ℝ}^{*}$$
26	3	recld	$$⊢A\in ℂ\to \Re \left(A\right)\in ℝ$$
27	26	recnd	$$⊢A\in ℂ\to \Re \left(A\right)\in ℂ$$
28	27	subidd	$$⊢A\in ℂ\to \Re \left(A\right)-\Re \left(A\right)=0$$
29	28	adantr	$$⊢\left(A\in ℂ\wedge \left|A\right|=1\right)\to \Re \left(A\right)-\Re \left(A\right)=0$$
30		1re	$$⊢1\in ℝ$$
31	30	a1i	$$⊢1\in ℂ\to 1\in ℝ$$
32	1 31	ax-mp	$$⊢1\in ℝ$$
33	3	releabsd	$$⊢A\in ℂ\to \Re \left(A\right)\le \left|A\right|$$
34	33	adantr	$$⊢\left(A\in ℂ\wedge \left|A\right|=1\right)\to \Re \left(A\right)\le \left|A\right|$$
35		id	$$⊢\left|A\right|=1\to \left|A\right|=1$$
36	35	adantl	$$⊢\left(A\in ℂ\wedge \left|A\right|=1\right)\to \left|A\right|=1$$
37	34 36	breqtrd	$$⊢\left(A\in ℂ\wedge \left|A\right|=1\right)\to \Re \left(A\right)\le 1$$
38		lesub1	$$⊢\left(\Re \left(A\right)\in ℝ\wedge 1\in ℝ\wedge \Re \left(A\right)\in ℝ\right)\to \left(\Re \left(A\right)\le 1\leftrightarrow \Re \left(A\right)-\Re \left(A\right)\le 1-\Re \left(A\right)\right)$$
39	38	3impcombi	$$⊢\left(1\in ℝ\wedge \Re \left(A\right)\in ℝ\wedge \Re \left(A\right)\le 1\right)\to \Re \left(A\right)-\Re \left(A\right)\le 1-\Re \left(A\right)$$
40	39	idiALT	$$⊢\left(1\in ℝ\wedge \Re \left(A\right)\in ℝ\wedge \Re \left(A\right)\le 1\right)\to \Re \left(A\right)-\Re \left(A\right)\le 1-\Re \left(A\right)$$
41	32 26 37 40	mp3an2ani	$$⊢\left(A\in ℂ\wedge \left|A\right|=1\right)\to \Re \left(A\right)-\Re \left(A\right)\le 1-\Re \left(A\right)$$
42	29 41	eqbrtrrd	$$⊢\left(A\in ℂ\wedge \left|A\right|=1\right)\to 0\le 1-\Re \left(A\right)$$
43	32	a1i	$$⊢\top \to 1\in ℝ$$
44	43	rered	$$⊢\top \to \Re \left(1\right)=1$$
45	44	mptru	$$⊢\Re \left(1\right)=1$$
46		oveq1	$$⊢\Re \left(1\right)=1\to \Re \left(1\right)-\Re \left(A\right)=1-\Re \left(A\right)$$
47	46	eqcomd	$$⊢\Re \left(1\right)=1\to 1-\Re \left(A\right)=\Re \left(1\right)-\Re \left(A\right)$$
48	45 47	ax-mp	$$⊢1-\Re \left(A\right)=\Re \left(1\right)-\Re \left(A\right)$$
49		resub	$$⊢\left(1\in ℂ\wedge A\in ℂ\right)\to \Re \left(1-A\right)=\Re \left(1\right)-\Re \left(A\right)$$
50	49	eqcomd	$$⊢\left(1\in ℂ\wedge A\in ℂ\right)\to \Re \left(1\right)-\Re \left(A\right)=\Re \left(1-A\right)$$
51	50	idiALT	$$⊢\left(1\in ℂ\wedge A\in ℂ\right)\to \Re \left(1\right)-\Re \left(A\right)=\Re \left(1-A\right)$$
52	1 3 51	sylancr	$$⊢A\in ℂ\to \Re \left(1\right)-\Re \left(A\right)=\Re \left(1-A\right)$$
53	48 52	syl5eq	$$⊢A\in ℂ\to 1-\Re \left(A\right)=\Re \left(1-A\right)$$
54	53	adantr	$$⊢\left(A\in ℂ\wedge \left|A\right|=1\right)\to 1-\Re \left(A\right)=\Re \left(1-A\right)$$
55	42 54	breqtrd	$$⊢\left(A\in ℂ\wedge \left|A\right|=1\right)\to 0\le \Re \left(1-A\right)$$
56		argrege0	$$⊢\left(1-A\in ℂ\wedge 1-A\ne 0\wedge 0\le \Re \left(1-A\right)\right)\to \Im \left(\log \left(1-A\right)\right)\in \left[-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right]$$
57	56	3coml	$$⊢\left(1-A\ne 0\wedge 0\le \Re \left(1-A\right)\wedge 1-A\in ℂ\right)\to \Im \left(\log \left(1-A\right)\right)\in \left[-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right]$$
58	57	3com13	$$⊢\left(1-A\in ℂ\wedge 0\le \Re \left(1-A\right)\wedge 1-A\ne 0\right)\to \Im \left(\log \left(1-A\right)\right)\in \left[-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right]$$
59	4 55 14 58	eel12131	$$⊢\left(A\in ℂ\wedge \left|A\right|=1\wedge \neg 1=A\right)\to \Im \left(\log \left(1-A\right)\right)\in \left[-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right]$$
60		iccleub	$$⊢\left(-\frac{\mathrm{\pi }}{2}\in {ℝ}^{*}\wedge \frac{\mathrm{\pi }}{2}\in {ℝ}^{*}\wedge \Im \left(\log \left(1-A\right)\right)\in \left[-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right]\right)\to \Im \left(\log \left(1-A\right)\right)\le \frac{\mathrm{\pi }}{2}$$
61	24 25 59 60	mp3an12i	$$⊢\left(A\in ℂ\wedge \left|A\right|=1\wedge \neg 1=A\right)\to \Im \left(\log \left(1-A\right)\right)\le \frac{\mathrm{\pi }}{2}$$
62		pipos	$$⊢0<\mathrm{\pi }$$
63	18 62	elrpii	$$⊢\mathrm{\pi }\in {ℝ}^{+}$$
64		rphalflt	$$⊢\mathrm{\pi }\in {ℝ}^{+}\to \frac{\mathrm{\pi }}{2}<\mathrm{\pi }$$
65	63 64	ax-mp	$$⊢\frac{\mathrm{\pi }}{2}<\mathrm{\pi }$$
66	65	a1i	$$⊢\left(A\in ℂ\wedge \left|A\right|=1\wedge \neg 1=A\right)\to \frac{\mathrm{\pi }}{2}<\mathrm{\pi }$$
67	17 22 23 61 66	lelttrd	$$⊢\left(A\in ℂ\wedge \left|A\right|=1\wedge \neg 1=A\right)\to \Im \left(\log \left(1-A\right)\right)<\mathrm{\pi }$$
68	17 67	ltned	$$⊢\left(A\in ℂ\wedge \left|A\right|=1\wedge \neg 1=A\right)\to \Im \left(\log \left(1-A\right)\right)\ne \mathrm{\pi }$$