trilpolemeq1 - Mathbox for Jim Kingdon

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

Theorem trilpolemeq1 16367

Description: Lemma for trilpo 16370. The 𝐴 = 1 case. This is proved by noting that if any (𝐹‘𝑥) is zero, then the infinite sum 𝐴 is less than one based on the term which is zero. We are using the fact that the 𝐹 sequence is decidable (in the sense that each element is either zero or one). (Contributed by Jim Kingdon, 23-Aug-2023.)

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

**Assertion**
Ref	Expression
trilpolemeq1	⊢ (𝜑 → ∀𝑥 ∈ ℕ (𝐹‘𝑥) = 1)

Distinct variable groups: 𝑖,𝐹 𝜑,𝑖,𝑥 Allowed substitution hints: 𝐴(𝑥,𝑖) 𝐹(𝑥)

Proof of Theorem trilpolemeq1 Dummy variable 𝑛 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		trilpolemeq1.a	. . . . 5 ⊢ (𝜑 → 𝐴 = 1)
2	1	ad2antrr 488	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝐴 = 1)
3		trilpolemgt1.f	. . . . . . . 8 ⊢ (𝜑 → 𝐹:ℕ⟶{0, 1})
4		trilpolemgt1.a	. . . . . . . 8 ⊢ 𝐴 = Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹‘𝑖))
5	3, 4	trilpolemcl 16364	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℝ)
6	5	ad2antrr 488	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝐴 ∈ ℝ)
7		nnuz 9754	. . . . . . . . . . . . . 14 ⊢ ℕ = (ℤ_≥‘1)
8		eqid 2229	. . . . . . . . . . . . . 14 ⊢ (ℤ_≥‘(𝑥 + 1)) = (ℤ_≥‘(𝑥 + 1))
9		simplr 528	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝑥 ∈ ℕ)
10	9	peano2nnd 9121	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (𝑥 + 1) ∈ ℕ)
11		eqid 2229	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ ↦ ((1 / (2↑𝑛)) · (𝐹‘𝑛))) = (𝑛 ∈ ℕ ↦ ((1 / (2↑𝑛)) · (𝐹‘𝑛)))
12		oveq2 6008	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑖 → (2↑𝑛) = (2↑𝑖))
13	12	oveq2d 6016	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑖 → (1 / (2↑𝑛)) = (1 / (2↑𝑖)))
14		fveq2 5626	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑖 → (𝐹‘𝑛) = (𝐹‘𝑖))
15	13, 14	oveq12d 6018	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑖 → ((1 / (2↑𝑛)) · (𝐹‘𝑛)) = ((1 / (2↑𝑖)) · (𝐹‘𝑖)))
16		simpr 110	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → 𝑖 ∈ ℕ)
17		2rp 9850	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 ∈ ℝ⁺
18	17	a1i 9	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → 2 ∈ ℝ⁺)
19	16	nnzd 9564	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → 𝑖 ∈ ℤ)
20	18, 19	rpexpcld 10914	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → (2↑𝑖) ∈ ℝ⁺)
21	20	rpreccld 9899	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → (1 / (2↑𝑖)) ∈ ℝ⁺)
22	21	rpred 9888	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → (1 / (2↑𝑖)) ∈ ℝ)
23		0re 8142	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ∈ ℝ
24		1re 8141	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ ℝ
25		prssi 3825	. . . . . . . . . . . . . . . . . 18 ⊢ ((0 ∈ ℝ ∧ 1 ∈ ℝ) → {0, 1} ⊆ ℝ)
26	23, 24, 25	mp2an 426	. . . . . . . . . . . . . . . . 17 ⊢ {0, 1} ⊆ ℝ
27	3	ad3antrrr 492	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → 𝐹:ℕ⟶{0, 1})
28	27, 16	ffvelcdmd 5770	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → (𝐹‘𝑖) ∈ {0, 1})
29	26, 28	sselid 3222	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → (𝐹‘𝑖) ∈ ℝ)
30	22, 29	remulcld 8173	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) ∈ ℝ)
31	11, 15, 16, 30	fvmptd3 5727	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((1 / (2↑𝑛)) · (𝐹‘𝑛)))‘𝑖) = ((1 / (2↑𝑖)) · (𝐹‘𝑖)))
32	30	recnd 8171	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) ∈ ℂ)
33	3, 11	trilpolemclim 16363	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → seq1( + , (𝑛 ∈ ℕ ↦ ((1 / (2↑𝑛)) · (𝐹‘𝑛)))) ∈ dom ⇝ )
34	33	ad2antrr 488	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → seq1( + , (𝑛 ∈ ℕ ↦ ((1 / (2↑𝑛)) · (𝐹‘𝑛)))) ∈ dom ⇝ )
35	7, 8, 10, 31, 32, 34	isumsplit 11997	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹‘𝑖)) = (Σ𝑖 ∈ (1...((𝑥 + 1) − 1))((1 / (2↑𝑖)) · (𝐹‘𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖))))
36	9	nncnd 9120	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝑥 ∈ ℂ)
37		1cnd 8158	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 1 ∈ ℂ)
38	36, 37	pncand 8454	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → ((𝑥 + 1) − 1) = 𝑥)
39	38	oveq2d 6016	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (1...((𝑥 + 1) − 1)) = (1...𝑥))
40	9, 7	eleqtrdi 2322	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝑥 ∈ (ℤ_≥‘1))
41		fzisfzounsn 10437	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (ℤ_≥‘1) → (1...𝑥) = ((1..^𝑥) ∪ {𝑥}))
42	40, 41	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (1...𝑥) = ((1..^𝑥) ∪ {𝑥}))
43	39, 42	eqtrd 2262	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (1...((𝑥 + 1) − 1)) = ((1..^𝑥) ∪ {𝑥}))
44	43	sumeq1d 11872	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ (1...((𝑥 + 1) − 1))((1 / (2↑𝑖)) · (𝐹‘𝑖)) = Σ𝑖 ∈ ((1..^𝑥) ∪ {𝑥})((1 / (2↑𝑖)) · (𝐹‘𝑖)))
45		nfv 1574	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑖((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0)
46		nfcv 2372	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑖((1 / (2↑𝑥)) · (𝐹‘𝑥))
47		1zzd 9469	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 1 ∈ ℤ)
48	9	nnzd 9564	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝑥 ∈ ℤ)
49		fzofig 10649	. . . . . . . . . . . . . . . . 17 ⊢ ((1 ∈ ℤ ∧ 𝑥 ∈ ℤ) → (1..^𝑥) ∈ Fin)
50	47, 48, 49	syl2anc 411	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (1..^𝑥) ∈ Fin)
51		fzonel 10353	. . . . . . . . . . . . . . . . 17 ⊢ ¬ 𝑥 ∈ (1..^𝑥)
52	51	a1i 9	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → ¬ 𝑥 ∈ (1..^𝑥))
53	17	a1i 9	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → 2 ∈ ℝ⁺)
54		elfzoelz 10339	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 ∈ (1..^𝑥) → 𝑖 ∈ ℤ)
55	54	adantl 277	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → 𝑖 ∈ ℤ)
56	53, 55	rpexpcld 10914	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → (2↑𝑖) ∈ ℝ⁺)
57	56	rpreccld 9899	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → (1 / (2↑𝑖)) ∈ ℝ⁺)
58	57	rpred 9888	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → (1 / (2↑𝑖)) ∈ ℝ)
59		elfzouz 10343	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ (1..^𝑥) → 𝑖 ∈ (ℤ_≥‘1))
60	59, 7	eleqtrrdi 2323	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 ∈ (1..^𝑥) → 𝑖 ∈ ℕ)
61	60, 29	sylan2 286	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → (𝐹‘𝑖) ∈ ℝ)
62	58, 61	remulcld 8173	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) ∈ ℝ)
63	62	recnd 8171	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) ∈ ℂ)
64		oveq2 6008	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑥 → (2↑𝑖) = (2↑𝑥))
65	64	oveq2d 6016	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑥 → (1 / (2↑𝑖)) = (1 / (2↑𝑥)))
66		fveq2 5626	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑥 → (𝐹‘𝑖) = (𝐹‘𝑥))
67	65, 66	oveq12d 6018	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑥 → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) = ((1 / (2↑𝑥)) · (𝐹‘𝑥)))
68	17	a1i 9	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 2 ∈ ℝ⁺)
69	68, 48	rpexpcld 10914	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (2↑𝑥) ∈ ℝ⁺)
70	69	rpreccld 9899	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (1 / (2↑𝑥)) ∈ ℝ⁺)
71	70	rpred 9888	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (1 / (2↑𝑥)) ∈ ℝ)
72	3	ad2antrr 488	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝐹:ℕ⟶{0, 1})
73	72, 9	ffvelcdmd 5770	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (𝐹‘𝑥) ∈ {0, 1})
74	26, 73	sselid 3222	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (𝐹‘𝑥) ∈ ℝ)
75	71, 74	remulcld 8173	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → ((1 / (2↑𝑥)) · (𝐹‘𝑥)) ∈ ℝ)
76	75	recnd 8171	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → ((1 / (2↑𝑥)) · (𝐹‘𝑥)) ∈ ℂ)
77	45, 46, 50, 9, 52, 63, 67, 76	fsumsplitsn 11916	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ ((1..^𝑥) ∪ {𝑥})((1 / (2↑𝑖)) · (𝐹‘𝑖)) = (Σ𝑖 ∈ (1..^𝑥)((1 / (2↑𝑖)) · (𝐹‘𝑖)) + ((1 / (2↑𝑥)) · (𝐹‘𝑥))))
78		simpr 110	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (𝐹‘𝑥) = 0)
79	78	oveq2d 6016	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → ((1 / (2↑𝑥)) · (𝐹‘𝑥)) = ((1 / (2↑𝑥)) · 0))
80	70	rpcnd 9890	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (1 / (2↑𝑥)) ∈ ℂ)
81	80	mul01d 8535	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → ((1 / (2↑𝑥)) · 0) = 0)
82	79, 81	eqtrd 2262	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → ((1 / (2↑𝑥)) · (𝐹‘𝑥)) = 0)
83	82	oveq2d 6016	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (Σ𝑖 ∈ (1..^𝑥)((1 / (2↑𝑖)) · (𝐹‘𝑖)) + ((1 / (2↑𝑥)) · (𝐹‘𝑥))) = (Σ𝑖 ∈ (1..^𝑥)((1 / (2↑𝑖)) · (𝐹‘𝑖)) + 0))
84	44, 77, 83	3eqtrd 2266	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ (1...((𝑥 + 1) − 1))((1 / (2↑𝑖)) · (𝐹‘𝑖)) = (Σ𝑖 ∈ (1..^𝑥)((1 / (2↑𝑖)) · (𝐹‘𝑖)) + 0))
85	84	oveq1d 6015	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (Σ𝑖 ∈ (1...((𝑥 + 1) − 1))((1 / (2↑𝑖)) · (𝐹‘𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖))) = ((Σ𝑖 ∈ (1..^𝑥)((1 / (2↑𝑖)) · (𝐹‘𝑖)) + 0) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖))))
86	35, 85	eqtrd 2262	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹‘𝑖)) = ((Σ𝑖 ∈ (1..^𝑥)((1 / (2↑𝑖)) · (𝐹‘𝑖)) + 0) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖))))
87	50, 62	fsumrecl 11907	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ (1..^𝑥)((1 / (2↑𝑖)) · (𝐹‘𝑖)) ∈ ℝ)
88		0red 8143	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 0 ∈ ℝ)
89	87, 88	readdcld 8172	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (Σ𝑖 ∈ (1..^𝑥)((1 / (2↑𝑖)) · (𝐹‘𝑖)) + 0) ∈ ℝ)
90	10	nnzd 9564	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (𝑥 + 1) ∈ ℤ)
91		eluznn 9791	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 + 1) ∈ ℕ ∧ 𝑖 ∈ (ℤ_≥‘(𝑥 + 1))) → 𝑖 ∈ ℕ)
92	10, 91	sylan 283	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (ℤ_≥‘(𝑥 + 1))) → 𝑖 ∈ ℕ)
93	92, 30	syldan 282	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (ℤ_≥‘(𝑥 + 1))) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) ∈ ℝ)
94	11, 15, 92, 93	fvmptd3 5727	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (ℤ_≥‘(𝑥 + 1))) → ((𝑛 ∈ ℕ ↦ ((1 / (2↑𝑛)) · (𝐹‘𝑛)))‘𝑖) = ((1 / (2↑𝑖)) · (𝐹‘𝑖)))
95	31, 32	eqeltrd 2306	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((1 / (2↑𝑛)) · (𝐹‘𝑛)))‘𝑖) ∈ ℂ)
96	7, 10, 95	iserex 11845	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (seq1( + , (𝑛 ∈ ℕ ↦ ((1 / (2↑𝑛)) · (𝐹‘𝑛)))) ∈ dom ⇝ ↔ seq(𝑥 + 1)( + , (𝑛 ∈ ℕ ↦ ((1 / (2↑𝑛)) · (𝐹‘𝑛)))) ∈ dom ⇝ ))
97	34, 96	mpbid 147	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → seq(𝑥 + 1)( + , (𝑛 ∈ ℕ ↦ ((1 / (2↑𝑛)) · (𝐹‘𝑛)))) ∈ dom ⇝ )
98	8, 90, 94, 93, 97	isumrecl 11935	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖)) ∈ ℝ)
99	50, 58	fsumrecl 11907	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ (1..^𝑥)(1 / (2↑𝑖)) ∈ ℝ)
100	99, 71	readdcld 8172	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (Σ𝑖 ∈ (1..^𝑥)(1 / (2↑𝑖)) + (1 / (2↑𝑥))) ∈ ℝ)
101		eqid 2229	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ ↦ (1 / (2↑𝑛))) = (𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))
102	92, 21	syldan 282	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (ℤ_≥‘(𝑥 + 1))) → (1 / (2↑𝑖)) ∈ ℝ⁺)
103	101, 13, 92, 102	fvmptd3 5727	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (ℤ_≥‘(𝑥 + 1))) → ((𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))‘𝑖) = (1 / (2↑𝑖)))
104	92, 22	syldan 282	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (ℤ_≥‘(𝑥 + 1))) → (1 / (2↑𝑖)) ∈ ℝ)
105		seqex 10666	. . . . . . . . . . . . . . . . 17 ⊢ seq1( + , (𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))) ∈ V
106		ax-1cn 8088	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℂ
107	101	geo2lim 12022	. . . . . . . . . . . . . . . . . 18 ⊢ (1 ∈ ℂ → seq1( + , (𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))) ⇝ 1)
108	106, 107	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ seq1( + , (𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))) ⇝ 1
109		breldmg 4928	. . . . . . . . . . . . . . . . 17 ⊢ ((seq1( + , (𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))) ∈ V ∧ 1 ∈ ℂ ∧ seq1( + , (𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))) ⇝ 1) → seq1( + , (𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))) ∈ dom ⇝ )
110	105, 106, 108, 109	mp3an 1371	. . . . . . . . . . . . . . . 16 ⊢ seq1( + , (𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))) ∈ dom ⇝
111	110	a1i 9	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → seq1( + , (𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))) ∈ dom ⇝ )
112	101, 13, 16, 21	fvmptd3 5727	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))‘𝑖) = (1 / (2↑𝑖)))
113	21	rpcnd 9890	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → (1 / (2↑𝑖)) ∈ ℂ)
114	112, 113	eqeltrd 2306	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))‘𝑖) ∈ ℂ)
115	7, 10, 114	iserex 11845	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (seq1( + , (𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))) ∈ dom ⇝ ↔ seq(𝑥 + 1)( + , (𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))) ∈ dom ⇝ ))
116	111, 115	mpbid 147	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → seq(𝑥 + 1)( + , (𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))) ∈ dom ⇝ )
117	8, 90, 103, 104, 116	isumrecl 11935	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖)) ∈ ℝ)
118		simpr 110	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 0) → (𝐹‘𝑖) = 0)
119	118	oveq2d 6016	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 0) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) = ((1 / (2↑𝑖)) · 0))
120	57	adantr 276	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 0) → (1 / (2↑𝑖)) ∈ ℝ⁺)
121	120	rpcnd 9890	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 0) → (1 / (2↑𝑖)) ∈ ℂ)
122	121	mul01d 8535	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 0) → ((1 / (2↑𝑖)) · 0) = 0)
123	119, 122	eqtrd 2262	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 0) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) = 0)
124	120	rpge0d 9892	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 0) → 0 ≤ (1 / (2↑𝑖)))
125	123, 124	eqbrtrd 4104	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 0) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) ≤ (1 / (2↑𝑖)))
126		simpr 110	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 1) → (𝐹‘𝑖) = 1)
127	126	oveq2d 6016	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 1) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) = ((1 / (2↑𝑖)) · 1))
128	58	adantr 276	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 1) → (1 / (2↑𝑖)) ∈ ℝ)
129	128	recnd 8171	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 1) → (1 / (2↑𝑖)) ∈ ℂ)
130	129	mulridd 8159	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 1) → ((1 / (2↑𝑖)) · 1) = (1 / (2↑𝑖)))
131	127, 130	eqtrd 2262	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 1) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) = (1 / (2↑𝑖)))
132	128	leidd 8657	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 1) → (1 / (2↑𝑖)) ≤ (1 / (2↑𝑖)))
133	131, 132	eqbrtrd 4104	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 1) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) ≤ (1 / (2↑𝑖)))
134	72	adantr 276	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → 𝐹:ℕ⟶{0, 1})
135	60	adantl 277	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → 𝑖 ∈ ℕ)
136	134, 135	ffvelcdmd 5770	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → (𝐹‘𝑖) ∈ {0, 1})
137		elpri 3689	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑖) ∈ {0, 1} → ((𝐹‘𝑖) = 0 ∨ (𝐹‘𝑖) = 1))
138	136, 137	syl 14	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → ((𝐹‘𝑖) = 0 ∨ (𝐹‘𝑖) = 1))
139	125, 133, 138	mpjaodan 803	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) ≤ (1 / (2↑𝑖)))
140	50, 62, 58, 139	fsumle 11969	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ (1..^𝑥)((1 / (2↑𝑖)) · (𝐹‘𝑖)) ≤ Σ𝑖 ∈ (1..^𝑥)(1 / (2↑𝑖)))
141	70	rpgt0d 9891	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 0 < (1 / (2↑𝑥)))
142	87, 88, 99, 71, 140, 141	leltaddd 8709	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (Σ𝑖 ∈ (1..^𝑥)((1 / (2↑𝑖)) · (𝐹‘𝑖)) + 0) < (Σ𝑖 ∈ (1..^𝑥)(1 / (2↑𝑖)) + (1 / (2↑𝑥))))
143	72, 4, 8, 10	trilpolemisumle 16365	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖)) ≤ Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖)))
144	89, 98, 100, 117, 142, 143	ltleaddd 8708	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → ((Σ𝑖 ∈ (1..^𝑥)((1 / (2↑𝑖)) · (𝐹‘𝑖)) + 0) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖))) < ((Σ𝑖 ∈ (1..^𝑥)(1 / (2↑𝑖)) + (1 / (2↑𝑥))) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))))
145	86, 144	eqbrtrd 4104	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹‘𝑖)) < ((Σ𝑖 ∈ (1..^𝑥)(1 / (2↑𝑖)) + (1 / (2↑𝑥))) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))))
146	4, 145	eqbrtrid 4117	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝐴 < ((Σ𝑖 ∈ (1..^𝑥)(1 / (2↑𝑖)) + (1 / (2↑𝑥))) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))))
147		nfcv 2372	. . . . . . . . . . . 12 ⊢ Ⅎ𝑖(1 / (2↑𝑥))
148	57	rpcnd 9890	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → (1 / (2↑𝑖)) ∈ ℂ)
149	45, 147, 50, 9, 52, 148, 65, 80	fsumsplitsn 11916	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ ((1..^𝑥) ∪ {𝑥})(1 / (2↑𝑖)) = (Σ𝑖 ∈ (1..^𝑥)(1 / (2↑𝑖)) + (1 / (2↑𝑥))))
150	149	oveq1d 6015	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (Σ𝑖 ∈ ((1..^𝑥) ∪ {𝑥})(1 / (2↑𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))) = ((Σ𝑖 ∈ (1..^𝑥)(1 / (2↑𝑖)) + (1 / (2↑𝑥))) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))))
151	146, 150	breqtrrd 4110	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝐴 < (Σ𝑖 ∈ ((1..^𝑥) ∪ {𝑥})(1 / (2↑𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))))
152	42	sumeq1d 11872	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ (1...𝑥)(1 / (2↑𝑖)) = Σ𝑖 ∈ ((1..^𝑥) ∪ {𝑥})(1 / (2↑𝑖)))
153	152	oveq1d 6015	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (Σ𝑖 ∈ (1...𝑥)(1 / (2↑𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))) = (Σ𝑖 ∈ ((1..^𝑥) ∪ {𝑥})(1 / (2↑𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))))
154	151, 153	breqtrrd 4110	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝐴 < (Σ𝑖 ∈ (1...𝑥)(1 / (2↑𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))))
155	7, 8, 10, 112, 113, 111	isumsplit 11997	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ ℕ (1 / (2↑𝑖)) = (Σ𝑖 ∈ (1...((𝑥 + 1) − 1))(1 / (2↑𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))))
156	39	sumeq1d 11872	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ (1...((𝑥 + 1) − 1))(1 / (2↑𝑖)) = Σ𝑖 ∈ (1...𝑥)(1 / (2↑𝑖)))
157	156	oveq1d 6015	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (Σ𝑖 ∈ (1...((𝑥 + 1) − 1))(1 / (2↑𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))) = (Σ𝑖 ∈ (1...𝑥)(1 / (2↑𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))))
158	155, 157	eqtrd 2262	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ ℕ (1 / (2↑𝑖)) = (Σ𝑖 ∈ (1...𝑥)(1 / (2↑𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))))
159	154, 158	breqtrrd 4110	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝐴 < Σ𝑖 ∈ ℕ (1 / (2↑𝑖)))
160		geoihalfsum 12028	. . . . . . 7 ⊢ Σ𝑖 ∈ ℕ (1 / (2↑𝑖)) = 1
161	159, 160	breqtrdi 4123	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝐴 < 1)
162	6, 161	ltned 8256	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝐴 ≠ 1)
163	162	neneqd 2421	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → ¬ 𝐴 = 1)
164	2, 163	pm2.65da 665	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ¬ (𝐹‘𝑥) = 0)
165	3	ffvelcdmda 5769	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (𝐹‘𝑥) ∈ {0, 1})
166		elpri 3689	. . . . 5 ⊢ ((𝐹‘𝑥) ∈ {0, 1} → ((𝐹‘𝑥) = 0 ∨ (𝐹‘𝑥) = 1))
167	165, 166	syl 14	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝐹‘𝑥) = 0 ∨ (𝐹‘𝑥) = 1))
168	167	orcomd 734	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝐹‘𝑥) = 1 ∨ (𝐹‘𝑥) = 0))
169	164, 168	ecased 1383	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (𝐹‘𝑥) = 1)
170	169	ralrimiva 2603	1 ⊢ (𝜑 → ∀𝑥 ∈ ℕ (𝐹‘𝑥) = 1)

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ∨ wo 713 = wceq 1395 ∈ wcel 2200 ∀wral 2508 Vcvv 2799 ∪ cun 3195 ⊆ wss 3197 {csn 3666 {cpr 3667 class class class wbr 4082 ↦ cmpt 4144 dom cdm 4718 ⟶wf 5313 ‘cfv 5317 (class class class)co 6000 Fincfn 6885 ℂcc 7993 ℝcr 7994 0cc0 7995 1c1 7996 + caddc 7998 · cmul 8000 < clt 8177 ≤ cle 8178 − cmin 8313 / cdiv 8815 ℕcn 9106 2c2 9157 ℤcz 9442 ℤ_≥cuz 9718 ℝ⁺crp 9845 ...cfz 10200 ..^cfzo 10334 seqcseq 10664 ↑cexp 10755 ⇝ cli 11784 Σcsu 11859

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 617 ax-in2 618 ax-io 714 ax-5 1493 ax-7 1494 ax-gen 1495 ax-ie1 1539 ax-ie2 1540 ax-8 1550 ax-10 1551 ax-11 1552 ax-i12 1553 ax-bndl 1555 ax-4 1556 ax-17 1572 ax-i9 1576 ax-ial 1580 ax-i5r 1581 ax-13 2202 ax-14 2203 ax-ext 2211 ax-coll 4198 ax-sep 4201 ax-nul 4209 ax-pow 4257 ax-pr 4292 ax-un 4523 ax-setind 4628 ax-iinf 4679 ax-cnex 8086 ax-resscn 8087 ax-1cn 8088 ax-1re 8089 ax-icn 8090 ax-addcl 8091 ax-addrcl 8092 ax-mulcl 8093 ax-mulrcl 8094 ax-addcom 8095 ax-mulcom 8096 ax-addass 8097 ax-mulass 8098 ax-distr 8099 ax-i2m1 8100 ax-0lt1 8101 ax-1rid 8102 ax-0id 8103 ax-rnegex 8104 ax-precex 8105 ax-cnre 8106 ax-pre-ltirr 8107 ax-pre-ltwlin 8108 ax-pre-lttrn 8109 ax-pre-apti 8110 ax-pre-ltadd 8111 ax-pre-mulgt0 8112 ax-pre-mulext 8113 ax-arch 8114 ax-caucvg 8115

This theorem depends on definitions: df-bi 117 df-dc 840 df-3or 1003 df-3an 1004 df-tru 1398 df-fal 1401 df-nf 1507 df-sb 1809 df-eu 2080 df-mo 2081 df-clab 2216 df-cleq 2222 df-clel 2225 df-nfc 2361 df-ne 2401 df-nel 2496 df-ral 2513 df-rex 2514 df-reu 2515 df-rmo 2516 df-rab 2517 df-v 2801 df-sbc 3029 df-csb 3125 df-dif 3199 df-un 3201 df-in 3203 df-ss 3210 df-nul 3492 df-if 3603 df-pw 3651 df-sn 3672 df-pr 3673 df-op 3675 df-uni 3888 df-int 3923 df-iun 3966 df-br 4083 df-opab 4145 df-mpt 4146 df-tr 4182 df-id 4383 df-po 4386 df-iso 4387 df-iord 4456 df-on 4458 df-ilim 4459 df-suc 4461 df-iom 4682 df-xp 4724 df-rel 4725 df-cnv 4726 df-co 4727 df-dm 4728 df-rn 4729 df-res 4730 df-ima 4731 df-iota 5277 df-fun 5319 df-fn 5320 df-f 5321 df-f1 5322 df-fo 5323 df-f1o 5324 df-fv 5325 df-isom 5326 df-riota 5953 df-ov 6003 df-oprab 6004 df-mpo 6005 df-1st 6284 df-2nd 6285 df-recs 6449 df-irdg 6514 df-frec 6535 df-1o 6560 df-oadd 6564 df-er 6678 df-en 6886 df-dom 6887 df-fin 6888 df-pnf 8179 df-mnf 8180 df-xr 8181 df-ltxr 8182 df-le 8183 df-sub 8315 df-neg 8316 df-reap 8718 df-ap 8725 df-div 8816 df-inn 9107 df-2 9165 df-3 9166 df-4 9167 df-n0 9366 df-z 9443 df-uz 9719 df-q 9811 df-rp 9846 df-ico 10086 df-fz 10201 df-fzo 10335 df-seqfrec 10665 df-exp 10756 df-ihash 10993 df-cj 11348 df-re 11349 df-im 11350 df-rsqrt 11504 df-abs 11505 df-clim 11785 df-sumdc 11860

This theorem is referenced by: trilpolemres 16369 redcwlpolemeq1 16381

W3C validator