Theorem lcmineqlem9

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

	Ref	Expression
Hypotheses	lcmineqlem9.1	$$⊢\phi \to M\in \mathbb{N}$$
	lcmineqlem9.2	$$⊢\phi \to N\in \mathbb{N}$$
	lcmineqlem9.3	$$⊢\phi \to M\le N$$
Assertion	lcmineqlem9	$$⊢\phi \to \left(x\in ℂ⟼{\left(1-x\right)}^{N-M}\right):ℂ\underset{cn}{⟶}ℂ$$

Proof

Step	Hyp	Ref	Expression
1		lcmineqlem9.1	$$⊢\phi \to M\in \mathbb{N}$$
2		lcmineqlem9.2	$$⊢\phi \to N\in \mathbb{N}$$
3		lcmineqlem9.3	$$⊢\phi \to M\le N$$
4		nfv	$$⊢Ⅎx\phi$$
5		ax-1cn	$$⊢1\in ℂ$$
6		eqid	$$⊢\left(x\in ℂ⟼1-x\right)=\left(x\in ℂ⟼1-x\right)$$
7	6	sub2cncf	$$⊢1\in ℂ\to \left(x\in ℂ⟼1-x\right):ℂ\underset{cn}{⟶}ℂ$$
8	5 7	mp1i	$$⊢\phi \to \left(x\in ℂ⟼1-x\right):ℂ\underset{cn}{⟶}ℂ$$
9	1	nnzd	$$⊢\phi \to M\in \mathbb{Z}$$
10	2	nnzd	$$⊢\phi \to N\in \mathbb{Z}$$
11		znn0sub	$$⊢\left(M\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to \left(M\le N\leftrightarrow N-M\in {\mathbb{N}}_0\right)$$
12	9 10 11	syl2anc	$$⊢\phi \to \left(M\le N\leftrightarrow N-M\in {\mathbb{N}}_0\right)$$
13	3 12	mpbid	$$⊢\phi \to N-M\in {\mathbb{N}}_0$$
14		expcncf	$$⊢N-M\in {\mathbb{N}}_0\to \left(y\in ℂ⟼y^{N-M}\right):ℂ\underset{cn}{⟶}ℂ$$
15	13 14	syl	$$⊢\phi \to \left(y\in ℂ⟼y^{N-M}\right):ℂ\underset{cn}{⟶}ℂ$$
16		ssidd	$$⊢\phi \to ℂ\subseteq ℂ$$
17		oveq1	$$⊢y=1-x\to y^{N-M}={\left(1-x\right)}^{N-M}$$
18	4 8 15 16 17	cncfcompt2	$$⊢\phi \to \left(x\in ℂ⟼{\left(1-x\right)}^{N-M}\right):ℂ\underset{cn}{⟶}ℂ$$