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 ( 𝑁 ∈ ℕ → ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 𝑁 ) ) ) = ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
2 fmtno ⊢ ( 𝑁 ∈ ℕ0 → ( FermatNo ‘ 𝑁 ) = ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) )
3 1 2 syl ⊢ ( 𝑁 ∈ ℕ → ( FermatNo ‘ 𝑁 ) = ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) )
4 3 fveq2d ⊢ ( 𝑁 ∈ ℕ → ( √ ‘ ( FermatNo ‘ 𝑁 ) ) = ( √ ‘ ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) ) )
5 4 fveq2d ⊢ ( 𝑁 ∈ ℕ → ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 𝑁 ) ) ) = ( ⌊ ‘ ( √ ‘ ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) ) ) )
6 id ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ )
7 1nn0 ⊢ 1 ∈ ℕ0
8 7 a1i ⊢ ( 𝑁 ∈ ℕ → 1 ∈ ℕ0 )
9 2nn ⊢ 2 ∈ ℕ
10 9 a1i ⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℕ )
11 2nn0 ⊢ 2 ∈ ℕ0
12 11 a1i ⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℕ0 )
13 nnm1nn0 ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℕ0 )
14 12 13 nn0expcld ⊢ ( 𝑁 ∈ ℕ → ( 2 ↑ ( 𝑁 − 1 ) ) ∈ ℕ0 )
15 peano2nn0 ⊢ ( ( 2 ↑ ( 𝑁 − 1 ) ) ∈ ℕ0 → ( ( 2 ↑ ( 𝑁 − 1 ) ) + 1 ) ∈ ℕ0 )
16 14 15 syl ⊢ ( 𝑁 ∈ ℕ → ( ( 2 ↑ ( 𝑁 − 1 ) ) + 1 ) ∈ ℕ0 )
17 10 16 nnexpcld ⊢ ( 𝑁 ∈ ℕ → ( 2 ↑ ( ( 2 ↑ ( 𝑁 − 1 ) ) + 1 ) ) ∈ ℕ )
18 nngt0 ⊢ ( ( 2 ↑ ( ( 2 ↑ ( 𝑁 − 1 ) ) + 1 ) ) ∈ ℕ → 0 < ( 2 ↑ ( ( 2 ↑ ( 𝑁 − 1 ) ) + 1 ) ) )
19 17 18 syl ⊢ ( 𝑁 ∈ ℕ → 0 < ( 2 ↑ ( ( 2 ↑ ( 𝑁 − 1 ) ) + 1 ) ) )
20 12 16 nn0expcld ⊢ ( 𝑁 ∈ ℕ → ( 2 ↑ ( ( 2 ↑ ( 𝑁 − 1 ) ) + 1 ) ) ∈ ℕ0 )
21 20 nn0red ⊢ ( 𝑁 ∈ ℕ → ( 2 ↑ ( ( 2 ↑ ( 𝑁 − 1 ) ) + 1 ) ) ∈ ℝ )
22 1re ⊢ 1 ∈ ℝ
23 22 a1i ⊢ ( 𝑁 ∈ ℕ → 1 ∈ ℝ )
24 21 23 jca ⊢ ( 𝑁 ∈ ℕ → ( ( 2 ↑ ( ( 2 ↑ ( 𝑁 − 1 ) ) + 1 ) ) ∈ ℝ ∧ 1 ∈ ℝ ) )
25 ltaddpos2 ⊢ ( ( ( 2 ↑ ( ( 2 ↑ ( 𝑁 − 1 ) ) + 1 ) ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( 0 < ( 2 ↑ ( ( 2 ↑ ( 𝑁 − 1 ) ) + 1 ) ) ↔ 1 < ( ( 2 ↑ ( ( 2 ↑ ( 𝑁 − 1 ) ) + 1 ) ) + 1 ) ) )
26 24 25 syl ⊢ ( 𝑁 ∈ ℕ → ( 0 < ( 2 ↑ ( ( 2 ↑ ( 𝑁 − 1 ) ) + 1 ) ) ↔ 1 < ( ( 2 ↑ ( ( 2 ↑ ( 𝑁 − 1 ) ) + 1 ) ) + 1 ) ) )
27 19 26 mpbid ⊢ ( 𝑁 ∈ ℕ → 1 < ( ( 2 ↑ ( ( 2 ↑ ( 𝑁 − 1 ) ) + 1 ) ) + 1 ) )
28 6 8 27 3jca ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 ∈ ℕ ∧ 1 ∈ ℕ0 ∧ 1 < ( ( 2 ↑ ( ( 2 ↑ ( 𝑁 − 1 ) ) + 1 ) ) + 1 ) ) )
29 sqrtpwpw2p ⊢ ( ( 𝑁 ∈ ℕ ∧ 1 ∈ ℕ0 ∧ 1 < ( ( 2 ↑ ( ( 2 ↑ ( 𝑁 − 1 ) ) + 1 ) ) + 1 ) ) → ( ⌊ ‘ ( √ ‘ ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) ) ) = ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) )
30 28 29 syl ⊢ ( 𝑁 ∈ ℕ → ( ⌊ ‘ ( √ ‘ ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) ) ) = ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) )
31 5 30 eqtrd ⊢ ( 𝑁 ∈ ℕ → ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 𝑁 ) ) ) = ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) )