Metamath Proof Explorer

Theorem perfectALTVlem2

Description: Lemma for perfectALTV . (Contributed by Mario Carneiro, 17-May-2016) (Revised by AV, 1-Jul-2020)

Ref Expression
Hypotheses perfectALTVlem.1 
|- ( ph -> A e. NN )
perfectALTVlem.2 
|- ( ph -> B e. NN )
perfectALTVlem.3 
|- ( ph -> B e. Odd )
perfectALTVlem.4 
|- ( ph -> ( 1 sigma ( ( 2 ^ A ) x. B ) ) = ( 2 x. ( ( 2 ^ A ) x. B ) ) )
Assertion perfectALTVlem2 
|- ( ph -> ( B e. Prime /\ B = ( ( 2 ^ ( A + 1 ) ) - 1 ) ) )

Proof

Step Hyp Ref Expression
1 perfectALTVlem.1 
 |-  ( ph -> A e. NN )
2 perfectALTVlem.2 
 |-  ( ph -> B e. NN )
3 perfectALTVlem.3 
 |-  ( ph -> B e. Odd )
4 perfectALTVlem.4 
 |-  ( ph -> ( 1 sigma ( ( 2 ^ A ) x. B ) ) = ( 2 x. ( ( 2 ^ A ) x. B ) ) )
5 1re 
 |-  1 e. RR
6 5 a1i 
 |-  ( ph -> 1 e. RR )
7 1 2 3 4 perfectALTVlem1 
 |-  ( ph -> ( ( 2 ^ ( A + 1 ) ) e. NN /\ ( ( 2 ^ ( A + 1 ) ) - 1 ) e. NN /\ ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) e. NN ) )
8 7 simp3d 
 |-  ( ph -> ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) e. NN )
9 8 nnred 
 |-  ( ph -> ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) e. RR )
10 2 nnred 
 |-  ( ph -> B e. RR )
11 8 nnge1d 
 |-  ( ph -> 1 <_ ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) )
12 2cn 
 |-  2 e. CC
13 exp1 
 |-  ( 2 e. CC -> ( 2 ^ 1 ) = 2 )
14 12 13 ax-mp 
 |-  ( 2 ^ 1 ) = 2
15 df-2 
 |-  2 = ( 1 + 1 )
16 14 15 eqtri 
 |-  ( 2 ^ 1 ) = ( 1 + 1 )
17 2re 
 |-  2 e. RR
18 17 a1i 
 |-  ( ph -> 2 e. RR )
19 1zzd 
 |-  ( ph -> 1 e. ZZ )
20 1 peano2nnd 
 |-  ( ph -> ( A + 1 ) e. NN )
21 20 nnzd 
 |-  ( ph -> ( A + 1 ) e. ZZ )
22 1lt2 
 |-  1 < 2
23 22 a1i 
 |-  ( ph -> 1 < 2 )
24 1 nnrpd 
 |-  ( ph -> A e. RR+ )
25 ltaddrp 
 |-  ( ( 1 e. RR /\ A e. RR+ ) -> 1 < ( 1 + A ) )
26 5 24 25 sylancr 
 |-  ( ph -> 1 < ( 1 + A ) )
27 ax-1cn 
 |-  1 e. CC
28 1 nncnd 
 |-  ( ph -> A e. CC )
29 addcom 
 |-  ( ( 1 e. CC /\ A e. CC ) -> ( 1 + A ) = ( A + 1 ) )
30 27 28 29 sylancr 
 |-  ( ph -> ( 1 + A ) = ( A + 1 ) )
31 26 30 breqtrd 
 |-  ( ph -> 1 < ( A + 1 ) )
32 ltexp2a 
 |-  ( ( ( 2 e. RR /\ 1 e. ZZ /\ ( A + 1 ) e. ZZ ) /\ ( 1 < 2 /\ 1 < ( A + 1 ) ) ) -> ( 2 ^ 1 ) < ( 2 ^ ( A + 1 ) ) )
33 18 19 21 23 31 32 syl32anc 
 |-  ( ph -> ( 2 ^ 1 ) < ( 2 ^ ( A + 1 ) ) )
34 16 33 eqbrtrrid 
 |-  ( ph -> ( 1 + 1 ) < ( 2 ^ ( A + 1 ) ) )
35 7 simp1d 
 |-  ( ph -> ( 2 ^ ( A + 1 ) ) e. NN )
36 35 nnred 
 |-  ( ph -> ( 2 ^ ( A + 1 ) ) e. RR )
37 6 6 36 ltaddsubd 
 |-  ( ph -> ( ( 1 + 1 ) < ( 2 ^ ( A + 1 ) ) <-> 1 < ( ( 2 ^ ( A + 1 ) ) - 1 ) ) )
38 34 37 mpbid 
 |-  ( ph -> 1 < ( ( 2 ^ ( A + 1 ) ) - 1 ) )
39 1rp 
 |-  1 e. RR+
40 39 a1i 
 |-  ( ph -> 1 e. RR+ )
41 peano2rem 
 |-  ( ( 2 ^ ( A + 1 ) ) e. RR -> ( ( 2 ^ ( A + 1 ) ) - 1 ) e. RR )
42 36 41 syl 
 |-  ( ph -> ( ( 2 ^ ( A + 1 ) ) - 1 ) e. RR )
43 expgt1 
 |-  ( ( 2 e. RR /\ ( A + 1 ) e. NN /\ 1 < 2 ) -> 1 < ( 2 ^ ( A + 1 ) ) )
44 18 20 23 43 syl3anc 
 |-  ( ph -> 1 < ( 2 ^ ( A + 1 ) ) )
