fmtnoprmfac1 - Mathbox for Alexander van der Vekens

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

Theorem fmtnoprmfac1 41477

Description: Divisor of Fermat number (special form of Euler's result, see fmtnofac1 41482): 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+1)+1 where k is a positive integer. (Contributed by AV, 25-Jul-2021.)

**Assertion**
Ref	Expression
fmtnoprmfac1	⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 1))) + 1))

Distinct variable groups: 𝑘,𝑁 𝑃,𝑘

**Proof of Theorem fmtnoprmfac1**
Step	Hyp	Ref	Expression
1		breq1 4656	. . . . . . 7 ⊢ (𝑃 = 2 → (𝑃 ∥ (FermatNo‘𝑁) ↔ 2 ∥ (FermatNo‘𝑁)))
2	1	adantr 481	. . . . . 6 ⊢ ((𝑃 = 2 ∧ 𝑁 ∈ ℕ) → (𝑃 ∥ (FermatNo‘𝑁) ↔ 2 ∥ (FermatNo‘𝑁)))
3		nnnn0 11299	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℕ₀)
4		fmtnoodd 41445	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ₀ → ¬ 2 ∥ (FermatNo‘𝑁))
5	3, 4	syl 17	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → ¬ 2 ∥ (FermatNo‘𝑁))
6	5	adantl 482	. . . . . . 7 ⊢ ((𝑃 = 2 ∧ 𝑁 ∈ ℕ) → ¬ 2 ∥ (FermatNo‘𝑁))
7	6	pm2.21d 118	. . . . . 6 ⊢ ((𝑃 = 2 ∧ 𝑁 ∈ ℕ) → (2 ∥ (FermatNo‘𝑁) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 1))) + 1)))
8	2, 7	sylbid 230	. . . . 5 ⊢ ((𝑃 = 2 ∧ 𝑁 ∈ ℕ) → (𝑃 ∥ (FermatNo‘𝑁) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 1))) + 1)))
9	8	a1d 25	. . . 4 ⊢ ((𝑃 = 2 ∧ 𝑁 ∈ ℕ) → (𝑃 ∈ ℙ → (𝑃 ∥ (FermatNo‘𝑁) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 1))) + 1))))
10	9	ex 450	. . 3 ⊢ (𝑃 = 2 → (𝑁 ∈ ℕ → (𝑃 ∈ ℙ → (𝑃 ∥ (FermatNo‘𝑁) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 1))) + 1)))))
11	10	3impd 1281	. 2 ⊢ (𝑃 = 2 → ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 1))) + 1)))
12		simpr1 1067	. . . . 5 ⊢ ((¬ 𝑃 = 2 ∧ (𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) → 𝑁 ∈ ℕ)
13		neqne 2802	. . . . . . . . . 10 ⊢ (¬ 𝑃 = 2 → 𝑃 ≠ 2)
14	13	anim2i 593	. . . . . . . . 9 ⊢ ((𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2) → (𝑃 ∈ ℙ ∧ 𝑃 ≠ 2))
15		eldifsn 4317	. . . . . . . . 9 ⊢ (𝑃 ∈ (ℙ ∖ {2}) ↔ (𝑃 ∈ ℙ ∧ 𝑃 ≠ 2))
16	14, 15	sylibr 224	. . . . . . . 8 ⊢ ((𝑃 ∈ ℙ ∧ ¬ 𝑃 = 2) → 𝑃 ∈ (ℙ ∖ {2}))
17	16	ex 450	. . . . . . 7 ⊢ (𝑃 ∈ ℙ → (¬ 𝑃 = 2 → 𝑃 ∈ (ℙ ∖ {2})))
18	17	3ad2ant2 1083	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁)) → (¬ 𝑃 = 2 → 𝑃 ∈ (ℙ ∖ {2})))
19	18	impcom 446	. . . . 5 ⊢ ((¬ 𝑃 = 2 ∧ (𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) → 𝑃 ∈ (ℙ ∖ {2}))
20		simpr3 1069	. . . . 5 ⊢ ((¬ 𝑃 = 2 ∧ (𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) → 𝑃 ∥ (FermatNo‘𝑁))
21		fmtnoprmfac1lem 41476	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑃 ∥ (FermatNo‘𝑁)) → ((od_ℤ‘𝑃)‘2) = (2↑(𝑁 + 1)))
22	12, 19, 20, 21	syl3anc 1326	. . . 4 ⊢ ((¬ 𝑃 = 2 ∧ (𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) → ((od_ℤ‘𝑃)‘2) = (2↑(𝑁 + 1)))
23		prmnn 15388	. . . . . . . 8 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
24	23	ad2antll 765	. . . . . . 7 ⊢ ((¬ 𝑃 = 2 ∧ (𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ)) → 𝑃 ∈ ℕ)
25		2z 11409	. . . . . . . 8 ⊢ 2 ∈ ℤ
26	25	a1i 11	. . . . . . 7 ⊢ ((¬ 𝑃 = 2 ∧ (𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ)) → 2 ∈ ℤ)
27	13	necomd 2849	. . . . . . . . 9 ⊢ (¬ 𝑃 = 2 → 2 ≠ 𝑃)
28	27	adantr 481	. . . . . . . 8 ⊢ ((¬ 𝑃 = 2 ∧ (𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ)) → 2 ≠ 𝑃)
29		2prm 15405	. . . . . . . . . . . 12 ⊢ 2 ∈ ℙ
30	29	a1i 11	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → 2 ∈ ℙ)
31	30	anim1i 592	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (2 ∈ ℙ ∧ 𝑃 ∈ ℙ))
32	31	adantl 482	. . . . . . . . 9 ⊢ ((¬ 𝑃 = 2 ∧ (𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ)) → (2 ∈ ℙ ∧ 𝑃 ∈ ℙ))
33		prmrp 15424	. . . . . . . . 9 ⊢ ((2 ∈ ℙ ∧ 𝑃 ∈ ℙ) → ((2 gcd 𝑃) = 1 ↔ 2 ≠ 𝑃))
34	32, 33	syl 17	. . . . . . . 8 ⊢ ((¬ 𝑃 = 2 ∧ (𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ)) → ((2 gcd 𝑃) = 1 ↔ 2 ≠ 𝑃))
35	28, 34	mpbird 247	. . . . . . 7 ⊢ ((¬ 𝑃 = 2 ∧ (𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ)) → (2 gcd 𝑃) = 1)
36		odzphi 15501	. . . . . . 7 ⊢ ((𝑃 ∈ ℕ ∧ 2 ∈ ℤ ∧ (2 gcd 𝑃) = 1) → ((od_ℤ‘𝑃)‘2) ∥ (ϕ‘𝑃))
37	24, 26, 35, 36	syl3anc 1326	. . . . . 6 ⊢ ((¬ 𝑃 = 2 ∧ (𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ)) → ((od_ℤ‘𝑃)‘2) ∥ (ϕ‘𝑃))
38		phiprm 15482	. . . . . . . . 9 ⊢ (𝑃 ∈ ℙ → (ϕ‘𝑃) = (𝑃 − 1))
39	38	ad2antll 765	. . . . . . . 8 ⊢ ((¬ 𝑃 = 2 ∧ (𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ)) → (ϕ‘𝑃) = (𝑃 − 1))
40	39	breq2d 4665	. . . . . . 7 ⊢ ((¬ 𝑃 = 2 ∧ (𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ)) → (((od_ℤ‘𝑃)‘2) ∥ (ϕ‘𝑃) ↔ ((od_ℤ‘𝑃)‘2) ∥ (𝑃 − 1)))
41		breq1 4656	. . . . . . . . . . 11 ⊢ (((od_ℤ‘𝑃)‘2) = (2↑(𝑁 + 1)) → (((od_ℤ‘𝑃)‘2) ∥ (𝑃 − 1) ↔ (2↑(𝑁 + 1)) ∥ (𝑃 − 1)))
42	41	adantl 482	. . . . . . . . . 10 ⊢ (((¬ 𝑃 = 2 ∧ (𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ)) ∧ ((od_ℤ‘𝑃)‘2) = (2↑(𝑁 + 1))) → (((od_ℤ‘𝑃)‘2) ∥ (𝑃 − 1) ↔ (2↑(𝑁 + 1)) ∥ (𝑃 − 1)))
43		2nn 11185	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℕ
44	43	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → 2 ∈ ℕ)
45		peano2nn 11032	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℕ)
46	45	nnnn0d 11351	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℕ₀)
47	44, 46	nnexpcld 13030	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ ℕ → (2↑(𝑁 + 1)) ∈ ℕ)
48	23	nnnn0d 11351	. . . . . . . . . . . . . . . 16 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ₀)
49		prmuz2 15408	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ (ℤ_≥‘2))
50		eluzle 11700	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃 ∈ (ℤ_≥‘2) → 2 ≤ 𝑃)
51	49, 50	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑃 ∈ ℙ → 2 ≤ 𝑃)
52		nn0ge2m1nn 11360	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 ∈ ℕ₀ ∧ 2 ≤ 𝑃) → (𝑃 − 1) ∈ ℕ)
53	48, 51, 52	syl2anc 693	. . . . . . . . . . . . . . 15 ⊢ (𝑃 ∈ ℙ → (𝑃 − 1) ∈ ℕ)
54	47, 53	anim12i 590	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → ((2↑(𝑁 + 1)) ∈ ℕ ∧ (𝑃 − 1) ∈ ℕ))
55	54	adantl 482	. . . . . . . . . . . . 13 ⊢ ((¬ 𝑃 = 2 ∧ (𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ)) → ((2↑(𝑁 + 1)) ∈ ℕ ∧ (𝑃 − 1) ∈ ℕ))
56		nndivides 14990	. . . . . . . . . . . . 13 ⊢ (((2↑(𝑁 + 1)) ∈ ℕ ∧ (𝑃 − 1) ∈ ℕ) → ((2↑(𝑁 + 1)) ∥ (𝑃 − 1) ↔ ∃𝑘 ∈ ℕ (𝑘 · (2↑(𝑁 + 1))) = (𝑃 − 1)))
57	55, 56	syl 17	. . . . . . . . . . . 12 ⊢ ((¬ 𝑃 = 2 ∧ (𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ)) → ((2↑(𝑁 + 1)) ∥ (𝑃 − 1) ↔ ∃𝑘 ∈ ℕ (𝑘 · (2↑(𝑁 + 1))) = (𝑃 − 1)))
58		eqcom 2629	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 · (2↑(𝑁 + 1))) = (𝑃 − 1) ↔ (𝑃 − 1) = (𝑘 · (2↑(𝑁 + 1))))
59	58	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((¬ 𝑃 = 2 ∧ (𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ)) ∧ 𝑘 ∈ ℕ) → ((𝑘 · (2↑(𝑁 + 1))) = (𝑃 − 1) ↔ (𝑃 − 1) = (𝑘 · (2↑(𝑁 + 1)))))
60	23	nncnd 11036	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℂ)
61	60	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → 𝑃 ∈ ℂ)
62	61	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 𝑃 ∈ ℂ)
63		1cnd 10056	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 1 ∈ ℂ)
64		nncn 11028	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
65	64	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℂ)
66		peano2nn0 11333	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑁 ∈ ℕ₀ → (𝑁 + 1) ∈ ℕ₀)
67	3, 66	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℕ₀)
68	44, 67	nnexpcld 13030	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℕ → (2↑(𝑁 + 1)) ∈ ℕ)
69	68	nncnd 11036	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ ℕ → (2↑(𝑁 + 1)) ∈ ℂ)
70	69	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (2↑(𝑁 + 1)) ∈ ℂ)
71	70	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (2↑(𝑁 + 1)) ∈ ℂ)
72	65, 71	mulcld 10060	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (𝑘 · (2↑(𝑁 + 1))) ∈ ℂ)
73	62, 63, 72	subadd2d 10411	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((𝑃 − 1) = (𝑘 · (2↑(𝑁 + 1))) ↔ ((𝑘 · (2↑(𝑁 + 1))) + 1) = 𝑃))
74	73	adantll 750	. . . . . . . . . . . . . . 15 ⊢ (((¬ 𝑃 = 2 ∧ (𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ)) ∧ 𝑘 ∈ ℕ) → ((𝑃 − 1) = (𝑘 · (2↑(𝑁 + 1))) ↔ ((𝑘 · (2↑(𝑁 + 1))) + 1) = 𝑃))
75		eqcom 2629	. . . . . . . . . . . . . . . 16 ⊢ (((𝑘 · (2↑(𝑁 + 1))) + 1) = 𝑃 ↔ 𝑃 = ((𝑘 · (2↑(𝑁 + 1))) + 1))
76	75	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((¬ 𝑃 = 2 ∧ (𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ)) ∧ 𝑘 ∈ ℕ) → (((𝑘 · (2↑(𝑁 + 1))) + 1) = 𝑃 ↔ 𝑃 = ((𝑘 · (2↑(𝑁 + 1))) + 1)))
77	59, 74, 76	3bitrd 294	. . . . . . . . . . . . . 14 ⊢ (((¬ 𝑃 = 2 ∧ (𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ)) ∧ 𝑘 ∈ ℕ) → ((𝑘 · (2↑(𝑁 + 1))) = (𝑃 − 1) ↔ 𝑃 = ((𝑘 · (2↑(𝑁 + 1))) + 1)))
78	77	rexbidva 3049	. . . . . . . . . . . . 13 ⊢ ((¬ 𝑃 = 2 ∧ (𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ)) → (∃𝑘 ∈ ℕ (𝑘 · (2↑(𝑁 + 1))) = (𝑃 − 1) ↔ ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 1))) + 1)))
79	78	biimpd 219	. . . . . . . . . . . 12 ⊢ ((¬ 𝑃 = 2 ∧ (𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ)) → (∃𝑘 ∈ ℕ (𝑘 · (2↑(𝑁 + 1))) = (𝑃 − 1) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 1))) + 1)))
80	57, 79	sylbid 230	. . . . . . . . . . 11 ⊢ ((¬ 𝑃 = 2 ∧ (𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ)) → ((2↑(𝑁 + 1)) ∥ (𝑃 − 1) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 1))) + 1)))
81	80	adantr 481	. . . . . . . . . 10 ⊢ (((¬ 𝑃 = 2 ∧ (𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ)) ∧ ((od_ℤ‘𝑃)‘2) = (2↑(𝑁 + 1))) → ((2↑(𝑁 + 1)) ∥ (𝑃 − 1) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 1))) + 1)))
82	42, 81	sylbid 230	. . . . . . . . 9 ⊢ (((¬ 𝑃 = 2 ∧ (𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ)) ∧ ((od_ℤ‘𝑃)‘2) = (2↑(𝑁 + 1))) → (((od_ℤ‘𝑃)‘2) ∥ (𝑃 − 1) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 1))) + 1)))
83	82	ex 450	. . . . . . . 8 ⊢ ((¬ 𝑃 = 2 ∧ (𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ)) → (((od_ℤ‘𝑃)‘2) = (2↑(𝑁 + 1)) → (((od_ℤ‘𝑃)‘2) ∥ (𝑃 − 1) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 1))) + 1))))
84	83	com23 86	. . . . . . 7 ⊢ ((¬ 𝑃 = 2 ∧ (𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ)) → (((od_ℤ‘𝑃)‘2) ∥ (𝑃 − 1) → (((od_ℤ‘𝑃)‘2) = (2↑(𝑁 + 1)) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 1))) + 1))))
85	40, 84	sylbid 230	. . . . . 6 ⊢ ((¬ 𝑃 = 2 ∧ (𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ)) → (((od_ℤ‘𝑃)‘2) ∥ (ϕ‘𝑃) → (((od_ℤ‘𝑃)‘2) = (2↑(𝑁 + 1)) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 1))) + 1))))
86	37, 85	mpd 15	. . . . 5 ⊢ ((¬ 𝑃 = 2 ∧ (𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ)) → (((od_ℤ‘𝑃)‘2) = (2↑(𝑁 + 1)) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 1))) + 1)))
87	86	3adantr3 1222	. . . 4 ⊢ ((¬ 𝑃 = 2 ∧ (𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) → (((od_ℤ‘𝑃)‘2) = (2↑(𝑁 + 1)) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 1))) + 1)))
88	22, 87	mpd 15	. . 3 ⊢ ((¬ 𝑃 = 2 ∧ (𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁))) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 1))) + 1))
89	88	ex 450	. 2 ⊢ (¬ 𝑃 = 2 → ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 1))) + 1)))
90	11, 89	pm2.61i 176	1 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 1))) + 1))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∧ wa 384 ∧ w3a 1037 = wceq 1483 ∈ wcel 1990 ≠ wne 2794 ∃wrex 2913 ∖ cdif 3571 {csn 4177 class class class wbr 4653 ‘cfv 5888 (class class class)co 6650 ℂcc 9934 1c1 9937 + caddc 9939 · cmul 9941 ≤ cle 10075 − cmin 10266 ℕcn 11020 2c2 11070 ℕ₀cn0 11292 ℤcz 11377 ℤ_≥cuz 11687 ↑cexp 12860 ∥ cdvds 14983 gcd cgcd 15216 ℙcprime 15385 od_ℤcodz 15468 ϕcphi 15469 FermatNocfmtno 41439

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-2o 7561 df-oadd 7564 df-er 7742 df-map 7859 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-sup 8348 df-inf 8349 df-card 8765 df-cda 8990 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-n0 11293 df-xnn0 11364 df-z 11378 df-uz 11688 df-q 11789 df-rp 11833 df-fz 12327 df-fzo 12466 df-fl 12593 df-mod 12669 df-seq 12802 df-exp 12861 df-hash 13118 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-dvds 14984 df-gcd 15217 df-prm 15386 df-odz 15470 df-phi 15471 df-pc 15542 df-fmtno 41440

This theorem is referenced by: fmtnoprmfac2lem1 41478

W3C validator