Theorem lcmineqlem9

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

	Ref	Expression
Hypotheses	lcmineqlem9.1	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
	lcmineqlem9.2	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	lcmineqlem9.3	⊢ ( 𝜑 → 𝑀 ≤ 𝑁 )
Assertion	lcmineqlem9	⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) ∈ ( ℂ –cn→ ℂ ) )

Proof

Step	Hyp	Ref	Expression
1		lcmineqlem9.1	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2		lcmineqlem9.2	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
3		lcmineqlem9.3	⊢ ( 𝜑 → 𝑀 ≤ 𝑁 )
4		nfv	⊢ Ⅎ 𝑥 𝜑
5		ax-1cn	⊢ 1 ∈ ℂ
6		eqid	⊢ ( 𝑥 ∈ ℂ ↦ ( 1 − 𝑥 ) ) = ( 𝑥 ∈ ℂ ↦ ( 1 − 𝑥 ) )
7	6	sub2cncf	⊢ ( 1 ∈ ℂ → ( 𝑥 ∈ ℂ ↦ ( 1 − 𝑥 ) ) ∈ ( ℂ –cn→ ℂ ) )
8	5 7	mp1i	⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ ( 1 − 𝑥 ) ) ∈ ( ℂ –cn→ ℂ ) )
9	1	nnzd	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
10	2	nnzd	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
11		znn0sub	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ≤ 𝑁 ↔ ( 𝑁 − 𝑀 ) ∈ ℕ0 ) )
12	9 10 11	syl2anc	⊢ ( 𝜑 → ( 𝑀 ≤ 𝑁 ↔ ( 𝑁 − 𝑀 ) ∈ ℕ0 ) )
13	3 12	mpbid	⊢ ( 𝜑 → ( 𝑁 − 𝑀 ) ∈ ℕ0 )
14		expcncf	⊢ ( ( 𝑁 − 𝑀 ) ∈ ℕ0 → ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ ( 𝑁 − 𝑀 ) ) ) ∈ ( ℂ –cn→ ℂ ) )
15	13 14	syl	⊢ ( 𝜑 → ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ ( 𝑁 − 𝑀 ) ) ) ∈ ( ℂ –cn→ ℂ ) )
16		ssidd	⊢ ( 𝜑 → ℂ ⊆ ℂ )
17		oveq1	⊢ ( 𝑦 = ( 1 − 𝑥 ) → ( 𝑦 ↑ ( 𝑁 − 𝑀 ) ) = ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) )
18	4 8 15 16 17	cncfcompt2	⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) ∈ ( ℂ –cn→ ℂ ) )