fmtnoprmfac1lem

Description: Lemma for fmtnoprmfac1 : The order of 2 modulo a prime that divides the n-th Fermat number is 2^(n+1). (Contributed by AV, 25-Jul-2021) (Proof shortened by AV, 18-Mar-2022)

		Ref	Expression
	Assertion	fmtnoprmfac1lem	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\}) \land P ∥ FermatNo (N)) \to {od}_{ℤ} (P) (2) = 2^{N + 1}$

Proof

Step	Hyp	Ref	Expression
1		eldifi	$⊢ P \in (ℙ ∖ \{2\}) \to P \in ℙ$
2		prmnn	$⊢ P \in ℙ \to P \in ℕ$
3	1 2	syl	$⊢ P \in (ℙ ∖ \{2\}) \to P \in ℕ$
4	3	ad2antlr	$⊢ ((N \in ℕ \land P \in (ℙ ∖ \{2\})) \land P ∥ FermatNo (N)) \to P \in ℕ$
5		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
6		fmtno	$⊢ N \in ℕ_{0} \to FermatNo (N) = 2^{2^{N}} + 1$
7	5 6	syl	$⊢ N \in ℕ \to FermatNo (N) = 2^{2^{N}} + 1$
8	7	breq2d	$⊢ N \in ℕ \to (P ∥ FermatNo (N) \leftrightarrow P ∥ (2^{2^{N}} + 1))$
9	8	adantr	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to (P ∥ FermatNo (N) \leftrightarrow P ∥ (2^{2^{N}} + 1))$
10	9	biimpa	$⊢ ((N \in ℕ \land P \in (ℙ ∖ \{2\})) \land P ∥ FermatNo (N)) \to P ∥ (2^{2^{N}} + 1)$
11		dvdsmod0	$⊢ (P \in ℕ \land P ∥ (2^{2^{N}} + 1)) \to (2^{2^{N}} + 1) \mod P = 0$
12	4 10 11	syl2anc	$⊢ ((N \in ℕ \land P \in (ℙ ∖ \{2\})) \land P ∥ FermatNo (N)) \to (2^{2^{N}} + 1) \mod P = 0$
13	12	ex	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to (P ∥ FermatNo (N) \to (2^{2^{N}} + 1) \mod P = 0)$
14		2nn	$⊢ 2 \in ℕ$
15	14	a1i	$⊢ N \in ℕ \to 2 \in ℕ$
16		2nn0	$⊢ 2 \in ℕ_{0}$
17	16	a1i	$⊢ N \in ℕ \to 2 \in ℕ_{0}$
18	17 5	nn0expcld	$⊢ N \in ℕ \to 2^{N} \in ℕ_{0}$
19	15 18	nnexpcld	$⊢ N \in ℕ \to 2^{2^{N}} \in ℕ$
20	19	nnzd	$⊢ N \in ℕ \to 2^{2^{N}} \in ℤ$
21	20	adantr	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to 2^{2^{N}} \in ℤ$
22		1zzd	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to 1 \in ℤ$
23	3	adantl	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to P \in ℕ$
24		summodnegmod	$⊢ (2^{2^{N}} \in ℤ \land 1 \in ℤ \land P \in ℕ) \to ((2^{2^{N}} + 1) \mod P = 0 \leftrightarrow 2^{2^{N}} \mod P = -1 \mod P)$
25	21 22 23 24	syl3anc	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to ((2^{2^{N}} + 1) \mod P = 0 \leftrightarrow 2^{2^{N}} \mod P = -1 \mod P)$
26		neg1z	$⊢ - 1 \in ℤ$
27	21 26	jctir	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to (2^{2^{N}} \in ℤ \land - 1 \in ℤ)$
28	27	adantr	$⊢ ((N \in ℕ \land P \in (ℙ ∖ \{2\})) \land 2^{2^{N}} \mod P = -1 \mod P) \to (2^{2^{N}} \in ℤ \land - 1 \in ℤ)$
29	2	nnrpd	$⊢ P \in ℙ \to P \in ℝ^{+}$
30	1 29	syl	$⊢ P \in (ℙ ∖ \{2\}) \to P \in ℝ^{+}$
31	17 30	anim12i	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to (2 \in ℕ_{0} \land P \in ℝ^{+})$
32	31	adantr	$⊢ ((N \in ℕ \land P \in (ℙ ∖ \{2\})) \land 2^{2^{N}} \mod P = -1 \mod P) \to (2 \in ℕ_{0} \land P \in ℝ^{+})$
33		simpr	$⊢ ((N \in ℕ \land P \in (ℙ ∖ \{2\})) \land 2^{2^{N}} \mod P = -1 \mod P) \to 2^{2^{N}} \mod P = -1 \mod P$
34		modexp	$⊢ ((2^{2^{N}} \in ℤ \land - 1 \in ℤ) \land (2 \in ℕ_{0} \land P \in ℝ^{+}) \land 2^{2^{N}} \mod P = -1 \mod P) \to {(2^{2^{N}})}^{2} \mod P = {(- 1)}^{2} \mod P$
35	28 32 33 34	syl3anc	$⊢ ((N \in ℕ \land P \in (ℙ ∖ \{2\})) \land 2^{2^{N}} \mod P = -1 \mod P) \to {(2^{2^{N}})}^{2} \mod P = {(- 1)}^{2} \mod P$
36	35	ex	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to (2^{2^{N}} \mod P = -1 \mod P \to {(2^{2^{N}})}^{2} \mod P = {(- 1)}^{2} \mod P)$
37		2cnd	$⊢ N \in ℕ \to 2 \in ℂ$
38	37 18 17	3jca	$⊢ N \in ℕ \to (2 \in ℂ \land 2^{N} \in ℕ_{0} \land 2 \in ℕ_{0})$
39	38	adantr	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to (2 \in ℂ \land 2^{N} \in ℕ_{0} \land 2 \in ℕ_{0})$
40		expmul	$⊢ (2 \in ℂ \land 2^{N} \in ℕ_{0} \land 2 \in ℕ_{0}) \to 2^{2^{N} \cdot 2} = {(2^{2^{N}})}^{2}$
41	39 40	syl	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to 2^{2^{N} \cdot 2} = {(2^{2^{N}})}^{2}$
42		2cnd	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to 2 \in ℂ$
43	5	adantr	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to N \in ℕ_{0}$
44	42 43	expp1d	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to 2^{N + 1} = 2^{N} \cdot 2$
45	44	eqcomd	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to 2^{N} \cdot 2 = 2^{N + 1}$
46	45	oveq2d	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to 2^{2^{N} \cdot 2} = 2^{2^{N + 1}}$
47	41 46	eqtr3d	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to {(2^{2^{N}})}^{2} = 2^{2^{N + 1}}$
48	47	oveq1d	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to {(2^{2^{N}})}^{2} \mod P = 2^{2^{N + 1}} \mod P$
49		neg1sqe1	$⊢ {(- 1)}^{2} = 1$
50	49	a1i	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to {(- 1)}^{2} = 1$
51	50	oveq1d	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to {(- 1)}^{2} \mod P = 1 \mod P$
52	3	nnred	$⊢ P \in (ℙ ∖ \{2\}) \to P \in ℝ$
53		prmgt1	$⊢ P \in ℙ \to 1 < P$
54	1 53	syl	$⊢ P \in (ℙ ∖ \{2\}) \to 1 < P$
55		1mod	$⊢ (P \in ℝ \land 1 < P) \to 1 \mod P = 1$
56	52 54 55	syl2anc	$⊢ P \in (ℙ ∖ \{2\}) \to 1 \mod P = 1$
57	56	adantl	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to 1 \mod P = 1$
58	51 57	eqtrd	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to {(- 1)}^{2} \mod P = 1$
59	48 58	eqeq12d	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to ({(2^{2^{N}})}^{2} \mod P = {(- 1)}^{2} \mod P \leftrightarrow 2^{2^{N + 1}} \mod P = 1)$
60		simpll	$⊢ (((N \in ℕ \land P \in (ℙ ∖ \{2\})) \land 2^{2^{N + 1}} \mod P = 1) \land (2^{2^{N}} + 1) \mod P = 0) \to (N \in ℕ \land P \in (ℙ ∖ \{2\}))$
61	20	adantr	$⊢ (N \in ℕ \land P \in ℙ) \to 2^{2^{N}} \in ℤ$
62		1zzd	$⊢ (N \in ℕ \land P \in ℙ) \to 1 \in ℤ$
63	2	adantl	$⊢ (N \in ℕ \land P \in ℙ) \to P \in ℕ$
64	61 62 63	3jca	$⊢ (N \in ℕ \land P \in ℙ) \to (2^{2^{N}} \in ℤ \land 1 \in ℤ \land P \in ℕ)$
65	1 64	sylan2	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to (2^{2^{N}} \in ℤ \land 1 \in ℤ \land P \in ℕ)$
66	65	adantr	$⊢ ((N \in ℕ \land P \in (ℙ ∖ \{2\})) \land 2^{2^{N + 1}} \mod P = 1) \to (2^{2^{N}} \in ℤ \land 1 \in ℤ \land P \in ℕ)$
67	66 24	syl	$⊢ ((N \in ℕ \land P \in (ℙ ∖ \{2\})) \land 2^{2^{N + 1}} \mod P = 1) \to ((2^{2^{N}} + 1) \mod P = 0 \leftrightarrow 2^{2^{N}} \mod P = -1 \mod P)$
68		m1modnnsub1	$⊢ P \in ℕ \to -1 \mod P = P - 1$
69	23 68	syl	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to -1 \mod P = P - 1$
70		eldifsni	$⊢ P \in (ℙ ∖ \{2\}) \to P \neq 2$
71	70	adantl	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to P \neq 2$
72	71	necomd	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to 2 \neq P$
73	3	nncnd	$⊢ P \in (ℙ ∖ \{2\}) \to P \in ℂ$
74	73	adantl	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to P \in ℂ$
75		1cnd	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to 1 \in ℂ$
76	74 75 75	subadd2d	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to (P - 1 = 1 \leftrightarrow 1 + 1 = P)$
77		1p1e2	$⊢ 1 + 1 = 2$
78	77	eqeq1i	$⊢ 1 + 1 = P \leftrightarrow 2 = P$
79	76 78	bitrdi	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to (P - 1 = 1 \leftrightarrow 2 = P)$
80	79	necon3bid	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to (P - 1 \neq 1 \leftrightarrow 2 \neq P)$
81	72 80	mpbird	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to P - 1 \neq 1$
82	69 81	eqnetrd	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to -1 \mod P \neq 1$
83	82	adantr	$⊢ ((N \in ℕ \land P \in (ℙ ∖ \{2\})) \land 2^{2^{N + 1}} \mod P = 1) \to -1 \mod P \neq 1$
84	83	adantr	$⊢ (((N \in ℕ \land P \in (ℙ ∖ \{2\})) \land 2^{2^{N + 1}} \mod P = 1) \land 2^{2^{N}} \mod P = -1 \mod P) \to -1 \mod P \neq 1$
85		eqeq1	$⊢ 2^{2^{N}} \mod P = -1 \mod P \to (2^{2^{N}} \mod P = 1 \leftrightarrow -1 \mod P = 1)$
86	85	adantl	$⊢ (((N \in ℕ \land P \in (ℙ ∖ \{2\})) \land 2^{2^{N + 1}} \mod P = 1) \land 2^{2^{N}} \mod P = -1 \mod P) \to (2^{2^{N}} \mod P = 1 \leftrightarrow -1 \mod P = 1)$
87	86	necon3bid	$⊢ (((N \in ℕ \land P \in (ℙ ∖ \{2\})) \land 2^{2^{N + 1}} \mod P = 1) \land 2^{2^{N}} \mod P = -1 \mod P) \to (2^{2^{N}} \mod P \neq 1 \leftrightarrow -1 \mod P \neq 1)$
88	84 87	mpbird	$⊢ (((N \in ℕ \land P \in (ℙ ∖ \{2\})) \land 2^{2^{N + 1}} \mod P = 1) \land 2^{2^{N}} \mod P = -1 \mod P) \to 2^{2^{N}} \mod P \neq 1$
89	88	ex	$⊢ ((N \in ℕ \land P \in (ℙ ∖ \{2\})) \land 2^{2^{N + 1}} \mod P = 1) \to (2^{2^{N}} \mod P = -1 \mod P \to 2^{2^{N}} \mod P \neq 1)$
90	67 89	sylbid	$⊢ ((N \in ℕ \land P \in (ℙ ∖ \{2\})) \land 2^{2^{N + 1}} \mod P = 1) \to ((2^{2^{N}} + 1) \mod P = 0 \to 2^{2^{N}} \mod P \neq 1)$
91	90	imp	$⊢ (((N \in ℕ \land P \in (ℙ ∖ \{2\})) \land 2^{2^{N + 1}} \mod P = 1) \land (2^{2^{N}} + 1) \mod P = 0) \to 2^{2^{N}} \mod P \neq 1$
92		simplr	$⊢ (((N \in ℕ \land P \in (ℙ ∖ \{2\})) \land 2^{2^{N + 1}} \mod P = 1) \land (2^{2^{N}} + 1) \mod P = 0) \to 2^{2^{N + 1}} \mod P = 1$
93		odz2prm2pw	$⊢ ((N \in ℕ \land P \in (ℙ ∖ \{2\})) \land (2^{2^{N}} \mod P \neq 1 \land 2^{2^{N + 1}} \mod P = 1)) \to {od}_{ℤ} (P) (2) = 2^{N + 1}$
94	60 91 92 93	syl12anc	$⊢ (((N \in ℕ \land P \in (ℙ ∖ \{2\})) \land 2^{2^{N + 1}} \mod P = 1) \land (2^{2^{N}} + 1) \mod P = 0) \to {od}_{ℤ} (P) (2) = 2^{N + 1}$
95	94	ex	$⊢ ((N \in ℕ \land P \in (ℙ ∖ \{2\})) \land 2^{2^{N + 1}} \mod P = 1) \to ((2^{2^{N}} + 1) \mod P = 0 \to {od}_{ℤ} (P) (2) = 2^{N + 1})$
96	95	ex	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to (2^{2^{N + 1}} \mod P = 1 \to ((2^{2^{N}} + 1) \mod P = 0 \to {od}_{ℤ} (P) (2) = 2^{N + 1}))$
97	59 96	sylbid	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to ({(2^{2^{N}})}^{2} \mod P = {(- 1)}^{2} \mod P \to ((2^{2^{N}} + 1) \mod P = 0 \to {od}_{ℤ} (P) (2) = 2^{N + 1}))$
98	36 97	syld	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to (2^{2^{N}} \mod P = -1 \mod P \to ((2^{2^{N}} + 1) \mod P = 0 \to {od}_{ℤ} (P) (2) = 2^{N + 1}))$
99	25 98	sylbid	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to ((2^{2^{N}} + 1) \mod P = 0 \to ((2^{2^{N}} + 1) \mod P = 0 \to {od}_{ℤ} (P) (2) = 2^{N + 1}))$
100	99	pm2.43d	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to ((2^{2^{N}} + 1) \mod P = 0 \to {od}_{ℤ} (P) (2) = 2^{N + 1})$
101	13 100	syld	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to (P ∥ FermatNo (N) \to {od}_{ℤ} (P) (2) = 2^{N + 1})$
102	101	3impia	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\}) \land P ∥ FermatNo (N)) \to {od}_{ℤ} (P) (2) = 2^{N + 1}$

Metamath Proof Explorer

Theorem fmtnoprmfac1lem

Proof