Theorem lcmineqlem9

Description: (1-x)^(N-M) is continuous. (Contributed by metakunt, 12-May-2024)

	Ref	Expression
Hypotheses	lcmineqlem9.1	|- ( ph -> M e. NN )
	lcmineqlem9.2	|- ( ph -> N e. NN )
	lcmineqlem9.3	|- ( ph -> M <_ N )
Assertion	lcmineqlem9	|- ( ph -> ( x e. CC |-> ( ( 1 - x ) ^ ( N - M ) ) ) e. ( CC -cn-> CC ) )

Proof

Step	Hyp	Ref	Expression
1		lcmineqlem9.1	|- ( ph -> M e. NN )
2		lcmineqlem9.2	|- ( ph -> N e. NN )
3		lcmineqlem9.3	|- ( ph -> M <_ N )
4		nfv	|- F/ x ph
5		ax-1cn	|- 1 e. CC
6		eqid	|- ( x e. CC |-> ( 1 - x ) ) = ( x e. CC |-> ( 1 - x ) )
7	6	sub2cncf	|- ( 1 e. CC -> ( x e. CC |-> ( 1 - x ) ) e. ( CC -cn-> CC ) )
8	5 7	mp1i	|- ( ph -> ( x e. CC |-> ( 1 - x ) ) e. ( CC -cn-> CC ) )
9	1	nnzd	|- ( ph -> M e. ZZ )
10	2	nnzd	|- ( ph -> N e. ZZ )
11		znn0sub	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M <_ N <-> ( N - M ) e. NN0 ) )
12	9 10 11	syl2anc	|- ( ph -> ( M <_ N <-> ( N - M ) e. NN0 ) )
13	3 12	mpbid	|- ( ph -> ( N - M ) e. NN0 )
14		expcncf	|- ( ( N - M ) e. NN0 -> ( y e. CC |-> ( y ^ ( N - M ) ) ) e. ( CC -cn-> CC ) )
15	13 14	syl	|- ( ph -> ( y e. CC |-> ( y ^ ( N - M ) ) ) e. ( CC -cn-> CC ) )
16		ssidd	|- ( ph -> CC C_ CC )
17		oveq1	|- ( y = ( 1 - x ) -> ( y ^ ( N - M ) ) = ( ( 1 - x ) ^ ( N - M ) ) )
18	4 8 15 16 17	cncfcompt2	|- ( ph -> ( x e. CC |-> ( ( 1 - x ) ^ ( N - M ) ) ) e. ( CC -cn-> CC ) )