Metamath Proof Explorer

Theorem perfectlem2

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

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