HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  opsqrlem6 Structured version   Visualization version   GIF version

Theorem opsqrlem6 30973
Description: Lemma for opsqri . (Contributed by NM, 23-Aug-2006.) (New usage is discouraged.)
Hypotheses
Ref Expression
opsqrlem2.1 ๐‘‡ โˆˆ HrmOp
opsqrlem2.2 ๐‘† = (๐‘ฅ โˆˆ HrmOp, ๐‘ฆ โˆˆ HrmOp โ†ฆ (๐‘ฅ +op ((1 / 2) ยทop (๐‘‡ โˆ’op (๐‘ฅ โˆ˜ ๐‘ฅ)))))
opsqrlem2.3 ๐น = seq1(๐‘†, (โ„• ร— { 0hop }))
opsqrlem6.4 ๐‘‡ โ‰คop Iop
Assertion
Ref Expression
opsqrlem6 (๐‘ โˆˆ โ„• โ†’ (๐นโ€˜๐‘) โ‰คop Iop )
Distinct variable group:   ๐‘ฅ,๐‘ฆ,๐‘‡
Allowed substitution hints:   ๐‘†(๐‘ฅ,๐‘ฆ)   ๐น(๐‘ฅ,๐‘ฆ)   ๐‘(๐‘ฅ,๐‘ฆ)

