Metamath Proof Explorer

Theorem fmtnoprmfac2

Description: Divisor of Fermat number (special form of Lucas' result, see fmtnofac2 ): Let F_n be a Fermat number. Let p be a prime divisor of F_n. Then p is in the form: k*2^(n+2)+1 where k is a positive integer. (Contributed by AV, 26-Jul-2021)

Ref Expression
Assertion fmtnoprmfac2 ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) → ∃ 𝑘 ∈ ℕ 𝑃 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) )

Proof

Step Hyp Ref Expression
1 breq1 ⊢ ( 𝑃 = 2 → ( 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ↔ 2 ∥ ( FermatNo ‘ 𝑁 ) ) )
2 1 adantr ⊢ ( ( 𝑃 = 2 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ↔ 2 ∥ ( FermatNo ‘ 𝑁 ) ) )
3 eluzge2nn0 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℕ0 )
4 fmtnoodd ⊢ ( 𝑁 ∈ ℕ0 → ¬ 2 ∥ ( FermatNo ‘ 𝑁 ) )
5 3 4 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ¬ 2 ∥ ( FermatNo ‘ 𝑁 ) )
6 5 adantl ⊢ ( ( 𝑃 = 2 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ¬ 2 ∥ ( FermatNo ‘ 𝑁 ) )
7 6 pm2.21d ⊢ ( ( 𝑃 = 2 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 2 ∥ ( FermatNo ‘ 𝑁 ) → ∃ 𝑘 ∈ ℕ 𝑃 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) )
8 2 7 sylbid ⊢ ( ( 𝑃 = 2 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑃 ∥ ( FermatNo ‘ 𝑁 ) → ∃ 𝑘 ∈ ℕ 𝑃 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) )
9 8 a1d ⊢ ( ( 𝑃 = 2 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑃 ∈ ℙ → ( 𝑃 ∥ ( FermatNo ‘ 𝑁 ) → ∃ 𝑘 ∈ ℕ 𝑃 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) ) )
10 9 ex ⊢ ( 𝑃 = 2 → ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑃 ∈ ℙ → ( 𝑃 ∥ ( FermatNo ‘ 𝑁 ) → ∃ 𝑘 ∈ ℕ 𝑃 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) ) ) )
11 10 3impd ⊢ ( 𝑃 = 2 → ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) → ∃ 𝑘 ∈ ℕ 𝑃 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) )
12 simpr1 ⊢ ( ( ¬ 𝑃 = 2 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) ) → 𝑁 ∈ ( ℤ≥ ‘ 2 ) )
13 neqne ⊢ ( ¬ 𝑃 = 2 → 𝑃 ≠ 2 )
14 13 anim2i ⊢ ( ( 𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2 ) → ( 𝑃 ∈ ℙ ∧ 𝑃 ≠ 2 ) )
15 eldifsn ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ↔ ( 𝑃 ∈ ℙ ∧ 𝑃 ≠ 2 ) )
16 14 15 sylibr ⊢ ( ( 𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2 ) → 𝑃 ∈ ( ℙ ∖ { 2 } ) )
17 16 ex ⊢ ( 𝑃 ∈ ℙ → ( ¬ 𝑃 = 2 → 𝑃 ∈ ( ℙ ∖ { 2 } ) ) )
18 17 3ad2ant2 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) → ( ¬ 𝑃 = 2 → 𝑃 ∈ ( ℙ ∖ { 2 } ) ) )
19 18 impcom ⊢ ( ( ¬ 𝑃 = 2 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) ) → 𝑃 ∈ ( ℙ ∖ { 2 } ) )
20 simpr3 ⊢ ( ( ¬ 𝑃 = 2 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) ) → 𝑃 ∥ ( FermatNo ‘ 𝑁 ) )
21 fmtnoprmfac2lem1 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) → ( ( 2 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = 1 )
22 12 19 20 21 syl3anc ⊢ ( ( ¬ 𝑃 = 2 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) ) → ( ( 2 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = 1 )
23 simpl ⊢ ( ( 𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2 ) → 𝑃 ∈ ℙ )
24 2nn ⊢ 2 ∈ ℕ
25 24 a1i ⊢ ( ( 𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2 ) → 2 ∈ ℕ )
26 oddprm ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ )
27 16 26 syl ⊢ ( ( 𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2 ) → ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ )
28 27 nnnn0d ⊢ ( ( 𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2 ) → ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ0 )
29 25 28 nnexpcld ⊢ ( ( 𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2 ) → ( 2 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ∈ ℕ )
30 29 nnzd ⊢ ( ( 𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2 ) → ( 2 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ∈ ℤ )
31 23 30 jca ⊢ ( ( 𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2 ) → ( 𝑃 ∈ ℙ ∧ ( 2 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ∈ ℤ ) )
32 31 ex ⊢ ( 𝑃 ∈ ℙ → ( ¬ 𝑃 = 2 → ( 𝑃 ∈ ℙ ∧ ( 2 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ∈ ℤ ) ) )
33 32 3ad2ant2 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) → ( ¬ 𝑃 = 2 → ( 𝑃 ∈ ℙ ∧ ( 2 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ∈ ℤ ) ) )
34 33 impcom ⊢ ( ( ¬ 𝑃 = 2 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) ) → ( 𝑃 ∈ ℙ ∧ ( 2 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ∈ ℤ ) )
35 modprm1div ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 2 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ∈ ℤ ) → ( ( ( 2 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = 1 ↔ 𝑃 ∥ ( ( 2 ↑ ( ( 𝑃 − 1 ) / 2 ) ) − 1 ) ) )
36 34 35 syl ⊢ ( ( ¬ 𝑃 = 2 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) ) → ( ( ( 2 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = 1 ↔ 𝑃 ∥ ( ( 2 ↑ ( ( 𝑃 − 1 ) / 2 ) ) − 1 ) ) )
37 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
38 37 adantr ⊢ ( ( 𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2 ) → 𝑃 ∈ ℕ )
39 2z ⊢ 2 ∈ ℤ
40 39 a1i ⊢ ( ( 𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2 ) → 2 ∈ ℤ )
41 13 necomd ⊢ ( ¬ 𝑃 = 2 → 2 ≠ 𝑃 )
42 41 adantl ⊢ ( ( 𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2 ) → 2 ≠ 𝑃 )
43 2prm ⊢ 2 ∈ ℙ
44 43 a1i ⊢ ( ¬ 𝑃 = 2 → 2 ∈ ℙ )
45 44 anim2i ⊢ ( ( 𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2 ) → ( 𝑃 ∈ ℙ ∧ 2 ∈ ℙ ) )
46 45 ancomd ⊢ ( ( 𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2 ) → ( 2 ∈ ℙ ∧ 𝑃 ∈ ℙ ) )
47 prmrp ⊢ ( ( 2 ∈ ℙ ∧ 𝑃 ∈ ℙ ) → ( ( 2 gcd 𝑃 ) = 1 ↔ 2 ≠ 𝑃 ) )
48 46 47 syl ⊢ ( ( 𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2 ) → ( ( 2 gcd 𝑃 ) = 1 ↔ 2 ≠ 𝑃 ) )
49 42 48 mpbird ⊢ ( ( 𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2 ) → ( 2 gcd 𝑃 ) = 1 )
50 38 40 49 3jca ⊢ ( ( 𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2 ) → ( 𝑃 ∈ ℕ ∧ 2 ∈ ℤ ∧ ( 2 gcd 𝑃 ) = 1 ) )
51 50 28 jca ⊢ ( ( 𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2 ) → ( ( 𝑃 ∈ ℕ ∧ 2 ∈ ℤ ∧ ( 2 gcd 𝑃 ) = 1 ) ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ0 ) )
52 51 ex ⊢ ( 𝑃 ∈ ℙ → ( ¬ 𝑃 = 2 → ( ( 𝑃 ∈ ℕ ∧ 2 ∈ ℤ ∧ ( 2 gcd 𝑃 ) = 1 ) ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ0 ) ) )
53 52 3ad2ant2 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) → ( ¬ 𝑃 = 2 → ( ( 𝑃 ∈ ℕ ∧ 2 ∈ ℤ ∧ ( 2 gcd 𝑃 ) = 1 ) ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ0 ) ) )
54 53 impcom ⊢ ( ( ¬ 𝑃 = 2 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) ) → ( ( 𝑃 ∈ ℕ ∧ 2 ∈ ℤ ∧ ( 2 gcd 𝑃 ) = 1 ) ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ0 ) )
55 odzdvds ⊢ ( ( ( 𝑃 ∈ ℕ ∧ 2 ∈ ℤ ∧ ( 2 gcd 𝑃 ) = 1 ) ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ0 ) → ( 𝑃 ∥ ( ( 2 ↑ ( ( 𝑃 − 1 ) / 2 ) ) − 1 ) ↔ ( ( odℤ ‘ 𝑃 ) ‘ 2 ) ∥ ( ( 𝑃 − 1 ) / 2 ) ) )
56 54 55 syl ⊢ ( ( ¬ 𝑃 = 2 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) ) → ( 𝑃 ∥ ( ( 2 ↑ ( ( 𝑃 − 1 ) / 2 ) ) − 1 ) ↔ ( ( odℤ ‘ 𝑃 ) ‘ 2 ) ∥ ( ( 𝑃 − 1 ) / 2 ) ) )
57 eluz2nn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℕ )
58 57 3ad2ant1 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) → 𝑁 ∈ ℕ )
59 58 adantl ⊢ ( ( ¬ 𝑃 = 2 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) ) → 𝑁 ∈ ℕ )
60 fmtnoprmfac1lem ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) → ( ( odℤ ‘ 𝑃 ) ‘ 2 ) = ( 2 ↑ ( 𝑁 + 1 ) ) )
61 59 19 20 60 syl3anc ⊢ ( ( ¬ 𝑃 = 2 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) ) → ( ( odℤ ‘ 𝑃 ) ‘ 2 ) = ( 2 ↑ ( 𝑁 + 1 ) ) )
62 breq1 ⊢ ( ( ( odℤ ‘ 𝑃 ) ‘ 2 ) = ( 2 ↑ ( 𝑁 + 1 ) ) → ( ( ( odℤ ‘ 𝑃 ) ‘ 2 ) ∥ ( ( 𝑃 − 1 ) / 2 ) ↔ ( 2 ↑ ( 𝑁 + 1 ) ) ∥ ( ( 𝑃 − 1 ) / 2 ) ) )
63 62 adantl ⊢ ( ( ( ¬ 𝑃 = 2 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) ) ∧ ( ( odℤ ‘ 𝑃 ) ‘ 2 ) = ( 2 ↑ ( 𝑁 + 1 ) ) ) → ( ( ( odℤ ‘ 𝑃 ) ‘ 2 ) ∥ ( ( 𝑃 − 1 ) / 2 ) ↔ ( 2 ↑ ( 𝑁 + 1 ) ) ∥ ( ( 𝑃 − 1 ) / 2 ) ) )
64 24 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 2 ∈ ℕ )
65 peano2nn ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + 1 ) ∈ ℕ )
66 57 65 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 + 1 ) ∈ ℕ )
67 66 nnnn0d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 + 1 ) ∈ ℕ0 )
68 64 67 nnexpcld ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 ↑ ( 𝑁 + 1 ) ) ∈ ℕ )
69 nndivides ⊢ ( ( ( 2 ↑ ( 𝑁 + 1 ) ) ∈ ℕ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ ) → ( ( 2 ↑ ( 𝑁 + 1 ) ) ∥ ( ( 𝑃 − 1 ) / 2 ) ↔ ∃ 𝑘 ∈ ℕ ( 𝑘 · ( 2 ↑ ( 𝑁 + 1 ) ) ) = ( ( 𝑃 − 1 ) / 2 ) ) )
70 68 27 69 syl2an ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2 ) ) → ( ( 2 ↑ ( 𝑁 + 1 ) ) ∥ ( ( 𝑃 − 1 ) / 2 ) ↔ ∃ 𝑘 ∈ ℕ ( 𝑘 · ( 2 ↑ ( 𝑁 + 1 ) ) ) = ( ( 𝑃 − 1 ) / 2 ) ) )
71 eqcom ⊢ ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 1 ) ) ) = ( ( 𝑃 − 1 ) / 2 ) ↔ ( ( 𝑃 − 1 ) / 2 ) = ( 𝑘 · ( 2 ↑ ( 𝑁 + 1 ) ) ) )
72 71 a1i ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 1 ) ) ) = ( ( 𝑃 − 1 ) / 2 ) ↔ ( ( 𝑃 − 1 ) / 2 ) = ( 𝑘 · ( 2 ↑ ( 𝑁 + 1 ) ) ) ) )
73 37 nncnd ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℂ )
74 peano2cnm ⊢ ( 𝑃 ∈ ℂ → ( 𝑃 − 1 ) ∈ ℂ )
75 73 74 syl ⊢ ( 𝑃 ∈ ℙ → ( 𝑃 − 1 ) ∈ ℂ )
76 75 adantl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ) → ( 𝑃 − 1 ) ∈ ℂ )
77 76 adantr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℕ ) → ( 𝑃 − 1 ) ∈ ℂ )
78 simpr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℕ )
79 68 ad2antrr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℕ ) → ( 2 ↑ ( 𝑁 + 1 ) ) ∈ ℕ )
80 78 79 nnmulcld ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℕ ) → ( 𝑘 · ( 2 ↑ ( 𝑁 + 1 ) ) ) ∈ ℕ )
81 80 nncnd ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℕ ) → ( 𝑘 · ( 2 ↑ ( 𝑁 + 1 ) ) ) ∈ ℂ )
82 2cnne0 ⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
83 82 a1i ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℕ ) → ( 2 ∈ ℂ ∧ 2 ≠ 0 ) )
84 divmul3 ⊢ ( ( ( 𝑃 − 1 ) ∈ ℂ ∧ ( 𝑘 · ( 2 ↑ ( 𝑁 + 1 ) ) ) ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( ( 𝑃 − 1 ) / 2 ) = ( 𝑘 · ( 2 ↑ ( 𝑁 + 1 ) ) ) ↔ ( 𝑃 − 1 ) = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 1 ) ) ) · 2 ) ) )
85 77 81 83 84 syl3anc ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℕ ) → ( ( ( 𝑃 − 1 ) / 2 ) = ( 𝑘 · ( 2 ↑ ( 𝑁 + 1 ) ) ) ↔ ( 𝑃 − 1 ) = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 1 ) ) ) · 2 ) ) )
86 nncn ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℂ )
87 86 adantl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℂ )
88 68 nncnd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 ↑ ( 𝑁 + 1 ) ) ∈ ℂ )
89 88 ad2antrr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℕ ) → ( 2 ↑ ( 𝑁 + 1 ) ) ∈ ℂ )
90 2cnd ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℕ ) → 2 ∈ ℂ )
91 87 89 90 mulassd ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 1 ) ) ) · 2 ) = ( 𝑘 · ( ( 2 ↑ ( 𝑁 + 1 ) ) · 2 ) ) )
92 2cnd ⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℂ )
93 65 nnnn0d ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + 1 ) ∈ ℕ0 )
94 92 93 expp1d ⊢ ( 𝑁 ∈ ℕ → ( 2 ↑ ( ( 𝑁 + 1 ) + 1 ) ) = ( ( 2 ↑ ( 𝑁 + 1 ) ) · 2 ) )
95 nncn ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
96 add1p1 ⊢ ( 𝑁 ∈ ℂ → ( ( 𝑁 + 1 ) + 1 ) = ( 𝑁 + 2 ) )
97 95 96 syl ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 + 1 ) + 1 ) = ( 𝑁 + 2 ) )
98 97 oveq2d ⊢ ( 𝑁 ∈ ℕ → ( 2 ↑ ( ( 𝑁 + 1 ) + 1 ) ) = ( 2 ↑ ( 𝑁 + 2 ) ) )
99 94 98 eqtr3d ⊢ ( 𝑁 ∈ ℕ → ( ( 2 ↑ ( 𝑁 + 1 ) ) · 2 ) = ( 2 ↑ ( 𝑁 + 2 ) ) )
100 57 99 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 2 ↑ ( 𝑁 + 1 ) ) · 2 ) = ( 2 ↑ ( 𝑁 + 2 ) ) )
101 100 ad2antrr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℕ ) → ( ( 2 ↑ ( 𝑁 + 1 ) ) · 2 ) = ( 2 ↑ ( 𝑁 + 2 ) ) )
102 101 oveq2d ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℕ ) → ( 𝑘 · ( ( 2 ↑ ( 𝑁 + 1 ) ) · 2 ) ) = ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) )
103 91 102 eqtrd ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 1 ) ) ) · 2 ) = ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) )
104 103 eqeq2d ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑃 − 1 ) = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 1 ) ) ) · 2 ) ↔ ( 𝑃 − 1 ) = ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) ) )
105 73 adantl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ) → 𝑃 ∈ ℂ )
106 105 adantr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℕ ) → 𝑃 ∈ ℂ )
107 1cnd ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℕ ) → 1 ∈ ℂ )
108 id ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ )
109 24 a1i ⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℕ )
110 108 109 nnaddcld ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + 2 ) ∈ ℕ )
111 110 nnnn0d ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + 2 ) ∈ ℕ0 )
112 57 111 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 + 2 ) ∈ ℕ0 )
113 64 112 nnexpcld ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 ↑ ( 𝑁 + 2 ) ) ∈ ℕ )
114 113 nncnd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 ↑ ( 𝑁 + 2 ) ) ∈ ℂ )
115 114 ad2antrr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℕ ) → ( 2 ↑ ( 𝑁 + 2 ) ) ∈ ℂ )
116 87 115 mulcld ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℕ ) → ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) ∈ ℂ )
117 106 107 116 subadd2d ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑃 − 1 ) = ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) ↔ ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) = 𝑃 ) )
118 eqcom ⊢ ( ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) = 𝑃 ↔ 𝑃 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) )
119 118 a1i ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℕ ) → ( ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) = 𝑃 ↔ 𝑃 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) )
120 104 117 119 3bitrd ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑃 − 1 ) = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 1 ) ) ) · 2 ) ↔ 𝑃 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) )
121 72 85 120 3bitrd ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 1 ) ) ) = ( ( 𝑃 − 1 ) / 2 ) ↔ 𝑃 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) )
122 121 rexbidva ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ) → ( ∃ 𝑘 ∈ ℕ ( 𝑘 · ( 2 ↑ ( 𝑁 + 1 ) ) ) = ( ( 𝑃 − 1 ) / 2 ) ↔ ∃ 𝑘 ∈ ℕ 𝑃 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) )
123 122 biimpd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ) → ( ∃ 𝑘 ∈ ℕ ( 𝑘 · ( 2 ↑ ( 𝑁 + 1 ) ) ) = ( ( 𝑃 − 1 ) / 2 ) → ∃ 𝑘 ∈ ℕ 𝑃 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) )
124 123 adantrr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2 ) ) → ( ∃ 𝑘 ∈ ℕ ( 𝑘 · ( 2 ↑ ( 𝑁 + 1 ) ) ) = ( ( 𝑃 − 1 ) / 2 ) → ∃ 𝑘 ∈ ℕ 𝑃 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) )
125 70 124 sylbid ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2 ) ) → ( ( 2 ↑ ( 𝑁 + 1 ) ) ∥ ( ( 𝑃 − 1 ) / 2 ) → ∃ 𝑘 ∈ ℕ 𝑃 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) )
126 125 expr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ) → ( ¬ 𝑃 = 2 → ( ( 2 ↑ ( 𝑁 + 1 ) ) ∥ ( ( 𝑃 − 1 ) / 2 ) → ∃ 𝑘 ∈ ℕ 𝑃 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) ) )
127 126 3adant3 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) → ( ¬ 𝑃 = 2 → ( ( 2 ↑ ( 𝑁 + 1 ) ) ∥ ( ( 𝑃 − 1 ) / 2 ) → ∃ 𝑘 ∈ ℕ 𝑃 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) ) )
128 127 impcom ⊢ ( ( ¬ 𝑃 = 2 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) ) → ( ( 2 ↑ ( 𝑁 + 1 ) ) ∥ ( ( 𝑃 − 1 ) / 2 ) → ∃ 𝑘 ∈ ℕ 𝑃 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) )
129 128 adantr ⊢ ( ( ( ¬ 𝑃 = 2 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) ) ∧ ( ( odℤ ‘ 𝑃 ) ‘ 2 ) = ( 2 ↑ ( 𝑁 + 1 ) ) ) → ( ( 2 ↑ ( 𝑁 + 1 ) ) ∥ ( ( 𝑃 − 1 ) / 2 ) → ∃ 𝑘 ∈ ℕ 𝑃 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) )
130 63 129 sylbid ⊢ ( ( ( ¬ 𝑃 = 2 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) ) ∧ ( ( odℤ ‘ 𝑃 ) ‘ 2 ) = ( 2 ↑ ( 𝑁 + 1 ) ) ) → ( ( ( odℤ ‘ 𝑃 ) ‘ 2 ) ∥ ( ( 𝑃 − 1 ) / 2 ) → ∃ 𝑘 ∈ ℕ 𝑃 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) )
131 130 ex ⊢ ( ( ¬ 𝑃 = 2 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) ) → ( ( ( odℤ ‘ 𝑃 ) ‘ 2 ) = ( 2 ↑ ( 𝑁 + 1 ) ) → ( ( ( odℤ ‘ 𝑃 ) ‘ 2 ) ∥ ( ( 𝑃 − 1 ) / 2 ) → ∃ 𝑘 ∈ ℕ 𝑃 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) ) )
132 61 131 mpd ⊢ ( ( ¬ 𝑃 = 2 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) ) → ( ( ( odℤ ‘ 𝑃 ) ‘ 2 ) ∥ ( ( 𝑃 − 1 ) / 2 ) → ∃ 𝑘 ∈ ℕ 𝑃 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) )
133 56 132 sylbid ⊢ ( ( ¬ 𝑃 = 2 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) ) → ( 𝑃 ∥ ( ( 2 ↑ ( ( 𝑃 − 1 ) / 2 ) ) − 1 ) → ∃ 𝑘 ∈ ℕ 𝑃 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) )
134 36 133 sylbid ⊢ ( ( ¬ 𝑃 = 2 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) ) → ( ( ( 2 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = 1 → ∃ 𝑘 ∈ ℕ 𝑃 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) )
135 22 134 mpd ⊢ ( ( ¬ 𝑃 = 2 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) ) → ∃ 𝑘 ∈ ℕ 𝑃 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) )
136 135 ex ⊢ ( ¬ 𝑃 = 2 → ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) → ∃ 𝑘 ∈ ℕ 𝑃 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) ) )
137 11 136 pm2.61i ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) → ∃ 𝑘 ∈ ℕ 𝑃 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) )