Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-fppr Structured version   Visualization version   GIF version

Definition df-fppr 44850
Description: Define the function that maps a positive integer to the set of Fermat pseudoprimes to the base of this positive integer. Since Fermat pseudoprimes shall be composite (positive) integers, they must be nonprime integers greater than or equal to 4 (we cannot use 𝑥 ∈ ℕ 𝑥 ∉ ℙ because 𝑥 = 1 would fulfil this requirement, but should not be regarded as "composite" integer). (Contributed by AV, 29-May-2023.)
Assertion
Ref Expression
df-fppr FPPr = (𝑛 ∈ ℕ ↦ {𝑥 ∈ (ℤ‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))})
Distinct variable group:   𝑥,𝑛

Detailed syntax breakdown of Definition df-fppr
StepHypRef Expression
1 cfppr 44849 . 2 class FPPr
2 vn . . 3 setvar 𝑛
3 cn 11830 . . 3 class
4 vx . . . . . . 7 setvar 𝑥
54cv 1542 . . . . . 6 class 𝑥
6 cprime 16228 . . . . . 6 class
75, 6wnel 3046 . . . . 5 wff 𝑥 ∉ ℙ
82cv 1542 . . . . . . . 8 class 𝑛
9 c1 10730 . . . . . . . . 9 class 1
10 cmin 11062 . . . . . . . . 9 class
115, 9, 10co 7213 . . . . . . . 8 class (𝑥 − 1)
12 cexp 13635 . . . . . . . 8 class
138, 11, 12co 7213 . . . . . . 7 class (𝑛↑(𝑥 − 1))
1413, 9, 10co 7213 . . . . . 6 class ((𝑛↑(𝑥 − 1)) − 1)
15 cdvds 15815 . . . . . 6 class
165, 14, 15wbr 5053 . . . . 5 wff 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1)
177, 16wa 399 . . . 4 wff (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))
18 c4 11887 . . . . 5 class 4
19 cuz 12438 . . . . 5 class
2018, 19cfv 6380 . . . 4 class (ℤ‘4)
2117, 4, 20crab 3065 . . 3 class {𝑥 ∈ (ℤ‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))}
222, 3, 21cmpt 5135 . 2 class (𝑛 ∈ ℕ ↦ {𝑥 ∈ (ℤ‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))})
231, 22wceq 1543 1 wff FPPr = (𝑛 ∈ ℕ ↦ {𝑥 ∈ (ℤ‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))})
Colors of variables: wff setvar class
This definition is referenced by:  fppr  44851  fpprbasnn  44854
  Copyright terms: Public domain W3C validator