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	$$⊢J=\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}$$
	oddpwdc.f	$$⊢F=\left(x\in J,y\in {\mathbb{N}}_0⟼2^{y}x\right)$$
Assertion	oddpwdc	$$⊢F:J\times {\mathbb{N}}_0\underset{1-1\; onto}{⟶}\mathbb{N}$$

Proof

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