Metamath Proof Explorer


Theorem expge1d

Description: A real greater than or equal to 1 raised to a nonnegative integer is greater than or equal to 1. (Contributed by Mario Carneiro, 28-May-2016)

Ref Expression
Hypotheses reexpcld.1
|- ( ph -> A e. RR )
reexpcld.2
|- ( ph -> N e. NN0 )
expge1d.3
|- ( ph -> 1 <_ A )
Assertion expge1d
|- ( ph -> 1 <_ ( A ^ N ) )

Proof

Step Hyp Ref Expression
1 reexpcld.1
 |-  ( ph -> A e. RR )
2 reexpcld.2
 |-  ( ph -> N e. NN0 )
3 expge1d.3
 |-  ( ph -> 1 <_ A )
4 expge1
 |-  ( ( A e. RR /\ N e. NN0 /\ 1 <_ A ) -> 1 <_ ( A ^ N ) )
5 1 2 3 4 syl3anc
 |-  ( ph -> 1 <_ ( A ^ N ) )