| Step | Hyp | Ref
| Expression |
| 1 | | 2nn 12339 |
. . . 4
⊢ 2 ∈
ℕ |
| 2 | | fpprel 47715 |
. . . 4
⊢ (2 ∈
ℕ → (𝑋 ∈ (
FPPr ‘2) ↔ (𝑋
∈ (ℤ≥‘4) ∧ 𝑋 ∉ ℙ ∧ ((2↑(𝑋 − 1)) mod 𝑋) = 1))) |
| 3 | 1, 2 | ax-mp 5 |
. . 3
⊢ (𝑋 ∈ ( FPPr ‘2) ↔
(𝑋 ∈
(ℤ≥‘4) ∧ 𝑋 ∉ ℙ ∧ ((2↑(𝑋 − 1)) mod 𝑋) = 1)) |
| 4 | | eluz4nn 12928 |
. . . . . . 7
⊢ (𝑋 ∈
(ℤ≥‘4) → 𝑋 ∈ ℕ) |
| 5 | 4 | adantr 480 |
. . . . . 6
⊢ ((𝑋 ∈
(ℤ≥‘4) ∧ ((2↑(𝑋 − 1)) mod 𝑋) = 1) → 𝑋 ∈ ℕ) |
| 6 | | eluzelz 12888 |
. . . . . . . . 9
⊢ (𝑋 ∈
(ℤ≥‘4) → 𝑋 ∈ ℤ) |
| 7 | | zeo2ALTV 47658 |
. . . . . . . . 9
⊢ (𝑋 ∈ ℤ → (𝑋 ∈ Even ↔ ¬ 𝑋 ∈ Odd )) |
| 8 | 6, 7 | syl 17 |
. . . . . . . 8
⊢ (𝑋 ∈
(ℤ≥‘4) → (𝑋 ∈ Even ↔ ¬ 𝑋 ∈ Odd )) |
| 9 | 8 | adantr 480 |
. . . . . . 7
⊢ ((𝑋 ∈
(ℤ≥‘4) ∧ ((2↑(𝑋 − 1)) mod 𝑋) = 1) → (𝑋 ∈ Even ↔ ¬ 𝑋 ∈ Odd )) |
| 10 | 9 | biimprd 248 |
. . . . . 6
⊢ ((𝑋 ∈
(ℤ≥‘4) ∧ ((2↑(𝑋 − 1)) mod 𝑋) = 1) → (¬ 𝑋 ∈ Odd → 𝑋 ∈ Even )) |
| 11 | | nnennexALTV 47688 |
. . . . . 6
⊢ ((𝑋 ∈ ℕ ∧ 𝑋 ∈ Even ) →
∃𝑦 ∈ ℕ
𝑋 = (2 · 𝑦)) |
| 12 | 5, 10, 11 | syl6an 684 |
. . . . 5
⊢ ((𝑋 ∈
(ℤ≥‘4) ∧ ((2↑(𝑋 − 1)) mod 𝑋) = 1) → (¬ 𝑋 ∈ Odd → ∃𝑦 ∈ ℕ 𝑋 = (2 · 𝑦))) |
| 13 | | oveq1 7438 |
. . . . . . . . . . . . . 14
⊢ (𝑋 = (2 · 𝑦) → (𝑋 − 1) = ((2 · 𝑦) − 1)) |
| 14 | 13 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ (𝑋 = (2 · 𝑦) → (2↑(𝑋 − 1)) = (2↑((2
· 𝑦) −
1))) |
| 15 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑋 = (2 · 𝑦) → 𝑋 = (2 · 𝑦)) |
| 16 | 14, 15 | oveq12d 7449 |
. . . . . . . . . . . 12
⊢ (𝑋 = (2 · 𝑦) → ((2↑(𝑋 − 1)) mod 𝑋) = ((2↑((2 · 𝑦) − 1)) mod (2 ·
𝑦))) |
| 17 | 16 | eqeq1d 2739 |
. . . . . . . . . . 11
⊢ (𝑋 = (2 · 𝑦) → (((2↑(𝑋 − 1)) mod 𝑋) = 1 ↔ ((2↑((2
· 𝑦) − 1)) mod
(2 · 𝑦)) =
1)) |
| 18 | 17 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝑋 ∈
(ℤ≥‘4) ∧ 𝑦 ∈ ℕ) ∧ 𝑋 = (2 · 𝑦)) → (((2↑(𝑋 − 1)) mod 𝑋) = 1 ↔ ((2↑((2 · 𝑦) − 1)) mod (2 ·
𝑦)) = 1)) |
| 19 | | 2z 12649 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℤ |
| 20 | 1 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℕ → 2 ∈
ℕ) |
| 21 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℕ) |
| 22 | 20, 21 | nnmulcld 12319 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℕ → (2
· 𝑦) ∈
ℕ) |
| 23 | | nnm1nn0 12567 |
. . . . . . . . . . . . . . . 16
⊢ ((2
· 𝑦) ∈ ℕ
→ ((2 · 𝑦)
− 1) ∈ ℕ0) |
| 24 | 22, 23 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℕ → ((2
· 𝑦) − 1)
∈ ℕ0) |
| 25 | | zexpcl 14117 |
. . . . . . . . . . . . . . 15
⊢ ((2
∈ ℤ ∧ ((2 · 𝑦) − 1) ∈ ℕ0)
→ (2↑((2 · 𝑦) − 1)) ∈
ℤ) |
| 26 | 19, 24, 25 | sylancr 587 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ →
(2↑((2 · 𝑦)
− 1)) ∈ ℤ) |
| 27 | 22 | nnrpd 13075 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ → (2
· 𝑦) ∈
ℝ+) |
| 28 | | modmuladdim 13955 |
. . . . . . . . . . . . . 14
⊢
(((2↑((2 · 𝑦) − 1)) ∈ ℤ ∧ (2
· 𝑦) ∈
ℝ+) → (((2↑((2 · 𝑦) − 1)) mod (2 · 𝑦)) = 1 → ∃𝑚 ∈ ℤ (2↑((2
· 𝑦) − 1)) =
((𝑚 · (2 ·
𝑦)) + 1))) |
| 29 | 26, 27, 28 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ →
(((2↑((2 · 𝑦)
− 1)) mod (2 · 𝑦)) = 1 → ∃𝑚 ∈ ℤ (2↑((2 · 𝑦) − 1)) = ((𝑚 · (2 · 𝑦)) + 1))) |
| 30 | 24 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ) → ((2
· 𝑦) − 1)
∈ ℕ0) |
| 31 | 19, 30, 25 | sylancr 587 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ) →
(2↑((2 · 𝑦)
− 1)) ∈ ℤ) |
| 32 | 31 | zcnd 12723 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ) →
(2↑((2 · 𝑦)
− 1)) ∈ ℂ) |
| 33 | | zcn 12618 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 ∈ ℤ → 𝑚 ∈
ℂ) |
| 34 | 33 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ) → 𝑚 ∈
ℂ) |
| 35 | | 2cnd 12344 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ) → 2 ∈
ℂ) |
| 36 | | nncn 12274 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℂ) |
| 37 | 36 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ) → 𝑦 ∈
ℂ) |
| 38 | 35, 37 | mulcld 11281 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ) → (2
· 𝑦) ∈
ℂ) |
| 39 | 34, 38 | mulcld 11281 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ) → (𝑚 · (2 · 𝑦)) ∈
ℂ) |
| 40 | | 1cnd 11256 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ) → 1 ∈
ℂ) |
| 41 | | subadd 11511 |
. . . . . . . . . . . . . . . . 17
⊢
(((2↑((2 · 𝑦) − 1)) ∈ ℂ ∧ (𝑚 · (2 · 𝑦)) ∈ ℂ ∧ 1 ∈
ℂ) → (((2↑((2 · 𝑦) − 1)) − (𝑚 · (2 · 𝑦))) = 1 ↔ ((𝑚 · (2 · 𝑦)) + 1) = (2↑((2 · 𝑦) − 1)))) |
| 42 | | eqcom 2744 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑚 · (2 · 𝑦)) + 1) = (2↑((2 ·
𝑦) − 1)) ↔
(2↑((2 · 𝑦)
− 1)) = ((𝑚 ·
(2 · 𝑦)) +
1)) |
| 43 | 41, 42 | bitrdi 287 |
. . . . . . . . . . . . . . . 16
⊢
(((2↑((2 · 𝑦) − 1)) ∈ ℂ ∧ (𝑚 · (2 · 𝑦)) ∈ ℂ ∧ 1 ∈
ℂ) → (((2↑((2 · 𝑦) − 1)) − (𝑚 · (2 · 𝑦))) = 1 ↔ (2↑((2 · 𝑦) − 1)) = ((𝑚 · (2 · 𝑦)) + 1))) |
| 44 | 32, 39, 40, 43 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ) →
(((2↑((2 · 𝑦)
− 1)) − (𝑚
· (2 · 𝑦))) =
1 ↔ (2↑((2 · 𝑦) − 1)) = ((𝑚 · (2 · 𝑦)) + 1))) |
| 45 | | 2cnd 12344 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 ∈ ℕ → 2 ∈
ℂ) |
| 46 | 45, 36 | mulcld 11281 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 ∈ ℕ → (2
· 𝑦) ∈
ℂ) |
| 47 | | 1cnd 11256 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 ∈ ℕ → 1 ∈
ℂ) |
| 48 | 46, 47 | subcld 11620 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ ℕ → ((2
· 𝑦) − 1)
∈ ℂ) |
| 49 | 48 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ) → ((2
· 𝑦) − 1)
∈ ℂ) |
| 50 | | npcan1 11688 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((2
· 𝑦) − 1)
∈ ℂ → ((((2 · 𝑦) − 1) − 1) + 1) = ((2 ·
𝑦) −
1)) |
| 51 | 49, 50 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ) → ((((2
· 𝑦) − 1)
− 1) + 1) = ((2 · 𝑦) − 1)) |
| 52 | 51 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ) → ((2
· 𝑦) − 1) =
((((2 · 𝑦) −
1) − 1) + 1)) |
| 53 | 52 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ) →
(2↑((2 · 𝑦)
− 1)) = (2↑((((2 · 𝑦) − 1) − 1) +
1))) |
| 54 | | 2t1e2 12429 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (2
· 1) = 2 |
| 55 | 54 | eqcomi 2746 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 2 = (2
· 1) |
| 56 | 55 | oveq2i 7442 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((2
· 𝑦) − 2) =
((2 · 𝑦) − (2
· 1)) |
| 57 | | sub1m1 12518 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((2
· 𝑦) ∈ ℂ
→ (((2 · 𝑦)
− 1) − 1) = ((2 · 𝑦) − 2)) |
| 58 | 38, 57 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ) → (((2
· 𝑦) − 1)
− 1) = ((2 · 𝑦) − 2)) |
| 59 | 35, 37, 40 | subdid 11719 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ) → (2
· (𝑦 − 1)) =
((2 · 𝑦) − (2
· 1))) |
| 60 | 56, 58, 59 | 3eqtr4a 2803 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ) → (((2
· 𝑦) − 1)
− 1) = (2 · (𝑦
− 1))) |
| 61 | | 2nn0 12543 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 2 ∈
ℕ0 |
| 62 | 61 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ) → 2 ∈
ℕ0) |
| 63 | | nnm1nn0 12567 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 ∈ ℕ → (𝑦 − 1) ∈
ℕ0) |
| 64 | 63 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ) → (𝑦 − 1) ∈
ℕ0) |
| 65 | 62, 64 | nn0mulcld 12592 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ) → (2
· (𝑦 − 1))
∈ ℕ0) |
| 66 | 60, 65 | eqeltrd 2841 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ) → (((2
· 𝑦) − 1)
− 1) ∈ ℕ0) |
| 67 | 35, 66 | expp1d 14187 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ) →
(2↑((((2 · 𝑦)
− 1) − 1) + 1)) = ((2↑(((2 · 𝑦) − 1) − 1)) ·
2)) |
| 68 | 35, 66 | expcld 14186 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ) →
(2↑(((2 · 𝑦)
− 1) − 1)) ∈ ℂ) |
| 69 | 68, 35 | mulcomd 11282 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ) →
((2↑(((2 · 𝑦)
− 1) − 1)) · 2) = (2 · (2↑(((2 · 𝑦) − 1) −
1)))) |
| 70 | 67, 69 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ) →
(2↑((((2 · 𝑦)
− 1) − 1) + 1)) = (2 · (2↑(((2 · 𝑦) − 1) −
1)))) |
| 71 | 53, 70 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ) →
(2↑((2 · 𝑦)
− 1)) = (2 · (2↑(((2 · 𝑦) − 1) − 1)))) |
| 72 | 34, 35, 37 | mul12d 11470 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ) → (𝑚 · (2 · 𝑦)) = (2 · (𝑚 · 𝑦))) |
| 73 | 71, 72 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ) →
((2↑((2 · 𝑦)
− 1)) − (𝑚
· (2 · 𝑦))) =
((2 · (2↑(((2 · 𝑦) − 1) − 1))) − (2 ·
(𝑚 · 𝑦)))) |
| 74 | 34, 37 | mulcld 11281 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ) → (𝑚 · 𝑦) ∈ ℂ) |
| 75 | 35, 68, 74 | subdid 11719 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ) → (2
· ((2↑(((2 · 𝑦) − 1) − 1)) − (𝑚 · 𝑦))) = ((2 · (2↑(((2 ·
𝑦) − 1) − 1)))
− (2 · (𝑚
· 𝑦)))) |
| 76 | 75 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ) → ((2
· (2↑(((2 · 𝑦) − 1) − 1))) − (2 ·
(𝑚 · 𝑦))) = (2 · ((2↑(((2
· 𝑦) − 1)
− 1)) − (𝑚
· 𝑦)))) |
| 77 | 73, 76 | eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ) →
((2↑((2 · 𝑦)
− 1)) − (𝑚
· (2 · 𝑦))) =
(2 · ((2↑(((2 · 𝑦) − 1) − 1)) − (𝑚 · 𝑦)))) |
| 78 | 77 | eqeq1d 2739 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ) →
(((2↑((2 · 𝑦)
− 1)) − (𝑚
· (2 · 𝑦))) =
1 ↔ (2 · ((2↑(((2 · 𝑦) − 1) − 1)) − (𝑚 · 𝑦))) = 1)) |
| 79 | | zexpcl 14117 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((2
∈ ℤ ∧ (((2 · 𝑦) − 1) − 1) ∈
ℕ0) → (2↑(((2 · 𝑦) − 1) − 1)) ∈
ℤ) |
| 80 | 19, 66, 79 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ) →
(2↑(((2 · 𝑦)
− 1) − 1)) ∈ ℤ) |
| 81 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ) → 𝑚 ∈
ℤ) |
| 82 | | nnz 12634 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℤ) |
| 83 | 82 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ) → 𝑦 ∈
ℤ) |
| 84 | 81, 83 | zmulcld 12728 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ) → (𝑚 · 𝑦) ∈ ℤ) |
| 85 | 80, 84 | zsubcld 12727 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ) →
((2↑(((2 · 𝑦)
− 1) − 1)) − (𝑚 · 𝑦)) ∈ ℤ) |
| 86 | | m2even 47641 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((2↑(((2 · 𝑦) − 1) − 1)) − (𝑚 · 𝑦)) ∈ ℤ → (2 ·
((2↑(((2 · 𝑦)
− 1) − 1)) − (𝑚 · 𝑦))) ∈ Even ) |
| 87 | 85, 86 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ) → (2
· ((2↑(((2 · 𝑦) − 1) − 1)) − (𝑚 · 𝑦))) ∈ Even ) |
| 88 | | 1oddALTV 47677 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
Odd |
| 89 | | zneoALTV 47656 |
. . . . . . . . . . . . . . . . . 18
⊢ (((2
· ((2↑(((2 · 𝑦) − 1) − 1)) − (𝑚 · 𝑦))) ∈ Even ∧ 1 ∈ Odd ) →
(2 · ((2↑(((2 · 𝑦) − 1) − 1)) − (𝑚 · 𝑦))) ≠ 1) |
| 90 | 87, 88, 89 | sylancl 586 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ) → (2
· ((2↑(((2 · 𝑦) − 1) − 1)) − (𝑚 · 𝑦))) ≠ 1) |
| 91 | | eqneqall 2951 |
. . . . . . . . . . . . . . . . 17
⊢ ((2
· ((2↑(((2 · 𝑦) − 1) − 1)) − (𝑚 · 𝑦))) = 1 → ((2 · ((2↑(((2
· 𝑦) − 1)
− 1)) − (𝑚
· 𝑦))) ≠ 1 →
𝑋 ∈ Odd
)) |
| 92 | 90, 91 | syl5com 31 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ) → ((2
· ((2↑(((2 · 𝑦) − 1) − 1)) − (𝑚 · 𝑦))) = 1 → 𝑋 ∈ Odd )) |
| 93 | 78, 92 | sylbid 240 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ) →
(((2↑((2 · 𝑦)
− 1)) − (𝑚
· (2 · 𝑦))) =
1 → 𝑋 ∈ Odd
)) |
| 94 | 44, 93 | sylbird 260 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℕ ∧ 𝑚 ∈ ℤ) →
((2↑((2 · 𝑦)
− 1)) = ((𝑚 ·
(2 · 𝑦)) + 1) →
𝑋 ∈ Odd
)) |
| 95 | 94 | rexlimdva 3155 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ →
(∃𝑚 ∈ ℤ
(2↑((2 · 𝑦)
− 1)) = ((𝑚 ·
(2 · 𝑦)) + 1) →
𝑋 ∈ Odd
)) |
| 96 | 29, 95 | syld 47 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ →
(((2↑((2 · 𝑦)
− 1)) mod (2 · 𝑦)) = 1 → 𝑋 ∈ Odd )) |
| 97 | 96 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈
(ℤ≥‘4) ∧ 𝑦 ∈ ℕ) → (((2↑((2
· 𝑦) − 1)) mod
(2 · 𝑦)) = 1 →
𝑋 ∈ Odd
)) |
| 98 | 97 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑋 ∈
(ℤ≥‘4) ∧ 𝑦 ∈ ℕ) ∧ 𝑋 = (2 · 𝑦)) → (((2↑((2 · 𝑦) − 1)) mod (2 ·
𝑦)) = 1 → 𝑋 ∈ Odd )) |
| 99 | 18, 98 | sylbid 240 |
. . . . . . . . 9
⊢ (((𝑋 ∈
(ℤ≥‘4) ∧ 𝑦 ∈ ℕ) ∧ 𝑋 = (2 · 𝑦)) → (((2↑(𝑋 − 1)) mod 𝑋) = 1 → 𝑋 ∈ Odd )) |
| 100 | 99 | ex 412 |
. . . . . . . 8
⊢ ((𝑋 ∈
(ℤ≥‘4) ∧ 𝑦 ∈ ℕ) → (𝑋 = (2 · 𝑦) → (((2↑(𝑋 − 1)) mod 𝑋) = 1 → 𝑋 ∈ Odd ))) |
| 101 | 100 | rexlimdva 3155 |
. . . . . . 7
⊢ (𝑋 ∈
(ℤ≥‘4) → (∃𝑦 ∈ ℕ 𝑋 = (2 · 𝑦) → (((2↑(𝑋 − 1)) mod 𝑋) = 1 → 𝑋 ∈ Odd ))) |
| 102 | 101 | com23 86 |
. . . . . 6
⊢ (𝑋 ∈
(ℤ≥‘4) → (((2↑(𝑋 − 1)) mod 𝑋) = 1 → (∃𝑦 ∈ ℕ 𝑋 = (2 · 𝑦) → 𝑋 ∈ Odd ))) |
| 103 | 102 | imp 406 |
. . . . 5
⊢ ((𝑋 ∈
(ℤ≥‘4) ∧ ((2↑(𝑋 − 1)) mod 𝑋) = 1) → (∃𝑦 ∈ ℕ 𝑋 = (2 · 𝑦) → 𝑋 ∈ Odd )) |
| 104 | 12, 103 | syld 47 |
. . . 4
⊢ ((𝑋 ∈
(ℤ≥‘4) ∧ ((2↑(𝑋 − 1)) mod 𝑋) = 1) → (¬ 𝑋 ∈ Odd → 𝑋 ∈ Odd )) |
| 105 | 104 | 3adant2 1132 |
. . 3
⊢ ((𝑋 ∈
(ℤ≥‘4) ∧ 𝑋 ∉ ℙ ∧ ((2↑(𝑋 − 1)) mod 𝑋) = 1) → (¬ 𝑋 ∈ Odd → 𝑋 ∈ Odd )) |
| 106 | 3, 105 | sylbi 217 |
. 2
⊢ (𝑋 ∈ ( FPPr ‘2) →
(¬ 𝑋 ∈ Odd →
𝑋 ∈ Odd
)) |
| 107 | 106 | pm2.18d 127 |
1
⊢ (𝑋 ∈ ( FPPr ‘2) →
𝑋 ∈ Odd
) |