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 44258
 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 44257 . 2 class FPPr
2 vn . . 3 setvar 𝑛
3 cn 11627 . . 3 class
4 vx . . . . . . 7 setvar 𝑥
54cv 1537 . . . . . 6 class 𝑥
6 cprime 16007 . . . . . 6 class
75, 6wnel 3091 . . . . 5 wff 𝑥 ∉ ℙ
82cv 1537 . . . . . . . 8 class 𝑛
9 c1 10529 . . . . . . . . 9 class 1
10 cmin 10861 . . . . . . . . 9 class
115, 9, 10co 7135 . . . . . . . 8 class (𝑥 − 1)
12 cexp 13427 . . . . . . . 8 class
138, 11, 12co 7135 . . . . . . 7 class (𝑛↑(𝑥 − 1))
1413, 9, 10co 7135 . . . . . 6 class ((𝑛↑(𝑥 − 1)) − 1)
15 cdvds 15601 . . . . . 6 class
165, 14, 15wbr 5030 . . . . 5 wff 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1)
177, 16wa 399 . . . 4 wff (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))
18 c4 11684 . . . . 5 class 4
19 cuz 12233 . . . . 5 class
2018, 19cfv 6324 . . . 4 class (ℤ‘4)
2117, 4, 20crab 3110 . . 3 class {𝑥 ∈ (ℤ‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))}
222, 3, 21cmpt 5110 . 2 class (𝑛 ∈ ℕ ↦ {𝑥 ∈ (ℤ‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))})
231, 22wceq 1538 1 wff FPPr = (𝑛 ∈ ℕ ↦ {𝑥 ∈ (ℤ‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))})
 Colors of variables: wff setvar class This definition is referenced by:  fppr  44259  fpprbasnn  44262
 Copyright terms: Public domain W3C validator