P. 362 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 36101-36200   *Has distinct variable group(s)

Type	Label	Description
Statement
Syntax	cmsy 36101	The syntax typecode function.
class mSyn
Syntax	cmesy 36102	The syntax typecode function for expressions.
class mESyn
Syntax	cmgfs 36103	The set of grammatical formal systems.
class mGFS
Syntax	cmtree 36104	The set of proof trees.
class mTree
Syntax	cmst 36105	The set of syntax trees.
class mST
Syntax	cmsax 36106	The indexing set for a syntax axiom.
class mSAX
Syntax	cmufs 36107	The set of unambiguous formal systems.
class mUFS
Definition	df-m0s 36108	Define a function mapping expressions to statements. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ m0St = (𝑎 ∈ V ↦ ⟨∅, ∅, 𝑎⟩)
Definition	df-msa 36109*	Define the set of syntax axioms. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mSA = (𝑡 ∈ V ↦ {𝑎 ∈ (mEx‘𝑡) ∣ ((m0St‘𝑎) ∈ (mAx‘𝑡) ∧ (1st ‘𝑎) ∈ (mVT‘𝑡) ∧ Fun (◡(2nd ‘𝑎) ↾ (mVR‘𝑡)))})
Definition	df-mwgfs 36110*	Define the set of weakly grammatical formal systems. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mWGFS = {𝑡 ∈ mFS ∣ ∀𝑑∀ℎ∀𝑎((⟨𝑑, ℎ, 𝑎⟩ ∈ (mAx‘𝑡) ∧ (1st ‘𝑎) ∈ (mVT‘𝑡)) → ∃𝑠 ∈ ran (mSubst‘𝑡)𝑎 ∈ (𝑠 “ (mSA‘𝑡)))}
Definition	df-msyn 36111	Define the syntax typecode function. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mSyn = Slot 6
Definition	df-mesyn 36112*	Define the syntax typecode function for expressions. (Contributed by Mario Carneiro, 12-Jun-2023.)
⊢ mESyn = (𝑡 ∈ V ↦ (𝑐 ∈ (mTC‘𝑡), 𝑒 ∈ (mREx‘𝑡) ↦ (((mSyn‘𝑡)‘𝑐)m0St𝑒)))
Definition	df-mgfs 36113*	Define the set of grammatical formal systems. (Contributed by Mario Carneiro, 12-Jun-2023.)
⊢ mGFS = {𝑡 ∈ mWGFS ∣ ((mSyn‘𝑡):(mTC‘𝑡)⟶(mVT‘𝑡) ∧ ∀𝑐 ∈ (mVT‘𝑡)((mSyn‘𝑡)‘𝑐) = 𝑐 ∧ ∀𝑑∀ℎ∀𝑎(⟨𝑑, ℎ, 𝑎⟩ ∈ (mAx‘𝑡) → ∀𝑒 ∈ (ℎ ∪ {𝑎})((mESyn‘𝑡)‘𝑒) ∈ (mPPSt‘𝑡)))}
Definition	df-mtree 36114*	Define the set of proof trees. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mTree = (𝑡 ∈ V ↦ (𝑑 ∈ 𝒫 (mDV‘𝑡), ℎ ∈ 𝒫 (mEx‘𝑡) ↦ ∩ {𝑟 ∣ (∀𝑒 ∈ ran (mVH‘𝑡)𝑒𝑟⟨(m0St‘𝑒), ∅⟩ ∧ ∀𝑒 ∈ ℎ 𝑒𝑟⟨((mStRed‘𝑡)‘⟨𝑑, ℎ, 𝑒⟩), ∅⟩ ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑) → ({(𝑠‘𝑝)} × X𝑒 ∈ (𝑜 ∪ ((mVH‘𝑡) “ ∪ ((mVars‘𝑡) “ (𝑜 ∪ {𝑝}))))(𝑟 “ {(𝑠‘𝑒)})) ⊆ 𝑟)))}))
Definition	df-mst 36115	Define the function mapping syntax expressions to syntax trees. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mST = (𝑡 ∈ V ↦ ((∅(mTree‘𝑡)∅) ↾ ((mEx‘𝑡) ↾ (mVT‘𝑡))))
Definition	df-msax 36116*	Define the indexing set for a syntax axiom's representation in a tree. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mSAX = (𝑡 ∈ V ↦ (𝑝 ∈ (mSA‘𝑡) ↦ ((mVH‘𝑡) “ ((mVars‘𝑡)‘𝑝))))
Definition	df-mufs 36117	Define the set of unambiguous formal systems. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mUFS = {𝑡 ∈ mGFS ∣ Fun (mST‘𝑡)}
21.6.15  Models of formal systems
Syntax	cmuv 36118	The universe of a model.
class mUV
Syntax	cmvl 36119	The set of valuations.
class mVL
Syntax	cmvsb 36120	Substitution for a valuation.
class mVSubst
Syntax	cmfsh 36121	The freshness relation of a model.
class mFresh
Syntax	cmfr 36122	The set of freshness relations.
class mFRel
Syntax	cmevl 36123	The evaluation function of a model.
class mEval
Syntax	cmdl 36124	The set of models.
class mMdl
Syntax	cusyn 36125	The syntax function applied to elements of the model.
class mUSyn
Syntax	cgmdl 36126	The set of models in a grammatical formal system.
class mGMdl
Syntax	cmitp 36127	The interpretation function of the model.
class mItp
Syntax	cmfitp 36128	The evaluation function derived from the interpretation.
class mFromItp
Definition	df-muv 36129	Define the universe of a model. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mUV = Slot 7
Definition	df-mfsh 36130	Define the freshness relation of a model. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mFresh = Slot ;19
Definition	df-mevl 36131	Define the evaluation function of a model. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mEval = Slot ;20
Definition	df-mvl 36132*	Define the set of valuations. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mVL = (𝑡 ∈ V ↦ X𝑣 ∈ (mVR‘𝑡)((mUV‘𝑡) “ {((mType‘𝑡)‘𝑣)}))
Definition	df-mvsb 36133*	Define substitution applied to a valuation. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mVSubst = (𝑡 ∈ V ↦ {⟨⟨𝑠, 𝑚⟩, 𝑥⟩ ∣ ((𝑠 ∈ ran (mSubst‘𝑡) ∧ 𝑚 ∈ (mVL‘𝑡)) ∧ ∀𝑣 ∈ (mVR‘𝑡)𝑚dom (mEval‘𝑡)(𝑠‘((mVH‘𝑡)‘𝑣)) ∧ 𝑥 = (𝑣 ∈ (mVR‘𝑡) ↦ (𝑚(mEval‘𝑡)(𝑠‘((mVH‘𝑡)‘𝑣)))))})
Definition	df-mfrel 36134*	Define the set of freshness relations. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mFRel = (𝑡 ∈ V ↦ {𝑟 ∈ 𝒫 ((mUV‘𝑡) × (mUV‘𝑡)) ∣ (◡𝑟 = 𝑟 ∧ ∀𝑐 ∈ (mVT‘𝑡)∀𝑤 ∈ (𝒫 (mUV‘𝑡) ∩ Fin)∃𝑣 ∈ ((mUV‘𝑡) “ {𝑐})𝑤 ⊆ (𝑟 “ {𝑣}))})
Definition	df-mdl 36135*	Define the set of models of a formal system. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mMdl = {𝑡 ∈ mFS ∣ [(mUV‘𝑡) / 𝑢][(mEx‘𝑡) / 𝑥][(mVL‘𝑡) / 𝑣][(mEval‘𝑡) / 𝑛][(mFresh‘𝑡) / 𝑓]((𝑢 ⊆ ((mTC‘𝑡) × V) ∧ 𝑓 ∈ (mFRel‘𝑡) ∧ 𝑛 ∈ (𝑢 ↑pm (𝑣 × (mEx‘𝑡)))) ∧ ∀𝑚 ∈ 𝑣 ((∀𝑒 ∈ 𝑥 (𝑛 “ {⟨𝑚, 𝑒⟩}) ⊆ (𝑢 “ {(1st ‘𝑒)}) ∧ ∀𝑦 ∈ (mVR‘𝑡)⟨𝑚, ((mVH‘𝑡)‘𝑦)⟩𝑛(𝑚‘𝑦) ∧ ∀𝑑∀ℎ∀𝑎(⟨𝑑, ℎ, 𝑎⟩ ∈ (mAx‘𝑡) → ((∀𝑦∀𝑧(𝑦𝑑𝑧 → (𝑚‘𝑦)𝑓(𝑚‘𝑧)) ∧ ℎ ⊆ (dom 𝑛 “ {𝑚})) → 𝑚dom 𝑛 𝑎))) ∧ (∀𝑠 ∈ ran (mSubst‘𝑡)∀𝑒 ∈ (mEx‘𝑡)∀𝑦(⟨𝑠, 𝑚⟩(mVSubst‘𝑡)𝑦 → (𝑛 “ {⟨𝑚, (𝑠‘𝑒)⟩}) = (𝑛 “ {⟨𝑦, 𝑒⟩})) ∧ ∀𝑝 ∈ 𝑣 ∀𝑒 ∈ 𝑥 ((𝑚 ↾ ((mVars‘𝑡)‘𝑒)) = (𝑝 ↾ ((mVars‘𝑡)‘𝑒)) → (𝑛 “ {⟨𝑚, 𝑒⟩}) = (𝑛 “ {⟨𝑝, 𝑒⟩})) ∧ ∀𝑦 ∈ 𝑢 ∀𝑒 ∈ 𝑥 ((𝑚 “ ((mVars‘𝑡)‘𝑒)) ⊆ (𝑓 “ {𝑦}) → (𝑛 “ {⟨𝑚, 𝑒⟩}) ⊆ (𝑓 “ {𝑦})))))}
Definition	df-musyn 36136*	Define the syntax typecode function for the model universe. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mUSyn = (𝑡 ∈ V ↦ (𝑣 ∈ (mUV‘𝑡) ↦ ⟨((mSyn‘𝑡)‘(1st ‘𝑣)), (2nd ‘𝑣)⟩))
Definition	df-gmdl 36137*	Define the set of models of a grammatical formal system. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mGMdl = {𝑡 ∈ (mGFS ∩ mMdl) ∣ (∀𝑐 ∈ (mTC‘𝑡)((mUV‘𝑡) “ {𝑐}) ⊆ ((mUV‘𝑡) “ {((mSyn‘𝑡)‘𝑐)}) ∧ ∀𝑣 ∈ (mUV‘𝑐)∀𝑤 ∈ (mUV‘𝑐)(𝑣(mFresh‘𝑡)𝑤 ↔ 𝑣(mFresh‘𝑡)((mUSyn‘𝑡)‘𝑤)) ∧ ∀𝑚 ∈ (mVL‘𝑡)∀𝑒 ∈ (mEx‘𝑡)((mEval‘𝑡) “ {⟨𝑚, 𝑒⟩}) = (((mEval‘𝑡) “ {⟨𝑚, ((mESyn‘𝑡)‘𝑒)⟩}) ∩ ((mUV‘𝑡) “ {(1st ‘𝑒)})))}
Definition	df-mitp 36138*	Define the interpretation function for a model. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mItp = (𝑡 ∈ V ↦ (𝑎 ∈ (mSA‘𝑡) ↦ (𝑔 ∈ X𝑖 ∈ ((mVars‘𝑡)‘𝑎)((mUV‘𝑡) “ {((mType‘𝑡)‘𝑖)}) ↦ (℩𝑥∃𝑚 ∈ (mVL‘𝑡)(𝑔 = (𝑚 ↾ ((mVars‘𝑡)‘𝑎)) ∧ 𝑥 = (𝑚(mEval‘𝑡)𝑎))))))
Definition	df-mfitp 36139*	Define a function that produces the evaluation function, given the interpretation function for a model. (Contributed by Mario Carneiro, 14-Jul-2016.)
⊢ mFromItp = (𝑡 ∈ V ↦ (𝑓 ∈ X𝑎 ∈ (mSA‘𝑡)(((mUV‘𝑡) “ {((1st ‘𝑡)‘𝑎)}) ↑m X𝑖 ∈ ((mVars‘𝑡)‘𝑎)((mUV‘𝑡) “ {((mType‘𝑡)‘𝑖)})) ↦ (℩𝑛 ∈ ((mUV‘𝑡) ↑pm ((mVL‘𝑡) × (mEx‘𝑡)))∀𝑚 ∈ (mVL‘𝑡)(∀𝑣 ∈ (mVR‘𝑡)⟨𝑚, ((mVH‘𝑡)‘𝑣)⟩𝑛(𝑚‘𝑣) ∧ ∀𝑒∀𝑎∀𝑔(𝑒(mST‘𝑡)⟨𝑎, 𝑔⟩ → ⟨𝑚, 𝑒⟩𝑛(𝑓‘(𝑖 ∈ ((mVars‘𝑡)‘𝑎) ↦ (𝑚𝑛(𝑔‘((mVH‘𝑡)‘𝑖)))))) ∧ ∀𝑒 ∈ (mEx‘𝑡)(𝑛 “ {⟨𝑚, 𝑒⟩}) = ((𝑛 “ {⟨𝑚, ((mESyn‘𝑡)‘𝑒)⟩}) ∩ ((mUV‘𝑡) “ {(1st ‘𝑒)}))))))
21.6.16  Splitting fields
Syntax	ccpms 36140	Completion of a metric space.
class cplMetSp
Syntax	chlb 36141	Embeddings for a direct limit.
class HomLimB
Syntax	chlim 36142	Direct limit structure.
class HomLim
Syntax	cpfl 36143	Polynomial extension field.
class polyFld
Syntax	csf1 36144	Splitting field for a single polynomial (auxiliary).
class splitFld1
Syntax	csf 36145	Splitting field for a finite set of polynomials.
class splitFld
Syntax	cpsl 36146	Splitting field for a sequence of polynomials.
class polySplitLim
Definition	df-cplmet 36147*	A function which completes the given metric space. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ cplMetSp = (𝑤 ∈ V ↦ ⦋((𝑤 ↑s ℕ) ↾s (Cau‘(dist‘𝑤))) / 𝑟⦌⦋(Base‘𝑟) / 𝑣⦌⦋{⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑔‘𝑗)(ball‘(dist‘𝑤))𝑥))} / 𝑒⦌((𝑟 /s 𝑒) sSet {⟨(dist‘ndx), {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ∃𝑝 ∈ 𝑣 ∃𝑞 ∈ 𝑣 ((𝑥 = [𝑝]𝑒 ∧ 𝑦 = [𝑞]𝑒) ∧ (𝑝 ∘f (dist‘𝑟)𝑞) ⇝ 𝑧)}⟩}))
Definition	df-homlimb 36148*	The input to this function is a sequence (on ℕ) of homomorphisms 𝐹(𝑛):𝑅(𝑛)⟶𝑅(𝑛 + 1). The resulting structure is the direct limit of the direct system so defined. This function returns the pair ⟨𝑆, 𝐺⟩ where 𝑆 is the terminal object and 𝐺 is a sequence of functions such that 𝐺(𝑛):𝑅(𝑛)⟶𝑆 and 𝐺(𝑛) = 𝐹(𝑛) ∘ 𝐺(𝑛 + 1). (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ HomLimB = (𝑓 ∈ V ↦ ⦋∪ 𝑛 ∈ ℕ ({𝑛} × dom (𝑓‘𝑛)) / 𝑣⦌⦋∩ {𝑠 ∣ (𝑠 Er 𝑣 ∧ (𝑥 ∈ 𝑣 ↦ ⟨((1st ‘𝑥) + 1), ((𝑓‘(1st ‘𝑥))‘(2nd ‘𝑥))⟩) ⊆ 𝑠)} / 𝑒⦌⟨(𝑣 / 𝑒), (𝑛 ∈ ℕ ↦ (𝑥 ∈ dom (𝑓‘𝑛) ↦ [⟨𝑛, 𝑥⟩]𝑒))⟩)
Definition	df-homlim 36149*	The input to this function is a sequence (on ℕ) of structures 𝑅(𝑛) and homomorphisms 𝐹(𝑛):𝑅(𝑛)⟶𝑅(𝑛 + 1). The resulting structure is the direct limit of the direct system so defined, and maintains any structures that were present in the original objects. TODO: generalize to directed sets? (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ HomLim = (𝑟 ∈ V, 𝑓 ∈ V ↦ ⦋( HomLimB ‘𝑓) / 𝑒⦌⦋(1st ‘𝑒) / 𝑣⦌⦋(2nd ‘𝑒) / 𝑔⦌({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), ∪ 𝑛 ∈ ℕ ran (𝑥 ∈ dom (𝑔‘𝑛), 𝑦 ∈ dom (𝑔‘𝑛) ↦ ⟨⟨((𝑔‘𝑛)‘𝑥), ((𝑔‘𝑛)‘𝑦)⟩, ((𝑔‘𝑛)‘(𝑥(+g‘(𝑟‘𝑛))𝑦))⟩)⟩, ⟨(.r‘ndx), ∪ 𝑛 ∈ ℕ ran (𝑥 ∈ dom (𝑔‘𝑛), 𝑦 ∈ dom (𝑔‘𝑛) ↦ ⟨⟨((𝑔‘𝑛)‘𝑥), ((𝑔‘𝑛)‘𝑦)⟩, ((𝑔‘𝑛)‘(𝑥(.r‘(𝑟‘𝑛))𝑦))⟩)⟩} ∪ {⟨(TopOpen‘ndx), {𝑠 ∈ 𝒫 𝑣 ∣ ∀𝑛 ∈ ℕ (◡(𝑔‘𝑛) “ 𝑠) ∈ (TopOpen‘(𝑟‘𝑛))}⟩, ⟨(dist‘ndx), ∪ 𝑛 ∈ ℕ ran (𝑥 ∈ dom ((𝑔‘𝑛)‘𝑛), 𝑦 ∈ dom ((𝑔‘𝑛)‘𝑛) ↦ ⟨⟨((𝑔‘𝑛)‘𝑥), ((𝑔‘𝑛)‘𝑦)⟩, (𝑥(dist‘(𝑟‘𝑛))𝑦)⟩)⟩, ⟨(le‘ndx), ∪ 𝑛 ∈ ℕ (◡(𝑔‘𝑛) ∘ ((le‘(𝑟‘𝑛)) ∘ (𝑔‘𝑛)))⟩}))
Definition	df-plfl 36150*	Define the field extension that augments a field with the root of the given irreducible polynomial, and extends the norm if one exists and the extension is unique. (Contributed by Mario Carneiro, 2-Dec-2014.) (Revised by Thierry Arnoux and Steven Nguyen, 21-Jun-2025.)
⊢ polyFld = (𝑟 ∈ V, 𝑝 ∈ V ↦ ⦋(Poly1‘𝑟) / 𝑠⦌⦋((RSpan‘𝑠)‘{𝑝}) / 𝑖⦌⦋(𝑐 ∈ (Base‘𝑟) ↦ [(𝑐( ·𝑠 ‘𝑠)(1r‘𝑠))](𝑠 ~QG 𝑖)) / 𝑓⦌⟨⦋(𝑠 /s (𝑠 ~QG 𝑖)) / 𝑡⦌((𝑡 toNrmGrp (℩𝑛 ∈ (AbsVal‘𝑡)(𝑛 ∘ 𝑓) = (norm‘𝑟))) sSet ⟨(le‘ndx), ⦋(𝑧 ∈ (Base‘𝑡) ↦ (℩𝑞 ∈ 𝑧 (𝑞(rem1p‘𝑟)𝑝) = 𝑞)) / 𝑔⦌(◡𝑔 ∘ ((le‘𝑠) ∘ 𝑔))⟩), 𝑓⟩)
Theorem	rexxfr3d 36151*	Transfer existential quantification from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. (Contributed by SN, 20-Jun-2025.)
⊢ (𝑥 = 𝑋 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ ∃𝑦 ∈ 𝐵 𝑥 = 𝑋))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑦 ∈ 𝐵 𝜒))
Theorem	rexxfr3dALT 36152*	Longer proof of rexxfr3d 36151 using ax-11 2195 instead of ax-12 2216, without the disjoint variable condition 𝐴𝑥𝑦. (Contributed by SN, 19-Jun-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝑋 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ ∃𝑦 ∈ 𝐵 𝑥 = 𝑋))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑦 ∈ 𝐵 𝜒))
Theorem	rspssbasd 36153	The span of a set of ring elements is a set of ring elements. (Contributed by SN, 19-Jun-2025.)
⊢ 𝐾 = (RSpan‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐺 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝐾‘𝐺) ⊆ 𝐵)
Theorem	ellcsrspsn 36154*	Membership in a left coset in a quotient of a ring by the span of a singleton (that is, by the ideal generated by an element). This characterization comes from eqglact 19278 and elrspsn 21408. (Contributed by SN, 19-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ ∼ = (𝑅 ~QG 𝐼)    &   ⊢ 𝑈 = (𝑅 /s ∼ )    &   ⊢ 𝐼 = ((RSpan‘𝑅)‘{𝑀})    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑀 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝑈))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 (𝑋 = [𝑥] ∼ ∧ 𝑋 = {𝑧 ∣ ∃𝑦 ∈ 𝐵 𝑧 = (𝑥 + (𝑦 · 𝑀))}))
Theorem	ply1divalg3 36155*	Uniqueness of polynomial remainder: convert the subtraction in ply1divalg2 26333 to addition. (Contributed by SN, 20-Jun-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ + = (+g‘𝑃)    &   ⊢ ∙ = (.r‘𝑃)    &   ⊢ 𝐶 = (Unic1p‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐶)    ⇒   ⊢ (𝜑 → ∃!𝑞 ∈ 𝐵 (𝐷‘(𝐹 + (𝑞 ∙ 𝐺))) < (𝐷‘𝐺))
Theorem	r1peuqusdeg1 36156*	Uniqueness of polynomial remainder in terms of a quotient structure in the sense of the right hand side of r1pid2 26356. (Contributed by SN, 21-Jun-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐼 = ((RSpan‘𝑃)‘{𝐹})    &   ⊢ 𝑇 = (𝑃 /s (𝑃 ~QG 𝐼))    &   ⊢ 𝑄 = (Base‘𝑇)    &   ⊢ 𝑁 = (Unic1p‘𝑅)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Domn)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑁)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑄)    ⇒   ⊢ (𝜑 → ∃!𝑞 ∈ 𝑍 (𝐷‘𝑞) < (𝐷‘𝐹))
Definition	df-sfl1 36157*	Temporary construction for the splitting field of a polynomial. The inputs are a field 𝑟 and a polynomial 𝑝 that we want to split, along with a tuple 𝑗 in the same format as the output. The output is a tuple ⟨𝑆, 𝐹⟩ where 𝑆 is the splitting field and 𝐹 is an injective homomorphism from the original field 𝑟. The function works by repeatedly finding the smallest monic irreducible factor, and extending the field by that factor using the polyFld construction. We keep track of a total order in each of the splitting fields so that we can pick an element definably without needing global choice. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ splitFld1 = (𝑟 ∈ V, 𝑗 ∈ V ↦ (𝑝 ∈ (Poly1‘𝑟) ↦ (rec((𝑠 ∈ V, 𝑓 ∈ V ↦ ⦋(Poly1‘𝑠) / 𝑚⦌⦋{𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠deg1𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩)), 𝑗)‘(card‘(1...(𝑟deg1𝑝))))))
Definition	df-sfl 36158*	Define the splitting field of a finite collection of polynomials, given a total ordered base field. The output is a tuple ⟨𝑆, 𝐹⟩ where 𝑆 is the totally ordered splitting field and 𝐹 is an injective homomorphism from the original field 𝑟. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ splitFld = (𝑟 ∈ V, 𝑝 ∈ V ↦ (℩𝑥∃𝑓(𝑓 Isom < , (lt‘𝑟)((1...(♯‘𝑝)), 𝑝) ∧ 𝑥 = (seq0((𝑒 ∈ V, 𝑔 ∈ V ↦ ((𝑟 splitFld1 𝑒)‘𝑔)), (𝑓 ∪ {⟨0, ⟨𝑟, ( I ↾ (Base‘𝑟))⟩⟩}))‘(♯‘𝑝)))))
Definition	df-psl 36159*	Define the direct limit of an increasing sequence of fields produced by pasting together the splitting fields for each sequence of polynomials. That is, given a ring 𝑟, a strict order on 𝑟, and a sequence 𝑝:ℕ⟶(𝒫 𝑟 ∩ Fin) of finite sets of polynomials to split, we construct the direct limit system of field extensions by splitting one set at a time and passing the resulting construction to HomLim. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ polySplitLim = (𝑟 ∈ V, 𝑝 ∈ ((𝒫 (Base‘𝑟) ∩ Fin) ↑m ℕ) ↦ ⦋(1st ∘ seq0((𝑔 ∈ V, 𝑞 ∈ V ↦ ⦋(1st ‘𝑔) / 𝑒⦌⦋(1st ‘𝑒) / 𝑠⦌⦋(𝑠 splitFld ran (𝑥 ∈ 𝑞 ↦ (𝑥 ∘ (2nd ‘𝑔)))) / 𝑓⦌⟨𝑓, ((2nd ‘𝑔) ∘ (2nd ‘𝑓))⟩), (𝑝 ∪ {⟨0, ⟨⟨𝑟, ∅⟩, ( I ↾ (Base‘𝑟))⟩⟩}))) / 𝑓⦌((1st ∘ (𝑓 shift 1)) HomLim (2nd ∘ 𝑓)))
21.6.17  p-adic number fields
Syntax	czr 36160	Integral elements of a ring.
class ZRing
Syntax	cgf 36161	Galois finite field.
class GF
Syntax	cgfo 36162	Galois limit field.
class GF∞
Syntax	ceqp 36163	Equivalence relation for df-qp 36174.
class ~Qp
Syntax	crqp 36164	Equivalence relation representatives for df-qp 36174.
class /Qp
Syntax	cqp 36165	The set of 𝑝-adic rational numbers.
class Qp
Syntax	czp 36166	The set of 𝑝-adic integers. (Not to be confused with czn 21689.)
class Zp
Syntax	cqpa 36167	Algebraic completion of the 𝑝-adic rational numbers.
class _Qp
Syntax	ccp 36168	Metric completion of _Qp.
class Cp
Definition	df-zrng 36169	Define the subring of integral elements in a ring. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ ZRing = (𝑟 ∈ V ↦ (𝑟 IntgRing ran (ℤRHom‘𝑟)))
Definition	df-gf 36170*	Define the Galois finite field of order 𝑝↑𝑛. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ GF = (𝑝 ∈ ℙ, 𝑛 ∈ ℕ ↦ ⦋(ℤ/nℤ‘𝑝) / 𝑟⦌(1st ‘(𝑟 splitFld {⦋(Poly1‘𝑟) / 𝑠⦌⦋(var1‘𝑟) / 𝑥⦌(((𝑝↑𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g‘𝑠)𝑥)})))
Definition	df-gfoo 36171*	Define the Galois field of order 𝑝↑+∞, as a direct limit of the Galois finite fields. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ GF∞ = (𝑝 ∈ ℙ ↦ ⦋(ℤ/nℤ‘𝑝) / 𝑟⦌(𝑟 polySplitLim (𝑛 ∈ ℕ ↦ {⦋(Poly1‘𝑟) / 𝑠⦌⦋(var1‘𝑟) / 𝑥⦌(((𝑝↑𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g‘𝑠)𝑥)})))
Definition	df-eqp 36172*	Define an equivalence relation on ℤ-indexed sequences of integers such that two sequences are equivalent iff the difference is equivalent to zero, and a sequence is equivalent to zero iff the sum Σ𝑘 ≤ 𝑛𝑓(𝑘)(𝑝↑𝑘) is a multiple of 𝑝↑(𝑛 + 1) for every 𝑛. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ ~Qp = (𝑝 ∈ ℙ ↦ {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ (ℤ ↑m ℤ) ∧ ∀𝑛 ∈ ℤ Σ𝑘 ∈ (ℤ≥‘-𝑛)(((𝑓‘-𝑘) − (𝑔‘-𝑘)) / (𝑝↑(𝑘 + (𝑛 + 1)))) ∈ ℤ)})
Definition	df-rqp 36173*	There is a unique element of (ℤ ↑m (0...(𝑝 − 1))) ~Qp -equivalent to any element of (ℤ ↑m ℤ), if the sequences are zero for sufficiently large negative values; this function selects that element. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ /Qp = (𝑝 ∈ ℙ ↦ (~Qp ∩ ⦋{𝑓 ∈ (ℤ ↑m ℤ) ∣ ∃𝑥 ∈ ran ℤ≥(◡𝑓 “ (ℤ ∖ {0})) ⊆ 𝑥} / 𝑦⦌(𝑦 × (𝑦 ∩ (ℤ ↑m (0...(𝑝 − 1)))))))
Definition	df-qp 36174*	Define the 𝑝-adic completion of the rational numbers, as a normed field structure with a total order (that is not compatible with the operations). (Contributed by Mario Carneiro, 2-Dec-2014.) (Revised by AV, 10-Oct-2021.)
⊢ Qp = (𝑝 ∈ ℙ ↦ ⦋{ℎ ∈ (ℤ ↑m (0...(𝑝 − 1))) ∣ ∃𝑥 ∈ ran ℤ≥(◡ℎ “ (ℤ ∖ {0})) ⊆ 𝑥} / 𝑏⦌(({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑓 ∘f + 𝑔)))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓‘𝑘) · (𝑔‘(𝑛 − 𝑘))))))⟩} ∪ {⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))}⟩}) toNrmGrp (𝑓 ∈ 𝑏 ↦ if(𝑓 = (ℤ × {0}), 0, (𝑝↑-inf((◡𝑓 “ (ℤ ∖ {0})), ℝ, < ))))))
Definition	df-zp 36175	Define the 𝑝-adic integers, as a subset of the 𝑝-adic rationals. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ Zp = (ZRing ∘ Qp)
Definition	df-qpa 36176*	Define the completion of the 𝑝-adic rationals. Here we simply define it as the splitting field of a dense sequence of polynomials (using as the 𝑛-th set the collection of polynomials with degree less than 𝑛 and with coefficients < (𝑝↑𝑛)). Krasner's lemma will then show that all monic polynomials have splitting fields isomorphic to a sufficiently close Eisenstein polynomial from the list, and unramified extensions are generated by the polynomial 𝑥↑(𝑝↑𝑛) − 𝑥, which is in the list. Thus, every finite extension of Qp is a subfield of this field extension, so it is algebraically closed. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ _Qp = (𝑝 ∈ ℙ ↦ ⦋(Qp‘𝑝) / 𝑟⦌(𝑟 polySplitLim (𝑛 ∈ ℕ ↦ {𝑓 ∈ (Poly1‘𝑟) ∣ ((𝑟deg1𝑓) ≤ 𝑛 ∧ ∀𝑑 ∈ ran (coe1‘𝑓)(◡𝑑 “ (ℤ ∖ {0})) ⊆ (0...𝑛))})))
Definition	df-cp 36177	Define the metric completion of the algebraic completion of the 𝑝 -adic rationals. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ Cp = ( cplMetSp ∘ _Qp)
21.7  Mathbox for Filip Cernatescu I hope someone will enjoy solving (proving) the simple equations, inequalities, and calculations from this mathbox. I have proved these problems (theorems) using the Milpgame proof assistant. (It can be downloaded from https://us.metamath.org/other/milpgame/milpgame.html.)
Theorem	problem1 36178	Practice problem 1. Clues: 5p4e9 12416 3p2e5 12409 eqtri 2789 oveq1i 7433. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Proof modification is discouraged.)
⊢ ((3 + 2) + 4) = 9
Theorem	problem2 36179	Practice problem 2. Clues: oveq12i 7435 adddiri 11240 add4i 11453 mulcli 11234 recni 11241 2re 12333 3eqtri 2793 10re 12752 5re 12346 1re 11226 4re 12343 eqcomi 2775 5p4e9 12416 oveq1i 7433 df-3 12322. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Revised by AV, 9-Sep-2021.) (Proof modification is discouraged.)
⊢ (((2 · ;10) + 5) + ((1 · ;10) + 4)) = ((3 · ;10) + 9)
Theorem	problem3 36180	Practice problem 3. Clues: eqcomi 2775 eqtri 2789 subaddrii 11565 recni 11241 4re 12343 3re 12339 1re 11226 df-4 12323 addcomi 11419. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ ℂ    &   ⊢ (𝐴 + 3) = 4    ⇒   ⊢ 𝐴 = 1
Theorem	problem4 36181	Practice problem 4. Clues: pm3.2i 476 eqcomi 2775 eqtri 2789 subaddrii 11565 recni 11241 7re 12352 6re 12349 ax-1cn 11176 df-7 12326 ax-mp 5 oveq1i 7433 3cn 12340 2cn 12334 df-3 12322 mullidi 11232 subdiri 11682 mp3an 1490 mulcli 11234 subadd23 11487 oveq2i 7434 oveq12i 7435 3t2e6 12424 mulcomi 11235 subcli 11552 biimpri 231 subadd2i 11564. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ (𝐴 + 𝐵) = 3    &   ⊢ ((3 · 𝐴) + (2 · 𝐵)) = 7    ⇒   ⊢ (𝐴 = 1 ∧ 𝐵 = 2)
Theorem	problem5 36182	Practice problem 5. Clues: 3brtr3i 5145 mpbi 233 breqtri 5141 ltaddsubi 11793 remulcli 11243 2re 12333 3re 12339 9re 12358 eqcomi 2775 mvlladdi 11494 3cn 6cn 12350 eqtr3i 2791 6p3e9 12418 addcomi 11419 ltdiv1ii 12162 6re 12349 nngt0i 12293 2nn 12332 divcan3i 11979 recni 11241 2cn 12334 2ne0 12365 mpbir 234 eqtri 2789 mulcomi 11235 3t2e6 12424 divmuli 11987. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ ℝ    &   ⊢ ((2 · 𝐴) + 3) < 9    ⇒   ⊢ 𝐴 < 3
Theorem	quad3 36183	Variant of quadratic equation with discriminant expanded. (Contributed by Filip Cernatescu, 19-Oct-2019.)
⊢ 𝑋 ∈ ℂ    &   ⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐴 ≠ 0    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) = 0    ⇒   ⊢ (𝑋 = ((-𝐵 + (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴)) ∨ 𝑋 = ((-𝐵 − (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴)))
21.8  Mathbox for Paul Chapman
21.8.1  Real and complex numbers (cont.)
Theorem	climuzcnv 36184*	Utility lemma to convert between 𝑚 ≤ 𝑘 and 𝑘 ∈ (ℤ≥‘𝑚) in limit theorems. (Contributed by Paul Chapman, 10-Nov-2012.)
⊢ (𝑚 ∈ ℕ → ((𝑘 ∈ (ℤ≥‘𝑚) → 𝜑) ↔ (𝑘 ∈ ℕ → (𝑚 ≤ 𝑘 → 𝜑))))
Theorem	sinccvglem 36185*	((sin‘𝑥) / 𝑥) ⇝ 1 as (real) 𝑥 ⇝ 0. (Contributed by Paul Chapman, 10-Nov-2012.) (Revised by Mario Carneiro, 21-May-2014.)
⊢ (𝜑 → 𝐹:ℕ⟶(ℝ ∖ {0}))    &   ⊢ (𝜑 → 𝐹 ⇝ 0)    &   ⊢ 𝐺 = (𝑥 ∈ (ℝ ∖ {0}) ↦ ((sin‘𝑥) / 𝑥))    &   ⊢ 𝐻 = (𝑥 ∈ ℂ ↦ (1 − ((𝑥↑2) / 3)))    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (abs‘(𝐹‘𝑘)) < 1)    ⇒   ⊢ (𝜑 → (𝐺 ∘ 𝐹) ⇝ 1)
Theorem	sinccvg 36186*	((sin‘𝑥) / 𝑥) ⇝ 1 as (real) 𝑥 ⇝ 0. (Contributed by Paul Chapman, 10-Nov-2012.) (Proof shortened by Mario Carneiro, 21-May-2014.)
⊢ ((𝐹:ℕ⟶(ℝ ∖ {0}) ∧ 𝐹 ⇝ 0) → ((𝑥 ∈ (ℝ ∖ {0}) ↦ ((sin‘𝑥) / 𝑥)) ∘ 𝐹) ⇝ 1)
Theorem	circum 36187*	The circumference of a circle of radius 𝑅, defined as the limit as 𝑛 ⇝ +∞ of the perimeter of an inscribed n-sided isogons, is ((2 · π) · 𝑅). (Contributed by Paul Chapman, 10-Nov-2012.) (Proof shortened by Mario Carneiro, 21-May-2014.)
⊢ 𝐴 = ((2 · π) / 𝑛)    &   ⊢ 𝑃 = (𝑛 ∈ ℕ ↦ ((2 · 𝑛) · (𝑅 · (sin‘(𝐴 / 2)))))    &   ⊢ 𝑅 ∈ ℝ    ⇒   ⊢ 𝑃 ⇝ ((2 · π) · 𝑅)
21.8.2  Miscellaneous theorems
Theorem	elfzm12 36188	Membership in a curtailed finite sequence of integers. (Contributed by Paul Chapman, 17-Nov-2012.)
⊢ (𝑁 ∈ ℕ → (𝑀 ∈ (1...(𝑁 − 1)) → 𝑀 ∈ (1...𝑁)))
Theorem	nn0seqcvg 36189*	A strictly-decreasing nonnegative integer sequence with initial term 𝑁 reaches zero by the 𝑁 th term. Inference version. (Contributed by Paul Chapman, 31-Mar-2011.)
⊢ 𝐹:ℕ0⟶ℕ0    &   ⊢ 𝑁 = (𝐹‘0)    &   ⊢ (𝑘 ∈ ℕ0 → ((𝐹‘(𝑘 + 1)) ≠ 0 → (𝐹‘(𝑘 + 1)) < (𝐹‘𝑘)))    ⇒   ⊢ (𝐹‘𝑁) = 0
Theorem	lediv2aALT 36190	Division of both sides of 'less than or equal to' by a nonnegative number. (Contributed by Paul Chapman, 7-Sep-2007.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (((𝐴 ∈ ℝ ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵) ∧ (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶)) → (𝐴 ≤ 𝐵 → (𝐶 / 𝐵) ≤ (𝐶 / 𝐴)))
Theorem	abs2sqlei 36191	The absolute values of two numbers compare as their squares. (Contributed by Paul Chapman, 7-Sep-2007.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ ((abs‘𝐴) ≤ (abs‘𝐵) ↔ ((abs‘𝐴)↑2) ≤ ((abs‘𝐵)↑2))
Theorem	abs2sqlti 36192	The absolute values of two numbers compare as their squares. (Contributed by Paul Chapman, 7-Sep-2007.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ ((abs‘𝐴) < (abs‘𝐵) ↔ ((abs‘𝐴)↑2) < ((abs‘𝐵)↑2))
Theorem	abs2sqle 36193	The absolute values of two numbers compare as their squares. (Contributed by Paul Chapman, 7-Sep-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((abs‘𝐴) ≤ (abs‘𝐵) ↔ ((abs‘𝐴)↑2) ≤ ((abs‘𝐵)↑2)))
Theorem	abs2sqlt 36194	The absolute values of two numbers compare as their squares. (Contributed by Paul Chapman, 7-Sep-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((abs‘𝐴) < (abs‘𝐵) ↔ ((abs‘𝐴)↑2) < ((abs‘𝐵)↑2)))
Theorem	abs2difi 36195	Difference of absolute values. (Contributed by Paul Chapman, 7-Sep-2007.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ ((abs‘𝐴) − (abs‘𝐵)) ≤ (abs‘(𝐴 − 𝐵))
Theorem	abs2difabsi 36196	Absolute value of difference of absolute values. (Contributed by Paul Chapman, 7-Sep-2007.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (abs‘((abs‘𝐴) − (abs‘𝐵))) ≤ (abs‘(𝐴 − 𝐵))
21.9  Mathbox for Hongxiu Chen
Theorem	2thALT 36197	Alternate proof of 2th 267. (Contributed by Hongxiu Chen, 29-Jun-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ 𝜓    ⇒   ⊢ (𝜑 ↔ 𝜓)
Theorem	orbi2iALT 36198	Alternate proof of orbi2i 926. (Contributed by Hongxiu Chen, 29-Jun-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ((𝜒 ∨ 𝜑) ↔ (𝜒 ∨ 𝜓))
Theorem	pm3.48ALT 36199	Alternate proof of pm3.48 978. (Contributed by Hongxiu Chen, 29-Jun-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((𝜑 → 𝜓) ∧ (𝜒 → 𝜃)) → ((𝜑 ∨ 𝜒) → (𝜓 ∨ 𝜃)))
Theorem	3jcadALT 36200	Alternate proof of 3jcad 1147. (Contributed by Hongxiu Chen, 29-Jun-2025.) (Proof modification is discouraged.) Use 3jcad instead. (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜓 → 𝜃))    &   ⊢ (𝜑 → (𝜓 → 𝜏))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃 ∧ 𝜏)))