Metamath Proof Explorer

Theorem cpnord

Description: C^n conditions are ordered by strength. (Contributed by Stefan O'Rear, 16-Nov-2014) (Revised by Mario Carneiro, 11-Feb-2015)

Ref Expression
Assertion cpnord 
|- ( ( S e. { RR , CC } /\ M e. NN0 /\ N e. ( ZZ>= ` M ) ) -> ( ( C^n ` S ) ` N ) C_ ( ( C^n ` S ) ` M ) )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( n = M -> ( ( C^n ` S ) ` n ) = ( ( C^n ` S ) ` M ) )
2 1 sseq1d 
 |-  ( n = M -> ( ( ( C^n ` S ) ` n ) C_ ( ( C^n ` S ) ` M ) <-> ( ( C^n ` S ) ` M ) C_ ( ( C^n ` S ) ` M ) ) )
3 2 imbi2d 
 |-  ( n = M -> ( ( ( S e. { RR , CC } /\ M e. NN0 ) -> ( ( C^n ` S ) ` n ) C_ ( ( C^n ` S ) ` M ) ) <-> ( ( S e. { RR , CC } /\ M e. NN0 ) -> ( ( C^n ` S ) ` M ) C_ ( ( C^n ` S ) ` M ) ) ) )
4 fveq2 
 |-  ( n = m -> ( ( C^n ` S ) ` n ) = ( ( C^n ` S ) ` m ) )
5 4 sseq1d 
 |-  ( n = m -> ( ( ( C^n ` S ) ` n ) C_ ( ( C^n ` S ) ` M ) <-> ( ( C^n ` S ) ` m ) C_ ( ( C^n ` S ) ` M ) ) )
6 5 imbi2d 
 |-  ( n = m -> ( ( ( S e. { RR , CC } /\ M e. NN0 ) -> ( ( C^n ` S ) ` n ) C_ ( ( C^n ` S ) ` M ) ) <-> ( ( S e. { RR , CC } /\ M e. NN0 ) -> ( ( C^n ` S ) ` m ) C_ ( ( C^n ` S ) ` M ) ) ) )
7 fveq2 
 |-  ( n = ( m + 1 ) -> ( ( C^n ` S ) ` n ) = ( ( C^n ` S ) ` ( m + 1 ) ) )
8 7 sseq1d 
 |-  ( n = ( m + 1 ) -> ( ( ( C^n ` S ) ` n ) C_ ( ( C^n ` S ) ` M ) <-> ( ( C^n ` S ) ` ( m + 1 ) ) C_ ( ( C^n ` S ) ` M ) ) )
9 8 imbi2d 
 |-  ( n = ( m + 1 ) -> ( ( ( S e. { RR , CC } /\ M e. NN0 ) -> ( ( C^n ` S ) ` n ) C_ ( ( C^n ` S ) ` M ) ) <-> ( ( S e. { RR , CC } /\ M e. NN0 ) -> ( ( C^n ` S ) ` ( m + 1 ) ) C_ ( ( C^n ` S ) ` M ) ) ) )
10 fveq2 
 |-  ( n = N -> ( ( C^n ` S ) ` n ) = ( ( C^n ` S ) ` N ) )
11 10 sseq1d 
 |-  ( n = N -> ( ( ( C^n ` S ) ` n ) C_ ( ( C^n ` S ) ` M ) <-> ( ( C^n ` S ) ` N ) C_ ( ( C^n ` S ) ` M ) ) )
12 11 imbi2d 
 |-  ( n = N -> ( ( ( S e. { RR , CC } /\ M e. NN0 ) -> ( ( C^n ` S ) ` n ) C_ ( ( C^n ` S ) ` M ) ) <-> ( ( S e. { RR , CC } /\ M e. NN0 ) -> ( ( C^n ` S ) ` N ) C_ ( ( C^n ` S ) ` M ) ) ) )
13 ssid 
 |-  ( ( C^n ` S ) ` M ) C_ ( ( C^n ` S ) ` M )
14 13 2a1i 
 |-  ( M e. ZZ -> ( ( S e. { RR , CC } /\ M e. NN0 ) -> ( ( C^n ` S ) ` M ) C_ ( ( C^n ` S ) ` M ) ) )
15 simprl 
 |-  ( ( ( ( S e. { RR , CC } /\ M e. NN0 ) /\ m e. ( ZZ>= ` M ) ) /\ ( f e. ( CC ^pm S ) /\ ( ( S Dn f ) ` ( m + 1 ) ) e. ( dom f -cn-> CC ) ) ) -> f e. ( CC ^pm S ) )
16 recnprss 
 |-  ( S e. { RR , CC } -> S C_ CC )
17 16 ad2antrr 
 |-  ( ( ( S e. { RR , CC } /\ M e. NN0 ) /\ m e. ( ZZ>= ` M ) ) -> S C_ CC )
