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 ( ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) ∧ 𝑀 ∈ β„• ∧ 𝑀 βˆ₯ ( FermatNo β€˜ 𝑁 ) ) β†’ βˆƒ π‘˜ ∈ β„•0 𝑀 = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) )

Proof

Step Hyp Ref Expression
1 breq1 ⊒ ( π‘₯ = 1 β†’ ( π‘₯ βˆ₯ ( FermatNo β€˜ 𝑁 ) ↔ 1 βˆ₯ ( FermatNo β€˜ 𝑁 ) ) )
2 1 anbi2d ⊒ ( π‘₯ = 1 β†’ ( ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) ∧ π‘₯ βˆ₯ ( FermatNo β€˜ 𝑁 ) ) ↔ ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) ∧ 1 βˆ₯ ( FermatNo β€˜ 𝑁 ) ) ) )
3 eqeq1 ⊒ ( π‘₯ = 1 β†’ ( π‘₯ = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ↔ 1 = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) )
4 3 rexbidv ⊒ ( π‘₯ = 1 β†’ ( βˆƒ π‘˜ ∈ β„•0 π‘₯ = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ↔ βˆƒ π‘˜ ∈ β„•0 1 = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) )
5 2 4 imbi12d ⊒ ( π‘₯ = 1 β†’ ( ( ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) ∧ π‘₯ βˆ₯ ( FermatNo β€˜ 𝑁 ) ) β†’ βˆƒ π‘˜ ∈ β„•0 π‘₯ = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) ↔ ( ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) ∧ 1 βˆ₯ ( FermatNo β€˜ 𝑁 ) ) β†’ βˆƒ π‘˜ ∈ β„•0 1 = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) ) )
6 breq1 ⊒ ( π‘₯ = 𝑦 β†’ ( π‘₯ βˆ₯ ( FermatNo β€˜ 𝑁 ) ↔ 𝑦 βˆ₯ ( FermatNo β€˜ 𝑁 ) ) )
7 6 anbi2d ⊒ ( π‘₯ = 𝑦 β†’ ( ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) ∧ π‘₯ βˆ₯ ( FermatNo β€˜ 𝑁 ) ) ↔ ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) ∧ 𝑦 βˆ₯ ( FermatNo β€˜ 𝑁 ) ) ) )
8 eqeq1 ⊒ ( π‘₯ = 𝑦 β†’ ( π‘₯ = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ↔ 𝑦 = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) )
9 8 rexbidv ⊒ ( π‘₯ = 𝑦 β†’ ( βˆƒ π‘˜ ∈ β„•0 π‘₯ = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ↔ βˆƒ π‘˜ ∈ β„•0 𝑦 = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) )
10 7 9 imbi12d ⊒ ( π‘₯ = 𝑦 β†’ ( ( ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) ∧ π‘₯ βˆ₯ ( FermatNo β€˜ 𝑁 ) ) β†’ βˆƒ π‘˜ ∈ β„•0 π‘₯ = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) ↔ ( ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) ∧ 𝑦 βˆ₯ ( FermatNo β€˜ 𝑁 ) ) β†’ βˆƒ π‘˜ ∈ β„•0 𝑦 = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) ) )
11 breq1 ⊒ ( π‘₯ = 𝑧 β†’ ( π‘₯ βˆ₯ ( FermatNo β€˜ 𝑁 ) ↔ 𝑧 βˆ₯ ( FermatNo β€˜ 𝑁 ) ) )
12 11 anbi2d ⊒ ( π‘₯ = 𝑧 β†’ ( ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) ∧ π‘₯ βˆ₯ ( FermatNo β€˜ 𝑁 ) ) ↔ ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) ∧ 𝑧 βˆ₯ ( FermatNo β€˜ 𝑁 ) ) ) )
13 eqeq1 ⊒ ( π‘₯ = 𝑧 β†’ ( π‘₯ = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ↔ 𝑧 = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) )
14 13 rexbidv ⊒ ( π‘₯ = 𝑧 β†’ ( βˆƒ π‘˜ ∈ β„•0 π‘₯ = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ↔ βˆƒ π‘˜ ∈ β„•0 𝑧 = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) )
15 12 14 imbi12d ⊒ ( π‘₯ = 𝑧 β†’ ( ( ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) ∧ π‘₯ βˆ₯ ( FermatNo β€˜ 𝑁 ) ) β†’ βˆƒ π‘˜ ∈ β„•0 π‘₯ = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) ↔ ( ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) ∧ 𝑧 βˆ₯ ( FermatNo β€˜ 𝑁 ) ) β†’ βˆƒ π‘˜ ∈ β„•0 𝑧 = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) ) )
16 breq1 ⊒ ( π‘₯ = ( 𝑦 Β· 𝑧 ) β†’ ( π‘₯ βˆ₯ ( FermatNo β€˜ 𝑁 ) ↔ ( 𝑦 Β· 𝑧 ) βˆ₯ ( FermatNo β€˜ 𝑁 ) ) )
17 16 anbi2d ⊒ ( π‘₯ = ( 𝑦 Β· 𝑧 ) β†’ ( ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) ∧ π‘₯ βˆ₯ ( FermatNo β€˜ 𝑁 ) ) ↔ ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) ∧ ( 𝑦 Β· 𝑧 ) βˆ₯ ( FermatNo β€˜ 𝑁 ) ) ) )
18 eqeq1 ⊒ ( π‘₯ = ( 𝑦 Β· 𝑧 ) β†’ ( π‘₯ = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ↔ ( 𝑦 Β· 𝑧 ) = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) )
19 18 rexbidv ⊒ ( π‘₯ = ( 𝑦 Β· 𝑧 ) β†’ ( βˆƒ π‘˜ ∈ β„•0 π‘₯ = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ↔ βˆƒ π‘˜ ∈ β„•0 ( 𝑦 Β· 𝑧 ) = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) )
20 17 19 imbi12d ⊒ ( π‘₯ = ( 𝑦 Β· 𝑧 ) β†’ ( ( ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) ∧ π‘₯ βˆ₯ ( FermatNo β€˜ 𝑁 ) ) β†’ βˆƒ π‘˜ ∈ β„•0 π‘₯ = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) ↔ ( ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) ∧ ( 𝑦 Β· 𝑧 ) βˆ₯ ( FermatNo β€˜ 𝑁 ) ) β†’ βˆƒ π‘˜ ∈ β„•0 ( 𝑦 Β· 𝑧 ) = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) ) )
21 breq1 ⊒ ( π‘₯ = 𝑀 β†’ ( π‘₯ βˆ₯ ( FermatNo β€˜ 𝑁 ) ↔ 𝑀 βˆ₯ ( FermatNo β€˜ 𝑁 ) ) )
22 21 anbi2d ⊒ ( π‘₯ = 𝑀 β†’ ( ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) ∧ π‘₯ βˆ₯ ( FermatNo β€˜ 𝑁 ) ) ↔ ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) ∧ 𝑀 βˆ₯ ( FermatNo β€˜ 𝑁 ) ) ) )
23 eqeq1 ⊒ ( π‘₯ = 𝑀 β†’ ( π‘₯ = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ↔ 𝑀 = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) )
24 23 rexbidv ⊒ ( π‘₯ = 𝑀 β†’ ( βˆƒ π‘˜ ∈ β„•0 π‘₯ = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ↔ βˆƒ π‘˜ ∈ β„•0 𝑀 = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) )
25 22 24 imbi12d ⊒ ( π‘₯ = 𝑀 β†’ ( ( ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) ∧ π‘₯ βˆ₯ ( FermatNo β€˜ 𝑁 ) ) β†’ βˆƒ π‘˜ ∈ β„•0 π‘₯ = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) ↔ ( ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) ∧ 𝑀 βˆ₯ ( FermatNo β€˜ 𝑁 ) ) β†’ βˆƒ π‘˜ ∈ β„•0 𝑀 = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) ) )
26 0nn0 ⊒ 0 ∈ β„•0
27 26 a1i ⊒ ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) β†’ 0 ∈ β„•0 )
28 oveq1 ⊒ ( π‘˜ = 0 β†’ ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) = ( 0 Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) )
29 28 oveq1d ⊒ ( π‘˜ = 0 β†’ ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) = ( ( 0 Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) )
30 29 eqeq2d ⊒ ( π‘˜ = 0 β†’ ( 1 = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ↔ 1 = ( ( 0 Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) )
31 30 adantl ⊒ ( ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) ∧ π‘˜ = 0 ) β†’ ( 1 = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ↔ 1 = ( ( 0 Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) )
32 2nn0 ⊒ 2 ∈ β„•0
33 32 a1i ⊒ ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) β†’ 2 ∈ β„•0 )
34 eluzge2nn0 ⊒ ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) β†’ 𝑁 ∈ β„•0 )
35 34 33 nn0addcld ⊒ ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) β†’ ( 𝑁 + 2 ) ∈ β„•0 )
36 33 35 nn0expcld ⊒ ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) β†’ ( 2 ↑ ( 𝑁 + 2 ) ) ∈ β„•0 )
37 36 nn0cnd ⊒ ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) β†’ ( 2 ↑ ( 𝑁 + 2 ) ) ∈ β„‚ )
38 37 mul02d ⊒ ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) β†’ ( 0 Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) = 0 )
39 38 oveq1d ⊒ ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) β†’ ( ( 0 Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) = ( 0 + 1 ) )
40 0p1e1 ⊒ ( 0 + 1 ) = 1
41 39 40 eqtr2di ⊒ ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) β†’ 1 = ( ( 0 Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) )
42 27 31 41 rspcedvd ⊒ ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) β†’ βˆƒ π‘˜ ∈ β„•0 1 = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) )
43 42 adantr ⊒ ( ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) ∧ 1 βˆ₯ ( FermatNo β€˜ 𝑁 ) ) β†’ βˆƒ π‘˜ ∈ β„•0 1 = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) )
44 simpl ⊒ ( ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) ∧ π‘₯ βˆ₯ ( FermatNo β€˜ 𝑁 ) ) β†’ 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) )
45 44 adantl ⊒ ( ( π‘₯ ∈ β„™ ∧ ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) ∧ π‘₯ βˆ₯ ( FermatNo β€˜ 𝑁 ) ) ) β†’ 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) )
46 simpl ⊒ ( ( π‘₯ ∈ β„™ ∧ ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) ∧ π‘₯ βˆ₯ ( FermatNo β€˜ 𝑁 ) ) ) β†’ π‘₯ ∈ β„™ )
47 simprr ⊒ ( ( π‘₯ ∈ β„™ ∧ ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) ∧ π‘₯ βˆ₯ ( FermatNo β€˜ 𝑁 ) ) ) β†’ π‘₯ βˆ₯ ( FermatNo β€˜ 𝑁 ) )
48 nnssnn0 ⊒ β„• βŠ† β„•0
49 fmtnoprmfac2 ⊒ ( ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) ∧ π‘₯ ∈ β„™ ∧ π‘₯ βˆ₯ ( FermatNo β€˜ 𝑁 ) ) β†’ βˆƒ π‘˜ ∈ β„• π‘₯ = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) )
50 ssrexv ⊒ ( β„• βŠ† β„•0 β†’ ( βˆƒ π‘˜ ∈ β„• π‘₯ = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) β†’ βˆƒ π‘˜ ∈ β„•0 π‘₯ = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) )
51 48 49 50 mpsyl ⊒ ( ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) ∧ π‘₯ ∈ β„™ ∧ π‘₯ βˆ₯ ( FermatNo β€˜ 𝑁 ) ) β†’ βˆƒ π‘˜ ∈ β„•0 π‘₯ = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) )
52 45 46 47 51 syl3anc ⊒ ( ( π‘₯ ∈ β„™ ∧ ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) ∧ π‘₯ βˆ₯ ( FermatNo β€˜ 𝑁 ) ) ) β†’ βˆƒ π‘˜ ∈ β„•0 π‘₯ = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) )
53 52 ex ⊒ ( π‘₯ ∈ β„™ β†’ ( ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) ∧ π‘₯ βˆ₯ ( FermatNo β€˜ 𝑁 ) ) β†’ βˆƒ π‘˜ ∈ β„•0 π‘₯ = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) )
54 fmtnofac2lem ⊒ ( ( 𝑦 ∈ ( β„€β‰₯ β€˜ 2 ) ∧ 𝑧 ∈ ( β„€β‰₯ β€˜ 2 ) ) β†’ ( ( ( ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) ∧ 𝑦 βˆ₯ ( FermatNo β€˜ 𝑁 ) ) β†’ βˆƒ π‘˜ ∈ β„•0 𝑦 = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) ∧ ( ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) ∧ 𝑧 βˆ₯ ( FermatNo β€˜ 𝑁 ) ) β†’ βˆƒ π‘˜ ∈ β„•0 𝑧 = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) ) β†’ ( ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) ∧ ( 𝑦 Β· 𝑧 ) βˆ₯ ( FermatNo β€˜ 𝑁 ) ) β†’ βˆƒ π‘˜ ∈ β„•0 ( 𝑦 Β· 𝑧 ) = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) ) )
55 5 10 15 20 25 43 53 54 prmind ⊒ ( 𝑀 ∈ β„• β†’ ( ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) ∧ 𝑀 βˆ₯ ( FermatNo β€˜ 𝑁 ) ) β†’ βˆƒ π‘˜ ∈ β„•0 𝑀 = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) )
56 55 expd ⊒ ( 𝑀 ∈ β„• β†’ ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) β†’ ( 𝑀 βˆ₯ ( FermatNo β€˜ 𝑁 ) β†’ βˆƒ π‘˜ ∈ β„•0 𝑀 = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) ) )
57 56 3imp21 ⊒ ( ( 𝑁 ∈ ( β„€β‰₯ β€˜ 2 ) ∧ 𝑀 ∈ β„• ∧ 𝑀 βˆ₯ ( FermatNo β€˜ 𝑁 ) ) β†’ βˆƒ π‘˜ ∈ β„•0 𝑀 = ( ( π‘˜ Β· ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) )