45 posdif 
 |-  ( ( 1 e. RR /\ ( 2 ^ ( A + 1 ) ) e. RR ) -> ( 1 < ( 2 ^ ( A + 1 ) ) <-> 0 < ( ( 2 ^ ( A + 1 ) ) - 1 ) ) )
46 5 36 45 sylancr 
 |-  ( ph -> ( 1 < ( 2 ^ ( A + 1 ) ) <-> 0 < ( ( 2 ^ ( A + 1 ) ) - 1 ) ) )
47 44 46 mpbid 
 |-  ( ph -> 0 < ( ( 2 ^ ( A + 1 ) ) - 1 ) )
48 42 47 jca 
 |-  ( ph -> ( ( ( 2 ^ ( A + 1 ) ) - 1 ) e. RR /\ 0 < ( ( 2 ^ ( A + 1 ) ) - 1 ) ) )
49 elrp 
 |-  ( ( ( 2 ^ ( A + 1 ) ) - 1 ) e. RR+ <-> ( ( ( 2 ^ ( A + 1 ) ) - 1 ) e. RR /\ 0 < ( ( 2 ^ ( A + 1 ) ) - 1 ) ) )
50 48 49 sylibr 
 |-  ( ph -> ( ( 2 ^ ( A + 1 ) ) - 1 ) e. RR+ )
51 nnrp 
 |-  ( B e. NN -> B e. RR+ )
52 2 51 syl 
 |-  ( ph -> B e. RR+ )
53 40 50 52 ltdiv2d 
 |-  ( ph -> ( 1 < ( ( 2 ^ ( A + 1 ) ) - 1 ) <-> ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) < ( B / 1 ) ) )
54 38 53 mpbid 
 |-  ( ph -> ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) < ( B / 1 ) )
55 2 nncnd 
 |-  ( ph -> B e. CC )
56 55 div1d 
 |-  ( ph -> ( B / 1 ) = B )
57 54 56 breqtrd 
 |-  ( ph -> ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) < B )
58 6 9 10 11 57 lelttrd 
 |-  ( ph -> 1 < B )
59 eluz2b2 
 |-  ( B e. ( ZZ>= ` 2 ) <-> ( B e. NN /\ 1 < B ) )
60 2 58 59 sylanbrc 
 |-  ( ph -> B e. ( ZZ>= ` 2 ) )
61 fzfid 
 |-  ( ph -> ( 1 ... B ) e. Fin )
62 dvdsssfz1 
 |-  ( B e. NN -> { x e. NN | x || B } C_ ( 1 ... B ) )
63 2 62 syl 
 |-  ( ph -> { x e. NN | x || B } C_ ( 1 ... B ) )
64 ssfi 
 |-  ( ( ( 1 ... B ) e. Fin /\ { x e. NN | x || B } C_ ( 1 ... B ) ) -> { x e. NN | x || B } e. Fin )
65 61 63 64 syl2anc 
 |-  ( ph -> { x e. NN | x || B } e. Fin )
66 65 ad2antrr 
 |-  ( ( ( ph /\ ( n e. NN /\ n || B ) ) /\ -. n e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } ) -> { x e. NN | x || B } e. Fin )
67 ssrab2 
 |-  { x e. NN | x || B } C_ NN
68 67 a1i 
 |-  ( ( ( ph /\ ( n e. NN /\ n || B ) ) /\ -. n e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } ) -> { x e. NN | x || B } C_ NN )
69 68 sselda 
 |-  ( ( ( ( ph /\ ( n e. NN /\ n || B ) ) /\ -. n e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } ) /\ k e. { x e. NN | x || B } ) -> k e. NN )
70 69 nnred 
 |-  ( ( ( ( ph /\ ( n e. NN /\ n || B ) ) /\ -. n e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } ) /\ k e. { x e. NN | x || B } ) -> k e. RR )
71 69 nnnn0d 
 |-  ( ( ( ( ph /\ ( n e. NN /\ n || B ) ) /\ -. n e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } ) /\ k e. { x e. NN | x || B } ) -> k e. NN0 )
72 71 nn0ge0d 
 |-  ( ( ( ( ph /\ ( n e. NN /\ n || B ) ) /\ -. n e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } ) /\ k e. { x e. NN | x || B } ) -> 0 <_ k )
73 df-tp 
 |-  { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B , n } = ( { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } u. { n } )
74 prssi 
 |-  ( ( ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) e. NN /\ B e. NN ) -> { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } C_ NN )
75 8 2 74 syl2anc 
 |-  ( ph -> { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } C_ NN )
76 75 ad2antrr 
 |-  ( ( ( ph /\ ( n e. NN /\ n || B ) ) /\ -. n e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } ) -> { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } C_ NN )
77 simplrl 
 |-  ( ( ( ph /\ ( n e. NN /\ n || B ) ) /\ -. n e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } ) -> n e. NN )
78 77 snssd 
 |-  ( ( ( ph /\ ( n e. NN /\ n || B ) ) /\ -. n e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } ) -> { n } C_ NN )
79 76 78 unssd 
 |-  ( ( ( ph /\ ( n e. NN /\ n || B ) ) /\ -. n e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } ) -> ( { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } u. { n } ) C_ NN )
80 73 79 eqsstrid 
 |-  ( ( ( ph /\ ( n e. NN /\ n || B ) ) /\ -. n e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } ) -> { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B , n } C_ NN )
81 eltpi 
 |-  ( x e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B , n } -> ( x = ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) \/ x = B \/ x = n ) )
82 7 simp2d 
 |-  ( ph -> ( ( 2 ^ ( A + 1 ) ) - 1 ) e. NN )
83 82 nnzd 
 |-  ( ph -> ( ( 2 ^ ( A + 1 ) ) - 1 ) e. ZZ )
84 8 nnzd 
 |-  ( ph -> ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) e. ZZ )
