prodmodclem2a - Intuitionistic Logic Explorer

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

Theorem prodmodclem2a 11517

Description: Lemma for prodmodc 11519. (Contributed by Scott Fenton, 4-Dec-2017.) (Revised by Jim Kingdon, 11-Apr-2024.)

**Hypotheses**
Ref	Expression
prodmo.1	⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))
prodmo.2	⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
prodmodc.3	⊢ 𝐺 = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑘⦌𝐵, 1))
prodmodclem2.4	⊢ 𝐻 = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝐾‘𝑗) / 𝑘⦌𝐵, 1))
prodmodclem2a.dc	⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑀)) → DECID 𝑘 ∈ 𝐴)
prodmolem2.5	⊢ (𝜑 → 𝑁 ∈ ℕ)
prodmolem2.6	⊢ (𝜑 → 𝑀 ∈ ℤ)
prodmolem2.7	⊢ (𝜑 → 𝐴 ⊆ (ℤ_≥‘𝑀))
prodmolem2.8	⊢ (𝜑 → 𝑓:(1...𝑁)–1-1-onto→𝐴)
prodmolem2.9	⊢ (𝜑 → 𝐾 Isom < , < ((1...(♯‘𝐴)), 𝐴))

**Assertion**
Ref	Expression
prodmodclem2a	⊢ (𝜑 → seq𝑀( · , 𝐹) ⇝ (seq1( · , 𝐺)‘𝑁))

Distinct variable groups: 𝐴,𝑗,𝑘 𝐵,𝑗 𝑘,𝐹 𝑗,𝐺 𝑗,𝐾,𝑘 𝑗,𝑀,𝑘 𝑗,𝑁,𝑘 𝑓,𝑗,𝑘 𝜑,𝑘 Allowed substitution hints: 𝜑(𝑓,𝑗) 𝐴(𝑓) 𝐵(𝑓,𝑘) 𝐹(𝑓,𝑗) 𝐺(𝑓,𝑘) 𝐻(𝑓,𝑗,𝑘) 𝐾(𝑓) 𝑀(𝑓) 𝑁(𝑓)

