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

Theorem seqcoll 13465
Description: The function 𝐹 contains a sparse set of nonzero values to be summed. The function 𝐺 is an order isomorphism from the set of nonzero values of 𝐹 to a 1-based finite sequence, and 𝐻 collects these nonzero values together. Under these conditions, the sum over the values in 𝐻 yields the same result as the sum over the original set 𝐹. (Contributed by Mario Carneiro, 2-Apr-2014.)
Hypotheses
Ref Expression
seqcoll.1 ((𝜑𝑘𝑆) → (𝑍 + 𝑘) = 𝑘)
seqcoll.1b ((𝜑𝑘𝑆) → (𝑘 + 𝑍) = 𝑘)
seqcoll.c ((𝜑 ∧ (𝑘𝑆𝑛𝑆)) → (𝑘 + 𝑛) ∈ 𝑆)
seqcoll.a (𝜑𝑍𝑆)
seqcoll.2 (𝜑𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴))
seqcoll.3 (𝜑𝑁 ∈ (1...(♯‘𝐴)))
seqcoll.4 (𝜑𝐴 ⊆ (ℤ𝑀))
seqcoll.5 ((𝜑𝑘 ∈ (𝑀...(𝐺‘(♯‘𝐴)))) → (𝐹𝑘) ∈ 𝑆)
seqcoll.6 ((𝜑𝑘 ∈ ((𝑀...(𝐺‘(♯‘𝐴))) ∖ 𝐴)) → (𝐹𝑘) = 𝑍)
seqcoll.7 ((𝜑𝑛 ∈ (1...(♯‘𝐴))) → (𝐻𝑛) = (𝐹‘(𝐺𝑛)))
Assertion
Ref Expression
seqcoll (𝜑 → (seq𝑀( + , 𝐹)‘(𝐺𝑁)) = (seq1( + , 𝐻)‘𝑁))
Distinct variable groups:   𝑘,𝑛,𝐴   𝑘,𝐹,𝑛   𝑘,𝐺,𝑛   𝑛,𝐻   𝑘,𝑀,𝑛   + ,𝑘,𝑛   𝜑,𝑘,𝑛   𝑆,𝑘,𝑛   𝑘,𝑍
Allowed substitution hints:   𝐻(𝑘)   𝑁(𝑘,𝑛)   𝑍(𝑛)

