Step | Hyp | Ref
| Expression |
1 | | eluzelz 12448 |
. . . . . 6
⊢ (𝑦 ∈
(ℤ≥‘2) → 𝑦 ∈ ℤ) |
2 | 1 | adantr 484 |
. . . . 5
⊢ ((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
→ 𝑦 ∈
ℤ) |
3 | | eluzelz 12448 |
. . . . . 6
⊢ (𝑧 ∈
(ℤ≥‘2) → 𝑧 ∈ ℤ) |
4 | 3 | adantl 485 |
. . . . 5
⊢ ((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
→ 𝑧 ∈
ℤ) |
5 | | eluzge2nn0 12483 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → 𝑁 ∈
ℕ0) |
6 | | fmtnonn 44656 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (FermatNo‘𝑁)
∈ ℕ) |
7 | 6 | nnzd 12281 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (FermatNo‘𝑁)
∈ ℤ) |
8 | 5, 7 | syl 17 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘2) → (FermatNo‘𝑁) ∈ ℤ) |
9 | | muldvds2 15843 |
. . . . 5
⊢ ((𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ∧
(FermatNo‘𝑁) ∈
ℤ) → ((𝑦
· 𝑧) ∥
(FermatNo‘𝑁) →
𝑧 ∥
(FermatNo‘𝑁))) |
10 | 2, 4, 8, 9 | syl2an3an 1424 |
. . . 4
⊢ (((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ 𝑁 ∈
(ℤ≥‘2)) → ((𝑦 · 𝑧) ∥ (FermatNo‘𝑁) → 𝑧 ∥ (FermatNo‘𝑁))) |
11 | | muldvds1 15842 |
. . . . . 6
⊢ ((𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ∧
(FermatNo‘𝑁) ∈
ℤ) → ((𝑦
· 𝑧) ∥
(FermatNo‘𝑁) →
𝑦 ∥
(FermatNo‘𝑁))) |
12 | 2, 4, 8, 11 | syl2an3an 1424 |
. . . . 5
⊢ (((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ 𝑁 ∈
(ℤ≥‘2)) → ((𝑦 · 𝑧) ∥ (FermatNo‘𝑁) → 𝑦 ∥ (FermatNo‘𝑁))) |
13 | | pm2.27 42 |
. . . . . . . 8
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑦 ∥ (FermatNo‘𝑁)) → (((𝑁 ∈ (ℤ≥‘2)
∧ 𝑦 ∥
(FermatNo‘𝑁)) →
∃𝑘 ∈
ℕ0 𝑦 =
((𝑘 · (2↑(𝑁 + 2))) + 1)) →
∃𝑘 ∈
ℕ0 𝑦 =
((𝑘 · (2↑(𝑁 + 2))) + 1))) |
14 | 13 | ad2ant2lr 748 |
. . . . . . 7
⊢ ((((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ 𝑁 ∈
(ℤ≥‘2)) ∧ (𝑦 ∥ (FermatNo‘𝑁) ∧ 𝑧 ∥ (FermatNo‘𝑁))) → (((𝑁 ∈ (ℤ≥‘2)
∧ 𝑦 ∥
(FermatNo‘𝑁)) →
∃𝑘 ∈
ℕ0 𝑦 =
((𝑘 · (2↑(𝑁 + 2))) + 1)) →
∃𝑘 ∈
ℕ0 𝑦 =
((𝑘 · (2↑(𝑁 + 2))) + 1))) |
15 | | pm2.27 42 |
. . . . . . . 8
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑧 ∥ (FermatNo‘𝑁)) → (((𝑁 ∈ (ℤ≥‘2)
∧ 𝑧 ∥
(FermatNo‘𝑁)) →
∃𝑘 ∈
ℕ0 𝑧 =
((𝑘 · (2↑(𝑁 + 2))) + 1)) →
∃𝑘 ∈
ℕ0 𝑧 =
((𝑘 · (2↑(𝑁 + 2))) + 1))) |
16 | 15 | ad2ant2l 746 |
. . . . . . 7
⊢ ((((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ 𝑁 ∈
(ℤ≥‘2)) ∧ (𝑦 ∥ (FermatNo‘𝑁) ∧ 𝑧 ∥ (FermatNo‘𝑁))) → (((𝑁 ∈ (ℤ≥‘2)
∧ 𝑧 ∥
(FermatNo‘𝑁)) →
∃𝑘 ∈
ℕ0 𝑧 =
((𝑘 · (2↑(𝑁 + 2))) + 1)) →
∃𝑘 ∈
ℕ0 𝑧 =
((𝑘 · (2↑(𝑁 + 2))) + 1))) |
17 | | oveq1 7220 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑚 → (𝑘 · (2↑(𝑁 + 2))) = (𝑚 · (2↑(𝑁 + 2)))) |
18 | 17 | oveq1d 7228 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑚 → ((𝑘 · (2↑(𝑁 + 2))) + 1) = ((𝑚 · (2↑(𝑁 + 2))) + 1)) |
19 | 18 | eqeq2d 2748 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑚 → (𝑦 = ((𝑘 · (2↑(𝑁 + 2))) + 1) ↔ 𝑦 = ((𝑚 · (2↑(𝑁 + 2))) + 1))) |
20 | 19 | cbvrexvw 3359 |
. . . . . . . . . 10
⊢
(∃𝑘 ∈
ℕ0 𝑦 =
((𝑘 · (2↑(𝑁 + 2))) + 1) ↔ ∃𝑚 ∈ ℕ0
𝑦 = ((𝑚 · (2↑(𝑁 + 2))) + 1)) |
21 | | oveq1 7220 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑛 → (𝑘 · (2↑(𝑁 + 2))) = (𝑛 · (2↑(𝑁 + 2)))) |
22 | 21 | oveq1d 7228 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑛 → ((𝑘 · (2↑(𝑁 + 2))) + 1) = ((𝑛 · (2↑(𝑁 + 2))) + 1)) |
23 | 22 | eqeq2d 2748 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑛 → (𝑧 = ((𝑘 · (2↑(𝑁 + 2))) + 1) ↔ 𝑧 = ((𝑛 · (2↑(𝑁 + 2))) + 1))) |
24 | 23 | cbvrexvw 3359 |
. . . . . . . . . . . . 13
⊢
(∃𝑘 ∈
ℕ0 𝑧 =
((𝑘 · (2↑(𝑁 + 2))) + 1) ↔ ∃𝑛 ∈ ℕ0
𝑧 = ((𝑛 · (2↑(𝑁 + 2))) + 1)) |
25 | | simpl 486 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑚 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) → 𝑚 ∈ ℕ0) |
26 | 25 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ (𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
→ 𝑚 ∈
ℕ0) |
27 | | 2nn0 12107 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 2 ∈
ℕ0 |
28 | 27 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈
(ℤ≥‘2) → 2 ∈
ℕ0) |
29 | 5, 28 | nn0addcld 12154 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 + 2) ∈
ℕ0) |
30 | 28, 29 | nn0expcld 13813 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈
(ℤ≥‘2) → (2↑(𝑁 + 2)) ∈
ℕ0) |
31 | 30 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ (𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
→ (2↑(𝑁 + 2))
∈ ℕ0) |
32 | 26, 31 | nn0mulcld 12155 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ (𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
→ (𝑚 ·
(2↑(𝑁 + 2))) ∈
ℕ0) |
33 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑚 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) → 𝑛 ∈ ℕ0) |
34 | 33 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ (𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
→ 𝑛 ∈
ℕ0) |
35 | 32, 34 | nn0mulcld 12155 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ (𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
→ ((𝑚 ·
(2↑(𝑁 + 2))) ·
𝑛) ∈
ℕ0) |
36 | | nn0addcl 12125 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑚 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) → (𝑚 + 𝑛) ∈
ℕ0) |
37 | 36 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ (𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
→ (𝑚 + 𝑛) ∈
ℕ0) |
38 | 35, 37 | nn0addcld 12154 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ (𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
→ (((𝑚 ·
(2↑(𝑁 + 2))) ·
𝑛) + (𝑚 + 𝑛)) ∈
ℕ0) |
39 | | oveq1 7220 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 = (((𝑚 · (2↑(𝑁 + 2))) · 𝑛) + (𝑚 + 𝑛)) → (𝑘 · (2↑(𝑁 + 2))) = ((((𝑚 · (2↑(𝑁 + 2))) · 𝑛) + (𝑚 + 𝑛)) · (2↑(𝑁 + 2)))) |
40 | 39 | oveq1d 7228 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 = (((𝑚 · (2↑(𝑁 + 2))) · 𝑛) + (𝑚 + 𝑛)) → ((𝑘 · (2↑(𝑁 + 2))) + 1) = (((((𝑚 · (2↑(𝑁 + 2))) · 𝑛) + (𝑚 + 𝑛)) · (2↑(𝑁 + 2))) + 1)) |
41 | 40 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = (((𝑚 · (2↑(𝑁 + 2))) · 𝑛) + (𝑚 + 𝑛)) → ((((((𝑚 · (2↑(𝑁 + 2))) · 𝑛) + (𝑚 + 𝑛)) · (2↑(𝑁 + 2))) + 1) = ((𝑘 · (2↑(𝑁 + 2))) + 1) ↔ (((((𝑚 · (2↑(𝑁 + 2))) · 𝑛) + (𝑚 + 𝑛)) · (2↑(𝑁 + 2))) + 1) = (((((𝑚 · (2↑(𝑁 + 2))) · 𝑛) + (𝑚 + 𝑛)) · (2↑(𝑁 + 2))) + 1))) |
42 | 41 | adantl 485 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ (𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ 𝑘 = (((𝑚 · (2↑(𝑁 + 2))) · 𝑛) + (𝑚 + 𝑛))) → ((((((𝑚 · (2↑(𝑁 + 2))) · 𝑛) + (𝑚 + 𝑛)) · (2↑(𝑁 + 2))) + 1) = ((𝑘 · (2↑(𝑁 + 2))) + 1) ↔ (((((𝑚 · (2↑(𝑁 + 2))) · 𝑛) + (𝑚 + 𝑛)) · (2↑(𝑁 + 2))) + 1) = (((((𝑚 · (2↑(𝑁 + 2))) · 𝑛) + (𝑚 + 𝑛)) · (2↑(𝑁 + 2))) + 1))) |
43 | | eqidd 2738 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ (𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
→ (((((𝑚 ·
(2↑(𝑁 + 2))) ·
𝑛) + (𝑚 + 𝑛)) · (2↑(𝑁 + 2))) + 1) = (((((𝑚 · (2↑(𝑁 + 2))) · 𝑛) + (𝑚 + 𝑛)) · (2↑(𝑁 + 2))) + 1)) |
44 | 38, 42, 43 | rspcedvd 3540 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ (𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
→ ∃𝑘 ∈
ℕ0 (((((𝑚
· (2↑(𝑁 + 2)))
· 𝑛) + (𝑚 + 𝑛)) · (2↑(𝑁 + 2))) + 1) = ((𝑘 · (2↑(𝑁 + 2))) + 1)) |
45 | | nn0cn 12100 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑚 ∈ ℕ0
→ 𝑚 ∈
ℂ) |
46 | 45 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑚 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) → 𝑚 ∈ ℂ) |
47 | 46 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ (𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
→ 𝑚 ∈
ℂ) |
48 | 30 | nn0cnd 12152 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈
(ℤ≥‘2) → (2↑(𝑁 + 2)) ∈ ℂ) |
49 | 48 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ (𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
→ (2↑(𝑁 + 2))
∈ ℂ) |
50 | 47, 49 | mulcld 10853 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ (𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
→ (𝑚 ·
(2↑(𝑁 + 2))) ∈
ℂ) |
51 | 33 | nn0cnd 12152 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑚 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) → 𝑛 ∈ ℂ) |
52 | 51 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ (𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
→ 𝑛 ∈
ℂ) |
53 | 52, 49 | mulcld 10853 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ (𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
→ (𝑛 ·
(2↑(𝑁 + 2))) ∈
ℂ) |
54 | 50, 53 | jca 515 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ (𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
→ ((𝑚 ·
(2↑(𝑁 + 2))) ∈
ℂ ∧ (𝑛 ·
(2↑(𝑁 + 2))) ∈
ℂ)) |
55 | 54 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ (𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ 𝑘 ∈
ℕ0) → ((𝑚 · (2↑(𝑁 + 2))) ∈ ℂ ∧ (𝑛 · (2↑(𝑁 + 2))) ∈
ℂ)) |
56 | | muladd11r 11045 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑚 · (2↑(𝑁 + 2))) ∈ ℂ ∧
(𝑛 · (2↑(𝑁 + 2))) ∈ ℂ) →
(((𝑚 ·
(2↑(𝑁 + 2))) + 1)
· ((𝑛 ·
(2↑(𝑁 + 2))) + 1)) =
((((𝑚 ·
(2↑(𝑁 + 2))) ·
(𝑛 · (2↑(𝑁 + 2)))) + ((𝑚 · (2↑(𝑁 + 2))) + (𝑛 · (2↑(𝑁 + 2))))) + 1)) |
57 | 55, 56 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ (𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ 𝑘 ∈
ℕ0) → (((𝑚 · (2↑(𝑁 + 2))) + 1) · ((𝑛 · (2↑(𝑁 + 2))) + 1)) = ((((𝑚 · (2↑(𝑁 + 2))) · (𝑛 · (2↑(𝑁 + 2)))) + ((𝑚 · (2↑(𝑁 + 2))) + (𝑛 · (2↑(𝑁 + 2))))) + 1)) |
58 | 25 | nn0cnd 12152 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑚 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) → 𝑚 ∈ ℂ) |
59 | 58 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ (𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
→ 𝑚 ∈
ℂ) |
60 | 59, 52, 49 | 3jca 1130 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ (𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
→ (𝑚 ∈ ℂ
∧ 𝑛 ∈ ℂ
∧ (2↑(𝑁 + 2))
∈ ℂ)) |
61 | 60 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ (𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ 𝑘 ∈
ℕ0) → (𝑚 ∈ ℂ ∧ 𝑛 ∈ ℂ ∧ (2↑(𝑁 + 2)) ∈
ℂ)) |
62 | | adddir 10824 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑚 ∈ ℂ ∧ 𝑛 ∈ ℂ ∧
(2↑(𝑁 + 2)) ∈
ℂ) → ((𝑚 + 𝑛) · (2↑(𝑁 + 2))) = ((𝑚 · (2↑(𝑁 + 2))) + (𝑛 · (2↑(𝑁 + 2))))) |
63 | 61, 62 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ (𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ 𝑘 ∈
ℕ0) → ((𝑚 + 𝑛) · (2↑(𝑁 + 2))) = ((𝑚 · (2↑(𝑁 + 2))) + (𝑛 · (2↑(𝑁 + 2))))) |
64 | 63 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ (𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ 𝑘 ∈
ℕ0) → ((𝑚 · (2↑(𝑁 + 2))) + (𝑛 · (2↑(𝑁 + 2)))) = ((𝑚 + 𝑛) · (2↑(𝑁 + 2)))) |
65 | 64 | oveq2d 7229 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ (𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ 𝑘 ∈
ℕ0) → ((((𝑚 · (2↑(𝑁 + 2))) · 𝑛) · (2↑(𝑁 + 2))) + ((𝑚 · (2↑(𝑁 + 2))) + (𝑛 · (2↑(𝑁 + 2))))) = ((((𝑚 · (2↑(𝑁 + 2))) · 𝑛) · (2↑(𝑁 + 2))) + ((𝑚 + 𝑛) · (2↑(𝑁 + 2))))) |
66 | 50 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ (𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ 𝑘 ∈
ℕ0) → (𝑚 · (2↑(𝑁 + 2))) ∈ ℂ) |
67 | 52 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ (𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ 𝑘 ∈
ℕ0) → 𝑛 ∈ ℂ) |
68 | 49 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ (𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ 𝑘 ∈
ℕ0) → (2↑(𝑁 + 2)) ∈ ℂ) |
69 | 66, 67, 68 | mulassd 10856 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ (𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ 𝑘 ∈
ℕ0) → (((𝑚 · (2↑(𝑁 + 2))) · 𝑛) · (2↑(𝑁 + 2))) = ((𝑚 · (2↑(𝑁 + 2))) · (𝑛 · (2↑(𝑁 + 2))))) |
70 | 69 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ (𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ 𝑘 ∈
ℕ0) → ((𝑚 · (2↑(𝑁 + 2))) · (𝑛 · (2↑(𝑁 + 2)))) = (((𝑚 · (2↑(𝑁 + 2))) · 𝑛) · (2↑(𝑁 + 2)))) |
71 | 70 | oveq1d 7228 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ (𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ 𝑘 ∈
ℕ0) → (((𝑚 · (2↑(𝑁 + 2))) · (𝑛 · (2↑(𝑁 + 2)))) + ((𝑚 · (2↑(𝑁 + 2))) + (𝑛 · (2↑(𝑁 + 2))))) = ((((𝑚 · (2↑(𝑁 + 2))) · 𝑛) · (2↑(𝑁 + 2))) + ((𝑚 · (2↑(𝑁 + 2))) + (𝑛 · (2↑(𝑁 + 2)))))) |
72 | 50, 52 | mulcld 10853 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ (𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
→ ((𝑚 ·
(2↑(𝑁 + 2))) ·
𝑛) ∈
ℂ) |
73 | 36 | nn0cnd 12152 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑚 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) → (𝑚 + 𝑛) ∈ ℂ) |
74 | 73 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ (𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
→ (𝑚 + 𝑛) ∈
ℂ) |
75 | 72, 74, 49 | 3jca 1130 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ (𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
→ (((𝑚 ·
(2↑(𝑁 + 2))) ·
𝑛) ∈ ℂ ∧
(𝑚 + 𝑛) ∈ ℂ ∧ (2↑(𝑁 + 2)) ∈
ℂ)) |
76 | 75 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ (𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ 𝑘 ∈
ℕ0) → (((𝑚 · (2↑(𝑁 + 2))) · 𝑛) ∈ ℂ ∧ (𝑚 + 𝑛) ∈ ℂ ∧ (2↑(𝑁 + 2)) ∈
ℂ)) |
77 | | adddir 10824 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑚 · (2↑(𝑁 + 2))) · 𝑛) ∈ ℂ ∧ (𝑚 + 𝑛) ∈ ℂ ∧ (2↑(𝑁 + 2)) ∈ ℂ) →
((((𝑚 ·
(2↑(𝑁 + 2))) ·
𝑛) + (𝑚 + 𝑛)) · (2↑(𝑁 + 2))) = ((((𝑚 · (2↑(𝑁 + 2))) · 𝑛) · (2↑(𝑁 + 2))) + ((𝑚 + 𝑛) · (2↑(𝑁 + 2))))) |
78 | 76, 77 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ (𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ 𝑘 ∈
ℕ0) → ((((𝑚 · (2↑(𝑁 + 2))) · 𝑛) + (𝑚 + 𝑛)) · (2↑(𝑁 + 2))) = ((((𝑚 · (2↑(𝑁 + 2))) · 𝑛) · (2↑(𝑁 + 2))) + ((𝑚 + 𝑛) · (2↑(𝑁 + 2))))) |
79 | 65, 71, 78 | 3eqtr4d 2787 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ (𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ 𝑘 ∈
ℕ0) → (((𝑚 · (2↑(𝑁 + 2))) · (𝑛 · (2↑(𝑁 + 2)))) + ((𝑚 · (2↑(𝑁 + 2))) + (𝑛 · (2↑(𝑁 + 2))))) = ((((𝑚 · (2↑(𝑁 + 2))) · 𝑛) + (𝑚 + 𝑛)) · (2↑(𝑁 + 2)))) |
80 | 79 | oveq1d 7228 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ (𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ 𝑘 ∈
ℕ0) → ((((𝑚 · (2↑(𝑁 + 2))) · (𝑛 · (2↑(𝑁 + 2)))) + ((𝑚 · (2↑(𝑁 + 2))) + (𝑛 · (2↑(𝑁 + 2))))) + 1) = (((((𝑚 · (2↑(𝑁 + 2))) · 𝑛) + (𝑚 + 𝑛)) · (2↑(𝑁 + 2))) + 1)) |
81 | 57, 80 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ (𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ 𝑘 ∈
ℕ0) → (((𝑚 · (2↑(𝑁 + 2))) + 1) · ((𝑛 · (2↑(𝑁 + 2))) + 1)) = (((((𝑚 · (2↑(𝑁 + 2))) · 𝑛) + (𝑚 + 𝑛)) · (2↑(𝑁 + 2))) + 1)) |
82 | 81 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 ∈
(ℤ≥‘2) ∧ (𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
∧ 𝑘 ∈
ℕ0) → ((((𝑚 · (2↑(𝑁 + 2))) + 1) · ((𝑛 · (2↑(𝑁 + 2))) + 1)) = ((𝑘 · (2↑(𝑁 + 2))) + 1) ↔ (((((𝑚 · (2↑(𝑁 + 2))) · 𝑛) + (𝑚 + 𝑛)) · (2↑(𝑁 + 2))) + 1) = ((𝑘 · (2↑(𝑁 + 2))) + 1))) |
83 | 82 | rexbidva 3215 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ (𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
→ (∃𝑘 ∈
ℕ0 (((𝑚
· (2↑(𝑁 + 2)))
+ 1) · ((𝑛 ·
(2↑(𝑁 + 2))) + 1)) =
((𝑘 · (2↑(𝑁 + 2))) + 1) ↔ ∃𝑘 ∈ ℕ0
(((((𝑚 ·
(2↑(𝑁 + 2))) ·
𝑛) + (𝑚 + 𝑛)) · (2↑(𝑁 + 2))) + 1) = ((𝑘 · (2↑(𝑁 + 2))) + 1))) |
84 | 44, 83 | mpbird 260 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ (𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
→ ∃𝑘 ∈
ℕ0 (((𝑚
· (2↑(𝑁 + 2)))
+ 1) · ((𝑛 ·
(2↑(𝑁 + 2))) + 1)) =
((𝑘 · (2↑(𝑁 + 2))) + 1)) |
85 | 84 | adantll 714 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ 𝑁 ∈
(ℤ≥‘2)) ∧ (𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
→ ∃𝑘 ∈
ℕ0 (((𝑚
· (2↑(𝑁 + 2)))
+ 1) · ((𝑛 ·
(2↑(𝑁 + 2))) + 1)) =
((𝑘 · (2↑(𝑁 + 2))) + 1)) |
86 | | oveq12 7222 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 = ((𝑚 · (2↑(𝑁 + 2))) + 1) ∧ 𝑧 = ((𝑛 · (2↑(𝑁 + 2))) + 1)) → (𝑦 · 𝑧) = (((𝑚 · (2↑(𝑁 + 2))) + 1) · ((𝑛 · (2↑(𝑁 + 2))) + 1))) |
87 | 86 | ancoms 462 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑧 = ((𝑛 · (2↑(𝑁 + 2))) + 1) ∧ 𝑦 = ((𝑚 · (2↑(𝑁 + 2))) + 1)) → (𝑦 · 𝑧) = (((𝑚 · (2↑(𝑁 + 2))) + 1) · ((𝑛 · (2↑(𝑁 + 2))) + 1))) |
88 | 87 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑧 = ((𝑛 · (2↑(𝑁 + 2))) + 1) ∧ 𝑦 = ((𝑚 · (2↑(𝑁 + 2))) + 1)) → ((𝑦 · 𝑧) = ((𝑘 · (2↑(𝑁 + 2))) + 1) ↔ (((𝑚 · (2↑(𝑁 + 2))) + 1) · ((𝑛 · (2↑(𝑁 + 2))) + 1)) = ((𝑘 · (2↑(𝑁 + 2))) + 1))) |
89 | 88 | rexbidv 3216 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑧 = ((𝑛 · (2↑(𝑁 + 2))) + 1) ∧ 𝑦 = ((𝑚 · (2↑(𝑁 + 2))) + 1)) → (∃𝑘 ∈ ℕ0
(𝑦 · 𝑧) = ((𝑘 · (2↑(𝑁 + 2))) + 1) ↔ ∃𝑘 ∈ ℕ0
(((𝑚 ·
(2↑(𝑁 + 2))) + 1)
· ((𝑛 ·
(2↑(𝑁 + 2))) + 1)) =
((𝑘 · (2↑(𝑁 + 2))) + 1))) |
90 | 85, 89 | syl5ibrcom 250 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ 𝑁 ∈
(ℤ≥‘2)) ∧ (𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
→ ((𝑧 = ((𝑛 · (2↑(𝑁 + 2))) + 1) ∧ 𝑦 = ((𝑚 · (2↑(𝑁 + 2))) + 1)) → ∃𝑘 ∈ ℕ0
(𝑦 · 𝑧) = ((𝑘 · (2↑(𝑁 + 2))) + 1))) |
91 | 90 | expd 419 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ 𝑁 ∈
(ℤ≥‘2)) ∧ (𝑚 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
→ (𝑧 = ((𝑛 · (2↑(𝑁 + 2))) + 1) → (𝑦 = ((𝑚 · (2↑(𝑁 + 2))) + 1) → ∃𝑘 ∈ ℕ0
(𝑦 · 𝑧) = ((𝑘 · (2↑(𝑁 + 2))) + 1)))) |
92 | 91 | anassrs 471 |
. . . . . . . . . . . . . 14
⊢
(((((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ 𝑁 ∈
(ℤ≥‘2)) ∧ 𝑚 ∈ ℕ0) ∧ 𝑛 ∈ ℕ0)
→ (𝑧 = ((𝑛 · (2↑(𝑁 + 2))) + 1) → (𝑦 = ((𝑚 · (2↑(𝑁 + 2))) + 1) → ∃𝑘 ∈ ℕ0
(𝑦 · 𝑧) = ((𝑘 · (2↑(𝑁 + 2))) + 1)))) |
93 | 92 | rexlimdva 3203 |
. . . . . . . . . . . . 13
⊢ ((((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ 𝑁 ∈
(ℤ≥‘2)) ∧ 𝑚 ∈ ℕ0) →
(∃𝑛 ∈
ℕ0 𝑧 =
((𝑛 · (2↑(𝑁 + 2))) + 1) → (𝑦 = ((𝑚 · (2↑(𝑁 + 2))) + 1) → ∃𝑘 ∈ ℕ0
(𝑦 · 𝑧) = ((𝑘 · (2↑(𝑁 + 2))) + 1)))) |
94 | 24, 93 | syl5bi 245 |
. . . . . . . . . . . 12
⊢ ((((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ 𝑁 ∈
(ℤ≥‘2)) ∧ 𝑚 ∈ ℕ0) →
(∃𝑘 ∈
ℕ0 𝑧 =
((𝑘 · (2↑(𝑁 + 2))) + 1) → (𝑦 = ((𝑚 · (2↑(𝑁 + 2))) + 1) → ∃𝑘 ∈ ℕ0
(𝑦 · 𝑧) = ((𝑘 · (2↑(𝑁 + 2))) + 1)))) |
95 | 94 | com23 86 |
. . . . . . . . . . 11
⊢ ((((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ 𝑁 ∈
(ℤ≥‘2)) ∧ 𝑚 ∈ ℕ0) → (𝑦 = ((𝑚 · (2↑(𝑁 + 2))) + 1) → (∃𝑘 ∈ ℕ0
𝑧 = ((𝑘 · (2↑(𝑁 + 2))) + 1) → ∃𝑘 ∈ ℕ0
(𝑦 · 𝑧) = ((𝑘 · (2↑(𝑁 + 2))) + 1)))) |
96 | 95 | rexlimdva 3203 |
. . . . . . . . . 10
⊢ (((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ 𝑁 ∈
(ℤ≥‘2)) → (∃𝑚 ∈ ℕ0 𝑦 = ((𝑚 · (2↑(𝑁 + 2))) + 1) → (∃𝑘 ∈ ℕ0
𝑧 = ((𝑘 · (2↑(𝑁 + 2))) + 1) → ∃𝑘 ∈ ℕ0
(𝑦 · 𝑧) = ((𝑘 · (2↑(𝑁 + 2))) + 1)))) |
97 | 20, 96 | syl5bi 245 |
. . . . . . . . 9
⊢ (((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ 𝑁 ∈
(ℤ≥‘2)) → (∃𝑘 ∈ ℕ0 𝑦 = ((𝑘 · (2↑(𝑁 + 2))) + 1) → (∃𝑘 ∈ ℕ0
𝑧 = ((𝑘 · (2↑(𝑁 + 2))) + 1) → ∃𝑘 ∈ ℕ0
(𝑦 · 𝑧) = ((𝑘 · (2↑(𝑁 + 2))) + 1)))) |
98 | 97 | impd 414 |
. . . . . . . 8
⊢ (((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ 𝑁 ∈
(ℤ≥‘2)) → ((∃𝑘 ∈ ℕ0 𝑦 = ((𝑘 · (2↑(𝑁 + 2))) + 1) ∧ ∃𝑘 ∈ ℕ0 𝑧 = ((𝑘 · (2↑(𝑁 + 2))) + 1)) → ∃𝑘 ∈ ℕ0
(𝑦 · 𝑧) = ((𝑘 · (2↑(𝑁 + 2))) + 1))) |
99 | 98 | adantr 484 |
. . . . . . 7
⊢ ((((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ 𝑁 ∈
(ℤ≥‘2)) ∧ (𝑦 ∥ (FermatNo‘𝑁) ∧ 𝑧 ∥ (FermatNo‘𝑁))) → ((∃𝑘 ∈ ℕ0 𝑦 = ((𝑘 · (2↑(𝑁 + 2))) + 1) ∧ ∃𝑘 ∈ ℕ0 𝑧 = ((𝑘 · (2↑(𝑁 + 2))) + 1)) → ∃𝑘 ∈ ℕ0
(𝑦 · 𝑧) = ((𝑘 · (2↑(𝑁 + 2))) + 1))) |
100 | 14, 16, 99 | syl2and 611 |
. . . . . 6
⊢ ((((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ 𝑁 ∈
(ℤ≥‘2)) ∧ (𝑦 ∥ (FermatNo‘𝑁) ∧ 𝑧 ∥ (FermatNo‘𝑁))) → ((((𝑁 ∈ (ℤ≥‘2)
∧ 𝑦 ∥
(FermatNo‘𝑁)) →
∃𝑘 ∈
ℕ0 𝑦 =
((𝑘 · (2↑(𝑁 + 2))) + 1)) ∧ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑧 ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ0 𝑧 = ((𝑘 · (2↑(𝑁 + 2))) + 1))) → ∃𝑘 ∈ ℕ0
(𝑦 · 𝑧) = ((𝑘 · (2↑(𝑁 + 2))) + 1))) |
101 | 100 | exp32 424 |
. . . . 5
⊢ (((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ 𝑁 ∈
(ℤ≥‘2)) → (𝑦 ∥ (FermatNo‘𝑁) → (𝑧 ∥ (FermatNo‘𝑁) → ((((𝑁 ∈ (ℤ≥‘2)
∧ 𝑦 ∥
(FermatNo‘𝑁)) →
∃𝑘 ∈
ℕ0 𝑦 =
((𝑘 · (2↑(𝑁 + 2))) + 1)) ∧ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑧 ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ0 𝑧 = ((𝑘 · (2↑(𝑁 + 2))) + 1))) → ∃𝑘 ∈ ℕ0
(𝑦 · 𝑧) = ((𝑘 · (2↑(𝑁 + 2))) + 1))))) |
102 | 12, 101 | syld 47 |
. . . 4
⊢ (((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ 𝑁 ∈
(ℤ≥‘2)) → ((𝑦 · 𝑧) ∥ (FermatNo‘𝑁) → (𝑧 ∥ (FermatNo‘𝑁) → ((((𝑁 ∈ (ℤ≥‘2)
∧ 𝑦 ∥
(FermatNo‘𝑁)) →
∃𝑘 ∈
ℕ0 𝑦 =
((𝑘 · (2↑(𝑁 + 2))) + 1)) ∧ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑧 ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ0 𝑧 = ((𝑘 · (2↑(𝑁 + 2))) + 1))) → ∃𝑘 ∈ ℕ0
(𝑦 · 𝑧) = ((𝑘 · (2↑(𝑁 + 2))) + 1))))) |
103 | 10, 102 | mpdd 43 |
. . 3
⊢ (((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ 𝑁 ∈
(ℤ≥‘2)) → ((𝑦 · 𝑧) ∥ (FermatNo‘𝑁) → ((((𝑁 ∈ (ℤ≥‘2)
∧ 𝑦 ∥
(FermatNo‘𝑁)) →
∃𝑘 ∈
ℕ0 𝑦 =
((𝑘 · (2↑(𝑁 + 2))) + 1)) ∧ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑧 ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ0 𝑧 = ((𝑘 · (2↑(𝑁 + 2))) + 1))) → ∃𝑘 ∈ ℕ0
(𝑦 · 𝑧) = ((𝑘 · (2↑(𝑁 + 2))) + 1)))) |
104 | 103 | expimpd 457 |
. 2
⊢ ((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
→ ((𝑁 ∈
(ℤ≥‘2) ∧ (𝑦 · 𝑧) ∥ (FermatNo‘𝑁)) → ((((𝑁 ∈ (ℤ≥‘2)
∧ 𝑦 ∥
(FermatNo‘𝑁)) →
∃𝑘 ∈
ℕ0 𝑦 =
((𝑘 · (2↑(𝑁 + 2))) + 1)) ∧ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑧 ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ0 𝑧 = ((𝑘 · (2↑(𝑁 + 2))) + 1))) → ∃𝑘 ∈ ℕ0
(𝑦 · 𝑧) = ((𝑘 · (2↑(𝑁 + 2))) + 1)))) |
105 | 104 | com23 86 |
1
⊢ ((𝑦 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
→ ((((𝑁 ∈
(ℤ≥‘2) ∧ 𝑦 ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ0 𝑦 = ((𝑘 · (2↑(𝑁 + 2))) + 1)) ∧ ((𝑁 ∈ (ℤ≥‘2)
∧ 𝑧 ∥
(FermatNo‘𝑁)) →
∃𝑘 ∈
ℕ0 𝑧 =
((𝑘 · (2↑(𝑁 + 2))) + 1))) → ((𝑁 ∈
(ℤ≥‘2) ∧ (𝑦 · 𝑧) ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ0 (𝑦 · 𝑧) = ((𝑘 · (2↑(𝑁 + 2))) + 1)))) |