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	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) → ∃ 𝑘 ∈ ℕ 𝑃 = ( ( 𝑘 · ( 2 ↑ ( 𝑁 + 2 ) ) ) + 1 ) )

Proof

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