Metamath Proof Explorer

Theorem perfectlem2

Description: Lemma for perfect . (Contributed by Mario Carneiro, 17-May-2016) Replace OLD theorem. (Revised by Wolf Lammen, 17-Sep-2020)

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

Proof

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