Proof of Theorem opsqrlem6
Dummy variables ๐‘— ๐‘˜ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 6839 . . 3 (๐‘— = 1 โ†’ (๐นโ€˜๐‘—) = (๐นโ€˜1))
21breq1d 5113 . 2 (๐‘— = 1 โ†’ ((๐นโ€˜๐‘—) โ‰คop Iop โ†” (๐นโ€˜1) โ‰คop Iop ))
3 fveq2 6839 . . 3 (๐‘— = (๐‘˜ + 1) โ†’ (๐นโ€˜๐‘—) = (๐นโ€˜(๐‘˜ + 1)))
43breq1d 5113 . 2 (๐‘— = (๐‘˜ + 1) โ†’ ((๐นโ€˜๐‘—) โ‰คop Iop โ†” (๐นโ€˜(๐‘˜ + 1)) โ‰คop Iop ))
5 fveq2 6839 . . 3 (๐‘— = ๐‘ โ†’ (๐นโ€˜๐‘—) = (๐นโ€˜๐‘))
65breq1d 5113 . 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 }))
107, 8, 9opsqrlem2 30969 . . 3 (๐นโ€˜1) = 0hop
11 idleop 30959 . . 3 0hop โ‰คop Iop
1210, 11eqbrtri 5124 . 2 (๐นโ€˜1) โ‰คop Iop
13 idhmop 30810 . . . . . . . 8 Iop โˆˆ HrmOp
147, 8, 9opsqrlem4 30971 . . . . . . . . 9 ๐น:โ„•โŸถHrmOp
1514ffvelcdmi 7030 . . . . . . . 8 (๐‘˜ โˆˆ โ„• โ†’ (๐นโ€˜๐‘˜) โˆˆ HrmOp)
16 hmopd 30850 . . . . . . . 8 (( Iop โˆˆ HrmOp โˆง (๐นโ€˜๐‘˜) โˆˆ HrmOp) โ†’ ( Iop โˆ’op (๐นโ€˜๐‘˜)) โˆˆ HrmOp)
1713, 15, 16sylancr 587 . . . . . . 7 (๐‘˜ โˆˆ โ„• โ†’ ( Iop โˆ’op (๐นโ€˜๐‘˜)) โˆˆ HrmOp)
18 eqid 2736 . . . . . . . 8 (( Iop โˆ’op (๐นโ€˜๐‘˜)) โˆ˜ ( Iop โˆ’op (๐นโ€˜๐‘˜))) = (( Iop โˆ’op (๐นโ€˜๐‘˜)) โˆ˜ ( Iop โˆ’op (๐นโ€˜๐‘˜)))
19 hmopco 30851 . . . . . . . 8 ((( Iop โˆ’op (๐นโ€˜๐‘˜)) โˆˆ HrmOp โˆง ( Iop โˆ’op (๐นโ€˜๐‘˜)) โˆˆ HrmOp โˆง (( Iop โˆ’op (๐นโ€˜๐‘˜)) โˆ˜ ( Iop โˆ’op (๐นโ€˜๐‘˜))) = (( Iop โˆ’op (๐นโ€˜๐‘˜)) โˆ˜ ( Iop โˆ’op (๐นโ€˜๐‘˜)))) โ†’ (( Iop โˆ’op (๐นโ€˜๐‘˜)) โˆ˜ ( Iop โˆ’op (๐นโ€˜๐‘˜))) โˆˆ HrmOp)
2018, 19mp3an3 1450 . . . . . . 7 ((( Iop โˆ’op (๐นโ€˜๐‘˜)) โˆˆ HrmOp โˆง ( Iop โˆ’op (๐นโ€˜๐‘˜)) โˆˆ HrmOp) โ†’ (( Iop โˆ’op (๐นโ€˜๐‘˜)) โˆ˜ ( Iop โˆ’op (๐นโ€˜๐‘˜))) โˆˆ HrmOp)
2117, 17, 20syl2anc 584 . . . . . 6 (๐‘˜ โˆˆ โ„• โ†’ (( Iop โˆ’op (๐นโ€˜๐‘˜)) โˆ˜ ( Iop โˆ’op (๐นโ€˜๐‘˜))) โˆˆ HrmOp)
22 leopsq 30957 . . . . . . 7 (( Iop โˆ’op (๐นโ€˜๐‘˜)) โˆˆ HrmOp โ†’ 0hop โ‰คop (( Iop โˆ’op (๐นโ€˜๐‘˜)) โˆ˜ ( Iop โˆ’op (๐นโ€˜๐‘˜))))
2317, 22syl 17 . . . . . 6 (๐‘˜ โˆˆ โ„• โ†’ 0hop โ‰คop (( Iop โˆ’op (๐นโ€˜๐‘˜)) โˆ˜ ( Iop โˆ’op (๐นโ€˜๐‘˜))))
24 opsqrlem6.4 . . . . . . . 8 ๐‘‡ โ‰คop Iop
25 leop3 30953 . . . . . . . . 9 ((๐‘‡ โˆˆ HrmOp โˆง Iop โˆˆ HrmOp) โ†’ (๐‘‡ โ‰คop Iop โ†” 0hop โ‰คop ( Iop โˆ’op ๐‘‡)))
267, 13, 25mp2an 690 . . . . . . . 8 (๐‘‡ โ‰คop Iop โ†” 0hop โ‰คop ( Iop โˆ’op ๐‘‡))
2724, 26mpbi 229 . . . . . . 7 0hop โ‰คop ( Iop โˆ’op ๐‘‡)
28 hmopd 30850 . . . . . . . . 9 (( Iop โˆˆ HrmOp โˆง ๐‘‡ โˆˆ HrmOp) โ†’ ( Iop โˆ’op ๐‘‡) โˆˆ HrmOp)
2913, 7, 28mp2an 690 . . . . . . . 8 ( Iop โˆ’op ๐‘‡) โˆˆ HrmOp
30 leopadd 30960 . . . . . . . 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 ๐‘‡)))
3129, 30mpanl2 699 . . . . . . 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 ๐‘‡)))
3227, 31mpanr2 702 . . . . . 6 (((( Iop โˆ’op (๐นโ€˜๐‘˜)) โˆ˜ ( Iop โˆ’op (๐นโ€˜๐‘˜))) โˆˆ HrmOp โˆง 0hop โ‰คop (( Iop โˆ’op (๐นโ€˜๐‘˜)) โˆ˜ ( Iop โˆ’op (๐นโ€˜๐‘˜)))) โ†’ 0hop โ‰คop ((( Iop โˆ’op (๐นโ€˜๐‘˜)) โˆ˜ ( Iop โˆ’op (๐นโ€˜๐‘˜))) +op ( Iop โˆ’op ๐‘‡)))
3321, 23, 32syl2anc 584 . . . . 5 (๐‘˜ โˆˆ โ„• โ†’ 0hop โ‰คop ((( Iop โˆ’op (๐นโ€˜๐‘˜)) โˆ˜ ( Iop โˆ’op (๐นโ€˜๐‘˜))) +op ( Iop โˆ’op ๐‘‡)))
34 2cn 12224 . . . . . . . . . 10 2 โˆˆ โ„‚
35 hmopf 30702 . . . . . . . . . . 11 ((๐นโ€˜๐‘˜) โˆˆ HrmOp โ†’ (๐นโ€˜๐‘˜): โ„‹โŸถ โ„‹)
3615, 35syl 17 . . . . . . . . . 10 (๐‘˜ โˆˆ โ„• โ†’ (๐นโ€˜๐‘˜): โ„‹โŸถ โ„‹)
37 homulcl 30587 . . . . . . . . . 10 ((2 โˆˆ โ„‚ โˆง (๐นโ€˜๐‘˜): โ„‹โŸถ โ„‹) โ†’ (2 ยทop (๐นโ€˜๐‘˜)): โ„‹โŸถ โ„‹)
3834, 36, 37sylancr 587 . . . . . . . . 9 (๐‘˜ โˆˆ โ„• โ†’ (2 ยทop (๐นโ€˜๐‘˜)): โ„‹โŸถ โ„‹)
39 hmopf 30702 . . . . . . . . . . 11 (๐‘‡ โˆˆ HrmOp โ†’ ๐‘‡: โ„‹โŸถ โ„‹)
407, 39ax-mp 5 . . . . . . . . . 10 ๐‘‡: โ„‹โŸถ โ„‹
41 fco 6689 . . . . . . . . . . 11 (((๐นโ€˜๐‘˜): โ„‹โŸถ โ„‹ โˆง (๐นโ€˜๐‘˜): โ„‹โŸถ โ„‹) โ†’ ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)): โ„‹โŸถ โ„‹)
4236, 36, 41syl2anc 584 . . . . . . . . . 10 (๐‘˜ โˆˆ โ„• โ†’ ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)): โ„‹โŸถ โ„‹)
43 hosubcl 30601 . . . . . . . . . 10 ((๐‘‡: โ„‹โŸถ โ„‹ โˆง ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)): โ„‹โŸถ โ„‹) โ†’ (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))): โ„‹โŸถ โ„‹)
4440, 42, 43sylancr 587 . . . . . . . . 9 (๐‘˜ โˆˆ โ„• โ†’ (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))): โ„‹โŸถ โ„‹)
45 hmopf 30702 . . . . . . . . . . . 12 ( Iop โˆˆ HrmOp โ†’ Iop : โ„‹โŸถ โ„‹)
4613, 45ax-mp 5 . . . . . . . . . . 11 Iop : โ„‹โŸถ โ„‹
47 homulcl 30587 . . . . . . . . . . 11 ((2 โˆˆ โ„‚ โˆง Iop : โ„‹โŸถ โ„‹) โ†’ (2 ยทop Iop ): โ„‹โŸถ โ„‹)
4834, 46, 47mp2an 690 . . . . . . . . . 10 (2 ยทop Iop ): โ„‹โŸถ โ„‹
49 hosubsub4 30646 . . . . . . . . . 10 (((2 ยทop Iop ): โ„‹โŸถ โ„‹ โˆง (2 ยทop (๐นโ€˜๐‘˜)): โ„‹โŸถ โ„‹ โˆง (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))): โ„‹โŸถ โ„‹) โ†’ (((2 ยทop Iop ) โˆ’op (2 ยทop (๐นโ€˜๐‘˜))) โˆ’op (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)))) = ((2 ยทop Iop ) โˆ’op ((2 ยทop (๐นโ€˜๐‘˜)) +op (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))))))
5048, 49mp3an1 1448 . . . . . . . . 9 (((2 ยทop (๐นโ€˜๐‘˜)): โ„‹โŸถ โ„‹ โˆง (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))): โ„‹โŸถ โ„‹) โ†’ (((2 ยทop Iop ) โˆ’op (2 ยทop (๐นโ€˜๐‘˜))) โˆ’op (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)))) = ((2 ยทop Iop ) โˆ’op ((2 ยทop (๐นโ€˜๐‘˜)) +op (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))))))
5138, 44, 50syl2anc 584 . . . . . . . 8 (๐‘˜ โˆˆ โ„• โ†’ (((2 ยทop Iop ) โˆ’op (2 ยทop (๐นโ€˜๐‘˜))) โˆ’op (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)))) = ((2 ยทop Iop ) โˆ’op ((2 ยทop (๐นโ€˜๐‘˜)) +op (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))))))
52 hosubcl 30601 . . . . . . . . . . . . . . 15 ((((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)): โ„‹โŸถ โ„‹ โˆง (2 ยทop (๐นโ€˜๐‘˜)): โ„‹โŸถ โ„‹) โ†’ (((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)) โˆ’op (2 ยทop (๐นโ€˜๐‘˜))): โ„‹โŸถ โ„‹)
5342, 38, 52syl2anc 584 . . . . . . . . . . . . . 14 (๐‘˜ โˆˆ โ„• โ†’ (((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)) โˆ’op (2 ยทop (๐นโ€˜๐‘˜))): โ„‹โŸถ โ„‹)
54 hoadd32 30611 . . . . . . . . . . . . . . 15 (( Iop : โ„‹โŸถ โ„‹ โˆง (((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)) โˆ’op (2 ยทop (๐นโ€˜๐‘˜))): โ„‹โŸถ โ„‹ โˆง Iop : โ„‹โŸถ โ„‹) โ†’ (( Iop +op (((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)) โˆ’op (2 ยทop (๐นโ€˜๐‘˜)))) +op Iop ) = (( Iop +op Iop ) +op (((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)) โˆ’op (2 ยทop (๐นโ€˜๐‘˜)))))
5546, 46, 54mp3an13 1452 . . . . . . . . . . . . . 14 ((((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)) โˆ’op (2 ยทop (๐นโ€˜๐‘˜))): โ„‹โŸถ โ„‹ โ†’ (( Iop +op (((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)) โˆ’op (2 ยทop (๐นโ€˜๐‘˜)))) +op Iop ) = (( Iop +op Iop ) +op (((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)) โˆ’op (2 ยทop (๐นโ€˜๐‘˜)))))
5653, 55syl 17 . . . . . . . . . . . . 13 (๐‘˜ โˆˆ โ„• โ†’ (( Iop +op (((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)) โˆ’op (2 ยทop (๐นโ€˜๐‘˜)))) +op Iop ) = (( Iop +op Iop ) +op (((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)) โˆ’op (2 ยทop (๐นโ€˜๐‘˜)))))
57 ho2times 30647 . . . . . . . . . . . . . . 15 ( Iop : โ„‹โŸถ โ„‹ โ†’ (2 ยทop Iop ) = ( Iop +op Iop ))
5846, 57ax-mp 5 . . . . . . . . . . . . . 14 (2 ยทop Iop ) = ( Iop +op Iop )
5958oveq1i 7363 . . . . . . . . . . . . 13 ((2 ยทop Iop ) +op (((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)) โˆ’op (2 ยทop (๐นโ€˜๐‘˜)))) = (( Iop +op Iop ) +op (((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)) โˆ’op (2 ยทop (๐นโ€˜๐‘˜))))
6056, 59eqtr4di 2794 . . . . . . . . . . . 12 (๐‘˜ โˆˆ โ„• โ†’ (( Iop +op (((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)) โˆ’op (2 ยทop (๐นโ€˜๐‘˜)))) +op Iop ) = ((2 ยทop Iop ) +op (((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)) โˆ’op (2 ยทop (๐นโ€˜๐‘˜)))))
61 hoaddsubass 30643 . . . . . . . . . . . . . 14 (((2 ยทop Iop ): โ„‹โŸถ โ„‹ โˆง ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)): โ„‹โŸถ โ„‹ โˆง (2 ยทop (๐นโ€˜๐‘˜)): โ„‹โŸถ โ„‹) โ†’ (((2 ยทop Iop ) +op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))) โˆ’op (2 ยทop (๐นโ€˜๐‘˜))) = ((2 ยทop Iop ) +op (((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)) โˆ’op (2 ยทop (๐นโ€˜๐‘˜)))))
6248, 61mp3an1 1448 . . . . . . . . . . . . 13 ((((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)): โ„‹โŸถ โ„‹ โˆง (2 ยทop (๐นโ€˜๐‘˜)): โ„‹โŸถ โ„‹) โ†’ (((2 ยทop Iop ) +op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))) โˆ’op (2 ยทop (๐นโ€˜๐‘˜))) = ((2 ยทop Iop ) +op (((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)) โˆ’op (2 ยทop (๐นโ€˜๐‘˜)))))
6342, 38, 62syl2anc 584 . . . . . . . . . . . 12 (๐‘˜ โˆˆ โ„• โ†’ (((2 ยทop Iop ) +op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))) โˆ’op (2 ยทop (๐นโ€˜๐‘˜))) = ((2 ยทop Iop ) +op (((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)) โˆ’op (2 ยทop (๐นโ€˜๐‘˜)))))
6460, 63eqtr4d 2779 . . . . . . . . . . 11 (๐‘˜ โˆˆ โ„• โ†’ (( Iop +op (((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)) โˆ’op (2 ยทop (๐นโ€˜๐‘˜)))) +op Iop ) = (((2 ยทop Iop ) +op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))) โˆ’op (2 ยทop (๐นโ€˜๐‘˜))))
6564oveq1d 7368 . . . . . . . . . 10 (๐‘˜ โˆˆ โ„• โ†’ ((( Iop +op (((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)) โˆ’op (2 ยทop (๐นโ€˜๐‘˜)))) +op Iop ) โˆ’op ๐‘‡) = ((((2 ยทop Iop ) +op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))) โˆ’op (2 ยทop (๐นโ€˜๐‘˜))) โˆ’op ๐‘‡))
66 hoaddcl 30586 . . . . . . . . . . . 12 (( Iop : โ„‹โŸถ โ„‹ โˆง (((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)) โˆ’op (2 ยทop (๐นโ€˜๐‘˜))): โ„‹โŸถ โ„‹) โ†’ ( Iop +op (((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)) โˆ’op (2 ยทop (๐นโ€˜๐‘˜)))): โ„‹โŸถ โ„‹)
6746, 53, 66sylancr 587 . . . . . . . . . . 11 (๐‘˜ โˆˆ โ„• โ†’ ( Iop +op (((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)) โˆ’op (2 ยทop (๐นโ€˜๐‘˜)))): โ„‹โŸถ โ„‹)
68 hoaddsubass 30643 . . . . . . . . . . . 12 ((( Iop +op (((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)) โˆ’op (2 ยทop (๐นโ€˜๐‘˜)))): โ„‹โŸถ โ„‹ โˆง Iop : โ„‹โŸถ โ„‹ โˆง ๐‘‡: โ„‹โŸถ โ„‹) โ†’ ((( Iop +op (((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)) โˆ’op (2 ยทop (๐นโ€˜๐‘˜)))) +op Iop ) โˆ’op ๐‘‡) = (( Iop +op (((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)) โˆ’op (2 ยทop (๐นโ€˜๐‘˜)))) +op ( Iop โˆ’op ๐‘‡)))
6946, 40, 68mp3an23 1453 . . . . . . . . . . 11 (( Iop +op (((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)) โˆ’op (2 ยทop (๐นโ€˜๐‘˜)))): โ„‹โŸถ โ„‹ โ†’ ((( Iop +op (((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)) โˆ’op (2 ยทop (๐นโ€˜๐‘˜)))) +op Iop ) โˆ’op ๐‘‡) = (( Iop +op (((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)) โˆ’op (2 ยทop (๐นโ€˜๐‘˜)))) +op ( Iop โˆ’op ๐‘‡)))
7067, 69syl 17 . . . . . . . . . 10 (๐‘˜ โˆˆ โ„• โ†’ ((( Iop +op (((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)) โˆ’op (2 ยทop (๐นโ€˜๐‘˜)))) +op Iop ) โˆ’op ๐‘‡) = (( Iop +op (((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)) โˆ’op (2 ยทop (๐นโ€˜๐‘˜)))) +op ( Iop โˆ’op ๐‘‡)))
71 hoaddcl 30586 . . . . . . . . . . . 12 (((2 ยทop Iop ): โ„‹โŸถ โ„‹ โˆง ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)): โ„‹โŸถ โ„‹) โ†’ ((2 ยทop Iop ) +op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))): โ„‹โŸถ โ„‹)
7248, 42, 71sylancr 587 . . . . . . . . . . 11 (๐‘˜ โˆˆ โ„• โ†’ ((2 ยทop Iop ) +op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))): โ„‹โŸถ โ„‹)
73 hosubsub4 30646 . . . . . . . . . . . 12 ((((2 ยทop Iop ) +op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))): โ„‹โŸถ โ„‹ โˆง (2 ยทop (๐นโ€˜๐‘˜)): โ„‹โŸถ โ„‹ โˆง ๐‘‡: โ„‹โŸถ โ„‹) โ†’ ((((2 ยทop Iop ) +op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))) โˆ’op (2 ยทop (๐นโ€˜๐‘˜))) โˆ’op ๐‘‡) = (((2 ยทop Iop ) +op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))) โˆ’op ((2 ยทop (๐นโ€˜๐‘˜)) +op ๐‘‡)))
7440, 73mp3an3 1450 . . . . . . . . . . 11 ((((2 ยทop Iop ) +op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))): โ„‹โŸถ โ„‹ โˆง (2 ยทop (๐นโ€˜๐‘˜)): โ„‹โŸถ โ„‹) โ†’ ((((2 ยทop Iop ) +op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))) โˆ’op (2 ยทop (๐นโ€˜๐‘˜))) โˆ’op ๐‘‡) = (((2 ยทop Iop ) +op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))) โˆ’op ((2 ยทop (๐นโ€˜๐‘˜)) +op ๐‘‡)))
7572, 38, 74syl2anc 584 . . . . . . . . . 10 (๐‘˜ โˆˆ โ„• โ†’ ((((2 ยทop Iop ) +op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))) โˆ’op (2 ยทop (๐นโ€˜๐‘˜))) โˆ’op ๐‘‡) = (((2 ยทop Iop ) +op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))) โˆ’op ((2 ยทop (๐นโ€˜๐‘˜)) +op ๐‘‡)))
7665, 70, 753eqtr3d 2784 . . . . . . . . 9 (๐‘˜ โˆˆ โ„• โ†’ (( Iop +op (((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)) โˆ’op (2 ยทop (๐นโ€˜๐‘˜)))) +op ( Iop โˆ’op ๐‘‡)) = (((2 ยทop Iop ) +op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))) โˆ’op ((2 ยทop (๐นโ€˜๐‘˜)) +op ๐‘‡)))
77 hosubadd4 30642 . . . . . . . . . . . 12 ((((2 ยทop Iop ): โ„‹โŸถ โ„‹ โˆง (2 ยทop (๐นโ€˜๐‘˜)): โ„‹โŸถ โ„‹) โˆง (๐‘‡: โ„‹โŸถ โ„‹ โˆง ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)): โ„‹โŸถ โ„‹)) โ†’ (((2 ยทop Iop ) โˆ’op (2 ยทop (๐นโ€˜๐‘˜))) โˆ’op (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)))) = (((2 ยทop Iop ) +op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))) โˆ’op ((2 ยทop (๐นโ€˜๐‘˜)) +op ๐‘‡)))
7840, 77mpanr1 701 . . . . . . . . . . 11 ((((2 ยทop Iop ): โ„‹โŸถ โ„‹ โˆง (2 ยทop (๐นโ€˜๐‘˜)): โ„‹โŸถ โ„‹) โˆง ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)): โ„‹โŸถ โ„‹) โ†’ (((2 ยทop Iop ) โˆ’op (2 ยทop (๐นโ€˜๐‘˜))) โˆ’op (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)))) = (((2 ยทop Iop ) +op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))) โˆ’op ((2 ยทop (๐นโ€˜๐‘˜)) +op ๐‘‡)))
7948, 78mpanl1 698 . . . . . . . . . 10 (((2 ยทop (๐นโ€˜๐‘˜)): โ„‹โŸถ โ„‹ โˆง ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)): โ„‹โŸถ โ„‹) โ†’ (((2 ยทop Iop ) โˆ’op (2 ยทop (๐นโ€˜๐‘˜))) โˆ’op (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)))) = (((2 ยทop Iop ) +op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))) โˆ’op ((2 ยทop (๐นโ€˜๐‘˜)) +op ๐‘‡)))
8038, 42, 79syl2anc 584 . . . . . . . . 9 (๐‘˜ โˆˆ โ„• โ†’ (((2 ยทop Iop ) โˆ’op (2 ยทop (๐นโ€˜๐‘˜))) โˆ’op (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)))) = (((2 ยทop Iop ) +op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))) โˆ’op ((2 ยทop (๐นโ€˜๐‘˜)) +op ๐‘‡)))
8176, 80eqtr4d 2779 . . . . . . . 8 (๐‘˜ โˆˆ โ„• โ†’ (( Iop +op (((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)) โˆ’op (2 ยทop (๐นโ€˜๐‘˜)))) +op ( Iop โˆ’op ๐‘‡)) = (((2 ยทop Iop ) โˆ’op (2 ยทop (๐นโ€˜๐‘˜))) โˆ’op (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)))))
82 halfcn 12364 . . . . . . . . . . . 12 (1 / 2) โˆˆ โ„‚
83 homulcl 30587 . . . . . . . . . . . 12 (((1 / 2) โˆˆ โ„‚ โˆง (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))): โ„‹โŸถ โ„‹) โ†’ ((1 / 2) ยทop (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)))): โ„‹โŸถ โ„‹)
8482, 44, 83sylancr 587 . . . . . . . . . . 11 (๐‘˜ โˆˆ โ„• โ†’ ((1 / 2) ยทop (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)))): โ„‹โŸถ โ„‹)
85 hoadddi 30631 . . . . . . . . . . . 12 ((2 โˆˆ โ„‚ โˆง (๐นโ€˜๐‘˜): โ„‹โŸถ โ„‹ โˆง ((1 / 2) ยทop (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)))): โ„‹โŸถ โ„‹) โ†’ (2 ยทop ((๐นโ€˜๐‘˜) +op ((1 / 2) ยทop (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)))))) = ((2 ยทop (๐นโ€˜๐‘˜)) +op (2 ยทop ((1 / 2) ยทop (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)))))))
8634, 85mp3an1 1448 . . . . . . . . . . 11 (((๐นโ€˜๐‘˜): โ„‹โŸถ โ„‹ โˆง ((1 / 2) ยทop (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)))): โ„‹โŸถ โ„‹) โ†’ (2 ยทop ((๐นโ€˜๐‘˜) +op ((1 / 2) ยทop (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)))))) = ((2 ยทop (๐นโ€˜๐‘˜)) +op (2 ยทop ((1 / 2) ยทop (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)))))))
8736, 84, 86syl2anc 584 . . . . . . . . . 10 (๐‘˜ โˆˆ โ„• โ†’ (2 ยทop ((๐นโ€˜๐‘˜) +op ((1 / 2) ยทop (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)))))) = ((2 ยทop (๐นโ€˜๐‘˜)) +op (2 ยทop ((1 / 2) ยทop (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)))))))
88 2ne0 12253 . . . . . . . . . . . . . 14 2 โ‰  0
8934, 88recidi 11882 . . . . . . . . . . . . 13 (2 ยท (1 / 2)) = 1
9089oveq1i 7363 . . . . . . . . . . . 12 ((2 ยท (1 / 2)) ยทop (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)))) = (1 ยทop (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))))
91 homulass 30630 . . . . . . . . . . . . . 14 ((2 โˆˆ โ„‚ โˆง (1 / 2) โˆˆ โ„‚ โˆง (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))): โ„‹โŸถ โ„‹) โ†’ ((2 ยท (1 / 2)) ยทop (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)))) = (2 ยทop ((1 / 2) ยทop (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))))))
9234, 82, 91mp3an12 1451 . . . . . . . . . . . . 13 ((๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))): โ„‹โŸถ โ„‹ โ†’ ((2 ยท (1 / 2)) ยทop (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)))) = (2 ยทop ((1 / 2) ยทop (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))))))
9344, 92syl 17 . . . . . . . . . . . 12 (๐‘˜ โˆˆ โ„• โ†’ ((2 ยท (1 / 2)) ยทop (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)))) = (2 ยทop ((1 / 2) ยทop (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))))))
94 homulid2 30628 . . . . . . . . . . . . 13 ((๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))): โ„‹โŸถ โ„‹ โ†’ (1 ยทop (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)))) = (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))))
9544, 94syl 17 . . . . . . . . . . . 12 (๐‘˜ โˆˆ โ„• โ†’ (1 ยทop (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)))) = (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))))
9690, 93, 953eqtr3a 2800 . . . . . . . . . . 11 (๐‘˜ โˆˆ โ„• โ†’ (2 ยทop ((1 / 2) ยทop (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))))) = (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))))
9796oveq2d 7369 . . . . . . . . . 10 (๐‘˜ โˆˆ โ„• โ†’ ((2 ยทop (๐นโ€˜๐‘˜)) +op (2 ยทop ((1 / 2) ยทop (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)))))) = ((2 ยทop (๐นโ€˜๐‘˜)) +op (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)))))
9887, 97eqtrd 2776 . . . . . . . . 9 (๐‘˜ โˆˆ โ„• โ†’ (2 ยทop ((๐นโ€˜๐‘˜) +op ((1 / 2) ยทop (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)))))) = ((2 ยทop (๐นโ€˜๐‘˜)) +op (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)))))
9998oveq2d 7369 . . . . . . . 8 (๐‘˜ โˆˆ โ„• โ†’ ((2 ยทop Iop ) โˆ’op (2 ยทop ((๐นโ€˜๐‘˜) +op ((1 / 2) ยทop (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))))))) = ((2 ยทop Iop ) โˆ’op ((2 ยทop (๐นโ€˜๐‘˜)) +op (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))))))
10051, 81, 993eqtr4d 2786 . . . . . . 7 (๐‘˜ โˆˆ โ„• โ†’ (( Iop +op (((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)) โˆ’op (2 ยทop (๐นโ€˜๐‘˜)))) +op ( Iop โˆ’op ๐‘‡)) = ((2 ยทop Iop ) โˆ’op (2 ยทop ((๐นโ€˜๐‘˜) +op ((1 / 2) ยทop (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))))))))
101 hoaddcl 30586 . . . . . . . . 9 (((๐นโ€˜๐‘˜): โ„‹โŸถ โ„‹ โˆง ((1 / 2) ยทop (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)))): โ„‹โŸถ โ„‹) โ†’ ((๐นโ€˜๐‘˜) +op ((1 / 2) ยทop (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))))): โ„‹โŸถ โ„‹)
10236, 84, 101syl2anc 584 . . . . . . . 8 (๐‘˜ โˆˆ โ„• โ†’ ((๐นโ€˜๐‘˜) +op ((1 / 2) ยทop (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))))): โ„‹โŸถ โ„‹)
103 hosubdi 30636 . . . . . . . . 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 ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))))))))
10434, 46, 103mp3an12 1451 . . . . . . . 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 ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))))))))
105102, 104syl 17 . . . . . . 7 (๐‘˜ โˆˆ โ„• โ†’ (2 ยทop ( Iop โˆ’op ((๐นโ€˜๐‘˜) +op ((1 / 2) ยทop (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))))))) = ((2 ยทop Iop ) โˆ’op (2 ยทop ((๐นโ€˜๐‘˜) +op ((1 / 2) ยทop (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))))))))
106100, 105eqtr4d 2779 . . . . . 6 (๐‘˜ โˆˆ โ„• โ†’ (( Iop +op (((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)) โˆ’op (2 ยทop (๐นโ€˜๐‘˜)))) +op ( Iop โˆ’op ๐‘‡)) = (2 ยทop ( Iop โˆ’op ((๐นโ€˜๐‘˜) +op ((1 / 2) ยทop (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))))))))
107 hosubcl 30601 . . . . . . . . . 10 (( Iop : โ„‹โŸถ โ„‹ โˆง (๐นโ€˜๐‘˜): โ„‹โŸถ โ„‹) โ†’ ( Iop โˆ’op (๐นโ€˜๐‘˜)): โ„‹โŸถ โ„‹)
10846, 36, 107sylancr 587 . . . . . . . . 9 (๐‘˜ โˆˆ โ„• โ†’ ( Iop โˆ’op (๐นโ€˜๐‘˜)): โ„‹โŸถ โ„‹)
109 hocsubdir 30613 . . . . . . . . . 10 (( Iop : โ„‹โŸถ โ„‹ โˆง (๐นโ€˜๐‘˜): โ„‹โŸถ โ„‹ โˆง ( Iop โˆ’op (๐นโ€˜๐‘˜)): โ„‹โŸถ โ„‹) โ†’ (( Iop โˆ’op (๐นโ€˜๐‘˜)) โˆ˜ ( Iop โˆ’op (๐นโ€˜๐‘˜))) = (( Iop โˆ˜ ( Iop โˆ’op (๐นโ€˜๐‘˜))) โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ ( Iop โˆ’op (๐นโ€˜๐‘˜)))))
11046, 109mp3an1 1448 . . . . . . . . 9 (((๐นโ€˜๐‘˜): โ„‹โŸถ โ„‹ โˆง ( Iop โˆ’op (๐นโ€˜๐‘˜)): โ„‹โŸถ โ„‹) โ†’ (( Iop โˆ’op (๐นโ€˜๐‘˜)) โˆ˜ ( Iop โˆ’op (๐นโ€˜๐‘˜))) = (( Iop โˆ˜ ( Iop โˆ’op (๐นโ€˜๐‘˜))) โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ ( Iop โˆ’op (๐นโ€˜๐‘˜)))))
11136, 108, 110syl2anc 584 . . . . . . . 8 (๐‘˜ โˆˆ โ„• โ†’ (( Iop โˆ’op (๐นโ€˜๐‘˜)) โˆ˜ ( Iop โˆ’op (๐นโ€˜๐‘˜))) = (( Iop โˆ˜ ( Iop โˆ’op (๐นโ€˜๐‘˜))) โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ ( Iop โˆ’op (๐นโ€˜๐‘˜)))))
112 hmoplin 30770 . . . . . . . . . . . . . . 15 ( Iop โˆˆ HrmOp โ†’ Iop โˆˆ LinOp)
11313, 112ax-mp 5 . . . . . . . . . . . . . 14 Iop โˆˆ LinOp
114 hoddi 30818 . . . . . . . . . . . . . 14 (( Iop โˆˆ LinOp โˆง Iop : โ„‹โŸถ โ„‹ โˆง (๐นโ€˜๐‘˜): โ„‹โŸถ โ„‹) โ†’ ( Iop โˆ˜ ( Iop โˆ’op (๐นโ€˜๐‘˜))) = (( Iop โˆ˜ Iop ) โˆ’op ( Iop โˆ˜ (๐นโ€˜๐‘˜))))
115113, 46, 114mp3an12 1451 . . . . . . . . . . . . 13 ((๐นโ€˜๐‘˜): โ„‹โŸถ โ„‹ โ†’ ( Iop โˆ˜ ( Iop โˆ’op (๐นโ€˜๐‘˜))) = (( Iop โˆ˜ Iop ) โˆ’op ( Iop โˆ˜ (๐นโ€˜๐‘˜))))
11636, 115syl 17 . . . . . . . . . . . 12 (๐‘˜ โˆˆ โ„• โ†’ ( Iop โˆ˜ ( Iop โˆ’op (๐นโ€˜๐‘˜))) = (( Iop โˆ˜ Iop ) โˆ’op ( Iop โˆ˜ (๐นโ€˜๐‘˜))))
11746hoid1i 30617 . . . . . . . . . . . . . 14 ( Iop โˆ˜ Iop ) = Iop
118117a1i 11 . . . . . . . . . . . . 13 (๐‘˜ โˆˆ โ„• โ†’ ( Iop โˆ˜ Iop ) = Iop )
119 hoico2 30585 . . . . . . . . . . . . . 14 ((๐นโ€˜๐‘˜): โ„‹โŸถ โ„‹ โ†’ ( Iop โˆ˜ (๐นโ€˜๐‘˜)) = (๐นโ€˜๐‘˜))
12036, 119syl 17 . . . . . . . . . . . . 13 (๐‘˜ โˆˆ โ„• โ†’ ( Iop โˆ˜ (๐นโ€˜๐‘˜)) = (๐นโ€˜๐‘˜))
121118, 120oveq12d 7371 . . . . . . . . . . . 12 (๐‘˜ โˆˆ โ„• โ†’ (( Iop โˆ˜ Iop ) โˆ’op ( Iop โˆ˜ (๐นโ€˜๐‘˜))) = ( Iop โˆ’op (๐นโ€˜๐‘˜)))
122116, 121eqtrd 2776 . . . . . . . . . . 11 (๐‘˜ โˆˆ โ„• โ†’ ( Iop โˆ˜ ( Iop โˆ’op (๐นโ€˜๐‘˜))) = ( Iop โˆ’op (๐นโ€˜๐‘˜)))
123 hmoplin 30770 . . . . . . . . . . . . . 14 ((๐นโ€˜๐‘˜) โˆˆ HrmOp โ†’ (๐นโ€˜๐‘˜) โˆˆ LinOp)
12415, 123syl 17 . . . . . . . . . . . . 13 (๐‘˜ โˆˆ โ„• โ†’ (๐นโ€˜๐‘˜) โˆˆ LinOp)
125 hoddi 30818 . . . . . . . . . . . . . 14 (((๐นโ€˜๐‘˜) โˆˆ LinOp โˆง Iop : โ„‹โŸถ โ„‹ โˆง (๐นโ€˜๐‘˜): โ„‹โŸถ โ„‹) โ†’ ((๐นโ€˜๐‘˜) โˆ˜ ( Iop โˆ’op (๐นโ€˜๐‘˜))) = (((๐นโ€˜๐‘˜) โˆ˜ Iop ) โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))))
12646, 125mp3an2 1449 . . . . . . . . . . . . 13 (((๐นโ€˜๐‘˜) โˆˆ LinOp โˆง (๐นโ€˜๐‘˜): โ„‹โŸถ โ„‹) โ†’ ((๐นโ€˜๐‘˜) โˆ˜ ( Iop โˆ’op (๐นโ€˜๐‘˜))) = (((๐นโ€˜๐‘˜) โˆ˜ Iop ) โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))))
127124, 36, 126syl2anc 584 . . . . . . . . . . . 12 (๐‘˜ โˆˆ โ„• โ†’ ((๐นโ€˜๐‘˜) โˆ˜ ( Iop โˆ’op (๐นโ€˜๐‘˜))) = (((๐นโ€˜๐‘˜) โˆ˜ Iop ) โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))))
128 hoico1 30584 . . . . . . . . . . . . . 14 ((๐นโ€˜๐‘˜): โ„‹โŸถ โ„‹ โ†’ ((๐นโ€˜๐‘˜) โˆ˜ Iop ) = (๐นโ€˜๐‘˜))
12936, 128syl 17 . . . . . . . . . . . . 13 (๐‘˜ โˆˆ โ„• โ†’ ((๐นโ€˜๐‘˜) โˆ˜ Iop ) = (๐นโ€˜๐‘˜))
130129oveq1d 7368 . . . . . . . . . . . 12 (๐‘˜ โˆˆ โ„• โ†’ (((๐นโ€˜๐‘˜) โˆ˜ Iop ) โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))) = ((๐นโ€˜๐‘˜) โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))))
131127, 130eqtrd 2776 . . . . . . . . . . 11 (๐‘˜ โˆˆ โ„• โ†’ ((๐นโ€˜๐‘˜) โˆ˜ ( Iop โˆ’op (๐นโ€˜๐‘˜))) = ((๐นโ€˜๐‘˜) โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))))
132122, 131oveq12d 7371 . . . . . . . . . 10 (๐‘˜ โˆˆ โ„• โ†’ (( Iop โˆ˜ ( Iop โˆ’op (๐นโ€˜๐‘˜))) โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ ( Iop โˆ’op (๐นโ€˜๐‘˜)))) = (( Iop โˆ’op (๐นโ€˜๐‘˜)) โˆ’op ((๐นโ€˜๐‘˜) โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)))))
13336, 46jctil 520 . . . . . . . . . . 11 (๐‘˜ โˆˆ โ„• โ†’ ( Iop : โ„‹โŸถ โ„‹ โˆง (๐นโ€˜๐‘˜): โ„‹โŸถ โ„‹))
134 hosubadd4 30642 . . . . . . . . . . 11 ((( Iop : โ„‹โŸถ โ„‹ โˆง (๐นโ€˜๐‘˜): โ„‹โŸถ โ„‹) โˆง ((๐นโ€˜๐‘˜): โ„‹โŸถ โ„‹ โˆง ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)): โ„‹โŸถ โ„‹)) โ†’ (( Iop โˆ’op (๐นโ€˜๐‘˜)) โˆ’op ((๐นโ€˜๐‘˜) โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)))) = (( Iop +op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))) โˆ’op ((๐นโ€˜๐‘˜) +op (๐นโ€˜๐‘˜))))
135133, 36, 42, 134syl12anc 835 . . . . . . . . . 10 (๐‘˜ โˆˆ โ„• โ†’ (( Iop โˆ’op (๐นโ€˜๐‘˜)) โˆ’op ((๐นโ€˜๐‘˜) โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)))) = (( Iop +op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))) โˆ’op ((๐นโ€˜๐‘˜) +op (๐นโ€˜๐‘˜))))
136132, 135eqtrd 2776 . . . . . . . . 9 (๐‘˜ โˆˆ โ„• โ†’ (( Iop โˆ˜ ( Iop โˆ’op (๐นโ€˜๐‘˜))) โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ ( Iop โˆ’op (๐นโ€˜๐‘˜)))) = (( Iop +op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))) โˆ’op ((๐นโ€˜๐‘˜) +op (๐นโ€˜๐‘˜))))
137 ho2times 30647 . . . . . . . . . . 11 ((๐นโ€˜๐‘˜): โ„‹โŸถ โ„‹ โ†’ (2 ยทop (๐นโ€˜๐‘˜)) = ((๐นโ€˜๐‘˜) +op (๐นโ€˜๐‘˜)))
13836, 137syl 17 . . . . . . . . . 10 (๐‘˜ โˆˆ โ„• โ†’ (2 ยทop (๐นโ€˜๐‘˜)) = ((๐นโ€˜๐‘˜) +op (๐นโ€˜๐‘˜)))
139138oveq2d 7369 . . . . . . . . 9 (๐‘˜ โˆˆ โ„• โ†’ (( Iop +op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))) โˆ’op (2 ยทop (๐นโ€˜๐‘˜))) = (( Iop +op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))) โˆ’op ((๐นโ€˜๐‘˜) +op (๐นโ€˜๐‘˜))))
140 hoaddsubass 30643 . . . . . . . . . . 11 (( Iop : โ„‹โŸถ โ„‹ โˆง ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)): โ„‹โŸถ โ„‹ โˆง (2 ยทop (๐นโ€˜๐‘˜)): โ„‹โŸถ โ„‹) โ†’ (( Iop +op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))) โˆ’op (2 ยทop (๐นโ€˜๐‘˜))) = ( Iop +op (((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)) โˆ’op (2 ยทop (๐นโ€˜๐‘˜)))))
14146, 140mp3an1 1448 . . . . . . . . . 10 ((((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)): โ„‹โŸถ โ„‹ โˆง (2 ยทop (๐นโ€˜๐‘˜)): โ„‹โŸถ โ„‹) โ†’ (( Iop +op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))) โˆ’op (2 ยทop (๐นโ€˜๐‘˜))) = ( Iop +op (((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)) โˆ’op (2 ยทop (๐นโ€˜๐‘˜)))))
14242, 38, 141syl2anc 584 . . . . . . . . 9 (๐‘˜ โˆˆ โ„• โ†’ (( Iop +op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))) โˆ’op (2 ยทop (๐นโ€˜๐‘˜))) = ( Iop +op (((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)) โˆ’op (2 ยทop (๐นโ€˜๐‘˜)))))
143136, 139, 1423eqtr2d 2782 . . . . . . . 8 (๐‘˜ โˆˆ โ„• โ†’ (( Iop โˆ˜ ( Iop โˆ’op (๐นโ€˜๐‘˜))) โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ ( Iop โˆ’op (๐นโ€˜๐‘˜)))) = ( Iop +op (((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)) โˆ’op (2 ยทop (๐นโ€˜๐‘˜)))))
144111, 143eqtrd 2776 . . . . . . 7 (๐‘˜ โˆˆ โ„• โ†’ (( Iop โˆ’op (๐นโ€˜๐‘˜)) โˆ˜ ( Iop โˆ’op (๐นโ€˜๐‘˜))) = ( Iop +op (((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)) โˆ’op (2 ยทop (๐นโ€˜๐‘˜)))))
145144oveq1d 7368 . . . . . 6 (๐‘˜ โˆˆ โ„• โ†’ ((( Iop โˆ’op (๐นโ€˜๐‘˜)) โˆ˜ ( Iop โˆ’op (๐นโ€˜๐‘˜))) +op ( Iop โˆ’op ๐‘‡)) = (( Iop +op (((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)) โˆ’op (2 ยทop (๐นโ€˜๐‘˜)))) +op ( Iop โˆ’op ๐‘‡)))
1467, 8, 9opsqrlem5 30972 . . . . . . . 8 (๐‘˜ โˆˆ โ„• โ†’ (๐นโ€˜(๐‘˜ + 1)) = ((๐นโ€˜๐‘˜) +op ((1 / 2) ยทop (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))))))
147146oveq2d 7369 . . . . . . 7 (๐‘˜ โˆˆ โ„• โ†’ ( Iop โˆ’op (๐นโ€˜(๐‘˜ + 1))) = ( Iop โˆ’op ((๐นโ€˜๐‘˜) +op ((1 / 2) ยทop (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜)))))))
148147oveq2d 7369 . . . . . 6 (๐‘˜ โˆˆ โ„• โ†’ (2 ยทop ( Iop โˆ’op (๐นโ€˜(๐‘˜ + 1)))) = (2 ยทop ( Iop โˆ’op ((๐นโ€˜๐‘˜) +op ((1 / 2) ยทop (๐‘‡ โˆ’op ((๐นโ€˜๐‘˜) โˆ˜ (๐นโ€˜๐‘˜))))))))
149106, 145, 1483eqtr4d 2786 . . . . 5 (๐‘˜ โˆˆ โ„• โ†’ ((( Iop โˆ’op (๐นโ€˜๐‘˜)) โˆ˜ ( Iop โˆ’op (๐นโ€˜๐‘˜))) +op ( Iop โˆ’op ๐‘‡)) = (2 ยทop ( Iop โˆ’op (๐นโ€˜(๐‘˜ + 1)))))
15033, 149breqtrd 5129 . . . 4 (๐‘˜ โˆˆ โ„• โ†’ 0hop โ‰คop (2 ยทop ( Iop โˆ’op (๐นโ€˜(๐‘˜ + 1)))))
151 peano2nn 12161 . . . . . . 7 (๐‘˜ โˆˆ โ„• โ†’ (๐‘˜ + 1) โˆˆ โ„•)
15214ffvelcdmi 7030 . . . . . . 7 ((๐‘˜ + 1) โˆˆ โ„• โ†’ (๐นโ€˜(๐‘˜ + 1)) โˆˆ HrmOp)
153151, 152syl 17 . . . . . 6 (๐‘˜ โˆˆ โ„• โ†’ (๐นโ€˜(๐‘˜ + 1)) โˆˆ HrmOp)
154 hmopd 30850 . . . . . 6 (( Iop โˆˆ HrmOp โˆง (๐นโ€˜(๐‘˜ + 1)) โˆˆ HrmOp) โ†’ ( Iop โˆ’op (๐นโ€˜(๐‘˜ + 1))) โˆˆ HrmOp)
15513, 153, 154sylancr 587 . . . . 5 (๐‘˜ โˆˆ โ„• โ†’ ( Iop โˆ’op (๐นโ€˜(๐‘˜ + 1))) โˆˆ HrmOp)
156 2re 12223 . . . . . 6 2 โˆˆ โ„
157 2pos 12252 . . . . . 6 0 < 2
158 leopmul 30962 . . . . . 6 ((2 โˆˆ โ„ โˆง ( Iop โˆ’op (๐นโ€˜(๐‘˜ + 1))) โˆˆ HrmOp โˆง 0 < 2) โ†’ ( 0hop โ‰คop ( Iop โˆ’op (๐นโ€˜(๐‘˜ + 1))) โ†” 0hop โ‰คop (2 ยทop ( Iop โˆ’op (๐นโ€˜(๐‘˜ + 1))))))
159156, 157, 158mp3an13 1452 . . . . 5 (( Iop โˆ’op (๐นโ€˜(๐‘˜ + 1))) โˆˆ HrmOp โ†’ ( 0hop โ‰คop ( Iop โˆ’op (๐นโ€˜(๐‘˜ + 1))) โ†” 0hop โ‰คop (2 ยทop ( Iop โˆ’op (๐นโ€˜(๐‘˜ + 1))))))
160155, 159syl 17 . . . 4 (๐‘˜ โˆˆ โ„• โ†’ ( 0hop โ‰คop ( Iop โˆ’op (๐นโ€˜(๐‘˜ + 1))) โ†” 0hop โ‰คop (2 ยทop ( Iop โˆ’op (๐นโ€˜(๐‘˜ + 1))))))
161150, 160mpbird 256 . . 3 (๐‘˜ โˆˆ โ„• โ†’ 0hop โ‰คop ( Iop โˆ’op (๐นโ€˜(๐‘˜ + 1))))
162 leop3 30953 . . . 4 (((๐นโ€˜(๐‘˜ + 1)) โˆˆ HrmOp โˆง Iop โˆˆ HrmOp) โ†’ ((๐นโ€˜(๐‘˜ + 1)) โ‰คop Iop โ†” 0hop โ‰คop ( Iop โˆ’op (๐นโ€˜(๐‘˜ + 1)))))
163153, 13, 162sylancl 586 . . 3 (๐‘˜ โˆˆ โ„• โ†’ ((๐นโ€˜(๐‘˜ + 1)) โ‰คop Iop โ†” 0hop โ‰คop ( Iop โˆ’op (๐นโ€˜(๐‘˜ + 1)))))
164161, 163mpbird 256 . 2 (๐‘˜ โˆˆ โ„• โ†’ (๐นโ€˜(๐‘˜ + 1)) โ‰คop Iop )
1652, 4, 6, 12, 164nn1suc 12171 1 (๐‘ โˆˆ โ„• โ†’ (๐นโ€˜๐‘) โ‰คop Iop )
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 396   = wceq 1541   โˆˆ wcel 2106  {csn 4584   class class class wbr 5103   ร— cxp 5629   โˆ˜ ccom 5635  โŸถwf 6489  โ€˜cfv 6493  (class class class)co 7353   โˆˆ cmpo 7355  โ„‚cc 11045  โ„cr 11046  0cc0 11047  1c1 11048   + caddc 11050   ยท cmul 11052   < clt 11185   / cdiv 11808  โ„•cn 12149  2c2 12204  seqcseq 13898   โ„‹chba 29747   +op chos 29766   ยทop chot 29767   โˆ’op chod 29768   0hop ch0o 29771   Iop chio 29772  LinOpclo 29775  HrmOpcho 29778   โ‰คop cleo 29786
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5240  ax-sep 5254  ax-nul 5261  ax-pow 5318  ax-pr 5382  ax-un 7668  ax-inf2 9573  ax-cc 10367  ax-cnex 11103  ax-resscn 11104  ax-1cn 11105  ax-icn 11106  ax-addcl 11107  ax-addrcl 11108  ax-mulcl 11109  ax-mulrcl 11110  ax-mulcom 11111  ax-addass 11112  ax-mulass 11113  ax-distr 11114  ax-i2m1 11115  ax-1ne0 11116  ax-1rid 11117  ax-rnegex 11118  ax-rrecex 11119  ax-cnre 11120  ax-pre-lttri 11121  ax-pre-lttrn 11122  ax-pre-ltadd 11123  ax-pre-mulgt0 11124  ax-pre-sup 11125  ax-addf 11126  ax-mulf 11127  ax-hilex 29827  ax-hfvadd 29828  ax-hvcom 29829  ax-hvass 29830  ax-hv0cl 29831  ax-hvaddid 29832  ax-hfvmul 29833  ax-hvmulid 29834  ax-hvmulass 29835  ax-hvdistr1 29836  ax-hvdistr2 29837  ax-hvmul0 29838  ax-hfi 29907  ax-his1 29910  ax-his2 29911  ax-his3 29912  ax-his4 29913  ax-hcompl 30030
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3351  df-reu 3352  df-rab 3406  df-v 3445  df-sbc 3738  df-csb 3854  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-nul 4281  df-if 4485  df-pw 4560  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4591  df-uni 4864  df-int 4906  df-iun 4954  df-iin 4955  df-br 5104  df-opab 5166  df-mpt 5187  df-tr 5221  df-id 5529  df-eprel 5535  df-po 5543  df-so 5544  df-fr 5586  df-se 5587  df-we 5588  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6251  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-iota 6445  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-isom 6502  df-riota 7309  df-ov 7356  df-oprab 7357  df-mpo 7358  df-of 7613  df-om 7799  df-1st 7917  df-2nd 7918  df-supp 8089  df-frecs 8208  df-wrecs 8239  df-recs 8313  df-rdg 8352  df-1o 8408  df-2o 8409  df-oadd 8412  df-omul 8413  df-er 8644  df-map 8763  df-pm 8764  df-ixp 8832  df-en 8880  df-dom 8881  df-sdom 8882  df-fin 8883  df-fsupp 9302  df-fi 9343  df-sup 9374  df-inf 9375  df-oi 9442  df-card 9871  df-acn 9874  df-pnf 11187  df-mnf 11188  df-xr 11189  df-ltxr 11190  df-le 11191  df-sub 11383  df-neg 11384  df-div 11809  df-nn 12150  df-2 12212  df-3 12213  df-4 12214  df-5 12215  df-6 12216  df-7 12217  df-8 12218  df-9 12219  df-n0 12410  df-z 12496  df-dec 12615  df-uz 12760  df-q 12866  df-rp 12908  df-xneg 13025  df-xadd 13026  df-xmul 13027  df-ioo 13260  df-ico 13262  df-icc 13263  df-fz 13417  df-fzo 13560  df-fl 13689  df-seq 13899  df-exp 13960  df-hash 14223  df-cj 14976  df-re 14977  df-im 14978  df-sqrt 15112  df-abs 15113  df-clim 15362  df-rlim 15363  df-sum 15563  df-struct 17011  df-sets 17028  df-slot 17046  df-ndx 17058  df-base 17076  df-ress 17105  df-plusg 17138  df-mulr 17139  df-starv 17140  df-sca 17141  df-vsca 17142  df-ip 17143  df-tset 17144  df-ple 17145  df-ds 17147  df-unif 17148  df-hom 17149  df-cco 17150  df-rest 17296  df-topn 17297  df-0g 17315  df-gsum 17316  df-topgen 17317  df-pt 17318  df-prds 17321  df-xrs 17376  df-qtop 17381  df-imas 17382  df-xps 17384  df-mre 17458  df-mrc 17459  df-acs 17461  df-mgm 18489  df-sgrp 18538  df-mnd 18549  df-submnd 18594  df-mulg 18864  df-cntz 19088  df-cmn 19555  df-psmet 20773  df-xmet 20774  df-met 20775  df-bl 20776  df-mopn 20777  df-fbas 20778  df-fg 20779  df-cnfld 20782  df-top 22227  df-topon 22244  df-topsp 22266  df-bases 22280  df-cld 22354  df-ntr 22355  df-cls 22356  df-nei 22433  df-cn 22562  df-cnp 22563  df-lm 22564  df-haus 22650  df-tx 22897  df-hmeo 23090  df-fil 23181  df-fm 23273  df-flim 23274  df-flf 23275  df-xms 23657  df-ms 23658  df-tms 23659  df-cfil 24603  df-cau 24604  df-cmet 24605  df-grpo 29321  df-gid 29322  df-ginv 29323  df-gdiv 29324  df-ablo 29373  df-vc 29387  df-nv 29420  df-va 29423  df-ba 29424  df-sm 29425  df-0v 29426  df-vs 29427  df-nmcv 29428  df-ims 29429  df-dip 29529  df-ssp 29550  df-ph 29641  df-cbn 29691  df-hnorm 29796  df-hba 29797  df-hvsub 29799  df-hlim 29800  df-hcau 29801  df-sh 30035  df-ch 30049  df-oc 30080  df-ch0 30081  df-shs 30136  df-pjh 30223  df-hosum 30558  df-homul 30559  df-hodif 30560  df-h0op 30576  df-iop 30577  df-lnop 30669  df-hmop 30672  df-leop 30680
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator