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 17102

Description: Lemma for trilpo 17104. 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 7480 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 8341	. . . 4 ⊢ (𝜑 → 1 ∈ ℝ)
2		trilpolemgt1.f	. . . . 5 ⊢ (𝜑 → 𝐹:ℕ⟶{0, 1})
3		trilpolemgt1.a	. . . . 5 ⊢ 𝐴 = Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹‘𝑖))
4	2, 3	trilpolemcl 17098	. . . 4 ⊢ (𝜑 → 𝐴 ∈ ℝ)
5	1, 4	resubcld 8708	. . 3 ⊢ (𝜑 → (1 − 𝐴) ∈ ℝ)
6		trilpolemlt1.a	. . . 4 ⊢ (𝜑 → 𝐴 < 1)
7	4, 1	posdifd 8860	. . . 4 ⊢ (𝜑 → (𝐴 < 1 ↔ 0 < (1 − 𝐴)))
8	6, 7	mpbid 147	. . 3 ⊢ (𝜑 → 0 < (1 − 𝐴))
9		nnrecl 9563	. . 3 ⊢ (((1 − 𝐴) ∈ ℝ ∧ 0 < (1 − 𝐴)) → ∃𝑛 ∈ ℕ (1 / 𝑛) < (1 − 𝐴))
10	5, 8, 9	syl2anc 415	. 2 ⊢ (𝜑 → ∃𝑛 ∈ ℕ (1 / 𝑛) < (1 − 𝐴))
11		elfznn 10462	. . . . . . 7 ⊢ (𝑥 ∈ (1...𝑛) → 𝑥 ∈ ℕ)
12	11	ad2antrl 494	. . . . . 6 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ (𝑥 ∈ (1...𝑛) ∧ ((𝐹 ↾ (1...𝑛))‘𝑥) = 0)) → 𝑥 ∈ ℕ)
13		simprl 535	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ (𝑥 ∈ (1...𝑛) ∧ ((𝐹 ↾ (1...𝑛))‘𝑥) = 0)) → 𝑥 ∈ (1...𝑛))
14	13	fvresd 5720	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ (𝑥 ∈ (1...𝑛) ∧ ((𝐹 ↾ (1...𝑛))‘𝑥) = 0)) → ((𝐹 ↾ (1...𝑛))‘𝑥) = (𝐹‘𝑥))
15		simprr 537	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ (𝑥 ∈ (1...𝑛) ∧ ((𝐹 ↾ (1...𝑛))‘𝑥) = 0)) → ((𝐹 ↾ (1...𝑛))‘𝑥) = 0)
16	14, 15	eqtr3d 2273	. . . . . 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 2649	. . 3 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → (∃𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 0 → ∃𝑥 ∈ ℕ (𝐹‘𝑥) = 0))
20		2rp 10061	. . . . . . . . . 10 ⊢ 2 ∈ ℝ⁺
21	20	a1i 9	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → 2 ∈ ℝ⁺)
22		simprl 535	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → 𝑛 ∈ ℕ)
23	22	nnzd 9769	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → 𝑛 ∈ ℤ)
24	21, 23	rpexpcld 11137	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → (2↑𝑛) ∈ ℝ⁺)
25	24	rprecred 10111	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → (1 / (2↑𝑛)) ∈ ℝ)
26	22	nnrecred 9352	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → (1 / 𝑛) ∈ ℝ)
27	5	adantr 276	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → (1 − 𝐴) ∈ ℝ)
28		2z 9674	. . . . . . . . . 10 ⊢ 2 ∈ ℤ
29		uzid 9938	. . . . . . . . . 10 ⊢ (2 ∈ ℤ → 2 ∈ (ℤ_≥‘2))
30	28, 29	mp1i 10	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → 2 ∈ (ℤ_≥‘2))
31	22	nnnn0d 9622	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → 𝑛 ∈ ℕ₀)
32		bernneq3 11102	. . . . . . . . 9 ⊢ ((2 ∈ (ℤ_≥‘2) ∧ 𝑛 ∈ ℕ₀) → 𝑛 < (2↑𝑛))
33	30, 31, 32	syl2anc 415	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → 𝑛 < (2↑𝑛))
34	22	nnrpd 10097	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → 𝑛 ∈ ℝ⁺)
35	34, 24	ltrecd 10118	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → (𝑛 < (2↑𝑛) ↔ (1 / (2↑𝑛)) < (1 / 𝑛)))
36	33, 35	mpbid 147	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → (1 / (2↑𝑛)) < (1 / 𝑛))
37		simprr 537	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → (1 / 𝑛) < (1 − 𝐴))
38	25, 26, 27, 36, 37	lttrd 8452	. . . . . 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 8341	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → 1 ∈ ℝ)
43	4	ad2antrr 492	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → 𝐴 ∈ ℝ)
44		0red 8327	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → 0 ∈ ℝ)
45		eqid 2238	. . . . . . . . . . 11 ⊢ (ℤ_≥‘(𝑛 + 1)) = (ℤ_≥‘(𝑛 + 1))
46	22	adantr 276	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → 𝑛 ∈ ℕ)
47	46	peano2nnd 9320	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → (𝑛 + 1) ∈ ℕ)
48	47	nnzd 9769	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → (𝑛 + 1) ∈ ℤ)
49		eluznn 10002	. . . . . . . . . . . . 13 ⊢ (((𝑛 + 1) ∈ ℕ ∧ 𝑖 ∈ (ℤ_≥‘(𝑛 + 1))) → 𝑖 ∈ ℕ)
50	47, 49	sylan 283	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (ℤ_≥‘(𝑛 + 1))) → 𝑖 ∈ ℕ)
51		eqid 2238	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ ℕ ↦ ((1 / (2↑𝑗)) · (𝐹‘𝑗))) = (𝑗 ∈ ℕ ↦ ((1 / (2↑𝑗)) · (𝐹‘𝑗)))
52		oveq2 6093	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝑖 → (2↑𝑗) = (2↑𝑖))
53	52	oveq2d 6101	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑖 → (1 / (2↑𝑗)) = (1 / (2↑𝑖)))
54		fveq2 5695	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑖 → (𝐹‘𝑗) = (𝐹‘𝑖))
55	53, 54	oveq12d 6103	. . . . . . . . . . . . 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 9769	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ ℕ) → 𝑖 ∈ ℤ)
59	57, 58	rpexpcld 11137	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ ℕ) → (2↑𝑖) ∈ ℝ⁺)
60	59	rprecred 10111	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ ℕ) → (1 / (2↑𝑖)) ∈ ℝ)
61		0re 8326	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ ℝ
62		1re 8325	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℝ
63		prssi 3873	. . . . . . . . . . . . . . . 16 ⊢ ((0 ∈ ℝ ∧ 1 ∈ ℝ) → {0, 1} ⊆ ℝ)
64	61, 62, 63	mp2an 430	. . . . . . . . . . . . . . 15 ⊢ {0, 1} ⊆ ℝ
65	2	adantr 276	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → 𝐹:ℕ⟶{0, 1})
66	65	ad2antrr 492	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ ℕ) → 𝐹:ℕ⟶{0, 1})
67	66, 56	ffvelcdmd 5844	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ ℕ) → (𝐹‘𝑖) ∈ {0, 1})
68	64, 67	sselid 3246	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ ℕ) → (𝐹‘𝑖) ∈ ℝ)
69	60, 68	remulcld 8356	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ ℕ) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) ∈ ℝ)
70	51, 55, 56, 69	fvmptd3 5799	. . . . . . . . . . . 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 17097	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → seq1( + , (𝑗 ∈ ℕ ↦ ((1 / (2↑𝑗)) · (𝐹‘𝑗)))) ∈ dom ⇝ )
75		nnuz 9960	. . . . . . . . . . . . 13 ⊢ ℕ = (ℤ_≥‘1)
76	69	recnd 8354	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ ℕ) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) ∈ ℂ)
77	70, 76	eqeltrd 2315	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ ((1 / (2↑𝑗)) · (𝐹‘𝑗)))‘𝑖) ∈ ℂ)
78	75, 47, 77	iserex 12107	. . . . . . . . . . . 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 12198	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → Σ𝑖 ∈ (ℤ_≥‘(𝑛 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖)) ∈ ℝ)
81		1zzd 9673	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → 1 ∈ ℤ)
82	81, 23	fzfigd 10870	. . . . . . . . . . . 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 10430	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (1...𝑛) → 𝑖 ∈ ℤ)
86	85	adantl 277	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (1...𝑛)) → 𝑖 ∈ ℤ)
87	84, 86	rpexpcld 11137	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (1...𝑛)) → (2↑𝑖) ∈ ℝ⁺)
88	87	rprecred 10111	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (1...𝑛)) → (1 / (2↑𝑖)) ∈ ℝ)
89	83, 88	fsumrecl 12170	. . . . . . . . . 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 10110	. . . . . . . . . . . . . 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 10103	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (ℤ_≥‘(𝑛 + 1))) → 0 ≤ (1 / (2↑𝑖)))
95		0le0 9394	. . . . . . . . . . . . . 14 ⊢ 0 ≤ 0
96		simpr 110	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (ℤ_≥‘(𝑛 + 1))) ∧ (𝐹‘𝑖) = 0) → (𝐹‘𝑖) = 0)
97	95, 96	breqtrrid 4168	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (ℤ_≥‘(𝑛 + 1))) ∧ (𝐹‘𝑖) = 0) → 0 ≤ (𝐹‘𝑖))
98		0le1 8809	. . . . . . . . . . . . . 14 ⊢ 0 ≤ 1
99		simpr 110	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (ℤ_≥‘(𝑛 + 1))) ∧ (𝐹‘𝑖) = 1) → (𝐹‘𝑖) = 1)
100	98, 99	breqtrrid 4168	. . . . . . . . . . . . 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 5844	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (ℤ_≥‘(𝑛 + 1))) → (𝐹‘𝑖) ∈ {0, 1})
103		elpri 3732	. . . . . . . . . . . . . 14 ⊢ ((𝐹‘𝑖) ∈ {0, 1} → ((𝐹‘𝑖) = 0 ∨ (𝐹‘𝑖) = 1))
104	102, 103	syl 14	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (ℤ_≥‘(𝑛 + 1))) → ((𝐹‘𝑖) = 0 ∨ (𝐹‘𝑖) = 1))
105	97, 100, 104	mpjaodan 810	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (ℤ_≥‘(𝑛 + 1))) → 0 ≤ (𝐹‘𝑖))
106	90, 91, 94, 105	mulge0d 8950	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (ℤ_≥‘(𝑛 + 1))) → 0 ≤ ((1 / (2↑𝑖)) · (𝐹‘𝑖)))
107	45, 48, 71, 72, 79, 106	isumge0 12199	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → 0 ≤ Σ𝑖 ∈ (ℤ_≥‘(𝑛 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖)))
108	44, 80, 89, 107	leadd2dd 8888	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → (Σ𝑖 ∈ (1...𝑛)(1 / (2↑𝑖)) + 0) ≤ (Σ𝑖 ∈ (1...𝑛)(1 / (2↑𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑛 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖))))
109	89	recnd 8354	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → Σ𝑖 ∈ (1...𝑛)(1 / (2↑𝑖)) ∈ ℂ)
110	109	addridd 8475	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → (Σ𝑖 ∈ (1...𝑛)(1 / (2↑𝑖)) + 0) = Σ𝑖 ∈ (1...𝑛)(1 / (2↑𝑖)))
111	110	eqcomd 2244	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → Σ𝑖 ∈ (1...𝑛)(1 / (2↑𝑖)) = (Σ𝑖 ∈ (1...𝑛)(1 / (2↑𝑖)) + 0))
112	75, 45, 47, 70, 76, 74	isumsplit 12260	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹‘𝑖)) = (Σ𝑖 ∈ (1...((𝑛 + 1) − 1))((1 / (2↑𝑖)) · (𝐹‘𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑛 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖))))
113	3, 112	eqtrid 2283	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → 𝐴 = (Σ𝑖 ∈ (1...((𝑛 + 1) − 1))((1 / (2↑𝑖)) · (𝐹‘𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑛 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖))))
114	46	nncnd 9319	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → 𝑛 ∈ ℂ)
115		1cnd 8342	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → 1 ∈ ℂ)
116	114, 115	pncand 8638	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → ((𝑛 + 1) − 1) = 𝑛)
117	116	oveq2d 6101	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → (1...((𝑛 + 1) − 1)) = (1...𝑛))
118		simpr 110	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (1...𝑛)) → 𝑖 ∈ (1...𝑛))
119	118	fvresd 5720	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (1...𝑛)) → ((𝐹 ↾ (1...𝑛))‘𝑖) = (𝐹‘𝑖))
120		fveqeq2 5704	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑖 → (((𝐹 ↾ (1...𝑛))‘𝑥) = 1 ↔ ((𝐹 ↾ (1...𝑛))‘𝑖) = 1))
121		simplr 533	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (1...𝑛)) → ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1)
122	120, 121, 118	rspcdva 2934	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (1...𝑛)) → ((𝐹 ↾ (1...𝑛))‘𝑖) = 1)
123	119, 122	eqtr3d 2273	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (1...𝑛)) → (𝐹‘𝑖) = 1)
124	123	oveq2d 6101	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (1...𝑛)) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) = ((1 / (2↑𝑖)) · 1))
125	87	rpreccld 10110	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (1...𝑛)) → (1 / (2↑𝑖)) ∈ ℝ⁺)
126	125	rpcnd 10101	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (1...𝑛)) → (1 / (2↑𝑖)) ∈ ℂ)
127	126	mulridd 8343	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (1...𝑛)) → ((1 / (2↑𝑖)) · 1) = (1 / (2↑𝑖)))
128	124, 127	eqtrd 2271	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (1...𝑛)) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) = (1 / (2↑𝑖)))
129	117, 128	sumeq12rdv 12141	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → Σ𝑖 ∈ (1...((𝑛 + 1) − 1))((1 / (2↑𝑖)) · (𝐹‘𝑖)) = Σ𝑖 ∈ (1...𝑛)(1 / (2↑𝑖)))
130	129	oveq1d 6100	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → (Σ𝑖 ∈ (1...((𝑛 + 1) − 1))((1 / (2↑𝑖)) · (𝐹‘𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑛 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖))) = (Σ𝑖 ∈ (1...𝑛)(1 / (2↑𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑛 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖))))
131	113, 130	eqtrd 2271	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → 𝐴 = (Σ𝑖 ∈ (1...𝑛)(1 / (2↑𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑛 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖))))
132	108, 111, 131	3brtr4d 4162	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → Σ𝑖 ∈ (1...𝑛)(1 / (2↑𝑖)) ≤ 𝐴)
133		geo2sum 12283	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ℕ ∧ 1 ∈ ℂ) → Σ𝑖 ∈ (1...𝑛)(1 / (2↑𝑖)) = (1 − (1 / (2↑𝑛))))
134	133	breq1d 4140	. . . . . . . . 9 ⊢ ((𝑛 ∈ ℕ ∧ 1 ∈ ℂ) → (Σ𝑖 ∈ (1...𝑛)(1 / (2↑𝑖)) ≤ 𝐴 ↔ (1 − (1 / (2↑𝑛))) ≤ 𝐴))
135	46, 115, 134	syl2anc 415	. . . . . . . 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 8876	. . . . . 6 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → (1 − 𝐴) ≤ (1 / (2↑𝑛)))
138	40, 41, 137	lensymd 8448	. . . . 5 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → ¬ (1 / (2↑𝑛)) < (1 − 𝐴))
139	39, 138	pm2.21dd 629	. . . 4 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → ∃𝑥 ∈ ℕ (𝐹‘𝑥) = 0)
140	139	ex 115	. . 3 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → (∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1 → ∃𝑥 ∈ ℕ (𝐹‘𝑥) = 0))
141		fveq1 5694	. . . . . . 7 ⊢ (𝑓 = (𝐹 ↾ (1...𝑛)) → (𝑓‘𝑥) = ((𝐹 ↾ (1...𝑛))‘𝑥))
142	141	eqeq1d 2247	. . . . . 6 ⊢ (𝑓 = (𝐹 ↾ (1...𝑛)) → ((𝑓‘𝑥) = 0 ↔ ((𝐹 ↾ (1...𝑛))‘𝑥) = 0))
143	142	rexbidv 2551	. . . . 5 ⊢ (𝑓 = (𝐹 ↾ (1...𝑛)) → (∃𝑥 ∈ (1...𝑛)(𝑓‘𝑥) = 0 ↔ ∃𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 0))
144	141	eqeq1d 2247	. . . . . 6 ⊢ (𝑓 = (𝐹 ↾ (1...𝑛)) → ((𝑓‘𝑥) = 1 ↔ ((𝐹 ↾ (1...𝑛))‘𝑥) = 1))
145	144	ralbidv 2550	. . . . 5 ⊢ (𝑓 = (𝐹 ↾ (1...𝑛)) → (∀𝑥 ∈ (1...𝑛)(𝑓‘𝑥) = 1 ↔ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1))
146	143, 145	orbi12d 805	. . . 4 ⊢ (𝑓 = (𝐹 ↾ (1...𝑛)) → ((∃𝑥 ∈ (1...𝑛)(𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ (1...𝑛)(𝑓‘𝑥) = 1) ↔ (∃𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 0 ∨ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1)))
147		finomni 7480	. . . . . 6 ⊢ ((1...𝑛) ∈ Fin → (1...𝑛) ∈ Omni)
148	82, 147	syl 14	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → (1...𝑛) ∈ Omni)
149		isomninn 17092	. . . . . 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 10464	. . . . . . 7 ⊢ (1...𝑛) ⊆ ℕ
153	152	a1i 9	. . . . . 6 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → (1...𝑛) ⊆ ℕ)
154	65, 153	fssresd 5566	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → (𝐹 ↾ (1...𝑛)):(1...𝑛)⟶{0, 1})
155		0red 8327	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → 0 ∈ ℝ)
156		1red 8341	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → 1 ∈ ℝ)
157		prexg 4349	. . . . . . 7 ⊢ ((0 ∈ ℝ ∧ 1 ∈ ℝ) → {0, 1} ∈ V)
158	155, 156, 157	syl2anc 415	. . . . . 6 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → {0, 1} ∈ V)
159	158, 82	elmapd 6936	. . . . 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 2934	. . 3 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → (∃𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 0 ∨ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1))
162	19, 140, 161	mpjaod 730	. 2 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → ∃𝑥 ∈ ℕ (𝐹‘𝑥) = 0)
163	10, 162	rexlimddv 2673	1 ⊢ (𝜑 → ∃𝑥 ∈ ℕ (𝐹‘𝑥) = 0)

