resqrexlemoverl - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > resqrexlemoverl		GIF version

Theorem resqrexlemoverl 11014

Description: Lemma for resqrex 11019. Every term in the sequence is an overestimate compared with the limit 𝐿. Although this theorem is stated in terms of a particular sequence the proof could be adapted for any decreasing convergent sequence. (Contributed by Jim Kingdon, 9-Aug-2021.)

**Hypotheses**
Ref	Expression
resqrexlemex.seq	⊢ 𝐹 = seq1((𝑦 ∈ ℝ⁺, 𝑧 ∈ ℝ⁺ ↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)}))
resqrexlemex.a	⊢ (𝜑 → 𝐴 ∈ ℝ)
resqrexlemex.agt0	⊢ (𝜑 → 0 ≤ 𝐴)
resqrexlemgt0.rr	⊢ (𝜑 → 𝐿 ∈ ℝ)
resqrexlemgt0.lim	⊢ (𝜑 → ∀𝑒 ∈ ℝ⁺ ∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ_≥‘𝑗)((𝐹‘𝑖) < (𝐿 + 𝑒) ∧ 𝐿 < ((𝐹‘𝑖) + 𝑒)))
resqrexlemoverl.k	⊢ (𝜑 → 𝐾 ∈ ℕ)

**Assertion**
Ref	Expression
resqrexlemoverl	⊢ (𝜑 → 𝐿 ≤ (𝐹‘𝐾))

Distinct variable groups: 𝑦,𝐴,𝑧 𝑒,𝐹,𝑖,𝑗 𝑦,𝐹,𝑧,𝑖,𝑗 𝑒,𝐾,𝑖,𝑗 𝑦,𝐾,𝑧 𝑒,𝐿,𝑖,𝑗 𝑦,𝐿,𝑧 𝜑,𝑦,𝑧 Allowed substitution hints: 𝜑(𝑒,𝑖,𝑗) 𝐴(𝑒,𝑖,𝑗)

