Metamath Proof Explorer

Theorem fmtnosqrt

Description: The floor of the square root of a Fermat number. (Contributed by AV, 28-Jul-2021)

Ref Expression
Assertion fmtnosqrt 
|- ( N e. NN -> ( |_ ` ( sqrt ` ( FermatNo ` N ) ) ) = ( 2 ^ ( 2 ^ ( N - 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
2 fmtno 
 |-  ( N e. NN0 -> ( FermatNo ` N ) = ( ( 2 ^ ( 2 ^ N ) ) + 1 ) )
3 1 2 syl 
 |-  ( N e. NN -> ( FermatNo ` N ) = ( ( 2 ^ ( 2 ^ N ) ) + 1 ) )
4 3 fveq2d 
 |-  ( N e. NN -> ( sqrt ` ( FermatNo ` N ) ) = ( sqrt ` ( ( 2 ^ ( 2 ^ N ) ) + 1 ) ) )
5 4 fveq2d 
 |-  ( N e. NN -> ( |_ ` ( sqrt ` ( FermatNo ` N ) ) ) = ( |_ ` ( sqrt ` ( ( 2 ^ ( 2 ^ N ) ) + 1 ) ) ) )
6 id 
 |-  ( N e. NN -> N e. NN )
7 1nn0 
 |-  1 e. NN0
8 7 a1i 
 |-  ( N e. NN -> 1 e. NN0 )
9 2nn 
 |-  2 e. NN
10 9 a1i 
 |-  ( N e. NN -> 2 e. NN )
11 2nn0 
 |-  2 e. NN0
12 11 a1i 
 |-  ( N e. NN -> 2 e. NN0 )
13 nnm1nn0 
 |-  ( N e. NN -> ( N - 1 ) e. NN0 )
14 12 13 nn0expcld 
 |-  ( N e. NN -> ( 2 ^ ( N - 1 ) ) e. NN0 )
15 peano2nn0 
 |-  ( ( 2 ^ ( N - 1 ) ) e. NN0 -> ( ( 2 ^ ( N - 1 ) ) + 1 ) e. NN0 )
16 14 15 syl 
 |-  ( N e. NN -> ( ( 2 ^ ( N - 1 ) ) + 1 ) e. NN0 )
17 10 16 nnexpcld 
 |-  ( N e. NN -> ( 2 ^ ( ( 2 ^ ( N - 1 ) ) + 1 ) ) e. NN )
18 nngt0 
 |-  ( ( 2 ^ ( ( 2 ^ ( N - 1 ) ) + 1 ) ) e. NN -> 0 < ( 2 ^ ( ( 2 ^ ( N - 1 ) ) + 1 ) ) )
19 17 18 syl 
 |-  ( N e. NN -> 0 < ( 2 ^ ( ( 2 ^ ( N - 1 ) ) + 1 ) ) )
20 12 16 nn0expcld 
 |-  ( N e. NN -> ( 2 ^ ( ( 2 ^ ( N - 1 ) ) + 1 ) ) e. NN0 )
21 20 nn0red 
 |-  ( N e. NN -> ( 2 ^ ( ( 2 ^ ( N - 1 ) ) + 1 ) ) e. RR )
22 1re 
 |-  1 e. RR
23 22 a1i 
 |-  ( N e. NN -> 1 e. RR )
24 21 23 jca 
 |-  ( N e. NN -> ( ( 2 ^ ( ( 2 ^ ( N - 1 ) ) + 1 ) ) e. RR /\ 1 e. RR ) )
25 ltaddpos2 
 |-  ( ( ( 2 ^ ( ( 2 ^ ( N - 1 ) ) + 1 ) ) e. RR /\ 1 e. RR ) -> ( 0 < ( 2 ^ ( ( 2 ^ ( N - 1 ) ) + 1 ) ) <-> 1 < ( ( 2 ^ ( ( 2 ^ ( N - 1 ) ) + 1 ) ) + 1 ) ) )
26 24 25 syl 
 |-  ( N e. NN -> ( 0 < ( 2 ^ ( ( 2 ^ ( N - 1 ) ) + 1 ) ) <-> 1 < ( ( 2 ^ ( ( 2 ^ ( N - 1 ) ) + 1 ) ) + 1 ) ) )
27 19 26 mpbid 
 |-  ( N e. NN -> 1 < ( ( 2 ^ ( ( 2 ^ ( N - 1 ) ) + 1 ) ) + 1 ) )
28 6 8 27 3jca 
 |-  ( N e. NN -> ( N e. NN /\ 1 e. NN0 /\ 1 < ( ( 2 ^ ( ( 2 ^ ( N - 1 ) ) + 1 ) ) + 1 ) ) )
29 sqrtpwpw2p 
 |-  ( ( N e. NN /\ 1 e. NN0 /\ 1 < ( ( 2 ^ ( ( 2 ^ ( N - 1 ) ) + 1 ) ) + 1 ) ) -> ( |_ ` ( sqrt ` ( ( 2 ^ ( 2 ^ N ) ) + 1 ) ) ) = ( 2 ^ ( 2 ^ ( N - 1 ) ) ) )
30 28 29 syl 
 |-  ( N e. NN -> ( |_ ` ( sqrt ` ( ( 2 ^ ( 2 ^ N ) ) + 1 ) ) ) = ( 2 ^ ( 2 ^ ( N - 1 ) ) ) )
31 5 30 eqtrd 
 |-  ( N e. NN -> ( |_ ` ( sqrt ` ( FermatNo ` N ) ) ) = ( 2 ^ ( 2 ^ ( N - 1 ) ) ) )