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 13105

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 12241	. . . 4 ⊢ (𝑁 ∈ (1...(#‘𝐴)) → 𝑁 ∈ ℕ)
3	1, 2	syl 17	. . 3 ⊢ (𝜑 → 𝑁 ∈ ℕ)
4		eleq1 2676	. . . . . 6 ⊢ (𝑦 = 1 → (𝑦 ∈ (1...(#‘𝐴)) ↔ 1 ∈ (1...(#‘𝐴))))
5		fveq2 6103	. . . . . . . 8 ⊢ (𝑦 = 1 → (𝐺‘𝑦) = (𝐺‘1))
6	5	fveq2d 6107	. . . . . . 7 ⊢ (𝑦 = 1 → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq𝑀( + , 𝐹)‘(𝐺‘1)))
7		fveq2 6103	. . . . . . 7 ⊢ (𝑦 = 1 → (seq1( + , 𝐻)‘𝑦) = (seq1( + , 𝐻)‘1))
8	6, 7	eqeq12d 2625	. . . . . 6 ⊢ (𝑦 = 1 → ((seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦) ↔ (seq𝑀( + , 𝐹)‘(𝐺‘1)) = (seq1( + , 𝐻)‘1)))
9	4, 8	imbi12d 333	. . . . 5 ⊢ (𝑦 = 1 → ((𝑦 ∈ (1...(#‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦)) ↔ (1 ∈ (1...(#‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘1)) = (seq1( + , 𝐻)‘1))))
10	9	imbi2d 329	. . . 4 ⊢ (𝑦 = 1 → ((𝜑 → (𝑦 ∈ (1...(#‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦))) ↔ (𝜑 → (1 ∈ (1...(#‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘1)) = (seq1( + , 𝐻)‘1)))))
11		eleq1 2676	. . . . . 6 ⊢ (𝑦 = 𝑚 → (𝑦 ∈ (1...(#‘𝐴)) ↔ 𝑚 ∈ (1...(#‘𝐴))))
12		fveq2 6103	. . . . . . . 8 ⊢ (𝑦 = 𝑚 → (𝐺‘𝑦) = (𝐺‘𝑚))
13	12	fveq2d 6107	. . . . . . 7 ⊢ (𝑦 = 𝑚 → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)))
14		fveq2 6103	. . . . . . 7 ⊢ (𝑦 = 𝑚 → (seq1( + , 𝐻)‘𝑦) = (seq1( + , 𝐻)‘𝑚))
15	13, 14	eqeq12d 2625	. . . . . 6 ⊢ (𝑦 = 𝑚 → ((seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦) ↔ (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq1( + , 𝐻)‘𝑚)))
16	11, 15	imbi12d 333	. . . . 5 ⊢ (𝑦 = 𝑚 → ((𝑦 ∈ (1...(#‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦)) ↔ (𝑚 ∈ (1...(#‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq1( + , 𝐻)‘𝑚))))
17	16	imbi2d 329	. . . 4 ⊢ (𝑦 = 𝑚 → ((𝜑 → (𝑦 ∈ (1...(#‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦))) ↔ (𝜑 → (𝑚 ∈ (1...(#‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq1( + , 𝐻)‘𝑚)))))
18		eleq1 2676	. . . . . 6 ⊢ (𝑦 = (𝑚 + 1) → (𝑦 ∈ (1...(#‘𝐴)) ↔ (𝑚 + 1) ∈ (1...(#‘𝐴))))
19		fveq2 6103	. . . . . . . 8 ⊢ (𝑦 = (𝑚 + 1) → (𝐺‘𝑦) = (𝐺‘(𝑚 + 1)))
20	19	fveq2d 6107	. . . . . . 7 ⊢ (𝑦 = (𝑚 + 1) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))))
21		fveq2 6103	. . . . . . 7 ⊢ (𝑦 = (𝑚 + 1) → (seq1( + , 𝐻)‘𝑦) = (seq1( + , 𝐻)‘(𝑚 + 1)))
22	20, 21	eqeq12d 2625	. . . . . 6 ⊢ (𝑦 = (𝑚 + 1) → ((seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦) ↔ (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1))))
23	18, 22	imbi12d 333	. . . . 5 ⊢ (𝑦 = (𝑚 + 1) → ((𝑦 ∈ (1...(#‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦)) ↔ ((𝑚 + 1) ∈ (1...(#‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1)))))
24	23	imbi2d 329	. . . 4 ⊢ (𝑦 = (𝑚 + 1) → ((𝜑 → (𝑦 ∈ (1...(#‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦))) ↔ (𝜑 → ((𝑚 + 1) ∈ (1...(#‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1))))))
25		eleq1 2676	. . . . . 6 ⊢ (𝑦 = 𝑁 → (𝑦 ∈ (1...(#‘𝐴)) ↔ 𝑁 ∈ (1...(#‘𝐴))))
26		fveq2 6103	. . . . . . . 8 ⊢ (𝑦 = 𝑁 → (𝐺‘𝑦) = (𝐺‘𝑁))
27	26	fveq2d 6107	. . . . . . 7 ⊢ (𝑦 = 𝑁 → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq𝑀( + , 𝐹)‘(𝐺‘𝑁)))
28		fveq2 6103	. . . . . . 7 ⊢ (𝑦 = 𝑁 → (seq1( + , 𝐻)‘𝑦) = (seq1( + , 𝐻)‘𝑁))
29	27, 28	eqeq12d 2625	. . . . . 6 ⊢ (𝑦 = 𝑁 → ((seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦) ↔ (seq𝑀( + , 𝐹)‘(𝐺‘𝑁)) = (seq1( + , 𝐻)‘𝑁)))
30	25, 29	imbi12d 333	. . . . 5 ⊢ (𝑦 = 𝑁 → ((𝑦 ∈ (1...(#‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦)) ↔ (𝑁 ∈ (1...(#‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑁)) = (seq1( + , 𝐻)‘𝑁))))
31	30	imbi2d 329	. . . 4 ⊢ (𝑦 = 𝑁 → ((𝜑 → (𝑦 ∈ (1...(#‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦))) ↔ (𝜑 → (𝑁 ∈ (1...(#‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑁)) = (seq1( + , 𝐻)‘𝑁)))))
32		seqcoll.1	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑆) → (𝑍 + 𝑘) = 𝑘)
33		seqcoll.a	. . . . . . . . 9 ⊢ (𝜑 → 𝑍 ∈ 𝑆)
34		seqcoll.4	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ⊆ (ℤ_≥‘𝑀))
35		seqcoll.2	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐺 Isom < , < ((1...(#‘𝐴)), 𝐴))
36		isof1o 6473	. . . . . . . . . . . . 13 ⊢ (𝐺 Isom < , < ((1...(#‘𝐴)), 𝐴) → 𝐺:(1...(#‘𝐴))–1-1-onto→𝐴)
37	35, 36	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺:(1...(#‘𝐴))–1-1-onto→𝐴)
38		f1of 6050	. . . . . . . . . . . 12 ⊢ (𝐺:(1...(#‘𝐴))–1-1-onto→𝐴 → 𝐺:(1...(#‘𝐴))⟶𝐴)
39	37, 38	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺:(1...(#‘𝐴))⟶𝐴)
40		elfzuz2 12217	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (1...(#‘𝐴)) → (#‘𝐴) ∈ (ℤ_≥‘1))
41	1, 40	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (#‘𝐴) ∈ (ℤ_≥‘1))
42		eluzfz1 12219	. . . . . . . . . . . 12 ⊢ ((#‘𝐴) ∈ (ℤ_≥‘1) → 1 ∈ (1...(#‘𝐴)))
43	41, 42	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ (1...(#‘𝐴)))
44	39, 43	ffvelrnd 6268	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺‘1) ∈ 𝐴)
45	34, 44	sseldd 3569	. . . . . . . . 9 ⊢ (𝜑 → (𝐺‘1) ∈ (ℤ_≥‘𝑀))
46		eluzle 11576	. . . . . . . . . . . . 13 ⊢ ((#‘𝐴) ∈ (ℤ_≥‘1) → 1 ≤ (#‘𝐴))
47	41, 46	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ≤ (#‘𝐴))
48		elfzelz 12213	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (1...(#‘𝐴)) → 𝑘 ∈ ℤ)
49	48	ssriv 3572	. . . . . . . . . . . . . . . 16 ⊢ (1...(#‘𝐴)) ⊆ ℤ
50		zssre 11261	. . . . . . . . . . . . . . . 16 ⊢ ℤ ⊆ ℝ
51	49, 50	sstri 3577	. . . . . . . . . . . . . . 15 ⊢ (1...(#‘𝐴)) ⊆ ℝ
52	51	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1...(#‘𝐴)) ⊆ ℝ)
53		ressxr 9962	. . . . . . . . . . . . . 14 ⊢ ℝ ⊆ ℝ^*
54	52, 53	syl6ss 3580	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1...(#‘𝐴)) ⊆ ℝ^*)
55		eluzelre 11574	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ (ℤ_≥‘𝑀) → 𝑘 ∈ ℝ)
56	55	ssriv 3572	. . . . . . . . . . . . . . 15 ⊢ (ℤ_≥‘𝑀) ⊆ ℝ
57	34, 56	syl6ss 3580	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ⊆ ℝ)
58	57, 53	syl6ss 3580	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ⊆ ℝ^*)
59		eluzfz2 12220	. . . . . . . . . . . . . 14 ⊢ ((#‘𝐴) ∈ (ℤ_≥‘1) → (#‘𝐴) ∈ (1...(#‘𝐴)))
60	41, 59	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (#‘𝐴) ∈ (1...(#‘𝐴)))
61		leisorel 13101	. . . . . . . . . . . . 13 ⊢ ((𝐺 Isom < , < ((1...(#‘𝐴)), 𝐴) ∧ ((1...(#‘𝐴)) ⊆ ℝ^* ∧ 𝐴 ⊆ ℝ^*) ∧ (1 ∈ (1...(#‘𝐴)) ∧ (#‘𝐴) ∈ (1...(#‘𝐴)))) → (1 ≤ (#‘𝐴) ↔ (𝐺‘1) ≤ (𝐺‘(#‘𝐴))))
62	35, 54, 58, 43, 60, 61	syl122anc 1327	. . . . . . . . . . . 12 ⊢ (𝜑 → (1 ≤ (#‘𝐴) ↔ (𝐺‘1) ≤ (𝐺‘(#‘𝐴))))
63	47, 62	mpbid 221	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐺‘1) ≤ (𝐺‘(#‘𝐴)))
64	39, 60	ffvelrnd 6268	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐺‘(#‘𝐴)) ∈ 𝐴)
65	34, 64	sseldd 3569	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐺‘(#‘𝐴)) ∈ (ℤ_≥‘𝑀))
66		eluzelz 11573	. . . . . . . . . . . . 13 ⊢ ((𝐺‘(#‘𝐴)) ∈ (ℤ_≥‘𝑀) → (𝐺‘(#‘𝐴)) ∈ ℤ)
67	65, 66	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐺‘(#‘𝐴)) ∈ ℤ)
68		elfz5 12205	. . . . . . . . . . . 12 ⊢ (((𝐺‘1) ∈ (ℤ_≥‘𝑀) ∧ (𝐺‘(#‘𝐴)) ∈ ℤ) → ((𝐺‘1) ∈ (𝑀...(𝐺‘(#‘𝐴))) ↔ (𝐺‘1) ≤ (𝐺‘(#‘𝐴))))
69	45, 67, 68	syl2anc 691	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐺‘1) ∈ (𝑀...(𝐺‘(#‘𝐴))) ↔ (𝐺‘1) ≤ (𝐺‘(#‘𝐴))))
70	63, 69	mpbird 246	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺‘1) ∈ (𝑀...(𝐺‘(#‘𝐴))))
71		fveq2 6103	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝐺‘1) → (𝐹‘𝑘) = (𝐹‘(𝐺‘1)))
72	71	eleq1d 2672	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝐺‘1) → ((𝐹‘𝑘) ∈ 𝑆 ↔ (𝐹‘(𝐺‘1)) ∈ 𝑆))
73	72	imbi2d 329	. . . . . . . . . . 11 ⊢ (𝑘 = (𝐺‘1) → ((𝜑 → (𝐹‘𝑘) ∈ 𝑆) ↔ (𝜑 → (𝐹‘(𝐺‘1)) ∈ 𝑆)))
74		seqcoll.5	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝐺‘(#‘𝐴)))) → (𝐹‘𝑘) ∈ 𝑆)
75	74	expcom 450	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (𝑀...(𝐺‘(#‘𝐴))) → (𝜑 → (𝐹‘𝑘) ∈ 𝑆))
76	73, 75	vtoclga 3245	. . . . . . . . . 10 ⊢ ((𝐺‘1) ∈ (𝑀...(𝐺‘(#‘𝐴))) → (𝜑 → (𝐹‘(𝐺‘1)) ∈ 𝑆))
77	70, 76	mpcom 37	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘(𝐺‘1)) ∈ 𝑆)
78		eluzelz 11573	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺‘1) ∈ (ℤ_≥‘𝑀) → (𝐺‘1) ∈ ℤ)
79	45, 78	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐺‘1) ∈ ℤ)
80		peano2zm 11297	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺‘1) ∈ ℤ → ((𝐺‘1) − 1) ∈ ℤ)
81	79, 80	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐺‘1) − 1) ∈ ℤ)
82	81	zred 11358	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐺‘1) − 1) ∈ ℝ)
83	79	zred 11358	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐺‘1) ∈ ℝ)
84	67	zred 11358	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐺‘(#‘𝐴)) ∈ ℝ)
85	83	lem1d 10836	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐺‘1) − 1) ≤ (𝐺‘1))
86	82, 83, 84, 85, 63	letrd 10073	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐺‘1) − 1) ≤ (𝐺‘(#‘𝐴)))
87		eluz 11577	. . . . . . . . . . . . . . 15 ⊢ ((((𝐺‘1) − 1) ∈ ℤ ∧ (𝐺‘(#‘𝐴)) ∈ ℤ) → ((𝐺‘(#‘𝐴)) ∈ (ℤ_≥‘((𝐺‘1) − 1)) ↔ ((𝐺‘1) − 1) ≤ (𝐺‘(#‘𝐴))))
88	81, 67, 87	syl2anc 691	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐺‘(#‘𝐴)) ∈ (ℤ_≥‘((𝐺‘1) − 1)) ↔ ((𝐺‘1) − 1) ≤ (𝐺‘(#‘𝐴))))
89	86, 88	mpbird 246	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐺‘(#‘𝐴)) ∈ (ℤ_≥‘((𝐺‘1) − 1)))
90		fzss2 12252	. . . . . . . . . . . . 13 ⊢ ((𝐺‘(#‘𝐴)) ∈ (ℤ_≥‘((𝐺‘1) − 1)) → (𝑀...((𝐺‘1) − 1)) ⊆ (𝑀...(𝐺‘(#‘𝐴))))
91	89, 90	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑀...((𝐺‘1) − 1)) ⊆ (𝑀...(𝐺‘(#‘𝐴))))
92	91	sselda 3568	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...((𝐺‘1) − 1))) → 𝑘 ∈ (𝑀...(𝐺‘(#‘𝐴))))
93		eluzel2 11568	. . . . . . . . . . . . . . 15 ⊢ ((𝐺‘1) ∈ (ℤ_≥‘𝑀) → 𝑀 ∈ ℤ)
94	45, 93	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ∈ ℤ)
95		elfzm11 12280	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℤ ∧ (𝐺‘1) ∈ ℤ) → (𝑘 ∈ (𝑀...((𝐺‘1) − 1)) ↔ (𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 < (𝐺‘1))))
96	94, 79, 95	syl2anc 691	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑘 ∈ (𝑀...((𝐺‘1) − 1)) ↔ (𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 < (𝐺‘1))))
97		simp3 1056	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 < (𝐺‘1)) → 𝑘 < (𝐺‘1))
98		f1ocnv 6062	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐺:(1...(#‘𝐴))–1-1-onto→𝐴 → ^◡𝐺:𝐴–1-1-onto→(1...(#‘𝐴)))
99	37, 98	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ^◡𝐺:𝐴–1-1-onto→(1...(#‘𝐴)))
100		f1of 6050	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (^◡𝐺:𝐴–1-1-onto→(1...(#‘𝐴)) → ^◡𝐺:𝐴⟶(1...(#‘𝐴)))
101	99, 100	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ^◡𝐺:𝐴⟶(1...(#‘𝐴)))
102	101	ffvelrnda 6267	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (^◡𝐺‘𝑘) ∈ (1...(#‘𝐴)))
103		elfznn 12241	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((^◡𝐺‘𝑘) ∈ (1...(#‘𝐴)) → (^◡𝐺‘𝑘) ∈ ℕ)
104	102, 103	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (^◡𝐺‘𝑘) ∈ ℕ)
105	104	nnge1d 10940	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 1 ≤ (^◡𝐺‘𝑘))
106	35	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐺 Isom < , < ((1...(#‘𝐴)), 𝐴))
107	54	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (1...(#‘𝐴)) ⊆ ℝ^*)
108	58	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐴 ⊆ ℝ^*)
109	43	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 1 ∈ (1...(#‘𝐴)))
110		leisorel 13101	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺 Isom < , < ((1...(#‘𝐴)), 𝐴) ∧ ((1...(#‘𝐴)) ⊆ ℝ^* ∧ 𝐴 ⊆ ℝ^*) ∧ (1 ∈ (1...(#‘𝐴)) ∧ (^◡𝐺‘𝑘) ∈ (1...(#‘𝐴)))) → (1 ≤ (^◡𝐺‘𝑘) ↔ (𝐺‘1) ≤ (𝐺‘(^◡𝐺‘𝑘))))
111	106, 107, 108, 109, 102, 110	syl122anc 1327	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (1 ≤ (^◡𝐺‘𝑘) ↔ (𝐺‘1) ≤ (𝐺‘(^◡𝐺‘𝑘))))
112	105, 111	mpbid 221	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐺‘1) ≤ (𝐺‘(^◡𝐺‘𝑘)))
113		f1ocnvfv2 6433	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺:(1...(#‘𝐴))–1-1-onto→𝐴 ∧ 𝑘 ∈ 𝐴) → (𝐺‘(^◡𝐺‘𝑘)) = 𝑘)
114	37, 113	sylan 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐺‘(^◡𝐺‘𝑘)) = 𝑘)
115	112, 114	breqtrd 4609	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐺‘1) ≤ 𝑘)
116	83	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐺‘1) ∈ ℝ)
117	57	sselda 3568	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑘 ∈ ℝ)
118	116, 117	lenltd 10062	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝐺‘1) ≤ 𝑘 ↔ ¬ 𝑘 < (𝐺‘1)))
119	115, 118	mpbid 221	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ¬ 𝑘 < (𝐺‘1))
120	119	ex 449	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑘 ∈ 𝐴 → ¬ 𝑘 < (𝐺‘1)))
121	120	con2d 128	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑘 < (𝐺‘1) → ¬ 𝑘 ∈ 𝐴))
122	97, 121	syl5 33	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 < (𝐺‘1)) → ¬ 𝑘 ∈ 𝐴))
123	96, 122	sylbid 229	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑘 ∈ (𝑀...((𝐺‘1) − 1)) → ¬ 𝑘 ∈ 𝐴))
124	123	imp 444	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...((𝐺‘1) − 1))) → ¬ 𝑘 ∈ 𝐴)
125	92, 124	eldifd 3551	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...((𝐺‘1) − 1))) → 𝑘 ∈ ((𝑀...(𝐺‘(#‘𝐴))) ∖ 𝐴))
126		seqcoll.6	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀...(𝐺‘(#‘𝐴))) ∖ 𝐴)) → (𝐹‘𝑘) = 𝑍)
127	125, 126	syldan 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...((𝐺‘1) − 1))) → (𝐹‘𝑘) = 𝑍)
128	32, 33, 45, 77, 127	seqid 12708	. . . . . . . 8 ⊢ (𝜑 → (seq𝑀( + , 𝐹) ↾ (ℤ_≥‘(𝐺‘1))) = seq(𝐺‘1)( + , 𝐹))
129	128	fveq1d 6105	. . . . . . 7 ⊢ (𝜑 → ((seq𝑀( + , 𝐹) ↾ (ℤ_≥‘(𝐺‘1)))‘(𝐺‘1)) = (seq(𝐺‘1)( + , 𝐹)‘(𝐺‘1)))
130		uzid 11578	. . . . . . . . 9 ⊢ ((𝐺‘1) ∈ ℤ → (𝐺‘1) ∈ (ℤ_≥‘(𝐺‘1)))
131	79, 130	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝐺‘1) ∈ (ℤ_≥‘(𝐺‘1)))
132		fvres 6117	. . . . . . . 8 ⊢ ((𝐺‘1) ∈ (ℤ_≥‘(𝐺‘1)) → ((seq𝑀( + , 𝐹) ↾ (ℤ_≥‘(𝐺‘1)))‘(𝐺‘1)) = (seq𝑀( + , 𝐹)‘(𝐺‘1)))
133	131, 132	syl 17	. . . . . . 7 ⊢ (𝜑 → ((seq𝑀( + , 𝐹) ↾ (ℤ_≥‘(𝐺‘1)))‘(𝐺‘1)) = (seq𝑀( + , 𝐹)‘(𝐺‘1)))
134		seq1 12676	. . . . . . . . 9 ⊢ ((𝐺‘1) ∈ ℤ → (seq(𝐺‘1)( + , 𝐹)‘(𝐺‘1)) = (𝐹‘(𝐺‘1)))
135	79, 134	syl 17	. . . . . . . 8 ⊢ (𝜑 → (seq(𝐺‘1)( + , 𝐹)‘(𝐺‘1)) = (𝐹‘(𝐺‘1)))
136		fveq2 6103	. . . . . . . . . . . 12 ⊢ (𝑛 = 1 → (𝐻‘𝑛) = (𝐻‘1))
137		fveq2 6103	. . . . . . . . . . . . 13 ⊢ (𝑛 = 1 → (𝐺‘𝑛) = (𝐺‘1))
138	137	fveq2d 6107	. . . . . . . . . . . 12 ⊢ (𝑛 = 1 → (𝐹‘(𝐺‘𝑛)) = (𝐹‘(𝐺‘1)))
139	136, 138	eqeq12d 2625	. . . . . . . . . . 11 ⊢ (𝑛 = 1 → ((𝐻‘𝑛) = (𝐹‘(𝐺‘𝑛)) ↔ (𝐻‘1) = (𝐹‘(𝐺‘1))))
140	139	imbi2d 329	. . . . . . . . . 10 ⊢ (𝑛 = 1 → ((𝜑 → (𝐻‘𝑛) = (𝐹‘(𝐺‘𝑛))) ↔ (𝜑 → (𝐻‘1) = (𝐹‘(𝐺‘1)))))
141		seqcoll.7	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(#‘𝐴))) → (𝐻‘𝑛) = (𝐹‘(𝐺‘𝑛)))
142	141	expcom 450	. . . . . . . . . 10 ⊢ (𝑛 ∈ (1...(#‘𝐴)) → (𝜑 → (𝐻‘𝑛) = (𝐹‘(𝐺‘𝑛))))
143	140, 142	vtoclga 3245	. . . . . . . . 9 ⊢ (1 ∈ (1...(#‘𝐴)) → (𝜑 → (𝐻‘1) = (𝐹‘(𝐺‘1))))
144	43, 143	mpcom 37	. . . . . . . 8 ⊢ (𝜑 → (𝐻‘1) = (𝐹‘(𝐺‘1)))
145	135, 144	eqtr4d 2647	. . . . . . 7 ⊢ (𝜑 → (seq(𝐺‘1)( + , 𝐹)‘(𝐺‘1)) = (𝐻‘1))
146	129, 133, 145	3eqtr3d 2652	. . . . . 6 ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘(𝐺‘1)) = (𝐻‘1))
147		1z 11284	. . . . . . 7 ⊢ 1 ∈ ℤ
148		seq1 12676	. . . . . . 7 ⊢ (1 ∈ ℤ → (seq1( + , 𝐻)‘1) = (𝐻‘1))
149	147, 148	ax-mp 5	. . . . . 6 ⊢ (seq1( + , 𝐻)‘1) = (𝐻‘1)
150	146, 149	syl6eqr 2662	. . . . 5 ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘(𝐺‘1)) = (seq1( + , 𝐻)‘1))
151	150	a1d 25	. . . 4 ⊢ (𝜑 → (1 ∈ (1...(#‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘1)) = (seq1( + , 𝐻)‘1)))
152		simplr 788	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → 𝑚 ∈ ℕ)
153		nnuz 11599	. . . . . . . . . . 11 ⊢ ℕ = (ℤ_≥‘1)
154	152, 153	syl6eleq 2698	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → 𝑚 ∈ (ℤ_≥‘1))
155		nnz 11276	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℤ)
156	155	ad2antlr 759	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → 𝑚 ∈ ℤ)
157		elfzuz3 12210	. . . . . . . . . . . 12 ⊢ ((𝑚 + 1) ∈ (1...(#‘𝐴)) → (#‘𝐴) ∈ (ℤ_≥‘(𝑚 + 1)))
158	157	adantl 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (#‘𝐴) ∈ (ℤ_≥‘(𝑚 + 1)))
159		peano2uzr 11619	. . . . . . . . . . 11 ⊢ ((𝑚 ∈ ℤ ∧ (#‘𝐴) ∈ (ℤ_≥‘(𝑚 + 1))) → (#‘𝐴) ∈ (ℤ_≥‘𝑚))
160	156, 158, 159	syl2anc 691	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (#‘𝐴) ∈ (ℤ_≥‘𝑚))
161		elfzuzb 12207	. . . . . . . . . 10 ⊢ (𝑚 ∈ (1...(#‘𝐴)) ↔ (𝑚 ∈ (ℤ_≥‘1) ∧ (#‘𝐴) ∈ (ℤ_≥‘𝑚)))
162	154, 160, 161	sylanbrc 695	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → 𝑚 ∈ (1...(#‘𝐴)))
163	162	ex 449	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑚 + 1) ∈ (1...(#‘𝐴)) → 𝑚 ∈ (1...(#‘𝐴))))
164	163	imim1d 80	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑚 ∈ (1...(#‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq1( + , 𝐻)‘𝑚)) → ((𝑚 + 1) ∈ (1...(#‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq1( + , 𝐻)‘𝑚))))
165		oveq1 6556	. . . . . . . . . 10 ⊢ ((seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq1( + , 𝐻)‘𝑚) → ((seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) + (𝐻‘(𝑚 + 1))) = ((seq1( + , 𝐻)‘𝑚) + (𝐻‘(𝑚 + 1))))
166		simpll 786	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → 𝜑)
167		seqcoll.1b	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑆) → (𝑘 + 𝑍) = 𝑘)
168	166, 167	sylan 487	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) ∧ 𝑘 ∈ 𝑆) → (𝑘 + 𝑍) = 𝑘)
169	34	ad2antrr 758	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → 𝐴 ⊆ (ℤ_≥‘𝑀))
170	39	ad2antrr 758	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → 𝐺:(1...(#‘𝐴))⟶𝐴)
171	170, 162	ffvelrnd 6268	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (𝐺‘𝑚) ∈ 𝐴)
172	169, 171	sseldd 3569	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (𝐺‘𝑚) ∈ (ℤ_≥‘𝑀))
173		nnre 10904	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℝ)
174	173	ad2antlr 759	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → 𝑚 ∈ ℝ)
175	174	ltp1d 10833	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → 𝑚 < (𝑚 + 1))
176	35	ad2antrr 758	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → 𝐺 Isom < , < ((1...(#‘𝐴)), 𝐴))
177		simpr 476	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (𝑚 + 1) ∈ (1...(#‘𝐴)))
178		isorel 6476	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺 Isom < , < ((1...(#‘𝐴)), 𝐴) ∧ (𝑚 ∈ (1...(#‘𝐴)) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴)))) → (𝑚 < (𝑚 + 1) ↔ (𝐺‘𝑚) < (𝐺‘(𝑚 + 1))))
179	176, 162, 177, 178	syl12anc 1316	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (𝑚 < (𝑚 + 1) ↔ (𝐺‘𝑚) < (𝐺‘(𝑚 + 1))))
180	175, 179	mpbid 221	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (𝐺‘𝑚) < (𝐺‘(𝑚 + 1)))
181		eluzelz 11573	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺‘𝑚) ∈ (ℤ_≥‘𝑀) → (𝐺‘𝑚) ∈ ℤ)
182	172, 181	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (𝐺‘𝑚) ∈ ℤ)
183	170, 177	ffvelrnd 6268	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (𝐺‘(𝑚 + 1)) ∈ 𝐴)
184	169, 183	sseldd 3569	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (𝐺‘(𝑚 + 1)) ∈ (ℤ_≥‘𝑀))
185		eluzelz 11573	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺‘(𝑚 + 1)) ∈ (ℤ_≥‘𝑀) → (𝐺‘(𝑚 + 1)) ∈ ℤ)
186	184, 185	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (𝐺‘(𝑚 + 1)) ∈ ℤ)
187		zltlem1 11307	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐺‘𝑚) ∈ ℤ ∧ (𝐺‘(𝑚 + 1)) ∈ ℤ) → ((𝐺‘𝑚) < (𝐺‘(𝑚 + 1)) ↔ (𝐺‘𝑚) ≤ ((𝐺‘(𝑚 + 1)) − 1)))
188	182, 186, 187	syl2anc 691	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → ((𝐺‘𝑚) < (𝐺‘(𝑚 + 1)) ↔ (𝐺‘𝑚) ≤ ((𝐺‘(𝑚 + 1)) − 1)))
189	180, 188	mpbid 221	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (𝐺‘𝑚) ≤ ((𝐺‘(𝑚 + 1)) − 1))
190		peano2zm 11297	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺‘(𝑚 + 1)) ∈ ℤ → ((𝐺‘(𝑚 + 1)) − 1) ∈ ℤ)
191	186, 190	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → ((𝐺‘(𝑚 + 1)) − 1) ∈ ℤ)
192		eluz 11577	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺‘𝑚) ∈ ℤ ∧ ((𝐺‘(𝑚 + 1)) − 1) ∈ ℤ) → (((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ_≥‘(𝐺‘𝑚)) ↔ (𝐺‘𝑚) ≤ ((𝐺‘(𝑚 + 1)) − 1)))
193	182, 191, 192	syl2anc 691	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ_≥‘(𝐺‘𝑚)) ↔ (𝐺‘𝑚) ≤ ((𝐺‘(𝑚 + 1)) − 1)))
194	189, 193	mpbird 246	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → ((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ_≥‘(𝐺‘𝑚)))
195	191	zred 11358	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → ((𝐺‘(𝑚 + 1)) − 1) ∈ ℝ)
196	186	zred 11358	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (𝐺‘(𝑚 + 1)) ∈ ℝ)
197	84	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (𝐺‘(#‘𝐴)) ∈ ℝ)
198	196	lem1d 10836	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → ((𝐺‘(𝑚 + 1)) − 1) ≤ (𝐺‘(𝑚 + 1)))
199		elfzle2 12216	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑚 + 1) ∈ (1...(#‘𝐴)) → (𝑚 + 1) ≤ (#‘𝐴))
200	199	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (𝑚 + 1) ≤ (#‘𝐴))
201	54	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (1...(#‘𝐴)) ⊆ ℝ^*)
202	58	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → 𝐴 ⊆ ℝ^*)
203	60	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (#‘𝐴) ∈ (1...(#‘𝐴)))
204		leisorel 13101	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐺 Isom < , < ((1...(#‘𝐴)), 𝐴) ∧ ((1...(#‘𝐴)) ⊆ ℝ^* ∧ 𝐴 ⊆ ℝ^*) ∧ ((𝑚 + 1) ∈ (1...(#‘𝐴)) ∧ (#‘𝐴) ∈ (1...(#‘𝐴)))) → ((𝑚 + 1) ≤ (#‘𝐴) ↔ (𝐺‘(𝑚 + 1)) ≤ (𝐺‘(#‘𝐴))))
205	176, 201, 202, 177, 203, 204	syl122anc 1327	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → ((𝑚 + 1) ≤ (#‘𝐴) ↔ (𝐺‘(𝑚 + 1)) ≤ (𝐺‘(#‘𝐴))))
206	200, 205	mpbid 221	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (𝐺‘(𝑚 + 1)) ≤ (𝐺‘(#‘𝐴)))
207	195, 196, 197, 198, 206	letrd 10073	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → ((𝐺‘(𝑚 + 1)) − 1) ≤ (𝐺‘(#‘𝐴)))
208	67	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (𝐺‘(#‘𝐴)) ∈ ℤ)
209		eluz 11577	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐺‘(𝑚 + 1)) − 1) ∈ ℤ ∧ (𝐺‘(#‘𝐴)) ∈ ℤ) → ((𝐺‘(#‘𝐴)) ∈ (ℤ_≥‘((𝐺‘(𝑚 + 1)) − 1)) ↔ ((𝐺‘(𝑚 + 1)) − 1) ≤ (𝐺‘(#‘𝐴))))
210	191, 208, 209	syl2anc 691	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → ((𝐺‘(#‘𝐴)) ∈ (ℤ_≥‘((𝐺‘(𝑚 + 1)) − 1)) ↔ ((𝐺‘(𝑚 + 1)) − 1) ≤ (𝐺‘(#‘𝐴))))
211	207, 210	mpbird 246	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (𝐺‘(#‘𝐴)) ∈ (ℤ_≥‘((𝐺‘(𝑚 + 1)) − 1)))
212		uztrn 11580	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐺‘(#‘𝐴)) ∈ (ℤ_≥‘((𝐺‘(𝑚 + 1)) − 1)) ∧ ((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ_≥‘(𝐺‘𝑚))) → (𝐺‘(#‘𝐴)) ∈ (ℤ_≥‘(𝐺‘𝑚)))
213	211, 194, 212	syl2anc 691	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (𝐺‘(#‘𝐴)) ∈ (ℤ_≥‘(𝐺‘𝑚)))
214		fzss2 12252	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺‘(#‘𝐴)) ∈ (ℤ_≥‘(𝐺‘𝑚)) → (𝑀...(𝐺‘𝑚)) ⊆ (𝑀...(𝐺‘(#‘𝐴))))
215	213, 214	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (𝑀...(𝐺‘𝑚)) ⊆ (𝑀...(𝐺‘(#‘𝐴))))
216	215	sselda 3568	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) ∧ 𝑘 ∈ (𝑀...(𝐺‘𝑚))) → 𝑘 ∈ (𝑀...(𝐺‘(#‘𝐴))))
217	166, 74	sylan 487	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) ∧ 𝑘 ∈ (𝑀...(𝐺‘(#‘𝐴)))) → (𝐹‘𝑘) ∈ 𝑆)
218	216, 217	syldan 486	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) ∧ 𝑘 ∈ (𝑀...(𝐺‘𝑚))) → (𝐹‘𝑘) ∈ 𝑆)
219		seqcoll.c	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑘 ∈ 𝑆 ∧ 𝑛 ∈ 𝑆)) → (𝑘 + 𝑛) ∈ 𝑆)
220	166, 219	sylan 487	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) ∧ (𝑘 ∈ 𝑆 ∧ 𝑛 ∈ 𝑆)) → (𝑘 + 𝑛) ∈ 𝑆)
221	172, 218, 220	seqcl 12683	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) ∈ 𝑆)
222		simplll 794	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) ∧ 𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1))) → 𝜑)
223		elfzuz 12209	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1)) → 𝑘 ∈ (ℤ_≥‘((𝐺‘𝑚) + 1)))
224		peano2uz 11617	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺‘𝑚) ∈ (ℤ_≥‘𝑀) → ((𝐺‘𝑚) + 1) ∈ (ℤ_≥‘𝑀))
225	172, 224	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → ((𝐺‘𝑚) + 1) ∈ (ℤ_≥‘𝑀))
226		uztrn 11580	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ (ℤ_≥‘((𝐺‘𝑚) + 1)) ∧ ((𝐺‘𝑚) + 1) ∈ (ℤ_≥‘𝑀)) → 𝑘 ∈ (ℤ_≥‘𝑀))
227	223, 225, 226	syl2anr 494	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) ∧ 𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1))) → 𝑘 ∈ (ℤ_≥‘𝑀))
228		elfzuz3 12210	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1)) → ((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ_≥‘𝑘))
229		uztrn 11580	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐺‘(#‘𝐴)) ∈ (ℤ_≥‘((𝐺‘(𝑚 + 1)) − 1)) ∧ ((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ_≥‘𝑘)) → (𝐺‘(#‘𝐴)) ∈ (ℤ_≥‘𝑘))
230	211, 228, 229	syl2an 493	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) ∧ 𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1))) → (𝐺‘(#‘𝐴)) ∈ (ℤ_≥‘𝑘))
231		elfzuzb 12207	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (𝑀...(𝐺‘(#‘𝐴))) ↔ (𝑘 ∈ (ℤ_≥‘𝑀) ∧ (𝐺‘(#‘𝐴)) ∈ (ℤ_≥‘𝑘)))
232	227, 230, 231	sylanbrc 695	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) ∧ 𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1))) → 𝑘 ∈ (𝑀...(𝐺‘(#‘𝐴))))
233		elfzle1 12215	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1)) → ((𝐺‘𝑚) + 1) ≤ 𝑘)
234		elfzle2 12216	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1)) → 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1))
235	233, 234	jca 553	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1)) → (((𝐺‘𝑚) + 1) ≤ 𝑘 ∧ 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1)))
236	155	ad2antlr 759	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(#‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → 𝑚 ∈ ℤ)
237	101	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(#‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → ^◡𝐺:𝐴⟶(1...(#‘𝐴)))
238		simprr 792	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(#‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → 𝑘 ∈ 𝐴)
239	237, 238	ffvelrnd 6268	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(#‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → (^◡𝐺‘𝑘) ∈ (1...(#‘𝐴)))
240		elfzelz 12213	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((^◡𝐺‘𝑘) ∈ (1...(#‘𝐴)) → (^◡𝐺‘𝑘) ∈ ℤ)
241	239, 240	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(#‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → (^◡𝐺‘𝑘) ∈ ℤ)
242		btwnnz 11329	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑚 ∈ ℤ ∧ 𝑚 < (^◡𝐺‘𝑘) ∧ (^◡𝐺‘𝑘) < (𝑚 + 1)) → ¬ (^◡𝐺‘𝑘) ∈ ℤ)
243	242	3expib 1260	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑚 ∈ ℤ → ((𝑚 < (^◡𝐺‘𝑘) ∧ (^◡𝐺‘𝑘) < (𝑚 + 1)) → ¬ (^◡𝐺‘𝑘) ∈ ℤ))
244	243	con2d 128	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 ∈ ℤ → ((^◡𝐺‘𝑘) ∈ ℤ → ¬ (𝑚 < (^◡𝐺‘𝑘) ∧ (^◡𝐺‘𝑘) < (𝑚 + 1))))
245	236, 241, 244	sylc 63	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(#‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → ¬ (𝑚 < (^◡𝐺‘𝑘) ∧ (^◡𝐺‘𝑘) < (𝑚 + 1)))
246	35	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(#‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → 𝐺 Isom < , < ((1...(#‘𝐴)), 𝐴))
247	162	adantrr 749	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(#‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → 𝑚 ∈ (1...(#‘𝐴)))
248		isorel 6476	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐺 Isom < , < ((1...(#‘𝐴)), 𝐴) ∧ (𝑚 ∈ (1...(#‘𝐴)) ∧ (^◡𝐺‘𝑘) ∈ (1...(#‘𝐴)))) → (𝑚 < (^◡𝐺‘𝑘) ↔ (𝐺‘𝑚) < (𝐺‘(^◡𝐺‘𝑘))))
249	246, 247, 239, 248	syl12anc 1316	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(#‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → (𝑚 < (^◡𝐺‘𝑘) ↔ (𝐺‘𝑚) < (𝐺‘(^◡𝐺‘𝑘))))
250	37	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(#‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → 𝐺:(1...(#‘𝐴))–1-1-onto→𝐴)
251	250, 238, 113	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(#‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → (𝐺‘(^◡𝐺‘𝑘)) = 𝑘)
252	251	breq2d 4595	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(#‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → ((𝐺‘𝑚) < (𝐺‘(^◡𝐺‘𝑘)) ↔ (𝐺‘𝑚) < 𝑘))
253	182	adantrr 749	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(#‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → (𝐺‘𝑚) ∈ ℤ)
254	34	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(#‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → 𝐴 ⊆ (ℤ_≥‘𝑀))
255	254, 238	sseldd 3569	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(#‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → 𝑘 ∈ (ℤ_≥‘𝑀))
256		eluzelz 11573	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 ∈ (ℤ_≥‘𝑀) → 𝑘 ∈ ℤ)
257	255, 256	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(#‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → 𝑘 ∈ ℤ)
258		zltp1le 11304	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐺‘𝑚) ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((𝐺‘𝑚) < 𝑘 ↔ ((𝐺‘𝑚) + 1) ≤ 𝑘))
259	253, 257, 258	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(#‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → ((𝐺‘𝑚) < 𝑘 ↔ ((𝐺‘𝑚) + 1) ≤ 𝑘))
260	249, 252, 259	3bitrd 293	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(#‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → (𝑚 < (^◡𝐺‘𝑘) ↔ ((𝐺‘𝑚) + 1) ≤ 𝑘))
261	177	adantrr 749	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(#‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → (𝑚 + 1) ∈ (1...(#‘𝐴)))
262		isorel 6476	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐺 Isom < , < ((1...(#‘𝐴)), 𝐴) ∧ ((^◡𝐺‘𝑘) ∈ (1...(#‘𝐴)) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴)))) → ((^◡𝐺‘𝑘) < (𝑚 + 1) ↔ (𝐺‘(^◡𝐺‘𝑘)) < (𝐺‘(𝑚 + 1))))
263	246, 239, 261, 262	syl12anc 1316	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(#‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → ((^◡𝐺‘𝑘) < (𝑚 + 1) ↔ (𝐺‘(^◡𝐺‘𝑘)) < (𝐺‘(𝑚 + 1))))
264	251	breq1d 4593	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(#‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → ((𝐺‘(^◡𝐺‘𝑘)) < (𝐺‘(𝑚 + 1)) ↔ 𝑘 < (𝐺‘(𝑚 + 1))))
265	186	adantrr 749	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(#‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → (𝐺‘(𝑚 + 1)) ∈ ℤ)
266		zltlem1 11307	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑘 ∈ ℤ ∧ (𝐺‘(𝑚 + 1)) ∈ ℤ) → (𝑘 < (𝐺‘(𝑚 + 1)) ↔ 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1)))
267	257, 265, 266	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(#‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → (𝑘 < (𝐺‘(𝑚 + 1)) ↔ 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1)))
268	263, 264, 267	3bitrd 293	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(#‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → ((^◡𝐺‘𝑘) < (𝑚 + 1) ↔ 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1)))
269	260, 268	anbi12d 743	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(#‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → ((𝑚 < (^◡𝐺‘𝑘) ∧ (^◡𝐺‘𝑘) < (𝑚 + 1)) ↔ (((𝐺‘𝑚) + 1) ≤ 𝑘 ∧ 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1))))
270	245, 269	mtbid 313	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(#‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → ¬ (((𝐺‘𝑚) + 1) ≤ 𝑘 ∧ 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1)))
271	270	expr 641	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (𝑘 ∈ 𝐴 → ¬ (((𝐺‘𝑚) + 1) ≤ 𝑘 ∧ 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1))))
272	271	con2d 128	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → ((((𝐺‘𝑚) + 1) ≤ 𝑘 ∧ 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1)) → ¬ 𝑘 ∈ 𝐴))
273	235, 272	syl5 33	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1)) → ¬ 𝑘 ∈ 𝐴))
274	273	imp 444	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) ∧ 𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1))) → ¬ 𝑘 ∈ 𝐴)
275	232, 274	eldifd 3551	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) ∧ 𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1))) → 𝑘 ∈ ((𝑀...(𝐺‘(#‘𝐴))) ∖ 𝐴))
276	222, 275, 126	syl2anc 691	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) ∧ 𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1))) → (𝐹‘𝑘) = 𝑍)
277	168, 172, 194, 221, 276	seqid2 12709	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq𝑀( + , 𝐹)‘((𝐺‘(𝑚 + 1)) − 1)))
278	277	oveq1d 6564	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → ((seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) + (𝐹‘(𝐺‘(𝑚 + 1)))) = ((seq𝑀( + , 𝐹)‘((𝐺‘(𝑚 + 1)) − 1)) + (𝐹‘(𝐺‘(𝑚 + 1)))))
279		fveq2 6103	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = (𝑚 + 1) → (𝐻‘𝑛) = (𝐻‘(𝑚 + 1)))
280		fveq2 6103	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = (𝑚 + 1) → (𝐺‘𝑛) = (𝐺‘(𝑚 + 1)))
281	280	fveq2d 6107	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = (𝑚 + 1) → (𝐹‘(𝐺‘𝑛)) = (𝐹‘(𝐺‘(𝑚 + 1))))
282	279, 281	eqeq12d 2625	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = (𝑚 + 1) → ((𝐻‘𝑛) = (𝐹‘(𝐺‘𝑛)) ↔ (𝐻‘(𝑚 + 1)) = (𝐹‘(𝐺‘(𝑚 + 1)))))
283	282	imbi2d 329	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = (𝑚 + 1) → ((𝜑 → (𝐻‘𝑛) = (𝐹‘(𝐺‘𝑛))) ↔ (𝜑 → (𝐻‘(𝑚 + 1)) = (𝐹‘(𝐺‘(𝑚 + 1))))))
284	283, 142	vtoclga 3245	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 + 1) ∈ (1...(#‘𝐴)) → (𝜑 → (𝐻‘(𝑚 + 1)) = (𝐹‘(𝐺‘(𝑚 + 1)))))
285	284	impcom 445	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (𝐻‘(𝑚 + 1)) = (𝐹‘(𝐺‘(𝑚 + 1))))
286	285	adantlr 747	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (𝐻‘(𝑚 + 1)) = (𝐹‘(𝐺‘(𝑚 + 1))))
287	286	oveq2d 6565	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → ((seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) + (𝐻‘(𝑚 + 1))) = ((seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) + (𝐹‘(𝐺‘(𝑚 + 1)))))
288	94	ad2antrr 758	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → 𝑀 ∈ ℤ)
289	186	zcnd 11359	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (𝐺‘(𝑚 + 1)) ∈ ℂ)
290		ax-1cn 9873	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
291		npcan 10169	. . . . . . . . . . . . . . 15 ⊢ (((𝐺‘(𝑚 + 1)) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝐺‘(𝑚 + 1)) − 1) + 1) = (𝐺‘(𝑚 + 1)))
292	289, 290, 291	sylancl 693	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (((𝐺‘(𝑚 + 1)) − 1) + 1) = (𝐺‘(𝑚 + 1)))
293		uztrn 11580	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ_≥‘(𝐺‘𝑚)) ∧ (𝐺‘𝑚) ∈ (ℤ_≥‘𝑀)) → ((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ_≥‘𝑀))
294	194, 172, 293	syl2anc 691	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → ((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ_≥‘𝑀))
295		eluzp1p1 11589	. . . . . . . . . . . . . . 15 ⊢ (((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ_≥‘𝑀) → (((𝐺‘(𝑚 + 1)) − 1) + 1) ∈ (ℤ_≥‘(𝑀 + 1)))
296	294, 295	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (((𝐺‘(𝑚 + 1)) − 1) + 1) ∈ (ℤ_≥‘(𝑀 + 1)))
297	292, 296	eqeltrrd 2689	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (𝐺‘(𝑚 + 1)) ∈ (ℤ_≥‘(𝑀 + 1)))
298		seqm1 12680	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℤ ∧ (𝐺‘(𝑚 + 1)) ∈ (ℤ_≥‘(𝑀 + 1))) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = ((seq𝑀( + , 𝐹)‘((𝐺‘(𝑚 + 1)) − 1)) + (𝐹‘(𝐺‘(𝑚 + 1)))))
299	288, 297, 298	syl2anc 691	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = ((seq𝑀( + , 𝐹)‘((𝐺‘(𝑚 + 1)) − 1)) + (𝐹‘(𝐺‘(𝑚 + 1)))))
300	278, 287, 299	3eqtr4rd 2655	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = ((seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) + (𝐻‘(𝑚 + 1))))
301		seqp1 12678	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ (ℤ_≥‘1) → (seq1( + , 𝐻)‘(𝑚 + 1)) = ((seq1( + , 𝐻)‘𝑚) + (𝐻‘(𝑚 + 1))))
302	154, 301	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (seq1( + , 𝐻)‘(𝑚 + 1)) = ((seq1( + , 𝐻)‘𝑚) + (𝐻‘(𝑚 + 1))))
303	300, 302	eqeq12d 2625	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → ((seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1)) ↔ ((seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) + (𝐻‘(𝑚 + 1))) = ((seq1( + , 𝐻)‘𝑚) + (𝐻‘(𝑚 + 1)))))
304	165, 303	syl5ibr 235	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → ((seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq1( + , 𝐻)‘𝑚) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1))))
305	304	ex 449	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑚 + 1) ∈ (1...(#‘𝐴)) → ((seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq1( + , 𝐻)‘𝑚) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1)))))
306	305	a2d 29	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (((𝑚 + 1) ∈ (1...(#‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq1( + , 𝐻)‘𝑚)) → ((𝑚 + 1) ∈ (1...(#‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1)))))
307	164, 306	syld 46	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑚 ∈ (1...(#‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq1( + , 𝐻)‘𝑚)) → ((𝑚 + 1) ∈ (1...(#‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1)))))
308	307	expcom 450	. . . . 5 ⊢ (𝑚 ∈ ℕ → (𝜑 → ((𝑚 ∈ (1...(#‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq1( + , 𝐻)‘𝑚)) → ((𝑚 + 1) ∈ (1...(#‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1))))))
309	308	a2d 29	. . . 4 ⊢ (𝑚 ∈ ℕ → ((𝜑 → (𝑚 ∈ (1...(#‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq1( + , 𝐻)‘𝑚))) → (𝜑 → ((𝑚 + 1) ∈ (1...(#‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1))))))
310	10, 17, 24, 31, 151, 309	nnind 10915	. . 3 ⊢ (𝑁 ∈ ℕ → (𝜑 → (𝑁 ∈ (1...(#‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑁)) = (seq1( + , 𝐻)‘𝑁))))
311	3, 310	mpcom 37	. 2 ⊢ (𝜑 → (𝑁 ∈ (1...(#‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑁)) = (seq1( + , 𝐻)‘𝑁)))
312	1, 311	mpd 15	1 ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘(𝐺‘𝑁)) = (seq1( + , 𝐻)‘𝑁))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 195 ∧ wa 383 ∧ w3a 1031 = wceq 1475 ∈ wcel 1977 ∖ cdif 3537 ⊆ wss 3540 class class class wbr 4583 ^◡ccnv 5037 ↾ cres 5040 ⟶wf 5800 –1-1-onto→wf1o 5803 ‘cfv 5804 Isom wiso 5805 (class class class)co 6549 ℂcc 9813 ℝcr 9814 1c1 9816 + caddc 9818 ℝ^*cxr 9952 < clt 9953 ≤ cle 9954 − cmin 10145 ℕcn 10897 ℤcz 11254 ℤ_≥cuz 11563 ...cfz 12197 seqcseq 12663 #chash 12979

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-isom 5813 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-om 6958 df-1st 7059 df-2nd 7060 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-er 7629 df-en 7842 df-dom 7843 df-sdom 7844 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-nn 10898 df-n0 11170 df-z 11255 df-uz 11564 df-fz 12198 df-seq 12664

This theorem is referenced by: seqcoll2 13106 summolem2a 14293 prodmolem2a 14503

W3C validator