prodmodclem2a - Intuitionistic Logic Explorer

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

Theorem prodmodclem2a 12200

Description: Lemma for prodmodc 12202. (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 9550	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ∈ ℤ)
7		prodmolem2.5	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℕ)
8	7	nnzd 9645	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℤ)
9	6, 8	fzfigd 10739	. . . . . . . . . . 11 ⊢ (𝜑 → (1...𝑁) ∈ Fin)
10		prodmolem2.8	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑓:(1...𝑁)–1-1-onto→𝐴)
11	9, 10	fihasheqf1od 11097	. . . . . . . . . 10 ⊢ (𝜑 → (♯‘(1...𝑁)) = (♯‘𝐴))
12	7	nnnn0d 9499	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
13		hashfz1 11091	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ₀ → (♯‘(1...𝑁)) = 𝑁)
14	12, 13	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → (♯‘(1...𝑁)) = 𝑁)
15	11, 14	eqtr3d 2266	. . . . . . . . 9 ⊢ (𝜑 → (♯‘𝐴) = 𝑁)
16	15	oveq2d 6044	. . . . . . . 8 ⊢ (𝜑 → (1...(♯‘𝐴)) = (1...𝑁))
17		isoeq4 5955	. . . . . . . 8 ⊢ ((1...(♯‘𝐴)) = (1...𝑁) → (𝐾 Isom < , < ((1...(♯‘𝐴)), 𝐴) ↔ 𝐾 Isom < , < ((1...𝑁), 𝐴)))
18	16, 17	syl 14	. . . . . . 7 ⊢ (𝜑 → (𝐾 Isom < , < ((1...(♯‘𝐴)), 𝐴) ↔ 𝐾 Isom < , < ((1...𝑁), 𝐴)))
19	5, 18	mpbid 147	. . . . . 6 ⊢ (𝜑 → 𝐾 Isom < , < ((1...𝑁), 𝐴))
20		isof1o 5958	. . . . . 6 ⊢ (𝐾 Isom < , < ((1...𝑁), 𝐴) → 𝐾:(1...𝑁)–1-1-onto→𝐴)
21		f1of 5592	. . . . . 6 ⊢ (𝐾:(1...𝑁)–1-1-onto→𝐴 → 𝐾:(1...𝑁)⟶𝐴)
22	19, 20, 21	3syl 17	. . . . 5 ⊢ (𝜑 → 𝐾:(1...𝑁)⟶𝐴)
23		nnuz 9836	. . . . . . 7 ⊢ ℕ = (ℤ_≥‘1)
24	7, 23	eleqtrdi 2324	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘1))
25		eluzfz2 10312	. . . . . 6 ⊢ (𝑁 ∈ (ℤ_≥‘1) → 𝑁 ∈ (1...𝑁))
26	24, 25	syl 14	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ (1...𝑁))
27	22, 26	ffvelcdmd 5791	. . . 4 ⊢ (𝜑 → (𝐾‘𝑁) ∈ 𝐴)
28	4, 27	sseldd 3229	. . 3 ⊢ (𝜑 → (𝐾‘𝑁) ∈ (ℤ_≥‘𝑀))
29	4	sselda 3228	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝑝 ∈ (ℤ_≥‘𝑀))
30	19, 20	syl 14	. . . . . . . . 9 ⊢ (𝜑 → 𝐾:(1...𝑁)–1-1-onto→𝐴)
31		f1ocnvfv2 5929	. . . . . . . . 9 ⊢ ((𝐾:(1...𝑁)–1-1-onto→𝐴 ∧ 𝑝 ∈ 𝐴) → (𝐾‘(^◡𝐾‘𝑝)) = 𝑝)
32	30, 31	sylan 283	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (𝐾‘(^◡𝐾‘𝑝)) = 𝑝)
33		f1ocnv 5605	. . . . . . . . . . . 12 ⊢ (𝐾:(1...𝑁)–1-1-onto→𝐴 → ^◡𝐾:𝐴–1-1-onto→(1...𝑁))
34		f1of 5592	. . . . . . . . . . . 12 ⊢ (^◡𝐾:𝐴–1-1-onto→(1...𝑁) → ^◡𝐾:𝐴⟶(1...𝑁))
35	30, 33, 34	3syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ^◡𝐾:𝐴⟶(1...𝑁))
36	35	ffvelcdmda 5790	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (^◡𝐾‘𝑝) ∈ (1...𝑁))
37		elfzle2 10308	. . . . . . . . . 10 ⊢ ((^◡𝐾‘𝑝) ∈ (1...𝑁) → (^◡𝐾‘𝑝) ≤ 𝑁)
38	36, 37	syl 14	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (^◡𝐾‘𝑝) ≤ 𝑁)
39	19	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝐾 Isom < , < ((1...𝑁), 𝐴))
40		fzssuz 10345	. . . . . . . . . . . . 13 ⊢ (1...𝑁) ⊆ (ℤ_≥‘1)
41		uzssz 9820	. . . . . . . . . . . . . 14 ⊢ (ℤ_≥‘1) ⊆ ℤ
42		zssre 9530	. . . . . . . . . . . . . 14 ⊢ ℤ ⊆ ℝ
43	41, 42	sstri 3237	. . . . . . . . . . . . 13 ⊢ (ℤ_≥‘1) ⊆ ℝ
44	40, 43	sstri 3237	. . . . . . . . . . . 12 ⊢ (1...𝑁) ⊆ ℝ
45		ressxr 8265	. . . . . . . . . . . 12 ⊢ ℝ ⊆ ℝ^*
46	44, 45	sstri 3237	. . . . . . . . . . 11 ⊢ (1...𝑁) ⊆ ℝ^*
47	46	a1i 9	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (1...𝑁) ⊆ ℝ^*)
48		uzssz 9820	. . . . . . . . . . . . . 14 ⊢ (ℤ_≥‘𝑀) ⊆ ℤ
49	48, 42	sstri 3237	. . . . . . . . . . . . 13 ⊢ (ℤ_≥‘𝑀) ⊆ ℝ
50	49, 45	sstri 3237	. . . . . . . . . . . 12 ⊢ (ℤ_≥‘𝑀) ⊆ ℝ^*
51	4, 50	sstrdi 3240	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ⊆ ℝ^*)
52	51	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝐴 ⊆ ℝ^*)
53	26	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝑁 ∈ (1...𝑁))
54		leisorel 11147	. . . . . . . . . 10 ⊢ ((𝐾 Isom < , < ((1...𝑁), 𝐴) ∧ ((1...𝑁) ⊆ ℝ^* ∧ 𝐴 ⊆ ℝ^*) ∧ ((^◡𝐾‘𝑝) ∈ (1...𝑁) ∧ 𝑁 ∈ (1...𝑁))) → ((^◡𝐾‘𝑝) ≤ 𝑁 ↔ (𝐾‘(^◡𝐾‘𝑝)) ≤ (𝐾‘𝑁)))
55	39, 47, 52, 36, 53, 54	syl122anc 1283	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → ((^◡𝐾‘𝑝) ≤ 𝑁 ↔ (𝐾‘(^◡𝐾‘𝑝)) ≤ (𝐾‘𝑁)))
56	38, 55	mpbid 147	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (𝐾‘(^◡𝐾‘𝑝)) ≤ (𝐾‘𝑁))
57	32, 56	eqbrtrrd 4117	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝑝 ≤ (𝐾‘𝑁))
58	4, 48	sstrdi 3240	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ⊆ ℤ)
59	58	sselda 3228	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝑝 ∈ ℤ)
60	48, 28	sselid 3226	. . . . . . . . 9 ⊢ (𝜑 → (𝐾‘𝑁) ∈ ℤ)
61	60	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (𝐾‘𝑁) ∈ ℤ)
62		eluz 9813	. . . . . . . 8 ⊢ ((𝑝 ∈ ℤ ∧ (𝐾‘𝑁) ∈ ℤ) → ((𝐾‘𝑁) ∈ (ℤ_≥‘𝑝) ↔ 𝑝 ≤ (𝐾‘𝑁)))
63	59, 61, 62	syl2anc 411	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → ((𝐾‘𝑁) ∈ (ℤ_≥‘𝑝) ↔ 𝑝 ≤ (𝐾‘𝑁)))
64	57, 63	mpbird 167	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (𝐾‘𝑁) ∈ (ℤ_≥‘𝑝))
65		elfzuzb 10299	. . . . . 6 ⊢ (𝑝 ∈ (𝑀...(𝐾‘𝑁)) ↔ (𝑝 ∈ (ℤ_≥‘𝑀) ∧ (𝐾‘𝑁) ∈ (ℤ_≥‘𝑝)))
66	29, 64, 65	sylanbrc 417	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝑝 ∈ (𝑀...(𝐾‘𝑁)))
67	66	ex 115	. . . 4 ⊢ (𝜑 → (𝑝 ∈ 𝐴 → 𝑝 ∈ (𝑀...(𝐾‘𝑁))))
68	67	ssrdv 3234	. . 3 ⊢ (𝜑 → 𝐴 ⊆ (𝑀...(𝐾‘𝑁)))
69	1, 2, 3, 28, 68	fproddccvg 12196	. 2 ⊢ (𝜑 → seq𝑀( · , 𝐹) ⇝ (seq𝑀( · , 𝐹)‘(𝐾‘𝑁)))
70		mullid 8220	. . . . 5 ⊢ (𝑚 ∈ ℂ → (1 · 𝑚) = 𝑚)
71	70	adantl 277	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ ℂ) → (1 · 𝑚) = 𝑚)
72		mulrid 8219	. . . . 5 ⊢ (𝑚 ∈ ℂ → (𝑚 · 1) = 𝑚)
73	72	adantl 277	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ ℂ) → (𝑚 · 1) = 𝑚)
74		mulcl 8202	. . . . 5 ⊢ ((𝑚 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑚 · 𝑥) ∈ ℂ)
75	74	adantl 277	. . . 4 ⊢ ((𝜑 ∧ (𝑚 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑚 · 𝑥) ∈ ℂ)
76		1cnd 8238	. . . 4 ⊢ (𝜑 → 1 ∈ ℂ)
77	26, 16	eleqtrrd 2311	. . . 4 ⊢ (𝜑 → 𝑁 ∈ (1...(♯‘𝐴)))
78		eluzelz 9809	. . . . . 6 ⊢ (𝑚 ∈ (ℤ_≥‘𝑀) → 𝑚 ∈ ℤ)
79		simpr 110	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) ∧ 𝑚 ∈ 𝐴) → 𝑚 ∈ 𝐴)
80	2	ralrimiva 2606	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
81	80	ad2antrr 488	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) ∧ 𝑚 ∈ 𝐴) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
82		nfcsb1v 3161	. . . . . . . . . 10 ⊢ Ⅎ𝑘⦋𝑚 / 𝑘⦌𝐵
83	82	nfel1 2386	. . . . . . . . 9 ⊢ Ⅎ𝑘⦋𝑚 / 𝑘⦌𝐵 ∈ ℂ
84		csbeq1a 3137	. . . . . . . . . 10 ⊢ (𝑘 = 𝑚 → 𝐵 = ⦋𝑚 / 𝑘⦌𝐵)
85	84	eleq1d 2300	. . . . . . . . 9 ⊢ (𝑘 = 𝑚 → (𝐵 ∈ ℂ ↔ ⦋𝑚 / 𝑘⦌𝐵 ∈ ℂ))
86	83, 85	rspc 2905	. . . . . . . 8 ⊢ (𝑚 ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋𝑚 / 𝑘⦌𝐵 ∈ ℂ))
87	79, 81, 86	sylc 62	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) ∧ 𝑚 ∈ 𝐴) → ⦋𝑚 / 𝑘⦌𝐵 ∈ ℂ)
88		1cnd 8238	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) ∧ ¬ 𝑚 ∈ 𝐴) → 1 ∈ ℂ)
89		eleq1 2294	. . . . . . . . 9 ⊢ (𝑘 = 𝑚 → (𝑘 ∈ 𝐴 ↔ 𝑚 ∈ 𝐴))
90	89	dcbid 846	. . . . . . . 8 ⊢ (𝑘 = 𝑚 → (DECID 𝑘 ∈ 𝐴 ↔ DECID 𝑚 ∈ 𝐴))
91	3	ralrimiva 2606	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑘 ∈ (ℤ_≥‘𝑀)DECID 𝑘 ∈ 𝐴)
92	91	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → ∀𝑘 ∈ (ℤ_≥‘𝑀)DECID 𝑘 ∈ 𝐴)
93		simpr 110	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → 𝑚 ∈ (ℤ_≥‘𝑀))
94	90, 92, 93	rspcdva 2916	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → DECID 𝑚 ∈ 𝐴)
95	87, 88, 94	ifcldadc 3639	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1) ∈ ℂ)
96		nfcv 2375	. . . . . . 7 ⊢ Ⅎ𝑘𝑚
97		nfv 1577	. . . . . . . 8 ⊢ Ⅎ𝑘 𝑚 ∈ 𝐴
98		nfcv 2375	. . . . . . . 8 ⊢ Ⅎ𝑘1
99	97, 82, 98	nfif 3638	. . . . . . 7 ⊢ Ⅎ𝑘if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1)
100	89, 84	ifbieq1d 3632	. . . . . . 7 ⊢ (𝑘 = 𝑚 → if(𝑘 ∈ 𝐴, 𝐵, 1) = if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1))
101	96, 99, 100, 1	fvmptf 5748	. . . . . 6 ⊢ ((𝑚 ∈ ℤ ∧ if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1) ∈ ℂ) → (𝐹‘𝑚) = if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1))
102	78, 95, 101	syl2an2 598	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → (𝐹‘𝑚) = if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1))
103	102, 95	eqeltrd 2308	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → (𝐹‘𝑚) ∈ ℂ)
104		prodmodclem2.4	. . . . . 6 ⊢ 𝐻 = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝐾‘𝑗) / 𝑘⦌𝐵, 1))
105		breq1 4096	. . . . . . 7 ⊢ (𝑗 = 𝑚 → (𝑗 ≤ (♯‘𝐴) ↔ 𝑚 ≤ (♯‘𝐴)))
106		fveq2 5648	. . . . . . . 8 ⊢ (𝑗 = 𝑚 → (𝐾‘𝑗) = (𝐾‘𝑚))
107	106	csbeq1d 3135	. . . . . . 7 ⊢ (𝑗 = 𝑚 → ⦋(𝐾‘𝑗) / 𝑘⦌𝐵 = ⦋(𝐾‘𝑚) / 𝑘⦌𝐵)
108	105, 107	ifbieq1d 3632	. . . . . 6 ⊢ (𝑗 = 𝑚 → if(𝑗 ≤ (♯‘𝐴), ⦋(𝐾‘𝑗) / 𝑘⦌𝐵, 1) = if(𝑚 ≤ (♯‘𝐴), ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 1))
109		elnnuz 9837	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ ↔ 𝑚 ∈ (ℤ_≥‘1))
110	109	biimpri 133	. . . . . . 7 ⊢ (𝑚 ∈ (ℤ_≥‘1) → 𝑚 ∈ ℕ)
111	110	adantl 277	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) → 𝑚 ∈ ℕ)
112	22	ad2antrr 488	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → 𝐾:(1...𝑁)⟶𝐴)
113		1zzd 9550	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → 1 ∈ ℤ)
114	8	ad2antrr 488	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → 𝑁 ∈ ℤ)
115		eluzelz 9809	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ (ℤ_≥‘1) → 𝑚 ∈ ℤ)
116	115	ad2antlr 489	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → 𝑚 ∈ ℤ)
117	113, 114, 116	3jca 1204	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → (1 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ))
118		eluzle 9812	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ (ℤ_≥‘1) → 1 ≤ 𝑚)
119	118	ad2antlr 489	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → 1 ≤ 𝑚)
120		simpr 110	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → 𝑚 ≤ (♯‘𝐴))
121	15	ad2antrr 488	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → (♯‘𝐴) = 𝑁)
122	120, 121	breqtrd 4119	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → 𝑚 ≤ 𝑁)
123	119, 122	jca 306	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → (1 ≤ 𝑚 ∧ 𝑚 ≤ 𝑁))
124		elfz2 10295	. . . . . . . . . 10 ⊢ (𝑚 ∈ (1...𝑁) ↔ ((1 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ) ∧ (1 ≤ 𝑚 ∧ 𝑚 ≤ 𝑁)))
125	117, 123, 124	sylanbrc 417	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → 𝑚 ∈ (1...𝑁))
126	112, 125	ffvelcdmd 5791	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → (𝐾‘𝑚) ∈ 𝐴)
127	80	ad2antrr 488	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
128		nfcsb1v 3161	. . . . . . . . . 10 ⊢ Ⅎ𝑘⦋(𝐾‘𝑚) / 𝑘⦌𝐵
129	128	nfel1 2386	. . . . . . . . 9 ⊢ Ⅎ𝑘⦋(𝐾‘𝑚) / 𝑘⦌𝐵 ∈ ℂ
130		csbeq1a 3137	. . . . . . . . . 10 ⊢ (𝑘 = (𝐾‘𝑚) → 𝐵 = ⦋(𝐾‘𝑚) / 𝑘⦌𝐵)
131	130	eleq1d 2300	. . . . . . . . 9 ⊢ (𝑘 = (𝐾‘𝑚) → (𝐵 ∈ ℂ ↔ ⦋(𝐾‘𝑚) / 𝑘⦌𝐵 ∈ ℂ))
132	129, 131	rspc 2905	. . . . . . . 8 ⊢ ((𝐾‘𝑚) ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋(𝐾‘𝑚) / 𝑘⦌𝐵 ∈ ℂ))
133	126, 127, 132	sylc 62	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ (♯‘𝐴)) → ⦋(𝐾‘𝑚) / 𝑘⦌𝐵 ∈ ℂ)
134		1cnd 8238	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ ¬ 𝑚 ≤ (♯‘𝐴)) → 1 ∈ ℂ)
135	111	nnzd 9645	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) → 𝑚 ∈ ℤ)
136	15, 8	eqeltrd 2308	. . . . . . . . 9 ⊢ (𝜑 → (♯‘𝐴) ∈ ℤ)
137	136	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) → (♯‘𝐴) ∈ ℤ)
138		zdcle 9600	. . . . . . . 8 ⊢ ((𝑚 ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ) → DECID 𝑚 ≤ (♯‘𝐴))
139	135, 137, 138	syl2anc 411	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) → DECID 𝑚 ≤ (♯‘𝐴))
140	133, 134, 139	ifcldadc 3639	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) → if(𝑚 ≤ (♯‘𝐴), ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 1) ∈ ℂ)
141	104, 108, 111, 140	fvmptd3 5749	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) → (𝐻‘𝑚) = if(𝑚 ≤ (♯‘𝐴), ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 1))
142	141, 140	eqeltrd 2308	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) → (𝐻‘𝑚) ∈ ℂ)
143		eldifi 3331	. . . . . . 7 ⊢ (𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → 𝑚 ∈ (𝑀...(𝐾‘(♯‘𝐴))))
144		elfzelz 10305	. . . . . . 7 ⊢ (𝑚 ∈ (𝑀...(𝐾‘(♯‘𝐴))) → 𝑚 ∈ ℤ)
145	143, 144	syl 14	. . . . . 6 ⊢ (𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → 𝑚 ∈ ℤ)
146		eldifn 3332	. . . . . . . . 9 ⊢ (𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → ¬ 𝑚 ∈ 𝐴)
147	146	iffalsed 3619	. . . . . . . 8 ⊢ (𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1) = 1)
148		ax-1cn 8168	. . . . . . . 8 ⊢ 1 ∈ ℂ
149	147, 148	eqeltrdi 2322	. . . . . . 7 ⊢ (𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1) ∈ ℂ)
150	149	adantl 277	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴)) → if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1) ∈ ℂ)
151	145, 150, 101	syl2an2 598	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴)) → (𝐹‘𝑚) = if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1))
152	147	adantl 277	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴)) → if(𝑚 ∈ 𝐴, ⦋𝑚 / 𝑘⦌𝐵, 1) = 1)
153	151, 152	eqtrd 2264	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴)) → (𝐹‘𝑚) = 1)
154		elfzle2 10308	. . . . . . 7 ⊢ (𝑥 ∈ (1...(♯‘𝐴)) → 𝑥 ≤ (♯‘𝐴))
155	154	adantl 277	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝑥 ≤ (♯‘𝐴))
156	155	iftrued 3616	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → if(𝑥 ≤ (♯‘𝐴), ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1) = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵)
157		breq1 4096	. . . . . . 7 ⊢ (𝑗 = 𝑥 → (𝑗 ≤ (♯‘𝐴) ↔ 𝑥 ≤ (♯‘𝐴)))
158		fveq2 5648	. . . . . . . 8 ⊢ (𝑗 = 𝑥 → (𝐾‘𝑗) = (𝐾‘𝑥))
159	158	csbeq1d 3135	. . . . . . 7 ⊢ (𝑗 = 𝑥 → ⦋(𝐾‘𝑗) / 𝑘⦌𝐵 = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵)
160	157, 159	ifbieq1d 3632	. . . . . 6 ⊢ (𝑗 = 𝑥 → if(𝑗 ≤ (♯‘𝐴), ⦋(𝐾‘𝑗) / 𝑘⦌𝐵, 1) = if(𝑥 ≤ (♯‘𝐴), ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1))
161		elfznn 10334	. . . . . . 7 ⊢ (𝑥 ∈ (1...(♯‘𝐴)) → 𝑥 ∈ ℕ)
162	161	adantl 277	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝑥 ∈ ℕ)
163	22	adantr 276	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝐾:(1...𝑁)⟶𝐴)
164		simpr 110	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝑥 ∈ (1...(♯‘𝐴)))
165	15	adantr 276	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (♯‘𝐴) = 𝑁)
166	165	oveq2d 6044	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (1...(♯‘𝐴)) = (1...𝑁))
167	164, 166	eleqtrd 2310	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝑥 ∈ (1...𝑁))
168	163, 167	ffvelcdmd 5791	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐾‘𝑥) ∈ 𝐴)
169	80	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
170		nfcsb1v 3161	. . . . . . . . . 10 ⊢ Ⅎ𝑘⦋(𝐾‘𝑥) / 𝑘⦌𝐵
171	170	nfel1 2386	. . . . . . . . 9 ⊢ Ⅎ𝑘⦋(𝐾‘𝑥) / 𝑘⦌𝐵 ∈ ℂ
172		csbeq1a 3137	. . . . . . . . . 10 ⊢ (𝑘 = (𝐾‘𝑥) → 𝐵 = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵)
173	172	eleq1d 2300	. . . . . . . . 9 ⊢ (𝑘 = (𝐾‘𝑥) → (𝐵 ∈ ℂ ↔ ⦋(𝐾‘𝑥) / 𝑘⦌𝐵 ∈ ℂ))
174	171, 173	rspc 2905	. . . . . . . 8 ⊢ ((𝐾‘𝑥) ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋(𝐾‘𝑥) / 𝑘⦌𝐵 ∈ ℂ))
175	168, 169, 174	sylc 62	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → ⦋(𝐾‘𝑥) / 𝑘⦌𝐵 ∈ ℂ)
176	156, 175	eqeltrd 2308	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → if(𝑥 ≤ (♯‘𝐴), ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1) ∈ ℂ)
177	104, 160, 162, 176	fvmptd3 5749	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐻‘𝑥) = if(𝑥 ≤ (♯‘𝐴), ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1))
178	4	adantr 276	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝐴 ⊆ (ℤ_≥‘𝑀))
179	178, 48	sstrdi 3240	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝐴 ⊆ ℤ)
180	179, 168	sseldd 3229	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐾‘𝑥) ∈ ℤ)
181	168	iftrued 3616	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1) = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵)
182	181, 175	eqeltrd 2308	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1) ∈ ℂ)
183		nfcv 2375	. . . . . . . 8 ⊢ Ⅎ𝑘(𝐾‘𝑥)
184		nfv 1577	. . . . . . . . 9 ⊢ Ⅎ𝑘(𝐾‘𝑥) ∈ 𝐴
185	184, 170, 98	nfif 3638	. . . . . . . 8 ⊢ Ⅎ𝑘if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1)
186		eleq1 2294	. . . . . . . . 9 ⊢ (𝑘 = (𝐾‘𝑥) → (𝑘 ∈ 𝐴 ↔ (𝐾‘𝑥) ∈ 𝐴))
187	186, 172	ifbieq1d 3632	. . . . . . . 8 ⊢ (𝑘 = (𝐾‘𝑥) → if(𝑘 ∈ 𝐴, 𝐵, 1) = if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1))
188	183, 185, 187, 1	fvmptf 5748	. . . . . . 7 ⊢ (((𝐾‘𝑥) ∈ ℤ ∧ if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1) ∈ ℂ) → (𝐹‘(𝐾‘𝑥)) = if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1))
189	180, 182, 188	syl2anc 411	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐹‘(𝐾‘𝑥)) = if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 1))
190	189, 181	eqtrd 2264	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐹‘(𝐾‘𝑥)) = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵)
191	156, 177, 190	3eqtr4d 2274	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐻‘𝑥) = (𝐹‘(𝐾‘𝑥)))
192	71, 73, 75, 76, 5, 77, 4, 103, 142, 153, 191	seq3coll 11152	. . 3 ⊢ (𝜑 → (seq𝑀( · , 𝐹)‘(𝐾‘𝑁)) = (seq1( · , 𝐻)‘𝑁))
193		prodmodc.3	. . . 4 ⊢ 𝐺 = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑘⦌𝐵, 1))
194	7, 7	jca 306	. . . 4 ⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 𝑁 ∈ ℕ))
195	1, 2, 193, 104, 194, 10, 30	prodmodclem3 12199	. . 3 ⊢ (𝜑 → (seq1( · , 𝐺)‘𝑁) = (seq1( · , 𝐻)‘𝑁))
196	192, 195	eqtr4d 2267	. 2 ⊢ (𝜑 → (seq𝑀( · , 𝐹)‘(𝐾‘𝑁)) = (seq1( · , 𝐺)‘𝑁))
197	69, 196	breqtrd 4119	1 ⊢ (𝜑 → seq𝑀( · , 𝐹) ⇝ (seq1( · , 𝐺)‘𝑁))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 DECID wdc 842 ∧ w3a 1005 = wceq 1398 ∈ wcel 2202 ∀wral 2511 ⦋csb 3128 ∖ cdif 3198 ⊆ wss 3201 ifcif 3607 class class class wbr 4093 ↦ cmpt 4155 ^◡ccnv 4730 ⟶wf 5329 –1-1-onto→wf1o 5332 ‘cfv 5333 Isom wiso 5334 (class class class)co 6028 ℂcc 8073 ℝcr 8074 1c1 8076 · cmul 8080 ℝ^*cxr 8255 < clt 8256 ≤ cle 8257 ℕcn 9185 ℕ₀cn0 9444 ℤcz 9523 ℤ_≥cuz 9799 ...cfz 10288 seqcseq 10755 ♯chash 11083 ⇝ cli 11901

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 619 ax-in2 620 ax-io 717 ax-5 1496 ax-7 1497 ax-gen 1498 ax-ie1 1542 ax-ie2 1543 ax-8 1553 ax-10 1554 ax-11 1555 ax-i12 1556 ax-bndl 1558 ax-4 1559 ax-17 1575 ax-i9 1579 ax-ial 1583 ax-i5r 1584 ax-13 2204 ax-14 2205 ax-ext 2213 ax-coll 4209 ax-sep 4212 ax-nul 4220 ax-pow 4270 ax-pr 4305 ax-un 4536 ax-setind 4641 ax-iinf 4692 ax-cnex 8166 ax-resscn 8167 ax-1cn 8168 ax-1re 8169 ax-icn 8170 ax-addcl 8171 ax-addrcl 8172 ax-mulcl 8173 ax-mulrcl 8174 ax-addcom 8175 ax-mulcom 8176 ax-addass 8177 ax-mulass 8178 ax-distr 8179 ax-i2m1 8180 ax-0lt1 8181 ax-1rid 8182 ax-0id 8183 ax-rnegex 8184 ax-precex 8185 ax-cnre 8186 ax-pre-ltirr 8187 ax-pre-ltwlin 8188 ax-pre-lttrn 8189 ax-pre-apti 8190 ax-pre-ltadd 8191 ax-pre-mulgt0 8192 ax-pre-mulext 8193

