perfectALTVlem2 - Mathbox for Alexander van der Vekens

	Mathbox for Alexander van der Vekens		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > perfectALTVlem2		Structured version Visualization version GIF version

Theorem perfectALTVlem2 45590

Description: Lemma for perfectALTV 45591. (Contributed by Mario Carneiro, 17-May-2016.) (Revised by AV, 1-Jul-2020.)

**Hypotheses**
Ref	Expression
perfectALTVlem.1	⊢ (𝜑 → 𝐴 ∈ ℕ)
perfectALTVlem.2	⊢ (𝜑 → 𝐵 ∈ ℕ)
perfectALTVlem.3	⊢ (𝜑 → 𝐵 ∈ Odd )
perfectALTVlem.4	⊢ (𝜑 → (1 σ ((2↑𝐴) · 𝐵)) = (2 · ((2↑𝐴) · 𝐵)))

**Assertion**
Ref	Expression
perfectALTVlem2	⊢ (𝜑 → (𝐵 ∈ ℙ ∧ 𝐵 = ((2↑(𝐴 + 1)) − 1)))

Proof of Theorem perfectALTVlem2 Dummy variables 𝑘 𝑛 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		perfectALTVlem.2	. . . 4 ⊢ (𝜑 → 𝐵 ∈ ℕ)
2		1re 11081	. . . . . 6 ⊢ 1 ∈ ℝ
3	2	a1i 11	. . . . 5 ⊢ (𝜑 → 1 ∈ ℝ)
4		perfectALTVlem.1	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ ℕ)
5		perfectALTVlem.3	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ∈ Odd )
6		perfectALTVlem.4	. . . . . . . 8 ⊢ (𝜑 → (1 σ ((2↑𝐴) · 𝐵)) = (2 · ((2↑𝐴) · 𝐵)))
7	4, 1, 5, 6	perfectALTVlem1 45589	. . . . . . 7 ⊢ (𝜑 → ((2↑(𝐴 + 1)) ∈ ℕ ∧ ((2↑(𝐴 + 1)) − 1) ∈ ℕ ∧ (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℕ))
8	7	simp3d 1144	. . . . . 6 ⊢ (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℕ)
9	8	nnred 12094	. . . . 5 ⊢ (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℝ)
10	1	nnred 12094	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ ℝ)
11	8	nnge1d 12127	. . . . 5 ⊢ (𝜑 → 1 ≤ (𝐵 / ((2↑(𝐴 + 1)) − 1)))
12		2cn 12154	. . . . . . . . . . 11 ⊢ 2 ∈ ℂ
13		exp1 13894	. . . . . . . . . . 11 ⊢ (2 ∈ ℂ → (2↑1) = 2)
14	12, 13	ax-mp 5	. . . . . . . . . 10 ⊢ (2↑1) = 2
15		df-2 12142	. . . . . . . . . 10 ⊢ 2 = (1 + 1)
16	14, 15	eqtri 2765	. . . . . . . . 9 ⊢ (2↑1) = (1 + 1)
17		2re 12153	. . . . . . . . . . 11 ⊢ 2 ∈ ℝ
18	17	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 2 ∈ ℝ)
19		1zzd 12457	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ ℤ)
20	4	peano2nnd 12096	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 + 1) ∈ ℕ)
21	20	nnzd 12531	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 + 1) ∈ ℤ)
22		1lt2 12250	. . . . . . . . . . 11 ⊢ 1 < 2
23	22	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 1 < 2)
24	4	nnrpd 12876	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ ℝ⁺)
25		ltaddrp 12873	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℝ ∧ 𝐴 ∈ ℝ⁺) → 1 < (1 + 𝐴))
26	2, 24, 25	sylancr 588	. . . . . . . . . . 11 ⊢ (𝜑 → 1 < (1 + 𝐴))
27		ax-1cn 11035	. . . . . . . . . . . 12 ⊢ 1 ∈ ℂ
28	4	nncnd 12095	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ ℂ)
29		addcom 11267	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (1 + 𝐴) = (𝐴 + 1))
30	27, 28, 29	sylancr 588	. . . . . . . . . . 11 ⊢ (𝜑 → (1 + 𝐴) = (𝐴 + 1))
31	26, 30	breqtrd 5123	. . . . . . . . . 10 ⊢ (𝜑 → 1 < (𝐴 + 1))
32		ltexp2a 13990	. . . . . . . . . 10 ⊢ (((2 ∈ ℝ ∧ 1 ∈ ℤ ∧ (𝐴 + 1) ∈ ℤ) ∧ (1 < 2 ∧ 1 < (𝐴 + 1))) → (2↑1) < (2↑(𝐴 + 1)))
33	18, 19, 21, 23, 31, 32	syl32anc 1378	. . . . . . . . 9 ⊢ (𝜑 → (2↑1) < (2↑(𝐴 + 1)))
34	16, 33	eqbrtrrid 5133	. . . . . . . 8 ⊢ (𝜑 → (1 + 1) < (2↑(𝐴 + 1)))
35	7	simp1d 1142	. . . . . . . . . 10 ⊢ (𝜑 → (2↑(𝐴 + 1)) ∈ ℕ)
36	35	nnred 12094	. . . . . . . . 9 ⊢ (𝜑 → (2↑(𝐴 + 1)) ∈ ℝ)
37	3, 3, 36	ltaddsubd 11681	. . . . . . . 8 ⊢ (𝜑 → ((1 + 1) < (2↑(𝐴 + 1)) ↔ 1 < ((2↑(𝐴 + 1)) − 1)))
38	34, 37	mpbid 231	. . . . . . 7 ⊢ (𝜑 → 1 < ((2↑(𝐴 + 1)) − 1))
39		1rp 12840	. . . . . . . . 9 ⊢ 1 ∈ ℝ⁺
40	39	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℝ⁺)
41		peano2rem 11394	. . . . . . . . . . 11 ⊢ ((2↑(𝐴 + 1)) ∈ ℝ → ((2↑(𝐴 + 1)) − 1) ∈ ℝ)
42	36, 41	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ((2↑(𝐴 + 1)) − 1) ∈ ℝ)
43		expgt1 13927	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℝ ∧ (𝐴 + 1) ∈ ℕ ∧ 1 < 2) → 1 < (2↑(𝐴 + 1)))
44	18, 20, 23, 43	syl3anc 1371	. . . . . . . . . . 11 ⊢ (𝜑 → 1 < (2↑(𝐴 + 1)))
45		posdif 11574	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℝ ∧ (2↑(𝐴 + 1)) ∈ ℝ) → (1 < (2↑(𝐴 + 1)) ↔ 0 < ((2↑(𝐴 + 1)) − 1)))
46	2, 36, 45	sylancr 588	. . . . . . . . . . 11 ⊢ (𝜑 → (1 < (2↑(𝐴 + 1)) ↔ 0 < ((2↑(𝐴 + 1)) − 1)))
47	44, 46	mpbid 231	. . . . . . . . . 10 ⊢ (𝜑 → 0 < ((2↑(𝐴 + 1)) − 1))
48	42, 47	jca 513	. . . . . . . . 9 ⊢ (𝜑 → (((2↑(𝐴 + 1)) − 1) ∈ ℝ ∧ 0 < ((2↑(𝐴 + 1)) − 1)))
49		elrp 12838	. . . . . . . . 9 ⊢ (((2↑(𝐴 + 1)) − 1) ∈ ℝ⁺ ↔ (((2↑(𝐴 + 1)) − 1) ∈ ℝ ∧ 0 < ((2↑(𝐴 + 1)) − 1)))
50	48, 49	sylibr 233	. . . . . . . 8 ⊢ (𝜑 → ((2↑(𝐴 + 1)) − 1) ∈ ℝ⁺)
51		nnrp 12847	. . . . . . . . 9 ⊢ (𝐵 ∈ ℕ → 𝐵 ∈ ℝ⁺)
52	1, 51	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ∈ ℝ⁺)
53	40, 50, 52	ltdiv2d 12901	. . . . . . 7 ⊢ (𝜑 → (1 < ((2↑(𝐴 + 1)) − 1) ↔ (𝐵 / ((2↑(𝐴 + 1)) − 1)) < (𝐵 / 1)))
54	38, 53	mpbid 231	. . . . . 6 ⊢ (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) < (𝐵 / 1))
55	1	nncnd 12095	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℂ)
56	55	div1d 11849	. . . . . 6 ⊢ (𝜑 → (𝐵 / 1) = 𝐵)
57	54, 56	breqtrd 5123	. . . . 5 ⊢ (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) < 𝐵)
58	3, 9, 10, 11, 57	lelttrd 11239	. . . 4 ⊢ (𝜑 → 1 < 𝐵)
59		eluz2b2 12767	. . . 4 ⊢ (𝐵 ∈ (ℤ_≥‘2) ↔ (𝐵 ∈ ℕ ∧ 1 < 𝐵))
60	1, 58, 59	sylanbrc 584	. . 3 ⊢ (𝜑 → 𝐵 ∈ (ℤ_≥‘2))
61		fzfid 13799	. . . . . . . . . . . 12 ⊢ (𝜑 → (1...𝐵) ∈ Fin)
62		dvdsssfz1 16127	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ ℕ → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵} ⊆ (1...𝐵))
63	1, 62	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵} ⊆ (1...𝐵))
64		ssfi 9043	. . . . . . . . . . . 12 ⊢ (((1...𝐵) ∈ Fin ∧ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵} ⊆ (1...𝐵)) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵} ∈ Fin)
65	61, 63, 64	syl2anc 585	. . . . . . . . . . 11 ⊢ (𝜑 → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵} ∈ Fin)
66	65	ad2antrr 724	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵} ∈ Fin)
67		ssrab2 4029	. . . . . . . . . . . . 13 ⊢ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵} ⊆ ℕ
68	67	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵} ⊆ ℕ)
69	68	sselda 3936	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) → 𝑘 ∈ ℕ)
70	69	nnred 12094	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) → 𝑘 ∈ ℝ)
71	69	nnnn0d 12399	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) → 𝑘 ∈ ℕ₀)
72	71	nn0ge0d 12402	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) → 0 ≤ 𝑘)
73		df-tp 4583	. . . . . . . . . . . 12 ⊢ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} = ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∪ {𝑛})
74		prssi 4773	. . . . . . . . . . . . . . 15 ⊢ (((𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℕ ∧ 𝐵 ∈ ℕ) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ⊆ ℕ)
75	8, 1, 74	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ (𝜑 → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ⊆ ℕ)
76	75	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ⊆ ℕ)
77		simplrl 775	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → 𝑛 ∈ ℕ)
78	77	snssd 4761	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {𝑛} ⊆ ℕ)
79	76, 78	unssd 4138	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∪ {𝑛}) ⊆ ℕ)
80	73, 79	eqsstrid 3984	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} ⊆ ℕ)
81		eltpi 4640	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} → (𝑥 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝑛))
82	7	simp2d 1143	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((2↑(𝐴 + 1)) − 1) ∈ ℕ)
83	82	nnzd 12531	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((2↑(𝐴 + 1)) − 1) ∈ ℤ)
84	8	nnzd 12531	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℤ)
85		dvdsmul2 16088	. . . . . . . . . . . . . . . . . 18 ⊢ ((((2↑(𝐴 + 1)) − 1) ∈ ℤ ∧ (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℤ) → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∥ (((2↑(𝐴 + 1)) − 1) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
86	83, 84, 85	syl2anc 585	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∥ (((2↑(𝐴 + 1)) − 1) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
87	82	nncnd 12095	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((2↑(𝐴 + 1)) − 1) ∈ ℂ)
88	82	nnne0d 12129	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((2↑(𝐴 + 1)) − 1) ≠ 0)
89	55, 87, 88	divcan2d 11859	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((2↑(𝐴 + 1)) − 1) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) = 𝐵)
90	86, 89	breqtrd 5123	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∥ 𝐵)
91		breq1 5100	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) → (𝑥 ∥ 𝐵 ↔ (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∥ 𝐵))
92	90, 91	syl5ibrcom 247	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑥 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) → 𝑥 ∥ 𝐵))
93	92	ad2antrr 724	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (𝑥 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) → 𝑥 ∥ 𝐵))
94	1	nnzd 12531	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 ∈ ℤ)
95		iddvds 16079	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 ∈ ℤ → 𝐵 ∥ 𝐵)
96	94, 95	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐵 ∥ 𝐵)
97		breq1 5100	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝐵 → (𝑥 ∥ 𝐵 ↔ 𝐵 ∥ 𝐵))
98	96, 97	syl5ibrcom 247	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑥 = 𝐵 → 𝑥 ∥ 𝐵))
99	98	ad2antrr 724	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (𝑥 = 𝐵 → 𝑥 ∥ 𝐵))
100		simplrr 776	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → 𝑛 ∥ 𝐵)
101		breq1 5100	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑛 → (𝑥 ∥ 𝐵 ↔ 𝑛 ∥ 𝐵))
102	100, 101	syl5ibrcom 247	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (𝑥 = 𝑛 → 𝑥 ∥ 𝐵))
103	93, 99, 102	3jaod 1428	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ((𝑥 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝑛) → 𝑥 ∥ 𝐵))
104	81, 103	syl5 34	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (𝑥 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} → 𝑥 ∥ 𝐵))
105	104	imp 408	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) ∧ 𝑥 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛}) → 𝑥 ∥ 𝐵)
106	80, 105	ssrabdv 4023	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} ⊆ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵})
107	66, 70, 72, 106	fsumless 15608	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛}𝑘 ≤ Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}𝑘)
108		simpr 486	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵})
109		disjsn 4664	. . . . . . . . . . . 12 ⊢ (({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∩ {𝑛}) = ∅ ↔ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵})
110	108, 109	sylibr 233	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∩ {𝑛}) = ∅)
111	73	a1i 11	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} = ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∪ {𝑛}))
112		tpfi 9193	. . . . . . . . . . . 12 ⊢ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} ∈ Fin
113	112	a1i 11	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} ∈ Fin)
114	80	sselda 3936	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) ∧ 𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛}) → 𝑘 ∈ ℕ)
115	114	nncnd 12095	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) ∧ 𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛}) → 𝑘 ∈ ℂ)
116	110, 111, 113, 115	fsumsplit 15553	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛}𝑘 = (Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 + Σ𝑘 ∈ {𝑛}𝑘))
117	8	nncnd 12095	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℂ)
118		id 22	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) → 𝑘 = (𝐵 / ((2↑(𝐴 + 1)) − 1)))
119	118	sumsn 15558	. . . . . . . . . . . . . . 15 ⊢ (((𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℕ ∧ (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℂ) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1))}𝑘 = (𝐵 / ((2↑(𝐴 + 1)) − 1)))
120	8, 117, 119	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ (𝜑 → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1))}𝑘 = (𝐵 / ((2↑(𝐴 + 1)) − 1)))
121		id 22	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝐵 → 𝑘 = 𝐵)
122	121	sumsn 15558	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ∈ ℕ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ {𝐵}𝑘 = 𝐵)
123	1, 55, 122	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ (𝜑 → Σ𝑘 ∈ {𝐵}𝑘 = 𝐵)
124	120, 123	oveq12d 7360	. . . . . . . . . . . . 13 ⊢ (𝜑 → (Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1))}𝑘 + Σ𝑘 ∈ {𝐵}𝑘) = ((𝐵 / ((2↑(𝐴 + 1)) − 1)) + 𝐵))
125		incom 4153	. . . . . . . . . . . . . . 15 ⊢ ({𝐵} ∩ {(𝐵 / ((2↑(𝐴 + 1)) − 1))}) = ({(𝐵 / ((2↑(𝐴 + 1)) − 1))} ∩ {𝐵})
126	9, 57	gtned 11216	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐵 ≠ (𝐵 / ((2↑(𝐴 + 1)) − 1)))
127		disjsn2 4665	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ≠ (𝐵 / ((2↑(𝐴 + 1)) − 1)) → ({𝐵} ∩ {(𝐵 / ((2↑(𝐴 + 1)) − 1))}) = ∅)
128	126, 127	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ({𝐵} ∩ {(𝐵 / ((2↑(𝐴 + 1)) − 1))}) = ∅)
129	125, 128	eqtr3id 2791	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ({(𝐵 / ((2↑(𝐴 + 1)) − 1))} ∩ {𝐵}) = ∅)
130		df-pr 4581	. . . . . . . . . . . . . . 15 ⊢ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} = ({(𝐵 / ((2↑(𝐴 + 1)) − 1))} ∪ {𝐵})
131	130	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} = ({(𝐵 / ((2↑(𝐴 + 1)) − 1))} ∪ {𝐵}))
132		prfi 9192	. . . . . . . . . . . . . . 15 ⊢ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∈ Fin
133	132	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∈ Fin)
134	75	sselda 3936	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → 𝑘 ∈ ℕ)
135	134	nncnd 12095	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → 𝑘 ∈ ℂ)
136	129, 131, 133, 135	fsumsplit 15553	. . . . . . . . . . . . 13 ⊢ (𝜑 → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 = (Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1))}𝑘 + Σ𝑘 ∈ {𝐵}𝑘))
137	87, 55	mulcld 11101	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((2↑(𝐴 + 1)) − 1) · 𝐵) ∈ ℂ)
138	55, 137, 87, 88	divdird 11895	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐵 + (((2↑(𝐴 + 1)) − 1) · 𝐵)) / ((2↑(𝐴 + 1)) − 1)) = ((𝐵 / ((2↑(𝐴 + 1)) − 1)) + ((((2↑(𝐴 + 1)) − 1) · 𝐵) / ((2↑(𝐴 + 1)) − 1))))
139	35	nncnd 12095	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (2↑(𝐴 + 1)) ∈ ℂ)
140	27	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 1 ∈ ℂ)
141	139, 140, 55	subdird 11538	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((2↑(𝐴 + 1)) − 1) · 𝐵) = (((2↑(𝐴 + 1)) · 𝐵) − (1 · 𝐵)))
142	55	mulid2d 11099	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (1 · 𝐵) = 𝐵)
143	142	oveq2d 7358	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((2↑(𝐴 + 1)) · 𝐵) − (1 · 𝐵)) = (((2↑(𝐴 + 1)) · 𝐵) − 𝐵))
144	141, 143	eqtrd 2777	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((2↑(𝐴 + 1)) − 1) · 𝐵) = (((2↑(𝐴 + 1)) · 𝐵) − 𝐵))
145	144	oveq2d 7358	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐵 + (((2↑(𝐴 + 1)) − 1) · 𝐵)) = (𝐵 + (((2↑(𝐴 + 1)) · 𝐵) − 𝐵)))
146	139, 55	mulcld 11101	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((2↑(𝐴 + 1)) · 𝐵) ∈ ℂ)
147	55, 146	pncan3d 11441	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐵 + (((2↑(𝐴 + 1)) · 𝐵) − 𝐵)) = ((2↑(𝐴 + 1)) · 𝐵))
148	145, 147	eqtrd 2777	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐵 + (((2↑(𝐴 + 1)) − 1) · 𝐵)) = ((2↑(𝐴 + 1)) · 𝐵))
149	148	oveq1d 7357	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐵 + (((2↑(𝐴 + 1)) − 1) · 𝐵)) / ((2↑(𝐴 + 1)) − 1)) = (((2↑(𝐴 + 1)) · 𝐵) / ((2↑(𝐴 + 1)) − 1)))
150	139, 55, 87, 88	divassd 11892	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((2↑(𝐴 + 1)) · 𝐵) / ((2↑(𝐴 + 1)) − 1)) = ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
151	149, 150	eqtrd 2777	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐵 + (((2↑(𝐴 + 1)) − 1) · 𝐵)) / ((2↑(𝐴 + 1)) − 1)) = ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
152	55, 87, 88	divcan3d 11862	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((((2↑(𝐴 + 1)) − 1) · 𝐵) / ((2↑(𝐴 + 1)) − 1)) = 𝐵)
153	152	oveq2d 7358	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐵 / ((2↑(𝐴 + 1)) − 1)) + ((((2↑(𝐴 + 1)) − 1) · 𝐵) / ((2↑(𝐴 + 1)) − 1))) = ((𝐵 / ((2↑(𝐴 + 1)) − 1)) + 𝐵))
154	138, 151, 153	3eqtr3d 2785	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) = ((𝐵 / ((2↑(𝐴 + 1)) − 1)) + 𝐵))
155	124, 136, 154	3eqtr4d 2787	. . . . . . . . . . . 12 ⊢ (𝜑 → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 = ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
156	155	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 = ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
157	77	nncnd 12095	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → 𝑛 ∈ ℂ)
158		id 22	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑛 → 𝑘 = 𝑛)
159	158	sumsn 15558	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ ℂ ∧ 𝑛 ∈ ℂ) → Σ𝑘 ∈ {𝑛}𝑘 = 𝑛)
160	157, 157, 159	syl2anc 585	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → Σ𝑘 ∈ {𝑛}𝑘 = 𝑛)
161	156, 160	oveq12d 7360	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 + Σ𝑘 ∈ {𝑛}𝑘) = (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛))
162	116, 161	eqtrd 2777	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛}𝑘 = (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛))
163	4	nnnn0d 12399	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐴 ∈ ℕ₀)
164		expp1 13895	. . . . . . . . . . . . . . . . 17 ⊢ ((2 ∈ ℂ ∧ 𝐴 ∈ ℕ₀) → (2↑(𝐴 + 1)) = ((2↑𝐴) · 2))
165	12, 163, 164	sylancr 588	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2↑(𝐴 + 1)) = ((2↑𝐴) · 2))
166		2nn 12152	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ∈ ℕ
167		nnexpcl 13901	. . . . . . . . . . . . . . . . . . 19 ⊢ ((2 ∈ ℕ ∧ 𝐴 ∈ ℕ₀) → (2↑𝐴) ∈ ℕ)
168	166, 163, 167	sylancr 588	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (2↑𝐴) ∈ ℕ)
169	168	nncnd 12095	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2↑𝐴) ∈ ℂ)
170		mulcom 11063	. . . . . . . . . . . . . . . . 17 ⊢ (((2↑𝐴) ∈ ℂ ∧ 2 ∈ ℂ) → ((2↑𝐴) · 2) = (2 · (2↑𝐴)))
171	169, 12, 170	sylancl 587	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((2↑𝐴) · 2) = (2 · (2↑𝐴)))
172	165, 171	eqtrd 2777	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2↑(𝐴 + 1)) = (2 · (2↑𝐴)))
173	172	oveq1d 7357	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2↑(𝐴 + 1)) · 𝐵) = ((2 · (2↑𝐴)) · 𝐵))
174	12	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 2 ∈ ℂ)
175	174, 169, 55	mulassd 11104	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 · (2↑𝐴)) · 𝐵) = (2 · ((2↑𝐴) · 𝐵)))
176		isodd7 45533	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∈ Odd ↔ (𝐵 ∈ ℤ ∧ (2 gcd 𝐵) = 1))
177		simpr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐵 ∈ ℤ ∧ (2 gcd 𝐵) = 1) → (2 gcd 𝐵) = 1)
178	176, 177	sylbi 216	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 ∈ Odd → (2 gcd 𝐵) = 1)
179	5, 178	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 gcd 𝐵) = 1)
180		2z 12458	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ∈ ℤ
181	180	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 2 ∈ ℤ)
182		rpexp1i 16526	. . . . . . . . . . . . . . . . . 18 ⊢ ((2 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∈ ℕ₀) → ((2 gcd 𝐵) = 1 → ((2↑𝐴) gcd 𝐵) = 1))
183	181, 94, 163, 182	syl3anc 1371	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((2 gcd 𝐵) = 1 → ((2↑𝐴) gcd 𝐵) = 1))
184	179, 183	mpd 15	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((2↑𝐴) gcd 𝐵) = 1)
185		sgmmul 26455	. . . . . . . . . . . . . . . 16 ⊢ ((1 ∈ ℂ ∧ ((2↑𝐴) ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ((2↑𝐴) gcd 𝐵) = 1)) → (1 σ ((2↑𝐴) · 𝐵)) = ((1 σ (2↑𝐴)) · (1 σ 𝐵)))
186	140, 168, 1, 184, 185	syl13anc 1372	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1 σ ((2↑𝐴) · 𝐵)) = ((1 σ (2↑𝐴)) · (1 σ 𝐵)))
187		pncan 11333	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐴 + 1) − 1) = 𝐴)
188	28, 27, 187	sylancl 587	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐴 + 1) − 1) = 𝐴)
189	188	oveq2d 7358	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (2↑((𝐴 + 1) − 1)) = (2↑𝐴))
190	189	oveq2d 7358	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (1 σ (2↑((𝐴 + 1) − 1))) = (1 σ (2↑𝐴)))
191		1sgm2ppw 26454	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 + 1) ∈ ℕ → (1 σ (2↑((𝐴 + 1) − 1))) = ((2↑(𝐴 + 1)) − 1))
192	20, 191	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (1 σ (2↑((𝐴 + 1) − 1))) = ((2↑(𝐴 + 1)) − 1))
193	190, 192	eqtr3d 2779	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1 σ (2↑𝐴)) = ((2↑(𝐴 + 1)) − 1))
194	193	oveq1d 7357	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((1 σ (2↑𝐴)) · (1 σ 𝐵)) = (((2↑(𝐴 + 1)) − 1) · (1 σ 𝐵)))
195	186, 6, 194	3eqtr3d 2785	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (2 · ((2↑𝐴) · 𝐵)) = (((2↑(𝐴 + 1)) − 1) · (1 σ 𝐵)))
196	173, 175, 195	3eqtrd 2781	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2↑(𝐴 + 1)) · 𝐵) = (((2↑(𝐴 + 1)) − 1) · (1 σ 𝐵)))
197	196	oveq1d 7357	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2↑(𝐴 + 1)) · 𝐵) / ((2↑(𝐴 + 1)) − 1)) = ((((2↑(𝐴 + 1)) − 1) · (1 σ 𝐵)) / ((2↑(𝐴 + 1)) − 1)))
198		1nn0 12355	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℕ₀
199		sgmnncl 26402	. . . . . . . . . . . . . . 15 ⊢ ((1 ∈ ℕ₀ ∧ 𝐵 ∈ ℕ) → (1 σ 𝐵) ∈ ℕ)
200	198, 1, 199	sylancr 588	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1 σ 𝐵) ∈ ℕ)
201	200	nncnd 12095	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1 σ 𝐵) ∈ ℂ)
202	201, 87, 88	divcan3d 11862	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((2↑(𝐴 + 1)) − 1) · (1 σ 𝐵)) / ((2↑(𝐴 + 1)) − 1)) = (1 σ 𝐵))
203	197, 150, 202	3eqtr3d 2785	. . . . . . . . . . 11 ⊢ (𝜑 → ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) = (1 σ 𝐵))
204		sgmval 26397	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℂ ∧ 𝐵 ∈ ℕ) → (1 σ 𝐵) = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵} (𝑘↑_𝑐1))
205	27, 1, 204	sylancr 588	. . . . . . . . . . 11 ⊢ (𝜑 → (1 σ 𝐵) = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵} (𝑘↑_𝑐1))
206		simpr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) → 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵})
207	67, 206	sselid 3934	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) → 𝑘 ∈ ℕ)
208	207	nncnd 12095	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) → 𝑘 ∈ ℂ)
209	208	cxp1d 25967	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) → (𝑘↑_𝑐1) = 𝑘)
210	209	sumeq2dv 15515	. . . . . . . . . . 11 ⊢ (𝜑 → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵} (𝑘↑_𝑐1) = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}𝑘)
211	203, 205, 210	3eqtrrd 2782	. . . . . . . . . 10 ⊢ (𝜑 → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}𝑘 = ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
212	211	ad2antrr 724	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}𝑘 = ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
213	107, 162, 212	3brtr3d 5128	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛) ≤ ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
214	36, 9	remulcld 11111	. . . . . . . . . . 11 ⊢ (𝜑 → ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) ∈ ℝ)
215	214	ad2antrr 724	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) ∈ ℝ)
216	77	nnrpd 12876	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → 𝑛 ∈ ℝ⁺)
217	215, 216	ltaddrpd 12911	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) < (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛))
218	77	nnred 12094	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → 𝑛 ∈ ℝ)
219	215, 218	readdcld 11110	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛) ∈ ℝ)
220	215, 219	ltnled 11228	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) < (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛) ↔ ¬ (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛) ≤ ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1)))))
221	217, 220	mpbid 231	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ¬ (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛) ≤ ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
222	213, 221	condan 816	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) → 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵})
223		elpri 4600	. . . . . . 7 ⊢ (𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵))
224	222, 223	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛 ∥ 𝐵)) → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵))
225	224	expr 458	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛 ∥ 𝐵 → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵)))
226	225	ralrimiva 3140	. . . 4 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝑛 ∥ 𝐵 → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵)))
227	3, 58	gtned 11216	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ≠ 1)
228	227	necomd 2997	. . . . . . . . 9 ⊢ (𝜑 → 1 ≠ 𝐵)
229		1nn 12090	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℕ
230	229	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ∈ ℕ)
231		1dvds 16080	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ ℤ → 1 ∥ 𝐵)
232	94, 231	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ∥ 𝐵)
233		breq1 5100	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 1 → (𝑛 ∥ 𝐵 ↔ 1 ∥ 𝐵))
234		eqeq1 2741	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 1 → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ↔ 1 = (𝐵 / ((2↑(𝐴 + 1)) − 1))))
235		eqeq1 2741	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 1 → (𝑛 = 𝐵 ↔ 1 = 𝐵))
236	234, 235	orbi12d 917	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 1 → ((𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵) ↔ (1 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 1 = 𝐵)))
237	233, 236	imbi12d 345	. . . . . . . . . . . . 13 ⊢ (𝑛 = 1 → ((𝑛 ∥ 𝐵 → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵)) ↔ (1 ∥ 𝐵 → (1 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 1 = 𝐵))))
238	237	rspcv 3570	. . . . . . . . . . . 12 ⊢ (1 ∈ ℕ → (∀𝑛 ∈ ℕ (𝑛 ∥ 𝐵 → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵)) → (1 ∥ 𝐵 → (1 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 1 = 𝐵))))
239	230, 226, 232, 238	syl3c 66	. . . . . . . . . . 11 ⊢ (𝜑 → (1 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 1 = 𝐵))
240	239	ord 862	. . . . . . . . . 10 ⊢ (𝜑 → (¬ 1 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) → 1 = 𝐵))
241	240	necon1ad 2958	. . . . . . . . 9 ⊢ (𝜑 → (1 ≠ 𝐵 → 1 = (𝐵 / ((2↑(𝐴 + 1)) − 1))))
242	228, 241	mpd 15	. . . . . . . 8 ⊢ (𝜑 → 1 = (𝐵 / ((2↑(𝐴 + 1)) − 1)))
243	242	eqeq2d 2748	. . . . . . 7 ⊢ (𝜑 → (𝑛 = 1 ↔ 𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1))))
244	243	orbi1d 915	. . . . . 6 ⊢ (𝜑 → ((𝑛 = 1 ∨ 𝑛 = 𝐵) ↔ (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵)))
245	244	imbi2d 341	. . . . 5 ⊢ (𝜑 → ((𝑛 ∥ 𝐵 → (𝑛 = 1 ∨ 𝑛 = 𝐵)) ↔ (𝑛 ∥ 𝐵 → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵))))
246	245	ralbidv 3171	. . . 4 ⊢ (𝜑 → (∀𝑛 ∈ ℕ (𝑛 ∥ 𝐵 → (𝑛 = 1 ∨ 𝑛 = 𝐵)) ↔ ∀𝑛 ∈ ℕ (𝑛 ∥ 𝐵 → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵))))
247	226, 246	mpbird 257	. . 3 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝑛 ∥ 𝐵 → (𝑛 = 1 ∨ 𝑛 = 𝐵)))
248		isprm2 16485	. . 3 ⊢ (𝐵 ∈ ℙ ↔ (𝐵 ∈ (ℤ_≥‘2) ∧ ∀𝑛 ∈ ℕ (𝑛 ∥ 𝐵 → (𝑛 = 1 ∨ 𝑛 = 𝐵))))
249	60, 247, 248	sylanbrc 584	. 2 ⊢ (𝜑 → 𝐵 ∈ ℙ)
250	214	ltp1d 12011	. . . 4 ⊢ (𝜑 → ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) < (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1))
251		peano2re 11254	. . . . . 6 ⊢ (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) ∈ ℝ → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ∈ ℝ)
252	214, 251	syl 17	. . . . 5 ⊢ (𝜑 → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ∈ ℝ)
253	214, 252	ltnled 11228	. . . 4 ⊢ (𝜑 → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) < (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ↔ ¬ (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ≤ ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1)))))
254	250, 253	mpbid 231	. . 3 ⊢ (𝜑 → ¬ (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ≤ ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
255	207	nnred 12094	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) → 𝑘 ∈ ℝ)
256	207	nnnn0d 12399	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) → 𝑘 ∈ ℕ₀)
257	256	nn0ge0d 12402	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}) → 0 ≤ 𝑘)
258		df-tp 4583	. . . . . . . . . 10 ⊢ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} = ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∪ {1})
259		snssi 4760	. . . . . . . . . . . 12 ⊢ (1 ∈ ℕ → {1} ⊆ ℕ)
260	229, 259	mp1i 13	. . . . . . . . . . 11 ⊢ (𝜑 → {1} ⊆ ℕ)
261	75, 260	unssd 4138	. . . . . . . . . 10 ⊢ (𝜑 → ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∪ {1}) ⊆ ℕ)
262	258, 261	eqsstrid 3984	. . . . . . . . 9 ⊢ (𝜑 → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} ⊆ ℕ)
263		eltpi 4640	. . . . . . . . . . 11 ⊢ (𝑥 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} → (𝑥 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑥 = 𝐵 ∨ 𝑥 = 1))
264		breq1 5100	. . . . . . . . . . . . 13 ⊢ (𝑥 = 1 → (𝑥 ∥ 𝐵 ↔ 1 ∥ 𝐵))
265	232, 264	syl5ibrcom 247	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑥 = 1 → 𝑥 ∥ 𝐵))
266	92, 98, 265	3jaod 1428	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑥 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑥 = 𝐵 ∨ 𝑥 = 1) → 𝑥 ∥ 𝐵))
267	263, 266	syl5 34	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} → 𝑥 ∥ 𝐵))
268	267	imp 408	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1}) → 𝑥 ∥ 𝐵)
269	262, 268	ssrabdv 4023	. . . . . . . 8 ⊢ (𝜑 → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} ⊆ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵})
270	65, 255, 257, 269	fsumless 15608	. . . . . . 7 ⊢ (𝜑 → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1}𝑘 ≤ Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}𝑘)
271	270	adantr 482	. . . . . 6 ⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1}𝑘 ≤ Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}𝑘)
272	55, 87, 88	diveq1ad 11866	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐵 / ((2↑(𝐴 + 1)) − 1)) = 1 ↔ 𝐵 = ((2↑(𝐴 + 1)) − 1)))
273	272	necon3bid 2986	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐵 / ((2↑(𝐴 + 1)) − 1)) ≠ 1 ↔ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)))
274	273	biimpar 479	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ≠ 1)
275	274	necomd 2997	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → 1 ≠ (𝐵 / ((2↑(𝐴 + 1)) − 1)))
276	228	adantr 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → 1 ≠ 𝐵)
277	275, 276	nelprd 4609	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → ¬ 1 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵})
278		disjsn 4664	. . . . . . . . 9 ⊢ (({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∩ {1}) = ∅ ↔ ¬ 1 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵})
279	277, 278	sylibr 233	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∩ {1}) = ∅)
280	258	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} = ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∪ {1}))
281		tpfi 9193	. . . . . . . . 9 ⊢ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} ∈ Fin
282	281	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} ∈ Fin)
283	262	adantr 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} ⊆ ℕ)
284	283	sselda 3936	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) ∧ 𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1}) → 𝑘 ∈ ℕ)
285	284	nncnd 12095	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) ∧ 𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1}) → 𝑘 ∈ ℂ)
286	279, 280, 282, 285	fsumsplit 15553	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1}𝑘 = (Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 + Σ𝑘 ∈ {1}𝑘))
287		id 22	. . . . . . . . . . 11 ⊢ (𝑘 = 1 → 𝑘 = 1)
288	287	sumsn 15558	. . . . . . . . . 10 ⊢ ((1 ∈ ℂ ∧ 1 ∈ ℂ) → Σ𝑘 ∈ {1}𝑘 = 1)
289	140, 27, 288	sylancl 587	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑘 ∈ {1}𝑘 = 1)
290	155, 289	oveq12d 7360	. . . . . . . 8 ⊢ (𝜑 → (Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 + Σ𝑘 ∈ {1}𝑘) = (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1))
291	290	adantr 482	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → (Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 + Σ𝑘 ∈ {1}𝑘) = (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1))
292	286, 291	eqtrd 2777	. . . . . 6 ⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1}𝑘 = (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1))
293	211	adantr 482	. . . . . 6 ⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝐵}𝑘 = ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
294	271, 292, 293	3brtr3d 5128	. . . . 5 ⊢ ((𝜑 ∧ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ≤ ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
295	294	ex 414	. . . 4 ⊢ (𝜑 → (𝐵 ≠ ((2↑(𝐴 + 1)) − 1) → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ≤ ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1)))))
296	295	necon1bd 2959	. . 3 ⊢ (𝜑 → (¬ (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ≤ ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) → 𝐵 = ((2↑(𝐴 + 1)) − 1)))
297	254, 296	mpd 15	. 2 ⊢ (𝜑 → 𝐵 = ((2↑(𝐴 + 1)) − 1))
298	249, 297	jca 513	1 ⊢ (𝜑 → (𝐵 ∈ ℙ ∧ 𝐵 = ((2↑(𝐴 + 1)) − 1)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 397 ∨ wo 845 ∨ w3o 1086 = wceq 1541 ∈ wcel 2106 ≠ wne 2941 ∀wral 3062 {crab 3404 ∪ cun 3900 ∩ cin 3901 ⊆ wss 3902 ∅c0 4274 {csn 4578 {cpr 4580 {ctp 4582 class class class wbr 5097 ‘cfv 6484 (class class class)co 7342 Fincfn 8809 ℂcc 10975 ℝcr 10976 0cc0 10977 1c1 10978 + caddc 10980 · cmul 10982 < clt 11115 ≤ cle 11116 − cmin 11311 / cdiv 11738 ℕcn 12079 2c2 12134 ℕ₀cn0 12339 ℤcz 12425 ℤ_≥cuz 12688 ℝ⁺crp 12836 ...cfz 13345 ↑cexp 13888 Σcsu 15497 ∥ cdvds 16063 gcd cgcd 16301 ℙcprime 16474 ↑_𝑐ccxp 25817 σ csgm 26351 Odd codd 45493

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2708 ax-rep 5234 ax-sep 5248 ax-nul 5255 ax-pow 5313 ax-pr 5377 ax-un 7655 ax-inf2 9503 ax-cnex 11033 ax-resscn 11034 ax-1cn 11035 ax-icn 11036 ax-addcl 11037 ax-addrcl 11038 ax-mulcl 11039 ax-mulrcl 11040 ax-mulcom 11041 ax-addass 11042 ax-mulass 11043 ax-distr 11044 ax-i2m1 11045 ax-1ne0 11046 ax-1rid 11047 ax-rnegex 11048 ax-rrecex 11049 ax-cnre 11050 ax-pre-lttri 11051 ax-pre-lttrn 11052 ax-pre-ltadd 11053 ax-pre-mulgt0 11054 ax-pre-sup 11055 ax-addf 11056 ax-mulf 11057

This theorem depends on definitions: df-bi 206 df-an 398 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2815 df-nfc 2887 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3350 df-reu 3351 df-rab 3405 df-v 3444 df-sbc 3732 df-csb 3848 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3921 df-nul 4275 df-if 4479 df-pw 4554 df-sn 4579 df-pr 4581 df-tp 4583 df-op 4585 df-uni 4858 df-int 4900 df-iun 4948 df-iin 4949 df-br 5098 df-opab 5160 df-mpt 5181 df-tr 5215 df-id 5523 df-eprel 5529 df-po 5537 df-so 5538 df-fr 5580 df-se 5581 df-we 5582 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-pred 6243 df-ord 6310 df-on 6311 df-lim 6312 df-suc 6313 df-iota 6436 df-fun 6486 df-fn 6487 df-f 6488 df-f1 6489 df-fo 6490 df-f1o 6491 df-fv 6492 df-isom 6493 df-riota 7298 df-ov 7345 df-oprab 7346 df-mpo 7347 df-of 7600 df-om 7786 df-1st 7904 df-2nd 7905 df-supp 8053 df-frecs 8172 df-wrecs 8203 df-recs 8277 df-rdg 8316 df-1o 8372 df-2o 8373 df-er 8574 df-map 8693 df-pm 8694 df-ixp 8762 df-en 8810 df-dom 8811 df-sdom 8812 df-fin 8813 df-fsupp 9232 df-fi 9273 df-sup 9304 df-inf 9305 df-oi 9372 df-card 9801 df-pnf 11117 df-mnf 11118 df-xr 11119 df-ltxr 11120 df-le 11121 df-sub 11313 df-neg 11314 df-div 11739 df-nn 12080 df-2 12142 df-3 12143 df-4 12144 df-5 12145 df-6 12146 df-7 12147 df-8 12148 df-9 12149 df-n0 12340 df-z 12426 df-dec 12544 df-uz 12689 df-q 12795 df-rp 12837 df-xneg 12954 df-xadd 12955 df-xmul 12956 df-ioo 13189 df-ioc 13190 df-ico 13191 df-icc 13192 df-fz 13346 df-fzo 13489 df-fl 13618 df-mod 13696 df-seq 13828 df-exp 13889 df-fac 14094 df-bc 14123 df-hash 14151 df-shft 14878 df-cj 14910 df-re 14911 df-im 14912 df-sqrt 15046 df-abs 15047 df-limsup 15280 df-clim 15297 df-rlim 15298 df-sum 15498 df-ef 15877 df-sin 15879 df-cos 15880 df-pi 15882 df-dvds 16064 df-gcd 16302 df-prm 16475 df-pc 16636 df-struct 16946 df-sets 16963 df-slot 16981 df-ndx 16993 df-base 17011 df-ress 17040 df-plusg 17073 df-mulr 17074 df-starv 17075 df-sca 17076 df-vsca 17077 df-ip 17078 df-tset 17079 df-ple 17080 df-ds 17082 df-unif 17083 df-hom 17084 df-cco 17085 df-rest 17231 df-topn 17232 df-0g 17250 df-gsum 17251 df-topgen 17252 df-pt 17253 df-prds 17256 df-xrs 17311 df-qtop 17316 df-imas 17317 df-xps 17319 df-mre 17393 df-mrc 17394 df-acs 17396 df-mgm 18424 df-sgrp 18473 df-mnd 18484 df-submnd 18529 df-mulg 18798 df-cntz 19020 df-cmn 19484 df-psmet 20695 df-xmet 20696 df-met 20697 df-bl 20698 df-mopn 20699 df-fbas 20700 df-fg 20701 df-cnfld 20704 df-top 22149 df-topon 22166 df-topsp 22188 df-bases 22202 df-cld 22276 df-ntr 22277 df-cls 22278 df-nei 22355 df-lp 22393 df-perf 22394 df-cn 22484 df-cnp 22485 df-haus 22572 df-tx 22819 df-hmeo 23012 df-fil 23103 df-fm 23195 df-flim 23196 df-flf 23197 df-xms 23579 df-ms 23580 df-tms 23581 df-cncf 24147 df-limc 25136 df-dv 25137 df-log 25818 df-cxp 25819 df-sgm 26357 df-even 45494 df-odd 45495

This theorem is referenced by: perfectALTV 45591

W3C validator