P. 415 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 41401-41500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	pfxtrcfv 41401	A symbol in a word truncated by one symbol. Could replace swrdtrcfv 13441. (Contributed by AV, 3-May-2020.)
|- ( ( W e. Word V /\ W =/= (/) /\ I e. ( 0..^ ( ( # ` W ) - 1 ) ) ) -> ( ( W prefix ( ( # ` W ) - 1 ) ) ` I ) = ( W ` I ) )
Theorem	pfxtrcfv0 41402	The first symbol in a word truncated by one symbol. Could replace swrdtrcfv0 13442. (Contributed by AV, 3-May-2020.)
|- ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> ( ( W prefix ( ( # ` W ) - 1 ) ) ` 0 ) = ( W ` 0 ) )
Theorem	pfxfvlsw 41403	The last symbol in a (not empty) prefix of a word. Could replace swrd0fvlsw 13443. (Contributed by AV, 3-May-2020.)
|- ( ( W e. Word V /\ L e. ( 1 ... ( # ` W ) ) ) -> ( lastS ` ( W prefix L ) ) = ( W ` ( L - 1 ) ) )
Theorem	pfxeq 41404*	The prefixes of two words are equal iff they have the same length and the same symbols at each position. Could replace swrdeq 13444. (Contributed by AV, 4-May-2020.)
|- ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( M <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) -> ( ( W prefix M ) = ( U prefix N ) <-> ( M = N /\ A. i e. ( 0..^ M ) ( W ` i ) = ( U ` i ) ) ) )
Theorem	pfxtrcfvl 41405	The last symbol in a word truncated by one symbol. Could replace swrdtrcfvl 13450. (Contributed by AV, 5-May-2020.)
|- ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> ( lastS ` ( W prefix ( ( # ` W ) - 1 ) ) ) = ( W ` ( ( # ` W ) - 2 ) ) )
Theorem	pfxsuffeqwrdeq 41406	Two words are equal if and only if they have the same prefix and the same suffix. Could replace 2swrdeqwrdeq 13453. (Contributed by AV, 5-May-2020.)
|- ( ( W e. Word V /\ S e. Word V /\ I e. ( 0..^ ( # ` W ) ) ) -> ( W = S <-> ( ( # ` W ) = ( # ` S ) /\ ( ( W prefix I ) = ( S prefix I ) /\ ( W substr <. I , ( # ` W ) >. ) = ( S substr <. I , ( # ` W ) >. ) ) ) ) )
Theorem	pfxsuff1eqwrdeq 41407	Two (nonempty) words are equal if and only if they have the same prefix and the same single symbol suffix. Could replace 2swrd1eqwrdeq 13454. (Contributed by AV, 6-May-2020.)
|- ( ( W e. Word V /\ U e. Word V /\ 0 < ( # ` W ) ) -> ( W = U <-> ( ( # ` W ) = ( # ` U ) /\ ( ( W prefix ( ( # ` W ) - 1 ) ) = ( U prefix ( ( # ` W ) - 1 ) ) /\ ( lastS ` W ) = ( lastS ` U ) ) ) ) )
Theorem	disjwrdpfx 41408*	Sets of words are disjoint if each set contains extensions of distinct words of a fixed length. Could replace disjxwrd 13455. (Contributed by AV, 6-May-2020.)
|- Disj y e. W { x e. Word V | ( x prefix N ) = y }
Theorem	ccatpfx 41409	Joining a prefix with an adjacent subword makes a longer prefix. (Contributed by AV, 7-May-2020.)
|- ( ( S e. Word A /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) -> ( ( S prefix Y ) ++ ( S substr <. Y , Z >. ) ) = ( S prefix Z ) )
Theorem	pfxccat1 41410	Recover the left half of a concatenated word. Could replace swrdccat1 13457. (Contributed by AV, 6-May-2020.)
|- ( ( S e. Word B /\ T e. Word B ) -> ( ( S ++ T ) prefix ( # ` S ) ) = S )
Theorem	pfx1 41411	A prefix of length 1. (Contributed by AV, 15-May-2020.)
|- ( ( W e. Word V /\ W =/= (/) ) -> ( W prefix 1 ) = <" ( W ` 0 ) "> )
Theorem	pfx2 41412	A prefix of length 2. (Contributed by AV, 15-May-2020.)
|- ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> ( W prefix 2 ) = <" ( W ` 0 ) ( W ` 1 ) "> )
Theorem	pfxswrd 41413	A prefix of a subword. Could replace swrd0swrd 13461. (Contributed by AV, 8-May-2020.)
|- ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) -> ( L e. ( 0 ... ( N - M ) ) -> ( ( W substr <. M , N >. ) prefix L ) = ( W substr <. M , ( M + L ) >. ) ) )
Theorem	swrdpfx 41414	A subword of a prefix. Could replace swrdswrd0 13462. (Contributed by AV, 8-May-2020.)
|- ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) ) -> ( ( K e. ( 0 ... N ) /\ L e. ( K ... N ) ) -> ( ( W prefix N ) substr <. K , L >. ) = ( W substr <. K , L >. ) ) )
Theorem	pfxpfx 41415	A prefix of a prefix. Could replace swrd0swrd0 13463. (Contributed by AV, 8-May-2020.)
|- ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ L e. ( 0 ... N ) ) -> ( ( W prefix N ) prefix L ) = ( W prefix L ) )
Theorem	pfxpfxid 41416	A prefix of a prefix with the same length is the prefix. Could replace swrd0swrdid 13464. (Contributed by AV, 8-May-2020.)
|- ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) ) -> ( ( W prefix N ) prefix N ) = ( W prefix N ) )
Theorem	pfxcctswrd 41417	The concatenation of the prefix of a word and the rest of the word yields the word itself. Could replace wrdcctswrd 13465. (Contributed by AV, 9-May-2020.)
|- ( ( W e. Word V /\ M e. ( 0 ... ( # ` W ) ) ) -> ( ( W prefix M ) ++ ( W substr <. M , ( # ` W ) >. ) ) = W )
Theorem	lenpfxcctswrd 41418	The length of the concatenation of the prefix of a word and the rest of the word is the length of the word. Could replace lencctswrd 13466. (Contributed by AV, 9-May-2020.)
|- ( ( W e. Word V /\ M e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( ( W prefix M ) ++ ( W substr <. M , ( # ` W ) >. ) ) ) = ( # ` W ) )
Theorem	lenrevpfxcctswrd 41419	The length of the concatenation of the rest of a word and the prefix of the word is the length of the word. Could replace lenrevcctswrd 13467. (Contributed by AV, 9-May-2020.)
|- ( ( W e. Word V /\ M e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( ( W substr <. M , ( # ` W ) >. ) ++ ( W prefix M ) ) ) = ( # ` W ) )
Theorem	pfxlswccat 41420	Reconstruct a nonempty word from its prefix and last symbol. Could replace swrdccatwrd 13468. (Contributed by AV, 9-May-2020.)
|- ( ( W e. Word V /\ W =/= (/) ) -> ( ( W prefix ( ( # ` W ) - 1 ) ) ++ <" ( lastS ` W ) "> ) = W )
Theorem	ccats1pfxeq 41421	The last symbol of a word concatenated with the word with the last symbol removed having results in the word itself. Could replace ccats1swrdeq 13469. (Contributed by AV, 9-May-2020.)
|- ( ( W e. Word V /\ U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) -> ( W = ( U prefix ( # ` W ) ) -> U = ( W ++ <" ( lastS ` U ) "> ) ) )
Theorem	ccats1pfxeqrex 41422*	There exists a symbol such that its concatenation with the prefix obtained by deleting the last symbol of a nonempty word results in the word itself. Could replace ccats1swrdeqrex 13478. (Contributed by AV, 9-May-2020.)
|- ( ( W e. Word V /\ U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) -> ( W = ( U prefix ( # ` W ) ) -> E. s e. V U = ( W ++ <" s "> ) ) )
Theorem	pfxccatin12lem1 41423	Lemma 1 for pfxccatin12 41425. Could replace swrdccatin12lem2b 13486. (Contributed by AV, 9-May-2020.)
|- ( ( M e. ( 0 ... L ) /\ N e. ( L ... X ) ) -> ( ( K e. ( 0..^ ( N - M ) ) /\ -. K e. ( 0..^ ( L - M ) ) ) -> ( K - ( L - M ) ) e. ( 0..^ ( N - L ) ) ) )
Theorem	pfxccatin12lem2 41424	Lemma 2 for pfxccatin12 41425. Could replace swrdccatin12lem2 13489. (Contributed by AV, 9-May-2020.)
|- L = ( # ` A )   =>    |- ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( ( K e. ( 0..^ ( N - M ) ) /\ -. K e. ( 0..^ ( L - M ) ) ) -> ( ( ( A ++ B ) substr <. M , N >. ) ` K ) = ( ( B prefix ( N - L ) ) ` ( K - ( # ` ( A substr <. M , L >. ) ) ) ) ) )
Theorem	pfxccatin12 41425	The subword of a concatenation of two words within both of the concatenated words. Could replace swrdccatin12 13491. (Contributed by AV, 9-May-2020.)
|- L = ( # ` A )   =>    |- ( ( A e. Word V /\ B e. Word V ) -> ( ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) -> ( ( A ++ B ) substr <. M , N >. ) = ( ( A substr <. M , L >. ) ++ ( B prefix ( N - L ) ) ) ) )
Theorem	pfxccat3 41426	The subword of a concatenation is either a subword of the first concatenated word or a subword of the second concatenated word or a concatenation of a suffix of the first word with a prefix of the second word. Could replace swrdccat3 13492. (Contributed by AV, 10-May-2020.)
|- L = ( # ` A )   =>    |- ( ( A e. Word V /\ B e. Word V ) -> ( ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( L + ( # ` B ) ) ) ) -> ( ( A ++ B ) substr <. M , N >. ) = if ( N <_ L , ( A substr <. M , N >. ) , if ( L <_ M , ( B substr <. ( M - L ) , ( N - L ) >. ) , ( ( A substr <. M , L >. ) ++ ( B prefix ( N - L ) ) ) ) ) ) )
Theorem	pfxccatpfx1 41427	A prefix of a concatenation being a prefix of the first concatenated word. (Contributed by AV, 10-May-2020.)
|- L = ( # ` A )   =>    |- ( ( A e. Word V /\ B e. Word V /\ N e. ( 0 ... L ) ) -> ( ( A ++ B ) prefix N ) = ( A prefix N ) )
Theorem	pfxccatpfx2 41428	A prefix of a concatenation of two words being the first word concatenated with a prefix of the second word. (Contributed by AV, 10-May-2020.)
|- L = ( # ` A )   &    |- M = ( # ` B )   =>    |- ( ( A e. Word V /\ B e. Word V /\ N e. ( ( L + 1 ) ... ( L + M ) ) ) -> ( ( A ++ B ) prefix N ) = ( A ++ ( B prefix ( N - L ) ) ) )
Theorem	pfxccat3a 41429	A prefix of a concatenation is either a prefix of the first concatenated word or a concatenation of the first word with a prefix of the second word. Could replace swrdccat3a 13494. (Contributed by AV, 10-May-2020.)
|- L = ( # ` A )   &    |- M = ( # ` B )   =>    |- ( ( A e. Word V /\ B e. Word V ) -> ( N e. ( 0 ... ( L + M ) ) -> ( ( A ++ B ) prefix N ) = if ( N <_ L , ( A prefix N ) , ( A ++ ( B prefix ( N - L ) ) ) ) ) )
Theorem	pfxccatid 41430	A prefix of a concatenation of length of the first concatenated word is the first word itself. Could replace swrdccatid 13497. (Contributed by AV, 10-May-2020.)
|- ( ( A e. Word V /\ B e. Word V /\ N = ( # ` A ) ) -> ( ( A ++ B ) prefix N ) = A )
Theorem	ccats1pfxeqbi 41431	A word is a prefix of a word with length greater by 1 than the first word iff the second word is the first word concatenated with the last symbol of the second word. Could replace ccats1swrdeqbi 13498. (Contributed by AV, 10-May-2020.)
|- ( ( W e. Word V /\ U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) -> ( W = ( U prefix ( # ` W ) ) <-> U = ( W ++ <" ( lastS ` U ) "> ) ) )
Theorem	pfxccatin12d 41432	The subword of a concatenation of two words within both of the concatenated words. Could replace swrdccatin12d 13501. (Contributed by AV, 10-May-2020.)
|- ( ph -> ( # ` A ) = L )   &    |- ( ph -> ( A e. Word V /\ B e. Word V ) )   &    |- ( ph -> M e. ( 0 ... L ) )   &    |- ( ph -> N e. ( L ... ( L + ( # ` B ) ) ) )   =>    |- ( ph -> ( ( A ++ B ) substr <. M , N >. ) = ( ( A substr <. M , L >. ) ++ ( B prefix ( N - L ) ) ) )
Theorem	reuccatpfxs1lem 41433*	Lemma for reuccatpfxs1 41434. Could replace reuccats1lem 13479. (Contributed by AV, 9-May-2020.)
|- ( ( ( W e. Word V /\ U e. X ) /\ A. s e. V ( ( W ++ <" s "> ) e. X -> S = s ) /\ A. x e. X ( x e. Word V /\ ( # ` x ) = ( ( # ` W ) + 1 ) ) ) -> ( W = ( U prefix ( # ` W ) ) -> U = ( W ++ <" S "> ) ) )
Theorem	reuccatpfxs1 41434*	There is a unique word having the length of a given word increased by 1 with the given word as prefix if there is a unique symbol which extends the given word. Could replace reuccats1 13480. (Contributed by AV, 10-May-2020.)
|- ( ( W e. Word V /\ A. x e. X ( x e. Word V /\ ( # ` x ) = ( ( # ` W ) + 1 ) ) ) -> ( E! v e. V ( W ++ <" v "> ) e. X -> E! w e. X W = ( w prefix ( # ` W ) ) ) )
Theorem	splvalpfx 41435	Value of the substring replacement operator. (Contributed by AV, 11-May-2020.)
|- ( ( S e. V /\ ( F e. NN0 /\ T e. X /\ R e. Y ) ) -> ( S splice <. F , T , R >. ) = ( ( ( S prefix F ) ++ R ) ++ ( S substr <. T , ( # ` S ) >. ) ) )
Theorem	repswpfx 41436	A prefix of a repeated symbol word is a repeated symbol word. (Contributed by AV, 11-May-2020.)
|- ( ( S e. V /\ N e. NN0 /\ L e. ( 0 ... N ) ) -> ( ( S repeatS N ) prefix L ) = ( S repeatS L ) )
Theorem	cshword2 41437	Perform a cyclical shift for a word. (Contributed by AV, 11-May-2020.)
|- ( ( W e. Word V /\ N e. ZZ ) -> ( W cyclShift N ) = ( ( W substr <. ( N mod ( # ` W ) ) , ( # ` W ) >. ) ++ ( W prefix ( N mod ( # ` W ) ) ) ) )
Theorem	pfxco 41438	Mapping of words commutes with the prefix operation. (Contributed by AV, 15-May-2020.)
|- ( ( W e. Word A /\ N e. ( 0 ... ( # ` W ) ) /\ F : A --> B ) -> ( F o. ( W prefix N ) ) = ( ( F o. W ) prefix N ) )
20.35.7  Number theory (extension)
20.35.7.1  Fermat numbers At first, the (sequence of) Fermat numbers FermatNo (the n-th Fermat number is denoted as (FermatNo ` n )) is defined, see df-fmtno 41440, and basic theorems are provided. Afterwards, it is shown that the first five Fermat numbers are prime, the (first) five Fermat primes, see fmtnofz04prm 41489, but that the fifth Fermat number (counting starts at 0!) is not prime, see fmtno5nprm 41495. The fourth Fermat number (i.e., the fifth Fermat prime) (FermatNo ` 4 ) = ;;;; 6 5 5 3 7 is currently the biggest number proven to be prime in set.mm, see 65537prm 41488 (previously, it was ;;; 4 0 0 1, see 4001prm 15852). Another important result of this section is Goldbach's theorem goldbachth 41459, showing that two different Fermut numbers are coprime. By this, it can be proven that there is an infinite number of primes, see prminf2 41500. Finally, it is shown that every prime of the form ( ( 2 ^ k ) + 1 ) must be a Fermat number (i.e., a Fermat prime), see 2pwp1prmfmtno 41504.
Syntax	cfmtno 41439	Extend class notation with the Fermat numbers.
class FermatNo
Definition	df-fmtno 41440	Define the function that enumerates the Fermat numbers, see definition in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.)
|- FermatNo = ( n e. NN0 |-> ( ( 2 ^ ( 2 ^ n ) ) + 1 ) )
Theorem	fmtno 41441	The N th Fermat number. (Contributed by AV, 13-Jun-2021.)
|- ( N e. NN0 -> (FermatNo ` N ) = ( ( 2 ^ ( 2 ^ N ) ) + 1 ) )
Theorem	fmtnoge3 41442	Each Fermat number is greater than or equal to 3. (Contributed by AV, 4-Aug-2021.)
|- ( N e. NN0 -> (FermatNo ` N ) e. ( ZZ>= ` 3 ) )
Theorem	fmtnonn 41443	Each Fermat number is a positive integer. (Contributed by AV, 26-Jul-2021.) (Proof shortened by AV, 4-Aug-2021.)
|- ( N e. NN0 -> (FermatNo ` N ) e. NN )
Theorem	fmtnom1nn 41444	A Fermat number minus one is a power of a power of two. (Contributed by AV, 29-Jul-2021.)
|- ( N e. NN0 -> ( (FermatNo ` N ) - 1 ) = ( 2 ^ ( 2 ^ N ) ) )
Theorem	fmtnoodd 41445	Each Fermat number is odd. (Contributed by AV, 26-Jul-2021.)
|- ( N e. NN0 -> -. 2 || (FermatNo ` N ) )
Theorem	fmtnorn 41446*	A Fermat number is a function value of the enumeration of the Fermat numbers. (Contributed by AV, 3-Aug-2021.)
|- ( F e. ran FermatNo <-> E. n e. NN0 (FermatNo ` n ) = F )
Theorem	fmtnof1 41447	The enumeration of the Fermat numbers is a one-one function into the positive integers. (Contributed by AV, 3-Aug-2021.)
|- FermatNo : NN0 -1-1-> NN
Theorem	fmtnoinf 41448	The set of Fermat numbers is infinite. (Contributed by AV, 3-Aug-2021.)
|- ran FermatNo e/ Fin
Theorem	fmtnorec1 41449	The first recurrence relation for Fermat numbers, see Wikipedia "Fermat number", https://en.wikipedia.org/wiki/Fermat_number#Basic_properties, 22-Jul-2021. (Contributed by AV, 22-Jul-2021.)
|- ( N e. NN0 -> (FermatNo ` ( N + 1 ) ) = ( ( ( (FermatNo ` N ) - 1 ) ^ 2 ) + 1 ) )
Theorem	sqrtpwpw2p 41450	The floor of the square root of 2 to the power of 2 to the power of a positive integer plus a bounded nonnegative integer. (Contributed by AV, 28-Jul-2021.)
|- ( ( N e. NN /\ M e. NN0 /\ M < ( ( 2 ^ ( ( 2 ^ ( N - 1 ) ) + 1 ) ) + 1 ) ) -> ( |_ ` ( sqr ` ( ( 2 ^ ( 2 ^ N ) ) + M ) ) ) = ( 2 ^ ( 2 ^ ( N - 1 ) ) ) )
Theorem	fmtnosqrt 41451	The floor of the square root of a Fermat number. (Contributed by AV, 28-Jul-2021.)
|- ( N e. NN -> ( |_ ` ( sqr ` (FermatNo ` N ) ) ) = ( 2 ^ ( 2 ^ ( N - 1 ) ) ) )
Theorem	fmtno0 41452	The 0 th Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.)
|- (FermatNo ` 0 ) = 3
Theorem	fmtno1 41453	The 1 st Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.)
|- (FermatNo ` 1 ) = 5
Theorem	fmtnorec2lem 41454*	Lemma for fmtnorec2 41455 (induction step). (Contributed by AV, 29-Jul-2021.)
|- ( y e. NN0 -> ( (FermatNo ` ( y + 1 ) ) = ( prod_ n e. ( 0 ... y ) (FermatNo ` n ) + 2 ) -> (FermatNo ` ( ( y + 1 ) + 1 ) ) = ( prod_ n e. ( 0 ... ( y + 1 ) ) (FermatNo ` n ) + 2 ) ) )
Theorem	fmtnorec2 41455*	The second recurrence relation for Fermat numbers, see ProofWiki "Product of Sequence of Fermat Numbers plus 2", 29-Jul-2021, https://proofwiki.org/wiki/Product_of_Sequence_of_Fermat_Numbers_plus_2 or Wikipedia "Fermat number", 29-Jul-2021, https://en.wikipedia.org/wiki/Fermat_number#Basic_properties. (Contributed by AV, 29-Jul-2021.)
|- ( N e. NN0 -> (FermatNo ` ( N + 1 ) ) = ( prod_ n e. ( 0 ... N ) (FermatNo ` n ) + 2 ) )
Theorem	fmtnodvds 41456	Any Fermat number divides a greater Fermat number minus 2. Corrolary of fmtnorec2 41455, see ProofWiki "Product of Sequence of Fermat Numbers plus 2/Corollary", 31-Jul-2021. (Contributed by AV, 1-Aug-2021.)
|- ( ( N e. NN0 /\ M e. NN ) -> (FermatNo ` N ) || ( (FermatNo ` ( N + M ) ) - 2 ) )
Theorem	goldbachthlem1 41457	Lemma 1 for goldbachth 41459. (Contributed by AV, 1-Aug-2021.)
|- ( ( N e. NN0 /\ M e. NN0 /\ M < N ) -> (FermatNo ` M ) || ( (FermatNo ` N ) - 2 ) )
Theorem	goldbachthlem2 41458	Lemma 2 for goldbachth 41459. (Contributed by AV, 1-Aug-2021.)
|- ( ( N e. NN0 /\ M e. NN0 /\ M < N ) -> ( (FermatNo ` N ) gcd (FermatNo ` M ) ) = 1 )
Theorem	goldbachth 41459	Goldbach's theorem: Two different Fermat numbers are coprime. See ProofWiki "Goldbach's theorem", 31-Jul-2021, https://proofwiki.org/wiki/Goldbach%27s_Theorem or Wikipedia "Fermat number", 31-Jul-2021, https://en.wikipedia.org/wiki/Fermat_number#Basic_properties. (Contributed by AV, 1-Aug-2021.)
|- ( ( N e. NN0 /\ M e. NN0 /\ N =/= M ) -> ( (FermatNo ` N ) gcd (FermatNo ` M ) ) = 1 )
Theorem	fmtnorec3 41460*	The third recurrence relation for Fermat numbers, see Wikipedia "Fermat number", 31-Jul-2021, https://en.wikipedia.org/wiki/Fermat_number#Basic_properties. (Contributed by AV, 2-Aug-2021.)
|- ( N e. ( ZZ>= ` 2 ) -> (FermatNo ` N ) = ( (FermatNo ` ( N - 1 ) ) + ( ( 2 ^ ( 2 ^ ( N - 1 ) ) ) x. prod_ n e. ( 0 ... ( N - 2 ) ) (FermatNo ` n ) ) ) )
Theorem	fmtnorec4 41461	The fourth recurrence relation for Fermat numbers, see Wikipedia "Fermat number", 31-Jul-2021, https://en.wikipedia.org/wiki/Fermat_number#Basic_properties. (Contributed by AV, 31-Jul-2021.)
|- ( N e. ( ZZ>= ` 2 ) -> (FermatNo ` N ) = ( ( (FermatNo ` ( N - 1 ) ) ^ 2 ) - ( 2 x. ( ( (FermatNo ` ( N - 2 ) ) - 1 ) ^ 2 ) ) ) )
Theorem	fmtno2 41462	The 2 nd Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.)
|- (FermatNo ` 2 ) = ; 1 7
Theorem	fmtno3 41463	The 3 rd Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.)
|- (FermatNo ` 3 ) = ;; 2 5 7
Theorem	fmtno4 41464	The 4 th Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.)
|- (FermatNo ` 4 ) = ;;;; 6 5 5 3 7
Theorem	fmtno5lem1 41465	Lemma 1 for fmtno5 41469. (Contributed by AV, 22-Jul-2021.)
|- (;;;; 6 5 5 3 6 x. 6 ) = ;;;;; 3 9 3 2 1 6
Theorem	fmtno5lem2 41466	Lemma 2 for fmtno5 41469. (Contributed by AV, 22-Jul-2021.)
|- (;;;; 6 5 5 3 6 x. 5 ) = ;;;;; 3 2 7 6 8 0
Theorem	fmtno5lem3 41467	Lemma 3 for fmtno5 41469. (Contributed by AV, 22-Jul-2021.)
|- (;;;; 6 5 5 3 6 x. 3 ) = ;;;;; 1 9 6 6 0 8
Theorem	fmtno5lem4 41468	Lemma 4 for fmtno5 41469. (Contributed by AV, 30-Jul-2021.)
|- (;;;; 6 5 5 3 6 ^ 2 ) = ;;;;;;;;; 4 2 9 4 9 6 7 2 9 6
Theorem	fmtno5 41469	The 5 th Fermat number. (Contributed by AV, 30-Jul-2021.)
|- (FermatNo ` 5 ) = ;;;;;;;;; 4 2 9 4 9 6 7 2 9 7
Theorem	fmtno0prm 41470	The 0 th Fermat number is a prime (first Fermat prime). (Contributed by AV, 13-Jun-2021.)
|- (FermatNo ` 0 ) e. Prime
Theorem	fmtno1prm 41471	The 1 st Fermat number is a prime (second Fermat prime). (Contributed by AV, 13-Jun-2021.)
|- (FermatNo ` 1 ) e. Prime
Theorem	fmtno2prm 41472	The 2 nd Fermat number is a prime (third Fermat prime). (Contributed by AV, 13-Jun-2021.)
|- (FermatNo ` 2 ) e. Prime
Theorem	257prm 41473	257 is a prime number (the fourth Fermat prime). (Contributed by AV, 15-Jun-2021.)
|- ;; 2 5 7 e. Prime
Theorem	fmtno3prm 41474	The 3 rd Fermat number is a prime (fourth Fermat prime). (Contributed by AV, 15-Jun-2021.)
|- (FermatNo ` 3 ) e. Prime
Theorem	odz2prm2pw 41475	Any power of two is coprime to any prime not being two. (Contributed by AV, 25-Jul-2021.)
|- ( ( ( N e. NN /\ P e. ( Prime \ { 2 } ) ) /\ ( ( ( 2 ^ ( 2 ^ N ) ) mod P ) =/= 1 /\ ( ( 2 ^ ( 2 ^ ( N + 1 ) ) ) mod P ) = 1 ) ) -> ( ( odZ ` P ) ` 2 ) = ( 2 ^ ( N + 1 ) ) )
Theorem	fmtnoprmfac1lem 41476	Lemma for fmtnoprmfac1 41477: The order of 2 modulo a prime that divides the n-th Fermat number is 2^(n+1). (Contributed by AV, 25-Jul-2021.)
|- ( ( N e. NN /\ P e. ( Prime \ { 2 } ) /\ P || (FermatNo ` N ) ) -> ( ( odZ ` P ) ` 2 ) = ( 2 ^ ( N + 1 ) ) )
Theorem	fmtnoprmfac1 41477*	Divisor of Fermat number (special form of Euler's result, see fmtnofac1 41482): Let Fn be a Fermat number. Let p be a prime divisor of Fn. Then p is in the form: k*2^(n+1)+1 where k is a positive integer. (Contributed by AV, 25-Jul-2021.)
|- ( ( N e. NN /\ P e. Prime /\ P || (FermatNo ` N ) ) -> E. k e. NN P = ( ( k x. ( 2 ^ ( N + 1 ) ) ) + 1 ) )
Theorem	fmtnoprmfac2lem1 41478	Lemma for fmtnoprmfac2 41479. (Contributed by AV, 26-Jul-2021.)
|- ( ( N e. ( ZZ>= ` 2 ) /\ P e. ( Prime \ { 2 } ) /\ P || (FermatNo ` N ) ) -> ( ( 2 ^ ( ( P - 1 ) / 2 ) ) mod P ) = 1 )
Theorem	fmtnoprmfac2 41479*	Divisor of Fermat number (special form of Lucas' result, see fmtnofac2 41481): Let Fn be a Fermat number. Let p be a prime divisor of Fn. Then p is in the form: k*2^(n+2)+1 where k is a positive integer. (Contributed by AV, 26-Jul-2021.)
|- ( ( N e. ( ZZ>= ` 2 ) /\ P e. Prime /\ P || (FermatNo ` N ) ) -> E. k e. NN P = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) )
Theorem	fmtnofac2lem 41480*	Lemma for fmtnofac2 41481 (Induction step). (Contributed by AV, 30-Jul-2021.)
|- ( ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) -> ( ( ( ( N e. ( ZZ>= ` 2 ) /\ y || (FermatNo ` N ) ) -> E. k e. NN0 y = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) /\ ( ( N e. ( ZZ>= ` 2 ) /\ z || (FermatNo ` N ) ) -> E. k e. NN0 z = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) ) -> ( ( N e. ( ZZ>= ` 2 ) /\ ( y x. z ) || (FermatNo ` N ) ) -> E. k e. NN0 ( y x. z ) = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) ) ) )
Theorem	fmtnofac2 41481*	Divisor of Fermat number (Euler's Result refined by François Édouard Anatole Lucas), see fmtnofac1 41482: Let Fn be a Fermat number. Let m be divisor of Fn. Then m is in the form: k*2^(n+2)+1 where k is a nonnegative integer. (Contributed by AV, 30-Jul-2021.)
|- ( ( N e. ( ZZ>= ` 2 ) /\ M e. NN /\ M || (FermatNo ` N ) ) -> E. k e. NN0 M = ( ( k x. ( 2 ^ ( N + 2 ) ) ) + 1 ) )
Theorem	fmtnofac1 41482*	Divisor of Fermat number (Euler's Result), see ProofWiki "Divisor of Fermat Number/Euler's Result", 24-Jul-2021, https://proofwiki.org/wiki/Divisor_of_Fermat_Number/Euler's_Result): "Let Fn be a Fermat number. Let m be divisor of Fn. Then m is in the form: k*2^(n+1)+1 where k is a positive integer." Here, however, k must be a nonnegative integer, because k must be 0 to represent 1 (which is a divisor of Fn ). Historical Note: In 1747, Leonhard Paul Euler proved that a divisor of a Fermat number Fn is always in the form kx2^(n+1)+1. This was later refined to k*2^(n+2)+1 by François Édouard Anatole Lucas, see fmtnofac2 41481. (Contributed by AV, 30-Jul-2021.)
|- ( ( N e. NN /\ M e. NN /\ M || (FermatNo ` N ) ) -> E. k e. NN0 M = ( ( k x. ( 2 ^ ( N + 1 ) ) ) + 1 ) )
Theorem	fmtno4sqrt 41483	The floor of the square root of the fourth Fermat number is 256. (Contributed by AV, 28-Jul-2021.)
|- ( |_ ` ( sqr ` (FermatNo ` 4 ) ) ) = ;; 2 5 6
Theorem	fmtno4prmfac 41484	If P was a (prime) factor of the fourth Fermat number less than the square root of the fourth Fermat number, it would be either 65 or 129 or 193. (Contributed by AV, 28-Jul-2021.)
|- ( ( P e. Prime /\ P || (FermatNo ` 4 ) /\ P <_ ( |_ ` ( sqr ` (FermatNo ` 4 ) ) ) ) -> ( P = ; 6 5 \/ P = ;; 1 2 9 \/ P = ;; 1 9 3 ) )
Theorem	fmtno4prmfac193 41485	If P was a (prime) factor of the fourth Fermat number, it would be 193. (Contributed by AV, 28-Jul-2021.)
|- ( ( P e. Prime /\ P || (FermatNo ` 4 ) /\ P <_ ( |_ ` ( sqr ` (FermatNo ` 4 ) ) ) ) -> P = ;; 1 9 3 )
Theorem	fmtno4nprmfac193 41486	193 is not a (prime) factor of the fourth Fermat number. (Contributed by AV, 24-Jul-2021.)
|- -. ;; 1 9 3 || (FermatNo ` 4 )
Theorem	fmtno4prm 41487	The 4-th Fermat number (65537) is a prime (the fifth Fermat prime). (Contributed by AV, 28-Jul-2021.)
|- (FermatNo ` 4 ) e. Prime
Theorem	65537prm 41488	65537 is a prime number (the fifth Fermat prime). (Contributed by AV, 28-Jul-2021.)
|- ;;;; 6 5 5 3 7 e. Prime
Theorem	fmtnofz04prm 41489	The first five Fermat numbers are prime, see remark in [ApostolNT] p. 7. (Contributed by AV, 28-Jul-2021.)
|- ( N e. ( 0 ... 4 ) -> (FermatNo ` N ) e. Prime )
Theorem	fmtnole4prm 41490	The first five Fermat numbers are prime. (Contributed by AV, 28-Jul-2021.)
|- ( ( N e. NN0 /\ N <_ 4 ) -> (FermatNo ` N ) e. Prime )
Theorem	fmtno5faclem1 41491	Lemma 1 for fmtno5fac 41494. (Contributed by AV, 22-Jul-2021.)
|- (;;;;;; 6 7 0 0 4 1 7 x. 4 ) = ;;;;;;; 2 6 8 0 1 6 6 8
Theorem	fmtno5faclem2 41492	Lemma 2 for fmtno5fac 41494. (Contributed by AV, 22-Jul-2021.)
|- (;;;;;; 6 7 0 0 4 1 7 x. 6 ) = ;;;;;;; 4 0 2 0 2 5 0 2
Theorem	fmtno5faclem3 41493	Lemma 3 for fmtno5fac 41494. (Contributed by AV, 22-Jul-2021.)
|- (;;;;;;;; 4 0 2 0 2 5 0 2 0 + ;;;;;;; 2 6 8 0 1 6 6 8 ) = ;;;;;;;; 4 2 8 8 2 6 6 8 8
Theorem	fmtno5fac 41494	The factorisation of the 5 th Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 22-Jul-2021.)
|- (FermatNo ` 5 ) = (;;;;;; 6 7 0 0 4 1 7 x. ;; 6 4 1 )
Theorem	fmtno5nprm 41495	The 5 th Fermat number is a not a prime. (Contributed by AV, 22-Jul-2021.)
|- (FermatNo ` 5 ) e/ Prime
Theorem	prmdvdsfmtnof1lem1 41496*	Lemma 1 for prmdvdsfmtnof1 41499. (Contributed by AV, 3-Aug-2021.)
|- I = inf ( { p e. Prime | p || F } , RR , < )   &    |- J = inf ( { p e. Prime | p || G } , RR , < )   =>    |- ( ( F e. ( ZZ>= ` 2 ) /\ G e. ( ZZ>= ` 2 ) ) -> ( I = J -> ( I e. Prime /\ I || F /\ I || G ) ) )
Theorem	prmdvdsfmtnof1lem2 41497	Lemma 2 for prmdvdsfmtnof1 41499. (Contributed by AV, 3-Aug-2021.)
|- ( ( F e. ran FermatNo /\ G e. ran FermatNo ) -> ( ( I e. Prime /\ I || F /\ I || G ) -> F = G ) )
Theorem	prmdvdsfmtnof 41498*	The mapping of a Fermat number to its smallest prime factor is a function. (Contributed by AV, 4-Aug-2021.)
|- F = ( f e. ran FermatNo |-> inf ( { p e. Prime | p || f } , RR , < ) )   =>    |- F : ran FermatNo --> Prime
Theorem	prmdvdsfmtnof1 41499*	The mapping of a Fermat number to its smallest prime factor is a one-to-one function. (Contributed by AV, 4-Aug-2021.)
|- F = ( f e. ran FermatNo |-> inf ( { p e. Prime | p || f } , RR , < ) )   =>    |- F : ran FermatNo -1-1-> Prime
Theorem	prminf2 41500	The set of prime numbers is infinite. The proof of this variant of prminf 15619 is based on Goldbach's theorem goldbachth 41459 (via prmdvdsfmtnof1 41499 and prmdvdsfmtnof1lem2 41497), see Wikipedia "Fermat number", 4-Aug-2021, https://en.wikipedia.org/wiki/Fermat_number#Basic_properties. (Contributed by AV, 4-Aug-2021.)
|- Prime e/ Fin