Step | Hyp | Ref
| Expression |
1 | | oddpwdc.f |
. . 3
⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦
((2↑𝑦) · 𝑥)) |
2 | | 2nn 12035 |
. . . . . . . 8
⊢ 2 ∈
ℕ |
3 | 2 | a1i 11 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ0
∧ 𝑥 ∈ 𝐽) → 2 ∈
ℕ) |
4 | | simpl 483 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ0
∧ 𝑥 ∈ 𝐽) → 𝑦 ∈ ℕ0) |
5 | 3, 4 | nnexpcld 13949 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ0
∧ 𝑥 ∈ 𝐽) → (2↑𝑦) ∈
ℕ) |
6 | | oddpwdc.j |
. . . . . . . 8
⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} |
7 | | ssrab2 4014 |
. . . . . . . 8
⊢ {𝑧 ∈ ℕ ∣ ¬ 2
∥ 𝑧} ⊆
ℕ |
8 | 6, 7 | eqsstri 3956 |
. . . . . . 7
⊢ 𝐽 ⊆
ℕ |
9 | | simpr 485 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ0
∧ 𝑥 ∈ 𝐽) → 𝑥 ∈ 𝐽) |
10 | 8, 9 | sselid 3920 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ0
∧ 𝑥 ∈ 𝐽) → 𝑥 ∈ ℕ) |
11 | 5, 10 | nnmulcld 12015 |
. . . . 5
⊢ ((𝑦 ∈ ℕ0
∧ 𝑥 ∈ 𝐽) → ((2↑𝑦) · 𝑥) ∈ ℕ) |
12 | 11 | ancoms 459 |
. . . 4
⊢ ((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) →
((2↑𝑦) · 𝑥) ∈
ℕ) |
13 | 12 | adantl 482 |
. . 3
⊢
((⊤ ∧ (𝑥
∈ 𝐽 ∧ 𝑦 ∈ ℕ0))
→ ((2↑𝑦) ·
𝑥) ∈
ℕ) |
14 | | id 22 |
. . . . . . 7
⊢ (𝑎 ∈ ℕ → 𝑎 ∈
ℕ) |
15 | 2 | a1i 11 |
. . . . . . . 8
⊢ (𝑎 ∈ ℕ → 2 ∈
ℕ) |
16 | | nn0ssre 12226 |
. . . . . . . . . . 11
⊢
ℕ0 ⊆ ℝ |
17 | | ltso 11044 |
. . . . . . . . . . 11
⊢ < Or
ℝ |
18 | | soss 5520 |
. . . . . . . . . . 11
⊢
(ℕ0 ⊆ ℝ → ( < Or ℝ →
< Or ℕ0)) |
19 | 16, 17, 18 | mp2 9 |
. . . . . . . . . 10
⊢ < Or
ℕ0 |
20 | 19 | a1i 11 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℕ → < Or
ℕ0) |
21 | | 0zd 12320 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ℕ → 0 ∈
ℤ) |
22 | | ssrab2 4014 |
. . . . . . . . . . 11
⊢ {𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎} ⊆
ℕ0 |
23 | 22 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ℕ → {𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎} ⊆
ℕ0) |
24 | | nnz 12331 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ ℕ → 𝑎 ∈
ℤ) |
25 | | oveq2 7277 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑛 → (2↑𝑘) = (2↑𝑛)) |
26 | 25 | breq1d 5085 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑛 → ((2↑𝑘) ∥ 𝑎 ↔ (2↑𝑛) ∥ 𝑎)) |
27 | 26 | elrab 3625 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎} ↔ (𝑛 ∈ ℕ0 ∧
(2↑𝑛) ∥ 𝑎)) |
28 | | simprl 768 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0
∧ (2↑𝑛) ∥
𝑎)) → 𝑛 ∈
ℕ0) |
29 | 28 | nn0red 12283 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0
∧ (2↑𝑛) ∥
𝑎)) → 𝑛 ∈
ℝ) |
30 | 2 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0
∧ (2↑𝑛) ∥
𝑎)) → 2 ∈
ℕ) |
31 | 30, 28 | nnexpcld 13949 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0
∧ (2↑𝑛) ∥
𝑎)) → (2↑𝑛) ∈
ℕ) |
32 | 31 | nnred 11977 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0
∧ (2↑𝑛) ∥
𝑎)) → (2↑𝑛) ∈
ℝ) |
33 | | simpl 483 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0
∧ (2↑𝑛) ∥
𝑎)) → 𝑎 ∈
ℕ) |
34 | 33 | nnred 11977 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0
∧ (2↑𝑛) ∥
𝑎)) → 𝑎 ∈
ℝ) |
35 | | 2re 12036 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℝ |
36 | 35 | leidi 11498 |
. . . . . . . . . . . . . . . 16
⊢ 2 ≤
2 |
37 | | nexple 31964 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈ ℕ0
∧ 2 ∈ ℝ ∧ 2 ≤ 2) → 𝑛 ≤ (2↑𝑛)) |
38 | 35, 36, 37 | mp3an23 1452 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ0
→ 𝑛 ≤ (2↑𝑛)) |
39 | 38 | ad2antrl 725 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0
∧ (2↑𝑛) ∥
𝑎)) → 𝑛 ≤ (2↑𝑛)) |
40 | 31 | nnzd 12414 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0
∧ (2↑𝑛) ∥
𝑎)) → (2↑𝑛) ∈
ℤ) |
41 | | simprr 770 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0
∧ (2↑𝑛) ∥
𝑎)) → (2↑𝑛) ∥ 𝑎) |
42 | | dvdsle 16008 |
. . . . . . . . . . . . . . . 16
⊢
(((2↑𝑛) ∈
ℤ ∧ 𝑎 ∈
ℕ) → ((2↑𝑛)
∥ 𝑎 →
(2↑𝑛) ≤ 𝑎)) |
43 | 42 | imp 407 |
. . . . . . . . . . . . . . 15
⊢
((((2↑𝑛) ∈
ℤ ∧ 𝑎 ∈
ℕ) ∧ (2↑𝑛)
∥ 𝑎) →
(2↑𝑛) ≤ 𝑎) |
44 | 40, 33, 41, 43 | syl21anc 835 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0
∧ (2↑𝑛) ∥
𝑎)) → (2↑𝑛) ≤ 𝑎) |
45 | 29, 32, 34, 39, 44 | letrd 11121 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0
∧ (2↑𝑛) ∥
𝑎)) → 𝑛 ≤ 𝑎) |
46 | 27, 45 | sylan2b 594 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}) → 𝑛 ≤ 𝑎) |
47 | 46 | ralrimiva 3103 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ ℕ →
∀𝑛 ∈ {𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}𝑛 ≤ 𝑎) |
48 | | brralrspcev 5135 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ ℤ ∧
∀𝑛 ∈ {𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}𝑛 ≤ 𝑎) → ∃𝑚 ∈ ℤ ∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}𝑛 ≤ 𝑚) |
49 | 24, 47, 48 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ℕ →
∃𝑚 ∈ ℤ
∀𝑛 ∈ {𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}𝑛 ≤ 𝑚) |
50 | | nn0uz 12609 |
. . . . . . . . . . 11
⊢
ℕ0 = (ℤ≥‘0) |
51 | 50 | uzsupss 12669 |
. . . . . . . . . 10
⊢ ((0
∈ ℤ ∧ {𝑘
∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ⊆ ℕ0 ∧
∃𝑚 ∈ ℤ
∀𝑛 ∈ {𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}𝑛 ≤ 𝑚) → ∃𝑚 ∈ ℕ0 (∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎} ¬ 𝑚 < 𝑛 ∧ ∀𝑛 ∈ ℕ0 (𝑛 < 𝑚 → ∃𝑜 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}𝑛 < 𝑜))) |
52 | 21, 23, 49, 51 | syl3anc 1370 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℕ →
∃𝑚 ∈
ℕ0 (∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎} ¬ 𝑚 < 𝑛 ∧ ∀𝑛 ∈ ℕ0 (𝑛 < 𝑚 → ∃𝑜 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}𝑛 < 𝑜))) |
53 | 20, 52 | supcl 9206 |
. . . . . . . 8
⊢ (𝑎 ∈ ℕ →
sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈
ℕ0) |
54 | 15, 53 | nnexpcld 13949 |
. . . . . . 7
⊢ (𝑎 ∈ ℕ →
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∈
ℕ) |
55 | | fzfi 13681 |
. . . . . . . . . . . 12
⊢
(0...𝑎) ∈
Fin |
56 | | 0zd 12320 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}) → 0 ∈
ℤ) |
57 | 24 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}) → 𝑎 ∈ ℤ) |
58 | 27, 28 | sylan2b 594 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}) → 𝑛 ∈ ℕ0) |
59 | 58 | nn0zd 12413 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}) → 𝑛 ∈ ℤ) |
60 | 58 | nn0ge0d 12285 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}) → 0 ≤ 𝑛) |
61 | 56, 57, 59, 60, 46 | elfzd 13236 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}) → 𝑛 ∈ (0...𝑎)) |
62 | 61 | ex 413 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ ℕ → (𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎} → 𝑛 ∈ (0...𝑎))) |
63 | 62 | ssrdv 3928 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ ℕ → {𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎} ⊆ (0...𝑎)) |
64 | | ssfi 8945 |
. . . . . . . . . . . 12
⊢
(((0...𝑎) ∈ Fin
∧ {𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ⊆ (0...𝑎)) → {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎} ∈ Fin) |
65 | 55, 63, 64 | sylancr 587 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ ℕ → {𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎} ∈
Fin) |
66 | | 0nn0 12237 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℕ0 |
67 | 66 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ ℕ → 0 ∈
ℕ0) |
68 | | 2cn 12037 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℂ |
69 | | exp0 13775 |
. . . . . . . . . . . . . . 15
⊢ (2 ∈
ℂ → (2↑0) = 1) |
70 | 68, 69 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
(2↑0) = 1 |
71 | | 1dvds 15969 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ ℤ → 1 ∥
𝑎) |
72 | 24, 71 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ ℕ → 1 ∥
𝑎) |
73 | 70, 72 | eqbrtrid 5110 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ ℕ →
(2↑0) ∥ 𝑎) |
74 | | oveq2 7277 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 0 → (2↑𝑘) = (2↑0)) |
75 | 74 | breq1d 5085 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 0 → ((2↑𝑘) ∥ 𝑎 ↔ (2↑0) ∥ 𝑎)) |
76 | 75 | elrab 3625 |
. . . . . . . . . . . . 13
⊢ (0 ∈
{𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ↔ (0 ∈ ℕ0 ∧
(2↑0) ∥ 𝑎)) |
77 | 67, 73, 76 | sylanbrc 583 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ ℕ → 0 ∈
{𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}) |
78 | 77 | ne0d 4271 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ ℕ → {𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎} ≠
∅) |
79 | | fisupcl 9217 |
. . . . . . . . . . 11
⊢ (( <
Or ℕ0 ∧ ({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎} ∈ Fin ∧ {𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎} ≠ ∅ ∧
{𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ⊆ ℕ0)) →
sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ {𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}) |
80 | 20, 65, 78, 23, 79 | syl13anc 1371 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ℕ →
sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ {𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}) |
81 | | oveq2 7277 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑙 → (2↑𝑘) = (2↑𝑙)) |
82 | 81 | breq1d 5085 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑙 → ((2↑𝑘) ∥ 𝑎 ↔ (2↑𝑙) ∥ 𝑎)) |
83 | 82 | cbvrabv 3425 |
. . . . . . . . . 10
⊢ {𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎} = {𝑙 ∈ ℕ0 ∣
(2↑𝑙) ∥ 𝑎} |
84 | 80, 83 | eleqtrdi 2849 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℕ →
sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ {𝑙 ∈ ℕ0
∣ (2↑𝑙) ∥
𝑎}) |
85 | | oveq2 7277 |
. . . . . . . . . . 11
⊢ (𝑙 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
→ (2↑𝑙) =
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, <
))) |
86 | 85 | breq1d 5085 |
. . . . . . . . . 10
⊢ (𝑙 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
→ ((2↑𝑙) ∥
𝑎 ↔ (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< )) ∥ 𝑎)) |
87 | 86 | elrab 3625 |
. . . . . . . . 9
⊢
(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ {𝑙 ∈ ℕ0
∣ (2↑𝑙) ∥
𝑎} ↔ (sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ) ∈ ℕ0 ∧ (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
∥ 𝑎)) |
88 | 84, 87 | sylib 217 |
. . . . . . . 8
⊢ (𝑎 ∈ ℕ →
(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈
ℕ0 ∧ (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
∥ 𝑎)) |
89 | 88 | simprd 496 |
. . . . . . 7
⊢ (𝑎 ∈ ℕ →
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∥ 𝑎) |
90 | | nndivdvds 15961 |
. . . . . . . 8
⊢ ((𝑎 ∈ ℕ ∧
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∈
ℕ) → ((2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
∥ 𝑎 ↔ (𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) ∈ ℕ)) |
91 | 90 | biimpa 477 |
. . . . . . 7
⊢ (((𝑎 ∈ ℕ ∧
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∈
ℕ) ∧ (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
∥ 𝑎) → (𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) ∈ ℕ) |
92 | 14, 54, 89, 91 | syl21anc 835 |
. . . . . 6
⊢ (𝑎 ∈ ℕ → (𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) ∈ ℕ) |
93 | | 1nn0 12238 |
. . . . . . . . . . 11
⊢ 1 ∈
ℕ0 |
94 | 93 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ℕ → 1 ∈
ℕ0) |
95 | 53, 94 | nn0addcld 12286 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℕ →
(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈
ℕ0) |
96 | 53 | nn0red 12283 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ ℕ →
sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈
ℝ) |
97 | 96 | ltp1d 11894 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ ℕ →
sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) <
(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) +
1)) |
98 | 20, 52 | supub 9207 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ ℕ →
((sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈
{𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎} → ¬ sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
< (sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) +
1))) |
99 | 97, 98 | mt2d 136 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ ℕ → ¬
(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈
{𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}) |
100 | 83 | eleq2i 2830 |
. . . . . . . . . . . 12
⊢
((sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈
{𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ↔ (sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ) +
1) ∈ {𝑙 ∈
ℕ0 ∣ (2↑𝑙) ∥ 𝑎}) |
101 | 99, 100 | sylnib 328 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ ℕ → ¬
(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈
{𝑙 ∈
ℕ0 ∣ (2↑𝑙) ∥ 𝑎}) |
102 | | oveq2 7277 |
. . . . . . . . . . . . 13
⊢ (𝑙 = (sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ) +
1) → (2↑𝑙) =
(2↑(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) +
1))) |
103 | 102 | breq1d 5085 |
. . . . . . . . . . . 12
⊢ (𝑙 = (sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ) +
1) → ((2↑𝑙)
∥ 𝑎 ↔
(2↑(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) ∥
𝑎)) |
104 | 103 | elrab 3625 |
. . . . . . . . . . 11
⊢
((sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈
{𝑙 ∈
ℕ0 ∣ (2↑𝑙) ∥ 𝑎} ↔ ((sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ) +
1) ∈ ℕ0 ∧ (2↑(sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ) +
1)) ∥ 𝑎)) |
105 | 101, 104 | sylnib 328 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ℕ → ¬
((sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈
ℕ0 ∧ (2↑(sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ) +
1)) ∥ 𝑎)) |
106 | | imnan 400 |
. . . . . . . . . 10
⊢
(((sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈
ℕ0 → ¬ (2↑(sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ) +
1)) ∥ 𝑎) ↔ ¬
((sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈
ℕ0 ∧ (2↑(sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ) +
1)) ∥ 𝑎)) |
107 | 105, 106 | sylibr 233 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℕ →
((sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈
ℕ0 → ¬ (2↑(sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ) +
1)) ∥ 𝑎)) |
108 | 95, 107 | mpd 15 |
. . . . . . . 8
⊢ (𝑎 ∈ ℕ → ¬
(2↑(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) ∥
𝑎) |
109 | | expp1 13778 |
. . . . . . . . . 10
⊢ ((2
∈ ℂ ∧ sup({𝑘
∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈
ℕ0) → (2↑(sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ) +
1)) = ((2↑sup({𝑘
∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ·
2)) |
110 | 68, 53, 109 | sylancr 587 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℕ →
(2↑(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) =
((2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ·
2)) |
111 | 110 | breq1d 5085 |
. . . . . . . 8
⊢ (𝑎 ∈ ℕ →
((2↑(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) ∥
𝑎 ↔
((2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2)
∥ 𝑎)) |
112 | 108, 111 | mtbid 324 |
. . . . . . 7
⊢ (𝑎 ∈ ℕ → ¬
((2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2)
∥ 𝑎) |
113 | | nncn 11970 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ ℕ → 𝑎 ∈
ℂ) |
114 | 54 | nncnd 11978 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ ℕ →
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∈
ℂ) |
115 | 54 | nnne0d 12012 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ ℕ →
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ≠
0) |
116 | 113, 114,
115 | divcan2d 11742 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ℕ →
((2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ·
(𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< )))) = 𝑎) |
117 | 116 | eqcomd 2744 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℕ → 𝑎 = ((2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< )) · (𝑎 /
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, <
))))) |
118 | 117 | breq2d 5087 |
. . . . . . . 8
⊢ (𝑎 ∈ ℕ →
(((2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2)
∥ 𝑎 ↔
((2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2)
∥ ((2↑sup({𝑘
∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ·
(𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< )))))) |
119 | 15 | nnzd 12414 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℕ → 2 ∈
ℤ) |
120 | 92 | nnzd 12414 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℕ → (𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) ∈ ℤ) |
121 | 54 | nnzd 12414 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℕ →
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∈
ℤ) |
122 | | dvdscmulr 15983 |
. . . . . . . . 9
⊢ ((2
∈ ℤ ∧ (𝑎 /
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈
ℤ ∧ ((2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
∈ ℤ ∧ (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
≠ 0)) → (((2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
· 2) ∥ ((2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
· (𝑎 /
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))) ↔ 2
∥ (𝑎 /
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, <
))))) |
123 | 119, 120,
121, 115, 122 | syl112anc 1373 |
. . . . . . . 8
⊢ (𝑎 ∈ ℕ →
(((2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2)
∥ ((2↑sup({𝑘
∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ·
(𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< )))) ↔ 2 ∥ (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, <
))))) |
124 | 118, 123 | bitrd 278 |
. . . . . . 7
⊢ (𝑎 ∈ ℕ →
(((2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2)
∥ 𝑎 ↔ 2 ∥
(𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))))) |
125 | 112, 124 | mtbid 324 |
. . . . . 6
⊢ (𝑎 ∈ ℕ → ¬ 2
∥ (𝑎 /
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, <
)))) |
126 | | breq2 5079 |
. . . . . . . 8
⊢ (𝑧 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
→ (2 ∥ 𝑧 ↔
2 ∥ (𝑎 /
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, <
))))) |
127 | 126 | notbid 318 |
. . . . . . 7
⊢ (𝑧 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
→ (¬ 2 ∥ 𝑧
↔ ¬ 2 ∥ (𝑎 /
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, <
))))) |
128 | 127, 6 | elrab2 3628 |
. . . . . 6
⊢ ((𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) ∈ 𝐽 ↔
((𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) ∈ ℕ ∧ ¬ 2 ∥ (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, <
))))) |
129 | 92, 125, 128 | sylanbrc 583 |
. . . . 5
⊢ (𝑎 ∈ ℕ → (𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) ∈ 𝐽) |
130 | 129, 53 | jca 512 |
. . . 4
⊢ (𝑎 ∈ ℕ → ((𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) ∈ 𝐽 ∧
sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈
ℕ0)) |
131 | 130 | adantl 482 |
. . 3
⊢
((⊤ ∧ 𝑎
∈ ℕ) → ((𝑎
/ (2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ 𝐽 ∧ sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
∈ ℕ0)) |
132 | | simpr 485 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑎 = ((2↑𝑦) · 𝑥)) |
133 | 2 | a1i 11 |
. . . . . . . . 9
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 2 ∈ ℕ) |
134 | | simplr 766 |
. . . . . . . . 9
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑦 ∈ ℕ0) |
135 | 133, 134 | nnexpcld 13949 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (2↑𝑦) ∈ ℕ) |
136 | 8 | sseli 3918 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐽 → 𝑥 ∈ ℕ) |
137 | 136 | ad2antrr 723 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑥 ∈ ℕ) |
138 | 135, 137 | nnmulcld 12015 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → ((2↑𝑦) · 𝑥) ∈ ℕ) |
139 | 132, 138 | eqeltrd 2839 |
. . . . . 6
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑎 ∈ ℕ) |
140 | | simplll 772 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑥 ∈ 𝐽) |
141 | | breq2 5079 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑥 → (2 ∥ 𝑧 ↔ 2 ∥ 𝑥)) |
142 | 141 | notbid 318 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑥 → (¬ 2 ∥ 𝑧 ↔ ¬ 2 ∥ 𝑥)) |
143 | 142, 6 | elrab2 3628 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐽 ↔ (𝑥 ∈ ℕ ∧ ¬ 2 ∥ 𝑥)) |
144 | 143 | simprbi 497 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐽 → ¬ 2 ∥ 𝑥) |
145 | | 2z 12341 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℤ |
146 | 134 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑦 ∈
ℕ0) |
147 | 146 | nn0zd 12413 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑦 ∈
ℤ) |
148 | 19 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ < Or ℕ0) |
149 | 139, 52 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → ∃𝑚 ∈ ℕ0 (∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎} ¬ 𝑚 < 𝑛 ∧ ∀𝑛 ∈ ℕ0 (𝑛 < 𝑚 → ∃𝑜 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}𝑛 < 𝑜))) |
150 | 149 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ ∃𝑚 ∈
ℕ0 (∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎} ¬ 𝑚 < 𝑛 ∧ ∀𝑛 ∈ ℕ0 (𝑛 < 𝑚 → ∃𝑜 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}𝑛 < 𝑜))) |
151 | 148, 150 | supcl 9206 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈
ℕ0) |
152 | 151 | nn0zd 12413 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈
ℤ) |
153 | | simpr 485 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑦 < sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< )) |
154 | | znnsub 12355 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℤ ∧ sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ) ∈ ℤ) → (𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
↔ (sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦) ∈
ℕ)) |
155 | 154 | biimpa 477 |
. . . . . . . . . . . . . . 15
⊢ (((𝑦 ∈ ℤ ∧ sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ) ∈ ℤ) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦) ∈
ℕ) |
156 | 147, 152,
153, 155 | syl21anc 835 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦) ∈
ℕ) |
157 | | iddvdsexp 15978 |
. . . . . . . . . . . . . 14
⊢ ((2
∈ ℤ ∧ (sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
− 𝑦) ∈ ℕ)
→ 2 ∥ (2↑(sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
− 𝑦))) |
158 | 145, 156,
157 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 2 ∥ (2↑(sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
− 𝑦))) |
159 | 145 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 2 ∈ ℤ) |
160 | 139, 120 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∈ ℤ) |
161 | 160 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (𝑎 /
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈
ℤ) |
162 | 156 | nnnn0d 12282 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦) ∈
ℕ0) |
163 | | zexpcl 13786 |
. . . . . . . . . . . . . . 15
⊢ ((2
∈ ℤ ∧ (sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
− 𝑦) ∈
ℕ0) → (2↑(sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
− 𝑦)) ∈
ℤ) |
164 | 145, 162,
163 | sylancr 587 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (2↑(sup({𝑘
∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) ∈
ℤ) |
165 | | dvdsmultr2 15996 |
. . . . . . . . . . . . . 14
⊢ ((2
∈ ℤ ∧ (𝑎 /
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈
ℤ ∧ (2↑(sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
− 𝑦)) ∈ ℤ)
→ (2 ∥ (2↑(sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
− 𝑦)) → 2
∥ ((𝑎 /
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ·
(2↑(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦))))) |
166 | 159, 161,
164, 165 | syl3anc 1370 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (2 ∥ (2↑(sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
− 𝑦)) → 2
∥ ((𝑎 /
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ·
(2↑(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦))))) |
167 | 158, 166 | mpd 15 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 2 ∥ ((𝑎 /
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ·
(2↑(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)))) |
168 | 137 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑥 ∈
ℕ) |
169 | 168 | nncnd 11978 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑥 ∈
ℂ) |
170 | | 2cnd 12040 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 2 ∈ ℂ) |
171 | 170, 162 | expcld 13853 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (2↑(sup({𝑘
∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) ∈
ℂ) |
172 | 139 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑎 ∈
ℕ) |
173 | 172 | nncnd 11978 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑎 ∈
ℂ) |
174 | 172, 114 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (2↑sup({𝑘
∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∈
ℂ) |
175 | | 2ne0 12066 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ≠
0 |
176 | 175 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 2 ≠ 0) |
177 | 170, 176,
152 | expne0d 13859 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (2↑sup({𝑘
∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ≠
0) |
178 | 173, 174,
177 | divcld 11740 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (𝑎 /
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈
ℂ) |
179 | 171, 178 | mulcld 10984 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ ((2↑(sup({𝑘
∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, <
)))) ∈ ℂ) |
180 | 170, 146 | expcld 13853 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (2↑𝑦) ∈
ℂ) |
181 | 170, 176,
147 | expne0d 13859 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (2↑𝑦) ≠
0) |
182 | 172, 117 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑎 =
((2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ·
(𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))))) |
183 | | simplr 766 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑎 = ((2↑𝑦) · 𝑥)) |
184 | 146 | nn0cnd 12284 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑦 ∈
ℂ) |
185 | 151 | nn0cnd 12284 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈
ℂ) |
186 | 184, 185 | pncan3d 11324 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (𝑦 + (sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ) − 𝑦)) =
sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, <
)) |
187 | 186 | oveq2d 7285 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (2↑(𝑦 +
(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦))) = (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) |
188 | 170, 162,
146 | expaddd 13855 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (2↑(𝑦 +
(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦))) = ((2↑𝑦) · (2↑(sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ) − 𝑦)))) |
189 | 187, 188 | eqtr3d 2780 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (2↑sup({𝑘
∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) =
((2↑𝑦) ·
(2↑(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)))) |
190 | 189 | oveq1d 7284 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ ((2↑sup({𝑘
∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ·
(𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< )))) = (((2↑𝑦)
· (2↑(sup({𝑘
∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦))) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, <
))))) |
191 | 182, 183,
190 | 3eqtr3d 2786 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ ((2↑𝑦) ·
𝑥) = (((2↑𝑦) · (2↑(sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ) − 𝑦)))
· (𝑎 /
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, <
))))) |
192 | 180, 171,
178 | mulassd 10987 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (((2↑𝑦)
· (2↑(sup({𝑘
∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦))) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, <
)))) = ((2↑𝑦) ·
((2↑(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, <
)))))) |
193 | 191, 192 | eqtrd 2778 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ ((2↑𝑦) ·
𝑥) = ((2↑𝑦) · ((2↑(sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ) − 𝑦)) ·
(𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< )))))) |
194 | 169, 179,
180, 181, 193 | mulcanad 11599 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑥 =
((2↑(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, <
))))) |
195 | 178, 171 | mulcomd 10985 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ ((𝑎 /
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ·
(2↑(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦))) = ((2↑(sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ) − 𝑦)) ·
(𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))))) |
196 | 194, 195 | eqtr4d 2781 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑥 = ((𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) · (2↑(sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
− 𝑦)))) |
197 | 167, 196 | breqtrrd 5103 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 2 ∥ 𝑥) |
198 | 144, 197 | nsyl3 138 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ ¬ 𝑥 ∈ 𝐽) |
199 | 140, 198 | pm2.65da 814 |
. . . . . . . . 9
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → ¬ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, <
)) |
200 | 137 | nnzd 12414 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑥 ∈ ℤ) |
201 | 135 | nnzd 12414 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (2↑𝑦) ∈ ℤ) |
202 | 139 | nnzd 12414 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑎 ∈ ℤ) |
203 | 135 | nncnd 11978 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (2↑𝑦) ∈ ℂ) |
204 | 137 | nncnd 11978 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑥 ∈ ℂ) |
205 | 203, 204 | mulcomd 10985 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → ((2↑𝑦) · 𝑥) = (𝑥 · (2↑𝑦))) |
206 | 132, 205 | eqtr2d 2779 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑥 · (2↑𝑦)) = 𝑎) |
207 | | dvds0lem 15965 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℤ ∧
(2↑𝑦) ∈ ℤ
∧ 𝑎 ∈ ℤ)
∧ (𝑥 ·
(2↑𝑦)) = 𝑎) → (2↑𝑦) ∥ 𝑎) |
208 | 200, 201,
202, 206, 207 | syl31anc 1372 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (2↑𝑦) ∥ 𝑎) |
209 | | oveq2 7277 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑦 → (2↑𝑘) = (2↑𝑦)) |
210 | 209 | breq1d 5085 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑦 → ((2↑𝑘) ∥ 𝑎 ↔ (2↑𝑦) ∥ 𝑎)) |
211 | 210 | elrab 3625 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎} ↔ (𝑦 ∈ ℕ0 ∧
(2↑𝑦) ∥ 𝑎)) |
212 | 134, 208,
211 | sylanbrc 583 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑦 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}) |
213 | 19 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → < Or
ℕ0) |
214 | 213, 149 | supub 9207 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑦 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎} → ¬ sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ) < 𝑦)) |
215 | 212, 214 | mpd 15 |
. . . . . . . . 9
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → ¬ sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
< 𝑦) |
216 | 134 | nn0red 12283 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑦 ∈ ℝ) |
217 | 139, 96 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
∈ ℝ) |
218 | 216, 217 | lttri3d 11104 |
. . . . . . . . 9
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
↔ (¬ 𝑦 <
sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∧ ¬
sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) < 𝑦))) |
219 | 199, 215,
218 | mpbir2and 710 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, <
)) |
220 | | simplr 766 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑎 = ((2↑𝑦) · 𝑥)) |
221 | 139 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑎 ∈
ℕ) |
222 | 221 | nncnd 11978 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑎 ∈
ℂ) |
223 | 137 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑥 ∈
ℕ) |
224 | 223 | nncnd 11978 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑥 ∈
ℂ) |
225 | | nnexpcl 13784 |
. . . . . . . . . . . . . . . 16
⊢ ((2
∈ ℕ ∧ 𝑦
∈ ℕ0) → (2↑𝑦) ∈ ℕ) |
226 | 2, 225 | mpan 687 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℕ0
→ (2↑𝑦) ∈
ℕ) |
227 | 226 | nncnd 11978 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ0
→ (2↑𝑦) ∈
ℂ) |
228 | 226 | nnne0d 12012 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ0
→ (2↑𝑦) ≠
0) |
229 | 227, 228 | jca 512 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ0
→ ((2↑𝑦) ∈
ℂ ∧ (2↑𝑦)
≠ 0)) |
230 | 229 | ad3antlr 728 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ ((2↑𝑦) ∈
ℂ ∧ (2↑𝑦)
≠ 0)) |
231 | | divmul2 11626 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧
((2↑𝑦) ∈ ℂ
∧ (2↑𝑦) ≠ 0))
→ ((𝑎 / (2↑𝑦)) = 𝑥 ↔ 𝑎 = ((2↑𝑦) · 𝑥))) |
232 | 222, 224,
230, 231 | syl3anc 1370 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ ((𝑎 / (2↑𝑦)) = 𝑥 ↔ 𝑎 = ((2↑𝑦) · 𝑥))) |
233 | 220, 232 | mpbird 256 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (𝑎 / (2↑𝑦)) = 𝑥) |
234 | | simpr 485 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< )) |
235 | 234 | oveq2d 7285 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (2↑𝑦) =
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, <
))) |
236 | 235 | oveq2d 7285 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (𝑎 / (2↑𝑦)) = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, <
)))) |
237 | 233, 236 | eqtr3d 2780 |
. . . . . . . . 9
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< )))) |
238 | 237 | ex 413 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
→ 𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))))) |
239 | 219, 238 | jcai 517 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
∧ 𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))))) |
240 | 239 | ancomd 462 |
. . . . . 6
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) |
241 | 139, 240 | jca 512 |
. . . . 5
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< )))) |
242 | | simprl 768 |
. . . . . . 7
⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) → 𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< )))) |
243 | 129 | adantr 481 |
. . . . . . 7
⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) → (𝑎 /
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ 𝐽) |
244 | 242, 243 | eqeltrd 2839 |
. . . . . 6
⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) → 𝑥 ∈
𝐽) |
245 | | simprr 770 |
. . . . . . 7
⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) → 𝑦 =
sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, <
)) |
246 | 53 | adantr 481 |
. . . . . . 7
⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) → sup({𝑘
∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈
ℕ0) |
247 | 245, 246 | eqeltrd 2839 |
. . . . . 6
⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) → 𝑦 ∈
ℕ0) |
248 | 117 | adantr 481 |
. . . . . . 7
⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) → 𝑎 =
((2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ·
(𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))))) |
249 | 245 | oveq2d 7285 |
. . . . . . . 8
⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) → (2↑𝑦)
= (2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, <
))) |
250 | 249, 242 | oveq12d 7287 |
. . . . . . 7
⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) → ((2↑𝑦)
· 𝑥) =
((2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ·
(𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))))) |
251 | 248, 250 | eqtr4d 2781 |
. . . . . 6
⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) → 𝑎 =
((2↑𝑦) · 𝑥)) |
252 | 244, 247,
251 | jca31 515 |
. . . . 5
⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) → ((𝑥 ∈
𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥))) |
253 | 241, 252 | impbii 208 |
. . . 4
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ↔ (𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< )))) |
254 | 253 | a1i 11 |
. . 3
⊢ (⊤
→ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ↔ (𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))))) |
255 | 1, 13, 131, 254 | f1od2 31043 |
. 2
⊢ (⊤
→ 𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ) |
256 | 255 | mptru 1546 |
1
⊢ 𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ |