trilpolemlt1 - Mathbox for Jim Kingdon

	Mathbox for Jim Kingdon		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > Mathboxes > trilpolemlt1		GIF version

Theorem trilpolemlt1 15685

Description: Lemma for trilpo 15687. The 𝐴 < 1 case. We can use the distance between 𝐴 and one (that is, 1 − 𝐴) to find a position in the sequence 𝑛 where terms after that point will not add up to as much as 1 − 𝐴. By finomni 7206 we know the terms up to 𝑛 either contain a zero or are all one. But if they are all one that contradicts the way we constructed 𝑛, so we know that the sequence contains a zero. (Contributed by Jim Kingdon, 23-Aug-2023.)

**Hypotheses**
Ref	Expression
trilpolemgt1.f	⊢ (𝜑 → 𝐹:ℕ⟶{0, 1})
trilpolemgt1.a	⊢ 𝐴 = Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹‘𝑖))
trilpolemlt1.a	⊢ (𝜑 → 𝐴 < 1)

**Assertion**
Ref	Expression
trilpolemlt1	⊢ (𝜑 → ∃𝑥 ∈ ℕ (𝐹‘𝑥) = 0)

Distinct variable groups: 𝐴,𝑖,𝑥 𝑥,𝐹,𝑖 𝜑,𝑖,𝑥

