Metamath Proof Explorer

Theorem rprisefaccl

Description: Closure law for rising factorial. (Contributed by Scott Fenton, 9-Jan-2018)

Ref Expression
Assertion rprisefaccl 
|- ( ( A e. RR+ /\ N e. NN0 ) -> ( A RiseFac N ) e. RR+ )

Proof

Step Hyp Ref Expression
1 rpssre 
 |-  RR+ C_ RR
2 ax-resscn 
 |-  RR C_ CC
3 1 2 sstri 
 |-  RR+ C_ CC
4 1rp 
 |-  1 e. RR+
5 rpmulcl 
 |-  ( ( x e. RR+ /\ y e. RR+ ) -> ( x x. y ) e. RR+ )
6 rpre 
 |-  ( A e. RR+ -> A e. RR )
7 nn0re 
 |-  ( k e. NN0 -> k e. RR )
8 readdcl 
 |-  ( ( A e. RR /\ k e. RR ) -> ( A + k ) e. RR )
9 6 7 8 syl2an 
 |-  ( ( A e. RR+ /\ k e. NN0 ) -> ( A + k ) e. RR )
10 6 adantr 
 |-  ( ( A e. RR+ /\ k e. NN0 ) -> A e. RR )
11 7 adantl 
 |-  ( ( A e. RR+ /\ k e. NN0 ) -> k e. RR )
12 rpgt0 
 |-  ( A e. RR+ -> 0 < A )
13 12 adantr 
 |-  ( ( A e. RR+ /\ k e. NN0 ) -> 0 < A )
14 nn0ge0 
 |-  ( k e. NN0 -> 0 <_ k )
15 14 adantl 
 |-  ( ( A e. RR+ /\ k e. NN0 ) -> 0 <_ k )
16 10 11 13 15 addgtge0d 
 |-  ( ( A e. RR+ /\ k e. NN0 ) -> 0 < ( A + k ) )
17 9 16 elrpd 
 |-  ( ( A e. RR+ /\ k e. NN0 ) -> ( A + k ) e. RR+ )
18 3 4 5 17 risefaccllem 
 |-  ( ( A e. RR+ /\ N e. NN0 ) -> ( A RiseFac N ) e. RR+ )