Metamath Proof Explorer

Theorem fmtnoprmfac1lem

Description: Lemma for fmtnoprmfac1 : The order of 2 modulo a prime that divides the n-th Fermat number is 2^(n+1). (Contributed by AV, 25-Jul-2021) (Proof shortened by AV, 18-Mar-2022)

Ref Expression
Assertion fmtnoprmfac1lem ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) → ( ( odℤ ‘ 𝑃 ) ‘ 2 ) = ( 2 ↑ ( 𝑁 + 1 ) ) )

Proof

Step Hyp Ref Expression
1 eldifi ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 𝑃 ∈ ℙ )
2 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
3 1 2 syl ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 𝑃 ∈ ℕ )
4 3 ad2antlr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) → 𝑃 ∈ ℕ )
5 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
6 fmtno ⊢ ( 𝑁 ∈ ℕ0 → ( FermatNo ‘ 𝑁 ) = ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) )
7 5 6 syl ⊢ ( 𝑁 ∈ ℕ → ( FermatNo ‘ 𝑁 ) = ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) )
8 7 breq2d ⊢ ( 𝑁 ∈ ℕ → ( 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ↔ 𝑃 ∥ ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) ) )
9 8 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ↔ 𝑃 ∥ ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) ) )
10 9 biimpa ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) → 𝑃 ∥ ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) )
11 dvdsmod0 ⊢ ( ( 𝑃 ∈ ℕ ∧ 𝑃 ∥ ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) ) → ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) mod 𝑃 ) = 0 )
12 4 10 11 syl2anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) → ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) mod 𝑃 ) = 0 )
13 12 ex ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( 𝑃 ∥ ( FermatNo ‘ 𝑁 ) → ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) mod 𝑃 ) = 0 ) )
14 2nn ⊢ 2 ∈ ℕ
15 14 a1i ⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℕ )
16 2nn0 ⊢ 2 ∈ ℕ0
17 16 a1i ⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℕ0 )
18 17 5 nn0expcld ⊢ ( 𝑁 ∈ ℕ → ( 2 ↑ 𝑁 ) ∈ ℕ0 )
19 15 18 nnexpcld ⊢ ( 𝑁 ∈ ℕ → ( 2 ↑ ( 2 ↑ 𝑁 ) ) ∈ ℕ )
20 19 nnzd ⊢ ( 𝑁 ∈ ℕ → ( 2 ↑ ( 2 ↑ 𝑁 ) ) ∈ ℤ )
21 20 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( 2 ↑ ( 2 ↑ 𝑁 ) ) ∈ ℤ )
22 1zzd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → 1 ∈ ℤ )
23 3 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → 𝑃 ∈ ℕ )
24 summodnegmod ⊢ ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) ∈ ℤ ∧ 1 ∈ ℤ ∧ 𝑃 ∈ ℕ ) → ( ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) mod 𝑃 ) = 0 ↔ ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) )
25 21 22 23 24 syl3anc ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) mod 𝑃 ) = 0 ↔ ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) )
26 neg1z ⊢ - 1 ∈ ℤ
27 21 26 jctir ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) ∈ ℤ ∧ - 1 ∈ ℤ ) )
28 27 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) → ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) ∈ ℤ ∧ - 1 ∈ ℤ ) )
29 2 nnrpd ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℝ+ )
30 1 29 syl ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 𝑃 ∈ ℝ+ )
31 17 30 anim12i ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( 2 ∈ ℕ0 ∧ 𝑃 ∈ ℝ+ ) )
32 31 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) → ( 2 ∈ ℕ0 ∧ 𝑃 ∈ ℝ+ ) )
33 simpr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) → ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) )
34 modexp ⊢ ( ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) ∈ ℤ ∧ - 1 ∈ ℤ ) ∧ ( 2 ∈ ℕ0 ∧ 𝑃 ∈ ℝ+ ) ∧ ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) → ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) ↑ 2 ) mod 𝑃 ) = ( ( - 1 ↑ 2 ) mod 𝑃 ) )
35 28 32 33 34 syl3anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) → ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) ↑ 2 ) mod 𝑃 ) = ( ( - 1 ↑ 2 ) mod 𝑃 ) )
36 35 ex ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) → ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) ↑ 2 ) mod 𝑃 ) = ( ( - 1 ↑ 2 ) mod 𝑃 ) ) )
37 2cnd ⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℂ )
38 37 18 17 3jca ⊢ ( 𝑁 ∈ ℕ → ( 2 ∈ ℂ ∧ ( 2 ↑ 𝑁 ) ∈ ℕ0 ∧ 2 ∈ ℕ0 ) )
39 38 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( 2 ∈ ℂ ∧ ( 2 ↑ 𝑁 ) ∈ ℕ0 ∧ 2 ∈ ℕ0 ) )
40 expmul ⊢ ( ( 2 ∈ ℂ ∧ ( 2 ↑ 𝑁 ) ∈ ℕ0 ∧ 2 ∈ ℕ0 ) → ( 2 ↑ ( ( 2 ↑ 𝑁 ) · 2 ) ) = ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) ↑ 2 ) )
41 39 40 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( 2 ↑ ( ( 2 ↑ 𝑁 ) · 2 ) ) = ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) ↑ 2 ) )
42 2cnd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → 2 ∈ ℂ )
43 5 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → 𝑁 ∈ ℕ0 )
44 42 43 expp1d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( 2 ↑ ( 𝑁 + 1 ) ) = ( ( 2 ↑ 𝑁 ) · 2 ) )
45 44 eqcomd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( 2 ↑ 𝑁 ) · 2 ) = ( 2 ↑ ( 𝑁 + 1 ) ) )
46 45 oveq2d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( 2 ↑ ( ( 2 ↑ 𝑁 ) · 2 ) ) = ( 2 ↑ ( 2 ↑ ( 𝑁 + 1 ) ) ) )
47 41 46 eqtr3d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) ↑ 2 ) = ( 2 ↑ ( 2 ↑ ( 𝑁 + 1 ) ) ) )
48 47 oveq1d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) ↑ 2 ) mod 𝑃 ) = ( ( 2 ↑ ( 2 ↑ ( 𝑁 + 1 ) ) ) mod 𝑃 ) )
49 neg1sqe1 ⊢ ( - 1 ↑ 2 ) = 1
50 49 a1i ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( - 1 ↑ 2 ) = 1 )
51 50 oveq1d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( - 1 ↑ 2 ) mod 𝑃 ) = ( 1 mod 𝑃 ) )
52 3 nnred ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 𝑃 ∈ ℝ )
53 prmgt1 ⊢ ( 𝑃 ∈ ℙ → 1 < 𝑃 )
54 1 53 syl ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 1 < 𝑃 )
55 1mod ⊢ ( ( 𝑃 ∈ ℝ ∧ 1 < 𝑃 ) → ( 1 mod 𝑃 ) = 1 )
56 52 54 55 syl2anc ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( 1 mod 𝑃 ) = 1 )
57 56 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( 1 mod 𝑃 ) = 1 )
58 51 57 eqtrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( - 1 ↑ 2 ) mod 𝑃 ) = 1 )
59 48 58 eqeq12d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) ↑ 2 ) mod 𝑃 ) = ( ( - 1 ↑ 2 ) mod 𝑃 ) ↔ ( ( 2 ↑ ( 2 ↑ ( 𝑁 + 1 ) ) ) mod 𝑃 ) = 1 ) )
60 simpll ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ( ( 2 ↑ ( 2 ↑ ( 𝑁 + 1 ) ) ) mod 𝑃 ) = 1 ) ∧ ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) mod 𝑃 ) = 0 ) → ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) )
61 20 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ) → ( 2 ↑ ( 2 ↑ 𝑁 ) ) ∈ ℤ )
62 1zzd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ) → 1 ∈ ℤ )
63 2 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ) → 𝑃 ∈ ℕ )
64 61 62 63 3jca ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ) → ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) ∈ ℤ ∧ 1 ∈ ℤ ∧ 𝑃 ∈ ℕ ) )
65 1 64 sylan2 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) ∈ ℤ ∧ 1 ∈ ℤ ∧ 𝑃 ∈ ℕ ) )
66 65 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ( ( 2 ↑ ( 2 ↑ ( 𝑁 + 1 ) ) ) mod 𝑃 ) = 1 ) → ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) ∈ ℤ ∧ 1 ∈ ℤ ∧ 𝑃 ∈ ℕ ) )
67 66 24 syl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ( ( 2 ↑ ( 2 ↑ ( 𝑁 + 1 ) ) ) mod 𝑃 ) = 1 ) → ( ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) mod 𝑃 ) = 0 ↔ ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) )
68 m1modnnsub1 ⊢ ( 𝑃 ∈ ℕ → ( - 1 mod 𝑃 ) = ( 𝑃 − 1 ) )
69 23 68 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( - 1 mod 𝑃 ) = ( 𝑃 − 1 ) )
70 eldifsni ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 𝑃 ≠ 2 )
71 70 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → 𝑃 ≠ 2 )
72 71 necomd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → 2 ≠ 𝑃 )
73 3 nncnd ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 𝑃 ∈ ℂ )
74 73 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → 𝑃 ∈ ℂ )
75 1cnd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → 1 ∈ ℂ )
76 74 75 75 subadd2d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( 𝑃 − 1 ) = 1 ↔ ( 1 + 1 ) = 𝑃 ) )
77 1p1e2 ⊢ ( 1 + 1 ) = 2
78 77 eqeq1i ⊢ ( ( 1 + 1 ) = 𝑃 ↔ 2 = 𝑃 )
79 76 78 bitrdi ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( 𝑃 − 1 ) = 1 ↔ 2 = 𝑃 ) )
80 79 necon3bid ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( 𝑃 − 1 ) ≠ 1 ↔ 2 ≠ 𝑃 ) )
81 72 80 mpbird ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( 𝑃 − 1 ) ≠ 1 )
82 69 81 eqnetrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( - 1 mod 𝑃 ) ≠ 1 )
83 82 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ( ( 2 ↑ ( 2 ↑ ( 𝑁 + 1 ) ) ) mod 𝑃 ) = 1 ) → ( - 1 mod 𝑃 ) ≠ 1 )
84 83 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ( ( 2 ↑ ( 2 ↑ ( 𝑁 + 1 ) ) ) mod 𝑃 ) = 1 ) ∧ ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) → ( - 1 mod 𝑃 ) ≠ 1 )
85 eqeq1 ⊢ ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) → ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) mod 𝑃 ) = 1 ↔ ( - 1 mod 𝑃 ) = 1 ) )
86 85 adantl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ( ( 2 ↑ ( 2 ↑ ( 𝑁 + 1 ) ) ) mod 𝑃 ) = 1 ) ∧ ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) → ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) mod 𝑃 ) = 1 ↔ ( - 1 mod 𝑃 ) = 1 ) )
87 86 necon3bid ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ( ( 2 ↑ ( 2 ↑ ( 𝑁 + 1 ) ) ) mod 𝑃 ) = 1 ) ∧ ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) → ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) mod 𝑃 ) ≠ 1 ↔ ( - 1 mod 𝑃 ) ≠ 1 ) )
88 84 87 mpbird ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ( ( 2 ↑ ( 2 ↑ ( 𝑁 + 1 ) ) ) mod 𝑃 ) = 1 ) ∧ ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) → ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) mod 𝑃 ) ≠ 1 )
89 88 ex ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ( ( 2 ↑ ( 2 ↑ ( 𝑁 + 1 ) ) ) mod 𝑃 ) = 1 ) → ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) → ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) mod 𝑃 ) ≠ 1 ) )
90 67 89 sylbid ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ( ( 2 ↑ ( 2 ↑ ( 𝑁 + 1 ) ) ) mod 𝑃 ) = 1 ) → ( ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) mod 𝑃 ) = 0 → ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) mod 𝑃 ) ≠ 1 ) )
91 90 imp ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ( ( 2 ↑ ( 2 ↑ ( 𝑁 + 1 ) ) ) mod 𝑃 ) = 1 ) ∧ ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) mod 𝑃 ) = 0 ) → ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) mod 𝑃 ) ≠ 1 )
92 simplr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ( ( 2 ↑ ( 2 ↑ ( 𝑁 + 1 ) ) ) mod 𝑃 ) = 1 ) ∧ ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) mod 𝑃 ) = 0 ) → ( ( 2 ↑ ( 2 ↑ ( 𝑁 + 1 ) ) ) mod 𝑃 ) = 1 )
93 odz2prm2pw ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) mod 𝑃 ) ≠ 1 ∧ ( ( 2 ↑ ( 2 ↑ ( 𝑁 + 1 ) ) ) mod 𝑃 ) = 1 ) ) → ( ( odℤ ‘ 𝑃 ) ‘ 2 ) = ( 2 ↑ ( 𝑁 + 1 ) ) )
94 60 91 92 93 syl12anc ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ( ( 2 ↑ ( 2 ↑ ( 𝑁 + 1 ) ) ) mod 𝑃 ) = 1 ) ∧ ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) mod 𝑃 ) = 0 ) → ( ( odℤ ‘ 𝑃 ) ‘ 2 ) = ( 2 ↑ ( 𝑁 + 1 ) ) )
95 94 ex ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ( ( 2 ↑ ( 2 ↑ ( 𝑁 + 1 ) ) ) mod 𝑃 ) = 1 ) → ( ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) mod 𝑃 ) = 0 → ( ( odℤ ‘ 𝑃 ) ‘ 2 ) = ( 2 ↑ ( 𝑁 + 1 ) ) ) )
96 95 ex ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( ( 2 ↑ ( 2 ↑ ( 𝑁 + 1 ) ) ) mod 𝑃 ) = 1 → ( ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) mod 𝑃 ) = 0 → ( ( odℤ ‘ 𝑃 ) ‘ 2 ) = ( 2 ↑ ( 𝑁 + 1 ) ) ) ) )
97 59 96 sylbid ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) ↑ 2 ) mod 𝑃 ) = ( ( - 1 ↑ 2 ) mod 𝑃 ) → ( ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) mod 𝑃 ) = 0 → ( ( odℤ ‘ 𝑃 ) ‘ 2 ) = ( 2 ↑ ( 𝑁 + 1 ) ) ) ) )
98 36 97 syld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) → ( ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) mod 𝑃 ) = 0 → ( ( odℤ ‘ 𝑃 ) ‘ 2 ) = ( 2 ↑ ( 𝑁 + 1 ) ) ) ) )
99 25 98 sylbid ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) mod 𝑃 ) = 0 → ( ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) mod 𝑃 ) = 0 → ( ( odℤ ‘ 𝑃 ) ‘ 2 ) = ( 2 ↑ ( 𝑁 + 1 ) ) ) ) )
100 99 pm2.43d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) mod 𝑃 ) = 0 → ( ( odℤ ‘ 𝑃 ) ‘ 2 ) = ( 2 ↑ ( 𝑁 + 1 ) ) ) )
101 13 100 syld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( 𝑃 ∥ ( FermatNo ‘ 𝑁 ) → ( ( odℤ ‘ 𝑃 ) ‘ 2 ) = ( 2 ↑ ( 𝑁 + 1 ) ) ) )
102 101 3impia ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) → ( ( odℤ ‘ 𝑃 ) ‘ 2 ) = ( 2 ↑ ( 𝑁 + 1 ) ) )