Theorem oddpwdc 31014

Description: Lemma for eulerpart 31042. 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 11448	. . . . . . . 8 ⊢ 2 ∈ ℕ
3	2	a1i 11	. . . . . . 7 ⊢ ((𝑦 ∈ ℕ0 ∧ 𝑥 ∈ 𝐽) → 2 ∈ ℕ)
4		simpl 476	. . . . . . 7 ⊢ ((𝑦 ∈ ℕ0 ∧ 𝑥 ∈ 𝐽) → 𝑦 ∈ ℕ0)
5	3, 4	nnexpcld 13351	. . . . . 6 ⊢ ((𝑦 ∈ ℕ0 ∧ 𝑥 ∈ 𝐽) → (2↑𝑦) ∈ ℕ)
6		oddpwdc.j	. . . . . . . 8 ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}
7		ssrab2 3908	. . . . . . . 8 ⊢ {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} ⊆ ℕ
8	6, 7	eqsstri 3854	. . . . . . 7 ⊢ 𝐽 ⊆ ℕ
9		simpr 479	. . . . . . 7 ⊢ ((𝑦 ∈ ℕ0 ∧ 𝑥 ∈ 𝐽) → 𝑥 ∈ 𝐽)
10	8, 9	sseldi 3819	. . . . . 6 ⊢ ((𝑦 ∈ ℕ0 ∧ 𝑥 ∈ 𝐽) → 𝑥 ∈ ℕ)
11	5, 10	nnmulcld 11428	. . . . 5 ⊢ ((𝑦 ∈ ℕ0 ∧ 𝑥 ∈ 𝐽) → ((2↑𝑦) · 𝑥) ∈ ℕ)
12	11	ancoms 452	. . . 4 ⊢ ((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) → ((2↑𝑦) · 𝑥) ∈ ℕ)
13	12	adantl 475	. . 3 ⊢ ((⊤ ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0)) → ((2↑𝑦) · 𝑥) ∈ ℕ)
14		id 22	. . . . . . 7 ⊢ (𝑎 ∈ ℕ → 𝑎 ∈ ℕ)
15	2	a1i 11	. . . . . . . 8 ⊢ (𝑎 ∈ ℕ → 2 ∈ ℕ)
16		nn0ssre 11646	. . . . . . . . . . 11 ⊢ ℕ0 ⊆ ℝ
17		ltso 10457	. . . . . . . . . . 11 ⊢ < Or ℝ
18		soss 5293	. . . . . . . . . . 11 ⊢ (ℕ0 ⊆ ℝ → ( < Or ℝ → < Or ℕ0))
19	16, 17, 18	mp2 9	. . . . . . . . . 10 ⊢ < Or ℕ0
20	19	a1i 11	. . . . . . . . 9 ⊢ (𝑎 ∈ ℕ → < Or ℕ0)
21		0zd 11740	. . . . . . . . . 10 ⊢ (𝑎 ∈ ℕ → 0 ∈ ℤ)
22		ssrab2 3908	. . . . . . . . . . 11 ⊢ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ⊆ ℕ0
23	22	a1i 11	. . . . . . . . . 10 ⊢ (𝑎 ∈ ℕ → {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ⊆ ℕ0)
24		nnz 11751	. . . . . . . . . . 11 ⊢ (𝑎 ∈ ℕ → 𝑎 ∈ ℤ)
25		oveq2 6930	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑛 → (2↑𝑘) = (2↑𝑛))
26	25	breq1d 4896	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑛 → ((2↑𝑘) ∥ 𝑎 ↔ (2↑𝑛) ∥ 𝑎))
27	26	elrab 3572	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ↔ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎))
28		simprl 761	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → 𝑛 ∈ ℕ0)
29	28	nn0red 11703	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → 𝑛 ∈ ℝ)
30	2	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → 2 ∈ ℕ)
31	30, 28	nnexpcld 13351	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → (2↑𝑛) ∈ ℕ)
32	31	nnred 11391	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → (2↑𝑛) ∈ ℝ)
33		simpl 476	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → 𝑎 ∈ ℕ)
34	33	nnred 11391	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → 𝑎 ∈ ℝ)
35		2re 11449	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℝ
36	35	leidi 10909	. . . . . . . . . . . . . . . 16 ⊢ 2 ≤ 2
37		nexple 30669	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ ℕ0 ∧ 2 ∈ ℝ ∧ 2 ≤ 2) → 𝑛 ≤ (2↑𝑛))
38	35, 36, 37	mp3an23 1526	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ0 → 𝑛 ≤ (2↑𝑛))
39	38	ad2antrl 718	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → 𝑛 ≤ (2↑𝑛))
40	31	nnzd 11833	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → (2↑𝑛) ∈ ℤ)
41		simprr 763	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → (2↑𝑛) ∥ 𝑎)
42		dvdsle 15439	. . . . . . . . . . . . . . . 16 ⊢ (((2↑𝑛) ∈ ℤ ∧ 𝑎 ∈ ℕ) → ((2↑𝑛) ∥ 𝑎 → (2↑𝑛) ≤ 𝑎))
43	42	imp 397	. . . . . . . . . . . . . . 15 ⊢ ((((2↑𝑛) ∈ ℤ ∧ 𝑎 ∈ ℕ) ∧ (2↑𝑛) ∥ 𝑎) → (2↑𝑛) ≤ 𝑎)
44	40, 33, 41, 43	syl21anc 828	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → (2↑𝑛) ≤ 𝑎)
45	29, 32, 34, 39, 44	letrd 10533	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → 𝑛 ≤ 𝑎)
46	27, 45	sylan2b 587	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}) → 𝑛 ≤ 𝑎)
47	46	ralrimiva 3148	. . . . . . . . . . 11 ⊢ (𝑎 ∈ ℕ → ∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}𝑛 ≤ 𝑎)
48		brralrspcev 4946	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ ℤ ∧ ∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}𝑛 ≤ 𝑎) → ∃𝑚 ∈ ℤ ∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}𝑛 ≤ 𝑚)
49	24, 47, 48	syl2anc 579	. . . . . . . . . 10 ⊢ (𝑎 ∈ ℕ → ∃𝑚 ∈ ℤ ∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}𝑛 ≤ 𝑚)
50		nn0uz 12028	. . . . . . . . . . 11 ⊢ ℕ0 = (ℤ≥‘0)
51	50	uzsupss 12087	. . . . . . . . . 10 ⊢ ((0 ∈ ℤ ∧ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ⊆ ℕ0 ∧ ∃𝑚 ∈ ℤ ∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}𝑛 ≤ 𝑚) → ∃𝑚 ∈ ℕ0 (∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ¬ 𝑚 < 𝑛 ∧ ∀𝑛 ∈ ℕ0 (𝑛 < 𝑚 → ∃𝑜 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}𝑛 < 𝑜)))
52	21, 23, 49, 51	syl3anc 1439	. . . . . . . . 9 ⊢ (𝑎 ∈ ℕ → ∃𝑚 ∈ ℕ0 (∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ¬ 𝑚 < 𝑛 ∧ ∀𝑛 ∈ ℕ0 (𝑛 < 𝑚 → ∃𝑜 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}𝑛 < 𝑜)))
53	20, 52	supcl 8652	. . . . . . . 8 ⊢ (𝑎 ∈ ℕ → sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℕ0)
54	15, 53	nnexpcld 13351	. . . . . . 7 ⊢ (𝑎 ∈ ℕ → (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∈ ℕ)
55		fzfi 13090	. . . . . . . . . . . 12 ⊢ (0...𝑎) ∈ Fin
56		0zd 11740	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}) → 0 ∈ ℤ)
57	24	adantr 474	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}) → 𝑎 ∈ ℤ)
58	27, 28	sylan2b 587	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}) → 𝑛 ∈ ℕ0)
59	58	nn0zd 11832	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}) → 𝑛 ∈ ℤ)
60	58	nn0ge0d 11705	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}) → 0 ≤ 𝑛)
61		elfz4 12652	. . . . . . . . . . . . . . 15 ⊢ (((0 ∈ ℤ ∧ 𝑎 ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ (0 ≤ 𝑛 ∧ 𝑛 ≤ 𝑎)) → 𝑛 ∈ (0...𝑎))
62	56, 57, 59, 60, 46, 61	syl32anc 1446	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}) → 𝑛 ∈ (0...𝑎))
63	62	ex 403	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ ℕ → (𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} → 𝑛 ∈ (0...𝑎)))
64	63	ssrdv 3827	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ ℕ → {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ⊆ (0...𝑎))
65		ssfi 8468	. . . . . . . . . . . 12 ⊢ (((0...𝑎) ∈ Fin ∧ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ⊆ (0...𝑎)) → {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ∈ Fin)
66	55, 64, 65	sylancr 581	. . . . . . . . . . 11 ⊢ (𝑎 ∈ ℕ → {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ∈ Fin)
67		0nn0 11659	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℕ0
68	67	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ ℕ → 0 ∈ ℕ0)
69		2cn 11450	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℂ
70		exp0 13182	. . . . . . . . . . . . . . 15 ⊢ (2 ∈ ℂ → (2↑0) = 1)
71	69, 70	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ (2↑0) = 1
72		1dvds 15403	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ ℤ → 1 ∥ 𝑎)
73	24, 72	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ ℕ → 1 ∥ 𝑎)
74	71, 73	syl5eqbr 4921	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ ℕ → (2↑0) ∥ 𝑎)
75		oveq2 6930	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 0 → (2↑𝑘) = (2↑0))
76	75	breq1d 4896	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 0 → ((2↑𝑘) ∥ 𝑎 ↔ (2↑0) ∥ 𝑎))
77	76	elrab 3572	. . . . . . . . . . . . 13 ⊢ (0 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ↔ (0 ∈ ℕ0 ∧ (2↑0) ∥ 𝑎))
78	68, 74, 77	sylanbrc 578	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ ℕ → 0 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎})
79	78	ne0d 4150	. . . . . . . . . . 11 ⊢ (𝑎 ∈ ℕ → {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ≠ ∅)
80		fisupcl 8663	. . . . . . . . . . 11 ⊢ (( < Or ℕ0 ∧ ({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ∈ Fin ∧ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ≠ ∅ ∧ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ⊆ ℕ0)) → sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎})
81	20, 66, 79, 23, 80	syl13anc 1440	. . . . . . . . . 10 ⊢ (𝑎 ∈ ℕ → sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎})
82		oveq2 6930	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑙 → (2↑𝑘) = (2↑𝑙))
83	82	breq1d 4896	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑙 → ((2↑𝑘) ∥ 𝑎 ↔ (2↑𝑙) ∥ 𝑎))
84	83	cbvrabv 3396	. . . . . . . . . 10 ⊢ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} = {𝑙 ∈ ℕ0 ∣ (2↑𝑙) ∥ 𝑎}
85	81, 84	syl6eleq 2869	. . . . . . . . 9 ⊢ (𝑎 ∈ ℕ → sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ {𝑙 ∈ ℕ0 ∣ (2↑𝑙) ∥ 𝑎})
86		oveq2 6930	. . . . . . . . . . 11 ⊢ (𝑙 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) → (2↑𝑙) = (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))
87	86	breq1d 4896	. . . . . . . . . 10 ⊢ (𝑙 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) → ((2↑𝑙) ∥ 𝑎 ↔ (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∥ 𝑎))
88	87	elrab 3572	. . . . . . . . 9 ⊢ (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ {𝑙 ∈ ℕ0 ∣ (2↑𝑙) ∥ 𝑎} ↔ (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℕ0 ∧ (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∥ 𝑎))
89	85, 88	sylib 210	. . . . . . . 8 ⊢ (𝑎 ∈ ℕ → (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℕ0 ∧ (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∥ 𝑎))
90	89	simprd 491	. . . . . . 7 ⊢ (𝑎 ∈ ℕ → (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∥ 𝑎)
91		nndivdvds 15396	. . . . . . . 8 ⊢ ((𝑎 ∈ ℕ ∧ (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∈ ℕ) → ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∥ 𝑎 ↔ (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ ℕ))
92	91	biimpa 470	. . . . . . 7 ⊢ (((𝑎 ∈ ℕ ∧ (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∈ ℕ) ∧ (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∥ 𝑎) → (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ ℕ)
93	14, 54, 90, 92	syl21anc 828	. . . . . 6 ⊢ (𝑎 ∈ ℕ → (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ ℕ)
94		1nn0 11660	. . . . . . . . . . 11 ⊢ 1 ∈ ℕ0
95	94	a1i 11	. . . . . . . . . 10 ⊢ (𝑎 ∈ ℕ → 1 ∈ ℕ0)
96	53, 95	nn0addcld 11706	. . . . . . . . 9 ⊢ (𝑎 ∈ ℕ → (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈ ℕ0)
97	53	nn0red 11703	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ ℕ → sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℝ)
98	97	ltp1d 11308	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ ℕ → sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) < (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1))
99	20, 52	supub 8653	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ ℕ → ((sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} → ¬ sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) < (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)))
100	98, 99	mt2d 134	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ ℕ → ¬ (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎})
101	84	eleq2i 2851	. . . . . . . . . . . 12 ⊢ ((sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ↔ (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈ {𝑙 ∈ ℕ0 ∣ (2↑𝑙) ∥ 𝑎})
102	100, 101	sylnib 320	. . . . . . . . . . 11 ⊢ (𝑎 ∈ ℕ → ¬ (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈ {𝑙 ∈ ℕ0 ∣ (2↑𝑙) ∥ 𝑎})
103		oveq2 6930	. . . . . . . . . . . . 13 ⊢ (𝑙 = (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) → (2↑𝑙) = (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)))
104	103	breq1d 4896	. . . . . . . . . . . 12 ⊢ (𝑙 = (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) → ((2↑𝑙) ∥ 𝑎 ↔ (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) ∥ 𝑎))
105	104	elrab 3572	. . . . . . . . . . 11 ⊢ ((sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈ {𝑙 ∈ ℕ0 ∣ (2↑𝑙) ∥ 𝑎} ↔ ((sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈ ℕ0 ∧ (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) ∥ 𝑎))
106	102, 105	sylnib 320	. . . . . . . . . 10 ⊢ (𝑎 ∈ ℕ → ¬ ((sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈ ℕ0 ∧ (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) ∥ 𝑎))
107		imnan 390	. . . . . . . . . 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)) ∥ 𝑎))
108	106, 107	sylibr 226	. . . . . . . . 9 ⊢ (𝑎 ∈ ℕ → ((sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈ ℕ0 → ¬ (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) ∥ 𝑎))
109	96, 108	mpd 15	. . . . . . . 8 ⊢ (𝑎 ∈ ℕ → ¬ (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) ∥ 𝑎)
110		expp1 13185	. . . . . . . . . 10 ⊢ ((2 ∈ ℂ ∧ sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℕ0) → (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) = ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2))
111	69, 53, 110	sylancr 581	. . . . . . . . 9 ⊢ (𝑎 ∈ ℕ → (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) = ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2))
112	111	breq1d 4896	. . . . . . . 8 ⊢ (𝑎 ∈ ℕ → ((2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) ∥ 𝑎 ↔ ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2) ∥ 𝑎))
113	109, 112	mtbid 316	. . . . . . 7 ⊢ (𝑎 ∈ ℕ → ¬ ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2) ∥ 𝑎)
114		nncn 11383	. . . . . . . . . . 11 ⊢ (𝑎 ∈ ℕ → 𝑎 ∈ ℂ)
115	54	nncnd 11392	. . . . . . . . . . 11 ⊢ (𝑎 ∈ ℕ → (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∈ ℂ)
116	54	nnne0d 11425	. . . . . . . . . . 11 ⊢ (𝑎 ∈ ℕ → (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ≠ 0)
117	114, 115, 116	divcan2d 11153	. . . . . . . . . 10 ⊢ (𝑎 ∈ ℕ → ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))) = 𝑎)
118	117	eqcomd 2784	. . . . . . . . 9 ⊢ (𝑎 ∈ ℕ → 𝑎 = ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
119	118	breq2d 4898	. . . . . . . 8 ⊢ (𝑎 ∈ ℕ → (((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2) ∥ 𝑎 ↔ ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2) ∥ ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))))))
120	15	nnzd 11833	. . . . . . . . 9 ⊢ (𝑎 ∈ ℕ → 2 ∈ ℤ)
121	93	nnzd 11833	. . . . . . . . 9 ⊢ (𝑎 ∈ ℕ → (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ ℤ)
122	54	nnzd 11833	. . . . . . . . 9 ⊢ (𝑎 ∈ ℕ → (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∈ ℤ)
123		dvdscmulr 15417	. . . . . . . . 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, < )))))
124	120, 121, 122, 116, 123	syl112anc 1442	. . . . . . . 8 ⊢ (𝑎 ∈ ℕ → (((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2) ∥ ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))) ↔ 2 ∥ (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
125	119, 124	bitrd 271	. . . . . . 7 ⊢ (𝑎 ∈ ℕ → (((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2) ∥ 𝑎 ↔ 2 ∥ (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
126	113, 125	mtbid 316	. . . . . 6 ⊢ (𝑎 ∈ ℕ → ¬ 2 ∥ (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))))
127		breq2 4890	. . . . . . . 8 ⊢ (𝑧 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → (2 ∥ 𝑧 ↔ 2 ∥ (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
128	127	notbid 310	. . . . . . 7 ⊢ (𝑧 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → (¬ 2 ∥ 𝑧 ↔ ¬ 2 ∥ (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
129	128, 6	elrab2 3576	. . . . . 6 ⊢ ((𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ 𝐽 ↔ ((𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ ℕ ∧ ¬ 2 ∥ (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
130	93, 126, 129	sylanbrc 578	. . . . 5 ⊢ (𝑎 ∈ ℕ → (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ 𝐽)
131	130, 53	jca 507	. . . 4 ⊢ (𝑎 ∈ ℕ → ((𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ 𝐽 ∧ sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℕ0))
132	131	adantl 475	. . 3 ⊢ ((⊤ ∧ 𝑎 ∈ ℕ) → ((𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ 𝐽 ∧ sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℕ0))
133		simpr 479	. . . . . . 7 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑎 = ((2↑𝑦) · 𝑥))
134	2	a1i 11	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 2 ∈ ℕ)
135		simplr 759	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑦 ∈ ℕ0)
136	134, 135	nnexpcld 13351	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (2↑𝑦) ∈ ℕ)
137	8	sseli 3817	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐽 → 𝑥 ∈ ℕ)
138	137	ad2antrr 716	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑥 ∈ ℕ)
139	136, 138	nnmulcld 11428	. . . . . . 7 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → ((2↑𝑦) · 𝑥) ∈ ℕ)
140	133, 139	eqeltrd 2859	. . . . . 6 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑎 ∈ ℕ)
141		simplll 765	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑥 ∈ 𝐽)
142		breq2 4890	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑥 → (2 ∥ 𝑧 ↔ 2 ∥ 𝑥))
143	142	notbid 310	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑥 → (¬ 2 ∥ 𝑧 ↔ ¬ 2 ∥ 𝑥))
144	143, 6	elrab2 3576	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐽 ↔ (𝑥 ∈ ℕ ∧ ¬ 2 ∥ 𝑥))
145	144	simprbi 492	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐽 → ¬ 2 ∥ 𝑥)
146		2z 11761	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℤ
147	135	adantr 474	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑦 ∈ ℕ0)
148	147	nn0zd 11832	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑦 ∈ ℤ)
149	19	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → < Or ℕ0)
150	140, 52	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → ∃𝑚 ∈ ℕ0 (∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ¬ 𝑚 < 𝑛 ∧ ∀𝑛 ∈ ℕ0 (𝑛 < 𝑚 → ∃𝑜 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}𝑛 < 𝑜)))
151	150	adantr 474	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → ∃𝑚 ∈ ℕ0 (∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ¬ 𝑚 < 𝑛 ∧ ∀𝑛 ∈ ℕ0 (𝑛 < 𝑚 → ∃𝑜 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}𝑛 < 𝑜)))
152	149, 151	supcl 8652	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℕ0)
153	152	nn0zd 11832	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℤ)
154		simpr 479	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))
155		znnsub 11775	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ ℤ ∧ sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℤ) → (𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ↔ (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦) ∈ ℕ))
156	155	biimpa 470	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 ∈ ℤ ∧ sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℤ) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦) ∈ ℕ)
157	148, 153, 154, 156	syl21anc 828	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦) ∈ ℕ)
158		iddvdsexp 15412	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℤ ∧ (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦) ∈ ℕ) → 2 ∥ (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)))
159	146, 157, 158	sylancr 581	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 2 ∥ (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)))
160	146	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 2 ∈ ℤ)
161	140, 121	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ ℤ)
162	161	adantr 474	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ ℤ)
163	157	nnnn0d 11702	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦) ∈ ℕ0)
164		zexpcl 13193	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℤ ∧ (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦) ∈ ℕ0) → (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) ∈ ℤ)
165	146, 163, 164	sylancr 581	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) ∈ ℤ)
166		dvdsmultr2 15428	. . . . . . . . . . . . . 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, < ) − 𝑦)))))
167	160, 162, 165, 166	syl3anc 1439	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (2 ∥ (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) → 2 ∥ ((𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) · (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)))))
168	159, 167	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 2 ∥ ((𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) · (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦))))
169	138	adantr 474	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑥 ∈ ℕ)
170	169	nncnd 11392	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑥 ∈ ℂ)
171		2cnd 11453	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 2 ∈ ℂ)
172	171, 163	expcld 13327	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) ∈ ℂ)
173	140	adantr 474	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑎 ∈ ℕ)
174	173	nncnd 11392	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑎 ∈ ℂ)
175	173, 115	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∈ ℂ)
176		2ne0 11486	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ≠ 0
177	176	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 2 ≠ 0)
178	171, 177, 153	expne0d 13333	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ≠ 0)
179	174, 175, 178	divcld 11151	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ ℂ)
180	172, 179	mulcld 10397	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → ((2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))) ∈ ℂ)
181	171, 147	expcld 13327	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (2↑𝑦) ∈ ℂ)
182	171, 177, 148	expne0d 13333	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (2↑𝑦) ≠ 0)
183	173, 118	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑎 = ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
184		simplr 759	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑎 = ((2↑𝑦) · 𝑥))
185	147	nn0cnd 11704	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑦 ∈ ℂ)
186	152	nn0cnd 11704	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℂ)
187	185, 186	pncan3d 10737	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (𝑦 + (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))
188	187	oveq2d 6938	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (2↑(𝑦 + (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦))) = (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))
189	171, 163, 147	expaddd 13329	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (2↑(𝑦 + (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦))) = ((2↑𝑦) · (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦))))
190	188, 189	eqtr3d 2816	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) = ((2↑𝑦) · (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦))))
191	190	oveq1d 6937	. . . . . . . . . . . . . . . 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, < )))))
192	183, 184, 191	3eqtr3d 2822	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → ((2↑𝑦) · 𝑥) = (((2↑𝑦) · (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦))) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
193	181, 172, 179	mulassd 10400	. . . . . . . . . . . . . . 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, < ))))))
194	192, 193	eqtrd 2814	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → ((2↑𝑦) · 𝑥) = ((2↑𝑦) · ((2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))))))
195	170, 180, 181, 182, 194	mulcanad 11010	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑥 = ((2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
196	179, 172	mulcomd 10398	. . . . . . . . . . . . 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, < )))))
197	195, 196	eqtr4d 2817	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑥 = ((𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) · (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦))))
198	168, 197	breqtrrd 4914	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 2 ∥ 𝑥)
199	145, 198	nsyl3 136	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → ¬ 𝑥 ∈ 𝐽)
200	141, 199	pm2.65da 807	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → ¬ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))
201	138	nnzd 11833	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑥 ∈ ℤ)
202	136	nnzd 11833	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (2↑𝑦) ∈ ℤ)
203	140	nnzd 11833	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑎 ∈ ℤ)
204	136	nncnd 11392	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (2↑𝑦) ∈ ℂ)
205	138	nncnd 11392	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑥 ∈ ℂ)
206	204, 205	mulcomd 10398	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → ((2↑𝑦) · 𝑥) = (𝑥 · (2↑𝑦)))
207	133, 206	eqtr2d 2815	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑥 · (2↑𝑦)) = 𝑎)
208		dvds0lem 15399	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℤ ∧ (2↑𝑦) ∈ ℤ ∧ 𝑎 ∈ ℤ) ∧ (𝑥 · (2↑𝑦)) = 𝑎) → (2↑𝑦) ∥ 𝑎)
209	201, 202, 203, 207, 208	syl31anc 1441	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (2↑𝑦) ∥ 𝑎)
210		oveq2 6930	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑦 → (2↑𝑘) = (2↑𝑦))
211	210	breq1d 4896	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑦 → ((2↑𝑘) ∥ 𝑎 ↔ (2↑𝑦) ∥ 𝑎))
212	211	elrab 3572	. . . . . . . . . . 11 ⊢ (𝑦 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ↔ (𝑦 ∈ ℕ0 ∧ (2↑𝑦) ∥ 𝑎))
213	135, 209, 212	sylanbrc 578	. . . . . . . . . 10 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑦 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎})
214	19	a1i 11	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → < Or ℕ0)
215	214, 150	supub 8653	. . . . . . . . . 10 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑦 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} → ¬ sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) < 𝑦))
216	213, 215	mpd 15	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → ¬ sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) < 𝑦)
217	135	nn0red 11703	. . . . . . . . . 10 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑦 ∈ ℝ)
218	140, 97	syl 17	. . . . . . . . . 10 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℝ)
219	217, 218	lttri3d 10516	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ↔ (¬ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∧ ¬ sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) < 𝑦)))
220	200, 216, 219	mpbir2and 703	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))
221		simplr 759	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑎 = ((2↑𝑦) · 𝑥))
222	140	adantr 474	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑎 ∈ ℕ)
223	222	nncnd 11392	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑎 ∈ ℂ)
224	138	adantr 474	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑥 ∈ ℕ)
225	224	nncnd 11392	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑥 ∈ ℂ)
226		nnexpcl 13191	. . . . . . . . . . . . . . . 16 ⊢ ((2 ∈ ℕ ∧ 𝑦 ∈ ℕ0) → (2↑𝑦) ∈ ℕ)
227	2, 226	mpan 680	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ0 → (2↑𝑦) ∈ ℕ)
228	227	nncnd 11392	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ0 → (2↑𝑦) ∈ ℂ)
229	227	nnne0d 11425	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ0 → (2↑𝑦) ≠ 0)
230	228, 229	jca 507	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ0 → ((2↑𝑦) ∈ ℂ ∧ (2↑𝑦) ≠ 0))
231	230	ad3antlr 721	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → ((2↑𝑦) ∈ ℂ ∧ (2↑𝑦) ≠ 0))
232		divmul2 11037	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ ((2↑𝑦) ∈ ℂ ∧ (2↑𝑦) ≠ 0)) → ((𝑎 / (2↑𝑦)) = 𝑥 ↔ 𝑎 = ((2↑𝑦) · 𝑥)))
233	223, 225, 231, 232	syl3anc 1439	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → ((𝑎 / (2↑𝑦)) = 𝑥 ↔ 𝑎 = ((2↑𝑦) · 𝑥)))
234	221, 233	mpbird 249	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (𝑎 / (2↑𝑦)) = 𝑥)
235		simpr 479	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))
236	235	oveq2d 6938	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (2↑𝑦) = (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))
237	236	oveq2d 6938	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (𝑎 / (2↑𝑦)) = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))))
238	234, 237	eqtr3d 2816	. . . . . . . . 9 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))))
239	238	ex 403	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) → 𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
240	220, 239	jcai 512	. . . . . . 7 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∧ 𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
241	240	ancomd 455	. . . . . 6 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))
242	140, 241	jca 507	. . . . 5 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))))
243		simprl 761	. . . . . . 7 ⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → 𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))))
244	130	adantr 474	. . . . . . 7 ⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ 𝐽)
245	243, 244	eqeltrd 2859	. . . . . 6 ⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → 𝑥 ∈ 𝐽)
246		simprr 763	. . . . . . 7 ⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))
247	53	adantr 474	. . . . . . 7 ⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℕ0)
248	246, 247	eqeltrd 2859	. . . . . 6 ⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → 𝑦 ∈ ℕ0)
249	118	adantr 474	. . . . . . 7 ⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → 𝑎 = ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
250	246	oveq2d 6938	. . . . . . . 8 ⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → (2↑𝑦) = (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))
251	250, 243	oveq12d 6940	. . . . . . 7 ⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → ((2↑𝑦) · 𝑥) = ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
252	249, 251	eqtr4d 2817	. . . . . 6 ⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → 𝑎 = ((2↑𝑦) · 𝑥))
253	245, 248, 252	jca31 510	. . . . 5 ⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → ((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)))
254	242, 253	impbii 201	. . . 4 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ↔ (𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))))
255	254	a1i 11	. . 3 ⊢ (⊤ → (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ↔ (𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
256	1, 13, 132, 255	f1od2 30065	. 2 ⊢ (⊤ → 𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ)
257	256	mptru 1609	1 ⊢ 𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   ∧ wa 386   = wceq 1601  ⊤wtru 1602   ∈ wcel 2107   ≠ wne 2969  ∀wral 3090  ∃wrex 3091  {crab 3094   ⊆ wss 3792  ∅c0 4141   class class class wbr 4886   Or wor 5273   × cxp 5353  –1-1-onto→wf1o 6134  (class class class)co 6922   ↦ cmpt2 6924  Fincfn 8241  supcsup 8634  ℂcc 10270  ℝcr 10271  0cc0 10272  1c1 10273   + caddc 10275   · cmul 10277   < clt 10411   ≤ cle 10412   − cmin 10606   / cdiv 11032  ℕcn 11374  2c2 11430  ℕ₀cn0 11642  ℤcz 11728  ...cfz 12643  ↑cexp 13178   ∥ cdvds 15387

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-cnex 10328  ax-resscn 10329  ax-1cn 10330  ax-icn 10331  ax-addcl 10332  ax-addrcl 10333  ax-mulcl 10334  ax-mulrcl 10335  ax-mulcom 10336  ax-addass 10337  ax-mulass 10338  ax-distr 10339  ax-i2m1 10340  ax-1ne0 10341  ax-1rid 10342  ax-rnegex 10343  ax-rrecex 10344  ax-cnre 10345  ax-pre-lttri 10346  ax-pre-lttrn 10347  ax-pre-ltadd 10348  ax-pre-mulgt0 10349

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-fal 1615  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-reu 3097  df-rmo 3098  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4672  df-iun 4755  df-br 4887  df-opab 4949  df-mpt 4966  df-tr 4988  df-id 5261  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-we 5316  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-pred 5933  df-ord 5979  df-on 5980  df-lim 5981  df-suc 5982  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-riota 6883  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-om 7344  df-1st 7445  df-2nd 7446  df-wrecs 7689  df-recs 7751  df-rdg 7789  df-1o 7843  df-er 8026  df-en 8242  df-dom 8243  df-sdom 8244  df-fin 8245  df-sup 8636  df-inf 8637  df-pnf 10413  df-mnf 10414  df-xr 10415  df-ltxr 10416  df-le 10417  df-sub 10608  df-neg 10609  df-div 11033  df-nn 11375  df-2 11438  df-n0 11643  df-z 11729  df-uz 11993  df-fz 12644  df-seq 13120  df-exp 13179  df-dvds 15388

This theorem is referenced by:  eulerpartgbij  31032  eulerpartlemgvv  31036  eulerpartlemgh  31038  eulerpartlemgf  31039