Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  odz2prm2pw Structured version   Visualization version   GIF version

Theorem odz2prm2pw 43123
Description: Any power of two is coprime to any prime not being two. (Contributed by AV, 25-Jul-2021.)
Assertion
Ref Expression
odz2prm2pw (((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ (((2↑(2↑𝑁)) mod 𝑃) ≠ 1 ∧ ((2↑(2↑(𝑁 + 1))) mod 𝑃) = 1)) → ((od𝑃)‘2) = (2↑(𝑁 + 1)))

Proof of Theorem odz2prm2pw
Dummy variable 𝑛 is distinct from all other variables.
StepHypRef Expression
1 eldifi 3988 . . . . . 6 (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℙ)
2 2nn 11512 . . . . . . . . 9 2 ∈ ℕ
32a1i 11 . . . . . . . 8 (𝑁 ∈ ℕ → 2 ∈ ℕ)
4 2nn0 11725 . . . . . . . . . 10 2 ∈ ℕ0
54a1i 11 . . . . . . . . 9 (𝑁 ∈ ℕ → 2 ∈ ℕ0)
6 peano2nn 11452 . . . . . . . . . 10 (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℕ)
76nnnn0d 11766 . . . . . . . . 9 (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℕ0)
85, 7nn0expcld 13421 . . . . . . . 8 (𝑁 ∈ ℕ → (2↑(𝑁 + 1)) ∈ ℕ0)
93, 8nnexpcld 13420 . . . . . . 7 (𝑁 ∈ ℕ → (2↑(2↑(𝑁 + 1))) ∈ ℕ)
109nnzd 11898 . . . . . 6 (𝑁 ∈ ℕ → (2↑(2↑(𝑁 + 1))) ∈ ℤ)
11 modprm1div 15989 . . . . . 6 ((𝑃 ∈ ℙ ∧ (2↑(2↑(𝑁 + 1))) ∈ ℤ) → (((2↑(2↑(𝑁 + 1))) mod 𝑃) = 1 ↔ 𝑃 ∥ ((2↑(2↑(𝑁 + 1))) − 1)))
121, 10, 11syl2anr 588 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → (((2↑(2↑(𝑁 + 1))) mod 𝑃) = 1 ↔ 𝑃 ∥ ((2↑(2↑(𝑁 + 1))) − 1)))
13 prmnn 15873 . . . . . . . . 9 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
141, 13syl 17 . . . . . . . 8 (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℕ)
1514adantl 474 . . . . . . 7 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → 𝑃 ∈ ℕ)
16 2z 11826 . . . . . . . 8 2 ∈ ℤ
1716a1i 11 . . . . . . 7 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → 2 ∈ ℤ)
18 eldifsn 4590 . . . . . . . . . 10 (𝑃 ∈ (ℙ ∖ {2}) ↔ (𝑃 ∈ ℙ ∧ 𝑃 ≠ 2))
19 simpr 477 . . . . . . . . . . 11 ((𝑃 ∈ ℙ ∧ 𝑃 ≠ 2) → 𝑃 ≠ 2)
2019necomd 3017 . . . . . . . . . 10 ((𝑃 ∈ ℙ ∧ 𝑃 ≠ 2) → 2 ≠ 𝑃)
2118, 20sylbi 209 . . . . . . . . 9 (𝑃 ∈ (ℙ ∖ {2}) → 2 ≠ 𝑃)
22 2prm 15891 . . . . . . . . . 10 2 ∈ ℙ
23 prmrp 15911 . . . . . . . . . 10 ((2 ∈ ℙ ∧ 𝑃 ∈ ℙ) → ((2 gcd 𝑃) = 1 ↔ 2 ≠ 𝑃))
2422, 1, 23sylancr 579 . . . . . . . . 9 (𝑃 ∈ (ℙ ∖ {2}) → ((2 gcd 𝑃) = 1 ↔ 2 ≠ 𝑃))
2521, 24mpbird 249 . . . . . . . 8 (𝑃 ∈ (ℙ ∖ {2}) → (2 gcd 𝑃) = 1)
2625adantl 474 . . . . . . 7 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → (2 gcd 𝑃) = 1)
2715, 17, 263jca 1109 . . . . . 6 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → (𝑃 ∈ ℕ ∧ 2 ∈ ℤ ∧ (2 gcd 𝑃) = 1))
288adantr 473 . . . . . 6 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → (2↑(𝑁 + 1)) ∈ ℕ0)
29 odzdvds 15987 . . . . . 6 (((𝑃 ∈ ℕ ∧ 2 ∈ ℤ ∧ (2 gcd 𝑃) = 1) ∧ (2↑(𝑁 + 1)) ∈ ℕ0) → (𝑃 ∥ ((2↑(2↑(𝑁 + 1))) − 1) ↔ ((od𝑃)‘2) ∥ (2↑(𝑁 + 1))))
3027, 28, 29syl2anc 576 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → (𝑃 ∥ ((2↑(2↑(𝑁 + 1))) − 1) ↔ ((od𝑃)‘2) ∥ (2↑(𝑁 + 1))))
3112, 30bitrd 271 . . . 4 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → (((2↑(2↑(𝑁 + 1))) mod 𝑃) = 1 ↔ ((od𝑃)‘2) ∥ (2↑(𝑁 + 1))))
32 nnnn0 11714 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
335, 32nn0expcld 13421 . . . . . . . . . . 11 (𝑁 ∈ ℕ → (2↑𝑁) ∈ ℕ0)
343, 33nnexpcld 13420 . . . . . . . . . 10 (𝑁 ∈ ℕ → (2↑(2↑𝑁)) ∈ ℕ)
3534nnzd 11898 . . . . . . . . 9 (𝑁 ∈ ℕ → (2↑(2↑𝑁)) ∈ ℤ)
36 modprm1div 15989 . . . . . . . . 9 ((𝑃 ∈ ℙ ∧ (2↑(2↑𝑁)) ∈ ℤ) → (((2↑(2↑𝑁)) mod 𝑃) = 1 ↔ 𝑃 ∥ ((2↑(2↑𝑁)) − 1)))
371, 35, 36syl2anr 588 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → (((2↑(2↑𝑁)) mod 𝑃) = 1 ↔ 𝑃 ∥ ((2↑(2↑𝑁)) − 1)))
3833adantr 473 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → (2↑𝑁) ∈ ℕ0)
39 odzdvds 15987 . . . . . . . . 9 (((𝑃 ∈ ℕ ∧ 2 ∈ ℤ ∧ (2 gcd 𝑃) = 1) ∧ (2↑𝑁) ∈ ℕ0) → (𝑃 ∥ ((2↑(2↑𝑁)) − 1) ↔ ((od𝑃)‘2) ∥ (2↑𝑁)))
4027, 38, 39syl2anc 576 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → (𝑃 ∥ ((2↑(2↑𝑁)) − 1) ↔ ((od𝑃)‘2) ∥ (2↑𝑁)))
4137, 40bitrd 271 . . . . . . 7 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → (((2↑(2↑𝑁)) mod 𝑃) = 1 ↔ ((od𝑃)‘2) ∥ (2↑𝑁)))
4241necon3abid 2998 . . . . . 6 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → (((2↑(2↑𝑁)) mod 𝑃) ≠ 1 ↔ ¬ ((od𝑃)‘2) ∥ (2↑𝑁)))
43 odzcl 15985 . . . . . . . . . 10 ((𝑃 ∈ ℕ ∧ 2 ∈ ℤ ∧ (2 gcd 𝑃) = 1) → ((od𝑃)‘2) ∈ ℕ)
4427, 43syl 17 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → ((od𝑃)‘2) ∈ ℕ)
457adantr 473 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → (𝑁 + 1) ∈ ℕ0)
46 dvdsprmpweqle 16077 . . . . . . . . 9 ((2 ∈ ℙ ∧ ((od𝑃)‘2) ∈ ℕ ∧ (𝑁 + 1) ∈ ℕ0) → (((od𝑃)‘2) ∥ (2↑(𝑁 + 1)) → ∃𝑛 ∈ ℕ0 (𝑛 ≤ (𝑁 + 1) ∧ ((od𝑃)‘2) = (2↑𝑛))))
4722, 44, 45, 46mp3an2i 1446 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → (((od𝑃)‘2) ∥ (2↑(𝑁 + 1)) → ∃𝑛 ∈ ℕ0 (𝑛 ≤ (𝑁 + 1) ∧ ((od𝑃)‘2) = (2↑𝑛))))
48 breq1 4929 . . . . . . . . . . . . 13 (((od𝑃)‘2) = (2↑𝑛) → (((od𝑃)‘2) ∥ (2↑𝑁) ↔ (2↑𝑛) ∥ (2↑𝑁)))
4948adantl 474 . . . . . . . . . . . 12 (((((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 ≤ (𝑁 + 1)) ∧ ((od𝑃)‘2) = (2↑𝑛)) → (((od𝑃)‘2) ∥ (2↑𝑁) ↔ (2↑𝑛) ∥ (2↑𝑁)))
5049notbid 310 . . . . . . . . . . 11 (((((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 ≤ (𝑁 + 1)) ∧ ((od𝑃)‘2) = (2↑𝑛)) → (¬ ((od𝑃)‘2) ∥ (2↑𝑁) ↔ ¬ (2↑𝑛) ∥ (2↑𝑁)))
51 simpr 477 . . . . . . . . . . . . . 14 (((((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 ≤ (𝑁 + 1)) ∧ ((od𝑃)‘2) = (2↑𝑛)) → ((od𝑃)‘2) = (2↑𝑛))
5251adantr 473 . . . . . . . . . . . . 13 ((((((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 ≤ (𝑁 + 1)) ∧ ((od𝑃)‘2) = (2↑𝑛)) ∧ ¬ (2↑𝑛) ∥ (2↑𝑁)) → ((od𝑃)‘2) = (2↑𝑛))
53 nn0re 11716 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ0𝑛 ∈ ℝ)
546nnred 11455 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℝ)
5554adantr 473 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → (𝑁 + 1) ∈ ℝ)
56 leloe 10526 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ℝ ∧ (𝑁 + 1) ∈ ℝ) → (𝑛 ≤ (𝑁 + 1) ↔ (𝑛 < (𝑁 + 1) ∨ 𝑛 = (𝑁 + 1))))
5753, 55, 56syl2anr 588 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ 𝑛 ∈ ℕ0) → (𝑛 ≤ (𝑁 + 1) ↔ (𝑛 < (𝑁 + 1) ∨ 𝑛 = (𝑁 + 1))))
58 simpr 477 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈ ℕ0)
59 nn0z 11817 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 ∈ ℕ0𝑛 ∈ ℤ)
6059adantl 474 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈ ℤ)
6160adantr 473 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 < (𝑁 + 1)) → 𝑛 ∈ ℤ)
62 nnz 11816 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
6362adantr 473 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → 𝑁 ∈ ℤ)
6463adantr 473 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ 𝑛 ∈ ℕ0) → 𝑁 ∈ ℤ)
6564adantr 473 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 < (𝑁 + 1)) → 𝑁 ∈ ℤ)
66 zleltp1 11845 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑛 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑛𝑁𝑛 < (𝑁 + 1)))
6759, 63, 66syl2anr 588 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ 𝑛 ∈ ℕ0) → (𝑛𝑁𝑛 < (𝑁 + 1)))
6867biimpar 470 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 < (𝑁 + 1)) → 𝑛𝑁)
69 eluz2 12063 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ (ℤ𝑛) ↔ (𝑛 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑛𝑁))
7061, 65, 68, 69syl3anbrc 1324 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 < (𝑁 + 1)) → 𝑁 ∈ (ℤ𝑛))
71 dvdsexp 15536 . . . . . . . . . . . . . . . . . . . . . 22 ((2 ∈ ℤ ∧ 𝑛 ∈ ℕ0𝑁 ∈ (ℤ𝑛)) → (2↑𝑛) ∥ (2↑𝑁))
7216, 58, 70, 71mp3an2ani 1448 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 < (𝑁 + 1)) → (2↑𝑛) ∥ (2↑𝑁))
7372pm2.24d 149 . . . . . . . . . . . . . . . . . . . 20 ((((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 < (𝑁 + 1)) → (¬ (2↑𝑛) ∥ (2↑𝑁) → (2↑𝑛) = (2↑(𝑁 + 1))))
7473expcom 406 . . . . . . . . . . . . . . . . . . 19 (𝑛 < (𝑁 + 1) → (((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ 𝑛 ∈ ℕ0) → (¬ (2↑𝑛) ∥ (2↑𝑁) → (2↑𝑛) = (2↑(𝑁 + 1)))))
75 oveq2 6983 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = (𝑁 + 1) → (2↑𝑛) = (2↑(𝑁 + 1)))
76752a1d 26 . . . . . . . . . . . . . . . . . . 19 (𝑛 = (𝑁 + 1) → (((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ 𝑛 ∈ ℕ0) → (¬ (2↑𝑛) ∥ (2↑𝑁) → (2↑𝑛) = (2↑(𝑁 + 1)))))
7774, 76jaoi 844 . . . . . . . . . . . . . . . . . 18 ((𝑛 < (𝑁 + 1) ∨ 𝑛 = (𝑁 + 1)) → (((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ 𝑛 ∈ ℕ0) → (¬ (2↑𝑛) ∥ (2↑𝑁) → (2↑𝑛) = (2↑(𝑁 + 1)))))
7877com12 32 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ 𝑛 ∈ ℕ0) → ((𝑛 < (𝑁 + 1) ∨ 𝑛 = (𝑁 + 1)) → (¬ (2↑𝑛) ∥ (2↑𝑁) → (2↑𝑛) = (2↑(𝑁 + 1)))))
7957, 78sylbid 232 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ 𝑛 ∈ ℕ0) → (𝑛 ≤ (𝑁 + 1) → (¬ (2↑𝑛) ∥ (2↑𝑁) → (2↑𝑛) = (2↑(𝑁 + 1)))))
8079imp 398 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 ≤ (𝑁 + 1)) → (¬ (2↑𝑛) ∥ (2↑𝑁) → (2↑𝑛) = (2↑(𝑁 + 1))))
8180adantr 473 . . . . . . . . . . . . . 14 (((((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 ≤ (𝑁 + 1)) ∧ ((od𝑃)‘2) = (2↑𝑛)) → (¬ (2↑𝑛) ∥ (2↑𝑁) → (2↑𝑛) = (2↑(𝑁 + 1))))
8281imp 398 . . . . . . . . . . . . 13 ((((((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 ≤ (𝑁 + 1)) ∧ ((od𝑃)‘2) = (2↑𝑛)) ∧ ¬ (2↑𝑛) ∥ (2↑𝑁)) → (2↑𝑛) = (2↑(𝑁 + 1)))
8352, 82eqtrd 2809 . . . . . . . . . . . 12 ((((((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 ≤ (𝑁 + 1)) ∧ ((od𝑃)‘2) = (2↑𝑛)) ∧ ¬ (2↑𝑛) ∥ (2↑𝑁)) → ((od𝑃)‘2) = (2↑(𝑁 + 1)))
8483ex 405 . . . . . . . . . . 11 (((((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 ≤ (𝑁 + 1)) ∧ ((od𝑃)‘2) = (2↑𝑛)) → (¬ (2↑𝑛) ∥ (2↑𝑁) → ((od𝑃)‘2) = (2↑(𝑁 + 1))))
8550, 84sylbid 232 . . . . . . . . . 10 (((((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 ≤ (𝑁 + 1)) ∧ ((od𝑃)‘2) = (2↑𝑛)) → (¬ ((od𝑃)‘2) ∥ (2↑𝑁) → ((od𝑃)‘2) = (2↑(𝑁 + 1))))
8685expl 450 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ 𝑛 ∈ ℕ0) → ((𝑛 ≤ (𝑁 + 1) ∧ ((od𝑃)‘2) = (2↑𝑛)) → (¬ ((od𝑃)‘2) ∥ (2↑𝑁) → ((od𝑃)‘2) = (2↑(𝑁 + 1)))))
8786rexlimdva 3224 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → (∃𝑛 ∈ ℕ0 (𝑛 ≤ (𝑁 + 1) ∧ ((od𝑃)‘2) = (2↑𝑛)) → (¬ ((od𝑃)‘2) ∥ (2↑𝑁) → ((od𝑃)‘2) = (2↑(𝑁 + 1)))))
8847, 87syld 47 . . . . . . 7 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → (((od𝑃)‘2) ∥ (2↑(𝑁 + 1)) → (¬ ((od𝑃)‘2) ∥ (2↑𝑁) → ((od𝑃)‘2) = (2↑(𝑁 + 1)))))
8988com23 86 . . . . . 6 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → (¬ ((od𝑃)‘2) ∥ (2↑𝑁) → (((od𝑃)‘2) ∥ (2↑(𝑁 + 1)) → ((od𝑃)‘2) = (2↑(𝑁 + 1)))))
9042, 89sylbid 232 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → (((2↑(2↑𝑁)) mod 𝑃) ≠ 1 → (((od𝑃)‘2) ∥ (2↑(𝑁 + 1)) → ((od𝑃)‘2) = (2↑(𝑁 + 1)))))
9190com23 86 . . . 4 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → (((od𝑃)‘2) ∥ (2↑(𝑁 + 1)) → (((2↑(2↑𝑁)) mod 𝑃) ≠ 1 → ((od𝑃)‘2) = (2↑(𝑁 + 1)))))
9231, 91sylbid 232 . . 3 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → (((2↑(2↑(𝑁 + 1))) mod 𝑃) = 1 → (((2↑(2↑𝑁)) mod 𝑃) ≠ 1 → ((od𝑃)‘2) = (2↑(𝑁 + 1)))))
9392com23 86 . 2 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → (((2↑(2↑𝑁)) mod 𝑃) ≠ 1 → (((2↑(2↑(𝑁 + 1))) mod 𝑃) = 1 → ((od𝑃)‘2) = (2↑(𝑁 + 1)))))
9493imp32 411 1 (((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ (((2↑(2↑𝑁)) mod 𝑃) ≠ 1 ∧ ((2↑(2↑(𝑁 + 1))) mod 𝑃) = 1)) → ((od𝑃)‘2) = (2↑(𝑁 + 1)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 387  wo 834  w3a 1069   = wceq 1508  wcel 2051  wne 2962  wrex 3084  cdif 3821  {csn 4436   class class class wbr 4926  cfv 6186  (class class class)co 6975  cr 10333  1c1 10335   + caddc 10337   < clt 10473  cle 10474  cmin 10669  cn 11438  2c2 11494  0cn0 11706  cz 11792  cuz 12057   mod cmo 13051  cexp 13243  cdvds 15466   gcd cgcd 15702  cprime 15870  odcodz 15955
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2745  ax-rep 5046  ax-sep 5057  ax-nul 5064  ax-pow 5116  ax-pr 5183  ax-un 7278  ax-cnex 10390  ax-resscn 10391  ax-1cn 10392  ax-icn 10393  ax-addcl 10394  ax-addrcl 10395  ax-mulcl 10396  ax-mulrcl 10397  ax-mulcom 10398  ax-addass 10399  ax-mulass 10400  ax-distr 10401  ax-i2m1 10402  ax-1ne0 10403  ax-1rid 10404  ax-rnegex 10405  ax-rrecex 10406  ax-cnre 10407  ax-pre-lttri 10408  ax-pre-lttrn 10409  ax-pre-ltadd 10410  ax-pre-mulgt0 10411  ax-pre-sup 10412
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3or 1070  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2548  df-eu 2585  df-clab 2754  df-cleq 2766  df-clel 2841  df-nfc 2913  df-ne 2963  df-nel 3069  df-ral 3088  df-rex 3089  df-reu 3090  df-rmo 3091  df-rab 3092  df-v 3412  df-sbc 3677  df-csb 3782  df-dif 3827  df-un 3829  df-in 3831  df-ss 3838  df-pss 3840  df-nul 4174  df-if 4346  df-pw 4419  df-sn 4437  df-pr 4439  df-tp 4441  df-op 4443  df-uni 4710  df-int 4747  df-iun 4791  df-br 4927  df-opab 4989  df-mpt 5006  df-tr 5028  df-id 5309  df-eprel 5314  df-po 5323  df-so 5324  df-fr 5363  df-we 5365  df-xp 5410  df-rel 5411  df-cnv 5412  df-co 5413  df-dm 5414  df-rn 5415  df-res 5416  df-ima 5417  df-pred 5984  df-ord 6030  df-on 6031  df-lim 6032  df-suc 6033  df-iota 6150  df-fun 6188  df-fn 6189  df-f 6190  df-f1 6191  df-fo 6192  df-f1o 6193  df-fv 6194  df-riota 6936  df-ov 6978  df-oprab 6979  df-mpo 6980  df-om 7396  df-1st 7500  df-2nd 7501  df-wrecs 7749  df-recs 7811  df-rdg 7849  df-1o 7904  df-2o 7905  df-oadd 7908  df-er 8088  df-map 8207  df-en 8306  df-dom 8307  df-sdom 8308  df-fin 8309  df-sup 8700  df-inf 8701  df-card 9161  df-pnf 10475  df-mnf 10476  df-xr 10477  df-ltxr 10478  df-le 10479  df-sub 10671  df-neg 10672  df-div 11098  df-nn 11439  df-2 11502  df-3 11503  df-n0 11707  df-xnn0 11779  df-z 11793  df-uz 12058  df-q 12162  df-rp 12204  df-fz 12708  df-fzo 12849  df-fl 12976  df-mod 13052  df-seq 13184  df-exp 13244  df-hash 13505  df-cj 14318  df-re 14319  df-im 14320  df-sqrt 14454  df-abs 14455  df-dvds 15467  df-gcd 15703  df-prm 15871  df-odz 15957  df-phi 15958  df-pc 16029
This theorem is referenced by:  fmtnoprmfac1lem  43124
  Copyright terms: Public domain W3C validator