Metamath Proof Explorer

Theorem odz2prm2pw

Description: Any power of two is coprime to any prime not being two. (Contributed by AV, 25-Jul-2021)

Ref Expression
Assertion odz2prm2pw ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) mod 𝑃 ) ≠ 1 ∧ ( ( 2 ↑ ( 2 ↑ ( 𝑁 + 1 ) ) ) mod 𝑃 ) = 1 ) ) → ( ( odℤ ‘ 𝑃 ) ‘ 2 ) = ( 2 ↑ ( 𝑁 + 1 ) ) )

Proof

Step Hyp Ref Expression
1 eldifi ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 𝑃 ∈ ℙ )
2 2nn ⊢ 2 ∈ ℕ
3 2 a1i ⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℕ )
4 2nn0 ⊢ 2 ∈ ℕ0
5 4 a1i ⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℕ0 )
6 peano2nn ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + 1 ) ∈ ℕ )
7 6 nnnn0d ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + 1 ) ∈ ℕ0 )
8 5 7 nn0expcld ⊢ ( 𝑁 ∈ ℕ → ( 2 ↑ ( 𝑁 + 1 ) ) ∈ ℕ0 )
9 3 8 nnexpcld ⊢ ( 𝑁 ∈ ℕ → ( 2 ↑ ( 2 ↑ ( 𝑁 + 1 ) ) ) ∈ ℕ )
10 9 nnzd ⊢ ( 𝑁 ∈ ℕ → ( 2 ↑ ( 2 ↑ ( 𝑁 + 1 ) ) ) ∈ ℤ )
11 modprm1div ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 2 ↑ ( 2 ↑ ( 𝑁 + 1 ) ) ) ∈ ℤ ) → ( ( ( 2 ↑ ( 2 ↑ ( 𝑁 + 1 ) ) ) mod 𝑃 ) = 1 ↔ 𝑃 ∥ ( ( 2 ↑ ( 2 ↑ ( 𝑁 + 1 ) ) ) − 1 ) ) )
12 1 10 11 syl2anr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( ( 2 ↑ ( 2 ↑ ( 𝑁 + 1 ) ) ) mod 𝑃 ) = 1 ↔ 𝑃 ∥ ( ( 2 ↑ ( 2 ↑ ( 𝑁 + 1 ) ) ) − 1 ) ) )
13 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
14 1 13 syl ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 𝑃 ∈ ℕ )
15 14 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → 𝑃 ∈ ℕ )
16 2z ⊢ 2 ∈ ℤ
17 16 a1i ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → 2 ∈ ℤ )
18 eldifsn ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ↔ ( 𝑃 ∈ ℙ ∧ 𝑃 ≠ 2 ) )
19 simpr ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑃 ≠ 2 ) → 𝑃 ≠ 2 )
20 19 necomd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑃 ≠ 2 ) → 2 ≠ 𝑃 )
21 18 20 sylbi ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 2 ≠ 𝑃 )
22 2prm ⊢ 2 ∈ ℙ
23 prmrp ⊢ ( ( 2 ∈ ℙ ∧ 𝑃 ∈ ℙ ) → ( ( 2 gcd 𝑃 ) = 1 ↔ 2 ≠ 𝑃 ) )
24 22 1 23 sylancr ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( ( 2 gcd 𝑃 ) = 1 ↔ 2 ≠ 𝑃 ) )
25 21 24 mpbird ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( 2 gcd 𝑃 ) = 1 )
26 25 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( 2 gcd 𝑃 ) = 1 )
27 15 17 26 3jca ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( 𝑃 ∈ ℕ ∧ 2 ∈ ℤ ∧ ( 2 gcd 𝑃 ) = 1 ) )
28 8 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( 2 ↑ ( 𝑁 + 1 ) ) ∈ ℕ0 )
29 odzdvds ⊢ ( ( ( 𝑃 ∈ ℕ ∧ 2 ∈ ℤ ∧ ( 2 gcd 𝑃 ) = 1 ) ∧ ( 2 ↑ ( 𝑁 + 1 ) ) ∈ ℕ0 ) → ( 𝑃 ∥ ( ( 2 ↑ ( 2 ↑ ( 𝑁 + 1 ) ) ) − 1 ) ↔ ( ( odℤ ‘ 𝑃 ) ‘ 2 ) ∥ ( 2 ↑ ( 𝑁 + 1 ) ) ) )
30 27 28 29 syl2anc ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( 𝑃 ∥ ( ( 2 ↑ ( 2 ↑ ( 𝑁 + 1 ) ) ) − 1 ) ↔ ( ( odℤ ‘ 𝑃 ) ‘ 2 ) ∥ ( 2 ↑ ( 𝑁 + 1 ) ) ) )
31 12 30 bitrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( ( 2 ↑ ( 2 ↑ ( 𝑁 + 1 ) ) ) mod 𝑃 ) = 1 ↔ ( ( odℤ ‘ 𝑃 ) ‘ 2 ) ∥ ( 2 ↑ ( 𝑁 + 1 ) ) ) )
32 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
33 5 32 nn0expcld ⊢ ( 𝑁 ∈ ℕ → ( 2 ↑ 𝑁 ) ∈ ℕ0 )
34 3 33 nnexpcld ⊢ ( 𝑁 ∈ ℕ → ( 2 ↑ ( 2 ↑ 𝑁 ) ) ∈ ℕ )
35 34 nnzd ⊢ ( 𝑁 ∈ ℕ → ( 2 ↑ ( 2 ↑ 𝑁 ) ) ∈ ℤ )
36 modprm1div ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 2 ↑ ( 2 ↑ 𝑁 ) ) ∈ ℤ ) → ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) mod 𝑃 ) = 1 ↔ 𝑃 ∥ ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) − 1 ) ) )
37 1 35 36 syl2anr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) mod 𝑃 ) = 1 ↔ 𝑃 ∥ ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) − 1 ) ) )
38 33 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( 2 ↑ 𝑁 ) ∈ ℕ0 )
39 odzdvds ⊢ ( ( ( 𝑃 ∈ ℕ ∧ 2 ∈ ℤ ∧ ( 2 gcd 𝑃 ) = 1 ) ∧ ( 2 ↑ 𝑁 ) ∈ ℕ0 ) → ( 𝑃 ∥ ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) − 1 ) ↔ ( ( odℤ ‘ 𝑃 ) ‘ 2 ) ∥ ( 2 ↑ 𝑁 ) ) )
40 27 38 39 syl2anc ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( 𝑃 ∥ ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) − 1 ) ↔ ( ( odℤ ‘ 𝑃 ) ‘ 2 ) ∥ ( 2 ↑ 𝑁 ) ) )
41 37 40 bitrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) mod 𝑃 ) = 1 ↔ ( ( odℤ ‘ 𝑃 ) ‘ 2 ) ∥ ( 2 ↑ 𝑁 ) ) )
42 41 necon3abid ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) mod 𝑃 ) ≠ 1 ↔ ¬ ( ( odℤ ‘ 𝑃 ) ‘ 2 ) ∥ ( 2 ↑ 𝑁 ) ) )
43 odzcl ⊢ ( ( 𝑃 ∈ ℕ ∧ 2 ∈ ℤ ∧ ( 2 gcd 𝑃 ) = 1 ) → ( ( odℤ ‘ 𝑃 ) ‘ 2 ) ∈ ℕ )
44 27 43 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( odℤ ‘ 𝑃 ) ‘ 2 ) ∈ ℕ )
45 7 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( 𝑁 + 1 ) ∈ ℕ0 )
46 dvdsprmpweqle ⊢ ( ( 2 ∈ ℙ ∧ ( ( odℤ ‘ 𝑃 ) ‘ 2 ) ∈ ℕ ∧ ( 𝑁 + 1 ) ∈ ℕ0 ) → ( ( ( odℤ ‘ 𝑃 ) ‘ 2 ) ∥ ( 2 ↑ ( 𝑁 + 1 ) ) → ∃ 𝑛 ∈ ℕ0 ( 𝑛 ≤ ( 𝑁 + 1 ) ∧ ( ( odℤ ‘ 𝑃 ) ‘ 2 ) = ( 2 ↑ 𝑛 ) ) ) )
47 22 44 45 46 mp3an2i ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( ( odℤ ‘ 𝑃 ) ‘ 2 ) ∥ ( 2 ↑ ( 𝑁 + 1 ) ) → ∃ 𝑛 ∈ ℕ0 ( 𝑛 ≤ ( 𝑁 + 1 ) ∧ ( ( odℤ ‘ 𝑃 ) ‘ 2 ) = ( 2 ↑ 𝑛 ) ) ) )
48 breq1 ⊢ ( ( ( odℤ ‘ 𝑃 ) ‘ 2 ) = ( 2 ↑ 𝑛 ) → ( ( ( odℤ ‘ 𝑃 ) ‘ 2 ) ∥ ( 2 ↑ 𝑁 ) ↔ ( 2 ↑ 𝑛 ) ∥ ( 2 ↑ 𝑁 ) ) )
49 48 adantl ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 ≤ ( 𝑁 + 1 ) ) ∧ ( ( odℤ ‘ 𝑃 ) ‘ 2 ) = ( 2 ↑ 𝑛 ) ) → ( ( ( odℤ ‘ 𝑃 ) ‘ 2 ) ∥ ( 2 ↑ 𝑁 ) ↔ ( 2 ↑ 𝑛 ) ∥ ( 2 ↑ 𝑁 ) ) )
50 49 notbid ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 ≤ ( 𝑁 + 1 ) ) ∧ ( ( odℤ ‘ 𝑃 ) ‘ 2 ) = ( 2 ↑ 𝑛 ) ) → ( ¬ ( ( odℤ ‘ 𝑃 ) ‘ 2 ) ∥ ( 2 ↑ 𝑁 ) ↔ ¬ ( 2 ↑ 𝑛 ) ∥ ( 2 ↑ 𝑁 ) ) )
51 simpr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 ≤ ( 𝑁 + 1 ) ) ∧ ( ( odℤ ‘ 𝑃 ) ‘ 2 ) = ( 2 ↑ 𝑛 ) ) → ( ( odℤ ‘ 𝑃 ) ‘ 2 ) = ( 2 ↑ 𝑛 ) )
52 51 adantr ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 ≤ ( 𝑁 + 1 ) ) ∧ ( ( odℤ ‘ 𝑃 ) ‘ 2 ) = ( 2 ↑ 𝑛 ) ) ∧ ¬ ( 2 ↑ 𝑛 ) ∥ ( 2 ↑ 𝑁 ) ) → ( ( odℤ ‘ 𝑃 ) ‘ 2 ) = ( 2 ↑ 𝑛 ) )
53 nn0re ⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℝ )
54 6 nnred ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + 1 ) ∈ ℝ )
55 54 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( 𝑁 + 1 ) ∈ ℝ )
56 leloe ⊢ ( ( 𝑛 ∈ ℝ ∧ ( 𝑁 + 1 ) ∈ ℝ ) → ( 𝑛 ≤ ( 𝑁 + 1 ) ↔ ( 𝑛 < ( 𝑁 + 1 ) ∨ 𝑛 = ( 𝑁 + 1 ) ) ) )
57 53 55 56 syl2anr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 ≤ ( 𝑁 + 1 ) ↔ ( 𝑛 < ( 𝑁 + 1 ) ∨ 𝑛 = ( 𝑁 + 1 ) ) ) )
58 simpr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℕ0 )
59 nn0z ⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℤ )
60 59 adantl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℤ )
61 60 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 < ( 𝑁 + 1 ) ) → 𝑛 ∈ ℤ )
62 nnz ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
63 62 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → 𝑁 ∈ ℤ )
64 63 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ 𝑛 ∈ ℕ0 ) → 𝑁 ∈ ℤ )
65 64 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 < ( 𝑁 + 1 ) ) → 𝑁 ∈ ℤ )
66 zleltp1 ⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑛 ≤ 𝑁 ↔ 𝑛 < ( 𝑁 + 1 ) ) )
67 59 63 66 syl2anr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 ≤ 𝑁 ↔ 𝑛 < ( 𝑁 + 1 ) ) )
68 67 biimpar ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 < ( 𝑁 + 1 ) ) → 𝑛 ≤ 𝑁 )
69 eluz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑛 ) ↔ ( 𝑛 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑛 ≤ 𝑁 ) )
70 61 65 68 69 syl3anbrc ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 < ( 𝑁 + 1 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑛 ) )
71 dvdsexp ⊢ ( ( 2 ∈ ℤ ∧ 𝑛 ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( 2 ↑ 𝑛 ) ∥ ( 2 ↑ 𝑁 ) )
72 16 58 70 71 mp3an2ani ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 < ( 𝑁 + 1 ) ) → ( 2 ↑ 𝑛 ) ∥ ( 2 ↑ 𝑁 ) )
73 72 pm2.24d ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 < ( 𝑁 + 1 ) ) → ( ¬ ( 2 ↑ 𝑛 ) ∥ ( 2 ↑ 𝑁 ) → ( 2 ↑ 𝑛 ) = ( 2 ↑ ( 𝑁 + 1 ) ) ) )
74 73 expcom ⊢ ( 𝑛 < ( 𝑁 + 1 ) → ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ¬ ( 2 ↑ 𝑛 ) ∥ ( 2 ↑ 𝑁 ) → ( 2 ↑ 𝑛 ) = ( 2 ↑ ( 𝑁 + 1 ) ) ) ) )
75 oveq2 ⊢ ( 𝑛 = ( 𝑁 + 1 ) → ( 2 ↑ 𝑛 ) = ( 2 ↑ ( 𝑁 + 1 ) ) )
76 75 2a1d ⊢ ( 𝑛 = ( 𝑁 + 1 ) → ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ¬ ( 2 ↑ 𝑛 ) ∥ ( 2 ↑ 𝑁 ) → ( 2 ↑ 𝑛 ) = ( 2 ↑ ( 𝑁 + 1 ) ) ) ) )
77 74 76 jaoi ⊢ ( ( 𝑛 < ( 𝑁 + 1 ) ∨ 𝑛 = ( 𝑁 + 1 ) ) → ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ¬ ( 2 ↑ 𝑛 ) ∥ ( 2 ↑ 𝑁 ) → ( 2 ↑ 𝑛 ) = ( 2 ↑ ( 𝑁 + 1 ) ) ) ) )
78 77 com12 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑛 < ( 𝑁 + 1 ) ∨ 𝑛 = ( 𝑁 + 1 ) ) → ( ¬ ( 2 ↑ 𝑛 ) ∥ ( 2 ↑ 𝑁 ) → ( 2 ↑ 𝑛 ) = ( 2 ↑ ( 𝑁 + 1 ) ) ) ) )
79 57 78 sylbid ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 ≤ ( 𝑁 + 1 ) → ( ¬ ( 2 ↑ 𝑛 ) ∥ ( 2 ↑ 𝑁 ) → ( 2 ↑ 𝑛 ) = ( 2 ↑ ( 𝑁 + 1 ) ) ) ) )
80 79 imp ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 ≤ ( 𝑁 + 1 ) ) → ( ¬ ( 2 ↑ 𝑛 ) ∥ ( 2 ↑ 𝑁 ) → ( 2 ↑ 𝑛 ) = ( 2 ↑ ( 𝑁 + 1 ) ) ) )
81 80 adantr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 ≤ ( 𝑁 + 1 ) ) ∧ ( ( odℤ ‘ 𝑃 ) ‘ 2 ) = ( 2 ↑ 𝑛 ) ) → ( ¬ ( 2 ↑ 𝑛 ) ∥ ( 2 ↑ 𝑁 ) → ( 2 ↑ 𝑛 ) = ( 2 ↑ ( 𝑁 + 1 ) ) ) )
82 81 imp ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 ≤ ( 𝑁 + 1 ) ) ∧ ( ( odℤ ‘ 𝑃 ) ‘ 2 ) = ( 2 ↑ 𝑛 ) ) ∧ ¬ ( 2 ↑ 𝑛 ) ∥ ( 2 ↑ 𝑁 ) ) → ( 2 ↑ 𝑛 ) = ( 2 ↑ ( 𝑁 + 1 ) ) )
83 52 82 eqtrd ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 ≤ ( 𝑁 + 1 ) ) ∧ ( ( odℤ ‘ 𝑃 ) ‘ 2 ) = ( 2 ↑ 𝑛 ) ) ∧ ¬ ( 2 ↑ 𝑛 ) ∥ ( 2 ↑ 𝑁 ) ) → ( ( odℤ ‘ 𝑃 ) ‘ 2 ) = ( 2 ↑ ( 𝑁 + 1 ) ) )
84 83 ex ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 ≤ ( 𝑁 + 1 ) ) ∧ ( ( odℤ ‘ 𝑃 ) ‘ 2 ) = ( 2 ↑ 𝑛 ) ) → ( ¬ ( 2 ↑ 𝑛 ) ∥ ( 2 ↑ 𝑁 ) → ( ( odℤ ‘ 𝑃 ) ‘ 2 ) = ( 2 ↑ ( 𝑁 + 1 ) ) ) )
85 50 84 sylbid ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 ≤ ( 𝑁 + 1 ) ) ∧ ( ( odℤ ‘ 𝑃 ) ‘ 2 ) = ( 2 ↑ 𝑛 ) ) → ( ¬ ( ( odℤ ‘ 𝑃 ) ‘ 2 ) ∥ ( 2 ↑ 𝑁 ) → ( ( odℤ ‘ 𝑃 ) ‘ 2 ) = ( 2 ↑ ( 𝑁 + 1 ) ) ) )
86 85 expl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑛 ≤ ( 𝑁 + 1 ) ∧ ( ( odℤ ‘ 𝑃 ) ‘ 2 ) = ( 2 ↑ 𝑛 ) ) → ( ¬ ( ( odℤ ‘ 𝑃 ) ‘ 2 ) ∥ ( 2 ↑ 𝑁 ) → ( ( odℤ ‘ 𝑃 ) ‘ 2 ) = ( 2 ↑ ( 𝑁 + 1 ) ) ) ) )
87 86 rexlimdva ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ∃ 𝑛 ∈ ℕ0 ( 𝑛 ≤ ( 𝑁 + 1 ) ∧ ( ( odℤ ‘ 𝑃 ) ‘ 2 ) = ( 2 ↑ 𝑛 ) ) → ( ¬ ( ( odℤ ‘ 𝑃 ) ‘ 2 ) ∥ ( 2 ↑ 𝑁 ) → ( ( odℤ ‘ 𝑃 ) ‘ 2 ) = ( 2 ↑ ( 𝑁 + 1 ) ) ) ) )
88 47 87 syld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( ( odℤ ‘ 𝑃 ) ‘ 2 ) ∥ ( 2 ↑ ( 𝑁 + 1 ) ) → ( ¬ ( ( odℤ ‘ 𝑃 ) ‘ 2 ) ∥ ( 2 ↑ 𝑁 ) → ( ( odℤ ‘ 𝑃 ) ‘ 2 ) = ( 2 ↑ ( 𝑁 + 1 ) ) ) ) )
89 88 com23 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ¬ ( ( odℤ ‘ 𝑃 ) ‘ 2 ) ∥ ( 2 ↑ 𝑁 ) → ( ( ( odℤ ‘ 𝑃 ) ‘ 2 ) ∥ ( 2 ↑ ( 𝑁 + 1 ) ) → ( ( odℤ ‘ 𝑃 ) ‘ 2 ) = ( 2 ↑ ( 𝑁 + 1 ) ) ) ) )
90 42 89 sylbid ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) mod 𝑃 ) ≠ 1 → ( ( ( odℤ ‘ 𝑃 ) ‘ 2 ) ∥ ( 2 ↑ ( 𝑁 + 1 ) ) → ( ( odℤ ‘ 𝑃 ) ‘ 2 ) = ( 2 ↑ ( 𝑁 + 1 ) ) ) ) )
91 90 com23 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( ( odℤ ‘ 𝑃 ) ‘ 2 ) ∥ ( 2 ↑ ( 𝑁 + 1 ) ) → ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) mod 𝑃 ) ≠ 1 → ( ( odℤ ‘ 𝑃 ) ‘ 2 ) = ( 2 ↑ ( 𝑁 + 1 ) ) ) ) )
92 31 91 sylbid ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( ( 2 ↑ ( 2 ↑ ( 𝑁 + 1 ) ) ) mod 𝑃 ) = 1 → ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) mod 𝑃 ) ≠ 1 → ( ( odℤ ‘ 𝑃 ) ‘ 2 ) = ( 2 ↑ ( 𝑁 + 1 ) ) ) ) )
93 92 com23 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) mod 𝑃 ) ≠ 1 → ( ( ( 2 ↑ ( 2 ↑ ( 𝑁 + 1 ) ) ) mod 𝑃 ) = 1 → ( ( odℤ ‘ 𝑃 ) ‘ 2 ) = ( 2 ↑ ( 𝑁 + 1 ) ) ) ) )
94 93 imp32 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) mod 𝑃 ) ≠ 1 ∧ ( ( 2 ↑ ( 2 ↑ ( 𝑁 + 1 ) ) ) mod 𝑃 ) = 1 ) ) → ( ( odℤ ‘ 𝑃 ) ‘ 2 ) = ( 2 ↑ ( 𝑁 + 1 ) ) )