85 dvdsmul2 
 |-  ( ( ( ( 2 ^ ( A + 1 ) ) - 1 ) e. ZZ /\ ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) e. ZZ ) -> ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) || ( ( ( 2 ^ ( A + 1 ) ) - 1 ) x. ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) ) )
86 83 84 85 syl2anc 
 |-  ( ph -> ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) || ( ( ( 2 ^ ( A + 1 ) ) - 1 ) x. ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) ) )
87 82 nncnd 
 |-  ( ph -> ( ( 2 ^ ( A + 1 ) ) - 1 ) e. CC )
88 82 nnne0d 
 |-  ( ph -> ( ( 2 ^ ( A + 1 ) ) - 1 ) =/= 0 )
89 55 87 88 divcan2d 
 |-  ( ph -> ( ( ( 2 ^ ( A + 1 ) ) - 1 ) x. ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) ) = B )
90 86 89 breqtrd 
 |-  ( ph -> ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) || B )
91 breq1 
 |-  ( x = ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) -> ( x || B <-> ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) || B ) )
92 90 91 syl5ibrcom 
 |-  ( ph -> ( x = ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) -> x || B ) )
93 92 ad2antrr 
 |-  ( ( ( ph /\ ( n e. NN /\ n || B ) ) /\ -. n e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } ) -> ( x = ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) -> x || B ) )
94 2 nnzd 
 |-  ( ph -> B e. ZZ )
95 iddvds 
 |-  ( B e. ZZ -> B || B )
96 94 95 syl 
 |-  ( ph -> B || B )
97 breq1 
 |-  ( x = B -> ( x || B <-> B || B ) )
98 96 97 syl5ibrcom 
 |-  ( ph -> ( x = B -> x || B ) )
99 98 ad2antrr 
 |-  ( ( ( ph /\ ( n e. NN /\ n || B ) ) /\ -. n e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } ) -> ( x = B -> x || B ) )
100 simplrr 
 |-  ( ( ( ph /\ ( n e. NN /\ n || B ) ) /\ -. n e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } ) -> n || B )
101 breq1 
 |-  ( x = n -> ( x || B <-> n || B ) )
102 100 101 syl5ibrcom 
 |-  ( ( ( ph /\ ( n e. NN /\ n || B ) ) /\ -. n e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } ) -> ( x = n -> x || B ) )
103 93 99 102 3jaod 
 |-  ( ( ( ph /\ ( n e. NN /\ n || B ) ) /\ -. n e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } ) -> ( ( x = ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) \/ x = B \/ x = n ) -> x || B ) )
104 81 103 syl5 
 |-  ( ( ( ph /\ ( n e. NN /\ n || B ) ) /\ -. n e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } ) -> ( x e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B , n } -> x || B ) )
105 104 imp 
 |-  ( ( ( ( ph /\ ( n e. NN /\ n || B ) ) /\ -. n e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } ) /\ x e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B , n } ) -> x || B )
106 80 105 ssrabdv 
 |-  ( ( ( ph /\ ( n e. NN /\ n || B ) ) /\ -. n e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } ) -> { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B , n } C_ { x e. NN | x || B } )
107 66 70 72 106 fsumless 
 |-  ( ( ( ph /\ ( n e. NN /\ n || B ) ) /\ -. n e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } ) -> sum_ k e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B , n } k <_ sum_ k e. { x e. NN | x || B } k )
108 simpr 
 |-  ( ( ( ph /\ ( n e. NN /\ n || B ) ) /\ -. n e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } ) -> -. n e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } )
109 disjsn 
 |-  ( ( { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } i^i { n } ) = (/) <-> -. n e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } )
110 108 109 sylibr 
 |-  ( ( ( ph /\ ( n e. NN /\ n || B ) ) /\ -. n e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } ) -> ( { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } i^i { n } ) = (/) )
111 73 a1i 
 |-  ( ( ( ph /\ ( n e. NN /\ n || B ) ) /\ -. n e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } ) -> { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B , n } = ( { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } u. { n } ) )
112 tpfi 
 |-  { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B , n } e. Fin
113 112 a1i 
 |-  ( ( ( ph /\ ( n e. NN /\ n || B ) ) /\ -. n e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } ) -> { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B , n } e. Fin )
114 80 sselda 
 |-  ( ( ( ( ph /\ ( n e. NN /\ n || B ) ) /\ -. n e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } ) /\ k e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B , n } ) -> k e. NN )
115 114 nncnd 
 |-  ( ( ( ( ph /\ ( n e. NN /\ n || B ) ) /\ -. n e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } ) /\ k e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B , n } ) -> k e. CC )
116 110 111 113 115 fsumsplit 
 |-  ( ( ( ph /\ ( n e. NN /\ n || B ) ) /\ -. n e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } ) -> sum_ k e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B , n } k = ( sum_ k e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } k + sum_ k e. { n } k ) )
117 8 nncnd 
 |-  ( ph -> ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) e. CC )
118 id 
 |-  ( k = ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) -> k = ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) )
119 118 sumsn 
 |-  ( ( ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) e. NN /\ ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) e. CC ) -> sum_ k e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) } k = ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) )
120 8 117 119 syl2anc 
 |-  ( ph -> sum_ k e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) } k = ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) )
121 id 
 |-  ( k = B -> k = B )
122 121 sumsn 
 |-  ( ( B e. NN /\ B e. CC ) -> sum_ k e. { B } k = B )
123 2 55 122 syl2anc 
 |-  ( ph -> sum_ k e. { B } k = B )
124 120 123 oveq12d 
 |-  ( ph -> ( sum_ k e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) } k + sum_ k e. { B } k ) = ( ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) + B ) )
125 incom 
 |-  ( { B } i^i { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) } ) = ( { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) } i^i { B } )
