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 14073

Description: Lemma for trilpo 14075. 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 7116 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 7935	. . . 4 ⊢ (𝜑 → 1 ∈ ℝ)
2		trilpolemgt1.f	. . . . 5 ⊢ (𝜑 → 𝐹:ℕ⟶{0, 1})
3		trilpolemgt1.a	. . . . 5 ⊢ 𝐴 = Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹‘𝑖))
4	2, 3	trilpolemcl 14069	. . . 4 ⊢ (𝜑 → 𝐴 ∈ ℝ)
5	1, 4	resubcld 8300	. . 3 ⊢ (𝜑 → (1 − 𝐴) ∈ ℝ)
6		trilpolemlt1.a	. . . 4 ⊢ (𝜑 → 𝐴 < 1)
7	4, 1	posdifd 8451	. . . 4 ⊢ (𝜑 → (𝐴 < 1 ↔ 0 < (1 − 𝐴)))
8	6, 7	mpbid 146	. . 3 ⊢ (𝜑 → 0 < (1 − 𝐴))
9		nnrecl 9133	. . 3 ⊢ (((1 − 𝐴) ∈ ℝ ∧ 0 < (1 − 𝐴)) → ∃𝑛 ∈ ℕ (1 / 𝑛) < (1 − 𝐴))
10	5, 8, 9	syl2anc 409	. 2 ⊢ (𝜑 → ∃𝑛 ∈ ℕ (1 / 𝑛) < (1 − 𝐴))
11		elfznn 10010	. . . . . . 7 ⊢ (𝑥 ∈ (1...𝑛) → 𝑥 ∈ ℕ)
12	11	ad2antrl 487	. . . . . 6 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ (𝑥 ∈ (1...𝑛) ∧ ((𝐹 ↾ (1...𝑛))‘𝑥) = 0)) → 𝑥 ∈ ℕ)
13		simprl 526	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ (𝑥 ∈ (1...𝑛) ∧ ((𝐹 ↾ (1...𝑛))‘𝑥) = 0)) → 𝑥 ∈ (1...𝑛))
14	13	fvresd 5521	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ (𝑥 ∈ (1...𝑛) ∧ ((𝐹 ↾ (1...𝑛))‘𝑥) = 0)) → ((𝐹 ↾ (1...𝑛))‘𝑥) = (𝐹‘𝑥))
15		simprr 527	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ (𝑥 ∈ (1...𝑛) ∧ ((𝐹 ↾ (1...𝑛))‘𝑥) = 0)) → ((𝐹 ↾ (1...𝑛))‘𝑥) = 0)
16	14, 15	eqtr3d 2205	. . . . . 6 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ (𝑥 ∈ (1...𝑛) ∧ ((𝐹 ↾ (1...𝑛))‘𝑥) = 0)) → (𝐹‘𝑥) = 0)
17	12, 16	jca 304	. . . . 5 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ (𝑥 ∈ (1...𝑛) ∧ ((𝐹 ↾ (1...𝑛))‘𝑥) = 0)) → (𝑥 ∈ ℕ ∧ (𝐹‘𝑥) = 0))
18	17	ex 114	. . . 4 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → ((𝑥 ∈ (1...𝑛) ∧ ((𝐹 ↾ (1...𝑛))‘𝑥) = 0) → (𝑥 ∈ ℕ ∧ (𝐹‘𝑥) = 0)))
19	18	reximdv2 2569	. . 3 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → (∃𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 0 → ∃𝑥 ∈ ℕ (𝐹‘𝑥) = 0))
20		2rp 9615	. . . . . . . . . 10 ⊢ 2 ∈ ℝ⁺
21	20	a1i 9	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → 2 ∈ ℝ⁺)
22		simprl 526	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → 𝑛 ∈ ℕ)
23	22	nnzd 9333	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → 𝑛 ∈ ℤ)
24	21, 23	rpexpcld 10633	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → (2↑𝑛) ∈ ℝ⁺)
25	24	rprecred 9665	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → (1 / (2↑𝑛)) ∈ ℝ)
26	22	nnrecred 8925	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → (1 / 𝑛) ∈ ℝ)
27	5	adantr 274	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → (1 − 𝐴) ∈ ℝ)
28		2z 9240	. . . . . . . . . 10 ⊢ 2 ∈ ℤ
29		uzid 9501	. . . . . . . . . 10 ⊢ (2 ∈ ℤ → 2 ∈ (ℤ_≥‘2))
30	28, 29	mp1i 10	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → 2 ∈ (ℤ_≥‘2))
31	22	nnnn0d 9188	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → 𝑛 ∈ ℕ₀)
32		bernneq3 10598	. . . . . . . . 9 ⊢ ((2 ∈ (ℤ_≥‘2) ∧ 𝑛 ∈ ℕ₀) → 𝑛 < (2↑𝑛))
33	30, 31, 32	syl2anc 409	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → 𝑛 < (2↑𝑛))
34	22	nnrpd 9651	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → 𝑛 ∈ ℝ⁺)
35	34, 24	ltrecd 9672	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → (𝑛 < (2↑𝑛) ↔ (1 / (2↑𝑛)) < (1 / 𝑛)))
36	33, 35	mpbid 146	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → (1 / (2↑𝑛)) < (1 / 𝑛))
37		simprr 527	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → (1 / 𝑛) < (1 − 𝐴))
38	25, 26, 27, 36, 37	lttrd 8045	. . . . . 6 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → (1 / (2↑𝑛)) < (1 − 𝐴))
39	38	adantr 274	. . . . 5 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → (1 / (2↑𝑛)) < (1 − 𝐴))
40	27	adantr 274	. . . . . 6 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → (1 − 𝐴) ∈ ℝ)
41	25	adantr 274	. . . . . 6 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → (1 / (2↑𝑛)) ∈ ℝ)
42		1red 7935	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → 1 ∈ ℝ)
43	4	ad2antrr 485	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → 𝐴 ∈ ℝ)
44		0red 7921	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → 0 ∈ ℝ)
45		eqid 2170	. . . . . . . . . . 11 ⊢ (ℤ_≥‘(𝑛 + 1)) = (ℤ_≥‘(𝑛 + 1))
46	22	adantr 274	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → 𝑛 ∈ ℕ)
47	46	peano2nnd 8893	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → (𝑛 + 1) ∈ ℕ)
48	47	nnzd 9333	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → (𝑛 + 1) ∈ ℤ)
49		eluznn 9559	. . . . . . . . . . . . 13 ⊢ (((𝑛 + 1) ∈ ℕ ∧ 𝑖 ∈ (ℤ_≥‘(𝑛 + 1))) → 𝑖 ∈ ℕ)
50	47, 49	sylan 281	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (ℤ_≥‘(𝑛 + 1))) → 𝑖 ∈ ℕ)
51		eqid 2170	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ ℕ ↦ ((1 / (2↑𝑗)) · (𝐹‘𝑗))) = (𝑗 ∈ ℕ ↦ ((1 / (2↑𝑗)) · (𝐹‘𝑗)))
52		oveq2 5861	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝑖 → (2↑𝑗) = (2↑𝑖))
53	52	oveq2d 5869	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑖 → (1 / (2↑𝑗)) = (1 / (2↑𝑖)))
54		fveq2 5496	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑖 → (𝐹‘𝑗) = (𝐹‘𝑖))
55	53, 54	oveq12d 5871	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑖 → ((1 / (2↑𝑗)) · (𝐹‘𝑗)) = ((1 / (2↑𝑖)) · (𝐹‘𝑖)))
56		simpr 109	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ ℕ) → 𝑖 ∈ ℕ)
57	20	a1i 9	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ ℕ) → 2 ∈ ℝ⁺)
58	56	nnzd 9333	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ ℕ) → 𝑖 ∈ ℤ)
59	57, 58	rpexpcld 10633	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ ℕ) → (2↑𝑖) ∈ ℝ⁺)
60	59	rprecred 9665	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ ℕ) → (1 / (2↑𝑖)) ∈ ℝ)
61		0re 7920	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ ℝ
62		1re 7919	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℝ
63		prssi 3738	. . . . . . . . . . . . . . . 16 ⊢ ((0 ∈ ℝ ∧ 1 ∈ ℝ) → {0, 1} ⊆ ℝ)
64	61, 62, 63	mp2an 424	. . . . . . . . . . . . . . 15 ⊢ {0, 1} ⊆ ℝ
65	2	adantr 274	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → 𝐹:ℕ⟶{0, 1})
66	65	ad2antrr 485	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ ℕ) → 𝐹:ℕ⟶{0, 1})
67	66, 56	ffvelrnd 5632	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ ℕ) → (𝐹‘𝑖) ∈ {0, 1})
68	64, 67	sselid 3145	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ ℕ) → (𝐹‘𝑖) ∈ ℝ)
69	60, 68	remulcld 7950	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ ℕ) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) ∈ ℝ)
70	51, 55, 56, 69	fvmptd3 5589	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ ((1 / (2↑𝑗)) · (𝐹‘𝑗)))‘𝑖) = ((1 / (2↑𝑖)) · (𝐹‘𝑖)))
71	50, 70	syldan 280	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (ℤ_≥‘(𝑛 + 1))) → ((𝑗 ∈ ℕ ↦ ((1 / (2↑𝑗)) · (𝐹‘𝑗)))‘𝑖) = ((1 / (2↑𝑖)) · (𝐹‘𝑖)))
72	50, 69	syldan 280	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (ℤ_≥‘(𝑛 + 1))) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) ∈ ℝ)
73	65	adantr 274	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → 𝐹:ℕ⟶{0, 1})
74	73, 51	trilpolemclim 14068	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → seq1( + , (𝑗 ∈ ℕ ↦ ((1 / (2↑𝑗)) · (𝐹‘𝑗)))) ∈ dom ⇝ )
75		nnuz 9522	. . . . . . . . . . . . 13 ⊢ ℕ = (ℤ_≥‘1)
76	69	recnd 7948	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ ℕ) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) ∈ ℂ)
77	70, 76	eqeltrd 2247	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ ((1 / (2↑𝑗)) · (𝐹‘𝑗)))‘𝑖) ∈ ℂ)
78	75, 47, 77	iserex 11302	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → (seq1( + , (𝑗 ∈ ℕ ↦ ((1 / (2↑𝑗)) · (𝐹‘𝑗)))) ∈ dom ⇝ ↔ seq(𝑛 + 1)( + , (𝑗 ∈ ℕ ↦ ((1 / (2↑𝑗)) · (𝐹‘𝑗)))) ∈ dom ⇝ ))
79	74, 78	mpbid 146	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → seq(𝑛 + 1)( + , (𝑗 ∈ ℕ ↦ ((1 / (2↑𝑗)) · (𝐹‘𝑗)))) ∈ dom ⇝ )
80	45, 48, 71, 72, 79	isumrecl 11392	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → Σ𝑖 ∈ (ℤ_≥‘(𝑛 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖)) ∈ ℝ)
81		1zzd 9239	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → 1 ∈ ℤ)
82	81, 23	fzfigd 10387	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → (1...𝑛) ∈ Fin)
83	82	adantr 274	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → (1...𝑛) ∈ Fin)
84	20	a1i 9	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (1...𝑛)) → 2 ∈ ℝ⁺)
85		elfzelz 9981	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (1...𝑛) → 𝑖 ∈ ℤ)
86	85	adantl 275	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (1...𝑛)) → 𝑖 ∈ ℤ)
87	84, 86	rpexpcld 10633	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (1...𝑛)) → (2↑𝑖) ∈ ℝ⁺)
88	87	rprecred 9665	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (1...𝑛)) → (1 / (2↑𝑖)) ∈ ℝ)
89	83, 88	fsumrecl 11364	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → Σ𝑖 ∈ (1...𝑛)(1 / (2↑𝑖)) ∈ ℝ)
90	50, 60	syldan 280	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (ℤ_≥‘(𝑛 + 1))) → (1 / (2↑𝑖)) ∈ ℝ)
91	50, 68	syldan 280	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (ℤ_≥‘(𝑛 + 1))) → (𝐹‘𝑖) ∈ ℝ)
92	59	rpreccld 9664	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ ℕ) → (1 / (2↑𝑖)) ∈ ℝ⁺)
93	50, 92	syldan 280	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (ℤ_≥‘(𝑛 + 1))) → (1 / (2↑𝑖)) ∈ ℝ⁺)
94	93	rpge0d 9657	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (ℤ_≥‘(𝑛 + 1))) → 0 ≤ (1 / (2↑𝑖)))
95		0le0 8967	. . . . . . . . . . . . . 14 ⊢ 0 ≤ 0
96		simpr 109	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (ℤ_≥‘(𝑛 + 1))) ∧ (𝐹‘𝑖) = 0) → (𝐹‘𝑖) = 0)
97	95, 96	breqtrrid 4027	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (ℤ_≥‘(𝑛 + 1))) ∧ (𝐹‘𝑖) = 0) → 0 ≤ (𝐹‘𝑖))
98		0le1 8400	. . . . . . . . . . . . . 14 ⊢ 0 ≤ 1
99		simpr 109	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (ℤ_≥‘(𝑛 + 1))) ∧ (𝐹‘𝑖) = 1) → (𝐹‘𝑖) = 1)
100	98, 99	breqtrrid 4027	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (ℤ_≥‘(𝑛 + 1))) ∧ (𝐹‘𝑖) = 1) → 0 ≤ (𝐹‘𝑖))
101	73	adantr 274	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (ℤ_≥‘(𝑛 + 1))) → 𝐹:ℕ⟶{0, 1})
102	101, 50	ffvelrnd 5632	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (ℤ_≥‘(𝑛 + 1))) → (𝐹‘𝑖) ∈ {0, 1})
103		elpri 3606	. . . . . . . . . . . . . 14 ⊢ ((𝐹‘𝑖) ∈ {0, 1} → ((𝐹‘𝑖) = 0 ∨ (𝐹‘𝑖) = 1))
104	102, 103	syl 14	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (ℤ_≥‘(𝑛 + 1))) → ((𝐹‘𝑖) = 0 ∨ (𝐹‘𝑖) = 1))
105	97, 100, 104	mpjaodan 793	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (ℤ_≥‘(𝑛 + 1))) → 0 ≤ (𝐹‘𝑖))
106	90, 91, 94, 105	mulge0d 8540	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (ℤ_≥‘(𝑛 + 1))) → 0 ≤ ((1 / (2↑𝑖)) · (𝐹‘𝑖)))
107	45, 48, 71, 72, 79, 106	isumge0 11393	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → 0 ≤ Σ𝑖 ∈ (ℤ_≥‘(𝑛 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖)))
108	44, 80, 89, 107	leadd2dd 8479	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → (Σ𝑖 ∈ (1...𝑛)(1 / (2↑𝑖)) + 0) ≤ (Σ𝑖 ∈ (1...𝑛)(1 / (2↑𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑛 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖))))
109	89	recnd 7948	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → Σ𝑖 ∈ (1...𝑛)(1 / (2↑𝑖)) ∈ ℂ)
110	109	addid1d 8068	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → (Σ𝑖 ∈ (1...𝑛)(1 / (2↑𝑖)) + 0) = Σ𝑖 ∈ (1...𝑛)(1 / (2↑𝑖)))
111	110	eqcomd 2176	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → Σ𝑖 ∈ (1...𝑛)(1 / (2↑𝑖)) = (Σ𝑖 ∈ (1...𝑛)(1 / (2↑𝑖)) + 0))
112	75, 45, 47, 70, 76, 74	isumsplit 11454	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹‘𝑖)) = (Σ𝑖 ∈ (1...((𝑛 + 1) − 1))((1 / (2↑𝑖)) · (𝐹‘𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑛 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖))))
113	3, 112	eqtrid 2215	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → 𝐴 = (Σ𝑖 ∈ (1...((𝑛 + 1) − 1))((1 / (2↑𝑖)) · (𝐹‘𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑛 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖))))
114	46	nncnd 8892	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → 𝑛 ∈ ℂ)
115		1cnd 7936	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → 1 ∈ ℂ)
116	114, 115	pncand 8231	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → ((𝑛 + 1) − 1) = 𝑛)
117	116	oveq2d 5869	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → (1...((𝑛 + 1) − 1)) = (1...𝑛))
118		simpr 109	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (1...𝑛)) → 𝑖 ∈ (1...𝑛))
119	118	fvresd 5521	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (1...𝑛)) → ((𝐹 ↾ (1...𝑛))‘𝑖) = (𝐹‘𝑖))
120		fveqeq2 5505	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑖 → (((𝐹 ↾ (1...𝑛))‘𝑥) = 1 ↔ ((𝐹 ↾ (1...𝑛))‘𝑖) = 1))
121		simplr 525	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (1...𝑛)) → ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1)
122	120, 121, 118	rspcdva 2839	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (1...𝑛)) → ((𝐹 ↾ (1...𝑛))‘𝑖) = 1)
123	119, 122	eqtr3d 2205	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (1...𝑛)) → (𝐹‘𝑖) = 1)
124	123	oveq2d 5869	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (1...𝑛)) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) = ((1 / (2↑𝑖)) · 1))
125	87	rpreccld 9664	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (1...𝑛)) → (1 / (2↑𝑖)) ∈ ℝ⁺)
126	125	rpcnd 9655	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (1...𝑛)) → (1 / (2↑𝑖)) ∈ ℂ)
127	126	mulid1d 7937	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (1...𝑛)) → ((1 / (2↑𝑖)) · 1) = (1 / (2↑𝑖)))
128	124, 127	eqtrd 2203	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) ∧ 𝑖 ∈ (1...𝑛)) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) = (1 / (2↑𝑖)))
129	117, 128	sumeq12rdv 11336	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → Σ𝑖 ∈ (1...((𝑛 + 1) − 1))((1 / (2↑𝑖)) · (𝐹‘𝑖)) = Σ𝑖 ∈ (1...𝑛)(1 / (2↑𝑖)))
130	129	oveq1d 5868	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → (Σ𝑖 ∈ (1...((𝑛 + 1) − 1))((1 / (2↑𝑖)) · (𝐹‘𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑛 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖))) = (Σ𝑖 ∈ (1...𝑛)(1 / (2↑𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑛 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖))))
131	113, 130	eqtrd 2203	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → 𝐴 = (Σ𝑖 ∈ (1...𝑛)(1 / (2↑𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑛 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖))))
132	108, 111, 131	3brtr4d 4021	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → Σ𝑖 ∈ (1...𝑛)(1 / (2↑𝑖)) ≤ 𝐴)
133		geo2sum 11477	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ℕ ∧ 1 ∈ ℂ) → Σ𝑖 ∈ (1...𝑛)(1 / (2↑𝑖)) = (1 − (1 / (2↑𝑛))))
134	133	breq1d 3999	. . . . . . . . 9 ⊢ ((𝑛 ∈ ℕ ∧ 1 ∈ ℂ) → (Σ𝑖 ∈ (1...𝑛)(1 / (2↑𝑖)) ≤ 𝐴 ↔ (1 − (1 / (2↑𝑛))) ≤ 𝐴))
135	46, 115, 134	syl2anc 409	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → (Σ𝑖 ∈ (1...𝑛)(1 / (2↑𝑖)) ≤ 𝐴 ↔ (1 − (1 / (2↑𝑛))) ≤ 𝐴))
136	132, 135	mpbid 146	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → (1 − (1 / (2↑𝑛))) ≤ 𝐴)
137	42, 41, 43, 136	subled 8467	. . . . . 6 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → (1 − 𝐴) ≤ (1 / (2↑𝑛)))
138	40, 41, 137	lensymd 8041	. . . . 5 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → ¬ (1 / (2↑𝑛)) < (1 − 𝐴))
139	39, 138	pm2.21dd 615	. . . 4 ⊢ (((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) ∧ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1) → ∃𝑥 ∈ ℕ (𝐹‘𝑥) = 0)
140	139	ex 114	. . 3 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → (∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1 → ∃𝑥 ∈ ℕ (𝐹‘𝑥) = 0))
141		fveq1 5495	. . . . . . 7 ⊢ (𝑓 = (𝐹 ↾ (1...𝑛)) → (𝑓‘𝑥) = ((𝐹 ↾ (1...𝑛))‘𝑥))
142	141	eqeq1d 2179	. . . . . 6 ⊢ (𝑓 = (𝐹 ↾ (1...𝑛)) → ((𝑓‘𝑥) = 0 ↔ ((𝐹 ↾ (1...𝑛))‘𝑥) = 0))
143	142	rexbidv 2471	. . . . 5 ⊢ (𝑓 = (𝐹 ↾ (1...𝑛)) → (∃𝑥 ∈ (1...𝑛)(𝑓‘𝑥) = 0 ↔ ∃𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 0))
144	141	eqeq1d 2179	. . . . . 6 ⊢ (𝑓 = (𝐹 ↾ (1...𝑛)) → ((𝑓‘𝑥) = 1 ↔ ((𝐹 ↾ (1...𝑛))‘𝑥) = 1))
145	144	ralbidv 2470	. . . . 5 ⊢ (𝑓 = (𝐹 ↾ (1...𝑛)) → (∀𝑥 ∈ (1...𝑛)(𝑓‘𝑥) = 1 ↔ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1))
146	143, 145	orbi12d 788	. . . 4 ⊢ (𝑓 = (𝐹 ↾ (1...𝑛)) → ((∃𝑥 ∈ (1...𝑛)(𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ (1...𝑛)(𝑓‘𝑥) = 1) ↔ (∃𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 0 ∨ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1)))
147		finomni 7116	. . . . . 6 ⊢ ((1...𝑛) ∈ Fin → (1...𝑛) ∈ Omni)
148	82, 147	syl 14	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → (1...𝑛) ∈ Omni)
149		isomninn 14063	. . . . . 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 146	. . . 4 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → ∀𝑓 ∈ ({0, 1} ↑_𝑚 (1...𝑛))(∃𝑥 ∈ (1...𝑛)(𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ (1...𝑛)(𝑓‘𝑥) = 1))
152		fz1ssnn 10012	. . . . . . 7 ⊢ (1...𝑛) ⊆ ℕ
153	152	a1i 9	. . . . . 6 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → (1...𝑛) ⊆ ℕ)
154	65, 153	fssresd 5374	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → (𝐹 ↾ (1...𝑛)):(1...𝑛)⟶{0, 1})
155		0red 7921	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → 0 ∈ ℝ)
156		1red 7935	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → 1 ∈ ℝ)
157		prexg 4196	. . . . . . 7 ⊢ ((0 ∈ ℝ ∧ 1 ∈ ℝ) → {0, 1} ∈ V)
158	155, 156, 157	syl2anc 409	. . . . . 6 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → {0, 1} ∈ V)
159	158, 82	elmapd 6640	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → ((𝐹 ↾ (1...𝑛)) ∈ ({0, 1} ↑_𝑚 (1...𝑛)) ↔ (𝐹 ↾ (1...𝑛)):(1...𝑛)⟶{0, 1}))
160	154, 159	mpbird 166	. . . 4 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → (𝐹 ↾ (1...𝑛)) ∈ ({0, 1} ↑_𝑚 (1...𝑛)))
161	146, 151, 160	rspcdva 2839	. . 3 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → (∃𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 0 ∨ ∀𝑥 ∈ (1...𝑛)((𝐹 ↾ (1...𝑛))‘𝑥) = 1))
162	19, 140, 161	mpjaod 713	. 2 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (1 − 𝐴))) → ∃𝑥 ∈ ℕ (𝐹‘𝑥) = 0)
163	10, 162	rexlimddv 2592	1 ⊢ (𝜑 → ∃𝑥 ∈ ℕ (𝐹‘𝑥) = 0)

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 ∨ wo 703 = wceq 1348 ∈ wcel 2141 ∀wral 2448 ∃wrex 2449 Vcvv 2730 ⊆ wss 3121 {cpr 3584 class class class wbr 3989 ↦ cmpt 4050 dom cdm 4611 ↾ cres 4613 ⟶wf 5194 ‘cfv 5198 (class class class)co 5853 ↑_𝑚 cmap 6626 Fincfn 6718 Omnicomni 7110 ℂcc 7772 ℝcr 7773 0cc0 7774 1c1 7775 + caddc 7777 · cmul 7779 < clt 7954 ≤ cle 7955 − cmin 8090 / cdiv 8589 ℕcn 8878 2c2 8929 ℕ₀cn0 9135 ℤcz 9212 ℤ_≥cuz 9487 ℝ⁺crp 9610 ...cfz 9965 seqcseq 10401 ↑cexp 10475 ⇝ cli 11241 Σcsu 11316

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 609 ax-in2 610 ax-io 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-10 1498 ax-11 1499 ax-i12 1500 ax-bndl 1502 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-13 2143 ax-14 2144 ax-ext 2152 ax-coll 4104 ax-sep 4107 ax-nul 4115 ax-pow 4160 ax-pr 4194 ax-un 4418 ax-setind 4521 ax-iinf 4572 ax-cnex 7865 ax-resscn 7866 ax-1cn 7867 ax-1re 7868 ax-icn 7869 ax-addcl 7870 ax-addrcl 7871 ax-mulcl 7872 ax-mulrcl 7873 ax-addcom 7874 ax-mulcom 7875 ax-addass 7876 ax-mulass 7877 ax-distr 7878 ax-i2m1 7879 ax-0lt1 7880 ax-1rid 7881 ax-0id 7882 ax-rnegex 7883 ax-precex 7884 ax-cnre 7885 ax-pre-ltirr 7886 ax-pre-ltwlin 7887 ax-pre-lttrn 7888 ax-pre-apti 7889 ax-pre-ltadd 7890 ax-pre-mulgt0 7891 ax-pre-mulext 7892 ax-arch 7893 ax-caucvg 7894

This theorem depends on definitions: df-bi 116 df-dc 830 df-3or 974 df-3an 975 df-tru 1351 df-fal 1354 df-nf 1454 df-sb 1756 df-eu 2022 df-mo 2023 df-clab 2157 df-cleq 2163 df-clel 2166 df-nfc 2301 df-ne 2341 df-nel 2436 df-ral 2453 df-rex 2454 df-reu 2455 df-rmo 2456 df-rab 2457 df-v 2732 df-sbc 2956 df-csb 3050 df-dif 3123 df-un 3125 df-in 3127 df-ss 3134 df-nul 3415 df-if 3527 df-pw 3568 df-sn 3589 df-pr 3590 df-op 3592 df-uni 3797 df-int 3832 df-iun 3875 df-br 3990 df-opab 4051 df-mpt 4052 df-tr 4088 df-id 4278 df-po 4281 df-iso 4282 df-iord 4351 df-on 4353 df-ilim 4354 df-suc 4356 df-iom 4575 df-xp 4617 df-rel 4618 df-cnv 4619 df-co 4620 df-dm 4621 df-rn 4622 df-res 4623 df-ima 4624 df-iota 5160 df-fun 5200 df-fn 5201 df-f 5202 df-f1 5203 df-fo 5204 df-f1o 5205 df-fv 5206 df-isom 5207 df-riota 5809 df-ov 5856 df-oprab 5857 df-mpo 5858 df-1st 6119 df-2nd 6120 df-recs 6284 df-irdg 6349 df-frec 6370 df-1o 6395 df-2o 6396 df-oadd 6399 df-er 6513 df-map 6628 df-en 6719 df-dom 6720 df-fin 6721 df-omni 7111 df-pnf 7956 df-mnf 7957 df-xr 7958 df-ltxr 7959 df-le 7960 df-sub 8092 df-neg 8093 df-reap 8494 df-ap 8501 df-div 8590 df-inn 8879 df-2 8937 df-3 8938 df-4 8939 df-n0 9136 df-z 9213 df-uz 9488 df-q 9579 df-rp 9611 df-ico 9851 df-fz 9966 df-fzo 10099 df-seqfrec 10402 df-exp 10476 df-ihash 10710 df-cj 10806 df-re 10807 df-im 10808 df-rsqrt 10962 df-abs 10963 df-clim 11242 df-sumdc 11317

This theorem is referenced by: trilpolemres 14074 neapmkvlem 14098

W3C validator