18 17 adantr 
 |-  ( ( ( ( S e. { RR , CC } /\ M e. NN0 ) /\ m e. ( ZZ>= ` M ) ) /\ ( f e. ( CC ^pm S ) /\ ( ( S Dn f ) ` ( m + 1 ) ) e. ( dom f -cn-> CC ) ) ) -> S C_ CC )
19 simplll 
 |-  ( ( ( ( S e. { RR , CC } /\ M e. NN0 ) /\ m e. ( ZZ>= ` M ) ) /\ ( f e. ( CC ^pm S ) /\ ( ( S Dn f ) ` ( m + 1 ) ) e. ( dom f -cn-> CC ) ) ) -> S e. { RR , CC } )
20 eluznn0 
 |-  ( ( M e. NN0 /\ m e. ( ZZ>= ` M ) ) -> m e. NN0 )
21 20 adantll 
 |-  ( ( ( S e. { RR , CC } /\ M e. NN0 ) /\ m e. ( ZZ>= ` M ) ) -> m e. NN0 )
22 21 adantr 
 |-  ( ( ( ( S e. { RR , CC } /\ M e. NN0 ) /\ m e. ( ZZ>= ` M ) ) /\ ( f e. ( CC ^pm S ) /\ ( ( S Dn f ) ` ( m + 1 ) ) e. ( dom f -cn-> CC ) ) ) -> m e. NN0 )
23 dvnf 
 |-  ( ( S e. { RR , CC } /\ f e. ( CC ^pm S ) /\ m e. NN0 ) -> ( ( S Dn f ) ` m ) : dom ( ( S Dn f ) ` m ) --> CC )
24 19 15 22 23 syl3anc 
 |-  ( ( ( ( S e. { RR , CC } /\ M e. NN0 ) /\ m e. ( ZZ>= ` M ) ) /\ ( f e. ( CC ^pm S ) /\ ( ( S Dn f ) ` ( m + 1 ) ) e. ( dom f -cn-> CC ) ) ) -> ( ( S Dn f ) ` m ) : dom ( ( S Dn f ) ` m ) --> CC )
25 dvnbss 
 |-  ( ( S e. { RR , CC } /\ f e. ( CC ^pm S ) /\ m e. NN0 ) -> dom ( ( S Dn f ) ` m ) C_ dom f )
26 19 15 22 25 syl3anc 
 |-  ( ( ( ( S e. { RR , CC } /\ M e. NN0 ) /\ m e. ( ZZ>= ` M ) ) /\ ( f e. ( CC ^pm S ) /\ ( ( S Dn f ) ` ( m + 1 ) ) e. ( dom f -cn-> CC ) ) ) -> dom ( ( S Dn f ) ` m ) C_ dom f )
27 dvnp1 
 |-  ( ( S C_ CC /\ f e. ( CC ^pm S ) /\ m e. NN0 ) -> ( ( S Dn f ) ` ( m + 1 ) ) = ( S _D ( ( S Dn f ) ` m ) ) )
28 18 15 22 27 syl3anc 
 |-  ( ( ( ( S e. { RR , CC } /\ M e. NN0 ) /\ m e. ( ZZ>= ` M ) ) /\ ( f e. ( CC ^pm S ) /\ ( ( S Dn f ) ` ( m + 1 ) ) e. ( dom f -cn-> CC ) ) ) -> ( ( S Dn f ) ` ( m + 1 ) ) = ( S _D ( ( S Dn f ) ` m ) ) )