126 9 57 gtned 
 |-  ( ph -> B =/= ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) )
127 disjsn2 
 |-  ( B =/= ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) -> ( { B } i^i { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) } ) = (/) )
128 126 127 syl 
 |-  ( ph -> ( { B } i^i { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) } ) = (/) )
129 125 128 eqtr3id 
 |-  ( ph -> ( { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) } i^i { B } ) = (/) )
130 df-pr 
 |-  { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } = ( { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) } u. { B } )
131 130 a1i 
 |-  ( ph -> { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } = ( { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) } u. { B } ) )
132 prfi 
 |-  { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } e. Fin
133 132 a1i 
 |-  ( ph -> { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } e. Fin )
134 75 sselda 
 |-  ( ( ph /\ k e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } ) -> k e. NN )
135 134 nncnd 
 |-  ( ( ph /\ k e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } ) -> k e. CC )
136 129 131 133 135 fsumsplit 
 |-  ( ph -> sum_ k e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } k = ( sum_ k e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) } k + sum_ k e. { B } k ) )
137 87 55 mulcld 
 |-  ( ph -> ( ( ( 2 ^ ( A + 1 ) ) - 1 ) x. B ) e. CC )
138 55 137 87 88 divdird 
 |-  ( ph -> ( ( B + ( ( ( 2 ^ ( A + 1 ) ) - 1 ) x. B ) ) / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) = ( ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) + ( ( ( ( 2 ^ ( A + 1 ) ) - 1 ) x. B ) / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) ) )
139 35 nncnd 
 |-  ( ph -> ( 2 ^ ( A + 1 ) ) e. CC )
140 27 a1i 
 |-  ( ph -> 1 e. CC )
141 139 140 55 subdird 
 |-  ( ph -> ( ( ( 2 ^ ( A + 1 ) ) - 1 ) x. B ) = ( ( ( 2 ^ ( A + 1 ) ) x. B ) - ( 1 x. B ) ) )
142 55 mulid2d 
 |-  ( ph -> ( 1 x. B ) = B )
143 142 oveq2d 
 |-  ( ph -> ( ( ( 2 ^ ( A + 1 ) ) x. B ) - ( 1 x. B ) ) = ( ( ( 2 ^ ( A + 1 ) ) x. B ) - B ) )
144 141 143 eqtrd 
 |-  ( ph -> ( ( ( 2 ^ ( A + 1 ) ) - 1 ) x. B ) = ( ( ( 2 ^ ( A + 1 ) ) x. B ) - B ) )
145 144 oveq2d 
 |-  ( ph -> ( B + ( ( ( 2 ^ ( A + 1 ) ) - 1 ) x. B ) ) = ( B + ( ( ( 2 ^ ( A + 1 ) ) x. B ) - B ) ) )
146 139 55 mulcld 
 |-  ( ph -> ( ( 2 ^ ( A + 1 ) ) x. B ) e. CC )
147 55 146 pncan3d 
 |-  ( ph -> ( B + ( ( ( 2 ^ ( A + 1 ) ) x. B ) - B ) ) = ( ( 2 ^ ( A + 1 ) ) x. B ) )
148 145 147 eqtrd 
 |-  ( ph -> ( B + ( ( ( 2 ^ ( A + 1 ) ) - 1 ) x. B ) ) = ( ( 2 ^ ( A + 1 ) ) x. B ) )
149 148 oveq1d 
 |-  ( ph -> ( ( B + ( ( ( 2 ^ ( A + 1 ) ) - 1 ) x. B ) ) / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) = ( ( ( 2 ^ ( A + 1 ) ) x. B ) / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) )
150 139 55 87 88 divassd 
 |-  ( ph -> ( ( ( 2 ^ ( A + 1 ) ) x. B ) / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) = ( ( 2 ^ ( A + 1 ) ) x. ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) ) )
151 149 150 eqtrd 
 |-  ( ph -> ( ( B + ( ( ( 2 ^ ( A + 1 ) ) - 1 ) x. B ) ) / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) = ( ( 2 ^ ( A + 1 ) ) x. ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) ) )
152 55 87 88 divcan3d 
 |-  ( ph -> ( ( ( ( 2 ^ ( A + 1 ) ) - 1 ) x. B ) / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) = B )
153 152 oveq2d 
 |-  ( ph -> ( ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) + ( ( ( ( 2 ^ ( A + 1 ) ) - 1 ) x. B ) / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) ) = ( ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) + B ) )
154 138 151 153 3eqtr3d 
 |-  ( ph -> ( ( 2 ^ ( A + 1 ) ) x. ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) ) = ( ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) + B ) )
155 124 136 154 3eqtr4d 
 |-  ( ph -> sum_ k e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } k = ( ( 2 ^ ( A + 1 ) ) x. ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) ) )
156 155 ad2antrr 
 |-  ( ( ( ph /\ ( n e. NN /\ n || B ) ) /\ -. n e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } ) -> sum_ k e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } k = ( ( 2 ^ ( A + 1 ) ) x. ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) ) )
157 77 nncnd 
 |-  ( ( ( ph /\ ( n e. NN /\ n || B ) ) /\ -. n e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } ) -> n e. CC )
158 id 
 |-  ( k = n -> k = n )
159 158 sumsn 
 |-  ( ( n e. CC /\ n e. CC ) -> sum_ k e. { n } k = n )
160 157 157 159 syl2anc 
 |-  ( ( ( ph /\ ( n e. NN /\ n || B ) ) /\ -. n e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } ) -> sum_ k e. { n } k = n )
161 156 160 oveq12d 
 |-  ( ( ( ph /\ ( n e. NN /\ n || B ) ) /\ -. n e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } ) -> ( sum_ k e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } k + sum_ k e. { n } k ) = ( ( ( 2 ^ ( A + 1 ) ) x. ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) ) + n ) )
