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

Theorem seqcoll 13822
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 12935 . . . 4 (𝑁 ∈ (1...(♯‘𝐴)) → 𝑁 ∈ ℕ)
31, 2syl 17 . . 3 (𝜑𝑁 ∈ ℕ)
4 eleq1 2880 . . . . . 6 (𝑦 = 1 → (𝑦 ∈ (1...(♯‘𝐴)) ↔ 1 ∈ (1...(♯‘𝐴))))
5 2fveq3 6654 . . . . . . 7 (𝑦 = 1 → (seq𝑀( + , 𝐹)‘(𝐺𝑦)) = (seq𝑀( + , 𝐹)‘(𝐺‘1)))
6 fveq2 6649 . . . . . . 7 (𝑦 = 1 → (seq1( + , 𝐻)‘𝑦) = (seq1( + , 𝐻)‘1))
75, 6eqeq12d 2817 . . . . . 6 (𝑦 = 1 → ((seq𝑀( + , 𝐹)‘(𝐺𝑦)) = (seq1( + , 𝐻)‘𝑦) ↔ (seq𝑀( + , 𝐹)‘(𝐺‘1)) = (seq1( + , 𝐻)‘1)))
84, 7imbi12d 348 . . . . 5 (𝑦 = 1 → ((𝑦 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺𝑦)) = (seq1( + , 𝐻)‘𝑦)) ↔ (1 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘1)) = (seq1( + , 𝐻)‘1))))
98imbi2d 344 . . . 4 (𝑦 = 1 → ((𝜑 → (𝑦 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺𝑦)) = (seq1( + , 𝐻)‘𝑦))) ↔ (𝜑 → (1 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘1)) = (seq1( + , 𝐻)‘1)))))
10 eleq1 2880 . . . . . 6 (𝑦 = 𝑚 → (𝑦 ∈ (1...(♯‘𝐴)) ↔ 𝑚 ∈ (1...(♯‘𝐴))))
11 2fveq3 6654 . . . . . . 7 (𝑦 = 𝑚 → (seq𝑀( + , 𝐹)‘(𝐺𝑦)) = (seq𝑀( + , 𝐹)‘(𝐺𝑚)))
12 fveq2 6649 . . . . . . 7 (𝑦 = 𝑚 → (seq1( + , 𝐻)‘𝑦) = (seq1( + , 𝐻)‘𝑚))
1311, 12eqeq12d 2817 . . . . . 6 (𝑦 = 𝑚 → ((seq𝑀( + , 𝐹)‘(𝐺𝑦)) = (seq1( + , 𝐻)‘𝑦) ↔ (seq𝑀( + , 𝐹)‘(𝐺𝑚)) = (seq1( + , 𝐻)‘𝑚)))
1410, 13imbi12d 348 . . . . 5 (𝑦 = 𝑚 → ((𝑦 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺𝑦)) = (seq1( + , 𝐻)‘𝑦)) ↔ (𝑚 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺𝑚)) = (seq1( + , 𝐻)‘𝑚))))
1514imbi2d 344 . . . 4 (𝑦 = 𝑚 → ((𝜑 → (𝑦 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺𝑦)) = (seq1( + , 𝐻)‘𝑦))) ↔ (𝜑 → (𝑚 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺𝑚)) = (seq1( + , 𝐻)‘𝑚)))))
16 eleq1 2880 . . . . . 6 (𝑦 = (𝑚 + 1) → (𝑦 ∈ (1...(♯‘𝐴)) ↔ (𝑚 + 1) ∈ (1...(♯‘𝐴))))
17 2fveq3 6654 . . . . . . 7 (𝑦 = (𝑚 + 1) → (seq𝑀( + , 𝐹)‘(𝐺𝑦)) = (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))))
18 fveq2 6649 . . . . . . 7 (𝑦 = (𝑚 + 1) → (seq1( + , 𝐻)‘𝑦) = (seq1( + , 𝐻)‘(𝑚 + 1)))
1917, 18eqeq12d 2817 . . . . . 6 (𝑦 = (𝑚 + 1) → ((seq𝑀( + , 𝐹)‘(𝐺𝑦)) = (seq1( + , 𝐻)‘𝑦) ↔ (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1))))
2016, 19imbi12d 348 . . . . 5 (𝑦 = (𝑚 + 1) → ((𝑦 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺𝑦)) = (seq1( + , 𝐻)‘𝑦)) ↔ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1)))))
2120imbi2d 344 . . . 4 (𝑦 = (𝑚 + 1) → ((𝜑 → (𝑦 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺𝑦)) = (seq1( + , 𝐻)‘𝑦))) ↔ (𝜑 → ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1))))))
22 eleq1 2880 . . . . . 6 (𝑦 = 𝑁 → (𝑦 ∈ (1...(♯‘𝐴)) ↔ 𝑁 ∈ (1...(♯‘𝐴))))
23 2fveq3 6654 . . . . . . 7 (𝑦 = 𝑁 → (seq𝑀( + , 𝐹)‘(𝐺𝑦)) = (seq𝑀( + , 𝐹)‘(𝐺𝑁)))
24 fveq2 6649 . . . . . . 7 (𝑦 = 𝑁 → (seq1( + , 𝐻)‘𝑦) = (seq1( + , 𝐻)‘𝑁))
2523, 24eqeq12d 2817 . . . . . 6 (𝑦 = 𝑁 → ((seq𝑀( + , 𝐹)‘(𝐺𝑦)) = (seq1( + , 𝐻)‘𝑦) ↔ (seq𝑀( + , 𝐹)‘(𝐺𝑁)) = (seq1( + , 𝐻)‘𝑁)))
2622, 25imbi12d 348 . . . . 5 (𝑦 = 𝑁 → ((𝑦 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺𝑦)) = (seq1( + , 𝐻)‘𝑦)) ↔ (𝑁 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺𝑁)) = (seq1( + , 𝐻)‘𝑁))))
2726imbi2d 344 . . . 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 7059 . . . . . . . . . . . . 13 (𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴) → 𝐺:(1...(♯‘𝐴))–1-1-onto𝐴)
3331, 32syl 17 . . . . . . . . . . . 12 (𝜑𝐺:(1...(♯‘𝐴))–1-1-onto𝐴)
34 f1of 6594 . . . . . . . . . . . 12 (𝐺:(1...(♯‘𝐴))–1-1-onto𝐴𝐺:(1...(♯‘𝐴))⟶𝐴)
3533, 34syl 17 . . . . . . . . . . 11 (𝜑𝐺:(1...(♯‘𝐴))⟶𝐴)
36 elfzuz2 12911 . . . . . . . . . . . . 13 (𝑁 ∈ (1...(♯‘𝐴)) → (♯‘𝐴) ∈ (ℤ‘1))
371, 36syl 17 . . . . . . . . . . . 12 (𝜑 → (♯‘𝐴) ∈ (ℤ‘1))
38 eluzfz1 12913 . . . . . . . . . . . 12 ((♯‘𝐴) ∈ (ℤ‘1) → 1 ∈ (1...(♯‘𝐴)))
3937, 38syl 17 . . . . . . . . . . 11 (𝜑 → 1 ∈ (1...(♯‘𝐴)))
4035, 39ffvelrnd 6833 . . . . . . . . . 10 (𝜑 → (𝐺‘1) ∈ 𝐴)
4130, 40sseldd 3919 . . . . . . . . 9 (𝜑 → (𝐺‘1) ∈ (ℤ𝑀))
42 eluzle 12248 . . . . . . . . . . . . 13 ((♯‘𝐴) ∈ (ℤ‘1) → 1 ≤ (♯‘𝐴))
4337, 42syl 17 . . . . . . . . . . . 12 (𝜑 → 1 ≤ (♯‘𝐴))
44 fzssz 12908 . . . . . . . . . . . . . . . 16 (1...(♯‘𝐴)) ⊆ ℤ
45 zssre 11980 . . . . . . . . . . . . . . . 16 ℤ ⊆ ℝ
4644, 45sstri 3927 . . . . . . . . . . . . . . 15 (1...(♯‘𝐴)) ⊆ ℝ
4746a1i 11 . . . . . . . . . . . . . 14 (𝜑 → (1...(♯‘𝐴)) ⊆ ℝ)
48 ressxr 10678 . . . . . . . . . . . . . 14 ℝ ⊆ ℝ*
4947, 48sstrdi 3930 . . . . . . . . . . . . 13 (𝜑 → (1...(♯‘𝐴)) ⊆ ℝ*)
50 eluzelre 12246 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (ℤ𝑀) → 𝑘 ∈ ℝ)
5150ssriv 3922 . . . . . . . . . . . . . . 15 (ℤ𝑀) ⊆ ℝ
5230, 51sstrdi 3930 . . . . . . . . . . . . . 14 (𝜑𝐴 ⊆ ℝ)
5352, 48sstrdi 3930 . . . . . . . . . . . . 13 (𝜑𝐴 ⊆ ℝ*)
54 eluzfz2 12914 . . . . . . . . . . . . . 14 ((♯‘𝐴) ∈ (ℤ‘1) → (♯‘𝐴) ∈ (1...(♯‘𝐴)))
5537, 54syl 17 . . . . . . . . . . . . 13 (𝜑 → (♯‘𝐴) ∈ (1...(♯‘𝐴)))
56 leisorel 13818 . . . . . . . . . . . . 13 ((𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴) ∧ ((1...(♯‘𝐴)) ⊆ ℝ*𝐴 ⊆ ℝ*) ∧ (1 ∈ (1...(♯‘𝐴)) ∧ (♯‘𝐴) ∈ (1...(♯‘𝐴)))) → (1 ≤ (♯‘𝐴) ↔ (𝐺‘1) ≤ (𝐺‘(♯‘𝐴))))
5731, 49, 53, 39, 55, 56syl122anc 1376 . . . . . . . . . . . 12 (𝜑 → (1 ≤ (♯‘𝐴) ↔ (𝐺‘1) ≤ (𝐺‘(♯‘𝐴))))
5843, 57mpbid 235 . . . . . . . . . . 11 (𝜑 → (𝐺‘1) ≤ (𝐺‘(♯‘𝐴)))
5935, 55ffvelrnd 6833 . . . . . . . . . . . . . 14 (𝜑 → (𝐺‘(♯‘𝐴)) ∈ 𝐴)
6030, 59sseldd 3919 . . . . . . . . . . . . 13 (𝜑 → (𝐺‘(♯‘𝐴)) ∈ (ℤ𝑀))
61 eluzelz 12245 . . . . . . . . . . . . 13 ((𝐺‘(♯‘𝐴)) ∈ (ℤ𝑀) → (𝐺‘(♯‘𝐴)) ∈ ℤ)
6260, 61syl 17 . . . . . . . . . . . 12 (𝜑 → (𝐺‘(♯‘𝐴)) ∈ ℤ)
63 elfz5 12898 . . . . . . . . . . . 12 (((𝐺‘1) ∈ (ℤ𝑀) ∧ (𝐺‘(♯‘𝐴)) ∈ ℤ) → ((𝐺‘1) ∈ (𝑀...(𝐺‘(♯‘𝐴))) ↔ (𝐺‘1) ≤ (𝐺‘(♯‘𝐴))))
6441, 62, 63syl2anc 587 . . . . . . . . . . 11 (𝜑 → ((𝐺‘1) ∈ (𝑀...(𝐺‘(♯‘𝐴))) ↔ (𝐺‘1) ≤ (𝐺‘(♯‘𝐴))))
6558, 64mpbird 260 . . . . . . . . . 10 (𝜑 → (𝐺‘1) ∈ (𝑀...(𝐺‘(♯‘𝐴))))
66 fveq2 6649 . . . . . . . . . . . . 13 (𝑘 = (𝐺‘1) → (𝐹𝑘) = (𝐹‘(𝐺‘1)))
6766eleq1d 2877 . . . . . . . . . . . 12 (𝑘 = (𝐺‘1) → ((𝐹𝑘) ∈ 𝑆 ↔ (𝐹‘(𝐺‘1)) ∈ 𝑆))
6867imbi2d 344 . . . . . . . . . . 11 (𝑘 = (𝐺‘1) → ((𝜑 → (𝐹𝑘) ∈ 𝑆) ↔ (𝜑 → (𝐹‘(𝐺‘1)) ∈ 𝑆)))
69 seqcoll.5 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (𝑀...(𝐺‘(♯‘𝐴)))) → (𝐹𝑘) ∈ 𝑆)
7069expcom 417 . . . . . . . . . . 11 (𝑘 ∈ (𝑀...(𝐺‘(♯‘𝐴))) → (𝜑 → (𝐹𝑘) ∈ 𝑆))
7168, 70vtoclga 3525 . . . . . . . . . 10 ((𝐺‘1) ∈ (𝑀...(𝐺‘(♯‘𝐴))) → (𝜑 → (𝐹‘(𝐺‘1)) ∈ 𝑆))
7265, 71mpcom 38 . . . . . . . . 9 (𝜑 → (𝐹‘(𝐺‘1)) ∈ 𝑆)
73 eluzelz 12245 . . . . . . . . . . . . . . . . . 18 ((𝐺‘1) ∈ (ℤ𝑀) → (𝐺‘1) ∈ ℤ)
7441, 73syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐺‘1) ∈ ℤ)
75 peano2zm 12017 . . . . . . . . . . . . . . . . 17 ((𝐺‘1) ∈ ℤ → ((𝐺‘1) − 1) ∈ ℤ)
7674, 75syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐺‘1) − 1) ∈ ℤ)
7776zred 12079 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐺‘1) − 1) ∈ ℝ)
7874zred 12079 . . . . . . . . . . . . . . 15 (𝜑 → (𝐺‘1) ∈ ℝ)
7962zred 12079 . . . . . . . . . . . . . . 15 (𝜑 → (𝐺‘(♯‘𝐴)) ∈ ℝ)
8078lem1d 11566 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐺‘1) − 1) ≤ (𝐺‘1))
8177, 78, 79, 80, 58letrd 10790 . . . . . . . . . . . . . 14 (𝜑 → ((𝐺‘1) − 1) ≤ (𝐺‘(♯‘𝐴)))
82 eluz 12249 . . . . . . . . . . . . . . 15 ((((𝐺‘1) − 1) ∈ ℤ ∧ (𝐺‘(♯‘𝐴)) ∈ ℤ) → ((𝐺‘(♯‘𝐴)) ∈ (ℤ‘((𝐺‘1) − 1)) ↔ ((𝐺‘1) − 1) ≤ (𝐺‘(♯‘𝐴))))
8376, 62, 82syl2anc 587 . . . . . . . . . . . . . 14 (𝜑 → ((𝐺‘(♯‘𝐴)) ∈ (ℤ‘((𝐺‘1) − 1)) ↔ ((𝐺‘1) − 1) ≤ (𝐺‘(♯‘𝐴))))
8481, 83mpbird 260 . . . . . . . . . . . . 13 (𝜑 → (𝐺‘(♯‘𝐴)) ∈ (ℤ‘((𝐺‘1) − 1)))
85 fzss2 12946 . . . . . . . . . . . . 13 ((𝐺‘(♯‘𝐴)) ∈ (ℤ‘((𝐺‘1) − 1)) → (𝑀...((𝐺‘1) − 1)) ⊆ (𝑀...(𝐺‘(♯‘𝐴))))
8684, 85syl 17 . . . . . . . . . . . 12 (𝜑 → (𝑀...((𝐺‘1) − 1)) ⊆ (𝑀...(𝐺‘(♯‘𝐴))))
8786sselda 3918 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (𝑀...((𝐺‘1) − 1))) → 𝑘 ∈ (𝑀...(𝐺‘(♯‘𝐴))))
88 eluzel2 12240 . . . . . . . . . . . . . . 15 ((𝐺‘1) ∈ (ℤ𝑀) → 𝑀 ∈ ℤ)
8941, 88syl 17 . . . . . . . . . . . . . 14 (𝜑𝑀 ∈ ℤ)
90 elfzm11 12977 . . . . . . . . . . . . . 14 ((𝑀 ∈ ℤ ∧ (𝐺‘1) ∈ ℤ) → (𝑘 ∈ (𝑀...((𝐺‘1) − 1)) ↔ (𝑘 ∈ ℤ ∧ 𝑀𝑘𝑘 < (𝐺‘1))))
9189, 74, 90syl2anc 587 . . . . . . . . . . . . 13 (𝜑 → (𝑘 ∈ (𝑀...((𝐺‘1) − 1)) ↔ (𝑘 ∈ ℤ ∧ 𝑀𝑘𝑘 < (𝐺‘1))))
92 simp3 1135 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℤ ∧ 𝑀𝑘𝑘 < (𝐺‘1)) → 𝑘 < (𝐺‘1))
9378adantr 484 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝐴) → (𝐺‘1) ∈ ℝ)
9452sselda 3918 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝐴) → 𝑘 ∈ ℝ)
95 f1ocnv 6606 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐺:(1...(♯‘𝐴))–1-1-onto𝐴𝐺:𝐴1-1-onto→(1...(♯‘𝐴)))
9633, 95syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐺:𝐴1-1-onto→(1...(♯‘𝐴)))
97 f1of 6594 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐺:𝐴1-1-onto→(1...(♯‘𝐴)) → 𝐺:𝐴⟶(1...(♯‘𝐴)))
9896, 97syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐺:𝐴⟶(1...(♯‘𝐴)))
9998ffvelrnda 6832 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘𝐴) → (𝐺𝑘) ∈ (1...(♯‘𝐴)))
100 elfznn 12935 . . . . . . . . . . . . . . . . . . . . 21 ((𝐺𝑘) ∈ (1...(♯‘𝐴)) → (𝐺𝑘) ∈ ℕ)
10199, 100syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘𝐴) → (𝐺𝑘) ∈ ℕ)
102101nnge1d 11677 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘𝐴) → 1 ≤ (𝐺𝑘))
10331adantr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘𝐴) → 𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴))
10449adantr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘𝐴) → (1...(♯‘𝐴)) ⊆ ℝ*)
10553adantr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘𝐴) → 𝐴 ⊆ ℝ*)
10639adantr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘𝐴) → 1 ∈ (1...(♯‘𝐴)))
107 leisorel 13818 . . . . . . . . . . . . . . . . . . . 20 ((𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴) ∧ ((1...(♯‘𝐴)) ⊆ ℝ*𝐴 ⊆ ℝ*) ∧ (1 ∈ (1...(♯‘𝐴)) ∧ (𝐺𝑘) ∈ (1...(♯‘𝐴)))) → (1 ≤ (𝐺𝑘) ↔ (𝐺‘1) ≤ (𝐺‘(𝐺𝑘))))
108103, 104, 105, 106, 99, 107syl122anc 1376 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘𝐴) → (1 ≤ (𝐺𝑘) ↔ (𝐺‘1) ≤ (𝐺‘(𝐺𝑘))))
109102, 108mpbid 235 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘𝐴) → (𝐺‘1) ≤ (𝐺‘(𝐺𝑘)))
110 f1ocnvfv2 7016 . . . . . . . . . . . . . . . . . . 19 ((𝐺:(1...(♯‘𝐴))–1-1-onto𝐴𝑘𝐴) → (𝐺‘(𝐺𝑘)) = 𝑘)
11133, 110sylan 583 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘𝐴) → (𝐺‘(𝐺𝑘)) = 𝑘)
112109, 111breqtrd 5059 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝐴) → (𝐺‘1) ≤ 𝑘)
11393, 94, 112lensymd 10784 . . . . . . . . . . . . . . . 16 ((𝜑𝑘𝐴) → ¬ 𝑘 < (𝐺‘1))
114113ex 416 . . . . . . . . . . . . . . 15 (𝜑 → (𝑘𝐴 → ¬ 𝑘 < (𝐺‘1)))
115114con2d 136 . . . . . . . . . . . . . 14 (𝜑 → (𝑘 < (𝐺‘1) → ¬ 𝑘𝐴))
11692, 115syl5 34 . . . . . . . . . . . . 13 (𝜑 → ((𝑘 ∈ ℤ ∧ 𝑀𝑘𝑘 < (𝐺‘1)) → ¬ 𝑘𝐴))
11791, 116sylbid 243 . . . . . . . . . . . 12 (𝜑 → (𝑘 ∈ (𝑀...((𝐺‘1) − 1)) → ¬ 𝑘𝐴))
118117imp 410 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (𝑀...((𝐺‘1) − 1))) → ¬ 𝑘𝐴)
11987, 118eldifd 3895 . . . . . . . . . 10 ((𝜑𝑘 ∈ (𝑀...((𝐺‘1) − 1))) → 𝑘 ∈ ((𝑀...(𝐺‘(♯‘𝐴))) ∖ 𝐴))
120 seqcoll.6 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝑀...(𝐺‘(♯‘𝐴))) ∖ 𝐴)) → (𝐹𝑘) = 𝑍)
121119, 120syldan 594 . . . . . . . . 9 ((𝜑𝑘 ∈ (𝑀...((𝐺‘1) − 1))) → (𝐹𝑘) = 𝑍)
12228, 29, 41, 72, 121seqid 13415 . . . . . . . 8 (𝜑 → (seq𝑀( + , 𝐹) ↾ (ℤ‘(𝐺‘1))) = seq(𝐺‘1)( + , 𝐹))
123122fveq1d 6651 . . . . . . 7 (𝜑 → ((seq𝑀( + , 𝐹) ↾ (ℤ‘(𝐺‘1)))‘(𝐺‘1)) = (seq(𝐺‘1)( + , 𝐹)‘(𝐺‘1)))
124 uzid 12250 . . . . . . . . 9 ((𝐺‘1) ∈ ℤ → (𝐺‘1) ∈ (ℤ‘(𝐺‘1)))
12574, 124syl 17 . . . . . . . 8 (𝜑 → (𝐺‘1) ∈ (ℤ‘(𝐺‘1)))
126125fvresd 6669 . . . . . . 7 (𝜑 → ((seq𝑀( + , 𝐹) ↾ (ℤ‘(𝐺‘1)))‘(𝐺‘1)) = (seq𝑀( + , 𝐹)‘(𝐺‘1)))
127 seq1 13381 . . . . . . . . 9 ((𝐺‘1) ∈ ℤ → (seq(𝐺‘1)( + , 𝐹)‘(𝐺‘1)) = (𝐹‘(𝐺‘1)))
12874, 127syl 17 . . . . . . . 8 (𝜑 → (seq(𝐺‘1)( + , 𝐹)‘(𝐺‘1)) = (𝐹‘(𝐺‘1)))
129 fveq2 6649 . . . . . . . . . . . 12 (𝑛 = 1 → (𝐻𝑛) = (𝐻‘1))
130 2fveq3 6654 . . . . . . . . . . . 12 (𝑛 = 1 → (𝐹‘(𝐺𝑛)) = (𝐹‘(𝐺‘1)))
131129, 130eqeq12d 2817 . . . . . . . . . . 11 (𝑛 = 1 → ((𝐻𝑛) = (𝐹‘(𝐺𝑛)) ↔ (𝐻‘1) = (𝐹‘(𝐺‘1))))
132131imbi2d 344 . . . . . . . . . 10 (𝑛 = 1 → ((𝜑 → (𝐻𝑛) = (𝐹‘(𝐺𝑛))) ↔ (𝜑 → (𝐻‘1) = (𝐹‘(𝐺‘1)))))
133 seqcoll.7 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...(♯‘𝐴))) → (𝐻𝑛) = (𝐹‘(𝐺𝑛)))
134133expcom 417 . . . . . . . . . 10 (𝑛 ∈ (1...(♯‘𝐴)) → (𝜑 → (𝐻𝑛) = (𝐹‘(𝐺𝑛))))
135132, 134vtoclga 3525 . . . . . . . . 9 (1 ∈ (1...(♯‘𝐴)) → (𝜑 → (𝐻‘1) = (𝐹‘(𝐺‘1))))
13639, 135mpcom 38 . . . . . . . 8 (𝜑 → (𝐻‘1) = (𝐹‘(𝐺‘1)))
137128, 136eqtr4d 2839 . . . . . . 7 (𝜑 → (seq(𝐺‘1)( + , 𝐹)‘(𝐺‘1)) = (𝐻‘1))
138123, 126, 1373eqtr3d 2844 . . . . . 6 (𝜑 → (seq𝑀( + , 𝐹)‘(𝐺‘1)) = (𝐻‘1))
139 1z 12004 . . . . . . 7 1 ∈ ℤ
140 seq1 13381 . . . . . . 7 (1 ∈ ℤ → (seq1( + , 𝐻)‘1) = (𝐻‘1))
141139, 140ax-mp 5 . . . . . 6 (seq1( + , 𝐻)‘1) = (𝐻‘1)
142138, 141eqtr4di 2854 . . . . 5 (𝜑 → (seq𝑀( + , 𝐹)‘(𝐺‘1)) = (seq1( + , 𝐻)‘1))
143142a1d 25 . . . 4 (𝜑 → (1 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘1)) = (seq1( + , 𝐻)‘1)))
144 simplr 768 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝑚 ∈ ℕ)
145 nnuz 12273 . . . . . . . . . . 11 ℕ = (ℤ‘1)
146144, 145eleqtrdi 2903 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝑚 ∈ (ℤ‘1))
147 nnz 11996 . . . . . . . . . . . 12 (𝑚 ∈ ℕ → 𝑚 ∈ ℤ)
148147ad2antlr 726 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝑚 ∈ ℤ)
149 elfzuz3 12903 . . . . . . . . . . . 12 ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (♯‘𝐴) ∈ (ℤ‘(𝑚 + 1)))
150149adantl 485 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (♯‘𝐴) ∈ (ℤ‘(𝑚 + 1)))
151 peano2uzr 12295 . . . . . . . . . . 11 ((𝑚 ∈ ℤ ∧ (♯‘𝐴) ∈ (ℤ‘(𝑚 + 1))) → (♯‘𝐴) ∈ (ℤ𝑚))
152148, 150, 151syl2anc 587 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (♯‘𝐴) ∈ (ℤ𝑚))
153 elfzuzb 12900 . . . . . . . . . 10 (𝑚 ∈ (1...(♯‘𝐴)) ↔ (𝑚 ∈ (ℤ‘1) ∧ (♯‘𝐴) ∈ (ℤ𝑚)))
154146, 152, 153sylanbrc 586 . . . . . . . . 9 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝑚 ∈ (1...(♯‘𝐴)))
155154ex 416 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ) → ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → 𝑚 ∈ (1...(♯‘𝐴))))
156155imim1d 82 . . . . . . 7 ((𝜑𝑚 ∈ ℕ) → ((𝑚 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺𝑚)) = (seq1( + , 𝐻)‘𝑚)) → ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺𝑚)) = (seq1( + , 𝐻)‘𝑚))))
157 oveq1 7146 . . . . . . . . . 10 ((seq𝑀( + , 𝐹)‘(𝐺𝑚)) = (seq1( + , 𝐻)‘𝑚) → ((seq𝑀( + , 𝐹)‘(𝐺𝑚)) + (𝐻‘(𝑚 + 1))) = ((seq1( + , 𝐻)‘𝑚) + (𝐻‘(𝑚 + 1))))
158 seqcoll.1b . . . . . . . . . . . . . . 15 ((𝜑𝑘𝑆) → (𝑘 + 𝑍) = 𝑘)
159158ad4ant14 751 . . . . . . . . . . . . . 14 ((((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘𝑆) → (𝑘 + 𝑍) = 𝑘)
16030ad2antrr 725 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝐴 ⊆ (ℤ𝑀))
16135ad2antrr 725 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝐺:(1...(♯‘𝐴))⟶𝐴)
162161, 154ffvelrnd 6833 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺𝑚) ∈ 𝐴)
163160, 162sseldd 3919 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺𝑚) ∈ (ℤ𝑀))
164 nnre 11636 . . . . . . . . . . . . . . . . . . 19 (𝑚 ∈ ℕ → 𝑚 ∈ ℝ)
165164ad2antlr 726 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝑚 ∈ ℝ)
166165ltp1d 11563 . . . . . . . . . . . . . . . . 17 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝑚 < (𝑚 + 1))
16731ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴))
168 simpr 488 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝑚 + 1) ∈ (1...(♯‘𝐴)))
169 isorel 7062 . . . . . . . . . . . . . . . . . 18 ((𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴) ∧ (𝑚 ∈ (1...(♯‘𝐴)) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴)))) → (𝑚 < (𝑚 + 1) ↔ (𝐺𝑚) < (𝐺‘(𝑚 + 1))))
170167, 154, 168, 169syl12anc 835 . . . . . . . . . . . . . . . . 17 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝑚 < (𝑚 + 1) ↔ (𝐺𝑚) < (𝐺‘(𝑚 + 1))))
171166, 170mpbid 235 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺𝑚) < (𝐺‘(𝑚 + 1)))
172 eluzelz 12245 . . . . . . . . . . . . . . . . . 18 ((𝐺𝑚) ∈ (ℤ𝑀) → (𝐺𝑚) ∈ ℤ)
173163, 172syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺𝑚) ∈ ℤ)
174161, 168ffvelrnd 6833 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(𝑚 + 1)) ∈ 𝐴)
175160, 174sseldd 3919 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(𝑚 + 1)) ∈ (ℤ𝑀))
176 eluzelz 12245 . . . . . . . . . . . . . . . . . 18 ((𝐺‘(𝑚 + 1)) ∈ (ℤ𝑀) → (𝐺‘(𝑚 + 1)) ∈ ℤ)
177175, 176syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(𝑚 + 1)) ∈ ℤ)
178 zltlem1 12027 . . . . . . . . . . . . . . . . 17 (((𝐺𝑚) ∈ ℤ ∧ (𝐺‘(𝑚 + 1)) ∈ ℤ) → ((𝐺𝑚) < (𝐺‘(𝑚 + 1)) ↔ (𝐺𝑚) ≤ ((𝐺‘(𝑚 + 1)) − 1)))
179173, 177, 178syl2anc 587 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝐺𝑚) < (𝐺‘(𝑚 + 1)) ↔ (𝐺𝑚) ≤ ((𝐺‘(𝑚 + 1)) − 1)))
180171, 179mpbid 235 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺𝑚) ≤ ((𝐺‘(𝑚 + 1)) − 1))
181 peano2zm 12017 . . . . . . . . . . . . . . . . 17 ((𝐺‘(𝑚 + 1)) ∈ ℤ → ((𝐺‘(𝑚 + 1)) − 1) ∈ ℤ)
182177, 181syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝐺‘(𝑚 + 1)) − 1) ∈ ℤ)
183 eluz 12249 . . . . . . . . . . . . . . . 16 (((𝐺𝑚) ∈ ℤ ∧ ((𝐺‘(𝑚 + 1)) − 1) ∈ ℤ) → (((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ‘(𝐺𝑚)) ↔ (𝐺𝑚) ≤ ((𝐺‘(𝑚 + 1)) − 1)))
184173, 182, 183syl2anc 587 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ‘(𝐺𝑚)) ↔ (𝐺𝑚) ≤ ((𝐺‘(𝑚 + 1)) − 1)))
185180, 184mpbird 260 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ‘(𝐺𝑚)))
186182zred 12079 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝐺‘(𝑚 + 1)) − 1) ∈ ℝ)
187177zred 12079 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(𝑚 + 1)) ∈ ℝ)
18879ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(♯‘𝐴)) ∈ ℝ)
189187lem1d 11566 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝐺‘(𝑚 + 1)) − 1) ≤ (𝐺‘(𝑚 + 1)))
190 elfzle2 12910 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (𝑚 + 1) ≤ (♯‘𝐴))
191190adantl 485 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝑚 + 1) ≤ (♯‘𝐴))
19249ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (1...(♯‘𝐴)) ⊆ ℝ*)
19353ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝐴 ⊆ ℝ*)
19455ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (♯‘𝐴) ∈ (1...(♯‘𝐴)))
195 leisorel 13818 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴) ∧ ((1...(♯‘𝐴)) ⊆ ℝ*𝐴 ⊆ ℝ*) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ (♯‘𝐴) ∈ (1...(♯‘𝐴)))) → ((𝑚 + 1) ≤ (♯‘𝐴) ↔ (𝐺‘(𝑚 + 1)) ≤ (𝐺‘(♯‘𝐴))))
196167, 192, 193, 168, 194, 195syl122anc 1376 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝑚 + 1) ≤ (♯‘𝐴) ↔ (𝐺‘(𝑚 + 1)) ≤ (𝐺‘(♯‘𝐴))))
197191, 196mpbid 235 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(𝑚 + 1)) ≤ (𝐺‘(♯‘𝐴)))
198186, 187, 188, 189, 197letrd 10790 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝐺‘(𝑚 + 1)) − 1) ≤ (𝐺‘(♯‘𝐴)))
19962ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(♯‘𝐴)) ∈ ℤ)
200 eluz 12249 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐺‘(𝑚 + 1)) − 1) ∈ ℤ ∧ (𝐺‘(♯‘𝐴)) ∈ ℤ) → ((𝐺‘(♯‘𝐴)) ∈ (ℤ‘((𝐺‘(𝑚 + 1)) − 1)) ↔ ((𝐺‘(𝑚 + 1)) − 1) ≤ (𝐺‘(♯‘𝐴))))
201182, 199, 200syl2anc 587 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝐺‘(♯‘𝐴)) ∈ (ℤ‘((𝐺‘(𝑚 + 1)) − 1)) ↔ ((𝐺‘(𝑚 + 1)) − 1) ≤ (𝐺‘(♯‘𝐴))))
202198, 201mpbird 260 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(♯‘𝐴)) ∈ (ℤ‘((𝐺‘(𝑚 + 1)) − 1)))
203 uztrn 12253 . . . . . . . . . . . . . . . . . . 19 (((𝐺‘(♯‘𝐴)) ∈ (ℤ‘((𝐺‘(𝑚 + 1)) − 1)) ∧ ((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ‘(𝐺𝑚))) → (𝐺‘(♯‘𝐴)) ∈ (ℤ‘(𝐺𝑚)))
204202, 185, 203syl2anc 587 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(♯‘𝐴)) ∈ (ℤ‘(𝐺𝑚)))
205 fzss2 12946 . . . . . . . . . . . . . . . . . 18 ((𝐺‘(♯‘𝐴)) ∈ (ℤ‘(𝐺𝑚)) → (𝑀...(𝐺𝑚)) ⊆ (𝑀...(𝐺‘(♯‘𝐴))))
206204, 205syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝑀...(𝐺𝑚)) ⊆ (𝑀...(𝐺‘(♯‘𝐴))))
207206sselda 3918 . . . . . . . . . . . . . . . 16 ((((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (𝑀...(𝐺𝑚))) → 𝑘 ∈ (𝑀...(𝐺‘(♯‘𝐴))))
20869ad4ant14 751 . . . . . . . . . . . . . . . 16 ((((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (𝑀...(𝐺‘(♯‘𝐴)))) → (𝐹𝑘) ∈ 𝑆)
209207, 208syldan 594 . . . . . . . . . . . . . . 15 ((((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (𝑀...(𝐺𝑚))) → (𝐹𝑘) ∈ 𝑆)
210 seqcoll.c . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑘𝑆𝑛𝑆)) → (𝑘 + 𝑛) ∈ 𝑆)
211210ad4ant14 751 . . . . . . . . . . . . . . 15 ((((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ (𝑘𝑆𝑛𝑆)) → (𝑘 + 𝑛) ∈ 𝑆)
212163, 209, 211seqcl 13390 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (seq𝑀( + , 𝐹)‘(𝐺𝑚)) ∈ 𝑆)
213 simplll 774 . . . . . . . . . . . . . . 15 ((((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (((𝐺𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1))) → 𝜑)
214 elfzuz 12902 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ (((𝐺𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1)) → 𝑘 ∈ (ℤ‘((𝐺𝑚) + 1)))
215 peano2uz 12293 . . . . . . . . . . . . . . . . . . 19 ((𝐺𝑚) ∈ (ℤ𝑀) → ((𝐺𝑚) + 1) ∈ (ℤ𝑀))
216163, 215syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝐺𝑚) + 1) ∈ (ℤ𝑀))
217 uztrn 12253 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ (ℤ‘((𝐺𝑚) + 1)) ∧ ((𝐺𝑚) + 1) ∈ (ℤ𝑀)) → 𝑘 ∈ (ℤ𝑀))
218214, 216, 217syl2anr 599 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (((𝐺𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1))) → 𝑘 ∈ (ℤ𝑀))
219 elfzuz3 12903 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ (((𝐺𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1)) → ((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ𝑘))
220 uztrn 12253 . . . . . . . . . . . . . . . . . 18 (((𝐺‘(♯‘𝐴)) ∈ (ℤ‘((𝐺‘(𝑚 + 1)) − 1)) ∧ ((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ𝑘)) → (𝐺‘(♯‘𝐴)) ∈ (ℤ𝑘))
221202, 219, 220syl2an 598 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (((𝐺𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1))) → (𝐺‘(♯‘𝐴)) ∈ (ℤ𝑘))
222 elfzuzb 12900 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ (𝑀...(𝐺‘(♯‘𝐴))) ↔ (𝑘 ∈ (ℤ𝑀) ∧ (𝐺‘(♯‘𝐴)) ∈ (ℤ𝑘)))
223218, 221, 222sylanbrc 586 . . . . . . . . . . . . . . . 16 ((((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (((𝐺𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1))) → 𝑘 ∈ (𝑀...(𝐺‘(♯‘𝐴))))
224147ad2antlr 726 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → 𝑚 ∈ ℤ)
22598ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → 𝐺:𝐴⟶(1...(♯‘𝐴)))
226 simprr 772 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → 𝑘𝐴)
227225, 226ffvelrnd 6833 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → (𝐺𝑘) ∈ (1...(♯‘𝐴)))
228 elfzelz 12906 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐺𝑘) ∈ (1...(♯‘𝐴)) → (𝐺𝑘) ∈ ℤ)
229227, 228syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → (𝐺𝑘) ∈ ℤ)
230 btwnnz 12050 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑚 ∈ ℤ ∧ 𝑚 < (𝐺𝑘) ∧ (𝐺𝑘) < (𝑚 + 1)) → ¬ (𝐺𝑘) ∈ ℤ)
2312303expib 1119 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 ∈ ℤ → ((𝑚 < (𝐺𝑘) ∧ (𝐺𝑘) < (𝑚 + 1)) → ¬ (𝐺𝑘) ∈ ℤ))
232231con2d 136 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 ∈ ℤ → ((𝐺𝑘) ∈ ℤ → ¬ (𝑚 < (𝐺𝑘) ∧ (𝐺𝑘) < (𝑚 + 1))))
233224, 229, 232sylc 65 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → ¬ (𝑚 < (𝐺𝑘) ∧ (𝐺𝑘) < (𝑚 + 1)))
23431ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → 𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴))
235154adantrr 716 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → 𝑚 ∈ (1...(♯‘𝐴)))
236 isorel 7062 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴) ∧ (𝑚 ∈ (1...(♯‘𝐴)) ∧ (𝐺𝑘) ∈ (1...(♯‘𝐴)))) → (𝑚 < (𝐺𝑘) ↔ (𝐺𝑚) < (𝐺‘(𝐺𝑘))))
237234, 235, 227, 236syl12anc 835 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → (𝑚 < (𝐺𝑘) ↔ (𝐺𝑚) < (𝐺‘(𝐺𝑘))))
23833ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → 𝐺:(1...(♯‘𝐴))–1-1-onto𝐴)
239238, 226, 110syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → (𝐺‘(𝐺𝑘)) = 𝑘)
240239breq2d 5045 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → ((𝐺𝑚) < (𝐺‘(𝐺𝑘)) ↔ (𝐺𝑚) < 𝑘))
241173adantrr 716 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → (𝐺𝑚) ∈ ℤ)
24230ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → 𝐴 ⊆ (ℤ𝑀))
243242, 226sseldd 3919 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → 𝑘 ∈ (ℤ𝑀))
244 eluzelz 12245 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 ∈ (ℤ𝑀) → 𝑘 ∈ ℤ)
245243, 244syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → 𝑘 ∈ ℤ)
246 zltp1le 12024 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐺𝑚) ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((𝐺𝑚) < 𝑘 ↔ ((𝐺𝑚) + 1) ≤ 𝑘))
247241, 245, 246syl2anc 587 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → ((𝐺𝑚) < 𝑘 ↔ ((𝐺𝑚) + 1) ≤ 𝑘))
248237, 240, 2473bitrd 308 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → (𝑚 < (𝐺𝑘) ↔ ((𝐺𝑚) + 1) ≤ 𝑘))
249168adantrr 716 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → (𝑚 + 1) ∈ (1...(♯‘𝐴)))
250 isorel 7062 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴) ∧ ((𝐺𝑘) ∈ (1...(♯‘𝐴)) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴)))) → ((𝐺𝑘) < (𝑚 + 1) ↔ (𝐺‘(𝐺𝑘)) < (𝐺‘(𝑚 + 1))))
251234, 227, 249, 250syl12anc 835 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → ((𝐺𝑘) < (𝑚 + 1) ↔ (𝐺‘(𝐺𝑘)) < (𝐺‘(𝑚 + 1))))
252239breq1d 5043 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → ((𝐺‘(𝐺𝑘)) < (𝐺‘(𝑚 + 1)) ↔ 𝑘 < (𝐺‘(𝑚 + 1))))
253177adantrr 716 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → (𝐺‘(𝑚 + 1)) ∈ ℤ)
254 zltlem1 12027 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑘 ∈ ℤ ∧ (𝐺‘(𝑚 + 1)) ∈ ℤ) → (𝑘 < (𝐺‘(𝑚 + 1)) ↔ 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1)))
255245, 253, 254syl2anc 587 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → (𝑘 < (𝐺‘(𝑚 + 1)) ↔ 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1)))
256251, 252, 2553bitrd 308 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → ((𝐺𝑘) < (𝑚 + 1) ↔ 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1)))
257248, 256anbi12d 633 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → ((𝑚 < (𝐺𝑘) ∧ (𝐺𝑘) < (𝑚 + 1)) ↔ (((𝐺𝑚) + 1) ≤ 𝑘𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1))))
258233, 257mtbid 327 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → ¬ (((𝐺𝑚) + 1) ≤ 𝑘𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1)))
259258expr 460 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝑘𝐴 → ¬ (((𝐺𝑚) + 1) ≤ 𝑘𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1))))
260259con2d 136 . . . . . . . . . . . . . . . . 17 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((((𝐺𝑚) + 1) ≤ 𝑘𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1)) → ¬ 𝑘𝐴))
261 elfzle1 12909 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ (((𝐺𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1)) → ((𝐺𝑚) + 1) ≤ 𝑘)
262 elfzle2 12910 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ (((𝐺𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1)) → 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1))
263261, 262jca 515 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ (((𝐺𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1)) → (((𝐺𝑚) + 1) ≤ 𝑘𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1)))
264260, 263impel 509 . . . . . . . . . . . . . . . 16 ((((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (((𝐺𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1))) → ¬ 𝑘𝐴)
265223, 264eldifd 3895 . . . . . . . . . . . . . . 15 ((((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (((𝐺𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1))) → 𝑘 ∈ ((𝑀...(𝐺‘(♯‘𝐴))) ∖ 𝐴))
266213, 265, 120syl2anc 587 . . . . . . . . . . . . . 14 ((((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (((𝐺𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1))) → (𝐹𝑘) = 𝑍)
267159, 163, 185, 212, 266seqid2 13416 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (seq𝑀( + , 𝐹)‘(𝐺𝑚)) = (seq𝑀( + , 𝐹)‘((𝐺‘(𝑚 + 1)) − 1)))
268267oveq1d 7154 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((seq𝑀( + , 𝐹)‘(𝐺𝑚)) + (𝐹‘(𝐺‘(𝑚 + 1)))) = ((seq𝑀( + , 𝐹)‘((𝐺‘(𝑚 + 1)) − 1)) + (𝐹‘(𝐺‘(𝑚 + 1)))))
269 fveq2 6649 . . . . . . . . . . . . . . . . . 18 (𝑛 = (𝑚 + 1) → (𝐻𝑛) = (𝐻‘(𝑚 + 1)))
270 2fveq3 6654 . . . . . . . . . . . . . . . . . 18 (𝑛 = (𝑚 + 1) → (𝐹‘(𝐺𝑛)) = (𝐹‘(𝐺‘(𝑚 + 1))))
271269, 270eqeq12d 2817 . . . . . . . . . . . . . . . . 17 (𝑛 = (𝑚 + 1) → ((𝐻𝑛) = (𝐹‘(𝐺𝑛)) ↔ (𝐻‘(𝑚 + 1)) = (𝐹‘(𝐺‘(𝑚 + 1)))))
272271imbi2d 344 . . . . . . . . . . . . . . . 16 (𝑛 = (𝑚 + 1) → ((𝜑 → (𝐻𝑛) = (𝐹‘(𝐺𝑛))) ↔ (𝜑 → (𝐻‘(𝑚 + 1)) = (𝐹‘(𝐺‘(𝑚 + 1))))))
273272, 134vtoclga 3525 . . . . . . . . . . . . . . 15 ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (𝜑 → (𝐻‘(𝑚 + 1)) = (𝐹‘(𝐺‘(𝑚 + 1)))))
274273impcom 411 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐻‘(𝑚 + 1)) = (𝐹‘(𝐺‘(𝑚 + 1))))
275274adantlr 714 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐻‘(𝑚 + 1)) = (𝐹‘(𝐺‘(𝑚 + 1))))
276275oveq2d 7155 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((seq𝑀( + , 𝐹)‘(𝐺𝑚)) + (𝐻‘(𝑚 + 1))) = ((seq𝑀( + , 𝐹)‘(𝐺𝑚)) + (𝐹‘(𝐺‘(𝑚 + 1)))))
27789ad2antrr 725 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝑀 ∈ ℤ)
278177zcnd 12080 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(𝑚 + 1)) ∈ ℂ)
279 ax-1cn 10588 . . . . . . . . . . . . . . 15 1 ∈ ℂ
280 npcan 10888 . . . . . . . . . . . . . . 15 (((𝐺‘(𝑚 + 1)) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝐺‘(𝑚 + 1)) − 1) + 1) = (𝐺‘(𝑚 + 1)))
281278, 279, 280sylancl 589 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (((𝐺‘(𝑚 + 1)) − 1) + 1) = (𝐺‘(𝑚 + 1)))
282 uztrn 12253 . . . . . . . . . . . . . . . 16 ((((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ‘(𝐺𝑚)) ∧ (𝐺𝑚) ∈ (ℤ𝑀)) → ((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ𝑀))
283185, 163, 282syl2anc 587 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ𝑀))
284 eluzp1p1 12262 . . . . . . . . . . . . . . 15 (((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ𝑀) → (((𝐺‘(𝑚 + 1)) − 1) + 1) ∈ (ℤ‘(𝑀 + 1)))
285283, 284syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (((𝐺‘(𝑚 + 1)) − 1) + 1) ∈ (ℤ‘(𝑀 + 1)))
286281, 285eqeltrrd 2894 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(𝑚 + 1)) ∈ (ℤ‘(𝑀 + 1)))
287 seqm1 13387 . . . . . . . . . . . . 13 ((𝑀 ∈ ℤ ∧ (𝐺‘(𝑚 + 1)) ∈ (ℤ‘(𝑀 + 1))) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = ((seq𝑀( + , 𝐹)‘((𝐺‘(𝑚 + 1)) − 1)) + (𝐹‘(𝐺‘(𝑚 + 1)))))
288277, 286, 287syl2anc 587 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = ((seq𝑀( + , 𝐹)‘((𝐺‘(𝑚 + 1)) − 1)) + (𝐹‘(𝐺‘(𝑚 + 1)))))
289268, 276, 2883eqtr4rd 2847 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = ((seq𝑀( + , 𝐹)‘(𝐺𝑚)) + (𝐻‘(𝑚 + 1))))
290 seqp1 13383 . . . . . . . . . . . 12 (𝑚 ∈ (ℤ‘1) → (seq1( + , 𝐻)‘(𝑚 + 1)) = ((seq1( + , 𝐻)‘𝑚) + (𝐻‘(𝑚 + 1))))
291146, 290syl 17 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (seq1( + , 𝐻)‘(𝑚 + 1)) = ((seq1( + , 𝐻)‘𝑚) + (𝐻‘(𝑚 + 1))))
292289, 291eqeq12d 2817 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1)) ↔ ((seq𝑀( + , 𝐹)‘(𝐺𝑚)) + (𝐻‘(𝑚 + 1))) = ((seq1( + , 𝐻)‘𝑚) + (𝐻‘(𝑚 + 1)))))
293157, 292syl5ibr 249 . . . . . . . . 9 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((seq𝑀( + , 𝐹)‘(𝐺𝑚)) = (seq1( + , 𝐻)‘𝑚) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1))))
294293ex 416 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ) → ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → ((seq𝑀( + , 𝐹)‘(𝐺𝑚)) = (seq1( + , 𝐻)‘𝑚) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1)))))
295294a2d 29 . . . . . . 7 ((𝜑𝑚 ∈ ℕ) → (((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺𝑚)) = (seq1( + , 𝐻)‘𝑚)) → ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1)))))
296156, 295syld 47 . . . . . 6 ((𝜑𝑚 ∈ ℕ) → ((𝑚 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺𝑚)) = (seq1( + , 𝐻)‘𝑚)) → ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1)))))
297296expcom 417 . . . . 5 (𝑚 ∈ ℕ → (𝜑 → ((𝑚 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺𝑚)) = (seq1( + , 𝐻)‘𝑚)) → ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1))))))
298297a2d 29 . . . 4 (𝑚 ∈ ℕ → ((𝜑 → (𝑚 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺𝑚)) = (seq1( + , 𝐻)‘𝑚))) → (𝜑 → ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1))))))
2999, 15, 21, 27, 143, 298nnind 11647 . . 3 (𝑁 ∈ ℕ → (𝜑 → (𝑁 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺𝑁)) = (seq1( + , 𝐻)‘𝑁))))
3003, 299mpcom 38 . 2 (𝜑 → (𝑁 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺𝑁)) = (seq1( + , 𝐻)‘𝑁)))
3011, 300mpd 15 1 (𝜑 → (seq𝑀( + , 𝐹)‘(𝐺𝑁)) = (seq1( + , 𝐻)‘𝑁))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  w3a 1084   = wceq 1538  wcel 2112  cdif 3881  wss 3884   class class class wbr 5033  ccnv 5522  cres 5525  wf 6324  1-1-ontowf1o 6327  cfv 6328   Isom wiso 6329  (class class class)co 7139  cc 10528  cr 10529  1c1 10531   + caddc 10533  *cxr 10667   < clt 10668  cle 10669  cmin 10863  cn 11629  cz 11973  cuz 12235  ...cfz 12889  seqcseq 13368  chash 13690
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-cnex 10586  ax-resscn 10587  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-addrcl 10591  ax-mulcl 10592  ax-mulrcl 10593  ax-mulcom 10594  ax-addass 10595  ax-mulass 10596  ax-distr 10597  ax-i2m1 10598  ax-1ne0 10599  ax-1rid 10600  ax-rnegex 10601  ax-rrecex 10602  ax-cnre 10603  ax-pre-lttri 10604  ax-pre-lttrn 10605  ax-pre-ltadd 10606  ax-pre-mulgt0 10607
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-nel 3095  df-ral 3114  df-rex 3115  df-reu 3116  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-isom 6337  df-riota 7097  df-ov 7142  df-oprab 7143  df-mpo 7144  df-om 7565  df-1st 7675  df-2nd 7676  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-er 8276  df-en 8497  df-dom 8498  df-sdom 8499  df-pnf 10670  df-mnf 10671  df-xr 10672  df-ltxr 10673  df-le 10674  df-sub 10865  df-neg 10866  df-nn 11630  df-n0 11890  df-z 11974  df-uz 12236  df-fz 12890  df-seq 13369
This theorem is referenced by:  seqcoll2  13823  summolem2a  15067  prodmolem2a  15283
  Copyright terms: Public domain W3C validator