Step | Hyp | Ref
| Expression |
1 | | perfectlem.2 |
. . . 4
⊢ (𝜑 → 𝐵 ∈ ℕ) |
2 | | 1red 10055 |
. . . . 5
⊢ (𝜑 → 1 ∈
ℝ) |
3 | | perfectlem.1 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℕ) |
4 | | perfectlem.3 |
. . . . . . . 8
⊢ (𝜑 → ¬ 2 ∥ 𝐵) |
5 | | perfectlem.4 |
. . . . . . . 8
⊢ (𝜑 → (1 σ ((2↑𝐴) · 𝐵)) = (2 · ((2↑𝐴) · 𝐵))) |
6 | 3, 1, 4, 5 | perfectlem1 24954 |
. . . . . . 7
⊢ (𝜑 → ((2↑(𝐴 + 1)) ∈ ℕ ∧
((2↑(𝐴 + 1)) −
1) ∈ ℕ ∧ (𝐵
/ ((2↑(𝐴 + 1)) −
1)) ∈ ℕ)) |
7 | 6 | simp3d 1075 |
. . . . . 6
⊢ (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈
ℕ) |
8 | 7 | nnred 11035 |
. . . . 5
⊢ (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈
ℝ) |
9 | 1 | nnred 11035 |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ ℝ) |
10 | 7 | nnge1d 11063 |
. . . . 5
⊢ (𝜑 → 1 ≤ (𝐵 / ((2↑(𝐴 + 1)) − 1))) |
11 | | 2cn 11091 |
. . . . . . . . . . 11
⊢ 2 ∈
ℂ |
12 | | exp1 12866 |
. . . . . . . . . . 11
⊢ (2 ∈
ℂ → (2↑1) = 2) |
13 | 11, 12 | ax-mp 5 |
. . . . . . . . . 10
⊢
(2↑1) = 2 |
14 | | df-2 11079 |
. . . . . . . . . 10
⊢ 2 = (1 +
1) |
15 | 13, 14 | eqtri 2644 |
. . . . . . . . 9
⊢
(2↑1) = (1 + 1) |
16 | | 2re 11090 |
. . . . . . . . . . 11
⊢ 2 ∈
ℝ |
17 | 16 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 2 ∈
ℝ) |
18 | | 1zzd 11408 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℤ) |
19 | 3 | peano2nnd 11037 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 + 1) ∈ ℕ) |
20 | 19 | nnzd 11481 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 + 1) ∈ ℤ) |
21 | | 1lt2 11194 |
. . . . . . . . . . 11
⊢ 1 <
2 |
22 | 21 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 1 < 2) |
23 | | 1re 10039 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℝ |
24 | 3 | nnrpd 11870 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈
ℝ+) |
25 | | ltaddrp 11867 |
. . . . . . . . . . . 12
⊢ ((1
∈ ℝ ∧ 𝐴
∈ ℝ+) → 1 < (1 + 𝐴)) |
26 | 23, 24, 25 | sylancr 695 |
. . . . . . . . . . 11
⊢ (𝜑 → 1 < (1 + 𝐴)) |
27 | | ax-1cn 9994 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℂ |
28 | 3 | nncnd 11036 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ ℂ) |
29 | | addcom 10222 |
. . . . . . . . . . . 12
⊢ ((1
∈ ℂ ∧ 𝐴
∈ ℂ) → (1 + 𝐴) = (𝐴 + 1)) |
30 | 27, 28, 29 | sylancr 695 |
. . . . . . . . . . 11
⊢ (𝜑 → (1 + 𝐴) = (𝐴 + 1)) |
31 | 26, 30 | breqtrd 4679 |
. . . . . . . . . 10
⊢ (𝜑 → 1 < (𝐴 + 1)) |
32 | | ltexp2a 12912 |
. . . . . . . . . 10
⊢ (((2
∈ ℝ ∧ 1 ∈ ℤ ∧ (𝐴 + 1) ∈ ℤ) ∧ (1 < 2 ∧
1 < (𝐴 + 1))) →
(2↑1) < (2↑(𝐴
+ 1))) |
33 | 17, 18, 20, 22, 31, 32 | syl32anc 1334 |
. . . . . . . . 9
⊢ (𝜑 → (2↑1) <
(2↑(𝐴 +
1))) |
34 | 15, 33 | syl5eqbrr 4689 |
. . . . . . . 8
⊢ (𝜑 → (1 + 1) <
(2↑(𝐴 +
1))) |
35 | 6 | simp1d 1073 |
. . . . . . . . . 10
⊢ (𝜑 → (2↑(𝐴 + 1)) ∈ ℕ) |
36 | 35 | nnred 11035 |
. . . . . . . . 9
⊢ (𝜑 → (2↑(𝐴 + 1)) ∈ ℝ) |
37 | 2, 2, 36 | ltaddsubd 10627 |
. . . . . . . 8
⊢ (𝜑 → ((1 + 1) <
(2↑(𝐴 + 1)) ↔ 1
< ((2↑(𝐴 + 1))
− 1))) |
38 | 34, 37 | mpbid 222 |
. . . . . . 7
⊢ (𝜑 → 1 < ((2↑(𝐴 + 1)) −
1)) |
39 | | 0lt1 10550 |
. . . . . . . . 9
⊢ 0 <
1 |
40 | 39 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 0 < 1) |
41 | | peano2rem 10348 |
. . . . . . . . 9
⊢
((2↑(𝐴 + 1))
∈ ℝ → ((2↑(𝐴 + 1)) − 1) ∈
ℝ) |
42 | 36, 41 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ((2↑(𝐴 + 1)) − 1) ∈
ℝ) |
43 | | expgt1 12898 |
. . . . . . . . . 10
⊢ ((2
∈ ℝ ∧ (𝐴 +
1) ∈ ℕ ∧ 1 < 2) → 1 < (2↑(𝐴 + 1))) |
44 | 17, 19, 22, 43 | syl3anc 1326 |
. . . . . . . . 9
⊢ (𝜑 → 1 < (2↑(𝐴 + 1))) |
45 | | posdif 10521 |
. . . . . . . . . 10
⊢ ((1
∈ ℝ ∧ (2↑(𝐴 + 1)) ∈ ℝ) → (1 <
(2↑(𝐴 + 1)) ↔ 0
< ((2↑(𝐴 + 1))
− 1))) |
46 | 23, 36, 45 | sylancr 695 |
. . . . . . . . 9
⊢ (𝜑 → (1 < (2↑(𝐴 + 1)) ↔ 0 <
((2↑(𝐴 + 1)) −
1))) |
47 | 44, 46 | mpbid 222 |
. . . . . . . 8
⊢ (𝜑 → 0 < ((2↑(𝐴 + 1)) −
1)) |
48 | 1 | nngt0d 11064 |
. . . . . . . 8
⊢ (𝜑 → 0 < 𝐵) |
49 | | ltdiv2 10909 |
. . . . . . . 8
⊢ (((1
∈ ℝ ∧ 0 < 1) ∧ (((2↑(𝐴 + 1)) − 1) ∈ ℝ ∧ 0
< ((2↑(𝐴 + 1))
− 1)) ∧ (𝐵 ∈
ℝ ∧ 0 < 𝐵))
→ (1 < ((2↑(𝐴
+ 1)) − 1) ↔ (𝐵
/ ((2↑(𝐴 + 1)) −
1)) < (𝐵 /
1))) |
50 | 2, 40, 42, 47, 9, 48, 49 | syl222anc 1342 |
. . . . . . 7
⊢ (𝜑 → (1 < ((2↑(𝐴 + 1)) − 1) ↔ (𝐵 / ((2↑(𝐴 + 1)) − 1)) < (𝐵 / 1))) |
51 | 38, 50 | mpbid 222 |
. . . . . 6
⊢ (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) < (𝐵 / 1)) |
52 | 1 | nncnd 11036 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ ℂ) |
53 | 52 | div1d 10793 |
. . . . . 6
⊢ (𝜑 → (𝐵 / 1) = 𝐵) |
54 | 51, 53 | breqtrd 4679 |
. . . . 5
⊢ (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) < 𝐵) |
55 | 2, 8, 9, 10, 54 | lelttrd 10195 |
. . . 4
⊢ (𝜑 → 1 < 𝐵) |
56 | | eluz2b2 11761 |
. . . 4
⊢ (𝐵 ∈
(ℤ≥‘2) ↔ (𝐵 ∈ ℕ ∧ 1 < 𝐵)) |
57 | 1, 55, 56 | sylanbrc 698 |
. . 3
⊢ (𝜑 → 𝐵 ∈
(ℤ≥‘2)) |
58 | | fzfid 12772 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1...𝐵) ∈ Fin) |
59 | | dvdsssfz1 15040 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ ℕ → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵} ⊆ (1...𝐵)) |
60 | 1, 59 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵} ⊆ (1...𝐵)) |
61 | | ssfi 8180 |
. . . . . . . . . . . 12
⊢
(((1...𝐵) ∈ Fin
∧ {𝑥 ∈ ℕ
∣ 𝑥 ∥ 𝐵} ⊆ (1...𝐵)) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵} ∈ Fin) |
62 | 58, 60, 61 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (𝜑 → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵} ∈ Fin) |
63 | 62 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵} ∈ Fin) |
64 | | ssrab2 3687 |
. . . . . . . . . . . . 13
⊢ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵} ⊆ ℕ |
65 | 64 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵} ⊆ ℕ) |
66 | 65 | sselda 3603 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) → 𝑘 ∈ ℕ) |
67 | 66 | nnred 11035 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) → 𝑘 ∈ ℝ) |
68 | 66 | nnnn0d 11351 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) → 𝑘 ∈ ℕ0) |
69 | 68 | nn0ge0d 11354 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) → 0 ≤ 𝑘) |
70 | | df-tp 4182 |
. . . . . . . . . . . 12
⊢ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} = ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∪ {𝑛}) |
71 | | prssi 4353 |
. . . . . . . . . . . . . . 15
⊢ (((𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℕ ∧
𝐵 ∈ ℕ) →
{(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ⊆
ℕ) |
72 | 7, 1, 71 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ⊆ ℕ) |
73 | 72 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ⊆ ℕ) |
74 | | simplrl 800 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → 𝑛 ∈ ℕ) |
75 | 74 | snssd 4340 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {𝑛} ⊆ ℕ) |
76 | 73, 75 | unssd 3789 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∪ {𝑛}) ⊆ ℕ) |
77 | 70, 76 | syl5eqss 3649 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} ⊆ ℕ) |
78 | | eltpi 4229 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} → (𝑥 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝑛)) |
79 | 6 | simp2d 1074 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((2↑(𝐴 + 1)) − 1) ∈
ℕ) |
80 | 79 | nnzd 11481 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((2↑(𝐴 + 1)) − 1) ∈
ℤ) |
81 | 7 | nnzd 11481 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈
ℤ) |
82 | | dvdsmul2 15004 |
. . . . . . . . . . . . . . . . . 18
⊢
((((2↑(𝐴 + 1))
− 1) ∈ ℤ ∧ (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℤ) →
(𝐵 / ((2↑(𝐴 + 1)) − 1)) ∥
(((2↑(𝐴 + 1)) −
1) · (𝐵 /
((2↑(𝐴 + 1)) −
1)))) |
83 | 80, 81, 82 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∥ (((2↑(𝐴 + 1)) − 1) ·
(𝐵 / ((2↑(𝐴 + 1)) −
1)))) |
84 | 79 | nncnd 11036 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((2↑(𝐴 + 1)) − 1) ∈
ℂ) |
85 | 79 | nnne0d 11065 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((2↑(𝐴 + 1)) − 1) ≠
0) |
86 | 52, 84, 85 | divcan2d 10803 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (((2↑(𝐴 + 1)) − 1) ·
(𝐵 / ((2↑(𝐴 + 1)) − 1))) = 𝐵) |
87 | 83, 86 | breqtrd 4679 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∥ 𝐵) |
88 | | breq1 4656 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) → (𝑥 ∥ 𝐵 ↔ (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∥ 𝐵)) |
89 | 87, 88 | syl5ibrcom 237 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑥 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) → 𝑥 ∥ 𝐵)) |
90 | 89 | ad2antrr 762 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (𝑥 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) → 𝑥 ∥ 𝐵)) |
91 | 1 | nnzd 11481 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐵 ∈ ℤ) |
92 | | iddvds 14995 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐵 ∈ ℤ → 𝐵 ∥ 𝐵) |
93 | 91, 92 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐵 ∥ 𝐵) |
94 | | breq1 4656 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝐵 → (𝑥 ∥ 𝐵 ↔ 𝐵 ∥ 𝐵)) |
95 | 93, 94 | syl5ibrcom 237 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑥 = 𝐵 → 𝑥 ∥ 𝐵)) |
96 | 95 | ad2antrr 762 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (𝑥 = 𝐵 → 𝑥 ∥ 𝐵)) |
97 | | simplrr 801 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → 𝑛 ∥ 𝐵) |
98 | | breq1 4656 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑛 → (𝑥 ∥ 𝐵 ↔ 𝑛 ∥ 𝐵)) |
99 | 97, 98 | syl5ibrcom 237 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (𝑥 = 𝑛 → 𝑥 ∥ 𝐵)) |
100 | 90, 96, 99 | 3jaod 1392 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ((𝑥 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝑛) → 𝑥 ∥ 𝐵)) |
101 | 78, 100 | syl5 34 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (𝑥 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} → 𝑥 ∥ 𝐵)) |
102 | 101 | imp 445 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) ∧ 𝑥 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛}) → 𝑥 ∥ 𝐵) |
103 | 77, 102 | ssrabdv 3681 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} ⊆ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) |
104 | 63, 67, 69, 103 | fsumless 14528 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛}𝑘 ≤ Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}𝑘) |
105 | | simpr 477 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) |
106 | | disjsn 4246 |
. . . . . . . . . . . 12
⊢ (({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∩ {𝑛}) = ∅ ↔ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) |
107 | 105, 106 | sylibr 224 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∩ {𝑛}) = ∅) |
108 | 70 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} = ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∪ {𝑛})) |
109 | | tpfi 8236 |
. . . . . . . . . . . 12
⊢ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} ∈ Fin |
110 | 109 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} ∈ Fin) |
111 | 77 | sselda 3603 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) ∧ 𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛}) → 𝑘 ∈ ℕ) |
112 | 111 | nncnd 11036 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) ∧ 𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛}) → 𝑘 ∈ ℂ) |
113 | 107, 108,
110, 112 | fsumsplit 14471 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛}𝑘 = (Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 + Σ𝑘 ∈ {𝑛}𝑘)) |
114 | 7 | nncnd 11036 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈
ℂ) |
115 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) → 𝑘 = (𝐵 / ((2↑(𝐴 + 1)) − 1))) |
116 | 115 | sumsn 14475 |
. . . . . . . . . . . . . . 15
⊢ (((𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℕ ∧
(𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈
ℂ) → Σ𝑘
∈ {(𝐵 /
((2↑(𝐴 + 1)) −
1))}𝑘 = (𝐵 / ((2↑(𝐴 + 1)) − 1))) |
117 | 7, 114, 116 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1))}𝑘 = (𝐵 / ((2↑(𝐴 + 1)) − 1))) |
118 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝐵 → 𝑘 = 𝐵) |
119 | 118 | sumsn 14475 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 ∈ ℕ ∧ 𝐵 ∈ ℂ) →
Σ𝑘 ∈ {𝐵}𝑘 = 𝐵) |
120 | 1, 52, 119 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → Σ𝑘 ∈ {𝐵}𝑘 = 𝐵) |
121 | 117, 120 | oveq12d 6668 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1))}𝑘 + Σ𝑘 ∈ {𝐵}𝑘) = ((𝐵 / ((2↑(𝐴 + 1)) − 1)) + 𝐵)) |
122 | | incom 3805 |
. . . . . . . . . . . . . . 15
⊢ ({𝐵} ∩ {(𝐵 / ((2↑(𝐴 + 1)) − 1))}) = ({(𝐵 / ((2↑(𝐴 + 1)) − 1))} ∩ {𝐵}) |
123 | 8, 54 | gtned 10172 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐵 ≠ (𝐵 / ((2↑(𝐴 + 1)) − 1))) |
124 | | disjsn2 4247 |
. . . . . . . . . . . . . . . 16
⊢ (𝐵 ≠ (𝐵 / ((2↑(𝐴 + 1)) − 1)) → ({𝐵} ∩ {(𝐵 / ((2↑(𝐴 + 1)) − 1))}) =
∅) |
125 | 123, 124 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ({𝐵} ∩ {(𝐵 / ((2↑(𝐴 + 1)) − 1))}) =
∅) |
126 | 122, 125 | syl5eqr 2670 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ({(𝐵 / ((2↑(𝐴 + 1)) − 1))} ∩ {𝐵}) = ∅) |
127 | | df-pr 4180 |
. . . . . . . . . . . . . . 15
⊢ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} = ({(𝐵 / ((2↑(𝐴 + 1)) − 1))} ∪ {𝐵}) |
128 | 127 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} = ({(𝐵 / ((2↑(𝐴 + 1)) − 1))} ∪ {𝐵})) |
129 | | prfi 8235 |
. . . . . . . . . . . . . . 15
⊢ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∈ Fin |
130 | 129 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∈ Fin) |
131 | 72 | sselda 3603 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → 𝑘 ∈ ℕ) |
132 | 131 | nncnd 11036 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → 𝑘 ∈ ℂ) |
133 | 126, 128,
130, 132 | fsumsplit 14471 |
. . . . . . . . . . . . 13
⊢ (𝜑 → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 = (Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1))}𝑘 + Σ𝑘 ∈ {𝐵}𝑘)) |
134 | 84, 52 | mulcld 10060 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((2↑(𝐴 + 1)) − 1) · 𝐵) ∈
ℂ) |
135 | 52, 134, 84, 85 | divdird 10839 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐵 + (((2↑(𝐴 + 1)) − 1) · 𝐵)) / ((2↑(𝐴 + 1)) − 1)) = ((𝐵 / ((2↑(𝐴 + 1)) − 1)) + ((((2↑(𝐴 + 1)) − 1) · 𝐵) / ((2↑(𝐴 + 1)) − 1)))) |
136 | 35 | nncnd 11036 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (2↑(𝐴 + 1)) ∈ ℂ) |
137 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 1 ∈
ℂ) |
138 | 136, 137,
52 | subdird 10487 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (((2↑(𝐴 + 1)) − 1) · 𝐵) = (((2↑(𝐴 + 1)) · 𝐵) − (1 · 𝐵))) |
139 | 52 | mulid2d 10058 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (1 · 𝐵) = 𝐵) |
140 | 139 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (((2↑(𝐴 + 1)) · 𝐵) − (1 · 𝐵)) = (((2↑(𝐴 + 1)) · 𝐵) − 𝐵)) |
141 | 138, 140 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((2↑(𝐴 + 1)) − 1) · 𝐵) = (((2↑(𝐴 + 1)) · 𝐵) − 𝐵)) |
142 | 141 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐵 + (((2↑(𝐴 + 1)) − 1) · 𝐵)) = (𝐵 + (((2↑(𝐴 + 1)) · 𝐵) − 𝐵))) |
143 | 136, 52 | mulcld 10060 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((2↑(𝐴 + 1)) · 𝐵) ∈
ℂ) |
144 | 52, 143 | pncan3d 10395 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐵 + (((2↑(𝐴 + 1)) · 𝐵) − 𝐵)) = ((2↑(𝐴 + 1)) · 𝐵)) |
145 | 142, 144 | eqtrd 2656 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐵 + (((2↑(𝐴 + 1)) − 1) · 𝐵)) = ((2↑(𝐴 + 1)) · 𝐵)) |
146 | 145 | oveq1d 6665 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐵 + (((2↑(𝐴 + 1)) − 1) · 𝐵)) / ((2↑(𝐴 + 1)) − 1)) = (((2↑(𝐴 + 1)) · 𝐵) / ((2↑(𝐴 + 1)) − 1))) |
147 | 136, 52, 84, 85 | divassd 10836 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((2↑(𝐴 + 1)) · 𝐵) / ((2↑(𝐴 + 1)) − 1)) = ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1)))) |
148 | 146, 147 | eqtrd 2656 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐵 + (((2↑(𝐴 + 1)) − 1) · 𝐵)) / ((2↑(𝐴 + 1)) − 1)) = ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1)))) |
149 | 52, 84, 85 | divcan3d 10806 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((((2↑(𝐴 + 1)) − 1) · 𝐵) / ((2↑(𝐴 + 1)) − 1)) = 𝐵) |
150 | 149 | oveq2d 6666 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐵 / ((2↑(𝐴 + 1)) − 1)) + ((((2↑(𝐴 + 1)) − 1) · 𝐵) / ((2↑(𝐴 + 1)) − 1))) = ((𝐵 / ((2↑(𝐴 + 1)) − 1)) + 𝐵)) |
151 | 135, 148,
150 | 3eqtr3d 2664 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) = ((𝐵 / ((2↑(𝐴 + 1)) − 1)) + 𝐵)) |
152 | 121, 133,
151 | 3eqtr4d 2666 |
. . . . . . . . . . . 12
⊢ (𝜑 → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 = ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1)))) |
153 | 152 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 = ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1)))) |
154 | 74 | nncnd 11036 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → 𝑛 ∈ ℂ) |
155 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑛 → 𝑘 = 𝑛) |
156 | 155 | sumsn 14475 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℂ ∧ 𝑛 ∈ ℂ) →
Σ𝑘 ∈ {𝑛}𝑘 = 𝑛) |
157 | 154, 154,
156 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → Σ𝑘 ∈ {𝑛}𝑘 = 𝑛) |
158 | 153, 157 | oveq12d 6668 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 + Σ𝑘 ∈ {𝑛}𝑘) = (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛)) |
159 | 113, 158 | eqtrd 2656 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛}𝑘 = (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛)) |
160 | 3 | nnnn0d 11351 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐴 ∈
ℕ0) |
161 | | expp1 12867 |
. . . . . . . . . . . . . . . . 17
⊢ ((2
∈ ℂ ∧ 𝐴
∈ ℕ0) → (2↑(𝐴 + 1)) = ((2↑𝐴) · 2)) |
162 | 11, 160, 161 | sylancr 695 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (2↑(𝐴 + 1)) = ((2↑𝐴) · 2)) |
163 | | 2nn 11185 |
. . . . . . . . . . . . . . . . . . 19
⊢ 2 ∈
ℕ |
164 | | nnexpcl 12873 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((2
∈ ℕ ∧ 𝐴
∈ ℕ0) → (2↑𝐴) ∈ ℕ) |
165 | 163, 160,
164 | sylancr 695 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (2↑𝐴) ∈ ℕ) |
166 | 165 | nncnd 11036 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (2↑𝐴) ∈ ℂ) |
167 | | mulcom 10022 |
. . . . . . . . . . . . . . . . 17
⊢
(((2↑𝐴) ∈
ℂ ∧ 2 ∈ ℂ) → ((2↑𝐴) · 2) = (2 · (2↑𝐴))) |
168 | 166, 11, 167 | sylancl 694 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((2↑𝐴) · 2) = (2 · (2↑𝐴))) |
169 | 162, 168 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (2↑(𝐴 + 1)) = (2 · (2↑𝐴))) |
170 | 169 | oveq1d 6665 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((2↑(𝐴 + 1)) · 𝐵) = ((2 · (2↑𝐴)) · 𝐵)) |
171 | | 2cnd 11093 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 2 ∈
ℂ) |
172 | 171, 166,
52 | mulassd 10063 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((2 · (2↑𝐴)) · 𝐵) = (2 · ((2↑𝐴) · 𝐵))) |
173 | | 2prm 15405 |
. . . . . . . . . . . . . . . . . . 19
⊢ 2 ∈
ℙ |
174 | | coprm 15423 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((2
∈ ℙ ∧ 𝐵
∈ ℤ) → (¬ 2 ∥ 𝐵 ↔ (2 gcd 𝐵) = 1)) |
175 | 173, 91, 174 | sylancr 695 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (¬ 2 ∥ 𝐵 ↔ (2 gcd 𝐵) = 1)) |
176 | 4, 175 | mpbid 222 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (2 gcd 𝐵) = 1) |
177 | | 2z 11409 |
. . . . . . . . . . . . . . . . . . 19
⊢ 2 ∈
ℤ |
178 | 177 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 2 ∈
ℤ) |
179 | | rpexp1i 15433 |
. . . . . . . . . . . . . . . . . 18
⊢ ((2
∈ ℤ ∧ 𝐵
∈ ℤ ∧ 𝐴
∈ ℕ0) → ((2 gcd 𝐵) = 1 → ((2↑𝐴) gcd 𝐵) = 1)) |
180 | 178, 91, 160, 179 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((2 gcd 𝐵) = 1 → ((2↑𝐴) gcd 𝐵) = 1)) |
181 | 176, 180 | mpd 15 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((2↑𝐴) gcd 𝐵) = 1) |
182 | | sgmmul 24926 |
. . . . . . . . . . . . . . . 16
⊢ ((1
∈ ℂ ∧ ((2↑𝐴) ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ((2↑𝐴) gcd 𝐵) = 1)) → (1 σ ((2↑𝐴) · 𝐵)) = ((1 σ (2↑𝐴)) · (1 σ 𝐵))) |
183 | 137, 165,
1, 181, 182 | syl13anc 1328 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (1 σ ((2↑𝐴) · 𝐵)) = ((1 σ (2↑𝐴)) · (1 σ 𝐵))) |
184 | | pncan 10287 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝐴 + 1)
− 1) = 𝐴) |
185 | 28, 27, 184 | sylancl 694 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝐴 + 1) − 1) = 𝐴) |
186 | 185 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (2↑((𝐴 + 1) − 1)) =
(2↑𝐴)) |
187 | 186 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (1 σ (2↑((𝐴 + 1) − 1))) = (1 σ
(2↑𝐴))) |
188 | | 1sgm2ppw 24925 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 + 1) ∈ ℕ → (1
σ (2↑((𝐴 + 1)
− 1))) = ((2↑(𝐴
+ 1)) − 1)) |
189 | 19, 188 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (1 σ (2↑((𝐴 + 1) − 1))) =
((2↑(𝐴 + 1)) −
1)) |
190 | 187, 189 | eqtr3d 2658 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1 σ (2↑𝐴)) = ((2↑(𝐴 + 1)) − 1)) |
191 | 190 | oveq1d 6665 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((1 σ (2↑𝐴)) · (1 σ 𝐵)) = (((2↑(𝐴 + 1)) − 1) · (1
σ 𝐵))) |
192 | 183, 5, 191 | 3eqtr3d 2664 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (2 · ((2↑𝐴) · 𝐵)) = (((2↑(𝐴 + 1)) − 1) · (1 σ 𝐵))) |
193 | 170, 172,
192 | 3eqtrd 2660 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((2↑(𝐴 + 1)) · 𝐵) = (((2↑(𝐴 + 1)) − 1) · (1 σ 𝐵))) |
194 | 193 | oveq1d 6665 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((2↑(𝐴 + 1)) · 𝐵) / ((2↑(𝐴 + 1)) − 1)) = ((((2↑(𝐴 + 1)) − 1) · (1
σ 𝐵)) /
((2↑(𝐴 + 1)) −
1))) |
195 | | 1nn0 11308 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℕ0 |
196 | | sgmnncl 24873 |
. . . . . . . . . . . . . . 15
⊢ ((1
∈ ℕ0 ∧ 𝐵 ∈ ℕ) → (1 σ 𝐵) ∈
ℕ) |
197 | 195, 1, 196 | sylancr 695 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (1 σ 𝐵) ∈
ℕ) |
198 | 197 | nncnd 11036 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1 σ 𝐵) ∈
ℂ) |
199 | 198, 84, 85 | divcan3d 10806 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((((2↑(𝐴 + 1)) − 1) · (1
σ 𝐵)) /
((2↑(𝐴 + 1)) −
1)) = (1 σ 𝐵)) |
200 | 194, 147,
199 | 3eqtr3d 2664 |
. . . . . . . . . . 11
⊢ (𝜑 → ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) = (1 σ 𝐵)) |
201 | | sgmval 24868 |
. . . . . . . . . . . 12
⊢ ((1
∈ ℂ ∧ 𝐵
∈ ℕ) → (1 σ 𝐵) = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵} (𝑘↑𝑐1)) |
202 | 27, 1, 201 | sylancr 695 |
. . . . . . . . . . 11
⊢ (𝜑 → (1 σ 𝐵) = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵} (𝑘↑𝑐1)) |
203 | | simpr 477 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) → 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) |
204 | 64, 203 | sseldi 3601 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) → 𝑘 ∈ ℕ) |
205 | 204 | nncnd 11036 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) → 𝑘 ∈ ℂ) |
206 | 205 | cxp1d 24452 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) → (𝑘↑𝑐1) = 𝑘) |
207 | 206 | sumeq2dv 14433 |
. . . . . . . . . . 11
⊢ (𝜑 → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵} (𝑘↑𝑐1) = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}𝑘) |
208 | 200, 202,
207 | 3eqtrrd 2661 |
. . . . . . . . . 10
⊢ (𝜑 → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}𝑘 = ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1)))) |
209 | 208 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}𝑘 = ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1)))) |
210 | 104, 159,
209 | 3brtr3d 4684 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛) ≤ ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1)))) |
211 | 36, 8 | remulcld 10070 |
. . . . . . . . . . 11
⊢ (𝜑 → ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) ∈
ℝ) |
212 | 211 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) ∈
ℝ) |
213 | 74 | nnrpd 11870 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → 𝑛 ∈ ℝ+) |
214 | 212, 213 | ltaddrpd 11905 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) < (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛)) |
215 | 74 | nnred 11035 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → 𝑛 ∈ ℝ) |
216 | 212, 215 | readdcld 10069 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛) ∈ ℝ) |
217 | 212, 216 | ltnled 10184 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) < (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛) ↔ ¬ (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛) ≤ ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))) |
218 | 214, 217 | mpbid 222 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ¬ (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛) ≤ ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1)))) |
219 | 210, 218 | condan 835 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) → 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) |
220 | | elpri 4197 |
. . . . . . 7
⊢ (𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵)) |
221 | 219, 220 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵)) |
222 | 221 | expr 643 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛 ∥ 𝐵 → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵))) |
223 | 222 | ralrimiva 2966 |
. . . 4
⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝑛 ∥ 𝐵 → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵))) |
224 | 2, 55 | gtned 10172 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ≠ 1) |
225 | 224 | necomd 2849 |
. . . . . . . . 9
⊢ (𝜑 → 1 ≠ 𝐵) |
226 | | 1nn 11031 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℕ |
227 | 226 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 1 ∈
ℕ) |
228 | | 1dvds 14996 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ ℤ → 1 ∥
𝐵) |
229 | 91, 228 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 1 ∥ 𝐵) |
230 | | breq1 4656 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 1 → (𝑛 ∥ 𝐵 ↔ 1 ∥ 𝐵)) |
231 | | eqeq1 2626 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 1 → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ↔ 1 = (𝐵 / ((2↑(𝐴 + 1)) − 1)))) |
232 | | eqeq1 2626 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 1 → (𝑛 = 𝐵 ↔ 1 = 𝐵)) |
233 | 231, 232 | orbi12d 746 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 1 → ((𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵) ↔ (1 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 1 = 𝐵))) |
234 | 230, 233 | imbi12d 334 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 1 → ((𝑛 ∥ 𝐵 → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵)) ↔ (1 ∥ 𝐵 → (1 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 1 = 𝐵)))) |
235 | 234 | rspcv 3305 |
. . . . . . . . . . . 12
⊢ (1 ∈
ℕ → (∀𝑛
∈ ℕ (𝑛 ∥
𝐵 → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵)) → (1 ∥ 𝐵 → (1 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 1 = 𝐵)))) |
236 | 227, 223,
229, 235 | syl3c 66 |
. . . . . . . . . . 11
⊢ (𝜑 → (1 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 1 = 𝐵)) |
237 | 236 | ord 392 |
. . . . . . . . . 10
⊢ (𝜑 → (¬ 1 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) → 1 = 𝐵)) |
238 | 237 | necon1ad 2811 |
. . . . . . . . 9
⊢ (𝜑 → (1 ≠ 𝐵 → 1 = (𝐵 / ((2↑(𝐴 + 1)) − 1)))) |
239 | 225, 238 | mpd 15 |
. . . . . . . 8
⊢ (𝜑 → 1 = (𝐵 / ((2↑(𝐴 + 1)) − 1))) |
240 | 239 | eqeq2d 2632 |
. . . . . . 7
⊢ (𝜑 → (𝑛 = 1 ↔ 𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)))) |
241 | 240 | orbi1d 739 |
. . . . . 6
⊢ (𝜑 → ((𝑛 = 1 ∨ 𝑛 = 𝐵) ↔ (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵))) |
242 | 241 | imbi2d 330 |
. . . . 5
⊢ (𝜑 → ((𝑛 ∥ 𝐵 → (𝑛 = 1 ∨ 𝑛 = 𝐵)) ↔ (𝑛 ∥ 𝐵 → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵)))) |
243 | 242 | ralbidv 2986 |
. . . 4
⊢ (𝜑 → (∀𝑛 ∈ ℕ (𝑛 ∥ 𝐵 → (𝑛 = 1 ∨ 𝑛 = 𝐵)) ↔ ∀𝑛 ∈ ℕ (𝑛 ∥ 𝐵 → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵)))) |
244 | 223, 243 | mpbird 247 |
. . 3
⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝑛 ∥ 𝐵 → (𝑛 = 1 ∨ 𝑛 = 𝐵))) |
245 | | isprm2 15395 |
. . 3
⊢ (𝐵 ∈ ℙ ↔ (𝐵 ∈
(ℤ≥‘2) ∧ ∀𝑛 ∈ ℕ (𝑛 ∥ 𝐵 → (𝑛 = 1 ∨ 𝑛 = 𝐵)))) |
246 | 57, 244, 245 | sylanbrc 698 |
. 2
⊢ (𝜑 → 𝐵 ∈ ℙ) |
247 | 211 | ltp1d 10954 |
. . . 4
⊢ (𝜑 → ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) < (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1)) |
248 | | peano2re 10209 |
. . . . . 6
⊢
(((2↑(𝐴 + 1))
· (𝐵 /
((2↑(𝐴 + 1)) −
1))) ∈ ℝ → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ∈
ℝ) |
249 | 211, 248 | syl 17 |
. . . . 5
⊢ (𝜑 → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ∈
ℝ) |
250 | 211, 249 | ltnled 10184 |
. . . 4
⊢ (𝜑 → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) < (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ↔ ¬
(((2↑(𝐴 + 1)) ·
(𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ≤
((2↑(𝐴 + 1)) ·
(𝐵 / ((2↑(𝐴 + 1)) −
1))))) |
251 | 247, 250 | mpbid 222 |
. . 3
⊢ (𝜑 → ¬ (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ≤
((2↑(𝐴 + 1)) ·
(𝐵 / ((2↑(𝐴 + 1)) −
1)))) |
252 | 204 | nnred 11035 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) → 𝑘 ∈ ℝ) |
253 | 204 | nnnn0d 11351 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) → 𝑘 ∈ ℕ0) |
254 | 253 | nn0ge0d 11354 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) → 0 ≤ 𝑘) |
255 | | df-tp 4182 |
. . . . . . . . . 10
⊢ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} = ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∪ {1}) |
256 | | snssi 4339 |
. . . . . . . . . . . 12
⊢ (1 ∈
ℕ → {1} ⊆ ℕ) |
257 | 226, 256 | mp1i 13 |
. . . . . . . . . . 11
⊢ (𝜑 → {1} ⊆
ℕ) |
258 | 72, 257 | unssd 3789 |
. . . . . . . . . 10
⊢ (𝜑 → ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∪ {1}) ⊆
ℕ) |
259 | 255, 258 | syl5eqss 3649 |
. . . . . . . . 9
⊢ (𝜑 → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} ⊆ ℕ) |
260 | | eltpi 4229 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} → (𝑥 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑥 = 𝐵 ∨ 𝑥 = 1)) |
261 | | breq1 4656 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 1 → (𝑥 ∥ 𝐵 ↔ 1 ∥ 𝐵)) |
262 | 229, 261 | syl5ibrcom 237 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 = 1 → 𝑥 ∥ 𝐵)) |
263 | 89, 95, 262 | 3jaod 1392 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑥 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑥 = 𝐵 ∨ 𝑥 = 1) → 𝑥 ∥ 𝐵)) |
264 | 260, 263 | syl5 34 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} → 𝑥 ∥ 𝐵)) |
265 | 264 | imp 445 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1}) → 𝑥 ∥ 𝐵) |
266 | 259, 265 | ssrabdv 3681 |
. . . . . . . 8
⊢ (𝜑 → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} ⊆ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) |
267 | 62, 252, 254, 266 | fsumless 14528 |
. . . . . . 7
⊢ (𝜑 → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1}𝑘 ≤ Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}𝑘) |
268 | 267 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1}𝑘 ≤ Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}𝑘) |
269 | 52, 84, 85 | diveq1ad 10810 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐵 / ((2↑(𝐴 + 1)) − 1)) = 1 ↔ 𝐵 = ((2↑(𝐴 + 1)) − 1))) |
270 | 269 | necon3bid 2838 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐵 / ((2↑(𝐴 + 1)) − 1)) ≠ 1 ↔ 𝐵 ≠ ((2↑(𝐴 + 1)) −
1))) |
271 | 270 | biimpar 502 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ≠ 1) |
272 | 271 | necomd 2849 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → 1 ≠ (𝐵 / ((2↑(𝐴 + 1)) − 1))) |
273 | 225 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → 1 ≠ 𝐵) |
274 | 272, 273 | nelprd 4203 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → ¬ 1 ∈
{(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) |
275 | | disjsn 4246 |
. . . . . . . . 9
⊢ (({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∩ {1}) = ∅ ↔ ¬ 1 ∈
{(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) |
276 | 274, 275 | sylibr 224 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∩ {1}) = ∅) |
277 | 255 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} = ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∪ {1})) |
278 | | tpfi 8236 |
. . . . . . . . 9
⊢ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} ∈ Fin |
279 | 278 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} ∈ Fin) |
280 | 259 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} ⊆ ℕ) |
281 | 280 | sselda 3603 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) ∧ 𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1}) → 𝑘 ∈ ℕ) |
282 | 281 | nncnd 11036 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) ∧ 𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1}) → 𝑘 ∈ ℂ) |
283 | 276, 277,
279, 282 | fsumsplit 14471 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1}𝑘 = (Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 + Σ𝑘 ∈ {1}𝑘)) |
284 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑘 = 1 → 𝑘 = 1) |
285 | 284 | sumsn 14475 |
. . . . . . . . . 10
⊢ ((1
∈ ℝ ∧ 1 ∈ ℂ) → Σ𝑘 ∈ {1}𝑘 = 1) |
286 | 2, 27, 285 | sylancl 694 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑘 ∈ {1}𝑘 = 1) |
287 | 152, 286 | oveq12d 6668 |
. . . . . . . 8
⊢ (𝜑 → (Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 + Σ𝑘 ∈ {1}𝑘) = (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1)) |
288 | 287 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → (Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 + Σ𝑘 ∈ {1}𝑘) = (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1)) |
289 | 283, 288 | eqtrd 2656 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1}𝑘 = (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1)) |
290 | 208 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}𝑘 = ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1)))) |
291 | 268, 289,
290 | 3brtr3d 4684 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ≤
((2↑(𝐴 + 1)) ·
(𝐵 / ((2↑(𝐴 + 1)) −
1)))) |
292 | 291 | ex 450 |
. . . 4
⊢ (𝜑 → (𝐵 ≠ ((2↑(𝐴 + 1)) − 1) → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ≤
((2↑(𝐴 + 1)) ·
(𝐵 / ((2↑(𝐴 + 1)) −
1))))) |
293 | 292 | necon1bd 2812 |
. . 3
⊢ (𝜑 → (¬ (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ≤
((2↑(𝐴 + 1)) ·
(𝐵 / ((2↑(𝐴 + 1)) − 1))) → 𝐵 = ((2↑(𝐴 + 1)) − 1))) |
294 | 251, 293 | mpd 15 |
. 2
⊢ (𝜑 → 𝐵 = ((2↑(𝐴 + 1)) − 1)) |
295 | 246, 294 | jca 554 |
1
⊢ (𝜑 → (𝐵 ∈ ℙ ∧ 𝐵 = ((2↑(𝐴 + 1)) − 1))) |