Proof of Theorem prodmodclem2a Dummy variables 𝑝 𝑚 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		prodmo.1	. . 3 ⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))
2		prodmo.2	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
3		prodmodclem2a.dc	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑀)) → DECID 𝑘 ∈ 𝐴)
4		prodmolem2.7	. . . 4 ⊢ (𝜑 → 𝐴 ⊆ (ℤ_≥‘𝑀))
5		prodmolem2.9	. . . . . . 7 ⊢ (𝜑 → 𝐾 Isom < , < ((1...(♯‘𝐴)), 𝐴))
6		1zzd 9218	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ∈ ℤ)
7		prodmolem2.5	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℕ)
8	7	nnzd 9312	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℤ)
9	6, 8	fzfigd 10366	. . . . . . . . . . 11 ⊢ (𝜑 → (1...𝑁) ∈ Fin)
10		prodmolem2.8	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑓:(1...𝑁)–1-1-onto→𝐴)
11	9, 10	fihasheqf1od 10703	. . . . . . . . . 10 ⊢ (𝜑 → (♯‘(1...𝑁)) = (♯‘𝐴))
12	7	nnnn0d 9167	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
13		hashfz1 10696	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ₀ → (♯‘(1...𝑁)) = 𝑁)
14	12, 13	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → (♯‘(1...𝑁)) = 𝑁)
15	11, 14	eqtr3d 2200	. . . . . . . . 9 ⊢ (𝜑 → (♯‘𝐴) = 𝑁)
16	15	oveq2d 5858	. . . . . . . 8 ⊢ (𝜑 → (1...(♯‘𝐴)) = (1...𝑁))
17		isoeq4 5772	. . . . . . . 8 ⊢ ((1...(♯‘𝐴)) = (1...𝑁) → (𝐾 Isom < , < ((1...(♯‘𝐴)), 𝐴) ↔ 𝐾 Isom < , < ((1...𝑁), 𝐴)))
18	16, 17	syl 14	. . . . . . 7 ⊢ (𝜑 → (𝐾 Isom < , < ((1...(♯‘𝐴)), 𝐴) ↔ 𝐾 Isom < , < ((1...𝑁), 𝐴)))
19	5, 18	mpbid 146	. . . . . 6 ⊢ (𝜑 → 𝐾 Isom < , < ((1...𝑁), 𝐴))
20		isof1o 5775	. . . . . 6 ⊢ (𝐾 Isom < , < ((1...𝑁), 𝐴) → 𝐾:(1...𝑁)–1-1-onto→𝐴)
21		f1of 5432	. . . . . 6 ⊢ (𝐾:(1...𝑁)–1-1-onto→𝐴 → 𝐾:(1...𝑁)⟶𝐴)
22	19, 20, 21	3syl 17	. . . . 5 ⊢ (𝜑 → 𝐾:(1...𝑁)⟶𝐴)
23		nnuz 9501	. . . . . . 7 ⊢ ℕ = (ℤ_≥‘1)
24	7, 23	eleqtrdi 2259	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘1))
25		eluzfz2 9967	. . . . . 6 ⊢ (𝑁 ∈ (ℤ_≥‘1) → 𝑁 ∈ (1...𝑁))
26	24, 25	syl 14	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ (1...𝑁))
27	22, 26	ffvelrnd 5621	. . . 4 ⊢ (𝜑 → (𝐾‘𝑁) ∈ 𝐴)
28	4, 27	sseldd 3143	. . 3 ⊢ (𝜑 → (𝐾‘𝑁) ∈ (ℤ_≥‘𝑀))
29	4	sselda 3142	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝑝 ∈ (ℤ_≥‘𝑀))
30	19, 20	syl 14	. . . . . . . . 9 ⊢ (𝜑 → 𝐾:(1...𝑁)–1-1-onto→𝐴)
31		f1ocnvfv2 5746	. . . . . . . . 9 ⊢ ((𝐾:(1...𝑁)–1-1-onto→𝐴 ∧ 𝑝 ∈ 𝐴) → (𝐾‘(^◡𝐾‘𝑝)) = 𝑝)
32	30, 31	sylan 281	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (𝐾‘(^◡𝐾‘𝑝)) = 𝑝)
33		f1ocnv 5445	. . . . . . . . . . . 12 ⊢ (𝐾:(1...𝑁)–1-1-onto→𝐴 → ^◡𝐾:𝐴–1-1-onto→(1...𝑁))
34		f1of 5432	. . . . . . . . . . . 12 ⊢ (^◡𝐾:𝐴–1-1-onto→(1...𝑁) → ^◡𝐾:𝐴⟶(1...𝑁))
35	30, 33, 34	3syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ^◡𝐾:𝐴⟶(1...𝑁))
36	35	ffvelrnda 5620	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (^◡𝐾‘𝑝) ∈ (1...𝑁))
37		elfzle2 9963	. . . . . . . . . 10 ⊢ ((^◡𝐾‘𝑝) ∈ (1...𝑁) → (^◡𝐾‘𝑝) ≤ 𝑁)
38	36, 37	syl 14	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (^◡𝐾‘𝑝) ≤ 𝑁)
39	19	adantr 274	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝐾 Isom < , < ((1...𝑁), 𝐴))
40		fzssuz 10000	. . . . . . . . . . . . 13 ⊢ (1...𝑁) ⊆ (ℤ_≥‘1)
41		uzssz 9485	. . . . . . . . . . . . . 14 ⊢ (ℤ_≥‘1) ⊆ ℤ
42		zssre 9198	. . . . . . . . . . . . . 14 ⊢ ℤ ⊆ ℝ
43	41, 42	sstri 3151	. . . . . . . . . . . . 13 ⊢ (ℤ_≥‘1) ⊆ ℝ
44	40, 43	sstri 3151	. . . . . . . . . . . 12 ⊢ (1...𝑁) ⊆ ℝ
45		ressxr 7942	. . . . . . . . . . . 12 ⊢ ℝ ⊆ ℝ^*
46	44, 45	sstri 3151	. . . . . . . . . . 11 ⊢ (1...𝑁) ⊆ ℝ^*
47	46	a1i 9	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (1...𝑁) ⊆ ℝ^*)
48		uzssz 9485	. . . . . . . . . . . . . 14 ⊢ (ℤ_≥‘𝑀) ⊆ ℤ
49	48, 42	sstri 3151	. . . . . . . . . . . . 13 ⊢ (ℤ_≥‘𝑀) ⊆ ℝ
50	49, 45	sstri 3151	. . . . . . . . . . . 12 ⊢ (ℤ_≥‘𝑀) ⊆ ℝ^*
51	4, 50	sstrdi 3154	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ⊆ ℝ^*)
52	51	adantr 274	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝐴 ⊆ ℝ^*)
53	26	adantr 274	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝑁 ∈ (1...𝑁))
54		leisorel 10750	. . . . . . . . . 10 ⊢ ((𝐾 Isom < , < ((1...𝑁), 𝐴) ∧ ((1...𝑁) ⊆ ℝ^* ∧ 𝐴 ⊆ ℝ^*) ∧ ((^◡𝐾‘𝑝) ∈ (1...𝑁) ∧ 𝑁 ∈ (1...𝑁))) → ((^◡𝐾‘𝑝) ≤ 𝑁 ↔ (𝐾‘(^◡𝐾‘𝑝)) ≤ (𝐾‘𝑁)))
55	39, 47, 52, 36, 53, 54	syl122anc 1237	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → ((^◡𝐾‘𝑝) ≤ 𝑁 ↔ (𝐾‘(^◡𝐾‘𝑝)) ≤ (𝐾‘𝑁)))
56	38, 55	mpbid 146	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (𝐾‘(^◡𝐾‘𝑝)) ≤ (𝐾‘𝑁))
57	32, 56	eqbrtrrd 4006	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝑝 ≤ (𝐾‘𝑁))
58	4, 48	sstrdi 3154	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ⊆ ℤ)
59	58	sselda 3142	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝑝 ∈ ℤ)
60	48, 28	sselid 3140	. . . . . . . . 9 ⊢ (𝜑 → (𝐾‘𝑁) ∈ ℤ)
61	60	adantr 274	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (𝐾‘𝑁) ∈ ℤ)
62		eluz 9479	. . . . . . . 8 ⊢ ((𝑝 ∈ ℤ ∧ (𝐾‘𝑁) ∈ ℤ) → ((𝐾‘𝑁) ∈ (ℤ_≥‘𝑝) ↔ 𝑝 ≤ (𝐾‘𝑁)))
63	59, 61, 62	syl2anc 409	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → ((𝐾‘𝑁) ∈ (ℤ_≥‘𝑝) ↔ 𝑝 ≤ (𝐾‘𝑁)))
64	57, 63	mpbird 166	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (𝐾‘𝑁) ∈ (ℤ_≥‘𝑝))
65		elfzuzb 9954	. . . . . 6 ⊢ (𝑝 ∈ (𝑀...(𝐾‘𝑁)) ↔ (𝑝 ∈ (ℤ_≥‘𝑀) ∧ (𝐾‘𝑁) ∈ (ℤ_≥‘𝑝)))
66	29, 64, 65	sylanbrc 414	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝑝 ∈ (𝑀...(𝐾‘𝑁)))
67	66	ex 114	. . . 4 ⊢ (𝜑 → (𝑝 ∈ 𝐴 → 𝑝 ∈ (𝑀...(𝐾‘𝑁))))
68	67	ssrdv 3148	. . 3 ⊢ (𝜑 → 𝐴 ⊆ (𝑀...(𝐾‘𝑁)))
69	1, 2, 3, 28, 68	fproddccvg 11513	. 2 ⊢ (𝜑 → seq𝑀( · , 𝐹) ⇝ (seq𝑀( · , 𝐹)‘(𝐾‘𝑁)))
70		mulid2 7897	. . . . 5 ⊢ (𝑚 ∈ ℂ → (1 · 𝑚) = 𝑚)
71	70	adantl 275	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ ℂ) → (1 · 𝑚) = 𝑚)
72		mulid1 7896	. . . . 5 ⊢ (𝑚 ∈ ℂ → (𝑚 · 1) = 𝑚)
73	72	adantl 275	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ ℂ) → (𝑚 · 1) = 𝑚)
74		mulcl 7880	. . . . 5 ⊢ ((𝑚 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑚 · 𝑥) ∈ ℂ)
75	74	adantl 275	. . . 4 ⊢ ((𝜑 ∧ (𝑚 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑚 · 𝑥) ∈ ℂ)
76		1cnd 7915	. . . 4 ⊢ (𝜑 → 1 ∈ ℂ)
77	26, 16	eleqtrrd 2246	. . . 4 ⊢ (𝜑 → 𝑁 ∈ (1...(♯‘𝐴)))
78		eluzelz 9475	. . . . . 6 ⊢ (𝑚 ∈ (ℤ_≥‘𝑀) → 𝑚 ∈ ℤ)
79		simpr 109	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) ∧ 𝑚 ∈ 𝐴) → 𝑚 ∈ 𝐴)
80	2	ralrimiva 2539	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
81	80	ad2antrr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) ∧ 𝑚 ∈ 𝐴) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
82		nfcsb1v 3078	. . . . . . . . . 10 ⊢ Ⅎ𝑘⦋𝑚 / 𝑘⦌𝐵
83	82	nfel1 2319	. . . . . . . . 9 ⊢ Ⅎ𝑘⦋𝑚 / 𝑘⦌𝐵 ∈ ℂ
84		csbeq1a 3054	. . . . . . . . . 10 ⊢ (𝑘 = 𝑚 → 𝐵 = ⦋𝑚 / 𝑘⦌𝐵)
85	84	eleq1d 2235	. . . . . . . . 9 ⊢ (𝑘 = 𝑚 → (𝐵 ∈ ℂ ↔ ⦋𝑚 / 𝑘⦌𝐵 ∈ ℂ))
86	83, 85	rspc 2824	. . . . . . . 8 ⊢ (𝑚 ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋𝑚 / 𝑘⦌𝐵 ∈ ℂ))
87	79, 81, 86	sylc 62	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) ∧ 𝑚 ∈ 𝐴) → ⦋𝑚 / 𝑘⦌𝐵 ∈ ℂ)
88		1cnd 7915	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) ∧ ¬ 𝑚 ∈ 𝐴) → 1 ∈ ℂ)
89		eleq1 2229	. . . . . . . . 9 ⊢ (𝑘 = 𝑚 → (𝑘 ∈ 𝐴 ↔ 𝑚 ∈ 𝐴))
90	89	dcbid 828	. . . . . . . 8 ⊢ (𝑘 = 𝑚 → (DECID 𝑘 ∈ 𝐴 ↔ DECID 𝑚 ∈ 𝐴))
91	3	ralrimiva 2539	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑘 ∈ (ℤ_≥‘𝑀)DECID 𝑘 ∈ 𝐴)
92	91	adantr 274	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → ∀𝑘 ∈ (ℤ_≥‘𝑀)DECID 𝑘 ∈ 𝐴)
93		simpr 109	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → 𝑚 ∈ (ℤ_≥‘𝑀))
94	90, 92, 93	rspcdva 2835	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → DECID 𝑚 ∈ 𝐴)
95	87, 88, 94	ifcldadc 3549	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1) ∈ ℂ)
96		nfcv 2308	. . . . . . 7 ⊢ Ⅎ𝑘𝑚
97		nfv 1516	. . . . . . . 8 ⊢ Ⅎ𝑘 𝑚 ∈ 𝐴
98		nfcv 2308	. . . . . . . 8 ⊢ Ⅎ𝑘1
99	97, 82, 98	nfif 3548	. . . . . . 7 ⊢ Ⅎ𝑘if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1)
100	89, 84	ifbieq1d 3542	. . . . . . 7 ⊢ (𝑘 = 𝑚 → if(𝑘 ∈ 𝐴, 𝐵, 1) = if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1))
101	96, 99, 100, 1	fvmptf 5578	. . . . . 6 ⊢ ((𝑚 ∈ ℤ ∧ if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1) ∈ ℂ) → (𝐹‘𝑚) = if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1))
102	78, 95, 101	syl2an2 584	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → (𝐹‘𝑚) = if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1))
103	102, 95	eqeltrd 2243	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → (𝐹‘𝑚) ∈ ℂ)
104		prodmodclem2.4	. . . . . 6 ⊢ 𝐻 = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝐾‘𝑗) / 𝑘⦌𝐵, 1))
105		breq1 3985	. . . . . . 7 ⊢ (𝑗 = 𝑚 → (𝑗 ≤ (♯‘𝐴) ↔ 𝑚 ≤ (♯‘𝐴)))
106		fveq2 5486	. . . . . . . 8 ⊢ (𝑗 = 𝑚 → (𝐾‘𝑗) = (𝐾‘𝑚))
107	106	csbeq1d 3052	. . . . . . 7 ⊢ (𝑗 = 𝑚 → ⦋(𝐾‘𝑗) / 𝑘⦌𝐵 = ⦋(𝐾‘𝑚) / 𝑘⦌𝐵)
108	105, 107	ifbieq1d 3542	. . . . . 6 ⊢ (𝑗 = 𝑚 → if(𝑗 ≤ (♯‘𝐴), ⦋(𝐾‘𝑗) / 𝑘⦌𝐵, 1) = if(𝑚 ≤ (♯‘𝐴), ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 1))
109		elnnuz 9502	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ ↔ 𝑚 ∈ (ℤ_≥‘1))
110	109	biimpri 132	. . . . . . 7 ⊢ (𝑚 ∈ (ℤ_≥‘1) → 𝑚 ∈ ℕ)
111	110	adantl 275	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) → 𝑚 ∈ ℕ)
112	22	ad2antrr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → 𝐾:(1...𝑁)⟶𝐴)
113		1zzd 9218	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → 1 ∈ ℤ)
114	8	ad2antrr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → 𝑁 ∈ ℤ)
115		eluzelz 9475	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ (ℤ_≥‘1) → 𝑚 ∈ ℤ)
116	115	ad2antlr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → 𝑚 ∈ ℤ)
117	113, 114, 116	3jca 1167	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → (1 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ))
118		eluzle 9478	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ (ℤ_≥‘1) → 1 ≤ 𝑚)
119	118	ad2antlr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → 1 ≤ 𝑚)
120		simpr 109	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → 𝑚 ≤ (♯‘𝐴))
121	15	ad2antrr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → (♯‘𝐴) = 𝑁)
122	120, 121	breqtrd 4008	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → 𝑚 ≤ 𝑁)
123	119, 122	jca 304	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → (1 ≤ 𝑚 ∧ 𝑚 ≤ 𝑁))
124		elfz2 9951	. . . . . . . . . 10 ⊢ (𝑚 ∈ (1...𝑁) ↔ ((1 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ) ∧ (1 ≤ 𝑚 ∧ 𝑚 ≤ 𝑁)))
125	117, 123, 124	sylanbrc 414	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → 𝑚 ∈ (1...𝑁))
126	112, 125	ffvelrnd 5621	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → (𝐾‘𝑚) ∈ 𝐴)
127	80	ad2antrr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
128		nfcsb1v 3078	. . . . . . . . . 10 ⊢ Ⅎ𝑘⦋(𝐾‘𝑚) / 𝑘⦌𝐵
129	128	nfel1 2319	. . . . . . . . 9 ⊢ Ⅎ𝑘⦋(𝐾‘𝑚) / 𝑘⦌𝐵 ∈ ℂ
130		csbeq1a 3054	. . . . . . . . . 10 ⊢ (𝑘 = (𝐾‘𝑚) → 𝐵 = ⦋(𝐾‘𝑚) / 𝑘⦌𝐵)
131	130	eleq1d 2235	. . . . . . . . 9 ⊢ (𝑘 = (𝐾‘𝑚) → (𝐵 ∈ ℂ ↔ ⦋(𝐾‘𝑚) / 𝑘⦌𝐵 ∈ ℂ))
132	129, 131	rspc 2824	. . . . . . . 8 ⊢ ((𝐾‘𝑚) ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋(𝐾‘𝑚) / 𝑘⦌𝐵 ∈ ℂ))
133	126, 127, 132	sylc 62	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → ⦋(𝐾‘𝑚) / 𝑘⦌𝐵 ∈ ℂ)
134		1cnd 7915	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ ¬ 𝑚 ≤ (♯‘𝐴)) → 1 ∈ ℂ)
135	111	nnzd 9312	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) → 𝑚 ∈ ℤ)
136	15, 8	eqeltrd 2243	. . . . . . . . 9 ⊢ (𝜑 → (♯‘𝐴) ∈ ℤ)
137	136	adantr 274	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) → (♯‘𝐴) ∈ ℤ)
138		zdcle 9267	. . . . . . . 8 ⊢ ((𝑚 ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ) → DECID 𝑚 ≤ (♯‘𝐴))
139	135, 137, 138	syl2anc 409	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) → DECID 𝑚 ≤ (♯‘𝐴))
140	133, 134, 139	ifcldadc 3549	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) → if(𝑚 ≤ (♯‘𝐴), ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 1) ∈ ℂ)
141	104, 108, 111, 140	fvmptd3 5579	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) → (𝐻‘𝑚) = if(𝑚 ≤ (♯‘𝐴), ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 1))
142	141, 140	eqeltrd 2243	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) → (𝐻‘𝑚) ∈ ℂ)
143		eldifi 3244	. . . . . . 7 ⊢ (𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → 𝑚 ∈ (𝑀...(𝐾‘(♯‘𝐴))))
144		elfzelz 9960	. . . . . . 7 ⊢ (𝑚 ∈ (𝑀...(𝐾‘(♯‘𝐴))) → 𝑚 ∈ ℤ)
145	143, 144	syl 14	. . . . . 6 ⊢ (𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → 𝑚 ∈ ℤ)
146		eldifn 3245	. . . . . . . . 9 ⊢ (𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → ¬ 𝑚 ∈ 𝐴)
147	146	iffalsed 3530	. . . . . . . 8 ⊢ (𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1) = 1)
148		ax-1cn 7846	. . . . . . . 8 ⊢ 1 ∈ ℂ
149	147, 148	eqeltrdi 2257	. . . . . . 7 ⊢ (𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1) ∈ ℂ)
150	149	adantl 275	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴)) → if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1) ∈ ℂ)
151	145, 150, 101	syl2an2 584	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴)) → (𝐹‘𝑚) = if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1))
152	147	adantl 275	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴)) → if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1) = 1)
153	151, 152	eqtrd 2198	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴)) → (𝐹‘𝑚) = 1)
154		elfzle2 9963	. . . . . . 7 ⊢ (𝑥 ∈ (1...(♯‘𝐴)) → 𝑥 ≤ (♯‘𝐴))
155	154	adantl 275	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝑥 ≤ (♯‘𝐴))
156	155	iftrued 3527	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → if(𝑥 ≤ (♯‘𝐴), ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1) = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵)
157		breq1 3985	. . . . . . 7 ⊢ (𝑗 = 𝑥 → (𝑗 ≤ (♯‘𝐴) ↔ 𝑥 ≤ (♯‘𝐴)))
158		fveq2 5486	. . . . . . . 8 ⊢ (𝑗 = 𝑥 → (𝐾‘𝑗) = (𝐾‘𝑥))
159	158	csbeq1d 3052	. . . . . . 7 ⊢ (𝑗 = 𝑥 → ⦋(𝐾‘𝑗) / 𝑘⦌𝐵 = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵)
160	157, 159	ifbieq1d 3542	. . . . . 6 ⊢ (𝑗 = 𝑥 → if(𝑗 ≤ (♯‘𝐴), ⦋(𝐾‘𝑗) / 𝑘⦌𝐵, 1) = if(𝑥 ≤ (♯‘𝐴), ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1))
161		elfznn 9989	. . . . . . 7 ⊢ (𝑥 ∈ (1...(♯‘𝐴)) → 𝑥 ∈ ℕ)
162	161	adantl 275	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝑥 ∈ ℕ)
163	22	adantr 274	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝐾:(1...𝑁)⟶𝐴)
164		simpr 109	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝑥 ∈ (1...(♯‘𝐴)))
165	15	adantr 274	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (♯‘𝐴) = 𝑁)
166	165	oveq2d 5858	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (1...(♯‘𝐴)) = (1...𝑁))
167	164, 166	eleqtrd 2245	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝑥 ∈ (1...𝑁))
168	163, 167	ffvelrnd 5621	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐾‘𝑥) ∈ 𝐴)
169	80	adantr 274	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
170		nfcsb1v 3078	. . . . . . . . . 10 ⊢ Ⅎ𝑘⦋(𝐾‘𝑥) / 𝑘⦌𝐵
171	170	nfel1 2319	. . . . . . . . 9 ⊢ Ⅎ𝑘⦋(𝐾‘𝑥) / 𝑘⦌𝐵 ∈ ℂ
172		csbeq1a 3054	. . . . . . . . . 10 ⊢ (𝑘 = (𝐾‘𝑥) → 𝐵 = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵)
173	172	eleq1d 2235	. . . . . . . . 9 ⊢ (𝑘 = (𝐾‘𝑥) → (𝐵 ∈ ℂ ↔ ⦋(𝐾‘𝑥) / 𝑘⦌𝐵 ∈ ℂ))
174	171, 173	rspc 2824	. . . . . . . 8 ⊢ ((𝐾‘𝑥) ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋(𝐾‘𝑥) / 𝑘⦌𝐵 ∈ ℂ))
175	168, 169, 174	sylc 62	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → ⦋(𝐾‘𝑥) / 𝑘⦌𝐵 ∈ ℂ)
176	156, 175	eqeltrd 2243	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → if(𝑥 ≤ (♯‘𝐴), ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1) ∈ ℂ)
177	104, 160, 162, 176	fvmptd3 5579	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐻‘𝑥) = if(𝑥 ≤ (♯‘𝐴), ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1))
178	4	adantr 274	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝐴 ⊆ (ℤ_≥‘𝑀))
179	178, 48	sstrdi 3154	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝐴 ⊆ ℤ)
180	179, 168	sseldd 3143	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐾‘𝑥) ∈ ℤ)
181	168	iftrued 3527	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1) = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵)
182	181, 175	eqeltrd 2243	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1) ∈ ℂ)
183		nfcv 2308	. . . . . . . 8 ⊢ Ⅎ𝑘(𝐾‘𝑥)
184		nfv 1516	. . . . . . . . 9 ⊢ Ⅎ𝑘(𝐾‘𝑥) ∈ 𝐴
185	184, 170, 98	nfif 3548	. . . . . . . 8 ⊢ Ⅎ𝑘if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1)
186		eleq1 2229	. . . . . . . . 9 ⊢ (𝑘 = (𝐾‘𝑥) → (𝑘 ∈ 𝐴 ↔ (𝐾‘𝑥) ∈ 𝐴))
187	186, 172	ifbieq1d 3542	. . . . . . . 8 ⊢ (𝑘 = (𝐾‘𝑥) → if(𝑘 ∈ 𝐴, 𝐵, 1) = if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1))
188	183, 185, 187, 1	fvmptf 5578	. . . . . . 7 ⊢ (((𝐾‘𝑥) ∈ ℤ ∧ if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1) ∈ ℂ) → (𝐹‘(𝐾‘𝑥)) = if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1))
189	180, 182, 188	syl2anc 409	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐹‘(𝐾‘𝑥)) = if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1))
190	189, 181	eqtrd 2198	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐹‘(𝐾‘𝑥)) = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵)
191	156, 177, 190	3eqtr4d 2208	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐻‘𝑥) = (𝐹‘(𝐾‘𝑥)))
192	71, 73, 75, 76, 5, 77, 4, 103, 142, 153, 191	seq3coll 10755	. . 3 ⊢ (𝜑 → (seq𝑀( · , 𝐹)‘(𝐾‘𝑁)) = (seq1( · , 𝐻)‘𝑁))
193		prodmodc.3	. . . 4 ⊢ 𝐺 = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑘⦌𝐵, 1))
194	7, 7	jca 304	. . . 4 ⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 𝑁 ∈ ℕ))
195	1, 2, 193, 104, 194, 10, 30	prodmodclem3 11516	. . 3 ⊢ (𝜑 → (seq1( · , 𝐺)‘𝑁) = (seq1( · , 𝐻)‘𝑁))
196	192, 195	eqtr4d 2201	. 2 ⊢ (𝜑 → (seq𝑀( · , 𝐹)‘(𝐾‘𝑁)) = (seq1( · , 𝐺)‘𝑁))
197	69, 196	breqtrd 4008	1 ⊢ (𝜑 → seq𝑀( · , 𝐹) ⇝ (seq1( · , 𝐺)‘𝑁))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 103 ↔ wb 104 DECID wdc 824 ∧ w3a 968 = wceq 1343 ∈ wcel 2136 ∀wral 2444 ⦋csb 3045 ∖ cdif 3113 ⊆ wss 3116 ifcif 3520 class class class wbr 3982 ↦ cmpt 4043 ^◡ccnv 4603 ⟶wf 5184 –1-1-onto→wf1o 5187 ‘cfv 5188 Isom wiso 5189 (class class class)co 5842 ℂcc 7751 ℝcr 7752 1c1 7754 · cmul 7758 ℝ^*cxr 7932 < clt 7933 ≤ cle 7934 ℕcn 8857 ℕ₀cn0 9114 ℤcz 9191 ℤ_≥cuz 9466 ...cfz 9944 seqcseq 10380 ♯chash 10688 ⇝ cli 11219

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 604 ax-in2 605 ax-io 699 ax-5 1435 ax-7 1436 ax-gen 1437 ax-ie1 1481 ax-ie2 1482 ax-8 1492 ax-10 1493 ax-11 1494 ax-i12 1495 ax-bndl 1497 ax-4 1498 ax-17 1514 ax-i9 1518 ax-ial 1522 ax-i5r 1523 ax-13 2138 ax-14 2139 ax-ext 2147 ax-coll 4097 ax-sep 4100 ax-nul 4108 ax-pow 4153 ax-pr 4187 ax-un 4411 ax-setind 4514 ax-iinf 4565 ax-cnex 7844 ax-resscn 7845 ax-1cn 7846 ax-1re 7847 ax-icn 7848 ax-addcl 7849 ax-addrcl 7850 ax-mulcl 7851 ax-mulrcl 7852 ax-addcom 7853 ax-mulcom 7854 ax-addass 7855 ax-mulass 7856 ax-distr 7857 ax-i2m1 7858 ax-0lt1 7859 ax-1rid 7860 ax-0id 7861 ax-rnegex 7862 ax-precex 7863 ax-cnre 7864 ax-pre-ltirr 7865 ax-pre-ltwlin 7866 ax-pre-lttrn 7867 ax-pre-apti 7868 ax-pre-ltadd 7869 ax-pre-mulgt0 7870 ax-pre-mulext 7871