162 116 161 eqtrd 
 |-  ( ( ( ph /\ ( n e. NN /\ n || B ) ) /\ -. n e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } ) -> sum_ k e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B , n } k = ( ( ( 2 ^ ( A + 1 ) ) x. ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) ) + n ) )
163 1 nnnn0d 
 |-  ( ph -> A e. NN0 )
164 expp1 
 |-  ( ( 2 e. CC /\ A e. NN0 ) -> ( 2 ^ ( A + 1 ) ) = ( ( 2 ^ A ) x. 2 ) )
165 12 163 164 sylancr 
 |-  ( ph -> ( 2 ^ ( A + 1 ) ) = ( ( 2 ^ A ) x. 2 ) )
166 2nn 
 |-  2 e. NN
167 nnexpcl 
 |-  ( ( 2 e. NN /\ A e. NN0 ) -> ( 2 ^ A ) e. NN )
168 166 163 167 sylancr 
 |-  ( ph -> ( 2 ^ A ) e. NN )
169 168 nncnd 
 |-  ( ph -> ( 2 ^ A ) e. CC )
170 mulcom 
 |-  ( ( ( 2 ^ A ) e. CC /\ 2 e. CC ) -> ( ( 2 ^ A ) x. 2 ) = ( 2 x. ( 2 ^ A ) ) )
171 169 12 170 sylancl 
 |-  ( ph -> ( ( 2 ^ A ) x. 2 ) = ( 2 x. ( 2 ^ A ) ) )
172 165 171 eqtrd 
 |-  ( ph -> ( 2 ^ ( A + 1 ) ) = ( 2 x. ( 2 ^ A ) ) )
173 172 oveq1d 
 |-  ( ph -> ( ( 2 ^ ( A + 1 ) ) x. B ) = ( ( 2 x. ( 2 ^ A ) ) x. B ) )
174 12 a1i 
 |-  ( ph -> 2 e. CC )
175 174 169 55 mulassd 
 |-  ( ph -> ( ( 2 x. ( 2 ^ A ) ) x. B ) = ( 2 x. ( ( 2 ^ A ) x. B ) ) )
176 isodd7 
 |-  ( B e. Odd <-> ( B e. ZZ /\ ( 2 gcd B ) = 1 ) )
177 simpr 
 |-  ( ( B e. ZZ /\ ( 2 gcd B ) = 1 ) -> ( 2 gcd B ) = 1 )
178 176 177 sylbi 
 |-  ( B e. Odd -> ( 2 gcd B ) = 1 )
179 3 178 syl 
 |-  ( ph -> ( 2 gcd B ) = 1 )
180 2z 
 |-  2 e. ZZ
181 180 a1i 
 |-  ( ph -> 2 e. ZZ )
182 rpexp1i 
 |-  ( ( 2 e. ZZ /\ B e. ZZ /\ A e. NN0 ) -> ( ( 2 gcd B ) = 1 -> ( ( 2 ^ A ) gcd B ) = 1 ) )
183 181 94 163 182 syl3anc 
 |-  ( ph -> ( ( 2 gcd B ) = 1 -> ( ( 2 ^ A ) gcd B ) = 1 ) )
184 179 183 mpd 
 |-  ( ph -> ( ( 2 ^ A ) gcd B ) = 1 )
185 sgmmul 
 |-  ( ( 1 e. CC /\ ( ( 2 ^ A ) e. NN /\ B e. NN /\ ( ( 2 ^ A ) gcd B ) = 1 ) ) -> ( 1 sigma ( ( 2 ^ A ) x. B ) ) = ( ( 1 sigma ( 2 ^ A ) ) x. ( 1 sigma B ) ) )
186 140 168 2 184 185 syl13anc 
 |-  ( ph -> ( 1 sigma ( ( 2 ^ A ) x. B ) ) = ( ( 1 sigma ( 2 ^ A ) ) x. ( 1 sigma B ) ) )
187 pncan 
 |-  ( ( A e. CC /\ 1 e. CC ) -> ( ( A + 1 ) - 1 ) = A )
188 28 27 187 sylancl 
 |-  ( ph -> ( ( A + 1 ) - 1 ) = A )
189 188 oveq2d 
 |-  ( ph -> ( 2 ^ ( ( A + 1 ) - 1 ) ) = ( 2 ^ A ) )
190 189 oveq2d 
 |-  ( ph -> ( 1 sigma ( 2 ^ ( ( A + 1 ) - 1 ) ) ) = ( 1 sigma ( 2 ^ A ) ) )
191 1sgm2ppw 
 |-  ( ( A + 1 ) e. NN -> ( 1 sigma ( 2 ^ ( ( A + 1 ) - 1 ) ) ) = ( ( 2 ^ ( A + 1 ) ) - 1 ) )
192 20 191 syl 
 |-  ( ph -> ( 1 sigma ( 2 ^ ( ( A + 1 ) - 1 ) ) ) = ( ( 2 ^ ( A + 1 ) ) - 1 ) )
193 190 192 eqtr3d 
 |-  ( ph -> ( 1 sigma ( 2 ^ A ) ) = ( ( 2 ^ ( A + 1 ) ) - 1 ) )
194 193 oveq1d 
 |-  ( ph -> ( ( 1 sigma ( 2 ^ A ) ) x. ( 1 sigma B ) ) = ( ( ( 2 ^ ( A + 1 ) ) - 1 ) x. ( 1 sigma B ) ) )
195 186 4 194 3eqtr3d 
 |-  ( ph -> ( 2 x. ( ( 2 ^ A ) x. B ) ) = ( ( ( 2 ^ ( A + 1 ) ) - 1 ) x. ( 1 sigma B ) ) )
