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

Metamath Proof Explorer

Theorem pfxccatin12lem1

Description: Lemma 1 for pfxccatin12 . (Contributed by AV, 30-Mar-2018) (Revised by AV, 9-May-2020)

Ref Expression
Assertion pfxccatin12lem1 ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) → ( ( 𝐾 ∈ ( 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 elfz2nn0 ⊢ ( 𝑀 ∈ ( 0 ... 𝐿 ) ↔ ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝑀 ≤ 𝐿 ) )
10 nn0cn ⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ∈ ℂ )
11 nn0cn ⊢ ( 𝐿 ∈ ℕ0 → 𝐿 ∈ ℂ )
12 elfzelz ⊢ ( 𝑁 ∈ ( 𝐿 ... 𝑋 ) → 𝑁 ∈ ℤ )
13 zcn ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
14 subcl ⊢ ( ( 𝐿 ∈ ℂ ∧ 𝑀 ∈ ℂ ) → ( 𝐿 − 𝑀 ) ∈ ℂ )
15 14 ancoms ⊢ ( ( 𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ ) → ( 𝐿 − 𝑀 ) ∈ ℂ )
16 15 addridd ⊢ ( ( 𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ ) → ( ( 𝐿 − 𝑀 ) + 0 ) = ( 𝐿 − 𝑀 ) )
17 16 eqcomd ⊢ ( ( 𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ ) → ( 𝐿 − 𝑀 ) = ( ( 𝐿 − 𝑀 ) + 0 ) )
18 17 adantl ⊢ ( ( 𝑁 ∈ ℂ ∧ ( 𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ ) ) → ( 𝐿 − 𝑀 ) = ( ( 𝐿 − 𝑀 ) + 0 ) )
19 simprr ⊢ ( ( 𝑁 ∈ ℂ ∧ ( 𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ ) ) → 𝐿 ∈ ℂ )
20 simpl ⊢ ( ( 𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ ) → 𝑀 ∈ ℂ )
21 20 adantl ⊢ ( ( 𝑁 ∈ ℂ ∧ ( 𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ ) ) → 𝑀 ∈ ℂ )
22 simpl ⊢ ( ( 𝑁 ∈ ℂ ∧ ( 𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ ) ) → 𝑁 ∈ ℂ )
23 19 21 22 npncan3d ⊢ ( ( 𝑁 ∈ ℂ ∧ ( 𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ ) ) → ( ( 𝐿 − 𝑀 ) + ( 𝑁 − 𝐿 ) ) = ( 𝑁 − 𝑀 ) )
24 23 eqcomd ⊢ ( ( 𝑁 ∈ ℂ ∧ ( 𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ ) ) → ( 𝑁 − 𝑀 ) = ( ( 𝐿 − 𝑀 ) + ( 𝑁 − 𝐿 ) ) )
25 18 24 oveq12d ⊢ ( ( 𝑁 ∈ ℂ ∧ ( 𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ ) ) → ( ( 𝐿 − 𝑀 ) ..^ ( 𝑁 − 𝑀 ) ) = ( ( ( 𝐿 − 𝑀 ) + 0 ) ..^ ( ( 𝐿 − 𝑀 ) + ( 𝑁 − 𝐿 ) ) ) )
26 25 ex ⊢ ( 𝑁 ∈ ℂ → ( ( 𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ ) → ( ( 𝐿 − 𝑀 ) ..^ ( 𝑁 − 𝑀 ) ) = ( ( ( 𝐿 − 𝑀 ) + 0 ) ..^ ( ( 𝐿 − 𝑀 ) + ( 𝑁 − 𝐿 ) ) ) ) )
27 12 13 26 3syl ⊢ ( 𝑁 ∈ ( 𝐿 ... 𝑋 ) → ( ( 𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ ) → ( ( 𝐿 − 𝑀 ) ..^ ( 𝑁 − 𝑀 ) ) = ( ( ( 𝐿 − 𝑀 ) + 0 ) ..^ ( ( 𝐿 − 𝑀 ) + ( 𝑁 − 𝐿 ) ) ) ) )
28 27 com12 ⊢ ( ( 𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ ) → ( 𝑁 ∈ ( 𝐿 ... 𝑋 ) → ( ( 𝐿 − 𝑀 ) ..^ ( 𝑁 − 𝑀 ) ) = ( ( ( 𝐿 − 𝑀 ) + 0 ) ..^ ( ( 𝐿 − 𝑀 ) + ( 𝑁 − 𝐿 ) ) ) ) )
29 10 11 28 syl2an ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) → ( 𝑁 ∈ ( 𝐿 ... 𝑋 ) → ( ( 𝐿 − 𝑀 ) ..^ ( 𝑁 − 𝑀 ) ) = ( ( ( 𝐿 − 𝑀 ) + 0 ) ..^ ( ( 𝐿 − 𝑀 ) + ( 𝑁 − 𝐿 ) ) ) ) )
30 29 3adant3 ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝑀 ≤ 𝐿 ) → ( 𝑁 ∈ ( 𝐿 ... 𝑋 ) → ( ( 𝐿 − 𝑀 ) ..^ ( 𝑁 − 𝑀 ) ) = ( ( ( 𝐿 − 𝑀 ) + 0 ) ..^ ( ( 𝐿 − 𝑀 ) + ( 𝑁 − 𝐿 ) ) ) ) )
31 9 30 sylbi ⊢ ( 𝑀 ∈ ( 0 ... 𝐿 ) → ( 𝑁 ∈ ( 𝐿 ... 𝑋 ) → ( ( 𝐿 − 𝑀 ) ..^ ( 𝑁 − 𝑀 ) ) = ( ( ( 𝐿 − 𝑀 ) + 0 ) ..^ ( ( 𝐿 − 𝑀 ) + ( 𝑁 − 𝐿 ) ) ) ) )
32 31 imp ⊢ ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) → ( ( 𝐿 − 𝑀 ) ..^ ( 𝑁 − 𝑀 ) ) = ( ( ( 𝐿 − 𝑀 ) + 0 ) ..^ ( ( 𝐿 − 𝑀 ) + ( 𝑁 − 𝐿 ) ) ) )
33 32 eleq2d ⊢ ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) → ( 𝐾 ∈ ( ( 𝐿 − 𝑀 ) ..^ ( 𝑁 − 𝑀 ) ) ↔ 𝐾 ∈ ( ( ( 𝐿 − 𝑀 ) + 0 ) ..^ ( ( 𝐿 − 𝑀 ) + ( 𝑁 − 𝐿 ) ) ) ) )
34 33 biimpa ⊢ ( ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) ∧ 𝐾 ∈ ( ( 𝐿 − 𝑀 ) ..^ ( 𝑁 − 𝑀 ) ) ) → 𝐾 ∈ ( ( ( 𝐿 − 𝑀 ) + 0 ) ..^ ( ( 𝐿 − 𝑀 ) + ( 𝑁 − 𝐿 ) ) ) )
35 0zd ⊢ ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) → 0 ∈ ℤ )
36 elfz2 ⊢ ( 𝑁 ∈ ( 𝐿 ... 𝑋 ) ↔ ( ( 𝐿 ∈ ℤ ∧ 𝑋 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐿 ≤ 𝑁 ∧ 𝑁 ≤ 𝑋 ) ) )
37 zsubcl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝑁 − 𝐿 ) ∈ ℤ )
38 37 ancoms ⊢ ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 − 𝐿 ) ∈ ℤ )
39 38 3adant2 ⊢ ( ( 𝐿 ∈ ℤ ∧ 𝑋 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 − 𝐿 ) ∈ ℤ )
40 39 adantr ⊢ ( ( ( 𝐿 ∈ ℤ ∧ 𝑋 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐿 ≤ 𝑁 ∧ 𝑁 ≤ 𝑋 ) ) → ( 𝑁 − 𝐿 ) ∈ ℤ )
41 36 40 sylbi ⊢ ( 𝑁 ∈ ( 𝐿 ... 𝑋 ) → ( 𝑁 − 𝐿 ) ∈ ℤ )
42 41 adantl ⊢ ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) → ( 𝑁 − 𝐿 ) ∈ ℤ )
43 6 35 42 3jca ⊢ ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) → ( ( 𝐿 − 𝑀 ) ∈ ℤ ∧ 0 ∈ ℤ ∧ ( 𝑁 − 𝐿 ) ∈ ℤ ) )
44 43 adantr ⊢ ( ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) ∧ 𝐾 ∈ ( ( 𝐿 − 𝑀 ) ..^ ( 𝑁 − 𝑀 ) ) ) → ( ( 𝐿 − 𝑀 ) ∈ ℤ ∧ 0 ∈ ℤ ∧ ( 𝑁 − 𝐿 ) ∈ ℤ ) )
45 fzosubel2 ⊢ ( ( 𝐾 ∈ ( ( ( 𝐿 − 𝑀 ) + 0 ) ..^ ( ( 𝐿 − 𝑀 ) + ( 𝑁 − 𝐿 ) ) ) ∧ ( ( 𝐿 − 𝑀 ) ∈ ℤ ∧ 0 ∈ ℤ ∧ ( 𝑁 − 𝐿 ) ∈ ℤ ) ) → ( 𝐾 − ( 𝐿 − 𝑀 ) ) ∈ ( 0 ..^ ( 𝑁 − 𝐿 ) ) )
46 34 44 45 syl2anc ⊢ ( ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) ∧ 𝐾 ∈ ( ( 𝐿 − 𝑀 ) ..^ ( 𝑁 − 𝑀 ) ) ) → ( 𝐾 − ( 𝐿 − 𝑀 ) ) ∈ ( 0 ..^ ( 𝑁 − 𝐿 ) ) )
47 46 ex ⊢ ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) → ( 𝐾 ∈ ( ( 𝐿 − 𝑀 ) ..^ ( 𝑁 − 𝑀 ) ) → ( 𝐾 − ( 𝐿 − 𝑀 ) ) ∈ ( 0 ..^ ( 𝑁 − 𝐿 ) ) ) )
48 8 47 syld ⊢ ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) → ( ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ¬ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) → ( 𝐾 − ( 𝐿 − 𝑀 ) ) ∈ ( 0 ..^ ( 𝑁 − 𝐿 ) ) ) )