Metamath Proof Explorer

Theorem fmtnof1

Description: The enumeration of the Fermat numbers is a one-one function into the positive integers. (Contributed by AV, 3-Aug-2021)

Ref Expression
Assertion fmtnof1 
|- FermatNo : NN0 -1-1-> NN

Proof

Step Hyp Ref Expression
1 df-fmtno 
 |-  FermatNo = ( n e. NN0 |-> ( ( 2 ^ ( 2 ^ n ) ) + 1 ) )
2 2nn 
 |-  2 e. NN
3 2 a1i 
 |-  ( n e. NN0 -> 2 e. NN )
4 2nn0 
 |-  2 e. NN0
5 4 a1i 
 |-  ( n e. NN0 -> 2 e. NN0 )
6 id 
 |-  ( n e. NN0 -> n e. NN0 )
7 5 6 nn0expcld 
 |-  ( n e. NN0 -> ( 2 ^ n ) e. NN0 )
8 3 7 nnexpcld 
 |-  ( n e. NN0 -> ( 2 ^ ( 2 ^ n ) ) e. NN )
9 8 peano2nnd 
 |-  ( n e. NN0 -> ( ( 2 ^ ( 2 ^ n ) ) + 1 ) e. NN )
10 1 9 fmpti 
 |-  FermatNo : NN0 --> NN
11 fmtno 
 |-  ( n e. NN0 -> ( FermatNo ` n ) = ( ( 2 ^ ( 2 ^ n ) ) + 1 ) )
12 fmtno 
 |-  ( m e. NN0 -> ( FermatNo ` m ) = ( ( 2 ^ ( 2 ^ m ) ) + 1 ) )
13 11 12 eqeqan12d 
 |-  ( ( n e. NN0 /\ m e. NN0 ) -> ( ( FermatNo ` n ) = ( FermatNo ` m ) <-> ( ( 2 ^ ( 2 ^ n ) ) + 1 ) = ( ( 2 ^ ( 2 ^ m ) ) + 1 ) ) )
14 5 7 nn0expcld 
 |-  ( n e. NN0 -> ( 2 ^ ( 2 ^ n ) ) e. NN0 )
15 14 nn0cnd 
 |-  ( n e. NN0 -> ( 2 ^ ( 2 ^ n ) ) e. CC )
16 15 adantr 
 |-  ( ( n e. NN0 /\ m e. NN0 ) -> ( 2 ^ ( 2 ^ n ) ) e. CC )
17 4 a1i 
 |-  ( m e. NN0 -> 2 e. NN0 )
18 id 
 |-  ( m e. NN0 -> m e. NN0 )
19 17 18 nn0expcld 
 |-  ( m e. NN0 -> ( 2 ^ m ) e. NN0 )
20 17 19 nn0expcld 
 |-  ( m e. NN0 -> ( 2 ^ ( 2 ^ m ) ) e. NN0 )
21 20 nn0cnd 
 |-  ( m e. NN0 -> ( 2 ^ ( 2 ^ m ) ) e. CC )
22 21 adantl 
 |-  ( ( n e. NN0 /\ m e. NN0 ) -> ( 2 ^ ( 2 ^ m ) ) e. CC )
23 1cnd 
 |-  ( ( n e. NN0 /\ m e. NN0 ) -> 1 e. CC )
24 16 22 23 addcan2d 
 |-  ( ( n e. NN0 /\ m e. NN0 ) -> ( ( ( 2 ^ ( 2 ^ n ) ) + 1 ) = ( ( 2 ^ ( 2 ^ m ) ) + 1 ) <-> ( 2 ^ ( 2 ^ n ) ) = ( 2 ^ ( 2 ^ m ) ) ) )
25 2re 
 |-  2 e. RR
26 25 a1i 
 |-  ( ( n e. NN0 /\ m e. NN0 ) -> 2 e. RR )
27 7 nn0zd 
 |-  ( n e. NN0 -> ( 2 ^ n ) e. ZZ )
28 27 adantr 
 |-  ( ( n e. NN0 /\ m e. NN0 ) -> ( 2 ^ n ) e. ZZ )
29 19 nn0zd 
 |-  ( m e. NN0 -> ( 2 ^ m ) e. ZZ )
30 29 adantl 
 |-  ( ( n e. NN0 /\ m e. NN0 ) -> ( 2 ^ m ) e. ZZ )
31 1lt2 
 |-  1 < 2
32 31 a1i 
 |-  ( ( n e. NN0 /\ m e. NN0 ) -> 1 < 2 )
33 expcan 
 |-  ( ( ( 2 e. RR /\ ( 2 ^ n ) e. ZZ /\ ( 2 ^ m ) e. ZZ ) /\ 1 < 2 ) -> ( ( 2 ^ ( 2 ^ n ) ) = ( 2 ^ ( 2 ^ m ) ) <-> ( 2 ^ n ) = ( 2 ^ m ) ) )
34 26 28 30 32 33 syl31anc 
 |-  ( ( n e. NN0 /\ m e. NN0 ) -> ( ( 2 ^ ( 2 ^ n ) ) = ( 2 ^ ( 2 ^ m ) ) <-> ( 2 ^ n ) = ( 2 ^ m ) ) )
35 24 34 bitrd 
 |-  ( ( n e. NN0 /\ m e. NN0 ) -> ( ( ( 2 ^ ( 2 ^ n ) ) + 1 ) = ( ( 2 ^ ( 2 ^ m ) ) + 1 ) <-> ( 2 ^ n ) = ( 2 ^ m ) ) )
36 nn0z 
 |-  ( n e. NN0 -> n e. ZZ )
37 36 adantr 
 |-  ( ( n e. NN0 /\ m e. NN0 ) -> n e. ZZ )
38 nn0z 
 |-  ( m e. NN0 -> m e. ZZ )
39 38 adantl 
 |-  ( ( n e. NN0 /\ m e. NN0 ) -> m e. ZZ )
40 expcan 
 |-  ( ( ( 2 e. RR /\ n e. ZZ /\ m e. ZZ ) /\ 1 < 2 ) -> ( ( 2 ^ n ) = ( 2 ^ m ) <-> n = m ) )
41 40 biimpd 
 |-  ( ( ( 2 e. RR /\ n e. ZZ /\ m e. ZZ ) /\ 1 < 2 ) -> ( ( 2 ^ n ) = ( 2 ^ m ) -> n = m ) )
42 26 37 39 32 41 syl31anc 
 |-  ( ( n e. NN0 /\ m e. NN0 ) -> ( ( 2 ^ n ) = ( 2 ^ m ) -> n = m ) )
43 35 42 sylbid 
 |-  ( ( n e. NN0 /\ m e. NN0 ) -> ( ( ( 2 ^ ( 2 ^ n ) ) + 1 ) = ( ( 2 ^ ( 2 ^ m ) ) + 1 ) -> n = m ) )
44 13 43 sylbid 
 |-  ( ( n e. NN0 /\ m e. NN0 ) -> ( ( FermatNo ` n ) = ( FermatNo ` m ) -> n = m ) )
45 44 rgen2 
 |-  A. n e. NN0 A. m e. NN0 ( ( FermatNo ` n ) = ( FermatNo ` m ) -> n = m )
46 dff13 
 |-  ( FermatNo : NN0 -1-1-> NN <-> ( FermatNo : NN0 --> NN /\ A. n e. NN0 A. m e. NN0 ( ( FermatNo ` n ) = ( FermatNo ` m ) -> n = m ) ) )
47 10 45 46 mpbir2an 
 |-  FermatNo : NN0 -1-1-> NN