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	sselid	$$⊢\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	56 57 59 60 46	elfzd	$$⊢\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)$$
62	61	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)$$
63	62	ssrdv	$$⊢a\in \mathbb{N}\to \left\{k\in {\mathbb{N}}_0|2^k\parallel a\right\}\subseteq \left(0\dots a\right)$$
64		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}$$
65	55 63 64	sylancr	$$⊢a\in \mathbb{N}\to \left\{k\in {\mathbb{N}}_0|2^k\parallel a\right\}\in \mathrm{Fin}$$
66		0nn0	$$⊢0\in {\mathbb{N}}_0$$
67	66	a1i	$$⊢a\in \mathbb{N}\to 0\in {\mathbb{N}}_0$$
68		2cn	$$⊢2\in ℂ$$
69		exp0	$$⊢2\in ℂ\to 2^0=1$$
70	68 69	ax-mp	$$⊢2^0=1$$
71		1dvds	$$⊢a\in \mathbb{Z}\to 1\parallel a$$
72	24 71	syl	$$⊢a\in \mathbb{N}\to 1\parallel a$$
73	70 72	eqbrtrid	$$⊢a\in \mathbb{N}\to 2^0\parallel a$$
74		oveq2	$$⊢k=0\to 2^k=2^0$$
75	74	breq1d	$$⊢k=0\to \left(2^k\parallel a\leftrightarrow 2^0\parallel a\right)$$
76	75	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)$$
77	67 73 76	sylanbrc	$$⊢a\in \mathbb{N}\to 0\in \left\{k\in {\mathbb{N}}_0|2^k\parallel a\right\}$$
78	77	ne0d	$$⊢a\in \mathbb{N}\to \left\{k\in {\mathbb{N}}_0|2^k\parallel a\right\}\ne \varnothing$$
79		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\}$$
80	20 65 78 23 79	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\}$$
81		oveq2	$$⊢k=l\to 2^k=2^l$$
82	81	breq1d	$$⊢k=l\to \left(2^k\parallel a\leftrightarrow 2^l\parallel a\right)$$
83	82	cbvrabv	$$⊢\left\{k\in {\mathbb{N}}_0|2^k\parallel a\right\}=\left\{l\in {\mathbb{N}}_0|2^l\parallel a\right\}$$
84	80 83	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\}$$
85		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)}$$
86	85	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)$$
87	86	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)$$
88	84 87	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)$$
89	88	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$$
90		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)$$
91	90	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}$$
92	14 54 89 91	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}$$
93		1nn0	$$⊢1\in {\mathbb{N}}_0$$
94	93	a1i	$$⊢a\in \mathbb{N}\to 1\in {\mathbb{N}}_0$$
95	53 94	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$$
96	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 ℝ$$
97	96	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$$
98	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)$$
99	97 98	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\}$$
100	83	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\}$$
101	99 100	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\}$$
102		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}$$
103	102	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)$$
104	103	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)$$
105	101 104	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)$$
106		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)$$
107	105 106	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)$$
108	95 107	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$$
109		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$$
110	68 53 109	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$$
111	110	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)$$
112	108 111	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$$
113		nncn	$$⊢a\in \mathbb{N}\to a\in ℂ$$
114	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 ℂ$$
115	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$$
116	113 114 115	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$$
117	116	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)$$
118	117	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)$$
119	15	nnzd	$$⊢a\in \mathbb{N}\to 2\in \mathbb{Z}$$
120	92	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}$$
121	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}$$
122		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)$$
123	119 120 121 115 122	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)$$
124	118 123	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)$$
125	112 124	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)$$
126		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)$$
127	126	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)$$
128	127 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)$$
129	92 125 128	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$$
130	129 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)$$
131	130	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)$$
132		simpr	$$⊢\left(\left(x\in J\wedge y\in {\mathbb{N}}_0\right)\wedge a=2^{y}x\right)\to a=2^{y}x$$
133	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}$$
134		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$$
135	133 134	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}$$
136	8	sseli	$$⊢x\in J\to x\in \mathbb{N}$$
137	136	ad2antrr	$$⊢\left(\left(x\in J\wedge y\in {\mathbb{N}}_0\right)\wedge a=2^{y}x\right)\to x\in \mathbb{N}$$
138	135 137	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}$$
139	132 138	eqeltrd	$$⊢\left(\left(x\in J\wedge y\in {\mathbb{N}}_0\right)\wedge a=2^{y}x\right)\to a\in \mathbb{N}$$
140		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$$
141		breq2	$$⊢z=x\to \left(2\parallel z\leftrightarrow 2\parallel x\right)$$
142	141	notbid	$$⊢z=x\to \left(\neg 2\parallel z\leftrightarrow \neg 2\parallel x\right)$$
143	142 1	elrab2	$$⊢x\in J\leftrightarrow \left(x\in \mathbb{N}\wedge \neg 2\parallel x\right)$$
144	143	simprbi	$$⊢x\in J\to \neg 2\parallel x$$
145		2z	$$⊢2\in \mathbb{Z}$$
146	134	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$$
147	146	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}$$
148	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$$
149	139 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)$$
150	149	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)$$
151	148 150	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$$
152	151	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}$$
153		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)$$
154		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)$$
155	154	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}$$
156	147 152 153 155	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}$$
157		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}$$
158	145 156 157	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}$$
159	145	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}$$
160	139 120	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}$$
161	160	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}$$
162	156	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$$
163		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}$$
164	145 162 163	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}$$
165		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)$$
166	159 161 164 165	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)$$
167	158 166	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}$$
168	137	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}$$
169	168	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 ℂ$$
170		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 ℂ$$
171	170 162	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 ℂ$$
172	139	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}$$
173	172	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 ℂ$$
174	172 114	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 ℂ$$
175		2ne0	$$⊢2\ne 0$$
176	175	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$$
177	170 176 152	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$$
178	173 174 177	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 ℂ$$
179	171 178	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 ℂ$$
180	170 146	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 ℂ$$
181	170 176 147	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$$
182	172 117	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)$$
183		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$$
184	146	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 ℂ$$
185	151	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 ℂ$$
186	184 185	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)$$
187	186	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)}$$
188	170 162 146	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}$$
189	187 188	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}$$
190	189	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)$$
191	182 183 190	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)$$
192	180 171 178	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)$$
193	191 192	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)$$
194	169 179 180 181 193	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)$$
195	178 171	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)$$
196	194 195	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}$$
197	167 196	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$$
198	144 197	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$$
199	140 198	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)$$
200	137	nnzd	$$⊢\left(\left(x\in J\wedge y\in {\mathbb{N}}_0\right)\wedge a=2^{y}x\right)\to x\in \mathbb{Z}$$
201	135	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}$$
202	139	nnzd	$$⊢\left(\left(x\in J\wedge y\in {\mathbb{N}}_0\right)\wedge a=2^{y}x\right)\to a\in \mathbb{Z}$$
203	135	nncnd	$$⊢\left(\left(x\in J\wedge y\in {\mathbb{N}}_0\right)\wedge a=2^{y}x\right)\to 2^y\in ℂ$$
204	137	nncnd	$$⊢\left(\left(x\in J\wedge y\in {\mathbb{N}}_0\right)\wedge a=2^{y}x\right)\to x\in ℂ$$
205	203 204	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$$
206	132 205	eqtr2d	$$⊢\left(\left(x\in J\wedge y\in {\mathbb{N}}_0\right)\wedge a=2^{y}x\right)\to x{2}^y=a$$
207		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$$
208	200 201 202 206 207	syl31anc	$$⊢\left(\left(x\in J\wedge y\in {\mathbb{N}}_0\right)\wedge a=2^{y}x\right)\to 2^y\parallel a$$
209		oveq2	$$⊢k=y\to 2^k=2^y$$
210	209	breq1d	$$⊢k=y\to \left(2^k\parallel a\leftrightarrow 2^y\parallel a\right)$$
211	210	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)$$
212	134 208 211	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\}$$
213	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$$
214	213 149	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)$$
215	212 214	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$$
216	134	nn0red	$$⊢\left(\left(x\in J\wedge y\in {\mathbb{N}}_0\right)\wedge a=2^{y}x\right)\to y\in ℝ$$
217	139 96	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 ℝ$$
218	216 217	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)$$
219	199 215 218	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)$$
220		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$$
221	139	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}$$
222	221	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 ℂ$$
223	137	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}$$
224	223	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 ℂ$$
225		nnexpcl	$$⊢\left(2\in \mathbb{N}\wedge y\in {\mathbb{N}}_0\right)\to 2^y\in \mathbb{N}$$
226	3 225	mpan	$$⊢y\in {\mathbb{N}}_0\to 2^y\in \mathbb{N}$$
227	226	nncnd	$$⊢y\in {\mathbb{N}}_0\to 2^y\in ℂ$$
228	226	nnne0d	$$⊢y\in {\mathbb{N}}_0\to 2^y\ne 0$$
229	227 228	jca	$$⊢y\in {\mathbb{N}}_0\to \left(2^y\in ℂ\wedge 2^y\ne 0\right)$$
230	229	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)$$
231		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)$$
232	222 224 230 231	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)$$
233	220 232	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$$
234		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)$$
235	234	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)}$$
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 \frac{a}{2^y}=\frac{a}{2^{sup\left(\left\{k\in {\mathbb{N}}_0|2^k\parallel a\right\},{\mathbb{N}}_0,<\right)}}$$
237	233 236	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)}}$$
238	237	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)$$
239	219 238	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)$$
240	239	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)$$
241	139 240	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)$$
242		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)}}$$
243	129	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$$
244	242 243	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$$
245		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)$$
246	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$$
247	245 246	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$$
248	117	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)$$
249	245	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)}$$
250	249 242	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)$$
251	248 250	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$$
252	244 247 251	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)$$
253	241 252	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)$$
254	253	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)$$
255	2 13 131 254	f1od2	$$⊢\top \to F:J\times {\mathbb{N}}_0\underset{1-1\; onto}{⟶}\mathbb{N}$$
256	255	mptru	$$⊢F:J\times {\mathbb{N}}_0\underset{1-1\; onto}{⟶}\mathbb{N}$$