Step | Hyp | Ref
| Expression |
1 | | oddpwdc.f |
. . 3
⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦
((2↑𝑦) · 𝑥)) |
2 | | 2nn 11698 |
. . . . . . . 8
⊢ 2 ∈
ℕ |
3 | 2 | a1i 11 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ0
∧ 𝑥 ∈ 𝐽) → 2 ∈
ℕ) |
4 | | simpl 483 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ0
∧ 𝑥 ∈ 𝐽) → 𝑦 ∈ ℕ0) |
5 | 3, 4 | nnexpcld 13594 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ0
∧ 𝑥 ∈ 𝐽) → (2↑𝑦) ∈
ℕ) |
6 | | oddpwdc.j |
. . . . . . . 8
⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} |
7 | | ssrab2 4053 |
. . . . . . . 8
⊢ {𝑧 ∈ ℕ ∣ ¬ 2
∥ 𝑧} ⊆
ℕ |
8 | 6, 7 | eqsstri 3998 |
. . . . . . 7
⊢ 𝐽 ⊆
ℕ |
9 | | simpr 485 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ0
∧ 𝑥 ∈ 𝐽) → 𝑥 ∈ 𝐽) |
10 | 8, 9 | sseldi 3962 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ0
∧ 𝑥 ∈ 𝐽) → 𝑥 ∈ ℕ) |
11 | 5, 10 | nnmulcld 11678 |
. . . . 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 11889 |
. . . . . . . . . . 11
⊢
ℕ0 ⊆ ℝ |
17 | | ltso 10709 |
. . . . . . . . . . 11
⊢ < Or
ℝ |
18 | | soss 5486 |
. . . . . . . . . . 11
⊢
(ℕ0 ⊆ ℝ → ( < Or ℝ →
< Or ℕ0)) |
19 | 16, 17, 18 | mp2 9 |
. . . . . . . . . 10
⊢ < Or
ℕ0 |
20 | 19 | a1i 11 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℕ → < Or
ℕ0) |
21 | | 0zd 11981 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ℕ → 0 ∈
ℤ) |
22 | | ssrab2 4053 |
. . . . . . . . . . 11
⊢ {𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎} ⊆
ℕ0 |
23 | 22 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ℕ → {𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎} ⊆
ℕ0) |
24 | | nnz 11992 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ ℕ → 𝑎 ∈
ℤ) |
25 | | oveq2 7153 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑛 → (2↑𝑘) = (2↑𝑛)) |
26 | 25 | breq1d 5067 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑛 → ((2↑𝑘) ∥ 𝑎 ↔ (2↑𝑛) ∥ 𝑎)) |
27 | 26 | elrab 3677 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎} ↔ (𝑛 ∈ ℕ0 ∧
(2↑𝑛) ∥ 𝑎)) |
28 | | simprl 767 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0
∧ (2↑𝑛) ∥
𝑎)) → 𝑛 ∈
ℕ0) |
29 | 28 | nn0red 11944 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0
∧ (2↑𝑛) ∥
𝑎)) → 𝑛 ∈
ℝ) |
30 | 2 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0
∧ (2↑𝑛) ∥
𝑎)) → 2 ∈
ℕ) |
31 | 30, 28 | nnexpcld 13594 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0
∧ (2↑𝑛) ∥
𝑎)) → (2↑𝑛) ∈
ℕ) |
32 | 31 | nnred 11641 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0
∧ (2↑𝑛) ∥
𝑎)) → (2↑𝑛) ∈
ℝ) |
33 | | simpl 483 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0
∧ (2↑𝑛) ∥
𝑎)) → 𝑎 ∈
ℕ) |
34 | 33 | nnred 11641 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0
∧ (2↑𝑛) ∥
𝑎)) → 𝑎 ∈
ℝ) |
35 | | 2re 11699 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℝ |
36 | 35 | leidi 11162 |
. . . . . . . . . . . . . . . 16
⊢ 2 ≤
2 |
37 | | nexple 31167 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈ ℕ0
∧ 2 ∈ ℝ ∧ 2 ≤ 2) → 𝑛 ≤ (2↑𝑛)) |
38 | 35, 36, 37 | mp3an23 1444 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ0
→ 𝑛 ≤ (2↑𝑛)) |
39 | 38 | ad2antrl 724 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0
∧ (2↑𝑛) ∥
𝑎)) → 𝑛 ≤ (2↑𝑛)) |
40 | 31 | nnzd 12074 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0
∧ (2↑𝑛) ∥
𝑎)) → (2↑𝑛) ∈
ℤ) |
41 | | simprr 769 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0
∧ (2↑𝑛) ∥
𝑎)) → (2↑𝑛) ∥ 𝑎) |
42 | | dvdsle 15648 |
. . . . . . . . . . . . . . . 16
⊢
(((2↑𝑛) ∈
ℤ ∧ 𝑎 ∈
ℕ) → ((2↑𝑛)
∥ 𝑎 →
(2↑𝑛) ≤ 𝑎)) |
43 | 42 | imp 407 |
. . . . . . . . . . . . . . 15
⊢
((((2↑𝑛) ∈
ℤ ∧ 𝑎 ∈
ℕ) ∧ (2↑𝑛)
∥ 𝑎) →
(2↑𝑛) ≤ 𝑎) |
44 | 40, 33, 41, 43 | syl21anc 833 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0
∧ (2↑𝑛) ∥
𝑎)) → (2↑𝑛) ≤ 𝑎) |
45 | 29, 32, 34, 39, 44 | letrd 10785 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0
∧ (2↑𝑛) ∥
𝑎)) → 𝑛 ≤ 𝑎) |
46 | 27, 45 | sylan2b 593 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}) → 𝑛 ≤ 𝑎) |
47 | 46 | ralrimiva 3179 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ ℕ →
∀𝑛 ∈ {𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}𝑛 ≤ 𝑎) |
48 | | brralrspcev 5117 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ ℤ ∧
∀𝑛 ∈ {𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}𝑛 ≤ 𝑎) → ∃𝑚 ∈ ℤ ∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}𝑛 ≤ 𝑚) |
49 | 24, 47, 48 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ℕ →
∃𝑚 ∈ ℤ
∀𝑛 ∈ {𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}𝑛 ≤ 𝑚) |
50 | | nn0uz 12268 |
. . . . . . . . . . 11
⊢
ℕ0 = (ℤ≥‘0) |
51 | 50 | uzsupss 12328 |
. . . . . . . . . 10
⊢ ((0
∈ ℤ ∧ {𝑘
∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ⊆ ℕ0 ∧
∃𝑚 ∈ ℤ
∀𝑛 ∈ {𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}𝑛 ≤ 𝑚) → ∃𝑚 ∈ ℕ0 (∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎} ¬ 𝑚 < 𝑛 ∧ ∀𝑛 ∈ ℕ0 (𝑛 < 𝑚 → ∃𝑜 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}𝑛 < 𝑜))) |
52 | 21, 23, 49, 51 | syl3anc 1363 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℕ →
∃𝑚 ∈
ℕ0 (∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎} ¬ 𝑚 < 𝑛 ∧ ∀𝑛 ∈ ℕ0 (𝑛 < 𝑚 → ∃𝑜 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}𝑛 < 𝑜))) |
53 | 20, 52 | supcl 8910 |
. . . . . . . 8
⊢ (𝑎 ∈ ℕ →
sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈
ℕ0) |
54 | 15, 53 | nnexpcld 13594 |
. . . . . . 7
⊢ (𝑎 ∈ ℕ →
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∈
ℕ) |
55 | | fzfi 13328 |
. . . . . . . . . . . 12
⊢
(0...𝑎) ∈
Fin |
56 | | 0zd 11981 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}) → 0 ∈
ℤ) |
57 | 24 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}) → 𝑎 ∈ ℤ) |
58 | 27, 28 | sylan2b 593 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}) → 𝑛 ∈ ℕ0) |
59 | 58 | nn0zd 12073 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}) → 𝑛 ∈ ℤ) |
60 | 58 | nn0ge0d 11946 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}) → 0 ≤ 𝑛) |
61 | | elfz4 12889 |
. . . . . . . . . . . . . . 15
⊢ (((0
∈ ℤ ∧ 𝑎
∈ ℤ ∧ 𝑛
∈ ℤ) ∧ (0 ≤ 𝑛 ∧ 𝑛 ≤ 𝑎)) → 𝑛 ∈ (0...𝑎)) |
62 | 56, 57, 59, 60, 46, 61 | syl32anc 1370 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}) → 𝑛 ∈ (0...𝑎)) |
63 | 62 | ex 413 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ ℕ → (𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎} → 𝑛 ∈ (0...𝑎))) |
64 | 63 | ssrdv 3970 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ ℕ → {𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎} ⊆ (0...𝑎)) |
65 | | ssfi 8726 |
. . . . . . . . . . . 12
⊢
(((0...𝑎) ∈ Fin
∧ {𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ⊆ (0...𝑎)) → {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎} ∈ Fin) |
66 | 55, 64, 65 | sylancr 587 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ ℕ → {𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎} ∈
Fin) |
67 | | 0nn0 11900 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℕ0 |
68 | 67 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ ℕ → 0 ∈
ℕ0) |
69 | | 2cn 11700 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℂ |
70 | | exp0 13421 |
. . . . . . . . . . . . . . 15
⊢ (2 ∈
ℂ → (2↑0) = 1) |
71 | 69, 70 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
(2↑0) = 1 |
72 | | 1dvds 15612 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ ℤ → 1 ∥
𝑎) |
73 | 24, 72 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ ℕ → 1 ∥
𝑎) |
74 | 71, 73 | eqbrtrid 5092 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ ℕ →
(2↑0) ∥ 𝑎) |
75 | | oveq2 7153 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 0 → (2↑𝑘) = (2↑0)) |
76 | 75 | breq1d 5067 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 0 → ((2↑𝑘) ∥ 𝑎 ↔ (2↑0) ∥ 𝑎)) |
77 | 76 | elrab 3677 |
. . . . . . . . . . . . 13
⊢ (0 ∈
{𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ↔ (0 ∈ ℕ0 ∧
(2↑0) ∥ 𝑎)) |
78 | 68, 74, 77 | sylanbrc 583 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ ℕ → 0 ∈
{𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}) |
79 | 78 | ne0d 4298 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ ℕ → {𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎} ≠
∅) |
80 | | fisupcl 8921 |
. . . . . . . . . . 11
⊢ (( <
Or ℕ0 ∧ ({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎} ∈ Fin ∧ {𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎} ≠ ∅ ∧
{𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ⊆ ℕ0)) →
sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ {𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}) |
81 | 20, 66, 79, 23, 80 | syl13anc 1364 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ℕ →
sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ {𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}) |
82 | | oveq2 7153 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑙 → (2↑𝑘) = (2↑𝑙)) |
83 | 82 | breq1d 5067 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑙 → ((2↑𝑘) ∥ 𝑎 ↔ (2↑𝑙) ∥ 𝑎)) |
84 | 83 | cbvrabv 3489 |
. . . . . . . . . 10
⊢ {𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎} = {𝑙 ∈ ℕ0 ∣
(2↑𝑙) ∥ 𝑎} |
85 | 81, 84 | eleqtrdi 2920 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℕ →
sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ {𝑙 ∈ ℕ0
∣ (2↑𝑙) ∥
𝑎}) |
86 | | oveq2 7153 |
. . . . . . . . . . 11
⊢ (𝑙 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
→ (2↑𝑙) =
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, <
))) |
87 | 86 | breq1d 5067 |
. . . . . . . . . 10
⊢ (𝑙 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
→ ((2↑𝑙) ∥
𝑎 ↔ (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< )) ∥ 𝑎)) |
88 | 87 | elrab 3677 |
. . . . . . . . 9
⊢
(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ {𝑙 ∈ ℕ0
∣ (2↑𝑙) ∥
𝑎} ↔ (sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ) ∈ ℕ0 ∧ (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
∥ 𝑎)) |
89 | 85, 88 | sylib 219 |
. . . . . . . 8
⊢ (𝑎 ∈ ℕ →
(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈
ℕ0 ∧ (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
∥ 𝑎)) |
90 | 89 | simprd 496 |
. . . . . . 7
⊢ (𝑎 ∈ ℕ →
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∥ 𝑎) |
91 | | nndivdvds 15604 |
. . . . . . . 8
⊢ ((𝑎 ∈ ℕ ∧
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∈
ℕ) → ((2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
∥ 𝑎 ↔ (𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) ∈ ℕ)) |
92 | 91 | biimpa 477 |
. . . . . . 7
⊢ (((𝑎 ∈ ℕ ∧
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∈
ℕ) ∧ (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
∥ 𝑎) → (𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) ∈ ℕ) |
93 | 14, 54, 90, 92 | syl21anc 833 |
. . . . . 6
⊢ (𝑎 ∈ ℕ → (𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) ∈ ℕ) |
94 | | 1nn0 11901 |
. . . . . . . . . . 11
⊢ 1 ∈
ℕ0 |
95 | 94 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ℕ → 1 ∈
ℕ0) |
96 | 53, 95 | nn0addcld 11947 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℕ →
(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈
ℕ0) |
97 | 53 | nn0red 11944 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ ℕ →
sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈
ℝ) |
98 | 97 | ltp1d 11558 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ ℕ →
sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) <
(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) +
1)) |
99 | 20, 52 | supub 8911 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ ℕ →
((sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈
{𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎} → ¬ sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
< (sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) +
1))) |
100 | 98, 99 | mt2d 138 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ ℕ → ¬
(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈
{𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}) |
101 | 84 | eleq2i 2901 |
. . . . . . . . . . . 12
⊢
((sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈
{𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ↔ (sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ) +
1) ∈ {𝑙 ∈
ℕ0 ∣ (2↑𝑙) ∥ 𝑎}) |
102 | 100, 101 | sylnib 329 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ ℕ → ¬
(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈
{𝑙 ∈
ℕ0 ∣ (2↑𝑙) ∥ 𝑎}) |
103 | | oveq2 7153 |
. . . . . . . . . . . . 13
⊢ (𝑙 = (sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ) +
1) → (2↑𝑙) =
(2↑(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) +
1))) |
104 | 103 | breq1d 5067 |
. . . . . . . . . . . 12
⊢ (𝑙 = (sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ) +
1) → ((2↑𝑙)
∥ 𝑎 ↔
(2↑(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) ∥
𝑎)) |
105 | 104 | elrab 3677 |
. . . . . . . . . . 11
⊢
((sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈
{𝑙 ∈
ℕ0 ∣ (2↑𝑙) ∥ 𝑎} ↔ ((sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ) +
1) ∈ ℕ0 ∧ (2↑(sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ) +
1)) ∥ 𝑎)) |
106 | 102, 105 | sylnib 329 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ℕ → ¬
((sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈
ℕ0 ∧ (2↑(sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ) +
1)) ∥ 𝑎)) |
107 | | 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)) ∥ 𝑎)) |
108 | 106, 107 | sylibr 235 |
. . . . . . . . 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 13424 |
. . . . . . . . . 10
⊢ ((2
∈ ℂ ∧ sup({𝑘
∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈
ℕ0) → (2↑(sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ) +
1)) = ((2↑sup({𝑘
∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ·
2)) |
111 | 69, 53, 110 | sylancr 587 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℕ →
(2↑(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) =
((2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ·
2)) |
112 | 111 | breq1d 5067 |
. . . . . . . 8
⊢ (𝑎 ∈ ℕ →
((2↑(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) ∥
𝑎 ↔
((2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2)
∥ 𝑎)) |
113 | 109, 112 | mtbid 325 |
. . . . . . 7
⊢ (𝑎 ∈ ℕ → ¬
((2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2)
∥ 𝑎) |
114 | | nncn 11634 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ ℕ → 𝑎 ∈
ℂ) |
115 | 54 | nncnd 11642 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ ℕ →
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∈
ℂ) |
116 | 54 | nnne0d 11675 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ ℕ →
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ≠
0) |
117 | 114, 115,
116 | divcan2d 11406 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ℕ →
((2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ·
(𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< )))) = 𝑎) |
118 | 117 | eqcomd 2824 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℕ → 𝑎 = ((2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< )) · (𝑎 /
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, <
))))) |
119 | 118 | breq2d 5069 |
. . . . . . . 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 12074 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℕ → 2 ∈
ℤ) |
121 | 93 | nnzd 12074 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℕ → (𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) ∈ ℤ) |
122 | 54 | nnzd 12074 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℕ →
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∈
ℤ) |
123 | | dvdscmulr 15626 |
. . . . . . . . 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 1366 |
. . . . . . . 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 280 |
. . . . . . 7
⊢ (𝑎 ∈ ℕ →
(((2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2)
∥ 𝑎 ↔ 2 ∥
(𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))))) |
126 | 113, 125 | mtbid 325 |
. . . . . 6
⊢ (𝑎 ∈ ℕ → ¬ 2
∥ (𝑎 /
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, <
)))) |
127 | | breq2 5061 |
. . . . . . . 8
⊢ (𝑧 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
→ (2 ∥ 𝑧 ↔
2 ∥ (𝑎 /
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, <
))))) |
128 | 127 | notbid 319 |
. . . . . . 7
⊢ (𝑧 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
→ (¬ 2 ∥ 𝑧
↔ ¬ 2 ∥ (𝑎 /
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, <
))))) |
129 | 128, 6 | elrab2 3680 |
. . . . . 6
⊢ ((𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) ∈ 𝐽 ↔
((𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) ∈ ℕ ∧ ¬ 2 ∥ (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, <
))))) |
130 | 93, 126, 129 | sylanbrc 583 |
. . . . 5
⊢ (𝑎 ∈ ℕ → (𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) ∈ 𝐽) |
131 | 130, 53 | jca 512 |
. . . 4
⊢ (𝑎 ∈ ℕ → ((𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) ∈ 𝐽 ∧
sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈
ℕ0)) |
132 | 131 | adantl 482 |
. . 3
⊢
((⊤ ∧ 𝑎
∈ ℕ) → ((𝑎
/ (2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ 𝐽 ∧ sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
∈ ℕ0)) |
133 | | simpr 485 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑎 = ((2↑𝑦) · 𝑥)) |
134 | 2 | a1i 11 |
. . . . . . . . 9
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 2 ∈ ℕ) |
135 | | simplr 765 |
. . . . . . . . 9
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑦 ∈ ℕ0) |
136 | 134, 135 | nnexpcld 13594 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (2↑𝑦) ∈ ℕ) |
137 | 8 | sseli 3960 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐽 → 𝑥 ∈ ℕ) |
138 | 137 | ad2antrr 722 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑥 ∈ ℕ) |
139 | 136, 138 | nnmulcld 11678 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → ((2↑𝑦) · 𝑥) ∈ ℕ) |
140 | 133, 139 | eqeltrd 2910 |
. . . . . 6
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑎 ∈ ℕ) |
141 | | simplll 771 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑥 ∈ 𝐽) |
142 | | breq2 5061 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑥 → (2 ∥ 𝑧 ↔ 2 ∥ 𝑥)) |
143 | 142 | notbid 319 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑥 → (¬ 2 ∥ 𝑧 ↔ ¬ 2 ∥ 𝑥)) |
144 | 143, 6 | elrab2 3680 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐽 ↔ (𝑥 ∈ ℕ ∧ ¬ 2 ∥ 𝑥)) |
145 | 144 | simprbi 497 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐽 → ¬ 2 ∥ 𝑥) |
146 | | 2z 12002 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℤ |
147 | 135 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑦 ∈
ℕ0) |
148 | 147 | nn0zd 12073 |
. . . . . . . . . . . . . . 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 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ ∃𝑚 ∈
ℕ0 (∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎} ¬ 𝑚 < 𝑛 ∧ ∀𝑛 ∈ ℕ0 (𝑛 < 𝑚 → ∃𝑜 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}𝑛 < 𝑜))) |
152 | 149, 151 | supcl 8910 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈
ℕ0) |
153 | 152 | nn0zd 12073 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈
ℤ) |
154 | | simpr 485 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑦 < sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< )) |
155 | | znnsub 12016 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℤ ∧ sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ) ∈ ℤ) → (𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
↔ (sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦) ∈
ℕ)) |
156 | 155 | biimpa 477 |
. . . . . . . . . . . . . . 15
⊢ (((𝑦 ∈ ℤ ∧ sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ) ∈ ℤ) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦) ∈
ℕ) |
157 | 148, 153,
154, 156 | syl21anc 833 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦) ∈
ℕ) |
158 | | iddvdsexp 15621 |
. . . . . . . . . . . . . 14
⊢ ((2
∈ ℤ ∧ (sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
− 𝑦) ∈ ℕ)
→ 2 ∥ (2↑(sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
− 𝑦))) |
159 | 146, 157,
158 | sylancr 587 |
. . . . . . . . . . . . 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 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (𝑎 /
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈
ℤ) |
163 | 157 | nnnn0d 11943 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦) ∈
ℕ0) |
164 | | zexpcl 13432 |
. . . . . . . . . . . . . . 15
⊢ ((2
∈ ℤ ∧ (sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
− 𝑦) ∈
ℕ0) → (2↑(sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
− 𝑦)) ∈
ℤ) |
165 | 146, 163,
164 | sylancr 587 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (2↑(sup({𝑘
∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) ∈
ℤ) |
166 | | dvdsmultr2 15637 |
. . . . . . . . . . . . . 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 1363 |
. . . . . . . . . . . . 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 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑥 ∈
ℕ) |
170 | 169 | nncnd 11642 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑥 ∈
ℂ) |
171 | | 2cnd 11703 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 2 ∈ ℂ) |
172 | 171, 163 | expcld 13498 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (2↑(sup({𝑘
∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) ∈
ℂ) |
173 | 140 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑎 ∈
ℕ) |
174 | 173 | nncnd 11642 |
. . . . . . . . . . . . . . . 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 11729 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ≠
0 |
177 | 176 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 2 ≠ 0) |
178 | 171, 177,
153 | expne0d 13504 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (2↑sup({𝑘
∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ≠
0) |
179 | 174, 175,
178 | divcld 11404 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (𝑎 /
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈
ℂ) |
180 | 172, 179 | mulcld 10649 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ ((2↑(sup({𝑘
∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, <
)))) ∈ ℂ) |
181 | 171, 147 | expcld 13498 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (2↑𝑦) ∈
ℂ) |
182 | 171, 177,
148 | expne0d 13504 |
. . . . . . . . . . . . . 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 765 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑎 = ((2↑𝑦) · 𝑥)) |
185 | 147 | nn0cnd 11945 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑦 ∈
ℂ) |
186 | 152 | nn0cnd 11945 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈
ℂ) |
187 | 185, 186 | pncan3d 10988 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (𝑦 + (sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ) − 𝑦)) =
sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, <
)) |
188 | 187 | oveq2d 7161 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (2↑(𝑦 +
(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦))) = (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) |
189 | 171, 163,
147 | expaddd 13500 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (2↑(𝑦 +
(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦))) = ((2↑𝑦) · (2↑(sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ) − 𝑦)))) |
190 | 188, 189 | eqtr3d 2855 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (2↑sup({𝑘
∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) =
((2↑𝑦) ·
(2↑(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)))) |
191 | 190 | oveq1d 7160 |
. . . . . . . . . . . . . . . 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 2861 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ ((2↑𝑦) ·
𝑥) = (((2↑𝑦) · (2↑(sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ) − 𝑦)))
· (𝑎 /
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, <
))))) |
193 | 181, 172,
179 | mulassd 10652 |
. . . . . . . . . . . . . . 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 2853 |
. . . . . . . . . . . . . 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 11263 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑥 =
((2↑(sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, <
))))) |
196 | 179, 172 | mulcomd 10650 |
. . . . . . . . . . . . 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 2856 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑥 = ((𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) · (2↑(sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
− 𝑦)))) |
198 | 168, 197 | breqtrrd 5085 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 2 ∥ 𝑥) |
199 | 145, 198 | nsyl3 140 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ ¬ 𝑥 ∈ 𝐽) |
200 | 141, 199 | pm2.65da 813 |
. . . . . . . . 9
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → ¬ 𝑦 < sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, <
)) |
201 | 138 | nnzd 12074 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑥 ∈ ℤ) |
202 | 136 | nnzd 12074 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (2↑𝑦) ∈ ℤ) |
203 | 140 | nnzd 12074 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑎 ∈ ℤ) |
204 | 136 | nncnd 11642 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (2↑𝑦) ∈ ℂ) |
205 | 138 | nncnd 11642 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑥 ∈ ℂ) |
206 | 204, 205 | mulcomd 10650 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → ((2↑𝑦) · 𝑥) = (𝑥 · (2↑𝑦))) |
207 | 133, 206 | eqtr2d 2854 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑥 · (2↑𝑦)) = 𝑎) |
208 | | dvds0lem 15608 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℤ ∧
(2↑𝑦) ∈ ℤ
∧ 𝑎 ∈ ℤ)
∧ (𝑥 ·
(2↑𝑦)) = 𝑎) → (2↑𝑦) ∥ 𝑎) |
209 | 201, 202,
203, 207, 208 | syl31anc 1365 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (2↑𝑦) ∥ 𝑎) |
210 | | oveq2 7153 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑦 → (2↑𝑘) = (2↑𝑦)) |
211 | 210 | breq1d 5067 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑦 → ((2↑𝑘) ∥ 𝑎 ↔ (2↑𝑦) ∥ 𝑎)) |
212 | 211 | elrab 3677 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎} ↔ (𝑦 ∈ ℕ0 ∧
(2↑𝑦) ∥ 𝑎)) |
213 | 135, 209,
212 | sylanbrc 583 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑦 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}) |
214 | 19 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → < Or
ℕ0) |
215 | 214, 150 | supub 8911 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑦 ∈ {𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎} → ¬ sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ) < 𝑦)) |
216 | 213, 215 | mpd 15 |
. . . . . . . . 9
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → ¬ sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
< 𝑦) |
217 | 135 | nn0red 11944 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑦 ∈ ℝ) |
218 | 140, 97 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
∈ ℝ) |
219 | 217, 218 | lttri3d 10768 |
. . . . . . . . 9
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
↔ (¬ 𝑦 <
sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∧ ¬
sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) < 𝑦))) |
220 | 200, 216,
219 | mpbir2and 709 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, <
)) |
221 | | simplr 765 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑎 = ((2↑𝑦) · 𝑥)) |
222 | 140 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑎 ∈
ℕ) |
223 | 222 | nncnd 11642 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑎 ∈
ℂ) |
224 | 138 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑥 ∈
ℕ) |
225 | 224 | nncnd 11642 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑥 ∈
ℂ) |
226 | | nnexpcl 13430 |
. . . . . . . . . . . . . . . 16
⊢ ((2
∈ ℕ ∧ 𝑦
∈ ℕ0) → (2↑𝑦) ∈ ℕ) |
227 | 2, 226 | mpan 686 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℕ0
→ (2↑𝑦) ∈
ℕ) |
228 | 227 | nncnd 11642 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ0
→ (2↑𝑦) ∈
ℂ) |
229 | 227 | nnne0d 11675 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ0
→ (2↑𝑦) ≠
0) |
230 | 228, 229 | jca 512 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ0
→ ((2↑𝑦) ∈
ℂ ∧ (2↑𝑦)
≠ 0)) |
231 | 230 | ad3antlr 727 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ ((2↑𝑦) ∈
ℂ ∧ (2↑𝑦)
≠ 0)) |
232 | | divmul2 11290 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧
((2↑𝑦) ∈ ℂ
∧ (2↑𝑦) ≠ 0))
→ ((𝑎 / (2↑𝑦)) = 𝑥 ↔ 𝑎 = ((2↑𝑦) · 𝑥))) |
233 | 223, 225,
231, 232 | syl3anc 1363 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ ((𝑎 / (2↑𝑦)) = 𝑥 ↔ 𝑎 = ((2↑𝑦) · 𝑥))) |
234 | 221, 233 | mpbird 258 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (𝑎 / (2↑𝑦)) = 𝑥) |
235 | | simpr 485 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< )) |
236 | 235 | oveq2d 7161 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (2↑𝑦) =
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, <
))) |
237 | 236 | oveq2d 7161 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ (𝑎 / (2↑𝑦)) = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, <
)))) |
238 | 234, 237 | eqtr3d 2855 |
. . . . . . . . 9
⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < ))
→ 𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< )))) |
239 | 238 | ex 413 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
→ 𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))))) |
240 | 220, 239 | jcai 517 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑦 = sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )
∧ 𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))))) |
241 | 240 | ancomd 462 |
. . . . . 6
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) |
242 | 140, 241 | jca 512 |
. . . . 5
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< )))) |
243 | | simprl 767 |
. . . . . . 7
⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) → 𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< )))) |
244 | 130 | adantr 481 |
. . . . . . 7
⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) → (𝑎 /
(2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ 𝐽) |
245 | 243, 244 | eqeltrd 2910 |
. . . . . 6
⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) → 𝑥 ∈
𝐽) |
246 | | simprr 769 |
. . . . . . 7
⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) → 𝑦 =
sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, <
)) |
247 | 53 | adantr 481 |
. . . . . . 7
⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) → sup({𝑘
∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈
ℕ0) |
248 | 246, 247 | eqeltrd 2910 |
. . . . . 6
⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) → 𝑦 ∈
ℕ0) |
249 | 118 | adantr 481 |
. . . . . . 7
⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) → 𝑎 =
((2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ·
(𝑎 / (2↑sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))))) |
250 | 246 | oveq2d 7161 |
. . . . . . . 8
⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) → (2↑𝑦)
= (2↑sup({𝑘 ∈
ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, <
))) |
251 | 250, 243 | oveq12d 7163 |
. . . . . . 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 2856 |
. . . . . 6
⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) → 𝑎 =
((2↑𝑦) · 𝑥)) |
253 | 245, 248,
252 | jca31 515 |
. . . . 5
⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣
(2↑𝑘) ∥ 𝑎}, ℕ0, < )))
∧ 𝑦 = sup({𝑘 ∈ ℕ0
∣ (2↑𝑘) ∥
𝑎}, ℕ0,
< ))) → ((𝑥 ∈
𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥))) |
254 | 242, 253 | impbii 210 |
. . . 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 30383 |
. 2
⊢ (⊤
→ 𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ) |
257 | 256 | mptru 1535 |
1
⊢ 𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ |