Theorem oddpwdc 34969

Description: Lemma for eulerpart 34997. The function 𝐹 that decomposes a number into its "odd" and "even" parts, which is to say the largest power of two and largest odd divisor of a number, is a bijection from pairs of a nonnegative integer and an odd number to positive integers. (Contributed by Thierry Arnoux, 15-Aug-2017.)

Hypotheses

Ref	Expression
oddpwdc.j	⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}
oddpwdc.f	⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))

Assertion

Ref	Expression
oddpwdc	⊢ 𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ

Distinct variable groups:   𝑥,𝑦,𝑧   𝑥,𝐽,𝑦

Allowed substitution hints:   𝐹(𝑥, 𝑦, 𝑧)   𝐽(𝑧)

Proof of Theorem oddpwdc

Dummy variables 𝑘 𝑎 𝑙 𝑚 𝑛 𝑜 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		oddpwdc.f	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))
2		2nn 12397	. . . . . . . 8 ⊢ 2 ∈ ℕ
3	2	a1i 11	. . . . . . 7 ⊢ ((𝑦 ∈ ℕ0 ∧ 𝑥 ∈ 𝐽) → 2 ∈ ℕ)
4		simpl 488	. . . . . . 7 ⊢ ((𝑦 ∈ ℕ0 ∧ 𝑥 ∈ 𝐽) → 𝑦 ∈ ℕ0)
5	3, 4	nnexpcld 14369	. . . . . 6 ⊢ ((𝑦 ∈ ℕ0 ∧ 𝑥 ∈ 𝐽) → (2↑𝑦) ∈ ℕ)
6		oddpwdc.j	. . . . . . . 8 ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}
7		ssrab2 4028	. . . . . . . 8 ⊢ {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} ⊆ ℕ
8	6, 7	eqsstri 3977	. . . . . . 7 ⊢ 𝐽 ⊆ ℕ
9		simpr 490	. . . . . . 7 ⊢ ((𝑦 ∈ ℕ0 ∧ 𝑥 ∈ 𝐽) → 𝑥 ∈ 𝐽)
10	8, 9	sselid 3929	. . . . . 6 ⊢ ((𝑦 ∈ ℕ0 ∧ 𝑥 ∈ 𝐽) → 𝑥 ∈ ℕ)
11	5, 10	nnmulcld 12372	. . . . 5 ⊢ ((𝑦 ∈ ℕ0 ∧ 𝑥 ∈ 𝐽) → ((2↑𝑦) · 𝑥) ∈ ℕ)
12	11	ancoms 464	. . . 4 ⊢ ((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) → ((2↑𝑦) · 𝑥) ∈ ℕ)
13	12	adantl 487	. . 3 ⊢ ((⊤ ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0)) → ((2↑𝑦) · 𝑥) ∈ ℕ)
14		id 23	. . . . . . 7 ⊢ (𝑎 ∈ ℕ → 𝑎 ∈ ℕ)
15	2	a1i 11	. . . . . . . 8 ⊢ (𝑎 ∈ ℕ → 2 ∈ ℕ)
16		nn0ssre 12591	. . . . . . . . . . 11 ⊢ ℕ0 ⊆ ℝ
17		ltso 11371	. . . . . . . . . . 11 ⊢ < Or ℝ
18		soss 5579	. . . . . . . . . . 11 ⊢ (ℕ0 ⊆ ℝ → ( < Or ℝ → < Or ℕ0))
19	16, 17, 18	mp2 9	. . . . . . . . . 10 ⊢ < Or ℕ0
20	19	a1i 11	. . . . . . . . 9 ⊢ (𝑎 ∈ ℕ → < Or ℕ0)
21		0zd 12686	. . . . . . . . . 10 ⊢ (𝑎 ∈ ℕ → 0 ∈ ℤ)
22		ssrab2 4028	. . . . . . . . . . 11 ⊢ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ⊆ ℕ0
23	22	a1i 11	. . . . . . . . . 10 ⊢ (𝑎 ∈ ℕ → {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ⊆ ℕ0)
24		nnz 12695	. . . . . . . . . . 11 ⊢ (𝑎 ∈ ℕ → 𝑎 ∈ ℤ)
25		oveq2 7420	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑛 → (2↑𝑘) = (2↑𝑛))
26	25	breq1d 5113	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑛 → ((2↑𝑘) ∥ 𝑎 ↔ (2↑𝑛) ∥ 𝑎))
27	26	elrab 3645	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ↔ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎))
28		simprl 783	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → 𝑛 ∈ ℕ0)
29	28	nn0red 12649	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → 𝑛 ∈ ℝ)
30	2	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → 2 ∈ ℕ)
31	30, 28	nnexpcld 14369	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → (2↑𝑛) ∈ ℕ)
32	31	nnred 12331	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → (2↑𝑛) ∈ ℝ)
33		simpl 488	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → 𝑎 ∈ ℕ)
34	33	nnred 12331	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → 𝑎 ∈ ℝ)
35		2re 12398	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℝ
36	35	leidi 11831	. . . . . . . . . . . . . . . 16 ⊢ 2 ≤ 2
37		nexple 33406	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ ℕ0 ∧ 2 ∈ ℝ ∧ 2 ≤ 2) → 𝑛 ≤ (2↑𝑛))
38	35, 36, 37	mp3an23 1482	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ0 → 𝑛 ≤ (2↑𝑛))
39	38	ad2antrl 741	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → 𝑛 ≤ (2↑𝑛))
40	31	nnzd 12700	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → (2↑𝑛) ∈ ℤ)
41		simprr 785	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → (2↑𝑛) ∥ 𝑎)
42		dvdsle 16460	. . . . . . . . . . . . . . . 16 ⊢ (((2↑𝑛) ∈ ℤ ∧ 𝑎 ∈ ℕ) → ((2↑𝑛) ∥ 𝑎 → (2↑𝑛) ≤ 𝑎))
43	42	imp 412	. . . . . . . . . . . . . . 15 ⊢ ((((2↑𝑛) ∈ ℤ ∧ 𝑎 ∈ ℕ) ∧ (2↑𝑛) ∥ 𝑎) → (2↑𝑛) ≤ 𝑎)
44	40, 33, 41, 43	syl21anc 851	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → (2↑𝑛) ≤ 𝑎)
45	29, 32, 34, 39, 44	letrd 11448	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → 𝑛 ≤ 𝑎)
46	27, 45	sylan2b 606	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}) → 𝑛 ≤ 𝑎)
47	46	ralrimiva 3155	. . . . . . . . . . 11 ⊢ (𝑎 ∈ ℕ → ∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}𝑛 ≤ 𝑎)
48		brralrspcev 5165	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ ℤ ∧ ∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}𝑛 ≤ 𝑎) → ∃𝑚 ∈ ℤ ∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}𝑛 ≤ 𝑚)
49	24, 47, 48	syl2anc 596	. . . . . . . . . 10 ⊢ (𝑎 ∈ ℕ → ∃𝑚 ∈ ℤ ∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}𝑛 ≤ 𝑚)
50		nn0uz 12984	. . . . . . . . . . 11 ⊢ ℕ0 = (ℤ≥‘0)
51	50	uzsupss 13048	. . . . . . . . . 10 ⊢ ((0 ∈ ℤ ∧ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ⊆ ℕ0 ∧ ∃𝑚 ∈ ℤ ∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}𝑛 ≤ 𝑚) → ∃𝑚 ∈ ℕ0 (∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ¬ 𝑚 < 𝑛 ∧ ∀𝑛 ∈ ℕ0 (𝑛 < 𝑚 → ∃𝑜 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}𝑛 < 𝑜)))
52	21, 23, 49, 51	syl3anc 1398	. . . . . . . . 9 ⊢ (𝑎 ∈ ℕ → ∃𝑚 ∈ ℕ0 (∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ¬ 𝑚 < 𝑛 ∧ ∀𝑛 ∈ ℕ0 (𝑛 < 𝑚 → ∃𝑜 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}𝑛 < 𝑜)))
53	20, 52	supcl 9434	. . . . . . . 8 ⊢ (𝑎 ∈ ℕ → sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℕ0)
54	15, 53	nnexpcld 14369	. . . . . . 7 ⊢ (𝑎 ∈ ℕ → (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∈ ℕ)
55		fzfi 14095	. . . . . . . . . . . 12 ⊢ (0...𝑎) ∈ Fin
56		0zd 12686	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}) → 0 ∈ ℤ)
57	24	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}) → 𝑎 ∈ ℤ)
58	27, 28	sylan2b 606	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}) → 𝑛 ∈ ℕ0)
59	58	nn0zd 12699	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}) → 𝑛 ∈ ℤ)
60	58	nn0ge0d 12651	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}) → 0 ≤ 𝑛)
61	56, 57, 59, 60, 46	elfzd 13628	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}) → 𝑛 ∈ (0...𝑎))
62	61	ex 418	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ ℕ → (𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} → 𝑛 ∈ (0...𝑎)))
63	62	ssrdv 3937	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ ℕ → {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ⊆ (0...𝑎))
64		ssfi 9172	. . . . . . . . . . . 12 ⊢ (((0...𝑎) ∈ Fin ∧ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ⊆ (0...𝑎)) → {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ∈ Fin)
65	55, 63, 64	sylancr 599	. . . . . . . . . . 11 ⊢ (𝑎 ∈ ℕ → {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ∈ Fin)
66		0nn0 12602	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℕ0
67	66	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ ℕ → 0 ∈ ℕ0)
68		2cn 12399	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℂ
69		exp0 14188	. . . . . . . . . . . . . . 15 ⊢ (2 ∈ ℂ → (2↑0) = 1)
70	68, 69	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ (2↑0) = 1
71		1dvds 16420	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ ℤ → 1 ∥ 𝑎)
72	24, 71	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ ℕ → 1 ∥ 𝑎)
73	70, 72	eqbrtrid 5140	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ ℕ → (2↑0) ∥ 𝑎)
74		oveq2 7420	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 0 → (2↑𝑘) = (2↑0))
75	74	breq1d 5113	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 0 → ((2↑𝑘) ∥ 𝑎 ↔ (2↑0) ∥ 𝑎))
76	75	elrab 3645	. . . . . . . . . . . . 13 ⊢ (0 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ↔ (0 ∈ ℕ0 ∧ (2↑0) ∥ 𝑎))
77	67, 73, 76	sylanbrc 595	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ ℕ → 0 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎})
78	77	ne0d 4288	. . . . . . . . . . 11 ⊢ (𝑎 ∈ ℕ → {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ≠ ∅)
79		fisupcl 9446	. . . . . . . . . . 11 ⊢ (( < Or ℕ0 ∧ ({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ∈ Fin ∧ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ≠ ∅ ∧ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ⊆ ℕ0)) → sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎})
80	20, 65, 78, 23, 79	syl13anc 1399	. . . . . . . . . 10 ⊢ (𝑎 ∈ ℕ → sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎})
81		oveq2 7420	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑙 → (2↑𝑘) = (2↑𝑙))
82	81	breq1d 5113	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑙 → ((2↑𝑘) ∥ 𝑎 ↔ (2↑𝑙) ∥ 𝑎))
83	82	cbvrabv 3423	. . . . . . . . . 10 ⊢ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} = {𝑙 ∈ ℕ0 ∣ (2↑𝑙) ∥ 𝑎}
84	80, 83	eleqtrdi 2871	. . . . . . . . 9 ⊢ (𝑎 ∈ ℕ → sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ {𝑙 ∈ ℕ0 ∣ (2↑𝑙) ∥ 𝑎})
85		oveq2 7420	. . . . . . . . . . 11 ⊢ (𝑙 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) → (2↑𝑙) = (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))
86	85	breq1d 5113	. . . . . . . . . 10 ⊢ (𝑙 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) → ((2↑𝑙) ∥ 𝑎 ↔ (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∥ 𝑎))
87	86	elrab 3645	. . . . . . . . 9 ⊢ (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ {𝑙 ∈ ℕ0 ∣ (2↑𝑙) ∥ 𝑎} ↔ (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℕ0 ∧ (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∥ 𝑎))
88	84, 87	sylib 221	. . . . . . . 8 ⊢ (𝑎 ∈ ℕ → (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℕ0 ∧ (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∥ 𝑎))
89	88	simprd 501	. . . . . . 7 ⊢ (𝑎 ∈ ℕ → (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∥ 𝑎)
90		nndivdvds 16411	. . . . . . . 8 ⊢ ((𝑎 ∈ ℕ ∧ (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∈ ℕ) → ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∥ 𝑎 ↔ (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ ℕ))
91	90	biimpa 482	. . . . . . 7 ⊢ (((𝑎 ∈ ℕ ∧ (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∈ ℕ) ∧ (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∥ 𝑎) → (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ ℕ)
92	14, 54, 89, 91	syl21anc 851	. . . . . 6 ⊢ (𝑎 ∈ ℕ → (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ ℕ)
93		1nn0 12603	. . . . . . . . . . 11 ⊢ 1 ∈ ℕ0
94	93	a1i 11	. . . . . . . . . 10 ⊢ (𝑎 ∈ ℕ → 1 ∈ ℕ0)
95	53, 94	nn0addcld 12652	. . . . . . . . 9 ⊢ (𝑎 ∈ ℕ → (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈ ℕ0)
96	53	nn0red 12649	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ ℕ → sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℝ)
97	96	ltp1d 12228	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ ℕ → sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) < (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1))
98	20, 52	supub 9435	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ ℕ → ((sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} → ¬ sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) < (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)))
99	97, 98	mt2d 137	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ ℕ → ¬ (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎})
100	83	eleq2i 2853	. . . . . . . . . . . 12 ⊢ ((sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ↔ (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈ {𝑙 ∈ ℕ0 ∣ (2↑𝑙) ∥ 𝑎})
101	99, 100	sylnib 331	. . . . . . . . . . 11 ⊢ (𝑎 ∈ ℕ → ¬ (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈ {𝑙 ∈ ℕ0 ∣ (2↑𝑙) ∥ 𝑎})
102		oveq2 7420	. . . . . . . . . . . . 13 ⊢ (𝑙 = (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) → (2↑𝑙) = (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)))
103	102	breq1d 5113	. . . . . . . . . . . 12 ⊢ (𝑙 = (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) → ((2↑𝑙) ∥ 𝑎 ↔ (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) ∥ 𝑎))
104	103	elrab 3645	. . . . . . . . . . 11 ⊢ ((sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈ {𝑙 ∈ ℕ0 ∣ (2↑𝑙) ∥ 𝑎} ↔ ((sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈ ℕ0 ∧ (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) ∥ 𝑎))
105	101, 104	sylnib 331	. . . . . . . . . 10 ⊢ (𝑎 ∈ ℕ → ¬ ((sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈ ℕ0 ∧ (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) ∥ 𝑎))
106		imnan 405	. . . . . . . . . 10 ⊢ (((sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈ ℕ0 → ¬ (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) ∥ 𝑎) ↔ ¬ ((sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈ ℕ0 ∧ (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) ∥ 𝑎))
107	105, 106	sylibr 237	. . . . . . . . 9 ⊢ (𝑎 ∈ ℕ → ((sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈ ℕ0 → ¬ (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) ∥ 𝑎))
108	95, 107	mpd 16	. . . . . . . 8 ⊢ (𝑎 ∈ ℕ → ¬ (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) ∥ 𝑎)
109		expp1 14191	. . . . . . . . . 10 ⊢ ((2 ∈ ℂ ∧ sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℕ0) → (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) = ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2))
110	68, 53, 109	sylancr 599	. . . . . . . . 9 ⊢ (𝑎 ∈ ℕ → (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) = ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2))
111	110	breq1d 5113	. . . . . . . 8 ⊢ (𝑎 ∈ ℕ → ((2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) ∥ 𝑎 ↔ ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2) ∥ 𝑎))
112	108, 111	mtbid 327	. . . . . . 7 ⊢ (𝑎 ∈ ℕ → ¬ ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2) ∥ 𝑎)
113		nncn 12324	. . . . . . . . . . 11 ⊢ (𝑎 ∈ ℕ → 𝑎 ∈ ℂ)
114	54	nncnd 12332	. . . . . . . . . . 11 ⊢ (𝑎 ∈ ℕ → (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∈ ℂ)
115	54	nnne0d 12369	. . . . . . . . . . 11 ⊢ (𝑎 ∈ ℕ → (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ≠ 0)
116	113, 114, 115	divcan2d 12076	. . . . . . . . . 10 ⊢ (𝑎 ∈ ℕ → ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))) = 𝑎)
117	116	eqcomd 2767	. . . . . . . . 9 ⊢ (𝑎 ∈ ℕ → 𝑎 = ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
118	117	breq2d 5115	. . . . . . . 8 ⊢ (𝑎 ∈ ℕ → (((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2) ∥ 𝑎 ↔ ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2) ∥ ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))))))
119	15	nnzd 12700	. . . . . . . . 9 ⊢ (𝑎 ∈ ℕ → 2 ∈ ℤ)
120	92	nnzd 12700	. . . . . . . . 9 ⊢ (𝑎 ∈ ℕ → (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ ℤ)
121	54	nnzd 12700	. . . . . . . . 9 ⊢ (𝑎 ∈ ℕ → (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∈ ℤ)
122		dvdscmulr 16434	. . . . . . . . 9 ⊢ ((2 ∈ ℤ ∧ (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ ℤ ∧ ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∈ ℤ ∧ (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ≠ 0)) → (((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2) ∥ ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))) ↔ 2 ∥ (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
123	119, 120, 121, 115, 122	syl112anc 1401	. . . . . . . 8 ⊢ (𝑎 ∈ ℕ → (((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2) ∥ ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))) ↔ 2 ∥ (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
124	118, 123	bitrd 282	. . . . . . 7 ⊢ (𝑎 ∈ ℕ → (((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2) ∥ 𝑎 ↔ 2 ∥ (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
125	112, 124	mtbid 327	. . . . . 6 ⊢ (𝑎 ∈ ℕ → ¬ 2 ∥ (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))))
126		breq2 5107	. . . . . . . 8 ⊢ (𝑧 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → (2 ∥ 𝑧 ↔ 2 ∥ (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
127	126	notbid 321	. . . . . . 7 ⊢ (𝑧 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → (¬ 2 ∥ 𝑧 ↔ ¬ 2 ∥ (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
128	127, 6	elrab2 3649	. . . . . 6 ⊢ ((𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ 𝐽 ↔ ((𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ ℕ ∧ ¬ 2 ∥ (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
129	92, 125, 128	sylanbrc 595	. . . . 5 ⊢ (𝑎 ∈ ℕ → (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ 𝐽)
130	129, 53	jca 521	. . . 4 ⊢ (𝑎 ∈ ℕ → ((𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ 𝐽 ∧ sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℕ0))
131	130	adantl 487	. . 3 ⊢ ((⊤ ∧ 𝑎 ∈ ℕ) → ((𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ 𝐽 ∧ sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℕ0))
132		simpr 490	. . . . . . 7 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑎 = ((2↑𝑦) · 𝑥))
133	2	a1i 11	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 2 ∈ ℕ)
134		simplr 781	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑦 ∈ ℕ0)
135	133, 134	nnexpcld 14369	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (2↑𝑦) ∈ ℕ)
136	8	sseli 3927	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐽 → 𝑥 ∈ ℕ)
137	136	ad2antrr 739	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑥 ∈ ℕ)
138	135, 137	nnmulcld 12372	. . . . . . 7 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → ((2↑𝑦) · 𝑥) ∈ ℕ)
139	132, 138	eqeltrd 2861	. . . . . 6 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑎 ∈ ℕ)
140		simplll 787	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑥 ∈ 𝐽)
141		breq2 5107	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑥 → (2 ∥ 𝑧 ↔ 2 ∥ 𝑥))
142	141	notbid 321	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑥 → (¬ 2 ∥ 𝑧 ↔ ¬ 2 ∥ 𝑥))
143	142, 6	elrab2 3649	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐽 ↔ (𝑥 ∈ ℕ ∧ ¬ 2 ∥ 𝑥))
144	143	simprbi 503	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐽 → ¬ 2 ∥ 𝑥)
145		2z 12709	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℤ
146	134	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑦 ∈ ℕ0)
147	146	nn0zd 12699	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑦 ∈ ℤ)
148	19	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → < Or ℕ0)
149	139, 52	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → ∃𝑚 ∈ ℕ0 (∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ¬ 𝑚 < 𝑛 ∧ ∀𝑛 ∈ ℕ0 (𝑛 < 𝑚 → ∃𝑜 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}𝑛 < 𝑜)))
150	149	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → ∃𝑚 ∈ ℕ0 (∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ¬ 𝑚 < 𝑛 ∧ ∀𝑛 ∈ ℕ0 (𝑛 < 𝑚 → ∃𝑜 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}𝑛 < 𝑜)))
151	148, 150	supcl 9434	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℕ0)
152	151	nn0zd 12699	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℤ)
153		simpr 490	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))
154		znnsub 12723	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ ℤ ∧ sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℤ) → (𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ↔ (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦) ∈ ℕ))
155	154	biimpa 482	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 ∈ ℤ ∧ sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℤ) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦) ∈ ℕ)
156	147, 152, 153, 155	syl21anc 851	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦) ∈ ℕ)
157		iddvdsexp 16429	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℤ ∧ (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦) ∈ ℕ) → 2 ∥ (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)))
158	145, 156, 157	sylancr 599	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 2 ∥ (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)))
159	145	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 2 ∈ ℤ)
160	139, 120	syl 18	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ ℤ)
161	160	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ ℤ)
162	156	nnnn0d 12648	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦) ∈ ℕ0)
163		zexpcl 14199	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℤ ∧ (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦) ∈ ℕ0) → (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) ∈ ℤ)
164	145, 162, 163	sylancr 599	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) ∈ ℤ)
165		dvdsmultr2 16448	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℤ ∧ (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ ℤ ∧ (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) ∈ ℤ) → (2 ∥ (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) → 2 ∥ ((𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) · (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)))))
166	159, 161, 164, 165	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (2 ∥ (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) → 2 ∥ ((𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) · (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)))))
167	158, 166	mpd 16	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 2 ∥ ((𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) · (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦))))
168	137	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑥 ∈ ℕ)
169	168	nncnd 12332	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑥 ∈ ℂ)
170		2cnd 12402	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 2 ∈ ℂ)
171	170, 162	expcld 14269	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) ∈ ℂ)
172	139	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑎 ∈ ℕ)
173	172	nncnd 12332	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑎 ∈ ℂ)
174	172, 114	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∈ ℂ)
175		2ne0 12430	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ≠ 0
176	175	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 2 ≠ 0)
177	170, 176, 152	expne0d 14275	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ≠ 0)
178	173, 174, 177	divcld 12074	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ ℂ)
179	171, 178	mulcld 11310	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → ((2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))) ∈ ℂ)
180	170, 146	expcld 14269	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (2↑𝑦) ∈ ℂ)
181	170, 176, 147	expne0d 14275	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (2↑𝑦) ≠ 0)
182	172, 117	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑎 = ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
183		simplr 781	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑎 = ((2↑𝑦) · 𝑥))
184	146	nn0cnd 12650	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑦 ∈ ℂ)
185	151	nn0cnd 12650	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℂ)
186	184, 185	pncan3d 11653	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (𝑦 + (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))
187	186	oveq2d 7428	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (2↑(𝑦 + (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦))) = (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))
188	170, 162, 146	expaddd 14271	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (2↑(𝑦 + (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦))) = ((2↑𝑦) · (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦))))
189	187, 188	eqtr3d 2798	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) = ((2↑𝑦) · (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦))))
190	189	oveq1d 7427	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))) = (((2↑𝑦) · (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦))) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
191	182, 183, 190	3eqtr3d 2804	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → ((2↑𝑦) · 𝑥) = (((2↑𝑦) · (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦))) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
192	180, 171, 178	mulassd 11313	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (((2↑𝑦) · (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦))) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))) = ((2↑𝑦) · ((2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))))))
193	191, 192	eqtrd 2796	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → ((2↑𝑦) · 𝑥) = ((2↑𝑦) · ((2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))))))
194	169, 179, 180, 181, 193	mulcanad 11932	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑥 = ((2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
195	178, 171	mulcomd 11311	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → ((𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) · (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦))) = ((2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
196	194, 195	eqtr4d 2799	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑥 = ((𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) · (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦))))
197	167, 196	breqtrrd 5133	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 2 ∥ 𝑥)
198	144, 197	nsyl3 139	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → ¬ 𝑥 ∈ 𝐽)
199	140, 198	pm2.65da 829	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → ¬ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))
200	137	nnzd 12700	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑥 ∈ ℤ)
201	135	nnzd 12700	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (2↑𝑦) ∈ ℤ)
202	139	nnzd 12700	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑎 ∈ ℤ)
203	135	nncnd 12332	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (2↑𝑦) ∈ ℂ)
204	137	nncnd 12332	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑥 ∈ ℂ)
205	203, 204	mulcomd 11311	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → ((2↑𝑦) · 𝑥) = (𝑥 · (2↑𝑦)))
206	132, 205	eqtr2d 2797	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑥 · (2↑𝑦)) = 𝑎)
207		dvds0lem 16416	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℤ ∧ (2↑𝑦) ∈ ℤ ∧ 𝑎 ∈ ℤ) ∧ (𝑥 · (2↑𝑦)) = 𝑎) → (2↑𝑦) ∥ 𝑎)
208	200, 201, 202, 206, 207	syl31anc 1400	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (2↑𝑦) ∥ 𝑎)
209		oveq2 7420	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑦 → (2↑𝑘) = (2↑𝑦))
210	209	breq1d 5113	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑦 → ((2↑𝑘) ∥ 𝑎 ↔ (2↑𝑦) ∥ 𝑎))
211	210	elrab 3645	. . . . . . . . . . 11 ⊢ (𝑦 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ↔ (𝑦 ∈ ℕ0 ∧ (2↑𝑦) ∥ 𝑎))
212	134, 208, 211	sylanbrc 595	. . . . . . . . . 10 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑦 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎})
213	19	a1i 11	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → < Or ℕ0)
214	213, 149	supub 9435	. . . . . . . . . 10 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑦 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} → ¬ sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) < 𝑦))
215	212, 214	mpd 16	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → ¬ sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) < 𝑦)
216	134	nn0red 12649	. . . . . . . . . 10 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑦 ∈ ℝ)
217	139, 96	syl 18	. . . . . . . . . 10 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℝ)
218	216, 217	lttri3d 11431	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ↔ (¬ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∧ ¬ sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) < 𝑦)))
219	199, 215, 218	mpbir2and 726	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))
220		simplr 781	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑎 = ((2↑𝑦) · 𝑥))
221	139	adantr 486	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑎 ∈ ℕ)
222	221	nncnd 12332	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑎 ∈ ℂ)
223	137	adantr 486	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑥 ∈ ℕ)
224	223	nncnd 12332	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑥 ∈ ℂ)
225		nnexpcl 14197	. . . . . . . . . . . . . . . 16 ⊢ ((2 ∈ ℕ ∧ 𝑦 ∈ ℕ0) → (2↑𝑦) ∈ ℕ)
226	2, 225	mpan 703	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ0 → (2↑𝑦) ∈ ℕ)
227	226	nncnd 12332	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ0 → (2↑𝑦) ∈ ℂ)
228	226	nnne0d 12369	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ0 → (2↑𝑦) ≠ 0)
229	227, 228	jca 521	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ0 → ((2↑𝑦) ∈ ℂ ∧ (2↑𝑦) ≠ 0))
230	229	ad3antlr 744	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → ((2↑𝑦) ∈ ℂ ∧ (2↑𝑦) ≠ 0))
231		divmul2 11959	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ ((2↑𝑦) ∈ ℂ ∧ (2↑𝑦) ≠ 0)) → ((𝑎 / (2↑𝑦)) = 𝑥 ↔ 𝑎 = ((2↑𝑦) · 𝑥)))
232	222, 224, 230, 231	syl3anc 1398	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → ((𝑎 / (2↑𝑦)) = 𝑥 ↔ 𝑎 = ((2↑𝑦) · 𝑥)))
233	220, 232	mpbird 260	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (𝑎 / (2↑𝑦)) = 𝑥)
234		simpr 490	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))
235	234	oveq2d 7428	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (2↑𝑦) = (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))
236	235	oveq2d 7428	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (𝑎 / (2↑𝑦)) = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))))
237	233, 236	eqtr3d 2798	. . . . . . . . 9 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))))
238	237	ex 418	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) → 𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
239	219, 238	jcai 526	. . . . . . 7 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∧ 𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
240	239	ancomd 467	. . . . . 6 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))
241	139, 240	jca 521	. . . . 5 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))))
242		simprl 783	. . . . . . 7 ⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → 𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))))
243	129	adantr 486	. . . . . . 7 ⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ 𝐽)
244	242, 243	eqeltrd 2861	. . . . . 6 ⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → 𝑥 ∈ 𝐽)
245		simprr 785	. . . . . . 7 ⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))
246	53	adantr 486	. . . . . . 7 ⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℕ0)
247	245, 246	eqeltrd 2861	. . . . . 6 ⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → 𝑦 ∈ ℕ0)
248	117	adantr 486	. . . . . . 7 ⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → 𝑎 = ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
249	245	oveq2d 7428	. . . . . . . 8 ⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → (2↑𝑦) = (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))
250	249, 242	oveq12d 7430	. . . . . . 7 ⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → ((2↑𝑦) · 𝑥) = ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
251	248, 250	eqtr4d 2799	. . . . . 6 ⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → 𝑎 = ((2↑𝑦) · 𝑥))
252	244, 247, 251	jca31 524	. . . . 5 ⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → ((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)))
253	241, 252	impbii 212	. . . 4 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ↔ (𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))))
254	253	a1i 11	. . 3 ⊢ (⊤ → (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ↔ (𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
255	1, 13, 131, 254	f1od2 33293	. 2 ⊢ (⊤ → 𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ)
256	255	mptru 1577	1 ⊢ 𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570  ⊤wtru 1571   ∈ wcel 2145   ≠ wne 2956  ∀wral 3077  ∃wrex 3087  {crab 3413   ⊆ wss 3899  ∅c0 4279   class class class wbr 5103   Or wor 5558   × cxp 5649  –1-1-onto→wf1o 6530  (class class class)co 7412   ∈ cmpo 7414  Fincfn 8957  supcsup 9416  ℂcc 11179  ℝcr 11180  0cc0 11181  1c1 11182   + caddc 11184   · cmul 11186   < clt 11324   ≤ cle 11325   − cmin 11522   / cdiv 11954  ℕcn 12316  2c2 12378  ℕ₀cn0 12587  ℤcz 12674  ...cfz 13620  ↑cexp 14184   ∥ cdvds 16402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7740  ax-cnex 11237  ax-resscn 11238  ax-1cn 11239  ax-icn 11240  ax-addcl 11241  ax-addrcl 11242  ax-mulcl 11243  ax-mulrcl 11244  ax-mulcom 11245  ax-addass 11246  ax-mulass 11247  ax-distr 11248  ax-i2m1 11249  ax-1ne0 11250  ax-1rid 11251  ax-rnegex 11252  ax-rrecex 11253  ax-cnre 11254  ax-pre-lttri 11255  ax-pre-lttrn 11256  ax-pre-ltadd 11257  ax-pre-mulgt0 11258

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6297  df-ord 6358  df-on 6359  df-lim 6360  df-suc 6361  df-iota 6487  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-riota 7369  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7867  df-1st 7990  df-2nd 7991  df-frecs 8283  df-wrecs 8314  df-recs 8363  df-rdg 8402  df-1o 8460  df-er 8701  df-en 8958  df-dom 8959  df-sdom 8960  df-fin 8961  df-sup 9418  df-inf 9419  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-sub 11524  df-neg 11525  df-div 11955  df-nn 12317  df-2 12386  df-n0 12588  df-z 12675  df-uz 12947  df-fz 13621  df-seq 14125  df-exp 14185  df-dvds 16403

This theorem is used by:  eulerpartgbij  34987  eulerpartlemgvv  34991  eulerpartlemgh  34993  eulerpartlemgf  34994