# Metamath Proof Explorer

## Theorem fmtnoprmfac2

Description: Divisor of Fermat number (special form of Lucas' result, see fmtnofac2 ): Let F_n be a Fermat number. Let p be a prime divisor of F_n. Then p is in the form: k*2^(n+2)+1 where k is a positive integer. (Contributed by AV, 26-Jul-2021)

Ref Expression
Assertion fmtnoprmfac2 ${⊢}\left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\wedge {P}\parallel \mathrm{FermatNo}\left({N}\right)\right)\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{P}={k}{2}^{{N}+2}+1$

### Proof

Step Hyp Ref Expression
1 breq1 ${⊢}{P}=2\to \left({P}\parallel \mathrm{FermatNo}\left({N}\right)↔2\parallel \mathrm{FermatNo}\left({N}\right)\right)$
2 1 adantr ${⊢}\left({P}=2\wedge {N}\in {ℤ}_{\ge 2}\right)\to \left({P}\parallel \mathrm{FermatNo}\left({N}\right)↔2\parallel \mathrm{FermatNo}\left({N}\right)\right)$
3 eluzge2nn0 ${⊢}{N}\in {ℤ}_{\ge 2}\to {N}\in {ℕ}_{0}$
4 fmtnoodd ${⊢}{N}\in {ℕ}_{0}\to ¬2\parallel \mathrm{FermatNo}\left({N}\right)$
5 3 4 syl ${⊢}{N}\in {ℤ}_{\ge 2}\to ¬2\parallel \mathrm{FermatNo}\left({N}\right)$
6 5 adantl ${⊢}\left({P}=2\wedge {N}\in {ℤ}_{\ge 2}\right)\to ¬2\parallel \mathrm{FermatNo}\left({N}\right)$
7 6 pm2.21d ${⊢}\left({P}=2\wedge {N}\in {ℤ}_{\ge 2}\right)\to \left(2\parallel \mathrm{FermatNo}\left({N}\right)\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{P}={k}{2}^{{N}+2}+1\right)$
8 2 7 sylbid ${⊢}\left({P}=2\wedge {N}\in {ℤ}_{\ge 2}\right)\to \left({P}\parallel \mathrm{FermatNo}\left({N}\right)\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{P}={k}{2}^{{N}+2}+1\right)$
9 8 a1d ${⊢}\left({P}=2\wedge {N}\in {ℤ}_{\ge 2}\right)\to \left({P}\in ℙ\to \left({P}\parallel \mathrm{FermatNo}\left({N}\right)\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{P}={k}{2}^{{N}+2}+1\right)\right)$
10 9 ex ${⊢}{P}=2\to \left({N}\in {ℤ}_{\ge 2}\to \left({P}\in ℙ\to \left({P}\parallel \mathrm{FermatNo}\left({N}\right)\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{P}={k}{2}^{{N}+2}+1\right)\right)\right)$
11 10 3impd ${⊢}{P}=2\to \left(\left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\wedge {P}\parallel \mathrm{FermatNo}\left({N}\right)\right)\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{P}={k}{2}^{{N}+2}+1\right)$
12 simpr1 ${⊢}\left(¬{P}=2\wedge \left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\wedge {P}\parallel \mathrm{FermatNo}\left({N}\right)\right)\right)\to {N}\in {ℤ}_{\ge 2}$
13 neqne ${⊢}¬{P}=2\to {P}\ne 2$
14 13 anim2i ${⊢}\left({P}\in ℙ\wedge ¬{P}=2\right)\to \left({P}\in ℙ\wedge {P}\ne 2\right)$
15 eldifsn ${⊢}{P}\in \left(ℙ\setminus \left\{2\right\}\right)↔\left({P}\in ℙ\wedge {P}\ne 2\right)$
16 14 15 sylibr ${⊢}\left({P}\in ℙ\wedge ¬{P}=2\right)\to {P}\in \left(ℙ\setminus \left\{2\right\}\right)$
17 16 ex ${⊢}{P}\in ℙ\to \left(¬{P}=2\to {P}\in \left(ℙ\setminus \left\{2\right\}\right)\right)$
18 17 3ad2ant2 ${⊢}\left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\wedge {P}\parallel \mathrm{FermatNo}\left({N}\right)\right)\to \left(¬{P}=2\to {P}\in \left(ℙ\setminus \left\{2\right\}\right)\right)$
19 18 impcom ${⊢}\left(¬{P}=2\wedge \left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\wedge {P}\parallel \mathrm{FermatNo}\left({N}\right)\right)\right)\to {P}\in \left(ℙ\setminus \left\{2\right\}\right)$
20 simpr3 ${⊢}\left(¬{P}=2\wedge \left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\wedge {P}\parallel \mathrm{FermatNo}\left({N}\right)\right)\right)\to {P}\parallel \mathrm{FermatNo}\left({N}\right)$
21 fmtnoprmfac2lem1 ${⊢}\left({N}\in {ℤ}_{\ge 2}\wedge {P}\in \left(ℙ\setminus \left\{2\right\}\right)\wedge {P}\parallel \mathrm{FermatNo}\left({N}\right)\right)\to {2}^{\frac{{P}-1}{2}}\mathrm{mod}{P}=1$
22 12 19 20 21 syl3anc ${⊢}\left(¬{P}=2\wedge \left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\wedge {P}\parallel \mathrm{FermatNo}\left({N}\right)\right)\right)\to {2}^{\frac{{P}-1}{2}}\mathrm{mod}{P}=1$
23 simpl ${⊢}\left({P}\in ℙ\wedge ¬{P}=2\right)\to {P}\in ℙ$
24 2nn ${⊢}2\in ℕ$
25 24 a1i ${⊢}\left({P}\in ℙ\wedge ¬{P}=2\right)\to 2\in ℕ$
26 oddprm ${⊢}{P}\in \left(ℙ\setminus \left\{2\right\}\right)\to \frac{{P}-1}{2}\in ℕ$
27 16 26 syl ${⊢}\left({P}\in ℙ\wedge ¬{P}=2\right)\to \frac{{P}-1}{2}\in ℕ$
28 27 nnnn0d ${⊢}\left({P}\in ℙ\wedge ¬{P}=2\right)\to \frac{{P}-1}{2}\in {ℕ}_{0}$
29 25 28 nnexpcld ${⊢}\left({P}\in ℙ\wedge ¬{P}=2\right)\to {2}^{\frac{{P}-1}{2}}\in ℕ$
30 29 nnzd ${⊢}\left({P}\in ℙ\wedge ¬{P}=2\right)\to {2}^{\frac{{P}-1}{2}}\in ℤ$
31 23 30 jca ${⊢}\left({P}\in ℙ\wedge ¬{P}=2\right)\to \left({P}\in ℙ\wedge {2}^{\frac{{P}-1}{2}}\in ℤ\right)$
32 31 ex ${⊢}{P}\in ℙ\to \left(¬{P}=2\to \left({P}\in ℙ\wedge {2}^{\frac{{P}-1}{2}}\in ℤ\right)\right)$
33 32 3ad2ant2 ${⊢}\left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\wedge {P}\parallel \mathrm{FermatNo}\left({N}\right)\right)\to \left(¬{P}=2\to \left({P}\in ℙ\wedge {2}^{\frac{{P}-1}{2}}\in ℤ\right)\right)$
34 33 impcom ${⊢}\left(¬{P}=2\wedge \left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\wedge {P}\parallel \mathrm{FermatNo}\left({N}\right)\right)\right)\to \left({P}\in ℙ\wedge {2}^{\frac{{P}-1}{2}}\in ℤ\right)$
35 modprm1div ${⊢}\left({P}\in ℙ\wedge {2}^{\frac{{P}-1}{2}}\in ℤ\right)\to \left({2}^{\frac{{P}-1}{2}}\mathrm{mod}{P}=1↔{P}\parallel \left({2}^{\frac{{P}-1}{2}}-1\right)\right)$
36 34 35 syl ${⊢}\left(¬{P}=2\wedge \left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\wedge {P}\parallel \mathrm{FermatNo}\left({N}\right)\right)\right)\to \left({2}^{\frac{{P}-1}{2}}\mathrm{mod}{P}=1↔{P}\parallel \left({2}^{\frac{{P}-1}{2}}-1\right)\right)$
37 prmnn ${⊢}{P}\in ℙ\to {P}\in ℕ$
38 37 adantr ${⊢}\left({P}\in ℙ\wedge ¬{P}=2\right)\to {P}\in ℕ$
39 2z ${⊢}2\in ℤ$
40 39 a1i ${⊢}\left({P}\in ℙ\wedge ¬{P}=2\right)\to 2\in ℤ$
41 13 necomd ${⊢}¬{P}=2\to 2\ne {P}$
42 41 adantl ${⊢}\left({P}\in ℙ\wedge ¬{P}=2\right)\to 2\ne {P}$
43 2prm ${⊢}2\in ℙ$
44 43 a1i ${⊢}¬{P}=2\to 2\in ℙ$
45 44 anim2i ${⊢}\left({P}\in ℙ\wedge ¬{P}=2\right)\to \left({P}\in ℙ\wedge 2\in ℙ\right)$
46 45 ancomd ${⊢}\left({P}\in ℙ\wedge ¬{P}=2\right)\to \left(2\in ℙ\wedge {P}\in ℙ\right)$
47 prmrp ${⊢}\left(2\in ℙ\wedge {P}\in ℙ\right)\to \left(2\mathrm{gcd}{P}=1↔2\ne {P}\right)$
48 46 47 syl ${⊢}\left({P}\in ℙ\wedge ¬{P}=2\right)\to \left(2\mathrm{gcd}{P}=1↔2\ne {P}\right)$
49 42 48 mpbird ${⊢}\left({P}\in ℙ\wedge ¬{P}=2\right)\to 2\mathrm{gcd}{P}=1$
50 38 40 49 3jca ${⊢}\left({P}\in ℙ\wedge ¬{P}=2\right)\to \left({P}\in ℕ\wedge 2\in ℤ\wedge 2\mathrm{gcd}{P}=1\right)$
51 50 28 jca ${⊢}\left({P}\in ℙ\wedge ¬{P}=2\right)\to \left(\left({P}\in ℕ\wedge 2\in ℤ\wedge 2\mathrm{gcd}{P}=1\right)\wedge \frac{{P}-1}{2}\in {ℕ}_{0}\right)$
52 51 ex ${⊢}{P}\in ℙ\to \left(¬{P}=2\to \left(\left({P}\in ℕ\wedge 2\in ℤ\wedge 2\mathrm{gcd}{P}=1\right)\wedge \frac{{P}-1}{2}\in {ℕ}_{0}\right)\right)$
53 52 3ad2ant2 ${⊢}\left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\wedge {P}\parallel \mathrm{FermatNo}\left({N}\right)\right)\to \left(¬{P}=2\to \left(\left({P}\in ℕ\wedge 2\in ℤ\wedge 2\mathrm{gcd}{P}=1\right)\wedge \frac{{P}-1}{2}\in {ℕ}_{0}\right)\right)$
54 53 impcom ${⊢}\left(¬{P}=2\wedge \left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\wedge {P}\parallel \mathrm{FermatNo}\left({N}\right)\right)\right)\to \left(\left({P}\in ℕ\wedge 2\in ℤ\wedge 2\mathrm{gcd}{P}=1\right)\wedge \frac{{P}-1}{2}\in {ℕ}_{0}\right)$
55 odzdvds ${⊢}\left(\left({P}\in ℕ\wedge 2\in ℤ\wedge 2\mathrm{gcd}{P}=1\right)\wedge \frac{{P}-1}{2}\in {ℕ}_{0}\right)\to \left({P}\parallel \left({2}^{\frac{{P}-1}{2}}-1\right)↔{\mathrm{od}}_{ℤ}\left({P}\right)\left(2\right)\parallel \left(\frac{{P}-1}{2}\right)\right)$
56 54 55 syl ${⊢}\left(¬{P}=2\wedge \left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\wedge {P}\parallel \mathrm{FermatNo}\left({N}\right)\right)\right)\to \left({P}\parallel \left({2}^{\frac{{P}-1}{2}}-1\right)↔{\mathrm{od}}_{ℤ}\left({P}\right)\left(2\right)\parallel \left(\frac{{P}-1}{2}\right)\right)$
57 eluz2nn ${⊢}{N}\in {ℤ}_{\ge 2}\to {N}\in ℕ$
58 57 3ad2ant1 ${⊢}\left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\wedge {P}\parallel \mathrm{FermatNo}\left({N}\right)\right)\to {N}\in ℕ$
59 58 adantl ${⊢}\left(¬{P}=2\wedge \left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\wedge {P}\parallel \mathrm{FermatNo}\left({N}\right)\right)\right)\to {N}\in ℕ$
60 fmtnoprmfac1lem ${⊢}\left({N}\in ℕ\wedge {P}\in \left(ℙ\setminus \left\{2\right\}\right)\wedge {P}\parallel \mathrm{FermatNo}\left({N}\right)\right)\to {\mathrm{od}}_{ℤ}\left({P}\right)\left(2\right)={2}^{{N}+1}$
61 59 19 20 60 syl3anc ${⊢}\left(¬{P}=2\wedge \left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\wedge {P}\parallel \mathrm{FermatNo}\left({N}\right)\right)\right)\to {\mathrm{od}}_{ℤ}\left({P}\right)\left(2\right)={2}^{{N}+1}$
62 breq1 ${⊢}{\mathrm{od}}_{ℤ}\left({P}\right)\left(2\right)={2}^{{N}+1}\to \left({\mathrm{od}}_{ℤ}\left({P}\right)\left(2\right)\parallel \left(\frac{{P}-1}{2}\right)↔{2}^{{N}+1}\parallel \left(\frac{{P}-1}{2}\right)\right)$
63 62 adantl ${⊢}\left(\left(¬{P}=2\wedge \left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\wedge {P}\parallel \mathrm{FermatNo}\left({N}\right)\right)\right)\wedge {\mathrm{od}}_{ℤ}\left({P}\right)\left(2\right)={2}^{{N}+1}\right)\to \left({\mathrm{od}}_{ℤ}\left({P}\right)\left(2\right)\parallel \left(\frac{{P}-1}{2}\right)↔{2}^{{N}+1}\parallel \left(\frac{{P}-1}{2}\right)\right)$
64 24 a1i ${⊢}{N}\in {ℤ}_{\ge 2}\to 2\in ℕ$
65 peano2nn ${⊢}{N}\in ℕ\to {N}+1\in ℕ$
66 57 65 syl ${⊢}{N}\in {ℤ}_{\ge 2}\to {N}+1\in ℕ$
67 66 nnnn0d ${⊢}{N}\in {ℤ}_{\ge 2}\to {N}+1\in {ℕ}_{0}$
68 64 67 nnexpcld ${⊢}{N}\in {ℤ}_{\ge 2}\to {2}^{{N}+1}\in ℕ$
69 nndivides ${⊢}\left({2}^{{N}+1}\in ℕ\wedge \frac{{P}-1}{2}\in ℕ\right)\to \left({2}^{{N}+1}\parallel \left(\frac{{P}-1}{2}\right)↔\exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{k}{2}^{{N}+1}=\frac{{P}-1}{2}\right)$
70 68 27 69 syl2an ${⊢}\left({N}\in {ℤ}_{\ge 2}\wedge \left({P}\in ℙ\wedge ¬{P}=2\right)\right)\to \left({2}^{{N}+1}\parallel \left(\frac{{P}-1}{2}\right)↔\exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{k}{2}^{{N}+1}=\frac{{P}-1}{2}\right)$
71 eqcom ${⊢}{k}{2}^{{N}+1}=\frac{{P}-1}{2}↔\frac{{P}-1}{2}={k}{2}^{{N}+1}$
72 71 a1i ${⊢}\left(\left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\right)\wedge {k}\in ℕ\right)\to \left({k}{2}^{{N}+1}=\frac{{P}-1}{2}↔\frac{{P}-1}{2}={k}{2}^{{N}+1}\right)$
73 37 nncnd ${⊢}{P}\in ℙ\to {P}\in ℂ$
74 peano2cnm ${⊢}{P}\in ℂ\to {P}-1\in ℂ$
75 73 74 syl ${⊢}{P}\in ℙ\to {P}-1\in ℂ$
76 75 adantl ${⊢}\left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\right)\to {P}-1\in ℂ$
77 76 adantr ${⊢}\left(\left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\right)\wedge {k}\in ℕ\right)\to {P}-1\in ℂ$
78 simpr ${⊢}\left(\left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\right)\wedge {k}\in ℕ\right)\to {k}\in ℕ$
79 68 ad2antrr ${⊢}\left(\left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\right)\wedge {k}\in ℕ\right)\to {2}^{{N}+1}\in ℕ$
80 78 79 nnmulcld ${⊢}\left(\left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\right)\wedge {k}\in ℕ\right)\to {k}{2}^{{N}+1}\in ℕ$
81 80 nncnd ${⊢}\left(\left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\right)\wedge {k}\in ℕ\right)\to {k}{2}^{{N}+1}\in ℂ$
82 2cnne0 ${⊢}\left(2\in ℂ\wedge 2\ne 0\right)$
83 82 a1i ${⊢}\left(\left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\right)\wedge {k}\in ℕ\right)\to \left(2\in ℂ\wedge 2\ne 0\right)$
84 divmul3 ${⊢}\left({P}-1\in ℂ\wedge {k}{2}^{{N}+1}\in ℂ\wedge \left(2\in ℂ\wedge 2\ne 0\right)\right)\to \left(\frac{{P}-1}{2}={k}{2}^{{N}+1}↔{P}-1={k}{2}^{{N}+1}\cdot 2\right)$
85 77 81 83 84 syl3anc ${⊢}\left(\left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\right)\wedge {k}\in ℕ\right)\to \left(\frac{{P}-1}{2}={k}{2}^{{N}+1}↔{P}-1={k}{2}^{{N}+1}\cdot 2\right)$
86 nncn ${⊢}{k}\in ℕ\to {k}\in ℂ$
87 86 adantl ${⊢}\left(\left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\right)\wedge {k}\in ℕ\right)\to {k}\in ℂ$
88 68 nncnd ${⊢}{N}\in {ℤ}_{\ge 2}\to {2}^{{N}+1}\in ℂ$
89 88 ad2antrr ${⊢}\left(\left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\right)\wedge {k}\in ℕ\right)\to {2}^{{N}+1}\in ℂ$
90 2cnd ${⊢}\left(\left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\right)\wedge {k}\in ℕ\right)\to 2\in ℂ$
91 87 89 90 mulassd ${⊢}\left(\left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\right)\wedge {k}\in ℕ\right)\to {k}{2}^{{N}+1}\cdot 2={k}{2}^{{N}+1}\cdot 2$
92 2cnd ${⊢}{N}\in ℕ\to 2\in ℂ$
93 65 nnnn0d ${⊢}{N}\in ℕ\to {N}+1\in {ℕ}_{0}$
94 92 93 expp1d ${⊢}{N}\in ℕ\to {2}^{{N}+1+1}={2}^{{N}+1}\cdot 2$
95 nncn ${⊢}{N}\in ℕ\to {N}\in ℂ$
96 add1p1 ${⊢}{N}\in ℂ\to {N}+1+1={N}+2$
97 95 96 syl ${⊢}{N}\in ℕ\to {N}+1+1={N}+2$
98 97 oveq2d ${⊢}{N}\in ℕ\to {2}^{{N}+1+1}={2}^{{N}+2}$
99 94 98 eqtr3d ${⊢}{N}\in ℕ\to {2}^{{N}+1}\cdot 2={2}^{{N}+2}$
100 57 99 syl ${⊢}{N}\in {ℤ}_{\ge 2}\to {2}^{{N}+1}\cdot 2={2}^{{N}+2}$
101 100 ad2antrr ${⊢}\left(\left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\right)\wedge {k}\in ℕ\right)\to {2}^{{N}+1}\cdot 2={2}^{{N}+2}$
102 101 oveq2d ${⊢}\left(\left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\right)\wedge {k}\in ℕ\right)\to {k}{2}^{{N}+1}\cdot 2={k}{2}^{{N}+2}$
103 91 102 eqtrd ${⊢}\left(\left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\right)\wedge {k}\in ℕ\right)\to {k}{2}^{{N}+1}\cdot 2={k}{2}^{{N}+2}$
104 103 eqeq2d ${⊢}\left(\left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\right)\wedge {k}\in ℕ\right)\to \left({P}-1={k}{2}^{{N}+1}\cdot 2↔{P}-1={k}{2}^{{N}+2}\right)$
105 73 adantl ${⊢}\left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\right)\to {P}\in ℂ$
106 105 adantr ${⊢}\left(\left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\right)\wedge {k}\in ℕ\right)\to {P}\in ℂ$
107 1cnd ${⊢}\left(\left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\right)\wedge {k}\in ℕ\right)\to 1\in ℂ$
108 id ${⊢}{N}\in ℕ\to {N}\in ℕ$
109 24 a1i ${⊢}{N}\in ℕ\to 2\in ℕ$
110 108 109 nnaddcld ${⊢}{N}\in ℕ\to {N}+2\in ℕ$
111 110 nnnn0d ${⊢}{N}\in ℕ\to {N}+2\in {ℕ}_{0}$
112 57 111 syl ${⊢}{N}\in {ℤ}_{\ge 2}\to {N}+2\in {ℕ}_{0}$
113 64 112 nnexpcld ${⊢}{N}\in {ℤ}_{\ge 2}\to {2}^{{N}+2}\in ℕ$
114 113 nncnd ${⊢}{N}\in {ℤ}_{\ge 2}\to {2}^{{N}+2}\in ℂ$
115 114 ad2antrr ${⊢}\left(\left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\right)\wedge {k}\in ℕ\right)\to {2}^{{N}+2}\in ℂ$
116 87 115 mulcld ${⊢}\left(\left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\right)\wedge {k}\in ℕ\right)\to {k}{2}^{{N}+2}\in ℂ$
117 106 107 116 subadd2d ${⊢}\left(\left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\right)\wedge {k}\in ℕ\right)\to \left({P}-1={k}{2}^{{N}+2}↔{k}{2}^{{N}+2}+1={P}\right)$
118 eqcom ${⊢}{k}{2}^{{N}+2}+1={P}↔{P}={k}{2}^{{N}+2}+1$
119 118 a1i ${⊢}\left(\left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\right)\wedge {k}\in ℕ\right)\to \left({k}{2}^{{N}+2}+1={P}↔{P}={k}{2}^{{N}+2}+1\right)$
120 104 117 119 3bitrd ${⊢}\left(\left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\right)\wedge {k}\in ℕ\right)\to \left({P}-1={k}{2}^{{N}+1}\cdot 2↔{P}={k}{2}^{{N}+2}+1\right)$
121 72 85 120 3bitrd ${⊢}\left(\left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\right)\wedge {k}\in ℕ\right)\to \left({k}{2}^{{N}+1}=\frac{{P}-1}{2}↔{P}={k}{2}^{{N}+2}+1\right)$
122 121 rexbidva ${⊢}\left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\right)\to \left(\exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{k}{2}^{{N}+1}=\frac{{P}-1}{2}↔\exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{P}={k}{2}^{{N}+2}+1\right)$
123 122 biimpd ${⊢}\left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\right)\to \left(\exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{k}{2}^{{N}+1}=\frac{{P}-1}{2}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{P}={k}{2}^{{N}+2}+1\right)$
124 123 adantrr ${⊢}\left({N}\in {ℤ}_{\ge 2}\wedge \left({P}\in ℙ\wedge ¬{P}=2\right)\right)\to \left(\exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{k}{2}^{{N}+1}=\frac{{P}-1}{2}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{P}={k}{2}^{{N}+2}+1\right)$
125 70 124 sylbid ${⊢}\left({N}\in {ℤ}_{\ge 2}\wedge \left({P}\in ℙ\wedge ¬{P}=2\right)\right)\to \left({2}^{{N}+1}\parallel \left(\frac{{P}-1}{2}\right)\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{P}={k}{2}^{{N}+2}+1\right)$
126 125 expr ${⊢}\left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\right)\to \left(¬{P}=2\to \left({2}^{{N}+1}\parallel \left(\frac{{P}-1}{2}\right)\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{P}={k}{2}^{{N}+2}+1\right)\right)$
127 126 3adant3 ${⊢}\left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\wedge {P}\parallel \mathrm{FermatNo}\left({N}\right)\right)\to \left(¬{P}=2\to \left({2}^{{N}+1}\parallel \left(\frac{{P}-1}{2}\right)\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{P}={k}{2}^{{N}+2}+1\right)\right)$
128 127 impcom ${⊢}\left(¬{P}=2\wedge \left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\wedge {P}\parallel \mathrm{FermatNo}\left({N}\right)\right)\right)\to \left({2}^{{N}+1}\parallel \left(\frac{{P}-1}{2}\right)\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{P}={k}{2}^{{N}+2}+1\right)$
129 128 adantr ${⊢}\left(\left(¬{P}=2\wedge \left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\wedge {P}\parallel \mathrm{FermatNo}\left({N}\right)\right)\right)\wedge {\mathrm{od}}_{ℤ}\left({P}\right)\left(2\right)={2}^{{N}+1}\right)\to \left({2}^{{N}+1}\parallel \left(\frac{{P}-1}{2}\right)\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{P}={k}{2}^{{N}+2}+1\right)$
130 63 129 sylbid ${⊢}\left(\left(¬{P}=2\wedge \left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\wedge {P}\parallel \mathrm{FermatNo}\left({N}\right)\right)\right)\wedge {\mathrm{od}}_{ℤ}\left({P}\right)\left(2\right)={2}^{{N}+1}\right)\to \left({\mathrm{od}}_{ℤ}\left({P}\right)\left(2\right)\parallel \left(\frac{{P}-1}{2}\right)\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{P}={k}{2}^{{N}+2}+1\right)$
131 130 ex ${⊢}\left(¬{P}=2\wedge \left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\wedge {P}\parallel \mathrm{FermatNo}\left({N}\right)\right)\right)\to \left({\mathrm{od}}_{ℤ}\left({P}\right)\left(2\right)={2}^{{N}+1}\to \left({\mathrm{od}}_{ℤ}\left({P}\right)\left(2\right)\parallel \left(\frac{{P}-1}{2}\right)\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{P}={k}{2}^{{N}+2}+1\right)\right)$
132 61 131 mpd ${⊢}\left(¬{P}=2\wedge \left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\wedge {P}\parallel \mathrm{FermatNo}\left({N}\right)\right)\right)\to \left({\mathrm{od}}_{ℤ}\left({P}\right)\left(2\right)\parallel \left(\frac{{P}-1}{2}\right)\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{P}={k}{2}^{{N}+2}+1\right)$
133 56 132 sylbid ${⊢}\left(¬{P}=2\wedge \left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\wedge {P}\parallel \mathrm{FermatNo}\left({N}\right)\right)\right)\to \left({P}\parallel \left({2}^{\frac{{P}-1}{2}}-1\right)\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{P}={k}{2}^{{N}+2}+1\right)$
134 36 133 sylbid ${⊢}\left(¬{P}=2\wedge \left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\wedge {P}\parallel \mathrm{FermatNo}\left({N}\right)\right)\right)\to \left({2}^{\frac{{P}-1}{2}}\mathrm{mod}{P}=1\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{P}={k}{2}^{{N}+2}+1\right)$
135 22 134 mpd ${⊢}\left(¬{P}=2\wedge \left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\wedge {P}\parallel \mathrm{FermatNo}\left({N}\right)\right)\right)\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{P}={k}{2}^{{N}+2}+1$
136 135 ex ${⊢}¬{P}=2\to \left(\left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\wedge {P}\parallel \mathrm{FermatNo}\left({N}\right)\right)\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{P}={k}{2}^{{N}+2}+1\right)$
137 11 136 pm2.61i ${⊢}\left({N}\in {ℤ}_{\ge 2}\wedge {P}\in ℙ\wedge {P}\parallel \mathrm{FermatNo}\left({N}\right)\right)\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{P}={k}{2}^{{N}+2}+1$