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	$⊢ φ \to A \in ℕ$
	perfectlem.2	$⊢ φ \to B \in ℕ$
	perfectlem.3	$⊢ φ \to \neg 2 ∥ B$
	perfectlem.4	$⊢ φ \to 1 σ 2^{A} B = 2 2^{A} B$
Assertion	perfectlem2	$⊢ φ \to (B \in ℙ \land B = 2^{A + 1} - 1)$

Proof

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

Metamath Proof Explorer

Theorem perfectlem2

Proof