Theorem oddpwdc 32308

Description: Lemma for eulerpart 32336. 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 12035	. . . . . . . 8 ⊢ 2 ∈ ℕ
3	2	a1i 11	. . . . . . 7 ⊢ ((𝑦 ∈ ℕ0 ∧ 𝑥 ∈ 𝐽) → 2 ∈ ℕ)
4		simpl 483	. . . . . . 7 ⊢ ((𝑦 ∈ ℕ0 ∧ 𝑥 ∈ 𝐽) → 𝑦 ∈ ℕ0)
5	3, 4	nnexpcld 13949	. . . . . 6 ⊢ ((𝑦 ∈ ℕ0 ∧ 𝑥 ∈ 𝐽) → (2↑𝑦) ∈ ℕ)
6		oddpwdc.j	. . . . . . . 8 ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}
7		ssrab2 4014	. . . . . . . 8 ⊢ {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} ⊆ ℕ
8	6, 7	eqsstri 3956	. . . . . . 7 ⊢ 𝐽 ⊆ ℕ
9		simpr 485	. . . . . . 7 ⊢ ((𝑦 ∈ ℕ0 ∧ 𝑥 ∈ 𝐽) → 𝑥 ∈ 𝐽)
10	8, 9	sselid 3920	. . . . . 6 ⊢ ((𝑦 ∈ ℕ0 ∧ 𝑥 ∈ 𝐽) → 𝑥 ∈ ℕ)
11	5, 10	nnmulcld 12015	. . . . 5 ⊢ ((𝑦 ∈ ℕ0 ∧ 𝑥 ∈ 𝐽) → ((2↑𝑦) · 𝑥) ∈ ℕ)
12	11	ancoms 459	. . . 4 ⊢ ((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) → ((2↑𝑦) · 𝑥) ∈ ℕ)
13	12	adantl 482	. . 3 ⊢ ((⊤ ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0)) → ((2↑𝑦) · 𝑥) ∈ ℕ)
14		id 22	. . . . . . 7 ⊢ (𝑎 ∈ ℕ → 𝑎 ∈ ℕ)
15	2	a1i 11	. . . . . . . 8 ⊢ (𝑎 ∈ ℕ → 2 ∈ ℕ)
16		nn0ssre 12226	. . . . . . . . . . 11 ⊢ ℕ0 ⊆ ℝ
17		ltso 11044	. . . . . . . . . . 11 ⊢ < Or ℝ
18		soss 5520	. . . . . . . . . . 11 ⊢ (ℕ0 ⊆ ℝ → ( < Or ℝ → < Or ℕ0))
19	16, 17, 18	mp2 9	. . . . . . . . . 10 ⊢ < Or ℕ0
20	19	a1i 11	. . . . . . . . 9 ⊢ (𝑎 ∈ ℕ → < Or ℕ0)
21		0zd 12320	. . . . . . . . . 10 ⊢ (𝑎 ∈ ℕ → 0 ∈ ℤ)
22		ssrab2 4014	. . . . . . . . . . 11 ⊢ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ⊆ ℕ0
23	22	a1i 11	. . . . . . . . . 10 ⊢ (𝑎 ∈ ℕ → {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ⊆ ℕ0)
24		nnz 12331	. . . . . . . . . . 11 ⊢ (𝑎 ∈ ℕ → 𝑎 ∈ ℤ)
25		oveq2 7277	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑛 → (2↑𝑘) = (2↑𝑛))
26	25	breq1d 5085	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑛 → ((2↑𝑘) ∥ 𝑎 ↔ (2↑𝑛) ∥ 𝑎))
27	26	elrab 3625	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ↔ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎))
28		simprl 768	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → 𝑛 ∈ ℕ0)
29	28	nn0red 12283	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → 𝑛 ∈ ℝ)
30	2	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → 2 ∈ ℕ)
31	30, 28	nnexpcld 13949	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → (2↑𝑛) ∈ ℕ)
32	31	nnred 11977	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → (2↑𝑛) ∈ ℝ)
33		simpl 483	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → 𝑎 ∈ ℕ)
34	33	nnred 11977	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → 𝑎 ∈ ℝ)
35		2re 12036	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℝ
36	35	leidi 11498	. . . . . . . . . . . . . . . 16 ⊢ 2 ≤ 2
37		nexple 31964	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ ℕ0 ∧ 2 ∈ ℝ ∧ 2 ≤ 2) → 𝑛 ≤ (2↑𝑛))
38	35, 36, 37	mp3an23 1452	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ0 → 𝑛 ≤ (2↑𝑛))
39	38	ad2antrl 725	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → 𝑛 ≤ (2↑𝑛))
40	31	nnzd 12414	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → (2↑𝑛) ∈ ℤ)
41		simprr 770	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → (2↑𝑛) ∥ 𝑎)
42		dvdsle 16008	. . . . . . . . . . . . . . . 16 ⊢ (((2↑𝑛) ∈ ℤ ∧ 𝑎 ∈ ℕ) → ((2↑𝑛) ∥ 𝑎 → (2↑𝑛) ≤ 𝑎))
43	42	imp 407	. . . . . . . . . . . . . . 15 ⊢ ((((2↑𝑛) ∈ ℤ ∧ 𝑎 ∈ ℕ) ∧ (2↑𝑛) ∥ 𝑎) → (2↑𝑛) ≤ 𝑎)
44	40, 33, 41, 43	syl21anc 835	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → (2↑𝑛) ≤ 𝑎)
45	29, 32, 34, 39, 44	letrd 11121	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → 𝑛 ≤ 𝑎)
46	27, 45	sylan2b 594	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}) → 𝑛 ≤ 𝑎)
47	46	ralrimiva 3103	. . . . . . . . . . 11 ⊢ (𝑎 ∈ ℕ → ∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}𝑛 ≤ 𝑎)
48		brralrspcev 5135	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ ℤ ∧ ∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}𝑛 ≤ 𝑎) → ∃𝑚 ∈ ℤ ∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}𝑛 ≤ 𝑚)
49	24, 47, 48	syl2anc 584	. . . . . . . . . 10 ⊢ (𝑎 ∈ ℕ → ∃𝑚 ∈ ℤ ∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}𝑛 ≤ 𝑚)
50		nn0uz 12609	. . . . . . . . . . 11 ⊢ ℕ0 = (ℤ≥‘0)
51	50	uzsupss 12669	. . . . . . . . . 10 ⊢ ((0 ∈ ℤ ∧ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ⊆ ℕ0 ∧ ∃𝑚 ∈ ℤ ∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}𝑛 ≤ 𝑚) → ∃𝑚 ∈ ℕ0 (∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ¬ 𝑚 < 𝑛 ∧ ∀𝑛 ∈ ℕ0 (𝑛 < 𝑚 → ∃𝑜 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}𝑛 < 𝑜)))
52	21, 23, 49, 51	syl3anc 1370	. . . . . . . . 9 ⊢ (𝑎 ∈ ℕ → ∃𝑚 ∈ ℕ0 (∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ¬ 𝑚 < 𝑛 ∧ ∀𝑛 ∈ ℕ0 (𝑛 < 𝑚 → ∃𝑜 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}𝑛 < 𝑜)))
53	20, 52	supcl 9206	. . . . . . . 8 ⊢ (𝑎 ∈ ℕ → sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℕ0)
54	15, 53	nnexpcld 13949	. . . . . . 7 ⊢ (𝑎 ∈ ℕ → (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∈ ℕ)
55		fzfi 13681	. . . . . . . . . . . 12 ⊢ (0...𝑎) ∈ Fin
56		0zd 12320	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}) → 0 ∈ ℤ)
57	24	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}) → 𝑎 ∈ ℤ)
58	27, 28	sylan2b 594	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}) → 𝑛 ∈ ℕ0)
59	58	nn0zd 12413	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}) → 𝑛 ∈ ℤ)
60	58	nn0ge0d 12285	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}) → 0 ≤ 𝑛)
61	56, 57, 59, 60, 46	elfzd 13236	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}) → 𝑛 ∈ (0...𝑎))
62	61	ex 413	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ ℕ → (𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} → 𝑛 ∈ (0...𝑎)))
63	62	ssrdv 3928	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ ℕ → {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ⊆ (0...𝑎))
64		ssfi 8945	. . . . . . . . . . . 12 ⊢ (((0...𝑎) ∈ Fin ∧ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ⊆ (0...𝑎)) → {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ∈ Fin)
65	55, 63, 64	sylancr 587	. . . . . . . . . . 11 ⊢ (𝑎 ∈ ℕ → {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ∈ Fin)
66		0nn0 12237	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℕ0
67	66	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ ℕ → 0 ∈ ℕ0)
68		2cn 12037	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℂ
69		exp0 13775	. . . . . . . . . . . . . . 15 ⊢ (2 ∈ ℂ → (2↑0) = 1)
70	68, 69	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ (2↑0) = 1
71		1dvds 15969	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ ℤ → 1 ∥ 𝑎)
72	24, 71	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ ℕ → 1 ∥ 𝑎)
73	70, 72	eqbrtrid 5110	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ ℕ → (2↑0) ∥ 𝑎)
74		oveq2 7277	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 0 → (2↑𝑘) = (2↑0))
75	74	breq1d 5085	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 0 → ((2↑𝑘) ∥ 𝑎 ↔ (2↑0) ∥ 𝑎))
76	75	elrab 3625	. . . . . . . . . . . . 13 ⊢ (0 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ↔ (0 ∈ ℕ0 ∧ (2↑0) ∥ 𝑎))
77	67, 73, 76	sylanbrc 583	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ ℕ → 0 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎})
78	77	ne0d 4271	. . . . . . . . . . 11 ⊢ (𝑎 ∈ ℕ → {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ≠ ∅)
79		fisupcl 9217	. . . . . . . . . . 11 ⊢ (( < Or ℕ0 ∧ ({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ∈ Fin ∧ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ≠ ∅ ∧ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ⊆ ℕ0)) → sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎})
80	20, 65, 78, 23, 79	syl13anc 1371	. . . . . . . . . 10 ⊢ (𝑎 ∈ ℕ → sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎})
81		oveq2 7277	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑙 → (2↑𝑘) = (2↑𝑙))
82	81	breq1d 5085	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑙 → ((2↑𝑘) ∥ 𝑎 ↔ (2↑𝑙) ∥ 𝑎))
83	82	cbvrabv 3425	. . . . . . . . . 10 ⊢ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} = {𝑙 ∈ ℕ0 ∣ (2↑𝑙) ∥ 𝑎}
84	80, 83	eleqtrdi 2849	. . . . . . . . 9 ⊢ (𝑎 ∈ ℕ → sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ {𝑙 ∈ ℕ0 ∣ (2↑𝑙) ∥ 𝑎})
85		oveq2 7277	. . . . . . . . . . 11 ⊢ (𝑙 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) → (2↑𝑙) = (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))
86	85	breq1d 5085	. . . . . . . . . 10 ⊢ (𝑙 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) → ((2↑𝑙) ∥ 𝑎 ↔ (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∥ 𝑎))
87	86	elrab 3625	. . . . . . . . 9 ⊢ (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ {𝑙 ∈ ℕ0 ∣ (2↑𝑙) ∥ 𝑎} ↔ (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℕ0 ∧ (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∥ 𝑎))
88	84, 87	sylib 217	. . . . . . . 8 ⊢ (𝑎 ∈ ℕ → (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℕ0 ∧ (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∥ 𝑎))
89	88	simprd 496	. . . . . . 7 ⊢ (𝑎 ∈ ℕ → (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∥ 𝑎)
90		nndivdvds 15961	. . . . . . . 8 ⊢ ((𝑎 ∈ ℕ ∧ (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∈ ℕ) → ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∥ 𝑎 ↔ (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ ℕ))
91	90	biimpa 477	. . . . . . 7 ⊢ (((𝑎 ∈ ℕ ∧ (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∈ ℕ) ∧ (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∥ 𝑎) → (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ ℕ)
92	14, 54, 89, 91	syl21anc 835	. . . . . 6 ⊢ (𝑎 ∈ ℕ → (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ ℕ)
93		1nn0 12238	. . . . . . . . . . 11 ⊢ 1 ∈ ℕ0
94	93	a1i 11	. . . . . . . . . 10 ⊢ (𝑎 ∈ ℕ → 1 ∈ ℕ0)
95	53, 94	nn0addcld 12286	. . . . . . . . 9 ⊢ (𝑎 ∈ ℕ → (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈ ℕ0)
96	53	nn0red 12283	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ ℕ → sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℝ)
97	96	ltp1d 11894	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ ℕ → sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) < (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1))
98	20, 52	supub 9207	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ ℕ → ((sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} → ¬ sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) < (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)))
99	97, 98	mt2d 136	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ ℕ → ¬ (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎})
100	83	eleq2i 2830	. . . . . . . . . . . 12 ⊢ ((sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ↔ (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈ {𝑙 ∈ ℕ0 ∣ (2↑𝑙) ∥ 𝑎})
101	99, 100	sylnib 328	. . . . . . . . . . 11 ⊢ (𝑎 ∈ ℕ → ¬ (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈ {𝑙 ∈ ℕ0 ∣ (2↑𝑙) ∥ 𝑎})
102		oveq2 7277	. . . . . . . . . . . . 13 ⊢ (𝑙 = (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) → (2↑𝑙) = (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)))
103	102	breq1d 5085	. . . . . . . . . . . 12 ⊢ (𝑙 = (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) → ((2↑𝑙) ∥ 𝑎 ↔ (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) ∥ 𝑎))
104	103	elrab 3625	. . . . . . . . . . 11 ⊢ ((sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈ {𝑙 ∈ ℕ0 ∣ (2↑𝑙) ∥ 𝑎} ↔ ((sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈ ℕ0 ∧ (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) ∥ 𝑎))
105	101, 104	sylnib 328	. . . . . . . . . 10 ⊢ (𝑎 ∈ ℕ → ¬ ((sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈ ℕ0 ∧ (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) ∥ 𝑎))
106		imnan 400	. . . . . . . . . 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 233	. . . . . . . . 9 ⊢ (𝑎 ∈ ℕ → ((sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈ ℕ0 → ¬ (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) ∥ 𝑎))
108	95, 107	mpd 15	. . . . . . . 8 ⊢ (𝑎 ∈ ℕ → ¬ (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) ∥ 𝑎)
109		expp1 13778	. . . . . . . . . 10 ⊢ ((2 ∈ ℂ ∧ sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℕ0) → (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) = ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2))
110	68, 53, 109	sylancr 587	. . . . . . . . 9 ⊢ (𝑎 ∈ ℕ → (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) = ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2))
111	110	breq1d 5085	. . . . . . . 8 ⊢ (𝑎 ∈ ℕ → ((2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) ∥ 𝑎 ↔ ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2) ∥ 𝑎))
112	108, 111	mtbid 324	. . . . . . 7 ⊢ (𝑎 ∈ ℕ → ¬ ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2) ∥ 𝑎)
113		nncn 11970	. . . . . . . . . . 11 ⊢ (𝑎 ∈ ℕ → 𝑎 ∈ ℂ)
114	54	nncnd 11978	. . . . . . . . . . 11 ⊢ (𝑎 ∈ ℕ → (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∈ ℂ)
115	54	nnne0d 12012	. . . . . . . . . . 11 ⊢ (𝑎 ∈ ℕ → (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ≠ 0)
116	113, 114, 115	divcan2d 11742	. . . . . . . . . 10 ⊢ (𝑎 ∈ ℕ → ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))) = 𝑎)
117	116	eqcomd 2744	. . . . . . . . 9 ⊢ (𝑎 ∈ ℕ → 𝑎 = ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
118	117	breq2d 5087	. . . . . . . 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 12414	. . . . . . . . 9 ⊢ (𝑎 ∈ ℕ → 2 ∈ ℤ)
120	92	nnzd 12414	. . . . . . . . 9 ⊢ (𝑎 ∈ ℕ → (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ ℤ)
121	54	nnzd 12414	. . . . . . . . 9 ⊢ (𝑎 ∈ ℕ → (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∈ ℤ)
122		dvdscmulr 15983	. . . . . . . . 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 1373	. . . . . . . 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 278	. . . . . . 7 ⊢ (𝑎 ∈ ℕ → (((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2) ∥ 𝑎 ↔ 2 ∥ (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
125	112, 124	mtbid 324	. . . . . 6 ⊢ (𝑎 ∈ ℕ → ¬ 2 ∥ (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))))
126		breq2 5079	. . . . . . . 8 ⊢ (𝑧 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → (2 ∥ 𝑧 ↔ 2 ∥ (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
127	126	notbid 318	. . . . . . 7 ⊢ (𝑧 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → (¬ 2 ∥ 𝑧 ↔ ¬ 2 ∥ (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
128	127, 6	elrab2 3628	. . . . . 6 ⊢ ((𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ 𝐽 ↔ ((𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ ℕ ∧ ¬ 2 ∥ (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
129	92, 125, 128	sylanbrc 583	. . . . 5 ⊢ (𝑎 ∈ ℕ → (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ 𝐽)
130	129, 53	jca 512	. . . 4 ⊢ (𝑎 ∈ ℕ → ((𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ 𝐽 ∧ sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℕ0))
131	130	adantl 482	. . 3 ⊢ ((⊤ ∧ 𝑎 ∈ ℕ) → ((𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ 𝐽 ∧ sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℕ0))
132		simpr 485	. . . . . . 7 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑎 = ((2↑𝑦) · 𝑥))
133	2	a1i 11	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 2 ∈ ℕ)
134		simplr 766	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑦 ∈ ℕ0)
135	133, 134	nnexpcld 13949	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (2↑𝑦) ∈ ℕ)
136	8	sseli 3918	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐽 → 𝑥 ∈ ℕ)
137	136	ad2antrr 723	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑥 ∈ ℕ)
138	135, 137	nnmulcld 12015	. . . . . . 7 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → ((2↑𝑦) · 𝑥) ∈ ℕ)
139	132, 138	eqeltrd 2839	. . . . . 6 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑎 ∈ ℕ)
140		simplll 772	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑥 ∈ 𝐽)
141		breq2 5079	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑥 → (2 ∥ 𝑧 ↔ 2 ∥ 𝑥))
142	141	notbid 318	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑥 → (¬ 2 ∥ 𝑧 ↔ ¬ 2 ∥ 𝑥))
143	142, 6	elrab2 3628	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐽 ↔ (𝑥 ∈ ℕ ∧ ¬ 2 ∥ 𝑥))
144	143	simprbi 497	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐽 → ¬ 2 ∥ 𝑥)
145		2z 12341	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℤ
146	134	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑦 ∈ ℕ0)
147	146	nn0zd 12413	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑦 ∈ ℤ)
148	19	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → < Or ℕ0)
149	139, 52	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → ∃𝑚 ∈ ℕ0 (∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ¬ 𝑚 < 𝑛 ∧ ∀𝑛 ∈ ℕ0 (𝑛 < 𝑚 → ∃𝑜 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}𝑛 < 𝑜)))
150	149	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → ∃𝑚 ∈ ℕ0 (∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ¬ 𝑚 < 𝑛 ∧ ∀𝑛 ∈ ℕ0 (𝑛 < 𝑚 → ∃𝑜 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}𝑛 < 𝑜)))
151	148, 150	supcl 9206	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℕ0)
152	151	nn0zd 12413	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℤ)
153		simpr 485	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))
154		znnsub 12355	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ ℤ ∧ sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℤ) → (𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ↔ (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦) ∈ ℕ))
155	154	biimpa 477	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 ∈ ℤ ∧ sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℤ) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦) ∈ ℕ)
156	147, 152, 153, 155	syl21anc 835	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦) ∈ ℕ)
157		iddvdsexp 15978	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℤ ∧ (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦) ∈ ℕ) → 2 ∥ (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)))
158	145, 156, 157	sylancr 587	. . . . . . . . . . . . 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 17	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ ℤ)
161	160	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ ℤ)
162	156	nnnn0d 12282	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦) ∈ ℕ0)
163		zexpcl 13786	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℤ ∧ (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦) ∈ ℕ0) → (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) ∈ ℤ)
164	145, 162, 163	sylancr 587	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) ∈ ℤ)
165		dvdsmultr2 15996	. . . . . . . . . . . . . 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 1370	. . . . . . . . . . . . 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 15	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 2 ∥ ((𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) · (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦))))
168	137	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑥 ∈ ℕ)
169	168	nncnd 11978	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑥 ∈ ℂ)
170		2cnd 12040	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 2 ∈ ℂ)
171	170, 162	expcld 13853	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) ∈ ℂ)
172	139	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑎 ∈ ℕ)
173	172	nncnd 11978	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑎 ∈ ℂ)
174	172, 114	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∈ ℂ)
175		2ne0 12066	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ≠ 0
176	175	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 2 ≠ 0)
177	170, 176, 152	expne0d 13859	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ≠ 0)
178	173, 174, 177	divcld 11740	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ ℂ)
179	171, 178	mulcld 10984	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → ((2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))) ∈ ℂ)
180	170, 146	expcld 13853	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (2↑𝑦) ∈ ℂ)
181	170, 176, 147	expne0d 13859	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (2↑𝑦) ≠ 0)
182	172, 117	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑎 = ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
183		simplr 766	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑎 = ((2↑𝑦) · 𝑥))
184	146	nn0cnd 12284	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑦 ∈ ℂ)
185	151	nn0cnd 12284	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℂ)
186	184, 185	pncan3d 11324	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (𝑦 + (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))
187	186	oveq2d 7285	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (2↑(𝑦 + (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦))) = (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))
188	170, 162, 146	expaddd 13855	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (2↑(𝑦 + (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦))) = ((2↑𝑦) · (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦))))
189	187, 188	eqtr3d 2780	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) = ((2↑𝑦) · (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦))))
190	189	oveq1d 7284	. . . . . . . . . . . . . . . 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 2786	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → ((2↑𝑦) · 𝑥) = (((2↑𝑦) · (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦))) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
192	180, 171, 178	mulassd 10987	. . . . . . . . . . . . . . 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 2778	. . . . . . . . . . . . . 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 11599	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑥 = ((2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
195	178, 171	mulcomd 10985	. . . . . . . . . . . . 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 2781	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑥 = ((𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) · (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦))))
197	167, 196	breqtrrd 5103	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 2 ∥ 𝑥)
198	144, 197	nsyl3 138	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → ¬ 𝑥 ∈ 𝐽)
199	140, 198	pm2.65da 814	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → ¬ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))
200	137	nnzd 12414	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑥 ∈ ℤ)
201	135	nnzd 12414	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (2↑𝑦) ∈ ℤ)
202	139	nnzd 12414	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑎 ∈ ℤ)
203	135	nncnd 11978	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (2↑𝑦) ∈ ℂ)
204	137	nncnd 11978	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑥 ∈ ℂ)
205	203, 204	mulcomd 10985	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → ((2↑𝑦) · 𝑥) = (𝑥 · (2↑𝑦)))
206	132, 205	eqtr2d 2779	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑥 · (2↑𝑦)) = 𝑎)
207		dvds0lem 15965	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℤ ∧ (2↑𝑦) ∈ ℤ ∧ 𝑎 ∈ ℤ) ∧ (𝑥 · (2↑𝑦)) = 𝑎) → (2↑𝑦) ∥ 𝑎)
208	200, 201, 202, 206, 207	syl31anc 1372	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (2↑𝑦) ∥ 𝑎)
209		oveq2 7277	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑦 → (2↑𝑘) = (2↑𝑦))
210	209	breq1d 5085	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑦 → ((2↑𝑘) ∥ 𝑎 ↔ (2↑𝑦) ∥ 𝑎))
211	210	elrab 3625	. . . . . . . . . . 11 ⊢ (𝑦 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ↔ (𝑦 ∈ ℕ0 ∧ (2↑𝑦) ∥ 𝑎))
212	134, 208, 211	sylanbrc 583	. . . . . . . . . 10 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑦 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎})
213	19	a1i 11	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → < Or ℕ0)
214	213, 149	supub 9207	. . . . . . . . . 10 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑦 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} → ¬ sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) < 𝑦))
215	212, 214	mpd 15	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → ¬ sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) < 𝑦)
216	134	nn0red 12283	. . . . . . . . . 10 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑦 ∈ ℝ)
217	139, 96	syl 17	. . . . . . . . . 10 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℝ)
218	216, 217	lttri3d 11104	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ↔ (¬ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∧ ¬ sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) < 𝑦)))
219	199, 215, 218	mpbir2and 710	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))
220		simplr 766	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑎 = ((2↑𝑦) · 𝑥))
221	139	adantr 481	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑎 ∈ ℕ)
222	221	nncnd 11978	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑎 ∈ ℂ)
223	137	adantr 481	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑥 ∈ ℕ)
224	223	nncnd 11978	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑥 ∈ ℂ)
225		nnexpcl 13784	. . . . . . . . . . . . . . . 16 ⊢ ((2 ∈ ℕ ∧ 𝑦 ∈ ℕ0) → (2↑𝑦) ∈ ℕ)
226	2, 225	mpan 687	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ0 → (2↑𝑦) ∈ ℕ)
227	226	nncnd 11978	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ0 → (2↑𝑦) ∈ ℂ)
228	226	nnne0d 12012	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ0 → (2↑𝑦) ≠ 0)
229	227, 228	jca 512	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ0 → ((2↑𝑦) ∈ ℂ ∧ (2↑𝑦) ≠ 0))
230	229	ad3antlr 728	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → ((2↑𝑦) ∈ ℂ ∧ (2↑𝑦) ≠ 0))
231		divmul2 11626	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ ((2↑𝑦) ∈ ℂ ∧ (2↑𝑦) ≠ 0)) → ((𝑎 / (2↑𝑦)) = 𝑥 ↔ 𝑎 = ((2↑𝑦) · 𝑥)))
232	222, 224, 230, 231	syl3anc 1370	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → ((𝑎 / (2↑𝑦)) = 𝑥 ↔ 𝑎 = ((2↑𝑦) · 𝑥)))
233	220, 232	mpbird 256	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (𝑎 / (2↑𝑦)) = 𝑥)
234		simpr 485	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))
235	234	oveq2d 7285	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (2↑𝑦) = (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))
236	235	oveq2d 7285	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (𝑎 / (2↑𝑦)) = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))))
237	233, 236	eqtr3d 2780	. . . . . . . . 9 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))))
238	237	ex 413	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) → 𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
239	219, 238	jcai 517	. . . . . . 7 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∧ 𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
240	239	ancomd 462	. . . . . 6 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))
241	139, 240	jca 512	. . . . 5 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))))
242		simprl 768	. . . . . . 7 ⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → 𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))))
243	129	adantr 481	. . . . . . 7 ⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ 𝐽)
244	242, 243	eqeltrd 2839	. . . . . 6 ⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → 𝑥 ∈ 𝐽)
245		simprr 770	. . . . . . 7 ⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))
246	53	adantr 481	. . . . . . 7 ⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℕ0)
247	245, 246	eqeltrd 2839	. . . . . 6 ⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → 𝑦 ∈ ℕ0)
248	117	adantr 481	. . . . . . 7 ⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → 𝑎 = ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
249	245	oveq2d 7285	. . . . . . . 8 ⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → (2↑𝑦) = (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))
250	249, 242	oveq12d 7287	. . . . . . 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 2781	. . . . . 6 ⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → 𝑎 = ((2↑𝑦) · 𝑥))
252	244, 247, 251	jca31 515	. . . . 5 ⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → ((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)))
253	241, 252	impbii 208	. . . 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 31043	. 2 ⊢ (⊤ → 𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ)
256	255	mptru 1546	1 ⊢ 𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539  ⊤wtru 1540   ∈ wcel 2106   ≠ wne 2943  ∀wral 3064  ∃wrex 3065  {crab 3068   ⊆ wss 3888  ∅c0 4258   class class class wbr 5075   Or wor 5499   × cxp 5584  –1-1-onto→wf1o 6427  (class class class)co 7269   ∈ cmpo 7271  Fincfn 8722  supcsup 9188  ℂcc 10858  ℝcr 10859  0cc0 10860  1c1 10861   + caddc 10863   · cmul 10865   < clt 10998   ≤ cle 10999   − cmin 11194   / cdiv 11621  ℕcn 11962  2c2 12017  ℕ₀cn0 12222  ℤcz 12308  ...cfz 13228  ↑cexp 13771   ∥ cdvds 15952

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7580  ax-cnex 10916  ax-resscn 10917  ax-1cn 10918  ax-icn 10919  ax-addcl 10920  ax-addrcl 10921  ax-mulcl 10922  ax-mulrcl 10923  ax-mulcom 10924  ax-addass 10925  ax-mulass 10926  ax-distr 10927  ax-i2m1 10928  ax-1ne0 10929  ax-1rid 10930  ax-rnegex 10931  ax-rrecex 10932  ax-cnre 10933  ax-pre-lttri 10934  ax-pre-lttrn 10935  ax-pre-ltadd 10936  ax-pre-mulgt0 10937

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-rmo 3071  df-reu 3072  df-rab 3073  df-v 3433  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-pss 3907  df-nul 4259  df-if 4462  df-pw 4537  df-sn 4564  df-pr 4566  df-op 4570  df-uni 4842  df-iun 4928  df-br 5076  df-opab 5138  df-mpt 5159  df-tr 5193  df-id 5486  df-eprel 5492  df-po 5500  df-so 5501  df-fr 5541  df-we 5543  df-xp 5592  df-rel 5593  df-cnv 5594  df-co 5595  df-dm 5596  df-rn 5597  df-res 5598  df-ima 5599  df-pred 6197  df-ord 6264  df-on 6265  df-lim 6266  df-suc 6267  df-iota 6386  df-fun 6430  df-fn 6431  df-f 6432  df-f1 6433  df-fo 6434  df-f1o 6435  df-fv 6436  df-riota 7226  df-ov 7272  df-oprab 7273  df-mpo 7274  df-om 7705  df-1st 7822  df-2nd 7823  df-frecs 8086  df-wrecs 8117  df-recs 8191  df-rdg 8230  df-1o 8286  df-er 8487  df-en 8723  df-dom 8724  df-sdom 8725  df-fin 8726  df-sup 9190  df-inf 9191  df-pnf 11000  df-mnf 11001  df-xr 11002  df-ltxr 11003  df-le 11004  df-sub 11196  df-neg 11197  df-div 11622  df-nn 11963  df-2 12025  df-n0 12223  df-z 12309  df-uz 12572  df-fz 13229  df-seq 13711  df-exp 13772  df-dvds 15953

This theorem is referenced by:  eulerpartgbij  32326  eulerpartlemgvv  32330  eulerpartlemgh  32332  eulerpartlemgf  32333