Theorem fmtno 48139

Description: The 𝑁 th Fermat number. (Contributed by AV, 13-Jun-2021.)

Assertion

Ref	Expression
fmtno	⊢ (𝑁 ∈ ℕ0 → (FermatNo‘𝑁) = ((2↑(2↑𝑁)) + 1))

Proof of Theorem fmtno

Dummy variable 𝑛 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-fmtno 48138	. 2 ⊢ FermatNo = (𝑛 ∈ ℕ0 ↦ ((2↑(2↑𝑛)) + 1))
2		oveq2 7405	. . . 4 ⊢ (𝑛 = 𝑁 → (2↑𝑛) = (2↑𝑁))
3	2	oveq2d 7413	. . 3 ⊢ (𝑛 = 𝑁 → (2↑(2↑𝑛)) = (2↑(2↑𝑁)))
4	3	oveq1d 7412	. 2 ⊢ (𝑛 = 𝑁 → ((2↑(2↑𝑛)) + 1) = ((2↑(2↑𝑁)) + 1))
5		id 22	. 2 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℕ0)
6		ovexd 7432	. 2 ⊢ (𝑁 ∈ ℕ0 → ((2↑(2↑𝑁)) + 1) ∈ V)
7	1, 4, 5, 6	fvmptd3 7000	1 ⊢ (𝑁 ∈ ℕ0 → (FermatNo‘𝑁) = ((2↑(2↑𝑁)) + 1))

Syntax hints:   → wi 4   = wceq 1561   ∈ wcel 2143  Vcvv 3455  ‘cfv 6522  (class class class)co 7397  1c1 11075   + caddc 11077  2c2 12273  ℕ₀cn0 12482  ↑cexp 14075  FermatNocfmtno 48137

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5247  ax-nul 5257  ax-pr 5391

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-nf 1805  df-sb 2092  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3078  df-rex 3088  df-rab 3416  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5102  df-opab 5164  df-mpt 5183  df-id 5543  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-iota 6478  df-fun 6524  df-fv 6530  df-ov 7400  df-fmtno 48138

This theorem is referenced by:  fmtnoge3  48140  fmtnom1nn  48142  fmtnoodd  48143  fmtnof1  48145  fmtnorec1  48147  fmtnosqrt  48149  fmtno0  48150  fmtno1  48151  fmtnorec2lem  48152  fmtnorec3  48158  fmtnorec4  48159  fmtno2  48160  fmtno3  48161  fmtno4  48162  fmtnoprmfac1lem  48174  fmtno4prm  48185  2pwp1prmfmtno  48200