FormalConjectures.OEIS.«63880»

/-
Copyright 2026 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
import FormalConjecturesUtil

Conjectures associated with A063880

A063880 lists numbers $n$ such that $\sigma(n) = 2 \cdot \text{usigma}(n)$, where $\sigma(n)$ is the sum of all divisors and $\text{usigma}(n)$ is the sum of unitary divisors.

Equivalently, these are numbers whose unitary and non-unitary divisors have equal sum.

The conjectures state that all members satisfy $n \equiv 108 \pmod{216}$, and that all primitive terms (those whose proper divisors aren't in the sequence) are powerful numbers, with $108$ being the only primitive term.

References:

A063880

namespace OeisA63880open scoped ArithmeticFunction.sigma

The set of unitary divisors of $n$: divisors $d$ such that $\gcd(d, n/d) = 1$.

def unitaryDivisors (n : ℕ) : Finset ℕ :=
  {d ∈ n.divisors | d.Coprime (n / d)}

The sum of unitary divisors of $n$, denoted $\text{usigma}(n)$.

def usigma (n : ℕ) : ℕ :=
  ∑ d ∈ unitaryDivisors n, d

A number $n$ is in the sequence A063880 if $\sigma(n) = 2 \cdot \text{usigma}(n)$.

def A (n : ℕ) : Prop :=
  0 < n ∧ σ 1 n = 2 * usigma n

A term $n$ is primitive if no proper divisor of $n$ is in the sequence.

abbrev IsPrimitiveTerm (n : ℕ) : Prop := {n | A n}.IsPrimitive n

$108$ is in the sequence A063880.

@[category test, AMS 11]
theorem a_108 : A 108 := by⊢ A 108
  refine ⟨by⊢ 0 < 108 norm_numAll goals completed! 🐙, ?_⟩
  decideAll goals completed! 🐙

$540$ is in the sequence A063880.

@[category test, AMS 11]
theorem a_540 : A 540 := by⊢ A 540
  refine ⟨by⊢ 0 < 540 norm_numAll goals completed! 🐙, ?_⟩
  decideAll goals completed! 🐙

$756$ is in the sequence A063880.

@[category test, AMS 11]
theorem a_756 : A 756 := by⊢ A 756
  refine ⟨by⊢ 0 < 756 norm_numAll goals completed! 🐙, ?_⟩
  decideAll goals completed! 🐙

$108$ is a primitive term.


@[category test, AMS 11]
theorem isPrimitiveTerm_108 : IsPrimitiveTerm 108 := by⊢ IsPrimitiveTerm 108
  rw [IsPrimitiveTerm,⊢ {n | A n}.IsPrimitive 108⊢ 108 ∈ {n | A n} ∧ ∀ d ∈ Nat.properDivisors 108, d ∉ {n | A n} Set.isPrimitive_iff⊢ 108 ∈ {n | A n} ∧ ∀ d ∈ Nat.properDivisors 108, d ∉ {n | A n}⊢ 108 ∈ {n | A n} ∧ ∀ d ∈ Nat.properDivisors 108, d ∉ {n | A n}]⊢ 108 ∈ {n | A n} ∧ ∀ d ∈ Nat.properDivisors 108, d ∉ {n | A n}
  refine ⟨a_108, ?_⟩⊢ ∀ d ∈ Nat.properDivisors 108, d ∉ {n | A n}
  intro d hdd:ℕhd:d ∈ Nat.properDivisors 108⊢ d ∉ {n | A n}
  have ⟨hdvd, hlt⟩ := Nat.mem_properDivisors.mp hdd:ℕhd:d ∈ Nat.properDivisors 108hdvd:d ∣ 108hlt:d < 108⊢ d ∉ {n | A n}
  interval_cases d«0»d:ℕhd:0 ∈ Nat.properDivisors 108hdvd:0 ∣ 108hlt:0 < 108⊢ 0 ∉ {n | A n}«1»d:ℕhd:1 ∈ Nat.properDivisors 108hdvd:1 ∣ 108hlt:1 < 108⊢ 1 ∉ {n | A n}«2»d:ℕhd:2 ∈ Nat.properDivisors 108hdvd:2 ∣ 108hlt:2 < 108⊢ 2 ∉ {n | A n}«3»d:ℕhd:3 ∈ Nat.properDivisors 108hdvd:3 ∣ 108hlt:3 < 108⊢ 3 ∉ {n | A n}«4»d:ℕhd:4 ∈ Nat.properDivisors 108hdvd:4 ∣ 108hlt:4 < 108⊢ 4 ∉ {n | A n}«5»d:ℕhd:5 ∈ Nat.properDivisors 108hdvd:5 ∣ 108hlt:5 < 108⊢ 5 ∉ {n | A n}«6»d:ℕhd:6 ∈ Nat.properDivisors 108hdvd:6 ∣ 108hlt:6 < 108⊢ 6 ∉ {n | A n}«7»d:ℕhd:7 ∈ Nat.properDivisors 108hdvd:7 ∣ 108hlt:7 < 108⊢ 7 ∉ {n | A n}«8»d:ℕhd:8 ∈ Nat.properDivisors 108hdvd:8 ∣ 108hlt:8 < 108⊢ 8 ∉ {n | A n}«9»d:ℕhd:9 ∈ Nat.properDivisors 108hdvd:9 ∣ 108hlt:9 < 108⊢ 9 ∉ {n | A n}«10»d:ℕhd:10 ∈ Nat.properDivisors 108hdvd:10 ∣ 108hlt:10 < 108⊢ 10 ∉ {n | A n}«11»d:ℕhd:11 ∈ Nat.properDivisors 108hdvd:11 ∣ 108hlt:11 < 108⊢ 11 ∉ {n | A n}«12»d:ℕhd:12 ∈ Nat.properDivisors 108hdvd:12 ∣ 108hlt:12 < 108⊢ 12 ∉ {n | A n}«13»d:ℕhd:13 ∈ Nat.properDivisors 108hdvd:13 ∣ 108hlt:13 < 108⊢ 13 ∉ {n | A n}«14»d:ℕhd:14 ∈ Nat.properDivisors 108hdvd:14 ∣ 108hlt:14 < 108⊢ 14 ∉ {n | A n}«15»d:ℕhd:15 ∈ Nat.properDivisors 108hdvd:15 ∣ 108hlt:15 < 108⊢ 15 ∉ {n | A n}«16»d:ℕhd:16 ∈ Nat.properDivisors 108hdvd:16 ∣ 108hlt:16 < 108⊢ 16 ∉ {n | A n}«17»d:ℕhd:17 ∈ Nat.properDivisors 108hdvd:17 ∣ 108hlt:17 < 108⊢ 17 ∉ {n | A n}«18»d:ℕhd:18 ∈ Nat.properDivisors 108hdvd:18 ∣ 108hlt:18 < 108⊢ 18 ∉ {n | A n}«19»d:ℕhd:19 ∈ Nat.properDivisors 108hdvd:19 ∣ 108hlt:19 < 108⊢ 19 ∉ {n | A n}«20»d:ℕhd:20 ∈ Nat.properDivisors 108hdvd:20 ∣ 108hlt:20 < 108⊢ 20 ∉ {n | A n}«21»d:ℕhd:21 ∈ Nat.properDivisors 108hdvd:21 ∣ 108hlt:21 < 108⊢ 21 ∉ {n | A n}«22»d:ℕhd:22 ∈ Nat.properDivisors 108hdvd:22 ∣ 108hlt:22 < 108⊢ 22 ∉ {n | A n}«23»d:ℕhd:23 ∈ Nat.properDivisors 108hdvd:23 ∣ 108hlt:23 < 108⊢ 23 ∉ {n | A n}«24»d:ℕhd:24 ∈ Nat.properDivisors 108hdvd:24 ∣ 108hlt:24 < 108⊢ 24 ∉ {n | A n}«25»d:ℕhd:25 ∈ Nat.properDivisors 108hdvd:25 ∣ 108hlt:25 < 108⊢ 25 ∉ {n | A n}«26»d:ℕhd:26 ∈ Nat.properDivisors 108hdvd:26 ∣ 108hlt:26 < 108⊢ 26 ∉ {n | A n}«27»d:ℕhd:27 ∈ Nat.properDivisors 108hdvd:27 ∣ 108hlt:27 < 108⊢ 27 ∉ {n | A n}«28»d:ℕhd:28 ∈ Nat.properDivisors 108hdvd:28 ∣ 108hlt:28 < 108⊢ 28 ∉ {n | A n}«29»d:ℕhd:29 ∈ Nat.properDivisors 108hdvd:29 ∣ 108hlt:29 < 108⊢ 29 ∉ {n | A n}«30»d:ℕhd:30 ∈ Nat.properDivisors 108hdvd:30 ∣ 108hlt:30 < 108⊢ 30 ∉ {n | A n}«31»d:ℕhd:31 ∈ Nat.properDivisors 108hdvd:31 ∣ 108hlt:31 < 108⊢ 31 ∉ {n | A n}«32»d:ℕhd:32 ∈ Nat.properDivisors 108hdvd:32 ∣ 108hlt:32 < 108⊢ 32 ∉ {n | A n}«33»d:ℕhd:33 ∈ Nat.properDivisors 108hdvd:33 ∣ 108hlt:33 < 108⊢ 33 ∉ {n | A n}«34»d:ℕhd:34 ∈ Nat.properDivisors 108hdvd:34 ∣ 108hlt:34 < 108⊢ 34 ∉ {n | A n}«35»d:ℕhd:35 ∈ Nat.properDivisors 108hdvd:35 ∣ 108hlt:35 < 108⊢ 35 ∉ {n | A n}«36»d:ℕhd:36 ∈ Nat.properDivisors 108hdvd:36 ∣ 108hlt:36 < 108⊢ 36 ∉ {n | A n}«37»d:ℕhd:37 ∈ Nat.properDivisors 108hdvd:37 ∣ 108hlt:37 < 108⊢ 37 ∉ {n | A n}«38»d:ℕhd:38 ∈ Nat.properDivisors 108hdvd:38 ∣ 108hlt:38 < 108⊢ 38 ∉ {n | A n}«39»d:ℕhd:39 ∈ Nat.properDivisors 108hdvd:39 ∣ 108hlt:39 < 108⊢ 39 ∉ {n | A n}«40»d:ℕhd:40 ∈ Nat.properDivisors 108hdvd:40 ∣ 108hlt:40 < 108⊢ 40 ∉ {n | A n}«41»d:ℕhd:41 ∈ Nat.properDivisors 108hdvd:41 ∣ 108hlt:41 < 108⊢ 41 ∉ {n | A n}«42»d:ℕhd:42 ∈ Nat.properDivisors 108hdvd:42 ∣ 108hlt:42 < 108⊢ 42 ∉ {n | A n}«43»d:ℕhd:43 ∈ Nat.properDivisors 108hdvd:43 ∣ 108hlt:43 < 108⊢ 43 ∉ {n | A n}«44»d:ℕhd:44 ∈ Nat.properDivisors 108hdvd:44 ∣ 108hlt:44 < 108⊢ 44 ∉ {n | A n}«45»d:ℕhd:45 ∈ Nat.properDivisors 108hdvd:45 ∣ 108hlt:45 < 108⊢ 45 ∉ {n | A n}«46»d:ℕhd:46 ∈ Nat.properDivisors 108hdvd:46 ∣ 108hlt:46 < 108⊢ 46 ∉ {n | A n}«47»d:ℕhd:47 ∈ Nat.properDivisors 108hdvd:47 ∣ 108hlt:47 < 108⊢ 47 ∉ {n | A n}«48»d:ℕhd:48 ∈ Nat.properDivisors 108hdvd:48 ∣ 108hlt:48 < 108⊢ 48 ∉ {n | A n}«49»d:ℕhd:49 ∈ Nat.properDivisors 108hdvd:49 ∣ 108hlt:49 < 108⊢ 49 ∉ {n | A n}«50»d:ℕhd:50 ∈ Nat.properDivisors 108hdvd:50 ∣ 108hlt:50 < 108⊢ 50 ∉ {n | A n}«51»d:ℕhd:51 ∈ Nat.properDivisors 108hdvd:51 ∣ 108hlt:51 < 108⊢ 51 ∉ {n | A n}«52»d:ℕhd:52 ∈ Nat.properDivisors 108hdvd:52 ∣ 108hlt:52 < 108⊢ 52 ∉ {n | A n}«53»d:ℕhd:53 ∈ Nat.properDivisors 108hdvd:53 ∣ 108hlt:53 < 108⊢ 53 ∉ {n | A n}«54»d:ℕhd:54 ∈ Nat.properDivisors 108hdvd:54 ∣ 108hlt:54 < 108⊢ 54 ∉ {n | A n}«55»d:ℕhd:55 ∈ Nat.properDivisors 108hdvd:55 ∣ 108hlt:55 < 108⊢ 55 ∉ {n | A n}«56»d:ℕhd:56 ∈ Nat.properDivisors 108hdvd:56 ∣ 108hlt:56 < 108⊢ 56 ∉ {n | A n}«57»d:ℕhd:57 ∈ Nat.properDivisors 108hdvd:57 ∣ 108hlt:57 < 108⊢ 57 ∉ {n | A n}«58»d:ℕhd:58 ∈ Nat.properDivisors 108hdvd:58 ∣ 108hlt:58 < 108⊢ 58 ∉ {n | A n}«59»d:ℕhd:59 ∈ Nat.properDivisors 108hdvd:59 ∣ 108hlt:59 < 108⊢ 59 ∉ {n | A n}«60»d:ℕhd:60 ∈ Nat.properDivisors 108hdvd:60 ∣ 108hlt:60 < 108⊢ 60 ∉ {n | A n}«61»d:ℕhd:61 ∈ Nat.properDivisors 108hdvd:61 ∣ 108hlt:61 < 108⊢ 61 ∉ {n | A n}«62»d:ℕhd:62 ∈ Nat.properDivisors 108hdvd:62 ∣ 108hlt:62 < 108⊢ 62 ∉ {n | A n}«63»d:ℕhd:63 ∈ Nat.properDivisors 108hdvd:63 ∣ 108hlt:63 < 108⊢ 63 ∉ {n | A n}«64»d:ℕhd:64 ∈ Nat.properDivisors 108hdvd:64 ∣ 108hlt:64 < 108⊢ 64 ∉ {n | A n}«65»d:ℕhd:65 ∈ Nat.properDivisors 108hdvd:65 ∣ 108hlt:65 < 108⊢ 65 ∉ {n | A n}«66»d:ℕhd:66 ∈ Nat.properDivisors 108hdvd:66 ∣ 108hlt:66 < 108⊢ 66 ∉ {n | A n}«67»d:ℕhd:67 ∈ Nat.properDivisors 108hdvd:67 ∣ 108hlt:67 < 108⊢ 67 ∉ {n | A n}«68»d:ℕhd:68 ∈ Nat.properDivisors 108hdvd:68 ∣ 108hlt:68 < 108⊢ 68 ∉ {n | A n}«69»d:ℕhd:69 ∈ Nat.properDivisors 108hdvd:69 ∣ 108hlt:69 < 108⊢ 69 ∉ {n | A n}«70»d:ℕhd:70 ∈ Nat.properDivisors 108hdvd:70 ∣ 108hlt:70 < 108⊢ 70 ∉ {n | A n}«71»d:ℕhd:71 ∈ Nat.properDivisors 108hdvd:71 ∣ 108hlt:71 < 108⊢ 71 ∉ {n | A n}«72»d:ℕhd:72 ∈ Nat.properDivisors 108hdvd:72 ∣ 108hlt:72 < 108⊢ 72 ∉ {n | A n}«73»d:ℕhd:73 ∈ Nat.properDivisors 108hdvd:73 ∣ 108hlt:73 < 108⊢ 73 ∉ {n | A n}«74»d:ℕhd:74 ∈ Nat.properDivisors 108hdvd:74 ∣ 108hlt:74 < 108⊢ 74 ∉ {n | A n}«75»d:ℕhd:75 ∈ Nat.properDivisors 108hdvd:75 ∣ 108hlt:75 < 108⊢ 75 ∉ {n | A n}«76»d:ℕhd:76 ∈ Nat.properDivisors 108hdvd:76 ∣ 108hlt:76 < 108⊢ 76 ∉ {n | A n}«77»d:ℕhd:77 ∈ Nat.properDivisors 108hdvd:77 ∣ 108hlt:77 < 108⊢ 77 ∉ {n | A n}«78»d:ℕhd:78 ∈ Nat.properDivisors 108hdvd:78 ∣ 108hlt:78 < 108⊢ 78 ∉ {n | A n}«79»d:ℕhd:79 ∈ Nat.properDivisors 108hdvd:79 ∣ 108hlt:79 < 108⊢ 79 ∉ {n | A n}«80»d:ℕhd:80 ∈ Nat.properDivisors 108hdvd:80 ∣ 108hlt:80 < 108⊢ 80 ∉ {n | A n}«81»d:ℕhd:81 ∈ Nat.properDivisors 108hdvd:81 ∣ 108hlt:81 < 108⊢ 81 ∉ {n | A n}«82»d:ℕhd:82 ∈ Nat.properDivisors 108hdvd:82 ∣ 108hlt:82 < 108⊢ 82 ∉ {n | A n}«83»d:ℕhd:83 ∈ Nat.properDivisors 108hdvd:83 ∣ 108hlt:83 < 108⊢ 83 ∉ {n | A n}«84»d:ℕhd:84 ∈ Nat.properDivisors 108hdvd:84 ∣ 108hlt:84 < 108⊢ 84 ∉ {n | A n}«85»d:ℕhd:85 ∈ Nat.properDivisors 108hdvd:85 ∣ 108hlt:85 < 108⊢ 85 ∉ {n | A n}«86»d:ℕhd:86 ∈ Nat.properDivisors 108hdvd:86 ∣ 108hlt:86 < 108⊢ 86 ∉ {n | A n}«87»d:ℕhd:87 ∈ Nat.properDivisors 108hdvd:87 ∣ 108hlt:87 < 108⊢ 87 ∉ {n | A n}«88»d:ℕhd:88 ∈ Nat.properDivisors 108hdvd:88 ∣ 108hlt:88 < 108⊢ 88 ∉ {n | A n}«89»d:ℕhd:89 ∈ Nat.properDivisors 108hdvd:89 ∣ 108hlt:89 < 108⊢ 89 ∉ {n | A n}«90»d:ℕhd:90 ∈ Nat.properDivisors 108hdvd:90 ∣ 108hlt:90 < 108⊢ 90 ∉ {n | A n}«91»d:ℕhd:91 ∈ Nat.properDivisors 108hdvd:91 ∣ 108hlt:91 < 108⊢ 91 ∉ {n | A n}«92»d:ℕhd:92 ∈ Nat.properDivisors 108hdvd:92 ∣ 108hlt:92 < 108⊢ 92 ∉ {n | A n}«93»d:ℕhd:93 ∈ Nat.properDivisors 108hdvd:93 ∣ 108hlt:93 < 108⊢ 93 ∉ {n | A n}«94»d:ℕhd:94 ∈ Nat.properDivisors 108hdvd:94 ∣ 108hlt:94 < 108⊢ 94 ∉ {n | A n}«95»d:ℕhd:95 ∈ Nat.properDivisors 108hdvd:95 ∣ 108hlt:95 < 108⊢ 95 ∉ {n | A n}«96»d:ℕhd:96 ∈ Nat.properDivisors 108hdvd:96 ∣ 108hlt:96 < 108⊢ 96 ∉ {n | A n}«97»d:ℕhd:97 ∈ Nat.properDivisors 108hdvd:97 ∣ 108hlt:97 < 108⊢ 97 ∉ {n | A n}«98»d:ℕhd:98 ∈ Nat.properDivisors 108hdvd:98 ∣ 108hlt:98 < 108⊢ 98 ∉ {n | A n}«99»d:ℕhd:99 ∈ Nat.properDivisors 108hdvd:99 ∣ 108hlt:99 < 108⊢ 99 ∉ {n | A n}«100»d:ℕhd:100 ∈ Nat.properDivisors 108hdvd:100 ∣ 108hlt:100 < 108⊢ 100 ∉ {n | A n}«101»d:ℕhd:101 ∈ Nat.properDivisors 108hdvd:101 ∣ 108hlt:101 < 108⊢ 101 ∉ {n | A n}«102»d:ℕhd:102 ∈ Nat.properDivisors 108hdvd:102 ∣ 108hlt:102 < 108⊢ 102 ∉ {n | A n}«103»d:ℕhd:103 ∈ Nat.properDivisors 108hdvd:103 ∣ 108hlt:103 < 108⊢ 103 ∉ {n | A n}«104»d:ℕhd:104 ∈ Nat.properDivisors 108hdvd:104 ∣ 108hlt:104 < 108⊢ 104 ∉ {n | A n}«105»d:ℕhd:105 ∈ Nat.properDivisors 108hdvd:105 ∣ 108hlt:105 < 108⊢ 105 ∉ {n | A n}«106»d:ℕhd:106 ∈ Nat.properDivisors 108hdvd:106 ∣ 108hlt:106 < 108⊢ 106 ∉ {n | A n}«107»d:ℕhd:107 ∈ Nat.properDivisors 108hdvd:107 ∣ 108hlt:107 < 108⊢ 107 ∉ {n | A n} <;>«0»d:ℕhd:0 ∈ Nat.properDivisors 108hdvd:0 ∣ 108hlt:0 < 108⊢ 0 ∉ {n | A n}«1»d:ℕhd:1 ∈ Nat.properDivisors 108hdvd:1 ∣ 108hlt:1 < 108⊢ 1 ∉ {n | A n}«2»d:ℕhd:2 ∈ Nat.properDivisors 108hdvd:2 ∣ 108hlt:2 < 108⊢ 2 ∉ {n | A n}«3»d:ℕhd:3 ∈ Nat.properDivisors 108hdvd:3 ∣ 108hlt:3 < 108⊢ 3 ∉ {n | A n}«4»d:ℕhd:4 ∈ Nat.properDivisors 108hdvd:4 ∣ 108hlt:4 < 108⊢ 4 ∉ {n | A n}«5»d:ℕhd:5 ∈ Nat.properDivisors 108hdvd:5 ∣ 108hlt:5 < 108⊢ 5 ∉ {n | A n}«6»d:ℕhd:6 ∈ Nat.properDivisors 108hdvd:6 ∣ 108hlt:6 < 108⊢ 6 ∉ {n | A n}«7»d:ℕhd:7 ∈ Nat.properDivisors 108hdvd:7 ∣ 108hlt:7 < 108⊢ 7 ∉ {n | A n}«8»d:ℕhd:8 ∈ Nat.properDivisors 108hdvd:8 ∣ 108hlt:8 < 108⊢ 8 ∉ {n | A n}«9»d:ℕhd:9 ∈ Nat.properDivisors 108hdvd:9 ∣ 108hlt:9 < 108⊢ 9 ∉ {n | A n}«10»d:ℕhd:10 ∈ Nat.properDivisors 108hdvd:10 ∣ 108hlt:10 < 108⊢ 10 ∉ {n | A n}«11»d:ℕhd:11 ∈ Nat.properDivisors 108hdvd:11 ∣ 108hlt:11 < 108⊢ 11 ∉ {n | A n}«12»d:ℕhd:12 ∈ Nat.properDivisors 108hdvd:12 ∣ 108hlt:12 < 108⊢ 12 ∉ {n | A n}«13»d:ℕhd:13 ∈ Nat.properDivisors 108hdvd:13 ∣ 108hlt:13 < 108⊢ 13 ∉ {n | A n}«14»d:ℕhd:14 ∈ Nat.properDivisors 108hdvd:14 ∣ 108hlt:14 < 108⊢ 14 ∉ {n | A n}«15»d:ℕhd:15 ∈ Nat.properDivisors 108hdvd:15 ∣ 108hlt:15 < 108⊢ 15 ∉ {n | A n}«16»d:ℕhd:16 ∈ Nat.properDivisors 108hdvd:16 ∣ 108hlt:16 < 108⊢ 16 ∉ {n | A n}«17»d:ℕhd:17 ∈ Nat.properDivisors 108hdvd:17 ∣ 108hlt:17 < 108⊢ 17 ∉ {n | A n}«18»d:ℕhd:18 ∈ Nat.properDivisors 108hdvd:18 ∣ 108hlt:18 < 108⊢ 18 ∉ {n | A n}«19»d:ℕhd:19 ∈ Nat.properDivisors 108hdvd:19 ∣ 108hlt:19 < 108⊢ 19 ∉ {n | A n}«20»d:ℕhd:20 ∈ Nat.properDivisors 108hdvd:20 ∣ 108hlt:20 < 108⊢ 20 ∉ {n | A n}«21»d:ℕhd:21 ∈ Nat.properDivisors 108hdvd:21 ∣ 108hlt:21 < 108⊢ 21 ∉ {n | A n}«22»d:ℕhd:22 ∈ Nat.properDivisors 108hdvd:22 ∣ 108hlt:22 < 108⊢ 22 ∉ {n | A n}«23»d:ℕhd:23 ∈ Nat.properDivisors 108hdvd:23 ∣ 108hlt:23 < 108⊢ 23 ∉ {n | A n}«24»d:ℕhd:24 ∈ Nat.properDivisors 108hdvd:24 ∣ 108hlt:24 < 108⊢ 24 ∉ {n | A n}«25»d:ℕhd:25 ∈ Nat.properDivisors 108hdvd:25 ∣ 108hlt:25 < 108⊢ 25 ∉ {n | A n}«26»d:ℕhd:26 ∈ Nat.properDivisors 108hdvd:26 ∣ 108hlt:26 < 108⊢ 26 ∉ {n | A n}«27»d:ℕhd:27 ∈ Nat.properDivisors 108hdvd:27 ∣ 108hlt:27 < 108⊢ 27 ∉ {n | A n}«28»d:ℕhd:28 ∈ Nat.properDivisors 108hdvd:28 ∣ 108hlt:28 < 108⊢ 28 ∉ {n | A n}«29»d:ℕhd:29 ∈ Nat.properDivisors 108hdvd:29 ∣ 108hlt:29 < 108⊢ 29 ∉ {n | A n}«30»d:ℕhd:30 ∈ Nat.properDivisors 108hdvd:30 ∣ 108hlt:30 < 108⊢ 30 ∉ {n | A n}«31»d:ℕhd:31 ∈ Nat.properDivisors 108hdvd:31 ∣ 108hlt:31 < 108⊢ 31 ∉ {n | A n}«32»d:ℕhd:32 ∈ Nat.properDivisors 108hdvd:32 ∣ 108hlt:32 < 108⊢ 32 ∉ {n | A n}«33»d:ℕhd:33 ∈ Nat.properDivisors 108hdvd:33 ∣ 108hlt:33 < 108⊢ 33 ∉ {n | A n}«34»d:ℕhd:34 ∈ Nat.properDivisors 108hdvd:34 ∣ 108hlt:34 < 108⊢ 34 ∉ {n | A n}«35»d:ℕhd:35 ∈ Nat.properDivisors 108hdvd:35 ∣ 108hlt:35 < 108⊢ 35 ∉ {n | A n}«36»d:ℕhd:36 ∈ Nat.properDivisors 108hdvd:36 ∣ 108hlt:36 < 108⊢ 36 ∉ {n | A n}«37»d:ℕhd:37 ∈ Nat.properDivisors 108hdvd:37 ∣ 108hlt:37 < 108⊢ 37 ∉ {n | A n}«38»d:ℕhd:38 ∈ Nat.properDivisors 108hdvd:38 ∣ 108hlt:38 < 108⊢ 38 ∉ {n | A n}«39»d:ℕhd:39 ∈ Nat.properDivisors 108hdvd:39 ∣ 108hlt:39 < 108⊢ 39 ∉ {n | A n}«40»d:ℕhd:40 ∈ Nat.properDivisors 108hdvd:40 ∣ 108hlt:40 < 108⊢ 40 ∉ {n | A n}«41»d:ℕhd:41 ∈ Nat.properDivisors 108hdvd:41 ∣ 108hlt:41 < 108⊢ 41 ∉ {n | A n}«42»d:ℕhd:42 ∈ Nat.properDivisors 108hdvd:42 ∣ 108hlt:42 < 108⊢ 42 ∉ {n | A n}«43»d:ℕhd:43 ∈ Nat.properDivisors 108hdvd:43 ∣ 108hlt:43 < 108⊢ 43 ∉ {n | A n}«44»d:ℕhd:44 ∈ Nat.properDivisors 108hdvd:44 ∣ 108hlt:44 < 108⊢ 44 ∉ {n | A n}«45»d:ℕhd:45 ∈ Nat.properDivisors 108hdvd:45 ∣ 108hlt:45 < 108⊢ 45 ∉ {n | A n}«46»d:ℕhd:46 ∈ Nat.properDivisors 108hdvd:46 ∣ 108hlt:46 < 108⊢ 46 ∉ {n | A n}«47»d:ℕhd:47 ∈ Nat.properDivisors 108hdvd:47 ∣ 108hlt:47 < 108⊢ 47 ∉ {n | A n}«48»d:ℕhd:48 ∈ Nat.properDivisors 108hdvd:48 ∣ 108hlt:48 < 108⊢ 48 ∉ {n | A n}«49»d:ℕhd:49 ∈ Nat.properDivisors 108hdvd:49 ∣ 108hlt:49 < 108⊢ 49 ∉ {n | A n}«50»d:ℕhd:50 ∈ Nat.properDivisors 108hdvd:50 ∣ 108hlt:50 < 108⊢ 50 ∉ {n | A n}«51»d:ℕhd:51 ∈ Nat.properDivisors 108hdvd:51 ∣ 108hlt:51 < 108⊢ 51 ∉ {n | A n}«52»d:ℕhd:52 ∈ Nat.properDivisors 108hdvd:52 ∣ 108hlt:52 < 108⊢ 52 ∉ {n | A n}«53»d:ℕhd:53 ∈ Nat.properDivisors 108hdvd:53 ∣ 108hlt:53 < 108⊢ 53 ∉ {n | A n}«54»d:ℕhd:54 ∈ Nat.properDivisors 108hdvd:54 ∣ 108hlt:54 < 108⊢ 54 ∉ {n | A n}«55»d:ℕhd:55 ∈ Nat.properDivisors 108hdvd:55 ∣ 108hlt:55 < 108⊢ 55 ∉ {n | A n}«56»d:ℕhd:56 ∈ Nat.properDivisors 108hdvd:56 ∣ 108hlt:56 < 108⊢ 56 ∉ {n | A n}«57»d:ℕhd:57 ∈ Nat.properDivisors 108hdvd:57 ∣ 108hlt:57 < 108⊢ 57 ∉ {n | A n}«58»d:ℕhd:58 ∈ Nat.properDivisors 108hdvd:58 ∣ 108hlt:58 < 108⊢ 58 ∉ {n | A n}«59»d:ℕhd:59 ∈ Nat.properDivisors 108hdvd:59 ∣ 108hlt:59 < 108⊢ 59 ∉ {n | A n}«60»d:ℕhd:60 ∈ Nat.properDivisors 108hdvd:60 ∣ 108hlt:60 < 108⊢ 60 ∉ {n | A n}«61»d:ℕhd:61 ∈ Nat.properDivisors 108hdvd:61 ∣ 108hlt:61 < 108⊢ 61 ∉ {n | A n}«62»d:ℕhd:62 ∈ Nat.properDivisors 108hdvd:62 ∣ 108hlt:62 < 108⊢ 62 ∉ {n | A n}«63»d:ℕhd:63 ∈ Nat.properDivisors 108hdvd:63 ∣ 108hlt:63 < 108⊢ 63 ∉ {n | A n}«64»d:ℕhd:64 ∈ Nat.properDivisors 108hdvd:64 ∣ 108hlt:64 < 108⊢ 64 ∉ {n | A n}«65»d:ℕhd:65 ∈ Nat.properDivisors 108hdvd:65 ∣ 108hlt:65 < 108⊢ 65 ∉ {n | A n}«66»d:ℕhd:66 ∈ Nat.properDivisors 108hdvd:66 ∣ 108hlt:66 < 108⊢ 66 ∉ {n | A n}«67»d:ℕhd:67 ∈ Nat.properDivisors 108hdvd:67 ∣ 108hlt:67 < 108⊢ 67 ∉ {n | A n}«68»d:ℕhd:68 ∈ Nat.properDivisors 108hdvd:68 ∣ 108hlt:68 < 108⊢ 68 ∉ {n | A n}«69»d:ℕhd:69 ∈ Nat.properDivisors 108hdvd:69 ∣ 108hlt:69 < 108⊢ 69 ∉ {n | A n}«70»d:ℕhd:70 ∈ Nat.properDivisors 108hdvd:70 ∣ 108hlt:70 < 108⊢ 70 ∉ {n | A n}«71»d:ℕhd:71 ∈ Nat.properDivisors 108hdvd:71 ∣ 108hlt:71 < 108⊢ 71 ∉ {n | A n}«72»d:ℕhd:72 ∈ Nat.properDivisors 108hdvd:72 ∣ 108hlt:72 < 108⊢ 72 ∉ {n | A n}«73»d:ℕhd:73 ∈ Nat.properDivisors 108hdvd:73 ∣ 108hlt:73 < 108⊢ 73 ∉ {n | A n}«74»d:ℕhd:74 ∈ Nat.properDivisors 108hdvd:74 ∣ 108hlt:74 < 108⊢ 74 ∉ {n | A n}«75»d:ℕhd:75 ∈ Nat.properDivisors 108hdvd:75 ∣ 108hlt:75 < 108⊢ 75 ∉ {n | A n}«76»d:ℕhd:76 ∈ Nat.properDivisors 108hdvd:76 ∣ 108hlt:76 < 108⊢ 76 ∉ {n | A n}«77»d:ℕhd:77 ∈ Nat.properDivisors 108hdvd:77 ∣ 108hlt:77 < 108⊢ 77 ∉ {n | A n}«78»d:ℕhd:78 ∈ Nat.properDivisors 108hdvd:78 ∣ 108hlt:78 < 108⊢ 78 ∉ {n | A n}«79»d:ℕhd:79 ∈ Nat.properDivisors 108hdvd:79 ∣ 108hlt:79 < 108⊢ 79 ∉ {n | A n}«80»d:ℕhd:80 ∈ Nat.properDivisors 108hdvd:80 ∣ 108hlt:80 < 108⊢ 80 ∉ {n | A n}«81»d:ℕhd:81 ∈ Nat.properDivisors 108hdvd:81 ∣ 108hlt:81 < 108⊢ 81 ∉ {n | A n}«82»d:ℕhd:82 ∈ Nat.properDivisors 108hdvd:82 ∣ 108hlt:82 < 108⊢ 82 ∉ {n | A n}«83»d:ℕhd:83 ∈ Nat.properDivisors 108hdvd:83 ∣ 108hlt:83 < 108⊢ 83 ∉ {n | A n}«84»d:ℕhd:84 ∈ Nat.properDivisors 108hdvd:84 ∣ 108hlt:84 < 108⊢ 84 ∉ {n | A n}«85»d:ℕhd:85 ∈ Nat.properDivisors 108hdvd:85 ∣ 108hlt:85 < 108⊢ 85 ∉ {n | A n}«86»d:ℕhd:86 ∈ Nat.properDivisors 108hdvd:86 ∣ 108hlt:86 < 108⊢ 86 ∉ {n | A n}«87»d:ℕhd:87 ∈ Nat.properDivisors 108hdvd:87 ∣ 108hlt:87 < 108⊢ 87 ∉ {n | A n}«88»d:ℕhd:88 ∈ Nat.properDivisors 108hdvd:88 ∣ 108hlt:88 < 108⊢ 88 ∉ {n | A n}«89»d:ℕhd:89 ∈ Nat.properDivisors 108hdvd:89 ∣ 108hlt:89 < 108⊢ 89 ∉ {n | A n}«90»d:ℕhd:90 ∈ Nat.properDivisors 108hdvd:90 ∣ 108hlt:90 < 108⊢ 90 ∉ {n | A n}«91»d:ℕhd:91 ∈ Nat.properDivisors 108hdvd:91 ∣ 108hlt:91 < 108⊢ 91 ∉ {n | A n}«92»d:ℕhd:92 ∈ Nat.properDivisors 108hdvd:92 ∣ 108hlt:92 < 108⊢ 92 ∉ {n | A n}«93»d:ℕhd:93 ∈ Nat.properDivisors 108hdvd:93 ∣ 108hlt:93 < 108⊢ 93 ∉ {n | A n}«94»d:ℕhd:94 ∈ Nat.properDivisors 108hdvd:94 ∣ 108hlt:94 < 108⊢ 94 ∉ {n | A n}«95»d:ℕhd:95 ∈ Nat.properDivisors 108hdvd:95 ∣ 108hlt:95 < 108⊢ 95 ∉ {n | A n}«96»d:ℕhd:96 ∈ Nat.properDivisors 108hdvd:96 ∣ 108hlt:96 < 108⊢ 96 ∉ {n | A n}«97»d:ℕhd:97 ∈ Nat.properDivisors 108hdvd:97 ∣ 108hlt:97 < 108⊢ 97 ∉ {n | A n}«98»d:ℕhd:98 ∈ Nat.properDivisors 108hdvd:98 ∣ 108hlt:98 < 108⊢ 98 ∉ {n | A n}«99»d:ℕhd:99 ∈ Nat.properDivisors 108hdvd:99 ∣ 108hlt:99 < 108⊢ 99 ∉ {n | A n}«100»d:ℕhd:100 ∈ Nat.properDivisors 108hdvd:100 ∣ 108hlt:100 < 108⊢ 100 ∉ {n | A n}«101»d:ℕhd:101 ∈ Nat.properDivisors 108hdvd:101 ∣ 108hlt:101 < 108⊢ 101 ∉ {n | A n}«102»d:ℕhd:102 ∈ Nat.properDivisors 108hdvd:102 ∣ 108hlt:102 < 108⊢ 102 ∉ {n | A n}«103»d:ℕhd:103 ∈ Nat.properDivisors 108hdvd:103 ∣ 108hlt:103 < 108⊢ 103 ∉ {n | A n}«104»d:ℕhd:104 ∈ Nat.properDivisors 108hdvd:104 ∣ 108hlt:104 < 108⊢ 104 ∉ {n | A n}«105»d:ℕhd:105 ∈ Nat.properDivisors 108hdvd:105 ∣ 108hlt:105 < 108⊢ 105 ∉ {n | A n}«106»d:ℕhd:106 ∈ Nat.properDivisors 108hdvd:106 ∣ 108hlt:106 < 108⊢ 106 ∉ {n | A n}«107»d:ℕhd:107 ∈ Nat.properDivisors 108hdvd:107 ∣ 108hlt:107 < 108⊢ 107 ∉ {n | A n} simp_all [A]All goals completed! 🐙 <;>«1»d:ℕ⊢ ¬1 = 2 * usigma 1«2»d:ℕ⊢ ¬(σ 1) 2 = 2 * usigma 2«3»d:ℕ⊢ ¬(σ 1) 3 = 2 * usigma 3«4»d:ℕ⊢ ¬(σ 1) 4 = 2 * usigma 4«6»d:ℕ⊢ ¬(σ 1) 6 = 2 * usigma 6«9»d:ℕ⊢ ¬(σ 1) 9 = 2 * usigma 9«12»d:ℕ⊢ ¬(σ 1) 12 = 2 * usigma 12«18»d:ℕ⊢ ¬(σ 1) 18 = 2 * usigma 18«27»d:ℕ⊢ ¬(σ 1) 27 = 2 * usigma 27«36»d:ℕ⊢ ¬(σ 1) 36 = 2 * usigma 36«54»d:ℕ⊢ ¬(σ 1) 54 = 2 * usigma 54 decideAll goals completed! 🐙

All members of the sequence satisfy $n \equiv 108 \pmod{216}$.

@[category research open, AMS 11]
theorem mod_216_of_a {n : ℕ} (h : A n) : n % 216 = 108 := byn:ℕh:A n⊢ n % 216 = 108
  sorryAll goals completed! 🐙

All primitive terms are powerful numbers.

@[category textbook, AMS 11]
theorem powerful_of_isPrimitiveTerm {n : ℕ} (h : IsPrimitiveTerm n) : n.Powerful := byn:ℕh:IsPrimitiveTerm n⊢ n.Powerful
  sorryAll goals completed! 🐙

$108$ is the only primitive term.

@[category research open, AMS 11]
theorem unique_primitive_108 {n : ℕ} (h : IsPrimitiveTerm n) : n = 108 := byn:ℕh:IsPrimitiveTerm n⊢ n = 108
  sorryAll goals completed! 🐙

If $m$ is a primitive term and $s$ is squarefree with $\gcd(m, s) = 1$, then $m \cdot s$ is in the sequence.

@[category textbook, AMS 11]
theorem a_of_primitive_mul_squarefree (m s : ℕ) (hm : IsPrimitiveTerm m)
    (hs : Squarefree s) (hcoprime : m.Coprime s) : A (m * s) := bym:ℕs:ℕhm:IsPrimitiveTerm mhs:Squarefree shcoprime:m.Coprime s⊢ A (m * s)
  sorryAll goals completed! 🐙

Non-primitive terms have the form $m \cdot s$ where $m$ is primitive and $s$ is squarefree with $\gcd(m, s) = 1$.

@[category research solved, AMS 11]
theorem exists_primitive_of_a {n : ℕ} (h : A n) :
    ∃ m s, IsPrimitiveTerm m ∧ Squarefree s ∧ m.Coprime s ∧ n = m * s := byn:ℕh:A n⊢ ∃ m s, IsPrimitiveTerm m ∧ Squarefree s ∧ m.Coprime s ∧ n = m * s
  sorryAll goals completed! 🐙

end OeisA63880