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 φ A
reexpcld.2 φ N 0
expge1d.3 φ 1 A
Assertion expge1d φ 1 A N

Proof

Step Hyp Ref Expression
1 reexpcld.1 φ A
2 reexpcld.2 φ N 0
3 expge1d.3 φ 1 A
4 expge1 A N 0 1 A 1 A N
5 1 2 3 4 syl3anc φ 1 A N