Theorem isosctrlem1ALTRO

Description: Lemma for isosctr. The proof of isosctrlem1ALTVD is a Virtual Deduction proof based on Saveliy Skresanov's proof of isosctrlem1. The proof of isosctrlem1ALTVD is verified by automatically transforming it into the Metamath proof of isosctrlem1ALT using completeusersproof, which is verified by the Metamath program. The proof of isosctrlem1ALTRO is a form of the completed proof which preserves the Virtual Deduction proof's step numbers and their ordering. (Contributed by Alan Sare, 22-Apr-2018.)

Assertion

Ref	Expression
isosctrlem1ALTRO	⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → (ℑ‘(log‘(1 − 𝐴))) ≠ 𝜋)

Proof of Theorem isosctrlem1ALTRO

Step	Hyp	Ref	Expression
1		id	⊢ (𝐴 ∈ ℂ → 𝐴 ∈ ℂ)
2		ax1cn	⊢ 1 ∈ ℂ
d41		subeq0	⊢ ((1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((1 − 𝐴) = 0 ↔ 1 = 𝐴))
d26	d41	biimpd	⊢ ((1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((1 − 𝐴) = 0 → 1 = 𝐴))
d1	d26	idi	⊢ ((1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((1 − 𝐴) = 0 → 1 = 𝐴))
3	2, 1, d1	sylancr	⊢ (𝐴 ∈ ℂ → ((1 − 𝐴) = 0 → 1 = 𝐴))
4	3	con3d	⊢ (𝐴 ∈ ℂ → (¬ 1 = 𝐴 → ¬ (1 − 𝐴) = 0))
d42		df-ne	⊢ ((1 − 𝐴) ≠ 0 ↔ ¬ (1 − 𝐴) = 0)
5	d42	biimpri	⊢ (¬ (1 − 𝐴) = 0 → (1 − 𝐴) ≠ 0)
6	4, 5	syl6	⊢ (𝐴 ∈ ℂ → (¬ 1 = 𝐴 → (1 − 𝐴) ≠ 0))
7	6	imp	⊢ ((𝐴 ∈ ℂ ∧ ¬ 1 = 𝐴) → (1 − 𝐴) ≠ 0)
8	1	releabsd	⊢ (𝐴 ∈ ℂ → (ℜ‘𝐴) ≤ (abs‘𝐴))
9		id	⊢ ((abs‘𝐴) = 1 → (abs‘𝐴) = 1)
d2	8	adantr	⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1) → (ℜ‘𝐴) ≤ (abs‘𝐴))
d3	9	adantl	⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1) → (abs‘𝐴) = 1)
10	d2, d3	breqtrd	⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1) → (ℜ‘𝐴) ≤ 1)
11	1	recld	⊢ (𝐴 ∈ ℂ → (ℜ‘𝐴) ∈ ℝ)
d43		1re	⊢ 1 ∈ ℝ
d4	d43	a1i	⊢ (1 ∈ ℂ → 1 ∈ ℝ)
12	2, d4	ax-mp	⊢ 1 ∈ ℝ
d44		lesub1	⊢ (((ℜ‘𝐴) ∈ ℝ ∧ 1 ∈ ℝ ∧ (ℜ‘𝐴) ∈ ℝ) → ((ℜ‘𝐴) ≤ 1 ↔ ((ℜ‘𝐴) − (ℜ‘𝐴)) ≤ (1 − (ℜ‘𝐴))))
d32	d44	3impcombi	⊢ ((1 ∈ ℝ ∧ (ℜ‘𝐴) ∈ ℝ ∧ (ℜ‘𝐴) ≤ 1) → ((ℜ‘𝐴) − (ℜ‘𝐴)) ≤ (1 − (ℜ‘𝐴)))
d5	d32	idi	⊢ ((1 ∈ ℝ ∧ (ℜ‘𝐴) ∈ ℝ ∧ (ℜ‘𝐴) ≤ 1) → ((ℜ‘𝐴) − (ℜ‘𝐴)) ≤ (1 − (ℜ‘𝐴)))
13	12, 11, 10, d5	eel0121	⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1) → ((ℜ‘𝐴) − (ℜ‘𝐴)) ≤ (1 − (ℜ‘𝐴)))
14	1	recld	⊢ (𝐴 ∈ ℂ → (ℜ‘𝐴) ∈ ℝ)
15	14	recnd	⊢ (𝐴 ∈ ℂ → (ℜ‘𝐴) ∈ ℂ)
16	15	subidd	⊢ (𝐴 ∈ ℂ → ((ℜ‘𝐴) − (ℜ‘𝐴)) = 0)
d6	16	adantr	⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1) → ((ℜ‘𝐴) − (ℜ‘𝐴)) = 0)
17	d6, 13	eqbrtrrd	⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1) → 0 ≤ (1 − (ℜ‘𝐴)))
d8	12	a1i	⊢ ( ⊤ → 1 ∈ ℝ)
d9	d8	rered	⊢ ( ⊤ → (ℜ‘1) = 1)
18	d9	trud	⊢ (ℜ‘1) = 1
d45		oveq1	⊢ ((ℜ‘1) = 1 → ((ℜ‘1) − (ℜ‘𝐴)) = (1 − (ℜ‘𝐴)))
d10	d45	eqcomd	⊢ ((ℜ‘1) = 1 → (1 − (ℜ‘𝐴)) = ((ℜ‘1) − (ℜ‘𝐴)))
19	18, d10	ax-mp	⊢ (1 − (ℜ‘𝐴)) = ((ℜ‘1) − (ℜ‘𝐴))
d46		resub	⊢ ((1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (ℜ‘(1 − 𝐴)) = ((ℜ‘1) − (ℜ‘𝐴)))
d34	d46	eqcomd	⊢ ((1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((ℜ‘1) − (ℜ‘𝐴)) = (ℜ‘(1 − 𝐴)))
d11	d34	idi	⊢ ((1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((ℜ‘1) − (ℜ‘𝐴)) = (ℜ‘(1 − 𝐴)))
20	2, 1, d11	sylancr	⊢ (𝐴 ∈ ℂ → ((ℜ‘1) − (ℜ‘𝐴)) = (ℜ‘(1 − 𝐴)))
21	19, 20	syl5eq	⊢ (𝐴 ∈ ℂ → (1 − (ℜ‘𝐴)) = (ℜ‘(1 − 𝐴)))
d12	21	adantr	⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1) → (1 − (ℜ‘𝐴)) = (ℜ‘(1 − 𝐴)))
22	17, d12	breqtrd	⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1) → 0 ≤ (ℜ‘(1 − 𝐴)))
d14	2	a1i	⊢ (𝐴 ∈ ℂ → 1 ∈ ℂ)
23	d14, 1	subcld	⊢ (𝐴 ∈ ℂ → (1 − 𝐴) ∈ ℂ)
d47		argrege0	⊢ (((1 − 𝐴) ∈ ℂ ∧ (1 − 𝐴) ≠ 0 ∧ 0 ≤ (ℜ‘(1 − 𝐴))) → (ℑ‘(log‘(1 − 𝐴))) ∈ (-(𝜋 / 2)[,](𝜋 / 2)))
d35	d47	3coml	⊢ (((1 − 𝐴) ≠ 0 ∧ 0 ≤ (ℜ‘(1 − 𝐴)) ∧ (1 − 𝐴) ∈ ℂ) → (ℑ‘(log‘(1 − 𝐴))) ∈ (-(𝜋 / 2)[,](𝜋 / 2)))
d16	d35	3com13	⊢ (((1 − 𝐴) ∈ ℂ ∧ 0 ≤ (ℜ‘(1 − 𝐴)) ∧ (1 − 𝐴) ≠ 0) → (ℑ‘(log‘(1 − 𝐴))) ∈ (-(𝜋 / 2)[,](𝜋 / 2)))
24	23, 22, 7, d16	eel12131	⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → (ℑ‘(log‘(1 − 𝐴))) ∈ (-(𝜋 / 2)[,](𝜋 / 2)))
25		pire	⊢ 𝜋 ∈ ℝ
26		2re	⊢ 2 ∈ ℝ
27		2ne0	⊢ 2 ≠ 0
28	25, 26, 27	redivcli	⊢ (𝜋 / 2) ∈ ℝ
29	28	rexri	⊢ (𝜋 / 2) ∈ ℝ*
30	28	renegcli	⊢ -(𝜋 / 2) ∈ ℝ
31	30	rexri	⊢ -(𝜋 / 2) ∈ ℝ*
d17		iccleub	⊢ ((-(𝜋 / 2) ∈ ℝ* ∧ (𝜋 / 2) ∈ ℝ* ∧ (ℑ‘(log‘(1 − 𝐴))) ∈ (-(𝜋 / 2)[,](𝜋 / 2))) → (ℑ‘(log‘(1 − 𝐴))) ≤ (𝜋 / 2))
32	31, 29, 24, d17	eel001	⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → (ℑ‘(log‘(1 − 𝐴))) ≤ (𝜋 / 2))
33		pipos	⊢ 0 < 𝜋
34	25, 33	elrpii	⊢ 𝜋 ∈ ℝ+
d18		rphalflt	⊢ (𝜋 ∈ ℝ+ → (𝜋 / 2) < 𝜋)
35	34, d18	ax-mp	⊢ (𝜋 / 2) < 𝜋
d19	23	adantr	⊢ ((𝐴 ∈ ℂ ∧ ¬ 1 = 𝐴) → (1 − 𝐴) ∈ ℂ)
36	d19, 7	logcld	⊢ ((𝐴 ∈ ℂ ∧ ¬ 1 = 𝐴) → (log‘(1 − 𝐴)) ∈ ℂ)
37	36	imcld	⊢ ((𝐴 ∈ ℂ ∧ ¬ 1 = 𝐴) → (ℑ‘(log‘(1 − 𝐴))) ∈ ℝ)
d21	28	a1i	⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → (𝜋 / 2) ∈ ℝ)
d22	35	a1i	⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → (𝜋 / 2) < 𝜋)
d23	25	a1i	⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → 𝜋 ∈ ℝ)
d24	37	3adant2	⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → (ℑ‘(log‘(1 − 𝐴))) ∈ ℝ)
38	d24, d21, d23, 32, d22	lelttrd	⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → (ℑ‘(log‘(1 − 𝐴))) < 𝜋)
qed	d24, 38	ltned	⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → (ℑ‘(log‘(1 − 𝐴))) ≠ 𝜋)