Theorem leexp1ad

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

	Ref	Expression
Hypotheses	leexp1ad.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	leexp1ad.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	leexp1ad.3	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	leexp1ad.4	⊢ ( 𝜑 → 0 ≤ 𝐴 )
	leexp1ad.5	⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
Assertion	leexp1ad	⊢ ( 𝜑 → ( 𝐴 ↑ 𝑁 ) ≤ ( 𝐵 ↑ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		leexp1ad.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		leexp1ad.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		leexp1ad.3	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
4		leexp1ad.4	⊢ ( 𝜑 → 0 ≤ 𝐴 )
5		leexp1ad.5	⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
6	1 2 3	3jca	⊢ ( 𝜑 → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) )
7	6 4 5	jca32	⊢ ( 𝜑 → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵 ) ) )
8		leexp1a	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵 ) ) → ( 𝐴 ↑ 𝑁 ) ≤ ( 𝐵 ↑ 𝑁 ) )
9	7 8	syl	⊢ ( 𝜑 → ( 𝐴 ↑ 𝑁 ) ≤ ( 𝐵 ↑ 𝑁 ) )