Metamath Proof Explorer

Theorem vdwnn

Description: Van der Waerden's theorem, infinitary version. For any finite coloring F of the positive integers, there is a color c that contains arbitrarily long arithmetic progressions. (Contributed by Mario Carneiro, 13-Sep-2014)

Ref Expression
Assertion vdwnn ( ( 𝑅 ∈ Fin ∧ 𝐹 : ℕ ⟶ 𝑅 ) → ∃ 𝑐 ∈ 𝑅 ∀ 𝑘 ∈ ℕ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) )

Proof

Step Hyp Ref Expression
1 simpll ⊢ ( ( ( 𝑅 ∈ Fin ∧ 𝐹 : ℕ ⟶ 𝑅 ) ∧ ¬ ∃ 𝑐 ∈ 𝑅 ∀ 𝑘 ∈ ℕ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) → 𝑅 ∈ Fin )
2 simplr ⊢ ( ( ( 𝑅 ∈ Fin ∧ 𝐹 : ℕ ⟶ 𝑅 ) ∧ ¬ ∃ 𝑐 ∈ 𝑅 ∀ 𝑘 ∈ ℕ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) → 𝐹 : ℕ ⟶ 𝑅 )
3 oveq1 ⊢ ( 𝑚 = 𝑤 → ( 𝑚 · 𝑑 ) = ( 𝑤 · 𝑑 ) )
4 3 oveq2d ⊢ ( 𝑚 = 𝑤 → ( 𝑎 + ( 𝑚 · 𝑑 ) ) = ( 𝑎 + ( 𝑤 · 𝑑 ) ) )
5 4 eleq1d ⊢ ( 𝑚 = 𝑤 → ( ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑢 } ) ↔ ( 𝑎 + ( 𝑤 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑢 } ) ) )
6 5 cbvralvw ⊢ ( ∀ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑢 } ) ↔ ∀ 𝑤 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑎 + ( 𝑤 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑢 } ) )
7 oveq1 ⊢ ( 𝑎 = 𝑦 → ( 𝑎 + ( 𝑤 · 𝑑 ) ) = ( 𝑦 + ( 𝑤 · 𝑑 ) ) )
8 7 eleq1d ⊢ ( 𝑎 = 𝑦 → ( ( 𝑎 + ( 𝑤 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑢 } ) ↔ ( 𝑦 + ( 𝑤 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑢 } ) ) )
9 8 ralbidv ⊢ ( 𝑎 = 𝑦 → ( ∀ 𝑤 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑎 + ( 𝑤 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑢 } ) ↔ ∀ 𝑤 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑦 + ( 𝑤 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑢 } ) ) )
10 6 9 syl5bb ⊢ ( 𝑎 = 𝑦 → ( ∀ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑢 } ) ↔ ∀ 𝑤 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑦 + ( 𝑤 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑢 } ) ) )
11 oveq2 ⊢ ( 𝑑 = 𝑧 → ( 𝑤 · 𝑑 ) = ( 𝑤 · 𝑧 ) )
12 11 oveq2d ⊢ ( 𝑑 = 𝑧 → ( 𝑦 + ( 𝑤 · 𝑑 ) ) = ( 𝑦 + ( 𝑤 · 𝑧 ) ) )
13 12 eleq1d ⊢ ( 𝑑 = 𝑧 → ( ( 𝑦 + ( 𝑤 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑢 } ) ↔ ( 𝑦 + ( 𝑤 · 𝑧 ) ) ∈ ( ◡ 𝐹 “ { 𝑢 } ) ) )
14 13 ralbidv ⊢ ( 𝑑 = 𝑧 → ( ∀ 𝑤 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑦 + ( 𝑤 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑢 } ) ↔ ∀ 𝑤 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑦 + ( 𝑤 · 𝑧 ) ) ∈ ( ◡ 𝐹 “ { 𝑢 } ) ) )
15 10 14 cbvrex2vw ⊢ ( ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑢 } ) ↔ ∃ 𝑦 ∈ ℕ ∃ 𝑧 ∈ ℕ ∀ 𝑤 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑦 + ( 𝑤 · 𝑧 ) ) ∈ ( ◡ 𝐹 “ { 𝑢 } ) )
16 oveq1 ⊢ ( 𝑘 = 𝑥 → ( 𝑘 − 1 ) = ( 𝑥 − 1 ) )
17 16 oveq2d ⊢ ( 𝑘 = 𝑥 → ( 0 ... ( 𝑘 − 1 ) ) = ( 0 ... ( 𝑥 − 1 ) ) )
18 17 raleqdv ⊢ ( 𝑘 = 𝑥 → ( ∀ 𝑤 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑦 + ( 𝑤 · 𝑧 ) ) ∈ ( ◡ 𝐹 “ { 𝑢 } ) ↔ ∀ 𝑤 ∈ ( 0 ... ( 𝑥 − 1 ) ) ( 𝑦 + ( 𝑤 · 𝑧 ) ) ∈ ( ◡ 𝐹 “ { 𝑢 } ) ) )
19 18 2rexbidv ⊢ ( 𝑘 = 𝑥 → ( ∃ 𝑦 ∈ ℕ ∃ 𝑧 ∈ ℕ ∀ 𝑤 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑦 + ( 𝑤 · 𝑧 ) ) ∈ ( ◡ 𝐹 “ { 𝑢 } ) ↔ ∃ 𝑦 ∈ ℕ ∃ 𝑧 ∈ ℕ ∀ 𝑤 ∈ ( 0 ... ( 𝑥 − 1 ) ) ( 𝑦 + ( 𝑤 · 𝑧 ) ) ∈ ( ◡ 𝐹 “ { 𝑢 } ) ) )
20 15 19 syl5bb ⊢ ( 𝑘 = 𝑥 → ( ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑢 } ) ↔ ∃ 𝑦 ∈ ℕ ∃ 𝑧 ∈ ℕ ∀ 𝑤 ∈ ( 0 ... ( 𝑥 − 1 ) ) ( 𝑦 + ( 𝑤 · 𝑧 ) ) ∈ ( ◡ 𝐹 “ { 𝑢 } ) ) )
21 20 notbid ⊢ ( 𝑘 = 𝑥 → ( ¬ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑢 } ) ↔ ¬ ∃ 𝑦 ∈ ℕ ∃ 𝑧 ∈ ℕ ∀ 𝑤 ∈ ( 0 ... ( 𝑥 − 1 ) ) ( 𝑦 + ( 𝑤 · 𝑧 ) ) ∈ ( ◡ 𝐹 “ { 𝑢 } ) ) )
22 21 cbvrabv ⊢ { 𝑘 ∈ ℕ ∣ ¬ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑢 } ) } = { 𝑥 ∈ ℕ ∣ ¬ ∃ 𝑦 ∈ ℕ ∃ 𝑧 ∈ ℕ ∀ 𝑤 ∈ ( 0 ... ( 𝑥 − 1 ) ) ( 𝑦 + ( 𝑤 · 𝑧 ) ) ∈ ( ◡ 𝐹 “ { 𝑢 } ) }
23 simpr ⊢ ( ( ( 𝑅 ∈ Fin ∧ 𝐹 : ℕ ⟶ 𝑅 ) ∧ ¬ ∃ 𝑐 ∈ 𝑅 ∀ 𝑘 ∈ ℕ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) → ¬ ∃ 𝑐 ∈ 𝑅 ∀ 𝑘 ∈ ℕ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) )
24 sneq ⊢ ( 𝑐 = 𝑢 → { 𝑐 } = { 𝑢 } )
25 24 imaeq2d ⊢ ( 𝑐 = 𝑢 → ( ◡ 𝐹 “ { 𝑐 } ) = ( ◡ 𝐹 “ { 𝑢 } ) )
26 25 eleq2d ⊢ ( 𝑐 = 𝑢 → ( ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ↔ ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑢 } ) ) )
27 26 ralbidv ⊢ ( 𝑐 = 𝑢 → ( ∀ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ↔ ∀ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑢 } ) ) )
28 27 2rexbidv ⊢ ( 𝑐 = 𝑢 → ( ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ↔ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑢 } ) ) )
29 28 ralbidv ⊢ ( 𝑐 = 𝑢 → ( ∀ 𝑘 ∈ ℕ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ↔ ∀ 𝑘 ∈ ℕ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑢 } ) ) )
30 29 cbvrexvw ⊢ ( ∃ 𝑐 ∈ 𝑅 ∀ 𝑘 ∈ ℕ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ↔ ∃ 𝑢 ∈ 𝑅 ∀ 𝑘 ∈ ℕ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑢 } ) )
31 23 30 sylnib ⊢ ( ( ( 𝑅 ∈ Fin ∧ 𝐹 : ℕ ⟶ 𝑅 ) ∧ ¬ ∃ 𝑐 ∈ 𝑅 ∀ 𝑘 ∈ ℕ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) → ¬ ∃ 𝑢 ∈ 𝑅 ∀ 𝑘 ∈ ℕ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑢 } ) )
32 rabn0 ⊢ ( { 𝑘 ∈ ℕ ∣ ¬ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑢 } ) } ≠ ∅ ↔ ∃ 𝑘 ∈ ℕ ¬ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑢 } ) )
33 rexnal ⊢ ( ∃ 𝑘 ∈ ℕ ¬ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑢 } ) ↔ ¬ ∀ 𝑘 ∈ ℕ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑢 } ) )
34 32 33 bitri ⊢ ( { 𝑘 ∈ ℕ ∣ ¬ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑢 } ) } ≠ ∅ ↔ ¬ ∀ 𝑘 ∈ ℕ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑢 } ) )
35 34 ralbii ⊢ ( ∀ 𝑢 ∈ 𝑅 { 𝑘 ∈ ℕ ∣ ¬ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑢 } ) } ≠ ∅ ↔ ∀ 𝑢 ∈ 𝑅 ¬ ∀ 𝑘 ∈ ℕ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑢 } ) )
36 ralnex ⊢ ( ∀ 𝑢 ∈ 𝑅 ¬ ∀ 𝑘 ∈ ℕ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑢 } ) ↔ ¬ ∃ 𝑢 ∈ 𝑅 ∀ 𝑘 ∈ ℕ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑢 } ) )
37 35 36 bitri ⊢ ( ∀ 𝑢 ∈ 𝑅 { 𝑘 ∈ ℕ ∣ ¬ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑢 } ) } ≠ ∅ ↔ ¬ ∃ 𝑢 ∈ 𝑅 ∀ 𝑘 ∈ ℕ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑢 } ) )
38 31 37 sylibr ⊢ ( ( ( 𝑅 ∈ Fin ∧ 𝐹 : ℕ ⟶ 𝑅 ) ∧ ¬ ∃ 𝑐 ∈ 𝑅 ∀ 𝑘 ∈ ℕ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) → ∀ 𝑢 ∈ 𝑅 { 𝑘 ∈ ℕ ∣ ¬ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑢 } ) } ≠ ∅ )
39 1 2 22 38 vdwnnlem3 ⊢ ¬ ( ( 𝑅 ∈ Fin ∧ 𝐹 : ℕ ⟶ 𝑅 ) ∧ ¬ ∃ 𝑐 ∈ 𝑅 ∀ 𝑘 ∈ ℕ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) )
40 iman ⊢ ( ( ( 𝑅 ∈ Fin ∧ 𝐹 : ℕ ⟶ 𝑅 ) → ∃ 𝑐 ∈ 𝑅 ∀ 𝑘 ∈ ℕ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) ↔ ¬ ( ( 𝑅 ∈ Fin ∧ 𝐹 : ℕ ⟶ 𝑅 ) ∧ ¬ ∃ 𝑐 ∈ 𝑅 ∀ 𝑘 ∈ ℕ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) ) )
41 39 40 mpbir ⊢ ( ( 𝑅 ∈ Fin ∧ 𝐹 : ℕ ⟶ 𝑅 ) → ∃ 𝑐 ∈ 𝑅 ∀ 𝑘 ∈ ℕ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ∀ 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ( 𝑎 + ( 𝑚 · 𝑑 ) ) ∈ ( ◡ 𝐹 “ { 𝑐 } ) )