Metamath Proof Explorer

Theorem opsqrlem4

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

Ref Expression
Hypotheses opsqrlem2.1 ⊢ 𝑇 ∈ HrmOp
opsqrlem2.2 ⊢ 𝑆 = ( 𝑥 ∈ HrmOp , 𝑦 ∈ HrmOp ↦ ( 𝑥 +op ( ( 1 / 2 ) ·op ( 𝑇 −op ( 𝑥 ∘ 𝑥 ) ) ) ) )
opsqrlem2.3 ⊢ 𝐹 = seq 1 ( 𝑆 , ( ℕ × { 0hop } ) )
Assertion opsqrlem4 𝐹 : ℕ ⟶ HrmOp

Proof

Step Hyp Ref Expression
1 opsqrlem2.1 ⊢ 𝑇 ∈ HrmOp
2 opsqrlem2.2 ⊢ 𝑆 = ( 𝑥 ∈ HrmOp , 𝑦 ∈ HrmOp ↦ ( 𝑥 +op ( ( 1 / 2 ) ·op ( 𝑇 −op ( 𝑥 ∘ 𝑥 ) ) ) ) )
3 opsqrlem2.3 ⊢ 𝐹 = seq 1 ( 𝑆 , ( ℕ × { 0hop } ) )
4 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
5 1zzd ⊢ ( ⊤ → 1 ∈ ℤ )
6 0hmop ⊢ 0hop ∈ HrmOp
7 6 elexi ⊢ 0hop ∈ V
8 7 fvconst2 ⊢ ( 𝑧 ∈ ℕ → ( ( ℕ × { 0hop } ) ‘ 𝑧 ) = 0hop )
9 8 6 eqeltrdi ⊢ ( 𝑧 ∈ ℕ → ( ( ℕ × { 0hop } ) ‘ 𝑧 ) ∈ HrmOp )
10 9 adantl ⊢ ( ( ⊤ ∧ 𝑧 ∈ ℕ ) → ( ( ℕ × { 0hop } ) ‘ 𝑧 ) ∈ HrmOp )
11 1 2 3 opsqrlem3 ⊢ ( ( 𝑧 ∈ HrmOp ∧ 𝑤 ∈ HrmOp ) → ( 𝑧 𝑆 𝑤 ) = ( 𝑧 +op ( ( 1 / 2 ) ·op ( 𝑇 −op ( 𝑧 ∘ 𝑧 ) ) ) ) )
12 halfre ⊢ ( 1 / 2 ) ∈ ℝ
13 simpl ⊢ ( ( 𝑧 ∈ HrmOp ∧ 𝑤 ∈ HrmOp ) → 𝑧 ∈ HrmOp )
14 eqidd ⊢ ( ( 𝑧 ∈ HrmOp ∧ 𝑤 ∈ HrmOp ) → ( 𝑧 ∘ 𝑧 ) = ( 𝑧 ∘ 𝑧 ) )
15 hmopco ⊢ ( ( 𝑧 ∈ HrmOp ∧ 𝑧 ∈ HrmOp ∧ ( 𝑧 ∘ 𝑧 ) = ( 𝑧 ∘ 𝑧 ) ) → ( 𝑧 ∘ 𝑧 ) ∈ HrmOp )
16 13 13 14 15 syl3anc ⊢ ( ( 𝑧 ∈ HrmOp ∧ 𝑤 ∈ HrmOp ) → ( 𝑧 ∘ 𝑧 ) ∈ HrmOp )
17 hmopd ⊢ ( ( 𝑇 ∈ HrmOp ∧ ( 𝑧 ∘ 𝑧 ) ∈ HrmOp ) → ( 𝑇 −op ( 𝑧 ∘ 𝑧 ) ) ∈ HrmOp )
18 1 16 17 sylancr ⊢ ( ( 𝑧 ∈ HrmOp ∧ 𝑤 ∈ HrmOp ) → ( 𝑇 −op ( 𝑧 ∘ 𝑧 ) ) ∈ HrmOp )
19 hmopm ⊢ ( ( ( 1 / 2 ) ∈ ℝ ∧ ( 𝑇 −op ( 𝑧 ∘ 𝑧 ) ) ∈ HrmOp ) → ( ( 1 / 2 ) ·op ( 𝑇 −op ( 𝑧 ∘ 𝑧 ) ) ) ∈ HrmOp )
20 12 18 19 sylancr ⊢ ( ( 𝑧 ∈ HrmOp ∧ 𝑤 ∈ HrmOp ) → ( ( 1 / 2 ) ·op ( 𝑇 −op ( 𝑧 ∘ 𝑧 ) ) ) ∈ HrmOp )
21 hmops ⊢ ( ( 𝑧 ∈ HrmOp ∧ ( ( 1 / 2 ) ·op ( 𝑇 −op ( 𝑧 ∘ 𝑧 ) ) ) ∈ HrmOp ) → ( 𝑧 +op ( ( 1 / 2 ) ·op ( 𝑇 −op ( 𝑧 ∘ 𝑧 ) ) ) ) ∈ HrmOp )
22 20 21 syldan ⊢ ( ( 𝑧 ∈ HrmOp ∧ 𝑤 ∈ HrmOp ) → ( 𝑧 +op ( ( 1 / 2 ) ·op ( 𝑇 −op ( 𝑧 ∘ 𝑧 ) ) ) ) ∈ HrmOp )
23 11 22 eqeltrd ⊢ ( ( 𝑧 ∈ HrmOp ∧ 𝑤 ∈ HrmOp ) → ( 𝑧 𝑆 𝑤 ) ∈ HrmOp )
24 23 adantl ⊢ ( ( ⊤ ∧ ( 𝑧 ∈ HrmOp ∧ 𝑤 ∈ HrmOp ) ) → ( 𝑧 𝑆 𝑤 ) ∈ HrmOp )
25 4 5 10 24 seqf ⊢ ( ⊤ → seq 1 ( 𝑆 , ( ℕ × { 0hop } ) ) : ℕ ⟶ HrmOp )
26 25 mptru ⊢ seq 1 ( 𝑆 , ( ℕ × { 0hop } ) ) : ℕ ⟶ HrmOp
27 3 feq1i ⊢ ( 𝐹 : ℕ ⟶ HrmOp ↔ seq 1 ( 𝑆 , ( ℕ × { 0hop } ) ) : ℕ ⟶ HrmOp )
28 26 27 mpbir ⊢ 𝐹 : ℕ ⟶ HrmOp