Metamath Proof Explorer

Theorem iihalf2cn

Description: The second half function is a continuous map. (Contributed by Mario Carneiro, 6-Jun-2014)

Ref Expression
Hypothesis iihalf2cn.1 ⊢ J = topGen ⁡ ran ⁡ . ↾ 𝑡 1 2 1
Assertion iihalf2cn ⊢ x ∈ 1 2 1 ⟼ 2 ⁢ x − 1 ∈ J Cn II

Proof

Step Hyp Ref Expression
1 iihalf2cn.1 ⊢ J = topGen ⁡ ran ⁡ . ↾ 𝑡 1 2 1
2 eqid ⊢ TopOpen ⁡ ℂ fld = TopOpen ⁡ ℂ fld
3 dfii2 ⊢ II = topGen ⁡ ran ⁡ . ↾ 𝑡 0 1
4 halfre ⊢ 1 2 ∈ ℝ
5 1re ⊢ 1 ∈ ℝ
6 iccssre ⊢ 1 2 ∈ ℝ ∧ 1 ∈ ℝ → 1 2 1 ⊆ ℝ
7 4 5 6 mp2an ⊢ 1 2 1 ⊆ ℝ
8 7 a1i ⊢ ⊤ → 1 2 1 ⊆ ℝ
9 unitssre ⊢ 0 1 ⊆ ℝ
10 9 a1i ⊢ ⊤ → 0 1 ⊆ ℝ
11 iihalf2 ⊢ x ∈ 1 2 1 → 2 ⁢ x − 1 ∈ 0 1
12 11 adantl ⊢ ⊤ ∧ x ∈ 1 2 1 → 2 ⁢ x − 1 ∈ 0 1
13 2 cnfldtopon ⊢ TopOpen ⁡ ℂ fld ∈ TopOn ⁡ ℂ
14 13 a1i ⊢ ⊤ → TopOpen ⁡ ℂ fld ∈ TopOn ⁡ ℂ
15 2cnd ⊢ ⊤ → 2 ∈ ℂ
16 14 14 15 cnmptc ⊢ ⊤ → x ∈ ℂ ⟼ 2 ∈ TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
17 14 cnmptid ⊢ ⊤ → x ∈ ℂ ⟼ x ∈ TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
18 2 mulcn ⊢ × ∈ TopOpen ⁡ ℂ fld × t TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
19 18 a1i ⊢ ⊤ → × ∈ TopOpen ⁡ ℂ fld × t TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
20 14 16 17 19 cnmpt12f ⊢ ⊤ → x ∈ ℂ ⟼ 2 ⁢ x ∈ TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
21 1cnd ⊢ ⊤ → 1 ∈ ℂ
22 14 14 21 cnmptc ⊢ ⊤ → x ∈ ℂ ⟼ 1 ∈ TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
23 2 subcn ⊢ − ∈ TopOpen ⁡ ℂ fld × t TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
24 23 a1i ⊢ ⊤ → − ∈ TopOpen ⁡ ℂ fld × t TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
25 14 20 22 24 cnmpt12f ⊢ ⊤ → x ∈ ℂ ⟼ 2 ⁢ x − 1 ∈ TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
26 2 1 3 8 10 12 25 cnmptre ⊢ ⊤ → x ∈ 1 2 1 ⟼ 2 ⁢ x − 1 ∈ J Cn II
27 26 mptru ⊢ x ∈ 1 2 1 ⟼ 2 ⁢ x − 1 ∈ J Cn II