Metamath Proof Explorer


Theorem lcmineqlem9

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

Ref Expression
Hypotheses lcmineqlem9.1 φ M
lcmineqlem9.2 φ N
lcmineqlem9.3 φ M N
Assertion lcmineqlem9 φ x 1 x N M : cn

Proof

Step Hyp Ref Expression
1 lcmineqlem9.1 φ M
2 lcmineqlem9.2 φ N
3 lcmineqlem9.3 φ M N
4 nfv x φ
5 ax-1cn 1
6 eqid x 1 x = x 1 x
7 6 sub2cncf 1 x 1 x : cn
8 5 7 mp1i φ x 1 x : cn
9 1 nnzd φ M
10 2 nnzd φ N
11 znn0sub M N M N N M 0
12 9 10 11 syl2anc φ M N N M 0
13 3 12 mpbid φ N M 0
14 expcncf N M 0 y y N M : cn
15 13 14 syl φ y y N M : cn
16 ssidd φ
17 oveq1 y = 1 x y N M = 1 x N M
18 4 8 15 16 17 cncfcompt2 φ x 1 x N M : cn