29 simprr 
 |-  ( ( ( ( S e. { RR , CC } /\ M e. NN0 ) /\ m e. ( ZZ>= ` M ) ) /\ ( f e. ( CC ^pm S ) /\ ( ( S Dn f ) ` ( m + 1 ) ) e. ( dom f -cn-> CC ) ) ) -> ( ( S Dn f ) ` ( m + 1 ) ) e. ( dom f -cn-> CC ) )
30 28 29 eqeltrrd 
 |-  ( ( ( ( S e. { RR , CC } /\ M e. NN0 ) /\ m e. ( ZZ>= ` M ) ) /\ ( f e. ( CC ^pm S ) /\ ( ( S Dn f ) ` ( m + 1 ) ) e. ( dom f -cn-> CC ) ) ) -> ( S _D ( ( S Dn f ) ` m ) ) e. ( dom f -cn-> CC ) )
31 cncff 
 |-  ( ( S _D ( ( S Dn f ) ` m ) ) e. ( dom f -cn-> CC ) -> ( S _D ( ( S Dn f ) ` m ) ) : dom f --> CC )
32 30 31 syl 
 |-  ( ( ( ( S e. { RR , CC } /\ M e. NN0 ) /\ m e. ( ZZ>= ` M ) ) /\ ( f e. ( CC ^pm S ) /\ ( ( S Dn f ) ` ( m + 1 ) ) e. ( dom f -cn-> CC ) ) ) -> ( S _D ( ( S Dn f ) ` m ) ) : dom f --> CC )
33 32 fdmd 
 |-  ( ( ( ( S e. { RR , CC } /\ M e. NN0 ) /\ m e. ( ZZ>= ` M ) ) /\ ( f e. ( CC ^pm S ) /\ ( ( S Dn f ) ` ( m + 1 ) ) e. ( dom f -cn-> CC ) ) ) -> dom ( S _D ( ( S Dn f ) ` m ) ) = dom f )
34 cnex 
 |-  CC e. _V
35 elpm2g 
 |-  ( ( CC e. _V /\ S e. { RR , CC } ) -> ( f e. ( CC ^pm S ) <-> ( f : dom f --> CC /\ dom f C_ S ) ) )
36 34 19 35 sylancr 
 |-  ( ( ( ( S e. { RR , CC } /\ M e. NN0 ) /\ m e. ( ZZ>= ` M ) ) /\ ( f e. ( CC ^pm S ) /\ ( ( S Dn f ) ` ( m + 1 ) ) e. ( dom f -cn-> CC ) ) ) -> ( f e. ( CC ^pm S ) <-> ( f : dom f --> CC /\ dom f C_ S ) ) )
37 15 36 mpbid 
 |-  ( ( ( ( S e. { RR , CC } /\ M e. NN0 ) /\ m e. ( ZZ>= ` M ) ) /\ ( f e. ( CC ^pm S ) /\ ( ( S Dn f ) ` ( m + 1 ) ) e. ( dom f -cn-> CC ) ) ) -> ( f : dom f --> CC /\ dom f C_ S ) )
38 37 simprd 
 |-  ( ( ( ( S e. { RR , CC } /\ M e. NN0 ) /\ m e. ( ZZ>= ` M ) ) /\ ( f e. ( CC ^pm S ) /\ ( ( S Dn f ) ` ( m + 1 ) ) e. ( dom f -cn-> CC ) ) ) -> dom f C_ S )
39 26 38 sstrd 
 |-  ( ( ( ( S e. { RR , CC } /\ M e. NN0 ) /\ m e. ( ZZ>= ` M ) ) /\ ( f e. ( CC ^pm S ) /\ ( ( S Dn f ) ` ( m + 1 ) ) e. ( dom f -cn-> CC ) ) ) -> dom ( ( S Dn f ) ` m ) C_ S )
40 18 24 39 dvbss 
 |-  ( ( ( ( S e. { RR , CC } /\ M e. NN0 ) /\ m e. ( ZZ>= ` M ) ) /\ ( f e. ( CC ^pm S ) /\ ( ( S Dn f ) ` ( m + 1 ) ) e. ( dom f -cn-> CC ) ) ) -> dom ( S _D ( ( S Dn f ) ` m ) ) C_ dom ( ( S Dn f ) ` m ) )
41 33 40 eqsstrrd 
 |-  ( ( ( ( S e. { RR , CC } /\ M e. NN0 ) /\ m e. ( ZZ>= ` M ) ) /\ ( f e. ( CC ^pm S ) /\ ( ( S Dn f ) ` ( m + 1 ) ) e. ( dom f -cn-> CC ) ) ) -> dom f C_ dom ( ( S Dn f ) ` m ) )
