Metamath Proof Explorer

Theorem sqrtpwpw2p

Description: 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)

Ref Expression
Assertion sqrtpwpw2p ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 โˆง ๐‘€ < ( ( 2 โ†‘ ( ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) + 1 ) ) + 1 ) ) โ†’ ( โŒŠ โ€˜ ( โˆš โ€˜ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) ) ) = ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 nncn โŠข ( ๐‘ โˆˆ โ„• โ†’ ๐‘ โˆˆ โ„‚ )
2 1 adantr โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 ) โ†’ ๐‘ โˆˆ โ„‚ )
3 npcan1 โŠข ( ๐‘ โˆˆ โ„‚ โ†’ ( ( ๐‘ โˆ’ 1 ) + 1 ) = ๐‘ )
4 2 3 syl โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 ) โ†’ ( ( ๐‘ โˆ’ 1 ) + 1 ) = ๐‘ )
5 4 eqcomd โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 ) โ†’ ๐‘ = ( ( ๐‘ โˆ’ 1 ) + 1 ) )
6 5 oveq2d โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 ) โ†’ ( 2 โ†‘ ๐‘ ) = ( 2 โ†‘ ( ( ๐‘ โˆ’ 1 ) + 1 ) ) )
7 2cnd โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 ) โ†’ 2 โˆˆ โ„‚ )
8 nnm1nn0 โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ๐‘ โˆ’ 1 ) โˆˆ โ„•0 )
9 8 adantr โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 ) โ†’ ( ๐‘ โˆ’ 1 ) โˆˆ โ„•0 )
10 7 9 expp1d โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 ) โ†’ ( 2 โ†‘ ( ( ๐‘ โˆ’ 1 ) + 1 ) ) = ( ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ยท 2 ) )
11 6 10 eqtrd โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 ) โ†’ ( 2 โ†‘ ๐‘ ) = ( ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ยท 2 ) )
12 11 oveq2d โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 ) โ†’ ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) = ( 2 โ†‘ ( ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ยท 2 ) ) )
13 2nn0 โŠข 2 โˆˆ โ„•0
14 13 a1i โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 ) โ†’ 2 โˆˆ โ„•0 )
15 13 a1i โŠข ( ๐‘ โˆˆ โ„• โ†’ 2 โˆˆ โ„•0 )
16 15 8 nn0expcld โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) โˆˆ โ„•0 )
17 16 adantr โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 ) โ†’ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) โˆˆ โ„•0 )
18 7 14 17 expmuld โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 ) โ†’ ( 2 โ†‘ ( ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ยท 2 ) ) = ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) โ†‘ 2 ) )
19 12 18 eqtrd โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 ) โ†’ ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) = ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) โ†‘ 2 ) )
20 nn0ge0 โŠข ( ๐‘€ โˆˆ โ„•0 โ†’ 0 โ‰ค ๐‘€ )
21 20 adantl โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 ) โ†’ 0 โ‰ค ๐‘€ )
22 nnnn0 โŠข ( ๐‘ โˆˆ โ„• โ†’ ๐‘ โˆˆ โ„•0 )
23 15 22 nn0expcld โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 2 โ†‘ ๐‘ ) โˆˆ โ„•0 )
24 15 23 nn0expcld โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) โˆˆ โ„•0 )
25 24 nn0red โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) โˆˆ โ„ )
26 nn0re โŠข ( ๐‘€ โˆˆ โ„•0 โ†’ ๐‘€ โˆˆ โ„ )
27 25 26 anim12i โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 ) โ†’ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) โˆˆ โ„ โˆง ๐‘€ โˆˆ โ„ ) )
28 addge01 โŠข ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) โˆˆ โ„ โˆง ๐‘€ โˆˆ โ„ ) โ†’ ( 0 โ‰ค ๐‘€ โ†” ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) โ‰ค ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) ) )
29 27 28 syl โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 ) โ†’ ( 0 โ‰ค ๐‘€ โ†” ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) โ‰ค ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) ) )
30 21 29 mpbid โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 ) โ†’ ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) โ‰ค ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) )
31 19 30 eqbrtrrd โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 ) โ†’ ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) โ†‘ 2 ) โ‰ค ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) )
32 24 adantr โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 ) โ†’ ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) โˆˆ โ„•0 )
33 simpr โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 ) โ†’ ๐‘€ โˆˆ โ„•0 )
34 32 33 nn0addcld โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 ) โ†’ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) โˆˆ โ„•0 )
35 nn0re โŠข ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) โˆˆ โ„•0 โ†’ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) โˆˆ โ„ )
36 nn0ge0 โŠข ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) โˆˆ โ„•0 โ†’ 0 โ‰ค ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) )
37 35 36 jca โŠข ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) โˆˆ โ„•0 โ†’ ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) โˆˆ โ„ โˆง 0 โ‰ค ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) ) )
38 34 37 syl โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 ) โ†’ ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) โˆˆ โ„ โˆง 0 โ‰ค ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) ) )
39 resqrtth โŠข ( ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) โˆˆ โ„ โˆง 0 โ‰ค ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) ) โ†’ ( ( โˆš โ€˜ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) ) โ†‘ 2 ) = ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) )
40 38 39 syl โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 ) โ†’ ( ( โˆš โ€˜ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) ) โ†‘ 2 ) = ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) )
41 31 40 breqtrrd โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 ) โ†’ ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) โ†‘ 2 ) โ‰ค ( ( โˆš โ€˜ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) ) โ†‘ 2 ) )
42 15 16 nn0expcld โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) โˆˆ โ„•0 )
43 nn0re โŠข ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) โˆˆ โ„•0 โ†’ ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) โˆˆ โ„ )
44 nn0ge0 โŠข ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) โˆˆ โ„•0 โ†’ 0 โ‰ค ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) )
45 43 44 jca โŠข ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) โˆˆ โ„•0 โ†’ ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) โˆˆ โ„ โˆง 0 โ‰ค ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) )
46 42 45 syl โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) โˆˆ โ„ โˆง 0 โ‰ค ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) )
47 46 adantr โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 ) โ†’ ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) โˆˆ โ„ โˆง 0 โ‰ค ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) )
48 resqrtcl โŠข ( ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) โˆˆ โ„ โˆง 0 โ‰ค ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) ) โ†’ ( โˆš โ€˜ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) ) โˆˆ โ„ )
49 38 48 syl โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 ) โ†’ ( โˆš โ€˜ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) ) โˆˆ โ„ )
50 sqrtge0 โŠข ( ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) โˆˆ โ„ โˆง 0 โ‰ค ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) ) โ†’ 0 โ‰ค ( โˆš โ€˜ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) ) )
51 38 50 syl โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 ) โ†’ 0 โ‰ค ( โˆš โ€˜ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) ) )
52 le2sq โŠข ( ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) โˆˆ โ„ โˆง 0 โ‰ค ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) โˆง ( ( โˆš โ€˜ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) ) โˆˆ โ„ โˆง 0 โ‰ค ( โˆš โ€˜ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) ) ) ) โ†’ ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) โ‰ค ( โˆš โ€˜ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) ) โ†” ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) โ†‘ 2 ) โ‰ค ( ( โˆš โ€˜ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) ) โ†‘ 2 ) ) )
53 47 49 51 52 syl12anc โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 ) โ†’ ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) โ‰ค ( โˆš โ€˜ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) ) โ†” ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) โ†‘ 2 ) โ‰ค ( ( โˆš โ€˜ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) ) โ†‘ 2 ) ) )
54 41 53 mpbird โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 ) โ†’ ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) โ‰ค ( โˆš โ€˜ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) ) )
55 54 3adant3 โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 โˆง ๐‘€ < ( ( 2 โ†‘ ( ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) + 1 ) ) + 1 ) ) โ†’ ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) โ‰ค ( โˆš โ€˜ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) ) )
56 26 adantl โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 ) โ†’ ๐‘€ โˆˆ โ„ )
57 peano2nn0 โŠข ( ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) โˆˆ โ„•0 โ†’ ( ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) + 1 ) โˆˆ โ„•0 )
58 16 57 syl โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) + 1 ) โˆˆ โ„•0 )
59 15 58 nn0expcld โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 2 โ†‘ ( ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) + 1 ) ) โˆˆ โ„•0 )
60 59 adantr โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 ) โ†’ ( 2 โ†‘ ( ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) + 1 ) ) โˆˆ โ„•0 )
61 peano2nn0 โŠข ( ( 2 โ†‘ ( ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) + 1 ) ) โˆˆ โ„•0 โ†’ ( ( 2 โ†‘ ( ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) + 1 ) ) + 1 ) โˆˆ โ„•0 )
62 60 61 syl โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 ) โ†’ ( ( 2 โ†‘ ( ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) + 1 ) ) + 1 ) โˆˆ โ„•0 )
63 62 nn0red โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 ) โ†’ ( ( 2 โ†‘ ( ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) + 1 ) ) + 1 ) โˆˆ โ„ )
64 32 nn0red โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 ) โ†’ ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) โˆˆ โ„ )
65 axltadd โŠข ( ( ๐‘€ โˆˆ โ„ โˆง ( ( 2 โ†‘ ( ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) + 1 ) ) + 1 ) โˆˆ โ„ โˆง ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) โˆˆ โ„ ) โ†’ ( ๐‘€ < ( ( 2 โ†‘ ( ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) + 1 ) ) + 1 ) โ†’ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) < ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ( ( 2 โ†‘ ( ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) + 1 ) ) + 1 ) ) ) )
66 56 63 64 65 syl3anc โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 ) โ†’ ( ๐‘€ < ( ( 2 โ†‘ ( ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) + 1 ) ) + 1 ) โ†’ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) < ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ( ( 2 โ†‘ ( ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) + 1 ) ) + 1 ) ) ) )
67 66 3impia โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 โˆง ๐‘€ < ( ( 2 โ†‘ ( ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) + 1 ) ) + 1 ) ) โ†’ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) < ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ( ( 2 โ†‘ ( ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) + 1 ) ) + 1 ) ) )
68 24 nn0cnd โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) โˆˆ โ„‚ )
69 68 3ad2ant1 โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 โˆง ๐‘€ < ( ( 2 โ†‘ ( ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) + 1 ) ) + 1 ) ) โ†’ ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) โˆˆ โ„‚ )
70 59 nn0cnd โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 2 โ†‘ ( ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) + 1 ) ) โˆˆ โ„‚ )
71 70 3ad2ant1 โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 โˆง ๐‘€ < ( ( 2 โ†‘ ( ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) + 1 ) ) + 1 ) ) โ†’ ( 2 โ†‘ ( ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) + 1 ) ) โˆˆ โ„‚ )
72 1cnd โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 โˆง ๐‘€ < ( ( 2 โ†‘ ( ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) + 1 ) ) + 1 ) ) โ†’ 1 โˆˆ โ„‚ )
73 69 71 72 addassd โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 โˆง ๐‘€ < ( ( 2 โ†‘ ( ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) + 1 ) ) + 1 ) ) โ†’ ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ( 2 โ†‘ ( ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) + 1 ) ) ) + 1 ) = ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ( ( 2 โ†‘ ( ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) + 1 ) ) + 1 ) ) )
74 67 73 breqtrrd โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 โˆง ๐‘€ < ( ( 2 โ†‘ ( ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) + 1 ) ) + 1 ) ) โ†’ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) < ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ( 2 โ†‘ ( ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) + 1 ) ) ) + 1 ) )
75 42 nn0cnd โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) โˆˆ โ„‚ )
76 binom21 โŠข ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) โˆˆ โ„‚ โ†’ ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) + 1 ) โ†‘ 2 ) = ( ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) โ†‘ 2 ) + ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) ) + 1 ) )
77 75 76 syl โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) + 1 ) โ†‘ 2 ) = ( ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) โ†‘ 2 ) + ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) ) + 1 ) )
78 2cnd โŠข ( ๐‘ โˆˆ โ„• โ†’ 2 โˆˆ โ„‚ )
79 78 15 16 expmuld โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 2 โ†‘ ( ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ยท 2 ) ) = ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) โ†‘ 2 ) )
80 78 8 expp1d โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 2 โ†‘ ( ( ๐‘ โˆ’ 1 ) + 1 ) ) = ( ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ยท 2 ) )
81 1 3 syl โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ( ๐‘ โˆ’ 1 ) + 1 ) = ๐‘ )
82 81 oveq2d โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 2 โ†‘ ( ( ๐‘ โˆ’ 1 ) + 1 ) ) = ( 2 โ†‘ ๐‘ ) )
83 80 82 eqtr3d โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ยท 2 ) = ( 2 โ†‘ ๐‘ ) )
84 83 oveq2d โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 2 โ†‘ ( ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ยท 2 ) ) = ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) )
85 79 84 eqtr3d โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) โ†‘ 2 ) = ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) )
86 78 75 mulcomd โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) = ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ยท 2 ) )
87 78 16 expp1d โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 2 โ†‘ ( ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) + 1 ) ) = ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ยท 2 ) )
88 86 87 eqtr4d โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) = ( 2 โ†‘ ( ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) + 1 ) ) )
89 85 88 oveq12d โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) โ†‘ 2 ) + ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) ) = ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ( 2 โ†‘ ( ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) + 1 ) ) ) )
90 89 oveq1d โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) โ†‘ 2 ) + ( 2 ยท ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) ) ) + 1 ) = ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ( 2 โ†‘ ( ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) + 1 ) ) ) + 1 ) )
91 77 90 eqtrd โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) + 1 ) โ†‘ 2 ) = ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ( 2 โ†‘ ( ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) + 1 ) ) ) + 1 ) )
92 91 adantr โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 ) โ†’ ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) + 1 ) โ†‘ 2 ) = ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ( 2 โ†‘ ( ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) + 1 ) ) ) + 1 ) )
93 40 92 breq12d โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 ) โ†’ ( ( ( โˆš โ€˜ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) ) โ†‘ 2 ) < ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) + 1 ) โ†‘ 2 ) โ†” ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) < ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ( 2 โ†‘ ( ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) + 1 ) ) ) + 1 ) ) )
94 93 3adant3 โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 โˆง ๐‘€ < ( ( 2 โ†‘ ( ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) + 1 ) ) + 1 ) ) โ†’ ( ( ( โˆš โ€˜ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) ) โ†‘ 2 ) < ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) + 1 ) โ†‘ 2 ) โ†” ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) < ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ( 2 โ†‘ ( ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) + 1 ) ) ) + 1 ) ) )
95 74 94 mpbird โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 โˆง ๐‘€ < ( ( 2 โ†‘ ( ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) + 1 ) ) + 1 ) ) โ†’ ( ( โˆš โ€˜ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) ) โ†‘ 2 ) < ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) + 1 ) โ†‘ 2 ) )
96 34 nn0red โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 ) โ†’ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) โˆˆ โ„ )
97 nn0ge0 โŠข ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) โˆˆ โ„•0 โ†’ 0 โ‰ค ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) )
98 24 97 syl โŠข ( ๐‘ โˆˆ โ„• โ†’ 0 โ‰ค ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) )
99 98 20 anim12i โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 ) โ†’ ( 0 โ‰ค ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) โˆง 0 โ‰ค ๐‘€ ) )
100 27 99 jca โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 ) โ†’ ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) โˆˆ โ„ โˆง ๐‘€ โˆˆ โ„ ) โˆง ( 0 โ‰ค ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) โˆง 0 โ‰ค ๐‘€ ) ) )
101 addge0 โŠข ( ( ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) โˆˆ โ„ โˆง ๐‘€ โˆˆ โ„ ) โˆง ( 0 โ‰ค ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) โˆง 0 โ‰ค ๐‘€ ) ) โ†’ 0 โ‰ค ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) )
102 100 101 syl โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 ) โ†’ 0 โ‰ค ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) )
103 96 102 resqrtcld โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 ) โ†’ ( โˆš โ€˜ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) ) โˆˆ โ„ )
104 peano2nn0 โŠข ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) โˆˆ โ„•0 โ†’ ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) + 1 ) โˆˆ โ„•0 )
105 42 104 syl โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) + 1 ) โˆˆ โ„•0 )
106 nn0re โŠข ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) + 1 ) โˆˆ โ„•0 โ†’ ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) + 1 ) โˆˆ โ„ )
107 nn0ge0 โŠข ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) + 1 ) โˆˆ โ„•0 โ†’ 0 โ‰ค ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) + 1 ) )
108 106 107 jca โŠข ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) + 1 ) โˆˆ โ„•0 โ†’ ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) + 1 ) โˆˆ โ„ โˆง 0 โ‰ค ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) + 1 ) ) )
109 105 108 syl โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) + 1 ) โˆˆ โ„ โˆง 0 โ‰ค ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) + 1 ) ) )
110 109 adantr โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 ) โ†’ ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) + 1 ) โˆˆ โ„ โˆง 0 โ‰ค ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) + 1 ) ) )
111 lt2sq โŠข ( ( ( ( โˆš โ€˜ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) ) โˆˆ โ„ โˆง 0 โ‰ค ( โˆš โ€˜ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) ) ) โˆง ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) + 1 ) โˆˆ โ„ โˆง 0 โ‰ค ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) + 1 ) ) ) โ†’ ( ( โˆš โ€˜ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) ) < ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) + 1 ) โ†” ( ( โˆš โ€˜ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) ) โ†‘ 2 ) < ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) + 1 ) โ†‘ 2 ) ) )
112 103 51 110 111 syl21anc โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 ) โ†’ ( ( โˆš โ€˜ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) ) < ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) + 1 ) โ†” ( ( โˆš โ€˜ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) ) โ†‘ 2 ) < ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) + 1 ) โ†‘ 2 ) ) )
113 112 3adant3 โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 โˆง ๐‘€ < ( ( 2 โ†‘ ( ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) + 1 ) ) + 1 ) ) โ†’ ( ( โˆš โ€˜ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) ) < ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) + 1 ) โ†” ( ( โˆš โ€˜ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) ) โ†‘ 2 ) < ( ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) + 1 ) โ†‘ 2 ) ) )
114 95 113 mpbird โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 โˆง ๐‘€ < ( ( 2 โ†‘ ( ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) + 1 ) ) + 1 ) ) โ†’ ( โˆš โ€˜ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) ) < ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) + 1 ) )
115 55 114 jca โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 โˆง ๐‘€ < ( ( 2 โ†‘ ( ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) + 1 ) ) + 1 ) ) โ†’ ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) โ‰ค ( โˆš โ€˜ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) ) โˆง ( โˆš โ€˜ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) ) < ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) + 1 ) ) )
116 42 nn0zd โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) โˆˆ โ„ค )
117 116 adantr โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 ) โ†’ ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) โˆˆ โ„ค )
118 49 117 jca โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 ) โ†’ ( ( โˆš โ€˜ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) ) โˆˆ โ„ โˆง ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) โˆˆ โ„ค ) )
119 118 3adant3 โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 โˆง ๐‘€ < ( ( 2 โ†‘ ( ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) + 1 ) ) + 1 ) ) โ†’ ( ( โˆš โ€˜ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) ) โˆˆ โ„ โˆง ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) โˆˆ โ„ค ) )
120 flbi โŠข ( ( ( โˆš โ€˜ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) ) โˆˆ โ„ โˆง ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) โˆˆ โ„ค ) โ†’ ( ( โŒŠ โ€˜ ( โˆš โ€˜ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) ) ) = ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) โ†” ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) โ‰ค ( โˆš โ€˜ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) ) โˆง ( โˆš โ€˜ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) ) < ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) + 1 ) ) ) )
121 119 120 syl โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 โˆง ๐‘€ < ( ( 2 โ†‘ ( ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) + 1 ) ) + 1 ) ) โ†’ ( ( โŒŠ โ€˜ ( โˆš โ€˜ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) ) ) = ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) โ†” ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) โ‰ค ( โˆš โ€˜ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) ) โˆง ( โˆš โ€˜ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) ) < ( ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) + 1 ) ) ) )
122 115 121 mpbird โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘€ โˆˆ โ„•0 โˆง ๐‘€ < ( ( 2 โ†‘ ( ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) + 1 ) ) + 1 ) ) โ†’ ( โŒŠ โ€˜ ( โˆš โ€˜ ( ( 2 โ†‘ ( 2 โ†‘ ๐‘ ) ) + ๐‘€ ) ) ) = ( 2 โ†‘ ( 2 โ†‘ ( ๐‘ โˆ’ 1 ) ) ) )