P. 317 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 31601-31700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sitmfval 31601	Value of the integral distance between two simple functions. (Contributed by Thierry Arnoux, 30-Jan-2018.)
⊢ 𝐷 = (dist‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures)    &   ⊢ (𝜑 → 𝐹 ∈ dom (𝑊sitg𝑀))    &   ⊢ (𝜑 → 𝐺 ∈ dom (𝑊sitg𝑀))    ⇒   ⊢ (𝜑 → (𝐹(𝑊sitm𝑀)𝐺) = (((ℝ*𝑠 ↾s (0[,]+∞))sitg𝑀)‘(𝐹 ∘f 𝐷𝐺)))
Theorem	sitmcl 31602	Closure of the integral distance between two simple functions, for an extended metric space. (Contributed by Thierry Arnoux, 13-Feb-2018.)
⊢ (𝜑 → 𝑊 ∈ Mnd)    &   ⊢ (𝜑 → 𝑊 ∈ ∞MetSp)    &   ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures)    &   ⊢ (𝜑 → 𝐹 ∈ dom (𝑊sitg𝑀))    &   ⊢ (𝜑 → 𝐺 ∈ dom (𝑊sitg𝑀))    ⇒   ⊢ (𝜑 → (𝐹(𝑊sitm𝑀)𝐺) ∈ (0[,]+∞))
Theorem	sitmf 31603	The integral metric as a function. (Contributed by Thierry Arnoux, 13-Mar-2018.)
⊢ (𝜑 → 𝑊 ∈ Mnd)    &   ⊢ (𝜑 → 𝑊 ∈ ∞MetSp)    &   ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures)    ⇒   ⊢ (𝜑 → (𝑊sitm𝑀):(dom (𝑊sitg𝑀) × dom (𝑊sitg𝑀))⟶(0[,]+∞))
Definition	df-itgm 31604*	Define the Bochner integral as the extension by continuity of the Bochnel integral for simple functions. Bogachev first defines 'fundamental in the mean' sequences, in definition 2.3.1 of [Bogachev] p. 116, and notes that those are actually Cauchy sequences for the pseudometric (𝑤sitm𝑚). He then defines the Bochner integral in chapter 2.4.4 in [Bogachev] p. 118. The definition of the Lebesgue integral, df-itg 24216. (Contributed by Thierry Arnoux, 13-Feb-2018.)
⊢ itgm = (𝑤 ∈ V, 𝑚 ∈ ∪ ran measures ↦ (((metUnif‘(𝑤sitm𝑚))CnExt(UnifSt‘𝑤))‘(𝑤sitg𝑚)))
20.3.19  Euler's partition theorem
Theorem	oddpwdc 31605*	Lemma for eulerpart 31633. 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.)
⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}    &   ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))    ⇒   ⊢ 𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ
Theorem	oddpwdcv 31606*	Lemma for eulerpart 31633: value of the 𝐹 function. (Contributed by Thierry Arnoux, 9-Sep-2017.)
⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}    &   ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))    ⇒   ⊢ (𝑊 ∈ (𝐽 × ℕ0) → (𝐹‘𝑊) = ((2↑(2nd ‘𝑊)) · (1st ‘𝑊)))
Theorem	eulerpartlemsv1 31607*	Lemma for eulerpart 31633. Value of the sum of a partition 𝐴. (Contributed by Thierry Arnoux, 26-Aug-2018.)
⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑆 = (𝑓 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) ↦ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘))    ⇒   ⊢ (𝐴 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) → (𝑆‘𝐴) = Σ𝑘 ∈ ℕ ((𝐴‘𝑘) · 𝑘))
Theorem	eulerpartlemelr 31608*	Lemma for eulerpart 31633. (Contributed by Thierry Arnoux, 8-Aug-2018.)
⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑆 = (𝑓 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) ↦ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘))    ⇒   ⊢ (𝐴 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) → (𝐴:ℕ⟶ℕ0 ∧ (◡𝐴 “ ℕ) ∈ Fin))
Theorem	eulerpartlemsv2 31609*	Lemma for eulerpart 31633. Value of the sum of a finite partition 𝐴 (Contributed by Thierry Arnoux, 19-Aug-2018.)
⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑆 = (𝑓 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) ↦ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘))    ⇒   ⊢ (𝐴 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) → (𝑆‘𝐴) = Σ𝑘 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑘) · 𝑘))
Theorem	eulerpartlemsf 31610*	Lemma for eulerpart 31633. (Contributed by Thierry Arnoux, 8-Aug-2018.)
⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑆 = (𝑓 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) ↦ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘))    ⇒   ⊢ 𝑆:((ℕ0 ↑m ℕ) ∩ 𝑅)⟶ℕ0
Theorem	eulerpartlems 31611*	Lemma for eulerpart 31633. (Contributed by Thierry Arnoux, 6-Aug-2018.) (Revised by Thierry Arnoux, 1-Sep-2019.)
⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑆 = (𝑓 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) ↦ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘))    ⇒   ⊢ ((𝐴 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) ∧ 𝑡 ∈ (ℤ≥‘((𝑆‘𝐴) + 1))) → (𝐴‘𝑡) = 0)
Theorem	eulerpartlemsv3 31612*	Lemma for eulerpart 31633. Value of the sum of a finite partition 𝐴 (Contributed by Thierry Arnoux, 19-Aug-2018.)
⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑆 = (𝑓 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) ↦ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘))    ⇒   ⊢ (𝐴 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) → (𝑆‘𝐴) = Σ𝑘 ∈ (1...(𝑆‘𝐴))((𝐴‘𝑘) · 𝑘))
Theorem	eulerpartlemgc 31613*	Lemma for eulerpart 31633. (Contributed by Thierry Arnoux, 9-Aug-2018.)
⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑆 = (𝑓 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) ↦ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘))    ⇒   ⊢ ((𝐴 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) ∧ (𝑡 ∈ ℕ ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) → ((2↑𝑛) · 𝑡) ≤ (𝑆‘𝐴))
Theorem	eulerpartleme 31614*	Lemma for eulerpart 31633. (Contributed by Mario Carneiro, 26-Jan-2015.)
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)}    ⇒   ⊢ (𝐴 ∈ 𝑃 ↔ (𝐴:ℕ⟶ℕ0 ∧ (◡𝐴 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝐴‘𝑘) · 𝑘) = 𝑁))
Theorem	eulerpartlemv 31615*	Lemma for eulerpart 31633. (Contributed by Thierry Arnoux, 19-Aug-2018.)
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)}    ⇒   ⊢ (𝐴 ∈ 𝑃 ↔ (𝐴:ℕ⟶ℕ0 ∧ (◡𝐴 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑘) · 𝑘) = 𝑁))
Theorem	eulerpartlemo 31616*	Lemma for eulerpart 31633: 𝑂 is the set of odd partitions of 𝑁. (Contributed by Thierry Arnoux, 10-Aug-2017.)
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)}    &   ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛}    &   ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1}    ⇒   ⊢ (𝐴 ∈ 𝑂 ↔ (𝐴 ∈ 𝑃 ∧ ∀𝑛 ∈ (◡𝐴 “ ℕ) ¬ 2 ∥ 𝑛))
Theorem	eulerpartlemd 31617*	Lemma for eulerpart 31633: 𝐷 is the set of distinct part. of 𝑁. (Contributed by Thierry Arnoux, 11-Aug-2017.)
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)}    &   ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛}    &   ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1}    ⇒   ⊢ (𝐴 ∈ 𝐷 ↔ (𝐴 ∈ 𝑃 ∧ (𝐴 “ ℕ) ⊆ {0, 1}))
Theorem	eulerpartlem1 31618*	Lemma for eulerpart 31633. (Contributed by Thierry Arnoux, 27-Aug-2017.) (Revised by Thierry Arnoux, 1-Sep-2019.)
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)}    &   ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛}    &   ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1}    &   ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}    &   ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))    &   ⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}    &   ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))})    ⇒   ⊢ 𝑀:𝐻–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)
Theorem	eulerpartlemb 31619*	Lemma for eulerpart 31633. The set of all partitions of 𝑁 is finite. (Contributed by Mario Carneiro, 26-Jan-2015.)
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)}    &   ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛}    &   ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1}    &   ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}    &   ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))    &   ⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}    &   ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))})    ⇒   ⊢ 𝑃 ∈ Fin
Theorem	eulerpartlemt0 31620*	Lemma for eulerpart 31633. (Contributed by Thierry Arnoux, 19-Sep-2017.)
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)}    &   ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛}    &   ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1}    &   ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}    &   ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))    &   ⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}    &   ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))})    &   ⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑇 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽}    ⇒   ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) ↔ (𝐴 ∈ (ℕ0 ↑m ℕ) ∧ (◡𝐴 “ ℕ) ∈ Fin ∧ (◡𝐴 “ ℕ) ⊆ 𝐽))
Theorem	eulerpartlemf 31621*	Lemma for eulerpart 31633: Odd partitions are zero for even numbers. (Contributed by Thierry Arnoux, 9-Sep-2017.)
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)}    &   ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛}    &   ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1}    &   ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}    &   ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))    &   ⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}    &   ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))})    &   ⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑇 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽}    ⇒   ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ (ℕ ∖ 𝐽)) → (𝐴‘𝑡) = 0)
Theorem	eulerpartlemt 31622*	Lemma for eulerpart 31633. (Contributed by Thierry Arnoux, 19-Sep-2017.)
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)}    &   ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛}    &   ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1}    &   ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}    &   ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))    &   ⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}    &   ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))})    &   ⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑇 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽}    ⇒   ⊢ ((ℕ0 ↑m 𝐽) ∩ 𝑅) = ran (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽))
Theorem	eulerpartgbij 31623*	Lemma for eulerpart 31633: The 𝐺 function is a bijection. (Contributed by Thierry Arnoux, 27-Aug-2017.) (Revised by Thierry Arnoux, 1-Sep-2019.)
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)}    &   ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛}    &   ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1}    &   ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}    &   ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))    &   ⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}    &   ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))})    &   ⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑇 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽}    &   ⊢ 𝐺 = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))    ⇒   ⊢ 𝐺:(𝑇 ∩ 𝑅)–1-1-onto→(({0, 1} ↑m ℕ) ∩ 𝑅)
Theorem	eulerpartlemgv 31624*	Lemma for eulerpart 31633: value of the function 𝐺. (Contributed by Thierry Arnoux, 13-Nov-2017.)
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)}    &   ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛}    &   ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1}    &   ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}    &   ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))    &   ⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}    &   ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))})    &   ⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑇 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽}    &   ⊢ 𝐺 = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))    ⇒   ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝐺‘𝐴) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽))))))
Theorem	eulerpartlemr 31625*	Lemma for eulerpart 31633. (Contributed by Thierry Arnoux, 13-Nov-2017.)
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)}    &   ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛}    &   ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1}    &   ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}    &   ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))    &   ⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}    &   ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))})    &   ⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑇 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽}    &   ⊢ 𝐺 = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))    ⇒   ⊢ 𝑂 = ((𝑇 ∩ 𝑅) ∩ 𝑃)
Theorem	eulerpartlemmf 31626*	Lemma for eulerpart 31633. (Contributed by Thierry Arnoux, 30-Aug-2018.) (Revised by Thierry Arnoux, 1-Sep-2019.)
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)}    &   ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛}    &   ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1}    &   ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}    &   ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))    &   ⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}    &   ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))})    &   ⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑇 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽}    &   ⊢ 𝐺 = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))    ⇒   ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (bits ∘ (𝐴 ↾ 𝐽)) ∈ 𝐻)
Theorem	eulerpartlemgvv 31627*	Lemma for eulerpart 31633: value of the function 𝐺 evaluated. (Contributed by Thierry Arnoux, 10-Aug-2018.)
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)}    &   ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛}    &   ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1}    &   ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}    &   ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))    &   ⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}    &   ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))})    &   ⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑇 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽}    &   ⊢ 𝐺 = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))    ⇒   ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) → ((𝐺‘𝐴)‘𝐵) = if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵, 1, 0))
Theorem	eulerpartlemgu 31628*	Lemma for eulerpart 31633: Rewriting the 𝑈 set for an odd partition Note that interestingly, this proof reuses marypha2lem2 8892. (Contributed by Thierry Arnoux, 10-Aug-2018.)
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)}    &   ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛}    &   ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1}    &   ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}    &   ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))    &   ⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}    &   ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))})    &   ⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑇 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽}    &   ⊢ 𝐺 = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))    &   ⊢ 𝑈 = ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))    ⇒   ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → 𝑈 = {⟨𝑡, 𝑛⟩ ∣ (𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽) ∧ 𝑛 ∈ ((bits ∘ 𝐴)‘𝑡))})
Theorem	eulerpartlemgh 31629*	Lemma for eulerpart 31633: The 𝐹 function is a bijection on the 𝑈 subsets. (Contributed by Thierry Arnoux, 15-Aug-2018.)
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)}    &   ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛}    &   ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1}    &   ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}    &   ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))    &   ⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}    &   ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))})    &   ⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑇 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽}    &   ⊢ 𝐺 = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))    &   ⊢ 𝑈 = ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))    ⇒   ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝐹 ↾ 𝑈):𝑈–1-1-onto→{𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})
Theorem	eulerpartlemgf 31630*	Lemma for eulerpart 31633: Images under 𝐺 have finite support. (Contributed by Thierry Arnoux, 29-Aug-2018.)
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)}    &   ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛}    &   ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1}    &   ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}    &   ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))    &   ⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}    &   ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))})    &   ⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑇 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽}    &   ⊢ 𝐺 = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))    ⇒   ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (◡(𝐺‘𝐴) “ ℕ) ∈ Fin)
Theorem	eulerpartlemgs2 31631*	Lemma for eulerpart 31633: The 𝐺 function also preserves partition sums. (Contributed by Thierry Arnoux, 10-Sep-2017.)
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)}    &   ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛}    &   ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1}    &   ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}    &   ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))    &   ⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}    &   ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))})    &   ⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑇 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽}    &   ⊢ 𝐺 = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))    &   ⊢ 𝑆 = (𝑓 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) ↦ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘))    ⇒   ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑆‘(𝐺‘𝐴)) = (𝑆‘𝐴))
Theorem	eulerpartlemn 31632*	Lemma for eulerpart 31633. (Contributed by Thierry Arnoux, 30-Aug-2018.)
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)}    &   ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛}    &   ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1}    &   ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}    &   ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))    &   ⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}    &   ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))})    &   ⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑇 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽}    &   ⊢ 𝐺 = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))    &   ⊢ 𝑆 = (𝑓 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) ↦ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘))    ⇒   ⊢ (𝐺 ↾ 𝑂):𝑂–1-1-onto→𝐷
Theorem	eulerpart 31633*	Euler's theorem on partitions, also known as a special case of Glaisher's theorem. Let 𝑃 be the set of all partitions of 𝑁, represented as multisets of positive integers, which is to say functions from ℕ to ℕ0 where the value of the function represents the number of repetitions of an individual element, and the sum of all the elements with repetition equals 𝑁. Then the set 𝑂 of all partitions that only consist of odd numbers and the set 𝐷 of all partitions which have no repeated elements have the same cardinality. This is Metamath 100 proof #45. (Contributed by Thierry Arnoux, 14-Aug-2018.) (Revised by Thierry Arnoux, 1-Sep-2019.)
⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)}    &   ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛}    &   ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1}    ⇒   ⊢ (♯‘𝑂) = (♯‘𝐷)
20.3.20  Sequences defined by strong recursion
Syntax	csseq 31634	Sequences defined by strong recursion.
class seqstr
Definition	df-sseq 31635*	Define a builder for sequences by strong recursion, i.e., by computing the value of the n-th element of the sequence from all preceding elements and not just the previous one. (Contributed by Thierry Arnoux, 21-Apr-2019.)
⊢ seqstr = (𝑚 ∈ V, 𝑓 ∈ V ↦ (𝑚 ∪ (lastS ∘ seq(♯‘𝑚)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝑓‘𝑥)”⟩)), (ℕ0 × {(𝑚 ++ ⟨“(𝑓‘𝑚)”⟩)})))))
Theorem	subiwrd 31636	Lemma for sseqp1 31646. (Contributed by Thierry Arnoux, 25-Apr-2019.)
⊢ (𝜑 → 𝑆 ∈ V)    &   ⊢ (𝜑 → 𝐹:ℕ0⟶𝑆)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐹 ↾ (0..^𝑁)) ∈ Word 𝑆)
Theorem	subiwrdlen 31637	Length of a subword of an infinite word. (Contributed by Thierry Arnoux, 25-Apr-2019.)
⊢ (𝜑 → 𝑆 ∈ V)    &   ⊢ (𝜑 → 𝐹:ℕ0⟶𝑆)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (♯‘(𝐹 ↾ (0..^𝑁))) = 𝑁)
Theorem	iwrdsplit 31638	Lemma for sseqp1 31646. (Contributed by Thierry Arnoux, 25-Apr-2019.) (Proof shortened by AV, 14-Oct-2022.)
⊢ (𝜑 → 𝑆 ∈ V)    &   ⊢ (𝜑 → 𝐹:ℕ0⟶𝑆)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐹 ↾ (0..^(𝑁 + 1))) = ((𝐹 ↾ (0..^𝑁)) ++ ⟨“(𝐹‘𝑁)”⟩))
Theorem	sseqval 31639*	Value of the strong sequence builder function. The set 𝑊 represents here the words of length greater than or equal to the lenght of the initial sequence 𝑀. (Contributed by Thierry Arnoux, 21-Apr-2019.)
⊢ (𝜑 → 𝑆 ∈ V)    &   ⊢ (𝜑 → 𝑀 ∈ Word 𝑆)    &   ⊢ 𝑊 = (Word 𝑆 ∩ (◡♯ “ (ℤ≥‘(♯‘𝑀))))    &   ⊢ (𝜑 → 𝐹:𝑊⟶𝑆)    ⇒   ⊢ (𝜑 → (𝑀seqstr𝐹) = (𝑀 ∪ (lastS ∘ seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ0 × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)})))))
Theorem	sseqfv1 31640	Value of the strong sequence builder function at one of its initial values. (Contributed by Thierry Arnoux, 21-Apr-2019.)
⊢ (𝜑 → 𝑆 ∈ V)    &   ⊢ (𝜑 → 𝑀 ∈ Word 𝑆)    &   ⊢ 𝑊 = (Word 𝑆 ∩ (◡♯ “ (ℤ≥‘(♯‘𝑀))))    &   ⊢ (𝜑 → 𝐹:𝑊⟶𝑆)    &   ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝑀)))    ⇒   ⊢ (𝜑 → ((𝑀seqstr𝐹)‘𝑁) = (𝑀‘𝑁))
Theorem	sseqfn 31641	A strong recursive sequence is a function over the nonnegative integers. (Contributed by Thierry Arnoux, 23-Apr-2019.)
⊢ (𝜑 → 𝑆 ∈ V)    &   ⊢ (𝜑 → 𝑀 ∈ Word 𝑆)    &   ⊢ 𝑊 = (Word 𝑆 ∩ (◡♯ “ (ℤ≥‘(♯‘𝑀))))    &   ⊢ (𝜑 → 𝐹:𝑊⟶𝑆)    ⇒   ⊢ (𝜑 → (𝑀seqstr𝐹) Fn ℕ0)
Theorem	sseqmw 31642	Lemma for sseqf 31643 amd sseqp1 31646. (Contributed by Thierry Arnoux, 25-Apr-2019.)
⊢ (𝜑 → 𝑆 ∈ V)    &   ⊢ (𝜑 → 𝑀 ∈ Word 𝑆)    &   ⊢ 𝑊 = (Word 𝑆 ∩ (◡♯ “ (ℤ≥‘(♯‘𝑀))))    &   ⊢ (𝜑 → 𝐹:𝑊⟶𝑆)    ⇒   ⊢ (𝜑 → 𝑀 ∈ 𝑊)
Theorem	sseqf 31643	A strong recursive sequence is a function over the nonnegative integers. (Contributed by Thierry Arnoux, 23-Apr-2019.) (Proof shortened by AV, 7-Mar-2022.)
⊢ (𝜑 → 𝑆 ∈ V)    &   ⊢ (𝜑 → 𝑀 ∈ Word 𝑆)    &   ⊢ 𝑊 = (Word 𝑆 ∩ (◡♯ “ (ℤ≥‘(♯‘𝑀))))    &   ⊢ (𝜑 → 𝐹:𝑊⟶𝑆)    ⇒   ⊢ (𝜑 → (𝑀seqstr𝐹):ℕ0⟶𝑆)
Theorem	sseqfres 31644	The first elements in the strong recursive sequence are the sequence initializer. (Contributed by Thierry Arnoux, 23-Apr-2019.)
⊢ (𝜑 → 𝑆 ∈ V)    &   ⊢ (𝜑 → 𝑀 ∈ Word 𝑆)    &   ⊢ 𝑊 = (Word 𝑆 ∩ (◡♯ “ (ℤ≥‘(♯‘𝑀))))    &   ⊢ (𝜑 → 𝐹:𝑊⟶𝑆)    ⇒   ⊢ (𝜑 → ((𝑀seqstr𝐹) ↾ (0..^(♯‘𝑀))) = 𝑀)
Theorem	sseqfv2 31645*	Value of the strong sequence builder function. (Contributed by Thierry Arnoux, 21-Apr-2019.)
⊢ (𝜑 → 𝑆 ∈ V)    &   ⊢ (𝜑 → 𝑀 ∈ Word 𝑆)    &   ⊢ 𝑊 = (Word 𝑆 ∩ (◡♯ “ (ℤ≥‘(♯‘𝑀))))    &   ⊢ (𝜑 → 𝐹:𝑊⟶𝑆)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(♯‘𝑀)))    ⇒   ⊢ (𝜑 → ((𝑀seqstr𝐹)‘𝑁) = (lastS‘(seq(♯‘𝑀)((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ++ ⟨“(𝐹‘𝑥)”⟩)), (ℕ0 × {(𝑀 ++ ⟨“(𝐹‘𝑀)”⟩)}))‘𝑁)))
Theorem	sseqp1 31646	Value of the strong sequence builder function at a successor. (Contributed by Thierry Arnoux, 24-Apr-2019.)
⊢ (𝜑 → 𝑆 ∈ V)    &   ⊢ (𝜑 → 𝑀 ∈ Word 𝑆)    &   ⊢ 𝑊 = (Word 𝑆 ∩ (◡♯ “ (ℤ≥‘(♯‘𝑀))))    &   ⊢ (𝜑 → 𝐹:𝑊⟶𝑆)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(♯‘𝑀)))    ⇒   ⊢ (𝜑 → ((𝑀seqstr𝐹)‘𝑁) = (𝐹‘((𝑀seqstr𝐹) ↾ (0..^𝑁))))
20.3.21  Fibonacci Numbers
Syntax	cfib 31647	The Fibonacci sequence.
class Fibci
Definition	df-fib 31648	Define the Fibonacci sequence, where that each element is the sum of the two preceding ones, starting from 0 and 1. (Contributed by Thierry Arnoux, 25-Apr-2019.)
⊢ Fibci = (⟨“01”⟩seqstr(𝑤 ∈ (Word ℕ0 ∩ (◡♯ “ (ℤ≥‘2))) ↦ ((𝑤‘((♯‘𝑤) − 2)) + (𝑤‘((♯‘𝑤) − 1)))))
Theorem	fiblem 31649	Lemma for fib0 31650, fib1 31651 and fibp1 31652. (Contributed by Thierry Arnoux, 25-Apr-2019.)
⊢ (𝑤 ∈ (Word ℕ0 ∩ (◡♯ “ (ℤ≥‘2))) ↦ ((𝑤‘((♯‘𝑤) − 2)) + (𝑤‘((♯‘𝑤) − 1)))):(Word ℕ0 ∩ (◡♯ “ (ℤ≥‘(♯‘⟨“01”⟩))))⟶ℕ0
Theorem	fib0 31650	Value of the Fibonacci sequence at index 0. (Contributed by Thierry Arnoux, 25-Apr-2019.)
⊢ (Fibci‘0) = 0
Theorem	fib1 31651	Value of the Fibonacci sequence at index 1. (Contributed by Thierry Arnoux, 25-Apr-2019.)
⊢ (Fibci‘1) = 1
Theorem	fibp1 31652	Value of the Fibonacci sequence at higher indices. (Contributed by Thierry Arnoux, 25-Apr-2019.)
⊢ (𝑁 ∈ ℕ → (Fibci‘(𝑁 + 1)) = ((Fibci‘(𝑁 − 1)) + (Fibci‘𝑁)))
Theorem	fib2 31653	Value of the Fibonacci sequence at index 2. (Contributed by Thierry Arnoux, 25-Apr-2019.)
⊢ (Fibci‘2) = 1
Theorem	fib3 31654	Value of the Fibonacci sequence at index 3. (Contributed by Thierry Arnoux, 25-Apr-2019.)
⊢ (Fibci‘3) = 2
Theorem	fib4 31655	Value of the Fibonacci sequence at index 4. (Contributed by Thierry Arnoux, 25-Apr-2019.)
⊢ (Fibci‘4) = 3
Theorem	fib5 31656	Value of the Fibonacci sequence at index 5. (Contributed by Thierry Arnoux, 25-Apr-2019.)
⊢ (Fibci‘5) = 5
Theorem	fib6 31657	Value of the Fibonacci sequence at index 6. (Contributed by Thierry Arnoux, 25-Apr-2019.)
⊢ (Fibci‘6) = 8
20.3.22  Probability
20.3.22.1  Probability Theory
Syntax	cprb 31658	Extend class notation to include the class of probability measures.
class Prob
Definition	df-prob 31659	Define the class of probability measures as the set of measures with total measure 1. (Contributed by Thierry Arnoux, 14-Sep-2016.)
⊢ Prob = {𝑝 ∈ ∪ ran measures ∣ (𝑝‘∪ dom 𝑝) = 1}
Theorem	elprob 31660	The property of being a probability measure. (Contributed by Thierry Arnoux, 8-Dec-2016.)
⊢ (𝑃 ∈ Prob ↔ (𝑃 ∈ ∪ ran measures ∧ (𝑃‘∪ dom 𝑃) = 1))
Theorem	domprobmeas 31661	A probability measure is a measure on its domain. (Contributed by Thierry Arnoux, 23-Dec-2016.)
⊢ (𝑃 ∈ Prob → 𝑃 ∈ (measures‘dom 𝑃))
Theorem	domprobsiga 31662	The domain of a probability measure is a sigma-algebra. (Contributed by Thierry Arnoux, 23-Dec-2016.)
⊢ (𝑃 ∈ Prob → dom 𝑃 ∈ ∪ ran sigAlgebra)
Theorem	probtot 31663	The probability of the universe set is 1. Second axiom of Kolmogorov. (Contributed by Thierry Arnoux, 8-Dec-2016.)
⊢ (𝑃 ∈ Prob → (𝑃‘∪ dom 𝑃) = 1)
Theorem	prob01 31664	A probability is an element of [ 0 , 1 ]. First axiom of Kolmogorov. (Contributed by Thierry Arnoux, 25-Dec-2016.)
⊢ ((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃) → (𝑃‘𝐴) ∈ (0[,]1))
Theorem	probnul 31665	The probability of the empty event set is 0. (Contributed by Thierry Arnoux, 25-Dec-2016.)
⊢ (𝑃 ∈ Prob → (𝑃‘∅) = 0)
Theorem	unveldomd 31666	The universe is an element of the domain of the probability, the universe (entire probability space) being ∪ dom 𝑃 in our construction. (Contributed by Thierry Arnoux, 22-Jan-2017.)
⊢ (𝜑 → 𝑃 ∈ Prob)    ⇒   ⊢ (𝜑 → ∪ dom 𝑃 ∈ dom 𝑃)
Theorem	unveldom 31667	The universe is an element of the domain of the probability, the universe (entire probability space) being ∪ dom 𝑃 in our construction. (Contributed by Thierry Arnoux, 22-Jan-2017.)
⊢ (𝑃 ∈ Prob → ∪ dom 𝑃 ∈ dom 𝑃)
Theorem	nuleldmp 31668	The empty set is an element of the domain of the probability. (Contributed by Thierry Arnoux, 22-Jan-2017.)
⊢ (𝑃 ∈ Prob → ∅ ∈ dom 𝑃)
Theorem	probcun 31669*	The probability of the union of a countable disjoint set of events is the sum of their probabilities. (Third axiom of Kolmogorov) Here, the Σ construct cannot be used as it can handle infinite indexing set only if they are subsets of ℤ, which is not the case here. (Contributed by Thierry Arnoux, 25-Dec-2016.)
⊢ ((𝑃 ∈ Prob ∧ 𝐴 ∈ 𝒫 dom 𝑃 ∧ (𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝑥)) → (𝑃‘∪ 𝐴) = Σ*𝑥 ∈ 𝐴(𝑃‘𝑥))
Theorem	probun 31670	The probability of the union two incompatible events is the sum of their probabilities. (Contributed by Thierry Arnoux, 25-Dec-2016.)
⊢ ((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃) → ((𝐴 ∩ 𝐵) = ∅ → (𝑃‘(𝐴 ∪ 𝐵)) = ((𝑃‘𝐴) + (𝑃‘𝐵))))
Theorem	probdif 31671	The probability of the difference of two event sets. (Contributed by Thierry Arnoux, 12-Dec-2016.)
⊢ ((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃) → (𝑃‘(𝐴 ∖ 𝐵)) = ((𝑃‘𝐴) − (𝑃‘(𝐴 ∩ 𝐵))))
Theorem	probinc 31672	A probability law is increasing with regard to event set inclusion. (Contributed by Thierry Arnoux, 10-Feb-2017.)
⊢ (((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃) ∧ 𝐴 ⊆ 𝐵) → (𝑃‘𝐴) ≤ (𝑃‘𝐵))
Theorem	probdsb 31673	The probability of the complement of a set. That is, the probability that the event 𝐴 does not occur. (Contributed by Thierry Arnoux, 15-Dec-2016.)
⊢ ((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃) → (𝑃‘(∪ dom 𝑃 ∖ 𝐴)) = (1 − (𝑃‘𝐴)))
Theorem	probmeasd 31674	A probability measure is a measure. (Contributed by Thierry Arnoux, 2-Feb-2017.)
⊢ (𝜑 → 𝑃 ∈ Prob)    ⇒   ⊢ (𝜑 → 𝑃 ∈ ∪ ran measures)
Theorem	probvalrnd 31675	The value of a probability is a real number. (Contributed by Thierry Arnoux, 2-Feb-2017.)
⊢ (𝜑 → 𝑃 ∈ Prob)    &   ⊢ (𝜑 → 𝐴 ∈ dom 𝑃)    ⇒   ⊢ (𝜑 → (𝑃‘𝐴) ∈ ℝ)
Theorem	probtotrnd 31676	The probability of the universe set is finite. (Contributed by Thierry Arnoux, 2-Feb-2017.)
⊢ (𝜑 → 𝑃 ∈ Prob)    ⇒   ⊢ (𝜑 → (𝑃‘∪ dom 𝑃) ∈ ℝ)
Theorem	totprobd 31677*	Law of total probability, deduction form. (Contributed by Thierry Arnoux, 25-Dec-2016.)
⊢ (𝜑 → 𝑃 ∈ Prob)    &   ⊢ (𝜑 → 𝐴 ∈ dom 𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝒫 dom 𝑃)    &   ⊢ (𝜑 → ∪ 𝐵 = ∪ dom 𝑃)    &   ⊢ (𝜑 → 𝐵 ≼ ω)    &   ⊢ (𝜑 → Disj 𝑏 ∈ 𝐵 𝑏)    ⇒   ⊢ (𝜑 → (𝑃‘𝐴) = Σ*𝑏 ∈ 𝐵(𝑃‘(𝑏 ∩ 𝐴)))
Theorem	totprob 31678*	Law of total probability. (Contributed by Thierry Arnoux, 25-Dec-2016.)
⊢ ((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ (∪ 𝐵 = ∪ dom 𝑃 ∧ 𝐵 ∈ 𝒫 dom 𝑃 ∧ (𝐵 ≼ ω ∧ Disj 𝑏 ∈ 𝐵 𝑏))) → (𝑃‘𝐴) = Σ*𝑏 ∈ 𝐵(𝑃‘(𝑏 ∩ 𝐴)))
Theorem	probfinmeasb 31679	Build a probability measure from a finite measure. (Contributed by Thierry Arnoux, 31-Jan-2017.)
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ (𝑀‘∪ 𝑆) ∈ ℝ+) → (𝑀 ∘f/c /𝑒 (𝑀‘∪ 𝑆)) ∈ Prob)
Theorem	probfinmeasbALTV 31680*	Alternate version of probfinmeasb 31679. (Contributed by Thierry Arnoux, 17-Dec-2016.) (New usage is discouraged.)
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ (𝑀‘∪ 𝑆) ∈ ℝ+) → (𝑥 ∈ 𝑆 ↦ ((𝑀‘𝑥) /𝑒 (𝑀‘∪ 𝑆))) ∈ Prob)
Theorem	probmeasb 31681*	Build a probability from a measure and a set with finite measure. (Contributed by Thierry Arnoux, 25-Dec-2016.)
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) → (𝑥 ∈ 𝑆 ↦ ((𝑀‘(𝑥 ∩ 𝐴)) / (𝑀‘𝐴))) ∈ Prob)
20.3.22.2  Conditional Probabilities
Syntax	ccprob 31682	Extends class notation with the conditional probability builder.
class cprob
Definition	df-cndprob 31683*	Define the conditional probability. (Contributed by Thierry Arnoux, 14-Sep-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.)
⊢ cprob = (𝑝 ∈ Prob ↦ (𝑎 ∈ dom 𝑝, 𝑏 ∈ dom 𝑝 ↦ ((𝑝‘(𝑎 ∩ 𝑏)) / (𝑝‘𝑏))))
Theorem	cndprobval 31684	The value of the conditional probability , i.e. the probability for the event 𝐴, given 𝐵, under the probability law 𝑃. (Contributed by Thierry Arnoux, 21-Jan-2017.)
⊢ ((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃) → ((cprob‘𝑃)‘⟨𝐴, 𝐵⟩) = ((𝑃‘(𝐴 ∩ 𝐵)) / (𝑃‘𝐵)))
Theorem	cndprobin 31685	An identity linking conditional probability and intersection. (Contributed by Thierry Arnoux, 13-Dec-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.)
⊢ (((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃) ∧ (𝑃‘𝐵) ≠ 0) → (((cprob‘𝑃)‘⟨𝐴, 𝐵⟩) · (𝑃‘𝐵)) = (𝑃‘(𝐴 ∩ 𝐵)))
Theorem	cndprob01 31686	The conditional probability has values in [0, 1]. (Contributed by Thierry Arnoux, 13-Dec-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.)
⊢ (((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃) ∧ (𝑃‘𝐵) ≠ 0) → ((cprob‘𝑃)‘⟨𝐴, 𝐵⟩) ∈ (0[,]1))
Theorem	cndprobtot 31687	The conditional probability given a certain event is one. (Contributed by Thierry Arnoux, 20-Dec-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.)
⊢ ((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ (𝑃‘𝐴) ≠ 0) → ((cprob‘𝑃)‘⟨∪ dom 𝑃, 𝐴⟩) = 1)
Theorem	cndprobnul 31688	The conditional probability given empty event is zero. (Contributed by Thierry Arnoux, 20-Dec-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.)
⊢ ((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ (𝑃‘𝐴) ≠ 0) → ((cprob‘𝑃)‘⟨∅, 𝐴⟩) = 0)
Theorem	cndprobprob 31689*	The conditional probability defines a probability law. (Contributed by Thierry Arnoux, 23-Dec-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.)
⊢ ((𝑃 ∈ Prob ∧ 𝐵 ∈ dom 𝑃 ∧ (𝑃‘𝐵) ≠ 0) → (𝑎 ∈ dom 𝑃 ↦ ((cprob‘𝑃)‘⟨𝑎, 𝐵⟩)) ∈ Prob)
Theorem	bayesth 31690	Bayes Theorem. (Contributed by Thierry Arnoux, 20-Dec-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.)
⊢ (((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃) ∧ (𝑃‘𝐴) ≠ 0 ∧ (𝑃‘𝐵) ≠ 0) → ((cprob‘𝑃)‘⟨𝐴, 𝐵⟩) = ((((cprob‘𝑃)‘⟨𝐵, 𝐴⟩) · (𝑃‘𝐴)) / (𝑃‘𝐵)))
20.3.22.3  Real-valued Random Variables
Syntax	crrv 31691	Extend class notation with the class of real-valued random variables.
class rRndVar
Definition	df-rrv 31692	In its generic definition, a random variable is a measurable function from a probability space to a Borel set. Here, we specifically target real-valued random variables, i.e. measurable function from a probability space to the Borel sigma-algebra on the set of real numbers. (Contributed by Thierry Arnoux, 20-Sep-2016.) (Revised by Thierry Arnoux, 25-Jan-2017.)
⊢ rRndVar = (𝑝 ∈ Prob ↦ (dom 𝑝MblFnM𝔅ℝ))
Theorem	rrvmbfm 31693	A real-valued random variable is a measurable function from its sample space to the Borel sigma-algebra. (Contributed by Thierry Arnoux, 25-Jan-2017.)
⊢ (𝜑 → 𝑃 ∈ Prob)    ⇒   ⊢ (𝜑 → (𝑋 ∈ (rRndVar‘𝑃) ↔ 𝑋 ∈ (dom 𝑃MblFnM𝔅ℝ)))
Theorem	isrrvv 31694*	Elementhood to the set of real-valued random variables with respect to the probability 𝑃. (Contributed by Thierry Arnoux, 25-Jan-2017.)
⊢ (𝜑 → 𝑃 ∈ Prob)    ⇒   ⊢ (𝜑 → (𝑋 ∈ (rRndVar‘𝑃) ↔ (𝑋:∪ dom 𝑃⟶ℝ ∧ ∀𝑦 ∈ 𝔅ℝ (◡𝑋 “ 𝑦) ∈ dom 𝑃)))
Theorem	rrvvf 31695	A real-valued random variable is a function. (Contributed by Thierry Arnoux, 25-Jan-2017.)
⊢ (𝜑 → 𝑃 ∈ Prob)    &   ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃))    ⇒   ⊢ (𝜑 → 𝑋:∪ dom 𝑃⟶ℝ)
Theorem	rrvfn 31696	A real-valued random variable is a function over the universe. (Contributed by Thierry Arnoux, 25-Jan-2017.)
⊢ (𝜑 → 𝑃 ∈ Prob)    &   ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃))    ⇒   ⊢ (𝜑 → 𝑋 Fn ∪ dom 𝑃)
Theorem	rrvdm 31697	The domain of a random variable is the universe. (Contributed by Thierry Arnoux, 25-Jan-2017.)
⊢ (𝜑 → 𝑃 ∈ Prob)    &   ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃))    ⇒   ⊢ (𝜑 → dom 𝑋 = ∪ dom 𝑃)
Theorem	rrvrnss 31698	The range of a random variable as a subset of ℝ. (Contributed by Thierry Arnoux, 6-Feb-2017.)
⊢ (𝜑 → 𝑃 ∈ Prob)    &   ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃))    ⇒   ⊢ (𝜑 → ran 𝑋 ⊆ ℝ)
Theorem	rrvf2 31699	A real-valued random variable is a function. (Contributed by Thierry Arnoux, 25-Jan-2017.)
⊢ (𝜑 → 𝑃 ∈ Prob)    &   ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃))    ⇒   ⊢ (𝜑 → 𝑋:dom 𝑋⟶ℝ)
Theorem	rrvdmss 31700	The domain of a random variable. This is useful to shorten proofs. (Contributed by Thierry Arnoux, 25-Jan-2017.)
⊢ (𝜑 → 𝑃 ∈ Prob)    &   ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃))    ⇒   ⊢ (𝜑 → ∪ dom 𝑃 ⊆ dom 𝑋)