This theorem depends on definitions: df-bi 117 df-dc 843 df-3or 1006 df-3an 1007 df-tru 1401 df-fal 1404 df-nf 1510 df-sb 1811 df-eu 2082 df-mo 2083 df-clab 2218 df-cleq 2224 df-clel 2227 df-nfc 2364 df-ne 2404 df-nel 2499 df-ral 2516 df-rex 2517 df-reu 2518 df-rmo 2519 df-rab 2520 df-v 2805 df-sbc 3033 df-csb 3129 df-dif 3203 df-un 3205 df-in 3207 df-ss 3214 df-nul 3497 df-if 3608 df-pw 3658 df-sn 3679 df-pr 3680 df-op 3682 df-uni 3899 df-int 3934 df-iun 3977 df-br 4094 df-opab 4156 df-mpt 4157 df-tr 4193 df-id 4396 df-po 4399 df-iso 4400 df-iord 4469 df-on 4471 df-ilim 4472 df-suc 4474 df-iom 4695 df-xp 4737 df-rel 4738 df-cnv 4739 df-co 4740 df-dm 4741 df-rn 4742 df-res 4743 df-ima 4744 df-iota 5293 df-fun 5335 df-fn 5336 df-f 5337 df-f1 5338 df-fo 5339 df-f1o 5340 df-fv 5341 df-isom 5342 df-riota 5981 df-ov 6031 df-oprab 6032 df-mpo 6033 df-1st 6312 df-2nd 6313 df-recs 6514 df-frec 6600 df-1o 6625 df-er 6745 df-en 6953 df-dom 6954 df-fin 6955 df-pnf 8258 df-mnf 8259 df-xr 8260 df-ltxr 8261 df-le 8262 df-sub 8394 df-neg 8395 df-reap 8797 df-ap 8804 df-div 8895 df-inn 9186 df-2 9244 df-n0 9445 df-z 9524 df-uz 9800 df-rp 9933 df-fz 10289 df-fzo 10423 df-seqfrec 10756 df-exp 10847 df-ihash 11084 df-cj 11465 df-rsqrt 11621 df-abs 11622 df-clim 11902

This theorem is referenced by: prodmodclem2 12201 zproddc 12203

W3C validator