seq3coll - Intuitionistic Logic Explorer

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

Theorem seq3coll 10777

Description: The function 𝐹 contains a sparse set of nonzero values to be summed. The function 𝐺 is an order isomorphism from the set of nonzero values of 𝐹 to a 1-based finite sequence, and 𝐻 collects these nonzero values together. Under these conditions, the sum over the values in 𝐻 yields the same result as the sum over the original set 𝐹. (Contributed by Mario Carneiro, 2-Apr-2014.) (Revised by Jim Kingdon, 9-Apr-2023.)

**Hypotheses**
Ref	Expression
seqcoll.1	⊢ ((𝜑 ∧ 𝑘 ∈ 𝑆) → (𝑍 + 𝑘) = 𝑘)
seqcoll.1b	⊢ ((𝜑 ∧ 𝑘 ∈ 𝑆) → (𝑘 + 𝑍) = 𝑘)
seqcoll.c	⊢ ((𝜑 ∧ (𝑘 ∈ 𝑆 ∧ 𝑛 ∈ 𝑆)) → (𝑘 + 𝑛) ∈ 𝑆)
seqcoll.a	⊢ (𝜑 → 𝑍 ∈ 𝑆)
seqcoll.2	⊢ (𝜑 → 𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴))
seqcoll.3	⊢ (𝜑 → 𝑁 ∈ (1...(♯‘𝐴)))
seqcoll.4	⊢ (𝜑 → 𝐴 ⊆ (ℤ_≥‘𝑀))
seqcoll.5	⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑀)) → (𝐹‘𝑘) ∈ 𝑆)
seqcoll.hcl	⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘1)) → (𝐻‘𝑘) ∈ 𝑆)
seqcoll.6	⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀...(𝐺‘(♯‘𝐴))) ∖ 𝐴)) → (𝐹‘𝑘) = 𝑍)
seqcoll.7	⊢ ((𝜑 ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (𝐻‘𝑛) = (𝐹‘(𝐺‘𝑛)))

**Assertion**
Ref	Expression
seq3coll	⊢ (𝜑 → (seq𝑀( + , 𝐹)‘(𝐺‘𝑁)) = (seq1( + , 𝐻)‘𝑁))

Distinct variable groups: 𝑘,𝑛,𝐴 𝑘,𝐹,𝑛 𝑘,𝐺,𝑛 𝑘,𝐻,𝑛 𝑘,𝑀,𝑛 + ,𝑘,𝑛 𝜑,𝑘,𝑛 𝑆,𝑘,𝑛 𝑘,𝑍,𝑛 Allowed substitution hints: 𝑁(𝑘,𝑛)

Proof of Theorem seq3coll Dummy variables 𝑚 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		seqcoll.3	. 2 ⊢ (𝜑 → 𝑁 ∈ (1...(♯‘𝐴)))
2		elfznn 10010	. . . 4 ⊢ (𝑁 ∈ (1...(♯‘𝐴)) → 𝑁 ∈ ℕ)
3	1, 2	syl 14	. . 3 ⊢ (𝜑 → 𝑁 ∈ ℕ)
4		eleq1 2233	. . . . . 6 ⊢ (𝑦 = 1 → (𝑦 ∈ (1...(♯‘𝐴)) ↔ 1 ∈ (1...(♯‘𝐴))))
5		2fveq3 5501	. . . . . . 7 ⊢ (𝑦 = 1 → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq𝑀( + , 𝐹)‘(𝐺‘1)))
6		fveq2 5496	. . . . . . 7 ⊢ (𝑦 = 1 → (seq1( + , 𝐻)‘𝑦) = (seq1( + , 𝐻)‘1))
7	5, 6	eqeq12d 2185	. . . . . 6 ⊢ (𝑦 = 1 → ((seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦) ↔ (seq𝑀( + , 𝐹)‘(𝐺‘1)) = (seq1( + , 𝐻)‘1)))
8	4, 7	imbi12d 233	. . . . 5 ⊢ (𝑦 = 1 → ((𝑦 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦)) ↔ (1 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘1)) = (seq1( + , 𝐻)‘1))))
9	8	imbi2d 229	. . . 4 ⊢ (𝑦 = 1 → ((𝜑 → (𝑦 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦))) ↔ (𝜑 → (1 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘1)) = (seq1( + , 𝐻)‘1)))))
10		eleq1 2233	. . . . . 6 ⊢ (𝑦 = 𝑚 → (𝑦 ∈ (1...(♯‘𝐴)) ↔ 𝑚 ∈ (1...(♯‘𝐴))))
11		2fveq3 5501	. . . . . . 7 ⊢ (𝑦 = 𝑚 → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)))
12		fveq2 5496	. . . . . . 7 ⊢ (𝑦 = 𝑚 → (seq1( + , 𝐻)‘𝑦) = (seq1( + , 𝐻)‘𝑚))
13	11, 12	eqeq12d 2185	. . . . . 6 ⊢ (𝑦 = 𝑚 → ((seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦) ↔ (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq1( + , 𝐻)‘𝑚)))
14	10, 13	imbi12d 233	. . . . 5 ⊢ (𝑦 = 𝑚 → ((𝑦 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦)) ↔ (𝑚 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq1( + , 𝐻)‘𝑚))))
15	14	imbi2d 229	. . . 4 ⊢ (𝑦 = 𝑚 → ((𝜑 → (𝑦 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦))) ↔ (𝜑 → (𝑚 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq1( + , 𝐻)‘𝑚)))))
16		eleq1 2233	. . . . . 6 ⊢ (𝑦 = (𝑚 + 1) → (𝑦 ∈ (1...(♯‘𝐴)) ↔ (𝑚 + 1) ∈ (1...(♯‘𝐴))))
17		2fveq3 5501	. . . . . . 7 ⊢ (𝑦 = (𝑚 + 1) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))))
18		fveq2 5496	. . . . . . 7 ⊢ (𝑦 = (𝑚 + 1) → (seq1( + , 𝐻)‘𝑦) = (seq1( + , 𝐻)‘(𝑚 + 1)))
19	17, 18	eqeq12d 2185	. . . . . 6 ⊢ (𝑦 = (𝑚 + 1) → ((seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦) ↔ (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1))))
20	16, 19	imbi12d 233	. . . . 5 ⊢ (𝑦 = (𝑚 + 1) → ((𝑦 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦)) ↔ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1)))))
21	20	imbi2d 229	. . . 4 ⊢ (𝑦 = (𝑚 + 1) → ((𝜑 → (𝑦 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦))) ↔ (𝜑 → ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1))))))
22		eleq1 2233	. . . . . 6 ⊢ (𝑦 = 𝑁 → (𝑦 ∈ (1...(♯‘𝐴)) ↔ 𝑁 ∈ (1...(♯‘𝐴))))
23		2fveq3 5501	. . . . . . 7 ⊢ (𝑦 = 𝑁 → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq𝑀( + , 𝐹)‘(𝐺‘𝑁)))
24		fveq2 5496	. . . . . . 7 ⊢ (𝑦 = 𝑁 → (seq1( + , 𝐻)‘𝑦) = (seq1( + , 𝐻)‘𝑁))
25	23, 24	eqeq12d 2185	. . . . . 6 ⊢ (𝑦 = 𝑁 → ((seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦) ↔ (seq𝑀( + , 𝐹)‘(𝐺‘𝑁)) = (seq1( + , 𝐻)‘𝑁)))
26	22, 25	imbi12d 233	. . . . 5 ⊢ (𝑦 = 𝑁 → ((𝑦 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦)) ↔ (𝑁 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑁)) = (seq1( + , 𝐻)‘𝑁))))
27	26	imbi2d 229	. . . 4 ⊢ (𝑦 = 𝑁 → ((𝜑 → (𝑦 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑦)) = (seq1( + , 𝐻)‘𝑦))) ↔ (𝜑 → (𝑁 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑁)) = (seq1( + , 𝐻)‘𝑁)))))
28		seqcoll.1	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑆) → (𝑍 + 𝑘) = 𝑘)
29		seqcoll.a	. . . . . . . . 9 ⊢ (𝜑 → 𝑍 ∈ 𝑆)
30		seqcoll.4	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ⊆ (ℤ_≥‘𝑀))
31		seqcoll.2	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴))
32		isof1o 5786	. . . . . . . . . . . . 13 ⊢ (𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴) → 𝐺:(1...(♯‘𝐴))–1-1-onto→𝐴)
33	31, 32	syl 14	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺:(1...(♯‘𝐴))–1-1-onto→𝐴)
34		f1of 5442	. . . . . . . . . . . 12 ⊢ (𝐺:(1...(♯‘𝐴))–1-1-onto→𝐴 → 𝐺:(1...(♯‘𝐴))⟶𝐴)
35	33, 34	syl 14	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺:(1...(♯‘𝐴))⟶𝐴)
36		elfzuz2 9985	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (1...(♯‘𝐴)) → (♯‘𝐴) ∈ (ℤ_≥‘1))
37	1, 36	syl 14	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘𝐴) ∈ (ℤ_≥‘1))
38		eluzfz1 9987	. . . . . . . . . . . 12 ⊢ ((♯‘𝐴) ∈ (ℤ_≥‘1) → 1 ∈ (1...(♯‘𝐴)))
39	37, 38	syl 14	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ (1...(♯‘𝐴)))
40	35, 39	ffvelrnd 5632	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺‘1) ∈ 𝐴)
41	30, 40	sseldd 3148	. . . . . . . . 9 ⊢ (𝜑 → (𝐺‘1) ∈ (ℤ_≥‘𝑀))
42		eluzle 9499	. . . . . . . . . . . . 13 ⊢ ((♯‘𝐴) ∈ (ℤ_≥‘1) → 1 ≤ (♯‘𝐴))
43	37, 42	syl 14	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ≤ (♯‘𝐴))
44		elfzelz 9981	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (1...(♯‘𝐴)) → 𝑘 ∈ ℤ)
45	44	ssriv 3151	. . . . . . . . . . . . . . . 16 ⊢ (1...(♯‘𝐴)) ⊆ ℤ
46		zssre 9219	. . . . . . . . . . . . . . . 16 ⊢ ℤ ⊆ ℝ
47	45, 46	sstri 3156	. . . . . . . . . . . . . . 15 ⊢ (1...(♯‘𝐴)) ⊆ ℝ
48	47	a1i 9	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1...(♯‘𝐴)) ⊆ ℝ)
49		ressxr 7963	. . . . . . . . . . . . . 14 ⊢ ℝ ⊆ ℝ^*
50	48, 49	sstrdi 3159	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1...(♯‘𝐴)) ⊆ ℝ^*)
51		eluzelre 9497	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ (ℤ_≥‘𝑀) → 𝑘 ∈ ℝ)
52	51	ssriv 3151	. . . . . . . . . . . . . . 15 ⊢ (ℤ_≥‘𝑀) ⊆ ℝ
53	30, 52	sstrdi 3159	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ⊆ ℝ)
54	53, 49	sstrdi 3159	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ⊆ ℝ^*)
55		eluzfz2 9988	. . . . . . . . . . . . . 14 ⊢ ((♯‘𝐴) ∈ (ℤ_≥‘1) → (♯‘𝐴) ∈ (1...(♯‘𝐴)))
56	37, 55	syl 14	. . . . . . . . . . . . 13 ⊢ (𝜑 → (♯‘𝐴) ∈ (1...(♯‘𝐴)))
57		leisorel 10772	. . . . . . . . . . . . 13 ⊢ ((𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴) ∧ ((1...(♯‘𝐴)) ⊆ ℝ^* ∧ 𝐴 ⊆ ℝ^*) ∧ (1 ∈ (1...(♯‘𝐴)) ∧ (♯‘𝐴) ∈ (1...(♯‘𝐴)))) → (1 ≤ (♯‘𝐴) ↔ (𝐺‘1) ≤ (𝐺‘(♯‘𝐴))))
58	31, 50, 54, 39, 56, 57	syl122anc 1242	. . . . . . . . . . . 12 ⊢ (𝜑 → (1 ≤ (♯‘𝐴) ↔ (𝐺‘1) ≤ (𝐺‘(♯‘𝐴))))
59	43, 58	mpbid 146	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐺‘1) ≤ (𝐺‘(♯‘𝐴)))
60	35, 56	ffvelrnd 5632	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐺‘(♯‘𝐴)) ∈ 𝐴)
61	30, 60	sseldd 3148	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐺‘(♯‘𝐴)) ∈ (ℤ_≥‘𝑀))
62		eluzelz 9496	. . . . . . . . . . . . 13 ⊢ ((𝐺‘(♯‘𝐴)) ∈ (ℤ_≥‘𝑀) → (𝐺‘(♯‘𝐴)) ∈ ℤ)
63	61, 62	syl 14	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐺‘(♯‘𝐴)) ∈ ℤ)
64		elfz5 9973	. . . . . . . . . . . 12 ⊢ (((𝐺‘1) ∈ (ℤ_≥‘𝑀) ∧ (𝐺‘(♯‘𝐴)) ∈ ℤ) → ((𝐺‘1) ∈ (𝑀...(𝐺‘(♯‘𝐴))) ↔ (𝐺‘1) ≤ (𝐺‘(♯‘𝐴))))
65	41, 63, 64	syl2anc 409	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐺‘1) ∈ (𝑀...(𝐺‘(♯‘𝐴))) ↔ (𝐺‘1) ≤ (𝐺‘(♯‘𝐴))))
66	59, 65	mpbird 166	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺‘1) ∈ (𝑀...(𝐺‘(♯‘𝐴))))
67		fveq2 5496	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝐺‘1) → (𝐹‘𝑘) = (𝐹‘(𝐺‘1)))
68	67	eleq1d 2239	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝐺‘1) → ((𝐹‘𝑘) ∈ 𝑆 ↔ (𝐹‘(𝐺‘1)) ∈ 𝑆))
69	68	imbi2d 229	. . . . . . . . . . 11 ⊢ (𝑘 = (𝐺‘1) → ((𝜑 → (𝐹‘𝑘) ∈ 𝑆) ↔ (𝜑 → (𝐹‘(𝐺‘1)) ∈ 𝑆)))
70		elfzuz 9977	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (𝑀...(𝐺‘(♯‘𝐴))) → 𝑘 ∈ (ℤ_≥‘𝑀))
71		seqcoll.5	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑀)) → (𝐹‘𝑘) ∈ 𝑆)
72	71	expcom 115	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (ℤ_≥‘𝑀) → (𝜑 → (𝐹‘𝑘) ∈ 𝑆))
73	70, 72	syl 14	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (𝑀...(𝐺‘(♯‘𝐴))) → (𝜑 → (𝐹‘𝑘) ∈ 𝑆))
74	69, 73	vtoclga 2796	. . . . . . . . . 10 ⊢ ((𝐺‘1) ∈ (𝑀...(𝐺‘(♯‘𝐴))) → (𝜑 → (𝐹‘(𝐺‘1)) ∈ 𝑆))
75	66, 74	mpcom 36	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘(𝐺‘1)) ∈ 𝑆)
76		eluzelz 9496	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺‘1) ∈ (ℤ_≥‘𝑀) → (𝐺‘1) ∈ ℤ)
77	41, 76	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐺‘1) ∈ ℤ)
78		peano2zm 9250	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺‘1) ∈ ℤ → ((𝐺‘1) − 1) ∈ ℤ)
79	77, 78	syl 14	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐺‘1) − 1) ∈ ℤ)
80	79	zred 9334	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐺‘1) − 1) ∈ ℝ)
81	77	zred 9334	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐺‘1) ∈ ℝ)
82	63	zred 9334	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐺‘(♯‘𝐴)) ∈ ℝ)
83	81	lem1d 8849	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐺‘1) − 1) ≤ (𝐺‘1))
84	80, 81, 82, 83, 59	letrd 8043	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐺‘1) − 1) ≤ (𝐺‘(♯‘𝐴)))
85		eluz 9500	. . . . . . . . . . . . . . 15 ⊢ ((((𝐺‘1) − 1) ∈ ℤ ∧ (𝐺‘(♯‘𝐴)) ∈ ℤ) → ((𝐺‘(♯‘𝐴)) ∈ (ℤ_≥‘((𝐺‘1) − 1)) ↔ ((𝐺‘1) − 1) ≤ (𝐺‘(♯‘𝐴))))
86	79, 63, 85	syl2anc 409	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐺‘(♯‘𝐴)) ∈ (ℤ_≥‘((𝐺‘1) − 1)) ↔ ((𝐺‘1) − 1) ≤ (𝐺‘(♯‘𝐴))))
87	84, 86	mpbird 166	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐺‘(♯‘𝐴)) ∈ (ℤ_≥‘((𝐺‘1) − 1)))
88		fzss2 10020	. . . . . . . . . . . . 13 ⊢ ((𝐺‘(♯‘𝐴)) ∈ (ℤ_≥‘((𝐺‘1) − 1)) → (𝑀...((𝐺‘1) − 1)) ⊆ (𝑀...(𝐺‘(♯‘𝐴))))
89	87, 88	syl 14	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑀...((𝐺‘1) − 1)) ⊆ (𝑀...(𝐺‘(♯‘𝐴))))
90	89	sselda 3147	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...((𝐺‘1) − 1))) → 𝑘 ∈ (𝑀...(𝐺‘(♯‘𝐴))))
91		eluzel2 9492	. . . . . . . . . . . . . . 15 ⊢ ((𝐺‘1) ∈ (ℤ_≥‘𝑀) → 𝑀 ∈ ℤ)
92	41, 91	syl 14	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ∈ ℤ)
93		elfzm11 10047	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℤ ∧ (𝐺‘1) ∈ ℤ) → (𝑘 ∈ (𝑀...((𝐺‘1) − 1)) ↔ (𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 < (𝐺‘1))))
94	92, 77, 93	syl2anc 409	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑘 ∈ (𝑀...((𝐺‘1) − 1)) ↔ (𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 < (𝐺‘1))))
95		simp3 994	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 < (𝐺‘1)) → 𝑘 < (𝐺‘1))
96	81	adantr 274	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐺‘1) ∈ ℝ)
97	53	sselda 3147	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑘 ∈ ℝ)
98		f1ocnv 5455	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐺:(1...(♯‘𝐴))–1-1-onto→𝐴 → ^◡𝐺:𝐴–1-1-onto→(1...(♯‘𝐴)))
99	33, 98	syl 14	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ^◡𝐺:𝐴–1-1-onto→(1...(♯‘𝐴)))
100		f1of 5442	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (^◡𝐺:𝐴–1-1-onto→(1...(♯‘𝐴)) → ^◡𝐺:𝐴⟶(1...(♯‘𝐴)))
101	99, 100	syl 14	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ^◡𝐺:𝐴⟶(1...(♯‘𝐴)))
102	101	ffvelrnda 5631	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (^◡𝐺‘𝑘) ∈ (1...(♯‘𝐴)))
103		elfznn 10010	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((^◡𝐺‘𝑘) ∈ (1...(♯‘𝐴)) → (^◡𝐺‘𝑘) ∈ ℕ)
104	102, 103	syl 14	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (^◡𝐺‘𝑘) ∈ ℕ)
105	104	nnge1d 8921	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 1 ≤ (^◡𝐺‘𝑘))
106	31	adantr 274	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴))
107	50	adantr 274	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (1...(♯‘𝐴)) ⊆ ℝ^*)
108	54	adantr 274	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐴 ⊆ ℝ^*)
109	39	adantr 274	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 1 ∈ (1...(♯‘𝐴)))
110		leisorel 10772	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴) ∧ ((1...(♯‘𝐴)) ⊆ ℝ^* ∧ 𝐴 ⊆ ℝ^*) ∧ (1 ∈ (1...(♯‘𝐴)) ∧ (^◡𝐺‘𝑘) ∈ (1...(♯‘𝐴)))) → (1 ≤ (^◡𝐺‘𝑘) ↔ (𝐺‘1) ≤ (𝐺‘(^◡𝐺‘𝑘))))
111	106, 107, 108, 109, 102, 110	syl122anc 1242	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (1 ≤ (^◡𝐺‘𝑘) ↔ (𝐺‘1) ≤ (𝐺‘(^◡𝐺‘𝑘))))
112	105, 111	mpbid 146	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐺‘1) ≤ (𝐺‘(^◡𝐺‘𝑘)))
113		f1ocnvfv2 5757	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺:(1...(♯‘𝐴))–1-1-onto→𝐴 ∧ 𝑘 ∈ 𝐴) → (𝐺‘(^◡𝐺‘𝑘)) = 𝑘)
114	33, 113	sylan 281	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐺‘(^◡𝐺‘𝑘)) = 𝑘)
115	112, 114	breqtrd 4015	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐺‘1) ≤ 𝑘)
116	96, 97, 115	lensymd 8041	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ¬ 𝑘 < (𝐺‘1))
117	116	ex 114	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑘 ∈ 𝐴 → ¬ 𝑘 < (𝐺‘1)))
118	117	con2d 619	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑘 < (𝐺‘1) → ¬ 𝑘 ∈ 𝐴))
119	95, 118	syl5 32	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 < (𝐺‘1)) → ¬ 𝑘 ∈ 𝐴))
120	94, 119	sylbid 149	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑘 ∈ (𝑀...((𝐺‘1) − 1)) → ¬ 𝑘 ∈ 𝐴))
121	120	imp 123	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...((𝐺‘1) − 1))) → ¬ 𝑘 ∈ 𝐴)
122	90, 121	eldifd 3131	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...((𝐺‘1) − 1))) → 𝑘 ∈ ((𝑀...(𝐺‘(♯‘𝐴))) ∖ 𝐴))
123		seqcoll.6	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀...(𝐺‘(♯‘𝐴))) ∖ 𝐴)) → (𝐹‘𝑘) = 𝑍)
124	122, 123	syldan 280	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...((𝐺‘1) − 1))) → (𝐹‘𝑘) = 𝑍)
125		seqcoll.c	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑘 ∈ 𝑆 ∧ 𝑛 ∈ 𝑆)) → (𝑘 + 𝑛) ∈ 𝑆)
126	28, 29, 41, 75, 124, 71, 125	seq3id 10464	. . . . . . . 8 ⊢ (𝜑 → (seq𝑀( + , 𝐹) ↾ (ℤ_≥‘(𝐺‘1))) = seq(𝐺‘1)( + , 𝐹))
127	126	fveq1d 5498	. . . . . . 7 ⊢ (𝜑 → ((seq𝑀( + , 𝐹) ↾ (ℤ_≥‘(𝐺‘1)))‘(𝐺‘1)) = (seq(𝐺‘1)( + , 𝐹)‘(𝐺‘1)))
128		uzid 9501	. . . . . . . . 9 ⊢ ((𝐺‘1) ∈ ℤ → (𝐺‘1) ∈ (ℤ_≥‘(𝐺‘1)))
129	77, 128	syl 14	. . . . . . . 8 ⊢ (𝜑 → (𝐺‘1) ∈ (ℤ_≥‘(𝐺‘1)))
130		fvres 5520	. . . . . . . 8 ⊢ ((𝐺‘1) ∈ (ℤ_≥‘(𝐺‘1)) → ((seq𝑀( + , 𝐹) ↾ (ℤ_≥‘(𝐺‘1)))‘(𝐺‘1)) = (seq𝑀( + , 𝐹)‘(𝐺‘1)))
131	129, 130	syl 14	. . . . . . 7 ⊢ (𝜑 → ((seq𝑀( + , 𝐹) ↾ (ℤ_≥‘(𝐺‘1)))‘(𝐺‘1)) = (seq𝑀( + , 𝐹)‘(𝐺‘1)))
132	92	adantr 274	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝐺‘1))) → 𝑀 ∈ ℤ)
133		eluzelz 9496	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (ℤ_≥‘(𝐺‘1)) → 𝑘 ∈ ℤ)
134	133	adantl 275	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝐺‘1))) → 𝑘 ∈ ℤ)
135	132	zred 9334	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝐺‘1))) → 𝑀 ∈ ℝ)
136	81	adantr 274	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝐺‘1))) → (𝐺‘1) ∈ ℝ)
137	134	zred 9334	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝐺‘1))) → 𝑘 ∈ ℝ)
138		eluzle 9499	. . . . . . . . . . . . . 14 ⊢ ((𝐺‘1) ∈ (ℤ_≥‘𝑀) → 𝑀 ≤ (𝐺‘1))
139	41, 138	syl 14	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ≤ (𝐺‘1))
140	139	adantr 274	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝐺‘1))) → 𝑀 ≤ (𝐺‘1))
141		eluzle 9499	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (ℤ_≥‘(𝐺‘1)) → (𝐺‘1) ≤ 𝑘)
142	141	adantl 275	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝐺‘1))) → (𝐺‘1) ≤ 𝑘)
143	135, 136, 137, 140, 142	letrd 8043	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝐺‘1))) → 𝑀 ≤ 𝑘)
144		eluz2 9493	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (ℤ_≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘))
145	132, 134, 143, 144	syl3anbrc 1176	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝐺‘1))) → 𝑘 ∈ (ℤ_≥‘𝑀))
146	145, 71	syldan 280	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝐺‘1))) → (𝐹‘𝑘) ∈ 𝑆)
147	77, 146, 125	seq3-1 10416	. . . . . . . 8 ⊢ (𝜑 → (seq(𝐺‘1)( + , 𝐹)‘(𝐺‘1)) = (𝐹‘(𝐺‘1)))
148		fveq2 5496	. . . . . . . . . . . 12 ⊢ (𝑛 = 1 → (𝐻‘𝑛) = (𝐻‘1))
149		2fveq3 5501	. . . . . . . . . . . 12 ⊢ (𝑛 = 1 → (𝐹‘(𝐺‘𝑛)) = (𝐹‘(𝐺‘1)))
150	148, 149	eqeq12d 2185	. . . . . . . . . . 11 ⊢ (𝑛 = 1 → ((𝐻‘𝑛) = (𝐹‘(𝐺‘𝑛)) ↔ (𝐻‘1) = (𝐹‘(𝐺‘1))))
151	150	imbi2d 229	. . . . . . . . . 10 ⊢ (𝑛 = 1 → ((𝜑 → (𝐻‘𝑛) = (𝐹‘(𝐺‘𝑛))) ↔ (𝜑 → (𝐻‘1) = (𝐹‘(𝐺‘1)))))
152		seqcoll.7	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (𝐻‘𝑛) = (𝐹‘(𝐺‘𝑛)))
153	152	expcom 115	. . . . . . . . . 10 ⊢ (𝑛 ∈ (1...(♯‘𝐴)) → (𝜑 → (𝐻‘𝑛) = (𝐹‘(𝐺‘𝑛))))
154	151, 153	vtoclga 2796	. . . . . . . . 9 ⊢ (1 ∈ (1...(♯‘𝐴)) → (𝜑 → (𝐻‘1) = (𝐹‘(𝐺‘1))))
155	39, 154	mpcom 36	. . . . . . . 8 ⊢ (𝜑 → (𝐻‘1) = (𝐹‘(𝐺‘1)))
156	147, 155	eqtr4d 2206	. . . . . . 7 ⊢ (𝜑 → (seq(𝐺‘1)( + , 𝐹)‘(𝐺‘1)) = (𝐻‘1))
157	127, 131, 156	3eqtr3d 2211	. . . . . 6 ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘(𝐺‘1)) = (𝐻‘1))
158		1zzd 9239	. . . . . . 7 ⊢ (𝜑 → 1 ∈ ℤ)
159		seqcoll.hcl	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘1)) → (𝐻‘𝑘) ∈ 𝑆)
160	158, 159, 125	seq3-1 10416	. . . . . 6 ⊢ (𝜑 → (seq1( + , 𝐻)‘1) = (𝐻‘1))
161	157, 160	eqtr4d 2206	. . . . 5 ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘(𝐺‘1)) = (seq1( + , 𝐻)‘1))
162	161	a1d 22	. . . 4 ⊢ (𝜑 → (1 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘1)) = (seq1( + , 𝐻)‘1)))
163		simplr 525	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝑚 ∈ ℕ)
164		nnuz 9522	. . . . . . . . . . 11 ⊢ ℕ = (ℤ_≥‘1)
165	163, 164	eleqtrdi 2263	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝑚 ∈ (ℤ_≥‘1))
166		nnz 9231	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℤ)
167	166	ad2antlr 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝑚 ∈ ℤ)
168		elfzuz3 9978	. . . . . . . . . . . 12 ⊢ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (♯‘𝐴) ∈ (ℤ_≥‘(𝑚 + 1)))
169	168	adantl 275	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (♯‘𝐴) ∈ (ℤ_≥‘(𝑚 + 1)))
170		peano2uzr 9544	. . . . . . . . . . 11 ⊢ ((𝑚 ∈ ℤ ∧ (♯‘𝐴) ∈ (ℤ_≥‘(𝑚 + 1))) → (♯‘𝐴) ∈ (ℤ_≥‘𝑚))
171	167, 169, 170	syl2anc 409	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (♯‘𝐴) ∈ (ℤ_≥‘𝑚))
172		elfzuzb 9975	. . . . . . . . . 10 ⊢ (𝑚 ∈ (1...(♯‘𝐴)) ↔ (𝑚 ∈ (ℤ_≥‘1) ∧ (♯‘𝐴) ∈ (ℤ_≥‘𝑚)))
173	165, 171, 172	sylanbrc 415	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝑚 ∈ (1...(♯‘𝐴)))
174	173	ex 114	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → 𝑚 ∈ (1...(♯‘𝐴))))
175	174	imim1d 75	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑚 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq1( + , 𝐻)‘𝑚)) → ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq1( + , 𝐻)‘𝑚))))
176		oveq1 5860	. . . . . . . . . 10 ⊢ ((seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq1( + , 𝐻)‘𝑚) → ((seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) + (𝐻‘(𝑚 + 1))) = ((seq1( + , 𝐻)‘𝑚) + (𝐻‘(𝑚 + 1))))
177		simpll 524	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝜑)
178		seqcoll.1b	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑆) → (𝑘 + 𝑍) = 𝑘)
179	177, 178	sylan 281	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ 𝑆) → (𝑘 + 𝑍) = 𝑘)
180	30	ad2antrr 485	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝐴 ⊆ (ℤ_≥‘𝑀))
181	35	ad2antrr 485	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝐺:(1...(♯‘𝐴))⟶𝐴)
182	181, 173	ffvelrnd 5632	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘𝑚) ∈ 𝐴)
183	180, 182	sseldd 3148	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘𝑚) ∈ (ℤ_≥‘𝑀))
184		nnre 8885	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℝ)
185	184	ad2antlr 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝑚 ∈ ℝ)
186	185	ltp1d 8846	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝑚 < (𝑚 + 1))
187	31	ad2antrr 485	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴))
188		simpr 109	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝑚 + 1) ∈ (1...(♯‘𝐴)))
189		isorel 5787	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴) ∧ (𝑚 ∈ (1...(♯‘𝐴)) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴)))) → (𝑚 < (𝑚 + 1) ↔ (𝐺‘𝑚) < (𝐺‘(𝑚 + 1))))
190	187, 173, 188, 189	syl12anc 1231	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝑚 < (𝑚 + 1) ↔ (𝐺‘𝑚) < (𝐺‘(𝑚 + 1))))
191	186, 190	mpbid 146	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘𝑚) < (𝐺‘(𝑚 + 1)))
192		eluzelz 9496	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺‘𝑚) ∈ (ℤ_≥‘𝑀) → (𝐺‘𝑚) ∈ ℤ)
193	183, 192	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘𝑚) ∈ ℤ)
194	181, 188	ffvelrnd 5632	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(𝑚 + 1)) ∈ 𝐴)
195	180, 194	sseldd 3148	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(𝑚 + 1)) ∈ (ℤ_≥‘𝑀))
196		eluzelz 9496	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺‘(𝑚 + 1)) ∈ (ℤ_≥‘𝑀) → (𝐺‘(𝑚 + 1)) ∈ ℤ)
197	195, 196	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(𝑚 + 1)) ∈ ℤ)
198		zltlem1 9269	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐺‘𝑚) ∈ ℤ ∧ (𝐺‘(𝑚 + 1)) ∈ ℤ) → ((𝐺‘𝑚) < (𝐺‘(𝑚 + 1)) ↔ (𝐺‘𝑚) ≤ ((𝐺‘(𝑚 + 1)) − 1)))
199	193, 197, 198	syl2anc 409	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝐺‘𝑚) < (𝐺‘(𝑚 + 1)) ↔ (𝐺‘𝑚) ≤ ((𝐺‘(𝑚 + 1)) − 1)))
200	191, 199	mpbid 146	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘𝑚) ≤ ((𝐺‘(𝑚 + 1)) − 1))
201		peano2zm 9250	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺‘(𝑚 + 1)) ∈ ℤ → ((𝐺‘(𝑚 + 1)) − 1) ∈ ℤ)
202	197, 201	syl 14	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝐺‘(𝑚 + 1)) − 1) ∈ ℤ)
203		eluz 9500	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺‘𝑚) ∈ ℤ ∧ ((𝐺‘(𝑚 + 1)) − 1) ∈ ℤ) → (((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ_≥‘(𝐺‘𝑚)) ↔ (𝐺‘𝑚) ≤ ((𝐺‘(𝑚 + 1)) − 1)))
204	193, 202, 203	syl2anc 409	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ_≥‘(𝐺‘𝑚)) ↔ (𝐺‘𝑚) ≤ ((𝐺‘(𝑚 + 1)) − 1)))
205	200, 204	mpbird 166	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ_≥‘(𝐺‘𝑚)))
206		eqid 2170	. . . . . . . . . . . . . . . 16 ⊢ (ℤ_≥‘𝑀) = (ℤ_≥‘𝑀)
207	92	ad2antrr 485	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝑀 ∈ ℤ)
208	177, 71	sylan 281	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (ℤ_≥‘𝑀)) → (𝐹‘𝑘) ∈ 𝑆)
209	177, 125	sylan 281	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ (𝑘 ∈ 𝑆 ∧ 𝑛 ∈ 𝑆)) → (𝑘 + 𝑛) ∈ 𝑆)
210	206, 207, 208, 209	seqf 10417	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → seq𝑀( + , 𝐹):(ℤ_≥‘𝑀)⟶𝑆)
211	210, 183	ffvelrnd 5632	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) ∈ 𝑆)
212		simplll 528	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1))) → 𝜑)
213		elfzuz 9977	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1)) → 𝑘 ∈ (ℤ_≥‘((𝐺‘𝑚) + 1)))
214		peano2uz 9542	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺‘𝑚) ∈ (ℤ_≥‘𝑀) → ((𝐺‘𝑚) + 1) ∈ (ℤ_≥‘𝑀))
215	183, 214	syl 14	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝐺‘𝑚) + 1) ∈ (ℤ_≥‘𝑀))
216		uztrn 9503	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ (ℤ_≥‘((𝐺‘𝑚) + 1)) ∧ ((𝐺‘𝑚) + 1) ∈ (ℤ_≥‘𝑀)) → 𝑘 ∈ (ℤ_≥‘𝑀))
217	213, 215, 216	syl2anr 288	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1))) → 𝑘 ∈ (ℤ_≥‘𝑀))
218	202	zred 9334	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝐺‘(𝑚 + 1)) − 1) ∈ ℝ)
219	197	zred 9334	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(𝑚 + 1)) ∈ ℝ)
220	82	ad2antrr 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(♯‘𝐴)) ∈ ℝ)
221	219	lem1d 8849	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝐺‘(𝑚 + 1)) − 1) ≤ (𝐺‘(𝑚 + 1)))
222		elfzle2 9984	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (𝑚 + 1) ≤ (♯‘𝐴))
223	222	adantl 275	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝑚 + 1) ≤ (♯‘𝐴))
224	50	ad2antrr 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (1...(♯‘𝐴)) ⊆ ℝ^*)
225	54	ad2antrr 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → 𝐴 ⊆ ℝ^*)
226	56	ad2antrr 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (♯‘𝐴) ∈ (1...(♯‘𝐴)))
227		leisorel 10772	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴) ∧ ((1...(♯‘𝐴)) ⊆ ℝ^* ∧ 𝐴 ⊆ ℝ^*) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ (♯‘𝐴) ∈ (1...(♯‘𝐴)))) → ((𝑚 + 1) ≤ (♯‘𝐴) ↔ (𝐺‘(𝑚 + 1)) ≤ (𝐺‘(♯‘𝐴))))
228	187, 224, 225, 188, 226, 227	syl122anc 1242	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝑚 + 1) ≤ (♯‘𝐴) ↔ (𝐺‘(𝑚 + 1)) ≤ (𝐺‘(♯‘𝐴))))
229	223, 228	mpbid 146	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(𝑚 + 1)) ≤ (𝐺‘(♯‘𝐴)))
230	218, 219, 220, 221, 229	letrd 8043	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝐺‘(𝑚 + 1)) − 1) ≤ (𝐺‘(♯‘𝐴)))
231	63	ad2antrr 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(♯‘𝐴)) ∈ ℤ)
232		eluz 9500	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐺‘(𝑚 + 1)) − 1) ∈ ℤ ∧ (𝐺‘(♯‘𝐴)) ∈ ℤ) → ((𝐺‘(♯‘𝐴)) ∈ (ℤ_≥‘((𝐺‘(𝑚 + 1)) − 1)) ↔ ((𝐺‘(𝑚 + 1)) − 1) ≤ (𝐺‘(♯‘𝐴))))
233	202, 231, 232	syl2anc 409	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝐺‘(♯‘𝐴)) ∈ (ℤ_≥‘((𝐺‘(𝑚 + 1)) − 1)) ↔ ((𝐺‘(𝑚 + 1)) − 1) ≤ (𝐺‘(♯‘𝐴))))
234	230, 233	mpbird 166	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(♯‘𝐴)) ∈ (ℤ_≥‘((𝐺‘(𝑚 + 1)) − 1)))
235		elfzuz3 9978	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1)) → ((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ_≥‘𝑘))
236		uztrn 9503	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐺‘(♯‘𝐴)) ∈ (ℤ_≥‘((𝐺‘(𝑚 + 1)) − 1)) ∧ ((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ_≥‘𝑘)) → (𝐺‘(♯‘𝐴)) ∈ (ℤ_≥‘𝑘))
237	234, 235, 236	syl2an 287	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1))) → (𝐺‘(♯‘𝐴)) ∈ (ℤ_≥‘𝑘))
238		elfzuzb 9975	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (𝑀...(𝐺‘(♯‘𝐴))) ↔ (𝑘 ∈ (ℤ_≥‘𝑀) ∧ (𝐺‘(♯‘𝐴)) ∈ (ℤ_≥‘𝑘)))
239	217, 237, 238	sylanbrc 415	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1))) → 𝑘 ∈ (𝑀...(𝐺‘(♯‘𝐴))))
240	166	ad2antlr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → 𝑚 ∈ ℤ)
241	101	ad2antrr 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → ^◡𝐺:𝐴⟶(1...(♯‘𝐴)))
242		simprr 527	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → 𝑘 ∈ 𝐴)
243	241, 242	ffvelrnd 5632	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → (^◡𝐺‘𝑘) ∈ (1...(♯‘𝐴)))
244		elfzelz 9981	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((^◡𝐺‘𝑘) ∈ (1...(♯‘𝐴)) → (^◡𝐺‘𝑘) ∈ ℤ)
245	243, 244	syl 14	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → (^◡𝐺‘𝑘) ∈ ℤ)
246		btwnnz 9306	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑚 ∈ ℤ ∧ 𝑚 < (^◡𝐺‘𝑘) ∧ (^◡𝐺‘𝑘) < (𝑚 + 1)) → ¬ (^◡𝐺‘𝑘) ∈ ℤ)
247	246	3expib 1201	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 ∈ ℤ → ((𝑚 < (^◡𝐺‘𝑘) ∧ (^◡𝐺‘𝑘) < (𝑚 + 1)) → ¬ (^◡𝐺‘𝑘) ∈ ℤ))
248	247	con2d 619	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 ∈ ℤ → ((^◡𝐺‘𝑘) ∈ ℤ → ¬ (𝑚 < (^◡𝐺‘𝑘) ∧ (^◡𝐺‘𝑘) < (𝑚 + 1))))
249	240, 245, 248	sylc 62	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → ¬ (𝑚 < (^◡𝐺‘𝑘) ∧ (^◡𝐺‘𝑘) < (𝑚 + 1)))
250	31	ad2antrr 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → 𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴))
251	173	adantrr 476	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → 𝑚 ∈ (1...(♯‘𝐴)))
252		isorel 5787	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴) ∧ (𝑚 ∈ (1...(♯‘𝐴)) ∧ (^◡𝐺‘𝑘) ∈ (1...(♯‘𝐴)))) → (𝑚 < (^◡𝐺‘𝑘) ↔ (𝐺‘𝑚) < (𝐺‘(^◡𝐺‘𝑘))))
253	250, 251, 243, 252	syl12anc 1231	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → (𝑚 < (^◡𝐺‘𝑘) ↔ (𝐺‘𝑚) < (𝐺‘(^◡𝐺‘𝑘))))
254	33	ad2antrr 485	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → 𝐺:(1...(♯‘𝐴))–1-1-onto→𝐴)
255	254, 242, 113	syl2anc 409	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → (𝐺‘(^◡𝐺‘𝑘)) = 𝑘)
256	255	breq2d 4001	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → ((𝐺‘𝑚) < (𝐺‘(^◡𝐺‘𝑘)) ↔ (𝐺‘𝑚) < 𝑘))
257	193	adantrr 476	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → (𝐺‘𝑚) ∈ ℤ)
258	30	ad2antrr 485	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → 𝐴 ⊆ (ℤ_≥‘𝑀))
259	258, 242	sseldd 3148	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → 𝑘 ∈ (ℤ_≥‘𝑀))
260		eluzelz 9496	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 ∈ (ℤ_≥‘𝑀) → 𝑘 ∈ ℤ)
261	259, 260	syl 14	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → 𝑘 ∈ ℤ)
262		zltp1le 9266	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐺‘𝑚) ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((𝐺‘𝑚) < 𝑘 ↔ ((𝐺‘𝑚) + 1) ≤ 𝑘))
263	257, 261, 262	syl2anc 409	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → ((𝐺‘𝑚) < 𝑘 ↔ ((𝐺‘𝑚) + 1) ≤ 𝑘))
264	253, 256, 263	3bitrd 213	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → (𝑚 < (^◡𝐺‘𝑘) ↔ ((𝐺‘𝑚) + 1) ≤ 𝑘))
265	188	adantrr 476	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → (𝑚 + 1) ∈ (1...(♯‘𝐴)))
266		isorel 5787	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴) ∧ ((^◡𝐺‘𝑘) ∈ (1...(♯‘𝐴)) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴)))) → ((^◡𝐺‘𝑘) < (𝑚 + 1) ↔ (𝐺‘(^◡𝐺‘𝑘)) < (𝐺‘(𝑚 + 1))))
267	250, 243, 265, 266	syl12anc 1231	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → ((^◡𝐺‘𝑘) < (𝑚 + 1) ↔ (𝐺‘(^◡𝐺‘𝑘)) < (𝐺‘(𝑚 + 1))))
268	255	breq1d 3999	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → ((𝐺‘(^◡𝐺‘𝑘)) < (𝐺‘(𝑚 + 1)) ↔ 𝑘 < (𝐺‘(𝑚 + 1))))
269	197	adantrr 476	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → (𝐺‘(𝑚 + 1)) ∈ ℤ)
270		zltlem1 9269	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 ∈ ℤ ∧ (𝐺‘(𝑚 + 1)) ∈ ℤ) → (𝑘 < (𝐺‘(𝑚 + 1)) ↔ 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1)))
271	261, 269, 270	syl2anc 409	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → (𝑘 < (𝐺‘(𝑚 + 1)) ↔ 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1)))
272	267, 268, 271	3bitrd 213	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → ((^◡𝐺‘𝑘) < (𝑚 + 1) ↔ 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1)))
273	264, 272	anbi12d 470	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → ((𝑚 < (^◡𝐺‘𝑘) ∧ (^◡𝐺‘𝑘) < (𝑚 + 1)) ↔ (((𝐺‘𝑚) + 1) ≤ 𝑘 ∧ 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1))))
274	249, 273	mtbid 667	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) ∧ 𝑘 ∈ 𝐴)) → ¬ (((𝐺‘𝑚) + 1) ≤ 𝑘 ∧ 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1)))
275	274	expr 373	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝑘 ∈ 𝐴 → ¬ (((𝐺‘𝑚) + 1) ≤ 𝑘 ∧ 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1))))
276	275	con2d 619	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((((𝐺‘𝑚) + 1) ≤ 𝑘 ∧ 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1)) → ¬ 𝑘 ∈ 𝐴))
277		elfzle1 9983	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1)) → ((𝐺‘𝑚) + 1) ≤ 𝑘)
278		elfzle2 9984	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1)) → 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1))
279	277, 278	jca 304	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1)) → (((𝐺‘𝑚) + 1) ≤ 𝑘 ∧ 𝑘 ≤ ((𝐺‘(𝑚 + 1)) − 1)))
280	276, 279	impel 278	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1))) → ¬ 𝑘 ∈ 𝐴)
281	239, 280	eldifd 3131	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1))) → 𝑘 ∈ ((𝑀...(𝐺‘(♯‘𝐴))) ∖ 𝐴))
282	212, 281, 123	syl2anc 409	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (((𝐺‘𝑚) + 1)...((𝐺‘(𝑚 + 1)) − 1))) → (𝐹‘𝑘) = 𝑍)
283	179, 183, 205, 211, 282, 208, 209	seq3id2 10465	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq𝑀( + , 𝐹)‘((𝐺‘(𝑚 + 1)) − 1)))
284	283	oveq1d 5868	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) + (𝐹‘(𝐺‘(𝑚 + 1)))) = ((seq𝑀( + , 𝐹)‘((𝐺‘(𝑚 + 1)) − 1)) + (𝐹‘(𝐺‘(𝑚 + 1)))))
285		fveq2 5496	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = (𝑚 + 1) → (𝐻‘𝑛) = (𝐻‘(𝑚 + 1)))
286		2fveq3 5501	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = (𝑚 + 1) → (𝐹‘(𝐺‘𝑛)) = (𝐹‘(𝐺‘(𝑚 + 1))))
287	285, 286	eqeq12d 2185	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = (𝑚 + 1) → ((𝐻‘𝑛) = (𝐹‘(𝐺‘𝑛)) ↔ (𝐻‘(𝑚 + 1)) = (𝐹‘(𝐺‘(𝑚 + 1)))))
288	287	imbi2d 229	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = (𝑚 + 1) → ((𝜑 → (𝐻‘𝑛) = (𝐹‘(𝐺‘𝑛))) ↔ (𝜑 → (𝐻‘(𝑚 + 1)) = (𝐹‘(𝐺‘(𝑚 + 1))))))
289	288, 153	vtoclga 2796	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (𝜑 → (𝐻‘(𝑚 + 1)) = (𝐹‘(𝐺‘(𝑚 + 1)))))
290	289	impcom 124	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐻‘(𝑚 + 1)) = (𝐹‘(𝐺‘(𝑚 + 1))))
291	290	adantlr 474	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐻‘(𝑚 + 1)) = (𝐹‘(𝐺‘(𝑚 + 1))))
292	291	oveq2d 5869	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) + (𝐻‘(𝑚 + 1))) = ((seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) + (𝐹‘(𝐺‘(𝑚 + 1)))))
293	197	zcnd 9335	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(𝑚 + 1)) ∈ ℂ)
294		ax-1cn 7867	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
295		npcan 8128	. . . . . . . . . . . . . . 15 ⊢ (((𝐺‘(𝑚 + 1)) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝐺‘(𝑚 + 1)) − 1) + 1) = (𝐺‘(𝑚 + 1)))
296	293, 294, 295	sylancl 411	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (((𝐺‘(𝑚 + 1)) − 1) + 1) = (𝐺‘(𝑚 + 1)))
297		uztrn 9503	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ_≥‘(𝐺‘𝑚)) ∧ (𝐺‘𝑚) ∈ (ℤ_≥‘𝑀)) → ((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ_≥‘𝑀))
298	205, 183, 297	syl2anc 409	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ_≥‘𝑀))
299		eluzp1p1 9512	. . . . . . . . . . . . . . 15 ⊢ (((𝐺‘(𝑚 + 1)) − 1) ∈ (ℤ_≥‘𝑀) → (((𝐺‘(𝑚 + 1)) − 1) + 1) ∈ (ℤ_≥‘(𝑀 + 1)))
300	298, 299	syl 14	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (((𝐺‘(𝑚 + 1)) − 1) + 1) ∈ (ℤ_≥‘(𝑀 + 1)))
301	296, 300	eqeltrrd 2248	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (𝐺‘(𝑚 + 1)) ∈ (ℤ_≥‘(𝑀 + 1)))
302	207, 301, 208, 209	seq3m1 10424	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = ((seq𝑀( + , 𝐹)‘((𝐺‘(𝑚 + 1)) − 1)) + (𝐹‘(𝐺‘(𝑚 + 1)))))
303	284, 292, 302	3eqtr4rd 2214	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = ((seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) + (𝐻‘(𝑚 + 1))))
304	177, 159	sylan 281	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) ∧ 𝑘 ∈ (ℤ_≥‘1)) → (𝐻‘𝑘) ∈ 𝑆)
305	165, 304, 209	seq3p1 10418	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → (seq1( + , 𝐻)‘(𝑚 + 1)) = ((seq1( + , 𝐻)‘𝑚) + (𝐻‘(𝑚 + 1))))
306	303, 305	eqeq12d 2185	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1)) ↔ ((seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) + (𝐻‘(𝑚 + 1))) = ((seq1( + , 𝐻)‘𝑚) + (𝐻‘(𝑚 + 1)))))
307	176, 306	syl5ibr 155	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(♯‘𝐴))) → ((seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq1( + , 𝐻)‘𝑚) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1))))
308	307	ex 114	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → ((seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq1( + , 𝐻)‘𝑚) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1)))))
309	308	a2d 26	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq1( + , 𝐻)‘𝑚)) → ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1)))))
310	175, 309	syld 45	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑚 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq1( + , 𝐻)‘𝑚)) → ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1)))))
311	310	expcom 115	. . . . 5 ⊢ (𝑚 ∈ ℕ → (𝜑 → ((𝑚 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq1( + , 𝐻)‘𝑚)) → ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1))))))
312	311	a2d 26	. . . 4 ⊢ (𝑚 ∈ ℕ → ((𝜑 → (𝑚 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑚)) = (seq1( + , 𝐻)‘𝑚))) → (𝜑 → ((𝑚 + 1) ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘(𝑚 + 1))) = (seq1( + , 𝐻)‘(𝑚 + 1))))))
313	9, 15, 21, 27, 162, 312	nnind 8894	. . 3 ⊢ (𝑁 ∈ ℕ → (𝜑 → (𝑁 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑁)) = (seq1( + , 𝐻)‘𝑁))))
314	3, 313	mpcom 36	. 2 ⊢ (𝜑 → (𝑁 ∈ (1...(♯‘𝐴)) → (seq𝑀( + , 𝐹)‘(𝐺‘𝑁)) = (seq1( + , 𝐻)‘𝑁)))
315	1, 314	mpd 13	1 ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘(𝐺‘𝑁)) = (seq1( + , 𝐻)‘𝑁))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 103 ↔ wb 104 ∧ w3a 973 = wceq 1348 ∈ wcel 2141 ∖ cdif 3118 ⊆ wss 3121 class class class wbr 3989 ^◡ccnv 4610 ↾ cres 4613 ⟶wf 5194 –1-1-onto→wf1o 5197 ‘cfv 5198 Isom wiso 5199 (class class class)co 5853 ℂcc 7772 ℝcr 7773 1c1 7775 + caddc 7777 ℝ^*cxr 7953 < clt 7954 ≤ cle 7955 − cmin 8090 ℕcn 8878 ℤcz 9212 ℤ_≥cuz 9487 ...cfz 9965 seqcseq 10401 ♯chash 10709

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 609 ax-in2 610 ax-io 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-10 1498 ax-11 1499 ax-i12 1500 ax-bndl 1502 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-13 2143 ax-14 2144 ax-ext 2152 ax-coll 4104 ax-sep 4107 ax-nul 4115 ax-pow 4160 ax-pr 4194 ax-un 4418 ax-setind 4521 ax-iinf 4572 ax-cnex 7865 ax-resscn 7866 ax-1cn 7867 ax-1re 7868 ax-icn 7869 ax-addcl 7870 ax-addrcl 7871 ax-mulcl 7872 ax-addcom 7874 ax-addass 7876 ax-distr 7878 ax-i2m1 7879 ax-0lt1 7880 ax-0id 7882 ax-rnegex 7883 ax-cnre 7885 ax-pre-ltirr 7886 ax-pre-ltwlin 7887 ax-pre-lttrn 7888 ax-pre-ltadd 7890

