Metamath Proof Explorer

Theorem fmtnofac2

Description: Divisor of Fermat number (Euler's Result refined by François Édouard Anatole Lucas), see fmtnofac1 : Let F_n be a Fermat number. Let m be divisor of F_n. Then m is in the form: k*2^(n+2)+1 where k is a nonnegative integer. (Contributed by AV, 30-Jul-2021)

Ref Expression
Assertion fmtnofac2 
|- ( ( N e. ( ZZ>= ` 2 ) /\ M e. NN /\ M || ( FermatNo ` N ) ) -> E. k e. NN0 M = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) )

Proof

Step Hyp Ref Expression
1 breq1 
 |-  ( x = 1 -> ( x || ( FermatNo ` N ) <-> 1 || ( FermatNo ` N ) ) )
2 1 anbi2d 
 |-  ( x = 1 -> ( ( N e. ( ZZ>= ` 2 ) /\ x || ( FermatNo ` N ) ) <-> ( N e. ( ZZ>= ` 2 ) /\ 1 || ( FermatNo ` N ) ) ) )
3 eqeq1 
 |-  ( x = 1 -> ( x = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) <-> 1 = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) )
4 3 rexbidv 
 |-  ( x = 1 -> ( E. k e. NN0 x = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) <-> E. k e. NN0 1 = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) )
5 2 4 imbi12d 
 |-  ( x = 1 -> ( ( ( N e. ( ZZ>= ` 2 ) /\ x || ( FermatNo ` N ) ) -> E. k e. NN0 x = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) <-> ( ( N e. ( ZZ>= ` 2 ) /\ 1 || ( FermatNo ` N ) ) -> E. k e. NN0 1 = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) ) )
6 breq1 
 |-  ( x = y -> ( x || ( FermatNo ` N ) <-> y || ( FermatNo ` N ) ) )
7 6 anbi2d 
 |-  ( x = y -> ( ( N e. ( ZZ>= ` 2 ) /\ x || ( FermatNo ` N ) ) <-> ( N e. ( ZZ>= ` 2 ) /\ y || ( FermatNo ` N ) ) ) )
8 eqeq1 
 |-  ( x = y -> ( x = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) <-> y = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) )
9 8 rexbidv 
 |-  ( x = y -> ( E. k e. NN0 x = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) <-> E. k e. NN0 y = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) )
10 7 9 imbi12d 
 |-  ( x = y -> ( ( ( N e. ( ZZ>= ` 2 ) /\ x || ( FermatNo ` N ) ) -> E. k e. NN0 x = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) <-> ( ( N e. ( ZZ>= ` 2 ) /\ y || ( FermatNo ` N ) ) -> E. k e. NN0 y = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) ) )
11 breq1 
 |-  ( x = z -> ( x || ( FermatNo ` N ) <-> z || ( FermatNo ` N ) ) )
12 11 anbi2d 
 |-  ( x = z -> ( ( N e. ( ZZ>= ` 2 ) /\ x || ( FermatNo ` N ) ) <-> ( N e. ( ZZ>= ` 2 ) /\ z || ( FermatNo ` N ) ) ) )
13 eqeq1 
 |-  ( x = z -> ( x = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) <-> z = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) )
14 13 rexbidv 
 |-  ( x = z -> ( E. k e. NN0 x = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) <-> E. k e. NN0 z = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) )
15 12 14 imbi12d 
 |-  ( x = z -> ( ( ( N e. ( ZZ>= ` 2 ) /\ x || ( FermatNo ` N ) ) -> E. k e. NN0 x = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) <-> ( ( N e. ( ZZ>= ` 2 ) /\ z || ( FermatNo ` N ) ) -> E. k e. NN0 z = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) ) )
16 breq1 
 |-  ( x = ( y x. z ) -> ( x || ( FermatNo ` N ) <-> ( y x. z ) || ( FermatNo ` N ) ) )
17 16 anbi2d 
 |-  ( x = ( y x. z ) -> ( ( N e. ( ZZ>= ` 2 ) /\ x || ( FermatNo ` N ) ) <-> ( N e. ( ZZ>= ` 2 ) /\ ( y x. z ) || ( FermatNo ` N ) ) ) )
18 eqeq1 
 |-  ( x = ( y x. z ) -> ( x = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) <-> ( y x. z ) = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) )
19 18 rexbidv 
 |-  ( x = ( y x. z ) -> ( E. k e. NN0 x = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) <-> E. k e. NN0 ( y x. z ) = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) )
20 17 19 imbi12d 
 |-  ( x = ( y x. z ) -> ( ( ( N e. ( ZZ>= ` 2 ) /\ x || ( FermatNo ` N ) ) -> E. k e. NN0 x = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) <-> ( ( N e. ( ZZ>= ` 2 ) /\ ( y x. z ) || ( FermatNo ` N ) ) -> E. k e. NN0 ( y x. z ) = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) ) )
21 breq1 
 |-  ( x = M -> ( x || ( FermatNo ` N ) <-> M || ( FermatNo ` N ) ) )
22 21 anbi2d 
 |-  ( x = M -> ( ( N e. ( ZZ>= ` 2 ) /\ x || ( FermatNo ` N ) ) <-> ( N e. ( ZZ>= ` 2 ) /\ M || ( FermatNo ` N ) ) ) )
