![]() |
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 43172 | . 2 ⊢ FermatNo = (𝑛 ∈ ℕ0 ↦ ((2↑(2↑𝑛)) + 1)) | |
2 | oveq2 7024 | . . . 4 ⊢ (𝑛 = 𝑁 → (2↑𝑛) = (2↑𝑁)) | |
3 | 2 | oveq2d 7032 | . . 3 ⊢ (𝑛 = 𝑁 → (2↑(2↑𝑛)) = (2↑(2↑𝑁))) |
4 | 3 | oveq1d 7031 | . 2 ⊢ (𝑛 = 𝑁 → ((2↑(2↑𝑛)) + 1) = ((2↑(2↑𝑁)) + 1)) |
5 | id 22 | . 2 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℕ0) | |
6 | ovexd 7050 | . 2 ⊢ (𝑁 ∈ ℕ0 → ((2↑(2↑𝑁)) + 1) ∈ V) | |
7 | 1, 4, 5, 6 | fvmptd3 6657 | 1 ⊢ (𝑁 ∈ ℕ0 → (FermatNo‘𝑁) = ((2↑(2↑𝑁)) + 1)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1522 ∈ wcel 2081 Vcvv 3437 ‘cfv 6225 (class class class)co 7016 1c1 10384 + caddc 10386 2c2 11540 ℕ0cn0 11745 ↑cexp 13279 FermatNocfmtno 43171 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-13 2344 ax-ext 2769 ax-sep 5094 ax-nul 5101 ax-pr 5221 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-mo 2576 df-eu 2612 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ral 3110 df-rex 3111 df-rab 3114 df-v 3439 df-sbc 3707 df-dif 3862 df-un 3864 df-in 3866 df-ss 3874 df-nul 4212 df-if 4382 df-sn 4473 df-pr 4475 df-op 4479 df-uni 4746 df-br 4963 df-opab 5025 df-mpt 5042 df-id 5348 df-xp 5449 df-rel 5450 df-cnv 5451 df-co 5452 df-dm 5453 df-iota 6189 df-fun 6227 df-fv 6233 df-ov 7019 df-fmtno 43172 |
This theorem is referenced by: fmtnoge3 43174 fmtnom1nn 43176 fmtnoodd 43177 fmtnof1 43179 fmtnorec1 43181 fmtnosqrt 43183 fmtno0 43184 fmtno1 43185 fmtnorec2lem 43186 fmtnorec3 43192 fmtnorec4 43193 fmtno2 43194 fmtno3 43195 fmtno4 43196 fmtnoprmfac1lem 43208 fmtno4prm 43219 2pwp1prmfmtno 43234 |
Copyright terms: Public domain | W3C validator |