Metamath Proof Explorer

Theorem knoppcnlem10

Description: Lemma for knoppcn . (Contributed by Asger C. Ipsen, 4-Apr-2021) (Revised by Asger C. Ipsen, 5-Jul-2021) Avoid ax-mulf . (Revised by GG, 19-Apr-2025)

Ref Expression
Hypotheses knoppcnlem10.t 
|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
knoppcnlem10.f 
|- F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )
knoppcnlem10.n 
|- ( ph -> N e. NN )
knoppcnlem10.1 
|- ( ph -> C e. RR )
knoppcnlem10.2 
|- ( ph -> M e. NN0 )
Assertion knoppcnlem10 
|- ( ph -> ( z e. RR |-> ( ( F ` z ) ` M ) ) e. ( ( topGen ` ran (,) ) Cn ( TopOpen ` CCfld ) ) )

Proof

Step Hyp Ref Expression
1 knoppcnlem10.t 
 |-  T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
2 knoppcnlem10.f 
 |-  F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )
3 knoppcnlem10.n 
 |-  ( ph -> N e. NN )
4 knoppcnlem10.1 
 |-  ( ph -> C e. RR )
5 knoppcnlem10.2 
 |-  ( ph -> M e. NN0 )
6 simpr 
 |-  ( ( ph /\ z e. RR ) -> z e. RR )
7 5 adantr 
 |-  ( ( ph /\ z e. RR ) -> M e. NN0 )
8 2 6 7 knoppcnlem1 
 |-  ( ( ph /\ z e. RR ) -> ( ( F ` z ) ` M ) = ( ( C ^ M ) x. ( T ` ( ( ( 2 x. N ) ^ M ) x. z ) ) ) )
9 8 mpteq2dva 
 |-  ( ph -> ( z e. RR |-> ( ( F ` z ) ` M ) ) = ( z e. RR |-> ( ( C ^ M ) x. ( T ` ( ( ( 2 x. N ) ^ M ) x. z ) ) ) ) )
10 retopon 
 |-  ( topGen ` ran (,) ) e. ( TopOn ` RR )
11 10 a1i 
 |-  ( ph -> ( topGen ` ran (,) ) e. ( TopOn ` RR ) )
12 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
13 12 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
14 13 a1i 
 |-  ( ph -> ( TopOpen ` CCfld ) e. ( TopOn ` CC ) )
15 4 recnd 
 |-  ( ph -> C e. CC )
16 15 5 expcld 
 |-  ( ph -> ( C ^ M ) e. CC )
17 11 14 16 cnmptc 
 |-  ( ph -> ( z e. RR |-> ( C ^ M ) ) e. ( ( topGen ` ran (,) ) Cn ( TopOpen ` CCfld ) ) )
18 2cnd 
 |-  ( ph -> 2 e. CC )
19 3 nncnd 
 |-  ( ph -> N e. CC )
20 18 19 mulcld 
 |-  ( ph -> ( 2 x. N ) e. CC )
21 20 5 expcld 
 |-  ( ph -> ( ( 2 x. N ) ^ M ) e. CC )
22 11 14 21 cnmptc 
 |-  ( ph -> ( z e. RR |-> ( ( 2 x. N ) ^ M ) ) e. ( ( topGen ` ran (,) ) Cn ( TopOpen ` CCfld ) ) )
23 12 tgioo2 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
24 23 oveq2i 
 |-  ( ( topGen ` ran (,) ) Cn ( topGen ` ran (,) ) ) = ( ( topGen ` ran (,) ) Cn ( ( TopOpen ` CCfld ) |`t RR ) )
25 12 cnfldtop 
 |-  ( TopOpen ` CCfld ) e. Top
26 cnrest2r 
 |-  ( ( TopOpen ` CCfld ) e. Top -> ( ( topGen ` ran (,) ) Cn ( ( TopOpen ` CCfld ) |`t RR ) ) C_ ( ( topGen ` ran (,) ) Cn ( TopOpen ` CCfld ) ) )
