Metamath Proof Explorer

Theorem 2pwp1prmfmtno

Description: Every prime number of the form ( ( 2 ^ k ) + 1 ) must be a Fermat number. (Contributed by AV, 7-Aug-2021)

Ref Expression
Assertion 2pwp1prmfmtno ( ( 𝐾 ∈ ℕ ∧ 𝑃 = ( ( 2 ↑ 𝐾 ) + 1 ) ∧ 𝑃 ∈ ℙ ) → ∃ 𝑛 ∈ ℕ0 𝑃 = ( FermatNo ‘ 𝑛 ) )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑃 = ( ( 2 ↑ 𝐾 ) + 1 ) ∧ 𝑃 ∈ ℙ ) → 𝐾 ∈ ℕ )
2 eleq1 ⊢ ( 𝑃 = ( ( 2 ↑ 𝐾 ) + 1 ) → ( 𝑃 ∈ ℙ ↔ ( ( 2 ↑ 𝐾 ) + 1 ) ∈ ℙ ) )
3 2 biimpa ⊢ ( ( 𝑃 = ( ( 2 ↑ 𝐾 ) + 1 ) ∧ 𝑃 ∈ ℙ ) → ( ( 2 ↑ 𝐾 ) + 1 ) ∈ ℙ )
4 3 3adant1 ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑃 = ( ( 2 ↑ 𝐾 ) + 1 ) ∧ 𝑃 ∈ ℙ ) → ( ( 2 ↑ 𝐾 ) + 1 ) ∈ ℙ )
5 2pwp1prm ⊢ ( ( 𝐾 ∈ ℕ ∧ ( ( 2 ↑ 𝐾 ) + 1 ) ∈ ℙ ) → ∃ 𝑛 ∈ ℕ0 𝐾 = ( 2 ↑ 𝑛 ) )
6 1 4 5 syl2anc ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑃 = ( ( 2 ↑ 𝐾 ) + 1 ) ∧ 𝑃 ∈ ℙ ) → ∃ 𝑛 ∈ ℕ0 𝐾 = ( 2 ↑ 𝑛 ) )
7 simpl ⊢ ( ( 𝑃 = ( ( 2 ↑ 𝐾 ) + 1 ) ∧ 𝐾 = ( 2 ↑ 𝑛 ) ) → 𝑃 = ( ( 2 ↑ 𝐾 ) + 1 ) )
8 oveq2 ⊢ ( 𝐾 = ( 2 ↑ 𝑛 ) → ( 2 ↑ 𝐾 ) = ( 2 ↑ ( 2 ↑ 𝑛 ) ) )
9 8 oveq1d ⊢ ( 𝐾 = ( 2 ↑ 𝑛 ) → ( ( 2 ↑ 𝐾 ) + 1 ) = ( ( 2 ↑ ( 2 ↑ 𝑛 ) ) + 1 ) )
10 9 adantl ⊢ ( ( 𝑃 = ( ( 2 ↑ 𝐾 ) + 1 ) ∧ 𝐾 = ( 2 ↑ 𝑛 ) ) → ( ( 2 ↑ 𝐾 ) + 1 ) = ( ( 2 ↑ ( 2 ↑ 𝑛 ) ) + 1 ) )
11 7 10 eqtrd ⊢ ( ( 𝑃 = ( ( 2 ↑ 𝐾 ) + 1 ) ∧ 𝐾 = ( 2 ↑ 𝑛 ) ) → 𝑃 = ( ( 2 ↑ ( 2 ↑ 𝑛 ) ) + 1 ) )
12 fmtno ⊢ ( 𝑛 ∈ ℕ0 → ( FermatNo ‘ 𝑛 ) = ( ( 2 ↑ ( 2 ↑ 𝑛 ) ) + 1 ) )
13 12 eqcomd ⊢ ( 𝑛 ∈ ℕ0 → ( ( 2 ↑ ( 2 ↑ 𝑛 ) ) + 1 ) = ( FermatNo ‘ 𝑛 ) )
14 11 13 sylan9eqr ⊢ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑃 = ( ( 2 ↑ 𝐾 ) + 1 ) ∧ 𝐾 = ( 2 ↑ 𝑛 ) ) ) → 𝑃 = ( FermatNo ‘ 𝑛 ) )
15 14 exp32 ⊢ ( 𝑛 ∈ ℕ0 → ( 𝑃 = ( ( 2 ↑ 𝐾 ) + 1 ) → ( 𝐾 = ( 2 ↑ 𝑛 ) → 𝑃 = ( FermatNo ‘ 𝑛 ) ) ) )
16 15 com12 ⊢ ( 𝑃 = ( ( 2 ↑ 𝐾 ) + 1 ) → ( 𝑛 ∈ ℕ0 → ( 𝐾 = ( 2 ↑ 𝑛 ) → 𝑃 = ( FermatNo ‘ 𝑛 ) ) ) )
17 16 3ad2ant2 ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑃 = ( ( 2 ↑ 𝐾 ) + 1 ) ∧ 𝑃 ∈ ℙ ) → ( 𝑛 ∈ ℕ0 → ( 𝐾 = ( 2 ↑ 𝑛 ) → 𝑃 = ( FermatNo ‘ 𝑛 ) ) ) )
18 17 imp ⊢ ( ( ( 𝐾 ∈ ℕ ∧ 𝑃 = ( ( 2 ↑ 𝐾 ) + 1 ) ∧ 𝑃 ∈ ℙ ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝐾 = ( 2 ↑ 𝑛 ) → 𝑃 = ( FermatNo ‘ 𝑛 ) ) )
19 18 reximdva ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑃 = ( ( 2 ↑ 𝐾 ) + 1 ) ∧ 𝑃 ∈ ℙ ) → ( ∃ 𝑛 ∈ ℕ0 𝐾 = ( 2 ↑ 𝑛 ) → ∃ 𝑛 ∈ ℕ0 𝑃 = ( FermatNo ‘ 𝑛 ) ) )
20 6 19 mpd ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑃 = ( ( 2 ↑ 𝐾 ) + 1 ) ∧ 𝑃 ∈ ℙ ) → ∃ 𝑛 ∈ ℕ0 𝑃 = ( FermatNo ‘ 𝑛 ) )