Proof of Theorem seqcoll
Dummy variables 𝑚 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 seqcoll.3 . 2 (𝜑𝑁 ∈ (1...(♯‘𝐴)))
2 elfznn 12593 . . . 4 (𝑁 ∈ (1...(♯‘𝐴)) → 𝑁 ∈ ℕ)
31, 2syl 17 . . 3 (𝜑𝑁 ∈ ℕ)
4 eleq1 2873 . . . . . 6 (𝑦 = 1 → (𝑦 ∈ (1...(♯‘𝐴)) ↔ 1 ∈ (1...(♯‘𝐴))))
5 2fveq3 6413 . . . . . . 7 (𝑦 = 1 → (seq𝑀( + , 𝐹)‘(𝐺𝑦)) = (seq𝑀( + , 𝐹)‘(𝐺‘1)))
6 fveq2 6408 . . . . . . 7 (𝑦 = 1 → (seq1( + , 𝐻)‘𝑦) = (seq1( + , 𝐻)‘1))
75, 6eqeq12d 2821 . . . . . 6 (𝑦 = 1 → ((seq𝑀( + , 𝐹)‘(𝐺𝑦)) = (seq1( + , 𝐻)‘𝑦) ↔ (seq𝑀( + , 𝐹)‘(𝐺‘1)) = (seq1( + , 𝐻)‘1)))
84, 7imbi12d 335 . . . . 5 (𝑦 = 1 → ((𝑦 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺𝑦)) = (seq1( + , 𝐻)‘𝑦)) ↔ (1 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘1)) = (seq1( + , 𝐻)‘1))))
98imbi2d 331 . . . 4 (𝑦 = 1 → ((𝜑 → (𝑦 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺𝑦)) = (seq1( + , 𝐻)‘𝑦))) ↔ (𝜑 → (1 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘1)) = (seq1( + , 𝐻)‘1)))))
10 eleq1 2873 . . . . . 6 (𝑦 = 𝑚 → (𝑦 ∈ (1...(♯‘𝐴)) ↔ 𝑚 ∈ (1...(♯‘𝐴))))
11 2fveq3 6413 . . . . . . 7 (𝑦 = 𝑚 → (seq𝑀( + , 𝐹)‘(𝐺𝑦)) = (seq𝑀( + , 𝐹)‘(𝐺𝑚)))
12 fveq2 6408 . . . . . . 7 (𝑦 = 𝑚 → (seq1( + , 𝐻)‘𝑦) = (seq1( + , 𝐻)‘𝑚))
1311, 12eqeq12d 2821 . . . . . 6 (𝑦 = 𝑚 → ((seq𝑀( + , 𝐹)‘(𝐺𝑦)) = (seq1( + , 𝐻)‘𝑦) ↔ (seq𝑀( + , 𝐹)‘(𝐺𝑚)) = (seq1( + , 𝐻)‘𝑚)))
1410, 13imbi12d 335 . . . . 5 (𝑦 = 𝑚 → ((𝑦 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺𝑦)) = (seq1( + , 𝐻)‘𝑦)) ↔ (𝑚 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺𝑚)) = (seq1( + , 𝐻)‘𝑚))))
1514imbi2d 331 . . . 4 (𝑦 = 𝑚 → ((𝜑 → (𝑦 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺𝑦)) = (seq1( + , 𝐻)‘𝑦))) ↔ (𝜑 → (𝑚 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺𝑚)) = (seq1( + , 𝐻)‘𝑚)))))
16 eleq1 2873 . . . . . 6 (𝑦 = (𝑚 + 1) → (𝑦 ∈ (1...(♯‘𝐴)) ↔ (𝑚 + 1) ∈ (1...(♯‘𝐴))))
17 2fveq3 6413 . . . . . . 7 (𝑦 = (𝑚 + 1) → (seq𝑀( + , 𝐹)‘(𝐺𝑦)) = (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))))
18 fveq2 6408 . . . . . . 7 (𝑦 = (𝑚 + 1) → (seq1( + , 𝐻)‘𝑦) = (seq1( + , 𝐻)‘(𝑚 + 1)))
1917, 18eqeq12d 2821 . . . . . 6 (𝑦 = (𝑚 + 1) → ((seq𝑀( + , 𝐹)‘(𝐺𝑦)) = (seq1( + , 𝐻)‘𝑦) ↔ (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1))))
2016, 19imbi12d 335 . . . . 5 (𝑦 = (𝑚 + 1) → ((𝑦 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺𝑦)) = (seq1( + , 𝐻)‘𝑦)) ↔ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1)))))
2120imbi2d 331 . . . 4 (𝑦 = (𝑚 + 1) → ((𝜑 → (𝑦 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺𝑦)) = (seq1( + , 𝐻)‘𝑦))) ↔ (𝜑 → ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1))))))
22 eleq1 2873 . . . . . 6 (𝑦 = 𝑁 → (𝑦 ∈ (1...(♯‘𝐴)) ↔ 𝑁 ∈ (1...(♯‘𝐴))))
23 2fveq3 6413 . . . . . . 7 (𝑦 = 𝑁 → (seq𝑀( + , 𝐹)‘(𝐺𝑦)) = (seq𝑀( + , 𝐹)‘(𝐺𝑁)))
24 fveq2 6408 . . . . . . 7 (𝑦 = 𝑁 → (seq1( + , 𝐻)‘𝑦) = (seq1( + , 𝐻)‘𝑁))
2523, 24eqeq12d 2821 . . . . . 6 (𝑦 = 𝑁 → ((seq𝑀( + , 𝐹)‘(𝐺𝑦)) = (seq1( + , 𝐻)‘𝑦) ↔ (seq𝑀( + , 𝐹)‘(𝐺𝑁)) = (seq1( + , 𝐻)‘𝑁)))
2622, 25imbi12d 335 . . . . 5 (𝑦 = 𝑁 → ((𝑦 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺𝑦)) = (seq1( + , 𝐻)‘𝑦)) ↔ (𝑁 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺𝑁)) = (seq1( + , 𝐻)‘𝑁))))
2726imbi2d 331 . . . 4 (𝑦 = 𝑁 → ((𝜑 → (𝑦 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺𝑦)) = (seq1( + , 𝐻)‘𝑦))) ↔ (𝜑 → (𝑁 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺𝑁)) = (seq1( + , 𝐻)‘𝑁)))))
28 seqcoll.1 . . . . . . . . 9 ((𝜑𝑘𝑆) → (𝑍 + 𝑘) = 𝑘)
29 seqcoll.a . . . . . . . . 9 (𝜑𝑍𝑆)
30 seqcoll.4 . . . . . . . . . 10 (𝜑𝐴 ⊆ (ℤ𝑀))
31 seqcoll.2 . . . . . . . . . . . . 13 (𝜑𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴))
32 isof1o 6797 . . . . . . . . . . . . 13 (𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴) → 𝐺:(1...(♯‘𝐴))–1-1-onto𝐴)
3331, 32syl 17 . . . . . . . . . . . 12 (𝜑𝐺:(1...(♯‘𝐴))–1-1-onto𝐴)
34 f1of 6353 . . . . . . . . . . . 12 (𝐺:(1...(♯‘𝐴))–1-1-onto𝐴𝐺:(1...(♯‘𝐴))⟶𝐴)
3533, 34syl 17 . . . . . . . . . . 11 (𝜑𝐺:(1...(♯‘𝐴))⟶𝐴)
36 elfzuz2 12569 . . . . . . . . . . . . 13 (𝑁 ∈ (1...(♯‘𝐴)) → (♯‘𝐴) ∈ (ℤ‘1))
371, 36syl 17 . . . . . . . . . . . 12 (𝜑 → (♯‘𝐴) ∈ (ℤ‘1))
38 eluzfz1 12571 . . . . . . . . . . . 12 ((♯‘𝐴) ∈ (ℤ‘1) → 1 ∈ (1...(♯‘𝐴)))
3937, 38syl 17 . . . . . . . . . . 11 (𝜑 → 1 ∈ (1...(♯‘𝐴)))
4035, 39ffvelrnd 6582 . . . . . . . . . 10 (𝜑 → (𝐺‘1) ∈ 𝐴)
4130, 40sseldd 3799 . . . . . . . . 9 (𝜑 → (𝐺‘1) ∈ (ℤ𝑀))
42 eluzle 11917 . . . . . . . . . . . . 13 ((♯‘𝐴) ∈ (ℤ‘1) → 1 ≤ (♯‘𝐴))
4337, 42syl 17 . . . . . . . . . . . 12 (𝜑 → 1 ≤ (♯‘𝐴))
44 elfzelz 12565 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ (1...(♯‘𝐴)) → 𝑘 ∈ ℤ)
4544ssriv 3802 . . . . . . . . . . . . . . . 16 (1...(♯‘𝐴)) ⊆ ℤ
46 zssre 11650 . . . . . . . . . . . . . . . 16 ℤ ⊆ ℝ
4745, 46sstri 3807 . . . . . . . . . . . . . . 15 (1...(♯‘𝐴)) ⊆ ℝ
4847a1i 11 . . . . . . . . . . . . . 14 (𝜑 → (1...(♯‘𝐴)) ⊆ ℝ)
49 ressxr 10368 . . . . . . . . . . . . . 14 ℝ ⊆ ℝ*
5048, 49syl6ss 3810 . . . . . . . . . . . . 13 (𝜑 → (1...(♯‘𝐴)) ⊆ ℝ*)
51 eluzelre 11915 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (ℤ𝑀) → 𝑘 ∈ ℝ)
5251ssriv 3802 . . . . . . . . . . . . . . 15 (ℤ𝑀) ⊆ ℝ
5330, 52syl6ss 3810 . . . . . . . . . . . . . 14 (𝜑𝐴 ⊆ ℝ)
5453, 49syl6ss 3810 . . . . . . . . . . . . 13 (𝜑𝐴 ⊆ ℝ*)
55 eluzfz2 12572 . . . . . . . . . . . . . 14 ((♯‘𝐴) ∈ (ℤ‘1) → (♯‘𝐴) ∈ (1...(♯‘𝐴)))
5637, 55syl 17 . . . . . . . . . . . . 13 (𝜑 → (♯‘𝐴) ∈ (1...(♯‘𝐴)))
57 leisorel 13461 . . . . . . . . . . . . 13 ((𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴) ∧ ((1...(♯‘𝐴)) ⊆ ℝ*𝐴 ⊆ ℝ*) ∧ (1 ∈ (1...(♯‘𝐴)) ∧ (♯‘𝐴) ∈ (1...(♯‘𝐴)))) → (1 ≤ (♯‘𝐴) ↔ (𝐺‘1) ≤ (𝐺‘(♯‘𝐴))))
5831, 50, 54, 39, 56, 57syl122anc 1491 . . . . . . . . . . . 12 (𝜑 → (1 ≤ (♯‘𝐴) ↔ (𝐺‘1) ≤ (𝐺‘(♯‘𝐴))))
5943, 58mpbid 223 . . . . . . . . . . 11 (𝜑 → (𝐺‘1) ≤ (𝐺‘(♯‘𝐴)))
6035, 56ffvelrnd 6582 . . . . . . . . . . . . . 14 (𝜑 → (𝐺‘(♯‘𝐴)) ∈ 𝐴)
6130, 60sseldd 3799 . . . . . . . . . . . . 13 (𝜑 → (𝐺‘(♯‘𝐴)) ∈ (ℤ𝑀))
62 eluzelz 11914 . . . . . . . . . . . . 13 ((𝐺‘(♯‘𝐴)) ∈ (ℤ𝑀) → (𝐺‘(♯‘𝐴)) ∈ ℤ)
6361, 62syl 17 . . . . . . . . . . . 12 (𝜑 → (𝐺‘(♯‘𝐴)) ∈ ℤ)
64 elfz5 12557 . . . . . . . . . . . 12 (((𝐺‘1) ∈ (ℤ𝑀) ∧ (𝐺‘(♯‘𝐴)) ∈ ℤ) → ((𝐺‘1) ∈ (𝑀...(𝐺‘(♯‘𝐴))) ↔ (𝐺‘1) ≤ (𝐺‘(♯‘𝐴))))
6541, 63, 64syl2anc 575 . . . . . . . . . . 11 (𝜑 → ((𝐺‘1) ∈ (𝑀...(𝐺‘(♯‘𝐴))) ↔ (𝐺‘1) ≤ (𝐺‘(♯‘𝐴))))
6659, 65mpbird 248 . . . . . . . . . 10 (𝜑 → (𝐺‘1) ∈ (𝑀...(𝐺‘(♯‘𝐴))))
67 fveq2 6408 . . . . . . . . . . . . 13 (𝑘 = (𝐺‘1) → (𝐹𝑘) = (𝐹‘(𝐺‘1)))
6867eleq1d 2870 . . . . . . . . . . . 12 (𝑘 = (𝐺‘1) → ((𝐹𝑘) ∈ 𝑆 ↔ (𝐹‘(𝐺‘1)) ∈ 𝑆))
6968imbi2d 331 . . . . . . . . . . 11 (𝑘 = (𝐺‘1) → ((𝜑 → (𝐹𝑘) ∈ 𝑆) ↔ (𝜑 → (𝐹‘(𝐺‘1)) ∈ 𝑆)))
70 seqcoll.5 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (𝑀...(𝐺‘(♯‘𝐴)))) → (𝐹𝑘) ∈ 𝑆)
7170expcom 400 . . . . . . . . . . 11 (𝑘 ∈ (𝑀...(𝐺‘(♯‘𝐴))) → (𝜑 → (𝐹𝑘) ∈ 𝑆))
7269, 71vtoclga 3465 . . . . . . . . . 10 ((𝐺‘1) ∈ (𝑀...(𝐺‘(♯‘𝐴))) → (𝜑 → (𝐹‘(𝐺‘1)) ∈ 𝑆))
7366, 72mpcom 38 . . . . . . . . 9 (𝜑 → (𝐹‘(𝐺‘1)) ∈ 𝑆)
74 eluzelz 11914 . . . . . . . . . . . . . . . . . 18 ((𝐺‘1) ∈ (ℤ𝑀) → (𝐺‘1) ∈ ℤ)
7541, 74syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐺‘1) ∈ ℤ)
76 peano2zm 11686 . . . . . . . . . . . . . . . . 17 ((𝐺‘1) ∈ ℤ → ((𝐺‘1) − 1) ∈ ℤ)
7775, 76syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐺‘1) − 1) ∈ ℤ)
7877zred 11748 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐺‘1) − 1) ∈ ℝ)
7975zred 11748 . . . . . . . . . . . . . . 15 (𝜑 → (𝐺‘1) ∈ ℝ)
8063zred 11748 . . . . . . . . . . . . . . 15 (𝜑 → (𝐺‘(♯‘𝐴)) ∈ ℝ)
8179lem1d 11242 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐺‘1) − 1) ≤ (𝐺‘1))
8278, 79, 80, 81, 59letrd 10479 . . . . . . . . . . . . . 14 (𝜑 → ((𝐺‘1) − 1) ≤ (𝐺‘(♯‘𝐴)))
83 eluz 11918 . . . . . . . . . . . . . . 15 ((((𝐺‘1) − 1) ∈ ℤ ∧ (𝐺‘(♯‘𝐴)) ∈ ℤ) → ((𝐺‘(♯‘𝐴)) ∈ (ℤ‘((𝐺‘1) − 1)) ↔ ((𝐺‘1) − 1) ≤ (𝐺‘(♯‘𝐴))))
8477, 63, 83syl2anc 575 . . . . . . . . . . . . . 14 (𝜑 → ((𝐺‘(♯‘𝐴)) ∈ (ℤ‘((𝐺‘1) − 1)) ↔ ((𝐺‘1) − 1) ≤ (𝐺‘(♯‘𝐴))))
8582, 84mpbird 248 . . . . . . . . . . . . 13 (𝜑 → (𝐺‘(♯‘𝐴)) ∈ (ℤ‘((𝐺‘1) − 1)))
86 fzss2 12604 . . . . . . . . . . . . 13 ((𝐺‘(♯‘𝐴)) ∈ (ℤ‘((𝐺‘1) − 1)) → (𝑀...((𝐺‘1) − 1)) ⊆ (𝑀...(𝐺‘(♯‘𝐴))))
8785, 86syl 17 . . . . . . . . . . . 12 (𝜑 → (𝑀...((𝐺‘1) − 1)) ⊆ (𝑀...(𝐺‘(♯‘𝐴))))
8887sselda 3798 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (𝑀...((𝐺‘1) − 1))) → 𝑘 ∈ (𝑀...(𝐺‘(♯‘𝐴))))
89 eluzel2 11909 . . . . . . . . . . . . . . 15 ((𝐺‘1) ∈ (ℤ𝑀) → 𝑀 ∈ ℤ)
9041, 89syl 17 . . . . . . . . . . . . . 14 (𝜑𝑀 ∈ ℤ)
91 elfzm11 12634 . . . . . . . . . . . . . 14 ((𝑀 ∈ ℤ ∧ (𝐺‘1) ∈ ℤ) → (𝑘 ∈ (𝑀...((𝐺‘1) − 1)) ↔ (𝑘 ∈ ℤ ∧ 𝑀𝑘𝑘 < (𝐺‘1))))
9290, 75, 91syl2anc 575 . . . . . . . . . . . . 13 (𝜑 → (𝑘 ∈ (𝑀...((𝐺‘1) − 1)) ↔ (𝑘 ∈ ℤ ∧ 𝑀𝑘𝑘 < (𝐺‘1))))
93 simp3 1161 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℤ ∧ 𝑀𝑘𝑘 < (𝐺‘1)) → 𝑘 < (𝐺‘1))
94 f1ocnv 6365 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐺:(1...(♯‘𝐴))–1-1-onto𝐴𝐺:𝐴1-1-onto→(1...(♯‘𝐴)))
9533, 94syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐺:𝐴1-1-onto→(1...(♯‘𝐴)))
96 f1of 6353 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐺:𝐴1-1-onto→(1...(♯‘𝐴)) → 𝐺:𝐴⟶(1...(♯‘𝐴)))
9795, 96syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐺:𝐴⟶(1...(♯‘𝐴)))
9897ffvelrnda 6581 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘𝐴) → (𝐺𝑘) ∈ (1...(♯‘𝐴)))
99 elfznn 12593 . . . . . . . . . . . . . . . . . . . . 21 ((𝐺𝑘) ∈ (1...(♯‘𝐴)) → (𝐺𝑘) ∈ ℕ)
10098, 99syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘𝐴) → (𝐺𝑘) ∈ ℕ)
101100nnge1d 11349 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘𝐴) → 1 ≤ (𝐺𝑘))
10231adantr 468 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘𝐴) → 𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴))
10350adantr 468 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘𝐴) → (1...(♯‘𝐴)) ⊆ ℝ*)
10454adantr 468 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘𝐴) → 𝐴 ⊆ ℝ*)
10539adantr 468 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘𝐴) → 1 ∈ (1...(♯‘𝐴)))
106 leisorel 13461 . . . . . . . . . . . . . . . . . . . 20 ((𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴) ∧ ((1...(♯‘𝐴)) ⊆ ℝ*𝐴 ⊆ ℝ*) ∧ (1 ∈ (1...(♯‘𝐴)) ∧ (𝐺𝑘) ∈ (1...(♯‘𝐴)))) → (1 ≤ (𝐺𝑘) ↔ (𝐺‘1) ≤ (𝐺‘(𝐺𝑘))))
107102, 103, 104, 105, 98, 106syl122anc 1491 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘𝐴) → (1 ≤ (𝐺𝑘) ↔ (𝐺‘1) ≤ (𝐺‘(𝐺𝑘))))
108101, 107mpbid 223 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘𝐴) → (𝐺‘1) ≤ (𝐺‘(𝐺𝑘)))
109 f1ocnvfv2 6757 . . . . . . . . . . . . . . . . . . 19 ((𝐺:(1...(♯‘𝐴))–1-1-onto𝐴𝑘𝐴) → (𝐺‘(𝐺𝑘)) = 𝑘)
11033, 109sylan 571 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘𝐴) → (𝐺‘(𝐺𝑘)) = 𝑘)
111108, 110breqtrd 4870 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝐴) → (𝐺‘1) ≤ 𝑘)
11279adantr 468 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘𝐴) → (𝐺‘1) ∈ ℝ)
11353sselda 3798 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘𝐴) → 𝑘 ∈ ℝ)
114112, 113lenltd 10468 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝐴) → ((𝐺‘1) ≤ 𝑘 ↔ ¬ 𝑘 < (𝐺‘1)))
115111, 114mpbid 223 . . . . . . . . . . . . . . . 16 ((𝜑𝑘𝐴) → ¬ 𝑘 < (𝐺‘1))
116115ex 399 . . . . . . . . . . . . . . 15 (𝜑 → (𝑘𝐴 → ¬ 𝑘 < (𝐺‘1)))
117116con2d 131 . . . . . . . . . . . . . 14 (𝜑 → (𝑘 < (𝐺‘1) → ¬ 𝑘𝐴))
11893, 117syl5 34 . . . . . . . . . . . . 13 (𝜑 → ((𝑘 ∈ ℤ ∧ 𝑀𝑘𝑘 < (𝐺‘1)) → ¬ 𝑘𝐴))
11992, 118sylbid 231 . . . . . . . . . . . 12 (𝜑 → (𝑘 ∈ (𝑀...((𝐺‘1) − 1)) → ¬ 𝑘𝐴))
120119imp 395 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (𝑀...((𝐺‘1) − 1))) → ¬ 𝑘𝐴)
12188, 120eldifd 3780 . . . . . . . . . 10 ((𝜑𝑘 ∈ (𝑀...((𝐺‘1) − 1))) → 𝑘 ∈ ((𝑀...(𝐺‘(♯‘𝐴))) ∖ 𝐴))
122 seqcoll.6 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝑀...(𝐺‘(♯‘𝐴))) ∖ 𝐴)) → (𝐹𝑘) = 𝑍)
123121, 122syldan 581 . . . . . . . . 9 ((𝜑𝑘 ∈ (𝑀...((𝐺‘1) − 1))) → (𝐹𝑘) = 𝑍)
12428, 29, 41, 73, 123seqid 13069 . . . . . . . 8 (𝜑 → (seq𝑀( + , 𝐹) ↾ (ℤ‘(𝐺‘1))) = seq(𝐺‘1)( + , 𝐹))
125124fveq1d 6410 . . . . . . 7 (𝜑 → ((seq𝑀( + , 𝐹) ↾ (ℤ‘(𝐺‘1)))‘(𝐺‘1)) = (seq(𝐺‘1)( + , 𝐹)‘(𝐺‘1)))
126 uzid 11919 . . . . . . . . 9 ((𝐺‘1) ∈ ℤ → (𝐺‘1) ∈ (ℤ‘(𝐺‘1)))
12775, 126syl 17 . . . . . . . 8 (𝜑 → (𝐺‘1) ∈ (ℤ‘(𝐺‘1)))
128 fvres 6427 . . . . . . . 8 ((𝐺‘1) ∈ (ℤ‘(𝐺‘1)) → ((seq𝑀( + , 𝐹) ↾ (ℤ‘(𝐺‘1)))‘(𝐺‘1)) = (seq𝑀( + , 𝐹)‘(𝐺‘1)))
129127, 128syl 17 . . . . . . 7 (𝜑 → ((seq𝑀( + , 𝐹) ↾ (ℤ‘(𝐺‘1)))‘(𝐺‘1)) = (seq𝑀( + , 𝐹)‘(𝐺‘1)))
130 seq1 13037 . . . . . . . . 9 ((𝐺‘1) ∈ ℤ → (seq(𝐺‘1)( + , 𝐹)‘(𝐺‘1)) = (𝐹‘(𝐺‘1)))
13175, 130syl 17 . . . . . . . 8 (𝜑 → (seq(𝐺‘1)( + , 𝐹)‘(𝐺‘1)) = (𝐹‘(𝐺‘1)))
132 fveq2 6408 . . . . . . . . . . . 12 (𝑛 = 1 → (𝐻𝑛) = (𝐻‘1))
133 2fveq3 6413 . . . . . . . . . . . 12 (𝑛 = 1 → (𝐹‘(𝐺𝑛)) = (𝐹‘(𝐺‘1)))
134132, 133eqeq12d 2821 . . . . . . . . . . 11 (𝑛 = 1 → ((𝐻𝑛) = (𝐹‘(𝐺𝑛)) ↔ (𝐻‘1) = (𝐹‘(𝐺‘1))))
135134imbi2d 331 . . . . . . . . . 10 (𝑛 = 1 → ((𝜑 → (𝐻𝑛) = (𝐹‘(𝐺𝑛))) ↔ (𝜑 → (𝐻‘1) = (𝐹‘(𝐺‘1)))))
136 seqcoll.7 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...(♯‘𝐴))) → (𝐻𝑛) = (𝐹‘(𝐺𝑛)))
137136expcom 400 . . . . . . . . . 10 (𝑛 ∈ (1...(♯‘𝐴)) → (𝜑 → (𝐻𝑛) = (𝐹‘(𝐺𝑛))))
138135, 137vtoclga 3465 . . . . . . . . 9 (1 ∈ (1...(♯‘𝐴)) → (𝜑 → (𝐻‘1) = (𝐹‘(𝐺‘1))))
13939, 138mpcom 38 . . . . . . . 8 (𝜑 → (𝐻‘1) = (𝐹‘(𝐺‘1)))
140131, 139eqtr4d 2843 . . . . . . 7 (𝜑 → (seq(𝐺‘1)( + , 𝐹)‘(𝐺‘1)) = (𝐻‘1))
141125, 129, 1403eqtr3d 2848 . . . . . 6 (𝜑 → (seq𝑀( + , 𝐹)‘(𝐺‘1)) = (𝐻‘1))
142 1z 11673 . . . . . . 7 1 ∈ ℤ
143 seq1 13037 . . . . . . 7 (1 ∈ ℤ → (seq1( + , 𝐻)‘1) = (𝐻‘1))
144142, 143ax-mp 5 . . . . . 6 (seq1( + , 𝐻)‘1) = (𝐻‘1)
145141, 144syl6eqr 2858 . . . . 5 (𝜑 → (seq𝑀( + , 𝐹)‘(𝐺‘1)) = (seq1( + , 𝐻)‘1))
146145a1d 25 . . . 4 (𝜑 → (1 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘1)) = (seq1( + , 𝐻)‘1)))
147 simplr 776 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝑚 ∈ ℕ)
148 nnuz 11941 . . . . . . . . . . 11 ℕ = (ℤ‘1)
149147, 148syl6eleq 2895 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝑚 ∈ (ℤ‘1))
150 nnz 11665 . . . . . . . . . . . 12 (𝑚 ∈ ℕ → 𝑚 ∈ ℤ)
151150ad2antlr 709 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝑚 ∈ ℤ)
152 elfzuz3 12562 . . . . . . . . . . . 12 ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (♯‘𝐴) ∈ (ℤ‘(𝑚 + 1)))
153152adantl 469 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (♯‘𝐴) ∈ (ℤ‘(𝑚 + 1)))
154 peano2uzr 11961 . . . . . . . . . . 11 ((𝑚 ∈ ℤ ∧ (♯‘𝐴) ∈ (ℤ‘(𝑚 + 1))) → (♯‘𝐴) ∈ (ℤ𝑚))
155151, 153, 154syl2anc 575 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (♯‘𝐴) ∈ (ℤ𝑚))
156 elfzuzb 12559 . . . . . . . . . 10 (𝑚 ∈ (1...(♯‘𝐴)) ↔ (𝑚 ∈ (ℤ‘1) ∧ (♯‘𝐴) ∈ (ℤ𝑚)))
157149, 155, 156sylanbrc 574 . . . . . . . . 9 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝑚 ∈ (1...(♯‘𝐴)))
158157ex 399 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ) → ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → 𝑚 ∈ (1...(♯‘𝐴))))
159158imim1d 82 . . . . . . 7 ((𝜑𝑚 ∈ ℕ) → ((𝑚 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺𝑚)) = (seq1( + , 𝐻)‘𝑚)) → ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺𝑚)) = (seq1( + , 𝐻)‘𝑚))))
160 oveq1 6881 . . . . . . . . . 10 ((seq𝑀( + , 𝐹)‘(𝐺𝑚)) = (seq1( + , 𝐻)‘𝑚) → ((seq𝑀( + , 𝐹)‘(𝐺𝑚)) + (𝐻‘(𝑚 + 1))) = ((seq1( + , 𝐻)‘𝑚) + (𝐻‘(𝑚 + 1))))
161 simpll 774 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝜑)
162 seqcoll.1b . . . . . . . . . . . . . . 15 ((𝜑𝑘𝑆) → (𝑘 + 𝑍) = 𝑘)
163161, 162sylan 571 . . . . . . . . . . . . . 14 ((((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘𝑆) → (𝑘 + 𝑍) = 𝑘)
16430ad2antrr 708 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝐴 ⊆ (ℤ𝑀))
16535ad2antrr 708 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝐺:(1...(♯‘𝐴))⟶𝐴)
166165, 157ffvelrnd 6582 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺𝑚) ∈ 𝐴)
167164, 166sseldd 3799 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺𝑚) ∈ (ℤ𝑀))
168 nnre 11312 . . . . . . . . . . . . . . . . . . 19 (𝑚 ∈ ℕ → 𝑚 ∈ ℝ)
169168ad2antlr 709 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝑚 ∈ ℝ)
170169ltp1d 11239 . . . . . . . . . . . . . . . . 17 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝑚 < (𝑚 + 1))
17131ad2antrr 708 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴))
172 simpr 473 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝑚 + 1) ∈ (1...(♯‘𝐴)))
173 isorel 6800 . . . . . . . . . . . . . . . . . 18 ((𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴) ∧ (𝑚 ∈ (1...(♯‘𝐴)) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴)))) → (𝑚 < (𝑚 + 1) ↔ (𝐺𝑚) < (𝐺‘(𝑚 + 1))))
174171, 157, 172, 173syl12anc 856 . . . . . . . . . . . . . . . . 17 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝑚 < (𝑚 + 1) ↔ (𝐺𝑚) < (𝐺‘(𝑚 + 1))))
175170, 174mpbid 223 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺𝑚) < (𝐺‘(𝑚 + 1)))
176 eluzelz 11914 . . . . . . . . . . . . . . . . . 18 ((𝐺𝑚) ∈ (ℤ𝑀) → (𝐺𝑚) ∈ ℤ)
177167, 176syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺𝑚) ∈ ℤ)
178165, 172ffvelrnd 6582 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(𝑚 + 1)) ∈ 𝐴)
179164, 178sseldd 3799 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(𝑚 + 1)) ∈ (ℤ𝑀))
180 eluzelz 11914 . . . . . . . . . . . . . . . . . 18 ((𝐺‘(𝑚 + 1)) ∈ (ℤ𝑀) → (𝐺‘(𝑚 + 1)) ∈ ℤ)
181179, 180syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(𝑚 + 1)) ∈ ℤ)
182 zltlem1 11696 . . . . . . . . . . . . . . . . 17 (((𝐺𝑚) ∈ ℤ ∧ (𝐺‘(𝑚 + 1)) ∈ ℤ) → ((𝐺𝑚) < (𝐺‘(𝑚 + 1)) ↔ (𝐺𝑚) ≤ ((𝐺‘(𝑚 + 1)) − 1)))
183177, 181, 182syl2anc 575 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝐺𝑚) < (𝐺‘(𝑚 + 1)) ↔ (𝐺𝑚) ≤ ((𝐺‘(𝑚 + 1)) − 1)))
184175, 183mpbid 223 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺𝑚) ≤ ((𝐺‘(𝑚 + 1)) − 1))
185 peano2zm 11686 . . . . . . . . . . . . . . . . 17 ((𝐺‘(𝑚 + 1)) ∈ ℤ → ((𝐺‘(𝑚 + 1)) − 1) ∈ ℤ)
186181, 185syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝐺‘(𝑚 + 1)) − 1) ∈ ℤ)
187 eluz 11918 . . . . . . . . . . . . . . . 16 (((𝐺𝑚) ∈ ℤ ∧ ((𝐺‘(𝑚 + 1)) − 1) ∈ ℤ) → (((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ‘(𝐺𝑚)) ↔ (𝐺𝑚) ≤ ((𝐺‘(𝑚 + 1)) − 1)))
188177, 186, 187syl2anc 575 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ‘(𝐺𝑚)) ↔ (𝐺𝑚) ≤ ((𝐺‘(𝑚 + 1)) − 1)))
189184, 188mpbird 248 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ‘(𝐺𝑚)))
190186zred 11748 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝐺‘(𝑚 + 1)) − 1) ∈ ℝ)
191181zred 11748 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(𝑚 + 1)) ∈ ℝ)
19280ad2antrr 708 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(♯‘𝐴)) ∈ ℝ)
193191lem1d 11242 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝐺‘(𝑚 + 1)) − 1) ≤ (𝐺‘(𝑚 + 1)))
194 elfzle2 12568 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (𝑚 + 1) ≤ (♯‘𝐴))
195194adantl 469 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝑚 + 1) ≤ (♯‘𝐴))
19650ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (1...(♯‘𝐴)) ⊆ ℝ*)
19754ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝐴 ⊆ ℝ*)
19856ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (♯‘𝐴) ∈ (1...(♯‘𝐴)))
199 leisorel 13461 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴) ∧ ((1...(♯‘𝐴)) ⊆ ℝ*𝐴 ⊆ ℝ*) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ (♯‘𝐴) ∈ (1...(♯‘𝐴)))) → ((𝑚 + 1) ≤ (♯‘𝐴) ↔ (𝐺‘(𝑚 + 1)) ≤ (𝐺‘(♯‘𝐴))))
200171, 196, 197, 172, 198, 199syl122anc 1491 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝑚 + 1) ≤ (♯‘𝐴) ↔ (𝐺‘(𝑚 + 1)) ≤ (𝐺‘(♯‘𝐴))))
201195, 200mpbid 223 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(𝑚 + 1)) ≤ (𝐺‘(♯‘𝐴)))
202190, 191, 192, 193, 201letrd 10479 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝐺‘(𝑚 + 1)) − 1) ≤ (𝐺‘(♯‘𝐴)))
20363ad2antrr 708 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(♯‘𝐴)) ∈ ℤ)
204 eluz 11918 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐺‘(𝑚 + 1)) − 1) ∈ ℤ ∧ (𝐺‘(♯‘𝐴)) ∈ ℤ) → ((𝐺‘(♯‘𝐴)) ∈ (ℤ‘((𝐺‘(𝑚 + 1)) − 1)) ↔ ((𝐺‘(𝑚 + 1)) − 1) ≤ (𝐺‘(♯‘𝐴))))
205186, 203, 204syl2anc 575 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝐺‘(♯‘𝐴)) ∈ (ℤ‘((𝐺‘(𝑚 + 1)) − 1)) ↔ ((𝐺‘(𝑚 + 1)) − 1) ≤ (𝐺‘(♯‘𝐴))))
206202, 205mpbird 248 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(♯‘𝐴)) ∈ (ℤ‘((𝐺‘(𝑚 + 1)) − 1)))
207 uztrn 11921 . . . . . . . . . . . . . . . . . . 19 (((𝐺‘(♯‘𝐴)) ∈ (ℤ‘((𝐺‘(𝑚 + 1)) − 1)) ∧ ((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ‘(𝐺𝑚))) → (𝐺‘(♯‘𝐴)) ∈ (ℤ‘(𝐺𝑚)))
208206, 189, 207syl2anc 575 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(♯‘𝐴)) ∈ (ℤ‘(𝐺𝑚)))
209 fzss2 12604 . . . . . . . . . . . . . . . . . 18 ((𝐺‘(♯‘𝐴)) ∈ (ℤ‘(𝐺𝑚)) → (𝑀...(𝐺𝑚)) ⊆ (𝑀...(𝐺‘(♯‘𝐴))))
210208, 209syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝑀...(𝐺𝑚)) ⊆ (𝑀...(𝐺‘(♯‘𝐴))))
211210sselda 3798 . . . . . . . . . . . . . . . 16 ((((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (𝑀...(𝐺𝑚))) → 𝑘 ∈ (𝑀...(𝐺‘(♯‘𝐴))))
212161, 70sylan 571 . . . . . . . . . . . . . . . 16 ((((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (𝑀...(𝐺‘(♯‘𝐴)))) → (𝐹𝑘) ∈ 𝑆)
213211, 212syldan 581 . . . . . . . . . . . . . . 15 ((((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (𝑀...(𝐺𝑚))) → (𝐹𝑘) ∈ 𝑆)
214 seqcoll.c . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑘𝑆𝑛𝑆)) → (𝑘 + 𝑛) ∈ 𝑆)
215161, 214sylan 571 . . . . . . . . . . . . . . 15 ((((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ (𝑘𝑆𝑛𝑆)) → (𝑘 + 𝑛) ∈ 𝑆)
216167, 213, 215seqcl 13044 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (seq𝑀( + , 𝐹)‘(𝐺𝑚)) ∈ 𝑆)
217 simplll 782 . . . . . . . . . . . . . . 15 ((((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (((𝐺𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1))) → 𝜑)
218 elfzuz 12561 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ (((𝐺𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1)) → 𝑘 ∈ (ℤ‘((𝐺𝑚) + 1)))
219 peano2uz 11959 . . . . . . . . . . . . . . . . . . 19 ((𝐺𝑚) ∈ (ℤ𝑀) → ((𝐺𝑚) + 1) ∈ (ℤ𝑀))
220167, 219syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝐺𝑚) + 1) ∈ (ℤ𝑀))
221 uztrn 11921 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ (ℤ‘((𝐺𝑚) + 1)) ∧ ((𝐺𝑚) + 1) ∈ (ℤ𝑀)) → 𝑘 ∈ (ℤ𝑀))
222218, 220, 221syl2anr 586 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (((𝐺𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1))) → 𝑘 ∈ (ℤ𝑀))
223 elfzuz3 12562 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ (((𝐺𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1)) → ((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ𝑘))
224 uztrn 11921 . . . . . . . . . . . . . . . . . 18 (((𝐺‘(♯‘𝐴)) ∈ (ℤ‘((𝐺‘(𝑚 + 1)) − 1)) ∧ ((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ𝑘)) → (𝐺‘(♯‘𝐴)) ∈ (ℤ𝑘))
225206, 223, 224syl2an 585 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (((𝐺𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1))) → (𝐺‘(♯‘𝐴)) ∈ (ℤ𝑘))
226 elfzuzb 12559 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ (𝑀...(𝐺‘(♯‘𝐴))) ↔ (𝑘 ∈ (ℤ𝑀) ∧ (𝐺‘(♯‘𝐴)) ∈ (ℤ𝑘)))
227222, 225, 226sylanbrc 574 . . . . . . . . . . . . . . . 16 ((((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (((𝐺𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1))) → 𝑘 ∈ (𝑀...(𝐺‘(♯‘𝐴))))
228 elfzle1 12567 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ (((𝐺𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1)) → ((𝐺𝑚) + 1) ≤ 𝑘)
229 elfzle2 12568 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ (((𝐺𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1)) → 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1))
230228, 229jca 503 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ (((𝐺𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1)) → (((𝐺𝑚) + 1) ≤ 𝑘𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1)))
231150ad2antlr 709 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → 𝑚 ∈ ℤ)
23297ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → 𝐺:𝐴⟶(1...(♯‘𝐴)))
233 simprr 780 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → 𝑘𝐴)
234232, 233ffvelrnd 6582 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → (𝐺𝑘) ∈ (1...(♯‘𝐴)))
235 elfzelz 12565 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐺𝑘) ∈ (1...(♯‘𝐴)) → (𝐺𝑘) ∈ ℤ)
236234, 235syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → (𝐺𝑘) ∈ ℤ)
237 btwnnz 11719 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑚 ∈ ℤ ∧ 𝑚 < (𝐺𝑘) ∧ (𝐺𝑘) < (𝑚 + 1)) → ¬ (𝐺𝑘) ∈ ℤ)
2382373expib 1145 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑚 ∈ ℤ → ((𝑚 < (𝐺𝑘) ∧ (𝐺𝑘) < (𝑚 + 1)) → ¬ (𝐺𝑘) ∈ ℤ))
239238con2d 131 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 ∈ ℤ → ((𝐺𝑘) ∈ ℤ → ¬ (𝑚 < (𝐺𝑘) ∧ (𝐺𝑘) < (𝑚 + 1))))
240231, 236, 239sylc 65 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → ¬ (𝑚 < (𝐺𝑘) ∧ (𝐺𝑘) < (𝑚 + 1)))
24131ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → 𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴))
242157adantrr 699 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → 𝑚 ∈ (1...(♯‘𝐴)))
243 isorel 6800 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴) ∧ (𝑚 ∈ (1...(♯‘𝐴)) ∧ (𝐺𝑘) ∈ (1...(♯‘𝐴)))) → (𝑚 < (𝐺𝑘) ↔ (𝐺𝑚) < (𝐺‘(𝐺𝑘))))
244241, 242, 234, 243syl12anc 856 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → (𝑚 < (𝐺𝑘) ↔ (𝐺𝑚) < (𝐺‘(𝐺𝑘))))
24533ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → 𝐺:(1...(♯‘𝐴))–1-1-onto𝐴)
246245, 233, 109syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → (𝐺‘(𝐺𝑘)) = 𝑘)
247246breq2d 4856 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → ((𝐺𝑚) < (𝐺‘(𝐺𝑘)) ↔ (𝐺𝑚) < 𝑘))
248177adantrr 699 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → (𝐺𝑚) ∈ ℤ)
24930ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → 𝐴 ⊆ (ℤ𝑀))
250249, 233sseldd 3799 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → 𝑘 ∈ (ℤ𝑀))
251 eluzelz 11914 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 ∈ (ℤ𝑀) → 𝑘 ∈ ℤ)
252250, 251syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → 𝑘 ∈ ℤ)
253 zltp1le 11693 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐺𝑚) ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((𝐺𝑚) < 𝑘 ↔ ((𝐺𝑚) + 1) ≤ 𝑘))
254248, 252, 253syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → ((𝐺𝑚) < 𝑘 ↔ ((𝐺𝑚) + 1) ≤ 𝑘))
255244, 247, 2543bitrd 296 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → (𝑚 < (𝐺𝑘) ↔ ((𝐺𝑚) + 1) ≤ 𝑘))
256172adantrr 699 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → (𝑚 + 1) ∈ (1...(♯‘𝐴)))
257 isorel 6800 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴) ∧ ((𝐺𝑘) ∈ (1...(♯‘𝐴)) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴)))) → ((𝐺𝑘) < (𝑚 + 1) ↔ (𝐺‘(𝐺𝑘)) < (𝐺‘(𝑚 + 1))))
258241, 234, 256, 257syl12anc 856 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → ((𝐺𝑘) < (𝑚 + 1) ↔ (𝐺‘(𝐺𝑘)) < (𝐺‘(𝑚 + 1))))
259246breq1d 4854 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → ((𝐺‘(𝐺𝑘)) < (𝐺‘(𝑚 + 1)) ↔ 𝑘 < (𝐺‘(𝑚 + 1))))
260181adantrr 699 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → (𝐺‘(𝑚 + 1)) ∈ ℤ)
261 zltlem1 11696 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑘 ∈ ℤ ∧ (𝐺‘(𝑚 + 1)) ∈ ℤ) → (𝑘 < (𝐺‘(𝑚 + 1)) ↔ 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1)))
262252, 260, 261syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → (𝑘 < (𝐺‘(𝑚 + 1)) ↔ 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1)))
263258, 259, 2623bitrd 296 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → ((𝐺𝑘) < (𝑚 + 1) ↔ 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1)))
264255, 263anbi12d 618 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → ((𝑚 < (𝐺𝑘) ∧ (𝐺𝑘) < (𝑚 + 1)) ↔ (((𝐺𝑚) + 1) ≤ 𝑘𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1))))
265240, 264mtbid 315 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → ¬ (((𝐺𝑚) + 1) ≤ 𝑘𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1)))
266265expr 446 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝑘𝐴 → ¬ (((𝐺𝑚) + 1) ≤ 𝑘𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1))))
267266con2d 131 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((((𝐺𝑚) + 1) ≤ 𝑘𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1)) → ¬ 𝑘𝐴))
268230, 267syl5 34 . . . . . . . . . . . . . . . . 17 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝑘 ∈ (((𝐺𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1)) → ¬ 𝑘𝐴))
269268imp 395 . . . . . . . . . . . . . . . 16 ((((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (((𝐺𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1))) → ¬ 𝑘𝐴)
270227, 269eldifd 3780 . . . . . . . . . . . . . . 15 ((((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (((𝐺𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1))) → 𝑘 ∈ ((𝑀...(𝐺‘(♯‘𝐴))) ∖ 𝐴))
271217, 270, 122syl2anc 575 . . . . . . . . . . . . . 14 ((((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (((𝐺𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1))) → (𝐹𝑘) = 𝑍)
272163, 167, 189, 216, 271seqid2 13070 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (seq𝑀( + , 𝐹)‘(𝐺𝑚)) = (seq𝑀( + , 𝐹)‘((𝐺‘(𝑚 + 1)) − 1)))
273272oveq1d 6889 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((seq𝑀( + , 𝐹)‘(𝐺𝑚)) + (𝐹‘(𝐺‘(𝑚 + 1)))) = ((seq𝑀( + , 𝐹)‘((𝐺‘(𝑚 + 1)) − 1)) + (𝐹‘(𝐺‘(𝑚 + 1)))))
274 fveq2 6408 . . . . . . . . . . . . . . . . . 18 (𝑛 = (𝑚 + 1) → (𝐻𝑛) = (𝐻‘(𝑚 + 1)))
275 2fveq3 6413 . . . . . . . . . . . . . . . . . 18 (𝑛 = (𝑚 + 1) → (𝐹‘(𝐺𝑛)) = (𝐹‘(𝐺‘(𝑚 + 1))))
276274, 275eqeq12d 2821 . . . . . . . . . . . . . . . . 17 (𝑛 = (𝑚 + 1) → ((𝐻𝑛) = (𝐹‘(𝐺𝑛)) ↔ (𝐻‘(𝑚 + 1)) = (𝐹‘(𝐺‘(𝑚 + 1)))))
277276imbi2d 331 . . . . . . . . . . . . . . . 16 (𝑛 = (𝑚 + 1) → ((𝜑 → (𝐻𝑛) = (𝐹‘(𝐺𝑛))) ↔ (𝜑 → (𝐻‘(𝑚 + 1)) = (𝐹‘(𝐺‘(𝑚 + 1))))))
278277, 137vtoclga 3465 . . . . . . . . . . . . . . 15 ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (𝜑 → (𝐻‘(𝑚 + 1)) = (𝐹‘(𝐺‘(𝑚 + 1)))))
279278impcom 396 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐻‘(𝑚 + 1)) = (𝐹‘(𝐺‘(𝑚 + 1))))
280279adantlr 697 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐻‘(𝑚 + 1)) = (𝐹‘(𝐺‘(𝑚 + 1))))
281280oveq2d 6890 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((seq𝑀( + , 𝐹)‘(𝐺𝑚)) + (𝐻‘(𝑚 + 1))) = ((seq𝑀( + , 𝐹)‘(𝐺𝑚)) + (𝐹‘(𝐺‘(𝑚 + 1)))))
28290ad2antrr 708 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝑀 ∈ ℤ)
283181zcnd 11749 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(𝑚 + 1)) ∈ ℂ)
284 ax-1cn 10279 . . . . . . . . . . . . . . 15 1 ∈ ℂ
285 npcan 10575 . . . . . . . . . . . . . . 15 (((𝐺‘(𝑚 + 1)) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝐺‘(𝑚 + 1)) − 1) + 1) = (𝐺‘(𝑚 + 1)))
286283, 284, 285sylancl 576 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (((𝐺‘(𝑚 + 1)) − 1) + 1) = (𝐺‘(𝑚 + 1)))
287 uztrn 11921 . . . . . . . . . . . . . . . 16 ((((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ‘(𝐺𝑚)) ∧ (𝐺𝑚) ∈ (ℤ𝑀)) → ((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ𝑀))
288189, 167, 287syl2anc 575 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ𝑀))
289 eluzp1p1 11930 . . . . . . . . . . . . . . 15 (((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ𝑀) → (((𝐺‘(𝑚 + 1)) − 1) + 1) ∈ (ℤ‘(𝑀 + 1)))
290288, 289syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (((𝐺‘(𝑚 + 1)) − 1) + 1) ∈ (ℤ‘(𝑀 + 1)))
291286, 290eqeltrrd 2886 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(𝑚 + 1)) ∈ (ℤ‘(𝑀 + 1)))
292 seqm1 13041 . . . . . . . . . . . . 13 ((𝑀 ∈ ℤ ∧ (𝐺‘(𝑚 + 1)) ∈ (ℤ‘(𝑀 + 1))) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = ((seq𝑀( + , 𝐹)‘((𝐺‘(𝑚 + 1)) − 1)) + (𝐹‘(𝐺‘(𝑚 + 1)))))
293282, 291, 292syl2anc 575 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = ((seq𝑀( + , 𝐹)‘((𝐺‘(𝑚 + 1)) − 1)) + (𝐹‘(𝐺‘(𝑚 + 1)))))
294273, 281, 2933eqtr4rd 2851 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = ((seq𝑀( + , 𝐹)‘(𝐺𝑚)) + (𝐻‘(𝑚 + 1))))
295 seqp1 13039 . . . . . . . . . . . 12 (𝑚 ∈ (ℤ‘1) → (seq1( + , 𝐻)‘(𝑚 + 1)) = ((seq1( + , 𝐻)‘𝑚) + (𝐻‘(𝑚 + 1))))
296149, 295syl 17 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (seq1( + , 𝐻)‘(𝑚 + 1)) = ((seq1( + , 𝐻)‘𝑚) + (𝐻‘(𝑚 + 1))))
297294, 296eqeq12d 2821 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1)) ↔ ((seq𝑀( + , 𝐹)‘(𝐺𝑚)) + (𝐻‘(𝑚 + 1))) = ((seq1( + , 𝐻)‘𝑚) + (𝐻‘(𝑚 + 1)))))
298160, 297syl5ibr 237 . . . . . . . . 9 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((seq𝑀( + , 𝐹)‘(𝐺𝑚)) = (seq1( + , 𝐻)‘𝑚) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1))))
299298ex 399 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ) → ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → ((seq𝑀( + , 𝐹)‘(𝐺𝑚)) = (seq1( + , 𝐻)‘𝑚) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1)))))
300299a2d 29 . . . . . . 7 ((𝜑𝑚 ∈ ℕ) → (((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺𝑚)) = (seq1( + , 𝐻)‘𝑚)) → ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1)))))
301159, 300syld 47 . . . . . 6 ((𝜑𝑚 ∈ ℕ) → ((𝑚 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺𝑚)) = (seq1( + , 𝐻)‘𝑚)) → ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1)))))
302301expcom 400 . . . . 5 (𝑚 ∈ ℕ → (𝜑 → ((𝑚 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺𝑚)) = (seq1( + , 𝐻)‘𝑚)) → ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1))))))
303302a2d 29 . . . 4 (𝑚 ∈ ℕ → ((𝜑 → (𝑚 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺𝑚)) = (seq1( + , 𝐻)‘𝑚))) → (𝜑 → ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1))))))
3049, 15, 21, 27, 146, 303nnind 11323 . . 3 (𝑁 ∈ ℕ → (𝜑 → (𝑁 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺𝑁)) = (seq1( + , 𝐻)‘𝑁))))
3053, 304mpcom 38 . 2 (𝜑 → (𝑁 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺𝑁)) = (seq1( + , 𝐻)‘𝑁)))
3061, 305mpd 15 1 (𝜑 → (seq𝑀( + , 𝐹)‘(𝐺𝑁)) = (seq1( + , 𝐻)‘𝑁))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3a 1100   = wceq 1637  wcel 2156  cdif 3766  wss 3769   class class class wbr 4844  ccnv 5310  cres 5313  wf 6097  1-1-ontowf1o 6100  cfv 6101   Isom wiso 6102  (class class class)co 6874  cc 10219  cr 10220  1c1 10222   + caddc 10224  *cxr 10358   < clt 10359  cle 10360  cmin 10551  cn 11305  cz 11643  cuz 11904  ...cfz 12549  seqcseq 13024  chash 13337
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7179  ax-cnex 10277  ax-resscn 10278  ax-1cn 10279  ax-icn 10280  ax-addcl 10281  ax-addrcl 10282  ax-mulcl 10283  ax-mulrcl 10284  ax-mulcom 10285  ax-addass 10286  ax-mulass 10287  ax-distr 10288  ax-i2m1 10289  ax-1ne0 10290  ax-1rid 10291  ax-rnegex 10292  ax-rrecex 10293  ax-cnre 10294  ax-pre-lttri 10295  ax-pre-lttrn 10296  ax-pre-ltadd 10297  ax-pre-mulgt0 10298
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-nel 3082  df-ral 3101  df-rex 3102  df-reu 3103  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-iun 4714  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6064  df-fun 6103  df-fn 6104  df-f 6105  df-f1 6106  df-fo 6107  df-f1o 6108  df-fv 6109  df-isom 6110  df-riota 6835  df-ov 6877  df-oprab 6878  df-mpt2 6879  df-om 7296  df-1st 7398  df-2nd 7399  df-wrecs 7642  df-recs 7704  df-rdg 7742  df-er 7979  df-en 8193  df-dom 8194  df-sdom 8195  df-pnf 10361  df-mnf 10362  df-xr 10363  df-ltxr 10364  df-le 10365  df-sub 10553  df-neg 10554  df-nn 11306  df-n0 11560  df-z 11644  df-uz 11905  df-fz 12550  df-seq 13025
This theorem is referenced by:  seqcoll2  13466  summolem2a  14669  prodmolem2a  14885
  Copyright terms: Public domain W3C validator