Step | Hyp | Ref
| Expression |
1 | | breq1 5043 |
. . . . . 6
⊢ (𝑥 = 1 → (𝑥 ∥ (FermatNo‘𝑁) ↔ 1 ∥ (FermatNo‘𝑁))) |
2 | 1 | anbi2d 632 |
. . . . 5
⊢ (𝑥 = 1 → ((𝑁 ∈ (ℤ≥‘2)
∧ 𝑥 ∥
(FermatNo‘𝑁)) ↔
(𝑁 ∈
(ℤ≥‘2) ∧ 1 ∥ (FermatNo‘𝑁)))) |
3 | | eqeq1 2743 |
. . . . . 6
⊢ (𝑥 = 1 → (𝑥 = ((𝑘 · (2↑(𝑁 + 2))) + 1) ↔ 1 = ((𝑘 · (2↑(𝑁 + 2))) + 1))) |
4 | 3 | rexbidv 3208 |
. . . . 5
⊢ (𝑥 = 1 → (∃𝑘 ∈ ℕ0
𝑥 = ((𝑘 · (2↑(𝑁 + 2))) + 1) ↔ ∃𝑘 ∈ ℕ0 1 =
((𝑘 · (2↑(𝑁 + 2))) + 1))) |
5 | 2, 4 | imbi12d 348 |
. . . 4
⊢ (𝑥 = 1 → (((𝑁 ∈ (ℤ≥‘2)
∧ 𝑥 ∥
(FermatNo‘𝑁)) →
∃𝑘 ∈
ℕ0 𝑥 =
((𝑘 · (2↑(𝑁 + 2))) + 1)) ↔ ((𝑁 ∈
(ℤ≥‘2) ∧ 1 ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ0 1 =
((𝑘 · (2↑(𝑁 + 2))) + 1)))) |
6 | | breq1 5043 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑥 ∥ (FermatNo‘𝑁) ↔ 𝑦 ∥ (FermatNo‘𝑁))) |
7 | 6 | anbi2d 632 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((𝑁 ∈ (ℤ≥‘2)
∧ 𝑥 ∥
(FermatNo‘𝑁)) ↔
(𝑁 ∈
(ℤ≥‘2) ∧ 𝑦 ∥ (FermatNo‘𝑁)))) |
8 | | eqeq1 2743 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑥 = ((𝑘 · (2↑(𝑁 + 2))) + 1) ↔ 𝑦 = ((𝑘 · (2↑(𝑁 + 2))) + 1))) |
9 | 8 | rexbidv 3208 |
. . . . 5
⊢ (𝑥 = 𝑦 → (∃𝑘 ∈ ℕ0 𝑥 = ((𝑘 · (2↑(𝑁 + 2))) + 1) ↔ ∃𝑘 ∈ ℕ0
𝑦 = ((𝑘 · (2↑(𝑁 + 2))) + 1))) |
10 | 7, 9 | imbi12d 348 |
. . . 4
⊢ (𝑥 = 𝑦 → (((𝑁 ∈ (ℤ≥‘2)
∧ 𝑥 ∥
(FermatNo‘𝑁)) →
∃𝑘 ∈
ℕ0 𝑥 =
((𝑘 · (2↑(𝑁 + 2))) + 1)) ↔ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑦 ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ0 𝑦 = ((𝑘 · (2↑(𝑁 + 2))) + 1)))) |
11 | | breq1 5043 |
. . . . . 6
⊢ (𝑥 = 𝑧 → (𝑥 ∥ (FermatNo‘𝑁) ↔ 𝑧 ∥ (FermatNo‘𝑁))) |
12 | 11 | anbi2d 632 |
. . . . 5
⊢ (𝑥 = 𝑧 → ((𝑁 ∈ (ℤ≥‘2)
∧ 𝑥 ∥
(FermatNo‘𝑁)) ↔
(𝑁 ∈
(ℤ≥‘2) ∧ 𝑧 ∥ (FermatNo‘𝑁)))) |
13 | | eqeq1 2743 |
. . . . . 6
⊢ (𝑥 = 𝑧 → (𝑥 = ((𝑘 · (2↑(𝑁 + 2))) + 1) ↔ 𝑧 = ((𝑘 · (2↑(𝑁 + 2))) + 1))) |
14 | 13 | rexbidv 3208 |
. . . . 5
⊢ (𝑥 = 𝑧 → (∃𝑘 ∈ ℕ0 𝑥 = ((𝑘 · (2↑(𝑁 + 2))) + 1) ↔ ∃𝑘 ∈ ℕ0
𝑧 = ((𝑘 · (2↑(𝑁 + 2))) + 1))) |
15 | 12, 14 | imbi12d 348 |
. . . 4
⊢ (𝑥 = 𝑧 → (((𝑁 ∈ (ℤ≥‘2)
∧ 𝑥 ∥
(FermatNo‘𝑁)) →
∃𝑘 ∈
ℕ0 𝑥 =
((𝑘 · (2↑(𝑁 + 2))) + 1)) ↔ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑧 ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ0 𝑧 = ((𝑘 · (2↑(𝑁 + 2))) + 1)))) |
16 | | breq1 5043 |
. . . . . 6
⊢ (𝑥 = (𝑦 · 𝑧) → (𝑥 ∥ (FermatNo‘𝑁) ↔ (𝑦 · 𝑧) ∥ (FermatNo‘𝑁))) |
17 | 16 | anbi2d 632 |
. . . . 5
⊢ (𝑥 = (𝑦 · 𝑧) → ((𝑁 ∈ (ℤ≥‘2)
∧ 𝑥 ∥
(FermatNo‘𝑁)) ↔
(𝑁 ∈
(ℤ≥‘2) ∧ (𝑦 · 𝑧) ∥ (FermatNo‘𝑁)))) |
18 | | eqeq1 2743 |
. . . . . 6
⊢ (𝑥 = (𝑦 · 𝑧) → (𝑥 = ((𝑘 · (2↑(𝑁 + 2))) + 1) ↔ (𝑦 · 𝑧) = ((𝑘 · (2↑(𝑁 + 2))) + 1))) |
19 | 18 | rexbidv 3208 |
. . . . 5
⊢ (𝑥 = (𝑦 · 𝑧) → (∃𝑘 ∈ ℕ0 𝑥 = ((𝑘 · (2↑(𝑁 + 2))) + 1) ↔ ∃𝑘 ∈ ℕ0
(𝑦 · 𝑧) = ((𝑘 · (2↑(𝑁 + 2))) + 1))) |
20 | 17, 19 | imbi12d 348 |
. . . 4
⊢ (𝑥 = (𝑦 · 𝑧) → (((𝑁 ∈ (ℤ≥‘2)
∧ 𝑥 ∥
(FermatNo‘𝑁)) →
∃𝑘 ∈
ℕ0 𝑥 =
((𝑘 · (2↑(𝑁 + 2))) + 1)) ↔ ((𝑁 ∈
(ℤ≥‘2) ∧ (𝑦 · 𝑧) ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ0 (𝑦 · 𝑧) = ((𝑘 · (2↑(𝑁 + 2))) + 1)))) |
21 | | breq1 5043 |
. . . . . 6
⊢ (𝑥 = 𝑀 → (𝑥 ∥ (FermatNo‘𝑁) ↔ 𝑀 ∥ (FermatNo‘𝑁))) |
22 | 21 | anbi2d 632 |
. . . . 5
⊢ (𝑥 = 𝑀 → ((𝑁 ∈ (ℤ≥‘2)
∧ 𝑥 ∥
(FermatNo‘𝑁)) ↔
(𝑁 ∈
(ℤ≥‘2) ∧ 𝑀 ∥ (FermatNo‘𝑁)))) |
23 | | eqeq1 2743 |
. . . . . 6
⊢ (𝑥 = 𝑀 → (𝑥 = ((𝑘 · (2↑(𝑁 + 2))) + 1) ↔ 𝑀 = ((𝑘 · (2↑(𝑁 + 2))) + 1))) |
24 | 23 | rexbidv 3208 |
. . . . 5
⊢ (𝑥 = 𝑀 → (∃𝑘 ∈ ℕ0 𝑥 = ((𝑘 · (2↑(𝑁 + 2))) + 1) ↔ ∃𝑘 ∈ ℕ0
𝑀 = ((𝑘 · (2↑(𝑁 + 2))) + 1))) |
25 | 22, 24 | imbi12d 348 |
. . . 4
⊢ (𝑥 = 𝑀 → (((𝑁 ∈ (ℤ≥‘2)
∧ 𝑥 ∥
(FermatNo‘𝑁)) →
∃𝑘 ∈
ℕ0 𝑥 =
((𝑘 · (2↑(𝑁 + 2))) + 1)) ↔ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑀 ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ0 𝑀 = ((𝑘 · (2↑(𝑁 + 2))) + 1)))) |
26 | | 0nn0 12003 |
. . . . . . 7
⊢ 0 ∈
ℕ0 |
27 | 26 | a1i 11 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → 0 ∈
ℕ0) |
28 | | oveq1 7189 |
. . . . . . . . 9
⊢ (𝑘 = 0 → (𝑘 · (2↑(𝑁 + 2))) = (0 · (2↑(𝑁 + 2)))) |
29 | 28 | oveq1d 7197 |
. . . . . . . 8
⊢ (𝑘 = 0 → ((𝑘 · (2↑(𝑁 + 2))) + 1) = ((0 · (2↑(𝑁 + 2))) + 1)) |
30 | 29 | eqeq2d 2750 |
. . . . . . 7
⊢ (𝑘 = 0 → (1 = ((𝑘 · (2↑(𝑁 + 2))) + 1) ↔ 1 = ((0
· (2↑(𝑁 + 2)))
+ 1))) |
31 | 30 | adantl 485 |
. . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑘 = 0) → (1 = ((𝑘 · (2↑(𝑁 + 2))) + 1) ↔ 1 = ((0 ·
(2↑(𝑁 + 2))) +
1))) |
32 | | 2nn0 12005 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℕ0 |
33 | 32 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘2) → 2 ∈
ℕ0) |
34 | | eluzge2nn0 12381 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘2) → 𝑁 ∈
ℕ0) |
35 | 34, 33 | nn0addcld 12052 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 + 2) ∈
ℕ0) |
36 | 33, 35 | nn0expcld 13711 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘2) → (2↑(𝑁 + 2)) ∈
ℕ0) |
37 | 36 | nn0cnd 12050 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘2) → (2↑(𝑁 + 2)) ∈ ℂ) |
38 | 37 | mul02d 10928 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘2) → (0 · (2↑(𝑁 + 2))) = 0) |
39 | 38 | oveq1d 7197 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘2) → ((0 · (2↑(𝑁 + 2))) + 1) = (0 + 1)) |
40 | | 0p1e1 11850 |
. . . . . . 7
⊢ (0 + 1) =
1 |
41 | 39, 40 | eqtr2di 2791 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → 1 = ((0 · (2↑(𝑁 + 2))) + 1)) |
42 | 27, 31, 41 | rspcedvd 3532 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘2) → ∃𝑘 ∈ ℕ0 1 = ((𝑘 · (2↑(𝑁 + 2))) + 1)) |
43 | 42 | adantr 484 |
. . . 4
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ 1 ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ0 1 =
((𝑘 · (2↑(𝑁 + 2))) + 1)) |
44 | | simpl 486 |
. . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑥 ∥ (FermatNo‘𝑁)) → 𝑁 ∈
(ℤ≥‘2)) |
45 | 44 | adantl 485 |
. . . . . 6
⊢ ((𝑥 ∈ ℙ ∧ (𝑁 ∈
(ℤ≥‘2) ∧ 𝑥 ∥ (FermatNo‘𝑁))) → 𝑁 ∈
(ℤ≥‘2)) |
46 | | simpl 486 |
. . . . . 6
⊢ ((𝑥 ∈ ℙ ∧ (𝑁 ∈
(ℤ≥‘2) ∧ 𝑥 ∥ (FermatNo‘𝑁))) → 𝑥 ∈ ℙ) |
47 | | simprr 773 |
. . . . . 6
⊢ ((𝑥 ∈ ℙ ∧ (𝑁 ∈
(ℤ≥‘2) ∧ 𝑥 ∥ (FermatNo‘𝑁))) → 𝑥 ∥ (FermatNo‘𝑁)) |
48 | | nnssnn0 11991 |
. . . . . . 7
⊢ ℕ
⊆ ℕ0 |
49 | | fmtnoprmfac2 44600 |
. . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑥 ∈ ℙ ∧ 𝑥 ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ 𝑥 = ((𝑘 · (2↑(𝑁 + 2))) + 1)) |
50 | | ssrexv 3954 |
. . . . . . 7
⊢ (ℕ
⊆ ℕ0 → (∃𝑘 ∈ ℕ 𝑥 = ((𝑘 · (2↑(𝑁 + 2))) + 1) → ∃𝑘 ∈ ℕ0
𝑥 = ((𝑘 · (2↑(𝑁 + 2))) + 1))) |
51 | 48, 49, 50 | mpsyl 68 |
. . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑥 ∈ ℙ ∧ 𝑥 ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ0 𝑥 = ((𝑘 · (2↑(𝑁 + 2))) + 1)) |
52 | 45, 46, 47, 51 | syl3anc 1372 |
. . . . 5
⊢ ((𝑥 ∈ ℙ ∧ (𝑁 ∈
(ℤ≥‘2) ∧ 𝑥 ∥ (FermatNo‘𝑁))) → ∃𝑘 ∈ ℕ0 𝑥 = ((𝑘 · (2↑(𝑁 + 2))) + 1)) |
53 | 52 | ex 416 |
. . . 4
⊢ (𝑥 ∈ ℙ → ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑥 ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ0 𝑥 = ((𝑘 · (2↑(𝑁 + 2))) + 1))) |
54 | | fmtnofac2lem 44601 |
. . . 4
⊢ ((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
→ ((((𝑁 ∈
(ℤ≥‘2) ∧ 𝑦 ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ0 𝑦 = ((𝑘 · (2↑(𝑁 + 2))) + 1)) ∧ ((𝑁 ∈ (ℤ≥‘2)
∧ 𝑧 ∥
(FermatNo‘𝑁)) →
∃𝑘 ∈
ℕ0 𝑧 =
((𝑘 · (2↑(𝑁 + 2))) + 1))) → ((𝑁 ∈
(ℤ≥‘2) ∧ (𝑦 · 𝑧) ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ0 (𝑦 · 𝑧) = ((𝑘 · (2↑(𝑁 + 2))) + 1)))) |
55 | 5, 10, 15, 20, 25, 43, 53, 54 | prmind 16139 |
. . 3
⊢ (𝑀 ∈ ℕ → ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑀 ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ0 𝑀 = ((𝑘 · (2↑(𝑁 + 2))) + 1))) |
56 | 55 | expd 419 |
. 2
⊢ (𝑀 ∈ ℕ → (𝑁 ∈
(ℤ≥‘2) → (𝑀 ∥ (FermatNo‘𝑁) → ∃𝑘 ∈ ℕ0 𝑀 = ((𝑘 · (2↑(𝑁 + 2))) + 1)))) |
57 | 56 | 3imp21 1115 |
1
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑀 ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ0 𝑀 = ((𝑘 · (2↑(𝑁 + 2))) + 1)) |