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 15771

Description: Lemma for trilpo 15774. 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 15768	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℝ)
6	5	ad2antrr 488	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝐴 ∈ ℝ)
7		nnuz 9654	. . . . . . . . . . . . . 14 ⊢ ℕ = (ℤ_≥‘1)
8		eqid 2196	. . . . . . . . . . . . . 14 ⊢ (ℤ_≥‘(𝑥 + 1)) = (ℤ_≥‘(𝑥 + 1))
9		simplr 528	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝑥 ∈ ℕ)
10	9	peano2nnd 9022	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (𝑥 + 1) ∈ ℕ)
11		eqid 2196	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ ↦ ((1 / (2↑𝑛)) · (𝐹‘𝑛))) = (𝑛 ∈ ℕ ↦ ((1 / (2↑𝑛)) · (𝐹‘𝑛)))
12		oveq2 5933	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑖 → (2↑𝑛) = (2↑𝑖))
13	12	oveq2d 5941	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑖 → (1 / (2↑𝑛)) = (1 / (2↑𝑖)))
14		fveq2 5561	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑖 → (𝐹‘𝑛) = (𝐹‘𝑖))
15	13, 14	oveq12d 5943	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑖 → ((1 / (2↑𝑛)) · (𝐹‘𝑛)) = ((1 / (2↑𝑖)) · (𝐹‘𝑖)))
16		simpr 110	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → 𝑖 ∈ ℕ)
17		2rp 9750	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 ∈ ℝ⁺
18	17	a1i 9	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → 2 ∈ ℝ⁺)
19	16	nnzd 9464	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → 𝑖 ∈ ℤ)
20	18, 19	rpexpcld 10806	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → (2↑𝑖) ∈ ℝ⁺)
21	20	rpreccld 9799	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → (1 / (2↑𝑖)) ∈ ℝ⁺)
22	21	rpred 9788	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → (1 / (2↑𝑖)) ∈ ℝ)
23		0re 8043	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ∈ ℝ
24		1re 8042	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ ℝ
25		prssi 3781	. . . . . . . . . . . . . . . . . 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 5701	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → (𝐹‘𝑖) ∈ {0, 1})
29	26, 28	sselid 3182	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → (𝐹‘𝑖) ∈ ℝ)
30	22, 29	remulcld 8074	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) ∈ ℝ)
31	11, 15, 16, 30	fvmptd3 5658	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((1 / (2↑𝑛)) · (𝐹‘𝑛)))‘𝑖) = ((1 / (2↑𝑖)) · (𝐹‘𝑖)))
32	30	recnd 8072	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) ∈ ℂ)
33	3, 11	trilpolemclim 15767	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → seq1( + , (𝑛 ∈ ℕ ↦ ((1 / (2↑𝑛)) · (𝐹‘𝑛)))) ∈ dom ⇝ )
34	33	ad2antrr 488	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → seq1( + , (𝑛 ∈ ℕ ↦ ((1 / (2↑𝑛)) · (𝐹‘𝑛)))) ∈ dom ⇝ )
35	7, 8, 10, 31, 32, 34	isumsplit 11673	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹‘𝑖)) = (Σ𝑖 ∈ (1...((𝑥 + 1) − 1))((1 / (2↑𝑖)) · (𝐹‘𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖))))
36	9	nncnd 9021	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝑥 ∈ ℂ)
37		1cnd 8059	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 1 ∈ ℂ)
38	36, 37	pncand 8355	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → ((𝑥 + 1) − 1) = 𝑥)
39	38	oveq2d 5941	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (1...((𝑥 + 1) − 1)) = (1...𝑥))
40	9, 7	eleqtrdi 2289	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝑥 ∈ (ℤ_≥‘1))
41		fzisfzounsn 10329	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (ℤ_≥‘1) → (1...𝑥) = ((1..^𝑥) ∪ {𝑥}))
42	40, 41	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (1...𝑥) = ((1..^𝑥) ∪ {𝑥}))
43	39, 42	eqtrd 2229	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (1...((𝑥 + 1) − 1)) = ((1..^𝑥) ∪ {𝑥}))
44	43	sumeq1d 11548	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ (1...((𝑥 + 1) − 1))((1 / (2↑𝑖)) · (𝐹‘𝑖)) = Σ𝑖 ∈ ((1..^𝑥) ∪ {𝑥})((1 / (2↑𝑖)) · (𝐹‘𝑖)))
45		nfv 1542	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑖((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0)
46		nfcv 2339	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑖((1 / (2↑𝑥)) · (𝐹‘𝑥))
47		1zzd 9370	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 1 ∈ ℤ)
48	9	nnzd 9464	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝑥 ∈ ℤ)
49		fzofig 10541	. . . . . . . . . . . . . . . . 17 ⊢ ((1 ∈ ℤ ∧ 𝑥 ∈ ℤ) → (1..^𝑥) ∈ Fin)
50	47, 48, 49	syl2anc 411	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (1..^𝑥) ∈ Fin)
51		fzonel 10253	. . . . . . . . . . . . . . . . 17 ⊢ ¬ 𝑥 ∈ (1..^𝑥)
52	51	a1i 9	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → ¬ 𝑥 ∈ (1..^𝑥))
53	17	a1i 9	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → 2 ∈ ℝ⁺)
54		elfzoelz 10239	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 ∈ (1..^𝑥) → 𝑖 ∈ ℤ)
55	54	adantl 277	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → 𝑖 ∈ ℤ)
56	53, 55	rpexpcld 10806	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → (2↑𝑖) ∈ ℝ⁺)
57	56	rpreccld 9799	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → (1 / (2↑𝑖)) ∈ ℝ⁺)
58	57	rpred 9788	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → (1 / (2↑𝑖)) ∈ ℝ)
59		elfzouz 10243	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ (1..^𝑥) → 𝑖 ∈ (ℤ_≥‘1))
60	59, 7	eleqtrrdi 2290	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 ∈ (1..^𝑥) → 𝑖 ∈ ℕ)
61	60, 29	sylan2 286	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → (𝐹‘𝑖) ∈ ℝ)
62	58, 61	remulcld 8074	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) ∈ ℝ)
63	62	recnd 8072	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) ∈ ℂ)
64		oveq2 5933	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑥 → (2↑𝑖) = (2↑𝑥))
65	64	oveq2d 5941	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑥 → (1 / (2↑𝑖)) = (1 / (2↑𝑥)))
66		fveq2 5561	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑥 → (𝐹‘𝑖) = (𝐹‘𝑥))
67	65, 66	oveq12d 5943	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑥 → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) = ((1 / (2↑𝑥)) · (𝐹‘𝑥)))
68	17	a1i 9	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 2 ∈ ℝ⁺)
69	68, 48	rpexpcld 10806	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (2↑𝑥) ∈ ℝ⁺)
70	69	rpreccld 9799	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (1 / (2↑𝑥)) ∈ ℝ⁺)
71	70	rpred 9788	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (1 / (2↑𝑥)) ∈ ℝ)
72	3	ad2antrr 488	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝐹:ℕ⟶{0, 1})
73	72, 9	ffvelcdmd 5701	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (𝐹‘𝑥) ∈ {0, 1})
74	26, 73	sselid 3182	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (𝐹‘𝑥) ∈ ℝ)
75	71, 74	remulcld 8074	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → ((1 / (2↑𝑥)) · (𝐹‘𝑥)) ∈ ℝ)
76	75	recnd 8072	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → ((1 / (2↑𝑥)) · (𝐹‘𝑥)) ∈ ℂ)
77	45, 46, 50, 9, 52, 63, 67, 76	fsumsplitsn 11592	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ ((1..^𝑥) ∪ {𝑥})((1 / (2↑𝑖)) · (𝐹‘𝑖)) = (Σ𝑖 ∈ (1..^𝑥)((1 / (2↑𝑖)) · (𝐹‘𝑖)) + ((1 / (2↑𝑥)) · (𝐹‘𝑥))))
78		simpr 110	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (𝐹‘𝑥) = 0)
79	78	oveq2d 5941	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → ((1 / (2↑𝑥)) · (𝐹‘𝑥)) = ((1 / (2↑𝑥)) · 0))
80	70	rpcnd 9790	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (1 / (2↑𝑥)) ∈ ℂ)
81	80	mul01d 8436	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → ((1 / (2↑𝑥)) · 0) = 0)
82	79, 81	eqtrd 2229	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → ((1 / (2↑𝑥)) · (𝐹‘𝑥)) = 0)
83	82	oveq2d 5941	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (Σ𝑖 ∈ (1..^𝑥)((1 / (2↑𝑖)) · (𝐹‘𝑖)) + ((1 / (2↑𝑥)) · (𝐹‘𝑥))) = (Σ𝑖 ∈ (1..^𝑥)((1 / (2↑𝑖)) · (𝐹‘𝑖)) + 0))
84	44, 77, 83	3eqtrd 2233	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ (1...((𝑥 + 1) − 1))((1 / (2↑𝑖)) · (𝐹‘𝑖)) = (Σ𝑖 ∈ (1..^𝑥)((1 / (2↑𝑖)) · (𝐹‘𝑖)) + 0))
85	84	oveq1d 5940	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (Σ𝑖 ∈ (1...((𝑥 + 1) − 1))((1 / (2↑𝑖)) · (𝐹‘𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖))) = ((Σ𝑖 ∈ (1..^𝑥)((1 / (2↑𝑖)) · (𝐹‘𝑖)) + 0) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖))))
86	35, 85	eqtrd 2229	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹‘𝑖)) = ((Σ𝑖 ∈ (1..^𝑥)((1 / (2↑𝑖)) · (𝐹‘𝑖)) + 0) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖))))
87	50, 62	fsumrecl 11583	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ (1..^𝑥)((1 / (2↑𝑖)) · (𝐹‘𝑖)) ∈ ℝ)
88		0red 8044	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 0 ∈ ℝ)
89	87, 88	readdcld 8073	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (Σ𝑖 ∈ (1..^𝑥)((1 / (2↑𝑖)) · (𝐹‘𝑖)) + 0) ∈ ℝ)
90	10	nnzd 9464	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (𝑥 + 1) ∈ ℤ)
91		eluznn 9691	. . . . . . . . . . . . . . . 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 5658	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (ℤ_≥‘(𝑥 + 1))) → ((𝑛 ∈ ℕ ↦ ((1 / (2↑𝑛)) · (𝐹‘𝑛)))‘𝑖) = ((1 / (2↑𝑖)) · (𝐹‘𝑖)))
95	31, 32	eqeltrd 2273	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((1 / (2↑𝑛)) · (𝐹‘𝑛)))‘𝑖) ∈ ℂ)
96	7, 10, 95	iserex 11521	. . . . . . . . . . . . . . 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 11611	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖)) ∈ ℝ)
99	50, 58	fsumrecl 11583	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ (1..^𝑥)(1 / (2↑𝑖)) ∈ ℝ)
100	99, 71	readdcld 8073	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (Σ𝑖 ∈ (1..^𝑥)(1 / (2↑𝑖)) + (1 / (2↑𝑥))) ∈ ℝ)
101		eqid 2196	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ ↦ (1 / (2↑𝑛))) = (𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))
102	92, 21	syldan 282	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (ℤ_≥‘(𝑥 + 1))) → (1 / (2↑𝑖)) ∈ ℝ⁺)
103	101, 13, 92, 102	fvmptd3 5658	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (ℤ_≥‘(𝑥 + 1))) → ((𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))‘𝑖) = (1 / (2↑𝑖)))
104	92, 22	syldan 282	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (ℤ_≥‘(𝑥 + 1))) → (1 / (2↑𝑖)) ∈ ℝ)
105		seqex 10558	. . . . . . . . . . . . . . . . 17 ⊢ seq1( + , (𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))) ∈ V
106		ax-1cn 7989	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℂ
107	101	geo2lim 11698	. . . . . . . . . . . . . . . . . 18 ⊢ (1 ∈ ℂ → seq1( + , (𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))) ⇝ 1)
108	106, 107	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ seq1( + , (𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))) ⇝ 1
109		breldmg 4873	. . . . . . . . . . . . . . . . 17 ⊢ ((seq1( + , (𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))) ∈ V ∧ 1 ∈ ℂ ∧ seq1( + , (𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))) ⇝ 1) → seq1( + , (𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))) ∈ dom ⇝ )
110	105, 106, 108, 109	mp3an 1348	. . . . . . . . . . . . . . . 16 ⊢ seq1( + , (𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))) ∈ dom ⇝
111	110	a1i 9	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → seq1( + , (𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))) ∈ dom ⇝ )
112	101, 13, 16, 21	fvmptd3 5658	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))‘𝑖) = (1 / (2↑𝑖)))
113	21	rpcnd 9790	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → (1 / (2↑𝑖)) ∈ ℂ)
114	112, 113	eqeltrd 2273	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))‘𝑖) ∈ ℂ)
115	7, 10, 114	iserex 11521	. . . . . . . . . . . . . . 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 11611	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖)) ∈ ℝ)
118		simpr 110	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 0) → (𝐹‘𝑖) = 0)
119	118	oveq2d 5941	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 0) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) = ((1 / (2↑𝑖)) · 0))
120	57	adantr 276	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 0) → (1 / (2↑𝑖)) ∈ ℝ⁺)
121	120	rpcnd 9790	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 0) → (1 / (2↑𝑖)) ∈ ℂ)
122	121	mul01d 8436	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 0) → ((1 / (2↑𝑖)) · 0) = 0)
123	119, 122	eqtrd 2229	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 0) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) = 0)
124	120	rpge0d 9792	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 0) → 0 ≤ (1 / (2↑𝑖)))
125	123, 124	eqbrtrd 4056	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 0) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) ≤ (1 / (2↑𝑖)))
126		simpr 110	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 1) → (𝐹‘𝑖) = 1)
127	126	oveq2d 5941	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 1) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) = ((1 / (2↑𝑖)) · 1))
128	58	adantr 276	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 1) → (1 / (2↑𝑖)) ∈ ℝ)
129	128	recnd 8072	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 1) → (1 / (2↑𝑖)) ∈ ℂ)
130	129	mulridd 8060	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 1) → ((1 / (2↑𝑖)) · 1) = (1 / (2↑𝑖)))
131	127, 130	eqtrd 2229	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 1) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) = (1 / (2↑𝑖)))
132	128	leidd 8558	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 1) → (1 / (2↑𝑖)) ≤ (1 / (2↑𝑖)))
133	131, 132	eqbrtrd 4056	. . . . . . . . . . . . . . . 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 5701	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → (𝐹‘𝑖) ∈ {0, 1})
137		elpri 3646	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑖) ∈ {0, 1} → ((𝐹‘𝑖) = 0 ∨ (𝐹‘𝑖) = 1))
138	136, 137	syl 14	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → ((𝐹‘𝑖) = 0 ∨ (𝐹‘𝑖) = 1))
139	125, 133, 138	mpjaodan 799	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) ≤ (1 / (2↑𝑖)))
140	50, 62, 58, 139	fsumle 11645	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ (1..^𝑥)((1 / (2↑𝑖)) · (𝐹‘𝑖)) ≤ Σ𝑖 ∈ (1..^𝑥)(1 / (2↑𝑖)))
141	70	rpgt0d 9791	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 0 < (1 / (2↑𝑥)))
142	87, 88, 99, 71, 140, 141	leltaddd 8610	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (Σ𝑖 ∈ (1..^𝑥)((1 / (2↑𝑖)) · (𝐹‘𝑖)) + 0) < (Σ𝑖 ∈ (1..^𝑥)(1 / (2↑𝑖)) + (1 / (2↑𝑥))))
143	72, 4, 8, 10	trilpolemisumle 15769	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖)) ≤ Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖)))
144	89, 98, 100, 117, 142, 143	ltleaddd 8609	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → ((Σ𝑖 ∈ (1..^𝑥)((1 / (2↑𝑖)) · (𝐹‘𝑖)) + 0) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖))) < ((Σ𝑖 ∈ (1..^𝑥)(1 / (2↑𝑖)) + (1 / (2↑𝑥))) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))))
145	86, 144	eqbrtrd 4056	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹‘𝑖)) < ((Σ𝑖 ∈ (1..^𝑥)(1 / (2↑𝑖)) + (1 / (2↑𝑥))) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))))
146	4, 145	eqbrtrid 4069	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝐴 < ((Σ𝑖 ∈ (1..^𝑥)(1 / (2↑𝑖)) + (1 / (2↑𝑥))) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))))
147		nfcv 2339	. . . . . . . . . . . 12 ⊢ Ⅎ𝑖(1 / (2↑𝑥))
148	57	rpcnd 9790	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → (1 / (2↑𝑖)) ∈ ℂ)
149	45, 147, 50, 9, 52, 148, 65, 80	fsumsplitsn 11592	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ ((1..^𝑥) ∪ {𝑥})(1 / (2↑𝑖)) = (Σ𝑖 ∈ (1..^𝑥)(1 / (2↑𝑖)) + (1 / (2↑𝑥))))
150	149	oveq1d 5940	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (Σ𝑖 ∈ ((1..^𝑥) ∪ {𝑥})(1 / (2↑𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))) = ((Σ𝑖 ∈ (1..^𝑥)(1 / (2↑𝑖)) + (1 / (2↑𝑥))) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))))
151	146, 150	breqtrrd 4062	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝐴 < (Σ𝑖 ∈ ((1..^𝑥) ∪ {𝑥})(1 / (2↑𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))))
152	42	sumeq1d 11548	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ (1...𝑥)(1 / (2↑𝑖)) = Σ𝑖 ∈ ((1..^𝑥) ∪ {𝑥})(1 / (2↑𝑖)))
153	152	oveq1d 5940	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (Σ𝑖 ∈ (1...𝑥)(1 / (2↑𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))) = (Σ𝑖 ∈ ((1..^𝑥) ∪ {𝑥})(1 / (2↑𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))))
154	151, 153	breqtrrd 4062	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝐴 < (Σ𝑖 ∈ (1...𝑥)(1 / (2↑𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))))
155	7, 8, 10, 112, 113, 111	isumsplit 11673	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ ℕ (1 / (2↑𝑖)) = (Σ𝑖 ∈ (1...((𝑥 + 1) − 1))(1 / (2↑𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))))
156	39	sumeq1d 11548	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ (1...((𝑥 + 1) − 1))(1 / (2↑𝑖)) = Σ𝑖 ∈ (1...𝑥)(1 / (2↑𝑖)))
157	156	oveq1d 5940	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (Σ𝑖 ∈ (1...((𝑥 + 1) − 1))(1 / (2↑𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))) = (Σ𝑖 ∈ (1...𝑥)(1 / (2↑𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))))
158	155, 157	eqtrd 2229	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ ℕ (1 / (2↑𝑖)) = (Σ𝑖 ∈ (1...𝑥)(1 / (2↑𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))))
159	154, 158	breqtrrd 4062	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝐴 < Σ𝑖 ∈ ℕ (1 / (2↑𝑖)))
160		geoihalfsum 11704	. . . . . . 7 ⊢ Σ𝑖 ∈ ℕ (1 / (2↑𝑖)) = 1
161	159, 160	breqtrdi 4075	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝐴 < 1)
162	6, 161	ltned 8157	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝐴 ≠ 1)
163	162	neneqd 2388	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → ¬ 𝐴 = 1)
164	2, 163	pm2.65da 662	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ¬ (𝐹‘𝑥) = 0)
165	3	ffvelcdmda 5700	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (𝐹‘𝑥) ∈ {0, 1})
166		elpri 3646	. . . . 5 ⊢ ((𝐹‘𝑥) ∈ {0, 1} → ((𝐹‘𝑥) = 0 ∨ (𝐹‘𝑥) = 1))
167	165, 166	syl 14	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝐹‘𝑥) = 0 ∨ (𝐹‘𝑥) = 1))
168	167	orcomd 730	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝐹‘𝑥) = 1 ∨ (𝐹‘𝑥) = 0))
169	164, 168	ecased 1360	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (𝐹‘𝑥) = 1)
170	169	ralrimiva 2570	1 ⊢ (𝜑 → ∀𝑥 ∈ ℕ (𝐹‘𝑥) = 1)

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ∨ wo 709 = wceq 1364 ∈ wcel 2167 ∀wral 2475 Vcvv 2763 ∪ cun 3155 ⊆ wss 3157 {csn 3623 {cpr 3624 class class class wbr 4034 ↦ cmpt 4095 dom cdm 4664 ⟶wf 5255 ‘cfv 5259 (class class class)co 5925 Fincfn 6808 ℂcc 7894 ℝcr 7895 0cc0 7896 1c1 7897 + caddc 7899 · cmul 7901 < clt 8078 ≤ cle 8079 − cmin 8214 / cdiv 8716 ℕcn 9007 2c2 9058 ℤcz 9343 ℤ_≥cuz 9618 ℝ⁺crp 9745 ...cfz 10100 ..^cfzo 10234 seqcseq 10556 ↑cexp 10647 ⇝ cli 11460 Σcsu 11535

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 4149 ax-sep 4152 ax-nul 4160 ax-pow 4208 ax-pr 4243 ax-un 4469 ax-setind 4574 ax-iinf 4625 ax-cnex 7987 ax-resscn 7988 ax-1cn 7989 ax-1re 7990 ax-icn 7991 ax-addcl 7992 ax-addrcl 7993 ax-mulcl 7994 ax-mulrcl 7995 ax-addcom 7996 ax-mulcom 7997 ax-addass 7998 ax-mulass 7999 ax-distr 8000 ax-i2m1 8001 ax-0lt1 8002 ax-1rid 8003 ax-0id 8004 ax-rnegex 8005 ax-precex 8006 ax-cnre 8007 ax-pre-ltirr 8008 ax-pre-ltwlin 8009 ax-pre-lttrn 8010 ax-pre-apti 8011 ax-pre-ltadd 8012 ax-pre-mulgt0 8013 ax-pre-mulext 8014 ax-arch 8015 ax-caucvg 8016

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 3452 df-if 3563 df-pw 3608 df-sn 3629 df-pr 3630 df-op 3632 df-uni 3841 df-int 3876 df-iun 3919 df-br 4035 df-opab 4096 df-mpt 4097 df-tr 4133 df-id 4329 df-po 4332 df-iso 4333 df-iord 4402 df-on 4404 df-ilim 4405 df-suc 4407 df-iom 4628 df-xp 4670 df-rel 4671 df-cnv 4672 df-co 4673 df-dm 4674 df-rn 4675 df-res 4676 df-ima 4677 df-iota 5220 df-fun 5261 df-fn 5262 df-f 5263 df-f1 5264 df-fo 5265 df-f1o 5266 df-fv 5267 df-isom 5268 df-riota 5880 df-ov 5928 df-oprab 5929 df-mpo 5930 df-1st 6207 df-2nd 6208 df-recs 6372 df-irdg 6437 df-frec 6458 df-1o 6483 df-oadd 6487 df-er 6601 df-en 6809 df-dom 6810 df-fin 6811 df-pnf 8080 df-mnf 8081 df-xr 8082 df-ltxr 8083 df-le 8084 df-sub 8216 df-neg 8217 df-reap 8619 df-ap 8626 df-div 8717 df-inn 9008 df-2 9066 df-3 9067 df-4 9068 df-n0 9267 df-z 9344 df-uz 9619 df-q 9711 df-rp 9746 df-ico 9986 df-fz 10101 df-fzo 10235 df-seqfrec 10557 df-exp 10648 df-ihash 10885 df-cj 11024 df-re 11025 df-im 11026 df-rsqrt 11180 df-abs 11181 df-clim 11461 df-sumdc 11536

This theorem is referenced by: trilpolemres 15773 redcwlpolemeq1 15785

W3C validator