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 15843

Description: Lemma for trilpo 15846. 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 15840	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℝ)
6	5	ad2antrr 488	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝐴 ∈ ℝ)
7		nnuz 9666	. . . . . . . . . . . . . 14 ⊢ ℕ = (ℤ_≥‘1)
8		eqid 2204	. . . . . . . . . . . . . 14 ⊢ (ℤ_≥‘(𝑥 + 1)) = (ℤ_≥‘(𝑥 + 1))
9		simplr 528	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝑥 ∈ ℕ)
10	9	peano2nnd 9033	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (𝑥 + 1) ∈ ℕ)
11		eqid 2204	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ ↦ ((1 / (2↑𝑛)) · (𝐹‘𝑛))) = (𝑛 ∈ ℕ ↦ ((1 / (2↑𝑛)) · (𝐹‘𝑛)))
12		oveq2 5942	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑖 → (2↑𝑛) = (2↑𝑖))
13	12	oveq2d 5950	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑖 → (1 / (2↑𝑛)) = (1 / (2↑𝑖)))
14		fveq2 5570	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑖 → (𝐹‘𝑛) = (𝐹‘𝑖))
15	13, 14	oveq12d 5952	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑖 → ((1 / (2↑𝑛)) · (𝐹‘𝑛)) = ((1 / (2↑𝑖)) · (𝐹‘𝑖)))
16		simpr 110	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → 𝑖 ∈ ℕ)
17		2rp 9762	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 ∈ ℝ⁺
18	17	a1i 9	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → 2 ∈ ℝ⁺)
19	16	nnzd 9476	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → 𝑖 ∈ ℤ)
20	18, 19	rpexpcld 10823	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → (2↑𝑖) ∈ ℝ⁺)
21	20	rpreccld 9811	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → (1 / (2↑𝑖)) ∈ ℝ⁺)
22	21	rpred 9800	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → (1 / (2↑𝑖)) ∈ ℝ)
23		0re 8054	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ∈ ℝ
24		1re 8053	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ ℝ
25		prssi 3790	. . . . . . . . . . . . . . . . . 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 5710	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → (𝐹‘𝑖) ∈ {0, 1})
29	26, 28	sselid 3190	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → (𝐹‘𝑖) ∈ ℝ)
30	22, 29	remulcld 8085	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) ∈ ℝ)
31	11, 15, 16, 30	fvmptd3 5667	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((1 / (2↑𝑛)) · (𝐹‘𝑛)))‘𝑖) = ((1 / (2↑𝑖)) · (𝐹‘𝑖)))
32	30	recnd 8083	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) ∈ ℂ)
33	3, 11	trilpolemclim 15839	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → seq1( + , (𝑛 ∈ ℕ ↦ ((1 / (2↑𝑛)) · (𝐹‘𝑛)))) ∈ dom ⇝ )
34	33	ad2antrr 488	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → seq1( + , (𝑛 ∈ ℕ ↦ ((1 / (2↑𝑛)) · (𝐹‘𝑛)))) ∈ dom ⇝ )
35	7, 8, 10, 31, 32, 34	isumsplit 11721	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹‘𝑖)) = (Σ𝑖 ∈ (1...((𝑥 + 1) − 1))((1 / (2↑𝑖)) · (𝐹‘𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖))))
36	9	nncnd 9032	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝑥 ∈ ℂ)
37		1cnd 8070	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 1 ∈ ℂ)
38	36, 37	pncand 8366	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → ((𝑥 + 1) − 1) = 𝑥)
39	38	oveq2d 5950	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (1...((𝑥 + 1) − 1)) = (1...𝑥))
40	9, 7	eleqtrdi 2297	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝑥 ∈ (ℤ_≥‘1))
41		fzisfzounsn 10346	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (ℤ_≥‘1) → (1...𝑥) = ((1..^𝑥) ∪ {𝑥}))
42	40, 41	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (1...𝑥) = ((1..^𝑥) ∪ {𝑥}))
43	39, 42	eqtrd 2237	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (1...((𝑥 + 1) − 1)) = ((1..^𝑥) ∪ {𝑥}))
44	43	sumeq1d 11596	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ (1...((𝑥 + 1) − 1))((1 / (2↑𝑖)) · (𝐹‘𝑖)) = Σ𝑖 ∈ ((1..^𝑥) ∪ {𝑥})((1 / (2↑𝑖)) · (𝐹‘𝑖)))
45		nfv 1550	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑖((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0)
46		nfcv 2347	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑖((1 / (2↑𝑥)) · (𝐹‘𝑥))
47		1zzd 9381	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 1 ∈ ℤ)
48	9	nnzd 9476	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝑥 ∈ ℤ)
49		fzofig 10558	. . . . . . . . . . . . . . . . 17 ⊢ ((1 ∈ ℤ ∧ 𝑥 ∈ ℤ) → (1..^𝑥) ∈ Fin)
50	47, 48, 49	syl2anc 411	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (1..^𝑥) ∈ Fin)
51		fzonel 10265	. . . . . . . . . . . . . . . . 17 ⊢ ¬ 𝑥 ∈ (1..^𝑥)
52	51	a1i 9	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → ¬ 𝑥 ∈ (1..^𝑥))
53	17	a1i 9	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → 2 ∈ ℝ⁺)
54		elfzoelz 10251	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 ∈ (1..^𝑥) → 𝑖 ∈ ℤ)
55	54	adantl 277	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → 𝑖 ∈ ℤ)
56	53, 55	rpexpcld 10823	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → (2↑𝑖) ∈ ℝ⁺)
57	56	rpreccld 9811	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → (1 / (2↑𝑖)) ∈ ℝ⁺)
58	57	rpred 9800	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → (1 / (2↑𝑖)) ∈ ℝ)
59		elfzouz 10255	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ (1..^𝑥) → 𝑖 ∈ (ℤ_≥‘1))
60	59, 7	eleqtrrdi 2298	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 ∈ (1..^𝑥) → 𝑖 ∈ ℕ)
61	60, 29	sylan2 286	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → (𝐹‘𝑖) ∈ ℝ)
62	58, 61	remulcld 8085	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) ∈ ℝ)
63	62	recnd 8083	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) ∈ ℂ)
64		oveq2 5942	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑥 → (2↑𝑖) = (2↑𝑥))
65	64	oveq2d 5950	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑥 → (1 / (2↑𝑖)) = (1 / (2↑𝑥)))
66		fveq2 5570	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑥 → (𝐹‘𝑖) = (𝐹‘𝑥))
67	65, 66	oveq12d 5952	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑥 → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) = ((1 / (2↑𝑥)) · (𝐹‘𝑥)))
68	17	a1i 9	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 2 ∈ ℝ⁺)
69	68, 48	rpexpcld 10823	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (2↑𝑥) ∈ ℝ⁺)
70	69	rpreccld 9811	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (1 / (2↑𝑥)) ∈ ℝ⁺)
71	70	rpred 9800	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (1 / (2↑𝑥)) ∈ ℝ)
72	3	ad2antrr 488	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝐹:ℕ⟶{0, 1})
73	72, 9	ffvelcdmd 5710	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (𝐹‘𝑥) ∈ {0, 1})
74	26, 73	sselid 3190	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (𝐹‘𝑥) ∈ ℝ)
75	71, 74	remulcld 8085	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → ((1 / (2↑𝑥)) · (𝐹‘𝑥)) ∈ ℝ)
76	75	recnd 8083	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → ((1 / (2↑𝑥)) · (𝐹‘𝑥)) ∈ ℂ)
77	45, 46, 50, 9, 52, 63, 67, 76	fsumsplitsn 11640	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ ((1..^𝑥) ∪ {𝑥})((1 / (2↑𝑖)) · (𝐹‘𝑖)) = (Σ𝑖 ∈ (1..^𝑥)((1 / (2↑𝑖)) · (𝐹‘𝑖)) + ((1 / (2↑𝑥)) · (𝐹‘𝑥))))
78		simpr 110	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (𝐹‘𝑥) = 0)
79	78	oveq2d 5950	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → ((1 / (2↑𝑥)) · (𝐹‘𝑥)) = ((1 / (2↑𝑥)) · 0))
80	70	rpcnd 9802	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (1 / (2↑𝑥)) ∈ ℂ)
81	80	mul01d 8447	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → ((1 / (2↑𝑥)) · 0) = 0)
82	79, 81	eqtrd 2237	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → ((1 / (2↑𝑥)) · (𝐹‘𝑥)) = 0)
83	82	oveq2d 5950	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (Σ𝑖 ∈ (1..^𝑥)((1 / (2↑𝑖)) · (𝐹‘𝑖)) + ((1 / (2↑𝑥)) · (𝐹‘𝑥))) = (Σ𝑖 ∈ (1..^𝑥)((1 / (2↑𝑖)) · (𝐹‘𝑖)) + 0))
84	44, 77, 83	3eqtrd 2241	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ (1...((𝑥 + 1) − 1))((1 / (2↑𝑖)) · (𝐹‘𝑖)) = (Σ𝑖 ∈ (1..^𝑥)((1 / (2↑𝑖)) · (𝐹‘𝑖)) + 0))
85	84	oveq1d 5949	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (Σ𝑖 ∈ (1...((𝑥 + 1) − 1))((1 / (2↑𝑖)) · (𝐹‘𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖))) = ((Σ𝑖 ∈ (1..^𝑥)((1 / (2↑𝑖)) · (𝐹‘𝑖)) + 0) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖))))
86	35, 85	eqtrd 2237	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹‘𝑖)) = ((Σ𝑖 ∈ (1..^𝑥)((1 / (2↑𝑖)) · (𝐹‘𝑖)) + 0) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖))))
87	50, 62	fsumrecl 11631	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ (1..^𝑥)((1 / (2↑𝑖)) · (𝐹‘𝑖)) ∈ ℝ)
88		0red 8055	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 0 ∈ ℝ)
89	87, 88	readdcld 8084	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (Σ𝑖 ∈ (1..^𝑥)((1 / (2↑𝑖)) · (𝐹‘𝑖)) + 0) ∈ ℝ)
90	10	nnzd 9476	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (𝑥 + 1) ∈ ℤ)
91		eluznn 9703	. . . . . . . . . . . . . . . 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 5667	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (ℤ_≥‘(𝑥 + 1))) → ((𝑛 ∈ ℕ ↦ ((1 / (2↑𝑛)) · (𝐹‘𝑛)))‘𝑖) = ((1 / (2↑𝑖)) · (𝐹‘𝑖)))
95	31, 32	eqeltrd 2281	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((1 / (2↑𝑛)) · (𝐹‘𝑛)))‘𝑖) ∈ ℂ)
96	7, 10, 95	iserex 11569	. . . . . . . . . . . . . . 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 11659	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖)) ∈ ℝ)
99	50, 58	fsumrecl 11631	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ (1..^𝑥)(1 / (2↑𝑖)) ∈ ℝ)
100	99, 71	readdcld 8084	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (Σ𝑖 ∈ (1..^𝑥)(1 / (2↑𝑖)) + (1 / (2↑𝑥))) ∈ ℝ)
101		eqid 2204	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ ↦ (1 / (2↑𝑛))) = (𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))
102	92, 21	syldan 282	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (ℤ_≥‘(𝑥 + 1))) → (1 / (2↑𝑖)) ∈ ℝ⁺)
103	101, 13, 92, 102	fvmptd3 5667	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (ℤ_≥‘(𝑥 + 1))) → ((𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))‘𝑖) = (1 / (2↑𝑖)))
104	92, 22	syldan 282	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (ℤ_≥‘(𝑥 + 1))) → (1 / (2↑𝑖)) ∈ ℝ)
105		seqex 10575	. . . . . . . . . . . . . . . . 17 ⊢ seq1( + , (𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))) ∈ V
106		ax-1cn 8000	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℂ
107	101	geo2lim 11746	. . . . . . . . . . . . . . . . . 18 ⊢ (1 ∈ ℂ → seq1( + , (𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))) ⇝ 1)
108	106, 107	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ seq1( + , (𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))) ⇝ 1
109		breldmg 4882	. . . . . . . . . . . . . . . . 17 ⊢ ((seq1( + , (𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))) ∈ V ∧ 1 ∈ ℂ ∧ seq1( + , (𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))) ⇝ 1) → seq1( + , (𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))) ∈ dom ⇝ )
110	105, 106, 108, 109	mp3an 1349	. . . . . . . . . . . . . . . 16 ⊢ seq1( + , (𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))) ∈ dom ⇝
111	110	a1i 9	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → seq1( + , (𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))) ∈ dom ⇝ )
112	101, 13, 16, 21	fvmptd3 5667	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))‘𝑖) = (1 / (2↑𝑖)))
113	21	rpcnd 9802	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → (1 / (2↑𝑖)) ∈ ℂ)
114	112, 113	eqeltrd 2281	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))‘𝑖) ∈ ℂ)
115	7, 10, 114	iserex 11569	. . . . . . . . . . . . . . 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 11659	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖)) ∈ ℝ)
118		simpr 110	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 0) → (𝐹‘𝑖) = 0)
119	118	oveq2d 5950	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 0) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) = ((1 / (2↑𝑖)) · 0))
120	57	adantr 276	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 0) → (1 / (2↑𝑖)) ∈ ℝ⁺)
121	120	rpcnd 9802	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 0) → (1 / (2↑𝑖)) ∈ ℂ)
122	121	mul01d 8447	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 0) → ((1 / (2↑𝑖)) · 0) = 0)
123	119, 122	eqtrd 2237	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 0) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) = 0)
124	120	rpge0d 9804	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 0) → 0 ≤ (1 / (2↑𝑖)))
125	123, 124	eqbrtrd 4065	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 0) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) ≤ (1 / (2↑𝑖)))
126		simpr 110	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 1) → (𝐹‘𝑖) = 1)
127	126	oveq2d 5950	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 1) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) = ((1 / (2↑𝑖)) · 1))
128	58	adantr 276	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 1) → (1 / (2↑𝑖)) ∈ ℝ)
129	128	recnd 8083	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 1) → (1 / (2↑𝑖)) ∈ ℂ)
130	129	mulridd 8071	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 1) → ((1 / (2↑𝑖)) · 1) = (1 / (2↑𝑖)))
131	127, 130	eqtrd 2237	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 1) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) = (1 / (2↑𝑖)))
132	128	leidd 8569	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 1) → (1 / (2↑𝑖)) ≤ (1 / (2↑𝑖)))
133	131, 132	eqbrtrd 4065	. . . . . . . . . . . . . . . 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 5710	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → (𝐹‘𝑖) ∈ {0, 1})
137		elpri 3655	. . . . . . . . . . . . . . . . 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 11693	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ (1..^𝑥)((1 / (2↑𝑖)) · (𝐹‘𝑖)) ≤ Σ𝑖 ∈ (1..^𝑥)(1 / (2↑𝑖)))
141	70	rpgt0d 9803	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 0 < (1 / (2↑𝑥)))
142	87, 88, 99, 71, 140, 141	leltaddd 8621	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (Σ𝑖 ∈ (1..^𝑥)((1 / (2↑𝑖)) · (𝐹‘𝑖)) + 0) < (Σ𝑖 ∈ (1..^𝑥)(1 / (2↑𝑖)) + (1 / (2↑𝑥))))
143	72, 4, 8, 10	trilpolemisumle 15841	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖)) ≤ Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖)))
144	89, 98, 100, 117, 142, 143	ltleaddd 8620	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → ((Σ𝑖 ∈ (1..^𝑥)((1 / (2↑𝑖)) · (𝐹‘𝑖)) + 0) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖))) < ((Σ𝑖 ∈ (1..^𝑥)(1 / (2↑𝑖)) + (1 / (2↑𝑥))) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))))
145	86, 144	eqbrtrd 4065	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹‘𝑖)) < ((Σ𝑖 ∈ (1..^𝑥)(1 / (2↑𝑖)) + (1 / (2↑𝑥))) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))))
146	4, 145	eqbrtrid 4078	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝐴 < ((Σ𝑖 ∈ (1..^𝑥)(1 / (2↑𝑖)) + (1 / (2↑𝑥))) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))))
147		nfcv 2347	. . . . . . . . . . . 12 ⊢ Ⅎ𝑖(1 / (2↑𝑥))
148	57	rpcnd 9802	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → (1 / (2↑𝑖)) ∈ ℂ)
149	45, 147, 50, 9, 52, 148, 65, 80	fsumsplitsn 11640	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ ((1..^𝑥) ∪ {𝑥})(1 / (2↑𝑖)) = (Σ𝑖 ∈ (1..^𝑥)(1 / (2↑𝑖)) + (1 / (2↑𝑥))))
150	149	oveq1d 5949	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (Σ𝑖 ∈ ((1..^𝑥) ∪ {𝑥})(1 / (2↑𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))) = ((Σ𝑖 ∈ (1..^𝑥)(1 / (2↑𝑖)) + (1 / (2↑𝑥))) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))))
151	146, 150	breqtrrd 4071	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝐴 < (Σ𝑖 ∈ ((1..^𝑥) ∪ {𝑥})(1 / (2↑𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))))
152	42	sumeq1d 11596	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ (1...𝑥)(1 / (2↑𝑖)) = Σ𝑖 ∈ ((1..^𝑥) ∪ {𝑥})(1 / (2↑𝑖)))
153	152	oveq1d 5949	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (Σ𝑖 ∈ (1...𝑥)(1 / (2↑𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))) = (Σ𝑖 ∈ ((1..^𝑥) ∪ {𝑥})(1 / (2↑𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))))
154	151, 153	breqtrrd 4071	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝐴 < (Σ𝑖 ∈ (1...𝑥)(1 / (2↑𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))))
155	7, 8, 10, 112, 113, 111	isumsplit 11721	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ ℕ (1 / (2↑𝑖)) = (Σ𝑖 ∈ (1...((𝑥 + 1) − 1))(1 / (2↑𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))))
156	39	sumeq1d 11596	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ (1...((𝑥 + 1) − 1))(1 / (2↑𝑖)) = Σ𝑖 ∈ (1...𝑥)(1 / (2↑𝑖)))
157	156	oveq1d 5949	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (Σ𝑖 ∈ (1...((𝑥 + 1) − 1))(1 / (2↑𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))) = (Σ𝑖 ∈ (1...𝑥)(1 / (2↑𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))))
158	155, 157	eqtrd 2237	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ ℕ (1 / (2↑𝑖)) = (Σ𝑖 ∈ (1...𝑥)(1 / (2↑𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))))
159	154, 158	breqtrrd 4071	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝐴 < Σ𝑖 ∈ ℕ (1 / (2↑𝑖)))
160		geoihalfsum 11752	. . . . . . 7 ⊢ Σ𝑖 ∈ ℕ (1 / (2↑𝑖)) = 1
161	159, 160	breqtrdi 4084	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝐴 < 1)
162	6, 161	ltned 8168	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝐴 ≠ 1)
163	162	neneqd 2396	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → ¬ 𝐴 = 1)
164	2, 163	pm2.65da 662	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ¬ (𝐹‘𝑥) = 0)
165	3	ffvelcdmda 5709	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (𝐹‘𝑥) ∈ {0, 1})
166		elpri 3655	. . . . 5 ⊢ ((𝐹‘𝑥) ∈ {0, 1} → ((𝐹‘𝑥) = 0 ∨ (𝐹‘𝑥) = 1))
167	165, 166	syl 14	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝐹‘𝑥) = 0 ∨ (𝐹‘𝑥) = 1))
168	167	orcomd 730	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝐹‘𝑥) = 1 ∨ (𝐹‘𝑥) = 0))
169	164, 168	ecased 1361	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (𝐹‘𝑥) = 1)
170	169	ralrimiva 2578	1 ⊢ (𝜑 → ∀𝑥 ∈ ℕ (𝐹‘𝑥) = 1)

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ∨ wo 709 = wceq 1372 ∈ wcel 2175 ∀wral 2483 Vcvv 2771 ∪ cun 3163 ⊆ wss 3165 {csn 3632 {cpr 3633 class class class wbr 4043 ↦ cmpt 4104 dom cdm 4673 ⟶wf 5264 ‘cfv 5268 (class class class)co 5934 Fincfn 6817 ℂcc 7905 ℝcr 7906 0cc0 7907 1c1 7908 + caddc 7910 · cmul 7912 < clt 8089 ≤ cle 8090 − cmin 8225 / cdiv 8727 ℕcn 9018 2c2 9069 ℤcz 9354 ℤ_≥cuz 9630 ℝ⁺crp 9757 ...cfz 10112 ..^cfzo 10246 seqcseq 10573 ↑cexp 10664 ⇝ cli 11508 Σcsu 11583

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 1469 ax-7 1470 ax-gen 1471 ax-ie1 1515 ax-ie2 1516 ax-8 1526 ax-10 1527 ax-11 1528 ax-i12 1529 ax-bndl 1531 ax-4 1532 ax-17 1548 ax-i9 1552 ax-ial 1556 ax-i5r 1557 ax-13 2177 ax-14 2178 ax-ext 2186 ax-coll 4158 ax-sep 4161 ax-nul 4169 ax-pow 4217 ax-pr 4252 ax-un 4478 ax-setind 4583 ax-iinf 4634 ax-cnex 7998 ax-resscn 7999 ax-1cn 8000 ax-1re 8001 ax-icn 8002 ax-addcl 8003 ax-addrcl 8004 ax-mulcl 8005 ax-mulrcl 8006 ax-addcom 8007 ax-mulcom 8008 ax-addass 8009 ax-mulass 8010 ax-distr 8011 ax-i2m1 8012 ax-0lt1 8013 ax-1rid 8014 ax-0id 8015 ax-rnegex 8016 ax-precex 8017 ax-cnre 8018 ax-pre-ltirr 8019 ax-pre-ltwlin 8020 ax-pre-lttrn 8021 ax-pre-apti 8022 ax-pre-ltadd 8023 ax-pre-mulgt0 8024 ax-pre-mulext 8025 ax-arch 8026 ax-caucvg 8027

This theorem depends on definitions: df-bi 117 df-dc 836 df-3or 981 df-3an 982 df-tru 1375 df-fal 1378 df-nf 1483 df-sb 1785 df-eu 2056 df-mo 2057 df-clab 2191 df-cleq 2197 df-clel 2200 df-nfc 2336 df-ne 2376 df-nel 2471 df-ral 2488 df-rex 2489 df-reu 2490 df-rmo 2491 df-rab 2492 df-v 2773 df-sbc 2998 df-csb 3093 df-dif 3167 df-un 3169 df-in 3171 df-ss 3178 df-nul 3460 df-if 3571 df-pw 3617 df-sn 3638 df-pr 3639 df-op 3641 df-uni 3850 df-int 3885 df-iun 3928 df-br 4044 df-opab 4105 df-mpt 4106 df-tr 4142 df-id 4338 df-po 4341 df-iso 4342 df-iord 4411 df-on 4413 df-ilim 4414 df-suc 4416 df-iom 4637 df-xp 4679 df-rel 4680 df-cnv 4681 df-co 4682 df-dm 4683 df-rn 4684 df-res 4685 df-ima 4686 df-iota 5229 df-fun 5270 df-fn 5271 df-f 5272 df-f1 5273 df-fo 5274 df-f1o 5275 df-fv 5276 df-isom 5277 df-riota 5889 df-ov 5937 df-oprab 5938 df-mpo 5939 df-1st 6216 df-2nd 6217 df-recs 6381 df-irdg 6446 df-frec 6467 df-1o 6492 df-oadd 6496 df-er 6610 df-en 6818 df-dom 6819 df-fin 6820 df-pnf 8091 df-mnf 8092 df-xr 8093 df-ltxr 8094 df-le 8095 df-sub 8227 df-neg 8228 df-reap 8630 df-ap 8637 df-div 8728 df-inn 9019 df-2 9077 df-3 9078 df-4 9079 df-n0 9278 df-z 9355 df-uz 9631 df-q 9723 df-rp 9758 df-ico 9998 df-fz 10113 df-fzo 10247 df-seqfrec 10574 df-exp 10665 df-ihash 10902 df-cj 11072 df-re 11073 df-im 11074 df-rsqrt 11228 df-abs 11229 df-clim 11509 df-sumdc 11584

This theorem is referenced by: trilpolemres 15845 redcwlpolemeq1 15857

W3C validator