Proof of Theorem trilpolemlt1 Dummy variables 𝑛 𝑓 𝑗 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		1red 8041	. . . 4 ⊢ (𝜑 → 1 ∈ ℝ)
2		trilpolemgt1.f	. . . . 5 ⊢ (𝜑 → 𝐹:ℕ⟶{0, 1})
3		trilpolemgt1.a	. . . . 5 ⊢ 𝐴 = Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹‘𝑖))
4	2, 3	trilpolemcl 15681	. . . 4 ⊢ (𝜑 → 𝐴 ∈ ℝ)
5	1, 4	resubcld 8407	. . 3 ⊢ (𝜑 → (1 − 𝐴) ∈ ℝ)
6		trilpolemlt1.a	. . . 4 ⊢ (𝜑 → 𝐴 < 1)
7	4, 1	posdifd 8559	. . . 4 ⊢ (𝜑 → (𝐴 < 1 ↔ 0 < (1 − 𝐴)))
8	6, 7	mpbid 147	. . 3 ⊢ (𝜑 → 0 < (1 − 𝐴))
9		nnrecl 9247	. . 3 ⊢ (((1 − 𝐴) ∈ ℝ ∧ 0 < (1 − 𝐴)) → ∃𝑛 ∈ ℕ (1 / 𝑛) < (1 − 𝐴))
10	5, 8, 9	syl2anc 411	. 2 ⊢ (𝜑 → ∃𝑛 ∈ ℕ (1 / 𝑛) < (1 − 𝐴))
11		elfznn 10129	. . . . . . 7 ⊢ (𝑥 ∈ (1...𝑛) → 𝑥 ∈ ℕ)
12	11	ad2antrl 490	. . . . . 6 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ (𝑥 ∈ (1...𝑛) ∧ ((𝐹 ↾ (1...𝑛))‘𝑥) = 0)) → 𝑥 ∈ ℕ)
13		simprl 529	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ (𝑥 ∈ (1...𝑛) ∧ ((𝐹 ↾ (1...𝑛))‘𝑥) = 0)) → 𝑥 ∈ (1...𝑛))
14	13	fvresd 5583	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ (𝑥 ∈ (1...𝑛) ∧ ((𝐹 ↾ (1...𝑛))‘𝑥) = 0)) → ((𝐹 ↾ (1...𝑛))‘𝑥) = (𝐹‘𝑥))
15		simprr 531	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ (𝑥 ∈ (1...𝑛) ∧ ((𝐹 ↾ (1...𝑛))‘𝑥) = 0)) → ((𝐹 ↾ (1...𝑛))‘𝑥) = 0)
16	14, 15	eqtr3d 2231	. . . . . 6 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ (𝑥 ∈ (1...𝑛) ∧ ((𝐹 ↾ (1...𝑛))‘𝑥) = 0)) → (𝐹‘𝑥) = 0)
17	12, 16	jca 306	. . . . 5 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ (𝑥 ∈ (1...𝑛) ∧ ((𝐹 ↾ (1...𝑛))‘𝑥) = 0)) → (𝑥 ∈ ℕ ∧ (𝐹‘𝑥) = 0))
18	17	ex 115	. . . 4 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → ((𝑥 ∈ (1...𝑛) ∧ ((𝐹 ↾ (1...𝑛))‘𝑥) = 0) → (𝑥 ∈ ℕ ∧ (𝐹‘𝑥) = 0)))
19	18	reximdv2 2596	. . 3 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → (∃𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 0 → ∃𝑥 ∈ ℕ (𝐹‘𝑥) = 0))
20		2rp 9733	. . . . . . . . . 10 ⊢ 2 ∈ ℝ⁺
21	20	a1i 9	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → 2 ∈ ℝ⁺)
22		simprl 529	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → 𝑛 ∈ ℕ)
23	22	nnzd 9447	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → 𝑛 ∈ ℤ)
24	21, 23	rpexpcld 10789	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → (2↑𝑛) ∈ ℝ⁺)
25	24	rprecred 9783	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → (1 / (2↑𝑛)) ∈ ℝ)
26	22	nnrecred 9037	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → (1 / 𝑛) ∈ ℝ)
27	5	adantr 276	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → (1 − 𝐴) ∈ ℝ)
28		2z 9354	. . . . . . . . . 10 ⊢ 2 ∈ ℤ
29		uzid 9615	. . . . . . . . . 10 ⊢ (2 ∈ ℤ → 2 ∈ (ℤ_≥‘2))
30	28, 29	mp1i 10	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → 2 ∈ (ℤ_≥‘2))
31	22	nnnn0d 9302	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → 𝑛 ∈ ℕ₀)
32		bernneq3 10754	. . . . . . . . 9 ⊢ ((2 ∈ (ℤ_≥‘2) ∧ 𝑛 ∈ ℕ₀) → 𝑛 < (2↑𝑛))
33	30, 31, 32	syl2anc 411	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → 𝑛 < (2↑𝑛))
34	22	nnrpd 9769	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → 𝑛 ∈ ℝ⁺)
35	34, 24	ltrecd 9790	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → (𝑛 < (2↑𝑛) ↔ (1 / (2↑𝑛)) < (1 / 𝑛)))
36	33, 35	mpbid 147	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → (1 / (2↑𝑛)) < (1 / 𝑛))
37		simprr 531	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → (1 / 𝑛) < (1 − 𝐴))
38	25, 26, 27, 36, 37	lttrd 8152	. . . . . 6 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → (1 / (2↑𝑛)) < (1 − 𝐴))
39	38	adantr 276	. . . . 5 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → (1 / (2↑𝑛)) < (1 − 𝐴))
40	27	adantr 276	. . . . . 6 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → (1 − 𝐴) ∈ ℝ)
41	25	adantr 276	. . . . . 6 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → (1 / (2↑𝑛)) ∈ ℝ)
42		1red 8041	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → 1 ∈ ℝ)
43	4	ad2antrr 488	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → 𝐴 ∈ ℝ)
44		0red 8027	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → 0 ∈ ℝ)
45		eqid 2196	. . . . . . . . . . 11 ⊢ (ℤ_≥‘(𝑛 + 1)) = (ℤ_≥‘(𝑛 + 1))
46	22	adantr 276	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → 𝑛 ∈ ℕ)
47	46	peano2nnd 9005	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → (𝑛 + 1) ∈ ℕ)
48	47	nnzd 9447	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → (𝑛 + 1) ∈ ℤ)
49		eluznn 9674	. . . . . . . . . . . . 13 ⊢ (((𝑛 + 1) ∈ ℕ ∧ 𝑖 ∈ (ℤ_≥‘(𝑛 + 1))) → 𝑖 ∈ ℕ)
50	47, 49	sylan 283	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (ℤ_≥‘(𝑛 + 1))) → 𝑖 ∈ ℕ)
51		eqid 2196	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ ℕ ↦ ((1 / (2↑𝑗)) · (𝐹‘𝑗))) = (𝑗 ∈ ℕ ↦ ((1 / (2↑𝑗)) · (𝐹‘𝑗)))
52		oveq2 5930	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝑖 → (2↑𝑗) = (2↑𝑖))
53	52	oveq2d 5938	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑖 → (1 / (2↑𝑗)) = (1 / (2↑𝑖)))
54		fveq2 5558	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑖 → (𝐹‘𝑗) = (𝐹‘𝑖))
55	53, 54	oveq12d 5940	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑖 → ((1 / (2↑𝑗)) · (𝐹‘𝑗)) = ((1 / (2↑𝑖)) · (𝐹‘𝑖)))
56		simpr 110	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ ℕ) → 𝑖 ∈ ℕ)
57	20	a1i 9	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ ℕ) → 2 ∈ ℝ⁺)
58	56	nnzd 9447	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ ℕ) → 𝑖 ∈ ℤ)
59	57, 58	rpexpcld 10789	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ ℕ) → (2↑𝑖) ∈ ℝ⁺)
60	59	rprecred 9783	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ ℕ) → (1 / (2↑𝑖)) ∈ ℝ)
61		0re 8026	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ ℝ
62		1re 8025	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℝ
63		prssi 3780	. . . . . . . . . . . . . . . 16 ⊢ ((0 ∈ ℝ ∧ 1 ∈ ℝ) → {0, 1} ⊆ ℝ)
64	61, 62, 63	mp2an 426	. . . . . . . . . . . . . . 15 ⊢ {0, 1} ⊆ ℝ
65	2	adantr 276	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → 𝐹:ℕ⟶{0, 1})
66	65	ad2antrr 488	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ ℕ) → 𝐹:ℕ⟶{0, 1})
67	66, 56	ffvelcdmd 5698	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ ℕ) → (𝐹‘𝑖) ∈ {0, 1})
68	64, 67	sselid 3181	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ ℕ) → (𝐹‘𝑖) ∈ ℝ)
69	60, 68	remulcld 8057	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ ℕ) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) ∈ ℝ)
70	51, 55, 56, 69	fvmptd3 5655	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ ((1 / (2↑𝑗)) · (𝐹‘𝑗)))‘𝑖) = ((1 / (2↑𝑖)) · (𝐹‘𝑖)))
71	50, 70	syldan 282	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (ℤ_≥‘(𝑛 + 1))) → ((𝑗 ∈ ℕ ↦ ((1 / (2↑𝑗)) · (𝐹‘𝑗)))‘𝑖) = ((1 / (2↑𝑖)) · (𝐹‘𝑖)))
72	50, 69	syldan 282	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (ℤ_≥‘(𝑛 + 1))) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) ∈ ℝ)
73	65	adantr 276	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → 𝐹:ℕ⟶{0, 1})
74	73, 51	trilpolemclim 15680	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → seq1( + , (𝑗 ∈ ℕ ↦ ((1 / (2↑𝑗)) · (𝐹‘𝑗)))) ∈ dom ⇝ )
75		nnuz 9637	. . . . . . . . . . . . 13 ⊢ ℕ = (ℤ_≥‘1)
76	69	recnd 8055	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ ℕ) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) ∈ ℂ)
77	70, 76	eqeltrd 2273	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ ((1 / (2↑𝑗)) · (𝐹‘𝑗)))‘𝑖) ∈ ℂ)
78	75, 47, 77	iserex 11504	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → (seq1( + , (𝑗 ∈ ℕ ↦ ((1 / (2↑𝑗)) · (𝐹‘𝑗)))) ∈ dom ⇝ ↔ seq(𝑛 + 1)( + , (𝑗 ∈ ℕ ↦ ((1 / (2↑𝑗)) · (𝐹‘𝑗)))) ∈ dom ⇝ ))
79	74, 78	mpbid 147	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → seq(𝑛 + 1)( + , (𝑗 ∈ ℕ ↦ ((1 / (2↑𝑗)) · (𝐹‘𝑗)))) ∈ dom ⇝ )
80	45, 48, 71, 72, 79	isumrecl 11594	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → Σ𝑖 ∈ (ℤ_≥‘(𝑛 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖)) ∈ ℝ)
81		1zzd 9353	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → 1 ∈ ℤ)
82	81, 23	fzfigd 10523	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → (1...𝑛) ∈ Fin)
83	82	adantr 276	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → (1...𝑛) ∈ Fin)
84	20	a1i 9	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (1...𝑛)) → 2 ∈ ℝ⁺)
85		elfzelz 10100	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (1...𝑛) → 𝑖 ∈ ℤ)
86	85	adantl 277	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (1...𝑛)) → 𝑖 ∈ ℤ)
87	84, 86	rpexpcld 10789	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (1...𝑛)) → (2↑𝑖) ∈ ℝ⁺)
88	87	rprecred 9783	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (1...𝑛)) → (1 / (2↑𝑖)) ∈ ℝ)
89	83, 88	fsumrecl 11566	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → Σ𝑖 ∈ (1...𝑛)(1 / (2↑𝑖)) ∈ ℝ)
90	50, 60	syldan 282	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (ℤ_≥‘(𝑛 + 1))) → (1 / (2↑𝑖)) ∈ ℝ)
91	50, 68	syldan 282	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (ℤ_≥‘(𝑛 + 1))) → (𝐹‘𝑖) ∈ ℝ)
92	59	rpreccld 9782	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ ℕ) → (1 / (2↑𝑖)) ∈ ℝ⁺)
93	50, 92	syldan 282	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (ℤ_≥‘(𝑛 + 1))) → (1 / (2↑𝑖)) ∈ ℝ⁺)
94	93	rpge0d 9775	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (ℤ_≥‘(𝑛 + 1))) → 0 ≤ (1 / (2↑𝑖)))
95		0le0 9079	. . . . . . . . . . . . . 14 ⊢ 0 ≤ 0
96		simpr 110	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (ℤ_≥‘(𝑛 + 1))) ∧ (𝐹‘𝑖) = 0) → (𝐹‘𝑖) = 0)
97	95, 96	breqtrrid 4071	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (ℤ_≥‘(𝑛 + 1))) ∧ (𝐹‘𝑖) = 0) → 0 ≤ (𝐹‘𝑖))
98		0le1 8508	. . . . . . . . . . . . . 14 ⊢ 0 ≤ 1
99		simpr 110	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (ℤ_≥‘(𝑛 + 1))) ∧ (𝐹‘𝑖) = 1) → (𝐹‘𝑖) = 1)
100	98, 99	breqtrrid 4071	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (ℤ_≥‘(𝑛 + 1))) ∧ (𝐹‘𝑖) = 1) → 0 ≤ (𝐹‘𝑖))
101	73	adantr 276	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (ℤ_≥‘(𝑛 + 1))) → 𝐹:ℕ⟶{0, 1})
102	101, 50	ffvelcdmd 5698	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (ℤ_≥‘(𝑛 + 1))) → (𝐹‘𝑖) ∈ {0, 1})
103		elpri 3645	. . . . . . . . . . . . . 14 ⊢ ((𝐹‘𝑖) ∈ {0, 1} → ((𝐹‘𝑖) = 0 ∨ (𝐹‘𝑖) = 1))
104	102, 103	syl 14	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (ℤ_≥‘(𝑛 + 1))) → ((𝐹‘𝑖) = 0 ∨ (𝐹‘𝑖) = 1))
105	97, 100, 104	mpjaodan 799	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (ℤ_≥‘(𝑛 + 1))) → 0 ≤ (𝐹‘𝑖))
106	90, 91, 94, 105	mulge0d 8648	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (ℤ_≥‘(𝑛 + 1))) → 0 ≤ ((1 / (2↑𝑖)) · (𝐹‘𝑖)))
107	45, 48, 71, 72, 79, 106	isumge0 11595	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → 0 ≤ Σ𝑖 ∈ (ℤ_≥‘(𝑛 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖)))
108	44, 80, 89, 107	leadd2dd 8587	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → (Σ𝑖 ∈ (1...𝑛)(1 / (2↑𝑖)) + 0) ≤ (Σ𝑖 ∈ (1...𝑛)(1 / (2↑𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑛 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖))))
109	89	recnd 8055	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → Σ𝑖 ∈ (1...𝑛)(1 / (2↑𝑖)) ∈ ℂ)
110	109	addridd 8175	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → (Σ𝑖 ∈ (1...𝑛)(1 / (2↑𝑖)) + 0) = Σ𝑖 ∈ (1...𝑛)(1 / (2↑𝑖)))
111	110	eqcomd 2202	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → Σ𝑖 ∈ (1...𝑛)(1 / (2↑𝑖)) = (Σ𝑖 ∈ (1...𝑛)(1 / (2↑𝑖)) + 0))
112	75, 45, 47, 70, 76, 74	isumsplit 11656	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹‘𝑖)) = (Σ𝑖 ∈ (1...((𝑛 + 1) − 1))((1 / (2↑𝑖)) · (𝐹‘𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑛 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖))))
113	3, 112	eqtrid 2241	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → 𝐴 = (Σ𝑖 ∈ (1...((𝑛 + 1) − 1))((1 / (2↑𝑖)) · (𝐹‘𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑛 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖))))
114	46	nncnd 9004	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → 𝑛 ∈ ℂ)
115		1cnd 8042	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → 1 ∈ ℂ)
116	114, 115	pncand 8338	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → ((𝑛 + 1) − 1) = 𝑛)
117	116	oveq2d 5938	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → (1...((𝑛 + 1) − 1)) = (1...𝑛))
118		simpr 110	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (1...𝑛)) → 𝑖 ∈ (1...𝑛))
119	118	fvresd 5583	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (1...𝑛)) → ((𝐹 ↾ (1...𝑛))‘𝑖) = (𝐹‘𝑖))
120		fveqeq2 5567	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑖 → (((𝐹 ↾ (1...𝑛))‘𝑥) = 1 ↔ ((𝐹 ↾ (1...𝑛))‘𝑖) = 1))
121		simplr 528	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (1...𝑛)) → ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1)
122	120, 121, 118	rspcdva 2873	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (1...𝑛)) → ((𝐹 ↾ (1...𝑛))‘𝑖) = 1)
123	119, 122	eqtr3d 2231	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (1...𝑛)) → (𝐹‘𝑖) = 1)
124	123	oveq2d 5938	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (1...𝑛)) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) = ((1 / (2↑𝑖)) · 1))
125	87	rpreccld 9782	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (1...𝑛)) → (1 / (2↑𝑖)) ∈ ℝ⁺)
126	125	rpcnd 9773	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (1...𝑛)) → (1 / (2↑𝑖)) ∈ ℂ)
127	126	mulridd 8043	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (1...𝑛)) → ((1 / (2↑𝑖)) · 1) = (1 / (2↑𝑖)))
128	124, 127	eqtrd 2229	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (1...𝑛)) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) = (1 / (2↑𝑖)))
129	117, 128	sumeq12rdv 11538	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → Σ𝑖 ∈ (1...((𝑛 + 1) − 1))((1 / (2↑𝑖)) · (𝐹‘𝑖)) = Σ𝑖 ∈ (1...𝑛)(1 / (2↑𝑖)))
130	129	oveq1d 5937	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → (Σ𝑖 ∈ (1...((𝑛 + 1) − 1))((1 / (2↑𝑖)) · (𝐹‘𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑛 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖))) = (Σ𝑖 ∈ (1...𝑛)(1 / (2↑𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑛 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖))))
131	113, 130	eqtrd 2229	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → 𝐴 = (Σ𝑖 ∈ (1...𝑛)(1 / (2↑𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑛 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖))))
132	108, 111, 131	3brtr4d 4065	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → Σ𝑖 ∈ (1...𝑛)(1 / (2↑𝑖)) ≤ 𝐴)
133		geo2sum 11679	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ℕ ∧ 1 ∈ ℂ) → Σ𝑖 ∈ (1...𝑛)(1 / (2↑𝑖)) = (1 − (1 / (2↑𝑛))))
134	133	breq1d 4043	. . . . . . . . 9 ⊢ ((𝑛 ∈ ℕ ∧ 1 ∈ ℂ) → (Σ𝑖 ∈ (1...𝑛)(1 / (2↑𝑖)) ≤ 𝐴 ↔ (1 − (1 / (2↑𝑛))) ≤ 𝐴))
135	46, 115, 134	syl2anc 411	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → (Σ𝑖 ∈ (1...𝑛)(1 / (2↑𝑖)) ≤ 𝐴 ↔ (1 − (1 / (2↑𝑛))) ≤ 𝐴))
136	132, 135	mpbid 147	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → (1 − (1 / (2↑𝑛))) ≤ 𝐴)
137	42, 41, 43, 136	subled 8575	. . . . . 6 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → (1 − 𝐴) ≤ (1 / (2↑𝑛)))
138	40, 41, 137	lensymd 8148	. . . . 5 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → ¬ (1 / (2↑𝑛)) < (1 − 𝐴))
139	39, 138	pm2.21dd 621	. . . 4 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → ∃𝑥 ∈ ℕ (𝐹‘𝑥) = 0)
140	139	ex 115	. . 3 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → (∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1 → ∃𝑥 ∈ ℕ (𝐹‘𝑥) = 0))
141		fveq1 5557	. . . . . . 7 ⊢ (𝑓 = (𝐹 ↾ (1...𝑛)) → (𝑓‘𝑥) = ((𝐹 ↾ (1...𝑛))‘𝑥))
142	141	eqeq1d 2205	. . . . . 6 ⊢ (𝑓 = (𝐹 ↾ (1...𝑛)) → ((𝑓‘𝑥) = 0 ↔ ((𝐹 ↾ (1...𝑛))‘𝑥) = 0))
143	142	rexbidv 2498	. . . . 5 ⊢ (𝑓 = (𝐹 ↾ (1...𝑛)) → (∃𝑥 ∈ (1...𝑛)(𝑓‘𝑥) = 0 ↔ ∃𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 0))
144	141	eqeq1d 2205	. . . . . 6 ⊢ (𝑓 = (𝐹 ↾ (1...𝑛)) → ((𝑓‘𝑥) = 1 ↔ ((𝐹 ↾ (1...𝑛))‘𝑥) = 1))
145	144	ralbidv 2497	. . . . 5 ⊢ (𝑓 = (𝐹 ↾ (1...𝑛)) → (∀𝑥 ∈ (1...𝑛)(𝑓‘𝑥) = 1 ↔ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1))
146	143, 145	orbi12d 794	. . . 4 ⊢ (𝑓 = (𝐹 ↾ (1...𝑛)) → ((∃𝑥 ∈ (1...𝑛)(𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ (1...𝑛)(𝑓‘𝑥) = 1) ↔ (∃𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 0 ∨ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1)))
147		finomni 7206	. . . . . 6 ⊢ ((1...𝑛) ∈ Fin → (1...𝑛) ∈ Omni)
148	82, 147	syl 14	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → (1...𝑛) ∈ Omni)
149		isomninn 15675	. . . . . 6 ⊢ ((1...𝑛) ∈ Omni → ((1...𝑛) ∈ Omni ↔ ∀𝑓 ∈ ({0, 1} ↑_𝑚 (1...𝑛))(∃𝑥 ∈ (1...𝑛)(𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ (1...𝑛)(𝑓‘𝑥) = 1)))
150	148, 149	syl 14	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → ((1...𝑛) ∈ Omni ↔ ∀𝑓 ∈ ({0, 1} ↑_𝑚 (1...𝑛))(∃𝑥 ∈ (1...𝑛)(𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ (1...𝑛)(𝑓‘𝑥) = 1)))
151	148, 150	mpbid 147	. . . 4 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → ∀𝑓 ∈ ({0, 1} ↑_𝑚 (1...𝑛))(∃𝑥 ∈ (1...𝑛)(𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ (1...𝑛)(𝑓‘𝑥) = 1))
152		fz1ssnn 10131	. . . . . . 7 ⊢ (1...𝑛) ⊆ ℕ
153	152	a1i 9	. . . . . 6 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → (1...𝑛) ⊆ ℕ)
154	65, 153	fssresd 5434	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → (𝐹 ↾ (1...𝑛)):(1...𝑛)⟶{0, 1})
155		0red 8027	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → 0 ∈ ℝ)
156		1red 8041	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → 1 ∈ ℝ)
157		prexg 4244	. . . . . . 7 ⊢ ((0 ∈ ℝ ∧ 1 ∈ ℝ) → {0, 1} ∈ V)
158	155, 156, 157	syl2anc 411	. . . . . 6 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → {0, 1} ∈ V)
159	158, 82	elmapd 6721	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → ((𝐹 ↾ (1...𝑛)) ∈ ({0, 1} ↑_𝑚 (1...𝑛)) ↔ (𝐹 ↾ (1...𝑛)):(1...𝑛)⟶{0, 1}))
160	154, 159	mpbird 167	. . . 4 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → (𝐹 ↾ (1...𝑛)) ∈ ({0, 1} ↑_𝑚 (1...𝑛)))
161	146, 151, 160	rspcdva 2873	. . 3 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → (∃𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 0 ∨ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1))
162	19, 140, 161	mpjaod 719	. 2 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → ∃𝑥 ∈ ℕ (𝐹‘𝑥) = 0)
163	10, 162	rexlimddv 2619	1 ⊢ (𝜑 → ∃𝑥 ∈ ℕ (𝐹‘𝑥) = 0)

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 709 = wceq 1364 ∈ wcel 2167 ∀wral 2475 ∃wrex 2476 Vcvv 2763 ⊆ wss 3157 {cpr 3623 class class class wbr 4033 ↦ cmpt 4094 dom cdm 4663 ↾ cres 4665 ⟶wf 5254 ‘cfv 5258 (class class class)co 5922 ↑_𝑚 cmap 6707 Fincfn 6799 Omnicomni 7200 ℂcc 7877 ℝcr 7878 0cc0 7879 1c1 7880 + caddc 7882 · cmul 7884 < clt 8061 ≤ cle 8062 − cmin 8197 / cdiv 8699 ℕcn 8990 2c2 9041 ℕ₀cn0 9249 ℤcz 9326 ℤ_≥cuz 9601 ℝ⁺crp 9728 ...cfz 10083 seqcseq 10539 ↑cexp 10630 ⇝ cli 11443 Σcsu 11518

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 ax-5 1461 ax-7 1462 ax-gen 1463 ax-ie1 1507 ax-ie2 1508 ax-8 1518 ax-10 1519 ax-11 1520 ax-i12 1521 ax-bndl 1523 ax-4 1524 ax-17 1540 ax-i9 1544 ax-ial 1548 ax-i5r 1549 ax-13 2169 ax-14 2170 ax-ext 2178 ax-coll 4148 ax-sep 4151 ax-nul 4159 ax-pow 4207 ax-pr 4242 ax-un 4468 ax-setind 4573 ax-iinf 4624 ax-cnex 7970 ax-resscn 7971 ax-1cn 7972 ax-1re 7973 ax-icn 7974 ax-addcl 7975 ax-addrcl 7976 ax-mulcl 7977 ax-mulrcl 7978 ax-addcom 7979 ax-mulcom 7980 ax-addass 7981 ax-mulass 7982 ax-distr 7983 ax-i2m1 7984 ax-0lt1 7985 ax-1rid 7986 ax-0id 7987 ax-rnegex 7988 ax-precex 7989 ax-cnre 7990 ax-pre-ltirr 7991 ax-pre-ltwlin 7992 ax-pre-lttrn 7993 ax-pre-apti 7994 ax-pre-ltadd 7995 ax-pre-mulgt0 7996 ax-pre-mulext 7997 ax-arch 7998 ax-caucvg 7999

This theorem depends on definitions: df-bi 117 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1475 df-sb 1777 df-eu 2048 df-mo 2049 df-clab 2183 df-cleq 2189 df-clel 2192 df-nfc 2328 df-ne 2368 df-nel 2463 df-ral 2480 df-rex 2481 df-reu 2482 df-rmo 2483 df-rab 2484 df-v 2765 df-sbc 2990 df-csb 3085 df-dif 3159 df-un 3161 df-in 3163 df-ss 3170 df-nul 3451 df-if 3562 df-pw 3607 df-sn 3628 df-pr 3629 df-op 3631 df-uni 3840 df-int 3875 df-iun 3918 df-br 4034 df-opab 4095 df-mpt 4096 df-tr 4132 df-id 4328 df-po 4331 df-iso 4332 df-iord 4401 df-on 4403 df-ilim 4404 df-suc 4406 df-iom 4627 df-xp 4669 df-rel 4670 df-cnv 4671 df-co 4672 df-dm 4673 df-rn 4674 df-res 4675 df-ima 4676 df-iota 5219 df-fun 5260 df-fn 5261 df-f 5262 df-f1 5263 df-fo 5264 df-f1o 5265 df-fv 5266 df-isom 5267 df-riota 5877 df-ov 5925 df-oprab 5926 df-mpo 5927 df-1st 6198 df-2nd 6199 df-recs 6363 df-irdg 6428 df-frec 6449 df-1o 6474 df-2o 6475 df-oadd 6478 df-er 6592 df-map 6709 df-en 6800 df-dom 6801 df-fin 6802 df-omni 7201 df-pnf 8063 df-mnf 8064 df-xr 8065 df-ltxr 8066 df-le 8067 df-sub 8199 df-neg 8200 df-reap 8602 df-ap 8609 df-div 8700 df-inn 8991 df-2 9049 df-3 9050 df-4 9051 df-n0 9250 df-z 9327 df-uz 9602 df-q 9694 df-rp 9729 df-ico 9969 df-fz 10084 df-fzo 10218 df-seqfrec 10540 df-exp 10631 df-ihash 10868 df-cj 11007 df-re 11008 df-im 11009 df-rsqrt 11163 df-abs 11164 df-clim 11444 df-sumdc 11519

This theorem is referenced by: trilpolemres 15686 neapmkvlem 15711

W3C validator