Metamath Proof Explorer


Theorem iihalf2cn

Description: The second half function is a continuous map. (Contributed by Mario Carneiro, 6-Jun-2014) Avoid ax-mulf . (Revised by GG, 16-Mar-2025)

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 1red 1
6 iccssre 1 2 1 1 2 1
7 4 5 6 sylancr 1 2 1
8 unitssre 0 1
9 8 a1i 0 1
10 iihalf2 x 1 2 1 2 x 1 0 1
11 10 adantl x 1 2 1 2 x 1 0 1
12 2 cnfldtopon TopOpen fld TopOn
13 12 a1i TopOpen fld TopOn
14 2cnd 2
15 13 13 14 cnmptc x 2 TopOpen fld Cn TopOpen fld
16 13 cnmptid x x TopOpen fld Cn TopOpen fld
17 2 mpomulcn u , v u v TopOpen fld × t TopOpen fld Cn TopOpen fld
18 17 a1i u , v u v TopOpen fld × t TopOpen fld Cn TopOpen fld
19 oveq12 u = 2 v = x u v = 2 x
20 13 15 16 13 13 18 19 cnmpt12 x 2 x TopOpen fld Cn TopOpen fld
21 1cnd 1
22 13 13 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 13 20 22 24 cnmpt12f x 2 x 1 TopOpen fld Cn TopOpen fld
26 2 1 3 7 9 11 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