Description: Divisor of Fermat number (Euler's Result), see ProofWiki "Divisor of Fermat Number/Euler's Result", 24-Jul-2021, https://proofwiki.org/wiki/Divisor_of_Fermat_Number/Euler's_Result ): "Let F_n be a Fermat number. Let m be divisor of F_n. Then m is in the form: k*2^(n+1)+1 where k is a positive integer." Here, however, k must be a nonnegative integer, because k must be 0 to represent 1 (which is a divisor of F_n ).
Historical Note: In 1747, Leonhard Paul Euler proved that a divisor of a Fermat number F_n is always in the form kx2^(n+1)+1. This was later refined to k*2^(n+2)+1 by François Édouard Anatole Lucas, see fmtnofac2 . (Contributed by AV, 30-Jul-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | fmtnofac1 | ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑀 ∥ ( FermatNo ‘ 𝑁 ) ) → ∃ 𝑘 ∈ ℕ0 𝑀 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 1 ) ) ) + 1 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elnn1uz2 | ⊢ ( 𝑁 ∈ ℕ ↔ ( 𝑁 = 1 ∨ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ) | |
| 2 | 5prm | ⊢ 5 ∈ ℙ | |
| 3 | dvdsprime | ⊢ ( ( 5 ∈ ℙ ∧ 𝑀 ∈ ℕ ) → ( 𝑀 ∥ 5 ↔ ( 𝑀 = 5 ∨ 𝑀 = 1 ) ) ) | |
| 4 | 2 3 | mpan | ⊢ ( 𝑀 ∈ ℕ → ( 𝑀 ∥ 5 ↔ ( 𝑀 = 5 ∨ 𝑀 = 1 ) ) ) |
| 5 | 1nn0 | ⊢ 1 ∈ ℕ0 | |
| 6 | 5 | a1i | ⊢ ( 𝑀 = 5 → 1 ∈ ℕ0 ) |
| 7 | simpl | ⊢ ( ( 𝑀 = 5 ∧ 𝑘 = 1 ) → 𝑀 = 5 ) | |
| 8 | oveq1 | ⊢ ( 𝑘 = 1 → ( 𝑘 · 4 ) = ( 1 · 4 ) ) | |
| 9 | 8 | oveq1d | ⊢ ( 𝑘 = 1 → ( ( 𝑘 · 4 ) + 1 ) = ( ( 1 · 4 ) + 1 ) ) |
| 10 | 9 | adantl | ⊢ ( ( 𝑀 = 5 ∧ 𝑘 = 1 ) → ( ( 𝑘 · 4 ) + 1 ) = ( ( 1 · 4 ) + 1 ) ) |
| 11 | 7 10 | eqeq12d | ⊢ ( ( 𝑀 = 5 ∧ 𝑘 = 1 ) → ( 𝑀 = ( ( 𝑘 · 4 ) + 1 ) ↔ 5 = ( ( 1 · 4 ) + 1 ) ) ) |
| 12 | df-5 | ⊢ 5 = ( 4 + 1 ) | |
| 13 | 4cn | ⊢ 4 ∈ ℂ | |
| 14 | 13 | mulid2i | ⊢ ( 1 · 4 ) = 4 |
| 15 | 14 | eqcomi | ⊢ 4 = ( 1 · 4 ) |
| 16 | 15 | oveq1i | ⊢ ( 4 + 1 ) = ( ( 1 · 4 ) + 1 ) |
| 17 | 12 16 | eqtri | ⊢ 5 = ( ( 1 · 4 ) + 1 ) |
| 18 | 17 | a1i | ⊢ ( 𝑀 = 5 → 5 = ( ( 1 · 4 ) + 1 ) ) |
| 19 | 6 11 18 | rspcedvd | ⊢ ( 𝑀 = 5 → ∃ 𝑘 ∈ ℕ0 𝑀 = ( ( 𝑘 · 4 ) + 1 ) ) |
| 20 | 0nn0 | ⊢ 0 ∈ ℕ0 | |
| 21 | 20 | a1i | ⊢ ( 𝑀 = 1 → 0 ∈ ℕ0 ) |
| 22 | simpl | ⊢ ( ( 𝑀 = 1 ∧ 𝑘 = 0 ) → 𝑀 = 1 ) | |
| 23 | oveq1 | ⊢ ( 𝑘 = 0 → ( 𝑘 · 4 ) = ( 0 · 4 ) ) | |
| 24 | 23 | oveq1d | ⊢ ( 𝑘 = 0 → ( ( 𝑘 · 4 ) + 1 ) = ( ( 0 · 4 ) + 1 ) ) |
| 25 | 24 | adantl | ⊢ ( ( 𝑀 = 1 ∧ 𝑘 = 0 ) → ( ( 𝑘 · 4 ) + 1 ) = ( ( 0 · 4 ) + 1 ) ) |
| 26 | 22 25 | eqeq12d | ⊢ ( ( 𝑀 = 1 ∧ 𝑘 = 0 ) → ( 𝑀 = ( ( 𝑘 · 4 ) + 1 ) ↔ 1 = ( ( 0 · 4 ) + 1 ) ) ) |
| 27 | 13 | mul02i | ⊢ ( 0 · 4 ) = 0 |
| 28 | 27 | oveq1i | ⊢ ( ( 0 · 4 ) + 1 ) = ( 0 + 1 ) |
| 29 | 0p1e1 | ⊢ ( 0 + 1 ) = 1 | |
| 30 | 28 29 | eqtri | ⊢ ( ( 0 · 4 ) + 1 ) = 1 |
| 31 | 30 | eqcomi | ⊢ 1 = ( ( 0 · 4 ) + 1 ) |
| 32 | 31 | a1i | ⊢ ( 𝑀 = 1 → 1 = ( ( 0 · 4 ) + 1 ) ) |
| 33 | 21 26 32 | rspcedvd | ⊢ ( 𝑀 = 1 → ∃ 𝑘 ∈ ℕ0 𝑀 = ( ( 𝑘 · 4 ) + 1 ) ) |
| 34 | 19 33 | jaoi | ⊢ ( ( 𝑀 = 5 ∨ 𝑀 = 1 ) → ∃ 𝑘 ∈ ℕ0 𝑀 = ( ( 𝑘 · 4 ) + 1 ) ) |
| 35 | 4 34 | syl6bi | ⊢ ( 𝑀 ∈ ℕ → ( 𝑀 ∥ 5 → ∃ 𝑘 ∈ ℕ0 𝑀 = ( ( 𝑘 · 4 ) + 1 ) ) ) |
| 36 | fveq2 | ⊢ ( 𝑁 = 1 → ( FermatNo ‘ 𝑁 ) = ( FermatNo ‘ 1 ) ) | |
| 37 | fmtno1 | ⊢ ( FermatNo ‘ 1 ) = 5 | |
| 38 | 36 37 | eqtrdi | ⊢ ( 𝑁 = 1 → ( FermatNo ‘ 𝑁 ) = 5 ) |
| 39 | 38 | breq2d | ⊢ ( 𝑁 = 1 → ( 𝑀 ∥ ( FermatNo ‘ 𝑁 ) ↔ 𝑀 ∥ 5 ) ) |
| 40 | oveq1 | ⊢ ( 𝑁 = 1 → ( 𝑁 + 1 ) = ( 1 + 1 ) ) | |
| 41 | 1p1e2 | ⊢ ( 1 + 1 ) = 2 | |
| 42 | 40 41 | eqtrdi | ⊢ ( 𝑁 = 1 → ( 𝑁 + 1 ) = 2 ) |
| 43 | 42 | oveq2d | ⊢ ( 𝑁 = 1 → ( 2 ↑ ( 𝑁 + 1 ) ) = ( 2 ↑ 2 ) ) |
| 44 | sq2 | ⊢ ( 2 ↑ 2 ) = 4 | |
| 45 | 43 44 | eqtrdi | ⊢ ( 𝑁 = 1 → ( 2 ↑ ( 𝑁 + 1 ) ) = 4 ) |
| 46 | 45 | oveq2d | ⊢ ( 𝑁 = 1 → ( 𝑘 · ( 2 ↑ ( 𝑁 + 1 ) ) ) = ( 𝑘 · 4 ) ) |
| 47 | 46 | oveq1d | ⊢ ( 𝑁 = 1 → ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 1 ) ) ) + 1 ) = ( ( 𝑘 · 4 ) + 1 ) ) |
| 48 | 47 | eqeq2d | ⊢ ( 𝑁 = 1 → ( 𝑀 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 1 ) ) ) + 1 ) ↔ 𝑀 = ( ( 𝑘 · 4 ) + 1 ) ) ) |
| 49 | 48 | rexbidv | ⊢ ( 𝑁 = 1 → ( ∃ 𝑘 ∈ ℕ0 𝑀 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 1 ) ) ) + 1 ) ↔ ∃ 𝑘 ∈ ℕ0 𝑀 = ( ( 𝑘 · 4 ) + 1 ) ) ) |
| 50 | 39 49 | imbi12d | ⊢ ( 𝑁 = 1 → ( ( 𝑀 ∥ ( FermatNo ‘ 𝑁 ) → ∃ 𝑘 ∈ ℕ0 𝑀 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 1 ) ) ) + 1 ) ) ↔ ( 𝑀 ∥ 5 → ∃ 𝑘 ∈ ℕ0 𝑀 = ( ( 𝑘 · 4 ) + 1 ) ) ) ) |
| 51 | 35 50 | syl5ibr | ⊢ ( 𝑁 = 1 → ( 𝑀 ∈ ℕ → ( 𝑀 ∥ ( FermatNo ‘ 𝑁 ) → ∃ 𝑘 ∈ ℕ0 𝑀 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 1 ) ) ) + 1 ) ) ) ) |
| 52 | fmtnofac2 | ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑀 ∥ ( FermatNo ‘ 𝑁 ) ) → ∃ 𝑛 ∈ ℕ0 𝑀 = ( ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) | |
| 53 | id | ⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℕ0 ) | |
| 54 | 2nn0 | ⊢ 2 ∈ ℕ0 | |
| 55 | 54 | a1i | ⊢ ( 𝑛 ∈ ℕ0 → 2 ∈ ℕ0 ) |
| 56 | 53 55 | nn0mulcld | ⊢ ( 𝑛 ∈ ℕ0 → ( 𝑛 · 2 ) ∈ ℕ0 ) |
| 57 | 56 | adantl | ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑀 ∥ ( FermatNo ‘ 𝑁 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 · 2 ) ∈ ℕ0 ) |
| 58 | 57 | adantr | ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑀 ∥ ( FermatNo ‘ 𝑁 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑀 = ( ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) → ( 𝑛 · 2 ) ∈ ℕ0 ) |
| 59 | simpr | ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑀 ∥ ( FermatNo ‘ 𝑁 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑀 = ( ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) → 𝑀 = ( ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) | |
| 60 | oveq1 | ⊢ ( 𝑘 = ( 𝑛 · 2 ) → ( 𝑘 · ( 2 ↑ ( 𝑁 + 1 ) ) ) = ( ( 𝑛 · 2 ) · ( 2 ↑ ( 𝑁 + 1 ) ) ) ) | |
| 61 | 60 | oveq1d | ⊢ ( 𝑘 = ( 𝑛 · 2 ) → ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 1 ) ) ) + 1 ) = ( ( ( 𝑛 · 2 ) · ( 2 ↑ ( 𝑁 + 1 ) ) ) + 1 ) ) |
| 62 | 59 61 | eqeqan12d | ⊢ ( ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑀 ∥ ( FermatNo ‘ 𝑁 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑀 = ( ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) ∧ 𝑘 = ( 𝑛 · 2 ) ) → ( 𝑀 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 1 ) ) ) + 1 ) ↔ ( ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) = ( ( ( 𝑛 · 2 ) · ( 2 ↑ ( 𝑁 + 1 ) ) ) + 1 ) ) ) |
| 63 | eluzge2nn0 | ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℕ0 ) | |
| 64 | 63 | nn0cnd | ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℂ ) |
| 65 | add1p1 | ⊢ ( 𝑁 ∈ ℂ → ( ( 𝑁 + 1 ) + 1 ) = ( 𝑁 + 2 ) ) | |
| 66 | 64 65 | syl | ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝑁 + 1 ) + 1 ) = ( 𝑁 + 2 ) ) |
| 67 | 66 | eqcomd | ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 + 2 ) = ( ( 𝑁 + 1 ) + 1 ) ) |
| 68 | 67 | oveq2d | ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 ↑ ( 𝑁 + 2 ) ) = ( 2 ↑ ( ( 𝑁 + 1 ) + 1 ) ) ) |
| 69 | 2cnd | ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 2 ∈ ℂ ) | |
| 70 | peano2nn0 | ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 ) | |
| 71 | 63 70 | syl | ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 + 1 ) ∈ ℕ0 ) |
| 72 | 69 71 | expp1d | ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 ↑ ( ( 𝑁 + 1 ) + 1 ) ) = ( ( 2 ↑ ( 𝑁 + 1 ) ) · 2 ) ) |
| 73 | 54 | a1i | ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 2 ∈ ℕ0 ) |
| 74 | 73 71 | nn0expcld | ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 ↑ ( 𝑁 + 1 ) ) ∈ ℕ0 ) |
| 75 | 74 | nn0cnd | ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 ↑ ( 𝑁 + 1 ) ) ∈ ℂ ) |
| 76 | 75 69 | mulcomd | ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 2 ↑ ( 𝑁 + 1 ) ) · 2 ) = ( 2 · ( 2 ↑ ( 𝑁 + 1 ) ) ) ) |
| 77 | 68 72 76 | 3eqtrd | ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 ↑ ( 𝑁 + 2 ) ) = ( 2 · ( 2 ↑ ( 𝑁 + 1 ) ) ) ) |
| 78 | 77 | adantr | ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑛 ∈ ℕ0 ) → ( 2 ↑ ( 𝑁 + 2 ) ) = ( 2 · ( 2 ↑ ( 𝑁 + 1 ) ) ) ) |
| 79 | 78 | oveq2d | ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) = ( 𝑛 · ( 2 · ( 2 ↑ ( 𝑁 + 1 ) ) ) ) ) |
| 80 | nn0cn | ⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℂ ) | |
| 81 | 80 | adantl | ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℂ ) |
| 82 | 2cnd | ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑛 ∈ ℕ0 ) → 2 ∈ ℂ ) | |
| 83 | 75 | adantr | ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑛 ∈ ℕ0 ) → ( 2 ↑ ( 𝑁 + 1 ) ) ∈ ℂ ) |
| 84 | 81 82 83 | mulassd | ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑛 · 2 ) · ( 2 ↑ ( 𝑁 + 1 ) ) ) = ( 𝑛 · ( 2 · ( 2 ↑ ( 𝑁 + 1 ) ) ) ) ) |
| 85 | 79 84 | eqtr4d | ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) = ( ( 𝑛 · 2 ) · ( 2 ↑ ( 𝑁 + 1 ) ) ) ) |
| 86 | 85 | 3ad2antl1 | ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑀 ∥ ( FermatNo ‘ 𝑁 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) = ( ( 𝑛 · 2 ) · ( 2 ↑ ( 𝑁 + 1 ) ) ) ) |
| 87 | 86 | adantr | ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑀 ∥ ( FermatNo ‘ 𝑁 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑀 = ( ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) → ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) = ( ( 𝑛 · 2 ) · ( 2 ↑ ( 𝑁 + 1 ) ) ) ) |
| 88 | 87 | oveq1d | ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑀 ∥ ( FermatNo ‘ 𝑁 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑀 = ( ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) → ( ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) = ( ( ( 𝑛 · 2 ) · ( 2 ↑ ( 𝑁 + 1 ) ) ) + 1 ) ) |
| 89 | 58 62 88 | rspcedvd | ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑀 ∥ ( FermatNo ‘ 𝑁 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑀 = ( ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) → ∃ 𝑘 ∈ ℕ0 𝑀 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 1 ) ) ) + 1 ) ) |
| 90 | 89 | rexlimdva2 | ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑀 ∥ ( FermatNo ‘ 𝑁 ) ) → ( ∃ 𝑛 ∈ ℕ0 𝑀 = ( ( 𝑛 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) → ∃ 𝑘 ∈ ℕ0 𝑀 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 1 ) ) ) + 1 ) ) ) |
| 91 | 52 90 | mpd | ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℕ ∧ 𝑀 ∥ ( FermatNo ‘ 𝑁 ) ) → ∃ 𝑘 ∈ ℕ0 𝑀 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 1 ) ) ) + 1 ) ) |
| 92 | 91 | 3exp | ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑀 ∈ ℕ → ( 𝑀 ∥ ( FermatNo ‘ 𝑁 ) → ∃ 𝑘 ∈ ℕ0 𝑀 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 1 ) ) ) + 1 ) ) ) ) |
| 93 | 51 92 | jaoi | ⊢ ( ( 𝑁 = 1 ∨ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑀 ∈ ℕ → ( 𝑀 ∥ ( FermatNo ‘ 𝑁 ) → ∃ 𝑘 ∈ ℕ0 𝑀 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 1 ) ) ) + 1 ) ) ) ) |
| 94 | 1 93 | sylbi | ⊢ ( 𝑁 ∈ ℕ → ( 𝑀 ∈ ℕ → ( 𝑀 ∥ ( FermatNo ‘ 𝑁 ) → ∃ 𝑘 ∈ ℕ0 𝑀 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 1 ) ) ) + 1 ) ) ) ) |
| 95 | 94 | 3imp | ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑀 ∥ ( FermatNo ‘ 𝑁 ) ) → ∃ 𝑘 ∈ ℕ0 𝑀 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 1 ) ) ) + 1 ) ) |