Colors of variables: wff set class

This proof depends on syntax axioms: → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 720 = wceq 1402 ∈ wcel 2209 ∀wral 2528 ∃wrex 2529 Vcvv 2821 ⊆ wss 3220 {cpr 3710 class class class wbr 4130 ↦ cmpt 4192 dom cdm 4774 ↾ cres 4776 ⟶wf 5373 ‘cfv 5377 (class class class)co 6085 ↑_𝑚 cmap 6922 Fincfn 7022 Omnicomni 7474 ℂcc 8177 ℝcr 8178 0cc0 8179 1c1 8180 + caddc 8182 · cmul 8184 < clt 8360 ≤ cle 8361 − cmin 8497 / cdiv 9003 ℕcn 9305 2c2 9356 ℕ₀cn0 9565 ℤcz 9646 ℤ_≥cuz 9923 ℝ⁺crp 10056 ...cfz 10413 seqcseq 10886 ↑cexp 10977 ⇝ cli 12046 Σcsu 12121

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 623 ax-in2 624 ax-io 721 ax-5 1500 ax-7 1501 ax-gen 1502 ax-ie1 1546 ax-ie2 1547 ax-8 1557 ax-10 1558 ax-11 1559 ax-i12 1560 ax-bndl 1562 ax-4 1563 ax-17 1579 ax-i9 1583 ax-ial 1587 ax-i5r 1588 ax-14 2212 ax-ext 2220 ax-coll 4246 ax-sep 4249 ax-nul 4259 ax-pow 4311 ax-pr 4346 ax-un 4578 ax-setind 4684 ax-iinf 4735 ax-cnex 8270 ax-resscn 8271 ax-1cn 8272 ax-1re 8273 ax-icn 8274 ax-addcl 8275 ax-addrcl 8276 ax-mulcl 8277 ax-mulrcl 8278 ax-addcom 8279 ax-mulcom 8280 ax-addass 8281 ax-mulass 8282 ax-distr 8283 ax-i2m1 8284 ax-0lt1 8285 ax-1rid 8286 ax-0id 8287 ax-rnegex 8288 ax-precex 8289 ax-cnre 8290 ax-pre-ltirr 8291 ax-pre-ltwlin 8292 ax-pre-lttrn 8293 ax-pre-apti 8294 ax-pre-ltadd 8295 ax-pre-mulgt0 8296 ax-pre-mulext 8297 ax-arch 8298 ax-caucvg 8299

This proof depends on definitions: df-bi 117 df-dc 847 df-3or 1010 df-3an 1011 df-tru 1405 df-fal 1408 df-nf 1514 df-sb 1816 df-eu 2089 df-mo 2090 df-clab 2225 df-cleq 2231 df-clel 2234 df-nfc 2381 df-ne 2421 df-nel 2516 df-ral 2533 df-rex 2534 df-reu 2535 df-rmo 2536 df-rab 2537 df-v 2823 df-sbc 3052 df-csb 3148 df-dif 3222 df-un 3224 df-in 3226 df-ss 3233 df-nul 3521 df-if 3639 df-pw 3690 df-sn 3715 df-pr 3716 df-op 3718 df-uni 3936 df-int 3971 df-iun 4014 df-br 4131 df-opab 4193 df-mpt 4194 df-tr 4230 df-id 4438 df-po 4441 df-iso 4442 df-iord 4511 df-on 4513 df-ilim 4514 df-suc 4516 df-iom 4738 df-xp 4780 df-rel 4781 df-cnv 4782 df-co 4783 df-dm 4784 df-rn 4785 df-res 4786 df-ima 4787 df-iota 5337 df-fun 5379 df-fn 5380 df-f 5381 df-f1 5382 df-fo 5383 df-f1o 5384 df-fv 5385 df-isom 5386 df-riota 6038 df-ov 6088 df-oprab 6089 df-mpo 6090 df-1st 6374 df-2nd 6375 df-recs 6576 df-irdg 6641 df-frec 6662 df-1o 6687 df-2o 6688 df-oadd 6691 df-er 6807 df-map 6924 df-en 7023 df-dom 7024 df-fin 7025 df-omni 7475 df-pnf 8362 df-mnf 8363 df-xr 8364 df-ltxr 8365 df-le 8366 df-sub 8499 df-neg 8500 df-reap 8904 df-ap 8911 df-div 9004 df-inn 9306 df-2 9364 df-3 9365 df-4 9366 df-n0 9566 df-z 9647 df-uz 9924 df-q 10022 df-rp 10057 df-ico 10298 df-fz 10414 df-fzo 10552 df-seqfrec 10887 df-exp 10978 df-ihash 11217 df-cj 11609 df-re 11610 df-im 11611 df-rsqrt 11766 df-abs 11767 df-clim 12047 df-sumdc 12122

This theorem is used by: trilpolemres 17103 neapmkvlem 17129

W3C validator