P. 265 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 26401-26500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dchrzrh1 26401	Value of a Dirichlet character at one. (Contributed by Mario Carneiro, 4-May-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    ⇒   ⊢ (𝜑 → (𝑋‘(𝐿‘1)) = 1)
Theorem	dchrzrhcl 26402	A Dirichlet character takes values in the complex numbers. (Contributed by Mario Carneiro, 12-May-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝑋‘(𝐿‘𝐴)) ∈ ℂ)
Theorem	dchrzrhmul 26403	A Dirichlet character is completely multiplicative. (Contributed by Mario Carneiro, 4-May-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐶 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝑋‘(𝐿‘(𝐴 · 𝐶))) = ((𝑋‘(𝐿‘𝐴)) · (𝑋‘(𝐿‘𝐶))))
Theorem	dchrplusg 26404	Group operation on the group of Dirichlet characters. (Contributed by Mario Carneiro, 18-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ · = (+g‘𝐺)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → · = ( ∘f · ↾ (𝐷 × 𝐷)))
Theorem	dchrmul 26405	Group operation on the group of Dirichlet characters. (Contributed by Mario Carneiro, 18-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ · = (+g‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐷)    ⇒   ⊢ (𝜑 → (𝑋 · 𝑌) = (𝑋 ∘f · 𝑌))
Theorem	dchrmulcl 26406	Closure of the group operation on Dirichlet characters. (Contributed by Mario Carneiro, 18-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ · = (+g‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐷)    ⇒   ⊢ (𝜑 → (𝑋 · 𝑌) ∈ 𝐷)
Theorem	dchrn0 26407	A Dirichlet character is nonzero on the units of ℤ/nℤ. (Contributed by Mario Carneiro, 18-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 𝐵 = (Base‘𝑍)    &   ⊢ 𝑈 = (Unit‘𝑍)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑋‘𝐴) ≠ 0 ↔ 𝐴 ∈ 𝑈))
Theorem	dchr1cl 26408*	Closure of the principal Dirichlet character. (Contributed by Mario Carneiro, 18-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 𝐵 = (Base‘𝑍)    &   ⊢ 𝑈 = (Unit‘𝑍)    &   ⊢ 1 = (𝑘 ∈ 𝐵 ↦ if(𝑘 ∈ 𝑈, 1, 0))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → 1 ∈ 𝐷)
Theorem	dchrmulid2 26409*	Left identity for the principal Dirichlet character. (Contributed by Mario Carneiro, 18-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 𝐵 = (Base‘𝑍)    &   ⊢ 𝑈 = (Unit‘𝑍)    &   ⊢ 1 = (𝑘 ∈ 𝐵 ↦ if(𝑘 ∈ 𝑈, 1, 0))    &   ⊢ · = (+g‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    ⇒   ⊢ (𝜑 → ( 1 · 𝑋) = 𝑋)
Theorem	dchrinvcl 26410*	Closure of the group inverse operation on Dirichlet characters. (Contributed by Mario Carneiro, 19-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 𝐵 = (Base‘𝑍)    &   ⊢ 𝑈 = (Unit‘𝑍)    &   ⊢ 1 = (𝑘 ∈ 𝐵 ↦ if(𝑘 ∈ 𝑈, 1, 0))    &   ⊢ · = (+g‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ 𝐾 = (𝑘 ∈ 𝐵 ↦ if(𝑘 ∈ 𝑈, (1 / (𝑋‘𝑘)), 0))    ⇒   ⊢ (𝜑 → (𝐾 ∈ 𝐷 ∧ (𝐾 · 𝑋) = 1 ))
Theorem	dchrabl 26411	The set of Dirichlet characters is an Abelian group. (Contributed by Mario Carneiro, 19-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    ⇒   ⊢ (𝑁 ∈ ℕ → 𝐺 ∈ Abel)
Theorem	dchrfi 26412	The group of Dirichlet characters is a finite group. (Contributed by Mario Carneiro, 19-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    ⇒   ⊢ (𝑁 ∈ ℕ → 𝐷 ∈ Fin)
Theorem	dchrghm 26413	A Dirichlet character restricted to the unit group of ℤ/nℤ is a group homomorphism into the multiplicative group of nonzero complex numbers. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 𝑈 = (Unit‘𝑍)    &   ⊢ 𝐻 = ((mulGrp‘𝑍) ↾s 𝑈)    &   ⊢ 𝑀 = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    ⇒   ⊢ (𝜑 → (𝑋 ↾ 𝑈) ∈ (𝐻 GrpHom 𝑀))
Theorem	dchr1 26414	Value of the principal Dirichlet character. (Contributed by Mario Carneiro, 28-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 1 = (0g‘𝐺)    &   ⊢ 𝑈 = (Unit‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ( 1 ‘𝐴) = 1)
Theorem	dchreq 26415*	A Dirichlet character is determined by its values on the unit group. (Contributed by Mario Carneiro, 28-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 𝑈 = (Unit‘𝑍)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐷)    ⇒   ⊢ (𝜑 → (𝑋 = 𝑌 ↔ ∀𝑘 ∈ 𝑈 (𝑋‘𝑘) = (𝑌‘𝑘)))
Theorem	dchrresb 26416	A Dirichlet character is determined by its values on the unit group. (Contributed by Mario Carneiro, 28-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 𝑈 = (Unit‘𝑍)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐷)    ⇒   ⊢ (𝜑 → ((𝑋 ↾ 𝑈) = (𝑌 ↾ 𝑈) ↔ 𝑋 = 𝑌))
Theorem	dchrabs 26417	A Dirichlet character takes values on the unit circle. (Contributed by Mario Carneiro, 28-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝑈 = (Unit‘𝑍)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (abs‘(𝑋‘𝐴)) = 1)
Theorem	dchrinv 26418	The inverse of a Dirichlet character is the conjugate (which is also the multiplicative inverse, because the values of 𝑋 are unimodular). (Contributed by Mario Carneiro, 28-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ 𝐼 = (invg‘𝐺)    ⇒   ⊢ (𝜑 → (𝐼‘𝑋) = (∗ ∘ 𝑋))
Theorem	dchrabs2 26419	A Dirichlet character takes values inside the unit circle. (Contributed by Mario Carneiro, 3-May-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐵 = (Base‘𝑍)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (abs‘(𝑋‘𝐴)) ≤ 1)
Theorem	dchr1re 26420	The principal Dirichlet character is a real character. (Contributed by Mario Carneiro, 2-May-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 1 = (0g‘𝐺)    &   ⊢ 𝐵 = (Base‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → 1 :𝐵⟶ℝ)
Theorem	dchrptlem1 26421*	Lemma for dchrpt 26424. (Contributed by Mario Carneiro, 28-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 𝐵 = (Base‘𝑍)    &   ⊢ 1 = (1r‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ≠ 1 )    &   ⊢ 𝑈 = (Unit‘𝑍)    &   ⊢ 𝐻 = ((mulGrp‘𝑍) ↾s 𝑈)    &   ⊢ · = (.g‘𝐻)    &   ⊢ 𝑆 = (𝑘 ∈ dom 𝑊 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑊 ∈ Word 𝑈)    &   ⊢ (𝜑 → 𝐻dom DProd 𝑆)    &   ⊢ (𝜑 → (𝐻 DProd 𝑆) = 𝑈)    &   ⊢ 𝑃 = (𝐻dProj𝑆)    &   ⊢ 𝑂 = (od‘𝐻)    &   ⊢ 𝑇 = (-1↑𝑐(2 / (𝑂‘(𝑊‘𝐼))))    &   ⊢ (𝜑 → 𝐼 ∈ dom 𝑊)    &   ⊢ (𝜑 → ((𝑃‘𝐼)‘𝐴) ≠ 1 )    &   ⊢ 𝑋 = (𝑢 ∈ 𝑈 ↦ (℩ℎ∃𝑚 ∈ ℤ (((𝑃‘𝐼)‘𝑢) = (𝑚 · (𝑊‘𝐼)) ∧ ℎ = (𝑇↑𝑚))))    ⇒   ⊢ (((𝜑 ∧ 𝐶 ∈ 𝑈) ∧ (𝑀 ∈ ℤ ∧ ((𝑃‘𝐼)‘𝐶) = (𝑀 · (𝑊‘𝐼)))) → (𝑋‘𝐶) = (𝑇↑𝑀))
Theorem	dchrptlem2 26422*	Lemma for dchrpt 26424. (Contributed by Mario Carneiro, 28-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 𝐵 = (Base‘𝑍)    &   ⊢ 1 = (1r‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ≠ 1 )    &   ⊢ 𝑈 = (Unit‘𝑍)    &   ⊢ 𝐻 = ((mulGrp‘𝑍) ↾s 𝑈)    &   ⊢ · = (.g‘𝐻)    &   ⊢ 𝑆 = (𝑘 ∈ dom 𝑊 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑊 ∈ Word 𝑈)    &   ⊢ (𝜑 → 𝐻dom DProd 𝑆)    &   ⊢ (𝜑 → (𝐻 DProd 𝑆) = 𝑈)    &   ⊢ 𝑃 = (𝐻dProj𝑆)    &   ⊢ 𝑂 = (od‘𝐻)    &   ⊢ 𝑇 = (-1↑𝑐(2 / (𝑂‘(𝑊‘𝐼))))    &   ⊢ (𝜑 → 𝐼 ∈ dom 𝑊)    &   ⊢ (𝜑 → ((𝑃‘𝐼)‘𝐴) ≠ 1 )    &   ⊢ 𝑋 = (𝑢 ∈ 𝑈 ↦ (℩ℎ∃𝑚 ∈ ℤ (((𝑃‘𝐼)‘𝑢) = (𝑚 · (𝑊‘𝐼)) ∧ ℎ = (𝑇↑𝑚))))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐷 (𝑥‘𝐴) ≠ 1)
Theorem	dchrptlem3 26423*	Lemma for dchrpt 26424. (Contributed by Mario Carneiro, 28-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 𝐵 = (Base‘𝑍)    &   ⊢ 1 = (1r‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ≠ 1 )    &   ⊢ 𝑈 = (Unit‘𝑍)    &   ⊢ 𝐻 = ((mulGrp‘𝑍) ↾s 𝑈)    &   ⊢ · = (.g‘𝐻)    &   ⊢ 𝑆 = (𝑘 ∈ dom 𝑊 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑊‘𝑘))))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑊 ∈ Word 𝑈)    &   ⊢ (𝜑 → 𝐻dom DProd 𝑆)    &   ⊢ (𝜑 → (𝐻 DProd 𝑆) = 𝑈)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐷 (𝑥‘𝐴) ≠ 1)
Theorem	dchrpt 26424*	For any element other than 1, there is a Dirichlet character that is not one at the given element. (Contributed by Mario Carneiro, 28-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 𝐵 = (Base‘𝑍)    &   ⊢ 1 = (1r‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ≠ 1 )    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐷 (𝑥‘𝐴) ≠ 1)
Theorem	dchrsum2 26425*	An orthogonality relation for Dirichlet characters: the sum of all the values of a Dirichlet character 𝑋 is 0 if 𝑋 is non-principal and ϕ(𝑛) otherwise. Part of Theorem 6.5.1 of [Shapiro] p. 230. (Contributed by Mario Carneiro, 28-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 1 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ 𝑈 = (Unit‘𝑍)    ⇒   ⊢ (𝜑 → Σ𝑎 ∈ 𝑈 (𝑋‘𝑎) = if(𝑋 = 1 , (ϕ‘𝑁), 0))
Theorem	dchrsum 26426*	An orthogonality relation for Dirichlet characters: the sum of all the values of a Dirichlet character 𝑋 is 0 if 𝑋 is non-principal and ϕ(𝑛) otherwise. Part of Theorem 6.5.1 of [Shapiro] p. 230. (Contributed by Mario Carneiro, 28-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 1 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ 𝐵 = (Base‘𝑍)    ⇒   ⊢ (𝜑 → Σ𝑎 ∈ 𝐵 (𝑋‘𝑎) = if(𝑋 = 1 , (ϕ‘𝑁), 0))
Theorem	sumdchr2 26427*	Lemma for sumdchr 26429. (Contributed by Mario Carneiro, 28-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 1 = (1r‘𝑍)    &   ⊢ 𝐵 = (Base‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) = if(𝐴 = 1 , (♯‘𝐷), 0))
Theorem	dchrhash 26428	There are exactly ϕ(𝑁) Dirichlet characters modulo 𝑁. Part of Theorem 6.5.1 of [Shapiro] p. 230. (Contributed by Mario Carneiro, 28-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    ⇒   ⊢ (𝑁 ∈ ℕ → (♯‘𝐷) = (ϕ‘𝑁))
Theorem	sumdchr 26429*	An orthogonality relation for Dirichlet characters: the sum of 𝑥(𝐴) for fixed 𝐴 and all 𝑥 is 0 if 𝐴 = 1 and ϕ(𝑛) otherwise. Theorem 6.5.1 of [Shapiro] p. 230. (Contributed by Mario Carneiro, 28-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 1 = (1r‘𝑍)    &   ⊢ 𝐵 = (Base‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → Σ𝑥 ∈ 𝐷 (𝑥‘𝐴) = if(𝐴 = 1 , (ϕ‘𝑁), 0))
Theorem	dchr2sum 26430*	An orthogonality relation for Dirichlet characters: the sum of 𝑋(𝑎) · ∗𝑌(𝑎) over all 𝑎 is nonzero only when 𝑋 = 𝑌. Part of Theorem 6.5.2 of [Shapiro] p. 232. (Contributed by Mario Carneiro, 28-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 𝐵 = (Base‘𝑍)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐷)    ⇒   ⊢ (𝜑 → Σ𝑎 ∈ 𝐵 ((𝑋‘𝑎) · (∗‘(𝑌‘𝑎))) = if(𝑋 = 𝑌, (ϕ‘𝑁), 0))
Theorem	sum2dchr 26431*	An orthogonality relation for Dirichlet characters: the sum of 𝑥(𝐴) for fixed 𝐴 and all 𝑥 is 0 if 𝐴 = 1 and ϕ(𝑛) otherwise. Part of Theorem 6.5.2 of [Shapiro] p. 232. (Contributed by Mario Carneiro, 28-Apr-2016.)
⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐵 = (Base‘𝑍)    &   ⊢ 𝑈 = (Unit‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑈)    ⇒   ⊢ (𝜑 → Σ𝑥 ∈ 𝐷 ((𝑥‘𝐴) · (∗‘(𝑥‘𝐶))) = if(𝐴 = 𝐶, (ϕ‘𝑁), 0))
14.4.7  Bertrand's postulate
Theorem	bcctr 26432	Value of the central binomial coefficient. (Contributed by Mario Carneiro, 13-Mar-2014.)
⊢ (𝑁 ∈ ℕ0 → ((2 · 𝑁)C𝑁) = ((!‘(2 · 𝑁)) / ((!‘𝑁) · (!‘𝑁))))
Theorem	pcbcctr 26433*	Prime count of a central binomial coefficient. (Contributed by Mario Carneiro, 12-Mar-2014.)
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (𝑃 pCnt ((2 · 𝑁)C𝑁)) = Σ𝑘 ∈ (1...(2 · 𝑁))((⌊‘((2 · 𝑁) / (𝑃↑𝑘))) − (2 · (⌊‘(𝑁 / (𝑃↑𝑘))))))
Theorem	bcmono 26434	The binomial coefficient is monotone in its second argument, up to the midway point. (Contributed by Mario Carneiro, 5-Mar-2014.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐵 ∈ (ℤ≥‘𝐴) ∧ 𝐵 ≤ (𝑁 / 2)) → (𝑁C𝐴) ≤ (𝑁C𝐵))
Theorem	bcmax 26435	The binomial coefficient takes its maximum value at the center. (Contributed by Mario Carneiro, 5-Mar-2014.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ) → ((2 · 𝑁)C𝐾) ≤ ((2 · 𝑁)C𝑁))
Theorem	bcp1ctr 26436	Ratio of two central binomial coefficients. (Contributed by Mario Carneiro, 10-Mar-2014.)
⊢ (𝑁 ∈ ℕ0 → ((2 · (𝑁 + 1))C(𝑁 + 1)) = (((2 · 𝑁)C𝑁) · (2 · (((2 · 𝑁) + 1) / (𝑁 + 1)))))
Theorem	bclbnd 26437	A bound on the binomial coefficient. (Contributed by Mario Carneiro, 11-Mar-2014.)
⊢ (𝑁 ∈ (ℤ≥‘4) → ((4↑𝑁) / 𝑁) < ((2 · 𝑁)C𝑁))
Theorem	efexple 26438	Convert a bound on a power to a bound on the exponent. (Contributed by Mario Carneiro, 11-Mar-2014.)
⊢ (((𝐴 ∈ ℝ ∧ 1 < 𝐴) ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+) → ((𝐴↑𝑁) ≤ 𝐵 ↔ 𝑁 ≤ (⌊‘((log‘𝐵) / (log‘𝐴)))))
Theorem	bpos1lem 26439*	Lemma for bpos1 26440. (Contributed by Mario Carneiro, 12-Mar-2014.)
⊢ (∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)) → 𝜑)    &   ⊢ (𝑁 ∈ (ℤ≥‘𝑃) → 𝜑)    &   ⊢ 𝑃 ∈ ℙ    &   ⊢ 𝐴 ∈ ℕ0    &   ⊢ (𝐴 · 2) = 𝐵    &   ⊢ 𝐴 < 𝑃    &   ⊢ (𝑃 < 𝐵 ∨ 𝑃 = 𝐵)    ⇒   ⊢ (𝑁 ∈ (ℤ≥‘𝐴) → 𝜑)
Theorem	bpos1 26440*	Bertrand's postulate, checked numerically for 𝑁 ≤ 64, using the prime sequence 2, 3, 5, 7, 13, 23, 43, 83. (Contributed by Mario Carneiro, 12-Mar-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.) (Proof shortened by AV, 15-Sep-2021.)
⊢ ((𝑁 ∈ ℕ ∧ 𝑁 ≤ ;64) → ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)))
Theorem	bposlem1 26441	An upper bound on the prime powers dividing a central binomial coefficient. (Contributed by Mario Carneiro, 9-Mar-2014.)
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (𝑃↑(𝑃 pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁))
Theorem	bposlem2 26442	There are no odd primes in the range (2𝑁 / 3, 𝑁] dividing the 𝑁-th central binomial coefficient. (Contributed by Mario Carneiro, 12-Mar-2014.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → 2 < 𝑃)    &   ⊢ (𝜑 → ((2 · 𝑁) / 3) < 𝑃)    &   ⊢ (𝜑 → 𝑃 ≤ 𝑁)    ⇒   ⊢ (𝜑 → (𝑃 pCnt ((2 · 𝑁)C𝑁)) = 0)
Theorem	bposlem3 26443*	Lemma for bpos 26450. Since the binomial coefficient does not have any primes in the range (2𝑁 / 3, 𝑁] or (2𝑁, +∞) by bposlem2 26442 and prmfac1 16435, respectively, and it does not have any in the range (𝑁, 2𝑁] by hypothesis, the product of the primes up through 2𝑁 / 3 must be sufficient to compose the whole binomial coefficient. (Contributed by Mario Carneiro, 13-Mar-2014.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘5))    &   ⊢ (𝜑 → ¬ ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)))    &   ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1))    &   ⊢ 𝐾 = (⌊‘((2 · 𝑁) / 3))    ⇒   ⊢ (𝜑 → (seq1( · , 𝐹)‘𝐾) = ((2 · 𝑁)C𝑁))
Theorem	bposlem4 26444*	Lemma for bpos 26450. (Contributed by Mario Carneiro, 13-Mar-2014.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘5))    &   ⊢ (𝜑 → ¬ ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)))    &   ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1))    &   ⊢ 𝐾 = (⌊‘((2 · 𝑁) / 3))    &   ⊢ 𝑀 = (⌊‘(√‘(2 · 𝑁)))    ⇒   ⊢ (𝜑 → 𝑀 ∈ (3...𝐾))
Theorem	bposlem5 26445*	Lemma for bpos 26450. Bound the product of all small primes in the binomial coefficient. (Contributed by Mario Carneiro, 15-Mar-2014.) (Proof shortened by AV, 15-Sep-2021.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘5))    &   ⊢ (𝜑 → ¬ ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)))    &   ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1))    &   ⊢ 𝐾 = (⌊‘((2 · 𝑁) / 3))    &   ⊢ 𝑀 = (⌊‘(√‘(2 · 𝑁)))    ⇒   ⊢ (𝜑 → (seq1( · , 𝐹)‘𝑀) ≤ ((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)))
Theorem	bposlem6 26446*	Lemma for bpos 26450. By using the various bounds at our disposal, arrive at an inequality that is false for 𝑁 large enough. (Contributed by Mario Carneiro, 14-Mar-2014.) (Revised by Wolf Lammen, 12-Sep-2020.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘5))    &   ⊢ (𝜑 → ¬ ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)))    &   ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1))    &   ⊢ 𝐾 = (⌊‘((2 · 𝑁) / 3))    &   ⊢ 𝑀 = (⌊‘(√‘(2 · 𝑁)))    ⇒   ⊢ (𝜑 → ((4↑𝑁) / 𝑁) < (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐(((4 · 𝑁) / 3) − 5))))
Theorem	bposlem7 26447*	Lemma for bpos 26450. The function 𝐹 is decreasing. (Contributed by Mario Carneiro, 13-Mar-2014.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) + ((log‘2) / (√‘(2 · 𝑛)))))    &   ⊢ 𝐺 = (𝑥 ∈ ℝ+ ↦ ((log‘𝑥) / 𝑥))    &   ⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → (e↑2) ≤ 𝐴)    &   ⊢ (𝜑 → (e↑2) ≤ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 < 𝐵 → (𝐹‘𝐵) < (𝐹‘𝐴)))
Theorem	bposlem8 26448	Lemma for bpos 26450. Evaluate 𝐹(64) and show it is less than log2. (Contributed by Mario Carneiro, 14-Mar-2014.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) + ((log‘2) / (√‘(2 · 𝑛)))))    &   ⊢ 𝐺 = (𝑥 ∈ ℝ+ ↦ ((log‘𝑥) / 𝑥))    ⇒   ⊢ ((𝐹‘;64) ∈ ℝ ∧ (𝐹‘;64) < (log‘2))
Theorem	bposlem9 26449*	Lemma for bpos 26450. Derive a contradiction. (Contributed by Mario Carneiro, 14-Mar-2014.) (Proof shortened by AV, 15-Sep-2021.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((((√‘2) · (𝐺‘(√‘𝑛))) + ((9 / 4) · (𝐺‘(𝑛 / 2)))) + ((log‘2) / (√‘(2 · 𝑛)))))    &   ⊢ 𝐺 = (𝑥 ∈ ℝ+ ↦ ((log‘𝑥) / 𝑥))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → ;64 < 𝑁)    &   ⊢ (𝜑 → ¬ ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	bpos 26450*	Bertrand's postulate: there is a prime between 𝑁 and 2𝑁 for every positive integer 𝑁. This proof follows Erdős's method, for the most part, but with some refinements due to Shigenori Tochiori to save us some calculations of large primes. See http://en.wikipedia.org/wiki/Proof_of_Bertrand%27s_postulate for an overview of the proof strategy. This is Metamath 100 proof #98. (Contributed by Mario Carneiro, 14-Mar-2014.)
⊢ (𝑁 ∈ ℕ → ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)))
14.4.8  Quadratic residues and the Legendre symbol If the congruence ((𝑥↑2) mod 𝑝) = (𝑛 mod 𝑝) has a solution we say that 𝑛 is a quadratic residue mod 𝑝. If the congruence has no solution we say that 𝑛 is a quadratic nonresidue mod 𝑝, see definition in [ApostolNT] p. 178. The Legendre symbol (𝑛 /L 𝑝) is defined in a way that its value is 1 if 𝑛 is a quadratic residue mod 𝑝 and -1 if 𝑛 is a quadratic nonresidue mod 𝑝 (and 0 if 𝑝 divides 𝑛), see lgsqr 26508. Originally, the Legendre symbol (𝑁 /L 𝑃) was defined for odd primes 𝑃 only (and arbitrary integers 𝑁) by Adrien-Marie Legendre in 1798, see definition in [ApostolNT] p. 179. It was generalized to be defined for any positive odd integer by Carl Gustav Jacob Jacobi in 1837 (therefore called "Jacobi symbol" since then), see definition in [ApostolNT] p. 188. Finally, it was generalized to be defined for any integer by Leopold Kronecker in 1885 (therefore called "Kronecker symbol" since then). The definition df-lgs 26452 for the "Legendre symbol" /L is actually the definition of the "Kronecker symbol". Since only one definition (and one class symbol) are provided in set.mm, the names "Legendre symbol", "Jacobi symbol" and "Kronecker symbol" are used synonymously for /L, but mostly it is called "Legendre symbol", even if it is used in the context of a "Jacobi symbol" or "Kronecker symbol".
Syntax	clgs 26451	Extend class notation with the Legendre symbol function.
class /L
Definition	df-lgs 26452*	Define the Legendre symbol (actually the Kronecker symbol, which extends the Legendre symbol to all integers, and also the Jacobi symbol, which restricts the Kronecker symbol to positive odd integers). See definition in [ApostolNT] p. 179 resp. definition in [ApostolNT] p. 188. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ /L = (𝑎 ∈ ℤ, 𝑛 ∈ ℤ ↦ if(𝑛 = 0, if((𝑎↑2) = 1, 1, 0), (if((𝑛 < 0 ∧ 𝑎 < 0), -1, 1) · (seq1( · , (𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, (if(𝑚 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑚 − 1) / 2)) + 1) mod 𝑚) − 1))↑(𝑚 pCnt 𝑛)), 1)))‘(abs‘𝑛)))))
Theorem	zabsle1 26453	{-1, 0, 1} is the set of all integers with absolute value at most 1. (Contributed by AV, 13-Jul-2021.)
⊢ (𝑍 ∈ ℤ → (𝑍 ∈ {-1, 0, 1} ↔ (abs‘𝑍) ≤ 1))
Theorem	lgslem1 26454	When 𝑎 is coprime to the prime 𝑝, 𝑎↑((𝑝 − 1) / 2) is equivalent mod 𝑝 to 1 or -1, and so adding 1 makes it equivalent to 0 or 2. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ∈ {0, 2})
Theorem	lgslem2 26455	The set 𝑍 of all integers with absolute value at most 1 contains {-1, 0, 1}. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ 𝑍 = {𝑥 ∈ ℤ ∣ (abs‘𝑥) ≤ 1}    ⇒   ⊢ (-1 ∈ 𝑍 ∧ 0 ∈ 𝑍 ∧ 1 ∈ 𝑍)
Theorem	lgslem3 26456*	The set 𝑍 of all integers with absolute value at most 1 is closed under multiplication. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ 𝑍 = {𝑥 ∈ ℤ ∣ (abs‘𝑥) ≤ 1}    ⇒   ⊢ ((𝐴 ∈ 𝑍 ∧ 𝐵 ∈ 𝑍) → (𝐴 · 𝐵) ∈ 𝑍)
Theorem	lgslem4 26457*	Lemma for lgsfcl2 26460. (Contributed by Mario Carneiro, 4-Feb-2015.) (Proof shortened by AV, 19-Mar-2022.)
⊢ 𝑍 = {𝑥 ∈ ℤ ∣ (abs‘𝑥) ≤ 1}    ⇒   ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) → ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1) ∈ 𝑍)
Theorem	lgsval 26458*	Value of the Legendre symbol at an arbitrary integer. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑁)), 1))    ⇒   ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 /L 𝑁) = if(𝑁 = 0, if((𝐴↑2) = 1, 1, 0), (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , 𝐹)‘(abs‘𝑁)))))
Theorem	lgsfval 26459*	Value of the function 𝐹 which defines the Legendre symbol at the primes. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑁)), 1))    ⇒   ⊢ (𝑀 ∈ ℕ → (𝐹‘𝑀) = if(𝑀 ∈ ℙ, (if(𝑀 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑀 − 1) / 2)) + 1) mod 𝑀) − 1))↑(𝑀 pCnt 𝑁)), 1))
Theorem	lgsfcl2 26460*	The function 𝐹 is closed in integers with absolute value less than 1 (namely {-1, 0, 1}, see zabsle1 26453). (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑁)), 1))    &   ⊢ 𝑍 = {𝑥 ∈ ℤ ∣ (abs‘𝑥) ≤ 1}    ⇒   ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → 𝐹:ℕ⟶𝑍)
Theorem	lgscllem 26461*	The Legendre symbol is an element of 𝑍. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑁)), 1))    &   ⊢ 𝑍 = {𝑥 ∈ ℤ ∣ (abs‘𝑥) ≤ 1}    ⇒   ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 /L 𝑁) ∈ 𝑍)
Theorem	lgsfcl 26462*	Closure of the function 𝐹 which defines the Legendre symbol at the primes. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑁)), 1))    ⇒   ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → 𝐹:ℕ⟶ℤ)
Theorem	lgsfle1 26463*	The function 𝐹 has magnitude less or equal to 1. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑁)), 1))    ⇒   ⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) ∧ 𝑀 ∈ ℕ) → (abs‘(𝐹‘𝑀)) ≤ 1)
Theorem	lgsval2lem 26464*	Lemma for lgsval2 26470. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑁)), 1))    ⇒   ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℙ) → (𝐴 /L 𝑁) = if(𝑁 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑁 − 1) / 2)) + 1) mod 𝑁) − 1)))
Theorem	lgsval4lem 26465*	Lemma for lgsval4 26474. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑁)), 1))    ⇒   ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1)))
Theorem	lgscl2 26466*	The Legendre symbol is an integer with absolute value less than or equal to 1. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ 𝑍 = {𝑥 ∈ ℤ ∣ (abs‘𝑥) ≤ 1}    ⇒   ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 /L 𝑁) ∈ 𝑍)
Theorem	lgs0 26467	The Legendre symbol when the second argument is zero. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ (𝐴 ∈ ℤ → (𝐴 /L 0) = if((𝐴↑2) = 1, 1, 0))
Theorem	lgscl 26468	The Legendre symbol is an integer. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 /L 𝑁) ∈ ℤ)
Theorem	lgsle1 26469	The Legendre symbol has absolute value less than or equal to 1. Together with lgscl 26468 this implies that it takes values in {-1, 0, 1}. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (abs‘(𝐴 /L 𝑁)) ≤ 1)
Theorem	lgsval2 26470	The Legendre symbol at a prime (this is the traditional domain of the Legendre symbol, except for the addition of prime 2). (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ ℙ) → (𝐴 /L 𝑃) = if(𝑃 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1)))
Theorem	lgs2 26471	The Legendre symbol at 2. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ (𝐴 ∈ ℤ → (𝐴 /L 2) = if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)))
Theorem	lgsval3 26472	The Legendre symbol at an odd prime (this is the traditional domain of the Legendre symbol). (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) → (𝐴 /L 𝑃) = ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1))
Theorem	lgsvalmod 26473	The Legendre symbol is equivalent to 𝑎↑((𝑝 − 1) / 2), mod 𝑝. This theorem is also called "Euler's criterion", see theorem 9.2 in [ApostolNT] p. 180, or a representation of Euler's criterion using the Legendre symbol, see also lgsqr 26508. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) → ((𝐴 /L 𝑃) mod 𝑃) = ((𝐴↑((𝑃 − 1) / 2)) mod 𝑃))
Theorem	lgsval4 26474*	Restate lgsval 26458 for nonzero 𝑁, where the function 𝐹 has been abbreviated into a self-referential expression taking the value of /L on the primes as given. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))    ⇒   ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝐴 /L 𝑁) = (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , 𝐹)‘(abs‘𝑁))))
Theorem	lgsfcl3 26475*	Closure of the function 𝐹 which defines the Legendre symbol at the primes. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))    ⇒   ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → 𝐹:ℕ⟶ℤ)
Theorem	lgsval4a 26476*	Same as lgsval4 26474 for positive 𝑁. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑁)), 1))    ⇒   ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐴 /L 𝑁) = (seq1( · , 𝐹)‘𝑁))
Theorem	lgscl1 26477	The value of the Legendre symbol is either -1 or 0 or 1. (Contributed by AV, 13-Jul-2021.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 /L 𝑁) ∈ {-1, 0, 1})
Theorem	lgsneg 26478	The Legendre symbol is either even or odd under negation with respect to the second parameter according to the sign of the first. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝐴 /L -𝑁) = (if(𝐴 < 0, -1, 1) · (𝐴 /L 𝑁)))
Theorem	lgsneg1 26479	The Legendre symbol for nonnegative first parameter is unchanged by negation of the second. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝑁 ∈ ℤ) → (𝐴 /L -𝑁) = (𝐴 /L 𝑁))
Theorem	lgsmod 26480	The Legendre (Jacobi) symbol is preserved under reduction mod 𝑛 when 𝑛 is odd. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁) → ((𝐴 mod 𝑁) /L 𝑁) = (𝐴 /L 𝑁))
Theorem	lgsdilem 26481	Lemma for lgsdi 26491 and lgsdir 26489: the sign part of the Legendre symbol is multiplicative. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → if((𝑁 < 0 ∧ (𝐴 · 𝐵) < 0), -1, 1) = (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · if((𝑁 < 0 ∧ 𝐵 < 0), -1, 1)))
Theorem	lgsdir2lem1 26482	Lemma for lgsdir2 26487. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ (((1 mod 8) = 1 ∧ (-1 mod 8) = 7) ∧ ((3 mod 8) = 3 ∧ (-3 mod 8) = 5))
Theorem	lgsdir2lem2 26483	Lemma for lgsdir2 26487. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ (𝐾 ∈ ℤ ∧ 2 ∥ (𝐾 + 1) ∧ ((𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴) → ((𝐴 mod 8) ∈ (0...𝐾) → (𝐴 mod 8) ∈ 𝑆)))    &   ⊢ 𝑀 = (𝐾 + 1)    &   ⊢ 𝑁 = (𝑀 + 1)    &   ⊢ 𝑁 ∈ 𝑆    ⇒   ⊢ (𝑁 ∈ ℤ ∧ 2 ∥ (𝑁 + 1) ∧ ((𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴) → ((𝐴 mod 8) ∈ (0...𝑁) → (𝐴 mod 8) ∈ 𝑆)))
Theorem	lgsdir2lem3 26484	Lemma for lgsdir2 26487. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ ((𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴) → (𝐴 mod 8) ∈ ({1, 7} ∪ {3, 5}))
Theorem	lgsdir2lem4 26485	Lemma for lgsdir2 26487. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐴 mod 8) ∈ {1, 7}) → (((𝐴 · 𝐵) mod 8) ∈ {1, 7} ↔ (𝐵 mod 8) ∈ {1, 7}))
Theorem	lgsdir2lem5 26486	Lemma for lgsdir2 26487. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ((𝐴 mod 8) ∈ {3, 5} ∧ (𝐵 mod 8) ∈ {3, 5})) → ((𝐴 · 𝐵) mod 8) ∈ {1, 7})
Theorem	lgsdir2 26487	The Legendre symbol is completely multiplicative at 2. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 · 𝐵) /L 2) = ((𝐴 /L 2) · (𝐵 /L 2)))
Theorem	lgsdirprm 26488	The Legendre symbol is completely multiplicative at the primes. See theorem 9.3 in [ApostolNT] p. 180. (Contributed by Mario Carneiro, 4-Feb-2015.) (Proof shortened by AV, 18-Mar-2022.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ((𝐴 · 𝐵) /L 𝑃) = ((𝐴 /L 𝑃) · (𝐵 /L 𝑃)))
Theorem	lgsdir 26489	The Legendre symbol is completely multiplicative in its left argument. Generalization of theorem 9.9(a) in [ApostolNT] p. 188 (which assumes that 𝐴 and 𝐵 are odd positive integers). Together with lgsqr 26508 this implies that the product of two quadratic residues or nonresidues is a residue, and the product of a residue and a nonresidue is a nonresidue. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → ((𝐴 · 𝐵) /L 𝑁) = ((𝐴 /L 𝑁) · (𝐵 /L 𝑁)))
Theorem	lgsdilem2 26490*	Lemma for lgsdi 26491. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ≠ 0)    &   ⊢ (𝜑 → 𝑁 ≠ 0)    &   ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)), 1))    ⇒   ⊢ (𝜑 → (seq1( · , 𝐹)‘(abs‘𝑀)) = (seq1( · , 𝐹)‘(abs‘(𝑀 · 𝑁))))
Theorem	lgsdi 26491	The Legendre symbol is completely multiplicative in its right argument. Generalization of theorem 9.9(b) in [ApostolNT] p. 188 (which assumes that 𝑀 and 𝑁 are odd positive integers). (Contributed by Mario Carneiro, 5-Feb-2015.)
⊢ (((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∧ 𝑁 ≠ 0)) → (𝐴 /L (𝑀 · 𝑁)) = ((𝐴 /L 𝑀) · (𝐴 /L 𝑁)))
Theorem	lgsne0 26492	The Legendre symbol is nonzero (and hence equal to 1 or -1) precisely when the arguments are coprime. (Contributed by Mario Carneiro, 5-Feb-2015.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐴 /L 𝑁) ≠ 0 ↔ (𝐴 gcd 𝑁) = 1))
Theorem	lgsabs1 26493	The Legendre symbol is nonzero (and hence equal to 1 or -1) precisely when the arguments are coprime. (Contributed by Mario Carneiro, 5-Feb-2015.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((abs‘(𝐴 /L 𝑁)) = 1 ↔ (𝐴 gcd 𝑁) = 1))
Theorem	lgssq 26494	The Legendre symbol at a square is equal to 1. Together with lgsmod 26480 this implies that the Legendre symbol takes value 1 at every quadratic residue. (Contributed by Mario Carneiro, 5-Feb-2015.) (Revised by AV, 20-Jul-2021.)
⊢ (((𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ 𝑁 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) → ((𝐴↑2) /L 𝑁) = 1)
Theorem	lgssq2 26495	The Legendre symbol at a square is equal to 1. (Contributed by Mario Carneiro, 5-Feb-2015.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ (𝐴 gcd 𝑁) = 1) → (𝐴 /L (𝑁↑2)) = 1)
Theorem	lgsprme0 26496	The Legendre symbol at any prime (even at 2) is 0 iff the prime does not divide the first argument. See definition in [ApostolNT] p. 179. (Contributed by AV, 20-Jul-2021.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ((𝐴 /L 𝑃) = 0 ↔ (𝐴 mod 𝑃) = 0))
Theorem	1lgs 26497	The Legendre symbol at 1. See example 1 in [ApostolNT] p. 180. (Contributed by Mario Carneiro, 28-Apr-2016.)
⊢ (𝑁 ∈ ℤ → (1 /L 𝑁) = 1)
Theorem	lgs1 26498	The Legendre symbol at 1. See definition in [ApostolNT] p. 188. (Contributed by Mario Carneiro, 28-Apr-2016.)
⊢ (𝐴 ∈ ℤ → (𝐴 /L 1) = 1)
Theorem	lgsmodeq 26499	The Legendre (Jacobi) symbol is preserved under reduction mod 𝑛 when 𝑛 is odd. Theorem 9.9(c) in [ApostolNT] p. 188. (Contributed by AV, 20-Jul-2021.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) → ((𝐴 mod 𝑁) = (𝐵 mod 𝑁) → (𝐴 /L 𝑁) = (𝐵 /L 𝑁)))
Theorem	lgsmulsqcoprm 26500	The Legendre (Jacobi) symbol is preserved under multiplication with a square of an integer coprime to the second argument. Theorem 9.9(d) in [ApostolNT] p. 188. (Contributed by AV, 20-Jul-2021.)
⊢ (((𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1)) → (((𝐴↑2) · 𝐵) /L 𝑁) = (𝐵 /L 𝑁))