MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  repswswrd Structured version   Visualization version   GIF version

Theorem repswswrd 13824
Description: A subword of a "repeated symbol word" is again a "repeated symbol word". The assumption N <_ L is required, because otherwise ( L < N ): ((𝑆 repeatS 𝐿) substr ⟨𝑀, 𝑁⟩) = ∅, but for M < N (𝑆 repeatS (𝑁𝑀))) ≠ ∅! The proof is relatively long because the border cases (𝑀 = 𝑁, ¬ (𝑀..^𝑁) ⊆ (0..^𝐿) must have been considered. (Contributed by AV, 6-Nov-2018.)
Assertion
Ref Expression
repswswrd (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) → ((𝑆 repeatS 𝐿) substr ⟨𝑀, 𝑁⟩) = (𝑆 repeatS (𝑁𝑀)))

Proof of Theorem repswswrd
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 repsw 13815 . . . . . 6 ((𝑆𝑉𝐿 ∈ ℕ0) → (𝑆 repeatS 𝐿) ∈ Word 𝑉)
2 nn0z 11653 . . . . . . 7 (𝑀 ∈ ℕ0𝑀 ∈ ℤ)
3 nn0z 11653 . . . . . . 7 (𝑁 ∈ ℕ0𝑁 ∈ ℤ)
42, 3anim12i 606 . . . . . 6 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
51, 4anim12i 606 . . . . 5 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) → ((𝑆 repeatS 𝐿) ∈ Word 𝑉 ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)))
6 3anass 1116 . . . . 5 (((𝑆 repeatS 𝐿) ∈ Word 𝑉𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ↔ ((𝑆 repeatS 𝐿) ∈ Word 𝑉 ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)))
75, 6sylibr 225 . . . 4 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) → ((𝑆 repeatS 𝐿) ∈ Word 𝑉𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
873adant3 1162 . . 3 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) → ((𝑆 repeatS 𝐿) ∈ Word 𝑉𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
9 swrdval 13627 . . 3 (((𝑆 repeatS 𝐿) ∈ Word 𝑉𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑆 repeatS 𝐿) substr ⟨𝑀, 𝑁⟩) = if((𝑀..^𝑁) ⊆ dom (𝑆 repeatS 𝐿), (𝑥 ∈ (0..^(𝑁𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅))
108, 9syl 17 . 2 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) → ((𝑆 repeatS 𝐿) substr ⟨𝑀, 𝑁⟩) = if((𝑀..^𝑁) ⊆ dom (𝑆 repeatS 𝐿), (𝑥 ∈ (0..^(𝑁𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅))
11 repsf 13813 . . . . . 6 ((𝑆𝑉𝐿 ∈ ℕ0) → (𝑆 repeatS 𝐿):(0..^𝐿)⟶𝑉)
12113ad2ant1 1163 . . . . 5 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) → (𝑆 repeatS 𝐿):(0..^𝐿)⟶𝑉)
1312fdmd 6234 . . . 4 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) → dom (𝑆 repeatS 𝐿) = (0..^𝐿))
1413sseq2d 3795 . . 3 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) → ((𝑀..^𝑁) ⊆ dom (𝑆 repeatS 𝐿) ↔ (𝑀..^𝑁) ⊆ (0..^𝐿)))
1514ifbid 4267 . 2 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) → if((𝑀..^𝑁) ⊆ dom (𝑆 repeatS 𝐿), (𝑥 ∈ (0..^(𝑁𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅))
16 fzon 12704 . . . . . . . . . . 11 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁𝑀 ↔ (𝑀..^𝑁) = ∅))
174, 16syl 17 . . . . . . . . . 10 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (𝑁𝑀 ↔ (𝑀..^𝑁) = ∅))
1817adantl 473 . . . . . . . . 9 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) → (𝑁𝑀 ↔ (𝑀..^𝑁) = ∅))
1918biimpac 470 . . . . . . . 8 ((𝑁𝑀 ∧ ((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → (𝑀..^𝑁) = ∅)
20 0ss 4136 . . . . . . . 8 ∅ ⊆ (0..^𝐿)
2119, 20syl6eqss 3817 . . . . . . 7 ((𝑁𝑀 ∧ ((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → (𝑀..^𝑁) ⊆ (0..^𝐿))
22 iftrue 4251 . . . . . . 7 ((𝑀..^𝑁) ⊆ (0..^𝐿) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑥 ∈ (0..^(𝑁𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))))
2321, 22syl 17 . . . . . 6 ((𝑁𝑀 ∧ ((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑥 ∈ (0..^(𝑁𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))))
24 nn0re 11553 . . . . . . . . . . . 12 (𝑀 ∈ ℕ0𝑀 ∈ ℝ)
25 nn0re 11553 . . . . . . . . . . . 12 (𝑁 ∈ ℕ0𝑁 ∈ ℝ)
2624, 25anim12ci 607 . . . . . . . . . . 11 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ))
2726adantl 473 . . . . . . . . . 10 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) → (𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ))
28 suble0 10801 . . . . . . . . . 10 ((𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ) → ((𝑁𝑀) ≤ 0 ↔ 𝑁𝑀))
2927, 28syl 17 . . . . . . . . 9 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) → ((𝑁𝑀) ≤ 0 ↔ 𝑁𝑀))
3029biimparc 471 . . . . . . . 8 ((𝑁𝑀 ∧ ((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → (𝑁𝑀) ≤ 0)
31 0z 11640 . . . . . . . . 9 0 ∈ ℤ
32 zsubcl 11672 . . . . . . . . . . . 12 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑁𝑀) ∈ ℤ)
333, 2, 32syl2anr 590 . . . . . . . . . . 11 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (𝑁𝑀) ∈ ℤ)
3433adantl 473 . . . . . . . . . 10 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) → (𝑁𝑀) ∈ ℤ)
3534adantl 473 . . . . . . . . 9 ((𝑁𝑀 ∧ ((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → (𝑁𝑀) ∈ ℤ)
36 fzon 12704 . . . . . . . . 9 ((0 ∈ ℤ ∧ (𝑁𝑀) ∈ ℤ) → ((𝑁𝑀) ≤ 0 ↔ (0..^(𝑁𝑀)) = ∅))
3731, 35, 36sylancr 581 . . . . . . . 8 ((𝑁𝑀 ∧ ((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → ((𝑁𝑀) ≤ 0 ↔ (0..^(𝑁𝑀)) = ∅))
3830, 37mpbid 223 . . . . . . 7 ((𝑁𝑀 ∧ ((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → (0..^(𝑁𝑀)) = ∅)
3938mpteq1d 4899 . . . . . 6 ((𝑁𝑀 ∧ ((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → (𝑥 ∈ (0..^(𝑁𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))) = (𝑥 ∈ ∅ ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))))
40 oveq2 6854 . . . . . . . . . . . . 13 (𝑀 = 𝑁 → (𝑁𝑀) = (𝑁𝑁))
4140oveq2d 6862 . . . . . . . . . . . 12 (𝑀 = 𝑁 → (𝑆 repeatS (𝑁𝑀)) = (𝑆 repeatS (𝑁𝑁)))
42 nn0cn 11554 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ0𝑁 ∈ ℂ)
4342adantl 473 . . . . . . . . . . . . . . . 16 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → 𝑁 ∈ ℂ)
4443subidd 10639 . . . . . . . . . . . . . . 15 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (𝑁𝑁) = 0)
4544adantl 473 . . . . . . . . . . . . . 14 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) → (𝑁𝑁) = 0)
4645oveq2d 6862 . . . . . . . . . . . . 13 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) → (𝑆 repeatS (𝑁𝑁)) = (𝑆 repeatS 0))
47 repsw0 13817 . . . . . . . . . . . . . 14 (𝑆𝑉 → (𝑆 repeatS 0) = ∅)
4847ad2antrr 717 . . . . . . . . . . . . 13 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) → (𝑆 repeatS 0) = ∅)
4946, 48eqtrd 2799 . . . . . . . . . . . 12 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) → (𝑆 repeatS (𝑁𝑁)) = ∅)
5041, 49sylan9eqr 2821 . . . . . . . . . . 11 ((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) ∧ 𝑀 = 𝑁) → (𝑆 repeatS (𝑁𝑀)) = ∅)
5150ex 401 . . . . . . . . . 10 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) → (𝑀 = 𝑁 → (𝑆 repeatS (𝑁𝑀)) = ∅))
5251adantl 473 . . . . . . . . 9 ((𝑁𝑀 ∧ ((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → (𝑀 = 𝑁 → (𝑆 repeatS (𝑁𝑀)) = ∅))
5352com12 32 . . . . . . . 8 (𝑀 = 𝑁 → ((𝑁𝑀 ∧ ((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → (𝑆 repeatS (𝑁𝑀)) = ∅))
54 elnn0z 11642 . . . . . . . . . . . . . . 15 ((𝑁𝑀) ∈ ℕ0 ↔ ((𝑁𝑀) ∈ ℤ ∧ 0 ≤ (𝑁𝑀)))
55 subge0 10800 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ) → (0 ≤ (𝑁𝑀) ↔ 𝑀𝑁))
5625, 24, 55syl2anr 590 . . . . . . . . . . . . . . . . . . . . 21 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (0 ≤ (𝑁𝑀) ↔ 𝑀𝑁))
5724, 25anim12i 606 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ))
58 letri3 10382 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑀 = 𝑁 ↔ (𝑀𝑁𝑁𝑀)))
5957, 58syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (𝑀 = 𝑁 ↔ (𝑀𝑁𝑁𝑀)))
6059biimprd 239 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → ((𝑀𝑁𝑁𝑀) → 𝑀 = 𝑁))
6160expd 404 . . . . . . . . . . . . . . . . . . . . 21 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (𝑀𝑁 → (𝑁𝑀𝑀 = 𝑁)))
6256, 61sylbid 231 . . . . . . . . . . . . . . . . . . . 20 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (0 ≤ (𝑁𝑀) → (𝑁𝑀𝑀 = 𝑁)))
6362com23 86 . . . . . . . . . . . . . . . . . . 19 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (𝑁𝑀 → (0 ≤ (𝑁𝑀) → 𝑀 = 𝑁)))
6463adantl 473 . . . . . . . . . . . . . . . . . 18 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) → (𝑁𝑀 → (0 ≤ (𝑁𝑀) → 𝑀 = 𝑁)))
6564impcom 396 . . . . . . . . . . . . . . . . 17 ((𝑁𝑀 ∧ ((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → (0 ≤ (𝑁𝑀) → 𝑀 = 𝑁))
6665com12 32 . . . . . . . . . . . . . . . 16 (0 ≤ (𝑁𝑀) → ((𝑁𝑀 ∧ ((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → 𝑀 = 𝑁))
6766adantl 473 . . . . . . . . . . . . . . 15 (((𝑁𝑀) ∈ ℤ ∧ 0 ≤ (𝑁𝑀)) → ((𝑁𝑀 ∧ ((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → 𝑀 = 𝑁))
6854, 67sylbi 208 . . . . . . . . . . . . . 14 ((𝑁𝑀) ∈ ℕ0 → ((𝑁𝑀 ∧ ((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → 𝑀 = 𝑁))
6968com12 32 . . . . . . . . . . . . 13 ((𝑁𝑀 ∧ ((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → ((𝑁𝑀) ∈ ℕ0𝑀 = 𝑁))
7069con3d 149 . . . . . . . . . . . 12 ((𝑁𝑀 ∧ ((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → (¬ 𝑀 = 𝑁 → ¬ (𝑁𝑀) ∈ ℕ0))
7170impcom 396 . . . . . . . . . . 11 ((¬ 𝑀 = 𝑁 ∧ (𝑁𝑀 ∧ ((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)))) → ¬ (𝑁𝑀) ∈ ℕ0)
72 df-nel 3041 . . . . . . . . . . 11 ((𝑁𝑀) ∉ ℕ0 ↔ ¬ (𝑁𝑀) ∈ ℕ0)
7371, 72sylibr 225 . . . . . . . . . 10 ((¬ 𝑀 = 𝑁 ∧ (𝑁𝑀 ∧ ((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)))) → (𝑁𝑀) ∉ ℕ0)
74 repsundef 13811 . . . . . . . . . 10 ((𝑁𝑀) ∉ ℕ0 → (𝑆 repeatS (𝑁𝑀)) = ∅)
7573, 74syl 17 . . . . . . . . 9 ((¬ 𝑀 = 𝑁 ∧ (𝑁𝑀 ∧ ((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)))) → (𝑆 repeatS (𝑁𝑀)) = ∅)
7675ex 401 . . . . . . . 8 𝑀 = 𝑁 → ((𝑁𝑀 ∧ ((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → (𝑆 repeatS (𝑁𝑀)) = ∅))
7753, 76pm2.61i 176 . . . . . . 7 ((𝑁𝑀 ∧ ((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → (𝑆 repeatS (𝑁𝑀)) = ∅)
78 mpt0 6201 . . . . . . 7 (𝑥 ∈ ∅ ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))) = ∅
7977, 78syl6reqr 2818 . . . . . 6 ((𝑁𝑀 ∧ ((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → (𝑥 ∈ ∅ ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))) = (𝑆 repeatS (𝑁𝑀)))
8023, 39, 793eqtrd 2803 . . . . 5 ((𝑁𝑀 ∧ ((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁𝑀)))
8180expcom 402 . . . 4 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) → (𝑁𝑀 → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁𝑀))))
82813adant3 1162 . . 3 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) → (𝑁𝑀 → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁𝑀))))
83 ltnle 10376 . . . . . . 7 ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑀 < 𝑁 ↔ ¬ 𝑁𝑀))
8457, 83syl 17 . . . . . 6 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (𝑀 < 𝑁 ↔ ¬ 𝑁𝑀))
8584bicomd 214 . . . . 5 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (¬ 𝑁𝑀𝑀 < 𝑁))
86853ad2ant2 1164 . . . 4 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) → (¬ 𝑁𝑀𝑀 < 𝑁))
8722adantr 472 . . . . . . 7 (((𝑀..^𝑁) ⊆ (0..^𝐿) ∧ (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁)) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑥 ∈ (0..^(𝑁𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))))
8843ad2ant2 1164 . . . . . . . . . . 11 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
8988adantr 472 . . . . . . . . . 10 ((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
90 0zd 11641 . . . . . . . . . . . . 13 (𝑆𝑉 → 0 ∈ ℤ)
91 nn0z 11653 . . . . . . . . . . . . 13 (𝐿 ∈ ℕ0𝐿 ∈ ℤ)
9290, 91anim12i 606 . . . . . . . . . . . 12 ((𝑆𝑉𝐿 ∈ ℕ0) → (0 ∈ ℤ ∧ 𝐿 ∈ ℤ))
93923ad2ant1 1163 . . . . . . . . . . 11 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) → (0 ∈ ℤ ∧ 𝐿 ∈ ℤ))
9493adantr 472 . . . . . . . . . 10 ((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) → (0 ∈ ℤ ∧ 𝐿 ∈ ℤ))
95 simpr 477 . . . . . . . . . 10 ((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) → 𝑀 < 𝑁)
96 ssfzo12bi 12778 . . . . . . . . . 10 (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ 𝑀 < 𝑁) → ((𝑀..^𝑁) ⊆ (0..^𝐿) ↔ (0 ≤ 𝑀𝑁𝐿)))
9789, 94, 95, 96syl3anc 1490 . . . . . . . . 9 ((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) → ((𝑀..^𝑁) ⊆ (0..^𝐿) ↔ (0 ≤ 𝑀𝑁𝐿)))
98 simpl1l 1293 . . . . . . . . . . . . . 14 ((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) → 𝑆𝑉)
9998ad2antrr 717 . . . . . . . . . . . . 13 ((((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀𝑁𝐿)) ∧ 𝑥 ∈ (0..^(𝑁𝑀))) → 𝑆𝑉)
100 simpl1r 1295 . . . . . . . . . . . . . 14 ((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) → 𝐿 ∈ ℕ0)
101100ad2antrr 717 . . . . . . . . . . . . 13 ((((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀𝑁𝐿)) ∧ 𝑥 ∈ (0..^(𝑁𝑀))) → 𝐿 ∈ ℕ0)
102 elfzonn0 12728 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (0..^(𝑁𝑀)) → 𝑥 ∈ ℕ0)
103 nn0addcl 11580 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ ℕ0𝑀 ∈ ℕ0) → (𝑥 + 𝑀) ∈ ℕ0)
104103expcom 402 . . . . . . . . . . . . . . . . . . 19 (𝑀 ∈ ℕ0 → (𝑥 ∈ ℕ0 → (𝑥 + 𝑀) ∈ ℕ0))
105104adantr 472 . . . . . . . . . . . . . . . . . 18 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (𝑥 ∈ ℕ0 → (𝑥 + 𝑀) ∈ ℕ0))
1061053ad2ant2 1164 . . . . . . . . . . . . . . . . 17 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) → (𝑥 ∈ ℕ0 → (𝑥 + 𝑀) ∈ ℕ0))
107106ad2antrr 717 . . . . . . . . . . . . . . . 16 (((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀𝑁𝐿)) → (𝑥 ∈ ℕ0 → (𝑥 + 𝑀) ∈ ℕ0))
108102, 107syl5com 31 . . . . . . . . . . . . . . 15 (𝑥 ∈ (0..^(𝑁𝑀)) → (((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀𝑁𝐿)) → (𝑥 + 𝑀) ∈ ℕ0))
109108impcom 396 . . . . . . . . . . . . . 14 ((((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀𝑁𝐿)) ∧ 𝑥 ∈ (0..^(𝑁𝑀))) → (𝑥 + 𝑀) ∈ ℕ0)
11091adantl 473 . . . . . . . . . . . . . . . . . 18 ((𝑆𝑉𝐿 ∈ ℕ0) → 𝐿 ∈ ℤ)
1111103ad2ant1 1163 . . . . . . . . . . . . . . . . 17 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) → 𝐿 ∈ ℤ)
112111adantr 472 . . . . . . . . . . . . . . . 16 ((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) → 𝐿 ∈ ℤ)
113 nn0re 11553 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐿 ∈ ℕ0𝐿 ∈ ℝ)
114113adantl 473 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑆𝑉𝐿 ∈ ℕ0) → 𝐿 ∈ ℝ)
115114, 57anim12ci 607 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) → ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝐿 ∈ ℝ))
116 df-3an 1109 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ) ↔ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝐿 ∈ ℝ))
117115, 116sylibr 225 . . . . . . . . . . . . . . . . . . . . 21 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) → (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ))
118 ltletr 10388 . . . . . . . . . . . . . . . . . . . . 21 ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ) → ((𝑀 < 𝑁𝑁𝐿) → 𝑀 < 𝐿))
119117, 118syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) → ((𝑀 < 𝑁𝑁𝐿) → 𝑀 < 𝐿))
120 elnn0z 11642 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑀 ∈ ℕ0 ↔ (𝑀 ∈ ℤ ∧ 0 ≤ 𝑀))
121 0red 10301 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑀 ∈ ℤ ∧ (𝑆𝑉𝐿 ∈ ℕ0)) → 0 ∈ ℝ)
122 zre 11633 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑀 ∈ ℤ → 𝑀 ∈ ℝ)
123122adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑀 ∈ ℤ ∧ (𝑆𝑉𝐿 ∈ ℕ0)) → 𝑀 ∈ ℝ)
124114adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑀 ∈ ℤ ∧ (𝑆𝑉𝐿 ∈ ℕ0)) → 𝐿 ∈ ℝ)
125 lelttr 10387 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((0 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ) → ((0 ≤ 𝑀𝑀 < 𝐿) → 0 < 𝐿))
126121, 123, 124, 125syl3anc 1490 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑀 ∈ ℤ ∧ (𝑆𝑉𝐿 ∈ ℕ0)) → ((0 ≤ 𝑀𝑀 < 𝐿) → 0 < 𝐿))
127126expd 404 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑀 ∈ ℤ ∧ (𝑆𝑉𝐿 ∈ ℕ0)) → (0 ≤ 𝑀 → (𝑀 < 𝐿 → 0 < 𝐿)))
128127impancom 443 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑀 ∈ ℤ ∧ 0 ≤ 𝑀) → ((𝑆𝑉𝐿 ∈ ℕ0) → (𝑀 < 𝐿 → 0 < 𝐿)))
129120, 128sylbi 208 . . . . . . . . . . . . . . . . . . . . . 22 (𝑀 ∈ ℕ0 → ((𝑆𝑉𝐿 ∈ ℕ0) → (𝑀 < 𝐿 → 0 < 𝐿)))
130129adantr 472 . . . . . . . . . . . . . . . . . . . . 21 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → ((𝑆𝑉𝐿 ∈ ℕ0) → (𝑀 < 𝐿 → 0 < 𝐿)))
131130impcom 396 . . . . . . . . . . . . . . . . . . . 20 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) → (𝑀 < 𝐿 → 0 < 𝐿))
132119, 131syld 47 . . . . . . . . . . . . . . . . . . 19 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) → ((𝑀 < 𝑁𝑁𝐿) → 0 < 𝐿))
133132expcomd 406 . . . . . . . . . . . . . . . . . 18 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) → (𝑁𝐿 → (𝑀 < 𝑁 → 0 < 𝐿)))
1341333impia 1145 . . . . . . . . . . . . . . . . 17 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) → (𝑀 < 𝑁 → 0 < 𝐿))
135134imp 395 . . . . . . . . . . . . . . . 16 ((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) → 0 < 𝐿)
136 elnnz 11639 . . . . . . . . . . . . . . . 16 (𝐿 ∈ ℕ ↔ (𝐿 ∈ ℤ ∧ 0 < 𝐿))
137112, 135, 136sylanbrc 578 . . . . . . . . . . . . . . 15 ((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) → 𝐿 ∈ ℕ)
138137ad2antrr 717 . . . . . . . . . . . . . 14 ((((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀𝑁𝐿)) ∧ 𝑥 ∈ (0..^(𝑁𝑀))) → 𝐿 ∈ ℕ)
139 elfzo0 12724 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (0..^(𝑁𝑀)) ↔ (𝑥 ∈ ℕ0 ∧ (𝑁𝑀) ∈ ℕ ∧ 𝑥 < (𝑁𝑀)))
140 nn0readdcl 11609 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑥 ∈ ℕ0𝑀 ∈ ℕ0) → (𝑥 + 𝑀) ∈ ℝ)
141140expcom 402 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑀 ∈ ℕ0 → (𝑥 ∈ ℕ0 → (𝑥 + 𝑀) ∈ ℝ))
142141ad2antrl 719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) → (𝑥 ∈ ℕ0 → (𝑥 + 𝑀) ∈ ℝ))
143142impcom 396 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → (𝑥 + 𝑀) ∈ ℝ)
14425adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → 𝑁 ∈ ℝ)
145144adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) → 𝑁 ∈ ℝ)
146145adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → 𝑁 ∈ ℝ)
147113ad2antrl 719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → 𝐿 ∈ ℝ)
148143, 146, 1473jca 1158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → ((𝑥 + 𝑀) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ))
149148ex 401 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 ∈ ℕ0 → ((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) → ((𝑥 + 𝑀) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ)))
150149adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥 ∈ ℕ0𝑥 < (𝑁𝑀)) → ((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) → ((𝑥 + 𝑀) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ)))
151150impcom 396 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) ∧ (𝑥 ∈ ℕ0𝑥 < (𝑁𝑀))) → ((𝑥 + 𝑀) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ))
152151adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) ∧ (𝑥 ∈ ℕ0𝑥 < (𝑁𝑀))) ∧ 𝑁𝐿) → ((𝑥 + 𝑀) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ))
153 nn0re 11553 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑥 ∈ ℕ0𝑥 ∈ ℝ)
154153adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → 𝑥 ∈ ℝ)
15524ad2antrl 719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) → 𝑀 ∈ ℝ)
156155adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → 𝑀 ∈ ℝ)
157154, 156, 146ltaddsubd 10886 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → ((𝑥 + 𝑀) < 𝑁𝑥 < (𝑁𝑀)))
158 idd 24 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) ∧ 𝑁𝐿) → ((𝑥 + 𝑀) < 𝑁 → (𝑥 + 𝑀) < 𝑁))
159158ex 401 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → (𝑁𝐿 → ((𝑥 + 𝑀) < 𝑁 → (𝑥 + 𝑀) < 𝑁)))
160159com23 86 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → ((𝑥 + 𝑀) < 𝑁 → (𝑁𝐿 → (𝑥 + 𝑀) < 𝑁)))
161157, 160sylbird 251 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → (𝑥 < (𝑁𝑀) → (𝑁𝐿 → (𝑥 + 𝑀) < 𝑁)))
162161impancom 443 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥 ∈ ℕ0𝑥 < (𝑁𝑀)) → ((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) → (𝑁𝐿 → (𝑥 + 𝑀) < 𝑁)))
163162impcom 396 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) ∧ (𝑥 ∈ ℕ0𝑥 < (𝑁𝑀))) → (𝑁𝐿 → (𝑥 + 𝑀) < 𝑁))
164163impac 548 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) ∧ (𝑥 ∈ ℕ0𝑥 < (𝑁𝑀))) ∧ 𝑁𝐿) → ((𝑥 + 𝑀) < 𝑁𝑁𝐿))
165 ltletr 10388 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑥 + 𝑀) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ) → (((𝑥 + 𝑀) < 𝑁𝑁𝐿) → (𝑥 + 𝑀) < 𝐿))
166152, 164, 165sylc 65 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) ∧ (𝑥 ∈ ℕ0𝑥 < (𝑁𝑀))) ∧ 𝑁𝐿) → (𝑥 + 𝑀) < 𝐿)
167166exp31 410 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) → ((𝑥 ∈ ℕ0𝑥 < (𝑁𝑀)) → (𝑁𝐿 → (𝑥 + 𝑀) < 𝐿)))
168167com23 86 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) → (𝑁𝐿 → ((𝑥 ∈ ℕ0𝑥 < (𝑁𝑀)) → (𝑥 + 𝑀) < 𝐿)))
169168ex 401 . . . . . . . . . . . . . . . . . . . . 21 (𝐿 ∈ ℕ0 → ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (𝑁𝐿 → ((𝑥 ∈ ℕ0𝑥 < (𝑁𝑀)) → (𝑥 + 𝑀) < 𝐿))))
170169adantl 473 . . . . . . . . . . . . . . . . . . . 20 ((𝑆𝑉𝐿 ∈ ℕ0) → ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (𝑁𝐿 → ((𝑥 ∈ ℕ0𝑥 < (𝑁𝑀)) → (𝑥 + 𝑀) < 𝐿))))
1711703imp 1137 . . . . . . . . . . . . . . . . . . 19 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) → ((𝑥 ∈ ℕ0𝑥 < (𝑁𝑀)) → (𝑥 + 𝑀) < 𝐿))
172171ad2antrr 717 . . . . . . . . . . . . . . . . . 18 (((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀𝑁𝐿)) → ((𝑥 ∈ ℕ0𝑥 < (𝑁𝑀)) → (𝑥 + 𝑀) < 𝐿))
173172com12 32 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ℕ0𝑥 < (𝑁𝑀)) → (((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀𝑁𝐿)) → (𝑥 + 𝑀) < 𝐿))
1741733adant2 1161 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℕ0 ∧ (𝑁𝑀) ∈ ℕ ∧ 𝑥 < (𝑁𝑀)) → (((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀𝑁𝐿)) → (𝑥 + 𝑀) < 𝐿))
175139, 174sylbi 208 . . . . . . . . . . . . . . 15 (𝑥 ∈ (0..^(𝑁𝑀)) → (((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀𝑁𝐿)) → (𝑥 + 𝑀) < 𝐿))
176175impcom 396 . . . . . . . . . . . . . 14 ((((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀𝑁𝐿)) ∧ 𝑥 ∈ (0..^(𝑁𝑀))) → (𝑥 + 𝑀) < 𝐿)
177 elfzo0 12724 . . . . . . . . . . . . . 14 ((𝑥 + 𝑀) ∈ (0..^𝐿) ↔ ((𝑥 + 𝑀) ∈ ℕ0𝐿 ∈ ℕ ∧ (𝑥 + 𝑀) < 𝐿))
178109, 138, 176, 177syl3anbrc 1443 . . . . . . . . . . . . 13 ((((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀𝑁𝐿)) ∧ 𝑥 ∈ (0..^(𝑁𝑀))) → (𝑥 + 𝑀) ∈ (0..^𝐿))
179 repswsymb 13814 . . . . . . . . . . . . 13 ((𝑆𝑉𝐿 ∈ ℕ0 ∧ (𝑥 + 𝑀) ∈ (0..^𝐿)) → ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀)) = 𝑆)
18099, 101, 178, 179syl3anc 1490 . . . . . . . . . . . 12 ((((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀𝑁𝐿)) ∧ 𝑥 ∈ (0..^(𝑁𝑀))) → ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀)) = 𝑆)
181180mpteq2dva 4905 . . . . . . . . . . 11 (((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀𝑁𝐿)) → (𝑥 ∈ (0..^(𝑁𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))) = (𝑥 ∈ (0..^(𝑁𝑀)) ↦ 𝑆))
182333ad2ant2 1164 . . . . . . . . . . . . . . . 16 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) → (𝑁𝑀) ∈ ℤ)
183182adantr 472 . . . . . . . . . . . . . . 15 ((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) → (𝑁𝑀) ∈ ℤ)
184573ad2ant2 1164 . . . . . . . . . . . . . . . . . 18 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) → (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ))
185 ltle 10385 . . . . . . . . . . . . . . . . . 18 ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑀 < 𝑁𝑀𝑁))
186184, 185syl 17 . . . . . . . . . . . . . . . . 17 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) → (𝑀 < 𝑁𝑀𝑁))
187263ad2ant2 1164 . . . . . . . . . . . . . . . . . 18 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) → (𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ))
188187, 55syl 17 . . . . . . . . . . . . . . . . 17 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) → (0 ≤ (𝑁𝑀) ↔ 𝑀𝑁))
189186, 188sylibrd 250 . . . . . . . . . . . . . . . 16 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) → (𝑀 < 𝑁 → 0 ≤ (𝑁𝑀)))
190189imp 395 . . . . . . . . . . . . . . 15 ((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) → 0 ≤ (𝑁𝑀))
191183, 190, 54sylanbrc 578 . . . . . . . . . . . . . 14 ((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) → (𝑁𝑀) ∈ ℕ0)
19298, 191jca 507 . . . . . . . . . . . . 13 ((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) → (𝑆𝑉 ∧ (𝑁𝑀) ∈ ℕ0))
193192adantr 472 . . . . . . . . . . . 12 (((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀𝑁𝐿)) → (𝑆𝑉 ∧ (𝑁𝑀) ∈ ℕ0))
194 reps 13810 . . . . . . . . . . . . 13 ((𝑆𝑉 ∧ (𝑁𝑀) ∈ ℕ0) → (𝑆 repeatS (𝑁𝑀)) = (𝑥 ∈ (0..^(𝑁𝑀)) ↦ 𝑆))
195194eqcomd 2771 . . . . . . . . . . . 12 ((𝑆𝑉 ∧ (𝑁𝑀) ∈ ℕ0) → (𝑥 ∈ (0..^(𝑁𝑀)) ↦ 𝑆) = (𝑆 repeatS (𝑁𝑀)))
196193, 195syl 17 . . . . . . . . . . 11 (((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀𝑁𝐿)) → (𝑥 ∈ (0..^(𝑁𝑀)) ↦ 𝑆) = (𝑆 repeatS (𝑁𝑀)))
197181, 196eqtrd 2799 . . . . . . . . . 10 (((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀𝑁𝐿)) → (𝑥 ∈ (0..^(𝑁𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))) = (𝑆 repeatS (𝑁𝑀)))
198197ex 401 . . . . . . . . 9 ((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) → ((0 ≤ 𝑀𝑁𝐿) → (𝑥 ∈ (0..^(𝑁𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))) = (𝑆 repeatS (𝑁𝑀))))
19997, 198sylbid 231 . . . . . . . 8 ((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) → ((𝑀..^𝑁) ⊆ (0..^𝐿) → (𝑥 ∈ (0..^(𝑁𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))) = (𝑆 repeatS (𝑁𝑀))))
200199impcom 396 . . . . . . 7 (((𝑀..^𝑁) ⊆ (0..^𝐿) ∧ (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁)) → (𝑥 ∈ (0..^(𝑁𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))) = (𝑆 repeatS (𝑁𝑀)))
20187, 200eqtrd 2799 . . . . . 6 (((𝑀..^𝑁) ⊆ (0..^𝐿) ∧ (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁)) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁𝑀)))
202 iffalse 4254 . . . . . . . 8 (¬ (𝑀..^𝑁) ⊆ (0..^𝐿) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = ∅)
203202adantr 472 . . . . . . 7 ((¬ (𝑀..^𝑁) ⊆ (0..^𝐿) ∧ (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁)) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = ∅)
20497notbid 309 . . . . . . . . 9 ((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) → (¬ (𝑀..^𝑁) ⊆ (0..^𝐿) ↔ ¬ (0 ≤ 𝑀𝑁𝐿)))
205 ianor 1004 . . . . . . . . . . 11 (¬ (0 ≤ 𝑀𝑁𝐿) ↔ (¬ 0 ≤ 𝑀 ∨ ¬ 𝑁𝐿))
206 nn0ge0 11570 . . . . . . . . . . . . . . . . 17 (𝑀 ∈ ℕ0 → 0 ≤ 𝑀)
207 pm2.24 122 . . . . . . . . . . . . . . . . 17 (0 ≤ 𝑀 → (¬ 0 ≤ 𝑀 → (𝑆 repeatS (𝑁𝑀)) = ∅))
208206, 207syl 17 . . . . . . . . . . . . . . . 16 (𝑀 ∈ ℕ0 → (¬ 0 ≤ 𝑀 → (𝑆 repeatS (𝑁𝑀)) = ∅))
209208adantr 472 . . . . . . . . . . . . . . 15 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (¬ 0 ≤ 𝑀 → (𝑆 repeatS (𝑁𝑀)) = ∅))
2102093ad2ant2 1164 . . . . . . . . . . . . . 14 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) → (¬ 0 ≤ 𝑀 → (𝑆 repeatS (𝑁𝑀)) = ∅))
211210adantr 472 . . . . . . . . . . . . 13 ((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) → (¬ 0 ≤ 𝑀 → (𝑆 repeatS (𝑁𝑀)) = ∅))
212211com12 32 . . . . . . . . . . . 12 (¬ 0 ≤ 𝑀 → ((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) → (𝑆 repeatS (𝑁𝑀)) = ∅))
213 pm2.24 122 . . . . . . . . . . . . . . 15 (𝑁𝐿 → (¬ 𝑁𝐿 → (𝑆 repeatS (𝑁𝑀)) = ∅))
2142133ad2ant3 1165 . . . . . . . . . . . . . 14 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) → (¬ 𝑁𝐿 → (𝑆 repeatS (𝑁𝑀)) = ∅))
215214adantr 472 . . . . . . . . . . . . 13 ((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) → (¬ 𝑁𝐿 → (𝑆 repeatS (𝑁𝑀)) = ∅))
216215com12 32 . . . . . . . . . . . 12 𝑁𝐿 → ((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) → (𝑆 repeatS (𝑁𝑀)) = ∅))
217212, 216jaoi 883 . . . . . . . . . . 11 ((¬ 0 ≤ 𝑀 ∨ ¬ 𝑁𝐿) → ((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) → (𝑆 repeatS (𝑁𝑀)) = ∅))
218205, 217sylbi 208 . . . . . . . . . 10 (¬ (0 ≤ 𝑀𝑁𝐿) → ((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) → (𝑆 repeatS (𝑁𝑀)) = ∅))
219218com12 32 . . . . . . . . 9 ((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) → (¬ (0 ≤ 𝑀𝑁𝐿) → (𝑆 repeatS (𝑁𝑀)) = ∅))
220204, 219sylbid 231 . . . . . . . 8 ((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) → (¬ (𝑀..^𝑁) ⊆ (0..^𝐿) → (𝑆 repeatS (𝑁𝑀)) = ∅))
221220impcom 396 . . . . . . 7 ((¬ (𝑀..^𝑁) ⊆ (0..^𝐿) ∧ (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁)) → (𝑆 repeatS (𝑁𝑀)) = ∅)
222203, 221eqtr4d 2802 . . . . . 6 ((¬ (𝑀..^𝑁) ⊆ (0..^𝐿) ∧ (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁)) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁𝑀)))
223201, 222pm2.61ian 846 . . . . 5 ((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁𝑀)))
224223ex 401 . . . 4 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) → (𝑀 < 𝑁 → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁𝑀))))
22586, 224sylbid 231 . . 3 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) → (¬ 𝑁𝑀 → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁𝑀))))
22682, 225pm2.61d 171 . 2 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁𝑀)))
22710, 15, 2263eqtrd 2803 1 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) → ((𝑆 repeatS 𝐿) substr ⟨𝑀, 𝑁⟩) = (𝑆 repeatS (𝑁𝑀)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 873  w3a 1107   = wceq 1652  wcel 2155  wnel 3040  wss 3734  c0 4081  ifcif 4245  cop 4342   class class class wbr 4811  cmpt 4890  dom cdm 5279  wf 6066  cfv 6070  (class class class)co 6846  cc 10191  cr 10192  0cc0 10193   + caddc 10196   < clt 10332  cle 10333  cmin 10525  cn 11279  0cn0 11543  cz 11629  ..^cfzo 12680  Word cword 13493   substr csubstr 13624   repeatS creps 13808
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4932  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7151  ax-cnex 10249  ax-resscn 10250  ax-1cn 10251  ax-icn 10252  ax-addcl 10253  ax-addrcl 10254  ax-mulcl 10255  ax-mulrcl 10256  ax-mulcom 10257  ax-addass 10258  ax-mulass 10259  ax-distr 10260  ax-i2m1 10261  ax-1ne0 10262  ax-1rid 10263  ax-rnegex 10264  ax-rrecex 10265  ax-cnre 10266  ax-pre-lttri 10267  ax-pre-lttrn 10268  ax-pre-ltadd 10269  ax-pre-mulgt0 10270
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-pss 3750  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-tp 4341  df-op 4343  df-uni 4597  df-int 4636  df-iun 4680  df-br 4812  df-opab 4874  df-mpt 4891  df-tr 4914  df-id 5187  df-eprel 5192  df-po 5200  df-so 5201  df-fr 5238  df-we 5240  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-pred 5867  df-ord 5913  df-on 5914  df-lim 5915  df-suc 5916  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078  df-riota 6807  df-ov 6849  df-oprab 6850  df-mpt2 6851  df-om 7268  df-1st 7370  df-2nd 7371  df-wrecs 7614  df-recs 7676  df-rdg 7714  df-1o 7768  df-er 7951  df-en 8165  df-dom 8166  df-sdom 8167  df-fin 8168  df-card 9020  df-pnf 10334  df-mnf 10335  df-xr 10336  df-ltxr 10337  df-le 10338  df-sub 10527  df-neg 10528  df-nn 11280  df-n0 11544  df-z 11630  df-uz 11894  df-fz 12541  df-fzo 12681  df-hash 13329  df-word 13494  df-substr 13625  df-reps 13809
This theorem is referenced by:  repswcshw  13857
  Copyright terms: Public domain W3C validator