| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | repsw 14814 | . . . . . 6
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → (𝑆 repeatS 𝐿) ∈ Word 𝑉) | 
| 2 |  | nn0z 12640 | . . . . . . 7
⊢ (𝑀 ∈ ℕ0
→ 𝑀 ∈
ℤ) | 
| 3 |  | nn0z 12640 | . . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) | 
| 4 | 2, 3 | anim12i 613 | . . . . . 6
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) | 
| 5 | 1, 4 | anim12i 613 | . . . . 5
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0)) → ((𝑆 repeatS 𝐿) ∈ Word 𝑉 ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) | 
| 6 |  | 3anass 1094 | . . . . 5
⊢ (((𝑆 repeatS 𝐿) ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ↔ ((𝑆 repeatS 𝐿) ∈ Word 𝑉 ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) | 
| 7 | 5, 6 | sylibr 234 | . . . 4
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0)) → ((𝑆 repeatS 𝐿) ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) | 
| 8 | 7 | 3adant3 1132 | . . 3
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) → ((𝑆 repeatS 𝐿) ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) | 
| 9 |  | swrdval 14682 | . . 3
⊢ (((𝑆 repeatS 𝐿) ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑆 repeatS 𝐿) substr 〈𝑀, 𝑁〉) = if((𝑀..^𝑁) ⊆ dom (𝑆 repeatS 𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅)) | 
| 10 | 8, 9 | syl 17 | . 2
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) → ((𝑆 repeatS 𝐿) substr 〈𝑀, 𝑁〉) = if((𝑀..^𝑁) ⊆ dom (𝑆 repeatS 𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅)) | 
| 11 |  | repsf 14812 | . . . . . 6
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → (𝑆 repeatS 𝐿):(0..^𝐿)⟶𝑉) | 
| 12 | 11 | 3ad2ant1 1133 | . . . . 5
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) → (𝑆 repeatS 𝐿):(0..^𝐿)⟶𝑉) | 
| 13 | 12 | fdmd 6745 | . . . 4
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) → dom (𝑆 repeatS 𝐿) = (0..^𝐿)) | 
| 14 | 13 | sseq2d 4015 | . . 3
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) → ((𝑀..^𝑁) ⊆ dom (𝑆 repeatS 𝐿) ↔ (𝑀..^𝑁) ⊆ (0..^𝐿))) | 
| 15 | 14 | ifbid 4548 | . 2
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) → if((𝑀..^𝑁) ⊆ dom (𝑆 repeatS 𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅)) | 
| 16 |  | fzon 13721 | . . . . . . . . . . 11
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ≤ 𝑀 ↔ (𝑀..^𝑁) = ∅)) | 
| 17 | 4, 16 | syl 17 | . . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑁 ≤ 𝑀 ↔ (𝑀..^𝑁) = ∅)) | 
| 18 | 17 | adantl 481 | . . . . . . . . 9
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0)) → (𝑁 ≤ 𝑀 ↔ (𝑀..^𝑁) = ∅)) | 
| 19 | 18 | biimpac 478 | . . . . . . . 8
⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0))) → (𝑀..^𝑁) = ∅) | 
| 20 |  | 0ss 4399 | . . . . . . . 8
⊢ ∅
⊆ (0..^𝐿) | 
| 21 | 19, 20 | eqsstrdi 4027 | . . . . . . 7
⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0))) → (𝑀..^𝑁) ⊆ (0..^𝐿)) | 
| 22 |  | iftrue 4530 | . . . . . . 7
⊢ ((𝑀..^𝑁) ⊆ (0..^𝐿) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀)))) | 
| 23 | 21, 22 | syl 17 | . . . . . 6
⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0))) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀)))) | 
| 24 |  | nn0re 12537 | . . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ0
→ 𝑀 ∈
ℝ) | 
| 25 |  | nn0re 12537 | . . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) | 
| 26 | 24, 25 | anim12ci 614 | . . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ)) | 
| 27 | 26 | adantl 481 | . . . . . . . . . 10
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0)) → (𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ)) | 
| 28 |  | suble0 11778 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ) → ((𝑁 − 𝑀) ≤ 0 ↔ 𝑁 ≤ 𝑀)) | 
| 29 | 27, 28 | syl 17 | . . . . . . . . 9
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0)) → ((𝑁 − 𝑀) ≤ 0 ↔ 𝑁 ≤ 𝑀)) | 
| 30 | 29 | biimparc 479 | . . . . . . . 8
⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0))) → (𝑁 − 𝑀) ≤ 0) | 
| 31 |  | 0z 12626 | . . . . . . . . 9
⊢ 0 ∈
ℤ | 
| 32 |  | zsubcl 12661 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑁 − 𝑀) ∈ ℤ) | 
| 33 | 3, 2, 32 | syl2anr 597 | . . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑁 − 𝑀) ∈ ℤ) | 
| 34 | 33 | adantl 481 | . . . . . . . . . 10
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0)) → (𝑁 − 𝑀) ∈ ℤ) | 
| 35 | 34 | adantl 481 | . . . . . . . . 9
⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0))) → (𝑁 − 𝑀) ∈ ℤ) | 
| 36 |  | fzon 13721 | . . . . . . . . 9
⊢ ((0
∈ ℤ ∧ (𝑁
− 𝑀) ∈ ℤ)
→ ((𝑁 − 𝑀) ≤ 0 ↔ (0..^(𝑁 − 𝑀)) = ∅)) | 
| 37 | 31, 35, 36 | sylancr 587 | . . . . . . . 8
⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0))) → ((𝑁 − 𝑀) ≤ 0 ↔ (0..^(𝑁 − 𝑀)) = ∅)) | 
| 38 | 30, 37 | mpbid 232 | . . . . . . 7
⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0))) → (0..^(𝑁 − 𝑀)) = ∅) | 
| 39 | 38 | mpteq1d 5236 | . . . . . 6
⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0))) → (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))) = (𝑥 ∈ ∅ ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀)))) | 
| 40 |  | mpt0 6709 | . . . . . . 7
⊢ (𝑥 ∈ ∅ ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))) = ∅ | 
| 41 |  | oveq2 7440 | . . . . . . . . . . . . 13
⊢ (𝑀 = 𝑁 → (𝑁 − 𝑀) = (𝑁 − 𝑁)) | 
| 42 | 41 | oveq2d 7448 | . . . . . . . . . . . 12
⊢ (𝑀 = 𝑁 → (𝑆 repeatS (𝑁 − 𝑀)) = (𝑆 repeatS (𝑁 − 𝑁))) | 
| 43 |  | nn0cn 12538 | . . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℂ) | 
| 44 | 43 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → 𝑁 ∈ ℂ) | 
| 45 | 44 | subidd 11609 | . . . . . . . . . . . . . . 15
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑁 − 𝑁) = 0) | 
| 46 | 45 | adantl 481 | . . . . . . . . . . . . . 14
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0)) → (𝑁 − 𝑁) = 0) | 
| 47 | 46 | oveq2d 7448 | . . . . . . . . . . . . 13
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0)) → (𝑆 repeatS (𝑁 − 𝑁)) = (𝑆 repeatS 0)) | 
| 48 |  | repsw0 14816 | . . . . . . . . . . . . . 14
⊢ (𝑆 ∈ 𝑉 → (𝑆 repeatS 0) = ∅) | 
| 49 | 48 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0)) → (𝑆 repeatS 0) = ∅) | 
| 50 | 47, 49 | eqtrd 2776 | . . . . . . . . . . . 12
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0)) → (𝑆 repeatS (𝑁 − 𝑁)) = ∅) | 
| 51 | 42, 50 | sylan9eqr 2798 | . . . . . . . . . . 11
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0)) ∧ 𝑀 = 𝑁) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅) | 
| 52 | 51 | ex 412 | . . . . . . . . . 10
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0)) → (𝑀 = 𝑁 → (𝑆 repeatS (𝑁 − 𝑀)) = ∅)) | 
| 53 | 52 | adantl 481 | . . . . . . . . 9
⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0))) → (𝑀 = 𝑁 → (𝑆 repeatS (𝑁 − 𝑀)) = ∅)) | 
| 54 | 53 | com12 32 | . . . . . . . 8
⊢ (𝑀 = 𝑁 → ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0))) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅)) | 
| 55 |  | elnn0z 12628 | . . . . . . . . . . . . . . 15
⊢ ((𝑁 − 𝑀) ∈ ℕ0 ↔ ((𝑁 − 𝑀) ∈ ℤ ∧ 0 ≤ (𝑁 − 𝑀))) | 
| 56 |  | subge0 11777 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ) → (0 ≤
(𝑁 − 𝑀) ↔ 𝑀 ≤ 𝑁)) | 
| 57 | 25, 24, 56 | syl2anr 597 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (0 ≤ (𝑁 − 𝑀) ↔ 𝑀 ≤ 𝑁)) | 
| 58 | 24, 25 | anim12i 613 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ)) | 
| 59 |  | letri3 11347 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑀 = 𝑁 ↔ (𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀))) | 
| 60 | 58, 59 | syl 17 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑀 = 𝑁 ↔ (𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀))) | 
| 61 | 60 | biimprd 248 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ((𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀) → 𝑀 = 𝑁)) | 
| 62 | 61 | expd 415 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑀 ≤ 𝑁 → (𝑁 ≤ 𝑀 → 𝑀 = 𝑁))) | 
| 63 | 57, 62 | sylbid 240 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (0 ≤ (𝑁 − 𝑀) → (𝑁 ≤ 𝑀 → 𝑀 = 𝑁))) | 
| 64 | 63 | com23 86 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑁 ≤ 𝑀 → (0 ≤ (𝑁 − 𝑀) → 𝑀 = 𝑁))) | 
| 65 | 64 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0)) → (𝑁 ≤ 𝑀 → (0 ≤ (𝑁 − 𝑀) → 𝑀 = 𝑁))) | 
| 66 | 65 | impcom 407 | . . . . . . . . . . . . . . . 16
⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0))) → (0 ≤ (𝑁 − 𝑀) → 𝑀 = 𝑁)) | 
| 67 | 66 | com12 32 | . . . . . . . . . . . . . . 15
⊢ (0 ≤
(𝑁 − 𝑀) → ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0))) → 𝑀 = 𝑁)) | 
| 68 | 55, 67 | simplbiim 504 | . . . . . . . . . . . . . 14
⊢ ((𝑁 − 𝑀) ∈ ℕ0 → ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0))) → 𝑀 = 𝑁)) | 
| 69 | 68 | com12 32 | . . . . . . . . . . . . 13
⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0))) → ((𝑁 − 𝑀) ∈ ℕ0 → 𝑀 = 𝑁)) | 
| 70 | 69 | con3d 152 | . . . . . . . . . . . 12
⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0))) → (¬ 𝑀 = 𝑁 → ¬ (𝑁 − 𝑀) ∈
ℕ0)) | 
| 71 | 70 | impcom 407 | . . . . . . . . . . 11
⊢ ((¬
𝑀 = 𝑁 ∧ (𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0)))) → ¬ (𝑁 − 𝑀) ∈
ℕ0) | 
| 72 |  | df-nel 3046 | . . . . . . . . . . 11
⊢ ((𝑁 − 𝑀) ∉ ℕ0 ↔ ¬
(𝑁 − 𝑀) ∈
ℕ0) | 
| 73 | 71, 72 | sylibr 234 | . . . . . . . . . 10
⊢ ((¬
𝑀 = 𝑁 ∧ (𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0)))) → (𝑁 − 𝑀) ∉
ℕ0) | 
| 74 |  | repsundef 14810 | . . . . . . . . . 10
⊢ ((𝑁 − 𝑀) ∉ ℕ0 → (𝑆 repeatS (𝑁 − 𝑀)) = ∅) | 
| 75 | 73, 74 | syl 17 | . . . . . . . . 9
⊢ ((¬
𝑀 = 𝑁 ∧ (𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0)))) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅) | 
| 76 | 75 | ex 412 | . . . . . . . 8
⊢ (¬
𝑀 = 𝑁 → ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0))) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅)) | 
| 77 | 54, 76 | pm2.61i 182 | . . . . . . 7
⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0))) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅) | 
| 78 | 40, 77 | eqtr4id 2795 | . . . . . 6
⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0))) → (𝑥 ∈ ∅ ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))) = (𝑆 repeatS (𝑁 − 𝑀))) | 
| 79 | 23, 39, 78 | 3eqtrd 2780 | . . . . 5
⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0))) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁 − 𝑀))) | 
| 80 | 79 | expcom 413 | . . . 4
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0)) → (𝑁 ≤ 𝑀 → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁 − 𝑀)))) | 
| 81 | 80 | 3adant3 1132 | . . 3
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) → (𝑁 ≤ 𝑀 → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁 − 𝑀)))) | 
| 82 |  | ltnle 11341 | . . . . . . 7
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑀 < 𝑁 ↔ ¬ 𝑁 ≤ 𝑀)) | 
| 83 | 58, 82 | syl 17 | . . . . . 6
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑀 < 𝑁 ↔ ¬ 𝑁 ≤ 𝑀)) | 
| 84 | 83 | bicomd 223 | . . . . 5
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (¬ 𝑁 ≤ 𝑀 ↔ 𝑀 < 𝑁)) | 
| 85 | 84 | 3ad2ant2 1134 | . . . 4
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) → (¬ 𝑁 ≤ 𝑀 ↔ 𝑀 < 𝑁)) | 
| 86 | 22 | adantr 480 | . . . . . . 7
⊢ (((𝑀..^𝑁) ⊆ (0..^𝐿) ∧ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁)) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀)))) | 
| 87 | 4 | 3ad2ant2 1134 | . . . . . . . . . . 11
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) | 
| 88 | 87 | adantr 480 | . . . . . . . . . 10
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) | 
| 89 |  | 0zd 12627 | . . . . . . . . . . . . 13
⊢ (𝑆 ∈ 𝑉 → 0 ∈ ℤ) | 
| 90 |  | nn0z 12640 | . . . . . . . . . . . . 13
⊢ (𝐿 ∈ ℕ0
→ 𝐿 ∈
ℤ) | 
| 91 | 89, 90 | anim12i 613 | . . . . . . . . . . . 12
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → (0
∈ ℤ ∧ 𝐿
∈ ℤ)) | 
| 92 | 91 | 3ad2ant1 1133 | . . . . . . . . . . 11
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) → (0 ∈ ℤ ∧ 𝐿 ∈
ℤ)) | 
| 93 | 92 | adantr 480 | . . . . . . . . . 10
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (0 ∈ ℤ ∧ 𝐿 ∈
ℤ)) | 
| 94 |  | simpr 484 | . . . . . . . . . 10
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → 𝑀 < 𝑁) | 
| 95 |  | ssfzo12bi 13801 | . . . . . . . . . 10
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ∈
ℤ ∧ 𝐿 ∈
ℤ) ∧ 𝑀 < 𝑁) → ((𝑀..^𝑁) ⊆ (0..^𝐿) ↔ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿))) | 
| 96 | 88, 93, 94, 95 | syl3anc 1372 | . . . . . . . . 9
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → ((𝑀..^𝑁) ⊆ (0..^𝐿) ↔ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿))) | 
| 97 |  | simpl1l 1224 | . . . . . . . . . . . . . 14
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → 𝑆 ∈ 𝑉) | 
| 98 | 97 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢
((((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → 𝑆 ∈ 𝑉) | 
| 99 |  | simpl1r 1225 | . . . . . . . . . . . . . 14
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → 𝐿 ∈
ℕ0) | 
| 100 | 99 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢
((((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → 𝐿 ∈
ℕ0) | 
| 101 |  | nn0addcl 12563 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → (𝑥 + 𝑀) ∈
ℕ0) | 
| 102 | 101 | expcom 413 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑀 ∈ ℕ0
→ (𝑥 ∈
ℕ0 → (𝑥 + 𝑀) ∈
ℕ0)) | 
| 103 | 102 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑥 ∈ ℕ0 → (𝑥 + 𝑀) ∈
ℕ0)) | 
| 104 | 103 | 3ad2ant2 1134 | . . . . . . . . . . . . . . . 16
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) → (𝑥 ∈ ℕ0 → (𝑥 + 𝑀) ∈
ℕ0)) | 
| 105 | 104 | ad2antrr 726 | . . . . . . . . . . . . . . 15
⊢
(((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) → (𝑥 ∈ ℕ0 → (𝑥 + 𝑀) ∈
ℕ0)) | 
| 106 |  | elfzonn0 13748 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (0..^(𝑁 − 𝑀)) → 𝑥 ∈ ℕ0) | 
| 107 | 105, 106 | impel 505 | . . . . . . . . . . . . . 14
⊢
((((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → (𝑥 + 𝑀) ∈
ℕ0) | 
| 108 | 90 | adantl 481 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → 𝐿 ∈
ℤ) | 
| 109 | 108 | 3ad2ant1 1133 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) → 𝐿 ∈ ℤ) | 
| 110 | 109 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → 𝐿 ∈ ℤ) | 
| 111 |  | nn0re 12537 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐿 ∈ ℕ0
→ 𝐿 ∈
ℝ) | 
| 112 | 111 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → 𝐿 ∈
ℝ) | 
| 113 | 112, 58 | anim12ci 614 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0)) → ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝐿 ∈ ℝ)) | 
| 114 |  | df-3an 1088 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ) ↔ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝐿 ∈
ℝ)) | 
| 115 | 113, 114 | sylibr 234 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0)) → (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ)) | 
| 116 |  | ltletr 11354 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ) → ((𝑀 < 𝑁 ∧ 𝑁 ≤ 𝐿) → 𝑀 < 𝐿)) | 
| 117 | 115, 116 | syl 17 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0)) → ((𝑀 < 𝑁 ∧ 𝑁 ≤ 𝐿) → 𝑀 < 𝐿)) | 
| 118 |  | elnn0z 12628 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑀 ∈ ℕ0
↔ (𝑀 ∈ ℤ
∧ 0 ≤ 𝑀)) | 
| 119 |  | 0red 11265 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑀 ∈ ℤ ∧ (𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0)) → 0
∈ ℝ) | 
| 120 |  | zre 12619 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℝ) | 
| 121 | 120 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑀 ∈ ℤ ∧ (𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0)) → 𝑀 ∈
ℝ) | 
| 122 | 112 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑀 ∈ ℤ ∧ (𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0)) → 𝐿 ∈
ℝ) | 
| 123 |  | lelttr 11352 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((0
∈ ℝ ∧ 𝑀
∈ ℝ ∧ 𝐿
∈ ℝ) → ((0 ≤ 𝑀 ∧ 𝑀 < 𝐿) → 0 < 𝐿)) | 
| 124 | 119, 121,
122, 123 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑀 ∈ ℤ ∧ (𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0)) → ((0
≤ 𝑀 ∧ 𝑀 < 𝐿) → 0 < 𝐿)) | 
| 125 | 124 | expd 415 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑀 ∈ ℤ ∧ (𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0)) → (0 ≤
𝑀 → (𝑀 < 𝐿 → 0 < 𝐿))) | 
| 126 | 125 | impancom 451 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑀 ∈ ℤ ∧ 0 ≤
𝑀) → ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → (𝑀 < 𝐿 → 0 < 𝐿))) | 
| 127 | 118, 126 | sylbi 217 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑀 ∈ ℕ0
→ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → (𝑀 < 𝐿 → 0 < 𝐿))) | 
| 128 | 127 | adantr 480 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → (𝑀 < 𝐿 → 0 < 𝐿))) | 
| 129 | 128 | impcom 407 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0)) → (𝑀 < 𝐿 → 0 < 𝐿)) | 
| 130 | 117, 129 | syld 47 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0)) → ((𝑀 < 𝑁 ∧ 𝑁 ≤ 𝐿) → 0 < 𝐿)) | 
| 131 | 130 | expcomd 416 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0)) → (𝑁 ≤ 𝐿 → (𝑀 < 𝑁 → 0 < 𝐿))) | 
| 132 | 131 | 3impia 1117 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) → (𝑀 < 𝑁 → 0 < 𝐿)) | 
| 133 | 132 | imp 406 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → 0 < 𝐿) | 
| 134 |  | elnnz 12625 | . . . . . . . . . . . . . . . 16
⊢ (𝐿 ∈ ℕ ↔ (𝐿 ∈ ℤ ∧ 0 <
𝐿)) | 
| 135 | 110, 133,
134 | sylanbrc 583 | . . . . . . . . . . . . . . 15
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → 𝐿 ∈ ℕ) | 
| 136 | 135 | ad2antrr 726 | . . . . . . . . . . . . . 14
⊢
((((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → 𝐿 ∈ ℕ) | 
| 137 |  | elfzo0 13741 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↔ (𝑥 ∈ ℕ0 ∧ (𝑁 − 𝑀) ∈ ℕ ∧ 𝑥 < (𝑁 − 𝑀))) | 
| 138 |  | nn0readdcl 12595 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑥 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → (𝑥 + 𝑀) ∈ ℝ) | 
| 139 | 138 | expcom 413 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑀 ∈ ℕ0
→ (𝑥 ∈
ℕ0 → (𝑥 + 𝑀) ∈ ℝ)) | 
| 140 | 139 | ad2antrl 728 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝐿 ∈ ℕ0
∧ (𝑀 ∈
ℕ0 ∧ 𝑁
∈ ℕ0)) → (𝑥 ∈ ℕ0 → (𝑥 + 𝑀) ∈ ℝ)) | 
| 141 | 140 | impcom 407 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑥 ∈ ℕ0
∧ (𝐿 ∈
ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)))
→ (𝑥 + 𝑀) ∈
ℝ) | 
| 142 | 25 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → 𝑁 ∈ ℝ) | 
| 143 | 142 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝐿 ∈ ℕ0
∧ (𝑀 ∈
ℕ0 ∧ 𝑁
∈ ℕ0)) → 𝑁 ∈ ℝ) | 
| 144 | 143 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑥 ∈ ℕ0
∧ (𝐿 ∈
ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)))
→ 𝑁 ∈
ℝ) | 
| 145 | 111 | ad2antrl 728 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑥 ∈ ℕ0
∧ (𝐿 ∈
ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)))
→ 𝐿 ∈
ℝ) | 
| 146 | 141, 144,
145 | 3jca 1128 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑥 ∈ ℕ0
∧ (𝐿 ∈
ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)))
→ ((𝑥 + 𝑀) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈
ℝ)) | 
| 147 | 146 | ex 412 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑥 ∈ ℕ0
→ ((𝐿 ∈
ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))
→ ((𝑥 + 𝑀) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈
ℝ))) | 
| 148 | 147 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑥 ∈ ℕ0
∧ 𝑥 < (𝑁 − 𝑀)) → ((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0)) → ((𝑥 + 𝑀) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ))) | 
| 149 | 148 | impcom 407 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝐿 ∈ ℕ0
∧ (𝑀 ∈
ℕ0 ∧ 𝑁
∈ ℕ0)) ∧ (𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀))) → ((𝑥 + 𝑀) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ)) | 
| 150 | 149 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐿 ∈ ℕ0
∧ (𝑀 ∈
ℕ0 ∧ 𝑁
∈ ℕ0)) ∧ (𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀))) ∧ 𝑁 ≤ 𝐿) → ((𝑥 + 𝑀) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ)) | 
| 151 |  | nn0re 12537 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑥 ∈ ℕ0
→ 𝑥 ∈
ℝ) | 
| 152 | 151 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑥 ∈ ℕ0
∧ (𝐿 ∈
ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)))
→ 𝑥 ∈
ℝ) | 
| 153 | 24 | ad2antrl 728 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝐿 ∈ ℕ0
∧ (𝑀 ∈
ℕ0 ∧ 𝑁
∈ ℕ0)) → 𝑀 ∈ ℝ) | 
| 154 | 153 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑥 ∈ ℕ0
∧ (𝐿 ∈
ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)))
→ 𝑀 ∈
ℝ) | 
| 155 | 152, 154,
144 | ltaddsubd 11864 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑥 ∈ ℕ0
∧ (𝐿 ∈
ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)))
→ ((𝑥 + 𝑀) < 𝑁 ↔ 𝑥 < (𝑁 − 𝑀))) | 
| 156 |  | idd 24 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑥 ∈ ℕ0
∧ (𝐿 ∈
ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)))
∧ 𝑁 ≤ 𝐿) → ((𝑥 + 𝑀) < 𝑁 → (𝑥 + 𝑀) < 𝑁)) | 
| 157 | 156 | ex 412 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑥 ∈ ℕ0
∧ (𝐿 ∈
ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)))
→ (𝑁 ≤ 𝐿 → ((𝑥 + 𝑀) < 𝑁 → (𝑥 + 𝑀) < 𝑁))) | 
| 158 | 157 | com23 86 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑥 ∈ ℕ0
∧ (𝐿 ∈
ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)))
→ ((𝑥 + 𝑀) < 𝑁 → (𝑁 ≤ 𝐿 → (𝑥 + 𝑀) < 𝑁))) | 
| 159 | 155, 158 | sylbird 260 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑥 ∈ ℕ0
∧ (𝐿 ∈
ℕ0 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)))
→ (𝑥 < (𝑁 − 𝑀) → (𝑁 ≤ 𝐿 → (𝑥 + 𝑀) < 𝑁))) | 
| 160 | 159 | impancom 451 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑥 ∈ ℕ0
∧ 𝑥 < (𝑁 − 𝑀)) → ((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0)) → (𝑁 ≤ 𝐿 → (𝑥 + 𝑀) < 𝑁))) | 
| 161 | 160 | impcom 407 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝐿 ∈ ℕ0
∧ (𝑀 ∈
ℕ0 ∧ 𝑁
∈ ℕ0)) ∧ (𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀))) → (𝑁 ≤ 𝐿 → (𝑥 + 𝑀) < 𝑁)) | 
| 162 | 161 | impac 552 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐿 ∈ ℕ0
∧ (𝑀 ∈
ℕ0 ∧ 𝑁
∈ ℕ0)) ∧ (𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀))) ∧ 𝑁 ≤ 𝐿) → ((𝑥 + 𝑀) < 𝑁 ∧ 𝑁 ≤ 𝐿)) | 
| 163 |  | ltletr 11354 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑥 + 𝑀) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ) → (((𝑥 + 𝑀) < 𝑁 ∧ 𝑁 ≤ 𝐿) → (𝑥 + 𝑀) < 𝐿)) | 
| 164 | 150, 162,
163 | sylc 65 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐿 ∈ ℕ0
∧ (𝑀 ∈
ℕ0 ∧ 𝑁
∈ ℕ0)) ∧ (𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀))) ∧ 𝑁 ≤ 𝐿) → (𝑥 + 𝑀) < 𝐿) | 
| 165 | 164 | exp31 419 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐿 ∈ ℕ0
∧ (𝑀 ∈
ℕ0 ∧ 𝑁
∈ ℕ0)) → ((𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀)) → (𝑁 ≤ 𝐿 → (𝑥 + 𝑀) < 𝐿))) | 
| 166 | 165 | com23 86 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐿 ∈ ℕ0
∧ (𝑀 ∈
ℕ0 ∧ 𝑁
∈ ℕ0)) → (𝑁 ≤ 𝐿 → ((𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀)) → (𝑥 + 𝑀) < 𝐿))) | 
| 167 | 166 | ex 412 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐿 ∈ ℕ0
→ ((𝑀 ∈
ℕ0 ∧ 𝑁
∈ ℕ0) → (𝑁 ≤ 𝐿 → ((𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀)) → (𝑥 + 𝑀) < 𝐿)))) | 
| 168 | 167 | adantl 481 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑁 ≤ 𝐿 → ((𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀)) → (𝑥 + 𝑀) < 𝐿)))) | 
| 169 | 168 | 3imp 1110 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) → ((𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀)) → (𝑥 + 𝑀) < 𝐿)) | 
| 170 | 169 | ad2antrr 726 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) → ((𝑥 ∈ ℕ0 ∧ 𝑥 < (𝑁 − 𝑀)) → (𝑥 + 𝑀) < 𝐿)) | 
| 171 | 170 | com12 32 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℕ0
∧ 𝑥 < (𝑁 − 𝑀)) → (((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) → (𝑥 + 𝑀) < 𝐿)) | 
| 172 | 171 | 3adant2 1131 | . . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℕ0
∧ (𝑁 − 𝑀) ∈ ℕ ∧ 𝑥 < (𝑁 − 𝑀)) → (((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) → (𝑥 + 𝑀) < 𝐿)) | 
| 173 | 137, 172 | sylbi 217 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (0..^(𝑁 − 𝑀)) → (((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) → (𝑥 + 𝑀) < 𝐿)) | 
| 174 | 173 | impcom 407 | . . . . . . . . . . . . . 14
⊢
((((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → (𝑥 + 𝑀) < 𝐿) | 
| 175 |  | elfzo0 13741 | . . . . . . . . . . . . . 14
⊢ ((𝑥 + 𝑀) ∈ (0..^𝐿) ↔ ((𝑥 + 𝑀) ∈ ℕ0 ∧ 𝐿 ∈ ℕ ∧ (𝑥 + 𝑀) < 𝐿)) | 
| 176 | 107, 136,
174, 175 | syl3anbrc 1343 | . . . . . . . . . . . . 13
⊢
((((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → (𝑥 + 𝑀) ∈ (0..^𝐿)) | 
| 177 |  | repswsymb 14813 | . . . . . . . . . . . . 13
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0 ∧ (𝑥 + 𝑀) ∈ (0..^𝐿)) → ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀)) = 𝑆) | 
| 178 | 98, 100, 176, 177 | syl3anc 1372 | . . . . . . . . . . . 12
⊢
((((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) ∧ 𝑥 ∈ (0..^(𝑁 − 𝑀))) → ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀)) = 𝑆) | 
| 179 | 178 | mpteq2dva 5241 | . . . . . . . . . . 11
⊢
(((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) → (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))) = (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ 𝑆)) | 
| 180 | 33 | 3ad2ant2 1134 | . . . . . . . . . . . . . . . 16
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) → (𝑁 − 𝑀) ∈ ℤ) | 
| 181 | 180 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (𝑁 − 𝑀) ∈ ℤ) | 
| 182 | 58 | 3ad2ant2 1134 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) → (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ)) | 
| 183 |  | ltle 11350 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑀 < 𝑁 → 𝑀 ≤ 𝑁)) | 
| 184 | 182, 183 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) → (𝑀 < 𝑁 → 𝑀 ≤ 𝑁)) | 
| 185 | 26 | 3ad2ant2 1134 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) → (𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ)) | 
| 186 | 185, 56 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) → (0 ≤ (𝑁 − 𝑀) ↔ 𝑀 ≤ 𝑁)) | 
| 187 | 184, 186 | sylibrd 259 | . . . . . . . . . . . . . . . 16
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) → (𝑀 < 𝑁 → 0 ≤ (𝑁 − 𝑀))) | 
| 188 | 187 | imp 406 | . . . . . . . . . . . . . . 15
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → 0 ≤ (𝑁 − 𝑀)) | 
| 189 | 181, 188,
55 | sylanbrc 583 | . . . . . . . . . . . . . 14
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (𝑁 − 𝑀) ∈
ℕ0) | 
| 190 | 97, 189 | jca 511 | . . . . . . . . . . . . 13
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (𝑆 ∈ 𝑉 ∧ (𝑁 − 𝑀) ∈
ℕ0)) | 
| 191 | 190 | adantr 480 | . . . . . . . . . . . 12
⊢
(((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) → (𝑆 ∈ 𝑉 ∧ (𝑁 − 𝑀) ∈
ℕ0)) | 
| 192 |  | reps 14809 | . . . . . . . . . . . . 13
⊢ ((𝑆 ∈ 𝑉 ∧ (𝑁 − 𝑀) ∈ ℕ0) → (𝑆 repeatS (𝑁 − 𝑀)) = (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ 𝑆)) | 
| 193 | 192 | eqcomd 2742 | . . . . . . . . . . . 12
⊢ ((𝑆 ∈ 𝑉 ∧ (𝑁 − 𝑀) ∈ ℕ0) → (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ 𝑆) = (𝑆 repeatS (𝑁 − 𝑀))) | 
| 194 | 191, 193 | syl 17 | . . . . . . . . . . 11
⊢
(((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) → (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ 𝑆) = (𝑆 repeatS (𝑁 − 𝑀))) | 
| 195 | 179, 194 | eqtrd 2776 | . . . . . . . . . 10
⊢
(((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿)) → (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))) = (𝑆 repeatS (𝑁 − 𝑀))) | 
| 196 | 195 | ex 412 | . . . . . . . . 9
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → ((0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿) → (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))) = (𝑆 repeatS (𝑁 − 𝑀)))) | 
| 197 | 96, 196 | sylbid 240 | . . . . . . . 8
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → ((𝑀..^𝑁) ⊆ (0..^𝐿) → (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))) = (𝑆 repeatS (𝑁 − 𝑀)))) | 
| 198 | 197 | impcom 407 | . . . . . . 7
⊢ (((𝑀..^𝑁) ⊆ (0..^𝐿) ∧ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁)) → (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))) = (𝑆 repeatS (𝑁 − 𝑀))) | 
| 199 | 86, 198 | eqtrd 2776 | . . . . . 6
⊢ (((𝑀..^𝑁) ⊆ (0..^𝐿) ∧ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁)) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁 − 𝑀))) | 
| 200 |  | iffalse 4533 | . . . . . . . 8
⊢ (¬
(𝑀..^𝑁) ⊆ (0..^𝐿) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = ∅) | 
| 201 | 200 | adantr 480 | . . . . . . 7
⊢ ((¬
(𝑀..^𝑁) ⊆ (0..^𝐿) ∧ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁)) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = ∅) | 
| 202 | 96 | notbid 318 | . . . . . . . . 9
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (¬ (𝑀..^𝑁) ⊆ (0..^𝐿) ↔ ¬ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿))) | 
| 203 |  | ianor 983 | . . . . . . . . . . 11
⊢ (¬ (0
≤ 𝑀 ∧ 𝑁 ≤ 𝐿) ↔ (¬ 0 ≤ 𝑀 ∨ ¬ 𝑁 ≤ 𝐿)) | 
| 204 |  | nn0ge0 12553 | . . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ ℕ0
→ 0 ≤ 𝑀) | 
| 205 |  | pm2.24 124 | . . . . . . . . . . . . . . . . 17
⊢ (0 ≤
𝑀 → (¬ 0 ≤
𝑀 → (𝑆 repeatS (𝑁 − 𝑀)) = ∅)) | 
| 206 | 204, 205 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ ℕ0
→ (¬ 0 ≤ 𝑀
→ (𝑆 repeatS (𝑁 − 𝑀)) = ∅)) | 
| 207 | 206 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (¬ 0 ≤ 𝑀 → (𝑆 repeatS (𝑁 − 𝑀)) = ∅)) | 
| 208 | 207 | 3ad2ant2 1134 | . . . . . . . . . . . . . 14
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) → (¬ 0 ≤ 𝑀 → (𝑆 repeatS (𝑁 − 𝑀)) = ∅)) | 
| 209 | 208 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (¬ 0 ≤ 𝑀 → (𝑆 repeatS (𝑁 − 𝑀)) = ∅)) | 
| 210 | 209 | com12 32 | . . . . . . . . . . . 12
⊢ (¬ 0
≤ 𝑀 → ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅)) | 
| 211 |  | pm2.24 124 | . . . . . . . . . . . . . . 15
⊢ (𝑁 ≤ 𝐿 → (¬ 𝑁 ≤ 𝐿 → (𝑆 repeatS (𝑁 − 𝑀)) = ∅)) | 
| 212 | 211 | 3ad2ant3 1135 | . . . . . . . . . . . . . 14
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) → (¬ 𝑁 ≤ 𝐿 → (𝑆 repeatS (𝑁 − 𝑀)) = ∅)) | 
| 213 | 212 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (¬ 𝑁 ≤ 𝐿 → (𝑆 repeatS (𝑁 − 𝑀)) = ∅)) | 
| 214 | 213 | com12 32 | . . . . . . . . . . . 12
⊢ (¬
𝑁 ≤ 𝐿 → ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅)) | 
| 215 | 210, 214 | jaoi 857 | . . . . . . . . . . 11
⊢ ((¬ 0
≤ 𝑀 ∨ ¬ 𝑁 ≤ 𝐿) → ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅)) | 
| 216 | 203, 215 | sylbi 217 | . . . . . . . . . 10
⊢ (¬ (0
≤ 𝑀 ∧ 𝑁 ≤ 𝐿) → ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅)) | 
| 217 | 216 | com12 32 | . . . . . . . . 9
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (¬ (0 ≤ 𝑀 ∧ 𝑁 ≤ 𝐿) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅)) | 
| 218 | 202, 217 | sylbid 240 | . . . . . . . 8
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → (¬ (𝑀..^𝑁) ⊆ (0..^𝐿) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅)) | 
| 219 | 218 | impcom 407 | . . . . . . 7
⊢ ((¬
(𝑀..^𝑁) ⊆ (0..^𝐿) ∧ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁)) → (𝑆 repeatS (𝑁 − 𝑀)) = ∅) | 
| 220 | 201, 219 | eqtr4d 2779 | . . . . . 6
⊢ ((¬
(𝑀..^𝑁) ⊆ (0..^𝐿) ∧ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁)) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁 − 𝑀))) | 
| 221 | 199, 220 | pm2.61ian 811 | . . . . 5
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) ∧ 𝑀 < 𝑁) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁 − 𝑀))) | 
| 222 | 221 | ex 412 | . . . 4
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) → (𝑀 < 𝑁 → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁 − 𝑀)))) | 
| 223 | 85, 222 | sylbid 240 | . . 3
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) → (¬ 𝑁 ≤ 𝑀 → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁 − 𝑀)))) | 
| 224 | 81, 223 | pm2.61d 179 | . 2
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁 − 𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁 − 𝑀))) | 
| 225 | 10, 15, 224 | 3eqtrd 2780 | 1
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ≤ 𝐿) → ((𝑆 repeatS 𝐿) substr 〈𝑀, 𝑁〉) = (𝑆 repeatS (𝑁 − 𝑀))) |