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 | |- ( ( N e. NN /\ M e. NN /\ M || ( FermatNo ` N ) ) -> E. k e. NN0 M = ( ( k x. ( 2 ^ ( N + 1 ) ) ) + 1 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elnn1uz2 | |- ( N e. NN <-> ( N = 1 \/ N e. ( ZZ>= ` 2 ) ) ) |
|
| 2 | 5prm | |- 5 e. Prime |
|
| 3 | dvdsprime | |- ( ( 5 e. Prime /\ M e. NN ) -> ( M || 5 <-> ( M = 5 \/ M = 1 ) ) ) |
|
| 4 | 2 3 | mpan | |- ( M e. NN -> ( M || 5 <-> ( M = 5 \/ M = 1 ) ) ) |
| 5 | 1nn0 | |- 1 e. NN0 |
|
| 6 | 5 | a1i | |- ( M = 5 -> 1 e. NN0 ) |
| 7 | simpl | |- ( ( M = 5 /\ k = 1 ) -> M = 5 ) |
|
| 8 | oveq1 | |- ( k = 1 -> ( k x. 4 ) = ( 1 x. 4 ) ) |
|
| 9 | 8 | oveq1d | |- ( k = 1 -> ( ( k x. 4 ) + 1 ) = ( ( 1 x. 4 ) + 1 ) ) |
| 10 | 9 | adantl | |- ( ( M = 5 /\ k = 1 ) -> ( ( k x. 4 ) + 1 ) = ( ( 1 x. 4 ) + 1 ) ) |
| 11 | 7 10 | eqeq12d | |- ( ( M = 5 /\ k = 1 ) -> ( M = ( ( k x. 4 ) + 1 ) <-> 5 = ( ( 1 x. 4 ) + 1 ) ) ) |
| 12 | df-5 | |- 5 = ( 4 + 1 ) |
|
| 13 | 4cn | |- 4 e. CC |
|
| 14 | 13 | mulid2i | |- ( 1 x. 4 ) = 4 |
| 15 | 14 | eqcomi | |- 4 = ( 1 x. 4 ) |
| 16 | 15 | oveq1i | |- ( 4 + 1 ) = ( ( 1 x. 4 ) + 1 ) |
| 17 | 12 16 | eqtri | |- 5 = ( ( 1 x. 4 ) + 1 ) |
| 18 | 17 | a1i | |- ( M = 5 -> 5 = ( ( 1 x. 4 ) + 1 ) ) |
| 19 | 6 11 18 | rspcedvd | |- ( M = 5 -> E. k e. NN0 M = ( ( k x. 4 ) + 1 ) ) |
| 20 | 0nn0 | |- 0 e. NN0 |
|
| 21 | 20 | a1i | |- ( M = 1 -> 0 e. NN0 ) |
| 22 | simpl | |- ( ( M = 1 /\ k = 0 ) -> M = 1 ) |
|
| 23 | oveq1 | |- ( k = 0 -> ( k x. 4 ) = ( 0 x. 4 ) ) |
|
| 24 | 23 | oveq1d | |- ( k = 0 -> ( ( k x. 4 ) + 1 ) = ( ( 0 x. 4 ) + 1 ) ) |
| 25 | 24 | adantl | |- ( ( M = 1 /\ k = 0 ) -> ( ( k x. 4 ) + 1 ) = ( ( 0 x. 4 ) + 1 ) ) |
| 26 | 22 25 | eqeq12d | |- ( ( M = 1 /\ k = 0 ) -> ( M = ( ( k x. 4 ) + 1 ) <-> 1 = ( ( 0 x. 4 ) + 1 ) ) ) |
| 27 | 13 | mul02i | |- ( 0 x. 4 ) = 0 |
| 28 | 27 | oveq1i | |- ( ( 0 x. 4 ) + 1 ) = ( 0 + 1 ) |
| 29 | 0p1e1 | |- ( 0 + 1 ) = 1 |
|
| 30 | 28 29 | eqtri | |- ( ( 0 x. 4 ) + 1 ) = 1 |
| 31 | 30 | eqcomi | |- 1 = ( ( 0 x. 4 ) + 1 ) |
| 32 | 31 | a1i | |- ( M = 1 -> 1 = ( ( 0 x. 4 ) + 1 ) ) |
| 33 | 21 26 32 | rspcedvd | |- ( M = 1 -> E. k e. NN0 M = ( ( k x. 4 ) + 1 ) ) |
| 34 | 19 33 | jaoi | |- ( ( M = 5 \/ M = 1 ) -> E. k e. NN0 M = ( ( k x. 4 ) + 1 ) ) |
| 35 | 4 34 | syl6bi | |- ( M e. NN -> ( M || 5 -> E. k e. NN0 M = ( ( k x. 4 ) + 1 ) ) ) |
| 36 | fveq2 | |- ( N = 1 -> ( FermatNo ` N ) = ( FermatNo ` 1 ) ) |
|
| 37 | fmtno1 | |- ( FermatNo ` 1 ) = 5 |
|
| 38 | 36 37 | eqtrdi | |- ( N = 1 -> ( FermatNo ` N ) = 5 ) |
| 39 | 38 | breq2d | |- ( N = 1 -> ( M || ( FermatNo ` N ) <-> M || 5 ) ) |
| 40 | oveq1 | |- ( N = 1 -> ( N + 1 ) = ( 1 + 1 ) ) |
|
| 41 | 1p1e2 | |- ( 1 + 1 ) = 2 |
|
| 42 | 40 41 | eqtrdi | |- ( N = 1 -> ( N + 1 ) = 2 ) |
| 43 | 42 | oveq2d | |- ( N = 1 -> ( 2 ^ ( N + 1 ) ) = ( 2 ^ 2 ) ) |
| 44 | sq2 | |- ( 2 ^ 2 ) = 4 |
|
| 45 | 43 44 | eqtrdi | |- ( N = 1 -> ( 2 ^ ( N + 1 ) ) = 4 ) |
| 46 | 45 | oveq2d | |- ( N = 1 -> ( k x. ( 2 ^ ( N + 1 ) ) ) = ( k x. 4 ) ) |
| 47 | 46 | oveq1d | |- ( N = 1 -> ( ( k x. ( 2 ^ ( N + 1 ) ) ) + 1 ) = ( ( k x. 4 ) + 1 ) ) |
| 48 | 47 | eqeq2d | |- ( N = 1 -> ( M = ( ( k x. ( 2 ^ ( N + 1 ) ) ) + 1 ) <-> M = ( ( k x. 4 ) + 1 ) ) ) |
| 49 | 48 | rexbidv | |- ( N = 1 -> ( E. k e. NN0 M = ( ( k x. ( 2 ^ ( N + 1 ) ) ) + 1 ) <-> E. k e. NN0 M = ( ( k x. 4 ) + 1 ) ) ) |
| 50 | 39 49 | imbi12d | |- ( N = 1 -> ( ( M || ( FermatNo ` N ) -> E. k e. NN0 M = ( ( k x. ( 2 ^ ( N + 1 ) ) ) + 1 ) ) <-> ( M || 5 -> E. k e. NN0 M = ( ( k x. 4 ) + 1 ) ) ) ) |
| 51 | 35 50 | syl5ibr | |- ( N = 1 -> ( M e. NN -> ( M || ( FermatNo ` N ) -> E. k e. NN0 M = ( ( k x. ( 2 ^ ( N + 1 ) ) ) + 1 ) ) ) ) |
| 52 | fmtnofac2 | |- ( ( N e. ( ZZ>= ` 2 ) /\ M e. NN /\ M || ( FermatNo ` N ) ) -> E. n e. NN0 M = ( ( n x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) |
|
| 53 | id | |- ( n e. NN0 -> n e. NN0 ) |
|
| 54 | 2nn0 | |- 2 e. NN0 |
|
| 55 | 54 | a1i | |- ( n e. NN0 -> 2 e. NN0 ) |
| 56 | 53 55 | nn0mulcld | |- ( n e. NN0 -> ( n x. 2 ) e. NN0 ) |
| 57 | 56 | adantl | |- ( ( ( N e. ( ZZ>= ` 2 ) /\ M e. NN /\ M || ( FermatNo ` N ) ) /\ n e. NN0 ) -> ( n x. 2 ) e. NN0 ) |
| 58 | 57 | adantr | |- ( ( ( ( N e. ( ZZ>= ` 2 ) /\ M e. NN /\ M || ( FermatNo ` N ) ) /\ n e. NN0 ) /\ M = ( ( n x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) -> ( n x. 2 ) e. NN0 ) |
| 59 | simpr | |- ( ( ( ( N e. ( ZZ>= ` 2 ) /\ M e. NN /\ M || ( FermatNo ` N ) ) /\ n e. NN0 ) /\ M = ( ( n x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) -> M = ( ( n x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) |
|
| 60 | oveq1 | |- ( k = ( n x. 2 ) -> ( k x. ( 2 ^ ( N + 1 ) ) ) = ( ( n x. 2 ) x. ( 2 ^ ( N + 1 ) ) ) ) |
|
| 61 | 60 | oveq1d | |- ( k = ( n x. 2 ) -> ( ( k x. ( 2 ^ ( N + 1 ) ) ) + 1 ) = ( ( ( n x. 2 ) x. ( 2 ^ ( N + 1 ) ) ) + 1 ) ) |
| 62 | 59 61 | eqeqan12d | |- ( ( ( ( ( N e. ( ZZ>= ` 2 ) /\ M e. NN /\ M || ( FermatNo ` N ) ) /\ n e. NN0 ) /\ M = ( ( n x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) /\ k = ( n x. 2 ) ) -> ( M = ( ( k x. ( 2 ^ ( N + 1 ) ) ) + 1 ) <-> ( ( n x. ( 2 ^ ( N + 2 ) ) ) + 1 ) = ( ( ( n x. 2 ) x. ( 2 ^ ( N + 1 ) ) ) + 1 ) ) ) |
| 63 | eluzge2nn0 | |- ( N e. ( ZZ>= ` 2 ) -> N e. NN0 ) |
|
| 64 | 63 | nn0cnd | |- ( N e. ( ZZ>= ` 2 ) -> N e. CC ) |
| 65 | add1p1 | |- ( N e. CC -> ( ( N + 1 ) + 1 ) = ( N + 2 ) ) |
|
| 66 | 64 65 | syl | |- ( N e. ( ZZ>= ` 2 ) -> ( ( N + 1 ) + 1 ) = ( N + 2 ) ) |
| 67 | 66 | eqcomd | |- ( N e. ( ZZ>= ` 2 ) -> ( N + 2 ) = ( ( N + 1 ) + 1 ) ) |
| 68 | 67 | oveq2d | |- ( N e. ( ZZ>= ` 2 ) -> ( 2 ^ ( N + 2 ) ) = ( 2 ^ ( ( N + 1 ) + 1 ) ) ) |
| 69 | 2cnd | |- ( N e. ( ZZ>= ` 2 ) -> 2 e. CC ) |
|
| 70 | peano2nn0 | |- ( N e. NN0 -> ( N + 1 ) e. NN0 ) |
|
| 71 | 63 70 | syl | |- ( N e. ( ZZ>= ` 2 ) -> ( N + 1 ) e. NN0 ) |
| 72 | 69 71 | expp1d | |- ( N e. ( ZZ>= ` 2 ) -> ( 2 ^ ( ( N + 1 ) + 1 ) ) = ( ( 2 ^ ( N + 1 ) ) x. 2 ) ) |
| 73 | 54 | a1i | |- ( N e. ( ZZ>= ` 2 ) -> 2 e. NN0 ) |
| 74 | 73 71 | nn0expcld | |- ( N e. ( ZZ>= ` 2 ) -> ( 2 ^ ( N + 1 ) ) e. NN0 ) |
| 75 | 74 | nn0cnd | |- ( N e. ( ZZ>= ` 2 ) -> ( 2 ^ ( N + 1 ) ) e. CC ) |
| 76 | 75 69 | mulcomd | |- ( N e. ( ZZ>= ` 2 ) -> ( ( 2 ^ ( N + 1 ) ) x. 2 ) = ( 2 x. ( 2 ^ ( N + 1 ) ) ) ) |
| 77 | 68 72 76 | 3eqtrd | |- ( N e. ( ZZ>= ` 2 ) -> ( 2 ^ ( N + 2 ) ) = ( 2 x. ( 2 ^ ( N + 1 ) ) ) ) |
| 78 | 77 | adantr | |- ( ( N e. ( ZZ>= ` 2 ) /\ n e. NN0 ) -> ( 2 ^ ( N + 2 ) ) = ( 2 x. ( 2 ^ ( N + 1 ) ) ) ) |
| 79 | 78 | oveq2d | |- ( ( N e. ( ZZ>= ` 2 ) /\ n e. NN0 ) -> ( n x. ( 2 ^ ( N + 2 ) ) ) = ( n x. ( 2 x. ( 2 ^ ( N + 1 ) ) ) ) ) |
| 80 | nn0cn | |- ( n e. NN0 -> n e. CC ) |
|
| 81 | 80 | adantl | |- ( ( N e. ( ZZ>= ` 2 ) /\ n e. NN0 ) -> n e. CC ) |
| 82 | 2cnd | |- ( ( N e. ( ZZ>= ` 2 ) /\ n e. NN0 ) -> 2 e. CC ) |
|
| 83 | 75 | adantr | |- ( ( N e. ( ZZ>= ` 2 ) /\ n e. NN0 ) -> ( 2 ^ ( N + 1 ) ) e. CC ) |
| 84 | 81 82 83 | mulassd | |- ( ( N e. ( ZZ>= ` 2 ) /\ n e. NN0 ) -> ( ( n x. 2 ) x. ( 2 ^ ( N + 1 ) ) ) = ( n x. ( 2 x. ( 2 ^ ( N + 1 ) ) ) ) ) |
| 85 | 79 84 | eqtr4d | |- ( ( N e. ( ZZ>= ` 2 ) /\ n e. NN0 ) -> ( n x. ( 2 ^ ( N + 2 ) ) ) = ( ( n x. 2 ) x. ( 2 ^ ( N + 1 ) ) ) ) |
| 86 | 85 | 3ad2antl1 | |- ( ( ( N e. ( ZZ>= ` 2 ) /\ M e. NN /\ M || ( FermatNo ` N ) ) /\ n e. NN0 ) -> ( n x. ( 2 ^ ( N + 2 ) ) ) = ( ( n x. 2 ) x. ( 2 ^ ( N + 1 ) ) ) ) |
| 87 | 86 | adantr | |- ( ( ( ( N e. ( ZZ>= ` 2 ) /\ M e. NN /\ M || ( FermatNo ` N ) ) /\ n e. NN0 ) /\ M = ( ( n x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) -> ( n x. ( 2 ^ ( N + 2 ) ) ) = ( ( n x. 2 ) x. ( 2 ^ ( N + 1 ) ) ) ) |
| 88 | 87 | oveq1d | |- ( ( ( ( N e. ( ZZ>= ` 2 ) /\ M e. NN /\ M || ( FermatNo ` N ) ) /\ n e. NN0 ) /\ M = ( ( n x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) -> ( ( n x. ( 2 ^ ( N + 2 ) ) ) + 1 ) = ( ( ( n x. 2 ) x. ( 2 ^ ( N + 1 ) ) ) + 1 ) ) |
| 89 | 58 62 88 | rspcedvd | |- ( ( ( ( N e. ( ZZ>= ` 2 ) /\ M e. NN /\ M || ( FermatNo ` N ) ) /\ n e. NN0 ) /\ M = ( ( n x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) -> E. k e. NN0 M = ( ( k x. ( 2 ^ ( N + 1 ) ) ) + 1 ) ) |
| 90 | 89 | rexlimdva2 | |- ( ( N e. ( ZZ>= ` 2 ) /\ M e. NN /\ M || ( FermatNo ` N ) ) -> ( E. n e. NN0 M = ( ( n x. ( 2 ^ ( N + 2 ) ) ) + 1 ) -> E. k e. NN0 M = ( ( k x. ( 2 ^ ( N + 1 ) ) ) + 1 ) ) ) |
| 91 | 52 90 | mpd | |- ( ( N e. ( ZZ>= ` 2 ) /\ M e. NN /\ M || ( FermatNo ` N ) ) -> E. k e. NN0 M = ( ( k x. ( 2 ^ ( N + 1 ) ) ) + 1 ) ) |
| 92 | 91 | 3exp | |- ( N e. ( ZZ>= ` 2 ) -> ( M e. NN -> ( M || ( FermatNo ` N ) -> E. k e. NN0 M = ( ( k x. ( 2 ^ ( N + 1 ) ) ) + 1 ) ) ) ) |
| 93 | 51 92 | jaoi | |- ( ( N = 1 \/ N e. ( ZZ>= ` 2 ) ) -> ( M e. NN -> ( M || ( FermatNo ` N ) -> E. k e. NN0 M = ( ( k x. ( 2 ^ ( N + 1 ) ) ) + 1 ) ) ) ) |
| 94 | 1 93 | sylbi | |- ( N e. NN -> ( M e. NN -> ( M || ( FermatNo ` N ) -> E. k e. NN0 M = ( ( k x. ( 2 ^ ( N + 1 ) ) ) + 1 ) ) ) ) |
| 95 | 94 | 3imp | |- ( ( N e. NN /\ M e. NN /\ M || ( FermatNo ` N ) ) -> E. k e. NN0 M = ( ( k x. ( 2 ^ ( N + 1 ) ) ) + 1 ) ) |