Metamath Proof Explorer

Theorem opsqrlem4

Description: Lemma for opsqri . (Contributed by NM, 17-Aug-2006) (New usage is discouraged.)

Ref Expression
Hypotheses opsqrlem2.1 ⊢ T ∈ HrmOp
opsqrlem2.2 ⊢ S = x ∈ HrmOp , y ∈ HrmOp ⟼ x + op 1 2 · op T - op x ∘ x
opsqrlem2.3 ⊢ F = seq 1 S ℕ × 0 hop
Assertion opsqrlem4 ⊢ F : ℕ ⟶ HrmOp

Proof

Step Hyp Ref Expression
1 opsqrlem2.1 ⊢ T ∈ HrmOp
2 opsqrlem2.2 ⊢ S = x ∈ HrmOp , y ∈ HrmOp ⟼ x + op 1 2 · op T - op x ∘ x
3 opsqrlem2.3 ⊢ F = seq 1 S ℕ × 0 hop
4 nnuz ⊢ ℕ = ℤ ≥ 1
5 1zzd ⊢ ⊤ → 1 ∈ ℤ
6 0hmop ⊢ 0 hop ∈ HrmOp
7 6 elexi ⊢ 0 hop ∈ V
8 7 fvconst2 ⊢ z ∈ ℕ → ℕ × 0 hop ⁡ z = 0 hop
9 8 6 eqeltrdi ⊢ z ∈ ℕ → ℕ × 0 hop ⁡ z ∈ HrmOp
10 9 adantl ⊢ ⊤ ∧ z ∈ ℕ → ℕ × 0 hop ⁡ z ∈ HrmOp
11 1 2 3 opsqrlem3 ⊢ z ∈ HrmOp ∧ w ∈ HrmOp → z S w = z + op 1 2 · op T - op z ∘ z
12 halfre ⊢ 1 2 ∈ ℝ
13 simpl ⊢ z ∈ HrmOp ∧ w ∈ HrmOp → z ∈ HrmOp
14 eqidd ⊢ z ∈ HrmOp ∧ w ∈ HrmOp → z ∘ z = z ∘ z
15 hmopco ⊢ z ∈ HrmOp ∧ z ∈ HrmOp ∧ z ∘ z = z ∘ z → z ∘ z ∈ HrmOp
16 13 13 14 15 syl3anc ⊢ z ∈ HrmOp ∧ w ∈ HrmOp → z ∘ z ∈ HrmOp
17 hmopd ⊢ T ∈ HrmOp ∧ z ∘ z ∈ HrmOp → T - op z ∘ z ∈ HrmOp
18 1 16 17 sylancr ⊢ z ∈ HrmOp ∧ w ∈ HrmOp → T - op z ∘ z ∈ HrmOp
19 hmopm ⊢ 1 2 ∈ ℝ ∧ T - op z ∘ z ∈ HrmOp → 1 2 · op T - op z ∘ z ∈ HrmOp
20 12 18 19 sylancr ⊢ z ∈ HrmOp ∧ w ∈ HrmOp → 1 2 · op T - op z ∘ z ∈ HrmOp
21 hmops ⊢ z ∈ HrmOp ∧ 1 2 · op T - op z ∘ z ∈ HrmOp → z + op 1 2 · op T - op z ∘ z ∈ HrmOp
22 20 21 syldan ⊢ z ∈ HrmOp ∧ w ∈ HrmOp → z + op 1 2 · op T - op z ∘ z ∈ HrmOp
23 11 22 eqeltrd ⊢ z ∈ HrmOp ∧ w ∈ HrmOp → z S w ∈ HrmOp
24 23 adantl ⊢ ⊤ ∧ z ∈ HrmOp ∧ w ∈ HrmOp → z S w ∈ HrmOp
25 4 5 10 24 seqf ⊢ ⊤ → seq 1 S ℕ × 0 hop : ℕ ⟶ HrmOp
26 25 mptru ⊢ seq 1 S ℕ × 0 hop : ℕ ⟶ HrmOp
27 3 feq1i ⊢ F : ℕ ⟶ HrmOp ↔ seq 1 S ℕ × 0 hop : ℕ ⟶ HrmOp
28 26 27 mpbir ⊢ F : ℕ ⟶ HrmOp