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 16644

Description: Lemma for trilpo 16647. 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 16641	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℝ)
6	5	ad2antrr 488	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝐴 ∈ ℝ)
7		nnuz 9791	. . . . . . . . . . . . . 14 ⊢ ℕ = (ℤ_≥‘1)
8		eqid 2231	. . . . . . . . . . . . . 14 ⊢ (ℤ_≥‘(𝑥 + 1)) = (ℤ_≥‘(𝑥 + 1))
9		simplr 529	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝑥 ∈ ℕ)
10	9	peano2nnd 9157	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (𝑥 + 1) ∈ ℕ)
11		eqid 2231	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ ↦ ((1 / (2↑𝑛)) · (𝐹‘𝑛))) = (𝑛 ∈ ℕ ↦ ((1 / (2↑𝑛)) · (𝐹‘𝑛)))
12		oveq2 6025	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑖 → (2↑𝑛) = (2↑𝑖))
13	12	oveq2d 6033	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑖 → (1 / (2↑𝑛)) = (1 / (2↑𝑖)))
14		fveq2 5639	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑖 → (𝐹‘𝑛) = (𝐹‘𝑖))
15	13, 14	oveq12d 6035	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑖 → ((1 / (2↑𝑛)) · (𝐹‘𝑛)) = ((1 / (2↑𝑖)) · (𝐹‘𝑖)))
16		simpr 110	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → 𝑖 ∈ ℕ)
17		2rp 9892	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 ∈ ℝ⁺
18	17	a1i 9	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → 2 ∈ ℝ⁺)
19	16	nnzd 9600	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → 𝑖 ∈ ℤ)
20	18, 19	rpexpcld 10958	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → (2↑𝑖) ∈ ℝ⁺)
21	20	rpreccld 9941	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → (1 / (2↑𝑖)) ∈ ℝ⁺)
22	21	rpred 9930	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → (1 / (2↑𝑖)) ∈ ℝ)
23		0re 8178	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ∈ ℝ
24		1re 8177	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ ℝ
25		prssi 3831	. . . . . . . . . . . . . . . . . 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 5783	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → (𝐹‘𝑖) ∈ {0, 1})
29	26, 28	sselid 3225	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → (𝐹‘𝑖) ∈ ℝ)
30	22, 29	remulcld 8209	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) ∈ ℝ)
31	11, 15, 16, 30	fvmptd3 5740	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((1 / (2↑𝑛)) · (𝐹‘𝑛)))‘𝑖) = ((1 / (2↑𝑖)) · (𝐹‘𝑖)))
32	30	recnd 8207	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) ∈ ℂ)
33	3, 11	trilpolemclim 16640	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → seq1( + , (𝑛 ∈ ℕ ↦ ((1 / (2↑𝑛)) · (𝐹‘𝑛)))) ∈ dom ⇝ )
34	33	ad2antrr 488	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → seq1( + , (𝑛 ∈ ℕ ↦ ((1 / (2↑𝑛)) · (𝐹‘𝑛)))) ∈ dom ⇝ )
35	7, 8, 10, 31, 32, 34	isumsplit 12051	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹‘𝑖)) = (Σ𝑖 ∈ (1...((𝑥 + 1) − 1))((1 / (2↑𝑖)) · (𝐹‘𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖))))
36	9	nncnd 9156	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝑥 ∈ ℂ)
37		1cnd 8194	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 1 ∈ ℂ)
38	36, 37	pncand 8490	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → ((𝑥 + 1) − 1) = 𝑥)
39	38	oveq2d 6033	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (1...((𝑥 + 1) − 1)) = (1...𝑥))
40	9, 7	eleqtrdi 2324	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝑥 ∈ (ℤ_≥‘1))
41		fzisfzounsn 10481	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (ℤ_≥‘1) → (1...𝑥) = ((1..^𝑥) ∪ {𝑥}))
42	40, 41	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (1...𝑥) = ((1..^𝑥) ∪ {𝑥}))
43	39, 42	eqtrd 2264	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (1...((𝑥 + 1) − 1)) = ((1..^𝑥) ∪ {𝑥}))
44	43	sumeq1d 11926	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ (1...((𝑥 + 1) − 1))((1 / (2↑𝑖)) · (𝐹‘𝑖)) = Σ𝑖 ∈ ((1..^𝑥) ∪ {𝑥})((1 / (2↑𝑖)) · (𝐹‘𝑖)))
45		nfv 1576	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑖((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0)
46		nfcv 2374	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑖((1 / (2↑𝑥)) · (𝐹‘𝑥))
47		1zzd 9505	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 1 ∈ ℤ)
48	9	nnzd 9600	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝑥 ∈ ℤ)
49		fzofig 10693	. . . . . . . . . . . . . . . . 17 ⊢ ((1 ∈ ℤ ∧ 𝑥 ∈ ℤ) → (1..^𝑥) ∈ Fin)
50	47, 48, 49	syl2anc 411	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (1..^𝑥) ∈ Fin)
51		fzonel 10395	. . . . . . . . . . . . . . . . 17 ⊢ ¬ 𝑥 ∈ (1..^𝑥)
52	51	a1i 9	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → ¬ 𝑥 ∈ (1..^𝑥))
53	17	a1i 9	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → 2 ∈ ℝ⁺)
54		elfzoelz 10381	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 ∈ (1..^𝑥) → 𝑖 ∈ ℤ)
55	54	adantl 277	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → 𝑖 ∈ ℤ)
56	53, 55	rpexpcld 10958	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → (2↑𝑖) ∈ ℝ⁺)
57	56	rpreccld 9941	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → (1 / (2↑𝑖)) ∈ ℝ⁺)
58	57	rpred 9930	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → (1 / (2↑𝑖)) ∈ ℝ)
59		elfzouz 10385	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ (1..^𝑥) → 𝑖 ∈ (ℤ_≥‘1))
60	59, 7	eleqtrrdi 2325	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 ∈ (1..^𝑥) → 𝑖 ∈ ℕ)
61	60, 29	sylan2 286	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → (𝐹‘𝑖) ∈ ℝ)
62	58, 61	remulcld 8209	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) ∈ ℝ)
63	62	recnd 8207	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) ∈ ℂ)
64		oveq2 6025	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑥 → (2↑𝑖) = (2↑𝑥))
65	64	oveq2d 6033	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑥 → (1 / (2↑𝑖)) = (1 / (2↑𝑥)))
66		fveq2 5639	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑥 → (𝐹‘𝑖) = (𝐹‘𝑥))
67	65, 66	oveq12d 6035	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑥 → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) = ((1 / (2↑𝑥)) · (𝐹‘𝑥)))
68	17	a1i 9	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 2 ∈ ℝ⁺)
69	68, 48	rpexpcld 10958	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (2↑𝑥) ∈ ℝ⁺)
70	69	rpreccld 9941	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (1 / (2↑𝑥)) ∈ ℝ⁺)
71	70	rpred 9930	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (1 / (2↑𝑥)) ∈ ℝ)
72	3	ad2antrr 488	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝐹:ℕ⟶{0, 1})
73	72, 9	ffvelcdmd 5783	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (𝐹‘𝑥) ∈ {0, 1})
74	26, 73	sselid 3225	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (𝐹‘𝑥) ∈ ℝ)
75	71, 74	remulcld 8209	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → ((1 / (2↑𝑥)) · (𝐹‘𝑥)) ∈ ℝ)
76	75	recnd 8207	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → ((1 / (2↑𝑥)) · (𝐹‘𝑥)) ∈ ℂ)
77	45, 46, 50, 9, 52, 63, 67, 76	fsumsplitsn 11970	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ ((1..^𝑥) ∪ {𝑥})((1 / (2↑𝑖)) · (𝐹‘𝑖)) = (Σ𝑖 ∈ (1..^𝑥)((1 / (2↑𝑖)) · (𝐹‘𝑖)) + ((1 / (2↑𝑥)) · (𝐹‘𝑥))))
78		simpr 110	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (𝐹‘𝑥) = 0)
79	78	oveq2d 6033	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → ((1 / (2↑𝑥)) · (𝐹‘𝑥)) = ((1 / (2↑𝑥)) · 0))
80	70	rpcnd 9932	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (1 / (2↑𝑥)) ∈ ℂ)
81	80	mul01d 8571	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → ((1 / (2↑𝑥)) · 0) = 0)
82	79, 81	eqtrd 2264	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → ((1 / (2↑𝑥)) · (𝐹‘𝑥)) = 0)
83	82	oveq2d 6033	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (Σ𝑖 ∈ (1..^𝑥)((1 / (2↑𝑖)) · (𝐹‘𝑖)) + ((1 / (2↑𝑥)) · (𝐹‘𝑥))) = (Σ𝑖 ∈ (1..^𝑥)((1 / (2↑𝑖)) · (𝐹‘𝑖)) + 0))
84	44, 77, 83	3eqtrd 2268	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ (1...((𝑥 + 1) − 1))((1 / (2↑𝑖)) · (𝐹‘𝑖)) = (Σ𝑖 ∈ (1..^𝑥)((1 / (2↑𝑖)) · (𝐹‘𝑖)) + 0))
85	84	oveq1d 6032	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (Σ𝑖 ∈ (1...((𝑥 + 1) − 1))((1 / (2↑𝑖)) · (𝐹‘𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖))) = ((Σ𝑖 ∈ (1..^𝑥)((1 / (2↑𝑖)) · (𝐹‘𝑖)) + 0) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖))))
86	35, 85	eqtrd 2264	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹‘𝑖)) = ((Σ𝑖 ∈ (1..^𝑥)((1 / (2↑𝑖)) · (𝐹‘𝑖)) + 0) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖))))
87	50, 62	fsumrecl 11961	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ (1..^𝑥)((1 / (2↑𝑖)) · (𝐹‘𝑖)) ∈ ℝ)
88		0red 8179	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 0 ∈ ℝ)
89	87, 88	readdcld 8208	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (Σ𝑖 ∈ (1..^𝑥)((1 / (2↑𝑖)) · (𝐹‘𝑖)) + 0) ∈ ℝ)
90	10	nnzd 9600	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (𝑥 + 1) ∈ ℤ)
91		eluznn 9833	. . . . . . . . . . . . . . . 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 5740	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (ℤ_≥‘(𝑥 + 1))) → ((𝑛 ∈ ℕ ↦ ((1 / (2↑𝑛)) · (𝐹‘𝑛)))‘𝑖) = ((1 / (2↑𝑖)) · (𝐹‘𝑖)))
95	31, 32	eqeltrd 2308	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((1 / (2↑𝑛)) · (𝐹‘𝑛)))‘𝑖) ∈ ℂ)
96	7, 10, 95	iserex 11899	. . . . . . . . . . . . . . 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 11989	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖)) ∈ ℝ)
99	50, 58	fsumrecl 11961	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ (1..^𝑥)(1 / (2↑𝑖)) ∈ ℝ)
100	99, 71	readdcld 8208	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (Σ𝑖 ∈ (1..^𝑥)(1 / (2↑𝑖)) + (1 / (2↑𝑥))) ∈ ℝ)
101		eqid 2231	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ ↦ (1 / (2↑𝑛))) = (𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))
102	92, 21	syldan 282	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (ℤ_≥‘(𝑥 + 1))) → (1 / (2↑𝑖)) ∈ ℝ⁺)
103	101, 13, 92, 102	fvmptd3 5740	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (ℤ_≥‘(𝑥 + 1))) → ((𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))‘𝑖) = (1 / (2↑𝑖)))
104	92, 22	syldan 282	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (ℤ_≥‘(𝑥 + 1))) → (1 / (2↑𝑖)) ∈ ℝ)
105		seqex 10710	. . . . . . . . . . . . . . . . 17 ⊢ seq1( + , (𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))) ∈ V
106		ax-1cn 8124	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℂ
107	101	geo2lim 12076	. . . . . . . . . . . . . . . . . 18 ⊢ (1 ∈ ℂ → seq1( + , (𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))) ⇝ 1)
108	106, 107	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ seq1( + , (𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))) ⇝ 1
109		breldmg 4937	. . . . . . . . . . . . . . . . 17 ⊢ ((seq1( + , (𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))) ∈ V ∧ 1 ∈ ℂ ∧ seq1( + , (𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))) ⇝ 1) → seq1( + , (𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))) ∈ dom ⇝ )
110	105, 106, 108, 109	mp3an 1373	. . . . . . . . . . . . . . . 16 ⊢ seq1( + , (𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))) ∈ dom ⇝
111	110	a1i 9	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → seq1( + , (𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))) ∈ dom ⇝ )
112	101, 13, 16, 21	fvmptd3 5740	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))‘𝑖) = (1 / (2↑𝑖)))
113	21	rpcnd 9932	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → (1 / (2↑𝑖)) ∈ ℂ)
114	112, 113	eqeltrd 2308	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))‘𝑖) ∈ ℂ)
115	7, 10, 114	iserex 11899	. . . . . . . . . . . . . . 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 11989	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖)) ∈ ℝ)
118		simpr 110	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 0) → (𝐹‘𝑖) = 0)
119	118	oveq2d 6033	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 0) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) = ((1 / (2↑𝑖)) · 0))
120	57	adantr 276	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 0) → (1 / (2↑𝑖)) ∈ ℝ⁺)
121	120	rpcnd 9932	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 0) → (1 / (2↑𝑖)) ∈ ℂ)
122	121	mul01d 8571	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 0) → ((1 / (2↑𝑖)) · 0) = 0)
123	119, 122	eqtrd 2264	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 0) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) = 0)
124	120	rpge0d 9934	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 0) → 0 ≤ (1 / (2↑𝑖)))
125	123, 124	eqbrtrd 4110	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 0) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) ≤ (1 / (2↑𝑖)))
126		simpr 110	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 1) → (𝐹‘𝑖) = 1)
127	126	oveq2d 6033	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 1) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) = ((1 / (2↑𝑖)) · 1))
128	58	adantr 276	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 1) → (1 / (2↑𝑖)) ∈ ℝ)
129	128	recnd 8207	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 1) → (1 / (2↑𝑖)) ∈ ℂ)
130	129	mulridd 8195	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 1) → ((1 / (2↑𝑖)) · 1) = (1 / (2↑𝑖)))
131	127, 130	eqtrd 2264	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 1) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) = (1 / (2↑𝑖)))
132	128	leidd 8693	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 1) → (1 / (2↑𝑖)) ≤ (1 / (2↑𝑖)))
133	131, 132	eqbrtrd 4110	. . . . . . . . . . . . . . . 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 5783	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → (𝐹‘𝑖) ∈ {0, 1})
137		elpri 3692	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑖) ∈ {0, 1} → ((𝐹‘𝑖) = 0 ∨ (𝐹‘𝑖) = 1))
138	136, 137	syl 14	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → ((𝐹‘𝑖) = 0 ∨ (𝐹‘𝑖) = 1))
139	125, 133, 138	mpjaodan 805	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) ≤ (1 / (2↑𝑖)))
140	50, 62, 58, 139	fsumle 12023	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ (1..^𝑥)((1 / (2↑𝑖)) · (𝐹‘𝑖)) ≤ Σ𝑖 ∈ (1..^𝑥)(1 / (2↑𝑖)))
141	70	rpgt0d 9933	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 0 < (1 / (2↑𝑥)))
142	87, 88, 99, 71, 140, 141	leltaddd 8745	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (Σ𝑖 ∈ (1..^𝑥)((1 / (2↑𝑖)) · (𝐹‘𝑖)) + 0) < (Σ𝑖 ∈ (1..^𝑥)(1 / (2↑𝑖)) + (1 / (2↑𝑥))))
143	72, 4, 8, 10	trilpolemisumle 16642	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖)) ≤ Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖)))
144	89, 98, 100, 117, 142, 143	ltleaddd 8744	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → ((Σ𝑖 ∈ (1..^𝑥)((1 / (2↑𝑖)) · (𝐹‘𝑖)) + 0) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖))) < ((Σ𝑖 ∈ (1..^𝑥)(1 / (2↑𝑖)) + (1 / (2↑𝑥))) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))))
145	86, 144	eqbrtrd 4110	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹‘𝑖)) < ((Σ𝑖 ∈ (1..^𝑥)(1 / (2↑𝑖)) + (1 / (2↑𝑥))) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))))
146	4, 145	eqbrtrid 4123	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝐴 < ((Σ𝑖 ∈ (1..^𝑥)(1 / (2↑𝑖)) + (1 / (2↑𝑥))) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))))
147		nfcv 2374	. . . . . . . . . . . 12 ⊢ Ⅎ𝑖(1 / (2↑𝑥))
148	57	rpcnd 9932	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → (1 / (2↑𝑖)) ∈ ℂ)
149	45, 147, 50, 9, 52, 148, 65, 80	fsumsplitsn 11970	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ ((1..^𝑥) ∪ {𝑥})(1 / (2↑𝑖)) = (Σ𝑖 ∈ (1..^𝑥)(1 / (2↑𝑖)) + (1 / (2↑𝑥))))
150	149	oveq1d 6032	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (Σ𝑖 ∈ ((1..^𝑥) ∪ {𝑥})(1 / (2↑𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))) = ((Σ𝑖 ∈ (1..^𝑥)(1 / (2↑𝑖)) + (1 / (2↑𝑥))) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))))
151	146, 150	breqtrrd 4116	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝐴 < (Σ𝑖 ∈ ((1..^𝑥) ∪ {𝑥})(1 / (2↑𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))))
152	42	sumeq1d 11926	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ (1...𝑥)(1 / (2↑𝑖)) = Σ𝑖 ∈ ((1..^𝑥) ∪ {𝑥})(1 / (2↑𝑖)))
153	152	oveq1d 6032	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (Σ𝑖 ∈ (1...𝑥)(1 / (2↑𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))) = (Σ𝑖 ∈ ((1..^𝑥) ∪ {𝑥})(1 / (2↑𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))))
154	151, 153	breqtrrd 4116	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝐴 < (Σ𝑖 ∈ (1...𝑥)(1 / (2↑𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))))
155	7, 8, 10, 112, 113, 111	isumsplit 12051	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ ℕ (1 / (2↑𝑖)) = (Σ𝑖 ∈ (1...((𝑥 + 1) − 1))(1 / (2↑𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))))
156	39	sumeq1d 11926	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ (1...((𝑥 + 1) − 1))(1 / (2↑𝑖)) = Σ𝑖 ∈ (1...𝑥)(1 / (2↑𝑖)))
157	156	oveq1d 6032	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (Σ𝑖 ∈ (1...((𝑥 + 1) − 1))(1 / (2↑𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))) = (Σ𝑖 ∈ (1...𝑥)(1 / (2↑𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))))
158	155, 157	eqtrd 2264	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ ℕ (1 / (2↑𝑖)) = (Σ𝑖 ∈ (1...𝑥)(1 / (2↑𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))))
159	154, 158	breqtrrd 4116	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝐴 < Σ𝑖 ∈ ℕ (1 / (2↑𝑖)))
160		geoihalfsum 12082	. . . . . . 7 ⊢ Σ𝑖 ∈ ℕ (1 / (2↑𝑖)) = 1
161	159, 160	breqtrdi 4129	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝐴 < 1)
162	6, 161	ltned 8292	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝐴 ≠ 1)
163	162	neneqd 2423	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → ¬ 𝐴 = 1)
164	2, 163	pm2.65da 667	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ¬ (𝐹‘𝑥) = 0)
165	3	ffvelcdmda 5782	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (𝐹‘𝑥) ∈ {0, 1})
166		elpri 3692	. . . . 5 ⊢ ((𝐹‘𝑥) ∈ {0, 1} → ((𝐹‘𝑥) = 0 ∨ (𝐹‘𝑥) = 1))
167	165, 166	syl 14	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝐹‘𝑥) = 0 ∨ (𝐹‘𝑥) = 1))
168	167	orcomd 736	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝐹‘𝑥) = 1 ∨ (𝐹‘𝑥) = 0))
169	164, 168	ecased 1385	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (𝐹‘𝑥) = 1)
170	169	ralrimiva 2605	1 ⊢ (𝜑 → ∀𝑥 ∈ ℕ (𝐹‘𝑥) = 1)

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ∨ wo 715 = wceq 1397 ∈ wcel 2202 ∀wral 2510 Vcvv 2802 ∪ cun 3198 ⊆ wss 3200 {csn 3669 {cpr 3670 class class class wbr 4088 ↦ cmpt 4150 dom cdm 4725 ⟶wf 5322 ‘cfv 5326 (class class class)co 6017 Fincfn 6908 ℂcc 8029 ℝcr 8030 0cc0 8031 1c1 8032 + caddc 8034 · cmul 8036 < clt 8213 ≤ cle 8214 − cmin 8349 / cdiv 8851 ℕcn 9142 2c2 9193 ℤcz 9478 ℤ_≥cuz 9754 ℝ⁺crp 9887 ...cfz 10242 ..^cfzo 10376 seqcseq 10708 ↑cexp 10799 ⇝ cli 11838 Σcsu 11913

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 619 ax-in2 620 ax-io 716 ax-5 1495 ax-7 1496 ax-gen 1497 ax-ie1 1541 ax-ie2 1542 ax-8 1552 ax-10 1553 ax-11 1554 ax-i12 1555 ax-bndl 1557 ax-4 1558 ax-17 1574 ax-i9 1578 ax-ial 1582 ax-i5r 1583 ax-13 2204 ax-14 2205 ax-ext 2213 ax-coll 4204 ax-sep 4207 ax-nul 4215 ax-pow 4264 ax-pr 4299 ax-un 4530 ax-setind 4635 ax-iinf 4686 ax-cnex 8122 ax-resscn 8123 ax-1cn 8124 ax-1re 8125 ax-icn 8126 ax-addcl 8127 ax-addrcl 8128 ax-mulcl 8129 ax-mulrcl 8130 ax-addcom 8131 ax-mulcom 8132 ax-addass 8133 ax-mulass 8134 ax-distr 8135 ax-i2m1 8136 ax-0lt1 8137 ax-1rid 8138 ax-0id 8139 ax-rnegex 8140 ax-precex 8141 ax-cnre 8142 ax-pre-ltirr 8143 ax-pre-ltwlin 8144 ax-pre-lttrn 8145 ax-pre-apti 8146 ax-pre-ltadd 8147 ax-pre-mulgt0 8148 ax-pre-mulext 8149 ax-arch 8150 ax-caucvg 8151

This theorem depends on definitions: df-bi 117 df-dc 842 df-3or 1005 df-3an 1006 df-tru 1400 df-fal 1403 df-nf 1509 df-sb 1811 df-eu 2082 df-mo 2083 df-clab 2218 df-cleq 2224 df-clel 2227 df-nfc 2363 df-ne 2403 df-nel 2498 df-ral 2515 df-rex 2516 df-reu 2517 df-rmo 2518 df-rab 2519 df-v 2804 df-sbc 3032 df-csb 3128 df-dif 3202 df-un 3204 df-in 3206 df-ss 3213 df-nul 3495 df-if 3606 df-pw 3654 df-sn 3675 df-pr 3676 df-op 3678 df-uni 3894 df-int 3929 df-iun 3972 df-br 4089 df-opab 4151 df-mpt 4152 df-tr 4188 df-id 4390 df-po 4393 df-iso 4394 df-iord 4463 df-on 4465 df-ilim 4466 df-suc 4468 df-iom 4689 df-xp 4731 df-rel 4732 df-cnv 4733 df-co 4734 df-dm 4735 df-rn 4736 df-res 4737 df-ima 4738 df-iota 5286 df-fun 5328 df-fn 5329 df-f 5330 df-f1 5331 df-fo 5332 df-f1o 5333 df-fv 5334 df-isom 5335 df-riota 5970 df-ov 6020 df-oprab 6021 df-mpo 6022 df-1st 6302 df-2nd 6303 df-recs 6470 df-irdg 6535 df-frec 6556 df-1o 6581 df-oadd 6585 df-er 6701 df-en 6909 df-dom 6910 df-fin 6911 df-pnf 8215 df-mnf 8216 df-xr 8217 df-ltxr 8218 df-le 8219 df-sub 8351 df-neg 8352 df-reap 8754 df-ap 8761 df-div 8852 df-inn 9143 df-2 9201 df-3 9202 df-4 9203 df-n0 9402 df-z 9479 df-uz 9755 df-q 9853 df-rp 9888 df-ico 10128 df-fz 10243 df-fzo 10377 df-seqfrec 10709 df-exp 10800 df-ihash 11037 df-cj 11402 df-re 11403 df-im 11404 df-rsqrt 11558 df-abs 11559 df-clim 11839 df-sumdc 11914

This theorem is referenced by: trilpolemres 16646 redcwlpolemeq1 16658

W3C validator