Step |
Hyp |
Ref |
Expression |
1 |
|
knoppndvlem13.c |
⊢ ( 𝜑 → 𝐶 ∈ ( - 1 (,) 1 ) ) |
2 |
|
knoppndvlem13.n |
⊢ ( 𝜑 → 𝑁 ∈ ℕ ) |
3 |
|
knoppndvlem13.1 |
⊢ ( 𝜑 → 1 < ( 𝑁 · ( abs ‘ 𝐶 ) ) ) |
4 |
3
|
adantr |
⊢ ( ( 𝜑 ∧ 𝐶 = 0 ) → 1 < ( 𝑁 · ( abs ‘ 𝐶 ) ) ) |
5 |
|
0lt1 |
⊢ 0 < 1 |
6 |
|
0re |
⊢ 0 ∈ ℝ |
7 |
|
1re |
⊢ 1 ∈ ℝ |
8 |
6 7
|
ltnsymi |
⊢ ( 0 < 1 → ¬ 1 < 0 ) |
9 |
5 8
|
ax-mp |
⊢ ¬ 1 < 0 |
10 |
9
|
a1i |
⊢ ( ( 𝜑 ∧ 𝐶 = 0 ) → ¬ 1 < 0 ) |
11 |
|
id |
⊢ ( 𝐶 = 0 → 𝐶 = 0 ) |
12 |
11
|
abs00bd |
⊢ ( 𝐶 = 0 → ( abs ‘ 𝐶 ) = 0 ) |
13 |
12
|
oveq2d |
⊢ ( 𝐶 = 0 → ( 𝑁 · ( abs ‘ 𝐶 ) ) = ( 𝑁 · 0 ) ) |
14 |
13
|
adantl |
⊢ ( ( 𝜑 ∧ 𝐶 = 0 ) → ( 𝑁 · ( abs ‘ 𝐶 ) ) = ( 𝑁 · 0 ) ) |
15 |
|
nncn |
⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ ) |
16 |
2 15
|
syl |
⊢ ( 𝜑 → 𝑁 ∈ ℂ ) |
17 |
16
|
adantr |
⊢ ( ( 𝜑 ∧ 𝐶 = 0 ) → 𝑁 ∈ ℂ ) |
18 |
17
|
mul01d |
⊢ ( ( 𝜑 ∧ 𝐶 = 0 ) → ( 𝑁 · 0 ) = 0 ) |
19 |
14 18
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝐶 = 0 ) → ( 𝑁 · ( abs ‘ 𝐶 ) ) = 0 ) |
20 |
19
|
eqcomd |
⊢ ( ( 𝜑 ∧ 𝐶 = 0 ) → 0 = ( 𝑁 · ( abs ‘ 𝐶 ) ) ) |
21 |
20
|
breq2d |
⊢ ( ( 𝜑 ∧ 𝐶 = 0 ) → ( 1 < 0 ↔ 1 < ( 𝑁 · ( abs ‘ 𝐶 ) ) ) ) |
22 |
10 21
|
mtbid |
⊢ ( ( 𝜑 ∧ 𝐶 = 0 ) → ¬ 1 < ( 𝑁 · ( abs ‘ 𝐶 ) ) ) |
23 |
4 22
|
pm2.65da |
⊢ ( 𝜑 → ¬ 𝐶 = 0 ) |
24 |
23
|
neqned |
⊢ ( 𝜑 → 𝐶 ≠ 0 ) |