27 25 26 ax-mp 
 |-  ( ( topGen ` ran (,) ) Cn ( ( TopOpen ` CCfld ) |`t RR ) ) C_ ( ( topGen ` ran (,) ) Cn ( TopOpen ` CCfld ) )
28 24 27 eqsstri 
 |-  ( ( topGen ` ran (,) ) Cn ( topGen ` ran (,) ) ) C_ ( ( topGen ` ran (,) ) Cn ( TopOpen ` CCfld ) )
29 11 cnmptid 
 |-  ( ph -> ( z e. RR |-> z ) e. ( ( topGen ` ran (,) ) Cn ( topGen ` ran (,) ) ) )
30 28 29 sselid 
 |-  ( ph -> ( z e. RR |-> z ) e. ( ( topGen ` ran (,) ) Cn ( TopOpen ` CCfld ) ) )
31 12 mpomulcn 
 |-  ( u e. CC , v e. CC |-> ( u x. v ) ) e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
32 31 a1i 
 |-  ( ph -> ( u e. CC , v e. CC |-> ( u x. v ) ) e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
33 oveq12 
 |-  ( ( u = ( ( 2 x. N ) ^ M ) /\ v = z ) -> ( u x. v ) = ( ( ( 2 x. N ) ^ M ) x. z ) )
34 11 22 30 14 14 32 33 cnmpt12 
 |-  ( ph -> ( z e. RR |-> ( ( ( 2 x. N ) ^ M ) x. z ) ) e. ( ( topGen ` ran (,) ) Cn ( TopOpen ` CCfld ) ) )
35 2re 
 |-  2 e. RR
36 35 a1i 
 |-  ( ph -> 2 e. RR )
37 3 nnred 
 |-  ( ph -> N e. RR )
38 36 37 remulcld 
 |-  ( ph -> ( 2 x. N ) e. RR )
39 38 5 reexpcld 
 |-  ( ph -> ( ( 2 x. N ) ^ M ) e. RR )
40 39 adantr 
 |-  ( ( ph /\ z e. RR ) -> ( ( 2 x. N ) ^ M ) e. RR )
41 40 6 remulcld 
 |-  ( ( ph /\ z e. RR ) -> ( ( ( 2 x. N ) ^ M ) x. z ) e. RR )
42 41 fmpttd 
 |-  ( ph -> ( z e. RR |-> ( ( ( 2 x. N ) ^ M ) x. z ) ) : RR --> RR )
43 42 frnd 
 |-  ( ph -> ran ( z e. RR |-> ( ( ( 2 x. N ) ^ M ) x. z ) ) C_ RR )
44 ax-resscn 
 |-  RR C_ CC
45 44 a1i 
 |-  ( ph -> RR C_ CC )
46 cnrest2 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ ran ( z e. RR |-> ( ( ( 2 x. N ) ^ M ) x. z ) ) C_ RR /\ RR C_ CC ) -> ( ( z e. RR |-> ( ( ( 2 x. N ) ^ M ) x. z ) ) e. ( ( topGen ` ran (,) ) Cn ( TopOpen ` CCfld ) ) <-> ( z e. RR |-> ( ( ( 2 x. N ) ^ M ) x. z ) ) e. ( ( topGen ` ran (,) ) Cn ( ( TopOpen ` CCfld ) |`t RR ) ) ) )
47 13 43 45 46 mp3an2i 
 |-  ( ph -> ( ( z e. RR |-> ( ( ( 2 x. N ) ^ M ) x. z ) ) e. ( ( topGen ` ran (,) ) Cn ( TopOpen ` CCfld ) ) <-> ( z e. RR |-> ( ( ( 2 x. N ) ^ M ) x. z ) ) e. ( ( topGen ` ran (,) ) Cn ( ( TopOpen ` CCfld ) |`t RR ) ) ) )
48 34 47 mpbid 
 |-  ( ph -> ( z e. RR |-> ( ( ( 2 x. N ) ^ M ) x. z ) ) e. ( ( topGen ` ran (,) ) Cn ( ( TopOpen ` CCfld ) |`t RR ) ) )
49 48 24 eleqtrrdi 
 |-  ( ph -> ( z e. RR |-> ( ( ( 2 x. N ) ^ M ) x. z ) ) e. ( ( topGen ` ran (,) ) Cn ( topGen ` ran (,) ) ) )
50 ssid 
 |-  CC C_ CC
51 cncfss 
 |-  ( ( RR C_ CC /\ CC C_ CC ) -> ( RR -cn-> RR ) C_ ( RR -cn-> CC ) )
52 44 50 51 mp2an 
 |-  ( RR -cn-> RR ) C_ ( RR -cn-> CC )
53 1 dnicn 
 |-  T e. ( RR -cn-> RR )
54 53 a1i 
 |-  ( ph -> T e. ( RR -cn-> RR ) )
55 52 54 sselid 
 |-  ( ph -> T e. ( RR -cn-> CC ) )
56 13 toponrestid 
 |-  ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC )
57 12 23 56 cncfcn 
 |-  ( ( RR C_ CC /\ CC C_ CC ) -> ( RR -cn-> CC ) = ( ( topGen ` ran (,) ) Cn ( TopOpen ` CCfld ) ) )
58 44 50 57 mp2an 
 |-  ( RR -cn-> CC ) = ( ( topGen ` ran (,) ) Cn ( TopOpen ` CCfld ) )
59 55 58 eleqtrdi 
 |-  ( ph -> T e. ( ( topGen ` ran (,) ) Cn ( TopOpen ` CCfld ) ) )
60 11 49 59 cnmpt11f 
 |-  ( ph -> ( z e. RR |-> ( T ` ( ( ( 2 x. N ) ^ M ) x. z ) ) ) e. ( ( topGen ` ran (,) ) Cn ( TopOpen ` CCfld ) ) )
61 oveq12 
 |-  ( ( u = ( C ^ M ) /\ v = ( T ` ( ( ( 2 x. N ) ^ M ) x. z ) ) ) -> ( u x. v ) = ( ( C ^ M ) x. ( T ` ( ( ( 2 x. N ) ^ M ) x. z ) ) ) )
62 11 17 60 14 14 32 61 cnmpt12 
 |-  ( ph -> ( z e. RR |-> ( ( C ^ M ) x. ( T ` ( ( ( 2 x. N ) ^ M ) x. z ) ) ) ) e. ( ( topGen ` ran (,) ) Cn ( TopOpen ` CCfld ) ) )
63 9 62 eqeltrd 
 |-  ( ph -> ( z e. RR |-> ( ( F ` z ) ` M ) ) e. ( ( topGen ` ran (,) ) Cn ( TopOpen ` CCfld ) ) )