This theorem depends on definitions: df-bi 116 df-3or 974 df-3an 975 df-tru 1351 df-fal 1354 df-nf 1454 df-sb 1756 df-eu 2022 df-mo 2023 df-clab 2157 df-cleq 2163 df-clel 2166 df-nfc 2301 df-ne 2341 df-nel 2436 df-ral 2453 df-rex 2454 df-reu 2455 df-rab 2457 df-v 2732 df-sbc 2956 df-csb 3050 df-dif 3123 df-un 3125 df-in 3127 df-ss 3134 df-nul 3415 df-pw 3568 df-sn 3589 df-pr 3590 df-op 3592 df-uni 3797 df-int 3832 df-iun 3875 df-br 3990 df-opab 4051 df-mpt 4052 df-tr 4088 df-id 4278 df-iord 4351 df-on 4353 df-ilim 4354 df-suc 4356 df-iom 4575 df-xp 4617 df-rel 4618 df-cnv 4619 df-co 4620 df-dm 4621 df-rn 4622 df-res 4623 df-ima 4624 df-iota 5160 df-fun 5200 df-fn 5201 df-f 5202 df-f1 5203 df-fo 5204 df-f1o 5205 df-fv 5206 df-isom 5207 df-riota 5809 df-ov 5856 df-oprab 5857 df-mpo 5858 df-1st 6119 df-2nd 6120 df-recs 6284 df-frec 6370 df-pnf 7956 df-mnf 7957 df-xr 7958 df-ltxr 7959 df-le 7960 df-sub 8092 df-neg 8093 df-inn 8879 df-n0 9136 df-z 9213 df-uz 9488 df-fz 9966 df-fzo 10099 df-seqfrec 10402

This theorem is referenced by: summodclem2a 11344 prodmodclem2a 11539

W3C validator