P. 171 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 17001-17100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	prmgapprmolem 17001	Lemma for prmgapprmo 17002: The primorial of a number plus an integer greater than 1 and less than or equal to the number are not coprime. (Contributed by AV, 15-Aug-2020.) (Revised by AV, 29-Aug-2020.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (2...𝑁)) → 1 < (((#p‘𝑁) + 𝐼) gcd 𝐼))
Theorem	prmgapprmo 17002*	Alternate proof of prmgap 16999: in contrast to prmgap 16999, where the gap starts at n! , the factorial of n, the gap starts at n#, the primorial of n. (Contributed by AV, 15-Aug-2020.) (Revised by AV, 29-Aug-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∀𝑛 ∈ ℕ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑛 ≤ (𝑞 − 𝑝) ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ)
6.2.17  Decimal arithmetic (cont.)
Theorem	dec2dvds 17003	Divisibility by two is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ (𝐵 · 2) = 𝐶    &   ⊢ 𝐷 = (𝐶 + 1)    ⇒   ⊢ ¬ 2 ∥ ;𝐴𝐷
Theorem	dec5dvds 17004	Divisibility by five is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ    &   ⊢ 𝐵 < 5    ⇒   ⊢ ¬ 5 ∥ ;𝐴𝐵
Theorem	dec5dvds2 17005	Divisibility by five is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ    &   ⊢ 𝐵 < 5    &   ⊢ (5 + 𝐵) = 𝐶    ⇒   ⊢ ¬ 5 ∥ ;𝐴𝐶
Theorem	dec5nprm 17006	A decimal number greater than 10 and ending with five is not a prime number. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ 𝐴 ∈ ℕ    ⇒   ⊢ ¬ ;𝐴5 ∈ ℙ
Theorem	dec2nprm 17007	A decimal number greater than 10 and ending with an even digit is not a prime number. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ (𝐵 · 2) = 𝐶    ⇒   ⊢ ¬ ;𝐴𝐶 ∈ ℙ
Theorem	modxai 17008	Add exponents in a power mod calculation. (Contributed by Mario Carneiro, 21-Feb-2014.) (Revised by Mario Carneiro, 5-Feb-2015.)
⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℤ    &   ⊢ 𝐾 ∈ ℕ0    &   ⊢ 𝑀 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐿 ∈ ℕ0    &   ⊢ ((𝐴↑𝐵) mod 𝑁) = (𝐾 mod 𝑁)    &   ⊢ ((𝐴↑𝐶) mod 𝑁) = (𝐿 mod 𝑁)    &   ⊢ (𝐵 + 𝐶) = 𝐸    &   ⊢ ((𝐷 · 𝑁) + 𝑀) = (𝐾 · 𝐿)    ⇒   ⊢ ((𝐴↑𝐸) mod 𝑁) = (𝑀 mod 𝑁)
Theorem	mod2xi 17009	Double exponents in a power mod calculation. (Contributed by Mario Carneiro, 21-Feb-2014.)
⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℤ    &   ⊢ 𝐾 ∈ ℕ0    &   ⊢ 𝑀 ∈ ℕ0    &   ⊢ ((𝐴↑𝐵) mod 𝑁) = (𝐾 mod 𝑁)    &   ⊢ (2 · 𝐵) = 𝐸    &   ⊢ ((𝐷 · 𝑁) + 𝑀) = (𝐾 · 𝐾)    ⇒   ⊢ ((𝐴↑𝐸) mod 𝑁) = (𝑀 mod 𝑁)
Theorem	modxp1i 17010	Add one to an exponent in a power mod calculation. (Contributed by Mario Carneiro, 21-Feb-2014.)
⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℤ    &   ⊢ 𝐾 ∈ ℕ0    &   ⊢ 𝑀 ∈ ℕ0    &   ⊢ ((𝐴↑𝐵) mod 𝑁) = (𝐾 mod 𝑁)    &   ⊢ (𝐵 + 1) = 𝐸    &   ⊢ ((𝐷 · 𝑁) + 𝑀) = (𝐾 · 𝐴)    ⇒   ⊢ ((𝐴↑𝐸) mod 𝑁) = (𝑀 mod 𝑁)
Theorem	mod2xnegi 17011	Version of mod2xi 17009 with a negative mod value. (Contributed by Mario Carneiro, 21-Feb-2014.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℤ    &   ⊢ 𝐾 ∈ ℕ    &   ⊢ 𝑀 ∈ ℕ0    &   ⊢ 𝐿 ∈ ℕ0    &   ⊢ ((𝐴↑𝐵) mod 𝑁) = (𝐿 mod 𝑁)    &   ⊢ (2 · 𝐵) = 𝐸    &   ⊢ (𝐿 + 𝐾) = 𝑁    &   ⊢ ((𝐷 · 𝑁) + 𝑀) = (𝐾 · 𝐾)    ⇒   ⊢ ((𝐴↑𝐸) mod 𝑁) = (𝑀 mod 𝑁)
Theorem	modsubi 17012	Subtract from within a mod calculation. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝑀 ∈ ℕ0    &   ⊢ (𝐴 mod 𝑁) = (𝐾 mod 𝑁)    &   ⊢ (𝑀 + 𝐵) = 𝐾    ⇒   ⊢ ((𝐴 − 𝐵) mod 𝑁) = (𝑀 mod 𝑁)
Theorem	gcdi 17013	Calculate a GCD via Euclid's algorithm. (Contributed by Mario Carneiro, 19-Feb-2014.)
⊢ 𝐾 ∈ ℕ0    &   ⊢ 𝑅 ∈ ℕ0    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ (𝑁 gcd 𝑅) = 𝐺    &   ⊢ ((𝐾 · 𝑁) + 𝑅) = 𝑀    ⇒   ⊢ (𝑀 gcd 𝑁) = 𝐺
Theorem	gcdmodi 17014	Calculate a GCD via Euclid's algorithm. Theorem 5.6 in [ApostolNT] p. 109. (Contributed by Mario Carneiro, 19-Feb-2014.)
⊢ 𝐾 ∈ ℕ0    &   ⊢ 𝑅 ∈ ℕ0    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ (𝐾 mod 𝑁) = (𝑅 mod 𝑁)    &   ⊢ (𝑁 gcd 𝑅) = 𝐺    ⇒   ⊢ (𝐾 gcd 𝑁) = 𝐺
Theorem	numexp0 17015	Calculate an integer power. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ (𝐴↑0) = 1
Theorem	numexp1 17016	Calculate an integer power. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ (𝐴↑1) = 𝐴
Theorem	numexpp1 17017	Calculate an integer power. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝑀 ∈ ℕ0    &   ⊢ (𝑀 + 1) = 𝑁    &   ⊢ ((𝐴↑𝑀) · 𝐴) = 𝐶    ⇒   ⊢ (𝐴↑𝑁) = 𝐶
Theorem	numexp2x 17018	Double an integer power. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝑀 ∈ ℕ0    &   ⊢ (2 · 𝑀) = 𝑁    &   ⊢ (𝐴↑𝑀) = 𝐷    &   ⊢ (𝐷 · 𝐷) = 𝐶    ⇒   ⊢ (𝐴↑𝑁) = 𝐶
Theorem	decsplit0b 17019	Split a decimal number into two parts. Base case: 𝑁 = 0. (Contributed by Mario Carneiro, 16-Jul-2015.) (Revised by AV, 8-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ ((𝐴 · (;10↑0)) + 𝐵) = (𝐴 + 𝐵)
Theorem	decsplit0 17020	Split a decimal number into two parts. Base case: 𝑁 = 0. (Contributed by Mario Carneiro, 16-Jul-2015.) (Revised by AV, 8-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ ((𝐴 · (;10↑0)) + 0) = 𝐴
Theorem	decsplit1 17021	Split a decimal number into two parts. Base case: 𝑁 = 1. (Contributed by Mario Carneiro, 16-Jul-2015.) (Revised by AV, 8-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ ((𝐴 · (;10↑1)) + 𝐵) = ;𝐴𝐵
Theorem	decsplit 17022	Split a decimal number into two parts. Inductive step. (Contributed by Mario Carneiro, 16-Jul-2015.) (Revised by AV, 8-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝑀 ∈ ℕ0    &   ⊢ (𝑀 + 1) = 𝑁    &   ⊢ ((𝐴 · (;10↑𝑀)) + 𝐵) = 𝐶    ⇒   ⊢ ((𝐴 · (;10↑𝑁)) + ;𝐵𝐷) = ;𝐶𝐷
Theorem	karatsuba 17023	The Karatsuba multiplication algorithm. If 𝑋 and 𝑌 are decomposed into two groups of digits of length 𝑀 (only the lower group is known to be this size but the algorithm is most efficient when the partition is chosen near the middle of the digit string), then 𝑋𝑌 can be written in three groups of digits, where each group needs only one multiplication. Thus, we can halve both inputs with only three multiplications on the smaller operands, yielding an asymptotic improvement of n^(log2 3) instead of n^2 for the "naive" algorithm decmul1c 12684. (Contributed by Mario Carneiro, 16-Jul-2015.) (Revised by AV, 9-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝑆 ∈ ℕ0    &   ⊢ 𝑀 ∈ ℕ0    &   ⊢ (𝐴 · 𝐶) = 𝑅    &   ⊢ (𝐵 · 𝐷) = 𝑇    &   ⊢ ((𝐴 + 𝐵) · (𝐶 + 𝐷)) = ((𝑅 + 𝑆) + 𝑇)    &   ⊢ ((𝐴 · (;10↑𝑀)) + 𝐵) = 𝑋    &   ⊢ ((𝐶 · (;10↑𝑀)) + 𝐷) = 𝑌    &   ⊢ ((𝑅 · (;10↑𝑀)) + 𝑆) = 𝑊    &   ⊢ ((𝑊 · (;10↑𝑀)) + 𝑇) = 𝑍    ⇒   ⊢ (𝑋 · 𝑌) = 𝑍
Theorem	2exp4 17024	Two to the fourth power is 16. (Contributed by Mario Carneiro, 20-Apr-2015.)
⊢ (2↑4) = ;16
Theorem	2exp5 17025	Two to the fifth power is 32. (Contributed by AV, 16-Aug-2021.)
⊢ (2↑5) = ;32
Theorem	2exp6 17026	Two to the sixth power is 64. (Contributed by Mario Carneiro, 20-Apr-2015.) (Proof shortened by OpenAI, 25-Mar-2020.)
⊢ (2↑6) = ;64
Theorem	2exp7 17027	Two to the seventh power is 128. (Contributed by AV, 16-Aug-2021.)
⊢ (2↑7) = ;;128
Theorem	2exp8 17028	Two to the eighth power is 256. (Contributed by Mario Carneiro, 20-Apr-2015.)
⊢ (2↑8) = ;;256
Theorem	2exp11 17029	Two to the eleventh power is 2048. (Contributed by AV, 16-Aug-2021.)
⊢ (2↑;11) = ;;;2048
Theorem	2exp16 17030	Two to the sixteenth power is 65536. (Contributed by Mario Carneiro, 20-Apr-2015.)
⊢ (2↑;16) = ;;;;65536
Theorem	3exp3 17031	Three to the third power is 27. (Contributed by Mario Carneiro, 20-Apr-2015.)
⊢ (3↑3) = ;27
Theorem	2expltfac 17032	The factorial grows faster than two to the power 𝑁. (Contributed by Mario Carneiro, 15-Sep-2016.)
⊢ (𝑁 ∈ (ℤ≥‘4) → (2↑𝑁) < (!‘𝑁))
6.2.18  Cyclical shifts of words (cont.)
Theorem	cshwsidrepsw 17033	If cyclically shifting a word of length being a prime number by a number of positions which is not divisible by the prime number results in the word itself, the word is a "repeated symbol word". (Contributed by AV, 18-May-2018.) (Revised by AV, 10-Nov-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) → ((𝐿 ∈ ℤ ∧ (𝐿 mod (♯‘𝑊)) ≠ 0 ∧ (𝑊 cyclShift 𝐿) = 𝑊) → 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊))))
Theorem	cshwsidrepswmod0 17034	If cyclically shifting a word of length being a prime number results in the word itself, the shift must be either by 0 (modulo the length of the word) or the word must be a "repeated symbol word". (Contributed by AV, 18-May-2018.) (Revised by AV, 10-Nov-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ ∧ 𝐿 ∈ ℤ) → ((𝑊 cyclShift 𝐿) = 𝑊 → ((𝐿 mod (♯‘𝑊)) = 0 ∨ 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)))))
Theorem	cshwshashlem1 17035*	If cyclically shifting a word of length being a prime number not consisting of identical symbols by at least one position (and not by as many positions as the length of the word), the result will not be the word itself. (Contributed by AV, 19-May-2018.) (Revised by AV, 8-Jun-2018.) (Revised by AV, 10-Nov-2018.)
⊢ (𝜑 → (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ))    ⇒   ⊢ ((𝜑 ∧ ∃𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0) ∧ 𝐿 ∈ (1..^(♯‘𝑊))) → (𝑊 cyclShift 𝐿) ≠ 𝑊)
Theorem	cshwshashlem2 17036*	If cyclically shifting a word of length being a prime number and not of identical symbols by different numbers of positions, the resulting words are different. (Contributed by Alexander van der Vekens, 19-May-2018.) (Revised by Alexander van der Vekens, 8-Jun-2018.)
⊢ (𝜑 → (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ))    ⇒   ⊢ ((𝜑 ∧ ∃𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0)) → ((𝐿 ∈ (0..^(♯‘𝑊)) ∧ 𝐾 ∈ (0..^(♯‘𝑊)) ∧ 𝐾 < 𝐿) → (𝑊 cyclShift 𝐿) ≠ (𝑊 cyclShift 𝐾)))
Theorem	cshwshashlem3 17037*	If cyclically shifting a word of length being a prime number and not of identical symbols by different numbers of positions, the resulting words are different. (Contributed by Alexander van der Vekens, 19-May-2018.) (Revised by Alexander van der Vekens, 8-Jun-2018.)
⊢ (𝜑 → (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ))    ⇒   ⊢ ((𝜑 ∧ ∃𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0)) → ((𝐿 ∈ (0..^(♯‘𝑊)) ∧ 𝐾 ∈ (0..^(♯‘𝑊)) ∧ 𝐾 ≠ 𝐿) → (𝑊 cyclShift 𝐿) ≠ (𝑊 cyclShift 𝐾)))
Theorem	cshwsdisj 17038*	The singletons resulting by cyclically shifting a given word of length being a prime number and not consisting of identical symbols is a disjoint collection. (Contributed by Alexander van der Vekens, 19-May-2018.) (Revised by Alexander van der Vekens, 8-Jun-2018.)
⊢ (𝜑 → (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ))    ⇒   ⊢ ((𝜑 ∧ ∃𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0)) → Disj 𝑛 ∈ (0..^(♯‘𝑊)){(𝑊 cyclShift 𝑛)})
Theorem	cshwsiun 17039*	The set of (different!) words resulting by cyclically shifting a given word is an indexed union. (Contributed by AV, 19-May-2018.) (Revised by AV, 8-Jun-2018.) (Proof shortened by AV, 8-Nov-2018.)
⊢ 𝑀 = {𝑤 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(♯‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤}    ⇒   ⊢ (𝑊 ∈ Word 𝑉 → 𝑀 = ∪ 𝑛 ∈ (0..^(♯‘𝑊)){(𝑊 cyclShift 𝑛)})
Theorem	cshwsex 17040*	The class of (different!) words resulting by cyclically shifting a given word is a set. (Contributed by AV, 8-Jun-2018.) (Revised by AV, 8-Nov-2018.)
⊢ 𝑀 = {𝑤 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(♯‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤}    ⇒   ⊢ (𝑊 ∈ Word 𝑉 → 𝑀 ∈ V)
Theorem	cshws0 17041*	The size of the set of (different!) words resulting by cyclically shifting an empty word is 0. (Contributed by AV, 8-Nov-2018.)
⊢ 𝑀 = {𝑤 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(♯‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤}    ⇒   ⊢ (𝑊 = ∅ → (♯‘𝑀) = 0)
Theorem	cshwrepswhash1 17042*	The size of the set of (different!) words resulting by cyclically shifting a nonempty "repeated symbol word" is 1. (Contributed by AV, 18-May-2018.) (Revised by AV, 8-Nov-2018.)
⊢ 𝑀 = {𝑤 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(♯‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤}    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑊 = (𝐴 repeatS 𝑁)) → (♯‘𝑀) = 1)
Theorem	cshwshashnsame 17043*	If a word (not consisting of identical symbols) has a length being a prime number, the size of the set of (different!) words resulting by cyclically shifting the original word equals the length of the original word. (Contributed by AV, 19-May-2018.) (Revised by AV, 10-Nov-2018.)
⊢ 𝑀 = {𝑤 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(♯‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤}    ⇒   ⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) → (∃𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0) → (♯‘𝑀) = (♯‘𝑊)))
Theorem	cshwshash 17044*	If a word has a length being a prime number, the size of the set of (different!) words resulting by cyclically shifting the original word equals the length of the original word or 1. (Contributed by AV, 19-May-2018.) (Revised by AV, 10-Nov-2018.)
⊢ 𝑀 = {𝑤 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(♯‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤}    ⇒   ⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) → ((♯‘𝑀) = (♯‘𝑊) ∨ (♯‘𝑀) = 1))
6.2.19  Specific prime numbers
Theorem	prmlem0 17045*	Lemma for prmlem1 17047 and prmlem2 17059. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ ((¬ 2 ∥ 𝑀 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁))    &   ⊢ (𝐾 ∈ ℙ → ¬ 𝐾 ∥ 𝑁)    &   ⊢ (𝐾 + 2) = 𝑀    ⇒   ⊢ ((¬ 2 ∥ 𝐾 ∧ 𝑥 ∈ (ℤ≥‘𝐾)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁))
Theorem	prmlem1a 17046*	A quick proof skeleton to show that the numbers less than 25 are prime, by trial division. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑁 ∈ ℕ    &   ⊢ 1 < 𝑁    &   ⊢ ¬ 2 ∥ 𝑁    &   ⊢ ¬ 3 ∥ 𝑁    &   ⊢ ((¬ 2 ∥ 5 ∧ 𝑥 ∈ (ℤ≥‘5)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁))    ⇒   ⊢ 𝑁 ∈ ℙ
Theorem	prmlem1 17047	A quick proof skeleton to show that the numbers less than 25 are prime, by trial division. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑁 ∈ ℕ    &   ⊢ 1 < 𝑁    &   ⊢ ¬ 2 ∥ 𝑁    &   ⊢ ¬ 3 ∥ 𝑁    &   ⊢ 𝑁 < ;25    ⇒   ⊢ 𝑁 ∈ ℙ
Theorem	5prm 17048	5 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.)
⊢ 5 ∈ ℙ
Theorem	6nprm 17049	6 is not a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ ¬ 6 ∈ ℙ
Theorem	7prm 17050	7 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.)
⊢ 7 ∈ ℙ
Theorem	8nprm 17051	8 is not a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ ¬ 8 ∈ ℙ
Theorem	9nprm 17052	9 is not a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ ¬ 9 ∈ ℙ
Theorem	10nprm 17053	10 is not a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
⊢ ¬ ;10 ∈ ℙ
Theorem	11prm 17054	11 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.)
⊢ ;11 ∈ ℙ
Theorem	13prm 17055	13 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.)
⊢ ;13 ∈ ℙ
Theorem	17prm 17056	17 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.)
⊢ ;17 ∈ ℙ
Theorem	19prm 17057	19 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.)
⊢ ;19 ∈ ℙ
Theorem	23prm 17058	23 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.)
⊢ ;23 ∈ ℙ
Theorem	prmlem2 17059	Our last proving session got as far as 25 because we started with the two "bootstrap" primes 2 and 3, and the next prime is 5, so knowing that 2 and 3 are prime and 4 is not allows to cover the numbers less than 5↑2 = 25. Additionally, nonprimes are "easy", so we can extend this range of known prime/nonprimes all the way until 29, which is the first prime larger than 25. Thus, in this lemma we extend another blanket out to 29↑2 = 841, from which we can prove even more primes. If we wanted, we could keep doing this, but the goal is Bertrand's postulate, and for that we only need a few large primes - we don't need to find them all, as we have been doing thus far. So after this blanket runs out, we'll have to switch to another method (see 1259prm 17075). As a side note, you can see the pattern of the primes in the indentation pattern of this lemma! (Contributed by Mario Carneiro, 18-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.)
⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑁 < ;;841    &   ⊢ 1 < 𝑁    &   ⊢ ¬ 2 ∥ 𝑁    &   ⊢ ¬ 3 ∥ 𝑁    &   ⊢ ¬ 5 ∥ 𝑁    &   ⊢ ¬ 7 ∥ 𝑁    &   ⊢ ¬ ;11 ∥ 𝑁    &   ⊢ ¬ ;13 ∥ 𝑁    &   ⊢ ¬ ;17 ∥ 𝑁    &   ⊢ ¬ ;19 ∥ 𝑁    &   ⊢ ¬ ;23 ∥ 𝑁    ⇒   ⊢ 𝑁 ∈ ℙ
Theorem	37prm 17060	37 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.)
⊢ ;37 ∈ ℙ
Theorem	43prm 17061	43 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.)
⊢ ;43 ∈ ℙ
Theorem	83prm 17062	83 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.)
⊢ ;83 ∈ ℙ
Theorem	139prm 17063	139 is a prime number. (Contributed by Mario Carneiro, 19-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.)
⊢ ;;139 ∈ ℙ
Theorem	163prm 17064	163 is a prime number. (Contributed by Mario Carneiro, 19-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.)
⊢ ;;163 ∈ ℙ
Theorem	317prm 17065	317 is a prime number. (Contributed by Mario Carneiro, 19-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.)
⊢ ;;317 ∈ ℙ
Theorem	631prm 17066	631 is a prime number. (Contributed by Mario Carneiro, 1-Mar-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.)
⊢ ;;631 ∈ ℙ
Theorem	prmo4 17067	The primorial of 4. (Contributed by AV, 28-Aug-2020.)
⊢ (#p‘4) = 6
Theorem	prmo5 17068	The primorial of 5. (Contributed by AV, 28-Aug-2020.)
⊢ (#p‘5) = ;30
Theorem	prmo6 17069	The primorial of 6. (Contributed by AV, 28-Aug-2020.)
⊢ (#p‘6) = ;30
6.2.20  Very large primes
Theorem	1259lem1 17070	Lemma for 1259prm 17075. Calculate a power mod. In decimal, we calculate 2↑16 = 52𝑁 + 68≡68 and 2↑17≡68 · 2 = 136 in this lemma. (Contributed by Mario Carneiro, 22-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) (Proof shortened by AV, 16-Sep-2021.)
⊢ 𝑁 = ;;;1259    ⇒   ⊢ ((2↑;17) mod 𝑁) = (;;136 mod 𝑁)
Theorem	1259lem2 17071	Lemma for 1259prm 17075. Calculate a power mod. In decimal, we calculate 2↑34 = (2↑17)↑2≡136↑2≡14𝑁 + 870. (Contributed by Mario Carneiro, 22-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) (Proof shortened by AV, 15-Sep-2021.)
⊢ 𝑁 = ;;;1259    ⇒   ⊢ ((2↑;34) mod 𝑁) = (;;870 mod 𝑁)
Theorem	1259lem3 17072	Lemma for 1259prm 17075. Calculate a power mod. In decimal, we calculate 2↑38 = 2↑34 · 2↑4≡870 · 16 = 11𝑁 + 71 and 2↑76 = (2↑34)↑2≡71↑2 = 4𝑁 + 5≡5. (Contributed by Mario Carneiro, 22-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) (Proof shortened by AV, 16-Sep-2021.)
⊢ 𝑁 = ;;;1259    ⇒   ⊢ ((2↑;76) mod 𝑁) = (5 mod 𝑁)
Theorem	1259lem4 17073	Lemma for 1259prm 17075. Calculate a power mod. In decimal, we calculate 2↑306 = (2↑76)↑4 · 4≡5↑4 · 4 = 2𝑁 − 18, 2↑612 = (2↑306)↑2≡18↑2 = 324, 2↑629 = 2↑612 · 2↑17≡324 · 136 = 35𝑁 − 1 and finally 2↑(𝑁 − 1) = (2↑629)↑2≡1↑2 = 1. (Contributed by Mario Carneiro, 22-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) (Proof shortened by AV, 16-Sep-2021.)
⊢ 𝑁 = ;;;1259    ⇒   ⊢ ((2↑(𝑁 − 1)) mod 𝑁) = (1 mod 𝑁)
Theorem	1259lem5 17074	Lemma for 1259prm 17075. Calculate the GCD of 2↑34 − 1≡869 with 𝑁 = 1259. (Contributed by Mario Carneiro, 22-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.)
⊢ 𝑁 = ;;;1259    ⇒   ⊢ (((2↑;34) − 1) gcd 𝑁) = 1
Theorem	1259prm 17075	1259 is a prime number. (Contributed by Mario Carneiro, 22-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.)
⊢ 𝑁 = ;;;1259    ⇒   ⊢ 𝑁 ∈ ℙ
Theorem	2503lem1 17076	Lemma for 2503prm 17079. Calculate a power mod. In decimal, we calculate 2↑18 = 512↑2 = 104𝑁 + 1832≡1832. (Contributed by Mario Carneiro, 3-Mar-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) (Proof shortened by AV, 16-Sep-2021.)
⊢ 𝑁 = ;;;2503    ⇒   ⊢ ((2↑;18) mod 𝑁) = (;;;1832 mod 𝑁)
Theorem	2503lem2 17077	Lemma for 2503prm 17079. Calculate a power mod. We calculate 2↑19 = 2↑18 · 2≡1832 · 2 = 𝑁 + 1161, 2↑38 = (2↑19)↑2≡1161↑2 = 538𝑁 + 1307, 2↑39 = 2↑38 · 2≡1307 · 2 = 𝑁 + 111, 2↑78 = (2↑39)↑2≡111↑2 = 5𝑁 − 194, 2↑156 = (2↑78)↑2≡194↑2 = 15𝑁 + 91, 2↑312 = (2↑156)↑2≡91↑2 = 3𝑁 + 772, 2↑624 = (2↑312)↑2≡772↑2 = 238𝑁 + 270, 2↑1248 = (2↑624)↑2≡270↑2 = 29𝑁 + 313, 2↑1251 = 2↑1248 · 8≡313 · 8 = 𝑁 + 1 and finally 2↑(𝑁 − 1) = (2↑1251)↑2≡1↑2 = 1. (Contributed by Mario Carneiro, 3-Mar-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) (Proof shortened by AV, 16-Sep-2021.)
⊢ 𝑁 = ;;;2503    ⇒   ⊢ ((2↑(𝑁 − 1)) mod 𝑁) = (1 mod 𝑁)
Theorem	2503lem3 17078	Lemma for 2503prm 17079. Calculate the GCD of 2↑18 − 1≡1831 with 𝑁 = 2503. (Contributed by Mario Carneiro, 3-Mar-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) (Proof shortened by AV, 15-Sep-2021.)
⊢ 𝑁 = ;;;2503    ⇒   ⊢ (((2↑;18) − 1) gcd 𝑁) = 1
Theorem	2503prm 17079	2503 is a prime number. (Contributed by Mario Carneiro, 3-Mar-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.)
⊢ 𝑁 = ;;;2503    ⇒   ⊢ 𝑁 ∈ ℙ
Theorem	4001lem1 17080	Lemma for 4001prm 17084. Calculate a power mod. In decimal, we calculate 2↑12 = 4096 = 𝑁 + 95, 2↑24 = (2↑12)↑2≡95↑2 = 2𝑁 + 1023, 2↑25 = 2↑24 · 2≡1023 · 2 = 2046, 2↑50 = (2↑25)↑2≡2046↑2 = 1046𝑁 + 1070, 2↑100 = (2↑50)↑2≡1070↑2 = 286𝑁 + 614 and 2↑200 = (2↑100)↑2≡614↑2 = 94𝑁 + 902 ≡902. (Contributed by Mario Carneiro, 3-Mar-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) (Proof shortened by AV, 16-Sep-2021.)
⊢ 𝑁 = ;;;4001    ⇒   ⊢ ((2↑;;200) mod 𝑁) = (;;902 mod 𝑁)
Theorem	4001lem2 17081	Lemma for 4001prm 17084. Calculate a power mod. In decimal, we calculate 2↑400 = (2↑200)↑2≡902↑2 = 203𝑁 + 1401 and 2↑800 = (2↑400)↑2≡1401↑2 = 490𝑁 + 2311 ≡2311. (Contributed by Mario Carneiro, 3-Mar-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) (Proof shortened by AV, 16-Sep-2021.)
⊢ 𝑁 = ;;;4001    ⇒   ⊢ ((2↑;;800) mod 𝑁) = (;;;2311 mod 𝑁)
Theorem	4001lem3 17082	Lemma for 4001prm 17084. Calculate a power mod. In decimal, we calculate 2↑1000 = 2↑800 · 2↑200≡2311 · 902 = 521𝑁 + 1 and finally 2↑(𝑁 − 1) = (2↑1000)↑4≡1↑4 = 1. (Contributed by Mario Carneiro, 3-Mar-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) (Proof shortened by AV, 16-Sep-2021.)
⊢ 𝑁 = ;;;4001    ⇒   ⊢ ((2↑(𝑁 − 1)) mod 𝑁) = (1 mod 𝑁)
Theorem	4001lem4 17083	Lemma for 4001prm 17084. Calculate the GCD of 2↑800 − 1≡2310 with 𝑁 = 4001. (Contributed by Mario Carneiro, 3-Mar-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) (Proof shortened by AV, 16-Sep-2021.)
⊢ 𝑁 = ;;;4001    ⇒   ⊢ (((2↑;;800) − 1) gcd 𝑁) = 1
Theorem	4001prm 17084	4001 is a prime number. (Contributed by Mario Carneiro, 3-Mar-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.) (Proof shortened by AV, 16-Sep-2021.)
⊢ 𝑁 = ;;;4001    ⇒   ⊢ 𝑁 ∈ ℙ
PART 7  BASIC STRUCTURES
7.1  Extensible structures
7.1.1  Basic definitions An "extensible structure" (or "structure" in short, at least in this section) is used to define a specific group, ring, poset, and so on. An extensible structure can contain many components. For example, a group will have at least two components (base set and operation), although it can be further specialized by adding other components such as a multiplicative operation for rings (and still remain a group per our definition). Thus, every ring is also a group. This extensible structure approach allows theorems from more general structures (such as groups) to be reused for more specialized structures (such as rings) without having to reprove anything. Structures are common in mathematics, but in informal (natural language) proofs the details are assumed in ways that we must make explicit. An extensible structure is implemented as a function (a set of ordered pairs) on a finite (and not necessarily sequential) subset of ℕ. The function's argument is the index of a structure component (such as 1 for the base set of a group), and its value is the component (such as the base set). By convention, we normally avoid direct reference to the hard-coded numeric index and instead use structure component extractors such as ndxid 17136 and strfv 17142. Using extractors makes it easier to change numeric indices and also makes the components' purpose clearer. For example, as noted in ndxid 17136, we can refer to a specific poset with base set 𝐵 and order relation 𝐿 using the extensible structure {⟨(Base‘ndx), 𝐵⟩, ⟨(le‘ndx), 𝐿⟩} rather than {⟨1, 𝐵⟩, ⟨;10, 𝐿⟩}. See section header comment mmtheorems.html#cnx 17136 for more details on numeric indices versus the structure component extractors. There are many other possible ways to handle structures. We chose this extensible structure approach because this approach (1) results in simpler notation than other approaches we are aware of, and (2) is easier to do proofs with. We cannot use an approach that uses "hidden" arguments; Metamath does not support hidden arguments, and in any case we want nothing hidden. It would be possible to use a categorical approach (e.g., something vaguely similar to Lean's mathlib). However, instances (the chain of proofs that an 𝑋 is a 𝑌 via a bunch of forgetful functors) can cause serious performance problems for automated tooling, and the resulting proofs would be painful to look at directly (in the case of Lean, they are long past the level where people would find it acceptable to look at them directly). Metamath is working under much stricter conditions than this, and it has still managed to achieve about the same level of flexibility through this "extensible structure" approach. To create a substructure of a given extensible structure, you can simply use the multifunction restriction operator for extensible structures ↾s as defined in df-ress 17170. This can be used to turn statements about rings into statements about subrings, modules into submodules, etc. This definition knows nothing about individual structures and merely truncates the Base set while leaving operators alone. Individual kinds of structures will need to handle this behavior by ignoring operators' values outside the range (like Ring), defining a function using the base set and applying that (like TopGrp), or explicitly truncating the slot before use (like MetSp). For example, the unital ring of integers ℤring is defined in df-zring 21414 as simply ℤring = (ℂfld ↾s ℤ). This can be similarly done for all other subsets of ℂ, which has all the structure we can show applies to it, and this all comes "for free". Should we come up with some new structure in the future that we wish ℂ to inherit, then we change the definition of ℂfld, reprove all the slot extraction theorems, add a new one, and that's it. None of the other downstream theorems have to change. Note that the construct of df-prds 17379 addresses a different situation. It is not possible to have SubGrp and SubRing be the same thing because they produce different outputs on the same input. The subgroups of an extensible structure treated as a group are not the same as the subrings of that same structure. With df-prds 17379 it can actually reasonably perform the task, that is, being the product group given a family of groups, while also being the product ring given a family of rings. There is no contradiction here because the group part of a product ring is a product group. There is also a general theory of "substructure algebras", in the form of df-mre 17517 and df-acs 17520. SubGrp is a Moore collection, as is SubRing, SubRng and many other substructure collections. But it is not useful for picking out a particular collection of interest; SubRing and SubGrp still need to be defined and they are distinct --- nothing is going to select these definitions for us. Extensible structures only work well when they represent concrete categories, where there is a "base set", morphisms are functions, and subobjects are subsets with induced operations. In short, they primarily work well for "sets with (some) extra structure". Extensible structures may not suffice for more complicated situations. For example, in manifolds, ↾s would not work. That said, extensible structures are sufficient for many of the structures that set.mm currently considers, and offer a good compromise for a goal-oriented formalization.
7.1.1.1  Extensible structures as structures with components
Syntax	cstr 17085	Extend class notation with the class of structures with components numbered below 𝐴.
class Struct
Definition	df-struct 17086*	Define a structure with components in 𝑀...𝑁. This is not a requirement for groups, posets, etc., but it is a useful assumption for component extraction theorems. As mentioned in the section header, an "extensible structure should be implemented as a function (a set of ordered pairs)". The current definition, however, is less restrictive: it allows for classes which contain the empty set ∅ to be extensible structures. Because of 0nelfun 6518, such classes cannot be functions. Without the empty set, however, a structure must be a function, see structn0fun 17090: 𝐹 Struct 𝑋 → Fun (𝐹 ∖ {∅}). Allowing an extensible structure to contain the empty set ensures that expressions like {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} are structures without asserting or implying that 𝐴, 𝐵, 𝐶 and 𝐷 are sets (if 𝐴 or 𝐵 is a proper class, then ⟨𝐴, 𝐵⟩ = ∅, see opprc 4854). This is used critically in strle1 17097, strle2 17098, strle3 17099 and strleun 17096 to avoid sethood hypotheses on the "payload" sets: without this, ipsstr 17268 and theorems like it will have many sethood assumptions, and may not even be usable in the empty context. Instead, the sethood assumption is deferred until it is actually needed, e.g., ipsbase 17269, which requires that the base set be a set but not any of the other components. Usually, a concrete structure like ℂfld does not contain the empty set, and therefore is a function, see cnfldfun 21335. (Contributed by Mario Carneiro, 29-Aug-2015.)
⊢ Struct = {⟨𝑓, 𝑥⟩ ∣ (𝑥 ∈ ( ≤ ∩ (ℕ × ℕ)) ∧ Fun (𝑓 ∖ {∅}) ∧ dom 𝑓 ⊆ (...‘𝑥))}
Theorem	brstruct 17087	The structure relation is a relation. (Contributed by Mario Carneiro, 29-Aug-2015.)
⊢ Rel Struct
Theorem	isstruct2 17088	The property of being a structure with components in (1st ‘𝑋)...(2nd ‘𝑋). (Contributed by Mario Carneiro, 29-Aug-2015.)
⊢ (𝐹 Struct 𝑋 ↔ (𝑋 ∈ ( ≤ ∩ (ℕ × ℕ)) ∧ Fun (𝐹 ∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋)))
Theorem	structex 17089	A structure is a set. (Contributed by AV, 10-Nov-2021.)
⊢ (𝐺 Struct 𝑋 → 𝐺 ∈ V)
Theorem	structn0fun 17090	A structure without the empty set is a function. (Contributed by AV, 13-Nov-2021.)
⊢ (𝐹 Struct 𝑋 → Fun (𝐹 ∖ {∅}))
Theorem	isstruct 17091	The property of being a structure with components in 𝑀...𝑁. (Contributed by Mario Carneiro, 29-Aug-2015.)
⊢ (𝐹 Struct ⟨𝑀, 𝑁⟩ ↔ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁) ∧ Fun (𝐹 ∖ {∅}) ∧ dom 𝐹 ⊆ (𝑀...𝑁)))
Theorem	structcnvcnv 17092	Two ways to express the relational part of a structure. (Contributed by Mario Carneiro, 29-Aug-2015.)
⊢ (𝐹 Struct 𝑋 → ◡◡𝐹 = (𝐹 ∖ {∅}))
Theorem	structfung 17093	The converse of the converse of a structure is a function. Closed form of structfun 17094. (Contributed by AV, 12-Nov-2021.)
⊢ (𝐹 Struct 𝑋 → Fun ◡◡𝐹)
Theorem	structfun 17094	Convert between two kinds of structure closure. (Contributed by Mario Carneiro, 29-Aug-2015.) (Proof shortened by AV, 12-Nov-2021.)
⊢ 𝐹 Struct 𝑋    ⇒   ⊢ Fun ◡◡𝐹
Theorem	structfn 17095	Convert between two kinds of structure closure. (Contributed by Mario Carneiro, 29-Aug-2015.)
⊢ 𝐹 Struct ⟨𝑀, 𝑁⟩    ⇒   ⊢ (Fun ◡◡𝐹 ∧ dom 𝐹 ⊆ (1...𝑁))
Theorem	strleun 17096	Combine two structures into one. (Contributed by Mario Carneiro, 29-Aug-2015.)
⊢ 𝐹 Struct ⟨𝐴, 𝐵⟩    &   ⊢ 𝐺 Struct ⟨𝐶, 𝐷⟩    &   ⊢ 𝐵 < 𝐶    ⇒   ⊢ (𝐹 ∪ 𝐺) Struct ⟨𝐴, 𝐷⟩
Theorem	strle1 17097	Make a structure from a singleton. (Contributed by Mario Carneiro, 29-Aug-2015.)
⊢ 𝐼 ∈ ℕ    &   ⊢ 𝐴 = 𝐼    ⇒   ⊢ {⟨𝐴, 𝑋⟩} Struct ⟨𝐼, 𝐼⟩
Theorem	strle2 17098	Make a structure from a pair. (Contributed by Mario Carneiro, 29-Aug-2015.)
⊢ 𝐼 ∈ ℕ    &   ⊢ 𝐴 = 𝐼    &   ⊢ 𝐼 < 𝐽    &   ⊢ 𝐽 ∈ ℕ    &   ⊢ 𝐵 = 𝐽    ⇒   ⊢ {⟨𝐴, 𝑋⟩, ⟨𝐵, 𝑌⟩} Struct ⟨𝐼, 𝐽⟩
Theorem	strle3 17099	Make a structure from a triple. (Contributed by Mario Carneiro, 29-Aug-2015.)
⊢ 𝐼 ∈ ℕ    &   ⊢ 𝐴 = 𝐼    &   ⊢ 𝐼 < 𝐽    &   ⊢ 𝐽 ∈ ℕ    &   ⊢ 𝐵 = 𝐽    &   ⊢ 𝐽 < 𝐾    &   ⊢ 𝐾 ∈ ℕ    &   ⊢ 𝐶 = 𝐾    ⇒   ⊢ {⟨𝐴, 𝑋⟩, ⟨𝐵, 𝑌⟩, ⟨𝐶, 𝑍⟩} Struct ⟨𝐼, 𝐾⟩
Theorem	sbcie2s 17100*	A special version of class substitution commonly used for structures. (Contributed by Thierry Arnoux, 14-Mar-2019.) (Revised by SN, 2-Mar-2025.)
⊢ 𝐴 = (𝐸‘𝑊)    &   ⊢ 𝐵 = (𝐹‘𝑊)    &   ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝑤 = 𝑊 → ([(𝐸‘𝑤) / 𝑎][(𝐹‘𝑤) / 𝑏]𝜑 ↔ 𝜓))