:: FDIFF_11 semantic presentation

REAL is V1() V46() V47() V48() V52() V62() set
NAT is V46() V47() V48() V49() V50() V51() V52() Element of K6(REAL)
K6(REAL) is set
COMPLEX is V1() V46() V52() V62() set
0 is set
1 is V1() V10() V11() V12() ext-real positive non negative V46() V47() V48() V49() V50() V51() V60() V61() Element of NAT
{0,1} is set
K7(REAL,REAL) is V36() V37() V38() set
K6(K7(REAL,REAL)) is set
K7(NAT,REAL) is V36() V37() V38() set
K6(K7(NAT,REAL)) is set
K7(NAT,COMPLEX) is V36() set
K6(K7(NAT,COMPLEX)) is set
K7(COMPLEX,COMPLEX) is V36() set
K6(K7(COMPLEX,COMPLEX)) is set
NAT is V46() V47() V48() V49() V50() V51() V52() set
K6(NAT) is set
K6(NAT) is set
INT is V1() V46() V47() V48() V49() V50() V52() V62() set
K7(1,1) is V23( RAT ) V23( INT ) V36() V37() V38() V39() set
RAT is V1() V46() V47() V48() V49() V52() V62() set
K6(K7(1,1)) is set
K7(K7(1,1),1) is V23( RAT ) V23( INT ) V36() V37() V38() V39() set
K6(K7(K7(1,1),1)) is set
K7(K7(1,1),REAL) is V36() V37() V38() set
K6(K7(K7(1,1),REAL)) is set
K7(K7(REAL,REAL),REAL) is V36() V37() V38() set
K6(K7(K7(REAL,REAL),REAL)) is set
2 is V1() V10() V11() V12() ext-real positive non negative V46() V47() V48() V49() V50() V51() V60() V61() Element of NAT
K7(2,2) is V23( RAT ) V23( INT ) V36() V37() V38() V39() set
K7(K7(2,2),REAL) is V36() V37() V38() set
K6(K7(K7(2,2),REAL)) is set
K427(2) is V180() L15()
the U1 of K427(2) is set
K485() is L6()
the U1 of K485() is set
K321() is V115() L7()
K490() is V89() L6()
K492() is M13(K490())
K470(K492(),K492()) is V88() V89() L6()
the U1 of K470(K492(),K492()) is set
PFuncs (REAL,REAL) is set
K7(NAT,(PFuncs (REAL,REAL))) is set
K6(K7(NAT,(PFuncs (REAL,REAL)))) is set
0 is V10() V11() V12() ext-real V46() V47() V48() V49() V50() V51() V60() V61() Element of NAT
sin is V19() V22( REAL ) V23( REAL ) V24() V33( REAL , REAL ) V36() V37() V38() Element of K6(K7(REAL,REAL))
dom sin is V46() V47() V48() Element of K6(REAL)
cos is V19() V22( REAL ) V23( REAL ) V24() V33( REAL , REAL ) V36() V37() V38() Element of K6(K7(REAL,REAL))
dom cos is V46() V47() V48() Element of K6(REAL)
exp_R is V19() V22( REAL ) V23( REAL ) V24() V33( REAL , REAL ) V36() V37() V38() Element of K6(K7(REAL,REAL))
PI is V1() V11() V12() ext-real positive non negative set
tan is V19() V22( REAL ) V23( REAL ) V24() V36() V37() V38() Element of K6(K7(REAL,REAL))
sin / cos is V19() V22( REAL ) V23( REAL ) V24() V36() V37() V38() Element of K6(K7(REAL,REAL))
4 is V1() V10() V11() V12() ext-real positive non negative V46() V47() V48() V49() V50() V51() V60() V61() Element of NAT
].0,4.[ is open V46() V47() V48() Element of K6(REAL)
cos / sin is V19() V22( REAL ) V23( REAL ) V24() V36() V37() V38() Element of K6(K7(REAL,REAL))
{0} is V46() V47() V48() V49() V50() V51() set
[#] REAL is V46() V47() V48() Element of K6(REAL)
dom exp_R is V46() V47() V48() Element of K6(REAL)
rng exp_R is V46() V47() V48() Element of K6(REAL)
K514(0) is V46() V47() V48() Element of K6(REAL)
sec is V19() V22( REAL ) V23( REAL ) V24() V36() V37() V38() Element of K6(K7(REAL,REAL))
cos ^ is V19() V22( REAL ) V23( REAL ) V24() V36() V37() V38() Element of K6(K7(REAL,REAL))
cosec is V19() V22( REAL ) V23( REAL ) V24() V36() V37() V38() Element of K6(K7(REAL,REAL))
sin ^ is V19() V22( REAL ) V23( REAL ) V24() V36() V37() V38() Element of K6(K7(REAL,REAL))
- 1 is V1() V11() V12() ext-real non positive negative V60() Element of REAL
[.(- 1),1.] is closed V46() V47() V48() Element of K6(REAL)
arctan is V19() V22( REAL ) V23( REAL ) V24() V36() V37() V38() Element of K6(K7(REAL,REAL))
dom arctan is V46() V47() V48() Element of K6(REAL)
arccot is V19() V22( REAL ) V23( REAL ) V24() V36() V37() V38() Element of K6(K7(REAL,REAL))
dom arccot is V46() V47() V48() Element of K6(REAL)
arccot | [.(- 1),1.] is V19() V22( REAL ) V23( REAL ) V24() V36() V37() V38() Element of K6(K7(REAL,REAL))
rng (arccot | [.(- 1),1.]) is V46() V47() V48() Element of K6(REAL)
PI is V1() V11() V12() ext-real positive non negative Element of REAL
PI / 4 is V1() V11() V12() ext-real positive non negative Element of REAL
K39(4) is V1() V11() V12() ext-real positive non negative set
K37(PI,K39(4)) is V1() V11() V12() ext-real positive non negative set
3 is V1() V10() V11() V12() ext-real positive non negative V46() V47() V48() V49() V50() V51() V60() V61() Element of NAT
3 / 4 is V1() V11() V12() ext-real positive non negative Element of REAL
K37(3,K39(4)) is V1() V11() V12() ext-real positive non negative set
(3 / 4) * PI is V1() V11() V12() ext-real positive non negative Element of REAL
[.(PI / 4),((3 / 4) * PI).] is closed V46() V47() V48() Element of K6(REAL)
].(- 1),1.[ is open V46() V47() V48() Element of K6(REAL)
dom tan is V46() V47() V48() Element of K6(REAL)
cot is V19() V22( REAL ) V23( REAL ) V24() V36() V37() V38() Element of K6(K7(REAL,REAL))
dom cot is V46() V47() V48() Element of K6(REAL)
arctan * sin is V19() V22( REAL ) V23( REAL ) V24() V36() V37() V38() Element of K6(K7(REAL,REAL))
dom (arctan * sin) is V46() V47() V48() Element of K6(REAL)
Z is open V46() V47() V48() Element of K6(REAL)
(arctan * sin) `| Z is V19() V22( REAL ) V23( REAL ) V24() V36() V37() V38() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((arctan * sin) `| Z) . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is V11() V12() ext-real set
1 + ((sin . x) ^2) is V11() V12() ext-real Element of REAL
(cos . x) / (1 + ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
K39((1 + ((sin . x) ^2))) is V11() V12() ext-real set
K37((cos . x),K39((1 + ((sin . x) ^2)))) is V11() V12() ext-real set
diff ((arctan * sin),x) is V11() V12() ext-real Element of REAL
diff (sin,x) is V11() V12() ext-real Element of REAL
(diff (sin,x)) / (1 + ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
K37((diff (sin,x)),K39((1 + ((sin . x) ^2)))) is V11() V12() ext-real set
x is V11() V12() ext-real Element of REAL
((arctan * sin) `| Z) . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is V11() V12() ext-real set
1 + ((sin . x) ^2) is V11() V12() ext-real Element of REAL
(cos . x) / (1 + ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
K39((1 + ((sin . x) ^2))) is V11() V12() ext-real set
K37((cos . x),K39((1 + ((sin . x) ^2)))) is V11() V12() ext-real set
arccot * sin is V19() V22( REAL ) V23( REAL ) V24() V36() V37() V38() Element of K6(K7(REAL,REAL))
dom (arccot * sin) is V46() V47() V48() Element of K6(REAL)
Z is open V46() V47() V48() Element of K6(REAL)
(arccot * sin) `| Z is V19() V22( REAL ) V23( REAL ) V24() V36() V37() V38() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((arccot * sin) `| Z) . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is V11() V12() ext-real set
1 + ((sin . x) ^2) is V11() V12() ext-real Element of REAL
(cos . x) / (1 + ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
K39((1 + ((sin . x) ^2))) is V11() V12() ext-real set
K37((cos . x),K39((1 + ((sin . x) ^2)))) is V11() V12() ext-real set
- ((cos . x) / (1 + ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
diff ((arccot * sin),x) is V11() V12() ext-real Element of REAL
diff (sin,x) is V11() V12() ext-real Element of REAL
(diff (sin,x)) / (1 + ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
K37((diff (sin,x)),K39((1 + ((sin . x) ^2)))) is V11() V12() ext-real set
- ((diff (sin,x)) / (1 + ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((arccot * sin) `| Z) . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is V11() V12() ext-real set
1 + ((sin . x) ^2) is V11() V12() ext-real Element of REAL
(cos . x) / (1 + ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
K39((1 + ((sin . x) ^2))) is V11() V12() ext-real set
K37((cos . x),K39((1 + ((sin . x) ^2)))) is V11() V12() ext-real set
- ((cos . x) / (1 + ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
arctan * cos is V19() V22( REAL ) V23( REAL ) V24() V36() V37() V38() Element of K6(K7(REAL,REAL))
dom (arctan * cos) is V46() V47() V48() Element of K6(REAL)
Z is open V46() V47() V48() Element of K6(REAL)
(arctan * cos) `| Z is V19() V22( REAL ) V23( REAL ) V24() V36() V37() V38() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((arctan * cos) `| Z) . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is V11() V12() ext-real set
1 + ((cos . x) ^2) is V11() V12() ext-real Element of REAL
(sin . x) / (1 + ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
K39((1 + ((cos . x) ^2))) is V11() V12() ext-real set
K37((sin . x),K39((1 + ((cos . x) ^2)))) is V11() V12() ext-real set
- ((sin . x) / (1 + ((cos . x) ^2))) is V11() V12() ext-real Element of REAL
diff ((arctan * cos),x) is V11() V12() ext-real Element of REAL
diff (cos,x) is V11() V12() ext-real Element of REAL
(diff (cos,x)) / (1 + ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
K37((diff (cos,x)),K39((1 + ((cos . x) ^2)))) is V11() V12() ext-real set
- (sin . x) is V11() V12() ext-real Element of REAL
(- (sin . x)) / (1 + ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
K37((- (sin . x)),K39((1 + ((cos . x) ^2)))) is V11() V12() ext-real set
x is V11() V12() ext-real Element of REAL
((arctan * cos) `| Z) . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is V11() V12() ext-real set
1 + ((cos . x) ^2) is V11() V12() ext-real Element of REAL
(sin . x) / (1 + ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
K39((1 + ((cos . x) ^2))) is V11() V12() ext-real set
K37((sin . x),K39((1 + ((cos . x) ^2)))) is V11() V12() ext-real set
- ((sin . x) / (1 + ((cos . x) ^2))) is V11() V12() ext-real Element of REAL
arccot * cos is V19() V22( REAL ) V23( REAL ) V24() V36() V37() V38() Element of K6(K7(REAL,REAL))
dom (arccot * cos) is V46() V47() V48() Element of K6(REAL)
Z is open V46() V47() V48() Element of K6(REAL)
(arccot * cos) `| Z is V19() V22( REAL ) V23( REAL ) V24() V36() V37() V38() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((arccot * cos) `| Z) . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is V11() V12() ext-real set
1 + ((cos . x) ^2) is V11() V12() ext-real Element of REAL
(sin . x) / (1 + ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
K39((1 + ((cos . x) ^2))) is V11() V12() ext-real set
K37((sin . x),K39((1 + ((cos . x) ^2)))) is V11() V12() ext-real set
diff ((arccot * cos),x) is V11() V12() ext-real Element of REAL
diff (cos,x) is V11() V12() ext-real Element of REAL
(diff (cos,x)) / (1 + ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
K37((diff (cos,x)),K39((1 + ((cos . x) ^2)))) is V11() V12() ext-real set
- ((diff (cos,x)) / (1 + ((cos . x) ^2))) is V11() V12() ext-real Element of REAL
- (sin . x) is V11() V12() ext-real Element of REAL
(- (sin . x)) / (1 + ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
K37((- (sin . x)),K39((1 + ((cos . x) ^2)))) is V11() V12() ext-real set
- ((- (sin . x)) / (1 + ((cos . x) ^2))) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((arccot * cos) `| Z) . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is V11() V12() ext-real set
1 + ((cos . x) ^2) is V11() V12() ext-real Element of REAL
(sin . x) / (1 + ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
K39((1 + ((cos . x) ^2))) is V11() V12() ext-real set
K37((sin . x),K39((1 + ((cos . x) ^2)))) is V11() V12() ext-real set
arctan * tan is V19() V22( REAL ) V23( REAL ) V24() V36() V37() V38() Element of K6(K7(REAL,REAL))
dom (arctan * tan) is V46() V47() V48() Element of K6(REAL)
Z is open V46() V47() V48() Element of K6(REAL)
(arctan * tan) `| Z is V19() V22( REAL ) V23( REAL ) V24() V36() V37() V38() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
tan . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((arctan * tan) `| Z) . x is V11() V12() ext-real Element of REAL
tan . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(sin . x) / (cos . x) is V11() V12() ext-real Element of REAL
K39((cos . x)) is V11() V12() ext-real set
K37((sin . x),K39((cos . x))) is V11() V12() ext-real set
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is V11() V12() ext-real set
diff ((arctan * tan),x) is V11() V12() ext-real Element of REAL
diff (tan,x) is V11() V12() ext-real Element of REAL
(tan . x) ^2 is V11() V12() ext-real Element of REAL
K37((tan . x),(tan . x)) is V11() V12() ext-real set
1 + ((tan . x) ^2) is V11() V12() ext-real Element of REAL
(diff (tan,x)) / (1 + ((tan . x) ^2)) is V11() V12() ext-real Element of REAL
K39((1 + ((tan . x) ^2))) is V11() V12() ext-real set
K37((diff (tan,x)),K39((1 + ((tan . x) ^2)))) is V11() V12() ext-real set
1 / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() V12() ext-real set
K37(1,K39(((cos . x) ^2))) is V11() V12() ext-real set
(1 / ((cos . x) ^2)) / (1 + ((tan . x) ^2)) is V11() V12() ext-real Element of REAL
K37((1 / ((cos . x) ^2)),K39((1 + ((tan . x) ^2)))) is V11() V12() ext-real set
((sin . x) / (cos . x)) * ((sin . x) / (cos . x)) is V11() V12() ext-real Element of REAL
1 + (((sin . x) / (cos . x)) * ((sin . x) / (cos . x))) is V11() V12() ext-real Element of REAL
((cos . x) ^2) * (1 + (((sin . x) / (cos . x)) * ((sin . x) / (cos . x)))) is V11() V12() ext-real Element of REAL
1 / (((cos . x) ^2) * (1 + (((sin . x) / (cos . x)) * ((sin . x) / (cos . x))))) is V11() V12() ext-real Element of REAL
K39((((cos . x) ^2) * (1 + (((sin . x) / (cos . x)) * ((sin . x) / (cos . x)))))) is V11() V12() ext-real set
K37(1,K39((((cos . x) ^2) * (1 + (((sin . x) / (cos . x)) * ((sin . x) / (cos . x))))))) is V11() V12() ext-real set
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is V11() V12() ext-real set
((sin . x) ^2) / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K37(((sin . x) ^2),K39(((cos . x) ^2))) is V11() V12() ext-real set
1 + (((sin . x) ^2) / ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
((cos . x) ^2) * (1 + (((sin . x) ^2) / ((cos . x) ^2))) is V11() V12() ext-real Element of REAL
1 / (((cos . x) ^2) * (1 + (((sin . x) ^2) / ((cos . x) ^2)))) is V11() V12() ext-real Element of REAL
K39((((cos . x) ^2) * (1 + (((sin . x) ^2) / ((cos . x) ^2))))) is V11() V12() ext-real set
K37(1,K39((((cos . x) ^2) * (1 + (((sin . x) ^2) / ((cos . x) ^2)))))) is V11() V12() ext-real set
((cos . x) ^2) * ((sin . x) ^2) is V11() V12() ext-real Element of REAL
(((cos . x) ^2) * ((sin . x) ^2)) / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K37((((cos . x) ^2) * ((sin . x) ^2)),K39(((cos . x) ^2))) is V11() V12() ext-real set
((cos . x) ^2) + ((((cos . x) ^2) * ((sin . x) ^2)) / ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
1 / (((cos . x) ^2) + ((((cos . x) ^2) * ((sin . x) ^2)) / ((cos . x) ^2))) is V11() V12() ext-real Element of REAL
K39((((cos . x) ^2) + ((((cos . x) ^2) * ((sin . x) ^2)) / ((cos . x) ^2)))) is V11() V12() ext-real set
K37(1,K39((((cos . x) ^2) + ((((cos . x) ^2) * ((sin . x) ^2)) / ((cos . x) ^2))))) is V11() V12() ext-real set
((cos . x) ^2) + ((sin . x) ^2) is V11() V12() ext-real Element of REAL
1 / (((cos . x) ^2) + ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
K39((((cos . x) ^2) + ((sin . x) ^2))) is V11() V12() ext-real set
K37(1,K39((((cos . x) ^2) + ((sin . x) ^2)))) is V11() V12() ext-real set
1 / 1 is V1() V11() V12() ext-real positive non negative Element of REAL
K39(1) is V1() V11() V12() ext-real positive non negative set
K37(1,K39(1)) is V1() V11() V12() ext-real positive non negative set
x is V11() V12() ext-real Element of REAL
((arctan * tan) `| Z) . x is V11() V12() ext-real Element of REAL
arccot * tan is V19() V22( REAL ) V23( REAL ) V24() V36() V37() V38() Element of K6(K7(REAL,REAL))
dom (arccot * tan) is V46() V47() V48() Element of K6(REAL)
Z is open V46() V47() V48() Element of K6(REAL)
(arccot * tan) `| Z is V19() V22( REAL ) V23( REAL ) V24() V36() V37() V38() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
tan . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((arccot * tan) `| Z) . x is V11() V12() ext-real Element of REAL
tan . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(sin . x) / (cos . x) is V11() V12() ext-real Element of REAL
K39((cos . x)) is V11() V12() ext-real set
K37((sin . x),K39((cos . x))) is V11() V12() ext-real set
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is V11() V12() ext-real set
diff ((arccot * tan),x) is V11() V12() ext-real Element of REAL
diff (tan,x) is V11() V12() ext-real Element of REAL
(tan . x) ^2 is V11() V12() ext-real Element of REAL
K37((tan . x),(tan . x)) is V11() V12() ext-real set
1 + ((tan . x) ^2) is V11() V12() ext-real Element of REAL
(diff (tan,x)) / (1 + ((tan . x) ^2)) is V11() V12() ext-real Element of REAL
K39((1 + ((tan . x) ^2))) is V11() V12() ext-real set
K37((diff (tan,x)),K39((1 + ((tan . x) ^2)))) is V11() V12() ext-real set
- ((diff (tan,x)) / (1 + ((tan . x) ^2))) is V11() V12() ext-real Element of REAL
1 / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() V12() ext-real set
K37(1,K39(((cos . x) ^2))) is V11() V12() ext-real set
(1 / ((cos . x) ^2)) / (1 + ((tan . x) ^2)) is V11() V12() ext-real Element of REAL
K37((1 / ((cos . x) ^2)),K39((1 + ((tan . x) ^2)))) is V11() V12() ext-real set
- ((1 / ((cos . x) ^2)) / (1 + ((tan . x) ^2))) is V11() V12() ext-real Element of REAL
((sin . x) / (cos . x)) * ((sin . x) / (cos . x)) is V11() V12() ext-real Element of REAL
1 + (((sin . x) / (cos . x)) * ((sin . x) / (cos . x))) is V11() V12() ext-real Element of REAL
((cos . x) ^2) * (1 + (((sin . x) / (cos . x)) * ((sin . x) / (cos . x)))) is V11() V12() ext-real Element of REAL
1 / (((cos . x) ^2) * (1 + (((sin . x) / (cos . x)) * ((sin . x) / (cos . x))))) is V11() V12() ext-real Element of REAL
K39((((cos . x) ^2) * (1 + (((sin . x) / (cos . x)) * ((sin . x) / (cos . x)))))) is V11() V12() ext-real set
K37(1,K39((((cos . x) ^2) * (1 + (((sin . x) / (cos . x)) * ((sin . x) / (cos . x))))))) is V11() V12() ext-real set
- (1 / (((cos . x) ^2) * (1 + (((sin . x) / (cos . x)) * ((sin . x) / (cos . x)))))) is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is V11() V12() ext-real set
((sin . x) ^2) / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K37(((sin . x) ^2),K39(((cos . x) ^2))) is V11() V12() ext-real set
1 + (((sin . x) ^2) / ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
((cos . x) ^2) * (1 + (((sin . x) ^2) / ((cos . x) ^2))) is V11() V12() ext-real Element of REAL
1 / (((cos . x) ^2) * (1 + (((sin . x) ^2) / ((cos . x) ^2)))) is V11() V12() ext-real Element of REAL
K39((((cos . x) ^2) * (1 + (((sin . x) ^2) / ((cos . x) ^2))))) is V11() V12() ext-real set
K37(1,K39((((cos . x) ^2) * (1 + (((sin . x) ^2) / ((cos . x) ^2)))))) is V11() V12() ext-real set
- (1 / (((cos . x) ^2) * (1 + (((sin . x) ^2) / ((cos . x) ^2))))) is V11() V12() ext-real Element of REAL
((cos . x) ^2) * ((sin . x) ^2) is V11() V12() ext-real Element of REAL
(((cos . x) ^2) * ((sin . x) ^2)) / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K37((((cos . x) ^2) * ((sin . x) ^2)),K39(((cos . x) ^2))) is V11() V12() ext-real set
((cos . x) ^2) + ((((cos . x) ^2) * ((sin . x) ^2)) / ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
1 / (((cos . x) ^2) + ((((cos . x) ^2) * ((sin . x) ^2)) / ((cos . x) ^2))) is V11() V12() ext-real Element of REAL
K39((((cos . x) ^2) + ((((cos . x) ^2) * ((sin . x) ^2)) / ((cos . x) ^2)))) is V11() V12() ext-real set
K37(1,K39((((cos . x) ^2) + ((((cos . x) ^2) * ((sin . x) ^2)) / ((cos . x) ^2))))) is V11() V12() ext-real set
- (1 / (((cos . x) ^2) + ((((cos . x) ^2) * ((sin . x) ^2)) / ((cos . x) ^2)))) is V11() V12() ext-real Element of REAL
((cos . x) ^2) + ((sin . x) ^2) is V11() V12() ext-real Element of REAL
1 / (((cos . x) ^2) + ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
K39((((cos . x) ^2) + ((sin . x) ^2))) is V11() V12() ext-real set
K37(1,K39((((cos . x) ^2) + ((sin . x) ^2)))) is V11() V12() ext-real set
- (1 / (((cos . x) ^2) + ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
1 / 1 is V1() V11() V12() ext-real positive non negative Element of REAL
K39(1) is V1() V11() V12() ext-real positive non negative set
K37(1,K39(1)) is V1() V11() V12() ext-real positive non negative set
- (1 / 1) is V1() V11() V12() ext-real non positive negative Element of REAL
x is V11() V12() ext-real Element of REAL
((arccot * tan) `| Z) . x is V11() V12() ext-real Element of REAL
arctan * cot is V19() V22( REAL ) V23( REAL ) V24() V36() V37() V38() Element of K6(K7(REAL,REAL))
dom (arctan * cot) is V46() V47() V48() Element of K6(REAL)
Z is open V46() V47() V48() Element of K6(REAL)
(arctan * cot) `| Z is V19() V22( REAL ) V23( REAL ) V24() V36() V37() V38() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((arctan * cot) `| Z) . x is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(cos . x) / (sin . x) is V11() V12() ext-real Element of REAL
K39((sin . x)) is V11() V12() ext-real set
K37((cos . x),K39((sin . x))) is V11() V12() ext-real set
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is V11() V12() ext-real set
diff ((arctan * cot),x) is V11() V12() ext-real Element of REAL
diff (cot,x) is V11() V12() ext-real Element of REAL
(cot . x) ^2 is V11() V12() ext-real Element of REAL
K37((cot . x),(cot . x)) is V11() V12() ext-real set
1 + ((cot . x) ^2) is V11() V12() ext-real Element of REAL
(diff (cot,x)) / (1 + ((cot . x) ^2)) is V11() V12() ext-real Element of REAL
K39((1 + ((cot . x) ^2))) is V11() V12() ext-real set
K37((diff (cot,x)),K39((1 + ((cot . x) ^2)))) is V11() V12() ext-real set
1 / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() V12() ext-real set
K37(1,K39(((sin . x) ^2))) is V11() V12() ext-real set
- (1 / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
(- (1 / ((sin . x) ^2))) / (1 + ((cot . x) ^2)) is V11() V12() ext-real Element of REAL
K37((- (1 / ((sin . x) ^2))),K39((1 + ((cot . x) ^2)))) is V11() V12() ext-real set
(1 / ((sin . x) ^2)) / (1 + ((cot . x) ^2)) is V11() V12() ext-real Element of REAL
K37((1 / ((sin . x) ^2)),K39((1 + ((cot . x) ^2)))) is V11() V12() ext-real set
- ((1 / ((sin . x) ^2)) / (1 + ((cot . x) ^2))) is V11() V12() ext-real Element of REAL
((cos . x) / (sin . x)) * ((cos . x) / (sin . x)) is V11() V12() ext-real Element of REAL
1 + (((cos . x) / (sin . x)) * ((cos . x) / (sin . x))) is V11() V12() ext-real Element of REAL
((sin . x) ^2) * (1 + (((cos . x) / (sin . x)) * ((cos . x) / (sin . x)))) is V11() V12() ext-real Element of REAL
1 / (((sin . x) ^2) * (1 + (((cos . x) / (sin . x)) * ((cos . x) / (sin . x))))) is V11() V12() ext-real Element of REAL
K39((((sin . x) ^2) * (1 + (((cos . x) / (sin . x)) * ((cos . x) / (sin . x)))))) is V11() V12() ext-real set
K37(1,K39((((sin . x) ^2) * (1 + (((cos . x) / (sin . x)) * ((cos . x) / (sin . x))))))) is V11() V12() ext-real set
- (1 / (((sin . x) ^2) * (1 + (((cos . x) / (sin . x)) * ((cos . x) / (sin . x)))))) is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is V11() V12() ext-real set
((cos . x) ^2) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K37(((cos . x) ^2),K39(((sin . x) ^2))) is V11() V12() ext-real set
1 + (((cos . x) ^2) / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
((sin . x) ^2) * (1 + (((cos . x) ^2) / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
1 / (((sin . x) ^2) * (1 + (((cos . x) ^2) / ((sin . x) ^2)))) is V11() V12() ext-real Element of REAL
K39((((sin . x) ^2) * (1 + (((cos . x) ^2) / ((sin . x) ^2))))) is V11() V12() ext-real set
K37(1,K39((((sin . x) ^2) * (1 + (((cos . x) ^2) / ((sin . x) ^2)))))) is V11() V12() ext-real set
- (1 / (((sin . x) ^2) * (1 + (((cos . x) ^2) / ((sin . x) ^2))))) is V11() V12() ext-real Element of REAL
((sin . x) ^2) * ((cos . x) ^2) is V11() V12() ext-real Element of REAL
(((sin . x) ^2) * ((cos . x) ^2)) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K37((((sin . x) ^2) * ((cos . x) ^2)),K39(((sin . x) ^2))) is V11() V12() ext-real set
((sin . x) ^2) + ((((sin . x) ^2) * ((cos . x) ^2)) / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
1 / (((sin . x) ^2) + ((((sin . x) ^2) * ((cos . x) ^2)) / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
K39((((sin . x) ^2) + ((((sin . x) ^2) * ((cos . x) ^2)) / ((sin . x) ^2)))) is V11() V12() ext-real set
K37(1,K39((((sin . x) ^2) + ((((sin . x) ^2) * ((cos . x) ^2)) / ((sin . x) ^2))))) is V11() V12() ext-real set
- (1 / (((sin . x) ^2) + ((((sin . x) ^2) * ((cos . x) ^2)) / ((sin . x) ^2)))) is V11() V12() ext-real Element of REAL
((sin . x) ^2) + ((cos . x) ^2) is V11() V12() ext-real Element of REAL
1 / (((sin . x) ^2) + ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
K39((((sin . x) ^2) + ((cos . x) ^2))) is V11() V12() ext-real set
K37(1,K39((((sin . x) ^2) + ((cos . x) ^2)))) is V11() V12() ext-real set
- (1 / (((sin . x) ^2) + ((cos . x) ^2))) is V11() V12() ext-real Element of REAL
1 / 1 is V1() V11() V12() ext-real positive non negative Element of REAL
K39(1) is V1() V11() V12() ext-real positive non negative set
K37(1,K39(1)) is V1() V11() V12() ext-real positive non negative set
- (1 / 1) is V1() V11() V12() ext-real non positive negative Element of REAL
x is V11() V12() ext-real Element of REAL
((arctan * cot) `| Z) . x is V11() V12() ext-real Element of REAL
arccot * cot is V19() V22( REAL ) V23( REAL ) V24() V36() V37() V38() Element of K6(K7(REAL,REAL))
dom (arccot * cot) is V46() V47() V48() Element of K6(REAL)
Z is open V46() V47() V48() Element of K6(REAL)
(arccot * cot) `| Z is V19() V22( REAL ) V23( REAL ) V24() V36() V37() V38() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((arccot * cot) `| Z) . x is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(cos . x) / (sin . x) is V11() V12() ext-real Element of REAL
K39((sin . x)) is V11() V12() ext-real set
K37((cos . x),K39((sin . x))) is V11() V12() ext-real set
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is V11() V12() ext-real set
diff ((arccot * cot),x) is V11() V12() ext-real Element of REAL
diff (cot,x) is V11() V12() ext-real Element of REAL
(cot . x) ^2 is V11() V12() ext-real Element of REAL
K37((cot . x),(cot . x)) is V11() V12() ext-real set
1 + ((cot . x) ^2) is V11() V12() ext-real Element of REAL
(diff (cot,x)) / (1 + ((cot . x) ^2)) is V11() V12() ext-real Element of REAL
K39((1 + ((cot . x) ^2))) is V11() V12() ext-real set
K37((diff (cot,x)),K39((1 + ((cot . x) ^2)))) is V11() V12() ext-real set
- ((diff (cot,x)) / (1 + ((cot . x) ^2))) is V11() V12() ext-real Element of REAL
1 / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() V12() ext-real set
K37(1,K39(((sin . x) ^2))) is V11() V12() ext-real set
- (1 / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
(- (1 / ((sin . x) ^2))) / (1 + ((cot . x) ^2)) is V11() V12() ext-real Element of REAL
K37((- (1 / ((sin . x) ^2))),K39((1 + ((cot . x) ^2)))) is V11() V12() ext-real set
- ((- (1 / ((sin . x) ^2))) / (1 + ((cot . x) ^2))) is V11() V12() ext-real Element of REAL
(1 / ((sin . x) ^2)) / (1 + ((cot . x) ^2)) is V11() V12() ext-real Element of REAL
K37((1 / ((sin . x) ^2)),K39((1 + ((cot . x) ^2)))) is V11() V12() ext-real set
((cos . x) / (sin . x)) * ((cos . x) / (sin . x)) is V11() V12() ext-real Element of REAL
1 + (((cos . x) / (sin . x)) * ((cos . x) / (sin . x))) is V11() V12() ext-real Element of REAL
((sin . x) ^2) * (1 + (((cos . x) / (sin . x)) * ((cos . x) / (sin . x)))) is V11() V12() ext-real Element of REAL
1 / (((sin . x) ^2) * (1 + (((cos . x) / (sin . x)) * ((cos . x) / (sin . x))))) is V11() V12() ext-real Element of REAL
K39((((sin . x) ^2) * (1 + (((cos . x) / (sin . x)) * ((cos . x) / (sin . x)))))) is V11() V12() ext-real set
K37(1,K39((((sin . x) ^2) * (1 + (((cos . x) / (sin . x)) * ((cos . x) / (sin . x))))))) is V11() V12() ext-real set
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is V11() V12() ext-real set
((cos . x) ^2) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K37(((cos . x) ^2),K39(((sin . x) ^2))) is V11() V12() ext-real set
1 + (((cos . x) ^2) / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
((sin . x) ^2) * (1 + (((cos . x) ^2) / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
1 / (((sin . x) ^2) * (1 + (((cos . x) ^2) / ((sin . x) ^2)))) is V11() V12() ext-real Element of REAL
K39((((sin . x) ^2) * (1 + (((cos . x) ^2) / ((sin . x) ^2))))) is V11() V12() ext-real set
K37(1,K39((((sin . x) ^2) * (1 + (((cos . x) ^2) / ((sin . x) ^2)))))) is V11() V12() ext-real set
((sin . x) ^2) * ((cos . x) ^2) is V11() V12() ext-real Element of REAL
(((sin . x) ^2) * ((cos . x) ^2)) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K37((((sin . x) ^2) * ((cos . x) ^2)),K39(((sin . x) ^2))) is V11() V12() ext-real set
((sin . x) ^2) + ((((sin . x) ^2) * ((cos . x) ^2)) / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
1 / (((sin . x) ^2) + ((((sin . x) ^2) * ((cos . x) ^2)) / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
K39((((sin . x) ^2) + ((((sin . x) ^2) * ((cos . x) ^2)) / ((sin . x) ^2)))) is V11() V12() ext-real set
K37(1,K39((((sin . x) ^2) + ((((sin . x) ^2) * ((cos . x) ^2)) / ((sin . x) ^2))))) is V11() V12() ext-real set
((sin . x) ^2) + ((cos . x) ^2) is V11() V12() ext-real Element of REAL
1 / (((sin . x) ^2) + ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
K39((((sin . x) ^2) + ((cos . x) ^2))) is V11() V12() ext-real set
K37(1,K39((((sin . x) ^2) + ((cos . x) ^2)))) is V11() V12() ext-real set
1 / 1 is V1() V11() V12() ext-real positive non negative Element of REAL
K39(1) is V1() V11() V12() ext-real positive non negative set
K37(1,K39(1)) is V1() V11() V12() ext-real positive non negative set
x is V11() V12() ext-real Element of REAL
((arccot * cot) `| Z) . x is V11() V12() ext-real Element of REAL
arctan * arctan is V19() V22( REAL ) V23( REAL ) V24() V36() V37() V38() Element of K6(K7(REAL,REAL))
dom (arctan * arctan) is V46() V47() V48() Element of K6(REAL)
Z is open V46() V47() V48() Element of K6(REAL)
(arctan * arctan) `| Z is V19() V22( REAL ) V23( REAL ) V24() V36() V37() V38() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
arctan . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((arctan * arctan) `| Z) . x is V11() V12() ext-real Element of REAL
x ^2 is V11() V12() ext-real Element of REAL
K37(x,x) is V11() V12() ext-real set
1 + (x ^2) is V11() V12() ext-real Element of REAL
arctan . x is V11() V12() ext-real Element of REAL
(arctan . x) ^2 is V11() V12() ext-real Element of REAL
K37((arctan . x),(arctan . x)) is V11() V12() ext-real set
1 + ((arctan . x) ^2) is V11() V12() ext-real Element of REAL
(1 + (x ^2)) * (1 + ((arctan . x) ^2)) is V11() V12() ext-real Element of REAL
1 / ((1 + (x ^2)) * (1 + ((arctan . x) ^2))) is V11() V12() ext-real Element of REAL
K39(((1 + (x ^2)) * (1 + ((arctan . x) ^2)))) is V11() V12() ext-real set
K37(1,K39(((1 + (x ^2)) * (1 + ((arctan . x) ^2))))) is V11() V12() ext-real set
diff ((arctan * arctan),x) is V11() V12() ext-real Element of REAL
diff (arctan,x) is V11() V12() ext-real Element of REAL
(diff (arctan,x)) / (1 + ((arctan . x) ^2)) is V11() V12() ext-real Element of REAL
K39((1 + ((arctan . x) ^2))) is V11() V12() ext-real set
K37((diff (arctan,x)),K39((1 + ((arctan . x) ^2)))) is V11() V12() ext-real set
arctan `| Z is V19() V22( REAL ) V23( REAL ) V24() V36() V37() V38() Element of K6(K7(REAL,REAL))
(arctan `| Z) . x is V11() V12() ext-real Element of REAL
((arctan `| Z) . x) / (1 + ((arctan . x) ^2)) is V11() V12() ext-real Element of REAL
K37(((arctan `| Z) . x),K39((1 + ((arctan . x) ^2)))) is V11() V12() ext-real set
1 / (1 + (x ^2)) is V11() V12() ext-real Element of REAL
K39((1 + (x ^2))) is V11() V12() ext-real set
K37(1,K39((1 + (x ^2)))) is V11() V12() ext-real set
(1 / (1 + (x ^2))) / (1 + ((arctan . x) ^2)) is V11() V12() ext-real Element of REAL
K37((1 / (1 + (x ^2))),K39((1 + ((arctan . x) ^2)))) is V11() V12() ext-real set
x is V11() V12() ext-real Element of REAL
((arctan * arctan) `| Z) . x is V11() V12() ext-real Element of REAL
x ^2 is V11() V12() ext-real Element of REAL
K37(x,x) is V11() V12() ext-real set
1 + (x ^2) is V11() V12() ext-real Element of REAL
arctan . x is V11() V12() ext-real Element of REAL
(arctan . x) ^2 is V11() V12() ext-real Element of REAL
K37((arctan . x),(arctan . x)) is V11() V12() ext-real set
1 + ((arctan . x) ^2) is V11() V12() ext-real Element of REAL
(1 + (x ^2)) * (1 + ((arctan . x) ^2)) is V11() V12() ext-real Element of REAL
1 / ((1 + (x ^2)) * (1 + ((arctan . x) ^2))) is V11() V12() ext-real Element of REAL
K39(((1 + (x ^2)) * (1 + ((arctan . x) ^2)))) is V11() V12() ext-real set
K37(1,K39(((1 + (x ^2)) * (1 + ((arctan . x) ^2))))) is V11() V12() ext-real set
arccot * arctan is V19() V22( REAL ) V23( REAL ) V24() V36() V37() V38() Element of K6(K7(REAL,REAL))
dom (arccot * arctan) is V46() V47() V48() Element of K6(REAL)
Z is open V46() V47() V48() Element of K6(REAL)
(arccot * arctan) `| Z is V19() V22( REAL ) V23( REAL ) V24() V36() V37() V38() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
arctan . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((arccot * arctan) `| Z) . x is V11() V12() ext-real Element of REAL
x ^2 is V11() V12() ext-real Element of REAL
K37(x,x) is V11() V12() ext-real set
1 + (x ^2) is V11() V12() ext-real Element of REAL
arctan . x is V11() V12() ext-real Element of REAL
(arctan . x) ^2 is V11() V12() ext-real Element of REAL
K37((arctan . x),(arctan . x)) is V11() V12() ext-real set
1 + ((arctan . x) ^2) is V11() V12() ext-real Element of REAL
(1 + (x ^2)) * (1 + ((arctan . x) ^2)) is V11() V12() ext-real Element of REAL
1 / ((1 + (x ^2)) * (1 + ((arctan . x) ^2))) is V11() V12() ext-real Element of REAL
K39(((1 + (x ^2)) * (1 + ((arctan . x) ^2)))) is V11() V12() ext-real set
K37(1,K39(((1 + (x ^2)) * (1 + ((arctan . x) ^2))))) is V11() V12() ext-real set
- (1 / ((1 + (x ^2)) * (1 + ((arctan . x) ^2)))) is V11() V12() ext-real Element of REAL
diff ((arccot * arctan),x) is V11() V12() ext-real Element of REAL
diff (arctan,x) is V11() V12() ext-real Element of REAL
(diff (arctan,x)) / (1 + ((arctan . x) ^2)) is V11() V12() ext-real Element of REAL
K39((1 + ((arctan . x) ^2))) is V11() V12() ext-real set
K37((diff (arctan,x)),K39((1 + ((arctan . x) ^2)))) is V11() V12() ext-real set
- ((diff (arctan,x)) / (1 + ((arctan . x) ^2))) is V11() V12() ext-real Element of REAL
arctan `| Z is V19() V22( REAL ) V23( REAL ) V24() V36() V37() V38() Element of K6(K7(REAL,REAL))
(arctan `| Z) . x is V11() V12() ext-real Element of REAL
((arctan `| Z) . x) / (1 + ((arctan . x) ^2)) is V11() V12() ext-real Element of REAL
K37(((arctan `| Z) . x),K39((1 + ((arctan . x) ^2)))) is V11() V12() ext-real set
- (((arctan `| Z) . x) / (1 + ((arctan . x) ^2))) is V11() V12() ext-real Element of REAL
1 / (1 + (x ^2)) is V11() V12() ext-real Element of REAL
K39((1 + (x ^2))) is V11() V12() ext-real set
K37(1,K39((1 + (x ^2)))) is V11() V12() ext-real set
(1 / (1 + (x ^2))) / (1 + ((arctan . x) ^2)) is V11() V12() ext-real Element of REAL
K37((1 / (1 + (x ^2))),K39((1 + ((arctan . x) ^2)))) is V11() V12() ext-real set
- ((1 / (1 + (x ^2))) / (1 + ((arctan . x) ^2))) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((arccot * arctan) `| Z) . x is V11() V12() ext-real Element of REAL
x ^2 is V11() V12() ext-real Element of REAL
K37(x,x) is V11() V12() ext-real set
1 + (x ^2) is V11() V12() ext-real Element of REAL
arctan . x is V11() V12() ext-real Element of REAL
(arctan . x) ^2 is V11() V12() ext-real Element of REAL
K37((arctan . x),(arctan . x)) is V11() V12() ext-real set
1 + ((arctan . x) ^2) is V11() V12() ext-real Element of REAL
(1 + (x ^2)) * (1 + ((arctan . x) ^2)) is V11() V12() ext-real Element of REAL
1 / ((1 + (x ^2)) * (1 + ((arctan . x) ^2))) is V11() V12() ext-real Element of REAL
K39(((1 + (x ^2)) * (1 + ((arctan . x) ^2)))) is V11() V12() ext-real set
K37(1,K39(((1 + (x ^2)) * (1 + ((arctan . x) ^2))))) is V11() V12() ext-real set
- (1 / ((1 + (x ^2)) * (1 + ((arctan . x) ^2)))) is V11() V12() ext-real Element of REAL
arctan * arccot is V19() V22( REAL ) V23( REAL ) V24() V36() V37() V38() Element of K6(K7(REAL,REAL))
dom (arctan * arccot) is V46() V47() V48() Element of K6(REAL)
Z is open V46() V47() V48() Element of K6(REAL)
(arctan * arccot) `| Z is V19() V22( REAL ) V23( REAL ) V24() V36() V37() V38() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
arccot . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((arctan * arccot) `| Z) . x is V11() V12() ext-real Element of REAL
x ^2 is V11() V12() ext-real Element of REAL
K37(x,x) is V11() V12() ext-real set
1 + (x ^2) is V11() V12() ext-real Element of REAL
arccot . x is V11() V12() ext-real Element of REAL
(arccot . x) ^2 is V11() V12() ext-real Element of REAL
K37((arccot . x),(arccot . x)) is V11() V12() ext-real set
1 + ((arccot . x) ^2) is V11() V12() ext-real Element of REAL
(1 + (x ^2)) * (1 + ((arccot . x) ^2)) is V11() V12() ext-real Element of REAL
1 / ((1 + (x ^2)) * (1 + ((arccot . x) ^2))) is V11() V12() ext-real Element of REAL
K39(((1 + (x ^2)) * (1 + ((arccot . x) ^2)))) is V11() V12() ext-real set
K37(1,K39(((1 + (x ^2)) * (1 + ((arccot . x) ^2))))) is V11() V12() ext-real set
- (1 / ((1 + (x ^2)) * (1 + ((arccot . x) ^2)))) is V11() V12() ext-real Element of REAL
diff ((arctan * arccot),x) is V11() V12() ext-real Element of REAL
diff (arccot,x) is V11() V12() ext-real Element of REAL
(diff (arccot,x)) / (1 + ((arccot . x) ^2)) is V11() V12() ext-real Element of REAL
K39((1 + ((arccot . x) ^2))) is V11() V12() ext-real set
K37((diff (arccot,x)),K39((1 + ((arccot . x) ^2)))) is V11() V12() ext-real set
arccot `| Z is V19() V22( REAL ) V23( REAL ) V24() V36() V37() V38() Element of K6(K7(REAL,REAL))
(arccot `| Z) . x is V11() V12() ext-real Element of REAL
((arccot `| Z) . x) / (1 + ((arccot . x) ^2)) is V11() V12() ext-real Element of REAL
K37(((arccot `| Z) . x),K39((1 + ((arccot . x) ^2)))) is V11() V12() ext-real set
1 / (1 + (x ^2)) is V11() V12() ext-real Element of REAL
K39((1 + (x ^2))) is V11() V12() ext-real set
K37(1,K39((1 + (x ^2)))) is V11() V12() ext-real set
- (1 / (1 + (x ^2))) is V11() V12() ext-real Element of REAL
(- (1 / (1 + (x ^2)))) / (1 + ((arccot . x) ^2)) is V11() V12() ext-real Element of REAL
K37((- (1 / (1 + (x ^2)))),K39((1 + ((arccot . x) ^2)))) is V11() V12() ext-real set
(1 / (1 + (x ^2))) / (1 + ((arccot . x) ^2)) is V11() V12() ext-real Element of REAL
K37((1 / (1 + (x ^2))),K39((1 + ((arccot . x) ^2)))) is V11() V12() ext-real set
- ((1 / (1 + (x ^2))) / (1 + ((arccot . x) ^2))) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((arctan * arccot) `| Z) . x is V11() V12() ext-real Element of REAL
x ^2 is V11() V12() ext-real Element of REAL
K37(x,x) is V11() V12() ext-real set
1 + (x ^2) is V11() V12() ext-real Element of REAL
arccot . x is V11() V12() ext-real Element of REAL
(arccot . x) ^2 is V11() V12() ext-real Element of REAL
K37((arccot . x),(arccot . x)) is V11() V12() ext-real set
1 + ((arccot . x) ^2) is V11() V12() ext-real Element of REAL
(1 + (x ^2)) * (1 + ((arccot . x) ^2)) is V11() V12() ext-real Element of REAL
1 / ((1 + (x ^2)) * (1 + ((arccot . x) ^2))) is V11() V12() ext-real Element of REAL
K39(((1 + (x ^2)) * (1 + ((arccot . x) ^2)))) is V11() V12() ext-real set
K37(1,K39(((1 + (x ^2)) * (1 + ((arccot . x) ^2))))) is V11() V12() ext-real set
- (1 / ((1 + (x ^2)) * (1 + ((arccot . x) ^2)))) is V11() V12() ext-real Element of REAL
arccot * arccot is V19() V22( REAL ) V23( REAL ) V24() V36() V37() V38() Element of K6(K7(REAL,REAL))
dom (arccot * arccot) is V46() V47() V48() Element of K6(REAL)
Z is open V46() V47() V48() Element of K6(REAL)
(arccot * arccot) `| Z is V19() V22( REAL ) V23( REAL ) V24() V36() V37() V38() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
arccot . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((arccot * arccot) `| Z) . x is V11() V12() ext-real Element of REAL
x ^2 is V11() V12() ext-real Element of REAL
K37(x,x) is V11() V12() ext-real set
1 + (x ^2) is V11() V12() ext-real Element of REAL
arccot . x is V11() V12() ext-real Element of REAL
(arccot . x) ^2 is V11() V12() ext-real Element of REAL
K37((arccot . x),(arccot . x)) is V11() V12() ext-real set
1 + ((arccot . x) ^2) is V11() V12() ext-real Element of REAL
(1 + (x ^2)) * (1 + ((arccot . x) ^2)) is V11() V12() ext-real Element of REAL
1 / ((1 + (x ^2)) * (1 + ((arccot . x) ^2))) is V11() V12() ext-real Element of REAL
K39(((1 + (x ^2)) * (1 + ((arccot . x) ^2)))) is V11() V12() ext-real set
K37(1,K39(((1 + (x ^2)) * (1 + ((arccot . x) ^2))))) is V11() V12() ext-real set
diff ((arccot * arccot),x) is V11() V12() ext-real Element of REAL
diff (arccot,x) is V11() V12() ext-real Element of REAL
(diff (arccot,x)) / (1 + ((arccot . x) ^2)) is V11() V12() ext-real Element of REAL
K39((1 + ((arccot . x) ^2))) is V11() V12() ext-real set
K37((diff (arccot,x)),K39((1 + ((arccot . x) ^2)))) is V11() V12() ext-real set
- ((diff (arccot,x)) / (1 + ((arccot . x) ^2))) is V11() V12() ext-real Element of REAL
arccot `| Z is V19() V22( REAL ) V23( REAL ) V24() V36() V37() V38() Element of K6(K7(REAL,REAL))
(arccot `| Z) . x is V11() V12() ext-real Element of REAL
((arccot `| Z) . x) / (1 + ((arccot . x) ^2)) is V11() V12() ext-real Element of REAL
K37(((arccot `| Z) . x),K39((1 + ((arccot . x) ^2)))) is V11() V12() ext-real set
- (((arccot `| Z) . x) / (1 + ((arccot . x) ^2))) is V11() V12() ext-real Element of REAL
1 / (1 + (x ^2)) is V11() V12() ext-real Element of REAL
K39((1 + (x ^2))) is V11() V12() ext-real set
K37(1,K39((1 + (x ^2)))) is V11() V12() ext-real set
- (1 / (1 + (x ^2))) is V11() V12() ext-real Element of REAL
(- (1 / (1 + (x ^2)))) / (1 + ((arccot . x) ^2)) is V11() V12() ext-real Element of REAL
K37((- (1 / (1 + (x ^2)))),K39((1 + ((arccot . x) ^2)))) is V11() V12() ext-real set
- ((- (1 / (1 + (x ^2)))) / (1 + ((arccot . x) ^2))) is V11() V12() ext-real Element of REAL
(1 / (1 + (x ^2))) / (1 + ((arccot . x) ^2)) is V11() V12() ext-real Element of REAL
K37((1 / (1 + (x ^2))),K39((1 + ((arccot . x) ^2)))) is V11() V12() ext-real set
x is V11() V12() ext-real Element of REAL
((arccot * arccot) `| Z) . x is V11() V12() ext-real Element of REAL
x ^2 is V11() V12() ext-real Element of REAL
K37(x,x) is V11() V12() ext-real set
1 + (x ^2) is V11() V12() ext-real Element of REAL
arccot . x is V11() V12() ext-real Element of REAL
(arccot . x) ^2 is V11() V12() ext-real Element of REAL
K37((arccot . x),(arccot . x)) is V11() V12() ext-real set
1 + ((arccot . x) ^2) is V11() V12() ext-real Element of REAL
(1 + (x ^2)) * (1 + ((arccot . x) ^2)) is V11() V12() ext-real Element of REAL
1 / ((1 + (x ^2)) * (1 + ((arccot . x) ^2))) is V11() V12() ext-real Element of REAL
K39(((1 + (x ^2)) * (1 + ((arccot . x) ^2)))) is V11() V12() ext-real set