Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  oddpwdc Structured version   Visualization version   GIF version

Theorem oddpwdc 29550
Description: Lemma for eulerpart 29578. The function 𝐹 that decomposes a number into its "odd" and "even" parts, which is to say the largest power of two and largest odd divisor of a number, is a bijection from pairs of a nonnegative integer and an odd number to positive integers. (Contributed by Thierry Arnoux, 15-Aug-2017.)
Hypotheses
Ref Expression
oddpwdc.j 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}
oddpwdc.f 𝐹 = (𝑥𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))
Assertion
Ref Expression
oddpwdc 𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ
Distinct variable groups:   𝑥,𝑦,𝑧   𝑥,𝐽,𝑦
Allowed substitution hints:   𝐹(𝑥,𝑦,𝑧)   𝐽(𝑧)

Proof of Theorem oddpwdc
Dummy variables 𝑘 𝑎 𝑙 𝑚 𝑛 𝑜 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oddpwdc.f . . 3 𝐹 = (𝑥𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))
2 2nn 10940 . . . . . . . 8 2 ∈ ℕ
32a1i 11 . . . . . . 7 ((𝑦 ∈ ℕ0𝑥𝐽) → 2 ∈ ℕ)
4 simpl 471 . . . . . . 7 ((𝑦 ∈ ℕ0𝑥𝐽) → 𝑦 ∈ ℕ0)
53, 4nnexpcld 12760 . . . . . 6 ((𝑦 ∈ ℕ0𝑥𝐽) → (2↑𝑦) ∈ ℕ)
6 oddpwdc.j . . . . . . . 8 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}
7 ssrab2 3554 . . . . . . . 8 {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} ⊆ ℕ
86, 7eqsstri 3502 . . . . . . 7 𝐽 ⊆ ℕ
9 simpr 475 . . . . . . 7 ((𝑦 ∈ ℕ0𝑥𝐽) → 𝑥𝐽)
108, 9sseldi 3470 . . . . . 6 ((𝑦 ∈ ℕ0𝑥𝐽) → 𝑥 ∈ ℕ)
115, 10nnmulcld 10823 . . . . 5 ((𝑦 ∈ ℕ0𝑥𝐽) → ((2↑𝑦) · 𝑥) ∈ ℕ)
1211ancoms 467 . . . 4 ((𝑥𝐽𝑦 ∈ ℕ0) → ((2↑𝑦) · 𝑥) ∈ ℕ)
1312adantl 480 . . 3 ((⊤ ∧ (𝑥𝐽𝑦 ∈ ℕ0)) → ((2↑𝑦) · 𝑥) ∈ ℕ)
14 id 22 . . . . . . 7 (𝑎 ∈ ℕ → 𝑎 ∈ ℕ)
152a1i 11 . . . . . . . 8 (𝑎 ∈ ℕ → 2 ∈ ℕ)
16 nn0ssre 11051 . . . . . . . . . . 11 0 ⊆ ℝ
17 ltso 9868 . . . . . . . . . . 11 < Or ℝ
18 soss 4871 . . . . . . . . . . 11 (ℕ0 ⊆ ℝ → ( < Or ℝ → < Or ℕ0))
1916, 17, 18mp2 9 . . . . . . . . . 10 < Or ℕ0
2019a1i 11 . . . . . . . . 9 (𝑎 ∈ ℕ → < Or ℕ0)
21 0zd 11130 . . . . . . . . . 10 (𝑎 ∈ ℕ → 0 ∈ ℤ)
22 ssrab2 3554 . . . . . . . . . . 11 {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ⊆ ℕ0
2322a1i 11 . . . . . . . . . 10 (𝑎 ∈ ℕ → {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ⊆ ℕ0)
24 nnz 11140 . . . . . . . . . . 11 (𝑎 ∈ ℕ → 𝑎 ∈ ℤ)
25 oveq2 6434 . . . . . . . . . . . . . . 15 (𝑘 = 𝑛 → (2↑𝑘) = (2↑𝑛))
2625breq1d 4491 . . . . . . . . . . . . . 14 (𝑘 = 𝑛 → ((2↑𝑘) ∥ 𝑎 ↔ (2↑𝑛) ∥ 𝑎))
2726elrab 3235 . . . . . . . . . . . . 13 (𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ↔ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎))
28 simprl 789 . . . . . . . . . . . . . . 15 ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → 𝑛 ∈ ℕ0)
2928nn0red 11107 . . . . . . . . . . . . . 14 ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → 𝑛 ∈ ℝ)
302a1i 11 . . . . . . . . . . . . . . . 16 ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → 2 ∈ ℕ)
3130, 28nnexpcld 12760 . . . . . . . . . . . . . . 15 ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → (2↑𝑛) ∈ ℕ)
3231nnred 10790 . . . . . . . . . . . . . 14 ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → (2↑𝑛) ∈ ℝ)
33 simpl 471 . . . . . . . . . . . . . . 15 ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → 𝑎 ∈ ℕ)
3433nnred 10790 . . . . . . . . . . . . . 14 ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → 𝑎 ∈ ℝ)
35 2re 10845 . . . . . . . . . . . . . . . 16 2 ∈ ℝ
3635leidi 10311 . . . . . . . . . . . . . . . 16 2 ≤ 2
37 nexple 29195 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ ℕ0 ∧ 2 ∈ ℝ ∧ 2 ≤ 2) → 𝑛 ≤ (2↑𝑛))
3835, 36, 37mp3an23 1407 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ0𝑛 ≤ (2↑𝑛))
3938ad2antrl 759 . . . . . . . . . . . . . 14 ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → 𝑛 ≤ (2↑𝑛))
4031nnzd 11221 . . . . . . . . . . . . . . 15 ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → (2↑𝑛) ∈ ℤ)
41 simprr 791 . . . . . . . . . . . . . . 15 ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → (2↑𝑛) ∥ 𝑎)
42 dvdsle 14739 . . . . . . . . . . . . . . . 16 (((2↑𝑛) ∈ ℤ ∧ 𝑎 ∈ ℕ) → ((2↑𝑛) ∥ 𝑎 → (2↑𝑛) ≤ 𝑎))
4342imp 443 . . . . . . . . . . . . . . 15 ((((2↑𝑛) ∈ ℤ ∧ 𝑎 ∈ ℕ) ∧ (2↑𝑛) ∥ 𝑎) → (2↑𝑛) ≤ 𝑎)
4440, 33, 41, 43syl21anc 1316 . . . . . . . . . . . . . 14 ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → (2↑𝑛) ≤ 𝑎)
4529, 32, 34, 39, 44letrd 9945 . . . . . . . . . . . . 13 ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → 𝑛𝑎)
4627, 45sylan2b 490 . . . . . . . . . . . 12 ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}) → 𝑛𝑎)
4746ralrimiva 2853 . . . . . . . . . . 11 (𝑎 ∈ ℕ → ∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}𝑛𝑎)
48 breq2 4485 . . . . . . . . . . . . 13 (𝑚 = 𝑎 → (𝑛𝑚𝑛𝑎))
4948ralbidv 2873 . . . . . . . . . . . 12 (𝑚 = 𝑎 → (∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}𝑛𝑚 ↔ ∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}𝑛𝑎))
5049rspcev 3186 . . . . . . . . . . 11 ((𝑎 ∈ ℤ ∧ ∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}𝑛𝑎) → ∃𝑚 ∈ ℤ ∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}𝑛𝑚)
5124, 47, 50syl2anc 690 . . . . . . . . . 10 (𝑎 ∈ ℕ → ∃𝑚 ∈ ℤ ∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}𝑛𝑚)
52 nn0uz 11462 . . . . . . . . . . 11 0 = (ℤ‘0)
5352uzsupss 11522 . . . . . . . . . 10 ((0 ∈ ℤ ∧ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ⊆ ℕ0 ∧ ∃𝑚 ∈ ℤ ∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}𝑛𝑚) → ∃𝑚 ∈ ℕ0 (∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ¬ 𝑚 < 𝑛 ∧ ∀𝑛 ∈ ℕ0 (𝑛 < 𝑚 → ∃𝑜 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}𝑛 < 𝑜)))
5421, 23, 51, 53syl3anc 1317 . . . . . . . . 9 (𝑎 ∈ ℕ → ∃𝑚 ∈ ℕ0 (∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ¬ 𝑚 < 𝑛 ∧ ∀𝑛 ∈ ℕ0 (𝑛 < 𝑚 → ∃𝑜 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}𝑛 < 𝑜)))
5520, 54supcl 8123 . . . . . . . 8 (𝑎 ∈ ℕ → sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℕ0)
5615, 55nnexpcld 12760 . . . . . . 7 (𝑎 ∈ ℕ → (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∈ ℕ)
57 fzfi 12501 . . . . . . . . . . . 12 (0...𝑎) ∈ Fin
58 0zd 11130 . . . . . . . . . . . . . . 15 ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}) → 0 ∈ ℤ)
5924adantr 479 . . . . . . . . . . . . . . 15 ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}) → 𝑎 ∈ ℤ)
6027, 28sylan2b 490 . . . . . . . . . . . . . . . 16 ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}) → 𝑛 ∈ ℕ0)
6160nn0zd 11220 . . . . . . . . . . . . . . 15 ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}) → 𝑛 ∈ ℤ)
6260nn0ge0d 11109 . . . . . . . . . . . . . . 15 ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}) → 0 ≤ 𝑛)
63 elfz4 12074 . . . . . . . . . . . . . . 15 (((0 ∈ ℤ ∧ 𝑎 ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ (0 ≤ 𝑛𝑛𝑎)) → 𝑛 ∈ (0...𝑎))
6458, 59, 61, 62, 46, 63syl32anc 1325 . . . . . . . . . . . . . 14 ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}) → 𝑛 ∈ (0...𝑎))
6564ex 448 . . . . . . . . . . . . 13 (𝑎 ∈ ℕ → (𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} → 𝑛 ∈ (0...𝑎)))
6665ssrdv 3478 . . . . . . . . . . . 12 (𝑎 ∈ ℕ → {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ⊆ (0...𝑎))
67 ssfi 7941 . . . . . . . . . . . 12 (((0...𝑎) ∈ Fin ∧ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ⊆ (0...𝑎)) → {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ∈ Fin)
6857, 66, 67sylancr 693 . . . . . . . . . . 11 (𝑎 ∈ ℕ → {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ∈ Fin)
69 0nn0 11062 . . . . . . . . . . . . . 14 0 ∈ ℕ0
7069a1i 11 . . . . . . . . . . . . 13 (𝑎 ∈ ℕ → 0 ∈ ℕ0)
71 2cn 10846 . . . . . . . . . . . . . . 15 2 ∈ ℂ
72 exp0 12594 . . . . . . . . . . . . . . 15 (2 ∈ ℂ → (2↑0) = 1)
7371, 72ax-mp 5 . . . . . . . . . . . . . 14 (2↑0) = 1
74 1dvds 14703 . . . . . . . . . . . . . . 15 (𝑎 ∈ ℤ → 1 ∥ 𝑎)
7524, 74syl 17 . . . . . . . . . . . . . 14 (𝑎 ∈ ℕ → 1 ∥ 𝑎)
7673, 75syl5eqbr 4516 . . . . . . . . . . . . 13 (𝑎 ∈ ℕ → (2↑0) ∥ 𝑎)
77 oveq2 6434 . . . . . . . . . . . . . . 15 (𝑘 = 0 → (2↑𝑘) = (2↑0))
7877breq1d 4491 . . . . . . . . . . . . . 14 (𝑘 = 0 → ((2↑𝑘) ∥ 𝑎 ↔ (2↑0) ∥ 𝑎))
7978elrab 3235 . . . . . . . . . . . . 13 (0 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ↔ (0 ∈ ℕ0 ∧ (2↑0) ∥ 𝑎))
8070, 76, 79sylanbrc 694 . . . . . . . . . . . 12 (𝑎 ∈ ℕ → 0 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎})
81 ne0i 3783 . . . . . . . . . . . 12 (0 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} → {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ≠ ∅)
8280, 81syl 17 . . . . . . . . . . 11 (𝑎 ∈ ℕ → {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ≠ ∅)
83 fisupcl 8134 . . . . . . . . . . 11 (( < Or ℕ0 ∧ ({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ∈ Fin ∧ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ≠ ∅ ∧ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ⊆ ℕ0)) → sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎})
8420, 68, 82, 23, 83syl13anc 1319 . . . . . . . . . 10 (𝑎 ∈ ℕ → sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎})
85 oveq2 6434 . . . . . . . . . . . 12 (𝑘 = 𝑙 → (2↑𝑘) = (2↑𝑙))
8685breq1d 4491 . . . . . . . . . . 11 (𝑘 = 𝑙 → ((2↑𝑘) ∥ 𝑎 ↔ (2↑𝑙) ∥ 𝑎))
8786cbvrabv 3076 . . . . . . . . . 10 {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} = {𝑙 ∈ ℕ0 ∣ (2↑𝑙) ∥ 𝑎}
8884, 87syl6eleq 2602 . . . . . . . . 9 (𝑎 ∈ ℕ → sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ {𝑙 ∈ ℕ0 ∣ (2↑𝑙) ∥ 𝑎})
89 oveq2 6434 . . . . . . . . . . 11 (𝑙 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) → (2↑𝑙) = (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))
9089breq1d 4491 . . . . . . . . . 10 (𝑙 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) → ((2↑𝑙) ∥ 𝑎 ↔ (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∥ 𝑎))
9190elrab 3235 . . . . . . . . 9 (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ {𝑙 ∈ ℕ0 ∣ (2↑𝑙) ∥ 𝑎} ↔ (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℕ0 ∧ (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∥ 𝑎))
9288, 91sylib 206 . . . . . . . 8 (𝑎 ∈ ℕ → (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℕ0 ∧ (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∥ 𝑎))
9392simprd 477 . . . . . . 7 (𝑎 ∈ ℕ → (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∥ 𝑎)
94 nndivdvds 14696 . . . . . . . 8 ((𝑎 ∈ ℕ ∧ (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∈ ℕ) → ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∥ 𝑎 ↔ (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ ℕ))
9594biimpa 499 . . . . . . 7 (((𝑎 ∈ ℕ ∧ (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∈ ℕ) ∧ (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∥ 𝑎) → (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ ℕ)
9614, 56, 93, 95syl21anc 1316 . . . . . 6 (𝑎 ∈ ℕ → (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ ℕ)
97 1nn0 11063 . . . . . . . . . . 11 1 ∈ ℕ0
9897a1i 11 . . . . . . . . . 10 (𝑎 ∈ ℕ → 1 ∈ ℕ0)
9955, 98nn0addcld 11110 . . . . . . . . 9 (𝑎 ∈ ℕ → (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈ ℕ0)
10055nn0red 11107 . . . . . . . . . . . . . 14 (𝑎 ∈ ℕ → sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℝ)
101100ltp1d 10704 . . . . . . . . . . . . 13 (𝑎 ∈ ℕ → sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) < (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1))
10220, 54supub 8124 . . . . . . . . . . . . 13 (𝑎 ∈ ℕ → ((sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} → ¬ sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) < (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)))
103101, 102mt2d 129 . . . . . . . . . . . 12 (𝑎 ∈ ℕ → ¬ (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎})
10487eleq2i 2584 . . . . . . . . . . . 12 ((sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ↔ (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈ {𝑙 ∈ ℕ0 ∣ (2↑𝑙) ∥ 𝑎})
105103, 104sylnib 316 . . . . . . . . . . 11 (𝑎 ∈ ℕ → ¬ (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈ {𝑙 ∈ ℕ0 ∣ (2↑𝑙) ∥ 𝑎})
106 oveq2 6434 . . . . . . . . . . . . 13 (𝑙 = (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) → (2↑𝑙) = (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)))
107106breq1d 4491 . . . . . . . . . . . 12 (𝑙 = (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) → ((2↑𝑙) ∥ 𝑎 ↔ (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) ∥ 𝑎))
108107elrab 3235 . . . . . . . . . . 11 ((sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈ {𝑙 ∈ ℕ0 ∣ (2↑𝑙) ∥ 𝑎} ↔ ((sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈ ℕ0 ∧ (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) ∥ 𝑎))
109105, 108sylnib 316 . . . . . . . . . 10 (𝑎 ∈ ℕ → ¬ ((sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈ ℕ0 ∧ (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) ∥ 𝑎))
110 imnan 436 . . . . . . . . . 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)) ∥ 𝑎))
111109, 110sylibr 222 . . . . . . . . 9 (𝑎 ∈ ℕ → ((sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈ ℕ0 → ¬ (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) ∥ 𝑎))
11299, 111mpd 15 . . . . . . . 8 (𝑎 ∈ ℕ → ¬ (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) ∥ 𝑎)
113 expp1 12597 . . . . . . . . . 10 ((2 ∈ ℂ ∧ sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℕ0) → (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) = ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2))
11471, 55, 113sylancr 693 . . . . . . . . 9 (𝑎 ∈ ℕ → (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) = ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2))
115114breq1d 4491 . . . . . . . 8 (𝑎 ∈ ℕ → ((2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) ∥ 𝑎 ↔ ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2) ∥ 𝑎))
116112, 115mtbid 312 . . . . . . 7 (𝑎 ∈ ℕ → ¬ ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2) ∥ 𝑎)
117 nncn 10783 . . . . . . . . . . 11 (𝑎 ∈ ℕ → 𝑎 ∈ ℂ)
11856nncnd 10791 . . . . . . . . . . 11 (𝑎 ∈ ℕ → (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∈ ℂ)
11956nnne0d 10820 . . . . . . . . . . 11 (𝑎 ∈ ℕ → (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ≠ 0)
120117, 118, 119divcan2d 10552 . . . . . . . . . 10 (𝑎 ∈ ℕ → ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))) = 𝑎)
121120eqcomd 2520 . . . . . . . . 9 (𝑎 ∈ ℕ → 𝑎 = ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
122121breq2d 4493 . . . . . . . 8 (𝑎 ∈ ℕ → (((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2) ∥ 𝑎 ↔ ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2) ∥ ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))))))
12315nnzd 11221 . . . . . . . . 9 (𝑎 ∈ ℕ → 2 ∈ ℤ)
12496nnzd 11221 . . . . . . . . 9 (𝑎 ∈ ℕ → (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ ℤ)
12556nnzd 11221 . . . . . . . . 9 (𝑎 ∈ ℕ → (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∈ ℤ)
126 dvdscmulr 14717 . . . . . . . . 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, < )))))
127123, 124, 125, 119, 126syl112anc 1321 . . . . . . . 8 (𝑎 ∈ ℕ → (((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2) ∥ ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))) ↔ 2 ∥ (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
128122, 127bitrd 266 . . . . . . 7 (𝑎 ∈ ℕ → (((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2) ∥ 𝑎 ↔ 2 ∥ (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
129116, 128mtbid 312 . . . . . 6 (𝑎 ∈ ℕ → ¬ 2 ∥ (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))))
130 breq2 4485 . . . . . . . 8 (𝑧 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → (2 ∥ 𝑧 ↔ 2 ∥ (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
131130notbid 306 . . . . . . 7 (𝑧 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → (¬ 2 ∥ 𝑧 ↔ ¬ 2 ∥ (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
132131, 6elrab2 3237 . . . . . 6 ((𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ 𝐽 ↔ ((𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ ℕ ∧ ¬ 2 ∥ (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
13396, 129, 132sylanbrc 694 . . . . 5 (𝑎 ∈ ℕ → (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ 𝐽)
134133, 55jca 552 . . . 4 (𝑎 ∈ ℕ → ((𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ 𝐽 ∧ sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℕ0))
135134adantl 480 . . 3 ((⊤ ∧ 𝑎 ∈ ℕ) → ((𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ 𝐽 ∧ sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℕ0))
136 simpr 475 . . . . . . 7 (((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑎 = ((2↑𝑦) · 𝑥))
1372a1i 11 . . . . . . . . 9 (((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 2 ∈ ℕ)
138 simplr 787 . . . . . . . . 9 (((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑦 ∈ ℕ0)
139137, 138nnexpcld 12760 . . . . . . . 8 (((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (2↑𝑦) ∈ ℕ)
1408sseli 3468 . . . . . . . . 9 (𝑥𝐽𝑥 ∈ ℕ)
141140ad2antrr 757 . . . . . . . 8 (((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑥 ∈ ℕ)
142139, 141nnmulcld 10823 . . . . . . 7 (((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → ((2↑𝑦) · 𝑥) ∈ ℕ)
143136, 142eqeltrd 2592 . . . . . 6 (((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑎 ∈ ℕ)
144 simplll 793 . . . . . . . . . 10 ((((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑥𝐽)
145 breq2 4485 . . . . . . . . . . . . . 14 (𝑧 = 𝑥 → (2 ∥ 𝑧 ↔ 2 ∥ 𝑥))
146145notbid 306 . . . . . . . . . . . . 13 (𝑧 = 𝑥 → (¬ 2 ∥ 𝑧 ↔ ¬ 2 ∥ 𝑥))
147146, 6elrab2 3237 . . . . . . . . . . . 12 (𝑥𝐽 ↔ (𝑥 ∈ ℕ ∧ ¬ 2 ∥ 𝑥))
148147simprbi 478 . . . . . . . . . . 11 (𝑥𝐽 → ¬ 2 ∥ 𝑥)
149 2z 11150 . . . . . . . . . . . . . 14 2 ∈ ℤ
150138adantr 479 . . . . . . . . . . . . . . . 16 ((((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑦 ∈ ℕ0)
151150nn0zd 11220 . . . . . . . . . . . . . . 15 ((((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑦 ∈ ℤ)
15219a1i 11 . . . . . . . . . . . . . . . . 17 ((((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → < Or ℕ0)
153143, 54syl 17 . . . . . . . . . . . . . . . . . 18 (((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → ∃𝑚 ∈ ℕ0 (∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ¬ 𝑚 < 𝑛 ∧ ∀𝑛 ∈ ℕ0 (𝑛 < 𝑚 → ∃𝑜 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}𝑛 < 𝑜)))
154153adantr 479 . . . . . . . . . . . . . . . . 17 ((((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → ∃𝑚 ∈ ℕ0 (∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ¬ 𝑚 < 𝑛 ∧ ∀𝑛 ∈ ℕ0 (𝑛 < 𝑚 → ∃𝑜 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}𝑛 < 𝑜)))
155152, 154supcl 8123 . . . . . . . . . . . . . . . 16 ((((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℕ0)
156155nn0zd 11220 . . . . . . . . . . . . . . 15 ((((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℤ)
157 simpr 475 . . . . . . . . . . . . . . 15 ((((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))
158 znnsub 11164 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ℤ ∧ sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℤ) → (𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ↔ (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦) ∈ ℕ))
159158biimpa 499 . . . . . . . . . . . . . . 15 (((𝑦 ∈ ℤ ∧ sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℤ) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦) ∈ ℕ)
160151, 156, 157, 159syl21anc 1316 . . . . . . . . . . . . . 14 ((((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦) ∈ ℕ)
161 iddvdsexp 14712 . . . . . . . . . . . . . 14 ((2 ∈ ℤ ∧ (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦) ∈ ℕ) → 2 ∥ (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)))
162149, 160, 161sylancr 693 . . . . . . . . . . . . 13 ((((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 2 ∥ (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)))
163149a1i 11 . . . . . . . . . . . . . 14 ((((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 2 ∈ ℤ)
164143, 124syl 17 . . . . . . . . . . . . . . 15 (((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ ℤ)
165164adantr 479 . . . . . . . . . . . . . 14 ((((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ ℤ)
166160nnnn0d 11106 . . . . . . . . . . . . . . 15 ((((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦) ∈ ℕ0)
167 zexpcl 12605 . . . . . . . . . . . . . . 15 ((2 ∈ ℤ ∧ (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦) ∈ ℕ0) → (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) ∈ ℤ)
168149, 166, 167sylancr 693 . . . . . . . . . . . . . 14 ((((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) ∈ ℤ)
169 dvdsmultr2 14728 . . . . . . . . . . . . . 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, < ) − 𝑦)))))
170163, 165, 168, 169syl3anc 1317 . . . . . . . . . . . . 13 ((((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (2 ∥ (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) → 2 ∥ ((𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) · (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)))))
171162, 170mpd 15 . . . . . . . . . . . 12 ((((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 2 ∥ ((𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) · (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦))))
172141adantr 479 . . . . . . . . . . . . . . 15 ((((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑥 ∈ ℕ)
173172nncnd 10791 . . . . . . . . . . . . . 14 ((((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑥 ∈ ℂ)
174 2cnd 10848 . . . . . . . . . . . . . . . 16 ((((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 2 ∈ ℂ)
175174, 166expcld 12738 . . . . . . . . . . . . . . 15 ((((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) ∈ ℂ)
176143adantr 479 . . . . . . . . . . . . . . . . 17 ((((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑎 ∈ ℕ)
177176nncnd 10791 . . . . . . . . . . . . . . . 16 ((((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑎 ∈ ℂ)
178176, 118syl 17 . . . . . . . . . . . . . . . 16 ((((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∈ ℂ)
179 2ne0 10868 . . . . . . . . . . . . . . . . . 18 2 ≠ 0
180179a1i 11 . . . . . . . . . . . . . . . . 17 ((((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 2 ≠ 0)
181174, 180, 156expne0d 12744 . . . . . . . . . . . . . . . 16 ((((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ≠ 0)
182177, 178, 181divcld 10550 . . . . . . . . . . . . . . 15 ((((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ ℂ)
183175, 182mulcld 9815 . . . . . . . . . . . . . 14 ((((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → ((2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))) ∈ ℂ)
184174, 150expcld 12738 . . . . . . . . . . . . . 14 ((((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (2↑𝑦) ∈ ℂ)
185174, 180, 151expne0d 12744 . . . . . . . . . . . . . 14 ((((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (2↑𝑦) ≠ 0)
186176, 121syl 17 . . . . . . . . . . . . . . . 16 ((((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑎 = ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
187 simplr 787 . . . . . . . . . . . . . . . 16 ((((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑎 = ((2↑𝑦) · 𝑥))
188150nn0cnd 11108 . . . . . . . . . . . . . . . . . . . 20 ((((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑦 ∈ ℂ)
189155nn0cnd 11108 . . . . . . . . . . . . . . . . . . . 20 ((((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℂ)
190188, 189pncan3d 10146 . . . . . . . . . . . . . . . . . . 19 ((((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (𝑦 + (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))
191190oveq2d 6442 . . . . . . . . . . . . . . . . . 18 ((((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (2↑(𝑦 + (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦))) = (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))
192174, 166, 150expaddd 12740 . . . . . . . . . . . . . . . . . 18 ((((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (2↑(𝑦 + (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦))) = ((2↑𝑦) · (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦))))
193191, 192eqtr3d 2550 . . . . . . . . . . . . . . . . 17 ((((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) = ((2↑𝑦) · (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦))))
194193oveq1d 6441 . . . . . . . . . . . . . . . 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, < )))))
195186, 187, 1943eqtr3d 2556 . . . . . . . . . . . . . . 15 ((((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → ((2↑𝑦) · 𝑥) = (((2↑𝑦) · (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦))) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
196184, 175, 182mulassd 9818 . . . . . . . . . . . . . . 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, < ))))))
197195, 196eqtrd 2548 . . . . . . . . . . . . . 14 ((((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → ((2↑𝑦) · 𝑥) = ((2↑𝑦) · ((2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))))))
198173, 183, 184, 185, 197mulcanad 10411 . . . . . . . . . . . . 13 ((((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑥 = ((2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
199182, 175mulcomd 9816 . . . . . . . . . . . . 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, < )))))
200198, 199eqtr4d 2551 . . . . . . . . . . . 12 ((((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑥 = ((𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) · (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦))))
201171, 200breqtrrd 4509 . . . . . . . . . . 11 ((((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 2 ∥ 𝑥)
202148, 201nsyl3 131 . . . . . . . . . 10 ((((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → ¬ 𝑥𝐽)
203144, 202pm2.65da 597 . . . . . . . . 9 (((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → ¬ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))
204141nnzd 11221 . . . . . . . . . . . 12 (((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑥 ∈ ℤ)
205139nnzd 11221 . . . . . . . . . . . 12 (((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (2↑𝑦) ∈ ℤ)
206143nnzd 11221 . . . . . . . . . . . 12 (((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑎 ∈ ℤ)
207139nncnd 10791 . . . . . . . . . . . . . 14 (((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (2↑𝑦) ∈ ℂ)
208141nncnd 10791 . . . . . . . . . . . . . 14 (((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑥 ∈ ℂ)
209207, 208mulcomd 9816 . . . . . . . . . . . . 13 (((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → ((2↑𝑦) · 𝑥) = (𝑥 · (2↑𝑦)))
210136, 209eqtr2d 2549 . . . . . . . . . . . 12 (((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑥 · (2↑𝑦)) = 𝑎)
211 dvds0lem 14699 . . . . . . . . . . . 12 (((𝑥 ∈ ℤ ∧ (2↑𝑦) ∈ ℤ ∧ 𝑎 ∈ ℤ) ∧ (𝑥 · (2↑𝑦)) = 𝑎) → (2↑𝑦) ∥ 𝑎)
212204, 205, 206, 210, 211syl31anc 1320 . . . . . . . . . . 11 (((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (2↑𝑦) ∥ 𝑎)
213 oveq2 6434 . . . . . . . . . . . . 13 (𝑘 = 𝑦 → (2↑𝑘) = (2↑𝑦))
214213breq1d 4491 . . . . . . . . . . . 12 (𝑘 = 𝑦 → ((2↑𝑘) ∥ 𝑎 ↔ (2↑𝑦) ∥ 𝑎))
215214elrab 3235 . . . . . . . . . . 11 (𝑦 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ↔ (𝑦 ∈ ℕ0 ∧ (2↑𝑦) ∥ 𝑎))
216138, 212, 215sylanbrc 694 . . . . . . . . . 10 (((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑦 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎})
21719a1i 11 . . . . . . . . . . 11 (((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → < Or ℕ0)
218217, 153supub 8124 . . . . . . . . . 10 (((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑦 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} → ¬ sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) < 𝑦))
219216, 218mpd 15 . . . . . . . . 9 (((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → ¬ sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) < 𝑦)
220138nn0red 11107 . . . . . . . . . 10 (((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑦 ∈ ℝ)
221143, 100syl 17 . . . . . . . . . 10 (((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℝ)
222220, 221lttri3d 9928 . . . . . . . . 9 (((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ↔ (¬ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∧ ¬ sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) < 𝑦)))
223203, 219, 222mpbir2and 958 . . . . . . . 8 (((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))
224 simplr 787 . . . . . . . . . . 11 ((((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑎 = ((2↑𝑦) · 𝑥))
225143adantr 479 . . . . . . . . . . . . 13 ((((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑎 ∈ ℕ)
226225nncnd 10791 . . . . . . . . . . . 12 ((((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑎 ∈ ℂ)
227141adantr 479 . . . . . . . . . . . . 13 ((((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑥 ∈ ℕ)
228227nncnd 10791 . . . . . . . . . . . 12 ((((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑥 ∈ ℂ)
229 nnexpcl 12603 . . . . . . . . . . . . . . . 16 ((2 ∈ ℕ ∧ 𝑦 ∈ ℕ0) → (2↑𝑦) ∈ ℕ)
2302, 229mpan 701 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ0 → (2↑𝑦) ∈ ℕ)
231230nncnd 10791 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ0 → (2↑𝑦) ∈ ℂ)
232230nnne0d 10820 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ0 → (2↑𝑦) ≠ 0)
233231, 232jca 552 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ0 → ((2↑𝑦) ∈ ℂ ∧ (2↑𝑦) ≠ 0))
234233ad3antlr 762 . . . . . . . . . . . 12 ((((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → ((2↑𝑦) ∈ ℂ ∧ (2↑𝑦) ≠ 0))
235 divmul2 10438 . . . . . . . . . . . 12 ((𝑎 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ ((2↑𝑦) ∈ ℂ ∧ (2↑𝑦) ≠ 0)) → ((𝑎 / (2↑𝑦)) = 𝑥𝑎 = ((2↑𝑦) · 𝑥)))
236226, 228, 234, 235syl3anc 1317 . . . . . . . . . . 11 ((((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → ((𝑎 / (2↑𝑦)) = 𝑥𝑎 = ((2↑𝑦) · 𝑥)))
237224, 236mpbird 245 . . . . . . . . . 10 ((((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (𝑎 / (2↑𝑦)) = 𝑥)
238 simpr 475 . . . . . . . . . . . 12 ((((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))
239238oveq2d 6442 . . . . . . . . . . 11 ((((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (2↑𝑦) = (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))
240239oveq2d 6442 . . . . . . . . . 10 ((((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (𝑎 / (2↑𝑦)) = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))))
241237, 240eqtr3d 2550 . . . . . . . . 9 ((((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))))
242241ex 448 . . . . . . . 8 (((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) → 𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
243223, 242jcai 556 . . . . . . 7 (((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∧ 𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
244243ancomd 465 . . . . . 6 (((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))
245143, 244jca 552 . . . . 5 (((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))))
246 simprl 789 . . . . . . 7 ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → 𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))))
247133adantr 479 . . . . . . 7 ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ 𝐽)
248246, 247eqeltrd 2592 . . . . . 6 ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → 𝑥𝐽)
249 simprr 791 . . . . . . 7 ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))
25055adantr 479 . . . . . . 7 ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℕ0)
251249, 250eqeltrd 2592 . . . . . 6 ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → 𝑦 ∈ ℕ0)
252121adantr 479 . . . . . . 7 ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → 𝑎 = ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
253249oveq2d 6442 . . . . . . . 8 ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → (2↑𝑦) = (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))
254253, 246oveq12d 6444 . . . . . . 7 ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → ((2↑𝑦) · 𝑥) = ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
255252, 254eqtr4d 2551 . . . . . 6 ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → 𝑎 = ((2↑𝑦) · 𝑥))
256248, 251, 255jca31 554 . . . . 5 ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → ((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)))
257245, 256impbii 197 . . . 4 (((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ↔ (𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))))
258257a1i 11 . . 3 (⊤ → (((𝑥𝐽𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ↔ (𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
2591, 13, 135, 258f1od2 28675 . 2 (⊤ → 𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ)
260259trud 1483 1 𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wa 382   = wceq 1474  wtru 1475  wcel 1938  wne 2684  wral 2800  wrex 2801  {crab 2804  wss 3444  c0 3777   class class class wbr 4481   Or wor 4852   × cxp 4930  1-1-ontowf1o 5688  (class class class)co 6426  cmpt2 6428  Fincfn 7717  supcsup 8105  cc 9689  cr 9690  0cc0 9691  1c1 9692   + caddc 9694   · cmul 9696   < clt 9829  cle 9830  cmin 10017   / cdiv 10433  cn 10775  2c2 10825  0cn0 11047  cz 11118  ...cfz 12065  cexp 12590  cdvds 14690
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-8 1940  ax-9 1947  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-sep 4607  ax-nul 4616  ax-pow 4668  ax-pr 4732  ax-un 6723  ax-cnex 9747  ax-resscn 9748  ax-1cn 9749  ax-icn 9750  ax-addcl 9751  ax-addrcl 9752  ax-mulcl 9753  ax-mulrcl 9754  ax-mulcom 9755  ax-addass 9756  ax-mulass 9757  ax-distr 9758  ax-i2m1 9759  ax-1ne0 9760  ax-1rid 9761  ax-rnegex 9762  ax-rrecex 9763  ax-cnre 9764  ax-pre-lttri 9765  ax-pre-lttrn 9766  ax-pre-ltadd 9767  ax-pre-mulgt0 9768
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-eu 2366  df-mo 2367  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ne 2686  df-nel 2687  df-ral 2805  df-rex 2806  df-reu 2807  df-rmo 2808  df-rab 2809  df-v 3079  df-sbc 3307  df-csb 3404  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-pss 3460  df-nul 3778  df-if 3940  df-pw 4013  df-sn 4029  df-pr 4031  df-tp 4033  df-op 4035  df-uni 4271  df-iun 4355  df-br 4482  df-opab 4542  df-mpt 4543  df-tr 4579  df-eprel 4843  df-id 4847  df-po 4853  df-so 4854  df-fr 4891  df-we 4893  df-xp 4938  df-rel 4939  df-cnv 4940  df-co 4941  df-dm 4942  df-rn 4943  df-res 4944  df-ima 4945  df-pred 5487  df-ord 5533  df-on 5534  df-lim 5535  df-suc 5536  df-iota 5653  df-fun 5691  df-fn 5692  df-f 5693  df-f1 5694  df-fo 5695  df-f1o 5696  df-fv 5697  df-riota 6388  df-ov 6429  df-oprab 6430  df-mpt2 6431  df-om 6834  df-1st 6934  df-2nd 6935  df-wrecs 7169  df-recs 7231  df-rdg 7269  df-1o 7323  df-er 7505  df-en 7718  df-dom 7719  df-sdom 7720  df-fin 7721  df-sup 8107  df-inf 8108  df-pnf 9831  df-mnf 9832  df-xr 9833  df-ltxr 9834  df-le 9835  df-sub 10019  df-neg 10020  df-div 10434  df-nn 10776  df-2 10834  df-n0 11048  df-z 11119  df-uz 11428  df-fz 12066  df-seq 12532  df-exp 12591  df-dvds 14691
This theorem is referenced by:  eulerpartgbij  29568  eulerpartlemgvv  29572  eulerpartlemgh  29574  eulerpartlemgf  29575
  Copyright terms: Public domain W3C validator