Metamath Proof Explorer


Theorem bposlem5

Description: Lemma for bpos . Bound the product of all small primes in the binomial coefficient. (Contributed by Mario Carneiro, 15-Mar-2014) (Proof shortened by AV, 15-Sep-2021)

Ref Expression
Hypotheses bpos.1 โŠข ( ๐œ‘ โ†’ ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 5 ) )
bpos.2 โŠข ( ๐œ‘ โ†’ ยฌ โˆƒ ๐‘ โˆˆ โ„™ ( ๐‘ < ๐‘ โˆง ๐‘ โ‰ค ( 2 ยท ๐‘ ) ) )
bpos.3 โŠข ๐น = ( ๐‘› โˆˆ โ„• โ†ฆ if ( ๐‘› โˆˆ โ„™ , ( ๐‘› โ†‘ ( ๐‘› pCnt ( ( 2 ยท ๐‘ ) C ๐‘ ) ) ) , 1 ) )
bpos.4 โŠข ๐พ = ( โŒŠ โ€˜ ( ( 2 ยท ๐‘ ) / 3 ) )
bpos.5 โŠข ๐‘€ = ( โŒŠ โ€˜ ( โˆš โ€˜ ( 2 ยท ๐‘ ) ) )
Assertion bposlem5 ( ๐œ‘ โ†’ ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘€ ) โ‰ค ( ( 2 ยท ๐‘ ) โ†‘๐‘ ( ( ( โˆš โ€˜ ( 2 ยท ๐‘ ) ) / 3 ) + 2 ) ) )

Proof

