Theorem leexp1ad

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

	Ref	Expression
Hypotheses	leexp1ad.1	|- ( ph -> A e. RR )
	leexp1ad.2	|- ( ph -> B e. RR )
	leexp1ad.3	|- ( ph -> N e. NN0 )
	leexp1ad.4	|- ( ph -> 0 <_ A )
	leexp1ad.5	|- ( ph -> A <_ B )
Assertion	leexp1ad	|- ( ph -> ( A ^ N ) <_ ( B ^ N ) )

Proof

Step	Hyp	Ref	Expression
1		leexp1ad.1	|- ( ph -> A e. RR )
2		leexp1ad.2	|- ( ph -> B e. RR )
3		leexp1ad.3	|- ( ph -> N e. NN0 )
4		leexp1ad.4	|- ( ph -> 0 <_ A )
5		leexp1ad.5	|- ( ph -> A <_ B )
6	1 2 3	3jca	|- ( ph -> ( A e. RR /\ B e. RR /\ N e. NN0 ) )
7	6 4 5	jca32	|- ( ph -> ( ( A e. RR /\ B e. RR /\ N e. NN0 ) /\ ( 0 <_ A /\ A <_ B ) ) )
8		leexp1a	|- ( ( ( A e. RR /\ B e. RR /\ N e. NN0 ) /\ ( 0 <_ A /\ A <_ B ) ) -> ( A ^ N ) <_ ( B ^ N ) )
9	7 8	syl	|- ( ph -> ( A ^ N ) <_ ( B ^ N ) )