seqcoll - Metamath Proof Explorer

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

Theorem seqcoll 14503

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.

Step	Hyp	Ref	Expression
1		seqcoll.3	. 2 ⊢ (𝜑 → 𝑁 ∈ (1...(♯‘𝐴)))
2		elfznn 13593	. . . 4 ⊢ (𝑁 ∈ (1...(♯‘𝐴)) → 𝑁 ∈ ℕ)
3	1, 2	syl 17	. . 3 ⊢ (𝜑 → 𝑁 ∈ ℕ)
4		eleq1 2829	. . . . . 6 ⊢ (𝑦 = 1 → (𝑦 ∈ (1...(♯‘𝐴)) ↔ 1 ∈ (1...(♯‘𝐴))))
5		2fveq3 6911	. . . . . . 7 ⊢ (𝑦 = 1 → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq𝑀( + , 𝐹)‘(𝐺‘1)))
6		fveq2 6906	. . . . . . 7 ⊢ (𝑦 = 1 → (seq1( + , 𝐻)‘𝑦) = (seq1( + , 𝐻)‘1))
7	5, 6	eqeq12d 2753	. . . . . 6 ⊢ (𝑦 = 1 → ((seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦) ↔ (seq𝑀( + , 𝐹)‘(𝐺‘1)) = (seq1( + , 𝐻)‘1)))
8	4, 7	imbi12d 344	. . . . 5 ⊢ (𝑦 = 1 → ((𝑦 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦)) ↔ (1 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘1)) = (seq1( + , 𝐻)‘1))))
9	8	imbi2d 340	. . . 4 ⊢ (𝑦 = 1 → ((𝜑 → (𝑦 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦))) ↔ (𝜑 → (1 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘1)) = (seq1( + , 𝐻)‘1)))))
10		eleq1 2829	. . . . . 6 ⊢ (𝑦 = 𝑚 → (𝑦 ∈ (1...(♯‘𝐴)) ↔ 𝑚 ∈ (1...(♯‘𝐴))))
11		2fveq3 6911	. . . . . . 7 ⊢ (𝑦 = 𝑚 → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)))
12		fveq2 6906	. . . . . . 7 ⊢ (𝑦 = 𝑚 → (seq1( + , 𝐻)‘𝑦) = (seq1( + , 𝐻)‘𝑚))
13	11, 12	eqeq12d 2753	. . . . . 6 ⊢ (𝑦 = 𝑚 → ((seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦) ↔ (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq1( + , 𝐻)‘𝑚)))
14	10, 13	imbi12d 344	. . . . 5 ⊢ (𝑦 = 𝑚 → ((𝑦 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦)) ↔ (𝑚 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq1( + , 𝐻)‘𝑚))))
15	14	imbi2d 340	. . . 4 ⊢ (𝑦 = 𝑚 → ((𝜑 → (𝑦 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦))) ↔ (𝜑 → (𝑚 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq1( + , 𝐻)‘𝑚)))))
16		eleq1 2829	. . . . . 6 ⊢ (𝑦 = (𝑚 + 1) → (𝑦 ∈ (1...(♯‘𝐴)) ↔ (𝑚 + 1) ∈ (1...(♯‘𝐴))))
17		2fveq3 6911	. . . . . . 7 ⊢ (𝑦 = (𝑚 + 1) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))))
18		fveq2 6906	. . . . . . 7 ⊢ (𝑦 = (𝑚 + 1) → (seq1( + , 𝐻)‘𝑦) = (seq1( + , 𝐻)‘(𝑚 + 1)))
19	17, 18	eqeq12d 2753	. . . . . 6 ⊢ (𝑦 = (𝑚 + 1) → ((seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦) ↔ (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1))))
20	16, 19	imbi12d 344	. . . . 5 ⊢ (𝑦 = (𝑚 + 1) → ((𝑦 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦)) ↔ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1)))))
21	20	imbi2d 340	. . . 4 ⊢ (𝑦 = (𝑚 + 1) → ((𝜑 → (𝑦 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦))) ↔ (𝜑 → ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1))))))
22		eleq1 2829	. . . . . 6 ⊢ (𝑦 = 𝑁 → (𝑦 ∈ (1...(♯‘𝐴)) ↔ 𝑁 ∈ (1...(♯‘𝐴))))
23		2fveq3 6911	. . . . . . 7 ⊢ (𝑦 = 𝑁 → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq𝑀( + , 𝐹)‘(𝐺‘𝑁)))
24		fveq2 6906	. . . . . . 7 ⊢ (𝑦 = 𝑁 → (seq1( + , 𝐻)‘𝑦) = (seq1( + , 𝐻)‘𝑁))
25	23, 24	eqeq12d 2753	. . . . . 6 ⊢ (𝑦 = 𝑁 → ((seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦) ↔ (seq𝑀( + , 𝐹)‘(𝐺‘𝑁)) = (seq1( + , 𝐻)‘𝑁)))
26	22, 25	imbi12d 344	. . . . 5 ⊢ (𝑦 = 𝑁 → ((𝑦 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦)) ↔ (𝑁 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑁)) = (seq1( + , 𝐻)‘𝑁))))
27	26	imbi2d 340	. . . 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 7343	. . . . . . . . . . . . 13 ⊢ (𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴) → 𝐺:(1...(♯‘𝐴))–1-1-onto→𝐴)
33	31, 32	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺:(1...(♯‘𝐴))–1-1-onto→𝐴)
34		f1of 6848	. . . . . . . . . . . 12 ⊢ (𝐺:(1...(♯‘𝐴))–1-1-onto→𝐴 → 𝐺:(1...(♯‘𝐴))⟶𝐴)
35	33, 34	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺:(1...(♯‘𝐴))⟶𝐴)
36		elfzuz2 13569	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (1...(♯‘𝐴)) → (♯‘𝐴) ∈ (ℤ_≥‘1))
37	1, 36	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘𝐴) ∈ (ℤ_≥‘1))
38		eluzfz1 13571	. . . . . . . . . . . 12 ⊢ ((♯‘𝐴) ∈ (ℤ_≥‘1) → 1 ∈ (1...(♯‘𝐴)))
39	37, 38	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ (1...(♯‘𝐴)))
40	35, 39	ffvelcdmd 7105	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺‘1) ∈ 𝐴)
41	30, 40	sseldd 3984	. . . . . . . . 9 ⊢ (𝜑 → (𝐺‘1) ∈ (ℤ_≥‘𝑀))
42		eluzle 12891	. . . . . . . . . . . . 13 ⊢ ((♯‘𝐴) ∈ (ℤ_≥‘1) → 1 ≤ (♯‘𝐴))
43	37, 42	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ≤ (♯‘𝐴))
44		fzssz 13566	. . . . . . . . . . . . . . . 16 ⊢ (1...(♯‘𝐴)) ⊆ ℤ
45		zssre 12620	. . . . . . . . . . . . . . . 16 ⊢ ℤ ⊆ ℝ
46	44, 45	sstri 3993	. . . . . . . . . . . . . . 15 ⊢ (1...(♯‘𝐴)) ⊆ ℝ
47	46	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1...(♯‘𝐴)) ⊆ ℝ)
48		ressxr 11305	. . . . . . . . . . . . . 14 ⊢ ℝ ⊆ ℝ^*
49	47, 48	sstrdi 3996	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1...(♯‘𝐴)) ⊆ ℝ^*)
50		eluzelre 12889	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ (ℤ_≥‘𝑀) → 𝑘 ∈ ℝ)
51	50	ssriv 3987	. . . . . . . . . . . . . . 15 ⊢ (ℤ_≥‘𝑀) ⊆ ℝ
52	30, 51	sstrdi 3996	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ⊆ ℝ)
53	52, 48	sstrdi 3996	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ⊆ ℝ^*)
54		eluzfz2 13572	. . . . . . . . . . . . . 14 ⊢ ((♯‘𝐴) ∈ (ℤ_≥‘1) → (♯‘𝐴) ∈ (1...(♯‘𝐴)))
55	37, 54	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (♯‘𝐴) ∈ (1...(♯‘𝐴)))
56		leisorel 14499	. . . . . . . . . . . . 13 ⊢ ((𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴) ∧ ((1...(♯‘𝐴)) ⊆ ℝ^* ∧ 𝐴 ⊆ ℝ^*) ∧ (1 ∈ (1...(♯‘𝐴)) ∧ (♯‘𝐴) ∈ (1...(♯‘𝐴)))) → (1 ≤ (♯‘𝐴) ↔ (𝐺‘1) ≤ (𝐺‘(♯‘𝐴))))
57	31, 49, 53, 39, 55, 56	syl122anc 1381	. . . . . . . . . . . 12 ⊢ (𝜑 → (1 ≤ (♯‘𝐴) ↔ (𝐺‘1) ≤ (𝐺‘(♯‘𝐴))))
58	43, 57	mpbid 232	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐺‘1) ≤ (𝐺‘(♯‘𝐴)))
59	35, 55	ffvelcdmd 7105	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐺‘(♯‘𝐴)) ∈ 𝐴)
60	30, 59	sseldd 3984	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐺‘(♯‘𝐴)) ∈ (ℤ_≥‘𝑀))
61		eluzelz 12888	. . . . . . . . . . . . 13 ⊢ ((𝐺‘(♯‘𝐴)) ∈ (ℤ_≥‘𝑀) → (𝐺‘(♯‘𝐴)) ∈ ℤ)
62	60, 61	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐺‘(♯‘𝐴)) ∈ ℤ)
63		elfz5 13556	. . . . . . . . . . . 12 ⊢ (((𝐺‘1) ∈ (ℤ_≥‘𝑀) ∧ (𝐺‘(♯‘𝐴)) ∈ ℤ) → ((𝐺‘1) ∈ (𝑀...(𝐺‘(♯‘𝐴))) ↔ (𝐺‘1) ≤ (𝐺‘(♯‘𝐴))))
64	41, 62, 63	syl2anc 584	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐺‘1) ∈ (𝑀...(𝐺‘(♯‘𝐴))) ↔ (𝐺‘1) ≤ (𝐺‘(♯‘𝐴))))
65	58, 64	mpbird 257	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺‘1) ∈ (𝑀...(𝐺‘(♯‘𝐴))))
66		fveq2 6906	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝐺‘1) → (𝐹‘𝑘) = (𝐹‘(𝐺‘1)))
67	66	eleq1d 2826	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝐺‘1) → ((𝐹‘𝑘) ∈ 𝑆 ↔ (𝐹‘(𝐺‘1)) ∈ 𝑆))
68	67	imbi2d 340	. . . . . . . . . . 11 ⊢ (𝑘 = (𝐺‘1) → ((𝜑 → (𝐹‘𝑘) ∈ 𝑆) ↔ (𝜑 → (𝐹‘(𝐺‘1)) ∈ 𝑆)))
69		seqcoll.5	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝐺‘(♯‘𝐴)))) → (𝐹‘𝑘) ∈ 𝑆)
70	69	expcom 413	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (𝑀...(𝐺‘(♯‘𝐴))) → (𝜑 → (𝐹‘𝑘) ∈ 𝑆))
71	68, 70	vtoclga 3577	. . . . . . . . . 10 ⊢ ((𝐺‘1) ∈ (𝑀...(𝐺‘(♯‘𝐴))) → (𝜑 → (𝐹‘(𝐺‘1)) ∈ 𝑆))
72	65, 71	mpcom 38	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘(𝐺‘1)) ∈ 𝑆)
73		eluzelz 12888	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺‘1) ∈ (ℤ_≥‘𝑀) → (𝐺‘1) ∈ ℤ)
74	41, 73	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐺‘1) ∈ ℤ)
75		peano2zm 12660	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺‘1) ∈ ℤ → ((𝐺‘1) − 1) ∈ ℤ)
76	74, 75	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐺‘1) − 1) ∈ ℤ)
77	76	zred 12722	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐺‘1) − 1) ∈ ℝ)
78	74	zred 12722	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐺‘1) ∈ ℝ)
79	62	zred 12722	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐺‘(♯‘𝐴)) ∈ ℝ)
80	78	lem1d 12201	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐺‘1) − 1) ≤ (𝐺‘1))
81	77, 78, 79, 80, 58	letrd 11418	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐺‘1) − 1) ≤ (𝐺‘(♯‘𝐴)))
82		eluz 12892	. . . . . . . . . . . . . . 15 ⊢ ((((𝐺‘1) − 1) ∈ ℤ ∧ (𝐺‘(♯‘𝐴)) ∈ ℤ) → ((𝐺‘(♯‘𝐴)) ∈ (ℤ_≥‘((𝐺‘1) − 1)) ↔ ((𝐺‘1) − 1) ≤ (𝐺‘(♯‘𝐴))))
83	76, 62, 82	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐺‘(♯‘𝐴)) ∈ (ℤ_≥‘((𝐺‘1) − 1)) ↔ ((𝐺‘1) − 1) ≤ (𝐺‘(♯‘𝐴))))
84	81, 83	mpbird 257	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐺‘(♯‘𝐴)) ∈ (ℤ_≥‘((𝐺‘1) − 1)))
85		fzss2 13604	. . . . . . . . . . . . 13 ⊢ ((𝐺‘(♯‘𝐴)) ∈ (ℤ_≥‘((𝐺‘1) − 1)) → (𝑀...((𝐺‘1) − 1)) ⊆ (𝑀...(𝐺‘(♯‘𝐴))))
86	84, 85	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑀...((𝐺‘1) − 1)) ⊆ (𝑀...(𝐺‘(♯‘𝐴))))
87	86	sselda 3983	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...((𝐺‘1) − 1))) → 𝑘 ∈ (𝑀...(𝐺‘(♯‘𝐴))))
88		eluzel2 12883	. . . . . . . . . . . . . . 15 ⊢ ((𝐺‘1) ∈ (ℤ_≥‘𝑀) → 𝑀 ∈ ℤ)
89	41, 88	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ∈ ℤ)
90		elfzm11 13635	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℤ ∧ (𝐺‘1) ∈ ℤ) → (𝑘 ∈ (𝑀...((𝐺‘1) − 1)) ↔ (𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 < (𝐺‘1))))
91	89, 74, 90	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑘 ∈ (𝑀...((𝐺‘1) − 1)) ↔ (𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 < (𝐺‘1))))
92		simp3 1139	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 < (𝐺‘1)) → 𝑘 < (𝐺‘1))
93	78	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐺‘1) ∈ ℝ)
94	52	sselda 3983	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑘 ∈ ℝ)
95		f1ocnv 6860	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐺:(1...(♯‘𝐴))–1-1-onto→𝐴 → ^◡𝐺:𝐴–1-1-onto→(1...(♯‘𝐴)))
96	33, 95	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ^◡𝐺:𝐴–1-1-onto→(1...(♯‘𝐴)))
97		f1of 6848	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (^◡𝐺:𝐴–1-1-onto→(1...(♯‘𝐴)) → ^◡𝐺:𝐴⟶(1...(♯‘𝐴)))
98	96, 97	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ^◡𝐺:𝐴⟶(1...(♯‘𝐴)))
99	98	ffvelcdmda 7104	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (^◡𝐺‘𝑘) ∈ (1...(♯‘𝐴)))
100		elfznn 13593	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((^◡𝐺‘𝑘) ∈ (1...(♯‘𝐴)) → (^◡𝐺‘𝑘) ∈ ℕ)
101	99, 100	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (^◡𝐺‘𝑘) ∈ ℕ)
102	101	nnge1d 12314	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 1 ≤ (^◡𝐺‘𝑘))
103	31	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴))
104	49	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (1...(♯‘𝐴)) ⊆ ℝ^*)
105	53	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐴 ⊆ ℝ^*)
106	39	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 1 ∈ (1...(♯‘𝐴)))
107		leisorel 14499	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴) ∧ ((1...(♯‘𝐴)) ⊆ ℝ^* ∧ 𝐴 ⊆ ℝ^*) ∧ (1 ∈ (1...(♯‘𝐴)) ∧ (^◡𝐺‘𝑘) ∈ (1...(♯‘𝐴)))) → (1 ≤ (^◡𝐺‘𝑘) ↔ (𝐺‘1) ≤ (𝐺‘(^◡𝐺‘𝑘))))
108	103, 104, 105, 106, 99, 107	syl122anc 1381	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (1 ≤ (^◡𝐺‘𝑘) ↔ (𝐺‘1) ≤ (𝐺‘(^◡𝐺‘𝑘))))
109	102, 108	mpbid 232	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐺‘1) ≤ (𝐺‘(^◡𝐺‘𝑘)))
110		f1ocnvfv2 7297	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺:(1...(♯‘𝐴))–1-1-onto→𝐴 ∧ 𝑘 ∈ 𝐴) → (𝐺‘(^◡𝐺‘𝑘)) = 𝑘)
111	33, 110	sylan 580	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐺‘(^◡𝐺‘𝑘)) = 𝑘)
112	109, 111	breqtrd 5169	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐺‘1) ≤ 𝑘)
113	93, 94, 112	lensymd 11412	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ¬ 𝑘 < (𝐺‘1))
114	113	ex 412	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑘 ∈ 𝐴 → ¬ 𝑘 < (𝐺‘1)))
115	114	con2d 134	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑘 < (𝐺‘1) → ¬ 𝑘 ∈ 𝐴))
116	92, 115	syl5 34	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 < (𝐺‘1)) → ¬ 𝑘 ∈ 𝐴))
117	91, 116	sylbid 240	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑘 ∈ (𝑀...((𝐺‘1) − 1)) → ¬ 𝑘 ∈ 𝐴))
118	117	imp 406	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...((𝐺‘1) − 1))) → ¬ 𝑘 ∈ 𝐴)
119	87, 118	eldifd 3962	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...((𝐺‘1) − 1))) → 𝑘 ∈ ((𝑀...(𝐺‘(♯‘𝐴))) ∖ 𝐴))
120		seqcoll.6	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀...(𝐺‘(♯‘𝐴))) ∖ 𝐴)) → (𝐹‘𝑘) = 𝑍)
121	119, 120	syldan 591	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...((𝐺‘1) − 1))) → (𝐹‘𝑘) = 𝑍)
122	28, 29, 41, 72, 121	seqid 14088	. . . . . . . 8 ⊢ (𝜑 → (seq𝑀( + , 𝐹) ↾ (ℤ_≥‘(𝐺‘1))) = seq(𝐺‘1)( + , 𝐹))
123	122	fveq1d 6908	. . . . . . 7 ⊢ (𝜑 → ((seq𝑀( + , 𝐹) ↾ (ℤ_≥‘(𝐺‘1)))‘(𝐺‘1)) = (seq(𝐺‘1)( + , 𝐹)‘(𝐺‘1)))
124		uzid 12893	. . . . . . . . 9 ⊢ ((𝐺‘1) ∈ ℤ → (𝐺‘1) ∈ (ℤ_≥‘(𝐺‘1)))
125	74, 124	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝐺‘1) ∈ (ℤ_≥‘(𝐺‘1)))
126	125	fvresd 6926	. . . . . . 7 ⊢ (𝜑 → ((seq𝑀( + , 𝐹) ↾ (ℤ_≥‘(𝐺‘1)))‘(𝐺‘1)) = (seq𝑀( + , 𝐹)‘(𝐺‘1)))
127		seq1 14055	. . . . . . . . 9 ⊢ ((𝐺‘1) ∈ ℤ → (seq(𝐺‘1)( + , 𝐹)‘(𝐺‘1)) = (𝐹‘(𝐺‘1)))
128	74, 127	syl 17	. . . . . . . 8 ⊢ (𝜑 → (seq(𝐺‘1)( + , 𝐹)‘(𝐺‘1)) = (𝐹‘(𝐺‘1)))
129		fveq2 6906	. . . . . . . . . . . 12 ⊢ (𝑛 = 1 → (𝐻‘𝑛) = (𝐻‘1))
130		2fveq3 6911	. . . . . . . . . . . 12 ⊢ (𝑛 = 1 → (𝐹‘(𝐺‘𝑛)) = (𝐹‘(𝐺‘1)))
131	129, 130	eqeq12d 2753	. . . . . . . . . . 11 ⊢ (𝑛 = 1 → ((𝐻‘𝑛) = (𝐹‘(𝐺‘𝑛)) ↔ (𝐻‘1) = (𝐹‘(𝐺‘1))))
132	131	imbi2d 340	. . . . . . . . . 10 ⊢ (𝑛 = 1 → ((𝜑 → (𝐻‘𝑛) = (𝐹‘(𝐺‘𝑛))) ↔ (𝜑 → (𝐻‘1) = (𝐹‘(𝐺‘1)))))
133		seqcoll.7	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (𝐻‘𝑛) = (𝐹‘(𝐺‘𝑛)))
134	133	expcom 413	. . . . . . . . . 10 ⊢ (𝑛 ∈ (1...(♯‘𝐴)) → (𝜑 → (𝐻‘𝑛) = (𝐹‘(𝐺‘𝑛))))
135	132, 134	vtoclga 3577	. . . . . . . . 9 ⊢ (1 ∈ (1...(♯‘𝐴)) → (𝜑 → (𝐻‘1) = (𝐹‘(𝐺‘1))))
136	39, 135	mpcom 38	. . . . . . . 8 ⊢ (𝜑 → (𝐻‘1) = (𝐹‘(𝐺‘1)))
137	128, 136	eqtr4d 2780	. . . . . . 7 ⊢ (𝜑 → (seq(𝐺‘1)( + , 𝐹)‘(𝐺‘1)) = (𝐻‘1))
138	123, 126, 137	3eqtr3d 2785	. . . . . 6 ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘(𝐺‘1)) = (𝐻‘1))
139		1z 12647	. . . . . . 7 ⊢ 1 ∈ ℤ
140		seq1 14055	. . . . . . 7 ⊢ (1 ∈ ℤ → (seq1( + , 𝐻)‘1) = (𝐻‘1))
141	139, 140	ax-mp 5	. . . . . 6 ⊢ (seq1( + , 𝐻)‘1) = (𝐻‘1)
142	138, 141	eqtr4di 2795	. . . . 5 ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘(𝐺‘1)) = (seq1( + , 𝐻)‘1))
143	142	a1d 25	. . . 4 ⊢ (𝜑 → (1 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘1)) = (seq1( + , 𝐻)‘1)))
144		simplr 769	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝑚 ∈ ℕ)
145		nnuz 12921	. . . . . . . . . . 11 ⊢ ℕ = (ℤ_≥‘1)
146	144, 145	eleqtrdi 2851	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝑚 ∈ (ℤ_≥‘1))
147		nnz 12634	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℤ)
148	147	ad2antlr 727	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝑚 ∈ ℤ)
149		elfzuz3 13561	. . . . . . . . . . . 12 ⊢ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (♯‘𝐴) ∈ (ℤ_≥‘(𝑚 + 1)))
150	149	adantl 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (♯‘𝐴) ∈ (ℤ_≥‘(𝑚 + 1)))
151		peano2uzr 12945	. . . . . . . . . . 11 ⊢ ((𝑚 ∈ ℤ ∧ (♯‘𝐴) ∈ (ℤ_≥‘(𝑚 + 1))) → (♯‘𝐴) ∈ (ℤ_≥‘𝑚))
152	148, 150, 151	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (♯‘𝐴) ∈ (ℤ_≥‘𝑚))
153		elfzuzb 13558	. . . . . . . . . 10 ⊢ (𝑚 ∈ (1...(♯‘𝐴)) ↔ (𝑚 ∈ (ℤ_≥‘1) ∧ (♯‘𝐴) ∈ (ℤ_≥‘𝑚)))
154	146, 152, 153	sylanbrc 583	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝑚 ∈ (1...(♯‘𝐴)))
155	154	ex 412	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → 𝑚 ∈ (1...(♯‘𝐴))))
156	155	imim1d 82	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑚 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq1( + , 𝐻)‘𝑚)) → ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq1( + , 𝐻)‘𝑚))))
157		oveq1 7438	. . . . . . . . . 10 ⊢ ((seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq1( + , 𝐻)‘𝑚) → ((seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) + (𝐻‘(𝑚 + 1))) = ((seq1( + , 𝐻)‘𝑚) + (𝐻‘(𝑚 + 1))))
158		seqcoll.1b	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑆) → (𝑘 + 𝑍) = 𝑘)
159	158	ad4ant14 752	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ 𝑆) → (𝑘 + 𝑍) = 𝑘)
160	30	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝐴 ⊆ (ℤ_≥‘𝑀))
161	35	ad2antrr 726	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝐺:(1...(♯‘𝐴))⟶𝐴)
162	161, 154	ffvelcdmd 7105	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘𝑚) ∈ 𝐴)
163	160, 162	sseldd 3984	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘𝑚) ∈ (ℤ_≥‘𝑀))
164		nnre 12273	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℝ)
165	164	ad2antlr 727	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝑚 ∈ ℝ)
166	165	ltp1d 12198	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝑚 < (𝑚 + 1))
167	31	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴))
168		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝑚 + 1) ∈ (1...(♯‘𝐴)))
169		isorel 7346	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴) ∧ (𝑚 ∈ (1...(♯‘𝐴)) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴)))) → (𝑚 < (𝑚 + 1) ↔ (𝐺‘𝑚) < (𝐺‘(𝑚 + 1))))
170	167, 154, 168, 169	syl12anc 837	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝑚 < (𝑚 + 1) ↔ (𝐺‘𝑚) < (𝐺‘(𝑚 + 1))))
171	166, 170	mpbid 232	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘𝑚) < (𝐺‘(𝑚 + 1)))
172		eluzelz 12888	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺‘𝑚) ∈ (ℤ_≥‘𝑀) → (𝐺‘𝑚) ∈ ℤ)
173	163, 172	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘𝑚) ∈ ℤ)
174	161, 168	ffvelcdmd 7105	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(𝑚 + 1)) ∈ 𝐴)
175	160, 174	sseldd 3984	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(𝑚 + 1)) ∈ (ℤ_≥‘𝑀))
176		eluzelz 12888	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺‘(𝑚 + 1)) ∈ (ℤ_≥‘𝑀) → (𝐺‘(𝑚 + 1)) ∈ ℤ)
177	175, 176	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(𝑚 + 1)) ∈ ℤ)
178		zltlem1 12670	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐺‘𝑚) ∈ ℤ ∧ (𝐺‘(𝑚 + 1)) ∈ ℤ) → ((𝐺‘𝑚) < (𝐺‘(𝑚 + 1)) ↔ (𝐺‘𝑚) ≤ ((𝐺‘(𝑚 + 1)) − 1)))
179	173, 177, 178	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝐺‘𝑚) < (𝐺‘(𝑚 + 1)) ↔ (𝐺‘𝑚) ≤ ((𝐺‘(𝑚 + 1)) − 1)))
180	171, 179	mpbid 232	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘𝑚) ≤ ((𝐺‘(𝑚 + 1)) − 1))
181		peano2zm 12660	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺‘(𝑚 + 1)) ∈ ℤ → ((𝐺‘(𝑚 + 1)) − 1) ∈ ℤ)
182	177, 181	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝐺‘(𝑚 + 1)) − 1) ∈ ℤ)
183		eluz 12892	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺‘𝑚) ∈ ℤ ∧ ((𝐺‘(𝑚 + 1)) − 1) ∈ ℤ) → (((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ_≥‘(𝐺‘𝑚)) ↔ (𝐺‘𝑚) ≤ ((𝐺‘(𝑚 + 1)) − 1)))
184	173, 182, 183	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ_≥‘(𝐺‘𝑚)) ↔ (𝐺‘𝑚) ≤ ((𝐺‘(𝑚 + 1)) − 1)))
185	180, 184	mpbird 257	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ_≥‘(𝐺‘𝑚)))
186	182	zred 12722	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝐺‘(𝑚 + 1)) − 1) ∈ ℝ)
187	177	zred 12722	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(𝑚 + 1)) ∈ ℝ)
188	79	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(♯‘𝐴)) ∈ ℝ)
189	187	lem1d 12201	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝐺‘(𝑚 + 1)) − 1) ≤ (𝐺‘(𝑚 + 1)))
190		elfzle2 13568	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (𝑚 + 1) ≤ (♯‘𝐴))
191	190	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝑚 + 1) ≤ (♯‘𝐴))
192	49	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (1...(♯‘𝐴)) ⊆ ℝ^*)
193	53	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝐴 ⊆ ℝ^*)
194	55	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (♯‘𝐴) ∈ (1...(♯‘𝐴)))
195		leisorel 14499	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴) ∧ ((1...(♯‘𝐴)) ⊆ ℝ^* ∧ 𝐴 ⊆ ℝ^*) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ (♯‘𝐴) ∈ (1...(♯‘𝐴)))) → ((𝑚 + 1) ≤ (♯‘𝐴) ↔ (𝐺‘(𝑚 + 1)) ≤ (𝐺‘(♯‘𝐴))))
196	167, 192, 193, 168, 194, 195	syl122anc 1381	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝑚 + 1) ≤ (♯‘𝐴) ↔ (𝐺‘(𝑚 + 1)) ≤ (𝐺‘(♯‘𝐴))))
197	191, 196	mpbid 232	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(𝑚 + 1)) ≤ (𝐺‘(♯‘𝐴)))
198	186, 187, 188, 189, 197	letrd 11418	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝐺‘(𝑚 + 1)) − 1) ≤ (𝐺‘(♯‘𝐴)))
199	62	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(♯‘𝐴)) ∈ ℤ)
200		eluz 12892	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐺‘(𝑚 + 1)) − 1) ∈ ℤ ∧ (𝐺‘(♯‘𝐴)) ∈ ℤ) → ((𝐺‘(♯‘𝐴)) ∈ (ℤ_≥‘((𝐺‘(𝑚 + 1)) − 1)) ↔ ((𝐺‘(𝑚 + 1)) − 1) ≤ (𝐺‘(♯‘𝐴))))
201	182, 199, 200	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝐺‘(♯‘𝐴)) ∈ (ℤ_≥‘((𝐺‘(𝑚 + 1)) − 1)) ↔ ((𝐺‘(𝑚 + 1)) − 1) ≤ (𝐺‘(♯‘𝐴))))
202	198, 201	mpbird 257	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(♯‘𝐴)) ∈ (ℤ_≥‘((𝐺‘(𝑚 + 1)) − 1)))
203		uztrn 12896	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐺‘(♯‘𝐴)) ∈ (ℤ_≥‘((𝐺‘(𝑚 + 1)) − 1)) ∧ ((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ_≥‘(𝐺‘𝑚))) → (𝐺‘(♯‘𝐴)) ∈ (ℤ_≥‘(𝐺‘𝑚)))
204	202, 185, 203	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(♯‘𝐴)) ∈ (ℤ_≥‘(𝐺‘𝑚)))
205		fzss2 13604	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺‘(♯‘𝐴)) ∈ (ℤ_≥‘(𝐺‘𝑚)) → (𝑀...(𝐺‘𝑚)) ⊆ (𝑀...(𝐺‘(♯‘𝐴))))
206	204, 205	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝑀...(𝐺‘𝑚)) ⊆ (𝑀...(𝐺‘(♯‘𝐴))))
207	206	sselda 3983	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (𝑀...(𝐺‘𝑚))) → 𝑘 ∈ (𝑀...(𝐺‘(♯‘𝐴))))
208	69	ad4ant14 752	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (𝑀...(𝐺‘(♯‘𝐴)))) → (𝐹‘𝑘) ∈ 𝑆)
209	207, 208	syldan 591	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (𝑀...(𝐺‘𝑚))) → (𝐹‘𝑘) ∈ 𝑆)
210		seqcoll.c	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑘 ∈ 𝑆 ∧ 𝑛 ∈ 𝑆)) → (𝑘 + 𝑛) ∈ 𝑆)
211	210	ad4ant14 752	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ (𝑘 ∈ 𝑆 ∧ 𝑛 ∈ 𝑆)) → (𝑘 + 𝑛) ∈ 𝑆)
212	163, 209, 211	seqcl 14063	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) ∈ 𝑆)
213		simplll 775	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1))) → 𝜑)
214		elfzuz 13560	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1)) → 𝑘 ∈ (ℤ_≥‘((𝐺‘𝑚) + 1)))
215		peano2uz 12943	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺‘𝑚) ∈ (ℤ_≥‘𝑀) → ((𝐺‘𝑚) + 1) ∈ (ℤ_≥‘𝑀))
216	163, 215	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝐺‘𝑚) + 1) ∈ (ℤ_≥‘𝑀))
217		uztrn 12896	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ (ℤ_≥‘((𝐺‘𝑚) + 1)) ∧ ((𝐺‘𝑚) + 1) ∈ (ℤ_≥‘𝑀)) → 𝑘 ∈ (ℤ_≥‘𝑀))
218	214, 216, 217	syl2anr 597	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1))) → 𝑘 ∈ (ℤ_≥‘𝑀))
219		elfzuz3 13561	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1)) → ((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ_≥‘𝑘))
220		uztrn 12896	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐺‘(♯‘𝐴)) ∈ (ℤ_≥‘((𝐺‘(𝑚 + 1)) − 1)) ∧ ((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ_≥‘𝑘)) → (𝐺‘(♯‘𝐴)) ∈ (ℤ_≥‘𝑘))
221	202, 219, 220	syl2an 596	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1))) → (𝐺‘(♯‘𝐴)) ∈ (ℤ_≥‘𝑘))
222		elfzuzb 13558	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (𝑀...(𝐺‘(♯‘𝐴))) ↔ (𝑘 ∈ (ℤ_≥‘𝑀) ∧ (𝐺‘(♯‘𝐴)) ∈ (ℤ_≥‘𝑘)))
223	218, 221, 222	sylanbrc 583	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1))) → 𝑘 ∈ (𝑀...(𝐺‘(♯‘𝐴))))
224	147	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → 𝑚 ∈ ℤ)
225	98	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → ^◡𝐺:𝐴⟶(1...(♯‘𝐴)))
226		simprr 773	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → 𝑘 ∈ 𝐴)
227	225, 226	ffvelcdmd 7105	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → (^◡𝐺‘𝑘) ∈ (1...(♯‘𝐴)))
228	227	elfzelzd 13565	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → (^◡𝐺‘𝑘) ∈ ℤ)
229		btwnnz 12694	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑚 ∈ ℤ ∧ 𝑚 < (^◡𝐺‘𝑘) ∧ (^◡𝐺‘𝑘) < (𝑚 + 1)) → ¬ (^◡𝐺‘𝑘) ∈ ℤ)
230	229	3expib 1123	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 ∈ ℤ → ((𝑚 < (^◡𝐺‘𝑘) ∧ (^◡𝐺‘𝑘) < (𝑚 + 1)) → ¬ (^◡𝐺‘𝑘) ∈ ℤ))
231	230	con2d 134	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 ∈ ℤ → ((^◡𝐺‘𝑘) ∈ ℤ → ¬ (𝑚 < (^◡𝐺‘𝑘) ∧ (^◡𝐺‘𝑘) < (𝑚 + 1))))
232	224, 228, 231	sylc 65	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → ¬ (𝑚 < (^◡𝐺‘𝑘) ∧ (^◡𝐺‘𝑘) < (𝑚 + 1)))
233	31	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → 𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴))
234	154	adantrr 717	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → 𝑚 ∈ (1...(♯‘𝐴)))
235		isorel 7346	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴) ∧ (𝑚 ∈ (1...(♯‘𝐴)) ∧ (^◡𝐺‘𝑘) ∈ (1...(♯‘𝐴)))) → (𝑚 < (^◡𝐺‘𝑘) ↔ (𝐺‘𝑚) < (𝐺‘(^◡𝐺‘𝑘))))
236	233, 234, 227, 235	syl12anc 837	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → (𝑚 < (^◡𝐺‘𝑘) ↔ (𝐺‘𝑚) < (𝐺‘(^◡𝐺‘𝑘))))
237	33	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → 𝐺:(1...(♯‘𝐴))–1-1-onto→𝐴)
238	237, 226, 110	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → (𝐺‘(^◡𝐺‘𝑘)) = 𝑘)
239	238	breq2d 5155	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → ((𝐺‘𝑚) < (𝐺‘(^◡𝐺‘𝑘)) ↔ (𝐺‘𝑚) < 𝑘))
240	173	adantrr 717	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → (𝐺‘𝑚) ∈ ℤ)
241	30	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → 𝐴 ⊆ (ℤ_≥‘𝑀))
242	241, 226	sseldd 3984	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → 𝑘 ∈ (ℤ_≥‘𝑀))
243		eluzelz 12888	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 ∈ (ℤ_≥‘𝑀) → 𝑘 ∈ ℤ)
244	242, 243	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → 𝑘 ∈ ℤ)
245		zltp1le 12667	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐺‘𝑚) ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((𝐺‘𝑚) < 𝑘 ↔ ((𝐺‘𝑚) + 1) ≤ 𝑘))
246	240, 244, 245	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → ((𝐺‘𝑚) < 𝑘 ↔ ((𝐺‘𝑚) + 1) ≤ 𝑘))
247	236, 239, 246	3bitrd 305	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → (𝑚 < (^◡𝐺‘𝑘) ↔ ((𝐺‘𝑚) + 1) ≤ 𝑘))
248	168	adantrr 717	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → (𝑚 + 1) ∈ (1...(♯‘𝐴)))
249		isorel 7346	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴) ∧ ((^◡𝐺‘𝑘) ∈ (1...(♯‘𝐴)) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴)))) → ((^◡𝐺‘𝑘) < (𝑚 + 1) ↔ (𝐺‘(^◡𝐺‘𝑘)) < (𝐺‘(𝑚 + 1))))
250	233, 227, 248, 249	syl12anc 837	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → ((^◡𝐺‘𝑘) < (𝑚 + 1) ↔ (𝐺‘(^◡𝐺‘𝑘)) < (𝐺‘(𝑚 + 1))))
251	238	breq1d 5153	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → ((𝐺‘(^◡𝐺‘𝑘)) < (𝐺‘(𝑚 + 1)) ↔ 𝑘 < (𝐺‘(𝑚 + 1))))
252	177	adantrr 717	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → (𝐺‘(𝑚 + 1)) ∈ ℤ)
253		zltlem1 12670	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 ∈ ℤ ∧ (𝐺‘(𝑚 + 1)) ∈ ℤ) → (𝑘 < (𝐺‘(𝑚 + 1)) ↔ 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1)))
254	244, 252, 253	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → (𝑘 < (𝐺‘(𝑚 + 1)) ↔ 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1)))
255	250, 251, 254	3bitrd 305	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → ((^◡𝐺‘𝑘) < (𝑚 + 1) ↔ 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1)))
256	247, 255	anbi12d 632	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → ((𝑚 < (^◡𝐺‘𝑘) ∧ (^◡𝐺‘𝑘) < (𝑚 + 1)) ↔ (((𝐺‘𝑚) + 1) ≤ 𝑘 ∧ 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1))))
257	232, 256	mtbid 324	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → ¬ (((𝐺‘𝑚) + 1) ≤ 𝑘 ∧ 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1)))
258	257	expr 456	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝑘 ∈ 𝐴 → ¬ (((𝐺‘𝑚) + 1) ≤ 𝑘 ∧ 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1))))
259	258	con2d 134	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((((𝐺‘𝑚) + 1) ≤ 𝑘 ∧ 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1)) → ¬ 𝑘 ∈ 𝐴))
260		elfzle1 13567	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1)) → ((𝐺‘𝑚) + 1) ≤ 𝑘)
261		elfzle2 13568	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1)) → 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1))
262	260, 261	jca 511	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1)) → (((𝐺‘𝑚) + 1) ≤ 𝑘 ∧ 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1)))
263	259, 262	impel 505	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1))) → ¬ 𝑘 ∈ 𝐴)
264	223, 263	eldifd 3962	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1))) → 𝑘 ∈ ((𝑀...(𝐺‘(♯‘𝐴))) ∖ 𝐴))
265	213, 264, 120	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1))) → (𝐹‘𝑘) = 𝑍)
266	159, 163, 185, 212, 265	seqid2 14089	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq𝑀( + , 𝐹)‘((𝐺‘(𝑚 + 1)) − 1)))
267	266	oveq1d 7446	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) + (𝐹‘(𝐺‘(𝑚 + 1)))) = ((seq𝑀( + , 𝐹)‘((𝐺‘(𝑚 + 1)) − 1)) + (𝐹‘(𝐺‘(𝑚 + 1)))))
268		fveq2 6906	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = (𝑚 + 1) → (𝐻‘𝑛) = (𝐻‘(𝑚 + 1)))
269		2fveq3 6911	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = (𝑚 + 1) → (𝐹‘(𝐺‘𝑛)) = (𝐹‘(𝐺‘(𝑚 + 1))))
270	268, 269	eqeq12d 2753	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = (𝑚 + 1) → ((𝐻‘𝑛) = (𝐹‘(𝐺‘𝑛)) ↔ (𝐻‘(𝑚 + 1)) = (𝐹‘(𝐺‘(𝑚 + 1)))))
271	270	imbi2d 340	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = (𝑚 + 1) → ((𝜑 → (𝐻‘𝑛) = (𝐹‘(𝐺‘𝑛))) ↔ (𝜑 → (𝐻‘(𝑚 + 1)) = (𝐹‘(𝐺‘(𝑚 + 1))))))
272	271, 134	vtoclga 3577	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (𝜑 → (𝐻‘(𝑚 + 1)) = (𝐹‘(𝐺‘(𝑚 + 1)))))
273	272	impcom 407	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐻‘(𝑚 + 1)) = (𝐹‘(𝐺‘(𝑚 + 1))))
274	273	adantlr 715	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐻‘(𝑚 + 1)) = (𝐹‘(𝐺‘(𝑚 + 1))))
275	274	oveq2d 7447	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) + (𝐻‘(𝑚 + 1))) = ((seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) + (𝐹‘(𝐺‘(𝑚 + 1)))))
276	89	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝑀 ∈ ℤ)
277	177	zcnd 12723	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(𝑚 + 1)) ∈ ℂ)
278		ax-1cn 11213	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
279		npcan 11517	. . . . . . . . . . . . . . 15 ⊢ (((𝐺‘(𝑚 + 1)) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝐺‘(𝑚 + 1)) − 1) + 1) = (𝐺‘(𝑚 + 1)))
280	277, 278, 279	sylancl 586	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (((𝐺‘(𝑚 + 1)) − 1) + 1) = (𝐺‘(𝑚 + 1)))
281		uztrn 12896	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ_≥‘(𝐺‘𝑚)) ∧ (𝐺‘𝑚) ∈ (ℤ_≥‘𝑀)) → ((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ_≥‘𝑀))
282	185, 163, 281	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ_≥‘𝑀))
283		eluzp1p1 12906	. . . . . . . . . . . . . . 15 ⊢ (((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ_≥‘𝑀) → (((𝐺‘(𝑚 + 1)) − 1) + 1) ∈ (ℤ_≥‘(𝑀 + 1)))
284	282, 283	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (((𝐺‘(𝑚 + 1)) − 1) + 1) ∈ (ℤ_≥‘(𝑀 + 1)))
285	280, 284	eqeltrrd 2842	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(𝑚 + 1)) ∈ (ℤ_≥‘(𝑀 + 1)))
286		seqm1 14060	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℤ ∧ (𝐺‘(𝑚 + 1)) ∈ (ℤ_≥‘(𝑀 + 1))) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = ((seq𝑀( + , 𝐹)‘((𝐺‘(𝑚 + 1)) − 1)) + (𝐹‘(𝐺‘(𝑚 + 1)))))
287	276, 285, 286	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = ((seq𝑀( + , 𝐹)‘((𝐺‘(𝑚 + 1)) − 1)) + (𝐹‘(𝐺‘(𝑚 + 1)))))
288	267, 275, 287	3eqtr4rd 2788	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = ((seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) + (𝐻‘(𝑚 + 1))))
289		seqp1 14057	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ (ℤ_≥‘1) → (seq1( + , 𝐻)‘(𝑚 + 1)) = ((seq1( + , 𝐻)‘𝑚) + (𝐻‘(𝑚 + 1))))
290	146, 289	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (seq1( + , 𝐻)‘(𝑚 + 1)) = ((seq1( + , 𝐻)‘𝑚) + (𝐻‘(𝑚 + 1))))
291	288, 290	eqeq12d 2753	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1)) ↔ ((seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) + (𝐻‘(𝑚 + 1))) = ((seq1( + , 𝐻)‘𝑚) + (𝐻‘(𝑚 + 1)))))
292	157, 291	imbitrrid 246	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq1( + , 𝐻)‘𝑚) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1))))
293	292	ex 412	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → ((seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq1( + , 𝐻)‘𝑚) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1)))))
294	293	a2d 29	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq1( + , 𝐻)‘𝑚)) → ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1)))))
295	156, 294	syld 47	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑚 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq1( + , 𝐻)‘𝑚)) → ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1)))))
296	295	expcom 413	. . . . 5 ⊢ (𝑚 ∈ ℕ → (𝜑 → ((𝑚 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq1( + , 𝐻)‘𝑚)) → ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1))))))
297	296	a2d 29	. . . 4 ⊢ (𝑚 ∈ ℕ → ((𝜑 → (𝑚 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq1( + , 𝐻)‘𝑚))) → (𝜑 → ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1))))))
298	9, 15, 21, 27, 143, 297	nnind 12284	. . 3 ⊢ (𝑁 ∈ ℕ → (𝜑 → (𝑁 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑁)) = (seq1( + , 𝐻)‘𝑁))))
299	3, 298	mpcom 38	. 2 ⊢ (𝜑 → (𝑁 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑁)) = (seq1( + , 𝐻)‘𝑁)))
300	1, 299	mpd 15	1 ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘(𝐺‘𝑁)) = (seq1( + , 𝐻)‘𝑁))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1540 ∈ wcel 2108 ∖ cdif 3948 ⊆ wss 3951 class class class wbr 5143 ^◡ccnv 5684 ↾ cres 5687 ⟶wf 6557 –1-1-onto→wf1o 6560 ‘cfv 6561 Isom wiso 6562 (class class class)co 7431 ℂcc 11153 ℝcr 11154 1c1 11156 + caddc 11158 ℝ^*cxr 11294 < clt 11295 ≤ cle 11296 − cmin 11492 ℕcn 12266 ℤcz 12613 ℤ_≥cuz 12878 ...cfz 13547 seqcseq 14042 ♯chash 14369

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755 ax-cnex 11211 ax-resscn 11212 ax-1cn 11213 ax-icn 11214 ax-addcl 11215 ax-addrcl 11216 ax-mulcl 11217 ax-mulrcl 11218 ax-mulcom 11219 ax-addass 11220 ax-mulass 11221 ax-distr 11222 ax-i2m1 11223 ax-1ne0 11224 ax-1rid 11225 ax-rnegex 11226 ax-rrecex 11227 ax-cnre 11228 ax-pre-lttri 11229 ax-pre-lttrn 11230 ax-pre-ltadd 11231 ax-pre-mulgt0 11232

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-reu 3381 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-pss 3971 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-iun 4993 df-br 5144 df-opab 5206 df-mpt 5226 df-tr 5260 df-id 5578 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5637 df-we 5639 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-pred 6321 df-ord 6387 df-on 6388 df-lim 6389 df-suc 6390 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-isom 6570 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-om 7888 df-1st 8014 df-2nd 8015 df-frecs 8306 df-wrecs 8337 df-recs 8411 df-rdg 8450 df-er 8745 df-en 8986 df-dom 8987 df-sdom 8988 df-pnf 11297 df-mnf 11298 df-xr 11299 df-ltxr 11300 df-le 11301 df-sub 11494 df-neg 11495 df-nn 12267 df-n0 12527 df-z 12614 df-uz 12879 df-fz 13548 df-seq 14043

This theorem is referenced by: seqcoll2 14504 summolem2a 15751 prodmolem2a 15970

W3C validator