Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for metakunt
Least common multiple inequality theorem
lcmineqlem9
Next ⟩
lcmineqlem10
Metamath Proof Explorer
Ascii
Unicode
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
ℂ