23 eqeq1 
 |-  ( x = M -> ( x = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) <-> M = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) )
24 23 rexbidv 
 |-  ( x = M -> ( E. k e. NN0 x = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) <-> E. k e. NN0 M = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) )
25 22 24 imbi12d 
 |-  ( x = M -> ( ( ( N e. ( ZZ>= ` 2 ) /\ x || ( FermatNo ` N ) ) -> E. k e. NN0 x = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) <-> ( ( N e. ( ZZ>= ` 2 ) /\ M || ( FermatNo ` N ) ) -> E. k e. NN0 M = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) ) )
26 0nn0 
 |-  0 e. NN0
27 26 a1i 
 |-  ( N e. ( ZZ>= ` 2 ) -> 0 e. NN0 )
28 oveq1 
 |-  ( k = 0 -> ( k x. ( 2 ^ ( N + 2 ) ) ) = ( 0 x. ( 2 ^ ( N + 2 ) ) ) )
29 28 oveq1d 
 |-  ( k = 0 -> ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) = ( ( 0 x. ( 2 ^ ( N + 2 ) ) ) + 1 ) )
30 29 eqeq2d 
 |-  ( k = 0 -> ( 1 = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) <-> 1 = ( ( 0 x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) )
31 30 adantl 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ k = 0 ) -> ( 1 = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) <-> 1 = ( ( 0 x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) )
32 2nn0 
 |-  2 e. NN0
33 32 a1i 
 |-  ( N e. ( ZZ>= ` 2 ) -> 2 e. NN0 )
34 eluzge2nn0 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. NN0 )
35 34 33 nn0addcld 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N + 2 ) e. NN0 )
36 33 35 nn0expcld 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 2 ^ ( N + 2 ) ) e. NN0 )
37 36 nn0cnd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 2 ^ ( N + 2 ) ) e. CC )
38 37 mul02d 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 0 x. ( 2 ^ ( N + 2 ) ) ) = 0 )
39 38 oveq1d 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( 0 x. ( 2 ^ ( N + 2 ) ) ) + 1 ) = ( 0 + 1 ) )
40 0p1e1 
 |-  ( 0 + 1 ) = 1
41 39 40 eqtr2di 
 |-  ( N e. ( ZZ>= ` 2 ) -> 1 = ( ( 0 x. ( 2 ^ ( N + 2 ) ) ) + 1 ) )
42 27 31 41 rspcedvd 
 |-  ( N e. ( ZZ>= ` 2 ) -> E. k e. NN0 1 = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) )
43 42 adantr 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ 1 || ( FermatNo ` N ) ) -> E. k e. NN0 1 = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) )
44 simpl 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ x || ( FermatNo ` N ) ) -> N e. ( ZZ>= ` 2 ) )
45 44 adantl 
 |-  ( ( x e. Prime /\ ( N e. ( ZZ>= ` 2 ) /\ x || ( FermatNo ` N ) ) ) -> N e. ( ZZ>= ` 2 ) )
46 simpl 
 |-  ( ( x e. Prime /\ ( N e. ( ZZ>= ` 2 ) /\ x || ( FermatNo ` N ) ) ) -> x e. Prime )
47 simprr 
 |-  ( ( x e. Prime /\ ( N e. ( ZZ>= ` 2 ) /\ x || ( FermatNo ` N ) ) ) -> x || ( FermatNo ` N ) )
48 nnssnn0 
 |-  NN C_ NN0
49 fmtnoprmfac2 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ x e. Prime /\ x || ( FermatNo ` N ) ) -> E. k e. NN x = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) )
50 ssrexv 
 |-  ( NN C_ NN0 -> ( E. k e. NN x = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) -> E. k e. NN0 x = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) )
51 48 49 50 mpsyl 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ x e. Prime /\ x || ( FermatNo ` N ) ) -> E. k e. NN0 x = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) )
52 45 46 47 51 syl3anc 
 |-  ( ( x e. Prime /\ ( N e. ( ZZ>= ` 2 ) /\ x || ( FermatNo ` N ) ) ) -> E. k e. NN0 x = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) )
53 52 ex 
 |-  ( x e. Prime -> ( ( N e. ( ZZ>= ` 2 ) /\ x || ( FermatNo ` N ) ) -> E. k e. NN0 x = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) )
54 fmtnofac2lem 
 |-  ( ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) -> ( ( ( ( N e. ( ZZ>= ` 2 ) /\ y || ( FermatNo ` N ) ) -> E. k e. NN0 y = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) /\ ( ( N e. ( ZZ>= ` 2 ) /\ z || ( FermatNo ` N ) ) -> E. k e. NN0 z = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) ) -> ( ( N e. ( ZZ>= ` 2 ) /\ ( y x. z ) || ( FermatNo ` N ) ) -> E. k e. NN0 ( y x. z ) = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) ) )
55 5 10 15 20 25 43 53 54 prmind 
 |-  ( M e. NN -> ( ( N e. ( ZZ>= ` 2 ) /\ M || ( FermatNo ` N ) ) -> E. k e. NN0 M = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) )
56 55 expd 
 |-  ( M e. NN -> ( N e. ( ZZ>= ` 2 ) -> ( M || ( FermatNo ` N ) -> E. k e. NN0 M = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) ) )
57 56 3imp21 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ M e. NN /\ M || ( FermatNo ` N ) ) -> E. k e. NN0 M = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) )