odz2prm2pw

Description: Any power of two is coprime to any prime not being two. (Contributed by AV, 25-Jul-2021)

		Ref	Expression
	Assertion	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}$

Proof

Step	Hyp	Ref	Expression
1		eldifi	$⊢ P \in (ℙ ∖ \{2\}) \to P \in ℙ$
2		2nn	$⊢ 2 \in ℕ$
3	2	a1i	$⊢ N \in ℕ \to 2 \in ℕ$
4		2nn0	$⊢ 2 \in ℕ_{0}$
5	4	a1i	$⊢ N \in ℕ \to 2 \in ℕ_{0}$
6		peano2nn	$⊢ N \in ℕ \to N + 1 \in ℕ$
7	6	nnnn0d	$⊢ N \in ℕ \to N + 1 \in ℕ_{0}$
8	5 7	nn0expcld	$⊢ N \in ℕ \to 2^{N + 1} \in ℕ_{0}$
9	3 8	nnexpcld	$⊢ N \in ℕ \to 2^{2^{N + 1}} \in ℕ$
10	9	nnzd	$⊢ N \in ℕ \to 2^{2^{N + 1}} \in ℤ$
11		modprm1div	$⊢ (P \in ℙ \land 2^{2^{N + 1}} \in ℤ) \to (2^{2^{N + 1}} \mod P = 1 \leftrightarrow P ∥ (2^{2^{N + 1}} - 1))$
12	1 10 11	syl2anr	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to (2^{2^{N + 1}} \mod P = 1 \leftrightarrow P ∥ (2^{2^{N + 1}} - 1))$
13		prmnn	$⊢ P \in ℙ \to P \in ℕ$
14	1 13	syl	$⊢ P \in (ℙ ∖ \{2\}) \to P \in ℕ$
15	14	adantl	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to P \in ℕ$
16		2z	$⊢ 2 \in ℤ$
17	16	a1i	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to 2 \in ℤ$
18		eldifsn	$⊢ P \in (ℙ ∖ \{2\}) \leftrightarrow (P \in ℙ \land P \neq 2)$
19		simpr	$⊢ (P \in ℙ \land P \neq 2) \to P \neq 2$
20	19	necomd	$⊢ (P \in ℙ \land P \neq 2) \to 2 \neq P$
21	18 20	sylbi	$⊢ P \in (ℙ ∖ \{2\}) \to 2 \neq P$
22		2prm	$⊢ 2 \in ℙ$
23		prmrp	$⊢ (2 \in ℙ \land P \in ℙ) \to (2 \gcd P = 1 \leftrightarrow 2 \neq P)$
24	22 1 23	sylancr	$⊢ P \in (ℙ ∖ \{2\}) \to (2 \gcd P = 1 \leftrightarrow 2 \neq P)$
25	21 24	mpbird	$⊢ P \in (ℙ ∖ \{2\}) \to 2 \gcd P = 1$
26	25	adantl	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to 2 \gcd P = 1$
27	15 17 26	3jca	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to (P \in ℕ \land 2 \in ℤ \land 2 \gcd P = 1)$
28	8	adantr	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to 2^{N + 1} \in ℕ_{0}$
29		odzdvds	$⊢ ((P \in ℕ \land 2 \in ℤ \land 2 \gcd P = 1) \land 2^{N + 1} \in ℕ_{0}) \to (P ∥ (2^{2^{N + 1}} - 1) \leftrightarrow {od}_{ℤ} (P) (2) ∥ 2^{N + 1})$
30	27 28 29	syl2anc	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to (P ∥ (2^{2^{N + 1}} - 1) \leftrightarrow {od}_{ℤ} (P) (2) ∥ 2^{N + 1})$
31	12 30	bitrd	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to (2^{2^{N + 1}} \mod P = 1 \leftrightarrow {od}_{ℤ} (P) (2) ∥ 2^{N + 1})$
32		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
33	5 32	nn0expcld	$⊢ N \in ℕ \to 2^{N} \in ℕ_{0}$
34	3 33	nnexpcld	$⊢ N \in ℕ \to 2^{2^{N}} \in ℕ$
35	34	nnzd	$⊢ N \in ℕ \to 2^{2^{N}} \in ℤ$
36		modprm1div	$⊢ (P \in ℙ \land 2^{2^{N}} \in ℤ) \to (2^{2^{N}} \mod P = 1 \leftrightarrow P ∥ (2^{2^{N}} - 1))$
37	1 35 36	syl2anr	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to (2^{2^{N}} \mod P = 1 \leftrightarrow P ∥ (2^{2^{N}} - 1))$
38	33	adantr	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to 2^{N} \in ℕ_{0}$
39		odzdvds	$⊢ ((P \in ℕ \land 2 \in ℤ \land 2 \gcd P = 1) \land 2^{N} \in ℕ_{0}) \to (P ∥ (2^{2^{N}} - 1) \leftrightarrow {od}_{ℤ} (P) (2) ∥ 2^{N})$
40	27 38 39	syl2anc	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to (P ∥ (2^{2^{N}} - 1) \leftrightarrow {od}_{ℤ} (P) (2) ∥ 2^{N})$
41	37 40	bitrd	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to (2^{2^{N}} \mod P = 1 \leftrightarrow {od}_{ℤ} (P) (2) ∥ 2^{N})$
42	41	necon3abid	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to (2^{2^{N}} \mod P \neq 1 \leftrightarrow \neg {od}_{ℤ} (P) (2) ∥ 2^{N})$
43		odzcl	$⊢ (P \in ℕ \land 2 \in ℤ \land 2 \gcd P = 1) \to {od}_{ℤ} (P) (2) \in ℕ$
44	27 43	syl	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to {od}_{ℤ} (P) (2) \in ℕ$
45	7	adantr	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to N + 1 \in ℕ_{0}$
46		dvdsprmpweqle	$⊢ (2 \in ℙ \land {od}_{ℤ} (P) (2) \in ℕ \land N + 1 \in ℕ_{0}) \to ({od}_{ℤ} (P) (2) ∥ 2^{N + 1} \to \exists n \in ℕ_{0} (n \leq N + 1 \land {od}_{ℤ} (P) (2) = 2^{n}))$
47	22 44 45 46	mp3an2i	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to ({od}_{ℤ} (P) (2) ∥ 2^{N + 1} \to \exists n \in ℕ_{0} (n \leq N + 1 \land {od}_{ℤ} (P) (2) = 2^{n}))$
48		breq1	$⊢ {od}_{ℤ} (P) (2) = 2^{n} \to ({od}_{ℤ} (P) (2) ∥ 2^{N} \leftrightarrow 2^{n} ∥ 2^{N})$
49	48	adantl	$⊢ ((((N \in ℕ \land P \in (ℙ ∖ \{2\})) \land n \in ℕ_{0}) \land n \leq N + 1) \land {od}_{ℤ} (P) (2) = 2^{n}) \to ({od}_{ℤ} (P) (2) ∥ 2^{N} \leftrightarrow 2^{n} ∥ 2^{N})$
50	49	notbid	$⊢ ((((N \in ℕ \land P \in (ℙ ∖ \{2\})) \land n \in ℕ_{0}) \land n \leq N + 1) \land {od}_{ℤ} (P) (2) = 2^{n}) \to (\neg {od}_{ℤ} (P) (2) ∥ 2^{N} \leftrightarrow \neg 2^{n} ∥ 2^{N})$
51		simpr	$⊢ ((((N \in ℕ \land P \in (ℙ ∖ \{2\})) \land n \in ℕ_{0}) \land n \leq N + 1) \land {od}_{ℤ} (P) (2) = 2^{n}) \to {od}_{ℤ} (P) (2) = 2^{n}$
52	51	adantr	$⊢ (((((N \in ℕ \land P \in (ℙ ∖ \{2\})) \land n \in ℕ_{0}) \land n \leq N + 1) \land {od}_{ℤ} (P) (2) = 2^{n}) \land \neg 2^{n} ∥ 2^{N}) \to {od}_{ℤ} (P) (2) = 2^{n}$
53		nn0re	$⊢ n \in ℕ_{0} \to n \in ℝ$
54	6	nnred	$⊢ N \in ℕ \to N + 1 \in ℝ$
55	54	adantr	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to N + 1 \in ℝ$
56		leloe	$⊢ (n \in ℝ \land N + 1 \in ℝ) \to (n \leq N + 1 \leftrightarrow (n < N + 1 \lor n = N + 1))$
57	53 55 56	syl2anr	$⊢ ((N \in ℕ \land P \in (ℙ ∖ \{2\})) \land n \in ℕ_{0}) \to (n \leq N + 1 \leftrightarrow (n < N + 1 \lor n = N + 1))$
58		simpr	$⊢ ((N \in ℕ \land P \in (ℙ ∖ \{2\})) \land n \in ℕ_{0}) \to n \in ℕ_{0}$
59		nn0z	$⊢ n \in ℕ_{0} \to n \in ℤ$
60	59	adantl	$⊢ ((N \in ℕ \land P \in (ℙ ∖ \{2\})) \land n \in ℕ_{0}) \to n \in ℤ$
61	60	adantr	$⊢ (((N \in ℕ \land P \in (ℙ ∖ \{2\})) \land n \in ℕ_{0}) \land n < N + 1) \to n \in ℤ$
62		nnz	$⊢ N \in ℕ \to N \in ℤ$
63	62	adantr	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to N \in ℤ$
64	63	adantr	$⊢ ((N \in ℕ \land P \in (ℙ ∖ \{2\})) \land n \in ℕ_{0}) \to N \in ℤ$
65	64	adantr	$⊢ (((N \in ℕ \land P \in (ℙ ∖ \{2\})) \land n \in ℕ_{0}) \land n < N + 1) \to N \in ℤ$
66		zleltp1	$⊢ (n \in ℤ \land N \in ℤ) \to (n \leq N \leftrightarrow n < N + 1)$
67	59 63 66	syl2anr	$⊢ ((N \in ℕ \land P \in (ℙ ∖ \{2\})) \land n \in ℕ_{0}) \to (n \leq N \leftrightarrow n < N + 1)$
68	67	biimpar	$⊢ (((N \in ℕ \land P \in (ℙ ∖ \{2\})) \land n \in ℕ_{0}) \land n < N + 1) \to n \leq N$
69		eluz2	$⊢ N \in ℤ_{\geq n} \leftrightarrow (n \in ℤ \land N \in ℤ \land n \leq N)$
70	61 65 68 69	syl3anbrc	$⊢ (((N \in ℕ \land P \in (ℙ ∖ \{2\})) \land n \in ℕ_{0}) \land n < N + 1) \to N \in ℤ_{\geq n}$
71		dvdsexp	$⊢ (2 \in ℤ \land n \in ℕ_{0} \land N \in ℤ_{\geq n}) \to 2^{n} ∥ 2^{N}$
72	16 58 70 71	mp3an2ani	$⊢ (((N \in ℕ \land P \in (ℙ ∖ \{2\})) \land n \in ℕ_{0}) \land n < N + 1) \to 2^{n} ∥ 2^{N}$
73	72	pm2.24d	$⊢ (((N \in ℕ \land P \in (ℙ ∖ \{2\})) \land n \in ℕ_{0}) \land n < N + 1) \to (\neg 2^{n} ∥ 2^{N} \to 2^{n} = 2^{N + 1})$
74	73	expcom	$⊢ n < N + 1 \to (((N \in ℕ \land P \in (ℙ ∖ \{2\})) \land n \in ℕ_{0}) \to (\neg 2^{n} ∥ 2^{N} \to 2^{n} = 2^{N + 1}))$
75		oveq2	$⊢ n = N + 1 \to 2^{n} = 2^{N + 1}$
76	75	2a1d	$⊢ n = N + 1 \to (((N \in ℕ \land P \in (ℙ ∖ \{2\})) \land n \in ℕ_{0}) \to (\neg 2^{n} ∥ 2^{N} \to 2^{n} = 2^{N + 1}))$
77	74 76	jaoi	$⊢ (n < N + 1 \lor n = N + 1) \to (((N \in ℕ \land P \in (ℙ ∖ \{2\})) \land n \in ℕ_{0}) \to (\neg 2^{n} ∥ 2^{N} \to 2^{n} = 2^{N + 1}))$
78	77	com12	$⊢ ((N \in ℕ \land P \in (ℙ ∖ \{2\})) \land n \in ℕ_{0}) \to ((n < N + 1 \lor n = N + 1) \to (\neg 2^{n} ∥ 2^{N} \to 2^{n} = 2^{N + 1}))$
79	57 78	sylbid	$⊢ ((N \in ℕ \land P \in (ℙ ∖ \{2\})) \land n \in ℕ_{0}) \to (n \leq N + 1 \to (\neg 2^{n} ∥ 2^{N} \to 2^{n} = 2^{N + 1}))$
80	79	imp	$⊢ (((N \in ℕ \land P \in (ℙ ∖ \{2\})) \land n \in ℕ_{0}) \land n \leq N + 1) \to (\neg 2^{n} ∥ 2^{N} \to 2^{n} = 2^{N + 1})$
81	80	adantr	$⊢ ((((N \in ℕ \land P \in (ℙ ∖ \{2\})) \land n \in ℕ_{0}) \land n \leq N + 1) \land {od}_{ℤ} (P) (2) = 2^{n}) \to (\neg 2^{n} ∥ 2^{N} \to 2^{n} = 2^{N + 1})$
82	81	imp	$⊢ (((((N \in ℕ \land P \in (ℙ ∖ \{2\})) \land n \in ℕ_{0}) \land n \leq N + 1) \land {od}_{ℤ} (P) (2) = 2^{n}) \land \neg 2^{n} ∥ 2^{N}) \to 2^{n} = 2^{N + 1}$
83	52 82	eqtrd	$⊢ (((((N \in ℕ \land P \in (ℙ ∖ \{2\})) \land n \in ℕ_{0}) \land n \leq N + 1) \land {od}_{ℤ} (P) (2) = 2^{n}) \land \neg 2^{n} ∥ 2^{N}) \to {od}_{ℤ} (P) (2) = 2^{N + 1}$
84	83	ex	$⊢ ((((N \in ℕ \land P \in (ℙ ∖ \{2\})) \land n \in ℕ_{0}) \land n \leq N + 1) \land {od}_{ℤ} (P) (2) = 2^{n}) \to (\neg 2^{n} ∥ 2^{N} \to {od}_{ℤ} (P) (2) = 2^{N + 1})$
85	50 84	sylbid	$⊢ ((((N \in ℕ \land P \in (ℙ ∖ \{2\})) \land n \in ℕ_{0}) \land n \leq N + 1) \land {od}_{ℤ} (P) (2) = 2^{n}) \to (\neg {od}_{ℤ} (P) (2) ∥ 2^{N} \to {od}_{ℤ} (P) (2) = 2^{N + 1})$
86	85	expl	$⊢ ((N \in ℕ \land P \in (ℙ ∖ \{2\})) \land n \in ℕ_{0}) \to ((n \leq N + 1 \land {od}_{ℤ} (P) (2) = 2^{n}) \to (\neg {od}_{ℤ} (P) (2) ∥ 2^{N} \to {od}_{ℤ} (P) (2) = 2^{N + 1}))$
87	86	rexlimdva	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to (\exists n \in ℕ_{0} (n \leq N + 1 \land {od}_{ℤ} (P) (2) = 2^{n}) \to (\neg {od}_{ℤ} (P) (2) ∥ 2^{N} \to {od}_{ℤ} (P) (2) = 2^{N + 1}))$
88	47 87	syld	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to ({od}_{ℤ} (P) (2) ∥ 2^{N + 1} \to (\neg {od}_{ℤ} (P) (2) ∥ 2^{N} \to {od}_{ℤ} (P) (2) = 2^{N + 1}))$
89	88	com23	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to (\neg {od}_{ℤ} (P) (2) ∥ 2^{N} \to ({od}_{ℤ} (P) (2) ∥ 2^{N + 1} \to {od}_{ℤ} (P) (2) = 2^{N + 1}))$
90	42 89	sylbid	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to (2^{2^{N}} \mod P \neq 1 \to ({od}_{ℤ} (P) (2) ∥ 2^{N + 1} \to {od}_{ℤ} (P) (2) = 2^{N + 1}))$
91	90	com23	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to ({od}_{ℤ} (P) (2) ∥ 2^{N + 1} \to (2^{2^{N}} \mod P \neq 1 \to {od}_{ℤ} (P) (2) = 2^{N + 1}))$
92	31 91	sylbid	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to (2^{2^{N + 1}} \mod P = 1 \to (2^{2^{N}} \mod P \neq 1 \to {od}_{ℤ} (P) (2) = 2^{N + 1}))$
93	92	com23	$⊢ (N \in ℕ \land P \in (ℙ ∖ \{2\})) \to (2^{2^{N}} \mod P \neq 1 \to (2^{2^{N + 1}} \mod P = 1 \to {od}_{ℤ} (P) (2) = 2^{N + 1}))$
94	93	imp32	$⊢ ((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}$

Metamath Proof Explorer

Theorem odz2prm2pw

Proof