Metamath Proof Explorer

Theorem expge1

Description: A real greater than or equal to 1 raised to a nonnegative integer is greater than or equal to 1. (Contributed by NM, 21-Feb-2005) (Revised by Mario Carneiro, 4-Jun-2014)

Ref Expression
Assertion expge1 ⊢A∈ℝ∧N∈ℕ0∧1≤A→1≤AN

Proof

Step Hyp Ref Expression
1 breq2 ⊢z=A→1≤z↔1≤A
2 1 elrab ⊢A∈z∈ℝ|1≤z↔A∈ℝ∧1≤A
3 ssrab2 ⊢z∈ℝ|1≤z⊆ℝ
4 ax-resscn ⊢ℝ⊆ℂ
5 3 4 sstri ⊢z∈ℝ|1≤z⊆ℂ
6 breq2 ⊢z=x→1≤z↔1≤x
7 6 elrab ⊢x∈z∈ℝ|1≤z↔x∈ℝ∧1≤x
8 breq2 ⊢z=y→1≤z↔1≤y
9 8 elrab ⊢y∈z∈ℝ|1≤z↔y∈ℝ∧1≤y
10 breq2 ⊢z=x⁢y→1≤z↔1≤x⁢y
11 remulcl ⊢x∈ℝ∧y∈ℝ→x⁢y∈ℝ
12 11 ad2ant2r ⊢x∈ℝ∧1≤x∧y∈ℝ∧1≤y→x⁢y∈ℝ
13 1t1e1 ⊢1⋅1=1
14 1re ⊢1∈ℝ
15 0le1 ⊢0≤1
16 14 15 pm3.2i ⊢1∈ℝ∧0≤1
17 16 jctl ⊢x∈ℝ→1∈ℝ∧0≤1∧x∈ℝ
18 16 jctl ⊢y∈ℝ→1∈ℝ∧0≤1∧y∈ℝ
19 lemul12a ⊢1∈ℝ∧0≤1∧x∈ℝ∧1∈ℝ∧0≤1∧y∈ℝ→1≤x∧1≤y→1⋅1≤x⁢y
20 17 18 19 syl2an ⊢x∈ℝ∧y∈ℝ→1≤x∧1≤y→1⋅1≤x⁢y
21 20 imp ⊢x∈ℝ∧y∈ℝ∧1≤x∧1≤y→1⋅1≤x⁢y
22 13 21 eqbrtrrid ⊢x∈ℝ∧y∈ℝ∧1≤x∧1≤y→1≤x⁢y
23 22 an4s ⊢x∈ℝ∧1≤x∧y∈ℝ∧1≤y→1≤x⁢y
24 10 12 23 elrabd ⊢x∈ℝ∧1≤x∧y∈ℝ∧1≤y→x⁢y∈z∈ℝ|1≤z
25 7 9 24 syl2anb ⊢x∈z∈ℝ|1≤z∧y∈z∈ℝ|1≤z→x⁢y∈z∈ℝ|1≤z
26 1le1 ⊢1≤1
27 breq2 ⊢z=1→1≤z↔1≤1
28 27 elrab ⊢1∈z∈ℝ|1≤z↔1∈ℝ∧1≤1
29 14 26 28 mpbir2an ⊢1∈z∈ℝ|1≤z
30 5 25 29 expcllem ⊢A∈z∈ℝ|1≤z∧N∈ℕ0→AN∈z∈ℝ|1≤z
31 2 30 sylanbr ⊢A∈ℝ∧1≤A∧N∈ℕ0→AN∈z∈ℝ|1≤z
32 31 3impa ⊢A∈ℝ∧1≤A∧N∈ℕ0→AN∈z∈ℝ|1≤z
33 32 3com23 ⊢A∈ℝ∧N∈ℕ0∧1≤A→AN∈z∈ℝ|1≤z
34 breq2 ⊢z=AN→1≤z↔1≤AN
35 34 elrab ⊢AN∈z∈ℝ|1≤z↔AN∈ℝ∧1≤AN
36 35 simprbi ⊢AN∈z∈ℝ|1≤z→1≤AN
37 33 36 syl ⊢A∈ℝ∧N∈ℕ0∧1≤A→1≤AN