P. 383 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 38201-38300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	7rexfrabdioph 38201*	Diophantine set builder for existential quantifier, explicit substitution, seven variables. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by Stefan O'Rear, 6-May-2015.)
⊢ 𝑀 = (𝑁 + 1)    &   ⊢ 𝐿 = (𝑀 + 1)    &   ⊢ 𝐾 = (𝐿 + 1)    &   ⊢ 𝐽 = (𝐾 + 1)    &   ⊢ 𝐼 = (𝐽 + 1)    &   ⊢ 𝐻 = (𝐼 + 1)    &   ⊢ 𝐺 = (𝐻 + 1)    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ {𝑡 ∈ (ℕ0 ↑𝑚 (1...𝐺)) ∣ [(𝑡 ↾ (1...𝑁)) / 𝑢][(𝑡‘𝑀) / 𝑣][(𝑡‘𝐿) / 𝑤][(𝑡‘𝐾) / 𝑥][(𝑡‘𝐽) / 𝑦][(𝑡‘𝐼) / 𝑧][(𝑡‘𝐻) / 𝑝][(𝑡‘𝐺) / 𝑞]𝜑} ∈ (Dioph‘𝐺)) → {𝑢 ∈ (ℕ0 ↑𝑚 (1...𝑁)) ∣ ∃𝑣 ∈ ℕ0 ∃𝑤 ∈ ℕ0 ∃𝑥 ∈ ℕ0 ∃𝑦 ∈ ℕ0 ∃𝑧 ∈ ℕ0 ∃𝑝 ∈ ℕ0 ∃𝑞 ∈ ℕ0 𝜑} ∈ (Dioph‘𝑁))
20.26.16  Diophantine sets 5: Arithmetic sets
Theorem	rabdiophlem1 38202*	Lemma for arithmetic diophantine sets. Convert polynomial-ness of an expression into a constraint suitable for ralimi 3161. (Contributed by Stefan O'Rear, 10-Oct-2014.)
⊢ ((𝑡 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) → ∀𝑡 ∈ (ℕ0 ↑𝑚 (1...𝑁))𝐴 ∈ ℤ)
Theorem	rabdiophlem2 38203*	Lemma for arithmetic diophantine sets. Reuse a polynomial expression under a new quantifier. (Contributed by Stefan O'Rear, 10-Oct-2014.)
⊢ 𝑀 = (𝑁 + 1)    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑢 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) → (𝑡 ∈ (ℤ ↑𝑚 (1...𝑀)) ↦ ⦋(𝑡 ↾ (1...𝑁)) / 𝑢⦌𝐴) ∈ (mzPoly‘(1...𝑀)))
Theorem	elnn0rabdioph 38204*	Diophantine set builder for nonnegativity constraints. The first builder which uses a witness variable internally; an expression is nonnegative if there is a nonnegative integer equal to it. (Contributed by Stefan O'Rear, 11-Oct-2014.)
⊢ ((𝑁 ∈ ℕ0 ∧ (𝑡 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) → {𝑡 ∈ (ℕ0 ↑𝑚 (1...𝑁)) ∣ 𝐴 ∈ ℕ0} ∈ (Dioph‘𝑁))
Theorem	rexzrexnn0 38205*	Rewrite a quantification over integers into a quantification over naturals. (Contributed by Stefan O'Rear, 11-Oct-2014.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = -𝑦 → (𝜑 ↔ 𝜒))    ⇒   ⊢ (∃𝑥 ∈ ℤ 𝜑 ↔ ∃𝑦 ∈ ℕ0 (𝜓 ∨ 𝜒))
Theorem	lerabdioph 38206*	Diophantine set builder for the "less than or equal to" relation. (Contributed by Stefan O'Rear, 11-Oct-2014.)
⊢ ((𝑁 ∈ ℕ0 ∧ (𝑡 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) ∧ (𝑡 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝐵) ∈ (mzPoly‘(1...𝑁))) → {𝑡 ∈ (ℕ0 ↑𝑚 (1...𝑁)) ∣ 𝐴 ≤ 𝐵} ∈ (Dioph‘𝑁))
Theorem	eluzrabdioph 38207*	Diophantine set builder for membership in a fixed upper set of integers. (Contributed by Stefan O'Rear, 11-Oct-2014.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ∧ (𝑡 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) → {𝑡 ∈ (ℕ0 ↑𝑚 (1...𝑁)) ∣ 𝐴 ∈ (ℤ≥‘𝑀)} ∈ (Dioph‘𝑁))
Theorem	elnnrabdioph 38208*	Diophantine set builder for positivity. (Contributed by Stefan O'Rear, 11-Oct-2014.)
⊢ ((𝑁 ∈ ℕ0 ∧ (𝑡 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) → {𝑡 ∈ (ℕ0 ↑𝑚 (1...𝑁)) ∣ 𝐴 ∈ ℕ} ∈ (Dioph‘𝑁))
Theorem	ltrabdioph 38209*	Diophantine set builder for the strict less than relation. (Contributed by Stefan O'Rear, 11-Oct-2014.)
⊢ ((𝑁 ∈ ℕ0 ∧ (𝑡 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) ∧ (𝑡 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝐵) ∈ (mzPoly‘(1...𝑁))) → {𝑡 ∈ (ℕ0 ↑𝑚 (1...𝑁)) ∣ 𝐴 < 𝐵} ∈ (Dioph‘𝑁))
Theorem	nerabdioph 38210*	Diophantine set builder for inequality. This not quite trivial theorem touches on something important; Diophantine sets are not closed under negation, but they contain an important subclass that is, namely the recursive sets. With this theorem and De Morgan's laws, all quantifier-free formulas can be negated. (Contributed by Stefan O'Rear, 11-Oct-2014.)
⊢ ((𝑁 ∈ ℕ0 ∧ (𝑡 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) ∧ (𝑡 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝐵) ∈ (mzPoly‘(1...𝑁))) → {𝑡 ∈ (ℕ0 ↑𝑚 (1...𝑁)) ∣ 𝐴 ≠ 𝐵} ∈ (Dioph‘𝑁))
Theorem	dvdsrabdioph 38211*	Divisibility is a Diophantine relation. (Contributed by Stefan O'Rear, 11-Oct-2014.)
⊢ ((𝑁 ∈ ℕ0 ∧ (𝑡 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) ∧ (𝑡 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝐵) ∈ (mzPoly‘(1...𝑁))) → {𝑡 ∈ (ℕ0 ↑𝑚 (1...𝑁)) ∣ 𝐴 ∥ 𝐵} ∈ (Dioph‘𝑁))
20.26.17  Diophantine sets 6: reusability. renumbering of variables
Theorem	eldioph4b 38212*	Membership in Dioph expressed using a quantified union to add witness variables instead of a restriction to remove them. (Contributed by Stefan O'Rear, 16-Oct-2014.)
⊢ 𝑊 ∈ V    &   ⊢ ¬ 𝑊 ∈ Fin    &   ⊢ (𝑊 ∩ ℕ) = ∅    ⇒   ⊢ (𝑆 ∈ (Dioph‘𝑁) ↔ (𝑁 ∈ ℕ0 ∧ ∃𝑝 ∈ (mzPoly‘(𝑊 ∪ (1...𝑁)))𝑆 = {𝑡 ∈ (ℕ0 ↑𝑚 (1...𝑁)) ∣ ∃𝑤 ∈ (ℕ0 ↑𝑚 𝑊)(𝑝‘(𝑡 ∪ 𝑤)) = 0}))
Theorem	eldioph4i 38213*	Forward-only version of eldioph4b 38212. (Contributed by Stefan O'Rear, 16-Oct-2014.)
⊢ 𝑊 ∈ V    &   ⊢ ¬ 𝑊 ∈ Fin    &   ⊢ (𝑊 ∩ ℕ) = ∅    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑃 ∈ (mzPoly‘(𝑊 ∪ (1...𝑁)))) → {𝑡 ∈ (ℕ0 ↑𝑚 (1...𝑁)) ∣ ∃𝑤 ∈ (ℕ0 ↑𝑚 𝑊)(𝑃‘(𝑡 ∪ 𝑤)) = 0} ∈ (Dioph‘𝑁))
Theorem	diophren 38214*	Change variables in a Diophantine set, using class notation. This allows already proved Diophantine sets to be reused in contexts with more variables. (Contributed by Stefan O'Rear, 16-Oct-2014.) (Revised by Stefan O'Rear, 5-Jun-2015.)
⊢ ((𝑆 ∈ (Dioph‘𝑁) ∧ 𝑀 ∈ ℕ0 ∧ 𝐹:(1...𝑁)⟶(1...𝑀)) → {𝑎 ∈ (ℕ0 ↑𝑚 (1...𝑀)) ∣ (𝑎 ∘ 𝐹) ∈ 𝑆} ∈ (Dioph‘𝑀))
Theorem	rabrenfdioph 38215*	Change variable numbers in a Diophantine class abstraction using explicit substitution. (Contributed by Stefan O'Rear, 17-Oct-2014.)
⊢ ((𝐵 ∈ ℕ0 ∧ 𝐹:(1...𝐴)⟶(1...𝐵) ∧ {𝑎 ∈ (ℕ0 ↑𝑚 (1...𝐴)) ∣ 𝜑} ∈ (Dioph‘𝐴)) → {𝑏 ∈ (ℕ0 ↑𝑚 (1...𝐵)) ∣ [(𝑏 ∘ 𝐹) / 𝑎]𝜑} ∈ (Dioph‘𝐵))
Theorem	rabren3dioph 38216*	Change variable numbers in a 3-variable Diophantine class abstraction. (Contributed by Stefan O'Rear, 17-Oct-2014.)
⊢ (((𝑎‘1) = (𝑏‘𝑋) ∧ (𝑎‘2) = (𝑏‘𝑌) ∧ (𝑎‘3) = (𝑏‘𝑍)) → (𝜑 ↔ 𝜓))    &   ⊢ 𝑋 ∈ (1...𝑁)    &   ⊢ 𝑌 ∈ (1...𝑁)    &   ⊢ 𝑍 ∈ (1...𝑁)    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ {𝑎 ∈ (ℕ0 ↑𝑚 (1...3)) ∣ 𝜑} ∈ (Dioph‘3)) → {𝑏 ∈ (ℕ0 ↑𝑚 (1...𝑁)) ∣ 𝜓} ∈ (Dioph‘𝑁))
20.26.18  Pigeonhole Principle and cardinality helpers
Theorem	fphpd 38217*	Pigeonhole principle expressed with implicit substitution. If the range is smaller than the domain, two inputs must be mapped to the same output. (Contributed by Stefan O'Rear, 19-Oct-2014.) (Revised by Stefan O'Rear, 6-May-2015.)
⊢ (𝜑 → 𝐵 ≺ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐵)    &   ⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 ∧ 𝐶 = 𝐷))
Theorem	fphpdo 38218*	Pigeonhole principle for sets of real numbers with implicit output reordering. (Contributed by Stefan O'Rear, 12-Sep-2014.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ V)    &   ⊢ (𝜑 → 𝐵 ≺ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝐶 ∈ 𝐵)    &   ⊢ (𝑧 = 𝑥 → 𝐶 = 𝐷)    &   ⊢ (𝑧 = 𝑦 → 𝐶 = 𝐸)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 (𝑥 < 𝑦 ∧ 𝐷 = 𝐸))
Theorem	ctbnfien 38219	An infinite subset of a countable set is countable, without using choice. (Contributed by Stefan O'Rear, 19-Oct-2014.) (Revised by Stefan O'Rear, 6-May-2015.)
⊢ (((𝑋 ≈ ω ∧ 𝑌 ≈ ω) ∧ (𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin)) → 𝐴 ≈ 𝑌)
Theorem	fiphp3d 38220*	Infinite pigeonhole principle for partitioning an infinite set between finitely many buckets. (Contributed by Stefan O'Rear, 18-Oct-2014.)
⊢ (𝜑 → 𝐴 ≈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐷 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ∃𝑦 ∈ 𝐵 {𝑥 ∈ 𝐴 ∣ 𝐷 = 𝑦} ≈ ℕ)
20.26.19  A non-closed set of reals is infinite
Theorem	rencldnfilem 38221*	Lemma for rencldnfi 38222. (Contributed by Stefan O'Rear, 18-Oct-2014.)
⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) < 𝑥) → ¬ 𝐴 ∈ Fin)
Theorem	rencldnfi 38222*	A set of real numbers which comes arbitrarily close to some target yet excludes it is infinite. The work is done in rencldnfilem 38221 using infima; this theorem removes the requirement that A be nonempty. (Contributed by Stefan O'Rear, 19-Oct-2014.)
⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ∧ ¬ 𝐵 ∈ 𝐴) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) < 𝑥) → ¬ 𝐴 ∈ Fin)
20.26.20  Lagrange's rational approximation theorem
Theorem	irrapxlem1 38223*	Lemma for irrapx1 38229. Divides the unit interval into 𝐵 half-open sections and using the pigeonhole principle fphpdo 38218 finds two multiples of 𝐴 in the same section mod 1. (Contributed by Stefan O'Rear, 12-Sep-2014.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ) → ∃𝑥 ∈ (0...𝐵)∃𝑦 ∈ (0...𝐵)(𝑥 < 𝑦 ∧ (⌊‘(𝐵 · ((𝐴 · 𝑥) mod 1))) = (⌊‘(𝐵 · ((𝐴 · 𝑦) mod 1)))))
Theorem	irrapxlem2 38224*	Lemma for irrapx1 38229. Two multiples in the same bucket means they are very close mod 1. (Contributed by Stefan O'Rear, 12-Sep-2014.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ) → ∃𝑥 ∈ (0...𝐵)∃𝑦 ∈ (0...𝐵)(𝑥 < 𝑦 ∧ (abs‘(((𝐴 · 𝑥) mod 1) − ((𝐴 · 𝑦) mod 1))) < (1 / 𝐵)))
Theorem	irrapxlem3 38225*	Lemma for irrapx1 38229. By subtraction, there is a multiple very close to an integer. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ) → ∃𝑥 ∈ (1...𝐵)∃𝑦 ∈ ℕ0 (abs‘((𝐴 · 𝑥) − 𝑦)) < (1 / 𝐵))
Theorem	irrapxlem4 38226*	Lemma for irrapx1 38229. Eliminate ranges, use positivity of the input to force positivity of the output by increasing 𝐵 as needed. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ) → ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℕ (abs‘((𝐴 · 𝑥) − 𝑦)) < (1 / if(𝑥 ≤ 𝐵, 𝐵, 𝑥)))
Theorem	irrapxlem5 38227*	Lemma for irrapx1 38229. Switching to real intervals and fraction syntax. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → ∃𝑥 ∈ ℚ (0 < 𝑥 ∧ (abs‘(𝑥 − 𝐴)) < 𝐵 ∧ (abs‘(𝑥 − 𝐴)) < ((denom‘𝑥)↑-2)))
Theorem	irrapxlem6 38228*	Lemma for irrapx1 38229. Explicit description of a non-closed set. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → ∃𝑥 ∈ {𝑦 ∈ ℚ ∣ (0 < 𝑦 ∧ (abs‘(𝑦 − 𝐴)) < ((denom‘𝑦)↑-2))} (abs‘(𝑥 − 𝐴)) < 𝐵)
Theorem	irrapx1 38229*	Dirichlet's approximation theorem. Every positive irrational number has infinitely many rational approximations which are closer than the inverse squares of their reduced denominators. Lemma 61 in [vandenDries] p. 42. (Contributed by Stefan O'Rear, 14-Sep-2014.)
⊢ (𝐴 ∈ (ℝ+ ∖ ℚ) → {𝑦 ∈ ℚ ∣ (0 < 𝑦 ∧ (abs‘(𝑦 − 𝐴)) < ((denom‘𝑦)↑-2))} ≈ ℕ)
20.26.21  Pell equations 1: A nontrivial solution always exists
Theorem	pellexlem1 38230	Lemma for pellex 38236. Arithmetical core of pellexlem3, norm lower bound. This begins Dirichlet's proof of the Pell equation solution existence; the proof here follows theorem 62 of [vandenDries] p. 43. (Contributed by Stefan O'Rear, 14-Sep-2014.)
⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ ¬ (√‘𝐷) ∈ ℚ) → ((𝐴↑2) − (𝐷 · (𝐵↑2))) ≠ 0)
Theorem	pellexlem2 38231	Lemma for pellex 38236. Arithmetical core of pellexlem3, norm upper bound. (Contributed by Stefan O'Rear, 14-Sep-2014.)
⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘((𝐴↑2) − (𝐷 · (𝐵↑2)))) < (1 + (2 · (√‘𝐷))))
Theorem	pellexlem3 38232*	Lemma for pellex 38236. To each good rational approximation of (√‘𝐷), there exists a near-solution. (Contributed by Stefan O'Rear, 14-Sep-2014.)
⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → {𝑥 ∈ ℚ ∣ (0 < 𝑥 ∧ (abs‘(𝑥 − (√‘𝐷))) < ((denom‘𝑥)↑-2))} ≼ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))})
Theorem	pellexlem4 38233*	Lemma for pellex 38236. Invoking irrapx1 38229, we have infinitely many near-solutions. (Contributed by Stefan O'Rear, 14-Sep-2014.)
⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ≈ ℕ)
Theorem	pellexlem5 38234*	Lemma for pellex 38236. Invoking fiphp3d 38220, we have infinitely many near-solutions for some specific norm. (Contributed by Stefan O'Rear, 19-Oct-2014.)
⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → ∃𝑥 ∈ ℤ (𝑥 ≠ 0 ∧ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≈ ℕ))
Theorem	pellexlem6 38235*	Lemma for pellex 38236. Doing a field division between near solutions get us to norm 1, and the modularity constraint ensures we still have an integer. Returning NN guarantees that we are not returning the trivial solution (1,0). We are not explicitly defining the Pell-field, Pell-ring, and Pell-norm explicitly because after this construction is done we will never use them. This is mostly basic algebraic number theory and could be simplified if a generic framework for that were in place. (Contributed by Stefan O'Rear, 19-Oct-2014.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℤ)    &   ⊢ (𝜑 → 𝐷 ∈ ℕ)    &   ⊢ (𝜑 → ¬ (√‘𝐷) ∈ ℚ)    &   ⊢ (𝜑 → 𝐸 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹 ∈ ℕ)    &   ⊢ (𝜑 → ¬ (𝐴 = 𝐸 ∧ 𝐵 = 𝐹))    &   ⊢ (𝜑 → 𝐶 ≠ 0)    &   ⊢ (𝜑 → ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 𝐶)    &   ⊢ (𝜑 → ((𝐸↑2) − (𝐷 · (𝐹↑2))) = 𝐶)    &   ⊢ (𝜑 → (𝐴 mod (abs‘𝐶)) = (𝐸 mod (abs‘𝐶)))    &   ⊢ (𝜑 → (𝐵 mod (abs‘𝐶)) = (𝐹 mod (abs‘𝐶)))    ⇒   ⊢ (𝜑 → ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)
Theorem	pellex 38236*	Every Pell equation has a nontrivial solution. Theorem 62 in [vandenDries] p. 43. (Contributed by Stefan O'Rear, 19-Oct-2014.)
⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℕ ((𝑥↑2) − (𝐷 · (𝑦↑2))) = 1)
20.26.22  Pell equations 2: Algebraic number theory of the solution set
Syntax	csquarenn 38237	Extend class notation to include the set of square positive integers.
class ◻NN
Syntax	cpell1qr 38238	Extend class notation to include the class of quadrant-1 Pell solutions.
class Pell1QR
Syntax	cpell1234qr 38239	Extend class notation to include the class of any-quadrant Pell solutions.
class Pell1234QR
Syntax	cpell14qr 38240	Extend class notation to include the class of positive Pell solutions.
class Pell14QR
Syntax	cpellfund 38241	Extend class notation to include the Pell-equation fundamental solution function.
class PellFund
Definition	df-squarenn 38242	Define the set of square positive integers. (Contributed by Stefan O'Rear, 18-Sep-2014.)
⊢ ◻NN = {𝑥 ∈ ℕ ∣ (√‘𝑥) ∈ ℚ}
Definition	df-pell1qr 38243*	Define the solutions of a Pell equation in the first quadrant. To avoid pair pain, we represent this via the canonical embedding into the reals. (Contributed by Stefan O'Rear, 17-Sep-2014.)
⊢ Pell1QR = (𝑥 ∈ (ℕ ∖ ◻NN) ↦ {𝑦 ∈ ℝ ∣ ∃𝑧 ∈ ℕ0 ∃𝑤 ∈ ℕ0 (𝑦 = (𝑧 + ((√‘𝑥) · 𝑤)) ∧ ((𝑧↑2) − (𝑥 · (𝑤↑2))) = 1)})
Definition	df-pell14qr 38244*	Define the positive solutions of a Pell equation. (Contributed by Stefan O'Rear, 17-Sep-2014.)
⊢ Pell14QR = (𝑥 ∈ (ℕ ∖ ◻NN) ↦ {𝑦 ∈ ℝ ∣ ∃𝑧 ∈ ℕ0 ∃𝑤 ∈ ℤ (𝑦 = (𝑧 + ((√‘𝑥) · 𝑤)) ∧ ((𝑧↑2) − (𝑥 · (𝑤↑2))) = 1)})
Definition	df-pell1234qr 38245*	Define the general solutions of a Pell equation. (Contributed by Stefan O'Rear, 17-Sep-2014.)
⊢ Pell1234QR = (𝑥 ∈ (ℕ ∖ ◻NN) ↦ {𝑦 ∈ ℝ ∣ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ (𝑦 = (𝑧 + ((√‘𝑥) · 𝑤)) ∧ ((𝑧↑2) − (𝑥 · (𝑤↑2))) = 1)})
Definition	df-pellfund 38246*	A function mapping Pell discriminants to the corresponding fundamental solution. (Contributed by Stefan O'Rear, 18-Sep-2014.) (Revised by AV, 17-Sep-2020.)
⊢ PellFund = (𝑥 ∈ (ℕ ∖ ◻NN) ↦ inf({𝑧 ∈ (Pell14QR‘𝑥) ∣ 1 < 𝑧}, ℝ, < ))
Theorem	pell1qrval 38247*	Value of the set of first-quadrant Pell solutions. (Contributed by Stefan O'Rear, 17-Sep-2014.)
⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (Pell1QR‘𝐷) = {𝑦 ∈ ℝ ∣ ∃𝑧 ∈ ℕ0 ∃𝑤 ∈ ℕ0 (𝑦 = (𝑧 + ((√‘𝐷) · 𝑤)) ∧ ((𝑧↑2) − (𝐷 · (𝑤↑2))) = 1)})
Theorem	elpell1qr 38248*	Membership in a first-quadrant Pell solution set. (Contributed by Stefan O'Rear, 17-Sep-2014.)
⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (𝐴 ∈ (Pell1QR‘𝐷) ↔ (𝐴 ∈ ℝ ∧ ∃𝑧 ∈ ℕ0 ∃𝑤 ∈ ℕ0 (𝐴 = (𝑧 + ((√‘𝐷) · 𝑤)) ∧ ((𝑧↑2) − (𝐷 · (𝑤↑2))) = 1))))
Theorem	pell14qrval 38249*	Value of the set of positive Pell solutions. (Contributed by Stefan O'Rear, 17-Sep-2014.)
⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (Pell14QR‘𝐷) = {𝑦 ∈ ℝ ∣ ∃𝑧 ∈ ℕ0 ∃𝑤 ∈ ℤ (𝑦 = (𝑧 + ((√‘𝐷) · 𝑤)) ∧ ((𝑧↑2) − (𝐷 · (𝑤↑2))) = 1)})
Theorem	elpell14qr 38250*	Membership in the set of positive Pell solutions. (Contributed by Stefan O'Rear, 17-Sep-2014.)
⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (𝐴 ∈ (Pell14QR‘𝐷) ↔ (𝐴 ∈ ℝ ∧ ∃𝑧 ∈ ℕ0 ∃𝑤 ∈ ℤ (𝐴 = (𝑧 + ((√‘𝐷) · 𝑤)) ∧ ((𝑧↑2) − (𝐷 · (𝑤↑2))) = 1))))
Theorem	pell1234qrval 38251*	Value of the set of general Pell solutions. (Contributed by Stefan O'Rear, 17-Sep-2014.)
⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (Pell1234QR‘𝐷) = {𝑦 ∈ ℝ ∣ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ (𝑦 = (𝑧 + ((√‘𝐷) · 𝑤)) ∧ ((𝑧↑2) − (𝐷 · (𝑤↑2))) = 1)})
Theorem	elpell1234qr 38252*	Membership in the set of general Pell solutions. (Contributed by Stefan O'Rear, 17-Sep-2014.)
⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (𝐴 ∈ (Pell1234QR‘𝐷) ↔ (𝐴 ∈ ℝ ∧ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ (𝐴 = (𝑧 + ((√‘𝐷) · 𝑤)) ∧ ((𝑧↑2) − (𝐷 · (𝑤↑2))) = 1))))
Theorem	pell1234qrre 38253	General Pell solutions are (coded as) real numbers. (Contributed by Stefan O'Rear, 17-Sep-2014.)
⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell1234QR‘𝐷)) → 𝐴 ∈ ℝ)
Theorem	pell1234qrne0 38254	No solution to a Pell equation is zero. (Contributed by Stefan O'Rear, 17-Sep-2014.)
⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell1234QR‘𝐷)) → 𝐴 ≠ 0)
Theorem	pell1234qrreccl 38255	General solutions of the Pell equation are closed under reciprocals. (Contributed by Stefan O'Rear, 18-Sep-2014.)
⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell1234QR‘𝐷)) → (1 / 𝐴) ∈ (Pell1234QR‘𝐷))
Theorem	pell1234qrmulcl 38256	General solutions of the Pell equation are closed under multiplication. (Contributed by Stefan O'Rear, 18-Sep-2014.)
⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell1234QR‘𝐷) ∧ 𝐵 ∈ (Pell1234QR‘𝐷)) → (𝐴 · 𝐵) ∈ (Pell1234QR‘𝐷))
Theorem	pell14qrss1234 38257	A positive Pell solution is a general Pell solution. (Contributed by Stefan O'Rear, 18-Sep-2014.)
⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (Pell14QR‘𝐷) ⊆ (Pell1234QR‘𝐷))
Theorem	pell14qrre 38258	A positive Pell solution is a real number. (Contributed by Stefan O'Rear, 18-Sep-2014.)
⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) → 𝐴 ∈ ℝ)
Theorem	pell14qrne0 38259	A positive Pell solution is a nonzero number. (Contributed by Stefan O'Rear, 17-Sep-2014.)
⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) → 𝐴 ≠ 0)
Theorem	pell14qrgt0 38260	A positive Pell solution is a positive number. (Contributed by Stefan O'Rear, 18-Sep-2014.)
⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) → 0 < 𝐴)
Theorem	pell14qrrp 38261	A positive Pell solution is a positive real. (Contributed by Stefan O'Rear, 19-Sep-2014.)
⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) → 𝐴 ∈ ℝ+)
Theorem	pell1234qrdich 38262	A general Pell solution is either a positive solution, or its negation is. (Contributed by Stefan O'Rear, 18-Sep-2014.)
⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell1234QR‘𝐷)) → (𝐴 ∈ (Pell14QR‘𝐷) ∨ -𝐴 ∈ (Pell14QR‘𝐷)))
Theorem	elpell14qr2 38263	A number is a positive Pell solution iff it is positive and a Pell solution, justifying our name choice. (Contributed by Stefan O'Rear, 19-Oct-2014.)
⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (𝐴 ∈ (Pell14QR‘𝐷) ↔ (𝐴 ∈ (Pell1234QR‘𝐷) ∧ 0 < 𝐴)))
Theorem	pell14qrmulcl 38264	Positive Pell solutions are closed under multiplication. (Contributed by Stefan O'Rear, 17-Sep-2014.)
⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 𝐵 ∈ (Pell14QR‘𝐷)) → (𝐴 · 𝐵) ∈ (Pell14QR‘𝐷))
Theorem	pell14qrreccl 38265	Positive Pell solutions are closed under reciprocal. (Contributed by Stefan O'Rear, 18-Sep-2014.)
⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) → (1 / 𝐴) ∈ (Pell14QR‘𝐷))
Theorem	pell14qrdivcl 38266	Positive Pell solutions are closed under division. (Contributed by Stefan O'Rear, 18-Sep-2014.)
⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 𝐵 ∈ (Pell14QR‘𝐷)) → (𝐴 / 𝐵) ∈ (Pell14QR‘𝐷))
Theorem	pell14qrexpclnn0 38267	Lemma for pell14qrexpcl 38268. (Contributed by Stefan O'Rear, 18-Sep-2014.)
⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 𝐵 ∈ ℕ0) → (𝐴↑𝐵) ∈ (Pell14QR‘𝐷))
Theorem	pell14qrexpcl 38268	Positive Pell solutions are closed under integer powers. (Contributed by Stefan O'Rear, 18-Sep-2014.)
⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 𝐵 ∈ ℤ) → (𝐴↑𝐵) ∈ (Pell14QR‘𝐷))
Theorem	pell1qrss14 38269	First-quadrant Pell solutions are a subset of the positive solutions. (Contributed by Stefan O'Rear, 18-Sep-2014.)
⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (Pell1QR‘𝐷) ⊆ (Pell14QR‘𝐷))
Theorem	pell14qrdich 38270	A positive Pell solution is either in the first quadrant, or its reciprocal is. (Contributed by Stefan O'Rear, 18-Sep-2014.)
⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) → (𝐴 ∈ (Pell1QR‘𝐷) ∨ (1 / 𝐴) ∈ (Pell1QR‘𝐷)))
Theorem	pell1qrge1 38271	A Pell solution in the first quadrant is at least 1. (Contributed by Stefan O'Rear, 17-Sep-2014.)
⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell1QR‘𝐷)) → 1 ≤ 𝐴)
Theorem	pell1qr1 38272	1 is a Pell solution and in the first quadrant as one. (Contributed by Stefan O'Rear, 17-Sep-2014.)
⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → 1 ∈ (Pell1QR‘𝐷))
Theorem	elpell1qr2 38273	The first quadrant solutions are precisely the positive Pell solutions which are at least one. (Contributed by Stefan O'Rear, 18-Sep-2014.)
⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (𝐴 ∈ (Pell1QR‘𝐷) ↔ (𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 ≤ 𝐴)))
Theorem	pell1qrgaplem 38274	Lemma for pell1qrgap 38275. (Contributed by Stefan O'Rear, 18-Sep-2014.)
⊢ (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → ((√‘(𝐷 + 1)) + (√‘𝐷)) ≤ (𝐴 + ((√‘𝐷) · 𝐵)))
Theorem	pell1qrgap 38275	First-quadrant Pell solutions are bounded away from 1. (This particular bound allows us to prove exact values for the fundamental solution later.) (Contributed by Stefan O'Rear, 18-Sep-2014.)
⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell1QR‘𝐷) ∧ 1 < 𝐴) → ((√‘(𝐷 + 1)) + (√‘𝐷)) ≤ 𝐴)
Theorem	pell14qrgap 38276	Positive Pell solutions are bounded away from 1. (Contributed by Stefan O'Rear, 18-Sep-2014.)
⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → ((√‘(𝐷 + 1)) + (√‘𝐷)) ≤ 𝐴)
Theorem	pell14qrgapw 38277	Positive Pell solutions are bounded away from 1, with a friendlier bound. (Contributed by Stefan O'Rear, 18-Sep-2014.)
⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → 2 < 𝐴)
Theorem	pellqrexplicit 38278	Condition for a calculated real to be a Pell solution. (Contributed by Stefan O'Rear, 19-Sep-2014.)
⊢ (((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1) → (𝐴 + ((√‘𝐷) · 𝐵)) ∈ (Pell1QR‘𝐷))
20.26.23  Pell equations 3: characterizing fundamental solution
Theorem	infmrgelbi 38279*	Any lower bound of a nonempty set of real numbers is less than or equal to its infimum, one-direction version. (Contributed by Stefan O'Rear, 1-Sep-2013.) (Revised by AV, 17-Sep-2020.)
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ 𝐵 ∈ ℝ) ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑥) → 𝐵 ≤ inf(𝐴, ℝ, < ))
Theorem	pellqrex 38280*	There is a nontrivial solution of a Pell equation in the first quadrant. (Contributed by Stefan O'Rear, 18-Sep-2014.)
⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → ∃𝑥 ∈ (Pell1QR‘𝐷)1 < 𝑥)
Theorem	pellfundval 38281*	Value of the fundamental solution of a Pell equation. (Contributed by Stefan O'Rear, 18-Sep-2014.) (Revised by AV, 17-Sep-2020.)
⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (PellFund‘𝐷) = inf({𝑥 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑥}, ℝ, < ))
Theorem	pellfundre 38282	The fundamental solution of a Pell equation exists as a real number. (Contributed by Stefan O'Rear, 18-Sep-2014.)
⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (PellFund‘𝐷) ∈ ℝ)
Theorem	pellfundge 38283	Lower bound on the fundamental solution of a Pell equation. (Contributed by Stefan O'Rear, 19-Sep-2014.)
⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → ((√‘(𝐷 + 1)) + (√‘𝐷)) ≤ (PellFund‘𝐷))
Theorem	pellfundgt1 38284	Weak lower bound on the Pell fundamental solution. (Contributed by Stefan O'Rear, 19-Sep-2014.)
⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → 1 < (PellFund‘𝐷))
Theorem	pellfundlb 38285	A nontrivial first quadrant solution is at least as large as the fundamental solution. (Contributed by Stefan O'Rear, 19-Sep-2014.) (Proof shortened by AV, 15-Sep-2020.)
⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → (PellFund‘𝐷) ≤ 𝐴)
Theorem	pellfundglb 38286*	If a real is larger than the fundamental solution, there is a nontrivial solution less than it. (Contributed by Stefan O'Rear, 18-Sep-2014.)
⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) → ∃𝑥 ∈ (Pell1QR‘𝐷)((PellFund‘𝐷) ≤ 𝑥 ∧ 𝑥 < 𝐴))
Theorem	pellfundex 38287	The fundamental solution as an infimum is itself a solution, showing that the solution set is discrete. Since the fundamental solution is an infimum, there must be an element ge to Fund and lt 2*Fund. If this element is equal to the fundamental solution we're done, otherwise use the infimum again to find another element which must be ge Fund and lt the first element; their ratio is a group element in (1,2), contradicting pell14qrgapw 38277. (Contributed by Stefan O'Rear, 18-Sep-2014.)
⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (PellFund‘𝐷) ∈ (Pell1QR‘𝐷))
Theorem	pellfund14gap 38288	There are no solutions between 1 and the fundamental solution. (Contributed by Stefan O'Rear, 18-Sep-2014.)
⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ (1 ≤ 𝐴 ∧ 𝐴 < (PellFund‘𝐷))) → 𝐴 = 1)
Theorem	pellfundrp 38289	The fundamental Pell solution is a positive real. (Contributed by Stefan O'Rear, 19-Sep-2014.)
⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (PellFund‘𝐷) ∈ ℝ+)
Theorem	pellfundne1 38290	The fundamental Pell solution is never 1. (Contributed by Stefan O'Rear, 19-Sep-2014.)
⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (PellFund‘𝐷) ≠ 1)
20.26.24  Logarithm laws generalized to an arbitrary base Section should be obsolete because its contents are covered by section "Logarithms to an arbitrary base" now.
Theorem	reglogcl 38291	General logarithm is a real number. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use relogbcl 24913 instead.
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1) → ((log‘𝐴) / (log‘𝐵)) ∈ ℝ)
Theorem	reglogltb 38292	General logarithm preserves "less than". (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use logblt 24924 instead.
⊢ (((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) ∧ (𝐶 ∈ ℝ+ ∧ 1 < 𝐶)) → (𝐴 < 𝐵 ↔ ((log‘𝐴) / (log‘𝐶)) < ((log‘𝐵) / (log‘𝐶))))
Theorem	reglogleb 38293	General logarithm preserves ≤. (Contributed by Stefan O'Rear, 19-Oct-2014.) (New usage is discouraged.) Use logbleb 24923 instead.
⊢ (((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) ∧ (𝐶 ∈ ℝ+ ∧ 1 < 𝐶)) → (𝐴 ≤ 𝐵 ↔ ((log‘𝐴) / (log‘𝐶)) ≤ ((log‘𝐵) / (log‘𝐶))))
Theorem	reglogmul 38294	Multiplication law for general log. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use relogbmul 24917 instead.
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ∧ (𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1)) → ((log‘(𝐴 · 𝐵)) / (log‘𝐶)) = (((log‘𝐴) / (log‘𝐶)) + ((log‘𝐵) / (log‘𝐶))))
Theorem	reglogexp 38295	Power law for general log. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use relogbzexp 24916 instead.
⊢ ((𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℤ ∧ (𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1)) → ((log‘(𝐴↑𝑁)) / (log‘𝐶)) = (𝑁 · ((log‘𝐴) / (log‘𝐶))))
Theorem	reglogbas 38296	General log of the base is 1. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use logbid1 24908 instead.
⊢ ((𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1) → ((log‘𝐶) / (log‘𝐶)) = 1)
Theorem	reglog1 38297	General log of 1 is 0. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use logb1 24909 instead.
⊢ ((𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1) → ((log‘1) / (log‘𝐶)) = 0)
Theorem	reglogexpbas 38298	General log of a power of the base is the exponent. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use relogbexp 24920 instead.
⊢ ((𝑁 ∈ ℤ ∧ (𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1)) → ((log‘(𝐶↑𝑁)) / (log‘𝐶)) = 𝑁)
20.26.25  Pell equations 4: the positive solution group is infinite cyclic
Theorem	pellfund14 38299*	Every positive Pell solution is a power of the fundamental solution. (Contributed by Stefan O'Rear, 19-Sep-2014.)
⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) → ∃𝑥 ∈ ℤ 𝐴 = ((PellFund‘𝐷)↑𝑥))
Theorem	pellfund14b 38300*	The positive Pell solutions are precisely the integer powers of the fundamental solution. To get the general solution set (which we will not be using), throw in a copy of Z/2Z. (Contributed by Stefan O'Rear, 19-Sep-2014.)
⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (𝐴 ∈ (Pell14QR‘𝐷) ↔ ∃𝑥 ∈ ℤ 𝐴 = ((PellFund‘𝐷)↑𝑥)))