Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  eulerpartlemgvv Structured version   Visualization version   GIF version

Theorem eulerpartlemgvv 31036
Description: Lemma for eulerpart 31042: value of the function 𝐺 evaluated. (Contributed by Thierry Arnoux, 10-Aug-2018.)
Hypotheses
Ref Expression
eulerpart.p 𝑃 = {𝑓 ∈ (ℕ0𝑚 ℕ) ∣ ((𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓𝑘) · 𝑘) = 𝑁)}
eulerpart.o 𝑂 = {𝑔𝑃 ∣ ∀𝑛 ∈ (𝑔 “ ℕ) ¬ 2 ∥ 𝑛}
eulerpart.d 𝐷 = {𝑔𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔𝑛) ≤ 1}
eulerpart.j 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}
eulerpart.f 𝐹 = (𝑥𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))
eulerpart.h 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}
eulerpart.m 𝑀 = (𝑟𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐽𝑦 ∈ (𝑟𝑥))})
eulerpart.r 𝑅 = {𝑓 ∣ (𝑓 “ ℕ) ∈ Fin}
eulerpart.t 𝑇 = {𝑓 ∈ (ℕ0𝑚 ℕ) ∣ (𝑓 “ ℕ) ⊆ 𝐽}
eulerpart.g 𝐺 = (𝑜 ∈ (𝑇𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
Assertion
Ref Expression
eulerpartlemgvv ((𝐴 ∈ (𝑇𝑅) ∧ 𝐵 ∈ ℕ) → ((𝐺𝐴)‘𝐵) = if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝐵, 1, 0))
Distinct variable groups:   𝑓,𝑘,𝑛,𝑡,𝑥,𝑦,𝑧   𝑓,𝑜,𝑟,𝐴   𝑜,𝐹   𝐻,𝑟   𝑓,𝐽   𝑛,𝑜,𝑟,𝐽,𝑥,𝑦   𝑜,𝑀   𝑓,𝑁   𝑔,𝑛,𝑃   𝑅,𝑜   𝑇,𝑜   𝑡,𝐴,𝑛,𝑥,𝑦   𝐵,𝑛,𝑡,𝑥,𝑦   𝑛,𝐹,𝑡,𝑥,𝑦   𝑡,𝐽   𝑛,𝑀,𝑡,𝑥,𝑦   𝑅,𝑛   𝑡,𝑟,𝑅,𝑥,𝑦   𝑇,𝑛,𝑟,𝑡,𝑥,𝑦
Allowed substitution hints:   𝐴(𝑧,𝑔,𝑘)   𝐵(𝑧,𝑓,𝑔,𝑘,𝑜,𝑟)   𝐷(𝑥,𝑦,𝑧,𝑡,𝑓,𝑔,𝑘,𝑛,𝑜,𝑟)   𝑃(𝑥,𝑦,𝑧,𝑡,𝑓,𝑘,𝑜,𝑟)   𝑅(𝑧,𝑓,𝑔,𝑘)   𝑇(𝑧,𝑓,𝑔,𝑘)   𝐹(𝑧,𝑓,𝑔,𝑘,𝑟)   𝐺(𝑥,𝑦,𝑧,𝑡,𝑓,𝑔,𝑘,𝑛,𝑜,𝑟)   𝐻(𝑥,𝑦,𝑧,𝑡,𝑓,𝑔,𝑘,𝑛,𝑜)   𝐽(𝑧,𝑔,𝑘)   𝑀(𝑧,𝑓,𝑔,𝑘,𝑟)   𝑁(𝑥,𝑦,𝑧,𝑡,𝑔,𝑘,𝑛,𝑜,𝑟)   𝑂(𝑥,𝑦,𝑧,𝑡,𝑓,𝑔,𝑘,𝑛,𝑜,𝑟)

Proof of Theorem eulerpartlemgvv
Dummy variable 𝑤 is distinct from all other variables.
StepHypRef Expression
1 eulerpart.p . . . . 5 𝑃 = {𝑓 ∈ (ℕ0𝑚 ℕ) ∣ ((𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓𝑘) · 𝑘) = 𝑁)}
2 eulerpart.o . . . . 5 𝑂 = {𝑔𝑃 ∣ ∀𝑛 ∈ (𝑔 “ ℕ) ¬ 2 ∥ 𝑛}
3 eulerpart.d . . . . 5 𝐷 = {𝑔𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔𝑛) ≤ 1}
4 eulerpart.j . . . . 5 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}
5 eulerpart.f . . . . 5 𝐹 = (𝑥𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))
6 eulerpart.h . . . . 5 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}
7 eulerpart.m . . . . 5 𝑀 = (𝑟𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐽𝑦 ∈ (𝑟𝑥))})
8 eulerpart.r . . . . 5 𝑅 = {𝑓 ∣ (𝑓 “ ℕ) ∈ Fin}
9 eulerpart.t . . . . 5 𝑇 = {𝑓 ∈ (ℕ0𝑚 ℕ) ∣ (𝑓 “ ℕ) ⊆ 𝐽}
10 eulerpart.g . . . . 5 𝐺 = (𝑜 ∈ (𝑇𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
111, 2, 3, 4, 5, 6, 7, 8, 9, 10eulerpartlemgv 31033 . . . 4 (𝐴 ∈ (𝑇𝑅) → (𝐺𝐴) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝐴𝐽))))))
1211fveq1d 6448 . . 3 (𝐴 ∈ (𝑇𝑅) → ((𝐺𝐴)‘𝐵) = (((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝐴𝐽)))))‘𝐵))
1312adantr 474 . 2 ((𝐴 ∈ (𝑇𝑅) ∧ 𝐵 ∈ ℕ) → ((𝐺𝐴)‘𝐵) = (((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝐴𝐽)))))‘𝐵))
14 nnex 11381 . . 3 ℕ ∈ V
15 imassrn 5731 . . . 4 (𝐹 “ (𝑀‘(bits ∘ (𝐴𝐽)))) ⊆ ran 𝐹
164, 5oddpwdc 31014 . . . . 5 𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ
17 f1of 6391 . . . . 5 (𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ → 𝐹:(𝐽 × ℕ0)⟶ℕ)
18 frn 6297 . . . . 5 (𝐹:(𝐽 × ℕ0)⟶ℕ → ran 𝐹 ⊆ ℕ)
1916, 17, 18mp2b 10 . . . 4 ran 𝐹 ⊆ ℕ
2015, 19sstri 3830 . . 3 (𝐹 “ (𝑀‘(bits ∘ (𝐴𝐽)))) ⊆ ℕ
21 simpr 479 . . 3 ((𝐴 ∈ (𝑇𝑅) ∧ 𝐵 ∈ ℕ) → 𝐵 ∈ ℕ)
22 indfval 30676 . . 3 ((ℕ ∈ V ∧ (𝐹 “ (𝑀‘(bits ∘ (𝐴𝐽)))) ⊆ ℕ ∧ 𝐵 ∈ ℕ) → (((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝐴𝐽)))))‘𝐵) = if(𝐵 ∈ (𝐹 “ (𝑀‘(bits ∘ (𝐴𝐽)))), 1, 0))
2314, 20, 21, 22mp3an12i 1538 . 2 ((𝐴 ∈ (𝑇𝑅) ∧ 𝐵 ∈ ℕ) → (((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝐴𝐽)))))‘𝐵) = if(𝐵 ∈ (𝐹 “ (𝑀‘(bits ∘ (𝐴𝐽)))), 1, 0))
24 ffn 6291 . . . . . 6 (𝐹:(𝐽 × ℕ0)⟶ℕ → 𝐹 Fn (𝐽 × ℕ0))
2516, 17, 24mp2b 10 . . . . 5 𝐹 Fn (𝐽 × ℕ0)
261, 2, 3, 4, 5, 6, 7, 8, 9, 10eulerpartlemmf 31035 . . . . . . . . 9 (𝐴 ∈ (𝑇𝑅) → (bits ∘ (𝐴𝐽)) ∈ 𝐻)
271, 2, 3, 4, 5, 6, 7eulerpartlem1 31027 . . . . . . . . . . 11 𝑀:𝐻1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)
28 f1of 6391 . . . . . . . . . . 11 (𝑀:𝐻1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin) → 𝑀:𝐻⟶(𝒫 (𝐽 × ℕ0) ∩ Fin))
2927, 28ax-mp 5 . . . . . . . . . 10 𝑀:𝐻⟶(𝒫 (𝐽 × ℕ0) ∩ Fin)
3029ffvelrni 6622 . . . . . . . . 9 ((bits ∘ (𝐴𝐽)) ∈ 𝐻 → (𝑀‘(bits ∘ (𝐴𝐽))) ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin))
3126, 30syl 17 . . . . . . . 8 (𝐴 ∈ (𝑇𝑅) → (𝑀‘(bits ∘ (𝐴𝐽))) ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin))
3231elin1d 4025 . . . . . . 7 (𝐴 ∈ (𝑇𝑅) → (𝑀‘(bits ∘ (𝐴𝐽))) ∈ 𝒫 (𝐽 × ℕ0))
3332adantr 474 . . . . . 6 ((𝐴 ∈ (𝑇𝑅) ∧ 𝐵 ∈ ℕ) → (𝑀‘(bits ∘ (𝐴𝐽))) ∈ 𝒫 (𝐽 × ℕ0))
3433elpwid 4391 . . . . 5 ((𝐴 ∈ (𝑇𝑅) ∧ 𝐵 ∈ ℕ) → (𝑀‘(bits ∘ (𝐴𝐽))) ⊆ (𝐽 × ℕ0))
35 fvelimab 6513 . . . . 5 ((𝐹 Fn (𝐽 × ℕ0) ∧ (𝑀‘(bits ∘ (𝐴𝐽))) ⊆ (𝐽 × ℕ0)) → (𝐵 ∈ (𝐹 “ (𝑀‘(bits ∘ (𝐴𝐽)))) ↔ ∃𝑤 ∈ (𝑀‘(bits ∘ (𝐴𝐽)))(𝐹𝑤) = 𝐵))
3625, 34, 35sylancr 581 . . . 4 ((𝐴 ∈ (𝑇𝑅) ∧ 𝐵 ∈ ℕ) → (𝐵 ∈ (𝐹 “ (𝑀‘(bits ∘ (𝐴𝐽)))) ↔ ∃𝑤 ∈ (𝑀‘(bits ∘ (𝐴𝐽)))(𝐹𝑤) = 𝐵))
374ssrab3 3909 . . . . . . . . 9 𝐽 ⊆ ℕ
38 fveq1 6445 . . . . . . . . . . . . . . . . . . 19 (𝑟 = (bits ∘ (𝐴𝐽)) → (𝑟𝑥) = ((bits ∘ (𝐴𝐽))‘𝑥))
3938eleq2d 2845 . . . . . . . . . . . . . . . . . 18 (𝑟 = (bits ∘ (𝐴𝐽)) → (𝑦 ∈ (𝑟𝑥) ↔ 𝑦 ∈ ((bits ∘ (𝐴𝐽))‘𝑥)))
4039anbi2d 622 . . . . . . . . . . . . . . . . 17 (𝑟 = (bits ∘ (𝐴𝐽)) → ((𝑥𝐽𝑦 ∈ (𝑟𝑥)) ↔ (𝑥𝐽𝑦 ∈ ((bits ∘ (𝐴𝐽))‘𝑥))))
4140opabbidv 4952 . . . . . . . . . . . . . . . 16 (𝑟 = (bits ∘ (𝐴𝐽)) → {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐽𝑦 ∈ (𝑟𝑥))} = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐽𝑦 ∈ ((bits ∘ (𝐴𝐽))‘𝑥))})
4214, 37ssexi 5040 . . . . . . . . . . . . . . . . . 18 𝐽 ∈ V
43 abid2 2912 . . . . . . . . . . . . . . . . . . . 20 {𝑦𝑦 ∈ ((bits ∘ (𝐴𝐽))‘𝑥)} = ((bits ∘ (𝐴𝐽))‘𝑥)
4443fvexi 6460 . . . . . . . . . . . . . . . . . . 19 {𝑦𝑦 ∈ ((bits ∘ (𝐴𝐽))‘𝑥)} ∈ V
4544a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑥𝐽 → {𝑦𝑦 ∈ ((bits ∘ (𝐴𝐽))‘𝑥)} ∈ V)
4642, 45opabex3 7424 . . . . . . . . . . . . . . . . 17 {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐽𝑦 ∈ ((bits ∘ (𝐴𝐽))‘𝑥))} ∈ V
4746a1i 11 . . . . . . . . . . . . . . . 16 (𝐴 ∈ (𝑇𝑅) → {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐽𝑦 ∈ ((bits ∘ (𝐴𝐽))‘𝑥))} ∈ V)
487, 41, 26, 47fvmptd3 6564 . . . . . . . . . . . . . . 15 (𝐴 ∈ (𝑇𝑅) → (𝑀‘(bits ∘ (𝐴𝐽))) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐽𝑦 ∈ ((bits ∘ (𝐴𝐽))‘𝑥))})
49 simpl 476 . . . . . . . . . . . . . . . . . 18 ((𝑥 = 𝑡𝑦 = 𝑛) → 𝑥 = 𝑡)
5049eleq1d 2844 . . . . . . . . . . . . . . . . 17 ((𝑥 = 𝑡𝑦 = 𝑛) → (𝑥𝐽𝑡𝐽))
51 simpr 479 . . . . . . . . . . . . . . . . . 18 ((𝑥 = 𝑡𝑦 = 𝑛) → 𝑦 = 𝑛)
5249fveq2d 6450 . . . . . . . . . . . . . . . . . 18 ((𝑥 = 𝑡𝑦 = 𝑛) → ((bits ∘ (𝐴𝐽))‘𝑥) = ((bits ∘ (𝐴𝐽))‘𝑡))
5351, 52eleq12d 2853 . . . . . . . . . . . . . . . . 17 ((𝑥 = 𝑡𝑦 = 𝑛) → (𝑦 ∈ ((bits ∘ (𝐴𝐽))‘𝑥) ↔ 𝑛 ∈ ((bits ∘ (𝐴𝐽))‘𝑡)))
5450, 53anbi12d 624 . . . . . . . . . . . . . . . 16 ((𝑥 = 𝑡𝑦 = 𝑛) → ((𝑥𝐽𝑦 ∈ ((bits ∘ (𝐴𝐽))‘𝑥)) ↔ (𝑡𝐽𝑛 ∈ ((bits ∘ (𝐴𝐽))‘𝑡))))
5554cbvopabv 4958 . . . . . . . . . . . . . . 15 {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐽𝑦 ∈ ((bits ∘ (𝐴𝐽))‘𝑥))} = {⟨𝑡, 𝑛⟩ ∣ (𝑡𝐽𝑛 ∈ ((bits ∘ (𝐴𝐽))‘𝑡))}
5648, 55syl6eq 2830 . . . . . . . . . . . . . 14 (𝐴 ∈ (𝑇𝑅) → (𝑀‘(bits ∘ (𝐴𝐽))) = {⟨𝑡, 𝑛⟩ ∣ (𝑡𝐽𝑛 ∈ ((bits ∘ (𝐴𝐽))‘𝑡))})
5756eleq2d 2845 . . . . . . . . . . . . 13 (𝐴 ∈ (𝑇𝑅) → (𝑤 ∈ (𝑀‘(bits ∘ (𝐴𝐽))) ↔ 𝑤 ∈ {⟨𝑡, 𝑛⟩ ∣ (𝑡𝐽𝑛 ∈ ((bits ∘ (𝐴𝐽))‘𝑡))}))
581, 2, 3, 4, 5, 6, 7, 8, 9eulerpartlemt0 31029 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐴 ∈ (𝑇𝑅) ↔ (𝐴 ∈ (ℕ0𝑚 ℕ) ∧ (𝐴 “ ℕ) ∈ Fin ∧ (𝐴 “ ℕ) ⊆ 𝐽))
5958simp1bi 1136 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐴 ∈ (𝑇𝑅) → 𝐴 ∈ (ℕ0𝑚 ℕ))
60 nn0ex 11649 . . . . . . . . . . . . . . . . . . . . . . . 24 0 ∈ V
6160, 14elmap 8169 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐴 ∈ (ℕ0𝑚 ℕ) ↔ 𝐴:ℕ⟶ℕ0)
6259, 61sylib 210 . . . . . . . . . . . . . . . . . . . . . 22 (𝐴 ∈ (𝑇𝑅) → 𝐴:ℕ⟶ℕ0)
63 ffun 6294 . . . . . . . . . . . . . . . . . . . . . 22 (𝐴:ℕ⟶ℕ0 → Fun 𝐴)
64 funres 6177 . . . . . . . . . . . . . . . . . . . . . 22 (Fun 𝐴 → Fun (𝐴𝐽))
6562, 63, 643syl 18 . . . . . . . . . . . . . . . . . . . . 21 (𝐴 ∈ (𝑇𝑅) → Fun (𝐴𝐽))
66 fssres 6320 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴:ℕ⟶ℕ0𝐽 ⊆ ℕ) → (𝐴𝐽):𝐽⟶ℕ0)
6762, 37, 66sylancl 580 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐴 ∈ (𝑇𝑅) → (𝐴𝐽):𝐽⟶ℕ0)
68 fdm 6299 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴𝐽):𝐽⟶ℕ0 → dom (𝐴𝐽) = 𝐽)
6968eleq2d 2845 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴𝐽):𝐽⟶ℕ0 → (𝑡 ∈ dom (𝐴𝐽) ↔ 𝑡𝐽))
7067, 69syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝐴 ∈ (𝑇𝑅) → (𝑡 ∈ dom (𝐴𝐽) ↔ 𝑡𝐽))
7170biimpar 471 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑡𝐽) → 𝑡 ∈ dom (𝐴𝐽))
72 fvco 6534 . . . . . . . . . . . . . . . . . . . . 21 ((Fun (𝐴𝐽) ∧ 𝑡 ∈ dom (𝐴𝐽)) → ((bits ∘ (𝐴𝐽))‘𝑡) = (bits‘((𝐴𝐽)‘𝑡)))
7365, 71, 72syl2an2r 675 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑡𝐽) → ((bits ∘ (𝐴𝐽))‘𝑡) = (bits‘((𝐴𝐽)‘𝑡)))
74 fvres 6465 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡𝐽 → ((𝐴𝐽)‘𝑡) = (𝐴𝑡))
7574fveq2d 6450 . . . . . . . . . . . . . . . . . . . . 21 (𝑡𝐽 → (bits‘((𝐴𝐽)‘𝑡)) = (bits‘(𝐴𝑡)))
7675adantl 475 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑡𝐽) → (bits‘((𝐴𝐽)‘𝑡)) = (bits‘(𝐴𝑡)))
7773, 76eqtrd 2814 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑡𝐽) → ((bits ∘ (𝐴𝐽))‘𝑡) = (bits‘(𝐴𝑡)))
7877eleq2d 2845 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑡𝐽) → (𝑛 ∈ ((bits ∘ (𝐴𝐽))‘𝑡) ↔ 𝑛 ∈ (bits‘(𝐴𝑡))))
7978pm5.32da 574 . . . . . . . . . . . . . . . . 17 (𝐴 ∈ (𝑇𝑅) → ((𝑡𝐽𝑛 ∈ ((bits ∘ (𝐴𝐽))‘𝑡)) ↔ (𝑡𝐽𝑛 ∈ (bits‘(𝐴𝑡)))))
8079opabbidv 4952 . . . . . . . . . . . . . . . 16 (𝐴 ∈ (𝑇𝑅) → {⟨𝑡, 𝑛⟩ ∣ (𝑡𝐽𝑛 ∈ ((bits ∘ (𝐴𝐽))‘𝑡))} = {⟨𝑡, 𝑛⟩ ∣ (𝑡𝐽𝑛 ∈ (bits‘(𝐴𝑡)))})
8180eleq2d 2845 . . . . . . . . . . . . . . 15 (𝐴 ∈ (𝑇𝑅) → (𝑤 ∈ {⟨𝑡, 𝑛⟩ ∣ (𝑡𝐽𝑛 ∈ ((bits ∘ (𝐴𝐽))‘𝑡))} ↔ 𝑤 ∈ {⟨𝑡, 𝑛⟩ ∣ (𝑡𝐽𝑛 ∈ (bits‘(𝐴𝑡)))}))
82 elopab 5220 . . . . . . . . . . . . . . 15 (𝑤 ∈ {⟨𝑡, 𝑛⟩ ∣ (𝑡𝐽𝑛 ∈ (bits‘(𝐴𝑡)))} ↔ ∃𝑡𝑛(𝑤 = ⟨𝑡, 𝑛⟩ ∧ (𝑡𝐽𝑛 ∈ (bits‘(𝐴𝑡)))))
8381, 82syl6bb 279 . . . . . . . . . . . . . 14 (𝐴 ∈ (𝑇𝑅) → (𝑤 ∈ {⟨𝑡, 𝑛⟩ ∣ (𝑡𝐽𝑛 ∈ ((bits ∘ (𝐴𝐽))‘𝑡))} ↔ ∃𝑡𝑛(𝑤 = ⟨𝑡, 𝑛⟩ ∧ (𝑡𝐽𝑛 ∈ (bits‘(𝐴𝑡))))))
84 ancom 454 . . . . . . . . . . . . . . . . 17 ((𝑤 = ⟨𝑡, 𝑛⟩ ∧ (𝑡𝐽𝑛 ∈ (bits‘(𝐴𝑡)))) ↔ ((𝑡𝐽𝑛 ∈ (bits‘(𝐴𝑡))) ∧ 𝑤 = ⟨𝑡, 𝑛⟩))
85 anass 462 . . . . . . . . . . . . . . . . 17 (((𝑡𝐽𝑛 ∈ (bits‘(𝐴𝑡))) ∧ 𝑤 = ⟨𝑡, 𝑛⟩) ↔ (𝑡𝐽 ∧ (𝑛 ∈ (bits‘(𝐴𝑡)) ∧ 𝑤 = ⟨𝑡, 𝑛⟩)))
8684, 85bitri 267 . . . . . . . . . . . . . . . 16 ((𝑤 = ⟨𝑡, 𝑛⟩ ∧ (𝑡𝐽𝑛 ∈ (bits‘(𝐴𝑡)))) ↔ (𝑡𝐽 ∧ (𝑛 ∈ (bits‘(𝐴𝑡)) ∧ 𝑤 = ⟨𝑡, 𝑛⟩)))
87862exbii 1893 . . . . . . . . . . . . . . 15 (∃𝑡𝑛(𝑤 = ⟨𝑡, 𝑛⟩ ∧ (𝑡𝐽𝑛 ∈ (bits‘(𝐴𝑡)))) ↔ ∃𝑡𝑛(𝑡𝐽 ∧ (𝑛 ∈ (bits‘(𝐴𝑡)) ∧ 𝑤 = ⟨𝑡, 𝑛⟩)))
88 df-rex 3096 . . . . . . . . . . . . . . . . . 18 (∃𝑛 ∈ (bits‘(𝐴𝑡))𝑤 = ⟨𝑡, 𝑛⟩ ↔ ∃𝑛(𝑛 ∈ (bits‘(𝐴𝑡)) ∧ 𝑤 = ⟨𝑡, 𝑛⟩))
8988anbi2i 616 . . . . . . . . . . . . . . . . 17 ((𝑡𝐽 ∧ ∃𝑛 ∈ (bits‘(𝐴𝑡))𝑤 = ⟨𝑡, 𝑛⟩) ↔ (𝑡𝐽 ∧ ∃𝑛(𝑛 ∈ (bits‘(𝐴𝑡)) ∧ 𝑤 = ⟨𝑡, 𝑛⟩)))
9089exbii 1892 . . . . . . . . . . . . . . . 16 (∃𝑡(𝑡𝐽 ∧ ∃𝑛 ∈ (bits‘(𝐴𝑡))𝑤 = ⟨𝑡, 𝑛⟩) ↔ ∃𝑡(𝑡𝐽 ∧ ∃𝑛(𝑛 ∈ (bits‘(𝐴𝑡)) ∧ 𝑤 = ⟨𝑡, 𝑛⟩)))
91 df-rex 3096 . . . . . . . . . . . . . . . 16 (∃𝑡𝐽𝑛 ∈ (bits‘(𝐴𝑡))𝑤 = ⟨𝑡, 𝑛⟩ ↔ ∃𝑡(𝑡𝐽 ∧ ∃𝑛 ∈ (bits‘(𝐴𝑡))𝑤 = ⟨𝑡, 𝑛⟩))
92 exdistr 1997 . . . . . . . . . . . . . . . 16 (∃𝑡𝑛(𝑡𝐽 ∧ (𝑛 ∈ (bits‘(𝐴𝑡)) ∧ 𝑤 = ⟨𝑡, 𝑛⟩)) ↔ ∃𝑡(𝑡𝐽 ∧ ∃𝑛(𝑛 ∈ (bits‘(𝐴𝑡)) ∧ 𝑤 = ⟨𝑡, 𝑛⟩)))
9390, 91, 923bitr4i 295 . . . . . . . . . . . . . . 15 (∃𝑡𝐽𝑛 ∈ (bits‘(𝐴𝑡))𝑤 = ⟨𝑡, 𝑛⟩ ↔ ∃𝑡𝑛(𝑡𝐽 ∧ (𝑛 ∈ (bits‘(𝐴𝑡)) ∧ 𝑤 = ⟨𝑡, 𝑛⟩)))
9487, 93bitr4i 270 . . . . . . . . . . . . . 14 (∃𝑡𝑛(𝑤 = ⟨𝑡, 𝑛⟩ ∧ (𝑡𝐽𝑛 ∈ (bits‘(𝐴𝑡)))) ↔ ∃𝑡𝐽𝑛 ∈ (bits‘(𝐴𝑡))𝑤 = ⟨𝑡, 𝑛⟩)
9583, 94syl6bb 279 . . . . . . . . . . . . 13 (𝐴 ∈ (𝑇𝑅) → (𝑤 ∈ {⟨𝑡, 𝑛⟩ ∣ (𝑡𝐽𝑛 ∈ ((bits ∘ (𝐴𝐽))‘𝑡))} ↔ ∃𝑡𝐽𝑛 ∈ (bits‘(𝐴𝑡))𝑤 = ⟨𝑡, 𝑛⟩))
9657, 95bitrd 271 . . . . . . . . . . . 12 (𝐴 ∈ (𝑇𝑅) → (𝑤 ∈ (𝑀‘(bits ∘ (𝐴𝐽))) ↔ ∃𝑡𝐽𝑛 ∈ (bits‘(𝐴𝑡))𝑤 = ⟨𝑡, 𝑛⟩))
9796biimpa 470 . . . . . . . . . . 11 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴𝐽)))) → ∃𝑡𝐽𝑛 ∈ (bits‘(𝐴𝑡))𝑤 = ⟨𝑡, 𝑛⟩)
9897adantlr 705 . . . . . . . . . 10 (((𝐴 ∈ (𝑇𝑅) ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴𝐽)))) → ∃𝑡𝐽𝑛 ∈ (bits‘(𝐴𝑡))𝑤 = ⟨𝑡, 𝑛⟩)
99 fveq2 6446 . . . . . . . . . . . . . 14 (𝑤 = ⟨𝑡, 𝑛⟩ → (𝐹𝑤) = (𝐹‘⟨𝑡, 𝑛⟩))
10099adantl 475 . . . . . . . . . . . . 13 (((((𝐴 ∈ (𝑇𝑅) ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴𝐽)))) ∧ (𝑡𝐽𝑛 ∈ (bits‘(𝐴𝑡)))) ∧ 𝑤 = ⟨𝑡, 𝑛⟩) → (𝐹𝑤) = (𝐹‘⟨𝑡, 𝑛⟩))
101 bitsss 15554 . . . . . . . . . . . . . . . . 17 (bits‘(𝐴𝑡)) ⊆ ℕ0
102101sseli 3817 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (bits‘(𝐴𝑡)) → 𝑛 ∈ ℕ0)
103102anim2i 610 . . . . . . . . . . . . . . 15 ((𝑡𝐽𝑛 ∈ (bits‘(𝐴𝑡))) → (𝑡𝐽𝑛 ∈ ℕ0))
104103ad2antlr 717 . . . . . . . . . . . . . 14 (((((𝐴 ∈ (𝑇𝑅) ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴𝐽)))) ∧ (𝑡𝐽𝑛 ∈ (bits‘(𝐴𝑡)))) ∧ 𝑤 = ⟨𝑡, 𝑛⟩) → (𝑡𝐽𝑛 ∈ ℕ0))
105 opelxp 5391 . . . . . . . . . . . . . . 15 (⟨𝑡, 𝑛⟩ ∈ (𝐽 × ℕ0) ↔ (𝑡𝐽𝑛 ∈ ℕ0))
1064, 5oddpwdcv 31015 . . . . . . . . . . . . . . . 16 (⟨𝑡, 𝑛⟩ ∈ (𝐽 × ℕ0) → (𝐹‘⟨𝑡, 𝑛⟩) = ((2↑(2nd ‘⟨𝑡, 𝑛⟩)) · (1st ‘⟨𝑡, 𝑛⟩)))
107 vex 3401 . . . . . . . . . . . . . . . . . . 19 𝑡 ∈ V
108 vex 3401 . . . . . . . . . . . . . . . . . . 19 𝑛 ∈ V
109107, 108op2nd 7454 . . . . . . . . . . . . . . . . . 18 (2nd ‘⟨𝑡, 𝑛⟩) = 𝑛
110109oveq2i 6933 . . . . . . . . . . . . . . . . 17 (2↑(2nd ‘⟨𝑡, 𝑛⟩)) = (2↑𝑛)
111107, 108op1st 7453 . . . . . . . . . . . . . . . . 17 (1st ‘⟨𝑡, 𝑛⟩) = 𝑡
112110, 111oveq12i 6934 . . . . . . . . . . . . . . . 16 ((2↑(2nd ‘⟨𝑡, 𝑛⟩)) · (1st ‘⟨𝑡, 𝑛⟩)) = ((2↑𝑛) · 𝑡)
113106, 112syl6eq 2830 . . . . . . . . . . . . . . 15 (⟨𝑡, 𝑛⟩ ∈ (𝐽 × ℕ0) → (𝐹‘⟨𝑡, 𝑛⟩) = ((2↑𝑛) · 𝑡))
114105, 113sylbir 227 . . . . . . . . . . . . . 14 ((𝑡𝐽𝑛 ∈ ℕ0) → (𝐹‘⟨𝑡, 𝑛⟩) = ((2↑𝑛) · 𝑡))
115104, 114syl 17 . . . . . . . . . . . . 13 (((((𝐴 ∈ (𝑇𝑅) ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴𝐽)))) ∧ (𝑡𝐽𝑛 ∈ (bits‘(𝐴𝑡)))) ∧ 𝑤 = ⟨𝑡, 𝑛⟩) → (𝐹‘⟨𝑡, 𝑛⟩) = ((2↑𝑛) · 𝑡))
116100, 115eqtr2d 2815 . . . . . . . . . . . 12 (((((𝐴 ∈ (𝑇𝑅) ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴𝐽)))) ∧ (𝑡𝐽𝑛 ∈ (bits‘(𝐴𝑡)))) ∧ 𝑤 = ⟨𝑡, 𝑛⟩) → ((2↑𝑛) · 𝑡) = (𝐹𝑤))
117116ex 403 . . . . . . . . . . 11 ((((𝐴 ∈ (𝑇𝑅) ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴𝐽)))) ∧ (𝑡𝐽𝑛 ∈ (bits‘(𝐴𝑡)))) → (𝑤 = ⟨𝑡, 𝑛⟩ → ((2↑𝑛) · 𝑡) = (𝐹𝑤)))
118117reximdvva 3201 . . . . . . . . . 10 (((𝐴 ∈ (𝑇𝑅) ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴𝐽)))) → (∃𝑡𝐽𝑛 ∈ (bits‘(𝐴𝑡))𝑤 = ⟨𝑡, 𝑛⟩ → ∃𝑡𝐽𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = (𝐹𝑤)))
11998, 118mpd 15 . . . . . . . . 9 (((𝐴 ∈ (𝑇𝑅) ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴𝐽)))) → ∃𝑡𝐽𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = (𝐹𝑤))
120 ssrexv 3886 . . . . . . . . 9 (𝐽 ⊆ ℕ → (∃𝑡𝐽𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = (𝐹𝑤) → ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = (𝐹𝑤)))
12137, 119, 120mpsyl 68 . . . . . . . 8 (((𝐴 ∈ (𝑇𝑅) ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴𝐽)))) → ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = (𝐹𝑤))
122121adantr 474 . . . . . . 7 ((((𝐴 ∈ (𝑇𝑅) ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴𝐽)))) ∧ (𝐹𝑤) = 𝐵) → ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = (𝐹𝑤))
123 eqeq2 2789 . . . . . . . . . 10 ((𝐹𝑤) = 𝐵 → (((2↑𝑛) · 𝑡) = (𝐹𝑤) ↔ ((2↑𝑛) · 𝑡) = 𝐵))
124123rexbidv 3237 . . . . . . . . 9 ((𝐹𝑤) = 𝐵 → (∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = (𝐹𝑤) ↔ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝐵))
125124adantl 475 . . . . . . . 8 ((((𝐴 ∈ (𝑇𝑅) ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴𝐽)))) ∧ (𝐹𝑤) = 𝐵) → (∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = (𝐹𝑤) ↔ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝐵))
126125rexbidv 3237 . . . . . . 7 ((((𝐴 ∈ (𝑇𝑅) ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴𝐽)))) ∧ (𝐹𝑤) = 𝐵) → (∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = (𝐹𝑤) ↔ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝐵))
127122, 126mpbid 224 . . . . . 6 ((((𝐴 ∈ (𝑇𝑅) ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴𝐽)))) ∧ (𝐹𝑤) = 𝐵) → ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝐵)
128127r19.29an 3263 . . . . 5 (((𝐴 ∈ (𝑇𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑤 ∈ (𝑀‘(bits ∘ (𝐴𝐽)))(𝐹𝑤) = 𝐵) → ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝐵)
129 simp-5l 775 . . . . . . . 8 ((((((𝐴 ∈ (𝑇𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝐵) ∧ 𝑥𝐽) ∧ 𝑦 ∈ (bits‘(𝐴𝑥))) ∧ ((2↑𝑦) · 𝑥) = 𝐵) → 𝐴 ∈ (𝑇𝑅))
130 simpllr 766 . . . . . . . 8 ((((((𝐴 ∈ (𝑇𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝐵) ∧ 𝑥𝐽) ∧ 𝑦 ∈ (bits‘(𝐴𝑥))) ∧ ((2↑𝑦) · 𝑥) = 𝐵) → 𝑥𝐽)
131 simplr 759 . . . . . . . . 9 ((((((𝐴 ∈ (𝑇𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝐵) ∧ 𝑥𝐽) ∧ 𝑦 ∈ (bits‘(𝐴𝑥))) ∧ ((2↑𝑦) · 𝑥) = 𝐵) → 𝑦 ∈ (bits‘(𝐴𝑥)))
13268eleq2d 2845 . . . . . . . . . . . . . 14 ((𝐴𝐽):𝐽⟶ℕ0 → (𝑥 ∈ dom (𝐴𝐽) ↔ 𝑥𝐽))
13367, 132syl 17 . . . . . . . . . . . . 13 (𝐴 ∈ (𝑇𝑅) → (𝑥 ∈ dom (𝐴𝐽) ↔ 𝑥𝐽))
134133biimpar 471 . . . . . . . . . . . 12 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑥𝐽) → 𝑥 ∈ dom (𝐴𝐽))
135 fvco 6534 . . . . . . . . . . . 12 ((Fun (𝐴𝐽) ∧ 𝑥 ∈ dom (𝐴𝐽)) → ((bits ∘ (𝐴𝐽))‘𝑥) = (bits‘((𝐴𝐽)‘𝑥)))
13665, 134, 135syl2an2r 675 . . . . . . . . . . 11 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑥𝐽) → ((bits ∘ (𝐴𝐽))‘𝑥) = (bits‘((𝐴𝐽)‘𝑥)))
137 fvres 6465 . . . . . . . . . . . . 13 (𝑥𝐽 → ((𝐴𝐽)‘𝑥) = (𝐴𝑥))
138137fveq2d 6450 . . . . . . . . . . . 12 (𝑥𝐽 → (bits‘((𝐴𝐽)‘𝑥)) = (bits‘(𝐴𝑥)))
139138adantl 475 . . . . . . . . . . 11 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑥𝐽) → (bits‘((𝐴𝐽)‘𝑥)) = (bits‘(𝐴𝑥)))
140136, 139eqtrd 2814 . . . . . . . . . 10 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑥𝐽) → ((bits ∘ (𝐴𝐽))‘𝑥) = (bits‘(𝐴𝑥)))
141129, 130, 140syl2anc 579 . . . . . . . . 9 ((((((𝐴 ∈ (𝑇𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝐵) ∧ 𝑥𝐽) ∧ 𝑦 ∈ (bits‘(𝐴𝑥))) ∧ ((2↑𝑦) · 𝑥) = 𝐵) → ((bits ∘ (𝐴𝐽))‘𝑥) = (bits‘(𝐴𝑥)))
142131, 141eleqtrrd 2862 . . . . . . . 8 ((((((𝐴 ∈ (𝑇𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝐵) ∧ 𝑥𝐽) ∧ 𝑦 ∈ (bits‘(𝐴𝑥))) ∧ ((2↑𝑦) · 𝑥) = 𝐵) → 𝑦 ∈ ((bits ∘ (𝐴𝐽))‘𝑥))
14348eleq2d 2845 . . . . . . . . . 10 (𝐴 ∈ (𝑇𝑅) → (⟨𝑥, 𝑦⟩ ∈ (𝑀‘(bits ∘ (𝐴𝐽))) ↔ ⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐽𝑦 ∈ ((bits ∘ (𝐴𝐽))‘𝑥))}))
144 opabid 5219 . . . . . . . . . 10 (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐽𝑦 ∈ ((bits ∘ (𝐴𝐽))‘𝑥))} ↔ (𝑥𝐽𝑦 ∈ ((bits ∘ (𝐴𝐽))‘𝑥)))
145143, 144syl6bb 279 . . . . . . . . 9 (𝐴 ∈ (𝑇𝑅) → (⟨𝑥, 𝑦⟩ ∈ (𝑀‘(bits ∘ (𝐴𝐽))) ↔ (𝑥𝐽𝑦 ∈ ((bits ∘ (𝐴𝐽))‘𝑥))))
146145biimpar 471 . . . . . . . 8 ((𝐴 ∈ (𝑇𝑅) ∧ (𝑥𝐽𝑦 ∈ ((bits ∘ (𝐴𝐽))‘𝑥))) → ⟨𝑥, 𝑦⟩ ∈ (𝑀‘(bits ∘ (𝐴𝐽))))
147129, 130, 142, 146syl12anc 827 . . . . . . 7 ((((((𝐴 ∈ (𝑇𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝐵) ∧ 𝑥𝐽) ∧ 𝑦 ∈ (bits‘(𝐴𝑥))) ∧ ((2↑𝑦) · 𝑥) = 𝐵) → ⟨𝑥, 𝑦⟩ ∈ (𝑀‘(bits ∘ (𝐴𝐽))))
148 simpr 479 . . . . . . . 8 ((((((𝐴 ∈ (𝑇𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝐵) ∧ 𝑥𝐽) ∧ 𝑦 ∈ (bits‘(𝐴𝑥))) ∧ ((2↑𝑦) · 𝑥) = 𝐵) → ((2↑𝑦) · 𝑥) = 𝐵)
14934ad4antr 722 . . . . . . . . 9 ((((((𝐴 ∈ (𝑇𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝐵) ∧ 𝑥𝐽) ∧ 𝑦 ∈ (bits‘(𝐴𝑥))) ∧ ((2↑𝑦) · 𝑥) = 𝐵) → (𝑀‘(bits ∘ (𝐴𝐽))) ⊆ (𝐽 × ℕ0))
150149, 147sseldd 3822 . . . . . . . 8 ((((((𝐴 ∈ (𝑇𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝐵) ∧ 𝑥𝐽) ∧ 𝑦 ∈ (bits‘(𝐴𝑥))) ∧ ((2↑𝑦) · 𝑥) = 𝐵) → ⟨𝑥, 𝑦⟩ ∈ (𝐽 × ℕ0))
151 opeq1 4636 . . . . . . . . . . . 12 (𝑡 = 𝑥 → ⟨𝑡, 𝑦⟩ = ⟨𝑥, 𝑦⟩)
152151eleq1d 2844 . . . . . . . . . . 11 (𝑡 = 𝑥 → (⟨𝑡, 𝑦⟩ ∈ (𝐽 × ℕ0) ↔ ⟨𝑥, 𝑦⟩ ∈ (𝐽 × ℕ0)))
153151fveq2d 6450 . . . . . . . . . . . 12 (𝑡 = 𝑥 → (𝐹‘⟨𝑡, 𝑦⟩) = (𝐹‘⟨𝑥, 𝑦⟩))
154 oveq2 6930 . . . . . . . . . . . 12 (𝑡 = 𝑥 → ((2↑𝑦) · 𝑡) = ((2↑𝑦) · 𝑥))
155153, 154eqeq12d 2793 . . . . . . . . . . 11 (𝑡 = 𝑥 → ((𝐹‘⟨𝑡, 𝑦⟩) = ((2↑𝑦) · 𝑡) ↔ (𝐹‘⟨𝑥, 𝑦⟩) = ((2↑𝑦) · 𝑥)))
156152, 155imbi12d 336 . . . . . . . . . 10 (𝑡 = 𝑥 → ((⟨𝑡, 𝑦⟩ ∈ (𝐽 × ℕ0) → (𝐹‘⟨𝑡, 𝑦⟩) = ((2↑𝑦) · 𝑡)) ↔ (⟨𝑥, 𝑦⟩ ∈ (𝐽 × ℕ0) → (𝐹‘⟨𝑥, 𝑦⟩) = ((2↑𝑦) · 𝑥))))
157 opeq2 4637 . . . . . . . . . . . . 13 (𝑛 = 𝑦 → ⟨𝑡, 𝑛⟩ = ⟨𝑡, 𝑦⟩)
158157eleq1d 2844 . . . . . . . . . . . 12 (𝑛 = 𝑦 → (⟨𝑡, 𝑛⟩ ∈ (𝐽 × ℕ0) ↔ ⟨𝑡, 𝑦⟩ ∈ (𝐽 × ℕ0)))
159157fveq2d 6450 . . . . . . . . . . . . 13 (𝑛 = 𝑦 → (𝐹‘⟨𝑡, 𝑛⟩) = (𝐹‘⟨𝑡, 𝑦⟩))
160 oveq2 6930 . . . . . . . . . . . . . 14 (𝑛 = 𝑦 → (2↑𝑛) = (2↑𝑦))
161160oveq1d 6937 . . . . . . . . . . . . 13 (𝑛 = 𝑦 → ((2↑𝑛) · 𝑡) = ((2↑𝑦) · 𝑡))
162159, 161eqeq12d 2793 . . . . . . . . . . . 12 (𝑛 = 𝑦 → ((𝐹‘⟨𝑡, 𝑛⟩) = ((2↑𝑛) · 𝑡) ↔ (𝐹‘⟨𝑡, 𝑦⟩) = ((2↑𝑦) · 𝑡)))
163158, 162imbi12d 336 . . . . . . . . . . 11 (𝑛 = 𝑦 → ((⟨𝑡, 𝑛⟩ ∈ (𝐽 × ℕ0) → (𝐹‘⟨𝑡, 𝑛⟩) = ((2↑𝑛) · 𝑡)) ↔ (⟨𝑡, 𝑦⟩ ∈ (𝐽 × ℕ0) → (𝐹‘⟨𝑡, 𝑦⟩) = ((2↑𝑦) · 𝑡))))
164163, 113chvarv 2361 . . . . . . . . . 10 (⟨𝑡, 𝑦⟩ ∈ (𝐽 × ℕ0) → (𝐹‘⟨𝑡, 𝑦⟩) = ((2↑𝑦) · 𝑡))
165156, 164chvarv 2361 . . . . . . . . 9 (⟨𝑥, 𝑦⟩ ∈ (𝐽 × ℕ0) → (𝐹‘⟨𝑥, 𝑦⟩) = ((2↑𝑦) · 𝑥))
166 eqeq2 2789 . . . . . . . . . 10 (((2↑𝑦) · 𝑥) = 𝐵 → ((𝐹‘⟨𝑥, 𝑦⟩) = ((2↑𝑦) · 𝑥) ↔ (𝐹‘⟨𝑥, 𝑦⟩) = 𝐵))
167166biimpa 470 . . . . . . . . 9 ((((2↑𝑦) · 𝑥) = 𝐵 ∧ (𝐹‘⟨𝑥, 𝑦⟩) = ((2↑𝑦) · 𝑥)) → (𝐹‘⟨𝑥, 𝑦⟩) = 𝐵)
168165, 167sylan2 586 . . . . . . . 8 ((((2↑𝑦) · 𝑥) = 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ (𝐽 × ℕ0)) → (𝐹‘⟨𝑥, 𝑦⟩) = 𝐵)
169148, 150, 168syl2anc 579 . . . . . . 7 ((((((𝐴 ∈ (𝑇𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝐵) ∧ 𝑥𝐽) ∧ 𝑦 ∈ (bits‘(𝐴𝑥))) ∧ ((2↑𝑦) · 𝑥) = 𝐵) → (𝐹‘⟨𝑥, 𝑦⟩) = 𝐵)
170 fveqeq2 6455 . . . . . . . 8 (𝑤 = ⟨𝑥, 𝑦⟩ → ((𝐹𝑤) = 𝐵 ↔ (𝐹‘⟨𝑥, 𝑦⟩) = 𝐵))
171170rspcev 3511 . . . . . . 7 ((⟨𝑥, 𝑦⟩ ∈ (𝑀‘(bits ∘ (𝐴𝐽))) ∧ (𝐹‘⟨𝑥, 𝑦⟩) = 𝐵) → ∃𝑤 ∈ (𝑀‘(bits ∘ (𝐴𝐽)))(𝐹𝑤) = 𝐵)
172147, 169, 171syl2anc 579 . . . . . 6 ((((((𝐴 ∈ (𝑇𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝐵) ∧ 𝑥𝐽) ∧ 𝑦 ∈ (bits‘(𝐴𝑥))) ∧ ((2↑𝑦) · 𝑥) = 𝐵) → ∃𝑤 ∈ (𝑀‘(bits ∘ (𝐴𝐽)))(𝐹𝑤) = 𝐵)
173 oveq2 6930 . . . . . . . . . . 11 (𝑡 = 𝑥 → ((2↑𝑛) · 𝑡) = ((2↑𝑛) · 𝑥))
174173eqeq1d 2780 . . . . . . . . . 10 (𝑡 = 𝑥 → (((2↑𝑛) · 𝑡) = 𝐵 ↔ ((2↑𝑛) · 𝑥) = 𝐵))
175160oveq1d 6937 . . . . . . . . . . 11 (𝑛 = 𝑦 → ((2↑𝑛) · 𝑥) = ((2↑𝑦) · 𝑥))
176175eqeq1d 2780 . . . . . . . . . 10 (𝑛 = 𝑦 → (((2↑𝑛) · 𝑥) = 𝐵 ↔ ((2↑𝑦) · 𝑥) = 𝐵))
177174, 176sylan9bb 505 . . . . . . . . 9 ((𝑡 = 𝑥𝑛 = 𝑦) → (((2↑𝑛) · 𝑡) = 𝐵 ↔ ((2↑𝑦) · 𝑥) = 𝐵))
178 simpl 476 . . . . . . . . . . 11 ((𝑡 = 𝑥𝑛 = 𝑦) → 𝑡 = 𝑥)
179178fveq2d 6450 . . . . . . . . . 10 ((𝑡 = 𝑥𝑛 = 𝑦) → (𝐴𝑡) = (𝐴𝑥))
180179fveq2d 6450 . . . . . . . . 9 ((𝑡 = 𝑥𝑛 = 𝑦) → (bits‘(𝐴𝑡)) = (bits‘(𝐴𝑥)))
181177, 180cbvrexdva2 3372 . . . . . . . 8 (𝑡 = 𝑥 → (∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝐵 ↔ ∃𝑦 ∈ (bits‘(𝐴𝑥))((2↑𝑦) · 𝑥) = 𝐵))
182181cbvrexv 3368 . . . . . . 7 (∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝐵 ↔ ∃𝑥 ∈ ℕ ∃𝑦 ∈ (bits‘(𝐴𝑥))((2↑𝑦) · 𝑥) = 𝐵)
183 nfv 1957 . . . . . . . . . . . . . 14 𝑦 𝐴 ∈ (𝑇𝑅)
184 nfv 1957 . . . . . . . . . . . . . . 15 𝑦 𝑥 ∈ ℕ
185 nfre1 3186 . . . . . . . . . . . . . . 15 𝑦𝑦 ∈ (bits‘(𝐴𝑥))((2↑𝑦) · 𝑥) = 𝐵
186184, 185nfan 1946 . . . . . . . . . . . . . 14 𝑦(𝑥 ∈ ℕ ∧ ∃𝑦 ∈ (bits‘(𝐴𝑥))((2↑𝑦) · 𝑥) = 𝐵)
187183, 186nfan 1946 . . . . . . . . . . . . 13 𝑦(𝐴 ∈ (𝑇𝑅) ∧ (𝑥 ∈ ℕ ∧ ∃𝑦 ∈ (bits‘(𝐴𝑥))((2↑𝑦) · 𝑥) = 𝐵))
188 simplr 759 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ (𝑇𝑅) ∧ 𝑥 ∈ ℕ) ∧ 𝑦 ∈ (bits‘(𝐴𝑥))) → 𝑥 ∈ ℕ)
189 n0i 4148 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (bits‘(𝐴𝑥)) → ¬ (bits‘(𝐴𝑥)) = ∅)
190189adantl 475 . . . . . . . . . . . . . . . . . . 19 (((𝐴 ∈ (𝑇𝑅) ∧ 𝑥 ∈ ℕ) ∧ 𝑦 ∈ (bits‘(𝐴𝑥))) → ¬ (bits‘(𝐴𝑥)) = ∅)
191 fveq2 6446 . . . . . . . . . . . . . . . . . . . 20 ((𝐴𝑥) = 0 → (bits‘(𝐴𝑥)) = (bits‘0))
192 0bits 15567 . . . . . . . . . . . . . . . . . . . 20 (bits‘0) = ∅
193191, 192syl6eq 2830 . . . . . . . . . . . . . . . . . . 19 ((𝐴𝑥) = 0 → (bits‘(𝐴𝑥)) = ∅)
194190, 193nsyl 138 . . . . . . . . . . . . . . . . . 18 (((𝐴 ∈ (𝑇𝑅) ∧ 𝑥 ∈ ℕ) ∧ 𝑦 ∈ (bits‘(𝐴𝑥))) → ¬ (𝐴𝑥) = 0)
19562ffvelrnda 6623 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑥 ∈ ℕ) → (𝐴𝑥) ∈ ℕ0)
196195adantr 474 . . . . . . . . . . . . . . . . . . . . 21 (((𝐴 ∈ (𝑇𝑅) ∧ 𝑥 ∈ ℕ) ∧ 𝑦 ∈ (bits‘(𝐴𝑥))) → (𝐴𝑥) ∈ ℕ0)
197 elnn0 11644 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴𝑥) ∈ ℕ0 ↔ ((𝐴𝑥) ∈ ℕ ∨ (𝐴𝑥) = 0))
198196, 197sylib 210 . . . . . . . . . . . . . . . . . . . 20 (((𝐴 ∈ (𝑇𝑅) ∧ 𝑥 ∈ ℕ) ∧ 𝑦 ∈ (bits‘(𝐴𝑥))) → ((𝐴𝑥) ∈ ℕ ∨ (𝐴𝑥) = 0))
199198orcomd 860 . . . . . . . . . . . . . . . . . . 19 (((𝐴 ∈ (𝑇𝑅) ∧ 𝑥 ∈ ℕ) ∧ 𝑦 ∈ (bits‘(𝐴𝑥))) → ((𝐴𝑥) = 0 ∨ (𝐴𝑥) ∈ ℕ))
200199orcanai 988 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ (𝑇𝑅) ∧ 𝑥 ∈ ℕ) ∧ 𝑦 ∈ (bits‘(𝐴𝑥))) ∧ ¬ (𝐴𝑥) = 0) → (𝐴𝑥) ∈ ℕ)
201194, 200mpdan 677 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ (𝑇𝑅) ∧ 𝑥 ∈ ℕ) ∧ 𝑦 ∈ (bits‘(𝐴𝑥))) → (𝐴𝑥) ∈ ℕ)
20258simp3bi 1138 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐴 ∈ (𝑇𝑅) → (𝐴 “ ℕ) ⊆ 𝐽)
203202sselda 3821 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑛 ∈ (𝐴 “ ℕ)) → 𝑛𝐽)
204 breq2 4890 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 = 𝑛 → (2 ∥ 𝑧 ↔ 2 ∥ 𝑛))
205204notbid 310 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 = 𝑛 → (¬ 2 ∥ 𝑧 ↔ ¬ 2 ∥ 𝑛))
206205, 4elrab2 3576 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛𝐽 ↔ (𝑛 ∈ ℕ ∧ ¬ 2 ∥ 𝑛))
207206simprbi 492 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛𝐽 → ¬ 2 ∥ 𝑛)
208203, 207syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑛 ∈ (𝐴 “ ℕ)) → ¬ 2 ∥ 𝑛)
209208ralrimiva 3148 . . . . . . . . . . . . . . . . . . . . 21 (𝐴 ∈ (𝑇𝑅) → ∀𝑛 ∈ (𝐴 “ ℕ) ¬ 2 ∥ 𝑛)
210 ffn 6291 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴:ℕ⟶ℕ0𝐴 Fn ℕ)
211 elpreima 6600 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴 Fn ℕ → (𝑛 ∈ (𝐴 “ ℕ) ↔ (𝑛 ∈ ℕ ∧ (𝐴𝑛) ∈ ℕ)))
21262, 210, 2113syl 18 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐴 ∈ (𝑇𝑅) → (𝑛 ∈ (𝐴 “ ℕ) ↔ (𝑛 ∈ ℕ ∧ (𝐴𝑛) ∈ ℕ)))
213212imbi1d 333 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐴 ∈ (𝑇𝑅) → ((𝑛 ∈ (𝐴 “ ℕ) → ¬ 2 ∥ 𝑛) ↔ ((𝑛 ∈ ℕ ∧ (𝐴𝑛) ∈ ℕ) → ¬ 2 ∥ 𝑛)))
214 impexp 443 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑛 ∈ ℕ ∧ (𝐴𝑛) ∈ ℕ) → ¬ 2 ∥ 𝑛) ↔ (𝑛 ∈ ℕ → ((𝐴𝑛) ∈ ℕ → ¬ 2 ∥ 𝑛)))
215213, 214syl6bb 279 . . . . . . . . . . . . . . . . . . . . . 22 (𝐴 ∈ (𝑇𝑅) → ((𝑛 ∈ (𝐴 “ ℕ) → ¬ 2 ∥ 𝑛) ↔ (𝑛 ∈ ℕ → ((𝐴𝑛) ∈ ℕ → ¬ 2 ∥ 𝑛))))
216215ralbidv2 3166 . . . . . . . . . . . . . . . . . . . . 21 (𝐴 ∈ (𝑇𝑅) → (∀𝑛 ∈ (𝐴 “ ℕ) ¬ 2 ∥ 𝑛 ↔ ∀𝑛 ∈ ℕ ((𝐴𝑛) ∈ ℕ → ¬ 2 ∥ 𝑛)))
217209, 216mpbid 224 . . . . . . . . . . . . . . . . . . . 20 (𝐴 ∈ (𝑇𝑅) → ∀𝑛 ∈ ℕ ((𝐴𝑛) ∈ ℕ → ¬ 2 ∥ 𝑛))
218 fveq2 6446 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑛 → (𝐴𝑥) = (𝐴𝑛))
219218eleq1d 2844 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑛 → ((𝐴𝑥) ∈ ℕ ↔ (𝐴𝑛) ∈ ℕ))
220 breq2 4890 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑛 → (2 ∥ 𝑥 ↔ 2 ∥ 𝑛))
221220notbid 310 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑛 → (¬ 2 ∥ 𝑥 ↔ ¬ 2 ∥ 𝑛))
222219, 221imbi12d 336 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑛 → (((𝐴𝑥) ∈ ℕ → ¬ 2 ∥ 𝑥) ↔ ((𝐴𝑛) ∈ ℕ → ¬ 2 ∥ 𝑛)))
223222cbvralv 3367 . . . . . . . . . . . . . . . . . . . 20 (∀𝑥 ∈ ℕ ((𝐴𝑥) ∈ ℕ → ¬ 2 ∥ 𝑥) ↔ ∀𝑛 ∈ ℕ ((𝐴𝑛) ∈ ℕ → ¬ 2 ∥ 𝑛))
224217, 223sylibr 226 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ (𝑇𝑅) → ∀𝑥 ∈ ℕ ((𝐴𝑥) ∈ ℕ → ¬ 2 ∥ 𝑥))
225224r19.21bi 3114 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ (𝑇𝑅) ∧ 𝑥 ∈ ℕ) → ((𝐴𝑥) ∈ ℕ → ¬ 2 ∥ 𝑥))
226225imp 397 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ (𝑇𝑅) ∧ 𝑥 ∈ ℕ) ∧ (𝐴𝑥) ∈ ℕ) → ¬ 2 ∥ 𝑥)
227201, 226syldan 585 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ (𝑇𝑅) ∧ 𝑥 ∈ ℕ) ∧ 𝑦 ∈ (bits‘(𝐴𝑥))) → ¬ 2 ∥ 𝑥)
228 breq2 4890 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑥 → (2 ∥ 𝑧 ↔ 2 ∥ 𝑥))
229228notbid 310 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑥 → (¬ 2 ∥ 𝑧 ↔ ¬ 2 ∥ 𝑥))
230229, 4elrab2 3576 . . . . . . . . . . . . . . . 16 (𝑥𝐽 ↔ (𝑥 ∈ ℕ ∧ ¬ 2 ∥ 𝑥))
231188, 227, 230sylanbrc 578 . . . . . . . . . . . . . . 15 (((𝐴 ∈ (𝑇𝑅) ∧ 𝑥 ∈ ℕ) ∧ 𝑦 ∈ (bits‘(𝐴𝑥))) → 𝑥𝐽)
232231adantlrr 711 . . . . . . . . . . . . . 14 (((𝐴 ∈ (𝑇𝑅) ∧ (𝑥 ∈ ℕ ∧ ∃𝑦 ∈ (bits‘(𝐴𝑥))((2↑𝑦) · 𝑥) = 𝐵)) ∧ 𝑦 ∈ (bits‘(𝐴𝑥))) → 𝑥𝐽)
233232adantr 474 . . . . . . . . . . . . 13 ((((𝐴 ∈ (𝑇𝑅) ∧ (𝑥 ∈ ℕ ∧ ∃𝑦 ∈ (bits‘(𝐴𝑥))((2↑𝑦) · 𝑥) = 𝐵)) ∧ 𝑦 ∈ (bits‘(𝐴𝑥))) ∧ ((2↑𝑦) · 𝑥) = 𝐵) → 𝑥𝐽)
234 simprr 763 . . . . . . . . . . . . 13 ((𝐴 ∈ (𝑇𝑅) ∧ (𝑥 ∈ ℕ ∧ ∃𝑦 ∈ (bits‘(𝐴𝑥))((2↑𝑦) · 𝑥) = 𝐵)) → ∃𝑦 ∈ (bits‘(𝐴𝑥))((2↑𝑦) · 𝑥) = 𝐵)
235187, 233, 234r19.29af 3262 . . . . . . . . . . . 12 ((𝐴 ∈ (𝑇𝑅) ∧ (𝑥 ∈ ℕ ∧ ∃𝑦 ∈ (bits‘(𝐴𝑥))((2↑𝑦) · 𝑥) = 𝐵)) → 𝑥𝐽)
236235, 234jca 507 . . . . . . . . . . 11 ((𝐴 ∈ (𝑇𝑅) ∧ (𝑥 ∈ ℕ ∧ ∃𝑦 ∈ (bits‘(𝐴𝑥))((2↑𝑦) · 𝑥) = 𝐵)) → (𝑥𝐽 ∧ ∃𝑦 ∈ (bits‘(𝐴𝑥))((2↑𝑦) · 𝑥) = 𝐵))
237236ex 403 . . . . . . . . . 10 (𝐴 ∈ (𝑇𝑅) → ((𝑥 ∈ ℕ ∧ ∃𝑦 ∈ (bits‘(𝐴𝑥))((2↑𝑦) · 𝑥) = 𝐵) → (𝑥𝐽 ∧ ∃𝑦 ∈ (bits‘(𝐴𝑥))((2↑𝑦) · 𝑥) = 𝐵)))
238237reximdv2 3195 . . . . . . . . 9 (𝐴 ∈ (𝑇𝑅) → (∃𝑥 ∈ ℕ ∃𝑦 ∈ (bits‘(𝐴𝑥))((2↑𝑦) · 𝑥) = 𝐵 → ∃𝑥𝐽𝑦 ∈ (bits‘(𝐴𝑥))((2↑𝑦) · 𝑥) = 𝐵))
239238imp 397 . . . . . . . 8 ((𝐴 ∈ (𝑇𝑅) ∧ ∃𝑥 ∈ ℕ ∃𝑦 ∈ (bits‘(𝐴𝑥))((2↑𝑦) · 𝑥) = 𝐵) → ∃𝑥𝐽𝑦 ∈ (bits‘(𝐴𝑥))((2↑𝑦) · 𝑥) = 𝐵)
240239adantlr 705 . . . . . . 7 (((𝐴 ∈ (𝑇𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑥 ∈ ℕ ∃𝑦 ∈ (bits‘(𝐴𝑥))((2↑𝑦) · 𝑥) = 𝐵) → ∃𝑥𝐽𝑦 ∈ (bits‘(𝐴𝑥))((2↑𝑦) · 𝑥) = 𝐵)
241182, 240sylan2b 587 . . . . . 6 (((𝐴 ∈ (𝑇𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝐵) → ∃𝑥𝐽𝑦 ∈ (bits‘(𝐴𝑥))((2↑𝑦) · 𝑥) = 𝐵)
242172, 241r19.29vva 3267 . . . . 5 (((𝐴 ∈ (𝑇𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝐵) → ∃𝑤 ∈ (𝑀‘(bits ∘ (𝐴𝐽)))(𝐹𝑤) = 𝐵)
243128, 242impbida 791 . . . 4 ((𝐴 ∈ (𝑇𝑅) ∧ 𝐵 ∈ ℕ) → (∃𝑤 ∈ (𝑀‘(bits ∘ (𝐴𝐽)))(𝐹𝑤) = 𝐵 ↔ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝐵))
24436, 243bitrd 271 . . 3 ((𝐴 ∈ (𝑇𝑅) ∧ 𝐵 ∈ ℕ) → (𝐵 ∈ (𝐹 “ (𝑀‘(bits ∘ (𝐴𝐽)))) ↔ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝐵))
245244ifbid 4329 . 2 ((𝐴 ∈ (𝑇𝑅) ∧ 𝐵 ∈ ℕ) → if(𝐵 ∈ (𝐹 “ (𝑀‘(bits ∘ (𝐴𝐽)))), 1, 0) = if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝐵, 1, 0))
24613, 23, 2453eqtrd 2818 1 ((𝐴 ∈ (𝑇𝑅) ∧ 𝐵 ∈ ℕ) → ((𝐺𝐴)‘𝐵) = if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴𝑡))((2↑𝑛) · 𝑡) = 𝐵, 1, 0))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 386  wo 836   = wceq 1601  wex 1823  wcel 2107  {cab 2763  wral 3090  wrex 3091  {crab 3094  Vcvv 3398  cin 3791  wss 3792  c0 4141  ifcif 4307  𝒫 cpw 4379  cop 4404   class class class wbr 4886  {copab 4948  cmpt 4965   × cxp 5353  ccnv 5354  dom cdm 5355  ran crn 5356  cres 5357  cima 5358  ccom 5359  Fun wfun 6129   Fn wfn 6130  wf 6131  1-1-ontowf1o 6134  cfv 6135  (class class class)co 6922  cmpt2 6924  1st c1st 7443  2nd c2nd 7444   supp csupp 7576  𝑚 cmap 8140  Fincfn 8241  0cc0 10272  1c1 10273   · cmul 10277  cle 10412  cn 11374  2c2 11430  0cn0 11642  cexp 13178  Σcsu 14824  cdvds 15387  bitscbits 15547  𝟭cind 30670
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-rep 5006  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-inf2 8835  ax-ac2 9620  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  ax-pre-sup 10350
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-int 4711  df-iun 4755  df-disj 4855  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-se 5315  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-isom 6144  df-riota 6883  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-om 7344  df-1st 7445  df-2nd 7446  df-supp 7577  df-wrecs 7689  df-recs 7751  df-rdg 7789  df-1o 7843  df-2o 7844  df-oadd 7847  df-er 8026  df-map 8142  df-pm 8143  df-en 8242  df-dom 8243  df-sdom 8244  df-fin 8245  df-sup 8636  df-inf 8637  df-oi 8704  df-card 9098  df-acn 9101  df-ac 9272  df-cda 9325  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-3 11439  df-n0 11643  df-xnn0 11715  df-z 11729  df-uz 11993  df-rp 12138  df-fz 12644  df-fzo 12785  df-fl 12912  df-mod 12988  df-seq 13120  df-exp 13179  df-hash 13436  df-cj 14246  df-re 14247  df-im 14248  df-sqrt 14382  df-abs 14383  df-clim 14627  df-sum 14825  df-dvds 15388  df-bits 15550  df-ind 30671
This theorem is referenced by:  eulerpartlemgs2  31040
  Copyright terms: Public domain W3C validator