42 26 41 eqssd 
 |-  ( ( ( ( S e. { RR , CC } /\ M e. NN0 ) /\ m e. ( ZZ>= ` M ) ) /\ ( f e. ( CC ^pm S ) /\ ( ( S Dn f ) ` ( m + 1 ) ) e. ( dom f -cn-> CC ) ) ) -> dom ( ( S Dn f ) ` m ) = dom f )
43 42 feq2d 
 |-  ( ( ( ( S e. { RR , CC } /\ M e. NN0 ) /\ m e. ( ZZ>= ` M ) ) /\ ( f e. ( CC ^pm S ) /\ ( ( S Dn f ) ` ( m + 1 ) ) e. ( dom f -cn-> CC ) ) ) -> ( ( ( S Dn f ) ` m ) : dom ( ( S Dn f ) ` m ) --> CC <-> ( ( S Dn f ) ` m ) : dom f --> CC ) )
44 24 43 mpbid 
 |-  ( ( ( ( S e. { RR , CC } /\ M e. NN0 ) /\ m e. ( ZZ>= ` M ) ) /\ ( f e. ( CC ^pm S ) /\ ( ( S Dn f ) ` ( m + 1 ) ) e. ( dom f -cn-> CC ) ) ) -> ( ( S Dn f ) ` m ) : dom f --> CC )
45 dvcn 
 |-  ( ( ( S C_ CC /\ ( ( S Dn f ) ` m ) : dom f --> CC /\ dom f C_ S ) /\ dom ( S _D ( ( S Dn f ) ` m ) ) = dom f ) -> ( ( S Dn f ) ` m ) e. ( dom f -cn-> CC ) )
46 18 44 38 33 45 syl31anc 
 |-  ( ( ( ( S e. { RR , CC } /\ M e. NN0 ) /\ m e. ( ZZ>= ` M ) ) /\ ( f e. ( CC ^pm S ) /\ ( ( S Dn f ) ` ( m + 1 ) ) e. ( dom f -cn-> CC ) ) ) -> ( ( S Dn f ) ` m ) e. ( dom f -cn-> CC ) )
47 15 46 jca 
 |-  ( ( ( ( S e. { RR , CC } /\ M e. NN0 ) /\ m e. ( ZZ>= ` M ) ) /\ ( f e. ( CC ^pm S ) /\ ( ( S Dn f ) ` ( m + 1 ) ) e. ( dom f -cn-> CC ) ) ) -> ( f e. ( CC ^pm S ) /\ ( ( S Dn f ) ` m ) e. ( dom f -cn-> CC ) ) )
48 47 ex 
 |-  ( ( ( S e. { RR , CC } /\ M e. NN0 ) /\ m e. ( ZZ>= ` M ) ) -> ( ( f e. ( CC ^pm S ) /\ ( ( S Dn f ) ` ( m + 1 ) ) e. ( dom f -cn-> CC ) ) -> ( f e. ( CC ^pm S ) /\ ( ( S Dn f ) ` m ) e. ( dom f -cn-> CC ) ) ) )
49 peano2nn0 
 |-  ( m e. NN0 -> ( m + 1 ) e. NN0 )
50 21 49 syl 
 |-  ( ( ( S e. { RR , CC } /\ M e. NN0 ) /\ m e. ( ZZ>= ` M ) ) -> ( m + 1 ) e. NN0 )
51 elcpn 
 |-  ( ( S C_ CC /\ ( m + 1 ) e. NN0 ) -> ( f e. ( ( C^n ` S ) ` ( m + 1 ) ) <-> ( f e. ( CC ^pm S ) /\ ( ( S Dn f ) ` ( m + 1 ) ) e. ( dom f -cn-> CC ) ) ) )
52 17 50 51 syl2anc 
 |-  ( ( ( S e. { RR , CC } /\ M e. NN0 ) /\ m e. ( ZZ>= ` M ) ) -> ( f e. ( ( C^n ` S ) ` ( m + 1 ) ) <-> ( f e. ( CC ^pm S ) /\ ( ( S Dn f ) ` ( m + 1 ) ) e. ( dom f -cn-> CC ) ) ) )
53 elcpn 
 |-  ( ( S C_ CC /\ m e. NN0 ) -> ( f e. ( ( C^n ` S ) ` m ) <-> ( f e. ( CC ^pm S ) /\ ( ( S Dn f ) ` m ) e. ( dom f -cn-> CC ) ) ) )
54 17 21 53 syl2anc 
 |-  ( ( ( S e. { RR , CC } /\ M e. NN0 ) /\ m e. ( ZZ>= ` M ) ) -> ( f e. ( ( C^n ` S ) ` m ) <-> ( f e. ( CC ^pm S ) /\ ( ( S Dn f ) ` m ) e. ( dom f -cn-> CC ) ) ) )
55 48 52 54 3imtr4d 
 |-  ( ( ( S e. { RR , CC } /\ M e. NN0 ) /\ m e. ( ZZ>= ` M ) ) -> ( f e. ( ( C^n ` S ) ` ( m + 1 ) ) -> f e. ( ( C^n ` S ) ` m ) ) )
56 55 ssrdv 
 |-  ( ( ( S e. { RR , CC } /\ M e. NN0 ) /\ m e. ( ZZ>= ` M ) ) -> ( ( C^n ` S ) ` ( m + 1 ) ) C_ ( ( C^n ` S ) ` m ) )
57 sstr2 
 |-  ( ( ( C^n ` S ) ` ( m + 1 ) ) C_ ( ( C^n ` S ) ` m ) -> ( ( ( C^n ` S ) ` m ) C_ ( ( C^n ` S ) ` M ) -> ( ( C^n ` S ) ` ( m + 1 ) ) C_ ( ( C^n ` S ) ` M ) ) )
58 56 57 syl 
 |-  ( ( ( S e. { RR , CC } /\ M e. NN0 ) /\ m e. ( ZZ>= ` M ) ) -> ( ( ( C^n ` S ) ` m ) C_ ( ( C^n ` S ) ` M ) -> ( ( C^n ` S ) ` ( m + 1 ) ) C_ ( ( C^n ` S ) ` M ) ) )
59 58 expcom 
 |-  ( m e. ( ZZ>= ` M ) -> ( ( S e. { RR , CC } /\ M e. NN0 ) -> ( ( ( C^n ` S ) ` m ) C_ ( ( C^n ` S ) ` M ) -> ( ( C^n ` S ) ` ( m + 1 ) ) C_ ( ( C^n ` S ) ` M ) ) ) )
60 59 a2d 
 |-  ( m e. ( ZZ>= ` M ) -> ( ( ( S e. { RR , CC } /\ M e. NN0 ) -> ( ( C^n ` S ) ` m ) C_ ( ( C^n ` S ) ` M ) ) -> ( ( S e. { RR , CC } /\ M e. NN0 ) -> ( ( C^n ` S ) ` ( m + 1 ) ) C_ ( ( C^n ` S ) ` M ) ) ) )
61 3 6 9 12 14 60 uzind4 
 |-  ( N e. ( ZZ>= ` M ) -> ( ( S e. { RR , CC } /\ M e. NN0 ) -> ( ( C^n ` S ) ` N ) C_ ( ( C^n ` S ) ` M ) ) )
62 61 com12 
 |-  ( ( S e. { RR , CC } /\ M e. NN0 ) -> ( N e. ( ZZ>= ` M ) -> ( ( C^n ` S ) ` N ) C_ ( ( C^n ` S ) ` M ) ) )
63 62 3impia 
 |-  ( ( S e. { RR , CC } /\ M e. NN0 /\ N e. ( ZZ>= ` M ) ) -> ( ( C^n ` S ) ` N ) C_ ( ( C^n ` S ) ` M ) )