Theorem fmtnoprmfac2lem1 48346

Description: Lemma for fmtnoprmfac2 48347. (Contributed by AV, 26-Jul-2021.)

Assertion

Ref	Expression
fmtnoprmfac2lem1	⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑃 ∥ (FermatNo‘𝑁)) → ((2↑((𝑃 − 1) / 2)) mod 𝑃) = 1)

Proof of Theorem fmtnoprmfac2lem1

Dummy variables 𝑘 𝑛 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eluz2nn 12918	. . 3 ⊢ (𝑁 ∈ (ℤ≥‘2) → 𝑁 ∈ ℕ)
2		eldifi 4084	. . 3 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℙ)
3		id 23	. . 3 ⊢ (𝑃 ∥ (FermatNo‘𝑁) → 𝑃 ∥ (FermatNo‘𝑁))
4		fmtnoprmfac1 48345	. . 3 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁)) → ∃𝑛 ∈ ℕ 𝑃 = ((𝑛 · (2↑(𝑁 + 1))) + 1))
5	1, 2, 3, 4	syl3an 1177	. 2 ⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑃 ∥ (FermatNo‘𝑁)) → ∃𝑛 ∈ ℕ 𝑃 = ((𝑛 · (2↑(𝑁 + 1))) + 1))
6		2z 12632	. . . . . 6 ⊢ 2 ∈ ℤ
7		simp2 1154	. . . . . 6 ⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑃 ∥ (FermatNo‘𝑁)) → 𝑃 ∈ (ℙ ∖ {2}))
8		lgsvalmod 27491	. . . . . . 7 ⊢ ((2 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) → ((2 /L 𝑃) mod 𝑃) = ((2↑((𝑃 − 1) / 2)) mod 𝑃))
9	8	eqcomd 2768	. . . . . 6 ⊢ ((2 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) → ((2↑((𝑃 − 1) / 2)) mod 𝑃) = ((2 /L 𝑃) mod 𝑃))
10	6, 7, 9	sylancr 598	. . . . 5 ⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑃 ∥ (FermatNo‘𝑁)) → ((2↑((𝑃 − 1) / 2)) mod 𝑃) = ((2 /L 𝑃) mod 𝑃))
11	10	ad2antrr 738	. . . 4 ⊢ ((((𝑁 ∈ (ℤ≥‘2) ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑃 ∥ (FermatNo‘𝑁)) ∧ 𝑛 ∈ ℕ) ∧ 𝑃 = ((𝑛 · (2↑(𝑁 + 1))) + 1)) → ((2↑((𝑃 − 1) / 2)) mod 𝑃) = ((2 /L 𝑃) mod 𝑃))
12		nncn 12247	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
13	12	adantl 486	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℂ)
14		2nn 12320	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℕ
15	14	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ (ℤ≥‘2) → 2 ∈ ℕ)
16		eluzge2nn0 12922	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ (ℤ≥‘2) → 𝑁 ∈ ℕ0)
17		peano2nn0 12550	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ0)
18	16, 17	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ (ℤ≥‘2) → (𝑁 + 1) ∈ ℕ0)
19	15, 18	nnexpcld 14288	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ (ℤ≥‘2) → (2↑(𝑁 + 1)) ∈ ℕ)
20	19	nncnd 12255	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ (ℤ≥‘2) → (2↑(𝑁 + 1)) ∈ ℂ)
21	20	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝑛 ∈ ℕ) → (2↑(𝑁 + 1)) ∈ ℂ)
22	13, 21	mulcomd 11236	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝑛 ∈ ℕ) → (𝑛 · (2↑(𝑁 + 1))) = ((2↑(𝑁 + 1)) · 𝑛))
23		8cn 12344	. . . . . . . . . . . . . . . 16 ⊢ 8 ∈ ℂ
24	23	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝑛 ∈ ℕ) → 8 ∈ ℂ)
25		0re 11216	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ ℝ
26		8pos 12362	. . . . . . . . . . . . . . . . 17 ⊢ 0 < 8
27	25, 26	gtneii 11328	. . . . . . . . . . . . . . . 16 ⊢ 8 ≠ 0
28	27	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝑛 ∈ ℕ) → 8 ≠ 0)
29	21, 24, 28	divcan2d 11999	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝑛 ∈ ℕ) → (8 · ((2↑(𝑁 + 1)) / 8)) = (2↑(𝑁 + 1)))
30	29	eqcomd 2768	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝑛 ∈ ℕ) → (2↑(𝑁 + 1)) = (8 · ((2↑(𝑁 + 1)) / 8)))
31	30	oveq1d 7427	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝑛 ∈ ℕ) → ((2↑(𝑁 + 1)) · 𝑛) = ((8 · ((2↑(𝑁 + 1)) / 8)) · 𝑛))
32	23	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ (ℤ≥‘2) → 8 ∈ ℂ)
33	27	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ (ℤ≥‘2) → 8 ≠ 0)
34	20, 32, 33	divcld 11997	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ (ℤ≥‘2) → ((2↑(𝑁 + 1)) / 8) ∈ ℂ)
35	34	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝑛 ∈ ℕ) → ((2↑(𝑁 + 1)) / 8) ∈ ℂ)
36	24, 35, 13	mulassd 11238	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝑛 ∈ ℕ) → ((8 · ((2↑(𝑁 + 1)) / 8)) · 𝑛) = (8 · (((2↑(𝑁 + 1)) / 8) · 𝑛)))
37	22, 31, 36	3eqtrd 2801	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝑛 ∈ ℕ) → (𝑛 · (2↑(𝑁 + 1))) = (8 · (((2↑(𝑁 + 1)) / 8) · 𝑛)))
38	37	oveq1d 7427	. . . . . . . . . 10 ⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝑛 ∈ ℕ) → ((𝑛 · (2↑(𝑁 + 1))) + 1) = ((8 · (((2↑(𝑁 + 1)) / 8) · 𝑛)) + 1))
39	38	eqeq2d 2773	. . . . . . . . 9 ⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝑛 ∈ ℕ) → (𝑃 = ((𝑛 · (2↑(𝑁 + 1))) + 1) ↔ 𝑃 = ((8 · (((2↑(𝑁 + 1)) / 8) · 𝑛)) + 1)))
40		oveq1 7419	. . . . . . . . . . . 12 ⊢ (𝑃 = ((8 · (((2↑(𝑁 + 1)) / 8) · 𝑛)) + 1) → (𝑃 mod 8) = (((8 · (((2↑(𝑁 + 1)) / 8) · 𝑛)) + 1) mod 8))
41	40	adantl 486	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ (ℤ≥‘2) ∧ 𝑛 ∈ ℕ) ∧ 𝑃 = ((8 · (((2↑(𝑁 + 1)) / 8) · 𝑛)) + 1)) → (𝑃 mod 8) = (((8 · (((2↑(𝑁 + 1)) / 8) · 𝑛)) + 1) mod 8))
42		3m1e2 12374	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (3 − 1) = 2
43		eluzle 12881	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑁 ∈ (ℤ≥‘2) → 2 ≤ 𝑁)
44	42, 43	eqbrtrid 5145	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑁 ∈ (ℤ≥‘2) → (3 − 1) ≤ 𝑁)
45		3re 12327	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 3 ∈ ℝ
46	45	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑁 ∈ (ℤ≥‘2) → 3 ∈ ℝ)
47		1red 11215	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑁 ∈ (ℤ≥‘2) → 1 ∈ ℝ)
48		eluzelre 12879	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑁 ∈ (ℤ≥‘2) → 𝑁 ∈ ℝ)
49	46, 47, 48	lesubaddd 11817	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑁 ∈ (ℤ≥‘2) → ((3 − 1) ≤ 𝑁 ↔ 3 ≤ (𝑁 + 1)))
50	44, 49	mpbid 235	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ (ℤ≥‘2) → 3 ≤ (𝑁 + 1))
51		3nn0 12528	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 3 ∈ ℕ0
52		nn0sub 12560	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((3 ∈ ℕ0 ∧ (𝑁 + 1) ∈ ℕ0) → (3 ≤ (𝑁 + 1) ↔ ((𝑁 + 1) − 3) ∈ ℕ0))
53	51, 18, 52	sylancr 598	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ (ℤ≥‘2) → (3 ≤ (𝑁 + 1) ↔ ((𝑁 + 1) − 3) ∈ ℕ0))
54	50, 53	mpbid 235	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ (ℤ≥‘2) → ((𝑁 + 1) − 3) ∈ ℕ0)
55	15, 54	nnexpcld 14288	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ (ℤ≥‘2) → (2↑((𝑁 + 1) − 3)) ∈ ℕ)
56	55	nnzd 12623	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ (ℤ≥‘2) → (2↑((𝑁 + 1) − 3)) ∈ ℤ)
57		oveq2 7420	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = (2↑((𝑁 + 1) − 3)) → (8 · 𝑘) = (8 · (2↑((𝑁 + 1) − 3))))
58	57	eqeq1d 2764	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = (2↑((𝑁 + 1) − 3)) → ((8 · 𝑘) = (2↑(𝑁 + 1)) ↔ (8 · (2↑((𝑁 + 1) − 3))) = (2↑(𝑁 + 1))))
59	58	adantl 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝑘 = (2↑((𝑁 + 1) − 3))) → ((8 · 𝑘) = (2↑(𝑁 + 1)) ↔ (8 · (2↑((𝑁 + 1) − 3))) = (2↑(𝑁 + 1))))
60		cu2 14243	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (2↑3) = 8
61	60	eqcomi 2771	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 8 = (2↑3)
62	61	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ (ℤ≥‘2) → 8 = (2↑3))
63		2cnne0 12459	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (2 ∈ ℂ ∧ 2 ≠ 0)
64	63	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ (ℤ≥‘2) → (2 ∈ ℂ ∧ 2 ≠ 0))
65		eluzelz 12878	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑁 ∈ (ℤ≥‘2) → 𝑁 ∈ ℤ)
66	65	peano2zd 12709	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ (ℤ≥‘2) → (𝑁 + 1) ∈ ℤ)
67		3z 12633	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 3 ∈ ℤ
68	67	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ (ℤ≥‘2) → 3 ∈ ℤ)
69		expsub 14153	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ ((𝑁 + 1) ∈ ℤ ∧ 3 ∈ ℤ)) → (2↑((𝑁 + 1) − 3)) = ((2↑(𝑁 + 1)) / (2↑3)))
70	64, 66, 68, 69	syl12anc 849	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ (ℤ≥‘2) → (2↑((𝑁 + 1) − 3)) = ((2↑(𝑁 + 1)) / (2↑3)))
71	62, 70	oveq12d 7430	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ (ℤ≥‘2) → (8 · (2↑((𝑁 + 1) − 3))) = ((2↑3) · ((2↑(𝑁 + 1)) / (2↑3))))
72		nnexpcl 14117	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((2 ∈ ℕ ∧ 3 ∈ ℕ0) → (2↑3) ∈ ℕ)
73	14, 51, 72	mp2an 704	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (2↑3) ∈ ℕ
74	73	nncni 12249	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (2↑3) ∈ ℂ
75	74	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ (ℤ≥‘2) → (2↑3) ∈ ℂ)
76		2cn 12322	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ∈ ℂ
77		2ne0 12353	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ≠ 0
78		expne0i 14137	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((2 ∈ ℂ ∧ 2 ≠ 0 ∧ 3 ∈ ℤ) → (2↑3) ≠ 0)
79	76, 77, 67, 78	mp3an 1489	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (2↑3) ≠ 0
80	79	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ (ℤ≥‘2) → (2↑3) ≠ 0)
81	20, 75, 80	divcan2d 11999	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ (ℤ≥‘2) → ((2↑3) · ((2↑(𝑁 + 1)) / (2↑3))) = (2↑(𝑁 + 1)))
82	71, 81	eqtrd 2797	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ (ℤ≥‘2) → (8 · (2↑((𝑁 + 1) − 3))) = (2↑(𝑁 + 1)))
83	56, 59, 82	rspcedvd 3582	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ (ℤ≥‘2) → ∃𝑘 ∈ ℤ (8 · 𝑘) = (2↑(𝑁 + 1)))
84		8nn 12342	. . . . . . . . . . . . . . . . . 18 ⊢ 8 ∈ ℕ
85		2nn0 12527	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 2 ∈ ℕ0
86	85	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ (ℤ≥‘2) → 2 ∈ ℕ0)
87	86, 18	nn0expcld 14289	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ (ℤ≥‘2) → (2↑(𝑁 + 1)) ∈ ℕ0)
88	87	nn0zd 12622	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ (ℤ≥‘2) → (2↑(𝑁 + 1)) ∈ ℤ)
89		zdiv 12672	. . . . . . . . . . . . . . . . . 18 ⊢ ((8 ∈ ℕ ∧ (2↑(𝑁 + 1)) ∈ ℤ) → (∃𝑘 ∈ ℤ (8 · 𝑘) = (2↑(𝑁 + 1)) ↔ ((2↑(𝑁 + 1)) / 8) ∈ ℤ))
90	84, 88, 89	sylancr 598	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ (ℤ≥‘2) → (∃𝑘 ∈ ℤ (8 · 𝑘) = (2↑(𝑁 + 1)) ↔ ((2↑(𝑁 + 1)) / 8) ∈ ℤ))
91	83, 90	mpbid 235	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ (ℤ≥‘2) → ((2↑(𝑁 + 1)) / 8) ∈ ℤ)
92	91	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝑛 ∈ ℕ) → ((2↑(𝑁 + 1)) / 8) ∈ ℤ)
93		nnz 12618	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℤ)
94	93	adantl 486	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℤ)
95	92, 94	zmulcld 12712	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝑛 ∈ ℕ) → (((2↑(𝑁 + 1)) / 8) · 𝑛) ∈ ℤ)
96	84	nnzi 12624	. . . . . . . . . . . . . . 15 ⊢ 8 ∈ ℤ
97		2re 12321	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℝ
98		8re 12343	. . . . . . . . . . . . . . . 16 ⊢ 8 ∈ ℝ
99		2lt8 12446	. . . . . . . . . . . . . . . 16 ⊢ 2 < 8
100	97, 98, 99	ltleii 11339	. . . . . . . . . . . . . . 15 ⊢ 2 ≤ 8
101		eluz2 12874	. . . . . . . . . . . . . . 15 ⊢ (8 ∈ (ℤ≥‘2) ↔ (2 ∈ ℤ ∧ 8 ∈ ℤ ∧ 2 ≤ 8))
102	6, 96, 100, 101	mpbir3an 1359	. . . . . . . . . . . . . 14 ⊢ 8 ∈ (ℤ≥‘2)
103		mulp1mod1 13954	. . . . . . . . . . . . . 14 ⊢ (((((2↑(𝑁 + 1)) / 8) · 𝑛) ∈ ℤ ∧ 8 ∈ (ℤ≥‘2)) → (((8 · (((2↑(𝑁 + 1)) / 8) · 𝑛)) + 1) mod 8) = 1)
104	95, 102, 103	sylancl 597	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝑛 ∈ ℕ) → (((8 · (((2↑(𝑁 + 1)) / 8) · 𝑛)) + 1) mod 8) = 1)
105		1nn 12250	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℕ
106		prid1g 4725	. . . . . . . . . . . . . 14 ⊢ (1 ∈ ℕ → 1 ∈ {1, 7})
107	105, 106	mp1i 14	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝑛 ∈ ℕ) → 1 ∈ {1, 7})
108	104, 107	eqeltrd 2862	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝑛 ∈ ℕ) → (((8 · (((2↑(𝑁 + 1)) / 8) · 𝑛)) + 1) mod 8) ∈ {1, 7})
109	108	adantr 485	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ (ℤ≥‘2) ∧ 𝑛 ∈ ℕ) ∧ 𝑃 = ((8 · (((2↑(𝑁 + 1)) / 8) · 𝑛)) + 1)) → (((8 · (((2↑(𝑁 + 1)) / 8) · 𝑛)) + 1) mod 8) ∈ {1, 7})
110	41, 109	eqeltrd 2862	. . . . . . . . . 10 ⊢ (((𝑁 ∈ (ℤ≥‘2) ∧ 𝑛 ∈ ℕ) ∧ 𝑃 = ((8 · (((2↑(𝑁 + 1)) / 8) · 𝑛)) + 1)) → (𝑃 mod 8) ∈ {1, 7})
111	110	ex 417	. . . . . . . . 9 ⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝑛 ∈ ℕ) → (𝑃 = ((8 · (((2↑(𝑁 + 1)) / 8) · 𝑛)) + 1) → (𝑃 mod 8) ∈ {1, 7}))
112	39, 111	sylbid 243	. . . . . . . 8 ⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝑛 ∈ ℕ) → (𝑃 = ((𝑛 · (2↑(𝑁 + 1))) + 1) → (𝑃 mod 8) ∈ {1, 7}))
113	112	3ad2antl1 1203	. . . . . . 7 ⊢ (((𝑁 ∈ (ℤ≥‘2) ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑃 ∥ (FermatNo‘𝑁)) ∧ 𝑛 ∈ ℕ) → (𝑃 = ((𝑛 · (2↑(𝑁 + 1))) + 1) → (𝑃 mod 8) ∈ {1, 7}))
114	113	imp 411	. . . . . 6 ⊢ ((((𝑁 ∈ (ℤ≥‘2) ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑃 ∥ (FermatNo‘𝑁)) ∧ 𝑛 ∈ ℕ) ∧ 𝑃 = ((𝑛 · (2↑(𝑁 + 1))) + 1)) → (𝑃 mod 8) ∈ {1, 7})
115		2lgs 27582	. . . . . . . . 9 ⊢ (𝑃 ∈ ℙ → ((2 /L 𝑃) = 1 ↔ (𝑃 mod 8) ∈ {1, 7}))
116	2, 115	syl 18	. . . . . . . 8 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((2 /L 𝑃) = 1 ↔ (𝑃 mod 8) ∈ {1, 7}))
117	116	3ad2ant2 1151	. . . . . . 7 ⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑃 ∥ (FermatNo‘𝑁)) → ((2 /L 𝑃) = 1 ↔ (𝑃 mod 8) ∈ {1, 7}))
118	117	ad2antrr 738	. . . . . 6 ⊢ ((((𝑁 ∈ (ℤ≥‘2) ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑃 ∥ (FermatNo‘𝑁)) ∧ 𝑛 ∈ ℕ) ∧ 𝑃 = ((𝑛 · (2↑(𝑁 + 1))) + 1)) → ((2 /L 𝑃) = 1 ↔ (𝑃 mod 8) ∈ {1, 7}))
119	114, 118	mpbird 260	. . . . 5 ⊢ ((((𝑁 ∈ (ℤ≥‘2) ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑃 ∥ (FermatNo‘𝑁)) ∧ 𝑛 ∈ ℕ) ∧ 𝑃 = ((𝑛 · (2↑(𝑁 + 1))) + 1)) → (2 /L 𝑃) = 1)
120	119	oveq1d 7427	. . . 4 ⊢ ((((𝑁 ∈ (ℤ≥‘2) ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑃 ∥ (FermatNo‘𝑁)) ∧ 𝑛 ∈ ℕ) ∧ 𝑃 = ((𝑛 · (2↑(𝑁 + 1))) + 1)) → ((2 /L 𝑃) mod 𝑃) = (1 mod 𝑃))
121		prmuz2 16760	. . . . . . 7 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ (ℤ≥‘2))
122		eluzelre 12879	. . . . . . . 8 ⊢ (𝑃 ∈ (ℤ≥‘2) → 𝑃 ∈ ℝ)
123		eluz2gt1 12950	. . . . . . . 8 ⊢ (𝑃 ∈ (ℤ≥‘2) → 1 < 𝑃)
124	122, 123	jca 520	. . . . . . 7 ⊢ (𝑃 ∈ (ℤ≥‘2) → (𝑃 ∈ ℝ ∧ 1 < 𝑃))
125		1mod 13943	. . . . . . 7 ⊢ ((𝑃 ∈ ℝ ∧ 1 < 𝑃) → (1 mod 𝑃) = 1)
126	2, 121, 124, 125	4syl 20	. . . . . 6 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (1 mod 𝑃) = 1)
127	126	3ad2ant2 1151	. . . . 5 ⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑃 ∥ (FermatNo‘𝑁)) → (1 mod 𝑃) = 1)
128	127	ad2antrr 738	. . . 4 ⊢ ((((𝑁 ∈ (ℤ≥‘2) ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑃 ∥ (FermatNo‘𝑁)) ∧ 𝑛 ∈ ℕ) ∧ 𝑃 = ((𝑛 · (2↑(𝑁 + 1))) + 1)) → (1 mod 𝑃) = 1)
129	11, 120, 128	3eqtrd 2801	. . 3 ⊢ ((((𝑁 ∈ (ℤ≥‘2) ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑃 ∥ (FermatNo‘𝑁)) ∧ 𝑛 ∈ ℕ) ∧ 𝑃 = ((𝑛 · (2↑(𝑁 + 1))) + 1)) → ((2↑((𝑃 − 1) / 2)) mod 𝑃) = 1)
130	129	rexlimdva2 3167	. 2 ⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑃 ∥ (FermatNo‘𝑁)) → (∃𝑛 ∈ ℕ 𝑃 = ((𝑛 · (2↑(𝑁 + 1))) + 1) → ((2↑((𝑃 − 1) / 2)) mod 𝑃) = 1))
131	5, 130	mpd 16	1 ⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑃 ∥ (FermatNo‘𝑁)) → ((2↑((𝑃 − 1) / 2)) mod 𝑃) = 1)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1102   = wceq 1569   ∈ wcel 2142   ≠ wne 2957  ∃wrex 3088   ∖ cdif 3901  {csn 4588  {cpr 4590   class class class wbr 5108  ‘cfv 6536  (class class class)co 7412  ℂcc 11104  ℝcr 11105  0cc0 11106  1c1 11107   + caddc 11109   · cmul 11111   < clt 11249   ≤ cle 11250   − cmin 11447   / cdiv 11877  ℕcn 12239  2c2 12301  3c3 12302  7c7 12306  8c8 12307  ℕ₀cn0 12510  ℤcz 12597  ℤ_≥cuz 12868   mod cmo 13909  ↑cexp 14104   ∥ cdvds 16316  ℙcprime 16735   /_L clgs 27469  FermatNocfmtno 48307

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-rep 5237  ax-sep 5256  ax-nul 5268  ax-pow 5335  ax-pr 5403  ax-un 7734  ax-inf2 9608  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1103  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-nf 1813  df-sb 2096  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-rmo 3368  df-reu 3369  df-rab 3416  df-v 3456  df-sbc 3744  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-tp 4593  df-op 4595  df-uni 4872  df-int 4912  df-iun 4957  df-br 5109  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5555  df-eprel 5560  df-po 5568  df-so 5569  df-fr 5613  df-se 5614  df-we 5615  df-xp 5666  df-rel 5667  df-cnv 5668  df-co 5669  df-dm 5670  df-rn 5671  df-res 5672  df-ima 5673  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-isom 6545  df-riota 7369  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7861  df-1st 7984  df-2nd 7985  df-frecs 8276  df-wrecs 8307  df-recs 8356  df-rdg 8395  df-1o 8451  df-2o 8452  df-oadd 8455  df-er 8692  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-sup 9400  df-inf 9401  df-oi 9470  df-dju 9894  df-card 9932  df-pnf 11251  df-mnf 11252  df-xr 11253  df-ltxr 11254  df-le 11255  df-sub 11449  df-neg 11450  df-div 11878  df-nn 12240  df-2 12309  df-3 12310  df-4 12311  df-5 12312  df-6 12313  df-7 12314  df-8 12315  df-n0 12511  df-xnn0 12584  df-z 12598  df-uz 12869  df-q 12979  df-rp 13023  df-ioo 13382  df-ico 13384  df-fz 13542  df-fzo 13690  df-fl 13832  df-mod 13910  df-seq 14045  df-exp 14105  df-fac 14317  df-hash 14374  df-cj 15157  df-re 15158  df-im 15159  df-sqrt 15293  df-abs 15294  df-clim 15546  df-prod 15965  df-dvds 16317  df-gcd 16559  df-prm 16736  df-odz 16830  df-phi 16831  df-pc 16903  df-lgs 27470  df-fmtno 48308

This theorem is used by:  fmtnoprmfac2  48347