| Step | Hyp | Ref
| Expression |
| 1 | | fveq2 6906 |
. . 3
⊢ (𝑗 = 1 → (𝐹‘𝑗) = (𝐹‘1)) |
| 2 | 1 | breq1d 5153 |
. 2
⊢ (𝑗 = 1 → ((𝐹‘𝑗) ≤op Iop ↔
(𝐹‘1)
≤op Iop )) |
| 3 | | fveq2 6906 |
. . 3
⊢ (𝑗 = (𝑘 + 1) → (𝐹‘𝑗) = (𝐹‘(𝑘 + 1))) |
| 4 | 3 | breq1d 5153 |
. 2
⊢ (𝑗 = (𝑘 + 1) → ((𝐹‘𝑗) ≤op Iop ↔
(𝐹‘(𝑘 + 1)) ≤op
Iop )) |
| 5 | | fveq2 6906 |
. . 3
⊢ (𝑗 = 𝑁 → (𝐹‘𝑗) = (𝐹‘𝑁)) |
| 6 | 5 | breq1d 5153 |
. 2
⊢ (𝑗 = 𝑁 → ((𝐹‘𝑗) ≤op Iop ↔
(𝐹‘𝑁) ≤op Iop
)) |
| 7 | | opsqrlem2.1 |
. . . 4
⊢ 𝑇 ∈ HrmOp |
| 8 | | opsqrlem2.2 |
. . . 4
⊢ 𝑆 = (𝑥 ∈ HrmOp, 𝑦 ∈ HrmOp ↦ (𝑥 +op ((1 / 2)
·op (𝑇 −op (𝑥 ∘ 𝑥))))) |
| 9 | | opsqrlem2.3 |
. . . 4
⊢ 𝐹 = seq1(𝑆, (ℕ × { 0hop
})) |
| 10 | 7, 8, 9 | opsqrlem2 32160 |
. . 3
⊢ (𝐹‘1) =
0hop |
| 11 | | idleop 32150 |
. . 3
⊢
0hop ≤op Iop |
| 12 | 10, 11 | eqbrtri 5164 |
. 2
⊢ (𝐹‘1) ≤op
Iop |
| 13 | | idhmop 32001 |
. . . . . . . 8
⊢
Iop ∈ HrmOp |
| 14 | 7, 8, 9 | opsqrlem4 32162 |
. . . . . . . . 9
⊢ 𝐹:ℕ⟶HrmOp |
| 15 | 14 | ffvelcdmi 7103 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → (𝐹‘𝑘) ∈ HrmOp) |
| 16 | | hmopd 32041 |
. . . . . . . 8
⊢ ((
Iop ∈ HrmOp ∧ (𝐹‘𝑘) ∈ HrmOp) → ( Iop
−op (𝐹‘𝑘)) ∈ HrmOp) |
| 17 | 13, 15, 16 | sylancr 587 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ → (
Iop −op (𝐹‘𝑘)) ∈ HrmOp) |
| 18 | | eqid 2737 |
. . . . . . . 8
⊢ ((
Iop −op (𝐹‘𝑘)) ∘ ( Iop
−op (𝐹‘𝑘))) = (( Iop −op
(𝐹‘𝑘)) ∘ ( Iop
−op (𝐹‘𝑘))) |
| 19 | | hmopco 32042 |
. . . . . . . 8
⊢ (((
Iop −op (𝐹‘𝑘)) ∈ HrmOp ∧ ( Iop
−op (𝐹‘𝑘)) ∈ HrmOp ∧ (( Iop
−op (𝐹‘𝑘)) ∘ ( Iop
−op (𝐹‘𝑘))) = (( Iop −op
(𝐹‘𝑘)) ∘ ( Iop
−op (𝐹‘𝑘)))) → (( Iop
−op (𝐹‘𝑘)) ∘ ( Iop
−op (𝐹‘𝑘))) ∈ HrmOp) |
| 20 | 18, 19 | mp3an3 1452 |
. . . . . . 7
⊢ (((
Iop −op (𝐹‘𝑘)) ∈ HrmOp ∧ ( Iop
−op (𝐹‘𝑘)) ∈ HrmOp) → (( Iop
−op (𝐹‘𝑘)) ∘ ( Iop
−op (𝐹‘𝑘))) ∈ HrmOp) |
| 21 | 17, 17, 20 | syl2anc 584 |
. . . . . 6
⊢ (𝑘 ∈ ℕ → ((
Iop −op (𝐹‘𝑘)) ∘ ( Iop
−op (𝐹‘𝑘))) ∈ HrmOp) |
| 22 | | leopsq 32148 |
. . . . . . 7
⊢ ((
Iop −op (𝐹‘𝑘)) ∈ HrmOp → 0hop
≤op (( Iop −op (𝐹‘𝑘)) ∘ ( Iop
−op (𝐹‘𝑘)))) |
| 23 | 17, 22 | syl 17 |
. . . . . 6
⊢ (𝑘 ∈ ℕ →
0hop ≤op (( Iop −op (𝐹‘𝑘)) ∘ ( Iop
−op (𝐹‘𝑘)))) |
| 24 | | opsqrlem6.4 |
. . . . . . . 8
⊢ 𝑇 ≤op
Iop |
| 25 | | leop3 32144 |
. . . . . . . . 9
⊢ ((𝑇 ∈ HrmOp ∧
Iop ∈ HrmOp) → (𝑇 ≤op Iop ↔
0hop ≤op ( Iop −op 𝑇))) |
| 26 | 7, 13, 25 | mp2an 692 |
. . . . . . . 8
⊢ (𝑇 ≤op
Iop ↔ 0hop ≤op ( Iop
−op 𝑇)) |
| 27 | 24, 26 | mpbi 230 |
. . . . . . 7
⊢
0hop ≤op ( Iop −op 𝑇) |
| 28 | | hmopd 32041 |
. . . . . . . . 9
⊢ ((
Iop ∈ HrmOp ∧ 𝑇 ∈ HrmOp) → ( Iop
−op 𝑇)
∈ HrmOp) |
| 29 | 13, 7, 28 | mp2an 692 |
. . . . . . . 8
⊢ (
Iop −op 𝑇) ∈ HrmOp |
| 30 | | leopadd 32151 |
. . . . . . . 8
⊢ (((((
Iop −op (𝐹‘𝑘)) ∘ ( Iop
−op (𝐹‘𝑘))) ∈ HrmOp ∧ ( Iop
−op 𝑇)
∈ HrmOp) ∧ ( 0hop ≤op (( Iop
−op (𝐹‘𝑘)) ∘ ( Iop
−op (𝐹‘𝑘))) ∧ 0hop ≤op (
Iop −op 𝑇))) → 0hop ≤op
((( Iop −op (𝐹‘𝑘)) ∘ ( Iop
−op (𝐹‘𝑘))) +op ( Iop
−op 𝑇))) |
| 31 | 29, 30 | mpanl2 701 |
. . . . . . 7
⊢ ((((
Iop −op (𝐹‘𝑘)) ∘ ( Iop
−op (𝐹‘𝑘))) ∈ HrmOp ∧ ( 0hop
≤op (( Iop −op (𝐹‘𝑘)) ∘ ( Iop
−op (𝐹‘𝑘))) ∧ 0hop ≤op (
Iop −op 𝑇))) → 0hop ≤op
((( Iop −op (𝐹‘𝑘)) ∘ ( Iop
−op (𝐹‘𝑘))) +op ( Iop
−op 𝑇))) |
| 32 | 27, 31 | mpanr2 704 |
. . . . . 6
⊢ ((((
Iop −op (𝐹‘𝑘)) ∘ ( Iop
−op (𝐹‘𝑘))) ∈ HrmOp ∧ 0hop
≤op (( Iop −op (𝐹‘𝑘)) ∘ ( Iop
−op (𝐹‘𝑘)))) → 0hop ≤op
((( Iop −op (𝐹‘𝑘)) ∘ ( Iop
−op (𝐹‘𝑘))) +op ( Iop
−op 𝑇))) |
| 33 | 21, 23, 32 | syl2anc 584 |
. . . . 5
⊢ (𝑘 ∈ ℕ →
0hop ≤op ((( Iop −op
(𝐹‘𝑘)) ∘ ( Iop
−op (𝐹‘𝑘))) +op ( Iop
−op 𝑇))) |
| 34 | | 2cn 12341 |
. . . . . . . . . 10
⊢ 2 ∈
ℂ |
| 35 | | hmopf 31893 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑘) ∈ HrmOp → (𝐹‘𝑘): ℋ⟶ ℋ) |
| 36 | 15, 35 | syl 17 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → (𝐹‘𝑘): ℋ⟶ ℋ) |
| 37 | | homulcl 31778 |
. . . . . . . . . 10
⊢ ((2
∈ ℂ ∧ (𝐹‘𝑘): ℋ⟶ ℋ) → (2
·op (𝐹‘𝑘)): ℋ⟶ ℋ) |
| 38 | 34, 36, 37 | sylancr 587 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → (2
·op (𝐹‘𝑘)): ℋ⟶ ℋ) |
| 39 | | hmopf 31893 |
. . . . . . . . . . 11
⊢ (𝑇 ∈ HrmOp → 𝑇: ℋ⟶
ℋ) |
| 40 | 7, 39 | ax-mp 5 |
. . . . . . . . . 10
⊢ 𝑇: ℋ⟶
ℋ |
| 41 | | fco 6760 |
. . . . . . . . . . 11
⊢ (((𝐹‘𝑘): ℋ⟶ ℋ ∧ (𝐹‘𝑘): ℋ⟶ ℋ) → ((𝐹‘𝑘) ∘ (𝐹‘𝑘)): ℋ⟶ ℋ) |
| 42 | 36, 36, 41 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → ((𝐹‘𝑘) ∘ (𝐹‘𝑘)): ℋ⟶ ℋ) |
| 43 | | hosubcl 31792 |
. . . . . . . . . 10
⊢ ((𝑇: ℋ⟶ ℋ ∧
((𝐹‘𝑘) ∘ (𝐹‘𝑘)): ℋ⟶ ℋ) → (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘))): ℋ⟶
ℋ) |
| 44 | 40, 42, 43 | sylancr 587 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘))): ℋ⟶
ℋ) |
| 45 | | hmopf 31893 |
. . . . . . . . . . . 12
⊢ (
Iop ∈ HrmOp → Iop : ℋ⟶
ℋ) |
| 46 | 13, 45 | ax-mp 5 |
. . . . . . . . . . 11
⊢
Iop : ℋ⟶ ℋ |
| 47 | | homulcl 31778 |
. . . . . . . . . . 11
⊢ ((2
∈ ℂ ∧ Iop : ℋ⟶ ℋ) → (2
·op Iop ): ℋ⟶
ℋ) |
| 48 | 34, 46, 47 | mp2an 692 |
. . . . . . . . . 10
⊢ (2
·op Iop ): ℋ⟶
ℋ |
| 49 | | hosubsub4 31837 |
. . . . . . . . . 10
⊢ (((2
·op Iop ): ℋ⟶ ℋ ∧ (2
·op (𝐹‘𝑘)): ℋ⟶ ℋ ∧ (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘))): ℋ⟶ ℋ) → (((2
·op Iop ) −op (2
·op (𝐹‘𝑘))) −op (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘)))) = ((2 ·op
Iop ) −op ((2 ·op (𝐹‘𝑘)) +op (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘)))))) |
| 50 | 48, 49 | mp3an1 1450 |
. . . . . . . . 9
⊢ (((2
·op (𝐹‘𝑘)): ℋ⟶ ℋ ∧ (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘))): ℋ⟶ ℋ) → (((2
·op Iop ) −op (2
·op (𝐹‘𝑘))) −op (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘)))) = ((2 ·op
Iop ) −op ((2 ·op (𝐹‘𝑘)) +op (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘)))))) |
| 51 | 38, 44, 50 | syl2anc 584 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → (((2
·op Iop ) −op (2
·op (𝐹‘𝑘))) −op (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘)))) = ((2 ·op
Iop ) −op ((2 ·op (𝐹‘𝑘)) +op (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘)))))) |
| 52 | | hosubcl 31792 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐹‘𝑘) ∘ (𝐹‘𝑘)): ℋ⟶ ℋ ∧ (2
·op (𝐹‘𝑘)): ℋ⟶ ℋ) → (((𝐹‘𝑘) ∘ (𝐹‘𝑘)) −op (2
·op (𝐹‘𝑘))): ℋ⟶
ℋ) |
| 53 | 42, 38, 52 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ → (((𝐹‘𝑘) ∘ (𝐹‘𝑘)) −op (2
·op (𝐹‘𝑘))): ℋ⟶
ℋ) |
| 54 | | hoadd32 31802 |
. . . . . . . . . . . . . . 15
⊢ ((
Iop : ℋ⟶ ℋ ∧ (((𝐹‘𝑘) ∘ (𝐹‘𝑘)) −op (2
·op (𝐹‘𝑘))): ℋ⟶ ℋ ∧
Iop : ℋ⟶ ℋ) → (( Iop
+op (((𝐹‘𝑘) ∘ (𝐹‘𝑘)) −op (2
·op (𝐹‘𝑘)))) +op Iop ) = ((
Iop +op Iop ) +op (((𝐹‘𝑘) ∘ (𝐹‘𝑘)) −op (2
·op (𝐹‘𝑘))))) |
| 55 | 46, 46, 54 | mp3an13 1454 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹‘𝑘) ∘ (𝐹‘𝑘)) −op (2
·op (𝐹‘𝑘))): ℋ⟶ ℋ → ((
Iop +op (((𝐹‘𝑘) ∘ (𝐹‘𝑘)) −op (2
·op (𝐹‘𝑘)))) +op Iop ) = ((
Iop +op Iop ) +op (((𝐹‘𝑘) ∘ (𝐹‘𝑘)) −op (2
·op (𝐹‘𝑘))))) |
| 56 | 53, 55 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → ((
Iop +op (((𝐹‘𝑘) ∘ (𝐹‘𝑘)) −op (2
·op (𝐹‘𝑘)))) +op Iop ) = ((
Iop +op Iop ) +op (((𝐹‘𝑘) ∘ (𝐹‘𝑘)) −op (2
·op (𝐹‘𝑘))))) |
| 57 | | ho2times 31838 |
. . . . . . . . . . . . . . 15
⊢ (
Iop : ℋ⟶ ℋ → (2 ·op
Iop ) = ( Iop +op Iop
)) |
| 58 | 46, 57 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ (2
·op Iop ) = ( Iop +op
Iop ) |
| 59 | 58 | oveq1i 7441 |
. . . . . . . . . . . . 13
⊢ ((2
·op Iop ) +op (((𝐹‘𝑘) ∘ (𝐹‘𝑘)) −op (2
·op (𝐹‘𝑘)))) = (( Iop +op
Iop ) +op (((𝐹‘𝑘) ∘ (𝐹‘𝑘)) −op (2
·op (𝐹‘𝑘)))) |
| 60 | 56, 59 | eqtr4di 2795 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → ((
Iop +op (((𝐹‘𝑘) ∘ (𝐹‘𝑘)) −op (2
·op (𝐹‘𝑘)))) +op Iop ) = ((2
·op Iop ) +op (((𝐹‘𝑘) ∘ (𝐹‘𝑘)) −op (2
·op (𝐹‘𝑘))))) |
| 61 | | hoaddsubass 31834 |
. . . . . . . . . . . . . 14
⊢ (((2
·op Iop ): ℋ⟶ ℋ ∧
((𝐹‘𝑘) ∘ (𝐹‘𝑘)): ℋ⟶ ℋ ∧ (2
·op (𝐹‘𝑘)): ℋ⟶ ℋ) → (((2
·op Iop ) +op ((𝐹‘𝑘) ∘ (𝐹‘𝑘))) −op (2
·op (𝐹‘𝑘))) = ((2 ·op
Iop ) +op (((𝐹‘𝑘) ∘ (𝐹‘𝑘)) −op (2
·op (𝐹‘𝑘))))) |
| 62 | 48, 61 | mp3an1 1450 |
. . . . . . . . . . . . 13
⊢ ((((𝐹‘𝑘) ∘ (𝐹‘𝑘)): ℋ⟶ ℋ ∧ (2
·op (𝐹‘𝑘)): ℋ⟶ ℋ) → (((2
·op Iop ) +op ((𝐹‘𝑘) ∘ (𝐹‘𝑘))) −op (2
·op (𝐹‘𝑘))) = ((2 ·op
Iop ) +op (((𝐹‘𝑘) ∘ (𝐹‘𝑘)) −op (2
·op (𝐹‘𝑘))))) |
| 63 | 42, 38, 62 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → (((2
·op Iop ) +op ((𝐹‘𝑘) ∘ (𝐹‘𝑘))) −op (2
·op (𝐹‘𝑘))) = ((2 ·op
Iop ) +op (((𝐹‘𝑘) ∘ (𝐹‘𝑘)) −op (2
·op (𝐹‘𝑘))))) |
| 64 | 60, 63 | eqtr4d 2780 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → ((
Iop +op (((𝐹‘𝑘) ∘ (𝐹‘𝑘)) −op (2
·op (𝐹‘𝑘)))) +op Iop ) = (((2
·op Iop ) +op ((𝐹‘𝑘) ∘ (𝐹‘𝑘))) −op (2
·op (𝐹‘𝑘)))) |
| 65 | 64 | oveq1d 7446 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → (((
Iop +op (((𝐹‘𝑘) ∘ (𝐹‘𝑘)) −op (2
·op (𝐹‘𝑘)))) +op Iop )
−op 𝑇) =
((((2 ·op Iop ) +op ((𝐹‘𝑘) ∘ (𝐹‘𝑘))) −op (2
·op (𝐹‘𝑘))) −op 𝑇)) |
| 66 | | hoaddcl 31777 |
. . . . . . . . . . . 12
⊢ ((
Iop : ℋ⟶ ℋ ∧ (((𝐹‘𝑘) ∘ (𝐹‘𝑘)) −op (2
·op (𝐹‘𝑘))): ℋ⟶ ℋ) → (
Iop +op (((𝐹‘𝑘) ∘ (𝐹‘𝑘)) −op (2
·op (𝐹‘𝑘)))): ℋ⟶
ℋ) |
| 67 | 46, 53, 66 | sylancr 587 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → (
Iop +op (((𝐹‘𝑘) ∘ (𝐹‘𝑘)) −op (2
·op (𝐹‘𝑘)))): ℋ⟶
ℋ) |
| 68 | | hoaddsubass 31834 |
. . . . . . . . . . . 12
⊢ (((
Iop +op (((𝐹‘𝑘) ∘ (𝐹‘𝑘)) −op (2
·op (𝐹‘𝑘)))): ℋ⟶ ℋ ∧
Iop : ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → (((
Iop +op (((𝐹‘𝑘) ∘ (𝐹‘𝑘)) −op (2
·op (𝐹‘𝑘)))) +op Iop )
−op 𝑇) =
(( Iop +op (((𝐹‘𝑘) ∘ (𝐹‘𝑘)) −op (2
·op (𝐹‘𝑘)))) +op ( Iop
−op 𝑇))) |
| 69 | 46, 40, 68 | mp3an23 1455 |
. . . . . . . . . . 11
⊢ ((
Iop +op (((𝐹‘𝑘) ∘ (𝐹‘𝑘)) −op (2
·op (𝐹‘𝑘)))): ℋ⟶ ℋ → (((
Iop +op (((𝐹‘𝑘) ∘ (𝐹‘𝑘)) −op (2
·op (𝐹‘𝑘)))) +op Iop )
−op 𝑇) =
(( Iop +op (((𝐹‘𝑘) ∘ (𝐹‘𝑘)) −op (2
·op (𝐹‘𝑘)))) +op ( Iop
−op 𝑇))) |
| 70 | 67, 69 | syl 17 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → (((
Iop +op (((𝐹‘𝑘) ∘ (𝐹‘𝑘)) −op (2
·op (𝐹‘𝑘)))) +op Iop )
−op 𝑇) =
(( Iop +op (((𝐹‘𝑘) ∘ (𝐹‘𝑘)) −op (2
·op (𝐹‘𝑘)))) +op ( Iop
−op 𝑇))) |
| 71 | | hoaddcl 31777 |
. . . . . . . . . . . 12
⊢ (((2
·op Iop ): ℋ⟶ ℋ ∧
((𝐹‘𝑘) ∘ (𝐹‘𝑘)): ℋ⟶ ℋ) → ((2
·op Iop ) +op ((𝐹‘𝑘) ∘ (𝐹‘𝑘))): ℋ⟶
ℋ) |
| 72 | 48, 42, 71 | sylancr 587 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → ((2
·op Iop ) +op ((𝐹‘𝑘) ∘ (𝐹‘𝑘))): ℋ⟶
ℋ) |
| 73 | | hosubsub4 31837 |
. . . . . . . . . . . 12
⊢ ((((2
·op Iop ) +op ((𝐹‘𝑘) ∘ (𝐹‘𝑘))): ℋ⟶ ℋ ∧ (2
·op (𝐹‘𝑘)): ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ)
→ ((((2 ·op Iop ) +op
((𝐹‘𝑘) ∘ (𝐹‘𝑘))) −op (2
·op (𝐹‘𝑘))) −op 𝑇) = (((2 ·op
Iop ) +op ((𝐹‘𝑘) ∘ (𝐹‘𝑘))) −op ((2
·op (𝐹‘𝑘)) +op 𝑇))) |
| 74 | 40, 73 | mp3an3 1452 |
. . . . . . . . . . 11
⊢ ((((2
·op Iop ) +op ((𝐹‘𝑘) ∘ (𝐹‘𝑘))): ℋ⟶ ℋ ∧ (2
·op (𝐹‘𝑘)): ℋ⟶ ℋ) → ((((2
·op Iop ) +op ((𝐹‘𝑘) ∘ (𝐹‘𝑘))) −op (2
·op (𝐹‘𝑘))) −op 𝑇) = (((2 ·op
Iop ) +op ((𝐹‘𝑘) ∘ (𝐹‘𝑘))) −op ((2
·op (𝐹‘𝑘)) +op 𝑇))) |
| 75 | 72, 38, 74 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → ((((2
·op Iop ) +op ((𝐹‘𝑘) ∘ (𝐹‘𝑘))) −op (2
·op (𝐹‘𝑘))) −op 𝑇) = (((2 ·op
Iop ) +op ((𝐹‘𝑘) ∘ (𝐹‘𝑘))) −op ((2
·op (𝐹‘𝑘)) +op 𝑇))) |
| 76 | 65, 70, 75 | 3eqtr3d 2785 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → ((
Iop +op (((𝐹‘𝑘) ∘ (𝐹‘𝑘)) −op (2
·op (𝐹‘𝑘)))) +op ( Iop
−op 𝑇)) =
(((2 ·op Iop ) +op ((𝐹‘𝑘) ∘ (𝐹‘𝑘))) −op ((2
·op (𝐹‘𝑘)) +op 𝑇))) |
| 77 | | hosubadd4 31833 |
. . . . . . . . . . . 12
⊢ ((((2
·op Iop ): ℋ⟶ ℋ ∧ (2
·op (𝐹‘𝑘)): ℋ⟶ ℋ) ∧ (𝑇: ℋ⟶ ℋ ∧
((𝐹‘𝑘) ∘ (𝐹‘𝑘)): ℋ⟶ ℋ)) → (((2
·op Iop ) −op (2
·op (𝐹‘𝑘))) −op (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘)))) = (((2 ·op
Iop ) +op ((𝐹‘𝑘) ∘ (𝐹‘𝑘))) −op ((2
·op (𝐹‘𝑘)) +op 𝑇))) |
| 78 | 40, 77 | mpanr1 703 |
. . . . . . . . . . 11
⊢ ((((2
·op Iop ): ℋ⟶ ℋ ∧ (2
·op (𝐹‘𝑘)): ℋ⟶ ℋ) ∧ ((𝐹‘𝑘) ∘ (𝐹‘𝑘)): ℋ⟶ ℋ) → (((2
·op Iop ) −op (2
·op (𝐹‘𝑘))) −op (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘)))) = (((2 ·op
Iop ) +op ((𝐹‘𝑘) ∘ (𝐹‘𝑘))) −op ((2
·op (𝐹‘𝑘)) +op 𝑇))) |
| 79 | 48, 78 | mpanl1 700 |
. . . . . . . . . 10
⊢ (((2
·op (𝐹‘𝑘)): ℋ⟶ ℋ ∧ ((𝐹‘𝑘) ∘ (𝐹‘𝑘)): ℋ⟶ ℋ) → (((2
·op Iop ) −op (2
·op (𝐹‘𝑘))) −op (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘)))) = (((2 ·op
Iop ) +op ((𝐹‘𝑘) ∘ (𝐹‘𝑘))) −op ((2
·op (𝐹‘𝑘)) +op 𝑇))) |
| 80 | 38, 42, 79 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → (((2
·op Iop ) −op (2
·op (𝐹‘𝑘))) −op (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘)))) = (((2 ·op
Iop ) +op ((𝐹‘𝑘) ∘ (𝐹‘𝑘))) −op ((2
·op (𝐹‘𝑘)) +op 𝑇))) |
| 81 | 76, 80 | eqtr4d 2780 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → ((
Iop +op (((𝐹‘𝑘) ∘ (𝐹‘𝑘)) −op (2
·op (𝐹‘𝑘)))) +op ( Iop
−op 𝑇)) =
(((2 ·op Iop ) −op (2
·op (𝐹‘𝑘))) −op (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘))))) |
| 82 | | halfcn 12481 |
. . . . . . . . . . . 12
⊢ (1 / 2)
∈ ℂ |
| 83 | | homulcl 31778 |
. . . . . . . . . . . 12
⊢ (((1 / 2)
∈ ℂ ∧ (𝑇
−op ((𝐹‘𝑘) ∘ (𝐹‘𝑘))): ℋ⟶ ℋ) → ((1 / 2)
·op (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘)))): ℋ⟶
ℋ) |
| 84 | 82, 44, 83 | sylancr 587 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → ((1 / 2)
·op (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘)))): ℋ⟶
ℋ) |
| 85 | | hoadddi 31822 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℂ ∧ (𝐹‘𝑘): ℋ⟶ ℋ ∧ ((1 / 2)
·op (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘)))): ℋ⟶ ℋ) → (2
·op ((𝐹‘𝑘) +op ((1 / 2)
·op (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘)))))) = ((2 ·op
(𝐹‘𝑘)) +op (2
·op ((1 / 2) ·op (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘))))))) |
| 86 | 34, 85 | mp3an1 1450 |
. . . . . . . . . . 11
⊢ (((𝐹‘𝑘): ℋ⟶ ℋ ∧ ((1 / 2)
·op (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘)))): ℋ⟶ ℋ) → (2
·op ((𝐹‘𝑘) +op ((1 / 2)
·op (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘)))))) = ((2 ·op
(𝐹‘𝑘)) +op (2
·op ((1 / 2) ·op (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘))))))) |
| 87 | 36, 84, 86 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → (2
·op ((𝐹‘𝑘) +op ((1 / 2)
·op (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘)))))) = ((2 ·op
(𝐹‘𝑘)) +op (2
·op ((1 / 2) ·op (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘))))))) |
| 88 | | 2ne0 12370 |
. . . . . . . . . . . . . 14
⊢ 2 ≠
0 |
| 89 | 34, 88 | recidi 11998 |
. . . . . . . . . . . . 13
⊢ (2
· (1 / 2)) = 1 |
| 90 | 89 | oveq1i 7441 |
. . . . . . . . . . . 12
⊢ ((2
· (1 / 2)) ·op (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘)))) = (1 ·op (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘)))) |
| 91 | | homulass 31821 |
. . . . . . . . . . . . . 14
⊢ ((2
∈ ℂ ∧ (1 / 2) ∈ ℂ ∧ (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘))): ℋ⟶ ℋ) → ((2
· (1 / 2)) ·op (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘)))) = (2 ·op ((1 /
2) ·op (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘)))))) |
| 92 | 34, 82, 91 | mp3an12 1453 |
. . . . . . . . . . . . 13
⊢ ((𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘))): ℋ⟶ ℋ → ((2
· (1 / 2)) ·op (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘)))) = (2 ·op ((1 /
2) ·op (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘)))))) |
| 93 | 44, 92 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → ((2
· (1 / 2)) ·op (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘)))) = (2 ·op ((1 /
2) ·op (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘)))))) |
| 94 | | homullid 31819 |
. . . . . . . . . . . . 13
⊢ ((𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘))): ℋ⟶ ℋ → (1
·op (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘)))) = (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘)))) |
| 95 | 44, 94 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → (1
·op (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘)))) = (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘)))) |
| 96 | 90, 93, 95 | 3eqtr3a 2801 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → (2
·op ((1 / 2) ·op (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘))))) = (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘)))) |
| 97 | 96 | oveq2d 7447 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → ((2
·op (𝐹‘𝑘)) +op (2
·op ((1 / 2) ·op (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘)))))) = ((2 ·op
(𝐹‘𝑘)) +op (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘))))) |
| 98 | 87, 97 | eqtrd 2777 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → (2
·op ((𝐹‘𝑘) +op ((1 / 2)
·op (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘)))))) = ((2 ·op
(𝐹‘𝑘)) +op (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘))))) |
| 99 | 98 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → ((2
·op Iop ) −op (2
·op ((𝐹‘𝑘) +op ((1 / 2)
·op (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘))))))) = ((2 ·op
Iop ) −op ((2 ·op (𝐹‘𝑘)) +op (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘)))))) |
| 100 | 51, 81, 99 | 3eqtr4d 2787 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ → ((
Iop +op (((𝐹‘𝑘) ∘ (𝐹‘𝑘)) −op (2
·op (𝐹‘𝑘)))) +op ( Iop
−op 𝑇)) =
((2 ·op Iop ) −op (2
·op ((𝐹‘𝑘) +op ((1 / 2)
·op (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘)))))))) |
| 101 | | hoaddcl 31777 |
. . . . . . . . 9
⊢ (((𝐹‘𝑘): ℋ⟶ ℋ ∧ ((1 / 2)
·op (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘)))): ℋ⟶ ℋ) → ((𝐹‘𝑘) +op ((1 / 2)
·op (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘))))): ℋ⟶
ℋ) |
| 102 | 36, 84, 101 | syl2anc 584 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → ((𝐹‘𝑘) +op ((1 / 2)
·op (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘))))): ℋ⟶
ℋ) |
| 103 | | hosubdi 31827 |
. . . . . . . . 9
⊢ ((2
∈ ℂ ∧ Iop : ℋ⟶ ℋ ∧ ((𝐹‘𝑘) +op ((1 / 2)
·op (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘))))): ℋ⟶ ℋ) → (2
·op ( Iop −op ((𝐹‘𝑘) +op ((1 / 2)
·op (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘))))))) = ((2 ·op
Iop ) −op (2 ·op ((𝐹‘𝑘) +op ((1 / 2)
·op (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘)))))))) |
| 104 | 34, 46, 103 | mp3an12 1453 |
. . . . . . . 8
⊢ (((𝐹‘𝑘) +op ((1 / 2)
·op (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘))))): ℋ⟶ ℋ → (2
·op ( Iop −op ((𝐹‘𝑘) +op ((1 / 2)
·op (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘))))))) = ((2 ·op
Iop ) −op (2 ·op ((𝐹‘𝑘) +op ((1 / 2)
·op (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘)))))))) |
| 105 | 102, 104 | syl 17 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ → (2
·op ( Iop −op ((𝐹‘𝑘) +op ((1 / 2)
·op (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘))))))) = ((2 ·op
Iop ) −op (2 ·op ((𝐹‘𝑘) +op ((1 / 2)
·op (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘)))))))) |
| 106 | 100, 105 | eqtr4d 2780 |
. . . . . 6
⊢ (𝑘 ∈ ℕ → ((
Iop +op (((𝐹‘𝑘) ∘ (𝐹‘𝑘)) −op (2
·op (𝐹‘𝑘)))) +op ( Iop
−op 𝑇)) =
(2 ·op ( Iop −op ((𝐹‘𝑘) +op ((1 / 2)
·op (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘)))))))) |
| 107 | | hosubcl 31792 |
. . . . . . . . . 10
⊢ ((
Iop : ℋ⟶ ℋ ∧ (𝐹‘𝑘): ℋ⟶ ℋ) → (
Iop −op (𝐹‘𝑘)): ℋ⟶ ℋ) |
| 108 | 46, 36, 107 | sylancr 587 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → (
Iop −op (𝐹‘𝑘)): ℋ⟶ ℋ) |
| 109 | | hocsubdir 31804 |
. . . . . . . . . 10
⊢ ((
Iop : ℋ⟶ ℋ ∧ (𝐹‘𝑘): ℋ⟶ ℋ ∧ (
Iop −op (𝐹‘𝑘)): ℋ⟶ ℋ) → ((
Iop −op (𝐹‘𝑘)) ∘ ( Iop
−op (𝐹‘𝑘))) = (( Iop ∘ (
Iop −op (𝐹‘𝑘))) −op ((𝐹‘𝑘) ∘ ( Iop
−op (𝐹‘𝑘))))) |
| 110 | 46, 109 | mp3an1 1450 |
. . . . . . . . 9
⊢ (((𝐹‘𝑘): ℋ⟶ ℋ ∧ (
Iop −op (𝐹‘𝑘)): ℋ⟶ ℋ) → ((
Iop −op (𝐹‘𝑘)) ∘ ( Iop
−op (𝐹‘𝑘))) = (( Iop ∘ (
Iop −op (𝐹‘𝑘))) −op ((𝐹‘𝑘) ∘ ( Iop
−op (𝐹‘𝑘))))) |
| 111 | 36, 108, 110 | syl2anc 584 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → ((
Iop −op (𝐹‘𝑘)) ∘ ( Iop
−op (𝐹‘𝑘))) = (( Iop ∘ (
Iop −op (𝐹‘𝑘))) −op ((𝐹‘𝑘) ∘ ( Iop
−op (𝐹‘𝑘))))) |
| 112 | | hmoplin 31961 |
. . . . . . . . . . . . . . 15
⊢ (
Iop ∈ HrmOp → Iop ∈
LinOp) |
| 113 | 13, 112 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
Iop ∈ LinOp |
| 114 | | hoddi 32009 |
. . . . . . . . . . . . . 14
⊢ ((
Iop ∈ LinOp ∧ Iop : ℋ⟶ ℋ
∧ (𝐹‘𝑘): ℋ⟶ ℋ)
→ ( Iop ∘ ( Iop −op (𝐹‘𝑘))) = (( Iop ∘
Iop ) −op ( Iop ∘ (𝐹‘𝑘)))) |
| 115 | 113, 46, 114 | mp3an12 1453 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑘): ℋ⟶ ℋ → (
Iop ∘ ( Iop −op (𝐹‘𝑘))) = (( Iop ∘
Iop ) −op ( Iop ∘ (𝐹‘𝑘)))) |
| 116 | 36, 115 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → (
Iop ∘ ( Iop −op (𝐹‘𝑘))) = (( Iop ∘
Iop ) −op ( Iop ∘ (𝐹‘𝑘)))) |
| 117 | 46 | hoid1i 31808 |
. . . . . . . . . . . . . 14
⊢ (
Iop ∘ Iop ) = Iop |
| 118 | 117 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → (
Iop ∘ Iop ) = Iop ) |
| 119 | | hoico2 31776 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘𝑘): ℋ⟶ ℋ → (
Iop ∘ (𝐹‘𝑘)) = (𝐹‘𝑘)) |
| 120 | 36, 119 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → (
Iop ∘ (𝐹‘𝑘)) = (𝐹‘𝑘)) |
| 121 | 118, 120 | oveq12d 7449 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → ((
Iop ∘ Iop ) −op ( Iop
∘ (𝐹‘𝑘))) = ( Iop
−op (𝐹‘𝑘))) |
| 122 | 116, 121 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → (
Iop ∘ ( Iop −op (𝐹‘𝑘))) = ( Iop −op
(𝐹‘𝑘))) |
| 123 | | hmoplin 31961 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘𝑘) ∈ HrmOp → (𝐹‘𝑘) ∈ LinOp) |
| 124 | 15, 123 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → (𝐹‘𝑘) ∈ LinOp) |
| 125 | | hoddi 32009 |
. . . . . . . . . . . . . 14
⊢ (((𝐹‘𝑘) ∈ LinOp ∧ Iop :
ℋ⟶ ℋ ∧ (𝐹‘𝑘): ℋ⟶ ℋ) → ((𝐹‘𝑘) ∘ ( Iop
−op (𝐹‘𝑘))) = (((𝐹‘𝑘) ∘ Iop )
−op ((𝐹‘𝑘) ∘ (𝐹‘𝑘)))) |
| 126 | 46, 125 | mp3an2 1451 |
. . . . . . . . . . . . 13
⊢ (((𝐹‘𝑘) ∈ LinOp ∧ (𝐹‘𝑘): ℋ⟶ ℋ) → ((𝐹‘𝑘) ∘ ( Iop
−op (𝐹‘𝑘))) = (((𝐹‘𝑘) ∘ Iop )
−op ((𝐹‘𝑘) ∘ (𝐹‘𝑘)))) |
| 127 | 124, 36, 126 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → ((𝐹‘𝑘) ∘ ( Iop
−op (𝐹‘𝑘))) = (((𝐹‘𝑘) ∘ Iop )
−op ((𝐹‘𝑘) ∘ (𝐹‘𝑘)))) |
| 128 | | hoico1 31775 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘𝑘): ℋ⟶ ℋ → ((𝐹‘𝑘) ∘ Iop ) = (𝐹‘𝑘)) |
| 129 | 36, 128 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → ((𝐹‘𝑘) ∘ Iop ) = (𝐹‘𝑘)) |
| 130 | 129 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → (((𝐹‘𝑘) ∘ Iop )
−op ((𝐹‘𝑘) ∘ (𝐹‘𝑘))) = ((𝐹‘𝑘) −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘)))) |
| 131 | 127, 130 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → ((𝐹‘𝑘) ∘ ( Iop
−op (𝐹‘𝑘))) = ((𝐹‘𝑘) −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘)))) |
| 132 | 122, 131 | oveq12d 7449 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → ((
Iop ∘ ( Iop −op (𝐹‘𝑘))) −op ((𝐹‘𝑘) ∘ ( Iop
−op (𝐹‘𝑘)))) = (( Iop −op
(𝐹‘𝑘)) −op ((𝐹‘𝑘) −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘))))) |
| 133 | 36, 46 | jctil 519 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → (
Iop : ℋ⟶ ℋ ∧ (𝐹‘𝑘): ℋ⟶ ℋ)) |
| 134 | | hosubadd4 31833 |
. . . . . . . . . . 11
⊢ (((
Iop : ℋ⟶ ℋ ∧ (𝐹‘𝑘): ℋ⟶ ℋ) ∧ ((𝐹‘𝑘): ℋ⟶ ℋ ∧ ((𝐹‘𝑘) ∘ (𝐹‘𝑘)): ℋ⟶ ℋ)) → ((
Iop −op (𝐹‘𝑘)) −op ((𝐹‘𝑘) −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘)))) = (( Iop +op
((𝐹‘𝑘) ∘ (𝐹‘𝑘))) −op ((𝐹‘𝑘) +op (𝐹‘𝑘)))) |
| 135 | 133, 36, 42, 134 | syl12anc 837 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → ((
Iop −op (𝐹‘𝑘)) −op ((𝐹‘𝑘) −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘)))) = (( Iop +op
((𝐹‘𝑘) ∘ (𝐹‘𝑘))) −op ((𝐹‘𝑘) +op (𝐹‘𝑘)))) |
| 136 | 132, 135 | eqtrd 2777 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → ((
Iop ∘ ( Iop −op (𝐹‘𝑘))) −op ((𝐹‘𝑘) ∘ ( Iop
−op (𝐹‘𝑘)))) = (( Iop +op
((𝐹‘𝑘) ∘ (𝐹‘𝑘))) −op ((𝐹‘𝑘) +op (𝐹‘𝑘)))) |
| 137 | | ho2times 31838 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑘): ℋ⟶ ℋ → (2
·op (𝐹‘𝑘)) = ((𝐹‘𝑘) +op (𝐹‘𝑘))) |
| 138 | 36, 137 | syl 17 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → (2
·op (𝐹‘𝑘)) = ((𝐹‘𝑘) +op (𝐹‘𝑘))) |
| 139 | 138 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → ((
Iop +op ((𝐹‘𝑘) ∘ (𝐹‘𝑘))) −op (2
·op (𝐹‘𝑘))) = (( Iop +op
((𝐹‘𝑘) ∘ (𝐹‘𝑘))) −op ((𝐹‘𝑘) +op (𝐹‘𝑘)))) |
| 140 | | hoaddsubass 31834 |
. . . . . . . . . . 11
⊢ ((
Iop : ℋ⟶ ℋ ∧ ((𝐹‘𝑘) ∘ (𝐹‘𝑘)): ℋ⟶ ℋ ∧ (2
·op (𝐹‘𝑘)): ℋ⟶ ℋ) → ((
Iop +op ((𝐹‘𝑘) ∘ (𝐹‘𝑘))) −op (2
·op (𝐹‘𝑘))) = ( Iop +op
(((𝐹‘𝑘) ∘ (𝐹‘𝑘)) −op (2
·op (𝐹‘𝑘))))) |
| 141 | 46, 140 | mp3an1 1450 |
. . . . . . . . . 10
⊢ ((((𝐹‘𝑘) ∘ (𝐹‘𝑘)): ℋ⟶ ℋ ∧ (2
·op (𝐹‘𝑘)): ℋ⟶ ℋ) → ((
Iop +op ((𝐹‘𝑘) ∘ (𝐹‘𝑘))) −op (2
·op (𝐹‘𝑘))) = ( Iop +op
(((𝐹‘𝑘) ∘ (𝐹‘𝑘)) −op (2
·op (𝐹‘𝑘))))) |
| 142 | 42, 38, 141 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → ((
Iop +op ((𝐹‘𝑘) ∘ (𝐹‘𝑘))) −op (2
·op (𝐹‘𝑘))) = ( Iop +op
(((𝐹‘𝑘) ∘ (𝐹‘𝑘)) −op (2
·op (𝐹‘𝑘))))) |
| 143 | 136, 139,
142 | 3eqtr2d 2783 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → ((
Iop ∘ ( Iop −op (𝐹‘𝑘))) −op ((𝐹‘𝑘) ∘ ( Iop
−op (𝐹‘𝑘)))) = ( Iop +op
(((𝐹‘𝑘) ∘ (𝐹‘𝑘)) −op (2
·op (𝐹‘𝑘))))) |
| 144 | 111, 143 | eqtrd 2777 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ → ((
Iop −op (𝐹‘𝑘)) ∘ ( Iop
−op (𝐹‘𝑘))) = ( Iop +op
(((𝐹‘𝑘) ∘ (𝐹‘𝑘)) −op (2
·op (𝐹‘𝑘))))) |
| 145 | 144 | oveq1d 7446 |
. . . . . 6
⊢ (𝑘 ∈ ℕ → (((
Iop −op (𝐹‘𝑘)) ∘ ( Iop
−op (𝐹‘𝑘))) +op ( Iop
−op 𝑇)) =
(( Iop +op (((𝐹‘𝑘) ∘ (𝐹‘𝑘)) −op (2
·op (𝐹‘𝑘)))) +op ( Iop
−op 𝑇))) |
| 146 | 7, 8, 9 | opsqrlem5 32163 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → (𝐹‘(𝑘 + 1)) = ((𝐹‘𝑘) +op ((1 / 2)
·op (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘)))))) |
| 147 | 146 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ → (
Iop −op (𝐹‘(𝑘 + 1))) = ( Iop
−op ((𝐹‘𝑘) +op ((1 / 2)
·op (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘))))))) |
| 148 | 147 | oveq2d 7447 |
. . . . . 6
⊢ (𝑘 ∈ ℕ → (2
·op ( Iop −op (𝐹‘(𝑘 + 1)))) = (2 ·op (
Iop −op ((𝐹‘𝑘) +op ((1 / 2)
·op (𝑇 −op ((𝐹‘𝑘) ∘ (𝐹‘𝑘)))))))) |
| 149 | 106, 145,
148 | 3eqtr4d 2787 |
. . . . 5
⊢ (𝑘 ∈ ℕ → (((
Iop −op (𝐹‘𝑘)) ∘ ( Iop
−op (𝐹‘𝑘))) +op ( Iop
−op 𝑇)) =
(2 ·op ( Iop −op (𝐹‘(𝑘 + 1))))) |
| 150 | 33, 149 | breqtrd 5169 |
. . . 4
⊢ (𝑘 ∈ ℕ →
0hop ≤op (2 ·op (
Iop −op (𝐹‘(𝑘 + 1))))) |
| 151 | | peano2nn 12278 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈
ℕ) |
| 152 | 14 | ffvelcdmi 7103 |
. . . . . . 7
⊢ ((𝑘 + 1) ∈ ℕ →
(𝐹‘(𝑘 + 1)) ∈
HrmOp) |
| 153 | 151, 152 | syl 17 |
. . . . . 6
⊢ (𝑘 ∈ ℕ → (𝐹‘(𝑘 + 1)) ∈ HrmOp) |
| 154 | | hmopd 32041 |
. . . . . 6
⊢ ((
Iop ∈ HrmOp ∧ (𝐹‘(𝑘 + 1)) ∈ HrmOp) → ( Iop
−op (𝐹‘(𝑘 + 1))) ∈ HrmOp) |
| 155 | 13, 153, 154 | sylancr 587 |
. . . . 5
⊢ (𝑘 ∈ ℕ → (
Iop −op (𝐹‘(𝑘 + 1))) ∈ HrmOp) |
| 156 | | 2re 12340 |
. . . . . 6
⊢ 2 ∈
ℝ |
| 157 | | 2pos 12369 |
. . . . . 6
⊢ 0 <
2 |
| 158 | | leopmul 32153 |
. . . . . 6
⊢ ((2
∈ ℝ ∧ ( Iop −op (𝐹‘(𝑘 + 1))) ∈ HrmOp ∧ 0 < 2) → (
0hop ≤op ( Iop −op (𝐹‘(𝑘 + 1))) ↔ 0hop
≤op (2 ·op ( Iop
−op (𝐹‘(𝑘 + 1)))))) |
| 159 | 156, 157,
158 | mp3an13 1454 |
. . . . 5
⊢ ((
Iop −op (𝐹‘(𝑘 + 1))) ∈ HrmOp → ( 0hop
≤op ( Iop −op (𝐹‘(𝑘 + 1))) ↔ 0hop
≤op (2 ·op ( Iop
−op (𝐹‘(𝑘 + 1)))))) |
| 160 | 155, 159 | syl 17 |
. . . 4
⊢ (𝑘 ∈ ℕ → (
0hop ≤op ( Iop −op (𝐹‘(𝑘 + 1))) ↔ 0hop
≤op (2 ·op ( Iop
−op (𝐹‘(𝑘 + 1)))))) |
| 161 | 150, 160 | mpbird 257 |
. . 3
⊢ (𝑘 ∈ ℕ →
0hop ≤op ( Iop −op (𝐹‘(𝑘 + 1)))) |
| 162 | | leop3 32144 |
. . . 4
⊢ (((𝐹‘(𝑘 + 1)) ∈ HrmOp ∧ Iop
∈ HrmOp) → ((𝐹‘(𝑘 + 1)) ≤op Iop
↔ 0hop ≤op ( Iop −op
(𝐹‘(𝑘 + 1))))) |
| 163 | 153, 13, 162 | sylancl 586 |
. . 3
⊢ (𝑘 ∈ ℕ → ((𝐹‘(𝑘 + 1)) ≤op Iop
↔ 0hop ≤op ( Iop −op
(𝐹‘(𝑘 + 1))))) |
| 164 | 161, 163 | mpbird 257 |
. 2
⊢ (𝑘 ∈ ℕ → (𝐹‘(𝑘 + 1)) ≤op Iop
) |
| 165 | 2, 4, 6, 12, 164 | nn1suc 12288 |
1
⊢ (𝑁 ∈ ℕ → (𝐹‘𝑁) ≤op Iop
) |