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 sseldi ⊢ ( ( 𝑦 ∈ ℕ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 elfz4 ⊢ ( ( ( 0 ∈ ℤ ∧ 𝑎 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ ( 0 ≤ 𝑛 ∧ 𝑛 ≤ 𝑎 ) ) → 𝑛 ∈ ( 0 ... 𝑎 ) )
62 56 57 59 60 46 61 syl32anc ⊢ ( ( 𝑎 ∈ ℕ ∧ 𝑛 ∈ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } ) → 𝑛 ∈ ( 0 ... 𝑎 ) )
63 62 ex ⊢ ( 𝑎 ∈ ℕ → ( 𝑛 ∈ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } → 𝑛 ∈ ( 0 ... 𝑎 ) ) )
64 63 ssrdv ⊢ ( 𝑎 ∈ ℕ → { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } ⊆ ( 0 ... 𝑎 ) )
65 ssfi ⊢ ( ( ( 0 ... 𝑎 ) ∈ Fin ∧ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } ⊆ ( 0 ... 𝑎 ) ) → { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } ∈ Fin )
66 55 64 65 sylancr ⊢ ( 𝑎 ∈ ℕ → { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } ∈ Fin )
67 0nn0 ⊢ 0 ∈ ℕ0
68 67 a1i ⊢ ( 𝑎 ∈ ℕ → 0 ∈ ℕ0 )
69 2cn ⊢ 2 ∈ ℂ
70 exp0 ⊢ ( 2 ∈ ℂ → ( 2 ↑ 0 ) = 1 )
71 69 70 ax-mp ⊢ ( 2 ↑ 0 ) = 1
72 1dvds ⊢ ( 𝑎 ∈ ℤ → 1 ∥ 𝑎 )
73 24 72 syl ⊢ ( 𝑎 ∈ ℕ → 1 ∥ 𝑎 )
74 71 73 eqbrtrid ⊢ ( 𝑎 ∈ ℕ → ( 2 ↑ 0 ) ∥ 𝑎 )
75 oveq2 ⊢ ( 𝑘 = 0 → ( 2 ↑ 𝑘 ) = ( 2 ↑ 0 ) )
76 75 breq1d ⊢ ( 𝑘 = 0 → ( ( 2 ↑ 𝑘 ) ∥ 𝑎 ↔ ( 2 ↑ 0 ) ∥ 𝑎 ) )
77 76 elrab ⊢ ( 0 ∈ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } ↔ ( 0 ∈ ℕ0 ∧ ( 2 ↑ 0 ) ∥ 𝑎 ) )
78 68 74 77 sylanbrc ⊢ ( 𝑎 ∈ ℕ → 0 ∈ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } )
79 78 ne0d ⊢ ( 𝑎 ∈ ℕ → { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } ≠ ∅ )
80 fisupcl ⊢ ( ( < Or ℕ0 ∧ ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } ∈ Fin ∧ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } ≠ ∅ ∧ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } ⊆ ℕ0 ) ) → sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ∈ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } )
81 20 66 79 23 80 syl13anc ⊢ ( 𝑎 ∈ ℕ → sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ∈ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } )
82 oveq2 ⊢ ( 𝑘 = 𝑙 → ( 2 ↑ 𝑘 ) = ( 2 ↑ 𝑙 ) )
83 82 breq1d ⊢ ( 𝑘 = 𝑙 → ( ( 2 ↑ 𝑘 ) ∥ 𝑎 ↔ ( 2 ↑ 𝑙 ) ∥ 𝑎 ) )
84 83 cbvrabv ⊢ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } = { 𝑙 ∈ ℕ0 ∣ ( 2 ↑ 𝑙 ) ∥ 𝑎 }
85 81 84 eleqtrdi ⊢ ( 𝑎 ∈ ℕ → sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ∈ { 𝑙 ∈ ℕ0 ∣ ( 2 ↑ 𝑙 ) ∥ 𝑎 } )
86 oveq2 ⊢ ( 𝑙 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) → ( 2 ↑ 𝑙 ) = ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) )
87 86 breq1d ⊢ ( 𝑙 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) → ( ( 2 ↑ 𝑙 ) ∥ 𝑎 ↔ ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ∥ 𝑎 ) )
88 87 elrab ⊢ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ∈ { 𝑙 ∈ ℕ0 ∣ ( 2 ↑ 𝑙 ) ∥ 𝑎 } ↔ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ∈ ℕ0 ∧ ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ∥ 𝑎 ) )
89 85 88 sylib ⊢ ( 𝑎 ∈ ℕ → ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ∈ ℕ0 ∧ ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ∥ 𝑎 ) )
90 89 simprd ⊢ ( 𝑎 ∈ ℕ → ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ∥ 𝑎 )
91 nndivdvds ⊢ ( ( 𝑎 ∈ ℕ ∧ ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ∈ ℕ ) → ( ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ∥ 𝑎 ↔ ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∈ ℕ ) )
92 91 biimpa ⊢ ( ( ( 𝑎 ∈ ℕ ∧ ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ∈ ℕ ) ∧ ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ∥ 𝑎 ) → ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∈ ℕ )
93 14 54 90 92 syl21anc ⊢ ( 𝑎 ∈ ℕ → ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∈ ℕ )
94 1nn0 ⊢ 1 ∈ ℕ0
95 94 a1i ⊢ ( 𝑎 ∈ ℕ → 1 ∈ ℕ0 )
96 53 95 nn0addcld ⊢ ( 𝑎 ∈ ℕ → ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) + 1 ) ∈ ℕ0 )
97 53 nn0red ⊢ ( 𝑎 ∈ ℕ → sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ∈ ℝ )
98 97 ltp1d ⊢ ( 𝑎 ∈ ℕ → sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) < ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) + 1 ) )
99 20 52 supub ⊢ ( 𝑎 ∈ ℕ → ( ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) + 1 ) ∈ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } → ¬ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) < ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) + 1 ) ) )
100 98 99 mt2d ⊢ ( 𝑎 ∈ ℕ → ¬ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) + 1 ) ∈ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } )
101 84 eleq2i ⊢ ( ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) + 1 ) ∈ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } ↔ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) + 1 ) ∈ { 𝑙 ∈ ℕ0 ∣ ( 2 ↑ 𝑙 ) ∥ 𝑎 } )
102 100 101 sylnib ⊢ ( 𝑎 ∈ ℕ → ¬ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) + 1 ) ∈ { 𝑙 ∈ ℕ0 ∣ ( 2 ↑ 𝑙 ) ∥ 𝑎 } )
103 oveq2 ⊢ ( 𝑙 = ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) + 1 ) → ( 2 ↑ 𝑙 ) = ( 2 ↑ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) + 1 ) ) )
104 103 breq1d ⊢ ( 𝑙 = ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) + 1 ) → ( ( 2 ↑ 𝑙 ) ∥ 𝑎 ↔ ( 2 ↑ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) + 1 ) ) ∥ 𝑎 ) )
105 104 elrab ⊢ ( ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) + 1 ) ∈ { 𝑙 ∈ ℕ0 ∣ ( 2 ↑ 𝑙 ) ∥ 𝑎 } ↔ ( ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) + 1 ) ∈ ℕ0 ∧ ( 2 ↑ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) + 1 ) ) ∥ 𝑎 ) )
106 102 105 sylnib ⊢ ( 𝑎 ∈ ℕ → ¬ ( ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) + 1 ) ∈ ℕ0 ∧ ( 2 ↑ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) + 1 ) ) ∥ 𝑎 ) )
107 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 ) ) ∥ 𝑎 ) )
108 106 107 sylibr ⊢ ( 𝑎 ∈ ℕ → ( ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) + 1 ) ∈ ℕ0 → ¬ ( 2 ↑ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) + 1 ) ) ∥ 𝑎 ) )
109 96 108 mpd ⊢ ( 𝑎 ∈ ℕ → ¬ ( 2 ↑ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) + 1 ) ) ∥ 𝑎 )
110 expp1 ⊢ ( ( 2 ∈ ℂ ∧ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ∈ ℕ0 ) → ( 2 ↑ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) + 1 ) ) = ( ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) · 2 ) )
111 69 53 110 sylancr ⊢ ( 𝑎 ∈ ℕ → ( 2 ↑ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) + 1 ) ) = ( ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) · 2 ) )
112 111 breq1d ⊢ ( 𝑎 ∈ ℕ → ( ( 2 ↑ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) + 1 ) ) ∥ 𝑎 ↔ ( ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) · 2 ) ∥ 𝑎 ) )
113 109 112 mtbid ⊢ ( 𝑎 ∈ ℕ → ¬ ( ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) · 2 ) ∥ 𝑎 )
114 nncn ⊢ ( 𝑎 ∈ ℕ → 𝑎 ∈ ℂ )
115 54 nncnd ⊢ ( 𝑎 ∈ ℕ → ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ∈ ℂ )
116 54 nnne0d ⊢ ( 𝑎 ∈ ℕ → ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ≠ 0 )
117 114 115 116 divcan2d ⊢ ( 𝑎 ∈ ℕ → ( ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) · ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ) = 𝑎 )
118 117 eqcomd ⊢ ( 𝑎 ∈ ℕ → 𝑎 = ( ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) · ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ) )
119 118 breq2d ⊢ ( 𝑎 ∈ ℕ → ( ( ( 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 ⊢ ( 𝑎 ∈ ℕ → 2 ∈ ℤ )
121 93 nnzd ⊢ ( 𝑎 ∈ ℕ → ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∈ ℤ )
122 54 nnzd ⊢ ( 𝑎 ∈ ℕ → ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ∈ ℤ )
123 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 , < ) ) ) ) )
124 120 121 122 116 123 syl112anc ⊢ ( 𝑎 ∈ ℕ → ( ( ( 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 ⊢ ( 𝑎 ∈ ℕ → ( ( ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) · 2 ) ∥ 𝑎 ↔ 2 ∥ ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ) )
126 113 125 mtbid ⊢ ( 𝑎 ∈ ℕ → ¬ 2 ∥ ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) )
127 breq2 ⊢ ( 𝑧 = ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) → ( 2 ∥ 𝑧 ↔ 2 ∥ ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ) )
128 127 notbid ⊢ ( 𝑧 = ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) → ( ¬ 2 ∥ 𝑧 ↔ ¬ 2 ∥ ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ) )
129 128 1 elrab2 ⊢ ( ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∈ 𝐽 ↔ ( ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∈ ℕ ∧ ¬ 2 ∥ ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ) )
130 93 126 129 sylanbrc ⊢ ( 𝑎 ∈ ℕ → ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∈ 𝐽 )
131 130 53 jca ⊢ ( 𝑎 ∈ ℕ → ( ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∈ 𝐽 ∧ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ∈ ℕ0 ) )
132 131 adantl ⊢ ( ( ⊤ ∧ 𝑎 ∈ ℕ ) → ( ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∈ 𝐽 ∧ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ∈ ℕ0 ) )
133 simpr ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) )
134 3 a1i ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → 2 ∈ ℕ )
135 simplr ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → 𝑦 ∈ ℕ0 )
136 134 135 nnexpcld ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → ( 2 ↑ 𝑦 ) ∈ ℕ )
137 8 sseli ⊢ ( 𝑥 ∈ 𝐽 → 𝑥 ∈ ℕ )
138 137 ad2antrr ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → 𝑥 ∈ ℕ )
139 136 138 nnmulcld ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → ( ( 2 ↑ 𝑦 ) · 𝑥 ) ∈ ℕ )
140 133 139 eqeltrd ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → 𝑎 ∈ ℕ )
141 simplll ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → 𝑥 ∈ 𝐽 )
142 breq2 ⊢ ( 𝑧 = 𝑥 → ( 2 ∥ 𝑧 ↔ 2 ∥ 𝑥 ) )
143 142 notbid ⊢ ( 𝑧 = 𝑥 → ( ¬ 2 ∥ 𝑧 ↔ ¬ 2 ∥ 𝑥 ) )
144 143 1 elrab2 ⊢ ( 𝑥 ∈ 𝐽 ↔ ( 𝑥 ∈ ℕ ∧ ¬ 2 ∥ 𝑥 ) )
145 144 simprbi ⊢ ( 𝑥 ∈ 𝐽 → ¬ 2 ∥ 𝑥 )
146 2z ⊢ 2 ∈ ℤ
147 135 adantr ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → 𝑦 ∈ ℕ0 )
148 147 nn0zd ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → 𝑦 ∈ ℤ )
149 19 a1i ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → < Or ℕ0 )
150 140 52 syl ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → ∃ 𝑚 ∈ ℕ0 ( ∀ 𝑛 ∈ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } ¬ 𝑚 < 𝑛 ∧ ∀ 𝑛 ∈ ℕ0 ( 𝑛 < 𝑚 → ∃ 𝑜 ∈ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } 𝑛 < 𝑜 ) ) )
151 150 adantr ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → ∃ 𝑚 ∈ ℕ0 ( ∀ 𝑛 ∈ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } ¬ 𝑚 < 𝑛 ∧ ∀ 𝑛 ∈ ℕ0 ( 𝑛 < 𝑚 → ∃ 𝑜 ∈ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } 𝑛 < 𝑜 ) ) )
152 149 151 supcl ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ∈ ℕ0 )
153 152 nn0zd ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ∈ ℤ )
154 simpr ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) )
155 znnsub ⊢ ( ( 𝑦 ∈ ℤ ∧ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ∈ ℤ ) → ( 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ↔ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) − 𝑦 ) ∈ ℕ ) )
156 155 biimpa ⊢ ( ( ( 𝑦 ∈ ℤ ∧ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ∈ ℤ ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) − 𝑦 ) ∈ ℕ )
157 148 153 154 156 syl21anc ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) − 𝑦 ) ∈ ℕ )
158 iddvdsexp ⊢ ( ( 2 ∈ ℤ ∧ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) − 𝑦 ) ∈ ℕ ) → 2 ∥ ( 2 ↑ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) − 𝑦 ) ) )
159 146 157 158 sylancr ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → 2 ∥ ( 2 ↑ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) − 𝑦 ) ) )
160 146 a1i ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → 2 ∈ ℤ )
161 140 121 syl ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∈ ℤ )
162 161 adantr ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∈ ℤ )
163 157 nnnn0d ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) − 𝑦 ) ∈ ℕ0 )
164 zexpcl ⊢ ( ( 2 ∈ ℤ ∧ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) − 𝑦 ) ∈ ℕ0 ) → ( 2 ↑ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) − 𝑦 ) ) ∈ ℤ )
165 146 163 164 sylancr ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → ( 2 ↑ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) − 𝑦 ) ) ∈ ℤ )
166 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 , < ) − 𝑦 ) ) ) ) )
167 160 162 165 166 syl3anc ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ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 ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → 2 ∥ ( ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) · ( 2 ↑ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) − 𝑦 ) ) ) )
169 138 adantr ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → 𝑥 ∈ ℕ )
170 169 nncnd ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → 𝑥 ∈ ℂ )
171 2cnd ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → 2 ∈ ℂ )
172 171 163 expcld ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → ( 2 ↑ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) − 𝑦 ) ) ∈ ℂ )
173 140 adantr ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → 𝑎 ∈ ℕ )
174 173 nncnd ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → 𝑎 ∈ ℂ )
175 173 115 syl ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ∈ ℂ )
176 2ne0 ⊢ 2 ≠ 0
177 176 a1i ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → 2 ≠ 0 )
178 171 177 153 expne0d ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ≠ 0 )
179 174 175 178 divcld ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∈ ℂ )
180 172 179 mulcld ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → ( ( 2 ↑ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) − 𝑦 ) ) · ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ) ∈ ℂ )
181 171 147 expcld ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → ( 2 ↑ 𝑦 ) ∈ ℂ )
182 171 177 148 expne0d ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → ( 2 ↑ 𝑦 ) ≠ 0 )
183 173 118 syl ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → 𝑎 = ( ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) · ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ) )
184 simplr ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) )
185 147 nn0cnd ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → 𝑦 ∈ ℂ )
186 152 nn0cnd ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ∈ ℂ )
187 185 186 pncan3d ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → ( 𝑦 + ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) − 𝑦 ) ) = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) )
188 187 oveq2d ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → ( 2 ↑ ( 𝑦 + ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) − 𝑦 ) ) ) = ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) )
189 171 163 147 expaddd ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → ( 2 ↑ ( 𝑦 + ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) − 𝑦 ) ) ) = ( ( 2 ↑ 𝑦 ) · ( 2 ↑ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) − 𝑦 ) ) ) )
190 188 189 eqtr3d ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) = ( ( 2 ↑ 𝑦 ) · ( 2 ↑ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) − 𝑦 ) ) ) )
191 190 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 , < ) ) ) ) )
192 183 184 191 3eqtr3d ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → ( ( 2 ↑ 𝑦 ) · 𝑥 ) = ( ( ( 2 ↑ 𝑦 ) · ( 2 ↑ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) − 𝑦 ) ) ) · ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ) )
193 181 172 179 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 , < ) ) ) ) ) )
194 192 193 eqtrd ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ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 ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → 𝑥 = ( ( 2 ↑ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) − 𝑦 ) ) · ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ) )
196 179 172 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 , < ) ) ) ) )
197 195 196 eqtr4d ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → 𝑥 = ( ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) · ( 2 ↑ ( sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) − 𝑦 ) ) ) )
198 168 197 breqtrrd ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → 2 ∥ 𝑥 )
199 145 198 nsyl3 ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → ¬ 𝑥 ∈ 𝐽 )
200 141 199 pm2.65da ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → ¬ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) )
201 138 nnzd ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → 𝑥 ∈ ℤ )
202 136 nnzd ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → ( 2 ↑ 𝑦 ) ∈ ℤ )
203 140 nnzd ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → 𝑎 ∈ ℤ )
204 136 nncnd ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → ( 2 ↑ 𝑦 ) ∈ ℂ )
205 138 nncnd ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → 𝑥 ∈ ℂ )
206 204 205 mulcomd ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → ( ( 2 ↑ 𝑦 ) · 𝑥 ) = ( 𝑥 · ( 2 ↑ 𝑦 ) ) )
207 133 206 eqtr2d ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → ( 𝑥 · ( 2 ↑ 𝑦 ) ) = 𝑎 )
208 dvds0lem ⊢ ( ( ( 𝑥 ∈ ℤ ∧ ( 2 ↑ 𝑦 ) ∈ ℤ ∧ 𝑎 ∈ ℤ ) ∧ ( 𝑥 · ( 2 ↑ 𝑦 ) ) = 𝑎 ) → ( 2 ↑ 𝑦 ) ∥ 𝑎 )
209 201 202 203 207 208 syl31anc ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → ( 2 ↑ 𝑦 ) ∥ 𝑎 )
210 oveq2 ⊢ ( 𝑘 = 𝑦 → ( 2 ↑ 𝑘 ) = ( 2 ↑ 𝑦 ) )
211 210 breq1d ⊢ ( 𝑘 = 𝑦 → ( ( 2 ↑ 𝑘 ) ∥ 𝑎 ↔ ( 2 ↑ 𝑦 ) ∥ 𝑎 ) )
212 211 elrab ⊢ ( 𝑦 ∈ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } ↔ ( 𝑦 ∈ ℕ0 ∧ ( 2 ↑ 𝑦 ) ∥ 𝑎 ) )
213 135 209 212 sylanbrc ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → 𝑦 ∈ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } )
214 19 a1i ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → < Or ℕ0 )
215 214 150 supub ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → ( 𝑦 ∈ { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } → ¬ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) < 𝑦 ) )
216 213 215 mpd ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → ¬ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) < 𝑦 )
217 135 nn0red ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → 𝑦 ∈ ℝ )
218 140 97 syl ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ∈ ℝ )
219 217 218 lttri3d ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → ( 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ↔ ( ¬ 𝑦 < sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ∧ ¬ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) < 𝑦 ) ) )
220 200 216 219 mpbir2and ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) )
221 simplr ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) )
222 140 adantr ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → 𝑎 ∈ ℕ )
223 222 nncnd ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → 𝑎 ∈ ℂ )
224 138 adantr ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → 𝑥 ∈ ℕ )
225 224 nncnd ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → 𝑥 ∈ ℂ )
226 nnexpcl ⊢ ( ( 2 ∈ ℕ ∧ 𝑦 ∈ ℕ0 ) → ( 2 ↑ 𝑦 ) ∈ ℕ )
227 3 226 mpan ⊢ ( 𝑦 ∈ ℕ0 → ( 2 ↑ 𝑦 ) ∈ ℕ )
228 227 nncnd ⊢ ( 𝑦 ∈ ℕ0 → ( 2 ↑ 𝑦 ) ∈ ℂ )
229 227 nnne0d ⊢ ( 𝑦 ∈ ℕ0 → ( 2 ↑ 𝑦 ) ≠ 0 )
230 228 229 jca ⊢ ( 𝑦 ∈ ℕ0 → ( ( 2 ↑ 𝑦 ) ∈ ℂ ∧ ( 2 ↑ 𝑦 ) ≠ 0 ) )
231 230 ad3antlr ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → ( ( 2 ↑ 𝑦 ) ∈ ℂ ∧ ( 2 ↑ 𝑦 ) ≠ 0 ) )
232 divmul2 ⊢ ( ( 𝑎 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ ( ( 2 ↑ 𝑦 ) ∈ ℂ ∧ ( 2 ↑ 𝑦 ) ≠ 0 ) ) → ( ( 𝑎 / ( 2 ↑ 𝑦 ) ) = 𝑥 ↔ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) )
233 223 225 231 232 syl3anc ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → ( ( 𝑎 / ( 2 ↑ 𝑦 ) ) = 𝑥 ↔ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) )
234 221 233 mpbird ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → ( 𝑎 / ( 2 ↑ 𝑦 ) ) = 𝑥 )
235 simpr ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) )
236 235 oveq2d ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → ( 2 ↑ 𝑦 ) = ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) )
237 236 oveq2d ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → ( 𝑎 / ( 2 ↑ 𝑦 ) ) = ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) )
238 234 237 eqtr3d ⊢ ( ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ∧ 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) → 𝑥 = ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) )
239 238 ex ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → ( 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) → 𝑥 = ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ) )
240 220 239 jcai ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → ( 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ∧ 𝑥 = ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ) )
241 240 ancomd ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → ( 𝑥 = ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∧ 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) )
242 140 241 jca ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) → ( 𝑎 ∈ ℕ ∧ ( 𝑥 = ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∧ 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) )
243 simprl ⊢ ( ( 𝑎 ∈ ℕ ∧ ( 𝑥 = ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∧ 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) → 𝑥 = ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) )
244 130 adantr ⊢ ( ( 𝑎 ∈ ℕ ∧ ( 𝑥 = ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∧ 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) → ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∈ 𝐽 )
245 243 244 eqeltrd ⊢ ( ( 𝑎 ∈ ℕ ∧ ( 𝑥 = ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∧ 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) → 𝑥 ∈ 𝐽 )
246 simprr ⊢ ( ( 𝑎 ∈ ℕ ∧ ( 𝑥 = ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∧ 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) → 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) )
247 53 adantr ⊢ ( ( 𝑎 ∈ ℕ ∧ ( 𝑥 = ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∧ 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) → sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ∈ ℕ0 )
248 246 247 eqeltrd ⊢ ( ( 𝑎 ∈ ℕ ∧ ( 𝑥 = ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∧ 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) → 𝑦 ∈ ℕ0 )
249 118 adantr ⊢ ( ( 𝑎 ∈ ℕ ∧ ( 𝑥 = ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∧ 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) → 𝑎 = ( ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) · ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ) )
250 246 oveq2d ⊢ ( ( 𝑎 ∈ ℕ ∧ ( 𝑥 = ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∧ 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) → ( 2 ↑ 𝑦 ) = ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) )
251 250 243 oveq12d ⊢ ( ( 𝑎 ∈ ℕ ∧ ( 𝑥 = ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∧ 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) → ( ( 2 ↑ 𝑦 ) · 𝑥 ) = ( ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) · ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ) )
252 249 251 eqtr4d ⊢ ( ( 𝑎 ∈ ℕ ∧ ( 𝑥 = ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∧ 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) → 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) )
253 245 248 252 jca31 ⊢ ( ( 𝑎 ∈ ℕ ∧ ( 𝑥 = ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∧ 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) → ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) )
254 242 253 impbii ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ↔ ( 𝑎 ∈ ℕ ∧ ( 𝑥 = ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∧ 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) )
255 254 a1i ⊢ ( ⊤ → ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑎 = ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) ↔ ( 𝑎 ∈ ℕ ∧ ( 𝑥 = ( 𝑎 / ( 2 ↑ sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ∧ 𝑦 = sup ( { 𝑘 ∈ ℕ0 ∣ ( 2 ↑ 𝑘 ) ∥ 𝑎 } , ℕ0 , < ) ) ) ) )
256 2 13 132 255 f1od2 ⊢ ( ⊤ → 𝐹 : ( 𝐽 × ℕ0 ) –1-1-onto→ ℕ )
257 256 mptru ⊢ 𝐹 : ( 𝐽 × ℕ0 ) –1-1-onto→ ℕ