Metamath Proof Explorer

Theorem perfectALTVlem1

Description: Lemma for perfectALTV . (Contributed by Mario Carneiro, 7-Jun-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 perfectALTVlem1 
|- ( ph -> ( ( 2 ^ ( A + 1 ) ) e. NN /\ ( ( 2 ^ ( A + 1 ) ) - 1 ) e. NN /\ ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) e. NN ) )

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 2nn 
 |-  2 e. NN
6 1 nnnn0d 
 |-  ( ph -> A e. NN0 )
7 peano2nn0 
 |-  ( A e. NN0 -> ( A + 1 ) e. NN0 )
8 6 7 syl 
 |-  ( ph -> ( A + 1 ) e. NN0 )
9 nnexpcl 
 |-  ( ( 2 e. NN /\ ( A + 1 ) e. NN0 ) -> ( 2 ^ ( A + 1 ) ) e. NN )
10 5 8 9 sylancr 
 |-  ( ph -> ( 2 ^ ( A + 1 ) ) e. NN )
11 2re 
 |-  2 e. RR
12 11 a1i 
 |-  ( ph -> 2 e. RR )
13 1 peano2nnd 
 |-  ( ph -> ( A + 1 ) e. NN )
14 1lt2 
 |-  1 < 2
15 14 a1i 
 |-  ( ph -> 1 < 2 )
16 expgt1 
 |-  ( ( 2 e. RR /\ ( A + 1 ) e. NN /\ 1 < 2 ) -> 1 < ( 2 ^ ( A + 1 ) ) )
17 12 13 15 16 syl3anc 
 |-  ( ph -> 1 < ( 2 ^ ( A + 1 ) ) )
18 1nn 
 |-  1 e. NN
19 nnsub 
 |-  ( ( 1 e. NN /\ ( 2 ^ ( A + 1 ) ) e. NN ) -> ( 1 < ( 2 ^ ( A + 1 ) ) <-> ( ( 2 ^ ( A + 1 ) ) - 1 ) e. NN ) )
20 18 10 19 sylancr 
 |-  ( ph -> ( 1 < ( 2 ^ ( A + 1 ) ) <-> ( ( 2 ^ ( A + 1 ) ) - 1 ) e. NN ) )
21 17 20 mpbid 
 |-  ( ph -> ( ( 2 ^ ( A + 1 ) ) - 1 ) e. NN )
22 10 nnzd 
 |-  ( ph -> ( 2 ^ ( A + 1 ) ) e. ZZ )
23 peano2zm 
 |-  ( ( 2 ^ ( A + 1 ) ) e. ZZ -> ( ( 2 ^ ( A + 1 ) ) - 1 ) e. ZZ )
24 22 23 syl 
 |-  ( ph -> ( ( 2 ^ ( A + 1 ) ) - 1 ) e. ZZ )
25 1nn0 
 |-  1 e. NN0
26 sgmnncl 
 |-  ( ( 1 e. NN0 /\ B e. NN ) -> ( 1 sigma B ) e. NN )
27 25 2 26 sylancr 
 |-  ( ph -> ( 1 sigma B ) e. NN )
28 27 nnzd 
 |-  ( ph -> ( 1 sigma B ) e. ZZ )
29 dvdsmul1 
 |-  ( ( ( ( 2 ^ ( A + 1 ) ) - 1 ) e. ZZ /\ ( 1 sigma B ) e. ZZ ) -> ( ( 2 ^ ( A + 1 ) ) - 1 ) || ( ( ( 2 ^ ( A + 1 ) ) - 1 ) x. ( 1 sigma B ) ) )
30 24 28 29 syl2anc 
 |-  ( ph -> ( ( 2 ^ ( A + 1 ) ) - 1 ) || ( ( ( 2 ^ ( A + 1 ) ) - 1 ) x. ( 1 sigma B ) ) )
31 2cn 
 |-  2 e. CC
32 expp1 
 |-  ( ( 2 e. CC /\ A e. NN0 ) -> ( 2 ^ ( A + 1 ) ) = ( ( 2 ^ A ) x. 2 ) )
33 31 6 32 sylancr 
 |-  ( ph -> ( 2 ^ ( A + 1 ) ) = ( ( 2 ^ A ) x. 2 ) )
34 nnexpcl 
 |-  ( ( 2 e. NN /\ A e. NN0 ) -> ( 2 ^ A ) e. NN )
35 5 6 34 sylancr 
 |-  ( ph -> ( 2 ^ A ) e. NN )
36 35 nncnd 
 |-  ( ph -> ( 2 ^ A ) e. CC )
