Metamath Proof Explorer


Theorem etransclem9

Description: If K divides N but K does not divide M then M + N cannot be zero. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses etransclem9.k ( 𝜑𝐾 ∈ ℤ )
etransclem9.kn0 ( 𝜑𝐾 ≠ 0 )
etransclem9.m ( 𝜑𝑀 ∈ ℤ )
etransclem9.n ( 𝜑𝑁 ∈ ℤ )
etransclem9.km ( 𝜑 → ¬ 𝐾𝑀 )
etransclem9.kn ( 𝜑𝐾𝑁 )
Assertion etransclem9 ( 𝜑 → ( 𝑀 + 𝑁 ) ≠ 0 )

Proof

Step Hyp Ref Expression
1 etransclem9.k ( 𝜑𝐾 ∈ ℤ )
2 etransclem9.kn0 ( 𝜑𝐾 ≠ 0 )
3 etransclem9.m ( 𝜑𝑀 ∈ ℤ )
4 etransclem9.n ( 𝜑𝑁 ∈ ℤ )
5 etransclem9.km ( 𝜑 → ¬ 𝐾𝑀 )
6 etransclem9.kn ( 𝜑𝐾𝑁 )
7 dvdsval2 ( ( 𝐾 ∈ ℤ ∧ 𝐾 ≠ 0 ∧ 𝑀 ∈ ℤ ) → ( 𝐾𝑀 ↔ ( 𝑀 / 𝐾 ) ∈ ℤ ) )
8 1 2 3 7 syl3anc ( 𝜑 → ( 𝐾𝑀 ↔ ( 𝑀 / 𝐾 ) ∈ ℤ ) )
9 5 8 mtbid ( 𝜑 → ¬ ( 𝑀 / 𝐾 ) ∈ ℤ )
10 df-neg - 𝑁 = ( 0 − 𝑁 )
11 10 a1i ( ( 𝜑 ∧ ( 𝑀 + 𝑁 ) = 0 ) → - 𝑁 = ( 0 − 𝑁 ) )
12 oveq1 ( ( 𝑀 + 𝑁 ) = 0 → ( ( 𝑀 + 𝑁 ) − 𝑁 ) = ( 0 − 𝑁 ) )
13 12 eqcomd ( ( 𝑀 + 𝑁 ) = 0 → ( 0 − 𝑁 ) = ( ( 𝑀 + 𝑁 ) − 𝑁 ) )
14 13 adantl ( ( 𝜑 ∧ ( 𝑀 + 𝑁 ) = 0 ) → ( 0 − 𝑁 ) = ( ( 𝑀 + 𝑁 ) − 𝑁 ) )
15 3 zcnd ( 𝜑𝑀 ∈ ℂ )
16 4 zcnd ( 𝜑𝑁 ∈ ℂ )
17 15 16 pncand ( 𝜑 → ( ( 𝑀 + 𝑁 ) − 𝑁 ) = 𝑀 )
18 17 adantr ( ( 𝜑 ∧ ( 𝑀 + 𝑁 ) = 0 ) → ( ( 𝑀 + 𝑁 ) − 𝑁 ) = 𝑀 )
19 11 14 18 3eqtrrd ( ( 𝜑 ∧ ( 𝑀 + 𝑁 ) = 0 ) → 𝑀 = - 𝑁 )
20 19 oveq1d ( ( 𝜑 ∧ ( 𝑀 + 𝑁 ) = 0 ) → ( 𝑀 / 𝐾 ) = ( - 𝑁 / 𝐾 ) )
21 dvdsnegb ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾𝑁𝐾 ∥ - 𝑁 ) )
22 1 4 21 syl2anc ( 𝜑 → ( 𝐾𝑁𝐾 ∥ - 𝑁 ) )
23 6 22 mpbid ( 𝜑𝐾 ∥ - 𝑁 )
24 4 znegcld ( 𝜑 → - 𝑁 ∈ ℤ )
25 dvdsval2 ( ( 𝐾 ∈ ℤ ∧ 𝐾 ≠ 0 ∧ - 𝑁 ∈ ℤ ) → ( 𝐾 ∥ - 𝑁 ↔ ( - 𝑁 / 𝐾 ) ∈ ℤ ) )
26 1 2 24 25 syl3anc ( 𝜑 → ( 𝐾 ∥ - 𝑁 ↔ ( - 𝑁 / 𝐾 ) ∈ ℤ ) )
27 23 26 mpbid ( 𝜑 → ( - 𝑁 / 𝐾 ) ∈ ℤ )
28 27 adantr ( ( 𝜑 ∧ ( 𝑀 + 𝑁 ) = 0 ) → ( - 𝑁 / 𝐾 ) ∈ ℤ )
29 20 28 eqeltrd ( ( 𝜑 ∧ ( 𝑀 + 𝑁 ) = 0 ) → ( 𝑀 / 𝐾 ) ∈ ℤ )
30 9 29 mtand ( 𝜑 → ¬ ( 𝑀 + 𝑁 ) = 0 )
31 30 neqned ( 𝜑 → ( 𝑀 + 𝑁 ) ≠ 0 )