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	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → ( ℑ ‘ ( log ‘ ( 1 − 𝐴 ) ) ) ≠ π )

Proof

Step	Hyp	Ref	Expression
1		ax-1cn	⊢ 1 ∈ ℂ
2	1	a1i	⊢ ( 𝐴 ∈ ℂ → 1 ∈ ℂ )
3		id	⊢ ( 𝐴 ∈ ℂ → 𝐴 ∈ ℂ )
4	2 3	subcld	⊢ ( 𝐴 ∈ ℂ → ( 1 − 𝐴 ) ∈ ℂ )
5	4	adantr	⊢ ( ( 𝐴 ∈ ℂ ∧ ¬ 1 = 𝐴 ) → ( 1 − 𝐴 ) ∈ ℂ )
6		subeq0	⊢ ( ( 1 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( 1 − 𝐴 ) = 0 ↔ 1 = 𝐴 ) )
7	6	biimpd	⊢ ( ( 1 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( 1 − 𝐴 ) = 0 → 1 = 𝐴 ) )
8	7	idiALT	⊢ ( ( 1 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( 1 − 𝐴 ) = 0 → 1 = 𝐴 ) )
9	1 3 8	sylancr	⊢ ( 𝐴 ∈ ℂ → ( ( 1 − 𝐴 ) = 0 → 1 = 𝐴 ) )
10	9	con3d	⊢ ( 𝐴 ∈ ℂ → ( ¬ 1 = 𝐴 → ¬ ( 1 − 𝐴 ) = 0 ) )
11		df-ne	⊢ ( ( 1 − 𝐴 ) ≠ 0 ↔ ¬ ( 1 − 𝐴 ) = 0 )
12	11	biimpri	⊢ ( ¬ ( 1 − 𝐴 ) = 0 → ( 1 − 𝐴 ) ≠ 0 )
13	10 12	syl6	⊢ ( 𝐴 ∈ ℂ → ( ¬ 1 = 𝐴 → ( 1 − 𝐴 ) ≠ 0 ) )
14	13	imp	⊢ ( ( 𝐴 ∈ ℂ ∧ ¬ 1 = 𝐴 ) → ( 1 − 𝐴 ) ≠ 0 )
15	5 14	logcld	⊢ ( ( 𝐴 ∈ ℂ ∧ ¬ 1 = 𝐴 ) → ( log ‘ ( 1 − 𝐴 ) ) ∈ ℂ )
16	15	imcld	⊢ ( ( 𝐴 ∈ ℂ ∧ ¬ 1 = 𝐴 ) → ( ℑ ‘ ( log ‘ ( 1 − 𝐴 ) ) ) ∈ ℝ )
17	16	3adant2	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → ( ℑ ‘ ( log ‘ ( 1 − 𝐴 ) ) ) ∈ ℝ )
18		pire	⊢ π ∈ ℝ
19		2re	⊢ 2 ∈ ℝ
20		2ne0	⊢ 2 ≠ 0
21	18 19 20	redivcli	⊢ ( π / 2 ) ∈ ℝ
22	21	a1i	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → ( π / 2 ) ∈ ℝ )
23	18	a1i	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → π ∈ ℝ )
24		neghalfpirx	⊢ - ( π / 2 ) ∈ ℝ*
25	21	rexri	⊢ ( π / 2 ) ∈ ℝ*
26	3	recld	⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ 𝐴 ) ∈ ℝ )
27	26	recnd	⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ 𝐴 ) ∈ ℂ )
28	27	subidd	⊢ ( 𝐴 ∈ ℂ → ( ( ℜ ‘ 𝐴 ) − ( ℜ ‘ 𝐴 ) ) = 0 )
29	28	adantr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ) → ( ( ℜ ‘ 𝐴 ) − ( ℜ ‘ 𝐴 ) ) = 0 )
30		1re	⊢ 1 ∈ ℝ
31	30	a1i	⊢ ( 1 ∈ ℂ → 1 ∈ ℝ )
32	1 31	ax-mp	⊢ 1 ∈ ℝ
33	3	releabsd	⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ 𝐴 ) ≤ ( abs ‘ 𝐴 ) )
34	33	adantr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ) → ( ℜ ‘ 𝐴 ) ≤ ( abs ‘ 𝐴 ) )
35		id	⊢ ( ( abs ‘ 𝐴 ) = 1 → ( abs ‘ 𝐴 ) = 1 )
36	35	adantl	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ) → ( abs ‘ 𝐴 ) = 1 )
37	34 36	breqtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ) → ( ℜ ‘ 𝐴 ) ≤ 1 )
38		lesub1	⊢ ( ( ( ℜ ‘ 𝐴 ) ∈ ℝ ∧ 1 ∈ ℝ ∧ ( ℜ ‘ 𝐴 ) ∈ ℝ ) → ( ( ℜ ‘ 𝐴 ) ≤ 1 ↔ ( ( ℜ ‘ 𝐴 ) − ( ℜ ‘ 𝐴 ) ) ≤ ( 1 − ( ℜ ‘ 𝐴 ) ) ) )
39	38	3impcombi	⊢ ( ( 1 ∈ ℝ ∧ ( ℜ ‘ 𝐴 ) ∈ ℝ ∧ ( ℜ ‘ 𝐴 ) ≤ 1 ) → ( ( ℜ ‘ 𝐴 ) − ( ℜ ‘ 𝐴 ) ) ≤ ( 1 − ( ℜ ‘ 𝐴 ) ) )
40	39	idiALT	⊢ ( ( 1 ∈ ℝ ∧ ( ℜ ‘ 𝐴 ) ∈ ℝ ∧ ( ℜ ‘ 𝐴 ) ≤ 1 ) → ( ( ℜ ‘ 𝐴 ) − ( ℜ ‘ 𝐴 ) ) ≤ ( 1 − ( ℜ ‘ 𝐴 ) ) )
41	32 26 37 40	mp3an2ani	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ) → ( ( ℜ ‘ 𝐴 ) − ( ℜ ‘ 𝐴 ) ) ≤ ( 1 − ( ℜ ‘ 𝐴 ) ) )
42	29 41	eqbrtrrd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ) → 0 ≤ ( 1 − ( ℜ ‘ 𝐴 ) ) )
43	32	a1i	⊢ ( ⊤ → 1 ∈ ℝ )
44	43	rered	⊢ ( ⊤ → ( ℜ ‘ 1 ) = 1 )
45	44	mptru	⊢ ( ℜ ‘ 1 ) = 1
46		oveq1	⊢ ( ( ℜ ‘ 1 ) = 1 → ( ( ℜ ‘ 1 ) − ( ℜ ‘ 𝐴 ) ) = ( 1 − ( ℜ ‘ 𝐴 ) ) )
47	46	eqcomd	⊢ ( ( ℜ ‘ 1 ) = 1 → ( 1 − ( ℜ ‘ 𝐴 ) ) = ( ( ℜ ‘ 1 ) − ( ℜ ‘ 𝐴 ) ) )
48	45 47	ax-mp	⊢ ( 1 − ( ℜ ‘ 𝐴 ) ) = ( ( ℜ ‘ 1 ) − ( ℜ ‘ 𝐴 ) )
49		resub	⊢ ( ( 1 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ℜ ‘ ( 1 − 𝐴 ) ) = ( ( ℜ ‘ 1 ) − ( ℜ ‘ 𝐴 ) ) )
50	49	eqcomd	⊢ ( ( 1 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( ℜ ‘ 1 ) − ( ℜ ‘ 𝐴 ) ) = ( ℜ ‘ ( 1 − 𝐴 ) ) )
51	50	idiALT	⊢ ( ( 1 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( ℜ ‘ 1 ) − ( ℜ ‘ 𝐴 ) ) = ( ℜ ‘ ( 1 − 𝐴 ) ) )
52	1 3 51	sylancr	⊢ ( 𝐴 ∈ ℂ → ( ( ℜ ‘ 1 ) − ( ℜ ‘ 𝐴 ) ) = ( ℜ ‘ ( 1 − 𝐴 ) ) )
53	48 52	syl5eq	⊢ ( 𝐴 ∈ ℂ → ( 1 − ( ℜ ‘ 𝐴 ) ) = ( ℜ ‘ ( 1 − 𝐴 ) ) )
54	53	adantr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ) → ( 1 − ( ℜ ‘ 𝐴 ) ) = ( ℜ ‘ ( 1 − 𝐴 ) ) )
55	42 54	breqtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ) → 0 ≤ ( ℜ ‘ ( 1 − 𝐴 ) ) )
56		argrege0	⊢ ( ( ( 1 − 𝐴 ) ∈ ℂ ∧ ( 1 − 𝐴 ) ≠ 0 ∧ 0 ≤ ( ℜ ‘ ( 1 − 𝐴 ) ) ) → ( ℑ ‘ ( log ‘ ( 1 − 𝐴 ) ) ) ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) )
57	56	3coml	⊢ ( ( ( 1 − 𝐴 ) ≠ 0 ∧ 0 ≤ ( ℜ ‘ ( 1 − 𝐴 ) ) ∧ ( 1 − 𝐴 ) ∈ ℂ ) → ( ℑ ‘ ( log ‘ ( 1 − 𝐴 ) ) ) ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) )
58	57	3com13	⊢ ( ( ( 1 − 𝐴 ) ∈ ℂ ∧ 0 ≤ ( ℜ ‘ ( 1 − 𝐴 ) ) ∧ ( 1 − 𝐴 ) ≠ 0 ) → ( ℑ ‘ ( log ‘ ( 1 − 𝐴 ) ) ) ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) )
59	4 55 14 58	eel12131	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → ( ℑ ‘ ( log ‘ ( 1 − 𝐴 ) ) ) ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) )
60		iccleub	⊢ ( ( - ( π / 2 ) ∈ ℝ* ∧ ( π / 2 ) ∈ ℝ* ∧ ( ℑ ‘ ( log ‘ ( 1 − 𝐴 ) ) ) ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) ) → ( ℑ ‘ ( log ‘ ( 1 − 𝐴 ) ) ) ≤ ( π / 2 ) )
61	24 25 59 60	mp3an12i	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → ( ℑ ‘ ( log ‘ ( 1 − 𝐴 ) ) ) ≤ ( π / 2 ) )
62		pipos	⊢ 0 < π
63	18 62	elrpii	⊢ π ∈ ℝ+
64		rphalflt	⊢ ( π ∈ ℝ+ → ( π / 2 ) < π )
65	63 64	ax-mp	⊢ ( π / 2 ) < π
66	65	a1i	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → ( π / 2 ) < π )
67	17 22 23 61 66	lelttrd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → ( ℑ ‘ ( log ‘ ( 1 − 𝐴 ) ) ) < π )
68	17 67	ltned	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → ( ℑ ‘ ( log ‘ ( 1 − 𝐴 ) ) ) ≠ π )