196 173 175 195 3eqtrd 
 |-  ( ph -> ( ( 2 ^ ( A + 1 ) ) x. B ) = ( ( ( 2 ^ ( A + 1 ) ) - 1 ) x. ( 1 sigma B ) ) )
197 196 oveq1d 
 |-  ( ph -> ( ( ( 2 ^ ( A + 1 ) ) x. B ) / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) = ( ( ( ( 2 ^ ( A + 1 ) ) - 1 ) x. ( 1 sigma B ) ) / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) )
198 1nn0 
 |-  1 e. NN0
199 sgmnncl 
 |-  ( ( 1 e. NN0 /\ B e. NN ) -> ( 1 sigma B ) e. NN )
200 198 2 199 sylancr 
 |-  ( ph -> ( 1 sigma B ) e. NN )
201 200 nncnd 
 |-  ( ph -> ( 1 sigma B ) e. CC )
202 201 87 88 divcan3d 
 |-  ( ph -> ( ( ( ( 2 ^ ( A + 1 ) ) - 1 ) x. ( 1 sigma B ) ) / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) = ( 1 sigma B ) )
203 197 150 202 3eqtr3d 
 |-  ( ph -> ( ( 2 ^ ( A + 1 ) ) x. ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) ) = ( 1 sigma B ) )
204 sgmval 
 |-  ( ( 1 e. CC /\ B e. NN ) -> ( 1 sigma B ) = sum_ k e. { x e. NN | x || B } ( k ^c 1 ) )
205 27 2 204 sylancr 
 |-  ( ph -> ( 1 sigma B ) = sum_ k e. { x e. NN | x || B } ( k ^c 1 ) )
206 simpr 
 |-  ( ( ph /\ k e. { x e. NN | x || B } ) -> k e. { x e. NN | x || B } )
207 67 206 sseldi 
 |-  ( ( ph /\ k e. { x e. NN | x || B } ) -> k e. NN )
208 207 nncnd 
 |-  ( ( ph /\ k e. { x e. NN | x || B } ) -> k e. CC )
209 208 cxp1d 
 |-  ( ( ph /\ k e. { x e. NN | x || B } ) -> ( k ^c 1 ) = k )
210 209 sumeq2dv 
 |-  ( ph -> sum_ k e. { x e. NN | x || B } ( k ^c 1 ) = sum_ k e. { x e. NN | x || B } k )
211 203 205 210 3eqtrrd 
 |-  ( ph -> sum_ k e. { x e. NN | x || B } k = ( ( 2 ^ ( A + 1 ) ) x. ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) ) )
212 211 ad2antrr 
 |-  ( ( ( ph /\ ( n e. NN /\ n || B ) ) /\ -. n e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } ) -> sum_ k e. { x e. NN | x || B } k = ( ( 2 ^ ( A + 1 ) ) x. ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) ) )
213 107 162 212 3brtr3d 
 |-  ( ( ( ph /\ ( n e. NN /\ n || B ) ) /\ -. n e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } ) -> ( ( ( 2 ^ ( A + 1 ) ) x. ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) ) + n ) <_ ( ( 2 ^ ( A + 1 ) ) x. ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) ) )
214 36 9 remulcld 
 |-  ( ph -> ( ( 2 ^ ( A + 1 ) ) x. ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) ) e. RR )
215 214 ad2antrr 
 |-  ( ( ( ph /\ ( n e. NN /\ n || B ) ) /\ -. n e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } ) -> ( ( 2 ^ ( A + 1 ) ) x. ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) ) e. RR )
216 77 nnrpd 
 |-  ( ( ( ph /\ ( n e. NN /\ n || B ) ) /\ -. n e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } ) -> n e. RR+ )
217 215 216 ltaddrpd 
 |-  ( ( ( ph /\ ( n e. NN /\ n || B ) ) /\ -. n e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } ) -> ( ( 2 ^ ( A + 1 ) ) x. ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) ) < ( ( ( 2 ^ ( A + 1 ) ) x. ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) ) + n ) )
218 77 nnred 
 |-  ( ( ( ph /\ ( n e. NN /\ n || B ) ) /\ -. n e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } ) -> n e. RR )
219 215 218 readdcld 
 |-  ( ( ( ph /\ ( n e. NN /\ n || B ) ) /\ -. n e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } ) -> ( ( ( 2 ^ ( A + 1 ) ) x. ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) ) + n ) e. RR )
220 215 219 ltnled 
 |-  ( ( ( ph /\ ( n e. NN /\ n || B ) ) /\ -. n e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } ) -> ( ( ( 2 ^ ( A + 1 ) ) x. ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) ) < ( ( ( 2 ^ ( A + 1 ) ) x. ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) ) + n ) <-> -. ( ( ( 2 ^ ( A + 1 ) ) x. ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) ) + n ) <_ ( ( 2 ^ ( A + 1 ) ) x. ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) ) ) )
221 217 220 mpbid 
 |-  ( ( ( ph /\ ( n e. NN /\ n || B ) ) /\ -. n e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } ) -> -. ( ( ( 2 ^ ( A + 1 ) ) x. ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) ) + n ) <_ ( ( 2 ^ ( A + 1 ) ) x. ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) ) )
222 213 221 condan 
 |-  ( ( ph /\ ( n e. NN /\ n || B ) ) -> n e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } )
223 elpri 
 |-  ( n e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } -> ( n = ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) \/ n = B ) )
224 222 223 syl 
 |-  ( ( ph /\ ( n e. NN /\ n || B ) ) -> ( n = ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) \/ n = B ) )
225 224 expr 
 |-  ( ( ph /\ n e. NN ) -> ( n || B -> ( n = ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) \/ n = B ) ) )
226 225 ralrimiva 
 |-  ( ph -> A. n e. NN ( n || B -> ( n = ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) \/ n = B ) ) )
