Metamath Proof Explorer


Theorem caushft

Description: A shifted Cauchy sequence is Cauchy. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 5-Jun-2014)

Ref Expression
Hypotheses caures.1 𝑍 = ( ℤ𝑀 )
caures.3 ( 𝜑𝑀 ∈ ℤ )
caures.4 ( 𝜑𝐷 ∈ ( Met ‘ 𝑋 ) )
caushft.4 𝑊 = ( ℤ ‘ ( 𝑀 + 𝑁 ) )
caushft.5 ( 𝜑𝑁 ∈ ℤ )
caushft.7 ( ( 𝜑𝑘𝑍 ) → ( 𝐹𝑘 ) = ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) )
caushft.8 ( 𝜑𝐹 ∈ ( Cau ‘ 𝐷 ) )
caushft.9 ( 𝜑𝐺 : 𝑊𝑋 )
Assertion caushft ( 𝜑𝐺 ∈ ( Cau ‘ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 caures.1 𝑍 = ( ℤ𝑀 )
2 caures.3 ( 𝜑𝑀 ∈ ℤ )
3 caures.4 ( 𝜑𝐷 ∈ ( Met ‘ 𝑋 ) )
4 caushft.4 𝑊 = ( ℤ ‘ ( 𝑀 + 𝑁 ) )
5 caushft.5 ( 𝜑𝑁 ∈ ℤ )
6 caushft.7 ( ( 𝜑𝑘𝑍 ) → ( 𝐹𝑘 ) = ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) )
7 caushft.8 ( 𝜑𝐹 ∈ ( Cau ‘ 𝐷 ) )
8 caushft.9 ( 𝜑𝐺 : 𝑊𝑋 )
9 metxmet ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
10 3 9 syl ( 𝜑𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
11 6 ralrimiva ( 𝜑 → ∀ 𝑘𝑍 ( 𝐹𝑘 ) = ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) )
12 fveq2 ( 𝑘 = 𝑗 → ( 𝐹𝑘 ) = ( 𝐹𝑗 ) )
13 fvoveq1 ( 𝑘 = 𝑗 → ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) = ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) )
14 12 13 eqeq12d ( 𝑘 = 𝑗 → ( ( 𝐹𝑘 ) = ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) ↔ ( 𝐹𝑗 ) = ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ) )
15 14 rspccva ( ( ∀ 𝑘𝑍 ( 𝐹𝑘 ) = ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) ∧ 𝑗𝑍 ) → ( 𝐹𝑗 ) = ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) )
16 11 15 sylan ( ( 𝜑𝑗𝑍 ) → ( 𝐹𝑗 ) = ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) )
17 1 10 2 6 16 iscau4 ( 𝜑 → ( 𝐹 ∈ ( Cau ‘ 𝐷 ) ↔ ( 𝐹 ∈ ( 𝑋pm ℂ ) ∧ ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) ∈ 𝑋 ∧ ( ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ) < 𝑥 ) ) ) )
18 7 17 mpbid ( 𝜑 → ( 𝐹 ∈ ( 𝑋pm ℂ ) ∧ ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) ∈ 𝑋 ∧ ( ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ) < 𝑥 ) ) )
19 18 simprd ( 𝜑 → ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) ∈ 𝑋 ∧ ( ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ) < 𝑥 ) )
20 1 eleq2i ( 𝑗𝑍𝑗 ∈ ( ℤ𝑀 ) )
21 20 biimpi ( 𝑗𝑍𝑗 ∈ ( ℤ𝑀 ) )
22 eluzadd ( ( 𝑗 ∈ ( ℤ𝑀 ) ∧ 𝑁 ∈ ℤ ) → ( 𝑗 + 𝑁 ) ∈ ( ℤ ‘ ( 𝑀 + 𝑁 ) ) )
23 21 5 22 syl2anr ( ( 𝜑𝑗𝑍 ) → ( 𝑗 + 𝑁 ) ∈ ( ℤ ‘ ( 𝑀 + 𝑁 ) ) )
24 23 4 eleqtrrdi ( ( 𝜑𝑗𝑍 ) → ( 𝑗 + 𝑁 ) ∈ 𝑊 )
25 simplr ( ( ( 𝜑𝑗𝑍 ) ∧ 𝑚 ∈ ( ℤ ‘ ( 𝑗 + 𝑁 ) ) ) → 𝑗𝑍 )
26 25 1 eleqtrdi ( ( ( 𝜑𝑗𝑍 ) ∧ 𝑚 ∈ ( ℤ ‘ ( 𝑗 + 𝑁 ) ) ) → 𝑗 ∈ ( ℤ𝑀 ) )
27 eluzelz ( 𝑗 ∈ ( ℤ𝑀 ) → 𝑗 ∈ ℤ )
28 26 27 syl ( ( ( 𝜑𝑗𝑍 ) ∧ 𝑚 ∈ ( ℤ ‘ ( 𝑗 + 𝑁 ) ) ) → 𝑗 ∈ ℤ )
29 5 ad2antrr ( ( ( 𝜑𝑗𝑍 ) ∧ 𝑚 ∈ ( ℤ ‘ ( 𝑗 + 𝑁 ) ) ) → 𝑁 ∈ ℤ )
30 simpr ( ( ( 𝜑𝑗𝑍 ) ∧ 𝑚 ∈ ( ℤ ‘ ( 𝑗 + 𝑁 ) ) ) → 𝑚 ∈ ( ℤ ‘ ( 𝑗 + 𝑁 ) ) )
31 eluzsub ( ( 𝑗 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑚 ∈ ( ℤ ‘ ( 𝑗 + 𝑁 ) ) ) → ( 𝑚𝑁 ) ∈ ( ℤ𝑗 ) )
32 28 29 30 31 syl3anc ( ( ( 𝜑𝑗𝑍 ) ∧ 𝑚 ∈ ( ℤ ‘ ( 𝑗 + 𝑁 ) ) ) → ( 𝑚𝑁 ) ∈ ( ℤ𝑗 ) )
33 simp3 ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) ∈ 𝑋 ∧ ( ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ) < 𝑥 ) → ( ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ) < 𝑥 )
34 33 ralimi ( ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) ∈ 𝑋 ∧ ( ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ) < 𝑥 ) → ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ) < 𝑥 )
35 fvoveq1 ( 𝑘 = ( 𝑚𝑁 ) → ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) = ( 𝐺 ‘ ( ( 𝑚𝑁 ) + 𝑁 ) ) )
36 35 oveq1d ( 𝑘 = ( 𝑚𝑁 ) → ( ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ) = ( ( 𝐺 ‘ ( ( 𝑚𝑁 ) + 𝑁 ) ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ) )
37 36 breq1d ( 𝑘 = ( 𝑚𝑁 ) → ( ( ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ) < 𝑥 ↔ ( ( 𝐺 ‘ ( ( 𝑚𝑁 ) + 𝑁 ) ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ) < 𝑥 ) )
38 37 rspcv ( ( 𝑚𝑁 ) ∈ ( ℤ𝑗 ) → ( ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ) < 𝑥 → ( ( 𝐺 ‘ ( ( 𝑚𝑁 ) + 𝑁 ) ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ) < 𝑥 ) )
39 32 34 38 syl2im ( ( ( 𝜑𝑗𝑍 ) ∧ 𝑚 ∈ ( ℤ ‘ ( 𝑗 + 𝑁 ) ) ) → ( ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) ∈ 𝑋 ∧ ( ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ) < 𝑥 ) → ( ( 𝐺 ‘ ( ( 𝑚𝑁 ) + 𝑁 ) ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ) < 𝑥 ) )
40 eluzelz ( 𝑚 ∈ ( ℤ ‘ ( 𝑗 + 𝑁 ) ) → 𝑚 ∈ ℤ )
41 40 adantl ( ( ( 𝜑𝑗𝑍 ) ∧ 𝑚 ∈ ( ℤ ‘ ( 𝑗 + 𝑁 ) ) ) → 𝑚 ∈ ℤ )
42 41 zcnd ( ( ( 𝜑𝑗𝑍 ) ∧ 𝑚 ∈ ( ℤ ‘ ( 𝑗 + 𝑁 ) ) ) → 𝑚 ∈ ℂ )
43 5 zcnd ( 𝜑𝑁 ∈ ℂ )
44 43 ad2antrr ( ( ( 𝜑𝑗𝑍 ) ∧ 𝑚 ∈ ( ℤ ‘ ( 𝑗 + 𝑁 ) ) ) → 𝑁 ∈ ℂ )
45 42 44 npcand ( ( ( 𝜑𝑗𝑍 ) ∧ 𝑚 ∈ ( ℤ ‘ ( 𝑗 + 𝑁 ) ) ) → ( ( 𝑚𝑁 ) + 𝑁 ) = 𝑚 )
46 45 fveq2d ( ( ( 𝜑𝑗𝑍 ) ∧ 𝑚 ∈ ( ℤ ‘ ( 𝑗 + 𝑁 ) ) ) → ( 𝐺 ‘ ( ( 𝑚𝑁 ) + 𝑁 ) ) = ( 𝐺𝑚 ) )
47 46 oveq1d ( ( ( 𝜑𝑗𝑍 ) ∧ 𝑚 ∈ ( ℤ ‘ ( 𝑗 + 𝑁 ) ) ) → ( ( 𝐺 ‘ ( ( 𝑚𝑁 ) + 𝑁 ) ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ) = ( ( 𝐺𝑚 ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ) )
48 3 ad2antrr ( ( ( 𝜑𝑗𝑍 ) ∧ 𝑚 ∈ ( ℤ ‘ ( 𝑗 + 𝑁 ) ) ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
49 8 ad2antrr ( ( ( 𝜑𝑗𝑍 ) ∧ 𝑚 ∈ ( ℤ ‘ ( 𝑗 + 𝑁 ) ) ) → 𝐺 : 𝑊𝑋 )
50 4 uztrn2 ( ( ( 𝑗 + 𝑁 ) ∈ 𝑊𝑚 ∈ ( ℤ ‘ ( 𝑗 + 𝑁 ) ) ) → 𝑚𝑊 )
51 24 50 sylan ( ( ( 𝜑𝑗𝑍 ) ∧ 𝑚 ∈ ( ℤ ‘ ( 𝑗 + 𝑁 ) ) ) → 𝑚𝑊 )
52 49 51 ffvelrnd ( ( ( 𝜑𝑗𝑍 ) ∧ 𝑚 ∈ ( ℤ ‘ ( 𝑗 + 𝑁 ) ) ) → ( 𝐺𝑚 ) ∈ 𝑋 )
53 8 adantr ( ( 𝜑𝑗𝑍 ) → 𝐺 : 𝑊𝑋 )
54 53 24 ffvelrnd ( ( 𝜑𝑗𝑍 ) → ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ∈ 𝑋 )
55 54 adantr ( ( ( 𝜑𝑗𝑍 ) ∧ 𝑚 ∈ ( ℤ ‘ ( 𝑗 + 𝑁 ) ) ) → ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ∈ 𝑋 )
56 metsym ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐺𝑚 ) ∈ 𝑋 ∧ ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ∈ 𝑋 ) → ( ( 𝐺𝑚 ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ) = ( ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) 𝐷 ( 𝐺𝑚 ) ) )
57 48 52 55 56 syl3anc ( ( ( 𝜑𝑗𝑍 ) ∧ 𝑚 ∈ ( ℤ ‘ ( 𝑗 + 𝑁 ) ) ) → ( ( 𝐺𝑚 ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ) = ( ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) 𝐷 ( 𝐺𝑚 ) ) )
58 47 57 eqtrd ( ( ( 𝜑𝑗𝑍 ) ∧ 𝑚 ∈ ( ℤ ‘ ( 𝑗 + 𝑁 ) ) ) → ( ( 𝐺 ‘ ( ( 𝑚𝑁 ) + 𝑁 ) ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ) = ( ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) 𝐷 ( 𝐺𝑚 ) ) )
59 58 breq1d ( ( ( 𝜑𝑗𝑍 ) ∧ 𝑚 ∈ ( ℤ ‘ ( 𝑗 + 𝑁 ) ) ) → ( ( ( 𝐺 ‘ ( ( 𝑚𝑁 ) + 𝑁 ) ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ) < 𝑥 ↔ ( ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) 𝐷 ( 𝐺𝑚 ) ) < 𝑥 ) )
60 39 59 sylibd ( ( ( 𝜑𝑗𝑍 ) ∧ 𝑚 ∈ ( ℤ ‘ ( 𝑗 + 𝑁 ) ) ) → ( ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) ∈ 𝑋 ∧ ( ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ) < 𝑥 ) → ( ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) 𝐷 ( 𝐺𝑚 ) ) < 𝑥 ) )
61 60 ralrimdva ( ( 𝜑𝑗𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) ∈ 𝑋 ∧ ( ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ) < 𝑥 ) → ∀ 𝑚 ∈ ( ℤ ‘ ( 𝑗 + 𝑁 ) ) ( ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) 𝐷 ( 𝐺𝑚 ) ) < 𝑥 ) )
62 fveq2 ( 𝑛 = ( 𝑗 + 𝑁 ) → ( ℤ𝑛 ) = ( ℤ ‘ ( 𝑗 + 𝑁 ) ) )
63 fveq2 ( 𝑛 = ( 𝑗 + 𝑁 ) → ( 𝐺𝑛 ) = ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) )
64 63 oveq1d ( 𝑛 = ( 𝑗 + 𝑁 ) → ( ( 𝐺𝑛 ) 𝐷 ( 𝐺𝑚 ) ) = ( ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) 𝐷 ( 𝐺𝑚 ) ) )
65 64 breq1d ( 𝑛 = ( 𝑗 + 𝑁 ) → ( ( ( 𝐺𝑛 ) 𝐷 ( 𝐺𝑚 ) ) < 𝑥 ↔ ( ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) 𝐷 ( 𝐺𝑚 ) ) < 𝑥 ) )
66 62 65 raleqbidv ( 𝑛 = ( 𝑗 + 𝑁 ) → ( ∀ 𝑚 ∈ ( ℤ𝑛 ) ( ( 𝐺𝑛 ) 𝐷 ( 𝐺𝑚 ) ) < 𝑥 ↔ ∀ 𝑚 ∈ ( ℤ ‘ ( 𝑗 + 𝑁 ) ) ( ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) 𝐷 ( 𝐺𝑚 ) ) < 𝑥 ) )
67 66 rspcev ( ( ( 𝑗 + 𝑁 ) ∈ 𝑊 ∧ ∀ 𝑚 ∈ ( ℤ ‘ ( 𝑗 + 𝑁 ) ) ( ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) 𝐷 ( 𝐺𝑚 ) ) < 𝑥 ) → ∃ 𝑛𝑊𝑚 ∈ ( ℤ𝑛 ) ( ( 𝐺𝑛 ) 𝐷 ( 𝐺𝑚 ) ) < 𝑥 )
68 24 61 67 syl6an ( ( 𝜑𝑗𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) ∈ 𝑋 ∧ ( ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ) < 𝑥 ) → ∃ 𝑛𝑊𝑚 ∈ ( ℤ𝑛 ) ( ( 𝐺𝑛 ) 𝐷 ( 𝐺𝑚 ) ) < 𝑥 ) )
69 68 rexlimdva ( 𝜑 → ( ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) ∈ 𝑋 ∧ ( ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ) < 𝑥 ) → ∃ 𝑛𝑊𝑚 ∈ ( ℤ𝑛 ) ( ( 𝐺𝑛 ) 𝐷 ( 𝐺𝑚 ) ) < 𝑥 ) )
70 69 ralimdv ( 𝜑 → ( ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) ∈ 𝑋 ∧ ( ( 𝐺 ‘ ( 𝑘 + 𝑁 ) ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 𝑁 ) ) ) < 𝑥 ) → ∀ 𝑥 ∈ ℝ+𝑛𝑊𝑚 ∈ ( ℤ𝑛 ) ( ( 𝐺𝑛 ) 𝐷 ( 𝐺𝑚 ) ) < 𝑥 ) )
71 19 70 mpd ( 𝜑 → ∀ 𝑥 ∈ ℝ+𝑛𝑊𝑚 ∈ ( ℤ𝑛 ) ( ( 𝐺𝑛 ) 𝐷 ( 𝐺𝑚 ) ) < 𝑥 )
72 2 5 zaddcld ( 𝜑 → ( 𝑀 + 𝑁 ) ∈ ℤ )
73 eqidd ( ( 𝜑𝑚𝑊 ) → ( 𝐺𝑚 ) = ( 𝐺𝑚 ) )
74 eqidd ( ( 𝜑𝑛𝑊 ) → ( 𝐺𝑛 ) = ( 𝐺𝑛 ) )
75 4 10 72 73 74 8 iscauf ( 𝜑 → ( 𝐺 ∈ ( Cau ‘ 𝐷 ) ↔ ∀ 𝑥 ∈ ℝ+𝑛𝑊𝑚 ∈ ( ℤ𝑛 ) ( ( 𝐺𝑛 ) 𝐷 ( 𝐺𝑚 ) ) < 𝑥 ) )
76 71 75 mpbird ( 𝜑𝐺 ∈ ( Cau ‘ 𝐷 ) )