Theorem leexp1ad

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

	Ref	Expression
Hypotheses	leexp1ad.1	$$⊢\phi \to A\in ℝ$$
	leexp1ad.2	$$⊢\phi \to B\in ℝ$$
	leexp1ad.3	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	leexp1ad.4	$$⊢\phi \to 0\le A$$
	leexp1ad.5	$$⊢\phi \to A\le B$$
Assertion	leexp1ad	$$⊢\phi \to A^N\le B^N$$

Proof

Step	Hyp	Ref	Expression
1		leexp1ad.1	$$⊢\phi \to A\in ℝ$$
2		leexp1ad.2	$$⊢\phi \to B\in ℝ$$
3		leexp1ad.3	$$⊢\phi \to N\in {\mathbb{N}}_0$$
4		leexp1ad.4	$$⊢\phi \to 0\le A$$
5		leexp1ad.5	$$⊢\phi \to A\le B$$
6	1 2 3	3jca	$$⊢\phi \to \left(A\in ℝ\wedge B\in ℝ\wedge N\in {\mathbb{N}}_0\right)$$
7	6 4 5	jca32	$$⊢\phi \to \left(\left(A\in ℝ\wedge B\in ℝ\wedge N\in {\mathbb{N}}_0\right)\wedge \left(0\le A\wedge A\le B\right)\right)$$
8		leexp1a	$$⊢\left(\left(A\in ℝ\wedge B\in ℝ\wedge N\in {\mathbb{N}}_0\right)\wedge \left(0\le A\wedge A\le B\right)\right)\to A^N\le B^N$$
9	7 8	syl	$$⊢\phi \to A^N\le B^N$$