Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  seq3coll GIF version

Theorem seq3coll 10690
 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.) (Revised by Jim Kingdon, 9-Apr-2023.)
Hypotheses
Ref Expression
seqcoll.1 ((𝜑𝑘𝑆) → (𝑍 + 𝑘) = 𝑘)
seqcoll.1b ((𝜑𝑘𝑆) → (𝑘 + 𝑍) = 𝑘)
seqcoll.c ((𝜑 ∧ (𝑘𝑆𝑛𝑆)) → (𝑘 + 𝑛) ∈ 𝑆)
seqcoll.a (𝜑𝑍𝑆)
seqcoll.2 (𝜑𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴))
seqcoll.3 (𝜑𝑁 ∈ (1...(♯‘𝐴)))
seqcoll.4 (𝜑𝐴 ⊆ (ℤ𝑀))
seqcoll.5 ((𝜑𝑘 ∈ (ℤ𝑀)) → (𝐹𝑘) ∈ 𝑆)
seqcoll.hcl ((𝜑𝑘 ∈ (ℤ‘1)) → (𝐻𝑘) ∈ 𝑆)
seqcoll.6 ((𝜑𝑘 ∈ ((𝑀...(𝐺‘(♯‘𝐴))) ∖ 𝐴)) → (𝐹𝑘) = 𝑍)
seqcoll.7 ((𝜑𝑛 ∈ (1...(♯‘𝐴))) → (𝐻𝑛) = (𝐹‘(𝐺𝑛)))
Assertion
Ref Expression
seq3coll (𝜑 → (seq𝑀( + , 𝐹)‘(𝐺𝑁)) = (seq1( + , 𝐻)‘𝑁))
Distinct variable groups:   𝑘,𝑛,𝐴   𝑘,𝐹,𝑛   𝑘,𝐺,𝑛   𝑘,𝐻,𝑛   𝑘,𝑀,𝑛   + ,𝑘,𝑛   𝜑,𝑘,𝑛   𝑆,𝑘,𝑛   𝑘,𝑍,𝑛
Allowed substitution hints:   𝑁(𝑘,𝑛)

