Definition df-eqp

Description: Define an equivalence relation on ZZ -indexed sequences of integers such that two sequences are equivalent iff the difference is equivalent to zero, and a sequence is equivalent to zero iff the sum sum_ k <_ n f ( k ) ( p ^ k ) is a multiple of p ^ ( n + 1 ) for every n . (Contributed by Mario Carneiro, 2-Dec-2014)

	Ref	Expression
Assertion	df-eqp	⊢ ~Qp = ( 𝑝 ∈ ℙ ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ ( ℤ ↑m ℤ ) ∧ ∀ 𝑛 ∈ ℤ Σ 𝑘 ∈ ( ℤ≥ ‘ - 𝑛 ) ( ( ( 𝑓 ‘ - 𝑘 ) − ( 𝑔 ‘ - 𝑘 ) ) / ( 𝑝 ↑ ( 𝑘 + ( 𝑛 + 1 ) ) ) ) ∈ ℤ ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ceqp	⊢ ~Qp
1		vp	⊢ 𝑝
2		cprime	⊢ ℙ
3		vf	⊢ 𝑓
4		vg	⊢ 𝑔
5	3	cv	⊢ 𝑓
6	4	cv	⊢ 𝑔
7	5 6	cpr	⊢ { 𝑓 , 𝑔 }
8		cz	⊢ ℤ
9		cmap	⊢ ↑m
10	8 8 9	co	⊢ ( ℤ ↑m ℤ )
11	7 10	wss	⊢ { 𝑓 , 𝑔 } ⊆ ( ℤ ↑m ℤ )
12		vn	⊢ 𝑛
13		vk	⊢ 𝑘
14		cuz	⊢ ℤ≥
15	12	cv	⊢ 𝑛
16	15	cneg	⊢ - 𝑛
17	16 14	cfv	⊢ ( ℤ≥ ‘ - 𝑛 )
18	13	cv	⊢ 𝑘
19	18	cneg	⊢ - 𝑘
20	19 5	cfv	⊢ ( 𝑓 ‘ - 𝑘 )
21		cmin	⊢ −
22	19 6	cfv	⊢ ( 𝑔 ‘ - 𝑘 )
23	20 22 21	co	⊢ ( ( 𝑓 ‘ - 𝑘 ) − ( 𝑔 ‘ - 𝑘 ) )
24		cdiv	⊢ /
25	1	cv	⊢ 𝑝
26		cexp	⊢ ↑
27		caddc	⊢ +
28		c1	⊢ 1
29	15 28 27	co	⊢ ( 𝑛 + 1 )
30	18 29 27	co	⊢ ( 𝑘 + ( 𝑛 + 1 ) )
31	25 30 26	co	⊢ ( 𝑝 ↑ ( 𝑘 + ( 𝑛 + 1 ) ) )
32	23 31 24	co	⊢ ( ( ( 𝑓 ‘ - 𝑘 ) − ( 𝑔 ‘ - 𝑘 ) ) / ( 𝑝 ↑ ( 𝑘 + ( 𝑛 + 1 ) ) ) )
33	17 32 13	csu	⊢ Σ 𝑘 ∈ ( ℤ≥ ‘ - 𝑛 ) ( ( ( 𝑓 ‘ - 𝑘 ) − ( 𝑔 ‘ - 𝑘 ) ) / ( 𝑝 ↑ ( 𝑘 + ( 𝑛 + 1 ) ) ) )
34	33 8	wcel	⊢ Σ 𝑘 ∈ ( ℤ≥ ‘ - 𝑛 ) ( ( ( 𝑓 ‘ - 𝑘 ) − ( 𝑔 ‘ - 𝑘 ) ) / ( 𝑝 ↑ ( 𝑘 + ( 𝑛 + 1 ) ) ) ) ∈ ℤ
35	34 12 8	wral	⊢ ∀ 𝑛 ∈ ℤ Σ 𝑘 ∈ ( ℤ≥ ‘ - 𝑛 ) ( ( ( 𝑓 ‘ - 𝑘 ) − ( 𝑔 ‘ - 𝑘 ) ) / ( 𝑝 ↑ ( 𝑘 + ( 𝑛 + 1 ) ) ) ) ∈ ℤ
36	11 35	wa	⊢ ( { 𝑓 , 𝑔 } ⊆ ( ℤ ↑m ℤ ) ∧ ∀ 𝑛 ∈ ℤ Σ 𝑘 ∈ ( ℤ≥ ‘ - 𝑛 ) ( ( ( 𝑓 ‘ - 𝑘 ) − ( 𝑔 ‘ - 𝑘 ) ) / ( 𝑝 ↑ ( 𝑘 + ( 𝑛 + 1 ) ) ) ) ∈ ℤ )
37	36 3 4	copab	⊢ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ ( ℤ ↑m ℤ ) ∧ ∀ 𝑛 ∈ ℤ Σ 𝑘 ∈ ( ℤ≥ ‘ - 𝑛 ) ( ( ( 𝑓 ‘ - 𝑘 ) − ( 𝑔 ‘ - 𝑘 ) ) / ( 𝑝 ↑ ( 𝑘 + ( 𝑛 + 1 ) ) ) ) ∈ ℤ ) }
38	1 2 37	cmpt	⊢ ( 𝑝 ∈ ℙ ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ ( ℤ ↑m ℤ ) ∧ ∀ 𝑛 ∈ ℤ Σ 𝑘 ∈ ( ℤ≥ ‘ - 𝑛 ) ( ( ( 𝑓 ‘ - 𝑘 ) − ( 𝑔 ‘ - 𝑘 ) ) / ( 𝑝 ↑ ( 𝑘 + ( 𝑛 + 1 ) ) ) ) ∈ ℤ ) } )
39	0 38	wceq	⊢ ~Qp = ( 𝑝 ∈ ℙ ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ ( ℤ ↑m ℤ ) ∧ ∀ 𝑛 ∈ ℤ Σ 𝑘 ∈ ( ℤ≥ ‘ - 𝑛 ) ( ( ( 𝑓 ‘ - 𝑘 ) − ( 𝑔 ‘ - 𝑘 ) ) / ( 𝑝 ↑ ( 𝑘 + ( 𝑛 + 1 ) ) ) ) ∈ ℤ ) } )