227 6 58 gtned 
 |-  ( ph -> B =/= 1 )
228 227 necomd 
 |-  ( ph -> 1 =/= B )
229 1nn 
 |-  1 e. NN
230 229 a1i 
 |-  ( ph -> 1 e. NN )
231 1dvds 
 |-  ( B e. ZZ -> 1 || B )
232 94 231 syl 
 |-  ( ph -> 1 || B )
233 breq1 
 |-  ( n = 1 -> ( n || B <-> 1 || B ) )
234 eqeq1 
 |-  ( n = 1 -> ( n = ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) <-> 1 = ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) ) )
235 eqeq1 
 |-  ( n = 1 -> ( n = B <-> 1 = B ) )
236 234 235 orbi12d 
 |-  ( n = 1 -> ( ( n = ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) \/ n = B ) <-> ( 1 = ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) \/ 1 = B ) ) )
237 233 236 imbi12d 
 |-  ( n = 1 -> ( ( n || B -> ( n = ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) \/ n = B ) ) <-> ( 1 || B -> ( 1 = ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) \/ 1 = B ) ) ) )
238 237 rspcv 
 |-  ( 1 e. NN -> ( A. n e. NN ( n || B -> ( n = ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) \/ n = B ) ) -> ( 1 || B -> ( 1 = ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) \/ 1 = B ) ) ) )
239 230 226 232 238 syl3c 
 |-  ( ph -> ( 1 = ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) \/ 1 = B ) )
240 239 ord 
 |-  ( ph -> ( -. 1 = ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) -> 1 = B ) )
241 240 necon1ad 
 |-  ( ph -> ( 1 =/= B -> 1 = ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) ) )
242 228 241 mpd 
 |-  ( ph -> 1 = ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) )
243 242 eqeq2d 
 |-  ( ph -> ( n = 1 <-> n = ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) ) )
244 243 orbi1d 
 |-  ( ph -> ( ( n = 1 \/ n = B ) <-> ( n = ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) \/ n = B ) ) )
245 244 imbi2d 
 |-  ( ph -> ( ( n || B -> ( n = 1 \/ n = B ) ) <-> ( n || B -> ( n = ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) \/ n = B ) ) ) )
246 245 ralbidv 
 |-  ( ph -> ( A. n e. NN ( n || B -> ( n = 1 \/ n = B ) ) <-> A. n e. NN ( n || B -> ( n = ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) \/ n = B ) ) ) )
247 226 246 mpbird 
 |-  ( ph -> A. n e. NN ( n || B -> ( n = 1 \/ n = B ) ) )
