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 13248

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 12370	. . . 4 ⊢ (𝑁 ∈ (1...(#‘𝐴)) → 𝑁 ∈ ℕ)
3	1, 2	syl 17	. . 3 ⊢ (𝜑 → 𝑁 ∈ ℕ)
4		eleq1 2689	. . . . . 6 ⊢ (𝑦 = 1 → (𝑦 ∈ (1...(#‘𝐴)) ↔ 1 ∈ (1...(#‘𝐴))))
5		fveq2 6191	. . . . . . . 8 ⊢ (𝑦 = 1 → (𝐺‘𝑦) = (𝐺‘1))
6	5	fveq2d 6195	. . . . . . 7 ⊢ (𝑦 = 1 → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq𝑀( + , 𝐹)‘(𝐺‘1)))
7		fveq2 6191	. . . . . . 7 ⊢ (𝑦 = 1 → (seq1( + , 𝐻)‘𝑦) = (seq1( + , 𝐻)‘1))
8	6, 7	eqeq12d 2637	. . . . . 6 ⊢ (𝑦 = 1 → ((seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦) ↔ (seq𝑀( + , 𝐹)‘(𝐺‘1)) = (seq1( + , 𝐻)‘1)))
9	4, 8	imbi12d 334	. . . . 5 ⊢ (𝑦 = 1 → ((𝑦 ∈ (1...(#‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦)) ↔ (1 ∈ (1...(#‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘1)) = (seq1( + , 𝐻)‘1))))
10	9	imbi2d 330	. . . 4 ⊢ (𝑦 = 1 → ((𝜑 → (𝑦 ∈ (1...(#‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦))) ↔ (𝜑 → (1 ∈ (1...(#‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘1)) = (seq1( + , 𝐻)‘1)))))
11		eleq1 2689	. . . . . 6 ⊢ (𝑦 = 𝑚 → (𝑦 ∈ (1...(#‘𝐴)) ↔ 𝑚 ∈ (1...(#‘𝐴))))
12		fveq2 6191	. . . . . . . 8 ⊢ (𝑦 = 𝑚 → (𝐺‘𝑦) = (𝐺‘𝑚))
13	12	fveq2d 6195	. . . . . . 7 ⊢ (𝑦 = 𝑚 → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)))
14		fveq2 6191	. . . . . . 7 ⊢ (𝑦 = 𝑚 → (seq1( + , 𝐻)‘𝑦) = (seq1( + , 𝐻)‘𝑚))
15	13, 14	eqeq12d 2637	. . . . . 6 ⊢ (𝑦 = 𝑚 → ((seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦) ↔ (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq1( + , 𝐻)‘𝑚)))
16	11, 15	imbi12d 334	. . . . 5 ⊢ (𝑦 = 𝑚 → ((𝑦 ∈ (1...(#‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦)) ↔ (𝑚 ∈ (1...(#‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq1( + , 𝐻)‘𝑚))))
17	16	imbi2d 330	. . . 4 ⊢ (𝑦 = 𝑚 → ((𝜑 → (𝑦 ∈ (1...(#‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦))) ↔ (𝜑 → (𝑚 ∈ (1...(#‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq1( + , 𝐻)‘𝑚)))))
18		eleq1 2689	. . . . . 6 ⊢ (𝑦 = (𝑚 + 1) → (𝑦 ∈ (1...(#‘𝐴)) ↔ (𝑚 + 1) ∈ (1...(#‘𝐴))))
19		fveq2 6191	. . . . . . . 8 ⊢ (𝑦 = (𝑚 + 1) → (𝐺‘𝑦) = (𝐺‘(𝑚 + 1)))
20	19	fveq2d 6195	. . . . . . 7 ⊢ (𝑦 = (𝑚 + 1) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))))
21		fveq2 6191	. . . . . . 7 ⊢ (𝑦 = (𝑚 + 1) → (seq1( + , 𝐻)‘𝑦) = (seq1( + , 𝐻)‘(𝑚 + 1)))
22	20, 21	eqeq12d 2637	. . . . . 6 ⊢ (𝑦 = (𝑚 + 1) → ((seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦) ↔ (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1))))
23	18, 22	imbi12d 334	. . . . 5 ⊢ (𝑦 = (𝑚 + 1) → ((𝑦 ∈ (1...(#‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦)) ↔ ((𝑚 + 1) ∈ (1...(#‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1)))))
24	23	imbi2d 330	. . . 4 ⊢ (𝑦 = (𝑚 + 1) → ((𝜑 → (𝑦 ∈ (1...(#‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦))) ↔ (𝜑 → ((𝑚 + 1) ∈ (1...(#‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1))))))
25		eleq1 2689	. . . . . 6 ⊢ (𝑦 = 𝑁 → (𝑦 ∈ (1...(#‘𝐴)) ↔ 𝑁 ∈ (1...(#‘𝐴))))
26		fveq2 6191	. . . . . . . 8 ⊢ (𝑦 = 𝑁 → (𝐺‘𝑦) = (𝐺‘𝑁))
27	26	fveq2d 6195	. . . . . . 7 ⊢ (𝑦 = 𝑁 → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq𝑀( + , 𝐹)‘(𝐺‘𝑁)))
28		fveq2 6191	. . . . . . 7 ⊢ (𝑦 = 𝑁 → (seq1( + , 𝐻)‘𝑦) = (seq1( + , 𝐻)‘𝑁))
29	27, 28	eqeq12d 2637	. . . . . 6 ⊢ (𝑦 = 𝑁 → ((seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦) ↔ (seq𝑀( + , 𝐹)‘(𝐺‘𝑁)) = (seq1( + , 𝐻)‘𝑁)))
30	25, 29	imbi12d 334	. . . . 5 ⊢ (𝑦 = 𝑁 → ((𝑦 ∈ (1...(#‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦)) ↔ (𝑁 ∈ (1...(#‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑁)) = (seq1( + , 𝐻)‘𝑁))))
31	30	imbi2d 330	. . . 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 6573	. . . . . . . . . . . . 13 ⊢ (𝐺 Isom < , < ((1...(#‘𝐴)), 𝐴) → 𝐺:(1...(#‘𝐴))–1-1-onto→𝐴)
37	35, 36	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺:(1...(#‘𝐴))–1-1-onto→𝐴)
38		f1of 6137	. . . . . . . . . . . 12 ⊢ (𝐺:(1...(#‘𝐴))–1-1-onto→𝐴 → 𝐺:(1...(#‘𝐴))⟶𝐴)
39	37, 38	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺:(1...(#‘𝐴))⟶𝐴)
40		elfzuz2 12346	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (1...(#‘𝐴)) → (#‘𝐴) ∈ (ℤ_≥‘1))
41	1, 40	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (#‘𝐴) ∈ (ℤ_≥‘1))
42		eluzfz1 12348	. . . . . . . . . . . 12 ⊢ ((#‘𝐴) ∈ (ℤ_≥‘1) → 1 ∈ (1...(#‘𝐴)))
43	41, 42	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ (1...(#‘𝐴)))
44	39, 43	ffvelrnd 6360	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺‘1) ∈ 𝐴)
45	34, 44	sseldd 3604	. . . . . . . . 9 ⊢ (𝜑 → (𝐺‘1) ∈ (ℤ_≥‘𝑀))
46		eluzle 11700	. . . . . . . . . . . . 13 ⊢ ((#‘𝐴) ∈ (ℤ_≥‘1) → 1 ≤ (#‘𝐴))
47	41, 46	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ≤ (#‘𝐴))
48		elfzelz 12342	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (1...(#‘𝐴)) → 𝑘 ∈ ℤ)
49	48	ssriv 3607	. . . . . . . . . . . . . . . 16 ⊢ (1...(#‘𝐴)) ⊆ ℤ
50		zssre 11384	. . . . . . . . . . . . . . . 16 ⊢ ℤ ⊆ ℝ
51	49, 50	sstri 3612	. . . . . . . . . . . . . . 15 ⊢ (1...(#‘𝐴)) ⊆ ℝ
52	51	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1...(#‘𝐴)) ⊆ ℝ)
53		ressxr 10083	. . . . . . . . . . . . . 14 ⊢ ℝ ⊆ ℝ^*
54	52, 53	syl6ss 3615	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1...(#‘𝐴)) ⊆ ℝ^*)
55		eluzelre 11698	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ (ℤ_≥‘𝑀) → 𝑘 ∈ ℝ)
56	55	ssriv 3607	. . . . . . . . . . . . . . 15 ⊢ (ℤ_≥‘𝑀) ⊆ ℝ
57	34, 56	syl6ss 3615	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ⊆ ℝ)
58	57, 53	syl6ss 3615	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ⊆ ℝ^*)
59		eluzfz2 12349	. . . . . . . . . . . . . 14 ⊢ ((#‘𝐴) ∈ (ℤ_≥‘1) → (#‘𝐴) ∈ (1...(#‘𝐴)))
60	41, 59	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (#‘𝐴) ∈ (1...(#‘𝐴)))
61		leisorel 13244	. . . . . . . . . . . . 13 ⊢ ((𝐺 Isom < , < ((1...(#‘𝐴)), 𝐴) ∧ ((1...(#‘𝐴)) ⊆ ℝ^* ∧ 𝐴 ⊆ ℝ^*) ∧ (1 ∈ (1...(#‘𝐴)) ∧ (#‘𝐴) ∈ (1...(#‘𝐴)))) → (1 ≤ (#‘𝐴) ↔ (𝐺‘1) ≤ (𝐺‘(#‘𝐴))))
62	35, 54, 58, 43, 60, 61	syl122anc 1335	. . . . . . . . . . . 12 ⊢ (𝜑 → (1 ≤ (#‘𝐴) ↔ (𝐺‘1) ≤ (𝐺‘(#‘𝐴))))
63	47, 62	mpbid 222	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐺‘1) ≤ (𝐺‘(#‘𝐴)))
64	39, 60	ffvelrnd 6360	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐺‘(#‘𝐴)) ∈ 𝐴)
65	34, 64	sseldd 3604	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐺‘(#‘𝐴)) ∈ (ℤ_≥‘𝑀))
66		eluzelz 11697	. . . . . . . . . . . . 13 ⊢ ((𝐺‘(#‘𝐴)) ∈ (ℤ_≥‘𝑀) → (𝐺‘(#‘𝐴)) ∈ ℤ)
67	65, 66	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐺‘(#‘𝐴)) ∈ ℤ)
68		elfz5 12334	. . . . . . . . . . . 12 ⊢ (((𝐺‘1) ∈ (ℤ_≥‘𝑀) ∧ (𝐺‘(#‘𝐴)) ∈ ℤ) → ((𝐺‘1) ∈ (𝑀...(𝐺‘(#‘𝐴))) ↔ (𝐺‘1) ≤ (𝐺‘(#‘𝐴))))
69	45, 67, 68	syl2anc 693	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐺‘1) ∈ (𝑀...(𝐺‘(#‘𝐴))) ↔ (𝐺‘1) ≤ (𝐺‘(#‘𝐴))))
70	63, 69	mpbird 247	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺‘1) ∈ (𝑀...(𝐺‘(#‘𝐴))))
71		fveq2 6191	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝐺‘1) → (𝐹‘𝑘) = (𝐹‘(𝐺‘1)))
72	71	eleq1d 2686	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝐺‘1) → ((𝐹‘𝑘) ∈ 𝑆 ↔ (𝐹‘(𝐺‘1)) ∈ 𝑆))
73	72	imbi2d 330	. . . . . . . . . . 11 ⊢ (𝑘 = (𝐺‘1) → ((𝜑 → (𝐹‘𝑘) ∈ 𝑆) ↔ (𝜑 → (𝐹‘(𝐺‘1)) ∈ 𝑆)))
74		seqcoll.5	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝐺‘(#‘𝐴)))) → (𝐹‘𝑘) ∈ 𝑆)
75	74	expcom 451	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (𝑀...(𝐺‘(#‘𝐴))) → (𝜑 → (𝐹‘𝑘) ∈ 𝑆))
76	73, 75	vtoclga 3272	. . . . . . . . . 10 ⊢ ((𝐺‘1) ∈ (𝑀...(𝐺‘(#‘𝐴))) → (𝜑 → (𝐹‘(𝐺‘1)) ∈ 𝑆))
77	70, 76	mpcom 38	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘(𝐺‘1)) ∈ 𝑆)
78		eluzelz 11697	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺‘1) ∈ (ℤ_≥‘𝑀) → (𝐺‘1) ∈ ℤ)
79	45, 78	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐺‘1) ∈ ℤ)
80		peano2zm 11420	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺‘1) ∈ ℤ → ((𝐺‘1) − 1) ∈ ℤ)
81	79, 80	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐺‘1) − 1) ∈ ℤ)
82	81	zred 11482	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐺‘1) − 1) ∈ ℝ)
83	79	zred 11482	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐺‘1) ∈ ℝ)
84	67	zred 11482	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐺‘(#‘𝐴)) ∈ ℝ)
85	83	lem1d 10957	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐺‘1) − 1) ≤ (𝐺‘1))
86	82, 83, 84, 85, 63	letrd 10194	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐺‘1) − 1) ≤ (𝐺‘(#‘𝐴)))
87		eluz 11701	. . . . . . . . . . . . . . 15 ⊢ ((((𝐺‘1) − 1) ∈ ℤ ∧ (𝐺‘(#‘𝐴)) ∈ ℤ) → ((𝐺‘(#‘𝐴)) ∈ (ℤ_≥‘((𝐺‘1) − 1)) ↔ ((𝐺‘1) − 1) ≤ (𝐺‘(#‘𝐴))))
88	81, 67, 87	syl2anc 693	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐺‘(#‘𝐴)) ∈ (ℤ_≥‘((𝐺‘1) − 1)) ↔ ((𝐺‘1) − 1) ≤ (𝐺‘(#‘𝐴))))
89	86, 88	mpbird 247	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐺‘(#‘𝐴)) ∈ (ℤ_≥‘((𝐺‘1) − 1)))
90		fzss2 12381	. . . . . . . . . . . . 13 ⊢ ((𝐺‘(#‘𝐴)) ∈ (ℤ_≥‘((𝐺‘1) − 1)) → (𝑀...((𝐺‘1) − 1)) ⊆ (𝑀...(𝐺‘(#‘𝐴))))
91	89, 90	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑀...((𝐺‘1) − 1)) ⊆ (𝑀...(𝐺‘(#‘𝐴))))
92	91	sselda 3603	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...((𝐺‘1) − 1))) → 𝑘 ∈ (𝑀...(𝐺‘(#‘𝐴))))
93		eluzel2 11692	. . . . . . . . . . . . . . 15 ⊢ ((𝐺‘1) ∈ (ℤ_≥‘𝑀) → 𝑀 ∈ ℤ)
94	45, 93	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ∈ ℤ)
95		elfzm11 12411	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℤ ∧ (𝐺‘1) ∈ ℤ) → (𝑘 ∈ (𝑀...((𝐺‘1) − 1)) ↔ (𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 < (𝐺‘1))))
96	94, 79, 95	syl2anc 693	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑘 ∈ (𝑀...((𝐺‘1) − 1)) ↔ (𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 < (𝐺‘1))))
97		simp3 1063	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 < (𝐺‘1)) → 𝑘 < (𝐺‘1))
98		f1ocnv 6149	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐺:(1...(#‘𝐴))–1-1-onto→𝐴 → ^◡𝐺:𝐴–1-1-onto→(1...(#‘𝐴)))
99	37, 98	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ^◡𝐺:𝐴–1-1-onto→(1...(#‘𝐴)))
100		f1of 6137	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (^◡𝐺:𝐴–1-1-onto→(1...(#‘𝐴)) → ^◡𝐺:𝐴⟶(1...(#‘𝐴)))
101	99, 100	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ^◡𝐺:𝐴⟶(1...(#‘𝐴)))
102	101	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (^◡𝐺‘𝑘) ∈ (1...(#‘𝐴)))
103		elfznn 12370	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((^◡𝐺‘𝑘) ∈ (1...(#‘𝐴)) → (^◡𝐺‘𝑘) ∈ ℕ)
104	102, 103	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (^◡𝐺‘𝑘) ∈ ℕ)
105	104	nnge1d 11063	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 1 ≤ (^◡𝐺‘𝑘))
106	35	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐺 Isom < , < ((1...(#‘𝐴)), 𝐴))
107	54	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (1...(#‘𝐴)) ⊆ ℝ^*)
108	58	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐴 ⊆ ℝ^*)
109	43	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 1 ∈ (1...(#‘𝐴)))
110		leisorel 13244	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺 Isom < , < ((1...(#‘𝐴)), 𝐴) ∧ ((1...(#‘𝐴)) ⊆ ℝ^* ∧ 𝐴 ⊆ ℝ^*) ∧ (1 ∈ (1...(#‘𝐴)) ∧ (^◡𝐺‘𝑘) ∈ (1...(#‘𝐴)))) → (1 ≤ (^◡𝐺‘𝑘) ↔ (𝐺‘1) ≤ (𝐺‘(^◡𝐺‘𝑘))))
111	106, 107, 108, 109, 102, 110	syl122anc 1335	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (1 ≤ (^◡𝐺‘𝑘) ↔ (𝐺‘1) ≤ (𝐺‘(^◡𝐺‘𝑘))))
112	105, 111	mpbid 222	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐺‘1) ≤ (𝐺‘(^◡𝐺‘𝑘)))
113		f1ocnvfv2 6533	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺:(1...(#‘𝐴))–1-1-onto→𝐴 ∧ 𝑘 ∈ 𝐴) → (𝐺‘(^◡𝐺‘𝑘)) = 𝑘)
114	37, 113	sylan 488	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐺‘(^◡𝐺‘𝑘)) = 𝑘)
115	112, 114	breqtrd 4679	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐺‘1) ≤ 𝑘)
116	83	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐺‘1) ∈ ℝ)
117	57	sselda 3603	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑘 ∈ ℝ)
118	116, 117	lenltd 10183	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝐺‘1) ≤ 𝑘 ↔ ¬ 𝑘 < (𝐺‘1)))
119	115, 118	mpbid 222	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ¬ 𝑘 < (𝐺‘1))
120	119	ex 450	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑘 ∈ 𝐴 → ¬ 𝑘 < (𝐺‘1)))
121	120	con2d 129	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑘 < (𝐺‘1) → ¬ 𝑘 ∈ 𝐴))
122	97, 121	syl5 34	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 < (𝐺‘1)) → ¬ 𝑘 ∈ 𝐴))
123	96, 122	sylbid 230	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑘 ∈ (𝑀...((𝐺‘1) − 1)) → ¬ 𝑘 ∈ 𝐴))
124	123	imp 445	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...((𝐺‘1) − 1))) → ¬ 𝑘 ∈ 𝐴)
125	92, 124	eldifd 3585	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...((𝐺‘1) − 1))) → 𝑘 ∈ ((𝑀...(𝐺‘(#‘𝐴))) ∖ 𝐴))
126		seqcoll.6	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀...(𝐺‘(#‘𝐴))) ∖ 𝐴)) → (𝐹‘𝑘) = 𝑍)
127	125, 126	syldan 487	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...((𝐺‘1) − 1))) → (𝐹‘𝑘) = 𝑍)
128	32, 33, 45, 77, 127	seqid 12846	. . . . . . . 8 ⊢ (𝜑 → (seq𝑀( + , 𝐹) ↾ (ℤ_≥‘(𝐺‘1))) = seq(𝐺‘1)( + , 𝐹))
129	128	fveq1d 6193	. . . . . . 7 ⊢ (𝜑 → ((seq𝑀( + , 𝐹) ↾ (ℤ_≥‘(𝐺‘1)))‘(𝐺‘1)) = (seq(𝐺‘1)( + , 𝐹)‘(𝐺‘1)))
130		uzid 11702	. . . . . . . . 9 ⊢ ((𝐺‘1) ∈ ℤ → (𝐺‘1) ∈ (ℤ_≥‘(𝐺‘1)))
131	79, 130	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝐺‘1) ∈ (ℤ_≥‘(𝐺‘1)))
132		fvres 6207	. . . . . . . 8 ⊢ ((𝐺‘1) ∈ (ℤ_≥‘(𝐺‘1)) → ((seq𝑀( + , 𝐹) ↾ (ℤ_≥‘(𝐺‘1)))‘(𝐺‘1)) = (seq𝑀( + , 𝐹)‘(𝐺‘1)))
133	131, 132	syl 17	. . . . . . 7 ⊢ (𝜑 → ((seq𝑀( + , 𝐹) ↾ (ℤ_≥‘(𝐺‘1)))‘(𝐺‘1)) = (seq𝑀( + , 𝐹)‘(𝐺‘1)))
134		seq1 12814	. . . . . . . . 9 ⊢ ((𝐺‘1) ∈ ℤ → (seq(𝐺‘1)( + , 𝐹)‘(𝐺‘1)) = (𝐹‘(𝐺‘1)))
135	79, 134	syl 17	. . . . . . . 8 ⊢ (𝜑 → (seq(𝐺‘1)( + , 𝐹)‘(𝐺‘1)) = (𝐹‘(𝐺‘1)))
136		fveq2 6191	. . . . . . . . . . . 12 ⊢ (𝑛 = 1 → (𝐻‘𝑛) = (𝐻‘1))
137		fveq2 6191	. . . . . . . . . . . . 13 ⊢ (𝑛 = 1 → (𝐺‘𝑛) = (𝐺‘1))
138	137	fveq2d 6195	. . . . . . . . . . . 12 ⊢ (𝑛 = 1 → (𝐹‘(𝐺‘𝑛)) = (𝐹‘(𝐺‘1)))
139	136, 138	eqeq12d 2637	. . . . . . . . . . 11 ⊢ (𝑛 = 1 → ((𝐻‘𝑛) = (𝐹‘(𝐺‘𝑛)) ↔ (𝐻‘1) = (𝐹‘(𝐺‘1))))
140	139	imbi2d 330	. . . . . . . . . 10 ⊢ (𝑛 = 1 → ((𝜑 → (𝐻‘𝑛) = (𝐹‘(𝐺‘𝑛))) ↔ (𝜑 → (𝐻‘1) = (𝐹‘(𝐺‘1)))))
141		seqcoll.7	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(#‘𝐴))) → (𝐻‘𝑛) = (𝐹‘(𝐺‘𝑛)))
142	141	expcom 451	. . . . . . . . . 10 ⊢ (𝑛 ∈ (1...(#‘𝐴)) → (𝜑 → (𝐻‘𝑛) = (𝐹‘(𝐺‘𝑛))))
143	140, 142	vtoclga 3272	. . . . . . . . 9 ⊢ (1 ∈ (1...(#‘𝐴)) → (𝜑 → (𝐻‘1) = (𝐹‘(𝐺‘1))))
144	43, 143	mpcom 38	. . . . . . . 8 ⊢ (𝜑 → (𝐻‘1) = (𝐹‘(𝐺‘1)))
145	135, 144	eqtr4d 2659	. . . . . . 7 ⊢ (𝜑 → (seq(𝐺‘1)( + , 𝐹)‘(𝐺‘1)) = (𝐻‘1))
146	129, 133, 145	3eqtr3d 2664	. . . . . 6 ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘(𝐺‘1)) = (𝐻‘1))
147		1z 11407	. . . . . . 7 ⊢ 1 ∈ ℤ
148		seq1 12814	. . . . . . 7 ⊢ (1 ∈ ℤ → (seq1( + , 𝐻)‘1) = (𝐻‘1))
149	147, 148	ax-mp 5	. . . . . 6 ⊢ (seq1( + , 𝐻)‘1) = (𝐻‘1)
150	146, 149	syl6eqr 2674	. . . . 5 ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘(𝐺‘1)) = (seq1( + , 𝐻)‘1))
151	150	a1d 25	. . . 4 ⊢ (𝜑 → (1 ∈ (1...(#‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘1)) = (seq1( + , 𝐻)‘1)))
152		simplr 792	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → 𝑚 ∈ ℕ)
153		nnuz 11723	. . . . . . . . . . 11 ⊢ ℕ = (ℤ_≥‘1)
154	152, 153	syl6eleq 2711	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → 𝑚 ∈ (ℤ_≥‘1))
155		nnz 11399	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℤ)
156	155	ad2antlr 763	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → 𝑚 ∈ ℤ)
157		elfzuz3 12339	. . . . . . . . . . . 12 ⊢ ((𝑚 + 1) ∈ (1...(#‘𝐴)) → (#‘𝐴) ∈ (ℤ_≥‘(𝑚 + 1)))
158	157	adantl 482	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (#‘𝐴) ∈ (ℤ_≥‘(𝑚 + 1)))
159		peano2uzr 11743	. . . . . . . . . . 11 ⊢ ((𝑚 ∈ ℤ ∧ (#‘𝐴) ∈ (ℤ_≥‘(𝑚 + 1))) → (#‘𝐴) ∈ (ℤ_≥‘𝑚))
160	156, 158, 159	syl2anc 693	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (#‘𝐴) ∈ (ℤ_≥‘𝑚))
161		elfzuzb 12336	. . . . . . . . . 10 ⊢ (𝑚 ∈ (1...(#‘𝐴)) ↔ (𝑚 ∈ (ℤ_≥‘1) ∧ (#‘𝐴) ∈ (ℤ_≥‘𝑚)))
162	154, 160, 161	sylanbrc 698	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → 𝑚 ∈ (1...(#‘𝐴)))
163	162	ex 450	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑚 + 1) ∈ (1...(#‘𝐴)) → 𝑚 ∈ (1...(#‘𝐴))))
164	163	imim1d 82	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑚 ∈ (1...(#‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq1( + , 𝐻)‘𝑚)) → ((𝑚 + 1) ∈ (1...(#‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq1( + , 𝐻)‘𝑚))))
165		oveq1 6657	. . . . . . . . . 10 ⊢ ((seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq1( + , 𝐻)‘𝑚) → ((seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) + (𝐻‘(𝑚 + 1))) = ((seq1( + , 𝐻)‘𝑚) + (𝐻‘(𝑚 + 1))))
166		simpll 790	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → 𝜑)
167		seqcoll.1b	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑆) → (𝑘 + 𝑍) = 𝑘)
168	166, 167	sylan 488	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) ∧ 𝑘 ∈ 𝑆) → (𝑘 + 𝑍) = 𝑘)
169	34	ad2antrr 762	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → 𝐴 ⊆ (ℤ_≥‘𝑀))
170	39	ad2antrr 762	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → 𝐺:(1...(#‘𝐴))⟶𝐴)
171	170, 162	ffvelrnd 6360	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (𝐺‘𝑚) ∈ 𝐴)
172	169, 171	sseldd 3604	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (𝐺‘𝑚) ∈ (ℤ_≥‘𝑀))
173		nnre 11027	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℝ)
174	173	ad2antlr 763	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → 𝑚 ∈ ℝ)
175	174	ltp1d 10954	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → 𝑚 < (𝑚 + 1))
176	35	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → 𝐺 Isom < , < ((1...(#‘𝐴)), 𝐴))
177		simpr 477	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (𝑚 + 1) ∈ (1...(#‘𝐴)))
178		isorel 6576	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺 Isom < , < ((1...(#‘𝐴)), 𝐴) ∧ (𝑚 ∈ (1...(#‘𝐴)) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴)))) → (𝑚 < (𝑚 + 1) ↔ (𝐺‘𝑚) < (𝐺‘(𝑚 + 1))))
179	176, 162, 177, 178	syl12anc 1324	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (𝑚 < (𝑚 + 1) ↔ (𝐺‘𝑚) < (𝐺‘(𝑚 + 1))))
180	175, 179	mpbid 222	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (𝐺‘𝑚) < (𝐺‘(𝑚 + 1)))
181		eluzelz 11697	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺‘𝑚) ∈ (ℤ_≥‘𝑀) → (𝐺‘𝑚) ∈ ℤ)
182	172, 181	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (𝐺‘𝑚) ∈ ℤ)
183	170, 177	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (𝐺‘(𝑚 + 1)) ∈ 𝐴)
184	169, 183	sseldd 3604	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (𝐺‘(𝑚 + 1)) ∈ (ℤ_≥‘𝑀))
185		eluzelz 11697	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺‘(𝑚 + 1)) ∈ (ℤ_≥‘𝑀) → (𝐺‘(𝑚 + 1)) ∈ ℤ)
186	184, 185	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (𝐺‘(𝑚 + 1)) ∈ ℤ)
187		zltlem1 11430	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐺‘𝑚) ∈ ℤ ∧ (𝐺‘(𝑚 + 1)) ∈ ℤ) → ((𝐺‘𝑚) < (𝐺‘(𝑚 + 1)) ↔ (𝐺‘𝑚) ≤ ((𝐺‘(𝑚 + 1)) − 1)))
188	182, 186, 187	syl2anc 693	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → ((𝐺‘𝑚) < (𝐺‘(𝑚 + 1)) ↔ (𝐺‘𝑚) ≤ ((𝐺‘(𝑚 + 1)) − 1)))
189	180, 188	mpbid 222	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (𝐺‘𝑚) ≤ ((𝐺‘(𝑚 + 1)) − 1))
190		peano2zm 11420	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺‘(𝑚 + 1)) ∈ ℤ → ((𝐺‘(𝑚 + 1)) − 1) ∈ ℤ)
191	186, 190	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → ((𝐺‘(𝑚 + 1)) − 1) ∈ ℤ)
192		eluz 11701	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺‘𝑚) ∈ ℤ ∧ ((𝐺‘(𝑚 + 1)) − 1) ∈ ℤ) → (((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ_≥‘(𝐺‘𝑚)) ↔ (𝐺‘𝑚) ≤ ((𝐺‘(𝑚 + 1)) − 1)))
193	182, 191, 192	syl2anc 693	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ_≥‘(𝐺‘𝑚)) ↔ (𝐺‘𝑚) ≤ ((𝐺‘(𝑚 + 1)) − 1)))
194	189, 193	mpbird 247	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → ((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ_≥‘(𝐺‘𝑚)))
195	191	zred 11482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → ((𝐺‘(𝑚 + 1)) − 1) ∈ ℝ)
196	186	zred 11482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (𝐺‘(𝑚 + 1)) ∈ ℝ)
197	84	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (𝐺‘(#‘𝐴)) ∈ ℝ)
198	196	lem1d 10957	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → ((𝐺‘(𝑚 + 1)) − 1) ≤ (𝐺‘(𝑚 + 1)))
199		elfzle2 12345	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑚 + 1) ∈ (1...(#‘𝐴)) → (𝑚 + 1) ≤ (#‘𝐴))
200	199	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (𝑚 + 1) ≤ (#‘𝐴))
201	54	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (1...(#‘𝐴)) ⊆ ℝ^*)
202	58	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → 𝐴 ⊆ ℝ^*)
203	60	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (#‘𝐴) ∈ (1...(#‘𝐴)))
204		leisorel 13244	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐺 Isom < , < ((1...(#‘𝐴)), 𝐴) ∧ ((1...(#‘𝐴)) ⊆ ℝ^* ∧ 𝐴 ⊆ ℝ^*) ∧ ((𝑚 + 1) ∈ (1...(#‘𝐴)) ∧ (#‘𝐴) ∈ (1...(#‘𝐴)))) → ((𝑚 + 1) ≤ (#‘𝐴) ↔ (𝐺‘(𝑚 + 1)) ≤ (𝐺‘(#‘𝐴))))
205	176, 201, 202, 177, 203, 204	syl122anc 1335	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → ((𝑚 + 1) ≤ (#‘𝐴) ↔ (𝐺‘(𝑚 + 1)) ≤ (𝐺‘(#‘𝐴))))
206	200, 205	mpbid 222	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (𝐺‘(𝑚 + 1)) ≤ (𝐺‘(#‘𝐴)))
207	195, 196, 197, 198, 206	letrd 10194	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → ((𝐺‘(𝑚 + 1)) − 1) ≤ (𝐺‘(#‘𝐴)))
208	67	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (𝐺‘(#‘𝐴)) ∈ ℤ)
209		eluz 11701	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐺‘(𝑚 + 1)) − 1) ∈ ℤ ∧ (𝐺‘(#‘𝐴)) ∈ ℤ) → ((𝐺‘(#‘𝐴)) ∈ (ℤ_≥‘((𝐺‘(𝑚 + 1)) − 1)) ↔ ((𝐺‘(𝑚 + 1)) − 1) ≤ (𝐺‘(#‘𝐴))))
210	191, 208, 209	syl2anc 693	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → ((𝐺‘(#‘𝐴)) ∈ (ℤ_≥‘((𝐺‘(𝑚 + 1)) − 1)) ↔ ((𝐺‘(𝑚 + 1)) − 1) ≤ (𝐺‘(#‘𝐴))))
211	207, 210	mpbird 247	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (𝐺‘(#‘𝐴)) ∈ (ℤ_≥‘((𝐺‘(𝑚 + 1)) − 1)))
212		uztrn 11704	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐺‘(#‘𝐴)) ∈ (ℤ_≥‘((𝐺‘(𝑚 + 1)) − 1)) ∧ ((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ_≥‘(𝐺‘𝑚))) → (𝐺‘(#‘𝐴)) ∈ (ℤ_≥‘(𝐺‘𝑚)))
213	211, 194, 212	syl2anc 693	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (𝐺‘(#‘𝐴)) ∈ (ℤ_≥‘(𝐺‘𝑚)))
214		fzss2 12381	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺‘(#‘𝐴)) ∈ (ℤ_≥‘(𝐺‘𝑚)) → (𝑀...(𝐺‘𝑚)) ⊆ (𝑀...(𝐺‘(#‘𝐴))))
215	213, 214	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (𝑀...(𝐺‘𝑚)) ⊆ (𝑀...(𝐺‘(#‘𝐴))))
216	215	sselda 3603	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) ∧ 𝑘 ∈ (𝑀...(𝐺‘𝑚))) → 𝑘 ∈ (𝑀...(𝐺‘(#‘𝐴))))
217	166, 74	sylan 488	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) ∧ 𝑘 ∈ (𝑀...(𝐺‘(#‘𝐴)))) → (𝐹‘𝑘) ∈ 𝑆)
218	216, 217	syldan 487	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) ∧ 𝑘 ∈ (𝑀...(𝐺‘𝑚))) → (𝐹‘𝑘) ∈ 𝑆)
219		seqcoll.c	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑘 ∈ 𝑆 ∧ 𝑛 ∈ 𝑆)) → (𝑘 + 𝑛) ∈ 𝑆)
220	166, 219	sylan 488	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) ∧ (𝑘 ∈ 𝑆 ∧ 𝑛 ∈ 𝑆)) → (𝑘 + 𝑛) ∈ 𝑆)
221	172, 218, 220	seqcl 12821	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) ∈ 𝑆)
222		simplll 798	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) ∧ 𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1))) → 𝜑)
223		elfzuz 12338	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1)) → 𝑘 ∈ (ℤ_≥‘((𝐺‘𝑚) + 1)))
224		peano2uz 11741	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺‘𝑚) ∈ (ℤ_≥‘𝑀) → ((𝐺‘𝑚) + 1) ∈ (ℤ_≥‘𝑀))
225	172, 224	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → ((𝐺‘𝑚) + 1) ∈ (ℤ_≥‘𝑀))
226		uztrn 11704	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ (ℤ_≥‘((𝐺‘𝑚) + 1)) ∧ ((𝐺‘𝑚) + 1) ∈ (ℤ_≥‘𝑀)) → 𝑘 ∈ (ℤ_≥‘𝑀))
227	223, 225, 226	syl2anr 495	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) ∧ 𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1))) → 𝑘 ∈ (ℤ_≥‘𝑀))
228		elfzuz3 12339	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1)) → ((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ_≥‘𝑘))
229		uztrn 11704	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐺‘(#‘𝐴)) ∈ (ℤ_≥‘((𝐺‘(𝑚 + 1)) − 1)) ∧ ((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ_≥‘𝑘)) → (𝐺‘(#‘𝐴)) ∈ (ℤ_≥‘𝑘))
230	211, 228, 229	syl2an 494	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) ∧ 𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1))) → (𝐺‘(#‘𝐴)) ∈ (ℤ_≥‘𝑘))
231		elfzuzb 12336	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (𝑀...(𝐺‘(#‘𝐴))) ↔ (𝑘 ∈ (ℤ_≥‘𝑀) ∧ (𝐺‘(#‘𝐴)) ∈ (ℤ_≥‘𝑘)))
232	227, 230, 231	sylanbrc 698	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) ∧ 𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1))) → 𝑘 ∈ (𝑀...(𝐺‘(#‘𝐴))))
233		elfzle1 12344	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1)) → ((𝐺‘𝑚) + 1) ≤ 𝑘)
234		elfzle2 12345	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1)) → 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1))
235	233, 234	jca 554	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1)) → (((𝐺‘𝑚) + 1) ≤ 𝑘 ∧ 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1)))
236	155	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(#‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → 𝑚 ∈ ℤ)
237	101	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(#‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → ^◡𝐺:𝐴⟶(1...(#‘𝐴)))
238		simprr 796	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(#‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → 𝑘 ∈ 𝐴)
239	237, 238	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(#‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → (^◡𝐺‘𝑘) ∈ (1...(#‘𝐴)))
240		elfzelz 12342	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((^◡𝐺‘𝑘) ∈ (1...(#‘𝐴)) → (^◡𝐺‘𝑘) ∈ ℤ)
241	239, 240	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(#‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → (^◡𝐺‘𝑘) ∈ ℤ)
242		btwnnz 11453	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑚 ∈ ℤ ∧ 𝑚 < (^◡𝐺‘𝑘) ∧ (^◡𝐺‘𝑘) < (𝑚 + 1)) → ¬ (^◡𝐺‘𝑘) ∈ ℤ)
243	242	3expib 1268	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑚 ∈ ℤ → ((𝑚 < (^◡𝐺‘𝑘) ∧ (^◡𝐺‘𝑘) < (𝑚 + 1)) → ¬ (^◡𝐺‘𝑘) ∈ ℤ))
244	243	con2d 129	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 ∈ ℤ → ((^◡𝐺‘𝑘) ∈ ℤ → ¬ (𝑚 < (^◡𝐺‘𝑘) ∧ (^◡𝐺‘𝑘) < (𝑚 + 1))))
245	236, 241, 244	sylc 65	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(#‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → ¬ (𝑚 < (^◡𝐺‘𝑘) ∧ (^◡𝐺‘𝑘) < (𝑚 + 1)))
246	35	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(#‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → 𝐺 Isom < , < ((1...(#‘𝐴)), 𝐴))
247	162	adantrr 753	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(#‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → 𝑚 ∈ (1...(#‘𝐴)))
248		isorel 6576	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐺 Isom < , < ((1...(#‘𝐴)), 𝐴) ∧ (𝑚 ∈ (1...(#‘𝐴)) ∧ (^◡𝐺‘𝑘) ∈ (1...(#‘𝐴)))) → (𝑚 < (^◡𝐺‘𝑘) ↔ (𝐺‘𝑚) < (𝐺‘(^◡𝐺‘𝑘))))
249	246, 247, 239, 248	syl12anc 1324	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(#‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → (𝑚 < (^◡𝐺‘𝑘) ↔ (𝐺‘𝑚) < (𝐺‘(^◡𝐺‘𝑘))))
250	37	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(#‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → 𝐺:(1...(#‘𝐴))–1-1-onto→𝐴)
251	250, 238, 113	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(#‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → (𝐺‘(^◡𝐺‘𝑘)) = 𝑘)
252	251	breq2d 4665	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(#‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → ((𝐺‘𝑚) < (𝐺‘(^◡𝐺‘𝑘)) ↔ (𝐺‘𝑚) < 𝑘))
253	182	adantrr 753	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(#‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → (𝐺‘𝑚) ∈ ℤ)
254	34	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(#‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → 𝐴 ⊆ (ℤ_≥‘𝑀))
255	254, 238	sseldd 3604	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(#‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → 𝑘 ∈ (ℤ_≥‘𝑀))
256		eluzelz 11697	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 ∈ (ℤ_≥‘𝑀) → 𝑘 ∈ ℤ)
257	255, 256	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(#‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → 𝑘 ∈ ℤ)
258		zltp1le 11427	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐺‘𝑚) ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((𝐺‘𝑚) < 𝑘 ↔ ((𝐺‘𝑚) + 1) ≤ 𝑘))
259	253, 257, 258	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(#‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → ((𝐺‘𝑚) < 𝑘 ↔ ((𝐺‘𝑚) + 1) ≤ 𝑘))
260	249, 252, 259	3bitrd 294	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(#‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → (𝑚 < (^◡𝐺‘𝑘) ↔ ((𝐺‘𝑚) + 1) ≤ 𝑘))
261	177	adantrr 753	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(#‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → (𝑚 + 1) ∈ (1...(#‘𝐴)))
262		isorel 6576	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐺 Isom < , < ((1...(#‘𝐴)), 𝐴) ∧ ((^◡𝐺‘𝑘) ∈ (1...(#‘𝐴)) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴)))) → ((^◡𝐺‘𝑘) < (𝑚 + 1) ↔ (𝐺‘(^◡𝐺‘𝑘)) < (𝐺‘(𝑚 + 1))))
263	246, 239, 261, 262	syl12anc 1324	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(#‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → ((^◡𝐺‘𝑘) < (𝑚 + 1) ↔ (𝐺‘(^◡𝐺‘𝑘)) < (𝐺‘(𝑚 + 1))))
264	251	breq1d 4663	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(#‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → ((𝐺‘(^◡𝐺‘𝑘)) < (𝐺‘(𝑚 + 1)) ↔ 𝑘 < (𝐺‘(𝑚 + 1))))
265	186	adantrr 753	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(#‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → (𝐺‘(𝑚 + 1)) ∈ ℤ)
266		zltlem1 11430	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑘 ∈ ℤ ∧ (𝐺‘(𝑚 + 1)) ∈ ℤ) → (𝑘 < (𝐺‘(𝑚 + 1)) ↔ 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1)))
267	257, 265, 266	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(#‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → (𝑘 < (𝐺‘(𝑚 + 1)) ↔ 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1)))
268	263, 264, 267	3bitrd 294	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(#‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → ((^◡𝐺‘𝑘) < (𝑚 + 1) ↔ 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1)))
269	260, 268	anbi12d 747	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(#‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → ((𝑚 < (^◡𝐺‘𝑘) ∧ (^◡𝐺‘𝑘) < (𝑚 + 1)) ↔ (((𝐺‘𝑚) + 1) ≤ 𝑘 ∧ 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1))))
270	245, 269	mtbid 314	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(#‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → ¬ (((𝐺‘𝑚) + 1) ≤ 𝑘 ∧ 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1)))
271	270	expr 643	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (𝑘 ∈ 𝐴 → ¬ (((𝐺‘𝑚) + 1) ≤ 𝑘 ∧ 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1))))
272	271	con2d 129	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → ((((𝐺‘𝑚) + 1) ≤ 𝑘 ∧ 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1)) → ¬ 𝑘 ∈ 𝐴))
273	235, 272	syl5 34	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1)) → ¬ 𝑘 ∈ 𝐴))
274	273	imp 445	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) ∧ 𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1))) → ¬ 𝑘 ∈ 𝐴)
275	232, 274	eldifd 3585	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) ∧ 𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1))) → 𝑘 ∈ ((𝑀...(𝐺‘(#‘𝐴))) ∖ 𝐴))
276	222, 275, 126	syl2anc 693	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) ∧ 𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1))) → (𝐹‘𝑘) = 𝑍)
277	168, 172, 194, 221, 276	seqid2 12847	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq𝑀( + , 𝐹)‘((𝐺‘(𝑚 + 1)) − 1)))
278	277	oveq1d 6665	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → ((seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) + (𝐹‘(𝐺‘(𝑚 + 1)))) = ((seq𝑀( + , 𝐹)‘((𝐺‘(𝑚 + 1)) − 1)) + (𝐹‘(𝐺‘(𝑚 + 1)))))
279		fveq2 6191	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = (𝑚 + 1) → (𝐻‘𝑛) = (𝐻‘(𝑚 + 1)))
280		fveq2 6191	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = (𝑚 + 1) → (𝐺‘𝑛) = (𝐺‘(𝑚 + 1)))
281	280	fveq2d 6195	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = (𝑚 + 1) → (𝐹‘(𝐺‘𝑛)) = (𝐹‘(𝐺‘(𝑚 + 1))))
282	279, 281	eqeq12d 2637	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = (𝑚 + 1) → ((𝐻‘𝑛) = (𝐹‘(𝐺‘𝑛)) ↔ (𝐻‘(𝑚 + 1)) = (𝐹‘(𝐺‘(𝑚 + 1)))))
283	282	imbi2d 330	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = (𝑚 + 1) → ((𝜑 → (𝐻‘𝑛) = (𝐹‘(𝐺‘𝑛))) ↔ (𝜑 → (𝐻‘(𝑚 + 1)) = (𝐹‘(𝐺‘(𝑚 + 1))))))
284	283, 142	vtoclga 3272	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 + 1) ∈ (1...(#‘𝐴)) → (𝜑 → (𝐻‘(𝑚 + 1)) = (𝐹‘(𝐺‘(𝑚 + 1)))))
285	284	impcom 446	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (𝐻‘(𝑚 + 1)) = (𝐹‘(𝐺‘(𝑚 + 1))))
286	285	adantlr 751	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (𝐻‘(𝑚 + 1)) = (𝐹‘(𝐺‘(𝑚 + 1))))
287	286	oveq2d 6666	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → ((seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) + (𝐻‘(𝑚 + 1))) = ((seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) + (𝐹‘(𝐺‘(𝑚 + 1)))))
288	94	ad2antrr 762	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → 𝑀 ∈ ℤ)
289	186	zcnd 11483	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (𝐺‘(𝑚 + 1)) ∈ ℂ)
290		ax-1cn 9994	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
291		npcan 10290	. . . . . . . . . . . . . . 15 ⊢ (((𝐺‘(𝑚 + 1)) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝐺‘(𝑚 + 1)) − 1) + 1) = (𝐺‘(𝑚 + 1)))
292	289, 290, 291	sylancl 694	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (((𝐺‘(𝑚 + 1)) − 1) + 1) = (𝐺‘(𝑚 + 1)))
293		uztrn 11704	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ_≥‘(𝐺‘𝑚)) ∧ (𝐺‘𝑚) ∈ (ℤ_≥‘𝑀)) → ((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ_≥‘𝑀))
294	194, 172, 293	syl2anc 693	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → ((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ_≥‘𝑀))
295		eluzp1p1 11713	. . . . . . . . . . . . . . 15 ⊢ (((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ_≥‘𝑀) → (((𝐺‘(𝑚 + 1)) − 1) + 1) ∈ (ℤ_≥‘(𝑀 + 1)))
296	294, 295	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (((𝐺‘(𝑚 + 1)) − 1) + 1) ∈ (ℤ_≥‘(𝑀 + 1)))
297	292, 296	eqeltrrd 2702	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (𝐺‘(𝑚 + 1)) ∈ (ℤ_≥‘(𝑀 + 1)))
298		seqm1 12818	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℤ ∧ (𝐺‘(𝑚 + 1)) ∈ (ℤ_≥‘(𝑀 + 1))) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = ((seq𝑀( + , 𝐹)‘((𝐺‘(𝑚 + 1)) − 1)) + (𝐹‘(𝐺‘(𝑚 + 1)))))
299	288, 297, 298	syl2anc 693	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = ((seq𝑀( + , 𝐹)‘((𝐺‘(𝑚 + 1)) − 1)) + (𝐹‘(𝐺‘(𝑚 + 1)))))
300	278, 287, 299	3eqtr4rd 2667	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = ((seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) + (𝐻‘(𝑚 + 1))))
301		seqp1 12816	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ (ℤ_≥‘1) → (seq1( + , 𝐻)‘(𝑚 + 1)) = ((seq1( + , 𝐻)‘𝑚) + (𝐻‘(𝑚 + 1))))
302	154, 301	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → (seq1( + , 𝐻)‘(𝑚 + 1)) = ((seq1( + , 𝐻)‘𝑚) + (𝐻‘(𝑚 + 1))))
303	300, 302	eqeq12d 2637	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → ((seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1)) ↔ ((seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) + (𝐻‘(𝑚 + 1))) = ((seq1( + , 𝐻)‘𝑚) + (𝐻‘(𝑚 + 1)))))
304	165, 303	syl5ibr 236	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(#‘𝐴))) → ((seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq1( + , 𝐻)‘𝑚) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1))))
305	304	ex 450	. . . . . . . 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 47	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑚 ∈ (1...(#‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq1( + , 𝐻)‘𝑚)) → ((𝑚 + 1) ∈ (1...(#‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1)))))
308	307	expcom 451	. . . . 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 11038	. . 3 ⊢ (𝑁 ∈ ℕ → (𝜑 → (𝑁 ∈ (1...(#‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑁)) = (seq1( + , 𝐻)‘𝑁))))
311	3, 310	mpcom 38	. 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 196 ∧ wa 384 ∧ w3a 1037 = wceq 1483 ∈ wcel 1990 ∖ cdif 3571 ⊆ wss 3574 class class class wbr 4653 ^◡ccnv 5113 ↾ cres 5116 ⟶wf 5884 –1-1-onto→wf1o 5887 ‘cfv 5888 Isom wiso 5889 (class class class)co 6650 ℂcc 9934 ℝcr 9935 1c1 9937 + caddc 9939 ℝ^*cxr 10073 < clt 10074 ≤ cle 10075 − cmin 10266 ℕcn 11020 ℤcz 11377 ℤ_≥cuz 11687 ...cfz 12326 seqcseq 12801 #chash 13117

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-er 7742 df-en 7956 df-dom 7957 df-sdom 7958 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-nn 11021 df-n0 11293 df-z 11378 df-uz 11688 df-fz 12327 df-seq 12802

This theorem is referenced by: seqcoll2 13249 summolem2a 14446 prodmolem2a 14664

W3C validator