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

Metamath Proof Explorer

Theorem pfxccatin12lem2a

Description: Lemma for pfxccatin12lem2 . (Contributed by AV, 30-Mar-2018) (Revised by AV, 27-May-2018)

Ref Expression
Assertion pfxccatin12lem2a ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) → ( ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ¬ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) → ( 𝐾 + 𝑀 ) ∈ ( 𝐿 ..^ 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 elfz2 ⊢ ( 𝑀 ∈ ( 0 ... 𝐿 ) ↔ ( ( 0 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ ( 0 ≤ 𝑀 ∧ 𝑀 ≤ 𝐿 ) ) )
2 zsubcl ⊢ ( ( 𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝐿 − 𝑀 ) ∈ ℤ )
3 2 3adant1 ⊢ ( ( 0 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝐿 − 𝑀 ) ∈ ℤ )
4 3 adantr ⊢ ( ( ( 0 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ ( 0 ≤ 𝑀 ∧ 𝑀 ≤ 𝐿 ) ) → ( 𝐿 − 𝑀 ) ∈ ℤ )
5 1 4 sylbi ⊢ ( 𝑀 ∈ ( 0 ... 𝐿 ) → ( 𝐿 − 𝑀 ) ∈ ℤ )
6 5 adantr ⊢ ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) → ( 𝐿 − 𝑀 ) ∈ ℤ )
7 elfzonelfzo ⊢ ( ( 𝐿 − 𝑀 ) ∈ ℤ → ( ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ¬ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) → 𝐾 ∈ ( ( 𝐿 − 𝑀 ) ..^ ( 𝑁 − 𝑀 ) ) ) )
8 6 7 syl ⊢ ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) → ( ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ¬ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) → 𝐾 ∈ ( ( 𝐿 − 𝑀 ) ..^ ( 𝑁 − 𝑀 ) ) ) )
9 elfzoelz ⊢ ( 𝐾 ∈ ( ( 𝐿 − 𝑀 ) ..^ ( 𝑁 − 𝑀 ) ) → 𝐾 ∈ ℤ )
10 elfzelz ⊢ ( 𝑁 ∈ ( 𝐿 ... 𝑋 ) → 𝑁 ∈ ℤ )
11 simpl ⊢ ( ( 𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → 𝐿 ∈ ℤ )
12 simpl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → 𝑁 ∈ ℤ )
13 11 12 anim12i ⊢ ( ( ( 𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
14 simpr ⊢ ( ( 𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → 𝑀 ∈ ℤ )
15 simpr ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → 𝐾 ∈ ℤ )
16 14 15 anim12ci ⊢ ( ( ( 𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) )
17 13 16 jca ⊢ ( ( ( 𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) )
18 17 exp32 ⊢ ( ( 𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑁 ∈ ℤ → ( 𝐾 ∈ ℤ → ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ) ) )
19 10 18 syl5 ⊢ ( ( 𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑁 ∈ ( 𝐿 ... 𝑋 ) → ( 𝐾 ∈ ℤ → ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ) ) )
20 19 3adant1 ⊢ ( ( 0 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑁 ∈ ( 𝐿 ... 𝑋 ) → ( 𝐾 ∈ ℤ → ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ) ) )
21 20 adantr ⊢ ( ( ( 0 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ ( 0 ≤ 𝑀 ∧ 𝑀 ≤ 𝐿 ) ) → ( 𝑁 ∈ ( 𝐿 ... 𝑋 ) → ( 𝐾 ∈ ℤ → ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ) ) )
22 1 21 sylbi ⊢ ( 𝑀 ∈ ( 0 ... 𝐿 ) → ( 𝑁 ∈ ( 𝐿 ... 𝑋 ) → ( 𝐾 ∈ ℤ → ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ) ) )
23 22 imp ⊢ ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) → ( 𝐾 ∈ ℤ → ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ) )
24 23 impcom ⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) ) → ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) )
25 elfzomelpfzo ⊢ ( ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( 𝐾 ∈ ( ( 𝐿 − 𝑀 ) ..^ ( 𝑁 − 𝑀 ) ) ↔ ( 𝐾 + 𝑀 ) ∈ ( 𝐿 ..^ 𝑁 ) ) )
26 24 25 syl ⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) ) → ( 𝐾 ∈ ( ( 𝐿 − 𝑀 ) ..^ ( 𝑁 − 𝑀 ) ) ↔ ( 𝐾 + 𝑀 ) ∈ ( 𝐿 ..^ 𝑁 ) ) )
27 elfz2 ⊢ ( 𝑁 ∈ ( 𝐿 ... 𝑋 ) ↔ ( ( 𝐿 ∈ ℤ ∧ 𝑋 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐿 ≤ 𝑁 ∧ 𝑁 ≤ 𝑋 ) ) )
28 simpl3 ⊢ ( ( ( 𝐿 ∈ ℤ ∧ 𝑋 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐿 ≤ 𝑁 ∧ 𝑁 ≤ 𝑋 ) ) → 𝑁 ∈ ℤ )
29 simpl2 ⊢ ( ( ( 𝐿 ∈ ℤ ∧ 𝑋 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐿 ≤ 𝑁 ∧ 𝑁 ≤ 𝑋 ) ) → 𝑋 ∈ ℤ )
30 simpr ⊢ ( ( 𝐿 ≤ 𝑁 ∧ 𝑁 ≤ 𝑋 ) → 𝑁 ≤ 𝑋 )
31 30 adantl ⊢ ( ( ( 𝐿 ∈ ℤ ∧ 𝑋 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐿 ≤ 𝑁 ∧ 𝑁 ≤ 𝑋 ) ) → 𝑁 ≤ 𝑋 )
32 28 29 31 3jca ⊢ ( ( ( 𝐿 ∈ ℤ ∧ 𝑋 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐿 ≤ 𝑁 ∧ 𝑁 ≤ 𝑋 ) ) → ( 𝑁 ∈ ℤ ∧ 𝑋 ∈ ℤ ∧ 𝑁 ≤ 𝑋 ) )
33 27 32 sylbi ⊢ ( 𝑁 ∈ ( 𝐿 ... 𝑋 ) → ( 𝑁 ∈ ℤ ∧ 𝑋 ∈ ℤ ∧ 𝑁 ≤ 𝑋 ) )
34 33 adantl ⊢ ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) → ( 𝑁 ∈ ℤ ∧ 𝑋 ∈ ℤ ∧ 𝑁 ≤ 𝑋 ) )
35 34 adantl ⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) ) → ( 𝑁 ∈ ℤ ∧ 𝑋 ∈ ℤ ∧ 𝑁 ≤ 𝑋 ) )
36 eluz2 ⊢ ( 𝑋 ∈ ( ℤ≥ ‘ 𝑁 ) ↔ ( 𝑁 ∈ ℤ ∧ 𝑋 ∈ ℤ ∧ 𝑁 ≤ 𝑋 ) )
37 35 36 sylibr ⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) ) → 𝑋 ∈ ( ℤ≥ ‘ 𝑁 ) )
38 fzoss2 ⊢ ( 𝑋 ∈ ( ℤ≥ ‘ 𝑁 ) → ( 𝐿 ..^ 𝑁 ) ⊆ ( 𝐿 ..^ 𝑋 ) )
39 37 38 syl ⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) ) → ( 𝐿 ..^ 𝑁 ) ⊆ ( 𝐿 ..^ 𝑋 ) )
40 39 sseld ⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) ) → ( ( 𝐾 + 𝑀 ) ∈ ( 𝐿 ..^ 𝑁 ) → ( 𝐾 + 𝑀 ) ∈ ( 𝐿 ..^ 𝑋 ) ) )
41 26 40 sylbid ⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) ) → ( 𝐾 ∈ ( ( 𝐿 − 𝑀 ) ..^ ( 𝑁 − 𝑀 ) ) → ( 𝐾 + 𝑀 ) ∈ ( 𝐿 ..^ 𝑋 ) ) )
42 41 ex ⊢ ( 𝐾 ∈ ℤ → ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) → ( 𝐾 ∈ ( ( 𝐿 − 𝑀 ) ..^ ( 𝑁 − 𝑀 ) ) → ( 𝐾 + 𝑀 ) ∈ ( 𝐿 ..^ 𝑋 ) ) ) )
43 42 com23 ⊢ ( 𝐾 ∈ ℤ → ( 𝐾 ∈ ( ( 𝐿 − 𝑀 ) ..^ ( 𝑁 − 𝑀 ) ) → ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) → ( 𝐾 + 𝑀 ) ∈ ( 𝐿 ..^ 𝑋 ) ) ) )
44 9 43 mpcom ⊢ ( 𝐾 ∈ ( ( 𝐿 − 𝑀 ) ..^ ( 𝑁 − 𝑀 ) ) → ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) → ( 𝐾 + 𝑀 ) ∈ ( 𝐿 ..^ 𝑋 ) ) )
45 44 com12 ⊢ ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) → ( 𝐾 ∈ ( ( 𝐿 − 𝑀 ) ..^ ( 𝑁 − 𝑀 ) ) → ( 𝐾 + 𝑀 ) ∈ ( 𝐿 ..^ 𝑋 ) ) )
46 8 45 syld ⊢ ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) → ( ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ¬ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) → ( 𝐾 + 𝑀 ) ∈ ( 𝐿 ..^ 𝑋 ) ) )