Step | Hyp | Ref
| Expression |
1 | | oddpwdc.f |
. . 3
⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦
((2↑𝑦) · 𝑥)) |
2 | | 2nn 11448 |
. . . . . . . 8
⊢ 2 ∈
ℕ |
3 | 2 | a1i 11 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ0
∧ 𝑥 ∈ 𝐽) → 2 ∈
ℕ) |
4 | | simpl 476 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ0
∧ 𝑥 ∈ 𝐽) → 𝑦 ∈ ℕ0) |
5 | 3, 4 | nnexpcld 13351 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ0
∧ 𝑥 ∈ 𝐽) → (2↑𝑦) ∈
ℕ) |
6 | | oddpwdc.j |
. . . . . . . 8
⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} |
7 | | ssrab2 3908 |
. . . . . . . 8
⊢ {𝑧 ∈ ℕ ∣ ¬ 2
∥ 𝑧} ⊆
ℕ |
8 | 6, 7 | eqsstri 3854 |
. . . . . . 7
⊢ 𝐽 ⊆
ℕ |
9 | | simpr 479 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ0
∧ 𝑥 ∈ 𝐽) → 𝑥 ∈ 𝐽) |
10 | 8, 9 | sseldi 3819 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ0
∧ 𝑥 ∈ 𝐽) → 𝑥 ∈ ℕ) |
11 | 5, 10 | nnmulcld 11428 |
. . . . 5
⊢ ((𝑦 ∈ ℕ0
∧ 𝑥 ∈ 𝐽) → ((2↑𝑦) · 𝑥) ∈ ℕ) |
12 | 11 | ancoms 452 |
. . . 4
⊢ ((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) →
((2↑𝑦) · 𝑥) ∈
ℕ) |
13 | 12 | adantl 475 |
. . 3
⊢
((⊤ ∧ (𝑥
∈ 𝐽 ∧ 𝑦 ∈ ℕ0))
→ ((2↑𝑦) ·
𝑥) ∈
ℕ) |
14 | | id 22 |
. . . . . . 7
⊢ (𝑎 ∈ ℕ → 𝑎 ∈
ℕ) |
15 | 2 | a1i 11 |
. . . . . . . 8
⊢ (𝑎 ∈ ℕ → 2 ∈
ℕ) |
16 | | nn0ssre 11646 |
. . . . . . . . . . 11
⊢
ℕ0 ⊆ ℝ |
17 | | ltso 10457 |
. . . . . . . . . . 11
⊢ < Or
ℝ |
18 | | soss 5293 |
. . . . . . . . . . 11
⊢
(ℕ0 ⊆ ℝ → ( < Or ℝ →
< Or ℕ0)) |
19 | 16, 17, 18 | mp2 9 |
. . . . . . . . . 10
⊢ < Or
ℕ0 |
20 | 19 | a1i 11 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℕ → < Or
ℕ0) |
21 | | 0zd 11740 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ℕ → 0 ∈
ℤ) |
22 | | ssrab2 3908 |
. . . . . . . . . . 11
⊢ {𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎} ⊆
ℕ0 |
23 | 22 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ℕ → {𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎} ⊆
ℕ0) |
24 | | nnz 11751 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ ℕ → 𝑎 ∈
ℤ) |
25 | | oveq2 6930 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑛 → (2↑𝑘) = (2↑𝑛)) |
26 | 25 | breq1d 4896 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑛 → ((2↑𝑘) ∥ 𝑎 ↔ (2↑𝑛) ∥ 𝑎)) |
27 | 26 | elrab 3572 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎} ↔ (𝑛 ∈ ℕ0 ∧
(2↑𝑛) ∥ 𝑎)) |
28 | | simprl 761 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0
∧ (2↑𝑛) ∥
𝑎)) → 𝑛 ∈
ℕ0) |
29 | 28 | nn0red 11703 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0
∧ (2↑𝑛) ∥
𝑎)) → 𝑛 ∈
ℝ) |
30 | 2 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0
∧ (2↑𝑛) ∥
𝑎)) → 2 ∈
ℕ) |
31 | 30, 28 | nnexpcld 13351 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0
∧ (2↑𝑛) ∥
𝑎)) → (2↑𝑛) ∈
ℕ) |
32 | 31 | nnred 11391 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0
∧ (2↑𝑛) ∥
𝑎)) → (2↑𝑛) ∈
ℝ) |
33 | | simpl 476 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0
∧ (2↑𝑛) ∥
𝑎)) → 𝑎 ∈
ℕ) |
34 | 33 | nnred 11391 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0
∧ (2↑𝑛) ∥
𝑎)) → 𝑎 ∈
ℝ) |
35 | | 2re 11449 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℝ |
36 | 35 | leidi 10909 |
. . . . . . . . . . . . . . . 16
⊢ 2 ≤
2 |
37 | | nexple 30669 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈ ℕ0
∧ 2 ∈ ℝ ∧ 2 ≤ 2) → 𝑛 ≤ (2↑𝑛)) |
38 | 35, 36, 37 | mp3an23 1526 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ0
→ 𝑛 ≤ (2↑𝑛)) |
39 | 38 | ad2antrl 718 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0
∧ (2↑𝑛) ∥
𝑎)) → 𝑛 ≤ (2↑𝑛)) |
40 | 31 | nnzd 11833 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0
∧ (2↑𝑛) ∥
𝑎)) → (2↑𝑛) ∈
ℤ) |
41 | | simprr 763 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0
∧ (2↑𝑛) ∥
𝑎)) → (2↑𝑛) ∥ 𝑎) |
42 | | dvdsle 15439 |
. . . . . . . . . . . . . . . 16
⊢
(((2↑𝑛) ∈
ℤ ∧ 𝑎 ∈
ℕ) → ((2↑𝑛)
∥ 𝑎 →
(2↑𝑛) ≤ 𝑎)) |
43 | 42 | imp 397 |
. . . . . . . . . . . . . . 15
⊢
((((2↑𝑛) ∈
ℤ ∧ 𝑎 ∈
ℕ) ∧ (2↑𝑛)
∥ 𝑎) →
(2↑𝑛) ≤ 𝑎) |
44 | 40, 33, 41, 43 | syl21anc 828 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0
∧ (2↑𝑛) ∥
𝑎)) → (2↑𝑛) ≤ 𝑎) |
45 | 29, 32, 34, 39, 44 | letrd 10533 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0
∧ (2↑𝑛) ∥
𝑎)) → 𝑛 ≤ 𝑎) |
46 | 27, 45 | sylan2b 587 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}) → 𝑛 ≤ 𝑎) |
47 | 46 | ralrimiva 3148 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ ℕ →
∀𝑛 ∈ {𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}𝑛 ≤ 𝑎) |
48 | | brralrspcev 4946 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ ℤ ∧
∀𝑛 ∈ {𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}𝑛 ≤ 𝑎) → ∃𝑚 ∈ ℤ ∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}𝑛 ≤ 𝑚) |
49 | 24, 47, 48 | syl2anc 579 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ℕ →
∃𝑚 ∈ ℤ
∀𝑛 ∈ {𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}𝑛 ≤ 𝑚) |
50 | | nn0uz 12028 |
. . . . . . . . . . 11
⊢
ℕ0 = (ℤ≥‘0) |
51 | 50 | uzsupss 12087 |
. . . . . . . . . 10
⊢ ((0
∈ ℤ ∧ {𝑘
∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ⊆ ℕ0 ∧
∃𝑚 ∈ ℤ
∀𝑛 ∈ {𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}𝑛 ≤ 𝑚) → ∃𝑚 ∈ ℕ0 (∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎} ¬ 𝑚 < 𝑛 ∧ ∀𝑛 ∈ ℕ0 (𝑛 < 𝑚 → ∃𝑜 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}𝑛 < 𝑜))) |
52 | 21, 23, 49, 51 | syl3anc 1439 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℕ →
∃𝑚 ∈
ℕ0 (∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎} ¬ 𝑚 < 𝑛 ∧ ∀𝑛 ∈ ℕ0 (𝑛 < 𝑚 → ∃𝑜 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}𝑛 < 𝑜))) |
53 | 20, 52 | supcl 8652 |
. . . . . . . 8
⊢ (𝑎 ∈ ℕ →
sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈
ℕ0) |
54 | 15, 53 | nnexpcld 13351 |
. . . . . . 7
⊢ (𝑎 ∈ ℕ →
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∈
ℕ) |
55 | | fzfi 13090 |
. . . . . . . . . . . 12
⊢
(0...𝑎) ∈
Fin |
56 | | 0zd 11740 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}) → 0 ∈
ℤ) |
57 | 24 | adantr 474 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}) → 𝑎 ∈ ℤ) |
58 | 27, 28 | sylan2b 587 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}) → 𝑛 ∈ ℕ0) |
59 | 58 | nn0zd 11832 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}) → 𝑛 ∈ ℤ) |
60 | 58 | nn0ge0d 11705 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}) → 0 ≤ 𝑛) |
61 | | elfz4 12652 |
. . . . . . . . . . . . . . 15
⊢ (((0
∈ ℤ ∧ 𝑎
∈ ℤ ∧ 𝑛
∈ ℤ) ∧ (0 ≤ 𝑛 ∧ 𝑛 ≤ 𝑎)) → 𝑛 ∈ (0...𝑎)) |
62 | 56, 57, 59, 60, 46, 61 | syl32anc 1446 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}) → 𝑛 ∈ (0...𝑎)) |
63 | 62 | ex 403 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ ℕ → (𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎} → 𝑛 ∈ (0...𝑎))) |
64 | 63 | ssrdv 3827 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ ℕ → {𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎} ⊆ (0...𝑎)) |
65 | | ssfi 8468 |
. . . . . . . . . . . 12
⊢
(((0...𝑎) ∈ Fin
∧ {𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ⊆ (0...𝑎)) → {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎} ∈ Fin) |
66 | 55, 64, 65 | sylancr 581 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ ℕ → {𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎} ∈
Fin) |
67 | | 0nn0 11659 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℕ0 |
68 | 67 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ ℕ → 0 ∈
ℕ0) |
69 | | 2cn 11450 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℂ |
70 | | exp0 13182 |
. . . . . . . . . . . . . . 15
⊢ (2 ∈
ℂ → (2↑0) = 1) |
71 | 69, 70 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
(2↑0) = 1 |
72 | | 1dvds 15403 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ ℤ → 1 ∥
𝑎) |
73 | 24, 72 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ ℕ → 1 ∥
𝑎) |
74 | 71, 73 | syl5eqbr 4921 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ ℕ →
(2↑0) ∥ 𝑎) |
75 | | oveq2 6930 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 0 → (2↑𝑘) = (2↑0)) |
76 | 75 | breq1d 4896 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 0 → ((2↑𝑘) ∥ 𝑎 ↔ (2↑0) ∥ 𝑎)) |
77 | 76 | elrab 3572 |
. . . . . . . . . . . . 13
⊢ (0 ∈
{𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ↔ (0 ∈ ℕ0 ∧
(2↑0) ∥ 𝑎)) |
78 | 68, 74, 77 | sylanbrc 578 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ ℕ → 0 ∈
{𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}) |
79 | 78 | ne0d 4150 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ ℕ → {𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎} ≠
∅) |
80 | | fisupcl 8663 |
. . . . . . . . . . 11
⊢ (( <
Or ℕ0 ∧ ({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎} ∈ Fin ∧ {𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎} ≠ ∅ ∧
{𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ⊆ ℕ0)) →
sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ {𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}) |
81 | 20, 66, 79, 23, 80 | syl13anc 1440 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ℕ →
sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ {𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}) |
82 | | oveq2 6930 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑙 → (2↑𝑘) = (2↑𝑙)) |
83 | 82 | breq1d 4896 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑙 → ((2↑𝑘) ∥ 𝑎 ↔ (2↑𝑙) ∥ 𝑎)) |
84 | 83 | cbvrabv 3396 |
. . . . . . . . . 10
⊢ {𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎} = {𝑙 ∈ ℕ0 ∣
(2↑𝑙) ∥ 𝑎} |
85 | 81, 84 | syl6eleq 2869 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℕ →
sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ {𝑙 ∈ ℕ0
∣ (2↑𝑙) ∥
𝑎}) |
86 | | oveq2 6930 |
. . . . . . . . . . 11
⊢ (𝑙 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
→ (2↑𝑙) =
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, <
))) |
87 | 86 | breq1d 4896 |
. . . . . . . . . 10
⊢ (𝑙 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
→ ((2↑𝑙) ∥
𝑎 ↔ (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< )) ∥ 𝑎)) |
88 | 87 | elrab 3572 |
. . . . . . . . 9
⊢
(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ {𝑙 ∈ ℕ0
∣ (2↑𝑙) ∥
𝑎} ↔ (sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ) ∈ ℕ0 ∧ (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
∥ 𝑎)) |
89 | 85, 88 | sylib 210 |
. . . . . . . 8
⊢ (𝑎 ∈ ℕ →
(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈
ℕ0 ∧ (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
∥ 𝑎)) |
90 | 89 | simprd 491 |
. . . . . . 7
⊢ (𝑎 ∈ ℕ →
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∥ 𝑎) |
91 | | nndivdvds 15396 |
. . . . . . . 8
⊢ ((𝑎 ∈ ℕ ∧
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∈
ℕ) → ((2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
∥ 𝑎 ↔ (𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) ∈ ℕ)) |
92 | 91 | biimpa 470 |
. . . . . . 7
⊢ (((𝑎 ∈ ℕ ∧
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∈
ℕ) ∧ (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
∥ 𝑎) → (𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) ∈ ℕ) |
93 | 14, 54, 90, 92 | syl21anc 828 |
. . . . . 6
⊢ (𝑎 ∈ ℕ → (𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) ∈ ℕ) |
94 | | 1nn0 11660 |
. . . . . . . . . . 11
⊢ 1 ∈
ℕ0 |
95 | 94 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ℕ → 1 ∈
ℕ0) |
96 | 53, 95 | nn0addcld 11706 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℕ →
(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈
ℕ0) |
97 | 53 | nn0red 11703 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ ℕ →
sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈
ℝ) |
98 | 97 | ltp1d 11308 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ ℕ →
sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) <
(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) +
1)) |
99 | 20, 52 | supub 8653 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ ℕ →
((sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈
{𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎} → ¬ sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
< (sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) +
1))) |
100 | 98, 99 | mt2d 134 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ ℕ → ¬
(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈
{𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}) |
101 | 84 | eleq2i 2851 |
. . . . . . . . . . . 12
⊢
((sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈
{𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ↔ (sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ) +
1) ∈ {𝑙 ∈
ℕ0 ∣ (2↑𝑙) ∥ 𝑎}) |
102 | 100, 101 | sylnib 320 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ ℕ → ¬
(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈
{𝑙 ∈
ℕ0 ∣ (2↑𝑙) ∥ 𝑎}) |
103 | | oveq2 6930 |
. . . . . . . . . . . . 13
⊢ (𝑙 = (sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ) +
1) → (2↑𝑙) =
(2↑(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) +
1))) |
104 | 103 | breq1d 4896 |
. . . . . . . . . . . 12
⊢ (𝑙 = (sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ) +
1) → ((2↑𝑙)
∥ 𝑎 ↔
(2↑(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) ∥
𝑎)) |
105 | 104 | elrab 3572 |
. . . . . . . . . . 11
⊢
((sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈
{𝑙 ∈
ℕ0 ∣ (2↑𝑙) ∥ 𝑎} ↔ ((sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ) +
1) ∈ ℕ0 ∧ (2↑(sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ) +
1)) ∥ 𝑎)) |
106 | 102, 105 | sylnib 320 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ℕ → ¬
((sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈
ℕ0 ∧ (2↑(sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ) +
1)) ∥ 𝑎)) |
107 | | imnan 390 |
. . . . . . . . . 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)) ∥ 𝑎)) |
108 | 106, 107 | sylibr 226 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℕ →
((sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈
ℕ0 → ¬ (2↑(sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ) +
1)) ∥ 𝑎)) |
109 | 96, 108 | mpd 15 |
. . . . . . . 8
⊢ (𝑎 ∈ ℕ → ¬
(2↑(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) ∥
𝑎) |
110 | | expp1 13185 |
. . . . . . . . . 10
⊢ ((2
∈ ℂ ∧ sup({𝑘
∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈
ℕ0) → (2↑(sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ) +
1)) = ((2↑sup({𝑘
∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ·
2)) |
111 | 69, 53, 110 | sylancr 581 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℕ →
(2↑(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) =
((2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ·
2)) |
112 | 111 | breq1d 4896 |
. . . . . . . 8
⊢ (𝑎 ∈ ℕ →
((2↑(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) ∥
𝑎 ↔
((2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2)
∥ 𝑎)) |
113 | 109, 112 | mtbid 316 |
. . . . . . 7
⊢ (𝑎 ∈ ℕ → ¬
((2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2)
∥ 𝑎) |
114 | | nncn 11383 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ ℕ → 𝑎 ∈
ℂ) |
115 | 54 | nncnd 11392 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ ℕ →
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∈
ℂ) |
116 | 54 | nnne0d 11425 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ ℕ →
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ≠
0) |
117 | 114, 115,
116 | divcan2d 11153 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ℕ →
((2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ·
(𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< )))) = 𝑎) |
118 | 117 | eqcomd 2784 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℕ → 𝑎 = ((2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< )) · (𝑎 /
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, <
))))) |
119 | 118 | breq2d 4898 |
. . . . . . . 8
⊢ (𝑎 ∈ ℕ →
(((2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2)
∥ 𝑎 ↔
((2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2)
∥ ((2↑sup({𝑘
∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ·
(𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< )))))) |
120 | 15 | nnzd 11833 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℕ → 2 ∈
ℤ) |
121 | 93 | nnzd 11833 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℕ → (𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) ∈ ℤ) |
122 | 54 | nnzd 11833 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℕ →
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∈
ℤ) |
123 | | dvdscmulr 15417 |
. . . . . . . . 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, <
))))) |
124 | 120, 121,
122, 116, 123 | syl112anc 1442 |
. . . . . . . 8
⊢ (𝑎 ∈ ℕ →
(((2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2)
∥ ((2↑sup({𝑘
∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ·
(𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< )))) ↔ 2 ∥ (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, <
))))) |
125 | 119, 124 | bitrd 271 |
. . . . . . 7
⊢ (𝑎 ∈ ℕ →
(((2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2)
∥ 𝑎 ↔ 2 ∥
(𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))))) |
126 | 113, 125 | mtbid 316 |
. . . . . 6
⊢ (𝑎 ∈ ℕ → ¬ 2
∥ (𝑎 /
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, <
)))) |
127 | | breq2 4890 |
. . . . . . . 8
⊢ (𝑧 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
→ (2 ∥ 𝑧 ↔
2 ∥ (𝑎 /
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, <
))))) |
128 | 127 | notbid 310 |
. . . . . . 7
⊢ (𝑧 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
→ (¬ 2 ∥ 𝑧
↔ ¬ 2 ∥ (𝑎 /
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, <
))))) |
129 | 128, 6 | elrab2 3576 |
. . . . . 6
⊢ ((𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) ∈ 𝐽 ↔
((𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) ∈ ℕ ∧ ¬ 2 ∥ (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, <
))))) |
130 | 93, 126, 129 | sylanbrc 578 |
. . . . 5
⊢ (𝑎 ∈ ℕ → (𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) ∈ 𝐽) |
131 | 130, 53 | jca 507 |
. . . 4
⊢ (𝑎 ∈ ℕ → ((𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) ∈ 𝐽 ∧
sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈
ℕ0)) |
132 | 131 | adantl 475 |
. . 3
⊢
((⊤ ∧ 𝑎
∈ ℕ) → ((𝑎
/ (2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ 𝐽 ∧ sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
∈ ℕ0)) |
133 | | simpr 479 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑎 = ((2↑𝑦) · 𝑥)) |
134 | 2 | a1i 11 |
. . . . . . . . 9
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 2 ∈ ℕ) |
135 | | simplr 759 |
. . . . . . . . 9
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑦 ∈ ℕ0) |
136 | 134, 135 | nnexpcld 13351 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (2↑𝑦) ∈ ℕ) |
137 | 8 | sseli 3817 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐽 → 𝑥 ∈ ℕ) |
138 | 137 | ad2antrr 716 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑥 ∈ ℕ) |
139 | 136, 138 | nnmulcld 11428 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → ((2↑𝑦) · 𝑥) ∈ ℕ) |
140 | 133, 139 | eqeltrd 2859 |
. . . . . 6
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑎 ∈ ℕ) |
141 | | simplll 765 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑥 ∈ 𝐽) |
142 | | breq2 4890 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑥 → (2 ∥ 𝑧 ↔ 2 ∥ 𝑥)) |
143 | 142 | notbid 310 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑥 → (¬ 2 ∥ 𝑧 ↔ ¬ 2 ∥ 𝑥)) |
144 | 143, 6 | elrab2 3576 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐽 ↔ (𝑥 ∈ ℕ ∧ ¬ 2 ∥ 𝑥)) |
145 | 144 | simprbi 492 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐽 → ¬ 2 ∥ 𝑥) |
146 | | 2z 11761 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℤ |
147 | 135 | adantr 474 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑦 ∈
ℕ0) |
148 | 147 | nn0zd 11832 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑦 ∈
ℤ) |
149 | 19 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ < Or ℕ0) |
150 | 140, 52 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → ∃𝑚 ∈ ℕ0 (∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎} ¬ 𝑚 < 𝑛 ∧ ∀𝑛 ∈ ℕ0 (𝑛 < 𝑚 → ∃𝑜 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}𝑛 < 𝑜))) |
151 | 150 | adantr 474 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ ∃𝑚 ∈
ℕ0 (∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎} ¬ 𝑚 < 𝑛 ∧ ∀𝑛 ∈ ℕ0 (𝑛 < 𝑚 → ∃𝑜 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}𝑛 < 𝑜))) |
152 | 149, 151 | supcl 8652 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈
ℕ0) |
153 | 152 | nn0zd 11832 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈
ℤ) |
154 | | simpr 479 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑦 < sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< )) |
155 | | znnsub 11775 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℤ ∧ sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ) ∈ ℤ) → (𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
↔ (sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦) ∈
ℕ)) |
156 | 155 | biimpa 470 |
. . . . . . . . . . . . . . 15
⊢ (((𝑦 ∈ ℤ ∧ sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ) ∈ ℤ) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦) ∈
ℕ) |
157 | 148, 153,
154, 156 | syl21anc 828 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦) ∈
ℕ) |
158 | | iddvdsexp 15412 |
. . . . . . . . . . . . . 14
⊢ ((2
∈ ℤ ∧ (sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
− 𝑦) ∈ ℕ)
→ 2 ∥ (2↑(sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
− 𝑦))) |
159 | 146, 157,
158 | sylancr 581 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 2 ∥ (2↑(sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
− 𝑦))) |
160 | 146 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 2 ∈ ℤ) |
161 | 140, 121 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∈ ℤ) |
162 | 161 | adantr 474 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (𝑎 /
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈
ℤ) |
163 | 157 | nnnn0d 11702 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦) ∈
ℕ0) |
164 | | zexpcl 13193 |
. . . . . . . . . . . . . . 15
⊢ ((2
∈ ℤ ∧ (sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
− 𝑦) ∈
ℕ0) → (2↑(sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
− 𝑦)) ∈
ℤ) |
165 | 146, 163,
164 | sylancr 581 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (2↑(sup({𝑘
∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) ∈
ℤ) |
166 | | dvdsmultr2 15428 |
. . . . . . . . . . . . . 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, < ) − 𝑦))))) |
167 | 160, 162,
165, 166 | syl3anc 1439 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (2 ∥ (2↑(sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
− 𝑦)) → 2
∥ ((𝑎 /
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ·
(2↑(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦))))) |
168 | 159, 167 | mpd 15 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 2 ∥ ((𝑎 /
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ·
(2↑(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)))) |
169 | 138 | adantr 474 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑥 ∈
ℕ) |
170 | 169 | nncnd 11392 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑥 ∈
ℂ) |
171 | | 2cnd 11453 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 2 ∈ ℂ) |
172 | 171, 163 | expcld 13327 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (2↑(sup({𝑘
∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) ∈
ℂ) |
173 | 140 | adantr 474 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑎 ∈
ℕ) |
174 | 173 | nncnd 11392 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑎 ∈
ℂ) |
175 | 173, 115 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (2↑sup({𝑘
∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∈
ℂ) |
176 | | 2ne0 11486 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ≠
0 |
177 | 176 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 2 ≠ 0) |
178 | 171, 177,
153 | expne0d 13333 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (2↑sup({𝑘
∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ≠
0) |
179 | 174, 175,
178 | divcld 11151 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (𝑎 /
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈
ℂ) |
180 | 172, 179 | mulcld 10397 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ ((2↑(sup({𝑘
∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, <
)))) ∈ ℂ) |
181 | 171, 147 | expcld 13327 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (2↑𝑦) ∈
ℂ) |
182 | 171, 177,
148 | expne0d 13333 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (2↑𝑦) ≠
0) |
183 | 173, 118 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑎 =
((2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ·
(𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))))) |
184 | | simplr 759 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑎 = ((2↑𝑦) · 𝑥)) |
185 | 147 | nn0cnd 11704 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑦 ∈
ℂ) |
186 | 152 | nn0cnd 11704 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈
ℂ) |
187 | 185, 186 | pncan3d 10737 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (𝑦 + (sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ) − 𝑦)) =
sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, <
)) |
188 | 187 | oveq2d 6938 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (2↑(𝑦 +
(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦))) = (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) |
189 | 171, 163,
147 | expaddd 13329 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (2↑(𝑦 +
(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦))) = ((2↑𝑦) · (2↑(sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ) − 𝑦)))) |
190 | 188, 189 | eqtr3d 2816 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (2↑sup({𝑘
∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) =
((2↑𝑦) ·
(2↑(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)))) |
191 | 190 | oveq1d 6937 |
. . . . . . . . . . . . . . . 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, <
))))) |
192 | 183, 184,
191 | 3eqtr3d 2822 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ ((2↑𝑦) ·
𝑥) = (((2↑𝑦) · (2↑(sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ) − 𝑦)))
· (𝑎 /
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, <
))))) |
193 | 181, 172,
179 | mulassd 10400 |
. . . . . . . . . . . . . . 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, <
)))))) |
194 | 192, 193 | eqtrd 2814 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ ((2↑𝑦) ·
𝑥) = ((2↑𝑦) · ((2↑(sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ) − 𝑦)) ·
(𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< )))))) |
195 | 170, 180,
181, 182, 194 | mulcanad 11010 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑥 =
((2↑(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, <
))))) |
196 | 179, 172 | mulcomd 10398 |
. . . . . . . . . . . . 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,
< ))))) |
197 | 195, 196 | eqtr4d 2817 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑥 = ((𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) · (2↑(sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
− 𝑦)))) |
198 | 168, 197 | breqtrrd 4914 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 2 ∥ 𝑥) |
199 | 145, 198 | nsyl3 136 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ ¬ 𝑥 ∈ 𝐽) |
200 | 141, 199 | pm2.65da 807 |
. . . . . . . . 9
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → ¬ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, <
)) |
201 | 138 | nnzd 11833 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑥 ∈ ℤ) |
202 | 136 | nnzd 11833 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (2↑𝑦) ∈ ℤ) |
203 | 140 | nnzd 11833 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑎 ∈ ℤ) |
204 | 136 | nncnd 11392 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (2↑𝑦) ∈ ℂ) |
205 | 138 | nncnd 11392 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑥 ∈ ℂ) |
206 | 204, 205 | mulcomd 10398 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → ((2↑𝑦) · 𝑥) = (𝑥 · (2↑𝑦))) |
207 | 133, 206 | eqtr2d 2815 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑥 · (2↑𝑦)) = 𝑎) |
208 | | dvds0lem 15399 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℤ ∧
(2↑𝑦) ∈ ℤ
∧ 𝑎 ∈ ℤ)
∧ (𝑥 ·
(2↑𝑦)) = 𝑎) → (2↑𝑦) ∥ 𝑎) |
209 | 201, 202,
203, 207, 208 | syl31anc 1441 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (2↑𝑦) ∥ 𝑎) |
210 | | oveq2 6930 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑦 → (2↑𝑘) = (2↑𝑦)) |
211 | 210 | breq1d 4896 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑦 → ((2↑𝑘) ∥ 𝑎 ↔ (2↑𝑦) ∥ 𝑎)) |
212 | 211 | elrab 3572 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎} ↔ (𝑦 ∈ ℕ0 ∧
(2↑𝑦) ∥ 𝑎)) |
213 | 135, 209,
212 | sylanbrc 578 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑦 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}) |
214 | 19 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → < Or
ℕ0) |
215 | 214, 150 | supub 8653 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑦 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎} → ¬ sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ) < 𝑦)) |
216 | 213, 215 | mpd 15 |
. . . . . . . . 9
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → ¬ sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
< 𝑦) |
217 | 135 | nn0red 11703 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑦 ∈ ℝ) |
218 | 140, 97 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
∈ ℝ) |
219 | 217, 218 | lttri3d 10516 |
. . . . . . . . 9
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
↔ (¬ 𝑦 <
sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∧ ¬
sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) < 𝑦))) |
220 | 200, 216,
219 | mpbir2and 703 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, <
)) |
221 | | simplr 759 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑎 = ((2↑𝑦) · 𝑥)) |
222 | 140 | adantr 474 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑎 ∈
ℕ) |
223 | 222 | nncnd 11392 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑎 ∈
ℂ) |
224 | 138 | adantr 474 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑥 ∈
ℕ) |
225 | 224 | nncnd 11392 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑥 ∈
ℂ) |
226 | | nnexpcl 13191 |
. . . . . . . . . . . . . . . 16
⊢ ((2
∈ ℕ ∧ 𝑦
∈ ℕ0) → (2↑𝑦) ∈ ℕ) |
227 | 2, 226 | mpan 680 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℕ0
→ (2↑𝑦) ∈
ℕ) |
228 | 227 | nncnd 11392 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ0
→ (2↑𝑦) ∈
ℂ) |
229 | 227 | nnne0d 11425 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ0
→ (2↑𝑦) ≠
0) |
230 | 228, 229 | jca 507 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ0
→ ((2↑𝑦) ∈
ℂ ∧ (2↑𝑦)
≠ 0)) |
231 | 230 | ad3antlr 721 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ ((2↑𝑦) ∈
ℂ ∧ (2↑𝑦)
≠ 0)) |
232 | | divmul2 11037 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧
((2↑𝑦) ∈ ℂ
∧ (2↑𝑦) ≠ 0))
→ ((𝑎 / (2↑𝑦)) = 𝑥 ↔ 𝑎 = ((2↑𝑦) · 𝑥))) |
233 | 223, 225,
231, 232 | syl3anc 1439 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ ((𝑎 / (2↑𝑦)) = 𝑥 ↔ 𝑎 = ((2↑𝑦) · 𝑥))) |
234 | 221, 233 | mpbird 249 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (𝑎 / (2↑𝑦)) = 𝑥) |
235 | | simpr 479 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< )) |
236 | 235 | oveq2d 6938 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (2↑𝑦) =
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, <
))) |
237 | 236 | oveq2d 6938 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (𝑎 / (2↑𝑦)) = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, <
)))) |
238 | 234, 237 | eqtr3d 2816 |
. . . . . . . . 9
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< )))) |
239 | 238 | ex 403 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
→ 𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))))) |
240 | 220, 239 | jcai 512 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
∧ 𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))))) |
241 | 240 | ancomd 455 |
. . . . . 6
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) |
242 | 140, 241 | jca 507 |
. . . . 5
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< )))) |
243 | | simprl 761 |
. . . . . . 7
⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) → 𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< )))) |
244 | 130 | adantr 474 |
. . . . . . 7
⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) → (𝑎 /
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ 𝐽) |
245 | 243, 244 | eqeltrd 2859 |
. . . . . 6
⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) → 𝑥 ∈
𝐽) |
246 | | simprr 763 |
. . . . . . 7
⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) → 𝑦 =
sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, <
)) |
247 | 53 | adantr 474 |
. . . . . . 7
⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) → sup({𝑘
∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈
ℕ0) |
248 | 246, 247 | eqeltrd 2859 |
. . . . . 6
⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) → 𝑦 ∈
ℕ0) |
249 | 118 | adantr 474 |
. . . . . . 7
⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) → 𝑎 =
((2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ·
(𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))))) |
250 | 246 | oveq2d 6938 |
. . . . . . . 8
⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) → (2↑𝑦)
= (2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, <
))) |
251 | 250, 243 | oveq12d 6940 |
. . . . . . 7
⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) → ((2↑𝑦)
· 𝑥) =
((2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ·
(𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))))) |
252 | 249, 251 | eqtr4d 2817 |
. . . . . 6
⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) → 𝑎 =
((2↑𝑦) · 𝑥)) |
253 | 245, 248,
252 | jca31 510 |
. . . . 5
⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) → ((𝑥 ∈
𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥))) |
254 | 242, 253 | impbii 201 |
. . . 4
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ↔ (𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< )))) |
255 | 254 | a1i 11 |
. . 3
⊢ (⊤
→ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ↔ (𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))))) |
256 | 1, 13, 132, 255 | f1od2 30065 |
. 2
⊢ (⊤
→ 𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ) |
257 | 256 | mptru 1609 |
1
⊢ 𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ |