Theorem oddpwdc 29743

Description: Lemma for eulerpart 29771. 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 11062	. . . . . . . 8 ⊢ 2 ∈ ℕ
3	2	a1i 11	. . . . . . 7 ⊢ ((𝑦 ∈ ℕ0 ∧ 𝑥 ∈ 𝐽) → 2 ∈ ℕ)
4		simpl 472	. . . . . . 7 ⊢ ((𝑦 ∈ ℕ0 ∧ 𝑥 ∈ 𝐽) → 𝑦 ∈ ℕ0)
5	3, 4	nnexpcld 12892	. . . . . 6 ⊢ ((𝑦 ∈ ℕ0 ∧ 𝑥 ∈ 𝐽) → (2↑𝑦) ∈ ℕ)
6		oddpwdc.j	. . . . . . . 8 ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}
7		ssrab2 3650	. . . . . . . 8 ⊢ {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} ⊆ ℕ
8	6, 7	eqsstri 3598	. . . . . . 7 ⊢ 𝐽 ⊆ ℕ
9		simpr 476	. . . . . . 7 ⊢ ((𝑦 ∈ ℕ0 ∧ 𝑥 ∈ 𝐽) → 𝑥 ∈ 𝐽)
10	8, 9	sseldi 3566	. . . . . 6 ⊢ ((𝑦 ∈ ℕ0 ∧ 𝑥 ∈ 𝐽) → 𝑥 ∈ ℕ)
11	5, 10	nnmulcld 10945	. . . . 5 ⊢ ((𝑦 ∈ ℕ0 ∧ 𝑥 ∈ 𝐽) → ((2↑𝑦) · 𝑥) ∈ ℕ)
12	11	ancoms 468	. . . 4 ⊢ ((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) → ((2↑𝑦) · 𝑥) ∈ ℕ)
13	12	adantl 481	. . 3 ⊢ ((⊤ ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0)) → ((2↑𝑦) · 𝑥) ∈ ℕ)
14		id 22	. . . . . . 7 ⊢ (𝑎 ∈ ℕ → 𝑎 ∈ ℕ)
15	2	a1i 11	. . . . . . . 8 ⊢ (𝑎 ∈ ℕ → 2 ∈ ℕ)
16		nn0ssre 11173	. . . . . . . . . . 11 ⊢ ℕ0 ⊆ ℝ
17		ltso 9997	. . . . . . . . . . 11 ⊢ < Or ℝ
18		soss 4977	. . . . . . . . . . 11 ⊢ (ℕ0 ⊆ ℝ → ( < Or ℝ → < Or ℕ0))
19	16, 17, 18	mp2 9	. . . . . . . . . 10 ⊢ < Or ℕ0
20	19	a1i 11	. . . . . . . . 9 ⊢ (𝑎 ∈ ℕ → < Or ℕ0)
21		0zd 11266	. . . . . . . . . 10 ⊢ (𝑎 ∈ ℕ → 0 ∈ ℤ)
22		ssrab2 3650	. . . . . . . . . . 11 ⊢ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ⊆ ℕ0
23	22	a1i 11	. . . . . . . . . 10 ⊢ (𝑎 ∈ ℕ → {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ⊆ ℕ0)
24		nnz 11276	. . . . . . . . . . 11 ⊢ (𝑎 ∈ ℕ → 𝑎 ∈ ℤ)
25		oveq2 6557	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑛 → (2↑𝑘) = (2↑𝑛))
26	25	breq1d 4593	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑛 → ((2↑𝑘) ∥ 𝑎 ↔ (2↑𝑛) ∥ 𝑎))
27	26	elrab 3331	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ↔ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎))
28		simprl 790	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → 𝑛 ∈ ℕ0)
29	28	nn0red 11229	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → 𝑛 ∈ ℝ)
30	2	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → 2 ∈ ℕ)
31	30, 28	nnexpcld 12892	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → (2↑𝑛) ∈ ℕ)
32	31	nnred 10912	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → (2↑𝑛) ∈ ℝ)
33		simpl 472	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → 𝑎 ∈ ℕ)
34	33	nnred 10912	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → 𝑎 ∈ ℝ)
35		2re 10967	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℝ
36	35	leidi 10441	. . . . . . . . . . . . . . . 16 ⊢ 2 ≤ 2
37		nexple 29399	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ ℕ0 ∧ 2 ∈ ℝ ∧ 2 ≤ 2) → 𝑛 ≤ (2↑𝑛))
38	35, 36, 37	mp3an23 1408	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ0 → 𝑛 ≤ (2↑𝑛))
39	38	ad2antrl 760	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → 𝑛 ≤ (2↑𝑛))
40	31	nnzd 11357	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → (2↑𝑛) ∈ ℤ)
41		simprr 792	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → (2↑𝑛) ∥ 𝑎)
42		dvdsle 14870	. . . . . . . . . . . . . . . 16 ⊢ (((2↑𝑛) ∈ ℤ ∧ 𝑎 ∈ ℕ) → ((2↑𝑛) ∥ 𝑎 → (2↑𝑛) ≤ 𝑎))
43	42	imp 444	. . . . . . . . . . . . . . 15 ⊢ ((((2↑𝑛) ∈ ℤ ∧ 𝑎 ∈ ℕ) ∧ (2↑𝑛) ∥ 𝑎) → (2↑𝑛) ≤ 𝑎)
44	40, 33, 41, 43	syl21anc 1317	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → (2↑𝑛) ≤ 𝑎)
45	29, 32, 34, 39, 44	letrd 10073	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ ℕ ∧ (𝑛 ∈ ℕ0 ∧ (2↑𝑛) ∥ 𝑎)) → 𝑛 ≤ 𝑎)
46	27, 45	sylan2b 491	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}) → 𝑛 ≤ 𝑎)
47	46	ralrimiva 2949	. . . . . . . . . . 11 ⊢ (𝑎 ∈ ℕ → ∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}𝑛 ≤ 𝑎)
48		breq2 4587	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑎 → (𝑛 ≤ 𝑚 ↔ 𝑛 ≤ 𝑎))
49	48	ralbidv 2969	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑎 → (∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}𝑛 ≤ 𝑚 ↔ ∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}𝑛 ≤ 𝑎))
50	49	rspcev 3282	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ ℤ ∧ ∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}𝑛 ≤ 𝑎) → ∃𝑚 ∈ ℤ ∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}𝑛 ≤ 𝑚)
51	24, 47, 50	syl2anc 691	. . . . . . . . . 10 ⊢ (𝑎 ∈ ℕ → ∃𝑚 ∈ ℤ ∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}𝑛 ≤ 𝑚)
52		nn0uz 11598	. . . . . . . . . . 11 ⊢ ℕ0 = (ℤ≥‘0)
53	52	uzsupss 11656	. . . . . . . . . 10 ⊢ ((0 ∈ ℤ ∧ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ⊆ ℕ0 ∧ ∃𝑚 ∈ ℤ ∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}𝑛 ≤ 𝑚) → ∃𝑚 ∈ ℕ0 (∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ¬ 𝑚 < 𝑛 ∧ ∀𝑛 ∈ ℕ0 (𝑛 < 𝑚 → ∃𝑜 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}𝑛 < 𝑜)))
54	21, 23, 51, 53	syl3anc 1318	. . . . . . . . 9 ⊢ (𝑎 ∈ ℕ → ∃𝑚 ∈ ℕ0 (∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ¬ 𝑚 < 𝑛 ∧ ∀𝑛 ∈ ℕ0 (𝑛 < 𝑚 → ∃𝑜 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}𝑛 < 𝑜)))
55	20, 54	supcl 8247	. . . . . . . 8 ⊢ (𝑎 ∈ ℕ → sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℕ0)
56	15, 55	nnexpcld 12892	. . . . . . 7 ⊢ (𝑎 ∈ ℕ → (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∈ ℕ)
57		fzfi 12633	. . . . . . . . . . . 12 ⊢ (0...𝑎) ∈ Fin
58		0zd 11266	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}) → 0 ∈ ℤ)
59	24	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}) → 𝑎 ∈ ℤ)
60	27, 28	sylan2b 491	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}) → 𝑛 ∈ ℕ0)
61	60	nn0zd 11356	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}) → 𝑛 ∈ ℤ)
62	60	nn0ge0d 11231	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}) → 0 ≤ 𝑛)
63		elfz4 12206	. . . . . . . . . . . . . . 15 ⊢ (((0 ∈ ℤ ∧ 𝑎 ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ (0 ≤ 𝑛 ∧ 𝑛 ≤ 𝑎)) → 𝑛 ∈ (0...𝑎))
64	58, 59, 61, 62, 46, 63	syl32anc 1326	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ ℕ ∧ 𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}) → 𝑛 ∈ (0...𝑎))
65	64	ex 449	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ ℕ → (𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} → 𝑛 ∈ (0...𝑎)))
66	65	ssrdv 3574	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ ℕ → {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ⊆ (0...𝑎))
67		ssfi 8065	. . . . . . . . . . . 12 ⊢ (((0...𝑎) ∈ Fin ∧ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ⊆ (0...𝑎)) → {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ∈ Fin)
68	57, 66, 67	sylancr 694	. . . . . . . . . . 11 ⊢ (𝑎 ∈ ℕ → {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ∈ Fin)
69		0nn0 11184	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℕ0
70	69	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ ℕ → 0 ∈ ℕ0)
71		2cn 10968	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℂ
72		exp0 12726	. . . . . . . . . . . . . . 15 ⊢ (2 ∈ ℂ → (2↑0) = 1)
73	71, 72	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ (2↑0) = 1
74		1dvds 14834	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ ℤ → 1 ∥ 𝑎)
75	24, 74	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ ℕ → 1 ∥ 𝑎)
76	73, 75	syl5eqbr 4618	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ ℕ → (2↑0) ∥ 𝑎)
77		oveq2 6557	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 0 → (2↑𝑘) = (2↑0))
78	77	breq1d 4593	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 0 → ((2↑𝑘) ∥ 𝑎 ↔ (2↑0) ∥ 𝑎))
79	78	elrab 3331	. . . . . . . . . . . . 13 ⊢ (0 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ↔ (0 ∈ ℕ0 ∧ (2↑0) ∥ 𝑎))
80	70, 76, 79	sylanbrc 695	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ ℕ → 0 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎})
81		ne0i 3880	. . . . . . . . . . . 12 ⊢ (0 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} → {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ≠ ∅)
82	80, 81	syl 17	. . . . . . . . . . 11 ⊢ (𝑎 ∈ ℕ → {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ≠ ∅)
83		fisupcl 8258	. . . . . . . . . . 11 ⊢ (( < Or ℕ0 ∧ ({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ∈ Fin ∧ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ≠ ∅ ∧ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ⊆ ℕ0)) → sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎})
84	20, 68, 82, 23, 83	syl13anc 1320	. . . . . . . . . 10 ⊢ (𝑎 ∈ ℕ → sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎})
85		oveq2 6557	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑙 → (2↑𝑘) = (2↑𝑙))
86	85	breq1d 4593	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑙 → ((2↑𝑘) ∥ 𝑎 ↔ (2↑𝑙) ∥ 𝑎))
87	86	cbvrabv 3172	. . . . . . . . . 10 ⊢ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} = {𝑙 ∈ ℕ0 ∣ (2↑𝑙) ∥ 𝑎}
88	84, 87	syl6eleq 2698	. . . . . . . . 9 ⊢ (𝑎 ∈ ℕ → sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ {𝑙 ∈ ℕ0 ∣ (2↑𝑙) ∥ 𝑎})
89		oveq2 6557	. . . . . . . . . . 11 ⊢ (𝑙 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) → (2↑𝑙) = (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))
90	89	breq1d 4593	. . . . . . . . . 10 ⊢ (𝑙 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) → ((2↑𝑙) ∥ 𝑎 ↔ (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∥ 𝑎))
91	90	elrab 3331	. . . . . . . . 9 ⊢ (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ {𝑙 ∈ ℕ0 ∣ (2↑𝑙) ∥ 𝑎} ↔ (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℕ0 ∧ (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∥ 𝑎))
92	88, 91	sylib 207	. . . . . . . 8 ⊢ (𝑎 ∈ ℕ → (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℕ0 ∧ (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∥ 𝑎))
93	92	simprd 478	. . . . . . 7 ⊢ (𝑎 ∈ ℕ → (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∥ 𝑎)
94		nndivdvds 14827	. . . . . . . 8 ⊢ ((𝑎 ∈ ℕ ∧ (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∈ ℕ) → ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∥ 𝑎 ↔ (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ ℕ))
95	94	biimpa 500	. . . . . . 7 ⊢ (((𝑎 ∈ ℕ ∧ (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∈ ℕ) ∧ (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∥ 𝑎) → (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ ℕ)
96	14, 56, 93, 95	syl21anc 1317	. . . . . 6 ⊢ (𝑎 ∈ ℕ → (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ ℕ)
97		1nn0 11185	. . . . . . . . . . 11 ⊢ 1 ∈ ℕ0
98	97	a1i 11	. . . . . . . . . 10 ⊢ (𝑎 ∈ ℕ → 1 ∈ ℕ0)
99	55, 98	nn0addcld 11232	. . . . . . . . 9 ⊢ (𝑎 ∈ ℕ → (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈ ℕ0)
100	55	nn0red 11229	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ ℕ → sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℝ)
101	100	ltp1d 10833	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ ℕ → sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) < (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1))
102	20, 54	supub 8248	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ ℕ → ((sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} → ¬ sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) < (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)))
103	101, 102	mt2d 130	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ ℕ → ¬ (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎})
104	87	eleq2i 2680	. . . . . . . . . . . 12 ⊢ ((sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ↔ (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈ {𝑙 ∈ ℕ0 ∣ (2↑𝑙) ∥ 𝑎})
105	103, 104	sylnib 317	. . . . . . . . . . 11 ⊢ (𝑎 ∈ ℕ → ¬ (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈ {𝑙 ∈ ℕ0 ∣ (2↑𝑙) ∥ 𝑎})
106		oveq2 6557	. . . . . . . . . . . . 13 ⊢ (𝑙 = (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) → (2↑𝑙) = (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)))
107	106	breq1d 4593	. . . . . . . . . . . 12 ⊢ (𝑙 = (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) → ((2↑𝑙) ∥ 𝑎 ↔ (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) ∥ 𝑎))
108	107	elrab 3331	. . . . . . . . . . 11 ⊢ ((sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈ {𝑙 ∈ ℕ0 ∣ (2↑𝑙) ∥ 𝑎} ↔ ((sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈ ℕ0 ∧ (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) ∥ 𝑎))
109	105, 108	sylnib 317	. . . . . . . . . 10 ⊢ (𝑎 ∈ ℕ → ¬ ((sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈ ℕ0 ∧ (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) ∥ 𝑎))
110		imnan 437	. . . . . . . . . 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)) ∥ 𝑎))
111	109, 110	sylibr 223	. . . . . . . . 9 ⊢ (𝑎 ∈ ℕ → ((sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1) ∈ ℕ0 → ¬ (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) ∥ 𝑎))
112	99, 111	mpd 15	. . . . . . . 8 ⊢ (𝑎 ∈ ℕ → ¬ (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) ∥ 𝑎)
113		expp1 12729	. . . . . . . . . 10 ⊢ ((2 ∈ ℂ ∧ sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℕ0) → (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) = ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2))
114	71, 55, 113	sylancr 694	. . . . . . . . 9 ⊢ (𝑎 ∈ ℕ → (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) = ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2))
115	114	breq1d 4593	. . . . . . . 8 ⊢ (𝑎 ∈ ℕ → ((2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) + 1)) ∥ 𝑎 ↔ ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2) ∥ 𝑎))
116	112, 115	mtbid 313	. . . . . . 7 ⊢ (𝑎 ∈ ℕ → ¬ ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2) ∥ 𝑎)
117		nncn 10905	. . . . . . . . . . 11 ⊢ (𝑎 ∈ ℕ → 𝑎 ∈ ℂ)
118	56	nncnd 10913	. . . . . . . . . . 11 ⊢ (𝑎 ∈ ℕ → (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∈ ℂ)
119	56	nnne0d 10942	. . . . . . . . . . 11 ⊢ (𝑎 ∈ ℕ → (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ≠ 0)
120	117, 118, 119	divcan2d 10682	. . . . . . . . . 10 ⊢ (𝑎 ∈ ℕ → ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))) = 𝑎)
121	120	eqcomd 2616	. . . . . . . . 9 ⊢ (𝑎 ∈ ℕ → 𝑎 = ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
122	121	breq2d 4595	. . . . . . . 8 ⊢ (𝑎 ∈ ℕ → (((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2) ∥ 𝑎 ↔ ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2) ∥ ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))))))
123	15	nnzd 11357	. . . . . . . . 9 ⊢ (𝑎 ∈ ℕ → 2 ∈ ℤ)
124	96	nnzd 11357	. . . . . . . . 9 ⊢ (𝑎 ∈ ℕ → (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ ℤ)
125	56	nnzd 11357	. . . . . . . . 9 ⊢ (𝑎 ∈ ℕ → (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∈ ℤ)
126		dvdscmulr 14848	. . . . . . . . 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, < )))))
127	123, 124, 125, 119, 126	syl112anc 1322	. . . . . . . 8 ⊢ (𝑎 ∈ ℕ → (((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2) ∥ ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))) ↔ 2 ∥ (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
128	122, 127	bitrd 267	. . . . . . 7 ⊢ (𝑎 ∈ ℕ → (((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · 2) ∥ 𝑎 ↔ 2 ∥ (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
129	116, 128	mtbid 313	. . . . . 6 ⊢ (𝑎 ∈ ℕ → ¬ 2 ∥ (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))))
130		breq2 4587	. . . . . . . 8 ⊢ (𝑧 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → (2 ∥ 𝑧 ↔ 2 ∥ (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
131	130	notbid 307	. . . . . . 7 ⊢ (𝑧 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → (¬ 2 ∥ 𝑧 ↔ ¬ 2 ∥ (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
132	131, 6	elrab2 3333	. . . . . 6 ⊢ ((𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ 𝐽 ↔ ((𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ ℕ ∧ ¬ 2 ∥ (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
133	96, 129, 132	sylanbrc 695	. . . . 5 ⊢ (𝑎 ∈ ℕ → (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ 𝐽)
134	133, 55	jca 553	. . . 4 ⊢ (𝑎 ∈ ℕ → ((𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ 𝐽 ∧ sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℕ0))
135	134	adantl 481	. . 3 ⊢ ((⊤ ∧ 𝑎 ∈ ℕ) → ((𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ 𝐽 ∧ sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℕ0))
136		simpr 476	. . . . . . 7 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑎 = ((2↑𝑦) · 𝑥))
137	2	a1i 11	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 2 ∈ ℕ)
138		simplr 788	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑦 ∈ ℕ0)
139	137, 138	nnexpcld 12892	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (2↑𝑦) ∈ ℕ)
140	8	sseli 3564	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐽 → 𝑥 ∈ ℕ)
141	140	ad2antrr 758	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑥 ∈ ℕ)
142	139, 141	nnmulcld 10945	. . . . . . 7 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → ((2↑𝑦) · 𝑥) ∈ ℕ)
143	136, 142	eqeltrd 2688	. . . . . 6 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑎 ∈ ℕ)
144		simplll 794	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑥 ∈ 𝐽)
145		breq2 4587	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑥 → (2 ∥ 𝑧 ↔ 2 ∥ 𝑥))
146	145	notbid 307	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑥 → (¬ 2 ∥ 𝑧 ↔ ¬ 2 ∥ 𝑥))
147	146, 6	elrab2 3333	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐽 ↔ (𝑥 ∈ ℕ ∧ ¬ 2 ∥ 𝑥))
148	147	simprbi 479	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐽 → ¬ 2 ∥ 𝑥)
149		2z 11286	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℤ
150	138	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑦 ∈ ℕ0)
151	150	nn0zd 11356	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑦 ∈ ℤ)
152	19	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → < Or ℕ0)
153	143, 54	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → ∃𝑚 ∈ ℕ0 (∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ¬ 𝑚 < 𝑛 ∧ ∀𝑛 ∈ ℕ0 (𝑛 < 𝑚 → ∃𝑜 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}𝑛 < 𝑜)))
154	153	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → ∃𝑚 ∈ ℕ0 (∀𝑛 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ¬ 𝑚 < 𝑛 ∧ ∀𝑛 ∈ ℕ0 (𝑛 < 𝑚 → ∃𝑜 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}𝑛 < 𝑜)))
155	152, 154	supcl 8247	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℕ0)
156	155	nn0zd 11356	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℤ)
157		simpr 476	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))
158		znnsub 11300	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ ℤ ∧ sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℤ) → (𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ↔ (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦) ∈ ℕ))
159	158	biimpa 500	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 ∈ ℤ ∧ sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℤ) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦) ∈ ℕ)
160	151, 156, 157, 159	syl21anc 1317	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦) ∈ ℕ)
161		iddvdsexp 14843	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℤ ∧ (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦) ∈ ℕ) → 2 ∥ (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)))
162	149, 160, 161	sylancr 694	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 2 ∥ (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)))
163	149	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 2 ∈ ℤ)
164	143, 124	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ ℤ)
165	164	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ ℤ)
166	160	nnnn0d 11228	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦) ∈ ℕ0)
167		zexpcl 12737	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℤ ∧ (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦) ∈ ℕ0) → (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) ∈ ℤ)
168	149, 166, 167	sylancr 694	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) ∈ ℤ)
169		dvdsmultr2 14859	. . . . . . . . . . . . . 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, < ) − 𝑦)))))
170	163, 165, 168, 169	syl3anc 1318	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (2 ∥ (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) → 2 ∥ ((𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) · (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)))))
171	162, 170	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 2 ∥ ((𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) · (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦))))
172	141	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑥 ∈ ℕ)
173	172	nncnd 10913	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑥 ∈ ℂ)
174		2cnd 10970	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 2 ∈ ℂ)
175	174, 166	expcld 12870	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) ∈ ℂ)
176	143	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑎 ∈ ℕ)
177	176	nncnd 10913	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑎 ∈ ℂ)
178	176, 118	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ∈ ℂ)
179		2ne0 10990	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ≠ 0
180	179	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 2 ≠ 0)
181	174, 180, 156	expne0d 12876	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) ≠ 0)
182	177, 178, 181	divcld 10680	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ ℂ)
183	175, 182	mulcld 9939	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → ((2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))) ∈ ℂ)
184	174, 150	expcld 12870	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (2↑𝑦) ∈ ℂ)
185	174, 180, 151	expne0d 12876	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (2↑𝑦) ≠ 0)
186	176, 121	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑎 = ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
187		simplr 788	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑎 = ((2↑𝑦) · 𝑥))
188	150	nn0cnd 11230	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑦 ∈ ℂ)
189	155	nn0cnd 11230	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℂ)
190	188, 189	pncan3d 10274	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (𝑦 + (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))
191	190	oveq2d 6565	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (2↑(𝑦 + (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦))) = (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))
192	174, 166, 150	expaddd 12872	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (2↑(𝑦 + (sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦))) = ((2↑𝑦) · (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦))))
193	191, 192	eqtr3d 2646	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) = ((2↑𝑦) · (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦))))
194	193	oveq1d 6564	. . . . . . . . . . . . . . . 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, < )))))
195	186, 187, 194	3eqtr3d 2652	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → ((2↑𝑦) · 𝑥) = (((2↑𝑦) · (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦))) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
196	184, 175, 182	mulassd 9942	. . . . . . . . . . . . . . 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, < ))))))
197	195, 196	eqtrd 2644	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → ((2↑𝑦) · 𝑥) = ((2↑𝑦) · ((2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))))))
198	173, 183, 184, 185, 197	mulcanad 10541	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑥 = ((2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦)) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
199	182, 175	mulcomd 9940	. . . . . . . . . . . . 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, < )))))
200	198, 199	eqtr4d 2647	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑥 = ((𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) · (2↑(sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) − 𝑦))))
201	171, 200	breqtrrd 4611	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 2 ∥ 𝑥)
202	148, 201	nsyl3 132	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → ¬ 𝑥 ∈ 𝐽)
203	144, 202	pm2.65da 598	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → ¬ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))
204	141	nnzd 11357	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑥 ∈ ℤ)
205	139	nnzd 11357	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (2↑𝑦) ∈ ℤ)
206	143	nnzd 11357	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑎 ∈ ℤ)
207	139	nncnd 10913	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (2↑𝑦) ∈ ℂ)
208	141	nncnd 10913	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑥 ∈ ℂ)
209	207, 208	mulcomd 9940	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → ((2↑𝑦) · 𝑥) = (𝑥 · (2↑𝑦)))
210	136, 209	eqtr2d 2645	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑥 · (2↑𝑦)) = 𝑎)
211		dvds0lem 14830	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℤ ∧ (2↑𝑦) ∈ ℤ ∧ 𝑎 ∈ ℤ) ∧ (𝑥 · (2↑𝑦)) = 𝑎) → (2↑𝑦) ∥ 𝑎)
212	204, 205, 206, 210, 211	syl31anc 1321	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (2↑𝑦) ∥ 𝑎)
213		oveq2 6557	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑦 → (2↑𝑘) = (2↑𝑦))
214	213	breq1d 4593	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑦 → ((2↑𝑘) ∥ 𝑎 ↔ (2↑𝑦) ∥ 𝑎))
215	214	elrab 3331	. . . . . . . . . . 11 ⊢ (𝑦 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} ↔ (𝑦 ∈ ℕ0 ∧ (2↑𝑦) ∥ 𝑎))
216	138, 212, 215	sylanbrc 695	. . . . . . . . . 10 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑦 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎})
217	19	a1i 11	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → < Or ℕ0)
218	217, 153	supub 8248	. . . . . . . . . 10 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑦 ∈ {𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎} → ¬ sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) < 𝑦))
219	216, 218	mpd 15	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → ¬ sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) < 𝑦)
220	138	nn0red 11229	. . . . . . . . . 10 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑦 ∈ ℝ)
221	143, 100	syl 17	. . . . . . . . . 10 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℝ)
222	220, 221	lttri3d 10056	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ↔ (¬ 𝑦 < sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∧ ¬ sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) < 𝑦)))
223	203, 219, 222	mpbir2and 959	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))
224		simplr 788	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑎 = ((2↑𝑦) · 𝑥))
225	143	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑎 ∈ ℕ)
226	225	nncnd 10913	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑎 ∈ ℂ)
227	141	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑥 ∈ ℕ)
228	227	nncnd 10913	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑥 ∈ ℂ)
229		nnexpcl 12735	. . . . . . . . . . . . . . . 16 ⊢ ((2 ∈ ℕ ∧ 𝑦 ∈ ℕ0) → (2↑𝑦) ∈ ℕ)
230	2, 229	mpan 702	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ0 → (2↑𝑦) ∈ ℕ)
231	230	nncnd 10913	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ0 → (2↑𝑦) ∈ ℂ)
232	230	nnne0d 10942	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ0 → (2↑𝑦) ≠ 0)
233	231, 232	jca 553	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ0 → ((2↑𝑦) ∈ ℂ ∧ (2↑𝑦) ≠ 0))
234	233	ad3antlr 763	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → ((2↑𝑦) ∈ ℂ ∧ (2↑𝑦) ≠ 0))
235		divmul2 10568	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ ((2↑𝑦) ∈ ℂ ∧ (2↑𝑦) ≠ 0)) → ((𝑎 / (2↑𝑦)) = 𝑥 ↔ 𝑎 = ((2↑𝑦) · 𝑥)))
236	226, 228, 234, 235	syl3anc 1318	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → ((𝑎 / (2↑𝑦)) = 𝑥 ↔ 𝑎 = ((2↑𝑦) · 𝑥)))
237	224, 236	mpbird 246	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (𝑎 / (2↑𝑦)) = 𝑥)
238		simpr 476	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))
239	238	oveq2d 6565	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (2↑𝑦) = (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))
240	239	oveq2d 6565	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → (𝑎 / (2↑𝑦)) = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))))
241	237, 240	eqtr3d 2646	. . . . . . . . 9 ⊢ ((((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) → 𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))))
242	241	ex 449	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) → 𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
243	223, 242	jcai 557	. . . . . . 7 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∧ 𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
244	243	ancomd 466	. . . . . 6 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))
245	143, 244	jca 553	. . . . 5 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) → (𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))))
246		simprl 790	. . . . . . 7 ⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → 𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))))
247	133	adantr 480	. . . . . . 7 ⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∈ 𝐽)
248	246, 247	eqeltrd 2688	. . . . . 6 ⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → 𝑥 ∈ 𝐽)
249		simprr 792	. . . . . . 7 ⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))
250	55	adantr 480	. . . . . . 7 ⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ) ∈ ℕ0)
251	249, 250	eqeltrd 2688	. . . . . 6 ⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → 𝑦 ∈ ℕ0)
252	121	adantr 480	. . . . . . 7 ⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → 𝑎 = ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
253	249	oveq2d 6565	. . . . . . . 8 ⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → (2↑𝑦) = (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))
254	253, 246	oveq12d 6567	. . . . . . 7 ⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → ((2↑𝑦) · 𝑥) = ((2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )) · (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
255	252, 254	eqtr4d 2647	. . . . . 6 ⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → 𝑎 = ((2↑𝑦) · 𝑥))
256	248, 251, 255	jca31 555	. . . . 5 ⊢ ((𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) → ((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)))
257	245, 256	impbii 198	. . . 4 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ↔ (𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))))
258	257	a1i 11	. . 3 ⊢ (⊤ → (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ℕ0) ∧ 𝑎 = ((2↑𝑦) · 𝑥)) ↔ (𝑎 ∈ ℕ ∧ (𝑥 = (𝑎 / (2↑sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < ))) ∧ 𝑦 = sup({𝑘 ∈ ℕ0 ∣ (2↑𝑘) ∥ 𝑎}, ℕ0, < )))))
259	1, 13, 135, 258	f1od2 28887	. 2 ⊢ (⊤ → 𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ)
260	259	trud 1484	1 ⊢ 𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475  ⊤wtru 1476   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  {crab 2900   ⊆ wss 3540  ∅c0 3874   class class class wbr 4583   Or wor 4958   × cxp 5036  –1-1-onto→wf1o 5803  (class class class)co 6549   ↦ cmpt2 6551  Fincfn 7841  supcsup 8229  ℂcc 9813  ℝcr 9814  0cc0 9815  1c1 9816   + caddc 9818   · cmul 9820   < clt 9953   ≤ cle 9954   − cmin 10145   / cdiv 10563  ℕcn 10897  2c2 10947  ℕ₀cn0 11169  ℤcz 11254  ...cfz 12197  ↑cexp 12722   ∥ cdvds 14821

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-sup 8231  df-inf 8232  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-n0 11170  df-z 11255  df-uz 11564  df-fz 12198  df-seq 12664  df-exp 12723  df-dvds 14822

This theorem is referenced by:  eulerpartgbij  29761  eulerpartlemgvv  29765  eulerpartlemgh  29767  eulerpartlemgf  29768