Metamath Proof Explorer


Theorem blsconn

Description: An open ball in the complex numbers is simply connected. (Contributed by Mario Carneiro, 12-Feb-2015)

Ref Expression
Hypotheses blsconn.j J=TopOpenfld
blsconn.s S=PballabsR
blsconn.k K=J𝑡S
Assertion blsconn PR*KSConn

Proof

Step Hyp Ref Expression
1 blsconn.j J=TopOpenfld
2 blsconn.s S=PballabsR
3 blsconn.k K=J𝑡S
4 cnxmet abs∞Met
5 blssm abs∞MetPR*PballabsR
6 4 5 mp3an1 PR*PballabsR
7 2 6 eqsstrid PR*S
8 2 blcvx PR*xSySt01tx+1tyS
9 7 8 1 3 cvxsconn PR*KSConn