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 16120

Description: Lemma for trilpo 16123. 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 16117	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℝ)
6	5	ad2antrr 488	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝐴 ∈ ℝ)
7		nnuz 9704	. . . . . . . . . . . . . 14 ⊢ ℕ = (ℤ_≥‘1)
8		eqid 2206	. . . . . . . . . . . . . 14 ⊢ (ℤ_≥‘(𝑥 + 1)) = (ℤ_≥‘(𝑥 + 1))
9		simplr 528	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝑥 ∈ ℕ)
10	9	peano2nnd 9071	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (𝑥 + 1) ∈ ℕ)
11		eqid 2206	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ ↦ ((1 / (2↑𝑛)) · (𝐹‘𝑛))) = (𝑛 ∈ ℕ ↦ ((1 / (2↑𝑛)) · (𝐹‘𝑛)))
12		oveq2 5965	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑖 → (2↑𝑛) = (2↑𝑖))
13	12	oveq2d 5973	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑖 → (1 / (2↑𝑛)) = (1 / (2↑𝑖)))
14		fveq2 5589	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑖 → (𝐹‘𝑛) = (𝐹‘𝑖))
15	13, 14	oveq12d 5975	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑖 → ((1 / (2↑𝑛)) · (𝐹‘𝑛)) = ((1 / (2↑𝑖)) · (𝐹‘𝑖)))
16		simpr 110	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → 𝑖 ∈ ℕ)
17		2rp 9800	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 ∈ ℝ⁺
18	17	a1i 9	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → 2 ∈ ℝ⁺)
19	16	nnzd 9514	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → 𝑖 ∈ ℤ)
20	18, 19	rpexpcld 10864	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → (2↑𝑖) ∈ ℝ⁺)
21	20	rpreccld 9849	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → (1 / (2↑𝑖)) ∈ ℝ⁺)
22	21	rpred 9838	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → (1 / (2↑𝑖)) ∈ ℝ)
23		0re 8092	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ∈ ℝ
24		1re 8091	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ ℝ
25		prssi 3797	. . . . . . . . . . . . . . . . . 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 5729	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → (𝐹‘𝑖) ∈ {0, 1})
29	26, 28	sselid 3195	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → (𝐹‘𝑖) ∈ ℝ)
30	22, 29	remulcld 8123	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) ∈ ℝ)
31	11, 15, 16, 30	fvmptd3 5686	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((1 / (2↑𝑛)) · (𝐹‘𝑛)))‘𝑖) = ((1 / (2↑𝑖)) · (𝐹‘𝑖)))
32	30	recnd 8121	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) ∈ ℂ)
33	3, 11	trilpolemclim 16116	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → seq1( + , (𝑛 ∈ ℕ ↦ ((1 / (2↑𝑛)) · (𝐹‘𝑛)))) ∈ dom ⇝ )
34	33	ad2antrr 488	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → seq1( + , (𝑛 ∈ ℕ ↦ ((1 / (2↑𝑛)) · (𝐹‘𝑛)))) ∈ dom ⇝ )
35	7, 8, 10, 31, 32, 34	isumsplit 11877	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹‘𝑖)) = (Σ𝑖 ∈ (1...((𝑥 + 1) − 1))((1 / (2↑𝑖)) · (𝐹‘𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖))))
36	9	nncnd 9070	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝑥 ∈ ℂ)
37		1cnd 8108	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 1 ∈ ℂ)
38	36, 37	pncand 8404	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → ((𝑥 + 1) − 1) = 𝑥)
39	38	oveq2d 5973	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (1...((𝑥 + 1) − 1)) = (1...𝑥))
40	9, 7	eleqtrdi 2299	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝑥 ∈ (ℤ_≥‘1))
41		fzisfzounsn 10387	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (ℤ_≥‘1) → (1...𝑥) = ((1..^𝑥) ∪ {𝑥}))
42	40, 41	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (1...𝑥) = ((1..^𝑥) ∪ {𝑥}))
43	39, 42	eqtrd 2239	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (1...((𝑥 + 1) − 1)) = ((1..^𝑥) ∪ {𝑥}))
44	43	sumeq1d 11752	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ (1...((𝑥 + 1) − 1))((1 / (2↑𝑖)) · (𝐹‘𝑖)) = Σ𝑖 ∈ ((1..^𝑥) ∪ {𝑥})((1 / (2↑𝑖)) · (𝐹‘𝑖)))
45		nfv 1552	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑖((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0)
46		nfcv 2349	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑖((1 / (2↑𝑥)) · (𝐹‘𝑥))
47		1zzd 9419	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 1 ∈ ℤ)
48	9	nnzd 9514	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝑥 ∈ ℤ)
49		fzofig 10599	. . . . . . . . . . . . . . . . 17 ⊢ ((1 ∈ ℤ ∧ 𝑥 ∈ ℤ) → (1..^𝑥) ∈ Fin)
50	47, 48, 49	syl2anc 411	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (1..^𝑥) ∈ Fin)
51		fzonel 10303	. . . . . . . . . . . . . . . . 17 ⊢ ¬ 𝑥 ∈ (1..^𝑥)
52	51	a1i 9	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → ¬ 𝑥 ∈ (1..^𝑥))
53	17	a1i 9	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → 2 ∈ ℝ⁺)
54		elfzoelz 10289	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 ∈ (1..^𝑥) → 𝑖 ∈ ℤ)
55	54	adantl 277	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → 𝑖 ∈ ℤ)
56	53, 55	rpexpcld 10864	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → (2↑𝑖) ∈ ℝ⁺)
57	56	rpreccld 9849	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → (1 / (2↑𝑖)) ∈ ℝ⁺)
58	57	rpred 9838	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → (1 / (2↑𝑖)) ∈ ℝ)
59		elfzouz 10293	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ (1..^𝑥) → 𝑖 ∈ (ℤ_≥‘1))
60	59, 7	eleqtrrdi 2300	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 ∈ (1..^𝑥) → 𝑖 ∈ ℕ)
61	60, 29	sylan2 286	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → (𝐹‘𝑖) ∈ ℝ)
62	58, 61	remulcld 8123	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) ∈ ℝ)
63	62	recnd 8121	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) ∈ ℂ)
64		oveq2 5965	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑥 → (2↑𝑖) = (2↑𝑥))
65	64	oveq2d 5973	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑥 → (1 / (2↑𝑖)) = (1 / (2↑𝑥)))
66		fveq2 5589	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑥 → (𝐹‘𝑖) = (𝐹‘𝑥))
67	65, 66	oveq12d 5975	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑥 → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) = ((1 / (2↑𝑥)) · (𝐹‘𝑥)))
68	17	a1i 9	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 2 ∈ ℝ⁺)
69	68, 48	rpexpcld 10864	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (2↑𝑥) ∈ ℝ⁺)
70	69	rpreccld 9849	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (1 / (2↑𝑥)) ∈ ℝ⁺)
71	70	rpred 9838	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (1 / (2↑𝑥)) ∈ ℝ)
72	3	ad2antrr 488	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝐹:ℕ⟶{0, 1})
73	72, 9	ffvelcdmd 5729	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (𝐹‘𝑥) ∈ {0, 1})
74	26, 73	sselid 3195	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (𝐹‘𝑥) ∈ ℝ)
75	71, 74	remulcld 8123	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → ((1 / (2↑𝑥)) · (𝐹‘𝑥)) ∈ ℝ)
76	75	recnd 8121	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → ((1 / (2↑𝑥)) · (𝐹‘𝑥)) ∈ ℂ)
77	45, 46, 50, 9, 52, 63, 67, 76	fsumsplitsn 11796	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ ((1..^𝑥) ∪ {𝑥})((1 / (2↑𝑖)) · (𝐹‘𝑖)) = (Σ𝑖 ∈ (1..^𝑥)((1 / (2↑𝑖)) · (𝐹‘𝑖)) + ((1 / (2↑𝑥)) · (𝐹‘𝑥))))
78		simpr 110	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (𝐹‘𝑥) = 0)
79	78	oveq2d 5973	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → ((1 / (2↑𝑥)) · (𝐹‘𝑥)) = ((1 / (2↑𝑥)) · 0))
80	70	rpcnd 9840	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (1 / (2↑𝑥)) ∈ ℂ)
81	80	mul01d 8485	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → ((1 / (2↑𝑥)) · 0) = 0)
82	79, 81	eqtrd 2239	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → ((1 / (2↑𝑥)) · (𝐹‘𝑥)) = 0)
83	82	oveq2d 5973	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (Σ𝑖 ∈ (1..^𝑥)((1 / (2↑𝑖)) · (𝐹‘𝑖)) + ((1 / (2↑𝑥)) · (𝐹‘𝑥))) = (Σ𝑖 ∈ (1..^𝑥)((1 / (2↑𝑖)) · (𝐹‘𝑖)) + 0))
84	44, 77, 83	3eqtrd 2243	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ (1...((𝑥 + 1) − 1))((1 / (2↑𝑖)) · (𝐹‘𝑖)) = (Σ𝑖 ∈ (1..^𝑥)((1 / (2↑𝑖)) · (𝐹‘𝑖)) + 0))
85	84	oveq1d 5972	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (Σ𝑖 ∈ (1...((𝑥 + 1) − 1))((1 / (2↑𝑖)) · (𝐹‘𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖))) = ((Σ𝑖 ∈ (1..^𝑥)((1 / (2↑𝑖)) · (𝐹‘𝑖)) + 0) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖))))
86	35, 85	eqtrd 2239	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹‘𝑖)) = ((Σ𝑖 ∈ (1..^𝑥)((1 / (2↑𝑖)) · (𝐹‘𝑖)) + 0) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖))))
87	50, 62	fsumrecl 11787	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ (1..^𝑥)((1 / (2↑𝑖)) · (𝐹‘𝑖)) ∈ ℝ)
88		0red 8093	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 0 ∈ ℝ)
89	87, 88	readdcld 8122	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (Σ𝑖 ∈ (1..^𝑥)((1 / (2↑𝑖)) · (𝐹‘𝑖)) + 0) ∈ ℝ)
90	10	nnzd 9514	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (𝑥 + 1) ∈ ℤ)
91		eluznn 9741	. . . . . . . . . . . . . . . 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 5686	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (ℤ_≥‘(𝑥 + 1))) → ((𝑛 ∈ ℕ ↦ ((1 / (2↑𝑛)) · (𝐹‘𝑛)))‘𝑖) = ((1 / (2↑𝑖)) · (𝐹‘𝑖)))
95	31, 32	eqeltrd 2283	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((1 / (2↑𝑛)) · (𝐹‘𝑛)))‘𝑖) ∈ ℂ)
96	7, 10, 95	iserex 11725	. . . . . . . . . . . . . . 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 11815	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖)) ∈ ℝ)
99	50, 58	fsumrecl 11787	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ (1..^𝑥)(1 / (2↑𝑖)) ∈ ℝ)
100	99, 71	readdcld 8122	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (Σ𝑖 ∈ (1..^𝑥)(1 / (2↑𝑖)) + (1 / (2↑𝑥))) ∈ ℝ)
101		eqid 2206	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ ↦ (1 / (2↑𝑛))) = (𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))
102	92, 21	syldan 282	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (ℤ_≥‘(𝑥 + 1))) → (1 / (2↑𝑖)) ∈ ℝ⁺)
103	101, 13, 92, 102	fvmptd3 5686	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (ℤ_≥‘(𝑥 + 1))) → ((𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))‘𝑖) = (1 / (2↑𝑖)))
104	92, 22	syldan 282	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (ℤ_≥‘(𝑥 + 1))) → (1 / (2↑𝑖)) ∈ ℝ)
105		seqex 10616	. . . . . . . . . . . . . . . . 17 ⊢ seq1( + , (𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))) ∈ V
106		ax-1cn 8038	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℂ
107	101	geo2lim 11902	. . . . . . . . . . . . . . . . . 18 ⊢ (1 ∈ ℂ → seq1( + , (𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))) ⇝ 1)
108	106, 107	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ seq1( + , (𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))) ⇝ 1
109		breldmg 4893	. . . . . . . . . . . . . . . . 17 ⊢ ((seq1( + , (𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))) ∈ V ∧ 1 ∈ ℂ ∧ seq1( + , (𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))) ⇝ 1) → seq1( + , (𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))) ∈ dom ⇝ )
110	105, 106, 108, 109	mp3an 1350	. . . . . . . . . . . . . . . 16 ⊢ seq1( + , (𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))) ∈ dom ⇝
111	110	a1i 9	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → seq1( + , (𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))) ∈ dom ⇝ )
112	101, 13, 16, 21	fvmptd3 5686	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))‘𝑖) = (1 / (2↑𝑖)))
113	21	rpcnd 9840	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → (1 / (2↑𝑖)) ∈ ℂ)
114	112, 113	eqeltrd 2283	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (1 / (2↑𝑛)))‘𝑖) ∈ ℂ)
115	7, 10, 114	iserex 11725	. . . . . . . . . . . . . . 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 11815	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖)) ∈ ℝ)
118		simpr 110	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 0) → (𝐹‘𝑖) = 0)
119	118	oveq2d 5973	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 0) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) = ((1 / (2↑𝑖)) · 0))
120	57	adantr 276	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 0) → (1 / (2↑𝑖)) ∈ ℝ⁺)
121	120	rpcnd 9840	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 0) → (1 / (2↑𝑖)) ∈ ℂ)
122	121	mul01d 8485	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 0) → ((1 / (2↑𝑖)) · 0) = 0)
123	119, 122	eqtrd 2239	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 0) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) = 0)
124	120	rpge0d 9842	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 0) → 0 ≤ (1 / (2↑𝑖)))
125	123, 124	eqbrtrd 4073	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 0) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) ≤ (1 / (2↑𝑖)))
126		simpr 110	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 1) → (𝐹‘𝑖) = 1)
127	126	oveq2d 5973	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 1) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) = ((1 / (2↑𝑖)) · 1))
128	58	adantr 276	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 1) → (1 / (2↑𝑖)) ∈ ℝ)
129	128	recnd 8121	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 1) → (1 / (2↑𝑖)) ∈ ℂ)
130	129	mulridd 8109	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 1) → ((1 / (2↑𝑖)) · 1) = (1 / (2↑𝑖)))
131	127, 130	eqtrd 2239	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 1) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) = (1 / (2↑𝑖)))
132	128	leidd 8607	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) ∧ (𝐹‘𝑖) = 1) → (1 / (2↑𝑖)) ≤ (1 / (2↑𝑖)))
133	131, 132	eqbrtrd 4073	. . . . . . . . . . . . . . . 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 5729	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → (𝐹‘𝑖) ∈ {0, 1})
137		elpri 3661	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑖) ∈ {0, 1} → ((𝐹‘𝑖) = 0 ∨ (𝐹‘𝑖) = 1))
138	136, 137	syl 14	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → ((𝐹‘𝑖) = 0 ∨ (𝐹‘𝑖) = 1))
139	125, 133, 138	mpjaodan 800	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → ((1 / (2↑𝑖)) · (𝐹‘𝑖)) ≤ (1 / (2↑𝑖)))
140	50, 62, 58, 139	fsumle 11849	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ (1..^𝑥)((1 / (2↑𝑖)) · (𝐹‘𝑖)) ≤ Σ𝑖 ∈ (1..^𝑥)(1 / (2↑𝑖)))
141	70	rpgt0d 9841	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 0 < (1 / (2↑𝑥)))
142	87, 88, 99, 71, 140, 141	leltaddd 8659	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (Σ𝑖 ∈ (1..^𝑥)((1 / (2↑𝑖)) · (𝐹‘𝑖)) + 0) < (Σ𝑖 ∈ (1..^𝑥)(1 / (2↑𝑖)) + (1 / (2↑𝑥))))
143	72, 4, 8, 10	trilpolemisumle 16118	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖)) ≤ Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖)))
144	89, 98, 100, 117, 142, 143	ltleaddd 8658	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → ((Σ𝑖 ∈ (1..^𝑥)((1 / (2↑𝑖)) · (𝐹‘𝑖)) + 0) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))((1 / (2↑𝑖)) · (𝐹‘𝑖))) < ((Σ𝑖 ∈ (1..^𝑥)(1 / (2↑𝑖)) + (1 / (2↑𝑥))) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))))
145	86, 144	eqbrtrd 4073	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹‘𝑖)) < ((Σ𝑖 ∈ (1..^𝑥)(1 / (2↑𝑖)) + (1 / (2↑𝑥))) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))))
146	4, 145	eqbrtrid 4086	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝐴 < ((Σ𝑖 ∈ (1..^𝑥)(1 / (2↑𝑖)) + (1 / (2↑𝑥))) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))))
147		nfcv 2349	. . . . . . . . . . . 12 ⊢ Ⅎ𝑖(1 / (2↑𝑥))
148	57	rpcnd 9840	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) ∧ 𝑖 ∈ (1..^𝑥)) → (1 / (2↑𝑖)) ∈ ℂ)
149	45, 147, 50, 9, 52, 148, 65, 80	fsumsplitsn 11796	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ ((1..^𝑥) ∪ {𝑥})(1 / (2↑𝑖)) = (Σ𝑖 ∈ (1..^𝑥)(1 / (2↑𝑖)) + (1 / (2↑𝑥))))
150	149	oveq1d 5972	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (Σ𝑖 ∈ ((1..^𝑥) ∪ {𝑥})(1 / (2↑𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))) = ((Σ𝑖 ∈ (1..^𝑥)(1 / (2↑𝑖)) + (1 / (2↑𝑥))) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))))
151	146, 150	breqtrrd 4079	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝐴 < (Σ𝑖 ∈ ((1..^𝑥) ∪ {𝑥})(1 / (2↑𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))))
152	42	sumeq1d 11752	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ (1...𝑥)(1 / (2↑𝑖)) = Σ𝑖 ∈ ((1..^𝑥) ∪ {𝑥})(1 / (2↑𝑖)))
153	152	oveq1d 5972	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (Σ𝑖 ∈ (1...𝑥)(1 / (2↑𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))) = (Σ𝑖 ∈ ((1..^𝑥) ∪ {𝑥})(1 / (2↑𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))))
154	151, 153	breqtrrd 4079	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝐴 < (Σ𝑖 ∈ (1...𝑥)(1 / (2↑𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))))
155	7, 8, 10, 112, 113, 111	isumsplit 11877	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ ℕ (1 / (2↑𝑖)) = (Σ𝑖 ∈ (1...((𝑥 + 1) − 1))(1 / (2↑𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))))
156	39	sumeq1d 11752	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ (1...((𝑥 + 1) − 1))(1 / (2↑𝑖)) = Σ𝑖 ∈ (1...𝑥)(1 / (2↑𝑖)))
157	156	oveq1d 5972	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → (Σ𝑖 ∈ (1...((𝑥 + 1) − 1))(1 / (2↑𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))) = (Σ𝑖 ∈ (1...𝑥)(1 / (2↑𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))))
158	155, 157	eqtrd 2239	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → Σ𝑖 ∈ ℕ (1 / (2↑𝑖)) = (Σ𝑖 ∈ (1...𝑥)(1 / (2↑𝑖)) + Σ𝑖 ∈ (ℤ_≥‘(𝑥 + 1))(1 / (2↑𝑖))))
159	154, 158	breqtrrd 4079	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝐴 < Σ𝑖 ∈ ℕ (1 / (2↑𝑖)))
160		geoihalfsum 11908	. . . . . . 7 ⊢ Σ𝑖 ∈ ℕ (1 / (2↑𝑖)) = 1
161	159, 160	breqtrdi 4092	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝐴 < 1)
162	6, 161	ltned 8206	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → 𝐴 ≠ 1)
163	162	neneqd 2398	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ (𝐹‘𝑥) = 0) → ¬ 𝐴 = 1)
164	2, 163	pm2.65da 663	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ¬ (𝐹‘𝑥) = 0)
165	3	ffvelcdmda 5728	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (𝐹‘𝑥) ∈ {0, 1})
166		elpri 3661	. . . . 5 ⊢ ((𝐹‘𝑥) ∈ {0, 1} → ((𝐹‘𝑥) = 0 ∨ (𝐹‘𝑥) = 1))
167	165, 166	syl 14	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝐹‘𝑥) = 0 ∨ (𝐹‘𝑥) = 1))
168	167	orcomd 731	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝐹‘𝑥) = 1 ∨ (𝐹‘𝑥) = 0))
169	164, 168	ecased 1362	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (𝐹‘𝑥) = 1)
170	169	ralrimiva 2580	1 ⊢ (𝜑 → ∀𝑥 ∈ ℕ (𝐹‘𝑥) = 1)

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ∨ wo 710 = wceq 1373 ∈ wcel 2177 ∀wral 2485 Vcvv 2773 ∪ cun 3168 ⊆ wss 3170 {csn 3638 {cpr 3639 class class class wbr 4051 ↦ cmpt 4113 dom cdm 4683 ⟶wf 5276 ‘cfv 5280 (class class class)co 5957 Fincfn 6840 ℂcc 7943 ℝcr 7944 0cc0 7945 1c1 7946 + caddc 7948 · cmul 7950 < clt 8127 ≤ cle 8128 − cmin 8263 / cdiv 8765 ℕcn 9056 2c2 9107 ℤcz 9392 ℤ_≥cuz 9668 ℝ⁺crp 9795 ...cfz 10150 ..^cfzo 10284 seqcseq 10614 ↑cexp 10705 ⇝ cli 11664 Σcsu 11739

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 711 ax-5 1471 ax-7 1472 ax-gen 1473 ax-ie1 1517 ax-ie2 1518 ax-8 1528 ax-10 1529 ax-11 1530 ax-i12 1531 ax-bndl 1533 ax-4 1534 ax-17 1550 ax-i9 1554 ax-ial 1558 ax-i5r 1559 ax-13 2179 ax-14 2180 ax-ext 2188 ax-coll 4167 ax-sep 4170 ax-nul 4178 ax-pow 4226 ax-pr 4261 ax-un 4488 ax-setind 4593 ax-iinf 4644 ax-cnex 8036 ax-resscn 8037 ax-1cn 8038 ax-1re 8039 ax-icn 8040 ax-addcl 8041 ax-addrcl 8042 ax-mulcl 8043 ax-mulrcl 8044 ax-addcom 8045 ax-mulcom 8046 ax-addass 8047 ax-mulass 8048 ax-distr 8049 ax-i2m1 8050 ax-0lt1 8051 ax-1rid 8052 ax-0id 8053 ax-rnegex 8054 ax-precex 8055 ax-cnre 8056 ax-pre-ltirr 8057 ax-pre-ltwlin 8058 ax-pre-lttrn 8059 ax-pre-apti 8060 ax-pre-ltadd 8061 ax-pre-mulgt0 8062 ax-pre-mulext 8063 ax-arch 8064 ax-caucvg 8065

This theorem depends on definitions: df-bi 117 df-dc 837 df-3or 982 df-3an 983 df-tru 1376 df-fal 1379 df-nf 1485 df-sb 1787 df-eu 2058 df-mo 2059 df-clab 2193 df-cleq 2199 df-clel 2202 df-nfc 2338 df-ne 2378 df-nel 2473 df-ral 2490 df-rex 2491 df-reu 2492 df-rmo 2493 df-rab 2494 df-v 2775 df-sbc 3003 df-csb 3098 df-dif 3172 df-un 3174 df-in 3176 df-ss 3183 df-nul 3465 df-if 3576 df-pw 3623 df-sn 3644 df-pr 3645 df-op 3647 df-uni 3857 df-int 3892 df-iun 3935 df-br 4052 df-opab 4114 df-mpt 4115 df-tr 4151 df-id 4348 df-po 4351 df-iso 4352 df-iord 4421 df-on 4423 df-ilim 4424 df-suc 4426 df-iom 4647 df-xp 4689 df-rel 4690 df-cnv 4691 df-co 4692 df-dm 4693 df-rn 4694 df-res 4695 df-ima 4696 df-iota 5241 df-fun 5282 df-fn 5283 df-f 5284 df-f1 5285 df-fo 5286 df-f1o 5287 df-fv 5288 df-isom 5289 df-riota 5912 df-ov 5960 df-oprab 5961 df-mpo 5962 df-1st 6239 df-2nd 6240 df-recs 6404 df-irdg 6469 df-frec 6490 df-1o 6515 df-oadd 6519 df-er 6633 df-en 6841 df-dom 6842 df-fin 6843 df-pnf 8129 df-mnf 8130 df-xr 8131 df-ltxr 8132 df-le 8133 df-sub 8265 df-neg 8266 df-reap 8668 df-ap 8675 df-div 8766 df-inn 9057 df-2 9115 df-3 9116 df-4 9117 df-n0 9316 df-z 9393 df-uz 9669 df-q 9761 df-rp 9796 df-ico 10036 df-fz 10151 df-fzo 10285 df-seqfrec 10615 df-exp 10706 df-ihash 10943 df-cj 11228 df-re 11229 df-im 11230 df-rsqrt 11384 df-abs 11385 df-clim 11665 df-sumdc 11740

This theorem is referenced by: trilpolemres 16122 redcwlpolemeq1 16134

W3C validator