Proof of Theorem seq3coll
Dummy variables 𝑚 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 seqcoll.3 . 2 (𝜑𝑁 ∈ (1...(♯‘𝐴)))
2 elfznn 9934 . . . 4 (𝑁 ∈ (1...(♯‘𝐴)) → 𝑁 ∈ ℕ)
31, 2syl 14 . . 3 (𝜑𝑁 ∈ ℕ)
4 eleq1 2217 . . . . . 6 (𝑦 = 1 → (𝑦 ∈ (1...(♯‘𝐴)) ↔ 1 ∈ (1...(♯‘𝐴))))
5 2fveq3 5466 . . . . . . 7 (𝑦 = 1 → (seq𝑀( + , 𝐹)‘(𝐺𝑦)) = (seq𝑀( + , 𝐹)‘(𝐺‘1)))
6 fveq2 5461 . . . . . . 7 (𝑦 = 1 → (seq1( + , 𝐻)‘𝑦) = (seq1( + , 𝐻)‘1))
75, 6eqeq12d 2169 . . . . . 6 (𝑦 = 1 → ((seq𝑀( + , 𝐹)‘(𝐺𝑦)) = (seq1( + , 𝐻)‘𝑦) ↔ (seq𝑀( + , 𝐹)‘(𝐺‘1)) = (seq1( + , 𝐻)‘1)))
84, 7imbi12d 233 . . . . 5 (𝑦 = 1 → ((𝑦 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺𝑦)) = (seq1( + , 𝐻)‘𝑦)) ↔ (1 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘1)) = (seq1( + , 𝐻)‘1))))
98imbi2d 229 . . . 4 (𝑦 = 1 → ((𝜑 → (𝑦 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺𝑦)) = (seq1( + , 𝐻)‘𝑦))) ↔ (𝜑 → (1 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘1)) = (seq1( + , 𝐻)‘1)))))
10 eleq1 2217 . . . . . 6 (𝑦 = 𝑚 → (𝑦 ∈ (1...(♯‘𝐴)) ↔ 𝑚 ∈ (1...(♯‘𝐴))))
11 2fveq3 5466 . . . . . . 7 (𝑦 = 𝑚 → (seq𝑀( + , 𝐹)‘(𝐺𝑦)) = (seq𝑀( + , 𝐹)‘(𝐺𝑚)))
12 fveq2 5461 . . . . . . 7 (𝑦 = 𝑚 → (seq1( + , 𝐻)‘𝑦) = (seq1( + , 𝐻)‘𝑚))
1311, 12eqeq12d 2169 . . . . . 6 (𝑦 = 𝑚 → ((seq𝑀( + , 𝐹)‘(𝐺𝑦)) = (seq1( + , 𝐻)‘𝑦) ↔ (seq𝑀( + , 𝐹)‘(𝐺𝑚)) = (seq1( + , 𝐻)‘𝑚)))
1410, 13imbi12d 233 . . . . 5 (𝑦 = 𝑚 → ((𝑦 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺𝑦)) = (seq1( + , 𝐻)‘𝑦)) ↔ (𝑚 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺𝑚)) = (seq1( + , 𝐻)‘𝑚))))
1514imbi2d 229 . . . 4 (𝑦 = 𝑚 → ((𝜑 → (𝑦 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺𝑦)) = (seq1( + , 𝐻)‘𝑦))) ↔ (𝜑 → (𝑚 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺𝑚)) = (seq1( + , 𝐻)‘𝑚)))))
16 eleq1 2217 . . . . . 6 (𝑦 = (𝑚 + 1) → (𝑦 ∈ (1...(♯‘𝐴)) ↔ (𝑚 + 1) ∈ (1...(♯‘𝐴))))
17 2fveq3 5466 . . . . . . 7 (𝑦 = (𝑚 + 1) → (seq𝑀( + , 𝐹)‘(𝐺𝑦)) = (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))))
18 fveq2 5461 . . . . . . 7 (𝑦 = (𝑚 + 1) → (seq1( + , 𝐻)‘𝑦) = (seq1( + , 𝐻)‘(𝑚 + 1)))
1917, 18eqeq12d 2169 . . . . . 6 (𝑦 = (𝑚 + 1) → ((seq𝑀( + , 𝐹)‘(𝐺𝑦)) = (seq1( + , 𝐻)‘𝑦) ↔ (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1))))
2016, 19imbi12d 233 . . . . 5 (𝑦 = (𝑚 + 1) → ((𝑦 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺𝑦)) = (seq1( + , 𝐻)‘𝑦)) ↔ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1)))))
2120imbi2d 229 . . . 4 (𝑦 = (𝑚 + 1) → ((𝜑 → (𝑦 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺𝑦)) = (seq1( + , 𝐻)‘𝑦))) ↔ (𝜑 → ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1))))))
22 eleq1 2217 . . . . . 6 (𝑦 = 𝑁 → (𝑦 ∈ (1...(♯‘𝐴)) ↔ 𝑁 ∈ (1...(♯‘𝐴))))
23 2fveq3 5466 . . . . . . 7 (𝑦 = 𝑁 → (seq𝑀( + , 𝐹)‘(𝐺𝑦)) = (seq𝑀( + , 𝐹)‘(𝐺𝑁)))
24 fveq2 5461 . . . . . . 7 (𝑦 = 𝑁 → (seq1( + , 𝐻)‘𝑦) = (seq1( + , 𝐻)‘𝑁))
2523, 24eqeq12d 2169 . . . . . 6 (𝑦 = 𝑁 → ((seq𝑀( + , 𝐹)‘(𝐺𝑦)) = (seq1( + , 𝐻)‘𝑦) ↔ (seq𝑀( + , 𝐹)‘(𝐺𝑁)) = (seq1( + , 𝐻)‘𝑁)))
2622, 25imbi12d 233 . . . . 5 (𝑦 = 𝑁 → ((𝑦 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺𝑦)) = (seq1( + , 𝐻)‘𝑦)) ↔ (𝑁 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺𝑁)) = (seq1( + , 𝐻)‘𝑁))))
2726imbi2d 229 . . . 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 5748 . . . . . . . . . . . . 13 (𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴) → 𝐺:(1...(♯‘𝐴))–1-1-onto𝐴)
3331, 32syl 14 . . . . . . . . . . . 12 (𝜑𝐺:(1...(♯‘𝐴))–1-1-onto𝐴)
34 f1of 5407 . . . . . . . . . . . 12 (𝐺:(1...(♯‘𝐴))–1-1-onto𝐴𝐺:(1...(♯‘𝐴))⟶𝐴)
3533, 34syl 14 . . . . . . . . . . 11 (𝜑𝐺:(1...(♯‘𝐴))⟶𝐴)
36 elfzuz2 9909 . . . . . . . . . . . . 13 (𝑁 ∈ (1...(♯‘𝐴)) → (♯‘𝐴) ∈ (ℤ‘1))
371, 36syl 14 . . . . . . . . . . . 12 (𝜑 → (♯‘𝐴) ∈ (ℤ‘1))
38 eluzfz1 9911 . . . . . . . . . . . 12 ((♯‘𝐴) ∈ (ℤ‘1) → 1 ∈ (1...(♯‘𝐴)))
3937, 38syl 14 . . . . . . . . . . 11 (𝜑 → 1 ∈ (1...(♯‘𝐴)))
4035, 39ffvelrnd 5596 . . . . . . . . . 10 (𝜑 → (𝐺‘1) ∈ 𝐴)
4130, 40sseldd 3125 . . . . . . . . 9 (𝜑 → (𝐺‘1) ∈ (ℤ𝑀))
42 eluzle 9430 . . . . . . . . . . . . 13 ((♯‘𝐴) ∈ (ℤ‘1) → 1 ≤ (♯‘𝐴))
4337, 42syl 14 . . . . . . . . . . . 12 (𝜑 → 1 ≤ (♯‘𝐴))
44 elfzelz 9906 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ (1...(♯‘𝐴)) → 𝑘 ∈ ℤ)
4544ssriv 3128 . . . . . . . . . . . . . . . 16 (1...(♯‘𝐴)) ⊆ ℤ
46 zssre 9153 . . . . . . . . . . . . . . . 16 ℤ ⊆ ℝ
4745, 46sstri 3133 . . . . . . . . . . . . . . 15 (1...(♯‘𝐴)) ⊆ ℝ
4847a1i 9 . . . . . . . . . . . . . 14 (𝜑 → (1...(♯‘𝐴)) ⊆ ℝ)
49 ressxr 7900 . . . . . . . . . . . . . 14 ℝ ⊆ ℝ*
5048, 49sstrdi 3136 . . . . . . . . . . . . 13 (𝜑 → (1...(♯‘𝐴)) ⊆ ℝ*)
51 eluzelre 9428 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (ℤ𝑀) → 𝑘 ∈ ℝ)
5251ssriv 3128 . . . . . . . . . . . . . . 15 (ℤ𝑀) ⊆ ℝ
5330, 52sstrdi 3136 . . . . . . . . . . . . . 14 (𝜑𝐴 ⊆ ℝ)
5453, 49sstrdi 3136 . . . . . . . . . . . . 13 (𝜑𝐴 ⊆ ℝ*)
55 eluzfz2 9912 . . . . . . . . . . . . . 14 ((♯‘𝐴) ∈ (ℤ‘1) → (♯‘𝐴) ∈ (1...(♯‘𝐴)))
5637, 55syl 14 . . . . . . . . . . . . 13 (𝜑 → (♯‘𝐴) ∈ (1...(♯‘𝐴)))
57 leisorel 10685 . . . . . . . . . . . . 13 ((𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴) ∧ ((1...(♯‘𝐴)) ⊆ ℝ*𝐴 ⊆ ℝ*) ∧ (1 ∈ (1...(♯‘𝐴)) ∧ (♯‘𝐴) ∈ (1...(♯‘𝐴)))) → (1 ≤ (♯‘𝐴) ↔ (𝐺‘1) ≤ (𝐺‘(♯‘𝐴))))
5831, 50, 54, 39, 56, 57syl122anc 1226 . . . . . . . . . . . 12 (𝜑 → (1 ≤ (♯‘𝐴) ↔ (𝐺‘1) ≤ (𝐺‘(♯‘𝐴))))
5943, 58mpbid 146 . . . . . . . . . . 11 (𝜑 → (𝐺‘1) ≤ (𝐺‘(♯‘𝐴)))
6035, 56ffvelrnd 5596 . . . . . . . . . . . . . 14 (𝜑 → (𝐺‘(♯‘𝐴)) ∈ 𝐴)
6130, 60sseldd 3125 . . . . . . . . . . . . 13 (𝜑 → (𝐺‘(♯‘𝐴)) ∈ (ℤ𝑀))
62 eluzelz 9427 . . . . . . . . . . . . 13 ((𝐺‘(♯‘𝐴)) ∈ (ℤ𝑀) → (𝐺‘(♯‘𝐴)) ∈ ℤ)
6361, 62syl 14 . . . . . . . . . . . 12 (𝜑 → (𝐺‘(♯‘𝐴)) ∈ ℤ)
64 elfz5 9898 . . . . . . . . . . . 12 (((𝐺‘1) ∈ (ℤ𝑀) ∧ (𝐺‘(♯‘𝐴)) ∈ ℤ) → ((𝐺‘1) ∈ (𝑀...(𝐺‘(♯‘𝐴))) ↔ (𝐺‘1) ≤ (𝐺‘(♯‘𝐴))))
6541, 63, 64syl2anc 409 . . . . . . . . . . 11 (𝜑 → ((𝐺‘1) ∈ (𝑀...(𝐺‘(♯‘𝐴))) ↔ (𝐺‘1) ≤ (𝐺‘(♯‘𝐴))))
6659, 65mpbird 166 . . . . . . . . . 10 (𝜑 → (𝐺‘1) ∈ (𝑀...(𝐺‘(♯‘𝐴))))
67 fveq2 5461 . . . . . . . . . . . . 13 (𝑘 = (𝐺‘1) → (𝐹𝑘) = (𝐹‘(𝐺‘1)))
6867eleq1d 2223 . . . . . . . . . . . 12 (𝑘 = (𝐺‘1) → ((𝐹𝑘) ∈ 𝑆 ↔ (𝐹‘(𝐺‘1)) ∈ 𝑆))
6968imbi2d 229 . . . . . . . . . . 11 (𝑘 = (𝐺‘1) → ((𝜑 → (𝐹𝑘) ∈ 𝑆) ↔ (𝜑 → (𝐹‘(𝐺‘1)) ∈ 𝑆)))
70 elfzuz 9902 . . . . . . . . . . . 12 (𝑘 ∈ (𝑀...(𝐺‘(♯‘𝐴))) → 𝑘 ∈ (ℤ𝑀))
71 seqcoll.5 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (ℤ𝑀)) → (𝐹𝑘) ∈ 𝑆)
7271expcom 115 . . . . . . . . . . . 12 (𝑘 ∈ (ℤ𝑀) → (𝜑 → (𝐹𝑘) ∈ 𝑆))
7370, 72syl 14 . . . . . . . . . . 11 (𝑘 ∈ (𝑀...(𝐺‘(♯‘𝐴))) → (𝜑 → (𝐹𝑘) ∈ 𝑆))
7469, 73vtoclga 2775 . . . . . . . . . 10 ((𝐺‘1) ∈ (𝑀...(𝐺‘(♯‘𝐴))) → (𝜑 → (𝐹‘(𝐺‘1)) ∈ 𝑆))
7566, 74mpcom 36 . . . . . . . . 9 (𝜑 → (𝐹‘(𝐺‘1)) ∈ 𝑆)
76 eluzelz 9427 . . . . . . . . . . . . . . . . . 18 ((𝐺‘1) ∈ (ℤ𝑀) → (𝐺‘1) ∈ ℤ)
7741, 76syl 14 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐺‘1) ∈ ℤ)
78 peano2zm 9184 . . . . . . . . . . . . . . . . 17 ((𝐺‘1) ∈ ℤ → ((𝐺‘1) − 1) ∈ ℤ)
7977, 78syl 14 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐺‘1) − 1) ∈ ℤ)
8079zred 9265 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐺‘1) − 1) ∈ ℝ)
8177zred 9265 . . . . . . . . . . . . . . 15 (𝜑 → (𝐺‘1) ∈ ℝ)
8263zred 9265 . . . . . . . . . . . . . . 15 (𝜑 → (𝐺‘(♯‘𝐴)) ∈ ℝ)
8381lem1d 8783 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐺‘1) − 1) ≤ (𝐺‘1))
8480, 81, 82, 83, 59letrd 7978 . . . . . . . . . . . . . 14 (𝜑 → ((𝐺‘1) − 1) ≤ (𝐺‘(♯‘𝐴)))
85 eluz 9431 . . . . . . . . . . . . . . 15 ((((𝐺‘1) − 1) ∈ ℤ ∧ (𝐺‘(♯‘𝐴)) ∈ ℤ) → ((𝐺‘(♯‘𝐴)) ∈ (ℤ‘((𝐺‘1) − 1)) ↔ ((𝐺‘1) − 1) ≤ (𝐺‘(♯‘𝐴))))
8679, 63, 85syl2anc 409 . . . . . . . . . . . . . 14 (𝜑 → ((𝐺‘(♯‘𝐴)) ∈ (ℤ‘((𝐺‘1) − 1)) ↔ ((𝐺‘1) − 1) ≤ (𝐺‘(♯‘𝐴))))
8784, 86mpbird 166 . . . . . . . . . . . . 13 (𝜑 → (𝐺‘(♯‘𝐴)) ∈ (ℤ‘((𝐺‘1) − 1)))
88 fzss2 9944 . . . . . . . . . . . . 13 ((𝐺‘(♯‘𝐴)) ∈ (ℤ‘((𝐺‘1) − 1)) → (𝑀...((𝐺‘1) − 1)) ⊆ (𝑀...(𝐺‘(♯‘𝐴))))
8987, 88syl 14 . . . . . . . . . . . 12 (𝜑 → (𝑀...((𝐺‘1) − 1)) ⊆ (𝑀...(𝐺‘(♯‘𝐴))))
9089sselda 3124 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (𝑀...((𝐺‘1) − 1))) → 𝑘 ∈ (𝑀...(𝐺‘(♯‘𝐴))))
91 eluzel2 9423 . . . . . . . . . . . . . . 15 ((𝐺‘1) ∈ (ℤ𝑀) → 𝑀 ∈ ℤ)
9241, 91syl 14 . . . . . . . . . . . . . 14 (𝜑𝑀 ∈ ℤ)
93 elfzm11 9971 . . . . . . . . . . . . . 14 ((𝑀 ∈ ℤ ∧ (𝐺‘1) ∈ ℤ) → (𝑘 ∈ (𝑀...((𝐺‘1) − 1)) ↔ (𝑘 ∈ ℤ ∧ 𝑀𝑘𝑘 < (𝐺‘1))))
9492, 77, 93syl2anc 409 . . . . . . . . . . . . 13 (𝜑 → (𝑘 ∈ (𝑀...((𝐺‘1) − 1)) ↔ (𝑘 ∈ ℤ ∧ 𝑀𝑘𝑘 < (𝐺‘1))))
95 simp3 984 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℤ ∧ 𝑀𝑘𝑘 < (𝐺‘1)) → 𝑘 < (𝐺‘1))
9681adantr 274 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝐴) → (𝐺‘1) ∈ ℝ)
9753sselda 3124 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝐴) → 𝑘 ∈ ℝ)
98 f1ocnv 5420 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐺:(1...(♯‘𝐴))–1-1-onto𝐴𝐺:𝐴1-1-onto→(1...(♯‘𝐴)))
9933, 98syl 14 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐺:𝐴1-1-onto→(1...(♯‘𝐴)))
100 f1of 5407 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐺:𝐴1-1-onto→(1...(♯‘𝐴)) → 𝐺:𝐴⟶(1...(♯‘𝐴)))
10199, 100syl 14 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐺:𝐴⟶(1...(♯‘𝐴)))
102101ffvelrnda 5595 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘𝐴) → (𝐺𝑘) ∈ (1...(♯‘𝐴)))
103 elfznn 9934 . . . . . . . . . . . . . . . . . . . . 21 ((𝐺𝑘) ∈ (1...(♯‘𝐴)) → (𝐺𝑘) ∈ ℕ)
104102, 103syl 14 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘𝐴) → (𝐺𝑘) ∈ ℕ)
105104nnge1d 8855 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘𝐴) → 1 ≤ (𝐺𝑘))
10631adantr 274 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘𝐴) → 𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴))
10750adantr 274 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘𝐴) → (1...(♯‘𝐴)) ⊆ ℝ*)
10854adantr 274 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘𝐴) → 𝐴 ⊆ ℝ*)
10939adantr 274 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘𝐴) → 1 ∈ (1...(♯‘𝐴)))
110 leisorel 10685 . . . . . . . . . . . . . . . . . . . 20 ((𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴) ∧ ((1...(♯‘𝐴)) ⊆ ℝ*𝐴 ⊆ ℝ*) ∧ (1 ∈ (1...(♯‘𝐴)) ∧ (𝐺𝑘) ∈ (1...(♯‘𝐴)))) → (1 ≤ (𝐺𝑘) ↔ (𝐺‘1) ≤ (𝐺‘(𝐺𝑘))))
111106, 107, 108, 109, 102, 110syl122anc 1226 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘𝐴) → (1 ≤ (𝐺𝑘) ↔ (𝐺‘1) ≤ (𝐺‘(𝐺𝑘))))
112105, 111mpbid 146 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘𝐴) → (𝐺‘1) ≤ (𝐺‘(𝐺𝑘)))
113 f1ocnvfv2 5719 . . . . . . . . . . . . . . . . . . 19 ((𝐺:(1...(♯‘𝐴))–1-1-onto𝐴𝑘𝐴) → (𝐺‘(𝐺𝑘)) = 𝑘)
11433, 113sylan 281 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘𝐴) → (𝐺‘(𝐺𝑘)) = 𝑘)
115112, 114breqtrd 3986 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝐴) → (𝐺‘1) ≤ 𝑘)
11696, 97, 115lensymd 7976 . . . . . . . . . . . . . . . 16 ((𝜑𝑘𝐴) → ¬ 𝑘 < (𝐺‘1))
117116ex 114 . . . . . . . . . . . . . . 15 (𝜑 → (𝑘𝐴 → ¬ 𝑘 < (𝐺‘1)))
118117con2d 614 . . . . . . . . . . . . . 14 (𝜑 → (𝑘 < (𝐺‘1) → ¬ 𝑘𝐴))
11995, 118syl5 32 . . . . . . . . . . . . 13 (𝜑 → ((𝑘 ∈ ℤ ∧ 𝑀𝑘𝑘 < (𝐺‘1)) → ¬ 𝑘𝐴))
12094, 119sylbid 149 . . . . . . . . . . . 12 (𝜑 → (𝑘 ∈ (𝑀...((𝐺‘1) − 1)) → ¬ 𝑘𝐴))
121120imp 123 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (𝑀...((𝐺‘1) − 1))) → ¬ 𝑘𝐴)
12290, 121eldifd 3108 . . . . . . . . . 10 ((𝜑𝑘 ∈ (𝑀...((𝐺‘1) − 1))) → 𝑘 ∈ ((𝑀...(𝐺‘(♯‘𝐴))) ∖ 𝐴))
123 seqcoll.6 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝑀...(𝐺‘(♯‘𝐴))) ∖ 𝐴)) → (𝐹𝑘) = 𝑍)
124122, 123syldan 280 . . . . . . . . 9 ((𝜑𝑘 ∈ (𝑀...((𝐺‘1) − 1))) → (𝐹𝑘) = 𝑍)
125 seqcoll.c . . . . . . . . 9 ((𝜑 ∧ (𝑘𝑆𝑛𝑆)) → (𝑘 + 𝑛) ∈ 𝑆)
12628, 29, 41, 75, 124, 71, 125seq3id 10385 . . . . . . . 8 (𝜑 → (seq𝑀( + , 𝐹) ↾ (ℤ‘(𝐺‘1))) = seq(𝐺‘1)( + , 𝐹))
127126fveq1d 5463 . . . . . . 7 (𝜑 → ((seq𝑀( + , 𝐹) ↾ (ℤ‘(𝐺‘1)))‘(𝐺‘1)) = (seq(𝐺‘1)( + , 𝐹)‘(𝐺‘1)))
128 uzid 9432 . . . . . . . . 9 ((𝐺‘1) ∈ ℤ → (𝐺‘1) ∈ (ℤ‘(𝐺‘1)))
12977, 128syl 14 . . . . . . . 8 (𝜑 → (𝐺‘1) ∈ (ℤ‘(𝐺‘1)))
130 fvres 5485 . . . . . . . 8 ((𝐺‘1) ∈ (ℤ‘(𝐺‘1)) → ((seq𝑀( + , 𝐹) ↾ (ℤ‘(𝐺‘1)))‘(𝐺‘1)) = (seq𝑀( + , 𝐹)‘(𝐺‘1)))
131129, 130syl 14 . . . . . . 7 (𝜑 → ((seq𝑀( + , 𝐹) ↾ (ℤ‘(𝐺‘1)))‘(𝐺‘1)) = (seq𝑀( + , 𝐹)‘(𝐺‘1)))
13292adantr 274 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (ℤ‘(𝐺‘1))) → 𝑀 ∈ ℤ)
133 eluzelz 9427 . . . . . . . . . . . 12 (𝑘 ∈ (ℤ‘(𝐺‘1)) → 𝑘 ∈ ℤ)
134133adantl 275 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (ℤ‘(𝐺‘1))) → 𝑘 ∈ ℤ)
135132zred 9265 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (ℤ‘(𝐺‘1))) → 𝑀 ∈ ℝ)
13681adantr 274 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (ℤ‘(𝐺‘1))) → (𝐺‘1) ∈ ℝ)
137134zred 9265 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (ℤ‘(𝐺‘1))) → 𝑘 ∈ ℝ)
138 eluzle 9430 . . . . . . . . . . . . . 14 ((𝐺‘1) ∈ (ℤ𝑀) → 𝑀 ≤ (𝐺‘1))
13941, 138syl 14 . . . . . . . . . . . . 13 (𝜑𝑀 ≤ (𝐺‘1))
140139adantr 274 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (ℤ‘(𝐺‘1))) → 𝑀 ≤ (𝐺‘1))
141 eluzle 9430 . . . . . . . . . . . . 13 (𝑘 ∈ (ℤ‘(𝐺‘1)) → (𝐺‘1) ≤ 𝑘)
142141adantl 275 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (ℤ‘(𝐺‘1))) → (𝐺‘1) ≤ 𝑘)
143135, 136, 137, 140, 142letrd 7978 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (ℤ‘(𝐺‘1))) → 𝑀𝑘)
144 eluz2 9424 . . . . . . . . . . 11 (𝑘 ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝑀𝑘))
145132, 134, 143, 144syl3anbrc 1166 . . . . . . . . . 10 ((𝜑𝑘 ∈ (ℤ‘(𝐺‘1))) → 𝑘 ∈ (ℤ𝑀))
146145, 71syldan 280 . . . . . . . . 9 ((𝜑𝑘 ∈ (ℤ‘(𝐺‘1))) → (𝐹𝑘) ∈ 𝑆)
14777, 146, 125seq3-1 10337 . . . . . . . 8 (𝜑 → (seq(𝐺‘1)( + , 𝐹)‘(𝐺‘1)) = (𝐹‘(𝐺‘1)))
148 fveq2 5461 . . . . . . . . . . . 12 (𝑛 = 1 → (𝐻𝑛) = (𝐻‘1))
149 2fveq3 5466 . . . . . . . . . . . 12 (𝑛 = 1 → (𝐹‘(𝐺𝑛)) = (𝐹‘(𝐺‘1)))
150148, 149eqeq12d 2169 . . . . . . . . . . 11 (𝑛 = 1 → ((𝐻𝑛) = (𝐹‘(𝐺𝑛)) ↔ (𝐻‘1) = (𝐹‘(𝐺‘1))))
151150imbi2d 229 . . . . . . . . . 10 (𝑛 = 1 → ((𝜑 → (𝐻𝑛) = (𝐹‘(𝐺𝑛))) ↔ (𝜑 → (𝐻‘1) = (𝐹‘(𝐺‘1)))))
152 seqcoll.7 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...(♯‘𝐴))) → (𝐻𝑛) = (𝐹‘(𝐺𝑛)))
153152expcom 115 . . . . . . . . . 10 (𝑛 ∈ (1...(♯‘𝐴)) → (𝜑 → (𝐻𝑛) = (𝐹‘(𝐺𝑛))))
154151, 153vtoclga 2775 . . . . . . . . 9 (1 ∈ (1...(♯‘𝐴)) → (𝜑 → (𝐻‘1) = (𝐹‘(𝐺‘1))))
15539, 154mpcom 36 . . . . . . . 8 (𝜑 → (𝐻‘1) = (𝐹‘(𝐺‘1)))
156147, 155eqtr4d 2190 . . . . . . 7 (𝜑 → (seq(𝐺‘1)( + , 𝐹)‘(𝐺‘1)) = (𝐻‘1))
157127, 131, 1563eqtr3d 2195 . . . . . 6 (𝜑 → (seq𝑀( + , 𝐹)‘(𝐺‘1)) = (𝐻‘1))
158 1zzd 9173 . . . . . . 7 (𝜑 → 1 ∈ ℤ)
159 seqcoll.hcl . . . . . . 7 ((𝜑𝑘 ∈ (ℤ‘1)) → (𝐻𝑘) ∈ 𝑆)
160158, 159, 125seq3-1 10337 . . . . . 6 (𝜑 → (seq1( + , 𝐻)‘1) = (𝐻‘1))
161157, 160eqtr4d 2190 . . . . 5 (𝜑 → (seq𝑀( + , 𝐹)‘(𝐺‘1)) = (seq1( + , 𝐻)‘1))
162161a1d 22 . . . 4 (𝜑 → (1 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘1)) = (seq1( + , 𝐻)‘1)))
163 simplr 520 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝑚 ∈ ℕ)
164 nnuz 9453 . . . . . . . . . . 11 ℕ = (ℤ‘1)
165163, 164eleqtrdi 2247 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝑚 ∈ (ℤ‘1))
166 nnz 9165 . . . . . . . . . . . 12 (𝑚 ∈ ℕ → 𝑚 ∈ ℤ)
167166ad2antlr 481 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝑚 ∈ ℤ)
168 elfzuz3 9903 . . . . . . . . . . . 12 ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (♯‘𝐴) ∈ (ℤ‘(𝑚 + 1)))
169168adantl 275 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (♯‘𝐴) ∈ (ℤ‘(𝑚 + 1)))
170 peano2uzr 9475 . . . . . . . . . . 11 ((𝑚 ∈ ℤ ∧ (♯‘𝐴) ∈ (ℤ‘(𝑚 + 1))) → (♯‘𝐴) ∈ (ℤ𝑚))
171167, 169, 170syl2anc 409 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (♯‘𝐴) ∈ (ℤ𝑚))
172 elfzuzb 9900 . . . . . . . . . 10 (𝑚 ∈ (1...(♯‘𝐴)) ↔ (𝑚 ∈ (ℤ‘1) ∧ (♯‘𝐴) ∈ (ℤ𝑚)))
173165, 171, 172sylanbrc 414 . . . . . . . . 9 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝑚 ∈ (1...(♯‘𝐴)))
174173ex 114 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ) → ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → 𝑚 ∈ (1...(♯‘𝐴))))
175174imim1d 75 . . . . . . 7 ((𝜑𝑚 ∈ ℕ) → ((𝑚 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺𝑚)) = (seq1( + , 𝐻)‘𝑚)) → ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺𝑚)) = (seq1( + , 𝐻)‘𝑚))))
176 oveq1 5821 . . . . . . . . . 10 ((seq𝑀( + , 𝐹)‘(𝐺𝑚)) = (seq1( + , 𝐻)‘𝑚) → ((seq𝑀( + , 𝐹)‘(𝐺𝑚)) + (𝐻‘(𝑚 + 1))) = ((seq1( + , 𝐻)‘𝑚) + (𝐻‘(𝑚 + 1))))
177 simpll 519 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝜑)
178 seqcoll.1b . . . . . . . . . . . . . . 15 ((𝜑𝑘𝑆) → (𝑘 + 𝑍) = 𝑘)
179177, 178sylan 281 . . . . . . . . . . . . . 14 ((((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘𝑆) → (𝑘 + 𝑍) = 𝑘)
18030ad2antrr 480 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝐴 ⊆ (ℤ𝑀))
18135ad2antrr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝐺:(1...(♯‘𝐴))⟶𝐴)
182181, 173ffvelrnd 5596 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺𝑚) ∈ 𝐴)
183180, 182sseldd 3125 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺𝑚) ∈ (ℤ𝑀))
184 nnre 8819 . . . . . . . . . . . . . . . . . . 19 (𝑚 ∈ ℕ → 𝑚 ∈ ℝ)
185184ad2antlr 481 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝑚 ∈ ℝ)
186185ltp1d 8780 . . . . . . . . . . . . . . . . 17 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝑚 < (𝑚 + 1))
18731ad2antrr 480 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴))
188 simpr 109 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝑚 + 1) ∈ (1...(♯‘𝐴)))
189 isorel 5749 . . . . . . . . . . . . . . . . . 18 ((𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴) ∧ (𝑚 ∈ (1...(♯‘𝐴)) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴)))) → (𝑚 < (𝑚 + 1) ↔ (𝐺𝑚) < (𝐺‘(𝑚 + 1))))
190187, 173, 188, 189syl12anc 1215 . . . . . . . . . . . . . . . . 17 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝑚 < (𝑚 + 1) ↔ (𝐺𝑚) < (𝐺‘(𝑚 + 1))))
191186, 190mpbid 146 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺𝑚) < (𝐺‘(𝑚 + 1)))
192 eluzelz 9427 . . . . . . . . . . . . . . . . . 18 ((𝐺𝑚) ∈ (ℤ𝑀) → (𝐺𝑚) ∈ ℤ)
193183, 192syl 14 . . . . . . . . . . . . . . . . 17 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺𝑚) ∈ ℤ)
194181, 188ffvelrnd 5596 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(𝑚 + 1)) ∈ 𝐴)
195180, 194sseldd 3125 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(𝑚 + 1)) ∈ (ℤ𝑀))
196 eluzelz 9427 . . . . . . . . . . . . . . . . . 18 ((𝐺‘(𝑚 + 1)) ∈ (ℤ𝑀) → (𝐺‘(𝑚 + 1)) ∈ ℤ)
197195, 196syl 14 . . . . . . . . . . . . . . . . 17 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(𝑚 + 1)) ∈ ℤ)
198 zltlem1 9203 . . . . . . . . . . . . . . . . 17 (((𝐺𝑚) ∈ ℤ ∧ (𝐺‘(𝑚 + 1)) ∈ ℤ) → ((𝐺𝑚) < (𝐺‘(𝑚 + 1)) ↔ (𝐺𝑚) ≤ ((𝐺‘(𝑚 + 1)) − 1)))
199193, 197, 198syl2anc 409 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝐺𝑚) < (𝐺‘(𝑚 + 1)) ↔ (𝐺𝑚) ≤ ((𝐺‘(𝑚 + 1)) − 1)))
200191, 199mpbid 146 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺𝑚) ≤ ((𝐺‘(𝑚 + 1)) − 1))
201 peano2zm 9184 . . . . . . . . . . . . . . . . 17 ((𝐺‘(𝑚 + 1)) ∈ ℤ → ((𝐺‘(𝑚 + 1)) − 1) ∈ ℤ)
202197, 201syl 14 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝐺‘(𝑚 + 1)) − 1) ∈ ℤ)
203 eluz 9431 . . . . . . . . . . . . . . . 16 (((𝐺𝑚) ∈ ℤ ∧ ((𝐺‘(𝑚 + 1)) − 1) ∈ ℤ) → (((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ‘(𝐺𝑚)) ↔ (𝐺𝑚) ≤ ((𝐺‘(𝑚 + 1)) − 1)))
204193, 202, 203syl2anc 409 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ‘(𝐺𝑚)) ↔ (𝐺𝑚) ≤ ((𝐺‘(𝑚 + 1)) − 1)))
205200, 204mpbird 166 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ‘(𝐺𝑚)))
206 eqid 2154 . . . . . . . . . . . . . . . 16 (ℤ𝑀) = (ℤ𝑀)
20792ad2antrr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝑀 ∈ ℤ)
208177, 71sylan 281 . . . . . . . . . . . . . . . 16 ((((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (ℤ𝑀)) → (𝐹𝑘) ∈ 𝑆)
209177, 125sylan 281 . . . . . . . . . . . . . . . 16 ((((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ (𝑘𝑆𝑛𝑆)) → (𝑘 + 𝑛) ∈ 𝑆)
210206, 207, 208, 209seqf 10338 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → seq𝑀( + , 𝐹):(ℤ𝑀)⟶𝑆)
211210, 183ffvelrnd 5596 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (seq𝑀( + , 𝐹)‘(𝐺𝑚)) ∈ 𝑆)
212 simplll 523 . . . . . . . . . . . . . . 15 ((((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (((𝐺𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1))) → 𝜑)
213 elfzuz 9902 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ (((𝐺𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1)) → 𝑘 ∈ (ℤ‘((𝐺𝑚) + 1)))
214 peano2uz 9473 . . . . . . . . . . . . . . . . . . 19 ((𝐺𝑚) ∈ (ℤ𝑀) → ((𝐺𝑚) + 1) ∈ (ℤ𝑀))
215183, 214syl 14 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝐺𝑚) + 1) ∈ (ℤ𝑀))
216 uztrn 9434 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ (ℤ‘((𝐺𝑚) + 1)) ∧ ((𝐺𝑚) + 1) ∈ (ℤ𝑀)) → 𝑘 ∈ (ℤ𝑀))
217213, 215, 216syl2anr 288 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (((𝐺𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1))) → 𝑘 ∈ (ℤ𝑀))
218202zred 9265 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝐺‘(𝑚 + 1)) − 1) ∈ ℝ)
219197zred 9265 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(𝑚 + 1)) ∈ ℝ)
22082ad2antrr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(♯‘𝐴)) ∈ ℝ)
221219lem1d 8783 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝐺‘(𝑚 + 1)) − 1) ≤ (𝐺‘(𝑚 + 1)))
222 elfzle2 9908 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (𝑚 + 1) ≤ (♯‘𝐴))
223222adantl 275 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝑚 + 1) ≤ (♯‘𝐴))
22450ad2antrr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (1...(♯‘𝐴)) ⊆ ℝ*)
22554ad2antrr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝐴 ⊆ ℝ*)
22656ad2antrr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (♯‘𝐴) ∈ (1...(♯‘𝐴)))
227 leisorel 10685 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴) ∧ ((1...(♯‘𝐴)) ⊆ ℝ*𝐴 ⊆ ℝ*) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ (♯‘𝐴) ∈ (1...(♯‘𝐴)))) → ((𝑚 + 1) ≤ (♯‘𝐴) ↔ (𝐺‘(𝑚 + 1)) ≤ (𝐺‘(♯‘𝐴))))
228187, 224, 225, 188, 226, 227syl122anc 1226 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝑚 + 1) ≤ (♯‘𝐴) ↔ (𝐺‘(𝑚 + 1)) ≤ (𝐺‘(♯‘𝐴))))
229223, 228mpbid 146 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(𝑚 + 1)) ≤ (𝐺‘(♯‘𝐴)))
230218, 219, 220, 221, 229letrd 7978 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝐺‘(𝑚 + 1)) − 1) ≤ (𝐺‘(♯‘𝐴)))
23163ad2antrr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(♯‘𝐴)) ∈ ℤ)
232 eluz 9431 . . . . . . . . . . . . . . . . . . . 20 ((((𝐺‘(𝑚 + 1)) − 1) ∈ ℤ ∧ (𝐺‘(♯‘𝐴)) ∈ ℤ) → ((𝐺‘(♯‘𝐴)) ∈ (ℤ‘((𝐺‘(𝑚 + 1)) − 1)) ↔ ((𝐺‘(𝑚 + 1)) − 1) ≤ (𝐺‘(♯‘𝐴))))
233202, 231, 232syl2anc 409 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝐺‘(♯‘𝐴)) ∈ (ℤ‘((𝐺‘(𝑚 + 1)) − 1)) ↔ ((𝐺‘(𝑚 + 1)) − 1) ≤ (𝐺‘(♯‘𝐴))))
234230, 233mpbird 166 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(♯‘𝐴)) ∈ (ℤ‘((𝐺‘(𝑚 + 1)) − 1)))
235 elfzuz3 9903 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ (((𝐺𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1)) → ((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ𝑘))
236 uztrn 9434 . . . . . . . . . . . . . . . . . 18 (((𝐺‘(♯‘𝐴)) ∈ (ℤ‘((𝐺‘(𝑚 + 1)) − 1)) ∧ ((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ𝑘)) → (𝐺‘(♯‘𝐴)) ∈ (ℤ𝑘))
237234, 235, 236syl2an 287 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (((𝐺𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1))) → (𝐺‘(♯‘𝐴)) ∈ (ℤ𝑘))
238 elfzuzb 9900 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ (𝑀...(𝐺‘(♯‘𝐴))) ↔ (𝑘 ∈ (ℤ𝑀) ∧ (𝐺‘(♯‘𝐴)) ∈ (ℤ𝑘)))
239217, 237, 238sylanbrc 414 . . . . . . . . . . . . . . . 16 ((((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (((𝐺𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1))) → 𝑘 ∈ (𝑀...(𝐺‘(♯‘𝐴))))
240166ad2antlr 481 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → 𝑚 ∈ ℤ)
241101ad2antrr 480 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → 𝐺:𝐴⟶(1...(♯‘𝐴)))
242 simprr 522 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → 𝑘𝐴)
243241, 242ffvelrnd 5596 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → (𝐺𝑘) ∈ (1...(♯‘𝐴)))
244 elfzelz 9906 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐺𝑘) ∈ (1...(♯‘𝐴)) → (𝐺𝑘) ∈ ℤ)
245243, 244syl 14 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → (𝐺𝑘) ∈ ℤ)
246 btwnnz 9237 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑚 ∈ ℤ ∧ 𝑚 < (𝐺𝑘) ∧ (𝐺𝑘) < (𝑚 + 1)) → ¬ (𝐺𝑘) ∈ ℤ)
2472463expib 1185 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 ∈ ℤ → ((𝑚 < (𝐺𝑘) ∧ (𝐺𝑘) < (𝑚 + 1)) → ¬ (𝐺𝑘) ∈ ℤ))
248247con2d 614 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 ∈ ℤ → ((𝐺𝑘) ∈ ℤ → ¬ (𝑚 < (𝐺𝑘) ∧ (𝐺𝑘) < (𝑚 + 1))))
249240, 245, 248sylc 62 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → ¬ (𝑚 < (𝐺𝑘) ∧ (𝐺𝑘) < (𝑚 + 1)))
25031ad2antrr 480 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → 𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴))
251173adantrr 471 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → 𝑚 ∈ (1...(♯‘𝐴)))
252 isorel 5749 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴) ∧ (𝑚 ∈ (1...(♯‘𝐴)) ∧ (𝐺𝑘) ∈ (1...(♯‘𝐴)))) → (𝑚 < (𝐺𝑘) ↔ (𝐺𝑚) < (𝐺‘(𝐺𝑘))))
253250, 251, 243, 252syl12anc 1215 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → (𝑚 < (𝐺𝑘) ↔ (𝐺𝑚) < (𝐺‘(𝐺𝑘))))
25433ad2antrr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → 𝐺:(1...(♯‘𝐴))–1-1-onto𝐴)
255254, 242, 113syl2anc 409 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → (𝐺‘(𝐺𝑘)) = 𝑘)
256255breq2d 3973 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → ((𝐺𝑚) < (𝐺‘(𝐺𝑘)) ↔ (𝐺𝑚) < 𝑘))
257193adantrr 471 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → (𝐺𝑚) ∈ ℤ)
25830ad2antrr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → 𝐴 ⊆ (ℤ𝑀))
259258, 242sseldd 3125 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → 𝑘 ∈ (ℤ𝑀))
260 eluzelz 9427 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 ∈ (ℤ𝑀) → 𝑘 ∈ ℤ)
261259, 260syl 14 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → 𝑘 ∈ ℤ)
262 zltp1le 9200 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐺𝑚) ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((𝐺𝑚) < 𝑘 ↔ ((𝐺𝑚) + 1) ≤ 𝑘))
263257, 261, 262syl2anc 409 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → ((𝐺𝑚) < 𝑘 ↔ ((𝐺𝑚) + 1) ≤ 𝑘))
264253, 256, 2633bitrd 213 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → (𝑚 < (𝐺𝑘) ↔ ((𝐺𝑚) + 1) ≤ 𝑘))
265188adantrr 471 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → (𝑚 + 1) ∈ (1...(♯‘𝐴)))
266 isorel 5749 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴) ∧ ((𝐺𝑘) ∈ (1...(♯‘𝐴)) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴)))) → ((𝐺𝑘) < (𝑚 + 1) ↔ (𝐺‘(𝐺𝑘)) < (𝐺‘(𝑚 + 1))))
267250, 243, 265, 266syl12anc 1215 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → ((𝐺𝑘) < (𝑚 + 1) ↔ (𝐺‘(𝐺𝑘)) < (𝐺‘(𝑚 + 1))))
268255breq1d 3971 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → ((𝐺‘(𝐺𝑘)) < (𝐺‘(𝑚 + 1)) ↔ 𝑘 < (𝐺‘(𝑚 + 1))))
269197adantrr 471 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → (𝐺‘(𝑚 + 1)) ∈ ℤ)
270 zltlem1 9203 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑘 ∈ ℤ ∧ (𝐺‘(𝑚 + 1)) ∈ ℤ) → (𝑘 < (𝐺‘(𝑚 + 1)) ↔ 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1)))
271261, 269, 270syl2anc 409 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → (𝑘 < (𝐺‘(𝑚 + 1)) ↔ 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1)))
272267, 268, 2713bitrd 213 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → ((𝐺𝑘) < (𝑚 + 1) ↔ 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1)))
273264, 272anbi12d 465 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → ((𝑚 < (𝐺𝑘) ∧ (𝐺𝑘) < (𝑚 + 1)) ↔ (((𝐺𝑚) + 1) ≤ 𝑘𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1))))
274249, 273mtbid 662 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘𝐴)) → ¬ (((𝐺𝑚) + 1) ≤ 𝑘𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1)))
275274expr 373 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝑘𝐴 → ¬ (((𝐺𝑚) + 1) ≤ 𝑘𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1))))
276275con2d 614 . . . . . . . . . . . . . . . . 17 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((((𝐺𝑚) + 1) ≤ 𝑘𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1)) → ¬ 𝑘𝐴))
277 elfzle1 9907 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ (((𝐺𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1)) → ((𝐺𝑚) + 1) ≤ 𝑘)
278 elfzle2 9908 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ (((𝐺𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1)) → 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1))
279277, 278jca 304 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ (((𝐺𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1)) → (((𝐺𝑚) + 1) ≤ 𝑘𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1)))
280276, 279impel 278 . . . . . . . . . . . . . . . 16 ((((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (((𝐺𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1))) → ¬ 𝑘𝐴)
281239, 280eldifd 3108 . . . . . . . . . . . . . . 15 ((((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (((𝐺𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1))) → 𝑘 ∈ ((𝑀...(𝐺‘(♯‘𝐴))) ∖ 𝐴))
282212, 281, 123syl2anc 409 . . . . . . . . . . . . . 14 ((((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (((𝐺𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1))) → (𝐹𝑘) = 𝑍)
283179, 183, 205, 211, 282, 208, 209seq3id2 10386 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (seq𝑀( + , 𝐹)‘(𝐺𝑚)) = (seq𝑀( + , 𝐹)‘((𝐺‘(𝑚 + 1)) − 1)))
284283oveq1d 5829 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((seq𝑀( + , 𝐹)‘(𝐺𝑚)) + (𝐹‘(𝐺‘(𝑚 + 1)))) = ((seq𝑀( + , 𝐹)‘((𝐺‘(𝑚 + 1)) − 1)) + (𝐹‘(𝐺‘(𝑚 + 1)))))
285 fveq2 5461 . . . . . . . . . . . . . . . . . 18 (𝑛 = (𝑚 + 1) → (𝐻𝑛) = (𝐻‘(𝑚 + 1)))
286 2fveq3 5466 . . . . . . . . . . . . . . . . . 18 (𝑛 = (𝑚 + 1) → (𝐹‘(𝐺𝑛)) = (𝐹‘(𝐺‘(𝑚 + 1))))
287285, 286eqeq12d 2169 . . . . . . . . . . . . . . . . 17 (𝑛 = (𝑚 + 1) → ((𝐻𝑛) = (𝐹‘(𝐺𝑛)) ↔ (𝐻‘(𝑚 + 1)) = (𝐹‘(𝐺‘(𝑚 + 1)))))
288287imbi2d 229 . . . . . . . . . . . . . . . 16 (𝑛 = (𝑚 + 1) → ((𝜑 → (𝐻𝑛) = (𝐹‘(𝐺𝑛))) ↔ (𝜑 → (𝐻‘(𝑚 + 1)) = (𝐹‘(𝐺‘(𝑚 + 1))))))
289288, 153vtoclga 2775 . . . . . . . . . . . . . . 15 ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (𝜑 → (𝐻‘(𝑚 + 1)) = (𝐹‘(𝐺‘(𝑚 + 1)))))
290289impcom 124 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐻‘(𝑚 + 1)) = (𝐹‘(𝐺‘(𝑚 + 1))))
291290adantlr 469 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐻‘(𝑚 + 1)) = (𝐹‘(𝐺‘(𝑚 + 1))))
292291oveq2d 5830 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((seq𝑀( + , 𝐹)‘(𝐺𝑚)) + (𝐻‘(𝑚 + 1))) = ((seq𝑀( + , 𝐹)‘(𝐺𝑚)) + (𝐹‘(𝐺‘(𝑚 + 1)))))
293197zcnd 9266 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(𝑚 + 1)) ∈ ℂ)
294 ax-1cn 7804 . . . . . . . . . . . . . . 15 1 ∈ ℂ
295 npcan 8063 . . . . . . . . . . . . . . 15 (((𝐺‘(𝑚 + 1)) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝐺‘(𝑚 + 1)) − 1) + 1) = (𝐺‘(𝑚 + 1)))
296293, 294, 295sylancl 410 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (((𝐺‘(𝑚 + 1)) − 1) + 1) = (𝐺‘(𝑚 + 1)))
297 uztrn 9434 . . . . . . . . . . . . . . . 16 ((((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ‘(𝐺𝑚)) ∧ (𝐺𝑚) ∈ (ℤ𝑀)) → ((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ𝑀))
298205, 183, 297syl2anc 409 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ𝑀))
299 eluzp1p1 9443 . . . . . . . . . . . . . . 15 (((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ𝑀) → (((𝐺‘(𝑚 + 1)) − 1) + 1) ∈ (ℤ‘(𝑀 + 1)))
300298, 299syl 14 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (((𝐺‘(𝑚 + 1)) − 1) + 1) ∈ (ℤ‘(𝑀 + 1)))
301296, 300eqeltrrd 2232 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(𝑚 + 1)) ∈ (ℤ‘(𝑀 + 1)))
302207, 301, 208, 209seq3m1 10345 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = ((seq𝑀( + , 𝐹)‘((𝐺‘(𝑚 + 1)) − 1)) + (𝐹‘(𝐺‘(𝑚 + 1)))))
303284, 292, 3023eqtr4rd 2198 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = ((seq𝑀( + , 𝐹)‘(𝐺𝑚)) + (𝐻‘(𝑚 + 1))))
304177, 159sylan 281 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (ℤ‘1)) → (𝐻𝑘) ∈ 𝑆)
305165, 304, 209seq3p1 10339 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (seq1( + , 𝐻)‘(𝑚 + 1)) = ((seq1( + , 𝐻)‘𝑚) + (𝐻‘(𝑚 + 1))))
306303, 305eqeq12d 2169 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1)) ↔ ((seq𝑀( + , 𝐹)‘(𝐺𝑚)) + (𝐻‘(𝑚 + 1))) = ((seq1( + , 𝐻)‘𝑚) + (𝐻‘(𝑚 + 1)))))
307176, 306syl5ibr 155 . . . . . . . . 9 (((𝜑𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((seq𝑀( + , 𝐹)‘(𝐺𝑚)) = (seq1( + , 𝐻)‘𝑚) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1))))
308307ex 114 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ) → ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → ((seq𝑀( + , 𝐹)‘(𝐺𝑚)) = (seq1( + , 𝐻)‘𝑚) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1)))))
309308a2d 26 . . . . . . 7 ((𝜑𝑚 ∈ ℕ) → (((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺𝑚)) = (seq1( + , 𝐻)‘𝑚)) → ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1)))))
310175, 309syld 45 . . . . . 6 ((𝜑𝑚 ∈ ℕ) → ((𝑚 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺𝑚)) = (seq1( + , 𝐻)‘𝑚)) → ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1)))))
311310expcom 115 . . . . 5 (𝑚 ∈ ℕ → (𝜑 → ((𝑚 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺𝑚)) = (seq1( + , 𝐻)‘𝑚)) → ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1))))))
312311a2d 26 . . . 4 (𝑚 ∈ ℕ → ((𝜑 → (𝑚 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺𝑚)) = (seq1( + , 𝐻)‘𝑚))) → (𝜑 → ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1))))))
3139, 15, 21, 27, 162, 312nnind 8828 . . 3 (𝑁 ∈ ℕ → (𝜑 → (𝑁 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺𝑁)) = (seq1( + , 𝐻)‘𝑁))))
3143, 313mpcom 36 . 2 (𝜑 → (𝑁 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺𝑁)) = (seq1( + , 𝐻)‘𝑁)))
3151, 314mpd 13 1 (𝜑 → (seq𝑀( + , 𝐹)‘(𝐺𝑁)) = (seq1( + , 𝐻)‘𝑁))
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   ∧ w3a 963   = wceq 1332   ∈ wcel 2125   ∖ cdif 3095   ⊆ wss 3098   class class class wbr 3961  ◡ccnv 4578   ↾ cres 4581  ⟶wf 5159  –1-1-onto→wf1o 5162  ‘cfv 5163   Isom wiso 5164  (class class class)co 5814  ℂcc 7709  ℝcr 7710  1c1 7712   + caddc 7714  ℝ*cxr 7890   < clt 7891   ≤ cle 7892   − cmin 8025  ℕcn 8812  ℤcz 9146  ℤ≥cuz 9418  ...cfz 9890  seqcseq 10322  ♯chash 10626 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1481  ax-10 1482  ax-11 1483  ax-i12 1484  ax-bndl 1486  ax-4 1487  ax-17 1503  ax-i9 1507  ax-ial 1511  ax-i5r 1512  ax-13 2127  ax-14 2128  ax-ext 2136  ax-coll 4075  ax-sep 4078  ax-nul 4086  ax-pow 4130  ax-pr 4164  ax-un 4388  ax-setind 4490  ax-iinf 4541  ax-cnex 7802  ax-resscn 7803  ax-1cn 7804  ax-1re 7805  ax-icn 7806  ax-addcl 7807  ax-addrcl 7808  ax-mulcl 7809  ax-addcom 7811  ax-addass 7813  ax-distr 7815  ax-i2m1 7816  ax-0lt1 7817  ax-0id 7819  ax-rnegex 7820  ax-cnre 7822  ax-pre-ltirr 7823  ax-pre-ltwlin 7824  ax-pre-lttrn 7825  ax-pre-ltadd 7827 This theorem depends on definitions:  df-bi 116  df-3or 964  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1740  df-eu 2006  df-mo 2007  df-clab 2141  df-cleq 2147  df-clel 2150  df-nfc 2285  df-ne 2325  df-nel 2420  df-ral 2437  df-rex 2438  df-reu 2439  df-rab 2441  df-v 2711  df-sbc 2934  df-csb 3028  df-dif 3100  df-un 3102  df-in 3104  df-ss 3111  df-nul 3391  df-pw 3541  df-sn 3562  df-pr 3563  df-op 3565  df-uni 3769  df-int 3804  df-iun 3847  df-br 3962  df-opab 4022  df-mpt 4023  df-tr 4059  df-id 4248  df-iord 4321  df-on 4323  df-ilim 4324  df-suc 4326  df-iom 4544  df-xp 4585  df-rel 4586  df-cnv 4587  df-co 4588  df-dm 4589  df-rn 4590  df-res 4591  df-ima 4592  df-iota 5128  df-fun 5165  df-fn 5166  df-f 5167  df-f1 5168  df-fo 5169  df-f1o 5170  df-fv 5171  df-isom 5172  df-riota 5770  df-ov 5817  df-oprab 5818  df-mpo 5819  df-1st 6078  df-2nd 6079  df-recs 6242  df-frec 6328  df-pnf 7893  df-mnf 7894  df-xr 7895  df-ltxr 7896  df-le 7897  df-sub 8027  df-neg 8028  df-inn 8813  df-n0 9070  df-z 9147  df-uz 9419  df-fz 9891  df-fzo 10020  df-seqfrec 10323 This theorem is referenced by:  summodclem2a  11255  prodmodclem2a  11450
 Copyright terms: Public domain W3C validator