Proof of Theorem resqrexlemoverl Dummy variable 𝑏 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		oveq2 5877	. . . . . . . . 9 ⊢ (𝑒 = (𝐿 − (𝐹‘𝐾)) → (𝐿 + 𝑒) = (𝐿 + (𝐿 − (𝐹‘𝐾))))
2	1	breq2d 4012	. . . . . . . 8 ⊢ (𝑒 = (𝐿 − (𝐹‘𝐾)) → ((𝐹‘𝑖) < (𝐿 + 𝑒) ↔ (𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾)))))
3		oveq2 5877	. . . . . . . . 9 ⊢ (𝑒 = (𝐿 − (𝐹‘𝐾)) → ((𝐹‘𝑖) + 𝑒) = ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾))))
4	3	breq2d 4012	. . . . . . . 8 ⊢ (𝑒 = (𝐿 − (𝐹‘𝐾)) → (𝐿 < ((𝐹‘𝑖) + 𝑒) ↔ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))
5	2, 4	anbi12d 473	. . . . . . 7 ⊢ (𝑒 = (𝐿 − (𝐹‘𝐾)) → (((𝐹‘𝑖) < (𝐿 + 𝑒) ∧ 𝐿 < ((𝐹‘𝑖) + 𝑒)) ↔ ((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾))))))
6	5	rexralbidv 2503	. . . . . 6 ⊢ (𝑒 = (𝐿 − (𝐹‘𝐾)) → (∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ_≥‘𝑗)((𝐹‘𝑖) < (𝐿 + 𝑒) ∧ 𝐿 < ((𝐹‘𝑖) + 𝑒)) ↔ ∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ_≥‘𝑗)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾))))))
7		resqrexlemgt0.lim	. . . . . . 7 ⊢ (𝜑 → ∀𝑒 ∈ ℝ⁺ ∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ_≥‘𝑗)((𝐹‘𝑖) < (𝐿 + 𝑒) ∧ 𝐿 < ((𝐹‘𝑖) + 𝑒)))
8	7	adantr 276	. . . . . 6 ⊢ ((𝜑 ∧ (𝐹‘𝐾) < 𝐿) → ∀𝑒 ∈ ℝ⁺ ∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ_≥‘𝑗)((𝐹‘𝑖) < (𝐿 + 𝑒) ∧ 𝐿 < ((𝐹‘𝑖) + 𝑒)))
9		resqrexlemex.seq	. . . . . . . . . . 11 ⊢ 𝐹 = seq1((𝑦 ∈ ℝ⁺, 𝑧 ∈ ℝ⁺ ↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)}))
10		resqrexlemex.a	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ ℝ)
11		resqrexlemex.agt0	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ≤ 𝐴)
12	9, 10, 11	resqrexlemf 11000	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:ℕ⟶ℝ⁺)
13		resqrexlemoverl.k	. . . . . . . . . 10 ⊢ (𝜑 → 𝐾 ∈ ℕ)
14	12, 13	ffvelcdmd 5648	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘𝐾) ∈ ℝ⁺)
15	14	rpred 9683	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘𝐾) ∈ ℝ)
16		resqrexlemgt0.rr	. . . . . . . 8 ⊢ (𝜑 → 𝐿 ∈ ℝ)
17		difrp 9679	. . . . . . . 8 ⊢ (((𝐹‘𝐾) ∈ ℝ ∧ 𝐿 ∈ ℝ) → ((𝐹‘𝐾) < 𝐿 ↔ (𝐿 − (𝐹‘𝐾)) ∈ ℝ⁺))
18	15, 16, 17	syl2anc 411	. . . . . . 7 ⊢ (𝜑 → ((𝐹‘𝐾) < 𝐿 ↔ (𝐿 − (𝐹‘𝐾)) ∈ ℝ⁺))
19	18	biimpa 296	. . . . . 6 ⊢ ((𝜑 ∧ (𝐹‘𝐾) < 𝐿) → (𝐿 − (𝐹‘𝐾)) ∈ ℝ⁺)
20	6, 8, 19	rspcdva 2846	. . . . 5 ⊢ ((𝜑 ∧ (𝐹‘𝐾) < 𝐿) → ∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ_≥‘𝑗)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))
21		fveq2 5511	. . . . . . 7 ⊢ (𝑗 = 𝑏 → (ℤ_≥‘𝑗) = (ℤ_≥‘𝑏))
22	21	raleqdv 2678	. . . . . 6 ⊢ (𝑗 = 𝑏 → (∀𝑖 ∈ (ℤ_≥‘𝑗)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))) ↔ ∀𝑖 ∈ (ℤ_≥‘𝑏)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾))))))
23	22	cbvrexv 2704	. . . . 5 ⊢ (∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ_≥‘𝑗)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))) ↔ ∃𝑏 ∈ ℕ ∀𝑖 ∈ (ℤ_≥‘𝑏)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))
24	20, 23	sylib 122	. . . 4 ⊢ ((𝜑 ∧ (𝐹‘𝐾) < 𝐿) → ∃𝑏 ∈ ℕ ∀𝑖 ∈ (ℤ_≥‘𝑏)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))
25		fveq2 5511	. . . . . . . . . . 11 ⊢ (𝑖 = 𝐾 → (𝐹‘𝑖) = (𝐹‘𝐾))
26	25	breq1d 4010	. . . . . . . . . 10 ⊢ (𝑖 = 𝐾 → ((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ↔ (𝐹‘𝐾) < (𝐿 + (𝐿 − (𝐹‘𝐾)))))
27	25	oveq1d 5884	. . . . . . . . . . 11 ⊢ (𝑖 = 𝐾 → ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾))) = ((𝐹‘𝐾) + (𝐿 − (𝐹‘𝐾))))
28	27	breq2d 4012	. . . . . . . . . 10 ⊢ (𝑖 = 𝐾 → (𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾))) ↔ 𝐿 < ((𝐹‘𝐾) + (𝐿 − (𝐹‘𝐾)))))
29	26, 28	anbi12d 473	. . . . . . . . 9 ⊢ (𝑖 = 𝐾 → (((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))) ↔ ((𝐹‘𝐾) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝐾) + (𝐿 − (𝐹‘𝐾))))))
30		simprr 531	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐹‘𝐾) < 𝐿) ∧ (𝑏 ∈ ℕ ∧ ∀𝑖 ∈ (ℤ_≥‘𝑏)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))) → ∀𝑖 ∈ (ℤ_≥‘𝑏)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))
31	30	adantr 276	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝐹‘𝐾) < 𝐿) ∧ (𝑏 ∈ ℕ ∧ ∀𝑖 ∈ (ℤ_≥‘𝑏)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))) ∧ 𝑏 ≤ 𝐾) → ∀𝑖 ∈ (ℤ_≥‘𝑏)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))
32		simprl 529	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐹‘𝐾) < 𝐿) ∧ (𝑏 ∈ ℕ ∧ ∀𝑖 ∈ (ℤ_≥‘𝑏)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))) → 𝑏 ∈ ℕ)
33	32	nnzd 9363	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐹‘𝐾) < 𝐿) ∧ (𝑏 ∈ ℕ ∧ ∀𝑖 ∈ (ℤ_≥‘𝑏)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))) → 𝑏 ∈ ℤ)
34	33	adantr 276	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝐹‘𝐾) < 𝐿) ∧ (𝑏 ∈ ℕ ∧ ∀𝑖 ∈ (ℤ_≥‘𝑏)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))) ∧ 𝑏 ≤ 𝐾) → 𝑏 ∈ ℤ)
35	13	ad2antrr 488	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐹‘𝐾) < 𝐿) ∧ (𝑏 ∈ ℕ ∧ ∀𝑖 ∈ (ℤ_≥‘𝑏)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))) → 𝐾 ∈ ℕ)
36	35	nnzd 9363	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐹‘𝐾) < 𝐿) ∧ (𝑏 ∈ ℕ ∧ ∀𝑖 ∈ (ℤ_≥‘𝑏)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))) → 𝐾 ∈ ℤ)
37	36	adantr 276	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝐹‘𝐾) < 𝐿) ∧ (𝑏 ∈ ℕ ∧ ∀𝑖 ∈ (ℤ_≥‘𝑏)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))) ∧ 𝑏 ≤ 𝐾) → 𝐾 ∈ ℤ)
38		simpr 110	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝐹‘𝐾) < 𝐿) ∧ (𝑏 ∈ ℕ ∧ ∀𝑖 ∈ (ℤ_≥‘𝑏)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))) ∧ 𝑏 ≤ 𝐾) → 𝑏 ≤ 𝐾)
39		eluz2 9523	. . . . . . . . . 10 ⊢ (𝐾 ∈ (ℤ_≥‘𝑏) ↔ (𝑏 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑏 ≤ 𝐾))
40	34, 37, 38, 39	syl3anbrc 1181	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝐹‘𝐾) < 𝐿) ∧ (𝑏 ∈ ℕ ∧ ∀𝑖 ∈ (ℤ_≥‘𝑏)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))) ∧ 𝑏 ≤ 𝐾) → 𝐾 ∈ (ℤ_≥‘𝑏))
41	29, 31, 40	rspcdva 2846	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝐹‘𝐾) < 𝐿) ∧ (𝑏 ∈ ℕ ∧ ∀𝑖 ∈ (ℤ_≥‘𝑏)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))) ∧ 𝑏 ≤ 𝐾) → ((𝐹‘𝐾) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝐾) + (𝐿 − (𝐹‘𝐾)))))
42	41	simprd 114	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝐹‘𝐾) < 𝐿) ∧ (𝑏 ∈ ℕ ∧ ∀𝑖 ∈ (ℤ_≥‘𝑏)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))) ∧ 𝑏 ≤ 𝐾) → 𝐿 < ((𝐹‘𝐾) + (𝐿 − (𝐹‘𝐾))))
43	14	ad2antrr 488	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐹‘𝐾) < 𝐿) ∧ (𝑏 ∈ ℕ ∧ ∀𝑖 ∈ (ℤ_≥‘𝑏)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))) → (𝐹‘𝐾) ∈ ℝ⁺)
44	43	rpcnd 9685	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐹‘𝐾) < 𝐿) ∧ (𝑏 ∈ ℕ ∧ ∀𝑖 ∈ (ℤ_≥‘𝑏)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))) → (𝐹‘𝐾) ∈ ℂ)
45	44	adantr 276	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝐹‘𝐾) < 𝐿) ∧ (𝑏 ∈ ℕ ∧ ∀𝑖 ∈ (ℤ_≥‘𝑏)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))) ∧ 𝑏 ≤ 𝐾) → (𝐹‘𝐾) ∈ ℂ)
46	16	ad2antrr 488	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐹‘𝐾) < 𝐿) ∧ (𝑏 ∈ ℕ ∧ ∀𝑖 ∈ (ℤ_≥‘𝑏)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))) → 𝐿 ∈ ℝ)
47	46	recnd 7976	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐹‘𝐾) < 𝐿) ∧ (𝑏 ∈ ℕ ∧ ∀𝑖 ∈ (ℤ_≥‘𝑏)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))) → 𝐿 ∈ ℂ)
48	47	adantr 276	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝐹‘𝐾) < 𝐿) ∧ (𝑏 ∈ ℕ ∧ ∀𝑖 ∈ (ℤ_≥‘𝑏)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))) ∧ 𝑏 ≤ 𝐾) → 𝐿 ∈ ℂ)
49	45, 48	pncan3d 8261	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝐹‘𝐾) < 𝐿) ∧ (𝑏 ∈ ℕ ∧ ∀𝑖 ∈ (ℤ_≥‘𝑏)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))) ∧ 𝑏 ≤ 𝐾) → ((𝐹‘𝐾) + (𝐿 − (𝐹‘𝐾))) = 𝐿)
50	42, 49	breqtrd 4026	. . . . . 6 ⊢ ((((𝜑 ∧ (𝐹‘𝐾) < 𝐿) ∧ (𝑏 ∈ ℕ ∧ ∀𝑖 ∈ (ℤ_≥‘𝑏)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))) ∧ 𝑏 ≤ 𝐾) → 𝐿 < 𝐿)
51	16	ad3antrrr 492	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝐹‘𝐾) < 𝐿) ∧ (𝑏 ∈ ℕ ∧ ∀𝑖 ∈ (ℤ_≥‘𝑏)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))) ∧ 𝑏 ≤ 𝐾) → 𝐿 ∈ ℝ)
52	51	ltnrd 8059	. . . . . 6 ⊢ ((((𝜑 ∧ (𝐹‘𝐾) < 𝐿) ∧ (𝑏 ∈ ℕ ∧ ∀𝑖 ∈ (ℤ_≥‘𝑏)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))) ∧ 𝑏 ≤ 𝐾) → ¬ 𝐿 < 𝐿)
53	50, 52	pm2.21fal 1373	. . . . 5 ⊢ ((((𝜑 ∧ (𝐹‘𝐾) < 𝐿) ∧ (𝑏 ∈ ℕ ∧ ∀𝑖 ∈ (ℤ_≥‘𝑏)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))) ∧ 𝑏 ≤ 𝐾) → ⊥)
54	10	ad3antrrr 492	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝐹‘𝐾) < 𝐿) ∧ (𝑏 ∈ ℕ ∧ ∀𝑖 ∈ (ℤ_≥‘𝑏)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))) ∧ 𝐾 < 𝑏) → 𝐴 ∈ ℝ)
55	11	ad3antrrr 492	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝐹‘𝐾) < 𝐿) ∧ (𝑏 ∈ ℕ ∧ ∀𝑖 ∈ (ℤ_≥‘𝑏)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))) ∧ 𝐾 < 𝑏) → 0 ≤ 𝐴)
56	13	ad3antrrr 492	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝐹‘𝐾) < 𝐿) ∧ (𝑏 ∈ ℕ ∧ ∀𝑖 ∈ (ℤ_≥‘𝑏)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))) ∧ 𝐾 < 𝑏) → 𝐾 ∈ ℕ)
57	32	adantr 276	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝐹‘𝐾) < 𝐿) ∧ (𝑏 ∈ ℕ ∧ ∀𝑖 ∈ (ℤ_≥‘𝑏)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))) ∧ 𝐾 < 𝑏) → 𝑏 ∈ ℕ)
58		simpr 110	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝐹‘𝐾) < 𝐿) ∧ (𝑏 ∈ ℕ ∧ ∀𝑖 ∈ (ℤ_≥‘𝑏)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))) ∧ 𝐾 < 𝑏) → 𝐾 < 𝑏)
59	9, 54, 55, 56, 57, 58	resqrexlemdecn 11005	. . . . . 6 ⊢ ((((𝜑 ∧ (𝐹‘𝐾) < 𝐿) ∧ (𝑏 ∈ ℕ ∧ ∀𝑖 ∈ (ℤ_≥‘𝑏)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))) ∧ 𝐾 < 𝑏) → (𝐹‘𝑏) < (𝐹‘𝐾))
60	15	ad3antrrr 492	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝐹‘𝐾) < 𝐿) ∧ (𝑏 ∈ ℕ ∧ ∀𝑖 ∈ (ℤ_≥‘𝑏)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))) ∧ 𝐾 < 𝑏) → (𝐹‘𝐾) ∈ ℝ)
61	12	ad2antrr 488	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐹‘𝐾) < 𝐿) ∧ (𝑏 ∈ ℕ ∧ ∀𝑖 ∈ (ℤ_≥‘𝑏)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))) → 𝐹:ℕ⟶ℝ⁺)
62	61, 32	ffvelcdmd 5648	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐹‘𝐾) < 𝐿) ∧ (𝑏 ∈ ℕ ∧ ∀𝑖 ∈ (ℤ_≥‘𝑏)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))) → (𝐹‘𝑏) ∈ ℝ⁺)
63	62	rpred 9683	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝐹‘𝐾) < 𝐿) ∧ (𝑏 ∈ ℕ ∧ ∀𝑖 ∈ (ℤ_≥‘𝑏)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))) → (𝐹‘𝑏) ∈ ℝ)
64	63	adantr 276	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝐹‘𝐾) < 𝐿) ∧ (𝑏 ∈ ℕ ∧ ∀𝑖 ∈ (ℤ_≥‘𝑏)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))) ∧ 𝐾 < 𝑏) → (𝐹‘𝑏) ∈ ℝ)
65		fveq2 5511	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑏 → (𝐹‘𝑖) = (𝐹‘𝑏))
66	65	breq1d 4010	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑏 → ((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ↔ (𝐹‘𝑏) < (𝐿 + (𝐿 − (𝐹‘𝐾)))))
67	65	oveq1d 5884	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑏 → ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾))) = ((𝐹‘𝑏) + (𝐿 − (𝐹‘𝐾))))
68	67	breq2d 4012	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑏 → (𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾))) ↔ 𝐿 < ((𝐹‘𝑏) + (𝐿 − (𝐹‘𝐾)))))
69	66, 68	anbi12d 473	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑏 → (((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))) ↔ ((𝐹‘𝑏) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑏) + (𝐿 − (𝐹‘𝐾))))))
70		uzid 9531	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ ℤ → 𝑏 ∈ (ℤ_≥‘𝑏))
71	33, 70	syl 14	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐹‘𝐾) < 𝐿) ∧ (𝑏 ∈ ℕ ∧ ∀𝑖 ∈ (ℤ_≥‘𝑏)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))) → 𝑏 ∈ (ℤ_≥‘𝑏))
72	69, 30, 71	rspcdva 2846	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐹‘𝐾) < 𝐿) ∧ (𝑏 ∈ ℕ ∧ ∀𝑖 ∈ (ℤ_≥‘𝑏)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))) → ((𝐹‘𝑏) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑏) + (𝐿 − (𝐹‘𝐾)))))
73	72	simprd 114	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐹‘𝐾) < 𝐿) ∧ (𝑏 ∈ ℕ ∧ ∀𝑖 ∈ (ℤ_≥‘𝑏)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))) → 𝐿 < ((𝐹‘𝑏) + (𝐿 − (𝐹‘𝐾))))
74	62	rpcnd 9685	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐹‘𝐾) < 𝐿) ∧ (𝑏 ∈ ℕ ∧ ∀𝑖 ∈ (ℤ_≥‘𝑏)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))) → (𝐹‘𝑏) ∈ ℂ)
75	74, 47, 44	addsubassd 8278	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐹‘𝐾) < 𝐿) ∧ (𝑏 ∈ ℕ ∧ ∀𝑖 ∈ (ℤ_≥‘𝑏)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))) → (((𝐹‘𝑏) + 𝐿) − (𝐹‘𝐾)) = ((𝐹‘𝑏) + (𝐿 − (𝐹‘𝐾))))
76	73, 75	breqtrrd 4028	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐹‘𝐾) < 𝐿) ∧ (𝑏 ∈ ℕ ∧ ∀𝑖 ∈ (ℤ_≥‘𝑏)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))) → 𝐿 < (((𝐹‘𝑏) + 𝐿) − (𝐹‘𝐾)))
77	15	ad2antrr 488	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐹‘𝐾) < 𝐿) ∧ (𝑏 ∈ ℕ ∧ ∀𝑖 ∈ (ℤ_≥‘𝑏)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))) → (𝐹‘𝐾) ∈ ℝ)
78	63, 46	readdcld 7977	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐹‘𝐾) < 𝐿) ∧ (𝑏 ∈ ℕ ∧ ∀𝑖 ∈ (ℤ_≥‘𝑏)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))) → ((𝐹‘𝑏) + 𝐿) ∈ ℝ)
79	77, 46, 78	ltaddsub2d 8493	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐹‘𝐾) < 𝐿) ∧ (𝑏 ∈ ℕ ∧ ∀𝑖 ∈ (ℤ_≥‘𝑏)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))) → (((𝐹‘𝐾) + 𝐿) < ((𝐹‘𝑏) + 𝐿) ↔ 𝐿 < (((𝐹‘𝑏) + 𝐿) − (𝐹‘𝐾))))
80	76, 79	mpbird 167	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐹‘𝐾) < 𝐿) ∧ (𝑏 ∈ ℕ ∧ ∀𝑖 ∈ (ℤ_≥‘𝑏)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))) → ((𝐹‘𝐾) + 𝐿) < ((𝐹‘𝑏) + 𝐿))
81	77, 63, 46	ltadd1d 8485	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐹‘𝐾) < 𝐿) ∧ (𝑏 ∈ ℕ ∧ ∀𝑖 ∈ (ℤ_≥‘𝑏)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))) → ((𝐹‘𝐾) < (𝐹‘𝑏) ↔ ((𝐹‘𝐾) + 𝐿) < ((𝐹‘𝑏) + 𝐿)))
82	80, 81	mpbird 167	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝐹‘𝐾) < 𝐿) ∧ (𝑏 ∈ ℕ ∧ ∀𝑖 ∈ (ℤ_≥‘𝑏)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))) → (𝐹‘𝐾) < (𝐹‘𝑏))
83	82	adantr 276	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝐹‘𝐾) < 𝐿) ∧ (𝑏 ∈ ℕ ∧ ∀𝑖 ∈ (ℤ_≥‘𝑏)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))) ∧ 𝐾 < 𝑏) → (𝐹‘𝐾) < (𝐹‘𝑏))
84	60, 64, 83	ltnsymd 8067	. . . . . 6 ⊢ ((((𝜑 ∧ (𝐹‘𝐾) < 𝐿) ∧ (𝑏 ∈ ℕ ∧ ∀𝑖 ∈ (ℤ_≥‘𝑏)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))) ∧ 𝐾 < 𝑏) → ¬ (𝐹‘𝑏) < (𝐹‘𝐾))
85	59, 84	pm2.21fal 1373	. . . . 5 ⊢ ((((𝜑 ∧ (𝐹‘𝐾) < 𝐿) ∧ (𝑏 ∈ ℕ ∧ ∀𝑖 ∈ (ℤ_≥‘𝑏)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))) ∧ 𝐾 < 𝑏) → ⊥)
86		zlelttric 9287	. . . . . 6 ⊢ ((𝑏 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑏 ≤ 𝐾 ∨ 𝐾 < 𝑏))
87	33, 36, 86	syl2anc 411	. . . . 5 ⊢ (((𝜑 ∧ (𝐹‘𝐾) < 𝐿) ∧ (𝑏 ∈ ℕ ∧ ∀𝑖 ∈ (ℤ_≥‘𝑏)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))) → (𝑏 ≤ 𝐾 ∨ 𝐾 < 𝑏))
88	53, 85, 87	mpjaodan 798	. . . 4 ⊢ (((𝜑 ∧ (𝐹‘𝐾) < 𝐿) ∧ (𝑏 ∈ ℕ ∧ ∀𝑖 ∈ (ℤ_≥‘𝑏)((𝐹‘𝑖) < (𝐿 + (𝐿 − (𝐹‘𝐾))) ∧ 𝐿 < ((𝐹‘𝑖) + (𝐿 − (𝐹‘𝐾)))))) → ⊥)
89	24, 88	rexlimddv 2599	. . 3 ⊢ ((𝜑 ∧ (𝐹‘𝐾) < 𝐿) → ⊥)
90	89	inegd 1372	. 2 ⊢ (𝜑 → ¬ (𝐹‘𝐾) < 𝐿)
91	16, 15	lenltd 8065	. 2 ⊢ (𝜑 → (𝐿 ≤ (𝐹‘𝐾) ↔ ¬ (𝐹‘𝐾) < 𝐿))
92	90, 91	mpbird 167	1 ⊢ (𝜑 → 𝐿 ≤ (𝐹‘𝐾))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 708 = wceq 1353 ⊥wfal 1358 ∈ wcel 2148 ∀wral 2455 ∃wrex 2456 {csn 3591 class class class wbr 4000 × cxp 4621 ⟶wf 5208 ‘cfv 5212 (class class class)co 5869 ∈ cmpo 5871 ℂcc 7800 ℝcr 7801 0cc0 7802 1c1 7803 + caddc 7805 < clt 7982 ≤ cle 7983 − cmin 8118 / cdiv 8618 ℕcn 8908 2c2 8959 ℤcz 9242 ℤ_≥cuz 9517 ℝ⁺crp 9640 seqcseq 10431

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 614 ax-in2 615 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-13 2150 ax-14 2151 ax-ext 2159 ax-coll 4115 ax-sep 4118 ax-nul 4126 ax-pow 4171 ax-pr 4206 ax-un 4430 ax-setind 4533 ax-iinf 4584 ax-cnex 7893 ax-resscn 7894 ax-1cn 7895 ax-1re 7896 ax-icn 7897 ax-addcl 7898 ax-addrcl 7899 ax-mulcl 7900 ax-mulrcl 7901 ax-addcom 7902 ax-mulcom 7903 ax-addass 7904 ax-mulass 7905 ax-distr 7906 ax-i2m1 7907 ax-0lt1 7908 ax-1rid 7909 ax-0id 7910 ax-rnegex 7911 ax-precex 7912 ax-cnre 7913 ax-pre-ltirr 7914 ax-pre-ltwlin 7915 ax-pre-lttrn 7916 ax-pre-apti 7917 ax-pre-ltadd 7918 ax-pre-mulgt0 7919 ax-pre-mulext 7920

This theorem depends on definitions: df-bi 117 df-dc 835 df-3or 979 df-3an 980 df-tru 1356 df-fal 1359 df-nf 1461 df-sb 1763 df-eu 2029 df-mo 2030 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ne 2348 df-nel 2443 df-ral 2460 df-rex 2461 df-reu 2462 df-rmo 2463 df-rab 2464 df-v 2739 df-sbc 2963 df-csb 3058 df-dif 3131 df-un 3133 df-in 3135 df-ss 3142 df-nul 3423 df-if 3535 df-pw 3576 df-sn 3597 df-pr 3598 df-op 3600 df-uni 3808 df-int 3843 df-iun 3886 df-br 4001 df-opab 4062 df-mpt 4063 df-tr 4099 df-id 4290 df-po 4293 df-iso 4294 df-iord 4363 df-on 4365 df-ilim 4366 df-suc 4368 df-iom 4587 df-xp 4629 df-rel 4630 df-cnv 4631 df-co 4632 df-dm 4633 df-rn 4634 df-res 4635 df-ima 4636 df-iota 5174 df-fun 5214 df-fn 5215 df-f 5216 df-f1 5217 df-fo 5218 df-f1o 5219 df-fv 5220 df-riota 5825 df-ov 5872 df-oprab 5873 df-mpo 5874 df-1st 6135 df-2nd 6136 df-recs 6300 df-frec 6386 df-pnf 7984 df-mnf 7985 df-xr 7986 df-ltxr 7987 df-le 7988 df-sub 8120 df-neg 8121 df-reap 8522 df-ap 8529 df-div 8619 df-inn 8909 df-2 8967 df-3 8968 df-4 8969 df-n0 9166 df-z 9243 df-uz 9518 df-rp 9641 df-seqfrec 10432 df-exp 10506

This theorem is referenced by: resqrexlemglsq 11015

W3C validator