Metamath Proof Explorer


Theorem knoppndvlem13

Description: Lemma for knoppndv . (Contributed by Asger C. Ipsen, 1-Jul-2021) (Revised by Asger C. Ipsen, 5-Jul-2021)

Ref Expression
Hypotheses knoppndvlem13.c ( 𝜑𝐶 ∈ ( - 1 (,) 1 ) )
knoppndvlem13.n ( 𝜑𝑁 ∈ ℕ )
knoppndvlem13.1 ( 𝜑 → 1 < ( 𝑁 · ( abs ‘ 𝐶 ) ) )
Assertion knoppndvlem13 ( 𝜑𝐶 ≠ 0 )

Proof

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 )