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

Theorem repswswrd 14138
Description: A subword of a "repeated symbol word" is again a "repeated symbol word". The assumption 𝑁𝐿 is required, because otherwise (𝐿 < 𝑁): ((𝑆 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 14129 . . . . . 6 ((𝑆𝑉𝐿 ∈ ℕ0) → (𝑆 repeatS 𝐿) ∈ Word 𝑉)
2 nn0z 11997 . . . . . . 7 (𝑀 ∈ ℕ0𝑀 ∈ ℤ)
3 nn0z 11997 . . . . . . 7 (𝑁 ∈ ℕ0𝑁 ∈ ℤ)
42, 3anim12i 614 . . . . . 6 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
51, 4anim12i 614 . . . . 5 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) → ((𝑆 repeatS 𝐿) ∈ Word 𝑉 ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)))
6 3anass 1089 . . . . 5 (((𝑆 repeatS 𝐿) ∈ Word 𝑉𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ↔ ((𝑆 repeatS 𝐿) ∈ Word 𝑉 ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)))
75, 6sylibr 236 . . . 4 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) → ((𝑆 repeatS 𝐿) ∈ Word 𝑉𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
873adant3 1126 . . 3 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) → ((𝑆 repeatS 𝐿) ∈ Word 𝑉𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
9 swrdval 13997 . . 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 14127 . . . . . 6 ((𝑆𝑉𝐿 ∈ ℕ0) → (𝑆 repeatS 𝐿):(0..^𝐿)⟶𝑉)
12113ad2ant1 1127 . . . . 5 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) → (𝑆 repeatS 𝐿):(0..^𝐿)⟶𝑉)
1312fdmd 6516 . . . 4 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) → dom (𝑆 repeatS 𝐿) = (0..^𝐿))
1413sseq2d 3997 . . 3 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) → ((𝑀..^𝑁) ⊆ dom (𝑆 repeatS 𝐿) ↔ (𝑀..^𝑁) ⊆ (0..^𝐿)))
1514ifbid 4487 . 2 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) → if((𝑀..^𝑁) ⊆ dom (𝑆 repeatS 𝐿), (𝑥 ∈ (0..^(𝑁𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅))
16 fzon 13050 . . . . . . . . . . 11 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁𝑀 ↔ (𝑀..^𝑁) = ∅))
174, 16syl 17 . . . . . . . . . 10 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (𝑁𝑀 ↔ (𝑀..^𝑁) = ∅))
1817adantl 484 . . . . . . . . 9 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) → (𝑁𝑀 ↔ (𝑀..^𝑁) = ∅))
1918biimpac 481 . . . . . . . 8 ((𝑁𝑀 ∧ ((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → (𝑀..^𝑁) = ∅)
20 0ss 4348 . . . . . . . 8 ∅ ⊆ (0..^𝐿)
2119, 20eqsstrdi 4019 . . . . . . 7 ((𝑁𝑀 ∧ ((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → (𝑀..^𝑁) ⊆ (0..^𝐿))
22 iftrue 4471 . . . . . . 7 ((𝑀..^𝑁) ⊆ (0..^𝐿) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑥 ∈ (0..^(𝑁𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))))
2321, 22syl 17 . . . . . 6 ((𝑁𝑀 ∧ ((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑥 ∈ (0..^(𝑁𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))))
24 nn0re 11898 . . . . . . . . . . . 12 (𝑀 ∈ ℕ0𝑀 ∈ ℝ)
25 nn0re 11898 . . . . . . . . . . . 12 (𝑁 ∈ ℕ0𝑁 ∈ ℝ)
2624, 25anim12ci 615 . . . . . . . . . . 11 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ))
2726adantl 484 . . . . . . . . . 10 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) → (𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ))
28 suble0 11146 . . . . . . . . . 10 ((𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ) → ((𝑁𝑀) ≤ 0 ↔ 𝑁𝑀))
2927, 28syl 17 . . . . . . . . 9 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) → ((𝑁𝑀) ≤ 0 ↔ 𝑁𝑀))
3029biimparc 482 . . . . . . . 8 ((𝑁𝑀 ∧ ((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → (𝑁𝑀) ≤ 0)
31 0z 11984 . . . . . . . . 9 0 ∈ ℤ
32 zsubcl 12016 . . . . . . . . . . . 12 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑁𝑀) ∈ ℤ)
333, 2, 32syl2anr 598 . . . . . . . . . . 11 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (𝑁𝑀) ∈ ℤ)
3433adantl 484 . . . . . . . . . 10 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) → (𝑁𝑀) ∈ ℤ)
3534adantl 484 . . . . . . . . 9 ((𝑁𝑀 ∧ ((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → (𝑁𝑀) ∈ ℤ)
36 fzon 13050 . . . . . . . . 9 ((0 ∈ ℤ ∧ (𝑁𝑀) ∈ ℤ) → ((𝑁𝑀) ≤ 0 ↔ (0..^(𝑁𝑀)) = ∅))
3731, 35, 36sylancr 589 . . . . . . . 8 ((𝑁𝑀 ∧ ((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → ((𝑁𝑀) ≤ 0 ↔ (0..^(𝑁𝑀)) = ∅))
3830, 37mpbid 234 . . . . . . 7 ((𝑁𝑀 ∧ ((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → (0..^(𝑁𝑀)) = ∅)
3938mpteq1d 5146 . . . . . 6 ((𝑁𝑀 ∧ ((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → (𝑥 ∈ (0..^(𝑁𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))) = (𝑥 ∈ ∅ ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))))
40 oveq2 7156 . . . . . . . . . . . . 13 (𝑀 = 𝑁 → (𝑁𝑀) = (𝑁𝑁))
4140oveq2d 7164 . . . . . . . . . . . 12 (𝑀 = 𝑁 → (𝑆 repeatS (𝑁𝑀)) = (𝑆 repeatS (𝑁𝑁)))
42 nn0cn 11899 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ0𝑁 ∈ ℂ)
4342adantl 484 . . . . . . . . . . . . . . . 16 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → 𝑁 ∈ ℂ)
4443subidd 10977 . . . . . . . . . . . . . . 15 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (𝑁𝑁) = 0)
4544adantl 484 . . . . . . . . . . . . . 14 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) → (𝑁𝑁) = 0)
4645oveq2d 7164 . . . . . . . . . . . . 13 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) → (𝑆 repeatS (𝑁𝑁)) = (𝑆 repeatS 0))
47 repsw0 14131 . . . . . . . . . . . . . 14 (𝑆𝑉 → (𝑆 repeatS 0) = ∅)
4847ad2antrr 724 . . . . . . . . . . . . 13 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) → (𝑆 repeatS 0) = ∅)
4946, 48eqtrd 2854 . . . . . . . . . . . 12 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) → (𝑆 repeatS (𝑁𝑁)) = ∅)
5041, 49sylan9eqr 2876 . . . . . . . . . . 11 ((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) ∧ 𝑀 = 𝑁) → (𝑆 repeatS (𝑁𝑀)) = ∅)
5150ex 415 . . . . . . . . . 10 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) → (𝑀 = 𝑁 → (𝑆 repeatS (𝑁𝑀)) = ∅))
5251adantl 484 . . . . . . . . 9 ((𝑁𝑀 ∧ ((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → (𝑀 = 𝑁 → (𝑆 repeatS (𝑁𝑀)) = ∅))
5352com12 32 . . . . . . . 8 (𝑀 = 𝑁 → ((𝑁𝑀 ∧ ((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → (𝑆 repeatS (𝑁𝑀)) = ∅))
54 elnn0z 11986 . . . . . . . . . . . . . . 15 ((𝑁𝑀) ∈ ℕ0 ↔ ((𝑁𝑀) ∈ ℤ ∧ 0 ≤ (𝑁𝑀)))
55 subge0 11145 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ) → (0 ≤ (𝑁𝑀) ↔ 𝑀𝑁))
5625, 24, 55syl2anr 598 . . . . . . . . . . . . . . . . . . . 20 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (0 ≤ (𝑁𝑀) ↔ 𝑀𝑁))
5724, 25anim12i 614 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ))
58 letri3 10718 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑀 = 𝑁 ↔ (𝑀𝑁𝑁𝑀)))
5957, 58syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (𝑀 = 𝑁 ↔ (𝑀𝑁𝑁𝑀)))
6059biimprd 250 . . . . . . . . . . . . . . . . . . . . 21 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → ((𝑀𝑁𝑁𝑀) → 𝑀 = 𝑁))
6160expd 418 . . . . . . . . . . . . . . . . . . . 20 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (𝑀𝑁 → (𝑁𝑀𝑀 = 𝑁)))
6256, 61sylbid 242 . . . . . . . . . . . . . . . . . . 19 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (0 ≤ (𝑁𝑀) → (𝑁𝑀𝑀 = 𝑁)))
6362com23 86 . . . . . . . . . . . . . . . . . 18 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (𝑁𝑀 → (0 ≤ (𝑁𝑀) → 𝑀 = 𝑁)))
6463adantl 484 . . . . . . . . . . . . . . . . 17 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) → (𝑁𝑀 → (0 ≤ (𝑁𝑀) → 𝑀 = 𝑁)))
6564impcom 410 . . . . . . . . . . . . . . . 16 ((𝑁𝑀 ∧ ((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → (0 ≤ (𝑁𝑀) → 𝑀 = 𝑁))
6665com12 32 . . . . . . . . . . . . . . 15 (0 ≤ (𝑁𝑀) → ((𝑁𝑀 ∧ ((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → 𝑀 = 𝑁))
6754, 66simplbiim 507 . . . . . . . . . . . . . 14 ((𝑁𝑀) ∈ ℕ0 → ((𝑁𝑀 ∧ ((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → 𝑀 = 𝑁))
6867com12 32 . . . . . . . . . . . . 13 ((𝑁𝑀 ∧ ((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → ((𝑁𝑀) ∈ ℕ0𝑀 = 𝑁))
6968con3d 155 . . . . . . . . . . . 12 ((𝑁𝑀 ∧ ((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → (¬ 𝑀 = 𝑁 → ¬ (𝑁𝑀) ∈ ℕ0))
7069impcom 410 . . . . . . . . . . 11 ((¬ 𝑀 = 𝑁 ∧ (𝑁𝑀 ∧ ((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)))) → ¬ (𝑁𝑀) ∈ ℕ0)
71 df-nel 3122 . . . . . . . . . . 11 ((𝑁𝑀) ∉ ℕ0 ↔ ¬ (𝑁𝑀) ∈ ℕ0)
7270, 71sylibr 236 . . . . . . . . . 10 ((¬ 𝑀 = 𝑁 ∧ (𝑁𝑀 ∧ ((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)))) → (𝑁𝑀) ∉ ℕ0)
73 repsundef 14125 . . . . . . . . . 10 ((𝑁𝑀) ∉ ℕ0 → (𝑆 repeatS (𝑁𝑀)) = ∅)
7472, 73syl 17 . . . . . . . . 9 ((¬ 𝑀 = 𝑁 ∧ (𝑁𝑀 ∧ ((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)))) → (𝑆 repeatS (𝑁𝑀)) = ∅)
7574ex 415 . . . . . . . 8 𝑀 = 𝑁 → ((𝑁𝑀 ∧ ((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → (𝑆 repeatS (𝑁𝑀)) = ∅))
7653, 75pm2.61i 183 . . . . . . 7 ((𝑁𝑀 ∧ ((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → (𝑆 repeatS (𝑁𝑀)) = ∅)
77 mpt0 6483 . . . . . . 7 (𝑥 ∈ ∅ ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))) = ∅
7876, 77syl6reqr 2873 . . . . . 6 ((𝑁𝑀 ∧ ((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → (𝑥 ∈ ∅ ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))) = (𝑆 repeatS (𝑁𝑀)))
7923, 39, 783eqtrd 2858 . . . . 5 ((𝑁𝑀 ∧ ((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁𝑀)))
8079expcom 416 . . . 4 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) → (𝑁𝑀 → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁𝑀))))
81803adant3 1126 . . 3 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) → (𝑁𝑀 → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁𝑀))))
82 ltnle 10712 . . . . . . 7 ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑀 < 𝑁 ↔ ¬ 𝑁𝑀))
8357, 82syl 17 . . . . . 6 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (𝑀 < 𝑁 ↔ ¬ 𝑁𝑀))
8483bicomd 225 . . . . 5 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (¬ 𝑁𝑀𝑀 < 𝑁))
85843ad2ant2 1128 . . . 4 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) → (¬ 𝑁𝑀𝑀 < 𝑁))
8622adantr 483 . . . . . . 7 (((𝑀..^𝑁) ⊆ (0..^𝐿) ∧ (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁)) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑥 ∈ (0..^(𝑁𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))))
8743ad2ant2 1128 . . . . . . . . . . 11 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
8887adantr 483 . . . . . . . . . 10 ((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
89 0zd 11985 . . . . . . . . . . . . 13 (𝑆𝑉 → 0 ∈ ℤ)
90 nn0z 11997 . . . . . . . . . . . . 13 (𝐿 ∈ ℕ0𝐿 ∈ ℤ)
9189, 90anim12i 614 . . . . . . . . . . . 12 ((𝑆𝑉𝐿 ∈ ℕ0) → (0 ∈ ℤ ∧ 𝐿 ∈ ℤ))
92913ad2ant1 1127 . . . . . . . . . . 11 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) → (0 ∈ ℤ ∧ 𝐿 ∈ ℤ))
9392adantr 483 . . . . . . . . . 10 ((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) → (0 ∈ ℤ ∧ 𝐿 ∈ ℤ))
94 simpr 487 . . . . . . . . . 10 ((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) → 𝑀 < 𝑁)
95 ssfzo12bi 13124 . . . . . . . . . 10 (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (0 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ 𝑀 < 𝑁) → ((𝑀..^𝑁) ⊆ (0..^𝐿) ↔ (0 ≤ 𝑀𝑁𝐿)))
9688, 93, 94, 95syl3anc 1365 . . . . . . . . 9 ((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) → ((𝑀..^𝑁) ⊆ (0..^𝐿) ↔ (0 ≤ 𝑀𝑁𝐿)))
97 simpl1l 1218 . . . . . . . . . . . . . 14 ((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) → 𝑆𝑉)
9897ad2antrr 724 . . . . . . . . . . . . 13 ((((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀𝑁𝐿)) ∧ 𝑥 ∈ (0..^(𝑁𝑀))) → 𝑆𝑉)
99 simpl1r 1219 . . . . . . . . . . . . . 14 ((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) → 𝐿 ∈ ℕ0)
10099ad2antrr 724 . . . . . . . . . . . . 13 ((((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀𝑁𝐿)) ∧ 𝑥 ∈ (0..^(𝑁𝑀))) → 𝐿 ∈ ℕ0)
101 nn0addcl 11924 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ ℕ0𝑀 ∈ ℕ0) → (𝑥 + 𝑀) ∈ ℕ0)
102101expcom 416 . . . . . . . . . . . . . . . . . 18 (𝑀 ∈ ℕ0 → (𝑥 ∈ ℕ0 → (𝑥 + 𝑀) ∈ ℕ0))
103102adantr 483 . . . . . . . . . . . . . . . . 17 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (𝑥 ∈ ℕ0 → (𝑥 + 𝑀) ∈ ℕ0))
1041033ad2ant2 1128 . . . . . . . . . . . . . . . 16 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) → (𝑥 ∈ ℕ0 → (𝑥 + 𝑀) ∈ ℕ0))
105104ad2antrr 724 . . . . . . . . . . . . . . 15 (((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀𝑁𝐿)) → (𝑥 ∈ ℕ0 → (𝑥 + 𝑀) ∈ ℕ0))
106 elfzonn0 13074 . . . . . . . . . . . . . . 15 (𝑥 ∈ (0..^(𝑁𝑀)) → 𝑥 ∈ ℕ0)
107105, 106impel 508 . . . . . . . . . . . . . 14 ((((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀𝑁𝐿)) ∧ 𝑥 ∈ (0..^(𝑁𝑀))) → (𝑥 + 𝑀) ∈ ℕ0)
10890adantl 484 . . . . . . . . . . . . . . . . . 18 ((𝑆𝑉𝐿 ∈ ℕ0) → 𝐿 ∈ ℤ)
1091083ad2ant1 1127 . . . . . . . . . . . . . . . . 17 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) → 𝐿 ∈ ℤ)
110109adantr 483 . . . . . . . . . . . . . . . 16 ((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) → 𝐿 ∈ ℤ)
111 nn0re 11898 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐿 ∈ ℕ0𝐿 ∈ ℝ)
112111adantl 484 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑆𝑉𝐿 ∈ ℕ0) → 𝐿 ∈ ℝ)
113112, 57anim12ci 615 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) → ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝐿 ∈ ℝ))
114 df-3an 1083 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ) ↔ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝐿 ∈ ℝ))
115113, 114sylibr 236 . . . . . . . . . . . . . . . . . . . . 21 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) → (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ))
116 ltletr 10724 . . . . . . . . . . . . . . . . . . . . 21 ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ) → ((𝑀 < 𝑁𝑁𝐿) → 𝑀 < 𝐿))
117115, 116syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) → ((𝑀 < 𝑁𝑁𝐿) → 𝑀 < 𝐿))
118 elnn0z 11986 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑀 ∈ ℕ0 ↔ (𝑀 ∈ ℤ ∧ 0 ≤ 𝑀))
119 0red 10636 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑀 ∈ ℤ ∧ (𝑆𝑉𝐿 ∈ ℕ0)) → 0 ∈ ℝ)
120 zre 11977 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑀 ∈ ℤ → 𝑀 ∈ ℝ)
121120adantr 483 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑀 ∈ ℤ ∧ (𝑆𝑉𝐿 ∈ ℕ0)) → 𝑀 ∈ ℝ)
122112adantl 484 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑀 ∈ ℤ ∧ (𝑆𝑉𝐿 ∈ ℕ0)) → 𝐿 ∈ ℝ)
123 lelttr 10723 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((0 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ) → ((0 ≤ 𝑀𝑀 < 𝐿) → 0 < 𝐿))
124119, 121, 122, 123syl3anc 1365 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑀 ∈ ℤ ∧ (𝑆𝑉𝐿 ∈ ℕ0)) → ((0 ≤ 𝑀𝑀 < 𝐿) → 0 < 𝐿))
125124expd 418 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑀 ∈ ℤ ∧ (𝑆𝑉𝐿 ∈ ℕ0)) → (0 ≤ 𝑀 → (𝑀 < 𝐿 → 0 < 𝐿)))
126125impancom 454 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑀 ∈ ℤ ∧ 0 ≤ 𝑀) → ((𝑆𝑉𝐿 ∈ ℕ0) → (𝑀 < 𝐿 → 0 < 𝐿)))
127118, 126sylbi 219 . . . . . . . . . . . . . . . . . . . . . 22 (𝑀 ∈ ℕ0 → ((𝑆𝑉𝐿 ∈ ℕ0) → (𝑀 < 𝐿 → 0 < 𝐿)))
128127adantr 483 . . . . . . . . . . . . . . . . . . . . 21 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → ((𝑆𝑉𝐿 ∈ ℕ0) → (𝑀 < 𝐿 → 0 < 𝐿)))
129128impcom 410 . . . . . . . . . . . . . . . . . . . 20 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) → (𝑀 < 𝐿 → 0 < 𝐿))
130117, 129syld 47 . . . . . . . . . . . . . . . . . . 19 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) → ((𝑀 < 𝑁𝑁𝐿) → 0 < 𝐿))
131130expcomd 419 . . . . . . . . . . . . . . . . . 18 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) → (𝑁𝐿 → (𝑀 < 𝑁 → 0 < 𝐿)))
1321313impia 1111 . . . . . . . . . . . . . . . . 17 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) → (𝑀 < 𝑁 → 0 < 𝐿))
133132imp 409 . . . . . . . . . . . . . . . 16 ((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) → 0 < 𝐿)
134 elnnz 11983 . . . . . . . . . . . . . . . 16 (𝐿 ∈ ℕ ↔ (𝐿 ∈ ℤ ∧ 0 < 𝐿))
135110, 133, 134sylanbrc 585 . . . . . . . . . . . . . . 15 ((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) → 𝐿 ∈ ℕ)
136135ad2antrr 724 . . . . . . . . . . . . . 14 ((((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀𝑁𝐿)) ∧ 𝑥 ∈ (0..^(𝑁𝑀))) → 𝐿 ∈ ℕ)
137 elfzo0 13070 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (0..^(𝑁𝑀)) ↔ (𝑥 ∈ ℕ0 ∧ (𝑁𝑀) ∈ ℕ ∧ 𝑥 < (𝑁𝑀)))
138 nn0readdcl 11953 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑥 ∈ ℕ0𝑀 ∈ ℕ0) → (𝑥 + 𝑀) ∈ ℝ)
139138expcom 416 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑀 ∈ ℕ0 → (𝑥 ∈ ℕ0 → (𝑥 + 𝑀) ∈ ℝ))
140139ad2antrl 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) → (𝑥 ∈ ℕ0 → (𝑥 + 𝑀) ∈ ℝ))
141140impcom 410 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → (𝑥 + 𝑀) ∈ ℝ)
14225adantl 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → 𝑁 ∈ ℝ)
143142adantl 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) → 𝑁 ∈ ℝ)
144143adantl 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → 𝑁 ∈ ℝ)
145111ad2antrl 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → 𝐿 ∈ ℝ)
146141, 144, 1453jca 1122 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → ((𝑥 + 𝑀) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ))
147146ex 415 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 ∈ ℕ0 → ((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) → ((𝑥 + 𝑀) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ)))
148147adantr 483 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥 ∈ ℕ0𝑥 < (𝑁𝑀)) → ((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) → ((𝑥 + 𝑀) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ)))
149148impcom 410 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) ∧ (𝑥 ∈ ℕ0𝑥 < (𝑁𝑀))) → ((𝑥 + 𝑀) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ))
150149adantr 483 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) ∧ (𝑥 ∈ ℕ0𝑥 < (𝑁𝑀))) ∧ 𝑁𝐿) → ((𝑥 + 𝑀) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ))
151 nn0re 11898 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑥 ∈ ℕ0𝑥 ∈ ℝ)
152151adantr 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → 𝑥 ∈ ℝ)
15324ad2antrl 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) → 𝑀 ∈ ℝ)
154153adantl 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → 𝑀 ∈ ℝ)
155152, 154, 144ltaddsubd 11232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → ((𝑥 + 𝑀) < 𝑁𝑥 < (𝑁𝑀)))
156 idd 24 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) ∧ 𝑁𝐿) → ((𝑥 + 𝑀) < 𝑁 → (𝑥 + 𝑀) < 𝑁))
157156ex 415 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → (𝑁𝐿 → ((𝑥 + 𝑀) < 𝑁 → (𝑥 + 𝑀) < 𝑁)))
158157com23 86 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → ((𝑥 + 𝑀) < 𝑁 → (𝑁𝐿 → (𝑥 + 𝑀) < 𝑁)))
159155, 158sylbird 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑥 ∈ ℕ0 ∧ (𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0))) → (𝑥 < (𝑁𝑀) → (𝑁𝐿 → (𝑥 + 𝑀) < 𝑁)))
160159impancom 454 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥 ∈ ℕ0𝑥 < (𝑁𝑀)) → ((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) → (𝑁𝐿 → (𝑥 + 𝑀) < 𝑁)))
161160impcom 410 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) ∧ (𝑥 ∈ ℕ0𝑥 < (𝑁𝑀))) → (𝑁𝐿 → (𝑥 + 𝑀) < 𝑁))
162161impac 555 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) ∧ (𝑥 ∈ ℕ0𝑥 < (𝑁𝑀))) ∧ 𝑁𝐿) → ((𝑥 + 𝑀) < 𝑁𝑁𝐿))
163 ltletr 10724 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑥 + 𝑀) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ) → (((𝑥 + 𝑀) < 𝑁𝑁𝐿) → (𝑥 + 𝑀) < 𝐿))
164150, 162, 163sylc 65 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) ∧ (𝑥 ∈ ℕ0𝑥 < (𝑁𝑀))) ∧ 𝑁𝐿) → (𝑥 + 𝑀) < 𝐿)
165164exp31 422 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) → ((𝑥 ∈ ℕ0𝑥 < (𝑁𝑀)) → (𝑁𝐿 → (𝑥 + 𝑀) < 𝐿)))
166165com23 86 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐿 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0)) → (𝑁𝐿 → ((𝑥 ∈ ℕ0𝑥 < (𝑁𝑀)) → (𝑥 + 𝑀) < 𝐿)))
167166ex 415 . . . . . . . . . . . . . . . . . . . . 21 (𝐿 ∈ ℕ0 → ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (𝑁𝐿 → ((𝑥 ∈ ℕ0𝑥 < (𝑁𝑀)) → (𝑥 + 𝑀) < 𝐿))))
168167adantl 484 . . . . . . . . . . . . . . . . . . . 20 ((𝑆𝑉𝐿 ∈ ℕ0) → ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (𝑁𝐿 → ((𝑥 ∈ ℕ0𝑥 < (𝑁𝑀)) → (𝑥 + 𝑀) < 𝐿))))
1691683imp 1105 . . . . . . . . . . . . . . . . . . 19 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) → ((𝑥 ∈ ℕ0𝑥 < (𝑁𝑀)) → (𝑥 + 𝑀) < 𝐿))
170169ad2antrr 724 . . . . . . . . . . . . . . . . . 18 (((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀𝑁𝐿)) → ((𝑥 ∈ ℕ0𝑥 < (𝑁𝑀)) → (𝑥 + 𝑀) < 𝐿))
171170com12 32 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ℕ0𝑥 < (𝑁𝑀)) → (((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀𝑁𝐿)) → (𝑥 + 𝑀) < 𝐿))
1721713adant2 1125 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℕ0 ∧ (𝑁𝑀) ∈ ℕ ∧ 𝑥 < (𝑁𝑀)) → (((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀𝑁𝐿)) → (𝑥 + 𝑀) < 𝐿))
173137, 172sylbi 219 . . . . . . . . . . . . . . 15 (𝑥 ∈ (0..^(𝑁𝑀)) → (((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀𝑁𝐿)) → (𝑥 + 𝑀) < 𝐿))
174173impcom 410 . . . . . . . . . . . . . 14 ((((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀𝑁𝐿)) ∧ 𝑥 ∈ (0..^(𝑁𝑀))) → (𝑥 + 𝑀) < 𝐿)
175 elfzo0 13070 . . . . . . . . . . . . . 14 ((𝑥 + 𝑀) ∈ (0..^𝐿) ↔ ((𝑥 + 𝑀) ∈ ℕ0𝐿 ∈ ℕ ∧ (𝑥 + 𝑀) < 𝐿))
176107, 136, 174, 175syl3anbrc 1337 . . . . . . . . . . . . 13 ((((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀𝑁𝐿)) ∧ 𝑥 ∈ (0..^(𝑁𝑀))) → (𝑥 + 𝑀) ∈ (0..^𝐿))
177 repswsymb 14128 . . . . . . . . . . . . 13 ((𝑆𝑉𝐿 ∈ ℕ0 ∧ (𝑥 + 𝑀) ∈ (0..^𝐿)) → ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀)) = 𝑆)
17898, 100, 176, 177syl3anc 1365 . . . . . . . . . . . 12 ((((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀𝑁𝐿)) ∧ 𝑥 ∈ (0..^(𝑁𝑀))) → ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀)) = 𝑆)
179178mpteq2dva 5152 . . . . . . . . . . 11 (((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀𝑁𝐿)) → (𝑥 ∈ (0..^(𝑁𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))) = (𝑥 ∈ (0..^(𝑁𝑀)) ↦ 𝑆))
180333ad2ant2 1128 . . . . . . . . . . . . . . . 16 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) → (𝑁𝑀) ∈ ℤ)
181180adantr 483 . . . . . . . . . . . . . . 15 ((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) → (𝑁𝑀) ∈ ℤ)
182573ad2ant2 1128 . . . . . . . . . . . . . . . . . 18 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) → (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ))
183 ltle 10721 . . . . . . . . . . . . . . . . . 18 ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑀 < 𝑁𝑀𝑁))
184182, 183syl 17 . . . . . . . . . . . . . . . . 17 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) → (𝑀 < 𝑁𝑀𝑁))
185263ad2ant2 1128 . . . . . . . . . . . . . . . . . 18 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) → (𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ))
186185, 55syl 17 . . . . . . . . . . . . . . . . 17 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) → (0 ≤ (𝑁𝑀) ↔ 𝑀𝑁))
187184, 186sylibrd 261 . . . . . . . . . . . . . . . 16 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) → (𝑀 < 𝑁 → 0 ≤ (𝑁𝑀)))
188187imp 409 . . . . . . . . . . . . . . 15 ((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) → 0 ≤ (𝑁𝑀))
189181, 188, 54sylanbrc 585 . . . . . . . . . . . . . 14 ((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) → (𝑁𝑀) ∈ ℕ0)
19097, 189jca 514 . . . . . . . . . . . . 13 ((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) → (𝑆𝑉 ∧ (𝑁𝑀) ∈ ℕ0))
191190adantr 483 . . . . . . . . . . . 12 (((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀𝑁𝐿)) → (𝑆𝑉 ∧ (𝑁𝑀) ∈ ℕ0))
192 reps 14124 . . . . . . . . . . . . 13 ((𝑆𝑉 ∧ (𝑁𝑀) ∈ ℕ0) → (𝑆 repeatS (𝑁𝑀)) = (𝑥 ∈ (0..^(𝑁𝑀)) ↦ 𝑆))
193192eqcomd 2825 . . . . . . . . . . . 12 ((𝑆𝑉 ∧ (𝑁𝑀) ∈ ℕ0) → (𝑥 ∈ (0..^(𝑁𝑀)) ↦ 𝑆) = (𝑆 repeatS (𝑁𝑀)))
194191, 193syl 17 . . . . . . . . . . 11 (((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀𝑁𝐿)) → (𝑥 ∈ (0..^(𝑁𝑀)) ↦ 𝑆) = (𝑆 repeatS (𝑁𝑀)))
195179, 194eqtrd 2854 . . . . . . . . . 10 (((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) ∧ (0 ≤ 𝑀𝑁𝐿)) → (𝑥 ∈ (0..^(𝑁𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))) = (𝑆 repeatS (𝑁𝑀)))
196195ex 415 . . . . . . . . 9 ((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) → ((0 ≤ 𝑀𝑁𝐿) → (𝑥 ∈ (0..^(𝑁𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))) = (𝑆 repeatS (𝑁𝑀))))
19796, 196sylbid 242 . . . . . . . 8 ((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) → ((𝑀..^𝑁) ⊆ (0..^𝐿) → (𝑥 ∈ (0..^(𝑁𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))) = (𝑆 repeatS (𝑁𝑀))))
198197impcom 410 . . . . . . 7 (((𝑀..^𝑁) ⊆ (0..^𝐿) ∧ (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁)) → (𝑥 ∈ (0..^(𝑁𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))) = (𝑆 repeatS (𝑁𝑀)))
19986, 198eqtrd 2854 . . . . . 6 (((𝑀..^𝑁) ⊆ (0..^𝐿) ∧ (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁)) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁𝑀)))
200 iffalse 4474 . . . . . . . 8 (¬ (𝑀..^𝑁) ⊆ (0..^𝐿) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = ∅)
201200adantr 483 . . . . . . 7 ((¬ (𝑀..^𝑁) ⊆ (0..^𝐿) ∧ (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁)) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = ∅)
20296notbid 320 . . . . . . . . 9 ((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) → (¬ (𝑀..^𝑁) ⊆ (0..^𝐿) ↔ ¬ (0 ≤ 𝑀𝑁𝐿)))
203 ianor 977 . . . . . . . . . . 11 (¬ (0 ≤ 𝑀𝑁𝐿) ↔ (¬ 0 ≤ 𝑀 ∨ ¬ 𝑁𝐿))
204 nn0ge0 11914 . . . . . . . . . . . . . . . . 17 (𝑀 ∈ ℕ0 → 0 ≤ 𝑀)
205 pm2.24 124 . . . . . . . . . . . . . . . . 17 (0 ≤ 𝑀 → (¬ 0 ≤ 𝑀 → (𝑆 repeatS (𝑁𝑀)) = ∅))
206204, 205syl 17 . . . . . . . . . . . . . . . 16 (𝑀 ∈ ℕ0 → (¬ 0 ≤ 𝑀 → (𝑆 repeatS (𝑁𝑀)) = ∅))
207206adantr 483 . . . . . . . . . . . . . . 15 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (¬ 0 ≤ 𝑀 → (𝑆 repeatS (𝑁𝑀)) = ∅))
2082073ad2ant2 1128 . . . . . . . . . . . . . 14 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) → (¬ 0 ≤ 𝑀 → (𝑆 repeatS (𝑁𝑀)) = ∅))
209208adantr 483 . . . . . . . . . . . . 13 ((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) → (¬ 0 ≤ 𝑀 → (𝑆 repeatS (𝑁𝑀)) = ∅))
210209com12 32 . . . . . . . . . . . 12 (¬ 0 ≤ 𝑀 → ((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) → (𝑆 repeatS (𝑁𝑀)) = ∅))
211 pm2.24 124 . . . . . . . . . . . . . . 15 (𝑁𝐿 → (¬ 𝑁𝐿 → (𝑆 repeatS (𝑁𝑀)) = ∅))
2122113ad2ant3 1129 . . . . . . . . . . . . . 14 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) → (¬ 𝑁𝐿 → (𝑆 repeatS (𝑁𝑀)) = ∅))
213212adantr 483 . . . . . . . . . . . . 13 ((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) → (¬ 𝑁𝐿 → (𝑆 repeatS (𝑁𝑀)) = ∅))
214213com12 32 . . . . . . . . . . . 12 𝑁𝐿 → ((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) → (𝑆 repeatS (𝑁𝑀)) = ∅))
215210, 214jaoi 853 . . . . . . . . . . 11 ((¬ 0 ≤ 𝑀 ∨ ¬ 𝑁𝐿) → ((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) → (𝑆 repeatS (𝑁𝑀)) = ∅))
216203, 215sylbi 219 . . . . . . . . . 10 (¬ (0 ≤ 𝑀𝑁𝐿) → ((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) → (𝑆 repeatS (𝑁𝑀)) = ∅))
217216com12 32 . . . . . . . . 9 ((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) → (¬ (0 ≤ 𝑀𝑁𝐿) → (𝑆 repeatS (𝑁𝑀)) = ∅))
218202, 217sylbid 242 . . . . . . . 8 ((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) → (¬ (𝑀..^𝑁) ⊆ (0..^𝐿) → (𝑆 repeatS (𝑁𝑀)) = ∅))
219218impcom 410 . . . . . . 7 ((¬ (𝑀..^𝑁) ⊆ (0..^𝐿) ∧ (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁)) → (𝑆 repeatS (𝑁𝑀)) = ∅)
220201, 219eqtr4d 2857 . . . . . 6 ((¬ (𝑀..^𝑁) ⊆ (0..^𝐿) ∧ (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁)) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁𝑀)))
221199, 220pm2.61ian 810 . . . . 5 ((((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) ∧ 𝑀 < 𝑁) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁𝑀)))
222221ex 415 . . . 4 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) → (𝑀 < 𝑁 → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁𝑀))))
22385, 222sylbid 242 . . 3 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) → (¬ 𝑁𝑀 → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁𝑀))))
22481, 223pm2.61d 180 . 2 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) → if((𝑀..^𝑁) ⊆ (0..^𝐿), (𝑥 ∈ (0..^(𝑁𝑀)) ↦ ((𝑆 repeatS 𝐿)‘(𝑥 + 𝑀))), ∅) = (𝑆 repeatS (𝑁𝑀)))
22510, 15, 2243eqtrd 2858 1 (((𝑆𝑉𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑁𝐿) → ((𝑆 repeatS 𝐿) substr ⟨𝑀, 𝑁⟩) = (𝑆 repeatS (𝑁𝑀)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 208  wa 398  wo 843  w3a 1081   = wceq 1530  wcel 2107  wnel 3121  wss 3934  c0 4289  ifcif 4465  cop 4565   class class class wbr 5057  cmpt 5137  dom cdm 5548  wf 6344  cfv 6348  (class class class)co 7148  cc 10527  cr 10528  0cc0 10529   + caddc 10532   < clt 10667  cle 10668  cmin 10862  cn 11630  0cn0 11889  cz 11973  ..^cfzo 13025  Word cword 13853   substr csubstr 13994   repeatS creps 14122
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-nel 3122  df-ral 3141  df-rex 3142  df-reu 3143  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-pss 3952  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4831  df-int 4868  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7106  df-ov 7151  df-oprab 7152  df-mpo 7153  df-om 7573  df-1st 7681  df-2nd 7682  df-wrecs 7939  df-recs 8000  df-rdg 8038  df-1o 8094  df-er 8281  df-en 8502  df-dom 8503  df-sdom 8504  df-fin 8505  df-card 9360  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-nn 11631  df-n0 11890  df-z 11974  df-uz 12236  df-fz 12885  df-fzo 13026  df-hash 13683  df-word 13854  df-substr 13995  df-reps 14123
This theorem is referenced by:  repswcshw  14166
  Copyright terms: Public domain W3C validator