37 mulcom 
 |-  ( ( ( 2 ^ A ) e. CC /\ 2 e. CC ) -> ( ( 2 ^ A ) x. 2 ) = ( 2 x. ( 2 ^ A ) ) )
38 36 31 37 sylancl 
 |-  ( ph -> ( ( 2 ^ A ) x. 2 ) = ( 2 x. ( 2 ^ A ) ) )
39 33 38 eqtrd 
 |-  ( ph -> ( 2 ^ ( A + 1 ) ) = ( 2 x. ( 2 ^ A ) ) )
40 39 oveq1d 
 |-  ( ph -> ( ( 2 ^ ( A + 1 ) ) x. B ) = ( ( 2 x. ( 2 ^ A ) ) x. B ) )
41 31 a1i 
 |-  ( ph -> 2 e. CC )
42 2 nncnd 
 |-  ( ph -> B e. CC )
43 41 36 42 mulassd 
 |-  ( ph -> ( ( 2 x. ( 2 ^ A ) ) x. B ) = ( 2 x. ( ( 2 ^ A ) x. B ) ) )
44 1cnd 
 |-  ( ph -> 1 e. CC )
45 isodd7 
 |-  ( B e. Odd <-> ( B e. ZZ /\ ( 2 gcd B ) = 1 ) )
46 45 simprbi 
 |-  ( B e. Odd -> ( 2 gcd B ) = 1 )
47 3 46 syl 
 |-  ( ph -> ( 2 gcd B ) = 1 )
48 2z 
 |-  2 e. ZZ
49 48 a1i 
 |-  ( ph -> 2 e. ZZ )
50 2 nnzd 
 |-  ( ph -> B e. ZZ )
51 rpexp1i 
 |-  ( ( 2 e. ZZ /\ B e. ZZ /\ A e. NN0 ) -> ( ( 2 gcd B ) = 1 -> ( ( 2 ^ A ) gcd B ) = 1 ) )
52 49 50 6 51 syl3anc 
 |-  ( ph -> ( ( 2 gcd B ) = 1 -> ( ( 2 ^ A ) gcd B ) = 1 ) )
53 47 52 mpd 
 |-  ( ph -> ( ( 2 ^ A ) gcd B ) = 1 )
54 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 ) ) )
55 44 35 2 53 54 syl13anc 
 |-  ( ph -> ( 1 sigma ( ( 2 ^ A ) x. B ) ) = ( ( 1 sigma ( 2 ^ A ) ) x. ( 1 sigma B ) ) )
56 1 nncnd 
 |-  ( ph -> A e. CC )
57 pncan1 
 |-  ( A e. CC -> ( ( A + 1 ) - 1 ) = A )
58 56 57 syl 
 |-  ( ph -> ( ( A + 1 ) - 1 ) = A )
59 58 oveq2d 
 |-  ( ph -> ( 2 ^ ( ( A + 1 ) - 1 ) ) = ( 2 ^ A ) )
60 59 oveq2d 
 |-  ( ph -> ( 1 sigma ( 2 ^ ( ( A + 1 ) - 1 ) ) ) = ( 1 sigma ( 2 ^ A ) ) )
61 1sgm2ppw 
 |-  ( ( A + 1 ) e. NN -> ( 1 sigma ( 2 ^ ( ( A + 1 ) - 1 ) ) ) = ( ( 2 ^ ( A + 1 ) ) - 1 ) )
62 13 61 syl 
 |-  ( ph -> ( 1 sigma ( 2 ^ ( ( A + 1 ) - 1 ) ) ) = ( ( 2 ^ ( A + 1 ) ) - 1 ) )
63 60 62 eqtr3d 
 |-  ( ph -> ( 1 sigma ( 2 ^ A ) ) = ( ( 2 ^ ( A + 1 ) ) - 1 ) )
64 63 oveq1d 
 |-  ( ph -> ( ( 1 sigma ( 2 ^ A ) ) x. ( 1 sigma B ) ) = ( ( ( 2 ^ ( A + 1 ) ) - 1 ) x. ( 1 sigma B ) ) )
65 55 4 64 3eqtr3d 
 |-  ( ph -> ( 2 x. ( ( 2 ^ A ) x. B ) ) = ( ( ( 2 ^ ( A + 1 ) ) - 1 ) x. ( 1 sigma B ) ) )
66 40 43 65 3eqtrd 
 |-  ( ph -> ( ( 2 ^ ( A + 1 ) ) x. B ) = ( ( ( 2 ^ ( A + 1 ) ) - 1 ) x. ( 1 sigma B ) ) )
67 30 66 breqtrrd 
 |-  ( ph -> ( ( 2 ^ ( A + 1 ) ) - 1 ) || ( ( 2 ^ ( A + 1 ) ) x. B ) )
