Metamath Proof Explorer

Theorem swrdnd2

Description: Value of the subword extractor outside its intended domain. (Contributed by Alexander van der Vekens, 24-May-2018)

Ref Expression
Assertion swrdnd2 ⊢ W ∈ Word V ∧ A ∈ ℤ ∧ B ∈ ℤ → B ≤ A ∨ W ≤ A ∨ B ≤ 0 → W substr A B = ∅

Proof

Step Hyp Ref Expression
1 3orass ⊢ B ≤ A ∨ W ≤ A ∨ B ≤ 0 ↔ B ≤ A ∨ W ≤ A ∨ B ≤ 0
2 pm2.24 ⊢ B ≤ A → ¬ B ≤ A → W ∈ Word V ∧ A ∈ ℤ ∧ B ∈ ℤ → W substr A B = ∅
3 swrdval ⊢ W ∈ Word V ∧ A ∈ ℤ ∧ B ∈ ℤ → W substr A B = if A ..^ B ⊆ dom ⁡ W x ∈ 0 ..^ B − A ⟼ W ⁡ x + A ∅
4 3 ad2antrr ⊢ W ∈ Word V ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ W ≤ A ∨ B ≤ 0 ∧ ¬ B ≤ A → W substr A B = if A ..^ B ⊆ dom ⁡ W x ∈ 0 ..^ B − A ⟼ W ⁡ x + A ∅
5 wrddm ⊢ W ∈ Word V → dom ⁡ W = 0 ..^ W
6 lencl ⊢ W ∈ Word V → W ∈ ℕ 0
7 3anass ⊢ W ∈ ℕ 0 ∧ A ∈ ℤ ∧ B ∈ ℤ ↔ W ∈ ℕ 0 ∧ A ∈ ℤ ∧ B ∈ ℤ
8 ssfzoulel ⊢ W ∈ ℕ 0 ∧ A ∈ ℤ ∧ B ∈ ℤ → W ≤ A ∨ B ≤ 0 → A ..^ B ⊆ 0 ..^ W → B ≤ A
9 8 imp ⊢ W ∈ ℕ 0 ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ W ≤ A ∨ B ≤ 0 → A ..^ B ⊆ 0 ..^ W → B ≤ A
10 7 9 sylanbr ⊢ W ∈ ℕ 0 ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ W ≤ A ∨ B ≤ 0 → A ..^ B ⊆ 0 ..^ W → B ≤ A
11 10 con3dimp ⊢ W ∈ ℕ 0 ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ W ≤ A ∨ B ≤ 0 ∧ ¬ B ≤ A → ¬ A ..^ B ⊆ 0 ..^ W
12 sseq2 ⊢ dom ⁡ W = 0 ..^ W → A ..^ B ⊆ dom ⁡ W ↔ A ..^ B ⊆ 0 ..^ W
13 12 notbid ⊢ dom ⁡ W = 0 ..^ W → ¬ A ..^ B ⊆ dom ⁡ W ↔ ¬ A ..^ B ⊆ 0 ..^ W
14 11 13 imbitrrid ⊢ dom ⁡ W = 0 ..^ W → W ∈ ℕ 0 ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ W ≤ A ∨ B ≤ 0 ∧ ¬ B ≤ A → ¬ A ..^ B ⊆ dom ⁡ W
15 14 exp5j ⊢ dom ⁡ W = 0 ..^ W → W ∈ ℕ 0 → A ∈ ℤ ∧ B ∈ ℤ → W ≤ A ∨ B ≤ 0 → ¬ B ≤ A → ¬ A ..^ B ⊆ dom ⁡ W
16 5 6 15 sylc ⊢ W ∈ Word V → A ∈ ℤ ∧ B ∈ ℤ → W ≤ A ∨ B ≤ 0 → ¬ B ≤ A → ¬ A ..^ B ⊆ dom ⁡ W
17 16 3impib ⊢ W ∈ Word V ∧ A ∈ ℤ ∧ B ∈ ℤ → W ≤ A ∨ B ≤ 0 → ¬ B ≤ A → ¬ A ..^ B ⊆ dom ⁡ W
18 17 imp31 ⊢ W ∈ Word V ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ W ≤ A ∨ B ≤ 0 ∧ ¬ B ≤ A → ¬ A ..^ B ⊆ dom ⁡ W
19 18 iffalsed ⊢ W ∈ Word V ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ W ≤ A ∨ B ≤ 0 ∧ ¬ B ≤ A → if A ..^ B ⊆ dom ⁡ W x ∈ 0 ..^ B − A ⟼ W ⁡ x + A ∅ = ∅
20 4 19 eqtrd ⊢ W ∈ Word V ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ W ≤ A ∨ B ≤ 0 ∧ ¬ B ≤ A → W substr A B = ∅
21 20 ex ⊢ W ∈ Word V ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ W ≤ A ∨ B ≤ 0 → ¬ B ≤ A → W substr A B = ∅
22 21 expcom ⊢ W ≤ A ∨ B ≤ 0 → W ∈ Word V ∧ A ∈ ℤ ∧ B ∈ ℤ → ¬ B ≤ A → W substr A B = ∅
23 22 com23 ⊢ W ≤ A ∨ B ≤ 0 → ¬ B ≤ A → W ∈ Word V ∧ A ∈ ℤ ∧ B ∈ ℤ → W substr A B = ∅
24 2 23 jaoi ⊢ B ≤ A ∨ W ≤ A ∨ B ≤ 0 → ¬ B ≤ A → W ∈ Word V ∧ A ∈ ℤ ∧ B ∈ ℤ → W substr A B = ∅
25 swrdlend ⊢ W ∈ Word V ∧ A ∈ ℤ ∧ B ∈ ℤ → B ≤ A → W substr A B = ∅
26 25 com12 ⊢ B ≤ A → W ∈ Word V ∧ A ∈ ℤ ∧ B ∈ ℤ → W substr A B = ∅
27 24 26 pm2.61d2 ⊢ B ≤ A ∨ W ≤ A ∨ B ≤ 0 → W ∈ Word V ∧ A ∈ ℤ ∧ B ∈ ℤ → W substr A B = ∅
28 1 27 sylbi ⊢ B ≤ A ∨ W ≤ A ∨ B ≤ 0 → W ∈ Word V ∧ A ∈ ℤ ∧ B ∈ ℤ → W substr A B = ∅
29 28 com12 ⊢ W ∈ Word V ∧ A ∈ ℤ ∧ B ∈ ℤ → B ≤ A ∨ W ≤ A ∨ B ≤ 0 → W substr A B = ∅