Step Hyp Ref Expression
1 bpos.1 โŠข ( ๐œ‘ โ†’ ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 5 ) )
2 bpos.2 โŠข ( ๐œ‘ โ†’ ยฌ โˆƒ ๐‘ โˆˆ โ„™ ( ๐‘ < ๐‘ โˆง ๐‘ โ‰ค ( 2 ยท ๐‘ ) ) )
3 bpos.3 โŠข ๐น = ( ๐‘› โˆˆ โ„• โ†ฆ if ( ๐‘› โˆˆ โ„™ , ( ๐‘› โ†‘ ( ๐‘› pCnt ( ( 2 ยท ๐‘ ) C ๐‘ ) ) ) , 1 ) )
4 bpos.4 โŠข ๐พ = ( โŒŠ โ€˜ ( ( 2 ยท ๐‘ ) / 3 ) )
5 bpos.5 โŠข ๐‘€ = ( โŒŠ โ€˜ ( โˆš โ€˜ ( 2 ยท ๐‘ ) ) )
6 id โŠข ( ๐‘› โˆˆ โ„™ โ†’ ๐‘› โˆˆ โ„™ )
7 5nn โŠข 5 โˆˆ โ„•
8 eluznn โŠข ( ( 5 โˆˆ โ„• โˆง ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 5 ) ) โ†’ ๐‘ โˆˆ โ„• )
9 7 1 8 sylancr โŠข ( ๐œ‘ โ†’ ๐‘ โˆˆ โ„• )
10 9 nnnn0d โŠข ( ๐œ‘ โ†’ ๐‘ โˆˆ โ„•0 )
11 fzctr โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ๐‘ โˆˆ ( 0 ... ( 2 ยท ๐‘ ) ) )
12 bccl2 โŠข ( ๐‘ โˆˆ ( 0 ... ( 2 ยท ๐‘ ) ) โ†’ ( ( 2 ยท ๐‘ ) C ๐‘ ) โˆˆ โ„• )
13 10 11 12 3syl โŠข ( ๐œ‘ โ†’ ( ( 2 ยท ๐‘ ) C ๐‘ ) โˆˆ โ„• )
14 pccl โŠข ( ( ๐‘› โˆˆ โ„™ โˆง ( ( 2 ยท ๐‘ ) C ๐‘ ) โˆˆ โ„• ) โ†’ ( ๐‘› pCnt ( ( 2 ยท ๐‘ ) C ๐‘ ) ) โˆˆ โ„•0 )
15 6 13 14 syl2anr โŠข ( ( ๐œ‘ โˆง ๐‘› โˆˆ โ„™ ) โ†’ ( ๐‘› pCnt ( ( 2 ยท ๐‘ ) C ๐‘ ) ) โˆˆ โ„•0 )
16 15 ralrimiva โŠข ( ๐œ‘ โ†’ โˆ€ ๐‘› โˆˆ โ„™ ( ๐‘› pCnt ( ( 2 ยท ๐‘ ) C ๐‘ ) ) โˆˆ โ„•0 )
17 3 16 pcmptcl โŠข ( ๐œ‘ โ†’ ( ๐น : โ„• โŸถ โ„• โˆง seq 1 ( ยท , ๐น ) : โ„• โŸถ โ„• ) )
18 17 simprd โŠข ( ๐œ‘ โ†’ seq 1 ( ยท , ๐น ) : โ„• โŸถ โ„• )
19 3nn โŠข 3 โˆˆ โ„•
20 2z โŠข 2 โˆˆ โ„ค
21 9 nnzd โŠข ( ๐œ‘ โ†’ ๐‘ โˆˆ โ„ค )
22 zmulcl โŠข ( ( 2 โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( 2 ยท ๐‘ ) โˆˆ โ„ค )
23 20 21 22 sylancr โŠข ( ๐œ‘ โ†’ ( 2 ยท ๐‘ ) โˆˆ โ„ค )
24 23 zred โŠข ( ๐œ‘ โ†’ ( 2 ยท ๐‘ ) โˆˆ โ„ )
25 2nn โŠข 2 โˆˆ โ„•
26 nnmulcl โŠข ( ( 2 โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) โ†’ ( 2 ยท ๐‘ ) โˆˆ โ„• )
27 25 9 26 sylancr โŠข ( ๐œ‘ โ†’ ( 2 ยท ๐‘ ) โˆˆ โ„• )
28 27 nnrpd โŠข ( ๐œ‘ โ†’ ( 2 ยท ๐‘ ) โˆˆ โ„+ )
29 28 rpge0d โŠข ( ๐œ‘ โ†’ 0 โ‰ค ( 2 ยท ๐‘ ) )
30 24 29 resqrtcld โŠข ( ๐œ‘ โ†’ ( โˆš โ€˜ ( 2 ยท ๐‘ ) ) โˆˆ โ„ )
31 30 flcld โŠข ( ๐œ‘ โ†’ ( โŒŠ โ€˜ ( โˆš โ€˜ ( 2 ยท ๐‘ ) ) ) โˆˆ โ„ค )
32 sqrt9 โŠข ( โˆš โ€˜ 9 ) = 3
33 9re โŠข 9 โˆˆ โ„
34 33 a1i โŠข ( ๐œ‘ โ†’ 9 โˆˆ โ„ )
35 10re โŠข 1 0 โˆˆ โ„
36 35 a1i โŠข ( ๐œ‘ โ†’ 1 0 โˆˆ โ„ )
37 lep1 โŠข ( 9 โˆˆ โ„ โ†’ 9 โ‰ค ( 9 + 1 ) )
38 33 37 ax-mp โŠข 9 โ‰ค ( 9 + 1 )
39 9p1e10 โŠข ( 9 + 1 ) = 1 0
40 38 39 breqtri โŠข 9 โ‰ค 1 0
41 40 a1i โŠข ( ๐œ‘ โ†’ 9 โ‰ค 1 0 )
42 5cn โŠข 5 โˆˆ โ„‚
43 2cn โŠข 2 โˆˆ โ„‚
44 5t2e10 โŠข ( 5 ยท 2 ) = 1 0
45 42 43 44 mulcomli โŠข ( 2 ยท 5 ) = 1 0
46 eluzle โŠข ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 5 ) โ†’ 5 โ‰ค ๐‘ )
47 1 46 syl โŠข ( ๐œ‘ โ†’ 5 โ‰ค ๐‘ )
48 9 nnred โŠข ( ๐œ‘ โ†’ ๐‘ โˆˆ โ„ )
49 5re โŠข 5 โˆˆ โ„
50 2re โŠข 2 โˆˆ โ„
51 2pos โŠข 0 < 2
52 50 51 pm3.2i โŠข ( 2 โˆˆ โ„ โˆง 0 < 2 )
53 lemul2 โŠข ( ( 5 โˆˆ โ„ โˆง ๐‘ โˆˆ โ„ โˆง ( 2 โˆˆ โ„ โˆง 0 < 2 ) ) โ†’ ( 5 โ‰ค ๐‘ โ†” ( 2 ยท 5 ) โ‰ค ( 2 ยท ๐‘ ) ) )
54 49 52 53 mp3an13 โŠข ( ๐‘ โˆˆ โ„ โ†’ ( 5 โ‰ค ๐‘ โ†” ( 2 ยท 5 ) โ‰ค ( 2 ยท ๐‘ ) ) )
55 48 54 syl โŠข ( ๐œ‘ โ†’ ( 5 โ‰ค ๐‘ โ†” ( 2 ยท 5 ) โ‰ค ( 2 ยท ๐‘ ) ) )
56 47 55 mpbid โŠข ( ๐œ‘ โ†’ ( 2 ยท 5 ) โ‰ค ( 2 ยท ๐‘ ) )
57 45 56 eqbrtrrid โŠข ( ๐œ‘ โ†’ 1 0 โ‰ค ( 2 ยท ๐‘ ) )
58 34 36 24 41 57 letrd โŠข ( ๐œ‘ โ†’ 9 โ‰ค ( 2 ยท ๐‘ ) )
59 0re โŠข 0 โˆˆ โ„
60 9pos โŠข 0 < 9
61 59 33 60 ltleii โŠข 0 โ‰ค 9
62 33 61 pm3.2i โŠข ( 9 โˆˆ โ„ โˆง 0 โ‰ค 9 )
63 24 29 jca โŠข ( ๐œ‘ โ†’ ( ( 2 ยท ๐‘ ) โˆˆ โ„ โˆง 0 โ‰ค ( 2 ยท ๐‘ ) ) )
64 sqrtle โŠข ( ( ( 9 โˆˆ โ„ โˆง 0 โ‰ค 9 ) โˆง ( ( 2 ยท ๐‘ ) โˆˆ โ„ โˆง 0 โ‰ค ( 2 ยท ๐‘ ) ) ) โ†’ ( 9 โ‰ค ( 2 ยท ๐‘ ) โ†” ( โˆš โ€˜ 9 ) โ‰ค ( โˆš โ€˜ ( 2 ยท ๐‘ ) ) ) )
65 62 63 64 sylancr โŠข ( ๐œ‘ โ†’ ( 9 โ‰ค ( 2 ยท ๐‘ ) โ†” ( โˆš โ€˜ 9 ) โ‰ค ( โˆš โ€˜ ( 2 ยท ๐‘ ) ) ) )
66 58 65 mpbid โŠข ( ๐œ‘ โ†’ ( โˆš โ€˜ 9 ) โ‰ค ( โˆš โ€˜ ( 2 ยท ๐‘ ) ) )
67 32 66 eqbrtrrid โŠข ( ๐œ‘ โ†’ 3 โ‰ค ( โˆš โ€˜ ( 2 ยท ๐‘ ) ) )
68 3z โŠข 3 โˆˆ โ„ค
69 flge โŠข ( ( ( โˆš โ€˜ ( 2 ยท ๐‘ ) ) โˆˆ โ„ โˆง 3 โˆˆ โ„ค ) โ†’ ( 3 โ‰ค ( โˆš โ€˜ ( 2 ยท ๐‘ ) ) โ†” 3 โ‰ค ( โŒŠ โ€˜ ( โˆš โ€˜ ( 2 ยท ๐‘ ) ) ) ) )
70 30 68 69 sylancl โŠข ( ๐œ‘ โ†’ ( 3 โ‰ค ( โˆš โ€˜ ( 2 ยท ๐‘ ) ) โ†” 3 โ‰ค ( โŒŠ โ€˜ ( โˆš โ€˜ ( 2 ยท ๐‘ ) ) ) ) )
71 67 70 mpbid โŠข ( ๐œ‘ โ†’ 3 โ‰ค ( โŒŠ โ€˜ ( โˆš โ€˜ ( 2 ยท ๐‘ ) ) ) )
72 68 eluz1i โŠข ( ( โŒŠ โ€˜ ( โˆš โ€˜ ( 2 ยท ๐‘ ) ) ) โˆˆ ( โ„คโ‰ฅ โ€˜ 3 ) โ†” ( ( โŒŠ โ€˜ ( โˆš โ€˜ ( 2 ยท ๐‘ ) ) ) โˆˆ โ„ค โˆง 3 โ‰ค ( โŒŠ โ€˜ ( โˆš โ€˜ ( 2 ยท ๐‘ ) ) ) ) )
73 31 71 72 sylanbrc โŠข ( ๐œ‘ โ†’ ( โŒŠ โ€˜ ( โˆš โ€˜ ( 2 ยท ๐‘ ) ) ) โˆˆ ( โ„คโ‰ฅ โ€˜ 3 ) )
74 5 73 eqeltrid โŠข ( ๐œ‘ โ†’ ๐‘€ โˆˆ ( โ„คโ‰ฅ โ€˜ 3 ) )
75 eluznn โŠข ( ( 3 โˆˆ โ„• โˆง ๐‘€ โˆˆ ( โ„คโ‰ฅ โ€˜ 3 ) ) โ†’ ๐‘€ โˆˆ โ„• )
76 19 74 75 sylancr โŠข ( ๐œ‘ โ†’ ๐‘€ โˆˆ โ„• )
77 18 76 ffvelcdmd โŠข ( ๐œ‘ โ†’ ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘€ ) โˆˆ โ„• )
78 77 nnred โŠข ( ๐œ‘ โ†’ ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘€ ) โˆˆ โ„ )
79 76 nnred โŠข ( ๐œ‘ โ†’ ๐‘€ โˆˆ โ„ )
80 ppicl โŠข ( ๐‘€ โˆˆ โ„ โ†’ ( ฯ€ โ€˜ ๐‘€ ) โˆˆ โ„•0 )
81 79 80 syl โŠข ( ๐œ‘ โ†’ ( ฯ€ โ€˜ ๐‘€ ) โˆˆ โ„•0 )
82 27 81 nnexpcld โŠข ( ๐œ‘ โ†’ ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ๐‘€ ) ) โˆˆ โ„• )
83 82 nnred โŠข ( ๐œ‘ โ†’ ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ๐‘€ ) ) โˆˆ โ„ )
84 nndivre โŠข ( ( ( โˆš โ€˜ ( 2 ยท ๐‘ ) ) โˆˆ โ„ โˆง 3 โˆˆ โ„• ) โ†’ ( ( โˆš โ€˜ ( 2 ยท ๐‘ ) ) / 3 ) โˆˆ โ„ )
85 30 19 84 sylancl โŠข ( ๐œ‘ โ†’ ( ( โˆš โ€˜ ( 2 ยท ๐‘ ) ) / 3 ) โˆˆ โ„ )
86 readdcl โŠข ( ( ( ( โˆš โ€˜ ( 2 ยท ๐‘ ) ) / 3 ) โˆˆ โ„ โˆง 2 โˆˆ โ„ ) โ†’ ( ( ( โˆš โ€˜ ( 2 ยท ๐‘ ) ) / 3 ) + 2 ) โˆˆ โ„ )
87 85 50 86 sylancl โŠข ( ๐œ‘ โ†’ ( ( ( โˆš โ€˜ ( 2 ยท ๐‘ ) ) / 3 ) + 2 ) โˆˆ โ„ )
88 24 29 87 recxpcld โŠข ( ๐œ‘ โ†’ ( ( 2 ยท ๐‘ ) โ†‘๐‘ ( ( ( โˆš โ€˜ ( 2 ยท ๐‘ ) ) / 3 ) + 2 ) ) โˆˆ โ„ )
89 fveq2 โŠข ( ๐‘ฅ = 1 โ†’ ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘ฅ ) = ( seq 1 ( ยท , ๐น ) โ€˜ 1 ) )
90 fveq2 โŠข ( ๐‘ฅ = 1 โ†’ ( ฯ€ โ€˜ ๐‘ฅ ) = ( ฯ€ โ€˜ 1 ) )
91 ppi1 โŠข ( ฯ€ โ€˜ 1 ) = 0
92 90 91 eqtrdi โŠข ( ๐‘ฅ = 1 โ†’ ( ฯ€ โ€˜ ๐‘ฅ ) = 0 )
93 92 oveq2d โŠข ( ๐‘ฅ = 1 โ†’ ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ๐‘ฅ ) ) = ( ( 2 ยท ๐‘ ) โ†‘ 0 ) )
94 89 93 breq12d โŠข ( ๐‘ฅ = 1 โ†’ ( ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘ฅ ) โ‰ค ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ๐‘ฅ ) ) โ†” ( seq 1 ( ยท , ๐น ) โ€˜ 1 ) โ‰ค ( ( 2 ยท ๐‘ ) โ†‘ 0 ) ) )
95 94 imbi2d โŠข ( ๐‘ฅ = 1 โ†’ ( ( ๐œ‘ โ†’ ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘ฅ ) โ‰ค ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ๐‘ฅ ) ) ) โ†” ( ๐œ‘ โ†’ ( seq 1 ( ยท , ๐น ) โ€˜ 1 ) โ‰ค ( ( 2 ยท ๐‘ ) โ†‘ 0 ) ) ) )
96 fveq2 โŠข ( ๐‘ฅ = ๐‘˜ โ†’ ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘ฅ ) = ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) )
97 fveq2 โŠข ( ๐‘ฅ = ๐‘˜ โ†’ ( ฯ€ โ€˜ ๐‘ฅ ) = ( ฯ€ โ€˜ ๐‘˜ ) )
98 97 oveq2d โŠข ( ๐‘ฅ = ๐‘˜ โ†’ ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ๐‘ฅ ) ) = ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ๐‘˜ ) ) )
99 96 98 breq12d โŠข ( ๐‘ฅ = ๐‘˜ โ†’ ( ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘ฅ ) โ‰ค ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ๐‘ฅ ) ) โ†” ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) โ‰ค ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ๐‘˜ ) ) ) )
100 99 imbi2d โŠข ( ๐‘ฅ = ๐‘˜ โ†’ ( ( ๐œ‘ โ†’ ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘ฅ ) โ‰ค ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ๐‘ฅ ) ) ) โ†” ( ๐œ‘ โ†’ ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) โ‰ค ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ๐‘˜ ) ) ) ) )
101 fveq2 โŠข ( ๐‘ฅ = ( ๐‘˜ + 1 ) โ†’ ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘ฅ ) = ( seq 1 ( ยท , ๐น ) โ€˜ ( ๐‘˜ + 1 ) ) )
102 fveq2 โŠข ( ๐‘ฅ = ( ๐‘˜ + 1 ) โ†’ ( ฯ€ โ€˜ ๐‘ฅ ) = ( ฯ€ โ€˜ ( ๐‘˜ + 1 ) ) )
103 102 oveq2d โŠข ( ๐‘ฅ = ( ๐‘˜ + 1 ) โ†’ ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ๐‘ฅ ) ) = ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ( ๐‘˜ + 1 ) ) ) )
104 101 103 breq12d โŠข ( ๐‘ฅ = ( ๐‘˜ + 1 ) โ†’ ( ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘ฅ ) โ‰ค ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ๐‘ฅ ) ) โ†” ( seq 1 ( ยท , ๐น ) โ€˜ ( ๐‘˜ + 1 ) ) โ‰ค ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ( ๐‘˜ + 1 ) ) ) ) )
105 104 imbi2d โŠข ( ๐‘ฅ = ( ๐‘˜ + 1 ) โ†’ ( ( ๐œ‘ โ†’ ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘ฅ ) โ‰ค ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ๐‘ฅ ) ) ) โ†” ( ๐œ‘ โ†’ ( seq 1 ( ยท , ๐น ) โ€˜ ( ๐‘˜ + 1 ) ) โ‰ค ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ( ๐‘˜ + 1 ) ) ) ) ) )
106 fveq2 โŠข ( ๐‘ฅ = ๐‘€ โ†’ ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘ฅ ) = ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘€ ) )
107 fveq2 โŠข ( ๐‘ฅ = ๐‘€ โ†’ ( ฯ€ โ€˜ ๐‘ฅ ) = ( ฯ€ โ€˜ ๐‘€ ) )
108 107 oveq2d โŠข ( ๐‘ฅ = ๐‘€ โ†’ ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ๐‘ฅ ) ) = ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ๐‘€ ) ) )
109 106 108 breq12d โŠข ( ๐‘ฅ = ๐‘€ โ†’ ( ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘ฅ ) โ‰ค ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ๐‘ฅ ) ) โ†” ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘€ ) โ‰ค ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ๐‘€ ) ) ) )
110 109 imbi2d โŠข ( ๐‘ฅ = ๐‘€ โ†’ ( ( ๐œ‘ โ†’ ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘ฅ ) โ‰ค ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ๐‘ฅ ) ) ) โ†” ( ๐œ‘ โ†’ ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘€ ) โ‰ค ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ๐‘€ ) ) ) ) )
111 1z โŠข 1 โˆˆ โ„ค
112 seq1 โŠข ( 1 โˆˆ โ„ค โ†’ ( seq 1 ( ยท , ๐น ) โ€˜ 1 ) = ( ๐น โ€˜ 1 ) )
113 111 112 ax-mp โŠข ( seq 1 ( ยท , ๐น ) โ€˜ 1 ) = ( ๐น โ€˜ 1 )
114 1nn โŠข 1 โˆˆ โ„•
115 1nprm โŠข ยฌ 1 โˆˆ โ„™
116 eleq1 โŠข ( ๐‘› = 1 โ†’ ( ๐‘› โˆˆ โ„™ โ†” 1 โˆˆ โ„™ ) )
117 115 116 mtbiri โŠข ( ๐‘› = 1 โ†’ ยฌ ๐‘› โˆˆ โ„™ )
118 117 iffalsed โŠข ( ๐‘› = 1 โ†’ if ( ๐‘› โˆˆ โ„™ , ( ๐‘› โ†‘ ( ๐‘› pCnt ( ( 2 ยท ๐‘ ) C ๐‘ ) ) ) , 1 ) = 1 )
119 1ex โŠข 1 โˆˆ V
120 118 3 119 fvmpt โŠข ( 1 โˆˆ โ„• โ†’ ( ๐น โ€˜ 1 ) = 1 )
121 114 120 ax-mp โŠข ( ๐น โ€˜ 1 ) = 1
122 113 121 eqtri โŠข ( seq 1 ( ยท , ๐น ) โ€˜ 1 ) = 1
123 1le1 โŠข 1 โ‰ค 1
124 122 123 eqbrtri โŠข ( seq 1 ( ยท , ๐น ) โ€˜ 1 ) โ‰ค 1
125 23 zcnd โŠข ( ๐œ‘ โ†’ ( 2 ยท ๐‘ ) โˆˆ โ„‚ )
126 125 exp0d โŠข ( ๐œ‘ โ†’ ( ( 2 ยท ๐‘ ) โ†‘ 0 ) = 1 )
127 124 126 breqtrrid โŠข ( ๐œ‘ โ†’ ( seq 1 ( ยท , ๐น ) โ€˜ 1 ) โ‰ค ( ( 2 ยท ๐‘ ) โ†‘ 0 ) )
128 18 ffvelcdmda โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โ†’ ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) โˆˆ โ„• )
129 128 nnred โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โ†’ ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) โˆˆ โ„ )
130 129 adantr โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โˆง ( ๐‘˜ + 1 ) โˆˆ โ„™ ) โ†’ ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) โˆˆ โ„ )
131 27 ad2antrr โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โˆง ( ๐‘˜ + 1 ) โˆˆ โ„™ ) โ†’ ( 2 ยท ๐‘ ) โˆˆ โ„• )
132 nnre โŠข ( ๐‘˜ โˆˆ โ„• โ†’ ๐‘˜ โˆˆ โ„ )
133 132 ad2antlr โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โˆง ( ๐‘˜ + 1 ) โˆˆ โ„™ ) โ†’ ๐‘˜ โˆˆ โ„ )
134 ppicl โŠข ( ๐‘˜ โˆˆ โ„ โ†’ ( ฯ€ โ€˜ ๐‘˜ ) โˆˆ โ„•0 )
135 133 134 syl โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โˆง ( ๐‘˜ + 1 ) โˆˆ โ„™ ) โ†’ ( ฯ€ โ€˜ ๐‘˜ ) โˆˆ โ„•0 )
136 131 135 nnexpcld โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โˆง ( ๐‘˜ + 1 ) โˆˆ โ„™ ) โ†’ ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ๐‘˜ ) ) โˆˆ โ„• )
137 136 nnred โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โˆง ( ๐‘˜ + 1 ) โˆˆ โ„™ ) โ†’ ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ๐‘˜ ) ) โˆˆ โ„ )
138 nnre โŠข ( ( 2 ยท ๐‘ ) โˆˆ โ„• โ†’ ( 2 ยท ๐‘ ) โˆˆ โ„ )
139 nngt0 โŠข ( ( 2 ยท ๐‘ ) โˆˆ โ„• โ†’ 0 < ( 2 ยท ๐‘ ) )
140 138 139 jca โŠข ( ( 2 ยท ๐‘ ) โˆˆ โ„• โ†’ ( ( 2 ยท ๐‘ ) โˆˆ โ„ โˆง 0 < ( 2 ยท ๐‘ ) ) )
141 27 140 syl โŠข ( ๐œ‘ โ†’ ( ( 2 ยท ๐‘ ) โˆˆ โ„ โˆง 0 < ( 2 ยท ๐‘ ) ) )
142 141 ad2antrr โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โˆง ( ๐‘˜ + 1 ) โˆˆ โ„™ ) โ†’ ( ( 2 ยท ๐‘ ) โˆˆ โ„ โˆง 0 < ( 2 ยท ๐‘ ) ) )
143 lemul1 โŠข ( ( ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) โˆˆ โ„ โˆง ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ๐‘˜ ) ) โˆˆ โ„ โˆง ( ( 2 ยท ๐‘ ) โˆˆ โ„ โˆง 0 < ( 2 ยท ๐‘ ) ) ) โ†’ ( ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) โ‰ค ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ๐‘˜ ) ) โ†” ( ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) ยท ( 2 ยท ๐‘ ) ) โ‰ค ( ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ๐‘˜ ) ) ยท ( 2 ยท ๐‘ ) ) ) )
144 130 137 142 143 syl3anc โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โˆง ( ๐‘˜ + 1 ) โˆˆ โ„™ ) โ†’ ( ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) โ‰ค ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ๐‘˜ ) ) โ†” ( ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) ยท ( 2 ยท ๐‘ ) ) โ‰ค ( ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ๐‘˜ ) ) ยท ( 2 ยท ๐‘ ) ) ) )
145 nnz โŠข ( ๐‘˜ โˆˆ โ„• โ†’ ๐‘˜ โˆˆ โ„ค )
146 145 adantl โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โ†’ ๐‘˜ โˆˆ โ„ค )
147 ppiprm โŠข ( ( ๐‘˜ โˆˆ โ„ค โˆง ( ๐‘˜ + 1 ) โˆˆ โ„™ ) โ†’ ( ฯ€ โ€˜ ( ๐‘˜ + 1 ) ) = ( ( ฯ€ โ€˜ ๐‘˜ ) + 1 ) )
148 146 147 sylan โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โˆง ( ๐‘˜ + 1 ) โˆˆ โ„™ ) โ†’ ( ฯ€ โ€˜ ( ๐‘˜ + 1 ) ) = ( ( ฯ€ โ€˜ ๐‘˜ ) + 1 ) )
149 148 oveq2d โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โˆง ( ๐‘˜ + 1 ) โˆˆ โ„™ ) โ†’ ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ( ๐‘˜ + 1 ) ) ) = ( ( 2 ยท ๐‘ ) โ†‘ ( ( ฯ€ โ€˜ ๐‘˜ ) + 1 ) ) )
150 125 ad2antrr โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โˆง ( ๐‘˜ + 1 ) โˆˆ โ„™ ) โ†’ ( 2 ยท ๐‘ ) โˆˆ โ„‚ )
151 150 135 expp1d โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โˆง ( ๐‘˜ + 1 ) โˆˆ โ„™ ) โ†’ ( ( 2 ยท ๐‘ ) โ†‘ ( ( ฯ€ โ€˜ ๐‘˜ ) + 1 ) ) = ( ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ๐‘˜ ) ) ยท ( 2 ยท ๐‘ ) ) )
152 149 151 eqtrd โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โˆง ( ๐‘˜ + 1 ) โˆˆ โ„™ ) โ†’ ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ( ๐‘˜ + 1 ) ) ) = ( ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ๐‘˜ ) ) ยท ( 2 ยท ๐‘ ) ) )
153 152 breq2d โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โˆง ( ๐‘˜ + 1 ) โˆˆ โ„™ ) โ†’ ( ( ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) ยท ( 2 ยท ๐‘ ) ) โ‰ค ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ( ๐‘˜ + 1 ) ) ) โ†” ( ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) ยท ( 2 ยท ๐‘ ) ) โ‰ค ( ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ๐‘˜ ) ) ยท ( 2 ยท ๐‘ ) ) ) )
154 144 153 bitr4d โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โˆง ( ๐‘˜ + 1 ) โˆˆ โ„™ ) โ†’ ( ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) โ‰ค ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ๐‘˜ ) ) โ†” ( ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) ยท ( 2 ยท ๐‘ ) ) โ‰ค ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ( ๐‘˜ + 1 ) ) ) ) )
155 simpr โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โ†’ ๐‘˜ โˆˆ โ„• )
156 nnuz โŠข โ„• = ( โ„คโ‰ฅ โ€˜ 1 )
157 155 156 eleqtrdi โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โ†’ ๐‘˜ โˆˆ ( โ„คโ‰ฅ โ€˜ 1 ) )
158 seqp1 โŠข ( ๐‘˜ โˆˆ ( โ„คโ‰ฅ โ€˜ 1 ) โ†’ ( seq 1 ( ยท , ๐น ) โ€˜ ( ๐‘˜ + 1 ) ) = ( ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) ยท ( ๐น โ€˜ ( ๐‘˜ + 1 ) ) ) )
159 157 158 syl โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โ†’ ( seq 1 ( ยท , ๐น ) โ€˜ ( ๐‘˜ + 1 ) ) = ( ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) ยท ( ๐น โ€˜ ( ๐‘˜ + 1 ) ) ) )
160 159 adantr โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โˆง ( ๐‘˜ + 1 ) โˆˆ โ„™ ) โ†’ ( seq 1 ( ยท , ๐น ) โ€˜ ( ๐‘˜ + 1 ) ) = ( ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) ยท ( ๐น โ€˜ ( ๐‘˜ + 1 ) ) ) )
161 peano2nn โŠข ( ๐‘˜ โˆˆ โ„• โ†’ ( ๐‘˜ + 1 ) โˆˆ โ„• )
162 161 adantl โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โ†’ ( ๐‘˜ + 1 ) โˆˆ โ„• )
163 eleq1 โŠข ( ๐‘› = ( ๐‘˜ + 1 ) โ†’ ( ๐‘› โˆˆ โ„™ โ†” ( ๐‘˜ + 1 ) โˆˆ โ„™ ) )
164 id โŠข ( ๐‘› = ( ๐‘˜ + 1 ) โ†’ ๐‘› = ( ๐‘˜ + 1 ) )
165 oveq1 โŠข ( ๐‘› = ( ๐‘˜ + 1 ) โ†’ ( ๐‘› pCnt ( ( 2 ยท ๐‘ ) C ๐‘ ) ) = ( ( ๐‘˜ + 1 ) pCnt ( ( 2 ยท ๐‘ ) C ๐‘ ) ) )
166 164 165 oveq12d โŠข ( ๐‘› = ( ๐‘˜ + 1 ) โ†’ ( ๐‘› โ†‘ ( ๐‘› pCnt ( ( 2 ยท ๐‘ ) C ๐‘ ) ) ) = ( ( ๐‘˜ + 1 ) โ†‘ ( ( ๐‘˜ + 1 ) pCnt ( ( 2 ยท ๐‘ ) C ๐‘ ) ) ) )
167 163 166 ifbieq1d โŠข ( ๐‘› = ( ๐‘˜ + 1 ) โ†’ if ( ๐‘› โˆˆ โ„™ , ( ๐‘› โ†‘ ( ๐‘› pCnt ( ( 2 ยท ๐‘ ) C ๐‘ ) ) ) , 1 ) = if ( ( ๐‘˜ + 1 ) โˆˆ โ„™ , ( ( ๐‘˜ + 1 ) โ†‘ ( ( ๐‘˜ + 1 ) pCnt ( ( 2 ยท ๐‘ ) C ๐‘ ) ) ) , 1 ) )
168 ovex โŠข ( ( ๐‘˜ + 1 ) โ†‘ ( ( ๐‘˜ + 1 ) pCnt ( ( 2 ยท ๐‘ ) C ๐‘ ) ) ) โˆˆ V
169 168 119 ifex โŠข if ( ( ๐‘˜ + 1 ) โˆˆ โ„™ , ( ( ๐‘˜ + 1 ) โ†‘ ( ( ๐‘˜ + 1 ) pCnt ( ( 2 ยท ๐‘ ) C ๐‘ ) ) ) , 1 ) โˆˆ V
170 167 3 169 fvmpt โŠข ( ( ๐‘˜ + 1 ) โˆˆ โ„• โ†’ ( ๐น โ€˜ ( ๐‘˜ + 1 ) ) = if ( ( ๐‘˜ + 1 ) โˆˆ โ„™ , ( ( ๐‘˜ + 1 ) โ†‘ ( ( ๐‘˜ + 1 ) pCnt ( ( 2 ยท ๐‘ ) C ๐‘ ) ) ) , 1 ) )
171 162 170 syl โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โ†’ ( ๐น โ€˜ ( ๐‘˜ + 1 ) ) = if ( ( ๐‘˜ + 1 ) โˆˆ โ„™ , ( ( ๐‘˜ + 1 ) โ†‘ ( ( ๐‘˜ + 1 ) pCnt ( ( 2 ยท ๐‘ ) C ๐‘ ) ) ) , 1 ) )
172 iftrue โŠข ( ( ๐‘˜ + 1 ) โˆˆ โ„™ โ†’ if ( ( ๐‘˜ + 1 ) โˆˆ โ„™ , ( ( ๐‘˜ + 1 ) โ†‘ ( ( ๐‘˜ + 1 ) pCnt ( ( 2 ยท ๐‘ ) C ๐‘ ) ) ) , 1 ) = ( ( ๐‘˜ + 1 ) โ†‘ ( ( ๐‘˜ + 1 ) pCnt ( ( 2 ยท ๐‘ ) C ๐‘ ) ) ) )
173 171 172 sylan9eq โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โˆง ( ๐‘˜ + 1 ) โˆˆ โ„™ ) โ†’ ( ๐น โ€˜ ( ๐‘˜ + 1 ) ) = ( ( ๐‘˜ + 1 ) โ†‘ ( ( ๐‘˜ + 1 ) pCnt ( ( 2 ยท ๐‘ ) C ๐‘ ) ) ) )
174 9 adantr โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โ†’ ๐‘ โˆˆ โ„• )
175 bposlem1 โŠข ( ( ๐‘ โˆˆ โ„• โˆง ( ๐‘˜ + 1 ) โˆˆ โ„™ ) โ†’ ( ( ๐‘˜ + 1 ) โ†‘ ( ( ๐‘˜ + 1 ) pCnt ( ( 2 ยท ๐‘ ) C ๐‘ ) ) ) โ‰ค ( 2 ยท ๐‘ ) )
176 174 175 sylan โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โˆง ( ๐‘˜ + 1 ) โˆˆ โ„™ ) โ†’ ( ( ๐‘˜ + 1 ) โ†‘ ( ( ๐‘˜ + 1 ) pCnt ( ( 2 ยท ๐‘ ) C ๐‘ ) ) ) โ‰ค ( 2 ยท ๐‘ ) )
177 173 176 eqbrtrd โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โˆง ( ๐‘˜ + 1 ) โˆˆ โ„™ ) โ†’ ( ๐น โ€˜ ( ๐‘˜ + 1 ) ) โ‰ค ( 2 ยท ๐‘ ) )
178 17 simpld โŠข ( ๐œ‘ โ†’ ๐น : โ„• โŸถ โ„• )
179 ffvelcdm โŠข ( ( ๐น : โ„• โŸถ โ„• โˆง ( ๐‘˜ + 1 ) โˆˆ โ„• ) โ†’ ( ๐น โ€˜ ( ๐‘˜ + 1 ) ) โˆˆ โ„• )
180 178 161 179 syl2an โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โ†’ ( ๐น โ€˜ ( ๐‘˜ + 1 ) ) โˆˆ โ„• )
181 180 nnred โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โ†’ ( ๐น โ€˜ ( ๐‘˜ + 1 ) ) โˆˆ โ„ )
182 181 adantr โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โˆง ( ๐‘˜ + 1 ) โˆˆ โ„™ ) โ†’ ( ๐น โ€˜ ( ๐‘˜ + 1 ) ) โˆˆ โ„ )
183 24 ad2antrr โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โˆง ( ๐‘˜ + 1 ) โˆˆ โ„™ ) โ†’ ( 2 ยท ๐‘ ) โˆˆ โ„ )
184 nnre โŠข ( ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) โˆˆ โ„• โ†’ ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) โˆˆ โ„ )
185 nngt0 โŠข ( ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) โˆˆ โ„• โ†’ 0 < ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) )
186 184 185 jca โŠข ( ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) โˆˆ โ„• โ†’ ( ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) โˆˆ โ„ โˆง 0 < ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) ) )
187 128 186 syl โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โ†’ ( ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) โˆˆ โ„ โˆง 0 < ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) ) )
188 187 adantr โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โˆง ( ๐‘˜ + 1 ) โˆˆ โ„™ ) โ†’ ( ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) โˆˆ โ„ โˆง 0 < ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) ) )
189 lemul2 โŠข ( ( ( ๐น โ€˜ ( ๐‘˜ + 1 ) ) โˆˆ โ„ โˆง ( 2 ยท ๐‘ ) โˆˆ โ„ โˆง ( ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) โˆˆ โ„ โˆง 0 < ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) ) ) โ†’ ( ( ๐น โ€˜ ( ๐‘˜ + 1 ) ) โ‰ค ( 2 ยท ๐‘ ) โ†” ( ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) ยท ( ๐น โ€˜ ( ๐‘˜ + 1 ) ) ) โ‰ค ( ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) ยท ( 2 ยท ๐‘ ) ) ) )
190 182 183 188 189 syl3anc โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โˆง ( ๐‘˜ + 1 ) โˆˆ โ„™ ) โ†’ ( ( ๐น โ€˜ ( ๐‘˜ + 1 ) ) โ‰ค ( 2 ยท ๐‘ ) โ†” ( ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) ยท ( ๐น โ€˜ ( ๐‘˜ + 1 ) ) ) โ‰ค ( ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) ยท ( 2 ยท ๐‘ ) ) ) )
191 177 190 mpbid โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โˆง ( ๐‘˜ + 1 ) โˆˆ โ„™ ) โ†’ ( ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) ยท ( ๐น โ€˜ ( ๐‘˜ + 1 ) ) ) โ‰ค ( ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) ยท ( 2 ยท ๐‘ ) ) )
192 160 191 eqbrtrd โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โˆง ( ๐‘˜ + 1 ) โˆˆ โ„™ ) โ†’ ( seq 1 ( ยท , ๐น ) โ€˜ ( ๐‘˜ + 1 ) ) โ‰ค ( ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) ยท ( 2 ยท ๐‘ ) ) )
193 ffvelcdm โŠข ( ( seq 1 ( ยท , ๐น ) : โ„• โŸถ โ„• โˆง ( ๐‘˜ + 1 ) โˆˆ โ„• ) โ†’ ( seq 1 ( ยท , ๐น ) โ€˜ ( ๐‘˜ + 1 ) ) โˆˆ โ„• )
194 18 161 193 syl2an โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โ†’ ( seq 1 ( ยท , ๐น ) โ€˜ ( ๐‘˜ + 1 ) ) โˆˆ โ„• )
195 194 nnred โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โ†’ ( seq 1 ( ยท , ๐น ) โ€˜ ( ๐‘˜ + 1 ) ) โˆˆ โ„ )
196 27 adantr โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โ†’ ( 2 ยท ๐‘ ) โˆˆ โ„• )
197 128 196 nnmulcld โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โ†’ ( ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) ยท ( 2 ยท ๐‘ ) ) โˆˆ โ„• )
198 197 nnred โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โ†’ ( ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) ยท ( 2 ยท ๐‘ ) ) โˆˆ โ„ )
199 162 nnred โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โ†’ ( ๐‘˜ + 1 ) โˆˆ โ„ )
200 ppicl โŠข ( ( ๐‘˜ + 1 ) โˆˆ โ„ โ†’ ( ฯ€ โ€˜ ( ๐‘˜ + 1 ) ) โˆˆ โ„•0 )
201 199 200 syl โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โ†’ ( ฯ€ โ€˜ ( ๐‘˜ + 1 ) ) โˆˆ โ„•0 )
202 196 201 nnexpcld โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โ†’ ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ( ๐‘˜ + 1 ) ) ) โˆˆ โ„• )
203 202 nnred โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โ†’ ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ( ๐‘˜ + 1 ) ) ) โˆˆ โ„ )
204 letr โŠข ( ( ( seq 1 ( ยท , ๐น ) โ€˜ ( ๐‘˜ + 1 ) ) โˆˆ โ„ โˆง ( ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) ยท ( 2 ยท ๐‘ ) ) โˆˆ โ„ โˆง ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ( ๐‘˜ + 1 ) ) ) โˆˆ โ„ ) โ†’ ( ( ( seq 1 ( ยท , ๐น ) โ€˜ ( ๐‘˜ + 1 ) ) โ‰ค ( ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) ยท ( 2 ยท ๐‘ ) ) โˆง ( ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) ยท ( 2 ยท ๐‘ ) ) โ‰ค ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ( ๐‘˜ + 1 ) ) ) ) โ†’ ( seq 1 ( ยท , ๐น ) โ€˜ ( ๐‘˜ + 1 ) ) โ‰ค ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ( ๐‘˜ + 1 ) ) ) ) )
205 195 198 203 204 syl3anc โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โ†’ ( ( ( seq 1 ( ยท , ๐น ) โ€˜ ( ๐‘˜ + 1 ) ) โ‰ค ( ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) ยท ( 2 ยท ๐‘ ) ) โˆง ( ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) ยท ( 2 ยท ๐‘ ) ) โ‰ค ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ( ๐‘˜ + 1 ) ) ) ) โ†’ ( seq 1 ( ยท , ๐น ) โ€˜ ( ๐‘˜ + 1 ) ) โ‰ค ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ( ๐‘˜ + 1 ) ) ) ) )
206 205 adantr โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โˆง ( ๐‘˜ + 1 ) โˆˆ โ„™ ) โ†’ ( ( ( seq 1 ( ยท , ๐น ) โ€˜ ( ๐‘˜ + 1 ) ) โ‰ค ( ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) ยท ( 2 ยท ๐‘ ) ) โˆง ( ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) ยท ( 2 ยท ๐‘ ) ) โ‰ค ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ( ๐‘˜ + 1 ) ) ) ) โ†’ ( seq 1 ( ยท , ๐น ) โ€˜ ( ๐‘˜ + 1 ) ) โ‰ค ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ( ๐‘˜ + 1 ) ) ) ) )
207 192 206 mpand โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โˆง ( ๐‘˜ + 1 ) โˆˆ โ„™ ) โ†’ ( ( ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) ยท ( 2 ยท ๐‘ ) ) โ‰ค ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ( ๐‘˜ + 1 ) ) ) โ†’ ( seq 1 ( ยท , ๐น ) โ€˜ ( ๐‘˜ + 1 ) ) โ‰ค ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ( ๐‘˜ + 1 ) ) ) ) )
208 154 207 sylbid โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โˆง ( ๐‘˜ + 1 ) โˆˆ โ„™ ) โ†’ ( ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) โ‰ค ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ๐‘˜ ) ) โ†’ ( seq 1 ( ยท , ๐น ) โ€˜ ( ๐‘˜ + 1 ) ) โ‰ค ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ( ๐‘˜ + 1 ) ) ) ) )
209 159 adantr โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โˆง ยฌ ( ๐‘˜ + 1 ) โˆˆ โ„™ ) โ†’ ( seq 1 ( ยท , ๐น ) โ€˜ ( ๐‘˜ + 1 ) ) = ( ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) ยท ( ๐น โ€˜ ( ๐‘˜ + 1 ) ) ) )
210 iffalse โŠข ( ยฌ ( ๐‘˜ + 1 ) โˆˆ โ„™ โ†’ if ( ( ๐‘˜ + 1 ) โˆˆ โ„™ , ( ( ๐‘˜ + 1 ) โ†‘ ( ( ๐‘˜ + 1 ) pCnt ( ( 2 ยท ๐‘ ) C ๐‘ ) ) ) , 1 ) = 1 )
211 171 210 sylan9eq โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โˆง ยฌ ( ๐‘˜ + 1 ) โˆˆ โ„™ ) โ†’ ( ๐น โ€˜ ( ๐‘˜ + 1 ) ) = 1 )
212 211 oveq2d โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โˆง ยฌ ( ๐‘˜ + 1 ) โˆˆ โ„™ ) โ†’ ( ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) ยท ( ๐น โ€˜ ( ๐‘˜ + 1 ) ) ) = ( ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) ยท 1 ) )
213 128 adantr โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โˆง ยฌ ( ๐‘˜ + 1 ) โˆˆ โ„™ ) โ†’ ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) โˆˆ โ„• )
214 213 nncnd โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โˆง ยฌ ( ๐‘˜ + 1 ) โˆˆ โ„™ ) โ†’ ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) โˆˆ โ„‚ )
215 214 mulridd โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โˆง ยฌ ( ๐‘˜ + 1 ) โˆˆ โ„™ ) โ†’ ( ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) ยท 1 ) = ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) )
216 209 212 215 3eqtrd โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โˆง ยฌ ( ๐‘˜ + 1 ) โˆˆ โ„™ ) โ†’ ( seq 1 ( ยท , ๐น ) โ€˜ ( ๐‘˜ + 1 ) ) = ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) )
217 ppinprm โŠข ( ( ๐‘˜ โˆˆ โ„ค โˆง ยฌ ( ๐‘˜ + 1 ) โˆˆ โ„™ ) โ†’ ( ฯ€ โ€˜ ( ๐‘˜ + 1 ) ) = ( ฯ€ โ€˜ ๐‘˜ ) )
218 146 217 sylan โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โˆง ยฌ ( ๐‘˜ + 1 ) โˆˆ โ„™ ) โ†’ ( ฯ€ โ€˜ ( ๐‘˜ + 1 ) ) = ( ฯ€ โ€˜ ๐‘˜ ) )
219 218 oveq2d โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โˆง ยฌ ( ๐‘˜ + 1 ) โˆˆ โ„™ ) โ†’ ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ( ๐‘˜ + 1 ) ) ) = ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ๐‘˜ ) ) )
220 216 219 breq12d โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โˆง ยฌ ( ๐‘˜ + 1 ) โˆˆ โ„™ ) โ†’ ( ( seq 1 ( ยท , ๐น ) โ€˜ ( ๐‘˜ + 1 ) ) โ‰ค ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ( ๐‘˜ + 1 ) ) ) โ†” ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) โ‰ค ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ๐‘˜ ) ) ) )
221 220 biimprd โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โˆง ยฌ ( ๐‘˜ + 1 ) โˆˆ โ„™ ) โ†’ ( ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) โ‰ค ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ๐‘˜ ) ) โ†’ ( seq 1 ( ยท , ๐น ) โ€˜ ( ๐‘˜ + 1 ) ) โ‰ค ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ( ๐‘˜ + 1 ) ) ) ) )
222 208 221 pm2.61dan โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„• ) โ†’ ( ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) โ‰ค ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ๐‘˜ ) ) โ†’ ( seq 1 ( ยท , ๐น ) โ€˜ ( ๐‘˜ + 1 ) ) โ‰ค ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ( ๐‘˜ + 1 ) ) ) ) )
223 222 expcom โŠข ( ๐‘˜ โˆˆ โ„• โ†’ ( ๐œ‘ โ†’ ( ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) โ‰ค ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ๐‘˜ ) ) โ†’ ( seq 1 ( ยท , ๐น ) โ€˜ ( ๐‘˜ + 1 ) ) โ‰ค ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ( ๐‘˜ + 1 ) ) ) ) ) )
224 223 a2d โŠข ( ๐‘˜ โˆˆ โ„• โ†’ ( ( ๐œ‘ โ†’ ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘˜ ) โ‰ค ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ๐‘˜ ) ) ) โ†’ ( ๐œ‘ โ†’ ( seq 1 ( ยท , ๐น ) โ€˜ ( ๐‘˜ + 1 ) ) โ‰ค ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ( ๐‘˜ + 1 ) ) ) ) ) )
225 95 100 105 110 127 224 nnind โŠข ( ๐‘€ โˆˆ โ„• โ†’ ( ๐œ‘ โ†’ ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘€ ) โ‰ค ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ๐‘€ ) ) ) )
226 76 225 mpcom โŠข ( ๐œ‘ โ†’ ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘€ ) โ‰ค ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ๐‘€ ) ) )
227 cxpexp โŠข ( ( ( 2 ยท ๐‘ ) โˆˆ โ„‚ โˆง ( ฯ€ โ€˜ ๐‘€ ) โˆˆ โ„•0 ) โ†’ ( ( 2 ยท ๐‘ ) โ†‘๐‘ ( ฯ€ โ€˜ ๐‘€ ) ) = ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ๐‘€ ) ) )
228 125 81 227 syl2anc โŠข ( ๐œ‘ โ†’ ( ( 2 ยท ๐‘ ) โ†‘๐‘ ( ฯ€ โ€˜ ๐‘€ ) ) = ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ๐‘€ ) ) )
229 81 nn0red โŠข ( ๐œ‘ โ†’ ( ฯ€ โ€˜ ๐‘€ ) โˆˆ โ„ )
230 nndivre โŠข ( ( ๐‘€ โˆˆ โ„ โˆง 3 โˆˆ โ„• ) โ†’ ( ๐‘€ / 3 ) โˆˆ โ„ )
231 79 19 230 sylancl โŠข ( ๐œ‘ โ†’ ( ๐‘€ / 3 ) โˆˆ โ„ )
232 readdcl โŠข ( ( ( ๐‘€ / 3 ) โˆˆ โ„ โˆง 2 โˆˆ โ„ ) โ†’ ( ( ๐‘€ / 3 ) + 2 ) โˆˆ โ„ )
233 231 50 232 sylancl โŠข ( ๐œ‘ โ†’ ( ( ๐‘€ / 3 ) + 2 ) โˆˆ โ„ )
234 76 nnnn0d โŠข ( ๐œ‘ โ†’ ๐‘€ โˆˆ โ„•0 )
235 234 nn0ge0d โŠข ( ๐œ‘ โ†’ 0 โ‰ค ๐‘€ )
236 ppiub โŠข ( ( ๐‘€ โˆˆ โ„ โˆง 0 โ‰ค ๐‘€ ) โ†’ ( ฯ€ โ€˜ ๐‘€ ) โ‰ค ( ( ๐‘€ / 3 ) + 2 ) )
237 79 235 236 syl2anc โŠข ( ๐œ‘ โ†’ ( ฯ€ โ€˜ ๐‘€ ) โ‰ค ( ( ๐‘€ / 3 ) + 2 ) )
238 50 a1i โŠข ( ๐œ‘ โ†’ 2 โˆˆ โ„ )
239 flle โŠข ( ( โˆš โ€˜ ( 2 ยท ๐‘ ) ) โˆˆ โ„ โ†’ ( โŒŠ โ€˜ ( โˆš โ€˜ ( 2 ยท ๐‘ ) ) ) โ‰ค ( โˆš โ€˜ ( 2 ยท ๐‘ ) ) )
240 30 239 syl โŠข ( ๐œ‘ โ†’ ( โŒŠ โ€˜ ( โˆš โ€˜ ( 2 ยท ๐‘ ) ) ) โ‰ค ( โˆš โ€˜ ( 2 ยท ๐‘ ) ) )
241 5 240 eqbrtrid โŠข ( ๐œ‘ โ†’ ๐‘€ โ‰ค ( โˆš โ€˜ ( 2 ยท ๐‘ ) ) )
242 3re โŠข 3 โˆˆ โ„
243 3pos โŠข 0 < 3
244 242 243 pm3.2i โŠข ( 3 โˆˆ โ„ โˆง 0 < 3 )
245 244 a1i โŠข ( ๐œ‘ โ†’ ( 3 โˆˆ โ„ โˆง 0 < 3 ) )
246 lediv1 โŠข ( ( ๐‘€ โˆˆ โ„ โˆง ( โˆš โ€˜ ( 2 ยท ๐‘ ) ) โˆˆ โ„ โˆง ( 3 โˆˆ โ„ โˆง 0 < 3 ) ) โ†’ ( ๐‘€ โ‰ค ( โˆš โ€˜ ( 2 ยท ๐‘ ) ) โ†” ( ๐‘€ / 3 ) โ‰ค ( ( โˆš โ€˜ ( 2 ยท ๐‘ ) ) / 3 ) ) )
247 79 30 245 246 syl3anc โŠข ( ๐œ‘ โ†’ ( ๐‘€ โ‰ค ( โˆš โ€˜ ( 2 ยท ๐‘ ) ) โ†” ( ๐‘€ / 3 ) โ‰ค ( ( โˆš โ€˜ ( 2 ยท ๐‘ ) ) / 3 ) ) )
248 241 247 mpbid โŠข ( ๐œ‘ โ†’ ( ๐‘€ / 3 ) โ‰ค ( ( โˆš โ€˜ ( 2 ยท ๐‘ ) ) / 3 ) )
249 231 85 238 248 leadd1dd โŠข ( ๐œ‘ โ†’ ( ( ๐‘€ / 3 ) + 2 ) โ‰ค ( ( ( โˆš โ€˜ ( 2 ยท ๐‘ ) ) / 3 ) + 2 ) )
250 229 233 87 237 249 letrd โŠข ( ๐œ‘ โ†’ ( ฯ€ โ€˜ ๐‘€ ) โ‰ค ( ( ( โˆš โ€˜ ( 2 ยท ๐‘ ) ) / 3 ) + 2 ) )
251 2t1e2 โŠข ( 2 ยท 1 ) = 2
252 9 nnge1d โŠข ( ๐œ‘ โ†’ 1 โ‰ค ๐‘ )
253 1re โŠข 1 โˆˆ โ„
254 lemul2 โŠข ( ( 1 โˆˆ โ„ โˆง ๐‘ โˆˆ โ„ โˆง ( 2 โˆˆ โ„ โˆง 0 < 2 ) ) โ†’ ( 1 โ‰ค ๐‘ โ†” ( 2 ยท 1 ) โ‰ค ( 2 ยท ๐‘ ) ) )
255 253 52 254 mp3an13 โŠข ( ๐‘ โˆˆ โ„ โ†’ ( 1 โ‰ค ๐‘ โ†” ( 2 ยท 1 ) โ‰ค ( 2 ยท ๐‘ ) ) )
256 48 255 syl โŠข ( ๐œ‘ โ†’ ( 1 โ‰ค ๐‘ โ†” ( 2 ยท 1 ) โ‰ค ( 2 ยท ๐‘ ) ) )
257 252 256 mpbid โŠข ( ๐œ‘ โ†’ ( 2 ยท 1 ) โ‰ค ( 2 ยท ๐‘ ) )
258 251 257 eqbrtrrid โŠข ( ๐œ‘ โ†’ 2 โ‰ค ( 2 ยท ๐‘ ) )
259 20 eluz1i โŠข ( ( 2 ยท ๐‘ ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†” ( ( 2 ยท ๐‘ ) โˆˆ โ„ค โˆง 2 โ‰ค ( 2 ยท ๐‘ ) ) )
260 23 258 259 sylanbrc โŠข ( ๐œ‘ โ†’ ( 2 ยท ๐‘ ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) )
261 eluz2gt1 โŠข ( ( 2 ยท ๐‘ ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ 1 < ( 2 ยท ๐‘ ) )
262 260 261 syl โŠข ( ๐œ‘ โ†’ 1 < ( 2 ยท ๐‘ ) )
263 24 262 229 87 cxpled โŠข ( ๐œ‘ โ†’ ( ( ฯ€ โ€˜ ๐‘€ ) โ‰ค ( ( ( โˆš โ€˜ ( 2 ยท ๐‘ ) ) / 3 ) + 2 ) โ†” ( ( 2 ยท ๐‘ ) โ†‘๐‘ ( ฯ€ โ€˜ ๐‘€ ) ) โ‰ค ( ( 2 ยท ๐‘ ) โ†‘๐‘ ( ( ( โˆš โ€˜ ( 2 ยท ๐‘ ) ) / 3 ) + 2 ) ) ) )
264 250 263 mpbid โŠข ( ๐œ‘ โ†’ ( ( 2 ยท ๐‘ ) โ†‘๐‘ ( ฯ€ โ€˜ ๐‘€ ) ) โ‰ค ( ( 2 ยท ๐‘ ) โ†‘๐‘ ( ( ( โˆš โ€˜ ( 2 ยท ๐‘ ) ) / 3 ) + 2 ) ) )
265 228 264 eqbrtrrd โŠข ( ๐œ‘ โ†’ ( ( 2 ยท ๐‘ ) โ†‘ ( ฯ€ โ€˜ ๐‘€ ) ) โ‰ค ( ( 2 ยท ๐‘ ) โ†‘๐‘ ( ( ( โˆš โ€˜ ( 2 ยท ๐‘ ) ) / 3 ) + 2 ) ) )
266 78 83 88 226 265 letrd โŠข ( ๐œ‘ โ†’ ( seq 1 ( ยท , ๐น ) โ€˜ ๐‘€ ) โ‰ค ( ( 2 ยท ๐‘ ) โ†‘๐‘ ( ( ( โˆš โ€˜ ( 2 ยท ๐‘ ) ) / 3 ) + 2 ) ) )