Congruence relation $\alpha_{nl}\equiv\alpha_n$ modulo primes above $l$

Throughout, $\zeta = (\zeta_n)$ is a compatible system of roots of unity in $\mathbb C$: for every square-free positive integer $n$, $\zeta_n$ is a primitive $n$-th root of unity, and $\zeta_{mn} = \zeta_m\zeta_n$ whenever $m,n$ are coprime square-free positive integers. Write $\alpha_n = 1-\zeta_n$ and $\mathbb Q(\zeta_n)\subseteq\mathbb C$ for the $n$-th cyclotomic field.

Let $n$ be square-free and let $l$ be a prime with $l\nmid n$. Let $\mathcal O$ be the ring of integers of $\mathbb Q(\zeta_{nl})$. Then for every prime ideal $\mathfrak P\subset\mathcal O$ lying above $l$ (i.e. $l\in\mathfrak P$),

This is the Euler-system congruence relation for cyclotomic units.

Formalization Note "$\mathfrak P$ lies above $l$" is encoded as: $\mathfrak P$ is a prime ideal of $\mathcal O$ containing $l$. Since $\alpha_{nl},\alpha_n$ are complex numbers, the statement takes elements $x,y\in\mathcal O$ whose images in $\mathbb C$ are $\alpha_{nl}$ and $\alpha_n$ respectively, and asserts $x-y\in\mathfrak P$ (such $x,y$ exist, as $\alpha_n,\alpha_{nl}$ are algebraic integers in $\mathbb Q(\zeta_{nl})$). No restriction $n>1$ is needed here.