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