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 ) )