This theorem depends on definitions: df-bi 116 df-dc 825 df-3or 969 df-3an 970 df-tru 1346 df-fal 1349 df-nf 1449 df-sb 1751 df-eu 2017 df-mo 2018 df-clab 2152 df-cleq 2158 df-clel 2161 df-nfc 2297 df-ne 2337 df-nel 2432 df-ral 2449 df-rex 2450 df-reu 2451 df-rmo 2452 df-rab 2453 df-v 2728 df-sbc 2952 df-csb 3046 df-dif 3118 df-un 3120 df-in 3122 df-ss 3129 df-nul 3410 df-if 3521 df-pw 3561 df-sn 3582 df-pr 3583 df-op 3585 df-uni 3790 df-int 3825 df-iun 3868 df-br 3983 df-opab 4044 df-mpt 4045 df-tr 4081 df-id 4271 df-po 4274 df-iso 4275 df-iord 4344 df-on 4346 df-ilim 4347 df-suc 4349 df-iom 4568 df-xp 4610 df-rel 4611 df-cnv 4612 df-co 4613 df-dm 4614 df-rn 4615 df-res 4616 df-ima 4617 df-iota 5153 df-fun 5190 df-fn 5191 df-f 5192 df-f1 5193 df-fo 5194 df-f1o 5195 df-fv 5196 df-isom 5197 df-riota 5798 df-ov 5845 df-oprab 5846 df-mpo 5847 df-1st 6108 df-2nd 6109 df-recs 6273 df-frec 6359 df-1o 6384 df-er 6501 df-en 6707 df-dom 6708 df-fin 6709 df-pnf 7935 df-mnf 7936 df-xr 7937 df-ltxr 7938 df-le 7939 df-sub 8071 df-neg 8072 df-reap 8473 df-ap 8480 df-div 8569 df-inn 8858 df-2 8916 df-n0 9115 df-z 9192 df-uz 9467 df-rp 9590 df-fz 9945 df-fzo 10078 df-seqfrec 10381 df-exp 10455 df-ihash 10689 df-cj 10784 df-rsqrt 10940 df-abs 10941 df-clim 11220

This theorem is referenced by: prodmodclem2 11518 zproddc 11520

W3C validator