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 42007
 Description: Divisor of Fermat number (special form of Lucas' result, see fmtnofac2 42009): 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 4789 . . . . . . 7 (𝑃 = 2 → (𝑃 ∥ (FermatNo‘𝑁) ↔ 2 ∥ (FermatNo‘𝑁)))
21adantr 466 . . . . . 6 ((𝑃 = 2 ∧ 𝑁 ∈ (ℤ‘2)) → (𝑃 ∥ (FermatNo‘𝑁) ↔ 2 ∥ (FermatNo‘𝑁)))
3 eluzge2nn0 11929 . . . . . . . . 9 (𝑁 ∈ (ℤ‘2) → 𝑁 ∈ ℕ0)
4 fmtnoodd 41973 . . . . . . . . 9 (𝑁 ∈ ℕ0 → ¬ 2 ∥ (FermatNo‘𝑁))
53, 4syl 17 . . . . . . . 8 (𝑁 ∈ (ℤ‘2) → ¬ 2 ∥ (FermatNo‘𝑁))
65adantl 467 . . . . . . 7 ((𝑃 = 2 ∧ 𝑁 ∈ (ℤ‘2)) → ¬ 2 ∥ (FermatNo‘𝑁))
76pm2.21d 119 . . . . . 6 ((𝑃 = 2 ∧ 𝑁 ∈ (ℤ‘2)) → (2 ∥ (FermatNo‘𝑁) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1)))
82, 7sylbid 230 . . . . 5 ((𝑃 = 2 ∧ 𝑁 ∈ (ℤ‘2)) → (𝑃 ∥ (FermatNo‘𝑁) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1)))
98a1d 25 . . . 4 ((𝑃 = 2 ∧ 𝑁 ∈ (ℤ‘2)) → (𝑃 ∈ ℙ → (𝑃 ∥ (FermatNo‘𝑁) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1))))
109ex 397 . . 3 (𝑃 = 2 → (𝑁 ∈ (ℤ‘2) → (𝑃 ∈ ℙ → (𝑃 ∥ (FermatNo‘𝑁) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1)))))
11103impd 1441 . 2 (𝑃 = 2 → ((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1)))
12 simpr1 1233 . . . . 5 ((¬ 𝑃 = 2 ∧ (𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) → 𝑁 ∈ (ℤ‘2))
13 neqne 2951 . . . . . . . . . 10 𝑃 = 2 → 𝑃 ≠ 2)
1413anim2i 603 . . . . . . . . 9 ((𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2) → (𝑃 ∈ ℙ ∧ 𝑃 ≠ 2))
15 eldifsn 4453 . . . . . . . . 9 (𝑃 ∈ (ℙ ∖ {2}) ↔ (𝑃 ∈ ℙ ∧ 𝑃 ≠ 2))
1614, 15sylibr 224 . . . . . . . 8 ((𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2) → 𝑃 ∈ (ℙ ∖ {2}))
1716ex 397 . . . . . . 7 (𝑃 ∈ ℙ → (¬ 𝑃 = 2 → 𝑃 ∈ (ℙ ∖ {2})))
18173ad2ant2 1128 . . . . . 6 ((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁)) → (¬ 𝑃 = 2 → 𝑃 ∈ (ℙ ∖ {2})))
1918impcom 394 . . . . 5 ((¬ 𝑃 = 2 ∧ (𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) → 𝑃 ∈ (ℙ ∖ {2}))
20 simpr3 1237 . . . . 5 ((¬ 𝑃 = 2 ∧ (𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) → 𝑃 ∥ (FermatNo‘𝑁))
21 fmtnoprmfac2lem1 42006 . . . . 5 ((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑃 ∥ (FermatNo‘𝑁)) → ((2↑((𝑃 − 1) / 2)) mod 𝑃) = 1)
2212, 19, 20, 21syl3anc 1476 . . . 4 ((¬ 𝑃 = 2 ∧ (𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) → ((2↑((𝑃 − 1) / 2)) mod 𝑃) = 1)
23 simpl 468 . . . . . . . . . 10 ((𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2) → 𝑃 ∈ ℙ)
24 2nn 11387 . . . . . . . . . . . . 13 2 ∈ ℕ
2524a1i 11 . . . . . . . . . . . 12 ((𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2) → 2 ∈ ℕ)
26 oddprm 15722 . . . . . . . . . . . . . 14 (𝑃 ∈ (ℙ ∖ {2}) → ((𝑃 − 1) / 2) ∈ ℕ)
2716, 26syl 17 . . . . . . . . . . . . 13 ((𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2) → ((𝑃 − 1) / 2) ∈ ℕ)
2827nnnn0d 11553 . . . . . . . . . . . 12 ((𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2) → ((𝑃 − 1) / 2) ∈ ℕ0)
2925, 28nnexpcld 13237 . . . . . . . . . . 11 ((𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2) → (2↑((𝑃 − 1) / 2)) ∈ ℕ)
3029nnzd 11683 . . . . . . . . . 10 ((𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2) → (2↑((𝑃 − 1) / 2)) ∈ ℤ)
3123, 30jca 501 . . . . . . . . 9 ((𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2) → (𝑃 ∈ ℙ ∧ (2↑((𝑃 − 1) / 2)) ∈ ℤ))
3231ex 397 . . . . . . . 8 (𝑃 ∈ ℙ → (¬ 𝑃 = 2 → (𝑃 ∈ ℙ ∧ (2↑((𝑃 − 1) / 2)) ∈ ℤ)))
33323ad2ant2 1128 . . . . . . 7 ((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁)) → (¬ 𝑃 = 2 → (𝑃 ∈ ℙ ∧ (2↑((𝑃 − 1) / 2)) ∈ ℤ)))
3433impcom 394 . . . . . 6 ((¬ 𝑃 = 2 ∧ (𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) → (𝑃 ∈ ℙ ∧ (2↑((𝑃 − 1) / 2)) ∈ ℤ))
35 modprm1div 15709 . . . . . 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 15595 . . . . . . . . . . . . 13 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
3837adantr 466 . . . . . . . . . . . 12 ((𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2) → 𝑃 ∈ ℕ)
39 2z 11611 . . . . . . . . . . . . 13 2 ∈ ℤ
4039a1i 11 . . . . . . . . . . . 12 ((𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2) → 2 ∈ ℤ)
4113necomd 2998 . . . . . . . . . . . . . 14 𝑃 = 2 → 2 ≠ 𝑃)
4241adantl 467 . . . . . . . . . . . . 13 ((𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2) → 2 ≠ 𝑃)
43 2prm 15612 . . . . . . . . . . . . . . . . 17 2 ∈ ℙ
4443a1i 11 . . . . . . . . . . . . . . . 16 𝑃 = 2 → 2 ∈ ℙ)
4544anim2i 603 . . . . . . . . . . . . . . 15 ((𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2) → (𝑃 ∈ ℙ ∧ 2 ∈ ℙ))
4645ancomd 453 . . . . . . . . . . . . . 14 ((𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2) → (2 ∈ ℙ ∧ 𝑃 ∈ ℙ))
47 prmrp 15631 . . . . . . . . . . . . . 14 ((2 ∈ ℙ ∧ 𝑃 ∈ ℙ) → ((2 gcd 𝑃) = 1 ↔ 2 ≠ 𝑃))
4846, 47syl 17 . . . . . . . . . . . . 13 ((𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2) → ((2 gcd 𝑃) = 1 ↔ 2 ≠ 𝑃))
4942, 48mpbird 247 . . . . . . . . . . . 12 ((𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2) → (2 gcd 𝑃) = 1)
5038, 40, 493jca 1122 . . . . . . . . . . 11 ((𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2) → (𝑃 ∈ ℕ ∧ 2 ∈ ℤ ∧ (2 gcd 𝑃) = 1))
5150, 28jca 501 . . . . . . . . . 10 ((𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2) → ((𝑃 ∈ ℕ ∧ 2 ∈ ℤ ∧ (2 gcd 𝑃) = 1) ∧ ((𝑃 − 1) / 2) ∈ ℕ0))
5251ex 397 . . . . . . . . 9 (𝑃 ∈ ℙ → (¬ 𝑃 = 2 → ((𝑃 ∈ ℕ ∧ 2 ∈ ℤ ∧ (2 gcd 𝑃) = 1) ∧ ((𝑃 − 1) / 2) ∈ ℕ0)))
53523ad2ant2 1128 . . . . . . . 8 ((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁)) → (¬ 𝑃 = 2 → ((𝑃 ∈ ℕ ∧ 2 ∈ ℤ ∧ (2 gcd 𝑃) = 1) ∧ ((𝑃 − 1) / 2) ∈ ℕ0)))
5453impcom 394 . . . . . . 7 ((¬ 𝑃 = 2 ∧ (𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) → ((𝑃 ∈ ℕ ∧ 2 ∈ ℤ ∧ (2 gcd 𝑃) = 1) ∧ ((𝑃 − 1) / 2) ∈ ℕ0))
55 odzdvds 15707 . . . . . . 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 11928 . . . . . . . . . 10 (𝑁 ∈ (ℤ‘2) → 𝑁 ∈ ℕ)
58573ad2ant1 1127 . . . . . . . . 9 ((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁)) → 𝑁 ∈ ℕ)
5958adantl 467 . . . . . . . 8 ((¬ 𝑃 = 2 ∧ (𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) → 𝑁 ∈ ℕ)
60 fmtnoprmfac1lem 42004 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑃 ∥ (FermatNo‘𝑁)) → ((od𝑃)‘2) = (2↑(𝑁 + 1)))
6159, 19, 20, 60syl3anc 1476 . . . . . . 7 ((¬ 𝑃 = 2 ∧ (𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) → ((od𝑃)‘2) = (2↑(𝑁 + 1)))
62 breq1 4789 . . . . . . . . . 10 (((od𝑃)‘2) = (2↑(𝑁 + 1)) → (((od𝑃)‘2) ∥ ((𝑃 − 1) / 2) ↔ (2↑(𝑁 + 1)) ∥ ((𝑃 − 1) / 2)))
6362adantl 467 . . . . . . . . 9 (((¬ 𝑃 = 2 ∧ (𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) ∧ ((od𝑃)‘2) = (2↑(𝑁 + 1))) → (((od𝑃)‘2) ∥ ((𝑃 − 1) / 2) ↔ (2↑(𝑁 + 1)) ∥ ((𝑃 − 1) / 2)))
6424a1i 11 . . . . . . . . . . . . . . . 16 (𝑁 ∈ (ℤ‘2) → 2 ∈ ℕ)
65 peano2nn 11234 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℕ)
6657, 65syl 17 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ (ℤ‘2) → (𝑁 + 1) ∈ ℕ)
6766nnnn0d 11553 . . . . . . . . . . . . . . . 16 (𝑁 ∈ (ℤ‘2) → (𝑁 + 1) ∈ ℕ0)
6864, 67nnexpcld 13237 . . . . . . . . . . . . . . 15 (𝑁 ∈ (ℤ‘2) → (2↑(𝑁 + 1)) ∈ ℕ)
69 nndivides 15199 . . . . . . . . . . . . . . 15 (((2↑(𝑁 + 1)) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ) → ((2↑(𝑁 + 1)) ∥ ((𝑃 − 1) / 2) ↔ ∃𝑘 ∈ ℕ (𝑘 · (2↑(𝑁 + 1))) = ((𝑃 − 1) / 2)))
7068, 27, 69syl2an 583 . . . . . . . . . . . . . 14 ((𝑁 ∈ (ℤ‘2) ∧ (𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2)) → ((2↑(𝑁 + 1)) ∥ ((𝑃 − 1) / 2) ↔ ∃𝑘 ∈ ℕ (𝑘 · (2↑(𝑁 + 1))) = ((𝑃 − 1) / 2)))
71 eqcom 2778 . . . . . . . . . . . . . . . . . . 19 ((𝑘 · (2↑(𝑁 + 1))) = ((𝑃 − 1) / 2) ↔ ((𝑃 − 1) / 2) = (𝑘 · (2↑(𝑁 + 1))))
7271a1i 11 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((𝑘 · (2↑(𝑁 + 1))) = ((𝑃 − 1) / 2) ↔ ((𝑃 − 1) / 2) = (𝑘 · (2↑(𝑁 + 1)))))
7337nncnd 11238 . . . . . . . . . . . . . . . . . . . . . 22 (𝑃 ∈ ℙ → 𝑃 ∈ ℂ)
74 peano2cnm 10549 . . . . . . . . . . . . . . . . . . . . . 22 (𝑃 ∈ ℂ → (𝑃 − 1) ∈ ℂ)
7573, 74syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑃 ∈ ℙ → (𝑃 − 1) ∈ ℂ)
7675adantl 467 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) → (𝑃 − 1) ∈ ℂ)
7776adantr 466 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (𝑃 − 1) ∈ ℂ)
78 simpr 471 . . . . . . . . . . . . . . . . . . . . 21 (((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
7968ad2antrr 705 . . . . . . . . . . . . . . . . . . . . 21 (((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (2↑(𝑁 + 1)) ∈ ℕ)
8078, 79nnmulcld 11270 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (𝑘 · (2↑(𝑁 + 1))) ∈ ℕ)
8180nncnd 11238 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (𝑘 · (2↑(𝑁 + 1))) ∈ ℂ)
82 2cnne0 11444 . . . . . . . . . . . . . . . . . . . 20 (2 ∈ ℂ ∧ 2 ≠ 0)
8382a1i 11 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (2 ∈ ℂ ∧ 2 ≠ 0))
84 divmul3 10892 . . . . . . . . . . . . . . . . . . 19 (((𝑃 − 1) ∈ ℂ ∧ (𝑘 · (2↑(𝑁 + 1))) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (((𝑃 − 1) / 2) = (𝑘 · (2↑(𝑁 + 1))) ↔ (𝑃 − 1) = ((𝑘 · (2↑(𝑁 + 1))) · 2)))
8577, 81, 83, 84syl3anc 1476 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (((𝑃 − 1) / 2) = (𝑘 · (2↑(𝑁 + 1))) ↔ (𝑃 − 1) = ((𝑘 · (2↑(𝑁 + 1))) · 2)))
86 nncn 11230 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
8786adantl 467 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℂ)
8868nncnd 11238 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ (ℤ‘2) → (2↑(𝑁 + 1)) ∈ ℂ)
8988ad2antrr 705 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (2↑(𝑁 + 1)) ∈ ℂ)
90 2cnd 11295 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 2 ∈ ℂ)
9187, 89, 90mulassd 10265 . . . . . . . . . . . . . . . . . . . . 21 (((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((𝑘 · (2↑(𝑁 + 1))) · 2) = (𝑘 · ((2↑(𝑁 + 1)) · 2)))
92 2cnd 11295 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑁 ∈ ℕ → 2 ∈ ℂ)
9365nnnn0d 11553 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℕ0)
9492, 93expp1d 13216 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ ℕ → (2↑((𝑁 + 1) + 1)) = ((2↑(𝑁 + 1)) · 2))
95 nncn 11230 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
96 add1p1 11485 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑁 ∈ ℂ → ((𝑁 + 1) + 1) = (𝑁 + 2))
9795, 96syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑁 ∈ ℕ → ((𝑁 + 1) + 1) = (𝑁 + 2))
9897oveq2d 6809 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ ℕ → (2↑((𝑁 + 1) + 1)) = (2↑(𝑁 + 2)))
9994, 98eqtr3d 2807 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ ℕ → ((2↑(𝑁 + 1)) · 2) = (2↑(𝑁 + 2)))
10057, 99syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ (ℤ‘2) → ((2↑(𝑁 + 1)) · 2) = (2↑(𝑁 + 2)))
101100ad2antrr 705 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((2↑(𝑁 + 1)) · 2) = (2↑(𝑁 + 2)))
102101oveq2d 6809 . . . . . . . . . . . . . . . . . . . . 21 (((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (𝑘 · ((2↑(𝑁 + 1)) · 2)) = (𝑘 · (2↑(𝑁 + 2))))
10391, 102eqtrd 2805 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((𝑘 · (2↑(𝑁 + 1))) · 2) = (𝑘 · (2↑(𝑁 + 2))))
104103eqeq2d 2781 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((𝑃 − 1) = ((𝑘 · (2↑(𝑁 + 1))) · 2) ↔ (𝑃 − 1) = (𝑘 · (2↑(𝑁 + 2)))))
10573adantl 467 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) → 𝑃 ∈ ℂ)
106105adantr 466 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 𝑃 ∈ ℂ)
107 1cnd 10258 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 1 ∈ ℂ)
108 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑁 ∈ ℕ → 𝑁 ∈ ℕ)
10924a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑁 ∈ ℕ → 2 ∈ ℕ)
110108, 109nnaddcld 11269 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑁 ∈ ℕ → (𝑁 + 2) ∈ ℕ)
111110nnnn0d 11553 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ ℕ → (𝑁 + 2) ∈ ℕ0)
11257, 111syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ (ℤ‘2) → (𝑁 + 2) ∈ ℕ0)
11364, 112nnexpcld 13237 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ (ℤ‘2) → (2↑(𝑁 + 2)) ∈ ℕ)
114113nncnd 11238 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁 ∈ (ℤ‘2) → (2↑(𝑁 + 2)) ∈ ℂ)
115114ad2antrr 705 . . . . . . . . . . . . . . . . . . . . 21 (((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (2↑(𝑁 + 2)) ∈ ℂ)
11687, 115mulcld 10262 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (𝑘 · (2↑(𝑁 + 2))) ∈ ℂ)
117106, 107, 116subadd2d 10613 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((𝑃 − 1) = (𝑘 · (2↑(𝑁 + 2))) ↔ ((𝑘 · (2↑(𝑁 + 2))) + 1) = 𝑃))
118 eqcom 2778 . . . . . . . . . . . . . . . . . . . 20 (((𝑘 · (2↑(𝑁 + 2))) + 1) = 𝑃𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1))
119118a1i 11 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (((𝑘 · (2↑(𝑁 + 2))) + 1) = 𝑃𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1)))
120104, 117, 1193bitrd 294 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((𝑃 − 1) = ((𝑘 · (2↑(𝑁 + 1))) · 2) ↔ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1)))
12172, 85, 1203bitrd 294 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((𝑘 · (2↑(𝑁 + 1))) = ((𝑃 − 1) / 2) ↔ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1)))
122121rexbidva 3197 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) → (∃𝑘 ∈ ℕ (𝑘 · (2↑(𝑁 + 1))) = ((𝑃 − 1) / 2) ↔ ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1)))
123122biimpd 219 . . . . . . . . . . . . . . 15 ((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) → (∃𝑘 ∈ ℕ (𝑘 · (2↑(𝑁 + 1))) = ((𝑃 − 1) / 2) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1)))
124123adantrr 696 . . . . . . . . . . . . . 14 ((𝑁 ∈ (ℤ‘2) ∧ (𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2)) → (∃𝑘 ∈ ℕ (𝑘 · (2↑(𝑁 + 1))) = ((𝑃 − 1) / 2) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1)))
12570, 124sylbid 230 . . . . . . . . . . . . 13 ((𝑁 ∈ (ℤ‘2) ∧ (𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2)) → ((2↑(𝑁 + 1)) ∥ ((𝑃 − 1) / 2) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1)))
126125expr 444 . . . . . . . . . . . 12 ((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) → (¬ 𝑃 = 2 → ((2↑(𝑁 + 1)) ∥ ((𝑃 − 1) / 2) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1))))
1271263adant3 1126 . . . . . . . . . . 11 ((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁)) → (¬ 𝑃 = 2 → ((2↑(𝑁 + 1)) ∥ ((𝑃 − 1) / 2) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1))))
128127impcom 394 . . . . . . . . . 10 ((¬ 𝑃 = 2 ∧ (𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) → ((2↑(𝑁 + 1)) ∥ ((𝑃 − 1) / 2) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1)))
129128adantr 466 . . . . . . . . 9 (((¬ 𝑃 = 2 ∧ (𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) ∧ ((od𝑃)‘2) = (2↑(𝑁 + 1))) → ((2↑(𝑁 + 1)) ∥ ((𝑃 − 1) / 2) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1)))
13063, 129sylbid 230 . . . . . . . 8 (((¬ 𝑃 = 2 ∧ (𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) ∧ ((od𝑃)‘2) = (2↑(𝑁 + 1))) → (((od𝑃)‘2) ∥ ((𝑃 − 1) / 2) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1)))
131130ex 397 . . . . . . 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 230 . . . . 5 ((¬ 𝑃 = 2 ∧ (𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) → (𝑃 ∥ ((2↑((𝑃 − 1) / 2)) − 1) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1)))
13436, 133sylbid 230 . . . 4 ((¬ 𝑃 = 2 ∧ (𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) → (((2↑((𝑃 − 1) / 2)) mod 𝑃) = 1 → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1)))
13522, 134mpd 15 . . 3 ((¬ 𝑃 = 2 ∧ (𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1))
136135ex 397 . 2 𝑃 = 2 → ((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1)))
13711, 136pm2.61i 176 1 ((𝑁 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 382   ∧ w3a 1071   = wceq 1631   ∈ wcel 2145   ≠ wne 2943  ∃wrex 3062   ∖ cdif 3720  {csn 4316   class class class wbr 4786  ‘cfv 6031  (class class class)co 6793  ℂcc 10136  0cc0 10138  1c1 10139   + caddc 10141   · cmul 10143   − cmin 10468   / cdiv 10886  ℕcn 11222  2c2 11272  ℕ0cn0 11494  ℤcz 11579  ℤ≥cuz 11888   mod cmo 12876  ↑cexp 13067   ∥ cdvds 15189   gcd cgcd 15424  ℙcprime 15592  odℤcodz 15675  FermatNocfmtno 41967 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-inf2 8702  ax-cnex 10194  ax-resscn 10195  ax-1cn 10196  ax-icn 10197  ax-addcl 10198  ax-addrcl 10199  ax-mulcl 10200  ax-mulrcl 10201  ax-mulcom 10202  ax-addass 10203  ax-mulass 10204  ax-distr 10205  ax-i2m1 10206  ax-1ne0 10207  ax-1rid 10208  ax-rnegex 10209  ax-rrecex 10210  ax-cnre 10211  ax-pre-lttri 10212  ax-pre-lttrn 10213  ax-pre-ltadd 10214  ax-pre-mulgt0 10215  ax-pre-sup 10216 This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-3or 1072  df-3an 1073  df-tru 1634  df-fal 1637  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-int 4612  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-se 5209  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-isom 6040  df-riota 6754  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-om 7213  df-1st 7315  df-2nd 7316  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-1o 7713  df-2o 7714  df-oadd 7717  df-er 7896  df-map 8011  df-en 8110  df-dom 8111  df-sdom 8112  df-fin 8113  df-sup 8504  df-inf 8505  df-oi 8571  df-card 8965  df-cda 9192  df-pnf 10278  df-mnf 10279  df-xr 10280  df-ltxr 10281  df-le 10282  df-sub 10470  df-neg 10471  df-div 10887  df-nn 11223  df-2 11281  df-3 11282  df-4 11283  df-5 11284  df-6 11285  df-7 11286  df-8 11287  df-n0 11495  df-xnn0 11566  df-z 11580  df-uz 11889  df-q 11992  df-rp 12036  df-ioo 12384  df-ico 12386  df-fz 12534  df-fzo 12674  df-fl 12801  df-mod 12877  df-seq 13009  df-exp 13068  df-fac 13265  df-hash 13322  df-cj 14047  df-re 14048  df-im 14049  df-sqrt 14183  df-abs 14184  df-clim 14427  df-prod 14843  df-dvds 15190  df-gcd 15425  df-prm 15593  df-odz 15677  df-phi 15678  df-pc 15749  df-lgs 25241  df-fmtno 41968 This theorem is referenced by:  fmtnofac2  42009  fmtno4prmfac  42012
 Copyright terms: Public domain W3C validator