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

Theorem fmtnoprmfac2 44537
Description: Divisor of Fermat number (special form of Lucas' result, see fmtnofac2 44539): Let Fn be a Fermat number. Let p be a prime divisor of Fn. Then p is in the form: k*2^(n+2)+1 where k is a positive integer. (Contributed by AV, 26-Jul-2021.)
Assertion
Ref Expression
fmtnoprmfac2 ((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1))
Distinct variable groups:   𝑘,𝑁   𝑃,𝑘

Proof of Theorem fmtnoprmfac2
StepHypRef Expression
1 breq1 5030 . . . . . . 7 (𝑃 = 2 → (𝑃 ∥ (FermatNo‘𝑁) ↔ 2 ∥ (FermatNo‘𝑁)))
21adantr 484 . . . . . 6 ((𝑃 = 2 ∧ 𝑁 ∈ (ℤ‘2)) → (𝑃 ∥ (FermatNo‘𝑁) ↔ 2 ∥ (FermatNo‘𝑁)))
3 eluzge2nn0 12362 . . . . . . . . 9 (𝑁 ∈ (ℤ‘2) → 𝑁 ∈ ℕ0)
4 fmtnoodd 44503 . . . . . . . . 9 (𝑁 ∈ ℕ0 → ¬ 2 ∥ (FermatNo‘𝑁))
53, 4syl 17 . . . . . . . 8 (𝑁 ∈ (ℤ‘2) → ¬ 2 ∥ (FermatNo‘𝑁))
65adantl 485 . . . . . . 7 ((𝑃 = 2 ∧ 𝑁 ∈ (ℤ‘2)) → ¬ 2 ∥ (FermatNo‘𝑁))
76pm2.21d 121 . . . . . 6 ((𝑃 = 2 ∧ 𝑁 ∈ (ℤ‘2)) → (2 ∥ (FermatNo‘𝑁) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1)))
82, 7sylbid 243 . . . . 5 ((𝑃 = 2 ∧ 𝑁 ∈ (ℤ‘2)) → (𝑃 ∥ (FermatNo‘𝑁) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1)))
98a1d 25 . . . 4 ((𝑃 = 2 ∧ 𝑁 ∈ (ℤ‘2)) → (𝑃 ∈ ℙ → (𝑃 ∥ (FermatNo‘𝑁) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1))))
109ex 416 . . 3 (𝑃 = 2 → (𝑁 ∈ (ℤ‘2) → (𝑃 ∈ ℙ → (𝑃 ∥ (FermatNo‘𝑁) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1)))))
11103impd 1349 . 2 (𝑃 = 2 → ((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1)))
12 simpr1 1195 . . . . 5 ((¬ 𝑃 = 2 ∧ (𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) → 𝑁 ∈ (ℤ‘2))
13 neqne 2942 . . . . . . . . . 10 𝑃 = 2 → 𝑃 ≠ 2)
1413anim2i 620 . . . . . . . . 9 ((𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2) → (𝑃 ∈ ℙ ∧ 𝑃 ≠ 2))
15 eldifsn 4672 . . . . . . . . 9 (𝑃 ∈ (ℙ ∖ {2}) ↔ (𝑃 ∈ ℙ ∧ 𝑃 ≠ 2))
1614, 15sylibr 237 . . . . . . . 8 ((𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2) → 𝑃 ∈ (ℙ ∖ {2}))
1716ex 416 . . . . . . 7 (𝑃 ∈ ℙ → (¬ 𝑃 = 2 → 𝑃 ∈ (ℙ ∖ {2})))
18173ad2ant2 1135 . . . . . 6 ((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁)) → (¬ 𝑃 = 2 → 𝑃 ∈ (ℙ ∖ {2})))
1918impcom 411 . . . . 5 ((¬ 𝑃 = 2 ∧ (𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) → 𝑃 ∈ (ℙ ∖ {2}))
20 simpr3 1197 . . . . 5 ((¬ 𝑃 = 2 ∧ (𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) → 𝑃 ∥ (FermatNo‘𝑁))
21 fmtnoprmfac2lem1 44536 . . . . 5 ((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑃 ∥ (FermatNo‘𝑁)) → ((2↑((𝑃 − 1) / 2)) mod 𝑃) = 1)
2212, 19, 20, 21syl3anc 1372 . . . 4 ((¬ 𝑃 = 2 ∧ (𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) → ((2↑((𝑃 − 1) / 2)) mod 𝑃) = 1)
23 simpl 486 . . . . . . . . . 10 ((𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2) → 𝑃 ∈ ℙ)
24 2nn 11782 . . . . . . . . . . . . 13 2 ∈ ℕ
2524a1i 11 . . . . . . . . . . . 12 ((𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2) → 2 ∈ ℕ)
26 oddprm 16240 . . . . . . . . . . . . . 14 (𝑃 ∈ (ℙ ∖ {2}) → ((𝑃 − 1) / 2) ∈ ℕ)
2716, 26syl 17 . . . . . . . . . . . . 13 ((𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2) → ((𝑃 − 1) / 2) ∈ ℕ)
2827nnnn0d 12029 . . . . . . . . . . . 12 ((𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2) → ((𝑃 − 1) / 2) ∈ ℕ0)
2925, 28nnexpcld 13691 . . . . . . . . . . 11 ((𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2) → (2↑((𝑃 − 1) / 2)) ∈ ℕ)
3029nnzd 12160 . . . . . . . . . 10 ((𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2) → (2↑((𝑃 − 1) / 2)) ∈ ℤ)
3123, 30jca 515 . . . . . . . . 9 ((𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2) → (𝑃 ∈ ℙ ∧ (2↑((𝑃 − 1) / 2)) ∈ ℤ))
3231ex 416 . . . . . . . 8 (𝑃 ∈ ℙ → (¬ 𝑃 = 2 → (𝑃 ∈ ℙ ∧ (2↑((𝑃 − 1) / 2)) ∈ ℤ)))
33323ad2ant2 1135 . . . . . . 7 ((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁)) → (¬ 𝑃 = 2 → (𝑃 ∈ ℙ ∧ (2↑((𝑃 − 1) / 2)) ∈ ℤ)))
3433impcom 411 . . . . . 6 ((¬ 𝑃 = 2 ∧ (𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) → (𝑃 ∈ ℙ ∧ (2↑((𝑃 − 1) / 2)) ∈ ℤ))
35 modprm1div 16227 . . . . . 6 ((𝑃 ∈ ℙ ∧ (2↑((𝑃 − 1) / 2)) ∈ ℤ) → (((2↑((𝑃 − 1) / 2)) mod 𝑃) = 1 ↔ 𝑃 ∥ ((2↑((𝑃 − 1) / 2)) − 1)))
3634, 35syl 17 . . . . 5 ((¬ 𝑃 = 2 ∧ (𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) → (((2↑((𝑃 − 1) / 2)) mod 𝑃) = 1 ↔ 𝑃 ∥ ((2↑((𝑃 − 1) / 2)) − 1)))
37 prmnn 16108 . . . . . . . . . . . . 13 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
3837adantr 484 . . . . . . . . . . . 12 ((𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2) → 𝑃 ∈ ℕ)
39 2z 12088 . . . . . . . . . . . . 13 2 ∈ ℤ
4039a1i 11 . . . . . . . . . . . 12 ((𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2) → 2 ∈ ℤ)
4113necomd 2989 . . . . . . . . . . . . . 14 𝑃 = 2 → 2 ≠ 𝑃)
4241adantl 485 . . . . . . . . . . . . 13 ((𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2) → 2 ≠ 𝑃)
43 2prm 16126 . . . . . . . . . . . . . . . . 17 2 ∈ ℙ
4443a1i 11 . . . . . . . . . . . . . . . 16 𝑃 = 2 → 2 ∈ ℙ)
4544anim2i 620 . . . . . . . . . . . . . . 15 ((𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2) → (𝑃 ∈ ℙ ∧ 2 ∈ ℙ))
4645ancomd 465 . . . . . . . . . . . . . 14 ((𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2) → (2 ∈ ℙ ∧ 𝑃 ∈ ℙ))
47 prmrp 16146 . . . . . . . . . . . . . 14 ((2 ∈ ℙ ∧ 𝑃 ∈ ℙ) → ((2 gcd 𝑃) = 1 ↔ 2 ≠ 𝑃))
4846, 47syl 17 . . . . . . . . . . . . 13 ((𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2) → ((2 gcd 𝑃) = 1 ↔ 2 ≠ 𝑃))
4942, 48mpbird 260 . . . . . . . . . . . 12 ((𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2) → (2 gcd 𝑃) = 1)
5038, 40, 493jca 1129 . . . . . . . . . . 11 ((𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2) → (𝑃 ∈ ℕ ∧ 2 ∈ ℤ ∧ (2 gcd 𝑃) = 1))
5150, 28jca 515 . . . . . . . . . 10 ((𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2) → ((𝑃 ∈ ℕ ∧ 2 ∈ ℤ ∧ (2 gcd 𝑃) = 1) ∧ ((𝑃 − 1) / 2) ∈ ℕ0))
5251ex 416 . . . . . . . . 9 (𝑃 ∈ ℙ → (¬ 𝑃 = 2 → ((𝑃 ∈ ℕ ∧ 2 ∈ ℤ ∧ (2 gcd 𝑃) = 1) ∧ ((𝑃 − 1) / 2) ∈ ℕ0)))
53523ad2ant2 1135 . . . . . . . 8 ((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁)) → (¬ 𝑃 = 2 → ((𝑃 ∈ ℕ ∧ 2 ∈ ℤ ∧ (2 gcd 𝑃) = 1) ∧ ((𝑃 − 1) / 2) ∈ ℕ0)))
5453impcom 411 . . . . . . 7 ((¬ 𝑃 = 2 ∧ (𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) → ((𝑃 ∈ ℕ ∧ 2 ∈ ℤ ∧ (2 gcd 𝑃) = 1) ∧ ((𝑃 − 1) / 2) ∈ ℕ0))
55 odzdvds 16225 . . . . . . 7 (((𝑃 ∈ ℕ ∧ 2 ∈ ℤ ∧ (2 gcd 𝑃) = 1) ∧ ((𝑃 − 1) / 2) ∈ ℕ0) → (𝑃 ∥ ((2↑((𝑃 − 1) / 2)) − 1) ↔ ((od𝑃)‘2) ∥ ((𝑃 − 1) / 2)))
5654, 55syl 17 . . . . . 6 ((¬ 𝑃 = 2 ∧ (𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) → (𝑃 ∥ ((2↑((𝑃 − 1) / 2)) − 1) ↔ ((od𝑃)‘2) ∥ ((𝑃 − 1) / 2)))
57 eluz2nn 12359 . . . . . . . . . 10 (𝑁 ∈ (ℤ‘2) → 𝑁 ∈ ℕ)
58573ad2ant1 1134 . . . . . . . . 9 ((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁)) → 𝑁 ∈ ℕ)
5958adantl 485 . . . . . . . 8 ((¬ 𝑃 = 2 ∧ (𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) → 𝑁 ∈ ℕ)
60 fmtnoprmfac1lem 44534 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑃 ∥ (FermatNo‘𝑁)) → ((od𝑃)‘2) = (2↑(𝑁 + 1)))
6159, 19, 20, 60syl3anc 1372 . . . . . . 7 ((¬ 𝑃 = 2 ∧ (𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) → ((od𝑃)‘2) = (2↑(𝑁 + 1)))
62 breq1 5030 . . . . . . . . . 10 (((od𝑃)‘2) = (2↑(𝑁 + 1)) → (((od𝑃)‘2) ∥ ((𝑃 − 1) / 2) ↔ (2↑(𝑁 + 1)) ∥ ((𝑃 − 1) / 2)))
6362adantl 485 . . . . . . . . 9 (((¬ 𝑃 = 2 ∧ (𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) ∧ ((od𝑃)‘2) = (2↑(𝑁 + 1))) → (((od𝑃)‘2) ∥ ((𝑃 − 1) / 2) ↔ (2↑(𝑁 + 1)) ∥ ((𝑃 − 1) / 2)))
6424a1i 11 . . . . . . . . . . . . . . . 16 (𝑁 ∈ (ℤ‘2) → 2 ∈ ℕ)
65 peano2nn 11721 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℕ)
6657, 65syl 17 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ (ℤ‘2) → (𝑁 + 1) ∈ ℕ)
6766nnnn0d 12029 . . . . . . . . . . . . . . . 16 (𝑁 ∈ (ℤ‘2) → (𝑁 + 1) ∈ ℕ0)
6864, 67nnexpcld 13691 . . . . . . . . . . . . . . 15 (𝑁 ∈ (ℤ‘2) → (2↑(𝑁 + 1)) ∈ ℕ)
69 nndivides 15702 . . . . . . . . . . . . . . 15 (((2↑(𝑁 + 1)) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ) → ((2↑(𝑁 + 1)) ∥ ((𝑃 − 1) / 2) ↔ ∃𝑘 ∈ ℕ (𝑘 · (2↑(𝑁 + 1))) = ((𝑃 − 1) / 2)))
7068, 27, 69syl2an 599 . . . . . . . . . . . . . 14 ((𝑁 ∈ (ℤ‘2) ∧ (𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2)) → ((2↑(𝑁 + 1)) ∥ ((𝑃 − 1) / 2) ↔ ∃𝑘 ∈ ℕ (𝑘 · (2↑(𝑁 + 1))) = ((𝑃 − 1) / 2)))
71 eqcom 2745 . . . . . . . . . . . . . . . . . . 19 ((𝑘 · (2↑(𝑁 + 1))) = ((𝑃 − 1) / 2) ↔ ((𝑃 − 1) / 2) = (𝑘 · (2↑(𝑁 + 1))))
7271a1i 11 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((𝑘 · (2↑(𝑁 + 1))) = ((𝑃 − 1) / 2) ↔ ((𝑃 − 1) / 2) = (𝑘 · (2↑(𝑁 + 1)))))
7337nncnd 11725 . . . . . . . . . . . . . . . . . . . . . 22 (𝑃 ∈ ℙ → 𝑃 ∈ ℂ)
74 peano2cnm 11023 . . . . . . . . . . . . . . . . . . . . . 22 (𝑃 ∈ ℂ → (𝑃 − 1) ∈ ℂ)
7573, 74syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑃 ∈ ℙ → (𝑃 − 1) ∈ ℂ)
7675adantl 485 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) → (𝑃 − 1) ∈ ℂ)
7776adantr 484 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (𝑃 − 1) ∈ ℂ)
78 simpr 488 . . . . . . . . . . . . . . . . . . . . 21 (((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
7968ad2antrr 726 . . . . . . . . . . . . . . . . . . . . 21 (((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (2↑(𝑁 + 1)) ∈ ℕ)
8078, 79nnmulcld 11762 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (𝑘 · (2↑(𝑁 + 1))) ∈ ℕ)
8180nncnd 11725 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (𝑘 · (2↑(𝑁 + 1))) ∈ ℂ)
82 2cnne0 11919 . . . . . . . . . . . . . . . . . . . 20 (2 ∈ ℂ ∧ 2 ≠ 0)
8382a1i 11 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (2 ∈ ℂ ∧ 2 ≠ 0))
84 divmul3 11374 . . . . . . . . . . . . . . . . . . 19 (((𝑃 − 1) ∈ ℂ ∧ (𝑘 · (2↑(𝑁 + 1))) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (((𝑃 − 1) / 2) = (𝑘 · (2↑(𝑁 + 1))) ↔ (𝑃 − 1) = ((𝑘 · (2↑(𝑁 + 1))) · 2)))
8577, 81, 83, 84syl3anc 1372 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (((𝑃 − 1) / 2) = (𝑘 · (2↑(𝑁 + 1))) ↔ (𝑃 − 1) = ((𝑘 · (2↑(𝑁 + 1))) · 2)))
86 nncn 11717 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
8786adantl 485 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℂ)
8868nncnd 11725 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ (ℤ‘2) → (2↑(𝑁 + 1)) ∈ ℂ)
8988ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (2↑(𝑁 + 1)) ∈ ℂ)
90 2cnd 11787 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 2 ∈ ℂ)
9187, 89, 90mulassd 10735 . . . . . . . . . . . . . . . . . . . . 21 (((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((𝑘 · (2↑(𝑁 + 1))) · 2) = (𝑘 · ((2↑(𝑁 + 1)) · 2)))
92 2cnd 11787 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑁 ∈ ℕ → 2 ∈ ℂ)
9365nnnn0d 12029 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℕ0)
9492, 93expp1d 13596 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ ℕ → (2↑((𝑁 + 1) + 1)) = ((2↑(𝑁 + 1)) · 2))
95 nncn 11717 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
96 add1p1 11960 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑁 ∈ ℂ → ((𝑁 + 1) + 1) = (𝑁 + 2))
9795, 96syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑁 ∈ ℕ → ((𝑁 + 1) + 1) = (𝑁 + 2))
9897oveq2d 7180 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ ℕ → (2↑((𝑁 + 1) + 1)) = (2↑(𝑁 + 2)))
9994, 98eqtr3d 2775 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ ℕ → ((2↑(𝑁 + 1)) · 2) = (2↑(𝑁 + 2)))
10057, 99syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ (ℤ‘2) → ((2↑(𝑁 + 1)) · 2) = (2↑(𝑁 + 2)))
101100ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((2↑(𝑁 + 1)) · 2) = (2↑(𝑁 + 2)))
102101oveq2d 7180 . . . . . . . . . . . . . . . . . . . . 21 (((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (𝑘 · ((2↑(𝑁 + 1)) · 2)) = (𝑘 · (2↑(𝑁 + 2))))
10391, 102eqtrd 2773 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((𝑘 · (2↑(𝑁 + 1))) · 2) = (𝑘 · (2↑(𝑁 + 2))))
104103eqeq2d 2749 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((𝑃 − 1) = ((𝑘 · (2↑(𝑁 + 1))) · 2) ↔ (𝑃 − 1) = (𝑘 · (2↑(𝑁 + 2)))))
10573adantl 485 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) → 𝑃 ∈ ℂ)
106105adantr 484 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 𝑃 ∈ ℂ)
107 1cnd 10707 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 1 ∈ ℂ)
108 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑁 ∈ ℕ → 𝑁 ∈ ℕ)
10924a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑁 ∈ ℕ → 2 ∈ ℕ)
110108, 109nnaddcld 11761 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑁 ∈ ℕ → (𝑁 + 2) ∈ ℕ)
111110nnnn0d 12029 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ ℕ → (𝑁 + 2) ∈ ℕ0)
11257, 111syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ (ℤ‘2) → (𝑁 + 2) ∈ ℕ0)
11364, 112nnexpcld 13691 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ (ℤ‘2) → (2↑(𝑁 + 2)) ∈ ℕ)
114113nncnd 11725 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁 ∈ (ℤ‘2) → (2↑(𝑁 + 2)) ∈ ℂ)
115114ad2antrr 726 . . . . . . . . . . . . . . . . . . . . 21 (((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (2↑(𝑁 + 2)) ∈ ℂ)
11687, 115mulcld 10732 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (𝑘 · (2↑(𝑁 + 2))) ∈ ℂ)
117106, 107, 116subadd2d 11087 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((𝑃 − 1) = (𝑘 · (2↑(𝑁 + 2))) ↔ ((𝑘 · (2↑(𝑁 + 2))) + 1) = 𝑃))
118 eqcom 2745 . . . . . . . . . . . . . . . . . . . 20 (((𝑘 · (2↑(𝑁 + 2))) + 1) = 𝑃𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1))
119118a1i 11 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (((𝑘 · (2↑(𝑁 + 2))) + 1) = 𝑃𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1)))
120104, 117, 1193bitrd 308 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((𝑃 − 1) = ((𝑘 · (2↑(𝑁 + 1))) · 2) ↔ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1)))
12172, 85, 1203bitrd 308 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((𝑘 · (2↑(𝑁 + 1))) = ((𝑃 − 1) / 2) ↔ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1)))
122121rexbidva 3205 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) → (∃𝑘 ∈ ℕ (𝑘 · (2↑(𝑁 + 1))) = ((𝑃 − 1) / 2) ↔ ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1)))
123122biimpd 232 . . . . . . . . . . . . . . 15 ((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) → (∃𝑘 ∈ ℕ (𝑘 · (2↑(𝑁 + 1))) = ((𝑃 − 1) / 2) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1)))
124123adantrr 717 . . . . . . . . . . . . . 14 ((𝑁 ∈ (ℤ‘2) ∧ (𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2)) → (∃𝑘 ∈ ℕ (𝑘 · (2↑(𝑁 + 1))) = ((𝑃 − 1) / 2) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1)))
12570, 124sylbid 243 . . . . . . . . . . . . 13 ((𝑁 ∈ (ℤ‘2) ∧ (𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2)) → ((2↑(𝑁 + 1)) ∥ ((𝑃 − 1) / 2) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1)))
126125expr 460 . . . . . . . . . . . 12 ((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) → (¬ 𝑃 = 2 → ((2↑(𝑁 + 1)) ∥ ((𝑃 − 1) / 2) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1))))
1271263adant3 1133 . . . . . . . . . . 11 ((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁)) → (¬ 𝑃 = 2 → ((2↑(𝑁 + 1)) ∥ ((𝑃 − 1) / 2) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1))))
128127impcom 411 . . . . . . . . . 10 ((¬ 𝑃 = 2 ∧ (𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) → ((2↑(𝑁 + 1)) ∥ ((𝑃 − 1) / 2) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1)))
129128adantr 484 . . . . . . . . 9 (((¬ 𝑃 = 2 ∧ (𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) ∧ ((od𝑃)‘2) = (2↑(𝑁 + 1))) → ((2↑(𝑁 + 1)) ∥ ((𝑃 − 1) / 2) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1)))
13063, 129sylbid 243 . . . . . . . 8 (((¬ 𝑃 = 2 ∧ (𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) ∧ ((od𝑃)‘2) = (2↑(𝑁 + 1))) → (((od𝑃)‘2) ∥ ((𝑃 − 1) / 2) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1)))
131130ex 416 . . . . . . 7 ((¬ 𝑃 = 2 ∧ (𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) → (((od𝑃)‘2) = (2↑(𝑁 + 1)) → (((od𝑃)‘2) ∥ ((𝑃 − 1) / 2) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1))))
13261, 131mpd 15 . . . . . 6 ((¬ 𝑃 = 2 ∧ (𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) → (((od𝑃)‘2) ∥ ((𝑃 − 1) / 2) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1)))
13356, 132sylbid 243 . . . . 5 ((¬ 𝑃 = 2 ∧ (𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) → (𝑃 ∥ ((2↑((𝑃 − 1) / 2)) − 1) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1)))
13436, 133sylbid 243 . . . 4 ((¬ 𝑃 = 2 ∧ (𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) → (((2↑((𝑃 − 1) / 2)) mod 𝑃) = 1 → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1)))
13522, 134mpd 15 . . 3 ((¬ 𝑃 = 2 ∧ (𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1))
136135ex 416 . 2 𝑃 = 2 → ((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1)))
13711, 136pm2.61i 185 1 ((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  w3a 1088   = wceq 1542  wcel 2113  wne 2934  wrex 3054  cdif 3838  {csn 4513   class class class wbr 5027  cfv 6333  (class class class)co 7164  cc 10606  0cc0 10608  1c1 10609   + caddc 10611   · cmul 10613  cmin 10941   / cdiv 11368  cn 11709  2c2 11764  0cn0 11969  cz 12055  cuz 12317   mod cmo 13321  cexp 13514  cdvds 15692   gcd cgcd 15930  cprime 16105  odcodz 16193  FermatNocfmtno 44497
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2161  ax-12 2178  ax-ext 2710  ax-rep 5151  ax-sep 5164  ax-nul 5171  ax-pow 5229  ax-pr 5293  ax-un 7473  ax-inf2 9170  ax-cnex 10664  ax-resscn 10665  ax-1cn 10666  ax-icn 10667  ax-addcl 10668  ax-addrcl 10669  ax-mulcl 10670  ax-mulrcl 10671  ax-mulcom 10672  ax-addass 10673  ax-mulass 10674  ax-distr 10675  ax-i2m1 10676  ax-1ne0 10677  ax-1rid 10678  ax-rnegex 10679  ax-rrecex 10680  ax-cnre 10681  ax-pre-lttri 10682  ax-pre-lttrn 10683  ax-pre-ltadd 10684  ax-pre-mulgt0 10685  ax-pre-sup 10686
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-nel 3039  df-ral 3058  df-rex 3059  df-reu 3060  df-rmo 3061  df-rab 3062  df-v 3399  df-sbc 3680  df-csb 3789  df-dif 3844  df-un 3846  df-in 3848  df-ss 3858  df-pss 3860  df-nul 4210  df-if 4412  df-pw 4487  df-sn 4514  df-pr 4516  df-tp 4518  df-op 4520  df-uni 4794  df-int 4834  df-iun 4880  df-br 5028  df-opab 5090  df-mpt 5108  df-tr 5134  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-se 5479  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6123  df-ord 6169  df-on 6170  df-lim 6171  df-suc 6172  df-iota 6291  df-fun 6335  df-fn 6336  df-f 6337  df-f1 6338  df-fo 6339  df-f1o 6340  df-fv 6341  df-isom 6342  df-riota 7121  df-ov 7167  df-oprab 7168  df-mpo 7169  df-om 7594  df-1st 7707  df-2nd 7708  df-wrecs 7969  df-recs 8030  df-rdg 8068  df-1o 8124  df-2o 8125  df-oadd 8128  df-er 8313  df-map 8432  df-en 8549  df-dom 8550  df-sdom 8551  df-fin 8552  df-sup 8972  df-inf 8973  df-oi 9040  df-dju 9396  df-card 9434  df-pnf 10748  df-mnf 10749  df-xr 10750  df-ltxr 10751  df-le 10752  df-sub 10943  df-neg 10944  df-div 11369  df-nn 11710  df-2 11772  df-3 11773  df-4 11774  df-5 11775  df-6 11776  df-7 11777  df-8 11778  df-n0 11970  df-xnn0 12042  df-z 12056  df-uz 12318  df-q 12424  df-rp 12466  df-ioo 12818  df-ico 12820  df-fz 12975  df-fzo 13118  df-fl 13246  df-mod 13322  df-seq 13454  df-exp 13515  df-fac 13719  df-hash 13776  df-cj 14541  df-re 14542  df-im 14543  df-sqrt 14677  df-abs 14678  df-clim 14928  df-prod 15345  df-dvds 15693  df-gcd 15931  df-prm 16106  df-odz 16195  df-phi 16196  df-pc 16267  df-lgs 26023  df-fmtno 44498
This theorem is referenced by:  fmtnofac2  44539  fmtno4prmfac  44542
  Copyright terms: Public domain W3C validator