fmtnoprmfac1lem - Mathbox for Alexander van der Vekens

	Mathbox for Alexander van der Vekens		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > fmtnoprmfac1lem		Structured version Visualization version GIF version

Theorem fmtnoprmfac1lem 46827

Description: Lemma for fmtnoprmfac1 46828: 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.)

**Assertion**
Ref	Expression
fmtnoprmfac1lem	⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑃 ∥ (FermatNo‘𝑁)) → ((od_ℤ‘𝑃)‘2) = (2↑(𝑁 + 1)))

**Proof of Theorem fmtnoprmfac1lem**
Step	Hyp	Ref	Expression
1		eldifi 4122	. . . . . . 7 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℙ)
2		prmnn 16636	. . . . . . 7 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
3	1, 2	syl 17	. . . . . 6 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℕ)
4	3	ad2antlr 726	. . . . 5 ⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ 𝑃 ∥ (FermatNo‘𝑁)) → 𝑃 ∈ ℕ)
5		nnnn0 12501	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℕ₀)
6		fmtno 46792	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ₀ → (FermatNo‘𝑁) = ((2↑(2↑𝑁)) + 1))
7	5, 6	syl 17	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → (FermatNo‘𝑁) = ((2↑(2↑𝑁)) + 1))
8	7	breq2d 5154	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → (𝑃 ∥ (FermatNo‘𝑁) ↔ 𝑃 ∥ ((2↑(2↑𝑁)) + 1)))
9	8	adantr 480	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → (𝑃 ∥ (FermatNo‘𝑁) ↔ 𝑃 ∥ ((2↑(2↑𝑁)) + 1)))
10	9	biimpa 476	. . . . 5 ⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ 𝑃 ∥ (FermatNo‘𝑁)) → 𝑃 ∥ ((2↑(2↑𝑁)) + 1))
11		dvdsmod0 16228	. . . . 5 ⊢ ((𝑃 ∈ ℕ ∧ 𝑃 ∥ ((2↑(2↑𝑁)) + 1)) → (((2↑(2↑𝑁)) + 1) mod 𝑃) = 0)
12	4, 10, 11	syl2anc 583	. . . 4 ⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ 𝑃 ∥ (FermatNo‘𝑁)) → (((2↑(2↑𝑁)) + 1) mod 𝑃) = 0)
13	12	ex 412	. . 3 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → (𝑃 ∥ (FermatNo‘𝑁) → (((2↑(2↑𝑁)) + 1) mod 𝑃) = 0))
14		2nn 12307	. . . . . . . . . 10 ⊢ 2 ∈ ℕ
15	14	a1i 11	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → 2 ∈ ℕ)
16		2nn0 12511	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ₀
17	16	a1i 11	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → 2 ∈ ℕ₀)
18	17, 5	nn0expcld 14232	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → (2↑𝑁) ∈ ℕ₀)
19	15, 18	nnexpcld 14231	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → (2↑(2↑𝑁)) ∈ ℕ)
20	19	nnzd 12607	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → (2↑(2↑𝑁)) ∈ ℤ)
21	20	adantr 480	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → (2↑(2↑𝑁)) ∈ ℤ)
22		1zzd 12615	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → 1 ∈ ℤ)
23	3	adantl 481	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → 𝑃 ∈ ℕ)
24		summodnegmod 16255	. . . . . 6 ⊢ (((2↑(2↑𝑁)) ∈ ℤ ∧ 1 ∈ ℤ ∧ 𝑃 ∈ ℕ) → ((((2↑(2↑𝑁)) + 1) mod 𝑃) = 0 ↔ ((2↑(2↑𝑁)) mod 𝑃) = (-1 mod 𝑃)))
25	21, 22, 23, 24	syl3anc 1369	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → ((((2↑(2↑𝑁)) + 1) mod 𝑃) = 0 ↔ ((2↑(2↑𝑁)) mod 𝑃) = (-1 mod 𝑃)))
26		neg1z 12620	. . . . . . . . . 10 ⊢ -1 ∈ ℤ
27	21, 26	jctir 520	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → ((2↑(2↑𝑁)) ∈ ℤ ∧ -1 ∈ ℤ))
28	27	adantr 480	. . . . . . . 8 ⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ((2↑(2↑𝑁)) mod 𝑃) = (-1 mod 𝑃)) → ((2↑(2↑𝑁)) ∈ ℤ ∧ -1 ∈ ℤ))
29	2	nnrpd 13038	. . . . . . . . . . 11 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℝ⁺)
30	1, 29	syl 17	. . . . . . . . . 10 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℝ⁺)
31	17, 30	anim12i 612	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → (2 ∈ ℕ₀ ∧ 𝑃 ∈ ℝ⁺))
32	31	adantr 480	. . . . . . . 8 ⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ((2↑(2↑𝑁)) mod 𝑃) = (-1 mod 𝑃)) → (2 ∈ ℕ₀ ∧ 𝑃 ∈ ℝ⁺))
33		simpr 484	. . . . . . . 8 ⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ((2↑(2↑𝑁)) mod 𝑃) = (-1 mod 𝑃)) → ((2↑(2↑𝑁)) mod 𝑃) = (-1 mod 𝑃))
34		modexp 14224	. . . . . . . 8 ⊢ ((((2↑(2↑𝑁)) ∈ ℤ ∧ -1 ∈ ℤ) ∧ (2 ∈ ℕ₀ ∧ 𝑃 ∈ ℝ⁺) ∧ ((2↑(2↑𝑁)) mod 𝑃) = (-1 mod 𝑃)) → (((2↑(2↑𝑁))↑2) mod 𝑃) = ((-1↑2) mod 𝑃))
35	28, 32, 33, 34	syl3anc 1369	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ((2↑(2↑𝑁)) mod 𝑃) = (-1 mod 𝑃)) → (((2↑(2↑𝑁))↑2) mod 𝑃) = ((-1↑2) mod 𝑃))
36	35	ex 412	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → (((2↑(2↑𝑁)) mod 𝑃) = (-1 mod 𝑃) → (((2↑(2↑𝑁))↑2) mod 𝑃) = ((-1↑2) mod 𝑃)))
37		2cnd 12312	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ → 2 ∈ ℂ)
38	37, 18, 17	3jca 1126	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → (2 ∈ ℂ ∧ (2↑𝑁) ∈ ℕ₀ ∧ 2 ∈ ℕ₀))
39	38	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → (2 ∈ ℂ ∧ (2↑𝑁) ∈ ℕ₀ ∧ 2 ∈ ℕ₀))
40		expmul 14096	. . . . . . . . . . 11 ⊢ ((2 ∈ ℂ ∧ (2↑𝑁) ∈ ℕ₀ ∧ 2 ∈ ℕ₀) → (2↑((2↑𝑁) · 2)) = ((2↑(2↑𝑁))↑2))
41	39, 40	syl 17	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → (2↑((2↑𝑁) · 2)) = ((2↑(2↑𝑁))↑2))
42		2cnd 12312	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → 2 ∈ ℂ)
43	5	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → 𝑁 ∈ ℕ₀)
44	42, 43	expp1d 14135	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → (2↑(𝑁 + 1)) = ((2↑𝑁) · 2))
45	44	eqcomd 2733	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → ((2↑𝑁) · 2) = (2↑(𝑁 + 1)))
46	45	oveq2d 7430	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → (2↑((2↑𝑁) · 2)) = (2↑(2↑(𝑁 + 1))))
47	41, 46	eqtr3d 2769	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → ((2↑(2↑𝑁))↑2) = (2↑(2↑(𝑁 + 1))))
48	47	oveq1d 7429	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → (((2↑(2↑𝑁))↑2) mod 𝑃) = ((2↑(2↑(𝑁 + 1))) mod 𝑃))
49		neg1sqe1 14183	. . . . . . . . . . 11 ⊢ (-1↑2) = 1
50	49	a1i 11	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → (-1↑2) = 1)
51	50	oveq1d 7429	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → ((-1↑2) mod 𝑃) = (1 mod 𝑃))
52	3	nnred 12249	. . . . . . . . . . 11 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℝ)
53		prmgt1 16659	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ ℙ → 1 < 𝑃)
54	1, 53	syl 17	. . . . . . . . . . 11 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 1 < 𝑃)
55		1mod 13892	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ ℝ ∧ 1 < 𝑃) → (1 mod 𝑃) = 1)
56	52, 54, 55	syl2anc 583	. . . . . . . . . 10 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (1 mod 𝑃) = 1)
57	56	adantl 481	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → (1 mod 𝑃) = 1)
58	51, 57	eqtrd 2767	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → ((-1↑2) mod 𝑃) = 1)
59	48, 58	eqeq12d 2743	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → ((((2↑(2↑𝑁))↑2) mod 𝑃) = ((-1↑2) mod 𝑃) ↔ ((2↑(2↑(𝑁 + 1))) mod 𝑃) = 1))
60		simpll 766	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ((2↑(2↑(𝑁 + 1))) mod 𝑃) = 1) ∧ (((2↑(2↑𝑁)) + 1) mod 𝑃) = 0) → (𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})))
61	20	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (2↑(2↑𝑁)) ∈ ℤ)
62		1zzd 12615	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → 1 ∈ ℤ)
63	2	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → 𝑃 ∈ ℕ)
64	61, 62, 63	3jca 1126	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → ((2↑(2↑𝑁)) ∈ ℤ ∧ 1 ∈ ℤ ∧ 𝑃 ∈ ℕ))
65	1, 64	sylan2 592	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → ((2↑(2↑𝑁)) ∈ ℤ ∧ 1 ∈ ℤ ∧ 𝑃 ∈ ℕ))
66	65	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ((2↑(2↑(𝑁 + 1))) mod 𝑃) = 1) → ((2↑(2↑𝑁)) ∈ ℤ ∧ 1 ∈ ℤ ∧ 𝑃 ∈ ℕ))
67	66, 24	syl 17	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ((2↑(2↑(𝑁 + 1))) mod 𝑃) = 1) → ((((2↑(2↑𝑁)) + 1) mod 𝑃) = 0 ↔ ((2↑(2↑𝑁)) mod 𝑃) = (-1 mod 𝑃)))
68		m1modnnsub1 13906	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑃 ∈ ℕ → (-1 mod 𝑃) = (𝑃 − 1))
69	23, 68	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → (-1 mod 𝑃) = (𝑃 − 1))
70		eldifsni 4789	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ≠ 2)
71	70	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → 𝑃 ≠ 2)
72	71	necomd 2991	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → 2 ≠ 𝑃)
73	3	nncnd 12250	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℂ)
74	73	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → 𝑃 ∈ ℂ)
75		1cnd 11231	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → 1 ∈ ℂ)
76	74, 75, 75	subadd2d 11612	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → ((𝑃 − 1) = 1 ↔ (1 + 1) = 𝑃))
77		1p1e2 12359	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1 + 1) = 2
78	77	eqeq1i 2732	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1 + 1) = 𝑃 ↔ 2 = 𝑃)
79	76, 78	bitrdi 287	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → ((𝑃 − 1) = 1 ↔ 2 = 𝑃))
80	79	necon3bid 2980	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → ((𝑃 − 1) ≠ 1 ↔ 2 ≠ 𝑃))
81	72, 80	mpbird 257	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → (𝑃 − 1) ≠ 1)
82	69, 81	eqnetrd 3003	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → (-1 mod 𝑃) ≠ 1)
83	82	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ((2↑(2↑(𝑁 + 1))) mod 𝑃) = 1) → (-1 mod 𝑃) ≠ 1)
84	83	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ((2↑(2↑(𝑁 + 1))) mod 𝑃) = 1) ∧ ((2↑(2↑𝑁)) mod 𝑃) = (-1 mod 𝑃)) → (-1 mod 𝑃) ≠ 1)
85		eqeq1 2731	. . . . . . . . . . . . . . . 16 ⊢ (((2↑(2↑𝑁)) mod 𝑃) = (-1 mod 𝑃) → (((2↑(2↑𝑁)) mod 𝑃) = 1 ↔ (-1 mod 𝑃) = 1))
86	85	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ((2↑(2↑(𝑁 + 1))) mod 𝑃) = 1) ∧ ((2↑(2↑𝑁)) mod 𝑃) = (-1 mod 𝑃)) → (((2↑(2↑𝑁)) mod 𝑃) = 1 ↔ (-1 mod 𝑃) = 1))
87	86	necon3bid 2980	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ((2↑(2↑(𝑁 + 1))) mod 𝑃) = 1) ∧ ((2↑(2↑𝑁)) mod 𝑃) = (-1 mod 𝑃)) → (((2↑(2↑𝑁)) mod 𝑃) ≠ 1 ↔ (-1 mod 𝑃) ≠ 1))
88	84, 87	mpbird 257	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ((2↑(2↑(𝑁 + 1))) mod 𝑃) = 1) ∧ ((2↑(2↑𝑁)) mod 𝑃) = (-1 mod 𝑃)) → ((2↑(2↑𝑁)) mod 𝑃) ≠ 1)
89	88	ex 412	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ((2↑(2↑(𝑁 + 1))) mod 𝑃) = 1) → (((2↑(2↑𝑁)) mod 𝑃) = (-1 mod 𝑃) → ((2↑(2↑𝑁)) mod 𝑃) ≠ 1))
90	67, 89	sylbid 239	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ((2↑(2↑(𝑁 + 1))) mod 𝑃) = 1) → ((((2↑(2↑𝑁)) + 1) mod 𝑃) = 0 → ((2↑(2↑𝑁)) mod 𝑃) ≠ 1))
91	90	imp 406	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ((2↑(2↑(𝑁 + 1))) mod 𝑃) = 1) ∧ (((2↑(2↑𝑁)) + 1) mod 𝑃) = 0) → ((2↑(2↑𝑁)) mod 𝑃) ≠ 1)
92		simplr 768	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ((2↑(2↑(𝑁 + 1))) mod 𝑃) = 1) ∧ (((2↑(2↑𝑁)) + 1) mod 𝑃) = 0) → ((2↑(2↑(𝑁 + 1))) mod 𝑃) = 1)
93		odz2prm2pw 46826	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ (((2↑(2↑𝑁)) mod 𝑃) ≠ 1 ∧ ((2↑(2↑(𝑁 + 1))) mod 𝑃) = 1)) → ((od_ℤ‘𝑃)‘2) = (2↑(𝑁 + 1)))
94	60, 91, 92, 93	syl12anc 836	. . . . . . . . 9 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ((2↑(2↑(𝑁 + 1))) mod 𝑃) = 1) ∧ (((2↑(2↑𝑁)) + 1) mod 𝑃) = 0) → ((od_ℤ‘𝑃)‘2) = (2↑(𝑁 + 1)))
95	94	ex 412	. . . . . . . 8 ⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ((2↑(2↑(𝑁 + 1))) mod 𝑃) = 1) → ((((2↑(2↑𝑁)) + 1) mod 𝑃) = 0 → ((od_ℤ‘𝑃)‘2) = (2↑(𝑁 + 1))))
96	95	ex 412	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → (((2↑(2↑(𝑁 + 1))) mod 𝑃) = 1 → ((((2↑(2↑𝑁)) + 1) mod 𝑃) = 0 → ((od_ℤ‘𝑃)‘2) = (2↑(𝑁 + 1)))))
97	59, 96	sylbid 239	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → ((((2↑(2↑𝑁))↑2) mod 𝑃) = ((-1↑2) mod 𝑃) → ((((2↑(2↑𝑁)) + 1) mod 𝑃) = 0 → ((od_ℤ‘𝑃)‘2) = (2↑(𝑁 + 1)))))
98	36, 97	syld 47	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → (((2↑(2↑𝑁)) mod 𝑃) = (-1 mod 𝑃) → ((((2↑(2↑𝑁)) + 1) mod 𝑃) = 0 → ((od_ℤ‘𝑃)‘2) = (2↑(𝑁 + 1)))))
99	25, 98	sylbid 239	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → ((((2↑(2↑𝑁)) + 1) mod 𝑃) = 0 → ((((2↑(2↑𝑁)) + 1) mod 𝑃) = 0 → ((od_ℤ‘𝑃)‘2) = (2↑(𝑁 + 1)))))
100	99	pm2.43d 53	. . 3 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → ((((2↑(2↑𝑁)) + 1) mod 𝑃) = 0 → ((od_ℤ‘𝑃)‘2) = (2↑(𝑁 + 1))))
101	13, 100	syld 47	. 2 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) → (𝑃 ∥ (FermatNo‘𝑁) → ((od_ℤ‘𝑃)‘2) = (2↑(𝑁 + 1))))
102	101	3impia 1115	1 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑃 ∥ (FermatNo‘𝑁)) → ((od_ℤ‘𝑃)‘2) = (2↑(𝑁 + 1)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 ∧ w3a 1085 = wceq 1534 ∈ wcel 2099 ≠ wne 2935 ∖ cdif 3941 {csn 4624 class class class wbr 5142 ‘cfv 6542 (class class class)co 7414 ℂcc 11128 ℝcr 11129 0cc0 11130 1c1 11131 + caddc 11133 · cmul 11135 < clt 11270 − cmin 11466 -cneg 11467 ℕcn 12234 2c2 12289 ℕ₀cn0 12494 ℤcz 12580 ℝ⁺crp 12998 mod cmo 13858 ↑cexp 14050 ∥ cdvds 16222 ℙcprime 16633 od_ℤcodz 16723 FermatNocfmtno 46790

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2164 ax-ext 2698 ax-rep 5279 ax-sep 5293 ax-nul 5300 ax-pow 5359 ax-pr 5423 ax-un 7734 ax-cnex 11186 ax-resscn 11187 ax-1cn 11188 ax-icn 11189 ax-addcl 11190 ax-addrcl 11191 ax-mulcl 11192 ax-mulrcl 11193 ax-mulcom 11194 ax-addass 11195 ax-mulass 11196 ax-distr 11197 ax-i2m1 11198 ax-1ne0 11199 ax-1rid 11200 ax-rnegex 11201 ax-rrecex 11202 ax-cnre 11203 ax-pre-lttri 11204 ax-pre-lttrn 11205 ax-pre-ltadd 11206 ax-pre-mulgt0 11207 ax-pre-sup 11208

This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3or 1086 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2705 df-cleq 2719 df-clel 2805 df-nfc 2880 df-ne 2936 df-nel 3042 df-ral 3057 df-rex 3066 df-rmo 3371 df-reu 3372 df-rab 3428 df-v 3471 df-sbc 3775 df-csb 3890 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-pss 3963 df-nul 4319 df-if 4525 df-pw 4600 df-sn 4625 df-pr 4627 df-op 4631 df-uni 4904 df-int 4945 df-iun 4993 df-br 5143 df-opab 5205 df-mpt 5226 df-tr 5260 df-id 5570 df-eprel 5576 df-po 5584 df-so 5585 df-fr 5627 df-we 5629 df-xp 5678 df-rel 5679 df-cnv 5680 df-co 5681 df-dm 5682 df-rn 5683 df-res 5684 df-ima 5685 df-pred 6299 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-riota 7370 df-ov 7417 df-oprab 7418 df-mpo 7419 df-om 7865 df-1st 7987 df-2nd 7988 df-frecs 8280 df-wrecs 8311 df-recs 8385 df-rdg 8424 df-1o 8480 df-2o 8481 df-oadd 8484 df-er 8718 df-en 8956 df-dom 8957 df-sdom 8958 df-fin 8959 df-sup 9457 df-inf 9458 df-card 9954 df-pnf 11272 df-mnf 11273 df-xr 11274 df-ltxr 11275 df-le 11276 df-sub 11468 df-neg 11469 df-div 11894 df-nn 12235 df-2 12297 df-3 12298 df-n0 12495 df-xnn0 12567 df-z 12581 df-uz 12845 df-q 12955 df-rp 12999 df-fz 13509 df-fzo 13652 df-fl 13781 df-mod 13859 df-seq 13991 df-exp 14051 df-hash 14314 df-cj 15070 df-re 15071 df-im 15072 df-sqrt 15206 df-abs 15207 df-dvds 16223 df-gcd 16461 df-prm 16634 df-odz 16725 df-phi 16726 df-pc 16797 df-fmtno 46791

This theorem is referenced by: fmtnoprmfac1 46828 fmtnoprmfac2 46830

W3C validator