![]() |
Mathbox for Alexander van der Vekens |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > fmtno | Structured version Visualization version GIF version |
Description: The 𝑁 th Fermat number. (Contributed by AV, 13-Jun-2021.) |
Ref | Expression |
---|---|
fmtno | ⊢ (𝑁 ∈ ℕ0 → (FermatNo‘𝑁) = ((2↑(2↑𝑁)) + 1)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-fmtno 41835 | . . 3 ⊢ FermatNo = (𝑛 ∈ ℕ0 ↦ ((2↑(2↑𝑛)) + 1)) | |
2 | 1 | a1i 11 | . 2 ⊢ (𝑁 ∈ ℕ0 → FermatNo = (𝑛 ∈ ℕ0 ↦ ((2↑(2↑𝑛)) + 1))) |
3 | oveq2 6741 | . . . . 5 ⊢ (𝑛 = 𝑁 → (2↑𝑛) = (2↑𝑁)) | |
4 | 3 | oveq2d 6749 | . . . 4 ⊢ (𝑛 = 𝑁 → (2↑(2↑𝑛)) = (2↑(2↑𝑁))) |
5 | 4 | oveq1d 6748 | . . 3 ⊢ (𝑛 = 𝑁 → ((2↑(2↑𝑛)) + 1) = ((2↑(2↑𝑁)) + 1)) |
6 | 5 | adantl 473 | . 2 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑛 = 𝑁) → ((2↑(2↑𝑛)) + 1) = ((2↑(2↑𝑁)) + 1)) |
7 | id 22 | . 2 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℕ0) | |
8 | ovexd 6763 | . 2 ⊢ (𝑁 ∈ ℕ0 → ((2↑(2↑𝑁)) + 1) ∈ V) | |
9 | 2, 6, 7, 8 | fvmptd 6370 | 1 ⊢ (𝑁 ∈ ℕ0 → (FermatNo‘𝑁) = ((2↑(2↑𝑁)) + 1)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1564 ∈ wcel 2071 Vcvv 3272 ↦ cmpt 4805 ‘cfv 5969 (class class class)co 6733 1c1 10018 + caddc 10020 2c2 11151 ℕ0cn0 11373 ↑cexp 12943 FermatNocfmtno 41834 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1818 ax-5 1920 ax-6 1986 ax-7 2022 ax-9 2080 ax-10 2100 ax-11 2115 ax-12 2128 ax-13 2323 ax-ext 2672 ax-sep 4857 ax-nul 4865 ax-pr 4979 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1074 df-tru 1567 df-ex 1786 df-nf 1791 df-sb 1979 df-eu 2543 df-mo 2544 df-clab 2679 df-cleq 2685 df-clel 2688 df-nfc 2823 df-ral 2987 df-rex 2988 df-rab 2991 df-v 3274 df-sbc 3510 df-csb 3608 df-dif 3651 df-un 3653 df-in 3655 df-ss 3662 df-nul 3992 df-if 4163 df-sn 4254 df-pr 4256 df-op 4260 df-uni 4513 df-br 4729 df-opab 4789 df-mpt 4806 df-id 5096 df-xp 5192 df-rel 5193 df-cnv 5194 df-co 5195 df-dm 5196 df-iota 5932 df-fun 5971 df-fv 5977 df-ov 6736 df-fmtno 41835 |
This theorem is referenced by: fmtnoge3 41837 fmtnom1nn 41839 fmtnoodd 41840 fmtnof1 41842 fmtnorec1 41844 fmtnosqrt 41846 fmtno0 41847 fmtno1 41848 fmtnorec2lem 41849 fmtnorec3 41855 fmtnorec4 41856 fmtno2 41857 fmtno3 41858 fmtno4 41859 fmtnoprmfac1lem 41871 fmtno4prm 41882 2pwp1prmfmtno 41899 |
Copyright terms: Public domain | W3C validator |