This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem leexp1ad

Description: Weak base ordering relationship for exponentiation, a deduction version. (Contributed by metakunt, 22-May-2024)

Ref Expression
Hypotheses leexp1ad.1 ⊢ φ → A ∈ ℝ
leexp1ad.2 ⊢ φ → B ∈ ℝ
leexp1ad.3 ⊢ φ → N ∈ ℕ 0
leexp1ad.4 ⊢ φ → 0 ≤ A
leexp1ad.5 ⊢ φ → A ≤ B
Assertion leexp1ad ⊢ φ → A N ≤ B N

Proof

Step Hyp Ref Expression
1 leexp1ad.1 ⊢ φ → A ∈ ℝ
2 leexp1ad.2 ⊢ φ → B ∈ ℝ
3 leexp1ad.3 ⊢ φ → N ∈ ℕ 0
4 leexp1ad.4 ⊢ φ → 0 ≤ A
5 leexp1ad.5 ⊢ φ → A ≤ B
6 leexp1a ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ N ∈ ℕ 0 ∧ 0 ≤ A ∧ A ≤ B → A N ≤ B N
7 1 2 3 4 5 6 syl32anc ⊢ φ → A N ≤ B N