This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pfxccatin12lem4

Description: Lemma 4 for pfxccatin12 . (Contributed by Alexander van der Vekens, 30-Mar-2018) (Revised by Alexander van der Vekens, 23-May-2018)

Ref Expression
Assertion pfxccatin12lem4 ( ( 𝐿 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ¬ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) → 𝐾 ∈ ( ( 𝐿 − 𝑀 ) ..^ ( ( 𝐿 − 𝑀 ) + ( 𝑁 − 𝐿 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 nn0z ⊢ ( 𝐿 ∈ ℕ0 → 𝐿 ∈ ℤ )
2 nn0z ⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ∈ ℤ )
3 zsubcl ⊢ ( ( 𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝐿 − 𝑀 ) ∈ ℤ )
4 1 2 3 syl2an ⊢ ( ( 𝐿 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ( 𝐿 − 𝑀 ) ∈ ℤ )
5 4 3adant3 ⊢ ( ( 𝐿 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℤ ) → ( 𝐿 − 𝑀 ) ∈ ℤ )
6 elfzonelfzo ⊢ ( ( 𝐿 − 𝑀 ) ∈ ℤ → ( ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ¬ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) → 𝐾 ∈ ( ( 𝐿 − 𝑀 ) ..^ ( 𝑁 − 𝑀 ) ) ) )
7 6 imp ⊢ ( ( ( 𝐿 − 𝑀 ) ∈ ℤ ∧ ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ¬ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) ) → 𝐾 ∈ ( ( 𝐿 − 𝑀 ) ..^ ( 𝑁 − 𝑀 ) ) )
8 5 7 sylan ⊢ ( ( ( 𝐿 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ¬ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) ) → 𝐾 ∈ ( ( 𝐿 − 𝑀 ) ..^ ( 𝑁 − 𝑀 ) ) )
9 nn0cn ⊢ ( 𝐿 ∈ ℕ0 → 𝐿 ∈ ℂ )
10 nn0cn ⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ∈ ℂ )
11 zcn ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
12 npncan3 ⊢ ( ( 𝐿 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( ( 𝐿 − 𝑀 ) + ( 𝑁 − 𝐿 ) ) = ( 𝑁 − 𝑀 ) )
13 9 10 11 12 syl3an ⊢ ( ( 𝐿 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℤ ) → ( ( 𝐿 − 𝑀 ) + ( 𝑁 − 𝐿 ) ) = ( 𝑁 − 𝑀 ) )
14 13 oveq2d ⊢ ( ( 𝐿 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℤ ) → ( ( 𝐿 − 𝑀 ) ..^ ( ( 𝐿 − 𝑀 ) + ( 𝑁 − 𝐿 ) ) ) = ( ( 𝐿 − 𝑀 ) ..^ ( 𝑁 − 𝑀 ) ) )
15 14 eleq2d ⊢ ( ( 𝐿 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∈ ( ( 𝐿 − 𝑀 ) ..^ ( ( 𝐿 − 𝑀 ) + ( 𝑁 − 𝐿 ) ) ) ↔ 𝐾 ∈ ( ( 𝐿 − 𝑀 ) ..^ ( 𝑁 − 𝑀 ) ) ) )
16 15 adantr ⊢ ( ( ( 𝐿 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ¬ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) ) → ( 𝐾 ∈ ( ( 𝐿 − 𝑀 ) ..^ ( ( 𝐿 − 𝑀 ) + ( 𝑁 − 𝐿 ) ) ) ↔ 𝐾 ∈ ( ( 𝐿 − 𝑀 ) ..^ ( 𝑁 − 𝑀 ) ) ) )
17 8 16 mpbird ⊢ ( ( ( 𝐿 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ¬ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) ) → 𝐾 ∈ ( ( 𝐿 − 𝑀 ) ..^ ( ( 𝐿 − 𝑀 ) + ( 𝑁 − 𝐿 ) ) ) )
18 17 ex ⊢ ( ( 𝐿 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ¬ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) → 𝐾 ∈ ( ( 𝐿 − 𝑀 ) ..^ ( ( 𝐿 − 𝑀 ) + ( 𝑁 − 𝐿 ) ) ) ) )