perfectALTVlem2

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

	Ref	Expression
Hypotheses	perfectALTVlem.1	$⊢ φ \to A \in ℕ$
	perfectALTVlem.2	$⊢ φ \to B \in ℕ$
	perfectALTVlem.3	$⊢ φ \to B \in Odd$
	perfectALTVlem.4	$⊢ φ \to 1 σ 2^{A} B = 2 2^{A} B$
Assertion	perfectALTVlem2	$⊢ φ \to (B \in ℙ \land B = 2^{A + 1} - 1)$

Proof

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

Metamath Proof Explorer

Theorem perfectALTVlem2

Proof