248 isprm2 
 |-  ( B e. Prime <-> ( B e. ( ZZ>= ` 2 ) /\ A. n e. NN ( n || B -> ( n = 1 \/ n = B ) ) ) )
249 60 247 248 sylanbrc 
 |-  ( ph -> B e. Prime )
250 214 ltp1d 
 |-  ( ph -> ( ( 2 ^ ( A + 1 ) ) x. ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) ) < ( ( ( 2 ^ ( A + 1 ) ) x. ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) ) + 1 ) )
251 peano2re 
 |-  ( ( ( 2 ^ ( A + 1 ) ) x. ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) ) e. RR -> ( ( ( 2 ^ ( A + 1 ) ) x. ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) ) + 1 ) e. RR )
252 214 251 syl 
 |-  ( ph -> ( ( ( 2 ^ ( A + 1 ) ) x. ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) ) + 1 ) e. RR )
253 214 252 ltnled 
 |-  ( ph -> ( ( ( 2 ^ ( A + 1 ) ) x. ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) ) < ( ( ( 2 ^ ( A + 1 ) ) x. ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) ) + 1 ) <-> -. ( ( ( 2 ^ ( A + 1 ) ) x. ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) ) + 1 ) <_ ( ( 2 ^ ( A + 1 ) ) x. ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) ) ) )
254 250 253 mpbid 
 |-  ( ph -> -. ( ( ( 2 ^ ( A + 1 ) ) x. ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) ) + 1 ) <_ ( ( 2 ^ ( A + 1 ) ) x. ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) ) )
255 207 nnred 
 |-  ( ( ph /\ k e. { x e. NN | x || B } ) -> k e. RR )
256 207 nnnn0d 
 |-  ( ( ph /\ k e. { x e. NN | x || B } ) -> k e. NN0 )
257 256 nn0ge0d 
 |-  ( ( ph /\ k e. { x e. NN | x || B } ) -> 0 <_ k )
258 df-tp 
 |-  { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B , 1 } = ( { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } u. { 1 } )
259 snssi 
 |-  ( 1 e. NN -> { 1 } C_ NN )
260 229 259 mp1i 
 |-  ( ph -> { 1 } C_ NN )
261 75 260 unssd 
 |-  ( ph -> ( { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } u. { 1 } ) C_ NN )
262 258 261 eqsstrid 
 |-  ( ph -> { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B , 1 } C_ NN )
263 eltpi 
 |-  ( x e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B , 1 } -> ( x = ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) \/ x = B \/ x = 1 ) )
264 breq1 
 |-  ( x = 1 -> ( x || B <-> 1 || B ) )
265 232 264 syl5ibrcom 
 |-  ( ph -> ( x = 1 -> x || B ) )
266 92 98 265 3jaod 
 |-  ( ph -> ( ( x = ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) \/ x = B \/ x = 1 ) -> x || B ) )
267 263 266 syl5 
 |-  ( ph -> ( x e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B , 1 } -> x || B ) )
268 267 imp 
 |-  ( ( ph /\ x e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B , 1 } ) -> x || B )
269 262 268 ssrabdv 
 |-  ( ph -> { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B , 1 } C_ { x e. NN | x || B } )
270 65 255 257 269 fsumless 
 |-  ( ph -> sum_ k e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B , 1 } k <_ sum_ k e. { x e. NN | x || B } k )
271 270 adantr 
 |-  ( ( ph /\ B =/= ( ( 2 ^ ( A + 1 ) ) - 1 ) ) -> sum_ k e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B , 1 } k <_ sum_ k e. { x e. NN | x || B } k )
272 55 87 88 diveq1ad 
 |-  ( ph -> ( ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) = 1 <-> B = ( ( 2 ^ ( A + 1 ) ) - 1 ) ) )
273 272 necon3bid 
 |-  ( ph -> ( ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) =/= 1 <-> B =/= ( ( 2 ^ ( A + 1 ) ) - 1 ) ) )
274 273 biimpar 
 |-  ( ( ph /\ B =/= ( ( 2 ^ ( A + 1 ) ) - 1 ) ) -> ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) =/= 1 )
275 274 necomd 
 |-  ( ( ph /\ B =/= ( ( 2 ^ ( A + 1 ) ) - 1 ) ) -> 1 =/= ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) )
276 228 adantr 
 |-  ( ( ph /\ B =/= ( ( 2 ^ ( A + 1 ) ) - 1 ) ) -> 1 =/= B )
277 275 276 nelprd 
 |-  ( ( ph /\ B =/= ( ( 2 ^ ( A + 1 ) ) - 1 ) ) -> -. 1 e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } )
278 disjsn 
 |-  ( ( { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } i^i { 1 } ) = (/) <-> -. 1 e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } )
279 277 278 sylibr 
 |-  ( ( ph /\ B =/= ( ( 2 ^ ( A + 1 ) ) - 1 ) ) -> ( { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } i^i { 1 } ) = (/) )
280 258 a1i 
 |-  ( ( ph /\ B =/= ( ( 2 ^ ( A + 1 ) ) - 1 ) ) -> { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B , 1 } = ( { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } u. { 1 } ) )
281 tpfi 
 |-  { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B , 1 } e. Fin
282 281 a1i 
 |-  ( ( ph /\ B =/= ( ( 2 ^ ( A + 1 ) ) - 1 ) ) -> { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B , 1 } e. Fin )
283 262 adantr 
 |-  ( ( ph /\ B =/= ( ( 2 ^ ( A + 1 ) ) - 1 ) ) -> { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B , 1 } C_ NN )
284 283 sselda 
 |-  ( ( ( ph /\ B =/= ( ( 2 ^ ( A + 1 ) ) - 1 ) ) /\ k e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B , 1 } ) -> k e. NN )
285 284 nncnd 
 |-  ( ( ( ph /\ B =/= ( ( 2 ^ ( A + 1 ) ) - 1 ) ) /\ k e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B , 1 } ) -> k e. CC )
286 279 280 282 285 fsumsplit 
 |-  ( ( ph /\ B =/= ( ( 2 ^ ( A + 1 ) ) - 1 ) ) -> sum_ k e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B , 1 } k = ( sum_ k e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } k + sum_ k e. { 1 } k ) )
287 id 
 |-  ( k = 1 -> k = 1 )
288 287 sumsn 
 |-  ( ( 1 e. CC /\ 1 e. CC ) -> sum_ k e. { 1 } k = 1 )
289 140 27 288 sylancl 
 |-  ( ph -> sum_ k e. { 1 } k = 1 )
290 155 289 oveq12d 
 |-  ( ph -> ( sum_ k e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } k + sum_ k e. { 1 } k ) = ( ( ( 2 ^ ( A + 1 ) ) x. ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) ) + 1 ) )
291 290 adantr 
 |-  ( ( ph /\ B =/= ( ( 2 ^ ( A + 1 ) ) - 1 ) ) -> ( sum_ k e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B } k + sum_ k e. { 1 } k ) = ( ( ( 2 ^ ( A + 1 ) ) x. ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) ) + 1 ) )
292 286 291 eqtrd 
 |-  ( ( ph /\ B =/= ( ( 2 ^ ( A + 1 ) ) - 1 ) ) -> sum_ k e. { ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) , B , 1 } k = ( ( ( 2 ^ ( A + 1 ) ) x. ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) ) + 1 ) )
293 211 adantr 
 |-  ( ( ph /\ B =/= ( ( 2 ^ ( A + 1 ) ) - 1 ) ) -> sum_ k e. { x e. NN | x || B } k = ( ( 2 ^ ( A + 1 ) ) x. ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) ) )
294 271 292 293 3brtr3d 
 |-  ( ( ph /\ B =/= ( ( 2 ^ ( A + 1 ) ) - 1 ) ) -> ( ( ( 2 ^ ( A + 1 ) ) x. ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) ) + 1 ) <_ ( ( 2 ^ ( A + 1 ) ) x. ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) ) )
295 294 ex 
 |-  ( ph -> ( B =/= ( ( 2 ^ ( A + 1 ) ) - 1 ) -> ( ( ( 2 ^ ( A + 1 ) ) x. ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) ) + 1 ) <_ ( ( 2 ^ ( A + 1 ) ) x. ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) ) ) )
296 295 necon1bd 
 |-  ( ph -> ( -. ( ( ( 2 ^ ( A + 1 ) ) x. ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) ) + 1 ) <_ ( ( 2 ^ ( A + 1 ) ) x. ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) ) -> B = ( ( 2 ^ ( A + 1 ) ) - 1 ) ) )
297 254 296 mpd 
 |-  ( ph -> B = ( ( 2 ^ ( A + 1 ) ) - 1 ) )
298 249 297 jca 
 |-  ( ph -> ( B e. Prime /\ B = ( ( 2 ^ ( A + 1 ) ) - 1 ) ) )