| Step | Hyp | Ref
| Expression |
| 1 | | breq1 5146 |
. . . . . 6
⊢ (𝑥 = 1 → (𝑥 ∥ (FermatNo‘𝑁) ↔ 1 ∥ (FermatNo‘𝑁))) |
| 2 | 1 | anbi2d 630 |
. . . . 5
⊢ (𝑥 = 1 → ((𝑁 ∈ (ℤ≥‘2)
∧ 𝑥 ∥
(FermatNo‘𝑁)) ↔
(𝑁 ∈
(ℤ≥‘2) ∧ 1 ∥ (FermatNo‘𝑁)))) |
| 3 | | eqeq1 2741 |
. . . . . 6
⊢ (𝑥 = 1 → (𝑥 = ((𝑘 · (2↑(𝑁 + 2))) + 1) ↔ 1 = ((𝑘 · (2↑(𝑁 + 2))) + 1))) |
| 4 | 3 | rexbidv 3179 |
. . . . 5
⊢ (𝑥 = 1 → (∃𝑘 ∈ ℕ0
𝑥 = ((𝑘 · (2↑(𝑁 + 2))) + 1) ↔ ∃𝑘 ∈ ℕ0 1 =
((𝑘 · (2↑(𝑁 + 2))) + 1))) |
| 5 | 2, 4 | imbi12d 344 |
. . . 4
⊢ (𝑥 = 1 → (((𝑁 ∈ (ℤ≥‘2)
∧ 𝑥 ∥
(FermatNo‘𝑁)) →
∃𝑘 ∈
ℕ0 𝑥 =
((𝑘 · (2↑(𝑁 + 2))) + 1)) ↔ ((𝑁 ∈
(ℤ≥‘2) ∧ 1 ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ0 1 =
((𝑘 · (2↑(𝑁 + 2))) + 1)))) |
| 6 | | breq1 5146 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑥 ∥ (FermatNo‘𝑁) ↔ 𝑦 ∥ (FermatNo‘𝑁))) |
| 7 | 6 | anbi2d 630 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((𝑁 ∈ (ℤ≥‘2)
∧ 𝑥 ∥
(FermatNo‘𝑁)) ↔
(𝑁 ∈
(ℤ≥‘2) ∧ 𝑦 ∥ (FermatNo‘𝑁)))) |
| 8 | | eqeq1 2741 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑥 = ((𝑘 · (2↑(𝑁 + 2))) + 1) ↔ 𝑦 = ((𝑘 · (2↑(𝑁 + 2))) + 1))) |
| 9 | 8 | rexbidv 3179 |
. . . . 5
⊢ (𝑥 = 𝑦 → (∃𝑘 ∈ ℕ0 𝑥 = ((𝑘 · (2↑(𝑁 + 2))) + 1) ↔ ∃𝑘 ∈ ℕ0
𝑦 = ((𝑘 · (2↑(𝑁 + 2))) + 1))) |
| 10 | 7, 9 | imbi12d 344 |
. . . 4
⊢ (𝑥 = 𝑦 → (((𝑁 ∈ (ℤ≥‘2)
∧ 𝑥 ∥
(FermatNo‘𝑁)) →
∃𝑘 ∈
ℕ0 𝑥 =
((𝑘 · (2↑(𝑁 + 2))) + 1)) ↔ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑦 ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ0 𝑦 = ((𝑘 · (2↑(𝑁 + 2))) + 1)))) |
| 11 | | breq1 5146 |
. . . . . 6
⊢ (𝑥 = 𝑧 → (𝑥 ∥ (FermatNo‘𝑁) ↔ 𝑧 ∥ (FermatNo‘𝑁))) |
| 12 | 11 | anbi2d 630 |
. . . . 5
⊢ (𝑥 = 𝑧 → ((𝑁 ∈ (ℤ≥‘2)
∧ 𝑥 ∥
(FermatNo‘𝑁)) ↔
(𝑁 ∈
(ℤ≥‘2) ∧ 𝑧 ∥ (FermatNo‘𝑁)))) |
| 13 | | eqeq1 2741 |
. . . . . 6
⊢ (𝑥 = 𝑧 → (𝑥 = ((𝑘 · (2↑(𝑁 + 2))) + 1) ↔ 𝑧 = ((𝑘 · (2↑(𝑁 + 2))) + 1))) |
| 14 | 13 | rexbidv 3179 |
. . . . 5
⊢ (𝑥 = 𝑧 → (∃𝑘 ∈ ℕ0 𝑥 = ((𝑘 · (2↑(𝑁 + 2))) + 1) ↔ ∃𝑘 ∈ ℕ0
𝑧 = ((𝑘 · (2↑(𝑁 + 2))) + 1))) |
| 15 | 12, 14 | imbi12d 344 |
. . . 4
⊢ (𝑥 = 𝑧 → (((𝑁 ∈ (ℤ≥‘2)
∧ 𝑥 ∥
(FermatNo‘𝑁)) →
∃𝑘 ∈
ℕ0 𝑥 =
((𝑘 · (2↑(𝑁 + 2))) + 1)) ↔ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑧 ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ0 𝑧 = ((𝑘 · (2↑(𝑁 + 2))) + 1)))) |
| 16 | | breq1 5146 |
. . . . . 6
⊢ (𝑥 = (𝑦 · 𝑧) → (𝑥 ∥ (FermatNo‘𝑁) ↔ (𝑦 · 𝑧) ∥ (FermatNo‘𝑁))) |
| 17 | 16 | anbi2d 630 |
. . . . 5
⊢ (𝑥 = (𝑦 · 𝑧) → ((𝑁 ∈ (ℤ≥‘2)
∧ 𝑥 ∥
(FermatNo‘𝑁)) ↔
(𝑁 ∈
(ℤ≥‘2) ∧ (𝑦 · 𝑧) ∥ (FermatNo‘𝑁)))) |
| 18 | | eqeq1 2741 |
. . . . . 6
⊢ (𝑥 = (𝑦 · 𝑧) → (𝑥 = ((𝑘 · (2↑(𝑁 + 2))) + 1) ↔ (𝑦 · 𝑧) = ((𝑘 · (2↑(𝑁 + 2))) + 1))) |
| 19 | 18 | rexbidv 3179 |
. . . . 5
⊢ (𝑥 = (𝑦 · 𝑧) → (∃𝑘 ∈ ℕ0 𝑥 = ((𝑘 · (2↑(𝑁 + 2))) + 1) ↔ ∃𝑘 ∈ ℕ0
(𝑦 · 𝑧) = ((𝑘 · (2↑(𝑁 + 2))) + 1))) |
| 20 | 17, 19 | imbi12d 344 |
. . . 4
⊢ (𝑥 = (𝑦 · 𝑧) → (((𝑁 ∈ (ℤ≥‘2)
∧ 𝑥 ∥
(FermatNo‘𝑁)) →
∃𝑘 ∈
ℕ0 𝑥 =
((𝑘 · (2↑(𝑁 + 2))) + 1)) ↔ ((𝑁 ∈
(ℤ≥‘2) ∧ (𝑦 · 𝑧) ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ0 (𝑦 · 𝑧) = ((𝑘 · (2↑(𝑁 + 2))) + 1)))) |
| 21 | | breq1 5146 |
. . . . . 6
⊢ (𝑥 = 𝑀 → (𝑥 ∥ (FermatNo‘𝑁) ↔ 𝑀 ∥ (FermatNo‘𝑁))) |
| 22 | 21 | anbi2d 630 |
. . . . 5
⊢ (𝑥 = 𝑀 → ((𝑁 ∈ (ℤ≥‘2)
∧ 𝑥 ∥
(FermatNo‘𝑁)) ↔
(𝑁 ∈
(ℤ≥‘2) ∧ 𝑀 ∥ (FermatNo‘𝑁)))) |
| 23 | | eqeq1 2741 |
. . . . . 6
⊢ (𝑥 = 𝑀 → (𝑥 = ((𝑘 · (2↑(𝑁 + 2))) + 1) ↔ 𝑀 = ((𝑘 · (2↑(𝑁 + 2))) + 1))) |
| 24 | 23 | rexbidv 3179 |
. . . . 5
⊢ (𝑥 = 𝑀 → (∃𝑘 ∈ ℕ0 𝑥 = ((𝑘 · (2↑(𝑁 + 2))) + 1) ↔ ∃𝑘 ∈ ℕ0
𝑀 = ((𝑘 · (2↑(𝑁 + 2))) + 1))) |
| 25 | 22, 24 | imbi12d 344 |
. . . 4
⊢ (𝑥 = 𝑀 → (((𝑁 ∈ (ℤ≥‘2)
∧ 𝑥 ∥
(FermatNo‘𝑁)) →
∃𝑘 ∈
ℕ0 𝑥 =
((𝑘 · (2↑(𝑁 + 2))) + 1)) ↔ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑀 ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ0 𝑀 = ((𝑘 · (2↑(𝑁 + 2))) + 1)))) |
| 26 | | 0nn0 12541 |
. . . . . . 7
⊢ 0 ∈
ℕ0 |
| 27 | 26 | a1i 11 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → 0 ∈
ℕ0) |
| 28 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑘 = 0 → (𝑘 · (2↑(𝑁 + 2))) = (0 · (2↑(𝑁 + 2)))) |
| 29 | 28 | oveq1d 7446 |
. . . . . . . 8
⊢ (𝑘 = 0 → ((𝑘 · (2↑(𝑁 + 2))) + 1) = ((0 · (2↑(𝑁 + 2))) + 1)) |
| 30 | 29 | eqeq2d 2748 |
. . . . . . 7
⊢ (𝑘 = 0 → (1 = ((𝑘 · (2↑(𝑁 + 2))) + 1) ↔ 1 = ((0
· (2↑(𝑁 + 2)))
+ 1))) |
| 31 | 30 | adantl 481 |
. . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑘 = 0) → (1 = ((𝑘 · (2↑(𝑁 + 2))) + 1) ↔ 1 = ((0 ·
(2↑(𝑁 + 2))) +
1))) |
| 32 | | 2nn0 12543 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℕ0 |
| 33 | 32 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘2) → 2 ∈
ℕ0) |
| 34 | | eluzge2nn0 12929 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘2) → 𝑁 ∈
ℕ0) |
| 35 | 34, 33 | nn0addcld 12591 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 + 2) ∈
ℕ0) |
| 36 | 33, 35 | nn0expcld 14285 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘2) → (2↑(𝑁 + 2)) ∈
ℕ0) |
| 37 | 36 | nn0cnd 12589 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘2) → (2↑(𝑁 + 2)) ∈ ℂ) |
| 38 | 37 | mul02d 11459 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘2) → (0 · (2↑(𝑁 + 2))) = 0) |
| 39 | 38 | oveq1d 7446 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘2) → ((0 · (2↑(𝑁 + 2))) + 1) = (0 + 1)) |
| 40 | | 0p1e1 12388 |
. . . . . . 7
⊢ (0 + 1) =
1 |
| 41 | 39, 40 | eqtr2di 2794 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → 1 = ((0 · (2↑(𝑁 + 2))) + 1)) |
| 42 | 27, 31, 41 | rspcedvd 3624 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘2) → ∃𝑘 ∈ ℕ0 1 = ((𝑘 · (2↑(𝑁 + 2))) + 1)) |
| 43 | 42 | adantr 480 |
. . . 4
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ 1 ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ0 1 =
((𝑘 · (2↑(𝑁 + 2))) + 1)) |
| 44 | | simpl 482 |
. . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑥 ∥ (FermatNo‘𝑁)) → 𝑁 ∈
(ℤ≥‘2)) |
| 45 | 44 | adantl 481 |
. . . . . 6
⊢ ((𝑥 ∈ ℙ ∧ (𝑁 ∈
(ℤ≥‘2) ∧ 𝑥 ∥ (FermatNo‘𝑁))) → 𝑁 ∈
(ℤ≥‘2)) |
| 46 | | simpl 482 |
. . . . . 6
⊢ ((𝑥 ∈ ℙ ∧ (𝑁 ∈
(ℤ≥‘2) ∧ 𝑥 ∥ (FermatNo‘𝑁))) → 𝑥 ∈ ℙ) |
| 47 | | simprr 773 |
. . . . . 6
⊢ ((𝑥 ∈ ℙ ∧ (𝑁 ∈
(ℤ≥‘2) ∧ 𝑥 ∥ (FermatNo‘𝑁))) → 𝑥 ∥ (FermatNo‘𝑁)) |
| 48 | | nnssnn0 12529 |
. . . . . . 7
⊢ ℕ
⊆ ℕ0 |
| 49 | | fmtnoprmfac2 47554 |
. . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑥 ∈ ℙ ∧ 𝑥 ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ 𝑥 = ((𝑘 · (2↑(𝑁 + 2))) + 1)) |
| 50 | | ssrexv 4053 |
. . . . . . 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 1373 |
. . . . 5
⊢ ((𝑥 ∈ ℙ ∧ (𝑁 ∈
(ℤ≥‘2) ∧ 𝑥 ∥ (FermatNo‘𝑁))) → ∃𝑘 ∈ ℕ0 𝑥 = ((𝑘 · (2↑(𝑁 + 2))) + 1)) |
| 53 | 52 | ex 412 |
. . . 4
⊢ (𝑥 ∈ ℙ → ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑥 ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ0 𝑥 = ((𝑘 · (2↑(𝑁 + 2))) + 1))) |
| 54 | | fmtnofac2lem 47555 |
. . . 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 16723 |
. . 3
⊢ (𝑀 ∈ ℕ → ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑀 ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ0 𝑀 = ((𝑘 · (2↑(𝑁 + 2))) + 1))) |
| 56 | 55 | expd 415 |
. 2
⊢ (𝑀 ∈ ℕ → (𝑁 ∈
(ℤ≥‘2) → (𝑀 ∥ (FermatNo‘𝑁) → ∃𝑘 ∈ ℕ0 𝑀 = ((𝑘 · (2↑(𝑁 + 2))) + 1)))) |
| 57 | 56 | 3imp21 1114 |
1
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑀 ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ0 𝑀 = ((𝑘 · (2↑(𝑁 + 2))) + 1)) |