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 ⊢ K ∈ ℕ ∧ P = 2 K + 1 ∧ P ∈ ℙ → ∃ n ∈ ℕ 0 P = FermatNo ⁡ n

Proof

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