Step | Hyp | Ref
| Expression |
1 | | oddpwdc.f |
. . 3
⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦
((2↑𝑦) · 𝑥)) |
2 | | 2nn 11185 |
. . . . . . . 8
⊢ 2 ∈
ℕ |
3 | 2 | a1i 11 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ0
∧ 𝑥 ∈ 𝐽) → 2 ∈
ℕ) |
4 | | simpl 473 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ0
∧ 𝑥 ∈ 𝐽) → 𝑦 ∈ ℕ0) |
5 | 3, 4 | nnexpcld 13030 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ0
∧ 𝑥 ∈ 𝐽) → (2↑𝑦) ∈
ℕ) |
6 | | oddpwdc.j |
. . . . . . . 8
⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} |
7 | | ssrab2 3687 |
. . . . . . . 8
⊢ {𝑧 ∈ ℕ ∣ ¬ 2
∥ 𝑧} ⊆
ℕ |
8 | 6, 7 | eqsstri 3635 |
. . . . . . 7
⊢ 𝐽 ⊆
ℕ |
9 | | simpr 477 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ0
∧ 𝑥 ∈ 𝐽) → 𝑥 ∈ 𝐽) |
10 | 8, 9 | sseldi 3601 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ0
∧ 𝑥 ∈ 𝐽) → 𝑥 ∈ ℕ) |
11 | 5, 10 | nnmulcld 11068 |
. . . . 5
⊢ ((𝑦 ∈ ℕ0
∧ 𝑥 ∈ 𝐽) → ((2↑𝑦) · 𝑥) ∈ ℕ) |
12 | 11 | ancoms 469 |
. . . 4
⊢ ((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) →
((2↑𝑦) · 𝑥) ∈
ℕ) |
13 | 12 | adantl 482 |
. . 3
⊢
((⊤ ∧ (𝑥
∈ 𝐽 ∧ 𝑦 ∈ ℕ0))
→ ((2↑𝑦) ·
𝑥) ∈
ℕ) |
14 | | id 22 |
. . . . . . 7
⊢ (𝑎 ∈ ℕ → 𝑎 ∈
ℕ) |
15 | 2 | a1i 11 |
. . . . . . . 8
⊢ (𝑎 ∈ ℕ → 2 ∈
ℕ) |
16 | | nn0ssre 11296 |
. . . . . . . . . . 11
⊢
ℕ0 ⊆ ℝ |
17 | | ltso 10118 |
. . . . . . . . . . 11
⊢ < Or
ℝ |
18 | | soss 5053 |
. . . . . . . . . . 11
⊢
(ℕ0 ⊆ ℝ → ( < Or ℝ →
< Or ℕ0)) |
19 | 16, 17, 18 | mp2 9 |
. . . . . . . . . 10
⊢ < Or
ℕ0 |
20 | 19 | a1i 11 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℕ → < Or
ℕ0) |
21 | | 0zd 11389 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ℕ → 0 ∈
ℤ) |
22 | | ssrab2 3687 |
. . . . . . . . . . 11
⊢ {𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎} ⊆
ℕ0 |
23 | 22 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ℕ → {𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎} ⊆
ℕ0) |
24 | | nnz 11399 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ ℕ → 𝑎 ∈
ℤ) |
25 | | oveq2 6658 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑛 → (2↑𝑘) = (2↑𝑛)) |
26 | 25 | breq1d 4663 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑛 → ((2↑𝑘) ∥ 𝑎 ↔ (2↑𝑛) ∥ 𝑎)) |
27 | 26 | elrab 3363 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎} ↔ (𝑛 ∈ ℕ0 ∧
(2↑𝑛) ∥ 𝑎)) |
28 | | simprl 794 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0
∧ (2↑𝑛) ∥
𝑎)) → 𝑛 ∈
ℕ0) |
29 | 28 | nn0red 11352 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0
∧ (2↑𝑛) ∥
𝑎)) → 𝑛 ∈
ℝ) |
30 | 2 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0
∧ (2↑𝑛) ∥
𝑎)) → 2 ∈
ℕ) |
31 | 30, 28 | nnexpcld 13030 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0
∧ (2↑𝑛) ∥
𝑎)) → (2↑𝑛) ∈
ℕ) |
32 | 31 | nnred 11035 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0
∧ (2↑𝑛) ∥
𝑎)) → (2↑𝑛) ∈
ℝ) |
33 | | simpl 473 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0
∧ (2↑𝑛) ∥
𝑎)) → 𝑎 ∈
ℕ) |
34 | 33 | nnred 11035 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0
∧ (2↑𝑛) ∥
𝑎)) → 𝑎 ∈
ℝ) |
35 | | 2re 11090 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℝ |
36 | 35 | leidi 10562 |
. . . . . . . . . . . . . . . 16
⊢ 2 ≤
2 |
37 | | nexple 30071 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈ ℕ0
∧ 2 ∈ ℝ ∧ 2 ≤ 2) → 𝑛 ≤ (2↑𝑛)) |
38 | 35, 36, 37 | mp3an23 1416 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ0
→ 𝑛 ≤ (2↑𝑛)) |
39 | 38 | ad2antrl 764 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0
∧ (2↑𝑛) ∥
𝑎)) → 𝑛 ≤ (2↑𝑛)) |
40 | 31 | nnzd 11481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0
∧ (2↑𝑛) ∥
𝑎)) → (2↑𝑛) ∈
ℤ) |
41 | | simprr 796 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0
∧ (2↑𝑛) ∥
𝑎)) → (2↑𝑛) ∥ 𝑎) |
42 | | dvdsle 15032 |
. . . . . . . . . . . . . . . 16
⊢
(((2↑𝑛) ∈
ℤ ∧ 𝑎 ∈
ℕ) → ((2↑𝑛)
∥ 𝑎 →
(2↑𝑛) ≤ 𝑎)) |
43 | 42 | imp 445 |
. . . . . . . . . . . . . . 15
⊢
((((2↑𝑛) ∈
ℤ ∧ 𝑎 ∈
ℕ) ∧ (2↑𝑛)
∥ 𝑎) →
(2↑𝑛) ≤ 𝑎) |
44 | 40, 33, 41, 43 | syl21anc 1325 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0
∧ (2↑𝑛) ∥
𝑎)) → (2↑𝑛) ≤ 𝑎) |
45 | 29, 32, 34, 39, 44 | letrd 10194 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0
∧ (2↑𝑛) ∥
𝑎)) → 𝑛 ≤ 𝑎) |
46 | 27, 45 | sylan2b 492 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}) → 𝑛 ≤ 𝑎) |
47 | 46 | ralrimiva 2966 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ ℕ →
∀𝑛 ∈ {𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}𝑛 ≤ 𝑎) |
48 | | breq2 4657 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑎 → (𝑛 ≤ 𝑚 ↔ 𝑛 ≤ 𝑎)) |
49 | 48 | ralbidv 2986 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑎 → (∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}𝑛 ≤ 𝑚 ↔ ∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}𝑛 ≤ 𝑎)) |
50 | 49 | rspcev 3309 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ ℤ ∧
∀𝑛 ∈ {𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}𝑛 ≤ 𝑎) → ∃𝑚 ∈ ℤ ∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}𝑛 ≤ 𝑚) |
51 | 24, 47, 50 | syl2anc 693 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ℕ →
∃𝑚 ∈ ℤ
∀𝑛 ∈ {𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}𝑛 ≤ 𝑚) |
52 | | nn0uz 11722 |
. . . . . . . . . . 11
⊢
ℕ0 = (ℤ≥‘0) |
53 | 52 | uzsupss 11780 |
. . . . . . . . . 10
⊢ ((0
∈ ℤ ∧ {𝑘
∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ⊆ ℕ0 ∧
∃𝑚 ∈ ℤ
∀𝑛 ∈ {𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}𝑛 ≤ 𝑚) → ∃𝑚 ∈ ℕ0 (∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎} ¬ 𝑚 < 𝑛 ∧ ∀𝑛 ∈ ℕ0 (𝑛 < 𝑚 → ∃𝑜 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}𝑛 < 𝑜))) |
54 | 21, 23, 51, 53 | syl3anc 1326 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℕ →
∃𝑚 ∈
ℕ0 (∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎} ¬ 𝑚 < 𝑛 ∧ ∀𝑛 ∈ ℕ0 (𝑛 < 𝑚 → ∃𝑜 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}𝑛 < 𝑜))) |
55 | 20, 54 | supcl 8364 |
. . . . . . . 8
⊢ (𝑎 ∈ ℕ →
sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈
ℕ0) |
56 | 15, 55 | nnexpcld 13030 |
. . . . . . 7
⊢ (𝑎 ∈ ℕ →
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∈
ℕ) |
57 | | fzfi 12771 |
. . . . . . . . . . . 12
⊢
(0...𝑎) ∈
Fin |
58 | | 0zd 11389 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}) → 0 ∈
ℤ) |
59 | 24 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}) → 𝑎 ∈ ℤ) |
60 | 27, 28 | sylan2b 492 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}) → 𝑛 ∈ ℕ0) |
61 | 60 | nn0zd 11480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}) → 𝑛 ∈ ℤ) |
62 | 60 | nn0ge0d 11354 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}) → 0 ≤ 𝑛) |
63 | | elfz4 12335 |
. . . . . . . . . . . . . . 15
⊢ (((0
∈ ℤ ∧ 𝑎
∈ ℤ ∧ 𝑛
∈ ℤ) ∧ (0 ≤ 𝑛 ∧ 𝑛 ≤ 𝑎)) → 𝑛 ∈ (0...𝑎)) |
64 | 58, 59, 61, 62, 46, 63 | syl32anc 1334 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}) → 𝑛 ∈ (0...𝑎)) |
65 | 64 | ex 450 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ ℕ → (𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎} → 𝑛 ∈ (0...𝑎))) |
66 | 65 | ssrdv 3609 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ ℕ → {𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎} ⊆ (0...𝑎)) |
67 | | ssfi 8180 |
. . . . . . . . . . . 12
⊢
(((0...𝑎) ∈ Fin
∧ {𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ⊆ (0...𝑎)) → {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎} ∈ Fin) |
68 | 57, 66, 67 | sylancr 695 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ ℕ → {𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎} ∈
Fin) |
69 | | 0nn0 11307 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℕ0 |
70 | 69 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ ℕ → 0 ∈
ℕ0) |
71 | | 2cn 11091 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℂ |
72 | | exp0 12864 |
. . . . . . . . . . . . . . 15
⊢ (2 ∈
ℂ → (2↑0) = 1) |
73 | 71, 72 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
(2↑0) = 1 |
74 | | 1dvds 14996 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ ℤ → 1 ∥
𝑎) |
75 | 24, 74 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ ℕ → 1 ∥
𝑎) |
76 | 73, 75 | syl5eqbr 4688 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ ℕ →
(2↑0) ∥ 𝑎) |
77 | | oveq2 6658 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 0 → (2↑𝑘) = (2↑0)) |
78 | 77 | breq1d 4663 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 0 → ((2↑𝑘) ∥ 𝑎 ↔ (2↑0) ∥ 𝑎)) |
79 | 78 | elrab 3363 |
. . . . . . . . . . . . 13
⊢ (0 ∈
{𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ↔ (0 ∈ ℕ0 ∧
(2↑0) ∥ 𝑎)) |
80 | 70, 76, 79 | sylanbrc 698 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ ℕ → 0 ∈
{𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}) |
81 | | ne0i 3921 |
. . . . . . . . . . . 12
⊢ (0 ∈
{𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎} → {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎} ≠ ∅) |
82 | 80, 81 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ ℕ → {𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎} ≠
∅) |
83 | | fisupcl 8375 |
. . . . . . . . . . 11
⊢ (( <
Or ℕ0 ∧ ({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎} ∈ Fin ∧ {𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎} ≠ ∅ ∧
{𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ⊆ ℕ0)) →
sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ {𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}) |
84 | 20, 68, 82, 23, 83 | syl13anc 1328 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ℕ →
sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ {𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}) |
85 | | oveq2 6658 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑙 → (2↑𝑘) = (2↑𝑙)) |
86 | 85 | breq1d 4663 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑙 → ((2↑𝑘) ∥ 𝑎 ↔ (2↑𝑙) ∥ 𝑎)) |
87 | 86 | cbvrabv 3199 |
. . . . . . . . . 10
⊢ {𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎} = {𝑙 ∈ ℕ0 ∣
(2↑𝑙) ∥ 𝑎} |
88 | 84, 87 | syl6eleq 2711 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℕ →
sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ {𝑙 ∈ ℕ0
∣ (2↑𝑙) ∥
𝑎}) |
89 | | oveq2 6658 |
. . . . . . . . . . 11
⊢ (𝑙 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
→ (2↑𝑙) =
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, <
))) |
90 | 89 | breq1d 4663 |
. . . . . . . . . 10
⊢ (𝑙 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
→ ((2↑𝑙) ∥
𝑎 ↔ (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< )) ∥ 𝑎)) |
91 | 90 | elrab 3363 |
. . . . . . . . 9
⊢
(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ {𝑙 ∈ ℕ0
∣ (2↑𝑙) ∥
𝑎} ↔ (sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ) ∈ ℕ0 ∧ (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
∥ 𝑎)) |
92 | 88, 91 | sylib 208 |
. . . . . . . 8
⊢ (𝑎 ∈ ℕ →
(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈
ℕ0 ∧ (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
∥ 𝑎)) |
93 | 92 | simprd 479 |
. . . . . . 7
⊢ (𝑎 ∈ ℕ →
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∥ 𝑎) |
94 | | nndivdvds 14989 |
. . . . . . . 8
⊢ ((𝑎 ∈ ℕ ∧
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∈
ℕ) → ((2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
∥ 𝑎 ↔ (𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) ∈ ℕ)) |
95 | 94 | biimpa 501 |
. . . . . . 7
⊢ (((𝑎 ∈ ℕ ∧
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∈
ℕ) ∧ (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
∥ 𝑎) → (𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) ∈ ℕ) |
96 | 14, 56, 93, 95 | syl21anc 1325 |
. . . . . 6
⊢ (𝑎 ∈ ℕ → (𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) ∈ ℕ) |
97 | | 1nn0 11308 |
. . . . . . . . . . 11
⊢ 1 ∈
ℕ0 |
98 | 97 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ℕ → 1 ∈
ℕ0) |
99 | 55, 98 | nn0addcld 11355 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℕ →
(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈
ℕ0) |
100 | 55 | nn0red 11352 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ ℕ →
sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈
ℝ) |
101 | 100 | ltp1d 10954 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ ℕ →
sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) <
(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) +
1)) |
102 | 20, 54 | supub 8365 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ ℕ →
((sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈
{𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎} → ¬ sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
< (sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) +
1))) |
103 | 101, 102 | mt2d 131 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ ℕ → ¬
(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈
{𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}) |
104 | 87 | eleq2i 2693 |
. . . . . . . . . . . 12
⊢
((sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈
{𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ↔ (sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ) +
1) ∈ {𝑙 ∈
ℕ0 ∣ (2↑𝑙) ∥ 𝑎}) |
105 | 103, 104 | sylnib 318 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ ℕ → ¬
(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈
{𝑙 ∈
ℕ0 ∣ (2↑𝑙) ∥ 𝑎}) |
106 | | oveq2 6658 |
. . . . . . . . . . . . 13
⊢ (𝑙 = (sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ) +
1) → (2↑𝑙) =
(2↑(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) +
1))) |
107 | 106 | breq1d 4663 |
. . . . . . . . . . . 12
⊢ (𝑙 = (sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ) +
1) → ((2↑𝑙)
∥ 𝑎 ↔
(2↑(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) ∥
𝑎)) |
108 | 107 | elrab 3363 |
. . . . . . . . . . 11
⊢
((sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈
{𝑙 ∈
ℕ0 ∣ (2↑𝑙) ∥ 𝑎} ↔ ((sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ) +
1) ∈ ℕ0 ∧ (2↑(sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ) +
1)) ∥ 𝑎)) |
109 | 105, 108 | sylnib 318 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ℕ → ¬
((sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈
ℕ0 ∧ (2↑(sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ) +
1)) ∥ 𝑎)) |
110 | | imnan 438 |
. . . . . . . . . 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)) ∥ 𝑎)) |
111 | 109, 110 | sylibr 224 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℕ →
((sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈
ℕ0 → ¬ (2↑(sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ) +
1)) ∥ 𝑎)) |
112 | 99, 111 | mpd 15 |
. . . . . . . 8
⊢ (𝑎 ∈ ℕ → ¬
(2↑(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) ∥
𝑎) |
113 | | expp1 12867 |
. . . . . . . . . 10
⊢ ((2
∈ ℂ ∧ sup({𝑘
∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈
ℕ0) → (2↑(sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ) +
1)) = ((2↑sup({𝑘
∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ·
2)) |
114 | 71, 55, 113 | sylancr 695 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℕ →
(2↑(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) =
((2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ·
2)) |
115 | 114 | breq1d 4663 |
. . . . . . . 8
⊢ (𝑎 ∈ ℕ →
((2↑(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) ∥
𝑎 ↔
((2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2)
∥ 𝑎)) |
116 | 112, 115 | mtbid 314 |
. . . . . . 7
⊢ (𝑎 ∈ ℕ → ¬
((2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2)
∥ 𝑎) |
117 | | nncn 11028 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ ℕ → 𝑎 ∈
ℂ) |
118 | 56 | nncnd 11036 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ ℕ →
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∈
ℂ) |
119 | 56 | nnne0d 11065 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ ℕ →
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ≠
0) |
120 | 117, 118,
119 | divcan2d 10803 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ℕ →
((2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ·
(𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< )))) = 𝑎) |
121 | 120 | eqcomd 2628 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℕ → 𝑎 = ((2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< )) · (𝑎 /
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, <
))))) |
122 | 121 | breq2d 4665 |
. . . . . . . 8
⊢ (𝑎 ∈ ℕ →
(((2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2)
∥ 𝑎 ↔
((2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2)
∥ ((2↑sup({𝑘
∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ·
(𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< )))))) |
123 | 15 | nnzd 11481 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℕ → 2 ∈
ℤ) |
124 | 96 | nnzd 11481 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℕ → (𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) ∈ ℤ) |
125 | 56 | nnzd 11481 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℕ →
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∈
ℤ) |
126 | | dvdscmulr 15010 |
. . . . . . . . 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, <
))))) |
127 | 123, 124,
125, 119, 126 | syl112anc 1330 |
. . . . . . . 8
⊢ (𝑎 ∈ ℕ →
(((2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2)
∥ ((2↑sup({𝑘
∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ·
(𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< )))) ↔ 2 ∥ (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, <
))))) |
128 | 122, 127 | bitrd 268 |
. . . . . . 7
⊢ (𝑎 ∈ ℕ →
(((2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2)
∥ 𝑎 ↔ 2 ∥
(𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))))) |
129 | 116, 128 | mtbid 314 |
. . . . . 6
⊢ (𝑎 ∈ ℕ → ¬ 2
∥ (𝑎 /
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, <
)))) |
130 | | breq2 4657 |
. . . . . . . 8
⊢ (𝑧 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
→ (2 ∥ 𝑧 ↔
2 ∥ (𝑎 /
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, <
))))) |
131 | 130 | notbid 308 |
. . . . . . 7
⊢ (𝑧 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
→ (¬ 2 ∥ 𝑧
↔ ¬ 2 ∥ (𝑎 /
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, <
))))) |
132 | 131, 6 | elrab2 3366 |
. . . . . 6
⊢ ((𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) ∈ 𝐽 ↔
((𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) ∈ ℕ ∧ ¬ 2 ∥ (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, <
))))) |
133 | 96, 129, 132 | sylanbrc 698 |
. . . . 5
⊢ (𝑎 ∈ ℕ → (𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) ∈ 𝐽) |
134 | 133, 55 | jca 554 |
. . . 4
⊢ (𝑎 ∈ ℕ → ((𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) ∈ 𝐽 ∧
sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈
ℕ0)) |
135 | 134 | adantl 482 |
. . 3
⊢
((⊤ ∧ 𝑎
∈ ℕ) → ((𝑎
/ (2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ 𝐽 ∧ sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
∈ ℕ0)) |
136 | | simpr 477 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑎 = ((2↑𝑦) · 𝑥)) |
137 | 2 | a1i 11 |
. . . . . . . . 9
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 2 ∈ ℕ) |
138 | | simplr 792 |
. . . . . . . . 9
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑦 ∈ ℕ0) |
139 | 137, 138 | nnexpcld 13030 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (2↑𝑦) ∈ ℕ) |
140 | 8 | sseli 3599 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐽 → 𝑥 ∈ ℕ) |
141 | 140 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑥 ∈ ℕ) |
142 | 139, 141 | nnmulcld 11068 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → ((2↑𝑦) · 𝑥) ∈ ℕ) |
143 | 136, 142 | eqeltrd 2701 |
. . . . . 6
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑎 ∈ ℕ) |
144 | | simplll 798 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑥 ∈ 𝐽) |
145 | | breq2 4657 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑥 → (2 ∥ 𝑧 ↔ 2 ∥ 𝑥)) |
146 | 145 | notbid 308 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑥 → (¬ 2 ∥ 𝑧 ↔ ¬ 2 ∥ 𝑥)) |
147 | 146, 6 | elrab2 3366 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐽 ↔ (𝑥 ∈ ℕ ∧ ¬ 2 ∥ 𝑥)) |
148 | 147 | simprbi 480 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐽 → ¬ 2 ∥ 𝑥) |
149 | | 2z 11409 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℤ |
150 | 138 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑦 ∈
ℕ0) |
151 | 150 | nn0zd 11480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑦 ∈
ℤ) |
152 | 19 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ < Or ℕ0) |
153 | 143, 54 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → ∃𝑚 ∈ ℕ0 (∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎} ¬ 𝑚 < 𝑛 ∧ ∀𝑛 ∈ ℕ0 (𝑛 < 𝑚 → ∃𝑜 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}𝑛 < 𝑜))) |
154 | 153 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ ∃𝑚 ∈
ℕ0 (∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎} ¬ 𝑚 < 𝑛 ∧ ∀𝑛 ∈ ℕ0 (𝑛 < 𝑚 → ∃𝑜 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}𝑛 < 𝑜))) |
155 | 152, 154 | supcl 8364 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈
ℕ0) |
156 | 155 | nn0zd 11480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈
ℤ) |
157 | | simpr 477 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑦 < sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< )) |
158 | | znnsub 11423 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℤ ∧ sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ) ∈ ℤ) → (𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
↔ (sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦) ∈
ℕ)) |
159 | 158 | biimpa 501 |
. . . . . . . . . . . . . . 15
⊢ (((𝑦 ∈ ℤ ∧ sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ) ∈ ℤ) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦) ∈
ℕ) |
160 | 151, 156,
157, 159 | syl21anc 1325 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦) ∈
ℕ) |
161 | | iddvdsexp 15005 |
. . . . . . . . . . . . . 14
⊢ ((2
∈ ℤ ∧ (sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
− 𝑦) ∈ ℕ)
→ 2 ∥ (2↑(sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
− 𝑦))) |
162 | 149, 160,
161 | sylancr 695 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 2 ∥ (2↑(sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
− 𝑦))) |
163 | 149 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 2 ∈ ℤ) |
164 | 143, 124 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∈ ℤ) |
165 | 164 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (𝑎 /
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈
ℤ) |
166 | 160 | nnnn0d 11351 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦) ∈
ℕ0) |
167 | | zexpcl 12875 |
. . . . . . . . . . . . . . 15
⊢ ((2
∈ ℤ ∧ (sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
− 𝑦) ∈
ℕ0) → (2↑(sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
− 𝑦)) ∈
ℤ) |
168 | 149, 166,
167 | sylancr 695 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (2↑(sup({𝑘
∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) ∈
ℤ) |
169 | | dvdsmultr2 15021 |
. . . . . . . . . . . . . 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, < ) − 𝑦))))) |
170 | 163, 165,
168, 169 | syl3anc 1326 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (2 ∥ (2↑(sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
− 𝑦)) → 2
∥ ((𝑎 /
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ·
(2↑(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦))))) |
171 | 162, 170 | mpd 15 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 2 ∥ ((𝑎 /
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ·
(2↑(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)))) |
172 | 141 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑥 ∈
ℕ) |
173 | 172 | nncnd 11036 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑥 ∈
ℂ) |
174 | | 2cnd 11093 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 2 ∈ ℂ) |
175 | 174, 166 | expcld 13008 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (2↑(sup({𝑘
∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) ∈
ℂ) |
176 | 143 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑎 ∈
ℕ) |
177 | 176 | nncnd 11036 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑎 ∈
ℂ) |
178 | 176, 118 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (2↑sup({𝑘
∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∈
ℂ) |
179 | | 2ne0 11113 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ≠
0 |
180 | 179 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 2 ≠ 0) |
181 | 174, 180,
156 | expne0d 13014 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (2↑sup({𝑘
∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ≠
0) |
182 | 177, 178,
181 | divcld 10801 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (𝑎 /
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈
ℂ) |
183 | 175, 182 | mulcld 10060 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ ((2↑(sup({𝑘
∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, <
)))) ∈ ℂ) |
184 | 174, 150 | expcld 13008 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (2↑𝑦) ∈
ℂ) |
185 | 174, 180,
151 | expne0d 13014 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (2↑𝑦) ≠
0) |
186 | 176, 121 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑎 =
((2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ·
(𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))))) |
187 | | simplr 792 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑎 = ((2↑𝑦) · 𝑥)) |
188 | 150 | nn0cnd 11353 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑦 ∈
ℂ) |
189 | 155 | nn0cnd 11353 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈
ℂ) |
190 | 188, 189 | pncan3d 10395 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (𝑦 + (sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ) − 𝑦)) =
sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, <
)) |
191 | 190 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (2↑(𝑦 +
(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦))) = (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) |
192 | 174, 166,
150 | expaddd 13010 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (2↑(𝑦 +
(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦))) = ((2↑𝑦) · (2↑(sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ) − 𝑦)))) |
193 | 191, 192 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (2↑sup({𝑘
∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) =
((2↑𝑦) ·
(2↑(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)))) |
194 | 193 | oveq1d 6665 |
. . . . . . . . . . . . . . . 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, <
))))) |
195 | 186, 187,
194 | 3eqtr3d 2664 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ ((2↑𝑦) ·
𝑥) = (((2↑𝑦) · (2↑(sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ) − 𝑦)))
· (𝑎 /
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, <
))))) |
196 | 184, 175,
182 | mulassd 10063 |
. . . . . . . . . . . . . . 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, <
)))))) |
197 | 195, 196 | eqtrd 2656 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ ((2↑𝑦) ·
𝑥) = ((2↑𝑦) · ((2↑(sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ) − 𝑦)) ·
(𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< )))))) |
198 | 173, 183,
184, 185, 197 | mulcanad 10662 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑥 =
((2↑(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, <
))))) |
199 | 182, 175 | mulcomd 10061 |
. . . . . . . . . . . . 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,
< ))))) |
200 | 198, 199 | eqtr4d 2659 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑥 = ((𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) · (2↑(sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
− 𝑦)))) |
201 | 171, 200 | breqtrrd 4681 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 2 ∥ 𝑥) |
202 | 148, 201 | nsyl3 133 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ ¬ 𝑥 ∈ 𝐽) |
203 | 144, 202 | pm2.65da 600 |
. . . . . . . . 9
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → ¬ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, <
)) |
204 | 141 | nnzd 11481 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑥 ∈ ℤ) |
205 | 139 | nnzd 11481 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (2↑𝑦) ∈ ℤ) |
206 | 143 | nnzd 11481 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑎 ∈ ℤ) |
207 | 139 | nncnd 11036 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (2↑𝑦) ∈ ℂ) |
208 | 141 | nncnd 11036 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑥 ∈ ℂ) |
209 | 207, 208 | mulcomd 10061 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → ((2↑𝑦) · 𝑥) = (𝑥 · (2↑𝑦))) |
210 | 136, 209 | eqtr2d 2657 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑥 · (2↑𝑦)) = 𝑎) |
211 | | dvds0lem 14992 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℤ ∧
(2↑𝑦) ∈ ℤ
∧ 𝑎 ∈ ℤ)
∧ (𝑥 ·
(2↑𝑦)) = 𝑎) → (2↑𝑦) ∥ 𝑎) |
212 | 204, 205,
206, 210, 211 | syl31anc 1329 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (2↑𝑦) ∥ 𝑎) |
213 | | oveq2 6658 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑦 → (2↑𝑘) = (2↑𝑦)) |
214 | 213 | breq1d 4663 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑦 → ((2↑𝑘) ∥ 𝑎 ↔ (2↑𝑦) ∥ 𝑎)) |
215 | 214 | elrab 3363 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎} ↔ (𝑦 ∈ ℕ0 ∧
(2↑𝑦) ∥ 𝑎)) |
216 | 138, 212,
215 | sylanbrc 698 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑦 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}) |
217 | 19 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → < Or
ℕ0) |
218 | 217, 153 | supub 8365 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑦 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎} → ¬ sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ) < 𝑦)) |
219 | 216, 218 | mpd 15 |
. . . . . . . . 9
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → ¬ sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
< 𝑦) |
220 | 138 | nn0red 11352 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑦 ∈ ℝ) |
221 | 143, 100 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
∈ ℝ) |
222 | 220, 221 | lttri3d 10177 |
. . . . . . . . 9
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
↔ (¬ 𝑦 <
sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∧ ¬
sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) < 𝑦))) |
223 | 203, 219,
222 | mpbir2and 957 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, <
)) |
224 | | simplr 792 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑎 = ((2↑𝑦) · 𝑥)) |
225 | 143 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑎 ∈
ℕ) |
226 | 225 | nncnd 11036 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑎 ∈
ℂ) |
227 | 141 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑥 ∈
ℕ) |
228 | 227 | nncnd 11036 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑥 ∈
ℂ) |
229 | | nnexpcl 12873 |
. . . . . . . . . . . . . . . 16
⊢ ((2
∈ ℕ ∧ 𝑦
∈ ℕ0) → (2↑𝑦) ∈ ℕ) |
230 | 2, 229 | mpan 706 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℕ0
→ (2↑𝑦) ∈
ℕ) |
231 | 230 | nncnd 11036 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ0
→ (2↑𝑦) ∈
ℂ) |
232 | 230 | nnne0d 11065 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ0
→ (2↑𝑦) ≠
0) |
233 | 231, 232 | jca 554 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ0
→ ((2↑𝑦) ∈
ℂ ∧ (2↑𝑦)
≠ 0)) |
234 | 233 | ad3antlr 767 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ ((2↑𝑦) ∈
ℂ ∧ (2↑𝑦)
≠ 0)) |
235 | | divmul2 10689 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧
((2↑𝑦) ∈ ℂ
∧ (2↑𝑦) ≠ 0))
→ ((𝑎 / (2↑𝑦)) = 𝑥 ↔ 𝑎 = ((2↑𝑦) · 𝑥))) |
236 | 226, 228,
234, 235 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ ((𝑎 / (2↑𝑦)) = 𝑥 ↔ 𝑎 = ((2↑𝑦) · 𝑥))) |
237 | 224, 236 | mpbird 247 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (𝑎 / (2↑𝑦)) = 𝑥) |
238 | | simpr 477 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< )) |
239 | 238 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (2↑𝑦) =
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, <
))) |
240 | 239 | oveq2d 6666 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (𝑎 / (2↑𝑦)) = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, <
)))) |
241 | 237, 240 | eqtr3d 2658 |
. . . . . . . . 9
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< )))) |
242 | 241 | ex 450 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
→ 𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))))) |
243 | 223, 242 | jcai 559 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
∧ 𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))))) |
244 | 243 | ancomd 467 |
. . . . . 6
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) |
245 | 143, 244 | jca 554 |
. . . . 5
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< )))) |
246 | | simprl 794 |
. . . . . . 7
⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) → 𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< )))) |
247 | 133 | adantr 481 |
. . . . . . 7
⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) → (𝑎 /
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ 𝐽) |
248 | 246, 247 | eqeltrd 2701 |
. . . . . 6
⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) → 𝑥 ∈
𝐽) |
249 | | simprr 796 |
. . . . . . 7
⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) → 𝑦 =
sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, <
)) |
250 | 55 | adantr 481 |
. . . . . . 7
⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) → sup({𝑘
∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈
ℕ0) |
251 | 249, 250 | eqeltrd 2701 |
. . . . . 6
⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) → 𝑦 ∈
ℕ0) |
252 | 121 | adantr 481 |
. . . . . . 7
⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) → 𝑎 =
((2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ·
(𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))))) |
253 | 249 | oveq2d 6666 |
. . . . . . . 8
⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) → (2↑𝑦)
= (2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, <
))) |
254 | 253, 246 | oveq12d 6668 |
. . . . . . 7
⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) → ((2↑𝑦)
· 𝑥) =
((2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ·
(𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))))) |
255 | 252, 254 | eqtr4d 2659 |
. . . . . 6
⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) → 𝑎 =
((2↑𝑦) · 𝑥)) |
256 | 248, 251,
255 | jca31 557 |
. . . . 5
⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) → ((𝑥 ∈
𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥))) |
257 | 245, 256 | impbii 199 |
. . . 4
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ↔ (𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< )))) |
258 | 257 | a1i 11 |
. . 3
⊢ (⊤
→ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ↔ (𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))))) |
259 | 1, 13, 135, 258 | f1od2 29499 |
. 2
⊢ (⊤
→ 𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ) |
260 | 259 | trud 1493 |
1
⊢ 𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ |