Metamath Proof Explorer

Definition df-iccp

Description: Define partitions of a closed interval of extended reals. Such partitions are finite increasing sequences of extended reals. (Contributed by AV, 8-Jul-2020)

Ref Expression
Assertion df-iccp 
|- RePart = ( m e. NN |-> { p e. ( RR* ^m ( 0 ... m ) ) | A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ciccp 
 |-  RePart
1 vm 
 |-  m
2 cn 
 |-  NN
3 vp 
 |-  p
4 cxr 
 |-  RR*
5 cmap 
 |-  ^m
6 cc0 
 |-  0
7 cfz 
 |-  ...
8 1 cv 
 |-  m
9 6 8 7 co 
 |-  ( 0 ... m )
10 4 9 5 co 
 |-  ( RR* ^m ( 0 ... m ) )
11 vi 
 |-  i
12 cfzo 
 |-  ..^
13 6 8 12 co 
 |-  ( 0 ..^ m )
14 3 cv 
 |-  p
15 11 cv 
 |-  i
16 15 14 cfv 
 |-  ( p ` i )
17 clt 
 |-  <
18 caddc 
 |-  +
19 c1 
 |-  1
20 15 19 18 co 
 |-  ( i + 1 )
21 20 14 cfv 
 |-  ( p ` ( i + 1 ) )
22 16 21 17 wbr 
 |-  ( p ` i ) < ( p ` ( i + 1 ) )
23 22 11 13 wral 
 |-  A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) )
24 23 3 10 crab 
 |-  { p e. ( RR* ^m ( 0 ... m ) ) | A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) }
25 1 2 24 cmpt 
 |-  ( m e. NN |-> { p e. ( RR* ^m ( 0 ... m ) ) | A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) } )
26 0 25 wceq 
 |-  RePart = ( m e. NN |-> { p e. ( RR* ^m ( 0 ... m ) ) | A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) } )