Metamath Proof Explorer

Theorem perfectlem1

Description: Lemma for perfect . (Contributed by Mario Carneiro, 7-Jun-2016)

Ref Expression
Hypotheses perfectlem.1 ⊢ ( 𝜑 → 𝐴 ∈ ℕ )
perfectlem.2 ⊢ ( 𝜑 → 𝐵 ∈ ℕ )
perfectlem.3 ⊢ ( 𝜑 → ¬ 2 ∥ 𝐵 )
perfectlem.4 ⊢ ( 𝜑 → ( 1 σ ( ( 2 ↑ 𝐴 ) · 𝐵 ) ) = ( 2 · ( ( 2 ↑ 𝐴 ) · 𝐵 ) ) )
Assertion perfectlem1 ( 𝜑 → ( ( 2 ↑ ( 𝐴 + 1 ) ) ∈ ℕ ∧ ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∈ ℕ ∧ ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ∈ ℕ ) )

Proof

Step Hyp Ref Expression
1 perfectlem.1 ⊢ ( 𝜑 → 𝐴 ∈ ℕ )
2 perfectlem.2 ⊢ ( 𝜑 → 𝐵 ∈ ℕ )
3 perfectlem.3 ⊢ ( 𝜑 → ¬ 2 ∥ 𝐵 )
4 perfectlem.4 ⊢ ( 𝜑 → ( 1 σ ( ( 2 ↑ 𝐴 ) · 𝐵 ) ) = ( 2 · ( ( 2 ↑ 𝐴 ) · 𝐵 ) ) )
5 2nn ⊢ 2 ∈ ℕ
6 1 nnnn0d ⊢ ( 𝜑 → 𝐴 ∈ ℕ0 )
7 peano2nn0 ⊢ ( 𝐴 ∈ ℕ0 → ( 𝐴 + 1 ) ∈ ℕ0 )
8 6 7 syl ⊢ ( 𝜑 → ( 𝐴 + 1 ) ∈ ℕ0 )
9 nnexpcl ⊢ ( ( 2 ∈ ℕ ∧ ( 𝐴 + 1 ) ∈ ℕ0 ) → ( 2 ↑ ( 𝐴 + 1 ) ) ∈ ℕ )
10 5 8 9 sylancr ⊢ ( 𝜑 → ( 2 ↑ ( 𝐴 + 1 ) ) ∈ ℕ )
11 2re ⊢ 2 ∈ ℝ
12 1 peano2nnd ⊢ ( 𝜑 → ( 𝐴 + 1 ) ∈ ℕ )
13 1lt2 ⊢ 1 < 2
14 13 a1i ⊢ ( 𝜑 → 1 < 2 )
15 expgt1 ⊢ ( ( 2 ∈ ℝ ∧ ( 𝐴 + 1 ) ∈ ℕ ∧ 1 < 2 ) → 1 < ( 2 ↑ ( 𝐴 + 1 ) ) )
16 11 12 14 15 mp3an2i ⊢ ( 𝜑 → 1 < ( 2 ↑ ( 𝐴 + 1 ) ) )
17 1nn ⊢ 1 ∈ ℕ
18 nnsub ⊢ ( ( 1 ∈ ℕ ∧ ( 2 ↑ ( 𝐴 + 1 ) ) ∈ ℕ ) → ( 1 < ( 2 ↑ ( 𝐴 + 1 ) ) ↔ ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∈ ℕ ) )
19 17 10 18 sylancr ⊢ ( 𝜑 → ( 1 < ( 2 ↑ ( 𝐴 + 1 ) ) ↔ ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∈ ℕ ) )
20 16 19 mpbid ⊢ ( 𝜑 → ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∈ ℕ )
21 10 nnzd ⊢ ( 𝜑 → ( 2 ↑ ( 𝐴 + 1 ) ) ∈ ℤ )
22 peano2zm ⊢ ( ( 2 ↑ ( 𝐴 + 1 ) ) ∈ ℤ → ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∈ ℤ )
23 21 22 syl ⊢ ( 𝜑 → ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∈ ℤ )
24 1nn0 ⊢ 1 ∈ ℕ0
25 sgmnncl ⊢ ( ( 1 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ) → ( 1 σ 𝐵 ) ∈ ℕ )
26 24 2 25 sylancr ⊢ ( 𝜑 → ( 1 σ 𝐵 ) ∈ ℕ )
27 26 nnzd ⊢ ( 𝜑 → ( 1 σ 𝐵 ) ∈ ℤ )
28 dvdsmul1 ⊢ ( ( ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∈ ℤ ∧ ( 1 σ 𝐵 ) ∈ ℤ ) → ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∥ ( ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) · ( 1 σ 𝐵 ) ) )
29 23 27 28 syl2anc ⊢ ( 𝜑 → ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∥ ( ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) · ( 1 σ 𝐵 ) ) )
30 2cn ⊢ 2 ∈ ℂ
31 expp1 ⊢ ( ( 2 ∈ ℂ ∧ 𝐴 ∈ ℕ0 ) → ( 2 ↑ ( 𝐴 + 1 ) ) = ( ( 2 ↑ 𝐴 ) · 2 ) )
32 30 6 31 sylancr ⊢ ( 𝜑 → ( 2 ↑ ( 𝐴 + 1 ) ) = ( ( 2 ↑ 𝐴 ) · 2 ) )
33 nnexpcl ⊢ ( ( 2 ∈ ℕ ∧ 𝐴 ∈ ℕ0 ) → ( 2 ↑ 𝐴 ) ∈ ℕ )
34 5 6 33 sylancr ⊢ ( 𝜑 → ( 2 ↑ 𝐴 ) ∈ ℕ )
35 34 nncnd ⊢ ( 𝜑 → ( 2 ↑ 𝐴 ) ∈ ℂ )
36 mulcom ⊢ ( ( ( 2 ↑ 𝐴 ) ∈ ℂ ∧ 2 ∈ ℂ ) → ( ( 2 ↑ 𝐴 ) · 2 ) = ( 2 · ( 2 ↑ 𝐴 ) ) )
37 35 30 36 sylancl ⊢ ( 𝜑 → ( ( 2 ↑ 𝐴 ) · 2 ) = ( 2 · ( 2 ↑ 𝐴 ) ) )
38 32 37 eqtrd ⊢ ( 𝜑 → ( 2 ↑ ( 𝐴 + 1 ) ) = ( 2 · ( 2 ↑ 𝐴 ) ) )
39 38 oveq1d ⊢ ( 𝜑 → ( ( 2 ↑ ( 𝐴 + 1 ) ) · 𝐵 ) = ( ( 2 · ( 2 ↑ 𝐴 ) ) · 𝐵 ) )
40 30 a1i ⊢ ( 𝜑 → 2 ∈ ℂ )
41 2 nncnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
42 40 35 41 mulassd ⊢ ( 𝜑 → ( ( 2 · ( 2 ↑ 𝐴 ) ) · 𝐵 ) = ( 2 · ( ( 2 ↑ 𝐴 ) · 𝐵 ) ) )
43 ax-1cn ⊢ 1 ∈ ℂ
44 43 a1i ⊢ ( 𝜑 → 1 ∈ ℂ )
45 2prm ⊢ 2 ∈ ℙ
46 2 nnzd ⊢ ( 𝜑 → 𝐵 ∈ ℤ )
47 coprm ⊢ ( ( 2 ∈ ℙ ∧ 𝐵 ∈ ℤ ) → ( ¬ 2 ∥ 𝐵 ↔ ( 2 gcd 𝐵 ) = 1 ) )
48 45 46 47 sylancr ⊢ ( 𝜑 → ( ¬ 2 ∥ 𝐵 ↔ ( 2 gcd 𝐵 ) = 1 ) )
49 3 48 mpbid ⊢ ( 𝜑 → ( 2 gcd 𝐵 ) = 1 )
50 2z ⊢ 2 ∈ ℤ
51 rpexp1i ⊢ ( ( 2 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∈ ℕ0 ) → ( ( 2 gcd 𝐵 ) = 1 → ( ( 2 ↑ 𝐴 ) gcd 𝐵 ) = 1 ) )
52 50 46 6 51 mp3an2i ⊢ ( 𝜑 → ( ( 2 gcd 𝐵 ) = 1 → ( ( 2 ↑ 𝐴 ) gcd 𝐵 ) = 1 ) )
53 49 52 mpd ⊢ ( 𝜑 → ( ( 2 ↑ 𝐴 ) gcd 𝐵 ) = 1 )
54 sgmmul ⊢ ( ( 1 ∈ ℂ ∧ ( ( 2 ↑ 𝐴 ) ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( ( 2 ↑ 𝐴 ) gcd 𝐵 ) = 1 ) ) → ( 1 σ ( ( 2 ↑ 𝐴 ) · 𝐵 ) ) = ( ( 1 σ ( 2 ↑ 𝐴 ) ) · ( 1 σ 𝐵 ) ) )
55 44 34 2 53 54 syl13anc ⊢ ( 𝜑 → ( 1 σ ( ( 2 ↑ 𝐴 ) · 𝐵 ) ) = ( ( 1 σ ( 2 ↑ 𝐴 ) ) · ( 1 σ 𝐵 ) ) )
56 1 nncnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
57 pncan ⊢ ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝐴 + 1 ) − 1 ) = 𝐴 )
58 56 43 57 sylancl ⊢ ( 𝜑 → ( ( 𝐴 + 1 ) − 1 ) = 𝐴 )
59 58 oveq2d ⊢ ( 𝜑 → ( 2 ↑ ( ( 𝐴 + 1 ) − 1 ) ) = ( 2 ↑ 𝐴 ) )
60 59 oveq2d ⊢ ( 𝜑 → ( 1 σ ( 2 ↑ ( ( 𝐴 + 1 ) − 1 ) ) ) = ( 1 σ ( 2 ↑ 𝐴 ) ) )
61 1sgm2ppw ⊢ ( ( 𝐴 + 1 ) ∈ ℕ → ( 1 σ ( 2 ↑ ( ( 𝐴 + 1 ) − 1 ) ) ) = ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) )
62 12 61 syl ⊢ ( 𝜑 → ( 1 σ ( 2 ↑ ( ( 𝐴 + 1 ) − 1 ) ) ) = ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) )
63 60 62 eqtr3d ⊢ ( 𝜑 → ( 1 σ ( 2 ↑ 𝐴 ) ) = ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) )
64 63 oveq1d ⊢ ( 𝜑 → ( ( 1 σ ( 2 ↑ 𝐴 ) ) · ( 1 σ 𝐵 ) ) = ( ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) · ( 1 σ 𝐵 ) ) )
65 55 4 64 3eqtr3d ⊢ ( 𝜑 → ( 2 · ( ( 2 ↑ 𝐴 ) · 𝐵 ) ) = ( ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) · ( 1 σ 𝐵 ) ) )
66 39 42 65 3eqtrd ⊢ ( 𝜑 → ( ( 2 ↑ ( 𝐴 + 1 ) ) · 𝐵 ) = ( ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) · ( 1 σ 𝐵 ) ) )
67 29 66 breqtrrd ⊢ ( 𝜑 → ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∥ ( ( 2 ↑ ( 𝐴 + 1 ) ) · 𝐵 ) )
68 23 21 gcdcomd ⊢ ( 𝜑 → ( ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) gcd ( 2 ↑ ( 𝐴 + 1 ) ) ) = ( ( 2 ↑ ( 𝐴 + 1 ) ) gcd ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) )
69 iddvdsexp ⊢ ( ( 2 ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℕ ) → 2 ∥ ( 2 ↑ ( 𝐴 + 1 ) ) )
70 50 12 69 sylancr ⊢ ( 𝜑 → 2 ∥ ( 2 ↑ ( 𝐴 + 1 ) ) )
71 n2dvds1 ⊢ ¬ 2 ∥ 1
72 50 a1i ⊢ ( 𝜑 → 2 ∈ ℤ )
73 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
74 72 21 73 3jca ⊢ ( 𝜑 → ( 2 ∈ ℤ ∧ ( 2 ↑ ( 𝐴 + 1 ) ) ∈ ℤ ∧ 1 ∈ ℤ ) )
75 dvdssub2 ⊢ ( ( ( 2 ∈ ℤ ∧ ( 2 ↑ ( 𝐴 + 1 ) ) ∈ ℤ ∧ 1 ∈ ℤ ) ∧ 2 ∥ ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) → ( 2 ∥ ( 2 ↑ ( 𝐴 + 1 ) ) ↔ 2 ∥ 1 ) )
76 74 75 sylan ⊢ ( ( 𝜑 ∧ 2 ∥ ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) → ( 2 ∥ ( 2 ↑ ( 𝐴 + 1 ) ) ↔ 2 ∥ 1 ) )
77 71 76 mtbiri ⊢ ( ( 𝜑 ∧ 2 ∥ ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) → ¬ 2 ∥ ( 2 ↑ ( 𝐴 + 1 ) ) )
78 77 ex ⊢ ( 𝜑 → ( 2 ∥ ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) → ¬ 2 ∥ ( 2 ↑ ( 𝐴 + 1 ) ) ) )
79 70 78 mt2d ⊢ ( 𝜑 → ¬ 2 ∥ ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) )
80 coprm ⊢ ( ( 2 ∈ ℙ ∧ ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∈ ℤ ) → ( ¬ 2 ∥ ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ↔ ( 2 gcd ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) = 1 ) )
81 45 23 80 sylancr ⊢ ( 𝜑 → ( ¬ 2 ∥ ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ↔ ( 2 gcd ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) = 1 ) )
82 79 81 mpbid ⊢ ( 𝜑 → ( 2 gcd ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) = 1 )
83 rpexp1i ⊢ ( ( 2 ∈ ℤ ∧ ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∈ ℤ ∧ ( 𝐴 + 1 ) ∈ ℕ0 ) → ( ( 2 gcd ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) = 1 → ( ( 2 ↑ ( 𝐴 + 1 ) ) gcd ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) = 1 ) )
84 50 23 8 83 mp3an2i ⊢ ( 𝜑 → ( ( 2 gcd ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) = 1 → ( ( 2 ↑ ( 𝐴 + 1 ) ) gcd ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) = 1 ) )
85 82 84 mpd ⊢ ( 𝜑 → ( ( 2 ↑ ( 𝐴 + 1 ) ) gcd ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) = 1 )
86 68 85 eqtrd ⊢ ( 𝜑 → ( ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) gcd ( 2 ↑ ( 𝐴 + 1 ) ) ) = 1 )
87 coprmdvds ⊢ ( ( ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∈ ℤ ∧ ( 2 ↑ ( 𝐴 + 1 ) ) ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∥ ( ( 2 ↑ ( 𝐴 + 1 ) ) · 𝐵 ) ∧ ( ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) gcd ( 2 ↑ ( 𝐴 + 1 ) ) ) = 1 ) → ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∥ 𝐵 ) )
88 23 21 46 87 syl3anc ⊢ ( 𝜑 → ( ( ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∥ ( ( 2 ↑ ( 𝐴 + 1 ) ) · 𝐵 ) ∧ ( ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) gcd ( 2 ↑ ( 𝐴 + 1 ) ) ) = 1 ) → ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∥ 𝐵 ) )
89 67 86 88 mp2and ⊢ ( 𝜑 → ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∥ 𝐵 )
90 nndivdvds ⊢ ( ( 𝐵 ∈ ℕ ∧ ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∈ ℕ ) → ( ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∥ 𝐵 ↔ ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ∈ ℕ ) )
91 2 20 90 syl2anc ⊢ ( 𝜑 → ( ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∥ 𝐵 ↔ ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ∈ ℕ ) )
92 89 91 mpbid ⊢ ( 𝜑 → ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ∈ ℕ )
93 10 20 92 3jca ⊢ ( 𝜑 → ( ( 2 ↑ ( 𝐴 + 1 ) ) ∈ ℕ ∧ ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ∈ ℕ ∧ ( 𝐵 / ( ( 2 ↑ ( 𝐴 + 1 ) ) − 1 ) ) ∈ ℕ ) )