68 24 22 gcdcomd 
 |-  ( ph -> ( ( ( 2 ^ ( A + 1 ) ) - 1 ) gcd ( 2 ^ ( A + 1 ) ) ) = ( ( 2 ^ ( A + 1 ) ) gcd ( ( 2 ^ ( A + 1 ) ) - 1 ) ) )
69 nnpw2evenALTV 
 |-  ( ( A + 1 ) e. NN -> ( 2 ^ ( A + 1 ) ) e. Even )
70 evenm1odd 
 |-  ( ( 2 ^ ( A + 1 ) ) e. Even -> ( ( 2 ^ ( A + 1 ) ) - 1 ) e. Odd )
71 isodd7 
 |-  ( ( ( 2 ^ ( A + 1 ) ) - 1 ) e. Odd <-> ( ( ( 2 ^ ( A + 1 ) ) - 1 ) e. ZZ /\ ( 2 gcd ( ( 2 ^ ( A + 1 ) ) - 1 ) ) = 1 ) )
72 71 simprbi 
 |-  ( ( ( 2 ^ ( A + 1 ) ) - 1 ) e. Odd -> ( 2 gcd ( ( 2 ^ ( A + 1 ) ) - 1 ) ) = 1 )
73 13 69 70 72 4syl 
 |-  ( ph -> ( 2 gcd ( ( 2 ^ ( A + 1 ) ) - 1 ) ) = 1 )
74 rpexp1i 
 |-  ( ( 2 e. ZZ /\ ( ( 2 ^ ( A + 1 ) ) - 1 ) e. ZZ /\ ( A + 1 ) e. NN0 ) -> ( ( 2 gcd ( ( 2 ^ ( A + 1 ) ) - 1 ) ) = 1 -> ( ( 2 ^ ( A + 1 ) ) gcd ( ( 2 ^ ( A + 1 ) ) - 1 ) ) = 1 ) )
75 49 24 8 74 syl3anc 
 |-  ( ph -> ( ( 2 gcd ( ( 2 ^ ( A + 1 ) ) - 1 ) ) = 1 -> ( ( 2 ^ ( A + 1 ) ) gcd ( ( 2 ^ ( A + 1 ) ) - 1 ) ) = 1 ) )
76 73 75 mpd 
 |-  ( ph -> ( ( 2 ^ ( A + 1 ) ) gcd ( ( 2 ^ ( A + 1 ) ) - 1 ) ) = 1 )
77 68 76 eqtrd 
 |-  ( ph -> ( ( ( 2 ^ ( A + 1 ) ) - 1 ) gcd ( 2 ^ ( A + 1 ) ) ) = 1 )
78 coprmdvds 
 |-  ( ( ( ( 2 ^ ( A + 1 ) ) - 1 ) e. ZZ /\ ( 2 ^ ( A + 1 ) ) e. ZZ /\ B e. ZZ ) -> ( ( ( ( 2 ^ ( A + 1 ) ) - 1 ) || ( ( 2 ^ ( A + 1 ) ) x. B ) /\ ( ( ( 2 ^ ( A + 1 ) ) - 1 ) gcd ( 2 ^ ( A + 1 ) ) ) = 1 ) -> ( ( 2 ^ ( A + 1 ) ) - 1 ) || B ) )
79 24 22 50 78 syl3anc 
 |-  ( ph -> ( ( ( ( 2 ^ ( A + 1 ) ) - 1 ) || ( ( 2 ^ ( A + 1 ) ) x. B ) /\ ( ( ( 2 ^ ( A + 1 ) ) - 1 ) gcd ( 2 ^ ( A + 1 ) ) ) = 1 ) -> ( ( 2 ^ ( A + 1 ) ) - 1 ) || B ) )
80 67 77 79 mp2and 
 |-  ( ph -> ( ( 2 ^ ( A + 1 ) ) - 1 ) || B )
81 nndivdvds 
 |-  ( ( B e. NN /\ ( ( 2 ^ ( A + 1 ) ) - 1 ) e. NN ) -> ( ( ( 2 ^ ( A + 1 ) ) - 1 ) || B <-> ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) e. NN ) )
82 2 21 81 syl2anc 
 |-  ( ph -> ( ( ( 2 ^ ( A + 1 ) ) - 1 ) || B <-> ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) e. NN ) )
83 80 82 mpbid 
 |-  ( ph -> ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) e. NN )
84 10 21 83 3jca 
 |-  ( ph -> ( ( 2 ^ ( A + 1 ) ) e. NN /\ ( ( 2 ^ ( A + 1 ) ) - 1 ) e. NN /\ ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) e. NN ) )