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	⊢ ( 𝜑 → 𝐴 ∈ ℕ )
	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 ) ) )