Metamath Proof Explorer


Theorem raddcn

Description: Addition in the real numbers is a continuous function. (Contributed by Thierry Arnoux, 23-May-2017)

Ref Expression
Hypothesis raddcn.1 J = topGen ran .
Assertion raddcn x , y x + y J × t J Cn J

Proof

Step Hyp Ref Expression
1 raddcn.1 J = topGen ran .
2 eqid TopOpen fld = TopOpen fld
3 2 addcn + TopOpen fld × t TopOpen fld Cn TopOpen fld
4 ax-resscn
5 xpss12 2 ×
6 4 4 5 mp2an 2 ×
7 2 cnfldtop TopOpen fld Top
8 2 cnfldtopon TopOpen fld TopOn
9 8 toponunii = TopOpen fld
10 7 7 9 9 txunii × = TopOpen fld × t TopOpen fld
11 10 cnrest + TopOpen fld × t TopOpen fld Cn TopOpen fld 2 × + 2 TopOpen fld × t TopOpen fld 𝑡 2 Cn TopOpen fld
12 3 6 11 mp2an + 2 TopOpen fld × t TopOpen fld 𝑡 2 Cn TopOpen fld
13 reex V
14 txrest TopOpen fld Top TopOpen fld Top V V TopOpen fld × t TopOpen fld 𝑡 2 = TopOpen fld 𝑡 × t TopOpen fld 𝑡
15 7 7 13 13 14 mp4an TopOpen fld × t TopOpen fld 𝑡 2 = TopOpen fld 𝑡 × t TopOpen fld 𝑡
16 2 tgioo2 topGen ran . = TopOpen fld 𝑡
17 1 16 eqtr2i TopOpen fld 𝑡 = J
18 17 17 oveq12i TopOpen fld 𝑡 × t TopOpen fld 𝑡 = J × t J
19 15 18 eqtri TopOpen fld × t TopOpen fld 𝑡 2 = J × t J
20 19 oveq1i TopOpen fld × t TopOpen fld 𝑡 2 Cn TopOpen fld = J × t J Cn TopOpen fld
21 12 20 eleqtri + 2 J × t J Cn TopOpen fld
22 ax-addf + : ×
23 ffn + : × + Fn ×
24 22 23 ax-mp + Fn ×
25 fnssres + Fn × 2 × + 2 Fn 2
26 24 6 25 mp2an + 2 Fn 2
27 fnov + 2 Fn 2 + 2 = x , y x + 2 y
28 26 27 mpbi + 2 = x , y x + 2 y
29 ovres x y x + 2 y = x + y
30 29 mpoeq3ia x , y x + 2 y = x , y x + y
31 28 30 eqtri + 2 = x , y x + y
32 31 rneqi ran + 2 = ran x , y x + y
33 readdcl x y x + y
34 33 rgen2a x y x + y
35 eqid x , y x + y = x , y x + y
36 35 rnmposs x y x + y ran x , y x + y
37 34 36 ax-mp ran x , y x + y
38 32 37 eqsstri ran + 2
39 cnrest2 TopOpen fld TopOn ran + 2 + 2 J × t J Cn TopOpen fld + 2 J × t J Cn TopOpen fld 𝑡
40 8 38 4 39 mp3an + 2 J × t J Cn TopOpen fld + 2 J × t J Cn TopOpen fld 𝑡
41 21 40 mpbi + 2 J × t J Cn TopOpen fld 𝑡
42 17 oveq2i J × t J Cn TopOpen fld 𝑡 = J × t J Cn J
43 41 31 42 3eltr3i x , y x + y J × t J Cn J