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 13821

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 12935	. . . 4 ⊢ (𝑁 ∈ (1...(♯‘𝐴)) → 𝑁 ∈ ℕ)
3	1, 2	syl 17	. . 3 ⊢ (𝜑 → 𝑁 ∈ ℕ)
4		eleq1 2900	. . . . . 6 ⊢ (𝑦 = 1 → (𝑦 ∈ (1...(♯‘𝐴)) ↔ 1 ∈ (1...(♯‘𝐴))))
5		2fveq3 6674	. . . . . . 7 ⊢ (𝑦 = 1 → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq𝑀( + , 𝐹)‘(𝐺‘1)))
6		fveq2 6669	. . . . . . 7 ⊢ (𝑦 = 1 → (seq1( + , 𝐻)‘𝑦) = (seq1( + , 𝐻)‘1))
7	5, 6	eqeq12d 2837	. . . . . 6 ⊢ (𝑦 = 1 → ((seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦) ↔ (seq𝑀( + , 𝐹)‘(𝐺‘1)) = (seq1( + , 𝐻)‘1)))
8	4, 7	imbi12d 347	. . . . 5 ⊢ (𝑦 = 1 → ((𝑦 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦)) ↔ (1 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘1)) = (seq1( + , 𝐻)‘1))))
9	8	imbi2d 343	. . . 4 ⊢ (𝑦 = 1 → ((𝜑 → (𝑦 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦))) ↔ (𝜑 → (1 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘1)) = (seq1( + , 𝐻)‘1)))))
10		eleq1 2900	. . . . . 6 ⊢ (𝑦 = 𝑚 → (𝑦 ∈ (1...(♯‘𝐴)) ↔ 𝑚 ∈ (1...(♯‘𝐴))))
11		2fveq3 6674	. . . . . . 7 ⊢ (𝑦 = 𝑚 → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)))
12		fveq2 6669	. . . . . . 7 ⊢ (𝑦 = 𝑚 → (seq1( + , 𝐻)‘𝑦) = (seq1( + , 𝐻)‘𝑚))
13	11, 12	eqeq12d 2837	. . . . . 6 ⊢ (𝑦 = 𝑚 → ((seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦) ↔ (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq1( + , 𝐻)‘𝑚)))
14	10, 13	imbi12d 347	. . . . 5 ⊢ (𝑦 = 𝑚 → ((𝑦 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦)) ↔ (𝑚 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq1( + , 𝐻)‘𝑚))))
15	14	imbi2d 343	. . . 4 ⊢ (𝑦 = 𝑚 → ((𝜑 → (𝑦 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦))) ↔ (𝜑 → (𝑚 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq1( + , 𝐻)‘𝑚)))))
16		eleq1 2900	. . . . . 6 ⊢ (𝑦 = (𝑚 + 1) → (𝑦 ∈ (1...(♯‘𝐴)) ↔ (𝑚 + 1) ∈ (1...(♯‘𝐴))))
17		2fveq3 6674	. . . . . . 7 ⊢ (𝑦 = (𝑚 + 1) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))))
18		fveq2 6669	. . . . . . 7 ⊢ (𝑦 = (𝑚 + 1) → (seq1( + , 𝐻)‘𝑦) = (seq1( + , 𝐻)‘(𝑚 + 1)))
19	17, 18	eqeq12d 2837	. . . . . 6 ⊢ (𝑦 = (𝑚 + 1) → ((seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦) ↔ (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1))))
20	16, 19	imbi12d 347	. . . . 5 ⊢ (𝑦 = (𝑚 + 1) → ((𝑦 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦)) ↔ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1)))))
21	20	imbi2d 343	. . . 4 ⊢ (𝑦 = (𝑚 + 1) → ((𝜑 → (𝑦 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦))) ↔ (𝜑 → ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1))))))
22		eleq1 2900	. . . . . 6 ⊢ (𝑦 = 𝑁 → (𝑦 ∈ (1...(♯‘𝐴)) ↔ 𝑁 ∈ (1...(♯‘𝐴))))
23		2fveq3 6674	. . . . . . 7 ⊢ (𝑦 = 𝑁 → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq𝑀( + , 𝐹)‘(𝐺‘𝑁)))
24		fveq2 6669	. . . . . . 7 ⊢ (𝑦 = 𝑁 → (seq1( + , 𝐻)‘𝑦) = (seq1( + , 𝐻)‘𝑁))
25	23, 24	eqeq12d 2837	. . . . . 6 ⊢ (𝑦 = 𝑁 → ((seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦) ↔ (seq𝑀( + , 𝐹)‘(𝐺‘𝑁)) = (seq1( + , 𝐻)‘𝑁)))
26	22, 25	imbi12d 347	. . . . 5 ⊢ (𝑦 = 𝑁 → ((𝑦 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦)) ↔ (𝑁 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑁)) = (seq1( + , 𝐻)‘𝑁))))
27	26	imbi2d 343	. . . 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 7075	. . . . . . . . . . . . 13 ⊢ (𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴) → 𝐺:(1...(♯‘𝐴))–1-1-onto→𝐴)
33	31, 32	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺:(1...(♯‘𝐴))–1-1-onto→𝐴)
34		f1of 6614	. . . . . . . . . . . 12 ⊢ (𝐺:(1...(♯‘𝐴))–1-1-onto→𝐴 → 𝐺:(1...(♯‘𝐴))⟶𝐴)
35	33, 34	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺:(1...(♯‘𝐴))⟶𝐴)
36		elfzuz2 12911	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (1...(♯‘𝐴)) → (♯‘𝐴) ∈ (ℤ_≥‘1))
37	1, 36	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘𝐴) ∈ (ℤ_≥‘1))
38		eluzfz1 12913	. . . . . . . . . . . 12 ⊢ ((♯‘𝐴) ∈ (ℤ_≥‘1) → 1 ∈ (1...(♯‘𝐴)))
39	37, 38	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ (1...(♯‘𝐴)))
40	35, 39	ffvelrnd 6851	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺‘1) ∈ 𝐴)
41	30, 40	sseldd 3967	. . . . . . . . 9 ⊢ (𝜑 → (𝐺‘1) ∈ (ℤ_≥‘𝑀))
42		eluzle 12255	. . . . . . . . . . . . 13 ⊢ ((♯‘𝐴) ∈ (ℤ_≥‘1) → 1 ≤ (♯‘𝐴))
43	37, 42	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ≤ (♯‘𝐴))
44		fzssz 12908	. . . . . . . . . . . . . . . 16 ⊢ (1...(♯‘𝐴)) ⊆ ℤ
45		zssre 11987	. . . . . . . . . . . . . . . 16 ⊢ ℤ ⊆ ℝ
46	44, 45	sstri 3975	. . . . . . . . . . . . . . 15 ⊢ (1...(♯‘𝐴)) ⊆ ℝ
47	46	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1...(♯‘𝐴)) ⊆ ℝ)
48		ressxr 10684	. . . . . . . . . . . . . 14 ⊢ ℝ ⊆ ℝ^*
49	47, 48	sstrdi 3978	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1...(♯‘𝐴)) ⊆ ℝ^*)
50		eluzelre 12253	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ (ℤ_≥‘𝑀) → 𝑘 ∈ ℝ)
51	50	ssriv 3970	. . . . . . . . . . . . . . 15 ⊢ (ℤ_≥‘𝑀) ⊆ ℝ
52	30, 51	sstrdi 3978	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ⊆ ℝ)
53	52, 48	sstrdi 3978	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ⊆ ℝ^*)
54		eluzfz2 12914	. . . . . . . . . . . . . 14 ⊢ ((♯‘𝐴) ∈ (ℤ_≥‘1) → (♯‘𝐴) ∈ (1...(♯‘𝐴)))
55	37, 54	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (♯‘𝐴) ∈ (1...(♯‘𝐴)))
56		leisorel 13817	. . . . . . . . . . . . 13 ⊢ ((𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴) ∧ ((1...(♯‘𝐴)) ⊆ ℝ^* ∧ 𝐴 ⊆ ℝ^*) ∧ (1 ∈ (1...(♯‘𝐴)) ∧ (♯‘𝐴) ∈ (1...(♯‘𝐴)))) → (1 ≤ (♯‘𝐴) ↔ (𝐺‘1) ≤ (𝐺‘(♯‘𝐴))))
57	31, 49, 53, 39, 55, 56	syl122anc 1375	. . . . . . . . . . . 12 ⊢ (𝜑 → (1 ≤ (♯‘𝐴) ↔ (𝐺‘1) ≤ (𝐺‘(♯‘𝐴))))
58	43, 57	mpbid 234	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐺‘1) ≤ (𝐺‘(♯‘𝐴)))
59	35, 55	ffvelrnd 6851	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐺‘(♯‘𝐴)) ∈ 𝐴)
60	30, 59	sseldd 3967	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐺‘(♯‘𝐴)) ∈ (ℤ_≥‘𝑀))
61		eluzelz 12252	. . . . . . . . . . . . 13 ⊢ ((𝐺‘(♯‘𝐴)) ∈ (ℤ_≥‘𝑀) → (𝐺‘(♯‘𝐴)) ∈ ℤ)
62	60, 61	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐺‘(♯‘𝐴)) ∈ ℤ)
63		elfz5 12899	. . . . . . . . . . . 12 ⊢ (((𝐺‘1) ∈ (ℤ_≥‘𝑀) ∧ (𝐺‘(♯‘𝐴)) ∈ ℤ) → ((𝐺‘1) ∈ (𝑀...(𝐺‘(♯‘𝐴))) ↔ (𝐺‘1) ≤ (𝐺‘(♯‘𝐴))))
64	41, 62, 63	syl2anc 586	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐺‘1) ∈ (𝑀...(𝐺‘(♯‘𝐴))) ↔ (𝐺‘1) ≤ (𝐺‘(♯‘𝐴))))
65	58, 64	mpbird 259	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺‘1) ∈ (𝑀...(𝐺‘(♯‘𝐴))))
66		fveq2 6669	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝐺‘1) → (𝐹‘𝑘) = (𝐹‘(𝐺‘1)))
67	66	eleq1d 2897	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝐺‘1) → ((𝐹‘𝑘) ∈ 𝑆 ↔ (𝐹‘(𝐺‘1)) ∈ 𝑆))
68	67	imbi2d 343	. . . . . . . . . . 11 ⊢ (𝑘 = (𝐺‘1) → ((𝜑 → (𝐹‘𝑘) ∈ 𝑆) ↔ (𝜑 → (𝐹‘(𝐺‘1)) ∈ 𝑆)))
69		seqcoll.5	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝐺‘(♯‘𝐴)))) → (𝐹‘𝑘) ∈ 𝑆)
70	69	expcom 416	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (𝑀...(𝐺‘(♯‘𝐴))) → (𝜑 → (𝐹‘𝑘) ∈ 𝑆))
71	68, 70	vtoclga 3573	. . . . . . . . . 10 ⊢ ((𝐺‘1) ∈ (𝑀...(𝐺‘(♯‘𝐴))) → (𝜑 → (𝐹‘(𝐺‘1)) ∈ 𝑆))
72	65, 71	mpcom 38	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘(𝐺‘1)) ∈ 𝑆)
73		eluzelz 12252	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺‘1) ∈ (ℤ_≥‘𝑀) → (𝐺‘1) ∈ ℤ)
74	41, 73	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐺‘1) ∈ ℤ)
75		peano2zm 12024	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺‘1) ∈ ℤ → ((𝐺‘1) − 1) ∈ ℤ)
76	74, 75	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐺‘1) − 1) ∈ ℤ)
77	76	zred 12086	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐺‘1) − 1) ∈ ℝ)
78	74	zred 12086	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐺‘1) ∈ ℝ)
79	62	zred 12086	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐺‘(♯‘𝐴)) ∈ ℝ)
80	78	lem1d 11572	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐺‘1) − 1) ≤ (𝐺‘1))
81	77, 78, 79, 80, 58	letrd 10796	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐺‘1) − 1) ≤ (𝐺‘(♯‘𝐴)))
82		eluz 12256	. . . . . . . . . . . . . . 15 ⊢ ((((𝐺‘1) − 1) ∈ ℤ ∧ (𝐺‘(♯‘𝐴)) ∈ ℤ) → ((𝐺‘(♯‘𝐴)) ∈ (ℤ_≥‘((𝐺‘1) − 1)) ↔ ((𝐺‘1) − 1) ≤ (𝐺‘(♯‘𝐴))))
83	76, 62, 82	syl2anc 586	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐺‘(♯‘𝐴)) ∈ (ℤ_≥‘((𝐺‘1) − 1)) ↔ ((𝐺‘1) − 1) ≤ (𝐺‘(♯‘𝐴))))
84	81, 83	mpbird 259	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐺‘(♯‘𝐴)) ∈ (ℤ_≥‘((𝐺‘1) − 1)))
85		fzss2 12946	. . . . . . . . . . . . 13 ⊢ ((𝐺‘(♯‘𝐴)) ∈ (ℤ_≥‘((𝐺‘1) − 1)) → (𝑀...((𝐺‘1) − 1)) ⊆ (𝑀...(𝐺‘(♯‘𝐴))))
86	84, 85	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑀...((𝐺‘1) − 1)) ⊆ (𝑀...(𝐺‘(♯‘𝐴))))
87	86	sselda 3966	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...((𝐺‘1) − 1))) → 𝑘 ∈ (𝑀...(𝐺‘(♯‘𝐴))))
88		eluzel2 12247	. . . . . . . . . . . . . . 15 ⊢ ((𝐺‘1) ∈ (ℤ_≥‘𝑀) → 𝑀 ∈ ℤ)
89	41, 88	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ∈ ℤ)
90		elfzm11 12977	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℤ ∧ (𝐺‘1) ∈ ℤ) → (𝑘 ∈ (𝑀...((𝐺‘1) − 1)) ↔ (𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 < (𝐺‘1))))
91	89, 74, 90	syl2anc 586	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑘 ∈ (𝑀...((𝐺‘1) − 1)) ↔ (𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 < (𝐺‘1))))
92		simp3 1134	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 < (𝐺‘1)) → 𝑘 < (𝐺‘1))
93	78	adantr 483	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐺‘1) ∈ ℝ)
94	52	sselda 3966	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑘 ∈ ℝ)
95		f1ocnv 6626	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐺:(1...(♯‘𝐴))–1-1-onto→𝐴 → ^◡𝐺:𝐴–1-1-onto→(1...(♯‘𝐴)))
96	33, 95	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ^◡𝐺:𝐴–1-1-onto→(1...(♯‘𝐴)))
97		f1of 6614	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (^◡𝐺:𝐴–1-1-onto→(1...(♯‘𝐴)) → ^◡𝐺:𝐴⟶(1...(♯‘𝐴)))
98	96, 97	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ^◡𝐺:𝐴⟶(1...(♯‘𝐴)))
99	98	ffvelrnda 6850	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (^◡𝐺‘𝑘) ∈ (1...(♯‘𝐴)))
100		elfznn 12935	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((^◡𝐺‘𝑘) ∈ (1...(♯‘𝐴)) → (^◡𝐺‘𝑘) ∈ ℕ)
101	99, 100	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (^◡𝐺‘𝑘) ∈ ℕ)
102	101	nnge1d 11684	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 1 ≤ (^◡𝐺‘𝑘))
103	31	adantr 483	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴))
104	49	adantr 483	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (1...(♯‘𝐴)) ⊆ ℝ^*)
105	53	adantr 483	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐴 ⊆ ℝ^*)
106	39	adantr 483	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 1 ∈ (1...(♯‘𝐴)))
107		leisorel 13817	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴) ∧ ((1...(♯‘𝐴)) ⊆ ℝ^* ∧ 𝐴 ⊆ ℝ^*) ∧ (1 ∈ (1...(♯‘𝐴)) ∧ (^◡𝐺‘𝑘) ∈ (1...(♯‘𝐴)))) → (1 ≤ (^◡𝐺‘𝑘) ↔ (𝐺‘1) ≤ (𝐺‘(^◡𝐺‘𝑘))))
108	103, 104, 105, 106, 99, 107	syl122anc 1375	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (1 ≤ (^◡𝐺‘𝑘) ↔ (𝐺‘1) ≤ (𝐺‘(^◡𝐺‘𝑘))))
109	102, 108	mpbid 234	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐺‘1) ≤ (𝐺‘(^◡𝐺‘𝑘)))
110		f1ocnvfv2 7033	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺:(1...(♯‘𝐴))–1-1-onto→𝐴 ∧ 𝑘 ∈ 𝐴) → (𝐺‘(^◡𝐺‘𝑘)) = 𝑘)
111	33, 110	sylan 582	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐺‘(^◡𝐺‘𝑘)) = 𝑘)
112	109, 111	breqtrd 5091	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐺‘1) ≤ 𝑘)
113	93, 94, 112	lensymd 10790	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ¬ 𝑘 < (𝐺‘1))
114	113	ex 415	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑘 ∈ 𝐴 → ¬ 𝑘 < (𝐺‘1)))
115	114	con2d 136	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑘 < (𝐺‘1) → ¬ 𝑘 ∈ 𝐴))
116	92, 115	syl5 34	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 < (𝐺‘1)) → ¬ 𝑘 ∈ 𝐴))
117	91, 116	sylbid 242	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑘 ∈ (𝑀...((𝐺‘1) − 1)) → ¬ 𝑘 ∈ 𝐴))
118	117	imp 409	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...((𝐺‘1) − 1))) → ¬ 𝑘 ∈ 𝐴)
119	87, 118	eldifd 3946	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...((𝐺‘1) − 1))) → 𝑘 ∈ ((𝑀...(𝐺‘(♯‘𝐴))) ∖ 𝐴))
120		seqcoll.6	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀...(𝐺‘(♯‘𝐴))) ∖ 𝐴)) → (𝐹‘𝑘) = 𝑍)
121	119, 120	syldan 593	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...((𝐺‘1) − 1))) → (𝐹‘𝑘) = 𝑍)
122	28, 29, 41, 72, 121	seqid 13414	. . . . . . . 8 ⊢ (𝜑 → (seq𝑀( + , 𝐹) ↾ (ℤ_≥‘(𝐺‘1))) = seq(𝐺‘1)( + , 𝐹))
123	122	fveq1d 6671	. . . . . . 7 ⊢ (𝜑 → ((seq𝑀( + , 𝐹) ↾ (ℤ_≥‘(𝐺‘1)))‘(𝐺‘1)) = (seq(𝐺‘1)( + , 𝐹)‘(𝐺‘1)))
124		uzid 12257	. . . . . . . . 9 ⊢ ((𝐺‘1) ∈ ℤ → (𝐺‘1) ∈ (ℤ_≥‘(𝐺‘1)))
125	74, 124	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝐺‘1) ∈ (ℤ_≥‘(𝐺‘1)))
126	125	fvresd 6689	. . . . . . 7 ⊢ (𝜑 → ((seq𝑀( + , 𝐹) ↾ (ℤ_≥‘(𝐺‘1)))‘(𝐺‘1)) = (seq𝑀( + , 𝐹)‘(𝐺‘1)))
127		seq1 13381	. . . . . . . . 9 ⊢ ((𝐺‘1) ∈ ℤ → (seq(𝐺‘1)( + , 𝐹)‘(𝐺‘1)) = (𝐹‘(𝐺‘1)))
128	74, 127	syl 17	. . . . . . . 8 ⊢ (𝜑 → (seq(𝐺‘1)( + , 𝐹)‘(𝐺‘1)) = (𝐹‘(𝐺‘1)))
129		fveq2 6669	. . . . . . . . . . . 12 ⊢ (𝑛 = 1 → (𝐻‘𝑛) = (𝐻‘1))
130		2fveq3 6674	. . . . . . . . . . . 12 ⊢ (𝑛 = 1 → (𝐹‘(𝐺‘𝑛)) = (𝐹‘(𝐺‘1)))
131	129, 130	eqeq12d 2837	. . . . . . . . . . 11 ⊢ (𝑛 = 1 → ((𝐻‘𝑛) = (𝐹‘(𝐺‘𝑛)) ↔ (𝐻‘1) = (𝐹‘(𝐺‘1))))
132	131	imbi2d 343	. . . . . . . . . 10 ⊢ (𝑛 = 1 → ((𝜑 → (𝐻‘𝑛) = (𝐹‘(𝐺‘𝑛))) ↔ (𝜑 → (𝐻‘1) = (𝐹‘(𝐺‘1)))))
133		seqcoll.7	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (𝐻‘𝑛) = (𝐹‘(𝐺‘𝑛)))
134	133	expcom 416	. . . . . . . . . 10 ⊢ (𝑛 ∈ (1...(♯‘𝐴)) → (𝜑 → (𝐻‘𝑛) = (𝐹‘(𝐺‘𝑛))))
135	132, 134	vtoclga 3573	. . . . . . . . 9 ⊢ (1 ∈ (1...(♯‘𝐴)) → (𝜑 → (𝐻‘1) = (𝐹‘(𝐺‘1))))
136	39, 135	mpcom 38	. . . . . . . 8 ⊢ (𝜑 → (𝐻‘1) = (𝐹‘(𝐺‘1)))
137	128, 136	eqtr4d 2859	. . . . . . 7 ⊢ (𝜑 → (seq(𝐺‘1)( + , 𝐹)‘(𝐺‘1)) = (𝐻‘1))
138	123, 126, 137	3eqtr3d 2864	. . . . . 6 ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘(𝐺‘1)) = (𝐻‘1))
139		1z 12011	. . . . . . 7 ⊢ 1 ∈ ℤ
140		seq1 13381	. . . . . . 7 ⊢ (1 ∈ ℤ → (seq1( + , 𝐻)‘1) = (𝐻‘1))
141	139, 140	ax-mp 5	. . . . . 6 ⊢ (seq1( + , 𝐻)‘1) = (𝐻‘1)
142	138, 141	syl6eqr 2874	. . . . 5 ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘(𝐺‘1)) = (seq1( + , 𝐻)‘1))
143	142	a1d 25	. . . 4 ⊢ (𝜑 → (1 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘1)) = (seq1( + , 𝐻)‘1)))
144		simplr 767	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝑚 ∈ ℕ)
145		nnuz 12280	. . . . . . . . . . 11 ⊢ ℕ = (ℤ_≥‘1)
146	144, 145	eleqtrdi 2923	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝑚 ∈ (ℤ_≥‘1))
147		nnz 12003	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℤ)
148	147	ad2antlr 725	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝑚 ∈ ℤ)
149		elfzuz3 12904	. . . . . . . . . . . 12 ⊢ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (♯‘𝐴) ∈ (ℤ_≥‘(𝑚 + 1)))
150	149	adantl 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (♯‘𝐴) ∈ (ℤ_≥‘(𝑚 + 1)))
151		peano2uzr 12302	. . . . . . . . . . 11 ⊢ ((𝑚 ∈ ℤ ∧ (♯‘𝐴) ∈ (ℤ_≥‘(𝑚 + 1))) → (♯‘𝐴) ∈ (ℤ_≥‘𝑚))
152	148, 150, 151	syl2anc 586	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (♯‘𝐴) ∈ (ℤ_≥‘𝑚))
153		elfzuzb 12901	. . . . . . . . . 10 ⊢ (𝑚 ∈ (1...(♯‘𝐴)) ↔ (𝑚 ∈ (ℤ_≥‘1) ∧ (♯‘𝐴) ∈ (ℤ_≥‘𝑚)))
154	146, 152, 153	sylanbrc 585	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝑚 ∈ (1...(♯‘𝐴)))
155	154	ex 415	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → 𝑚 ∈ (1...(♯‘𝐴))))
156	155	imim1d 82	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑚 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq1( + , 𝐻)‘𝑚)) → ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq1( + , 𝐻)‘𝑚))))
157		oveq1 7162	. . . . . . . . . 10 ⊢ ((seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq1( + , 𝐻)‘𝑚) → ((seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) + (𝐻‘(𝑚 + 1))) = ((seq1( + , 𝐻)‘𝑚) + (𝐻‘(𝑚 + 1))))
158		seqcoll.1b	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑆) → (𝑘 + 𝑍) = 𝑘)
159	158	ad4ant14 750	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ 𝑆) → (𝑘 + 𝑍) = 𝑘)
160	30	ad2antrr 724	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝐴 ⊆ (ℤ_≥‘𝑀))
161	35	ad2antrr 724	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝐺:(1...(♯‘𝐴))⟶𝐴)
162	161, 154	ffvelrnd 6851	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘𝑚) ∈ 𝐴)
163	160, 162	sseldd 3967	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘𝑚) ∈ (ℤ_≥‘𝑀))
164		nnre 11644	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℝ)
165	164	ad2antlr 725	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝑚 ∈ ℝ)
166	165	ltp1d 11569	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝑚 < (𝑚 + 1))
167	31	ad2antrr 724	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴))
168		simpr 487	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝑚 + 1) ∈ (1...(♯‘𝐴)))
169		isorel 7078	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴) ∧ (𝑚 ∈ (1...(♯‘𝐴)) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴)))) → (𝑚 < (𝑚 + 1) ↔ (𝐺‘𝑚) < (𝐺‘(𝑚 + 1))))
170	167, 154, 168, 169	syl12anc 834	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝑚 < (𝑚 + 1) ↔ (𝐺‘𝑚) < (𝐺‘(𝑚 + 1))))
171	166, 170	mpbid 234	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘𝑚) < (𝐺‘(𝑚 + 1)))
172		eluzelz 12252	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺‘𝑚) ∈ (ℤ_≥‘𝑀) → (𝐺‘𝑚) ∈ ℤ)
173	163, 172	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘𝑚) ∈ ℤ)
174	161, 168	ffvelrnd 6851	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(𝑚 + 1)) ∈ 𝐴)
175	160, 174	sseldd 3967	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(𝑚 + 1)) ∈ (ℤ_≥‘𝑀))
176		eluzelz 12252	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺‘(𝑚 + 1)) ∈ (ℤ_≥‘𝑀) → (𝐺‘(𝑚 + 1)) ∈ ℤ)
177	175, 176	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(𝑚 + 1)) ∈ ℤ)
178		zltlem1 12034	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐺‘𝑚) ∈ ℤ ∧ (𝐺‘(𝑚 + 1)) ∈ ℤ) → ((𝐺‘𝑚) < (𝐺‘(𝑚 + 1)) ↔ (𝐺‘𝑚) ≤ ((𝐺‘(𝑚 + 1)) − 1)))
179	173, 177, 178	syl2anc 586	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝐺‘𝑚) < (𝐺‘(𝑚 + 1)) ↔ (𝐺‘𝑚) ≤ ((𝐺‘(𝑚 + 1)) − 1)))
180	171, 179	mpbid 234	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘𝑚) ≤ ((𝐺‘(𝑚 + 1)) − 1))
181		peano2zm 12024	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺‘(𝑚 + 1)) ∈ ℤ → ((𝐺‘(𝑚 + 1)) − 1) ∈ ℤ)
182	177, 181	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝐺‘(𝑚 + 1)) − 1) ∈ ℤ)
183		eluz 12256	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺‘𝑚) ∈ ℤ ∧ ((𝐺‘(𝑚 + 1)) − 1) ∈ ℤ) → (((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ_≥‘(𝐺‘𝑚)) ↔ (𝐺‘𝑚) ≤ ((𝐺‘(𝑚 + 1)) − 1)))
184	173, 182, 183	syl2anc 586	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ_≥‘(𝐺‘𝑚)) ↔ (𝐺‘𝑚) ≤ ((𝐺‘(𝑚 + 1)) − 1)))
185	180, 184	mpbird 259	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ_≥‘(𝐺‘𝑚)))
186	182	zred 12086	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝐺‘(𝑚 + 1)) − 1) ∈ ℝ)
187	177	zred 12086	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(𝑚 + 1)) ∈ ℝ)
188	79	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(♯‘𝐴)) ∈ ℝ)
189	187	lem1d 11572	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝐺‘(𝑚 + 1)) − 1) ≤ (𝐺‘(𝑚 + 1)))
190		elfzle2 12910	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (𝑚 + 1) ≤ (♯‘𝐴))
191	190	adantl 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝑚 + 1) ≤ (♯‘𝐴))
192	49	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (1...(♯‘𝐴)) ⊆ ℝ^*)
193	53	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝐴 ⊆ ℝ^*)
194	55	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (♯‘𝐴) ∈ (1...(♯‘𝐴)))
195		leisorel 13817	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴) ∧ ((1...(♯‘𝐴)) ⊆ ℝ^* ∧ 𝐴 ⊆ ℝ^*) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ (♯‘𝐴) ∈ (1...(♯‘𝐴)))) → ((𝑚 + 1) ≤ (♯‘𝐴) ↔ (𝐺‘(𝑚 + 1)) ≤ (𝐺‘(♯‘𝐴))))
196	167, 192, 193, 168, 194, 195	syl122anc 1375	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝑚 + 1) ≤ (♯‘𝐴) ↔ (𝐺‘(𝑚 + 1)) ≤ (𝐺‘(♯‘𝐴))))
197	191, 196	mpbid 234	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(𝑚 + 1)) ≤ (𝐺‘(♯‘𝐴)))
198	186, 187, 188, 189, 197	letrd 10796	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝐺‘(𝑚 + 1)) − 1) ≤ (𝐺‘(♯‘𝐴)))
199	62	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(♯‘𝐴)) ∈ ℤ)
200		eluz 12256	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐺‘(𝑚 + 1)) − 1) ∈ ℤ ∧ (𝐺‘(♯‘𝐴)) ∈ ℤ) → ((𝐺‘(♯‘𝐴)) ∈ (ℤ_≥‘((𝐺‘(𝑚 + 1)) − 1)) ↔ ((𝐺‘(𝑚 + 1)) − 1) ≤ (𝐺‘(♯‘𝐴))))
201	182, 199, 200	syl2anc 586	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝐺‘(♯‘𝐴)) ∈ (ℤ_≥‘((𝐺‘(𝑚 + 1)) − 1)) ↔ ((𝐺‘(𝑚 + 1)) − 1) ≤ (𝐺‘(♯‘𝐴))))
202	198, 201	mpbird 259	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(♯‘𝐴)) ∈ (ℤ_≥‘((𝐺‘(𝑚 + 1)) − 1)))
203		uztrn 12260	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐺‘(♯‘𝐴)) ∈ (ℤ_≥‘((𝐺‘(𝑚 + 1)) − 1)) ∧ ((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ_≥‘(𝐺‘𝑚))) → (𝐺‘(♯‘𝐴)) ∈ (ℤ_≥‘(𝐺‘𝑚)))
204	202, 185, 203	syl2anc 586	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(♯‘𝐴)) ∈ (ℤ_≥‘(𝐺‘𝑚)))
205		fzss2 12946	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺‘(♯‘𝐴)) ∈ (ℤ_≥‘(𝐺‘𝑚)) → (𝑀...(𝐺‘𝑚)) ⊆ (𝑀...(𝐺‘(♯‘𝐴))))
206	204, 205	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝑀...(𝐺‘𝑚)) ⊆ (𝑀...(𝐺‘(♯‘𝐴))))
207	206	sselda 3966	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (𝑀...(𝐺‘𝑚))) → 𝑘 ∈ (𝑀...(𝐺‘(♯‘𝐴))))
208	69	ad4ant14 750	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (𝑀...(𝐺‘(♯‘𝐴)))) → (𝐹‘𝑘) ∈ 𝑆)
209	207, 208	syldan 593	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (𝑀...(𝐺‘𝑚))) → (𝐹‘𝑘) ∈ 𝑆)
210		seqcoll.c	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑘 ∈ 𝑆 ∧ 𝑛 ∈ 𝑆)) → (𝑘 + 𝑛) ∈ 𝑆)
211	210	ad4ant14 750	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ (𝑘 ∈ 𝑆 ∧ 𝑛 ∈ 𝑆)) → (𝑘 + 𝑛) ∈ 𝑆)
212	163, 209, 211	seqcl 13389	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) ∈ 𝑆)
213		simplll 773	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1))) → 𝜑)
214		elfzuz 12903	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1)) → 𝑘 ∈ (ℤ_≥‘((𝐺‘𝑚) + 1)))
215		peano2uz 12300	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺‘𝑚) ∈ (ℤ_≥‘𝑀) → ((𝐺‘𝑚) + 1) ∈ (ℤ_≥‘𝑀))
216	163, 215	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝐺‘𝑚) + 1) ∈ (ℤ_≥‘𝑀))
217		uztrn 12260	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ (ℤ_≥‘((𝐺‘𝑚) + 1)) ∧ ((𝐺‘𝑚) + 1) ∈ (ℤ_≥‘𝑀)) → 𝑘 ∈ (ℤ_≥‘𝑀))
218	214, 216, 217	syl2anr 598	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1))) → 𝑘 ∈ (ℤ_≥‘𝑀))
219		elfzuz3 12904	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1)) → ((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ_≥‘𝑘))
220		uztrn 12260	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐺‘(♯‘𝐴)) ∈ (ℤ_≥‘((𝐺‘(𝑚 + 1)) − 1)) ∧ ((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ_≥‘𝑘)) → (𝐺‘(♯‘𝐴)) ∈ (ℤ_≥‘𝑘))
221	202, 219, 220	syl2an 597	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1))) → (𝐺‘(♯‘𝐴)) ∈ (ℤ_≥‘𝑘))
222		elfzuzb 12901	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (𝑀...(𝐺‘(♯‘𝐴))) ↔ (𝑘 ∈ (ℤ_≥‘𝑀) ∧ (𝐺‘(♯‘𝐴)) ∈ (ℤ_≥‘𝑘)))
223	218, 221, 222	sylanbrc 585	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1))) → 𝑘 ∈ (𝑀...(𝐺‘(♯‘𝐴))))
224	147	ad2antlr 725	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → 𝑚 ∈ ℤ)
225	98	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → ^◡𝐺:𝐴⟶(1...(♯‘𝐴)))
226		simprr 771	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → 𝑘 ∈ 𝐴)
227	225, 226	ffvelrnd 6851	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → (^◡𝐺‘𝑘) ∈ (1...(♯‘𝐴)))
228		elfzelz 12907	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((^◡𝐺‘𝑘) ∈ (1...(♯‘𝐴)) → (^◡𝐺‘𝑘) ∈ ℤ)
229	227, 228	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → (^◡𝐺‘𝑘) ∈ ℤ)
230		btwnnz 12057	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑚 ∈ ℤ ∧ 𝑚 < (^◡𝐺‘𝑘) ∧ (^◡𝐺‘𝑘) < (𝑚 + 1)) → ¬ (^◡𝐺‘𝑘) ∈ ℤ)
231	230	3expib 1118	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 ∈ ℤ → ((𝑚 < (^◡𝐺‘𝑘) ∧ (^◡𝐺‘𝑘) < (𝑚 + 1)) → ¬ (^◡𝐺‘𝑘) ∈ ℤ))
232	231	con2d 136	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 ∈ ℤ → ((^◡𝐺‘𝑘) ∈ ℤ → ¬ (𝑚 < (^◡𝐺‘𝑘) ∧ (^◡𝐺‘𝑘) < (𝑚 + 1))))
233	224, 229, 232	sylc 65	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → ¬ (𝑚 < (^◡𝐺‘𝑘) ∧ (^◡𝐺‘𝑘) < (𝑚 + 1)))
234	31	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → 𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴))
235	154	adantrr 715	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → 𝑚 ∈ (1...(♯‘𝐴)))
236		isorel 7078	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴) ∧ (𝑚 ∈ (1...(♯‘𝐴)) ∧ (^◡𝐺‘𝑘) ∈ (1...(♯‘𝐴)))) → (𝑚 < (^◡𝐺‘𝑘) ↔ (𝐺‘𝑚) < (𝐺‘(^◡𝐺‘𝑘))))
237	234, 235, 227, 236	syl12anc 834	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → (𝑚 < (^◡𝐺‘𝑘) ↔ (𝐺‘𝑚) < (𝐺‘(^◡𝐺‘𝑘))))
238	33	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → 𝐺:(1...(♯‘𝐴))–1-1-onto→𝐴)
239	238, 226, 110	syl2anc 586	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → (𝐺‘(^◡𝐺‘𝑘)) = 𝑘)
240	239	breq2d 5077	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → ((𝐺‘𝑚) < (𝐺‘(^◡𝐺‘𝑘)) ↔ (𝐺‘𝑚) < 𝑘))
241	173	adantrr 715	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → (𝐺‘𝑚) ∈ ℤ)
242	30	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → 𝐴 ⊆ (ℤ_≥‘𝑀))
243	242, 226	sseldd 3967	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → 𝑘 ∈ (ℤ_≥‘𝑀))
244		eluzelz 12252	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 ∈ (ℤ_≥‘𝑀) → 𝑘 ∈ ℤ)
245	243, 244	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → 𝑘 ∈ ℤ)
246		zltp1le 12031	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐺‘𝑚) ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((𝐺‘𝑚) < 𝑘 ↔ ((𝐺‘𝑚) + 1) ≤ 𝑘))
247	241, 245, 246	syl2anc 586	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → ((𝐺‘𝑚) < 𝑘 ↔ ((𝐺‘𝑚) + 1) ≤ 𝑘))
248	237, 240, 247	3bitrd 307	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → (𝑚 < (^◡𝐺‘𝑘) ↔ ((𝐺‘𝑚) + 1) ≤ 𝑘))
249	168	adantrr 715	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → (𝑚 + 1) ∈ (1...(♯‘𝐴)))
250		isorel 7078	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴) ∧ ((^◡𝐺‘𝑘) ∈ (1...(♯‘𝐴)) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴)))) → ((^◡𝐺‘𝑘) < (𝑚 + 1) ↔ (𝐺‘(^◡𝐺‘𝑘)) < (𝐺‘(𝑚 + 1))))
251	234, 227, 249, 250	syl12anc 834	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → ((^◡𝐺‘𝑘) < (𝑚 + 1) ↔ (𝐺‘(^◡𝐺‘𝑘)) < (𝐺‘(𝑚 + 1))))
252	239	breq1d 5075	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → ((𝐺‘(^◡𝐺‘𝑘)) < (𝐺‘(𝑚 + 1)) ↔ 𝑘 < (𝐺‘(𝑚 + 1))))
253	177	adantrr 715	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → (𝐺‘(𝑚 + 1)) ∈ ℤ)
254		zltlem1 12034	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 ∈ ℤ ∧ (𝐺‘(𝑚 + 1)) ∈ ℤ) → (𝑘 < (𝐺‘(𝑚 + 1)) ↔ 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1)))
255	245, 253, 254	syl2anc 586	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → (𝑘 < (𝐺‘(𝑚 + 1)) ↔ 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1)))
256	251, 252, 255	3bitrd 307	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → ((^◡𝐺‘𝑘) < (𝑚 + 1) ↔ 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1)))
257	248, 256	anbi12d 632	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → ((𝑚 < (^◡𝐺‘𝑘) ∧ (^◡𝐺‘𝑘) < (𝑚 + 1)) ↔ (((𝐺‘𝑚) + 1) ≤ 𝑘 ∧ 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1))))
258	233, 257	mtbid 326	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → ¬ (((𝐺‘𝑚) + 1) ≤ 𝑘 ∧ 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1)))
259	258	expr 459	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝑘 ∈ 𝐴 → ¬ (((𝐺‘𝑚) + 1) ≤ 𝑘 ∧ 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1))))
260	259	con2d 136	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((((𝐺‘𝑚) + 1) ≤ 𝑘 ∧ 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1)) → ¬ 𝑘 ∈ 𝐴))
261		elfzle1 12909	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1)) → ((𝐺‘𝑚) + 1) ≤ 𝑘)
262		elfzle2 12910	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1)) → 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1))
263	261, 262	jca 514	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1)) → (((𝐺‘𝑚) + 1) ≤ 𝑘 ∧ 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1)))
264	260, 263	impel 508	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1))) → ¬ 𝑘 ∈ 𝐴)
265	223, 264	eldifd 3946	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1))) → 𝑘 ∈ ((𝑀...(𝐺‘(♯‘𝐴))) ∖ 𝐴))
266	213, 265, 120	syl2anc 586	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1))) → (𝐹‘𝑘) = 𝑍)
267	159, 163, 185, 212, 266	seqid2 13415	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq𝑀( + , 𝐹)‘((𝐺‘(𝑚 + 1)) − 1)))
268	267	oveq1d 7170	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) + (𝐹‘(𝐺‘(𝑚 + 1)))) = ((seq𝑀( + , 𝐹)‘((𝐺‘(𝑚 + 1)) − 1)) + (𝐹‘(𝐺‘(𝑚 + 1)))))
269		fveq2 6669	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = (𝑚 + 1) → (𝐻‘𝑛) = (𝐻‘(𝑚 + 1)))
270		2fveq3 6674	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = (𝑚 + 1) → (𝐹‘(𝐺‘𝑛)) = (𝐹‘(𝐺‘(𝑚 + 1))))
271	269, 270	eqeq12d 2837	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = (𝑚 + 1) → ((𝐻‘𝑛) = (𝐹‘(𝐺‘𝑛)) ↔ (𝐻‘(𝑚 + 1)) = (𝐹‘(𝐺‘(𝑚 + 1)))))
272	271	imbi2d 343	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = (𝑚 + 1) → ((𝜑 → (𝐻‘𝑛) = (𝐹‘(𝐺‘𝑛))) ↔ (𝜑 → (𝐻‘(𝑚 + 1)) = (𝐹‘(𝐺‘(𝑚 + 1))))))
273	272, 134	vtoclga 3573	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (𝜑 → (𝐻‘(𝑚 + 1)) = (𝐹‘(𝐺‘(𝑚 + 1)))))
274	273	impcom 410	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐻‘(𝑚 + 1)) = (𝐹‘(𝐺‘(𝑚 + 1))))
275	274	adantlr 713	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐻‘(𝑚 + 1)) = (𝐹‘(𝐺‘(𝑚 + 1))))
276	275	oveq2d 7171	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) + (𝐻‘(𝑚 + 1))) = ((seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) + (𝐹‘(𝐺‘(𝑚 + 1)))))
277	89	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝑀 ∈ ℤ)
278	177	zcnd 12087	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(𝑚 + 1)) ∈ ℂ)
279		ax-1cn 10594	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
280		npcan 10894	. . . . . . . . . . . . . . 15 ⊢ (((𝐺‘(𝑚 + 1)) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝐺‘(𝑚 + 1)) − 1) + 1) = (𝐺‘(𝑚 + 1)))
281	278, 279, 280	sylancl 588	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (((𝐺‘(𝑚 + 1)) − 1) + 1) = (𝐺‘(𝑚 + 1)))
282		uztrn 12260	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ_≥‘(𝐺‘𝑚)) ∧ (𝐺‘𝑚) ∈ (ℤ_≥‘𝑀)) → ((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ_≥‘𝑀))
283	185, 163, 282	syl2anc 586	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ_≥‘𝑀))
284		eluzp1p1 12269	. . . . . . . . . . . . . . 15 ⊢ (((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ_≥‘𝑀) → (((𝐺‘(𝑚 + 1)) − 1) + 1) ∈ (ℤ_≥‘(𝑀 + 1)))
285	283, 284	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (((𝐺‘(𝑚 + 1)) − 1) + 1) ∈ (ℤ_≥‘(𝑀 + 1)))
286	281, 285	eqeltrrd 2914	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(𝑚 + 1)) ∈ (ℤ_≥‘(𝑀 + 1)))
287		seqm1 13386	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℤ ∧ (𝐺‘(𝑚 + 1)) ∈ (ℤ_≥‘(𝑀 + 1))) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = ((seq𝑀( + , 𝐹)‘((𝐺‘(𝑚 + 1)) − 1)) + (𝐹‘(𝐺‘(𝑚 + 1)))))
288	277, 286, 287	syl2anc 586	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = ((seq𝑀( + , 𝐹)‘((𝐺‘(𝑚 + 1)) − 1)) + (𝐹‘(𝐺‘(𝑚 + 1)))))
289	268, 276, 288	3eqtr4rd 2867	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = ((seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) + (𝐻‘(𝑚 + 1))))
290		seqp1 13383	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ (ℤ_≥‘1) → (seq1( + , 𝐻)‘(𝑚 + 1)) = ((seq1( + , 𝐻)‘𝑚) + (𝐻‘(𝑚 + 1))))
291	146, 290	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (seq1( + , 𝐻)‘(𝑚 + 1)) = ((seq1( + , 𝐻)‘𝑚) + (𝐻‘(𝑚 + 1))))
292	289, 291	eqeq12d 2837	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1)) ↔ ((seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) + (𝐻‘(𝑚 + 1))) = ((seq1( + , 𝐻)‘𝑚) + (𝐻‘(𝑚 + 1)))))
293	157, 292	syl5ibr 248	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq1( + , 𝐻)‘𝑚) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1))))
294	293	ex 415	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → ((seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq1( + , 𝐻)‘𝑚) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1)))))
295	294	a2d 29	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq1( + , 𝐻)‘𝑚)) → ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1)))))
296	156, 295	syld 47	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑚 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq1( + , 𝐻)‘𝑚)) → ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1)))))
297	296	expcom 416	. . . . 5 ⊢ (𝑚 ∈ ℕ → (𝜑 → ((𝑚 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq1( + , 𝐻)‘𝑚)) → ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1))))))
298	297	a2d 29	. . . 4 ⊢ (𝑚 ∈ ℕ → ((𝜑 → (𝑚 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq1( + , 𝐻)‘𝑚))) → (𝜑 → ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1))))))
299	9, 15, 21, 27, 143, 298	nnind 11655	. . 3 ⊢ (𝑁 ∈ ℕ → (𝜑 → (𝑁 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑁)) = (seq1( + , 𝐻)‘𝑁))))
300	3, 299	mpcom 38	. 2 ⊢ (𝜑 → (𝑁 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑁)) = (seq1( + , 𝐻)‘𝑁)))
301	1, 300	mpd 15	1 ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘(𝐺‘𝑁)) = (seq1( + , 𝐻)‘𝑁))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 398 ∧ w3a 1083 = wceq 1533 ∈ wcel 2110 ∖ cdif 3932 ⊆ wss 3935 class class class wbr 5065 ^◡ccnv 5553 ↾ cres 5556 ⟶wf 6350 –1-1-onto→wf1o 6353 ‘cfv 6354 Isom wiso 6355 (class class class)co 7155 ℂcc 10534 ℝcr 10535 1c1 10537 + caddc 10539 ℝ^*cxr 10673 < clt 10674 ≤ cle 10675 − cmin 10869 ℕcn 11637 ℤcz 11980 ℤ_≥cuz 12242 ...cfz 12891 seqcseq 13368 ♯chash 13689

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 ax-sep 5202 ax-nul 5209 ax-pow 5265 ax-pr 5329 ax-un 7460 ax-cnex 10592 ax-resscn 10593 ax-1cn 10594 ax-icn 10595 ax-addcl 10596 ax-addrcl 10597 ax-mulcl 10598 ax-mulrcl 10599 ax-mulcom 10600 ax-addass 10601 ax-mulass 10602 ax-distr 10603 ax-i2m1 10604 ax-1ne0 10605 ax-1rid 10606 ax-rnegex 10607 ax-rrecex 10608 ax-cnre 10609 ax-pre-lttri 10610 ax-pre-lttrn 10611 ax-pre-ltadd 10612 ax-pre-mulgt0 10613

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rab 3147 df-v 3496 df-sbc 3772 df-csb 3883 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-pss 3953 df-nul 4291 df-if 4467 df-pw 4540 df-sn 4567 df-pr 4569 df-tp 4571 df-op 4573 df-uni 4838 df-iun 4920 df-br 5066 df-opab 5128 df-mpt 5146 df-tr 5172 df-id 5459 df-eprel 5464 df-po 5473 df-so 5474 df-fr 5513 df-we 5515 df-xp 5560 df-rel 5561 df-cnv 5562 df-co 5563 df-dm 5564 df-rn 5565 df-res 5566 df-ima 5567 df-pred 6147 df-ord 6193 df-on 6194 df-lim 6195 df-suc 6196 df-iota 6313 df-fun 6356 df-fn 6357 df-f 6358 df-f1 6359 df-fo 6360 df-f1o 6361 df-fv 6362 df-isom 6363 df-riota 7113 df-ov 7158 df-oprab 7159 df-mpo 7160 df-om 7580 df-1st 7688 df-2nd 7689 df-wrecs 7946 df-recs 8007 df-rdg 8045 df-er 8288 df-en 8509 df-dom 8510 df-sdom 8511 df-pnf 10676 df-mnf 10677 df-xr 10678 df-ltxr 10679 df-le 10680 df-sub 10871 df-neg 10872 df-nn 11638 df-n0 11897 df-z 11981 df-uz 12243 df-fz 12892 df-seq 13369

This theorem is referenced by: seqcoll2 13822 summolem2a 15071 prodmolem2a 15287

W3C validator