Metamath Proof Explorer

Theorem oddpwdc

Description: Lemma for eulerpart . The function F 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)

Ref Expression
Hypotheses oddpwdc.j ⊢ 𝐽 = { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 }
oddpwdc.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐽 , 𝑦 ∈ ℕ0 ↦ ( ( 2 ↑ 𝑦 ) · 𝑥 ) )
Assertion oddpwdc 𝐹 : ( 𝐽 × ℕ0 ) –1-1-onto→ ℕ

Proof

Step Hyp Ref Expression
1 oddpwdc.j ⊢ 𝐽 = { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 }
2 oddpwdc.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐽 , 𝑦 ∈ ℕ0 ↦ ( ( 2 ↑ 𝑦 ) · 𝑥 ) )
3 2nn ⊢ 2 ∈ ℕ
4 3 a1i ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑥 ∈ 𝐽 ) → 2 ∈ ℕ )
5 simpl ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑥 ∈ 𝐽 ) → 𝑦 ∈ ℕ0 )
6 4 5 nnexpcld ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑥 ∈ 𝐽 ) → ( 2 ↑ 𝑦 ) ∈ ℕ )
7 ssrab2 ⊢ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ⊆ ℕ
8 1 7 eqsstri ⊢ 𝐽 ⊆ ℕ
9 simpr ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑥 ∈ 𝐽 ) → 𝑥 ∈ 𝐽 )
10 8 9 sselid ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑥 ∈ 𝐽 ) → 𝑥 ∈ ℕ )
11 6 10 nnmulcld ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑥 ∈ 𝐽 ) → ( ( 2 ↑ 𝑦 ) · 𝑥 ) ∈ ℕ )
12 11 ancoms ⊢ ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) → ( ( 2 ↑ 𝑦 ) · 𝑥 ) ∈ ℕ )
13 12 adantl ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ) → ( ( 2 ↑ 𝑦 ) · 𝑥 ) ∈ ℕ )
14 id ⊢ ( 𝑎 ∈ ℕ → 𝑎 ∈ ℕ )
15 3 a1i ⊢ ( 𝑎 ∈ ℕ → 2 ∈ ℕ )
16 nn0ssre ⊢ ℕ0 ⊆ ℝ
17 ltso ⊢ < Or ℝ
18 soss ⊢ ( ℕ0 ⊆ ℝ → ( < Or ℝ → < Or ℕ0 ) )
19 16 17 18 mp2 ⊢ < Or ℕ0
20 19 a1i ⊢ ( 𝑎 ∈ ℕ → < Or ℕ0 )
21 0zd ⊢ ( 𝑎 ∈ ℕ → 0 ∈ ℤ )
22 ssrab2 ⊢ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } ⊆ ℕ0
23 22 a1i ⊢ ( 𝑎 ∈ ℕ → { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } ⊆ ℕ0 )
24 nnz ⊢ ( 𝑎 ∈ ℕ → 𝑎 ∈ ℤ )
25 oveq2 ⊢ ( 𝑘 = 𝑛 → ( 2 ↑ 𝑘 ) = ( 2 ↑ 𝑛 ) )
26 25 breq1d ⊢ ( 𝑘 = 𝑛 → ( ( 2 ↑ 𝑘 ) ∥ 𝑎 ↔ ( 2 ↑ 𝑛 ) ∥ 𝑎 ) )
27 26 elrab ⊢ ( 𝑛 ∈ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } ↔ ( 𝑛 ∈ ℕ0 ∧ ( 2 ↑ 𝑛 ) ∥ 𝑎 ) )
28 simprl ⊢ ( ( 𝑎 ∈ ℕ ∧ ( 𝑛 ∈ ℕ0 ∧ ( 2 ↑ 𝑛 ) ∥ 𝑎 ) ) → 𝑛 ∈ ℕ0 )
29 28 nn0red ⊢ ( ( 𝑎 ∈ ℕ ∧ ( 𝑛 ∈ ℕ0 ∧ ( 2 ↑ 𝑛 ) ∥ 𝑎 ) ) → 𝑛 ∈ ℝ )
30 3 a1i ⊢ ( ( 𝑎 ∈ ℕ ∧ ( 𝑛 ∈ ℕ0 ∧ ( 2 ↑ 𝑛 ) ∥ 𝑎 ) ) → 2 ∈ ℕ )
31 30 28 nnexpcld ⊢ ( ( 𝑎 ∈ ℕ ∧ ( 𝑛 ∈ ℕ0 ∧ ( 2 ↑ 𝑛 ) ∥ 𝑎 ) ) → ( 2 ↑ 𝑛 ) ∈ ℕ )
32 31 nnred ⊢ ( ( 𝑎 ∈ ℕ ∧ ( 𝑛 ∈ ℕ0 ∧ ( 2 ↑ 𝑛 ) ∥ 𝑎 ) ) → ( 2 ↑ 𝑛 ) ∈ ℝ )
33 simpl ⊢ ( ( 𝑎 ∈ ℕ ∧ ( 𝑛 ∈ ℕ0 ∧ ( 2 ↑ 𝑛 ) ∥ 𝑎 ) ) → 𝑎 ∈ ℕ )
34 33 nnred ⊢ ( ( 𝑎 ∈ ℕ ∧ ( 𝑛 ∈ ℕ0 ∧ ( 2 ↑ 𝑛 ) ∥ 𝑎 ) ) → 𝑎 ∈ ℝ )
35 2re ⊢ 2 ∈ ℝ
36 35 leidi ⊢ 2 ≤ 2
37 nexple ⊢ ( ( 𝑛 ∈ ℕ0 ∧ 2 ∈ ℝ ∧ 2 ≤ 2 ) → 𝑛 ≤ ( 2 ↑ 𝑛 ) )
38 35 36 37 mp3an23 ⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ≤ ( 2 ↑ 𝑛 ) )
39 38 ad2antrl ⊢ ( ( 𝑎 ∈ ℕ ∧ ( 𝑛 ∈ ℕ0 ∧ ( 2 ↑ 𝑛 ) ∥ 𝑎 ) ) → 𝑛 ≤ ( 2 ↑ 𝑛 ) )
40 31 nnzd ⊢ ( ( 𝑎 ∈ ℕ ∧ ( 𝑛 ∈ ℕ0 ∧ ( 2 ↑ 𝑛 ) ∥ 𝑎 ) ) → ( 2 ↑ 𝑛 ) ∈ ℤ )
41 simprr ⊢ ( ( 𝑎 ∈ ℕ ∧ ( 𝑛 ∈ ℕ0 ∧ ( 2 ↑ 𝑛 ) ∥ 𝑎 ) ) → ( 2 ↑ 𝑛 ) ∥ 𝑎 )
42 dvdsle ⊢ ( ( ( 2 ↑ 𝑛 ) ∈ ℤ ∧ 𝑎 ∈ ℕ ) → ( ( 2 ↑ 𝑛 ) ∥ 𝑎 → ( 2 ↑ 𝑛 ) ≤ 𝑎 ) )
43 42 imp ⊢ ( ( ( ( 2 ↑ 𝑛 ) ∈ ℤ ∧ 𝑎 ∈ ℕ ) ∧ ( 2 ↑ 𝑛 ) ∥ 𝑎 ) → ( 2 ↑ 𝑛 ) ≤ 𝑎 )
44 40 33 41 43 syl21anc ⊢ ( ( 𝑎 ∈ ℕ ∧ ( 𝑛 ∈ ℕ0 ∧ ( 2 ↑ 𝑛 ) ∥ 𝑎 ) ) → ( 2 ↑ 𝑛 ) ≤ 𝑎 )
45 29 32 34 39 44 letrd ⊢ ( ( 𝑎 ∈ ℕ ∧ ( 𝑛 ∈ ℕ0 ∧ ( 2 ↑ 𝑛 ) ∥ 𝑎 ) ) → 𝑛 ≤ 𝑎 )
46 27 45 sylan2b ⊢ ( ( 𝑎 ∈ ℕ ∧ 𝑛 ∈ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } ) → 𝑛 ≤ 𝑎 )
47 46 ralrimiva ⊢ ( 𝑎 ∈ ℕ → ∀ 𝑛 ∈ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } 𝑛 ≤ 𝑎 )
48 brralrspcev ⊢ ( ( 𝑎 ∈ ℤ ∧ ∀ 𝑛 ∈ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } 𝑛 ≤ 𝑎 ) → ∃ 𝑚 ∈ ℤ ∀ 𝑛 ∈ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } 𝑛 ≤ 𝑚 )
49 24 47 48 syl2anc ⊢ ( 𝑎 ∈ ℕ → ∃ 𝑚 ∈ ℤ ∀ 𝑛 ∈ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } 𝑛 ≤ 𝑚 )
50 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
51 50 uzsupss ⊢ ( ( 0 ∈ ℤ ∧ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } ⊆ ℕ0 ∧ ∃ 𝑚 ∈ ℤ ∀ 𝑛 ∈ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } 𝑛 ≤ 𝑚 ) → ∃ 𝑚 ∈ ℕ0 ( ∀ 𝑛 ∈ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } ¬ 𝑚 < 𝑛 ∧ ∀ 𝑛 ∈ ℕ0 ( 𝑛 < 𝑚 → ∃ 𝑜 ∈ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } 𝑛 < 𝑜 ) ) )
52 21 23 49 51 syl3anc ⊢ ( 𝑎 ∈ ℕ → ∃ 𝑚 ∈ ℕ0 ( ∀ 𝑛 ∈ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } ¬ 𝑚 < 𝑛 ∧ ∀ 𝑛 ∈ ℕ0 ( 𝑛 < 𝑚 → ∃ 𝑜 ∈ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } 𝑛 < 𝑜 ) ) )
53 20 52 supcl ⊢ ( 𝑎 ∈ ℕ → sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ∈ ℕ0 )
54 15 53 nnexpcld ⊢ ( 𝑎 ∈ ℕ → ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ∈ ℕ )
55 fzfi ⊢ ( 0 ... 𝑎 ) ∈ Fin
56 0zd ⊢ ( ( 𝑎 ∈ ℕ ∧ 𝑛 ∈ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } ) → 0 ∈ ℤ )
57 24 adantr ⊢ ( ( 𝑎 ∈ ℕ ∧ 𝑛 ∈ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } ) → 𝑎 ∈ ℤ )
58 27 28 sylan2b ⊢ ( ( 𝑎 ∈ ℕ ∧ 𝑛 ∈ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } ) → 𝑛 ∈ ℕ0 )
59 58 nn0zd ⊢ ( ( 𝑎 ∈ ℕ ∧ 𝑛 ∈ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } ) → 𝑛 ∈ ℤ )
60 58 nn0ge0d ⊢ ( ( 𝑎 ∈ ℕ ∧ 𝑛 ∈ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } ) → 0 ≤ 𝑛 )
61 56 57 59 60 46 elfzd ⊢ ( ( 𝑎 ∈ ℕ ∧ 𝑛 ∈ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } ) → 𝑛 ∈ ( 0 ... 𝑎 ) )
62 61 ex ⊢ ( 𝑎 ∈ ℕ → ( 𝑛 ∈ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } → 𝑛 ∈ ( 0 ... 𝑎 ) ) )
63 62 ssrdv ⊢ ( 𝑎 ∈ ℕ → { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } ⊆ ( 0 ... 𝑎 ) )
64 ssfi ⊢ ( ( ( 0 ... 𝑎 ) ∈ Fin ∧ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } ⊆ ( 0 ... 𝑎 ) ) → { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } ∈ Fin )
65 55 63 64 sylancr ⊢ ( 𝑎 ∈ ℕ → { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } ∈ Fin )
66 0nn0 ⊢ 0 ∈ ℕ0
67 66 a1i ⊢ ( 𝑎 ∈ ℕ → 0 ∈ ℕ0 )
68 2cn ⊢ 2 ∈ ℂ
69 exp0 ⊢ ( 2 ∈ ℂ → ( 2 ↑ 0 ) = 1 )
70 68 69 ax-mp ⊢ ( 2 ↑ 0 ) = 1
71 1dvds ⊢ ( 𝑎 ∈ ℤ → 1 ∥ 𝑎 )
72 24 71 syl ⊢ ( 𝑎 ∈ ℕ → 1 ∥ 𝑎 )
73 70 72 eqbrtrid ⊢ ( 𝑎 ∈ ℕ → ( 2 ↑ 0 ) ∥ 𝑎 )
74 oveq2 ⊢ ( 𝑘 = 0 → ( 2 ↑ 𝑘 ) = ( 2 ↑ 0 ) )
75 74 breq1d ⊢ ( 𝑘 = 0 → ( ( 2 ↑ 𝑘 ) ∥ 𝑎 ↔ ( 2 ↑ 0 ) ∥ 𝑎 ) )
76 75 elrab ⊢ ( 0 ∈ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } ↔ ( 0 ∈ ℕ0 ∧ ( 2 ↑ 0 ) ∥ 𝑎 ) )
77 67 73 76 sylanbrc ⊢ ( 𝑎 ∈ ℕ → 0 ∈ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } )
78 77 ne0d ⊢ ( 𝑎 ∈ ℕ → { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } ≠ ∅ )
79 fisupcl ⊢ ( ( < Or ℕ0 ∧ ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } ∈ Fin ∧ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } ≠ ∅ ∧ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } ⊆ ℕ0 ) ) → sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ∈ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } )
80 20 65 78 23 79 syl13anc ⊢ ( 𝑎 ∈ ℕ → sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ∈ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } )
81 oveq2 ⊢ ( 𝑘 = 𝑙 → ( 2 ↑ 𝑘 ) = ( 2 ↑ 𝑙 ) )
82 81 breq1d ⊢ ( 𝑘 = 𝑙 → ( ( 2 ↑ 𝑘 ) ∥ 𝑎 ↔ ( 2 ↑ 𝑙 ) ∥ 𝑎 ) )
83 82 cbvrabv ⊢ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } = { 𝑙 ∈ ℕ0 ∣ ( 2 ↑ 𝑙 ) ∥ 𝑎 }
84 80 83 eleqtrdi ⊢ ( 𝑎 ∈ ℕ → sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ∈ { 𝑙 ∈ ℕ0 ∣ ( 2 ↑ 𝑙 ) ∥ 𝑎 } )
85 oveq2 ⊢ ( 𝑙 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) → ( 2 ↑ 𝑙 ) = ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) )
86 85 breq1d ⊢ ( 𝑙 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) → ( ( 2 ↑ 𝑙 ) ∥ 𝑎 ↔ ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ∥ 𝑎 ) )
87 86 elrab ⊢ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ∈ { 𝑙 ∈ ℕ0 ∣ ( 2 ↑ 𝑙 ) ∥ 𝑎 } ↔ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ∈ ℕ0 ∧ ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ∥ 𝑎 ) )
88 84 87 sylib ⊢ ( 𝑎 ∈ ℕ → ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ∈ ℕ0 ∧ ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ∥ 𝑎 ) )
89 88 simprd ⊢ ( 𝑎 ∈ ℕ → ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ∥ 𝑎 )
90 nndivdvds ⊢ ( ( 𝑎 ∈ ℕ ∧ ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ∈ ℕ ) → ( ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ∥ 𝑎 ↔ ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∈ ℕ ) )
91 90 biimpa ⊢ ( ( ( 𝑎 ∈ ℕ ∧ ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ∈ ℕ ) ∧ ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ∥ 𝑎 ) → ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∈ ℕ )
92 14 54 89 91 syl21anc ⊢ ( 𝑎 ∈ ℕ → ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∈ ℕ )
93 1nn0 ⊢ 1 ∈ ℕ0
94 93 a1i ⊢ ( 𝑎 ∈ ℕ → 1 ∈ ℕ0 )
95 53 94 nn0addcld ⊢ ( 𝑎 ∈ ℕ → ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) + 1 ) ∈ ℕ0 )
96 53 nn0red ⊢ ( 𝑎 ∈ ℕ → sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ∈ ℝ )
97 96 ltp1d ⊢ ( 𝑎 ∈ ℕ → sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) < ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) + 1 ) )
98 20 52 supub ⊢ ( 𝑎 ∈ ℕ → ( ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) + 1 ) ∈ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } → ¬ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) < ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) + 1 ) ) )
99 97 98 mt2d ⊢ ( 𝑎 ∈ ℕ → ¬ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) + 1 ) ∈ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } )
100 83 eleq2i ⊢ ( ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) + 1 ) ∈ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } ↔ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) + 1 ) ∈ { 𝑙 ∈ ℕ0 ∣ ( 2 ↑ 𝑙 ) ∥ 𝑎 } )
101 99 100 sylnib ⊢ ( 𝑎 ∈ ℕ → ¬ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) + 1 ) ∈ { 𝑙 ∈ ℕ0 ∣ ( 2 ↑ 𝑙 ) ∥ 𝑎 } )
102 oveq2 ⊢ ( 𝑙 = ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) + 1 ) → ( 2 ↑ 𝑙 ) = ( 2 ↑ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) + 1 ) ) )
103 102 breq1d ⊢ ( 𝑙 = ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) + 1 ) → ( ( 2 ↑ 𝑙 ) ∥ 𝑎 ↔ ( 2 ↑ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) + 1 ) ) ∥ 𝑎 ) )
104 103 elrab ⊢ ( ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) + 1 ) ∈ { 𝑙 ∈ ℕ0 ∣ ( 2 ↑ 𝑙 ) ∥ 𝑎 } ↔ ( ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) + 1 ) ∈ ℕ0 ∧ ( 2 ↑ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) + 1 ) ) ∥ 𝑎 ) )
105 101 104 sylnib ⊢ ( 𝑎 ∈ ℕ → ¬ ( ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) + 1 ) ∈ ℕ0 ∧ ( 2 ↑ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) + 1 ) ) ∥ 𝑎 ) )
106 imnan ⊢ ( ( ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) + 1 ) ∈ ℕ0 → ¬ ( 2 ↑ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) + 1 ) ) ∥ 𝑎 ) ↔ ¬ ( ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) + 1 ) ∈ ℕ0 ∧ ( 2 ↑ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) + 1 ) ) ∥ 𝑎 ) )
107 105 106 sylibr ⊢ ( 𝑎 ∈ ℕ → ( ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) + 1 ) ∈ ℕ0 → ¬ ( 2 ↑ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) + 1 ) ) ∥ 𝑎 ) )
108 95 107 mpd ⊢ ( 𝑎 ∈ ℕ → ¬ ( 2 ↑ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) + 1 ) ) ∥ 𝑎 )
109 expp1 ⊢ ( ( 2 ∈ ℂ ∧ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ∈ ℕ0 ) → ( 2 ↑ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) + 1 ) ) = ( ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) · 2 ) )
110 68 53 109 sylancr ⊢ ( 𝑎 ∈ ℕ → ( 2 ↑ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) + 1 ) ) = ( ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) · 2 ) )
111 110 breq1d ⊢ ( 𝑎 ∈ ℕ → ( ( 2 ↑ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) + 1 ) ) ∥ 𝑎 ↔ ( ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) · 2 ) ∥ 𝑎 ) )
112 108 111 mtbid ⊢ ( 𝑎 ∈ ℕ → ¬ ( ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) · 2 ) ∥ 𝑎 )
113 nncn ⊢ ( 𝑎 ∈ ℕ → 𝑎 ∈ ℂ )
114 54 nncnd ⊢ ( 𝑎 ∈ ℕ → ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ∈ ℂ )
115 54 nnne0d ⊢ ( 𝑎 ∈ ℕ → ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ≠ 0 )
116 113 114 115 divcan2d ⊢ ( 𝑎 ∈ ℕ → ( ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) · ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ) = 𝑎 )
117 116 eqcomd ⊢ ( 𝑎 ∈ ℕ → 𝑎 = ( ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) · ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ) )
118 117 breq2d ⊢ ( 𝑎 ∈ ℕ → ( ( ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) · 2 ) ∥ 𝑎 ↔ ( ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) · 2 ) ∥ ( ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) · ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ) ) )
119 15 nnzd ⊢ ( 𝑎 ∈ ℕ → 2 ∈ ℤ )
120 92 nnzd ⊢ ( 𝑎 ∈ ℕ → ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∈ ℤ )
121 54 nnzd ⊢ ( 𝑎 ∈ ℕ → ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ∈ ℤ )
122 dvdscmulr ⊢ ( ( 2 ∈ ℤ ∧ ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∈ ℤ ∧ ( ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ∈ ℤ ∧ ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ≠ 0 ) ) → ( ( ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) · 2 ) ∥ ( ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) · ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ) ↔ 2 ∥ ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ) )
123 119 120 121 115 122 syl112anc ⊢ ( 𝑎 ∈ ℕ → ( ( ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) · 2 ) ∥ ( ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) · ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ) ↔ 2 ∥ ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ) )
124 118 123 bitrd ⊢ ( 𝑎 ∈ ℕ → ( ( ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) · 2 ) ∥ 𝑎 ↔ 2 ∥ ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ) )
125 112 124 mtbid ⊢ ( 𝑎 ∈ ℕ → ¬ 2 ∥ ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) )
126 breq2 ⊢ ( 𝑧 = ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) → ( 2 ∥ 𝑧 ↔ 2 ∥ ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ) )
127 126 notbid ⊢ ( 𝑧 = ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) → ( ¬ 2 ∥ 𝑧 ↔ ¬ 2 ∥ ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ) )
128 127 1 elrab2 ⊢ ( ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∈ 𝐽 ↔ ( ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∈ ℕ ∧ ¬ 2 ∥ ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ) )
129 92 125 128 sylanbrc ⊢ ( 𝑎 ∈ ℕ → ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∈ 𝐽 )
130 129 53 jca ⊢ ( 𝑎 ∈ ℕ → ( ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∈ 𝐽 ∧ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ∈ ℕ0 ) )
131 130 adantl ⊢ ( ( ⊤ ∧ 𝑎 ∈ ℕ ) → ( ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∈ 𝐽 ∧ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ∈ ℕ0 ) )
132 simpr ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) )
133 3 a1i ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → 2 ∈ ℕ )
134 simplr ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → 𝑦 ∈ ℕ0 )
135 133 134 nnexpcld ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → ( 2 ↑ 𝑦 ) ∈ ℕ )
136 8 sseli ⊢ ( 𝑥 ∈ 𝐽 → 𝑥 ∈ ℕ )
137 136 ad2antrr ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → 𝑥 ∈ ℕ )
138 135 137 nnmulcld ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → ( ( 2 ↑ 𝑦 ) · 𝑥 ) ∈ ℕ )
139 132 138 eqeltrd ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → 𝑎 ∈ ℕ )
140 simplll ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → 𝑥 ∈ 𝐽 )
141 breq2 ⊢ ( 𝑧 = 𝑥 → ( 2 ∥ 𝑧 ↔ 2 ∥ 𝑥 ) )
142 141 notbid ⊢ ( 𝑧 = 𝑥 → ( ¬ 2 ∥ 𝑧 ↔ ¬ 2 ∥ 𝑥 ) )
143 142 1 elrab2 ⊢ ( 𝑥 ∈ 𝐽 ↔ ( 𝑥 ∈ ℕ ∧ ¬ 2 ∥ 𝑥 ) )
144 143 simprbi ⊢ ( 𝑥 ∈ 𝐽 → ¬ 2 ∥ 𝑥 )
145 2z ⊢ 2 ∈ ℤ
146 134 adantr ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → 𝑦 ∈ ℕ0 )
147 146 nn0zd ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → 𝑦 ∈ ℤ )
148 19 a1i ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → < Or ℕ0 )
149 139 52 syl ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → ∃ 𝑚 ∈ ℕ0 ( ∀ 𝑛 ∈ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } ¬ 𝑚 < 𝑛 ∧ ∀ 𝑛 ∈ ℕ0 ( 𝑛 < 𝑚 → ∃ 𝑜 ∈ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } 𝑛 < 𝑜 ) ) )
150 149 adantr ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → ∃ 𝑚 ∈ ℕ0 ( ∀ 𝑛 ∈ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } ¬ 𝑚 < 𝑛 ∧ ∀ 𝑛 ∈ ℕ0 ( 𝑛 < 𝑚 → ∃ 𝑜 ∈ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } 𝑛 < 𝑜 ) ) )
151 148 150 supcl ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ∈ ℕ0 )
152 151 nn0zd ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ∈ ℤ )
153 simpr ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) )
154 znnsub ⊢ ( ( 𝑦 ∈ ℤ ∧ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ∈ ℤ ) → ( 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ↔ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) − 𝑦 ) ∈ ℕ ) )
155 154 biimpa ⊢ ( ( ( 𝑦 ∈ ℤ ∧ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ∈ ℤ ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) − 𝑦 ) ∈ ℕ )
156 147 152 153 155 syl21anc ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) − 𝑦 ) ∈ ℕ )
157 iddvdsexp ⊢ ( ( 2 ∈ ℤ ∧ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) − 𝑦 ) ∈ ℕ ) → 2 ∥ ( 2 ↑ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) − 𝑦 ) ) )
158 145 156 157 sylancr ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → 2 ∥ ( 2 ↑ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) − 𝑦 ) ) )
159 145 a1i ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → 2 ∈ ℤ )
160 139 120 syl ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∈ ℤ )
161 160 adantr ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∈ ℤ )
162 156 nnnn0d ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) − 𝑦 ) ∈ ℕ0 )
163 zexpcl ⊢ ( ( 2 ∈ ℤ ∧ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) − 𝑦 ) ∈ ℕ0 ) → ( 2 ↑ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) − 𝑦 ) ) ∈ ℤ )
164 145 162 163 sylancr ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → ( 2 ↑ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) − 𝑦 ) ) ∈ ℤ )
165 dvdsmultr2 ⊢ ( ( 2 ∈ ℤ ∧ ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∈ ℤ ∧ ( 2 ↑ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) − 𝑦 ) ) ∈ ℤ ) → ( 2 ∥ ( 2 ↑ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) − 𝑦 ) ) → 2 ∥ ( ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) · ( 2 ↑ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) − 𝑦 ) ) ) ) )
166 159 161 164 165 syl3anc ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → ( 2 ∥ ( 2 ↑ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) − 𝑦 ) ) → 2 ∥ ( ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) · ( 2 ↑ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) − 𝑦 ) ) ) ) )
167 158 166 mpd ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → 2 ∥ ( ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) · ( 2 ↑ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) − 𝑦 ) ) ) )
168 137 adantr ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → 𝑥 ∈ ℕ )
169 168 nncnd ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → 𝑥 ∈ ℂ )
170 2cnd ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → 2 ∈ ℂ )
171 170 162 expcld ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → ( 2 ↑ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) − 𝑦 ) ) ∈ ℂ )
172 139 adantr ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → 𝑎 ∈ ℕ )
173 172 nncnd ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → 𝑎 ∈ ℂ )
174 172 114 syl ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ∈ ℂ )
175 2ne0 ⊢ 2 ≠ 0
176 175 a1i ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → 2 ≠ 0 )
177 170 176 152 expne0d ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ≠ 0 )
178 173 174 177 divcld ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∈ ℂ )
179 171 178 mulcld ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → ( ( 2 ↑ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) − 𝑦 ) ) · ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ) ∈ ℂ )
180 170 146 expcld ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → ( 2 ↑ 𝑦 ) ∈ ℂ )
181 170 176 147 expne0d ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → ( 2 ↑ 𝑦 ) ≠ 0 )
182 172 117 syl ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → 𝑎 = ( ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) · ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ) )
183 simplr ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) )
184 146 nn0cnd ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → 𝑦 ∈ ℂ )
185 151 nn0cnd ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ∈ ℂ )
186 184 185 pncan3d ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → ( 𝑦 + ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) − 𝑦 ) ) = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) )
187 186 oveq2d ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → ( 2 ↑ ( 𝑦 + ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) − 𝑦 ) ) ) = ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) )
188 170 162 146 expaddd ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → ( 2 ↑ ( 𝑦 + ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) − 𝑦 ) ) ) = ( ( 2 ↑ 𝑦 ) · ( 2 ↑ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) − 𝑦 ) ) ) )
189 187 188 eqtr3d ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) = ( ( 2 ↑ 𝑦 ) · ( 2 ↑ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) − 𝑦 ) ) ) )
190 189 oveq1d ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → ( ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) · ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ) = ( ( ( 2 ↑ 𝑦 ) · ( 2 ↑ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) − 𝑦 ) ) ) · ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ) )
191 182 183 190 3eqtr3d ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → ( ( 2 ↑ 𝑦 ) · 𝑥 ) = ( ( ( 2 ↑ 𝑦 ) · ( 2 ↑ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) − 𝑦 ) ) ) · ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ) )
192 180 171 178 mulassd ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → ( ( ( 2 ↑ 𝑦 ) · ( 2 ↑ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) − 𝑦 ) ) ) · ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ) = ( ( 2 ↑ 𝑦 ) · ( ( 2 ↑ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) − 𝑦 ) ) · ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ) ) )
193 191 192 eqtrd ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → ( ( 2 ↑ 𝑦 ) · 𝑥 ) = ( ( 2 ↑ 𝑦 ) · ( ( 2 ↑ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) − 𝑦 ) ) · ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ) ) )
194 169 179 180 181 193 mulcanad ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → 𝑥 = ( ( 2 ↑ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) − 𝑦 ) ) · ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ) )
195 178 171 mulcomd ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → ( ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) · ( 2 ↑ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) − 𝑦 ) ) ) = ( ( 2 ↑ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) − 𝑦 ) ) · ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ) )
196 194 195 eqtr4d ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → 𝑥 = ( ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) · ( 2 ↑ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) − 𝑦 ) ) ) )
197 167 196 breqtrrd ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → 2 ∥ 𝑥 )
198 144 197 nsyl3 ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → ¬ 𝑥 ∈ 𝐽 )
199 140 198 pm2.65da ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → ¬ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) )
200 137 nnzd ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → 𝑥 ∈ ℤ )
201 135 nnzd ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → ( 2 ↑ 𝑦 ) ∈ ℤ )
202 139 nnzd ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → 𝑎 ∈ ℤ )
203 135 nncnd ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → ( 2 ↑ 𝑦 ) ∈ ℂ )
204 137 nncnd ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → 𝑥 ∈ ℂ )
205 203 204 mulcomd ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → ( ( 2 ↑ 𝑦 ) · 𝑥 ) = ( 𝑥 · ( 2 ↑ 𝑦 ) ) )
206 132 205 eqtr2d ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → ( 𝑥 · ( 2 ↑ 𝑦 ) ) = 𝑎 )
207 dvds0lem ⊢ ( ( ( 𝑥 ∈ ℤ ∧ ( 2 ↑ 𝑦 ) ∈ ℤ ∧ 𝑎 ∈ ℤ ) ∧ ( 𝑥 · ( 2 ↑ 𝑦 ) ) = 𝑎 ) → ( 2 ↑ 𝑦 ) ∥ 𝑎 )
208 200 201 202 206 207 syl31anc ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → ( 2 ↑ 𝑦 ) ∥ 𝑎 )
209 oveq2 ⊢ ( 𝑘 = 𝑦 → ( 2 ↑ 𝑘 ) = ( 2 ↑ 𝑦 ) )
210 209 breq1d ⊢ ( 𝑘 = 𝑦 → ( ( 2 ↑ 𝑘 ) ∥ 𝑎 ↔ ( 2 ↑ 𝑦 ) ∥ 𝑎 ) )
211 210 elrab ⊢ ( 𝑦 ∈ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } ↔ ( 𝑦 ∈ ℕ0 ∧ ( 2 ↑ 𝑦 ) ∥ 𝑎 ) )
212 134 208 211 sylanbrc ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → 𝑦 ∈ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } )
213 19 a1i ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → < Or ℕ0 )
214 213 149 supub ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → ( 𝑦 ∈ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } → ¬ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) < 𝑦 ) )
215 212 214 mpd ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → ¬ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) < 𝑦 )
216 134 nn0red ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → 𝑦 ∈ ℝ )
217 139 96 syl ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ∈ ℝ )
218 216 217 lttri3d ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → ( 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ↔ ( ¬ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ∧ ¬ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) < 𝑦 ) ) )
219 199 215 218 mpbir2and ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) )
220 simplr ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) )
221 139 adantr ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → 𝑎 ∈ ℕ )
222 221 nncnd ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → 𝑎 ∈ ℂ )
223 137 adantr ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → 𝑥 ∈ ℕ )
224 223 nncnd ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → 𝑥 ∈ ℂ )
225 nnexpcl ⊢ ( ( 2 ∈ ℕ ∧ 𝑦 ∈ ℕ0 ) → ( 2 ↑ 𝑦 ) ∈ ℕ )
226 3 225 mpan ⊢ ( 𝑦 ∈ ℕ0 → ( 2 ↑ 𝑦 ) ∈ ℕ )
227 226 nncnd ⊢ ( 𝑦 ∈ ℕ0 → ( 2 ↑ 𝑦 ) ∈ ℂ )
228 226 nnne0d ⊢ ( 𝑦 ∈ ℕ0 → ( 2 ↑ 𝑦 ) ≠ 0 )
229 227 228 jca ⊢ ( 𝑦 ∈ ℕ0 → ( ( 2 ↑ 𝑦 ) ∈ ℂ ∧ ( 2 ↑ 𝑦 ) ≠ 0 ) )
230 229 ad3antlr ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → ( ( 2 ↑ 𝑦 ) ∈ ℂ ∧ ( 2 ↑ 𝑦 ) ≠ 0 ) )
231 divmul2 ⊢ ( ( 𝑎 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ ( ( 2 ↑ 𝑦 ) ∈ ℂ ∧ ( 2 ↑ 𝑦 ) ≠ 0 ) ) → ( ( 𝑎 / ( 2 ↑ 𝑦 ) ) = 𝑥 ↔ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) )
232 222 224 230 231 syl3anc ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → ( ( 𝑎 / ( 2 ↑ 𝑦 ) ) = 𝑥 ↔ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) )
233 220 232 mpbird ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → ( 𝑎 / ( 2 ↑ 𝑦 ) ) = 𝑥 )
234 simpr ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) )
235 234 oveq2d ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → ( 2 ↑ 𝑦 ) = ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) )
236 235 oveq2d ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → ( 𝑎 / ( 2 ↑ 𝑦 ) ) = ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) )
237 233 236 eqtr3d ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → 𝑥 = ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) )
238 237 ex ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → ( 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) → 𝑥 = ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ) )
239 219 238 jcai ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → ( 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ∧ 𝑥 = ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ) )
240 239 ancomd ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → ( 𝑥 = ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∧ 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) )
241 139 240 jca ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → ( 𝑎 ∈ ℕ ∧ ( 𝑥 = ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∧ 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) )
242 simprl ⊢ ( ( 𝑎 ∈ ℕ ∧ ( 𝑥 = ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∧ 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) → 𝑥 = ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) )
243 129 adantr ⊢ ( ( 𝑎 ∈ ℕ ∧ ( 𝑥 = ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∧ 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) → ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∈ 𝐽 )
244 242 243 eqeltrd ⊢ ( ( 𝑎 ∈ ℕ ∧ ( 𝑥 = ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∧ 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) → 𝑥 ∈ 𝐽 )
245 simprr ⊢ ( ( 𝑎 ∈ ℕ ∧ ( 𝑥 = ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∧ 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) → 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) )
246 53 adantr ⊢ ( ( 𝑎 ∈ ℕ ∧ ( 𝑥 = ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∧ 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) → sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ∈ ℕ0 )
247 245 246 eqeltrd ⊢ ( ( 𝑎 ∈ ℕ ∧ ( 𝑥 = ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∧ 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) → 𝑦 ∈ ℕ0 )
248 117 adantr ⊢ ( ( 𝑎 ∈ ℕ ∧ ( 𝑥 = ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∧ 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) → 𝑎 = ( ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) · ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ) )
249 245 oveq2d ⊢ ( ( 𝑎 ∈ ℕ ∧ ( 𝑥 = ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∧ 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) → ( 2 ↑ 𝑦 ) = ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) )
250 249 242 oveq12d ⊢ ( ( 𝑎 ∈ ℕ ∧ ( 𝑥 = ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∧ 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) → ( ( 2 ↑ 𝑦 ) · 𝑥 ) = ( ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) · ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ) )
251 248 250 eqtr4d ⊢ ( ( 𝑎 ∈ ℕ ∧ ( 𝑥 = ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∧ 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) → 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) )
252 244 247 251 jca31 ⊢ ( ( 𝑎 ∈ ℕ ∧ ( 𝑥 = ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∧ 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) → ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) )
253 241 252 impbii ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ↔ ( 𝑎 ∈ ℕ ∧ ( 𝑥 = ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∧ 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) )
254 253 a1i ⊢ ( ⊤ → ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ↔ ( 𝑎 ∈ ℕ ∧ ( 𝑥 = ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∧ 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ) )
255 2 13 131 254 f1od2 ⊢ ( ⊤ → 𝐹 : ( 𝐽 × ℕ0 ) –1-1-onto→ ℕ )
256 255 mptru ⊢ 𝐹 : ( 𝐽 × ℕ0 ) –1-1-onto→ ℕ